--- a/src/HOL/BNF/Tools/bnf_fp_sugar.ML Wed Sep 26 10:00:59 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_sugar.ML Wed Sep 26 10:00:59 2012 +0200
@@ -9,19 +9,13 @@
sig
val datatypes: bool ->
(mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
- BNF_Def.BNF list -> local_theory ->
- (BNF_Def.BNF list * term list * term list * term list * term list * thm * thm list *
- thm list * thm list * thm list * thm list list * thm list * thm list * thm list) *
- local_theory) ->
+ BNF_Def.BNF list -> local_theory -> BNF_FP.fp_result * local_theory) ->
bool * ((((typ * sort) list * binding) * mixfix) * ((((binding * binding) *
(binding * typ) list) * (binding * term) list) * mixfix) list) list ->
local_theory -> local_theory
val parse_datatype_cmd: bool ->
(mixfix list -> (string * sort) list option -> binding list -> typ list * typ list list ->
- BNF_Def.BNF list -> local_theory ->
- (BNF_Def.BNF list * term list * term list * term list * term list * thm * thm list *
- thm list * thm list * thm list * thm list list * thm list * thm list * thm list) *
- local_theory) ->
+ BNF_Def.BNF list -> local_theory -> BNF_FP.fp_result * local_theory) ->
(local_theory -> local_theory) parser
end;
@@ -34,6 +28,8 @@
open BNF_FP
open BNF_FP_Sugar_Tactics
+val mp_conj = @{thm mp_conj};
+
val simp_attrs = @{attributes [simp]};
val code_simp_attrs = Code.add_default_eqn_attrib :: simp_attrs;
@@ -96,6 +92,11 @@
Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
end;
+fun mk_rel live Ts Us t =
+ let val [Type (_, Ts0), Type (_, Us0)] = binder_types (snd (strip_typeN live (fastype_of t))) in
+ Term.subst_atomic_types (Ts0 @ Us0 ~~ Ts @ Us) t
+ end;
+
fun liveness_of_fp_bnf n bnf =
(case T_of_bnf bnf of
Type (_, Ts) => map (not o member (op =) (deads_of_bnf bnf)) Ts
@@ -119,6 +120,10 @@
op aconv (Logic.dest_implies (Thm.prop_of thm))
handle TERM _ => false;
+fun reassoc_conjs thm =
+ reassoc_conjs (thm RS @{thm conj_assoc[THEN iffD1]})
+ handle THM _ => thm;
+
fun type_args_constrained_of (((cAs, _), _), _) = cAs;
fun type_binding_of (((_, b), _), _) = b;
fun mixfix_of ((_, mx), _) = mx;
@@ -205,13 +210,15 @@
| A' :: _ => error ("Extra type variable on right-hand side: " ^
quote (Syntax.string_of_typ no_defs_lthy (TFree A'))));
- fun eq_fpT (T as Type (s, Us)) (Type (s', Us')) =
+ fun eq_fpT_check (T as Type (s, Us)) (Type (s', Us')) =
s = s' andalso (Us = Us' orelse error ("Illegal occurrence of recursive type " ^
quote (Syntax.string_of_typ fake_lthy T)))
- | eq_fpT _ _ = false;
+ | eq_fpT_check _ _ = false;
fun freeze_fp (T as Type (s, Us)) =
- (case find_index (eq_fpT T) fake_Ts of ~1 => Type (s, map freeze_fp Us) | j => nth Xs j)
+ (case find_index (eq_fpT_check T) fake_Ts of
+ ~1 => Type (s, map freeze_fp Us)
+ | kk => nth Xs kk)
| freeze_fp T = T;
val ctr_TsssXs = map (map (map freeze_fp)) fake_ctr_Tsss;
@@ -222,8 +229,8 @@
(* TODO: clean up list *)
val (pre_bnfs, ((fp_bnfs as any_fp_bnf :: _, dtors0, ctors0, fp_folds0, fp_recs0, fp_induct,
- dtor_ctors, ctor_dtors, ctor_injects, fp_map_thms, fp_set_thmss, fp_rel_thms,
- fp_fold_thms, fp_rec_thms), lthy)) =
+ fp_strong_induct, dtor_ctors, ctor_dtors, ctor_injects, fp_map_thms, fp_set_thmss,
+ fp_rel_thms, fp_fold_thms, fp_rec_thms), lthy)) =
fp_bnf construct_fp fp_bs mixfixes (map dest_TFree unsorted_As) fp_eqs no_defs_lthy0;
val timer = time (Timer.startRealTimer ());
@@ -247,8 +254,8 @@
val pre_set_defss = map set_defs_of_bnf pre_bnfs;
val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
val nested_set_natural's = maps set_natural'_of_bnf nested_bnfs;
+ val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
val nesting_set_natural's = maps set_natural'_of_bnf nesting_bnfs;
- val nesting_map_ids = map map_id_of_bnf nesting_bnfs;
val live = live_of_bnf any_fp_bnf;
@@ -279,7 +286,7 @@
val (((fold_only as (gss, _, _), rec_only as (hss, _, _)),
(zs, cs, cpss, unfold_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))),
- names_lthy) =
+ names_lthy0) =
if lfp then
let
val y_Tsss =
@@ -520,14 +527,13 @@
fun mk_rel_thm postproc ctr_defs' xs cxIn ys cyIn =
fold_thms lthy ctr_defs'
- (unfold_thms lthy (pre_rel_def ::
- (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_rel)
+ (unfold_thms lthy (pre_rel_def :: (if lfp then [] else [dtor_ctor]) @
+ sum_prod_thms_rel)
(cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
|> postproc |> thaw (xs @ ys);
fun mk_pos_rel_thm (((ctr_def', xs), cxIn), ((_, ys), cyIn)) =
- mk_rel_thm (perhaps (try (fn th => th RS @{thm eq_sym_Unity_imp}))) [ctr_def']
- xs cxIn ys cyIn;
+ mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] xs cxIn ys cyIn;
val pos_rel_thms = map mk_pos_rel_thm (op ~~ rel_infos);
@@ -647,19 +653,18 @@
val bnf = the (bnf_of lthy s);
val live = live_of_bnf bnf;
val mapx = mk_map live Ts Us (map_of_bnf bnf);
- val TUs = map dest_funT (fst (strip_typeN live (fastype_of mapx)));
- val args = map build_arg TUs;
- in Term.list_comb (mapx, args) end;
+ val TUs' = map dest_funT (fst (strip_typeN live (fastype_of mapx)));
+ in Term.list_comb (mapx, map build_arg TUs') end;
(* TODO: Add map, sets, rel simps *)
val mk_simp_thmss =
- map3 (fn (_, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn fold_likes =>
+ map3 (fn (_, _, _, injects, distincts, cases, _, _, _) => fn rec_likes => fn fold_likes =>
injects @ distincts @ cases @ rec_likes @ fold_likes);
fun derive_induct_fold_rec_thms_for_types (((ctrss, xsss, ctr_defss, wrap_ress), (folds, recs,
fold_defs, rec_defs)), lthy) =
let
- val (((phis, phis'), us'), names_lthy) =
+ val (((ps, ps'), us'), names_lthy) =
lthy
|> mk_Frees' "P" (map mk_pred1T fpTs)
||>> Variable.variant_fixes fp_b_names;
@@ -704,17 +709,17 @@
in
flat (map2 (map o apfst o cons) xysets ppremss)
end)
- | i => [([], (i + 1, x))])
+ | kk => [([], (kk + 1, x))])
| mk_raw_prem_prems _ _ = [];
fun close_prem_prem xs t =
fold_rev Logic.all (map Free (drop (nn + length xs)
- (rev (Term.add_frees t (map dest_Free xs @ phis'))))) t;
+ (rev (Term.add_frees t (map dest_Free xs @ ps'))))) t;
fun mk_prem_prem xs (xysets, (j, x)) =
close_prem_prem xs (Logic.list_implies (map (fn (x', (y, set)) =>
HOLogic.mk_Trueprop (HOLogic.mk_mem (y, set $ x'))) xysets,
- HOLogic.mk_Trueprop (nth phis (j - 1) $ x)));
+ HOLogic.mk_Trueprop (nth ps (j - 1) $ x)));
fun mk_raw_prem phi ctr ctr_Ts =
let
@@ -725,23 +730,24 @@
fun mk_prem (xs, raw_pprems, concl) =
fold_rev Logic.all xs (Logic.list_implies (map (mk_prem_prem xs) raw_pprems, concl));
- val raw_premss = map3 (map2 o mk_raw_prem) phis ctrss ctr_Tsss;
+ val raw_premss = map3 (map2 o mk_raw_prem) ps ctrss ctr_Tsss;
val goal =
Library.foldr (Logic.list_implies o apfst (map mk_prem)) (raw_premss,
- HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) phis us)));
+ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 (curry (op $)) ps us)));
val kksss = map (map (map (fst o snd) o #2)) raw_premss;
val ctor_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
- val induct_thm =
+ val thm =
Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
mk_induct_tac ctxt nn ns mss kksss (flat ctr_defss) ctor_induct'
nested_set_natural's pre_set_defss)
|> singleton (Proof_Context.export names_lthy lthy)
+ |> Thm.close_derivation;
in
- `(conj_dests nn) induct_thm
+ `(conj_dests nn) thm
end;
(* TODO: Generate nicer names in case of clashes *)
@@ -757,27 +763,28 @@
fold_rev (fold_rev Logic.all) (xs :: fss)
(mk_Trueprop_eq (frec_like $ xctr, Term.list_comb (f, fxs)));
- fun build_call frec_likes maybe_tick (T, U) =
+ fun build_rec_like frec_likes maybe_tick (T, U) =
if T = U then
id_const T
else
(case find_index (curry (op =) T) fpTs of
- ~1 => build_map (build_call frec_likes maybe_tick) T U
- | j => maybe_tick (nth us j) (nth frec_likes j));
+ ~1 => build_map (build_rec_like frec_likes maybe_tick) T U
+ | kk => maybe_tick (nth us kk) (nth frec_likes kk));
fun mk_U maybe_mk_prodT =
typ_subst (map2 (fn fpT => fn C => (fpT, maybe_mk_prodT fpT C)) fpTs Cs);
- fun intr_calls frec_likes maybe_cons maybe_tick maybe_mk_prodT (x as Free (_, T)) =
+ fun intr_rec_likes frec_likes maybe_cons maybe_tick maybe_mk_prodT (x as Free (_, T)) =
if member (op =) fpTs T then
- maybe_cons x [build_call frec_likes (K I) (T, mk_U (K I) T) $ x]
+ maybe_cons x [build_rec_like frec_likes (K I) (T, mk_U (K I) T) $ x]
else if exists_fp_subtype T then
- [build_call frec_likes maybe_tick (T, mk_U maybe_mk_prodT T) $ x]
+ [build_rec_like frec_likes maybe_tick (T, mk_U maybe_mk_prodT T) $ x]
else
[x];
- val gxsss = map (map (maps (intr_calls gfolds (K I) (K I) (K I)))) xsss;
- val hxsss = map (map (maps (intr_calls hrecs cons tick (curry HOLogic.mk_prodT)))) xsss;
+ val gxsss = map (map (maps (intr_rec_likes gfolds (K I) (K I) (K I)))) xsss;
+ val hxsss =
+ map (map (maps (intr_rec_likes hrecs cons tick (curry HOLogic.mk_prodT)))) xsss;
val fold_goalss = map5 (map4 o mk_goal gss) gfolds xctrss gss xsss gxsss;
val rec_goalss = map5 (map4 o mk_goal hss) hrecs xctrss hss xsss hxsss;
@@ -789,7 +796,9 @@
map2 (map o mk_rec_like_tac pre_map_defs nesting_map_ids rec_defs) fp_rec_thms
ctr_defss;
- fun prove goal tac = Skip_Proof.prove lthy [] [] goal (tac o #context);
+ fun prove goal tac =
+ Skip_Proof.prove lthy [] [] goal (tac o #context)
+ |> Thm.close_derivation;
in
(map2 (map2 prove) fold_goalss fold_tacss,
map2 (map2 prove) rec_goalss rec_tacss)
@@ -822,28 +831,99 @@
fun derive_coinduct_unfold_corec_thms_for_types (((ctrss, _, ctr_defss, wrap_ress), (unfolds,
corecs, unfold_defs, corec_defs)), lthy) =
let
+ val nesting_rel_eqs = map rel_eq_of_bnf nesting_bnfs;
+
val discss = map (map (mk_disc_or_sel As) o #1) wrap_ress;
- val selsss = map #2 wrap_ress;
- val disc_thmsss = map #6 wrap_ress;
- val discIss = map #7 wrap_ress;
- val sel_thmsss = map #8 wrap_ress;
+ val selsss = map (map (map (mk_disc_or_sel As)) o #2) wrap_ress;
+ val exhaust_thms = map #3 wrap_ress;
+ val disc_thmsss = map #7 wrap_ress;
+ val discIss = map #8 wrap_ress;
+ val sel_thmsss = map #9 wrap_ress;
- val (us', _) =
+ val (((rs, us'), vs'), names_lthy) =
lthy
- |> Variable.variant_fixes fp_b_names;
+ |> mk_Frees "R" (map (fn T => mk_pred2T T T) fpTs)
+ ||>> Variable.variant_fixes fp_b_names
+ ||>> Variable.variant_fixes (map (suffix "'") fp_b_names);
val us = map2 (curry Free) us' fpTs;
+ val udiscss = map2 (map o rapp) us discss;
+ val uselsss = map2 (map o map o rapp) us selsss;
- val (coinduct_thms, coinduct_thm) =
+ val vs = map2 (curry Free) vs' fpTs;
+ val vdiscss = map2 (map o rapp) vs discss;
+ val vselsss = map2 (map o map o rapp) vs selsss;
+
+ val ((coinduct_thms, coinduct_thm), (strong_coinduct_thms, strong_coinduct_thm)) =
let
+ val uvrs = map3 (fn r => fn u => fn v => r $ u $ v) rs us vs;
+ val uv_eqs = map2 (curry HOLogic.mk_eq) us vs;
+ val strong_rs =
+ map4 (fn u => fn v => fn uvr => fn uv_eq =>
+ fold_rev Term.lambda [u, v] (HOLogic.mk_disj (uvr, uv_eq))) us vs uvrs uv_eqs;
+
+ fun build_rel_step build_arg (Type (s, Ts)) =
+ let
+ val bnf = the (bnf_of lthy s);
+ val live = live_of_bnf bnf;
+ val rel = mk_rel live Ts Ts (rel_of_bnf bnf);
+ val Ts' = map domain_type (fst (strip_typeN live (fastype_of rel)));
+ in Term.list_comb (rel, map build_arg Ts') end;
+
+ fun build_rel rs' T =
+ (case find_index (curry (op =) T) fpTs of
+ ~1 =>
+ if exists_fp_subtype T then build_rel_step (build_rel rs') T
+ else HOLogic.eq_const T
+ | kk => nth rs' kk);
+
+ fun build_rel_app rs' usel vsel =
+ fold rapp [usel, vsel] (build_rel rs' (fastype_of usel));
+
+ fun mk_prem_ctr_concls rs' n k udisc usels vdisc vsels =
+ (if k = n then [] else [HOLogic.mk_eq (udisc, vdisc)]) @
+ (if null usels then
+ []
+ else
+ [Library.foldr HOLogic.mk_imp (if n = 1 then [] else [udisc, vdisc],
+ Library.foldr1 HOLogic.mk_conj (map2 (build_rel_app rs') usels vsels))]);
+
+ fun mk_prem_concl rs' n udiscs uselss vdiscs vselss =
+ Library.foldr1 HOLogic.mk_conj
+ (flat (map5 (mk_prem_ctr_concls rs' n) (1 upto n) udiscs uselss vdiscs vselss))
+ handle List.Empty => @{term True};
+
+ fun mk_prem rs' uvr u v n udiscs uselss vdiscs vselss =
+ fold_rev Logic.all [u, v] (Logic.mk_implies (HOLogic.mk_Trueprop uvr,
+ HOLogic.mk_Trueprop (mk_prem_concl rs' n udiscs uselss vdiscs vselss)));
+
+ val concl =
+ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
+ (map3 (fn uvr => fn u => fn v => HOLogic.mk_imp (uvr, HOLogic.mk_eq (u, v)))
+ uvrs us vs));
+
+ fun mk_goal rs' =
+ Logic.list_implies (map8 (mk_prem rs') uvrs us vs ns udiscss uselsss vdiscss vselsss,
+ concl);
+
+ val goal = mk_goal rs;
+ val strong_goal = mk_goal strong_rs;
+
+ fun prove dtor_coinduct' goal =
+ Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+ mk_coinduct_tac ctxt nesting_rel_eqs nn ns dtor_coinduct' pre_rel_defs dtor_ctors
+ exhaust_thms ctr_defss disc_thmsss sel_thmsss)
+ |> singleton (Proof_Context.export names_lthy lthy)
+ |> Thm.close_derivation;
+
fun postproc nn thm =
Thm.permute_prems 0 nn
- (if nn = 1 then thm RS mp else funpow nn (fn thm => thm RS @{thm mp_conj}) thm)
- |> Drule.zero_var_indexes;
-
- val coinduct_thm = fp_induct;
+ (if nn = 1 then thm RS mp
+ else funpow nn (fn thm => reassoc_conjs (thm RS mp_conj)) thm)
+ |> Drule.zero_var_indexes
+ |> `(conj_dests nn);
in
- `(conj_dests nn) coinduct_thm
+ (postproc nn (prove fp_induct goal), postproc nn (prove fp_strong_induct strong_goal))
end;
fun mk_maybe_not pos = not pos ? HOLogic.mk_not;
@@ -859,27 +939,28 @@
(Logic.list_implies (seq_conds (HOLogic.mk_Trueprop oo mk_maybe_not) n k cps,
mk_Trueprop_eq (fcorec_like $ c, Term.list_comb (ctr, take m cfs'))));
- fun build_call frec_likes maybe_tack (T, U) =
+ fun build_corec_like fcorec_likes maybe_tack (T, U) =
if T = U then
id_const T
else
(case find_index (curry (op =) U) fpTs of
- ~1 => build_map (build_call frec_likes maybe_tack) T U
- | j => maybe_tack (nth cs j, nth us j) (nth frec_likes j));
+ ~1 => build_map (build_corec_like fcorec_likes maybe_tack) T U
+ | kk => maybe_tack (nth cs kk, nth us kk) (nth fcorec_likes kk));
fun mk_U maybe_mk_sumT =
typ_subst (map2 (fn C => fn fpT => (maybe_mk_sumT fpT C, fpT)) Cs fpTs);
- fun intr_calls frec_likes maybe_mk_sumT maybe_tack cqf =
+ fun intr_corec_likes fcorec_likes maybe_mk_sumT maybe_tack cqf =
let val T = fastype_of cqf in
if exists_subtype (member (op =) Cs) T then
- build_call frec_likes maybe_tack (T, mk_U maybe_mk_sumT T) $ cqf
+ build_corec_like fcorec_likes maybe_tack (T, mk_U maybe_mk_sumT T) $ cqf
else
cqf
end;
- val crgsss' = map (map (map (intr_calls gunfolds (K I) (K I)))) crgsss;
- val cshsss' = map (map (map (intr_calls hcorecs (curry mk_sumT) (tack z)))) cshsss;
+ val crgsss' = map (map (map (intr_corec_likes gunfolds (K I) (K I)))) crgsss;
+ val cshsss' =
+ map (map (map (intr_corec_likes hcorecs (curry mk_sumT) (tack z)))) cshsss;
val unfold_goalss =
map8 (map4 oooo mk_goal pgss) cs cpss gunfolds ns kss ctrss mss crgsss';
@@ -936,8 +1017,8 @@
fun prove goal tac =
Skip_Proof.prove lthy [] [] goal (tac o #context)
- |> Thm.close_derivation
- |> singleton (Proof_Context.export names_lthy no_defs_lthy);
+ |> singleton (Proof_Context.export names_lthy0 no_defs_lthy)
+ |> Thm.close_derivation;
fun proves [_] [_] = []
| proves goals tacs = map2 prove goals tacs;
@@ -983,7 +1064,12 @@
|> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
val common_notes =
- (if nn > 1 then [(coinductN, [coinduct_thm], [])] (* FIXME: attribs *) else [])
+ (if nn > 1 then
+ (* FIXME: attribs *)
+ [(coinductN, [coinduct_thm], []),
+ (strong_coinductN, [strong_coinduct_thm], [])]
+ else
+ [])
|> map (fn (thmN, thms, attrs) =>
((Binding.qualify true fp_common_name (Binding.name thmN), attrs), [(thms, [])]));
@@ -997,6 +1083,7 @@
(sel_unfoldsN, sel_unfold_thmss, simp_attrs),
(sel_corecsN, sel_corec_thmss, simp_attrs),
(simpsN, simp_thmss, []),
+ (strong_coinductN, map single strong_coinduct_thms, []), (* FIXME: attribs *)
(unfoldsN, unfold_thmss, [])]
|> maps (fn (thmN, thmss, attrs) =>
map_filter (fn (_, []) => NONE | (b, thms) =>