--- a/src/HOL/Tools/datatype_package.ML Fri Oct 28 09:35:04 2005 +0200
+++ b/src/HOL/Tools/datatype_package.ML Fri Oct 28 09:36:19 2005 +0200
@@ -18,7 +18,7 @@
include BASIC_DATATYPE_PACKAGE
val quiet_mode : bool ref
val add_datatype : bool -> string list -> (string list * bstring * mixfix *
- (bstring * string list * mixfix) list) list -> theory -> theory *
+ (bstring * string list * mixfix) list) list -> theory ->
{distinct : thm list list,
inject : thm list list,
exhaustion : thm list,
@@ -27,9 +27,9 @@
split_thms : (thm * thm) list,
induction : thm,
size : thm list,
- simps : thm list}
+ simps : thm list} * theory
val add_datatype_i : bool -> bool -> string list -> (string list * bstring * mixfix *
- (bstring * typ list * mixfix) list) list -> theory -> theory *
+ (bstring * typ list * mixfix) list) list -> theory ->
{distinct : thm list list,
inject : thm list list,
exhaustion : thm list,
@@ -38,10 +38,10 @@
split_thms : (thm * thm) list,
induction : thm,
size : thm list,
- simps : thm list}
+ simps : thm list} * theory
val rep_datatype_i : string list option -> (thm list * theory attribute list) list list ->
(thm list * theory attribute list) list list -> (thm list * theory attribute list) ->
- theory -> theory *
+ theory ->
{distinct : thm list list,
inject : thm list list,
exhaustion : thm list,
@@ -50,9 +50,9 @@
split_thms : (thm * thm) list,
induction : thm,
size : thm list,
- simps : thm list}
+ simps : thm list} * theory
val rep_datatype : string list option -> (thmref * Attrib.src list) list list ->
- (thmref * Attrib.src list) list list -> thmref * Attrib.src list -> theory -> theory *
+ (thmref * Attrib.src list) list list -> thmref * Attrib.src list -> theory ->
{distinct : thm list list,
inject : thm list list,
exhaustion : thm list,
@@ -61,7 +61,7 @@
split_thms : (thm * thm) list,
induction : thm,
size : thm list,
- simps : thm list}
+ simps : thm list} * theory
val get_datatypes : theory -> DatatypeAux.datatype_info Symtab.table
val print_datatypes : theory -> unit
val datatype_info : theory -> string -> DatatypeAux.datatype_info option
@@ -377,6 +377,8 @@
(**** translation rules for case ****)
+fun find_first f = Library.find_first f;
+
fun case_tr sg [t, u] =
let
fun case_error s name ts = raise TERM ("Error in case expression" ^
@@ -687,8 +689,7 @@
(#1 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
- (thy12,
- {distinct = distinct,
+ ({distinct = distinct,
inject = inject,
exhaustion = exhaustion,
rec_thms = rec_thms,
@@ -696,7 +697,7 @@
split_thms = split_thms,
induction = induct,
size = size_thms,
- simps = simps})
+ simps = simps}, thy12)
end;
@@ -745,8 +746,7 @@
(#1 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
- (thy12,
- {distinct = distinct,
+ ({distinct = distinct,
inject = inject,
exhaustion = casedist_thms,
rec_thms = rec_thms,
@@ -754,7 +754,7 @@
split_thms = split_thms,
induction = induct,
size = size_thms,
- simps = simps})
+ simps = simps}, thy12)
end;
@@ -853,8 +853,7 @@
(#1 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
- (thy11,
- {distinct = distinct,
+ ({distinct = distinct,
inject = inject,
exhaustion = casedist_thms,
rec_thms = rec_thms,
@@ -862,7 +861,7 @@
split_thms = split_thms,
induction = induction',
size = size_thms,
- simps = simps})
+ simps = simps}, thy11)
end;
val rep_datatype = gen_rep_datatype IsarThy.apply_theorems;
@@ -968,7 +967,7 @@
val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
val specs = map (fn ((((_, vs), t), mx), cons) =>
(vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
- in #1 o add_datatype false names specs end;
+ in snd o add_datatype false names specs end;
val datatypeP =
OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
@@ -981,7 +980,7 @@
Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 P.xthms1)) [[]] --
(P.$$$ "induction" |-- P.!!! P.xthm);
-fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #1 o rep_datatype opt_ts dss iss ind;
+fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #2 o rep_datatype opt_ts dss iss ind;
val rep_datatypeP =
OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_decl
--- a/src/HOL/Tools/inductive_realizer.ML Fri Oct 28 09:35:04 2005 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML Fri Oct 28 09:36:19 2005 +0200
@@ -195,6 +195,8 @@
in fun_of args' [] (rev args) used (Logic.strip_imp_prems rule') end;
+fun find_first f = Library.find_first f;
+
fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies =
let
val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct));
@@ -308,12 +310,14 @@
(** datatype representing computational content of inductive set **)
- val (thy2, (dummies, dt_info)) = thy1 |>
- (if null dts then rpair ([], NONE) else
- apsnd (apsnd SOME) o 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;
+ val (thy2, (dummies, dt_info)) =
+ 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, []);
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));