kings-crown/FVELER_Isabelle huggingface dataset:
theory ExtraCorres

lemma wp_from_corres_unit:
  "\<lbrakk> corres_underlying state_relation nf nf' r G G' f f';
     \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>P'\<rbrace> f' \<lbrace>\<lambda>_. Q'\<rbrace>; nf \<Longrightarrow> no_fail P f \<rbrakk> \<Longrightarrow>
  \<lbrace>\<lambda>s'. \<exists>s. (s,s') \<in> state_relation \<and> P s \<and> G s \<and> P' s' \<and> G' s'\<rbrace>
  f' \<lbrace>\<lambda>_ s'. \<exists>s. (s,s') \<in> state_relation \<and> Q s \<and> Q' s'\<rbrace>" by (auto intro!: wp_from_corres_u_unit)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corres_underlying state_relation nf nf' r G G' f f'; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>; \<lbrace>P'\<rbrace> f' \<lbrace>\<lambda>_. Q'\<rbrace>; nf \<Longrightarrow> no_fail P f\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> P s \<and> G s \<and> P' s' \<and> G' s'\<rbrace> f' \<lbrace>\<lambda>_ s'. \<exists>s. (s, s') \<in> state_relation \<and> Q s \<and> Q' s'\<rbrace>
theory ExtraCorres

lemma hoare_from_abs:
  assumes corres: "corres_underlying srel nf nf' rrel G G' f f'"
  assumes cross2: "\<And>s s' r r'. \<lbrakk>(s, s') \<in> srel; rrel r r'; Q r s; S s\<rbrakk> \<Longrightarrow> Q' r' s'"
  assumes abs_valid: "\<lbrace>P and R\<rbrace> f \<lbrace>\<lambda>rv. Q rv and S\<rbrace>"
  assumes cross1: "\<And>s s'. \<lbrakk>(s, s') \<in> srel; P' s'; R' s'\<rbrakk> \<Longrightarrow> P s"
  assumes nf: "nf \<Longrightarrow> no_fail (P and R and G) f"
  shows "\<lbrace>P' and G' and R' and ex_abs_underlying srel (G and R)\<rbrace> f' \<lbrace>Q'\<rbrace>" using assms apply (clarsimp simp: valid_def ex_abs_underlying_def corres_underlying_def no_fail_def) by fast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P' and G' and R' and ex_abs_underlying srel (G and R)\<rbrace> f' \<lbrace>Q'\<rbrace> proof (prove)
