--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Wed Sep 18 20:33:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Wed Sep 18 20:54:46 2013 +0200
@@ -518,23 +518,23 @@
ks goals inject_thmss distinct_thmsss
end;
- val (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
- disc_exhaust_thms, collapse_thms, expand_thms, case_conv_thms) =
+ val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms,
+ disc_exclude_thms, disc_exhaust_thms, collapse_thms, expand_thms, case_conv_thms) =
if no_discs_sels then
- ([], [], [], [], [], [], [], [], [], [])
+ ([], [], [], [], [], [], [], [], [], [], [])
else
let
fun make_sel_thm xs' case_thm sel_def =
zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs')
(Drule.forall_intr_vars (case_thm RS (sel_def RS trans)))));
+ val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss;
+
fun has_undefined_rhs thm =
(case snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) of
Const (@{const_name undefined}, _) => true
| _ => false);
- val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss;
-
val all_sel_thms =
(if all_sels_distinct andalso forall null sel_defaultss then
flat sel_thmss
@@ -593,8 +593,16 @@
map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose
end;
- val disc_thms = flat (map2 (fn b => if is_disc_binding_valid b then I else K [])
- disc_bindings disc_thmss);
+ val nontriv_disc_thms =
+ flat (map2 (fn b => if is_disc_binding_valid b then I else K [])
+ disc_bindings disc_thmss);
+
+ fun is_discI_boring b =
+ (n = 1 andalso Binding.is_empty b) orelse Binding.eq_name (b, equal_binding);
+
+ val nontriv_discI_thms =
+ flat (map2 (fn b => if is_discI_boring b then K [] else single) disc_bindings
+ discI_thms);
val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) =
let
@@ -693,12 +701,11 @@
|> Proof_Context.export names_lthy lthy
end;
in
- (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
- [disc_exhaust_thm], collapse_thms, expand_thms, case_conv_thms)
+ (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms,
+ nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], collapse_thms,
+ expand_thms, case_conv_thms)
end;
- val nontriv_discI_thms = if n = 1 then [] else discI_thms;
-
val (case_cong_thm, weak_case_cong_thm) =
let
fun mk_prem xctr xs xf xg =
@@ -753,7 +760,7 @@
(case_congN, [case_cong_thm], []),
(case_convN, case_conv_thms, []),
(collapseN, collapse_thms, simp_attrs),
- (discN, disc_thms, simp_attrs),
+ (discN, nontriv_disc_thms, simp_attrs),
(discIN, nontriv_discI_thms, []),
(disc_excludeN, disc_exclude_thms, []),
(disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]),
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Wed Sep 18 20:33:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Wed Sep 18 20:54:46 2013 +0200
@@ -13,8 +13,10 @@
val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic
val mk_primcorec_ctr_or_sel_tac: Proof.context -> thm list -> thm -> int -> int ->
thm list list list -> thm list -> thm list -> thm list -> tactic
+ val mk_primcorec_disc_of_ctr_tac: thm -> thm -> tactic;
val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
tactic
+ val mk_primcorec_sel_of_ctr_tac: thm -> thm -> tactic;
val mk_primrec_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> tactic
end;
@@ -51,23 +53,29 @@
fun mk_primcorec_prelude ctxt defs thm =
unfold_thms_tac ctxt defs THEN HEADGOAL (rtac thm) THEN unfold_thms_tac ctxt @{thms split};
-fun mk_primcorec_disc_tac ctxt defs disc k m exclsss =
- mk_primcorec_prelude ctxt defs disc THEN mk_primcorec_cases_tac ctxt k m exclsss;
+fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss =
+ mk_primcorec_prelude ctxt defs disc_corec THEN mk_primcorec_cases_tac ctxt k m exclsss;
-fun mk_primcorec_ctr_or_sel_tac ctxt defs eq_thm k m exclsss maps map_idents map_comps =
- mk_primcorec_prelude ctxt defs (eq_thm RS trans) THEN
+fun mk_primcorec_ctr_or_sel_tac ctxt defs f_eq k m exclsss maps map_idents map_comps =
+ mk_primcorec_prelude ctxt defs (f_eq RS trans) THEN
mk_primcorec_cases_tac ctxt k m exclsss THEN
unfold_thms_tac ctxt (@{thms if_if_True if_if_False if_True if_False if_cancel[of _ True]
if_cancel[of _ False] o_def split_def sum.cases} @ maps @ map_comps @ map_idents) THEN
HEADGOAL (rtac refl);
-fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse disc sels =
- HEADGOAL (rtac (collapse RS sym RS trans) THEN' rtac disc THEN' REPEAT_DETERM_N m o atac) THEN
- unfold_thms_tac ctxt sels THEN HEADGOAL (rtac refl);
+fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse disc_f sel_fs =
+ HEADGOAL (rtac (collapse RS sym RS trans) THEN' rtac disc_f THEN' REPEAT_DETERM_N m o atac) THEN
+ unfold_thms_tac ctxt sel_fs THEN HEADGOAL (rtac refl);
+
+fun mk_primcorec_disc_of_ctr_tac discI f_ctr =
+ HEADGOAL (rtac discI THEN' rtac f_ctr) THEN ALLGOALS atac;
-fun mk_primcorec_code_of_ctr_case_tac ctxt m ctr_thm =
+fun mk_primcorec_sel_of_ctr_tac sel f_ctr =
+ HEADGOAL (etac (f_ctr RS arg_cong RS trans) THEN' rtac sel);
+
+fun mk_primcorec_code_of_ctr_case_tac ctxt m f_ctr =
HEADGOAL (REPEAT o rtac @{thm eq_ifI}) THEN
- mk_primcorec_prelude ctxt [] (ctr_thm RS trans) THEN
+ mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN
REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt) THEN
HEADGOAL (asm_simp_tac (ss_only @{thms if_True if_False not_False_eq_True} ctxt));
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 18 20:33:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 18 20:54:46 2013 +0200
@@ -31,6 +31,8 @@
sels: term list,
pred: int option,
calls: corec_call list,
+ discI: thm,
+ sel_thms: thm list,
collapse: thm,
corec_thm: thm,
disc_corec: thm,
@@ -96,6 +98,8 @@
sels: term list,
pred: int option,
calls: corec_call list,
+ discI: thm,
+ sel_thms: thm list,
collapse: thm,
corec_thm: thm,
disc_corec: thm,
@@ -431,11 +435,13 @@
else No_Corec) g_i
| call_of _ [q_i] [g_i, g_i'] _ = Direct_Corec (q_i, g_i, g_i');
- fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss collapse corec_thm disc_corec sel_corecs =
+ fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss discI sel_thms collapse corec_thm
+ disc_corec sel_corecs =
let val nullary = not (can dest_funT (fastype_of ctr)) in
{ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_ho,
- calls = map3 (call_of nullary) q_iss f_iss f_Tss, collapse = collapse,
- corec_thm = corec_thm, disc_corec = disc_corec, sel_corecs = sel_corecs}
+ calls = map3 (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms,
+ collapse = collapse, corec_thm = corec_thm, disc_corec = disc_corec,
+ sel_corecs = sel_corecs}
end;
fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss
@@ -445,14 +451,16 @@
val discs = #discs (nth ctr_sugars index);
val selss = #selss (nth ctr_sugars index);
val p_ios = map SOME p_is @ [NONE];
+ val discIs = #discIs (nth ctr_sugars index);
+ val sel_thmss = #sel_thmss (nth ctr_sugars index);
val collapses = #collapses (nth ctr_sugars index);
val corec_thms = co_rec_of (nth coiter_thmsss index);
val disc_corecs = (case co_rec_of (nth disc_coitersss index) of [] => [TrueI]
| thms => thms);
val sel_corecss = co_rec_of (nth sel_coiterssss index);
in
- map11 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss collapses corec_thms
- disc_corecs sel_corecss
+ map13 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss collapses
+ corec_thms disc_corecs sel_corecss
end;
fun mk_spec {T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss,
--- a/src/HOL/BNF/Tools/bnf_util.ML Wed Sep 18 20:33:36 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML Wed Sep 18 20:54:46 2013 +0200
@@ -29,6 +29,9 @@
val map12: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm) ->
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
'i list -> 'j list -> 'k list -> 'l list -> 'm list
+ val map13: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n) ->
+ 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
+ 'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list
val fold_map2: ('a -> 'b -> 'c -> 'd * 'c) -> 'a list -> 'b list -> 'c -> 'd list * 'c
val fold_map3: ('a -> 'b -> 'c -> 'd -> 'e * 'd) ->
'a list -> 'b list -> 'c list -> 'd -> 'e list * 'd
@@ -248,6 +251,13 @@
map12 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s
| map12 _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
+fun map13 _ [] [] [] [] [] [] [] [] [] [] [] [] [] = []
+ | map13 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s)
+ (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) =
+ f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ::
+ map13 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s
+ | map13 _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
+
fun fold_map2 _ [] [] acc = ([], acc)
| fold_map2 f (x1::x1s) (x2::x2s) acc =
let