kings-crown/FVELER_Isabelle huggingface dataset:
theory Machine_Word_32

lemma unat_less_2p_word_bits:
  "unat (x :: machine_word) < 2 ^ word_bits" apply (simp only: word_bits_def) apply (rule unat_lt2p) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat x < 2 ^ word_bits proof (prove)
goal (1 subgoal):
 1. unat x < 2 ^ LENGTH(32) proof (prove)
goal:
No subgoals!
theory Machine_Word_32

lemma unat_less_word_bits:
  fixes y :: machine_word
  shows "x < unat y \<Longrightarrow> x < 2 ^ word_bits" unfolding word_bits_def by (rule order_less_trans [OF _ unat_lt2p])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < unat y \<Longrightarrow> x < 2 ^ word_bits proof (prove)
goal (1 subgoal):
 1. x < unat y \<Longrightarrow> x < 2 ^ LENGTH(32)
theory Machine_Word_32

lemma unat_mask_2_less_4:
  "unat (p AND mask 2 :: machine_word) < 4" by (rule unat_less_helper) (simp only: take_bit_eq_mod word_mod_less_divisor flip: take_bit_eq_mask, simp add: word_mod_less_divisor)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (p && mask 2) < 4
theory Machine_Word_32

lemma unat_mult_simple:
  \<open>unat (x * y) = unat x * unat y\<close>
    if \<open>unat x * unat y < 2 ^ LENGTH(machine_word_len)\<close>
    for x y :: machine_word using that by (simp flip: unat_mult_lem)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (x * y) = unat x * unat y proof (prove)
using this:
unat x * unat y < 2 ^ LENGTH(32)

goal (1 subgoal):
 1. unat (x * y) = unat x * unat y
theory Machine_Word_32

lemma upto_2_helper:
  "{0..<2 :: machine_word} = {0, 1}" by (safe; simp) unat_arith

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. {0..<2} = {0, 1}
theory Machine_Word_32

