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