# HG changeset patch
# User wenzelm
# Date 1082141949 -7200
# Node ID 9de4d64eee3b2c34799b95dc809383e1ce94fe13
# Parent  1946097f706883da1516f48db99623f141455e74
'instance' and intro_classes now handle general sorts;

diff -r 1946097f7068 -r 9de4d64eee3b doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Fri Apr 16 20:34:41 2004 +0200
+++ b/doc-src/IsarRef/generic.tex	Fri Apr 16 20:59:09 2004 +0200
@@ -22,7 +22,7 @@
 \begin{rail}
   'axclass' classdecl (axmdecl prop +)
   ;
-  'instance' (nameref ('<' | subseteq) nameref | nameref '::' simplearity)
+  'instance' (nameref ('<' | subseteq) nameref | nameref '::' arity)
   ;
 \end{rail}
 
@@ -39,8 +39,8 @@
   The ``axioms'' are stored as theorems according to the given name
   specifications, adding the class name $c$ as name space prefix; the same
   facts are also stored collectively as $c{\dtt}axioms$.
-
-\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)c$] setup a
+  
+\item [$\INSTANCE~c@1 \subseteq c@2$ and $\INSTANCE~t :: (\vec s)s$] setup a
   goal stating a class relation or type arity.  The proof would usually
   proceed by $intro_classes$, and then establish the characteristic theorems
   of the type classes involved.  After finishing the proof, the theory will be
diff -r 1946097f7068 -r 9de4d64eee3b doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Fri Apr 16 20:34:41 2004 +0200
+++ b/doc-src/IsarRef/syntax.tex	Fri Apr 16 20:59:09 2004 +0200
@@ -204,7 +204,7 @@
 \railalias{subseteq}{\isasymsubseteq}
 \railterm{subseteq}
 
-\indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity}
+\indexouternonterm{sort}\indexouternonterm{arity}
 \indexouternonterm{classdecl}
 \begin{rail}
   classdecl: name (('<' | subseteq) (nameref + ','))?
@@ -213,8 +213,6 @@
   ;
   arity: ('(' (sort + ',') ')')? sort
   ;
-  simplearity: ('(' (sort + ',') ')')? nameref
-  ;
 \end{rail}
 
 
diff -r 1946097f7068 -r 9de4d64eee3b src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Apr 16 20:34:41 2004 +0200
+++ b/src/Provers/classical.ML	Fri Apr 16 20:59:09 2004 +0200
@@ -924,7 +924,8 @@
 
 (** proof methods **)
 
-(* METHOD_CLASET' *)
+fun METHOD_CLASET tac ctxt =
+  Method.METHOD (tac ctxt (get_local_claset ctxt));
 
 fun METHOD_CLASET' tac ctxt =
   Method.METHOD (HEADGOAL o tac ctxt (get_local_claset ctxt));
@@ -947,12 +948,12 @@
   | rule_tac rules _ _ facts = Method.rule_tac rules facts;
 
 fun default_tac rules ctxt cs facts =
-  rule_tac rules ctxt cs facts ORELSE'
+  HEADGOAL (rule_tac rules ctxt cs facts) ORELSE
   AxClass.default_intro_classes_tac facts;
 
 in
   val rule = METHOD_CLASET' o rule_tac;
-  val default = METHOD_CLASET' o default_tac;
+  val default = METHOD_CLASET o default_tac;
 end;
 
 
diff -r 1946097f7068 -r 9de4d64eee3b src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Fri Apr 16 20:34:41 2004 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Fri Apr 16 20:59:09 2004 +0200
@@ -47,7 +47,6 @@
   val uname: token list -> string option * token list
   val sort: token list -> string * token list
   val arity: token list -> (string list * string) * token list
-  val simple_arity: token list -> (string list * xclass) * token list
   val type_args: token list -> string list * token list
   val typ: token list -> string * token list
   val opt_infix: token list -> Syntax.mixfix * token list
@@ -185,7 +184,6 @@
   Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- cod;
 
 val arity = gen_arity sort;
-val simple_arity = gen_arity xname;
 
 
 (* types *)
diff -r 1946097f7068 -r 9de4d64eee3b src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Fri Apr 16 20:34:41 2004 +0200
+++ b/src/Pure/axclass.ML	Fri Apr 16 20:59:09 2004 +0200
@@ -24,12 +24,12 @@
     -> thm list -> tactic option -> theory -> theory
   val add_inst_arity: xstring * string list * string -> tactic -> theory -> theory
   val add_inst_arity_i: string * sort list * sort -> tactic -> theory -> theory
-  val default_intro_classes_tac: thm list -> int -> tactic
+  val default_intro_classes_tac: thm list -> tactic
   val axclass_tac: thm list -> tactic
   val instance_subclass_proof: xclass * xclass -> bool -> theory -> ProofHistory.T
   val instance_subclass_proof_i: class * class -> bool -> theory -> ProofHistory.T
-  val instance_arity_proof: xstring * string list * xclass -> bool -> theory -> ProofHistory.T
-  val instance_arity_proof_i: string * sort list * class -> bool -> theory -> ProofHistory.T
+  val instance_arity_proof: xstring * string list * string -> bool -> theory -> ProofHistory.T
+  val instance_arity_proof_i: string * sort list * sort -> bool -> theory -> ProofHistory.T
   val setup: (theory -> theory) list
 end;
 
@@ -94,11 +94,13 @@
 
 (* arities as terms *)
 
-fun mk_arity (t, ss, c) =
+fun mk_arity (t, Ss, c) =
   let
-    val tfrees = ListPair.map TFree (Term.invent_type_names [] (length ss), ss);
+    val tfrees = ListPair.map TFree (Term.invent_type_names [] (length Ss), Ss);
   in Logic.mk_inclass (Type (t, tfrees), c) end;
 
+fun mk_arities (t, Ss, S) = map (fn c => mk_arity (t, Ss, c)) S;
+
 fun dest_arity tm =
   let
     fun err () = raise TERM ("dest_arity", [tm]);
@@ -299,29 +301,30 @@
 
 (* intro_classes *)
 
-fun intro_classes_tac facts i st =
-  ((Method.insert_tac facts THEN'
-    REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st)))) i
-    THEN Tactic.distinct_subgoals_tac) st;    (*affects all subgoals!?*)
+fun intro_classes_tac facts st =
+  (ALLGOALS (Method.insert_tac facts THEN'
+      REPEAT_ALL_NEW (resolve_tac (class_axms (Thm.sign_of_thm st))))
+    THEN Tactic.distinct_subgoals_tac) st;
 
 val intro_classes_method =
