--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 06 13:33:15 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Oct 06 13:33:24 2014 +0200
@@ -20,7 +20,8 @@
rel_injects: thm list,
rel_distincts: thm list,
rel_sels: thm list,
- rel_intros: thm list}
+ rel_intros: thm list,
+ rel_cases: thm list}
type fp_co_induct_sugar =
{co_rec: term,
@@ -176,7 +177,8 @@
rel_injects: thm list,
rel_distincts: thm list,
rel_sels: thm list,
- rel_intros: thm list};
+ rel_intros: thm list,
+ rel_cases: thm list};
type fp_co_induct_sugar =
{co_rec: term,
@@ -203,14 +205,15 @@
fp_co_induct_sugar: fp_co_induct_sugar};
fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, map_sels, rel_injects, rel_distincts,
- rel_sels, rel_intros} : fp_bnf_sugar) =
+ rel_sels, rel_intros, rel_cases} : fp_bnf_sugar) =
{map_thms = map (Morphism.thm phi) map_thms,
map_disc_iffs = map (Morphism.thm phi) map_disc_iffs,
map_sels = map (Morphism.thm phi) map_sels,
rel_injects = map (Morphism.thm phi) rel_injects,
rel_distincts = map (Morphism.thm phi) rel_distincts,
rel_sels = map (Morphism.thm phi) rel_sels,
- rel_intros = map (Morphism.thm phi) rel_intros};
+ rel_intros = map (Morphism.thm phi) rel_intros,
+ rel_cases = map (Morphism.thm phi) rel_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_selss} : fp_co_induct_sugar) =
@@ -294,7 +297,7 @@
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
- rel_distinctss map_disc_iffss map_selss rel_selss rel_intross noted =
+ rel_distinctss map_disc_iffss map_selss rel_selss rel_intross rel_casess noted =
let
val fp_sugars =
map_index (fn (kk, T) =>
@@ -312,7 +315,8 @@
rel_injects = nth rel_injectss kk,
rel_distincts = nth rel_distinctss kk,
rel_sels = nth rel_selss kk,
- rel_intros = nth rel_intross kk},
+ rel_intros = nth rel_intross kk,
+ rel_cases = nth rel_casess kk},
fp_co_induct_sugar =
{co_rec = nth co_recs kk,
common_co_inducts = common_co_inducts,
@@ -472,7 +476,7 @@
distincts, distinct_discsss, ...} : ctr_sugar)
lthy =
if live = 0 then
- (([], [], [], [], [], [], [], []), lthy)
+ (([], [], [], [], [], [], [], [], []), lthy)
else
let
val n = length ctr_Tss;
@@ -959,6 +963,7 @@
map subst rel_distinct_thms,
map subst rel_sel_thms,
map subst rel_intro_thms,
+ [subst rel_cases_thm],
map (map subst) set0_thmss), lthy')
end;
@@ -2063,7 +2068,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_list4 o apfst split_list8 o split_list)
+ |>> apsnd split_list o apfst (apsnd split_list4 o apfst split_list9 o split_list)
o split_list;
fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects
@@ -2097,7 +2102,7 @@
fun derive_note_induct_recs_thms_for_types
((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss,
- rel_intross, setss),
+ rel_intross, rel_casess, setss),
(ctrss, _, ctr_defss, ctr_sugars)),
(recs, rec_defs)), lthy) =
let
@@ -2156,7 +2161,7 @@
|-> 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 []) (replicate nn [])
- rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss rel_intross
+ rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss rel_intross rel_casess
end;
fun derive_corec_transfer_thms lthy corecs corec_defs =
@@ -2176,7 +2181,7 @@
fun derive_note_coinduct_corecs_thms_for_types
((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss,
- rel_intross, setss),
+ rel_intross, rel_casess, setss),
(_, _, ctr_defss, ctr_sugars)),
(corecs, corec_defs)), lthy) =
let
@@ -2272,7 +2277,7 @@
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_selss rel_selss
- rel_intross
+ rel_intross rel_casess
end;
val lthy'' = lthy'
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Oct 06 13:33:15 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Oct 06 13:33:24 2014 +0200
@@ -294,7 +294,7 @@
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
({fp_bnf_sugar = {map_disc_iffs, map_sels, rel_injects, rel_distincts, rel_sels,
- rel_intros, ...}, ...} : fp_sugar) =
+ rel_intros, rel_cases, ...}, ...} : 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, absT_info = absT_info, fp_nesting_bnfs = fp_nesting_bnfs,
live_nesting_bnfs = live_nesting_bnfs,
@@ -309,7 +309,8 @@
rel_injects = rel_injects,
rel_distincts = rel_distincts,
rel_sels = rel_sels,
- rel_intros = rel_intros},
+ rel_intros = rel_intros,
+ rel_cases = rel_cases},
fp_co_induct_sugar =
{co_rec = co_rec,
common_co_inducts = common_co_inducts,
--- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:33:15 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Oct 06 13:33:24 2014 +0200
@@ -87,7 +87,8 @@
rel_injects = @{thms rel_sum_simps(1,4)},
rel_distincts = @{thms rel_sum_simps(2,3)[THEN eq_False[THEN iffD1]]},
rel_sels = [],
- rel_intros = []},
+ rel_intros = [],
+ rel_cases = []},
fp_co_induct_sugar =
{co_rec = Const (@{const_name case_sum}, map (fn Ts => (Ts ---> C)) ctr_Tss ---> fpT --> C),
common_co_inducts = @{thms sum.induct},
@@ -135,7 +136,8 @@
rel_injects = @{thms rel_prod_apply},
rel_distincts = [],
rel_sels = [],
- rel_intros = []},
+ rel_intros = [],
+ rel_cases = []},
fp_co_induct_sugar =
{co_rec = Const (@{const_name case_prod}, (ctr_Ts ---> C) --> fpT --> C),
common_co_inducts = @{thms prod.induct},
--- a/src/HOL/Tools/BNF/bnf_util.ML Mon Oct 06 13:33:15 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Mon Oct 06 13:33:24 2014 +0200
@@ -65,6 +65,8 @@
'd list * 'e list * 'f list * 'g list
val split_list8: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h) list -> 'a list * 'b list * 'c list *
'd list * 'e list * 'f list * 'g list * 'h list
+ val split_list9: ('a * 'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i) list -> 'a list * 'b list *
+ 'c list * 'd list * 'e list * 'f list * 'g list * 'h list * 'i list
val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context
val mk_Freesss: string -> typ list list list -> Proof.context ->
@@ -315,6 +317,12 @@
let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8) = split_list8 xs;
in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8) end;
+fun split_list9 [] = ([], [], [], [], [], [], [], [], [])
+ | split_list9 ((x1, x2, x3, x4, x5, x6, x7, x8, x9) :: xs) =
+ let val (xs1, xs2, xs3, xs4, xs5, xs6, xs7, xs8, xs9) = split_list9 xs;
+ in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5, x6 :: xs6, x7 :: xs7, x8 :: xs8,
+ x9 :: xs9) end;
+
val parse_type_arg_constrained =
Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);