theory Nondet_While_Loop_Rules

lemma whileLoop_terminates_liftE:
  "whileLoop_terminatesE C (\<lambda>r. liftE (B r)) r s = whileLoop_terminates C B r s" apply (subst eq_sym_conv) apply (clarsimp simp: whileLoop_terminatesE_def) apply (rule iffI) apply (erule whileLoop_terminates.induct) apply (rule whileLoop_terminates.intros) apply clarsimp apply (clarsimp simp: split_def) apply (rule whileLoop_terminates.intros(2)) apply clarsimp apply (clarsimp simp: liftE_def in_bind return_def lift_def[abs_def]
                          bind_def lift_def throwError_def o_def
                   split: sum.splits
                   cong: sum.case_cong) apply (drule (1) bspec) apply clarsimp apply (subgoal_tac
         "case Inr r of
            Inl _ \<Rightarrow> True
          | Inr r \<Rightarrow> whileLoop_terminates
                       (\<lambda>r s. (\<lambda>r s. case r of Inl _ \<Rightarrow> False | Inr v \<Rightarrow> C v s) (Inr r) s)
                       (\<lambda>r. lift (\<lambda>r. liftE (B r)) (Inr r) >>= (\<lambda>x. return (projr x))) r s") apply (clarsimp simp: liftE_def lift_def) apply (erule whileLoop_terminates.induct) apply (clarsimp simp: liftE_def lift_def split: sum.splits) apply (erule whileLoop_terminates.intros) apply (clarsimp simp: liftE_def split: sum.splits) apply (clarsimp simp: bind_def return_def split_def lift_def) apply (erule whileLoop_terminates.intros) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. whileLoop_terminatesE C (\<lambda>r. liftE (B r)) r s = whileLoop_terminates C B r s proof (prove)
goal (1 subgoal):
 1. whileLoop_terminates C B r s = whileLoop_terminatesE C (\<lambda>r. liftE (B r)) r s proof (prove)
goal (1 subgoal):
 1. whileLoop_terminates C B r s = whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr r) s proof (prove)
goal (2 subgoals):
 1. whileLoop_terminates C B r s \<Longrightarrow> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr r) s
 2. whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr r) s \<Longrightarrow> whileLoop_terminates C B r s proof (prove)
goal (3 subgoals):
 1. \<And>r s. \<not> C r s \<Longrightarrow> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr r) s
 2. \<And>r s. \<lbrakk>C r s; \<forall>(r', s')\<in>fst (B r s). whileLoop_terminates C B r' s' \<and> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr r') s'\<rbrakk> \<Longrightarrow> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr r) s
 3. whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr r) s \<Longrightarrow> whileLoop_terminates C B r s proof (prove)
goal (3 subgoals):
 1. \<And>r s. \<not> C r s \<Longrightarrow> \<not> (case Inr r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
 2. \<And>r s. \<lbrakk>C r s; \<forall>(r', s')\<in>fst (B r s). whileLoop_terminates C B r' s' \<and> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr r') s'\<rbrakk> \<Longrightarrow> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr r) s
 3. whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr r) s \<Longrightarrow> whileLoop_terminates C B r s proof (prove)
goal (2 subgoals):
 1. \<And>r s. \<lbrakk>C r s; \<forall>(r', s')\<in>fst (B r s). whileLoop_terminates C B r' s' \<and> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr r') s'\<rbrakk> \<Longrightarrow> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr r) s
 2. whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr r) s \<Longrightarrow> whileLoop_terminates C B r s proof (prove)
goal (2 subgoals):
 1. \<And>r s. \<lbrakk>C r s; \<forall>x\<in>fst (B r s). whileLoop_terminates C B (fst x) (snd x) \<and> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr (fst x)) (snd x)\<rbrakk> \<Longrightarrow> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr r) s
 2. whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr r) s \<Longrightarrow> whileLoop_terminates C B r s proof (prove)
goal (3 subgoals):
 1. \<And>r s. \<lbrakk>C r s; \<forall>x\<in>fst (B r s). whileLoop_terminates C B (fst x) (snd x) \<and> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr (fst x)) (snd x)\<rbrakk> \<Longrightarrow> case Inr r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s
 2. \<And>r s. \<lbrakk>C r s; \<forall>x\<in>fst (B r s). whileLoop_terminates C B (fst x) (snd x) \<and> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr (fst x)) (snd x)\<rbrakk> \<Longrightarrow> \<forall>(r', s')\<in>fst (lift (\<lambda>r. liftE (B r)) (Inr r) s). whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) r' s'
 3. whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr r) s \<Longrightarrow> whileLoop_terminates C B r s proof (prove)
goal (2 subgoals):
 1. \<And>r s. \<lbrakk>C r s; \<forall>x\<in>fst (B r s). whileLoop_terminates C B (fst x) (snd x) \<and> whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr (fst x)) (snd x)\<rbrakk> \<Longrightarrow> \<forall>(r', s')\<in>fst (lift (\<lambda>r. liftE (B r)) (Inr r) s). whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) r' s'
 2. whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr r) s \<Longrightarrow> whileLoop_terminates C B r s proof (prove)
