diff -r bd976af8bf18 -r b39347206719 src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Jul 18 12:09:44 2002 +0200 +++ b/src/Pure/Isar/locale.ML Thu Jul 18 12:10:24 2002 +0200 @@ -46,10 +46,9 @@ string 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: bstring option option -> bstring - -> expr -> context attribute element list -> theory -> theory - val add_locale_i: bstring option option -> bstring - -> expr -> context attribute element_i list -> theory -> theory + val add_locale: bool -> bstring -> expr -> context attribute element list -> theory -> theory + val add_locale_i: bool -> bstring -> expr -> context attribute element_i list + -> theory -> theory val smart_have_thmss: string -> (string * 'a) Library.option -> ((bstring * theory attribute list) * (thm list * theory attribute list) list) list -> theory -> theory * (bstring * thm list) list @@ -67,7 +66,6 @@ structure Locale: LOCALE = struct - (** locale elements and expressions **) type context = ProofContext.context; @@ -204,7 +202,7 @@ fun rename_facts prfx elem = let fun qualify (arg as ((name, atts), x)) = - if prfx = "" orelse name = "" orelse NameSpace.is_qualified name then arg + if prfx = "" orelse name = "" then arg else ((NameSpace.pack [prfx, name], atts), x); in (case elem of @@ -545,9 +543,14 @@ end; fun eval_text _ _ _ (text, Fixes _) = text - | eval_text _ _ do_text ((spec, (xs, env, defs)), Assumes asms) = - let val ts = map (norm_term env) (flat (map (map #1 o #2) asms)) - in (if do_text then spec @ ts else spec, (foldl Term.add_frees (xs, ts), env, defs)) end + | eval_text _ _ is_ext ((((exts, exts'), (ints, ints')), (xs, env, defs)), Assumes asms) = + let + val ts = flat (map (map #1 o #2) asms); + val ts' = map (norm_term env) ts; + val spec' = + if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints')) + else ((exts, exts'), (ints @ ts, ints' @ ts')); + in (spec', (foldl Term.add_frees (xs, ts'), env, defs)) end | eval_text ctxt id _ ((spec, binds), Defines defs) = (spec, foldl (bind_def ctxt id) (binds, map (#1 o #2) defs)) | eval_text _ _ _ (text, Notes _) = text; @@ -625,8 +628,8 @@ (map (ProofContext.default_type ctxt) xs); val parms = param_types (xs ~~ typing); - val (text, elemss) = - finish_elemss ctxt parms do_close (([], ([], [], [])), raw_elemss ~~ proppss); + val (text, elemss) = finish_elemss ctxt parms do_close + (((([], []), ([], [])), ([], [], [])), raw_elemss ~~ proppss); in ((parms, elemss, concl), text) end; in @@ -681,10 +684,6 @@ val ((parms, all_elemss, concl), (spec, (_, _, defs))) = prep_elemss do_close context fixed_params (raw_import_elemss @ raw_elemss) raw_concl; - val xs = foldl Term.add_frees ([], spec); - val xs' = parms |> mapfilter (fn (x, _) => - (case assoc_string (xs, x) of None => None | Some T => Some (x, T))); - val n = length raw_import_elemss; val (import_ctxt, (import_elemss, import_facts)) = activate_facts prep_facts (context, take (n, all_elemss)); @@ -692,7 +691,7 @@ activate_facts prep_facts (import_ctxt, drop (n, all_elemss)); in ((((import_ctxt, (import_elemss, import_facts)), - (ctxt, (elemss, facts))), (xs', spec, defs)), concl) + (ctxt, (elemss, facts))), (parms, spec, defs)), concl) end; val gen_context = prep_context_statement intern_expr read_elemss get_facts; @@ -733,7 +732,6 @@ fun print_locale thy import body = let - val sg = Theory.sign_of thy; val thy_ctxt = ProofContext.init thy; val (((_, (import_elemss, _)), (ctxt, (elemss, _))), _) = read_context import body thy_ctxt; val all_elems = flat (map #2 (import_elemss @ elemss)); @@ -834,7 +832,7 @@ local val introN = "intro"; -val axiomsN = "axioms"; +val axiomsN = "_axioms"; fun atomize_spec sign ts = let @@ -846,84 +844,95 @@ else (body, bodyT, ObjectLogic.atomize_rule sign (Thm.cterm_of sign t)) end; -fun print_translation name xs thy = - let - val n = length xs; - fun aprop_tr' c = (c, fn args => - if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args) - else raise Match); - in thy |> Theory.add_trfuns ([], [], map aprop_tr' (NameSpace.accesses' name), []) end; +fun aprop_tr' n c = (c, fn args => + if length args = n then Syntax.const "_aprop" $ Term.list_comb (Syntax.free c, args) + else raise Match); -in - -fun define_pred bname loc (xs, ts, defs) elemss thy = +fun def_pred bname parms defs ts ts' thy = let val sign = Theory.sign_of thy; val name = Sign.full_name sign bname; - - (* predicate definition and syntax *) + val (body, bodyT, body_eq) = atomize_spec sign ts'; + val env = Term.add_term_free_names (body, []); + val xs = filter (fn (x, _) => x mem_string env) parms; + 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 (body, bodyT, body_eq) = atomize_spec sign ts; - val predT = map #2 xs ---> bodyT; - val head = Term.list_comb (Const (name, predT), map Free xs); + val args = map Logic.mk_type extraTs @ map Free xs; + val head = Term.list_comb (Const (name, predT), args); val statement = ObjectLogic.assert_propT sign head; val (defs_thy, [pred_def]) = thy - |> (if bodyT = propT then print_translation name xs else I) + |> (if bodyT <> propT then I else + Theory.add_trfuns ([], [], map (aprop_tr' (length args)) (NameSpace.accesses' name), [])) |> Theory.add_consts_i [(bname, predT, Syntax.NoSyn)] |> PureThy.add_defs_i false [((Thm.def_name bname, Logic.mk_equals (head, body)), [])]; + val defs_sign = Theory.sign_of defs_thy; val cert = Thm.cterm_of defs_sign; - - (* introduction rule *) - - val intro = Tactic.prove_standard defs_sign (map #1 xs) ts statement (fn _ => + val intro = Tactic.prove_standard defs_sign [] [] 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); - - - (* derived axioms *) + 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.conj_elim_precise (length ts); - - val assumes = elemss |> map (fn (("", _), es) => - flat (es |> map (fn Assumes asms => flat (map (map #1 o #2) asms) | _ => [])) - | _ => []) |> flat; - - val axioms = (assumes ~~ conjuncts) |> map (fn (t, ax) => + val axioms = (ts ~~ conjuncts) |> map (fn (t, ax) => Tactic.prove defs_sign [] [] t (fn _ => Tactic.rewrite_goals_tac defs THEN Tactic.compose_tac (false, ax, 0) 1)); + in (defs_thy, (statement, intro, axioms)) end; - val implies_intr_assumes = Drule.implies_intr_list (map cert assumes); - fun implies_elim_axioms th = Drule.implies_elim_list (implies_intr_assumes th) axioms; +fun change_elem _ (axms, Assumes asms) = + apsnd Notes ((axms, asms) |> foldl_map (fn (axs, (a, spec)) => + let val n = length spec + in (Library.drop (n, axs), (a, [(Library.take (n, axs), [])])) end)) + | change_elem f (axms, Notes facts) = (axms, Notes (map (apsnd (map (apfst (map f)))) facts)) + | change_elem _ e = e; + +fun change_elemss axioms elemss = (axioms, elemss) |> foldl_map + (fn (axms, (id as ("", _), es)) => + foldl_map (change_elem (Drule.satisfy_hyps axioms)) (axms, es) |> apsnd (pair id) + | x => x) |> #2; + +in - fun change_elem (axms, Assumes asms) = - apsnd Notes ((axms, asms) |> foldl_map (fn (axs, (a, spec)) => - let val n = length spec - in (Library.drop (n, axs), (a, [(Library.take (n, axs), [])])) end)) - | change_elem (axms, Notes facts) = - (axms, Notes (facts |> map (apsnd (map (apfst (map implies_elim_axioms)))))) - | change_elem e = e; - - val elemss' = ((axioms, elemss) |> foldl_map - (fn (axms, (id as ("", _), es)) => foldl_map change_elem (axms, es) |> apsnd (pair id) - | x => x) |> #2) @ - [(("", []), [Assumes [((NameSpace.pack [loc, axiomsN], []), [(statement, ([], []))])]])]; - in - defs_thy - |> have_thmss_qualified "" bname - [((introN, [ContextRules.intro_query_global None]), [([intro], [])])] - |> #1 |> rpair elemss' - end; +fun define_preds bname (parms, ((exts, exts'), (ints, ints')), defs) elemss thy = + let + val (thy', (elemss', more_ts)) = + if Library.null exts then (thy, (elemss, [])) + else + let + val aname = bname ^ axiomsN; + val (def_thy, (statement, intro, axioms)) = + thy |> def_pred aname parms defs exts exts'; + val elemss' = change_elemss axioms elemss @ + [(("", []), [Assumes [((aname, []), [(statement, ([], []))])]])]; + in + def_thy |> have_thmss_qualified "" aname + [((introN, [ContextRules.intro_query_global None]), [([intro], [])])] + |> #1 |> rpair (elemss', [statement]) + end; + val (thy'', view) = + if Library.null more_ts andalso Library.null ints then (thy', None) + else + let + val (def_thy, (statement, intro, axioms)) = + thy' |> def_pred bname parms defs (ints @ more_ts) (ints' @ more_ts); + in + def_thy |> have_thmss_qualified "" bname + [((introN, [ContextRules.intro_query_global None]), [([intro], [])])] + |> #1 |> rpair (Some (statement, axioms)) + end; + in (thy'', (elemss', view)) end; end; @@ -932,7 +941,7 @@ local -fun gen_add_locale prep_ctxt prep_expr pname bname raw_import raw_body thy = +fun gen_add_locale prep_ctxt prep_expr do_pred bname raw_import raw_body thy = let val sign = Theory.sign_of thy; val name = Sign.full_name sign bname; @@ -944,12 +953,9 @@ prep_ctxt raw_import raw_body thy_ctxt; val elemss = import_elemss @ body_elemss; - val (pred_thy, elemss') = - if pname = Some None orelse Library.null (#1 text) then (thy, elemss) - else if pname = None then thy |> define_pred (bname ^ "_axioms") bname text elemss - else thy |> define_pred (the (the pname)) bname text elemss; - val elems' = elemss' |> filter (equal "" o #1 o #1) |> map #2 |> flat; - + val (pred_thy, (elemss', view)) = (* FIXME use 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; @@ -959,7 +965,7 @@ ((a, []), [(map export ths, [])]))) |> #1 |> declare_locale name |> put_locale name (make_locale (prep_expr sign raw_import) - (map (fn e => (e, stamp ())) elems') + (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;