--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Feb 17 17:08:03 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Feb 17 17:08:36 2016 +0100
@@ -27,6 +27,7 @@
rel_sels: thm list,
rel_intros: thm list,
rel_cases: thm list,
+ pred_injects: thm list,
set_thms: thm list,
set_selssss: thm list list list list,
set_introssss: thm list list list list,
@@ -195,6 +196,7 @@
val map_disc_iffN = "map_disc_iff";
val map_o_corecN = "map_o_corec";
val map_selN = "map_sel";
+val pred_injectN = "pred_inject";
val rec_o_mapN = "rec_o_map";
val rec_transferN = "rec_transfer";
val set_casesN = "set_cases";
@@ -221,6 +223,7 @@
rel_sels: thm list,
rel_intros: thm list,
rel_cases: thm list,
+ pred_injects: thm list,
set_thms: thm list,
set_selssss: thm list list list list,
set_introssss: thm list list list list,
@@ -265,7 +268,7 @@
fun strong_co_induct_of [_, s] = s;
fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, map_selss, rel_injects, rel_distincts,
- rel_sels, rel_intros, rel_cases, set_thms, set_selssss, set_introssss,
+ rel_sels, rel_intros, rel_cases, pred_injects, set_thms, set_selssss, set_introssss,
set_cases} : fp_bnf_sugar) =
{map_thms = map (Morphism.thm phi) map_thms,
map_disc_iffs = map (Morphism.thm phi) map_disc_iffs,
@@ -275,6 +278,7 @@
rel_sels = map (Morphism.thm phi) rel_sels,
rel_intros = map (Morphism.thm phi) rel_intros,
rel_cases = map (Morphism.thm phi) rel_cases,
+ pred_injects = map (Morphism.thm phi) pred_injects,
set_thms = map (Morphism.thm phi) set_thms,
set_selssss = map (map (map (map (Morphism.thm phi)))) set_selssss,
set_introssss = map (map (map (map (Morphism.thm phi)))) set_introssss,
@@ -369,10 +373,10 @@
fun interpret_bnfs_register_fp_sugars plugins Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs
live_nesting_bnfs fp_res ctrXs_Tsss ctor_iff_dtors ctr_defss ctr_sugars co_recs co_rec_defs
map_thmss common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss
- 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 co_rec_o_mapss noted =
+ rel_distinctss map_disc_iffss map_selsss rel_selss rel_intross rel_casess pred_injectss
+ 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 co_rec_o_mapss noted =
let
val fp_sugars =
map_index (fn (kk, T) =>
@@ -398,6 +402,7 @@
rel_sels = nth rel_selss kk,
rel_intros = nth rel_intross kk,
rel_cases = nth rel_casess kk,
+ pred_injects = nth pred_injectss kk,
set_thms = nth set_thmss kk,
set_selssss = nth set_selsssss kk,
set_introssss = nth set_introsssss kk,
@@ -566,10 +571,10 @@
b_names Ts thmss)
#> filter_out (null o fst o hd o snd);
-fun derive_map_set_rel_thms plugins fp live As Bs C E abs_inverses ctr_defs' fp_nesting_set_maps
- live_nesting_map_id0s live_nesting_set_maps live_nesting_rel_eqs fp_b_name fp_bnf fpT ctor
- ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm
- ctr_Tss abs
+fun derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs'
+ fp_nesting_set_maps fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps
+ live_nesting_rel_eqs live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor ctor_dtor
+ dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs
({casex, case_thms, discs, selss, sel_defs, ctrs, exhaust, exhaust_discs, disc_thmss, sel_thmss,
injects, distincts, distinct_discsss, ...} : ctr_sugar)
lthy =
@@ -582,13 +587,15 @@
val fpBT = B_ify_T fpT;
val live_AsBs = filter (op <>) (As ~~ Bs);
+ val live_As = map fst live_AsBs;
val fTs = map (op -->) live_AsBs;
- val (((((((xss, yss), fs), Rs), ta), tb), thesis), names_lthy) = lthy
+ val ((((((((xss, yss), fs), Ps), Rs), ta), tb), thesis), names_lthy) = lthy
|> fold (fold Variable.declare_typ) [As, Bs]
|> mk_Freess "x" ctr_Tss
||>> mk_Freess "y" (map (map B_ify_T) ctr_Tss)
||>> mk_Frees "f" fTs
+ ||>> mk_Frees "P" (map mk_pred1T live_As)
||>> mk_Frees "R" (map (uncurry mk_pred2T) live_AsBs)
||>> yield_singleton (mk_Frees "a") fpT
||>> yield_singleton (mk_Frees "b") fpBT
@@ -597,7 +604,7 @@
val ctrAs = map (mk_ctr As) ctrs;
val ctrBs = map (mk_ctr Bs) ctrs;
- fun derive_rel_cases relAsBs rel_inject_thms rel_distinct_thms =
+ fun derive_rel_case relAsBs rel_inject_thms rel_distinct_thms =
let
val rel_Rs_a_b = list_comb (relAsBs, Rs) $ ta $ tb;
@@ -622,13 +629,13 @@
val goal = Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms, thesis);
in
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
- mk_rel_cases_tac ctxt (Thm.cterm_of ctxt ta) (Thm.cterm_of ctxt tb) exhaust injects
+ mk_rel_case_tac ctxt (Thm.cterm_of ctxt ta) (Thm.cterm_of ctxt tb) exhaust injects
rel_inject_thms distincts rel_distinct_thms live_nesting_rel_eqs)
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
end;
- fun derive_case_transfer rel_cases_thm =
+ fun derive_case_transfer rel_case_thm =
let
val (S, names_lthy) = yield_singleton (mk_Frees "S") (mk_pred2T C E) names_lthy;
val caseA = mk_case As C casex;
@@ -636,7 +643,7 @@
val goal = mk_parametricity_goal names_lthy (S :: Rs) caseA caseB;
in
Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
- mk_case_transfer_tac ctxt rel_cases_thm case_thms)
+ mk_case_transfer_tac ctxt rel_case_thm case_thms)
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation
end;
@@ -645,9 +652,9 @@
if plugins transfer_plugin then
let
val relAsBs = HOLogic.eq_const fpT;
- val rel_cases_thm = derive_rel_cases relAsBs [] [];
-
- val case_transfer_thm = derive_case_transfer rel_cases_thm;
+ val rel_case_thm = derive_rel_case relAsBs [] [];
+
+ val case_transfer_thm = derive_case_transfer rel_case_thm;
val notes =
[(case_transferN, [case_transfer_thm], K [])]
@@ -658,11 +665,11 @@
val subst = Morphism.thm (substitute_noted_thm noted);
in
- (([], [], [], [], [], [], [], [], [], [], [], [], [], [subst case_transfer_thm], [], []),
- lthy')
+ (([], [], [], [], [], [], [], [], [], [], [], [], [], [], [subst case_transfer_thm], [],
+ []), lthy')
end
else
- (([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], []), lthy)
+ (([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], []), lthy)
else
let
val mapx = mk_map live As Bs (map_of_bnf fp_bnf);
@@ -891,7 +898,8 @@
(map (rapp ta) selAs) (map (rapp tb) selBs)))]);
val goals =
- if n = 0 then []
+ if n = 0 then
+ []
else
[mk_Trueprop_eq (build_rel_app names_lthy Rs [] ta tb,
(case flat (@{map 5} (mk_conjunct n) (1 upto n) discAs selAss discBs selBss) of
@@ -909,9 +917,9 @@
map prove goals
end;
- val (rel_cases_thm, rel_cases_attrs) =
+ val (rel_case_thm, rel_case_attrs) =
let
- val thm = derive_rel_cases relAsBs rel_inject_thms rel_distinct_thms;
+ val thm = derive_rel_case relAsBs rel_inject_thms rel_distinct_thms;
val ctr_names = quasi_unambiguous_case_names (map name_of_ctr ctrAs);
val case_names_attr = Attrib.internal (K (Rule_Cases.case_names ctr_names));
val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
@@ -920,16 +928,18 @@
(thm, [consumes_attr, case_names_attr, cases_pred_attr ""])
end;
- val case_transfer_thm = derive_case_transfer rel_cases_thm;
+ val case_transfer_thm = derive_case_transfer rel_case_thm;
val sel_transfer_thms =
- if null selAss then []
+ if null selAss then
+ []
else
let
val shared_sels = foldl1 (uncurry (inter (op =))) (map (op ~~) (selAss ~~ selBss));
val goals = map (uncurry (mk_parametricity_goal names_lthy Rs)) shared_sels;
in
- if null goals then []
+ if null goals then
+ []
else
let
val goal = Logic.mk_conjunction_balanced goals;
@@ -1092,6 +1102,51 @@
end)
end;
+ val pred_injects =
+ let
+ fun top_sweep_rewr_conv rewrs =
+ Conv.top_sweep_conv (K (Conv.rewrs_conv rewrs)) @{context};
+
+ val rel_eq_onp_with_tops_of = Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv
+ (top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})));
+
+ val eq_onps = map (rel_eq_onp_with_tops_of)
+ (map rel_eq_onp_of_bnf fp_bnfs @ fp_nesting_rel_eq_onps @ live_nesting_rel_eq_onps);
+ val cTs = map (SOME o Thm.ctyp_of lthy) (maps (replicate 2) live_As);
+ val cts = map (SOME o Thm.cterm_of lthy) (map mk_eq_onp Ps);
+
+ val get_rhs = Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq #> snd;
+
+ val pred_eq_onp_conj =
+ List.foldr (fn (_, thm) => thm RS @{thm eq_onp_live_step}) @{thm refl[of True]};
+
+ fun predify_rel_inject rel_inject =
+ let
+ val conjuncts = try (get_rhs #> HOLogic.dest_conj) rel_inject |> the_default [];
+
+ fun postproc thm =
+ if conjuncts <> [] then
+ @{thm box_equals} OF [thm, @{thm eq_onp_same_args},
+ pred_eq_onp_conj conjuncts |> unfold_thms lthy @{thms simp_thms(21)}]
+ else
+ thm RS (@{thm eq_onp_same_args} RS iffD1);
+ in
+ rel_inject
+ |> Thm.instantiate' cTs cts
+ |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv
+ (Raw_Simplifier.rewrite lthy false
+ @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]})))
+ |> unfold_thms lthy eq_onps
+ |> postproc
+ |> unfold_thms lthy @{thms top_conj}
+ end;
+ in
+ rel_inject_thms
+ |> map (unfold_thms lthy [@{thm conj_assoc}])
+ |> map predify_rel_inject
+ |> Proof_Context.export names_lthy lthy
+ end;
+
val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else [];
val anonymous_notes =
@@ -1106,7 +1161,8 @@
(mapN, map_thms, K (code_attrs @ nitpicksimp_attrs @ simp_attrs)),
(map_disc_iffN, map_disc_iff_thms, K simp_attrs),
(map_selN, map_sel_thms, K []),
- (rel_casesN, [rel_cases_thm], K rel_cases_attrs),
+ (pred_injectN, pred_injects, K simp_attrs),
+ (rel_casesN, [rel_case_thm], K rel_case_attrs),
(rel_distinctN, rel_distinct_thms, K simp_attrs),
(rel_injectN, rel_inject_thms, K simp_attrs),
(rel_introsN, rel_intro_thms, K []),
@@ -1133,7 +1189,8 @@
map subst rel_distinct_thms,
map subst rel_sel_thms,
map subst rel_intro_thms,
- [subst rel_cases_thm],
+ [subst rel_case_thm],
+ map subst pred_injects,
map subst set_thms,
map (map (map (map subst))) set_sel_thmssss,
map (map (map (map subst))) set_intros_thmssss,
@@ -2143,10 +2200,12 @@
val pre_set_defss = map set_defs_of_bnf pre_bnfs;
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 fp_nesting_rel_eq_onps = map rel_eq_onp_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;
+ val live_nesting_rel_eq_onps = map rel_eq_onp_of_bnf live_nesting_bnfs;
val live = live_of_bnf any_fp_bnf;
val _ =
@@ -2287,10 +2346,11 @@
in
(wrap_ctrs
#> (fn (ctr_sugar, lthy) =>
- derive_map_set_rel_thms plugins fp live As Bs C E abs_inverses ctr_defs'
- fp_nesting_set_maps live_nesting_map_id0s live_nesting_set_maps live_nesting_rel_eqs
- fp_b_name fp_bnf fpT ctor ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def
- fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs ctr_sugar lthy
+ derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs'
+ fp_nesting_set_maps fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps
+ live_nesting_rel_eqs live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor
+ ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms
+ fp_rel_thm ctr_Tss abs ctr_sugar lthy
|>> pair ctr_sugar)
##>>
(if fp = Least_FP then define_rec (the recs_args_types) mk_binding fpTs Cs reps
@@ -2298,9 +2358,9 @@
#> massage_res, lthy')
end;
- fun wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types (wrap_one_etc, lthy) =
+ fun wrap_ctrs_derive_map_set_rel_pred_thms_define_co_rec_for_types (wrap_one_etc, lthy) =
fold_map I wrap_one_etc lthy
- |>> apsnd split_list o apfst (apsnd @{split_list 5} o apfst @{split_list 16} o split_list)
+ |>> apsnd split_list o apfst (apsnd @{split_list 5} o apfst @{split_list 17} o split_list)
o split_list;
fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects
@@ -2337,7 +2397,8 @@
end;
fun derive_rec_o_map_thmss lthy recs rec_defs =
- if live = 0 then replicate nn []
+ if live = 0 then
+ replicate nn []
else
let
fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy);
@@ -2404,7 +2465,7 @@
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,
+ rel_intross, rel_casess, pred_injectss, set_thmss, set_selsssss, set_introsssss,
set_casess, ctr_transferss, case_transferss, disc_transferss, sel_transferss),
(ctrss, _, ctor_iff_dtors, ctr_defss, ctr_sugars)),
(recs, rec_defs)), lthy) =
@@ -2468,10 +2529,10 @@
fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctor_iff_dtors ctr_defss ctr_sugars
recs rec_defs map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn [])
(replicate nn []) rel_injectss 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 (replicate nn []) (replicate nn []) rec_transfer_thmss
- common_rel_induct_thms rel_induct_thmss [] (replicate nn []) sel_transferss
- rec_o_map_thmss
+ rel_intross rel_casess pred_injectss 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 =
@@ -2491,7 +2552,8 @@
end;
fun derive_map_o_corec_thmss lthy0 lthy2 corecs corec_defs =
- if live = 0 then replicate nn []
+ if live = 0 then
+ replicate nn []
else
let
fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy0);
@@ -2551,8 +2613,8 @@
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,
- ctr_transferss, case_transferss, disc_transferss, sel_transferss),
+ rel_intross, rel_casess, pred_injectss, set_thmss, set_selsssss, set_introsssss,
+ set_casess, ctr_transferss, case_transferss, disc_transferss, sel_transferss),
(_, _, ctor_iff_dtors, ctr_defss, ctr_sugars)),
(corecs, corec_defs)), lthy) =
let
@@ -2647,10 +2709,11 @@
corecs corec_defs map_thmss [coinduct_thm, coinduct_strong_thm]
(transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss
corec_sel_thmsss rel_injectss 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 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 map_o_corec_thmss
+ rel_intross rel_casess pred_injectss 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 map_o_corec_thmss
end;
val lthy'' = lthy'
@@ -2659,7 +2722,7 @@
xtor_co_recs ctor_dtors dtor_ctors ctor_injects pre_map_defs pre_set_defss pre_rel_defs
xtor_maps xtor_setss xtor_rels ns kss mss abss abs_injects type_definitions ctr_bindingss
ctr_mixfixess ctr_Tsss disc_bindingss sel_bindingsss raw_sel_default_eqss
- |> wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types
+ |> wrap_ctrs_derive_map_set_rel_pred_thms_define_co_rec_for_types
|> case_fp fp derive_note_induct_recs_thms_for_types
derive_note_coinduct_corecs_thms_for_types;