made tactic more flexible w.r.t. case expressions and such
--- a/src/HOL/BNF/BNF_FP_Base.thy Wed Sep 25 21:25:53 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Base.thy Thu Sep 26 01:05:06 2013 +0200
@@ -13,6 +13,9 @@
imports BNF_Comp BNF_Ctr_Sugar
begin
+lemma not_TrueE: "\<not> True \<Longrightarrow> P"
+by (erule notE, rule TrueI)
+
lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
by auto
@@ -162,16 +165,6 @@
lemma eq_ifI: "\<lbrakk>b \<Longrightarrow> t = x; \<not> b \<Longrightarrow> t = y\<rbrakk> \<Longrightarrow> t = (if b then x else y)"
by fastforce
-lemma if_if_True:
- "(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) =
- (if b then x else if b' then x' else f y')"
- by simp
-
-lemma if_if_False:
- "(if (if b then False else b') then (if b then x else x') else f (if b then y else y')) =
- (if b then f y else if b' then x' else f y')"
- by simp
-
ML_file "Tools/bnf_fp_util.ML"
ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
ML_file "Tools/bnf_fp_def_sugar.ML"
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Wed Sep 25 21:25:53 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML Thu Sep 26 01:05:06 2013 +0200
@@ -802,7 +802,7 @@
|> curry Logic.list_all (map dest_Free fun_args);
in
mk_primcorec_ctr_or_sel_tac lthy def_thms sel_corec k m exclsss
- nested_maps nested_map_idents nested_map_comps
+ nested_maps nested_map_idents nested_map_comps [] []
|> K |> Goal.prove lthy [] [] t
|> pair sel
end;
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Wed Sep 25 21:25:53 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Thu Sep 26 01:05:06 2013 +0200
@@ -12,7 +12,7 @@
val mk_primcorec_code_of_ctr_tac: Proof.context -> thm list -> int list -> thm list -> tactic
val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> 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
+ thm list list list -> thm list -> thm 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
@@ -56,12 +56,17 @@
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 f_eq k m exclsss maps map_idents map_comps =
+fun mk_primcorec_ctr_or_sel_tac ctxt defs f_eq k m exclsss maps map_idents map_comps splits
+ split_asms =
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);
+ unfold_thms_tac ctxt (@{thms o_def split_def sum.cases} @ maps @ map_comps @ map_idents) THEN
+ HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE'
+ eresolve_tac @{thms not_TrueE FalseE} ORELSE'
+ resolve_tac @{thms allI impI conjI} ORELSE'
+ Splitter.split_asm_tac (@{thm split_if_asm} :: split_asms) ORELSE'
+ Splitter.split_tac (@{thm split_if} :: splits) ORELSE'
+ etac notE THEN' atac));
fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs =
HEADGOAL (rtac ((if null sel_fs then collapse else collapse RS sym) RS trans) THEN'