# HG changeset patch # User wenzelm # Date 1138144899 -3600 # Node ID ea3b5e22eab509425bcb02ab9d152613efacbba6 # Parent a9c38d41cd27295654469e88c92dac47de8eb0d4 added constant definition; tuned interfaces; tuned; diff -r a9c38d41cd27 -r ea3b5e22eab5 src/Pure/Isar/local_theory.ML --- a/src/Pure/Isar/local_theory.ML Wed Jan 25 00:21:38 2006 +0100 +++ b/src/Pure/Isar/local_theory.ML Wed Jan 25 00:21:39 2006 +0100 @@ -7,22 +7,28 @@ signature LOCAL_THEORY = sig - val map_theory: (theory -> theory) -> Proof.context -> Proof.context - val map_theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * 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 hyps_of: Proof.context -> term list + val standard: Proof.context -> thm -> thm val pretty_consts: Proof.context -> (string * typ) list -> Pretty.T + val theory: (theory -> theory) -> Proof.context -> Proof.context + val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context + val init: xstring option -> theory -> Proof.context + val init_i: string option -> theory -> Proof.context + val exit: Proof.context -> theory val consts: ((string * typ) * mixfix) list -> Proof.context -> term list * Proof.context + val axioms: ((string * Attrib.src list) * term list) list -> Proof.context -> + (bstring * thm list) 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 -> + 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 + val def: (string * mixfix) * ((string * Attrib.src list) * term) -> + Proof.context -> (term * (bstring * thm)) * Proof.context + val def': (Proof.context -> term -> thm -> thm) -> + (string * mixfix) * ((string * Attrib.src list) * term) -> + Proof.context -> (term * (bstring * thm)) * Proof.context end; structure LocalTheory: LOCAL_THEORY = @@ -38,8 +44,9 @@ {locale: string option, params: (string * typ) list, hyps: term list, + standard: Proof.context -> thm -> thm, exit: theory -> theory}; - fun init _ = {locale = NONE, params = [], hyps = [], exit = I}; + fun init _ = {locale = NONE, params = [], hyps = [], standard = K Drule.standard, exit = I}; fun print _ _ = (); ); @@ -48,38 +55,8 @@ val locale_of = #locale o Data.get; val params_of = #params o Data.get; val hyps_of = #hyps o Data.get; - - - -(** theory **) - -fun map_theory f ctxt = - ProofContext.transfer (f (ProofContext.theory_of ctxt)) ctxt; - -fun map_theory_result f ctxt = - let val (res, thy') = f (ProofContext.theory_of ctxt) - in (res, ProofContext.transfer thy' ctxt) end; +fun standard ctxt = #standard (Data.get ctxt) ctxt; -fun init_i NONE thy = ProofContext.init thy - | init_i (SOME loc) thy = - thy - |> Locale.init loc - |> ProofContext.inferred_fixes - ||>> `ProofContext.assms_of - |-> (fn (params, hyps) => Data.put - {locale = SOME loc, - 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 **) (* pretty_consts *) @@ -101,6 +78,37 @@ end; + +(** theory **) + +fun theory f ctxt = + ProofContext.transfer (f (ProofContext.theory_of ctxt)) ctxt; + +fun theory_result f ctxt = + let val (res, thy') = f (ProofContext.theory_of ctxt) + in (res, ProofContext.transfer thy' ctxt) end; + +fun init_i NONE thy = ProofContext.init thy + | init_i (SOME loc) thy = + thy + |> Locale.init loc + |> ProofContext.inferred_fixes + |> (fn (params, ctxt) => Data.put + {locale = SOME loc, + params = params, + hyps = ProofContext.assms_of ctxt, + standard = fn inner => ProofContext.export_standard inner ctxt, + exit = Sign.restore_naming thy} ctxt) + |> 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 **) + (* consts *) fun consts decls ctxt = @@ -111,59 +119,95 @@ val Ps = map snd params; in ctxt - |> map_theory (Sign.add_consts_i (decls |> map (fn ((c, T), mx) => (c, Ps ---> T, mx)))) + |> 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 *) +(* fact definition *) fun notes kind facts ctxt = (case locale_of ctxt of - NONE => ctxt |> map_theory_result + NONE => ctxt |> 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)); + | SOME loc => ctxt |> theory_result (Locale.note_thmss_i kind loc facts #> apsnd #1)); -fun note a ths ctxt = +fun note (a, ths) ctxt = ctxt |> notes Drule.theoremK [(a, [(ths, [])])] |>> hd; (* axioms *) -fun forall_elim frees = +local + +fun add_axiom hyps (name, prop) thy = 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 name' = if name = "" then "axiom_" ^ string_of_int (serial ()) else name; 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 cert = Thm.cterm_of thy'; + fun all_polymorphic (x, T) th = + let 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; + fun implies_polymorphic hyp th = Thm.assume (cert hyp) COMP th; val th = Thm.get_axiom_i thy' (Sign.full_name thy' name') - |> forall_elim frees |> implies_elim hyps - |> Goal.norm_hhf; + |> fold_map all_polymorphic frees |-> Drule.cterm_instantiate + |> fold implies_polymorphic hyps in (th, thy') end; +in + fun axioms specs ctxt = let - val thy = ProofContext.theory_of ctxt; - val hyps = hyps_of ctxt; + fun name_list name [x] = [(name, x)] + | name_list name xs = PureThy.name_multi name xs; + val fixes_ctxt = fold (fold ProofContext.fix_frees o snd) specs ctxt; in ctxt |> fold_map (fn ((name, atts), props) => - map_theory_result (fold_map (add_axiom name hyps) props) #-> note (name, atts)) specs + theory_result (fold_map (add_axiom (hyps_of ctxt)) (name_list name props)) + #-> (fn ths => note ((name, atts), map (standard fixes_ctxt) ths))) specs end; end; + + +(* constant definition *) + +local + +fun add_def (name, prop) thy = + let + val thy' = thy |> Theory.add_defs_i false [(name, prop)]; + val th = Thm.get_axiom_i thy' (Sign.full_name thy' name); + val cert = Thm.cterm_of thy'; + val subst = map2 (fn var => fn free => (cert (Var var), cert (Free free))) + (Term.add_vars (Thm.prop_of th) []) (Term.add_frees prop []); + in (Drule.cterm_instantiate subst th, thy') end; + +in + +fun def' finish (var, spec) ctxt = + let + val (x, mx) = var; + val ((name, atts), rhs) = spec; + val name' = if name = "" then Thm.def_name x else name; + in + ctxt + |> consts [((x, Term.fastype_of rhs), mx)] + |-> (fn [lhs] => + theory_result (add_def (name', Logic.mk_equals (lhs, rhs))) + #-> (fn th => fn ctxt' => note ((name', atts), [finish ctxt' lhs th]) ctxt') + #> apfst (fn (b, [th]) => (lhs, (b, th)))) + end; + +end; + +fun def (var, spec) = + def' (fn ctxt => fn _ => standard (ProofContext.fix_frees (snd spec) ctxt)) (var, spec); + +end;