author haftmann Sun Jul 23 07:19:26 2006 +0200 (2006-07-23) changeset 20182 79c9ff40d760 parent 20181 87b2dfbf31fc child 20183 fd546b0c8a7c
tactic for prove_instance_arity now gets definition theorems as arguments
```     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Jul 21 14:49:11 2006 +0200
1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Sun Jul 23 07:19:26 2006 +0200
1.3 @@ -19,8 +19,8 @@
1.4      -> ((string * sort) list * (string * (string * typ list) list) list)
1.5    val get_datatype_arities: theory -> string list -> sort
1.6      -> (string * (((string * sort list) * sort)  * term list)) list option
1.7 -  val datatype_prove_arities : tactic -> string list -> sort
1.8 -    -> ((string * term list) list
1.9 +  val prove_arities: (thm list -> tactic) -> string list -> sort
1.10 +    -> (((string * sort list) * sort) list -> (string * term list) list
1.11      -> ((bstring * attribute list) * term) list) -> theory -> theory
1.12    val setup: theory -> theory
1.13  end;
1.14 @@ -373,7 +373,7 @@
1.15      ) else NONE
1.16    end;
1.17
1.18 -fun datatype_prove_arities tac tycos sort f thy =
1.19 +fun prove_arities tac tycos sort f thy =
1.20    case get_datatype_arities thy tycos sort
1.21     of NONE => thy
1.22      | SOME insts => let
1.23 @@ -382,11 +382,11 @@
1.24              (Type (tyco, map TFree (Name.give_names Name.context "'a" asorts)), sort);
1.25          val (arities, css) = (split_list o map_filter
1.26            (fn (tyco, (arity, cs)) => if proven arity
1.27 -            then SOME (arity, (tyco, cs)) else NONE)) insts;
1.28 +            then NONE else SOME (arity, (tyco, cs)))) insts;
1.29        in
1.30          thy
1.31 -        |> ClassPackage.prove_instance_arity tac
1.32 -             arities ("", []) (f css)
1.33 +        |> K ((not o null) arities) ? ClassPackage.prove_instance_arity tac
1.34 +             arities ("", []) (f arities css)
1.35        end;
1.36
1.37  fun dtyp_of_case_const thy c =
```
```     2.1 --- a/src/Pure/Tools/class_package.ML	Fri Jul 21 14:49:11 2006 +0200
2.2 +++ b/src/Pure/Tools/class_package.ML	Sun Jul 23 07:19:26 2006 +0200
2.3 @@ -18,7 +18,7 @@
2.4    val instance_arity_i: ((string * sort list) * sort) list
2.5      -> bstring * attribute list -> ((bstring * attribute list) * term) list
2.6      -> theory -> Proof.state
2.7 -  val prove_instance_arity: tactic -> ((string * sort list) * sort) list
2.8 +  val prove_instance_arity: (thm list -> tactic) -> ((string * sort list) * sort) list
2.9      -> bstring * attribute list -> ((bstring * attribute list) * term) list
2.10      -> theory -> theory
2.11    val instance_sort: string * string -> theory -> Proof.state
2.12 @@ -52,7 +52,7 @@
2.13    val sortlookups_const: theory -> string * typ -> classlookup list list
2.14  end;
2.15
2.16 -structure ClassPackage: CLASS_PACKAGE =
2.17 +structure ClassPackage : CLASS_PACKAGE =
2.18  struct
2.19
2.20
2.21 @@ -281,12 +281,12 @@
2.22
2.23  in
2.24
2.25 -val axclass_instance_sort =
2.26 -  gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I o single;
2.27  val axclass_instance_arity =
2.29  val axclass_instance_arity_i =
2.30    gen_instance (Logic.mk_arities oo Sign.cert_arity) AxClass.add_arity;
2.31 +val axclass_instance_sort =
2.32 +  gen_instance (single oo (Logic.mk_classrel oo AxClass.read_classrel)) AxClass.add_classrel I o single;
2.33
2.34  end;
2.35
2.36 @@ -511,21 +511,21 @@
2.37      |-> (fn (cs, def_thms) =>
2.39      #> note_all
2.40 -    #> do_proof (after_qed cs) arities)
2.41 +    #> do_proof (map snd def_thms) (after_qed cs) arities)
2.42    end;
2.43
2.44  fun instance_arity' do_proof = gen_instance_arity Sign.read_arity Attrib.attribute
2.46  fun instance_arity_i' do_proof = gen_instance_arity Sign.cert_arity (K I)
2.48 -fun tactic_proof tac after_qed arities =
2.49 -  fold (fn arity => AxClass.prove_arity arity tac) arities
2.50 +fun tactic_proof tac def_thms after_qed arities =
2.51 +  fold (fn arity => AxClass.prove_arity arity (tac def_thms)) arities
2.52    #> after_qed;
2.53
2.54  in
2.55
2.56 -val instance_arity = instance_arity' axclass_instance_arity_i;
2.57 -val instance_arity_i = instance_arity_i' axclass_instance_arity_i;
2.58 +val instance_arity = instance_arity' (K axclass_instance_arity_i);
2.59 +val instance_arity_i = instance_arity_i' (K axclass_instance_arity_i);
2.60  val prove_instance_arity = instance_arity_i' o tactic_proof;
2.61
2.62  end; (* local *)
```