--- 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;