# HG changeset patch # User wenzelm # Date 1392066498 -3600 # Node ID 169e12bbf9a3a163e4fec748d7abfc1a92f41981 # Parent 1107de77c63398a809eed858cf2bef90017b4964 discontinued axiomatic 'classes', 'classrel', 'arities'; diff -r 1107de77c633 -r 169e12bbf9a3 NEWS --- 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. diff -r 1107de77c633 -r 169e12bbf9a3 etc/isar-keywords-ZF.el --- 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" diff -r 1107de77c633 -r 169e12bbf9a3 etc/isar-keywords.el --- 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" diff -r 1107de77c633 -r 169e12bbf9a3 src/Doc/Classes/Classes.thy --- 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 :: "\ \ \" 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::\\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 \ (\\idem) \ \" -(*<*)proof qed (rule idem)(*>*) +(*<*)sorry(*>*) text {* \noindent This gives you the full power of the Isabelle module system; diff -r 1107de77c633 -r 169e12bbf9a3 src/Doc/IsarRef/Spec.thy --- 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 \ theory"} \\ - @{command_def "classrel"} & : & @{text "theory \ theory"} & (axiomatic!) \\ @{command_def "default_sort"} & : & @{text "local_theory \ local_theory"} \end{matharray} @{rail \ - @@{command classes} (@{syntax classdecl} +) - ; - @@{command classrel} (@{syntax nameref} ('<' | '\') @{syntax nameref} + @'and') - ; @@{command default_sort} @{syntax sort} \} \begin{description} - \item @{command "classes"}~@{text "c \ c\<^sub>1, \, c\<^sub>n"} declares class - @{text c} to be a subclass of existing classes @{text "c\<^sub>1, \, 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 \ 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 \ local_theory"} \\ @{command_def "typedecl"} & : & @{text "local_theory \ local_theory"} \\ - @{command_def "arities"} & : & @{text "theory \ theory"} & (axiomatic!) \\ \end{matharray} @{rail \ @@{command type_synonym} (@{syntax typespec} '=' @{syntax type} @{syntax mixfix}?) ; @@{command typedecl} @{syntax typespec} @{syntax mixfix}? - ; - @@{command arities} (@{syntax nameref} '::' @{syntax arity} +) \} \begin{description} @@ -1161,14 +1141,7 @@ \item @{command "typedecl"}~@{text "(\\<^sub>1, \, \\<^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, \, - s)s"}. - - \item @{command "arities"}~@{text "t :: (s\<^sub>1, \, 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, \, s)s"}. \end{description} *} diff -r 1107de77c633 -r 169e12bbf9a3 src/Doc/ROOT --- 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 diff -r 1107de77c633 -r 169e12bbf9a3 src/HOL/HOL.thy --- 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} *} diff -r 1107de77c633 -r 169e12bbf9a3 src/Pure/Isar/isar_syn.ML --- 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 "\"} || @{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 "\"} || @{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 *) diff -r 1107de77c633 -r 169e12bbf9a3 src/Pure/Pure.thy --- 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" diff -r 1107de77c633 -r 169e12bbf9a3 src/Pure/axclass.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;