kings-crown/FVELER_Isabelle huggingface dataset:
theory SpecValid_R

lemma fudge_hoare:
  "s \<turnstile> \<lbrace>P\<rbrace> \<lambda>s. f s \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" .

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory SpecValid_R

lemma split_spec_whenE [wp_split]:
  "\<lbrakk> G \<Longrightarrow> s' \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk>  \<Longrightarrow>
     s' \<turnstile> \<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> Q () s)\<rbrace> whenE G f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" apply (cases G, simp_all add: whenE_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (G \<Longrightarrow> s' \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> Q () s)\<rbrace> whenE G f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> G \<Longrightarrow> s' \<turnstile> \<lbrace>Q ()\<rbrace> returnOk () \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal:
No subgoals!
theory SpecValid_R

lemma spec_valid_conj_lift:
  "\<lbrakk> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; s \<turnstile> \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace> \<rbrakk>
     \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>" apply (simp add: spec_valid_def) apply (drule(1) hoare_vcg_conj_lift) apply (simp add: conj_comms) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>; s \<turnstile> \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>\<lambda>sa. sa = s \<and> P sa\<rbrace> f \<lbrace>Q\<rbrace>; \<lbrace>\<lambda>sa. sa = s \<and> P' sa\<rbrace> f \<lbrace>Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. sa = s \<and> P sa \<and> P' sa\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>\<lambda>sa. sa = s \<and> P' sa\<rbrace> f \<lbrace>Q'\<rbrace>; \<lbrace>\<lambda>sa. (sa = s \<and> P sa) \<and> sa = s \<and> P' sa\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. sa = s \<and> P sa \<and> P' sa\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace> proof (prove)
goal:
No subgoals!
theory SpecValid_R

lemma spec_valid_conj_liftE1:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,-; s \<turnstile> \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>,\<lbrace>E'\<rbrace> \<rbrakk>
     \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>,\<lbrace>E'\<rbrace>" apply (simp add: spec_validE_def) apply (drule(1) hoare_vcg_conj_liftE1) apply (simp add: conj_comms pred_conj_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -; s \<turnstile> \<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>E'\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, \<lbrace>E'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, -; \<lbrace>\<lambda>sa. sa = s \<and> P' sa\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>E'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. sa = s \<and> P sa \<and> P' sa\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, \<lbrace>E'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>\<lambda>sa. sa = s \<and> P' sa\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>E'\<rbrace>; \<lbrace>P and (\<lambda>sa. sa = s \<and> P' sa)\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, \<lbrace>E'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. sa = s \<and> P sa \<and> P' sa\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, \<lbrace>E'\<rbrace> proof (prove)
goal:
No subgoals!
theory SpecValid_R

lemma spec_valid_conj_liftE2:
  "\<lbrakk> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>,-; s \<turnstile> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E'\<rbrace> \<rbrakk>
     \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>,\<lbrace>E'\<rbrace>" apply (simp add: spec_validE_def) apply (drule(1) hoare_vcg_conj_liftE1) apply (simp add: conj_comms pred_conj_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>, -; s \<turnstile> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E'\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>\<lambda>s. P s \<and> P' s\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, \<lbrace>E'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>, -; \<lbrace>\<lambda>sa. sa = s \<and> P' sa\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. sa = s \<and> P sa \<and> P' sa\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, \<lbrace>E'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>\<lambda>sa. sa = s \<and> P' sa\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E'\<rbrace>; \<lbrace>P and (\<lambda>sa. sa = s \<and> P' sa)\<rbrace> f \<lbrace>\<lambda>rv s. Q' rv s \<and> Q rv s\<rbrace>, \<lbrace>E'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. sa = s \<and> P sa \<and> P' sa\<rbrace> f \<lbrace>\<lambda>rv s. Q rv s \<and> Q' rv s\<rbrace>, \<lbrace>E'\<rbrace> proof (prove)
