memorizing and exporting destruction rules
authorhaftmann
Thu Dec 13 07:09:07 2007 +0100 (2007-12-13)
changeset 25619e4d5cd384245
parent 25618 01f20279fea1
child 25620 a6cb8f60cff7
memorizing and exporting destruction rules
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/locale.ML	Thu Dec 13 07:09:06 2007 +0100
     1.2 +++ b/src/Pure/Isar/locale.ML	Thu Dec 13 07:09:07 2007 +0100
     1.3 @@ -58,8 +58,8 @@
     1.4      ((string * Attrib.src list) * term list) list
     1.5    val global_asms_of: theory -> string ->
     1.6      ((string * Attrib.src list) * term list) list
     1.7 -  val intros: theory -> string ->
     1.8 -    thm list * thm list
     1.9 +  val intros: theory -> string -> thm list * thm list
    1.10 +  val dests: theory -> string -> thm list
    1.11  
    1.12    (* Processing of locale statements *)
    1.13    val read_context_statement: xstring option -> Element.context element list ->
    1.14 @@ -177,8 +177,10 @@
    1.15    decls: decl list * decl list,                    (*type/term_syntax declarations*)
    1.16    regs: ((string * string list) * Element.witness list) list,
    1.17      (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *)
    1.18 -  intros: thm list * thm list}
    1.19 +  intros: thm list * thm list,
    1.20      (* Introduction rules: of delta predicate and locale predicate. *)
    1.21 +  dests: thm list}
    1.22 +    (* Destruction rules relative to canonical order in locale context. *)
    1.23  
    1.24  (* CB: an internal (Int) locale element was either imported or included,
    1.25     an external (Ext) element appears directly in the locale text. *)
    1.26 @@ -363,7 +365,7 @@
    1.27    val extend = I;
    1.28  
    1.29    fun join_locales _
    1.30 -    ({axiom, imports, elems, params, lparams, decls = (decls1, decls2), regs, intros}: locale,
    1.31 +    ({axiom, imports, elems, params, lparams, decls = (decls1, decls2), regs, intros, dests}: locale,
    1.32        {elems = elems', decls = (decls1', decls2'), regs = regs', ...}: locale) =
    1.33       {axiom = axiom,
    1.34        imports = imports,
    1.35 @@ -374,7 +376,8 @@
    1.36         (Library.merge (eq_snd (op =)) (decls1, decls1'),
    1.37          Library.merge (eq_snd (op =)) (decls2, decls2')),
    1.38        regs = merge_alists regs regs',
    1.39 -      intros = intros};
    1.40 +      intros = intros,
    1.41 +      dests = dests};
    1.42    fun merge _ ((space1, locs1), (space2, locs2)) =
    1.43      (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2));
    1.44  );
    1.45 @@ -420,14 +423,14 @@
    1.46  
    1.47  fun change_locale name f thy =
    1.48    let
    1.49 -    val {axiom, imports, elems, params, lparams, decls, regs, intros} =
    1.50 +    val {axiom, imports, elems, params, lparams, decls, regs, intros, dests} =
    1.51          the_locale thy name;
    1.52 -    val (axiom', imports', elems', params', lparams', decls', regs', intros') =
    1.53 -      f (axiom, imports, elems, params, lparams, decls, regs, intros);
    1.54 +    val (axiom', imports', elems', params', lparams', decls', regs', intros', dests') =
    1.55 +      f (axiom, imports, elems, params, lparams, decls, regs, intros, dests);
    1.56    in
    1.57      put_locale name {axiom = axiom', imports = imports', elems = elems',
    1.58        params = params', lparams = lparams', decls = decls', regs = regs',
    1.59 -      intros = intros'} thy
    1.60 +      intros = intros', dests = dests'} thy
    1.61    end;
    1.62  
    1.63  
    1.64 @@ -485,8 +488,8 @@
    1.65  
    1.66  
    1.67  fun put_registration_in_locale name id =
    1.68 -  change_locale name (fn (axiom, imports, elems, params, lparams, decls, regs, intros) =>
    1.69 -    (axiom, imports, elems, params, lparams, decls, regs @ [(id, [])], intros));
    1.70 +  change_locale name (fn (axiom, imports, elems, params, lparams, decls, regs, intros, dests) =>
    1.71 +    (axiom, imports, elems, params, lparams, decls, regs @ [(id, [])], intros, dests));
    1.72  
    1.73  
    1.74  (* add witness theorem to registration, ignored if registration not present *)
    1.75 @@ -499,11 +502,11 @@
    1.76  
    1.77  
    1.78  fun add_witness_in_locale name id thm =
    1.79 -  change_locale name (fn (axiom, imports, elems, params, lparams, decls, regs, intros) =>
    1.80 +  change_locale name (fn (axiom, imports, elems, params, lparams, decls, regs, intros, dests) =>
    1.81      let
    1.82        fun add (id', thms) =
    1.83          if id = id' then (id', thm :: thms) else (id', thms);
    1.84 -    in (axiom, imports, elems, params, lparams, decls, map add regs, intros) end);
    1.85 +    in (axiom, imports, elems, params, lparams, decls, map add regs, intros, dests) end);
    1.86  
    1.87  
    1.88  (* add equation to registration, ignored if registration not present *)
    1.89 @@ -1426,8 +1429,14 @@
    1.90  
    1.91  in
    1.92  
    1.93 -fun parameters_of thy name =
    1.94 -  the_locale thy name |> #params;
    1.95 +fun parameters_of thy = #params o the_locale thy;
    1.96 +
    1.97 +fun intros thy = #intros o the_locale thy;
    1.98 +  (*returns introduction rule for delta predicate and locale predicate
    1.99 +    as a pair of singleton lists*)
   1.100 +
   1.101 +fun dests thy = #dests o the_locale thy;
   1.102 +
   1.103  
   1.104  fun parameters_of_expr thy expr =
   1.105    let
   1.106 @@ -1449,11 +1458,6 @@
   1.107  
   1.108  end;
   1.109  
   1.110 -fun intros thy =
   1.111 -  #intros o the o Symtab.lookup (#2 (LocalesData.get thy));
   1.112 -    (*returns introduction rule for delta predicate and locale predicate
   1.113 -      as a pair of singleton lists*)
   1.114 -
   1.115  
   1.116  (* full context statements: imports + elements + conclusion *)
   1.117  
   1.118 @@ -1699,9 +1703,9 @@
   1.119          (ctxt, [((("", []), Assumed []), [Ext (Notes (kind, args))])]);
   1.120      val ctxt'' = ctxt' |> ProofContext.theory
   1.121        (change_locale loc
   1.122 -        (fn (axiom, imports, elems, params, lparams, decls, regs, intros) =>
   1.123 +        (fn (axiom, imports, elems, params, lparams, decls, regs, intros, dests) =>
   1.124            (axiom, imports, elems @ [(Notes args', stamp ())],
   1.125 -            params, lparams, decls, regs, intros))
   1.126 +            params, lparams, decls, regs, intros, dests))
   1.127        #> note_thmss_registrations loc args');
   1.128    in ctxt'' end;
   1.129  
   1.130 @@ -1714,8 +1718,8 @@
   1.131  
   1.132  fun add_decls add loc decl =
   1.133    ProofContext.theory (change_locale loc
   1.134 -    (fn (axiom, imports, elems, params, lparams, decls, regs, intros) =>
   1.135 -      (axiom, imports, elems, params, lparams, add (decl, stamp ()) decls, regs, intros))) #>
   1.136 +    (fn (axiom, imports, elems, params, lparams, decls, regs, intros, dests) =>
   1.137 +      (axiom, imports, elems, params, lparams, add (decl, stamp ()) decls, regs, intros, dests))) #>
   1.138    add_thmss loc Thm.internalK
   1.139      [(("", [Attrib.internal (decl_attrib decl)]), [([Drule.dummy_thm], [])])];
   1.140  
   1.141 @@ -1978,7 +1982,8 @@
   1.142          lparams = map #1 (params_of' body_elemss),
   1.143          decls = ([], []),
   1.144          regs = regs,
   1.145 -        intros = intros}
   1.146 +        intros = intros,
   1.147 +        dests = map Element.conclude_witness predicate_axioms}
   1.148        |> init name;
   1.149    in (name, loc_ctxt) end;
   1.150