lemma word_ge_min:
  \<open>- (2 ^ (word_bits - 1)) \<le> sint x\<close> for x :: machine_word using sint_ge [of x] by (simp add: word_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. - (2 ^ (word_bits - 1)) \<le> sint x proof (prove)
using this:
- (2 ^ (LENGTH(32) - 1)) \<le> sint x

goal (1 subgoal):
 1. - (2 ^ (word_bits - 1)) \<le> sint x
theory Machine_Word_32

lemma word_rsplit_0:
  "word_rsplit (0::machine_word) = [0, 0, 0, (0::8 word)]" by (simp add: word_rsplit_def bin_rsplit_def word_bits_def word_size_def Cons_replicate_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_rsplit 0 = [0, 0, 0, 0]
theory Word_Lemmas_32_Internal

lemma zero_le_sint_32:
  "\<lbrakk> 0 \<le> (a :: word32); a < 0x80000000 \<rbrakk>
   \<Longrightarrow> 0 \<le> sint a" by (clarsimp simp: sint_eq_uint_32 unat_less_helper)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 \<le> a; a < 0x80000000\<rbrakk> \<Longrightarrow> 0 \<le> sint a
theory Word_Lemmas_32_Internal

lemma upto_enum_inc_1:
  "a < 2 ^ word_bits - 1
   \<Longrightarrow> [(0:: 'a :: len word) .e. 1 + a] = [0.e.a] @ [(1+a)]" using upper_trivial upto_enum_inc_1_len by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. a < 2 ^ word_bits - 1 \<Longrightarrow> [0 .e. 1 + a] = [0 .e. a] @ [1 + a] proof (prove)
using this:
?x \<noteq> 2 ^ LENGTH(?'a) - 1 \<Longrightarrow> ?x < 2 ^ LENGTH(?'a) - 1
?a < - 1 \<Longrightarrow> [0 .e. 1 + ?a] = [0 .e. ?a] @ [1 + ?a]

goal (1 subgoal):
 1. a < 2 ^ word_bits - 1 \<Longrightarrow> [0 .e. 1 + a] = [0 .e. a] @ [1 + a]
theory Word_Lemmas_32_Internal

lemma le_32_mask_eq:
  "(bits :: word32) \<le> 32 \<Longrightarrow> bits && mask 6 = bits" by (fastforce elim: le_less_trans intro: less_mask_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bits \<le> 0x20 \<Longrightarrow> bits && mask 6 = bits
theory Word_Lemmas_32_Internal

lemma mask_eq1_nochoice:
  "(x :: word32) && 1 = x
   \<Longrightarrow> x = 0 \<or> x = 1" using mask_eq1_nochoice len32 by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x && 1 = x \<Longrightarrow> x = 0 \<or> x = 1 proof (prove)
using this:
\<lbrakk>1 < LENGTH(?'a); ?x && 1 = ?x\<rbrakk> \<Longrightarrow> ?x = 0 \<or> ?x = 1
len_of ?x = 32

goal (1 subgoal):
 1. x && 1 = x \<Longrightarrow> x = 0 \<or> x = 1
theory Word_Lemmas_32_Internal

lemma word_log2_max_word32[simp]:
  "word_log2 (w :: 32 word) < 32" using word_log2_max[where w=w] by (simp add: word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_log2 w < 32 proof (prove)
using this:
word_log2 w < size w

goal (1 subgoal):
 1. word_log2 w < 32
theory Word_Lemmas_32_Internal

lemma mapping_two_power_16_64_inequality:
  assumes sz: "sz \<le> 4" and len: "unat (len :: word32) = 2 ^ sz"
  shows "unat (len * 8 - 1) \<le> 127" using pow_sub_less[where 'a=32 and b=3, simplified] proof - have len2: "len = 2 ^ sz" apply (rule word_unat.Rep_eqD, simp only: len) using sz apply simp done show ?thesis using two_power_increasing_less_1[where 'a=32 and n="sz + 3" and m=7] by (simp add: word_le_nat_alt sz power_add len2 field_simps bintrunc_Suc_numeral) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (len * 8 - 1) \<le> 127 proof (prove)
using this:
\<lbrakk>?a \<le> 29; unat ?x = 2 ^ ?a\<rbrakk> \<Longrightarrow> unat (?x * 8 - 1) < 2 ^ (?a + 3)

goal (1 subgoal):
 1. unat (len * 8 - 1) \<le> 127 proof (state)
goal (1 subgoal):
 1. (\<And>a x. \<lbrakk>a \<le> 29; unat x = 2 ^ a\<rbrakk> \<Longrightarrow> unat (x * 8 - 1) < 2 ^ (a + 3)) \<Longrightarrow> unat (len * 8 - 1) \<le> 127 proof (prove)
goal (1 subgoal):
 1. len = 2 ^ sz proof (prove)
goal (1 subgoal):
 1. 2 ^ sz = unat (2 ^ sz) proof (prove)
using this:
sz \<le> 4

goal (1 subgoal):
 1. 2 ^ sz = unat (2 ^ sz) proof (prove)
goal:
No subgoals! proof (state)
this:
len = 2 ^ sz

goal (1 subgoal):
 1. (\<And>a x. \<lbrakk>a \<le> 29; unat x = 2 ^ a\<rbrakk> \<Longrightarrow> unat (x * 8 - 1) < 2 ^ (a + 3)) \<Longrightarrow> unat (len * 8 - 1) \<le> 127 proof (prove)
goal (1 subgoal):
 1. unat (len * 8 - 1) \<le> 127 proof (prove)
using this:
\<lbrakk>sz + 3 \<le> 7; 7 \<le> LENGTH(32)\<rbrakk> \<Longrightarrow> 2 ^ (sz + 3) - 1 \<le> 2 ^ 7 - 1

goal (1 subgoal):
 1. unat (len * 8 - 1) \<le> 127 proof (state)
this:
unat (len * 8 - 1) \<le> 127

goal:
No subgoals!
theory Word_Lemmas_32_Internal

lemma scast_mask_8:
  "scast (mask 8 :: sword32) = (mask 8 :: word32)" by (clarsimp simp: mask_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. SCAST(32 signed \<rightarrow> 32) (mask 8) = mask 8
theory Word_Lemmas_32_Internal

lemma signed_unat_minus_one_32:
  "unat (-1 :: 32 signed word) = 4294967295" by (simp del: word_pow_0 diff_0 add: unat_sub_if' minus_one_word)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (- 1) = 4294967295
theory Word_Lemmas_32_Internal

lemma neq_0_unat: "x \<noteq> 0 \<Longrightarrow> 0 < unat x" for x::machine_word by (simp add: unat_gt_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<noteq> 0 \<Longrightarrow> 0 < unat x
theory Distinct_Prop

lemma distinct_prop_map:
  "distinct_prop P (map f xs) = distinct_prop (\<lambda>x y. P (f x) (f y)) xs" by (induct xs) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct_prop P (map f xs) = distinct_prop (\<lambda>x y. P (f x) (f y)) xs
theory Distinct_Prop

lemma distinct_prop_append:
  "distinct_prop P (xs @ ys) =
    (distinct_prop P xs \<and> distinct_prop P ys \<and> (\<forall>x \<in> set xs. \<forall>y \<in> set ys. P x y))" by (induct xs arbitrary: ys) (auto simp: conj_comms ball_Un)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct_prop P (xs @ ys) = (distinct_prop P xs \<and> distinct_prop P ys \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set ys. P x y))
theory Distinct_Prop

lemma distinct_prop_distinct:
  "\<lbrakk> distinct xs; \<And>x y. \<lbrakk> x \<in> set xs; y \<in> set xs; x \<noteq> y \<rbrakk> \<Longrightarrow> P x y \<rbrakk> \<Longrightarrow> distinct_prop P xs" by (induct xs) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; \<And>x y. \<lbrakk>x \<in> set xs; y \<in> set xs; x \<noteq> y\<rbrakk> \<Longrightarrow> P x y\<rbrakk> \<Longrightarrow> distinct_prop P xs
theory Distinct_Prop

lemma distinct_prop_True [simp]:
  "distinct_prop (\<lambda>x y. True) xs" by (induct xs, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct_prop (\<lambda>x y. True) xs
theory Distinct_Prop

lemma distinct_prefix:
  "\<lbrakk> distinct xs; ys \<le> xs \<rbrakk> \<Longrightarrow> distinct ys" apply (induct xs arbitrary: ys; clarsimp) apply (case_tac ys; clarsimp) by (fastforce simp: less_eq_list_def dest: set_mono_prefix)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct xs; ys \<le> xs\<rbrakk> \<Longrightarrow> distinct ys proof (prove)
goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. ys \<le> xs \<Longrightarrow> distinct ys; a \<notin> set xs; ys \<le> a # xs\<rbrakk> \<Longrightarrow> distinct ys proof (prove)
goal (1 subgoal):
 1. \<And>a xs list. \<lbrakk>\<And>ys. ys \<le> xs \<Longrightarrow> distinct ys; a \<notin> set xs; list \<le> xs; a \<in> set list\<rbrakk> \<Longrightarrow> False
theory Distinct_Prop

lemma distinct_sets_prop:
  "distinct_sets xs = distinct_prop (\<lambda>x y. x \<inter> y = {}) xs" by (induct xs) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct_sets xs = distinct_prop (\<lambda>x y. x \<inter> y = {}) xs
theory Distinct_Prop

lemma distinct_take_strg:
  "distinct xs \<longrightarrow> distinct (take n xs)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct xs \<longrightarrow> distinct (take n xs)
theory Distinct_Prop

lemma distinct_prop_prefixE:
  "\<lbrakk> distinct_prop P ys; prefix xs ys \<rbrakk> \<Longrightarrow> distinct_prop P xs" apply (induct xs arbitrary: ys; clarsimp) apply (case_tac ys; clarsimp) by (fastforce dest: set_mono_prefix)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_prop P ys; prefix xs ys\<rbrakk> \<Longrightarrow> distinct_prop P xs proof (prove)
goal (1 subgoal):
 1. \<And>a xs ys. \<lbrakk>\<And>ys. \<lbrakk>distinct_prop P ys; prefix xs ys\<rbrakk> \<Longrightarrow> distinct_prop P xs; distinct_prop P ys; prefix (a # xs) ys\<rbrakk> \<Longrightarrow> (\<forall>y\<in>set xs. P a y) \<and> distinct_prop P xs proof (prove)
goal (1 subgoal):
 1. \<And>a xs list x. \<lbrakk>\<And>ys. \<lbrakk>distinct_prop P ys; prefix xs ys\<rbrakk> \<Longrightarrow> distinct_prop P xs; prefix xs list; \<forall>x\<in>set list. P a x; distinct_prop P list; x \<in> set xs\<rbrakk> \<Longrightarrow> P a x
theory Distinct_Prop

lemma distinct_sets_union_sub:
  "\<lbrakk>x \<in> A; distinct_sets [A,B]\<rbrakk> \<Longrightarrow> A \<union> B - {x} = A - {x} \<union> B" by (auto simp: distinct_sets_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> A; distinct_sets [A, B]\<rbrakk> \<Longrightarrow> A \<union> B - {x} = A - {x} \<union> B
theory Distinct_Prop

lemma distinct_sets_append1:
  "distinct_sets (xs @ ys) \<Longrightarrow> distinct_sets xs" by (drule distinct_sets_append, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct_sets (xs @ ys) \<Longrightarrow> distinct_sets xs
theory Distinct_Prop

lemma distinct_sets_append2:
  "distinct_sets (xs @ ys) \<Longrightarrow> distinct_sets ys" by (drule distinct_sets_append, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct_sets (xs @ ys) \<Longrightarrow> distinct_sets ys
theory Distinct_Prop

lemma distinct_sets_append_Cons:
  "distinct_sets (xs @ a # ys) \<Longrightarrow> distinct_sets (xs @ ys)" apply (subst distinct_sets_prop)+ apply (subst (asm) distinct_sets_prop) apply (subst distinct_prop_append) apply (subst (asm) distinct_prop_append) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct_sets (xs @ a # ys) \<Longrightarrow> distinct_sets (xs @ ys) proof (prove)
goal (1 subgoal):
 1. distinct_sets (xs @ a # ys) \<Longrightarrow> distinct_prop (\<lambda>x y. x \<inter> y = {}) (xs @ ys) proof (prove)
goal (1 subgoal):
 1. distinct_prop (\<lambda>x y. x \<inter> y = {}) (xs @ a # ys) \<Longrightarrow> distinct_prop (\<lambda>x y. x \<inter> y = {}) (xs @ ys) proof (prove)
goal (1 subgoal):
 1. distinct_prop (\<lambda>x y. x \<inter> y = {}) (xs @ a # ys) \<Longrightarrow> distinct_prop (\<lambda>x y. x \<inter> y = {}) xs \<and> distinct_prop (\<lambda>x y. x \<inter> y = {}) ys \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set ys. x \<inter> y = {}) proof (prove)
goal (1 subgoal):
 1. distinct_prop (\<lambda>x y. x \<inter> y = {}) xs \<and> distinct_prop (\<lambda>x y. x \<inter> y = {}) (a # ys) \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set (a # ys). x \<inter> y = {}) \<Longrightarrow> distinct_prop (\<lambda>x y. x \<inter> y = {}) xs \<and> distinct_prop (\<lambda>x y. x \<inter> y = {}) ys \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set ys. x \<inter> y = {}) proof (prove)
goal:
No subgoals!
theory Distinct_Prop

lemma distinct_sets_append_Cons_disjoint:
  "distinct_sets (xs @ a # ys) \<Longrightarrow>  a \<inter> \<Union> (set xs) = {} " apply (subst (asm) distinct_sets_prop) apply (subst (asm) distinct_prop_append) apply (subst Int_commute) apply (subst Union_disjoint) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct_sets (xs @ a # ys) \<Longrightarrow> a \<inter> \<Union> (set xs) = {} proof (prove)
goal (1 subgoal):
 1. distinct_prop (\<lambda>x y. x \<inter> y = {}) (xs @ a # ys) \<Longrightarrow> a \<inter> \<Union> (set xs) = {} proof (prove)
goal (1 subgoal):
 1. distinct_prop (\<lambda>x y. x \<inter> y = {}) xs \<and> distinct_prop (\<lambda>x y. x \<inter> y = {}) (a # ys) \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set (a # ys). x \<inter> y = {}) \<Longrightarrow> a \<inter> \<Union> (set xs) = {} proof (prove)
goal (1 subgoal):
 1. distinct_prop (\<lambda>x y. x \<inter> y = {}) xs \<and> distinct_prop (\<lambda>x y. x \<inter> y = {}) (a # ys) \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set (a # ys). x \<inter> y = {}) \<Longrightarrow> \<Union> (set xs) \<inter> a = {} proof (prove)
goal (1 subgoal):
 1. distinct_prop (\<lambda>x y. x \<inter> y = {}) xs \<and> distinct_prop (\<lambda>x y. x \<inter> y = {}) (a # ys) \<and> (\<forall>x\<in>set xs. \<forall>y\<in>set (a # ys). x \<inter> y = {}) \<Longrightarrow> \<forall>B\<in>set xs. B \<inter> a = {} proof (prove)
goal:
No subgoals!
theory Distinct_Prop

lemma distinct_prop_take:
  "\<lbrakk>distinct_prop P xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_prop P (take i xs)" by (metis take_is_prefix distinct_prop_prefixE)

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

lemma distinct_sets_take:
  "\<lbrakk>distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (take i xs)" by (simp add: distinct_sets_prop distinct_prop_take)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (take i xs)
theory Distinct_Prop

lemma distinct_prop_take_Suc:
  "\<lbrakk>distinct_prop P xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_prop P (take (Suc i) xs)" by (metis distinct_prop_take not_less take_all)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_prop P xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_prop P (take (Suc i) xs)
theory Distinct_Prop

lemma distinct_prop_rev:
  "distinct_prop P (rev xs) = distinct_prop (\<lambda>y x. P x y) xs" by (induct xs) (auto simp: distinct_prop_append)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct_prop P (rev xs) = distinct_prop (\<lambda>y x. P x y) xs
theory Distinct_Prop

lemma distinct_sets_rev [simp]:
  "distinct_sets (rev xs) = distinct_sets xs" apply (unfold distinct_sets_prop) apply (subst distinct_prop_rev) apply (subst Int_commute) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct_sets (rev xs) = distinct_sets xs proof (prove)
goal (1 subgoal):
 1. distinct_prop (\<lambda>x y. x \<inter> y = {}) (rev xs) = distinct_prop (\<lambda>x y. x \<inter> y = {}) xs proof (prove)
goal (1 subgoal):
 1. distinct_prop (\<lambda>y x. x \<inter> y = {}) xs = distinct_prop (\<lambda>x y. x \<inter> y = {}) xs proof (prove)
goal (1 subgoal):
 1. distinct_prop (\<lambda>y x. y \<inter> x = {}) xs = distinct_prop (\<lambda>x y. x \<inter> y = {}) xs proof (prove)
goal:
No subgoals!
theory Distinct_Prop

lemma distinct_sets_drop:
  "\<lbrakk>distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (drop i xs)" apply (cases "i=0", simp) apply (subst distinct_sets_rev [symmetric]) apply (subst rev_drop) apply (subst distinct_sets_take, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (drop i xs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_sets xs; i < length xs; i \<noteq> 0\<rbrakk> \<Longrightarrow> distinct_sets (drop i xs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_sets xs; i < length xs; i \<noteq> 0\<rbrakk> \<Longrightarrow> distinct_sets (rev (drop i xs)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_sets xs; i < length xs; i \<noteq> 0\<rbrakk> \<Longrightarrow> distinct_sets (take (length xs - i) (rev xs)) proof (prove)
goal:
No subgoals!
theory Distinct_Prop

lemma distinct_sets_drop_Suc:
  "\<lbrakk>distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (drop (Suc i) xs)" apply (subst distinct_sets_rev [symmetric]) apply (subst rev_drop) apply (subst distinct_sets_take, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (drop (Suc i) xs) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (rev (drop (Suc i) xs)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_sets xs; i < length xs\<rbrakk> \<Longrightarrow> distinct_sets (take (length xs - Suc i) (rev xs)) proof (prove)
goal:
No subgoals!
theory Distinct_Prop

lemma distinct_sets_take_nth:
  "\<lbrakk>distinct_sets xs; i < length xs; x \<in> set (take i xs)\<rbrakk> \<Longrightarrow> x \<inter> xs ! i = {}" apply (drule (1) distinct_sets_take_Suc) apply (subst (asm) take_Suc_conv_app_nth, assumption) apply (unfold distinct_sets_prop) apply (subst (asm) distinct_prop_append) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_sets xs; i < length xs; x \<in> set (take i xs)\<rbrakk> \<Longrightarrow> x \<inter> xs ! i = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length xs; x \<in> set (take i xs); distinct_sets (take (Suc i) xs)\<rbrakk> \<Longrightarrow> x \<inter> xs ! i = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length xs; x \<in> set (take i xs); distinct_sets (take i xs @ [xs ! i])\<rbrakk> \<Longrightarrow> x \<inter> xs ! i = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length xs; x \<in> set (take i xs); distinct_prop (\<lambda>x y. x \<inter> y = {}) (take i xs @ [xs ! i])\<rbrakk> \<Longrightarrow> x \<inter> xs ! i = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length xs; x \<in> set (take i xs); distinct_prop (\<lambda>x y. x \<inter> y = {}) (take i xs) \<and> distinct_prop (\<lambda>x y. x \<inter> y = {}) [xs ! i] \<and> (\<forall>x\<in>set (take i xs). \<forall>y\<in>set [xs ! i]. x \<inter> y = {})\<rbrakk> \<Longrightarrow> x \<inter> xs ! i = {} proof (prove)
goal:
No subgoals!
theory Distinct_Prop

lemma distinct_sets_append_distinct:
  "\<lbrakk>x \<in> set xs; y \<in> set ys; distinct_sets (xs @ ys)\<rbrakk> \<Longrightarrow> x \<inter> y = {}" unfolding distinct_sets_prop by (clarsimp simp: distinct_prop_append)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set xs; y \<in> set ys; distinct_sets (xs @ ys)\<rbrakk> \<Longrightarrow> x \<inter> y = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x \<in> set xs; y \<in> set ys; distinct_prop (\<lambda>x y. x \<inter> y = {}) (xs @ ys)\<rbrakk> \<Longrightarrow> x \<inter> y = {}
theory Distinct_Prop

lemma distinct_sets_map_update:
  "\<lbrakk>distinct_sets (map f xs); i < length xs; f a \<subseteq> f(xs ! i)\<rbrakk>
  \<Longrightarrow> distinct_sets (map f (xs[i := a]))" by (metis distinct_sets_update length_map map_update nth_map)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>distinct_sets (map f xs); i < length xs; f a \<subseteq> f (xs ! i)\<rbrakk> \<Longrightarrow> distinct_sets (map f (xs[i := a]))
theory Distinct_Prop

lemma Union_list_update:
  "\<lbrakk>i < length xs; distinct_sets (map f xs)\<rbrakk>
  \<Longrightarrow> (\<Union>x\<in>set (xs [i := a]). f x) = (\<Union>x\<in>set xs. f x) - f (xs ! i) \<union> f a" apply (induct xs arbitrary: i; clarsimp) apply (case_tac i; (clarsimp, fastforce)) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < length xs; distinct_sets (map f xs)\<rbrakk> \<Longrightarrow> \<Union> (f ` set (xs[i := a])) = \<Union> (f ` set xs) - f (xs ! i) \<union> f a proof (prove)
goal (1 subgoal):
 1. \<And>aa xs i. \<lbrakk>\<And>i. i < length xs \<Longrightarrow> \<Union> (f ` set (xs[i := a])) = \<Union> (f ` set xs) - f (xs ! i) \<union> f a; i < Suc (length xs); f aa \<inter> \<Union> (f ` set xs) = {}; distinct_sets (map f xs)\<rbrakk> \<Longrightarrow> \<Union> (f ` set (case i of 0 \<Rightarrow> a # xs | Suc j \<Rightarrow> aa # xs[j := a])) = f aa \<union> \<Union> (f ` set xs) - f ((aa # xs) ! i) \<union> f a proof (prove)
goal:
No subgoals!
theory Distinct_Prop

lemma fst_enumerate:
  "i < length xs \<Longrightarrow> fst (enumerate n xs ! i) = i + n" by (metis add.commute fst_conv nth_enumerate_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i < length xs \<Longrightarrow> fst (enumerate n xs ! i) = i + n
theory Distinct_Prop

lemma snd_enumerate:
  "i < length xs \<Longrightarrow> snd (enumerate n xs ! i) = xs ! i" by (metis nth_enumerate_eq snd_conv)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i < length xs \<Longrightarrow> snd (enumerate n xs ! i) = xs ! i
theory Distinct_Prop

lemma enumerate_member:
  assumes "i < length xs"
  shows "(n + i, xs ! i) \<in> set (enumerate n xs)" proof - have pair_unpack: "\<And>a b x. ((a, b) = x) = (a = fst x \<and> b = snd x)" by fastforce from assms have "(n + i, xs ! i) = enumerate n xs ! i" by (auto simp: fst_enumerate snd_enumerate pair_unpack) with assms show ?thesis by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (n + i, xs ! i) \<in> set (enumerate n xs) proof (state)
goal (1 subgoal):
 1. (n + i, xs ! i) \<in> set (enumerate n xs) proof (prove)
goal (1 subgoal):
 1. \<And>a b x. ((a, b) = x) = (a = fst x \<and> b = snd x) proof (state)
this:
((?a, ?b) = ?x) = (?a = fst ?x \<and> ?b = snd ?x)

goal (1 subgoal):
 1. (n + i, xs ! i) \<in> set (enumerate n xs) proof (chain)
picking this:
i < length xs proof (prove)
using this:
i < length xs

goal (1 subgoal):
 1. (n + i, xs ! i) = enumerate n xs ! i proof (state)
this:
(n + i, xs ! i) = enumerate n xs ! i

goal (1 subgoal):
 1. (n + i, xs ! i) \<in> set (enumerate n xs) proof (chain)
picking this:
i < length xs
(n + i, xs ! i) = enumerate n xs ! i proof (prove)
using this:
i < length xs
(n + i, xs ! i) = enumerate n xs ! i

goal (1 subgoal):
 1. (n + i, xs ! i) \<in> set (enumerate n xs) proof (state)
this:
(n + i, xs ! i) \<in> set (enumerate n xs)

goal:
No subgoals!