src/Pure/axclass.ML
changeset 24589 d3fca349736c
parent 24271 499608101177
child 24681 9d4982db0742
     1.1 --- a/src/Pure/axclass.ML	Sat Sep 15 19:27:43 2007 +0200
     1.2 +++ b/src/Pure/axclass.ML	Sat Sep 15 19:27:44 2007 +0200
     1.3 @@ -8,6 +8,16 @@
     1.4  
     1.5  signature AX_CLASS =
     1.6  sig
     1.7 +  val define_class: bstring * class list -> string list ->
     1.8 +    ((bstring * attribute list) * term list) list -> theory -> class * theory
     1.9 +  val define_class_params: bstring * class list -> ((bstring * typ) * mixfix) list ->
    1.10 +    (theory -> (string * typ) list -> ((bstring * attribute list) * term list) list) ->
    1.11 +    string list -> theory ->
    1.12 +    (class * ((string * typ) list * thm list)) * theory
    1.13 +  val add_classrel: thm -> theory -> theory
    1.14 +  val add_arity: thm -> theory -> theory
    1.15 +  val prove_classrel: class * class -> tactic -> theory -> theory
    1.16 +  val prove_arity: string * sort list * sort -> tactic -> theory -> theory
    1.17    val get_definition: theory -> class -> {def: thm, intro: thm, axioms: thm list,
    1.18      params: (string * typ) list}
    1.19    val class_intros: theory -> thm list
    1.20 @@ -17,12 +27,6 @@
    1.21    val print_axclasses: theory -> unit
    1.22    val cert_classrel: theory -> class * class -> class * class
    1.23    val read_classrel: theory -> xstring * xstring -> class * class
    1.24 -  val add_classrel: thm -> theory -> theory
    1.25 -  val add_arity: thm -> theory -> theory
    1.26 -  val prove_classrel: class * class -> tactic -> theory -> theory
    1.27 -  val prove_arity: string * sort list * sort -> tactic -> theory -> theory
    1.28 -  val define_class: bstring * class list -> string list ->
    1.29 -    ((bstring * attribute list) * term list) list -> theory -> class * theory
    1.30    val axiomatize_class: bstring * xstring list -> theory -> theory
    1.31    val axiomatize_class_i: bstring * class list -> theory -> theory
    1.32    val axiomatize_classrel: (xstring * xstring) list -> theory -> theory
    1.33 @@ -359,6 +363,40 @@
    1.34  
    1.35  
    1.36  
    1.37 +(** axclasses with implicit parameter handling **)
    1.38 +
    1.39 +fun define_class_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy =
    1.40 +  let
    1.41 +    val superclasses = map (Sign.certify_class thy) raw_superclasses;
    1.42 +    val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts;
    1.43 +    val prefix = Logic.const_of_class name;
    1.44 +    fun mk_const_name c = NameSpace.map_base (NameSpace.append prefix)
    1.45 +      (Sign.full_name thy c);
    1.46 +    fun add_const ((c, ty), syn) =
    1.47 +      Sign.add_consts_authentic [(c, ty, syn)]
    1.48 +      #> pair (mk_const_name c, ty);
    1.49 +    fun mk_axioms cs thy =
    1.50 +      raw_dep_axioms thy cs
    1.51 +      |> (map o apsnd o map) (Sign.cert_prop thy)
    1.52 +      |> rpair thy;
    1.53 +    fun add_constraint class (c, ty) =
    1.54 +      Sign.add_const_constraint_i (c, SOME
    1.55 +        (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
    1.56 +  in
    1.57 +    thy
    1.58 +    |> Theory.add_path prefix
    1.59 +    |> fold_map add_const consts
    1.60 +    ||> Theory.restore_naming thy
    1.61 +    |-> (fn cs => mk_axioms cs
    1.62 +    #-> (fn axioms_prop => define_class (name, superclasses)
    1.63 +           (map fst cs @ other_consts) axioms_prop
    1.64 +    #-> (fn class => `(fn thy => get_definition thy class)
    1.65 +    #-> (fn {axioms, ...} => fold (add_constraint class) cs
    1.66 +    #> pair (class, (cs, axioms))))))
    1.67 +  end;
    1.68 +
    1.69 +
    1.70 +
    1.71  (** axiomatizations **)
    1.72  
    1.73  local