--- a/src/HOL/Tools/datatype_abs_proofs.ML Thu Dec 01 06:28:41 2005 +0100
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Thu Dec 01 08:28:02 2005 +0100
@@ -19,28 +19,28 @@
sig
val prove_casedist_thms : string list ->
DatatypeAux.descr list -> (string * sort) list -> thm ->
- theory attribute list -> theory -> theory * thm list
+ theory attribute list -> theory -> thm list * theory
val prove_primrec_thms : bool -> string list ->
DatatypeAux.descr list -> (string * sort) list ->
DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
- simpset -> thm -> theory -> theory * (string list * thm list)
+ simpset -> thm -> theory -> (string list * thm list) * theory
val prove_case_thms : bool -> string list ->
DatatypeAux.descr list -> (string * sort) list ->
- string list -> thm list -> theory -> theory * (thm list list * string list)
+ string list -> thm list -> theory -> (thm list list * string list) * theory
val prove_split_thms : string list ->
DatatypeAux.descr list -> (string * sort) list ->
thm list list -> thm list list -> thm list -> thm list list -> theory ->
- theory * (thm * thm) list
+ (thm * thm) list * theory
val prove_size_thms : bool -> string list ->
DatatypeAux.descr list -> (string * sort) list ->
- string list -> thm list -> theory -> theory * thm list
+ string list -> thm list -> theory -> thm list * theory
val prove_nchotomys : string list -> DatatypeAux.descr list ->
- (string * sort) list -> thm list -> theory -> theory * thm list
+ (string * sort) list -> thm list -> theory -> thm list * theory
val prove_weak_case_congs : string list -> DatatypeAux.descr list ->
- (string * sort) list -> theory -> theory * thm list
+ (string * sort) list -> theory -> thm list * theory
val prove_case_congs : string list ->
DatatypeAux.descr list -> (string * sort) list ->
- thm list -> thm list list -> theory -> theory * thm list
+ thm list -> thm list list -> theory -> thm list * theory
end;
structure DatatypeAbsProofs: DATATYPE_ABS_PROOFS =
@@ -84,7 +84,10 @@
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
+ thy
+ |> store_thms_atts "exhaust" new_type_names (map single case_names_exhausts) casedist_thms
+ end;
(*************************** primrec combinators ******************************)
@@ -256,9 +259,11 @@
(DatatypeProp.make_primrecs new_type_names descr sorts thy2)
in
- thy2 |> Theory.add_path (space_implode "_" new_type_names) |>
- PureThy.add_thmss [(("recs", rec_thms), [])] |>>
- Theory.parent_path |> apsnd (pair reccomb_names o List.concat)
+ thy2
+ |> Theory.add_path (space_implode "_" new_type_names)
+ |> PureThy.add_thmss [(("recs", rec_thms), [])] |> Library.swap
+ ||> Theory.parent_path
+ |-> (fn thms => pair (reccomb_names, Library.flat thms))
end;
@@ -326,10 +331,10 @@
(DatatypeProp.make_cases new_type_names descr sorts thy2)
in
- thy2 |>
- parent_path flat_names |>
- store_thmss "cases" new_type_names case_thms |>
- apsnd (rpair case_names)
+ thy2
+ |> parent_path flat_names
+ |> store_thmss "cases" new_type_names case_thms
+ |-> (fn thmss => pair (thmss, case_names))
end;
@@ -365,8 +370,10 @@
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 |> apsnd ListPair.zip
+ thy
+ |> store_thms "split" new_type_names split_thms
+ ||>> store_thms "split_asm" new_type_names split_asm_thms
+ |-> (fn (thms1, thms2) => pair (thms1 ~~ thms2))
end;
(******************************* size functions *******************************)
@@ -376,7 +383,7 @@
is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs)
(List.concat descr)
then
- (thy, [])
+ ([], thy)
else
let
val _ = message "Proving equations for size function ...";
@@ -426,9 +433,11 @@
(DatatypeProp.make_size descr sorts thy')
in
- thy' |> Theory.add_path big_name |>
- PureThy.add_thmss [(("size", size_thms), [])] |>>
- Theory.parent_path |> apsnd List.concat
+ thy'
+ |> Theory.add_path big_name
+ |> PureThy.add_thmss [(("size", size_thms), [])] |> Library.swap
+ ||> Theory.parent_path
+ |-> (fn thmss => pair (Library.flat thmss))
end;
fun prove_weak_case_congs new_type_names descr sorts thy =
--- a/src/HOL/Tools/datatype_aux.ML Thu Dec 01 06:28:41 2005 +0100
+++ b/src/HOL/Tools/datatype_aux.ML Thu Dec 01 08:28:02 2005 +0100
@@ -15,12 +15,10 @@
val add_path : bool -> string -> theory -> theory
val parent_path : bool -> theory -> theory
- val store_thmss_atts : string -> string list -> theory attribute list list -> thm list list
- -> theory -> theory * thm list list
- val store_thmss : string -> string list -> thm list list -> theory -> theory * thm list list
+ val store_thmss : string -> string list -> thm list list -> theory -> thm list list * theory
val store_thms_atts : string -> string list -> theory attribute list list -> thm list
- -> theory -> theory * thm list
- val store_thms : string -> string list -> thm list -> theory -> theory * thm list
+ -> theory -> thm list * theory
+ val store_thms : string -> string list -> thm list -> theory -> thm list * theory
val split_conj_thm : thm -> thm list
val mk_conj : term list -> term
@@ -86,7 +84,7 @@
foldl_map (fn (thy', ((tname, atts), thms)) => thy' |>
Theory.add_path tname |>
(apsnd hd o PureThy.add_thmss [((label, thms), atts)]) |>>
- Theory.parent_path);
+ Theory.parent_path) |> Library.swap;
fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []);
@@ -95,7 +93,7 @@
foldl_map (fn (thy', ((tname, atts), thm)) => thy' |>
Theory.add_path tname |>
(apsnd hd o PureThy.add_thms [((label, thm), atts)]) |>>
- Theory.parent_path);
+ Theory.parent_path) |> Library.swap;
fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []);
--- a/src/HOL/Tools/datatype_package.ML Thu Dec 01 06:28:41 2005 +0100
+++ b/src/HOL/Tools/datatype_package.ML Thu Dec 01 08:28:02 2005 +0100
@@ -686,7 +686,7 @@
put_datatypes (fold Symtab.update dt_infos dt_info) |>
add_cases_induct dt_infos induct |>
Theory.parent_path |>
- (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
+ store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd |>
DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos);
in
({distinct = distinct,
@@ -708,25 +708,25 @@
let
val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
- val (thy2, inject, distinct, dist_rewrites, simproc_dists, induct) = thy |>
+ val ((inject, distinct, dist_rewrites, simproc_dists, induct), thy2) = thy |>
DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts
types_syntax constr_syntax case_names_induct;
- val (thy3, casedist_thms) = DatatypeAbsProofs.prove_casedist_thms new_type_names descr
+ val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms new_type_names descr
sorts induct case_names_exhausts thy2;
- val (thy4, (reccomb_names, rec_thms)) = DatatypeAbsProofs.prove_primrec_thms
+ val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
flat_names new_type_names descr sorts dt_info inject dist_rewrites dist_ss induct thy3;
- val (thy6, (case_thms, case_names)) = DatatypeAbsProofs.prove_case_thms
+ val ((case_thms, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
flat_names new_type_names descr sorts reccomb_names rec_thms thy4;
- val (thy7, split_thms) = DatatypeAbsProofs.prove_split_thms new_type_names
+ val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms new_type_names
descr sorts inject dist_rewrites casedist_thms case_thms thy6;
- val (thy8, nchotomys) = DatatypeAbsProofs.prove_nchotomys new_type_names
+ val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys new_type_names
descr sorts casedist_thms thy7;
- val (thy9, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names
+ val (case_congs, thy9) = DatatypeAbsProofs.prove_case_congs new_type_names
descr sorts nchotomys case_thms thy8;
- val (thy10, weak_case_congs) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
+ val (weak_case_congs, thy10) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
descr sorts thy9;
- val (thy11, size_thms) = DatatypeAbsProofs.prove_size_thms flat_names new_type_names
+ val (size_thms, thy11) = DatatypeAbsProofs.prove_size_thms flat_names new_type_names
descr sorts reccomb_names rec_thms thy10;
val dt_infos = map (make_dt_info (List.concat descr) induct reccomb_names rec_thms)
@@ -743,7 +743,7 @@
put_datatypes (fold Symtab.update dt_infos dt_info) |>
add_cases_induct dt_infos induct |>
Theory.parent_path |>
- (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
+ store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd |>
DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos);
in
({distinct = distinct,
@@ -810,32 +810,32 @@
val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
- val (thy2, casedist_thms) = thy1 |>
+ val (casedist_thms, thy2) = thy1 |>
DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction
case_names_exhausts;
- val (thy3, (reccomb_names, rec_thms)) = DatatypeAbsProofs.prove_primrec_thms
+ val ((reccomb_names, rec_thms), thy3) = DatatypeAbsProofs.prove_primrec_thms
false new_type_names [descr] sorts dt_info inject distinct dist_ss induction thy2;
- val (thy4, (case_thms, case_names)) = DatatypeAbsProofs.prove_case_thms false
+ val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms false
new_type_names [descr] sorts reccomb_names rec_thms thy3;
- val (thy5, split_thms) = DatatypeAbsProofs.prove_split_thms
+ val (split_thms, thy5) = DatatypeAbsProofs.prove_split_thms
new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
- val (thy6, nchotomys) = DatatypeAbsProofs.prove_nchotomys new_type_names
+ val (nchotomys, thy6) = DatatypeAbsProofs.prove_nchotomys new_type_names
[descr] sorts casedist_thms thy5;
- val (thy7, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names
+ val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
[descr] sorts nchotomys case_thms thy6;
- val (thy8, weak_case_congs) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
+ val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
[descr] sorts thy7;
- val (thy9, size_thms) =
+ val (size_thms, thy9) =
if Context.exists_name "NatArith" thy8 then
DatatypeAbsProofs.prove_size_thms false new_type_names
[descr] sorts reccomb_names rec_thms thy8
- else (thy8, []);
+ else ([], thy8);
- val (thy10, [induction']) = thy9 |>
- (#1 o store_thmss "inject" new_type_names inject) |>
- (#1 o store_thmss "distinct" new_type_names distinct) |>
+ val ([induction'], thy10) = thy9 |>
+ store_thmss "inject" new_type_names inject |> snd |>
+ store_thmss "distinct" new_type_names distinct |> snd |>
Theory.add_path (space_implode "_" new_type_names) |>
- PureThy.add_thms [(("induct", induction), [case_names_induct])];
+ PureThy.add_thms [(("induct", induction), [case_names_induct])] |> Library.swap;
val dt_infos = map (make_dt_info descr induction' reccomb_names rec_thms)
((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
@@ -850,7 +850,7 @@
put_datatypes (fold Symtab.update dt_infos dt_info) |>
add_cases_induct dt_infos induction' |>
Theory.parent_path |>
- (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
+ (snd o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos);
in
({distinct = distinct,
--- a/src/HOL/Tools/datatype_rep_proofs.ML Thu Dec 01 06:28:41 2005 +0100
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Thu Dec 01 08:28:02 2005 +0100
@@ -16,8 +16,8 @@
val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
string list -> DatatypeAux.descr list -> (string * sort) 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
+ -> theory -> (thm list list * thm list list * thm list list *
+ DatatypeAux.simproc_dist list * thm) * theory
end;
structure DatatypeRepProofs : DATATYPE_REP_PROOFS =
@@ -577,9 +577,11 @@
val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms);
- val (thy6, (constr_inject', distinct_thms'))= thy5 |> parent_path flat_names |>
- store_thmss "inject" new_type_names constr_inject |>>>
- store_thmss "distinct" new_type_names distinct_thms;
+ val ((constr_inject', distinct_thms'), thy6) =
+ thy5
+ |> parent_path flat_names
+ |> store_thmss "inject" new_type_names constr_inject
+ ||>> store_thmss "distinct" new_type_names distinct_thms;
(*************************** induction theorem ****************************)
@@ -642,7 +644,8 @@
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
+ ((constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct'), thy7)
end;
end;
--- a/src/HOL/Tools/inductive_realizer.ML Thu Dec 01 06:28:41 2005 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Thu Dec 01 08:28:02 2005 +0100
@@ -239,13 +239,19 @@
if name = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
else x;
-fun add_dummies f dts used thy =
- apsnd (pair (map fst dts)) (f (map snd dts) thy)
- handle DatatypeAux.Datatype_Empty name' =>
+fun add_dummies f [] _ thy =
+ (([], NONE), thy)
+ | add_dummies f dts used thy =
+ thy
+ |> f (map snd dts)
+ |-> (fn dtinfo => pair ((map fst dts), SOME dtinfo))
+ handle DatatypeAux.Datatype_Empty name' =>
let
val name = Sign.base_name name';
val dname = variant used "Dummy"
- in add_dummies f (map (add_dummy name dname) dts) (dname :: used) thy
+ in
+ thy
+ |> add_dummies f (map (add_dummy name dname) dts) (dname :: used)
end;
fun mk_realizer thy vs params ((rule, rrule), rt) =
@@ -310,15 +316,14 @@
(** datatype representing computational content of inductive set **)
- val (thy2, (dummies, dt_info)) =
+ val ((dummies, dt_info), thy2) =
thy1
- |> (if null dts
- then rpair ([], NONE)
- else add_dummies (DatatypePackage.add_datatype_i false false
- (map #2 dts)) (map (pair false) dts) [] #> (fn (v, (b, thy)) => (thy, (b, SOME v))))
- |>> Extraction.add_typeof_eqns_i ty_eqs
- |>> Extraction.add_realizes_eqns_i rlz_eqs;
- fun get f x = getOpt (Option.map f x, []);
+ |> add_dummies
+ (DatatypePackage.add_datatype_i false false (map #2 dts))
+ (map (pair false) dts) []
+ ||> Extraction.add_typeof_eqns_i ty_eqs
+ ||> Extraction.add_realizes_eqns_i rlz_eqs;
+ fun get f = (these oo Option.map) f;
val rec_names = distinct (map (fst o dest_Const o head_of o fst o
HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info));
val (_, constrss) = foldl_map (fn ((recs, dummies), (s, rs)) =>