theory Nondet_Lemmas

lemma whileLoop_unroll:
  "whileLoop C B r = condition (C r) (B r >>= whileLoop C B) (return r)"
  (is "?LHS r = ?RHS r") proof - have "\<And>r s. \<not> C r s \<Longrightarrow> ?LHS r s = ?RHS r s" by (clarsimp simp: whileLoop_cond_fail condition_def bind_def return_def) moreover have "\<And>r s. C r s \<Longrightarrow> ?LHS r s = (B r >>= whileLoop C B) s" apply (rule monad_state_eqI) apply (clarsimp simp: whileLoop_def bind_def split_def) apply (subst (asm) whileLoop_results_simps_valid) apply fastforce apply (clarsimp simp: whileLoop_def bind_def split_def) apply (subst whileLoop_results.simps) apply fastforce apply (clarsimp simp: whileLoop_def bind_def split_def) apply (subst whileLoop_results.simps) apply (subst whileLoop_terminates.simps) apply fastforce done ultimately show ?thesis by (fastforce simp: condition_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. whileLoop C
  B r = condition (C r)
  (B r >>= whileLoop C
  B)
  (return r) proof (state)
goal (1 subgoal):
 1. whileLoop C
  B r = condition (C r)
  (B r >>= whileLoop C
  B)
  (return r) proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<not> C r s \<Longrightarrow> whileLoop C
  B r s = condition (C r)
  (B r >>= whileLoop C
  B)
  (return r) s proof (state)
this:
\<not> C ?r ?s \<Longrightarrow> whileLoop C
  B ?r ?s = condition (C ?r)
  (B ?r >>= whileLoop C
  B)
  (return ?r) ?s

goal (1 subgoal):
 1. whileLoop C
  B r = condition (C r)
  (B r >>= whileLoop C
  B)
  (return r) proof (state)
this:
\<not> C ?r ?s \<Longrightarrow> whileLoop C
  B ?r ?s = condition (C ?r)
  (B ?r >>= whileLoop C
  B)
  (return ?r) ?s

goal (1 subgoal):
 1. whileLoop C
  B r = condition (C r)
  (B r >>= whileLoop C
  B)
  (return r) proof (prove)
goal (1 subgoal):
 1. \<And>r s. C r s \<Longrightarrow> whileLoop C
  B r s = (B r >>= whileLoop C
  B) s proof (prove)
goal (3 subgoals):
 1. \<And>r s ra t. \<lbrakk>C r s; (ra, t) \<in> fst (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> (ra, t) \<in> fst ((B r >>= whileLoop C
  B) s)
 2. \<And>r s ra t. \<lbrakk>C r s; (ra, t) \<in> fst ((B r >>= whileLoop C
  B) s)\<rbrakk> \<Longrightarrow> (ra, t) \<in> fst (whileLoop C
  B r s)
 3. \<And>r s. C r s \<Longrightarrow> snd (whileLoop C
  B r s) = snd ((B r >>= whileLoop C
  B) s) proof (prove)
goal (3 subgoals):
 1. \<And>r s ra t. \<lbrakk>C r s; (Some (r, s), Some (ra, t)) \<in> whileLoop_results C B\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B r s). (Some x, Some (ra, t)) \<in> whileLoop_results C B
 2. \<And>r s ra t. \<lbrakk>C r s; (ra, t) \<in> fst ((B r >>= whileLoop C
  B) s)\<rbrakk> \<Longrightarrow> (ra, t) \<in> fst (whileLoop C
  B r s)
 3. \<And>r s. C r s \<Longrightarrow> snd (whileLoop C
  B r s) = snd ((B r >>= whileLoop C
  B) s) proof (prove)
goal (3 subgoals):
 1. \<And>r s ra t. \<lbrakk>C r s; (\<exists>rb sa. (r, s) = (rb, sa) \<and> (ra, t) = (rb, sa) \<and> \<not> C rb sa) \<or> (\<exists>rb sa. (r, s) = (rb, sa) \<and> C rb sa \<and> (\<exists>r' s'. (r', s') \<in> fst (B rb sa) \<and> (Some (r', s'), Some (ra, t)) \<in> whileLoop_results C B))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (B r s). (Some x, Some (ra, t)) \<in> whileLoop_results C B
 2. \<And>r s ra t. \<lbrakk>C r s; (ra, t) \<in> fst ((B r >>= whileLoop C
  B) s)\<rbrakk> \<Longrightarrow> (ra, t) \<in> fst (whileLoop C
  B r s)
 3. \<And>r s. C r s \<Longrightarrow> snd (whileLoop C
  B r s) = snd ((B r >>= whileLoop C
  B) s) proof (prove)
goal (2 subgoals):
 1. \<And>r s ra t. \<lbrakk>C r s; (ra, t) \<in> fst ((B r >>= whileLoop C
  B) s)\<rbrakk> \<Longrightarrow> (ra, t) \<in> fst (whileLoop C
  B r s)
 2. \<And>r s. C r s \<Longrightarrow> snd (whileLoop C
  B r s) = snd ((B r >>= whileLoop C
  B) s) proof (prove)
goal (2 subgoals):
 1. \<And>r s ra t a b. \<lbrakk>C r s; (a, b) \<in> fst (B r s); (Some (a, b), Some (ra, t)) \<in> whileLoop_results C B\<rbrakk> \<Longrightarrow> (Some (r, s), Some (ra, t)) \<in> whileLoop_results C B
 2. \<And>r s. C r s \<Longrightarrow> snd (whileLoop C
  B r s) = snd ((B r >>= whileLoop C
  B) s) proof (prove)
goal (2 subgoals):
 1. \<And>r s ra t a b. \<lbrakk>C r s; (a, b) \<in> fst (B r s); (Some (a, b), Some (ra, t)) \<in> whileLoop_results C B\<rbrakk> \<Longrightarrow> (\<exists>rb sa. Some (r, s) = Some (rb, sa) \<and> Some (ra, t) = Some (rb, sa) \<and> \<not> C rb sa) \<or> (\<exists>rb sa. Some (r, s) = Some (rb, sa) \<and> Some (ra, t) = None \<and> C rb sa \<and> snd (B rb sa)) \<or> (\<exists>rb sa r' s' z. Some (r, s) = Some (rb, sa) \<and> Some (ra, t) = z \<and> C rb sa \<and> (r', s') \<in> fst (B rb sa) \<and> (Some (r', s'), z) \<in> whileLoop_results C B)
 2. \<And>r s. C r s \<Longrightarrow> snd (whileLoop C
  B r s) = snd ((B r >>= whileLoop C
  B) s) proof (prove)
goal (1 subgoal):
 1. \<And>r s. C r s \<Longrightarrow> snd (whileLoop C
  B r s) = snd ((B r >>= whileLoop C
  B) s) proof (prove)
goal (1 subgoal):
 1. \<And>r s. C r s \<Longrightarrow> ((Some (r, s), None) \<in> whileLoop_results C B \<or> \<not> whileLoop_terminates C B r s) = ((\<exists>x\<in>fst (B r s). (Some x, None) \<in> whileLoop_results C B \<or> \<not> whileLoop_terminates C B (fst x) (snd x)) \<or> snd (B r s)) proof (prove)
goal (1 subgoal):
 1. \<And>r s. C r s \<Longrightarrow> (((\<exists>ra sa. Some (r, s) = Some (ra, sa) \<and> None = Some (ra, sa) \<and> \<not> C ra sa) \<or> (\<exists>ra sa. Some (r, s) = Some (ra, sa) \<and> None = None \<and> C ra sa \<and> snd (B ra sa)) \<or> (\<exists>ra sa r' s' z. Some (r, s) = Some (ra, sa) \<and> None = z \<and> C ra sa \<and> (r', s') \<in> fst (B ra sa) \<and> (Some (r', s'), z) \<in> whileLoop_results C B)) \<or> \<not> whileLoop_terminates C B r s) = ((\<exists>x\<in>fst (B r s). (Some x, None) \<in> whileLoop_results C B \<or> \<not> whileLoop_terminates C B (fst x) (snd x)) \<or> snd (B r s)) proof (prove)
goal (1 subgoal):
 1. \<And>r s. C r s \<Longrightarrow> (((\<exists>ra sa. Some (r, s) = Some (ra, sa) \<and> None = Some (ra, sa) \<and> \<not> C ra sa) \<or> (\<exists>ra sa. Some (r, s) = Some (ra, sa) \<and> None = None \<and> C ra sa \<and> snd (B ra sa)) \<or> (\<exists>ra sa r' s' z. Some (r, s) = Some (ra, sa) \<and> None = z \<and> C ra sa \<and> (r', s') \<in> fst (B ra sa) \<and> (Some (r', s'), z) \<in> whileLoop_results C B)) \<or> \<not> ((\<exists>ra sa. r = ra \<and> s = sa \<and> \<not> C ra sa) \<or> (\<exists>ra sa. r = ra \<and> s = sa \<and> C ra sa \<and> (\<forall>(x, y)\<in>fst (B ra sa). whileLoop_terminates C B x y)))) = ((\<exists>x\<in>fst (B r s). (Some x, None) \<in> whileLoop_results C B \<or> \<not> whileLoop_terminates C B (fst x) (snd x)) \<or> snd (B r s)) proof (prove)
goal:
No subgoals! proof (state)
this:
C ?r ?s \<Longrightarrow> whileLoop C
  B ?r ?s = (B ?r >>= whileLoop C
  B) ?s

goal (1 subgoal):
 1. whileLoop C
  B r = condition (C r)
  (B r >>= whileLoop C
  B)
  (return r) proof (chain)
picking this:
\<not> C ?r ?s \<Longrightarrow> whileLoop C
  B ?r ?s = condition (C ?r)
  (B ?r >>= whileLoop C
  B)
  (return ?r) ?s
C ?r ?s \<Longrightarrow> whileLoop C
  B ?r ?s = (B ?r >>= whileLoop C
  B) ?s proof (prove)
using this:
\<not> C ?r ?s \<Longrightarrow> whileLoop C
  B ?r ?s = condition (C ?r)
  (B ?r >>= whileLoop C
  B)
  (return ?r) ?s
C ?r ?s \<Longrightarrow> whileLoop C
  B ?r ?s = (B ?r >>= whileLoop C
  B) ?s

goal (1 subgoal):
 1. whileLoop C
  B r = condition (C r)
  (B r >>= whileLoop C
  B)
  (return r) proof (state)
this:
whileLoop C
  B r = condition (C r)
  (B r >>= whileLoop C
  B)
  (return r)

goal:
No subgoals!