--- a/src/Pure/Isar/locale.ML Tue Sep 30 15:10:59 2003 +0200
+++ b/src/Pure/Isar/locale.ML Tue Sep 30 15:13:02 2003 +0200
@@ -1,15 +1,15 @@
(* Title: Pure/Isar/locale.ML
ID: $Id$
- Author: Markus Wenzel, LMU/TU München
+ Author: Markus Wenzel, LMU/TU Muenchen
License: GPL (GNU GENERAL PUBLIC LICENSE)
Locales -- Isar proof contexts as meta-level predicates, with local
syntax and implicit structures.
-Draws some basic ideas from Florian Kammüller's original version of
+Draws some basic ideas from Florian Kammueller's original version of
locales, but uses the richer infrastructure of Isar instead of the raw
meta-logic. Furthermore, we provide structured import of contexts
-(with merge and rename operations), well as type-inference of the
+(with merge and rename operations), as well as type-inference of the
signature parts, and predicate definitions of the specification text.
*)
@@ -58,6 +58,7 @@
theory -> theory * (bstring * thm list) list
val add_thmss: string -> ((string * thm list) * context attribute list) list ->
theory * context -> (theory * context) * (string * thm list) list
+ val prune_prems: theory -> thm -> thm
val setup: (theory -> theory) list
end;
@@ -97,7 +98,6 @@
{view = view, import = import, elems = elems, params = params}: locale;
-
(** theory data **)
structure LocalesArgs =
@@ -141,6 +141,185 @@
| None => error ("Unknown locale " ^ quote name));
+(* import hierarchy
+ implementation could be more efficient, eg. by maintaining a database
+ of dependencies *)
+
+fun imports thy (upper, lower) =
+ let
+ val sign = sign_of thy;
+ fun imps (Locale name) low = (name = low) orelse
+ (case get_locale thy name of
+ None => false
+ | Some {import, ...} => imps import low)
+ | imps (Rename (expr, _)) low = imps expr low
+ | imps (Merge es) low = exists (fn e => imps e low) es;
+ in
+ imps (Locale (intern sign upper)) (intern sign lower)
+ end;
+
+(** Name suffix of internal delta predicates.
+ These specify additional assumptions in a locale with import.
+ Also name of theorem set with destruct rules for locale main
+ predicates. **)
+
+val axiomsN = "axioms";
+
+local
+
+(* A trie-like structure is used to compute a cover of a normalised
+ locale specification. Entries of the trie will be identifiers:
+ locale names with parameter lists. *)
+
+datatype 'a trie = Trie of ('a * 'a trie) list;
+
+(* Subsumption relation on identifiers *)
+
+fun subsumes thy ((name1, args1), (name2, args2)) =
+ (name2 = "" andalso null args2) orelse
+ ((name2 = name1 orelse imports thy (name1, name2)) andalso
+ (args2 prefix args1));
+
+(* Insert into trie, wherever possible but avoiding branching *)
+
+fun insert_ident subs id (Trie trie) =
+ let
+ fun insert id [] = [(id, Trie [])]
+ | insert id ((id', Trie t')::ts) =
+ if subs (id, id')
+ then if null ts
+ then [(id', Trie (insert id t'))] (* avoid new branch *)
+ else (id', Trie (insert id t'))::insert id ts
+ else (id', Trie t')::insert id ts
+ in Trie (insert id trie) end;
+
+(* List of leaves of a trie, removing duplicates *)
+
+fun leaves _ (Trie []) = []
+ | leaves eq (Trie ((id, Trie [])::ts)) =
+ gen_ins eq (id, leaves eq (Trie ts))
+ | leaves eq (Trie ((id, ts')::ts)) =
+ gen_merge_lists eq (leaves eq ts') (leaves eq (Trie ts));
+
+in
+
+(* Prune premises: remove internal delta predicates.
+
+ Assumes no outer quanfifiers and no flex-flex pairs.
+ May change names of TVars.
+ Performs compress and close_derivation on result, if modified. *)
+
+fun prune_prems thy thm = let
+ val sign = Theory.sign_of thy;
+ fun analyse cprem =
+ (* Returns None if head of premise is not a predicate defined by a locale,
+ returns also None if locale has import but predicate is not *_axioms
+ since this is a premise that wasn't generated by includes. *)
+ case Term.strip_comb (ObjectLogic.drop_judgment sign (term_of cprem)) of
+ (Const (raw_name, T), args) => let
+ val name = unsuffix ("_" ^ axiomsN) raw_name
+ handle LIST _ => raw_name
+ in case get_locale thy name of
+ None => None
+ | Some {import, ...} =>
+ if name = raw_name andalso import <> empty
+ then None
+ else Some (((name, args), T), name = raw_name)
+ end
+ | _ => None;
+ val TFrees = add_term_tfree_names (prop_of thm, []);
+ (* Ignores TFrees in flex-flex pairs ! *)
+ val (frozen, thaw) = Drule.freeze_thaw thm;
+ val cprop = cprop_of frozen;
+ val cprems = Drule.strip_imp_prems cprop;
+ val analysis = map analyse cprems;
+in
+ if foldl (fn (b, None) => b | (b, Some (_, b')) => b andalso b')
+ (true, analysis)
+ then thm (* No premise contains *_axioms predicate
+ ==> no changes necessary. *)
+ else let
+ val ids = map (apsome fst) analysis;
+ (* Analyse dependencies of locale premises: store in trie. *)
+ fun subs ((x, _), (y, _)) = subsumes thy (x, y);
+ val Trie depcs = foldl (fn (trie, None) => trie
+ | (trie, Some id) => insert_ident subs id trie)
+ (Trie [], ids);
+ (* Assemble new theorem; new prems will be hyps.
+ Axioms is an intermeditate list of locale axioms required to
+ replace old premises by new ones. *)
+ fun scan ((roots, thm, cprems', axioms), (cprem, id)) =
+ case id of
+ None => (roots, implies_elim thm (assume cprem),
+ cprems' @ [cprem], [])
+ (* Normal premise: keep *)
+ | Some id => (* Locale premise *)
+ let
+ fun elim_ax [] thm = (* locale has no axioms *)
+ implies_elim thm (assume cprem)
+ | elim_ax axs thm = let
+ (* Eliminate first premise of thm, which is of the form
+ id. Add hyp of the used axiom to thm. *)
+ val ax = the (assoc (axs, fst (fst id)))
+ handle _ => error ("Internal error in Locale.prune_\
+ \prems: axiom for premise" ^
+ fst (fst id) ^ " not found.");
+ val [ax_cprem] = Drule.strip_imp_prems (cprop_of ax)
+ handle _ => error ("Internal error in Locale.prune_\
+ \prems: exactly one premise in axiom expected.");
+ val ax_hyp = implies_elim ax (assume (ax_cprem))
+ in implies_elim thm ax_hyp
+ end
+ in
+ if null roots
+ then (roots, elim_ax axioms thm, cprems', axioms)
+ (* Remaining premise: drop *)
+ else let
+ fun mk_cprem ((name, args), T) = cterm_of sign
+ (ObjectLogic.assert_propT sign
+ (Term.list_comb (Const (name, T), args)));
+ fun get_axs ((name, args), _) = let
+ val {view = (_, axioms), ...} = the_locale thy name;
+ fun inst ax =
+ let
+ val std = standard ax;
+ val (prem, concl) =
+ Logic.dest_implies (prop_of std);
+ val (Const (name2, _), _) = Term.strip_comb
+ (ObjectLogic.drop_judgment sign concl);
+ val (_, vars) = Term.strip_comb
+ (ObjectLogic.drop_judgment sign prem);
+ val cert = map (cterm_of sign);
+ in (unsuffix ("_" ^ axiomsN) name2
+ handle LIST _ => name2,
+ cterm_instantiate (cert vars ~~ cert args) std)
+ end;
+ in map inst axioms end;
+ val (id', trie) = hd roots;
+ in if id = id'
+ then (* Initial premise *)
+ let
+ val lvs = leaves eq_fst (Trie [(id', trie)]);
+ val axioms' = flat (map get_axs lvs)
+ in (tl roots, elim_ax axioms' thm,
+ cprems' @ map (mk_cprem) lvs, axioms')
+ end
+ else (roots, elim_ax axioms thm, cprems', axioms)
+ (* Remaining premise: drop *)
+ end
+ end;
+ val (_, thm', cprems', _) =
+ (foldl scan ((depcs, frozen, [], []), cprems ~~ ids));
+ val thm'' = implies_intr_list cprems' thm';
+ in
+ fst (varifyT' TFrees (thaw thm''))
+ |> Thm.compress |> Drule.close_derivation
+ end
+end;
+
+end (* local *)
+
+
(* diagnostics *)
fun err_in_locale ctxt msg ids =
@@ -265,15 +444,17 @@
fun unify_frozen ctxt maxidx Ts Us =
let
- val tsig = Sign.tsig_of (ProofContext.sign_of ctxt);
- fun unify (env, (Some T, Some U)) = (Type.unify tsig env (U, T)
- handle Type.TUNIFY => raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
- | unify (env, _) = env;
fun paramify (i, None) = (i, None)
| paramify (i, Some T) = apsnd Some (Type.paramify_dummies (i, T));
val (maxidx', Ts') = foldl_map paramify (maxidx, Ts);
val (maxidx'', Us') = foldl_map paramify (maxidx', Us);
+ val tsig = Sign.tsig_of (ProofContext.sign_of ctxt);
+
+ fun unify (env, (Some T, Some U)) = (Type.unify tsig env (U, T)
+ handle Type.TUNIFY =>
+ raise TYPE ("unify_frozen: failed to unify types", [U, T], []))
+ | unify (env, _) = env;
val (unifier, _) = foldl unify ((Vartab.empty, maxidx''), Ts' ~~ Us');
val Vs = map (apsome (Envir.norm_type unifier)) Us';
val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (mapfilter I Vs));
@@ -323,7 +504,7 @@
foldr Term.add_typ_tfrees (mapfilter snd ps, [])
|> mapfilter (fn (a, S) =>
let val T = Envir.norm_type unifier' (TVar ((a, i), S))
- in if T = TFree (a, S) then None else Some ((a, S), T) end);
+ in if T = TFree (a, S) then None else Some ((a, S), T) end)
in map inst_parms idx_parmss end;
in
@@ -354,6 +535,8 @@
end;
fun identify ((ids, parms), Locale name) =
+ (* CB: ids is list of pairs: locale name and list of parameter renamings,
+ parms is accumulated list of parameters *)
let
val {import, params, ...} = the_locale thy name;
val ps = map #1 (#1 params);
@@ -510,12 +693,19 @@
in
+(* CB: only called by prep_elemss. *)
+
fun declare_elemss prep_fixes fixed_params raw_elemss ctxt =
let
+ (* CB: fix of type bug of goal in target with context elements.
+ Parameters new in context elements must receive types that are
+ distinct from types of parameters in target (fixed_params). *)
+ val ctxt_with_fixed =
+ ProofContext.declare_terms (map Free fixed_params) ctxt;
val int_elemss =
raw_elemss
|> mapfilter (fn (id, Int es) => Some (id, es) | _ => None)
- |> unify_elemss ctxt fixed_params;
+ |> unify_elemss ctxt_with_fixed fixed_params;
val (_, raw_elemss') =
foldl_map (fn ((_, es) :: elemss, (id, Int _)) => (elemss, (id, Int es)) | x => x)
(int_elemss, raw_elemss);
@@ -689,13 +879,24 @@
apsnd (map (apsnd Int)) (flatten_expr context (ids, prep_expr sign expr));
val (import_ids, raw_import_elemss) = flatten ([], Expr import);
+ (* CB: normalise "includes" among elements *)
val raw_elemss = flat (#2 ((foldl_map flatten (import_ids, elements))));
val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close
context fixed_params (raw_import_elemss @ raw_elemss) raw_concl;
-
val (ps,qs) = splitAt(length raw_import_elemss, all_elemss)
val ((import_ctxt, axioms'), (import_elemss, _)) =
activate_facts prep_facts ((context, axioms), ps);
+
+(* CB: testing *)
+
+val axioms' = if true (* null axioms *) then axioms' else
+let val {view = (ax3_view, ax3_axioms), ...} =
+ the_locale (ProofContext.theory_of context) "Type.ax3";
+val ax_TrueFalse = Thm.assume (read_cterm (sign_of_thm (hd axioms))
+ ("True <-> False", propT));
+val {view = (ax4_view, ax4_axioms), ...} =
+ the_locale (ProofContext.theory_of context) "Type.ax4";
+in axioms' @ ax3_axioms @ [ax_TrueFalse] @ (tl ax4_axioms) end;
val ((ctxt, _), (elemss, _)) =
activate_facts prep_facts ((import_ctxt, axioms'), qs);
in
@@ -710,6 +911,7 @@
val thy = ProofContext.theory_of ctxt;
val locale = apsome (prep_locale (Theory.sign_of thy)) raw_locale;
val ((view_statement, view_axioms), fixed_params, import) =
+(* view_axioms are xxx.axioms of locale xxx *)
(case locale of None => (([], []), [], empty)
| Some name =>
let val {view, params = (ps, _), ...} = the_locale thy name
@@ -720,10 +922,29 @@
in
+(* CB
+arguments are (see below): x->import, y->body (elements?), z->context
fun read_context x y z = #1 (gen_context true [] [] x y [] z);
fun cert_context x y z = #1 (gen_context_i true [] [] x y [] z);
+*)
+fun read_context x y z = (warning "read_context\n"; #1 (gen_context true [] [] x y [] z));
+fun cert_context x y z = (warning "cert_context\n"; #1 (gen_context_i true [] [] x y [] z));
+
+(* CB
val read_context_statement = gen_statement intern gen_context;
val cert_context_statement = gen_statement (K I) gen_context_i;
+*)
+
+fun read_context_statement so cs xss ctxt =
+let val (locale, view_statement, locale_ctxt, elems_ctxt, concl') =
+ gen_statement intern gen_context so cs xss ctxt;
+in (locale, view_statement, locale_ctxt, elems_ctxt, concl')
+end;
+fun cert_context_statement so cs xss ctxt =
+let val (locale, view_statement, locale_ctxt, elems_ctxt, concl') =
+ gen_statement (K I) gen_context_i so cs xss ctxt;
+in (locale, view_statement, locale_ctxt, elems_ctxt, concl')
+end;
end;
@@ -837,7 +1058,6 @@
local
val introN = "intro";
-val axiomsN = "axioms";
fun atomize_spec sign ts =
let
@@ -979,6 +1199,7 @@
in
val add_locale = gen_add_locale read_context intern_expr;
+
val add_locale_i = gen_add_locale cert_context (K I);
end;