--- a/src/HOL/Algebra/abstract/Ideal2.thy Mon Feb 22 17:02:39 2010 +0100
+++ b/src/HOL/Algebra/abstract/Ideal2.thy Tue Feb 23 10:11:12 2010 +0100
@@ -1,6 +1,5 @@
(*
Ideals for commutative rings
- $Id$
Author: Clemens Ballarin, started 24 September 1999
*)
@@ -23,9 +22,8 @@
text {* Principle ideal domains *}
-axclass pid < "domain"
- pid_ax: "is_ideal I ==> is_pideal I"
-
+class pid =
+ assumes pid_ax: "is_ideal (I :: 'a::domain \<Rightarrow> _) \<Longrightarrow> is_pideal I"
(* is_ideal *)
--- a/src/HOL/Bali/Decl.thy Mon Feb 22 17:02:39 2010 +0100
+++ b/src/HOL/Bali/Decl.thy Tue Feb 23 10:11:12 2010 +0100
@@ -230,18 +230,22 @@
datatype memberid = fid vname | mid sig
-axclass has_memberid < "type"
-consts
- memberid :: "'a::has_memberid \<Rightarrow> memberid"
+class has_memberid =
+ fixes memberid :: "'a \<Rightarrow> memberid"
-instance memberdecl::has_memberid ..
+instantiation memberdecl :: has_memberid
+begin
-defs (overloaded)
+definition
memberdecl_memberid_def:
"memberid m \<equiv> (case m of
fdecl (vn,f) \<Rightarrow> fid vn
| mdecl (sig,m) \<Rightarrow> mid sig)"
+instance ..
+
+end
+
lemma memberid_fdecl_simp[simp]: "memberid (fdecl (vn,f)) = fid vn"
by (simp add: memberdecl_memberid_def)
@@ -254,12 +258,17 @@
lemma memberid_mdecl_simp1: "memberid (mdecl m) = mid (fst m)"
by (cases m) (simp add: memberdecl_memberid_def)
-instance * :: (type, has_memberid) has_memberid ..
+instantiation * :: (type, has_memberid) has_memberid
+begin
-defs (overloaded)
+definition
pair_memberid_def:
"memberid p \<equiv> memberid (snd p)"
+instance ..
+
+end
+
lemma memberid_pair_simp[simp]: "memberid (c,m) = memberid m"
by (simp add: pair_memberid_def)
--- a/src/HOL/Bali/DeclConcepts.thy Mon Feb 22 17:02:39 2010 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy Tue Feb 23 10:11:12 2010 +0100
@@ -79,41 +79,60 @@
text {* overloaded selector @{text accmodi} to select the access modifier
out of various HOL types *}
-axclass has_accmodi < "type"
-consts accmodi:: "'a::has_accmodi \<Rightarrow> acc_modi"
+class has_accmodi =
+ fixes accmodi:: "'a \<Rightarrow> acc_modi"
+
+instantiation acc_modi :: has_accmodi
+begin
-instance acc_modi::has_accmodi ..
+definition
+ acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a"
-defs (overloaded)
-acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a"
+instance ..
+
+end
lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a"
by (simp add: acc_modi_accmodi_def)
-instance decl_ext_type:: ("type") has_accmodi ..
+instantiation decl_ext_type:: (type) has_accmodi
+begin
-defs (overloaded)
-decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d"
+definition
+ decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d"
+instance ..
+
+end
lemma decl_acc_modi_simp[simp]: "accmodi (d::('a::type) decl_scheme) = access d"
by (simp add: decl_acc_modi_def)
-instance * :: ("type",has_accmodi) has_accmodi ..
+instantiation * :: (type, has_accmodi) has_accmodi
+begin
-defs (overloaded)
-pair_acc_modi_def: "accmodi p \<equiv> (accmodi (snd p))"
+definition
+ pair_acc_modi_def: "accmodi p \<equiv> (accmodi (snd p))"
+
+instance ..
+
+end
lemma pair_acc_modi_simp[simp]: "accmodi (x,a) = (accmodi a)"
by (simp add: pair_acc_modi_def)
-instance memberdecl :: has_accmodi ..
+instantiation memberdecl :: has_accmodi
+begin
-defs (overloaded)
-memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of
+definition
+ memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of
fdecl f \<Rightarrow> accmodi f
| mdecl m \<Rightarrow> accmodi m)"
+instance ..
+
+end
+
lemma memberdecl_fdecl_acc_modi_simp[simp]:
"accmodi (fdecl m) = accmodi m"
by (simp add: memberdecl_acc_modi_def)
@@ -125,21 +144,35 @@
text {* overloaded selector @{text declclass} to select the declaring class
out of various HOL types *}
-axclass has_declclass < "type"
-consts declclass:: "'a::has_declclass \<Rightarrow> qtname"
+class has_declclass =
+ fixes declclass:: "'a \<Rightarrow> qtname"
+
+instantiation qtname_ext_type :: (type) has_declclass
+begin
-instance qtname_ext_type::("type") has_declclass ..
+definition
+ "declclass q \<equiv> \<lparr> pid = pid q, tid = tid q \<rparr>"
+
+instance ..
-defs (overloaded)
-qtname_declclass_def: "declclass (q::qtname) \<equiv> q"
+end
+
+lemma qtname_declclass_def:
+ "declclass q \<equiv> (q::qtname)"
+ by (induct q) (simp add: declclass_qtname_ext_type_def)
lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q"
by (simp add: qtname_declclass_def)
-instance * :: ("has_declclass","type") has_declclass ..
+instantiation * :: (has_declclass, type) has_declclass
+begin
-defs (overloaded)
-pair_declclass_def: "declclass p \<equiv> declclass (fst p)"
+definition
+ pair_declclass_def: "declclass p \<equiv> declclass (fst p)"
+
+instance ..
+
+end
lemma pair_declclass_simp[simp]: "declclass (c,x) = declclass c"
by (simp add: pair_declclass_def)
@@ -147,25 +180,38 @@
text {* overloaded selector @{text is_static} to select the static modifier
out of various HOL types *}
+class has_static =
+ fixes is_static :: "'a \<Rightarrow> bool"
-axclass has_static < "type"
-consts is_static :: "'a::has_static \<Rightarrow> bool"
+instantiation decl_ext_type :: (has_static) has_static
+begin
-instance decl_ext_type :: ("has_static") has_static ..
+instance ..
+
+end
-instance member_ext_type :: ("type") has_static ..
+instantiation member_ext_type :: (type) has_static
+begin
+
+instance ..
-defs (overloaded)
-static_field_type_is_static_def:
- "is_static (m::('b member_scheme)) \<equiv> static m"
+end
+
+axiomatization where
+ static_field_type_is_static_def: "is_static (m::('a member_scheme)) \<equiv> static m"
lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m"
by (simp add: static_field_type_is_static_def)
-instance * :: ("type","has_static") has_static ..
+instantiation * :: (type, has_static) has_static
+begin
-defs (overloaded)
-pair_is_static_def: "is_static p \<equiv> is_static (snd p)"
+definition
+ pair_is_static_def: "is_static p \<equiv> is_static (snd p)"
+
+instance ..
+
+end
lemma pair_is_static_simp [simp]: "is_static (x,s) = is_static s"
by (simp add: pair_is_static_def)
@@ -173,14 +219,19 @@
lemma pair_is_static_simp1: "is_static p = is_static (snd p)"
by (simp add: pair_is_static_def)
-instance memberdecl:: has_static ..
+instantiation memberdecl :: has_static
+begin
-defs (overloaded)
+definition
memberdecl_is_static_def:
"is_static m \<equiv> (case m of
fdecl f \<Rightarrow> is_static f
| mdecl m \<Rightarrow> is_static m)"
+instance ..
+
+end
+
lemma memberdecl_is_static_fdecl_simp[simp]:
"is_static (fdecl f) = is_static f"
by (simp add: memberdecl_is_static_def)
@@ -389,18 +440,32 @@
text {* overloaded selector @{text resTy} to select the result type
out of various HOL types *}
-axclass has_resTy < "type"
-consts resTy:: "'a::has_resTy \<Rightarrow> ty"
+class has_resTy =
+ fixes resTy:: "'a \<Rightarrow> ty"
+
+instantiation decl_ext_type :: (has_resTy) has_resTy
+begin
-instance decl_ext_type :: ("has_resTy") has_resTy ..
+instance ..
+
+end
+
+instantiation member_ext_type :: (has_resTy) has_resTy
+begin
-instance member_ext_type :: ("has_resTy") has_resTy ..
+instance ..
-instance mhead_ext_type :: ("type") has_resTy ..
+end
+
+instantiation mhead_ext_type :: (type) has_resTy
+begin
-defs (overloaded)
-mhead_ext_type_resTy_def:
- "resTy (m::('b mhead_scheme)) \<equiv> resT m"
+instance ..
+
+end
+
+axiomatization where
+ mhead_ext_type_resTy_def: "resTy (m::('b mhead_scheme)) \<equiv> resT m"
lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m"
by (simp add: mhead_ext_type_resTy_def)
@@ -408,10 +473,15 @@
lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m"
by (simp add: mhead_def mhead_resTy_simp)
-instance * :: ("type","has_resTy") has_resTy ..
+instantiation * :: ("type","has_resTy") has_resTy
+begin
-defs (overloaded)
-pair_resTy_def: "resTy p \<equiv> resTy (snd p)"
+definition
+ pair_resTy_def: "resTy p \<equiv> resTy (snd p)"
+
+instance ..
+
+end
lemma pair_resTy_simp[simp]: "resTy (x,m) = resTy m"
by (simp add: pair_resTy_def)
--- a/src/HOL/Bali/Name.thy Mon Feb 22 17:02:39 2010 +0100
+++ b/src/HOL/Bali/Name.thy Tue Feb 23 10:11:12 2010 +0100
@@ -48,29 +48,34 @@
pid :: pname
tid :: tname
-axclass has_pname < "type"
-consts pname::"'a::has_pname \<Rightarrow> pname"
+class has_pname =
+ fixes pname :: "'a \<Rightarrow> pname"
-instance pname::has_pname ..
+instantiation pname :: has_pname
+begin
-defs (overloaded)
-pname_pname_def: "pname (p::pname) \<equiv> p"
+definition
+ pname_pname_def: "pname (p::pname) \<equiv> p"
-axclass has_tname < "type"
-consts tname::"'a::has_tname \<Rightarrow> tname"
+instance ..
+
+end
-instance tname::has_tname ..
+class has_tname =
+ fixes tname :: "'a \<Rightarrow> tname"
-defs (overloaded)
-tname_tname_def: "tname (t::tname) \<equiv> t"
+instantiation tname :: has_tname
+begin
-axclass has_qtname < type
-consts qtname:: "'a::has_qtname \<Rightarrow> qtname"
+definition
+ tname_tname_def: "tname (t::tname) \<equiv> t"
+
+instance ..
-instance qtname_ext_type :: (type) has_qtname ..
+end
-defs (overloaded)
-qtname_qtname_def: "qtname (q::qtname) \<equiv> q"
+definition
+ qtname_qtname_def: "qtname (q::'a qtname_ext_type) \<equiv> q"
translations
"mname" <= "Name.mname"
--- a/src/HOL/Bali/Term.thy Mon Feb 22 17:02:39 2010 +0100
+++ b/src/HOL/Bali/Term.thy Tue Feb 23 10:11:12 2010 +0100
@@ -295,8 +295,8 @@
following.
*}
-axclass inj_term < "type"
-consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 1000)
+class inj_term =
+ fixes inj_term:: "'a \<Rightarrow> term" ("\<langle>_\<rangle>" 1000)
text {* How this overloaded injections work can be seen in the theory
@{text DefiniteAssignment}. Other big inductive relations on
@@ -308,10 +308,15 @@
as bridge between the different conventions.
*}
-instance stmt::inj_term ..
+instantiation stmt :: inj_term
+begin
-defs (overloaded)
-stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
+definition
+ stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c"
+
+instance ..
+
+end
lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c"
by (simp add: stmt_inj_term_def)
@@ -319,10 +324,15 @@
lemma stmt_inj_term [iff]: "\<langle>x::stmt\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
by (simp add: stmt_inj_term_simp)
-instance expr::inj_term ..
+instantiation expr :: inj_term
+begin
-defs (overloaded)
-expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
+definition
+ expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e"
+
+instance ..
+
+end
lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e"
by (simp add: expr_inj_term_def)
@@ -330,10 +340,15 @@
lemma expr_inj_term [iff]: "\<langle>x::expr\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
by (simp add: expr_inj_term_simp)
-instance var::inj_term ..
+instantiation var :: inj_term
+begin
-defs (overloaded)
-var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
+definition
+ var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v"
+
+instance ..
+
+end
lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v"
by (simp add: var_inj_term_def)
@@ -341,10 +356,32 @@
lemma var_inj_term [iff]: "\<langle>x::var\<rangle> = \<langle>y\<rangle> \<equiv> x = y"
by (simp add: var_inj_term_simp)
-instance "list":: (type) inj_term ..
+class expr_of =
+ fixes expr_of :: "'a \<Rightarrow> expr"
+
+instantiation expr :: expr_of
+begin
+
+definition
+ "expr_of = (\<lambda>(e::expr). e)"
+
+instance ..
+
+end
-defs (overloaded)
-expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es"
+instantiation list :: (expr_of) inj_term
+begin
+
+definition
+ "\<langle>es::'a list\<rangle> \<equiv> In3 (map expr_of es)"
+
+instance ..
+
+end
+
+lemma expr_list_inj_term_def:
+ "\<langle>es::expr list\<rangle> \<equiv> In3 es"
+ by (simp add: inj_term_list_def expr_of_expr_def)
lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es"
by (simp add: expr_list_inj_term_def)
--- a/src/HOL/ex/PER.thy Mon Feb 22 17:02:39 2010 +0100
+++ b/src/HOL/ex/PER.thy Tue Feb 23 10:11:12 2010 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/ex/PER.thy
- ID: $Id$
Author: Oscar Slotosch and Markus Wenzel, TU Muenchen
*)
@@ -30,12 +29,10 @@
but not necessarily reflexive.
*}
-consts
- eqv :: "'a => 'a => bool" (infixl "\<sim>" 50)
-
-axclass partial_equiv < type
- partial_equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
- partial_equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
+class partial_equiv =
+ fixes eqv :: "'a => 'a => bool" (infixl "\<sim>" 50)
+ assumes partial_equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
+ assumes partial_equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
text {*
\medskip The domain of a partial equivalence relation is the set of
@@ -70,7 +67,10 @@
structural one corresponding to the congruence property.
*}
-defs (overloaded)
+instantiation "fun" :: (partial_equiv, partial_equiv) partial_equiv
+begin
+
+definition
eqv_fun_def: "f \<sim> g == \<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y --> f x \<sim> g y"
lemma partial_equiv_funI [intro?]:
@@ -86,8 +86,7 @@
spaces (in \emph{both} argument positions).
*}
-instance "fun" :: (partial_equiv, partial_equiv) partial_equiv
-proof
+instance proof
fix f g h :: "'a::partial_equiv => 'b::partial_equiv"
assume fg: "f \<sim> g"
show "g \<sim> f"
@@ -110,6 +109,8 @@
qed
qed
+end
+
subsection {* Total equivalence *}
@@ -120,8 +121,8 @@
symmetric.
*}
-axclass equiv < partial_equiv
- eqv_refl [intro]: "x \<sim> x"
+class equiv =
+ assumes eqv_refl [intro]: "x \<sim> x"
text {*
On total equivalences all elements are reflexive, and congruence
@@ -150,7 +151,7 @@
\emph{equivalence classes} over elements of the base type @{typ 'a}.
*}
-typedef 'a quot = "{{x. a \<sim> x}| a::'a. True}"
+typedef 'a quot = "{{x. a \<sim> x}| a::'a::partial_equiv. True}"
by blast
lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"
--- a/src/HOL/ex/Refute_Examples.thy Mon Feb 22 17:02:39 2010 +0100
+++ b/src/HOL/ex/Refute_Examples.thy Tue Feb 23 10:11:12 2010 +0100
@@ -1417,29 +1417,20 @@
(*****************************************************************************)
-subsubsection {* Axiomatic type classes and overloading *}
+subsubsection {* Type classes and overloading *}
text {* A type class without axioms: *}
-axclass classA
+class classA
lemma "P (x::'a::classA)"
refute
oops
-text {* The axiom of this type class does not contain any type variables: *}
-
-axclass classB
- classB_ax: "P | ~ P"
-
-lemma "P (x::'a::classB)"
- refute
-oops
-
text {* An axiom with a type variable (denoting types which have at least two elements): *}
-axclass classC < type
- classC_ax: "\<exists>x y. x \<noteq> y"
+class classC =
+ assumes classC_ax: "\<exists>x y. x \<noteq> y"
lemma "P (x::'a::classC)"
refute
@@ -1451,11 +1442,9 @@
text {* A type class for which a constant is defined: *}
-consts
- classD_const :: "'a \<Rightarrow> 'a"
-
-axclass classD < type
- classD_ax: "classD_const (classD_const x) = classD_const x"
+class classD =
+ fixes classD_const :: "'a \<Rightarrow> 'a"
+ assumes classD_ax: "classD_const (classD_const x) = classD_const x"
lemma "P (x::'a::classD)"
refute
@@ -1463,16 +1452,12 @@
text {* A type class with multiple superclasses: *}
-axclass classE < classC, classD
+class classE = classC + classD
lemma "P (x::'a::classE)"
refute
oops
-lemma "P (x::'a::{classB, classE})"
- refute
-oops
-
text {* OFCLASS: *}
lemma "OFCLASS('a::type, type_class)"
@@ -1485,12 +1470,6 @@
apply intro_classes
done
-lemma "OFCLASS('a, classB_class)"
- refute -- {* no countermodel exists *}
- apply intro_classes
- apply simp
-done
-
lemma "OFCLASS('a::type, classC_class)"
refute
oops
--- a/src/Pure/Isar/class_target.ML Mon Feb 22 17:02:39 2010 +0100
+++ b/src/Pure/Isar/class_target.ML Tue Feb 23 10:11:12 2010 +0100
@@ -56,11 +56,6 @@
(*tactics*)
val intro_classes_tac: thm list -> tactic
val default_intro_tac: Proof.context -> thm list -> tactic
-
- (*old axclass layer*)
- val axclass_cmd: binding * xstring list
- -> (Attrib.binding * string list) list
- -> theory -> class * theory
end;
structure Class_Target : CLASS_TARGET =
@@ -629,24 +624,5 @@
Method.setup (Binding.name "default") (Attrib.thms >> (METHOD oo default_tac))
"apply some intro/elim rule"));
-
-(** old axclass command **)
-
-fun axclass_cmd (class, raw_superclasses) raw_specs thy =
- let
- val _ = Output.legacy_feature "command \"axclass\" deprecated; use \"class\" instead.";
- val ctxt = ProofContext.init thy;
- val superclasses = map (Sign.read_class thy) raw_superclasses;
- val name_atts = map ((apsnd o map) (Attrib.attribute thy) o fst)
- raw_specs;
- val axiomss = ProofContext.read_propp (ctxt, map (map (rpair []) o snd)
- raw_specs)
- |> snd
- |> (map o map) fst;
- in
- AxClass.define_class (class, superclasses) []
- (name_atts ~~ axiomss) thy
- end;
-
end;
--- a/src/Pure/Isar/isar_syn.ML Mon Feb 22 17:02:39 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML Tue Feb 23 10:11:12 2010 +0100
@@ -99,13 +99,6 @@
OuterSyntax.command "defaultsort" "declare default sort" K.thy_decl
(P.sort >> (Toplevel.theory o Sign.add_defsort));
-val _ =
- OuterSyntax.command "axclass" "define axiomatic type class" K.thy_decl
- (P.binding -- Scan.optional ((P.$$$ "\\<subseteq>" || P.$$$ "<") |--
- P.!!! (P.list1 P.xname)) []
- -- Scan.repeat (SpecParse.thm_name ":" -- (P.prop >> single))
- >> (fn (x, y) => Toplevel.theory (snd o Class.axclass_cmd x y)));
-
(* types *)