--- a/src/Pure/Isar/locale.ML Wed Jul 24 00:11:56 2002 +0200
+++ b/src/Pure/Isar/locale.ML Wed Jul 24 00:12:50 2002 +0200
@@ -40,10 +40,10 @@
val locale_facts_i: theory -> string -> thm list
val read_context_statement: xstring option -> context attribute element list ->
(string * (string list * string list)) list list -> context ->
- string option * cterm option * context * context * (term * (term list * term list)) list list
+ string option * cterm list * context * context * (term * (term list * term list)) list list
val cert_context_statement: string option -> context attribute element_i list ->
(term * (term list * term list)) list list -> context ->
- string option * cterm option * context * context * (term * (term list * term list)) list list
+ string option * cterm list * context * context * (term * (term list * term list)) list list
val print_locales: theory -> unit
val print_locale: theory -> expr -> context attribute element list -> unit
val add_locale: bool -> bstring -> expr -> context attribute element list -> theory -> theory
@@ -89,16 +89,8 @@
type 'att element = (string, string, string, 'att) elem_expr;
type 'att element_i = (typ, term, thm list, 'att) elem_expr;
-type view = (cterm * thm list) option;
-
-fun view_statement (None: view) = None
- | view_statement (Some (ct, _)) = Some ct;
-
-fun view_axioms (None: view) = []
- | view_axioms (Some (_, axs)) = axs;
-
type locale =
- {view: view, (*external view on assumptions*)
+ {view: cterm list * thm list, (*external view on assumptions*)
import: expr, (*dynamic import*)
elems: ((typ, term, thm list, context attribute) elem * stamp) list, (*static content*)
params: (string * typ option) list * string list}; (*all/local params*)
@@ -722,14 +714,14 @@
let
val thy = ProofContext.theory_of ctxt;
val locale = apsome (prep_locale (Theory.sign_of thy)) raw_locale;
- val (view, fixed_params, import) =
- (case locale of None => (None, [], empty)
+ val ((view_statement, view_axioms), fixed_params, import) =
+ (case locale of None => (([], []), [], empty)
| Some name =>
let val {view, params = (ps, _), ...} = the_locale thy name
in (view, param_types ps, Locale name) end);
val ((((locale_ctxt, _), (elems_ctxt, _)), _), concl') =
- prep_ctxt false (view_axioms view) fixed_params import elems concl ctxt;
- in (locale, view_statement view, locale_ctxt, elems_ctxt, concl') end;
+ prep_ctxt false view_axioms fixed_params import elems concl ctxt;
+ in (locale, view_statement, locale_ctxt, elems_ctxt, concl') end;
fun gen_facts prep_locale thy name =
let val ((((_, (_, facts)), _), _), _) = thy |> ProofContext.init
@@ -845,9 +837,9 @@
let
val args' = map (fn ((a, ths), atts) => ((a, atts), [(ths, [])])) args;
val thy' = put_facts loc args' thy;
- val {view, ...} = the_locale thy loc;
+ val {view = (_, view_axioms), ...} = the_locale thy loc;
val ((ctxt', _), (_, facts')) =
- activate_facts (K I) ((ctxt, view_axioms view), [((loc, []), [Notes args'])]);
+ activate_facts (K I) ((ctxt, view_axioms), [((loc, []), [Notes args'])]);
in ((thy', ctxt'), map #1 facts') end;
end;
@@ -901,7 +893,7 @@
val defs_sign = Theory.sign_of defs_thy;
val cert = Thm.cterm_of defs_sign;
- val intro = Tactic.prove_standard defs_sign [] [] statement (fn _ =>
+ val intro = Tactic.prove_standard defs_sign [] ts' statement (fn _ =>
Tactic.rewrite_goals_tac [pred_def] THEN
Tactic.compose_tac (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) ts'), 0) 1);
@@ -947,7 +939,7 @@
|> #1 |> rpair (elemss', [statement])
end;
val (thy'', view) =
- if Library.null more_ts andalso Library.null ints then (thy', None)
+ if Library.null more_ts andalso Library.null ints then (thy', ([], []))
else
let
val (def_thy, (statement, intro, axioms)) =
@@ -956,7 +948,7 @@
in
def_thy |> have_thmss_qualified "" bname
[((introN, [ContextRules.intro_query_global None]), [([intro], [])])]
- |> #1 |> rpair (Some (cstatement, axioms))
+ |> #1 |> rpair ([cstatement], axioms)
end;
in (thy'', (elemss', view)) end;
@@ -979,12 +971,12 @@
prep_ctxt raw_import raw_body thy_ctxt;
val elemss = import_elemss @ body_elemss;
- val (pred_thy, (elemss', view)) =
+ val (pred_thy, (elemss', view as (view_statement, view_axioms))) =
if do_pred then thy |> define_preds bname text elemss
- else (thy, (elemss, None));
+ else (thy, (elemss, ([], [])));
val pred_ctxt = ProofContext.init pred_thy;
- val ((ctxt, _), (_, facts)) = activate_facts (K I) ((pred_ctxt, view_axioms view), elemss')
- val export = ProofContext.export_standard (view_statement view) ctxt pred_ctxt;
+ val ((ctxt, _), (_, facts)) = activate_facts (K I) ((pred_ctxt, view_axioms), elemss')
+ val export = ProofContext.export_standard view_statement ctxt pred_ctxt;
in
pred_thy
|> have_thmss_qualified "" name (facts |> filter #2 |> map (fn ((a, ths), _) =>
--- a/src/Pure/Isar/proof.ML Wed Jul 24 00:11:56 2002 +0200
+++ b/src/Pure/Isar/proof.ML Wed Jul 24 00:12:50 2002 +0200
@@ -133,16 +133,16 @@
datatype kind =
Theorem of {kind: string,
theory_spec: (bstring * theory attribute list) * theory attribute list list,
- locale_spec: ((string * (context attribute list * context attribute list list)) *
- cterm option) option} |
+ locale_spec: (string * (context attribute list * context attribute list list)) option,
+ view: cterm list} |
Show of context attribute list list |
Have of context attribute list list;
-fun kind_name _ (Theorem {kind = s, theory_spec = ((a, _), _), locale_spec = None}) =
- s ^ (if a = "" then "" else " " ^ a)
+fun kind_name _ (Theorem {kind = s, theory_spec = ((a, _), _),
+ locale_spec = None, view = _}) = s ^ (if a = "" then "" else " " ^ a)
| kind_name sg (Theorem {kind = s, theory_spec = ((a, _), _),
- locale_spec = Some ((name, _), _)}) =
- s ^ " (in " ^ Locale.cond_extern sg name ^ ")" ^ (if a = "" then "" else " " ^ a)
+ locale_spec = Some (name, _), view = _}) =
+ s ^ " (in " ^ Locale.cond_extern sg name ^ ")" ^ (if a = "" then "" else " " ^ a)
| kind_name _ (Show _) = "show"
| kind_name _ (Have _) = "have";
@@ -692,8 +692,6 @@
val init = init_state thy;
val (opt_name, view, locale_ctxt, elems_ctxt, propp) =
prep (apsome fst raw_locale) elems (map snd concl) (context_of init);
- val locale_spec =
- (case raw_locale of None => None | Some (_, x) => Some ((the opt_name, x), view));
in
init
|> open_block
@@ -701,7 +699,10 @@
|> open_block
|> map_context (K elems_ctxt)
|> setup_goal I ProofContext.bind_propp_schematic_i ProofContext.fix_frees
- (Theorem {kind = kind, theory_spec = (a, map (snd o fst) concl), locale_spec = locale_spec})
+ (Theorem {kind = kind,
+ theory_spec = (a, map (snd o fst) concl),
+ locale_spec = (case raw_locale of None => None | Some (_, x) => Some (the opt_name, x)),
+ view = view})
Seq.single true (map (fst o fst) concl) propp
end;
@@ -802,19 +803,18 @@
val (goal_ctxt, (((kind, names, tss), (_, raw_thm)), _)) = current_goal state;
val locale_ctxt = context_of (state |> close_block);
val theory_ctxt = context_of (state |> close_block |> close_block);
- val {kind = k, theory_spec = ((name, atts), attss), locale_spec} =
+ val {kind = k, theory_spec = ((name, atts), attss), locale_spec, view} =
(case kind of Theorem x => x | _ => err_malformed "finish_global" state);
- val view = (case locale_spec of Some (_, Some view) => Some view | _ => None);
val ts = flat tss;
- val locale_results = map (ProofContext.export_standard None goal_ctxt locale_ctxt)
+ val locale_results = map (ProofContext.export_standard [] goal_ctxt locale_ctxt)
(prep_result state ts raw_thm);
val results = map (Drule.strip_shyps_warning o
ProofContext.export_standard view locale_ctxt theory_ctxt) locale_results;
val (theory', results') =
theory_of state
- |> (case locale_spec of None => I | Some ((loc, (loc_atts, loc_attss)), view) => fn thy =>
+ |> (case locale_spec of None => I | Some (loc, (loc_atts, loc_attss)) => fn thy =>
if length names <> length loc_attss then
raise THEORY ("Bad number of locale attributes", [thy])
else (thy, locale_ctxt)
@@ -823,10 +823,10 @@
if name = "" andalso null loc_atts then thy'
else (thy', ctxt')
|> (#1 o #1 o Locale.add_thmss loc [((name, flat (map #2 res)), loc_atts)])))
- |> Locale.smart_have_thmss k (apsome #1 locale_spec)
+ |> Locale.smart_have_thmss k locale_spec
((names ~~ attss) ~~ map (single o Thm.no_attributes) (Library.unflat tss results))
|> (fn (thy, res) => (thy, res)
- |>> (#1 o Locale.smart_have_thmss k (apsome #1 locale_spec)
+ |>> (#1 o Locale.smart_have_thmss k locale_spec
[((name, atts), [(flat (map #2 res), [])])]));
in (theory', ((k, name), results')) end;
--- a/src/Pure/Isar/proof_context.ML Wed Jul 24 00:11:56 2002 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Jul 24 00:12:50 2002 +0200
@@ -48,7 +48,7 @@
val generalize: context -> context -> term list -> term list
val find_free: term -> string -> term option
val export: bool -> context -> context -> thm -> thm Seq.seq
- val export_standard: cterm option -> context -> context -> thm -> thm
+ val export_standard: cterm list -> context -> context -> thm -> thm
val drop_schematic: indexname * term option -> indexname * term option
val add_binds: (indexname * string option) list -> context -> context
val add_binds_i: (indexname * term option) list -> context -> context
@@ -731,7 +731,7 @@
fun find_free t x = foldl_aterms (get_free x) (None, t);
-fun export0 view is_goal inner outer =
+fun export_view view is_goal inner outer =
let
val gen = generalize_tfrees inner outer;
val fixes = fixed_names_of inner \\ fixed_names_of outer;
@@ -740,7 +740,7 @@
in fn thm => thm
|> Tactic.norm_hhf_rule
|> Seq.EVERY (rev exp_asms)
- |> Seq.map (case view of None => I | Some A => Thm.implies_intr A)
+ |> Seq.map (Drule.implies_intr_list view)
|> Seq.map (fn rule =>
let
val {sign, prop, ...} = Thm.rep_thm rule;
@@ -754,10 +754,10 @@
end)
end;
-val export = export0 None;
+val export = export_view [];
fun export_standard view inner outer =
- let val exp = export0 view false inner outer in
+ let val exp = export_view view false inner outer in
fn th =>
(case Seq.pull (exp th) of
Some (th', _) => th' |> Drule.local_standard