kings-crown/FVELER_Isabelle huggingface dataset:
theory Nondet_Reader_Option

lemma gets_the_Some:
  "gets_the (\<lambda>_. Some x) = return x" by (simp add: gets_the_def assert_opt_Some)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (\<lambda>_. Some x) = return x
theory Nondet_Reader_Option

lemma gets_the_oapply2_comp:
  "gets_the (oapply2 y x \<circ> f) = gets_map (swp f y) x" by (clarsimp simp: gets_map_def gets_the_def o_def gets_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the (oapply2 y x \<circ> f) = gets_map (swp f y) x
theory Nondet_Reader_Option

lemma gets_the_conv:
  "(gets_the B s) = (case B s of Some r' \<Rightarrow> ({(r', s)}, False) | _ \<Rightarrow> ({}, True))" by (auto simp: gets_the_def gets_def get_def bind_def return_def fail_def assert_opt_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. gets_the B s = (case B s of None \<Rightarrow> ({}, True) | Some r' \<Rightarrow> ({(r', s)}, False))
theory Rule_By_Method

lemma "Q \<longrightarrow> Q \<and> Q" by (rule baz)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Q \<longrightarrow> Q \<and> Q
theory Rule_By_Method

lemma assumes A shows A by (silly_rule A rule: \<open>A\<close>)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A
theory Rule_By_Method

lemma assumes A[simp]: "A" shows A apply (match conclusion in P for P \<Rightarrow>
       \<open>rule [[@\<open>erule thin_rl, rule revcut_rl[of "P"], simp\<close>]]\<close>) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A proof (prove)
goal:
No subgoals!
theory Eisbach_Methods

lemma protect_start: "(protect_concl P \<Longrightarrow> protect_false) \<Longrightarrow> P" by (simp add: protect_concl_def protect_false_def) (rule ccontr)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (protect_concl P \<Longrightarrow> protect_false) \<Longrightarrow> P
theory Eisbach_Methods

lemma protect_end: "protect_concl P \<Longrightarrow> P \<Longrightarrow> protect_false" by (simp add: protect_concl_def protect_false_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>protect_concl P; P\<rbrakk> \<Longrightarrow> protect_false
theory Eisbach_Methods

lemma atomize_conj' [atomize]: "(A &^& B) == Trueprop (A & B)" by (simp add: conjunction'_def, rule atomize_conj)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (A &^& B) \<equiv> A \<and> B
theory Eisbach_Methods

