moved axclass module closer to core system
authorhaftmann
Fri Apr 20 11:21:47 2007 +0200 (2007-04-20 ago)
changeset 2274517bc6af2011e
parent 22744 5cbe966d67a2
child 22746 f090ecd44f12
moved axclass module closer to core system
src/HOL/Nominal/nominal_atoms.ML
src/Pure/axclass.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Fri Apr 20 11:21:42 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Fri Apr 20 11:21:47 2007 +0200
     1.3 @@ -224,7 +224,7 @@
     1.4                         (HOLogic.mk_Trueprop (cprm_eq $ pi1 $ pi2),
     1.5                          HOLogic.mk_Trueprop (HOLogic.mk_eq (cperm $ pi1 $ x, cperm $ pi2 $ x)));
     1.6        in
     1.7 -          AxClass.define_class_i (cl_name, ["HOL.type"]) []
     1.8 +          AxClass.define_class (cl_name, ["HOL.type"]) []
     1.9                  [((cl_name ^ "1", [Simplifier.simp_add]), [axiom1]),
    1.10                   ((cl_name ^ "2", []), [axiom2]),                           
    1.11                   ((cl_name ^ "3", []), [axiom3])] thy                          
    1.12 @@ -273,7 +273,7 @@
    1.13            val axiom1   = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
    1.14  
    1.15         in  
    1.16 -        AxClass.define_class_i (cl_name, [pt_name]) [] [((cl_name ^ "1", []), [axiom1])] thy            
    1.17 +        AxClass.define_class (cl_name, [pt_name]) [] [((cl_name ^ "1", []), [axiom1])] thy            
    1.18         end) ak_names_types thy8; 
    1.19  	 
    1.20       (* proves that every fs_<ak>-type together with <ak>-type   *)
    1.21 @@ -322,7 +322,7 @@
    1.22  			   (HOLogic.mk_eq (cperm1 $ pi1 $ (cperm2 $ pi2 $ x), 
    1.23                                             cperm2 $ (cperm3 $ pi1 $ pi2) $ (cperm1 $ pi1 $ x)));
    1.24  	       in  
    1.25 -		 AxClass.define_class_i (cl_name, ["HOL.type"]) [] [((cl_name ^ "1", []), [ax1])] thy'  
    1.26 +		 AxClass.define_class (cl_name, ["HOL.type"]) [] [((cl_name ^ "1", []), [ax1])] thy'  
    1.27  	       end) ak_names_types thy) ak_names_types thy12;
    1.28  
    1.29          (* proves for every <ak>-combination a cp_<ak1>_<ak2>_inst theorem;     *)
     2.1 --- a/src/Pure/axclass.ML	Fri Apr 20 11:21:42 2007 +0200
     2.2 +++ b/src/Pure/axclass.ML	Fri Apr 20 11:21:47 2007 +0200
     2.3 @@ -21,11 +21,8 @@
     2.4    val add_arity: thm -> theory -> theory
     2.5    val prove_classrel: class * class -> tactic -> theory -> theory
     2.6    val prove_arity: string * sort list * sort -> tactic -> theory -> theory
     2.7 -  val define_class: bstring * xstring list -> string list ->
     2.8 -    ((bstring * Attrib.src list) * string list) list -> theory -> class * theory
     2.9 -  val define_class_i: bstring * class list -> string list ->
    2.10 +  val define_class: bstring * class list -> string list ->
    2.11      ((bstring * attribute list) * term list) list -> theory -> class * theory
    2.12 -  val read_param: theory -> string -> string
    2.13    val axiomatize_class: bstring * xstring list -> theory -> theory
    2.14    val axiomatize_class_i: bstring * class list -> theory -> theory
    2.15    val axiomatize_classrel: (xstring * xstring) list -> theory -> theory
    2.16 @@ -270,18 +267,7 @@
    2.17  
    2.18  (** class definitions **)
    2.19  
    2.20 -fun read_param thy raw_t =
    2.21 -  let
    2.22 -    val t = Sign.read_term thy raw_t
    2.23 -  in case try dest_Const t
    2.24 -   of SOME (c, _) => c
    2.25 -    | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
    2.26 -  end;
    2.27 -
    2.28 -local
    2.29 -
    2.30 -fun def_class prep_class prep_att prep_param prep_propp
    2.31 -    (bclass, raw_super) raw_params raw_specs thy =
    2.32 +fun define_class (bclass, raw_super) params raw_specs thy =
    2.33    let
    2.34      val ctxt = ProofContext.init thy;
    2.35      val pp = ProofContext.pp ctxt;
    2.36 @@ -291,7 +277,7 @@
    2.37  
    2.38      val bconst = Logic.const_of_class bclass;
    2.39      val class = Sign.full_name thy bclass;
    2.40 -    val super = map (prep_class thy) raw_super |> Sign.certify_sort thy;
    2.41 +    val super = Sign.certify_sort thy raw_super;
    2.42  
    2.43      fun prep_axiom t =
    2.44        (case Term.add_tfrees t [] of
    2.45 @@ -305,9 +291,10 @@
    2.46        |> map_types (Term.map_atyps (fn TFree _ => Term.aT [] | U => U))
    2.47        |> Logic.close_form;
    2.48  
    2.49 -    val axiomss = prep_propp (ctxt, map (map (rpair []) o snd) raw_specs)
    2.50 +    (*FIXME is ProofContext.cert_propp really neccessary?*)
    2.51 +    val axiomss = ProofContext.cert_propp (ctxt, map (map (rpair []) o snd) raw_specs)
    2.52        |> snd |> map (map (prep_axiom o fst));
    2.53 -    val name_atts = Attrib.map_specs (prep_att thy) raw_specs |> map fst;
    2.54 +    val name_atts = map fst raw_specs;
    2.55  
    2.56  
    2.57      (* definition *)
    2.58 @@ -336,7 +323,6 @@
    2.59  
    2.60      (* params *)
    2.61  
    2.62 -    val params = map (prep_param thy) raw_params;
    2.63      val params_typs = map (fn param =>
    2.64        let
    2.65          val ty = Sign.the_const_type thy param;
    2.66 @@ -361,13 +347,6 @@
    2.67  
    2.68    in (class, result_thy) end;
    2.69  
    2.70 -in
    2.71 -
    2.72 -val define_class = def_class Sign.read_class Attrib.attribute read_param ProofContext.read_propp;
    2.73 -val define_class_i = def_class Sign.certify_class (K I) (K I) ProofContext.cert_propp;
    2.74 -
    2.75 -end;
    2.76 -
    2.77  
    2.78  
    2.79  (** axiomatizations **)