1.1 --- a/NEWS	Mon Feb 10 22:07:50 2014 +0100
     1.2 +++ b/NEWS	Mon Feb 10 22:08:18 2014 +0100
     1.3 @@ -44,6 +44,16 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Low-level type-class commands 'classes', 'classrel', 'arities' have
     1.8 +been discontinued to avoid the danger of non-trivial axiomatization
     1.9 +that is not immediately visible.  INCOMPATIBILITY, use regular
    1.10 +'instance' with proof.  The required OFCLASS(...) theorem might be
    1.11 +postulated via 'axiomatization' beforehand, or the proof finished
    1.12 +trivially if the underlying class definition is made vacuous (without
    1.13 +any assumptions).  See also Isabelle/ML operations
    1.14 +Axclass.axiomatize_class, Axclass.axiomatize_classrel,
    1.15 +Axclass.axiomatize_arity.
    1.16 +
    1.17  * Attributes "where" and "of" allow an optional context of local
    1.18  variables ('for' declaration): these variables become schematic in the
    1.19  instantiated theorem.

     2.1 --- a/etc/isar-keywords-ZF.el	Mon Feb 10 22:07:50 2014 +0100
     2.2 +++ b/etc/isar-keywords-ZF.el	Mon Feb 10 22:08:18 2014 +0100
     2.3 @@ -24,7 +24,6 @@
     2.4      "also"
     2.5      "apply"
     2.6      "apply_end"
     2.7 -    "arities"
     2.8      "assume"
     2.9      "attribute_setup"
    2.10      "axiomatization"
    2.11 @@ -37,8 +36,6 @@
    2.12      "chapter"
    2.13      "class"
    2.14      "class_deps"
    2.15 -    "classes"
    2.16 -    "classrel"
    2.17      "codatatype"
    2.18      "code_datatype"
    2.19      "coinductive"
    2.20 @@ -346,13 +343,10 @@
    2.21    '("ML"
    2.22      "ML_file"
    2.23      "abbreviation"
    2.24 -    "arities"
    2.25      "attribute_setup"
    2.26      "axiomatization"
    2.27      "bundle"
    2.28      "class"
    2.29 -    "classes"
    2.30 -    "classrel"
    2.31      "codatatype"
    2.32      "code_datatype"
    2.33      "coinductive"

     3.1 --- a/etc/isar-keywords.el	Mon Feb 10 22:07:50 2014 +0100
     3.2 +++ b/etc/isar-keywords.el	Mon Feb 10 22:08:18 2014 +0100
     3.3 @@ -25,7 +25,6 @@
     3.4      "also"
     3.5      "apply"
     3.6      "apply_end"
     3.7 -    "arities"
     3.8      "assume"
     3.9      "atom_decl"
    3.10      "attribute_setup"
    3.11 @@ -45,8 +44,6 @@
    3.12      "chapter"
    3.13      "class"
    3.14      "class_deps"
    3.15 -    "classes"
    3.16 -    "classrel"
    3.17      "codatatype"
    3.18      "code_datatype"
    3.19      "code_deps"
    3.20 @@ -481,7 +478,6 @@
    3.21      "ML_file"
    3.22      "abbreviation"
    3.23      "adhoc_overloading"
    3.24 -    "arities"
    3.25      "atom_decl"
    3.26      "attribute_setup"
    3.27      "axiomatization"
    3.28 @@ -490,8 +486,6 @@
    3.29      "bundle"
    3.30      "case_of_simps"
    3.31      "class"
    3.32 -    "classes"
    3.33 -    "classrel"
    3.34      "codatatype"
    3.35      "code_datatype"
    3.36      "code_identifier"

     4.1 --- a/src/Doc/Classes/Classes.thy	Mon Feb 10 22:07:50 2014 +0100
     4.2 +++ b/src/Doc/Classes/Classes.thy	Mon Feb 10 22:08:18 2014 +0100
     4.3 @@ -356,19 +356,14 @@
     4.4  consts %quote f :: "\<alpha> \<Rightarrow> \<alpha>"
     4.5  
     4.6  text {*
     4.7 -  \noindent The connection to the type system is done by means
     4.8 -  of a primitive type class
     4.9 -*} (*<*)setup %invisible {* Sign.add_path "foo" *}
    4.10 -(*>*)
    4.11 -classes %quote idem < type
    4.12 -(*<*)axiomatization where idem: "f (f (x::\<alpha>\<Colon>idem)) = f x"
    4.13 -setup %invisible {* Sign.parent_path *}(*>*)
    4.14 -
    4.15 -text {* \noindent together with a corresponding interpretation: *}
    4.16 +  \noindent The connection to the type system is done by means of a
    4.17 +  primitive type class @{text "idem"}, together with a corresponding
    4.18 +  interpretation:
    4.19 +*}
    4.20  
    4.21  interpretation %quote idem_class:
    4.22    idem "f \<Colon> (\<alpha>\<Colon>idem) \<Rightarrow> \<alpha>"
    4.23 -(*<*)proof qed (rule idem)(*>*)
    4.24 +(*<*)sorry(*>*)
    4.25  
    4.26  text {*
    4.27    \noindent This gives you the full power of the Isabelle module system;

     5.1 --- a/src/Doc/IsarRef/Spec.thy	Mon Feb 10 22:07:50 2014 +0100
     5.2 +++ b/src/Doc/IsarRef/Spec.thy	Mon Feb 10 22:08:18 2014 +0100
     5.3 @@ -1085,36 +1085,19 @@
     5.4  
     5.5  section {* Primitive specification elements *}
     5.6  
     5.7 -subsection {* Type classes and sorts \label{sec:classes} *}
     5.8 +subsection {* Sorts *}
     5.9  
    5.10  text {*
    5.11    \begin{matharray}{rcll}
    5.12 -    @{command_def "classes"} & : & @{text "theory \<rightarrow> theory"} \\
    5.13 -    @{command_def "classrel"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
    5.14      @{command_def "default_sort"} & : & @{text "local_theory \<rightarrow> local_theory"}
    5.15    \end{matharray}
    5.16  
    5.17    @{rail \<open>
    5.18 -    @@{command classes} (@{syntax classdecl} +)
    5.19 -    ;
    5.20 -    @@{command classrel} (@{syntax nameref} ('<' | '\<subseteq>') @{syntax nameref} + @'and')
    5.21 -    ;
    5.22      @@{command default_sort} @{syntax sort}
    5.23    \<close>}
    5.24  
    5.25    \begin{description}
    5.26  
    5.27 -  \item @{command "classes"}~@{text "c \<subseteq> c\<^sub>1, \<dots>, c\<^sub>n"} declares class
    5.28 -  @{text c} to be a subclass of existing classes @{text "c\<^sub>1, \<dots>, c\<^sub>n"}.
    5.29 -  Isabelle implicitly maintains the transitive closure of the class
    5.30 -  hierarchy.  Cyclic class structures are not permitted.
    5.31 -
    5.32 -  \item @{command "classrel"}~@{text "c\<^sub>1 \<subseteq> c\<^sub>2"} states subclass
    5.33 -  relations between existing classes @{text "c\<^sub>1"} and @{text "c\<^sub>2"}.
    5.34 -  This is done axiomatically!  The @{command_ref "subclass"} and
    5.35 -  @{command_ref "instance"} commands (see \secref{sec:class}) provide
    5.36 -  a way to introduce proven class relations.
    5.37 -
    5.38    \item @{command "default_sort"}~@{text s} makes sort @{text s} the
    5.39    new default sort for any type variable that is given explicitly in
    5.40    the text, but lacks a sort constraint (wrt.\ the current context).
    5.41 @@ -1138,15 +1121,12 @@
    5.42    \begin{matharray}{rcll}
    5.43      @{command_def "type_synonym"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
    5.44      @{command_def "typedecl"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
    5.45 -    @{command_def "arities"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
    5.46    \end{matharray}
    5.47  
    5.48    @{rail \<open>
    5.49      @@{command type_synonym} (@{syntax typespec} '=' @{syntax type} @{syntax mixfix}?)
    5.50      ;
    5.51      @@{command typedecl} @{syntax typespec} @{syntax mixfix}?
    5.52 -    ;
    5.53 -    @@{command arities} (@{syntax nameref} '::' @{syntax arity} +)
    5.54    \<close>}
    5.55  
    5.56    \begin{description}
    5.57 @@ -1161,14 +1141,7 @@
    5.58    \item @{command "typedecl"}~@{text "(\<alpha>\<^sub>1, \<dots>, \<alpha>\<^sub>n) t"} declares a new
    5.59    type constructor @{text t}.  If the object-logic defines a base sort
    5.60    @{text s}, then the constructor is declared to operate on that, via
    5.61 -  the axiomatic specification @{command arities}~@{text "t :: (s, \<dots>,
    5.62 -  s)s"}.
    5.63 -
    5.64 -  \item @{command "arities"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s"} augments
    5.65 -  Isabelle's order-sorted signature of types by new type constructor
    5.66 -  arities.  This is done axiomatically!  The @{command_ref "instantiation"}
    5.67 -  target (see \secref{sec:class}) provides a way to introduce
    5.68 -  proven type arities.
    5.69 +  the axiomatic type-class instance @{text "t :: (s, \<dots>, s)s"}.
    5.70  
    5.71    \end{description}
    5.72  *}

     6.1 --- a/src/Doc/ROOT	Mon Feb 10 22:07:50 2014 +0100
     6.2 +++ b/src/Doc/ROOT	Mon Feb 10 22:08:18 2014 +0100
     6.3 @@ -1,7 +1,7 @@
     6.4  chapter Doc
     6.5  
     6.6  session Classes (doc) in "Classes" = HOL +
     6.7 -  options [document_variants = "classes"]
     6.8 +  options [document_variants = "classes", quick_and_dirty]
     6.9    theories [document = false] Setup
    6.10    theories Classes
    6.11    files

     7.1 --- a/src/HOL/HOL.thy	Mon Feb 10 22:07:50 2014 +0100
     7.2 +++ b/src/HOL/HOL.thy	Mon Feb 10 22:08:18 2014 +0100
     7.3 @@ -45,7 +45,7 @@
     7.4  
     7.5  subsubsection {* Core syntax *}
     7.6  
     7.7 -classes type
     7.8 +setup {* Axclass.axiomatize_class (@{binding type}, []) *}
     7.9  default_sort type
    7.10  setup {* Object_Logic.add_base_sort @{sort type} *}
    7.11  

     8.1 --- a/src/Pure/Isar/isar_syn.ML	Mon Feb 10 22:07:50 2014 +0100
     8.2 +++ b/src/Pure/Isar/isar_syn.ML	Mon Feb 10 22:08:18 2014 +0100
     8.3 @@ -73,19 +73,7 @@
     8.4  
     8.5  (** theory commands **)
     8.6  
     8.7 -(* classes and sorts *)
     8.8 -
     8.9 -val _ =
    8.10 -  Outer_Syntax.command @{command_spec "classes"} "declare type classes"
    8.11 -    (Scan.repeat1 (Parse.binding -- Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<"}) |--
    8.12 -        Parse.!!! (Parse.list1 Parse.class)) [])
    8.13 -      >> (Toplevel.theory o fold Axclass.axiomatize_class_cmd));
    8.14 -
    8.15 -val _ =
    8.16 -  Outer_Syntax.command @{command_spec "classrel"} "state inclusion of type classes (axiomatic!)"
    8.17 -    (Parse.and_list1 (Parse.class -- ((@{keyword "\<subseteq>"} || @{keyword "<"})
    8.18 -        |-- Parse.!!! Parse.class))
    8.19 -    >> (Toplevel.theory o Axclass.axiomatize_classrel_cmd));
    8.20 +(* sorts *)
    8.21  
    8.22  val _ =
    8.23    Outer_Syntax.local_theory @{command_spec "default_sort"}
    8.24 @@ -111,10 +99,6 @@
    8.25      "declare syntactic type constructors (grammar nonterminal symbols)"
    8.26      (Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
    8.27  
    8.28 -val _ =
    8.29 -  Outer_Syntax.command @{command_spec "arities"} "state type arities (axiomatic!)"
    8.30 -    (Scan.repeat1 Parse.arity >> (Toplevel.theory o fold Axclass.axiomatize_arity_cmd));
    8.31 -
    8.32  
    8.33  (* consts and syntax *)
    8.34  

     9.1 --- a/src/Pure/Pure.thy	Mon Feb 10 22:07:50 2014 +0100
     9.2 +++ b/src/Pure/Pure.thy	Mon Feb 10 22:08:18 2014 +0100
     9.3 @@ -25,10 +25,9 @@
     9.4    and "subsect" :: prf_heading3 % "proof"
     9.5    and "subsubsect" :: prf_heading4 % "proof"
     9.6    and "txt" "txt_raw" :: prf_decl % "proof"
     9.7 -  and "classes" "classrel" "default_sort" "typedecl" "type_synonym"
     9.8 -    "nonterminal" "arities" "judgment" "consts" "syntax" "no_syntax"
     9.9 -    "translations" "no_translations" "defs" "definition"
    9.10 -    "abbreviation" "type_notation" "no_type_notation" "notation"
    9.11 +  and "default_sort" "typedecl" "type_synonym" "nonterminal" "judgment"
    9.12 +    "consts" "syntax" "no_syntax" "translations" "no_translations" "defs"
    9.13 +    "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
    9.14      "no_notation" "axiomatization" "theorems" "lemmas" "declare"
    9.15      "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
    9.16    and "ML" :: thy_decl % "ML"

    10.1 --- a/src/Pure/axclass.ML	Mon Feb 10 22:07:50 2014 +0100
    10.2 +++ b/src/Pure/axclass.ML	Mon Feb 10 22:08:18 2014 +0100
    10.3 @@ -30,12 +30,9 @@
    10.4    val prove_arity: string * sort list * sort -> (Proof.context -> tactic) -> theory -> theory
    10.5    val define_class: binding * class list -> string list ->
    10.6      (Thm.binding * term list) list -> theory -> class * theory
    10.7 +  val axiomatize_classrel: (class * class) list -> theory -> theory
    10.8 +  val axiomatize_arity: arity -> theory -> theory
    10.9    val axiomatize_class: binding * class list -> theory -> theory
   10.10 -  val axiomatize_class_cmd: binding * xstring list -> theory -> theory
   10.11 -  val axiomatize_classrel: (class * class) list -> theory -> theory
   10.12 -  val axiomatize_classrel_cmd: (xstring * xstring) list -> theory -> theory
   10.13 -  val axiomatize_arity: arity -> theory -> theory
   10.14 -  val axiomatize_arity_cmd: xstring * string list * string -> theory -> theory
   10.15  end;
   10.16  
   10.17  structure Axclass: AXCLASS =
   10.18 @@ -596,38 +593,30 @@
   10.19      |-> fold (add o Drule.export_without_context o snd)
   10.20    end;
   10.21  
   10.22 -fun ax_classrel prep =
   10.23 -  axiomatize (map o prep) (map Logic.mk_classrel)
   10.24 -    (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
   10.25 -
   10.26 -fun ax_arity prep =
   10.27 -  axiomatize (prep o Proof_Context.init_global) Logic.mk_arities
   10.28 -    (map (prefix arity_prefix) o Logic.name_arities) add_arity;
   10.29 -
   10.30  fun class_const c =
   10.31    (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);
   10.32  
   10.33 -fun ax_class prep_class prep_classrel (bclass, raw_super) thy =
   10.34 +in
   10.35 +
   10.36 +val axiomatize_classrel =
   10.37 +  axiomatize (map o cert_classrel) (map Logic.mk_classrel)
   10.38 +    (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
   10.39 +
   10.40 +val axiomatize_arity =
   10.41 +  axiomatize (Proof_Context.cert_arity o Proof_Context.init_global) Logic.mk_arities
   10.42 +    (map (prefix arity_prefix) o Logic.name_arities) add_arity;
   10.43 +
   10.44 +fun axiomatize_class (bclass, raw_super) thy =
   10.45    let
   10.46      val class = Sign.full_name thy bclass;
   10.47 -    val super = map (prep_class thy) raw_super |> Sign.minimize_sort thy;
   10.48 +    val super = map (Sign.certify_class thy) raw_super |> Sign.minimize_sort thy;
   10.49    in
   10.50      thy
   10.51      |> Sign.primitive_class (bclass, super)
   10.52 -    |> ax_classrel prep_classrel (map (fn c => (class, c)) super)
   10.53 +    |> axiomatize_classrel (map (fn c => (class, c)) super)
   10.54      |> Theory.add_deps_global "" (class_const class) (map class_const super)
   10.55    end;
   10.56  
   10.57 -in
   10.58 -
   10.59 -val axiomatize_class = ax_class Sign.certify_class cert_classrel;
   10.60 -val axiomatize_class_cmd =
   10.61 -  ax_class (Proof_Context.read_class o Proof_Context.init_global) read_classrel;
   10.62 -val axiomatize_classrel = ax_classrel cert_classrel;
   10.63 -val axiomatize_classrel_cmd = ax_classrel read_classrel;
   10.64 -val axiomatize_arity = ax_arity Proof_Context.cert_arity;
   10.65 -val axiomatize_arity_cmd = ax_arity Proof_Context.read_arity;
   10.66 -
   10.67  end;
   10.68  
   10.69  end;