# HG changeset patch # User wenzelm # Date 1027097047 -7200 # Node ID c136276dc8479b77b7aff25c910ce141b7095c3a # Parent 1cadd412da48c887793b70323e5e29cdba98f0aa support locale ``views'' (for cumulative predicates); diff -r 1cadd412da48 -r c136276dc847 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Fri Jul 19 18:06:31 2002 +0200 +++ b/src/Pure/Isar/locale.ML Fri Jul 19 18:44:07 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 * context * context * (term * (term list * term list)) list list + string option * cterm option * 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 * context * context * (term * (term list * term list)) list list + string option * cterm option * 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,13 +89,22 @@ 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 = - {import: expr, (*dynamic import*) + {view: view, (*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 vs. local params*) + params: (string * typ option) list * string list}; (*all/local params*) -fun make_locale import elems params = - {import = import, elems = elems, params = params}: locale; +fun make_locale view import elems params = + {view = view, import = import, elems = elems, params = params}: locale; @@ -111,8 +120,8 @@ val prep_ext = I; (*joining of locale elements: only facts may be added later!*) - fun join ({import, elems, params}: locale, {elems = elems', ...}: locale) = - Some (make_locale import (gen_merge_lists eq_snd elems elems') params); + fun join ({view, import, elems, params}: locale, {elems = elems', ...}: locale) = + Some (make_locale view import (gen_merge_lists eq_snd elems elems') params); fun merge ((space1, locs1), (space2, locs2)) = (NameSpace.merge (space1, space2), Symtab.join join (locs1, locs2)); @@ -397,35 +406,47 @@ local -fun activate_elem _ (ctxt, Fixes fixes) = (ctxt |> ProofContext.add_fixes fixes, []) - | activate_elem _ (ctxt, Assumes asms) = - ctxt |> ProofContext.fix_frees (flat (map (map #1 o #2) asms)) - |> ProofContext.assume_i ProofContext.export_assume asms - |> apsnd (map (rpair false)) - | activate_elem _ (ctxt, Defines defs) = - ctxt |> ProofContext.assume_i ProofContext.export_def - (defs |> map (fn ((name, atts), (t, ps)) => - let val (c, t') = ProofContext.cert_def ctxt t - in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end)) - |> apsnd (map (rpair false)) - | activate_elem b (ctxt, Notes facts) = - ctxt |> ProofContext.have_thmss_i facts |> apsnd (map (rpair b)); +fun export_axioms axs _ hyps th = + th |> Drule.satisfy_hyps axs + |> Drule.implies_intr_list (Library.drop (length axs, hyps)) + |> Seq.single; -fun activate_elems ((name, ps), elems) = ProofContext.qualified_result (fn ctxt => - foldl_map (activate_elem (name = "")) (ctxt, elems) handle ProofContext.CONTEXT (msg, ctxt) => - err_in_locale ctxt msg [(name, map fst ps)]); +fun activate_elem _ ((ctxt, axs), Fixes fixes) = ((ctxt |> ProofContext.add_fixes fixes, axs), []) + | activate_elem _ ((ctxt, axs), Assumes asms) = + let + val ts = flat (map (map #1 o #2) asms); + val n = length ts; + val (ctxt', res) = + ctxt |> ProofContext.fix_frees ts + |> ProofContext.assume_i (export_axioms (Library.take (n, axs))) asms; + in ((ctxt', Library.drop (n, axs)), map (rpair false) res) end + | activate_elem _ ((ctxt, axs), Defines defs) = + let val (ctxt', res) = + ctxt |> ProofContext.assume_i ProofContext.export_def + (defs |> map (fn ((name, atts), (t, ps)) => + let val (c, t') = ProofContext.cert_def ctxt t + in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end)) + in ((ctxt', axs), map (rpair false) res) end + | activate_elem is_ext ((ctxt, axs), Notes facts) = + let val (ctxt', res) = ctxt |> ProofContext.have_thmss_i facts + in ((ctxt', axs), map (rpair is_ext) res) end; -fun activate_elemss prep_facts = foldl_map (fn (ctxt, ((name, ps), raw_elems)) => +fun activate_elems ((name, ps), elems) (ctxt, axs) = + let val ((ctxt', axs'), res) = + foldl_map (activate_elem (name = "")) ((ProofContext.qualified true ctxt, axs), elems) + handle ProofContext.CONTEXT (msg, ctxt) => err_in_locale ctxt msg [(name, map fst ps)] + in ((ProofContext.restore_qualified ctxt ctxt', axs'), res) end; + +fun activate_elemss prep_facts = foldl_map (fn ((ctxt, axs), ((name, ps), raw_elems)) => let val elems = map (prep_facts ctxt) raw_elems; - val (ctxt', facts) = apsnd flat (activate_elems ((name, ps), elems) ctxt); - in (ctxt', (((name, ps), elems), facts)) end); + val ((ctxt', axs'), res) = apsnd flat (activate_elems ((name, ps), elems) (ctxt, axs)); + in ((ctxt', axs'), (((name, ps), elems), res)) end); in -fun activate_facts prep_facts ctxt_elemss = - let val (ctxt', (elemss', factss)) = apsnd split_list (activate_elemss prep_facts ctxt_elemss) - in (ctxt', (elemss', flat factss)) end; +fun activate_facts prep_facts arg = + apsnd (apsnd flat o Library.split_list) (activate_elemss prep_facts arg); end; @@ -617,8 +638,8 @@ val all_propp' = map2 (op ~~) (#1 (#2 (ProofContext.bind_propp_schematic_i (ctxt, all_propp))), map (map snd) all_propp); val n = length raw_concl; - val concl = take (n, all_propp'); - val propp = drop (n, all_propp'); + val concl = Library.take (n, all_propp'); + val propp = Library.drop (n, all_propp'); val propps = unflat raw_propps propp; val proppss = map (uncurry unflat) (raw_proppss ~~ propps); @@ -669,7 +690,7 @@ local fun prep_context_statement prep_expr prep_elemss prep_facts - do_close fixed_params import elements raw_concl context = + do_close axioms fixed_params import elements raw_concl context = let val sign = ProofContext.sign_of context; @@ -685,10 +706,10 @@ context fixed_params (raw_import_elemss @ raw_elemss) raw_concl; val n = length raw_import_elemss; - val (import_ctxt, (import_elemss, import_facts)) = - activate_facts prep_facts (context, take (n, all_elemss)); - val (ctxt, (elemss, facts)) = - activate_facts prep_facts (import_ctxt, drop (n, all_elemss)); + val ((import_ctxt, axioms'), (import_elemss, import_facts)) = + activate_facts prep_facts ((context, axioms), Library.take (n, all_elemss)); + val ((ctxt, _), (elemss, facts)) = + activate_facts prep_facts ((import_ctxt, axioms'), Library.drop (n, all_elemss)); in ((((import_ctxt, (import_elemss, import_facts)), (ctxt, (elemss, facts))), (parms, spec, defs)), concl) @@ -697,28 +718,31 @@ val gen_context = prep_context_statement intern_expr read_elemss get_facts; val gen_context_i = prep_context_statement (K I) cert_elemss get_facts_i; -fun gen_facts prep_locale thy name = - let val ((((_, (_, facts)), _), _), _) = thy |> ProofContext.init - |> gen_context_i false [] (Locale (prep_locale (Theory.sign_of thy) name)) [] []; - in flat (map (#2 o #1) facts) end; - fun gen_statement prep_locale prep_ctxt raw_locale elems concl ctxt = let val thy = ProofContext.theory_of ctxt; val locale = apsome (prep_locale (Theory.sign_of thy)) raw_locale; - val (fixed_params, import) = - (case locale of None => ([], empty) - | Some name => (param_types (#1 (#params (the_locale thy name))), Locale name)); + val (view, fixed_params, import) = + (case locale of None => (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 fixed_params import elems concl ctxt; - in (locale, locale_ctxt, elems_ctxt, concl') end; + prep_ctxt false (view_axioms view) fixed_params import elems concl ctxt; + in (locale, view_statement view, locale_ctxt, elems_ctxt, concl') end; + +fun gen_facts prep_locale thy name = + let val ((((_, (_, facts)), _), _), _) = thy |> ProofContext.init + |> gen_context_i false [] [] (Locale (prep_locale (Theory.sign_of thy) name)) [] []; + in flat (map (#2 o #1) facts) end; in -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); val locale_facts = gen_facts intern; val locale_facts_i = gen_facts (K I); + +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); val read_context_statement = gen_statement intern gen_context; val cert_context_statement = gen_statement (K I) gen_context_i; @@ -792,18 +816,18 @@ fun put_facts loc args thy = let - val {import, elems, params} = the_locale thy loc; + val {view, import, elems, params} = the_locale thy loc; val note = Notes (map (fn ((a, more_atts), th_atts) => ((a, more_atts), map (apfst (map (curry Thm.name_thm a))) th_atts)) args); - in thy |> put_locale loc (make_locale import (elems @ [(note, stamp ())]) params) end; + in thy |> put_locale loc (make_locale view import (elems @ [(note, stamp ())]) params) end; fun gen_have_thmss prep_locale get_thms kind raw_loc raw_args thy = let val thy_ctxt = ProofContext.init thy; val loc = prep_locale (Theory.sign_of thy) raw_loc; - val loc_ctxt = #1 (#1 (#1 (cert_context (Locale loc) [] thy_ctxt))); + val (_, view, loc_ctxt, _, _) = cert_context_statement (Some loc) [] [] thy_ctxt; val args = map (apsnd (map (apfst (get_thms loc_ctxt)))) raw_args; - val export = ProofContext.export_standard loc_ctxt thy_ctxt; + val export = ProofContext.export_standard view loc_ctxt thy_ctxt; val results = map (map export o #2) (#2 (ProofContext.have_thmss_i args loc_ctxt)); val args' = map (rpair [] o #1 o #1) args ~~ map (single o Thm.no_attributes) results; in @@ -821,7 +845,9 @@ let val args' = map (fn ((a, ths), atts) => ((a, atts), [(ths, [])])) args; val thy' = put_facts loc args' thy; - val (ctxt', (_, facts')) = activate_facts (K I) (ctxt, [((loc, []), [Notes args'])]); + val {view, ...} = the_locale thy loc; + val ((ctxt', _), (_, facts')) = + activate_facts (K I) ((ctxt, view_axioms view), [((loc, []), [Notes args'])]); in ((thy', ctxt'), map #1 facts') end; end; @@ -859,7 +885,7 @@ val Ts = map #2 xs; val extraTs = (Term.term_tfrees body \\ foldr Term.add_typ_tfrees (Ts, [])) |> Library.sort_wrt #1 |> map TFree; - val predT = extraTs ---> Ts ---> bodyT; + val predT = map Term.itselfT extraTs ---> Ts ---> bodyT; val args = map Logic.mk_type extraTs @ map Free xs; val head = Term.list_comb (Const (name, predT), args); @@ -881,9 +907,8 @@ Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) ts'), 0) 1); val conjuncts = - Thm.assume (cert statement) - |> Tactic.rewrite_rule [pred_def] - |> Thm.equal_elim (Thm.symmetric body_eq) + Drule.equal_elim_rule1 OF [Thm.symmetric body_eq, + Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))] |> Drule.conj_elim_precise (length ts); val axioms = (ts ~~ conjuncts) |> map (fn (t, ax) => Tactic.prove defs_sign [] [] t (fn _ => @@ -927,10 +952,11 @@ let val (def_thy, (statement, intro, axioms)) = thy' |> def_pred bname parms defs (ints @ more_ts) (ints' @ more_ts); + val cstatement = Thm.cterm_of (Theory.sign_of def_thy) statement; in def_thy |> have_thmss_qualified "" bname [((introN, [ContextRules.intro_query_global None]), [([intro], [])])] - |> #1 |> rpair (Some (statement, axioms)) + |> #1 |> rpair (Some (cstatement, axioms)) end; in (thy'', (elemss', view)) end; @@ -953,18 +979,18 @@ prep_ctxt raw_import raw_body thy_ctxt; val elemss = import_elemss @ body_elemss; - val (pred_thy, (elemss', view)) = (* FIXME use view *) + val (pred_thy, (elemss', view)) = if do_pred then thy |> define_preds bname text elemss else (thy, (elemss, None)); val pred_ctxt = ProofContext.init pred_thy; - val (ctxt, (_, facts)) = activate_facts (K I) (pred_ctxt, elemss') - val export = ProofContext.export_standard ctxt pred_ctxt; + val ((ctxt, _), (_, facts)) = activate_facts (K I) ((pred_ctxt, view_axioms view), elemss') + val export = ProofContext.export_standard (view_statement view) ctxt pred_ctxt; in pred_thy |> have_thmss_qualified "" name (facts |> filter #2 |> map (fn ((a, ths), _) => ((a, []), [(map export ths, [])]))) |> #1 |> declare_locale name - |> put_locale name (make_locale (prep_expr sign raw_import) + |> put_locale name (make_locale view (prep_expr sign raw_import) (map (fn e => (e, stamp ())) (flat (map #2 (filter (equal "" o #1 o #1) elemss')))) (params_of elemss', map #1 (params_of body_elemss))) end; diff -r 1cadd412da48 -r c136276dc847 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Fri Jul 19 18:06:31 2002 +0200 +++ b/src/Pure/Isar/proof.ML Fri Jul 19 18:44:07 2002 +0200 @@ -133,14 +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)) option} | + locale_spec: ((string * (context attribute list * context attribute list list)) * + cterm option) option} | 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) - | 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) + | 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) | kind_name _ (Show _) = "show" | kind_name _ (Have _) = "have"; @@ -688,9 +690,10 @@ fun global_goal prep kind raw_locale a elems concl thy = let val init = init_state thy; - val (opt_name, locale_ctxt, elems_ctxt, propp) = + 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)); + val locale_spec = + (case raw_locale of None => None | Some (_, x) => Some ((the opt_name, x), view)); in init |> open_block @@ -799,18 +802,19 @@ 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} = + (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 goal_ctxt locale_ctxt) + val locale_results = map (ProofContext.export_standard None goal_ctxt locale_ctxt) (prep_result state ts raw_thm); val results = map (Drule.strip_shyps_warning o - ProofContext.export_standard locale_ctxt theory_ctxt) locale_results; - val {kind = k, theory_spec = ((name, atts), attss), locale_spec} = - (case kind of Theorem x => x | _ => err_malformed "finish_global" state); + 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)) => fn thy => + |> (case locale_spec of None => I | Some ((loc, (loc_atts, loc_attss)), view) => fn thy => if length names <> length loc_attss then raise THEORY ("Bad number of locale attributes", [thy]) else (thy, locale_ctxt) @@ -819,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 locale_spec + |> Locale.smart_have_thmss k (apsome #1 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 locale_spec + |>> (#1 o Locale.smart_have_thmss k (apsome #1 locale_spec) [((name, atts), [(flat (map #2 res), [])])])); in (theory', ((k, name), results')) end; diff -r 1cadd412da48 -r c136276dc847 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri Jul 19 18:06:31 2002 +0200 +++ b/src/Pure/Isar/proof_context.ML Fri Jul 19 18:44:07 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: context -> context -> thm -> thm + val export_standard: cterm option -> 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 @@ -77,7 +77,8 @@ val get_thms: context -> string -> thm list val get_thms_closure: context -> string -> thm list val cond_extern: context -> string -> xstring - val qualified_result: (context -> context * 'a) -> context -> context * 'a + val qualified: bool -> context -> context + val restore_qualified: context -> context -> context val put_thm: string * thm -> context -> context val put_thms: string * thm list -> context -> context val put_thmss: (string * thm list) list -> context -> context @@ -730,7 +731,7 @@ fun find_free t x = foldl_aterms (get_free x) (None, t); -fun export is_goal inner outer = +fun export0 view is_goal inner outer = let val gen = generalize_tfrees inner outer; val fixes = fixed_names_of inner \\ fixed_names_of outer; @@ -739,6 +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 (fn rule => let val {sign, prop, ...} = Thm.rep_thm rule; @@ -752,8 +754,10 @@ end) end; -fun export_standard inner outer = - let val exp = export false inner outer in +val export = export0 None; + +fun export_standard view inner outer = + let val exp = export0 view false inner outer in fn th => (case Seq.pull (exp th) of Some (th', _) => th' |> Drule.local_standard @@ -946,12 +950,11 @@ fun cond_extern (Context {thms = (_, space, _, _), ...}) = NameSpace.cond_extern space; -fun set_qual q = map_context (fn (thy, syntax, data, asms, binds, +fun qualified q = map_context (fn (thy, syntax, data, asms, binds, (_, space, tab, index), cases, defs) => (thy, syntax, data, asms, binds, (q, space, tab, index), cases, defs)); -fun qualified_result f (ctxt as Context {thms, ...}) = - ctxt |> set_qual true |> f |>> set_qual (#1 thms); +fun restore_qualified (Context {thms, ...}) = qualified (#1 thms); (* put_thm(s) *)