-  ("intro_classes", Method.no_args (Method.METHOD (HEADGOAL o intro_classes_tac)),
+  ("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
     "back-chain introduction rules of axiomatic type classes");
 
 
 (* default method *)
 
-fun default_intro_classes_tac [] i = intro_classes_tac [] i
-  | default_intro_classes_tac _ _ = Tactical.no_tac;    (*no error message!*)
+fun default_intro_classes_tac [] = intro_classes_tac []
+  | default_intro_classes_tac _ = Tactical.no_tac;    (*no error message!*)
 
 fun default_tac rules ctxt facts =
-  HEADGOAL (Method.some_rule_tac rules ctxt facts ORELSE' default_intro_classes_tac facts);
+  HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
+    default_intro_classes_tac facts;
 
 val default_method =
   ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule");
 
 
-(* axclass_tac *)
+(* old-style axclass_tac *)
 
 (*(1) repeatedly resolve goals of form "OFCLASS(ty, c_class)",
       try class_trivs first, then "cI" axioms
@@ -333,13 +336,13 @@
     val defs = filter is_def thms;
     val non_defs = filter_out is_def thms;
   in
-    HEADGOAL (intro_classes_tac []) THEN
+    intro_classes_tac [] THEN
     TRY (rewrite_goals_tac defs) THEN
     TRY (REPEAT_FIRST (fn i => assume_tac i ORELSE resolve_tac non_defs i))
   end;
 
 
-(* provers *)
+(* old-style provers *)
 
 fun prove mk_prop str_of sign prop thms usr_tac =
   (Tactic.prove sign [] [] (mk_prop prop) (K (axclass_tac thms THEN (if_none usr_tac all_tac)))
@@ -377,8 +380,6 @@
 
 val read_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.read_sort;
 val cert_arity = prep_arity (K I) Sign.certify_sort Sign.certify_sort;
-val read_simple_arity = prep_arity Sign.intern_tycon Sign.read_sort Sign.intern_class;
-fun cert_simple_arity arg = prep_arity (K I) Sign.certify_sort (K I) arg;
 
 
 (* old-style instance declarations *)
@@ -417,17 +418,18 @@
 
 (** instance proof interfaces **)
 
-fun inst_attribute add_thms (thy, thm) = (add_thms [thm] thy, thm);
+fun inst_proof mk_prop add_thms inst int theory =
+  theory
+  |> IsarThy.multi_theorem_i Drule.internalK
+    ("", [fn (thy, th) => (add_thms [th] thy, th)]) []
+    (map (fn t => (("", []), [(t, ([], []))])) (mk_prop (Theory.sign_of theory) inst)) int;
 
-fun inst_proof mk_prop add_thms sig_prop int thy =
-  thy
-  |> IsarThy.theorem_i Drule.internalK (("", [inst_attribute add_thms]),
-    (mk_prop (Theory.sign_of thy) sig_prop, ([], []))) int;
-
-val instance_subclass_proof = inst_proof (mk_classrel oo read_classrel) add_classrel_thms;
-val instance_subclass_proof_i = inst_proof (mk_classrel oo cert_classrel) add_classrel_thms;
-val instance_arity_proof = inst_proof (mk_arity oo read_simple_arity) add_arity_thms;
-val instance_arity_proof_i = inst_proof (mk_arity oo cert_simple_arity) add_arity_thms;
+val instance_subclass_proof =
+  inst_proof (single oo (mk_classrel oo read_classrel)) add_classrel_thms;
+val instance_subclass_proof_i =
+  inst_proof (single oo (mk_classrel oo cert_classrel)) add_classrel_thms;
+val instance_arity_proof = inst_proof (mk_arities oo read_arity) add_arity_thms;
+val instance_arity_proof_i = inst_proof (mk_arities oo cert_arity) add_arity_thms;
 
 
 
@@ -453,7 +455,7 @@
 val instanceP =
   OuterSyntax.command "instance" "prove type arity or subclass relation" K.thy_goal
     ((P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.xname) >> instance_subclass_proof ||
-      (P.xname -- (P.$$$ "::" |-- P.simple_arity) >> P.triple2) >> instance_arity_proof)
+      (P.xname -- (P.$$$ "::" |-- P.arity) >> P.triple2) >> instance_arity_proof)
       >> (Toplevel.print oo Toplevel.theory_to_proof));
 
 val _ = OuterSyntax.add_parsers [axclassP, instanceP];