src/Pure/Isar/element.ML
author wenzelm
Fri Apr 27 22:47:30 2012 +0200 (2012-04-27)
changeset 47815 43f677b3ae91
parent 47249 c0481c3c2a6c
child 49750 444cfaa331c9
permissions -rw-r--r--
clarified signature;
     1 (*  Title:      Pure/Isar/element.ML
     2     Author:     Makarius
     3 
     4 Explicit data structures for some Isar language elements, with derived
     5 logical operations.
     6 *)
     7 
     8 signature ELEMENT =
     9 sig
    10   datatype ('typ, 'term) stmt =
    11     Shows of (Attrib.binding * ('term * 'term list) list) list |
    12     Obtains of (binding * ((binding * 'typ option) list * 'term list)) list
    13   type statement = (string, string) stmt
    14   type statement_i = (typ, term) stmt
    15   datatype ('typ, 'term, 'fact) ctxt =
    16     Fixes of (binding * 'typ option * mixfix) list |
    17     Constrains of (string * 'typ) list |
    18     Assumes of (Attrib.binding * ('term * 'term list) list) list |
    19     Defines of (Attrib.binding * ('term * 'term list)) list |
    20     Notes of string * (Attrib.binding * ('fact * Attrib.src list) list) list
    21   type context = (string, string, Facts.ref) ctxt
    22   type context_i = (typ, term, thm list) ctxt
    23   val map_ctxt: {binding: binding -> binding, typ: 'typ -> 'a, term: 'term -> 'b,
    24     pattern: 'term -> 'b, fact: 'fact -> 'c, attrib: Attrib.src -> Attrib.src} ->
    25     ('typ, 'term, 'fact) ctxt -> ('a, 'b, 'c) ctxt
    26   val map_ctxt_attrib: (Attrib.src -> Attrib.src) ->
    27     ('typ, 'term, 'fact) ctxt -> ('typ, 'term, 'fact) ctxt
    28   val transform_ctxt: morphism -> context_i -> context_i
    29   val transform_facts: morphism ->
    30     (Attrib.binding * (thm list * Args.src list) list) list ->
    31     (Attrib.binding * (thm list * Args.src list) list) list
    32   val pretty_stmt: Proof.context -> statement_i -> Pretty.T list
    33   val pretty_ctxt: Proof.context -> context_i -> Pretty.T list
    34   val pretty_statement: Proof.context -> string -> thm -> Pretty.T
    35   type witness
    36   val prove_witness: Proof.context -> term -> tactic -> witness
    37   val witness_proof: (witness list list -> Proof.context -> Proof.context) ->
    38     term list list -> Proof.context -> Proof.state
    39   val witness_proof_eqs: (witness list list -> thm list -> Proof.context -> Proof.context) ->
    40     term list list -> term list -> Proof.context -> Proof.state
    41   val witness_local_proof: (witness list list -> Proof.state -> Proof.state) ->
    42     string -> term list list -> Proof.context -> bool -> Proof.state -> Proof.state
    43   val witness_local_proof_eqs: (witness list list -> thm list -> Proof.state -> Proof.state) ->
    44     string -> term list list -> term list -> Proof.context -> bool -> Proof.state ->
    45     Proof.state
    46   val transform_witness: morphism -> witness -> witness
    47   val conclude_witness: witness -> thm
    48   val pretty_witness: Proof.context -> witness -> Pretty.T
    49   val instT_morphism: theory -> typ Symtab.table -> morphism
    50   val inst_morphism: theory -> typ Symtab.table * term Symtab.table -> morphism
    51   val satisfy_morphism: witness list -> morphism
    52   val eq_morphism: theory -> thm list -> morphism option
    53   val transfer_morphism: theory -> morphism
    54   val init: context_i -> Context.generic -> Context.generic
    55   val activate_i: context_i -> Proof.context -> context_i * Proof.context
    56   val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
    57 end;
    58 
    59 structure Element: ELEMENT =
    60 struct
    61 
    62 (** language elements **)
    63 
    64 (* statement *)
    65 
    66 datatype ('typ, 'term) stmt =
    67   Shows of (Attrib.binding * ('term * 'term list) list) list |
    68   Obtains of (binding * ((binding * 'typ option) list * 'term list)) list;
    69 
    70 type statement = (string, string) stmt;
    71 type statement_i = (typ, term) stmt;
    72 
    73 
    74 (* context *)
    75 
    76 datatype ('typ, 'term, 'fact) ctxt =
    77   Fixes of (binding * 'typ option * mixfix) list |
    78   Constrains of (string * 'typ) list |
    79   Assumes of (Attrib.binding * ('term * 'term list) list) list |
    80   Defines of (Attrib.binding * ('term * 'term list)) list |
    81   Notes of string * (Attrib.binding * ('fact * Attrib.src list) list) list;
    82 
    83 type context = (string, string, Facts.ref) ctxt;
    84 type context_i = (typ, term, thm list) ctxt;
    85 
    86 fun map_ctxt {binding, typ, term, pattern, fact, attrib} =
    87   fn Fixes fixes => Fixes (fixes |> map (fn (x, T, mx) => (binding x, Option.map typ T, mx)))
    88    | Constrains xs => Constrains (xs |> map (fn (x, T) =>
    89       (Variable.check_name (binding (Binding.name x)), typ T)))
    90    | Assumes asms => Assumes (asms |> map (fn ((a, atts), propps) =>
    91       ((binding a, map attrib atts), propps |> map (fn (t, ps) => (term t, map pattern ps)))))
    92    | Defines defs => Defines (defs |> map (fn ((a, atts), (t, ps)) =>
    93       ((binding a, map attrib atts), (term t, map pattern ps))))
    94    | Notes (kind, facts) => Notes (kind, facts |> map (fn ((a, atts), bs) =>
    95       ((binding a, map attrib atts), bs |> map (fn (ths, btts) => (fact ths, map attrib btts)))));
    96 
    97 fun map_ctxt_attrib attrib =
    98   map_ctxt {binding = I, typ = I, term = I, pattern = I, fact = I, attrib = attrib};
    99 
   100 fun transform_ctxt phi = map_ctxt
   101  {binding = Morphism.binding phi,
   102   typ = Morphism.typ phi,
   103   term = Morphism.term phi,
   104   pattern = Morphism.term phi,
   105   fact = Morphism.fact phi,
   106   attrib = Args.transform_values phi};
   107 
   108 fun transform_facts phi facts =
   109   Notes ("", facts) |> transform_ctxt phi |> (fn Notes (_, facts') => facts');
   110 
   111 
   112 
   113 (** pretty printing **)
   114 
   115 fun pretty_items _ _ [] = []
   116   | pretty_items keyword sep (x :: ys) =
   117       Pretty.block [Pretty.keyword keyword, Pretty.brk 1, x] ::
   118         map (fn y => Pretty.block [Pretty.str "  ", Pretty.keyword sep, Pretty.brk 1, y]) ys;
   119 
   120 fun pretty_name_atts ctxt (b, atts) sep =
   121   if Attrib.is_empty_binding (b, atts) then []
   122   else
   123     [Pretty.block (Pretty.breaks
   124       (Binding.pretty b :: Attrib.pretty_attribs ctxt atts @ [Pretty.str sep]))];
   125 
   126 
   127 (* pretty_stmt *)
   128 
   129 fun pretty_stmt ctxt =
   130   let
   131     val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
   132     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
   133     val prt_terms = separate (Pretty.keyword "and") o map prt_term;
   134     val prt_name_atts = pretty_name_atts ctxt;
   135 
   136     fun prt_show (a, ts) =
   137       Pretty.block (Pretty.breaks (prt_name_atts a ":" @ prt_terms (map fst ts)));
   138 
   139     fun prt_var (x, SOME T) = Pretty.block
   140           [Pretty.str (Binding.name_of x ^ " ::"), Pretty.brk 1, prt_typ T]
   141       | prt_var (x, NONE) = Pretty.str (Binding.name_of x);
   142     val prt_vars = separate (Pretty.keyword "and") o map prt_var;
   143 
   144     fun prt_obtain (_, ([], ts)) = Pretty.block (Pretty.breaks (prt_terms ts))
   145       | prt_obtain (_, (xs, ts)) = Pretty.block (Pretty.breaks
   146           (prt_vars xs @ [Pretty.keyword "where"] @ prt_terms ts));
   147   in
   148     fn Shows shows => pretty_items "shows" "and" (map prt_show shows)
   149      | Obtains obtains => pretty_items "obtains" "|" (map prt_obtain obtains)
   150   end;
   151 
   152 
   153 (* pretty_ctxt *)
   154 
   155 fun pretty_ctxt ctxt =
   156   let
   157     val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
   158     val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
   159     val prt_thm = Pretty.backquote o Display.pretty_thm ctxt;
   160     val prt_name_atts = pretty_name_atts ctxt;
   161 
   162     fun prt_mixfix NoSyn = []
   163       | prt_mixfix mx = [Pretty.brk 2, Mixfix.pretty_mixfix mx];
   164 
   165     fun prt_fix (x, SOME T, mx) = Pretty.block (Pretty.str (Binding.name_of x ^ " ::") ::
   166           Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
   167       | prt_fix (x, NONE, mx) = Pretty.block (Pretty.str (Binding.name_of x) ::
   168           Pretty.brk 1 :: prt_mixfix mx);
   169     fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn);
   170 
   171     fun prt_asm (a, ts) =
   172       Pretty.block (Pretty.breaks (prt_name_atts a ":" @ map (prt_term o fst) ts));
   173     fun prt_def (a, (t, _)) =
   174       Pretty.block (Pretty.breaks (prt_name_atts a ":" @ [prt_term t]));
   175 
   176     fun prt_fact (ths, []) = map prt_thm ths
   177       | prt_fact (ths, atts) = Pretty.enclose "(" ")"
   178           (Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts;
   179     fun prt_note (a, ths) =
   180       Pretty.block (Pretty.breaks (flat (prt_name_atts a "=" :: map prt_fact ths)));
   181   in
   182     fn Fixes fixes => pretty_items "fixes" "and" (map prt_fix fixes)
   183      | Constrains xs => pretty_items "constrains" "and" (map prt_constrain xs)
   184      | Assumes asms => pretty_items "assumes" "and" (map prt_asm asms)
   185      | Defines defs => pretty_items "defines" "and" (map prt_def defs)
   186      | Notes ("", facts) => pretty_items "notes" "and" (map prt_note facts)
   187      | Notes (kind, facts) => pretty_items ("notes " ^ kind) "and" (map prt_note facts)
   188   end;
   189 
   190 
   191 (* pretty_statement *)
   192 
   193 local
   194 
   195 fun standard_elim th =
   196   (case Object_Logic.elim_concl th of
   197     SOME C =>
   198       let
   199         val cert = Thm.cterm_of (Thm.theory_of_thm th);
   200         val thesis = Var ((Auto_Bind.thesisN, Thm.maxidx_of th + 1), fastype_of C);
   201         val th' = Thm.instantiate ([], [(cert C, cert thesis)]) th;
   202       in (th', true) end
   203   | NONE => (th, false));
   204 
   205 fun thm_name kind th prts =
   206   let val head =
   207     if Thm.has_name_hint th then
   208       Pretty.block [Pretty.command kind,
   209         Pretty.brk 1, Pretty.str (Long_Name.base_name (Thm.get_name_hint th) ^ ":")]
   210     else Pretty.command kind
   211   in Pretty.block (Pretty.fbreaks (head :: prts)) end;
   212 
   213 fun obtain prop ctxt =
   214   let
   215     val ((ps, prop'), ctxt') = Variable.focus prop ctxt;
   216     fun fix (x, T) = (Binding.name (Variable.revert_fixed ctxt' x), SOME T);
   217     val xs = map (fix o #2) ps;
   218     val As = Logic.strip_imp_prems prop';
   219   in ((Binding.empty, (xs, As)), ctxt') end;
   220 
   221 in
   222 
   223 fun pretty_statement ctxt kind raw_th =
   224   let
   225     val thy = Proof_Context.theory_of ctxt;
   226 
   227     val (th, is_elim) = standard_elim (Raw_Simplifier.norm_hhf raw_th);
   228     val ((_, [th']), ctxt') = Variable.import true [th] (Variable.set_body true ctxt);
   229     val prop = Thm.prop_of th';
   230     val (prems, concl) = Logic.strip_horn prop;
   231     val concl_term = Object_Logic.drop_judgment thy concl;
   232 
   233     val fixes = fold_aterms (fn v as Free (x, T) =>
   234         if Variable.newly_fixed ctxt' ctxt x andalso not (v aconv concl_term)
   235         then insert (op =) (Variable.revert_fixed ctxt' x, T) else I | _ => I) prop [] |> rev;
   236     val (assumes, cases) = take_suffix (fn prem =>
   237       is_elim andalso concl aconv Logic.strip_assums_concl prem) prems;
   238   in
   239     pretty_ctxt ctxt' (Fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) fixes)) @
   240     pretty_ctxt ctxt' (Assumes (map (fn t => (Attrib.empty_binding, [(t, [])])) assumes)) @
   241      (if null cases then pretty_stmt ctxt' (Shows [(Attrib.empty_binding, [(concl, [])])])
   242       else
   243         let val (clauses, ctxt'') = fold_map obtain cases ctxt'
   244         in pretty_stmt ctxt'' (Obtains clauses) end)
   245   end |> thm_name kind raw_th;
   246 
   247 end;
   248 
   249 
   250 
   251 (** logical operations **)
   252 
   253 (* witnesses -- hypotheses as protected facts *)
   254 
   255 datatype witness = Witness of term * thm;
   256 
   257 val mark_witness = Logic.protect;
   258 fun witness_prop (Witness (t, _)) = t;
   259 fun witness_hyps (Witness (_, th)) = Thm.hyps_of th;
   260 fun map_witness f (Witness witn) = Witness (f witn);
   261 
   262 fun transform_witness phi = map_witness (fn (t, th) => (Morphism.term phi t, Morphism.thm phi th));
   263 
   264 fun prove_witness ctxt t tac =
   265   Witness (t, Thm.close_derivation (Goal.prove ctxt [] [] (mark_witness t) (fn _ =>
   266     Tactic.rtac Drule.protectI 1 THEN tac)));
   267 
   268 
   269 local
   270 
   271 val refine_witness =
   272   Proof.refine (Method.Basic (K (RAW_METHOD
   273     (K (ALLGOALS
   274       (CONJUNCTS (ALLGOALS
   275         (CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI))))))))));
   276 
   277 fun gen_witness_proof proof after_qed wit_propss eq_props =
   278   let
   279     val propss =
   280       (map o map) (fn prop => (mark_witness prop, [])) wit_propss @
   281         [map (rpair []) eq_props];
   282     fun after_qed' thmss =
   283       let val (wits, eqs) = split_last ((map o map) Thm.close_derivation thmss);
   284       in after_qed ((map2 o map2) (curry Witness) wit_propss wits) eqs end;
   285   in proof after_qed' propss #> refine_witness #> Seq.hd end;
   286 
   287 fun proof_local cmd goal_ctxt int after_qed' propss =
   288   Proof.map_context (K goal_ctxt) #>
   289   Proof.local_goal (K (K ())) (K I) Proof_Context.bind_propp_i cmd NONE
   290     after_qed' (map (pair Thm.empty_binding) propss);
   291 
   292 in
   293 
   294 fun witness_proof after_qed wit_propss =
   295   gen_witness_proof (Proof.theorem NONE) (fn wits => fn _ => after_qed wits)
   296     wit_propss [];
   297 
   298 val witness_proof_eqs = gen_witness_proof (Proof.theorem NONE);
   299 
   300 fun witness_local_proof after_qed cmd wit_propss goal_ctxt int =
   301   gen_witness_proof (proof_local cmd goal_ctxt int)
   302     (fn wits => fn _ => after_qed wits) wit_propss [];
   303 
   304 fun witness_local_proof_eqs after_qed cmd wit_propss eq_props goal_ctxt int =
   305   gen_witness_proof (proof_local cmd goal_ctxt int) after_qed wit_propss eq_props;
   306 
   307 end;
   308 
   309 
   310 fun compose_witness (Witness (_, th)) r =
   311   let
   312     val th' = Goal.conclude th;
   313     val A = Thm.cprem_of r 1;
   314   in
   315     Thm.implies_elim
   316       (Conv.gconv_rule Drule.beta_eta_conversion 1 r)
   317       (Conv.fconv_rule Drule.beta_eta_conversion
   318         (Thm.instantiate (Thm.match (Thm.cprop_of th', A)) th'))
   319   end;
   320 
   321 fun conclude_witness (Witness (_, th)) =
   322   Thm.close_derivation (Raw_Simplifier.norm_hhf_protect (Goal.conclude th));
   323 
   324 fun pretty_witness ctxt witn =
   325   let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in
   326     Pretty.block (prt_term (witness_prop witn) ::
   327       (if Config.get ctxt show_hyps then [Pretty.brk 2, Pretty.list "[" "]"
   328          (map prt_term (witness_hyps witn))] else []))
   329   end;
   330 
   331 
   332 (* derived rules *)
   333 
   334 fun instantiate_tfrees thy subst th =
   335   let
   336     val certT = Thm.ctyp_of thy;
   337     val idx = Thm.maxidx_of th + 1;
   338     fun cert_inst (a, (S, T)) = (certT (TVar ((a, idx), S)), certT T);
   339 
   340     fun add_inst (a, S) insts =
   341       if AList.defined (op =) insts a then insts
   342       else (case AList.lookup (op =) subst a of NONE => insts | SOME T => (a, (S, T)) :: insts);
   343     val insts =
   344       (Term.fold_types o Term.fold_atyps) (fn TFree v => add_inst v | _ => I)
   345         (Thm.full_prop_of th) [];
   346   in
   347     th
   348     |> Thm.generalize (map fst insts, []) idx
   349     |> Thm.instantiate (map cert_inst insts, [])
   350   end;
   351 
   352 fun instantiate_frees thy subst =
   353   let val cert = Thm.cterm_of thy in
   354     Drule.forall_intr_list (map (cert o Free o fst) subst) #>
   355     Drule.forall_elim_list (map (cert o snd) subst)
   356   end;
   357 
   358 fun hyps_rule rule th =
   359   let val {hyps, ...} = Thm.crep_thm th in
   360     Drule.implies_elim_list
   361       (rule (Drule.implies_intr_list hyps th))
   362       (map (Thm.assume o Drule.cterm_rule rule) hyps)
   363   end;
   364 
   365 
   366 (* instantiate types *)
   367 
   368 fun instT_type_same env =
   369   if Symtab.is_empty env then Same.same
   370   else
   371     Term_Subst.map_atypsT_same
   372       (fn TFree (a, _) => (case Symtab.lookup env a of SOME T => T | NONE => raise Same.SAME)
   373         | _ => raise Same.SAME);
   374 
   375 fun instT_term_same env =
   376   if Symtab.is_empty env then Same.same
   377   else Term_Subst.map_types_same (instT_type_same env);
   378 
   379 val instT_type = Same.commit o instT_type_same;
   380 val instT_term = Same.commit o instT_term_same;
   381 
   382 fun instT_subst env th =
   383   (Thm.fold_terms o Term.fold_types o Term.fold_atyps)
   384     (fn T as TFree (a, _) =>
   385       let val T' = the_default T (Symtab.lookup env a)
   386       in if T = T' then I else insert (eq_fst (op =)) (a, T') end
   387     | _ => I) th [];
   388 
   389 fun instT_thm thy env th =
   390   if Symtab.is_empty env then th
   391   else
   392     let val subst = instT_subst env th
   393     in if null subst then th else th |> hyps_rule (instantiate_tfrees thy subst) end;
   394 
   395 fun instT_morphism thy env =
   396   let val thy_ref = Theory.check_thy thy in
   397     Morphism.morphism
   398      {binding = [],
   399       typ = [instT_type env],
   400       term = [instT_term env],
   401       fact = [map (fn th => instT_thm (Theory.deref thy_ref) env th)]}
   402   end;
   403 
   404 
   405 (* instantiate types and terms *)
   406 
   407 fun inst_term (envT, env) =
   408   if Symtab.is_empty env then instT_term envT
   409   else
   410     instT_term envT #>
   411     Same.commit (Term_Subst.map_aterms_same
   412       (fn Free (x, _) => (case Symtab.lookup env x of SOME t => t | NONE => raise Same.SAME)
   413         | _ => raise Same.SAME)) #>
   414     Envir.beta_norm;
   415 
   416 fun inst_subst (envT, env) th =
   417   (Thm.fold_terms o Term.fold_aterms)
   418     (fn Free (x, T) =>
   419       let
   420         val T' = instT_type envT T;
   421         val t = Free (x, T');
   422         val t' = the_default t (Symtab.lookup env x);
   423       in if t aconv t' then I else insert (eq_fst (op =)) ((x, T'), t') end
   424     | _ => I) th [];
   425 
   426 fun inst_thm thy (envT, env) th =
   427   if Symtab.is_empty env then instT_thm thy envT th
   428   else
   429     let
   430       val substT = instT_subst envT th;
   431       val subst = inst_subst (envT, env) th;
   432     in
   433       if null substT andalso null subst then th
   434       else th |> hyps_rule
   435        (instantiate_tfrees thy substT #>
   436         instantiate_frees thy subst #>
   437         Conv.fconv_rule (Thm.beta_conversion true))
   438     end;
   439 
   440 fun inst_morphism thy (envT, env) =
   441   let val thy_ref = Theory.check_thy thy in
   442     Morphism.morphism
   443      {binding = [],
   444       typ = [instT_type envT],
   445       term = [inst_term (envT, env)],
   446       fact = [map (fn th => inst_thm (Theory.deref thy_ref) (envT, env) th)]}
   447   end;
   448 
   449 
   450 (* satisfy hypotheses *)
   451 
   452 fun satisfy_thm witns thm =
   453   thm |> fold (fn hyp =>
   454     (case find_first (fn Witness (t, _) => Thm.term_of hyp aconv t) witns of
   455       NONE => I
   456     | SOME w => Thm.implies_intr hyp #> compose_witness w)) (#hyps (Thm.crep_thm thm));
   457 
   458 val satisfy_morphism = Morphism.thm_morphism o satisfy_thm;
   459 
   460 
   461 (* rewriting with equalities *)
   462 
   463 fun eq_morphism _ [] = NONE
   464   | eq_morphism thy thms =
   465       SOME (Morphism.morphism
   466        {binding = [],
   467         typ = [],
   468         term = [Raw_Simplifier.rewrite_term thy thms []],
   469         fact = [map (Raw_Simplifier.rewrite_rule thms)]});
   470 
   471 
   472 (* transfer to theory using closure *)
   473 
   474 fun transfer_morphism thy =
   475   let val thy_ref = Theory.check_thy thy
   476   in Morphism.thm_morphism (fn th => Thm.transfer (Theory.deref thy_ref) th) end;
   477 
   478 
   479 
   480 (** activate in context **)
   481 
   482 (* init *)
   483 
   484 fun init (Fixes fixes) = Context.map_proof (Proof_Context.add_fixes fixes #> #2)
   485   | init (Constrains _) = I
   486   | init (Assumes asms) = Context.map_proof (fn ctxt =>
   487       let
   488         val asms' = Attrib.map_specs (map (Attrib.attribute ctxt)) asms;
   489         val (_, ctxt') = ctxt
   490           |> fold Variable.auto_fixes (maps (map #1 o #2) asms')
   491           |> Proof_Context.add_assms_i Assumption.assume_export asms';
   492       in ctxt' end)
   493   | init (Defines defs) = Context.map_proof (fn ctxt =>
   494       let
   495         val defs' = Attrib.map_specs (map (Attrib.attribute ctxt)) defs;
   496         val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
   497             let val ((c, _), t') = Local_Defs.cert_def ctxt t  (* FIXME adapt ps? *)
   498             in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
   499         val (_, ctxt') = ctxt
   500           |> fold Variable.auto_fixes (map #1 asms)
   501           |> Proof_Context.add_assms_i Local_Defs.def_export (map #2 asms);
   502       in ctxt' end)
   503   | init (Notes (kind, facts)) = Attrib.generic_notes kind facts #> #2;
   504 
   505 
   506 (* activate *)
   507 
   508 fun activate_i elem ctxt =
   509   let
   510     val elem' = map_ctxt_attrib Args.assignable elem;
   511     val ctxt' = Context.proof_map (init elem') ctxt;
   512   in (map_ctxt_attrib Args.closure elem', ctxt') end;
   513 
   514 fun activate raw_elem ctxt =
   515   let val elem = raw_elem |> map_ctxt
   516    {binding = I,
   517     typ = I,
   518     term = I,
   519     pattern = I,
   520     fact = Proof_Context.get_fact ctxt,
   521     attrib = Attrib.intern_src (Proof_Context.theory_of ctxt)}
   522   in activate_i elem ctxt end;
   523 
   524 end;