lemma context_conjunction'I:
  "PROP P \<Longrightarrow> (PROP P \<Longrightarrow> PROP Q) \<Longrightarrow> PROP P &^& PROP Q" apply (simp add: conjunction'_def) apply (rule conjunctionI) apply assumption apply (erule meta_mp) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PROP P; PROP P \<Longrightarrow> PROP Q\<rbrakk> \<Longrightarrow> PROP P &^& PROP Q proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PROP P; PROP P \<Longrightarrow> PROP Q\<rbrakk> \<Longrightarrow> PROP P &&& PROP Q proof (prove)
goal (2 subgoals):
 1. \<lbrakk>PROP P; PROP P \<Longrightarrow> PROP Q\<rbrakk> \<Longrightarrow> PROP P
 2. \<lbrakk>PROP P; PROP P \<Longrightarrow> PROP Q\<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. PROP P \<Longrightarrow> PROP P proof (prove)
goal:
No subgoals!
theory Eisbach_Methods

lemma conjunction'I:
  "PROP P \<Longrightarrow> PROP Q \<Longrightarrow> PROP P &^& PROP Q" by (rule context_conjunction'I; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PROP P; PROP Q\<rbrakk> \<Longrightarrow> PROP P &^& PROP Q
theory Eisbach_Methods

lemma protectE: "PROP protect P \<Longrightarrow> (PROP P \<Longrightarrow> PROP R) \<Longrightarrow> PROP R" by (simp add: protect_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>protect PROP P; PROP P \<Longrightarrow> PROP R\<rbrakk> \<Longrightarrow> PROP R
theory Eisbach_Methods

lemma context_conjunction'I_protected:
  assumes P: "PROP P"
  assumes PQ: "PROP protect (PROP P) \<Longrightarrow> PROP Q"
  shows
  "PROP P &^& PROP Q" apply (simp add: conjunction'_def) apply (rule P) apply (rule PQ) apply (simp add: protect_def) by (rule P)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. PROP P &^& PROP Q proof (prove)
goal (1 subgoal):
 1. PROP P &&& PROP Q proof (prove)
goal (1 subgoal):
 1. PROP Q proof (prove)
goal (1 subgoal):
 1. protect PROP P proof (prove)
goal (1 subgoal):
 1. PROP P
theory Eisbach_Methods

lemma conjunction'_sym: "PROP P &^& PROP Q \<Longrightarrow> PROP Q &^& PROP P" apply (simp add: conjunction'_def) apply (frule conjunctionD1) apply (drule conjunctionD2) apply (rule conjunctionI) by assumption+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. PROP P &^& PROP Q \<Longrightarrow> PROP Q &^& PROP P proof (prove)
goal (1 subgoal):
 1. PROP P &&& PROP Q \<Longrightarrow> PROP Q &&& PROP P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PROP P &&& PROP Q; PROP P\<rbrakk> \<Longrightarrow> PROP Q &&& PROP P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PROP P; PROP Q\<rbrakk> \<Longrightarrow> PROP Q &&& PROP P proof (prove)
goal (2 subgoals):
 1. \<lbrakk>PROP P; PROP Q\<rbrakk> \<Longrightarrow> PROP Q
 2. \<lbrakk>PROP P; PROP Q\<rbrakk> \<Longrightarrow> PROP P
theory Eisbach_Methods

lemma assumes A[simp]:A shows A by (rule [[@\<open>prove_prop A\<close>]])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A
theory Eisbach_Methods

lemma assumes A[simp]:A shows A by (ruleP False | ruleP A)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A
theory Eisbach_Methods

lemma assumes A:A shows A by (ruleP "\<And>P. P \<Longrightarrow> P \<Longrightarrow> P", rule A, rule A)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A
theory Eisbach_Methods

lemma bool_protectD:
  "bool_protect P \<Longrightarrow> P" unfolding bool_protect_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bool_protect P \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow> P
theory Eisbach_Methods

lemma bool_protectI:
  "P \<Longrightarrow> bool_protect P" unfolding bool_protect_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow> bool_protect P proof (prove)
goal (1 subgoal):
 1. P \<Longrightarrow> P
theory Extract_Conjunct

lemma focus_example:
  "focus C [right B, left D, left E, right A] \<longleftrightarrow> A \<and> ((B \<and> C) \<and> D) \<and> E" unfolding focus_defs by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. focus C [right B, left D, left E, right A] = (A \<and> ((B \<and> C) \<and> D) \<and> E) proof (prove)
goal (1 subgoal):
 1. focus_conj C [B, D, E, A] = (A \<and> ((B \<and> C) \<and> D) \<and> E)
theory Extract_Conjunct

lemma focus_top_iff: "E \<and> focus P [] \<longleftrightarrow> E \<and> P" unfolding focus_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (E \<and> focus P []) = (E \<and> P) proof (prove)
goal (1 subgoal):
 1. (E \<and> focus_conj P []) = (E \<and> P)
theory Extract_Conjunct

lemma focus_left_iff: "E \<and> focus L (left R # P) \<longleftrightarrow> E \<and> focus (L \<and> R) P" unfolding focus_defs by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (E \<and> focus L (left R # P)) = (E \<and> focus (L \<and> R) P) proof (prove)
goal (1 subgoal):
 1. (E \<and> focus_conj L (R # P)) = (E \<and> focus_conj (L \<and> R) P)
theory Extract_Conjunct

lemma focus_right_iff: "E \<and> focus R (right L # P) \<longleftrightarrow> E \<and> focus (L \<and> R) P" unfolding focus_defs using conj_commute by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (E \<and> focus R (right L # P)) = (E \<and> focus (L \<and> R) P) proof (prove)
goal (1 subgoal):
 1. (E \<and> focus_conj R (L # P)) = (E \<and> focus_conj (L \<and> R) P) proof (prove)
using this:
(?P \<and> ?Q) = (?Q \<and> ?P)

goal (1 subgoal):
 1. (E \<and> focus_conj R (L # P)) = (E \<and> focus_conj (L \<and> R) P)
theory Extract_Conjunct

lemma extract_focus_iff: "focus C (tag t S # P) \<longleftrightarrow> (C \<and> focus S P)" unfolding focus_defs by (induct P arbitrary: S) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. focus C (tag t S # P) = (C \<and> focus S P) proof (prove)
goal (1 subgoal):
 1. focus_conj C (S # P) = (C \<and> focus_conj S P)
theory Extract_Conjunct

lemma "\<lbrakk> A; B; \<lbrakk> A; B; D; E \<rbrakk> \<Longrightarrow> C; D; E \<rbrakk> \<Longrightarrow> A \<and> ((B \<and> C) \<and> D) \<and> E" apply (lift_conjunct \<open>match conclusion in C \<Rightarrow> \<open>-\<close>\<close>)
  \<comment> \<open>@{term C} as been moved to the front of the conclusion.\<close> apply (match conclusion in \<open>C \<and> A \<and> (B \<and> D) \<and> E\<close> \<Rightarrow> \<open>-\<close>) oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B; \<lbrakk>A; B; D; E\<rbrakk> \<Longrightarrow> C; D; E\<rbrakk> \<Longrightarrow> A \<and> ((B \<and> C) \<and> D) \<and> E proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B; \<lbrakk>A; B; D; E\<rbrakk> \<Longrightarrow> C; D; E\<rbrakk> \<Longrightarrow> C \<and> A \<and> (B \<and> D) \<and> E proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B; \<lbrakk>A; B; D; E\<rbrakk> \<Longrightarrow> C; D; E\<rbrakk> \<Longrightarrow> C \<and> A \<and> (B \<and> D) \<and> E
theory Extract_Conjunct

lemma "\<lbrakk> A; B; \<lbrakk> A; B; D; E \<rbrakk> \<Longrightarrow> C; D; E \<rbrakk> \<Longrightarrow> A \<and> ((B \<and> C) \<and> D) \<and> E" apply (extract_conjunct \<open>match conclusion in C \<Rightarrow> \<open>-\<close>\<close>)
  \<comment> \<open>@{method extract_conjunct} gives us the matched conjunct @{term C} as a separate subgoal.\<close> apply (match conclusion in C \<Rightarrow> \<open>-\<close>) apply blast
  \<comment> \<open>The other subgoal contains the remaining conjuncts untouched.\<close> apply (match conclusion in \<open>A \<and> (B \<and> D) \<and> E\<close> \<Rightarrow> \<open>-\<close>) oops

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B; \<lbrakk>A; B; D; E\<rbrakk> \<Longrightarrow> C; D; E\<rbrakk> \<Longrightarrow> A \<and> ((B \<and> C) \<and> D) \<and> E proof (prove)
goal (2 subgoals):
 1. \<lbrakk>A; B; \<lbrakk>A; B; D; E\<rbrakk> \<Longrightarrow> C; D; E\<rbrakk> \<Longrightarrow> C
 2. \<lbrakk>A; B; \<lbrakk>A; B; D; E\<rbrakk> \<Longrightarrow> C; D; E\<rbrakk> \<Longrightarrow> A \<and> (B \<and> D) \<and> E proof (prove)
goal (2 subgoals):
 1. \<lbrakk>A; B; \<lbrakk>A; B; D; E\<rbrakk> \<Longrightarrow> C; D; E\<rbrakk> \<Longrightarrow> C
 2. \<lbrakk>A; B; \<lbrakk>A; B; D; E\<rbrakk> \<Longrightarrow> C; D; E\<rbrakk> \<Longrightarrow> A \<and> (B \<and> D) \<and> E proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B; \<lbrakk>A; B; D; E\<rbrakk> \<Longrightarrow> C; D; E\<rbrakk> \<Longrightarrow> A \<and> (B \<and> D) \<and> E proof (prove)
goal (1 subgoal):
 1. \<lbrakk>A; B; \<lbrakk>A; B; D; E\<rbrakk> \<Longrightarrow> C; D; E\<rbrakk> \<Longrightarrow> A \<and> (B \<and> D) \<and> E
theory Extract_Conjunct

lemma "\<lbrakk> A; B; \<lbrakk> A; B; D; E \<rbrakk> \<Longrightarrow> C; D; E \<rbrakk> \<Longrightarrow> A \<and> ((B \<and> C) \<and> D) \<and> E" apply (apply_conjunct \<open>match conclusion in C \<Rightarrow> \<open>match premises in H: _ \<Rightarrow> \<open>rule H\<close>\<close>\<close>)
  \<comment> \<open>We get four subgoals from applying the given method to the matched conjunct @{term C}.\<close> apply (match premises in H: A \<Rightarrow> \<open>rule H\<close>) apply (match premises in H: B \<Rightarrow> \<open>rule H\<close>) apply (match premises in H: D \<Rightarrow> \<open>rule H\<close>) apply (match premises in H: E \<Rightarrow> \<open>rule H\<close>)
  \<comment> \<open>The last subgoal contains the remaining conjuncts untouched.\<close> apply (match conclusion in \<open>A \<and> (B \<and> D) \<and> E\<close> \<Rightarrow> \<open>-\<close>) oops

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

lemma "eval_bool_test_locale.z > 150" by eval_bool

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 150 < eval_bool_test_locale.z
theory None_Top_Bot

lemma none_top_simps[simp]:
  "none_top f None = top"
  "none_top f (Some x) = f x" by (auto simp: none_top_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_top f None = top &&& none_top f (Some x) = f x
theory None_Top_Bot

lemma none_top_split:
  "P (none_top f opt) = ((opt = None \<longrightarrow> P top) \<and> (\<forall>x. opt = Some x \<longrightarrow> P (f x)))" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P (none_top f opt) = ((opt = None \<longrightarrow> P top) \<and> (\<forall>x. opt = Some x \<longrightarrow> P (f x)))
theory None_Top_Bot

lemma none_top_split_asm:
  "P (none_top f opt) = (\<not> (opt = None \<and> \<not> P top \<or> (\<exists>x. opt = Some x \<and> \<not> P (f x))))" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P (none_top f opt) = (\<not> (opt = None \<and> \<not> P top \<or> (\<exists>x. opt = Some x \<and> \<not> P (f x))))
theory None_Top_Bot

lemma none_top_if:
  "none_top f opt = (if opt = None then top else f (the opt))" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_top f opt = (if opt = None then top else f (the opt))
theory None_Top_Bot

lemma none_top_Inf:
  "none_top f opt = (Inf {f x |x. opt = Some x} :: 'a :: complete_lattice)" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_top f opt = Inf {f x |x. opt = Some x}
theory None_Top_Bot

lemma none_top_top[simp]:
  "none_top top = top" by (rule ext) (simp split: none_top_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_top top = top
theory None_Top_Bot

lemma none_top_bool_all:
  "none_top f opt = (\<forall>x. opt = Some x \<longrightarrow> f x)" by (auto simp: none_top_Inf)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_top f opt = (\<forall>x. opt = Some x \<longrightarrow> f x)
theory None_Top_Bot

lemma none_top_bool_cases:
  "none_top f opt = (opt = None \<or> (\<exists>x. opt = Some x \<and> f x))" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_top f opt = (opt = None \<or> (\<exists>x. opt = Some x \<and> f x))
theory None_Top_Bot

lemma none_top_boolD:
  "none_top f opt \<Longrightarrow> opt = None \<or> (\<exists>x. opt = Some x \<and> f x)" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_top f opt \<Longrightarrow> opt = None \<or> (\<exists>x. opt = Some x \<and> f x)
theory None_Top_Bot

lemma none_top_boolE:
  "\<lbrakk> none_top f opt; opt = None \<Longrightarrow> P; \<And>x. \<lbrakk> opt = Some x; f x \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>none_top f opt; opt = None \<Longrightarrow> P; \<And>x. \<lbrakk>opt = Some x; f x\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory None_Top_Bot

lemma none_top_False_bool_None[simp]:
  "none_top \<bottom> opt = (opt = None)" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_top (\<lambda>_. False) opt = (opt = None)
theory None_Top_Bot

lemma none_top_bot_bool_None[intro!, simp]:
  "none_top bot opt = (opt = None)" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_top bot opt = (opt = None)
theory None_Top_Bot

lemma none_top_True[simp]:
  "none_top \<top> = \<top>" by (rule ext) (simp split: none_top_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_top (\<lambda>_. True) = (\<lambda>_. True)
theory None_Top_Bot

lemma none_top_True_bool[intro!]:
  "none_top \<top> opt" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_top (\<lambda>_. True) opt
theory None_Top_Bot

lemma none_top_fun_all:
  "none_top f opt s = (\<forall>x. opt = Some x \<longrightarrow> f x s)" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_top f opt s = (\<forall>x. opt = Some x \<longrightarrow> f x s)
theory None_Top_Bot

lemma none_top_fun_cases:
  "none_top f opt s = (opt = None \<or> (\<exists>x. opt = Some x \<and> f x s))" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_top f opt s = (opt = None \<or> (\<exists>x. opt = Some x \<and> f x s))
theory None_Top_Bot

lemma none_top_funI:
  "(\<And>x. opt = Some x \<Longrightarrow> f x s) \<Longrightarrow> none_top f opt s" by (simp add: none_top_fun_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. opt = Some x \<Longrightarrow> f x s) \<Longrightarrow> none_top f opt s
theory None_Top_Bot

lemma none_top_funD:
  "none_top f opt s \<Longrightarrow> opt = None \<or> (\<exists>x. opt = Some x \<and> f x s)" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_top f opt s \<Longrightarrow> opt = None \<or> (\<exists>x. opt = Some x \<and> f x s)
theory None_Top_Bot

lemma none_top_funE:
  "\<lbrakk> none_top f opt s; opt = None \<Longrightarrow> P; \<And>x. \<lbrakk> opt = Some x; f x s \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>none_top f opt s; opt = None \<Longrightarrow> P; \<And>x. \<lbrakk>opt = Some x; f x s\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory None_Top_Bot

lemma none_top_False_fun_None[simp]:
  "none_top \<bottom>\<bottom> opt s = (opt = None)" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_top (\<lambda>_ _. False) opt s = (opt = None)
theory None_Top_Bot

lemma none_top_True_True[simp]:
  "none_top \<top>\<top> = \<top>\<top>" by (rule ext) (simp split: none_top_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_top (\<lambda>_ _. True) = (\<lambda>_ _. True)
theory None_Top_Bot

lemma none_top_True_fun[intro!]:
  "none_top \<top>\<top> opt s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_top (\<lambda>_ _. True) opt s
theory None_Top_Bot

lemma none_bot_simps[simp]:
  "none_bot f None = bot"
  "none_bot f (Some x) = f x" by (auto simp: none_bot_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_bot f None = bot &&& none_bot f (Some x) = f x
theory None_Top_Bot

lemma none_bot_split:
  "P (none_bot f opt) = ((opt = None \<longrightarrow> P bot) \<and> (\<forall>x. opt = Some x \<longrightarrow> P (f x)))" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P (none_bot f opt) = ((opt = None \<longrightarrow> P bot) \<and> (\<forall>x. opt = Some x \<longrightarrow> P (f x)))
theory None_Top_Bot

lemma none_bot_split_asm:
  "P (none_bot f opt) = (\<not> (opt = None \<and> \<not> P bot \<or> (\<exists>x. opt = Some x \<and> \<not> P (f x))))" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P (none_bot f opt) = (\<not> (opt = None \<and> \<not> P bot \<or> (\<exists>x. opt = Some x \<and> \<not> P (f x))))
theory None_Top_Bot

lemma none_bot_Sup:
  "none_bot f opt = (Sup {f x |x. opt = Some x} :: 'a :: complete_lattice)" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_bot f opt = Sup {f x |x. opt = Some x}
theory None_Top_Bot

lemma none_bot_if:
  "none_bot f opt = (if opt = None then bot else f (the opt))" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_bot f opt = (if opt = None then bot else f (the opt))
theory None_Top_Bot

lemma none_bot_bot[simp]:
  "none_bot bot = bot" by (rule ext) (simp split: none_bot_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_bot bot = bot
theory None_Top_Bot

lemma none_bot_bool_ex:
  "none_bot f opt = (\<exists>x. opt = Some x \<and> f x)" by (auto simp: none_bot_Sup)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_bot f opt = (\<exists>x. opt = Some x \<and> f x)
theory None_Top_Bot

lemma none_bot_boolI:
  "\<exists>x. opt = Some x \<and> f x \<Longrightarrow> none_bot f opt" by (auto simp: none_bot_bool_ex)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>x. opt = Some x \<and> f x \<Longrightarrow> none_bot f opt
theory None_Top_Bot

lemma none_bot_boolD:
  "none_bot f opt \<Longrightarrow> \<exists>x. opt = Some x \<and> f x" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_bot f opt \<Longrightarrow> \<exists>x. opt = Some x \<and> f x
theory None_Top_Bot

lemma none_bot_boolE:
  "\<lbrakk> none_bot f opt; \<And>x. \<lbrakk> opt = Some x; f x \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>none_bot f opt; \<And>x. \<lbrakk>opt = Some x; f x\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory None_Top_Bot

lemma none_bot_top_bool_neq_None[simp]:
  "none_bot top opt = (opt \<noteq> None)" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_bot top opt = (opt \<noteq> None)
theory None_Top_Bot

lemma none_bot_True_bool_neq_None[simp]:
  "none_bot \<top> opt = (opt \<noteq> None)" by (cases opt) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_bot (\<lambda>_. True) opt = (opt \<noteq> None)
theory None_Top_Bot

lemma none_bot_False_bool[simp]:
  "none_bot \<bottom> = \<bottom>" by (rule ext) (simp split: none_bot_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_bot (\<lambda>_. False) = (\<lambda>_. False)
theory None_Top_Bot

lemma none_bot_False_boolE[dest!]:
  "none_bot \<bottom> opt \<Longrightarrow> False" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. none_bot (\<lambda>_. False) opt \<Longrightarrow> False