# HG changeset patch
# User haftmann
# Date 1133422082 -3600
# Node ID 4595eb4627fa9f6037461833de3e2026c7763843
# Parent  e61d2424863d3c4926009a68dad1f76214be585d
oriented pairs theory * 'a to 'a * theory

diff -r e61d2424863d -r 4595eb4627fa src/HOL/Tools/datatype_abs_proofs.ML
--- 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 =
diff -r e61d2424863d -r 4595eb4627fa src/HOL/Tools/datatype_aux.ML
--- 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) []);
 
diff -r e61d2424863d -r 4595eb4627fa src/HOL/Tools/datatype_package.ML
--- 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,
diff -r e61d2424863d -r 4595eb4627fa src/HOL/Tools/datatype_rep_proofs.ML
--- 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;
diff -r e61d2424863d -r 4595eb4627fa src/HOL/Tools/inductive_realizer.ML
--- 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)) =>