kings-crown/FVELER_Isabelle huggingface dataset:
theory Nondet_Lemmas

lemma bind_eqI:
  "\<lbrakk> f = f'; \<And>x. g x = g' x \<rbrakk> \<Longrightarrow> f >>= g = f' >>= g'" by (auto simp: bind_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f = f'; \<And>x. g x = g' x\<rbrakk> \<Longrightarrow> f >>= g = f' >>= g'
theory Nondet_Lemmas

lemma condition_split:
  "P (condition C a b s) \<longleftrightarrow> (C s \<longrightarrow> P (a s)) \<and> (\<not>C s \<longrightarrow> P (b s))" by (clarsimp simp: condition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P (condition C
  a
  b s) = ((C s \<longrightarrow> P (a s)) \<and> (\<not> C s \<longrightarrow> P (b s)))
theory Nondet_Lemmas

lemma condition_split_asm:
  "P (condition C a b s) \<longleftrightarrow> (\<not>(C s \<and> \<not> P (a s) \<or> \<not>C s \<and> \<not>P (b s)))" by (clarsimp simp: condition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P (condition C
  a
  b s) = (\<not> (C s \<and> \<not> P (a s) \<or> \<not> C s \<and> \<not> P (b s)))
theory Nondet_Lemmas

lemma condition_true_triv[simp]:
  "condition (\<lambda>_. True) A B = A" by (fastforce split: condition_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. condition (\<lambda>_. True)
  A
  B = A
theory Nondet_Lemmas

lemma condition_false_triv[simp]:
  "condition (\<lambda>_. False) A B = B" by (fastforce split: condition_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. condition (\<lambda>_. False)
  A
  B = B
theory Nondet_Lemmas

lemma condition_true:
  "P s \<Longrightarrow> condition P A B s = A s" by (clarsimp simp: condition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P s \<Longrightarrow> condition P
  A
  B s = A s
theory Nondet_Lemmas

lemma condition_false:
  "\<not> P s \<Longrightarrow> condition P A B s = B s" by (clarsimp simp: condition_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> P s \<Longrightarrow> condition P
  A
  B s = B s
theory Nondet_Lemmas

lemma monad_eqI [intro]:
  "\<lbrakk> \<And>r t s. (r, t) \<in> fst (A s) \<Longrightarrow> (r, t) \<in> fst (B s);
     \<And>r t s. (r, t) \<in> fst (B s) \<Longrightarrow> (r, t) \<in> fst (A s);
     \<And>x. snd (A x) = snd (B x) \<rbrakk>
  \<Longrightarrow> A = B" for A :: "('s, 'a) nondet_monad" by (fastforce intro!: set_eqI prod_eqI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r t s. (r, t) \<in> fst (A s) \<Longrightarrow> (r, t) \<in> fst (B s); \<And>r t s. (r, t) \<in> fst (B s) \<Longrightarrow> (r, t) \<in> fst (A s); \<And>x. snd (A x) = snd (B x)\<rbrakk> \<Longrightarrow> A = B
theory Nondet_Lemmas

lemma whileLoop_cond_fail:
  "\<not> C x s \<Longrightarrow> whileLoop C B x s = return x s" by (auto simp: return_def whileLoop_def
           intro: whileLoop_results.intros whileLoop_terminates.intros
           elim!: whileLoop_results.cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> C x s \<Longrightarrow> whileLoop C
  B x s = return x s
theory Nondet_Lemmas

lemma whileLoopE_cond_fail:
  "\<not> C x s \<Longrightarrow> whileLoopE C B x s = returnOk x s" unfolding whileLoopE_def returnOk_def by (auto intro: whileLoop_cond_fail)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> C x s \<Longrightarrow> whileLoopE C
  B x s = returnOk x s proof (prove)
goal (1 subgoal):
 1. \<not> C x s \<Longrightarrow> whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> C v s)
  (lift B) (Inr x) s = (return \<circ> Inr) x s
theory Nondet_Lemmas

lemma whileLoop_results_simps_no_move[simp]:
  "(Some x, Some x) \<in> whileLoop_results C B \<longleftrightarrow> \<not>C (fst x) (snd x)"
  (is "?LHS x \<longleftrightarrow> ?RHS x") proof (rule iffI) assume "?LHS x" then have "(\<exists>a. Some x = Some a) \<longrightarrow> ?RHS (the (Some x))" by (induct rule: whileLoop_results.induct, auto) thus "?RHS x" by clarsimp next assume "?RHS x" thus "?LHS x" by (metis surjective_pairing whileLoop_results.intros(1)) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((Some x, Some x) \<in> whileLoop_results C B) = (\<not> C (fst x) (snd x)) proof (state)
goal (2 subgoals):
 1. (Some x, Some x) \<in> whileLoop_results C B \<Longrightarrow> \<not> C (fst x) (snd x)
 2. \<not> C (fst x) (snd x) \<Longrightarrow> (Some x, Some x) \<in> whileLoop_results C B proof (state)
this:
(Some x, Some x) \<in> whileLoop_results C B

goal (2 subgoals):
 1. (Some x, Some x) \<in> whileLoop_results C B \<Longrightarrow> \<not> C (fst x) (snd x)
 2. \<not> C (fst x) (snd x) \<Longrightarrow> (Some x, Some x) \<in> whileLoop_results C B proof (chain)
picking this:
(Some x, Some x) \<in> whileLoop_results C B proof (prove)
using this:
(Some x, Some x) \<in> whileLoop_results C B

goal (1 subgoal):
 1. (\<exists>a. Some x = Some a) \<longrightarrow> \<not> C (fst (the (Some x))) (snd (the (Some x))) proof (state)
this:
(\<exists>a. Some x = Some a) \<longrightarrow> \<not> C (fst (the (Some x))) (snd (the (Some x)))

goal (2 subgoals):
 1. (Some x, Some x) \<in> whileLoop_results C B \<Longrightarrow> \<not> C (fst x) (snd x)
 2. \<not> C (fst x) (snd x) \<Longrightarrow> (Some x, Some x) \<in> whileLoop_results C B proof (prove)
using this:
(\<exists>a. Some x = Some a) \<longrightarrow> \<not> C (fst (the (Some x))) (snd (the (Some x)))

goal (1 subgoal):
 1. \<not> C (fst x) (snd x) proof (state)
this:
\<not> C (fst x) (snd x)

goal (1 subgoal):
 1. \<not> C (fst x) (snd x) \<Longrightarrow> (Some x, Some x) \<in> whileLoop_results C B proof (state)
goal (1 subgoal):
 1. \<not> C (fst x) (snd x) \<Longrightarrow> (Some x, Some x) \<in> whileLoop_results C B proof (state)
this:
\<not> C (fst x) (snd x)

goal (1 subgoal):
 1. \<not> C (fst x) (snd x) \<Longrightarrow> (Some x, Some x) \<in> whileLoop_results C B proof (prove)
using this:
\<not> C (fst x) (snd x)

goal (1 subgoal):
 1. (Some x, Some x) \<in> whileLoop_results C B proof (state)
this:
(Some x, Some x) \<in> whileLoop_results C B

goal:
No subgoals!
theory Nondet_Lemmas

lemma whileLoopE_unroll':
  "whileLoopE C B r = condition (C r) (B r) (returnOk r) >>=E whileLoopE C B" apply (subst whileLoopE_unroll) apply (fastforce simp: condition_def bindE_def bind_def lift_def split_def whileLoopE_cond_fail
                         returnOk_def return_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. whileLoopE C
  B r = condition (C r)
  (B r)
  (returnOk r) >>=E whileLoopE C
  B proof (prove)
goal (1 subgoal):
 1. condition (C r)
  (B r >>=E whileLoopE C
  B)
  (returnOk r) = condition (C r)
  (B r)
  (returnOk r) >>=E whileLoopE C
  B proof (prove)
goal:
No subgoals!
theory Nondet_In_Monad

lemma in_throwError:
  "((v, s') \<in> fst (throwError e s)) = (v = Inl e \<and> s' = s)" by (simp add: throwError_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((v, s') \<in> fst (throwError e s)) = (v = Inl e \<and> s' = s)
theory Nondet_In_Monad

lemma in_returnOk:
  "((v', s') \<in> fst (returnOk v s)) = (v' = Inr v \<and> s' = s)" by (simp add: returnOk_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((v', s') \<in> fst (returnOk v s)) = (v' = Inr v \<and> s' = s)
theory Nondet_In_Monad

lemma in_bind:
  "((r,s') \<in> fst ((do x \<leftarrow> f; g x od) s)) =
   (\<exists>s'' x. (x, s'') \<in> fst (f s) \<and> (r, s') \<in> fst (g x s''))" by (force simp: bind_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, s') \<in> fst ((f >>= g) s)) = (\<exists>s'' x. (x, s'') \<in> fst (f s) \<and> (r, s') \<in> fst (g x s''))
theory Nondet_In_Monad

lemma in_bindE_R:
  "((Inr r,s') \<in> fst ((doE x \<leftarrow> f; g x odE) s)) =
  (\<exists>s'' x. (Inr x, s'') \<in> fst (f s) \<and> (Inr r, s') \<in> fst (g x s''))" unfolding bindE_def lift_def split_def bind_def by (force simp: throwError_def return_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((Inr r, s') \<in> fst ((f >>=E g) s)) = (\<exists>s'' x. (Inr x, s'') \<in> fst (f s) \<and> (Inr r, s') \<in> fst (g x s'')) proof (prove)
goal (1 subgoal):
 1. ((Inr r, s') \<in> fst (\<Union> (fst ` (\<lambda>p. (case fst p of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> g x) (snd p)) ` fst (f s)), True \<in> snd ` (\<lambda>p. (case fst p of Inl x \<Rightarrow> throwError x | Inr x \<Rightarrow> g x) (snd p)) ` fst (f s) \<or> snd (f s))) = (\<exists>s'' x. (Inr x, s'') \<in> fst (f s) \<and> (Inr r, s') \<in> fst (g x s''))
theory Nondet_In_Monad

lemma in_bindE_L:
  "((Inl r, s') \<in> fst ((doE x \<leftarrow> f; g x odE) s)) \<Longrightarrow>
   (\<exists>s'' x. (Inr x, s'') \<in> fst (f s) \<and> (Inl r, s') \<in> fst (g x s'')) \<or> ((Inl r, s') \<in> fst (f s))" by (simp add: bindE_def bind_def)
     (force simp: return_def throwError_def lift_def split_def split: sum.splits if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (Inl r, s') \<in> fst ((f >>=E g) s) \<Longrightarrow> (\<exists>s'' x. (Inr x, s'') \<in> fst (f s) \<and> (Inl r, s') \<in> fst (g x s'')) \<or> (Inl r, s') \<in> fst (f s)
theory Nondet_In_Monad

lemma in_return:
  "(r, s') \<in> fst (return v s) = (r = v \<and> s' = s)" by (simp add: return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, s') \<in> fst (return v s)) = (r = v \<and> s' = s)
theory Nondet_In_Monad

lemma in_liftE:
  "((v, s') \<in> fst (liftE f s)) = (\<exists>v'. v = Inr v' \<and> (v', s') \<in> fst (f s))" by (force simp: liftE_def in_bind in_return)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((v, s') \<in> fst (liftE f s)) = (\<exists>v'. v = Inr v' \<and> (v', s') \<in> fst (f s))
theory Nondet_In_Monad

lemma in_whenE:
  "((v, s') \<in> fst (whenE P f s)) = ((P \<longrightarrow> (v, s') \<in> fst (f s)) \<and> (\<not>P \<longrightarrow> v = Inr () \<and> s' = s))" by (simp add: whenE_def in_returnOk)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((v, s') \<in> fst (whenE P f s)) = ((P \<longrightarrow> (v, s') \<in> fst (f s)) \<and> (\<not> P \<longrightarrow> v = Inr () \<and> s' = s))
theory Nondet_In_Monad

lemma inl_whenE:
  "((Inl x, s') \<in> fst (whenE P f s)) = (P \<and> (Inl x, s') \<in> fst (f s))" by (auto simp add: in_whenE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((Inl x, s') \<in> fst (whenE P f s)) = (P \<and> (Inl x, s') \<in> fst (f s))
theory Nondet_In_Monad

lemma inr_in_unlessE_throwError[termination_simp]:
  "(Inr (), s') \<in> fst (unlessE P (throwError E) s) = (P \<and> s'=s)" by (simp add: unlessE_def returnOk_def throwError_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((Inr (), s') \<in> fst (unlessE P (throwError E) s)) = (P \<and> s' = s)
theory Nondet_In_Monad

lemma in_assert:
  "(r, s') \<in> fst (assert P s) = (P \<and> s' = s)" by (simp add: assert_def return_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, s') \<in> fst (assert P s)) = (P \<and> s' = s)
theory Nondet_In_Monad

lemma in_assertE:
  "(r, s') \<in> fst (assertE P s) = (P \<and> r = Inr () \<and> s' = s)" by (simp add: assertE_def returnOk_def return_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, s') \<in> fst (assertE P s)) = (P \<and> r = Inr () \<and> s' = s)
theory Nondet_In_Monad

lemma in_assert_opt:
  "(r, s') \<in> fst (assert_opt v s) = (v = Some r \<and> s' = s)" by (auto simp: assert_opt_def in_fail in_return split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, s') \<in> fst (assert_opt v s)) = (v = Some r \<and> s' = s)
theory Nondet_In_Monad

lemma in_get:
  "(r, s') \<in> fst (get s) = (r = s \<and> s' = s)" by (simp add: get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, s') \<in> fst (get s)) = (r = s \<and> s' = s)
theory Nondet_In_Monad

lemma in_gets:
  "(r, s') \<in> fst (gets f s) = (r = f s \<and> s' = s)" by (simp add: simpler_gets_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, s') \<in> fst (gets f s)) = (r = f s \<and> s' = s)
theory Nondet_In_Monad

lemma in_put:
  "(r, s') \<in> fst (put x s) = (s' = x \<and> r = ())" by (simp add: put_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, s') \<in> fst (put x s)) = (s' = x \<and> r = ())
theory Nondet_In_Monad

lemma in_when:
  "(v, s') \<in> fst (when P f s) = ((P \<longrightarrow> (v, s') \<in> fst (f s)) \<and> (\<not>P \<longrightarrow> v = () \<and> s' = s))" by (simp add: when_def in_return)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((v, s') \<in> fst (when P f s)) = ((P \<longrightarrow> (v, s') \<in> fst (f s)) \<and> (\<not> P \<longrightarrow> v = () \<and> s' = s))
theory Nondet_In_Monad

lemma in_unless:
  "(v, s') \<in> fst (unless P f s) = ((\<not> P \<longrightarrow> (v, s') \<in> fst (f s)) \<and> (P \<longrightarrow> v = () \<and> s' = s))" by (simp add: unless_def in_when)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((v, s') \<in> fst (unless P f s)) = ((\<not> P \<longrightarrow> (v, s') \<in> fst (f s)) \<and> (P \<longrightarrow> v = () \<and> s' = s))
theory Nondet_In_Monad

lemma in_unlessE:
  "(v, s') \<in> fst (unlessE P f s) = ((\<not> P \<longrightarrow> (v, s') \<in> fst (f s)) \<and> (P \<longrightarrow> v = Inr () \<and> s' = s))" by (simp add: unlessE_def in_returnOk)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((v, s') \<in> fst (unlessE P f s)) = ((\<not> P \<longrightarrow> (v, s') \<in> fst (f s)) \<and> (P \<longrightarrow> v = Inr () \<and> s' = s))
theory Nondet_In_Monad

lemma inl_unlessE:
  "((Inl x, s') \<in> fst (unlessE P f s)) = (\<not> P \<and> (Inl x, s') \<in> fst (f s))" by (auto simp add: in_unlessE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((Inl x, s') \<in> fst (unlessE P f s)) = (\<not> P \<and> (Inl x, s') \<in> fst (f s))
theory Nondet_In_Monad

lemma in_modify:
  "(v, s') \<in> fst (modify f s) = (s'=f s \<and> v = ())" by (simp add: modify_def bind_def get_def put_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((v, s') \<in> fst (modify f s)) = (s' = f s \<and> v = ())
theory Nondet_In_Monad

lemma gets_the_in_monad:
  "((v, s') \<in> fst (gets_the f s)) = (s' = s \<and> f s = Some v)" by (auto simp: gets_the_def in_bind in_gets in_assert_opt split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((v, s') \<in> fst (gets_the f s)) = (s' = s \<and> f s = Some v)
theory Nondet_In_Monad

lemma in_alternative:
  "(r,s') \<in> fst ((f \<sqinter> g) s) = ((r,s') \<in> fst (f s) \<or> (r,s') \<in> fst (g s))" by (simp add: alternative_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, s') \<in> fst ((f \<sqinter> g) s)) = ((r, s') \<in> fst (f s) \<or> (r, s') \<in> fst (g s))
theory Nondet_In_Monad

lemma in_liftM:
  "((r, s') \<in> fst (liftM t f s)) = (\<exists>r'. (r', s') \<in> fst (f s) \<and> r = t r')" by (simp add: liftM_def return_def bind_def Bex_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((r, s') \<in> fst (liftM t f s)) = (\<exists>r'. (r', s') \<in> fst (f s) \<and> r = t r')
theory Nondet_In_Monad

lemma in_bindE:
  "(rv, s') \<in> fst ((f >>=E (\<lambda>rv'. g rv')) s) =
   ((\<exists>ex. rv = Inl ex \<and> (Inl ex, s') \<in> fst (f s)) \<or>
    (\<exists>rv' s''. (rv, s') \<in> fst (g rv' s'') \<and> (Inr rv', s'') \<in> fst (f s)))" by (force simp: bindE_def bind_def lift_def throwError_def return_def  split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((rv, s') \<in> fst ((f >>=E g) s)) = ((\<exists>ex. rv = Inl ex \<and> (Inl ex, s') \<in> fst (f s)) \<or> (\<exists>rv' s''. (rv, s') \<in> fst (g rv' s'') \<and> (Inr rv', s'') \<in> fst (f s)))
theory Nondet_In_Monad

lemma bind_det_exec:
  "fst (a s) = {(r,s')} \<Longrightarrow> fst ((a >>= b) s) = fst (b r s')" by (simp add: bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst (a s) = {(r, s')} \<Longrightarrow> fst ((a >>= b) s) = fst (b r s')
theory Nondet_In_Monad

lemma in_bind_det_exec:
  "fst (a s) = {(r,s')} \<Longrightarrow> (s'' \<in> fst ((a >>= b) s)) = (s'' \<in> fst (b r s'))" by (simp add: bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst (a s) = {(r, s')} \<Longrightarrow> (s'' \<in> fst ((a >>= b) s)) = (s'' \<in> fst (b r s'))
theory Nondet_In_Monad

lemma exec_put:
  "(put s' >>= m) s = m () s'" by (simp add: bind_def put_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (put s' >>= m) s = m () s'
theory Nondet_In_Monad

lemma bind_execI:
  "\<lbrakk> (r'',s'') \<in> fst (f s); \<exists>x \<in> fst (g r'' s''). P x \<rbrakk> \<Longrightarrow> \<exists>x \<in> fst ((f >>= g) s). P x" by (force simp: in_bind split_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(r'', s'') \<in> fst (f s); \<exists>x\<in>fst (g r'' s''). P x\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst ((f >>= g) s). P x
theory Nondet_VCG

lemma validE_def2:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<equiv> \<forall>s. P s \<longrightarrow> (\<forall>(r,s') \<in> fst (f s). case r of Inr b \<Rightarrow> Q b s' | Inl a \<Rightarrow> E a s')" by (unfold valid_def validE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<equiv> \<forall>s. P s \<longrightarrow> (\<forall>(r, s')\<in>fst (f s). case r of Inl a \<Rightarrow> E a s' | Inr b \<Rightarrow> Q b s')
theory Nondet_VCG

lemma valid_make_schematic_post:
  "(\<forall>s0. \<lbrace> \<lambda>s. P s0 s \<rbrace> f \<lbrace> \<lambda>rv s. Q s0 rv s \<rbrace>) \<Longrightarrow>
   \<lbrace> \<lambda>s. \<exists>s0. P s0 s \<and> (\<forall>rv s'. Q s0 rv s' \<longrightarrow> Q' rv s') \<rbrace> f \<lbrace> Q' \<rbrace>" by (auto simp add: valid_def split: prod.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s0. \<lbrace>P s0\<rbrace> f \<lbrace>Q s0\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>s0. P s0 s \<and> (\<forall>rv s'. Q s0 rv s' \<longrightarrow> Q' rv s')\<rbrace> f \<lbrace>Q'\<rbrace>
theory Nondet_VCG

lemma validE_make_schematic_post:
  "(\<forall>s0. \<lbrace> \<lambda>s. P s0 s \<rbrace> f \<lbrace> \<lambda>rv s. Q s0 rv s \<rbrace>, \<lbrace> \<lambda>rv s. E s0 rv s \<rbrace>) \<Longrightarrow>
   \<lbrace> \<lambda>s. \<exists>s0. P s0 s \<and> (\<forall>rv s'. Q s0 rv s' \<longrightarrow> Q' rv s')
        \<and> (\<forall>rv s'. E s0 rv s' \<longrightarrow> E' rv s') \<rbrace> f \<lbrace> Q' \<rbrace>, \<lbrace> E' \<rbrace>" by (auto simp add: validE_def valid_def split: prod.splits sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s0. \<lbrace>P s0\<rbrace> f \<lbrace>Q s0\<rbrace>, \<lbrace>E s0\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. \<exists>s0. P s0 s \<and> (\<forall>rv s'. Q s0 rv s' \<longrightarrow> Q' rv s') \<and> (\<forall>rv s'. E s0 rv s' \<longrightarrow> E' rv s')\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>E'\<rbrace>
theory Nondet_VCG

lemma hoare_pre_imp:
  "\<lbrakk> \<And>s. P s \<Longrightarrow> Q s; \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>" by (fastforce simp: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. P s \<Longrightarrow> Q s; \<lbrace>Q\<rbrace> a \<lbrace>R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> a \<lbrace>R\<rbrace>
theory Nondet_VCG

lemma hoare_vcg_precond_impE_R: (* FIXME lib: rename to hoare_weaken_preE_R *)
  "\<lbrakk> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>,-; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-" unfolding validE_R_def by (rule hoare_vcg_precond_impE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>, -; \<And>s. P s \<Longrightarrow> P' s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; \<And>s. P s \<Longrightarrow> P' s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
theory Nondet_VCG

lemma hoare_weaken_preE_E:
  "\<lbrakk> \<lbrace>P'\<rbrace> f -,\<lbrace>Q\<rbrace>; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f -,\<lbrace>Q\<rbrace>" by (fastforce simp add: validE_E_def validE_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P'\<rbrace> f -, \<lbrace>Q\<rbrace>; \<And>s. P s \<Longrightarrow> P' s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f -, \<lbrace>Q\<rbrace>
theory Nondet_VCG

lemma wpc_helper_valid:
  "\<lbrace>Q\<rbrace> g \<lbrace>S\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> g \<lbrace>S\<rbrace>" by (clarsimp simp: wpc_helper_def elim!: hoare_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> g \<lbrace>S\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> g \<lbrace>S\<rbrace>
theory Nondet_VCG

lemma wpc_helper_validE:
  "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,\<lbrace>E\<rbrace>" by (clarsimp simp: wpc_helper_def elim!: hoare_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, \<lbrace>E\<rbrace>
theory Nondet_VCG

lemma wpc_helper_validE_R:
  "\<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>,- \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>,-" by (clarsimp simp: wpc_helper_def elim!: hoare_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> f \<lbrace>R\<rbrace>, - \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> f \<lbrace>R\<rbrace>, -
theory Nondet_VCG

lemma wpc_helper_validR_R:
  "\<lbrace>Q\<rbrace> f -,\<lbrace>E\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> f -,\<lbrace>E\<rbrace>" by (clarsimp simp: wpc_helper_def elim!: hoare_pre)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Q\<rbrace> f -, \<lbrace>E\<rbrace> \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') \<lbrace>P\<rbrace> f -, \<lbrace>E\<rbrace>
theory Nondet_VCG

lemma bind_wp[wp_split]:
  "\<lbrakk> \<And>r. \<lbrace>Q' r\<rbrace> g r \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace>f \<lbrace>Q'\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= (\<lambda>rv. g rv) \<lbrace>Q\<rbrace>" by (fastforce simp: valid_def bind_def' intro: image_eqI[rotated])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>r. \<lbrace>Q' r\<rbrace> g r \<lbrace>Q\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g \<lbrace>Q\<rbrace>
theory Nondet_VCG

lemma seq:
  "\<lbrakk> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>; \<And>x. P x \<Longrightarrow> \<lbrace>C\<rbrace> g x \<lbrace>D\<rbrace>; \<And>x s. B x s \<Longrightarrow> P x \<and> C s \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> do x \<leftarrow> f; g x od \<lbrace>D\<rbrace>" by (fastforce simp: valid_def bind_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>; \<And>x. P x \<Longrightarrow> \<lbrace>C\<rbrace> g x \<lbrace>D\<rbrace>; \<And>x s. B x s \<Longrightarrow> P x \<and> C s\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> f >>= g \<lbrace>D\<rbrace>