explizit "type" superclass
authorhaftmann
Tue Mar 20 08:27:15 2007 +0100 (2007-03-20)
changeset 22473753123c89d72
parent 22472 bfd9c0fd70b1
child 22474 ecdaec8cf13a
explizit "type" superclass
doc-src/IsarAdvanced/Classes/Thy/Classes.thy
doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
src/HOL/Code_Generator.thy
src/HOL/Divides.thy
src/HOL/Finite_Set.thy
src/HOL/HOL.thy
src/HOL/Integ/Numeral.thy
src/HOL/Library/Kleene_Algebras.thy
src/HOL/Library/Parity.thy
src/HOL/Library/Quotient.thy
src/HOL/Nat.thy
src/HOL/Orderings.thy
src/HOL/ex/Classpackage.thy
src/HOL/ex/CodeCollections.thy
src/HOL/ex/CodeEval.thy
src/Pure/Tools/class_package.ML
     1.1 --- a/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Mon Mar 19 19:28:27 2007 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Classes/Thy/Classes.thy	Tue Mar 20 08:27:15 2007 +0100
     1.3 @@ -161,7 +161,7 @@
     1.4    assumed to be associative:
     1.5  *}
     1.6  
     1.7 -    class semigroup =
     1.8 +    class semigroup = type +
     1.9        fixes mult :: "\<alpha> \<Rightarrow> \<alpha> \<Rightarrow> \<alpha>"    (infixl "\<^loc>\<otimes>" 70)
    1.10        assumes assoc: "(x \<^loc>\<otimes> y) \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)"
    1.11  
    1.12 @@ -333,7 +333,7 @@
    1.13    is nothing else than a locale:
    1.14  *}
    1.15  
    1.16 -class idem =
    1.17 +class idem = type +
    1.18    fixes f :: "\<alpha> \<Rightarrow> \<alpha>"
    1.19    assumes idem: "f (f x) = f x"
    1.20  
     2.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon Mar 19 19:28:27 2007 +0100
     2.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Tue Mar 20 08:27:15 2007 +0100
     2.3 @@ -141,12 +141,10 @@
     2.4    most cases code generation proceeds without further ado:
     2.5  *}
     2.6  
     2.7 -consts
     2.8 -  fac :: "nat \<Rightarrow> nat"
     2.9 -
    2.10 -primrec
    2.11 -  "fac 0 = 1"
    2.12 -  "fac (Suc n) = Suc n * fac n"
    2.13 +fun
    2.14 +  fac :: "nat \<Rightarrow> nat" where
    2.15 +    "fac 0 = 1"
    2.16 +  | "fac (Suc n) = Suc n * fac n"
    2.17  
    2.18  text {*
    2.19    This executable specification is now turned to SML code:
    2.20 @@ -324,7 +322,7 @@
    2.21    assigning to each of its inhabitants a \qt{null} value:
    2.22  *}
    2.23  
    2.24 -class null =
    2.25 +class null = type +
    2.26    fixes null :: 'a
    2.27  
    2.28  consts
    2.29 @@ -551,9 +549,6 @@
    2.30  fun
    2.31    in_interval :: "nat \<times> nat \<Rightarrow> nat \<Rightarrow> bool" where
    2.32    "in_interval (k, l) n \<longleftrightarrow> k \<le> n \<and> n \<le> l"
    2.33 -(*<*)
    2.34 -declare in_interval.simps [code func]
    2.35 -(*>*)
    2.36  
    2.37  (*<*)
    2.38  code_type %tt bool
    2.39 @@ -716,15 +711,12 @@
    2.40  
    2.41  fun
    2.42    collect_duplicates :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    2.43 -  "collect_duplicates xs ys [] = xs"
    2.44 -  "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
    2.45 -    then if z \<in> set ys
    2.46 -      then collect_duplicates xs ys zs
    2.47 -      else collect_duplicates xs (z#ys) zs
    2.48 -    else collect_duplicates (z#xs) (z#ys) zs)"
    2.49 -(*<*)
    2.50 -lemmas [code func] = collect_duplicates.simps
    2.51 -(*>*)
    2.52 +    "collect_duplicates xs ys [] = xs"
    2.53 +  | "collect_duplicates xs ys (z#zs) = (if z \<in> set xs
    2.54 +      then if z \<in> set ys
    2.55 +        then collect_duplicates xs ys zs
    2.56 +        else collect_duplicates xs (z#ys) zs
    2.57 +      else collect_duplicates (z#xs) (z#ys) zs)"
    2.58  
    2.59  text {*
    2.60    The membership test during preprocessing is rewritten,
    2.61 @@ -749,7 +741,7 @@
    2.62  consts "op =" :: "'a"
    2.63  (*>*)
    2.64  
    2.65 -class eq (attach "op =") = notes reflexive
    2.66 +class eq (attach "op =") = type
    2.67  
    2.68  text {*
    2.69    This merely introduces a class @{text eq} with corresponding
    2.70 @@ -782,11 +774,8 @@
    2.71  
    2.72  fun
    2.73    lookup :: "(key \<times> 'a) list \<Rightarrow> key \<Rightarrow> 'a option" where
    2.74 -  "lookup [] l = None"
    2.75 -  "lookup ((k, v) # xs) l = (if k = l then Some v else lookup xs l)"
    2.76 -(*<*)
    2.77 -lemmas [code func] = lookup.simps
    2.78 -(*>*)
    2.79 +    "lookup [] l = None"
    2.80 +  | "lookup ((k, v) # xs) l = (if k = l then Some v else lookup xs l)"
    2.81  
    2.82  code_type %tt key
    2.83    (SML "string")
    2.84 @@ -883,7 +872,7 @@
    2.85  
    2.86  (*<*)
    2.87  setup {* Sign.add_path "bar" *}
    2.88 -class eq = fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    2.89 +class eq = type + fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    2.90  (*>*)
    2.91  
    2.92  code_class %tt eq
    2.93 @@ -1091,11 +1080,8 @@
    2.94  
    2.95  fun
    2.96    dummy_option :: "'a list \<Rightarrow> 'a option" where
    2.97 -  "dummy_option (x#xs) = Some x"
    2.98 -  "dummy_option [] = arbitrary"
    2.99 -(*<*)
   2.100 -declare dummy_option.simps [code func]
   2.101 -(*>*)
   2.102 +    "dummy_option (x#xs) = Some x"
   2.103 +  | "dummy_option [] = arbitrary"
   2.104  
   2.105  code_gen dummy_option (*<*)(SML #)(*>*)(SML "examples/arbitrary.ML")
   2.106  
     3.1 --- a/src/HOL/Code_Generator.thy	Mon Mar 19 19:28:27 2007 +0100
     3.2 +++ b/src/HOL/Code_Generator.thy	Tue Mar 20 08:27:15 2007 +0100
     3.3 @@ -75,7 +75,7 @@
     3.4  
     3.5  text {* operational equality for code generation *}
     3.6  
     3.7 -class eq (attach "op =") = notes reflexive
     3.8 +class eq (attach "op =") = type
     3.9  
    3.10  
    3.11  text {* equality for Haskell *}
     4.1 --- a/src/HOL/Divides.thy	Mon Mar 19 19:28:27 2007 +0100
     4.2 +++ b/src/HOL/Divides.thy	Tue Mar 20 08:27:15 2007 +0100
     4.3 @@ -12,7 +12,7 @@
     4.4  
     4.5  (*We use the same class for div and mod;
     4.6    moreover, dvd is defined whenever multiplication is*)
     4.7 -class div =
     4.8 +class div = type +
     4.9    fixes div :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    4.10    fixes mod :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
    4.11  begin
     5.1 --- a/src/HOL/Finite_Set.thy	Mon Mar 19 19:28:27 2007 +0100
     5.2 +++ b/src/HOL/Finite_Set.thy	Tue Mar 20 08:27:15 2007 +0100
     5.3 @@ -2533,7 +2533,7 @@
     5.4  
     5.5  subsection {* Class @{text finite} *}
     5.6  
     5.7 -class finite (attach UNIV) =
     5.8 +class finite (attach UNIV) = type +
     5.9    assumes finite: "finite UNIV"
    5.10  
    5.11  lemma finite_set: "finite (A::'a::finite set)"
     6.1 --- a/src/HOL/HOL.thy	Mon Mar 19 19:28:27 2007 +0100
     6.2 +++ b/src/HOL/HOL.thy	Tue Mar 20 08:27:15 2007 +0100
     6.3 @@ -179,26 +179,26 @@
     6.4  
     6.5  subsubsection {* Generic algebraic operations *}
     6.6  
     6.7 -class zero =
     6.8 +class zero = type + 
     6.9    fixes zero :: "'a"  ("\<^loc>0")
    6.10  
    6.11 -class one =
    6.12 +class one = type +
    6.13    fixes one  :: "'a"  ("\<^loc>1")
    6.14  
    6.15  hide (open) const zero one
    6.16  
    6.17 -class plus =
    6.18 +class plus = type +
    6.19    fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>+" 65)
    6.20  
    6.21 -class minus =
    6.22 +class minus = type +
    6.23    fixes uminus :: "'a \<Rightarrow> 'a" 
    6.24      and minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>-" 65)
    6.25      and abs :: "'a \<Rightarrow> 'a"
    6.26  
    6.27 -class times =
    6.28 +class times = type +
    6.29    fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>*" 70)
    6.30  
    6.31 -class inverse = 
    6.32 +class inverse = type +
    6.33    fixes inverse :: "'a \<Rightarrow> 'a"
    6.34      and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "\<^loc>'/" 70)
    6.35  
     7.1 --- a/src/HOL/Integ/Numeral.thy	Mon Mar 19 19:28:27 2007 +0100
     7.2 +++ b/src/HOL/Integ/Numeral.thy	Tue Mar 20 08:27:15 2007 +0100
     7.3 @@ -42,7 +42,7 @@
     7.4    Bit :: "int \<Rightarrow> bit \<Rightarrow> int" (infixl "BIT" 90) where
     7.5    "k BIT b = (case b of B0 \<Rightarrow> 0 | B1 \<Rightarrow> 1) + k + k"
     7.6  
     7.7 -class number = -- {* for numeric types: nat, int, real, \dots *}
     7.8 +class number = type + -- {* for numeric types: nat, int, real, \dots *}
     7.9    fixes number_of :: "int \<Rightarrow> 'a"
    7.10  
    7.11  syntax
     8.1 --- a/src/HOL/Library/Kleene_Algebras.thy	Mon Mar 19 19:28:27 2007 +0100
     8.2 +++ b/src/HOL/Library/Kleene_Algebras.thy	Tue Mar 20 08:27:15 2007 +0100
     8.3 @@ -9,7 +9,7 @@
     8.4  
     8.5  text {* A type class of kleene algebras *}
     8.6  
     8.7 -class star = 
     8.8 +class star = type +
     8.9    fixes star :: "'a \<Rightarrow> 'a"
    8.10  
    8.11  class idem_add = ab_semigroup_add +
     9.1 --- a/src/HOL/Library/Parity.thy	Mon Mar 19 19:28:27 2007 +0100
     9.2 +++ b/src/HOL/Library/Parity.thy	Tue Mar 20 08:27:15 2007 +0100
     9.3 @@ -9,7 +9,7 @@
     9.4  imports Main
     9.5  begin
     9.6  
     9.7 -class even_odd =
     9.8 +class even_odd = type + 
     9.9    fixes even :: "'a \<Rightarrow> bool"
    9.10  
    9.11  abbreviation
    10.1 --- a/src/HOL/Library/Quotient.thy	Mon Mar 19 19:28:27 2007 +0100
    10.2 +++ b/src/HOL/Library/Quotient.thy	Tue Mar 20 08:27:15 2007 +0100
    10.3 @@ -21,7 +21,7 @@
    10.4   "\<sim> :: 'a => 'a => bool"}.
    10.5  *}
    10.6  
    10.7 -class eqv =
    10.8 +class eqv = type +
    10.9    fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<^loc>\<sim>" 50)
   10.10  
   10.11  class equiv = eqv +
    11.1 --- a/src/HOL/Nat.thy	Mon Mar 19 19:28:27 2007 +0100
    11.2 +++ b/src/HOL/Nat.thy	Tue Mar 20 08:27:15 2007 +0100
    11.3 @@ -106,7 +106,7 @@
    11.4  
    11.5  text {* size of a datatype value *}
    11.6  
    11.7 -class size =
    11.8 +class size = type +
    11.9    fixes size :: "'a \<Rightarrow> nat"
   11.10  
   11.11  text {* @{typ nat} is a datatype *}
   11.12 @@ -476,7 +476,7 @@
   11.13  
   11.14  subsection {* Arithmetic operators *}
   11.15  
   11.16 -class power =
   11.17 +class power = type +
   11.18    fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"            (infixr "\<^loc>^" 80)
   11.19  
   11.20  text {* arithmetic operators @{text "+ -"} and @{text "*"} *}
    12.1 --- a/src/HOL/Orderings.thy	Mon Mar 19 19:28:27 2007 +0100
    12.2 +++ b/src/HOL/Orderings.thy	Tue Mar 20 08:27:15 2007 +0100
    12.3 @@ -11,7 +11,7 @@
    12.4  
    12.5  subsection {* Order syntax *}
    12.6  
    12.7 -class ord =
    12.8 +class ord = type +
    12.9    fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubseteq>" 50)
   12.10      and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"  (infix "\<sqsubset>" 50)
   12.11  begin
    13.1 --- a/src/HOL/ex/Classpackage.thy	Mon Mar 19 19:28:27 2007 +0100
    13.2 +++ b/src/HOL/ex/Classpackage.thy	Tue Mar 20 08:27:15 2007 +0100
    13.3 @@ -8,7 +8,7 @@
    13.4  imports Main
    13.5  begin
    13.6  
    13.7 -class semigroup =
    13.8 +class semigroup = type +
    13.9    fixes mult :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "\<^loc>\<otimes>" 70)
   13.10    assumes assoc: "x \<^loc>\<otimes> y \<^loc>\<otimes> z = x \<^loc>\<otimes> (y \<^loc>\<otimes> z)"
   13.11  
    14.1 --- a/src/HOL/ex/CodeCollections.thy	Mon Mar 19 19:28:27 2007 +0100
    14.2 +++ b/src/HOL/ex/CodeCollections.thy	Tue Mar 20 08:27:15 2007 +0100
    14.3 @@ -74,7 +74,7 @@
    14.4    "list_ex P xs \<longleftrightarrow> (\<exists>x\<in>set xs. P x)"
    14.5    by (induct xs) auto
    14.6  
    14.7 -class finite =
    14.8 +class finite = type +
    14.9    fixes fin :: "'a list"
   14.10    assumes member_fin: "x \<in> set fin"
   14.11  begin
    15.1 --- a/src/HOL/ex/CodeEval.thy	Mon Mar 19 19:28:27 2007 +0100
    15.2 +++ b/src/HOL/ex/CodeEval.thy	Tue Mar 20 08:27:15 2007 +0100
    15.3 @@ -10,7 +10,7 @@
    15.4  
    15.5  subsection {* The typ_of class *}
    15.6  
    15.7 -class typ_of =
    15.8 +class typ_of = type +
    15.9    fixes typ_of :: "'a itself \<Rightarrow> typ"
   15.10  
   15.11  ML {*
    16.1 --- a/src/Pure/Tools/class_package.ML	Mon Mar 19 19:28:27 2007 +0100
    16.2 +++ b/src/Pure/Tools/class_package.ML	Tue Mar 20 08:27:15 2007 +0100
    16.3 @@ -417,13 +417,8 @@
    16.4  
    16.5  local
    16.6  
    16.7 -fun certify_class thy class =
    16.8 -  tap (the_class_data thy) (Sign.certify_class thy class);
    16.9 -
   16.10 -fun read_class thy =
   16.11 -  certify_class thy o Sign.intern_class thy;
   16.12 -
   16.13 -fun gen_class add_locale prep_class prep_param bname raw_supclasses raw_elems raw_other_consts thy =
   16.14 +fun gen_class add_locale prep_class prep_param bname
   16.15 +    raw_supclasses raw_elems raw_other_consts thy =
   16.16    let
   16.17      (*FIXME need proper concept for reading locale statements*)
   16.18      fun subst_classtyvar (_, _) =
   16.19 @@ -436,25 +431,27 @@
   16.20      val (elems, includes) = fold_rev (fn Locale.Elem e => apfst (cons e)
   16.21        | Locale.Expr i => apsnd (cons i)) raw_elems ([], []);
   16.22      val supclasses = map (prep_class thy) raw_supclasses;
   16.23 -    val supsort =
   16.24 -      supclasses
   16.25 -      |> Sign.certify_sort thy
   16.26 -      |> (fn [] => Sign.defaultS thy | S => S); (*FIXME Why syntax defaultS?*)
   16.27 -    val suplocales = map (Locale.Locale o #locale o the_class_data thy) supclasses;
   16.28 +    val sups = filter (is_some o lookup_class_data thy) supclasses;
   16.29 +    val supsort = Sign.certify_sort thy supclasses;
   16.30 +    val suplocales = map (Locale.Locale o #locale o the_class_data thy) sups;
   16.31      val supexpr = Locale.Merge (suplocales @ includes);
   16.32      val supparams = (map fst o Locale.parameters_of_expr thy)
   16.33        (Locale.Merge suplocales);
   16.34 -    val supconsts = AList.make
   16.35 -      (the o AList.lookup (op =) (param_map thy supclasses)) (map fst supparams);
   16.36 +    val supconsts = AList.make (the o AList.lookup (op =) (param_map thy sups))
   16.37 +      (map fst supparams);
   16.38      (*val elems_constrains = map
   16.39        (Element.Constrains o apsnd (Term.map_type_tfree subst_classtyvar)) supparams;*)
   16.40 +    fun mk_tyvar (_, sort) = TFree (AxClass.param_tyvarname,
   16.41 +      if Sign.subsort thy (supsort, sort) then sort else error
   16.42 +        ("Sort " ^ Sign.string_of_sort thy sort
   16.43 +          ^ " is less general than permitted least general sort "
   16.44 +          ^ Sign.string_of_sort thy supsort));
   16.45      fun extract_params thy name_locale =
   16.46 -      let   
   16.47 +      let
   16.48          val params = Locale.parameters_of thy name_locale;
   16.49        in
   16.50          (map (fst o fst) params, params
   16.51 -        |> (map o apfst o apsnd o Term.map_type_tfree)
   16.52 -             (K (TFree (AxClass.param_tyvarname, Sign.defaultS thy)))
   16.53 +        |> (map o apfst o apsnd o Term.map_type_tfree) mk_tyvar
   16.54          |> (map o apsnd) (fork_mixfix true NONE #> fst)
   16.55          |> chop (length supconsts)
   16.56          |> snd)
   16.57 @@ -493,7 +490,7 @@
   16.58        #-> (fn (name_axclass, ((_, (ax_terms, ax_axioms)), consts)) =>
   16.59          `(fn thy => extract_axiom_names thy name_locale)
   16.60        #-> (fn axiom_names =>
   16.61 -        add_class_data ((name_axclass, supclasses),
   16.62 +        add_class_data ((name_axclass, sups),
   16.63            (name_locale, map (fst o fst) params ~~ map fst consts,
   16.64              map2 make_witness ax_terms ax_axioms, axiom_names))
   16.65        #> prove_interpretation ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
   16.66 @@ -505,8 +502,8 @@
   16.67  
   16.68  in
   16.69  
   16.70 -val class_cmd = gen_class Locale.add_locale read_class AxClass.read_param;
   16.71 -val class = gen_class Locale.add_locale_i certify_class (K I);
   16.72 +val class_cmd = gen_class Locale.add_locale Sign.intern_class AxClass.read_param;
   16.73 +val class = gen_class Locale.add_locale_i Sign.certify_class (K I);
   16.74  
   16.75  end; (*local*)
   16.76