disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
authorwenzelm
Sat Mar 27 17:36:32 2010 +0100 (2010-03-27)
changeset 3598876ca601c941e
parent 35987 7c728daf4876
child 35989 3418cdf1855e
disallow premises in primitive Theory.add_def -- handle in Thm.add_def;
eliminated obsolete Sign.cert_def;
misc tuning and clarification;
src/Pure/more_thm.ML
src/Pure/sign.ML
src/Pure/theory.ML
     1.1 --- a/src/Pure/more_thm.ML	Sat Mar 27 16:01:45 2010 +0100
     1.2 +++ b/src/Pure/more_thm.ML	Sat Mar 27 17:36:32 2010 +0100
     1.3 @@ -347,21 +347,30 @@
     1.4  fun add_axiom (b, prop) thy =
     1.5    let
     1.6      val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b;
     1.7 +    val _ = Sign.no_vars (Syntax.pp_global thy) prop;
     1.8      val (strip, recover, prop') = stripped_sorts thy prop;
     1.9      val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
    1.10      val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
    1.11      val thy' =
    1.12        Theory.add_axiom (b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop')) thy;
    1.13      val axm' = Thm.axiom thy' (Sign.full_name thy' b');
    1.14 -    val thm = unvarify_global (Thm.instantiate (recover, []) axm') |> fold elim_implies of_sorts;
    1.15 +    val thm =
    1.16 +      Thm.instantiate (recover, []) axm'
    1.17 +      |> unvarify_global
    1.18 +      |> fold elim_implies of_sorts;
    1.19    in (thm, thy') end;
    1.20  
    1.21  fun add_def unchecked overloaded (b, prop) thy =
    1.22    let
    1.23 -    val (strip, recover, prop') = stripped_sorts thy prop;
    1.24 -    val thy' = Theory.add_def unchecked overloaded (b, prop') thy;
    1.25 +    val _ = Sign.no_vars (Syntax.pp_global thy) prop;
    1.26 +    val prems = map (Thm.cterm_of thy) (Logic.strip_imp_prems prop);
    1.27 +    val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
    1.28 +    val thy' = Theory.add_def unchecked overloaded (b, concl') thy;
    1.29      val axm' = Thm.axiom thy' (Sign.full_name thy' b);
    1.30 -    val thm = unvarify_global (Thm.instantiate (recover, []) axm');
    1.31 +    val thm =
    1.32 +      Thm.instantiate (recover, []) axm'
    1.33 +      |> unvarify_global
    1.34 +      |> fold_rev Thm.implies_intr prems;
    1.35    in (thm, thy') end;
    1.36  
    1.37  
     2.1 --- a/src/Pure/sign.ML	Sat Mar 27 16:01:45 2010 +0100
     2.2 +++ b/src/Pure/sign.ML	Sat Mar 27 17:36:32 2010 +0100
     2.3 @@ -68,7 +68,6 @@
     2.4    val cert_prop: theory -> term -> term
     2.5    val no_frees: Pretty.pp -> term -> term
     2.6    val no_vars: Pretty.pp -> term -> term
     2.7 -  val cert_def: Proof.context -> term -> (string * typ) * term
     2.8    val add_defsort: string -> theory -> theory
     2.9    val add_defsort_i: sort -> theory -> theory
    2.10    val add_types: (binding * int * mixfix) list -> theory -> theory
    2.11 @@ -332,14 +331,6 @@
    2.12  val no_frees = no_variables "free" Term.add_frees Term.add_tfrees Free TFree;
    2.13  val no_vars = no_variables "schematic" Term.add_vars Term.add_tvars Var TVar;
    2.14  
    2.15 -fun cert_def ctxt tm =
    2.16 -  let val ((lhs, rhs), _) = tm
    2.17 -    |> no_vars (Syntax.pp ctxt)
    2.18 -    |> Logic.strip_imp_concl
    2.19 -    |> Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false)
    2.20 -  in (Term.dest_Const (Term.head_of lhs), rhs) end
    2.21 -  handle TERM (msg, _) => error msg;
    2.22 -
    2.23  
    2.24  
    2.25  (** signature extension functions **)  (*exception ERROR/TYPE*)
     3.1 --- a/src/Pure/theory.ML	Sat Mar 27 16:01:45 2010 +0100
     3.2 +++ b/src/Pure/theory.ML	Sat Mar 27 17:36:32 2010 +0100
     3.3 @@ -240,7 +240,9 @@
     3.4    let
     3.5      val ctxt = ProofContext.init thy;
     3.6      val name = Sign.full_name thy b;
     3.7 -    val (lhs_const, rhs) = Sign.cert_def ctxt tm;
     3.8 +    val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
     3.9 +      handle TERM (msg, _) => error msg;
    3.10 +    val lhs_const = Term.dest_Const (Term.head_of lhs);
    3.11      val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
    3.12      val _ = check_overloading thy overloaded lhs_const;
    3.13    in defs |> dependencies thy unchecked (SOME name) name lhs_const rhs_consts end