kings-crown/FVELER_Isabelle huggingface dataset:
theory Lib

lemma list_case_If2:
  "case_list f g xs = If (xs = []) f (g (hd xs) (tl xs))" by (simp split: list.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case xs of [] \<Rightarrow> f | x # xa \<Rightarrow> g x xa) = (if xs = [] then f else g (hd xs) (tl xs))
theory Lib

lemma length_ineq_not_Nil:
  "length xs > n \<Longrightarrow> xs \<noteq> []"
  "length xs \<ge> n \<Longrightarrow> n \<noteq> 0 \<longrightarrow> xs \<noteq> []"
  "\<not> length xs < n \<Longrightarrow> n \<noteq> 0 \<longrightarrow> xs \<noteq> []"
  "\<not> length xs \<le> n \<Longrightarrow> xs \<noteq> []" by auto

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

lemma numeral_eqs:
  "2 = Suc (Suc 0)"
  "3 = Suc (Suc (Suc 0))"
  "4 = Suc (Suc (Suc (Suc 0)))"
  "5 = Suc (Suc (Suc (Suc (Suc 0))))"
  "6 = Suc (Suc (Suc (Suc (Suc (Suc 0)))))" by simp+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (2 = Suc (Suc 0) &&& 3 = Suc (Suc (Suc 0))) &&& 4 = Suc (Suc (Suc (Suc 0))) &&& 5 = Suc (Suc (Suc (Suc (Suc 0)))) &&& 6 = Suc (Suc (Suc (Suc (Suc (Suc 0)))))
theory Lib

lemma length_takeWhile_ge:
  "length (takeWhile f xs) = n \<Longrightarrow> length xs = n \<or> (length xs > n \<and> \<not> f (xs ! n))" by (induct xs arbitrary: n) (auto split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (takeWhile f xs) = n \<Longrightarrow> length xs = n \<or> n < length xs \<and> \<not> f (xs ! n)
theory Lib

lemma length_takeWhile_le:
  "\<not> f (xs ! n) \<Longrightarrow> length (takeWhile f xs) \<le> n" by (induct xs arbitrary: n; simp) (case_tac n; simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> f (xs ! n) \<Longrightarrow> length (takeWhile f xs) \<le> n
theory Lib

lemma map_fst_filter_zip[simp]:
 "map fst (filter (\<lambda>(_, x). P x) (zip ls (map f ls))) = filter (\<lambda>x. P (f x)) ls" by (induction ls; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map fst (filter (\<lambda>(uu_, x). P x) (zip ls (map f ls))) = filter (\<lambda>x. P (f x)) ls
theory Lib

lemma map_fst_dropWhile_zip[simp]:
 "map fst (dropWhile (\<lambda>(_, x). P x) (zip ls (map f ls))) = dropWhile (\<lambda>x. P (f x)) ls" by (induction ls; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map fst (dropWhile (\<lambda>(uu_, x). P x) (zip ls (map f ls))) = dropWhile (\<lambda>x. P (f x)) ls
theory Lib

lemma map_fst_takeWhile_zip[simp]:
 "map fst (takeWhile (\<lambda>(_, x). P x) (zip ls (map f ls))) = takeWhile (\<lambda>x. P (f x)) ls" by (induction ls; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map fst (takeWhile (\<lambda>(uu_, x). P x) (zip ls (map f ls))) = takeWhile (\<lambda>x. P (f x)) ls
theory Lib

lemma suffix_tl:
  "suffix xs ys \<Longrightarrow> suffix (tl xs) ys" apply (clarsimp simp: suffix_def) apply (metis append.assoc append_Cons append_Nil list.exhaust_sel list.sel(2)) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. suffix xs ys \<Longrightarrow> suffix (tl xs) ys proof (prove)
goal (1 subgoal):
 1. \<And>zs. ys = zs @ xs \<Longrightarrow> \<exists>zsa. zs @ xs = zsa @ tl xs proof (prove)
goal:
No subgoals!
theory Lib

lemma nonempty_proper_suffix_split:
  "\<lbrakk>sfx \<noteq> []; sfx \<noteq> queue; suffix sfx queue\<rbrakk> \<Longrightarrow> (\<exists>xs ys. xs \<noteq> [] \<and> queue = xs @ hd sfx # ys)" apply (clarsimp simp: suffix_def) apply (fastforce simp: neq_Nil_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sfx \<noteq> []; sfx \<noteq> queue; suffix sfx queue\<rbrakk> \<Longrightarrow> \<exists>xs ys. xs \<noteq> [] \<and> queue = xs @ hd sfx # ys proof (prove)
goal (1 subgoal):
 1. \<And>zs. \<lbrakk>sfx \<noteq> []; queue = zs @ sfx; \<forall>xs. xs = [] \<or> (\<forall>ys. zs @ sfx \<noteq> xs @ hd sfx # ys)\<rbrakk> \<Longrightarrow> zs = [] proof (prove)
goal:
No subgoals!
theory Lib

lemma nonempty_proper_suffix_split_distinct:
  "\<lbrakk>sfx \<noteq> []; sfx \<noteq> queue; suffix sfx queue; distinct queue\<rbrakk>
   \<Longrightarrow> \<exists>xs ys. xs \<noteq> [] \<and> queue = xs @ hd sfx # ys \<and> hd queue \<noteq> hd sfx" apply (frule (2) nonempty_proper_suffix_split) apply (cases sfx; fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sfx \<noteq> []; sfx \<noteq> queue; suffix sfx queue; distinct queue\<rbrakk> \<Longrightarrow> \<exists>xs ys. xs \<noteq> [] \<and> queue = xs @ hd sfx # ys \<and> hd queue \<noteq> hd sfx proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sfx \<noteq> []; sfx \<noteq> queue; suffix sfx queue; distinct queue; \<exists>xs ys. xs \<noteq> [] \<and> queue = xs @ hd sfx # ys\<rbrakk> \<Longrightarrow> \<exists>xs ys. xs \<noteq> [] \<and> queue = xs @ hd sfx # ys \<and> hd queue \<noteq> hd sfx proof (prove)
goal:
No subgoals!
theory Lib

lemma hd_drop_conv_nth2:
  "n < length xs \<Longrightarrow> hd (drop n xs) = xs ! n" by (rule hd_drop_conv_nth) clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < length xs \<Longrightarrow> hd (drop n xs) = xs ! n
theory Lib

lemma map_upt_eq_vals_D:
  "\<lbrakk> map f [0 ..< n] = ys; m < length ys \<rbrakk> \<Longrightarrow> f m = ys ! m" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>map f [0..<n] = ys; m < length ys\<rbrakk> \<Longrightarrow> f m = ys ! m
theory Lib

lemma length_le_helper:
  "\<lbrakk> n \<le> length xs; n \<noteq> 0 \<rbrakk> \<Longrightarrow> xs \<noteq> [] \<and> n - 1 \<le> length (tl xs)" by (cases xs, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> length xs; n \<noteq> 0\<rbrakk> \<Longrightarrow> xs \<noteq> [] \<and> n - 1 \<le> length (tl xs)
theory Lib

lemma all_ex_eq_helper:
  "(\<forall>v. (\<exists>v'. v = f v' \<and> P v v') \<longrightarrow> Q v)
      = (\<forall>v'. P (f v') v' \<longrightarrow> Q (f v'))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>v. (\<exists>v'. v = f v' \<and> P v v') \<longrightarrow> Q v) = (\<forall>v'. P (f v') v' \<longrightarrow> Q (f v'))
theory Lib

lemma nat_less_cases':
  "(x::nat) < y \<Longrightarrow> x = y - 1 \<or> x < y - 1" by auto

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

lemma filter_to_shorter_upto:
  "n \<le> m \<Longrightarrow> filter (\<lambda>x. x < n) [0 ..< m] = [0 ..< n]" by (induct m) (auto elim: le_SucE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<le> m \<Longrightarrow> filter (\<lambda>x. x < n) [0..<m] = [0..<n]
theory Lib

lemma in_emptyE: "\<lbrakk> A = {}; x \<in> A \<rbrakk> \<Longrightarrow> P" by blast

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

lemma Ball_emptyI:
  "S = {} \<Longrightarrow> (\<forall>x \<in> S. P x)" by simp

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

lemma allfEI:
  "\<lbrakk> \<forall>x. P x; \<And>x. P (f x) \<Longrightarrow> Q x \<rbrakk> \<Longrightarrow> \<forall>x. Q x" by fastforce

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

lemma cart_singleton_empty2:
  "({x} \<times> S = {}) = (S = {})"
  "({} = S \<times> {e}) = (S = {})" by auto

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

lemma domE :
  "\<lbrakk> x \<in> dom m; \<And>r. \<lbrakk>m x = Some r\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> dom m; \<And>r. m x = Some r \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory Lib

lemma dom_eqD:
  "\<lbrakk> f x = Some v; dom f = S \<rbrakk> \<Longrightarrow> x \<in> S" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f x = Some v; dom f = S\<rbrakk> \<Longrightarrow> x \<in> S
theory Lib

lemma dom_eq_All:
  "dom f = dom f' \<Longrightarrow>
   (\<forall>x. f x = None \<longrightarrow> f' x = None) \<and> (\<forall>x v. f x = Some v \<longrightarrow> (\<exists>v'. f' x = Some v'))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom f = dom f' \<Longrightarrow> (\<forall>x. f x = None \<longrightarrow> f' x = None) \<and> (\<forall>x v. f x = Some v \<longrightarrow> (\<exists>v'. f' x = Some v'))
theory Lib

lemma exception_set_finite1:
  "finite {x. P x} \<Longrightarrow> finite {x. (x = y \<longrightarrow> Q x) \<and> P x}" by (simp add: Collect_conj_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finite {x. P x} \<Longrightarrow> finite {x. (x = y \<longrightarrow> Q x) \<and> P x}
theory Lib

lemma exception_set_finite2:
  "finite {x. P x} \<Longrightarrow> finite {x. x \<noteq> y \<longrightarrow> P x}" by (simp add: imp_conv_disj)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. finite {x. P x} \<Longrightarrow> finite {x. x \<noteq> y \<longrightarrow> P x}
theory Lib

lemma exfEI:
  "\<lbrakk> \<exists>x. P x; \<And>x. P x \<Longrightarrow> Q (f x) \<rbrakk> \<Longrightarrow> \<exists>x. Q x" by fastforce

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

lemma Collect_int_vars:
  "{s. P rv s} \<inter> {s. rv = xf s} = {s. P (xf s) s} \<inter> {s. rv = xf s}" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {s. P rv s} \<inter> {s. rv = xf s} = {s. P (xf s) s} \<inter> {s. rv = xf s}
theory Lib

lemma if_0_1_eq:
  "((if P then 1 else 0) = (case Q of True \<Rightarrow> of_nat 1 | False \<Rightarrow> of_nat 0)) = (P = Q)" by (simp split: if_split bool.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((if P then 1::'a else (0::'a)) = (case Q of True \<Rightarrow> of_nat 1 | False \<Rightarrow> of_nat 0)) = (P = Q)
theory Lib

lemma modify_map_exists_cte :
  "(\<exists>cte. modify_map m p f p' = Some cte) = (\<exists>cte. m p' = Some cte)" by (simp add: modify_map_def)

(* 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 dom_eqI:
  assumes c1: "\<And>x y. P x = Some y \<Longrightarrow> \<exists>y. Q x = Some y"
  and     c2: "\<And>x y. Q x = Some y \<Longrightarrow> \<exists>y. P x = Some y"
  shows "dom P = dom Q" unfolding dom_def by (auto simp: c1 c2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom P = dom Q proof (prove)
goal (1 subgoal):
 1. {a. P a \<noteq> None} = {a. Q a \<noteq> None}
theory Lib

lemma dvd_reduce_multiple:
  fixes k :: nat
  shows "(k dvd k * m + n) = (k dvd n)" by (induct m) (auto simp: add_ac)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (k dvd k * m + n) = (k dvd n)
theory Lib

lemma image_iff2:
  "inj f \<Longrightarrow> f x \<in> f ` S = (x \<in> S)" by (rule inj_image_mem_iff)

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

lemma map_comp_restrict_map_Some_iff:
  "((g \<circ>\<^sub>m (m |` S)) x = Some y) = ((g \<circ>\<^sub>m m) x = Some y \<and> x \<in> S)" by (auto simp add: map_comp_Some_iff restrict_map_Some_iff)

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

lemma range_subsetD:
  fixes a :: "'a :: order"
  shows "\<lbrakk> {a..b} \<subseteq> {c..d}; a \<le> b \<rbrakk> \<Longrightarrow> c \<le> a \<and> b \<le> d" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{a..b} \<subseteq> {c..d}; a \<le> b\<rbrakk> \<Longrightarrow> c \<le> a \<and> b \<le> d
theory Lib

lemma case_option_dom:
  "(case f x of None \<Rightarrow> a | Some v \<Rightarrow> b v) = (if x \<in> dom f then b (the (f x)) else a)" by (auto split: option.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case f x of None \<Rightarrow> a | Some v \<Rightarrow> b v) = (if x \<in> dom f then b (the (f x)) else a)
theory Lib

lemma contrapos_imp:
  "P \<longrightarrow> Q \<Longrightarrow> \<not> Q \<longrightarrow> \<not> P" by clarsimp

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

lemma filter_eq_If:
  "distinct xs \<Longrightarrow> filter (\<lambda>v. v = x) xs = (if x \<in> set xs then [x] else [])" by (induct xs) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct xs \<Longrightarrow> filter (\<lambda>v. v = x) xs = (if x \<in> set xs then [x] else [])
theory Lib

lemma filter_last_equals_butlast:
  "\<lbrakk>distinct q; q \<noteq> []\<rbrakk> \<Longrightarrow> filter ((\<noteq>) (last q)) q = butlast q" apply (induct q rule: length_induct) apply (rename_tac list) apply (case_tac list; simp) apply (fastforce simp: filter_id_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct q; q \<noteq> []\<rbrakk> \<Longrightarrow> filter ((\<noteq>) (last q)) q = butlast q proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<forall>ys. length ys < length xs \<longrightarrow> distinct ys \<longrightarrow> ys \<noteq> [] \<longrightarrow> filter ((\<noteq>) (last ys)) ys = butlast ys; distinct xs; xs \<noteq> []\<rbrakk> \<Longrightarrow> filter ((\<noteq>) (last xs)) xs = butlast xs proof (prove)
goal (1 subgoal):
 1. \<And>list. \<lbrakk>\<forall>ys. length ys < length list \<longrightarrow> distinct ys \<longrightarrow> ys \<noteq> [] \<longrightarrow> filter ((\<noteq>) (last ys)) ys = butlast ys; distinct list; list \<noteq> []\<rbrakk> \<Longrightarrow> filter ((\<noteq>) (last list)) list = butlast list proof (prove)
goal (1 subgoal):
 1. \<And>list a lista. \<lbrakk>\<forall>ys. length ys < Suc (length lista) \<longrightarrow> distinct ys \<longrightarrow> ys \<noteq> [] \<longrightarrow> filter ((\<noteq>) (last ys)) ys = butlast ys; a \<notin> set lista \<and> distinct lista; list = a # lista\<rbrakk> \<Longrightarrow> last lista = a \<longrightarrow> lista \<noteq> [] \<longrightarrow> filter ((\<noteq>) a) lista = a # butlast lista proof (prove)
goal:
No subgoals!
theory Lib

lemma filter_middle_distinct:
  "\<lbrakk>distinct q; q = ys @ t # zs\<rbrakk> \<Longrightarrow> filter ((\<noteq>) t) q = ys @ zs" apply (induct q rule: length_induct) apply (rename_tac list) apply (case_tac list; simp) apply (subst filter_True | fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct q; q = ys @ t # zs\<rbrakk> \<Longrightarrow> filter ((\<noteq>) t) q = ys @ zs proof (prove)
goal (1 subgoal):
 1. \<And>xs. \<lbrakk>\<forall>ysa. length ysa < length xs \<longrightarrow> distinct ysa \<longrightarrow> ysa = ys @ t # zs \<longrightarrow> filter ((\<noteq>) t) ysa = ys @ zs; distinct xs; xs = ys @ t # zs\<rbrakk> \<Longrightarrow> filter ((\<noteq>) t) xs = ys @ zs proof (prove)
goal (1 subgoal):
 1. \<And>list. \<lbrakk>\<forall>ysa. length ysa < length list \<longrightarrow> distinct ysa \<longrightarrow> ysa = ys @ t # zs \<longrightarrow> filter ((\<noteq>) t) ysa = ys @ zs; distinct list; list = ys @ t # zs\<rbrakk> \<Longrightarrow> filter ((\<noteq>) t) list = ys @ zs proof (prove)
goal (1 subgoal):
 1. \<And>list a lista. \<lbrakk>distinct ys \<and> t \<notin> set zs \<and> distinct zs \<and> t \<notin> set ys \<and> set ys \<inter> set zs = {}; a # lista = ys @ t # zs; list = ys @ t # zs\<rbrakk> \<Longrightarrow> filter ((\<noteq>) t) ys @ filter ((\<noteq>) t) zs = ys @ zs proof (prove)
goal:
No subgoals!
theory Lib

lemma (in semigroup_add) foldl_assoc:
shows "foldl (+) (x+y) zs = x + (foldl (+) y zs)" by (induct zs arbitrary: y) (simp_all add:add.assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldl (+) (x + y) zs = x + foldl (+) y zs
theory Lib

lemma (in monoid_add) foldl_absorb0:
shows "x + (foldl (+) 0 zs) = foldl (+) x zs" by (induct zs) (simp_all add:foldl_assoc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x + foldl (+) (0::'a) zs = foldl (+) x zs
theory Lib

lemma foldl_use_filter:
  "\<lbrakk> \<And>v x. \<lbrakk> \<not> g x; x \<in> set xs \<rbrakk> \<Longrightarrow> f v x = v \<rbrakk> \<Longrightarrow> foldl f v xs = foldl f v (filter g xs)" by (induct xs arbitrary: v) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>v x. \<lbrakk>\<not> g x; x \<in> set xs\<rbrakk> \<Longrightarrow> f v x = v) \<Longrightarrow> foldl f v xs = foldl f v (filter g xs)
theory Lib

lemma map_comp_update_lift:
  assumes fv: "f v = Some v'"
  shows "(f \<circ>\<^sub>m (g(ptr \<mapsto> v))) = ((f \<circ>\<^sub>m g)(ptr \<mapsto> v'))" by (simp add: fv map_comp_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f \<circ>\<^sub>m g(ptr \<mapsto> v) = (f \<circ>\<^sub>m g)(ptr \<mapsto> v')
theory Lib

lemma restrict_map_cong:
  assumes sv: "S = S'"
  and     rl: "\<And>p. p \<in> S' \<Longrightarrow> mp p = mp' p"
  shows   "mp |` S = mp' |` S'" using expand_restrict_map_eq rl sv by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mp |` S = mp' |` S' proof (prove)
using this:
(?m |` ?S = ?m' |` ?S) = (\<forall>x. x \<in> ?S \<longrightarrow> ?m x = ?m' x)
?p \<in> S' \<Longrightarrow> mp ?p = mp' ?p
S = S'

goal (1 subgoal):
 1. mp |` S = mp' |` S'
theory Lib

lemma case_option_over_if:
  "case_option P Q (if G then None else Some v)
        = (if G then P else Q v)"
  "case_option P Q (if G then Some v else None)
        = (if G then Q v else P)" by (simp split: if_split)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case if G then None else Some v of None \<Rightarrow> P | Some x \<Rightarrow> Q x) = (if G then P else Q v) &&& (case if G then Some v else None of None \<Rightarrow> P | Some x \<Rightarrow> Q x) = (if G then Q v else P)
theory Lib

lemma take_min_len:
  "take (min (length xs) n) xs = take n xs" by (simp add: min_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. take (min (length xs) n) xs = take n xs
theory Lib

lemma fold_and_false[simp]:
  "\<not>(fold (\<and>) xs False)" apply clarsimp apply (induct xs) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> fold (\<and>) xs False proof (prove)
goal (1 subgoal):
 1. fold (\<and>) xs False \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. fold (\<and>) [] False \<Longrightarrow> False
 2. \<And>a xs. \<lbrakk>fold (\<and>) xs False \<Longrightarrow> False; fold (\<and>) (a # xs) False\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>fold (\<and>) xs False \<Longrightarrow> False; fold (\<and>) (a # xs) False\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Lib

lemma fold_or_true[simp]:
  "fold (\<or>) xs True" by (induct xs, simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fold (\<or>) xs True
theory Lib

lemma fold_or_false:
  "\<not>(fold (\<or>) xs False) \<Longrightarrow> \<forall>i < length xs. \<not>(xs ! i)" apply (induct xs, simp+) apply (case_tac a, simp+) apply (rule allI, case_tac "i = 0", simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> fold (\<or>) xs False \<Longrightarrow> \<forall>i<length xs. \<not> xs ! i proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<not> fold (\<or>) xs False \<Longrightarrow> \<forall>i<length xs. \<not> xs ! i; \<not> fold (\<or>) xs a\<rbrakk> \<Longrightarrow> \<forall>i<Suc (length xs). \<not> (a # xs) ! i proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<forall>i<length xs. \<not> xs ! i; \<not> fold (\<or>) xs False; \<not> a\<rbrakk> \<Longrightarrow> \<forall>i<Suc (length xs). \<not> (False # xs) ! i proof (prove)
goal:
No subgoals!
theory Lib

lemma map_fst_zip_prefix:
  "map fst (zip xs ys) \<le> xs" by (two_induct xs ys)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map fst (zip xs ys) \<le> xs
theory Lib

lemma map_snd_zip_prefix:
  "map snd (zip xs ys) \<le> ys" by (two_induct xs ys)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map snd (zip xs ys) \<le> ys
theory Lib

lemma nth_upt_0 [simp]:
  "i < length xs \<Longrightarrow> [0..<length xs] ! i = i" by simp

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

lemma take_insert_nth:
  "i < length xs\<Longrightarrow> insert (xs ! i) (set (take i xs)) = set (take (Suc i) xs)" by (subst take_Suc_conv_app_nth, assumption, fastforce)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i < length xs \<Longrightarrow> insert (xs ! i) (set (take i xs)) = set (take (Suc i) xs)
theory Lib

lemma zip_take_drop:
  "\<lbrakk>n < length xs; length ys = length xs\<rbrakk> \<Longrightarrow>
    zip xs (take n ys @ a # drop (Suc n) ys) =
    zip (take n xs) (take n ys) @ (xs ! n, a) #  zip (drop (Suc n) xs) (drop (Suc n) ys)" by (subst id_take_nth_drop, assumption, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < length xs; length ys = length xs\<rbrakk> \<Longrightarrow> zip xs (take n ys @ a # drop (Suc n) ys) = zip (take n xs) (take n ys) @ (xs ! n, a) # zip (drop (Suc n) xs) (drop (Suc n) ys)
theory Lib

lemma take_nth_distinct:
  "\<lbrakk>distinct xs; n < length xs; xs ! n \<in> set (take n xs)\<rbrakk> \<Longrightarrow> False" by (fastforce simp: distinct_conv_nth in_set_conv_nth)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; n < length xs; xs ! n \<in> set (take n xs)\<rbrakk> \<Longrightarrow> False
theory Lib

lemma take_drop_append:
  "drop a xs = take b (drop a xs) @ drop (a + b) xs" by (metis append_take_drop_id drop_drop add.commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. drop a xs = take b (drop a xs) @ drop (a + b) xs
theory Lib

lemma drop_take_drop:
  "drop a (take (b + a) xs) @ drop (b + a) xs = drop a xs" by (metis add.commute take_drop take_drop_append)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. drop a (take (b + a) xs) @ drop (b + a) xs = drop a xs
theory Lib

lemma not_prefixI:
  "\<lbrakk> xs \<noteq> ys; length xs = length ys\<rbrakk> \<Longrightarrow> \<not> xs \<le> ys" by (auto elim: prefixE)

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

lemma map_fst_zip':
  "length xs \<le> length ys \<Longrightarrow> map fst (zip xs ys) = xs" by (metis length_map length_zip map_fst_zip_prefix min_absorb1 not_prefixI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs \<le> length ys \<Longrightarrow> map fst (zip xs ys) = xs
theory Lib

lemma zip_take_length:
  "zip xs (take (length xs) ys) = zip xs ys" by (metis length_take length_zip nat_le_linear take_all take_zip)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zip xs (take (length xs) ys) = zip xs ys
theory Lib

lemma zip_singleton:
  "ys \<noteq> [] \<Longrightarrow> zip [a] ys = [(a, ys ! 0)]" by (case_tac ys, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ys \<noteq> [] \<Longrightarrow> zip [a] ys = [(a, ys ! 0)]
theory Lib

lemma zip_append_singleton:
  "\<lbrakk>i = length xs; length xs < length ys\<rbrakk> \<Longrightarrow> zip (xs @ [a]) ys = (zip xs ys) @ [(a,ys ! i)]" by (induct xs; case_tac ys; simp)
     (clarsimp simp: zip_append1 zip_take_length zip_singleton)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i = length xs; length xs < length ys\<rbrakk> \<Longrightarrow> zip (xs @ [a]) ys = zip xs ys @ [(a, ys ! i)]