--- a/NEWS Fri Sep 10 23:18:51 2021 +0200
+++ b/NEWS Sat Sep 11 13:04:32 2021 +0200
@@ -248,6 +248,9 @@
adoption; better use TVars.add, TVars.add_tfrees etc. for scalable
accumulation of items.
+* ML antiquotations \<^tvar>\<open>?'a::sort\<close> and \<^var>\<open>?x::type\<close> inline
+corresponding ML values, notably as arguments for Thm.instantiate etc.
+
* The "build" combinators of various data structures help to build
content from bottom-up, by applying an "add" function the "empty" value.
For example:
--- a/etc/symbols Fri Sep 10 23:18:51 2021 +0200
+++ b/etc/symbols Sat Sep 11 13:04:32 2021 +0200
@@ -482,10 +482,12 @@
\<^theory_context> argument: cartouche
\<^tool> argument: cartouche
\<^try> argument: cartouche
+\<^tvar> argument: cartouche
\<^typ> argument: cartouche
\<^type_abbrev> argument: cartouche
\<^type_name> argument: cartouche
\<^type_syntax> argument: cartouche
+\<^var> argument: cartouche
\<^oracle_name> argument: cartouche
\<^code> argument: cartouche
\<^computation> argument: cartouche
--- a/src/HOL/Decision_Procs/approximation.ML Fri Sep 10 23:18:51 2021 +0200
+++ b/src/HOL/Decision_Procs/approximation.ML Sat Sep 11 13:04:32 2021 +0200
@@ -76,9 +76,7 @@
|> Thm.cterm_of ctxt
in
(resolve_tac ctxt [Thm.instantiate (TVars.empty,
- Vars.make [((("n", 0), \<^typ>\<open>nat\<close>), n),
- ((("prec", 0), \<^typ>\<open>nat\<close>), p),
- ((("ss", 0), \<^typ>\<open>nat list\<close>), s)])
+ Vars.make [(\<^var>\<open>?n::nat\<close>, n), (\<^var>\<open>?prec::nat\<close>, p), (\<^var>\<open>?ss::nat list\<close>, s)])
@{thm approx_form}] i
THEN simp_tac (put_simpset (simpset_of \<^context>) ctxt) i) st
end
@@ -94,9 +92,7 @@
|> Thm.cterm_of ctxt
in
resolve_tac ctxt [Thm.instantiate (TVars.empty,
- Vars.make [((("s", 0), \<^typ>\<open>nat\<close>), s),
- ((("t", 0), \<^typ>\<open>nat\<close>), t),
- ((("prec", 0), \<^typ>\<open>nat\<close>), p)])
+ Vars.make [(\<^var>\<open>?s::nat\<close>, s), (\<^var>\<open>?t::nat\<close>, t), (\<^var>\<open>?prec::nat\<close>, p)])
@{thm approx_tse_form}] i st
end
end
--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Fri Sep 10 23:18:51 2021 +0200
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Sat Sep 11 13:04:32 2021 +0200
@@ -476,7 +476,7 @@
fun real_not_eq_conv ct =
let
val (l,r) = dest_eq (Thm.dest_arg ct)
- val th = Thm.instantiate (TVars.empty, Vars.make [((("x", 0), \<^typ>\<open>real\<close>),l),((("y", 0), \<^typ>\<open>real\<close>),r)]) neq_th
+ val th = Thm.instantiate (TVars.empty, Vars.make [(\<^var>\<open>?x::real\<close>,l),(\<^var>\<open>?y::real\<close>,r)]) neq_th
val th_p = poly_conv(Thm.dest_arg(Thm.dest_arg1(Thm.rhs_of th)))
val th_x = Drule.arg_cong_rule \<^cterm>\<open>uminus :: real \<Rightarrow> _\<close> th_p
val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
--- a/src/HOL/Library/cconv.ML Fri Sep 10 23:18:51 2021 +0200
+++ b/src/HOL/Library/cconv.ML Sat Sep 11 13:04:32 2021 +0200
@@ -184,7 +184,7 @@
| _ => cv ct)
fun inst_imp_cong ct =
- Thm.instantiate (TVars.empty, Vars.make [((("A", 0), propT), ct)]) Drule.imp_cong
+ Thm.instantiate (TVars.empty, Vars.make [(\<^var>\<open>?A::prop\<close>, ct)]) Drule.imp_cong
(*rewrite B in A1 \<Longrightarrow> ... \<Longrightarrow> An \<Longrightarrow> B*)
fun concl_cconv 0 cv ct = cv ct
@@ -205,11 +205,11 @@
| SOME (A,B) => strip_prems (i - 1) (A::As) B
val (prem, (prems, concl)) = ct |> Thm.dest_implies ||> strip_prems n []
val rewr_imp_concl =
- Thm.instantiate (TVars.empty, Vars.make [((("C", 0), propT), concl)]) @{thm rewr_imp}
+ Thm.instantiate (TVars.empty, Vars.make [(\<^var>\<open>?C::prop\<close>, concl)]) @{thm rewr_imp}
val th1 = cv prem RS rewr_imp_concl
val nprems = Thm.nprems_of th1
fun inst_cut_rl ct =
- Thm.instantiate (TVars.empty, Vars.make [((("psi", 0), propT), ct)]) cut_rl
+ Thm.instantiate (TVars.empty, Vars.make [(\<^var>\<open>?psi::prop\<close>, ct)]) cut_rl
fun f p th = (th RS inst_cut_rl p)
|> Conv.fconv_rule (Conv.concl_conv nprems (Conv.rewr_conv @{thm imp_cong_eq}))
in fold f prems th1 end
--- a/src/HOL/Tools/Meson/meson_clausify.ML Fri Sep 10 23:18:51 2021 +0200
+++ b/src/HOL/Tools/Meson/meson_clausify.ML Sat Sep 11 13:04:32 2021 +0200
@@ -370,9 +370,9 @@
th ctxt1
val (cnf_ths, ctxt2) = clausify nnf_th
fun intr_imp ct th =
- Thm.instantiate (TVars.empty,
- Vars.make [((("i", 0), \<^typ>\<open>nat\<close>), Thm.cterm_of ctxt2 (HOLogic.mk_nat ax_no))])
- (zero_var_indexes @{thm skolem_COMBK_D})
+ Thm.instantiate
+ (TVars.empty, Vars.make [(\<^var>\<open>?i::nat\<close>, Thm.cterm_of ctxt2 (HOLogic.mk_nat ax_no))])
+ (zero_var_indexes @{thm skolem_COMBK_D})
RS Thm.implies_intr ct th
in
(opt |> Option.map (I #>> singleton (Variable.export ctxt2 ctxt0)
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML Fri Sep 10 23:18:51 2021 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML Sat Sep 11 13:04:32 2021 +0200
@@ -103,7 +103,7 @@
fun inst_excluded_middle i_atom =
@{lemma "P \<Longrightarrow> \<not> P \<Longrightarrow> False" by (rule notE)}
- |> instantiate_normalize (TVars.empty, Vars.make [((("P", 0), \<^typ>\<open>bool\<close>), i_atom)])
+ |> instantiate_normalize (TVars.empty, Vars.make [(\<^var>\<open>?P::bool\<close>, i_atom)])
fun assume_inference ctxt type_enc concealed sym_tab atom =
singleton (hol_terms_of_metis ctxt type_enc concealed sym_tab) (Metis_Term.Fn atom)
--- a/src/HOL/Tools/hologic.ML Fri Sep 10 23:18:51 2021 +0200
+++ b/src/HOL/Tools/hologic.ML Sat Sep 11 13:04:32 2021 +0200
@@ -205,14 +205,14 @@
let
val (P, Q) = apply2 (Object_Logic.dest_judgment ctxt o Thm.cprop_of) (thP, thQ)
handle CTERM (msg, _) => raise THM (msg, 0, [thP, thQ]);
- val inst = (TVars.empty, Vars.make [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]);
+ val inst = (TVars.empty, Vars.make [(\<^var>\<open>?P::bool\<close>, P), (\<^var>\<open>?Q::bool\<close>, Q)]);
in Drule.implies_elim_list (Thm.instantiate inst @{thm conjI}) [thP, thQ] end;
fun conj_elim ctxt thPQ =
let
val (P, Q) = Thm.dest_binop (Object_Logic.dest_judgment ctxt (Thm.cprop_of thPQ))
handle CTERM (msg, _) => raise THM (msg, 0, [thPQ]);
- val inst = (TVars.empty, Vars.make [((("P", 0), boolT), P), ((("Q", 0), boolT), Q)]);
+ val inst = (TVars.empty, Vars.make [(\<^var>\<open>?P::bool\<close>, P), (\<^var>\<open>?Q::bool\<close>, Q)]);
val thP = Thm.implies_elim (Thm.instantiate inst @{thm conjunct1}) thPQ;
val thQ = Thm.implies_elim (Thm.instantiate inst @{thm conjunct2}) thPQ;
in (thP, thQ) end;
--- a/src/HOL/Tools/lin_arith.ML Fri Sep 10 23:18:51 2021 +0200
+++ b/src/HOL/Tools/lin_arith.ML Sat Sep 11 13:04:32 2021 +0200
@@ -60,9 +60,8 @@
fun is_nat t = (fastype_of1 t = HOLogic.natT);
fun mk_nat_thm thy t =
- let val ct = Thm.global_cterm_of thy t in
- Drule.instantiate_normalize (TVars.empty, Vars.make [((("n", 0), HOLogic.natT), ct)]) @{thm le0}
- end;
+ let val ct = Thm.global_cterm_of thy t
+ in Drule.instantiate_normalize (TVars.empty, Vars.make [(\<^var>\<open>?n::nat\<close>, ct)]) @{thm le0} end;
end;
--- a/src/HOL/Tools/record.ML Fri Sep 10 23:18:51 2021 +0200
+++ b/src/HOL/Tools/record.ML Sat Sep 11 13:04:32 2021 +0200
@@ -1771,8 +1771,7 @@
fun mk_eq_refl ctxt =
@{thm equal_refl}
|> Thm.instantiate
- (TVars.make [((("'a", 0), \<^sort>\<open>equal\<close>), Thm.ctyp_of ctxt (Logic.varifyT_global extT))],
- Vars.empty)
+ (TVars.make [(\<^tvar>\<open>?'a::equal\<close>, Thm.ctyp_of ctxt (Logic.varifyT_global extT))], Vars.empty)
|> Axclass.unoverload ctxt;
val ensure_random_record = ensure_sort_record (\<^sort>\<open>random\<close>, mk_random_eq);
val ensure_exhaustive_record =
--- a/src/HOL/Tools/sat.ML Fri Sep 10 23:18:51 2021 +0200
+++ b/src/HOL/Tools/sat.ML Sat Sep 11 13:04:32 2021 +0200
@@ -171,8 +171,7 @@
val cLit =
snd (Thm.dest_comb (if hyp1_is_neg then hyp2 else hyp1)) (* strip Trueprop *)
in
- Thm.instantiate (TVars.empty, Vars.make [((("P", 0), HOLogic.boolT), cLit)])
- resolution_thm
+ Thm.instantiate (TVars.empty, Vars.make [(\<^var>\<open>?P::bool\<close>, cLit)]) resolution_thm
end
val _ =
--- a/src/Pure/ML/ml_antiquotations1.ML Fri Sep 10 23:18:51 2021 +0200
+++ b/src/Pure/ML/ml_antiquotations1.ML Sat Sep 11 13:04:32 2021 +0200
@@ -88,6 +88,26 @@
ML_Syntax.print_string (Thm.check_oracle ctxt (name, pos)))));
+(* schematic variables *)
+
+val schematic_input =
+ Args.context -- Scan.lift Args.embedded_input >> (fn (ctxt, src) =>
+ (Proof_Context.set_mode Proof_Context.mode_schematic ctxt,
+ (Syntax.implode_input src, Input.pos_of src)));
+
+val _ = Theory.setup
+ (ML_Antiquotation.inline_embedded \<^binding>\<open>tvar\<close>
+ (schematic_input >> (fn (ctxt, (s, pos)) =>
+ (case Syntax.read_typ ctxt s of
+ TVar v => ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_sort v
+ | _ => error ("Schematic type variable expected" ^ Position.here pos)))) #>
+ ML_Antiquotation.inline_embedded \<^binding>\<open>var\<close>
+ (schematic_input >> (fn (ctxt, (s, pos)) =>
+ (case Syntax.read_term ctxt s of
+ Var v => ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_typ v
+ | _ => error ("Schematic variable expected" ^ Position.here pos)))));
+
+
(* type classes *)
fun class syn = Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) =>
--- a/src/ZF/Tools/inductive_package.ML Fri Sep 10 23:18:51 2021 +0200
+++ b/src/ZF/Tools/inductive_package.ML Sat Sep 11 13:04:32 2021 +0200
@@ -508,8 +508,8 @@
The name "x.1" comes from the "RS spec" !*)
val inst =
case elem_frees of [_] => I
- | _ => Drule.instantiate_normalize (TVars.empty, Vars.make [(((("x",1), Ind_Syntax.iT)),
- Thm.global_cterm_of thy4 elem_tuple)]);
+ | _ => Drule.instantiate_normalize (TVars.empty,
+ Vars.make [(\<^var>\<open>?x1::i\<close>, Thm.global_cterm_of thy4 elem_tuple)]);
(*strip quantifier and the implication*)
val induct0 = inst (quant_induct RS @{thm spec} RSN (2, @{thm rev_mp}));