kings-crown/FVELER_Isabelle huggingface dataset:
theory TacticTutorial

lemma "A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X \<Longrightarrow> A \<or> B \<or> C \<or> D \<or> E \<Longrightarrow> X" apply (tactic \<open>HEADGOAL (REPEAT_ALL_NEW (eresolve_tac @{context} @{thms disjE}))\<close>) apply (tactic \<open>subgoal_auto_tac @{context} 3\<close>)  (* Only removes "C ==> X" case. *)
      apply (tactic \<open>subgoal_auto_tac @{context} 4\<close>)  (* Only removes "E ==> X" case. *)
   oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; A \<or> B \<or> C \<or> D \<or> E\<rbrakk> \<Longrightarrow> X proof (prove)
goal (5 subgoals):
 1. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; A\<rbrakk> \<Longrightarrow> X
 2. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; B\<rbrakk> \<Longrightarrow> X
 3. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; C\<rbrakk> \<Longrightarrow> X
 4. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; D\<rbrakk> \<Longrightarrow> X
 5. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; E\<rbrakk> \<Longrightarrow> X proof (prove)
goal (4 subgoals):
 1. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; A\<rbrakk> \<Longrightarrow> X
 2. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; B\<rbrakk> \<Longrightarrow> X
 3. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; D\<rbrakk> \<Longrightarrow> X
 4. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; E\<rbrakk> \<Longrightarrow> X proof (prove)
goal (4 subgoals):
 1. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; A\<rbrakk> \<Longrightarrow> X
 2. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; B\<rbrakk> \<Longrightarrow> X
 3. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; D\<rbrakk> \<Longrightarrow> X
 4. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; E\<rbrakk> \<Longrightarrow> X proof (prove)
goal (3 subgoals):
 1. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; A\<rbrakk> \<Longrightarrow> X
 2. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; B\<rbrakk> \<Longrightarrow> X
 3. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; D\<rbrakk> \<Longrightarrow> X proof (prove)
goal (3 subgoals):
 1. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; A\<rbrakk> \<Longrightarrow> X
 2. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; B\<rbrakk> \<Longrightarrow> X
 3. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; D\<rbrakk> \<Longrightarrow> X
theory TacticTutorial

lemma "A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X \<Longrightarrow> A \<or> B \<or> C \<or> D \<or> E \<Longrightarrow> X" apply (tactic \<open>HEADGOAL (REPEAT_ALL_NEW (eresolve_tac @{context} @{thms disjE}))\<close>) apply (tactic \<open>better_subgoal_auto_tac @{context} 3\<close>)  (* Only removes "C ==> X" case. *)
      apply (tactic \<open>better_subgoal_auto_tac @{context} 4\<close>)  (* Only removes "E ==> X" case. *)
   oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; A \<or> B \<or> C \<or> D \<or> E\<rbrakk> \<Longrightarrow> X proof (prove)
goal (5 subgoals):
 1. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; A\<rbrakk> \<Longrightarrow> X
 2. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; B\<rbrakk> \<Longrightarrow> X
 3. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; C\<rbrakk> \<Longrightarrow> X
 4. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; D\<rbrakk> \<Longrightarrow> X
 5. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; E\<rbrakk> \<Longrightarrow> X proof (prove)
goal (4 subgoals):
 1. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; A\<rbrakk> \<Longrightarrow> X
 2. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; B\<rbrakk> \<Longrightarrow> X
 3. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; D\<rbrakk> \<Longrightarrow> X
 4. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; E\<rbrakk> \<Longrightarrow> X proof (prove)
goal (4 subgoals):
 1. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; A\<rbrakk> \<Longrightarrow> X
 2. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; B\<rbrakk> \<Longrightarrow> X
 3. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; D\<rbrakk> \<Longrightarrow> X
 4. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; E\<rbrakk> \<Longrightarrow> X proof (prove)
goal (3 subgoals):
 1. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; A\<rbrakk> \<Longrightarrow> X
 2. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; B\<rbrakk> \<Longrightarrow> X
 3. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; D\<rbrakk> \<Longrightarrow> X proof (prove)
