--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sat Mar 27 14:48:46 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sat Mar 27 18:12:02 2010 +0100
@@ -91,10 +91,10 @@
val (c, thy') =
Sign.declare_const ((Binding.conceal (Binding.name cname), cT), NoSyn) thy
val cdef = cname ^ "_def"
- val thy'' =
- Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
- val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
- in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
+ val (ax, thy'') =
+ Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy'
+ val ax' = Drule.export_without_context ax
+ in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy'') end
| dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx =
(*Universal quant: insert a free variable into body and continue*)
let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
--- a/src/HOL/Tools/record.ML Sat Mar 27 14:48:46 2010 +0100
+++ b/src/HOL/Tools/record.ML Sat Mar 27 18:12:02 2010 +0100
@@ -272,7 +272,7 @@
infix 0 :== ===;
infixr 0 ==>;
-val op :== = Primitive_Defs.mk_defpair;
+val op :== = OldGoals.mk_defpair;
val op === = Trueprop o HOLogic.mk_eq;
val op ==> = Logic.mk_implies;
--- a/src/Pure/Proof/extraction.ML Sat Mar 27 14:48:46 2010 +0100
+++ b/src/Pure/Proof/extraction.ML Sat Mar 27 18:12:02 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:48:46 2010 +0100
+++ b/src/Pure/Proof/proofchecker.ML Sat Mar 27 18:12:02 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:48:46 2010 +0100
+++ b/src/Pure/conjunction.ML Sat Mar 27 18:12:02 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:48:46 2010 +0100
+++ b/src/Pure/drule.ML Sat Mar 27 18:12:02 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:48:46 2010 +0100
+++ b/src/Pure/more_thm.ML Sat Mar 27 18:12:02 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 =
@@ -334,21 +347,30 @@
fun add_axiom (b, prop) thy =
let
val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b;
+ val _ = Sign.no_vars (Syntax.pp_global thy) prop;
val (strip, recover, prop') = stripped_sorts thy prop;
val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
val thy' =
Theory.add_axiom (b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop')) thy;
val axm' = Thm.axiom thy' (Sign.full_name thy' b');
- val thm = unvarify_global (Thm.instantiate (recover, []) axm') |> fold elim_implies of_sorts;
+ val thm =
+ Thm.instantiate (recover, []) axm'
+ |> unvarify_global
+ |> fold elim_implies of_sorts;
in (thm, thy') end;
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 _ = Sign.no_vars (Syntax.pp_global thy) prop;
+ val prems = map (Thm.cterm_of thy) (Logic.strip_imp_prems prop);
+ val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
+ val thy' = Theory.add_def unchecked overloaded (b, concl') thy;
val axm' = Thm.axiom thy' (Sign.full_name thy' b);
- val thm = unvarify_global (Thm.instantiate (recover, []) axm');
+ val thm =
+ Thm.instantiate (recover, []) axm'
+ |> unvarify_global
+ |> fold_rev Thm.implies_intr prems;
in (thm, thy') end;
--- a/src/Pure/old_goals.ML Sat Mar 27 14:48:46 2010 +0100
+++ b/src/Pure/old_goals.ML Sat Mar 27 18:12:02 2010 +0100
@@ -10,6 +10,7 @@
signature OLD_GOALS =
sig
+ val mk_defpair: term * term -> string * term
val strip_context: term -> (string * typ) list * term list * term
val metahyps_thms: int -> thm -> thm list option
val METAHYPS: (thm list -> tactic) -> int -> tactic
@@ -66,6 +67,13 @@
structure OldGoals: OLD_GOALS =
struct
+fun mk_defpair (lhs, rhs) =
+ (case Term.head_of lhs of
+ Const (name, _) =>
+ (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
+ | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
+
+
(**** METAHYPS -- tactical for using hypotheses as meta-level assumptions
METAHYPS (fn prems => tac prems) i
--- a/src/Pure/primitive_defs.ML Sat Mar 27 14:48:46 2010 +0100
+++ b/src/Pure/primitive_defs.ML Sat Mar 27 18:12:02 2010 +0100
@@ -9,7 +9,6 @@
val dest_def: Proof.context -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
term -> (term * term) * term
val abs_def: term -> term * term
- val mk_defpair: term * term -> string * term
end;
structure Primitive_Defs: PRIMITIVE_DEFS =
@@ -78,10 +77,4 @@
val rhs' = Term.list_abs_free (map Term.dest_Free args, rhs);
in (lhs', rhs') end;
-fun mk_defpair (lhs, rhs) =
- (case Term.head_of lhs of
- Const (name, _) =>
- (Long_Name.base_name name ^ "_def", Logic.mk_equals (lhs, rhs))
- | _ => raise TERM ("Malformed definition: head of lhs not a constant", [lhs, rhs]));
-
end;
--- a/src/Pure/pure_thy.ML Sat Mar 27 14:48:46 2010 +0100
+++ b/src/Pure/pure_thy.ML Sat Mar 27 18:12:02 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/sign.ML Sat Mar 27 14:48:46 2010 +0100
+++ b/src/Pure/sign.ML Sat Mar 27 18:12:02 2010 +0100
@@ -68,7 +68,6 @@
val cert_prop: theory -> term -> term
val no_frees: Pretty.pp -> term -> term
val no_vars: Pretty.pp -> term -> term
- val cert_def: Proof.context -> term -> (string * typ) * term
val add_defsort: string -> theory -> theory
val add_defsort_i: sort -> theory -> theory
val add_types: (binding * int * mixfix) list -> theory -> theory
@@ -332,14 +331,6 @@
val no_frees = no_variables "free" Term.add_frees Term.add_tfrees Free TFree;
val no_vars = no_variables "schematic" Term.add_vars Term.add_tvars Var TVar;
-fun cert_def ctxt tm =
- let val ((lhs, rhs), _) = tm
- |> no_vars (Syntax.pp ctxt)
- |> Logic.strip_imp_concl
- |> Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false)
- in (Term.dest_Const (Term.head_of lhs), rhs) end
- handle TERM (msg, _) => error msg;
-
(** signature extension functions **) (*exception ERROR/TYPE*)
--- a/src/Pure/term.ML Sat Mar 27 14:48:46 2010 +0100
+++ b/src/Pure/term.ML Sat Mar 27 18:12:02 2010 +0100
@@ -72,6 +72,7 @@
val map_type_tfree: (string * sort -> typ) -> typ -> typ
val map_types: (typ -> typ) -> term -> term
val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
+ val fold_atyps_sorts: (typ * sort -> 'a -> 'a) -> typ -> 'a -> 'a
val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
val fold_types: (typ -> 'a -> 'a) -> term -> 'a -> 'a
@@ -431,6 +432,9 @@
fun fold_atyps f (Type (_, Ts)) = fold (fold_atyps f) Ts
| fold_atyps f T = f T;
+fun fold_atyps_sorts f =
+ fold_atyps (fn T as TFree (_, S) => f (T, S) | T as TVar (_, S) => f (T, S));
+
fun fold_aterms f (t $ u) = fold_aterms f t #> fold_aterms f u
| fold_aterms f (Abs (_, _, t)) = fold_aterms f t
| fold_aterms f a = f a;
--- a/src/Pure/theory.ML Sat Mar 27 14:48:46 2010 +0100
+++ b/src/Pure/theory.ML Sat Mar 27 18:12:02 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,27 +150,27 @@
-(** add axioms **)
+(** primitive specifications **)
-(* prepare axioms *)
+(* raw axioms *)
fun cert_axm thy (b, raw_tm) =
let
val t = Sign.cert_prop thy raw_tm
handle TYPE (msg, _, _) => error msg
| TERM (msg, _) => error msg;
- in
- Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
- (b, Sign.no_vars (Syntax.pp_global thy) t)
- end;
+ val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
-fun read_axm thy (b, str) =
- cert_axm thy (b, Syntax.read_prop_global thy str) handle ERROR msg =>
+ val bad_sorts =
+ rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []);
+ val _ = null bad_sorts orelse
+ error ("Illegal sort constraints in primitive specification: " ^
+ commas (map (setmp_CRITICAL show_sorts true (Syntax.string_of_typ_global thy)) bad_sorts));
+ in
+ (b, Sign.no_vars (Syntax.pp_global thy) t)
+ end 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 +178,6 @@
in axioms' end);
-
-(** add constant definitions **)
-
(* dependencies *)
fun dependencies thy unchecked def description lhs rhs =
@@ -213,7 +209,7 @@
in (t, add_deps "" const [] thy') end;
-(* check_overloading *)
+(* overloading *)
fun check_overloading thy overloaded (c, T) =
let
@@ -236,13 +232,17 @@
end;
-(* check_def *)
+(* definitional axioms *)
+
+local
fun check_def thy unchecked overloaded (b, tm) defs =
let
val ctxt = ProofContext.init thy;
val name = Sign.full_name thy b;
- val (lhs_const, rhs) = Sign.cert_def ctxt tm;
+ val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
+ handle TERM (msg, _) => error msg;
+ val lhs_const = Term.dest_Const (Term.head_of lhs);
val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
val _ = check_overloading thy overloaded lhs_const;
in defs |> dependencies thy unchecked (SOME name) name lhs_const rhs_consts end
@@ -250,22 +250,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;
--- a/src/Pure/thm.ML Sat Mar 27 14:48:46 2010 +0100
+++ b/src/Pure/thm.ML Sat Mar 27 18:12:02 2010 +0100
@@ -484,10 +484,7 @@
| strip_shyps (thm as Thm (der, {thy_ref, tags, maxidx, shyps, hyps, tpairs, prop})) =
let
val thy = Theory.deref thy_ref;
- val present =
- (fold_terms o fold_types o fold_atyps)
- (fn T as TFree (_, S) => insert (eq_snd op =) (T, S)
- | T as TVar (_, S) => insert (eq_snd op =) (T, S)) thm [];
+ val present = (fold_terms o fold_types o fold_atyps_sorts) (insert (eq_snd op =)) thm [];
val extra = fold (Sorts.remove_sort o #2) present shyps;
val witnessed = Sign.witness_sorts thy present extra;
val extra' = fold (Sorts.remove_sort o #2) witnessed extra
--- a/src/ZF/Tools/datatype_package.ML Sat Mar 27 14:48:46 2010 +0100
+++ b/src/ZF/Tools/datatype_package.ML Sat Mar 27 18:12:02 2010 +0100
@@ -108,7 +108,7 @@
let val ncon = length con_ty_list (*number of constructors*)
fun mk_def (((id,T,syn), name, args, prems), kcon) =
(*kcon is index of constructor*)
- Primitive_Defs.mk_defpair (list_comb (Const (full_name name, T), args),
+ OldGoals.mk_defpair (list_comb (Const (full_name name, T), args),
mk_inject npart kpart
(mk_inject ncon kcon (mk_tuple args)))
in ListPair.map mk_def (con_ty_list, 1 upto ncon) end;
@@ -157,7 +157,7 @@
val case_const = Const (case_name, case_typ);
val case_tm = list_comb (case_const, case_args);
- val case_def = Primitive_Defs.mk_defpair
+ val case_def = OldGoals.mk_defpair
(case_tm, Balanced_Tree.make (fn (t1, t2) => Su.elim $ t1 $ t2) (map call_case case_lists));
@@ -232,7 +232,7 @@
val recursor_cases = map call_recursor (flat case_lists ~~ flat recursor_lists);
val recursor_def =
- Primitive_Defs.mk_defpair
+ OldGoals.mk_defpair
(recursor_tm,
@{const Univ.Vrecursor} $
absfree ("rec", @{typ i}, list_comb (case_const, recursor_cases)));
--- a/src/ZF/Tools/inductive_package.ML Sat Mar 27 14:48:46 2010 +0100
+++ b/src/ZF/Tools/inductive_package.ML Sat Mar 27 18:12:02 2010 +0100
@@ -156,7 +156,7 @@
val big_rec_tm = list_comb(Const(big_rec_name,recT), rec_params);
(*The individual sets must already be declared*)
- val axpairs = map Primitive_Defs.mk_defpair
+ val axpairs = map OldGoals.mk_defpair
((big_rec_tm, fp_rhs) ::
(case parts of
[_] => [] (*no mutual recursion*)