goal (2 subgoals):
 1. \<And>r s a b. \<lbrakk>\<forall>x\<in>fst (B r s). whileLoop_terminates C B (fst x) (snd x) \<and> whileLoop_terminates (\<lambda>r s. (\<exists>x1. r = Inr x1) \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> C x2 s)) (\<lambda>r. case r of Inl e \<Rightarrow> \<lambda>s. ({(Inl e, s)}, False) | Inr v' \<Rightarrow> \<lambda>s. (\<Union>a\<in>fst (B v' s). fst (case a of (r, s) \<Rightarrow> ({(Inr r, s)}, False)), (\<exists>x\<in>fst (B v' s). snd (case x of (r, s) \<Rightarrow> ({(Inr r, s)}, False))) \<or> snd (B v' s))) (Inr (fst x)) (snd x); C r s; (a, b) \<in> fst (B r s)\<rbrakk> \<Longrightarrow> whileLoop_terminates (\<lambda>r s. (\<exists>x1. r = Inr x1) \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> C x2 s)) (\<lambda>r. case r of Inl e \<Rightarrow> \<lambda>s. ({(Inl e, s)}, False) | Inr v' \<Rightarrow> \<lambda>a. (\<Union>a\<in>fst (B v' a). fst (case a of (r, s) \<Rightarrow> ({(Inr r, s)}, False)), (\<exists>x\<in>fst (B v' a). snd (case x of (r, s) \<Rightarrow> ({(Inr r, s)}, False))) \<or> snd (B v' a))) (Inr a) b
 2. whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr r) s \<Longrightarrow> whileLoop_terminates C B r s proof (prove)
