kings-crown/FVELER_Isabelle huggingface dataset:
theory None_Top_Bot

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

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

lemma none_bot_funI:
  "\<exists>x. opt = Some x \<and> f x s \<Longrightarrow> none_bot f opt s" by (simp add: none_bot_fun_ex)

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

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

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

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

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

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

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

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

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

lemma nat_diff_less:
  "\<lbrakk> x < y + z; z \<le> x\<rbrakk> \<Longrightarrow> x - z < y" for x :: nat using less_diff_conv2 by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x < y + z; z \<le> x\<rbrakk> \<Longrightarrow> x - z < y proof (prove)
using this:
?k \<le> ?j \<Longrightarrow> (?j - ?k < ?i) = (?j < ?i + ?k)

goal (1 subgoal):
 1. \<lbrakk>x < y + z; z \<le> x\<rbrakk> \<Longrightarrow> x - z < y
theory CLib

lemma foldl_conv_concat:
  "foldl (@) xs xss = xs @ concat xss" proof (induct xss arbitrary: xs) case Nil show ?case by simp next case Cons then show ?case by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldl (@) xs xss = xs @ concat xss proof (state)
goal (2 subgoals):
 1. \<And>xs. foldl (@) xs [] = xs @ concat []
 2. \<And>a xss xs. (\<And>xs. foldl (@) xs xss = xs @ concat xss) \<Longrightarrow> foldl (@) xs (a # xss) = xs @ concat (a # xss) proof (state)
this:


goal (2 subgoals):
 1. \<And>xs. foldl (@) xs [] = xs @ concat []
 2. \<And>a xss xs. (\<And>xs. foldl (@) xs xss = xs @ concat xss) \<Longrightarrow> foldl (@) xs (a # xss) = xs @ concat (a # xss) proof (prove)
goal (1 subgoal):
 1. foldl (@) xs [] = xs @ concat [] proof (state)
this:
foldl (@) xs [] = xs @ concat []

goal (1 subgoal):
 1. \<And>a xss xs. (\<And>xs. foldl (@) xs xss = xs @ concat xss) \<Longrightarrow> foldl (@) xs (a # xss) = xs @ concat (a # xss) proof (state)
goal (1 subgoal):
 1. \<And>a xss xs. (\<And>xs. foldl (@) xs xss = xs @ concat xss) \<Longrightarrow> foldl (@) xs (a # xss) = xs @ concat (a # xss) proof (state)
this:
foldl (@) ?xs xss_ = ?xs @ concat xss_

goal (1 subgoal):
 1. \<And>a xss xs. (\<And>xs. foldl (@) xs xss = xs @ concat xss) \<Longrightarrow> foldl (@) xs (a # xss) = xs @ concat (a # xss) proof (chain)
picking this:
foldl (@) ?xs xss_ = ?xs @ concat xss_ proof (prove)
using this:
foldl (@) ?xs xss_ = ?xs @ concat xss_

goal (1 subgoal):
 1. foldl (@) xs (a_ # xss_) = xs @ concat (a_ # xss_) proof (state)
this:
foldl (@) xs (a_ # xss_) = xs @ concat (a_ # xss_)

goal:
No subgoals!
theory CLib

lemma foldl_concat_concat:
  "foldl (@) [] (xs @ ys) = foldl (@) [] xs @ foldl (@) [] ys" by (simp add: foldl_conv_concat)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldl (@) [] (xs @ ys) = foldl (@) [] xs @ foldl (@) [] ys
theory CLib

lemma take_drop_foldl_concat:
  "\<lbrakk> \<And>y. y < m \<Longrightarrow> length (f y) = n; x < m \<rbrakk> \<Longrightarrow>
   take n (drop (x * n) (foldl (@) [] (map f [0 ..< m]))) = f x" apply (subst split_upt_on_n, assumption) apply (simp only: foldl_concat_concat map_append) apply (subst drop_append_miracle) apply (induct x; simp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>y. y < m \<Longrightarrow> length (f y) = n; x < m\<rbrakk> \<Longrightarrow> take n (drop (x * n) (foldl (@) [] (map f [0..<m]))) = f x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>y. y < m \<Longrightarrow> length (f y) = n; x < m\<rbrakk> \<Longrightarrow> take n (drop (x * n) (foldl (@) [] (map f ([0..<x] @ [x] @ [Suc x..<m])))) = f x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>y. y < m \<Longrightarrow> length (f y) = n; x < m\<rbrakk> \<Longrightarrow> take n (drop (x * n) (foldl (@) [] (map f [0..<x]) @ foldl (@) [] (map f [x]) @ foldl (@) [] (map f [Suc x..<m]))) = f x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<And>y. y < m \<Longrightarrow> length (f y) = n; x < m\<rbrakk> \<Longrightarrow> x * n = length (foldl (@) [] (map f [0..<x]))
 2. \<lbrakk>\<And>y. y < m \<Longrightarrow> length (f y) = n; x < m\<rbrakk> \<Longrightarrow> take n (foldl (@) [] (map f [x]) @ foldl (@) [] (map f [Suc x..<m])) = f x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>y. y < m \<Longrightarrow> length (f y) = n; x < m\<rbrakk> \<Longrightarrow> take n (foldl (@) [] (map f [x]) @ foldl (@) [] (map f [Suc x..<m])) = f x proof (prove)
goal:
No subgoals!
theory CLib

lemma foldl_does_nothing:
  "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f s x = s \<rbrakk> \<Longrightarrow> foldl f s xs = s" by (induct xs) auto

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

lemma eq1: "(1 :: nat) = 1 + 0" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 = 1 + 0
theory Try_Attribute

lemma eq2: "(2 :: nat) = 1 + 1" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 2 = 1 + 1
theory Try_Attribute

lemma ineq: "(1 :: nat) < 2" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 < 2
theory Repeat_Attribute

lemma test1: "True \<Longrightarrow> True" .

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. True \<Longrightarrow> True
theory Repeat_Attribute

lemma test2: "True \<Longrightarrow> True \<Longrightarrow> True" .

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>True; True\<rbrakk> \<Longrightarrow> True
theory NICTATools

lemma test_unused_meta_forall: "\<And>x. y \<or> \<not> y" oops

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

lemma hd_map_simp:
  "b \<noteq> [] \<Longrightarrow> hd (map a b) = a (hd b)" by (rule hd_map)

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

lemma tl_map_simp:
  "tl (map a b) = map a (tl b)" by (induct b,auto)

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

lemma Collect_eq:
  "{x. P x} = {x. Q x} \<longleftrightarrow> (\<forall>x. P x = Q x)" by (rule iffI) auto

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

lemma iff_impI: "\<lbrakk>P \<Longrightarrow> Q = R\<rbrakk> \<Longrightarrow> (P \<longrightarrow> Q) = (P \<longrightarrow> R)" by blast

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

lemma if_apply_cong[fundef_cong]:
  "\<lbrakk> P = P'; x = x'; P' \<Longrightarrow> f x' = f' x'; \<not> P' \<Longrightarrow> g x' = g' x' \<rbrakk>
     \<Longrightarrow> (if P then f else g) x = (if P' then f' else g') x'" by simp

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

lemma case_prod_apply_cong[fundef_cong]:
  "\<lbrakk> f (fst p) (snd p) s = f' (fst p') (snd p') s' \<rbrakk> \<Longrightarrow> case_prod f p s = case_prod f' p' s'" by (simp add: split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f (fst p) (snd p) s = f' (fst p') (snd p') s' \<Longrightarrow> (case p of (x, xa) \<Rightarrow> f x xa) s = (case p' of (x, xa) \<Rightarrow> f' x xa) s'
theory Lib

lemma prod_injects:
  "(x,y) = p \<Longrightarrow> x = fst p \<and> y = snd p"
  "p = (x,y) \<Longrightarrow> x = fst p \<and> y = snd p" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((x, y) = p \<Longrightarrow> x = fst p \<and> y = snd p) &&& (p = (x, y) \<Longrightarrow> x = fst p \<and> y = snd p)
theory Lib

lemma opt_rel_None_rhs[simp]:
  "opt_rel f x None = (x = None)" by (cases x, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. opt_rel f x None = (x = None)
theory Lib

lemma opt_rel_Some_rhs[simp]:
  "opt_rel f x (Some y) = (\<exists>x'. x = Some x' \<and> f x' y)" by (cases x, simp_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. opt_rel f x (Some y) = (\<exists>x'. x = Some x' \<and> f x' y)
theory Lib

lemma tranclD2:
  "(x, y) \<in> R\<^sup>+ \<Longrightarrow> \<exists>z. (x, z) \<in> R\<^sup>* \<and> (z, y) \<in> R" by (erule tranclE) auto

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

lemma linorder_min_same1 [simp]:
  "(min y x = y) = (y \<le> (x::'a::linorder))" by (auto simp: min_def linorder_not_less)

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

lemma linorder_min_same2 [simp]:
  "(min x y = y) = (y \<le> (x::'a::linorder))" by (auto simp: min_def linorder_not_le)

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

lemma False_implies_equals [simp]:
  "((False \<Longrightarrow> P) \<Longrightarrow> PROP Q) \<equiv> PROP Q" apply (rule equal_intr_rule) apply (erule meta_mp) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((False \<Longrightarrow> P) \<Longrightarrow> PROP Q) \<equiv> PROP Q proof (prove)
goal (2 subgoals):
 1. ((False \<Longrightarrow> P) \<Longrightarrow> PROP Q) \<Longrightarrow> PROP Q
 2. \<lbrakk>PROP Q; False \<Longrightarrow> P\<rbrakk> \<Longrightarrow> PROP Q proof (prove)
goal (2 subgoals):
 1. False \<Longrightarrow> P
 2. \<lbrakk>PROP Q; False \<Longrightarrow> P\<rbrakk> \<Longrightarrow> PROP Q proof (prove)
goal (1 subgoal):
 1. \<lbrakk>PROP Q; False \<Longrightarrow> P\<rbrakk> \<Longrightarrow> PROP Q proof (prove)
goal:
No subgoals!
theory Lib

lemma split_paired_Ball:
  "(\<forall>x \<in> A. P x) = (\<forall>x y. (x,y) \<in> A \<longrightarrow> P (x,y))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>A. P x) = (\<forall>x y. (x, y) \<in> A \<longrightarrow> P (x, y))
theory Lib

lemma split_paired_Bex:
  "(\<exists>x \<in> A. P x) = (\<exists>x y. (x,y) \<in> A \<and> P (x,y))" by auto

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

lemma bexI_minus:
  "\<lbrakk> P x; x \<in> A; x \<notin> B \<rbrakk> \<Longrightarrow> \<exists>x \<in> A - B. P x" unfolding Bex_def by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P x; x \<in> A; x \<notin> B\<rbrakk> \<Longrightarrow> \<exists>x\<in>A - B. P x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P x; x \<in> A; x \<notin> B\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> A - B \<and> P x
theory Lib

lemma delete_remove1:
  "delete x xs = remove1 x xs" by (induct xs, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. delete x xs = remove1 x xs
theory Lib

lemma ignore_if:
  "(y and z) s \<Longrightarrow> (if x then y else z) s" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (y and z) s \<Longrightarrow> (if x then y else z) s
theory Lib

lemma isRight_right_map:
  "isRight (case_sum Inl (Inr o f) v) = isRight v" by (simp split: sum.split)

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

lemma first_in_uptoD:
  "a \<le> b \<Longrightarrow> (a::'a::order) \<in> {a..b}" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a \<le> b \<Longrightarrow> a \<in> {a..b}
theory Lib

lemma construct_singleton:
  "\<lbrakk> S \<noteq> {}; \<forall>s\<in>S. \<forall>s'. s \<noteq> s' \<longrightarrow> s' \<notin> S \<rbrakk> \<Longrightarrow> \<exists>x. S = {x}" by blast

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

lemma bleeding_obvious:
  "(P \<Longrightarrow> True) \<equiv> (Trueprop True)" by (rule, simp_all)

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

lemma Some_helper:
  "x = Some y \<Longrightarrow> x \<noteq> None" by simp

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

lemma ExNot [iff]: "Ex Not" by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Ex Not
theory Lib

lemma cases_simp2 [simp]:
  "((\<not> P \<longrightarrow> Q) \<and> (P \<longrightarrow> Q)) = Q" by blast

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

lemma a_imp_b_imp_b:
  "((a \<longrightarrow> b) \<longrightarrow> b) = (a \<or> b)" by blast

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

lemma length_neq:
  "length as \<noteq> length bs \<Longrightarrow> as \<noteq> bs" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length as \<noteq> length bs \<Longrightarrow> as \<noteq> bs
theory Lib

lemma take_neq_length:
  "\<lbrakk> x \<noteq> y; x \<le> length as; y \<le> length bs\<rbrakk> \<Longrightarrow> take x as \<noteq> take y bs" by (rule length_neq, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<noteq> y; x \<le> length as; y \<le> length bs\<rbrakk> \<Longrightarrow> take x as \<noteq> take y bs
theory Lib

lemma eq_concat_lenD:
  "xs = ys @ zs \<Longrightarrow> length xs = length ys + length zs" by simp

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

lemma map_upt_reindex': "map f [a ..< b] = map (\<lambda>n. f (n + a - x)) [x ..< x + b - a]" by (rule nth_equalityI; clarsimp simp: add.commute)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map f [a..<b] = map (\<lambda>n. f (n + a - x)) [x..<x + b - a]
theory Lib

lemma map_upt_reindex: "map f [a ..< b] = map (\<lambda>n. f (n + a)) [0 ..< b - a]" by (subst map_upt_reindex' [where x=0]) clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map f [a..<b] = map (\<lambda>n. f (n + a)) [0..<b - a]
theory Lib

lemma notemptyI:
  "x \<in> S \<Longrightarrow> S \<noteq> {}" by clarsimp

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

lemma setcomp_Max_has_prop:
  assumes a: "P x"
  shows "P (Max {(x::'a::{finite,linorder}). P x})" proof - from a have "Max {x. P x} \<in> {x. P x}" by - (rule Max_in, auto intro: notemptyI) thus ?thesis by auto qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P (Max {x. P x}) proof (state)
goal (1 subgoal):
 1. P (Max {x. P x}) proof (chain)
picking this:
P x proof (prove)
using this:
P x

goal (1 subgoal):
 1. Max {x. P x} \<in> {x. P x} proof (state)
this:
Max {x. P x} \<in> {x. P x}

goal (1 subgoal):
 1. P (Max {x. P x}) proof (prove)
using this:
Max {x. P x} \<in> {x. P x}

goal (1 subgoal):
 1. P (Max {x. P x}) proof (state)
this:
P (Max {x. P x})

goal:
No subgoals!
theory Lib

lemma cons_set_intro:
  "lst = x # xs \<Longrightarrow> x \<in> set lst" by fastforce

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

lemma list_all2_conj_nth:
  assumes lall: "list_all2 P as cs"
  and       rl: "\<And>n. \<lbrakk>P (as ! n) (cs ! n); n < length as\<rbrakk> \<Longrightarrow> Q (as ! n) (cs ! n)"
  shows   "list_all2 (\<lambda>a b. P a b \<and> Q a b) as cs" proof (rule list_all2_all_nthI) from lall show "length as = length cs" .. next fix n assume "n < length as" show "P (as ! n) (cs ! n) \<and> Q (as ! n) (cs ! n)" proof from lall show "P (as ! n) (cs ! n)" by (rule list_all2_nthD) fact thus "Q (as ! n) (cs ! n)" by (rule rl) fact qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_all2 (\<lambda>a b. P a b \<and> Q a b) as cs proof (state)
goal (2 subgoals):
 1. length as = length cs
 2. \<And>n. n < length as \<Longrightarrow> P (as ! n) (cs ! n) \<and> Q (as ! n) (cs ! n) proof (chain)
picking this:
list_all2 P as cs proof (prove)
using this:
list_all2 P as cs

goal (1 subgoal):
 1. length as = length cs proof (state)
this:
length as = length cs

goal (1 subgoal):
 1. \<And>n. n < length as \<Longrightarrow> P (as ! n) (cs ! n) \<and> Q (as ! n) (cs ! n) proof (state)
goal (1 subgoal):
 1. \<And>n. n < length as \<Longrightarrow> P (as ! n) (cs ! n) \<and> Q (as ! n) (cs ! n) proof (state)
goal (1 subgoal):
 1. \<And>n. n < length as \<Longrightarrow> P (as ! n) (cs ! n) \<and> Q (as ! n) (cs ! n) proof (state)
this:
n < length as

goal (1 subgoal):
 1. \<And>n. n < length as \<Longrightarrow> P (as ! n) (cs ! n) \<and> Q (as ! n) (cs ! n) proof (prove)
goal (1 subgoal):
 1. P (as ! n) (cs ! n) \<and> Q (as ! n) (cs ! n) proof (state)
goal (2 subgoals):
 1. P (as ! n) (cs ! n)
 2. Q (as ! n) (cs ! n) proof (chain)
picking this:
list_all2 P as cs proof (prove)
using this:
list_all2 P as cs

goal (1 subgoal):
 1. P (as ! n) (cs ! n) proof (state)
this:
P (as ! n) (cs ! n)

goal (1 subgoal):
 1. Q (as ! n) (cs ! n) proof (prove)
using this:
P (as ! n) (cs ! n)

goal (1 subgoal):
 1. Q (as ! n) (cs ! n) proof (state)
this:
Q (as ! n) (cs ! n)

goal:
No subgoals! proof (state)
this:
P (as ! n) (cs ! n) \<and> Q (as ! n) (cs ! n)

goal:
No subgoals!
theory Lib

lemma list_all2_conj:
  assumes lall1: "list_all2 P as cs"
  and     lall2: "list_all2 Q as cs"
  shows   "list_all2 (\<lambda>a b. P a b \<and> Q a b) as cs" proof (rule list_all2_all_nthI) from lall1 show "length as = length cs" .. next fix n assume "n < length as" show "P (as ! n) (cs ! n) \<and> Q (as ! n) (cs ! n)" proof from lall1 show "P (as ! n) (cs ! n)" by (rule list_all2_nthD) fact from lall2 show "Q (as ! n) (cs ! n)" by (rule list_all2_nthD) fact qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_all2 (\<lambda>a b. P a b \<and> Q a b) as cs proof (state)
goal (2 subgoals):
 1. length as = length cs
 2. \<And>n. n < length as \<Longrightarrow> P (as ! n) (cs ! n) \<and> Q (as ! n) (cs ! n) proof (chain)
picking this:
list_all2 P as cs proof (prove)
using this:
list_all2 P as cs

goal (1 subgoal):
 1. length as = length cs proof (state)
this:
length as = length cs

goal (1 subgoal):
 1. \<And>n. n < length as \<Longrightarrow> P (as ! n) (cs ! n) \<and> Q (as ! n) (cs ! n) proof (state)
goal (1 subgoal):
 1. \<And>n. n < length as \<Longrightarrow> P (as ! n) (cs ! n) \<and> Q (as ! n) (cs ! n) proof (state)
goal (1 subgoal):
 1. \<And>n. n < length as \<Longrightarrow> P (as ! n) (cs ! n) \<and> Q (as ! n) (cs ! n) proof (state)
this:
n < length as

goal (1 subgoal):
 1. \<And>n. n < length as \<Longrightarrow> P (as ! n) (cs ! n) \<and> Q (as ! n) (cs ! n) proof (prove)
goal (1 subgoal):
 1. P (as ! n) (cs ! n) \<and> Q (as ! n) (cs ! n) proof (state)
goal (2 subgoals):
 1. P (as ! n) (cs ! n)
 2. Q (as ! n) (cs ! n) proof (chain)
picking this:
list_all2 P as cs proof (prove)
using this:
list_all2 P as cs

goal (1 subgoal):
 1. P (as ! n) (cs ! n) proof (state)
this:
P (as ! n) (cs ! n)

goal (1 subgoal):
 1. Q (as ! n) (cs ! n) proof (chain)
picking this:
list_all2 Q as cs proof (prove)
using this:
list_all2 Q as cs

goal (1 subgoal):
 1. Q (as ! n) (cs ! n) proof (state)
this:
Q (as ! n) (cs ! n)

goal:
No subgoals! proof (state)
this:
P (as ! n) (cs ! n) \<and> Q (as ! n) (cs ! n)

goal:
No subgoals!
theory Lib

lemma all_set_into_list_all2:
  assumes lall: "\<forall>x \<in> set ls. P x"
  and           "length ls = length ls'"
  shows  "list_all2 (\<lambda>a b. P a) ls ls'" proof (rule list_all2_all_nthI) fix n assume "n < length ls" from lall show "P (ls ! n)" by (rule bspec [OF _ nth_mem]) fact qed fact

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_all2 (\<lambda>a b. P a) ls ls' proof (state)
goal (2 subgoals):
 1. length ls = length ls'
 2. \<And>n. n < length ls \<Longrightarrow> P (ls ! n) proof (state)
goal (2 subgoals):
 1. length ls = length ls'
 2. \<And>n. n < length ls \<Longrightarrow> P (ls ! n) proof (state)
this:
n < length ls

goal (2 subgoals):
 1. length ls = length ls'
 2. \<And>n. n < length ls \<Longrightarrow> P (ls ! n) proof (chain)
picking this:
\<forall>x\<in>set ls. P x proof (prove)
using this:
\<forall>x\<in>set ls. P x

goal (1 subgoal):
 1. P (ls ! n) proof (state)
this:
P (ls ! n)

goal (1 subgoal):
 1. length ls = length ls'
theory Lib

lemma True_notin_set_replicate_conv:
  "True \<notin> set ls = (ls = replicate (length ls) False)" by (induct ls) simp+

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

lemma Collect_singleton_eqI:
  "(\<And>x. P x = (x = v)) \<Longrightarrow> {x. P x} = {v}" by auto

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

lemma exEI:
  "\<lbrakk> \<exists>y. P y; \<And>x. P x \<Longrightarrow> Q x \<rbrakk> \<Longrightarrow> \<exists>z. Q z" by (rule ex_forward)

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

lemma allEI:
  assumes "\<forall>x. P x"
  assumes "\<And>x. P x \<Longrightarrow> Q x"
  shows   "\<forall>x. Q x" using assms by (rule all_forward)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x. Q x proof (prove)
using this:
\<forall>x. P x
P ?x \<Longrightarrow> Q ?x

goal (1 subgoal):
 1. \<forall>x. Q x
theory Lib

lemma bexEI:
  "\<lbrakk>\<exists>x\<in>S. Q x; \<And>x. \<lbrakk>x \<in> S; Q x\<rbrakk> \<Longrightarrow> P x\<rbrakk> \<Longrightarrow> \<exists>x\<in>S. P x" by blast

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

lemma orthD1:
  "\<lbrakk> S \<inter> S' = {}; x \<in> S\<rbrakk> \<Longrightarrow> x \<notin> S'" by auto

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

lemma orthD2:
  "\<lbrakk> S \<inter> S' = {}; x \<in> S'\<rbrakk> \<Longrightarrow> x \<notin> S" by auto

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

lemma ball_reorder:
  "(\<forall>x \<in> A. \<forall>y \<in> B. P x y) = (\<forall>y \<in> B. \<forall>x \<in> A.  P x y)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>A. \<forall>y\<in>B. P x y) = (\<forall>y\<in>B. \<forall>x\<in>A. P x y)