moved Drule.forall_intr_frees to Thm.forall_intr_frees (in more_thm.ML, which is loaded before pure_thy.ML);
discontinued old-style Theory.add_defs(_i) in favour of more basic Theory.add_def;
modernized PureThy.add_defs etc. -- refer to high-level Thm.add_def;
--- a/src/Pure/Proof/extraction.ML Sat Mar 27 14:10:37 2010 +0100
+++ b/src/Pure/Proof/extraction.ML Sat Mar 27 15:20:31 2010 +0100
@@ -733,7 +733,7 @@
thy'
|> PureThy.store_thm (Binding.qualified_name (corr_name s vs),
Thm.varifyT_global (funpow (length (OldTerm.term_vars corr_prop))
- (Thm.forall_elim_var 0) (forall_intr_frees
+ (Thm.forall_elim_var 0) (Thm.forall_intr_frees
(ProofChecker.thm_of_proof thy'
(fst (Proofterm.freeze_thaw_prf prf))))))
|> snd
--- a/src/Pure/Proof/proofchecker.ML Sat Mar 27 14:10:37 2010 +0100
+++ b/src/Pure/Proof/proofchecker.ML Sat Mar 27 15:20:31 2010 +0100
@@ -40,7 +40,7 @@
val ctye = map (pairself (Thm.ctyp_of thy))
(map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts)
in
- Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm'))
+ Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
end;
fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts), _))) =
--- a/src/Pure/conjunction.ML Sat Mar 27 14:10:37 2010 +0100
+++ b/src/Pure/conjunction.ML Sat Mar 27 15:20:31 2010 +0100
@@ -137,7 +137,7 @@
fun comp_rule th rule =
Thm.adjust_maxidx_thm ~1 (th COMP
- (rule |> Drule.forall_intr_frees |> Thm.forall_elim_vars (Thm.maxidx_of th + 1)));
+ (rule |> Thm.forall_intr_frees |> Thm.forall_elim_vars (Thm.maxidx_of th + 1)));
in
--- a/src/Pure/drule.ML Sat Mar 27 14:10:37 2010 +0100
+++ b/src/Pure/drule.ML Sat Mar 27 15:20:31 2010 +0100
@@ -16,7 +16,6 @@
val cterm_fun: (term -> term) -> (cterm -> cterm)
val ctyp_fun: (typ -> typ) -> (ctyp -> ctyp)
val forall_intr_list: cterm list -> thm -> thm
- val forall_intr_frees: thm -> thm
val forall_intr_vars: thm -> thm
val forall_elim_list: cterm list -> thm -> thm
val gen_all: thm -> thm
@@ -214,16 +213,6 @@
(*Generalization over a list of variables*)
val forall_intr_list = fold_rev forall_intr;
-(*Generalization over all suitable Free variables*)
-fun forall_intr_frees th =
- let
- val thy = Thm.theory_of_thm th;
- val {prop, hyps, tpairs, ...} = rep_thm th;
- val fixed = fold Term.add_frees (Thm.terms_of_tpairs tpairs @ hyps) [];
- val frees = Term.fold_aterms (fn Free v =>
- if member (op =) fixed v then I else insert (op =) v | _ => I) prop [];
- in fold (forall_intr o cterm_of thy o Free) frees th end;
-
(*Generalization over Vars -- canonical order*)
fun forall_intr_vars th =
fold forall_intr
@@ -306,7 +295,7 @@
val export_without_context_open =
implies_intr_hyps
- #> forall_intr_frees
+ #> Thm.forall_intr_frees
#> `Thm.maxidx_of
#-> (fn maxidx =>
Thm.forall_elim_vars (maxidx + 1)
--- a/src/Pure/more_thm.ML Sat Mar 27 14:10:37 2010 +0100
+++ b/src/Pure/more_thm.ML Sat Mar 27 15:20:31 2010 +0100
@@ -59,6 +59,7 @@
(ctyp * ctyp) list * (cterm * cterm) list
val certify_instantiate:
((indexname * sort) * typ) list * ((indexname * typ) * term) list -> thm -> thm
+ val forall_intr_frees: thm -> thm
val unvarify_global: thm -> thm
val close_derivation: thm -> thm
val add_axiom: binding * term -> theory -> thm * theory
@@ -295,6 +296,18 @@
Thm.instantiate (certify_inst (Thm.theory_of_thm th) insts) th;
+(* forall_intr_frees: generalization over all suitable Free variables *)
+
+fun forall_intr_frees th =
+ let
+ val thy = Thm.theory_of_thm th;
+ val {prop, hyps, tpairs, ...} = Thm.rep_thm th;
+ val fixed = fold Term.add_frees (Thm.terms_of_tpairs tpairs @ hyps) [];
+ val frees = Term.fold_aterms (fn Free v =>
+ if member (op =) fixed v then I else insert (op =) v | _ => I) prop [];
+ in fold (Thm.forall_intr o Thm.cterm_of thy o Free) frees th end;
+
+
(* unvarify_global: global schematic variables *)
fun unvarify_global th =
@@ -346,7 +359,7 @@
fun add_def unchecked overloaded (b, prop) thy =
let
val (strip, recover, prop') = stripped_sorts thy prop;
- val thy' = Theory.add_defs_i unchecked overloaded [(b, prop')] thy;
+ val thy' = Theory.add_def unchecked overloaded (b, prop') thy;
val axm' = Thm.axiom thy' (Sign.full_name thy' b);
val thm = unvarify_global (Thm.instantiate (recover, []) axm');
in (thm, thy') end;
--- a/src/Pure/pure_thy.ML Sat Mar 27 14:10:37 2010 +0100
+++ b/src/Pure/pure_thy.ML Sat Mar 27 15:20:31 2010 +0100
@@ -200,16 +200,30 @@
(* store axioms as theorems *)
local
- fun add_axm add = fold_map (fn ((b, prop), atts) => fn thy =>
- let
- val thy' = add [(b, prop)] thy;
- val thm = Thm.forall_elim_vars 0 (Thm.axiom thy' (Sign.full_name thy' b));
- in apfst hd (gen_add_thms (K I) [((b, thm), atts)] thy') end);
+
+fun no_read _ (_, t) = t;
+
+fun read thy (b, str) =
+ Syntax.read_prop_global thy str handle ERROR msg =>
+ cat_error msg ("The error(s) above occurred in definition " ^ quote (Binding.str_of b));
+
+fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
+ let
+ val prop = prep thy (b, raw_prop);
+ val (def, thy') = Thm.add_def unchecked overloaded (b, prop) thy;
+ val thm = def
+ |> Thm.forall_intr_frees
+ |> Thm.forall_elim_vars 0
+ |> Thm.varifyT_global;
+ in yield_singleton (gen_add_thms (K I)) ((b, thm), atts) thy' end);
+
in
- val add_defs = add_axm o Theory.add_defs_i false;
- val add_defs_unchecked = add_axm o Theory.add_defs_i true;
- val add_defs_cmd = add_axm o Theory.add_defs false;
- val add_defs_unchecked_cmd = add_axm o Theory.add_defs true;
+
+val add_defs = add no_read false;
+val add_defs_unchecked = add no_read true;
+val add_defs_cmd = add read false;
+val add_defs_unchecked_cmd = add read true;
+
end;
--- a/src/Pure/theory.ML Sat Mar 27 14:10:37 2010 +0100
+++ b/src/Pure/theory.ML Sat Mar 27 15:20:31 2010 +0100
@@ -30,8 +30,7 @@
val end_theory: theory -> theory
val add_axiom: binding * term -> theory -> theory
val add_deps: string -> string * typ -> (string * typ) list -> theory -> theory
- val add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory
- val add_defs: bool -> bool -> (binding * string) list -> theory -> theory
+ val add_def: bool -> bool -> binding * term -> theory -> theory
val add_finals_i: bool -> term list -> theory -> theory
val add_finals: bool -> string list -> theory -> theory
val specify_const: (binding * typ) * mixfix -> theory -> term * theory
@@ -151,9 +150,9 @@
-(** add axioms **)
+(** primitive specifications **)
-(* prepare axioms *)
+(* raw axioms *)
fun cert_axm thy (b, raw_tm) =
let
@@ -165,13 +164,6 @@
(b, Sign.no_vars (Syntax.pp_global thy) t)
end;
-fun read_axm thy (b, str) =
- cert_axm thy (b, Syntax.read_prop_global thy str) handle ERROR msg =>
- cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
-
-
-(* add_axiom *)
-
fun add_axiom raw_axm thy = thy |> map_axioms (fn axioms =>
let
val axm = apsnd Logic.varify_global (cert_axm thy raw_axm);
@@ -179,9 +171,6 @@
in axioms' end);
-
-(** add constant definitions **)
-
(* dependencies *)
fun dependencies thy unchecked def description lhs rhs =
@@ -213,7 +202,7 @@
in (t, add_deps "" const [] thy') end;
-(* check_overloading *)
+(* overloading *)
fun check_overloading thy overloaded (c, T) =
let
@@ -236,7 +225,9 @@
end;
-(* check_def *)
+(* definitional axioms *)
+
+local
fun check_def thy unchecked overloaded (b, tm) defs =
let
@@ -250,22 +241,14 @@
[Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.str_of b) ^ ":"),
Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
-
-(* add_defs(_i) *)
-
-local
-
-fun gen_add_defs prep_axm unchecked overloaded raw_axms thy =
- let val axms = map (prep_axm thy) raw_axms in
- thy
- |> map_defs (fold (check_def thy unchecked overloaded) axms)
- |> fold add_axiom axms
- end;
-
in
-val add_defs_i = gen_add_defs cert_axm;
-val add_defs = gen_add_defs read_axm;
+fun add_def unchecked overloaded raw_axm thy =
+ let val axm = cert_axm thy raw_axm in
+ thy
+ |> map_defs (check_def thy unchecked overloaded axm)
+ |> add_axiom axm
+ end;
end;