goal (2 subgoals):
 1. \<And>r s a b. \<lbrakk>C r s; (a, b) \<in> fst (B r s); whileLoop_terminates C B (fst (a, b)) (snd (a, b)) \<and> whileLoop_terminates (\<lambda>r s. (\<exists>x1. r = Inr x1) \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> C x2 s)) (\<lambda>r. case r of Inl e \<Rightarrow> \<lambda>s. ({(Inl e, s)}, False) | Inr v' \<Rightarrow> \<lambda>s. (\<Union>a\<in>fst (B v' s). fst (case a of (r, s) \<Rightarrow> ({(Inr r, s)}, False)), (\<exists>x\<in>fst (B v' s). snd (case x of (r, s) \<Rightarrow> ({(Inr r, s)}, False))) \<or> snd (B v' s))) (Inr (fst (a, b))) (snd (a, b))\<rbrakk> \<Longrightarrow> whileLoop_terminates (\<lambda>r s. (\<exists>x1. r = Inr x1) \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> C x2 s)) (\<lambda>r. case r of Inl e \<Rightarrow> \<lambda>s. ({(Inl e, s)}, False) | Inr v' \<Rightarrow> \<lambda>a. (\<Union>a\<in>fst (B v' a). fst (case a of (r, s) \<Rightarrow> ({(Inr r, s)}, False)), (\<exists>x\<in>fst (B v' a). snd (case x of (r, s) \<Rightarrow> ({(Inr r, s)}, False))) \<or> snd (B v' a))) (Inr a) b
 2. whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr r) s \<Longrightarrow> whileLoop_terminates C B 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 (\<lambda>r. liftE (B r))) (Inr r) s \<Longrightarrow> whileLoop_terminates C B 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 (\<lambda>r. liftE (B r))) (Inr r) s; case Inr r of Inl x \<Rightarrow> True | Inr r \<Rightarrow> whileLoop_terminates (\<lambda>r s. case Inr r of Inl x \<Rightarrow> False | Inr v \<Rightarrow> C v s) (\<lambda>r. do x <- lift (\<lambda>r. liftE (B r)) (Inr r);
return (projr x)
od) r s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B r s
 2. whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) (Inr r) s \<Longrightarrow> case Inr r of Inl x \<Rightarrow> True | Inr r \<Rightarrow> whileLoop_terminates (\<lambda>r s. case Inr r of Inl x \<Rightarrow> False | Inr v \<Rightarrow> C v s) (\<lambda>r. do x <- lift (\<lambda>r. liftE (B r)) (Inr r);
return (projr x)
od) 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 (\<lambda>r. liftE (B r))) (Inr r) s \<Longrightarrow> case Inr r of Inl x \<Rightarrow> True | Inr r \<Rightarrow> whileLoop_terminates (\<lambda>r s. case Inr r of Inl x \<Rightarrow> False | Inr v \<Rightarrow> C v s) (\<lambda>r. do x <- lift (\<lambda>r. liftE (B r)) (Inr r);
return (projr x)
od) r 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 r \<Rightarrow> whileLoop_terminates (\<lambda>r s. case Inr r of Inl x \<Rightarrow> False | Inr v \<Rightarrow> C v s) (\<lambda>r. do x <- lift (\<lambda>r. liftE (B r)) (Inr r);
return (projr x)
od) r 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 (\<lambda>r. liftE (B r)) r s). whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) r' s' \<and> (case r' of Inl x \<Rightarrow> True | Inr r \<Rightarrow> whileLoop_terminates (\<lambda>r s. case Inr r of Inl x \<Rightarrow> False | Inr v \<Rightarrow> C v s) (\<lambda>r. do x <- lift (\<lambda>r. liftE (B r)) (Inr r);
return (projr x)
od) r s')\<rbrakk> \<Longrightarrow> case r of Inl x \<Rightarrow> True | Inr r \<Rightarrow> whileLoop_terminates (\<lambda>r s. case Inr r of Inl x \<Rightarrow> False | Inr v \<Rightarrow> C v s) (\<lambda>r. do x <- lift (\<lambda>r. liftE (B r)) (Inr r);
return (projr x)
od) r s proof (prove)
goal (2 subgoals):
 1. \<And>s x2. \<not> C x2 s \<Longrightarrow> whileLoop_terminates C B x2 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 (\<lambda>r. liftE (B r)) r s). whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) r' s' \<and> (case r' of Inl x \<Rightarrow> True | Inr r \<Rightarrow> whileLoop_terminates (\<lambda>r s. case Inr r of Inl x \<Rightarrow> False | Inr v \<Rightarrow> C v s) (\<lambda>r. do x <- lift (\<lambda>r. liftE (B r)) (Inr r);
return (projr x)
od) r s')\<rbrakk> \<Longrightarrow> case r of Inl x \<Rightarrow> True | Inr r \<Rightarrow> whileLoop_terminates (\<lambda>r s. case Inr r of Inl x \<Rightarrow> False | Inr v \<Rightarrow> C v s) (\<lambda>r. do x <- lift (\<lambda>r. liftE (B r)) (Inr r);
return (projr x)
od) r 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 (\<lambda>r. liftE (B r)) r s). whileLoop_terminates (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s) (lift (\<lambda>r. liftE (B r))) r' s' \<and> (case r' of Inl x \<Rightarrow> True | Inr r \<Rightarrow> whileLoop_terminates (\<lambda>r s. case Inr r of Inl x \<Rightarrow> False | Inr v \<Rightarrow> C v s) (\<lambda>r. do x <- lift (\<lambda>r. liftE (B r)) (Inr r);
return (projr x)
od) r s')\<rbrakk> \<Longrightarrow> case r of Inl x \<Rightarrow> True | Inr r \<Rightarrow> whileLoop_terminates (\<lambda>r s. case Inr r of Inl x \<Rightarrow> False | Inr v \<Rightarrow> C v s) (\<lambda>r. do x <- lift (\<lambda>r. liftE (B r)) (Inr r);
return (projr x)
od) r s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>\<forall>x\<in>fst (lift (\<lambda>r. do r <- B r;
return (Inr r)
od) (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 (\<lambda>r. do r <- B r;
return (Inr r)
od)) 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 (\<lambda>r. do r <- B r;
return (Inr r)
od)) (Inr x2) s' \<and> whileLoop_terminates C (\<lambda>r. do x <- lift (\<lambda>r. do r <- B r;
return (Inr r)
od) (Inr r);
return (projr x)
od) x2 s'); C x2 s\<rbrakk> \<Longrightarrow> whileLoop_terminates C (\<lambda>r. do x <- lift (\<lambda>r. do r <- B r;
return (Inr r)
od) (Inr r);
return (projr x)
od) x2 s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>\<forall>y\<in>fst (B x2 s). whileLoop_terminates (\<lambda>r s. (\<exists>x1. r = Inr x1) \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> C x2 s)) (\<lambda>r. case r of Inl x \<Rightarrow> throwError x | Inr v' \<Rightarrow> \<lambda>s. (\<Union>x\<in>fst (B v' s). {(Inr (fst x), snd x)}, snd (B v' s))) (Inr (fst y)) (snd y) \<and> whileLoop_terminates C B (fst y) (snd y); C x2 s\<rbrakk> \<Longrightarrow> whileLoop_terminates C B x2 s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<forall>y\<in>fst (B x2 s). whileLoop_terminates (\<lambda>r s. (\<exists>x1. r = Inr x1) \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> C x2 s)) (\<lambda>r. case r of Inl x \<Rightarrow> throwError x | Inr v' \<Rightarrow> \<lambda>s. (\<Union>x\<in>fst (B v' s). {(Inr (fst x), snd x)}, snd (B v' s))) (Inr (fst y)) (snd y) \<and> whileLoop_terminates C B (fst y) (snd y) \<Longrightarrow> \<forall>(r', s')\<in>fst (B x2 s). whileLoop_terminates C B r' s' proof (prove)
goal:
No subgoals!