--- 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"
--- 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")
--- 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 *}
--- 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
--- 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)"
--- 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)
--- 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
--- 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 +
--- 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
--- 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 +
--- 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 "*"} *}
--- 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
--- 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)"
--- 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
--- 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 {*
--- 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*)