added type classes to constant's type
authornipkow
Fri Jul 07 18:27:47 2000 +0200 (2000-07-07)
changeset 9279fb4186e20148
parent 9278 0b8e87bb91d9
child 9280 78a9bca983ac
added type classes to constant's type
src/HOL/Algebra/poly/PolyHomo.thy
src/HOL/BCV/DFAandWTI.thy
src/HOL/BCV/DFAimpl.thy
src/HOL/Real/Hyperreal/Zorn.thy
src/HOL/Real/Lubs.thy
src/HOL/ex/LocaleGroup.thy
src/HOL/ex/MonoidGroup.thy
     1.1 --- a/src/HOL/Algebra/poly/PolyHomo.thy	Fri Jul 07 17:15:17 2000 +0200
     1.2 +++ b/src/HOL/Algebra/poly/PolyHomo.thy	Fri Jul 07 18:27:47 2000 +0200
     1.3 @@ -13,7 +13,7 @@
     1.4  
     1.5  consts
     1.6    EVAL2	:: ('a::ringS => 'b) => 'b => 'a up => 'b::ringS
     1.7 -  EVAL	:: 'a => 'a up => 'a
     1.8 +  EVAL	:: 'a::ringS => 'a up => 'a
     1.9  
    1.10  defs
    1.11    EVAL2_def	"EVAL2 phi a p == SUM (deg p) (%i. phi (coeff i p) * a ^ i)"
     2.1 --- a/src/HOL/BCV/DFAandWTI.thy	Fri Jul 07 17:15:17 2000 +0200
     2.2 +++ b/src/HOL/BCV/DFAandWTI.thy	Fri Jul 07 18:27:47 2000 +0200
     2.3 @@ -12,13 +12,13 @@
     2.4  
     2.5  constdefs
     2.6  
     2.7 - stable :: (nat => 's => 's option) => (nat => nat list) => nat => 's os => bool
     2.8 + stable :: (nat => 's::ord => 's option) => (nat => nat list) => nat => 's os => bool
     2.9  "stable step succs p sos ==
    2.10   !s. sos!p = Some s --> (? t. step p s = Some(t) &
    2.11                                (!q:set(succs p). Some t <= sos!q))"
    2.12  
    2.13   wti_is_fix_step ::
    2.14 -   "(nat => 's => 's option)
    2.15 +   "(nat => 's::ord => 's option)
    2.16      => (nat => 's os => bool)
    2.17      => (nat => nat list)
    2.18      => nat => 's set => bool"
    2.19 @@ -30,7 +30,7 @@
    2.20  "welltyping wti tos == !p<size(tos). wti p tos"
    2.21  
    2.22   is_dfa ::  ('s os => bool)
    2.23 -            => (nat => 's => 's option)
    2.24 +            => (nat => 's::ord => 's option)
    2.25              => (nat => nat list)
    2.26              => nat => 's set => bool
    2.27  "is_dfa dfa step succs n L == !sos : listsn n (option L).
     3.1 --- a/src/HOL/BCV/DFAimpl.thy	Fri Jul 07 17:15:17 2000 +0200
     3.2 +++ b/src/HOL/BCV/DFAimpl.thy	Fri Jul 07 18:27:47 2000 +0200
     3.3 @@ -34,11 +34,11 @@
     3.4   step_pres_type :: "(nat => 's => 's option) => nat => 's set => bool"
     3.5  "step_pres_type step n L == !s:L. !p<n. !t. step p s = Some(t) --> t:L"
     3.6  
     3.7 - step_mono_None :: "(nat => 's => 's option) => nat => 's set => bool"
     3.8 + step_mono_None :: "(nat => 's::ord => 's option) => nat => 's set => bool"
     3.9  "step_mono_None step n L == !s p t.
    3.10     s : L & p < n & s <= t & step p s = None --> step p t = None"
    3.11  
    3.12 - step_mono :: "(nat => 's => 's option) => nat => 's set => bool"
    3.13 + step_mono :: "(nat => 's::ord => 's option) => nat => 's set => bool"
    3.14  "step_mono step n L == !s p t u.
    3.15     s : L & p < n & s <= t & step p s = Some(u)
    3.16     --> (!v. step p t = Some(v) --> u <= v)"
     4.1 --- a/src/HOL/Real/Hyperreal/Zorn.thy	Fri Jul 07 17:15:17 2000 +0200
     4.2 +++ b/src/HOL/Real/Hyperreal/Zorn.thy	Fri Jul 07 18:27:47 2000 +0200
     4.3 @@ -5,24 +5,24 @@
     4.4      Description : Zorn's Lemma -- See lcp's Zorn.thy in ZF
     4.5  *) 
     4.6  
     4.7 -Zorn = Main +  
     4.8 +Zorn = Main +
     4.9  
    4.10  constdefs
    4.11 -  chain     ::  'a set => 'a set set
    4.12 +  chain     ::  'a::ord set => 'a set set
    4.13      "chain S  == {F. F <= S & (ALL x: F. ALL y: F. x <= y | y <= x)}" 
    4.14  
    4.15 -  super     ::  ['a set,'a set] => (('a set) set) 
    4.16 +  super     ::  ['a::ord set,'a set] => 'a set set
    4.17      "super S c == {d. d: chain(S) & c < d}"
    4.18  
    4.19 -  maxchain  ::  'a set => 'a set set
    4.20 +  maxchain  ::  'a::ord set => 'a set set
    4.21      "maxchain S == {c. c: chain S & super S c = {}}"
    4.22  
    4.23 -  succ      ::  ['a set,'a set] => 'a set
    4.24 +  succ      ::  ['a::ord set,'a set] => 'a set
    4.25      "succ S c == if (c ~: chain S| c: maxchain S) 
    4.26                   then c else (@c'. c': (super S c))" 
    4.27  
    4.28  consts 
    4.29 -  "TFin" :: 'a set => 'a set set
    4.30 +  "TFin" :: 'a::ord set => 'a set set
    4.31  
    4.32  inductive "TFin(S)"
    4.33    intrs
     5.1 --- a/src/HOL/Real/Lubs.thy	Fri Jul 07 17:15:17 2000 +0200
     5.2 +++ b/src/HOL/Real/Lubs.thy	Fri Jul 07 18:27:47 2000 +0200
     5.3 @@ -11,20 +11,20 @@
     5.4  
     5.5  consts
     5.6      
     5.7 -    "*<=" :: ['a set, 'a] => bool     (infixl 70)
     5.8 -    "<=*" :: ['a, 'a set] => bool     (infixl 70)
     5.9 +    "*<=" :: ['a set, 'a::ord] => bool     (infixl 70)
    5.10 +    "<=*" :: ['a::ord, 'a set] => bool     (infixl 70)
    5.11  
    5.12  constdefs
    5.13 -    leastP      :: ['a =>bool,'a] => bool
    5.14 +    leastP      :: ['a =>bool,'a::ord] => bool
    5.15      "leastP P x == (P x & x <=* Collect P)"
    5.16  
    5.17 -    isLub       :: ['a set, 'a set, 'a] => bool    
    5.18 +    isLub       :: ['a set, 'a set, 'a::ord] => bool    
    5.19      "isLub R S x  == leastP (isUb R S) x"
    5.20  
    5.21 -    isUb        :: ['a set, 'a set, 'a] => bool     
    5.22 +    isUb        :: ['a set, 'a set, 'a::ord] => bool     
    5.23      "isUb R S x   == S *<= x & x: R"
    5.24  
    5.25 -    ubs         :: ['a set, 'a set] => 'a set
    5.26 +    ubs         :: ['a set, 'a::ord set] => 'a set
    5.27      "ubs R S      == Collect (isUb R S)"
    5.28  
    5.29  defs
     6.1 --- a/src/HOL/ex/LocaleGroup.thy	Fri Jul 07 17:15:17 2000 +0200
     6.2 +++ b/src/HOL/ex/LocaleGroup.thy	Fri Jul 07 18:27:47 2000 +0200
     6.3 @@ -14,7 +14,7 @@
     6.4    unit     :: "'a"
     6.5  
     6.6  constdefs
     6.7 -  Group :: "('a, 'more) grouptype_scheme set"
     6.8 +  Group :: "('a, 'more::more) grouptype_scheme set"
     6.9    "Group == {G. (bin_op G): carrier G -> carrier G -> carrier G &
    6.10  	        inverse G : carrier G -> carrier G 
    6.11               & unit G : carrier G &
     7.1 --- a/src/HOL/ex/MonoidGroup.thy	Fri Jul 07 17:15:17 2000 +0200
     7.2 +++ b/src/HOL/ex/MonoidGroup.thy	Fri Jul 07 18:27:47 2000 +0200
     7.3 @@ -17,15 +17,15 @@
     7.4    inv :: "'a => 'a"
     7.5  
     7.6  constdefs
     7.7 -  monoid :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |) => bool"
     7.8 +  monoid :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more::more |) => bool"
     7.9    "monoid M == ALL x y z.
    7.10      times M (times M x y) z = times M x (times M y z) &
    7.11 -    times M (one M) x & times M x (one M) = x"
    7.12 +    times M (one M) x = x & times M x (one M) = x"
    7.13  
    7.14 -  group :: "(| times :: ['a, 'a] => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'more |) => bool"
    7.15 +  group :: "(| times :: ['a, 'a] => 'a, one :: 'a, inv :: 'a => 'a, ... :: 'more::more |) => bool"
    7.16    "group G == monoid G & (ALL x. times G (inv G x) x = one G)"
    7.17  
    7.18 -  reverse :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |) =>
    7.19 +  reverse :: "(| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more::more |) =>
    7.20      (| times :: ['a, 'a] => 'a, one :: 'a, ... :: 'more |)"
    7.21    "reverse M == M (| times := %x y. times M y x |)"
    7.22