theory Nondet_While_Loop_Rules

lemma whileLoop_terminatesE_induct [consumes 1]:
  assumes induct: "whileLoop_terminatesE C B r s"
  and init: "\<And>r s. \<not> C r s \<Longrightarrow> I r s"
  and step: "\<And>r s r' s'. \<lbrakk> C r s; \<forall>(v', s') \<in> fst (B r s). case v' of Inl _ \<Rightarrow> True | Inr r' \<Rightarrow> I r' s' \<rbrakk> \<Longrightarrow> I r s"
  shows "I r s" apply (insert induct) apply (clarsimp simp: whileLoop_terminatesE_def) apply (subgoal_tac "(\<lambda>r s. case (Inr r) of Inl x \<Rightarrow> True | Inr x \<Rightarrow> I x s) r s") apply simp apply (induction rule: whileLoop_terminates.induct) apply (clarsimp split: sum.splits elim!: init) apply (clarsimp split: sum.splits) apply (rule step) apply simp apply (force simp: lift_def split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. I r s proof (prove)
goal (1 subgoal):
 1. whileLoop_terminatesE C B r s \<Longrightarrow> I r s proof (prove)
goal (1 subgoal):
 1. whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift B) (Inr r) s \<Longrightarrow> I r s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift B) (Inr r) s; case Inr r of Inl x \<Rightarrow> True | Inr x \<Rightarrow> I x s\<rbrakk> \<Longrightarrow> I r s
 2. whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift B) (Inr r) s \<Longrightarrow> case Inr r of Inl x \<Rightarrow> True | Inr x \<Rightarrow> I x s proof (prove)
goal (1 subgoal):
 1. whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift B) (Inr r) s \<Longrightarrow> case Inr r of Inl x \<Rightarrow> True | Inr x \<Rightarrow> I x s proof (prove)
goal (2 subgoals):
 1. \<And>r s. \<not> (case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) \<Longrightarrow> case r of Inl x \<Rightarrow> True | Inr x \<Rightarrow> I x s
 2. \<And>r s. \<lbrakk>case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s; \<forall>(r', s')\<in>fst (lift B r s). whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift B) r' s' \<and> (case r' of Inl x \<Rightarrow> True | Inr x \<Rightarrow> I x s')\<rbrakk> \<Longrightarrow> case r of Inl x \<Rightarrow> True | Inr x \<Rightarrow> I x s proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s; \<forall>(r', s')\<in>fst (lift B r s). whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift B) r' s' \<and> (case r' of Inl x \<Rightarrow> True | Inr x \<Rightarrow> I x s')\<rbrakk> \<Longrightarrow> case r of Inl x \<Rightarrow> True | Inr x \<Rightarrow> I x s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>\<forall>x\<in>fst (lift B (Inr x2) s). case x of (r', s') \<Rightarrow> ((\<exists>x1. r' = Inr x1) \<or> whileLoop_terminates (\<lambda>r s. (\<exists>x1. r = Inr x1) \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> C x2 s)) (lift B) r' s') \<and> (\<forall>x2. r' = Inr x2 \<longrightarrow> whileLoop_terminates (\<lambda>r s. (\<exists>x1. r = Inr x1) \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> C x2 s)) (lift B) (Inr x2) s' \<and> I x2 s'); C x2 s\<rbrakk> \<Longrightarrow> I x2 s proof (prove)
goal (2 subgoals):
 1. \<And>s x2. \<lbrakk>\<forall>x\<in>fst (lift B (Inr x2) s). case x of (r', s') \<Rightarrow> ((\<exists>x1. r' = Inr x1) \<or> whileLoop_terminates (\<lambda>r s. (\<exists>x1. r = Inr x1) \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> C x2 s)) (lift B) r' s') \<and> (\<forall>x2. r' = Inr x2 \<longrightarrow> whileLoop_terminates (\<lambda>r s. (\<exists>x1. r = Inr x1) \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> C x2 s)) (lift B) (Inr x2) s' \<and> I x2 s'); C x2 s\<rbrakk> \<Longrightarrow> C x2 s
 2. \<And>s x2. \<lbrakk>\<forall>x\<in>fst (lift B (Inr x2) s). case x of (r', s') \<Rightarrow> ((\<exists>x1. r' = Inr x1) \<or> whileLoop_terminates (\<lambda>r s. (\<exists>x1. r = Inr x1) \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> C x2 s)) (lift B) r' s') \<and> (\<forall>x2. r' = Inr x2 \<longrightarrow> whileLoop_terminates (\<lambda>r s. (\<exists>x1. r = Inr x1) \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> C x2 s)) (lift B) (Inr x2) s' \<and> I x2 s'); C x2 s\<rbrakk> \<Longrightarrow> \<forall>(v', s')\<in>fst (B x2 s). case v' of Inl x \<Rightarrow> True | Inr r' \<Rightarrow> I r' s' proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>\<forall>x\<in>fst (lift B (Inr x2) s). case x of (r', s') \<Rightarrow> ((\<exists>x1. r' = Inr x1) \<or> whileLoop_terminates (\<lambda>r s. (\<exists>x1. r = Inr x1) \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> C x2 s)) (lift B) r' s') \<and> (\<forall>x2. r' = Inr x2 \<longrightarrow> whileLoop_terminates (\<lambda>r s. (\<exists>x1. r = Inr x1) \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> C x2 s)) (lift B) (Inr x2) s' \<and> I x2 s'); C x2 s\<rbrakk> \<Longrightarrow> \<forall>(v', s')\<in>fst (B x2 s). case v' of Inl x \<Rightarrow> True | Inr r' \<Rightarrow> I r' s' proof (prove)
goal:
No subgoals!