oriented pairs theory * 'a to 'a * theory
authorhaftmann
Thu Dec 01 08:28:02 2005 +0100 (2005-12-01)
changeset 183144595eb4627fa
parent 18313 e61d2424863d
child 18315 e52f867ab851
oriented pairs theory * 'a to 'a * theory
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_aux.ML
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/datatype_rep_proofs.ML
src/HOL/Tools/inductive_realizer.ML
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Thu Dec 01 06:28:41 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Thu Dec 01 08:28:02 2005 +0100
     1.3 @@ -19,28 +19,28 @@
     1.4  sig
     1.5    val prove_casedist_thms : string list ->
     1.6      DatatypeAux.descr list -> (string * sort) list -> thm ->
     1.7 -    theory attribute list -> theory -> theory * thm list
     1.8 +    theory attribute list -> theory -> thm list * theory
     1.9    val prove_primrec_thms : bool -> string list ->
    1.10      DatatypeAux.descr list -> (string * sort) list ->
    1.11        DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
    1.12 -        simpset -> thm -> theory -> theory * (string list * thm list)
    1.13 +        simpset -> thm -> theory -> (string list * thm list) * theory
    1.14    val prove_case_thms : bool -> string list ->
    1.15      DatatypeAux.descr list -> (string * sort) list ->
    1.16 -      string list -> thm list -> theory -> theory * (thm list list * string list)
    1.17 +      string list -> thm list -> theory -> (thm list list * string list) * theory
    1.18    val prove_split_thms : string list ->
    1.19      DatatypeAux.descr list -> (string * sort) list ->
    1.20        thm list list -> thm list list -> thm list -> thm list list -> theory ->
    1.21 -        theory * (thm * thm) list
    1.22 +        (thm * thm) list * theory
    1.23    val prove_size_thms : bool -> string list ->
    1.24      DatatypeAux.descr list -> (string * sort) list ->
    1.25 -      string list -> thm list -> theory -> theory * thm list
    1.26 +      string list -> thm list -> theory -> thm list * theory
    1.27    val prove_nchotomys : string list -> DatatypeAux.descr list ->
    1.28 -    (string * sort) list -> thm list -> theory -> theory * thm list
    1.29 +    (string * sort) list -> thm list -> theory -> thm list * theory
    1.30    val prove_weak_case_congs : string list -> DatatypeAux.descr list ->
    1.31 -    (string * sort) list -> theory -> theory * thm list
    1.32 +    (string * sort) list -> theory -> thm list * theory
    1.33    val prove_case_congs : string list ->
    1.34      DatatypeAux.descr list -> (string * sort) list ->
    1.35 -      thm list -> thm list list -> theory -> theory * thm list
    1.36 +      thm list -> thm list list -> theory -> thm list * theory
    1.37  end;
    1.38  
    1.39  structure DatatypeAbsProofs: DATATYPE_ABS_PROOFS =
    1.40 @@ -84,7 +84,10 @@
    1.41  
    1.42      val casedist_thms = map prove_casedist_thm ((0 upto (length newTs - 1)) ~~
    1.43        (DatatypeProp.make_casedists descr sorts) ~~ newTs)
    1.44 -  in thy |> store_thms_atts "exhaust" new_type_names (map single case_names_exhausts) casedist_thms end;
    1.45 +  in
    1.46 +    thy
    1.47 +    |> store_thms_atts "exhaust" new_type_names (map single case_names_exhausts) casedist_thms
    1.48 +  end;
    1.49  
    1.50  
    1.51  (*************************** primrec combinators ******************************)
    1.52 @@ -256,9 +259,11 @@
    1.53             (DatatypeProp.make_primrecs new_type_names descr sorts thy2)
    1.54  
    1.55    in
    1.56 -    thy2 |> Theory.add_path (space_implode "_" new_type_names) |>
    1.57 -    PureThy.add_thmss [(("recs", rec_thms), [])] |>>
    1.58 -    Theory.parent_path |> apsnd (pair reccomb_names o List.concat)
    1.59 +    thy2
    1.60 +    |> Theory.add_path (space_implode "_" new_type_names)
    1.61 +    |> PureThy.add_thmss [(("recs", rec_thms), [])] |> Library.swap
    1.62 +    ||> Theory.parent_path
    1.63 +    |-> (fn thms => pair (reccomb_names, Library.flat thms))
    1.64    end;
    1.65  
    1.66  
    1.67 @@ -326,10 +331,10 @@
    1.68            (DatatypeProp.make_cases new_type_names descr sorts thy2)
    1.69  
    1.70    in
    1.71 -    thy2 |>
    1.72 -    parent_path flat_names |>
    1.73 -    store_thmss "cases" new_type_names case_thms |>
    1.74 -    apsnd (rpair case_names)
    1.75 +    thy2
    1.76 +    |> parent_path flat_names
    1.77 +    |> store_thmss "cases" new_type_names case_thms
    1.78 +    |-> (fn thmss => pair (thmss, case_names))
    1.79    end;
    1.80  
    1.81  
    1.82 @@ -365,8 +370,10 @@
    1.83      val (split_thms, split_asm_thms) = ListPair.unzip split_thm_pairs
    1.84  
    1.85    in
    1.86 -    thy |> store_thms "split" new_type_names split_thms |>>>
    1.87 -      store_thms "split_asm" new_type_names split_asm_thms |> apsnd ListPair.zip
    1.88 +    thy
    1.89 +    |> store_thms "split" new_type_names split_thms
    1.90 +    ||>> store_thms "split_asm" new_type_names split_asm_thms
    1.91 +    |-> (fn (thms1, thms2) => pair (thms1 ~~ thms2))
    1.92    end;
    1.93  
    1.94  (******************************* size functions *******************************)
    1.95 @@ -376,7 +383,7 @@
    1.96      is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs)
    1.97        (List.concat descr)
    1.98    then
    1.99 -    (thy, [])
   1.100 +    ([], thy)
   1.101    else
   1.102    let
   1.103      val _ = message "Proving equations for size function ...";
   1.104 @@ -426,9 +433,11 @@
   1.105          (DatatypeProp.make_size descr sorts thy')
   1.106  
   1.107    in
   1.108 -    thy' |> Theory.add_path big_name |>
   1.109 -    PureThy.add_thmss [(("size", size_thms), [])] |>>
   1.110 -    Theory.parent_path |> apsnd List.concat
   1.111 +    thy'
   1.112 +    |> Theory.add_path big_name
   1.113 +    |> PureThy.add_thmss [(("size", size_thms), [])] |> Library.swap
   1.114 +    ||> Theory.parent_path
   1.115 +    |-> (fn thmss => pair (Library.flat thmss))
   1.116    end;
   1.117  
   1.118  fun prove_weak_case_congs new_type_names descr sorts thy =
     2.1 --- a/src/HOL/Tools/datatype_aux.ML	Thu Dec 01 06:28:41 2005 +0100
     2.2 +++ b/src/HOL/Tools/datatype_aux.ML	Thu Dec 01 08:28:02 2005 +0100
     2.3 @@ -15,12 +15,10 @@
     2.4    val add_path : bool -> string -> theory -> theory
     2.5    val parent_path : bool -> theory -> theory
     2.6  
     2.7 -  val store_thmss_atts : string -> string list -> theory attribute list list -> thm list list
     2.8 -    -> theory -> theory * thm list list
     2.9 -  val store_thmss : string -> string list -> thm list list -> theory -> theory * thm list list
    2.10 +  val store_thmss : string -> string list -> thm list list -> theory -> thm list list * theory
    2.11    val store_thms_atts : string -> string list -> theory attribute list list -> thm list
    2.12 -    -> theory -> theory * thm list
    2.13 -  val store_thms : string -> string list -> thm list -> theory -> theory * thm list
    2.14 +    -> theory -> thm list * theory
    2.15 +  val store_thms : string -> string list -> thm list -> theory -> thm list * theory
    2.16  
    2.17    val split_conj_thm : thm -> thm list
    2.18    val mk_conj : term list -> term
    2.19 @@ -86,7 +84,7 @@
    2.20    foldl_map (fn (thy', ((tname, atts), thms)) => thy' |>
    2.21      Theory.add_path tname |>
    2.22      (apsnd hd o PureThy.add_thmss [((label, thms), atts)]) |>>
    2.23 -    Theory.parent_path);
    2.24 +    Theory.parent_path) |> Library.swap;
    2.25  
    2.26  fun store_thmss label tnames = store_thmss_atts label tnames (replicate (length tnames) []);
    2.27  
    2.28 @@ -95,7 +93,7 @@
    2.29    foldl_map (fn (thy', ((tname, atts), thm)) => thy' |>
    2.30      Theory.add_path tname |>
    2.31      (apsnd hd o PureThy.add_thms [((label, thm), atts)]) |>>
    2.32 -    Theory.parent_path);
    2.33 +    Theory.parent_path) |> Library.swap;
    2.34  
    2.35  fun store_thms label tnames = store_thms_atts label tnames (replicate (length tnames) []);
    2.36  
     3.1 --- a/src/HOL/Tools/datatype_package.ML	Thu Dec 01 06:28:41 2005 +0100
     3.2 +++ b/src/HOL/Tools/datatype_package.ML	Thu Dec 01 08:28:02 2005 +0100
     3.3 @@ -686,7 +686,7 @@
     3.4        put_datatypes (fold Symtab.update dt_infos dt_info) |>
     3.5        add_cases_induct dt_infos induct |>
     3.6        Theory.parent_path |>
     3.7 -      (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
     3.8 +      store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd |>
     3.9        DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos);
    3.10    in
    3.11      ({distinct = distinct,
    3.12 @@ -708,25 +708,25 @@
    3.13    let
    3.14      val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
    3.15  
    3.16 -    val (thy2, inject, distinct, dist_rewrites, simproc_dists, induct) = thy |>
    3.17 +    val ((inject, distinct, dist_rewrites, simproc_dists, induct), thy2) = thy |>
    3.18        DatatypeRepProofs.representation_proofs flat_names dt_info new_type_names descr sorts
    3.19          types_syntax constr_syntax case_names_induct;
    3.20  
    3.21 -    val (thy3, casedist_thms) = DatatypeAbsProofs.prove_casedist_thms new_type_names descr
    3.22 +    val (casedist_thms, thy3) = DatatypeAbsProofs.prove_casedist_thms new_type_names descr
    3.23        sorts induct case_names_exhausts thy2;
    3.24 -    val (thy4, (reccomb_names, rec_thms)) = DatatypeAbsProofs.prove_primrec_thms
    3.25 +    val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
    3.26        flat_names new_type_names descr sorts dt_info inject dist_rewrites dist_ss induct thy3;
    3.27 -    val (thy6, (case_thms, case_names)) = DatatypeAbsProofs.prove_case_thms
    3.28 +    val ((case_thms, case_names), thy6) = DatatypeAbsProofs.prove_case_thms
    3.29        flat_names new_type_names descr sorts reccomb_names rec_thms thy4;
    3.30 -    val (thy7, split_thms) = DatatypeAbsProofs.prove_split_thms new_type_names
    3.31 +    val (split_thms, thy7) = DatatypeAbsProofs.prove_split_thms new_type_names
    3.32        descr sorts inject dist_rewrites casedist_thms case_thms thy6;
    3.33 -    val (thy8, nchotomys) = DatatypeAbsProofs.prove_nchotomys new_type_names
    3.34 +    val (nchotomys, thy8) = DatatypeAbsProofs.prove_nchotomys new_type_names
    3.35        descr sorts casedist_thms thy7;
    3.36 -    val (thy9, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names
    3.37 +    val (case_congs, thy9) = DatatypeAbsProofs.prove_case_congs new_type_names
    3.38        descr sorts nchotomys case_thms thy8;
    3.39 -    val (thy10, weak_case_congs) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
    3.40 +    val (weak_case_congs, thy10) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
    3.41        descr sorts thy9;
    3.42 -    val (thy11, size_thms) = DatatypeAbsProofs.prove_size_thms flat_names new_type_names
    3.43 +    val (size_thms, thy11) = DatatypeAbsProofs.prove_size_thms flat_names new_type_names
    3.44        descr sorts reccomb_names rec_thms thy10;
    3.45  
    3.46      val dt_infos = map (make_dt_info (List.concat descr) induct reccomb_names rec_thms)
    3.47 @@ -743,7 +743,7 @@
    3.48        put_datatypes (fold Symtab.update dt_infos dt_info) |>
    3.49        add_cases_induct dt_infos induct |>
    3.50        Theory.parent_path |>
    3.51 -      (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
    3.52 +      store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd |>
    3.53        DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos);
    3.54    in
    3.55      ({distinct = distinct,
    3.56 @@ -810,32 +810,32 @@
    3.57  
    3.58      val _ = message ("Proofs for datatype(s) " ^ commas_quote new_type_names);
    3.59  
    3.60 -    val (thy2, casedist_thms) = thy1 |>
    3.61 +    val (casedist_thms, thy2) = thy1 |>
    3.62        DatatypeAbsProofs.prove_casedist_thms new_type_names [descr] sorts induction
    3.63          case_names_exhausts;
    3.64 -    val (thy3, (reccomb_names, rec_thms)) = DatatypeAbsProofs.prove_primrec_thms
    3.65 +    val ((reccomb_names, rec_thms), thy3) = DatatypeAbsProofs.prove_primrec_thms
    3.66        false new_type_names [descr] sorts dt_info inject distinct dist_ss induction thy2;
    3.67 -    val (thy4, (case_thms, case_names)) = DatatypeAbsProofs.prove_case_thms false
    3.68 +    val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms false
    3.69        new_type_names [descr] sorts reccomb_names rec_thms thy3;
    3.70 -    val (thy5, split_thms) = DatatypeAbsProofs.prove_split_thms
    3.71 +    val (split_thms, thy5) = DatatypeAbsProofs.prove_split_thms
    3.72        new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
    3.73 -    val (thy6, nchotomys) = DatatypeAbsProofs.prove_nchotomys new_type_names
    3.74 +    val (nchotomys, thy6) = DatatypeAbsProofs.prove_nchotomys new_type_names
    3.75        [descr] sorts casedist_thms thy5;
    3.76 -    val (thy7, case_congs) = DatatypeAbsProofs.prove_case_congs new_type_names
    3.77 +    val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
    3.78        [descr] sorts nchotomys case_thms thy6;
    3.79 -    val (thy8, weak_case_congs) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
    3.80 +    val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
    3.81        [descr] sorts thy7;
    3.82 -    val (thy9, size_thms) =
    3.83 +    val (size_thms, thy9) =
    3.84        if Context.exists_name "NatArith" thy8 then
    3.85          DatatypeAbsProofs.prove_size_thms false new_type_names
    3.86            [descr] sorts reccomb_names rec_thms thy8
    3.87 -      else (thy8, []);
    3.88 +      else ([], thy8);
    3.89  
    3.90 -    val (thy10, [induction']) = thy9 |>
    3.91 -      (#1 o store_thmss "inject" new_type_names inject) |>
    3.92 -      (#1 o store_thmss "distinct" new_type_names distinct) |>
    3.93 +    val ([induction'], thy10) = thy9 |>
    3.94 +      store_thmss "inject" new_type_names inject |> snd |>
    3.95 +      store_thmss "distinct" new_type_names distinct |> snd |>
    3.96        Theory.add_path (space_implode "_" new_type_names) |>
    3.97 -      PureThy.add_thms [(("induct", induction), [case_names_induct])];
    3.98 +      PureThy.add_thms [(("induct", induction), [case_names_induct])] |> Library.swap;
    3.99  
   3.100      val dt_infos = map (make_dt_info descr induction' reccomb_names rec_thms)
   3.101        ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
   3.102 @@ -850,7 +850,7 @@
   3.103        put_datatypes (fold Symtab.update dt_infos dt_info) |>
   3.104        add_cases_induct dt_infos induction' |>
   3.105        Theory.parent_path |>
   3.106 -      (#1 o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
   3.107 +      (snd o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
   3.108        DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos);
   3.109    in
   3.110      ({distinct = distinct,
     4.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Thu Dec 01 06:28:41 2005 +0100
     4.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Thu Dec 01 08:28:02 2005 +0100
     4.3 @@ -16,8 +16,8 @@
     4.4    val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
     4.5      string list -> DatatypeAux.descr list -> (string * sort) list ->
     4.6        (string * mixfix) list -> (string * mixfix) list list -> theory attribute
     4.7 -        -> theory -> theory * thm list list * thm list list * thm list list *
     4.8 -          DatatypeAux.simproc_dist list * thm
     4.9 +        -> theory -> (thm list list * thm list list * thm list list *
    4.10 +          DatatypeAux.simproc_dist list * thm) * theory
    4.11  end;
    4.12  
    4.13  structure DatatypeRepProofs : DATATYPE_REP_PROOFS =
    4.14 @@ -577,9 +577,11 @@
    4.15      val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
    4.16        ((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms);
    4.17  
    4.18 -    val (thy6, (constr_inject', distinct_thms'))= thy5 |> parent_path flat_names |>
    4.19 -      store_thmss "inject" new_type_names constr_inject |>>>
    4.20 -      store_thmss "distinct" new_type_names distinct_thms;
    4.21 +    val ((constr_inject', distinct_thms'), thy6) =
    4.22 +      thy5
    4.23 +      |> parent_path flat_names
    4.24 +      |> store_thmss "inject" new_type_names constr_inject
    4.25 +      ||>> store_thmss "distinct" new_type_names distinct_thms;
    4.26  
    4.27      (*************************** induction theorem ****************************)
    4.28  
    4.29 @@ -642,7 +644,8 @@
    4.30        PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
    4.31        Theory.parent_path;
    4.32  
    4.33 -  in (thy7, constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct')
    4.34 +  in
    4.35 +    ((constr_inject', distinct_thms', dist_rewrites, simproc_dists, dt_induct'), thy7)
    4.36    end;
    4.37  
    4.38  end;
     5.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Dec 01 06:28:41 2005 +0100
     5.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Dec 01 08:28:02 2005 +0100
     5.3 @@ -239,13 +239,19 @@
     5.4    if name = s then (true, (vs, s, mfx, (dname, [HOLogic.unitT], NoSyn) :: cs))
     5.5    else x;
     5.6  
     5.7 -fun add_dummies f dts used thy =
     5.8 -  apsnd (pair (map fst dts)) (f (map snd dts) thy)
     5.9 -  handle DatatypeAux.Datatype_Empty name' =>
    5.10 +fun add_dummies f [] _ thy =
    5.11 +      (([], NONE), thy)
    5.12 +  | add_dummies f dts used thy =
    5.13 +      thy
    5.14 +      |> f (map snd dts)
    5.15 +      |-> (fn dtinfo => pair ((map fst dts), SOME dtinfo))
    5.16 +    handle DatatypeAux.Datatype_Empty name' =>
    5.17        let
    5.18          val name = Sign.base_name name';
    5.19          val dname = variant used "Dummy"
    5.20 -      in add_dummies f (map (add_dummy name dname) dts) (dname :: used) thy
    5.21 +      in
    5.22 +        thy
    5.23 +        |> add_dummies f (map (add_dummy name dname) dts) (dname :: used)
    5.24        end;
    5.25  
    5.26  fun mk_realizer thy vs params ((rule, rrule), rt) =
    5.27 @@ -310,15 +316,14 @@
    5.28  
    5.29      (** datatype representing computational content of inductive set **)
    5.30  
    5.31 -    val (thy2, (dummies, dt_info)) =
    5.32 +    val ((dummies, dt_info), thy2) =
    5.33        thy1
    5.34 -      |> (if null dts
    5.35 -          then rpair ([], NONE)
    5.36 -          else add_dummies (DatatypePackage.add_datatype_i false false
    5.37 -            (map #2 dts)) (map (pair false) dts) [] #> (fn (v, (b, thy)) => (thy, (b, SOME v))))
    5.38 -      |>> Extraction.add_typeof_eqns_i ty_eqs
    5.39 -      |>> Extraction.add_realizes_eqns_i rlz_eqs;
    5.40 -    fun get f x = getOpt (Option.map f x, []);
    5.41 +      |> add_dummies
    5.42 +           (DatatypePackage.add_datatype_i false false (map #2 dts))
    5.43 +           (map (pair false) dts) []
    5.44 +      ||> Extraction.add_typeof_eqns_i ty_eqs
    5.45 +      ||> Extraction.add_realizes_eqns_i rlz_eqs;
    5.46 +    fun get f = (these oo Option.map) f;
    5.47      val rec_names = distinct (map (fst o dest_Const o head_of o fst o
    5.48        HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info));
    5.49      val (_, constrss) = foldl_map (fn ((recs, dummies), (s, rs)) =>