goal:
No subgoals!
theory SpecValid_R

lemma hoare_pre_spec_valid:
  "\<lbrakk> s \<turnstile> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>; P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" apply (simp add: spec_valid_def) apply (erule hoare_pre) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>; P s \<Longrightarrow> P' s\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>\<lambda>sa. sa = s \<and> P' sa\<rbrace> f \<lbrace>Q\<rbrace>; P s \<Longrightarrow> P' s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. sa = s \<and> P sa\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>P s \<Longrightarrow> P' s; sa = s \<and> P sa\<rbrakk> \<Longrightarrow> sa = s \<and> P' sa proof (prove)
goal:
No subgoals!
theory SpecValid_R

lemma hoare_pre_spec_validE:
  "\<lbrakk> s \<turnstile> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" apply (simp add: spec_validE_def) apply (erule hoare_pre) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> \<lbrace>P'\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; P s \<Longrightarrow> P' s\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>\<lambda>sa. sa = s \<and> P' sa\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; P s \<Longrightarrow> P' s\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>sa. sa = s \<and> P sa\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>sa. \<lbrakk>P s \<Longrightarrow> P' s; sa = s \<and> P sa\<rbrakk> \<Longrightarrow> sa = s \<and> P' sa proof (prove)
goal:
No subgoals!
theory SpecValid_R

lemma spec_validE_if:
  "\<lbrakk> G \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<not> G \<Longrightarrow> s \<turnstile> \<lbrace>P'\<rbrace> g \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P and P'\<rbrace> if G then f else g \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" apply (cases G, simp_all) apply (clarsimp elim!: hoare_pre_spec_validE)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; \<not> G \<Longrightarrow> s \<turnstile> \<lbrace>P'\<rbrace> g \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P and P'\<rbrace> if G then f else g \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; G\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P and P'\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
 2. \<lbrakk>s \<turnstile> \<lbrace>P'\<rbrace> g \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>; \<not> G\<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P and P'\<rbrace> g \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal:
No subgoals!
theory SpecValid_R

lemma spec_strengthen_post:
  "\<lbrakk> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>; \<And>s r. Q' s r \<Longrightarrow> Q s r \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" by (simp add: spec_valid_def valid_def
                split_def split: sum.splits)

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

lemma spec_strengthen_postE:
  "\<lbrakk> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q'\<rbrace>, \<lbrace>E\<rbrace>; \<And>s r. Q' s r \<Longrightarrow> Q s r \<rbrakk> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>" by (simp add: spec_valid_def spec_validE_def validE_def valid_def
                split_def split: sum.splits)

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

lemma (in submonad_args) argsD1:
  "\<And>x s. guard s \<Longrightarrow> fetch (replace x s) = x" by (simp add: args)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>x s. guard s \<Longrightarrow> fetch (replace x s) = x
theory SubMonadLib

