kings-crown/FVELER_Isabelle huggingface dataset:
theory Lib

lemma ranE:
  "\<lbrakk> v \<in> ran f; \<And>x. f x = Some v \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" by (auto simp: ran_def)

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

lemma ran_map_option_restrict_eq:
  "\<lbrakk> x \<in> ran (map_option f o g); x \<notin> ran (map_option f o (g |` (- {y}))) \<rbrakk>
        \<Longrightarrow> \<exists>v. g y = Some v \<and> f v = x" apply (clarsimp simp: elim!: ranE) apply (rename_tac w z) apply (case_tac "w = y") apply clarsimp apply (erule notE, rule_tac a=w in ranI) apply (simp add: restrict_map_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> ran (map_option f \<circ> g); x \<notin> ran (map_option f \<circ> g |` (- {y}))\<rbrakk> \<Longrightarrow> \<exists>v. g y = Some v \<and> f v = x proof (prove)
goal (1 subgoal):
 1. \<And>xa z. \<lbrakk>f z \<notin> ran (map_option f \<circ> g |` (- {y})); g xa = Some z; x = f z\<rbrakk> \<Longrightarrow> \<exists>v. g y = Some v \<and> f v = f z proof (prove)
goal (1 subgoal):
 1. \<And>w z. \<lbrakk>f z \<notin> ran (map_option f \<circ> g |` (- {y})); g w = Some z; x = f z\<rbrakk> \<Longrightarrow> \<exists>v. g y = Some v \<and> f v = f z proof (prove)
goal (2 subgoals):
 1. \<And>w z. \<lbrakk>f z \<notin> ran (map_option f \<circ> g |` (- {y})); g w = Some z; x = f z; w = y\<rbrakk> \<Longrightarrow> \<exists>v. g y = Some v \<and> f v = f z
 2. \<And>w z. \<lbrakk>f z \<notin> ran (map_option f \<circ> g |` (- {y})); g w = Some z; x = f z; w \<noteq> y\<rbrakk> \<Longrightarrow> \<exists>v. g y = Some v \<and> f v = f z proof (prove)
goal (1 subgoal):
 1. \<And>w z. \<lbrakk>f z \<notin> ran (map_option f \<circ> g |` (- {y})); g w = Some z; x = f z; w \<noteq> y\<rbrakk> \<Longrightarrow> \<exists>v. g y = Some v \<and> f v = f z proof (prove)
goal (1 subgoal):
 1. \<And>w z. \<lbrakk>g w = Some z; x = f z; w \<noteq> y\<rbrakk> \<Longrightarrow> (map_option f \<circ> g |` (- {y})) w = Some (f z) proof (prove)
goal:
No subgoals!
theory Lib

lemma map_zip_fst:
  "length xs = length ys \<Longrightarrow> map (\<lambda>(x, y). f x) (zip xs ys) = map f xs" by (two_induct xs ys)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<Longrightarrow> map2 (\<lambda>x y. f x) xs ys = map f xs
theory Lib

