kings-crown/FVELER_Isabelle huggingface dataset:
theory Corres_C

lemma ccorres_sequence_while_genQ:
  fixes i :: "nat" and xf :: "globals myvars \<Rightarrow> ('c :: len) word"
  assumes one: "\<And>n ys. \<lbrakk> n < length xs \<rbrakk> \<Longrightarrow>
                    ccorres (\<lambda>rv rv'. r' (ys @ [rv]) rv') xf'
                            (F (n * j)) ({s. xf s = of_nat (i + n * j) \<and> r' ys (xf' s)} \<inter> Q) hs
                            (xs ! n) body"
  and      pn: "\<And>n. P n = (n < of_nat (i + length xs * j))"
  and   bodyi: "\<forall>s. xf s < of_nat (i + length xs * j)
      \<longrightarrow> \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> ({s} \<inter> Q) body {t. xf t = xf s \<and> xf_update (\<lambda>x. xf t + of_nat j) t \<in> Q}"
  and      hi: "\<And>n. Suc n < length xs \<Longrightarrow> \<lbrace> F (n * j) \<rbrace> (xs ! n) \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>"
  and     lxs: "i + length xs * j< 2 ^ len_of TYPE('c)"
  and      xf: "\<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s"
  and     xf': "\<forall>s f. xf' (xf_update f s) = (xf' s)"
  and       j: "j > 0"
  shows  "ccorres (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = of_nat (i + length xs * of_nat j))
                  (\<lambda>s. (xf s, xf' s))
                  (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = of_nat i \<and> r' [] (xf' s)} \<inter> Q) hs
                  (sequence xs)
                  (While {s. P (xf s)}
                     (body ;; Basic (\<lambda>s. xf_update (\<lambda>_. xf s + of_nat j) s)))"
  (is "ccorres ?r' ?xf' ?G (?G' \<inter> _) hs (sequence xs) ?body") apply (rule ccorres_sequence_while_genQ' [OF one pn bodyi hi lxs xf xf']) apply simp apply simp apply (clarsimp simp: rf_sr_def xf) apply (simp add: j) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (i + length xs * of_nat j)) (\<lambda>s. (xf s, xf' s)) (\<lambda>s. P 0 \<longrightarrow> F 0 s) ({s. xf s = word_of_nat i \<and> r' [] (xf' s)} \<inter> Q) hs (Nondet_Monad.sequence xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + word_of_nat j) s))) proof (prove)
goal (4 subgoals):
 1. \<And>n ys. n < length xs \<Longrightarrow> n < length xs
 2. \<And>n. Suc n < length xs \<Longrightarrow> Suc n < length xs
 3. \<And>s r f. (s, r) \<in> rf_sr \<Longrightarrow> (s, xf_update f r) \<in> rf_sr
 4. 0 < j proof (prove)
goal (3 subgoals):
 1. \<And>n. Suc n < length xs \<Longrightarrow> Suc n < length xs
 2. \<And>s r f. (s, r) \<in> rf_sr \<Longrightarrow> (s, xf_update f r) \<in> rf_sr
 3. 0 < j proof (prove)
goal (2 subgoals):
 1. \<And>s r f. (s, r) \<in> rf_sr \<Longrightarrow> (s, xf_update f r) \<in> rf_sr
 2. 0 < j proof (prove)
goal (1 subgoal):
 1. 0 < j proof (prove)
goal:
No subgoals!
theory Corres_C

lemma i_xf_for_sequence:
  "\<forall>s f. i_' (i_'_update f s) = f (i_' s) \<and> globals (i_'_update f s) = globals s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s f. i_' (i_'_update f s) = f (i_' s) \<and> globals (i_'_update f s) = globals s
theory Corres_C

lemma ccorres_sequenceE_while_down:
  fixes xf :: "globals myvars \<Rightarrow> ('c :: len) word"
  assumes one: "\<And>n ys. \<lbrakk> n < length xs; n = length ys \<rbrakk> \<Longrightarrow>
                    ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv rv'. r' (ys @ [rv]) rv')) xf'
                            (inl_rrel arrel) axf
                            (F n) (Q \<inter> {s. xf s = (startv - of_nat n) \<and> r' ys (xf' s)}) hs
                            (xs ! n) body"
  and      pn: "\<And>n. (n < length xs \<longrightarrow> P (startv - of_nat n)) \<and> \<not> P (startv - of_nat (length xs))"
  and   bodyi: "\<And>s. s \<in> Q \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> {t. xf t = xf s}), UNIV"
  and      hi: "\<And>n. n < length xs \<Longrightarrow> \<lbrace> F n \<rbrace> (xs ! n) \<lbrace>\<lambda>_. F (Suc n)\<rbrace>,-"
  and      xf: "\<forall>s f. xf (xf_update f s) = f (xf s)"
  and     xf': "\<forall>s f. xf' (xf_update f s) = (xf' s)
                               \<and> ((xf_update f s \<in> Q) = (s \<in> Q))
                               \<and> (\<forall>s'. ((s', xf_update f s) \<in> sr) = ((s', s) \<in> sr))"
  shows  "ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = (startv - of_nat (length xs))))
                  (\<lambda>s. (xf s, xf' s)) arrel axf
                  (F 0) (Q \<inter> {s. xf s = (startv - of_nat 0) \<and> r' [] (xf' s)}) hs
                  (sequenceE xs)
                  (While {s. P (xf s)}
                     (body ;; Basic (\<lambda>s. xf_update (\<lambda>_. xf s - 1) s)))"
  (is "ccorres_underlying sr \<Gamma> (inr_rrel ?r') ?xf' arrel axf ?G ?G' hs (sequenceE xs) ?body") by (rule ccorres_sequenceE_while_gen_either_way
                   [OF one, where xf_update=xf_update],
      simp_all add: bodyi hi xf xf' pn)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = startv - word_of_nat (length xs))) (\<lambda>s. (xf s, xf' s)) arrel axf (F 0) (Q \<inter> {s. xf s = startv - word_of_nat 0 \<and> r' [] (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s - 1) s)))
theory Corres_C

lemma ccorres_sequenceE_while_gen':
  fixes i :: "nat" and xf :: "globals myvars \<Rightarrow> ('c :: len) word"
  assumes one: "\<And>n ys. \<lbrakk> n < length xs; n = length ys \<rbrakk> \<Longrightarrow>
                    ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv rv'. r' (ys @ [rv]) rv')) xf'
                            (inl_rrel arrel) axf
                            (F n) (Q \<inter> {s. xf s = of_nat (i + n) \<and> r' ys (xf' s)}) hs
                            (xs ! n) body"
  and      pn: "\<And>n. P n = (n < of_nat (i + length xs))"
  and   bodyi: "\<And>s. s \<in> Q \<Longrightarrow> \<Gamma> \<turnstile>\<^bsub>/UNIV\<^esub> {s} body (Q \<inter> {t. xf t = xf s}), UNIV"
  and      hi: "\<And>n. n < length xs \<Longrightarrow> \<lbrace> F n \<rbrace> (xs ! n) \<lbrace>\<lambda>_. F (Suc n)\<rbrace>,-"
  and     lxs: "i + length xs < 2 ^ len_of TYPE('c)"
  and      xf: "\<forall>s f. xf (xf_update f s) = f (xf s)"
  and     xf': "\<forall>s f. xf' (xf_update f s) = (xf' s)
                               \<and> ((xf_update f s \<in> Q) = (s \<in> Q))
                               \<and> (\<forall>s'. ((s', xf_update f s) \<in> sr) = ((s', s) \<in> sr))"
  shows  "ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = of_nat (i + length xs)))
                  (\<lambda>s. (xf s, xf' s)) arrel axf
                  (F 0) (Q \<inter> {s. xf s = of_nat i \<and> r' [] (xf' s)}) hs
                  (sequenceE xs)
                  (While {s. P (xf s)}
                     (body ;; Basic (\<lambda>s. xf_update (\<lambda>_. xf s + 1) s)))"
  (is "ccorres_underlying sr \<Gamma> (inr_rrel ?r') ?xf' arrel axf ?G ?G' hs (sequenceE xs) ?body") apply (rule ccorres_sequenceE_while_gen_either_way
                   [OF one, where xf_update=xf_update, simplified add_0_right],
         simp_all add: bodyi hi lxs xf xf' pn) apply clarsimp apply (simp only: Abs_fnat_hom_add, rule of_nat_mono_maybe) apply (rule lxs) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr \<Gamma> (inr_rrel (\<lambda>rv (i', rv'). r' rv rv' \<and> i' = word_of_nat (i + length xs))) (\<lambda>s. (xf s, xf' s)) arrel axf (F 0) (Q \<inter> {s. xf s = word_of_nat i \<and> r' [] (xf' s)}) hs (sequenceE xs) (While {s. P (xf s)} (body;;
Basic (\<lambda>s. xf_update (\<lambda>_. xf s + 1) s))) proof (prove)
goal (1 subgoal):
 1. \<And>n. n < length xs \<longrightarrow> word_of_nat i + word_of_nat n < word_of_nat i + word_of_nat (length xs) proof (prove)
goal (1 subgoal):
 1. \<And>n. n < length xs \<Longrightarrow> word_of_nat i + word_of_nat n < word_of_nat i + word_of_nat (length xs) proof (prove)
goal (2 subgoals):
 1. \<And>n. n < length xs \<Longrightarrow> i + length xs < 2 ^ LENGTH('c)
 2. \<And>n. n < length xs \<Longrightarrow> i + n < i + length xs proof (prove)
goal (1 subgoal):
 1. \<And>n. n < length xs \<Longrightarrow> i + n < i + length xs proof (prove)
goal:
No subgoals!
theory Corres_C

lemma never_continues_creturn [C_simp_throws]:
  "never_continues \<Gamma> (creturn rtu xfu v)" by (auto simp: never_continues_def creturn_def elim: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. never_continues \<Gamma> (creturn rtu xfu v)
theory Corres_C

lemma never_continues_creturn_void [C_simp_throws]:
  "never_continues \<Gamma> (creturn_void rtu)" by (auto simp: never_continues_def creturn_void_def elim: exec_elim_cases)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. never_continues \<Gamma> (creturn_void rtu)
theory L4VerifiedLinks

lemma corresXF_impl_corres:
  "\<lbrakk> corresXF st (\<lambda>_ _. ()) (\<lambda>_ _. ()) P G G'; no_fail \<top> G \<rbrakk> \<Longrightarrow>
   corres_underlying {(a, b). a = st b} nf True (dc \<oplus> dc) \<top> P G G'" apply (clarsimp simp: corres_underlying_def corresXF_def no_fail_def) apply (erule allE, erule (1) impE) apply clarsimp apply (erule (1) my_BallE) apply (force split: sum.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>corresXF st (\<lambda>_ _. ()) (\<lambda>_ _. ()) P G G'; no_fail (\<lambda>_. True) G\<rbrakk> \<Longrightarrow> corres_underlying {(a, b). a = st b} nf True (dc \<oplus> dc) (\<lambda>_. True) P G G' proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (G' s). case x of (Inl ra, t) \<Rightarrow> (Inl (), st t) \<in> fst (G (st s)) | (Inr ra, t) \<Rightarrow> (Inr (), st t) \<in> fst (G (st s))) \<and> \<not> snd (G' s); \<forall>s. \<not> snd (G s); P b; (a, ba) \<in> fst (G' b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (G (st b)). case x of (r, t) \<Rightarrow> t = st ba \<and> (dc \<oplus> dc) r a proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>\<forall>s. \<not> snd (G s); P b; (a, ba) \<in> fst (G' b); (\<forall>x\<in>fst (G' b). case x of (Inl ra, t) \<Rightarrow> (Inl (), st t) \<in> fst (G (st b)) | (Inr ra, t) \<Rightarrow> (Inr (), st t) \<in> fst (G (st b))) \<and> \<not> snd (G' b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (G (st b)). case x of (r, t) \<Rightarrow> t = st ba \<and> (dc \<oplus> dc) r a proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>\<forall>s. \<not> snd (G s); P b; (a, ba) \<in> fst (G' b); \<forall>x\<in>fst (G' b). case x of (Inl ra, t) \<Rightarrow> (Inl (), st t) \<in> fst (G (st b)) | (Inr ra, t) \<Rightarrow> (Inr (), st t) \<in> fst (G (st b)); \<not> snd (G' b)\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (G (st b)). case x of (r, t) \<Rightarrow> t = st ba \<and> (dc \<oplus> dc) r a proof (prove)
goal (1 subgoal):
 1. \<And>b a ba. \<lbrakk>\<forall>s. \<not> snd (G s); P b; (a, ba) \<in> fst (G' b); \<not> snd (G' b); case (a, ba) of (Inl ra, t) \<Rightarrow> (Inl (), st t) \<in> fst (G (st b)) | (Inr ra, t) \<Rightarrow> (Inr (), st t) \<in> fst (G (st b))\<rbrakk> \<Longrightarrow> \<exists>x\<in>fst (G (st b)). case x of (r, t) \<Rightarrow> t = st ba \<and> (dc \<oplus> dc) r a proof (prove)
goal:
No subgoals!
theory AutoCorresModifiesProofs

lemma valid_inv_weaken:
  "\<lbrakk> valid P f (\<lambda>_. R); \<And>s. I s \<Longrightarrow> P s; \<And>s. R s \<Longrightarrow> I' s \<rbrakk> \<Longrightarrow> valid I f (\<lambda>_. I')" by (fastforce simp: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. R\<rbrace>; \<And>s. I s \<Longrightarrow> P s; \<And>s. R s \<Longrightarrow> I' s\<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I'\<rbrace>
theory AutoCorresModifiesProofs

lemma valid_inv_weaken':
  "\<lbrakk> valid I f (\<lambda>_. Q); \<And>s. Q s \<Longrightarrow> I' s \<rbrakk> \<Longrightarrow> valid I f (\<lambda>_. I')" by (rule valid_inv_weaken)

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

lemma All_to_all:
  "Trueprop (\<forall>x. P x) \<equiv> (\<And>x. P x)" by presburger

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x. P x \<equiv> (\<And>x. P x)
theory AutoCorresModifiesProofs

lemma when_inv[valid_inv]:
  "\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace> \<Longrightarrow> \<lbrace>I\<rbrace> when c f \<lbrace>\<lambda>_. I\<rbrace>" apply wp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace> \<Longrightarrow> \<lbrace>I\<rbrace> when c f \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; I s\<rbrakk> \<Longrightarrow> (if c then I else I) s proof (prove)
goal:
No subgoals!
theory AutoCorresModifiesProofs

lemma bind_inv[valid_inv]:
  "\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace> \<Longrightarrow> (\<And>x. \<lbrace>I\<rbrace> g x \<lbrace>\<lambda>_. I\<rbrace>) \<Longrightarrow> \<lbrace>I\<rbrace> f >>= g \<lbrace>\<lambda>_. I\<rbrace>" apply (wp; assumption) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; \<And>x. \<lbrace>I\<rbrace> g x \<lbrace>\<lambda>_. I\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> f >>= g \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal:
No subgoals!
theory AutoCorresModifiesProofs

lemma guard_inv[valid_inv]:
  "\<lbrace>I\<rbrace> guard G \<lbrace>\<lambda>_. I\<rbrace>" by (fastforce simp: valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> guard G \<lbrace>\<lambda>_. I\<rbrace>
theory AutoCorresModifiesProofs

lemma modify_inv[valid_inv]:
  "(\<And>s. I s \<Longrightarrow> I (f s)) \<Longrightarrow> \<lbrace>I\<rbrace> modify f \<lbrace>\<lambda>_. I\<rbrace>" apply wp by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. I s \<Longrightarrow> I (f s)) \<Longrightarrow> \<lbrace>I\<rbrace> modify f \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>s. I s \<Longrightarrow> I (f s); I s\<rbrakk> \<Longrightarrow> I (f s)
theory AutoCorresModifiesProofs

lemma skip_inv[valid_inv]:
  "\<lbrace>I\<rbrace> skip \<lbrace>\<lambda>_. I\<rbrace>" by (rule skip_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> skip \<lbrace>\<lambda>_. I\<rbrace>
theory AutoCorresModifiesProofs

lemma select_inv[valid_inv]:
  "\<lbrace>I\<rbrace> select f \<lbrace>\<lambda>_. I\<rbrace>" by (rule hoare_weaken_pre, rule select_wp, blast)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> select f \<lbrace>\<lambda>_. I\<rbrace>
theory AutoCorresModifiesProofs

lemma condition_inv[valid_inv]:
  "\<lbrace>I\<rbrace> t \<lbrace>\<lambda>_. I\<rbrace> \<Longrightarrow> \<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace> \<Longrightarrow> \<lbrace>I\<rbrace> condition c t f\<lbrace>\<lambda>_. I\<rbrace>" apply (rule hoare_weaken_pre) apply (rule condition_wp) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>I\<rbrace> t \<lbrace>\<lambda>_. I\<rbrace>; \<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> condition c
  t
  f \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrace>I\<rbrace> t \<lbrace>\<lambda>_. I\<rbrace>; \<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q\<rbrace> condition c
  t
  f \<lbrace>\<lambda>_. I\<rbrace>
 2. \<And>s. \<lbrakk>\<lbrace>I\<rbrace> t \<lbrace>\<lambda>_. I\<rbrace>; \<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; I s\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<lbrace>I\<rbrace> t \<lbrace>\<lambda>_. I\<rbrace>; \<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q3\<rbrace> t \<lbrace>\<lambda>_. I\<rbrace>
 2. \<lbrakk>\<lbrace>I\<rbrace> t \<lbrace>\<lambda>_. I\<rbrace>; \<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?R3\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>
 3. \<And>s. \<lbrakk>\<lbrace>I\<rbrace> t \<lbrace>\<lambda>_. I\<rbrace>; \<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; I s\<rbrakk> \<Longrightarrow> if c s then ?Q3 s else ?R3 s proof (prove)
goal:
No subgoals!
theory AutoCorresModifiesProofs

lemma whileLoop_inv[valid_inv]:
  "\<lbrakk>\<And>r. \<lbrace>I\<rbrace> b r \<lbrace>\<lambda>_. I\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> whileLoop c b r \<lbrace>\<lambda>_. I\<rbrace>" apply (rule whileLoop_wp) apply (blast intro: hoare_weaken_pre) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>r. \<lbrace>I\<rbrace> b r \<lbrace>\<lambda>_. I\<rbrace>) \<Longrightarrow> \<lbrace>I\<rbrace> whileLoop c
  b r \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>r. (\<And>r. \<lbrace>I\<rbrace> b r \<lbrace>\<lambda>_. I\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. I s \<and> c r s\<rbrace> b r \<lbrace>\<lambda>a. I\<rbrace>
 2. \<And>r s. \<lbrakk>\<And>r. \<lbrace>I\<rbrace> b r \<lbrace>\<lambda>_. I\<rbrace>; I s; \<not> c r s\<rbrakk> \<Longrightarrow> I s proof (prove)
goal (1 subgoal):
 1. \<And>r s. \<lbrakk>\<And>r. \<lbrace>I\<rbrace> b r \<lbrace>\<lambda>_. I\<rbrace>; I s; \<not> c r s\<rbrakk> \<Longrightarrow> I s proof (prove)
goal:
No subgoals!
theory AutoCorresModifiesProofs

lemma valid_case_prod_inv[valid_inv]:
  "(\<And>x y. \<lbrace>I\<rbrace> f x y \<lbrace>\<lambda>_. I\<rbrace>) \<Longrightarrow> \<lbrace>I\<rbrace> case v of (x, y) \<Rightarrow> f x y \<lbrace>\<lambda>_. I\<rbrace>" apply wp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. \<lbrace>I\<rbrace> f x y \<lbrace>\<lambda>_. I\<rbrace>) \<Longrightarrow> \<lbrace>I\<rbrace> case v of (x, y) \<Rightarrow> f x y \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x y. (\<And>x y. \<lbrace>I\<rbrace> f x y \<lbrace>\<lambda>_. I\<rbrace>) \<Longrightarrow> \<lbrace>?P1 x y\<rbrace> f x y \<lbrace>\<lambda>_. I\<rbrace>
 2. \<And>s. \<lbrakk>\<And>x y. \<lbrace>I\<rbrace> f x y \<lbrace>\<lambda>_. I\<rbrace>; I s\<rbrakk> \<Longrightarrow> (case v of (x, xa) \<Rightarrow> ?P1 x xa) s proof (prove)
goal:
No subgoals!
theory AutoCorresModifiesProofs

lemma unknown_inv[valid_inv]:
  "\<lbrace>I\<rbrace> unknown \<lbrace>\<lambda>_. I\<rbrace>" apply (unfold unknown_def) apply (rule select_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> unknown \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> select UNIV \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal:
No subgoals!
theory AutoCorresModifiesProofs

lemma throwError_inv[valid_inv]:
  "\<lbrace>I\<rbrace> throwError e \<lbrace>\<lambda>_. I\<rbrace>" by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>I\<rbrace> throwError e \<lbrace>\<lambda>_. I\<rbrace>
theory AutoCorresModifiesProofs

lemma catch_inv[valid_inv]:
  "\<lbrakk> \<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; \<And>e. \<lbrace>I\<rbrace> h e \<lbrace>\<lambda>_. I\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> catch f h \<lbrace>\<lambda>_. I\<rbrace>" apply wpsimp apply assumption apply (simp add: validE_def) by assumption

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; \<And>e. \<lbrace>I\<rbrace> h e \<lbrace>\<lambda>_. I\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> f <catch> h \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; \<And>e. \<lbrace>I\<rbrace> h e \<lbrace>\<lambda>_. I\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?E2 x\<rbrace> h x \<lbrace>\<lambda>_. I\<rbrace>
 2. \<lbrakk>\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; \<And>e. \<lbrace>I\<rbrace> h e \<lbrace>\<lambda>_. I\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q1\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>, \<lbrace>?E2\<rbrace>
 3. \<And>s. \<lbrakk>\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; \<And>e. \<lbrace>I\<rbrace> h e \<lbrace>\<lambda>_. I\<rbrace>; I s\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; \<And>e. \<lbrace>I\<rbrace> h e \<lbrace>\<lambda>_. I\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?Q1\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>, \<lbrace>\<lambda>x. I\<rbrace>
 2. \<And>s. \<lbrakk>\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; \<And>e. \<lbrace>I\<rbrace> h e \<lbrace>\<lambda>_. I\<rbrace>; I s\<rbrakk> \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; \<And>e. \<lbrace>I\<rbrace> h e \<lbrace>\<lambda>_. I\<rbrace>; I s\<rbrakk> \<Longrightarrow> I s
theory AutoCorresModifiesProofs

lemma whileLoopE_inv[valid_inv]:
  "(\<And>r. \<lbrace>I\<rbrace> b r \<lbrace>\<lambda>_. I\<rbrace>) \<Longrightarrow> \<lbrace>I\<rbrace> whileLoopE c b r \<lbrace>\<lambda>_. I\<rbrace>" apply (unfold whileLoopE_def) apply (rule whileLoop_inv) apply (auto simp: lift_def split: sum.splits intro: throwError_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>r. \<lbrace>I\<rbrace> b r \<lbrace>\<lambda>_. I\<rbrace>) \<Longrightarrow> \<lbrace>I\<rbrace> whileLoopE c
  b r \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>r. \<lbrace>I\<rbrace> b r \<lbrace>\<lambda>_. I\<rbrace>) \<Longrightarrow> \<lbrace>I\<rbrace> whileLoop (\<lambda>r s. case r of Inl a \<Rightarrow> False | Inr v \<Rightarrow> c v s)
  (Nondet_Monad.lift b) (Inr r) \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>r. (\<And>r. \<lbrace>I\<rbrace> b r \<lbrace>\<lambda>_. I\<rbrace>) \<Longrightarrow> \<lbrace>I\<rbrace> Nondet_Monad.lift b r \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal:
No subgoals!
theory AutoCorresModifiesProofs

lemma bindE_inv[valid_inv]:
  "\<lbrakk> \<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; \<And>x. \<lbrace>I\<rbrace> g x \<lbrace>\<lambda>_. I\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> f >>=E g \<lbrace>\<lambda>_. I\<rbrace>" apply (unfold bindE_def) apply (rule bind_inv) apply (auto simp: lift_def split: sum.splits intro: throwError_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; \<And>x. \<lbrace>I\<rbrace> g x \<lbrace>\<lambda>_. I\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> f >>=E g \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; \<And>x. \<lbrace>I\<rbrace> g x \<lbrace>\<lambda>_. I\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> f >>= Nondet_Monad.lift g \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; \<And>x. \<lbrace>I\<rbrace> g x \<lbrace>\<lambda>_. I\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>
 2. \<And>x. \<lbrakk>\<lbrace>I\<rbrace> f \<lbrace>\<lambda>_. I\<rbrace>; \<And>x. \<lbrace>I\<rbrace> g x \<lbrace>\<lambda>_. I\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>I\<rbrace> Nondet_Monad.lift g x \<lbrace>\<lambda>_. I\<rbrace> proof (prove)
goal:
No subgoals!