using this:
corres_underlying srel nf nf' rrel G G' f f'
\<lbrakk>(?s, ?s') \<in> srel; rrel ?r ?r'; Q ?r ?s; S ?s\<rbrakk> \<Longrightarrow> Q' ?r' ?s'
\<lbrace>P and R\<rbrace> f \<lbrace>\<lambda>rv. Q rv and S\<rbrace>
\<lbrakk>(?s, ?s') \<in> srel; P' ?s'; R' ?s'\<rbrakk> \<Longrightarrow> P ?s
nf \<Longrightarrow> no_fail (P and R and G) f

goal (1 subgoal):
 1. \<lbrace>P' and G' and R' and ex_abs_underlying srel (G and R)\<rbrace> f' \<lbrace>Q'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b sa. \<lbrakk>\<forall>x\<in>srel. case x of (s, s') \<Rightarrow> G s \<and> G' s' \<longrightarrow> (nf \<longrightarrow> \<not> snd (f s)) \<longrightarrow> (\<forall>x\<in>fst (f' s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f s). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> rrel r r') \<and> (nf' \<longrightarrow> \<not> snd (f' s')); \<And>s s' r r'. \<lbrakk>(s, s') \<in> srel; rrel r r'; Q r s; S s\<rbrakk> \<Longrightarrow> Q' r' s'; \<forall>s. P s \<and> R s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, s') \<Rightarrow> Q r s' \<and> S s'); \<And>s s'. \<lbrakk>(s, s') \<in> srel; P' s'; R' s'\<rbrakk> \<Longrightarrow> P s; nf \<Longrightarrow> \<forall>s. P s \<and> R s \<and> G s \<longrightarrow> \<not> snd (f s); (a, b) \<in> fst (f' s); P' s; G' s; R' s; (sa, s) \<in> srel; G sa; R sa\<rbrakk> \<Longrightarrow> Q' a b
theory ExtraCorres

lemma hoare_from_abs_inv:
  assumes abs_valid: "f \<lbrace>P\<rbrace>"
  assumes cross: "\<And>s s'. (s, s') \<in> srel \<Longrightarrow> P s = P' s'"
  assumes corres: "corres_underlying srel nf nf' rrel G G' f f'"
  assumes nf: "nf \<Longrightarrow> no_fail (P and G) f"
  shows "\<lbrace>P' and G' and ex_abs_underlying srel G\<rbrace> f' \<lbrace>\<lambda>_. P'\<rbrace>" using assms by (fastforce intro: hoare_from_abs[where R=\<top> and S=\<top> and R'=\<top> and Q="\<lambda>_. P" , simplified])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P' and G' and ex_abs_underlying srel G\<rbrace> f' \<lbrace>\<lambda>_. P'\<rbrace> proof (prove)
using this:
\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. P\<rbrace>
(?s, ?s') \<in> srel \<Longrightarrow> P ?s = P' ?s'
corres_underlying srel nf nf' rrel G G' f f'
nf \<Longrightarrow> no_fail (P and G) f

goal (1 subgoal):
 1. \<lbrace>P' and G' and ex_abs_underlying srel G\<rbrace> f' \<lbrace>\<lambda>_. P'\<rbrace>
theory ExtraCorres

lemma corres_from_valid_det:
  assumes det: "det_wp P f"
  assumes nf': "nf' \<Longrightarrow> no_fail (P' and ex_abs_underlying srel P) f'"
  assumes valid:
    "\<And>s rv t.
      \<lbrakk>fst (f s) = {(rv, t)}; P s\<rbrakk>
      \<Longrightarrow> \<lbrace>\<lambda>s'. P' s' \<and> (s, s') \<in> srel\<rbrace> f' \<lbrace>\<lambda>rv' t'. (t, t') \<in> srel \<and> rrel rv rv'\<rbrace>"
  shows "corres_underlying srel nf nf' rrel P P' f f'" apply (clarsimp simp: corres_underlying_def) apply (intro conjI) apply (insert det) apply (clarsimp simp: det_wp_def) apply (force dest: use_valid[OF _ valid]) apply (fastforce dest: nf' simp: no_fail_def ex_abs_underlying_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying srel nf nf' rrel P P' f f' proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> srel; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (f' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> rrel r r') \<and> (nf' \<longrightarrow> \<not> snd (f' b)) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> srel; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> rrel r r'
 2. \<And>a b. \<lbrakk>(a, b) \<in> srel; P a; P' b; nf \<longrightarrow> \<not> snd (f a)\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd (f' b) proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> srel; P a; P' b; nf \<longrightarrow> \<not> snd (f a); det_wp P f\<rbrakk> \<Longrightarrow> \<forall>x\<in>fst (f' b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (f a). case x of (r, t) \<Rightarrow> (t, t') \<in> srel \<and> rrel r r'
 2. \<And>a b. \<lbrakk>(a, b) \<in> srel; P a; P' b; nf \<longrightarrow> \<not> snd (f a); det_wp P f\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd (f' b) proof (prove)
goal (2 subgoals):
 1. \<And>a b aa ba. \<lbrakk>(a, b) \<in> srel; P a; P' b; nf \<longrightarrow> \<not> snd (f a); \<forall>s. P s \<longrightarrow> (\<exists>a b. f s = ({(a, b)}, False)); (aa, ba) \<in> fst (f' b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (f a). case x of (r, t) \<Rightarrow> (t, ba) \<in> srel \<and> rrel r aa
 2. \<And>a b. \<lbrakk>(a, b) \<in> srel; P a; P' b; nf \<longrightarrow> \<not> snd (f a); det_wp P f\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd (f' b) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> srel; P a; P' b; nf \<longrightarrow> \<not> snd (f a); det_wp P f\<rbrakk> \<Longrightarrow> nf' \<longrightarrow> \<not> snd (f' b) proof (prove)
goal:
No subgoals!
theory ExtraCorres

lemma gets_the_corres_ex_abs':
 "\<lbrakk>no_ofail P a; no_ofail (P' and ex_abs_underlying sr P) b\<rbrakk> \<Longrightarrow>
   corres_underlying sr False True r P P' (gets_the a) (gets_the b)
   = (\<forall>s s'. P s \<and> P' s' \<and> (s, s') \<in> sr \<longrightarrow> r (the (a s)) (the (b s')))" by (fastforce simp: gets_the_def no_ofail_def corres_underlying_def split_def exec_gets
                      assert_opt_def fail_def return_def ex_abs_underlying_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_ofail P a; no_ofail (P' and ex_abs_underlying sr P) b\<rbrakk> \<Longrightarrow> corres_underlying sr False True r P P' (gets_the a) (gets_the b) = (\<forall>s s'. P s \<and> P' s' \<and> (s, s') \<in> sr \<longrightarrow> r (the (a s)) (the (b s')))
theory ExtraCorres

lemma gets_the_corres':
 "\<lbrakk>no_ofail P a; no_ofail P' b\<rbrakk> \<Longrightarrow>
   corres_underlying sr False True r P P' (gets_the a) (gets_the b)
   = (\<forall>s s'. P s \<and> P' s' \<and> (s, s') \<in> sr \<longrightarrow> r (the (a s)) (the (b s')))" apply (erule gets_the_corres_ex_abs') apply (fastforce intro: no_ofail_pre_imp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_ofail P a; no_ofail P' b\<rbrakk> \<Longrightarrow> corres_underlying sr False True r P P' (gets_the a) (gets_the b) = (\<forall>s s'. P s \<and> P' s' \<and> (s, s') \<in> sr \<longrightarrow> r (the (a s)) (the (b s'))) proof (prove)
goal (1 subgoal):
 1. no_ofail P' b \<Longrightarrow> no_ofail (P' and ex_abs_underlying sr P) b proof (prove)
goal:
No subgoals!
theory ExtraCorres

lemma gets_the_corres_relation:
 "\<lbrakk>no_ofail P f; corres_underlying sr False True r P P' (gets_the f) (gets_the f');
   P s; P' s'; (s, s') \<in> sr\<rbrakk>
  \<Longrightarrow> r (the (f s)) (the (f' s'))" apply (rule_tac P=P and a=f and b=f' and P'=P'
               in gets_the_corres_ex_abs'[THEN iffD1, rule_format];
         fastforce?) apply (rule no_ofail_gets_the_eq[THEN iffD2]) apply (fastforce intro: corres_u_nofail) done


\<comment> \<open>Some @{term corres_underlying} rules for @{term whileLoop}\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_ofail P f; corres_underlying sr False True r P P' (gets_the f) (gets_the f'); P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> r (the (f s)) (the (f' s')) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_ofail P f; corres_underlying sr False True r P P' (gets_the f) (gets_the f'); P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> no_ofail (P' and ex_abs_underlying sr P) f' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_ofail P f; corres_underlying sr False True r P P' (gets_the f) (gets_the f'); P s; P' s'; (s, s') \<in> sr\<rbrakk> \<Longrightarrow> no_fail (P' and ex_abs_underlying sr P) (gets_the f') proof (prove)
goal:
No subgoals!
theory ExtraCorres

lemma ifM_corres:
  assumes   test: "corres_underlying srel nf nf' (=) A A' test test'"
  and          l: "corres_underlying srel nf nf' rrel Q Q' a a'"
  and          r: "corres_underlying srel nf nf' rrel R R' b b'"
  and  abs_valid: "\<lbrace>B\<rbrace> test \<lbrace>\<lambda>c s. c \<longrightarrow> Q s\<rbrace>"
                  "\<lbrace>C\<rbrace> test \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> R s\<rbrace>"
  and conc_valid: "\<lbrace>B'\<rbrace> test' \<lbrace>\<lambda>c s. c \<longrightarrow> Q' s\<rbrace>"
                  "\<lbrace>C'\<rbrace> test' \<lbrace>\<lambda>c s. \<not> c \<longrightarrow> R' s\<rbrace>"
  shows "corres_underlying srel nf nf' rrel (A and B and C) (A' and B' and C')
           (ifM test a b) (ifM test' a' b')" unfolding ifM_def apply (rule corres_guard_imp) apply (rule corres_split[OF test]) apply (erule corres_if[OF _ l r]) apply (wpsimp wp: abs_valid conc_valid hoare_vcg_if_lift2)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying srel nf nf' rrel (A and B and C) (A' and B' and C') (ifM test a b) (ifM test' a' b') proof (prove)
goal (1 subgoal):
 1. corres_underlying srel nf nf' rrel (A and B and C) (A' and B' and C') (do c <- test;
if c then a else b
od) (do c <- test';
if c then a' else b'
od) proof (prove)
goal (3 subgoals):
 1. corres_underlying srel nf nf' rrel ?Q ?Q' (do c <- test;
if c then a else b
od) (do c <- test';
if c then a' else b'
od)
 2. \<And>s. (A and B and C) s \<Longrightarrow> ?Q s
 3. \<And>s. (A' and B' and C') s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>c ca. c = ca \<Longrightarrow> corres_underlying srel nf nf' rrel (?R4 c) (?R'4 ca) (if c then a else b) (if ca then a' else b')
 2. \<lbrace>?Q4\<rbrace> test \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> test' \<lbrace>?R'4\<rbrace>
 4. \<And>s. (A and B and C) s \<Longrightarrow> (A and ?Q4) s
 5. \<And>s. (A' and B' and C') s \<Longrightarrow> (A' and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> test \<lbrace>\<lambda>c. if c then Q else R\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> test' \<lbrace>\<lambda>ca. if ca then Q' else R'\<rbrace>
 3. \<And>s. (A and B and C) s \<Longrightarrow> (A and ?Q4) s
 4. \<And>s. (A' and B' and C') s \<Longrightarrow> (A' and ?Q'4) s proof (prove)
goal:
No subgoals!
theory ExtraCorres

lemma notM_corres:
  "corres_underlying srel nf nf' (=) G G' a a'
   \<Longrightarrow> corres_underlying srel nf nf' (=) G G' (notM a) (notM a')" unfolding notM_def apply (rule corres_guard_imp) apply (erule corres_split) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying srel nf nf' (=) G G' a a' \<Longrightarrow> corres_underlying srel nf nf' (=) G G' (notM a) (notM a') proof (prove)
goal (1 subgoal):
 1. corres_underlying srel nf nf' (=) G G' a a' \<Longrightarrow> corres_underlying srel nf nf' (=) G G' (do c <- a;
return (\<not> c)
od) (do c <- a';
return (\<not> c)
od) proof (prove)
goal (3 subgoals):
 1. corres_underlying srel nf nf' (=) G G' a a' \<Longrightarrow> corres_underlying srel nf nf' (=) ?Q ?Q' (do c <- a;
return (\<not> c)
od) (do c <- a';
return (\<not> c)
od)
 2. \<And>s. \<lbrakk>corres_underlying srel nf nf' (=) G G' a a'; G s\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s. \<lbrakk>corres_underlying srel nf nf' (=) G G' a a'; G' s\<rbrakk> \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>c ca. c = ca \<Longrightarrow> corres_underlying srel nf nf' (=) (?R4 c) (?R'4 ca) (return (\<not> c)) (return (\<not> ca))
 2. \<lbrace>?Q4\<rbrace> a \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> a' \<lbrace>?R'4\<rbrace>
 4. \<And>s. \<lbrakk>corres_underlying srel nf nf' (=) G G' a a'; G s\<rbrakk> \<Longrightarrow> (G and ?Q4) s
 5. \<And>s. \<lbrakk>corres_underlying srel nf nf' (=) G G' a a'; G' s\<rbrakk> \<Longrightarrow> (G' and ?Q'4) s proof (prove)
goal:
No subgoals!
theory ExtraCorres

lemma ifM_to_top_of_bind:
  "((ifM test true false) >>= z) = ifM test (true >>= z) (false >>= z)" by (force simp: ifM_def bind_def split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ifM test true false >>= z = ifM test (true >>= z) (false >>= z)
theory SpecValid_R

lemma use_spec':
  assumes x: "\<And>s. s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>"
  shows      "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" apply (clarsimp simp: valid_def) apply (cut_tac s=s in x) apply (clarsimp simp: valid_def spec_valid_def) apply (erule(1) my_BallE, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (f s); s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (f s); \<forall>x\<in>fst (f s). case x of (x, xa) \<Rightarrow> Q x xa\<rbrakk> \<Longrightarrow> Q a b proof (prove)
goal:
No subgoals!
theory SpecValid_R

lemma use_specE':
  "\<lbrakk> \<And>s. s \<turnstile> \<lbrace>P'\<rbrace> f' \<lbrace>Q'\<rbrace>,\<lbrace>E\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>P'\<rbrace> f' \<lbrace>Q'\<rbrace>,\<lbrace>E\<rbrace>" apply (simp add: validE_def spec_validE_def) apply (fold spec_valid_def) apply (simp add: use_spec') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. s \<turnstile> \<lbrace>P'\<rbrace> f' \<lbrace>Q'\<rbrace>, \<lbrace>E\<rbrace>) \<Longrightarrow> \<lbrace>P'\<rbrace> f' \<lbrace>Q'\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<lbrace>\<lambda>sa. sa = s \<and> P' sa\<rbrace> f' \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q' r s\<rbrace>) \<Longrightarrow> \<lbrace>P'\<rbrace> f' \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q' r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>s. s \<turnstile> \<lbrace>P'\<rbrace> f' \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q' r s\<rbrace>) \<Longrightarrow> \<lbrace>P'\<rbrace> f' \<lbrace>\<lambda>v s. case v of Inl e \<Rightarrow> E e s | Inr r \<Rightarrow> Q' r s\<rbrace> proof (prove)
goal:
No subgoals!
theory SpecValid_R

lemma drop_equalled_validE:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. s = s' \<and> P s\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (erule hoare_pre, clarsimp)

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

lemma drop_spec_valid[wp_split]:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" apply (simp add: spec_valid_def) apply (erule hoare_vcg_precond_imp) apply clarsimp done

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

lemma drop_spec_validE[wp_split]:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" apply (simp add: spec_validE_def) apply (erule hoare_vcg_precond_impE) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace> \<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. sa = s \<and> P sa \<Longrightarrow> P sa proof (prove)
goal:
No subgoals!
theory SpecValid_R

lemma split_spec_bind[wp_split]:
  assumes x: "\<And>rv s''. (rv, s'') \<in> fst (f s') \<Longrightarrow> s'' \<turnstile> \<lbrace>B rv\<rbrace> g rv \<lbrace>C\<rbrace>"
  shows "s' \<turnstile> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace>
   \<Longrightarrow> s' \<turnstile> \<lbrace>A\<rbrace> f >>= g \<lbrace>C\<rbrace>" apply (clarsimp simp: spec_valid_def valid_def bind_def lift_def split_def) apply (erule(1) my_BallE, simp) apply (drule x) apply (fastforce simp: spec_valid_def valid_def split_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> \<lbrace>A\<rbrace> f \<lbrace>B\<rbrace> \<Longrightarrow> s' \<turnstile> \<lbrace>A\<rbrace> f >>= g \<lbrace>C\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>A s'; (a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); \<forall>x\<in>fst (f s'). B (fst x) (snd x)\<rbrakk> \<Longrightarrow> C aa ba proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>A s'; (a, b) \<in> fst (f s'); (aa, ba) \<in> fst (g a b); B a b\<rbrakk> \<Longrightarrow> C aa ba proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ba. \<lbrakk>A s'; (aa, ba) \<in> fst (g a b); B a b; b \<turnstile> \<lbrace>B a\<rbrace> g a \<lbrace>C\<rbrace>\<rbrakk> \<Longrightarrow> C aa ba proof (prove)
goal:
No subgoals!
theory SpecValid_R

lemma split_spec_if[wp_split]:
  "\<lbrakk> G \<Longrightarrow> s' \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>;
     \<not> G \<Longrightarrow> s' \<turnstile> \<lbrace>P'\<rbrace> f' \<lbrace>Q\<rbrace>
   \<rbrakk>  \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)\<rbrace> if G then f else f' \<lbrace>Q\<rbrace>" by (cases G, simp+)

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

lemma split_spec_ifE[wp_split]:
  "\<lbrakk> G \<Longrightarrow> s' \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>;
     \<not> 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> P' s)\<rbrace> if G then f else f' \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by (cases G, simp+)

(* 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> f' \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>\<rbrakk> \<Longrightarrow> s' \<turnstile> \<lbrace>\<lambda>s. (G \<longrightarrow> P s) \<and> (\<not> G \<longrightarrow> P' s)\<rbrace> if G then f else f' \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory SpecValid_R

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

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

lemma spec_fun_applyE [wp_split]:
  "s \<turnstile> \<lbrace>P\<rbrace> f x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> f $ x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by simp

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

lemma split_spec_K_bind[wp_split]:
  "s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> K_bind f x \<lbrace>Q\<rbrace>" by simp

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

lemma split_spec_K_bindE[wp_split]:
  "s \<turnstile> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace> \<Longrightarrow> s \<turnstile> \<lbrace>P\<rbrace> K_bind f x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by simp

(* 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> K_bind f x \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>