tactic for prove_instance_arity now gets definition theorems as arguments
authorhaftmann
Sun Jul 23 07:19:26 2006 +0200 (2006-07-23)
changeset 2018279c9ff40d760
parent 20181 87b2dfbf31fc
child 20183 fd546b0c8a7c
tactic for prove_instance_arity now gets definition theorems as arguments
src/HOL/Tools/datatype_codegen.ML
src/Pure/Tools/class_package.ML
     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.28    gen_instance (Logic.mk_arities oo Sign.read_arity) AxClass.add_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.38         fold add_inst_def 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.45    read_def do_proof;
    2.46  fun instance_arity_i' do_proof = gen_instance_arity Sign.cert_arity (K I)
    2.47    read_def_i do_proof;
    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 *)