prefer vacuous definitional type classes over axiomatic ones;
authorwenzelm
Mon Feb 10 17:20:11 2014 +0100 (2014-02-10 ago)
changeset 553804de48353034e
parent 55379 9701dbc35f86
child 55381 ca31f042414f
prefer vacuous definitional type classes over axiomatic ones;
src/CCL/CCL.thy
src/CCL/Set.thy
src/FOL/IFOL.thy
src/FOL/ex/Locale_Test/Locale_Test1.thy
src/FOL/ex/Nat.thy
src/FOL/ex/Natural_Numbers.thy
src/FOL/ex/Prolog.thy
src/FOLP/IFOLP.thy
src/FOLP/ex/Nat.thy
src/HOL/ex/Higher_Order_Logic.thy
src/LCF/LCF.thy
src/Sequents/LK/Nat.thy
src/Sequents/LK0.thy
src/ZF/ZF.thy
     1.1 --- a/src/CCL/CCL.thy	Mon Feb 10 14:33:47 2014 +0100
     1.2 +++ b/src/CCL/CCL.thy	Mon Feb 10 17:20:11 2014 +0100
     1.3 @@ -16,13 +16,13 @@
     1.4    being defined which contains only executable terms.
     1.5  *}
     1.6  
     1.7 -classes prog < "term"
     1.8 +class prog = "term"
     1.9  default_sort prog
    1.10  
    1.11 -arities "fun" :: (prog, prog) prog
    1.12 +instance "fun" :: (prog, prog) prog ..
    1.13  
    1.14  typedecl i
    1.15 -arities i :: prog
    1.16 +instance i :: prog ..
    1.17  
    1.18  
    1.19  consts
     2.1 --- a/src/CCL/Set.thy	Mon Feb 10 14:33:47 2014 +0100
     2.2 +++ b/src/CCL/Set.thy	Mon Feb 10 17:20:11 2014 +0100
     2.3 @@ -7,7 +7,7 @@
     2.4  declare [[eta_contract]]
     2.5  
     2.6  typedecl 'a set
     2.7 -arities set :: ("term") "term"
     2.8 +instance set :: ("term") "term" ..
     2.9  
    2.10  consts
    2.11    Collect       :: "['a => o] => 'a set"                    (*comprehension*)
     3.1 --- a/src/FOL/IFOL.thy	Mon Feb 10 14:33:47 2014 +0100
     3.2 +++ b/src/FOL/IFOL.thy	Mon Feb 10 17:20:11 2014 +0100
     3.3 @@ -24,7 +24,7 @@
     3.4  
     3.5  setup Pure_Thy.old_appl_syntax_setup
     3.6  
     3.7 -classes "term"
     3.8 +class "term"
     3.9  default_sort "term"
    3.10  
    3.11  typedecl o
     4.1 --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Feb 10 14:33:47 2014 +0100
     4.2 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Feb 10 17:20:11 2014 +0100
     4.3 @@ -8,7 +8,9 @@
     4.4  imports FOL
     4.5  begin
     4.6  
     4.7 -typedecl int arities int :: "term"
     4.8 +typedecl int
     4.9 +instance int :: "term" ..
    4.10 +
    4.11  consts plus :: "int => int => int" (infixl "+" 60)
    4.12    zero :: int ("0")
    4.13    minus :: "int => int" ("- _")
     5.1 --- a/src/FOL/ex/Nat.thy	Mon Feb 10 14:33:47 2014 +0100
     5.2 +++ b/src/FOL/ex/Nat.thy	Mon Feb 10 17:20:11 2014 +0100
     5.3 @@ -10,7 +10,7 @@
     5.4  begin
     5.5  
     5.6  typedecl nat
     5.7 -arities nat :: "term"
     5.8 +instance nat :: "term" ..
     5.9  
    5.10  axiomatization
    5.11    Zero :: nat  ("0") and
     6.1 --- a/src/FOL/ex/Natural_Numbers.thy	Mon Feb 10 14:33:47 2014 +0100
     6.2 +++ b/src/FOL/ex/Natural_Numbers.thy	Mon Feb 10 17:20:11 2014 +0100
     6.3 @@ -14,7 +14,7 @@
     6.4  *}
     6.5  
     6.6  typedecl nat
     6.7 -arities nat :: "term"
     6.8 +instance nat :: "term" ..
     6.9  
    6.10  axiomatization
    6.11    Zero :: nat    ("0") and
     7.1 --- a/src/FOL/ex/Prolog.thy	Mon Feb 10 14:33:47 2014 +0100
     7.2 +++ b/src/FOL/ex/Prolog.thy	Mon Feb 10 17:20:11 2014 +0100
     7.3 @@ -10,7 +10,7 @@
     7.4  begin
     7.5  
     7.6  typedecl 'a list
     7.7 -arities list :: ("term") "term"
     7.8 +instance list :: ("term") "term" ..
     7.9  
    7.10  axiomatization
    7.11    Nil     :: "'a list" and
     8.1 --- a/src/FOLP/IFOLP.thy	Mon Feb 10 14:33:47 2014 +0100
     8.2 +++ b/src/FOLP/IFOLP.thy	Mon Feb 10 17:20:11 2014 +0100
     8.3 @@ -13,7 +13,7 @@
     8.4  
     8.5  setup Pure_Thy.old_appl_syntax_setup
     8.6  
     8.7 -classes "term"
     8.8 +class "term"
     8.9  default_sort "term"
    8.10  
    8.11  typedecl p
     9.1 --- a/src/FOLP/ex/Nat.thy	Mon Feb 10 14:33:47 2014 +0100
     9.2 +++ b/src/FOLP/ex/Nat.thy	Mon Feb 10 17:20:11 2014 +0100
     9.3 @@ -10,7 +10,7 @@
     9.4  begin
     9.5  
     9.6  typedecl nat
     9.7 -arities nat :: "term"
     9.8 +instance nat :: "term" ..
     9.9  
    9.10  axiomatization
    9.11    Zero :: nat    ("0") and
    10.1 --- a/src/HOL/ex/Higher_Order_Logic.thy	Mon Feb 10 14:33:47 2014 +0100
    10.2 +++ b/src/HOL/ex/Higher_Order_Logic.thy	Mon Feb 10 17:20:11 2014 +0100
    10.3 @@ -18,13 +18,12 @@
    10.4  
    10.5  subsection {* Pure Logic *}
    10.6  
    10.7 -classes type
    10.8 +class type
    10.9  default_sort type
   10.10  
   10.11  typedecl o
   10.12 -arities
   10.13 -  o :: type
   10.14 -  "fun" :: (type, type) type
   10.15 +instance o :: type ..
   10.16 +instance "fun" :: (type, type) type ..
   10.17  
   10.18  
   10.19  subsubsection {* Basic logical connectives *}
    11.1 --- a/src/LCF/LCF.thy	Mon Feb 10 14:33:47 2014 +0100
    11.2 +++ b/src/LCF/LCF.thy	Mon Feb 10 17:20:11 2014 +0100
    11.3 @@ -13,7 +13,7 @@
    11.4  
    11.5  subsection {* Natural Deduction Rules for LCF *}
    11.6  
    11.7 -classes cpo < "term"
    11.8 +class cpo = "term"
    11.9  default_sort cpo
   11.10  
   11.11  typedecl tr
   11.12 @@ -21,12 +21,11 @@
   11.13  typedecl ('a,'b) prod  (infixl "*" 6)
   11.14  typedecl ('a,'b) sum  (infixl "+" 5)
   11.15  
   11.16 -arities
   11.17 -  "fun" :: (cpo, cpo) cpo
   11.18 -  prod :: (cpo, cpo) cpo
   11.19 -  sum :: (cpo, cpo) cpo
   11.20 -  tr :: cpo
   11.21 -  void :: cpo
   11.22 +instance "fun" :: (cpo, cpo) cpo ..
   11.23 +instance prod :: (cpo, cpo) cpo ..
   11.24 +instance sum :: (cpo, cpo) cpo ..
   11.25 +instance tr :: cpo ..
   11.26 +instance void :: cpo ..
   11.27  
   11.28  consts
   11.29   UU     :: "'a"
    12.1 --- a/src/Sequents/LK/Nat.thy	Mon Feb 10 14:33:47 2014 +0100
    12.2 +++ b/src/Sequents/LK/Nat.thy	Mon Feb 10 17:20:11 2014 +0100
    12.3 @@ -10,7 +10,7 @@
    12.4  begin
    12.5  
    12.6  typedecl nat
    12.7 -arities nat :: "term"
    12.8 +instance nat :: "term" ..
    12.9  
   12.10  axiomatization
   12.11    Zero :: nat      ("0") and
    13.1 --- a/src/Sequents/LK0.thy	Mon Feb 10 14:33:47 2014 +0100
    13.2 +++ b/src/Sequents/LK0.thy	Mon Feb 10 17:20:11 2014 +0100
    13.3 @@ -12,7 +12,7 @@
    13.4  imports Sequents
    13.5  begin
    13.6  
    13.7 -classes "term"
    13.8 +class "term"
    13.9  default_sort "term"
   13.10  
   13.11  consts
    14.1 --- a/src/ZF/ZF.thy	Mon Feb 10 14:33:47 2014 +0100
    14.2 +++ b/src/ZF/ZF.thy	Mon Feb 10 17:20:11 2014 +0100
    14.3 @@ -12,7 +12,7 @@
    14.4  declare [[eta_contract = false]]
    14.5  
    14.6  typedecl i
    14.7 -arities  i :: "term"
    14.8 +instance i :: "term" ..
    14.9  
   14.10  axiomatization
   14.11    zero :: "i"  ("0")   --{*the empty set*}  and