--- a/NEWS Wed Jan 26 16:49:56 2022 +0100
+++ b/NEWS Thu Jan 27 08:52:24 2022 +0100
@@ -56,6 +56,9 @@
- Added option "-y" for a dry run.
- Renamed run_action to run in Mirabelle.action record. Minor INCOMPATIBILITY.
+* Meson
+ - Added support for polymorphic "using" facts. Minor INCOMPATIBILITY.
+
*** System ***
--- a/src/HOL/Library/More_List.thy Wed Jan 26 16:49:56 2022 +0100
+++ b/src/HOL/Library/More_List.thy Thu Jan 27 08:52:24 2022 +0100
@@ -91,11 +91,11 @@
where
"no_leading P xs \<longleftrightarrow> (xs \<noteq> [] \<longrightarrow> \<not> P (hd xs))"
-lemma no_leading_Nil [simp, intro!]:
+lemma no_leading_Nil [iff]:
"no_leading P []"
by (simp add: no_leading_def)
-lemma no_leading_Cons [simp, intro!]:
+lemma no_leading_Cons [iff]:
"no_leading P (x # xs) \<longleftrightarrow> \<not> P x"
by (simp add: no_leading_def)
@@ -148,7 +148,7 @@
"no_trailing P xs \<longleftrightarrow> (xs \<noteq> [] \<longrightarrow> \<not> P (last xs))"
by (induct xs) simp_all
-lemma no_trailing_Nil [simp, intro!]:
+lemma no_trailing_Nil [iff]:
"no_trailing P []"
by simp
--- a/src/HOL/Tools/Meson/meson_tactic.ML Wed Jan 26 16:49:56 2022 +0100
+++ b/src/HOL/Tools/Meson/meson_tactic.ML Thu Jan 27 08:52:24 2022 +0100
@@ -20,10 +20,20 @@
false true 0) ths)
end
+(* This is part of a workaround to avoid freezing schematic variables in \<^text>\<open>using\<close> facts. See
+ \<^file>\<open>~~/src/HOL/Tools/Metis/metis_tactic.ML\<close> for details. *)
+val has_tvar = exists_type (exists_subtype (fn TVar _ => true | _ => false)) o Thm.prop_of
+
val _ =
Theory.setup
- (Method.setup \<^binding>\<open>meson\<close> (Attrib.thms >> (fn ths => fn ctxt =>
- SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
+ (Method.setup \<^binding>\<open>meson\<close> (Attrib.thms >> (fn ths => fn ctxt0 =>
+ CONTEXT_METHOD (fn facts => fn (ctxt, st) =>
+ let val (schem_facts, nonschem_facts) = List.partition has_tvar facts in
+ st
+ |> HEADGOAL (Method.insert_tac ctxt nonschem_facts THEN'
+ CHANGED_PROP o meson_general_tac ctxt0 (schem_facts @ ths))
+ |> TACTIC_CONTEXT ctxt
+ end)))
"MESON resolution proof procedure")
end;