lemma map_zip_fst':
  "length xs \<le> length ys \<Longrightarrow> map (\<lambda>(x, y). f x) (zip xs ys) = map f xs" by (metis length_map map_fst_zip' map_zip_fst zip_map_fst_snd)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs \<le> length ys \<Longrightarrow> map2 (\<lambda>x y. f x) xs ys = map f xs
theory Lib

lemma map_zip_snd:
  "length xs = length ys \<Longrightarrow> map (\<lambda>(x, y). f y) (zip xs ys) = map f ys" by (two_induct xs ys)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs = length ys \<Longrightarrow> map2 (\<lambda>x. f) xs ys = map f ys
theory Lib

lemma map_of_zip_tuple_in:
  "\<lbrakk>(x, y) \<in> set (zip xs ys); distinct xs\<rbrakk> \<Longrightarrow> map_of (zip xs ys) x = Some y" by (two_induct xs ys) (auto intro: in_set_zipE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, y) \<in> set (zip xs ys); distinct xs\<rbrakk> \<Longrightarrow> map_of (zip xs ys) x = Some y
theory Lib

lemma in_set_zip1:
  "(x, y) \<in> set (zip xs ys) \<Longrightarrow> x \<in> set xs" by (erule in_set_zipE)

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

lemma in_set_zip2:
  "(x, y) \<in> set (zip xs ys) \<Longrightarrow> y \<in> set ys" by (erule in_set_zipE)

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

lemma map_zip_snd_take:
  "map (\<lambda>(x, y). f y) (zip xs ys) = map f (take (length xs) ys)" apply (subst map_zip_snd' [symmetric, where xs=xs and ys="take (length xs) ys"], simp) apply (subst zip_take_length [symmetric], simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map2 (\<lambda>x. f) xs ys = map f (take (length xs) ys) proof (prove)
goal (1 subgoal):
 1. map2 (\<lambda>x. f) xs ys = map2 (\<lambda>x. f) xs (take (length xs) ys) proof (prove)
goal:
No subgoals!
theory Lib

lemma map_of_zip_is_index:
  "\<lbrakk>length xs = length ys; x \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>i. (map_of (zip xs ys)) x = Some (ys ! i)" apply (induct rule: list_induct2; simp) apply (rule conjI; clarsimp) apply (metis nth_Cons_0) apply (metis nth_Cons_Suc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>length xs = length ys; x \<in> set xs\<rbrakk> \<Longrightarrow> \<exists>i. map_of (zip xs ys) x = Some (ys ! i) proof (prove)
goal (1 subgoal):
 1. \<And>xa xs y ys. \<lbrakk>length xs = length ys; x \<in> set xs \<Longrightarrow> \<exists>i. map_of (zip xs ys) x = Some (ys ! i); x = xa \<or> x \<in> set xs\<rbrakk> \<Longrightarrow> (x = xa \<longrightarrow> (\<exists>i. y = (y # ys) ! i)) \<and> (x \<noteq> xa \<longrightarrow> (\<exists>i. map_of (zip xs ys) x = Some ((y # ys) ! i))) proof (prove)
goal (2 subgoals):
 1. \<And>xs y ys. \<lbrakk>length xs = length ys; x \<in> set xs \<Longrightarrow> \<exists>i. map_of (zip xs ys) x = Some (ys ! i)\<rbrakk> \<Longrightarrow> \<exists>i. y = (y # ys) ! i
 2. \<And>xa xs y ys i. \<lbrakk>length xs = length ys; x \<noteq> xa; x \<in> set xs; map_of (zip xs ys) x = Some (ys ! i)\<rbrakk> \<Longrightarrow> \<exists>ia. ys ! i = (y # ys) ! ia proof (prove)
goal (1 subgoal):
 1. \<And>xa xs y ys i. \<lbrakk>length xs = length ys; x \<noteq> xa; x \<in> set xs; map_of (zip xs ys) x = Some (ys ! i)\<rbrakk> \<Longrightarrow> \<exists>ia. ys ! i = (y # ys) ! ia proof (prove)
goal:
No subgoals!
theory Lib

lemma map_of_zip_take_update:
  "\<lbrakk>i < length xs; length xs \<le> length ys; distinct xs\<rbrakk>
  \<Longrightarrow> (map_of (zip (take i xs) ys)) (xs ! i \<mapsto> ys ! i) = map_of (zip (take (Suc i) xs) ys)" apply (rule ext, rename_tac x) apply (case_tac "x=xs ! i"; clarsimp) apply (rule map_of_is_SomeI[symmetric]) apply (simp add: map_fst_zip') apply (force simp add: set_zip) apply (clarsimp simp: take_Suc_conv_app_nth zip_append_singleton map_add_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length xs; length xs \<le> length ys; distinct xs\<rbrakk> \<Longrightarrow> (map_of (zip (take i xs) ys))(xs ! i \<mapsto> ys ! i) = map_of (zip (take (Suc i) xs) ys) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>i < length xs; length xs \<le> length ys; distinct xs\<rbrakk> \<Longrightarrow> ((map_of (zip (take i xs) ys))(xs ! i \<mapsto> ys ! i)) x = map_of (zip (take (Suc i) xs) ys) x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i < length xs; length xs \<le> length ys; distinct xs\<rbrakk> \<Longrightarrow> Some (ys ! i) = map_of (zip (take (Suc i) xs) ys) (xs ! i)
 2. \<And>x. \<lbrakk>i < length xs; length xs \<le> length ys; distinct xs; x \<noteq> xs ! i\<rbrakk> \<Longrightarrow> map_of (zip (take i xs) ys) x = map_of (zip (take (Suc i) xs) ys) x proof (prove)
goal (3 subgoals):
 1. \<lbrakk>i < length xs; length xs \<le> length ys; distinct xs\<rbrakk> \<Longrightarrow> distinct (map fst (zip (take (Suc i) xs) ys))
 2. \<lbrakk>i < length xs; length xs \<le> length ys; distinct xs\<rbrakk> \<Longrightarrow> (xs ! i, ys ! i) \<in> set (zip (take (Suc i) xs) ys)
 3. \<And>x. \<lbrakk>i < length xs; length xs \<le> length ys; distinct xs; x \<noteq> xs ! i\<rbrakk> \<Longrightarrow> map_of (zip (take i xs) ys) x = map_of (zip (take (Suc i) xs) ys) x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>i < length xs; length xs \<le> length ys; distinct xs\<rbrakk> \<Longrightarrow> (xs ! i, ys ! i) \<in> set (zip (take (Suc i) xs) ys)
 2. \<And>x. \<lbrakk>i < length xs; length xs \<le> length ys; distinct xs; x \<noteq> xs ! i\<rbrakk> \<Longrightarrow> map_of (zip (take i xs) ys) x = map_of (zip (take (Suc i) xs) ys) x proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>i < length xs; length xs \<le> length ys; distinct xs; x \<noteq> xs ! i\<rbrakk> \<Longrightarrow> map_of (zip (take i xs) ys) x = map_of (zip (take (Suc i) xs) ys) x proof (prove)
goal:
No subgoals!
theory Lib

lemma map_of_zip_is_Some':
  "length xs \<le> length ys \<Longrightarrow> (x \<in> set xs) = (\<exists>y. map_of (zip xs ys) x = Some y)" apply (subst zip_take_length[symmetric]) apply (rule map_of_zip_is_Some) by (metis length_take min_absorb2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length xs \<le> length ys \<Longrightarrow> (x \<in> set xs) = (\<exists>y. map_of (zip xs ys) x = Some y) proof (prove)
goal (1 subgoal):
 1. length xs \<le> length ys \<Longrightarrow> (x \<in> set xs) = (\<exists>y. map_of (zip xs (take (length xs) ys)) x = Some y) proof (prove)
goal (1 subgoal):
 1. length xs \<le> length ys \<Longrightarrow> length xs = length (take (length xs) ys)
theory Lib

lemma map_of_zip_inj:
  "\<lbrakk>distinct xs; distinct ys; length xs = length ys\<rbrakk>
    \<Longrightarrow> inj_on (\<lambda>x. (the (map_of (zip xs ys) x))) (set xs)" apply (clarsimp simp: inj_on_def) apply (subst (asm) map_of_zip_is_Some, assumption)+ apply clarsimp apply (clarsimp simp: set_zip) by (metis nth_eq_iff_index_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; distinct ys; length xs = length ys\<rbrakk> \<Longrightarrow> inj_on (\<lambda>x. the (map_of (zip xs ys) x)) (set xs) proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>distinct xs; distinct ys; length xs = length ys; x \<in> set xs; y \<in> set xs; the (map_of (zip xs ys) x) = the (map_of (zip xs ys) y)\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>distinct xs; distinct ys; length xs = length ys; \<exists>y. map_of (zip xs ys) x = Some y; \<exists>ya. map_of (zip xs ys) y = Some ya; the (map_of (zip xs ys) x) = the (map_of (zip xs ys) y)\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>x y yb. \<lbrakk>distinct xs; distinct ys; length xs = length ys; (x, yb) \<in> set (zip xs ys); (y, yb) \<in> set (zip xs ys)\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<And>i ia. \<lbrakk>distinct xs; distinct ys; length xs = length ys; i < length ys; ys ! i = ys ! ia; ia < length ys\<rbrakk> \<Longrightarrow> xs ! i = xs ! ia
theory Lib

lemma list_all_nth:
  "\<lbrakk>list_all P xs; i < length xs\<rbrakk> \<Longrightarrow> P (xs ! i)" by (metis list_all_length)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all P xs; i < length xs\<rbrakk> \<Longrightarrow> P (xs ! i)
theory Lib

lemma list_all_update:
  "\<lbrakk>list_all P xs; i < length xs; \<And>x. P x \<Longrightarrow> P (f x)\<rbrakk>
  \<Longrightarrow> list_all P (xs [i := f (xs ! i)])" by (metis length_list_update list_all_length nth_list_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all P xs; i < length xs; \<And>x. P x \<Longrightarrow> P (f x)\<rbrakk> \<Longrightarrow> list_all P (xs[i := f (xs ! i)])
theory Lib

lemma list_allI:
  "\<lbrakk>list_all P xs; \<And>x. P x \<Longrightarrow> P' x\<rbrakk> \<Longrightarrow> list_all P' xs" by (metis list_all_length)

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

lemma list_all_imp_filter2:
  "list_all (\<lambda>x. f x \<longrightarrow> g x) xs = list_all (\<lambda>x. \<not>f x) [x\<leftarrow>xs . (\<lambda>x. \<not>g x) x]" by (fastforce simp: Ball_set_list_all[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. list_all (\<lambda>x. f x \<longrightarrow> g x) xs = list_all (\<lambda>x. \<not> f x) (filter (\<lambda>x. \<not> g x) xs)
theory Lib

lemma list_all_imp_chain:
  "\<lbrakk>list_all (\<lambda>x. f x \<longrightarrow> g x) xs; list_all (\<lambda>x. f' x \<longrightarrow> f x) xs\<rbrakk>
  \<Longrightarrow>  list_all (\<lambda>x. f' x \<longrightarrow> g x) xs" by (clarsimp simp: Ball_set_list_all [symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>list_all (\<lambda>x. f x \<longrightarrow> g x) xs; list_all (\<lambda>x. f' x \<longrightarrow> f x) xs\<rbrakk> \<Longrightarrow> list_all (\<lambda>x. f' x \<longrightarrow> g x) xs
theory Lib

lemma inj_Pair:
  "inj_on (Pair x) S" by (rule inj_onI, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj_on (Pair x) S
theory Lib

lemma inj_on_split:
  "inj_on f S \<Longrightarrow> inj_on (\<lambda>x. (z, f x)) S" by (auto simp: inj_on_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. inj_on f S \<Longrightarrow> inj_on (\<lambda>x. (z, f x)) S
theory Lib

lemma split_state_strg:
  "(\<exists>x. f s = x \<and> P x s) \<longrightarrow> P (f s) s" by clarsimp

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

lemma theD:
  "\<lbrakk>the (f x) = y;  x \<in> dom f \<rbrakk> \<Longrightarrow> f x = Some y" by (auto simp add: dom_def)

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

lemma bspec_split:
  "\<lbrakk> \<forall>(a, b) \<in> S. P a b; (a, b) \<in> S \<rbrakk> \<Longrightarrow> P a b" by fastforce

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

lemma all_eq_trans:
  "\<lbrakk> \<forall>x. P x = Q x; \<forall>x. Q x = R x \<rbrakk> \<Longrightarrow> \<forall>x. P x = R x" by simp

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

lemma set_zip_same:
  "set (zip xs xs) = Id \<inter> (set xs \<times> set xs)" by (induct xs) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set (zip xs xs) = Restr Id (set xs)
theory Lib

lemma ball_ran_updI:
  "(\<forall>x \<in> ran m. P x) \<Longrightarrow> P v \<Longrightarrow> (\<forall>x \<in> ran (m (y \<mapsto> v)). P x)" by (auto simp add: ran_def)

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

lemma not_psubset_eq:
  "\<lbrakk> \<not> A \<subset> B; A \<subseteq> B \<rbrakk> \<Longrightarrow> A = B" by blast

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

lemma set_as_imp:
  "(A \<inter> P \<union> B \<inter> -P) = {s. (s \<in> P \<longrightarrow> s \<in> A) \<and> (s \<notin> P \<longrightarrow> s \<in> B)}" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. A \<inter> P \<union> B \<inter> - P = {s. (s \<in> P \<longrightarrow> s \<in> A) \<and> (s \<notin> P \<longrightarrow> s \<in> B)}
theory Lib

lemma in_image_op_plus:
  "(x + y \<in> (+) x ` S) = ((y :: 'a :: ring) \<in> S)" by (simp add: image_def)

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

lemma insert_subtract_new:
  "x \<notin> S \<Longrightarrow> (insert x S - S) = {x}" by auto

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

lemma minus_Suc_0_lt:
  "a \<noteq> 0 \<Longrightarrow> a - Suc 0 < a" by simp

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

lemma fst_last_zip_upt:
  "zip [0 ..< m] xs \<noteq> [] \<Longrightarrow>
   fst (last (zip [0 ..< m] xs)) = (if length xs < m then length xs - 1 else m - 1)" apply (subst last_conv_nth, assumption) apply (simp only: One_nat_def) apply (subst nth_zip; simp) apply (rule order_less_le_trans[OF minus_Suc_0_lt]; simp) apply (rule order_less_le_trans[OF minus_Suc_0_lt]; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zip [0..<m] xs \<noteq> [] \<Longrightarrow> fst (last (zip [0..<m] xs)) = (if length xs < m then length xs - 1 else m - 1) proof (prove)
goal (1 subgoal):
 1. zip [0..<m] xs \<noteq> [] \<Longrightarrow> fst (zip [0..<m] xs ! (length (zip [0..<m] xs) - 1)) = (if length xs < m then length xs - 1 else m - 1) proof (prove)
goal (1 subgoal):
 1. zip [0..<m] xs \<noteq> [] \<Longrightarrow> fst (zip [0..<m] xs ! (length (zip [0..<m] xs) - Suc 0)) = (if length xs < m then length xs - Suc 0 else m - Suc 0) proof (prove)
goal (2 subgoals):
 1. 0 < m \<and> xs \<noteq> [] \<Longrightarrow> min m (length xs) - Suc 0 < m
 2. 0 < m \<and> xs \<noteq> [] \<Longrightarrow> min m (length xs) - Suc 0 < length xs proof (prove)
goal (1 subgoal):
 1. 0 < m \<and> xs \<noteq> [] \<Longrightarrow> min m (length xs) - Suc 0 < length xs proof (prove)
goal:
No subgoals!
theory Lib

lemma neq_into_nprefix:
  "\<lbrakk> x \<noteq> take (length x) y \<rbrakk> \<Longrightarrow> \<not> x \<le> y" by (clarsimp simp: prefix_def less_eq_list_def)

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

lemma suffix_eqI:
  "\<lbrakk> suffix xs as; suffix xs bs; length as = length bs;
    take (length as - length xs) as \<le> take (length bs - length xs) bs\<rbrakk> \<Longrightarrow> as = bs" by (clarsimp elim!: prefixE suffixE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>suffix xs as; suffix xs bs; length as = length bs; take (length as - length xs) as \<le> take (length bs - length xs) bs\<rbrakk> \<Longrightarrow> as = bs
theory Lib

lemma distinct_imply_not_in_tail:
  "\<lbrakk> distinct list; suffix (y # ys) list\<rbrakk> \<Longrightarrow> y \<notin> set ys" by (clarsimp simp:suffix_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct list; suffix (y # ys) list\<rbrakk> \<Longrightarrow> y \<notin> set ys
theory Lib

lemma list_induct_suffix [case_names Nil Cons]:
  assumes nilr: "P []"
  and    consr: "\<And>x xs. \<lbrakk>P xs; suffix (x # xs) as \<rbrakk> \<Longrightarrow> P (x # xs)"
  shows  "P as" proof - define as' where "as' == as" have "suffix as as'" unfolding as'_def by simp then show ?thesis proof (induct as) case Nil show ?case by fact next case (Cons x xs) show ?case proof (rule consr) from Cons.prems show "suffix (x # xs) as" unfolding as'_def . then have "suffix xs as'" by (auto dest: suffix_ConsD simp: as'_def) then show "P xs" using Cons.hyps by simp qed qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P as proof (state)
goal (1 subgoal):
 1. P as proof (state)
this:
as' \<equiv> as

goal (1 subgoal):
 1. P as proof (prove)
goal (1 subgoal):
 1. suffix as as' proof (prove)
goal (1 subgoal):
 1. suffix as as proof (state)
this:
suffix as as'

goal (1 subgoal):
 1. P as proof (chain)
picking this:
suffix as as' proof (prove)
using this:
suffix as as'

goal (1 subgoal):
 1. P as proof (state)
goal (2 subgoals):
 1. suffix [] as' \<Longrightarrow> P []
 2. \<And>a as. \<lbrakk>suffix as as' \<Longrightarrow> P as; suffix (a # as) as'\<rbrakk> \<Longrightarrow> P (a # as) proof (state)
this:
suffix [] as'

goal (2 subgoals):
 1. suffix [] as' \<Longrightarrow> P []
 2. \<And>a as. \<lbrakk>suffix as as' \<Longrightarrow> P as; suffix (a # as) as'\<rbrakk> \<Longrightarrow> P (a # as) proof (prove)
goal (1 subgoal):
 1. P [] proof (state)
this:
P []

goal (1 subgoal):
 1. \<And>a as. \<lbrakk>suffix as as' \<Longrightarrow> P as; suffix (a # as) as'\<rbrakk> \<Longrightarrow> P (a # as) proof (state)
goal (1 subgoal):
 1. \<And>a as. \<lbrakk>suffix as as' \<Longrightarrow> P as; suffix (a # as) as'\<rbrakk> \<Longrightarrow> P (a # as) proof (state)
this:
suffix xs as' \<Longrightarrow> P xs
suffix (x # xs) as'

goal (1 subgoal):
 1. \<And>a as. \<lbrakk>suffix as as' \<Longrightarrow> P as; suffix (a # as) as'\<rbrakk> \<Longrightarrow> P (a # as) proof (prove)
goal (1 subgoal):
 1. P (x # xs) proof (state)
goal (2 subgoals):
 1. P xs
 2. suffix (x # xs) as proof (chain)
picking this:
suffix (x # xs) as' proof (prove)
using this:
suffix (x # xs) as'

goal (1 subgoal):
 1. suffix (x # xs) as proof (prove)
using this:
suffix (x # xs) as

goal (1 subgoal):
 1. suffix (x # xs) as proof (state)
this:
suffix (x # xs) as

goal (1 subgoal):
 1. P xs proof (chain)
picking this:
suffix (x # xs) as proof (prove)
using this:
suffix (x # xs) as

goal (1 subgoal):
 1. suffix xs as' proof (state)
this:
suffix xs as'

goal (1 subgoal):
 1. P xs proof (chain)
picking this:
suffix xs as' proof (prove)
using this:
suffix xs as'

goal (1 subgoal):
 1. P xs proof (prove)
using this:
suffix xs as'
suffix xs as' \<Longrightarrow> P xs

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

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

goal:
No subgoals! proof (state)
this:
P as

goal:
No subgoals!