--- a/NEWS Fri Feb 23 14:56:32 2018 +0000
+++ b/NEWS Fri Feb 23 16:03:26 2018 +0000
@@ -167,6 +167,15 @@
latex and bibtex process. Minor INCOMPATIBILITY.
+*** Isar ***
+
+* Command 'interpret' no longer exposes resulting theorems as literal
+facts, notably for the \<open>prop\<close> notation or the "fact" proof method. This
+improves modularity of proofs and scalability of locale interpretation.
+Rare INCOMPATIBILITY, need to refer to explicitly named facts instead
+(e.g. use 'find_theorems' or 'try' to figure this out).
+
+
*** HOL ***
* Clarifed theorem names:
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Feb 23 14:56:32 2018 +0000
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Feb 23 16:03:26 2018 +0000
@@ -849,10 +849,9 @@
|> infer_instantiate' lthy (replicate live NONE @
[SOME (Thm.cterm_of lthy (ctorA $ y))])
|> unfold_thms lthy [dtor_ctor];
-
- val map_ctor_thm0 = fp_map_thm' RS ctor_cong RS (ctor_dtor RS sym RS trans);
in
- Thm.generalize ([], [y_s]) (Thm.maxidx_of map_ctor_thm0 + 1) map_ctor_thm0
+ (fp_map_thm' RS ctor_cong RS (ctor_dtor RS sym RS trans))
+ |> Drule.generalize ([], [y_s])
end;
val map_thms =
@@ -926,13 +925,12 @@
val ((y as Free (y_s, _), z as Free (z_s, _)), _) = lthy
|> yield_singleton (mk_Frees "y") y_T
||>> yield_singleton (mk_Frees "z") z_T;
-
- val rel_ctor_thm0 = fp_rel_thm
- |> infer_instantiate' lthy (replicate live NONE @
- [SOME (Thm.cterm_of lthy (ctorA $ y)), SOME (Thm.cterm_of lthy (ctorB $ z))])
- |> unfold_thms lthy [dtor_ctor];
in
- Thm.generalize ([], [y_s, z_s]) (Thm.maxidx_of rel_ctor_thm0 + 1) rel_ctor_thm0
+ fp_rel_thm
+ |> infer_instantiate' lthy (replicate live NONE @
+ [SOME (Thm.cterm_of lthy (ctorA $ y)), SOME (Thm.cterm_of lthy (ctorB $ z))])
+ |> unfold_thms lthy [dtor_ctor]
+ |> Drule.generalize ([], [y_s, z_s])
end;
val rel_inject_thms =
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Fri Feb 23 14:56:32 2018 +0000
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML Fri Feb 23 16:03:26 2018 +0000
@@ -158,9 +158,9 @@
let
val s = Name.uu;
val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
- val split' = Thm.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split;
in
- Thm.generalize ([], [s]) (Thm.maxidx_of split' + 1) split'
+ Thm.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split
+ |> Drule.generalize ([], [s])
end
| _ => split);
--- a/src/HOL/Tools/Lifting/lifting_def.ML Fri Feb 23 14:56:32 2018 +0000
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Fri Feb 23 16:03:26 2018 +0000
@@ -187,7 +187,7 @@
let
val [rty, rty'] = binder_types typ
in
- if Term.is_TVar rty andalso is_Type rty' then
+ if Term.is_TVar rty andalso Term.is_Type rty' then
(xi, Thm.cterm_of ctxt (HOLogic.eq_const rty')) :: subst
else
subst
@@ -472,7 +472,7 @@
if same_type_constrs (rty, qty) then
forall (no_no_code ctxt) (Targs rty ~~ Targs qty)
else
- if is_Type qty then
+ if Term.is_Type qty then
if Lifting_Info.is_no_code_type ctxt (Tname qty) then false
else
let
--- a/src/HOL/Tools/Lifting/lifting_util.ML Fri Feb 23 14:56:32 2018 +0000
+++ b/src/HOL/Tools/Lifting/lifting_util.ML Fri Feb 23 16:03:26 2018 +0000
@@ -25,7 +25,6 @@
val get_args: int -> term -> term list
val strip_args: int -> term -> term
val all_args_conv: conv -> conv
- val is_Type: typ -> bool
val same_type_constrs: typ * typ -> bool
val Targs: typ -> typ list
val Tname: typ -> string
@@ -108,9 +107,6 @@
fun all_args_conv conv ctm = Conv.try_conv (Conv.combination_conv (all_args_conv conv) conv) ctm
-fun is_Type (Type _) = true
- | is_Type _ = false
-
fun same_type_constrs (Type (r, _), Type (q, _)) = (r = q)
| same_type_constrs _ = false
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Feb 23 14:56:32 2018 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Feb 23 16:03:26 2018 +0000
@@ -83,7 +83,6 @@
val const_match : theory -> (string * typ) * (string * typ) -> bool
val term_match : theory -> term * term -> bool
val frac_from_term_pair : typ -> term -> term -> term
- val is_TFree : typ -> bool
val is_fun_type : typ -> bool
val is_set_type : typ -> bool
val is_fun_or_set_type : typ -> bool
@@ -478,9 +477,6 @@
| n2 => Const (@{const_name divide}, T --> T --> T)
$ HOLogic.mk_number T n1 $ HOLogic.mk_number T n2
-fun is_TFree (TFree _) = true
- | is_TFree _ = false
-
fun is_fun_type (Type (@{type_name fun}, _)) = true
| is_fun_type _ = false
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Feb 23 14:56:32 2018 +0000
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Feb 23 16:03:26 2018 +0000
@@ -38,9 +38,6 @@
fun type_name_of_bnf bnf = T_of_bnf bnf |> dest_Type |> fst
-fun is_Type (Type _) = true
- | is_Type _ = false
-
fun bnf_only_type_ctr f bnf = if is_Type (T_of_bnf bnf) then f bnf else I
fun bnf_of_fp_sugar (fp_sugar:fp_sugar) = nth (#bnfs (#fp_res fp_sugar)) (#fp_res_index fp_sugar)
--- a/src/Pure/Isar/class_declaration.ML Fri Feb 23 14:56:32 2018 +0000
+++ b/src/Pure/Isar/class_declaration.ML Fri Feb 23 16:03:26 2018 +0000
@@ -29,15 +29,19 @@
let
val empty_ctxt = Proof_Context.init_global thy;
+ val certT = Thm.trim_context_ctyp o Thm.global_ctyp_of thy;
+ val cert = Thm.trim_context_cterm o Thm.global_cterm_of thy;
+
(* instantiation of canonical interpretation *)
- val aT = TFree (Name.aT, base_sort);
+ val a_tfree = (Name.aT, base_sort);
+ val a_type = TFree a_tfree;
val param_map_const = (map o apsnd) Const param_map;
- val param_map_inst = (map o apsnd)
- (Const o apsnd (map_atyps (K aT))) param_map;
- val const_morph = Element.inst_morphism thy
- (Symtab.empty, Symtab.make param_map_inst);
- val typ_morph = Element.inst_morphism thy
- (Symtab.empty |> Symtab.update (Name.aT, TFree (Name.aT, [class])), Symtab.empty);
+ val param_map_inst = param_map |> map (fn (x, (c, T)) =>
+ let val T' = map_atyps (K a_type) T in ((x, T'), cert (Const (c, T'))) end);
+ val const_morph =
+ Element.instantiate_normalize_morphism ([], param_map_inst);
+ val typ_morph =
+ Element.instantiate_normalize_morphism ([(a_tfree, certT (TFree (Name.aT, [class])))], [])
val (([raw_props], _, [(_, raw_inst_morph)], _, export_morph), _) = empty_ctxt
|> Expression.cert_goal_expression ([(class, (("", false),
(Expression.Named param_map_const, [])))], []);
@@ -84,16 +88,16 @@
val some_assm_intro = Option.map prove_assm_intro (fst (Locale.intros_of thy class));
(* of_class *)
- val of_class_prop_concl = Logic.mk_of_class (aT, class);
+ val of_class_prop_concl = Logic.mk_of_class (a_type, class);
val of_class_prop =
(case some_prop of
NONE => of_class_prop_concl
| SOME prop => Logic.mk_implies (Morphism.term const_morph
- ((map_types o map_atyps) (K aT) prop), of_class_prop_concl));
+ ((map_types o map_atyps) (K a_type) prop), of_class_prop_concl));
val sup_of_classes = map (snd o Class.rules thy) sups;
val loc_axiom_intros = map Drule.export_without_context_open (Locale.axioms_of thy class);
val axclass_intro = #intro (Axclass.get_info thy class);
- val base_sort_trivs = Thm.of_sort (Thm.global_ctyp_of thy aT, base_sort);
+ val base_sort_trivs = Thm.of_sort (Thm.global_ctyp_of thy a_type, base_sort);
fun tac ctxt =
REPEAT (SOMEGOAL
(match_tac ctxt (axclass_intro :: sup_of_classes @ loc_axiom_intros @ base_sort_trivs)
--- a/src/Pure/Isar/element.ML Fri Feb 23 14:56:32 2018 +0000
+++ b/src/Pure/Isar/element.ML Fri Feb 23 16:03:26 2018 +0000
@@ -47,8 +47,8 @@
val transform_witness: morphism -> witness -> witness
val conclude_witness: Proof.context -> witness -> thm
val pretty_witness: Proof.context -> witness -> Pretty.T
- val instT_morphism: theory -> typ Symtab.table -> morphism
- val inst_morphism: theory -> typ Symtab.table * term Symtab.table -> morphism
+ val instantiate_normalize_morphism:
+ ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> morphism
val satisfy_morphism: witness list -> morphism
val eq_morphism: theory -> thm list -> morphism option
val init: context_i -> Context.generic -> Context.generic
@@ -321,18 +321,6 @@
end;
-
-fun compose_witness (Witness (_, th)) r =
- let
- val th' = Goal.conclude th;
- val A = Thm.cprem_of r 1;
- in
- Thm.implies_elim
- (Conv.gconv_rule Drule.beta_eta_conversion 1 r)
- (Conv.fconv_rule Drule.beta_eta_conversion
- (Thm.instantiate (Thm.match (Thm.cprop_of th', A)) th'))
- end;
-
fun conclude_witness ctxt (Witness (_, th)) =
Thm.close_derivation (Raw_Simplifier.norm_hhf_protect ctxt (Goal.conclude th));
@@ -344,127 +332,52 @@
end;
-(* derived rules *)
-
-fun instantiate_tfrees thy subst th =
- let
- val idx = Thm.maxidx_of th + 1;
- fun cert_inst (a, (S, T)) = (((a, idx), S), Thm.global_ctyp_of thy T);
-
- fun add_inst (a, S) insts =
- if AList.defined (op =) insts a then insts
- else (case AList.lookup (op =) subst a of NONE => insts | SOME T => (a, (S, T)) :: insts);
- val insts =
- (Term.fold_types o Term.fold_atyps) (fn TFree v => add_inst v | _ => I)
- (Thm.full_prop_of th) [];
- in
- th
- |> Thm.generalize (map fst insts, []) idx
- |> Thm.instantiate (map cert_inst insts, [])
- end;
-
-fun instantiate_frees thy subst =
- Drule.forall_intr_list (map (Thm.global_cterm_of thy o Free o fst) subst) #>
- Drule.forall_elim_list (map (Thm.global_cterm_of thy o snd) subst);
-
-fun hyps_rule rule th =
- let val hyps = Thm.chyps_of th in
- Drule.implies_elim_list
- (rule (Drule.implies_intr_list hyps th))
- (map (Thm.assume o Drule.cterm_rule rule) hyps)
- end;
-
-
-(* instantiate types *)
-
-fun instT_type_same env =
- if Symtab.is_empty env then Same.same
- else
- Term_Subst.map_atypsT_same
- (fn TFree (a, _) => (case Symtab.lookup env a of SOME T => T | NONE => raise Same.SAME)
- | _ => raise Same.SAME);
-
-fun instT_term_same env =
- if Symtab.is_empty env then Same.same
- else Term_Subst.map_types_same (instT_type_same env);
-
-val instT_type = Same.commit o instT_type_same;
-val instT_term = Same.commit o instT_term_same;
-
-fun instT_subst env th =
- (Thm.fold_terms o Term.fold_types o Term.fold_atyps)
- (fn T as TFree (a, _) =>
- let val T' = the_default T (Symtab.lookup env a)
- in if T = T' then I else insert (eq_fst (op =)) (a, T') end
- | _ => I) th [];
+(* instantiate frees, with beta normalization *)
-fun instT_thm thy env th =
- if Symtab.is_empty env then th
- else
- let val subst = instT_subst env th
- in if null subst then th else th |> hyps_rule (instantiate_tfrees thy subst) end;
-
-fun instT_morphism thy env =
- Morphism.morphism "Element.instT"
- {binding = [],
- typ = [instT_type env],
- term = [instT_term env],
- fact = [map (instT_thm thy env)]};
-
-
-(* instantiate types and terms *)
-
-fun inst_term (envT, env) =
- if Symtab.is_empty env then instT_term envT
- else
- instT_term envT #>
- Same.commit (Term_Subst.map_aterms_same
- (fn Free (x, _) => (case Symtab.lookup env x of SOME t => t | NONE => raise Same.SAME)
- | _ => raise Same.SAME)) #>
- Envir.beta_norm;
-
-fun inst_subst (envT, env) th =
- (Thm.fold_terms o Term.fold_aterms)
- (fn Free (x, T) =>
- let
- val T' = instT_type envT T;
- val t = Free (x, T');
- val t' = the_default t (Symtab.lookup env x);
- in if t aconv t' then I else insert (eq_fst (op =)) ((x, T'), t') end
- | _ => I) th [];
-
-fun inst_thm thy (envT, env) th =
- if Symtab.is_empty env then instT_thm thy envT th
- else
- let
- val substT = instT_subst envT th;
- val subst = inst_subst (envT, env) th;
- in
- if null substT andalso null subst then th
- else th |> hyps_rule
- (instantiate_tfrees thy substT #>
- instantiate_frees thy subst #>
- Conv.fconv_rule (Thm.beta_conversion true))
- end;
-
-fun inst_morphism thy (envT, env) =
- Morphism.morphism "Element.inst"
- {binding = [],
- typ = [instT_type envT],
- term = [inst_term (envT, env)],
- fact = [map (inst_thm thy (envT, env))]};
+fun instantiate_normalize_morphism insts =
+ Morphism.instantiate_frees_morphism insts $>
+ Morphism.term_morphism "beta_norm" Envir.beta_norm $>
+ Morphism.thm_morphism "beta_conversion" (Conv.fconv_rule (Thm.beta_conversion true));
(* satisfy hypotheses *)
+local
+
+val norm_term = Envir.beta_eta_contract;
+val norm_conv = Drule.beta_eta_conversion;
+val norm_cterm = Thm.rhs_of o norm_conv;
+
+fun find_witness witns hyp =
+ (case find_first (fn Witness (t, _) => hyp aconv t) witns of
+ NONE =>
+ let val hyp' = norm_term hyp
+ in find_first (fn Witness (t, _) => hyp' aconv norm_term t) witns end
+ | some => some);
+
+fun compose_witness (Witness (_, th)) r =
+ let
+ val th' = Goal.conclude th;
+ val A = Thm.cprem_of r 1;
+ in
+ Thm.implies_elim
+ (Conv.gconv_rule norm_conv 1 r)
+ (Conv.fconv_rule norm_conv
+ (Thm.instantiate (Thm.match (apply2 norm_cterm (Thm.cprop_of th', A))) th'))
+ end;
+
+in
+
fun satisfy_thm witns thm =
- thm |> fold (fn hyp =>
- (case find_first (fn Witness (t, _) => Thm.term_of hyp aconv t) witns of
+ (Thm.chyps_of thm, thm) |-> fold (fn hyp =>
+ (case find_witness witns (Thm.term_of hyp) of
NONE => I
- | SOME w => Thm.implies_intr hyp #> compose_witness w)) (Thm.chyps_of thm);
+ | SOME w => Thm.implies_intr hyp #> compose_witness w));
val satisfy_morphism = Morphism.thm_morphism "Element.satisfy" o satisfy_thm;
+end;
+
(* rewriting with equalities *)
--- a/src/Pure/Isar/expression.ML Fri Feb 23 14:56:32 2018 +0000
+++ b/src/Pure/Isar/expression.ML Fri Feb 23 16:03:26 2018 +0000
@@ -169,24 +169,30 @@
fun inst_morphism (parm_names, parm_types) ((prfx, mandatory), insts') ctxt =
let
(* parameters *)
- val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
+ val type_parms = fold Term.add_tfreesT parm_types [];
- (* type inference and contexts *)
+ (* type inference *)
val parm_types' = map (Type_Infer.paramify_vars o Logic.varifyT_global) parm_types;
- val type_parms = fold Term.add_tvarsT parm_types' [] |> map (Logic.mk_type o TVar);
- val arg = type_parms @ map2 Type.constraint parm_types' insts';
- val res = Syntax.check_terms (Config.put Type_Infer.object_logic false ctxt) arg;
- val ctxt' = ctxt |> fold Variable.auto_fixes res;
+ val type_parms' = fold Term.add_tvarsT parm_types' [];
+ val checked =
+ (map (Logic.mk_type o TVar) type_parms' @ map2 Type.constraint parm_types' insts')
+ |> Syntax.check_terms (Config.put Type_Infer.object_logic false ctxt)
+ val (type_parms'', insts'') = chop (length type_parms') checked;
+
+ (* context *)
+ val ctxt' = fold Variable.auto_fixes checked ctxt;
+ val certT = Thm.trim_context_ctyp o Thm.ctyp_of ctxt';
+ val cert = Thm.trim_context_cterm o Thm.cterm_of ctxt';
(* instantiation *)
- val (type_parms'', res') = chop (length type_parms) res;
- val insts'' = (parm_names ~~ res') |> map_filter
- (fn inst as (x, Free (y, _)) => if x = y then NONE else SOME inst
- | inst => SOME inst);
- val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
- val inst = Symtab.make insts'';
+ val instT =
+ (type_parms ~~ map Logic.dest_type type_parms'')
+ |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (v, T));
+ val cert_inst =
+ ((parm_names ~~ map (Term_Subst.instantiateT_frees instT) parm_types) ~~ insts'')
+ |> map_filter (fn (v, t) => if Free v = t then NONE else SOME (v, cert t));
in
- (Element.inst_morphism (Proof_Context.theory_of ctxt) (instT, inst) $>
+ (Element.instantiate_normalize_morphism (map (apsnd certT) instT, cert_inst) $>
Morphism.binding_morphism "Expression.inst" (Binding.prefix mandatory prfx), ctxt')
end;
@@ -309,8 +315,7 @@
fun finish_inst ctxt (loc, (prfx, inst)) =
let
val thy = Proof_Context.theory_of ctxt;
- val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
- val (morph, _) = inst_morphism (parm_names, parm_types) (prfx, inst) ctxt;
+ val (morph, _) = inst_morphism (Locale.params_types_of thy loc) (prfx, inst) ctxt;
in (loc, morph) end;
fun finish_fixes (parms: (string * typ) list) = map (fn (binding, _, mx) =>
@@ -371,23 +376,26 @@
fun prep_insts_cumulative (loc, (prfx, (inst, eqns))) (i, insts, eqnss, ctxt) =
let
- val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
+ val (parm_names, parm_types) = Locale.params_types_of thy loc;
val inst' = prep_inst ctxt parm_names inst;
val eqns' = map (apsnd (parse_eqn ctxt)) eqns;
val parm_types' = parm_types
- |> map (Type_Infer.paramify_vars o
- Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT_global);
+ |> map (Logic.varifyT_global #>
+ Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) #>
+ Type_Infer.paramify_vars);
val inst'' = map2 Type.constraint parm_types' inst';
val insts' = insts @ [(loc, (prfx, inst''))];
val eqnss' = eqnss @ [eqns'];
val ((insts'', eqnss'', _, _), _) = check_autofix insts' eqnss' [] [] ctxt;
- val inst''' = insts'' |> List.last |> snd |> snd;
- val eqns'' = eqnss'' |> List.last;
- val (inst_morph, _) = inst_morphism (parm_names, parm_types) (prfx, inst''') ctxt;
- val rewrite_morph = eqns'' |> map (snd #> Thm.cterm_of ctxt #> Thm.assume #> Local_Defs.abs_def_rule ctxt) |>
- Element.eq_morphism (Proof_Context.theory_of ctxt) |> the_default Morphism.identity;
- val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt;
- in (i + 1, insts', eqnss', ctxt'') end;
+ val (inst_morph, _) =
+ inst_morphism (parm_names, parm_types) (prfx, #2 (#2 (List.last insts''))) ctxt;
+ val rewrite_morph =
+ List.last eqnss''
+ |> map (snd #> Thm.cterm_of ctxt #> Thm.assume #> Local_Defs.abs_def_rule ctxt)
+ |> Element.eq_morphism (Proof_Context.theory_of ctxt)
+ |> the_default Morphism.identity;
+ val ctxt' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt;
+ in (i + 1, insts', eqnss', ctxt') end;
fun prep_elem raw_elem ctxt =
let
--- a/src/Pure/Isar/interpretation.ML Fri Feb 23 14:56:32 2018 +0000
+++ b/src/Pure/Isar/interpretation.ML Fri Feb 23 16:03:26 2018 +0000
@@ -175,10 +175,14 @@
fun setup_proof after_qed propss eqns goal_ctxt =
Element.witness_local_proof_eqs (lift_after_qed after_qed) "interpret"
propss eqns goal_ctxt state;
+ fun add_registration reg mixin export ctxt = ctxt
+ |> Proof_Context.set_stmt false
+ |> Context.proof_map (Locale.add_registration reg mixin export)
+ |> Proof_Context.restore_stmt ctxt;
in
Proof.context_of state
|> generic_interpretation prep_interpretation setup_proof
- Attrib.local_notes (Context.proof_map ooo Locale.add_registration) expression [] raw_eqns
+ Attrib.local_notes add_registration expression [] raw_eqns
end;
in
--- a/src/Pure/Isar/locale.ML Fri Feb 23 14:56:32 2018 +0000
+++ b/src/Pure/Isar/locale.ML Fri Feb 23 16:03:26 2018 +0000
@@ -49,6 +49,7 @@
val pretty_name: Proof.context -> string -> Pretty.T
val defined: theory -> string -> bool
val params_of: theory -> string -> ((string * typ) * mixfix) list
+ val params_types_of: theory -> string -> string list * typ list
val intros_of: theory -> string -> thm option * thm option
val axioms_of: theory -> string -> thm list
val instance_of: theory -> string -> morphism -> term list
@@ -212,6 +213,7 @@
(** Primitive operations **)
fun params_of thy = snd o #parameters o the_locale thy;
+fun params_types_of thy loc = split_list (map #1 (params_of thy loc));
fun intros_of thy = (apply2 o Option.map) (Thm.transfer thy) o #intros o the_locale thy;
--- a/src/Pure/Syntax/printer.ML Fri Feb 23 14:56:32 2018 +0000
+++ b/src/Pure/Syntax/printer.ML Fri Feb 23 16:03:26 2018 +0000
@@ -75,7 +75,7 @@
fun type_emphasis ctxt T =
T <> dummyT andalso
(Config.get ctxt show_types orelse Config.get ctxt show_markup orelse
- Config.get ctxt show_type_emphasis andalso not (can dest_Type T));
+ Config.get ctxt show_type_emphasis andalso not (is_Type T));
--- a/src/Pure/more_thm.ML Fri Feb 23 14:56:32 2018 +0000
+++ b/src/Pure/more_thm.ML Fri Feb 23 16:03:26 2018 +0000
@@ -72,6 +72,7 @@
val forall_intr_name: string * cterm -> thm -> thm
val forall_elim_var: int -> thm -> thm
val forall_elim_vars: int -> thm -> thm
+ val instantiate_frees: ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> thm -> thm
val instantiate': ctyp option list -> cterm option list -> thm -> thm
val forall_intr_frees: thm -> thm
val unvarify_global: theory -> thm -> thm
@@ -406,6 +407,29 @@
end;
+(* instantiate frees *)
+
+fun instantiate_frees ([], []) th = th
+ | instantiate_frees (instT, inst) th =
+ let
+ val idx = Thm.maxidx_of th + 1;
+ fun index ((a, A), b) = (((a, idx), A), b);
+ val insts = (map index instT, map index inst);
+ val frees = (map (#1 o #1) instT, map (#1 o #1) inst);
+
+ val hyps = Thm.chyps_of th;
+ val inst_cterm =
+ Thm.generalize_cterm frees idx #>
+ Thm.instantiate_cterm insts;
+ in
+ th
+ |> fold_rev Thm.implies_intr hyps
+ |> Thm.generalize frees idx
+ |> Thm.instantiate insts
+ |> fold (elim_implies o Thm.assume o inst_cterm) hyps
+ end;
+
+
(* instantiate by left-to-right occurrence of variables *)
fun instantiate' cTs cts thm =
--- a/src/Pure/morphism.ML Fri Feb 23 14:56:32 2018 +0000
+++ b/src/Pure/morphism.ML Fri Feb 23 16:03:26 2018 +0000
@@ -42,6 +42,8 @@
val transfer_morphism': Proof.context -> morphism
val transfer_morphism'': Context.generic -> morphism
val trim_context_morphism: morphism
+ val instantiate_frees_morphism:
+ ((string * sort) * ctyp) list * ((string * typ) * cterm) list -> morphism
val instantiate_morphism:
((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> morphism
end;
@@ -127,6 +129,22 @@
val trim_context_morphism = thm_morphism "trim_context" Thm.trim_context;
+
+(* instantiate *)
+
+fun instantiate_frees_morphism ([], []) = identity
+ | instantiate_frees_morphism (cinstT, cinst) =
+ let
+ val instT = map (apsnd Thm.typ_of) cinstT;
+ val inst = map (apsnd Thm.term_of) cinst;
+ in
+ morphism "instantiate_frees"
+ {binding = [],
+ typ = if null instT then [] else [Term_Subst.instantiateT_frees instT],
+ term = [Term_Subst.instantiate_frees (instT, inst)],
+ fact = [map (Thm.instantiate_frees (cinstT, cinst))]}
+ end;
+
fun instantiate_morphism ([], []) = identity
| instantiate_morphism (cinstT, cinst) =
let
--- a/src/Pure/term.ML Fri Feb 23 14:56:32 2018 +0000
+++ b/src/Pure/term.ML Fri Feb 23 16:03:26 2018 +0000
@@ -34,14 +34,16 @@
val no_dummyT: typ -> typ
val --> : typ * typ -> typ
val ---> : typ list * typ -> typ
+ val is_Type: typ -> bool
+ val is_TFree: typ -> bool
+ val is_TVar: typ -> bool
val dest_Type: typ -> string * typ list
+ val dest_TFree: typ -> string * sort
val dest_TVar: typ -> indexname * sort
- val dest_TFree: typ -> string * sort
val is_Bound: term -> bool
val is_Const: term -> bool
val is_Free: term -> bool
val is_Var: term -> bool
- val is_TVar: typ -> bool
val dest_Const: term -> string * typ
val dest_Free: term -> string * typ
val dest_Var: term -> indexname * typ
@@ -246,12 +248,29 @@
(*handy for multiple args: [T1,...,Tn]--->T gives T1-->(T2--> ... -->T)*)
val op ---> = Library.foldr (op -->);
+
+(** Discriminators **)
+
+fun is_Type (Type _) = true
+ | is_Type _ = false;
+
+fun is_TFree (TFree _) = true
+ | is_TFree _ = false;
+
+fun is_TVar (TVar _) = true
+ | is_TVar _ = false;
+
+
+(** Destructors **)
+
fun dest_Type (Type x) = x
| dest_Type T = raise TYPE ("dest_Type", [T], []);
+
+fun dest_TFree (TFree x) = x
+ | dest_TFree T = raise TYPE ("dest_TFree", [T], []);
+
fun dest_TVar (TVar x) = x
| dest_TVar T = raise TYPE ("dest_TVar", [T], []);
-fun dest_TFree (TFree x) = x
- | dest_TFree T = raise TYPE ("dest_TFree", [T], []);
(** Discriminators **)
@@ -268,9 +287,6 @@
fun is_Var (Var _) = true
| is_Var _ = false;
-fun is_TVar (TVar _) = true
- | is_TVar _ = false;
-
(** Destructors **)
--- a/src/Pure/term_subst.ML Fri Feb 23 14:56:32 2018 +0000
+++ b/src/Pure/term_subst.ML Fri Feb 23 16:03:26 2018 +0000
@@ -17,6 +17,12 @@
val instantiate_maxidx:
((indexname * sort) * (typ * int)) list * ((indexname * typ) * (term * int)) list ->
term -> int -> term * int
+ val instantiateT_frees_same: ((string * sort) * typ) list -> typ Same.operation
+ val instantiate_frees_same: ((string * sort) * typ) list * ((string * typ) * term) list ->
+ term Same.operation
+ val instantiateT_frees: ((string * sort) * typ) list -> typ -> typ
+ val instantiate_frees: ((string * sort) * typ) list * ((string * typ) * term) list ->
+ term -> term
val instantiateT_same: ((indexname * sort) * typ) list -> typ Same.operation
val instantiate_same: ((indexname * sort) * typ) list * ((indexname * typ) * term) list ->
term Same.operation
@@ -92,6 +98,42 @@
fun generalize names i tm = Same.commit (generalize_same names i) tm;
+(* instantiation of free variables (types before terms) *)
+
+fun instantiateT_frees_same [] _ = raise Same.SAME
+ | instantiateT_frees_same instT ty =
+ let
+ fun subst (Type (a, Ts)) = Type (a, Same.map subst Ts)
+ | subst (TFree v) =
+ (case AList.lookup (op =) instT v of
+ SOME T => T
+ | NONE => raise Same.SAME)
+ | subst _ = raise Same.SAME;
+ in subst ty end;
+
+fun instantiate_frees_same ([], []) _ = raise Same.SAME
+ | instantiate_frees_same (instT, inst) tm =
+ let
+ val substT = instantiateT_frees_same instT;
+ fun subst (Const (c, T)) = Const (c, substT T)
+ | subst (Free (x, T)) =
+ let val (T', same) = (substT T, false) handle Same.SAME => (T, true) in
+ (case AList.lookup (op =) inst (x, T') of
+ SOME t => t
+ | NONE => if same then raise Same.SAME else Free (x, T'))
+ end
+ | subst (Var (xi, T)) = Var (xi, substT T)
+ | subst (Bound _) = raise Same.SAME
+ | subst (Abs (x, T, t)) =
+ (Abs (x, substT T, Same.commit subst t)
+ handle Same.SAME => Abs (x, T, subst t))
+ | subst (t $ u) = (subst t $ Same.commit subst u handle Same.SAME => t $ subst u);
+ in subst tm end;
+
+fun instantiateT_frees instT ty = Same.commit (instantiateT_frees_same instT) ty;
+fun instantiate_frees inst tm = Same.commit (instantiate_frees_same inst) tm;
+
+
(* instantiation of schematic variables (types before terms) -- recomputes maxidx *)
local
--- a/src/Pure/thm.ML Fri Feb 23 14:56:32 2018 +0000
+++ b/src/Pure/thm.ML Fri Feb 23 16:03:26 2018 +0000
@@ -75,6 +75,7 @@
exception CONTEXT of string * ctyp list * cterm list * thm list * Context.generic option
val theory_of_cterm: cterm -> theory
val theory_of_thm: thm -> theory
+ val trim_context_ctyp: ctyp -> ctyp
val trim_context_cterm: cterm -> cterm
val trim_context: thm -> thm
val transfer_cterm: theory -> cterm -> cterm
@@ -118,6 +119,8 @@
val equal_elim: thm -> thm -> thm
val flexflex_rule: Proof.context option -> thm -> thm Seq.seq
val generalize: string list * string list -> int -> thm -> thm
+ val generalize_cterm: string list * string list -> int -> cterm -> cterm
+ val generalize_ctyp: string list -> int -> ctyp -> ctyp
val instantiate: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
thm -> thm
val instantiate_cterm: ((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list ->
@@ -410,6 +413,13 @@
Context.certificate_theory (cert_of th)
handle ERROR msg => raise CONTEXT (msg, [], [], [th], NONE);
+fun trim_context_ctyp cT =
+ (case cT of
+ Ctyp {cert = Context.Certificate_Id _, ...} => cT
+ | Ctyp {cert = Context.Certificate thy, T, maxidx, sorts} =>
+ Ctyp {cert = Context.Certificate_Id (Context.theory_id thy),
+ T = T, maxidx = maxidx, sorts = sorts});
+
fun trim_context_cterm ct =
(case ct of
Cterm {cert = Context.Certificate_Id _, ...} => ct
@@ -1152,6 +1162,23 @@
prop = prop'})
end;
+fun generalize_cterm ([], []) _ ct = ct
+ | generalize_cterm (tfrees, frees) idx (ct as Cterm {cert, t, T, maxidx, sorts}) =
+ if idx <= maxidx then raise CTERM ("generalize_cterm: bad index", [ct])
+ else
+ Cterm {cert = cert, sorts = sorts,
+ T = Term_Subst.generalizeT tfrees idx T,
+ t = Term_Subst.generalize (tfrees, frees) idx t,
+ maxidx = Int.max (maxidx, idx)};
+
+fun generalize_ctyp [] _ cT = cT
+ | generalize_ctyp tfrees idx (Ctyp {cert, T, maxidx, sorts}) =
+ if idx <= maxidx then raise CTERM ("generalize_ctyp: bad index", [])
+ else
+ Ctyp {cert = cert, sorts = sorts,
+ T = Term_Subst.generalizeT tfrees idx T,
+ maxidx = Int.max (maxidx, idx)};
+
(*Instantiation of schematic variables
A