merged
authorhaftmann
Wed Jan 21 23:42:37 2009 +0100 (2009-01-21)
changeset 296119891e3646809
parent 29607 2db3537c3535
parent 29610 83d282f12352
child 29612 4f68e0f8f4fd
merged
src/HOL/ATP_Linkup.thy
     1.1 --- a/NEWS	Wed Jan 21 23:25:17 2009 +0100
     1.2 +++ b/NEWS	Wed Jan 21 23:42:37 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/ATP_Linkup.thy	Wed Jan 21 23:25:17 2009 +0100
     2.2 +++ b/src/HOL/ATP_Linkup.thy	Wed Jan 21 23:42:37 2009 +0100
     2.3 @@ -7,7 +7,7 @@
     2.4  header {* The Isabelle-ATP Linkup *}
     2.5  
     2.6  theory ATP_Linkup
     2.7 -imports Record Hilbert_Choice
     2.8 +imports Divides Record Hilbert_Choice
     2.9  uses
    2.10    "Tools/polyhash.ML"
    2.11    "Tools/res_clause.ML"
     3.1 --- a/src/HOL/Datatype.thy	Wed Jan 21 23:25:17 2009 +0100
     3.2 +++ b/src/HOL/Datatype.thy	Wed Jan 21 23:42:37 2009 +0100
     3.3 @@ -8,7 +8,7 @@
     3.4  header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
     3.5  
     3.6  theory Datatype
     3.7 -imports Nat Relation
     3.8 +imports Nat Product_Type
     3.9  begin
    3.10  
    3.11  typedef (Node)
    3.12 @@ -509,15 +509,6 @@
    3.13  lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma, standard]
    3.14  
    3.15  
    3.16 -(*** Domain ***)
    3.17 -
    3.18 -lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
    3.19 -by auto
    3.20 -
    3.21 -lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
    3.22 -by auto
    3.23 -
    3.24 -
    3.25  text {* hides popular names *}
    3.26  hide (open) type node item
    3.27  hide (open) const Push Node Atom Leaf Numb Lim Split Case
     4.1 --- a/src/HOL/Finite_Set.thy	Wed Jan 21 23:25:17 2009 +0100
     4.2 +++ b/src/HOL/Finite_Set.thy	Wed Jan 21 23:42:37 2009 +0100
     4.3 @@ -6,7 +6,7 @@
     4.4  header {* Finite sets *}
     4.5  
     4.6  theory Finite_Set
     4.7 -imports Datatype Divides Transitive_Closure
     4.8 +imports Nat Product_Type Power
     4.9  begin
    4.10  
    4.11  subsection {* Definition and basic properties *}
    4.12 @@ -380,46 +380,6 @@
    4.13  by(blast intro: finite_subset[OF subset_Pow_Union])
    4.14  
    4.15  
    4.16 -lemma finite_converse [iff]: "finite (r^-1) = finite r"
    4.17 -  apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
    4.18 -   apply simp
    4.19 -   apply (rule iffI)
    4.20 -    apply (erule finite_imageD [unfolded inj_on_def])
    4.21 -    apply (simp split add: split_split)
    4.22 -   apply (erule finite_imageI)
    4.23 -  apply (simp add: converse_def image_def, auto)
    4.24 -  apply (rule bexI)
    4.25 -   prefer 2 apply assumption
    4.26 -  apply simp
    4.27 -  done
    4.28 -
    4.29 -
    4.30 -text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
    4.31 -Ehmety) *}
    4.32 -
    4.33 -lemma finite_Field: "finite r ==> finite (Field r)"
    4.34 -  -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
    4.35 -  apply (induct set: finite)
    4.36 -   apply (auto simp add: Field_def Domain_insert Range_insert)
    4.37 -  done
    4.38 -
    4.39 -lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
    4.40 -  apply clarify
    4.41 -  apply (erule trancl_induct)
    4.42 -   apply (auto simp add: Field_def)
    4.43 -  done
    4.44 -
    4.45 -lemma finite_trancl: "finite (r^+) = finite r"
    4.46 -  apply auto
    4.47 -   prefer 2
    4.48 -   apply (rule trancl_subset_Field2 [THEN finite_subset])
    4.49 -   apply (rule finite_SigmaI)
    4.50 -    prefer 3
    4.51 -    apply (blast intro: r_into_trancl' finite_subset)
    4.52 -   apply (auto simp add: finite_Field)
    4.53 -  done
    4.54 -
    4.55 -
    4.56  subsection {* Class @{text finite}  *}
    4.57  
    4.58  setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
    4.59 @@ -471,9 +431,6 @@
    4.60  instance "+" :: (finite, finite) finite
    4.61    by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
    4.62  
    4.63 -instance option :: (finite) finite
    4.64 -  by default (simp add: insert_None_conv_UNIV [symmetric])
    4.65 -
    4.66  
    4.67  subsection {* A fold functional for finite sets *}
    4.68  
     5.1 --- a/src/HOL/HOL.thy	Wed Jan 21 23:25:17 2009 +0100
     5.2 +++ b/src/HOL/HOL.thy	Wed Jan 21 23:42:37 2009 +0100
     5.3 @@ -208,34 +208,34 @@
     5.4  
     5.5  subsubsection {* Generic classes and algebraic operations *}
     5.6  
     5.7 -class default = type +
     5.8 +class default =
     5.9    fixes default :: 'a
    5.10  
    5.11 -class zero = type + 
    5.12 +class zero = 
    5.13    fixes zero :: 'a  ("0")
    5.14  
    5.15 -class one = type +
    5.16 +class one =
    5.17    fixes one  :: 'a  ("1")
    5.18  
    5.19  hide (open) const zero one
    5.20  
    5.21 -class plus = type +
    5.22 +class plus =
    5.23    fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "+" 65)
    5.24  
    5.25 -class minus = type +
    5.26 +class minus =
    5.27    fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "-" 65)
    5.28  
    5.29 -class uminus = type +
    5.30 +class uminus =
    5.31    fixes uminus :: "'a \<Rightarrow> 'a"  ("- _" [81] 80)
    5.32  
    5.33 -class times = type +
    5.34 +class times =
    5.35    fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "*" 70)
    5.36  
    5.37 -class inverse = type +
    5.38 +class inverse =
    5.39    fixes inverse :: "'a \<Rightarrow> 'a"
    5.40      and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"  (infixl "'/" 70)
    5.41  
    5.42 -class abs = type +
    5.43 +class abs =
    5.44    fixes abs :: "'a \<Rightarrow> 'a"
    5.45  begin
    5.46  
    5.47 @@ -247,10 +247,10 @@
    5.48  
    5.49  end
    5.50  
    5.51 -class sgn = type +
    5.52 +class sgn =
    5.53    fixes sgn :: "'a \<Rightarrow> 'a"
    5.54  
    5.55 -class ord = type +
    5.56 +class ord =
    5.57    fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    5.58      and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    5.59  begin
    5.60 @@ -1675,7 +1675,7 @@
    5.61  
    5.62  text {* Equality *}
    5.63  
    5.64 -class eq = type +
    5.65 +class eq =
    5.66    fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
    5.67    assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
    5.68  begin
     6.1 --- a/src/HOL/Int.thy	Wed Jan 21 23:25:17 2009 +0100
     6.2 +++ b/src/HOL/Int.thy	Wed Jan 21 23:42:37 2009 +0100
     6.3 @@ -599,7 +599,7 @@
     6.4    Bit1 :: "int \<Rightarrow> int" where
     6.5    [code del]: "Bit1 k = 1 + k + k"
     6.6  
     6.7 -class number = type + -- {* for numeric types: nat, int, real, \dots *}
     6.8 +class number = -- {* for numeric types: nat, int, real, \dots *}
     6.9    fixes number_of :: "int \<Rightarrow> 'a"
    6.10  
    6.11  use "Tools/numeral.ML"
     7.1 --- a/src/HOL/Library/Eval_Witness.thy	Wed Jan 21 23:25:17 2009 +0100
     7.2 +++ b/src/HOL/Library/Eval_Witness.thy	Wed Jan 21 23:42:37 2009 +0100
     7.3 @@ -32,7 +32,7 @@
     7.4    with the oracle.  
     7.5  *}
     7.6  
     7.7 -class ml_equiv = type
     7.8 +class ml_equiv
     7.9  
    7.10  text {*
    7.11    Instances of @{text "ml_equiv"} should only be declared for those types,
     8.1 --- a/src/HOL/Library/Quotient.thy	Wed Jan 21 23:25:17 2009 +0100
     8.2 +++ b/src/HOL/Library/Quotient.thy	Wed Jan 21 23:42:37 2009 +0100
     8.3 @@ -21,7 +21,7 @@
     8.4   "\<sim> :: 'a => 'a => bool"}.
     8.5  *}
     8.6  
     8.7 -class eqv = type +
     8.8 +class eqv =
     8.9    fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool"    (infixl "\<sim>" 50)
    8.10  
    8.11  class equiv = eqv +
     9.1 --- a/src/HOL/Nat.thy	Wed Jan 21 23:25:17 2009 +0100
     9.2 +++ b/src/HOL/Nat.thy	Wed Jan 21 23:42:37 2009 +0100
     9.3 @@ -1515,7 +1515,7 @@
     9.4  
     9.5  subsection {* size of a datatype value *}
     9.6  
     9.7 -class size = type +
     9.8 +class size =
     9.9    fixes size :: "'a \<Rightarrow> nat" -- {* see further theory @{text Wellfounded} *}
    9.10  
    9.11  end
    10.1 --- a/src/HOL/Nominal/Examples/W.thy	Wed Jan 21 23:25:17 2009 +0100
    10.2 +++ b/src/HOL/Nominal/Examples/W.thy	Wed Jan 21 23:42:37 2009 +0100
    10.3 @@ -49,7 +49,7 @@
    10.4  
    10.5  text {* free type variables *}
    10.6  
    10.7 -class ftv = type +
    10.8 +class ftv =
    10.9    fixes ftv :: "'a \<Rightarrow> tvar list"
   10.10  
   10.11  instantiation * :: (ftv, ftv) ftv
    11.1 --- a/src/HOL/Parity.thy	Wed Jan 21 23:25:17 2009 +0100
    11.2 +++ b/src/HOL/Parity.thy	Wed Jan 21 23:42:37 2009 +0100
    11.3 @@ -8,7 +8,7 @@
    11.4  imports Plain Presburger
    11.5  begin
    11.6  
    11.7 -class even_odd = type + 
    11.8 +class even_odd = 
    11.9    fixes even :: "'a \<Rightarrow> bool"
   11.10  
   11.11  abbreviation
    12.1 --- a/src/HOL/Plain.thy	Wed Jan 21 23:25:17 2009 +0100
    12.2 +++ b/src/HOL/Plain.thy	Wed Jan 21 23:42:37 2009 +0100
    12.3 @@ -1,7 +1,7 @@
    12.4  header {* Plain HOL *}
    12.5  
    12.6  theory Plain
    12.7 -imports Datatype FunDef Record SAT Extraction
    12.8 +imports Datatype FunDef Record SAT Extraction Divides
    12.9  begin
   12.10  
   12.11  text {*
   12.12 @@ -9,6 +9,9 @@
   12.13    include @{text Hilbert_Choice}.
   12.14  *}
   12.15  
   12.16 +instance option :: (finite) finite
   12.17 +  by default (simp add: insert_None_conv_UNIV [symmetric])
   12.18 +
   12.19  ML {* path_add "~~/src/HOL/Library" *}
   12.20  
   12.21  end
    13.1 --- a/src/HOL/Power.thy	Wed Jan 21 23:25:17 2009 +0100
    13.2 +++ b/src/HOL/Power.thy	Wed Jan 21 23:42:37 2009 +0100
    13.3 @@ -11,7 +11,7 @@
    13.4  imports Nat
    13.5  begin
    13.6  
    13.7 -class power = type +
    13.8 +class power =
    13.9    fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"            (infixr "^" 80)
   13.10  
   13.11  subsection{*Powers for Arbitrary Monoids*}
    14.1 --- a/src/HOL/RealVector.thy	Wed Jan 21 23:25:17 2009 +0100
    14.2 +++ b/src/HOL/RealVector.thy	Wed Jan 21 23:42:37 2009 +0100
    14.3 @@ -124,7 +124,7 @@
    14.4  
    14.5  subsection {* Real vector spaces *}
    14.6  
    14.7 -class scaleR = type +
    14.8 +class scaleR =
    14.9    fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "*\<^sub>R" 75)
   14.10  begin
   14.11  
   14.12 @@ -418,7 +418,7 @@
   14.13  
   14.14  subsection {* Real normed vector spaces *}
   14.15  
   14.16 -class norm = type +
   14.17 +class norm =
   14.18    fixes norm :: "'a \<Rightarrow> real"
   14.19  
   14.20  instantiation real :: norm
    15.1 --- a/src/HOL/Relation.thy	Wed Jan 21 23:25:17 2009 +0100
    15.2 +++ b/src/HOL/Relation.thy	Wed Jan 21 23:42:37 2009 +0100
    15.3 @@ -1,5 +1,4 @@
    15.4  (*  Title:      HOL/Relation.thy
    15.5 -    ID:         $Id$
    15.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    15.7      Copyright   1996  University of Cambridge
    15.8  *)
    15.9 @@ -7,7 +6,7 @@
   15.10  header {* Relations *}
   15.11  
   15.12  theory Relation
   15.13 -imports Product_Type
   15.14 +imports Datatype Finite_Set
   15.15  begin
   15.16  
   15.17  subsection {* Definitions *}
   15.18 @@ -379,6 +378,12 @@
   15.19  lemma fst_eq_Domain: "fst ` R = Domain R";
   15.20  by (auto intro!:image_eqI)
   15.21  
   15.22 +lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
   15.23 +by auto
   15.24 +
   15.25 +lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
   15.26 +by auto
   15.27 +
   15.28  
   15.29  subsection {* Range *}
   15.30  
   15.31 @@ -566,6 +571,31 @@
   15.32    done
   15.33  
   15.34  
   15.35 +subsection {* Finiteness *}
   15.36 +
   15.37 +lemma finite_converse [iff]: "finite (r^-1) = finite r"
   15.38 +  apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
   15.39 +   apply simp
   15.40 +   apply (rule iffI)
   15.41 +    apply (erule finite_imageD [unfolded inj_on_def])
   15.42 +    apply (simp split add: split_split)
   15.43 +   apply (erule finite_imageI)
   15.44 +  apply (simp add: converse_def image_def, auto)
   15.45 +  apply (rule bexI)
   15.46 +   prefer 2 apply assumption
   15.47 +  apply simp
   15.48 +  done
   15.49 +
   15.50 +text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
   15.51 +Ehmety) *}
   15.52 +
   15.53 +lemma finite_Field: "finite r ==> finite (Field r)"
   15.54 +  -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
   15.55 +  apply (induct set: finite)
   15.56 +   apply (auto simp add: Field_def Domain_insert Range_insert)
   15.57 +  done
   15.58 +
   15.59 +
   15.60  subsection {* Version of @{text lfp_induct} for binary relations *}
   15.61  
   15.62  lemmas lfp_induct2 = 
    16.1 --- a/src/HOL/SizeChange/Kleene_Algebras.thy	Wed Jan 21 23:25:17 2009 +0100
    16.2 +++ b/src/HOL/SizeChange/Kleene_Algebras.thy	Wed Jan 21 23:42:37 2009 +0100
    16.3 @@ -11,7 +11,7 @@
    16.4  
    16.5  text {* A type class of kleene algebras *}
    16.6  
    16.7 -class star = type +
    16.8 +class star =
    16.9    fixes star :: "'a \<Rightarrow> 'a"
   16.10  
   16.11  class idem_add = ab_semigroup_add +
    17.1 --- a/src/HOL/Transitive_Closure.thy	Wed Jan 21 23:25:17 2009 +0100
    17.2 +++ b/src/HOL/Transitive_Closure.thy	Wed Jan 21 23:42:37 2009 +0100
    17.3 @@ -1,5 +1,4 @@
    17.4  (*  Title:      HOL/Transitive_Closure.thy
    17.5 -    ID:         $Id$
    17.6      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    17.7      Copyright   1992  University of Cambridge
    17.8  *)
    17.9 @@ -568,6 +567,22 @@
   17.10     apply auto
   17.11    done
   17.12  
   17.13 +lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
   17.14 +  apply clarify
   17.15 +  apply (erule trancl_induct)
   17.16 +   apply (auto simp add: Field_def)
   17.17 +  done
   17.18 +
   17.19 +lemma finite_trancl: "finite (r^+) = finite r"
   17.20 +  apply auto
   17.21 +   prefer 2
   17.22 +   apply (rule trancl_subset_Field2 [THEN finite_subset])
   17.23 +   apply (rule finite_SigmaI)
   17.24 +    prefer 3
   17.25 +    apply (blast intro: r_into_trancl' finite_subset)
   17.26 +   apply (auto simp add: finite_Field)
   17.27 +  done
   17.28 +
   17.29  text {* More about converse @{text rtrancl} and @{text trancl}, should
   17.30    be merged with main body. *}
   17.31  
    18.1 --- a/src/HOL/Typedef.thy	Wed Jan 21 23:25:17 2009 +0100
    18.2 +++ b/src/HOL/Typedef.thy	Wed Jan 21 23:42:37 2009 +0100
    18.3 @@ -123,7 +123,7 @@
    18.4  text {* This class is just a workaround for classes without parameters;
    18.5    it shall disappear as soon as possible. *}
    18.6  
    18.7 -class itself = type + 
    18.8 +class itself = 
    18.9    fixes itself :: "'a itself"
   18.10  
   18.11  setup {*
    19.1 --- a/src/HOL/Wellfounded.thy	Wed Jan 21 23:25:17 2009 +0100
    19.2 +++ b/src/HOL/Wellfounded.thy	Wed Jan 21 23:42:37 2009 +0100
    19.3 @@ -7,7 +7,7 @@
    19.4  header {*Well-founded Recursion*}
    19.5  
    19.6  theory Wellfounded
    19.7 -imports Finite_Set Nat
    19.8 +imports Finite_Set Transitive_Closure Nat
    19.9  uses ("Tools/function_package/size.ML")
   19.10  begin
   19.11  
    20.1 --- a/src/HOL/Word/BitSyntax.thy	Wed Jan 21 23:25:17 2009 +0100
    20.2 +++ b/src/HOL/Word/BitSyntax.thy	Wed Jan 21 23:42:37 2009 +0100
    20.3 @@ -12,7 +12,7 @@
    20.4  imports BinGeneral
    20.5  begin
    20.6  
    20.7 -class bit = type +
    20.8 +class bit =
    20.9    fixes bitNOT :: "'a \<Rightarrow> 'a"       ("NOT _" [70] 71)
   20.10      and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64)
   20.11      and bitOR  :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "OR"  59)
    21.1 --- a/src/HOL/Word/Size.thy	Wed Jan 21 23:25:17 2009 +0100
    21.2 +++ b/src/HOL/Word/Size.thy	Wed Jan 21 23:42:37 2009 +0100
    21.3 @@ -18,7 +18,7 @@
    21.4    some duplication with the definitions in @{text "Numeral_Type"}.
    21.5  *}
    21.6  
    21.7 -class len0 = type +
    21.8 +class len0 =
    21.9    fixes len_of :: "'a itself \<Rightarrow> nat"
   21.10  
   21.11  text {* 
    22.1 --- a/src/HOLCF/Porder.thy	Wed Jan 21 23:25:17 2009 +0100
    22.2 +++ b/src/HOLCF/Porder.thy	Wed Jan 21 23:42:37 2009 +0100
    22.3 @@ -10,7 +10,7 @@
    22.4  
    22.5  subsection {* Type class for partial orders *}
    22.6  
    22.7 -class sq_ord = type +
    22.8 +class sq_ord =
    22.9    fixes sq_le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
   22.10  
   22.11  notation
    23.1 --- a/src/Pure/Isar/class.ML	Wed Jan 21 23:25:17 2009 +0100
    23.2 +++ b/src/Pure/Isar/class.ML	Wed Jan 21 23:42:37 2009 +0100
    23.3 @@ -92,8 +92,8 @@
    23.4  fun add_typ_check level name f = Context.proof_map (Syntax.add_typ_check level name (fn xs => fn ctxt =>
    23.5    let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end));
    23.6  
    23.7 -fun singleton_infer_param change_sort = (map o map_atyps) (fn T as TVar (vi as (_, i), sort) =>
    23.8 -      if TypeInfer.is_param vi then TypeInfer.param i (Name.aT, change_sort sort)
    23.9 +val singleton_infer_param = (map o map_atyps) (fn T as TVar (vi as (_, i), sort) =>
   23.10 +      if TypeInfer.is_param vi then TypeInfer.param i (Name.aT, sort)
   23.11        else error ("Illegal schematic type variable in class specification: " ^ Term.string_of_vname vi)
   23.12          (*FIXME does not occur*)
   23.13    | T as TFree (v, sort) =>
   23.14 @@ -119,11 +119,12 @@
   23.15    let
   23.16      (* prepare import *)
   23.17      val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy));
   23.18 -    val (sups, others_basesort) = map (prep_class thy) raw_supclasses
   23.19 -      |> Sign.minimize_sort thy
   23.20 -      |> List.partition (is_class thy);
   23.21 -
   23.22 -    val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
   23.23 +    val sups = map (prep_class thy) raw_supclasses
   23.24 +      |> Sign.minimize_sort thy;
   23.25 +    val _ = case filter_out (is_class thy) sups
   23.26 +     of [] => ()
   23.27 +      | no_classes => error ("These are not classes: " ^ commas (map quote no_classes));
   23.28 +          val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
   23.29      val supparam_names = map fst supparams;
   23.30      val _ = if has_duplicates (op =) supparam_names
   23.31        then error ("Duplicate parameter(s) in superclasses: "
   23.32 @@ -131,7 +132,7 @@
   23.33        else ();
   23.34      val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional [])))
   23.35        sups, []);
   23.36 -    val given_basesort = fold inter_sort (map (base_sort thy) sups) others_basesort;
   23.37 +    val given_basesort = fold inter_sort (map (base_sort thy) sups) [];
   23.38  
   23.39      (* infer types and base sort *)
   23.40      val base_constraints = (map o apsnd)
   23.41 @@ -139,10 +140,9 @@
   23.42          (these_operations thy sups);
   23.43      val ((_, _, inferred_elems), _) = ProofContext.init thy
   23.44        |> fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
   23.45 -      |> add_typ_check ~1 "singleton_infer_param" (singleton_infer_param (inter_sort given_basesort))
   23.46 +      |> add_typ_check ~1 "singleton_infer_param" singleton_infer_param
   23.47        |> add_typ_check ~2 "singleton_fixate" singleton_fixate
   23.48        |> prep_decl supexpr raw_elems;
   23.49 -    (*FIXME propagation of given base sort into class spec broken*)
   23.50      (*FIXME check for *all* side conditions here, extra check function for elements,
   23.51        less side-condition checks in check phase*)
   23.52      val base_sort = if null inferred_elems then given_basesort else
   23.53 @@ -170,45 +170,6 @@
   23.54  val cert_class_spec = prep_class_spec (K I) Expression.cert_declaration;
   23.55  val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration;
   23.56  
   23.57 -(*fun prep_class_spec prep_class process_decl thy raw_supclasses raw_elems =
   23.58 -  let
   23.59 -    (*FIXME 2009 simplify*)
   23.60 -    val supclasses = map (prep_class thy) raw_supclasses;
   23.61 -    val supsort = Sign.minimize_sort thy supclasses;
   23.62 -    val (sups, bases) = List.partition (is_class thy) supsort;
   23.63 -    val base_sort = if null sups then supsort else
   23.64 -      Library.foldr (Sorts.inter_sort (Sign.classes_of thy))
   23.65 -        (map (base_sort thy) sups, bases);
   23.66 -    val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
   23.67 -    val supparam_names = map fst supparams;
   23.68 -    val _ = if has_duplicates (op =) supparam_names
   23.69 -      then error ("Duplicate parameter(s) in superclasses: "
   23.70 -        ^ (commas o map quote o duplicates (op =)) supparam_names)
   23.71 -      else ();
   23.72 -
   23.73 -    val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional [])))
   23.74 -      sups, []);
   23.75 -    val constrain = Element.Constrains ((map o apsnd o map_atyps)
   23.76 -      (K (TFree (Name.aT, base_sort))) supparams);
   23.77 -      (*FIXME 2009 perhaps better: control type variable by explicit
   23.78 -      parameter instantiation of import expression*)
   23.79 -    val begin_ctxt = begin sups base_sort
   23.80 -      #> fold (Variable.declare_constraints o Free) ((map o apsnd o map_atyps)
   23.81 -          (K (TFree (Name.aT, base_sort))) supparams) (*FIXME
   23.82 -            should constraints be issued in begin?*)
   23.83 -    val ((_, _, syntax_elems), _) = ProofContext.init thy
   23.84 -      |> begin_ctxt
   23.85 -      |> process_decl supexpr raw_elems;
   23.86 -    fun fork_syn (Element.Fixes xs) =
   23.87 -          fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs
   23.88 -          #>> Element.Fixes
   23.89 -      | fork_syn x = pair x;
   23.90 -    val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
   23.91 -  in (((sups, supparam_names), (supsort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end;
   23.92 -
   23.93 -val cert_class_spec = prep_class_spec (K I) Expression.cert_declaration;
   23.94 -val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration;*)
   23.95 -
   23.96  fun add_consts bname class base_sort sups supparams global_syntax thy =
   23.97    let
   23.98      (*FIXME 2009 simplify*)
    24.1 --- a/src/Pure/Isar/class_target.ML	Wed Jan 21 23:25:17 2009 +0100
    24.2 +++ b/src/Pure/Isar/class_target.ML	Wed Jan 21 23:42:37 2009 +0100
    24.3 @@ -55,8 +55,6 @@
    24.4      -> (Attrib.binding * string list) list
    24.5      -> theory -> class * theory
    24.6    val classrel_cmd: xstring * xstring -> theory -> Proof.state
    24.7 -
    24.8 -  (*old instance layer*)
    24.9    val instance_arity: (theory -> theory) -> arity -> theory -> Proof.state
   24.10    val instance_arity_cmd: bstring * xstring list * xstring -> theory -> Proof.state
   24.11  end;
   24.12 @@ -275,7 +273,7 @@
   24.13      val intros = (snd o rules thy) sup :: map_filter I
   24.14        [Option.map (Drule.standard' o Element.conclude_witness) some_wit,
   24.15          (fst o rules thy) sub];
   24.16 -    val tac = ALLGOALS (EVERY' (map Tactic.rtac intros));
   24.17 +    val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
   24.18      val classrel = Goal.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
   24.19        (K tac);
   24.20      val diff_sort = Sign.complete_sort thy [sup]
   24.21 @@ -285,9 +283,9 @@
   24.22      |> AxClass.add_classrel classrel
   24.23      |> ClassData.map (Graph.add_edge (sub, sup))
   24.24      |> activate_defs sub (these_defs thy diff_sort)
   24.25 -    |> fold2 (fn dep_morph => fn wit => Locale.add_dependency sub (sup,
   24.26 -        dep_morph $> Element.satisfy_morphism [wit] $> export))
   24.27 -          (the_list some_dep_morph) (the_list some_wit)
   24.28 +    |> fold (fn dep_morph => Locale.add_dependency sub (sup,
   24.29 +        dep_morph $> Element.satisfy_morphism (the_list some_wit) $> export))
   24.30 +          (the_list some_dep_morph)
   24.31      |> (fn thy => fold_rev Locale.activate_global_facts
   24.32        (Locale.get_registrations thy) thy)
   24.33    end;
    25.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Jan 21 23:25:17 2009 +0100
    25.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Jan 21 23:42:37 2009 +0100
    25.3 @@ -428,7 +428,7 @@
    25.4  
    25.5  val _ =
    25.6    OuterSyntax.command "class" "define type class" K.thy_decl
    25.7 -   (P.name -- (P.$$$ "=" |-- class_val) -- P.opt_begin
    25.8 +   (P.name -- Scan.optional (P.$$$ "=" |-- class_val) ([], []) -- P.opt_begin
    25.9      >> (fn ((name, (supclasses, elems)), begin) =>
   25.10          (begin ? Toplevel.print) o Toplevel.begin_local_theory begin
   25.11            (Class.class_cmd name supclasses elems #> snd)));