no base sort in class import
authorhaftmann
Wed Jan 21 23:40:23 2009 +0100 (2009-01-21)
changeset 29608564ea783ace8
parent 29586 4f9803829625
child 29609 a010aab5bed0
no base sort in class import
NEWS
src/HOL/HOL.thy
src/HOL/Int.thy
src/HOL/Library/Eval_Witness.thy
src/HOL/Library/Quotient.thy
src/HOL/Nat.thy
src/HOL/Nominal/Examples/W.thy
src/HOL/Parity.thy
src/HOL/Power.thy
src/HOL/RealVector.thy
src/HOL/SizeChange/Kleene_Algebras.thy
src/HOL/Typedef.thy
src/HOL/Word/BitSyntax.thy
src/HOL/Word/Size.thy
src/HOLCF/Porder.thy
src/Pure/Isar/class.ML
     1.1 --- a/NEWS	Wed Jan 21 18:37:44 2009 +0100
     1.2 +++ b/NEWS	Wed Jan 21 23:40:23 2009 +0100
     1.3 @@ -66,6 +66,12 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Class declaration: sc. "base sort" must not be given in import list
     1.8 +any longer but is inferred from the specification.  Particularly in HOL,
     1.9 +write
    1.10 +
    1.11 +    class foo = ...     instead of      class foo = type + ...
    1.12 +
    1.13  * Type Binding.T gradually replaces formerly used type bstring for names
    1.14  to be bound.  Name space interface for declarations has been simplified:
    1.15  
     2.1 --- a/src/HOL/HOL.thy	Wed Jan 21 18:37:44 2009 +0100
     2.2 +++ b/src/HOL/HOL.thy	Wed Jan 21 23:40:23 2009 +0100
     2.3 @@ -208,34 +208,34 @@
     2.4  
     2.5  subsubsection {* Generic classes and algebraic operations *}
     2.6  
     2.7 -class default = type +
     2.8 +class default =
     2.9    fixes default :: 'a
    2.10  
    2.11 -class zero = type + 
    2.12 +class zero = 
    2.13    fixes zero :: 'a  ("0")
    2.14  
    2.15 -class one = type +
    2.16 +class one =
    2.17    fixes one  :: 'a  ("1")
    2.18  
    2.19  hide (open) const zero one
    2.20  
    2.21 -class plus = type +
    2.22 +class plus =
    2.23    fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
    2.24  
    2.25 -class minus = type +
    2.26 +class minus =
    2.27    fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
    2.28  
    2.29 -class uminus = type +
    2.30 +class uminus =
    2.31    fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
    2.32  
    2.33 -class times = type +
    2.34 +class times =
    2.35    fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
    2.36  
    2.37 -class inverse = type +
    2.38 +class inverse =
    2.39    fixes inverse :: "'a \<Rightarrow> 'a"
    2.40      and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
    2.41  
    2.42 -class abs = type +
    2.43 +class abs =
    2.44    fixes abs :: "'a \<Rightarrow> 'a"
    2.45  begin
    2.46  
    2.47 @@ -247,10 +247,10 @@
    2.48  
    2.49  end
    2.50  
    2.51 -class sgn = type +
    2.52 +class sgn =
    2.53    fixes sgn :: "'a \<Rightarrow> 'a"
    2.54  
    2.55 -class ord = type +
    2.56 +class ord =
    2.57    fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    2.58      and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    2.59  begin
    2.60 @@ -1675,7 +1675,7 @@
    2.61  
    2.62  text {* Equality *}
    2.63  
    2.64 -class eq = type +
    2.65 +class eq =
    2.66    fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    2.67    assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
    2.68  begin
     3.1 --- a/src/HOL/Int.thy	Wed Jan 21 18:37:44 2009 +0100
     3.2 +++ b/src/HOL/Int.thy	Wed Jan 21 23:40:23 2009 +0100
     3.3 @@ -599,7 +599,7 @@
     3.4    Bit1 :: "int \<Rightarrow> int" where
     3.5    [code del]: "Bit1 k = 1 + k + k"
     3.6  
     3.7 -class number = type + -- {* for numeric types: nat, int, real, \dots *}
     3.8 +class number = -- {* for numeric types: nat, int, real, \dots *}
     3.9    fixes number_of :: "int \<Rightarrow> 'a"
    3.10  
    3.11  use "Tools/numeral.ML"
     4.1 --- a/src/HOL/Library/Eval_Witness.thy	Wed Jan 21 18:37:44 2009 +0100
     4.2 +++ b/src/HOL/Library/Eval_Witness.thy	Wed Jan 21 23:40:23 2009 +0100
     4.3 @@ -32,7 +32,7 @@
     4.4    with the oracle.  
     4.5  *}
     4.6  
     4.7 -class ml_equiv = type
     4.8 +class ml_equiv
     4.9  
    4.10  text {*
    4.11    Instances of @{text "ml_equiv"} should only be declared for those types,
     5.1 --- a/src/HOL/Library/Quotient.thy	Wed Jan 21 18:37:44 2009 +0100
     5.2 +++ b/src/HOL/Library/Quotient.thy	Wed Jan 21 23:40:23 2009 +0100
     5.3 @@ -21,7 +21,7 @@
     5.4   "\<sim> :: 'a => 'a => bool"}.
     5.5  *}
     5.6  
     5.7 -class eqv = type +
     5.8 +class eqv =
     5.9    fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<sim>" 50)
    5.10  
    5.11  class equiv = eqv +
     6.1 --- a/src/HOL/Nat.thy	Wed Jan 21 18:37:44 2009 +0100
     6.2 +++ b/src/HOL/Nat.thy	Wed Jan 21 23:40:23 2009 +0100
     6.3 @@ -1515,7 +1515,7 @@
     6.4  
     6.5  subsection {* size of a datatype value *}
     6.6  
     6.7 -class size = type +
     6.8 +class size =
     6.9    fixes size :: "'a \<Rightarrow> nat" -- {* see further theory @{text Wellfounded} *}
    6.10  
    6.11  end
     7.1 --- a/src/HOL/Nominal/Examples/W.thy	Wed Jan 21 18:37:44 2009 +0100
     7.2 +++ b/src/HOL/Nominal/Examples/W.thy	Wed Jan 21 23:40:23 2009 +0100
     7.3 @@ -49,7 +49,7 @@
     7.4  
     7.5  text {* free type variables *}
     7.6  
     7.7 -class ftv = type +
     7.8 +class ftv =
     7.9    fixes ftv :: "'a \<Rightarrow> tvar list"
    7.10  
    7.11  instantiation * :: (ftv, ftv) ftv
     8.1 --- a/src/HOL/Parity.thy	Wed Jan 21 18:37:44 2009 +0100
     8.2 +++ b/src/HOL/Parity.thy	Wed Jan 21 23:40:23 2009 +0100
     8.3 @@ -8,7 +8,7 @@
     8.4  imports Plain Presburger
     8.5  begin
     8.6  
     8.7 -class even_odd = type + 
     8.8 +class even_odd = 
     8.9    fixes even :: "'a \<Rightarrow> bool"
    8.10  
    8.11  abbreviation
     9.1 --- a/src/HOL/Power.thy	Wed Jan 21 18:37:44 2009 +0100
     9.2 +++ b/src/HOL/Power.thy	Wed Jan 21 23:40:23 2009 +0100
     9.3 @@ -11,7 +11,7 @@
     9.4  imports Nat
     9.5  begin
     9.6  
     9.7 -class power = type +
     9.8 +class power =
     9.9    fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"            (infixr "^" 80)
    9.10  
    9.11  subsection{*Powers for Arbitrary Monoids*}
    10.1 --- a/src/HOL/RealVector.thy	Wed Jan 21 18:37:44 2009 +0100
    10.2 +++ b/src/HOL/RealVector.thy	Wed Jan 21 23:40:23 2009 +0100
    10.3 @@ -124,7 +124,7 @@
    10.4  
    10.5  subsection {* Real vector spaces *}
    10.6  
    10.7 -class scaleR = type +
    10.8 +class scaleR =
    10.9    fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "*\<^sub>R" 75)
   10.10  begin
   10.11  
   10.12 @@ -418,7 +418,7 @@
   10.13  
   10.14  subsection {* Real normed vector spaces *}
   10.15  
   10.16 -class norm = type +
   10.17 +class norm =
   10.18    fixes norm :: "'a \<Rightarrow> real"
   10.19  
   10.20  instantiation real :: norm
    11.1 --- a/src/HOL/SizeChange/Kleene_Algebras.thy	Wed Jan 21 18:37:44 2009 +0100
    11.2 +++ b/src/HOL/SizeChange/Kleene_Algebras.thy	Wed Jan 21 23:40:23 2009 +0100
    11.3 @@ -11,7 +11,7 @@
    11.4  
    11.5  text {* A type class of kleene algebras *}
    11.6  
    11.7 -class star = type +
    11.8 +class star =
    11.9    fixes star :: "'a \<Rightarrow> 'a"
   11.10  
   11.11  class idem_add = ab_semigroup_add +
    12.1 --- a/src/HOL/Typedef.thy	Wed Jan 21 18:37:44 2009 +0100
    12.2 +++ b/src/HOL/Typedef.thy	Wed Jan 21 23:40:23 2009 +0100
    12.3 @@ -123,7 +123,7 @@
    12.4  text {* This class is just a workaround for classes without parameters;
    12.5    it shall disappear as soon as possible. *}
    12.6  
    12.7 -class itself = type + 
    12.8 +class itself = 
    12.9    fixes itself :: "'a itself"
   12.10  
   12.11  setup {*
    13.1 --- a/src/HOL/Word/BitSyntax.thy	Wed Jan 21 18:37:44 2009 +0100
    13.2 +++ b/src/HOL/Word/BitSyntax.thy	Wed Jan 21 23:40:23 2009 +0100
    13.3 @@ -12,7 +12,7 @@
    13.4  imports BinGeneral
    13.5  begin
    13.6  
    13.7 -class bit = type +
    13.8 +class bit =
    13.9    fixes bitNOT :: "'a \<Rightarrow> 'a"       ("NOT _" [70] 71)
   13.10      and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64)
   13.11      and bitOR  :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "OR"  59)
    14.1 --- a/src/HOL/Word/Size.thy	Wed Jan 21 18:37:44 2009 +0100
    14.2 +++ b/src/HOL/Word/Size.thy	Wed Jan 21 23:40:23 2009 +0100
    14.3 @@ -18,7 +18,7 @@
    14.4    some duplication with the definitions in @{text "Numeral_Type"}.
    14.5  *}
    14.6  
    14.7 -class len0 = type +
    14.8 +class len0 =
    14.9    fixes len_of :: "'a itself \<Rightarrow> nat"
   14.10  
   14.11  text {* 
    15.1 --- a/src/HOLCF/Porder.thy	Wed Jan 21 18:37:44 2009 +0100
    15.2 +++ b/src/HOLCF/Porder.thy	Wed Jan 21 23:40:23 2009 +0100
    15.3 @@ -10,7 +10,7 @@
    15.4  
    15.5  subsection {* Type class for partial orders *}
    15.6  
    15.7 -class sq_ord = type +
    15.8 +class sq_ord =
    15.9    fixes sq_le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   15.10  
   15.11  notation
    16.1 --- a/src/Pure/Isar/class.ML	Wed Jan 21 18:37:44 2009 +0100
    16.2 +++ b/src/Pure/Isar/class.ML	Wed Jan 21 23:40:23 2009 +0100
    16.3 @@ -92,8 +92,8 @@
    16.4  fun add_typ_check level name f = Context.proof_map (Syntax.add_typ_check level name (fn xs => fn ctxt =>
    16.5    let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end));
    16.6  
    16.7 -fun singleton_infer_param change_sort = (map o map_atyps) (fn T as TVar (vi as (_, i), sort) =>
    16.8 -      if TypeInfer.is_param vi then TypeInfer.param i (Name.aT, change_sort sort)
    16.9 +val singleton_infer_param = (map o map_atyps) (fn T as TVar (vi as (_, i), sort) =>
   16.10 +      if TypeInfer.is_param vi then TypeInfer.param i (Name.aT, sort)
   16.11        else error ("Illegal schematic type variable in class specification: " ^ Term.string_of_vname vi)
   16.12          (*FIXME does not occur*)
   16.13    | T as TFree (v, sort) =>
   16.14 @@ -119,11 +119,12 @@
   16.15    let
   16.16      (* prepare import *)
   16.17      val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy));
   16.18 -    val (sups, others_basesort) = map (prep_class thy) raw_supclasses
   16.19 -      |> Sign.minimize_sort thy
   16.20 -      |> List.partition (is_class thy);
   16.21 -
   16.22 -    val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
   16.23 +    val sups = map (prep_class thy) raw_supclasses
   16.24 +      |> Sign.minimize_sort thy;
   16.25 +    val _ = case filter_out (is_class thy) sups
   16.26 +     of [] => ()
   16.27 +      | no_classes => error ("These are not classes: " ^ commas (map quote no_classes));
   16.28 +          val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
   16.29      val supparam_names = map fst supparams;
   16.30      val _ = if has_duplicates (op =) supparam_names
   16.31        then error ("Duplicate parameter(s) in superclasses: "
   16.32 @@ -131,7 +132,7 @@
   16.33        else ();
   16.34      val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional [])))
   16.35        sups, []);
   16.36 -    val given_basesort = fold inter_sort (map (base_sort thy) sups) others_basesort;
   16.37 +    val given_basesort = fold inter_sort (map (base_sort thy) sups) [];
   16.38  
   16.39      (* infer types and base sort *)
   16.40      val base_constraints = (map o apsnd)
   16.41 @@ -139,10 +140,9 @@
   16.42          (these_operations thy sups);
   16.43      val ((_, _, inferred_elems), _) = ProofContext.init thy
   16.44        |> fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
   16.45 -      |> add_typ_check ~1 "singleton_infer_param" (singleton_infer_param (inter_sort given_basesort))
   16.46 +      |> add_typ_check ~1 "singleton_infer_param" singleton_infer_param
   16.47        |> add_typ_check ~2 "singleton_fixate" singleton_fixate
   16.48        |> prep_decl supexpr raw_elems;
   16.49 -    (*FIXME propagation of given base sort into class spec broken*)
   16.50      (*FIXME check for *all* side conditions here, extra check function for elements,
   16.51        less side-condition checks in check phase*)
   16.52      val base_sort = if null inferred_elems then given_basesort else
   16.53 @@ -170,45 +170,6 @@
   16.54  val cert_class_spec = prep_class_spec (K I) Expression.cert_declaration;
   16.55  val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration;
   16.56  
   16.57 -(*fun prep_class_spec prep_class process_decl thy raw_supclasses raw_elems =
   16.58 -  let
   16.59 -    (*FIXME 2009 simplify*)
   16.60 -    val supclasses = map (prep_class thy) raw_supclasses;
   16.61 -    val supsort = Sign.minimize_sort thy supclasses;
   16.62 -    val (sups, bases) = List.partition (is_class thy) supsort;
   16.63 -    val base_sort = if null sups then supsort else
   16.64 -      Library.foldr (Sorts.inter_sort (Sign.classes_of thy))
   16.65 -        (map (base_sort thy) sups, bases);
   16.66 -    val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
   16.67 -    val supparam_names = map fst supparams;
   16.68 -    val _ = if has_duplicates (op =) supparam_names
   16.69 -      then error ("Duplicate parameter(s) in superclasses: "
   16.70 -        ^ (commas o map quote o duplicates (op =)) supparam_names)
   16.71 -      else ();
   16.72 -
   16.73 -    val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional [])))
   16.74 -      sups, []);
   16.75 -    val constrain = Element.Constrains ((map o apsnd o map_atyps)
   16.76 -      (K (TFree (Name.aT, base_sort))) supparams);
   16.77 -      (*FIXME 2009 perhaps better: control type variable by explicit
   16.78 -      parameter instantiation of import expression*)
   16.79 -    val begin_ctxt = begin sups base_sort
   16.80 -      #> fold (Variable.declare_constraints o Free) ((map o apsnd o map_atyps)
   16.81 -          (K (TFree (Name.aT, base_sort))) supparams) (*FIXME
   16.82 -            should constraints be issued in begin?*)
   16.83 -    val ((_, _, syntax_elems), _) = ProofContext.init thy
   16.84 -      |> begin_ctxt
   16.85 -      |> process_decl supexpr raw_elems;
   16.86 -    fun fork_syn (Element.Fixes xs) =
   16.87 -          fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs
   16.88 -          #>> Element.Fixes
   16.89 -      | fork_syn x = pair x;
   16.90 -    val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
   16.91 -  in (((sups, supparam_names), (supsort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end;
   16.92 -
   16.93 -val cert_class_spec = prep_class_spec (K I) Expression.cert_declaration;
   16.94 -val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration;*)
   16.95 -
   16.96  fun add_consts bname class base_sort sups supparams global_syntax thy =
   16.97    let
   16.98      (*FIXME 2009 simplify*)