clarified class interfaces and internals
authorhaftmann
Sat Sep 15 19:27:44 2007 +0200 (2007-09-15)
changeset 24589d3fca349736c
parent 24588 ed9a1254d674
child 24590 733120d04233
clarified class interfaces and internals
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/datatype_package.ML
src/Pure/Isar/class.ML
src/Pure/Isar/isar_syn.ML
src/Pure/axclass.ML
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Sat Sep 15 19:27:43 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Sat Sep 15 19:27:44 2007 +0200
     1.3 @@ -427,7 +427,7 @@
     1.4          val n = Sign.arity_number thy tyco;
     1.5        in
     1.6          thy
     1.7 -        |> Class.prove_instance_arity (Class.intro_classes_tac [])
     1.8 +        |> Class.prove_instance (Class.intro_classes_tac [])
     1.9              [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
    1.10          |> snd
    1.11        end
     2.1 --- a/src/HOL/Tools/datatype_codegen.ML	Sat Sep 15 19:27:43 2007 +0200
     2.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Sat Sep 15 19:27:44 2007 +0200
     2.3 @@ -1,4 +1,4 @@
     2.4 -(*  Title:      HOL/datatype_codegen.ML
     2.5 +(*  Title:      HOL/Tools/datatype_codegen.ML
     2.6      ID:         $Id$
     2.7      Author:     Stefan Berghofer & Florian Haftmann, TU Muenchen
     2.8  
     2.9 @@ -590,7 +590,7 @@
    2.10          |> not (null arities) ? (
    2.11              f arities css
    2.12              #-> (fn defs =>
    2.13 -              Class.prove_instance_arity tac arities defs
    2.14 +              Class.prove_instance tac arities defs
    2.15              #-> (fn defs =>
    2.16                after_qed arities css defs)))
    2.17        end;
     3.1 --- a/src/HOL/Tools/datatype_package.ML	Sat Sep 15 19:27:43 2007 +0200
     3.2 +++ b/src/HOL/Tools/datatype_package.ML	Sat Sep 15 19:27:44 2007 +0200
     3.3 @@ -565,7 +565,7 @@
     3.4          val n = Sign.arity_number thy tyco;
     3.5        in
     3.6          thy
     3.7 -        |> Class.prove_instance_arity (Class.intro_classes_tac [])
     3.8 +        |> Class.prove_instance (Class.intro_classes_tac [])
     3.9              [(tyco, replicate n HOLogic.typeS, [HOLogic.class_size])] []
    3.10          |> snd
    3.11        end
     4.1 --- a/src/Pure/Isar/class.ML	Sat Sep 15 19:27:43 2007 +0200
     4.2 +++ b/src/Pure/Isar/class.ML	Sat Sep 15 19:27:44 2007 +0200
     4.3 @@ -10,23 +10,32 @@
     4.4    val fork_mixfix: bool -> string option -> mixfix -> mixfix * mixfix
     4.5  
     4.6    val axclass_cmd: bstring * xstring list
     4.7 -    -> ((bstring * Attrib.src list) * string list) list -> theory -> class * theory
     4.8 +    -> ((bstring * Attrib.src list) * string list) list
     4.9 +    -> theory -> class * theory
    4.10 +  val classrel_cmd: xstring * xstring -> theory -> Proof.state
    4.11    val class: bstring -> class list -> Element.context_i Locale.element list
    4.12      -> string list -> theory -> string * Proof.context
    4.13 -  val class_cmd: bstring -> string list -> Element.context Locale.element list
    4.14 -    -> string list -> theory -> string * Proof.context
    4.15 -  val class_of_locale: theory -> string -> class option
    4.16 +  val class_cmd: bstring -> xstring list -> Element.context Locale.element list
    4.17 +    -> xstring list -> theory -> string * Proof.context
    4.18    val add_const_in_class: string -> (string * term) * Syntax.mixfix
    4.19      -> theory -> theory
    4.20 +  val interpretation_in_class: class * class -> theory -> Proof.state
    4.21 +  val interpretation_in_class_cmd: xstring * xstring -> theory -> Proof.state
    4.22 +  val prove_interpretation_in_class: tactic -> class * class -> theory -> theory
    4.23 +  val intro_classes_tac: thm list -> tactic
    4.24 +  val default_intro_classes_tac: thm list -> tactic
    4.25 +  val class_of_locale: theory -> string -> class option
    4.26 +  val print_classes: theory -> unit
    4.27  
    4.28 -  val instance_arity: arity list -> ((bstring * Attrib.src list) * term) list
    4.29 +  val instance_arity: (theory -> theory) -> arity list -> theory -> Proof.state
    4.30 +  val instance: arity list -> ((bstring * Attrib.src list) * term) list
    4.31      -> (thm list -> theory -> theory)
    4.32      -> theory -> Proof.state
    4.33 -  val instance_arity_cmd: (bstring * string list * string) list
    4.34 -    -> ((bstring * Attrib.src list) * string) list
    4.35 +  val instance_cmd: (bstring * xstring list * xstring) list
    4.36 +    -> ((bstring * Attrib.src list) * xstring) list
    4.37      -> (thm list -> theory -> theory)
    4.38      -> theory -> Proof.state
    4.39 -  val prove_instance_arity: tactic -> arity list
    4.40 +  val prove_instance: tactic -> arity list
    4.41      -> ((bstring * Attrib.src list) * term) list
    4.42      -> theory -> thm list * theory
    4.43    val unoverload: theory -> conv
    4.44 @@ -35,16 +44,6 @@
    4.45    val inst_const: theory -> string * string -> string
    4.46    val param_const: theory -> string -> (string * string) option
    4.47    val params_of_sort: theory -> sort -> (string * (string * typ)) list
    4.48 -  val intro_classes_tac: thm list -> tactic
    4.49 -  val default_intro_classes_tac: thm list -> tactic
    4.50 -
    4.51 -  val instance_class: class * class -> theory -> Proof.state
    4.52 -  val instance_class_cmd: string * string -> theory -> Proof.state
    4.53 -  val instance_sort: class * sort -> theory -> Proof.state
    4.54 -  val instance_sort_cmd: string * string -> theory -> Proof.state
    4.55 -  val prove_instance_sort: tactic -> class * sort -> theory -> theory
    4.56 -
    4.57 -  val print_classes: theory -> unit
    4.58  end;
    4.59  
    4.60  structure Class : CLASS =
    4.61 @@ -60,20 +59,55 @@
    4.62      val mx_local = if is_loc then mx else NoSyn;
    4.63    in (mx_global, mx_local) end;
    4.64  
    4.65 +fun prove_interpretation tac prfx_atts expr insts =
    4.66 +  Locale.interpretation_i I prfx_atts expr insts
    4.67 +  #> Proof.global_terminal_proof
    4.68 +      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
    4.69 +  #> ProofContext.theory_of;
    4.70 +
    4.71 +fun prove_interpretation_in tac after_qed (name, expr) =
    4.72 +  Locale.interpretation_in_locale
    4.73 +      (ProofContext.theory after_qed) (name, expr)
    4.74 +  #> Proof.global_terminal_proof
    4.75 +      (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
    4.76 +  #> ProofContext.theory_of;
    4.77 +
    4.78 +fun OF_LAST thm1 thm2 =
    4.79 +  let
    4.80 +    val n = (length o Logic.strip_imp_prems o prop_of) thm2;
    4.81 +  in (thm1 RSN (n, thm2)) end;
    4.82 +
    4.83 +fun strip_all_ofclass thy sort =
    4.84 +  let
    4.85 +    val typ = TVar ((AxClass.param_tyvarname, 0), sort);
    4.86 +    fun prem_inclass t =
    4.87 +      case Logic.strip_imp_prems t
    4.88 +       of ofcls :: _ => try Logic.dest_inclass ofcls
    4.89 +        | [] => NONE;
    4.90 +    fun strip_ofclass class thm =
    4.91 +      thm OF (fst o AxClass.of_sort thy (typ, [class])) AxClass.cache;
    4.92 +    fun strip thm = case (prem_inclass o Thm.prop_of) thm
    4.93 +     of SOME (_, class) => thm |> strip_ofclass class |> strip
    4.94 +      | NONE => thm;
    4.95 +  in strip end;
    4.96 +
    4.97 +
    4.98 +(** axclass command **)
    4.99 +
   4.100  fun axclass_cmd (class, raw_superclasses) raw_specs thy =
   4.101    let
   4.102      val ctxt = ProofContext.init thy;
   4.103      val superclasses = map (Sign.read_class thy) raw_superclasses;
   4.104 -    val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst) raw_specs;
   4.105 -    val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd) raw_specs)
   4.106 +    val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst)
   4.107 +      raw_specs;
   4.108 +    val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd)
   4.109 +          raw_specs)
   4.110        |> snd
   4.111        |> (map o map) fst;
   4.112 -  in AxClass.define_class (class, superclasses) [] (name_atts ~~ axiomss) thy end;
   4.113 -
   4.114 -
   4.115 -(** axclasses with implicit parameter handling **)
   4.116 -
   4.117 -(* axclass instances *)
   4.118 +  in
   4.119 +    AxClass.define_class (class, superclasses) []
   4.120 +      (name_atts ~~ axiomss) thy
   4.121 +  end;
   4.122  
   4.123  local
   4.124  
   4.125 @@ -84,54 +118,25 @@
   4.126    in
   4.127      thy
   4.128      |> ProofContext.init
   4.129 -    |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])]) o maps (mk_prop thy)) insts)
   4.130 +    |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])])
   4.131 +        o maps (mk_prop thy)) insts)
   4.132    end;
   4.133  
   4.134  in
   4.135  
   4.136 -val axclass_instance_arity =
   4.137 +val instance_arity =
   4.138    gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity;
   4.139 -val axclass_instance_sort =
   4.140 +val classrel =
   4.141    gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel))
   4.142      AxClass.add_classrel I o single;
   4.143 +val classrel_cmd =
   4.144 +  gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel))
   4.145 +    AxClass.add_classrel I o single;
   4.146  
   4.147  end; (*local*)
   4.148  
   4.149  
   4.150 -(* introducing axclasses with implicit parameter handling *)
   4.151 -
   4.152 -fun axclass_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy =
   4.153 -  let
   4.154 -    val superclasses = map (Sign.certify_class thy) raw_superclasses;
   4.155 -    val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts;
   4.156 -    val prefix = Logic.const_of_class name;
   4.157 -    fun mk_const_name c = NameSpace.map_base (NameSpace.append prefix)
   4.158 -      (Sign.full_name thy c);
   4.159 -    fun add_const ((c, ty), syn) =
   4.160 -      Sign.add_consts_authentic [(c, ty, syn)]
   4.161 -      #> pair (mk_const_name c, ty);
   4.162 -    fun mk_axioms cs thy =
   4.163 -      raw_dep_axioms thy cs
   4.164 -      |> (map o apsnd o map) (Sign.cert_prop thy)
   4.165 -      |> rpair thy;
   4.166 -    fun add_constraint class (c, ty) =
   4.167 -      Sign.add_const_constraint_i (c, SOME
   4.168 -        (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
   4.169 -  in
   4.170 -    thy
   4.171 -    |> Theory.add_path prefix
   4.172 -    |> fold_map add_const consts
   4.173 -    ||> Theory.restore_naming thy
   4.174 -    |-> (fn cs => mk_axioms cs
   4.175 -    #-> (fn axioms_prop => AxClass.define_class (name, superclasses)
   4.176 -           (map fst cs @ other_consts) axioms_prop
   4.177 -    #-> (fn class => `(fn thy => AxClass.get_definition thy class)
   4.178 -    #-> (fn {intro, axioms, ...} => fold (add_constraint class) cs
   4.179 -    #> pair (class, ((intro, (map Thm.prop_of axioms, axioms)), cs))))))
   4.180 -  end;
   4.181 -
   4.182 -
   4.183 -(* explicit constants for overloaded definitions *)
   4.184 +(** explicit constants for overloaded definitions **)
   4.185  
   4.186  structure InstData = TheoryDataFun
   4.187  (
   4.188 @@ -146,22 +151,22 @@
   4.189        Symtab.merge (K true) (tabb1, tabb2));
   4.190  );
   4.191  
   4.192 -fun inst_thms f thy =
   4.193 -  (Symtab.fold (Symtab.fold (cons o f o snd o snd) o snd) o fst) (InstData.get thy) [];
   4.194 -fun add_inst (c, tyco) inst = (InstData.map o apfst o Symtab.map_default (c, Symtab.empty))
   4.195 -  (Symtab.update_new (tyco, inst))
   4.196 +fun inst_thms f thy = (Symtab.fold (Symtab.fold (cons o f o snd o snd) o snd) o fst)
   4.197 +    (InstData.get thy) [];
   4.198 +fun add_inst (c, tyco) inst = (InstData.map o apfst
   4.199 +      o Symtab.map_default (c, Symtab.empty)) (Symtab.update_new (tyco, inst))
   4.200    #> (InstData.map o apsnd) (Symtab.update_new (fst inst, (c, tyco)));
   4.201  
   4.202 -fun unoverload thy thm = MetaSimplifier.rewrite false (inst_thms I thy) thm;
   4.203 -fun overload thy thm = MetaSimplifier.rewrite false (inst_thms symmetric thy) thm;
   4.204 +fun unoverload thy = MetaSimplifier.rewrite false (inst_thms I thy);
   4.205 +fun overload thy = MetaSimplifier.rewrite false (inst_thms symmetric thy);
   4.206  
   4.207  fun inst_const thy (c, tyco) =
   4.208    (fst o the o Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c)) tyco;
   4.209  fun unoverload_const thy (c_ty as (c, _)) =
   4.210    case AxClass.class_of_param thy c
   4.211     of SOME class => (case Sign.const_typargs thy c_ty
   4.212 -       of [Type (tyco, _)] =>
   4.213 -            (case Symtab.lookup ((the o Symtab.lookup (fst (InstData.get thy))) c) tyco
   4.214 +       of [Type (tyco, _)] => (case Symtab.lookup
   4.215 +           ((the o Symtab.lookup (fst (InstData.get thy))) c) tyco
   4.216               of SOME (c, _) => c
   4.217                | NONE => c)
   4.218          | [_] => c)
   4.219 @@ -192,7 +197,8 @@
   4.220  
   4.221  fun add_def ((class, tyco), ((name, prop), atts)) thy =
   4.222    let
   4.223 -    val ((lhs as Const (c, ty), args), rhs) = (apfst Term.strip_comb o Logic.dest_equals) prop;
   4.224 +    val ((lhs as Const (c, ty), args), rhs) =
   4.225 +      (apfst Term.strip_comb o Logic.dest_equals) prop;
   4.226      fun add_inst' def ([], (Const (c_inst, ty))) =
   4.227            if forall (fn TFree _ => true | _ => false) (Sign.const_typargs thy (c_inst, ty))
   4.228            then add_inst (c, tyco) (c_inst, def)
   4.229 @@ -205,7 +211,7 @@
   4.230    end;
   4.231  
   4.232  
   4.233 -(* instances with implicit parameter handling *)
   4.234 +(** instances with implicit parameter handling **)
   4.235  
   4.236  local
   4.237  
   4.238 @@ -223,7 +229,7 @@
   4.239  fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Theory.read_axm;
   4.240  fun read_def thy = gen_read_def thy (K I) (K I);
   4.241  
   4.242 -fun gen_instance_arity prep_arity read_def do_proof raw_arities raw_defs after_qed theory =
   4.243 +fun gen_instance prep_arity read_def do_proof raw_arities raw_defs after_qed theory =
   4.244    let
   4.245      val arities = map (prep_arity theory) raw_arities;
   4.246      val _ = if null arities then error "at least one arity must be given" else ();
   4.247 @@ -231,7 +237,8 @@
   4.248       of [] => ()
   4.249        | dupl_tycos => error ("type constructors occur more than once in arities: "
   4.250            ^ (commas o map quote) dupl_tycos);
   4.251 -    val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra o Sign.classes_of) theory
   4.252 +    val super_sort =
   4.253 +      (Graph.all_succs o #classes o Sorts.rep_algebra o Sign.classes_of) theory;
   4.254      fun get_consts_class tyco ty class =
   4.255        let
   4.256          val cs = (these o Option.map snd o try (AxClass.params_of_class theory)) class;
   4.257 @@ -241,7 +248,8 @@
   4.258        end;
   4.259      fun get_consts_sort (tyco, asorts, sort) =
   4.260        let
   4.261 -        val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) (Name.names Name.context "'a" asorts))
   4.262 +        val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort))
   4.263 +          (Name.names Name.context "'a" asorts))
   4.264        in maps (get_consts_class tyco ty) (super_sort sort) end;
   4.265      val cs = maps get_consts_sort arities;
   4.266      fun mk_typnorm thy (ty, ty_sc) =
   4.267 @@ -288,8 +296,6 @@
   4.268      |-> (fn (cs, defs) => do_proof (after_qed' cs defs) arities defs)
   4.269    end;
   4.270  
   4.271 -fun instance_arity_cmd' do_proof = gen_instance_arity Sign.read_arity read_def_cmd do_proof;
   4.272 -fun instance_arity' do_proof = gen_instance_arity Sign.cert_arity read_def do_proof;
   4.273  fun tactic_proof tac f arities defs =
   4.274    fold (fn arity => AxClass.prove_arity arity tac) arities
   4.275    #> f
   4.276 @@ -297,26 +303,27 @@
   4.277  
   4.278  in
   4.279  
   4.280 -val instance_arity_cmd = instance_arity_cmd'
   4.281 -  (fn f => fn arities => fn defs => axclass_instance_arity f arities);
   4.282 -val instance_arity = instance_arity'
   4.283 -  (fn f => fn arities => fn defs => axclass_instance_arity f arities);
   4.284 -fun prove_instance_arity tac arities defs =
   4.285 -  instance_arity' (tactic_proof tac) arities defs (K I);
   4.286 +val instance = gen_instance Sign.cert_arity read_def
   4.287 +  (fn f => fn arities => fn defs => instance_arity f arities);
   4.288 +val instance_cmd = gen_instance Sign.read_arity read_def_cmd
   4.289 +  (fn f => fn arities => fn defs => instance_arity f arities);
   4.290 +fun prove_instance tac arities defs =
   4.291 +  gen_instance Sign.cert_arity read_def
   4.292 +    (tactic_proof tac) arities defs (K I);
   4.293  
   4.294  end; (*local*)
   4.295  
   4.296  
   4.297  
   4.298 -(** combining locales and axclasses **)
   4.299 -
   4.300 -(* theory data *)
   4.301 +(** class data **)
   4.302  
   4.303  datatype class_data = ClassData of {
   4.304    locale: string,
   4.305    consts: (string * string) list
   4.306      (*locale parameter ~> toplevel theory constant*),
   4.307    v: string option,
   4.308 +  inst: typ Symtab.table * term Symtab.table
   4.309 +    (*canonical interpretation*),
   4.310    intro: thm
   4.311  } * thm list (*derived defs*);
   4.312  
   4.313 @@ -336,13 +343,13 @@
   4.314  
   4.315  (* queries *)
   4.316  
   4.317 -val lookup_class_data = Option.map rep_classdata oo try o Graph.get_node o fst o ClassData.get;
   4.318 +val lookup_class_data = Option.map rep_classdata oo try o Graph.get_node
   4.319 +  o fst o ClassData.get;
   4.320  fun class_of_locale thy = Symtab.lookup ((snd o ClassData.get) thy);
   4.321  
   4.322 -fun the_class_data thy class =
   4.323 -  case lookup_class_data thy class
   4.324 -    of NONE => error ("undeclared class " ^ quote class)
   4.325 -     | SOME data => data;
   4.326 +fun the_class_data thy class = case lookup_class_data thy class
   4.327 + of NONE => error ("undeclared class " ^ quote class)
   4.328 +  | SOME data => data;
   4.329  
   4.330  val ancestry = Graph.all_succs o fst o ClassData.get;
   4.331  
   4.332 @@ -391,18 +398,18 @@
   4.333        ]
   4.334      ]
   4.335    in
   4.336 -    (Pretty.writeln o Pretty.chunks o separate (Pretty.str "") o map mk_entry o Sorts.all_classes)
   4.337 -      algebra
   4.338 +    (Pretty.writeln o Pretty.chunks o separate (Pretty.str "")
   4.339 +      o map mk_entry o Sorts.all_classes) algebra
   4.340    end;
   4.341  
   4.342  
   4.343  (* updaters *)
   4.344  
   4.345 -fun add_class_data ((class, superclasses), (locale, consts, v, intro)) =
   4.346 +fun add_class_data ((class, superclasses), (locale, consts, v, inst, intro)) =
   4.347    ClassData.map (fn (gr, tab) => (
   4.348      gr
   4.349      |> Graph.new_node (class, ClassData ({ locale = locale, consts = consts,
   4.350 -         v = v, intro = intro }, []))
   4.351 +         v = v, inst = inst, intro = intro }, []))
   4.352      |> fold (curry Graph.add_edge class) superclasses,
   4.353      tab
   4.354      |> Symtab.update (locale, class)
   4.355 @@ -411,7 +418,65 @@
   4.356  fun add_class_const_thm (class, thm) = (ClassData.map o apfst o Graph.map_node class)
   4.357    (fn ClassData (data, thms) => ClassData (data, thm :: thms));
   4.358  
   4.359 -(* tactics and methods *)
   4.360 +
   4.361 +(** rule calculation, tactics and methods **)
   4.362 +
   4.363 +fun class_intro thy locale class sups =
   4.364 +  let
   4.365 +    fun class_elim class =
   4.366 +      case (map Drule.unconstrainTs o #axioms o AxClass.get_definition thy) class
   4.367 +       of [thm] => SOME thm
   4.368 +        | [] => NONE;
   4.369 +    val pred_intro = case Locale.intros thy locale
   4.370 +     of ([ax_intro], [intro]) => intro |> OF_LAST ax_intro |> SOME
   4.371 +      | ([intro], []) => SOME intro
   4.372 +      | ([], [intro]) => SOME intro
   4.373 +      | _ => NONE;
   4.374 +    val pred_intro' = pred_intro
   4.375 +      |> Option.map (fn intro => intro OF map_filter class_elim sups);
   4.376 +    val class_intro = (#intro o AxClass.get_definition thy) class;
   4.377 +    val raw_intro = case pred_intro'
   4.378 +     of SOME pred_intro => class_intro |> OF_LAST pred_intro
   4.379 +      | NONE => class_intro;
   4.380 +    val sort = Sign.super_classes thy class;
   4.381 +    val typ = TVar ((AxClass.param_tyvarname, 0), sort);
   4.382 +    val defs = these_defs thy sups;
   4.383 +  in
   4.384 +    raw_intro
   4.385 +    |> Drule.instantiate' [SOME (Thm.ctyp_of thy typ)] []
   4.386 +    |> strip_all_ofclass thy sort
   4.387 +    |> Thm.strip_shyps
   4.388 +    |> MetaSimplifier.rewrite_rule defs
   4.389 +    |> Drule.unconstrainTs
   4.390 +  end;
   4.391 +
   4.392 +fun class_interpretation class facts defs thy =
   4.393 +  let
   4.394 +    val ({ locale, inst, ... }, _) = the_class_data thy class;
   4.395 +    val tac = (ALLGOALS o ProofContext.fact_tac) facts;
   4.396 +    val prfx = Logic.const_of_class (NameSpace.base class);
   4.397 +  in
   4.398 +    prove_interpretation tac ((false, prfx), []) (Locale.Locale locale)
   4.399 +      (inst, defs) thy
   4.400 +  end;
   4.401 +
   4.402 +fun interpretation_in_rule thy (class1, class2) =
   4.403 +  let
   4.404 +    fun mk_axioms class =
   4.405 +      let
   4.406 +        val ({ locale, inst = (_, insttab), ... }, _) = the_class_data thy class;
   4.407 +      in
   4.408 +        Locale.global_asms_of thy locale
   4.409 +        |> maps snd
   4.410 +        |> (map o map_aterms) (fn Free (s, _) => (the o Symtab.lookup insttab) s | t => t)
   4.411 +        |> (map o map_types o map_atyps) (fn TFree _ => TFree ("'a", [class1]) | T => T)
   4.412 +        |> map (ObjectLogic.ensure_propT thy)
   4.413 +      end;
   4.414 +    val (prems, concls) = pairself mk_axioms (class1, class2);
   4.415 +  in
   4.416 +    Goal.prove_global thy [] prems (Logic.mk_conjunction_list concls)
   4.417 +      (Locale.intro_locales_tac true (ProofContext.init thy))
   4.418 +  end;
   4.419  
   4.420  fun intro_classes_tac facts st =
   4.421    let
   4.422 @@ -443,102 +508,9 @@
   4.423      "apply some intro/elim rule")]);
   4.424  
   4.425  
   4.426 -(* tactical interfaces to locale commands *)
   4.427 -
   4.428 -fun prove_interpretation tac prfx_atts expr insts thy =
   4.429 -  thy
   4.430 -  |> Locale.interpretation_i I prfx_atts expr insts
   4.431 -  |> Proof.global_terminal_proof (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
   4.432 -  |> ProofContext.theory_of;
   4.433 -
   4.434 -fun prove_interpretation_in tac after_qed (name, expr) thy =
   4.435 -  thy
   4.436 -  |> Locale.interpretation_in_locale (ProofContext.theory after_qed) (name, expr)
   4.437 -  |> Proof.global_terminal_proof (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
   4.438 -  |> ProofContext.theory_of;
   4.439 -
   4.440 -
   4.441 -(* constructing class introduction and other rules from axclass and locale rules *)
   4.442 -
   4.443 -fun mk_instT class = Symtab.empty
   4.444 -  |> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class]));
   4.445 -
   4.446 -fun mk_inst class param_names cs =
   4.447 -  Symtab.empty
   4.448 -  |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
   4.449 -       (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;
   4.450 -
   4.451 -fun OF_LAST thm1 thm2 =
   4.452 -  let
   4.453 -    val n = (length o Logic.strip_imp_prems o prop_of) thm2;
   4.454 -  in (thm1 RSN (n, thm2)) end;
   4.455 -
   4.456 -fun strip_all_ofclass thy sort =
   4.457 -  let
   4.458 -    val typ = TVar ((AxClass.param_tyvarname, 0), sort);
   4.459 -    fun prem_inclass t =
   4.460 -      case Logic.strip_imp_prems t
   4.461 -       of ofcls :: _ => try Logic.dest_inclass ofcls
   4.462 -        | [] => NONE;
   4.463 -    fun strip_ofclass class thm =
   4.464 -      thm OF (fst o AxClass.of_sort thy (typ, [class])) AxClass.cache;
   4.465 -    fun strip thm = case (prem_inclass o Thm.prop_of) thm
   4.466 -     of SOME (_, class) => thm |> strip_ofclass class |> strip
   4.467 -      | NONE => thm;
   4.468 -  in strip end;
   4.469 +(** classes and class target **)
   4.470  
   4.471 -fun class_intro thy locale class sups =
   4.472 -  let
   4.473 -    fun class_elim class =
   4.474 -      case (map Drule.unconstrainTs o #axioms o AxClass.get_definition thy) class
   4.475 -       of [thm] => SOME thm
   4.476 -        | [] => NONE;
   4.477 -    val pred_intro = case Locale.intros thy locale
   4.478 -     of ([ax_intro], [intro]) => intro |> OF_LAST ax_intro |> SOME
   4.479 -      | ([intro], []) => SOME intro
   4.480 -      | ([], [intro]) => SOME intro
   4.481 -      | _ => NONE;
   4.482 -    val pred_intro' = pred_intro
   4.483 -      |> Option.map (fn intro => intro OF map_filter class_elim sups);
   4.484 -    val class_intro = (#intro o AxClass.get_definition thy) class;
   4.485 -    val raw_intro = case pred_intro'
   4.486 -     of SOME pred_intro => class_intro |> OF_LAST pred_intro
   4.487 -      | NONE => class_intro;
   4.488 -    val sort = Sign.super_classes thy class;
   4.489 -    val typ = TVar ((AxClass.param_tyvarname, 0), sort);
   4.490 -    val defs = these_defs thy sups;
   4.491 -  in
   4.492 -    raw_intro
   4.493 -    |> Drule.instantiate' [SOME (Thm.ctyp_of thy typ)] []
   4.494 -    |> strip_all_ofclass thy sort
   4.495 -    |> Thm.strip_shyps
   4.496 -    |> MetaSimplifier.rewrite_rule defs
   4.497 -    |> Drule.unconstrainTs
   4.498 -  end;
   4.499 -
   4.500 -fun interpretation_in_rule thy (class1, class2) =
   4.501 -  let
   4.502 -    val (params, consts) = split_list (params_of_sort thy [class1]);
   4.503 -    (*FIXME also remember this at add_class*)
   4.504 -    fun mk_axioms class =
   4.505 -      let
   4.506 -        val name_locale = (#locale o fst o the_class_data thy) class;
   4.507 -        val inst = mk_inst class params consts;
   4.508 -      in
   4.509 -        Locale.global_asms_of thy name_locale
   4.510 -        |> maps snd
   4.511 -        |> (map o map_aterms) (fn Free (s, _) => (the o Symtab.lookup inst) s | t => t)
   4.512 -        |> (map o map_types o map_atyps) (fn TFree _ => TFree ("'a", [class1]) | T => T)
   4.513 -        |> map (ObjectLogic.ensure_propT thy)
   4.514 -      end;
   4.515 -    val (prems, concls) = pairself mk_axioms (class1, class2);
   4.516 -  in
   4.517 -    Goal.prove_global thy [] prems (Logic.mk_conjunction_list concls)
   4.518 -      (Locale.intro_locales_tac true (ProofContext.init thy))
   4.519 -  end;
   4.520 -
   4.521 -
   4.522 -(* classes *)
   4.523 +(* class definition *)
   4.524  
   4.525  local
   4.526  
   4.527 @@ -553,11 +525,18 @@
   4.528  fun gen_class add_locale prep_class prep_param bname
   4.529      raw_supclasses raw_elems raw_other_consts thy =
   4.530    let
   4.531 +    fun mk_instT class = Symtab.empty
   4.532 +      |> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class]));
   4.533 +    fun mk_inst class param_names cs =
   4.534 +      Symtab.empty
   4.535 +      |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
   4.536 +           (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;
   4.537      (*FIXME need proper concept for reading locale statements*)
   4.538      fun subst_classtyvar (_, _) =
   4.539            TFree (AxClass.param_tyvarname, [])
   4.540        | subst_classtyvar (v, sort) =
   4.541 -          error ("Sort constraint illegal in type class, for type variable " ^ v ^ "::" ^ Sign.string_of_sort thy sort);
   4.542 +          error ("Sort constraint illegal in type class, for type variable "
   4.543 +            ^ v ^ "::" ^ Sign.string_of_sort thy sort);
   4.544      (*val subst_classtyvars = Element.map_ctxt {name = I, var = I, term = I,
   4.545        typ = Term.map_type_tfree subst_classtyvar, fact = I, attrib = I};*)
   4.546      val other_consts = map (prep_param thy) raw_other_consts;
   4.547 @@ -602,7 +581,7 @@
   4.548          val super_defs = these_defs thy sups;
   4.549          fun prep_asm ((name, atts), ts) =
   4.550            ((NameSpace.base name, map (Attrib.attribute thy) atts),
   4.551 -            (map o map_aterms) ((*MetaSimplifier.rewrite_term thy super_defs [] o *)subst) ts);
   4.552 +            (map o map_aterms) subst ts);
   4.553        in
   4.554          Locale.global_asms_of thy name_locale
   4.555          |> map prep_asm
   4.556 @@ -617,21 +596,17 @@
   4.557      |-> (fn name_locale => ProofContext.theory_result (
   4.558        `(fn thy => extract_params thy name_locale)
   4.559        #-> (fn (v, (param_names, params)) =>
   4.560 -        axclass_params (bname, supsort) params (extract_assumes name_locale params) other_consts
   4.561 -      #-> (fn (name_axclass, ((_, (ax_terms, ax_axioms)), consts)) =>
   4.562 +        AxClass.define_class_params (bname, supsort) params
   4.563 +          (extract_assumes name_locale params) other_consts
   4.564 +      #-> (fn (name_axclass, (consts, axioms)) =>
   4.565          `(fn thy => class_intro thy name_locale name_axclass sups)
   4.566        #-> (fn class_intro =>
   4.567          add_class_data ((name_axclass, sups),
   4.568            (name_locale, map (fst o fst) params ~~ map fst consts, v,
   4.569 -            class_intro))
   4.570 -        (*FIXME: class_data should already contain data relevant
   4.571 -          for interpretation; use this later for class target*)
   4.572 -        (*FIXME: general export_fixes which may be parametrized
   4.573 -          with pieces of an emerging class*)
   4.574 +            (mk_instT name_axclass, mk_inst name_axclass param_names
   4.575 +              (map snd supconsts @ consts)), class_intro))
   4.576        #> note_intro name_axclass class_intro
   4.577 -      #> prove_interpretation ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
   4.578 -          ((false, Logic.const_of_class bname), []) (Locale.Locale name_locale)
   4.579 -          ((mk_instT name_axclass, mk_inst name_axclass param_names (map snd supconsts @ consts)), [])
   4.580 +      #> class_interpretation name_axclass axioms []
   4.581        #> pair name_axclass
   4.582        )))))
   4.583    end;
   4.584 @@ -643,73 +618,8 @@
   4.585  
   4.586  end; (*local*)
   4.587  
   4.588 -local
   4.589  
   4.590 -fun instance_subclass (class1, class2) thy  =
   4.591 -  let
   4.592 -    val interp = interpretation_in_rule thy (class1, class2);
   4.593 -    val ax = #axioms (AxClass.get_definition thy class1);
   4.594 -    val intro = #intro (AxClass.get_definition thy class2)
   4.595 -      |> Drule.instantiate' [SOME (Thm.ctyp_of thy
   4.596 -          (TVar ((AxClass.param_tyvarname, 0), [class1])))] [];
   4.597 -    val thm = 
   4.598 -      intro
   4.599 -      |> OF_LAST (interp OF ax)
   4.600 -      |> strip_all_ofclass thy (Sign.super_classes thy class2);
   4.601 -  in
   4.602 -    thy |> AxClass.add_classrel thm
   4.603 -  end;
   4.604 -
   4.605 -fun instance_subsort (class, sort) thy =
   4.606 -  let
   4.607 -    val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra
   4.608 -      o Sign.classes_of) thy sort;
   4.609 -    val classes = filter_out (fn class' => Sign.subsort thy ([class], [class']))
   4.610 -      (rev super_sort);
   4.611 -  in
   4.612 -    thy |> fold (curry instance_subclass class) classes
   4.613 -  end;
   4.614 -
   4.615 -fun instance_sort' do_proof (class, sort) theory =
   4.616 -  let
   4.617 -    val loc_name = (#locale o fst o the_class_data theory) class;
   4.618 -    val loc_expr =
   4.619 -      (Locale.Merge o map (Locale.Locale o #locale o fst o the_class_data theory)) sort;
   4.620 -  in
   4.621 -    theory
   4.622 -    |> do_proof (instance_subsort (class, sort)) (loc_name, loc_expr)
   4.623 -  end;
   4.624 -
   4.625 -fun gen_instance_sort prep_class prep_sort (raw_class, raw_sort) theory =
   4.626 -  let
   4.627 -    val class = prep_class theory raw_class;
   4.628 -    val sort = prep_sort theory raw_sort;
   4.629 -  in
   4.630 -    theory
   4.631 -    |> instance_sort' (Locale.interpretation_in_locale o ProofContext.theory) (class, sort)
   4.632 -  end;
   4.633 -
   4.634 -fun gen_instance_class prep_class (raw_class, raw_superclass) theory =
   4.635 -  let
   4.636 -    val class = prep_class theory raw_class;
   4.637 -    val superclass = prep_class theory raw_superclass;
   4.638 -  in
   4.639 -    theory
   4.640 -    |> axclass_instance_sort (class, superclass)
   4.641 -  end;
   4.642 -
   4.643 -in
   4.644 -
   4.645 -val instance_sort_cmd = gen_instance_sort Sign.read_class Syntax.global_read_sort;
   4.646 -val instance_sort = gen_instance_sort Sign.certify_class Sign.certify_sort;
   4.647 -val prove_instance_sort = instance_sort' o prove_interpretation_in;
   4.648 -val instance_class_cmd = gen_instance_class Sign.read_class;
   4.649 -val instance_class = gen_instance_class Sign.certify_class;
   4.650 -
   4.651 -end; (*local*)
   4.652 -
   4.653 -
   4.654 -(** class target **)
   4.655 +(* definition in class target *)
   4.656  
   4.657  fun export_fixes thy class =
   4.658    let
   4.659 @@ -740,14 +650,10 @@
   4.660      val (syn', _) = fork_mixfix true NONE syn;
   4.661      fun interpret def =
   4.662        let
   4.663 -        val def' = symmetric def
   4.664 -        val tac = (ALLGOALS o ProofContext.fact_tac) [def'];
   4.665 -        val name_locale = (#locale o fst o the_class_data thy) class;
   4.666 +        val def' = symmetric def;
   4.667          val def_eq = Thm.prop_of def';
   4.668 -        val (params, consts) = split_list (params_of_sort thy [class]);
   4.669        in
   4.670 -        prove_interpretation tac ((false, prfx), []) (Locale.Locale name_locale)
   4.671 -          ((mk_instT class, mk_inst class params consts), [def_eq])
   4.672 +        class_interpretation class [def'] [def_eq]
   4.673          #> add_class_const_thm (class, def')
   4.674        end;
   4.675    in
   4.676 @@ -762,4 +668,53 @@
   4.677      |> Sign.restore_naming thy
   4.678    end;
   4.679  
   4.680 +
   4.681 +(* interpretation in class target *)
   4.682 +
   4.683 +local
   4.684 +
   4.685 +fun gen_interpretation_in_class prep_class do_proof (raw_class, raw_superclass) theory =
   4.686 +  let
   4.687 +    val class = prep_class theory raw_class;
   4.688 +    val superclass = prep_class theory raw_superclass;
   4.689 +    val loc_name = (#locale o fst o the_class_data theory) class;
   4.690 +    val loc_expr = (Locale.Locale o #locale o fst o the_class_data theory) superclass;
   4.691 +    fun prove_classrel (class, superclass) thy =
   4.692 +      let
   4.693 +        val classes = (Graph.all_succs o #classes o Sorts.rep_algebra
   4.694 +              o Sign.classes_of) thy [superclass]
   4.695 +          |> filter_out (fn class' => Sign.subsort thy ([class], [class']));
   4.696 +        fun instance_subclass (class1, class2) thy  =
   4.697 +          let
   4.698 +            val interp = interpretation_in_rule thy (class1, class2);
   4.699 +            val ax = #axioms (AxClass.get_definition thy class1);
   4.700 +            val intro = #intro (AxClass.get_definition thy class2)
   4.701 +              |> Drule.instantiate' [SOME (Thm.ctyp_of thy
   4.702 +                  (TVar ((AxClass.param_tyvarname, 0), [class1])))] [];
   4.703 +            val thm = 
   4.704 +              intro
   4.705 +              |> OF_LAST (interp OF ax)
   4.706 +              |> strip_all_ofclass thy (Sign.super_classes thy class2);
   4.707 +          in
   4.708 +            thy |> AxClass.add_classrel thm
   4.709 +          end;
   4.710 +      in
   4.711 +        thy |> fold_rev (curry instance_subclass class) classes
   4.712 +      end;
   4.713 +  in
   4.714 +    theory
   4.715 +    |> do_proof (prove_classrel (class, superclass)) (loc_name, loc_expr)
   4.716 +  end;
   4.717 +
   4.718 +in
   4.719 +
   4.720 +val interpretation_in_class = gen_interpretation_in_class Sign.certify_class
   4.721 +  (Locale.interpretation_in_locale o ProofContext.theory);
   4.722 +val interpretation_in_class_cmd = gen_interpretation_in_class Sign.read_class
   4.723 +  (Locale.interpretation_in_locale o ProofContext.theory);
   4.724 +val prove_interpretation_in_class = gen_interpretation_in_class Sign.certify_class
   4.725 +  o prove_interpretation_in;
   4.726 +
   4.727 +end; (*local*)
   4.728 +
   4.729  end;
     5.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Sep 15 19:27:43 2007 +0200
     5.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Sep 15 19:27:44 2007 +0200
     5.3 @@ -427,13 +427,24 @@
     5.4  val instanceP =
     5.5    OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal ((
     5.6        P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
     5.7 -           >> Class.instance_class_cmd
     5.8 +           >> Class.classrel_cmd
     5.9        || P.$$$ "advanced" |-- P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname)
    5.10 -           >> Class.instance_sort_cmd
    5.11 +           >> Class.interpretation_in_class_cmd
    5.12        || P.and_list1 P.arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop)
    5.13 -           >> (fn (arities, defs) => Class.instance_arity_cmd arities defs (fold (Code.add_func false)))
    5.14 +           >> (fn (arities, defs) => Class.instance_cmd arities defs (fold (Code.add_func false)))
    5.15      ) >> (Toplevel.print oo Toplevel.theory_to_proof));
    5.16  
    5.17 +val instantiationP =
    5.18 +  OuterSyntax.command "instantiation" "prove type arity" K.thy_decl (
    5.19 +      P.and_list1 P.arity -- P.opt_begin
    5.20 +           >> (fn (arities, begin) => (begin ? Toplevel.print)
    5.21 +            o Toplevel.begin_local_theory begin
    5.22 +                (Instance.begin_instantiation_cmd arities)));
    5.23 +
    5.24 +val instance_proofP =
    5.25 +  OuterSyntax.command "instance_proof" "prove type arity relation" K.thy_goal
    5.26 +      (Scan.succeed ((Toplevel.print oo Toplevel.local_theory_to_proof NONE) Instance.proof_instantiation));
    5.27 +
    5.28  end;
    5.29  
    5.30  
    5.31 @@ -993,7 +1004,7 @@
    5.32    simproc_setupP, parse_ast_translationP, parse_translationP,
    5.33    print_translationP, typed_print_translationP,
    5.34    print_ast_translationP, token_translationP, oracleP, contextP,
    5.35 -  localeP, classP, instanceP, code_datatypeP,
    5.36 +  localeP, classP, instanceP, instantiationP, instance_proofP, code_datatypeP,
    5.37    (*proof commands*)
    5.38    theoremP, lemmaP, corollaryP, haveP, henceP, showP, thusP, fixP,
    5.39    assumeP, presumeP, defP, obtainP, guessP, letP, caseP, thenP, fromP,
     6.1 --- a/src/Pure/axclass.ML	Sat Sep 15 19:27:43 2007 +0200
     6.2 +++ b/src/Pure/axclass.ML	Sat Sep 15 19:27:44 2007 +0200
     6.3 @@ -8,6 +8,16 @@
     6.4  
     6.5  signature AX_CLASS =
     6.6  sig
     6.7 +  val define_class: bstring * class list -> string list ->
     6.8 +    ((bstring * attribute list) * term list) list -> theory -> class * theory
     6.9 +  val define_class_params: bstring * class list -> ((bstring * typ) * mixfix) list ->
    6.10 +    (theory -> (string * typ) list -> ((bstring * attribute list) * term list) list) ->
    6.11 +    string list -> theory ->
    6.12 +    (class * ((string * typ) list * thm list)) * theory
    6.13 +  val add_classrel: thm -> theory -> theory
    6.14 +  val add_arity: thm -> theory -> theory
    6.15 +  val prove_classrel: class * class -> tactic -> theory -> theory
    6.16 +  val prove_arity: string * sort list * sort -> tactic -> theory -> theory
    6.17    val get_definition: theory -> class -> {def: thm, intro: thm, axioms: thm list,
    6.18      params: (string * typ) list}
    6.19    val class_intros: theory -> thm list
    6.20 @@ -17,12 +27,6 @@
    6.21    val print_axclasses: theory -> unit
    6.22    val cert_classrel: theory -> class * class -> class * class
    6.23    val read_classrel: theory -> xstring * xstring -> class * class
    6.24 -  val add_classrel: thm -> theory -> theory
    6.25 -  val add_arity: thm -> theory -> theory
    6.26 -  val prove_classrel: class * class -> tactic -> theory -> theory
    6.27 -  val prove_arity: string * sort list * sort -> tactic -> theory -> theory
    6.28 -  val define_class: bstring * class list -> string list ->
    6.29 -    ((bstring * attribute list) * term list) list -> theory -> class * theory
    6.30    val axiomatize_class: bstring * xstring list -> theory -> theory
    6.31    val axiomatize_class_i: bstring * class list -> theory -> theory
    6.32    val axiomatize_classrel: (xstring * xstring) list -> theory -> theory
    6.33 @@ -359,6 +363,40 @@
    6.34  
    6.35  
    6.36  
    6.37 +(** axclasses with implicit parameter handling **)
    6.38 +
    6.39 +fun define_class_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy =
    6.40 +  let
    6.41 +    val superclasses = map (Sign.certify_class thy) raw_superclasses;
    6.42 +    val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts;
    6.43 +    val prefix = Logic.const_of_class name;
    6.44 +    fun mk_const_name c = NameSpace.map_base (NameSpace.append prefix)
    6.45 +      (Sign.full_name thy c);
    6.46 +    fun add_const ((c, ty), syn) =
    6.47 +      Sign.add_consts_authentic [(c, ty, syn)]
    6.48 +      #> pair (mk_const_name c, ty);
    6.49 +    fun mk_axioms cs thy =
    6.50 +      raw_dep_axioms thy cs
    6.51 +      |> (map o apsnd o map) (Sign.cert_prop thy)
    6.52 +      |> rpair thy;
    6.53 +    fun add_constraint class (c, ty) =
    6.54 +      Sign.add_const_constraint_i (c, SOME
    6.55 +        (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
    6.56 +  in
    6.57 +    thy
    6.58 +    |> Theory.add_path prefix
    6.59 +    |> fold_map add_const consts
    6.60 +    ||> Theory.restore_naming thy
    6.61 +    |-> (fn cs => mk_axioms cs
    6.62 +    #-> (fn axioms_prop => define_class (name, superclasses)
    6.63 +           (map fst cs @ other_consts) axioms_prop
    6.64 +    #-> (fn class => `(fn thy => get_definition thy class)
    6.65 +    #-> (fn {axioms, ...} => fold (add_constraint class) cs
    6.66 +    #> pair (class, (cs, axioms))))))
    6.67 +  end;
    6.68 +
    6.69 +
    6.70 +
    6.71  (** axiomatizations **)
    6.72  
    6.73  local