# HG changeset patch # User wenzelm # Date 1519240422 -3600 # Node ID 8e4ff46f807dabf670163855497af3aa89a94467 # Parent 67caf783b9eec34719206bca91a44ea3cafb39ab more standard instantiate operations, where substitutions are already certified and stored with trimmed theory certificate; diff -r 67caf783b9ee -r 8e4ff46f807d src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Wed Feb 21 18:41:41 2018 +0100 +++ b/src/Pure/Isar/class_declaration.ML Wed Feb 21 20:13:42 2018 +0100 @@ -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) diff -r 67caf783b9ee -r 8e4ff46f807d src/Pure/Isar/element.ML --- a/src/Pure/Isar/element.ML Wed Feb 21 18:41:41 2018 +0100 +++ b/src/Pure/Isar/element.ML Wed Feb 21 20:13:42 2018 +0100 @@ -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 @@ -344,115 +344,12 @@ 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 *) diff -r 67caf783b9ee -r 8e4ff46f807d src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Wed Feb 21 18:41:41 2018 +0100 +++ b/src/Pure/Isar/expression.ML Wed Feb 21 20:13:42 2018 +0100 @@ -171,7 +171,7 @@ (* parameters *) val type_parms = fold Term.add_tfreesT parm_types []; - (* type inference and context *) + (* 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' []; val checked = @@ -179,19 +179,20 @@ |> Syntax.check_terms (Config.put Type_Infer.object_logic false ctxt) val (type_parms'', insts'') = chop (length type_parms') checked; - val ctxt' = ctxt |> fold Variable.auto_fixes 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 instT = (type_parms ~~ map Logic.dest_type type_parms'') - |> map_filter (fn (v, T) => if TFree v = T then NONE else SOME (#1 v, T)) - |> Symtab.make; - val inst = - (parm_names ~~ insts'') - |> filter (fn (a, Free (b, _)) => a <> b | _ => true) - |> Symtab.make; + |> 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;