--- 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 = (\<Union>x\<in>A. \<Union>y\<in>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} \<in> [A]\<^bsup>2\<^esup> \<longleftrightarrow> x \<in> A \<and> y \<in> A \<and> x \<noteq> y"
+ by (auto simp: nsets_2_eq Set.doubleton_eq_iff)
+
lemma binomial_eq_nsets: "n choose k = card (nsets {0..<n} k)"
apply (simp add: binomial_def nsets_def)
by (meson subset_eq_atLeast0_lessThan_finite)
@@ -41,7 +47,7 @@
using that card_mono leD by auto
qed
-lemma nsets_eq_empty: "n < r \<Longrightarrow> nsets {..<n} r = {}"
+lemma nsets_eq_empty: "\<lbrakk>finite A; card A < r\<rbrakk> \<Longrightarrow> 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 \<in> [f`A]\<^bsup>k\<^esup>" "inj_on f A"
+ obtains Y where "Y \<in> [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 \<in> S \<rightarrow> T" and "inj_on g S"
+ shows "(\<lambda>X. g ` X) \<in> [S]\<^bsup>k\<^esup> \<rightarrow> [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 \<in> [T]\<^bsup>k\<^esup> \<rightarrow> D" and "g \<in> S \<rightarrow> T" and "inj_on g S"
+ shows "f \<circ> (\<lambda>X. g ` X) \<in> [S]\<^bsup>k\<^esup> \<rightarrow> D"
+proof -
+ have "(\<lambda>X. g ` X) \<in> [S]\<^bsup>k\<^esup> \<rightarrow> [T]\<^bsup>k\<^esup>"
+ using assms by (simp add: nsets_image_funcset)
+ then show ?thesis
+ using f by fastforce
+qed
+
subsubsection \<open>Partition predicates\<close>
definition partn :: "'a set \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'b set \<Rightarrow> bool"
--- 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 \<Longrightarrow> n = 0 \<or> n = Suc 0"
by (auto simp add: numeral_2_eq_2)
+lemma less_2_cases_iff: "n < 2 \<longleftrightarrow> n = 0 \<or> n = Suc 0"
+ by (auto simp add: numeral_2_eq_2)
+
text \<open>Removal of Small Numerals: 0, 1 and (in additive positions) 2.\<close>
-text \<open>bh: Are these rules really a good idea?\<close>
+text \<open>bh: Are these rules really a good idea? LCP: well, it already happens for 0 and 1!\<close>
lemma add_2_eq_Suc [simp]: "2 + n = Suc (Suc n)"
by simp
--- 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 _ => ["<markup>"] | 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 _ => ["<markup>"] | 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 @ ["..."];
--- 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;
-
--- 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 **)
--- 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*)