--- a/src/HOL/BNF_Fixpoint_Base.thy Tue Oct 21 17:23:12 2014 +0200
+++ b/src/HOL/BNF_Fixpoint_Base.thy Tue Oct 21 17:23:12 2014 +0200
@@ -186,6 +186,16 @@
lemma inj_on_convol_ident: "inj_on (\<lambda>x. (x, f x)) X"
unfolding inj_on_def by simp
+lemma map_sum_if_distrib_then:
+ "\<And>f g e x y. map_sum f g (if e then Inl x else y) = (if e then Inl (f x) else map_sum f g y)"
+ "\<And>f g e x y. map_sum f g (if e then Inr x else y) = (if e then Inr (g x) else map_sum f g y)"
+ by simp_all
+
+lemma map_sum_if_distrib_else:
+ "\<And>f g e x y. map_sum f g (if e then x else Inl y) = (if e then map_sum f g x else Inl (f y))"
+ "\<And>f g e x y. map_sum f g (if e then x else Inr y) = (if e then map_sum f g x else Inr (g y))"
+ by simp_all
+
lemma case_prod_app: "case_prod f x y = case_prod (\<lambda>l r. f l r y) x"
by (case_tac x) simp
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Oct 21 17:23:12 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Oct 21 17:23:12 2014 +0200
@@ -42,7 +42,7 @@
co_rec_selss: thm list list,
co_rec_codes: thm list,
co_rec_transfers: thm list,
- rec_o_maps: thm list,
+ co_rec_o_maps: thm list,
common_rel_co_inducts: thm list,
rel_co_inducts: thm list,
common_set_inducts: thm list,
@@ -176,6 +176,7 @@
val corec_codeN = "corec_code";
val corec_transferN = "corec_transfer";
val map_disc_iffN = "map_disc_iff";
+val map_o_corecN = "map_o_corec";
val map_selN = "map_sel";
val rec_o_mapN = "rec_o_map";
val rec_transferN = "rec_transfer";
@@ -218,7 +219,7 @@
co_rec_selss: thm list list,
co_rec_codes: thm list,
co_rec_transfers: thm list,
- rec_o_maps: thm list,
+ co_rec_o_maps: thm list,
common_rel_co_inducts: thm list,
rel_co_inducts: thm list,
common_set_inducts: thm list,
@@ -257,7 +258,7 @@
set_cases = map (Morphism.thm phi) set_cases};
fun morph_fp_co_induct_sugar phi ({co_rec, common_co_inducts, co_inducts, co_rec_def, co_rec_thms,
- co_rec_discs, co_rec_disc_iffs, co_rec_selss, co_rec_codes, co_rec_transfers, rec_o_maps,
+ co_rec_discs, co_rec_disc_iffs, co_rec_selss, co_rec_codes, co_rec_transfers, co_rec_o_maps,
common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts} : fp_co_induct_sugar) =
{co_rec = Morphism.term phi co_rec,
common_co_inducts = map (Morphism.thm phi) common_co_inducts,
@@ -269,7 +270,7 @@
co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss,
co_rec_codes = map (Morphism.thm phi) co_rec_codes,
co_rec_transfers = map (Morphism.thm phi) co_rec_transfers,
- rec_o_maps = map (Morphism.thm phi) rec_o_maps,
+ co_rec_o_maps = map (Morphism.thm phi) co_rec_o_maps,
common_rel_co_inducts = map (Morphism.thm phi) common_rel_co_inducts,
rel_co_inducts = map (Morphism.thm phi) rel_co_inducts,
common_set_inducts = map (Morphism.thm phi) common_set_inducts,
@@ -352,7 +353,7 @@
rel_distinctss map_disc_iffss map_selsss rel_selss rel_intross rel_casess set_thmss set_selsssss
set_introsssss set_casess ctr_transferss case_transferss disc_transferss co_rec_disc_iffss
co_rec_codess co_rec_transferss common_rel_co_inducts rel_co_inductss common_set_inducts
- set_inductss sel_transferss rec_o_mapss noted =
+ set_inductss sel_transferss co_rec_o_mapss noted =
let
val fp_sugars =
map_index (fn (kk, T) =>
@@ -392,7 +393,7 @@
co_rec_selss = nth co_rec_selsss kk,
co_rec_codes = nth co_rec_codess kk,
co_rec_transfers = nth co_rec_transferss kk,
- rec_o_maps = nth rec_o_mapss kk,
+ co_rec_o_maps = nth co_rec_o_mapss kk,
common_rel_co_inducts = common_rel_co_inducts,
rel_co_inducts = nth rel_co_inductss kk,
common_set_inducts = common_set_inducts,
@@ -2296,8 +2297,8 @@
val rec_o_map_thms =
@{map 3} (fn goal => fn rec_def => fn ctor_rec_o_map =>
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
- ctor_rec_o_map)
+ mk_co_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s
+ abs_inverses ctor_rec_o_map)
|> Thm.close_derivation)
rec_o_map_goals rec_defs xtor_co_rec_o_maps;
in
@@ -2391,6 +2392,66 @@
|> map Thm.close_derivation
end;
+ fun derive_map_o_corec_thmss lthy0 lthy2 corecs corec_defs =
+ if live = 0 then replicate nn []
+ else
+ let
+ fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy0);
+ val maps0 = map map_of_bnf fp_bnfs;
+ val ABs = As ~~ Bs
+ val liveness = map (op <>) ABs;
+ val f_names = variant_names num_As "f";
+ val fs = map2 (curry Free) f_names (map (op -->) ABs);
+ val live_fs = AList.find (op =) (fs ~~ liveness) true;
+
+ val fmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_fs)) maps0;
+
+ val corec_Ts as corec_T1 :: _ = map fastype_of corecs;
+ val corec_arg_Ts = binder_fun_types corec_T1;
+
+ val B_ify = Term.subst_atomic_types (As ~~ Bs);
+ val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
+
+ val num_rec_args = length corec_arg_Ts;
+ val g_names = variant_names num_rec_args "g";
+ val gs = map2 (curry Free) g_names corec_arg_Ts;
+ val gcorecs = map (fn corecx => Term.list_comb (corecx, gs)) corecs;
+
+ val map_o_corec_lhss = map2 (curry HOLogic.mk_comp) fmaps gcorecs;
+
+ val ABgs = ABs ~~ fs;
+
+ fun mk_map_o_corec_arg corec_argB_T g =
+ let
+ val T = range_type (fastype_of g);
+ val U = range_type corec_argB_T;
+ in
+ if T = U then g
+ else HOLogic.mk_comp (build_map lthy2 [] (the o AList.lookup (op =) ABgs) (T, U), g)
+ end;
+
+ fun mk_map_o_corec_rhs corecx =
+ let val args = map2 (mk_map_o_corec_arg o B_ify_T) corec_arg_Ts gs in
+ Term.list_comb (B_ify corecx, args)
+ end;
+
+ val map_o_corec_rhss = map mk_map_o_corec_rhs corecs;
+
+ val map_o_corec_goals =
+ map2 (fold_rev (fold_rev Logic.all) [fs, gs] o HOLogic.mk_Trueprop oo
+ curry HOLogic.mk_eq) map_o_corec_lhss map_o_corec_rhss;
+
+ val map_o_corec_thms =
+ @{map 3} (fn goal => fn corec_def => fn dtor_map_o_corec =>
+ Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} =>
+ mk_co_rec_o_map_tac ctxt corec_def pre_map_defs live_nesting_map_ident0s
+ abs_inverses dtor_map_o_corec)
+ |> Thm.close_derivation)
+ map_o_corec_goals corec_defs xtor_co_rec_o_maps;
+ in
+ map single map_o_corec_thms
+ end;
+
fun derive_note_coinduct_corecs_thms_for_types
((((map_thmss, map_disc_iffss, map_selsss, rel_injectss, rel_distinctss, rel_selss,
rel_intross, rel_casess, set_thmss, set_selsssss, set_introsssss, set_casess,
@@ -2446,6 +2507,8 @@
(rel_coinduct_attrs, common_rel_coinduct_attrs))
end;
+ val map_o_corec_thmss = derive_map_o_corec_thmss lthy lthy corecs corec_defs;
+
val (set_induct_thms, set_induct_attrss) =
derive_set_induct_thms_for_types lthy nn fpTs (map #ctrs ctr_sugars)
(map (map (mk_set As)) (map sets_of_bnf fp_bnfs)) dtor_set_inducts
@@ -2477,6 +2540,7 @@
(corec_disc_iffN, corec_disc_iff_thmss, K corec_disc_iff_attrs),
(corec_selN, corec_sel_thmss, K corec_sel_attrs),
(corec_transferN, corec_transfer_thmss, K []),
+ (map_o_corecN, map_o_corec_thmss, K []),
(rel_coinductN, rel_coinduct_thmss, K (rel_coinduct_attrs @ [coinduct_pred_attr ""])),
(simpsN, simp_thmss, K [])]
|> massage_multi_notes fp_b_names fpTs;
@@ -2493,7 +2557,7 @@
rel_intross rel_casess set_thmss set_selsssss set_introsssss set_casess ctr_transferss
case_transferss disc_transferss corec_disc_iff_thmss (map single corec_code_thms)
corec_transfer_thmss common_rel_coinduct_thms rel_coinduct_thmss set_induct_thms
- (replicate nn (if nn = 1 then set_induct_thms else [])) sel_transferss (replicate nn [])
+ (replicate nn (if nn = 1 then set_induct_thms else [])) sel_transferss map_o_corec_thmss
end;
val lthy'' = lthy'
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Oct 21 17:23:12 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Oct 21 17:23:12 2014 +0200
@@ -19,6 +19,8 @@
thm list list list -> tactic
val mk_corec_tac: thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic
val mk_corec_disc_iff_tac: thm list -> thm list -> thm list -> Proof.context -> tactic
+ val mk_co_rec_o_map_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> thm -> thm ->
+ thm Seq.seq
val mk_corec_transfer_tac: Proof.context -> cterm list -> cterm list -> thm list -> thm list ->
thm list -> thm list -> thm list -> ''a list -> ''a list list -> ''a list list list list ->
''a list list list list -> tactic
@@ -34,8 +36,6 @@
val mk_map_disc_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic
val mk_map_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list ->
thm list -> tactic
- val mk_rec_o_map_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> thm -> thm ->
- thm Seq.seq
val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
tactic
val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list ->
@@ -163,13 +163,14 @@
@{thms comp_def convol_def fst_conv id_def case_prod_Pair_iden snd_conv split_conv
case_unit_Unity} @ sumprod_thms_map;
-fun mk_rec_o_map_tac ctxt rec_def pre_map_defs map_ident0s abs_inverses ctor_rec_o_map =
+fun mk_co_rec_o_map_tac ctxt co_rec_def pre_map_defs map_ident0s abs_inverses xtor_co_rec_o_map =
let
- val rec_o_map_simps =
- @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum case_prod_map_prod id_bnf_def};
+ val rec_o_map_simps = @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum map_sum.simps
+ case_prod_map_prod id_bnf_def map_prod_simp map_sum_if_distrib_then map_sum_if_distrib_else
+ if_distrib[THEN sym]};
in
- HEADGOAL (subst_tac @{context} (SOME [1, 2]) [rec_def] THEN'
- rtac (ctor_rec_o_map RS trans) THEN'
+ HEADGOAL (subst_tac @{context} (SOME [1, 2]) [co_rec_def] THEN'
+ rtac (xtor_co_rec_o_map RS trans) THEN'
CONVERSION Thm.eta_long_conversion THEN'
asm_simp_tac (ss_only (pre_map_defs @ distinct Thm.eq_thm_prop (map_ident0s @ abs_inverses) @
rec_o_map_simps) ctxt))
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Oct 21 17:23:12 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Oct 21 17:23:12 2014 +0200
@@ -297,7 +297,7 @@
fp_bnf_sugar = {map_disc_iffs, map_selss, rel_injects, rel_distincts, rel_sels,
rel_intros, rel_cases, set_thms, set_selssss, set_introssss, set_cases, ...},
fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers,
- rec_o_maps, common_rel_co_inducts, rel_co_inducts, common_set_inducts,
+ co_rec_o_maps, common_rel_co_inducts, rel_co_inducts, common_set_inducts,
set_inducts, ...},
...} : fp_sugar) =
{T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk,
@@ -335,7 +335,7 @@
co_rec_selss = co_rec_sel_thmss,
co_rec_codes = co_rec_codes,
co_rec_transfers = co_rec_transfers,
- rec_o_maps = rec_o_maps,
+ co_rec_o_maps = co_rec_o_maps,
common_rel_co_inducts = common_rel_co_inducts,
rel_co_inducts = rel_co_inducts,
common_set_inducts = common_set_inducts,
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Oct 21 17:23:12 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Oct 21 17:23:12 2014 +0200
@@ -109,7 +109,7 @@
co_rec_selss = [],
co_rec_codes = [],
co_rec_transfers = [],
- rec_o_maps = @{thms case_sum_o_map_sum},
+ co_rec_o_maps = @{thms case_sum_o_map_sum},
common_rel_co_inducts = [],
rel_co_inducts = [],
common_set_inducts = [],
@@ -175,7 +175,7 @@
co_rec_selss = [],
co_rec_codes = [],
co_rec_transfers = [],
- rec_o_maps = @{thms case_prod_o_map_prod},
+ co_rec_o_maps = @{thms case_prod_o_map_prod},
common_rel_co_inducts = [],
rel_co_inducts = [],
common_set_inducts = [],
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Oct 21 17:23:12 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Oct 21 17:23:12 2014 +0200
@@ -285,7 +285,8 @@
curry Logic.list_implies size_o_map_conds o HOLogic.mk_Trueprop oo
curry HOLogic.mk_eq) size_o_map_lhss size_o_map_rhss;
- val rec_o_maps = fold_rev (curry (op @) o (#rec_o_maps o #fp_co_induct_sugar)) fp_sugars [];
+ val rec_o_maps =
+ fold_rev (curry (op @) o (#co_rec_o_maps o #fp_co_induct_sugar)) fp_sugars [];
val size_o_map_thmss =
if nested_size_o_maps_complete then