--- a/src/Doc/Codegen/Computations.thy Mon Oct 25 13:56:08 2021 +0100
+++ b/src/Doc/Codegen/Computations.thy Mon Oct 25 23:10:06 2021 +0200
@@ -272,8 +272,9 @@
ML %quote \<open>
local
- fun raw_dvd (b, ct) = Thm.mk_binop \<^cterm>\<open>Pure.eq :: bool \<Rightarrow> bool \<Rightarrow> prop\<close>
- ct (if b then \<^cterm>\<open>True\<close> else \<^cterm>\<open>False\<close>);
+ fun raw_dvd (b, ct) =
+ \<^instantiate>\<open>x = ct and y = \<open>if b then \<^cterm>\<open>True\<close> else \<^cterm>\<open>False\<close>\<close>
+ in cterm \<open>x \<equiv> y\<close> for x y :: bool\<close>;
val (_, dvd_oracle) = Context.>>> (Context.map_theory_result
(Thm.add_oracle (\<^binding>\<open>dvd\<close>, raw_dvd)));
--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Mon Oct 25 13:56:08 2021 +0100
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML Mon Oct 25 23:10:06 2021 +0200
@@ -285,14 +285,16 @@
val (a, b) = Rat.dest x
in
if b = 1 then Numeral.mk_cnumber \<^ctyp>\<open>real\<close> a
- else Thm.apply (Thm.apply \<^cterm>\<open>(/) :: real \<Rightarrow> _\<close>
- (Numeral.mk_cnumber \<^ctyp>\<open>real\<close> a))
- (Numeral.mk_cnumber \<^ctyp>\<open>real\<close> b)
+ else
+ \<^instantiate>\<open>
+ a = \<open>Numeral.mk_cnumber \<^ctyp>\<open>real\<close> a\<close> and
+ b = \<open>Numeral.mk_cnumber \<^ctyp>\<open>real\<close> b\<close>
+ in cterm \<open>a / b\<close> for a b :: real\<close>
end;
fun dest_ratconst t =
case Thm.term_of t of
- Const(\<^const_name>\<open>divide\<close>, _)$a$b => Rat.make(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
+ \<^Const_>\<open>divide _ for a b\<close> => Rat.make(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd)
| _ => Rat.of_int (HOLogic.dest_number (Thm.term_of t) |> snd)
fun is_ratconst t = can dest_ratconst t
@@ -319,8 +321,9 @@
(* Map back polynomials to HOL. *)
-fun cterm_of_varpow x k = if k = 1 then x else Thm.apply (Thm.apply \<^cterm>\<open>(^) :: real \<Rightarrow> _\<close> x)
- (Numeral.mk_cnumber \<^ctyp>\<open>nat\<close> k)
+fun cterm_of_varpow x k =
+ if k = 1 then x
+ else \<^instantiate>\<open>x and k = \<open>Numeral.mk_cnumber \<^ctyp>\<open>nat\<close> k\<close> in cterm \<open>x ^ k\<close> for x :: real\<close>
fun cterm_of_monomial m =
if FuncUtil.Ctermfunc.is_empty m then \<^cterm>\<open>1::real\<close>
@@ -328,13 +331,13 @@
let
val m' = FuncUtil.dest_monomial m
val vps = fold_rev (fn (x,k) => cons (cterm_of_varpow x k)) m' []
- in foldr1 (fn (s, t) => Thm.apply (Thm.apply \<^cterm>\<open>(*) :: real \<Rightarrow> _\<close> s) t) vps
+ in foldr1 (fn (s, t) => \<^instantiate>\<open>s and t in cterm \<open>s * t\<close> for s t :: real\<close>) vps
end
fun cterm_of_cmonomial (m,c) =
if FuncUtil.Ctermfunc.is_empty m then cterm_of_rat c
else if c = @1 then cterm_of_monomial m
- else Thm.apply (Thm.apply \<^cterm>\<open>(*)::real \<Rightarrow> _\<close> (cterm_of_rat c)) (cterm_of_monomial m);
+ else \<^instantiate>\<open>x = \<open>cterm_of_rat c\<close> and y = \<open>cterm_of_monomial m\<close> in cterm \<open>x * y\<close> for x y :: real\<close>;
fun cterm_of_poly p =
if FuncUtil.Monomialfunc.is_empty p then \<^cterm>\<open>0::real\<close>
@@ -342,7 +345,7 @@
let
val cms = map cterm_of_cmonomial
(sort (prod_ord FuncUtil.monomial_order (K EQUAL)) (FuncUtil.Monomialfunc.dest p))
- in foldr1 (fn (t1, t2) => Thm.apply(Thm.apply \<^cterm>\<open>(+) :: real \<Rightarrow> _\<close> t1) t2) cms
+ in foldr1 (fn (t1, t2) => \<^instantiate>\<open>t1 and t2 in cterm \<open>t1 + t2\<close> for t1 t2 :: real\<close>) cms
end;
(* A general real arithmetic prover *)
@@ -400,15 +403,15 @@
Axiom_eq n => nth eqs n
| Axiom_le n => nth les n
| Axiom_lt n => nth lts n
- | Rational_eq x => eqT_elim(numeric_eq_conv(Thm.apply \<^cterm>\<open>Trueprop\<close>
- (Thm.apply (Thm.apply \<^cterm>\<open>(=)::real \<Rightarrow> _\<close> (mk_numeric x))
- \<^cterm>\<open>0::real\<close>)))
- | Rational_le x => eqT_elim(numeric_ge_conv(Thm.apply \<^cterm>\<open>Trueprop\<close>
- (Thm.apply (Thm.apply \<^cterm>\<open>(\<le>)::real \<Rightarrow> _\<close>
- \<^cterm>\<open>0::real\<close>) (mk_numeric x))))
- | Rational_lt x => eqT_elim(numeric_gt_conv(Thm.apply \<^cterm>\<open>Trueprop\<close>
- (Thm.apply (Thm.apply \<^cterm>\<open>(<)::real \<Rightarrow> _\<close> \<^cterm>\<open>0::real\<close>)
- (mk_numeric x))))
+ | Rational_eq x =>
+ eqT_elim (numeric_eq_conv
+ \<^instantiate>\<open>x = \<open>mk_numeric x\<close> in cprop \<open>x = 0\<close> for x :: real\<close>)
+ | Rational_le x =>
+ eqT_elim (numeric_ge_conv
+ \<^instantiate>\<open>x = \<open>mk_numeric x\<close> in cprop \<open>x \<ge> 0\<close> for x :: real\<close>)
+ | Rational_lt x =>
+ eqT_elim (numeric_gt_conv
+ \<^instantiate>\<open>x = \<open>mk_numeric x\<close> in cprop \<open>x > 0\<close> for x :: real\<close>)
| Square pt => square_rule (cterm_of_poly pt)
| Eqmul(pt,p) => emul_rule (cterm_of_poly pt) (translate p)
| Sum(p1,p2) => add_rule (translate p1) (translate p2)
@@ -438,8 +441,8 @@
else error "disj_cases : conclusions not alpha convertible"
in Thm.implies_elim (Thm.implies_elim
(Thm.implies_elim (Thm.instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
- (Thm.implies_intr (Thm.apply \<^cterm>\<open>Trueprop\<close> p) th1))
- (Thm.implies_intr (Thm.apply \<^cterm>\<open>Trueprop\<close> q) th2)
+ (Thm.implies_intr \<^instantiate>\<open>p in cprop p\<close> th1))
+ (Thm.implies_intr \<^instantiate>\<open>q in cprop q\<close> th2)
end
fun overall cert_choice dun ths =
case ths of
@@ -481,8 +484,8 @@
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
val th' = Drule.binop_cong_rule \<^cterm>\<open>HOL.disj\<close>
- (Drule.arg_cong_rule (Thm.apply \<^cterm>\<open>(<)::real \<Rightarrow> _\<close> \<^cterm>\<open>0::real\<close>) th_p)
- (Drule.arg_cong_rule (Thm.apply \<^cterm>\<open>(<)::real \<Rightarrow> _\<close> \<^cterm>\<open>0::real\<close>) th_n)
+ (Drule.arg_cong_rule \<^cterm>\<open>(<) (0::real)\<close> th_p)
+ (Drule.arg_cong_rule \<^cterm>\<open>(<) (0::real)\<close> th_n)
in Thm.transitive th th'
end
fun equal_implies_1_rule PQ =
@@ -495,7 +498,7 @@
let
fun h (acc, t) =
case Thm.term_of t of
- Const(\<^const_name>\<open>Ex\<close>,_)$Abs(_,_,_) =>
+ \<^Const_>\<open>Ex _ for \<open>Abs _\<close>\<close> =>
h (Thm.dest_abs_global (Thm.dest_arg t) |>> (fn v => v::acc))
| _ => (acc,t)
in fn t => h ([],t)
@@ -508,39 +511,38 @@
fun mk_forall x th =
let
- val T = Thm.typ_of_cterm x
- val all = Thm.cterm_of ctxt (Const (\<^const_name>\<open>All\<close>, (T --> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>bool\<close>))
+ val T = Thm.ctyp_of_cterm x
+ val all = \<^instantiate>\<open>'a = T in cterm All\<close>
in Drule.arg_cong_rule all (Thm.abstract_rule (name_of x) x th) end
val specl = fold_rev (fn x => fn th => Thm.instantiate' [] [SOME x] (th RS spec));
- fun ext T = Thm.cterm_of ctxt (Const (\<^const_name>\<open>Ex\<close>, (T --> \<^typ>\<open>bool\<close>) --> \<^typ>\<open>bool\<close>))
- fun mk_ex v t = Thm.apply (ext (Thm.typ_of_cterm v)) (Thm.lambda v t)
+ fun mk_ex v t =
+ \<^instantiate>\<open>'a = \<open>Thm.ctyp_of_cterm v\<close> and P = \<open>Thm.lambda v t\<close>
+ in cprop \<open>Ex P\<close> for P :: \<open>'a \<Rightarrow> bool\<close>\<close>
fun choose v th th' =
case Thm.concl_of th of
- \<^term>\<open>Trueprop\<close> $ (Const(\<^const_name>\<open>Ex\<close>,_)$_) =>
- let
- val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
- val T = Thm.dest_ctyp0 (Thm.ctyp_of_cterm p)
- val th0 = fconv_rule (Thm.beta_conversion true)
- (Thm.instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
- val pv = (Thm.rhs_of o Thm.beta_conversion true)
- (Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.apply p v))
- val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
- in Thm.implies_elim (Thm.implies_elim th0 th) th1 end
+ \<^Const_>\<open>Trueprop for \<^Const_>\<open>Ex _ for _\<close>\<close> =>
+ let
+ val p = (funpow 2 Thm.dest_arg o Thm.cprop_of) th
+ val T = Thm.dest_ctyp0 (Thm.ctyp_of_cterm p)
+ val th0 = fconv_rule (Thm.beta_conversion true)
+ (Thm.instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o Thm.cprop_of) th'] exE)
+ val pv = (Thm.rhs_of o Thm.beta_conversion true)
+ (Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.apply p v))
+ val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
+ in Thm.implies_elim (Thm.implies_elim th0 th) th1 end
| _ => raise THM ("choose",0,[th, th'])
fun simple_choose v th =
- choose v
- (Thm.assume
- ((Thm.apply \<^cterm>\<open>Trueprop\<close> o mk_ex v) (Thm.dest_arg (hd (Thm.chyps_of th))))) th
+ choose v (Thm.assume (mk_ex v (Thm.dest_arg (hd (Thm.chyps_of th))))) th
val strip_forall =
let
fun h (acc, t) =
case Thm.term_of t of
- Const(\<^const_name>\<open>All\<close>,_)$Abs(_,_,_) =>
+ \<^Const_>\<open>All _ for \<open>Abs _\<close>\<close> =>
h (Thm.dest_abs_global (Thm.dest_arg t) |>> (fn v => v::acc))
| _ => (acc,t)
in fn t => h ([],t)
@@ -558,7 +560,7 @@
fun absremover ct = (literals_conv [\<^term>\<open>HOL.conj\<close>, \<^term>\<open>HOL.disj\<close>] []
(try_conv (absconv1 then_conv binop_conv (arg_conv poly_conv))) then_conv
try_conv (absconv2 then_conv nnf_norm_conv' then_conv binop_conv absremover)) ct
- val nct = Thm.apply \<^cterm>\<open>Trueprop\<close> (Thm.apply \<^cterm>\<open>Not\<close> ct)
+ val nct = \<^instantiate>\<open>A = ct in cprop \<open>\<not> A\<close>\<close>
val th0 = (init_conv then_conv arg_conv nnf_norm_conv') nct
val tm0 = Thm.dest_arg (Thm.rhs_of th0)
val (th, certificates) =
@@ -688,8 +690,8 @@
fun is_alien ct =
case Thm.term_of ct of
- Const(\<^const_name>\<open>of_nat\<close>, _)$ n => not (can HOLogic.dest_number n)
- | Const(\<^const_name>\<open>of_int\<close>, _)$ n => not (can HOLogic.dest_number n)
+ \<^Const_>\<open>of_nat _ for n\<close> => not (can HOLogic.dest_number n)
+ | \<^Const_>\<open>of_int _ for n\<close> => not (can HOLogic.dest_number n)
| _ => false
in
fun real_linear_prover translator (eq,le,lt) =
--- a/src/HOL/Tools/BNF/bnf_comp.ML Mon Oct 25 13:56:08 2021 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Mon Oct 25 23:10:06 2021 +0200
@@ -153,15 +153,10 @@
"_permute_" ^ implode (map string_of_int src) ^ "_" ^ implode (map string_of_int dest);
-(*copied from Envir.expand_term_free*)
-fun expand_term_const defs =
- let
- val eqs = map ((fn ((x, U), u) => (x, (U, u))) o apfst dest_Const) defs;
- val get = fn Const (x, _) => AList.lookup (op =) eqs x | _ => NONE;
- in Envir.expand_term get end;
-
val id_bnf_def = @{thm id_bnf_def};
-val expand_id_bnf_def = expand_term_const [Thm.prop_of id_bnf_def |> Logic.dest_equals];
+val expand_id_bnf_def =
+ Envir.expand_term_defs dest_Const
+ [Thm.prop_of id_bnf_def |> Logic.dest_equals |> apfst dest_Const];
fun is_sum_prod_natLeq (Const (\<^const_name>\<open>csum\<close>, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
| is_sum_prod_natLeq (Const (\<^const_name>\<open>cprod\<close>, _) $ t $ u) = forall is_sum_prod_natLeq [t, u]
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Mon Oct 25 13:56:08 2021 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Mon Oct 25 23:10:06 2021 +0200
@@ -65,7 +65,7 @@
val (_, [inner_t]) = strip_comb (HOLogic.dest_Trueprop pre_res)
val pre_rhs =
fold (curry HOLogic.mk_conj) (map HOLogic.dest_Trueprop prems'') inner_t
- val rhs = Envir.expand_term_frees subst pre_rhs
+ val rhs = Envir.expand_term_defs dest_Free subst pre_rhs
in
(case try_destruct_case thy (var_names @ names') rhs of
NONE => [(subst, rhs)]
@@ -116,7 +116,7 @@
val constT = map fastype_of frees ---> HOLogic.boolT
val lhs = list_comb (Const (full_constname, constT), frees)
fun mk_def (subst, rhs) =
- Logic.mk_equals (fold Envir.expand_term_frees (map single subst) lhs, rhs)
+ Logic.mk_equals (fold (Envir.expand_term_defs dest_Free) (map single subst) lhs, rhs)
val new_defs = map mk_def srs
val (definition, thy') = thy
|> Sign.add_consts [(Binding.name constname, constT, NoSyn)]
--- a/src/HOL/ex/Sorting_Algorithms_Examples.thy Mon Oct 25 13:56:08 2021 +0100
+++ b/src/HOL/ex/Sorting_Algorithms_Examples.thy Mon Oct 25 23:10:06 2021 +0200
@@ -23,8 +23,9 @@
val term_of_int_list = HOLogic.mk_list \<^typ>\<open>int\<close>
o map (HOLogic.mk_number \<^typ>\<open>int\<close> o @{code integer_of_int});
- fun raw_sort (ctxt, ct, ks) = Thm.mk_binop \<^cterm>\<open>Pure.eq :: int list \<Rightarrow> int list \<Rightarrow> prop\<close>
- ct (Thm.cterm_of ctxt (term_of_int_list ks));
+ fun raw_sort (ctxt, ct, ks) =
+ \<^instantiate>\<open>x = ct and y = \<open>Thm.cterm_of ctxt (term_of_int_list ks)\<close>
+ in cterm \<open>x \<equiv> y\<close> for x y :: \<open>int list\<close>\<close>;
val (_, sort_oracle) = Context.>>> (Context.map_theory_result
(Thm.add_oracle (\<^binding>\<open>sort\<close>, raw_sort)));
--- a/src/Pure/Isar/local_defs.ML Mon Oct 25 13:56:08 2021 +0100
+++ b/src/Pure/Isar/local_defs.ML Mon Oct 25 23:10:06 2021 +0200
@@ -93,7 +93,7 @@
(Names.empty, Names.build (fold (Names.add_set o #1 o head_of_def o Thm.term_of) defs))
#> funpow (length defs) (fn th => Drule.reflexive_thm RS th);
-val expand_term = Envir.expand_term_frees o map (abs_def o Thm.term_of);
+val expand_term = Envir.expand_term_defs dest_Free o map (abs_def o Thm.term_of);
fun def_export _ defs = (expand defs, expand_term defs);
@@ -125,7 +125,7 @@
|> Proof_Context.add_fixes [(x, SOME T, mx)];
val lhs = Free (x', T);
val _ = cert_def ctxt' (K []) (Logic.mk_equals (lhs, rhs));
- fun abbrev_export _ _ = (I, Envir.expand_term_frees [((x', T), rhs)]);
+ fun abbrev_export _ _ = (I, Envir.expand_term_defs dest_Free [((x', T), rhs)]);
val (_, ctxt'') = Assumption.add_assms abbrev_export [] ctxt';
in ((lhs, rhs), ctxt'') end;
--- a/src/Pure/ML/ml_antiquotations.ML Mon Oct 25 13:56:08 2021 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML Mon Oct 25 23:10:06 2021 +0200
@@ -13,9 +13,9 @@
type insts = ((indexname * sort) * typ) list * ((indexname * typ) * term) list
type cinsts = ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
val instantiate_typ: insts -> typ -> typ
- val instantiate_ctyp: cinsts -> ctyp -> ctyp
+ val instantiate_ctyp: Position.T -> cinsts -> ctyp -> ctyp
val instantiate_term: insts -> term -> term
- val instantiate_cterm: cinsts -> cterm -> cterm
+ val instantiate_cterm: Position.T -> cinsts -> cterm -> cterm
end;
structure ML_Antiquotations: ML_ANTIQUOTATIONS =
@@ -227,7 +227,7 @@
(Scan.succeed "ML_Antiquotations.dest_judgment ML_context"));
-(* type/term instantiations and constructors *)
+(* type/term instantiations *)
fun make_ctyp ctxt T = Thm.ctyp_of ctxt T |> Thm.trim_context_ctyp;
fun make_cterm ctxt t = Thm.cterm_of ctxt t |> Thm.trim_context_cterm;
@@ -235,22 +235,27 @@
type insts = ((indexname * sort) * typ) list * ((indexname * typ) * term) list
type cinsts = ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list
-fun instantiate_typ (insts: insts) = Term_Subst.instantiateT (TVars.make (#1 insts));
-fun instantiate_ctyp (cinsts: cinsts) = Thm.instantiate_ctyp (TVars.make (#1 cinsts));
+fun instantiate_typ (insts: insts) =
+ Term_Subst.instantiateT (TVars.make (#1 insts));
+
+fun instantiate_ctyp pos (cinsts: cinsts) cT =
+ Thm.instantiate_ctyp (TVars.make (#1 cinsts)) cT
+ handle CTERM (msg, args) => Exn.reraise (CTERM (msg ^ Position.here pos, args));
fun instantiate_term (insts: insts) =
let
val instT = TVars.make (#1 insts);
val instantiateT = Term_Subst.instantiateT instT;
val inst = Vars.make ((map o apfst o apsnd) instantiateT (#2 insts));
- in Term_Subst.instantiate (instT, inst) end;
+ in Term_Subst.instantiate_beta (instT, inst) end;
-fun instantiate_cterm (cinsts: cinsts) =
+fun instantiate_cterm pos (cinsts: cinsts) ct =
let
val cinstT = TVars.make (#1 cinsts);
val instantiateT = Term_Subst.instantiateT (TVars.map (K Thm.typ_of) cinstT);
val cinst = Vars.make ((map o apfst o apsnd) instantiateT (#2 cinsts));
- in Thm.instantiate_cterm (cinstT, cinst) end;
+ in Thm.instantiate_beta_cterm (cinstT, cinst) ct end
+ handle CTERM (msg, args) => Exn.reraise (CTERM (msg ^ Position.here pos, args));
local
@@ -290,6 +295,16 @@
(Context_Position.reports ctxt (map (pair pos) (Syntax_Phases.markup_free ctxt x)); (x, T))
| NONE => error ("No occurrence of variable " ^ quote x ^ Position.here pos));
+fun missing_instT envT instT =
+ (case filter_out (fn (a, _) => exists (fn (b, _) => a = b) instT) envT of
+ [] => ()
+ | bad => error ("No instantiation for free type variable(s) " ^ commas_quote (map #1 bad)));
+
+fun missing_inst env inst =
+ (case filter_out (fn (a, _) => exists (fn (b, _) => a = b) inst) env of
+ [] => ()
+ | bad => error ("No instantiation for free variable(s) " ^ commas_quote (map #1 bad)));
+
fun make_instT (a, pos) T =
(case try (Term.dest_TVar o Logic.dest_type) T of
NONE => error ("Not a free type variable " ^ quote a ^ Position.here pos)
@@ -300,15 +315,21 @@
NONE => error ("Not a free variable " ^ quote a ^ Position.here pos)
| SOME v => ml (ML_Syntax.print_pair ML_Syntax.print_indexname ML_Syntax.print_typ v));
+fun term_env t = (Term.add_tfrees t [], Term.add_frees t []);
+
fun prepare_insts ctxt1 ctxt0 (instT, inst) t =
let
- val envT = Term.add_tfrees t [];
- val env = Term.add_frees t [];
+ val (envT, env) = term_env t;
val freesT = map (Logic.mk_type o TFree o get_tfree envT) instT;
val frees = map (Free o check_free ctxt1 env) inst;
val (t' :: varsT, vars) =
Variable.export_terms ctxt1 ctxt0 (t :: freesT @ frees)
|> chop (1 + length freesT);
+
+ val (envT', env') = term_env t';
+ val _ = missing_instT (subtract (eq_fst op =) envT' envT) instT;
+ val _ = missing_inst (subtract (eq_fst op =) env' env) inst;
+
val ml_insts = (map2 make_instT instT varsT, map2 make_inst inst vars);
in (ml_insts, t') end;
@@ -338,19 +359,25 @@
val (ml_insts, t') = prepare_insts ctxt1 ctxt insts t;
in prepare_ml range arg (ML_Syntax.print_term t') ml_insts ctxt end;
-fun typ_ml kind = (kind, "", "ML_Antiquotations.instantiate_typ");
-fun term_ml kind = (kind, "", "ML_Antiquotations.instantiate_term");
-fun ctyp_ml kind =
- (kind, "ML_Antiquotations.make_ctyp ML_context", "ML_Antiquotations.instantiate_ctyp");
-fun cterm_ml kind =
- (kind, "ML_Antiquotations.make_cterm ML_context", "ML_Antiquotations.instantiate_cterm");
+val ml_here = ML_Syntax.atomic o ML_Syntax.print_position;
+
+fun typ_ml (kind, _: Position.T) = (kind, "", "ML_Antiquotations.instantiate_typ ");
+fun term_ml (kind, _: Position.T) = (kind, "", "ML_Antiquotations.instantiate_term ");
+fun ctyp_ml (kind, pos) =
+ (kind, "ML_Antiquotations.make_ctyp ML_context",
+ "ML_Antiquotations.instantiate_ctyp " ^ ml_here pos);
+fun cterm_ml (kind, pos) =
+ (kind, "ML_Antiquotations.make_cterm ML_context",
+ "ML_Antiquotations.instantiate_cterm " ^ ml_here pos);
+
+val command_name = Parse.position o Parse.command_name;
fun parse_body range =
- (Parse.command_name "typ" >> typ_ml || Parse.command_name "ctyp" >> ctyp_ml) --
+ (command_name "typ" >> typ_ml || command_name "ctyp" >> ctyp_ml) --
Parse.!!! Parse.typ >> prepare_type range ||
- (Parse.command_name "term" >> term_ml || Parse.command_name "cterm" >> cterm_ml)
+ (command_name "term" >> term_ml || command_name "cterm" >> cterm_ml)
-- Parse.!!! (Parse.term -- Parse.for_fixes) >> prepare_term Syntax.read_term range ||
- (Parse.command_name "prop" >> term_ml || Parse.command_name "cprop" >> cterm_ml)
+ (command_name "prop" >> term_ml || command_name "cprop" >> cterm_ml)
-- Parse.!!! (Parse.term -- Parse.for_fixes) >> prepare_term Syntax.read_prop range;
val _ = Theory.setup
@@ -373,6 +400,8 @@
in end;
+(* type/term constructors *)
+
local
val keywords = Keyword.add_minor_keywords ["for", "=>"] Keyword.empty_keywords;
--- a/src/Pure/envir.ML Mon Oct 25 13:56:08 2021 +0100
+++ b/src/Pure/envir.ML Mon Oct 25 23:10:06 2021 +0200
@@ -48,7 +48,7 @@
val subst_term: Type.tyenv * tenv -> term -> term
val expand_atom: typ -> typ * term -> term
val expand_term: (term -> (typ * term) option) -> term -> term
- val expand_term_frees: ((string * typ) * term) list -> term -> term
+ val expand_term_defs: (term -> string * typ) -> ((string * typ) * term) list -> term -> term
end;
structure Envir: ENVIR =
@@ -415,10 +415,10 @@
end;
in expand end;
-fun expand_term_frees defs =
+fun expand_term_defs dest defs =
let
- val eqs = map (fn ((x, U), u) => (x, (U, u))) defs;
- val get = fn Free (x, _) => AList.lookup (op =) eqs x | _ => NONE;
+ val eqs = map (fn ((x, U), u) => (x: string, (U, u))) defs;
+ fun get t = (case try dest t of SOME (x, _: typ) => AList.lookup (op =) eqs x | _ => NONE);
in expand_term get end;
end;
--- a/src/Pure/term.ML Mon Oct 25 13:56:08 2021 +0100
+++ b/src/Pure/term.ML Mon Oct 25 23:10:06 2021 +0200
@@ -124,6 +124,7 @@
val a_itselfT: typ
val argument_type_of: term -> int -> typ
val abs: string * typ -> term -> term
+ val args_of: term -> term list
val add_tvar_namesT: typ -> indexname list -> indexname list
val add_tvar_names: term -> indexname list -> indexname list
val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
@@ -423,6 +424,10 @@
| stripc x = x
in stripc(u,[]) end;
+fun args_of u =
+ let fun args (f $ x) xs = args f (x :: xs)
+ | args _ xs = xs
+ in args u [] end;
(*maps f(t1,...,tn) to f , which is never a combination*)
fun head_of (f$t) = head_of f
--- a/src/Pure/term_subst.ML Mon Oct 25 13:56:08 2021 +0100
+++ b/src/Pure/term_subst.ML Mon Oct 25 23:10:06 2021 +0200
@@ -13,17 +13,21 @@
val generalize_same: Names.set * Names.set -> int -> term Same.operation
val generalizeT: Names.set -> int -> typ -> typ
val generalize: Names.set * Names.set -> int -> term -> term
- val instantiateT_maxidx: (typ * int) TVars.table -> typ -> int -> typ * int
- val instantiate_maxidx: (typ * int) TVars.table * (term * int) Vars.table ->
- term -> int -> term * int
val instantiateT_frees_same: typ TFrees.table -> typ Same.operation
val instantiate_frees_same: typ TFrees.table * term Frees.table -> term Same.operation
val instantiateT_frees: typ TFrees.table -> typ -> typ
val instantiate_frees: typ TFrees.table * term Frees.table -> term -> term
+ val instantiateT_maxidx: (typ * int) TVars.table -> typ -> int -> typ * int
+ val instantiate_maxidx: (typ * int) TVars.table * (term * int) Vars.table ->
+ term -> int -> term * int
+ val instantiate_beta_maxidx: (typ * int) TVars.table * (term * int) Vars.table ->
+ term -> int -> term * int
val instantiateT_same: typ TVars.table -> typ Same.operation
val instantiate_same: typ TVars.table * term Vars.table -> term Same.operation
+ val instantiate_beta_same: typ TVars.table * term Vars.table -> term Same.operation
val instantiateT: typ TVars.table -> typ -> typ
val instantiate: typ TVars.table * term Vars.table -> term -> term
+ val instantiate_beta: typ TVars.table * term Vars.table -> term -> term
val zero_var_indexes_inst: Name.context -> term list -> typ TVars.table * term Vars.table
val zero_var_indexes: term -> term
val zero_var_indexes_list: term list -> term list
@@ -104,7 +108,7 @@
fun subst (Type (a, Ts)) = Type (a, Same.map subst Ts)
| subst (TFree v) =
(case TFrees.lookup instT v of
- SOME T => T
+ SOME T' => T'
| NONE => raise Same.SAME)
| subst _ = raise Same.SAME;
in subst ty end;
@@ -118,7 +122,7 @@
| subst (Free (x, T)) =
let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in
(case Frees.lookup inst (x, T') of
- SOME t => t
+ SOME t' => t'
| NONE => if same then raise Same.SAME else Free (x, T'))
end
| subst (Var (xi, T)) = Var (xi, substT T)
@@ -147,7 +151,7 @@
fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts)
| subst_typ (TVar ((a, i), S)) =
(case TVars.lookup instT ((a, i), S) of
- SOME (T, j) => (maxify j; T)
+ SOME (T', j) => (maxify j; T')
| NONE => (maxify i; raise Same.SAME))
| subst_typ _ = raise Same.SAME
and subst_typs (T :: Ts) =
@@ -166,14 +170,55 @@
| subst (Var ((x, i), T)) =
let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in
(case Vars.lookup inst ((x, i), T') of
- SOME (t, j) => (maxify j; t)
+ SOME (t', j) => (maxify j; t')
| NONE => (maxify i; if same then raise Same.SAME else Var ((x, i), T')))
end
| subst (Bound _) = raise Same.SAME
| subst (Abs (x, T, t)) =
- (Abs (x, substT T, Same.commit subst t)
+ (Abs (x, substT T, subst_commit t)
handle Same.SAME => Abs (x, T, subst t))
- | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
+ | subst (t $ u) = (subst t $ subst_commit u handle Same.SAME => t $ subst u)
+ and subst_commit t = Same.commit subst t;
+ in subst tm end;
+
+(*version with local beta reduction*)
+fun inst_beta_same maxidx (instT, inst) tm =
+ let
+ fun maxify i = if i > ! maxidx then maxidx := i else ();
+
+ val substT = instT_same maxidx instT;
+
+ fun expand_head t =
+ (case Term.head_of t of
+ Var ((x, i), T) =>
+ let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in
+ (case Vars.lookup inst ((x, i), T') of
+ SOME (t', j) => (maxify j; SOME t')
+ | NONE => (maxify i; if same then NONE else SOME (Var ((x, i), T'))))
+ end
+ | _ => NONE);
+
+ fun subst t =
+ (case expand_head t of
+ NONE =>
+ (case t of
+ Const (c, T) => Const (c, substT T)
+ | Free (x, T) => Free (x, substT T)
+ | Var _ => raise Same.SAME
+ | Bound _ => raise Same.SAME
+ | Abs (x, T, b) =>
+ (Abs (x, substT T, subst_commit b)
+ handle Same.SAME => Abs (x, T, subst b))
+ | _ $ _ => subst_comb t)
+ | SOME (u as Abs _) => Term.betapplys (u, map subst_commit (Term.args_of t))
+ | SOME u => subst_head u t)
+ and subst_comb (t $ u) = (subst_comb t $ subst_commit u handle Same.SAME => t $ subst u)
+ | subst_comb (Var _) = raise Same.SAME
+ | subst_comb t = subst t
+ and subst_head h (t $ u) = subst_head h t $ subst_commit u
+ | subst_head h _ = h
+ and subst_commit t = Same.commit subst t;
+
in subst tm end;
in
@@ -186,6 +231,11 @@
let val maxidx = Unsynchronized.ref i
in (Same.commit (inst_same maxidx insts) tm, ! maxidx) end;
+fun instantiate_beta_maxidx insts tm i =
+ let val maxidx = Unsynchronized.ref i
+ in (Same.commit (inst_beta_same maxidx insts) tm, ! maxidx) end;
+
+
fun instantiateT_same instT ty =
if TVars.is_empty instT then raise Same.SAME
else instT_same (Unsynchronized.ref ~1) (no_indexesT instT) ty;
@@ -194,9 +244,17 @@
if TVars.is_empty instT andalso Vars.is_empty inst then raise Same.SAME
else inst_same (Unsynchronized.ref ~1) (no_indexesT instT, no_indexes inst) tm;
+fun instantiate_beta_same (instT, inst) tm =
+ if TVars.is_empty instT andalso Vars.is_empty inst then raise Same.SAME
+ else inst_beta_same (Unsynchronized.ref ~1) (no_indexesT instT, no_indexes inst) tm;
+
+
fun instantiateT instT ty = Same.commit (instantiateT_same instT) ty;
+
fun instantiate inst tm = Same.commit (instantiate_same inst) tm;
+fun instantiate_beta inst tm = Same.commit (instantiate_beta_same inst) tm;
+
end;
--- a/src/Pure/thm.ML Mon Oct 25 13:56:08 2021 +0100
+++ b/src/Pure/thm.ML Mon Oct 25 23:10:06 2021 +0200
@@ -157,7 +157,9 @@
val generalize_cterm: Names.set * Names.set -> int -> cterm -> cterm
val generalize_ctyp: Names.set -> int -> ctyp -> ctyp
val instantiate: ctyp TVars.table * cterm Vars.table -> thm -> thm
+ val instantiate_beta: ctyp TVars.table * cterm Vars.table -> thm -> thm
val instantiate_cterm: ctyp TVars.table * cterm Vars.table -> cterm -> cterm
+ val instantiate_beta_cterm: ctyp TVars.table * cterm Vars.table -> cterm -> cterm
val trivial: cterm -> thm
val of_class: ctyp * class -> thm
val unconstrainT: thm -> thm
@@ -1675,7 +1677,7 @@
(*Left-to-right replacements: ctpairs = [..., (vi, ti), ...].
Instantiates distinct Vars by terms of same type.
Does NOT normalize the resulting theorem!*)
-fun instantiate (instT, inst) th =
+fun gen_instantiate inst_fn (instT, inst) th =
if TVars.is_empty instT andalso Vars.is_empty inst then th
else
let
@@ -1684,7 +1686,7 @@
handle CONTEXT (msg, cTs, cts, ths, context) =>
raise CONTEXT (msg, cTs, cts, th :: ths, context);
- val subst = Term_Subst.instantiate_maxidx (instT', inst');
+ val subst = inst_fn (instT', inst');
val (prop', maxidx1) = subst prop ~1;
val (tpairs', maxidx') =
fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1;
@@ -1708,19 +1710,25 @@
end
handle TYPE (msg, _, _) => raise THM (msg, 0, [th]);
-fun instantiate_cterm (instT, inst) ct =
+val instantiate = gen_instantiate Term_Subst.instantiate_maxidx;
+val instantiate_beta = gen_instantiate Term_Subst.instantiate_beta_maxidx;
+
+fun gen_instantiate_cterm inst_fn (instT, inst) ct =
if TVars.is_empty instT andalso Vars.is_empty inst then ct
else
let
val Cterm {cert, t, T, sorts, ...} = ct;
val ((instT', inst'), (cert', sorts')) = prep_insts (instT, inst) (cert, sorts);
- val subst = Term_Subst.instantiate_maxidx (instT', inst');
+ val subst = inst_fn (instT', inst');
val substT = Term_Subst.instantiateT_maxidx instT';
val (t', maxidx1) = subst t ~1;
val (T', maxidx') = substT T maxidx1;
in Cterm {cert = cert', t = t', T = T', sorts = sorts', maxidx = maxidx'} end
handle TYPE (msg, _, _) => raise CTERM (msg, [ct]);
+val instantiate_cterm = gen_instantiate_cterm Term_Subst.instantiate_maxidx;
+val instantiate_beta_cterm = gen_instantiate_cterm Term_Subst.instantiate_beta_maxidx;
+
end;