# HG changeset patch # User nipkow # Date 1582045691 -3600 # Node ID dd7e398a04ae351b88a546d591fd99f490d9f762 # Parent 09c850e82258086f26d459b0814eeef8a1a6fc25# Parent d6e139438e4acba106398b22377364e45d272555 merged diff -r d6e139438e4a -r dd7e398a04ae src/HOL/Library/Ramsey.thy --- a/src/HOL/Library/Ramsey.thy Tue Feb 18 18:08:08 2020 +0100 +++ b/src/HOL/Library/Ramsey.thy Tue Feb 18 18:08:11 2020 +0100 @@ -21,6 +21,12 @@ lemma nsets_2_eq: "nsets A 2 = (\x\A. \y\A - {x}. {{x, y}})" by (auto simp: nsets_def card_2_iff) +lemma nsets_doubleton_2_eq [simp]: "[{x, y}]\<^bsup>2\<^esup> = (if x=y then {} else {{x, y}})" + by (auto simp: nsets_2_eq) + +lemma doubleton_in_nsets_2 [simp]: "{x,y} \ [A]\<^bsup>2\<^esup> \ x \ A \ y \ A \ x \ y" + by (auto simp: nsets_2_eq Set.doubleton_eq_iff) + lemma binomial_eq_nsets: "n choose k = card (nsets {0.. nsets {..finite A; card A < r\ \ nsets A r = {}" by (simp add: nsets_eq_empty_iff) lemma nsets_empty_iff: "nsets {} r = (if r=0 then {{}} else {})" @@ -79,6 +85,29 @@ by (auto simp: bij_betw_def inj_on_nsets) qed +lemma nset_image_obtains: + assumes "X \ [f`A]\<^bsup>k\<^esup>" "inj_on f A" + obtains Y where "Y \ [A]\<^bsup>k\<^esup>" "X = f ` Y" + using assms + apply (clarsimp simp add: nsets_def subset_image_iff) + by (metis card_image finite_imageD inj_on_subset) + +lemma nsets_image_funcset: + assumes "g \ S \ T" and "inj_on g S" + shows "(\X. g ` X) \ [S]\<^bsup>k\<^esup> \ [T]\<^bsup>k\<^esup>" + using assms + by (fastforce simp add: nsets_def card_image inj_on_subset subset_iff simp flip: image_subset_iff_funcset) + +lemma nsets_compose_image_funcset: + assumes f: "f \ [T]\<^bsup>k\<^esup> \ D" and "g \ S \ T" and "inj_on g S" + shows "f \ (\X. g ` X) \ [S]\<^bsup>k\<^esup> \ D" +proof - + have "(\X. g ` X) \ [S]\<^bsup>k\<^esup> \ [T]\<^bsup>k\<^esup>" + using assms by (simp add: nsets_image_funcset) + then show ?thesis + using f by fastforce +qed + subsubsection \Partition predicates\ definition partn :: "'a set \ nat \ nat \ 'b set \ bool" diff -r d6e139438e4a -r dd7e398a04ae src/HOL/Num.thy --- a/src/HOL/Num.thy Tue Feb 18 18:08:08 2020 +0100 +++ b/src/HOL/Num.thy Tue Feb 18 18:08:11 2020 +0100 @@ -1107,8 +1107,11 @@ lemma less_2_cases: "n < 2 \ n = 0 \ n = Suc 0" by (auto simp add: numeral_2_eq_2) +lemma less_2_cases_iff: "n < 2 \ n = 0 \ n = Suc 0" + by (auto simp add: numeral_2_eq_2) + text \Removal of Small Numerals: 0, 1 and (in additive positions) 2.\ -text \bh: Are these rules really a good idea?\ +text \bh: Are these rules really a good idea? LCP: well, it already happens for 0 and 1!\ lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)" by simp diff -r d6e139438e4a -r dd7e398a04ae src/Pure/ML/ml_syntax.ML --- a/src/Pure/ML/ml_syntax.ML Tue Feb 18 18:08:08 2020 +0100 +++ b/src/Pure/ML/ml_syntax.ML Tue Feb 18 18:08:11 2020 +0100 @@ -128,8 +128,9 @@ fun pretty_string max_len str = let val body = - maps (fn XML.Elem _ => [""] | XML.Text s => Symbol.explode s) (YXML.parse_body str) - handle Fail _ => Symbol.explode str; + if YXML.is_wellformed str then + maps (fn XML.Elem _ => [""] | XML.Text s => Symbol.explode s) (YXML.parse_body str) + else Symbol.explode str; val body' = if length body <= max_len then body else take (Int.max (max_len, 0)) body @ ["..."]; diff -r d6e139438e4a -r dd7e398a04ae src/Pure/PIDE/yxml.ML --- a/src/Pure/PIDE/yxml.ML Tue Feb 18 18:08:08 2020 +0100 +++ b/src/Pure/PIDE/yxml.ML Tue Feb 18 18:08:11 2020 +0100 @@ -29,6 +29,7 @@ val parse_body: string -> XML.body val parse: string -> XML.tree val content_of: string -> string + val is_wellformed: string -> bool end; structure YXML: YXML = @@ -158,5 +159,7 @@ val content_of = parse_body #> XML.content_of; +fun is_wellformed s = string_of_body (parse_body s) = s + handle Fail _ => false; + end; - diff -r d6e139438e4a -r dd7e398a04ae src/Pure/sorts.ML --- a/src/Pure/sorts.ML Tue Feb 18 18:08:08 2020 +0100 +++ b/src/Pure/sorts.ML Tue Feb 18 18:08:11 2020 +0100 @@ -37,7 +37,6 @@ val inter_sort: algebra -> sort * sort -> sort val minimize_sort: algebra -> sort -> sort val complete_sort: algebra -> sort -> sort - val minimal_sorts: algebra -> sort list -> sort Ord_List.T val add_class: Context.generic -> class * class list -> algebra -> algebra val add_classrel: Context.generic -> class * class -> algebra -> algebra val add_arities: Context.generic -> string * (class * sort list) list -> algebra -> algebra @@ -177,12 +176,6 @@ fun complete_sort algebra = Graph.all_succs (classes_of algebra) o minimize_sort algebra; -fun minimal_sorts algebra raw_sorts = - let - fun le S1 S2 = sort_le algebra (S1, S2); - val sorts = make (map (minimize_sort algebra) raw_sorts); - in sorts |> filter_out (fn S => exists (fn S' => le S' S andalso not (le S S')) sorts) end; - (** build algebras **) diff -r d6e139438e4a -r dd7e398a04ae src/Pure/thm.ML --- a/src/Pure/thm.ML Tue Feb 18 18:08:08 2020 +0100 +++ b/src/Pure/thm.ML Tue Feb 18 18:08:11 2020 +0100 @@ -1694,27 +1694,43 @@ end |> solve_constraints; (*Remove extra sorts that are witnessed by type signature information*) -fun strip_shyps0 (thm as Thm (_, {shyps = [], ...})) = thm - | strip_shyps0 (thm as Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop})) = +fun strip_shyps thm = + (case thm of + Thm (_, {shyps = [], ...}) => thm + | Thm (der, {cert, tags, maxidx, constraints, shyps, hyps, tpairs, prop}) => let val thy = theory_of_thm thm; + val algebra = Sign.classes_of thy; + val minimize = Sorts.minimize_sort algebra; + val le = Sorts.sort_le algebra; + fun lt (S1, S2) = le (S1, S2) andalso not (le (S2, S1)); + fun rel (S1, S2) = if S1 = S2 then [] else [(Term.aT S1, S2)]; val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm []; val extra = fold (Sorts.remove_sort o #2) present shyps; val witnessed = Sign.witness_sorts thy present extra; - val extra' = fold (Sorts.remove_sort o #2) witnessed extra - |> Sorts.minimal_sorts algebra; - val constraints' = fold (insert_constraints thy) witnessed constraints; + val non_witnessed = fold (Sorts.remove_sort o #2) witnessed extra |> map (`minimize); + + val extra' = + non_witnessed |> map_filter (fn (S, _) => + if non_witnessed |> exists (fn (S', _) => lt (S', S)) then NONE else SOME S) + |> Sorts.make; + + val constrs' = + non_witnessed |> maps (fn (S1, S2) => + let val S0 = the (find_first (fn S => le (S, S1)) extra') + in rel (S0, S1) @ rel (S1, S2) end); + + val constraints' = fold (insert_constraints thy) (witnessed @ constrs') constraints; val shyps' = fold (Sorts.insert_sort o #2) present extra'; in Thm (deriv_rule_unconditional (Proofterm.strip_shyps_proof algebra present witnessed extra') der, {cert = cert, tags = tags, maxidx = maxidx, constraints = constraints', shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop}) - end; - -val strip_shyps = solve_constraints #> strip_shyps0 #> solve_constraints; + end) + |> solve_constraints; (*Internalize sort constraints of type variables*)