# HG changeset patch # User wenzelm # Date 1138059809 -3600 # Node ID 2f064e6bea7e4ac15b6b1e5c51cabbbe34710e9f # Parent 932750b85c5bd95d30ee26fe2b99007471df83c8 added actual operations; diff -r 932750b85c5b -r 2f064e6bea7e src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Tue Jan 24 00:43:28 2006 +0100 +++ b/src/Pure/Isar/local_theory.ML Tue Jan 24 00:43:29 2006 +0100 @@ -9,17 +9,27 @@ sig val map_theory: (theory -> theory) -> Proof.context -> Proof.context val map_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context - val init: string option -> theory -> Proof.context + val init: xstring option -> theory -> Proof.context + val init_i: string option -> theory -> Proof.context val exit: Proof.context -> theory + val locale_of: Proof.context -> string option val params_of: Proof.context -> (string * typ) list - val consts: (string * typ * mixfix) list -> Proof.context -> - ((string * typ) list * term list) * Proof.context + val hyps_of: Proof.context -> term list + val pretty_consts: Proof.context -> (string * typ) list -> Pretty.T + val consts: ((string * typ) * mixfix) list -> Proof.context -> term list * Proof.context + val notes: string -> ((bstring * Attrib.src list) * (thm list * Attrib.src list) list) list -> + Proof.context -> (bstring * thm list) list * Proof.context + val note: (bstring * Attrib.src list) -> thm list -> Proof.context -> + (bstring * thm list) * Proof.context + val axioms: ((string * Attrib.src list) * term list) list -> Proof.context -> + (bstring * thm list) list * Proof.context end; structure LocalTheory: LOCAL_THEORY = struct -(* local context data *) + +(** local context data **) structure Data = ProofDataFun ( @@ -35,8 +45,13 @@ val _ = Context.add_setup Data.init; +val locale_of = #locale o Data.get; +val params_of = #params o Data.get; +val hyps_of = #hyps o Data.get; -(* theory *) + + +(** theory **) fun map_theory f ctxt = ProofContext.transfer (f (ProofContext.theory_of ctxt)) ctxt; @@ -45,39 +60,110 @@ let val (res, thy') = f (ProofContext.theory_of ctxt) in (res, ProofContext.transfer thy' ctxt) end; -fun init NONE thy = ProofContext.init thy - | init (SOME loc) thy = +fun init_i NONE thy = ProofContext.init thy + | init_i (SOME loc) thy = thy |> Locale.init loc - |> (fn ctxt => Data.put + |> ProofContext.inferred_fixes + ||>> `ProofContext.assms_of + |-> (fn (params, hyps) => Data.put {locale = SOME loc, - params = Locale.the_params thy loc, - hyps = ProofContext.assms_of ctxt, (* FIXME query locale!! *) - exit = Sign.restore_naming thy} ctxt) - |> map_theory (Sign.add_path loc #> Sign.no_base_names); + params = params, + hyps = hyps, + exit = Sign.restore_naming thy}) + |> map_theory (Sign.add_path (Sign.base_name loc) #> Sign.no_base_names); + +fun init target thy = init_i (Option.map (Locale.intern thy) target) thy; fun exit ctxt = #exit (Data.get ctxt) (ProofContext.theory_of ctxt); -(* local theory *) + +(** local theory **) + +(* pretty_consts *) + +local + +fun pretty_var ctxt (x, T) = + Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1, + Pretty.quote (ProofContext.pretty_typ ctxt T)]; -val params_of = #params o Data.get; +fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs); + +in + +fun pretty_consts ctxt cs = + (case params_of ctxt of + [] => pretty_vars ctxt "constants" cs + | ps => Pretty.chunks [pretty_vars ctxt "parameters" ps, pretty_vars ctxt "constants" cs]); + +end; + + +(* consts *) fun consts decls ctxt = let val thy = ProofContext.theory_of ctxt; val params = params_of ctxt; val ps = map Free params; - val Us = map snd params; - - val xs = decls |> map (fn (c, _, mx) => Syntax.const_name c mx); - val Ts = map #2 decls; - fun const x T = Term.list_comb (Const (Sign.full_name thy x, Us ---> T), ps); + val Ps = map snd params; in ctxt - |> map_theory (Sign.add_consts_i (decls |> map (fn (c, T, mx) => (c, Us ---> T, mx)))) - |> ProofContext.add_fixes_i (decls |> map (fn (c, T, mx) => (c, SOME T, mx))) - |-> (fn xs' => pair ((xs' ~~ Ts), map2 const xs Ts)) + |> map_theory (Sign.add_consts_i (decls |> map (fn ((c, T), mx) => (c, Ps ---> T, mx)))) + |> pair (decls |> map (fn ((c, T), _) => + Term.list_comb (Const (Sign.full_name thy c, Ps ---> T), ps))) + end; + + +(* notes *) + +fun notes kind facts ctxt = + (case locale_of ctxt of + NONE => ctxt |> map_theory_result + (PureThy.note_thmss_i (Drule.kind kind) + (Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts)) + | SOME loc => ctxt |> map_theory_result (Locale.note_thmss_i kind loc facts #> apsnd #1)); + +fun note a ths ctxt = + ctxt |> notes Drule.theoremK [(a, [(ths, [])])] |>> hd; + + +(* axioms *) + +fun forall_elim frees = + let + fun elim (x, T) th = + let + val cert = Thm.cterm_of (Thm.theory_of_thm th); + val var = cert (Var ((x, 0), #1 (Logic.dest_all (Thm.prop_of th)))); + in ((var, cert (Free (x, T))), Thm.forall_elim var th) end; + in fold_map elim frees #-> Drule.cterm_instantiate end; + +fun implies_elim hyps rule = + let val cert = Thm.cterm_of (Thm.theory_of_thm rule) + in fold (fn hyp => fn th => Thm.assume (cert hyp) COMP th) hyps rule end; + +fun add_axiom name hyps prop thy = + let + val name' = (if name = "" then "axiom" else name) ^ "_" ^ string_of_int (serial ()); + val frees = rev ([] |> Term.add_frees prop |> fold Term.add_frees hyps); + val prop' = Term.list_all_free (frees, Logic.list_implies (hyps, prop)); + val thy' = thy |> Theory.add_axioms_i [(name', prop')]; + val th = + Thm.get_axiom_i thy' (Sign.full_name thy' name') + |> forall_elim frees |> implies_elim hyps + |> Goal.norm_hhf; + in (th, thy') end; + +fun axioms specs ctxt = + let + val thy = ProofContext.theory_of ctxt; + val hyps = hyps_of ctxt; + in + ctxt |> fold_map (fn ((name, atts), props) => + map_theory_result (fold_map (add_axiom name hyps) props) #-> note (name, atts)) specs end; end;