# HG changeset patch
# User haftmann
# Date 1174375635 -3600
# Node ID 753123c89d721298c3e463a051e8199b8f083ebc
# Parent  bfd9c0fd70b1e88900b1a606a3f88a97a4b8f40f
explizit "type" superclass

diff -r bfd9c0fd70b1 -r 753123c89d72 doc-src/IsarAdvanced/Classes/Thy/Classes.thy
--- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Mon Mar 19 19:28:27 2007 +0100
+++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Tue Mar 20 08:27:15 2007 +0100
@@ -161,7 +161,7 @@
   assumed to be associative:
 *}
 
-    class semigroup =
+    class semigroup = type +
       fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"    (infixl "\<^loc>\<otimes>" 70)
       assumes assoc: "(x \<^loc>\<otimes> y) \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)"
 
@@ -333,7 +333,7 @@
   is nothing else than a locale:
 *}
 
-class idem =
+class idem = type +
   fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
   assumes idem: "f (f x) = f x"
 
diff -r bfd9c0fd70b1 -r 753123c89d72 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon Mar 19 19:28:27 2007 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Mar 20 08:27:15 2007 +0100
@@ -141,12 +141,10 @@
   most cases code generation proceeds without further ado:
 *}
 
-consts
-  fac :: "nat \<Rightarrow> nat"
-
-primrec
-  "fac 0 = 1"
-  "fac (Suc n) = Suc n * fac n"
+fun
+  fac :: "nat \<Rightarrow> nat" where
+    "fac 0 = 1"
+  | "fac (Suc n) = Suc n * fac n"
 
 text {*
   This executable specification is now turned to SML code:
@@ -324,7 +322,7 @@
   assigning to each of its inhabitants a \qt{null} value:
 *}
 
-class null =
+class null = type +
   fixes null :: 'a
 
 consts
@@ -551,9 +549,6 @@
 fun
   in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
   "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
-(*<*)
-declare in_interval.simps [code func]
-(*>*)
 
 (*<*)
 code_type %tt bool
@@ -716,15 +711,12 @@
 
 fun
   collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-  "collect_duplicates xs ys [] = xs"