goal (3 subgoals):
 1. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; A\<rbrakk> \<Longrightarrow> X
 2. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; B\<rbrakk> \<Longrightarrow> X
 3. \<lbrakk>A = B \<and> B = C \<and> C = D \<and> D = E \<and> E = X; D\<rbrakk> \<Longrightarrow> X
theory Trace_No_Throw

lemma no_throw_def':
  "no_throw P A = (\<forall>s. P s \<longrightarrow> (\<forall>(r, t) \<in> mres (A s). (\<exists>x. r = Inr x)))" by (clarsimp simp: no_throw_def validE_def2 split_def split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_throw P A = (\<forall>s. P s \<longrightarrow> (\<forall>(r, t)\<in>mres (A s). \<exists>x. r = Inr x))
theory Trace_No_Throw

lemma no_throw_returnOk[simp]:
  "no_throw P (returnOk a)" unfolding no_throw_def by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_throw P (returnOk a) proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> returnOk a \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>
theory Trace_No_Throw

lemma no_throw_liftE[simp]:
  "no_throw P (liftE x)" by (wpsimp simp: liftE_def no_throw_def validE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_throw P (liftE x)
theory Trace_No_Throw

lemma no_throw_bindE:
  "\<lbrakk> no_throw A X; \<And>a. no_throw B (Y a); \<lbrace> A \<rbrace> X \<lbrace> \<lambda>_. B \<rbrace>,\<lbrace> \<lambda>_ _. True \<rbrace> \<rbrakk>
   \<Longrightarrow> no_throw A (X >>=E Y)" unfolding no_throw_def using hoare_validE_cases seqE by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_throw A X; \<And>a. no_throw B (Y a); \<lbrace>A\<rbrace> X \<lbrace>\<lambda>_. B\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> no_throw A (X >>=E Y) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>A\<rbrace> X \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>; \<And>a. \<lbrace>B\<rbrace> Y a \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>; \<lbrace>A\<rbrace> X \<lbrace>\<lambda>_. B\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> X >>=E Y \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
using this:
\<lbrakk>\<lbrace>?P\<rbrace> ?f \<lbrace>?Q\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>; \<lbrace>?P\<rbrace> ?f \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?R\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?P\<rbrace> ?f \<lbrace>?Q\<rbrace>, \<lbrace>?R\<rbrace>
\<lbrakk>\<lbrace>?A\<rbrace> ?f \<lbrace>?B\<rbrace>, \<lbrace>?E\<rbrace>; \<And>x. \<lbrace>?B x\<rbrace> ?g x \<lbrace>?C\<rbrace>, \<lbrace>?E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?A\<rbrace> ?f >>=E ?g \<lbrace>?C\<rbrace>, \<lbrace>?E\<rbrace>

goal (1 subgoal):
 1. \<lbrakk>\<lbrace>A\<rbrace> X \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>; \<And>a. \<lbrace>B\<rbrace> Y a \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>; \<lbrace>A\<rbrace> X \<lbrace>\<lambda>_. B\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> X >>=E Y \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>
theory Trace_No_Throw

lemma no_throw_bindE_simple:
  "\<lbrakk> no_throw \<top> L; \<And>x. no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L >>=E R)" using hoareE_TrueI no_throw_bindE by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>no_throw (\<lambda>_. True) L; \<And>x. no_throw (\<lambda>_. True) (R x)\<rbrakk> \<Longrightarrow> no_throw (\<lambda>_. True) (L >>=E R) proof (prove)
using this:
\<lbrace>?P\<rbrace> ?f \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r _. True\<rbrace>
\<lbrakk>no_throw ?A ?X; \<And>a. no_throw ?B (?Y a); \<lbrace>?A\<rbrace> ?X \<lbrace>\<lambda>_. ?B\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>\<rbrakk> \<Longrightarrow> no_throw ?A (?X >>=E ?Y)

goal (1 subgoal):
 1. \<lbrakk>no_throw (\<lambda>_. True) L; \<And>x. no_throw (\<lambda>_. True) (R x)\<rbrakk> \<Longrightarrow> no_throw (\<lambda>_. True) (L >>=E R)
theory Trace_No_Throw

lemma no_throw_handleE_simple:
  "\<lbrakk> \<And>x. no_throw \<top> L \<or> no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L <handle> R)" by (fastforce simp: no_throw_def' handleE_def handleE'_def validE_def valid_def bind_def return_def
                      mres_def image_def
                split: sum.splits tmres.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. no_throw (\<lambda>_. True) L \<or> no_throw (\<lambda>_. True) (R x)) \<Longrightarrow> no_throw (\<lambda>_. True) (L <handle> R)
theory Trace_No_Throw

lemma no_throw_handle2:
  "\<lbrakk> \<And>a. no_throw Y (B a); \<lbrace> X \<rbrace> A \<lbrace> \<lambda>_ _. True \<rbrace>,\<lbrace> \<lambda>_. Y \<rbrace> \<rbrakk> \<Longrightarrow> no_throw X (A <handle2> B)" by (fastforce simp: no_throw_def' handleE'_def validE_def valid_def bind_def return_def mres_def
                      image_def
                split: sum.splits tmres.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a. no_throw Y (B a); \<lbrace>X\<rbrace> A \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. Y\<rbrace>\<rbrakk> \<Longrightarrow> no_throw X (A <handle2> B)
theory Trace_No_Throw

lemma no_throw_handle:
  "\<lbrakk> \<And>a. no_throw Y (B a); \<lbrace> X \<rbrace> A \<lbrace> \<lambda>_ _. True \<rbrace>,\<lbrace> \<lambda>_. Y \<rbrace> \<rbrakk> \<Longrightarrow> no_throw X (A <handle> B)" unfolding handleE_def by (rule no_throw_handle2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a. no_throw Y (B a); \<lbrace>X\<rbrace> A \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. Y\<rbrace>\<rbrakk> \<Longrightarrow> no_throw X (A <handle> B) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>a. no_throw Y (B a); \<lbrace>X\<rbrace> A \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. Y\<rbrace>\<rbrakk> \<Longrightarrow> no_throw X (A <handle2> B)
theory Trace_No_Throw

lemma no_throw_fail[simp]:
  "no_throw P fail" by (clarsimp simp: no_throw_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_throw P fail
theory Trace_No_Throw

lemma handleE'_nothrow_lhs:
  "no_throw \<top> L \<Longrightarrow> no_throw \<top> (L <handle2> R)" unfolding no_throw_def using handleE'_wp[rotated] by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_throw (\<lambda>_. True) L \<Longrightarrow> no_throw (\<lambda>_. True) (L <handle2> R) proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> L \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> L <handle2> R \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace> proof (prove)
using this:
\<lbrakk>\<lbrace>?P\<rbrace> ?f \<lbrace>?Q\<rbrace>, \<lbrace>?F\<rbrace>; \<And>x. \<lbrace>?F x\<rbrace> ?handler x \<lbrace>?Q\<rbrace>, \<lbrace>?E\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>?P\<rbrace> ?f <handle2> ?handler \<lbrace>?Q\<rbrace>, \<lbrace>?E\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> L \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> L <handle2> R \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>
theory Trace_No_Throw

lemma handleE'_nothrow_rhs:
  "\<lbrakk> \<And>x. no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L <handle2> R)" unfolding no_throw_def by (metis hoareE_TrueI no_throw_def no_throw_handle2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. no_throw (\<lambda>_. True) (R x)) \<Longrightarrow> no_throw (\<lambda>_. True) (L <handle2> R) proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrace>\<lambda>_. True\<rbrace> R x \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> L <handle2> R \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_ _. False\<rbrace>
theory Trace_No_Throw

lemma handleE_nothrow_lhs:
  "no_throw \<top> L \<Longrightarrow> no_throw \<top> (L <handle> R)" by (metis handleE'_nothrow_lhs handleE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_throw (\<lambda>_. True) L \<Longrightarrow> no_throw (\<lambda>_. True) (L <handle> R)
theory Trace_No_Throw

lemma handleE_nothrow_rhs:
  "\<lbrakk> \<And>x. no_throw \<top> (R x) \<rbrakk> \<Longrightarrow> no_throw \<top> (L <handle> R)" by (metis no_throw_handleE_simple)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. no_throw (\<lambda>_. True) (R x)) \<Longrightarrow> no_throw (\<lambda>_. True) (L <handle> R)
theory Trace_No_Throw

lemma no_throw_Inr:
  "\<lbrakk> x \<in> mres (A s); no_throw P A; P s \<rbrakk> \<Longrightarrow> \<exists>y. fst x = Inr y" by (fastforce simp: no_throw_def' split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> mres (A s); no_throw P A; P s\<rbrakk> \<Longrightarrow> \<exists>y. fst x = Inr y
theory Trace_No_Throw

lemma mres_parallel:
  "x \<in> mres (parallel f g s) \<Longrightarrow> x \<in> mres (f s) \<and> x \<in> mres (g s)" unfolding parallel_def2 mres_def apply (clarsimp simp: image_def) apply (auto intro!: bexI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> mres (parallel f g s) \<Longrightarrow> x \<in> mres (f s) \<and> x \<in> mres (g s) proof (prove)
goal (1 subgoal):
 1. x \<in> Result -` snd ` {(xs, rv). \<exists>ys zs. (ys, rv) \<in> f s \<and> (zs, rv) \<in> g s \<and> list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs \<and> xs = map2 (\<lambda>(idn, s) (idn', uu_). (if idn = Env then idn' else idn, s)) ys zs} \<Longrightarrow> x \<in> Result -` snd ` f s \<and> x \<in> Result -` snd ` g s proof (prove)
goal (1 subgoal):
 1. \<And>ys zs. \<lbrakk>(ys, Result x) \<in> f s; (zs, Result x) \<in> g s; list_all2 (\<lambda>y z. (fst y = Env \<or> fst z = Env) \<and> snd y = snd z) ys zs\<rbrakk> \<Longrightarrow> (\<exists>xa\<in>f s. Result x = snd xa) \<and> (\<exists>xa\<in>g s. Result x = snd xa) proof (prove)
goal:
No subgoals!
theory Trace_No_Throw

lemma no_throw_parallel:
  "\<lbrakk> no_throw P f \<or> no_throw Q g \<rbrakk> \<Longrightarrow> no_throw (P and Q) (parallel f g)" unfolding no_throw_def' apply (auto dest!: mres_parallel) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_throw P f \<or> no_throw Q g \<Longrightarrow> no_throw (P and Q) (parallel f g) proof (prove)
goal (1 subgoal):
 1. (\<forall>s. P s \<longrightarrow> (\<forall>(r, t)\<in>mres (f s). \<exists>x. r = Inr x)) \<or> (\<forall>s. Q s \<longrightarrow> (\<forall>(r, t)\<in>mres (g s). \<exists>x. r = Inr x)) \<Longrightarrow> \<forall>s. (P and Q) s \<longrightarrow> (\<forall>(r, t)\<in>mres (parallel f g s). \<exists>x. r = Inr x) proof (prove)
goal:
No subgoals!
theory Trace_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 Trace_Empty_Fail

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

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

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

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

lemma empty_fail_not_snd:
  "\<lbrakk> \<not> failed (m s); empty_fail m \<rbrakk> \<Longrightarrow> \<exists>v. v \<in> mres (m s)" by (fastforce simp: empty_fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> failed (m s); empty_fail m\<rbrakk> \<Longrightarrow> \<exists>v. v \<in> mres (m s)
theory Trace_Empty_Fail

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

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

lemma empty_fail_bindD1:
  "empty_fail (a >>= b) \<Longrightarrow> empty_fail a" unfolding empty_fail_def bind_def apply (erule all_reg[rotated]) by (force simp: split_def mres_def vimage_def failed_def split: tmres.splits)

(* 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. mres (\<Union>(xs, y)\<in>a s. case_tmres {(xs, Failed)} {(xs, Incomplete)} (\<lambda>(rv, s). (\<lambda>(a, y). (a @ xs, y)) ` b rv s) y) = {} \<longrightarrow> failed (\<Union>(xs, y)\<in>a s. case_tmres {(xs, Failed)} {(xs, Incomplete)} (\<lambda>(rv, s). (\<lambda>(a, y). (a @ xs, y)) ` b rv s) y) \<Longrightarrow> \<forall>s. mres (a s) = {} \<longrightarrow> failed (a s) proof (prove)
goal (1 subgoal):
 1. \<forall>x. (mres (\<Union>(xs, y)\<in>a x. case_tmres {(xs, Failed)} {(xs, Incomplete)} (\<lambda>(rv, s). (\<lambda>(a, y). (a @ xs, y)) ` b rv s) y) = {} \<longrightarrow> failed (\<Union>(xs, y)\<in>a x. case_tmres {(xs, Failed)} {(xs, Incomplete)} (\<lambda>(rv, s). (\<lambda>(a, y). (a @ xs, y)) ` b rv s) y)) \<longrightarrow> mres (a x) = {} \<longrightarrow> failed (a x)
theory Trace_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 Trace_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 Trace_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 Trace_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 Trace_Empty_Fail

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

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

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

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

lemma empty_fail_gets[empty_fail_term]:
  "empty_fail (gets f)" by (simp add: empty_fail_def simpler_gets_def mres_def vimage_def)

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

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

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

lemma mres_bind_empty:
  "mres ((f >>= g) s) = {}
   \<Longrightarrow> mres (f s) = {} \<or> (\<forall>res\<in>mres (f s). mres (g (fst res) (snd res)) = {})" apply (clarsimp simp: bind_def mres_def split_def) apply (clarsimp simp: image_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mres ((f >>= g) s) = {} \<Longrightarrow> mres (f s) = {} \<or> (\<forall>res\<in>mres (f s). mres (g (fst res) (snd res)) = {}) proof (prove)
goal (1 subgoal):
 1. \<And>a b aa. \<lbrakk>Result -` snd ` (\<Union>x\<in>f s. case snd x of Failed \<Rightarrow> {(fst x, Failed)} | Incomplete \<Rightarrow> {(fst x, Incomplete)} | Result p \<Rightarrow> (\<lambda>xa. (fst xa @ fst x, snd xa)) ` g (fst p) (snd p)) = {}; Result -` snd ` f s \<noteq> {}; (aa, Result (a, b)) \<in> f s\<rbrakk> \<Longrightarrow> Result -` snd ` g a b = {} proof (prove)
goal (1 subgoal):
 1. \<And>a b aa ab ba ac ad bc ae. \<lbrakk>\<forall>a b y. (\<forall>x\<in>f s. y \<noteq> (case snd x of Failed \<Rightarrow> {(fst x, Failed)} | Incomplete \<Rightarrow> {(fst x, Incomplete)} | Result p \<Rightarrow> (\<lambda>xa. (fst xa @ fst x, snd xa)) ` g (fst p) (snd p))) \<or> (\<forall>x\<in>y. Result (a, b) \<noteq> snd x); (aa, Result (a, b)) \<in> f s; (ac, Result (ab, ba)) \<in> f s; (ae, Result (ad, bc)) \<in> g a b\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Trace_Empty_Fail

lemma bind_failedI1:
  "failed (f s) \<Longrightarrow> failed ((f >>= g) s)" by (force simp: bind_def vimage_def failed_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. failed (f s) \<Longrightarrow> failed ((f >>= g) s)
theory Trace_Empty_Fail

lemma bind_failedI2:
  "\<lbrakk>\<forall>res\<in>mres (f s). failed (g (fst res) (snd res)); mres (f s) \<noteq> {}\<rbrakk>
   \<Longrightarrow> failed ((f >>= g) s)" by (force simp: bind_def mres_def image_def split_def failed_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>res\<in>mres (f s). failed (g (fst res) (snd res)); mres (f s) \<noteq> {}\<rbrakk> \<Longrightarrow> failed ((f >>= g) s)