ClassPackage renamed to Class
authorhaftmann
Fri Aug 10 17:04:24 2007 +0200 (2007-08-10)
changeset 24218fbf1646b267c
parent 24217 5c4913b478f5
child 24219 e558fe311376
ClassPackage renamed to Class
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_package.ML
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_package.ML
src/HOLCF/Tools/pcpodef_package.ML
src/Provers/classical.ML
src/Pure/Isar/class.ML
src/Pure/Isar/theory_target.ML
src/Pure/Tools/class_package.ML
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Fri Aug 10 17:04:20 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Fri Aug 10 17:04:24 2007 +0200
     1.3 @@ -409,14 +409,14 @@
     1.4             val cls_name = Sign.full_name thy' ("pt_"^ak_name);
     1.5             val at_inst  = PureThy.get_thm thy' (Name ("at_"^ak_name'^"_inst")); 
     1.6  
     1.7 -           val proof1 = EVERY [ClassPackage.intro_classes_tac [],
     1.8 +           val proof1 = EVERY [Class.intro_classes_tac [],
     1.9                                   rtac ((at_inst RS at_pt_inst) RS pt1) 1,
    1.10                                   rtac ((at_inst RS at_pt_inst) RS pt2) 1,
    1.11                                   rtac ((at_inst RS at_pt_inst) RS pt3) 1,
    1.12                                   atac 1];
    1.13             val simp_s = HOL_basic_ss addsimps 
    1.14                          PureThy.get_thmss thy' [Name (ak_name^"_prm_"^ak_name'^"_def")];  
    1.15 -           val proof2 = EVERY [ClassPackage.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
    1.16 +           val proof2 = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
    1.17  
    1.18           in
    1.19             thy'
    1.20 @@ -441,7 +441,7 @@
    1.21            val pt_inst  = PureThy.get_thm thy (Name ("pt_"^ak_name^"_inst"));
    1.22  
    1.23            fun pt_proof thm = 
    1.24 -              EVERY [ClassPackage.intro_classes_tac [],
    1.25 +              EVERY [Class.intro_classes_tac [],
    1.26                       rtac (thm RS pt1) 1, rtac (thm RS pt2) 1, rtac (thm RS pt3) 1, atac 1];
    1.27  
    1.28            val pt_thm_fun   = at_thm RS (pt_inst RS (pt_inst RS pt_fun_inst));
    1.29 @@ -488,12 +488,12 @@
    1.30                 (if ak_name = ak_name'
    1.31                  then
    1.32                    let val at_thm = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));
    1.33 -                  in  EVERY [ClassPackage.intro_classes_tac [],
    1.34 +                  in  EVERY [Class.intro_classes_tac [],
    1.35                               rtac ((at_thm RS fs_at_inst) RS fs1) 1] end
    1.36                  else
    1.37                    let val dj_inst = PureThy.get_thm thy' (Name ("dj_"^ak_name'^"_"^ak_name));
    1.38                        val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI];
    1.39 -                  in EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1] end)
    1.40 +                  in EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1] end)
    1.41          in
    1.42           AxClass.prove_arity (qu_name,[],[qu_class]) proof thy'
    1.43          end) ak_names thy) ak_names thy18;
    1.44 @@ -510,7 +510,7 @@
    1.45          let
    1.46            val cls_name = Sign.full_name thy ("fs_"^ak_name);
    1.47            val fs_inst  = PureThy.get_thm thy (Name ("fs_"^ak_name^"_inst"));
    1.48 -          fun fs_proof thm = EVERY [ClassPackage.intro_classes_tac [], rtac (thm RS fs1) 1];
    1.49 +          fun fs_proof thm = EVERY [Class.intro_classes_tac [], rtac (thm RS fs1) 1];
    1.50  
    1.51            val fs_thm_unit  = fs_unit_inst;
    1.52            val fs_thm_prod  = fs_inst RS (fs_inst RS fs_prod_inst);
    1.53 @@ -557,7 +557,7 @@
    1.54                      val pt_inst  = PureThy.get_thm thy'' (Name ("pt_"^ak_name''^"_inst"));
    1.55                      val at_inst  = PureThy.get_thm thy'' (Name ("at_"^ak_name''^"_inst"));
    1.56                    in
    1.57 -		   EVERY [ClassPackage.intro_classes_tac [],
    1.58 +		   EVERY [Class.intro_classes_tac [],
    1.59                            rtac (at_inst RS (pt_inst RS pt_perm_compose)) 1]
    1.60                    end)
    1.61  		else
    1.62 @@ -569,7 +569,7 @@
    1.63                                             [Name (ak_name' ^"_prm_"^ak_name^"_def"),
    1.64                                              Name (ak_name''^"_prm_"^ak_name^"_def")]));
    1.65                    in
    1.66 -                    EVERY [ClassPackage.intro_classes_tac [], simp_tac simp_s 1]
    1.67 +                    EVERY [Class.intro_classes_tac [], simp_tac simp_s 1]
    1.68                    end))
    1.69                in
    1.70                  AxClass.prove_arity (name,[],[cls_name]) proof thy''
    1.71 @@ -592,7 +592,7 @@
    1.72              val pt_inst  = PureThy.get_thm thy' (Name ("pt_"^ak_name^"_inst"));
    1.73              val at_inst  = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));
    1.74  
    1.75 -            fun cp_proof thm  = EVERY [ClassPackage.intro_classes_tac [],rtac (thm RS cp1) 1];
    1.76 +            fun cp_proof thm  = EVERY [Class.intro_classes_tac [],rtac (thm RS cp1) 1];
    1.77  	  
    1.78              val cp_thm_unit = cp_unit_inst;
    1.79              val cp_thm_prod = cp_inst RS (cp_inst RS cp_prod_inst);
    1.80 @@ -623,7 +623,7 @@
    1.81  	     let
    1.82  	       val qu_class = Sign.full_name thy ("pt_"^ak_name);
    1.83  	       val simp_s = HOL_basic_ss addsimps [defn];
    1.84 -               val proof = EVERY [ClassPackage.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
    1.85 +               val proof = EVERY [Class.intro_classes_tac [], REPEAT (asm_simp_tac simp_s 1)];
    1.86               in 
    1.87  	       AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
    1.88               end) ak_names;
    1.89 @@ -634,7 +634,7 @@
    1.90  	       val qu_class = Sign.full_name thy ("fs_"^ak_name);
    1.91  	       val supp_def = @{thm "Nominal.supp_def"};
    1.92                 val simp_s = HOL_ss addsimps [supp_def,Collect_const,finite_emptyI,defn];
    1.93 -               val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
    1.94 +               val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
    1.95               in 
    1.96  	       AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
    1.97               end) ak_names;
    1.98 @@ -645,7 +645,7 @@
    1.99  	       val qu_class = Sign.full_name thy ("cp_"^ak_name^"_"^ak_name');
   1.100  	       val supp_def = @{thm "Nominal.supp_def"};
   1.101                 val simp_s = HOL_ss addsimps [defn];
   1.102 -               val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
   1.103 +               val proof = EVERY [Class.intro_classes_tac [], asm_simp_tac simp_s 1];
   1.104               in
   1.105  	       AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
   1.106               end) ak_names)) ak_names;
     2.1 --- a/src/HOL/Nominal/nominal_package.ML	Fri Aug 10 17:04:20 2007 +0200
     2.2 +++ b/src/HOL/Nominal/nominal_package.ML	Fri Aug 10 17:04:24 2007 +0200
     2.3 @@ -502,7 +502,7 @@
     2.4        in
     2.5          foldl (fn ((s, tvs), thy) => AxClass.prove_arity
     2.6              (s, replicate (length tvs) (cp_class :: classes), [cp_class])
     2.7 -            (ClassPackage.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
     2.8 +            (Class.intro_classes_tac [] THEN ALLGOALS (resolve_tac thms)) thy)
     2.9            thy (full_new_type_names' ~~ tyvars)
    2.10        end;
    2.11  
    2.12 @@ -510,7 +510,7 @@
    2.13        fold (fn name1 => fold (composition_instance name1) atoms) atoms |>
    2.14        curry (Library.foldr (fn ((i, (tyname, args, _)), thy) =>
    2.15          AxClass.prove_arity (tyname, replicate (length args) classes, classes)
    2.16 -        (ClassPackage.intro_classes_tac [] THEN REPEAT (EVERY
    2.17 +        (Class.intro_classes_tac [] THEN REPEAT (EVERY
    2.18             [resolve_tac perm_empty_thms 1,
    2.19              resolve_tac perm_append_thms 1,
    2.20              resolve_tac perm_eq_thms 1, assume_tac 1])) thy))
    2.21 @@ -681,7 +681,7 @@
    2.22            AxClass.prove_arity
    2.23              (Sign.intern_type thy name,
    2.24                replicate (length tvs) (classes @ cp_classes), [class])
    2.25 -            (EVERY [ClassPackage.intro_classes_tac [],
    2.26 +            (EVERY [Class.intro_classes_tac [],
    2.27                rewrite_goals_tac [perm_def],
    2.28                asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1,
    2.29                asm_full_simp_tac (simpset_of thy addsimps
    2.30 @@ -706,7 +706,7 @@
    2.31            AxClass.prove_arity
    2.32              (Sign.intern_type thy name,
    2.33                replicate (length tvs) (classes @ cp_classes), [class])
    2.34 -            (EVERY [ClassPackage.intro_classes_tac [],
    2.35 +            (EVERY [Class.intro_classes_tac [],
    2.36                rewrite_goals_tac [perm_def],
    2.37                asm_full_simp_tac (simpset_of thy addsimps
    2.38                  ((Rep RS perm_closed1 RS Abs_inverse) ::
    2.39 @@ -1142,7 +1142,7 @@
    2.40          in fold (fn T => AxClass.prove_arity
    2.41              (fst (dest_Type T),
    2.42                replicate (length sorts) [class], [class])
    2.43 -            (ClassPackage.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
    2.44 +            (Class.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
    2.45          end) (atoms ~~ finite_supp_thms);
    2.46  
    2.47      (**** strong induction theorem ****)
     3.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Fri Aug 10 17:04:20 2007 +0200
     3.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Fri Aug 10 17:04:24 2007 +0200
     3.3 @@ -428,7 +428,7 @@
     3.4        in
     3.5          thy
     3.6          |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, [HOLogic.class_size])
     3.7 -             (ClassPackage.intro_classes_tac [])
     3.8 +             (Class.intro_classes_tac [])
     3.9        end
    3.10  
    3.11      val (size_def_thms, thy') =
     4.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Aug 10 17:04:20 2007 +0200
     4.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Aug 10 17:04:24 2007 +0200
     4.3 @@ -566,7 +566,7 @@
     4.4        in
     4.5          thy
     4.6          |> AxClass.prove_arity (tyco, replicate n HOLogic.typeS, [HOLogic.class_size])
     4.7 -             (ClassPackage.intro_classes_tac [])
     4.8 +             (Class.intro_classes_tac [])
     4.9        end
    4.10  
    4.11      val thy2' = thy
     5.1 --- a/src/HOLCF/Tools/pcpodef_package.ML	Fri Aug 10 17:04:20 2007 +0200
     5.2 +++ b/src/HOLCF/Tools/pcpodef_package.ML	Fri Aug 10 17:04:24 2007 +0200
     5.3 @@ -94,7 +94,7 @@
     5.4      fun make_po tac theory = theory
     5.5        |> TypedefPackage.add_typedef_i def (SOME name) (t, vs, mx) set opt_morphs tac
     5.6        ||> AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.sq_ord"])
     5.7 -           (ClassPackage.intro_classes_tac [])
     5.8 +           (Class.intro_classes_tac [])
     5.9        ||>> PureThy.add_defs_i true [Thm.no_attributes less_def]
    5.10        |-> (fn ((_, {type_definition, set_def, ...}), [less_definition]) =>
    5.11            AxClass.prove_arity (full_tname, lhs_sorts, ["Porder.po"])
     6.1 --- a/src/Provers/classical.ML	Fri Aug 10 17:04:20 2007 +0200
     6.2 +++ b/src/Provers/classical.ML	Fri Aug 10 17:04:24 2007 +0200
     6.3 @@ -1022,7 +1022,7 @@
     6.4  
     6.5  fun default_tac rules ctxt cs facts =
     6.6    HEADGOAL (rule_tac rules ctxt cs facts) ORELSE
     6.7 -  ClassPackage.default_intro_classes_tac facts;
     6.8 +  Class.default_intro_classes_tac facts;
     6.9  
    6.10  in
    6.11    val rule = METHOD_CLASET' o rule_tac;
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/Isar/class.ML	Fri Aug 10 17:04:24 2007 +0200
     7.3 @@ -0,0 +1,682 @@
     7.4 +(*  Title:      Pure/Isar/class.ML
     7.5 +    ID:         $Id$
     7.6 +    Author:     Florian Haftmann, TU Muenchen
     7.7 +
     7.8 +Type classes derived from primitive axclasses and locales.
     7.9 +*)
    7.10 +
    7.11 +signature CLASS =
    7.12 +sig
    7.13 +  val fork_mixfix: bool -> string option -> mixfix -> mixfix * mixfix
    7.14 +
    7.15 +  val axclass_cmd: bstring * xstring list
    7.16 +    -> ((bstring * Attrib.src list) * string list) list -> theory -> class * theory
    7.17 +  val class: bstring -> class list -> Element.context_i Locale.element list
    7.18 +    -> string list -> theory -> string * Proof.context
    7.19 +  val class_cmd: bstring -> string list -> Element.context Locale.element list
    7.20 +    -> string list -> theory -> string * Proof.context
    7.21 +  val instance_arity: arity list -> ((bstring * Attrib.src list) * term) list
    7.22 +    -> theory -> Proof.state
    7.23 +  val instance_arity_cmd: (bstring * string list * string) list
    7.24 +    -> ((bstring * Attrib.src list) * string) list
    7.25 +    -> theory -> Proof.state
    7.26 +  val prove_instance_arity: tactic -> arity list
    7.27 +    -> ((bstring * Attrib.src list) * term) list
    7.28 +    -> theory -> theory
    7.29 +  val instance_class: class * class -> theory -> Proof.state
    7.30 +  val instance_class_cmd: string * string -> theory -> Proof.state
    7.31 +  val instance_sort: class * sort -> theory -> Proof.state
    7.32 +  val instance_sort_cmd: string * string -> theory -> Proof.state
    7.33 +  val prove_instance_sort: tactic -> class * sort -> theory -> theory
    7.34 +
    7.35 +  val class_of_locale: theory -> string -> class option
    7.36 +  val add_const_in_class: string -> (string * term) * Syntax.mixfix
    7.37 +    -> theory -> theory
    7.38 +
    7.39 +  val print_classes: theory -> unit
    7.40 +  val intro_classes_tac: thm list -> tactic
    7.41 +  val default_intro_classes_tac: thm list -> tactic
    7.42 +end;
    7.43 +
    7.44 +structure Class : CLASS =
    7.45 +struct
    7.46 +
    7.47 +(** auxiliary **)
    7.48 +
    7.49 +fun fork_mixfix is_loc some_class mx =
    7.50 +  let
    7.51 +    val mx' = Syntax.unlocalize_mixfix mx;
    7.52 +    val mx_global = if is_some some_class orelse (is_loc andalso mx = mx')
    7.53 +      then NoSyn else mx';
    7.54 +    val mx_local = if is_loc then mx else NoSyn;
    7.55 +  in (mx_global, mx_local) end;
    7.56 +
    7.57 +fun axclass_cmd (class, raw_superclasses) raw_specs thy =
    7.58 +  let
    7.59 +    val ctxt = ProofContext.init thy;
    7.60 +    val superclasses = map (Sign.read_class thy) raw_superclasses;
    7.61 +    val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst) raw_specs;
    7.62 +    val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd) raw_specs)
    7.63 +      |> snd
    7.64 +      |> (map o map) fst;
    7.65 +  in AxClass.define_class (class, superclasses) [] (name_atts ~~ axiomss) thy end;
    7.66 +
    7.67 +
    7.68 +(** axclasses with implicit parameter handling **)
    7.69 +
    7.70 +(* axclass instances *)
    7.71 +
    7.72 +local
    7.73 +
    7.74 +fun gen_instance mk_prop add_thm after_qed insts thy =
    7.75 +  let
    7.76 +    fun after_qed' results =
    7.77 +      ProofContext.theory ((fold o fold) add_thm results #> after_qed);
    7.78 +  in
    7.79 +    thy
    7.80 +    |> ProofContext.init
    7.81 +    |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])]) o maps (mk_prop thy)) insts)
    7.82 +  end;
    7.83 +
    7.84 +in
    7.85 +
    7.86 +val axclass_instance_arity =
    7.87 +  gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity;
    7.88 +val axclass_instance_sort =
    7.89 +  gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel))
    7.90 +    AxClass.add_classrel I o single;
    7.91 +
    7.92 +end; (*local*)
    7.93 +
    7.94 +
    7.95 +(* introducing axclasses with implicit parameter handling *)
    7.96 +
    7.97 +fun axclass_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy =
    7.98 +  let
    7.99 +    val superclasses = map (Sign.certify_class thy) raw_superclasses;
   7.100 +    val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts;
   7.101 +    val prefix = Logic.const_of_class name;
   7.102 +    fun mk_const_name c = NameSpace.map_base (NameSpace.append prefix)
   7.103 +      (Sign.full_name thy c);
   7.104 +    fun add_const ((c, ty), syn) =
   7.105 +      Sign.add_consts_authentic [(c, ty, syn)]
   7.106 +      #> pair (mk_const_name c, ty);
   7.107 +    fun mk_axioms cs thy =
   7.108 +      raw_dep_axioms thy cs
   7.109 +      |> (map o apsnd o map) (Sign.cert_prop thy)
   7.110 +      |> rpair thy;
   7.111 +    fun add_constraint class (c, ty) =
   7.112 +      Sign.add_const_constraint_i (c, SOME
   7.113 +        (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
   7.114 +  in
   7.115 +    thy
   7.116 +    |> Theory.add_path prefix
   7.117 +    |> fold_map add_const consts
   7.118 +    ||> Theory.restore_naming thy
   7.119 +    |-> (fn cs => mk_axioms cs
   7.120 +    #-> (fn axioms_prop => AxClass.define_class (name, superclasses)
   7.121 +           (map fst cs @ other_consts) axioms_prop
   7.122 +    #-> (fn class => `(fn thy => AxClass.get_definition thy class)
   7.123 +    #-> (fn {intro, axioms, ...} => fold (add_constraint class) cs
   7.124 +    #> pair (class, ((intro, (map Thm.prop_of axioms, axioms)), cs))))))
   7.125 +  end;
   7.126 +
   7.127 +
   7.128 +(* instances with implicit parameter handling *)
   7.129 +
   7.130 +local
   7.131 +
   7.132 +fun gen_read_def thy prep_att read_def ((raw_name, raw_atts), raw_t) =
   7.133 +  let
   7.134 +    val (_, t) = read_def thy (raw_name, raw_t);
   7.135 +    val ((c, ty), _) = Sign.cert_def (Sign.pp thy) t;
   7.136 +    val atts = map (prep_att thy) raw_atts;
   7.137 +    val insts = Consts.typargs (Sign.consts_of thy) (c, ty);
   7.138 +    val name = case raw_name
   7.139 +     of "" => NONE
   7.140 +      | _ => SOME raw_name;
   7.141 +  in (c, (insts, ((name, t), atts))) end;
   7.142 +
   7.143 +fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Theory.read_axm;
   7.144 +fun read_def thy = gen_read_def thy (K I) (K I);
   7.145 +
   7.146 +fun gen_instance_arity prep_arity read_def do_proof raw_arities raw_defs theory =
   7.147 +  let
   7.148 +    val arities = map (prep_arity theory) raw_arities;
   7.149 +    val _ = if null arities then error "at least one arity must be given" else ();
   7.150 +    val _ = case (duplicates (op =) o map #1) arities
   7.151 +     of [] => ()
   7.152 +      | dupl_tycos => error ("type constructors occur more than once in arities: "
   7.153 +          ^ (commas o map quote) dupl_tycos);
   7.154 +    val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra o Sign.classes_of) theory
   7.155 +    fun get_consts_class tyco ty class =
   7.156 +      let
   7.157 +        val cs = (these o Option.map snd o try (AxClass.params_of_class theory)) class;
   7.158 +        val subst_ty = map_type_tfree (K ty);
   7.159 +      in
   7.160 +        map (fn (c, ty) => (c, ((tyco, class), subst_ty ty))) cs
   7.161 +      end;
   7.162 +    fun get_consts_sort (tyco, asorts, sort) =
   7.163 +      let
   7.164 +        val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) (Name.names Name.context "'a" asorts))
   7.165 +      in maps (get_consts_class tyco ty) (super_sort sort) end;
   7.166 +    val cs = maps get_consts_sort arities;
   7.167 +    fun mk_typnorm thy (ty, ty_sc) =
   7.168 +      case try (Sign.typ_match thy (Logic.varifyT ty_sc, ty)) Vartab.empty
   7.169 +       of SOME env => SOME (Logic.varifyT #> Envir.typ_subst_TVars env #> Logic.unvarifyT)
   7.170 +        | NONE => NONE;
   7.171 +    fun read_defs defs cs thy_read =
   7.172 +      let
   7.173 +        fun read raw_def cs =
   7.174 +          let
   7.175 +            val (c, (inst, ((name_opt, t), atts))) = read_def thy_read raw_def;
   7.176 +            val ty = Consts.instance (Sign.consts_of thy_read) (c, inst);
   7.177 +            val ((tyco, class), ty') = case AList.lookup (op =) cs c
   7.178 +             of NONE => error ("illegal definition for constant " ^ quote c)
   7.179 +              | SOME class_ty => class_ty;
   7.180 +            val name = case name_opt
   7.181 +             of NONE => Thm.def_name (Logic.name_arity (tyco, [], c))
   7.182 +              | SOME name => name;
   7.183 +            val t' = case mk_typnorm thy_read (ty', ty)
   7.184 +             of NONE => error ("illegal definition for constant " ^
   7.185 +                  quote (c ^ "::" ^ setmp show_sorts true
   7.186 +                    (Sign.string_of_typ thy_read) ty))
   7.187 +              | SOME norm => map_types norm t
   7.188 +          in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end;
   7.189 +      in fold_map read defs cs end;
   7.190 +    val (defs, _) = read_defs raw_defs cs
   7.191 +      (fold Sign.primitive_arity arities (Theory.copy theory));
   7.192 +    fun get_remove_contraint c thy =
   7.193 +      let
   7.194 +        val ty = Sign.the_const_constraint thy c;
   7.195 +      in
   7.196 +        thy
   7.197 +        |> Sign.add_const_constraint_i (c, NONE)
   7.198 +        |> pair (c, Logic.unvarifyT ty)
   7.199 +      end;
   7.200 +    fun add_defs defs thy =
   7.201 +      thy
   7.202 +      |> PureThy.add_defs_i true (map ((apsnd o map) (Attrib.attribute thy) o snd) defs)
   7.203 +      |-> (fn thms => pair (map fst defs ~~ thms));
   7.204 +    fun after_qed cs defs thy =
   7.205 +      thy
   7.206 +      |> fold Sign.add_const_constraint_i (map (apsnd SOME) cs)
   7.207 +      |> fold (Code.add_func false o snd) defs;
   7.208 +  in
   7.209 +    theory
   7.210 +    |> fold_map get_remove_contraint (map fst cs |> distinct (op =))
   7.211 +    ||>> add_defs defs
   7.212 +    |-> (fn (cs, defs) => do_proof (after_qed cs defs) arities)
   7.213 +  end;
   7.214 +
   7.215 +fun instance_arity_cmd' do_proof = gen_instance_arity Sign.read_arity read_def_cmd do_proof;
   7.216 +fun instance_arity' do_proof = gen_instance_arity Sign.cert_arity read_def do_proof;
   7.217 +fun tactic_proof tac after_qed arities =
   7.218 +  fold (fn arity => AxClass.prove_arity arity tac) arities
   7.219 +  #> after_qed;
   7.220 +
   7.221 +in
   7.222 +
   7.223 +val instance_arity_cmd = instance_arity_cmd' axclass_instance_arity;
   7.224 +val instance_arity = instance_arity' axclass_instance_arity;
   7.225 +val prove_instance_arity = instance_arity' o tactic_proof;
   7.226 +
   7.227 +end; (*local*)
   7.228 +
   7.229 +
   7.230 +
   7.231 +(** combining locales and axclasses **)
   7.232 +
   7.233 +(* theory data *)
   7.234 +
   7.235 +datatype class_data = ClassData of {
   7.236 +  locale: string,
   7.237 +  consts: (string * string) list
   7.238 +    (*locale parameter ~> toplevel theory constant*),
   7.239 +  v: string option,
   7.240 +  intro: thm
   7.241 +} * thm list (*derived defs*);
   7.242 +
   7.243 +fun rep_classdata (ClassData c) = c;
   7.244 +
   7.245 +fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2));
   7.246 +
   7.247 +structure ClassData = TheoryDataFun
   7.248 +(
   7.249 +  type T = class_data Graph.T * class Symtab.table (*locale name ~> class name*);
   7.250 +  val empty = (Graph.empty, Symtab.empty);
   7.251 +  val copy = I;
   7.252 +  val extend = I;
   7.253 +  fun merge _ = merge_pair (Graph.merge (K true)) (Symtab.merge (K true));
   7.254 +);
   7.255 +
   7.256 +
   7.257 +(* queries *)
   7.258 +
   7.259 +val lookup_class_data = Option.map rep_classdata oo try o Graph.get_node o fst o ClassData.get;
   7.260 +fun class_of_locale thy = Symtab.lookup ((snd o ClassData.get) thy);
   7.261 +
   7.262 +fun the_class_data thy class =
   7.263 +  case lookup_class_data thy class
   7.264 +    of NONE => error ("undeclared class " ^ quote class)
   7.265 +     | SOME data => data;
   7.266 +
   7.267 +val ancestry = Graph.all_succs o fst o ClassData.get;
   7.268 +
   7.269 +fun param_map thy =
   7.270 +  let
   7.271 +    fun params class =
   7.272 +      let
   7.273 +        val const_typs = (#params o AxClass.get_definition thy) class;
   7.274 +        val const_names = (#consts o fst o the_class_data thy) class;
   7.275 +      in
   7.276 +        (map o apsnd) (fn c => (c, (the o AList.lookup (op =) const_typs) c)) const_names
   7.277 +      end;
   7.278 +  in maps params o ancestry thy end;
   7.279 +
   7.280 +fun these_defs thy = maps (these o Option.map snd o lookup_class_data thy) o ancestry thy;
   7.281 +
   7.282 +fun these_intros thy =
   7.283 +  Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o fst o rep_classdata) data))
   7.284 +    ((fst o ClassData.get) thy) [];
   7.285 +
   7.286 +fun print_classes thy =
   7.287 +  let
   7.288 +    val algebra = Sign.classes_of thy;
   7.289 +    val arities =
   7.290 +      Symtab.empty
   7.291 +      |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) =>
   7.292 +           Symtab.map_default (class, []) (insert (op =) tyco)) arities)
   7.293 +             ((#arities o Sorts.rep_algebra) algebra);
   7.294 +    val the_arities = these o Symtab.lookup arities;
   7.295 +    fun mk_arity class tyco =
   7.296 +      let
   7.297 +        val Ss = Sorts.mg_domain algebra tyco [class];
   7.298 +      in Sign.pretty_arity thy (tyco, Ss, [class]) end;
   7.299 +    fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
   7.300 +      ^ setmp show_sorts false (Sign.string_of_typ thy o Type.strip_sorts) ty);
   7.301 +    fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
   7.302 +      (SOME o Pretty.str) ("class " ^ class ^ ":"),
   7.303 +      (SOME o Pretty.block) [Pretty.str "supersort: ",
   7.304 +        (Sign.pretty_sort thy o Sign.certify_sort thy o Sign.super_classes thy) class],
   7.305 +      Option.map (Pretty.str o prefix "locale: " o #locale o fst) (lookup_class_data thy class),
   7.306 +      ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param
   7.307 +        o these o Option.map #params o try (AxClass.get_definition thy)) class,
   7.308 +      (SOME o Pretty.block o Pretty.breaks) [
   7.309 +        Pretty.str "instances:",
   7.310 +        Pretty.list "" "" (map (mk_arity class) (the_arities class))
   7.311 +      ]
   7.312 +    ]
   7.313 +  in
   7.314 +    (Pretty.writeln o Pretty.chunks o separate (Pretty.str "") o map mk_entry o Sorts.all_classes)
   7.315 +      algebra
   7.316 +  end;
   7.317 +
   7.318 +
   7.319 +(* updaters *)
   7.320 +
   7.321 +fun add_class_data ((class, superclasses), (locale, consts, v, intro)) =
   7.322 +  ClassData.map (fn (gr, tab) => (
   7.323 +    gr
   7.324 +    |> Graph.new_node (class, ClassData ({ locale = locale, consts = consts,
   7.325 +         v = v, intro = intro }, []))
   7.326 +    |> fold (curry Graph.add_edge class) superclasses,
   7.327 +    tab
   7.328 +    |> Symtab.update (locale, class)
   7.329 +  ));
   7.330 +
   7.331 +fun add_class_const_thm (class, thm) = (ClassData.map o apfst o Graph.map_node class)
   7.332 +  (fn ClassData (data, thms) => ClassData (data, thm :: thms));
   7.333 +
   7.334 +(* tactics and methods *)
   7.335 +
   7.336 +fun intro_classes_tac facts st =
   7.337 +  let
   7.338 +    val thy = Thm.theory_of_thm st;
   7.339 +    val classes = Sign.all_classes thy;
   7.340 +    val class_trivs = map (Thm.class_triv thy) classes;
   7.341 +    val class_intros = these_intros thy;
   7.342 +    fun add_axclass_intro class =
   7.343 +      case try (AxClass.get_definition thy) class of SOME {intro, ...} => cons intro | _ => I;
   7.344 +    val axclass_intros = fold add_axclass_intro classes [];
   7.345 +  in
   7.346 +    st
   7.347 +    |> ((ALLGOALS (Method.insert_tac facts THEN'
   7.348 +          REPEAT_ALL_NEW (resolve_tac (class_trivs @ class_intros @ axclass_intros))))
   7.349 +            THEN Tactic.distinct_subgoals_tac)
   7.350 +  end;
   7.351 +
   7.352 +fun default_intro_classes_tac [] = intro_classes_tac []
   7.353 +  | default_intro_classes_tac _ = Tactical.no_tac;    (*no error message!*)
   7.354 +
   7.355 +fun default_tac rules ctxt facts =
   7.356 +  HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
   7.357 +    default_intro_classes_tac facts;
   7.358 +
   7.359 +val _ = Context.add_setup (Method.add_methods
   7.360 + [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
   7.361 +    "back-chain introduction rules of classes"),
   7.362 +  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
   7.363 +    "apply some intro/elim rule")]);
   7.364 +
   7.365 +
   7.366 +(* tactical interfaces to locale commands *)
   7.367 +
   7.368 +fun prove_interpretation tac prfx_atts expr insts thy =
   7.369 +  thy
   7.370 +  |> Locale.interpretation_i I prfx_atts expr insts
   7.371 +  |> Proof.global_terminal_proof (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
   7.372 +  |> ProofContext.theory_of;
   7.373 +
   7.374 +fun prove_interpretation_in tac after_qed (name, expr) thy =
   7.375 +  thy
   7.376 +  |> Locale.interpretation_in_locale (ProofContext.theory after_qed) (name, expr)
   7.377 +  |> Proof.global_terminal_proof (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
   7.378 +  |> ProofContext.theory_of;
   7.379 +
   7.380 +
   7.381 +(* constructing class introduction and other rules from axclass and locale rules *)
   7.382 +
   7.383 +fun mk_instT class = Symtab.empty
   7.384 +  |> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class]));
   7.385 +
   7.386 +fun mk_inst class param_names cs =
   7.387 +  Symtab.empty
   7.388 +  |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
   7.389 +       (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;
   7.390 +
   7.391 +fun OF_LAST thm1 thm2 =
   7.392 +  let
   7.393 +    val n = (length o Logic.strip_imp_prems o prop_of) thm2;
   7.394 +  in (thm1 RSN (n, thm2)) end;
   7.395 +
   7.396 +fun strip_all_ofclass thy sort =
   7.397 +  let
   7.398 +    val typ = TVar ((AxClass.param_tyvarname, 0), sort);
   7.399 +    fun prem_inclass t =
   7.400 +      case Logic.strip_imp_prems t
   7.401 +       of ofcls :: _ => try Logic.dest_inclass ofcls
   7.402 +        | [] => NONE;
   7.403 +    fun strip_ofclass class thm =
   7.404 +      thm OF (fst o AxClass.of_sort thy (typ, [class])) AxClass.cache;
   7.405 +    fun strip thm = case (prem_inclass o Thm.prop_of) thm
   7.406 +     of SOME (_, class) => thm |> strip_ofclass class |> strip
   7.407 +      | NONE => thm;
   7.408 +  in strip end;
   7.409 +
   7.410 +fun class_intro thy locale class sups =
   7.411 +  let
   7.412 +    fun class_elim class =
   7.413 +      case (map Drule.unconstrainTs o #axioms o AxClass.get_definition thy) class
   7.414 +       of [thm] => SOME thm
   7.415 +        | [] => NONE;
   7.416 +    val pred_intro = case Locale.intros thy locale
   7.417 +     of ([ax_intro], [intro]) => intro |> OF_LAST ax_intro |> SOME
   7.418 +      | ([intro], []) => SOME intro
   7.419 +      | ([], [intro]) => SOME intro
   7.420 +      | _ => NONE;
   7.421 +    val pred_intro' = pred_intro
   7.422 +      |> Option.map (fn intro => intro OF map_filter class_elim sups);
   7.423 +    val class_intro = (#intro o AxClass.get_definition thy) class;
   7.424 +    val raw_intro = case pred_intro'
   7.425 +     of SOME pred_intro => class_intro |> OF_LAST pred_intro
   7.426 +      | NONE => class_intro;
   7.427 +    val sort = Sign.super_classes thy class;
   7.428 +    val typ = TVar ((AxClass.param_tyvarname, 0), sort);
   7.429 +    val defs = these_defs thy sups;
   7.430 +  in
   7.431 +    raw_intro
   7.432 +    |> Drule.instantiate' [SOME (Thm.ctyp_of thy typ)] []
   7.433 +    |> strip_all_ofclass thy sort
   7.434 +    |> Thm.strip_shyps
   7.435 +    |> MetaSimplifier.rewrite_rule defs
   7.436 +    |> Drule.unconstrainTs
   7.437 +  end;
   7.438 +
   7.439 +fun interpretation_in_rule thy (class1, class2) =
   7.440 +  let
   7.441 +    val (params, consts) = split_list (param_map thy [class1]);
   7.442 +    (*FIXME also remember this at add_class*)
   7.443 +    fun mk_axioms class =
   7.444 +      let
   7.445 +        val name_locale = (#locale o fst o the_class_data thy) class;
   7.446 +        val inst = mk_inst class params consts;
   7.447 +      in
   7.448 +        Locale.global_asms_of thy name_locale
   7.449 +        |> maps snd
   7.450 +        |> (map o map_aterms) (fn Free (s, _) => (the o Symtab.lookup inst) s | t => t)
   7.451 +        |> (map o map_types o map_atyps) (fn TFree _ => TFree ("'a", [class1]) | T => T)
   7.452 +        |> map (ObjectLogic.ensure_propT thy)
   7.453 +      end;
   7.454 +    val (prems, concls) = pairself mk_axioms (class1, class2);
   7.455 +  in
   7.456 +    Goal.prove_global thy [] prems (Logic.mk_conjunction_list concls)
   7.457 +      (Locale.intro_locales_tac true (ProofContext.init thy))
   7.458 +  end;
   7.459 +
   7.460 +
   7.461 +(* classes *)
   7.462 +
   7.463 +local
   7.464 +
   7.465 +fun read_param thy raw_t =
   7.466 +  let
   7.467 +    val t = Sign.read_term thy raw_t
   7.468 +  in case try dest_Const t
   7.469 +   of SOME (c, _) => c
   7.470 +    | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
   7.471 +  end;
   7.472 +
   7.473 +fun gen_class add_locale prep_class prep_param bname
   7.474 +    raw_supclasses raw_elems raw_other_consts thy =
   7.475 +  let
   7.476 +    (*FIXME need proper concept for reading locale statements*)
   7.477 +    fun subst_classtyvar (_, _) =
   7.478 +          TFree (AxClass.param_tyvarname, [])
   7.479 +      | subst_classtyvar (v, sort) =
   7.480 +          error ("Sort constraint illegal in type class, for type variable " ^ v ^ "::" ^ Sign.string_of_sort thy sort);
   7.481 +    (*val subst_classtyvars = Element.map_ctxt {name = I, var = I, term = I,
   7.482 +      typ = Term.map_type_tfree subst_classtyvar, fact = I, attrib = I};*)
   7.483 +    val other_consts = map (prep_param thy) raw_other_consts;
   7.484 +    val (elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
   7.485 +      | Locale.Expr i => apsnd (cons i)) raw_elems ([], []);
   7.486 +    val supclasses = map (prep_class thy) raw_supclasses;
   7.487 +    val sups = filter (is_some o lookup_class_data thy) supclasses
   7.488 +      |> Sign.certify_sort thy;
   7.489 +    val supsort = Sign.certify_sort thy supclasses;
   7.490 +    val suplocales = map (Locale.Locale o #locale o fst o the_class_data thy) sups;
   7.491 +    val supexpr = Locale.Merge (suplocales @ includes);
   7.492 +    val supparams = (map fst o Locale.parameters_of_expr thy)
   7.493 +      (Locale.Merge suplocales);
   7.494 +    val supconsts = AList.make (the o AList.lookup (op =) (param_map thy sups))
   7.495 +      (map fst supparams);
   7.496 +    (*val elems_constrains = map
   7.497 +      (Element.Constrains o apsnd (Term.map_type_tfree subst_classtyvar)) supparams;*)
   7.498 +    fun mk_tyvar (_, sort) = TFree (AxClass.param_tyvarname,
   7.499 +      if Sign.subsort thy (supsort, sort) then sort else error
   7.500 +        ("Sort " ^ Sign.string_of_sort thy sort
   7.501 +          ^ " is less general than permitted least general sort "
   7.502 +          ^ Sign.string_of_sort thy supsort));
   7.503 +    fun extract_params thy name_locale =
   7.504 +      let
   7.505 +        val params = Locale.parameters_of thy name_locale;
   7.506 +        val v = case (maps typ_tfrees o map (snd o fst)) params
   7.507 +         of (v, _) :: _ => SOME v
   7.508 +          | _ => NONE;
   7.509 +      in
   7.510 +        (v, (map (fst o fst) params, params
   7.511 +        |> (map o apfst o apsnd o Term.map_type_tfree) mk_tyvar
   7.512 +        |> (map o apsnd) (fork_mixfix true NONE #> fst)
   7.513 +        |> chop (length supconsts)
   7.514 +        |> snd))
   7.515 +      end;
   7.516 +    fun extract_assumes name_locale params thy cs =
   7.517 +      let
   7.518 +        val consts = supconsts @ (map (fst o fst) params ~~ cs);
   7.519 +        fun subst (Free (c, ty)) =
   7.520 +              Const ((fst o the o AList.lookup (op =) consts) c, ty)
   7.521 +          | subst t = t;
   7.522 +        val super_defs = these_defs thy sups;
   7.523 +        fun prep_asm ((name, atts), ts) =
   7.524 +          ((NameSpace.base name, map (Attrib.attribute thy) atts),
   7.525 +            (map o map_aterms) ((*MetaSimplifier.rewrite_term thy super_defs [] o *)subst) ts);
   7.526 +      in
   7.527 +        Locale.global_asms_of thy name_locale
   7.528 +        |> map prep_asm
   7.529 +      end;
   7.530 +    fun note_intro name_axclass class_intro =
   7.531 +      PureThy.note_thmss_qualified "" ((Logic.const_of_class o NameSpace.base) name_axclass)
   7.532 +        [(("intro", []), [([class_intro], [])])]
   7.533 +      #> snd
   7.534 +  in
   7.535 +    thy
   7.536 +    |> add_locale (SOME "") bname supexpr ((*elems_constrains @*) elems)
   7.537 +    |-> (fn name_locale => ProofContext.theory_result (
   7.538 +      `(fn thy => extract_params thy name_locale)
   7.539 +      #-> (fn (v, (param_names, params)) =>
   7.540 +        axclass_params (bname, supsort) params (extract_assumes name_locale params) other_consts
   7.541 +      #-> (fn (name_axclass, ((_, (ax_terms, ax_axioms)), consts)) =>
   7.542 +        `(fn thy => class_intro thy name_locale name_axclass sups)
   7.543 +      #-> (fn class_intro =>
   7.544 +        add_class_data ((name_axclass, sups),
   7.545 +          (name_locale, map (fst o fst) params ~~ map fst consts, v,
   7.546 +            class_intro))
   7.547 +        (*FIXME: class_data should already contain data relevant
   7.548 +          for interpretation; use this later for class target*)
   7.549 +        (*FIXME: general export_fixes which may be parametrized
   7.550 +          with pieces of an emerging class*)
   7.551 +      #> note_intro name_axclass class_intro
   7.552 +      #> prove_interpretation ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
   7.553 +          ((false, Logic.const_of_class bname), []) (Locale.Locale name_locale)
   7.554 +          ((mk_instT name_axclass, mk_inst name_axclass param_names (map snd supconsts @ consts)), [])
   7.555 +      #> pair name_axclass
   7.556 +      )))))
   7.557 +  end;
   7.558 +
   7.559 +in
   7.560 +
   7.561 +val class_cmd = gen_class Locale.add_locale Sign.intern_class read_param;
   7.562 +val class = gen_class Locale.add_locale_i Sign.certify_class (K I);
   7.563 +
   7.564 +end; (*local*)
   7.565 +
   7.566 +local
   7.567 +
   7.568 +fun instance_subclass (class1, class2) thy  =
   7.569 +  let
   7.570 +    val interp = interpretation_in_rule thy (class1, class2);
   7.571 +    val ax = #axioms (AxClass.get_definition thy class1);
   7.572 +    val intro = #intro (AxClass.get_definition thy class2)
   7.573 +      |> Drule.instantiate' [SOME (Thm.ctyp_of thy
   7.574 +          (TVar ((AxClass.param_tyvarname, 0), [class1])))] [];
   7.575 +    val thm = 
   7.576 +      intro
   7.577 +      |> OF_LAST (interp OF ax)
   7.578 +      |> strip_all_ofclass thy (Sign.super_classes thy class2);
   7.579 +  in
   7.580 +    thy |> AxClass.add_classrel thm
   7.581 +  end;
   7.582 +
   7.583 +fun instance_subsort (class, sort) thy =
   7.584 +  let
   7.585 +    val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra
   7.586 +      o Sign.classes_of) thy sort;
   7.587 +    val classes = filter_out (fn class' => Sign.subsort thy ([class], [class']))
   7.588 +      (rev super_sort);
   7.589 +  in
   7.590 +    thy |> fold (curry instance_subclass class) classes
   7.591 +  end;
   7.592 +
   7.593 +fun instance_sort' do_proof (class, sort) theory =
   7.594 +  let
   7.595 +    val loc_name = (#locale o fst o the_class_data theory) class;
   7.596 +    val loc_expr =
   7.597 +      (Locale.Merge o map (Locale.Locale o #locale o fst o the_class_data theory)) sort;
   7.598 +  in
   7.599 +    theory
   7.600 +    |> do_proof (instance_subsort (class, sort)) (loc_name, loc_expr)
   7.601 +  end;
   7.602 +
   7.603 +fun gen_instance_sort prep_class prep_sort (raw_class, raw_sort) theory =
   7.604 +  let
   7.605 +    val class = prep_class theory raw_class;
   7.606 +    val sort = prep_sort theory raw_sort;
   7.607 +  in
   7.608 +    theory
   7.609 +    |> instance_sort' (Locale.interpretation_in_locale o ProofContext.theory) (class, sort)
   7.610 +  end;
   7.611 +
   7.612 +fun gen_instance_class prep_class (raw_class, raw_superclass) theory =
   7.613 +  let
   7.614 +    val class = prep_class theory raw_class;
   7.615 +    val superclass = prep_class theory raw_superclass;
   7.616 +  in
   7.617 +    theory
   7.618 +    |> axclass_instance_sort (class, superclass)
   7.619 +  end;
   7.620 +
   7.621 +in
   7.622 +
   7.623 +val instance_sort_cmd = gen_instance_sort Sign.read_class Sign.read_sort;
   7.624 +val instance_sort = gen_instance_sort Sign.certify_class Sign.certify_sort;
   7.625 +val prove_instance_sort = instance_sort' o prove_interpretation_in;
   7.626 +val instance_class_cmd = gen_instance_class Sign.read_class;
   7.627 +val instance_class = gen_instance_class Sign.certify_class;
   7.628 +
   7.629 +end; (*local*)
   7.630 +
   7.631 +
   7.632 +(** class target **)
   7.633 +
   7.634 +fun export_fixes thy class =
   7.635 +  let
   7.636 +    val v = (#v o fst o the_class_data thy) class;
   7.637 +    val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) [class];
   7.638 +    val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
   7.639 +      if SOME w = v then TFree (w, constrain_sort sort) else TFree var);
   7.640 +    val consts = param_map thy [class];
   7.641 +    fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) consts v
   7.642 +         of SOME (c, _) => Const (c, ty)
   7.643 +          | NONE => t)
   7.644 +      | subst_aterm t = t;
   7.645 +  in map_types subst_typ #> Term.map_aterms subst_aterm end;
   7.646 +
   7.647 +fun add_const_in_class class ((c, rhs), syn) thy =
   7.648 +  let
   7.649 +    val prfx = (Logic.const_of_class o NameSpace.base) class;
   7.650 +    fun mk_name inject c =
   7.651 +      let
   7.652 +        val n1 = Sign.full_name thy c;
   7.653 +        val n2 = NameSpace.qualifier n1;
   7.654 +        val n3 = NameSpace.base n1;
   7.655 +      in NameSpace.implode (n2 :: inject @ [n3]) end;
   7.656 +    val abbr' = mk_name [prfx, prfx] c;
   7.657 +    val rhs' = export_fixes thy class rhs;
   7.658 +    val ty' = Term.fastype_of rhs';
   7.659 +    val def = (c, Logic.mk_equals (Const (mk_name [prfx] c, ty'), rhs'));
   7.660 +    val (syn', _) = fork_mixfix true NONE syn;
   7.661 +    fun interpret def =
   7.662 +      let
   7.663 +        val def' = symmetric def
   7.664 +        val tac = (ALLGOALS o ProofContext.fact_tac) [def'];
   7.665 +        val name_locale = (#locale o fst o the_class_data thy) class;
   7.666 +        val def_eq = Thm.prop_of def';
   7.667 +        val (params, consts) = split_list (param_map thy [class]);
   7.668 +      in
   7.669 +        prove_interpretation tac ((false, prfx), []) (Locale.Locale name_locale)
   7.670 +          ((mk_instT class, mk_inst class params consts), [def_eq])
   7.671 +        #> add_class_const_thm (class, def')
   7.672 +      end;
   7.673 +  in
   7.674 +    thy
   7.675 +    |> Sign.hide_consts_i true [abbr']
   7.676 +    |> Sign.add_path prfx
   7.677 +    |> Sign.add_consts_authentic [(c, ty', syn')]
   7.678 +    |> Sign.parent_path
   7.679 +    |> Sign.sticky_prefix prfx
   7.680 +    |> PureThy.add_defs_i false [(def, [])]
   7.681 +    |-> (fn [def] => interpret def)
   7.682 +    |> Sign.restore_naming thy
   7.683 +  end;
   7.684 +
   7.685 +end;
     8.1 --- a/src/Pure/Isar/theory_target.ML	Fri Aug 10 17:04:20 2007 +0200
     8.2 +++ b/src/Pure/Isar/theory_target.ML	Fri Aug 10 17:04:24 2007 +0200
     8.3 @@ -83,12 +83,12 @@
     8.4        let
     8.5          val U = map #2 xs ---> T;
     8.6          val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs);
     8.7 -        val (mx1, mx2) = ClassPackage.fork_mixfix is_loc some_class mx;
     8.8 +        val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx;
     8.9          val thy' = Sign.add_consts_authentic [(c, U, mx1)] thy;
    8.10        in (((c, mx2), t), thy') end;
    8.11  
    8.12      fun const_class (SOME class) ((c, _), mx) (_, t) =
    8.13 -          ClassPackage.add_const_in_class class ((c, t), mx)
    8.14 +          Class.add_const_in_class class ((c, t), mx)
    8.15        | const_class NONE _ _ = I;
    8.16  
    8.17      val (abbrs, lthy') = lthy
    8.18 @@ -136,7 +136,7 @@
    8.19  
    8.20      val ((lhs as Const (full_c, _), rhs), lthy1) = lthy
    8.21        |> LocalTheory.theory_result (Sign.add_abbrev (#1 prmode) (c, u'));
    8.22 -    val (mx1, mx2) = ClassPackage.fork_mixfix is_loc some_class mx;
    8.23 +    val (mx1, mx2) = Class.fork_mixfix is_loc some_class mx;
    8.24    in
    8.25      lthy1
    8.26      |> LocalTheory.theory (Sign.add_notation prmode [(lhs, mx1)])
    8.27 @@ -341,7 +341,7 @@
    8.28    let
    8.29      val thy = ProofContext.theory_of ctxt;
    8.30      val is_loc = loc <> "";
    8.31 -    val some_class = ClassPackage.class_of_locale thy loc;
    8.32 +    val some_class = Class.class_of_locale thy loc;
    8.33    in
    8.34      ctxt
    8.35      |> Data.put (if is_loc then SOME loc else NONE)
     9.1 --- a/src/Pure/Tools/class_package.ML	Fri Aug 10 17:04:20 2007 +0200
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,686 +0,0 @@
     9.4 -(*  Title:      Pure/Tools/class_package.ML
     9.5 -    ID:         $Id$
     9.6 -    Author:     Florian Haftmann, TU Muenchen
     9.7 -
     9.8 -Type classes derived from primitive axclasses and locales.
     9.9 -*)
    9.10 -
    9.11 -signature CLASS_PACKAGE =
    9.12 -sig
    9.13 -  val fork_mixfix: bool -> string option -> mixfix -> mixfix * mixfix
    9.14 -
    9.15 -  val axclass_cmd: bstring * xstring list
    9.16 -    -> ((bstring * Attrib.src list) * string list) list -> theory -> class * theory
    9.17 -  val class: bstring -> class list -> Element.context_i Locale.element list
    9.18 -    -> string list -> theory -> string * Proof.context
    9.19 -  val class_cmd: bstring -> string list -> Element.context Locale.element list
    9.20 -    -> string list -> theory -> string * Proof.context
    9.21 -  val instance_arity: arity list -> ((bstring * Attrib.src list) * term) list
    9.22 -    -> theory -> Proof.state
    9.23 -  val instance_arity_cmd: (bstring * string list * string) list
    9.24 -    -> ((bstring * Attrib.src list) * string) list
    9.25 -    -> theory -> Proof.state
    9.26 -  val prove_instance_arity: tactic -> arity list
    9.27 -    -> ((bstring * Attrib.src list) * term) list
    9.28 -    -> theory -> theory
    9.29 -  val instance_class: class * class -> theory -> Proof.state
    9.30 -  val instance_class_cmd: string * string -> theory -> Proof.state
    9.31 -  val instance_sort: class * sort -> theory -> Proof.state
    9.32 -  val instance_sort_cmd: string * string -> theory -> Proof.state
    9.33 -  val prove_instance_sort: tactic -> class * sort -> theory -> theory
    9.34 -
    9.35 -  val class_of_locale: theory -> string -> class option
    9.36 -  val add_const_in_class: string -> (string * term) * Syntax.mixfix
    9.37 -    -> theory -> theory
    9.38 -
    9.39 -  val print_classes: theory -> unit
    9.40 -  val intro_classes_tac: thm list -> tactic
    9.41 -  val default_intro_classes_tac: thm list -> tactic
    9.42 -end;
    9.43 -
    9.44 -structure ClassPackage : CLASS_PACKAGE =
    9.45 -struct
    9.46 -
    9.47 -(** auxiliary **)
    9.48 -
    9.49 -fun fork_mixfix is_loc some_class mx =
    9.50 -  let
    9.51 -    val mx' = Syntax.unlocalize_mixfix mx;
    9.52 -    val mx_global = if is_some some_class orelse (is_loc andalso mx = mx')
    9.53 -      then NoSyn else mx';
    9.54 -    val mx_local = if is_loc then mx else NoSyn;
    9.55 -  in (mx_global, mx_local) end;
    9.56 -
    9.57 -fun axclass_cmd (class, raw_superclasses) raw_specs thy =
    9.58 -  let
    9.59 -    val ctxt = ProofContext.init thy;
    9.60 -    val superclasses = map (Sign.read_class thy) raw_superclasses;
    9.61 -    val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst) raw_specs;
    9.62 -    val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd) raw_specs)
    9.63 -      |> snd
    9.64 -      |> (map o map) fst;
    9.65 -  in AxClass.define_class (class, superclasses) [] (name_atts ~~ axiomss) thy end;
    9.66 -
    9.67 -
    9.68 -(** AxClasses with implicit parameter handling **)
    9.69 -
    9.70 -(* AxClass instances *)
    9.71 -
    9.72 -local
    9.73 -
    9.74 -fun gen_instance mk_prop add_thm after_qed insts thy =
    9.75 -  let
    9.76 -    fun after_qed' results =
    9.77 -      ProofContext.theory ((fold o fold) add_thm results #> after_qed);
    9.78 -  in
    9.79 -    thy
    9.80 -    |> ProofContext.init
    9.81 -    |> Proof.theorem_i NONE after_qed' ((map (fn t => [(t, [])]) o maps (mk_prop thy)) insts)
    9.82 -  end;
    9.83 -
    9.84 -in
    9.85 -
    9.86 -val axclass_instance_arity =
    9.87 -  gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity;
    9.88 -val axclass_instance_sort =
    9.89 -  gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel))
    9.90 -    AxClass.add_classrel I o single;
    9.91 -
    9.92 -end; (*local*)
    9.93 -
    9.94 -
    9.95 -(* introducing axclasses with implicit parameter handling *)
    9.96 -
    9.97 -fun axclass_params (name, raw_superclasses) raw_consts raw_dep_axioms other_consts thy =
    9.98 -  let
    9.99 -    val superclasses = map (Sign.certify_class thy) raw_superclasses;
   9.100 -    val consts = (map o apfst o apsnd) (Sign.certify_typ thy) raw_consts;
   9.101 -    val prefix = Logic.const_of_class name;
   9.102 -    fun mk_const_name c = NameSpace.map_base (NameSpace.append prefix)
   9.103 -      (Sign.full_name thy c);
   9.104 -    fun add_const ((c, ty), syn) =
   9.105 -      Sign.add_consts_authentic [(c, ty, syn)]
   9.106 -      #> pair (mk_const_name c, ty);
   9.107 -    fun mk_axioms cs thy =
   9.108 -      raw_dep_axioms thy cs
   9.109 -      |> (map o apsnd o map) (Sign.cert_prop thy)
   9.110 -      |> rpair thy;
   9.111 -    fun add_constraint class (c, ty) =
   9.112 -      Sign.add_const_constraint_i (c, SOME
   9.113 -        (Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty));
   9.114 -  in
   9.115 -    thy
   9.116 -    |> Theory.add_path prefix
   9.117 -    |> fold_map add_const consts
   9.118 -    ||> Theory.restore_naming thy
   9.119 -    |-> (fn cs => mk_axioms cs
   9.120 -    #-> (fn axioms_prop => AxClass.define_class (name, superclasses)
   9.121 -           (map fst cs @ other_consts) axioms_prop
   9.122 -    #-> (fn class => `(fn thy => AxClass.get_definition thy class)
   9.123 -    #-> (fn {intro, axioms, ...} => fold (add_constraint class) cs
   9.124 -    #> pair (class, ((intro, (map Thm.prop_of axioms, axioms)), cs))))))
   9.125 -  end;
   9.126 -
   9.127 -
   9.128 -(* instances with implicit parameter handling *)
   9.129 -
   9.130 -local
   9.131 -
   9.132 -fun gen_read_def thy prep_att read_def ((raw_name, raw_atts), raw_t) =
   9.133 -  let
   9.134 -    val (_, t) = read_def thy (raw_name, raw_t);
   9.135 -    val ((c, ty), _) = Sign.cert_def (Sign.pp thy) t;
   9.136 -    val atts = map (prep_att thy) raw_atts;
   9.137 -    val insts = Consts.typargs (Sign.consts_of thy) (c, ty);
   9.138 -    val name = case raw_name
   9.139 -     of "" => NONE
   9.140 -      | _ => SOME raw_name;
   9.141 -  in (c, (insts, ((name, t), atts))) end;
   9.142 -
   9.143 -fun read_def_cmd thy = gen_read_def thy Attrib.intern_src Theory.read_axm;
   9.144 -fun read_def thy = gen_read_def thy (K I) (K I);
   9.145 -
   9.146 -fun gen_instance_arity prep_arity read_def do_proof raw_arities raw_defs theory =
   9.147 -  let
   9.148 -    val arities = map (prep_arity theory) raw_arities;
   9.149 -    val _ = if null arities then error "at least one arity must be given" else ();
   9.150 -    val _ = case (duplicates (op =) o map #1) arities
   9.151 -     of [] => ()
   9.152 -      | dupl_tycos => error ("type constructors occur more than once in arities: "
   9.153 -          ^ (commas o map quote) dupl_tycos);
   9.154 -    val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra o Sign.classes_of) theory
   9.155 -    fun get_consts_class tyco ty class =
   9.156 -      let
   9.157 -        val cs = (these o Option.map snd o try (AxClass.params_of_class theory)) class;
   9.158 -        val subst_ty = map_type_tfree (K ty);
   9.159 -      in
   9.160 -        map (fn (c, ty) => (c, ((tyco, class), subst_ty ty))) cs
   9.161 -      end;
   9.162 -    fun get_consts_sort (tyco, asorts, sort) =
   9.163 -      let
   9.164 -        val ty = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) (Name.names Name.context "'a" asorts))
   9.165 -      in maps (get_consts_class tyco ty) (super_sort sort) end;
   9.166 -    val cs = maps get_consts_sort arities;
   9.167 -    fun mk_typnorm thy (ty, ty_sc) =
   9.168 -      case try (Sign.typ_match thy (Logic.varifyT ty_sc, ty)) Vartab.empty
   9.169 -       of SOME env => SOME (Logic.varifyT #> Envir.typ_subst_TVars env #> Logic.unvarifyT)
   9.170 -        | NONE => NONE;
   9.171 -    fun read_defs defs cs thy_read =
   9.172 -      let
   9.173 -        fun read raw_def cs =
   9.174 -          let
   9.175 -            val (c, (inst, ((name_opt, t), atts))) = read_def thy_read raw_def;
   9.176 -            val ty = Consts.instance (Sign.consts_of thy_read) (c, inst);
   9.177 -            val ((tyco, class), ty') = case AList.lookup (op =) cs c
   9.178 -             of NONE => error ("illegal definition for constant " ^ quote c)
   9.179 -              | SOME class_ty => class_ty;
   9.180 -            val name = case name_opt
   9.181 -             of NONE => Thm.def_name (Logic.name_arity (tyco, [], c))
   9.182 -              | SOME name => name;
   9.183 -            val t' = case mk_typnorm thy_read (ty', ty)
   9.184 -             of NONE => error ("illegal definition for constant " ^
   9.185 -                  quote (c ^ "::" ^ setmp show_sorts true
   9.186 -                    (Sign.string_of_typ thy_read) ty))
   9.187 -              | SOME norm => map_types norm t
   9.188 -          in (((class, tyco), ((name, t'), atts)), AList.delete (op =) c cs) end;
   9.189 -      in fold_map read defs cs end;
   9.190 -    val (defs, _) = read_defs raw_defs cs
   9.191 -      (fold Sign.primitive_arity arities (Theory.copy theory));
   9.192 -    fun get_remove_contraint c thy =
   9.193 -      let
   9.194 -        val ty = Sign.the_const_constraint thy c;
   9.195 -      in
   9.196 -        thy
   9.197 -        |> Sign.add_const_constraint_i (c, NONE)
   9.198 -        |> pair (c, Logic.unvarifyT ty)
   9.199 -      end;
   9.200 -    fun add_defs defs thy =
   9.201 -      thy
   9.202 -      |> PureThy.add_defs_i true (map ((apsnd o map) (Attrib.attribute thy) o snd) defs)
   9.203 -      |-> (fn thms => pair (map fst defs ~~ thms));
   9.204 -    fun after_qed cs defs thy =
   9.205 -      thy
   9.206 -      |> fold Sign.add_const_constraint_i (map (apsnd SOME) cs)
   9.207 -      |> fold (CodegenData.add_func false o snd) defs;
   9.208 -  in
   9.209 -    theory
   9.210 -    |> fold_map get_remove_contraint (map fst cs |> distinct (op =))
   9.211 -    ||>> add_defs defs
   9.212 -    |-> (fn (cs, defs) => do_proof (after_qed cs defs) arities)
   9.213 -  end;
   9.214 -
   9.215 -fun instance_arity_cmd' do_proof = gen_instance_arity Sign.read_arity read_def_cmd do_proof;
   9.216 -fun instance_arity' do_proof = gen_instance_arity Sign.cert_arity read_def do_proof;
   9.217 -fun tactic_proof tac after_qed arities =
   9.218 -  fold (fn arity => AxClass.prove_arity arity tac) arities
   9.219 -  #> after_qed;
   9.220 -
   9.221 -in
   9.222 -
   9.223 -val instance_arity_cmd = instance_arity_cmd' axclass_instance_arity;
   9.224 -val instance_arity = instance_arity' axclass_instance_arity;
   9.225 -val prove_instance_arity = instance_arity' o tactic_proof;
   9.226 -
   9.227 -end; (*local*)
   9.228 -
   9.229 -
   9.230 -
   9.231 -(** combining locales and axclasses **)
   9.232 -
   9.233 -(* theory data *)
   9.234 -
   9.235 -datatype class_data = ClassData of {
   9.236 -  locale: string,
   9.237 -  consts: (string * string) list
   9.238 -    (*locale parameter ~> toplevel theory constant*),
   9.239 -  v: string option,
   9.240 -  intro: thm
   9.241 -} * thm list (*derived defs*);
   9.242 -
   9.243 -fun rep_classdata (ClassData c) = c;
   9.244 -
   9.245 -fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2));
   9.246 -
   9.247 -structure ClassData = TheoryDataFun
   9.248 -(
   9.249 -  type T = class_data Graph.T * class Symtab.table (*locale name ~> class name*);
   9.250 -  val empty = (Graph.empty, Symtab.empty);
   9.251 -  val copy = I;
   9.252 -  val extend = I;
   9.253 -  fun merge _ = merge_pair (Graph.merge (K true)) (Symtab.merge (K true));
   9.254 -);
   9.255 -
   9.256 -
   9.257 -(* queries *)
   9.258 -
   9.259 -val lookup_class_data = Option.map rep_classdata oo try o Graph.get_node o fst o ClassData.get;
   9.260 -fun class_of_locale thy = Symtab.lookup ((snd o ClassData.get) thy);
   9.261 -
   9.262 -fun the_class_data thy class =
   9.263 -  case lookup_class_data thy class
   9.264 -    of NONE => error ("undeclared class " ^ quote class)
   9.265 -     | SOME data => data;
   9.266 -
   9.267 -val ancestry = Graph.all_succs o fst o ClassData.get;
   9.268 -
   9.269 -fun param_map thy =
   9.270 -  let
   9.271 -    fun params class =
   9.272 -      let
   9.273 -        val const_typs = (#params o AxClass.get_definition thy) class;
   9.274 -        val const_names = (#consts o fst o the_class_data thy) class;
   9.275 -      in
   9.276 -        (map o apsnd) (fn c => (c, (the o AList.lookup (op =) const_typs) c)) const_names
   9.277 -      end;
   9.278 -  in maps params o ancestry thy end;
   9.279 -
   9.280 -fun these_defs thy = maps (these o Option.map snd o lookup_class_data thy) o ancestry thy;
   9.281 -
   9.282 -fun these_intros thy =
   9.283 -  Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o fst o rep_classdata) data))
   9.284 -    ((fst o ClassData.get) thy) [];
   9.285 -
   9.286 -fun print_classes thy =
   9.287 -  let
   9.288 -    val algebra = Sign.classes_of thy;
   9.289 -    val arities =
   9.290 -      Symtab.empty
   9.291 -      |> Symtab.fold (fn (tyco, arities) => fold (fn (class, _) =>
   9.292 -           Symtab.map_default (class, []) (insert (op =) tyco)) arities)
   9.293 -             ((#arities o Sorts.rep_algebra) algebra);
   9.294 -    val the_arities = these o Symtab.lookup arities;
   9.295 -    fun mk_arity class tyco =
   9.296 -      let
   9.297 -        val Ss = Sorts.mg_domain algebra tyco [class];
   9.298 -      in Sign.pretty_arity thy (tyco, Ss, [class]) end;
   9.299 -    fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
   9.300 -      ^ setmp show_sorts false (Sign.string_of_typ thy o Type.strip_sorts) ty);
   9.301 -    fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
   9.302 -      (SOME o Pretty.str) ("class " ^ class ^ ":"),
   9.303 -      (SOME o Pretty.block) [Pretty.str "supersort: ",
   9.304 -        (Sign.pretty_sort thy o Sign.certify_sort thy o Sign.super_classes thy) class],
   9.305 -      Option.map (Pretty.str o prefix "locale: " o #locale o fst) (lookup_class_data thy class),
   9.306 -      ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param
   9.307 -        o these o Option.map #params o try (AxClass.get_definition thy)) class,
   9.308 -      (SOME o Pretty.block o Pretty.breaks) [
   9.309 -        Pretty.str "instances:",
   9.310 -        Pretty.list "" "" (map (mk_arity class) (the_arities class))
   9.311 -      ]
   9.312 -    ]
   9.313 -  in
   9.314 -    (Pretty.writeln o Pretty.chunks o separate (Pretty.str "") o map mk_entry o Sorts.all_classes)
   9.315 -      algebra
   9.316 -  end;
   9.317 -
   9.318 -
   9.319 -(* updaters *)
   9.320 -
   9.321 -fun add_class_data ((class, superclasses), (locale, consts, v, intro)) =
   9.322 -  ClassData.map (fn (gr, tab) => (
   9.323 -    gr
   9.324 -    |> Graph.new_node (class, ClassData ({ locale = locale, consts = consts,
   9.325 -         v = v, intro = intro }, []))
   9.326 -    |> fold (curry Graph.add_edge class) superclasses,
   9.327 -    tab
   9.328 -    |> Symtab.update (locale, class)
   9.329 -  ));
   9.330 -
   9.331 -fun add_class_const_thm (class, thm) = (ClassData.map o apfst o Graph.map_node class)
   9.332 -  (fn ClassData (data, thms) => ClassData (data, thm :: thms));
   9.333 -
   9.334 -(* tactics and methods *)
   9.335 -
   9.336 -fun intro_classes_tac facts st =
   9.337 -  let
   9.338 -    val thy = Thm.theory_of_thm st;
   9.339 -    val classes = Sign.all_classes thy;
   9.340 -    val class_trivs = map (Thm.class_triv thy) classes;
   9.341 -    val class_intros = these_intros thy;
   9.342 -    fun add_axclass_intro class =
   9.343 -      case try (AxClass.get_definition thy) class of SOME {intro, ...} => cons intro | _ => I;
   9.344 -    val axclass_intros = fold add_axclass_intro classes [];
   9.345 -  in
   9.346 -    st
   9.347 -    |> ((ALLGOALS (Method.insert_tac facts THEN'
   9.348 -          REPEAT_ALL_NEW (resolve_tac (class_trivs @ class_intros @ axclass_intros))))
   9.349 -            THEN Tactic.distinct_subgoals_tac)
   9.350 -  end;
   9.351 -
   9.352 -fun default_intro_classes_tac [] = intro_classes_tac []
   9.353 -  | default_intro_classes_tac _ = Tactical.no_tac;    (*no error message!*)
   9.354 -
   9.355 -fun default_tac rules ctxt facts =
   9.356 -  HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
   9.357 -    default_intro_classes_tac facts;
   9.358 -
   9.359 -val _ = Context.add_setup (Method.add_methods
   9.360 - [("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
   9.361 -    "back-chain introduction rules of classes"),
   9.362 -  ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac),
   9.363 -    "apply some intro/elim rule")]);
   9.364 -
   9.365 -
   9.366 -(* tactical interfaces to locale commands *)
   9.367 -
   9.368 -fun prove_interpretation tac prfx_atts expr insts thy =
   9.369 -  thy
   9.370 -  |> Locale.interpretation_i I prfx_atts expr insts
   9.371 -  |> Proof.global_terminal_proof (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
   9.372 -  |> ProofContext.theory_of;
   9.373 -
   9.374 -fun prove_interpretation_in tac after_qed (name, expr) thy =
   9.375 -  thy
   9.376 -  |> Locale.interpretation_in_locale (ProofContext.theory after_qed) (name, expr)
   9.377 -  |> Proof.global_terminal_proof (Method.Basic (K (Method.SIMPLE_METHOD tac), Position.none), NONE)
   9.378 -  |> ProofContext.theory_of;
   9.379 -
   9.380 -
   9.381 -(* constructing class introduction and other rules from axclass and locale rules *)
   9.382 -
   9.383 -fun mk_instT class = Symtab.empty
   9.384 -  |> Symtab.update (AxClass.param_tyvarname, TFree (AxClass.param_tyvarname, [class]));
   9.385 -
   9.386 -fun mk_inst class param_names cs =
   9.387 -  Symtab.empty
   9.388 -  |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
   9.389 -       (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;
   9.390 -
   9.391 -fun OF_LAST thm1 thm2 =
   9.392 -  let
   9.393 -    val n = (length o Logic.strip_imp_prems o prop_of) thm2;
   9.394 -  in (thm1 RSN (n, thm2)) end;
   9.395 -
   9.396 -fun strip_all_ofclass thy sort =
   9.397 -  let
   9.398 -    val typ = TVar ((AxClass.param_tyvarname, 0), sort);
   9.399 -    fun prem_inclass t =
   9.400 -      case Logic.strip_imp_prems t
   9.401 -       of ofcls :: _ => try Logic.dest_inclass ofcls
   9.402 -        | [] => NONE;
   9.403 -    fun strip_ofclass class thm =
   9.404 -      thm OF (fst o AxClass.of_sort thy (typ, [class])) AxClass.cache;
   9.405 -    fun strip thm = case (prem_inclass o Thm.prop_of) thm
   9.406 -     of SOME (_, class) => thm |> strip_ofclass class |> strip
   9.407 -      | NONE => thm;
   9.408 -  in strip end;
   9.409 -
   9.410 -fun class_intro thy locale class sups =
   9.411 -  let
   9.412 -    fun class_elim class =
   9.413 -      case (map Drule.unconstrainTs o #axioms o AxClass.get_definition thy) class
   9.414 -       of [thm] => SOME thm
   9.415 -        | [] => NONE;
   9.416 -    val pred_intro = case Locale.intros thy locale
   9.417 -     of ([ax_intro], [intro]) => intro |> OF_LAST ax_intro |> SOME
   9.418 -      | ([intro], []) => SOME intro
   9.419 -      | ([], [intro]) => SOME intro
   9.420 -      | _ => NONE;
   9.421 -    val pred_intro' = pred_intro
   9.422 -      |> Option.map (fn intro => intro OF map_filter class_elim sups);
   9.423 -    val class_intro = (#intro o AxClass.get_definition thy) class;
   9.424 -    val raw_intro = case pred_intro'
   9.425 -     of SOME pred_intro => class_intro |> OF_LAST pred_intro
   9.426 -      | NONE => class_intro;
   9.427 -    val sort = Sign.super_classes thy class;
   9.428 -    val typ = TVar ((AxClass.param_tyvarname, 0), sort);
   9.429 -    val defs = these_defs thy sups;
   9.430 -  in
   9.431 -    raw_intro
   9.432 -    |> Drule.instantiate' [SOME (Thm.ctyp_of thy typ)] []
   9.433 -    |> strip_all_ofclass thy sort
   9.434 -    |> Thm.strip_shyps
   9.435 -    |> MetaSimplifier.rewrite_rule defs
   9.436 -    |> Drule.unconstrainTs
   9.437 -  end;
   9.438 -
   9.439 -fun interpretation_in_rule thy (class1, class2) =
   9.440 -  let
   9.441 -    val (params, consts) = split_list (param_map thy [class1]);
   9.442 -    (*FIXME also remember this at add_class*)
   9.443 -    fun mk_axioms class =
   9.444 -      let
   9.445 -        val name_locale = (#locale o fst o the_class_data thy) class;
   9.446 -        val inst = mk_inst class params consts;
   9.447 -      in
   9.448 -        Locale.global_asms_of thy name_locale
   9.449 -        |> maps snd
   9.450 -        |> (map o map_aterms) (fn Free (s, _) => (the o Symtab.lookup inst) s | t => t)
   9.451 -        |> (map o map_types o map_atyps) (fn TFree _ => TFree ("'a", [class1]) | T => T)
   9.452 -        |> map (ObjectLogic.ensure_propT thy)
   9.453 -      end;
   9.454 -    val (prems, concls) = pairself mk_axioms (class1, class2);
   9.455 -  in
   9.456 -    Goal.prove_global thy [] prems (Logic.mk_conjunction_list concls)
   9.457 -      (Locale.intro_locales_tac true (ProofContext.init thy))
   9.458 -  end;
   9.459 -
   9.460 -
   9.461 -(* classes *)
   9.462 -
   9.463 -local
   9.464 -
   9.465 -fun read_param thy raw_t =
   9.466 -  let
   9.467 -    val t = Sign.read_term thy raw_t
   9.468 -  in case try dest_Const t
   9.469 -   of SOME (c, _) => c
   9.470 -    | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
   9.471 -  end;
   9.472 -
   9.473 -fun gen_class add_locale prep_class prep_param bname
   9.474 -    raw_supclasses raw_elems raw_other_consts thy =
   9.475 -  let
   9.476 -    (*FIXME need proper concept for reading locale statements*)
   9.477 -    fun subst_classtyvar (_, _) =
   9.478 -          TFree (AxClass.param_tyvarname, [])
   9.479 -      | subst_classtyvar (v, sort) =
   9.480 -          error ("Sort constraint illegal in type class, for type variable " ^ v ^ "::" ^ Sign.string_of_sort thy sort);
   9.481 -    (*val subst_classtyvars = Element.map_ctxt {name = I, var = I, term = I,
   9.482 -      typ = Term.map_type_tfree subst_classtyvar, fact = I, attrib = I};*)
   9.483 -    val other_consts = map (prep_param thy) raw_other_consts;
   9.484 -    val (elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
   9.485 -      | Locale.Expr i => apsnd (cons i)) raw_elems ([], []);
   9.486 -    val supclasses = map (prep_class thy) raw_supclasses;
   9.487 -    val sups = filter (is_some o lookup_class_data thy) supclasses
   9.488 -      |> Sign.certify_sort thy;
   9.489 -    val supsort = Sign.certify_sort thy supclasses;
   9.490 -    val suplocales = map (Locale.Locale o #locale o fst o the_class_data thy) sups;
   9.491 -    val supexpr = Locale.Merge (suplocales @ includes);
   9.492 -    val supparams = (map fst o Locale.parameters_of_expr thy)
   9.493 -      (Locale.Merge suplocales);
   9.494 -    val supconsts = AList.make (the o AList.lookup (op =) (param_map thy sups))
   9.495 -      (map fst supparams);
   9.496 -    (*val elems_constrains = map
   9.497 -      (Element.Constrains o apsnd (Term.map_type_tfree subst_classtyvar)) supparams;*)
   9.498 -    fun mk_tyvar (_, sort) = TFree (AxClass.param_tyvarname,
   9.499 -      if Sign.subsort thy (supsort, sort) then sort else error
   9.500 -        ("Sort " ^ Sign.string_of_sort thy sort
   9.501 -          ^ " is less general than permitted least general sort "
   9.502 -          ^ Sign.string_of_sort thy supsort));
   9.503 -    fun extract_params thy name_locale =
   9.504 -      let
   9.505 -        val params = Locale.parameters_of thy name_locale;
   9.506 -        val v = case (maps typ_tfrees o map (snd o fst)) params
   9.507 -         of (v, _) :: _ => SOME v
   9.508 -          | _ => NONE;
   9.509 -      in
   9.510 -        (v, (map (fst o fst) params, params
   9.511 -        |> (map o apfst o apsnd o Term.map_type_tfree) mk_tyvar
   9.512 -        |> (map o apsnd) (fork_mixfix true NONE #> fst)
   9.513 -        |> chop (length supconsts)
   9.514 -        |> snd))
   9.515 -      end;
   9.516 -    fun extract_assumes name_locale params thy cs =
   9.517 -      let
   9.518 -        val consts = supconsts @ (map (fst o fst) params ~~ cs);
   9.519 -        fun subst (Free (c, ty)) =
   9.520 -              Const ((fst o the o AList.lookup (op =) consts) c, ty)
   9.521 -          | subst t = t;
   9.522 -        val super_defs = these_defs thy sups;
   9.523 -        fun prep_asm ((name, atts), ts) =
   9.524 -          ((NameSpace.base name, map (Attrib.attribute thy) atts),
   9.525 -            (map o map_aterms) ((*MetaSimplifier.rewrite_term thy super_defs [] o *)subst) ts);
   9.526 -      in
   9.527 -        Locale.global_asms_of thy name_locale
   9.528 -        |> map prep_asm
   9.529 -      end;
   9.530 -    fun note_intro name_axclass class_intro =
   9.531 -      PureThy.note_thmss_qualified "" ((Logic.const_of_class o NameSpace.base) name_axclass)
   9.532 -        [(("intro", []), [([class_intro], [])])]
   9.533 -      #> snd
   9.534 -  in
   9.535 -    thy
   9.536 -    |> add_locale (SOME "") bname supexpr ((*elems_constrains @*) elems)
   9.537 -    |-> (fn name_locale => ProofContext.theory_result (
   9.538 -      `(fn thy => extract_params thy name_locale)
   9.539 -      #-> (fn (v, (param_names, params)) =>
   9.540 -        axclass_params (bname, supsort) params (extract_assumes name_locale params) other_consts
   9.541 -      #-> (fn (name_axclass, ((_, (ax_terms, ax_axioms)), consts)) =>
   9.542 -        `(fn thy => class_intro thy name_locale name_axclass sups)
   9.543 -      #-> (fn class_intro =>
   9.544 -        add_class_data ((name_axclass, sups),
   9.545 -          (name_locale, map (fst o fst) params ~~ map fst consts, v,
   9.546 -            class_intro))
   9.547 -        (*FIXME: class_data should already contain data relevant
   9.548 -          for interpretation; use this later for class target*)
   9.549 -        (*FIXME: general export_fixes which may be parametrized
   9.550 -          with pieces of an emerging class*)
   9.551 -      #> note_intro name_axclass class_intro
   9.552 -      #> prove_interpretation ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
   9.553 -          ((false, Logic.const_of_class bname), []) (Locale.Locale name_locale)
   9.554 -          ((mk_instT name_axclass, mk_inst name_axclass param_names (map snd supconsts @ consts)), [])
   9.555 -      #> pair name_axclass
   9.556 -      )))))
   9.557 -  end;
   9.558 -
   9.559 -in
   9.560 -
   9.561 -val class_cmd = gen_class Locale.add_locale Sign.intern_class read_param;
   9.562 -val class = gen_class Locale.add_locale_i Sign.certify_class (K I);
   9.563 -
   9.564 -end; (*local*)
   9.565 -
   9.566 -local
   9.567 -
   9.568 -fun singular_instance_subclass (class1, class2) thy  =
   9.569 -  let
   9.570 -    val interp = interpretation_in_rule thy (class1, class2);
   9.571 -    val ax = #axioms (AxClass.get_definition thy class1);
   9.572 -    val intro = #intro (AxClass.get_definition thy class2)
   9.573 -      |> Drule.instantiate' [SOME (Thm.ctyp_of thy
   9.574 -          (TVar ((AxClass.param_tyvarname, 0), [class1])))] [];
   9.575 -    val thm = 
   9.576 -      intro
   9.577 -      |> OF_LAST (interp OF ax)
   9.578 -      |> strip_all_ofclass thy (Sign.super_classes thy class2);
   9.579 -  in
   9.580 -    thy |> AxClass.add_classrel thm
   9.581 -  end;
   9.582 -
   9.583 -fun instance_subsort (class, sort) thy =
   9.584 -  let
   9.585 -    val super_sort = (Graph.all_succs o #classes o Sorts.rep_algebra
   9.586 -      o Sign.classes_of) thy sort;
   9.587 -    val classes = filter_out (fn class' => Sign.subsort thy ([class], [class']))
   9.588 -      (rev super_sort);
   9.589 -  in
   9.590 -    thy |> fold (curry singular_instance_subclass class) classes
   9.591 -  end;
   9.592 -
   9.593 -fun instance_sort' do_proof (class, sort) theory =
   9.594 -  let
   9.595 -    val loc_name = (#locale o fst o the_class_data theory) class;
   9.596 -    val loc_expr =
   9.597 -      (Locale.Merge o map (Locale.Locale o #locale o fst o the_class_data theory)) sort;
   9.598 -  in
   9.599 -    theory
   9.600 -    |> do_proof (instance_subsort (class, sort)) (loc_name, loc_expr)
   9.601 -  end;
   9.602 -
   9.603 -fun gen_instance_sort prep_class prep_sort (raw_class, raw_sort) theory =
   9.604 -  let
   9.605 -    val class = prep_class theory raw_class;
   9.606 -    val sort = prep_sort theory raw_sort;
   9.607 -  in
   9.608 -    theory
   9.609 -    |> instance_sort' (Locale.interpretation_in_locale o ProofContext.theory) (class, sort)
   9.610 -  end;
   9.611 -
   9.612 -fun gen_instance_class prep_class (raw_class, raw_superclass) theory =
   9.613 -  let
   9.614 -    val class = prep_class theory raw_class;
   9.615 -    val superclass = prep_class theory raw_superclass;
   9.616 -  in
   9.617 -    theory
   9.618 -    |> axclass_instance_sort (class, superclass)
   9.619 -  end;
   9.620 -
   9.621 -in
   9.622 -
   9.623 -val instance_sort_cmd = gen_instance_sort Sign.read_class Sign.read_sort;
   9.624 -val instance_sort = gen_instance_sort Sign.certify_class Sign.certify_sort;
   9.625 -val prove_instance_sort = instance_sort' o prove_interpretation_in;
   9.626 -val instance_class_cmd = gen_instance_class Sign.read_class;
   9.627 -val instance_class = gen_instance_class Sign.certify_class;
   9.628 -
   9.629 -end; (*local*)
   9.630 -
   9.631 -
   9.632 -(** class target **)
   9.633 -
   9.634 -fun export_fixes thy class =
   9.635 -  let
   9.636 -    val v = (#v o fst o the_class_data thy) class;
   9.637 -    val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) [class];
   9.638 -    val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
   9.639 -      if SOME w = v then TFree (w, constrain_sort sort) else TFree var);
   9.640 -    val consts = param_map thy [class];
   9.641 -    fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) consts v
   9.642 -         of SOME (c, _) => Const (c, ty)
   9.643 -          | NONE => t)
   9.644 -      | subst_aterm t = t;
   9.645 -  in map_types subst_typ #> Term.map_aterms subst_aterm end;
   9.646 -
   9.647 -fun add_const_in_class class ((c, rhs), syn) thy =
   9.648 -  let
   9.649 -    val prfx = (Logic.const_of_class o NameSpace.base) class;
   9.650 -    fun mk_name inject c =
   9.651 -      let
   9.652 -        val n1 = Sign.full_name thy c;
   9.653 -        val n2 = NameSpace.qualifier n1;
   9.654 -        val n3 = NameSpace.base n1;
   9.655 -      in NameSpace.implode (n2 :: inject @ [n3]) end;
   9.656 -    val abbr' = mk_name [prfx, prfx] c;
   9.657 -    val rhs' = export_fixes thy class rhs;
   9.658 -    val ty' = Term.fastype_of rhs';
   9.659 -    val def = (c, Logic.mk_equals (Const (mk_name [prfx] c, ty'), rhs'));
   9.660 -    val (syn', _) = fork_mixfix true NONE syn;
   9.661 -    fun interpret def =
   9.662 -      let
   9.663 -        val def' = symmetric def
   9.664 -        val tac = (ALLGOALS o ProofContext.fact_tac) [def'];
   9.665 -        val name_locale = (#locale o fst o the_class_data thy) class;
   9.666 -        val def_eq = Thm.prop_of def';
   9.667 -        val (params, consts) = split_list (param_map thy [class]);
   9.668 -      in
   9.669 -        prove_interpretation tac ((false, prfx), []) (Locale.Locale name_locale)
   9.670 -          ((mk_instT class, mk_inst class params consts), [def_eq])
   9.671 -        #> add_class_const_thm (class, def')
   9.672 -      end;
   9.673 -  in
   9.674 -    thy
   9.675 -    |> Sign.hide_consts_i true [abbr']
   9.676 -    |> Sign.add_path prfx
   9.677 -    |> Sign.add_consts_authentic [(c, ty', syn')]
   9.678 -    |> Sign.parent_path
   9.679 -    |> Sign.sticky_prefix prfx
   9.680 -    |> PureThy.add_defs_i false [(def, [])]
   9.681 -    |-> (fn [def] => interpret def)
   9.682 -    |> Sign.restore_naming thy
   9.683 -  end;
   9.684 -
   9.685 -
   9.686 -(** experimental interpretation_in **)
   9.687 -
   9.688 -
   9.689 -end;