src/HOL/Tools/datatype_abs_proofs.ML
changeset 8477 17231d71171a
parent 8436 8a87fa482baf
child 8601 8fb3a81b4ccf
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Wed Mar 15 18:52:07 2000 +0100
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Wed Mar 15 23:36:46 2000 +0100
     1.3 @@ -24,7 +24,7 @@
     1.4    val prove_primrec_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
     1.5      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
     1.6        DatatypeAux.datatype_info Symtab.table -> thm list list -> thm list list ->
     1.7 -        simpset -> thm -> theory -> theory * string list * thm list
     1.8 +        simpset -> thm -> theory -> theory * (string list * thm list)
     1.9    val prove_case_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
    1.10      (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
    1.11        string list -> thm list -> theory -> theory * (thm list list * string list)
    1.12 @@ -62,13 +62,14 @@
    1.13      val recTs = get_rec_types descr' sorts;
    1.14      val newTs = take (length (hd descr), recTs);
    1.15  
    1.16 +    val {maxidx, ...} = rep_thm induct;
    1.17      val induct_Ps = map head_of (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of induct)));
    1.18  
    1.19      fun prove_casedist_thm ((i, t), T) =
    1.20        let
    1.21          val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) =>
    1.22            Abs ("z", T', Const ("True", T''))) induct_Ps;
    1.23 -        val P = Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", 0), T), Bound 0) $
    1.24 +        val P = Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx+1), T), Bound 0) $
    1.25            Var (("P", 0), HOLogic.boolT))
    1.26          val insts = take (i, dummyPs) @ (P::(drop (i + 1, dummyPs)));
    1.27          val cert = cterm_of (Theory.sign_of thy);
    1.28 @@ -280,12 +281,12 @@
    1.29             (DatatypeProp.make_primrecs new_type_names descr sorts thy2)
    1.30  
    1.31    in
    1.32 -    (thy2 |> Theory.add_path (space_implode "_" new_type_names) |>
    1.33 -             (#1 o PureThy.add_thmss [(("recs", rec_thms), [])]) |>
    1.34 -             Theory.parent_path,
    1.35 -     reccomb_names, rec_thms)
    1.36 +    thy2 |> Theory.add_path (space_implode "_" new_type_names) |>
    1.37 +    PureThy.add_thmss [(("recs", rec_thms), [])] |>>
    1.38 +    Theory.parent_path |> apsnd (pair reccomb_names o flat)
    1.39    end;
    1.40  
    1.41 +
    1.42  (***************************** case combinators *******************************)
    1.43  
    1.44  fun prove_case_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
    1.45 @@ -349,13 +350,15 @@
    1.46      val case_thms = map (map (fn t => prove_goalw_cterm (case_defs @
    1.47        (map mk_meta_eq primrec_thms)) (cterm_of (Theory.sign_of thy2) t)
    1.48          (fn _ => [rtac refl 1])))
    1.49 -          (DatatypeProp.make_cases new_type_names descr sorts thy2);
    1.50 +          (DatatypeProp.make_cases new_type_names descr sorts thy2)
    1.51  
    1.52 -    val thy3 = thy2 |> Theory.add_trrules_i
    1.53 +  in
    1.54 +    thy2 |> Theory.add_trrules_i
    1.55        (DatatypeProp.make_case_trrules new_type_names descr) |>
    1.56 -      parent_path flat_names;
    1.57 -
    1.58 -  in thy3 |> store_thmss "cases" new_type_names case_thms |> apsnd (rpair case_names) end;
    1.59 +    parent_path flat_names |>
    1.60 +    store_thmss "cases" new_type_names case_thms |>
    1.61 +    apsnd (rpair case_names)
    1.62 +  end;
    1.63  
    1.64  
    1.65  (******************************* case splitting *******************************)
    1.66 @@ -453,12 +456,12 @@
    1.67          (DatatypeProp.make_size new_type_names descr sorts thy')
    1.68  
    1.69    in
    1.70 -    (thy' |> Theory.add_path big_name |>
    1.71 -             (#1 o PureThy.add_thmss [(("size", size_thms), [])]) |>
    1.72 -             Theory.parent_path,
    1.73 -     size_thms)
    1.74 +    thy' |> Theory.add_path big_name |>
    1.75 +    PureThy.add_thmss [(("size", size_thms), [])] |>>
    1.76 +    Theory.parent_path |> apsnd flat
    1.77    end;
    1.78  
    1.79 +
    1.80  (************************* additional theorems for TFL ************************)
    1.81  
    1.82  fun prove_nchotomys new_type_names descr sorts casedist_thms thy =