--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 02 09:50:22 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 02 09:50:22 2014 +0100
@@ -968,6 +968,8 @@
fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
+ val p_imp_p = mk_imp_p [mk_imp_p []];
+
fun prove thmss'' def_thms' lthy =
let
val def_thms = map (snd o snd) def_thms';
@@ -987,6 +989,8 @@
|> K |> Goal.prove lthy [] [] goal
|> Thm.close_derivation])
disc_eqnss nchotomy_thmss;
+ val nontriv_exhaust_thmss =
+ map (filter_out (fn thm => prop_of thm aconv p_imp_p)) exhaust_thmss;
val excludess' = map (op ~~) (goal_idxss ~~ exclude_thmss);
fun mk_excludesss excludes n =
@@ -1224,7 +1228,7 @@
(discN, disc_thmss, simp_attrs),
(disc_iffN, disc_iff_thmss, []),
(excludeN, exclude_thmss, []),
- (exhaustN, exhaust_thmss, []),
+ (exhaustN, nontriv_exhaust_thmss, []),
(selN, sel_thmss, simp_attrs),
(simpsN, simp_thmss, []),
(strong_coinductN, map (if n2m then single else K []) strong_coinduct_thms, [])]
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Thu Jan 02 09:50:22 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Thu Jan 02 09:50:22 2014 +0100
@@ -86,12 +86,12 @@
rtac fun_exhaust THEN'
EVERY' (map2 (fn k' => fn disc =>
if k' = k then
- REPEAT_DETERM o (atac ORELSE' etac conjI)
+ REPEAT_DETERM o (atac ORELSE' rtac TrueI ORELSE' etac conjI)
else
dtac disc THEN' (REPEAT_DETERM o atac) THEN' dresolve_tac disc_excludes THEN'
etac notE THEN' atac)
ks fun_discs) THEN'
- etac (unfold_thms ctxt [atomize_conjL] (nth fun_discs (k - 1))))
+ rtac (unfold_thms ctxt [atomize_conjL] (nth fun_discs (k - 1))) THEN_MAYBE' atac)
end;
fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms map_idents map_comps fun_sel k m