kings-crown/FVELER_Isabelle huggingface dataset:
theory Word_8

lemma set_strip_insert: "\<lbrakk> x \<in> insert a S; x \<noteq> a \<rbrakk> \<Longrightarrow> x \<in> S" by simp

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

lemma len16: "len_of (x :: 16 itself) = 16" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. len_of x = 16
theory Word_16

lemma word16_and_max_simp:
  \<open>x AND 0xFFFF = x\<close> for x :: \<open>16 word\<close> using word_and_full_mask_simp [of x] by (simp add: numeral_eq_Suc mask_Suc_exp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x AND 65535 = x proof (prove)
using this:
x AND mask LENGTH(16) = x

goal (1 subgoal):
 1. x AND 65535 = x
theory Many_More

lemma nat_less_mult_monoish: "\<lbrakk> a < b; c < (d :: nat) \<rbrakk> \<Longrightarrow> (a + 1) * (c + 1) <= b * d" apply (drule Suc_leI)+ apply (drule(1) mult_le_mono) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a < b; c < d\<rbrakk> \<Longrightarrow> (a + 1) * (c + 1) \<le> b * d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc a \<le> b; Suc c \<le> d\<rbrakk> \<Longrightarrow> (a + 1) * (c + 1) \<le> b * d proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc c \<le> d; Suc a * Suc c \<le> b * d\<rbrakk> \<Longrightarrow> (a + 1) * (c + 1) \<le> b * d proof (prove)
goal:
No subgoals!
theory Many_More

lemma if_and_helper:
  "(If x v v') AND v'' = If x (v AND v'') (v' AND v'')" by (rule if_distrib)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if x then v else v') AND v'' = (if x then v AND v'' else v' AND v'')
theory Many_More

lemma eq_eqI:
  "a = b \<Longrightarrow> (a = x) = (b = x)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a = b \<Longrightarrow> (a = x) = (b = x)
theory Many_More

