adapted to new PureThy.add_thms etc.;
authorwenzelm
Mon Mar 13 13:24:12 2000 +0100 (2000-03-13)
changeset 84368a87fa482baf
parent 8435 51a040fd2200
child 8437 258281c43dea
adapted to new PureThy.add_thms etc.;
proper handling of case names;
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_rep_proofs.ML
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Mon Mar 13 13:22:31 2000 +0100
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Mon Mar 13 13:24:12 2000 +0100
     1.3 @@ -20,14 +20,14 @@
     1.4  sig
     1.5    val prove_casedist_thms : string list -> (int * (string * DatatypeAux.dtyp list *
     1.6      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
     1.7 -      thm -> theory -> theory * thm list
     1.8 +      thm -> theory attribute list -> theory -> theory * thm list
     1.9    val prove_primrec_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
    1.10      (string * DatatypeAux.dtyp list) list)) list 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    val prove_case_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
    1.14      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    1.15 -      string list -> thm list -> theory -> theory * string list * thm list list
    1.16 +      string list -> thm list -> theory -> theory * (thm list list * string list)
    1.17    val prove_split_thms : string list -> (int * (string * DatatypeAux.dtyp list *
    1.18      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    1.19        thm list list -> thm list list -> thm list -> thm list list -> theory ->
    1.20 @@ -43,7 +43,7 @@
    1.21        thm list -> thm list list -> theory -> theory * thm list
    1.22  end;
    1.23  
    1.24 -structure DatatypeAbsProofs : DATATYPE_ABS_PROOFS =
    1.25 +structure DatatypeAbsProofs: DATATYPE_ABS_PROOFS =
    1.26  struct
    1.27  
    1.28  open DatatypeAux;
    1.29 @@ -54,7 +54,7 @@
    1.30  
    1.31  (************************ case distinction theorems ***************************)
    1.32  
    1.33 -fun prove_casedist_thms new_type_names descr sorts induct thy =
    1.34 +fun prove_casedist_thms new_type_names descr sorts induct case_names_exhausts thy =
    1.35    let
    1.36      val _ = message "Proving case distinction theorems ...";
    1.37  
    1.38 @@ -85,10 +85,8 @@
    1.39  
    1.40      val casedist_thms = map prove_casedist_thm ((0 upto (length newTs - 1)) ~~
    1.41        (DatatypeProp.make_casedists descr sorts) ~~ newTs)
    1.42 +  in thy |> store_thms_atts "exhaust" new_type_names (map single case_names_exhausts) casedist_thms end;
    1.43  
    1.44 -  in
    1.45 -    (store_thms "exhaust" new_type_names casedist_thms thy, casedist_thms)
    1.46 -  end;
    1.47  
    1.48  (*************************** primrec combinators ******************************)
    1.49  
    1.50 @@ -256,7 +254,7 @@
    1.51        (Const (name, reccomb_fn_Ts @ [T] ---> T'), rec_fns))
    1.52          (reccomb_names ~~ recTs ~~ rec_result_Ts);
    1.53  
    1.54 -    val thy2 = thy1 |>
    1.55 +    val (thy2, reccomb_defs) = thy1 |>
    1.56        Theory.add_consts_i (map (fn ((name, T), T') =>
    1.57          (Sign.base_name name, reccomb_fn_Ts @ [T] ---> T', NoSyn))
    1.58            (reccomb_names ~~ recTs ~~ rec_result_Ts)) |>
    1.59 @@ -264,10 +262,9 @@
    1.60          ((Sign.base_name name) ^ "_def", Logic.mk_equals (comb, absfree ("x", T,
    1.61             Const ("Eps", (T' --> HOLogic.boolT) --> T') $ absfree ("y", T',
    1.62               HOLogic.mk_mem (HOLogic.mk_prod (Free ("x", T), Free ("y", T')), set))))))
    1.63 -               (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) |>
    1.64 +               (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts)) |>>
    1.65        parent_path flat_names;
    1.66  
    1.67 -    val reccomb_defs = map ((get_def thy2) o Sign.base_name) reccomb_names;
    1.68  
    1.69      (* prove characteristic equations for primrec combinators *)
    1.70  
    1.71 @@ -284,7 +281,7 @@
    1.72  
    1.73    in
    1.74      (thy2 |> Theory.add_path (space_implode "_" new_type_names) |>
    1.75 -             PureThy.add_thmss [(("recs", rec_thms), [])] |>
    1.76 +             (#1 o PureThy.add_thmss [(("recs", rec_thms), [])]) |>
    1.77               Theory.parent_path,
    1.78       reccomb_names, rec_thms)
    1.79    end;
    1.80 @@ -342,10 +339,10 @@
    1.81              Logic.mk_equals (list_comb (Const (name, caseT), fns1),
    1.82                list_comb (reccomb, (flat (take (i, case_dummy_fns))) @
    1.83                  fns2 @ (flat (drop (i + 1, case_dummy_fns))) )));
    1.84 -          val thy' = thy |>
    1.85 +          val (thy', [def_thm]) = thy |>
    1.86              Theory.add_consts_i [decl] |> (PureThy.add_defs_i o map Thm.no_attributes) [def];
    1.87  
    1.88 -        in (defs @ [get_def thy' (Sign.base_name name)], thy')
    1.89 +        in (defs @ [def_thm], thy')
    1.90          end) (([], thy1), (hd descr) ~~ newTs ~~ case_names ~~
    1.91            (take (length newTs, reccomb_names)));
    1.92  
    1.93 @@ -358,9 +355,7 @@
    1.94        (DatatypeProp.make_case_trrules new_type_names descr) |>
    1.95        parent_path flat_names;
    1.96  
    1.97 -  in
    1.98 -    (store_thmss "cases" new_type_names case_thms thy3, case_names, case_thms)
    1.99 -  end;
   1.100 +  in thy3 |> store_thmss "cases" new_type_names case_thms |> apsnd (rpair case_names) end;
   1.101  
   1.102  
   1.103  (******************************* case splitting *******************************)
   1.104 @@ -395,9 +390,8 @@
   1.105      val (split_thms, split_asm_thms) = ListPair.unzip split_thm_pairs
   1.106  
   1.107    in
   1.108 -    (thy |> store_thms "split" new_type_names split_thms |>
   1.109 -            store_thms "split_asm" new_type_names split_asm_thms,
   1.110 -     split_thm_pairs)
   1.111 +    thy |> store_thms "split" new_type_names split_thms |>>>
   1.112 +      store_thms "split_asm" new_type_names split_asm_thms |> apsnd ListPair.zip
   1.113    end;
   1.114  
   1.115  (******************************* size functions *******************************)
   1.116 @@ -442,17 +436,16 @@
   1.117      val fs = flat (map (fn (_, (_, _, constrs)) => map make_sizefun constrs) descr');
   1.118      val fTs = map fastype_of fs;
   1.119  
   1.120 -    val thy' = thy1 |>
   1.121 +    val (thy', size_def_thms) = thy1 |>
   1.122        Theory.add_consts_i (map (fn (s, T) =>
   1.123          (Sign.base_name s, T --> HOLogic.natT, NoSyn))
   1.124            (drop (length (hd descr), size_names ~~ recTs))) |>
   1.125        (PureThy.add_defs_i o map Thm.no_attributes) (map (fn (((s, T), def_name), rec_name) =>
   1.126          (def_name, Logic.mk_equals (Const (s, T --> HOLogic.natT),
   1.127            list_comb (Const (rec_name, fTs @ [T] ---> HOLogic.natT), fs))))
   1.128 -            (size_names ~~ recTs ~~ def_names ~~ reccomb_names)) |>
   1.129 +            (size_names ~~ recTs ~~ def_names ~~ reccomb_names)) |>>
   1.130        parent_path flat_names;
   1.131  
   1.132 -    val size_def_thms = map (get_thm thy') def_names;
   1.133      val rewrites = size_def_thms @ map mk_meta_eq primrec_thms;
   1.134  
   1.135      val size_thms = map (fn t => prove_goalw_cterm rewrites
   1.136 @@ -461,7 +454,7 @@
   1.137  
   1.138    in
   1.139      (thy' |> Theory.add_path big_name |>
   1.140 -             PureThy.add_thmss [(("size", size_thms), [])] |>
   1.141 +             (#1 o PureThy.add_thmss [(("size", size_thms), [])]) |>
   1.142               Theory.parent_path,
   1.143       size_thms)
   1.144    end;
   1.145 @@ -488,9 +481,7 @@
   1.146      val nchotomys =
   1.147        map prove_nchotomy (DatatypeProp.make_nchotomys descr sorts ~~ casedist_thms)
   1.148  
   1.149 -  in
   1.150 -    (store_thms "nchotomy" new_type_names nchotomys thy, nchotomys)
   1.151 -  end;
   1.152 +  in thy |> store_thms "nchotomy" new_type_names nchotomys end;
   1.153  
   1.154  fun prove_case_congs new_type_names descr sorts nchotomys case_thms thy =
   1.155    let
   1.156 @@ -515,8 +506,6 @@
   1.157      val case_congs = map prove_case_cong (DatatypeProp.make_case_congs
   1.158        new_type_names descr sorts thy ~~ nchotomys ~~ case_thms)
   1.159  
   1.160 -  in
   1.161 -    (store_thms "case_cong" new_type_names case_congs thy, case_congs)
   1.162 -  end;
   1.163 +  in thy |> store_thms "case_cong" new_type_names case_congs end;
   1.164  
   1.165  end;
     2.1 --- a/src/HOL/Tools/datatype_rep_proofs.ML	Mon Mar 13 13:22:31 2000 +0100
     2.2 +++ b/src/HOL/Tools/datatype_rep_proofs.ML	Mon Mar 13 13:24:12 2000 +0100
     2.3 @@ -17,8 +17,8 @@
     2.4    val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
     2.5      string list -> (int * (string * DatatypeAux.dtyp list *
     2.6        (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
     2.7 -        (string * mixfix) list -> (string * mixfix) list list -> theory ->
     2.8 -          theory * thm list list * thm list list * thm list list *
     2.9 +        (string * mixfix) list -> (string * mixfix) list list -> theory attribute
    2.10 +          -> theory -> theory * thm list list * thm list list * thm list list *
    2.11              DatatypeAux.simproc_dist list * thm
    2.12  end;
    2.13  
    2.14 @@ -42,7 +42,7 @@
    2.15  (******************************************************************************)
    2.16  
    2.17  fun representation_proofs flat_names (dt_info : datatype_info Symtab.table)
    2.18 -      new_type_names descr sorts types_syntax constr_syntax thy =
    2.19 +      new_type_names descr sorts types_syntax constr_syntax case_names_induct thy =
    2.20    let
    2.21      val Datatype_thy = theory "Datatype";
    2.22      val node_name = Sign.intern_tycon (Theory.sign_of Datatype_thy) "node";
    2.23 @@ -231,12 +231,11 @@
    2.24          val def_name = (Sign.base_name cname) ^ "_def";
    2.25          val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
    2.26            (Const (rep_name, T --> Univ_elT) $ lhs, rhs));
    2.27 -        val thy' = thy |>
    2.28 +        val (thy', [def_thm]) = thy |>
    2.29            Theory.add_consts_i [(cname', constrT, mx)] |>
    2.30            (PureThy.add_defs_i o map Thm.no_attributes) [(def_name, def)];
    2.31  
    2.32 -      in (thy', defs @ [get_thm thy' def_name], eqns @ [eqn], i + 1)
    2.33 -      end;
    2.34 +      in (thy', defs @ [def_thm], eqns @ [eqn], i + 1) end;
    2.35  
    2.36      (* constructor definitions for datatype *)
    2.37  
    2.38 @@ -382,8 +381,7 @@
    2.39          val defs = map (fn (rec_name, (T, iso_name)) => ((Sign.base_name iso_name) ^ "_def",
    2.40            equals (T --> Univ_elT) $ Const (iso_name, T --> Univ_elT) $
    2.41              list_comb (Const (rec_name, fTs @ [T] ---> Univ_elT), fs))) (rec_names ~~ isos);
    2.42 -        val thy' = (PureThy.add_defs_i o map Thm.no_attributes) defs thy;
    2.43 -        val def_thms = map (get_thm thy') (map fst defs);
    2.44 +        val (thy', def_thms) = (PureThy.add_defs_i o map Thm.no_attributes) defs thy;
    2.45  
    2.46          (* prove characteristic equations *)
    2.47  
    2.48 @@ -580,8 +578,8 @@
    2.49        ((DatatypeProp.make_injs descr sorts) ~~ constr_rep_thms);
    2.50  
    2.51      val thy6 = thy5 |> parent_path flat_names |>
    2.52 -      store_thmss "inject" new_type_names constr_inject |>
    2.53 -      store_thmss "distinct" new_type_names distinct_thms;
    2.54 +      (#1 o store_thmss "inject" new_type_names constr_inject) |>
    2.55 +      (#1 o store_thmss "distinct" new_type_names distinct_thms);
    2.56  
    2.57      (*************************** induction theorem ****************************)
    2.58  
    2.59 @@ -638,12 +636,12 @@
    2.60                rtac allI 1, dtac FunsD 1, etac CollectD 1]))]))
    2.61                  (prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
    2.62  
    2.63 -    val thy7 = thy6 |>
    2.64 +    val (thy7, [dt_induct']) = thy6 |>
    2.65        Theory.add_path big_name |>
    2.66 -      PureThy.add_thms [(("induct", dt_induct), [])] |>
    2.67 +      PureThy.add_thms [(("induct", dt_induct), [case_names_induct])] |>>
    2.68        Theory.parent_path;
    2.69  
    2.70 -  in (thy7, constr_inject, distinct_thms, dist_rewrites, simproc_dists, dt_induct)
    2.71 +  in (thy7, constr_inject, distinct_thms, dist_rewrites, simproc_dists, dt_induct')
    2.72    end;
    2.73  
    2.74  end;