kings-crown/FVELER_Isabelle huggingface dataset:
theory Lib

lemma hd_map: "ls \<noteq> [] \<Longrightarrow> hd (map f ls) = f (hd ls)" by (cases ls) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ls \<noteq> [] \<Longrightarrow> hd (map f ls) = f (hd ls)
theory Lib

lemma tl_map: "tl (map f ls) = map f (tl ls)" by (cases ls) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tl (map f ls) = map f (tl ls)
theory Lib

lemma not_NilE:
  "\<lbrakk> xs \<noteq> []; \<And>x xs'. xs = x # xs' \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" by (cases xs) auto

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

lemma map_upt_unfold:
  assumes ab: "a < b"
  shows   "map f [a ..< b] = f a # map f [Suc a ..< b]" using assms upt_conv_Cons by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map f [a..<b] = f a # map f [Suc a..<b] proof (prove)
using this:
a < b
?i < ?j \<Longrightarrow> [?i..<?j] = ?i # [Suc ?i..<?j]

goal (1 subgoal):
 1. map f [a..<b] = f a # map f [Suc a..<b]
theory Lib

lemma tl_nat_list_simp:
  "tl [a..<b] = [a + 1 ..<b]" by (induct b, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tl [a..<b] = [a + 1..<b]
theory Lib

lemma image_Collect2:
  "case_prod f ` {x. P (fst x) (snd x)} = {f x y |x y. P x y}" by (subst image_Collect) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>(x, y). f x y) ` {x. P (fst x) (snd x)} = {f x y |x y. P x y}
theory Lib

lemma image_id':
  "id ` Y = Y" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. id ` Y = Y
theory Lib

