--- a/src/HOL/Tools/datatype_abs_proofs.ML Mon Mar 13 13:22:31 2000 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Mon Mar 13 13:24:12 2000 +0100
@@ -20,14 +20,14 @@
sig
val prove_casedist_thms : string list -> (int * (string * DatatypeAux.dtyp list *
(string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
- thm -> theory -> theory * thm list
+ thm -> theory attribute list -> theory -> theory * thm list
val prove_primrec_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
(string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
simpset -> thm -> theory -> theory * string list * thm list
val prove_case_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
(string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
- string list -> thm list -> theory -> theory * string list * thm list list
+ string list -> thm list -> theory -> theory * (thm list list * string list)
val prove_split_thms : string list -> (int * (string * DatatypeAux.dtyp list *
(string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
thm list list -> thm list list -> thm list -> thm list list -> theory ->
@@ -43,7 +43,7 @@
thm list -> thm list list -> theory -> theory * thm list
end;
-structure DatatypeAbsProofs : DATATYPE_ABS_PROOFS =
+structure DatatypeAbsProofs: DATATYPE_ABS_PROOFS =
struct
open DatatypeAux;
@@ -54,7 +54,7 @@
(************************ case distinction theorems ***************************)
-fun prove_casedist_thms new_type_names descr sorts induct thy =
+fun prove_casedist_thms new_type_names descr sorts induct case_names_exhausts thy =
let
val _ = message "Proving case distinction theorems ...";
@@ -85,10 +85,8 @@
val casedist_thms = map prove_casedist_thm ((0 upto (length newTs - 1)) ~~
(DatatypeProp.make_casedists descr sorts) ~~ newTs)
+ in thy |> store_thms_atts "exhaust" new_type_names (map single case_names_exhausts) casedist_thms end;
- in
- (store_thms "exhaust" new_type_names casedist_thms thy, casedist_thms)
- end;
(*************************** primrec combinators ******************************)
@@ -256,7 +254,7 @@
(Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
(reccomb_names ~~ recTs ~~ rec_result_Ts);
- val thy2 = thy1 |>
+ val (thy2, reccomb_defs) = thy1 |>
Theory.add_consts_i (map (fn ((name, T), T') =>
(Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
(reccomb_names ~~ recTs ~~ rec_result_Ts)) |>
@@ -264,10 +262,9 @@
((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T,
Const ("Eps", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set))))))
- (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) |>
+ (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) |>>
parent_path flat_names;
- val reccomb_defs = map ((get_def thy2) o Sign.base_name) reccomb_names;
(* prove characteristic equations for primrec combinators *)
@@ -284,7 +281,7 @@
in
(thy2 |> Theory.add_path (space_implode "_" new_type_names) |>
- PureThy.add_thmss [(("recs", rec_thms), [])] |>
+ (#1 o PureThy.add_thmss [(("recs", rec_thms), [])]) |>
Theory.parent_path,
reccomb_names, rec_thms)
end;
@@ -342,10 +339,10 @@
Logic.mk_equals (list_comb (Const (name, caseT), fns1),
list_comb (reccomb, (flat (take (i, case_dummy_fns))) @
fns2 @ (flat (drop (i + 1, case_dummy_fns))) )));
- val thy' = thy |>
+ val (thy', [def_thm]) = thy |>
Theory.add_consts_i [decl] |> (PureThy.add_defs_i o map Thm.no_attributes) [def];
- in (defs @ [get_def thy' (Sign.base_name name)], thy')
+ in (defs @ [def_thm], thy')
end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
(take (length newTs, reccomb_names)));
@@ -358,9 +355,7 @@
(DatatypeProp.make_case_trrules new_type_names descr) |>
parent_path flat_names;
- in
- (store_thmss "cases" new_type_names case_thms thy3, case_names, case_thms)
- end;
+ in thy3 |> store_thmss "cases" new_type_names case_thms |> apsnd (rpair case_names) end;
(******************************* case splitting *******************************)
@@ -395,9 +390,8 @@
val (split_thms, split_asm_thms) = ListPair.unzip split_thm_pairs
in
- (thy |> store_thms "split" new_type_names split_thms |>
- store_thms "split_asm" new_type_names split_asm_thms,
- split_thm_pairs)
+ thy |> store_thms "split" new_type_names split_thms |>>>
+ store_thms "split_asm" new_type_names split_asm_thms |> apsnd ListPair.zip
end;
(******************************* size functions *******************************)
@@ -442,17 +436,16 @@
val fs = flat (map (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr');
val fTs = map fastype_of fs;
- val thy' = thy1 |>
+ val (thy', size_def_thms) = thy1 |>
Theory.add_consts_i (map (fn (s, T) =>
(Sign.base_name s, T --> HOLogic.natT, NoSyn))
(drop (length (hd descr), size_names ~~ recTs))) |>
(PureThy.add_defs_i o map Thm.no_attributes) (map (fn (((s, T), def_name), rec_name) =>
(def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT),
list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs))))
- (size_names ~~ recTs ~~ def_names ~~ reccomb_names)) |>
+ (size_names ~~ recTs ~~ def_names ~~ reccomb_names)) |>>
parent_path flat_names;
- val size_def_thms = map (get_thm thy') def_names;
val rewrites = size_def_thms @ map mk_meta_eq primrec_thms;
val size_thms = map (fn t => prove_goalw_cterm rewrites
@@ -461,7 +454,7 @@
in
(thy' |> Theory.add_path big_name |>
- PureThy.add_thmss [(("size", size_thms), [])] |>
+ (#1 o PureThy.add_thmss [(("size", size_thms), [])]) |>
Theory.parent_path,
size_thms)
end;
@@ -488,9 +481,7 @@
val nchotomys =
map prove_nchotomy (DatatypeProp.make_nchotomys descr sorts ~~ casedist_thms)
- in
- (store_thms "nchotomy" new_type_names nchotomys thy, nchotomys)
- end;
+ in thy |> store_thms "nchotomy" new_type_names nchotomys end;
fun prove_case_congs new_type_names descr sorts nchotomys case_thms thy =
let
@@ -515,8 +506,6 @@
val case_congs = map prove_case_cong (DatatypeProp.make_case_congs
new_type_names descr sorts thy ~~ nchotomys ~~ case_thms)
- in
- (store_thms "case_cong" new_type_names case_congs thy, case_congs)
- end;
+ in thy |> store_thms "case_cong" new_type_names case_congs end;
end;
--- a/src/HOL/Tools/datatype_rep_proofs.ML Mon Mar 13 13:22:31 2000 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Mon Mar 13 13:24:12 2000 +0100
@@ -17,8 +17,8 @@
val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
string list -> (int * (string * DatatypeAux.dtyp list *
(string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
- (string * mixfix) list -> (string * mixfix) list list -> theory ->
- theory * thm list list * thm list list * thm list list *
+ (string * mixfix) list -> (string * mixfix) list list -> theory attribute
+ -> theory -> theory * thm list list * thm list list * thm list list *
DatatypeAux.simproc_dist list * thm
end;
@@ -42,7 +42,7 @@
(******************************************************************************)
fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
- new_type_names descr sorts types_syntax constr_syntax thy =
+ new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
let
val Datatype_thy = theory "Datatype";
val node_name = Sign.intern_tycon (Theory.sign_of Datatype_thy) "node";
@@ -231,12 +231,11 @@
val def_name = (Sign.base_name cname) ^ "_def";
val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
(Const (rep_name, T --> Univ_elT) $ lhs, rhs));
- val thy' = thy |>
+ val (thy', [def_thm]) = thy |>
Theory.add_consts_i [(cname', constrT, mx)] |>
(PureThy.add_defs_i o map Thm.no_attributes) [(def_name, def)];
- in (thy', defs @ [get_thm thy' def_name], eqns @ [eqn], i + 1)
- end;
+ in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
(* constructor definitions for datatype *)
@@ -382,8 +381,7 @@
val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def",
equals (T --> Univ_elT) $ Const (iso_name, T --> Univ_elT) $
list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs))) (rec_names ~~ isos);
- val thy' = (PureThy.add_defs_i o map Thm.no_attributes) defs thy;
- val def_thms = map (get_thm thy') (map fst defs);
+ val (thy', def_thms) = (PureThy.add_defs_i o map Thm.no_attributes) defs thy;
(* prove characteristic equations *)
@@ -580,8 +578,8 @@
((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms);
val thy6 = thy5 |> parent_path flat_names |>
- store_thmss "inject" new_type_names constr_inject |>
- store_thmss "distinct" new_type_names distinct_thms;
+ (#1 o store_thmss "inject" new_type_names constr_inject) |>
+ (#1 o store_thmss "distinct" new_type_names distinct_thms);
(*************************** induction theorem ****************************)
@@ -638,12 +636,12 @@
rtac allI 1, dtac FunsD 1, etac CollectD 1]))]))
(prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
- val thy7 = thy6 |>
+ val (thy7, [dt_induct']) = thy6 |>
Theory.add_path big_name |>
- PureThy.add_thms [(("induct", dt_induct), [])] |>
+ PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
Theory.parent_path;
- in (thy7, constr_inject, distinct_thms, dist_rewrites, simproc_dists, dt_induct)
+ in (thy7, constr_inject, distinct_thms, dist_rewrites, simproc_dists, dt_induct')
end;
end;