theory Nondet_While_Loop_Rules

lemma in_whileLoop_induct[consumes 1]:
  assumes in_whileLoop: "(r', s') \<in> fst (whileLoop C B r s)"
  and init_I: "\<And> r s. \<not> C r s \<Longrightarrow> I r s r s"
  and step: "\<And>r s r' s' r'' s''. \<lbrakk> C r s; (r', s') \<in> fst (B r s);
                                   (r'', s'') \<in> fst (whileLoop C B r' s');
                                   I r' s' r'' s'' \<rbrakk> \<Longrightarrow> I r s r'' s''"
  shows "I r s r' s'" proof cases assume "C r s" { obtain a where a_def: "a = Some (r, s)" by blast obtain b where b_def: "b = Some (r', s')" by blast have "\<lbrakk> (a, b) \<in> whileLoop_results C B; \<exists>x. a = Some x;  \<exists>x. b = Some x \<rbrakk>
          \<Longrightarrow> I (fst (the a)) (snd (the a)) (fst (the b)) (snd (the b))" by (induct rule: whileLoop_results.induct)
         (auto simp: init_I whileLoop_def intro: step) hence "(Some (r, s), Some (r', s')) \<in> whileLoop_results C B \<Longrightarrow> I r s r' s'" by (clarsimp simp: a_def b_def) } thus ?thesis using in_whileLoop by (clarsimp simp: whileLoop_def) next assume "\<not> C r s" hence "r' = r \<and> s' = s" using in_whileLoop by (subst (asm) whileLoop_unroll, clarsimp simp: condition_def return_def) thus ?thesis by (metis init_I \<open>\<not> C r s\<close>) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. I r s r' s' proof (state)
goal (2 subgoals):
 1. ?P \<Longrightarrow> I r s r' s'
 2. \<not> ?P \<Longrightarrow> I r s r' s' proof (state)
this:
C r s

goal (2 subgoals):
 1. ?P \<Longrightarrow> I r s r' s'
 2. \<not> ?P \<Longrightarrow> I r s r' s' proof (state)
this:
C r s

goal (2 subgoals):
 1. ?P \<Longrightarrow> I r s r' s'
 2. \<not> ?P \<Longrightarrow> I r s r' s' proof (prove)
goal (1 subgoal):
 1. (\<And>a. a = Some (r, s) \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
a = Some (r, s)

goal (2 subgoals):
 1. ?P \<Longrightarrow> I r s r' s'
 2. \<not> ?P \<Longrightarrow> I r s r' s' proof (prove)
goal (1 subgoal):
 1. (\<And>b. b = Some (r', s') \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
b = Some (r', s')

goal (2 subgoals):
 1. ?P \<Longrightarrow> I r s r' s'
 2. \<not> ?P \<Longrightarrow> I r s r' s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, b) \<in> whileLoop_results C B; \<exists>x. a = Some x; \<exists>x. b = Some x\<rbrakk> \<Longrightarrow> I (fst (the a)) (snd (the a)) (fst (the b)) (snd (the b)) proof (state)
this:
\<lbrakk>(a, b) \<in> whileLoop_results C B; \<exists>x. a = Some x; \<exists>x. b = Some x\<rbrakk> \<Longrightarrow> I (fst (the a)) (snd (the a)) (fst (the b)) (snd (the b))

goal (2 subgoals):
 1. ?P \<Longrightarrow> I r s r' s'
 2. \<not> ?P \<Longrightarrow> I r s r' s' proof (prove)
using this:
\<lbrakk>(a, b) \<in> whileLoop_results C B; \<exists>x. a = Some x; \<exists>x. b = Some x\<rbrakk> \<Longrightarrow> I (fst (the a)) (snd (the a)) (fst (the b)) (snd (the b))

goal (1 subgoal):
 1. (Some (r, s), Some (r', s')) \<in> whileLoop_results C B \<Longrightarrow> I r s r' s' proof (state)
this:
(Some (r, s), Some (r', s')) \<in> whileLoop_results C B \<Longrightarrow> I r s r' s'

goal (2 subgoals):
 1. ?P \<Longrightarrow> I r s r' s'
 2. \<not> ?P \<Longrightarrow> I r s r' s' proof (state)
this:
(Some (r, s), Some (r', s')) \<in> whileLoop_results C B \<Longrightarrow> I r s r' s'

goal (2 subgoals):
 1. ?P \<Longrightarrow> I r s r' s'
 2. \<not> ?P \<Longrightarrow> I r s r' s' proof (prove)
using this:
(Some (r, s), Some (r', s')) \<in> whileLoop_results C B \<Longrightarrow> I r s r' s'

goal (1 subgoal):
 1. I r s r' s' proof (prove)
using this:
(Some (r, s), Some (r', s')) \<in> whileLoop_results C B \<Longrightarrow> I r s r' s'
(r', s') \<in> fst (whileLoop C
  B r s)

goal (1 subgoal):
 1. I r s r' s' proof (state)
this:
I r s r' s'

goal (1 subgoal):
 1. \<not> C r s \<Longrightarrow> I r s r' s' proof (state)
goal (1 subgoal):
 1. \<not> C r s \<Longrightarrow> I r s r' s' proof (state)
this:
\<not> C r s

goal (1 subgoal):
 1. \<not> C r s \<Longrightarrow> I r s r' s' proof (prove)
using this:
\<not> C r s

goal (1 subgoal):
 1. r' = r \<and> s' = s proof (prove)
using this:
\<not> C r s
(r', s') \<in> fst (whileLoop C
  B r s)

goal (1 subgoal):
 1. r' = r \<and> s' = s proof (state)
this:
r' = r \<and> s' = s

goal (1 subgoal):
 1. \<not> C r s \<Longrightarrow> I r s r' s' proof (prove)
using this:
r' = r \<and> s' = s

goal (1 subgoal):
 1. I r s r' s' proof (state)
this:
I r s r' s'

goal:
No subgoals!