kings-crown/FVELER_Isabelle huggingface dataset:
theory Strengthen

lemma strengthen_ex[strg]:
  "\<lbrakk> \<And>x. st F (\<longrightarrow>) (P x) (Q x) \<rbrakk>
    \<Longrightarrow> st F (\<longrightarrow>) (\<exists>x. P x) (\<exists>x. Q x)" by (cases F, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. st F (\<longrightarrow>) (P x) (Q x)) \<Longrightarrow> st F (\<longrightarrow>) (\<exists>x. P x) (\<exists>x. Q x)
theory Strengthen

lemma strengthen_Ball[strg]:
  "\<lbrakk> st_ord (Not F) S S';
        \<And>x. x \<in> S \<Longrightarrow> st F (\<longrightarrow>) (P x) (Q x) \<rbrakk>
    \<Longrightarrow> st F (\<longrightarrow>) (\<forall>x \<in> S. P x) (\<forall>x \<in> S'. Q x)" by (cases F, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st (\<not> F) (\<subseteq>) S S'; \<And>x. x \<in> S \<Longrightarrow> st F (\<longrightarrow>) (P x) (Q x)\<rbrakk> \<Longrightarrow> st F (\<longrightarrow>) (\<forall>x\<in>S. P x) (\<forall>x\<in>S'. Q x)
theory Strengthen

lemma strengthen_Bex[strg]:
  "\<lbrakk> st_ord F S S';
        \<And>x. x \<in> S \<Longrightarrow> st F (\<longrightarrow>) (P x) (Q x) \<rbrakk>
    \<Longrightarrow> st F (\<longrightarrow>) (\<exists>x \<in> S. P x) (\<exists>x \<in> S'. Q x)" by (cases F, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st F (\<subseteq>) S S'; \<And>x. x \<in> S \<Longrightarrow> st F (\<longrightarrow>) (P x) (Q x)\<rbrakk> \<Longrightarrow> st F (\<longrightarrow>) (\<exists>x\<in>S. P x) (\<exists>x\<in>S'. Q x)
theory Strengthen

lemma strengthen_Collect[strg]:
  "\<lbrakk> \<And>x. st F (\<longrightarrow>) (P x) (P' x) \<rbrakk>
    \<Longrightarrow> st_ord F {x. P x} {x. P' x}" by (cases F, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. st F (\<longrightarrow>) (P x) (P' x)) \<Longrightarrow> st F (\<subseteq>) {x. P x} {x. P' x}
theory Strengthen

lemma strengthen_mem[strg]:
  "\<lbrakk> st_ord F S S' \<rbrakk>
    \<Longrightarrow> st F (\<longrightarrow>) (x \<in> S) (x \<in> S')" by (cases F, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st F (\<subseteq>) S S' \<Longrightarrow> st F (\<longrightarrow>) (x \<in> S) (x \<in> S')
theory Strengthen

lemma strengthen_ord[strg]:
  "st_ord (\<not> F) x x' \<Longrightarrow> st_ord F y y'
    \<Longrightarrow> st F (\<longrightarrow>) (x \<le> y) (x' \<le> y')" by (cases F, simp_all, (metis order_trans)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st (\<not> F) (\<le>) x x'; st F (\<le>) y y'\<rbrakk> \<Longrightarrow> st F (\<longrightarrow>) (x \<le> y) (x' \<le> y')
theory Strengthen

lemma strengthen_strict_ord[strg]:
  "st_ord (\<not> F) x x' \<Longrightarrow> st_ord F y y'
    \<Longrightarrow> st F (\<longrightarrow>) (x < y) (x' < y')" by (cases F, simp_all, (metis order_le_less_trans order_less_le_trans)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st (\<not> F) (\<le>) x x'; st F (\<le>) y y'\<rbrakk> \<Longrightarrow> st F (\<longrightarrow>) (x < y) (x' < y')
theory Strengthen

lemma strengthen_image[strg]:
  "st_ord F S S' \<Longrightarrow> st_ord F (f ` S) (f ` S')" by (cases F, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st F (\<subseteq>) S S' \<Longrightarrow> st F (\<subseteq>) (f ` S) (f ` S')
theory Strengthen

lemma strengthen_vimage[strg]:
  "st_ord F S S' \<Longrightarrow> st_ord F (f -` S) (f -` S')" by (cases F, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st F (\<subseteq>) S S' \<Longrightarrow> st F (\<subseteq>) (f -` S) (f -` S')
theory Strengthen

lemma strengthen_Int[strg]:
  "st_ord F A A' \<Longrightarrow> st_ord F B B' \<Longrightarrow> st_ord F (A \<inter> B) (A' \<inter> B')" by (cases F, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st F (\<subseteq>) A A'; st F (\<subseteq>) B B'\<rbrakk> \<Longrightarrow> st F (\<subseteq>) (A \<inter> B) (A' \<inter> B')
theory Strengthen

lemma strengthen_Un[strg]:
  "st_ord F A A' \<Longrightarrow> st_ord F B B' \<Longrightarrow> st_ord F (A \<union> B) (A' \<union> B')" by (cases F, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st F (\<subseteq>) A A'; st F (\<subseteq>) B B'\<rbrakk> \<Longrightarrow> st F (\<subseteq>) (A \<union> B) (A' \<union> B')
theory Strengthen

lemma strengthen_UN[strg]:
  "st_ord F A A' \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> st_ord F (B x) (B' x))
    \<Longrightarrow> st_ord F (\<Union>x \<in> A. B x) (\<Union>x \<in> A'. B' x)" by (cases F, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st F (\<subseteq>) A A'; \<And>x. x \<in> A \<Longrightarrow> st F (\<subseteq>) (B x) (B' x)\<rbrakk> \<Longrightarrow> st F (\<subseteq>) (\<Union> (B ` A)) (\<Union> (B' ` A'))
theory Strengthen

lemma strengthen_INT[strg]:
  "st_ord (\<not> F) A A' \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> st_ord F (B x) (B' x))
    \<Longrightarrow> st_ord F (\<Inter>x \<in> A. B x) (\<Inter>x \<in> A'. B' x)" by (cases F, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st (\<not> F) (\<subseteq>) A A'; \<And>x. x \<in> A \<Longrightarrow> st F (\<subseteq>) (B x) (B' x)\<rbrakk> \<Longrightarrow> st F (\<subseteq>) (\<Inter> (B ` A)) (\<Inter> (B' ` A'))
theory Strengthen

lemma strengthen_imp_strengthen_prop[strg]:
  "st False (\<longrightarrow>) P Q \<Longrightarrow> PROP (st_prop1 (Trueprop P) (Trueprop Q))"
  "st True (\<longrightarrow>) P Q \<Longrightarrow> PROP (st_prop2 (Trueprop P) (Trueprop Q))" unfolding st_prop1_def st_prop2_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P =strg<--|=> Q \<Longrightarrow> st_prop1 (P) (Q)) &&& (P =strg-->|=> Q \<Longrightarrow> st_prop2 (P) (Q)) proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>P =strg<--|=> Q; Q\<rbrakk> \<Longrightarrow> P) &&& (\<lbrakk>P =strg-->|=> Q; P\<rbrakk> \<Longrightarrow> Q)
theory Strengthen

lemma st_prop_meta_imp[strg]:
  "PROP (st_prop2 (PROP X) (PROP X'))
    \<Longrightarrow> PROP (st_prop1 (PROP Y) (PROP Y'))
    \<Longrightarrow> PROP (st_prop1 (PROP X \<Longrightarrow> PROP Y) (PROP X' \<Longrightarrow> PROP Y'))"
  "PROP (st_prop1 (PROP X) (PROP X'))
    \<Longrightarrow> PROP (st_prop2 (PROP Y) (PROP Y'))
    \<Longrightarrow> PROP (st_prop2 (PROP X \<Longrightarrow> PROP Y) (PROP X' \<Longrightarrow> PROP Y'))" unfolding st_prop1_def st_prop2_def by (erule meta_mp | assumption)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>st_prop2 PROP X PROP X'; st_prop1 PROP Y PROP Y'\<rbrakk> \<Longrightarrow> st_prop1 (PROP X \<Longrightarrow> PROP Y) (PROP X' \<Longrightarrow> PROP Y')) &&& (\<lbrakk>st_prop1 PROP X PROP X'; st_prop2 PROP Y PROP Y'\<rbrakk> \<Longrightarrow> st_prop2 (PROP X \<Longrightarrow> PROP Y) (PROP X' \<Longrightarrow> PROP Y')) proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>PROP X \<Longrightarrow> PROP X'; PROP Y' \<Longrightarrow> PROP Y; PROP X' \<Longrightarrow> PROP Y'; PROP X\<rbrakk> \<Longrightarrow> PROP Y) &&& (\<lbrakk>PROP X' \<Longrightarrow> PROP X; PROP Y \<Longrightarrow> PROP Y'; PROP X \<Longrightarrow> PROP Y; PROP X'\<rbrakk> \<Longrightarrow> PROP Y')
theory Strengthen

lemma silly_trans:
  "silly x y \<Longrightarrow> silly y z \<Longrightarrow> silly x z" by (simp add: silly_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silly x y; silly y z\<rbrakk> \<Longrightarrow> silly x z
theory Strengthen

lemma silly_refl:
  "silly x x" by (simp add: silly_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. silly x x
theory Strengthen

lemma foo:
  "silly x y \<Longrightarrow> silly a b \<Longrightarrow> silly b c
    \<Longrightarrow> silly x y \<and> (\<forall>x :: nat. silly a c )" using [[strengthen_trace = true]] apply (strengthen silly_trans[mk_strg I E])+ apply (strengthen silly_refl) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silly x y; silly a b; silly b c\<rbrakk> \<Longrightarrow> silly x y \<and> (\<forall>x. silly a c) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silly x y; silly a b; silly b c\<rbrakk> \<Longrightarrow> silly x y \<and> (\<forall>x. silly a c) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silly x y; silly a b; silly b c\<rbrakk> \<Longrightarrow> silly y y \<and> (\<forall>x. silly c c) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silly x y; silly a b; silly b c\<rbrakk> \<Longrightarrow> True \<and> (\<forall>x. True) proof (prove)
goal:
No subgoals!
theory Strengthen

lemma foo_asm:
  "silly x y \<Longrightarrow> silly y z
    \<Longrightarrow> (silly x z \<Longrightarrow> silly a b) \<Longrightarrow> silly z z \<Longrightarrow> silly a b" apply (strengthen_asm silly_trans[mk_strg I A]) apply (strengthen_asm silly_trans[mk_strg I A]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silly x y; silly y z; silly x z \<Longrightarrow> silly a b; silly z z\<rbrakk> \<Longrightarrow> silly a b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silly x y; silly y z; silly z z; silly y z \<Longrightarrow> silly a b\<rbrakk> \<Longrightarrow> silly a b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silly x y; silly y z; silly z z; silly z z \<Longrightarrow> silly a b\<rbrakk> \<Longrightarrow> silly a b proof (prove)
goal:
No subgoals!
theory Strengthen

lemma foo_method:
  "silly x y \<Longrightarrow> silly a b \<Longrightarrow> silly b c
    \<Longrightarrow> silly x y \<and> (\<forall>x :: nat. z \<longrightarrow> silly a c )" using [[strengthen_trace = true]] apply simp apply (strengthen_method \<open>rule silly_trans\<close>) apply (strengthen_method \<open>rule exI[where x=b]\<close>) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silly x y; silly a b; silly b c\<rbrakk> \<Longrightarrow> silly x y \<and> (\<forall>x. z \<longrightarrow> silly a c) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silly x y; silly a b; silly b c\<rbrakk> \<Longrightarrow> silly x y \<and> (\<forall>x. z \<longrightarrow> silly a c) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silly x y; silly a b; silly b c\<rbrakk> \<Longrightarrow> z \<longrightarrow> silly a c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silly x y; silly a b; silly b c\<rbrakk> \<Longrightarrow> z \<longrightarrow> (\<exists>y. silly a y \<and> silly y c) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>silly x y; silly a b; silly b c\<rbrakk> \<Longrightarrow> z \<longrightarrow> silly a b \<and> silly b c proof (prove)
goal:
No subgoals!
theory WPFix

lemma use_strengthen_prop_intro:
  "PROP P \<Longrightarrow> PROP (strengthen_implementation.st_prop1 (PROP Q) (PROP P))
    \<Longrightarrow> PROP Q" unfolding strengthen_implementation.st_prop1_def apply (drule(1) meta_mp)+ apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PROP P; strengthen_implementation.st_prop1 PROP Q PROP P\<rbrakk> \<Longrightarrow> PROP Q proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PROP P; PROP P \<Longrightarrow> PROP Q\<rbrakk> \<Longrightarrow> PROP Q proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PROP P; PROP Q\<rbrakk> \<Longrightarrow> PROP Q proof (prove)
goal:
No subgoals!
theory WPFix

lemma strengthen_to_conjunct1_target:
  "strengthen_implementation.st True (\<longrightarrow>)
    (target_var n (P \<and> Q)) (target_var n P)" by (simp add: strengthen_implementation.st_def target_var_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. target_var n (P \<and> Q) =strg-->|=> target_var n P
theory WPFix

lemma strengthen_to_conjunct2_target_trans:
  "strengthen_implementation.st True (\<longrightarrow>)
        (target_var n Q) R
    \<Longrightarrow> strengthen_implementation.st True (\<longrightarrow>)
        (target_var n (P \<and> Q)) R" by (simp add: strengthen_implementation.st_def target_var_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. target_var n Q =strg-->|=> R \<Longrightarrow> target_var n (P \<and> Q) =strg-->|=> R
theory WPFix

lemma target_var_drop_func:
  "target_var n f = (\<lambda>x. target_var n (f x))" by (simp add: target_var_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. target_var n f = (\<lambda>x. target_var n (f x))
theory WPFix

lemma strg_target_to_true:
  "strengthen_implementation.st F (\<longrightarrow>) (target_var n True) True" by (simp add: target_var_def strengthen_implementation.strengthen_refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. strengthen_implementation.st F (\<longrightarrow>) (target_var n True) True
theory WPFix

lemma demo1:
  "(\<exists>Ia Ib Ic Id Ra.
    (Ia (Suc 0) \<longrightarrow> Qa)
  \<and> (Ib \<longrightarrow> Qb)
  \<and> (Ic \<longrightarrow> Ra)
  \<and> (Id \<longrightarrow> Qc)
  \<and> (Id \<longrightarrow> Qd)
  \<and> (Qa \<and> Qb \<and> Qc \<and> Qd \<longrightarrow> Ia v \<and> Ib \<and> Ic \<and> Id))" apply (intro exI conjI impI) 
   (* apply assumption+ won't work here, since it will pick Id
      incorrectly. the presence of the goal ?Ra is also dangerous.
      wpfix handles this by setting Ra to True and splitting
      Id into a conjunction. *)
   apply (wpfix | assumption)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>Ia Ib Ic Id Ra. (Ia (Suc 0) \<longrightarrow> Qa) \<and> (Ib \<longrightarrow> Qb) \<and> (Ic \<longrightarrow> Ra) \<and> (Id \<longrightarrow> Qc) \<and> (Id \<longrightarrow> Qd) \<and> (Qa \<and> Qb \<and> Qc \<and> Qd \<longrightarrow> Ia v \<and> Ib \<and> Ic \<and> Id) proof (prove)
goal (9 subgoals):
 1. ?Ia (Suc 0) \<Longrightarrow> Qa
 2. ?Ib1 \<Longrightarrow> Qb
 3. ?Ic2 \<Longrightarrow> ?Ra4
 4. ?Id3 \<Longrightarrow> Qc
 5. ?Id3 \<Longrightarrow> Qd
 6. Qa \<and> Qb \<and> Qc \<and> Qd \<Longrightarrow> ?Ia v
 7. Qa \<and> Qb \<and> Qc \<and> Qd \<Longrightarrow> ?Ib1
 8. Qa \<and> Qb \<and> Qc \<and> Qd \<Longrightarrow> ?Ic2
 9. Qa \<and> Qb \<and> Qc \<and> Qd \<Longrightarrow> ?Id3 proof (prove)
goal (9 subgoals):
 1. ?Ia (Suc 0) \<Longrightarrow> Qa
 2. ?Ib1 \<Longrightarrow> Qb
 3. ?Ic2 \<Longrightarrow> ?Ra4
 4. ?Id3 \<Longrightarrow> Qc
 5. ?Id3 \<Longrightarrow> Qd
 6. Qa \<and> Qb \<and> Qc \<and> Qd \<Longrightarrow> ?Ia v
 7. Qa \<and> Qb \<and> Qc \<and> Qd \<Longrightarrow> ?Ib1
 8. Qa \<and> Qb \<and> Qc \<and> Qd \<Longrightarrow> ?Ic2
 9. Qa \<and> Qb \<and> Qc \<and> Qd \<Longrightarrow> ?Id3 proof (prove)
goal (4 subgoals):
 1. Qa \<and> Qb \<and> Qc \<and> Qd \<Longrightarrow> Qa
 2. Qa \<and> Qb \<and> Qc \<and> Qd \<Longrightarrow> Qb
 3. Qa \<and> Qb \<and> Qc \<and> Qd \<Longrightarrow> True
 4. Qa \<and> Qb \<and> Qc \<and> Qd \<Longrightarrow> Qc \<and> Qd proof (prove)
goal:
No subgoals!
theory WPFix

lemma (in datatype_schem_demo) demo3:
  "\<exists>x. \<forall>a b. x (basic a b) = a" apply (rule exI, (rule allI)+) apply (wpfix add: get_basic_0.simps) \<comment> \<open>Only exposes `a` to the schematic.\<close> by (rule refl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>x. \<forall>a b. x (basic a b) = a proof (prove)
goal (1 subgoal):
 1. \<And>a b. ?x (basic a b) = a proof (prove)
goal (1 subgoal):
 1. \<And>a b. ?x6 a (basic a b) = a
theory WP

lemma conj_TrueI2: "P \<Longrightarrow> P \<and> True" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow> P \<and> True
theory Nondet_Empty_Fail

lemma wpc_helper_empty_fail_final:
  "empty_fail f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (empty_fail f)" by (clarsimp simp: wpc_helper_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (empty_fail f)
theory Nondet_Empty_Fail

lemma empty_failI:
  "(\<And>s. fst (m s) = {} \<Longrightarrow> snd (m s)) \<Longrightarrow> empty_fail m" by (simp add: empty_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. fst (m s) = {} \<Longrightarrow> snd (m s)) \<Longrightarrow> empty_fail m
theory Nondet_Empty_Fail

lemma empty_failD:
  "\<lbrakk> empty_fail m; fst (m s) = {} \<rbrakk> \<Longrightarrow> snd (m s)" by (simp add: empty_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail m; fst (m s) = {}\<rbrakk> \<Longrightarrow> snd (m s)
theory Nondet_Empty_Fail

lemma empty_failD3:
  "\<lbrakk> empty_fail f; \<not> snd (f s) \<rbrakk> \<Longrightarrow> fst (f s) \<noteq> {}" by (drule(1) empty_failD2, clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail f; \<not> snd (f s)\<rbrakk> \<Longrightarrow> fst (f s) \<noteq> {}
theory Nondet_Empty_Fail

lemma empty_fail_bindD1:
  "empty_fail (a >>= b) \<Longrightarrow> empty_fail a" unfolding empty_fail_def bind_def by (fastforce simp: split_def image_image)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (a >>= b) \<Longrightarrow> empty_fail a proof (prove)
goal (1 subgoal):
 1. \<forall>s. fst (\<Union> (fst ` (\<lambda>(x, y). b x y) ` fst (a s)), True \<in> snd ` (\<lambda>(x, y). b x y) ` fst (a s) \<or> snd (a s)) = {} \<longrightarrow> snd (\<Union> (fst ` (\<lambda>(x, y). b x y) ` fst (a s)), True \<in> snd ` (\<lambda>(x, y). b x y) ` fst (a s) \<or> snd (a s)) \<Longrightarrow> \<forall>s. fst (a s) = {} \<longrightarrow> snd (a s)
theory Nondet_Empty_Fail

lemma empty_fail_K_bind[empty_fail_cond]:
  "empty_fail f \<Longrightarrow> empty_fail (K_bind f x)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> empty_fail (K_bind f x)
theory Nondet_Empty_Fail

lemma empty_fail_fun_app[empty_fail_cond]:
  "empty_fail (f x) \<Longrightarrow> empty_fail (f $ x)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (f x) \<Longrightarrow> empty_fail (f $ x)
theory Nondet_Empty_Fail

lemma empty_fail_If[empty_fail_cond]:
  "\<lbrakk> P \<Longrightarrow> empty_fail f; \<not>P \<Longrightarrow> empty_fail g \<rbrakk> \<Longrightarrow> empty_fail (if P then f else g)" by (simp split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Longrightarrow> empty_fail f; \<not> P \<Longrightarrow> empty_fail g\<rbrakk> \<Longrightarrow> empty_fail (if P then f else g)
theory Nondet_Empty_Fail

lemma empty_fail_If_applied[empty_fail_cond]:
  "\<lbrakk> P \<Longrightarrow> empty_fail (f x); \<not>P \<Longrightarrow> empty_fail (g x) \<rbrakk> \<Longrightarrow> empty_fail ((if P then f else g) x)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Longrightarrow> empty_fail (f x); \<not> P \<Longrightarrow> empty_fail (g x)\<rbrakk> \<Longrightarrow> empty_fail ((if P then f else g) x)
theory Nondet_Empty_Fail

lemma empty_fail_put[empty_fail_term]:
  "empty_fail (put f)" by (simp add: put_def empty_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (put f)
theory Nondet_Empty_Fail

lemma empty_fail_modify[empty_fail_term]:
  "empty_fail (modify f)" by (simp add: empty_fail_def simpler_modify_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (modify f)
theory Nondet_Empty_Fail

lemma empty_fail_select[empty_fail_cond]:
  "S \<noteq> {} \<Longrightarrow> empty_fail (select S)" by (simp add: empty_fail_def select_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S \<noteq> {} \<Longrightarrow> empty_fail (select S)
theory Nondet_Empty_Fail

lemma empty_fail_bind[empty_fail_cond]:
  "\<lbrakk> empty_fail a; \<And>x. empty_fail (b x) \<rbrakk> \<Longrightarrow> empty_fail (a >>= b)" by (fastforce simp: bind_def empty_fail_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail a; \<And>x. empty_fail (b x)\<rbrakk> \<Longrightarrow> empty_fail (a >>= b)
theory Nondet_Empty_Fail

lemma empty_fail_return[empty_fail_term]:
  "empty_fail (return x)" by (simp add: empty_fail_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (return x)
theory Nondet_Empty_Fail

lemma empty_fail_returnOk[empty_fail_term]:
  "empty_fail (returnOk v)" by (fastforce simp: returnOk_def empty_fail_term)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (returnOk v)
theory Nondet_Empty_Fail

lemma empty_fail_throwError[empty_fail_term]:
  "empty_fail (throwError v)" by (fastforce simp: throwError_def empty_fail_term)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (throwError v)
theory Nondet_Empty_Fail

lemma empty_fail_lift[empty_fail_cond]:
  "\<lbrakk> \<And>x. empty_fail (f x) \<rbrakk> \<Longrightarrow> empty_fail (lift f x)" unfolding lift_def by (auto simp: empty_fail_term split: sum.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. empty_fail (f x)) \<Longrightarrow> empty_fail (lift f x) proof (prove)
goal (1 subgoal):
 1. (\<And>x. empty_fail (f x)) \<Longrightarrow> empty_fail (case x of Inl e \<Rightarrow> throwError e | Inr v' \<Rightarrow> f v')
theory Nondet_Empty_Fail

lemma empty_fail_bindE[empty_fail_cond]:
  "\<lbrakk> empty_fail f; \<And>rv. empty_fail (g rv) \<rbrakk> \<Longrightarrow> empty_fail (f >>=E g)" by (simp add: bindE_def empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail f; \<And>rv. empty_fail (g rv)\<rbrakk> \<Longrightarrow> empty_fail (f >>=E g)
theory Nondet_Empty_Fail

lemma empty_fail_assert[empty_fail_term]:
  "empty_fail (assert P)" unfolding assert_def by (simp add: empty_fail_term)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (assert P) proof (prove)
goal (1 subgoal):
 1. empty_fail (if P then return () else fail)
theory Nondet_Empty_Fail

lemma empty_fail_assert_opt[empty_fail_term]:
  "empty_fail (assert_opt x)" by (simp add: assert_opt_def empty_fail_term split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (assert_opt x)
theory Nondet_Empty_Fail

lemma empty_fail_mk_ef[empty_fail_term]:
  "empty_fail (mk_ef o m)" by (simp add: empty_fail_def mk_ef_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (mk_ef \<circ> m)
theory Nondet_Empty_Fail

lemma empty_fail_gets_the[empty_fail_term]:
  "empty_fail (gets_the f)" unfolding gets_the_def by (simp add: empty_fail_cond empty_fail_term)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (gets_the f) proof (prove)
goal (1 subgoal):
 1. empty_fail (gets f >>= assert_opt)
theory Nondet_Empty_Fail

lemma empty_fail_gets_map[empty_fail_term]:
  "empty_fail (gets_map f p)" unfolding gets_map_def by (simp add: empty_fail_term empty_fail_cond)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (gets_map f p) proof (prove)
goal (1 subgoal):
 1. empty_fail (do m <- gets f;
assert_opt (m p)
od)
theory Nondet_Empty_Fail

lemma empty_fail_whenEs[empty_fail_cond]:
  "(P \<Longrightarrow> empty_fail f) \<Longrightarrow> empty_fail (whenE P f)"
  "(\<not>P \<Longrightarrow> empty_fail f) \<Longrightarrow> empty_fail (unlessE P f)" by (auto simp add: whenE_def unlessE_def empty_fail_term)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((P \<Longrightarrow> empty_fail f) \<Longrightarrow> empty_fail (whenE P f)) &&& ((\<not> P \<Longrightarrow> empty_fail f) \<Longrightarrow> empty_fail (unlessE P f))
theory Nondet_Empty_Fail

lemma empty_fail_assertE[empty_fail_term]:
  "empty_fail (assertE P)" by (simp add: assertE_def empty_fail_term)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (assertE P)
theory Nondet_Empty_Fail

lemma empty_fail_get[empty_fail_term]:
  "empty_fail get" by (simp add: empty_fail_def get_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail get
theory Nondet_Empty_Fail

lemma empty_fail_catch[empty_fail_cond]:
  "\<lbrakk> empty_fail f; \<And>x. empty_fail (g x) \<rbrakk> \<Longrightarrow> empty_fail (catch f g)" by (simp add: catch_def empty_fail_cond empty_fail_term split: sum.split)

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