# HG changeset patch # User wenzelm # Date 1635196206 -7200 # Node ID 42fb56041c11291c9d97c36f70886484f419f4c2 # Parent cff477b6d015cf9cb48cfed69922de1ca838ede4# Parent c14787d73db690d62e5f50fe5697c7c90da4ba54 merged diff -r cff477b6d015 -r 42fb56041c11 src/Doc/Codegen/Computations.thy --- 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 \ local - fun raw_dvd (b, ct) = Thm.mk_binop \<^cterm>\Pure.eq :: bool \ bool \ prop\ - ct (if b then \<^cterm>\True\ else \<^cterm>\False\); + fun raw_dvd (b, ct) = + \<^instantiate>\x = ct and y = \if b then \<^cterm>\True\ else \<^cterm>\False\\ + in cterm \x \ y\ for x y :: bool\; val (_, dvd_oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (\<^binding>\dvd\, raw_dvd))); diff -r cff477b6d015 -r 42fb56041c11 src/HOL/Library/Sum_of_Squares/positivstellensatz.ML --- 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>\real\ a - else Thm.apply (Thm.apply \<^cterm>\(/) :: real \ _\ - (Numeral.mk_cnumber \<^ctyp>\real\ a)) - (Numeral.mk_cnumber \<^ctyp>\real\ b) + else + \<^instantiate>\ + a = \Numeral.mk_cnumber \<^ctyp>\real\ a\ and + b = \Numeral.mk_cnumber \<^ctyp>\real\ b\ + in cterm \a / b\ for a b :: real\ end; fun dest_ratconst t = case Thm.term_of t of - Const(\<^const_name>\divide\, _)$a$b => Rat.make(HOLogic.dest_number a |> snd, HOLogic.dest_number b |> snd) + \<^Const_>\divide _ for a b\ => 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>\(^) :: real \ _\ x) - (Numeral.mk_cnumber \<^ctyp>\nat\ k) +fun cterm_of_varpow x k = + if k = 1 then x + else \<^instantiate>\x and k = \Numeral.mk_cnumber \<^ctyp>\nat\ k\ in cterm \x ^ k\ for x :: real\ fun cterm_of_monomial m = if FuncUtil.Ctermfunc.is_empty m then \<^cterm>\1::real\ @@ -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>\(*) :: real \ _\ s) t) vps + in foldr1 (fn (s, t) => \<^instantiate>\s and t in cterm \s * t\ for s t :: real\) 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>\(*)::real \ _\ (cterm_of_rat c)) (cterm_of_monomial m); + else \<^instantiate>\x = \cterm_of_rat c\ and y = \cterm_of_monomial m\ in cterm \x * y\ for x y :: real\; fun cterm_of_poly p = if FuncUtil.Monomialfunc.is_empty p then \<^cterm>\0::real\ @@ -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>\(+) :: real \ _\ t1) t2) cms + in foldr1 (fn (t1, t2) => \<^instantiate>\t1 and t2 in cterm \t1 + t2\ for t1 t2 :: real\) 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>\Trueprop\ - (Thm.apply (Thm.apply \<^cterm>\(=)::real \ _\ (mk_numeric x)) - \<^cterm>\0::real\))) - | Rational_le x => eqT_elim(numeric_ge_conv(Thm.apply \<^cterm>\Trueprop\ - (Thm.apply (Thm.apply \<^cterm>\(\)::real \ _\ - \<^cterm>\0::real\) (mk_numeric x)))) - | Rational_lt x => eqT_elim(numeric_gt_conv(Thm.apply \<^cterm>\Trueprop\ - (Thm.apply (Thm.apply \<^cterm>\(<)::real \ _\ \<^cterm>\0::real\) - (mk_numeric x)))) + | Rational_eq x => + eqT_elim (numeric_eq_conv + \<^instantiate>\x = \mk_numeric x\ in cprop \x = 0\ for x :: real\) + | Rational_le x => + eqT_elim (numeric_ge_conv + \<^instantiate>\x = \mk_numeric x\ in cprop \x \ 0\ for x :: real\) + | Rational_lt x => + eqT_elim (numeric_gt_conv + \<^instantiate>\x = \mk_numeric x\ in cprop \x > 0\ for x :: real\) | 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>\Trueprop\ p) th1)) - (Thm.implies_intr (Thm.apply \<^cterm>\Trueprop\ q) th2) + (Thm.implies_intr \<^instantiate>\p in cprop p\ th1)) + (Thm.implies_intr \<^instantiate>\q in cprop q\ th2) end fun overall cert_choice dun ths = case ths of @@ -481,8 +484,8 @@ val th_x = Drule.arg_cong_rule \<^cterm>\uminus :: real \ _\ th_p val th_n = fconv_rule (arg_conv poly_neg_conv) th_x val th' = Drule.binop_cong_rule \<^cterm>\HOL.disj\ - (Drule.arg_cong_rule (Thm.apply \<^cterm>\(<)::real \ _\ \<^cterm>\0::real\) th_p) - (Drule.arg_cong_rule (Thm.apply \<^cterm>\(<)::real \ _\ \<^cterm>\0::real\) th_n) + (Drule.arg_cong_rule \<^cterm>\(<) (0::real)\ th_p) + (Drule.arg_cong_rule \<^cterm>\(<) (0::real)\ 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>\Ex\,_)$Abs(_,_,_) => + \<^Const_>\Ex _ for \Abs _\\ => 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>\All\, (T --> \<^typ>\bool\) --> \<^typ>\bool\)) + val T = Thm.ctyp_of_cterm x + val all = \<^instantiate>\'a = T in cterm All\ 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>\Ex\, (T --> \<^typ>\bool\) --> \<^typ>\bool\)) - fun mk_ex v t = Thm.apply (ext (Thm.typ_of_cterm v)) (Thm.lambda v t) + fun mk_ex v t = + \<^instantiate>\'a = \Thm.ctyp_of_cterm v\ and P = \Thm.lambda v t\ + in cprop \Ex P\ for P :: \'a \ bool\\ fun choose v th th' = case Thm.concl_of th of - \<^term>\Trueprop\ $ (Const(\<^const_name>\Ex\,_)$_) => - 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>\Trueprop\ (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_>\Trueprop for \<^Const_>\Ex _ for _\\ => + 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>\Trueprop\ (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>\Trueprop\ 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>\All\,_)$Abs(_,_,_) => + \<^Const_>\All _ for \Abs _\\ => 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>\HOL.conj\, \<^term>\HOL.disj\] [] (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>\Trueprop\ (Thm.apply \<^cterm>\Not\ ct) + val nct = \<^instantiate>\A = ct in cprop \\ A\\ 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>\of_nat\, _)$ n => not (can HOLogic.dest_number n) - | Const(\<^const_name>\of_int\, _)$ n => not (can HOLogic.dest_number n) + \<^Const_>\of_nat _ for n\ => not (can HOLogic.dest_number n) + | \<^Const_>\of_int _ for n\ => not (can HOLogic.dest_number n) | _ => false in fun real_linear_prover translator (eq,le,lt) = diff -r cff477b6d015 -r 42fb56041c11 src/HOL/Tools/BNF/bnf_comp.ML --- 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>\csum\, _) $ t $ u) = forall is_sum_prod_natLeq [t, u] | is_sum_prod_natLeq (Const (\<^const_name>\cprod\, _) $ t $ u) = forall is_sum_prod_natLeq [t, u] diff -r cff477b6d015 -r 42fb56041c11 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- 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)] diff -r cff477b6d015 -r 42fb56041c11 src/HOL/ex/Sorting_Algorithms_Examples.thy --- 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>\int\ o map (HOLogic.mk_number \<^typ>\int\ o @{code integer_of_int}); - fun raw_sort (ctxt, ct, ks) = Thm.mk_binop \<^cterm>\Pure.eq :: int list \ int list \ prop\ - ct (Thm.cterm_of ctxt (term_of_int_list ks)); + fun raw_sort (ctxt, ct, ks) = + \<^instantiate>\x = ct and y = \Thm.cterm_of ctxt (term_of_int_list ks)\ + in cterm \x \ y\ for x y :: \int list\\; val (_, sort_oracle) = Context.>>> (Context.map_theory_result (Thm.add_oracle (\<^binding>\sort\, raw_sort))); diff -r cff477b6d015 -r 42fb56041c11 src/Pure/Isar/local_defs.ML --- 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; diff -r cff477b6d015 -r 42fb56041c11 src/Pure/ML/ml_antiquotations.ML --- 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; diff -r cff477b6d015 -r 42fb56041c11 src/Pure/envir.ML --- 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; diff -r cff477b6d015 -r 42fb56041c11 src/Pure/term.ML --- 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 diff -r cff477b6d015 -r 42fb56041c11 src/Pure/term_subst.ML --- 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; diff -r cff477b6d015 -r 42fb56041c11 src/Pure/thm.ML --- 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;