Reimplemented parts of datatype package dealing with datatypes involving
function types. Now also supports functions with more than one argument.
--- a/src/HOL/Tools/datatype_abs_proofs.ML Thu Oct 10 14:23:47 2002 +0200
+++ b/src/HOL/Tools/datatype_abs_proofs.ML Thu Oct 10 14:26:50 2002 +0200
@@ -18,31 +18,29 @@
signature DATATYPE_ABS_PROOFS =
sig
- val prove_casedist_thms : string list -> (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
- thm -> theory attribute list -> theory -> theory * thm list
- val prove_primrec_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+ val prove_casedist_thms : string list ->
+ DatatypeAux.descr list -> (string * sort) list -> thm ->
+ theory attribute list -> theory -> theory * thm list
+ 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)
- val prove_case_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+ val prove_case_thms : bool -> string list ->
+ DatatypeAux.descr list -> (string * sort) list ->
string list -> thm list -> theory -> theory * (thm list list * string list)
- val prove_split_thms : string list -> (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+ 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
- val prove_size_thms : bool -> string list -> (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+ val prove_size_thms : bool -> string list ->
+ DatatypeAux.descr list -> (string * sort) list ->
string list -> thm list -> theory -> theory * thm list
- val prove_nchotomys : string list -> (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
- thm list -> theory -> theory * thm list
- val prove_weak_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
- theory -> theory * thm list
- val prove_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
+ val prove_nchotomys : string list -> DatatypeAux.descr list ->
+ (string * sort) list -> thm list -> theory -> theory * thm list
+ val prove_weak_case_congs : string list -> DatatypeAux.descr list ->
+ (string * sort) list -> theory -> theory * thm list
+ val prove_case_congs : string list ->
+ DatatypeAux.descr list -> (string * sort) list ->
thm list -> thm list list -> theory -> theory * thm list
end;
@@ -51,10 +49,6 @@
open DatatypeAux;
-val thin = read_instantiate_sg (Theory.sign_of Set.thy) [("V", "?X : ?Y")] thin_rl;
-
-val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma);
-
(************************ case distinction theorems ***************************)
fun prove_casedist_thms new_type_names descr sorts induct case_names_exhausts thy =
@@ -99,8 +93,6 @@
let
val _ = message "Constructing primrec combinators ...";
- val fun_rel_comp_name = "Relation.fun_rel_comp";
-
val big_name = space_implode "_" new_type_names;
val thy0 = add_path flat_names big_name thy;
@@ -126,9 +118,8 @@
val Ts = map (typ_of_dtyp descr' sorts) cargs;
val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
- fun mk_argT (DtRec k, _) = nth_elem (k, rec_result_Ts)
- | mk_argT (DtType ("fun", [_, DtRec k]), Type ("fun", [T, _])) =
- T --> nth_elem (k, rec_result_Ts);
+ fun mk_argT (dt, T) =
+ binder_types T ---> nth_elem (body_index dt, rec_result_Ts);
val argTs = Ts @ map mk_argT recs
in argTs ---> nth_elem (i, rec_result_Ts)
@@ -148,20 +139,17 @@
let
fun mk_prem ((dt, U), (j, k, prems, t1s, t2s)) =
let val free1 = mk_Free "x" U j
- in (case (dt, U) of
- (DtRec m, _) =>
- let val free2 = mk_Free "y" (nth_elem (m, rec_result_Ts)) k
- in (j + 1, k + 1, (HOLogic.mk_Trueprop (HOLogic.mk_mem
- (HOLogic.mk_prod (free1, free2), nth_elem (m, rec_sets))))::prems,
+ in (case (strip_dtyp dt, strip_type U) of
+ ((_, DtRec m), (Us, _)) =>
+ let
+ val free2 = mk_Free "y" (Us ---> nth_elem (m, rec_result_Ts)) k;
+ val i = length Us
+ in (j + 1, k + 1, HOLogic.mk_Trueprop (HOLogic.list_all
+ (map (pair "x") Us, HOLogic.mk_mem (HOLogic.mk_prod
+ (app_bnds free1 i, app_bnds free2 i),
+ nth_elem (m, rec_sets)))) :: prems,
free1::t1s, free2::t2s)
end
- | (DtType ("fun", [_, DtRec m]), U' as Type ("fun", [T', _])) =>
- let val free2 = mk_Free "y" (T' --> nth_elem (m, rec_result_Ts)) k
- in (j + 1, k + 1, (HOLogic.mk_Trueprop (HOLogic.mk_mem (free2,
- Const (fun_rel_comp_name, [U', snd (strip_type (nth_elem (m, rec_set_Ts)))] --->
- HOLogic.mk_setT (T' --> nth_elem (m, rec_result_Ts))) $
- free1 $ nth_elem (m, rec_sets))))::prems, free1::t1s, free2::t2s)
- end
| _ => (j + 1, k, prems, free1::t1s, t2s))
end;
@@ -180,7 +168,7 @@
val (thy1, {intrs = rec_intrs, elims = rec_elims, ...}) =
setmp InductivePackage.quiet_mode (!quiet_mode)
(InductivePackage.add_inductive_i false true big_rec_name' false false true
- rec_sets (map (fn x => (("", x), [])) rec_intr_ts) [fun_rel_comp_mono]) thy0;
+ rec_sets (map (fn x => (("", x), [])) rec_intr_ts) []) thy0;
(* prove uniqueness and termination of primrec combinators *)
@@ -202,16 +190,14 @@
val k = length (filter is_rec_type cargs)
in (EVERY [DETERM tac,
- REPEAT (dtac fun_rel_comp_unique 1),
REPEAT (etac ex1E 1), rtac ex1I 1,
DEPTH_SOLVE_1 (ares_tac [intr] 1),
- REPEAT_DETERM_N k (etac thin 1),
+ REPEAT_DETERM_N k (etac thin_rl 1 THEN rotate_tac 1 1),
etac elim 1,
REPEAT_DETERM_N j distinct_tac,
etac Pair_inject 1, TRY (dresolve_tac inject 1),
REPEAT (etac conjE 1), hyp_subst_tac 1,
- REPEAT (etac allE 1),
- REPEAT (dtac mp 1 THEN atac 1),
+ REPEAT (EVERY [etac allE 1, dtac mp 1, atac 1]),
TRY (hyp_subst_tac 1),
rtac refl 1,
REPEAT_DETERM_N (n - j - 1) distinct_tac],
@@ -236,7 +222,8 @@
val induct' = cterm_instantiate ((map cert induct_Ps) ~~
(map cert insts)) induct;
val (tac, _) = foldl mk_unique_tac
- (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_tac) 1, rec_intrs),
+ (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_tac) 1
+ THEN rewtac (mk_meta_eq choice_eq), rec_intrs),
descr' ~~ rec_elims ~~ recTs ~~ rec_result_Ts);
in split_conj_thm (prove_goalw_cterm []
@@ -277,8 +264,7 @@
[rtac the1_equality 1,
resolve_tac rec_unique_thms 1,
resolve_tac rec_intrs 1,
- rewrite_goals_tac [o_def, fun_rel_comp_def],
- REPEAT ((rtac CollectI 1 THEN rtac allI 1) ORELSE resolve_tac rec_total_thms 1)]))
+ REPEAT (rtac allI 1 ORELSE resolve_tac rec_total_thms 1)]))
(DatatypeProp.make_primrecs new_type_names descr sorts thy2)
in
@@ -302,8 +288,7 @@
val newTs = take (length (hd descr), recTs);
val T' = TFree (variant used "'t", HOLogic.typeS);
- fun mk_dummyT (DtRec _) = T'
- | mk_dummyT (DtType ("fun", [T, _])) = typ_of_dtyp descr' sorts T --> T'
+ fun mk_dummyT dt = binder_types (typ_of_dtyp descr' sorts dt) ---> T';
val case_dummy_fns = map (fn (_, (_, _, constrs)) => map (fn (_, cargs) =>
let
@@ -401,8 +386,9 @@
(******************************* size functions *******************************)
fun prove_size_thms flat_names new_type_names descr sorts reccomb_names primrec_thms thy =
- if exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists
- (fn (DtType ("fun", [_, DtRec _])) => true | _ => false) cargs) constrs) (flat descr)
+ if exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
+ is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs)
+ (flat descr)
then
(thy, [])
else
--- a/src/HOL/Tools/datatype_aux.ML Thu Oct 10 14:23:47 2002 +0200
+++ b/src/HOL/Tools/datatype_aux.ML Thu Oct 10 14:26:50 2002 +0200
@@ -25,6 +25,9 @@
val mk_conj : term list -> term
val mk_disj : term list -> term
+ val app_bnds : term -> int -> term
+
+ val cong_tac : int -> tactic
val indtac : thm -> int -> tactic
val exh_tac : (string -> thm) -> int -> tactic
@@ -44,25 +47,21 @@
val dtyp_of_typ : (string * string list) list -> typ -> dtyp
val mk_Free : string -> typ -> int -> term
val is_rec_type : dtyp -> bool
- val typ_of_dtyp : (int * (string * dtyp list *
- (string * dtyp list) list)) list -> (string * sort) list -> dtyp -> typ
+ val typ_of_dtyp : descr -> (string * sort) list -> dtyp -> typ
val dest_DtTFree : dtyp -> string
val dest_DtRec : dtyp -> int
+ val strip_dtyp : dtyp -> dtyp list * dtyp
+ val body_index : dtyp -> int
+ val mk_fun_dtyp : dtyp list -> dtyp -> dtyp
val dest_TFree : typ -> string
- val get_nonrec_types : (int * (string * dtyp list *
- (string * dtyp list) list)) list -> (string * sort) list -> typ list
- val get_branching_types : (int * (string * dtyp list *
- (string * dtyp list) list)) list -> (string * sort) list -> typ list
- val get_rec_types : (int * (string * dtyp list *
- (string * dtyp list) list)) list -> (string * sort) list -> typ list
- val check_nonempty : (int * (string * dtyp list *
- (string * dtyp list) list)) list list -> unit
+ val get_nonrec_types : descr -> (string * sort) list -> typ list
+ val get_branching_types : descr -> (string * sort) list -> typ list
+ val get_arities : descr -> int list
+ val get_rec_types : descr -> (string * sort) list -> typ list
+ val check_nonempty : descr list -> unit
val unfold_datatypes :
- Sign.sg -> (int * (string * dtyp list * (string * dtyp list) list)) list ->
- (string * sort) list -> datatype_info Symtab.table ->
- (int * (string * dtyp list * (string * dtyp list) list)) list -> int ->
- (int * (string * dtyp list *
- (string * dtyp list) list)) list list * int
+ Sign.sg -> descr -> (string * sort) list -> datatype_info Symtab.table ->
+ descr -> int -> descr list * int
end;
structure DatatypeAux : DATATYPE_AUX =
@@ -105,6 +104,23 @@
val mk_conj = foldr1 (HOLogic.mk_binop "op &");
val mk_disj = foldr1 (HOLogic.mk_binop "op |");
+fun app_bnds t i = list_comb (t, map Bound (i - 1 downto 0));
+
+
+fun cong_tac i st = (case Logic.strip_assums_concl
+ (nth_elem (i - 1, prems_of st)) of
+ _ $ (_ $ (f $ x) $ (g $ y)) =>
+ let
+ val cong' = lift_rule (st, i) cong;
+ val _ $ (_ $ (f' $ x') $ (g' $ y')) =
+ Logic.strip_assums_concl (prop_of cong');
+ val insts = map (pairself (cterm_of (#sign (rep_thm st))) o
+ apsnd (curry list_abs (Logic.strip_params (concl_of cong'))) o
+ apfst head_of) [(f', f), (g', g), (x', x), (y', y)]
+ in compose_tac (false, cterm_instantiate insts cong', 2) i st
+ handle THM _ => no_tac st
+ end
+ | _ => no_tac st);
(* instantiate induction rule *)
@@ -198,6 +214,14 @@
| is_rec_type (DtRec _) = true
| is_rec_type _ = false;
+fun strip_dtyp (DtType ("fun", [T, U])) = apfst (cons T) (strip_dtyp U)
+ | strip_dtyp T = ([], T);
+
+val body_index = dest_DtRec o snd o strip_dtyp;
+
+fun mk_fun_dtyp [] U = U
+ | mk_fun_dtyp (T :: Ts) U = DtType ("fun", [T, mk_fun_dtyp Ts U]);
+
fun dest_TFree (TFree (n, _)) = n;
fun name_of_typ (Type (s, Ts)) = space_implode "_"
@@ -223,14 +247,9 @@
(* find all non-recursive types in datatype description *)
fun get_nonrec_types descr sorts =
- let fun add (Ts, T as DtTFree _) = T ins Ts
- | add (Ts, T as DtType ("fun", [_, DtRec _])) = Ts
- | add (Ts, T as DtType _) = T ins Ts
- | add (Ts, _) = Ts
- in map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
+ map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
foldl (fn (Ts', (_, cargs)) =>
- foldl add (Ts', cargs)) (Ts, constrs)) ([], descr))
- end;
+ filter_out is_rec_type cargs union Ts') (Ts, constrs)) ([], descr));
(* get all recursive types in datatype description *)
@@ -239,13 +258,14 @@
(* get all branching types *)
-fun get_branching_types descr sorts =
- let fun add (Ts, DtType ("fun", [T, DtRec _])) = T ins Ts
- | add (Ts, _) = Ts
- in map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
- foldl (fn (Ts', (_, cargs)) =>
- foldl add (Ts', cargs)) (Ts, constrs)) ([], descr))
- end;
+fun get_branching_types descr sorts =
+ map (typ_of_dtyp descr sorts) (foldl (fn (Ts, (_, (_, _, constrs))) =>
+ foldl (fn (Ts', (_, cargs)) => foldr op union (map (fst o strip_dtyp)
+ cargs, Ts')) (Ts, constrs)) ([], descr));
+
+fun get_arities descr = foldl (fn (is, (_, (_, _, constrs))) =>
+ foldl (fn (is', (_, cargs)) => map (length o fst o strip_dtyp)
+ (filter is_rec_type cargs) union is') (is, constrs)) ([], descr);
(* nonemptiness check for datatypes *)
@@ -255,11 +275,10 @@
fun is_nonempty_dt is i =
let
val (_, _, constrs) = the (assoc (descr', i));
- fun arg_nonempty (DtRec i) = if i mem is then false
+ fun arg_nonempty (_, DtRec i) = if i mem is then false
else is_nonempty_dt (i::is) i
- | arg_nonempty (DtType ("fun", [_, T])) = arg_nonempty T
| arg_nonempty _ = true;
- in exists ((forall arg_nonempty) o snd) constrs
+ in exists ((forall (arg_nonempty o strip_dtyp)) o snd) constrs
end
in assert_all (fn (i, _) => is_nonempty_dt [i] i) (hd descr)
(fn (_, (s, _, _)) => "Nonemptiness check failed for datatype " ^ s)
@@ -290,22 +309,21 @@
(* unfold a single constructor argument *)
- fun unfold_arg ((i, Ts, descrs), T as (DtType (tname, dts))) =
- if is_rec_type T then
- if tname = "fun" then
- if is_rec_type (hd dts) then
- typ_error T "Non-strictly positive recursive occurrence of type"
- else
- (case hd (tl dts) of
- DtType ("fun", _) => typ_error T "Curried function types not allowed"
- | T' => let val (i', [T''], descrs') = unfold_arg ((i, [], descrs), T')
- in (i', Ts @ [DtType (tname, [hd dts, T''])], descrs') end)
- else
- let val (index, descr) = get_dt_descr T i tname dts;
- val (descr', i') = unfold_datatypes sign orig_descr sorts dt_info descr (i + length descr)
- in (i', Ts @ [DtRec index], descrs @ descr') end
- else (i, Ts @ [T], descrs)
- | unfold_arg ((i, Ts, descrs), T) = (i, Ts @ [T], descrs);
+ fun unfold_arg ((i, Ts, descrs), T) =
+ if is_rec_type T then
+ let val (Us, U) = strip_dtyp T
+ in if exists is_rec_type Us then
+ typ_error T "Non-strictly positive recursive occurrence of type"
+ else (case U of
+ DtType (tname, dts) =>
+ let
+ val (index, descr) = get_dt_descr T i tname dts;
+ val (descr', i') = unfold_datatypes sign orig_descr sorts
+ dt_info descr (i + length descr)
+ in (i', Ts @ [mk_fun_dtyp Us (DtRec index)], descrs @ descr') end
+ | _ => (i, Ts @ [T], descrs))
+ end
+ else (i, Ts @ [T], descrs);
(* unfold a constructor *)
--- a/src/HOL/Tools/datatype_package.ML Thu Oct 10 14:23:47 2002 +0200
+++ b/src/HOL/Tools/datatype_package.ML Thu Oct 10 14:26:50 2002 +0200
@@ -450,7 +450,8 @@
val newTs = take (length (hd descr), recTs);
val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists
- (fn (DtType ("fun", [_, DtRec _])) => true | _ => false) cargs) constrs) descr';
+ (fn dt => is_rec_type dt andalso not (null (fst (strip_dtyp dt))))
+ cargs) constrs) descr';
(**** declare new types and constants ****)
@@ -470,9 +471,8 @@
val Ts = map (typ_of_dtyp descr' sorts) cargs;
val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
- fun mk_argT (DtRec k, _) = nth_elem (k, rec_result_Ts)
- | mk_argT (DtType ("fun", [_, DtRec k]), Type ("fun", [T, _])) =
- T --> nth_elem (k, rec_result_Ts);
+ fun mk_argT (dt, T) =
+ binder_types T ---> nth_elem (body_index dt, rec_result_Ts);
val argTs = Ts @ map mk_argT recs
in argTs ---> nth_elem (i, rec_result_Ts)
--- a/src/HOL/Tools/datatype_prop.ML Thu Oct 10 14:23:47 2002 +0200
+++ b/src/HOL/Tools/datatype_prop.ML Thu Oct 10 14:26:50 2002 +0200
@@ -11,38 +11,27 @@
val dtK : int ref
val indexify_names: string list -> string list
val make_tnames: typ list -> string list
- val make_injs : (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
- term list list
- val make_ind : (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> term
- val make_casedists : (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> term list
- val make_primrecs : string list -> (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
- theory -> term list
- val make_cases : string list -> (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
- theory -> term list list
- val make_distincts : string list -> (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
- theory -> term list list
- val make_splits : string list -> (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
- theory -> (term * term) list
- val make_case_trrules : string list -> (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list list -> ast Syntax.trrule list
- val make_size : (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
- theory -> term list
- val make_weak_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
- theory -> term list
- val make_case_congs : string list -> (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list ->
- theory -> term list
- val make_nchotomys : (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list list -> (string * sort) list -> term list
+ val make_injs : DatatypeAux.descr list -> (string * sort) list -> term list list
+ val make_ind : DatatypeAux.descr list -> (string * sort) list -> term
+ val make_casedists : DatatypeAux.descr list -> (string * sort) list -> term list
+ val make_primrecs : string list -> DatatypeAux.descr list ->
+ (string * sort) list -> theory -> term list
+ val make_cases : string list -> DatatypeAux.descr list ->
+ (string * sort) list -> theory -> term list list
+ val make_distincts : string list -> DatatypeAux.descr list ->
+ (string * sort) list -> theory -> term list list
+ val make_splits : string list -> DatatypeAux.descr list ->
+ (string * sort) list -> theory -> (term * term) list
+ val make_case_trrules : string list -> DatatypeAux.descr list ->
+ ast Syntax.trrule list
+ val make_size : DatatypeAux.descr list -> (string * sort) list ->
+ theory -> term list
+ val make_weak_case_congs : string list -> DatatypeAux.descr list ->
+ (string * sort) list -> theory -> term list
+ val make_case_congs : string list -> DatatypeAux.descr list ->
+ (string * sort) list -> theory -> term list
+ val make_nchotomys : DatatypeAux.descr list ->
+ (string * sort) list -> term list
end;
structure DatatypeProp : DATATYPE_PROP =
@@ -111,11 +100,11 @@
fun make_ind_prem k T (cname, cargs) =
let
- fun mk_prem ((DtRec k, s), T) = HOLogic.mk_Trueprop
- (make_pred k T $ Free (s, T))
- | mk_prem ((DtType ("fun", [_, DtRec k]), s), T' as Type ("fun", [T, U])) =
- all T $ Abs ("x", T, HOLogic.mk_Trueprop
- (make_pred k U $ (Free (s, T') $ Bound 0)));
+ fun mk_prem ((dt, s), T) =
+ let val (Us, U) = strip_type T
+ in list_all (map (pair "x") Us, HOLogic.mk_Trueprop
+ (make_pred (body_index dt) U $ app_bnds (Free (s, T)) (length Us)))
+ end;
val recs = filter is_rec_type cargs;
val Ts = map (typ_of_dtyp descr' sorts) cargs;
@@ -168,8 +157,6 @@
fun make_primrecs new_type_names descr sorts thy =
let
- val o_name = "Fun.comp";
-
val sign = Theory.sign_of thy;
val descr' = flat descr;
@@ -185,9 +172,8 @@
val Ts = map (typ_of_dtyp descr' sorts) cargs;
val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
- fun mk_argT (DtRec k, _) = nth_elem (k, rec_result_Ts)
- | mk_argT (DtType ("fun", [_, DtRec k]), Type ("fun", [T, _])) =
- T --> nth_elem (k, rec_result_Ts);
+ fun mk_argT (dt, T) =
+ binder_types T ---> nth_elem (body_index dt, rec_result_Ts);
val argTs = Ts @ map mk_argT recs
in argTs ---> nth_elem (i, rec_result_Ts)
@@ -215,17 +201,17 @@
val frees = map Free (tnames ~~ Ts);
val frees' = map Free (rec_tnames ~~ recTs');
- fun mk_reccomb (DtRec i, _) = nth_elem (i, reccombs)
- | mk_reccomb (DtType ("fun", [_, DtRec i]), Type ("fun", [T, U])) =
- let val T' = nth_elem (i, rec_result_Ts)
- in Const (o_name, [U --> T', T --> U, T] ---> T') $ nth_elem (i, reccombs)
- end;
+ fun mk_reccomb ((dt, T), t) =
+ let val (Us, U) = strip_type T
+ in list_abs (map (pair "x") Us,
+ nth_elem (body_index dt, reccombs) $ app_bnds t (length Us))
+ end;
- val reccombs' = map mk_reccomb (recs ~~ recTs')
+ val reccombs' = map mk_reccomb (recs ~~ recTs' ~~ frees')
in (ts @ [HOLogic.mk_Trueprop (HOLogic.mk_eq
(comb_t $ list_comb (Const (cname, Ts ---> T), frees),
- list_comb (f, frees @ (map (op $) (reccombs' ~~ frees')))))], fs)
+ list_comb (f, frees @ reccombs')))], fs)
end
in fst (foldl (fn (x, ((dt, T), comb_t)) =>
--- a/src/HOL/Tools/datatype_realizer.ML Thu Oct 10 14:23:47 2002 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML Thu Oct 10 14:26:50 2002 +0200
@@ -88,23 +88,18 @@
in (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs'))
(list_comb (Const (cname, Ts ---> T), map Free frees))), f')
end
- | mk_prems vs (((DtRec k, s), T) :: ds) =
+ | mk_prems vs (((dt, s), T) :: ds) =
let
+ val k = body_index dt;
+ val (Us, U) = strip_type T;
+ val i = length Us;
val rT = nth_elem (k, rec_result_Ts);
- val r = Free ("r" ^ s, rT);
+ val r = Free ("r" ^ s, Us ---> rT);
val (p, f) = mk_prems (vs @ [r]) ds
- in (mk_all k ("r" ^ s) rT (Logic.mk_implies
- (HOLogic.mk_Trueprop (make_pred k rT T r (Free (s, T))), p)), f)
- end
- | mk_prems vs (((DtType ("fun", [_, DtRec k]), s),
- T' as Type ("fun", [T, U])) :: ds) =
- let
- val rT = nth_elem (k, rec_result_Ts);
- val r = Free ("r" ^ s, T --> rT);
- val (p, f) = mk_prems (vs @ [r]) ds
- in (mk_all k ("r" ^ s) (T --> rT) (Logic.mk_implies
- (all T $ Abs ("x", T, HOLogic.mk_Trueprop (make_pred k rT U
- (r $ Bound 0) (Free (s, T') $ Bound 0))), p)), f)
+ in (mk_all k ("r" ^ s) (Us ---> rT) (Logic.mk_implies
+ (list_all (map (pair "x") Us, HOLogic.mk_Trueprop
+ (make_pred k rT U (app_bnds r i)
+ (app_bnds (Free (s, T)) i))), p)), f)
end
in (j + 1,
--- a/src/HOL/Tools/datatype_rep_proofs.ML Thu Oct 10 14:23:47 2002 +0200
+++ b/src/HOL/Tools/datatype_rep_proofs.ML Thu Oct 10 14:26:50 2002 +0200
@@ -15,11 +15,10 @@
signature DATATYPE_REP_PROOFS =
sig
val representation_proofs : bool -> DatatypeAux.datatype_info Symtab.table ->
- string list -> (int * (string * DatatypeAux.dtyp list *
- (string * DatatypeAux.dtyp list) list)) list 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
+ 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
end;
structure DatatypeRepProofs : DATATYPE_REP_PROOFS =
@@ -54,19 +53,15 @@
val Leaf_name = "Datatype_Universe.Leaf";
val Numb_name = "Datatype_Universe.Numb";
val Lim_name = "Datatype_Universe.Lim";
- val Funs_name = "Datatype_Universe.Funs";
- val o_name = "Fun.comp";
- val sum_case_name = "Datatype.sum.sum_case";
+ val Suml_name = "Datatype.Suml";
+ val Sumr_name = "Datatype.Sumr";
- val [In0_inject, In1_inject, Scons_inject, Leaf_inject, In0_eq, In1_eq,
- In0_not_In1, In1_not_In0, Funs_mono, FunsI, Lim_inject,
- Funs_inv, FunsD, Funs_rangeE, Funs_nonempty, sum_case_inject] = map (get_thm Datatype_thy)
- ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject", "In0_eq", "In1_eq",
- "In0_not_In1", "In1_not_In0", "Funs_mono", "FunsI", "Lim_inject",
- "Funs_inv", "FunsD", "Funs_rangeE", "Funs_nonempty", "sum_case_inject"];
-
- val Funs_IntE = (Int_lower2 RS Funs_mono RS
- (Int_lower1 RS Funs_mono RS Int_greatest) RS subsetD) RS IntE;
+ val [In0_inject, In1_inject, Scons_inject, Leaf_inject,
+ In0_eq, In1_eq, In0_not_In1, In1_not_In0,
+ Lim_inject, Suml_inject, Sumr_inject] = map (get_thm Datatype_thy)
+ ["In0_inject", "In1_inject", "Scons_inject", "Leaf_inject",
+ "In0_eq", "In1_eq", "In0_not_In1", "In1_not_In0",
+ "Lim_inject", "Suml_inject", "Sumr_inject"];
val descr' = flat descr;
@@ -83,6 +78,7 @@
val branchTs = get_branching_types descr' sorts;
val branchT = if null branchTs then HOLogic.unitT
else fold_bal (fn (T, U) => Type ("+", [T, U])) branchTs;
+ val arities = get_arities descr' \ 0;
val unneeded_vars = hd tyvars \\ foldr add_typ_tfree_names (leafTs' @ branchTs, []);
val leafTs = leafTs' @ (map (fn n => TFree (n, the (assoc (sorts, n)))) unneeded_vars);
val recTs = get_rec_types descr' sorts;
@@ -131,16 +127,16 @@
let
val n2 = n div 2;
val Type (_, [T1, T2]) = T;
- val sum_case = Const (sum_case_name, [T1 --> Univ_elT, T2 --> Univ_elT, T] ---> Univ_elT)
+ fun mkT U = (U --> Univ_elT) --> T --> Univ_elT
in
- if i <= n2 then
- sum_case $ (mk_inj T1 n2 i) $ Const ("arbitrary", T2 --> Univ_elT)
- else
- sum_case $ Const ("arbitrary", T1 --> Univ_elT) $ mk_inj T2 (n - n2) (i - n2)
+ if i <= n2 then Const (Suml_name, mkT T1) $ mk_inj T1 n2 i
+ else Const (Sumr_name, mkT T2) $ mk_inj T2 (n - n2) (i - n2)
end
in mk_inj branchT (length branchTs) (1 + find_index_eq T' branchTs)
end;
+ val mk_lim = foldr (fn (T, t) => Lim $ mk_fun_inj T (Abs ("x", T, t)));
+
(************** generate introduction rules for representing set **********)
val _ = message "Constructing representing sets ...";
@@ -149,28 +145,26 @@
fun make_intr s n (i, (_, cargs)) =
let
- fun mk_prem (DtRec k, (j, prems, ts)) =
- let val free_t = mk_Free "x" Univ_elT j
- in (j + 1, (HOLogic.mk_mem (free_t,
- Const (nth_elem (k, rep_set_names), UnivT)))::prems, free_t::ts)
+ fun mk_prem (dt, (j, prems, ts)) = (case strip_dtyp dt of
+ (dts, DtRec k) =>
+ let
+ val Ts = map (typ_of_dtyp descr' sorts) dts;
+ val free_t =
+ app_bnds (mk_Free "x" (Ts ---> Univ_elT) j) (length Ts)
+ in (j + 1, list_all (map (pair "x") Ts,
+ HOLogic.mk_Trueprop (HOLogic.mk_mem (free_t,
+ Const (nth_elem (k, rep_set_names), UnivT)))) :: prems,
+ mk_lim (Ts, free_t) :: ts)
end
- | mk_prem (DtType ("fun", [T, DtRec k]), (j, prems, ts)) =
- let val T' = typ_of_dtyp descr' sorts T;
- val free_t = mk_Free "x" (T' --> Univ_elT) j
- in (j + 1, (HOLogic.mk_mem (free_t,
- Const (Funs_name, UnivT --> HOLogic.mk_setT (T' --> Univ_elT)) $
- Const (nth_elem (k, rep_set_names), UnivT)))::prems,
- Lim $ mk_fun_inj T' free_t::ts)
- end
- | mk_prem (dt, (j, prems, ts)) =
+ | _ =>
let val T = typ_of_dtyp descr' sorts dt
in (j + 1, prems, (Leaf $ mk_inj T (mk_Free "x" T j))::ts)
- end;
+ end);
val (_, prems, ts) = foldr mk_prem (cargs, (1, [], []));
val concl = HOLogic.mk_Trueprop (HOLogic.mk_mem
(mk_univ_inj ts n i, Const (s, UnivT)))
- in Logic.list_implies (map HOLogic.mk_Trueprop prems, concl)
+ in Logic.list_implies (prems, concl)
end;
val consts = map (fn s => Const (s, UnivT)) rep_set_names;
@@ -182,7 +176,7 @@
val (thy2, {raw_induct = rep_induct, intrs = rep_intrs, ...}) =
setmp InductivePackage.quiet_mode (!quiet_mode)
(InductivePackage.add_inductive_i false true big_rec_name false true false
- consts (map (fn x => (("", x), [])) intr_ts) [Funs_mono]) thy1;
+ consts (map (fn x => (("", x), [])) intr_ts) []) thy1;
(********************************* typedef ********************************)
@@ -191,7 +185,7 @@
(TypedefPackage.add_typedef_i false (Some name') (name, tvs, mx) c None
(rtac exI 1 THEN
QUIET_BREADTH_FIRST (has_fewer_prems 1)
- (resolve_tac (Funs_nonempty::rep_intrs) 1))) thy |> #1)
+ (resolve_tac rep_intrs 1))) thy |> #1)
(parent_path flat_names thy2, types_syntax ~~ tyvars ~~
(take (length newTs, consts)) ~~ new_type_names));
@@ -216,16 +210,10 @@
fun constr_arg (dt, (j, l_args, r_args)) =
let val T = typ_of_dtyp descr' sorts dt;
val free_t = mk_Free "x" T j
- in (case dt of
- DtRec m => (j + 1, free_t::l_args, (Const (nth_elem (m, all_rep_names),
- T --> Univ_elT) $ free_t)::r_args)
- | DtType ("fun", [T', DtRec m]) =>
- let val ([T''], T''') = strip_type T
- in (j + 1, free_t::l_args, (Lim $ mk_fun_inj T''
- (Const (o_name, [T''' --> Univ_elT, T, T''] ---> Univ_elT) $
- Const (nth_elem (m, all_rep_names), T''' --> Univ_elT) $ free_t))::r_args)
- end
-
+ in (case (strip_dtyp dt, strip_type T) of
+ ((_, DtRec m), (Us, U)) => (j + 1, free_t :: l_args, mk_lim (Us,
+ Const (nth_elem (m, all_rep_names), U --> Univ_elT) $
+ app_bnds free_t (length Us)) :: r_args)
| _ => (j + 1, free_t::l_args, (Leaf $ mk_inj T free_t)::r_args))
end;
@@ -321,11 +309,11 @@
(* isomorphisms are defined using primrec-combinators: *)
(* generate appropriate functions for instantiating primrec-combinator *)
(* *)
- (* e.g. dt_Rep_i = list_rec ... (%h t y. In1 ((Leaf h) $ y)) *)
+ (* e.g. dt_Rep_i = list_rec ... (%h t y. In1 (Scons (Leaf h) y)) *)
(* *)
(* also generate characteristic equations for isomorphisms *)
(* *)
- (* e.g. dt_Rep_i (cons h t) = In1 ((dt_Rep_j h) $ (dt_Rep_i t)) *)
+ (* e.g. dt_Rep_i (cons h t) = In1 (Scons (dt_Rep_j h) (dt_Rep_i t)) *)
(*---------------------------------------------------------------------*)
fun make_iso_def k ks n ((fs, eqns, i), (cname, cargs)) =
@@ -337,24 +325,18 @@
val constr = Const (cname, argTs ---> T);
fun process_arg ks' ((i2, i2', ts, Ts), dt) =
- let val T' = typ_of_dtyp descr' sorts dt
- in (case dt of
- DtRec j => if j mem ks' then
- (i2 + 1, i2' + 1, ts @ [mk_Free "y" Univ_elT i2'], Ts @ [Univ_elT])
+ let
+ val T' = typ_of_dtyp descr' sorts dt;
+ val (Us, U) = strip_type T'
+ in (case strip_dtyp dt of
+ (_, DtRec j) => if j mem ks' then
+ (i2 + 1, i2' + 1, ts @ [mk_lim (Us, app_bnds
+ (mk_Free "y" (Us ---> Univ_elT) i2') (length Us))],
+ Ts @ [Us ---> Univ_elT])
else
- (i2 + 1, i2', ts @ [Const (nth_elem (j, all_rep_names),
- T' --> Univ_elT) $ mk_Free "x" T' i2], Ts)
- | (DtType ("fun", [_, DtRec j])) =>
- let val ([T''], T''') = strip_type T'
- in if j mem ks' then
- (i2 + 1, i2' + 1, ts @ [Lim $ mk_fun_inj T''
- (mk_Free "y" (T'' --> Univ_elT) i2')], Ts @ [T'' --> Univ_elT])
- else
- (i2 + 1, i2', ts @ [Lim $ mk_fun_inj T''
- (Const (o_name, [T''' --> Univ_elT, T', T''] ---> Univ_elT) $
- Const (nth_elem (j, all_rep_names), T''' --> Univ_elT) $
- mk_Free "x" T' i2)], Ts)
- end
+ (i2 + 1, i2', ts @ [mk_lim (Us,
+ Const (nth_elem (j, all_rep_names), U --> Univ_elT) $
+ app_bnds (mk_Free "x" T' i2) (length Us))], Ts)
| _ => (i2 + 1, i2', ts @ [Leaf $ mk_inj T' (mk_Free "x" T' i2)], Ts))
end;
@@ -406,18 +388,25 @@
fun mk_funs_inv thm =
let
- val [_, t] = prems_of Funs_inv;
- val [_ $ (_ $ _ $ R)] = Logic.strip_assums_hyp t;
- val _ $ (_ $ (r $ (a $ _)) $ _) = Logic.strip_assums_concl t;
- val [_ $ (_ $ _ $ R')] = prems_of thm;
- val _ $ (_ $ (r' $ (a' $ _)) $ _) = concl_of thm;
- val inv' = cterm_instantiate (map
- ((pairself (cterm_of (sign_of_thm thm))) o
- (apsnd (map_term_types (incr_tvar 1))))
- [(R, R'), (r, r'), (a, a')]) Funs_inv
- in
- rule_by_tactic (atac 2) (thm RSN (2, inv'))
- end;
+ val {sign, prop, ...} = rep_thm thm;
+ val (_ $ (_ $ (Const (_, Type (_, [U, _])) $ _ $ S)) $
+ (_ $ (_ $ (r $ (a $ _)) $ _)), _) = Type.freeze_thaw prop;
+ val used = add_term_tfree_names (a, []);
+
+ fun mk_thm i =
+ let
+ val Ts = map (TFree o rpair HOLogic.typeS)
+ (variantlist (replicate i "'t", used));
+ val f = Free ("f", Ts ---> U)
+ in prove_goalw_cterm [] (cterm_of sign (Logic.mk_implies
+ (HOLogic.mk_Trueprop (HOLogic.list_all
+ (map (pair "x") Ts, HOLogic.mk_mem (app_bnds f i, S))),
+ HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
+ r $ (a $ app_bnds f i)), f))))) (fn prems =>
+ [cut_facts_tac prems 1, REPEAT (rtac ext 1),
+ REPEAT (etac allE 1), rtac thm 1, atac 1])
+ end
+ in map (fn r => r RS subst) (thm :: map mk_thm arities) end;
(* prove inj dt_Rep_i and dt_Rep_i x : dt_rep_set_i *)
@@ -440,8 +429,8 @@
val (ind_concl1, ind_concl2) = ListPair.unzip (map mk_ind_concl ds);
val rewrites = map mk_meta_eq iso_char_thms;
- val inj_thms' = flat (map (fn r => [r RS injD, r RS inj_o])
- (map snd newT_iso_inj_thms @ inj_thms));
+ val inj_thms' = map (fn r => r RS injD)
+ (map snd newT_iso_inj_thms @ inj_thms);
val inj_thm = prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5)
(HOLogic.mk_Trueprop (mk_conj ind_concl1))) (fn _ =>
@@ -455,13 +444,15 @@
REPEAT (dresolve_tac [In0_inject, In1_inject] 1),
(eresolve_tac [In0_not_In1 RS notE, In1_not_In0 RS notE] 1)
ORELSE (EVERY
- [REPEAT (eresolve_tac (Scons_inject :: sum_case_inject ::
- map make_elim (inj_thms' @
- [Leaf_inject, Lim_inject, Inl_inject, Inr_inject])) 1),
- REPEAT ((EVERY [etac allE 1, dtac mp 1, atac 1]) ORELSE
- (dtac inj_fun_lemma 1 THEN atac 1)),
- REPEAT (hyp_subst_tac 1),
- rtac refl 1])])])]);
+ [REPEAT (eresolve_tac (Scons_inject ::
+ map make_elim [Leaf_inject, Inl_inject, Inr_inject]) 1),
+ REPEAT (cong_tac 1), rtac refl 1,
+ REPEAT (atac 1 ORELSE (EVERY
+ [REPEAT (rtac ext 1),
+ REPEAT (eresolve_tac (mp :: allE ::
+ map make_elim (Suml_inject :: Sumr_inject ::
+ Lim_inject :: fun_cong :: inj_thms')) 1),
+ atac 1]))])])])]);
val inj_thms'' = map (fn r => r RS datatype_injI)
(split_conj_thm inj_thm);
@@ -472,11 +463,9 @@
(HOLogic.mk_Trueprop (mk_conj ind_concl2)))
(fn _ =>
[(indtac induction THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
- rewrite_goals_tac (o_def :: rewrites),
- REPEAT (EVERY
- [resolve_tac rep_intrs 1,
- REPEAT (FIRST [atac 1, etac spec 1,
- resolve_tac (FunsI :: elem_thms) 1])])]);
+ rewrite_goals_tac rewrites,
+ REPEAT ((resolve_tac rep_intrs THEN_ALL_NEW
+ ((REPEAT o etac allE) THEN' ares_tac elem_thms)) 1)]);
in (inj_thms'' @ inj_thms, elem_thms @ (split_conj_thm elem_thm))
end;
@@ -502,18 +491,20 @@
(* all the theorems are proved by one single simultaneous induction *)
+ val range_eqs = map (fn r => mk_meta_eq (r RS range_ex1_eq))
+ iso_inj_thms_unfolded;
+
val iso_thms = if length descr = 1 then [] else
drop (length newTs, split_conj_thm
(prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) iso_t) (fn _ =>
- [indtac rep_induct 1,
+ [(indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
REPEAT (rtac TrueI 1),
+ rewrite_goals_tac (mk_meta_eq choice_eq ::
+ symmetric (mk_meta_eq expand_fun_eq) :: range_eqs),
+ rewrite_goals_tac (map symmetric range_eqs),
REPEAT (EVERY
- [rewrite_goals_tac [mk_meta_eq Collect_mem_eq],
- REPEAT (etac Funs_IntE 1),
- REPEAT (eresolve_tac (rangeE ::
- map (fn r => r RS Funs_rangeE) iso_inj_thms_unfolded) 1),
- REPEAT (eresolve_tac (map (fn (iso, _, _) => iso RS subst) newT_iso_axms @
- map (fn (iso, _, _) => mk_funs_inv iso RS subst) newT_iso_axms) 1),
+ [REPEAT (eresolve_tac ([rangeE, ex1_implies_ex RS exE] @
+ flat (map (mk_funs_inv o #1) newT_iso_axms)) 1),
TRY (hyp_subst_tac 1),
rtac (sym RS range_eqI) 1,
resolve_tac iso_char_thms 1])])));
@@ -523,8 +514,7 @@
map2 (fn (r_inj, r) => f_myinv_f OF [r_inj, r RS mp])
(iso_inj_thms_unfolded, iso_thms);
- val Abs_inverse_thms = map (fn r => r RS subst) (Abs_inverse_thms' @
- map mk_funs_inv Abs_inverse_thms');
+ val Abs_inverse_thms = flat (map mk_funs_inv Abs_inverse_thms');
(******************* freeness theorems for constructors *******************)
@@ -541,7 +531,7 @@
rewrite_goals_tac rewrites,
rtac refl 1,
resolve_tac rep_intrs 2,
- REPEAT (resolve_tac (FunsI :: iso_elem_thms) 1)])
+ REPEAT (resolve_tac iso_elem_thms 1)])
end;
(*--------------------------------------------------------------*)
@@ -575,17 +565,19 @@
(* prove injectivity of constructors *)
fun prove_constr_inj_thm rep_thms t =
- let val inj_thms = Scons_inject::sum_case_inject::(map make_elim
+ let val inj_thms = Scons_inject :: (map make_elim
((map (fn r => r RS injD) iso_inj_thms) @
- [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject, Lim_inject]))
+ [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject,
+ Lim_inject, Suml_inject, Sumr_inject]))
in prove_goalw_cterm [] (cterm_of (Theory.sign_of thy5) t) (fn _ =>
[rtac iffI 1,
REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
dresolve_tac rep_congs 1, dtac box_equals 1,
- REPEAT (resolve_tac rep_thms 1), rewtac o_def,
+ REPEAT (resolve_tac rep_thms 1),
REPEAT (eresolve_tac inj_thms 1),
- REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [rtac ext 1, dtac fun_cong 1,
- eresolve_tac inj_thms 1, atac 1]))])
+ REPEAT (ares_tac [conjI] 1 ORELSE (EVERY [REPEAT (rtac ext 1),
+ REPEAT (eresolve_tac (make_elim fun_cong :: inj_thms) 1),
+ atac 1]))])
end;
val constr_inject = map (fn (ts, thms) => map (prove_constr_inj_thm thms) ts)
@@ -641,12 +633,12 @@
val dt_induct = prove_goalw_cterm [] (cert
(DatatypeProp.make_ind descr sorts)) (fn prems =>
- [rtac indrule_lemma' 1, indtac rep_induct 1,
+ [rtac indrule_lemma' 1,
+ (indtac rep_induct THEN_ALL_NEW ObjectLogic.atomize_tac) 1,
EVERY (map (fn (prem, r) => (EVERY
- [REPEAT (eresolve_tac (Funs_IntE::Abs_inverse_thms) 1),
+ [REPEAT (eresolve_tac Abs_inverse_thms 1),
simp_tac (HOL_basic_ss addsimps ((symmetric r)::Rep_inverse_thms')) 1,
- DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE (EVERY [rewtac o_def,
- dtac FunsD 1, etac CollectD 1]))]))
+ DEPTH_SOLVE_1 (ares_tac [prem] 1 ORELSE etac allE 1)]))
(prems ~~ (constr_defs @ (map mk_meta_eq iso_char_thms))))]);
val (thy7, [dt_induct']) = thy6 |>
--- a/src/HOL/Tools/primrec_package.ML Thu Oct 10 14:23:47 2002 +0200
+++ b/src/HOL/Tools/primrec_package.ML Thu Oct 10 14:26:50 2002 +0200
@@ -141,16 +141,13 @@
(fnames', fnss', (Const ("arbitrary", dummyT))::fns))
| Some (ls, cargs', rs, rhs, eq) =>
let
- fun rec_index (DtRec k) = k
- | rec_index (DtType ("fun", [_, DtRec k])) = k;
-
val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
val rargs = map fst recs;
val subs = map (rpair dummyT o fst)
(rev (rename_wrt_term rhs rargs));
val ((fnames'', fnss''), rhs') =
(subst (map (fn ((x, y), z) =>
- (Free x, (rec_index y, Free z)))
+ (Free x, (body_index y, Free z)))
(recs ~~ subs))
((fnames', fnss'), rhs))
handle RecError s => primrec_eq_err sign s eq
@@ -257,7 +254,7 @@
(if eq_set (names1, names2) then (PureThy.add_defs_i false o map Thm.no_attributes) defs'
else primrec_err ("functions " ^ commas_quote names2 ^
"\nare not mutually recursive"));
- val rewrites = o_def :: (map mk_meta_eq rec_rewrites) @ defs_thms';
+ val rewrites = (map mk_meta_eq rec_rewrites) @ defs_thms';
val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names1 ^ " ...");
val simps = map (fn (_, t) => prove_goalw_cterm rewrites (cterm_of (Theory.sign_of thy') t)
(fn _ => [rtac refl 1])) eqns;