theory Nondet_Lemmas

lemma whileLoopE_unroll:
  "whileLoopE C B r = condition (C r) (B r >>=E whileLoopE C B) (returnOk r)" unfolding whileLoopE_def apply (rule ext) apply (subst whileLoop_unroll) apply (clarsimp simp: bindE_def returnOk_def lift_def split: condition_splits) apply (rule arg_cong[where f="\<lambda>a. (B r >>= a) x" for x]) apply (rule ext)+ apply (clarsimp simp: lift_def split: sum.splits) apply (subst whileLoop_unroll) apply (clarsimp simp: condition_false throwError_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. whileLoopE C
  B r = condition (C r)
  (B r >>=E whileLoopE C
  B)
  (returnOk r) proof (prove)
goal (1 subgoal):
 1. whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B) (Inr r) = condition (C r)
  (doE r <- B r;
whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B) (Inr r)
odE)
  (returnOk r) proof (prove)
goal (1 subgoal):
 1. \<And>x. whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B) (Inr r) x = condition (C r)
  (doE r <- B r;
whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B) (Inr r)
odE)
  (returnOk r) x proof (prove)
goal (1 subgoal):
 1. \<And>x. condition (\<lambda>s. case Inr r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B (Inr r) >>= whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B))
  (return (Inr r)) x = condition (C r)
  (doE r <- B r;
whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B) (Inr r)
odE)
  (returnOk r) x proof (prove)
goal (1 subgoal):
 1. \<And>x. C r x \<Longrightarrow> (B r >>= whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B)) x = (B r >>= lift (\<lambda>r. whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B) (Inr r))) x proof (prove)
goal (1 subgoal):
 1. \<And>x. C r x \<Longrightarrow> whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B) = lift (\<lambda>r. whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B) (Inr r)) proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. C r x \<Longrightarrow> whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B) xa xb = lift (\<lambda>r. whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B) (Inr r)) xa xb proof (prove)
goal (1 subgoal):
 1. \<And>x xb x1. C r x \<Longrightarrow> whileLoop (\<lambda>r s. (\<exists>x1. r = Inr x1) \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> C x2 s))
  (lift B) (Inl x1) xb = throwError x1 xb proof (prove)
goal (1 subgoal):
 1. \<And>x xb x1. C r x \<Longrightarrow> condition (\<lambda>s. (\<exists>x1a. Inl x1 = Inr x1a) \<and> (\<forall>x2. Inl x1 = Inr x2 \<longrightarrow> C x2 s))
  (lift B (Inl x1) >>= whileLoop (\<lambda>r s. (\<exists>x1. r = Inr x1) \<and> (\<forall>x2. r = Inr x2 \<longrightarrow> C x2 s))
  (lift B))
  (return (Inl x1)) xb = throwError x1 xb proof (prove)
goal:
No subgoals!