lemma image_invert:
  assumes r: "f \<circ> g = id"
  and     g: "B = g ` A"
  shows  "A = f ` B" by (simp add: g image_comp r)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A = f ` B
theory Lib

lemma Collect_image_fun_cong:
  assumes rl: "\<And>a. P a \<Longrightarrow> f a = g a"
  shows   "{f x | x. P x} = {g x | x. P x}" using rl by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {f x |x. P x} = {g x |x. P x} proof (prove)
using this:
P ?a \<Longrightarrow> f ?a = g ?a

goal (1 subgoal):
 1. {f x |x. P x} = {g x |x. P x}
theory Lib

lemma inj_on_take:
  shows "inj_on (take n) {x. drop n x = k}" proof (rule inj_onI) fix x y assume xv: "x \<in> {x. drop n x = k}"
    and yv: "y \<in> {x. drop n x = k}"
    and tk: "take n x = take n y" from xv have "take n x @ k = x" using append_take_drop_id mem_Collect_eq by auto moreover from yv tk have "take n x @ k = y" using append_take_drop_id mem_Collect_eq by auto ultimately show "x = y" by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj_on (take n) {x. drop n x = k} proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> {x. drop n x = k}; y \<in> {x. drop n x = k}; take n x = take n y\<rbrakk> \<Longrightarrow> x = y proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> {x. drop n x = k}; y \<in> {x. drop n x = k}; take n x = take n y\<rbrakk> \<Longrightarrow> x = y proof (state)
this:
x \<in> {x. drop n x = k}
y \<in> {x. drop n x = k}
take n x = take n y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> {x. drop n x = k}; y \<in> {x. drop n x = k}; take n x = take n y\<rbrakk> \<Longrightarrow> x = y proof (chain)
picking this:
x \<in> {x. drop n x = k} proof (prove)
using this:
x \<in> {x. drop n x = k}

goal (1 subgoal):
 1. take n x @ k = x proof (prove)
using this:
x \<in> {x. drop n x = k}
take ?n ?xs @ drop ?n ?xs = ?xs
(?a \<in> Collect ?P) = ?P ?a

goal (1 subgoal):
 1. take n x @ k = x proof (state)
this:
take n x @ k = x

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> {x. drop n x = k}; y \<in> {x. drop n x = k}; take n x = take n y\<rbrakk> \<Longrightarrow> x = y proof (state)
this:
take n x @ k = x

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> {x. drop n x = k}; y \<in> {x. drop n x = k}; take n x = take n y\<rbrakk> \<Longrightarrow> x = y proof (chain)
picking this:
y \<in> {x. drop n x = k}
take n x = take n y proof (prove)
using this:
y \<in> {x. drop n x = k}
take n x = take n y

goal (1 subgoal):
 1. take n x @ k = y proof (prove)
using this:
y \<in> {x. drop n x = k}
take n x = take n y
take ?n ?xs @ drop ?n ?xs = ?xs
(?a \<in> Collect ?P) = ?P ?a

goal (1 subgoal):
 1. take n x @ k = y proof (state)
this:
take n x @ k = y

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> {x. drop n x = k}; y \<in> {x. drop n x = k}; take n x = take n y\<rbrakk> \<Longrightarrow> x = y proof (chain)
picking this:
take n x @ k = x
take n x @ k = y proof (prove)
using this:
take n x @ k = x
take n x @ k = y

goal (1 subgoal):
 1. x = y proof (state)
this:
x = y

goal:
No subgoals!
theory Lib

lemma foldr_upd_app:
  assumes xin: "x \<in> set as"
  shows "(foldr (\<lambda>p ps. ps (p \<mapsto> f p)) as g) x = Some (f x)"
  (is "(?f as g) x = Some (f x)") using xin proof (induct as arbitrary: x) case Nil thus ?case by simp next case (Cons a as) from Cons.prems show ?case by (subst foldr.simps) (auto intro: Cons.hyps) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g x = Some (f x) proof (prove)
using this:
x \<in> set as

goal (1 subgoal):
 1. foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g x = Some (f x) proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> set [] \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) [] g x = Some (f x)
 2. \<And>a as x. \<lbrakk>\<And>x. x \<in> set as \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g x = Some (f x); x \<in> set (a # as)\<rbrakk> \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g x = Some (f x) proof (state)
this:
x \<in> set []

goal (2 subgoals):
 1. \<And>x. x \<in> set [] \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) [] g x = Some (f x)
 2. \<And>a as x. \<lbrakk>\<And>x. x \<in> set as \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g x = Some (f x); x \<in> set (a # as)\<rbrakk> \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g x = Some (f x) proof (prove)
using this:
x \<in> set []

goal (1 subgoal):
 1. foldr (\<lambda>p ps. ps(p \<mapsto> f p)) [] g x = Some (f x) proof (state)
this:
foldr (\<lambda>p ps. ps(p \<mapsto> f p)) [] g x = Some (f x)

goal (1 subgoal):
 1. \<And>a as x. \<lbrakk>\<And>x. x \<in> set as \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g x = Some (f x); x \<in> set (a # as)\<rbrakk> \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g x = Some (f x) proof (state)
goal (1 subgoal):
 1. \<And>a as x. \<lbrakk>\<And>x. x \<in> set as \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g x = Some (f x); x \<in> set (a # as)\<rbrakk> \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g x = Some (f x) proof (state)
this:
?x \<in> set as \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g ?x = Some (f ?x)
x \<in> set (a # as)

goal (1 subgoal):
 1. \<And>a as x. \<lbrakk>\<And>x. x \<in> set as \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g x = Some (f x); x \<in> set (a # as)\<rbrakk> \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g x = Some (f x) proof (chain)
picking this:
x \<in> set (a # as) proof (prove)
using this:
x \<in> set (a # as)

goal (1 subgoal):
 1. foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g x = Some (f x) proof (state)
this:
foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g x = Some (f x)

goal:
No subgoals!
theory Lib

lemma foldr_upd_app_other:
  assumes xin: "x \<notin> set as"
  shows "(foldr (\<lambda>p ps. ps (p \<mapsto> f p)) as g) x = g x"
  (is "(?f as g) x = g x") using xin proof (induct as arbitrary: x) case Nil thus ?case by simp next case (Cons a as) from Cons.prems show ?case by (subst foldr.simps) (auto intro: Cons.hyps) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g x = g x proof (prove)
using this:
x \<notin> set as

goal (1 subgoal):
 1. foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g x = g x proof (state)
goal (2 subgoals):
 1. \<And>x. x \<notin> set [] \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) [] g x = g x
 2. \<And>a as x. \<lbrakk>\<And>x. x \<notin> set as \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g x = g x; x \<notin> set (a # as)\<rbrakk> \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g x = g x proof (state)
this:
x \<notin> set []

goal (2 subgoals):
 1. \<And>x. x \<notin> set [] \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) [] g x = g x
 2. \<And>a as x. \<lbrakk>\<And>x. x \<notin> set as \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g x = g x; x \<notin> set (a # as)\<rbrakk> \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g x = g x proof (prove)
using this:
x \<notin> set []

goal (1 subgoal):
 1. foldr (\<lambda>p ps. ps(p \<mapsto> f p)) [] g x = g x proof (state)
this:
foldr (\<lambda>p ps. ps(p \<mapsto> f p)) [] g x = g x

goal (1 subgoal):
 1. \<And>a as x. \<lbrakk>\<And>x. x \<notin> set as \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g x = g x; x \<notin> set (a # as)\<rbrakk> \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g x = g x proof (state)
goal (1 subgoal):
 1. \<And>a as x. \<lbrakk>\<And>x. x \<notin> set as \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g x = g x; x \<notin> set (a # as)\<rbrakk> \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g x = g x proof (state)
this:
?x \<notin> set as \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g ?x = g ?x
x \<notin> set (a # as)

goal (1 subgoal):
 1. \<And>a as x. \<lbrakk>\<And>x. x \<notin> set as \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g x = g x; x \<notin> set (a # as)\<rbrakk> \<Longrightarrow> foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g x = g x proof (chain)
picking this:
x \<notin> set (a # as) proof (prove)
using this:
x \<notin> set (a # as)

goal (1 subgoal):
 1. foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g x = g x proof (state)
this:
foldr (\<lambda>p ps. ps(p \<mapsto> f p)) (a # as) g x = g x

goal:
No subgoals!
theory Lib

lemma foldr_upd_app_if:
  "foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g = (\<lambda>x. if x \<in> set as then Some (f x) else g x)" by (auto simp: foldr_upd_app foldr_upd_app_other)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>p ps. ps(p \<mapsto> f p)) as g = (\<lambda>x. if x \<in> set as then Some (f x) else g x)
theory Lib

lemma foldl_fun_upd_value:
  "\<And>Y. foldl (\<lambda>f p. f(p := X p)) Y e p = (if p\<in>set e then X p else Y p)" by (induct e) simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>Y. foldl (\<lambda>f p. f(p := X p)) Y e p = (if p \<in> set e then X p else Y p)
theory Lib

lemma foldr_fun_upd_value:
  "\<And>Y. foldr (\<lambda>p f. f(p := X p)) e Y p = (if p\<in>set e then X p else Y p)" by (induct e) simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>Y. foldr (\<lambda>p f. f(p := X p)) e Y p = (if p \<in> set e then X p else Y p)
theory Lib

lemma foldl_fun_upd_eq_foldr:
  "!!m. foldl (\<lambda>f p. f(p := g p)) m xs = foldr (\<lambda>p f. f(p := g p)) xs m" by (rule ext) (simp add: foldl_fun_upd_value foldr_fun_upd_value)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>m. foldl (\<lambda>f p. f(p := g p)) m xs = foldr (\<lambda>p f. f(p := g p)) xs m
theory Lib

lemma Cons_eq_neq:
  "\<lbrakk> y = x; x # xs \<noteq> y # ys \<rbrakk> \<Longrightarrow> xs \<noteq> ys" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y = x; x # xs \<noteq> y # ys\<rbrakk> \<Longrightarrow> xs \<noteq> ys
theory Lib

lemma map_upt_append:
  assumes lt: "x \<le> y"
  and    lt2: "a \<le> x"
  shows   "map f [a ..< y] = map f [a ..< x] @ map f [x ..< y]" proof (subst map_append [symmetric], rule arg_cong [where f = "map f"]) from lt obtain k where ky: "x + k = y" by (auto simp: le_iff_add) thus "[a ..< y] = [a ..< x] @ [x ..< y]" using lt2 by (auto intro: upt_add_eq_append) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map f [a..<y] = map f [a..<x] @ map f [x..<y] proof (state)
goal (1 subgoal):
 1. [a..<y] = [a..<x] @ [x..<y] proof (chain)
picking this:
x \<le> y proof (prove)
using this:
x \<le> y

goal (1 subgoal):
 1. (\<And>k. x + k = y \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
x + k = y

goal (1 subgoal):
 1. [a..<y] = [a..<x] @ [x..<y] proof (prove)
using this:
x + k = y

goal (1 subgoal):
 1. [a..<y] = [a..<x] @ [x..<y] proof (prove)
using this:
x + k = y
a \<le> x

goal (1 subgoal):
 1. [a..<y] = [a..<x] @ [x..<y] proof (state)
this:
[a..<y] = [a..<x] @ [x..<y]

goal:
No subgoals!
theory Lib

lemma min_of_mono':
  assumes "(f a \<le> f c) = (a \<le> c)"
  shows "min (f a) (f c) = f (min a c)" unfolding min_def by (subst if_distrib [where f = f, symmetric], rule arg_cong [where f = f], rule if_cong [OF _ refl refl]) fact+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. min (f a) (f c) = f (min a c) proof (prove)
goal (1 subgoal):
 1. (if f a \<le> f c then f a else f c) = f (if a \<le> c then a else c)
theory Lib

lemma take_map_Not:
  "(take n (map Not xs) = take n xs) = (n = 0 \<or> xs = [])" by (cases n; simp) (cases xs; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (take n (map Not xs) = take n xs) = (n = 0 \<or> xs = [])
theory Lib

lemma trancl_trancl:
  "(R\<^sup>+)\<^sup>+ = R\<^sup>+" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (R\<^sup>+)\<^sup>+ = R\<^sup>+
theory Lib

lemma rtrancl_eq_reflc_trans:
  assumes trans: "trans X"
  shows "rtrancl X = X \<union> Id" by (simp only: rtrancl_trancl_reflcl trancl_id[OF trans])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. X\<^sup>* = X\<^sup>=
theory Lib

lemma rtrancl_id:
  assumes refl: "Id \<subseteq> X"
  assumes trans: "trans X"
  shows "rtrancl X = X" using refl rtrancl_eq_reflc_trans[OF trans] by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. X\<^sup>* = X proof (prove)
using this:
Id \<subseteq> X
X\<^sup>* = X\<^sup>=

goal (1 subgoal):
 1. X\<^sup>* = X
theory Lib

lemma rtranclp_eq_reflcp_transp:
  assumes trans: "transp X"
  shows "rtranclp X = (\<lambda>x y. X x y \<or> x = y)" by (simp add: Enum.rtranclp_rtrancl_eq fun_eq_iff
                rtrancl_eq_reflc_trans trans[unfolded transp_trans])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. X\<^sup>*\<^sup>* = (\<lambda>x y. X x y \<or> x = y)
theory Lib

lemma rtranclp_id:
  shows "reflp X \<Longrightarrow> transp X \<Longrightarrow> rtranclp X = X" apply (simp add: rtranclp_eq_reflcp_transp) apply (auto simp: fun_eq_iff elim: reflpD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reflp X; transp X\<rbrakk> \<Longrightarrow> X\<^sup>*\<^sup>* = X proof (prove)
goal (1 subgoal):
 1. \<lbrakk>reflp X; transp X\<rbrakk> \<Longrightarrow> (\<lambda>x y. X x y \<or> x = y) = X proof (prove)
goal:
No subgoals!
theory Lib

lemma if_1_0_0:
  "((if P then 1 else 0) = (0 :: ('a :: zero_neq_one))) = (\<not> P)" by (simp split: if_split)

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

lemma neq_Nil_lengthI:
  "Suc 0 \<le> length xs \<Longrightarrow> xs \<noteq> []" by (cases xs, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Suc 0 \<le> length xs \<Longrightarrow> xs \<noteq> []
theory Lib

lemma in_singleton:
  "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_set:
 "x \<in> set [a] \<Longrightarrow> x = a" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> set [a] \<Longrightarrow> x = a
theory Lib

lemma take_drop_eqI:
  assumes t: "take n xs = take n ys"
  assumes d: "drop n xs = drop n ys"
  shows "xs = ys" proof - have "xs = take n xs @ drop n xs" by simp with t d have "xs = take n ys @ drop n ys" by simp moreover have "ys = take n ys @ drop n ys" by simp ultimately show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xs = ys proof (state)
goal (1 subgoal):
 1. xs = ys proof (prove)
goal (1 subgoal):
 1. xs = take n xs @ drop n xs proof (state)
this:
xs = take n xs @ drop n xs

goal (1 subgoal):
 1. xs = ys proof (chain)
picking this:
take n xs = take n ys
drop n xs = drop n ys
xs = take n xs @ drop n xs proof (prove)
using this:
take n xs = take n ys
drop n xs = drop n ys
xs = take n xs @ drop n xs

goal (1 subgoal):
 1. xs = take n ys @ drop n ys proof (state)
this:
xs = take n ys @ drop n ys

goal (1 subgoal):
 1. xs = ys proof (state)
this:
xs = take n ys @ drop n ys

goal (1 subgoal):
 1. xs = ys proof (prove)
goal (1 subgoal):
 1. ys = take n ys @ drop n ys proof (state)
this:
ys = take n ys @ drop n ys

goal (1 subgoal):
 1. xs = ys proof (chain)
picking this:
xs = take n ys @ drop n ys
ys = take n ys @ drop n ys proof (prove)
using this:
xs = take n ys @ drop n ys
ys = take n ys @ drop n ys

goal (1 subgoal):
 1. xs = ys proof (state)
this:
xs = ys

goal:
No subgoals!
theory Lib

lemma append_len2:
  "zs = xs @ ys \<Longrightarrow> length xs = length zs - length ys" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zs = xs @ ys \<Longrightarrow> length xs = length zs - length ys
theory Lib

lemma not_in_domIff:"f x = None = (x \<notin> dom f)" by blast

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

lemma not_in_domD:
  "x \<notin> dom f \<Longrightarrow> f x = None" by (simp add:not_in_domIff)

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

lemma graph_of_Some_update:
  "graph_of (f (p \<mapsto> v)) = (graph_of f - {p} \<times> UNIV) \<union> {(p,v)}" by (auto simp: graph_of_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. graph_of (f(p \<mapsto> v)) = graph_of f - {p} \<times> UNIV \<union> {(p, v)}
theory Lib

lemma graph_of_restrict_map:
  "graph_of (m |` S) \<subseteq> graph_of m" by (simp add: graph_of_def restrict_map_def subset_iff)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. graph_of (m |` S) \<subseteq> graph_of m
