kings-crown/FVELER_Isabelle huggingface dataset:
theory Enumeration_Word

lemma upto_enum_red2:
  assumes szv: "sz < LENGTH('a :: len)"
  shows "[(0:: 'a :: len word) .e. 2 ^ sz - 1] =
  map of_nat [0 ..< 2 ^ sz]" using szv apply (subst unat_power_lower[OF szv, symmetric]) apply (rule upto_enum_red') apply (subst word_le_nat_alt, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. [0 .e. 2 ^ sz - 1] = map word_of_nat [0..<2 ^ sz] proof (prove)
using this:
sz < LENGTH('a)

goal (1 subgoal):
 1. [0 .e. 2 ^ sz - 1] = map word_of_nat [0..<2 ^ sz] proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> [0 .e. 2 ^ sz - 1] = map word_of_nat [0..<unat (2 ^ sz)] proof (prove)
goal (1 subgoal):
 1. sz < LENGTH('a) \<Longrightarrow> 1 \<le> 2 ^ sz proof (prove)
goal:
No subgoals!
theory Enumeration_Word

lemma upto_enum_word:
  "[x .e. y] = map of_nat [unat x ..< Suc (unat y)]" apply (subst upto_enum_red) apply clarsimp apply (subst toEnum_of_nat) prefer 2 apply (rule refl) apply (erule disjE, simp) apply clarsimp apply (erule order_less_trans) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. [x .e. y] = map word_of_nat [unat x..<Suc (unat y)] proof (prove)
goal (1 subgoal):
 1. map toEnum [fromEnum x..<Suc (fromEnum y)] = map word_of_nat [unat x..<Suc (unat y)] proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>unat x \<le> unat y; xa = unat y \<or> unat x \<le> xa \<and> xa < unat y\<rbrakk> \<Longrightarrow> toEnum xa = word_of_nat xa proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>unat x \<le> unat y; xa = unat y \<or> unat x \<le> xa \<and> xa < unat y\<rbrakk> \<Longrightarrow> xa < 2 ^ LENGTH('a)
 2. \<And>xa. \<lbrakk>unat x \<le> unat y; xa = unat y \<or> unat x \<le> xa \<and> xa < unat y\<rbrakk> \<Longrightarrow> word_of_nat xa = word_of_nat xa proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrakk>unat x \<le> unat y; xa = unat y \<or> unat x \<le> xa \<and> xa < unat y\<rbrakk> \<Longrightarrow> word_of_nat xa = word_of_nat xa
 2. \<And>xa. \<lbrakk>unat x \<le> unat y; xa = unat y \<or> unat x \<le> xa \<and> xa < unat y\<rbrakk> \<Longrightarrow> xa < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>unat x \<le> unat y; xa = unat y \<or> unat x \<le> xa \<and> xa < unat y\<rbrakk> \<Longrightarrow> xa < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>unat x \<le> unat y; unat x \<le> xa \<and> xa < unat y\<rbrakk> \<Longrightarrow> xa < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>unat x \<le> xa; xa < unat y\<rbrakk> \<Longrightarrow> xa < 2 ^ LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<And>xa. unat x \<le> xa \<Longrightarrow> unat y < 2 ^ LENGTH('a) proof (prove)
goal:
No subgoals!
theory Enumeration_Word

lemma word_upto_Cons_eq:
  "x < y \<Longrightarrow> [x::'a::len word .e. y] = x # [x + 1 .e. y]" apply (subst upto_enum_red) apply (subst upt_conv_Cons) apply simp_all apply unat_arith apply (simp only: list.map list.inject upto_enum_red to_from_enum simp_thms) apply simp_all apply unat_arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < y \<Longrightarrow> [x .e. y] = x # [x + 1 .e. y] proof (prove)
goal (1 subgoal):
 1. x < y \<Longrightarrow> map toEnum [fromEnum x..<Suc (fromEnum y)] = x # [x + 1 .e. y] proof (prove)
goal (2 subgoals):
 1. x < y \<Longrightarrow> fromEnum x < Suc (fromEnum y)
 2. x < y \<Longrightarrow> map toEnum (fromEnum x # [Suc (fromEnum x)..<Suc (fromEnum y)]) = x # [x + 1 .e. y] proof (prove)
goal (2 subgoals):
 1. x < y \<Longrightarrow> unat x < Suc (unat y)
 2. x < y \<Longrightarrow> (Suc (unat x) \<le> unat y \<longrightarrow> map toEnum [Suc (unat x)..<unat y] @ [y] = [x + 1 .e. y]) \<and> (\<not> Suc (unat x) \<le> unat y \<longrightarrow> [] = [x + 1 .e. y]) proof (prove)
goal (1 subgoal):
 1. x < y \<Longrightarrow> (Suc (unat x) \<le> unat y \<longrightarrow> map toEnum [Suc (unat x)..<unat y] @ [y] = [x + 1 .e. y]) \<and> (\<not> Suc (unat x) \<le> unat y \<longrightarrow> [] = [x + 1 .e. y]) proof (prove)
goal (1 subgoal):
 1. x < y \<Longrightarrow> (Suc (unat x) \<le> unat y \<longrightarrow> map toEnum [Suc (unat x)..<unat y] @ [y] = map toEnum [fromEnum (x + 1)..<Suc (fromEnum y)]) \<and> (\<not> Suc (unat x) \<le> unat y \<longrightarrow> [] = map toEnum [fromEnum (x + 1)..<Suc (fromEnum y)]) proof (prove)
goal (1 subgoal):
 1. x < y \<Longrightarrow> (unat (x + 1) \<le> unat y \<longrightarrow> (Suc (unat x) \<le> unat y \<longrightarrow> map toEnum [Suc (unat x)..<unat y] = map toEnum [unat (x + 1)..<unat y]) \<and> Suc (unat x) \<le> unat y) \<and> (\<not> unat (x + 1) \<le> unat y \<longrightarrow> \<not> Suc (unat x) \<le> unat y) proof (prove)
goal:
No subgoals!
theory Enumeration_Word

lemma distinct_enum_upto:
  "distinct [(0 :: 'a::len word) .e. b]" proof - have "\<And>(b::'a word). [0 .e. b] = nths enum {..< Suc (fromEnum b)}" apply (subst upto_enum_red) apply (subst nths_upt_eq_take) apply (subst enum_word_def) apply (subst take_map) apply (subst take_upt) apply (simp only: add_0 fromEnum_unat) apply (rule order_trans [OF _ order_eq_refl]) apply (rule Suc_leI [OF unat_lt2p]) apply simp apply clarsimp apply (rule toEnum_of_nat) apply (erule order_less_trans [OF _ unat_lt2p]) done then show ?thesis by (rule ssubst) (rule distinct_nthsI, simp) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct [0 .e. b] proof (state)
goal (1 subgoal):
 1. distinct [0 .e. b] proof (prove)
goal (1 subgoal):
 1. \<And>b. [0 .e. b] = nths enum {..<Suc (fromEnum b)} proof (prove)
goal (1 subgoal):
 1. \<And>b. map toEnum [fromEnum 0..<Suc (fromEnum b)] = nths enum {..<Suc (fromEnum b)} proof (prove)
goal (1 subgoal):
 1. \<And>b. map toEnum [fromEnum 0..<Suc (fromEnum b)] = take (Suc (fromEnum b)) enum proof (prove)
goal (1 subgoal):
 1. \<And>b. map toEnum [fromEnum 0..<Suc (fromEnum b)] = take (Suc (fromEnum b)) (map word_of_nat [0..<2 ^ LENGTH('a)]) proof (prove)
goal (1 subgoal):
 1. \<And>b. map toEnum [fromEnum 0..<Suc (fromEnum b)] = map word_of_nat (take (Suc (fromEnum b)) [0..<2 ^ LENGTH('a)]) proof (prove)
goal (2 subgoals):
 1. \<And>b. 0 + Suc (fromEnum b) \<le> 2 ^ LENGTH('a)
 2. \<And>b. map toEnum [fromEnum 0..<Suc (fromEnum b)] = map word_of_nat [0..<0 + Suc (fromEnum b)] proof (prove)
goal (2 subgoals):
 1. \<And>b. Suc (unat b) \<le> 2 ^ LENGTH('a)
 2. \<And>b. map toEnum [fromEnum 0..<Suc (fromEnum b)] = map word_of_nat [0..<0 + Suc (fromEnum b)] proof (prove)
goal (3 subgoals):
 1. \<And>b. Suc (unat b) \<le> ?y5 b
 2. \<And>b. ?y5 b = 2 ^ LENGTH('a)
 3. \<And>b. map toEnum [fromEnum 0..<Suc (fromEnum b)] = map word_of_nat [0..<0 + Suc (fromEnum b)] proof (prove)
goal (2 subgoals):
 1. \<And>b. 2 ^ LENGTH('a) = 2 ^ LENGTH('a)
 2. \<And>b. map toEnum [fromEnum 0..<Suc (fromEnum b)] = map word_of_nat [0..<0 + Suc (fromEnum b)] proof (prove)
goal (1 subgoal):
 1. \<And>b. map toEnum [fromEnum 0..<Suc (fromEnum b)] = map word_of_nat [0..<0 + Suc (fromEnum b)] proof (prove)
goal (1 subgoal):
 1. \<And>b x. x < unat b \<Longrightarrow> toEnum x = word_of_nat x proof (prove)
goal (1 subgoal):
 1. \<And>b x. x < unat b \<Longrightarrow> x < 2 ^ LENGTH('a) proof (prove)
goal:
No subgoals! proof (state)
this:
[0 .e. ?b] = nths enum {..<Suc (fromEnum ?b)}

goal (1 subgoal):
 1. distinct [0 .e. b] proof (chain)
picking this:
[0 .e. ?b] = nths enum {..<Suc (fromEnum ?b)} proof (prove)
using this:
[0 .e. ?b] = nths enum {..<Suc (fromEnum ?b)}

goal (1 subgoal):
 1. distinct [0 .e. b] proof (state)
this:
distinct [0 .e. b]

goal:
No subgoals!
theory Enumeration_Word

lemma upto_enum_less:
  assumes xin: "x \<in> set [(a::'a::len word).e.2 ^ n - 1]"
  and     nv:  "n < LENGTH('a::len)"
  shows   "x < 2 ^ n" proof (cases n) case 0 then show ?thesis using xin by simp next case (Suc m) show ?thesis using xin nv le_m1_iff_lt p2_gt_0 by auto qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x < 2 ^ n proof (state)
goal (2 subgoals):
 1. n = 0 \<Longrightarrow> x < 2 ^ n
 2. \<And>nat. n = Suc nat \<Longrightarrow> x < 2 ^ n proof (state)
this:
n = 0

goal (2 subgoals):
 1. n = 0 \<Longrightarrow> x < 2 ^ n
 2. \<And>nat. n = Suc nat \<Longrightarrow> x < 2 ^ n proof (chain)
picking this:
n = 0 proof (prove)
using this:
n = 0

goal (1 subgoal):
 1. x < 2 ^ n proof (prove)
using this:
n = 0
x \<in> set [a .e. 2 ^ n - 1]

goal (1 subgoal):
 1. x < 2 ^ n proof (state)
this:
x < 2 ^ n

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> x < 2 ^ n proof (state)
goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> x < 2 ^ n proof (state)
this:
n = Suc m

goal (1 subgoal):
 1. \<And>nat. n = Suc nat \<Longrightarrow> x < 2 ^ n proof (prove)
goal (1 subgoal):
 1. x < 2 ^ n proof (prove)
using this:
x \<in> set [a .e. 2 ^ n - 1]
n < LENGTH('a)
(0 < ?x) = ((?y \<le> ?x - 1) = (?y < ?x))
(0 < 2 ^ ?n) = (?n < LENGTH(?'a))

goal (1 subgoal):
 1. x < 2 ^ n proof (state)
this:
x < 2 ^ n

goal:
No subgoals!
theory Enumeration_Word

lemma upto_enum_len_less:
  "\<lbrakk> n \<le> length [a, b .e. c]; n \<noteq> 0 \<rbrakk> \<Longrightarrow> a \<le> c" unfolding upto_enum_step_def by (simp split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> length [a , b .e. c]; n \<noteq> 0\<rbrakk> \<Longrightarrow> a \<le> c proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<le> length (if c < a then [] else map (\<lambda>x. a + x * (b - a)) [0 .e. (c - a) div (b - a)]); n \<noteq> 0\<rbrakk> \<Longrightarrow> a \<le> c
theory Enumeration_Word

lemma length_upto_enum_step:
  fixes x :: "'a :: len word"
  shows "x \<le> z \<Longrightarrow> length [x , y .e. z] = (unat ((z - x) div (y - x))) + 1" unfolding upto_enum_step_def by (simp add: upto_enum_red)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<le> z \<Longrightarrow> length [x , y .e. z] = unat ((z - x) div (y - x)) + 1 proof (prove)
goal (1 subgoal):
 1. x \<le> z \<Longrightarrow> length (if z < x then [] else map (\<lambda>xa. x + xa * (y - x)) [0 .e. (z - x) div (y - x)]) = unat ((z - x) div (y - x)) + 1
theory Enumeration_Word

lemma map_length_unfold_one:
  fixes x :: "'a::len word"
  assumes xv: "Suc (unat x) < 2 ^ LENGTH('a)"
  and     ax: "a < x"
  shows   "map f [a .e. x] = f a # map f [a + 1 .e. x]" by (subst word_upto_Cons_eq, auto, fact+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map f [a .e. x] = f a # map f [a + 1 .e. x]
theory Enumeration_Word

lemma upto_enum_set_conv2:
  fixes a :: "'a::len word"
  shows "set [a .e. b] = {a .. b}" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set [a .e. b] = {a..b}
theory Enumeration_Word

lemma length_upto_enum [simp]:
  fixes a :: "'a :: len word"
  shows "length [a .e. b] = Suc (unat b) - unat a" apply (simp add: word_le_nat_alt upto_enum_red) apply (clarsimp simp: Suc_diff_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length [a .e. b] = Suc (unat b) - unat a proof (prove)
goal (1 subgoal):
 1. unat a \<le> unat b \<longrightarrow> Suc (unat b - unat a) = Suc (unat b) - unat a proof (prove)
goal:
No subgoals!
theory Enumeration_Word

lemma length_upto_enum_cases:
  fixes a :: "'a::len word"
  shows "length [a .e. b] = (if a \<le> b then Suc (unat b) - unat a else 0)" apply (case_tac "a \<le> b") apply (clarsimp) apply (clarsimp simp: upto_enum_def) apply unat_arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length [a .e. b] = (if a \<le> b then Suc (unat b) - unat a else 0) proof (prove)
goal (2 subgoals):
 1. a \<le> b \<Longrightarrow> length [a .e. b] = (if a \<le> b then Suc (unat b) - unat a else 0)
 2. \<not> a \<le> b \<Longrightarrow> length [a .e. b] = (if a \<le> b then Suc (unat b) - unat a else 0) proof (prove)
goal (1 subgoal):
 1. \<not> a \<le> b \<Longrightarrow> length [a .e. b] = (if a \<le> b then Suc (unat b) - unat a else 0) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> a \<le> b; unat a \<le> unat b\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Enumeration_Word

lemma length_upto_enum_less_one:
  "\<lbrakk>a \<le> b; b \<noteq> 0\<rbrakk>
  \<Longrightarrow> length [a .e. b - 1] = unat (b - a)" apply clarsimp apply (subst unat_sub[symmetric], assumption) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> b; b \<noteq> 0\<rbrakk> \<Longrightarrow> length [a .e. b - 1] = unat (b - a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> b; b \<noteq> 0\<rbrakk> \<Longrightarrow> unat b - unat a = unat (b - a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> b; b \<noteq> 0\<rbrakk> \<Longrightarrow> unat (b - a) = unat (b - a) proof (prove)
goal:
No subgoals!
theory Enumeration_Word

lemma drop_upto_enum:
  "drop (unat n) [0 .e. m] = [n .e. m]" apply (clarsimp simp: upto_enum_def) apply (induct m, simp) by (metis drop_map drop_upt plus_nat.add_0)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. drop (unat n) [0 .e. m] = [n .e. m] proof (prove)
goal (1 subgoal):
 1. unat n \<le> unat m \<Longrightarrow> drop (unat n) (map toEnum [0..<unat m]) = map toEnum [unat n..<unat m] proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>1 + m \<noteq> 0; unat n \<le> unat m \<Longrightarrow> drop (unat n) (map toEnum [0..<unat m]) = map toEnum [unat n..<unat m]; unat n \<le> unat (1 + m)\<rbrakk> \<Longrightarrow> drop (unat n) (map toEnum [0..<unat (1 + m)]) = map toEnum [unat n..<unat (1 + m)]
theory Enumeration_Word

lemma distinct_enum_upto' [simp]:
  "distinct [a::'a::len word .e. b]" apply (subst drop_upto_enum [symmetric]) apply (rule distinct_drop) apply (rule distinct_enum_upto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. distinct [a .e. b] proof (prove)
goal (1 subgoal):
 1. distinct (drop (unat a) [0 .e. b]) proof (prove)
goal (1 subgoal):
 1. distinct [0 .e. b] proof (prove)
goal:
No subgoals!
theory Enumeration_Word

lemma length_interval:
  "\<lbrakk>set xs = {x. (a::'a::len word) \<le> x \<and> x \<le> b}; distinct xs\<rbrakk>
  \<Longrightarrow> length xs = Suc (unat b) - unat a" apply (frule distinct_card) apply (subgoal_tac "set xs = set [a .e. b]") apply (cut_tac distinct_card [where xs="[a .e. b]"]) apply (subst (asm) length_upto_enum) apply clarsimp apply (rule distinct_enum_upto') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set xs = {x. a \<le> x \<and> x \<le> b}; distinct xs\<rbrakk> \<Longrightarrow> length xs = Suc (unat b) - unat a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set xs = {x. a \<le> x \<and> x \<le> b}; distinct xs; card (set xs) = length xs\<rbrakk> \<Longrightarrow> length xs = Suc (unat b) - unat a proof (prove)
goal (2 subgoals):
 1. \<lbrakk>set xs = {x. a \<le> x \<and> x \<le> b}; distinct xs; card (set xs) = length xs; set xs = set [a .e. b]\<rbrakk> \<Longrightarrow> length xs = Suc (unat b) - unat a
 2. \<lbrakk>set xs = {x. a \<le> x \<and> x \<le> b}; distinct xs; card (set xs) = length xs\<rbrakk> \<Longrightarrow> set xs = set [a .e. b] proof (prove)
goal (3 subgoals):
 1. \<lbrakk>set xs = {x. a \<le> x \<and> x \<le> b}; distinct xs; card (set xs) = length xs; set xs = set [a .e. b]; card (set [a .e. b]) = length [a .e. b]\<rbrakk> \<Longrightarrow> length xs = Suc (unat b) - unat a
 2. \<lbrakk>set xs = {x. a \<le> x \<and> x \<le> b}; distinct xs; card (set xs) = length xs; set xs = set [a .e. b]\<rbrakk> \<Longrightarrow> distinct [a .e. b]
 3. \<lbrakk>set xs = {x. a \<le> x \<and> x \<le> b}; distinct xs; card (set xs) = length xs\<rbrakk> \<Longrightarrow> set xs = set [a .e. b] proof (prove)
goal (3 subgoals):
 1. \<lbrakk>set xs = {x. a \<le> x \<and> x \<le> b}; distinct xs; card (set xs) = length xs; set xs = set [a .e. b]; card (set [a .e. b]) = Suc (unat b) - unat a\<rbrakk> \<Longrightarrow> length xs = Suc (unat b) - unat a
 2. \<lbrakk>set xs = {x. a \<le> x \<and> x \<le> b}; distinct xs; card (set xs) = length xs; set xs = set [a .e. b]\<rbrakk> \<Longrightarrow> distinct [a .e. b]
 3. \<lbrakk>set xs = {x. a \<le> x \<and> x \<le> b}; distinct xs; card (set xs) = length xs\<rbrakk> \<Longrightarrow> set xs = set [a .e. b] proof (prove)
goal (2 subgoals):
 1. \<lbrakk>set xs = {x. a \<le> x \<and> x \<le> b}; distinct xs; card (set xs) = length xs; set xs = set [a .e. b]\<rbrakk> \<Longrightarrow> distinct [a .e. b]
 2. \<lbrakk>set xs = {x. a \<le> x \<and> x \<le> b}; distinct xs; card (set xs) = length xs\<rbrakk> \<Longrightarrow> set xs = set [a .e. b] proof (prove)
goal (1 subgoal):
 1. \<lbrakk>set xs = {x. a \<le> x \<and> x \<le> b}; distinct xs; card (set xs) = length xs\<rbrakk> \<Longrightarrow> set xs = set [a .e. b] proof (prove)
goal:
No subgoals!
theory Enumeration_Word

lemma remdups_enum_upto:
  fixes s::"'a::len word"
  shows "remdups [s .e. e] = [s .e. e]" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. remdups [s .e. e] = [s .e. e]
theory Enumeration_Word

lemma length_upto_enum_one:
  fixes x :: "'a :: len word"
  assumes lt1: "x < y" and lt2: "z < y" and lt3: "x \<le> z"
  shows "[x , y .e. z] = [x]" unfolding upto_enum_step_def proof (subst upto_enum_red, subst if_not_P [OF leD [OF lt3]], clarsimp, rule conjI) show "unat ((z - x) div (y - x)) = 0" proof (subst unat_div, rule div_less) have syx: "unat (y - x) = unat y - unat x" by (rule unat_sub [OF order_less_imp_le]) fact moreover have "unat (z - x) = unat z - unat x" by (rule unat_sub) fact ultimately show "unat (z - x) < unat (y - x)" using lt2 lt3 unat_mono word_less_minus_mono_left by blast qed then show "(z - x) div (y - x) * (y - x) = 0" by (simp add: unat_div) (simp add: word_arith_nat_defs(6)) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. [x , y .e. z] = [x] proof (prove)
goal (1 subgoal):
 1. (if z < x then [] else map (\<lambda>xa. x + xa * (y - x)) [0 .e. (z - x) div (y - x)]) = [x] proof (state)
goal (2 subgoals):
 1. unat ((z - x) div (y - x)) = 0
 2. (z - x) div (y - x) * (y - x) = 0 proof (prove)
goal (1 subgoal):
 1. unat ((z - x) div (y - x)) = 0 proof (state)
goal (1 subgoal):
 1. unat (z - x) < unat (y - x) proof (prove)
goal (1 subgoal):
 1. unat (y - x) = unat y - unat x proof (state)
this:
unat (y - x) = unat y - unat x

goal (1 subgoal):
 1. unat (z - x) < unat (y - x) proof (state)
this:
unat (y - x) = unat y - unat x

goal (1 subgoal):
 1. unat (z - x) < unat (y - x) proof (prove)
goal (1 subgoal):
 1. unat (z - x) = unat z - unat x proof (state)
this:
unat (z - x) = unat z - unat x

goal (1 subgoal):
 1. unat (z - x) < unat (y - x) proof (chain)
picking this:
unat (y - x) = unat y - unat x
unat (z - x) = unat z - unat x proof (prove)
using this:
unat (y - x) = unat y - unat x
unat (z - x) = unat z - unat x

goal (1 subgoal):
 1. unat (z - x) < unat (y - x) proof (prove)
using this:
unat (y - x) = unat y - unat x
unat (z - x) = unat z - unat x
z < y
x \<le> z
?a < ?b \<Longrightarrow> unat ?a < unat ?b
\<lbrakk>?y < ?z; ?x \<le> ?y\<rbrakk> \<Longrightarrow> ?y - ?x < ?z - ?x

goal (1 subgoal):
 1. unat (z - x) < unat (y - x) proof (state)
this:
unat (z - x) < unat (y - x)

goal:
No subgoals! proof (state)
this:
unat ((z - x) div (y - x)) = 0

goal (1 subgoal):
 1. (z - x) div (y - x) * (y - x) = 0 proof (chain)
picking this:
unat ((z - x) div (y - x)) = 0 proof (prove)
using this:
unat ((z - x) div (y - x)) = 0

goal (1 subgoal):
 1. (z - x) div (y - x) * (y - x) = 0 proof (state)
this:
(z - x) div (y - x) * (y - x) = 0

goal:
No subgoals!
theory More_Sublist

lemma same_length_is_parallel:
  assumes len: "\<forall>y \<in> set as. length y = x"
  shows  "\<forall>x \<in> set as. \<forall>y \<in> set as - {x}. x \<parallel> y" proof (rule, rule) fix x y assume xi: "x \<in> set as" and yi: "y \<in> set as - {x}" from len obtain q where len': "\<forall>y \<in> set as. length y = q" .. show "x \<parallel> y" proof (rule not_equal_is_parallel) from xi yi show "x \<noteq> y" by auto from xi yi len' show "length x = length y" by (auto dest: bspec) qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set as. \<forall>y\<in>set as - {x}. x \<parallel> y proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set as; y \<in> set as - {x}\<rbrakk> \<Longrightarrow> x \<parallel> y proof (state)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set as; y \<in> set as - {x}\<rbrakk> \<Longrightarrow> x \<parallel> y proof (state)
this:
x \<in> set as
y \<in> set as - {x}

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set as; y \<in> set as - {x}\<rbrakk> \<Longrightarrow> x \<parallel> y proof (chain)
picking this:
\<forall>y\<in>set as. length y = x proof (prove)
using this:
\<forall>y\<in>set as. length y = x

goal (1 subgoal):
 1. (\<And>q. \<forall>y\<in>set as. length y = q \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
\<forall>y\<in>set as. length y = q

goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> set as; y \<in> set as - {x}\<rbrakk> \<Longrightarrow> x \<parallel> y proof (prove)
goal (1 subgoal):
 1. x \<parallel> y proof (state)
goal (2 subgoals):
 1. x \<noteq> y
 2. length x = length y proof (chain)
picking this:
x \<in> set as
y \<in> set as - {x} proof (prove)
using this:
x \<in> set as
y \<in> set as - {x}

goal (1 subgoal):
 1. x \<noteq> y proof (state)
this:
x \<noteq> y

goal (1 subgoal):
 1. length x = length y proof (chain)
picking this:
x \<in> set as
y \<in> set as - {x}
\<forall>y\<in>set as. length y = q proof (prove)
using this:
x \<in> set as
y \<in> set as - {x}
\<forall>y\<in>set as. length y = q

goal (1 subgoal):
 1. length x = length y proof (state)
this:
length x = length y

goal:
No subgoals! proof (state)
this:
x \<parallel> y

goal:
No subgoals!
theory More_Sublist

lemma sublist_equal_part:
  "prefix xs ys \<Longrightarrow> take (length xs) ys = xs" by (clarsimp simp: prefix_def)

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

lemma prefix_length_less:
  "strict_prefix xs ys \<Longrightarrow> length xs < length ys" apply (clarsimp simp: strict_prefix_def) apply (frule prefix_length_le) apply (rule ccontr, simp) apply (clarsimp simp: prefix_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. strict_prefix xs ys \<Longrightarrow> length xs < length ys proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix xs ys; xs \<noteq> ys\<rbrakk> \<Longrightarrow> length xs < length ys proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix xs ys; xs \<noteq> ys; length xs \<le> length ys\<rbrakk> \<Longrightarrow> length xs < length ys proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prefix xs ys; xs \<noteq> ys; length xs = length ys\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory More_Sublist

lemma not_prefix_longer:
  "\<lbrakk> length xs > length ys \<rbrakk> \<Longrightarrow> \<not> prefix xs ys" by (clarsimp dest!: prefix_length_le)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length ys < length xs \<Longrightarrow> \<not> prefix xs ys
theory More_Sublist

lemma map_prefixI:
  "prefix xs ys \<Longrightarrow> prefix (map f xs) (map f ys)" by (clarsimp simp: prefix_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. prefix xs ys \<Longrightarrow> prefix (map f xs) (map f ys)