# HG changeset patch # User wenzelm # Date 1729887741 -7200 # Node ID d912f97aaa861e806011456ac18058f55b93f028 # Parent 7e86118f4791396c8a076a2f92d26803a5774ae7# Parent 0c9075bdff38bd79f85d61da2b60c4fe104117b8 merged diff -r 7e86118f4791 -r d912f97aaa86 src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy --- a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Fri Oct 25 17:01:23 2024 +0200 +++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy Fri Oct 25 22:22:21 2024 +0200 @@ -28,6 +28,8 @@ syntax "_MTuple" :: "['a, args] \ 'a * 'b" (\(\indent=2 notation=\mixfix message tuple\\\_,/ _\)\) +syntax_consts + "_MTuple" \ MPair translations "\x, y, z\" \ "\x, \y, z\\" "\x, y\" \ "CONST MPair x y" diff -r 7e86118f4791 -r d912f97aaa86 src/Doc/Tutorial/Protocol/Message.thy --- a/src/Doc/Tutorial/Protocol/Message.thy Fri Oct 25 17:01:23 2024 +0200 +++ b/src/Doc/Tutorial/Protocol/Message.thy Fri Oct 25 22:22:21 2024 +0200 @@ -81,6 +81,8 @@ text\Concrete syntax: messages appear as \\A,B,NA\\, etc...\ syntax "_MTuple" :: "['a, args] \ 'a * 'b" ("(\indent=2 notation=\mixfix message tuple\\\_,/ _\)") +syntax_consts + "_MTuple" \ MPair translations "\x, y, z\" \ "\x, \y, z\\" "\x, y\" \ "CONST MPair x y" diff -r 7e86118f4791 -r d912f97aaa86 src/HOL/Library/FuncSet.thy --- a/src/HOL/Library/FuncSet.thy Fri Oct 25 17:01:23 2024 +0200 +++ b/src/HOL/Library/FuncSet.thy Fri Oct 25 22:22:21 2024 +0200 @@ -405,17 +405,13 @@ lemma PiE_insert_eq: "Pi\<^sub>E (insert x S) T = (\(y, g). g(x := y)) ` (T x \ Pi\<^sub>E S T)" proof - - { - fix f assume "f \ Pi\<^sub>E (insert x S) T" "x \ S" - then have "f \ (\(y, g). g(x := y)) ` (T x \ Pi\<^sub>E S T)" - by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem) - } + have "f \ (\(y, g). g(x := y)) ` (T x \ Pi\<^sub>E S T)" if "f \ Pi\<^sub>E (insert x S) T" "x \ S" for f + using that + by (auto intro!: image_eqI[where x="(f x, f(x := undefined))"] intro: fun_upd_in_PiE PiE_mem) moreover - { - fix f assume "f \ Pi\<^sub>E (insert x S) T" "x \ S" - then have "f \ (\(y, g). g(x := y)) ` (T x \ Pi\<^sub>E S T)" - by (auto intro!: image_eqI[where x="(f x, f)"] intro: fun_upd_in_PiE PiE_mem simp: insert_absorb) - } + have "f \ (\(y, g). g(x := y)) ` (T x \ Pi\<^sub>E S T)" if "f \ Pi\<^sub>E (insert x S) T" "x \ S" for f + using that + by (auto intro!: image_eqI[where x="(f x, f)"] intro: fun_upd_in_PiE PiE_mem simp: insert_absorb) ultimately show ?thesis by (auto intro: PiE_fun_upd) qed @@ -487,8 +483,7 @@ by auto qed (auto simp: PiE_def) -lemma PiE_eq_iff: - "Pi\<^sub>E I F = Pi\<^sub>E I F' \ (\i\I. F i = F' i) \ ((\i\I. F i = {}) \ (\i\I. F' i = {}))" +lemma PiE_eq_iff: "Pi\<^sub>E I F = Pi\<^sub>E I F' \ (\i\I. F i = F' i) \ ((\i\I. F i = {}) \ (\i\I. F' i = {}))" proof (intro iffI disjCI) assume eq[simp]: "Pi\<^sub>E I F = Pi\<^sub>E I F'" assume "\ ((\i\I. F i = {}) \ (\i\I. F' i = {}))" @@ -528,8 +523,7 @@ by simp qed simp -lemma PiE_eq: - "PiE I S = PiE I T \ PiE I S = {} \ PiE I T = {} \ (\i \ I. S i = T i)" +lemma PiE_eq: "PiE I S = PiE I T \ PiE I S = {} \ PiE I T = {} \ (\i \ I. S i = T i)" by (auto simp: PiE_eq_iff PiE_eq_empty_iff) lemma PiE_UNIV [simp]: "PiE UNIV (\i. UNIV) = UNIV" @@ -542,7 +536,7 @@ proof - have "x \ S i \ \f\Pi\<^sub>E I S. x = f i" for x using that - by (force intro: bexI [where x="\k. if k=i then x else f k"]) + by (force intro: bexI [where x="\k. if k=i then x else f k"]) then show ?thesis using that by force qed @@ -552,15 +546,16 @@ lemma PiE_singleton: assumes "f \ extensional A" - shows "PiE A (\x. {f x}) = {f}" + shows "PiE A (\x. {f x}) = {f}" proof - - { - fix g assume "g \ PiE A (\x. {f x})" - hence "g x = f x" for x + have "g = f" if "g \ PiE A (\x. {f x})" for g + proof - + from that have "g x = f x" for x using assms by (cases "x \ A") (auto simp: extensional_def) - hence "g = f" by (simp add: fun_eq_iff) - } - thus ?thesis using assms by (auto simp: extensional_def) + then show ?thesis by (simp add: fun_eq_iff) + qed + with assms show ?thesis + by (auto simp: extensional_def) qed lemma PiE_eq_singleton: "(\\<^sub>E i\I. S i) = {\i\I. f i} \ (\i\I. S i = {f i})" @@ -568,14 +563,15 @@ lemma PiE_over_singleton_iff: "(\\<^sub>E x\{a}. B x) = (\b \ B a. {\x \ {a}. b})" proof - - have "\x. \x a \ B a; x \ extensional {a}\ \ \xa\B a. x = (\x\{a}. xa)" - using PiE_singleton by fastforce + have "\xa\B a. x = (\x\{a}. xa)" if "x a \ B a" and "x \ extensional {a}" for x + using that PiE_singleton by fastforce then show ?thesis by (auto simp: PiE_iff split: if_split_asm) qed lemma all_PiE_elements: - "(\z \ PiE I S. \i \ I. P i (z i)) \ PiE I S = {} \ (\i \ I. \x \ S i. P i x)" (is "?lhs = ?rhs") + "(\z \ PiE I S. \i \ I. P i (z i)) \ PiE I S = {} \ (\i \ I. \x \ S i. P i x)" + (is "?lhs = ?rhs") proof (cases "PiE I S = {}") case False then obtain f where f: "\i. i \ I \ f i \ S i" @@ -616,12 +612,12 @@ shows "{f. f \ (insert x S) \\<^sub>E T \ inj_on f (insert x S)} = (\(y, g). g(x:=y)) ` {(y, g). y \ T \ g \ S \\<^sub>E (T - {y}) \ inj_on g S}" proof - - have "\a f y. \f \ S \\<^sub>E T - {a}; a = (if y = x then a else f y); y \ S\ - \ False" - using assms by (auto dest!: PiE_mem split: if_split_asm) + have False if "f \ S \\<^sub>E T - {a}" and "a = (if y = x then a else f y)" and "y \ S" for a f y + using assms that by (auto dest!: PiE_mem split: if_split_asm) moreover - have "\f. \ f \ insert x S \\<^sub>E T; inj_on f S; \xb\S. f x \ f xb\ - \ \b. b \ S \\<^sub>E T - {f x} \ inj_on b S \ f = b(x := f x)" + have "\b. b \ S \\<^sub>E T - {f x} \ inj_on b S \ f = b(x := f x)" + if "f \ insert x S \\<^sub>E T" and "inj_on f S" and "\xb\S. f x \ f xb" for f + using that unfolding inj_on_def by (smt (verit, ccfv_threshold) PiE_restrict fun_upd_apply fun_upd_triv insert_Diff insert_iff restrict_PiE_iff restrict_upd) @@ -630,15 +626,15 @@ apply (auto simp: image_iff intro: extensional_funcset_fun_upd_inj_onI extensional_funcset_fun_upd_extends_rangeI del: PiE_I PiE_E) apply (smt (verit, best) PiE_cong PiE_mem inj_on_def insertCI) - by blast + apply blast + done qed lemma extensional_funcset_extend_domain_inj_onI: assumes "x \ S" shows "inj_on (\(y, g). g(x := y)) {(y, g). y \ T \ g \ S \\<^sub>E (T - {y}) \ inj_on g S}" using assms - apply (simp add: inj_on_def) - by (metis PiE_restrict fun_upd_apply restrict_fupd) + by (simp add: inj_on_def) (metis PiE_restrict fun_upd_apply restrict_fupd) subsubsection \Misc properties of functions, composition and restriction from HOL Light\ @@ -654,24 +650,19 @@ by (metis (mono_tags, opaque_lifting) f_inv_into_f imageI inv_into_into mem_Collect_eq) qed auto -lemma function_factors_left: - "(\x y. (g x = g y) \ (f x = f y)) \ (\h. f = h \ g)" +lemma function_factors_left: "(\x y. (g x = g y) \ (f x = f y)) \ (\h. f = h \ g)" using function_factors_left_gen [of "\x. True" g f] unfolding o_def by blast -lemma function_factors_right_gen: - "(\x. P x \ (\y. g y = f x)) \ (\h. \x. P x \ f x = g(h x))" +lemma function_factors_right_gen: "(\x. P x \ (\y. g y = f x)) \ (\h. \x. P x \ f x = g(h x))" by metis -lemma function_factors_right: - "(\x. \y. g y = f x) \ (\h. f = g \ h)" +lemma function_factors_right: "(\x. \y. g y = f x) \ (\h. f = g \ h)" unfolding o_def by metis -lemma restrict_compose_right: - "restrict (g \ restrict f S) S = restrict (g \ f) S" +lemma restrict_compose_right: "restrict (g \ restrict f S) S = restrict (g \ f) S" by auto -lemma restrict_compose_left: - "f ` S \ T \ restrict (restrict g T \ f) S = restrict (g \ f) S" +lemma restrict_compose_left: "f ` S \ T \ restrict (restrict g T \ f) S = restrict (g \ f) S" by fastforce @@ -696,80 +687,89 @@ lemma card_PiE: "finite S \ card (\\<^sub>E i \ S. T i) = (\ i\S. card (T i))" proof (induct rule: finite_induct) case empty - then show ?case by auto + then show ?case + by auto next case (insert x S) then show ?case by (simp add: PiE_insert_eq inj_combinator card_image card_cartesian_product) qed -lemma card_funcsetE: "finite A \ card (A \\<^sub>E B) = card B ^ card A" - by (subst card_PiE, auto) +lemma card_funcsetE: "finite A \ card (A \\<^sub>E B) = card B ^ card A" + by (subst card_PiE) auto -lemma card_inj_on_subset_funcset: assumes finB: "finite B" - and finC: "finite C" - and AB: "A \ B" -shows "card {f \ B \\<^sub>E C. inj_on f A} = - card C^(card B - card A) * prod ((-) (card C)) {0 ..< card A}" +lemma card_inj_on_subset_funcset: + assumes finB: "finite B" + and finC: "finite C" + and AB: "A \ B" + shows "card {f \ B \\<^sub>E C. inj_on f A} = + card C^(card B - card A) * prod ((-) (card C)) {0 ..< card A}" proof - - define D where "D = B - A" - from AB have B: "B = A \ D" and disj: "A \ D = {}" unfolding D_def by auto - have sub: "card B - card A = card D" unfolding D_def using finB AB + define D where "D = B - A" + from AB have B: "B = A \ D" and disj: "A \ D = {}" + unfolding D_def by auto + have sub: "card B - card A = card D" + unfolding D_def using finB AB by (metis card_Diff_subset finite_subset) - have "finite A" "finite D" using finB unfolding B by auto - thus ?thesis unfolding sub unfolding B using disj + from finB B have "finite A" "finite D" by auto + then show ?thesis + unfolding sub unfolding B using disj proof (induct A rule: finite_induct) case empty - from card_funcsetE[OF this(1), of C] show ?case by auto + from card_funcsetE[OF this(1), of C] show ?case + by auto next case (insert a A) - have "{f. f \ insert a A \ D \\<^sub>E C \ inj_on f (insert a A)} - = {f(a := c) | f c. f \ A \ D \\<^sub>E C \ inj_on f A \ c \ C - f ` A}" + have "{f. f \ insert a A \ D \\<^sub>E C \ inj_on f (insert a A)} = + {f(a := c) | f c. f \ A \ D \\<^sub>E C \ inj_on f A \ c \ C - f ` A}" (is "?l = ?r") proof - show "?r \ ?l" - by (auto intro: inj_on_fun_updI split: if_splits) - { - fix f - assume f: "f \ ?l" - let ?g = "f(a := undefined)" - let ?h = "?g(a := f a)" + show "?r \ ?l" + by (auto intro: inj_on_fun_updI split: if_splits) + have "f \ ?r" if f: "f \ ?l" for f + proof - + let ?g = "f(a := undefined)" + let ?h = "?g(a := f a)" have mem: "f a \ C - ?g ` A" using insert(1,2,4,5) f by auto from f have f: "f \ insert a A \ D \\<^sub>E C" "inj_on f (insert a A)" by auto hence "?g \ A \ D \\<^sub>E C" "inj_on ?g A" using \a \ A\ \insert a A \ D = {}\ by (auto split: if_splits simp: inj_on_def) with mem have "?h \ ?r" by blast also have "?h = f" by auto - finally have "f \ ?r" . - } - thus "?l \ ?r" by auto + finally show ?thesis . + qed + then show "?l \ ?r" by auto qed - also have "\ = (\ (f, c). f (a := c)) ` + also have "\ = (\ (f, c). f (a := c)) ` (Sigma {f . f \ A \ D \\<^sub>E C \ inj_on f A} (\ f. C - f ` A))" by auto - also have "card (...) = card (Sigma {f . f \ A \ D \\<^sub>E C \ inj_on f A} (\ f. C - f ` A))" - proof (rule card_image, intro inj_onI, clarsimp, goal_cases) + also have "card (...) = card (Sigma {f . f \ A \ D \\<^sub>E C \ inj_on f A} (\ f. C - f ` A))" + proof (rule card_image, intro inj_onI, clarsimp, goal_cases) case (1 f c g d) - let ?f = "f(a := c, a := undefined)" - let ?g = "g(a := d, a := undefined)" - from 1 have id: "f(a := c) = g(a := d)" by auto - from fun_upd_eqD[OF id] - have cd: "c = d" by auto - from id have "?f = ?g" by auto - also have "?f = f" using `f \ A \ D \\<^sub>E C` insert(1,2,4,5) + let ?f = "f(a := c, a := undefined)" + let ?g = "g(a := d, a := undefined)" + from 1 have id: "f(a := c) = g(a := d)" + by auto + from fun_upd_eqD[OF id] + have cd: "c = d" + by auto + from id have "?f = ?g" + by auto + also have "?f = f" using `f \ A \ D \\<^sub>E C` insert(1,2,4,5) by (intro ext, auto) - also have "?g = g" using `g \ A \ D \\<^sub>E C` insert(1,2,4,5) + also have "?g = g" using `g \ A \ D \\<^sub>E C` insert(1,2,4,5) by (intro ext, auto) - finally show "f = g \ c = d" using cd by auto + finally show "f = g \ c = d" + using cd by auto qed - also have "\ = (\f\{f \ A \ D \\<^sub>E C. inj_on f A}. card (C - f ` A))" + also have "\ = (\f\{f \ A \ D \\<^sub>E C. inj_on f A}. card (C - f ` A))" by (rule card_SigmaI, rule finite_subset[of _ "A \ D \\<^sub>E C"], insert \finite C\ \finite D\ \finite A\, auto intro!: finite_PiE) also have "\ = (\f\{f \ A \ D \\<^sub>E C. inj_on f A}. card C - card A)" by (rule sum.cong[OF refl], subst card_Diff_subset, insert \finite A\, auto simp: card_image) - also have "\ = (card C - card A) * card {f \ A \ D \\<^sub>E C. inj_on f A}" + also have "\ = (card C - card A) * card {f \ A \ D \\<^sub>E C. inj_on f A}" by simp - also have "\ = card C ^ card D * ((card C - card A) * prod ((-) (card C)) {0.. = card C ^ card D * ((card C - card A) * prod ((-) (card C)) {0.. lemma pigeonhole_card: assumes "f \ A \ B" "finite A" "finite B" "B \ {}" - shows "\y\B. card (f -` {y} \ A) * card B \ card A" + shows "\y\B. card (f -` {y} \ A) * card B \ card A" proof - from assms have "card B > 0" by auto @@ -802,11 +802,11 @@ unfolding M_def using assms by (intro sum_mono Max.coboundedI) auto also have "\ = card B * M" by simp - finally have "M * card B \ card A" + finally have *: "M * card B \ card A" by (simp add: mult_ac) - moreover have "M \ (\y. card (f -` {y} \ A)) ` B" - unfolding M_def using assms \B \ {}\ by (intro Max_in) auto - ultimately show ?thesis + from assms have "M \ (\y. card (f -` {y} \ A)) ` B" + unfolding M_def by (intro Max_in) auto + with * show ?thesis by blast qed diff -r 7e86118f4791 -r d912f97aaa86 src/HOL/ex/Birthday_Paradox.thy --- a/src/HOL/ex/Birthday_Paradox.thy Fri Oct 25 17:01:23 2024 +0200 +++ b/src/HOL/ex/Birthday_Paradox.thy Fri Oct 25 22:22:21 2024 +0200 @@ -1,68 +1,81 @@ -(* Title: HOL/ex/Birthday_Paradox.thy - Author: Lukas Bulwahn, TU Muenchen, 2007 +(* Title: HOL/ex/Birthday_Paradox.thy + Author: Lukas Bulwahn, TU Muenchen, 2007 *) section \A Formulation of the Birthday Paradox\ theory Birthday_Paradox -imports Main "HOL-Library.FuncSet" + imports "HOL-Library.FuncSet" begin section \Cardinality\ lemma card_product_dependent: assumes "finite S" - assumes "\x \ S. finite (T x)" + and "\x \ S. finite (T x)" shows "card {(x, y). x \ S \ y \ T x} = (\x \ S. card (T x))" - using card_SigmaI[OF assms, symmetric] by (auto intro!: arg_cong[where f=card] simp add: Sigma_def) + using card_SigmaI[OF assms, symmetric] + by (auto intro!: arg_cong[where f=card] simp add: Sigma_def) lemma card_extensional_funcset_inj_on: assumes "finite S" "finite T" "card S \ card T" shows "card {f \ extensional_funcset S T. inj_on f S} = fact (card T) div (fact (card T - card S))" -using assms + using assms proof (induct S arbitrary: T rule: finite_induct) case empty - from this show ?case by (simp add: Collect_conv_if PiE_empty_domain) + from this show ?case + by (simp add: Collect_conv_if PiE_empty_domain) next case (insert x S) - { fix x - from \finite T\ have "finite (T - {x})" by auto - from \finite S\ this have "finite (extensional_funcset S (T - {x}))" + have finite_delete: "finite {f : extensional_funcset S (T - {x}). inj_on f S}" for x + proof - + from \finite T\ have "finite (T - {x})" + by auto + from \finite S\ this have *: "finite (extensional_funcset S (T - {x}))" by (rule finite_PiE) - moreover - have "{f : extensional_funcset S (T - {x}). inj_on f S} \ (extensional_funcset S (T - {x}))" by auto - ultimately have "finite {f : extensional_funcset S (T - {x}). inj_on f S}" + have "{f : extensional_funcset S (T - {x}). inj_on f S} \ (extensional_funcset S (T - {x}))" + by auto + with * show ?thesis by (auto intro: finite_subset) - } note finite_delete = this - from insert have hyps: "\y \ T. card ({g. g \ extensional_funcset S (T - {y}) \ inj_on g S}) = fact (card T - 1) div fact ((card T - 1) - card S)"(is "\ _ \ T. _ = ?k") by auto + qed + from insert have hyps: "\y \ T. card ({g. g \ extensional_funcset S (T - {y}) \ inj_on g S}) = + fact (card T - 1) div fact ((card T - 1) - card S)"(is "\ _ \ T. _ = ?k") + by auto from extensional_funcset_extend_domain_inj_on_eq[OF \x \ S\] have "card {f. f \ extensional_funcset (insert x S) T \ inj_on f (insert x S)} = - card ((\(y, g). g(x := y)) ` {(y, g). y \ T \ g \ extensional_funcset S (T - {y}) \ inj_on g S})" + card ((\(y, g). g(x := y)) ` {(y, g). y \ T \ g \ extensional_funcset S (T - {y}) \ inj_on g S})" by metis - also from extensional_funcset_extend_domain_inj_onI[OF \x \ S\, of T] have "\ = card {(y, g). y \ T \ g \ extensional_funcset S (T - {y}) \ inj_on g S}" + also from extensional_funcset_extend_domain_inj_onI[OF \x \ S\, of T] + have "\ = card {(y, g). y \ T \ g \ extensional_funcset S (T - {y}) \ inj_on g S}" by (simp add: card_image) also have "card {(y, g). y \ T \ g \ extensional_funcset S (T - {y}) \ inj_on g S} = - card {(y, g). y \ T \ g \ {f \ extensional_funcset S (T - {y}). inj_on f S}}" by auto - also from \finite T\ finite_delete have "... = (\y \ T. card {g. g \ extensional_funcset S (T - {y}) \ inj_on g S})" + card {(y, g). y \ T \ g \ {f \ extensional_funcset S (T - {y}). inj_on f S}}" + by auto + also from \finite T\ finite_delete + have "\ = (\y \ T. card {g. g \ extensional_funcset S (T - {y}) \ inj_on g S})" by (subst card_product_dependent) auto - also from hyps have "... = (card T) * ?k" + also from hyps have "\ = (card T) * ?k" by auto - also have "... = card T * fact (card T - 1) div fact (card T - card (insert x S))" + also have "\ = card T * fact (card T - 1) div fact (card T - card (insert x S))" using insert unfolding div_mult1_eq[of "card T" "fact (card T - 1)"] by (simp add: fact_mod) - also have "... = fact (card T) div fact (card T - card (insert x S))" + also have "\ = fact (card T) div fact (card T - card (insert x S))" using insert by (simp add: fact_reduce[of "card T"]) finally show ?case . qed lemma card_extensional_funcset_not_inj_on: assumes "finite S" "finite T" "card S \ card T" - shows "card {f \ extensional_funcset S T. \ inj_on f S} = (card T) ^ (card S) - (fact (card T)) div (fact (card T - card S))" + shows "card {f \ extensional_funcset S T. \ inj_on f S} = + (card T) ^ (card S) - (fact (card T)) div (fact (card T - card S))" proof - - have subset: "{f : extensional_funcset S T. inj_on f S} <= extensional_funcset S T" by auto - from finite_subset[OF subset] assms have finite: "finite {f : extensional_funcset S T. inj_on f S}" + have subset: "{f \ extensional_funcset S T. inj_on f S} \ extensional_funcset S T" + by auto + from finite_subset[OF subset] assms + have finite: "finite {f : extensional_funcset S T. inj_on f S}" by (auto intro!: finite_PiE) - have "{f \ extensional_funcset S T. \ inj_on f S} = extensional_funcset S T - {f \ extensional_funcset S T. inj_on f S}" by auto + have "{f \ extensional_funcset S T. \ inj_on f S} = + extensional_funcset S T - {f \ extensional_funcset S T. inj_on f S}" by auto from assms this finite subset show ?thesis by (simp add: card_Diff_subset card_PiE card_extensional_funcset_inj_on prod_constant) qed @@ -71,16 +84,18 @@ "prod f {m..(n::nat)} = (if n < m then 1 else (if n = 0 then f 0 else f n * prod f {m..(n - 1)}))" by auto (auto simp add: gr0_conv_Suc atLeastAtMostSuc_conv) + section \Birthday paradox\ lemma birthday_paradox: assumes "card S = 23" "card T = 365" shows "2 * card {f \ extensional_funcset S T. \ inj_on f S} \ card (extensional_funcset S T)" proof - - from \card S = 23\ \card T = 365\ have "finite S" "finite T" "card S <= card T" by (auto intro: card_ge_0_finite) + from \card S = 23\ \card T = 365\ have "finite S" "finite T" "card S \ card T" + by (auto intro: card_ge_0_finite) from assms show ?thesis using card_PiE[OF \finite S\, of "\i. T"] \finite S\ - card_extensional_funcset_not_inj_on[OF \finite S\ \finite T\ \card S <= card T\] + card_extensional_funcset_not_inj_on[OF \finite S\ \finite T\ \card S \ card T\] by (simp add: fact_div_fact prod_upto_nat_unfold prod_constant) qed diff -r 7e86118f4791 -r d912f97aaa86 src/HOL/ex/Code_Lazy_Demo.thy --- a/src/HOL/ex/Code_Lazy_Demo.thy Fri Oct 25 17:01:23 2024 +0200 +++ b/src/HOL/ex/Code_Lazy_Demo.thy Fri Oct 25 22:22:21 2024 +0200 @@ -113,7 +113,8 @@ = L (\\\) | Node tree tree (infix \\\ 900) -notation (output) Node (\\(//\<^bold>l: _//\<^bold>r: _)\) +notation (output) Node + (\(\indent=1 notation=\mixfix tree node\\\//(\open_block notation=\mixfix tree branch\\\<^bold>l: _)//(\open_block notation=\mixfix tree branch\\\<^bold>r: _))\) code_lazy_type tree diff -r 7e86118f4791 -r d912f97aaa86 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Fri Oct 25 17:01:23 2024 +0200 +++ b/src/Pure/Isar/attrib.ML Fri Oct 25 22:22:21 2024 +0200 @@ -612,7 +612,6 @@ register_config_bool Syntax.ambiguity_warning #> register_config_int Syntax.ambiguity_limit #> register_config_bool Syntax_Trans.eta_contract #> - register_config_bool Syntax_Phases.const_syntax_legacy #> register_config_bool Name_Space.names_long #> register_config_bool Name_Space.names_short #> register_config_bool Name_Space.names_unique #> diff -r 7e86118f4791 -r d912f97aaa86 src/Pure/Syntax/syntax_phases.ML --- a/src/Pure/Syntax/syntax_phases.ML Fri Oct 25 17:01:23 2024 +0200 +++ b/src/Pure/Syntax/syntax_phases.ML Fri Oct 25 22:22:21 2024 +0200 @@ -15,7 +15,6 @@ Position.report_text list * term Exn.result -> Position.report_text list * term Exn.result val parse_ast_pattern: Proof.context -> string * string -> Ast.ast val term_of_typ: Proof.context -> typ -> term - val const_syntax_legacy: bool Config.T val print_checks: Proof.context -> unit val typ_check: int -> string -> (Proof.context -> typ list -> typ list) -> Context.generic -> Context.generic @@ -153,8 +152,6 @@ (* parsetree_to_ast *) -val const_syntax_legacy = Config.declare_bool ("const_syntax_legacy", \<^here>) (K false); - fun parsetree_literals (Parser.Markup (_, ts)) = maps parsetree_literals ts | parsetree_literals (Parser.Node _) = [] | parsetree_literals (Parser.Tip tok) = @@ -224,7 +221,6 @@ val args = maps asts_of pts; fun head () = if not (null ps) andalso (Lexicon.is_fixed a orelse Lexicon.is_const a) - andalso not (Config.get ctxt const_syntax_legacy) then Ast.constrain (Ast.Constant a) (ast_of_pos ps) else Ast.Constant a; val _ = List.app (fn pos => report pos markup_cache a) ps; diff -r 7e86118f4791 -r d912f97aaa86 src/Pure/term_items.ML --- a/src/Pure/term_items.ML Fri Oct 25 17:01:23 2024 +0200 +++ b/src/Pure/term_items.ML Fri Oct 25 22:22:21 2024 +0200 @@ -224,6 +224,13 @@ end; +structure Indexnames: TERM_ITEMS = Term_Items +( + type key = indexname; + val ord = Term_Ord.fast_indexname_ord; +); + + structure Types: sig include TERM_ITEMS diff -r 7e86118f4791 -r d912f97aaa86 src/Pure/type_infer.ML --- a/src/Pure/type_infer.ML Fri Oct 25 17:01:23 2024 +0200 +++ b/src/Pure/type_infer.ML Fri Oct 25 22:22:21 2024 +0200 @@ -65,7 +65,7 @@ fun add_parms tye T = (case deref tye T of Type (_, Ts) => fold (add_parms tye) Ts - | TVar (xi, _) => if is_param xi then insert (op =) xi else I + | TVar (xi, _) => if is_param xi then Indexnames.add_set xi else I | _ => I); fun add_names tye T = @@ -81,9 +81,9 @@ let val used = (fold o fold_types) (add_names tye) ts (fold (add_names tye) Ts (Variable.names_of ctxt)); - val parms = rev ((fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts [])); - val names = Name.invent used ("?" ^ Name.aT) (length parms); - val tab = Vartab.make (parms ~~ names); + val parms = (fold o fold_types) (add_parms tye) ts (fold (add_parms tye) Ts Indexnames.empty); + val names = Name.invent used ("?" ^ Name.aT) (Indexnames.size parms); + val tab = Vartab.make (Indexnames.list_set parms ~~ names); fun finish_typ T = (case deref tye T of