theory Nondet_While_Loop_Rules

lemma whileLoop_results_induct_lemma2 [consumes 1]:
  "\<lbrakk> (a, b) \<in> whileLoop_results C B;
     a = Some (x :: 'a \<times> 'b); b = Some y;
     P x; \<And>s t. \<lbrakk> P s; t \<in> fst (B (fst s) (snd s)); C (fst s) (snd s) \<rbrakk> \<Longrightarrow> P t \<rbrakk> \<Longrightarrow> P y" apply (induct arbitrary: x y rule: whileLoop_results.induct) apply simp apply simp apply atomize apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, b) \<in> whileLoop_results C B; a = Some x; b = Some y; P x; \<And>s t. \<lbrakk>P s; t \<in> fst (B (fst s) (snd s)); C (fst s) (snd s)\<rbrakk> \<Longrightarrow> P t\<rbrakk> \<Longrightarrow> P y proof (prove)
goal (3 subgoals):
 1. \<And>r s x y. \<lbrakk>\<not> C r s; Some (r, s) = Some x; Some (r, s) = Some y; P x; \<And>s t. \<lbrakk>P s; t \<in> fst (B (fst s) (snd s)); C (fst s) (snd s)\<rbrakk> \<Longrightarrow> P t\<rbrakk> \<Longrightarrow> P y
 2. \<And>r s x y. \<lbrakk>C r s; snd (B r s); Some (r, s) = Some x; None = Some y; P x; \<And>s t. \<lbrakk>P s; t \<in> fst (B (fst s) (snd s)); C (fst s) (snd s)\<rbrakk> \<Longrightarrow> P t\<rbrakk> \<Longrightarrow> P y
 3. \<And>r s r' s' z x y. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B; \<And>x y. \<lbrakk>Some (r', s') = Some x; z = Some y; P x; \<And>s t. \<lbrakk>P s; t \<in> fst (B (fst s) (snd s)); C (fst s) (snd s)\<rbrakk> \<Longrightarrow> P t\<rbrakk> \<Longrightarrow> P y; Some (r, s) = Some x; z = Some y; P x; \<And>s t. \<lbrakk>P s; t \<in> fst (B (fst s) (snd s)); C (fst s) (snd s)\<rbrakk> \<Longrightarrow> P t\<rbrakk> \<Longrightarrow> P y proof (prove)
goal (2 subgoals):
 1. \<And>r s x y. \<lbrakk>C r s; snd (B r s); Some (r, s) = Some x; None = Some y; P x; \<And>s t. \<lbrakk>P s; t \<in> fst (B (fst s) (snd s)); C (fst s) (snd s)\<rbrakk> \<Longrightarrow> P t\<rbrakk> \<Longrightarrow> P y
 2. \<And>r s r' s' z x y. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B; \<And>x y. \<lbrakk>Some (r', s') = Some x; z = Some y; P x; \<And>s t. \<lbrakk>P s; t \<in> fst (B (fst s) (snd s)); C (fst s) (snd s)\<rbrakk> \<Longrightarrow> P t\<rbrakk> \<Longrightarrow> P y; Some (r, s) = Some x; z = Some y; P x; \<And>s t. \<lbrakk>P s; t \<in> fst (B (fst s) (snd s)); C (fst s) (snd s)\<rbrakk> \<Longrightarrow> P t\<rbrakk> \<Longrightarrow> P y proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s' z x y. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B; \<And>x y. \<lbrakk>Some (r', s') = Some x; z = Some y; P x; \<And>s t. \<lbrakk>P s; t \<in> fst (B (fst s) (snd s)); C (fst s) (snd s)\<rbrakk> \<Longrightarrow> P t\<rbrakk> \<Longrightarrow> P y; Some (r, s) = Some x; z = Some y; P x; \<And>s t. \<lbrakk>P s; t \<in> fst (B (fst s) (snd s)); C (fst s) (snd s)\<rbrakk> \<Longrightarrow> P t\<rbrakk> \<Longrightarrow> P y proof (prove)
goal (1 subgoal):
 1. \<And>r s r' s' z x y. \<lbrakk>C r s; (r', s') \<in> fst (B r s); (Some (r', s'), z) \<in> whileLoop_results C B; \<forall>x y. Some (r', s') = Some x \<longrightarrow> z = Some y \<longrightarrow> P x \<longrightarrow> (\<forall>s t. P s \<longrightarrow> t \<in> fst (B (fst s) (snd s)) \<longrightarrow> C (fst s) (snd s) \<longrightarrow> P t) \<longrightarrow> P y; Some (r, s) = Some x; z = Some y; P x; \<forall>s t. P s \<longrightarrow> t \<in> fst (B (fst s) (snd s)) \<longrightarrow> C (fst s) (snd s) \<longrightarrow> P t\<rbrakk> \<Longrightarrow> P y proof (prove)
goal:
No subgoals!