lemma map2_Cons_2_3:
  "(map2 f xs (y # ys) = (z # zs)) = (\<exists>x xs'. xs = x # xs' \<and> f x y = z \<and> map2 f xs' ys = zs)" by (case_tac xs, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (map2 f xs (y # ys) = z # zs) = (\<exists>x xs'. xs = x # xs' \<and> f x y = z \<and> map2 f xs' ys = zs)
theory Many_More

lemma map2_xor_replicate_False:
  "map2 (\<lambda>x y. x \<longleftrightarrow> \<not> y) xs (replicate n False) = take n xs" apply (induct xs arbitrary: n, simp) apply (case_tac n; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map2 (\<lambda>x y. x = (\<not> y)) xs (replicate n False) = take n xs proof (prove)
goal (1 subgoal):
 1. \<And>a xs n. (\<And>n. map2 (\<lambda>x y. x = (\<not> y)) xs (replicate n False) = take n xs) \<Longrightarrow> map2 (\<lambda>x y. x = (\<not> y)) (a # xs) (replicate n False) = take n (a # xs) proof (prove)
goal:
No subgoals!
theory Many_More

lemma plus_Collect_helper:
  "(+) x ` {xa. P (xa :: 'a :: len word)} = {xa. P (xa - x)}" by (fastforce simp add: image_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (+) x ` {xa. P xa} = {xa. P (xa - x)}
theory Many_More

lemma plus_Collect_helper2:
  "(+) (- x) ` {xa. P (xa :: 'a :: len word)} = {xa. P (x + xa)}" using plus_Collect_helper [of "- x" P] by (simp add: ac_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (+) (- x) ` {xa. P xa} = {xa. P (x + xa)} proof (prove)
using this:
(+) (- x) ` {xa. P xa} = {xa. P (xa - - x)}

goal (1 subgoal):
 1. (+) (- x) ` {xa. P xa} = {xa. P (x + xa)}
theory Many_More

lemma range_subset_eq2:
  "{a :: 'a :: len word .. b} \<noteq> {} \<Longrightarrow> ({a .. b} \<subseteq> {c .. d}) = (c \<le> a \<and> b \<le> d)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {a..b} \<noteq> {} \<Longrightarrow> ({a..b} \<subseteq> {c..d}) = (c \<le> a \<and> b \<le> d)
theory Many_More

lemma nat_mod_power_lem:
  fixes a :: nat
  shows "1 < a \<Longrightarrow> a ^ n mod a ^ m = (if m \<le> n then 0 else a ^ n)" apply (clarsimp) apply (clarsimp simp add: le_iff_add power_add) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 < a \<Longrightarrow> a ^ n mod a ^ m = (if m \<le> n then 0 else a ^ n) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>Suc 0 < a; m \<le> n\<rbrakk> \<Longrightarrow> a ^ n mod a ^ m = 0 proof (prove)
goal:
No subgoals!
theory Many_More

lemma i_hate_words_helper:
  "i \<le> (j - k :: nat) \<Longrightarrow> i \<le> j" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i \<le> j - k \<Longrightarrow> i \<le> j
theory Many_More

lemma i_hate_words:
  "unat (a :: 'a word) \<le> unat (b :: 'a :: len word) - Suc 0
    \<Longrightarrow> a \<noteq> -1" apply (frule i_hate_words_helper) apply (subst(asm) word_le_nat_alt[symmetric]) apply (clarsimp simp only: word_minus_one_le) apply (simp only: linorder_not_less[symmetric]) apply (erule notE) apply (rule diff_Suc_less) apply (subst neq0_conv[symmetric]) apply (subst unat_eq_0) apply (rule notI, drule arg_cong[where f="(+) 1"]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat a \<le> unat b - Suc 0 \<Longrightarrow> a \<noteq> - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat a \<le> unat b - Suc 0; unat a \<le> unat b\<rbrakk> \<Longrightarrow> a \<noteq> - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat a \<le> unat b - Suc 0; a \<le> b\<rbrakk> \<Longrightarrow> a \<noteq> - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat (- 1) \<le> unat (- 1) - Suc 0; b = - 1; a = - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> unat (- 1) - Suc 0 < unat (- 1); b = - 1; a = - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b = - 1; a = - 1\<rbrakk> \<Longrightarrow> unat (- 1) - Suc 0 < unat (- 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b = - 1; a = - 1\<rbrakk> \<Longrightarrow> 0 < unat (- 1) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b = - 1; a = - 1\<rbrakk> \<Longrightarrow> unat (- 1) \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b = - 1; a = - 1\<rbrakk> \<Longrightarrow> - 1 \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a = - 1; - 1 = 0; 1 + b = 1 + - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Many_More

lemma If_eq_obvious:
  "x \<noteq> z \<Longrightarrow> ((if P then x else y) = z) = (\<not> P \<and> y = z)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<noteq> z \<Longrightarrow> ((if P then x else y) = z) = (\<not> P \<and> y = z)
theory Many_More

lemma Some_to_the:
  "v = Some x \<Longrightarrow> x = the v" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. v = Some x \<Longrightarrow> x = the v
theory Many_More

lemma dom_if_Some:
  "dom (\<lambda>x. if P x then Some (f x) else g x) = {x. P x} \<union> dom g" by fastforce

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

lemma dom_insert_absorb:
  "x \<in> dom f \<Longrightarrow> insert x (dom f) = dom f" by (fact insert_absorb)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> dom f \<Longrightarrow> insert x (dom f) = dom f
theory Many_More

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

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

lemma ptr_add_image_multI:
  "\<lbrakk> \<And>x y. (x * val = y * val') = (x * val'' = y); x * val'' \<in> S \<rbrakk> \<Longrightarrow>
     ptr_add ptr (x * val) \<in> (\<lambda>p. ptr_add ptr (p * val')) ` S" by (auto simp add: image_iff) metis

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>x y. (x * val = y * val') = (x * val'' = y); x * val'' \<in> S\<rbrakk> \<Longrightarrow> ptr_add ptr (x * val) \<in> (\<lambda>p. ptr_add ptr (p * val')) ` S
theory Many_More

lemma dom_if:
  "dom (\<lambda>a. if a \<in> addrs then Some (f a) else g a)  = addrs \<union> dom g" by (auto simp: dom_def split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (\<lambda>a. if a \<in> addrs then Some (f a) else g a) = addrs \<union> dom g
theory Many_More

lemma drop_append_miracle:
  "n = length xs \<Longrightarrow> drop n (xs @ ys) = ys" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n = length xs \<Longrightarrow> drop n (xs @ ys) = ys
theory Many_More

lemma foldr_does_nothing_to_xf:
  "\<lbrakk> \<And>x s. x \<in> set xs \<Longrightarrow> xf (f x s) = xf s \<rbrakk> \<Longrightarrow> xf (foldr f xs s) = xf s" by (induct xs, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>x s. x \<in> set xs \<Longrightarrow> xf (f x s) = xf s) \<Longrightarrow> xf (foldr f xs s) = xf s
theory Many_More

lemma mod_mod_power_int:
  fixes k :: int
  shows "k mod 2 ^ m mod 2 ^ n = k mod 2 ^ (min m n)" by (fact mod_exp_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. k mod 2 ^ m mod 2 ^ n = k mod 2 ^ min m n
theory Many_More

lemma le_step_down_nat:"\<lbrakk>(i::nat) \<le> n; i = n \<longrightarrow> P; i \<le> n - 1 \<longrightarrow> P\<rbrakk> \<Longrightarrow> P" by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> n; i = n \<longrightarrow> P; i \<le> n - 1 \<longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory Many_More

lemma le_step_down_int:"\<lbrakk>(i::int) \<le> n; i = n \<longrightarrow> P; i \<le> n - 1 \<longrightarrow> P\<rbrakk> \<Longrightarrow> P" by arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i \<le> n; i = n \<longrightarrow> P; i \<le> n - 1 \<longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory Many_More

lemma replicate_numeral [simp]: "replicate (numeral k) x = x # replicate (pred_numeral k) x" by (simp add: numeral_eq_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. replicate (numeral k) x = x # replicate (pred_numeral k) x
theory Many_More

lemma list_exhaust_size_gt0:
  assumes "\<And>a list. y = a # list \<Longrightarrow> P"
  shows "0 < length y \<Longrightarrow> P" apply (cases y) apply simp apply (rule assms) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < length y \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<lbrakk>0 < length y; y = []\<rbrakk> \<Longrightarrow> P
 2. \<And>a list. \<lbrakk>0 < length y; y = a # list\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>0 < length y; y = a # list\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>0 < length y; y = a # list\<rbrakk> \<Longrightarrow> y = ?a1 a list # ?list1 a list proof (prove)
goal:
No subgoals!
theory Many_More

lemma list_exhaust_size_eq0:
  assumes "y = [] \<Longrightarrow> P"
  shows "length y = 0 \<Longrightarrow> P" apply (cases y) apply (rule assms) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length y = 0 \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length y = 0; y = []\<rbrakk> \<Longrightarrow> P
 2. \<And>a list. \<lbrakk>length y = 0; y = a # list\<rbrakk> \<Longrightarrow> P proof (prove)
goal (2 subgoals):
 1. \<lbrakk>length y = 0; y = []\<rbrakk> \<Longrightarrow> y = []
 2. \<And>a list. \<lbrakk>length y = 0; y = a # list\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<And>a list. \<lbrakk>length y = 0; y = a # list\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!
theory Many_More

lemma size_Cons_lem_eq: "y = xa # list \<Longrightarrow> size y = Suc k \<Longrightarrow> size list = k" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>y = xa # list; length y = Suc k\<rbrakk> \<Longrightarrow> length list = k
theory Many_More

lemma takeWhile_take_has_property:
  "n \<le> length (takeWhile P xs) \<Longrightarrow> \<forall>x \<in> set (take n xs). P x" by (induct xs arbitrary: n; simp split: if_split_asm) (case_tac n, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n \<le> length (takeWhile P xs) \<Longrightarrow> \<forall>x\<in>set (take n xs). P x
theory Many_More

lemma takeWhile_take_has_property_nth:
  "\<lbrakk> n < length (takeWhile P xs) \<rbrakk> \<Longrightarrow> P (xs ! n)" by (induct xs arbitrary: n; simp split: if_split_asm) (case_tac n, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < length (takeWhile P xs) \<Longrightarrow> P (xs ! n)
theory Many_More

lemma takeWhile_replicate_empty:
  "\<not> f x \<Longrightarrow> takeWhile f (replicate len x) = []" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> f x \<Longrightarrow> takeWhile f (replicate len x) = []
theory Many_More

lemma takeWhile_replicate_id:
  "f x \<Longrightarrow> takeWhile f (replicate len x) = replicate len x" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f x \<Longrightarrow> takeWhile f (replicate len x) = replicate len x
theory Many_More

lemma takeWhile_all:
  "length (takeWhile P xs) = length xs \<Longrightarrow> \<forall>x \<in> set xs. P x" by (induct xs) (auto split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length (takeWhile P xs) = length xs \<Longrightarrow> \<forall>x\<in>set xs. P x
theory Many_More

lemma nth_rev: "n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs - 1 - n)" using rev_nth by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs - 1 - n) proof (prove)
using this:
?n < length ?xs \<Longrightarrow> rev ?xs ! ?n = ?xs ! (length ?xs - Suc ?n)

goal (1 subgoal):
 1. n < length xs \<Longrightarrow> rev xs ! n = xs ! (length xs - 1 - n)
theory Many_More

lemma nth_rev_alt: "n < length ys \<Longrightarrow> ys ! n = rev ys ! (length ys - Suc n)" by (simp add: nth_rev)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < length ys \<Longrightarrow> ys ! n = rev ys ! (length ys - Suc n)
theory Many_More

lemma hd_butlast: "length xs > 1 \<Longrightarrow> hd (butlast xs) = hd xs" by (cases xs) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 < length xs \<Longrightarrow> hd (butlast xs) = hd xs
theory Many_More

lemma split_upt_on_n:
  "n < m \<Longrightarrow> [0 ..< m] = [0 ..< n] @ [n] @ [Suc n ..< m]" by (metis append_Cons append_Nil less_Suc_eq_le less_imp_le_nat upt_add_eq_append'
            upt_rec zero_less_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < m \<Longrightarrow> [0..<m] = [0..<n] @ [n] @ [Suc n..<m]
theory Many_More

lemma drop_eq_mono:
  assumes le: "m \<le> n"
  assumes drop: "drop m xs = drop m ys"
  shows "drop n xs = drop n ys" proof - have ex: "\<exists>p. n = p + m" by (rule exI[of _ "n - m"]) (simp add: le) then obtain p where p: "n = p + m" by blast show ?thesis unfolding p drop_drop[symmetric] drop by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. drop n xs = drop n ys proof (state)
goal (1 subgoal):
 1. drop n xs = drop n ys proof (prove)
goal (1 subgoal):
 1. \<exists>p. n = p + m proof (state)
this:
\<exists>p. n = p + m

goal (1 subgoal):
 1. drop n xs = drop n ys proof (chain)
picking this:
\<exists>p. n = p + m proof (prove)
using this:
\<exists>p. n = p + m

goal (1 subgoal):
 1. (\<And>p. n = p + m \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
n = p + m

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

goal:
No subgoals!
theory Many_More

lemma drop_Suc_nth:
  "n < length xs \<Longrightarrow> drop n xs = xs!n # drop (Suc n) xs" by (simp add: Cons_nth_drop_Suc)

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

lemma and_len: "xs = ys \<Longrightarrow> xs = ys \<and> length xs = length ys" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. xs = ys \<Longrightarrow> xs = ys \<and> length xs = length ys
theory Many_More

lemma tl_if: "tl (if p then xs else ys) = (if p then tl xs else tl ys)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tl (if p then xs else ys) = (if p then tl xs else tl ys)
theory Many_More

lemma if_single: "(if xc then [xab] else [an]) = [if xc then xab else an]" by auto

\<comment> \<open>note -- \<open>if_Cons\<close> can cause blowup in the size, if \<open>p\<close> is complex, so make a simproc\<close>

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if xc then [xab] else [an]) = [if xc then xab else an]
theory Many_More

lemma if_Cons: "(if p then x # xs else y # ys) = If p x y # If p xs ys" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if p then x # xs else y # ys) = (if p then x else y) # (if p then xs else ys)
theory Many_More

lemma list_of_false:
  "True \<notin> set xs \<Longrightarrow> xs = replicate (length xs) False" by (induct xs, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. True \<notin> set xs \<Longrightarrow> xs = replicate (length xs) False
theory Many_More

lemma list_all2_induct [consumes 1, case_names Nil Cons]:
  assumes lall: "list_all2 Q xs ys"
  and     nilr: "P [] []"
  and    consr: "\<And>x xs y ys. \<lbrakk>list_all2 Q xs ys; Q x y; P xs ys\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys)"
  shows  "P xs ys" using lall proof (induct rule: list_induct2 [OF list_all2_lengthD [OF lall]]) case 1 then show ?case by auto fact+ next case (2 x xs y ys) show ?case proof (rule consr) from "2.prems" show "list_all2 Q xs ys" and "Q x y" by simp_all then show "P xs ys" by (intro "2.hyps") qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P xs ys proof (prove)
using this:
list_all2 Q xs ys

goal (1 subgoal):
 1. P xs ys proof (state)
goal (2 subgoals):
 1. list_all2 Q [] [] \<Longrightarrow> P [] []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; list_all2 Q xs ys \<Longrightarrow> P xs ys; list_all2 Q (x # xs) (y # ys)\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys) proof (state)
this:
list_all2 Q [] []

goal (2 subgoals):
 1. list_all2 Q [] [] \<Longrightarrow> P [] []
 2. \<And>x xs y ys. \<lbrakk>length xs = length ys; list_all2 Q xs ys \<Longrightarrow> P xs ys; list_all2 Q (x # xs) (y # ys)\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys) proof (chain)
picking this:
list_all2 Q [] [] proof (prove)
using this:
list_all2 Q [] []

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

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; list_all2 Q xs ys \<Longrightarrow> P xs ys; list_all2 Q (x # xs) (y # ys)\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys) proof (state)
goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; list_all2 Q xs ys \<Longrightarrow> P xs ys; list_all2 Q (x # xs) (y # ys)\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys) proof (state)
this:
length xs = length ys
list_all2 Q xs ys \<Longrightarrow> P xs ys
list_all2 Q (x # xs) (y # ys)

goal (1 subgoal):
 1. \<And>x xs y ys. \<lbrakk>length xs = length ys; list_all2 Q xs ys \<Longrightarrow> P xs ys; list_all2 Q (x # xs) (y # ys)\<rbrakk> \<Longrightarrow> P (x # xs) (y # ys) proof (prove)
goal (1 subgoal):
 1. P (x # xs) (y # ys) proof (state)
goal (3 subgoals):
 1. list_all2 Q xs ys
 2. Q x y
 3. P xs ys proof (chain)
picking this:
list_all2 Q (x # xs) (y # ys) proof (prove)
using this:
list_all2 Q (x # xs) (y # ys)

goal (1 subgoal):
 1. list_all2 Q xs ys &&& Q x y proof (state)
this:
list_all2 Q xs ys
Q x y

goal (1 subgoal):
 1. P xs ys proof (chain)
picking this:
list_all2 Q xs ys
Q x y proof (prove)
using this:
list_all2 Q xs ys
Q x y

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

goal:
No subgoals! proof (state)
this:
P (x # xs) (y # ys)

goal:
No subgoals!
theory Many_More

lemma replicate_minus:
  "k < n \<Longrightarrow> replicate n False = replicate (n - k) False @ replicate k False" by (subst replicate_add [symmetric]) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. k < n \<Longrightarrow> replicate n False = replicate (n - k) False @ replicate k False
theory Many_More

lemma cart_singleton_empty:
  "(S \<times> {e} = {}) = (S = {})" by blast

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

lemma power_numeral: "a ^ numeral k = a * a ^ (pred_numeral k)" by (simp add: numeral_eq_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a ^ numeral k = a * a ^ pred_numeral k
theory Many_More

lemma funpow_numeral [simp]: "f ^^ numeral k = f \<circ> f ^^ (pred_numeral k)" by (simp add: numeral_eq_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f ^^ numeral k = f \<circ> f ^^ pred_numeral k
theory Many_More

lemma funpow_minus_simp: "0 < n \<Longrightarrow> f ^^ n = f \<circ> f ^^ (n - 1)" by (auto dest: gr0_implies_Suc)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 0 < n \<Longrightarrow> f ^^ n = f \<circ> f ^^ (n - 1)
theory Many_More

lemma rco_alt: "(f \<circ> g) ^^ n \<circ> f = f \<circ> (g \<circ> f) ^^ n" apply (rule ext) apply (induct n) apply (simp_all add: o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (f \<circ> g) ^^ n \<circ> f = f \<circ> (g \<circ> f) ^^ n proof (prove)
goal (1 subgoal):
 1. \<And>x. ((f \<circ> g) ^^ n \<circ> f) x = (f \<circ> (g \<circ> f) ^^ n) x proof (prove)
goal (2 subgoals):
 1. \<And>x. ((f \<circ> g) ^^ 0 \<circ> f) x = (f \<circ> (g \<circ> f) ^^ 0) x
 2. \<And>n x. (\<And>x. ((f \<circ> g) ^^ n \<circ> f) x = (f \<circ> (g \<circ> f) ^^ n) x) \<Longrightarrow> ((f \<circ> g) ^^ Suc n \<circ> f) x = (f \<circ> (g \<circ> f) ^^ Suc n) x proof (prove)
goal:
No subgoals!
theory Many_More

lemma union_sub:
  "\<lbrakk>B \<subseteq> A; C \<subseteq> B\<rbrakk> \<Longrightarrow> (A - B) \<union> (B - C) = (A - C)" by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>B \<subseteq> A; C \<subseteq> B\<rbrakk> \<Longrightarrow> A - B \<union> (B - C) = A - C
theory Many_More

lemma insert_sub:
  "x \<in> xs \<Longrightarrow> (insert x (xs - ys)) = (xs - (ys - {x}))" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> xs \<Longrightarrow> insert x (xs - ys) = xs - (ys - {x})
theory Many_More

lemma ran_upd:
  "\<lbrakk> inj_on f (dom f); f y = Some z \<rbrakk> \<Longrightarrow> ran (\<lambda>x. if x = y then None else f x) = ran f - {z}" unfolding ran_def apply (rule set_eqI) apply simp by (metis domI inj_on_eq_iff option.sel)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on f (dom f); f y = Some z\<rbrakk> \<Longrightarrow> ran (\<lambda>x. if x = y then None else f x) = ran f - {z} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>inj_on f (dom f); f y = Some z\<rbrakk> \<Longrightarrow> {b. \<exists>a. (if a = y then None else f a) = Some b} = {b. \<exists>a. f a = Some b} - {z} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>inj_on f (dom f); f y = Some z\<rbrakk> \<Longrightarrow> (x \<in> {b. \<exists>a. (if a = y then None else f a) = Some b}) = (x \<in> {b. \<exists>a. f a = Some b} - {z}) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>inj_on f (dom f); f y = Some z\<rbrakk> \<Longrightarrow> (\<exists>a. a \<noteq> y \<and> (a \<noteq> y \<longrightarrow> f a = Some x)) = ((\<exists>a. f a = Some x) \<and> x \<noteq> z)
theory Many_More

lemma if_apply_def2:
  "(if P then F else G) = (\<lambda>x. (P \<longrightarrow> F x) \<and> (\<not> P \<longrightarrow> G x))" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if P then F else G) = (\<lambda>x. (P \<longrightarrow> F x) \<and> (\<not> P \<longrightarrow> G x))
theory Many_More

lemma case_bool_If:
  "case_bool P Q b = (if b then P else Q)" by simp

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

lemma if_f:
  "(if a then f b else f c) = f (if a then b else c)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (if a then f b else f c) = f (if a then b else c)