lemma (in submonad) guarded_sm:
  "\<And>s. guard s \<Longrightarrow>
   fn m s = (do
     substate \<leftarrow> gets fetch;
     (rv, substate') \<leftarrow> select_f (m substate);
     modify (replace substate');
     return rv
   od) s" unfolding fn_is_sm submonad_fn_def by (simp add: stateAssert_def get_def assert_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s. guard s \<Longrightarrow> fn m s = (do substate <- gets fetch;
(rv, substate') <- select_f (m substate);
modify (replace substate');
return rv
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. guard s \<Longrightarrow> (do stateAssert guard [];
substate <- gets fetch;
(rv, substate') <- select_f (m substate);
modify (replace substate');
return rv
od) s = (do substate <- gets fetch;
(rv, substate') <- select_f (m substate);
modify (replace substate');
return rv
od) s
theory SubMonadLib

lemma modify_modify:
  "modify fn1 >>= (\<lambda>x. modify fn2) = modify (fn2 \<circ> fn1)" by (simp add: bind_def modify_def get_def put_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- modify fn1;
modify fn2
od = modify (fn2 \<circ> fn1)
theory SubMonadLib

lemma stateAssert_stateAssert:
  "(stateAssert g [] >>= (\<lambda>u. stateAssert g' [])) = stateAssert (g and g') []" by (simp add: ext stateAssert_def bind_def get_def assert_def fail_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do u <- stateAssert g [];
stateAssert g' []
od = stateAssert (g and g') []
theory SubMonadLib

lemma modify_stateAssert:
  "\<lbrakk> \<And>s x. g (r x s) = g s \<rbrakk> \<Longrightarrow>
   (modify (r x) >>= (\<lambda>u. stateAssert g []))
            = (stateAssert g [] >>= (\<lambda>u. modify (r x)))" by (simp add: ext stateAssert_def bind_def get_def assert_def fail_def
                return_def modify_def put_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s x. g (r x s) = g s) \<Longrightarrow> do u <- modify (r x);
stateAssert g []
od = do u <- stateAssert g [];
modify (r x)
od
theory SubMonadLib

lemma gets_stateAssert:
  "(gets f >>= (\<lambda>x. stateAssert g' [] >>= (\<lambda>u. m x)))
            = (stateAssert g' [] >>= (\<lambda>u. gets f >>= (\<lambda>x. m x)))" by (simp add: ext stateAssert_def bind_def gets_def get_def
                assert_def fail_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- gets f;
u <- stateAssert g' [];
m x
od = do u <- stateAssert g' [];
gets f >>= m
od
theory SubMonadLib

lemma select_f_stateAssert:
  "empty_fail m \<Longrightarrow>
   (select_f (m a) >>= (\<lambda>x. stateAssert g [] >>= (\<lambda>u. n x))) =
   (stateAssert g [] >>= (\<lambda>u. select_f (m a) >>= (\<lambda>x. n x)))" apply (rule ext) apply (clarsimp simp: stateAssert_def bind_def select_f_def get_def
                        assert_def return_def fail_def split_def image_image) apply (simp only: image_def) apply (clarsimp simp: stateAssert_def bind_def select_f_def get_def
                        assert_def return_def fail_def split_def image_image) apply (simp only: image_def mem_simps empty_fail_def simp_thms) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail m \<Longrightarrow> do x <- select_f (m a);
u <- stateAssert g [];
n x
od = do u <- stateAssert g [];
select_f (m a) >>= n
od proof (prove)
goal (1 subgoal):
 1. \<And>x. empty_fail m \<Longrightarrow> (do x <- select_f (m a);
u <- stateAssert g [];
n x
od) x = (do u <- stateAssert g [];
select_f (m a) >>= n
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x. empty_fail m \<Longrightarrow> (g x \<longrightarrow> (\<Union>x\<in>fst (m a) \<times> {x}. \<Union>xa\<in>fst ((if g (snd x) then return () else fail) (snd x)). fst (n (fst x) (snd xa))) = (\<Union>x\<in>fst (m a) \<times> {x}. fst (n (fst x) (snd x)))) \<and> (\<not> g x \<longrightarrow> (\<exists>aa b. (aa, b) \<in> fst (m a)) \<or> snd (m a)) proof (prove)
goal (1 subgoal):
 1. \<And>x. empty_fail m \<Longrightarrow> (g x \<longrightarrow> \<Union> {y. \<exists>x\<in>fst (m a) \<times> {x}. y = \<Union> {y. \<exists>xa\<in>fst ((if g (snd x) then return () else fail) (snd x)). y = fst (n (fst x) (snd xa))}} = \<Union> {y. \<exists>x\<in>fst (m a) \<times> {x}. y = fst (n (fst x) (snd x))}) \<and> (\<not> g x \<longrightarrow> (\<exists>aa b. (aa, b) \<in> fst (m a)) \<or> snd (m a)) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>empty_fail m; \<not> g x; \<not> snd (m a)\<rbrakk> \<Longrightarrow> \<exists>aa b. (aa, b) \<in> fst (m a) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>s. fst (m s) = {} \<longrightarrow> snd (m s); \<not> g x; \<not> snd (m a)\<rbrakk> \<Longrightarrow> \<exists>aa b. (aa, b) \<in> fst (m a) proof (prove)
goal:
No subgoals!
theory SubMonadLib

lemma bind_select_f_bind':
  shows "(select_f (m s) >>= (\<lambda>x. select_f (split n x))) = (select_f ((m >>= n) s))" apply (rule ext) apply (force simp: select_f_def bind_def split_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- select_f (m s);
select_f (case x of (x, xa) \<Rightarrow> n x xa)
od = select_f ((m >>= n) s) proof (prove)
goal (1 subgoal):
 1. \<And>x. (do x <- select_f (m s);
select_f (case x of (x, xa) \<Rightarrow> n x xa)
od) x = select_f ((m >>= n) s) x proof (prove)
goal:
No subgoals!
theory SubMonadLib

lemma bind_select_f_bind:
  "(select_f (m1 s) >>= (\<lambda>x. select_f (m2 (fst x) (snd x)))) = (select_f ((m1 >>= m2) s))" by (insert bind_select_f_bind' [where m=m1 and n=m2 and s=s],
      simp add: split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do x <- select_f (m1 s);
select_f (m2 (fst x) (snd x))
od = select_f ((m1 >>= m2) s)
theory SubMonadLib

lemma select_from_gets: "select_f (gets f s) = return (f s, s)" apply (rule ext) apply (simp add: select_f_def return_def simpler_gets_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. select_f (gets f s) = return (f s, s) proof (prove)
goal (1 subgoal):
 1. \<And>x. select_f (gets f s) x = return (f s, s) x proof (prove)
goal:
No subgoals!
theory SubMonadLib

lemma select_from_gets':
  "(select_f \<circ> gets f) = (\<lambda>s. return (f s, s))" apply (rule ext) apply (simp add: o_def select_from_gets) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. select_f \<circ> gets f = (\<lambda>s. return (f s, s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. (select_f \<circ> gets f) s = return (f s, s) proof (prove)
goal:
No subgoals!
theory SubMonadLib

lemma bind_subst_lift:
  "(f >>= g) = h \<Longrightarrow> (do x \<leftarrow> f; y \<leftarrow> g x; j y od) = (h >>= j)" by (simp add: bind_assoc[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f >>= g = h \<Longrightarrow> do x <- f;
g x >>= j
od = h >>= j
theory SubMonadLib

lemma modify_gets:
  "\<lbrakk> \<And>x s. g (r x s) = g s; \<And>x s. g s \<longrightarrow> f (r x s) = x \<rbrakk>
   \<Longrightarrow> (modify (r x) >>= (\<lambda>u. stateAssert g [] >>= (\<lambda>u'. gets f)))
            = (stateAssert g [] >>= (\<lambda>u'. modify (r x) >>= (\<lambda>u. return x)))" by (simp add: ext stateAssert_def assert_def modify_def bind_def get_def
                put_def gets_def return_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x s. g (r x s) = g s; \<And>x s. g s \<longrightarrow> f (r x s) = x\<rbrakk> \<Longrightarrow> do u <- modify (r x);
u' <- stateAssert g [];
gets f
od = do u' <- stateAssert g [];
u <- modify (r x);
return x
od
theory SubMonadLib

lemma (in submonad_args) gets_modify:
  "\<And>s. guard s \<Longrightarrow>
   (do x \<leftarrow> gets fetch; u \<leftarrow> modify (replace x); f x od) s = ((gets fetch) >>= f) s" by (clarsimp simp: modify_def gets_def return_def bind_def
                     put_def args get_def
              split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s. guard s \<Longrightarrow> (do x <- gets fetch;
u <- modify (replace x);
f x
od) s = (gets fetch >>= f) s
theory SubMonadLib

lemma (in submonad) guard_preserved:
  "\<And>s s'. \<lbrakk> (rv, s') \<in> fst (fn m s) \<rbrakk> \<Longrightarrow> guard s'" unfolding fn_is_sm submonad_fn_def by (clarsimp simp: stateAssert_def gets_def get_def bind_def modify_def put_def
                     return_def select_f_def replace_preserves_guard in_monad)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. (rv, s') \<in> fst (fn m s) \<Longrightarrow> guard s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. (rv, s') \<in> fst ((do stateAssert guard [];
substate <- gets fetch;
(rv, substate') <- select_f (m substate);
modify (replace substate');
return rv
od) s) \<Longrightarrow> guard s'
theory SubMonadLib

lemma fst_stateAssertD:
  "\<And>s s' v. (v, s') \<in> fst (stateAssert g [] s) \<Longrightarrow> s' = s \<and> g s" by (clarsimp simp: stateAssert_def in_monad)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s s' v. (v, s') \<in> fst (stateAssert g [] s) \<Longrightarrow> s' = s \<and> g s
theory SubMonadLib

lemma (in submonad) guarded_return:
  "\<And>s. guard s \<Longrightarrow> fn (return x) s = return x s" using args guarded_gets by (fastforce simp: gets_def bind_def get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s. guard s \<Longrightarrow> fn (return x) s = return x s proof (prove)
using this:
\<forall>x s. guard s \<longrightarrow> fetch (replace x s) = x
\<forall>x y s. replace x (replace y s) = replace x s
\<forall>s. replace (fetch s) s = s
guard ?s \<Longrightarrow> fn (gets ?f) ?s = gets (?f \<circ> fetch) ?s

goal (1 subgoal):
 1. \<And>s. guard s \<Longrightarrow> fn (return x) s = return x s
theory SubMonadLib

lemma (in submonad_args) submonad_fn_gets:
  "submonad_fn fetch replace guard (gets f) =
   (stateAssert guard [] >>= (\<lambda>u. gets (f \<circ> fetch)))" apply (simp add: ext select_from_gets submonad_fn_def) apply (rule bind_cong [OF refl]) apply (clarsimp simp: gets_modify dest!: fst_stateAssertD) apply (simp add: gets_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. submonad_fn fetch replace guard (gets f) = do u <- stateAssert guard [];
gets (f \<circ> fetch)
od proof (prove)
goal (1 subgoal):
 1. do y <- stateAssert guard [];
substate <- gets fetch;
y <- modify (replace substate);
return (f substate)
od = do u <- stateAssert guard [];
gets (f \<circ> fetch)
od proof (prove)
goal (1 subgoal):
 1. \<And>v s s'. (v, s') \<in> fst (stateAssert guard [] s) \<Longrightarrow> (do substate <- gets fetch;
y <- modify (replace substate);
return (f substate)
od) s' = gets (f \<circ> fetch) s' proof (prove)
goal (1 subgoal):
 1. \<And>s. guard s \<Longrightarrow> (do substate <- gets fetch;
return (f substate)
od) s = gets (f \<circ> fetch) s proof (prove)
goal:
No subgoals!
theory SubMonadLib

lemma (in submonad) return:
  "fn (return x) = (stateAssert guard [] >>= (\<lambda>u. return x))" using args gets by (fastforce simp: gets_def bind_def get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fn (return x) = do u <- stateAssert guard [];
return x
od proof (prove)
using this:
\<forall>x s. guard s \<longrightarrow> fetch (replace x s) = x
\<forall>x y s. replace x (replace y s) = replace x s
\<forall>s. replace (fetch s) s = s
fn (gets ?f) = do u <- stateAssert guard [];
gets (?f \<circ> fetch)
od

goal (1 subgoal):
 1. fn (return x) = do u <- stateAssert guard [];
return x
od