theory Lib

lemma graph_ofD:
  "(x,y) \<in> graph_of f \<Longrightarrow> f x = Some y" by (simp add: graph_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, y) \<in> graph_of f \<Longrightarrow> f x = Some y
theory Lib

lemma graph_ofI:
  "m x = Some y \<Longrightarrow> (x, y) \<in> graph_of m" by (simp add: graph_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. m x = Some y \<Longrightarrow> (x, y) \<in> graph_of m
theory Lib

lemma graph_of_empty :
  "graph_of Map.empty = {}" by (simp add: graph_of_def)

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

lemma graph_of_SomeD:
  "\<lbrakk> graph_of f \<subseteq> graph_of g; f x = Some y \<rbrakk> \<Longrightarrow> g x = Some y" unfolding graph_of_def by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>graph_of f \<subseteq> graph_of g; f x = Some y\<rbrakk> \<Longrightarrow> g x = Some y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{(x, y). f x = Some y} \<subseteq> {(x, y). g x = Some y}; f x = Some y\<rbrakk> \<Longrightarrow> g x = Some y
theory Lib

lemma graph_of_comp:
  "\<lbrakk> g x = y; f y = Some z \<rbrakk> \<Longrightarrow> (x,z) \<in> graph_of (f \<circ> g)" by (auto simp: graph_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>g x = y; f y = Some z\<rbrakk> \<Longrightarrow> (x, z) \<in> graph_of (f \<circ> g)
theory Lib

lemma in_set_zip_refl :
  "(x,y) \<in> set (zip xs xs) = (y = x \<and> x \<in> set xs)" by (induct xs) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((x, y) \<in> set (zip xs xs)) = (y = x \<and> x \<in> set xs)
theory Lib

lemma map_conv_upd:
  "m v = None \<Longrightarrow> m o (f (x := v)) = (m o f) (x := None)" by (rule ext) (clarsimp simp: o_def)

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

lemma case_sum_triv [simp]:
    "(case x of Inl x \<Rightarrow> Inl x | Inr x \<Rightarrow> Inr x) = x" by (clarsimp split: sum.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case x of Inl x \<Rightarrow> Inl x | Inr x \<Rightarrow> Inr x) = x
theory Lib

lemma set_eq_UNIV: "({a. P a} = UNIV) = (\<forall>a. P a)" by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ({a. P a} = UNIV) = (\<forall>a. P a)
theory Lib

lemma allE2:
  "\<lbrakk>\<forall>x y. P x y; P x y \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" by blast

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

lemma my_BallE: "\<lbrakk> \<forall>x \<in> A. P x; y \<in> A; P y \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q" by (simp add: Ball_def)

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

lemma unit_Inl_or_Inr [simp]:
  "\<And>a. (a \<noteq> Inl ()) = (a = Inr ())"
  "\<And>a. (a \<noteq> Inr ()) = (a = Inl ())" by (case_tac a; clarsimp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>a. (a \<noteq> Inl ()) = (a = Inr ())) &&& (\<And>a. (a \<noteq> Inr ()) = (a = Inl ()))
theory Lib

lemma disjE_L: "\<lbrakk> a \<or> b; a \<Longrightarrow> R; \<lbrakk> \<not> a; b \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" by blast

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

lemma disjE_R: "\<lbrakk> a \<or> b; \<lbrakk> \<not> b; a \<rbrakk> \<Longrightarrow> R; \<lbrakk> b \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" by blast

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

lemma int_max_thms:
    "(a :: int) \<le> max a b"
    "(b :: int) \<le> max a b" by (auto simp: max_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<le> max a b &&& b \<le> max a b
theory Lib

lemma sgn_sgn_nonneg [simp]:
  "sgn (a :: int) * sgn a \<noteq> -1" by (clarsimp simp: sgn_if)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sgn a * sgn a \<noteq> - 1
theory Lib

lemma inj_inj_on:
  "inj f \<Longrightarrow> inj_on f A" by (metis injD inj_onI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj f \<Longrightarrow> inj_on f A
theory Lib

lemma pre_post_ex:
  "\<lbrakk>\<exists>x. P x; \<And>x. P x \<Longrightarrow> Q x\<rbrakk> \<Longrightarrow> \<exists>x. Q x" by auto

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

lemma all_conj_increase:
  "(( \<forall>x. P x) \<and> Q) = (\<forall>x. P x \<and> Q)"
  "(R \<and> (\<forall>x. S x)) = (\<forall>x. R \<and> S x)" by simp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((\<forall>x. P x) \<and> Q) = (\<forall>x. P x \<and> Q) &&& (R \<and> (\<forall>x. S x)) = (\<forall>x. R \<and> S x)