--- a/src/HOL/BNF_Fixpoint_Base.thy Tue Oct 21 17:23:10 2014 +0200
+++ b/src/HOL/BNF_Fixpoint_Base.thy Tue Oct 21 17:23:11 2014 +0200
@@ -199,6 +199,9 @@
lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x"
by (case_tac x) simp+
+lemma case_prod_o_map_prod: "case_prod f \<circ> map_prod g1 g2 = case_prod (\<lambda>l r. f (g1 l) (g2 r))"
+ unfolding comp_def by auto
+
lemma case_prod_transfer:
"(rel_fun (rel_fun A (rel_fun B C)) (rel_fun (rel_prod A B) C)) case_prod case_prod"
unfolding rel_fun_def rel_prod_def by simp
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Oct 21 17:23:10 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Oct 21 17:23:11 2014 +0200
@@ -42,6 +42,7 @@
co_rec_selss: thm list list,
co_rec_codes: thm list,
co_rec_transfers: thm list,
+ rec_o_maps: thm list,
common_rel_co_inducts: thm list,
rel_co_inducts: thm list,
common_set_inducts: thm list,
@@ -176,6 +177,7 @@
val corec_transferN = "corec_transfer";
val map_disc_iffN = "map_disc_iff";
val map_selN = "map_sel";
+val rec_o_mapN = "rec_o_map";
val rec_transferN = "rec_transfer";
val set_casesN = "set_cases";
val set_introsN = "set_intros";
@@ -216,6 +218,7 @@
co_rec_selss: thm list list,
co_rec_codes: thm list,
co_rec_transfers: thm list,
+ rec_o_maps: thm list,
common_rel_co_inducts: thm list,
rel_co_inducts: thm list,
common_set_inducts: thm list,
@@ -254,7 +257,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,
+ co_rec_discs, co_rec_disc_iffs, co_rec_selss, co_rec_codes, co_rec_transfers, 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,
@@ -266,6 +269,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,
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,
@@ -348,7 +352,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 noted =
+ set_inductss sel_transferss rec_o_mapss noted =
let
val fp_sugars =
map_index (fn (kk, T) =>
@@ -388,6 +392,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,
common_rel_co_inducts = common_rel_co_inducts,
rel_co_inducts = nth rel_co_inductss kk,
common_set_inducts = common_set_inducts,
@@ -1999,7 +2004,7 @@
dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors,
ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_setss, xtor_rels,
xtor_co_rec_thms, xtor_rel_co_induct, dtor_set_inducts,
- xtor_co_rec_transfers, ...},
+ xtor_co_rec_transfers, xtor_co_rec_o_maps, ...},
lthy)) =
fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As)
(map dest_TFree killed_As) fp_eqs no_defs_lthy
@@ -2048,6 +2053,7 @@
val pre_rel_defs = map rel_def_of_bnf pre_bnfs;
val fp_nesting_set_maps = maps set_map_of_bnf fp_nesting_bnfs;
val live_nesting_map_id0s = map map_id0_of_bnf live_nesting_bnfs;
+ val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs;
val live_nesting_set_maps = maps set_map_of_bnf live_nesting_bnfs;
val live_nesting_rel_eqs = map rel_eq_of_bnf live_nesting_bnfs;
@@ -2064,6 +2070,7 @@
(liveness_of_fp_bnf num_As any_fp_bnf) As Bs0;
val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
+ val live_AsBs = filter (op <>) (As ~~ Bs);
val ctors = map (mk_ctor As) ctors0;
val dtors = map (mk_dtor As) dtors0;
@@ -2208,11 +2215,10 @@
fun mk_co_rec_transfer_goals lthy co_recs =
let
- val liveAsBs = filter (op <>) (As ~~ Bs);
- val B_ify = Term.subst_atomic_types (liveAsBs @ (Cs ~~ Es));
+ val B_ify = Term.subst_atomic_types (live_AsBs @ (Cs ~~ Es));
val ((Rs, Ss), names_lthy) = lthy
- |> mk_Frees "R" (map (uncurry mk_pred2T) liveAsBs)
+ |> mk_Frees "R" (map (uncurry mk_pred2T) live_AsBs)
||>> mk_Frees "S" (map2 mk_pred2T Cs Es);
val co_recBs = map B_ify co_recs;
@@ -2231,6 +2237,73 @@
|> map Thm.close_derivation
end;
+ fun derive_rec_o_map_thmss lthy recs rec_defs =
+ if live = 0 then replicate nn []
+ else
+ let
+ fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy);
+
+ 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_gs = AList.find (op =) (fs ~~ liveness) true;
+
+ val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0;
+
+ val rec_Ts as rec_T1 :: _ = map fastype_of recs;
+ val rec_arg_Ts = binder_fun_types rec_T1;
+
+ val B_ify_T = Term.typ_subst_atomic (As ~~ Bs);
+
+ val num_rec_args = length rec_arg_Ts;
+ val g_Ts = map B_ify_T rec_arg_Ts;
+ val g_names = variant_names num_rec_args "g";
+ val gs = map2 (curry Free) g_names g_Ts;
+ val grecs = map (fn recx => Term.list_comb (Term.map_types B_ify_T recx, gs)) recs;
+
+ val rec_o_map_lhss = map2 (curry HOLogic.mk_comp) grecs gmaps;
+
+ val ABfs = ABs ~~ fs;
+
+ fun mk_rec_arg_arg (x as Free (_, T)) =
+ let val U = B_ify_T T in
+ if T = U then x else build_map lthy [] (the o AList.lookup (op =) ABfs) (T, U) $ x
+ end;
+
+ fun mk_rec_o_map_arg rec_arg_T h =
+ let
+ val x_Ts = binder_types rec_arg_T;
+ val m = length x_Ts;
+ val x_names = variant_names m "x";
+ val xs = map2 (curry Free) x_names x_Ts;
+ val xs' = map mk_rec_arg_arg xs;
+ in
+ fold_rev Term.lambda xs (Term.list_comb (h, xs'))
+ end;
+
+ fun mk_rec_o_map_rhs recx =
+ let val args = map2 mk_rec_o_map_arg rec_arg_Ts gs in
+ Term.list_comb (recx, args)
+ end;
+
+ val rec_o_map_rhss = map mk_rec_o_map_rhs recs;
+
+ val rec_o_map_goals =
+ map2 (fold_rev (fold_rev Logic.all) [fs, gs] o HOLogic.mk_Trueprop oo
+ curry HOLogic.mk_eq) rec_o_map_lhss rec_o_map_rhss;
+ 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)
+ |> Thm.close_derivation)
+ rec_o_map_goals rec_defs xtor_co_rec_o_maps;
+ in
+ map single rec_o_map_thms
+ end;
+
fun derive_note_induct_recs_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,
@@ -2265,6 +2338,8 @@
(rel_induct_attrs, rel_induct_attrs))
end;
+ val rec_o_map_thmss = derive_rec_o_map_thmss lthy recs rec_defs;
+
val simp_thmss =
@{map 6} mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss set_thmss;
@@ -2279,6 +2354,7 @@
val notes =
[(inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]),
(recN, rec_thmss, K rec_attrs),
+ (rec_o_mapN, rec_o_map_thmss, K []),
(rec_transferN, rec_transfer_thmss, K []),
(rel_inductN, rel_induct_thmss, K (rel_induct_attrs @ [induct_pred_attr ""])),
(simpsN, simp_thmss, K [])]
@@ -2297,6 +2373,7 @@
rel_intross rel_casess set_thmss set_selsssss set_introsssss set_casess ctr_transferss
case_transferss disc_transferss (replicate nn []) (replicate nn []) rec_transfer_thmss
common_rel_induct_thms rel_induct_thmss [] (replicate nn []) sel_transferss
+ rec_o_map_thmss
end;
fun derive_corec_transfer_thms lthy corecs corec_defs =
@@ -2416,7 +2493,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 (if nn = 1 then set_induct_thms else [])) sel_transferss (replicate nn [])
end;
val lthy'' = lthy'
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Oct 21 17:23:10 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Oct 21 17:23:11 2014 +0200
@@ -34,6 +34,8 @@
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 ->
@@ -161,6 +163,18 @@
@{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 =
+ 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};
+ in
+ HEADGOAL (subst_tac @{context} (SOME [1, 2]) [rec_def] THEN'
+ rtac (ctor_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))
+ end;
+
fun mk_rec_tac pre_map_defs map_ident0s rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt =
HEADGOAL ((if is_def_looping ctr_def then subst_tac ctxt NONE
else SELECT_GOAL o unfold_thms_tac ctxt) [ctr_def]) THEN
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Oct 21 17:23:10 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Oct 21 17:23:11 2014 +0200
@@ -297,7 +297,8 @@
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,
- common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts, ...},
+ 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,
pre_bnf = pre_bnf, fp_bnf = nth (#bnfs fp_res) kk, absT_info = absT_info,
@@ -334,6 +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,
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:10 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Oct 21 17:23:11 2014 +0200
@@ -109,6 +109,7 @@
co_rec_selss = [],
co_rec_codes = [],
co_rec_transfers = [],
+ rec_o_maps = @{thms case_sum_o_map_sum},
common_rel_co_inducts = [],
rel_co_inducts = [],
common_set_inducts = [],
@@ -174,6 +175,7 @@
co_rec_selss = [],
co_rec_codes = [],
co_rec_transfers = [],
+ 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:10 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Oct 21 17:23:11 2014 +0200
@@ -22,8 +22,6 @@
open BNF_FP_Def_Sugar
val size_N = "size_";
-
-val rec_o_mapN = "rec_o_map";
val sizeN = "size";
val size_o_mapN = "size_o_map";
@@ -62,14 +60,6 @@
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};
-fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
- ctor_rec_o_map =
- HEADGOAL (subst_tac @{context} (SOME [1, 2]) [rec_def] THEN' rtac (ctor_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 (live_nesting_map_ident0s @ abs_inverses) @ rec_o_map_simps)
- ctxt));
-
val size_o_map_simps = @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};
fun mk_size_o_map_tac ctxt size_def rec_o_map inj_maps size_maps =
@@ -271,63 +261,12 @@
val maps0 = map map_of_bnf fp_bnfs;
- val (rec_o_map_thmss, size_o_map_thmss) =
- if live = 0 then
- `I (replicate nn [])
+ val size_o_map_thmss =
+ if live = 0 then replicate nn []
else
let
- val pre_bnfs = map #pre_bnf fp_sugars;
- val pre_map_defs = map map_def_of_bnf pre_bnfs;
- val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs;
- val abs_inverses = map (#abs_inverse o #absT_info) fp_sugars;
- val rec_defs = map (#co_rec_def o #fp_co_induct_sugar) fp_sugars;
-
val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0;
- val num_rec_args = length rec_arg_Ts;
- val h_Ts = map B_ify rec_arg_Ts;
- val h_names = variant_names num_rec_args "h";
- val hs = map2 (curry Free) h_names h_Ts;
- val hrecs = map (fn recx => Term.list_comb (Term.map_types B_ify recx, hs)) recs;
-
- val rec_o_map_lhss = map2 (curry HOLogic.mk_comp) hrecs gmaps;
-
- val ABgs = ABs ~~ gs;
-
- fun mk_rec_arg_arg (x as Free (_, T)) =
- let val U = B_ify T in
- if T = U then x else build_map lthy2 [] (the o AList.lookup (op =) ABgs) (T, U) $ x
- end;
-
- fun mk_rec_o_map_arg rec_arg_T h =
- let
- val x_Ts = binder_types rec_arg_T;
- val m = length x_Ts;
- val x_names = variant_names m "x";
- val xs = map2 (curry Free) x_names x_Ts;
- val xs' = map mk_rec_arg_arg xs;
- in
- fold_rev Term.lambda xs (Term.list_comb (h, xs'))
- end;
-
- fun mk_rec_o_map_rhs recx =
- let val args = map2 mk_rec_o_map_arg rec_arg_Ts hs in
- Term.list_comb (recx, args)
- end;
-
- val rec_o_map_rhss = map mk_rec_o_map_rhs recs;
-
- val rec_o_map_goals =
- map2 (fold_rev (fold_rev Logic.all) [gs, hs] o HOLogic.mk_Trueprop oo
- curry HOLogic.mk_eq) rec_o_map_lhss rec_o_map_rhss;
- val rec_o_map_thms =
- @{map 3} (fn goal => fn rec_def => fn ctor_rec_o_map =>
- Goal.prove_sorry lthy2 [] [] 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)
- |> Thm.close_derivation)
- rec_o_map_goals rec_defs ctor_rec_o_maps;
-
val size_o_map_conds =
if exists (can Logic.dest_implies o Thm.prop_of) nested_size_o_maps then
map (HOLogic.mk_Trueprop o mk_inj) live_gs
@@ -346,6 +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 size_o_map_thmss =
if nested_size_o_maps_complete then
@{map 3} (fn goal => fn size_def => fn rec_o_map =>
@@ -353,11 +294,11 @@
mk_size_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps)
|> Thm.close_derivation
|> single)
- size_o_map_goals size_defs rec_o_map_thms
+ size_o_map_goals size_defs rec_o_maps
else
replicate nn [];
in
- (map single rec_o_map_thms, size_o_map_thmss)
+ size_o_map_thmss
end;
(* Ideally, the "[code]" attribute would be generated only if the "code" plugin is enabled. *)
@@ -372,8 +313,7 @@
#> filter_out (null o fst o hd o snd);
val notes =
- [(rec_o_mapN, rec_o_map_thmss, []),
- (sizeN, size_thmss, code_attrs :: nitpicksimp_attrs @ simp_attrs),
+ [(sizeN, size_thmss, code_attrs :: nitpicksimp_attrs @ simp_attrs),
(size_o_mapN, size_o_map_thmss, [])]
|> massage_multi_notes;