-  "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
-    then if z \<in> set ys
-      then collect_duplicates xs ys zs
-      else collect_duplicates xs (z#ys) zs
-    else collect_duplicates (z#xs) (z#ys) zs)"
-(*<*)
-lemmas [code func] = collect_duplicates.simps
-(*>*)
+    "collect_duplicates xs ys [] = xs"
+  | "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
+      then if z \<in> set ys
+        then collect_duplicates xs ys zs
+        else collect_duplicates xs (z#ys) zs
+      else collect_duplicates (z#xs) (z#ys) zs)"
 
 text {*
   The membership test during preprocessing is rewritten,
@@ -749,7 +741,7 @@
 consts "op =" :: "'a"
 (*>*)
 
-class eq (attach "op =") = notes reflexive
+class eq (attach "op =") = type
 
 text {*
   This merely introduces a class @{text eq} with corresponding
@@ -782,11 +774,8 @@
 
 fun
   lookup :: "(key \<times> 'a) list \<Rightarrow> key \<Rightarrow> 'a option" where
-  "lookup [] l = None"
-  "lookup ((k, v) # xs) l = (if k = l then Some v else lookup xs l)"
-(*<*)
-lemmas [code func] = lookup.simps
-(*>*)
+    "lookup [] l = None"
+  | "lookup ((k, v) # xs) l = (if k = l then Some v else lookup xs l)"
 
 code_type %tt key
   (SML "string")
@@ -883,7 +872,7 @@
 
 (*<*)
 setup {* Sign.add_path "bar" *}
-class eq = fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+class eq = type + fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
 (*>*)
 
 code_class %tt eq
@@ -1091,11 +1080,8 @@
 
 fun
   dummy_option :: "'a list \<Rightarrow> 'a option" where
-  "dummy_option (x#xs) = Some x"
-  "dummy_option [] = arbitrary"
-(*<*)
-declare dummy_option.simps [code func]
-(*>*)
+    "dummy_option (x#xs) = Some x"
+  | "dummy_option [] = arbitrary"
 
 code_gen dummy_option (*<*)(SML #)(*>*)(SML "examples/arbitrary.ML")
 
diff -r bfd9c0fd70b1 -r 753123c89d72 src/HOL/Code_Generator.thy
--- a/src/HOL/Code_Generator.thy	Mon Mar 19 19:28:27 2007 +0100
+++ b/src/HOL/Code_Generator.thy	Tue Mar 20 08:27:15 2007 +0100
@@ -75,7 +75,7 @@
 
 text {* operational equality for code generation *}
 
-class eq (attach "op =") = notes reflexive
+class eq (attach "op =") = type
 
 
 text {* equality for Haskell *}
diff -r bfd9c0fd70b1 -r 753123c89d72 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Mon Mar 19 19:28:27 2007 +0100
+++ b/src/HOL/Divides.thy	Tue Mar 20 08:27:15 2007 +0100
@@ -12,7 +12,7 @@
 
 (*We use the same class for div and mod;
   moreover, dvd is defined whenever multiplication is*)
-class div =
+class div = type +
   fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
   fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
 begin
diff -r bfd9c0fd70b1 -r 753123c89d72 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Mar 19 19:28:27 2007 +0100
+++ b/src/HOL/Finite_Set.thy	Tue Mar 20 08:27:15 2007 +0100
@@ -2533,7 +2533,7 @@
 
 subsection {* Class @{text finite} *}
 
-class finite (attach UNIV) =
+class finite (attach UNIV) = type +
   assumes finite: "finite UNIV"
 
 lemma finite_set: "finite (A::'a::finite set)"
diff -r bfd9c0fd70b1 -r 753123c89d72 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Mon Mar 19 19:28:27 2007 +0100
+++ b/src/HOL/HOL.thy	Tue Mar 20 08:27:15 2007 +0100
@@ -179,26 +179,26 @@
 
 subsubsection {* Generic algebraic operations *}
 
-class zero =
+class zero = type + 
   fixes zero :: "'a"  ("\<^loc>0")
 
-class one =
+class one = type +
   fixes one  :: "'a"  ("\<^loc>1")
 
 hide (open) const zero one
 
-class plus =
+class plus = type +
   fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>+" 65)
 
-class minus =
+class minus = type +
   fixes uminus :: "'a \<Rightarrow> 'a" 
     and minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>-" 65)
     and abs :: "'a \<Rightarrow> 'a"
 
-class times =
+class times = type +
   fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>*" 70)
 
-class inverse = 
+class inverse = type +
   fixes inverse :: "'a \<Rightarrow> 'a"
     and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>'/" 70)
 
diff -r bfd9c0fd70b1 -r 753123c89d72 src/HOL/Integ/Numeral.thy
--- a/src/HOL/Integ/Numeral.thy	Mon Mar 19 19:28:27 2007 +0100
+++ b/src/HOL/Integ/Numeral.thy	Tue Mar 20 08:27:15 2007 +0100
@@ -42,7 +42,7 @@
   Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
   "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
 
-class number = -- {* for numeric types: nat, int, real, \dots *}
+class number = type + -- {* for numeric types: nat, int, real, \dots *}
   fixes number_of :: "int \<Rightarrow> 'a"
 
 syntax
diff -r bfd9c0fd70b1 -r 753123c89d72 src/HOL/Library/Kleene_Algebras.thy
--- a/src/HOL/Library/Kleene_Algebras.thy	Mon Mar 19 19:28:27 2007 +0100
+++ b/src/HOL/Library/Kleene_Algebras.thy	Tue Mar 20 08:27:15 2007 +0100
@@ -9,7 +9,7 @@
 
 text {* A type class of kleene algebras *}
 
-class star = 
+class star = type +
   fixes star :: "'a \<Rightarrow> 'a"
 
 class idem_add = ab_semigroup_add +
diff -r bfd9c0fd70b1 -r 753123c89d72 src/HOL/Library/Parity.thy
--- a/src/HOL/Library/Parity.thy	Mon Mar 19 19:28:27 2007 +0100
+++ b/src/HOL/Library/Parity.thy	Tue Mar 20 08:27:15 2007 +0100
@@ -9,7 +9,7 @@
 imports Main
 begin
 
-class even_odd =
+class even_odd = type + 
   fixes even :: "'a \<Rightarrow> bool"
 
 abbreviation
diff -r bfd9c0fd70b1 -r 753123c89d72 src/HOL/Library/Quotient.thy
--- a/src/HOL/Library/Quotient.thy	Mon Mar 19 19:28:27 2007 +0100
+++ b/src/HOL/Library/Quotient.thy	Tue Mar 20 08:27:15 2007 +0100
@@ -21,7 +21,7 @@
  "\<sim> :: 'a => 'a => bool"}.
 *}
 
-class eqv =
+class eqv = type +
   fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<^loc>\<sim>" 50)
 
 class equiv = eqv +
diff -r bfd9c0fd70b1 -r 753123c89d72 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Mar 19 19:28:27 2007 +0100
+++ b/src/HOL/Nat.thy	Tue Mar 20 08:27:15 2007 +0100
@@ -106,7 +106,7 @@
 
 text {* size of a datatype value *}
 
-class size =
+class size = type +
   fixes size :: "'a \<Rightarrow> nat"
 
 text {* @{typ nat} is a datatype *}
@@ -476,7 +476,7 @@
 
 subsection {* Arithmetic operators *}
 
-class power =
+class power = type +
   fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"            (infixr "\<^loc>^" 80)
 
 text {* arithmetic operators @{text "+ -"} and @{text "*"} *}
diff -r bfd9c0fd70b1 -r 753123c89d72 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Mar 19 19:28:27 2007 +0100
+++ b/src/HOL/Orderings.thy	Tue Mar 20 08:27:15 2007 +0100
@@ -11,7 +11,7 @@
 
 subsection {* Order syntax *}
 
-class ord =
+class ord = type +
   fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubseteq>" 50)
     and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubset>" 50)
 begin
diff -r bfd9c0fd70b1 -r 753123c89d72 src/HOL/ex/Classpackage.thy
--- a/src/HOL/ex/Classpackage.thy	Mon Mar 19 19:28:27 2007 +0100
+++ b/src/HOL/ex/Classpackage.thy	Tue Mar 20 08:27:15 2007 +0100
@@ -8,7 +8,7 @@
 imports Main
 begin
 
-class semigroup =
+class semigroup = type +
   fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>\<otimes>" 70)
   assumes assoc: "x \<^loc>\<otimes> y \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)"
 
diff -r bfd9c0fd70b1 -r 753123c89d72 src/HOL/ex/CodeCollections.thy
--- a/src/HOL/ex/CodeCollections.thy	Mon Mar 19 19:28:27 2007 +0100
+++ b/src/HOL/ex/CodeCollections.thy	Tue Mar 20 08:27:15 2007 +0100
@@ -74,7 +74,7 @@
   "list_ex P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)"
   by (induct xs) auto
 
-class finite =
+class finite = type +
   fixes fin :: "'a list"
   assumes member_fin: "x \<in> set fin"
 begin
diff -r bfd9c0fd70b1 -r 753123c89d72 src/HOL/ex/CodeEval.thy
--- a/src/HOL/ex/CodeEval.thy	Mon Mar 19 19:28:27 2007 +0100
+++ b/src/HOL/ex/CodeEval.thy	Tue Mar 20 08:27:15 2007 +0100
@@ -10,7 +10,7 @@
 
 subsection {* The typ_of class *}
 
-class typ_of =
+class typ_of = type +
   fixes typ_of :: "'a itself \<Rightarrow> typ"
 
 ML {*
diff -r bfd9c0fd70b1 -r 753123c89d72 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Mon Mar 19 19:28:27 2007 +0100
+++ b/src/Pure/Tools/class_package.ML	Tue Mar 20 08:27:15 2007 +0100
@@ -417,13 +417,8 @@
 
 local
 
-fun certify_class thy class =
-  tap (the_class_data thy) (Sign.certify_class thy class);
-
-fun read_class thy =
-  certify_class thy o Sign.intern_class thy;
-
-fun gen_class add_locale prep_class prep_param bname raw_supclasses raw_elems raw_other_consts thy =
+fun gen_class add_locale prep_class prep_param bname
+    raw_supclasses raw_elems raw_other_consts thy =
   let
     (*FIXME need proper concept for reading locale statements*)
     fun subst_classtyvar (_, _) =
@@ -436,25 +431,27 @@
     val (elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
       | Locale.Expr i => apsnd (cons i)) raw_elems ([], []);
     val supclasses = map (prep_class thy) raw_supclasses;
-    val supsort =
-      supclasses
-      |> Sign.certify_sort thy
-      |> (fn [] => Sign.defaultS thy | S => S); (*FIXME Why syntax defaultS?*)
-    val suplocales = map (Locale.Locale o #locale o the_class_data thy) supclasses;
+    val sups = filter (is_some o lookup_class_data thy) supclasses;
+    val supsort = Sign.certify_sort thy supclasses;
+    val suplocales = map (Locale.Locale o #locale o the_class_data thy) sups;
     val supexpr = Locale.Merge (suplocales @ includes);
     val supparams = (map fst o Locale.parameters_of_expr thy)
       (Locale.Merge suplocales);
-    val supconsts = AList.make
-      (the o AList.lookup (op =) (param_map thy supclasses)) (map fst supparams);
+    val supconsts = AList.make (the o AList.lookup (op =) (param_map thy sups))
+      (map fst supparams);
     (*val elems_constrains = map
       (Element.Constrains o apsnd (Term.map_type_tfree subst_classtyvar)) supparams;*)
+    fun mk_tyvar (_, sort) = TFree (AxClass.param_tyvarname,
+      if Sign.subsort thy (supsort, sort) then sort else error
+        ("Sort " ^ Sign.string_of_sort thy sort
+          ^ " is less general than permitted least general sort "
+          ^ Sign.string_of_sort thy supsort));
     fun extract_params thy name_locale =
-      let   
+      let
         val params = Locale.parameters_of thy name_locale;
       in
         (map (fst o fst) params, params
-        |> (map o apfst o apsnd o Term.map_type_tfree)
-             (K (TFree (AxClass.param_tyvarname, Sign.defaultS thy)))
+        |> (map o apfst o apsnd o Term.map_type_tfree) mk_tyvar
         |> (map o apsnd) (fork_mixfix true NONE #> fst)
         |> chop (length supconsts)
         |> snd)
@@ -493,7 +490,7 @@
       #-> (fn (name_axclass, ((_, (ax_terms, ax_axioms)), consts)) =>
         `(fn thy => extract_axiom_names thy name_locale)
       #-> (fn axiom_names =>
-        add_class_data ((name_axclass, supclasses),
+        add_class_data ((name_axclass, sups),
           (name_locale, map (fst o fst) params ~~ map fst consts,
             map2 make_witness ax_terms ax_axioms, axiom_names))
       #> prove_interpretation ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
@@ -505,8 +502,8 @@
 
 in
 
-val class_cmd = gen_class Locale.add_locale read_class AxClass.read_param;
-val class = gen_class Locale.add_locale_i certify_class (K I);
+val class_cmd = gen_class Locale.add_locale Sign.intern_class AxClass.read_param;
+val class = gen_class Locale.add_locale_i Sign.certify_class (K I);
 
 end; (*local*)