# HG changeset patch # User ballarin # Date 1064927582 -7200 # Node ID ebf291f3b449df8ecfebdd5c0dbd1c85ca6b7fdd # Parent 5369d671f1009b48d660d5c73c8f6e973413d612 Improvements to Isar/Locales: premises generated by "includes" elements changed. Bugfix "unify_frozen". diff -r 5369d671f100 -r ebf291f3b449 src/Pure/Isar/locale.ML --- 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; diff -r 5369d671f100 -r ebf291f3b449 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Tue Sep 30 15:10:59 2003 +0200 +++ b/src/Pure/Isar/method.ML Tue Sep 30 15:13:02 2003 +0200 @@ -674,7 +674,7 @@ fun inst_args_var f src ctxt = f ctxt (#2 (syntax (Args.goal_spec HEADGOAL -- insts_var) src ctxt)); fun goal_args' args tac src ctxt = #2 (syntax (Args.goal_spec HEADGOAL -- args >> - (fn (quant, s) => SIMPLE_METHOD' quant ( (*K (impose_hyps_tac ctxt) THEN' *) tac s))) src ctxt); + (fn (quant, s) => SIMPLE_METHOD' quant (tac s))) src ctxt); fun goal_args args tac = goal_args' (Scan.lift args) tac; diff -r 5369d671f100 -r ebf291f3b449 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Tue Sep 30 15:10:59 2003 +0200 +++ b/src/Pure/Isar/proof.ML Tue Sep 30 15:13:02 2003 +0200 @@ -821,8 +821,13 @@ val ts = flat tss; val locale_results = map (ProofContext.export_standard [] goal_ctxt locale_ctxt) (prep_result state ts raw_thm); + + val locale_results' = map + (Locale.prune_prems (ProofContext.theory_of locale_ctxt)) + locale_results; + val results = map (Drule.strip_shyps_warning o - ProofContext.export_standard view locale_ctxt theory_ctxt) locale_results; + ProofContext.export_standard view locale_ctxt theory_ctxt) locale_results'; val (theory', results') = theory_of state @@ -830,7 +835,7 @@ if length names <> length loc_attss then raise THEORY ("Bad number of locale attributes", [thy]) else (thy, locale_ctxt) - |> Locale.add_thmss loc ((names ~~ Library.unflat tss locale_results) ~~ loc_attss) + |> Locale.add_thmss loc ((names ~~ Library.unflat tss locale_results') ~~ loc_attss) |> (fn ((thy', ctxt'), res) => if name = "" andalso null loc_atts then thy' else (thy', ctxt')