kings-crown/FVELER_Isabelle huggingface dataset:
theory Lib

lemma modify_map_None:
  "m x = None \<Longrightarrow> modify_map m x f = m" by (rule ext) (simp add: modify_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m x = None \<Longrightarrow> modify_map m x f = m
theory Lib

lemma modify_map_ndom :
  "x \<notin> dom m \<Longrightarrow> modify_map m x f = m" by (rule modify_map_None) clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<notin> dom m \<Longrightarrow> modify_map m x f = m
theory Lib

lemma modify_map_app:
  "(modify_map m p f) q = (if p = q then map_option f (m p) else m q)" unfolding modify_map_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify_map m p f q = (if p = q then map_option f (m p) else m q) proof (prove)
goal (1 subgoal):
 1. (m(p := map_option f (m p))) q = (if p = q then map_option f (m p) else m q)
theory Lib

lemma modify_map_apply:
  "m p = Some x \<Longrightarrow> modify_map m p f = m (p \<mapsto> f x)" by (simp add: modify_map_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m p = Some x \<Longrightarrow> modify_map m p f = m(p \<mapsto> f x)
theory Lib

lemma modify_map_com:
  assumes com: "\<And>x. f (g x) = g (f x)"
  shows "modify_map (modify_map m x g) y f = modify_map (modify_map m y f) x g" using assms by (auto simp: modify_map_def map_option_case split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify_map (modify_map m x g) y f = modify_map (modify_map m y f) x g proof (prove)
using this:
f (g ?x) = g (f ?x)

goal (1 subgoal):
 1. modify_map (modify_map m x g) y f = modify_map (modify_map m y f) x g
theory Lib

lemma modify_map_comp:
  "modify_map m x (f o g) = modify_map (modify_map m x g) x f" by (rule ext) (simp add: modify_map_def option.map_comp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify_map m x (f \<circ> g) = modify_map (modify_map m x g) x f
theory Lib

lemma modify_map_exists_eq:
  "(\<exists>cte. modify_map m p' f p= Some cte) = (\<exists>cte. m p = Some cte)" by (auto simp: modify_map_def split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<exists>cte. modify_map m p' f p = Some cte) = (\<exists>cte. m p = Some cte)
theory Lib

lemma modify_map_other:
  "p \<noteq> q \<Longrightarrow> (modify_map m p f) q = (m q)" by (simp add: modify_map_app)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p \<noteq> q \<Longrightarrow> modify_map m p f q = m q
theory Lib

lemma modify_map_same:
  "modify_map m p f p = map_option f (m p)" by (simp add: modify_map_app)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify_map m p f p = map_option f (m p)
theory Lib

lemma next_update_is_modify:
  "\<lbrakk> m p = Some cte'; cte = f cte' \<rbrakk> \<Longrightarrow> (m(p \<mapsto> cte)) = modify_map m p f" unfolding modify_map_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some cte'; cte = f cte'\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) = modify_map m p f proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m p = Some cte'; cte = f cte'\<rbrakk> \<Longrightarrow> m(p \<mapsto> cte) = m(p := map_option f (m p))
theory Lib

lemma nat_power_minus_less:
  "a < 2 ^ (x - n) \<Longrightarrow> (a :: nat) < 2 ^ x" by (erule order_less_le_trans) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a < 2 ^ (x - n) \<Longrightarrow> a < 2 ^ x
theory Lib

lemma neg_rtranclI:
  "\<lbrakk> x \<noteq> y; (x, y) \<notin> R\<^sup>+ \<rbrakk> \<Longrightarrow> (x, y) \<notin> R\<^sup>*" by (meson rtranclD)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; (x, y) \<notin> R\<^sup>+\<rbrakk> \<Longrightarrow> (x, y) \<notin> R\<^sup>*
theory Lib

lemma neg_rtrancl_into_trancl:
  "\<not> (x, y) \<in> R\<^sup>* \<Longrightarrow> \<not> (x, y) \<in> R\<^sup>+" by (erule contrapos_nn, erule trancl_into_rtrancl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, y) \<notin> R\<^sup>* \<Longrightarrow> (x, y) \<notin> R\<^sup>+
theory Lib

lemma set_neqI:
  "\<lbrakk> x \<in> S; x \<notin> S' \<rbrakk> \<Longrightarrow> S \<noteq> S'" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> S; x \<notin> S'\<rbrakk> \<Longrightarrow> S \<noteq> S'
theory Lib

lemma set_pair_UN:
  "{x. P x} = \<Union> ((\<lambda>xa. {xa} \<times> {xb. P (xa, xb)}) ` {xa. \<exists>xb. P (xa, xb)})" by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {x. P x} = (\<Union>xa\<in>{xa. \<exists>xb. P (xa, xb)}. {xa} \<times> {xb. P (xa, xb)})
theory Lib

lemma singleton_elemD: "S = {x} \<Longrightarrow> x \<in> S" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S = {x} \<Longrightarrow> x \<in> S
theory Lib

lemma singleton_eqD: "A = {x} \<Longrightarrow> x \<in> A" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A = {x} \<Longrightarrow> x \<in> A
theory Lib

lemma ball_ran_fun_updI:
  "\<lbrakk> \<forall>v \<in> ran m. P v; \<forall>v. y = Some v \<longrightarrow> P v \<rbrakk> \<Longrightarrow> \<forall>v \<in> ran (m (x := y)). P v" by (auto simp add: ran_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>v\<in>ran m. P v; \<forall>v. y = Some v \<longrightarrow> P v\<rbrakk> \<Longrightarrow> \<forall>v\<in>ran (m(x := y)). P v
theory Lib

lemma cart_helper:
  "({} = {x} \<times> S) = (S = {})" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ({} = {x} \<times> S) = (S = {})
theory Lib

lemma disjCI2: "(\<not> P \<Longrightarrow> Q) \<Longrightarrow> P \<or> Q" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<not> P \<Longrightarrow> Q) \<Longrightarrow> P \<or> Q
theory Lib

lemma insert_UNIV :
  "insert x UNIV = UNIV" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. insert x UNIV = UNIV
theory Lib

lemma not_singletonE:
  "\<lbrakk> \<forall>p. S \<noteq> {p}; S \<noteq> {}; \<And>p p'. \<lbrakk> p \<noteq> p'; p \<in> S; p' \<in> S \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p. S \<noteq> {p}; S \<noteq> {}; \<And>p p'. \<lbrakk>p \<noteq> p'; p \<in> S; p' \<in> S\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Lib

lemma not_singleton_oneE:
  "\<lbrakk> \<forall>p. S \<noteq> {p}; p \<in> S; \<And>p'. \<lbrakk> p \<noteq> p'; p' \<in> S \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" using not_singletonE by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p. S \<noteq> {p}; p \<in> S; \<And>p'. \<lbrakk>p \<noteq> p'; p' \<in> S\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R proof (prove)
using this:
\<lbrakk>\<forall>p. ?S \<noteq> {p}; ?S \<noteq> {}; \<And>p p'. \<lbrakk>p \<noteq> p'; p \<in> ?S; p' \<in> ?S\<rbrakk> \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R

goal (1 subgoal):
 1. \<lbrakk>\<forall>p. S \<noteq> {p}; p \<in> S; \<And>p'. \<lbrakk>p \<noteq> p'; p' \<in> S\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Lib

lemma ball_ran_modify_map_eq:
  "\<lbrakk> \<forall>v. m x = Some v \<longrightarrow> P (f v) = P v \<rbrakk>
  \<Longrightarrow> (\<forall>v \<in> ran (modify_map m x f). P v) = (\<forall>v \<in> ran m. P v)" by (auto simp: modify_map_def ball_ran_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>v. m x = Some v \<longrightarrow> P (f v) = P v \<Longrightarrow> (\<forall>v\<in>ran (modify_map m x f). P v) = (\<forall>v\<in>ran m. P v)
theory Lib

lemma eq_singleton_redux:
  "\<lbrakk> S = {x} \<rbrakk> \<Longrightarrow> x \<in> S" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. S = {x} \<Longrightarrow> x \<in> S
theory Lib

lemma if_eq_elem_helperE:
  "\<lbrakk> x \<in> (if P then S else S');  \<lbrakk> P;   x \<in> S  \<rbrakk> \<Longrightarrow> a = b;  \<lbrakk> \<not> P; x \<in> S' \<rbrakk> \<Longrightarrow> a = c \<rbrakk>
  \<Longrightarrow> a = (if P then b else c)" by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> (if P then S else S'); \<lbrakk>P; x \<in> S\<rbrakk> \<Longrightarrow> a = b; \<lbrakk>\<not> P; x \<in> S'\<rbrakk> \<Longrightarrow> a = c\<rbrakk> \<Longrightarrow> a = (if P then b else c)
theory Lib

lemma modify_map_K_D:
  "modify_map m p (\<lambda>x. y) p' = Some v \<Longrightarrow> (m (p \<mapsto> y)) p' = Some v" by (simp add: modify_map_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify_map m p (\<lambda>x. y) p' = Some v \<Longrightarrow> (m(p \<mapsto> y)) p' = Some v
theory Lib

lemma tranclE2:
  assumes trancl: "(a, b) \<in> r\<^sup>+"
  and       base: "(a, b) \<in> r \<Longrightarrow> P"
  and       step: "\<And>c. \<lbrakk>(a, c) \<in> r; (c, b) \<in> r\<^sup>+\<rbrakk> \<Longrightarrow> P"
  shows "P" using trancl base step proof - note rl = converse_trancl_induct [where P = "\<lambda>x. x = a \<longrightarrow> P"] from trancl have "a = a \<longrightarrow> P" by (rule rl, (iprover intro: base step)+) thus ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P proof (prove)
using this:
(a, b) \<in> r\<^sup>+
(a, b) \<in> r \<Longrightarrow> P
\<lbrakk>(a, ?c) \<in> r; (?c, b) \<in> r\<^sup>+\<rbrakk> \<Longrightarrow> P

goal (1 subgoal):
 1. P proof (state)
goal (1 subgoal):
 1. \<lbrakk>(a, b) \<in> r\<^sup>+; (a, b) \<in> r \<Longrightarrow> P; \<And>c. \<lbrakk>(a, c) \<in> r; (c, b) \<in> r\<^sup>+\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (state)
this:
\<lbrakk>(?a, ?b) \<in> ?r\<^sup>+; \<And>y. (y, ?b) \<in> ?r \<Longrightarrow> y = a \<longrightarrow> P; \<And>y z. \<lbrakk>(y, z) \<in> ?r; (z, ?b) \<in> ?r\<^sup>+; z = a \<longrightarrow> P\<rbrakk> \<Longrightarrow> y = a \<longrightarrow> P\<rbrakk> \<Longrightarrow> ?a = a \<longrightarrow> P

goal (1 subgoal):
 1. \<lbrakk>(a, b) \<in> r\<^sup>+; (a, b) \<in> r \<Longrightarrow> P; \<And>c. \<lbrakk>(a, c) \<in> r; (c, b) \<in> r\<^sup>+\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (chain)
picking this:
(a, b) \<in> r\<^sup>+ proof (prove)
using this:
(a, b) \<in> r\<^sup>+

goal (1 subgoal):
 1. a = a \<longrightarrow> P proof (state)
this:
a = a \<longrightarrow> P

goal (1 subgoal):
 1. \<lbrakk>(a, b) \<in> r\<^sup>+; (a, b) \<in> r \<Longrightarrow> P; \<And>c. \<lbrakk>(a, c) \<in> r; (c, b) \<in> r\<^sup>+\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
using this:
a = a \<longrightarrow> P

goal (1 subgoal):
 1. P proof (state)
this:
P

goal:
No subgoals!
theory Lib

lemma weak_imp_cong:
  "\<lbrakk> P = R; Q = S \<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) = (R \<longrightarrow> S)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P = R; Q = S\<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) = (R \<longrightarrow> S)
theory Lib

lemma Collect_Diff_restrict_simp:
  "T - {x \<in> T. Q x} = T - {x. Q x}" by (auto intro: Collect_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. T - {x \<in> T. Q x} = T - {x. Q x}
theory Lib

lemma Collect_Int_pred_eq:
  "{x \<in> S. P x} \<inter> {x \<in> T. P x} = {x \<in> (S \<inter> T). P x}" by (simp add: Collect_conj_eq [symmetric] conj_comms)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {x \<in> S. P x} \<inter> {x \<in> T. P x} = {x \<in> S \<inter> T. P x}
theory Lib

lemma Collect_restrict_predR:
  "{x. P x} \<inter> T = {} \<Longrightarrow> {x. P x} \<inter> {x \<in> T. Q x} = {}" by (fastforce simp: disjoint_iff_not_equal)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {x. P x} \<inter> T = {} \<Longrightarrow> {x. P x} \<inter> {x \<in> T. Q x} = {}
theory Lib

lemma ballEI:
  "\<lbrakk> \<forall>x \<in> S. Q x; \<And>x. \<lbrakk> x \<in> S; Q x \<rbrakk> \<Longrightarrow> P x \<rbrakk> \<Longrightarrow> \<forall>x \<in> S. P x" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>S. Q x; \<And>x. \<lbrakk>x \<in> S; Q x\<rbrakk> \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> \<forall>x\<in>S. P x
theory Lib

lemma dom_if_None:
  "dom (\<lambda>x. if P x then None else f x) = dom f - {x. P x}" by (simp add: dom_def) fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (\<lambda>x. if P x then None else f x) = dom f - {x. P x}
theory Lib

lemma restrict_map_Some_iff:
  "((m |` S) x = Some y) = (m x = Some y \<and> x \<in> S)" by (cases "x \<in> S", simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((m |` S) x = Some y) = (m x = Some y \<and> x \<in> S)
theory Lib

lemma context_case_bools:
  "\<lbrakk> \<And>v. P v \<Longrightarrow> R v; \<lbrakk> \<not> P v; \<And>v. P v \<Longrightarrow> R v \<rbrakk> \<Longrightarrow> R v \<rbrakk> \<Longrightarrow> R v" by (cases "P v", simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>v. P v \<Longrightarrow> R v; \<lbrakk>\<not> P v; \<And>v. P v \<Longrightarrow> R v\<rbrakk> \<Longrightarrow> R v\<rbrakk> \<Longrightarrow> R v
theory Lib

lemma inj_on_fun_upd_strongerI:
  "\<lbrakk>inj_on f A; y \<notin> f ` (A - {x})\<rbrakk> \<Longrightarrow> inj_on (f(x := y)) A" by (fastforce simp: inj_on_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on f A; y \<notin> f ` (A - {x})\<rbrakk> \<Longrightarrow> inj_on (f(x := y)) A
theory Lib

lemma less_handy_casesE:
  "\<lbrakk> m < n; m = 0 \<Longrightarrow> R; \<And>m' n'. \<lbrakk> n = Suc n'; m = Suc m'; m < n \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" by (case_tac n; simp) (case_tac m; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m < n; m = 0 \<Longrightarrow> R; \<And>m' n'. \<lbrakk>n = Suc n'; m = Suc m'; m < n\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Lib

lemma subset_drop_Diff_strg:
  "(A \<subseteq> C) \<longrightarrow> (A - B \<subseteq> C)" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A \<subseteq> C \<longrightarrow> A - B \<subseteq> C
theory Lib

lemma inj_case_bool:
  "inj (case_bool a b) = (a \<noteq> b)" by (auto dest: inj_onD[where x=True and y=False] intro: inj_onI split: bool.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj (case_bool a b) = (a \<noteq> b)
theory Lib

lemma foldl_fun_upd:
  "foldl (\<lambda>s r. s (r := g r)) f rs = (\<lambda>x. if x \<in> set rs then g x else f x)" by (induct rs arbitrary: f) (auto simp: fun_eq_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldl (\<lambda>s r. s(r := g r)) f rs = (\<lambda>x. if x \<in> set rs then g x else f x)
theory Lib

lemma if_Const_helper:
  "If P (Con x) (Con y) = Con (If P x y)" by (simp split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if P then Con x else Con y) = Con (if P then x else y)
theory Lib

lemma expand_restrict_map_eq:
  "(m |` S = m' |` S) = (\<forall>x. x \<in> S \<longrightarrow> m x = m' x)" by (simp add: fun_eq_iff restrict_map_def split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (m |` S = m' |` S) = (\<forall>x. x \<in> S \<longrightarrow> m x = m' x)
theory Lib

lemma disj_imp_rhs:
  "(P \<Longrightarrow> Q) \<Longrightarrow> (P \<or> Q) = Q" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> Q) \<Longrightarrow> (P \<or> Q) = Q
theory Lib

lemma remove1_filter:
  "distinct xs \<Longrightarrow> remove1 x xs = filter (\<lambda>y. x \<noteq> y) xs" by (induct xs) (auto intro!: filter_True [symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct xs \<Longrightarrow> remove1 x xs = filter ((\<noteq>) x) xs
theory Lib

lemma Int_Union_empty:
  "(\<And>x. x \<in> S \<Longrightarrow> A \<inter> P x = {}) \<Longrightarrow> A \<inter> (\<Union>x \<in> S. P x) = {}" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> S \<Longrightarrow> A \<inter> P x = {}) \<Longrightarrow> A \<inter> \<Union> (P ` S) = {}
theory Lib

lemma UN_Int_empty:
  "(\<And>x. x \<in> S \<Longrightarrow> P x \<inter> T = {}) \<Longrightarrow> (\<Union>x \<in> S. P x) \<inter> T = {}" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x \<in> S \<Longrightarrow> P x \<inter> T = {}) \<Longrightarrow> \<Union> (P ` S) \<inter> T = {}
theory Lib

lemma disjointI:
  "\<lbrakk>\<And>x y. \<lbrakk> x \<in> A; y \<in> B \<rbrakk> \<Longrightarrow> x \<noteq> y \<rbrakk> \<Longrightarrow> A \<inter> B = {}" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x y. \<lbrakk>x \<in> A; y \<in> B\<rbrakk> \<Longrightarrow> x \<noteq> y) \<Longrightarrow> A \<inter> B = {}
theory Lib

lemma UN_disjointI:
  assumes rl: "\<And>x y. \<lbrakk> x \<in> A; y \<in> B \<rbrakk> \<Longrightarrow> P x \<inter> Q y = {}"
  shows "(\<Union>x \<in> A. P x) \<inter> (\<Union>x \<in> B. Q x) = {}" by (auto dest: rl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<Union> (P ` A) \<inter> \<Union> (Q ` B) = {}
theory Lib

lemma UN_set_member:
  assumes sub: "A \<subseteq> (\<Union>x \<in> S. P x)"
  and      nz: "A \<noteq> {}"
  shows    "\<exists>x \<in> S. P x \<inter> A \<noteq> {}" proof - from nz obtain z where zA: "z \<in> A" by fastforce with sub obtain x where "x \<in> S" and "z \<in> P x" by auto hence "P x \<inter> A \<noteq> {}" using zA by auto thus ?thesis using sub nz by auto qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>S. P x \<inter> A \<noteq> {} proof (state)
goal (1 subgoal):
 1. \<exists>x\<in>S. P x \<inter> A \<noteq> {} proof (chain)
picking this:
A \<noteq> {} proof (prove)
using this:
A \<noteq> {}

goal (1 subgoal):
 1. (\<And>z. z \<in> A \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
z \<in> A

goal (1 subgoal):
 1. \<exists>x\<in>S. P x \<inter> A \<noteq> {} proof (chain)
picking this:
A \<subseteq> \<Union> (P ` S)
z \<in> A proof (prove)
using this:
A \<subseteq> \<Union> (P ` S)
z \<in> A

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>x \<in> S; z \<in> P x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
x \<in> S
z \<in> P x

goal (1 subgoal):
 1. \<exists>x\<in>S. P x \<inter> A \<noteq> {} proof (prove)
using this:
x \<in> S
z \<in> P x

goal (1 subgoal):
 1. P x \<inter> A \<noteq> {} proof (prove)
using this:
x \<in> S
z \<in> P x
z \<in> A

goal (1 subgoal):
 1. P x \<inter> A \<noteq> {} proof (state)
this:
P x \<inter> A \<noteq> {}

goal (1 subgoal):
 1. \<exists>x\<in>S. P x \<inter> A \<noteq> {} proof (prove)
using this:
P x \<inter> A \<noteq> {}

goal (1 subgoal):
 1. \<exists>x\<in>S. P x \<inter> A \<noteq> {} proof (prove)
using this:
P x \<inter> A \<noteq> {}
A \<subseteq> \<Union> (P ` S)
A \<noteq> {}

goal (1 subgoal):
 1. \<exists>x\<in>S. P x \<inter> A \<noteq> {} proof (state)
this:
\<exists>x\<in>S. P x \<inter> A \<noteq> {}

goal:
No subgoals!
theory Lib

lemma append_Cons_cases [consumes 1, case_names pre mid post]:
  "\<lbrakk>(x, y) \<in> set (as @ b # bs);
    (x, y) \<in> set as \<Longrightarrow> R;
    \<lbrakk>(x, y) \<notin> set as; (x, y) \<notin> set bs; (x, y) = b\<rbrakk> \<Longrightarrow> R;
    (x, y) \<in> set bs \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, y) \<in> set (as @ b # bs); (x, y) \<in> set as \<Longrightarrow> R; \<lbrakk>(x, y) \<notin> set as; (x, y) \<notin> set bs; (x, y) = b\<rbrakk> \<Longrightarrow> R; (x, y) \<in> set bs \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Lib

lemma disjoint_subset_neg1:
  "\<lbrakk> B \<inter> C = {}; A \<subseteq> B; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<not> A \<subseteq> C" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B \<inter> C = {}; A \<subseteq> B; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> A \<subseteq> C
theory Lib

lemma disjoint_subset_neg2:
  "\<lbrakk> B \<inter> C = {}; A \<subseteq> C; A \<noteq> {} \<rbrakk> \<Longrightarrow> \<not> A \<subseteq> B" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B \<inter> C = {}; A \<subseteq> C; A \<noteq> {}\<rbrakk> \<Longrightarrow> \<not> A \<subseteq> B
theory Lib

lemma iffE2:
  "\<lbrakk> P = Q; \<lbrakk> P; Q \<rbrakk> \<Longrightarrow> R; \<lbrakk> \<not> P; \<not> Q \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P = Q; \<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R; \<lbrakk>\<not> P; \<not> Q\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R
theory Lib

lemma list_case_If:
  "(case xs of [] \<Rightarrow> P | _ \<Rightarrow> Q) = (if xs = [] then P else Q)" by (rule list.case_eq_if)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case xs of [] \<Rightarrow> P | a # list \<Rightarrow> Q) = (if xs = [] then P else Q)
theory Lib

lemma lifted_if_collapse:
  "(if P then \<top> else f) = (\<lambda>s. \<not>P \<longrightarrow> f s)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if P then \<lambda>_. True else f) = (\<lambda>s. \<not> P \<longrightarrow> f s)
theory Lib

lemma remove1_Nil_in_set:
  "\<lbrakk> remove1 x xs = []; xs \<noteq> [] \<rbrakk> \<Longrightarrow> x \<in> set xs" by (induct xs) (auto split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>remove1 x xs = []; xs \<noteq> []\<rbrakk> \<Longrightarrow> x \<in> set xs
theory Lib

lemma remove1_empty:
  "(remove1 v xs = []) = (xs = [v] \<or> xs = [])" by (cases xs; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (remove1 v xs = []) = (xs = [v] \<or> xs = [])
theory Lib

lemma set_remove1:
  "x \<in> set (remove1 y xs) \<Longrightarrow> x \<in> set xs" by (induct xs) (auto split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> set (remove1 y xs) \<Longrightarrow> x \<in> set xs
theory Lib

lemma disjI2_strg:
  "Q \<longrightarrow> (P \<or> Q)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Q \<longrightarrow> P \<or> Q
theory Lib

lemma if_both_strengthen:
  "P \<and> Q \<longrightarrow> (if G then P else Q)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P \<and> Q \<longrightarrow> (if G then P else Q)
theory Lib

lemma if_both_strengthen2:
  "P s \<and> Q s \<longrightarrow> (if G then P else Q) s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P s \<and> Q s \<longrightarrow> (if G then P else Q) s
theory Lib

lemma if_swap:
  "(if P then Q else R) = (if \<not>P then R else Q)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if P then Q else R) = (if \<not> P then R else Q)
theory Lib

lemma list_cons_rewrite:
  "(\<forall>x xs. L = x # xs \<longrightarrow> P x xs) = (L \<noteq> [] \<longrightarrow> P (hd L) (tl L))" by (auto simp: neq_Nil_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>x xs. L = x # xs \<longrightarrow> P x xs) = (L \<noteq> [] \<longrightarrow> P (hd L) (tl L))
theory Lib

lemma ran_ball_triv:
  "\<And>P m S. \<lbrakk> \<forall>x \<in> (ran S). P x ; m \<in> (ran S) \<rbrakk> \<Longrightarrow> P m" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P m S. \<lbrakk>\<forall>x\<in>ran S. P x; m \<in> ran S\<rbrakk> \<Longrightarrow> P m
theory Lib

lemma singleton_tuple_cartesian:
  "({(a, b)} = S \<times> T) = ({a} = S \<and> {b} = T)"
  "(S \<times> T = {(a, b)}) = ({a} = S \<and> {b} = T)" by blast+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ({(a, b)} = S \<times> T) = ({a} = S \<and> {b} = T) &&& (S \<times> T = {(a, b)}) = ({a} = S \<and> {b} = T)
theory Lib

lemma case_sum_True :
  "(case r of Inl a \<Rightarrow> True | Inr b \<Rightarrow> f b) = (\<forall>b. r = Inr b \<longrightarrow> f b)" by (cases r) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case r of Inl a \<Rightarrow> True | Inr b \<Rightarrow> f b) = (\<forall>b. r = Inr b \<longrightarrow> f b)