Thm.add_axiom/add_def: return internal name of foundational axiom;
authorwenzelm
Sun Apr 11 14:30:34 2010 +0200 (2010-04-11 ago)
changeset 3610619deea200358
parent 36105 42c37cf849cd
child 36107 2af69e16eced
Thm.add_axiom/add_def: return internal name of foundational axiom;
src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
src/HOL/Tools/typedef.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/overloading.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/theory_target.ML
src/Pure/axclass.ML
src/Pure/more_thm.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sun Apr 11 14:06:35 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sun Apr 11 14:30:34 2010 +0200
     1.3 @@ -91,7 +91,7 @@
     1.4              val (c, thy') =
     1.5                Sign.declare_const ((Binding.conceal (Binding.name cname), cT), NoSyn) thy
     1.6              val cdef = cname ^ "_def"
     1.7 -            val (ax, thy'') =
     1.8 +            val ((_, ax), thy'') =
     1.9                Thm.add_def true false (Binding.name cdef, Logic.mk_equals (c, rhs)) thy'
    1.10              val ax' = Drule.export_without_context ax
    1.11            in dec_sko (subst_bound (list_comb (c, args), p)) (ax' :: axs, thy'') end
     2.1 --- a/src/HOL/Tools/typedef.ML	Sun Apr 11 14:06:35 2010 +0200
     2.2 +++ b/src/HOL/Tools/typedef.ML	Sun Apr 11 14:30:34 2010 +0200
     2.3 @@ -117,7 +117,7 @@
     2.4  
     2.5      val typedef_deps = Term.add_consts A [];
     2.6  
     2.7 -    val (axiom, axiom_thy) = consts_thy
     2.8 +    val ((axiom_name, axiom), axiom_thy) = consts_thy
     2.9        |> Thm.add_axiom (typedef_name, mk_typedef newT oldT RepC AbsC A)
    2.10        ||> Theory.add_deps "" (dest_Const RepC) typedef_deps
    2.11        ||> Theory.add_deps "" (dest_Const AbsC) typedef_deps;
     3.1 --- a/src/Pure/Isar/class_target.ML	Sun Apr 11 14:06:35 2010 +0200
     3.2 +++ b/src/Pure/Isar/class_target.ML	Sun Apr 11 14:30:34 2010 +0200
     3.3 @@ -333,8 +333,8 @@
     3.4      |> Sign.declare_const ((b, Type.strip_sorts ty'), mx)
     3.5      |> snd
     3.6      |> Thm.add_def false false (b_def, def_eq)
     3.7 -    |>> Thm.varifyT_global
     3.8 -    |-> (fn def_thm => PureThy.store_thm (b_def, def_thm)
     3.9 +    |>> apsnd Thm.varifyT_global
    3.10 +    |-> (fn (_, def_thm) => PureThy.store_thm (b_def, def_thm)
    3.11        #> snd
    3.12        #> null type_params ? register_operation class (c', (dict', SOME (Thm.symmetric def_thm))))
    3.13      |> Sign.add_const_constraint (c', SOME ty')
     4.1 --- a/src/Pure/Isar/overloading.ML	Sun Apr 11 14:06:35 2010 +0200
     4.2 +++ b/src/Pure/Isar/overloading.ML	Sun Apr 11 14:30:34 2010 +0200
     4.3 @@ -165,8 +165,9 @@
     4.4  
     4.5  fun declare c_ty = pair (Const c_ty);
     4.6  
     4.7 -fun define checked b (c, t) = Thm.add_def (not checked) true
     4.8 -  (b, Logic.mk_equals (Const (c, Term.fastype_of t), t));
     4.9 +fun define checked b (c, t) =
    4.10 +  Thm.add_def (not checked) true (b, Logic.mk_equals (Const (c, Term.fastype_of t), t))
    4.11 +  #>> snd;
    4.12  
    4.13  fun confirm b = map_overloading (filter_out (fn (_, (c', _)) => c' = Binding.name_of b))
    4.14    #> Local_Theory.target synchronize_syntax
     5.1 --- a/src/Pure/Isar/specification.ML	Sun Apr 11 14:06:35 2010 +0200
     5.2 +++ b/src/Pure/Isar/specification.ML	Sun Apr 11 14:30:34 2010 +0200
     5.3 @@ -173,7 +173,7 @@
     5.4          fold_map Thm.add_axiom
     5.5            (map (apfst (fn a => Binding.map_name (K a) b))
     5.6              (PureThy.name_multi (Name.of_binding b) (map subst props)))
     5.7 -        #>> (fn ths => ((b, atts), [(ths, [])])));
     5.8 +        #>> (fn ths => ((b, atts), [(map #2 ths, [])])));
     5.9  
    5.10      (*facts*)
    5.11      val (facts, facts_lthy) = axioms_thy
     6.1 --- a/src/Pure/Isar/theory_target.ML	Sun Apr 11 14:06:35 2010 +0200
     6.2 +++ b/src/Pure/Isar/theory_target.ML	Sun Apr 11 14:30:34 2010 +0200
     6.3 @@ -315,7 +315,7 @@
     6.4          | NONE =>
     6.5              if is_some (Class_Target.instantiation_param lthy b)
     6.6              then AxClass.define_overloaded name' (head, rhs')
     6.7 -            else Thm.add_def false false (name', Logic.mk_equals (lhs', rhs')));
     6.8 +            else Thm.add_def false false (name', Logic.mk_equals (lhs', rhs')) #>> snd);
     6.9      val def = Local_Defs.trans_terms lthy3
    6.10        [(*c == global.c xs*)     local_def,
    6.11         (*global.c xs == rhs'*)  global_def,
     7.1 --- a/src/Pure/axclass.ML	Sun Apr 11 14:06:35 2010 +0200
     7.2 +++ b/src/Pure/axclass.ML	Sun Apr 11 14:30:34 2010 +0200
     7.3 @@ -306,11 +306,11 @@
     7.4      |-> (fn const' as Const (c'', _) =>
     7.5        Thm.add_def false true
     7.6          (Binding.name (Thm.def_name c'), Logic.mk_equals (Const (c, T'), const'))
     7.7 -      #>> Thm.varifyT_global
     7.8 -      #-> (fn thm => add_inst_param (c, tyco) (c'', thm)
     7.9 -      #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
    7.10 -      #> snd
    7.11 -      #> pair (Const (c, T))))
    7.12 +      #>> apsnd Thm.varifyT_global
    7.13 +      #-> (fn (_, thm) => add_inst_param (c, tyco) (c'', thm)
    7.14 +        #> PureThy.add_thm ((Binding.conceal (Binding.name c'), thm), [])
    7.15 +        #> snd
    7.16 +        #> pair (Const (c, T))))
    7.17      ||> Sign.restore_naming thy
    7.18    end;
    7.19  
    7.20 @@ -325,7 +325,7 @@
    7.21    in
    7.22      thy
    7.23      |> Thm.add_def false false (b', prop)
    7.24 -    |>> (fn thm =>  Drule.transitive_thm OF [eq, thm])
    7.25 +    |>> (fn (_, thm) =>  Drule.transitive_thm OF [eq, thm])
    7.26    end;
    7.27  
    7.28  
    7.29 @@ -515,7 +515,7 @@
    7.30  
    7.31  fun add_axiom (b, prop) =
    7.32    Thm.add_axiom (b, prop) #->
    7.33 -  (fn thm => PureThy.add_thm ((b, Drule.export_without_context thm), []));
    7.34 +  (fn (_, thm) => PureThy.add_thm ((b, Drule.export_without_context thm), []));
    7.35  
    7.36  fun axiomatize prep mk name add raw_args thy =
    7.37    let
     8.1 --- a/src/Pure/more_thm.ML	Sun Apr 11 14:06:35 2010 +0200
     8.2 +++ b/src/Pure/more_thm.ML	Sun Apr 11 14:30:34 2010 +0200
     8.3 @@ -62,8 +62,8 @@
     8.4    val forall_intr_frees: thm -> thm
     8.5    val unvarify_global: thm -> thm
     8.6    val close_derivation: thm -> thm
     8.7 -  val add_axiom: binding * term -> theory -> thm * theory
     8.8 -  val add_def: bool -> bool -> binding * term -> theory -> thm * theory
     8.9 +  val add_axiom: binding * term -> theory -> (string * thm) * theory
    8.10 +  val add_def: bool -> bool -> binding * term -> theory -> (string * thm) * theory
    8.11    type binding = binding * attribute list
    8.12    val empty_binding: binding
    8.13    val rule_attribute: (Context.generic -> thm -> thm) -> attribute
    8.14 @@ -347,31 +347,36 @@
    8.15  fun add_axiom (b, prop) thy =
    8.16    let
    8.17      val b' = if Binding.is_empty b then Binding.name ("unnamed_axiom_" ^ serial_string ()) else b;
    8.18 +
    8.19      val _ = Sign.no_vars (Syntax.pp_global thy) prop;
    8.20      val (strip, recover, prop') = stripped_sorts thy prop;
    8.21      val constraints = map (fn (TFree (_, S), T) => (T, S)) strip;
    8.22      val of_sorts = maps (fn (T as TFree (_, S), _) => of_sort (Thm.ctyp_of thy T, S)) strip;
    8.23 +
    8.24      val thy' =
    8.25        Theory.add_axiom (b', Logic.list_implies (maps Logic.mk_of_sort constraints, prop')) thy;
    8.26 -    val axm' = Thm.axiom thy' (Sign.full_name thy' b');
    8.27 +    val axm_name = Sign.full_name thy' b';
    8.28 +    val axm' = Thm.axiom thy' axm_name;
    8.29      val thm =
    8.30        Thm.instantiate (recover, []) axm'
    8.31        |> unvarify_global
    8.32        |> fold elim_implies of_sorts;
    8.33 -  in (thm, thy') end;
    8.34 +  in ((axm_name, thm), thy') end;
    8.35  
    8.36  fun add_def unchecked overloaded (b, prop) thy =
    8.37    let
    8.38      val _ = Sign.no_vars (Syntax.pp_global thy) prop;
    8.39      val prems = map (Thm.cterm_of thy) (Logic.strip_imp_prems prop);
    8.40      val (_, recover, concl') = stripped_sorts thy (Logic.strip_imp_concl prop);
    8.41 +
    8.42      val thy' = Theory.add_def unchecked overloaded (b, concl') thy;
    8.43 -    val axm' = Thm.axiom thy' (Sign.full_name thy' b);
    8.44 +    val axm_name = Sign.full_name thy' b;
    8.45 +    val axm' = Thm.axiom thy' axm_name;
    8.46      val thm =
    8.47        Thm.instantiate (recover, []) axm'
    8.48        |> unvarify_global
    8.49        |> fold_rev Thm.implies_intr prems;
    8.50 -  in (thm, thy') end;
    8.51 +  in ((axm_name, thm), thy') end;
    8.52  
    8.53  
    8.54  
     9.1 --- a/src/Pure/pure_thy.ML	Sun Apr 11 14:06:35 2010 +0200
     9.2 +++ b/src/Pure/pure_thy.ML	Sun Apr 11 14:30:34 2010 +0200
     9.3 @@ -210,7 +210,7 @@
     9.4  fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
     9.5    let
     9.6      val prop = prep thy (b, raw_prop);
     9.7 -    val (def, thy') = Thm.add_def unchecked overloaded (b, prop) thy;
     9.8 +    val ((_, def), thy') = Thm.add_def unchecked overloaded (b, prop) thy;
     9.9      val thm = def
    9.10        |> Thm.forall_intr_frees
    9.11        |> Thm.forall_elim_vars 0