--- a/NEWS Wed Jan 21 23:25:17 2009 +0100
+++ b/NEWS Wed Jan 21 23:42:37 2009 +0100
@@ -66,6 +66,12 @@
*** Pure ***
+* Class declaration: sc. "base sort" must not be given in import list
+any longer but is inferred from the specification. Particularly in HOL,
+write
+
+ class foo = ... instead of class foo = type + ...
+
* Type Binding.T gradually replaces formerly used type bstring for names
to be bound. Name space interface for declarations has been simplified:
--- a/src/HOL/ATP_Linkup.thy Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOL/ATP_Linkup.thy Wed Jan 21 23:42:37 2009 +0100
@@ -7,7 +7,7 @@
header {* The Isabelle-ATP Linkup *}
theory ATP_Linkup
-imports Record Hilbert_Choice
+imports Divides Record Hilbert_Choice
uses
"Tools/polyhash.ML"
"Tools/res_clause.ML"
--- a/src/HOL/Datatype.thy Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOL/Datatype.thy Wed Jan 21 23:42:37 2009 +0100
@@ -8,7 +8,7 @@
header {* Analogues of the Cartesian Product and Disjoint Sum for Datatypes *}
theory Datatype
-imports Nat Relation
+imports Nat Product_Type
begin
typedef (Node)
@@ -509,15 +509,6 @@
lemmas dsum_subset_Sigma = subset_trans [OF dsum_mono dsum_Sigma, standard]
-(*** Domain ***)
-
-lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
-by auto
-
-lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
-by auto
-
-
text {* hides popular names *}
hide (open) type node item
hide (open) const Push Node Atom Leaf Numb Lim Split Case
--- a/src/HOL/Finite_Set.thy Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOL/Finite_Set.thy Wed Jan 21 23:42:37 2009 +0100
@@ -6,7 +6,7 @@
header {* Finite sets *}
theory Finite_Set
-imports Datatype Divides Transitive_Closure
+imports Nat Product_Type Power
begin
subsection {* Definition and basic properties *}
@@ -380,46 +380,6 @@
by(blast intro: finite_subset[OF subset_Pow_Union])
-lemma finite_converse [iff]: "finite (r^-1) = finite r"
- apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
- apply simp
- apply (rule iffI)
- apply (erule finite_imageD [unfolded inj_on_def])
- apply (simp split add: split_split)
- apply (erule finite_imageI)
- apply (simp add: converse_def image_def, auto)
- apply (rule bexI)
- prefer 2 apply assumption
- apply simp
- done
-
-
-text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
-Ehmety) *}
-
-lemma finite_Field: "finite r ==> finite (Field r)"
- -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
- apply (induct set: finite)
- apply (auto simp add: Field_def Domain_insert Range_insert)
- done
-
-lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
- apply clarify
- apply (erule trancl_induct)
- apply (auto simp add: Field_def)
- done
-
-lemma finite_trancl: "finite (r^+) = finite r"
- apply auto
- prefer 2
- apply (rule trancl_subset_Field2 [THEN finite_subset])
- apply (rule finite_SigmaI)
- prefer 3
- apply (blast intro: r_into_trancl' finite_subset)
- apply (auto simp add: finite_Field)
- done
-
-
subsection {* Class @{text finite} *}
setup {* Sign.add_path "finite" *} -- {*FIXME: name tweaking*}
@@ -471,9 +431,6 @@
instance "+" :: (finite, finite) finite
by default (simp only: UNIV_Plus_UNIV [symmetric] finite_Plus finite)
-instance option :: (finite) finite
- by default (simp add: insert_None_conv_UNIV [symmetric])
-
subsection {* A fold functional for finite sets *}
--- a/src/HOL/HOL.thy Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOL/HOL.thy Wed Jan 21 23:42:37 2009 +0100
@@ -208,34 +208,34 @@
subsubsection {* Generic classes and algebraic operations *}
-class default = type +
+class default =
fixes default :: 'a
-class zero = type +
+class zero =
fixes zero :: 'a ("0")
-class one = type +
+class one =
fixes one :: 'a ("1")
hide (open) const zero one
-class plus = type +
+class plus =
fixes plus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "+" 65)
-class minus = type +
+class minus =
fixes minus :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "-" 65)
-class uminus = type +
+class uminus =
fixes uminus :: "'a \<Rightarrow> 'a" ("- _" [81] 80)
-class times = type +
+class times =
fixes times :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "*" 70)
-class inverse = type +
+class inverse =
fixes inverse :: "'a \<Rightarrow> 'a"
and divide :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixl "'/" 70)
-class abs = type +
+class abs =
fixes abs :: "'a \<Rightarrow> 'a"
begin
@@ -247,10 +247,10 @@
end
-class sgn = type +
+class sgn =
fixes sgn :: "'a \<Rightarrow> 'a"
-class ord = type +
+class ord =
fixes less_eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
and less :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
begin
@@ -1675,7 +1675,7 @@
text {* Equality *}
-class eq = type +
+class eq =
fixes eq :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
assumes eq_equals: "eq x y \<longleftrightarrow> x = y"
begin
--- a/src/HOL/Int.thy Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOL/Int.thy Wed Jan 21 23:42:37 2009 +0100
@@ -599,7 +599,7 @@
Bit1 :: "int \<Rightarrow> int" where
[code del]: "Bit1 k = 1 + k + k"
-class number = type + -- {* for numeric types: nat, int, real, \dots *}
+class number = -- {* for numeric types: nat, int, real, \dots *}
fixes number_of :: "int \<Rightarrow> 'a"
use "Tools/numeral.ML"
--- a/src/HOL/Library/Eval_Witness.thy Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOL/Library/Eval_Witness.thy Wed Jan 21 23:42:37 2009 +0100
@@ -32,7 +32,7 @@
with the oracle.
*}
-class ml_equiv = type
+class ml_equiv
text {*
Instances of @{text "ml_equiv"} should only be declared for those types,
--- a/src/HOL/Library/Quotient.thy Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOL/Library/Quotient.thy Wed Jan 21 23:42:37 2009 +0100
@@ -21,7 +21,7 @@
"\<sim> :: 'a => 'a => bool"}.
*}
-class eqv = type +
+class eqv =
fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sim>" 50)
class equiv = eqv +
--- a/src/HOL/Nat.thy Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOL/Nat.thy Wed Jan 21 23:42:37 2009 +0100
@@ -1515,7 +1515,7 @@
subsection {* size of a datatype value *}
-class size = type +
+class size =
fixes size :: "'a \<Rightarrow> nat" -- {* see further theory @{text Wellfounded} *}
end
--- a/src/HOL/Nominal/Examples/W.thy Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOL/Nominal/Examples/W.thy Wed Jan 21 23:42:37 2009 +0100
@@ -49,7 +49,7 @@
text {* free type variables *}
-class ftv = type +
+class ftv =
fixes ftv :: "'a \<Rightarrow> tvar list"
instantiation * :: (ftv, ftv) ftv
--- a/src/HOL/Parity.thy Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOL/Parity.thy Wed Jan 21 23:42:37 2009 +0100
@@ -8,7 +8,7 @@
imports Plain Presburger
begin
-class even_odd = type +
+class even_odd =
fixes even :: "'a \<Rightarrow> bool"
abbreviation
--- a/src/HOL/Plain.thy Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOL/Plain.thy Wed Jan 21 23:42:37 2009 +0100
@@ -1,7 +1,7 @@
header {* Plain HOL *}
theory Plain
-imports Datatype FunDef Record SAT Extraction
+imports Datatype FunDef Record SAT Extraction Divides
begin
text {*
@@ -9,6 +9,9 @@
include @{text Hilbert_Choice}.
*}
+instance option :: (finite) finite
+ by default (simp add: insert_None_conv_UNIV [symmetric])
+
ML {* path_add "~~/src/HOL/Library" *}
end
--- a/src/HOL/Power.thy Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOL/Power.thy Wed Jan 21 23:42:37 2009 +0100
@@ -11,7 +11,7 @@
imports Nat
begin
-class power = type +
+class power =
fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80)
subsection{*Powers for Arbitrary Monoids*}
--- a/src/HOL/RealVector.thy Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOL/RealVector.thy Wed Jan 21 23:42:37 2009 +0100
@@ -124,7 +124,7 @@
subsection {* Real vector spaces *}
-class scaleR = type +
+class scaleR =
fixes scaleR :: "real \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "*\<^sub>R" 75)
begin
@@ -418,7 +418,7 @@
subsection {* Real normed vector spaces *}
-class norm = type +
+class norm =
fixes norm :: "'a \<Rightarrow> real"
instantiation real :: norm
--- a/src/HOL/Relation.thy Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOL/Relation.thy Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Relation.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1996 University of Cambridge
*)
@@ -7,7 +6,7 @@
header {* Relations *}
theory Relation
-imports Product_Type
+imports Datatype Finite_Set
begin
subsection {* Definitions *}
@@ -379,6 +378,12 @@
lemma fst_eq_Domain: "fst ` R = Domain R";
by (auto intro!:image_eqI)
+lemma Domain_dprod [simp]: "Domain (dprod r s) = uprod (Domain r) (Domain s)"
+by auto
+
+lemma Domain_dsum [simp]: "Domain (dsum r s) = usum (Domain r) (Domain s)"
+by auto
+
subsection {* Range *}
@@ -566,6 +571,31 @@
done
+subsection {* Finiteness *}
+
+lemma finite_converse [iff]: "finite (r^-1) = finite r"
+ apply (subgoal_tac "r^-1 = (%(x,y). (y,x))`r")
+ apply simp
+ apply (rule iffI)
+ apply (erule finite_imageD [unfolded inj_on_def])
+ apply (simp split add: split_split)
+ apply (erule finite_imageI)
+ apply (simp add: converse_def image_def, auto)
+ apply (rule bexI)
+ prefer 2 apply assumption
+ apply simp
+ done
+
+text {* \paragraph{Finiteness of transitive closure} (Thanks to Sidi
+Ehmety) *}
+
+lemma finite_Field: "finite r ==> finite (Field r)"
+ -- {* A finite relation has a finite field (@{text "= domain \<union> range"}. *}
+ apply (induct set: finite)
+ apply (auto simp add: Field_def Domain_insert Range_insert)
+ done
+
+
subsection {* Version of @{text lfp_induct} for binary relations *}
lemmas lfp_induct2 =
--- a/src/HOL/SizeChange/Kleene_Algebras.thy Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOL/SizeChange/Kleene_Algebras.thy Wed Jan 21 23:42:37 2009 +0100
@@ -11,7 +11,7 @@
text {* A type class of kleene algebras *}
-class star = type +
+class star =
fixes star :: "'a \<Rightarrow> 'a"
class idem_add = ab_semigroup_add +
--- a/src/HOL/Transitive_Closure.thy Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOL/Transitive_Closure.thy Wed Jan 21 23:42:37 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/Transitive_Closure.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
*)
@@ -568,6 +567,22 @@
apply auto
done
+lemma trancl_subset_Field2: "r^+ <= Field r \<times> Field r"
+ apply clarify
+ apply (erule trancl_induct)
+ apply (auto simp add: Field_def)
+ done
+
+lemma finite_trancl: "finite (r^+) = finite r"
+ apply auto
+ prefer 2
+ apply (rule trancl_subset_Field2 [THEN finite_subset])
+ apply (rule finite_SigmaI)
+ prefer 3
+ apply (blast intro: r_into_trancl' finite_subset)
+ apply (auto simp add: finite_Field)
+ done
+
text {* More about converse @{text rtrancl} and @{text trancl}, should
be merged with main body. *}
--- a/src/HOL/Typedef.thy Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOL/Typedef.thy Wed Jan 21 23:42:37 2009 +0100
@@ -123,7 +123,7 @@
text {* This class is just a workaround for classes without parameters;
it shall disappear as soon as possible. *}
-class itself = type +
+class itself =
fixes itself :: "'a itself"
setup {*
--- a/src/HOL/Wellfounded.thy Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOL/Wellfounded.thy Wed Jan 21 23:42:37 2009 +0100
@@ -7,7 +7,7 @@
header {*Well-founded Recursion*}
theory Wellfounded
-imports Finite_Set Nat
+imports Finite_Set Transitive_Closure Nat
uses ("Tools/function_package/size.ML")
begin
--- a/src/HOL/Word/BitSyntax.thy Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOL/Word/BitSyntax.thy Wed Jan 21 23:42:37 2009 +0100
@@ -12,7 +12,7 @@
imports BinGeneral
begin
-class bit = type +
+class bit =
fixes bitNOT :: "'a \<Rightarrow> 'a" ("NOT _" [70] 71)
and bitAND :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "AND" 64)
and bitOR :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" (infixr "OR" 59)
--- a/src/HOL/Word/Size.thy Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOL/Word/Size.thy Wed Jan 21 23:42:37 2009 +0100
@@ -18,7 +18,7 @@
some duplication with the definitions in @{text "Numeral_Type"}.
*}
-class len0 = type +
+class len0 =
fixes len_of :: "'a itself \<Rightarrow> nat"
text {*
--- a/src/HOLCF/Porder.thy Wed Jan 21 23:25:17 2009 +0100
+++ b/src/HOLCF/Porder.thy Wed Jan 21 23:42:37 2009 +0100
@@ -10,7 +10,7 @@
subsection {* Type class for partial orders *}
-class sq_ord = type +
+class sq_ord =
fixes sq_le :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
notation
--- a/src/Pure/Isar/class.ML Wed Jan 21 23:25:17 2009 +0100
+++ b/src/Pure/Isar/class.ML Wed Jan 21 23:42:37 2009 +0100
@@ -92,8 +92,8 @@
fun add_typ_check level name f = Context.proof_map (Syntax.add_typ_check level name (fn xs => fn ctxt =>
let val xs' = f xs in if eq_list (op =) (xs, xs') then NONE else SOME (xs', ctxt) end));
-fun singleton_infer_param change_sort = (map o map_atyps) (fn T as TVar (vi as (_, i), sort) =>
- if TypeInfer.is_param vi then TypeInfer.param i (Name.aT, change_sort sort)
+val singleton_infer_param = (map o map_atyps) (fn T as TVar (vi as (_, i), sort) =>
+ if TypeInfer.is_param vi then TypeInfer.param i (Name.aT, sort)
else error ("Illegal schematic type variable in class specification: " ^ Term.string_of_vname vi)
(*FIXME does not occur*)
| T as TFree (v, sort) =>
@@ -119,11 +119,12 @@
let
(* prepare import *)
val inter_sort = curry (Sorts.inter_sort (Sign.classes_of thy));
- val (sups, others_basesort) = map (prep_class thy) raw_supclasses
- |> Sign.minimize_sort thy
- |> List.partition (is_class thy);
-
- val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
+ val sups = map (prep_class thy) raw_supclasses
+ |> Sign.minimize_sort thy;
+ val _ = case filter_out (is_class thy) sups
+ of [] => ()
+ | no_classes => error ("These are not classes: " ^ commas (map quote no_classes));
+ val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
val supparam_names = map fst supparams;
val _ = if has_duplicates (op =) supparam_names
then error ("Duplicate parameter(s) in superclasses: "
@@ -131,7 +132,7 @@
else ();
val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional [])))
sups, []);
- val given_basesort = fold inter_sort (map (base_sort thy) sups) others_basesort;
+ val given_basesort = fold inter_sort (map (base_sort thy) sups) [];
(* infer types and base sort *)
val base_constraints = (map o apsnd)
@@ -139,10 +140,9 @@
(these_operations thy sups);
val ((_, _, inferred_elems), _) = ProofContext.init thy
|> fold (ProofContext.add_const_constraint o apsnd SOME) base_constraints
- |> add_typ_check ~1 "singleton_infer_param" (singleton_infer_param (inter_sort given_basesort))
+ |> add_typ_check ~1 "singleton_infer_param" singleton_infer_param
|> add_typ_check ~2 "singleton_fixate" singleton_fixate
|> prep_decl supexpr raw_elems;
- (*FIXME propagation of given base sort into class spec broken*)
(*FIXME check for *all* side conditions here, extra check function for elements,
less side-condition checks in check phase*)
val base_sort = if null inferred_elems then given_basesort else
@@ -170,45 +170,6 @@
val cert_class_spec = prep_class_spec (K I) Expression.cert_declaration;
val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration;
-(*fun prep_class_spec prep_class process_decl thy raw_supclasses raw_elems =
- let
- (*FIXME 2009 simplify*)
- val supclasses = map (prep_class thy) raw_supclasses;
- val supsort = Sign.minimize_sort thy supclasses;
- val (sups, bases) = List.partition (is_class thy) supsort;
- val base_sort = if null sups then supsort else
- Library.foldr (Sorts.inter_sort (Sign.classes_of thy))
- (map (base_sort thy) sups, bases);
- val supparams = (map o apsnd) (snd o snd) (these_params thy sups);
- val supparam_names = map fst supparams;
- val _ = if has_duplicates (op =) supparam_names
- then error ("Duplicate parameter(s) in superclasses: "
- ^ (commas o map quote o duplicates (op =)) supparam_names)
- else ();
-
- val supexpr = (map (fn sup => (sup, (("", false), Expression.Positional [])))
- sups, []);
- val constrain = Element.Constrains ((map o apsnd o map_atyps)
- (K (TFree (Name.aT, base_sort))) supparams);
- (*FIXME 2009 perhaps better: control type variable by explicit
- parameter instantiation of import expression*)
- val begin_ctxt = begin sups base_sort
- #> fold (Variable.declare_constraints o Free) ((map o apsnd o map_atyps)
- (K (TFree (Name.aT, base_sort))) supparams) (*FIXME
- should constraints be issued in begin?*)
- val ((_, _, syntax_elems), _) = ProofContext.init thy
- |> begin_ctxt
- |> process_decl supexpr raw_elems;
- fun fork_syn (Element.Fixes xs) =
- fold_map (fn (c, ty, syn) => cons (Binding.base_name c, syn) #> pair (c, ty, NoSyn)) xs
- #>> Element.Fixes
- | fork_syn x = pair x;
- val (elems, global_syntax) = fold_map fork_syn syntax_elems [];
- in (((sups, supparam_names), (supsort, base_sort, supexpr)), (constrain :: elems, global_syntax)) end;
-
-val cert_class_spec = prep_class_spec (K I) Expression.cert_declaration;
-val read_class_spec = prep_class_spec Sign.intern_class Expression.cert_read_declaration;*)
-
fun add_consts bname class base_sort sups supparams global_syntax thy =
let
(*FIXME 2009 simplify*)
--- a/src/Pure/Isar/class_target.ML Wed Jan 21 23:25:17 2009 +0100
+++ b/src/Pure/Isar/class_target.ML Wed Jan 21 23:42:37 2009 +0100
@@ -55,8 +55,6 @@
-> (Attrib.binding * string list) list
-> theory -> class * theory
val classrel_cmd: xstring * xstring -> theory -> Proof.state
-
- (*old instance layer*)
val instance_arity: (theory -> theory) -> arity -> theory -> Proof.state
val instance_arity_cmd: bstring * xstring list * xstring -> theory -> Proof.state
end;
@@ -275,7 +273,7 @@
val intros = (snd o rules thy) sup :: map_filter I
[Option.map (Drule.standard' o Element.conclude_witness) some_wit,
(fst o rules thy) sub];
- val tac = ALLGOALS (EVERY' (map Tactic.rtac intros));
+ val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
val classrel = Goal.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
(K tac);
val diff_sort = Sign.complete_sort thy [sup]
@@ -285,9 +283,9 @@
|> AxClass.add_classrel classrel
|> ClassData.map (Graph.add_edge (sub, sup))
|> activate_defs sub (these_defs thy diff_sort)
- |> fold2 (fn dep_morph => fn wit => Locale.add_dependency sub (sup,
- dep_morph $> Element.satisfy_morphism [wit] $> export))
- (the_list some_dep_morph) (the_list some_wit)
+ |> fold (fn dep_morph => Locale.add_dependency sub (sup,
+ dep_morph $> Element.satisfy_morphism (the_list some_wit) $> export))
+ (the_list some_dep_morph)
|> (fn thy => fold_rev Locale.activate_global_facts
(Locale.get_registrations thy) thy)
end;
--- a/src/Pure/Isar/isar_syn.ML Wed Jan 21 23:25:17 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML Wed Jan 21 23:42:37 2009 +0100
@@ -428,7 +428,7 @@
val _ =
OuterSyntax.command "class" "define type class" K.thy_decl
- (P.name -- (P.$$$ "=" |-- class_val) -- P.opt_begin
+ (P.name -- Scan.optional (P.$$$ "=" |-- class_val) ([], []) -- P.opt_begin
>> (fn ((name, (supclasses, elems)), begin) =>
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin
(Class.class_cmd name supclasses elems #> snd)));