# HG changeset patch # User wenzelm # Date 1631358272 -7200 # Node ID b2ad24b5a42cef8e94918f907099cbf9c2664aeb # Parent 7492cd35782ebb54a0adc4d98eec9922879941a5 more antiquotations; diff -r 7492cd35782e -r b2ad24b5a42c NEWS --- 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>\?'a::sort\ and \<^var>\?x::type\ 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: diff -r 7492cd35782e -r b2ad24b5a42c etc/symbols --- 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 diff -r 7492cd35782e -r b2ad24b5a42c src/HOL/Decision_Procs/approximation.ML --- 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>\nat\), n), - ((("prec", 0), \<^typ>\nat\), p), - ((("ss", 0), \<^typ>\nat list\), s)]) + Vars.make [(\<^var>\?n::nat\, n), (\<^var>\?prec::nat\, p), (\<^var>\?ss::nat list\, 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>\nat\), s), - ((("t", 0), \<^typ>\nat\), t), - ((("prec", 0), \<^typ>\nat\), p)]) + Vars.make [(\<^var>\?s::nat\, s), (\<^var>\?t::nat\, t), (\<^var>\?prec::nat\, p)]) @{thm approx_tse_form}] i st end end diff -r 7492cd35782e -r b2ad24b5a42c src/HOL/Library/Sum_of_Squares/positivstellensatz.ML --- 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>\real\),l),((("y", 0), \<^typ>\real\),r)]) neq_th + val th = Thm.instantiate (TVars.empty, Vars.make [(\<^var>\?x::real\,l),(\<^var>\?y::real\,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>\uminus :: real \ _\ th_p val th_n = fconv_rule (arg_conv poly_neg_conv) th_x diff -r 7492cd35782e -r b2ad24b5a42c src/HOL/Library/cconv.ML --- 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>\?A::prop\, ct)]) Drule.imp_cong (*rewrite B in A1 \ ... \ An \ 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>\?C::prop\, 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>\?psi::prop\, 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 diff -r 7492cd35782e -r b2ad24b5a42c src/HOL/Tools/Meson/meson_clausify.ML --- 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>\nat\), Thm.cterm_of ctxt2 (HOLogic.mk_nat ax_no))]) - (zero_var_indexes @{thm skolem_COMBK_D}) + Thm.instantiate + (TVars.empty, Vars.make [(\<^var>\?i::nat\, 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) diff -r 7492cd35782e -r b2ad24b5a42c src/HOL/Tools/Metis/metis_reconstruct.ML --- 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 \ \ P \ False" by (rule notE)} - |> instantiate_normalize (TVars.empty, Vars.make [((("P", 0), \<^typ>\bool\), i_atom)]) + |> instantiate_normalize (TVars.empty, Vars.make [(\<^var>\?P::bool\, 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) diff -r 7492cd35782e -r b2ad24b5a42c src/HOL/Tools/hologic.ML --- 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>\?P::bool\, P), (\<^var>\?Q::bool\, 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>\?P::bool\, P), (\<^var>\?Q::bool\, 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; diff -r 7492cd35782e -r b2ad24b5a42c src/HOL/Tools/lin_arith.ML --- 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>\?n::nat\, ct)]) @{thm le0} end; end; diff -r 7492cd35782e -r b2ad24b5a42c src/HOL/Tools/record.ML --- 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>\equal\), Thm.ctyp_of ctxt (Logic.varifyT_global extT))], - Vars.empty) + (TVars.make [(\<^tvar>\?'a::equal\, Thm.ctyp_of ctxt (Logic.varifyT_global extT))], Vars.empty) |> Axclass.unoverload ctxt; val ensure_random_record = ensure_sort_record (\<^sort>\random\, mk_random_eq); val ensure_exhaustive_record = diff -r 7492cd35782e -r b2ad24b5a42c src/HOL/Tools/sat.ML --- 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>\?P::bool\, cLit)]) resolution_thm end val _ = diff -r 7492cd35782e -r b2ad24b5a42c src/Pure/ML/ml_antiquotations1.ML --- 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>\tvar\ + (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>\var\ + (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) => diff -r 7492cd35782e -r b2ad24b5a42c src/ZF/Tools/inductive_package.ML --- 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>\?x1::i\, 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}));