--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Feb 15 12:48:10 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Feb 15 13:30:04 2016 +0100
@@ -10,6 +10,7 @@
sig
type fp_ctr_sugar =
{ctrXs_Tss: typ list list,
+ ctor_iff_dtor: thm,
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
ctr_transfers: thm list,
@@ -181,9 +182,10 @@
open BNF_FP_Util
open BNF_FP_Def_Sugar_Tactics
-val EqN = "Eq_";
+val Eq_prefix = "Eq_";
val case_transferN = "case_transfer";
+val ctor_iff_dtorN = "ctor_iff_dtor";
val ctr_transferN = "ctr_transfer";
val disc_transferN = "disc_transfer";
val sel_transferN = "sel_transfer";
@@ -201,6 +203,7 @@
type fp_ctr_sugar =
{ctrXs_Tss: typ list list,
+ ctor_iff_dtor: thm,
ctr_defs: thm list,
ctr_sugar: Ctr_Sugar.ctr_sugar,
ctr_transfers: thm list,
@@ -295,9 +298,10 @@
common_set_inducts = map (Morphism.thm phi) common_set_inducts,
set_inducts = map (Morphism.thm phi) set_inducts};
-fun morph_fp_ctr_sugar phi ({ctrXs_Tss, ctr_defs, ctr_sugar, ctr_transfers, case_transfers,
- disc_transfers, sel_transfers} : fp_ctr_sugar) =
+fun morph_fp_ctr_sugar phi ({ctrXs_Tss, ctor_iff_dtor, ctr_defs, ctr_sugar, ctr_transfers,
+ case_transfers, disc_transfers, sel_transfers} : fp_ctr_sugar) =
{ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
+ ctor_iff_dtor = Morphism.thm phi ctor_iff_dtor,
ctr_defs = map (Morphism.thm phi) ctr_defs,
ctr_sugar = morph_ctr_sugar phi ctr_sugar,
ctr_transfers = map (Morphism.thm phi) ctr_transfers,
@@ -364,8 +368,8 @@
register_fp_sugars_raw fp_sugars #> interpret_fp_sugars plugins fp_sugars;
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 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
+ 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
@@ -379,6 +383,7 @@
fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
fp_ctr_sugar =
{ctrXs_Tss = nth ctrXs_Tsss kk,
+ ctor_iff_dtor = nth ctor_iff_dtors kk,
ctr_defs = nth ctr_defss kk,
ctr_sugar = nth ctr_sugars kk,
ctr_transfers = nth ctr_transferss kk,
@@ -1542,7 +1547,7 @@
flat (map2 append disc_concls ctr_concls)
end;
- val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names);
+ val coinduct_cases = quasi_unambiguous_case_names (map (prefix Eq_prefix) fp_b_names);
val coinduct_conclss =
@{map 3} (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss;
@@ -2190,6 +2195,19 @@
val u = Free (u', fpT);
+ val ctor_iff_dtor_thm =
+ let
+ val goal =
+ fold_rev Logic.all [w, u]
+ (mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w)));
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} =>
+ mk_ctor_iff_dtor_tac ctxt (map (SOME o Thm.ctyp_of lthy) [ctr_absT, fpT])
+ (Thm.cterm_of lthy ctor) (Thm.cterm_of lthy dtor) ctor_dtor dtor_ctor)
+ |> Thm.close_derivation
+ end;
+
val ctr_rhss =
map2 (fn k => fn xs => fold_rev Term.lambda xs (ctor $ mk_absumprod ctr_absT abs n k xs))
ks xss;
@@ -2213,26 +2231,11 @@
fun wrap_ctrs lthy =
let
+ val sumEN_thm' =
+ unfold_thms lthy @{thms unit_all_eq1} (mk_absumprodE type_definition ms);
+
fun exhaust_tac {context = ctxt, prems = _} =
- let
- val ctor_iff_dtor_thm =
- let
- val goal =
- fold_rev Logic.all [w, u]
- (mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w)));
- val vars = Variable.add_free_names lthy goal [];
- in
- Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} =>
- mk_ctor_iff_dtor_tac ctxt (map (SOME o Thm.ctyp_of lthy) [ctr_absT, fpT])
- (Thm.cterm_of lthy ctor) (Thm.cterm_of lthy dtor) ctor_dtor dtor_ctor)
- |> Thm.close_derivation
- end;
-
- val sumEN_thm' =
- unfold_thms lthy @{thms unit_all_eq1} (mk_absumprodE type_definition ms);
- in
- mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor_thm sumEN_thm'
- end;
+ mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor_thm sumEN_thm';
val inject_tacss =
map2 (fn ctr_def => fn 0 => [] | _ => [fn {context = ctxt, ...} =>
@@ -2264,14 +2267,22 @@
val anonymous_notes =
[([case_cong], fundefcong_attrs)]
|> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])]));
+
+ val notes =
+ if Config.get lthy' bnf_internals then
+ [(ctor_iff_dtorN, [ctor_iff_dtor_thm], K [])]
+ |> massage_simple_notes fp_b_name
+ else
+ [];
in
- (ctr_sugar, lthy' |> Local_Theory.notes anonymous_notes |> snd)
+ (ctr_sugar, lthy' |> Local_Theory.notes (anonymous_notes @ notes) |> snd)
end;
fun mk_binding pre = Binding.qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b);
fun massage_res (((ctr_sugar, maps_sets_rels), co_rec_res), lthy) =
- (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_rec_res), lthy);
+ (((maps_sets_rels, (ctrs, xss, ctor_iff_dtor_thm, ctr_defs, ctr_sugar)), co_rec_res),
+ lthy);
in
(wrap_ctrs
#> (fn (ctr_sugar, lthy) =>
@@ -2288,7 +2299,7 @@
fun wrap_ctrs_derive_map_set_rel_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 4} o apfst @{split_list 16} o split_list)
+ |>> apsnd split_list o apfst (apsnd @{split_list 5} o apfst @{split_list 16} o split_list)
o split_list;
fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects
@@ -2394,7 +2405,7 @@
((((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),
- (ctrss, _, ctr_defss, ctr_sugars)),
+ (ctrss, _, ctor_iff_dtors, ctr_defss, ctr_sugars)),
(recs, rec_defs)), lthy) =
let
val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, rec_attrs)) =
@@ -2453,8 +2464,8 @@
|>> name_noted_thms
(fst (dest_Type (hd fpTs)) ^ implode (map (prefix "_") (tl fp_b_names))) inductN
|-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Least_FP pre_bnfs absT_infos
- fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs
- map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn [])
+ 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
@@ -2541,7 +2552,7 @@
((((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),
- (_, _, ctr_defss, ctr_sugars)),
+ (_, _, ctor_iff_dtors, ctr_defss, ctr_sugars)),
(corecs, corec_defs)), lthy) =
let
val (([(coinduct_thms, coinduct_thm), (coinduct_strong_thms, coinduct_strong_thm)],
@@ -2631,8 +2642,8 @@
[flat corec_sel_thmss, flat corec_thmss]
|> Local_Theory.notes (common_notes @ notes)
|-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos
- fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs
- map_thmss [coinduct_thm, coinduct_strong_thm]
+ fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctor_iff_dtors ctr_defss ctr_sugars
+ 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
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Feb 15 12:48:10 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Feb 15 13:30:04 2016 +0100
@@ -144,6 +144,7 @@
morph_ctr_sugar phi ctr_sugar
end;
+ val ctor_iff_dtors = map (#ctor_iff_dtor o #fp_ctr_sugar) fp_sugars0;
val ctr_defss = map (#ctr_defs o #fp_ctr_sugar) fp_sugars0;
val mapss = map (#map_thms o #fp_bnf_sugar) fp_sugars0;
val ctr_sugars = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0;
@@ -291,8 +292,8 @@
val names_lthy = lthy |> fold Variable.declare_typ (As @ Cs @ Xs);
val phi = Proof_Context.export_morphism names_lthy lthy;
- fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec
- co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss
+ fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctor_iff_dtor ctr_defs ctr_sugar
+ co_rec co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss
({fp_ctr_sugar = {ctr_transfers, case_transfers, disc_transfers, sel_transfers, ...},
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, ...},
@@ -305,6 +306,7 @@
fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs,
fp_ctr_sugar =
{ctrXs_Tss = ctrXs_Tss,
+ ctor_iff_dtor = ctor_iff_dtor,
ctr_defs = ctr_defs,
ctr_sugar = ctr_sugar,
ctr_transfers = ctr_transfers,
@@ -343,8 +345,8 @@
|> morph_fp_sugar phi;
val target_fp_sugars =
- @{map 16} mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss
- ctr_sugars co_recs co_rec_defs mapss (transpose co_inductss') co_rec_thmss
+ @{map 17} mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctor_iff_dtors
+ ctr_defss ctr_sugars co_recs co_rec_defs mapss (transpose co_inductss') co_rec_thmss
co_rec_disc_thmss co_rec_sel_thmsss fp_sugars0;
val n2m_sugar = (target_fp_sugars, fp_sugar_thms);