--- a/NEWS Mon Feb 10 22:07:50 2014 +0100
+++ b/NEWS Mon Feb 10 22:08:18 2014 +0100
@@ -44,6 +44,16 @@
*** Pure ***
+* Low-level type-class commands 'classes', 'classrel', 'arities' have
+been discontinued to avoid the danger of non-trivial axiomatization
+that is not immediately visible. INCOMPATIBILITY, use regular
+'instance' with proof. The required OFCLASS(...) theorem might be
+postulated via 'axiomatization' beforehand, or the proof finished
+trivially if the underlying class definition is made vacuous (without
+any assumptions). See also Isabelle/ML operations
+Axclass.axiomatize_class, Axclass.axiomatize_classrel,
+Axclass.axiomatize_arity.
+
* Attributes "where" and "of" allow an optional context of local
variables ('for' declaration): these variables become schematic in the
instantiated theorem.
--- a/etc/isar-keywords-ZF.el Mon Feb 10 22:07:50 2014 +0100
+++ b/etc/isar-keywords-ZF.el Mon Feb 10 22:08:18 2014 +0100
@@ -24,7 +24,6 @@
"also"
"apply"
"apply_end"
- "arities"
"assume"
"attribute_setup"
"axiomatization"
@@ -37,8 +36,6 @@
"chapter"
"class"
"class_deps"
- "classes"
- "classrel"
"codatatype"
"code_datatype"
"coinductive"
@@ -346,13 +343,10 @@
'("ML"
"ML_file"
"abbreviation"
- "arities"
"attribute_setup"
"axiomatization"
"bundle"
"class"
- "classes"
- "classrel"
"codatatype"
"code_datatype"
"coinductive"
--- a/etc/isar-keywords.el Mon Feb 10 22:07:50 2014 +0100
+++ b/etc/isar-keywords.el Mon Feb 10 22:08:18 2014 +0100
@@ -25,7 +25,6 @@
"also"
"apply"
"apply_end"
- "arities"
"assume"
"atom_decl"
"attribute_setup"
@@ -45,8 +44,6 @@
"chapter"
"class"
"class_deps"
- "classes"
- "classrel"
"codatatype"
"code_datatype"
"code_deps"
@@ -481,7 +478,6 @@
"ML_file"
"abbreviation"
"adhoc_overloading"
- "arities"
"atom_decl"
"attribute_setup"
"axiomatization"
@@ -490,8 +486,6 @@
"bundle"
"case_of_simps"
"class"
- "classes"
- "classrel"
"codatatype"
"code_datatype"
"code_identifier"
--- a/src/Doc/Classes/Classes.thy Mon Feb 10 22:07:50 2014 +0100
+++ b/src/Doc/Classes/Classes.thy Mon Feb 10 22:08:18 2014 +0100
@@ -356,19 +356,14 @@
consts %quote f :: "\<alpha> \<Rightarrow> \<alpha>"
text {*
- \noindent The connection to the type system is done by means
- of a primitive type class
-*} (*<*)setup %invisible {* Sign.add_path "foo" *}
-(*>*)
-classes %quote idem < type
-(*<*)axiomatization where idem: "f (f (x::\<alpha>\<Colon>idem)) = f x"
-setup %invisible {* Sign.parent_path *}(*>*)
-
-text {* \noindent together with a corresponding interpretation: *}
+ \noindent The connection to the type system is done by means of a
+ primitive type class @{text "idem"}, together with a corresponding
+ interpretation:
+*}
interpretation %quote idem_class:
idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"
-(*<*)proof qed (rule idem)(*>*)
+(*<*)sorry(*>*)
text {*
\noindent This gives you the full power of the Isabelle module system;
--- a/src/Doc/IsarRef/Spec.thy Mon Feb 10 22:07:50 2014 +0100
+++ b/src/Doc/IsarRef/Spec.thy Mon Feb 10 22:08:18 2014 +0100
@@ -1085,36 +1085,19 @@
section {* Primitive specification elements *}
-subsection {* Type classes and sorts \label{sec:classes} *}
+subsection {* Sorts *}
text {*
\begin{matharray}{rcll}
- @{command_def "classes"} & : & @{text "theory \<rightarrow> theory"} \\
- @{command_def "classrel"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
@{command_def "default_sort"} & : & @{text "local_theory \<rightarrow> local_theory"}
\end{matharray}
@{rail \<open>
- @@{command classes} (@{syntax classdecl} +)
- ;
- @@{command classrel} (@{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} + @'and')
- ;
@@{command default_sort} @{syntax sort}
\<close>}
\begin{description}
- \item @{command "classes"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n"} declares class
- @{text c} to be a subclass of existing classes @{text "c\<^sub>1, \<dots>, c\<^sub>n"}.
- Isabelle implicitly maintains the transitive closure of the class
- hierarchy. Cyclic class structures are not permitted.
-
- \item @{command "classrel"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} states subclass
- relations between existing classes @{text "c\<^sub>1"} and @{text "c\<^sub>2"}.
- This is done axiomatically! The @{command_ref "subclass"} and
- @{command_ref "instance"} commands (see \secref{sec:class}) provide
- a way to introduce proven class relations.
-
\item @{command "default_sort"}~@{text s} makes sort @{text s} the
new default sort for any type variable that is given explicitly in
the text, but lacks a sort constraint (wrt.\ the current context).
@@ -1138,15 +1121,12 @@
\begin{matharray}{rcll}
@{command_def "type_synonym"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
@{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
- @{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
\end{matharray}
@{rail \<open>
@@{command type_synonym} (@{syntax typespec} '=' @{syntax type} @{syntax mixfix}?)
;
@@{command typedecl} @{syntax typespec} @{syntax mixfix}?
- ;
- @@{command arities} (@{syntax nameref} '::' @{syntax arity} +)
\<close>}
\begin{description}
@@ -1161,14 +1141,7 @@
\item @{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} declares a new
type constructor @{text t}. If the object-logic defines a base sort
@{text s}, then the constructor is declared to operate on that, via
- the axiomatic specification @{command arities}~@{text "t :: (s, \<dots>,
- s)s"}.
-
- \item @{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} augments
- Isabelle's order-sorted signature of types by new type constructor
- arities. This is done axiomatically! The @{command_ref "instantiation"}
- target (see \secref{sec:class}) provides a way to introduce
- proven type arities.
+ the axiomatic type-class instance @{text "t :: (s, \<dots>, s)s"}.
\end{description}
*}
--- a/src/Doc/ROOT Mon Feb 10 22:07:50 2014 +0100
+++ b/src/Doc/ROOT Mon Feb 10 22:08:18 2014 +0100
@@ -1,7 +1,7 @@
chapter Doc
session Classes (doc) in "Classes" = HOL +
- options [document_variants = "classes"]
+ options [document_variants = "classes", quick_and_dirty]
theories [document = false] Setup
theories Classes
files
--- a/src/HOL/HOL.thy Mon Feb 10 22:07:50 2014 +0100
+++ b/src/HOL/HOL.thy Mon Feb 10 22:08:18 2014 +0100
@@ -45,7 +45,7 @@
subsubsection {* Core syntax *}
-classes type
+setup {* Axclass.axiomatize_class (@{binding type}, []) *}
default_sort type
setup {* Object_Logic.add_base_sort @{sort type} *}
--- a/src/Pure/Isar/isar_syn.ML Mon Feb 10 22:07:50 2014 +0100
+++ b/src/Pure/Isar/isar_syn.ML Mon Feb 10 22:08:18 2014 +0100
@@ -73,19 +73,7 @@
(** theory commands **)
-(* classes and sorts *)
-
-val _ =
- Outer_Syntax.command @{command_spec "classes"} "declare type classes"
- (Scan.repeat1 (Parse.binding -- Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<"}) |--
- Parse.!!! (Parse.list1 Parse.class)) [])
- >> (Toplevel.theory o fold Axclass.axiomatize_class_cmd));
-
-val _ =
- Outer_Syntax.command @{command_spec "classrel"} "state inclusion of type classes (axiomatic!)"
- (Parse.and_list1 (Parse.class -- ((@{keyword "\<subseteq>"} || @{keyword "<"})
- |-- Parse.!!! Parse.class))
- >> (Toplevel.theory o Axclass.axiomatize_classrel_cmd));
+(* sorts *)
val _ =
Outer_Syntax.local_theory @{command_spec "default_sort"}
@@ -111,10 +99,6 @@
"declare syntactic type constructors (grammar nonterminal symbols)"
(Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
-val _ =
- Outer_Syntax.command @{command_spec "arities"} "state type arities (axiomatic!)"
- (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold Axclass.axiomatize_arity_cmd));
-
(* consts and syntax *)
--- a/src/Pure/Pure.thy Mon Feb 10 22:07:50 2014 +0100
+++ b/src/Pure/Pure.thy Mon Feb 10 22:08:18 2014 +0100
@@ -25,10 +25,9 @@
and "subsect" :: prf_heading3 % "proof"
and "subsubsect" :: prf_heading4 % "proof"
and "txt" "txt_raw" :: prf_decl % "proof"
- and "classes" "classrel" "default_sort" "typedecl" "type_synonym"
- "nonterminal" "arities" "judgment" "consts" "syntax" "no_syntax"
- "translations" "no_translations" "defs" "definition"
- "abbreviation" "type_notation" "no_type_notation" "notation"
+ and "default_sort" "typedecl" "type_synonym" "nonterminal" "judgment"
+ "consts" "syntax" "no_syntax" "translations" "no_translations" "defs"
+ "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
"no_notation" "axiomatization" "theorems" "lemmas" "declare"
"hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
and "ML" :: thy_decl % "ML"
--- a/src/Pure/axclass.ML Mon Feb 10 22:07:50 2014 +0100
+++ b/src/Pure/axclass.ML Mon Feb 10 22:08:18 2014 +0100
@@ -30,12 +30,9 @@
val prove_arity: string * sort list * sort -> (Proof.context -> tactic) -> theory -> theory
val define_class: binding * class list -> string list ->
(Thm.binding * term list) list -> theory -> class * theory
+ val axiomatize_classrel: (class * class) list -> theory -> theory
+ val axiomatize_arity: arity -> theory -> theory
val axiomatize_class: binding * class list -> theory -> theory
- val axiomatize_class_cmd: binding * xstring list -> theory -> theory
- val axiomatize_classrel: (class * class) list -> theory -> theory
- val axiomatize_classrel_cmd: (xstring * xstring) list -> theory -> theory
- val axiomatize_arity: arity -> theory -> theory
- val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
end;
structure Axclass: AXCLASS =
@@ -596,38 +593,30 @@
|-> fold (add o Drule.export_without_context o snd)
end;
-fun ax_classrel prep =
- axiomatize (map o prep) (map Logic.mk_classrel)
- (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
-
-fun ax_arity prep =
- axiomatize (prep o Proof_Context.init_global) Logic.mk_arities
- (map (prefix arity_prefix) o Logic.name_arities) add_arity;
-
fun class_const c =
(Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);
-fun ax_class prep_class prep_classrel (bclass, raw_super) thy =
+in
+
+val axiomatize_classrel =
+ axiomatize (map o cert_classrel) (map Logic.mk_classrel)
+ (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
+
+val axiomatize_arity =
+ axiomatize (Proof_Context.cert_arity o Proof_Context.init_global) Logic.mk_arities
+ (map (prefix arity_prefix) o Logic.name_arities) add_arity;
+
+fun axiomatize_class (bclass, raw_super) thy =
let
val class = Sign.full_name thy bclass;
- val super = map (prep_class thy) raw_super |> Sign.minimize_sort thy;
+ val super = map (Sign.certify_class thy) raw_super |> Sign.minimize_sort thy;
in
thy
|> Sign.primitive_class (bclass, super)
- |> ax_classrel prep_classrel (map (fn c => (class, c)) super)
+ |> axiomatize_classrel (map (fn c => (class, c)) super)
|> Theory.add_deps_global "" (class_const class) (map class_const super)
end;
-in
-
-val axiomatize_class = ax_class Sign.certify_class cert_classrel;
-val axiomatize_class_cmd =
- ax_class (Proof_Context.read_class o Proof_Context.init_global) read_classrel;
-val axiomatize_classrel = ax_classrel cert_classrel;
-val axiomatize_classrel_cmd = ax_classrel read_classrel;
-val axiomatize_arity = ax_arity Proof_Context.cert_arity;
-val axiomatize_arity_cmd = ax_arity Proof_Context.read_arity;
-
end;
end;