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)));