# HG changeset patch
# User haftmann
# Date 1153631966 -7200
# Node ID 79c9ff40d760fcc9a0bdc602201c6fa8f3b91401
# Parent  87b2dfbf31fc3707ef3d5410f23ab8cb077316d0
tactic for prove_instance_arity now gets definition theorems as arguments

diff -r 87b2dfbf31fc -r 79c9ff40d760 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Fri Jul 21 14:49:11 2006 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML	Sun Jul 23 07:19:26 2006 +0200
@@ -19,8 +19,8 @@
     -> ((string * sort) list * (string * (string * typ list) list) list)
   val get_datatype_arities: theory -> string list -> sort
     -> (string * (((string * sort list) * sort)  * term list)) list option
-  val datatype_prove_arities : tactic -> string list -> sort
-    -> ((string * term list) list
+  val prove_arities: (thm list -> tactic) -> string list -> sort
+    -> (((string * sort list) * sort) list -> (string * term list) list
     -> ((bstring * attribute list) * term) list) -> theory -> theory
   val setup: theory -> theory
 end;
@@ -373,7 +373,7 @@
     ) else NONE
   end;
 
-fun datatype_prove_arities tac tycos sort f thy =
+fun prove_arities tac tycos sort f thy =
   case get_datatype_arities thy tycos sort
    of NONE => thy
     | SOME insts => let
@@ -382,11 +382,11 @@
             (Type (tyco, map TFree (Name.give_names Name.context "'a" asorts)), sort);
         val (arities, css) = (split_list o map_filter
           (fn (tyco, (arity, cs)) => if proven arity
-            then SOME (arity, (tyco, cs)) else NONE)) insts;
+            then NONE else SOME (arity, (tyco, cs)))) insts;
       in
         thy
-        |> ClassPackage.prove_instance_arity tac
-             arities ("", []) (f css)
+        |> K ((not o null) arities) ? ClassPackage.prove_instance_arity tac
+             arities ("", []) (f arities css)
       end;
 
 fun dtyp_of_case_const thy c =
diff -r 87b2dfbf31fc -r 79c9ff40d760 src/Pure/Tools/class_package.ML
--- a/src/Pure/Tools/class_package.ML	Fri Jul 21 14:49:11 2006 +0200
+++ b/src/Pure/Tools/class_package.ML	Sun Jul 23 07:19:26 2006 +0200
@@ -18,7 +18,7 @@
   val instance_arity_i: ((string * sort list) * sort) list
     -> bstring * attribute list -> ((bstring * attribute list) * term) list
     -> theory -> Proof.state
-  val prove_instance_arity: tactic -> ((string * sort list) * sort) list
+  val prove_instance_arity: (thm list -> tactic) -> ((string * sort list) * sort) list
     -> bstring * attribute list -> ((bstring * attribute list) * term) list
     -> theory -> theory
   val instance_sort: string * string -> theory -> Proof.state
@@ -52,7 +52,7 @@
   val sortlookups_const: theory -> string * typ -> classlookup list list
 end;
 
-structure ClassPackage: CLASS_PACKAGE =
+structure ClassPackage : CLASS_PACKAGE =
 struct
 
 
@@ -281,12 +281,12 @@
 
 in
 
-val axclass_instance_sort =
-  gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I o single;
 val axclass_instance_arity =
   gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_arity;
 val axclass_instance_arity_i =
   gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity;
+val axclass_instance_sort =      
+  gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I o single;
 
 end;
 
@@ -511,21 +511,21 @@
     |-> (fn (cs, def_thms) =>
        fold add_inst_def def_thms
     #> note_all
-    #> do_proof (after_qed cs) arities)
+    #> do_proof (map snd def_thms) (after_qed cs) arities)
   end;
 
 fun instance_arity' do_proof = gen_instance_arity Sign.read_arity Attrib.attribute
   read_def do_proof;
 fun instance_arity_i' do_proof = gen_instance_arity Sign.cert_arity (K I)
   read_def_i do_proof;
-fun tactic_proof tac after_qed arities =
-  fold (fn arity => AxClass.prove_arity arity tac) arities
+fun tactic_proof tac def_thms after_qed arities =
+  fold (fn arity => AxClass.prove_arity arity (tac def_thms)) arities
   #> after_qed;
 
 in
 
-val instance_arity = instance_arity' axclass_instance_arity_i;
-val instance_arity_i = instance_arity_i' axclass_instance_arity_i;
+val instance_arity = instance_arity' (K axclass_instance_arity_i);
+val instance_arity_i = instance_arity_i' (K axclass_instance_arity_i);
 val prove_instance_arity = instance_arity_i' o tactic_proof;
 
 end; (* local *)