theory Nondet_While_Loop_Rules

lemma snd_whileLoop_induct [consumes 1]:
  assumes induct: "snd (whileLoop C B r s)"
  and terminates: "\<not> whileLoop_terminates C B r s \<Longrightarrow> I r s"
  and init: "\<And> r s. \<lbrakk> snd (B r s); C r s \<rbrakk> \<Longrightarrow> I r s"
  and step: "\<And>r s r' s' r'' s''. \<lbrakk> C r s; (r', s') \<in> fst (B r s); snd (whileLoop C B r' s');
                                   I r' s' \<rbrakk> \<Longrightarrow> I r s"
  shows "I r s" apply (insert init induct) apply atomize apply (unfold whileLoop_def) apply clarsimp apply (erule disjE) apply (erule rev_mp) apply (induct "Some (r, s)" "None :: ('a \<times> 'b) option" arbitrary: r s rule: whileLoop_results.induct) apply clarsimp apply clarsimp apply (erule (1) step) apply (clarsimp simp: whileLoop_def) apply clarsimp apply (metis terminates) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. I r s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r s. \<lbrakk>snd (B r s); C r s\<rbrakk> \<Longrightarrow> I r s; snd (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> I r s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s; snd (whileLoop C
  B r s)\<rbrakk> \<Longrightarrow> I r s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s; snd ({(r', s'). (Some (r, s), Some (r', s')) \<in> whileLoop_results C B}, (Some (r, s), None) \<in> whileLoop_results C B \<or> \<not> whileLoop_terminates C B r s)\<rbrakk> \<Longrightarrow> I r s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s; (Some (r, s), None) \<in> whileLoop_results C B \<or> \<not> whileLoop_terminates C B r s\<rbrakk> \<Longrightarrow> I r s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s; (Some (r, s), None) \<in> whileLoop_results C B\<rbrakk> \<Longrightarrow> I r s
 2. \<lbrakk>\<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s; \<not> whileLoop_terminates C B r s\<rbrakk> \<Longrightarrow> I r s proof (prove)
goal (2 subgoals):
 1. (Some (r, s), None) \<in> whileLoop_results C B \<Longrightarrow> (\<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s) \<longrightarrow> I r s
 2. \<lbrakk>\<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s; \<not> whileLoop_terminates C B r s\<rbrakk> \<Longrightarrow> I r s proof (prove)
goal (3 subgoals):
 1. \<And>r s. \<lbrakk>C r s; snd (B r s)\<rbrakk> \<Longrightarrow> (\<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s) \<longrightarrow> I r s
 2. \<And>r s r' s'. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), None) \<in> whileLoop_results C B; (\<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s) \<longrightarrow> I r' s'\<rbrakk> \<Longrightarrow> (\<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s) \<longrightarrow> I r s
 3. \<lbrakk>\<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s; \<not> whileLoop_terminates C B r s\<rbrakk> \<Longrightarrow> I r s proof (prove)
goal (2 subgoals):
 1. \<And>r s r' s'. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), None) \<in> whileLoop_results C B; (\<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s) \<longrightarrow> I r' s'\<rbrakk> \<Longrightarrow> (\<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s) \<longrightarrow> I r s
 2. \<lbrakk>\<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s; \<not> whileLoop_terminates C B r s\<rbrakk> \<Longrightarrow> I r s proof (prove)
goal (2 subgoals):
 1. \<And>r s r' s'. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), None) \<in> whileLoop_results C B; \<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s; I r' s'\<rbrakk> \<Longrightarrow> I r s
 2. \<lbrakk>\<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s; \<not> whileLoop_terminates C B r s\<rbrakk> \<Longrightarrow> I r s proof (prove)
goal (3 subgoals):
 1. \<And>r s r' s'. \<lbrakk>(r', s') \<in> fst (B r s); (Some (r', s'), None) \<in> whileLoop_results C B; \<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s; I r' s'\<rbrakk> \<Longrightarrow> snd (whileLoop C
  B r' s')
 2. \<And>r s r' s'. \<lbrakk>(r', s') \<in> fst (B r s); (Some (r', s'), None) \<in> whileLoop_results C B; \<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s; I r' s'\<rbrakk> \<Longrightarrow> I r' s'
 3. \<lbrakk>\<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s; \<not> whileLoop_terminates C B r s\<rbrakk> \<Longrightarrow> I r s proof (prove)
goal (2 subgoals):
 1. \<And>r s r' s'. \<lbrakk>(r', s') \<in> fst (B r s); (Some (r', s'), None) \<in> whileLoop_results C B; \<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s; I r' s'\<rbrakk> \<Longrightarrow> I r' s'
 2. \<lbrakk>\<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s; \<not> whileLoop_terminates C B r s\<rbrakk> \<Longrightarrow> I r s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>r s. snd (B r s) \<longrightarrow> C r s \<longrightarrow> I r s; \<not> whileLoop_terminates C B r s\<rbrakk> \<Longrightarrow> I r s proof (prove)
goal:
No subgoals!