# HG changeset patch # User nipkow # Date 1738096924 -3600 # Node ID afae60d6ff1588b7752861e89a211a2e61fa4ff0 # Parent dfde9a8296f525476846136e27eb572da3898fbc extracted the ^^ subtheory for modularity reasons diff -r dfde9a8296f5 -r afae60d6ff15 src/HOL/List.thy --- a/src/HOL/List.thy Tue Jan 28 17:30:00 2025 +0100 +++ b/src/HOL/List.thy Tue Jan 28 21:42:04 2025 +0100 @@ -263,15 +263,6 @@ replicate_0: "replicate 0 x = []" | replicate_Suc: "replicate (Suc n) x = x # replicate n x" -overloading pow_list == "compow :: nat \ 'a list \ 'a list" -begin - -primrec pow_list :: "nat \ 'a list \ 'a list" where -"pow_list 0 xs = []" | -"pow_list (Suc n) xs = xs @ pow_list n xs" - -end - text \ Function \size\ is overloaded for all datatypes. Users may refer to the list version as \length\.\ @@ -4846,134 +4837,6 @@ by (subst foldr_fold [symmetric]) simp_all -subsubsection \\<^term>\xs ^^ n\\ - -context -begin - -interpretation monoid_mult "[]" "append" - rewrites "power u n = u ^^ n" -proof- - show "class.monoid_mult [] (@)" - by (unfold_locales, simp_all) - show "power.power [] (@) u n = u ^^ n" - by(induction n) (auto simp add: power.power.simps) -qed - -\ \inherited power properties\ - -lemmas pow_list_zero = power.power_0 and - pow_list_one = power_Suc0_right and - pow_list_1 = power_one_right and - pow_list_Nil = power_one and - pow_list_2 = power2_eq_square and - pow_list_Suc = power_Suc and - pow_list_Suc2 = power_Suc2 and - pow_list_comm = power_commutes and - pow_list_add = power_add and - pow_list_eq_if = power_eq_if and - pow_list_mult = power_mult and - pow_list_commuting_commutes = power_commuting_commutes - -end - -lemma pow_list_alt: "xs^^n = concat (replicate n xs)" -by (induct n) auto - -lemma pow_list_single: "[a] ^^ m = replicate m a" -by(simp add: pow_list_alt) - -lemma length_pow_list_single [simp]: "length([a] ^^ n) = n" -by (simp add: pow_list_single) - -lemma nth_pow_list_single: "i < m \ ([a] ^^ m) ! i = a" -by (simp add: pow_list_single) - -lemma pow_list_not_NilD: "xs ^^ m \ [] \ 0 < m" -by (cases m) auto - -lemma length_pow_list: "length(xs ^^ k) = k * length xs" -by (induction k) simp+ - -lemma pow_list_set: "set (w ^^ Suc k) = set w" -by (induction k)(simp_all) - -lemma pow_list_slide: "xs @ (ys @ xs) ^^ n @ ys = (xs @ ys)^^(Suc n)" -by (induction n) simp+ - -lemma hd_pow_list: "0 < n \ hd(xs ^^ n) = hd xs" -by(auto simp: pow_list_alt hd_append gr0_conv_Suc) - -lemma rev_pow_list: "rev (xs ^^ m) = (rev xs) ^^ m" -by (induction m)(auto simp: pow_list_comm) - -lemma eq_pow_list_iff_eq_exp[simp]: assumes "xs \ []" shows "xs ^^ k = xs ^^ m \ k = m" -proof - assume "k = m" thus "xs ^^ k = xs ^^ m" by simp -next - assume "xs ^^ k = xs ^^ m" - thus "k = m" using \xs \ []\[folded length_0_conv] - by (metis length_pow_list mult_cancel2) -qed - -lemma pow_list_Nil_iff_0: "xs \ [] \ xs ^^ m = [] \ m = 0" -by (simp add: pow_list_eq_if) - -lemma pow_list_Nil_iff_Nil: "0 < m \ xs ^^ m = [] \ xs = []" -by (cases xs) (auto simp add: pow_list_Nil pow_list_Nil_iff_0) - -lemma pow_eq_eq: - assumes "xs ^^ k = ys ^^ k" and "0 < k" - shows "(xs::'a list) = ys" -proof- - have "length xs = length ys" - using assms(1) length_pow_list by (metis nat_mult_eq_cancel1[OF \0 < k\]) - thus ?thesis by (metis Suc_pred append_eq_append_conv assms(1,2) pow_list.simps(2)) -qed - -lemma map_pow_list[simp]: "map f (xs ^^ k) = (map f xs) ^^ k" -by (induction k) simp_all - -lemma concat_pow_list: "concat (xs ^^ k) = (concat xs) ^^ k" -by (induction k) simp_all - -lemma concat_pow_list_single[simp]: "concat ([a] ^^ k) = a ^^ k" -by (simp add: pow_list_alt) - -lemma pow_list_single_Nil_iff: "[a] ^^ n = [] \ n = 0" -by (simp add: pow_list_single) - -lemma hd_pow_list_single: "k \ 0 \ hd ([a] ^^ k) = a" -by (cases k) simp+ - -lemma index_pow_mod: "i < length(xs ^^ k) \ (xs ^^ k)!i = xs!(i mod length xs)" -proof(induction k) - have aux: "length(xs ^^ Suc l) = length(xs ^^ l) + length xs" for l - by simp - have aux1: "length (xs ^^ l) \ i \ i < length(xs ^^ l) + length xs \ i mod length xs = i - length(xs^^l)" for l - unfolding length_pow_list[of l xs] - using less_diff_conv2[of "l * length xs" i "length xs", unfolded add.commute[of "length xs" "l * length xs"]] - le_add_diff_inverse[of "l*length xs" i] - by (simp add: mod_nat_eqI) - case (Suc k) - show ?case - unfolding aux sym[OF pow_list_Suc2[symmetric]] nth_append le_mod_geq - using aux1[ OF _ Suc.prems[unfolded aux]] - Suc.IH pow_list_Suc2[symmetric] Suc.prems[unfolded aux] leI[of i "length(xs ^^ k)"] by presburger -qed auto - -lemma unique_letter_word: assumes "\c. c \ set w \ c = a" shows "w = [a] ^^ length w" - using assms proof (induction w) - case (Cons b w) - have "[a] ^^ length w = w" using Cons.IH[OF Cons.prems[OF list.set_intros(2)]].. - then show "b # w = [a] ^^ length(b # w)" - unfolding Cons.prems[OF list.set_intros(1)] by auto -qed simp - -lemma count_list_pow_list: "count_list (w ^^ k) a = k * (count_list w a)" -by (induction k) simp+ - - subsubsection \\<^const>\enumerate\\ lemma enumerate_simps [simp, code]: @@ -6833,21 +6696,6 @@ lemma replicate_in_lists: "a \ A \ replicate k a \ lists A" by (induction k) auto -lemma sing_pow_lists: "a \ A \ [a] ^^ n \ lists A" -by (induction n) auto - -lemma one_generated_list_power: "u \ lists {x} \ \k. concat u = x ^^ k" -proof(induction u rule: lists.induct) - case Nil - then show ?case by (metis concat.simps(1) pow_list.simps(1)) -next - case Cons - then show ?case by (metis concat.simps(2) pow_list_Suc singletonD) -qed - -lemma pow_list_in_lists: "0 < k \ u ^^ k \ lists B \ u \ lists B" -by (metis Suc_pred in_lists_conv_set pow_list_set) - subsubsection \Inductive definition for membership\