1.1 --- a/src/HOL/BNF/BNF_FP_Base.thy Wed Sep 18 15:33:32 2013 +0200
1.2 +++ b/src/HOL/BNF/BNF_FP_Base.thy Wed Sep 18 15:33:32 2013 +0200
1.3 @@ -159,6 +159,9 @@
1.4 (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
1.5 unfolding Grp_def by rule auto
1.6
1.7 +lemma eq_ifI: "\<lbrakk>b \<Longrightarrow> t = x; \<not> b \<Longrightarrow> t = y\<rbrakk> \<Longrightarrow> t = (if b then x else y)"
1.8 + by fastforce
1.9 +
1.10 lemma if_if_True:
1.11 "(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) =
1.12 (if b then x else if b' then x' else f y')"
2.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Wed Sep 18 15:33:32 2013 +0200
2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Wed Sep 18 15:33:32 2013 +0200
2.3 @@ -7,12 +7,14 @@
2.4
2.5 signature BNF_FP_REC_SUGAR_TACTICS =
2.6 sig
2.7 - val mk_primcorec_taut_tac: Proof.context -> tactic
2.8 - val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
2.9 - tactic
2.10 + val mk_primcorec_code_tac: Proof.context -> thm -> thm list -> tactic
2.11 + val mk_primcorec_code_of_ctr_tac: Proof.context -> thm list -> thm list -> tactic
2.12 val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic
2.13 val mk_primcorec_ctr_or_sel_tac: Proof.context -> thm list -> thm -> int -> int ->
2.14 thm list list list -> thm list -> thm list -> thm list -> tactic
2.15 + val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
2.16 + tactic
2.17 + val mk_primcorec_taut_tac: Proof.context -> tactic
2.18 val mk_primrec_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> tactic
2.19 end;
2.20
2.21 @@ -55,12 +57,30 @@
2.22 mk_primcorec_prelude ctxt defs disc THEN mk_primcorec_cases_tac ctxt k m exclsss;
2.23
2.24 fun mk_primcorec_ctr_or_sel_tac ctxt defs eq_thm k m exclsss maps map_idents map_comps =
2.25 - mk_primcorec_prelude ctxt defs (eq_thm RS trans) THEN mk_primcorec_cases_tac ctxt k m exclsss THEN
2.26 - unfold_thms_tac ctxt (@{thms if_if_True if_if_False if_True if_False o_def split_def sum.cases} @
2.27 - maps @ map_comps @ map_idents) THEN HEADGOAL (rtac refl);
2.28 + mk_primcorec_prelude ctxt defs (eq_thm RS trans) THEN
2.29 + mk_primcorec_cases_tac ctxt k m exclsss THEN
2.30 + unfold_thms_tac ctxt (@{thms if_if_True if_if_False if_True if_False if_cancel[of _ True]
2.31 + if_cancel[of _ False] o_def split_def sum.cases} @ maps @ map_comps @ map_idents) THEN
2.32 + HEADGOAL (rtac refl);
2.33
2.34 fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse disc sels =
2.35 HEADGOAL (rtac (collapse RS sym RS trans) THEN' rtac disc THEN' REPEAT_DETERM_N m o atac) THEN
2.36 unfold_thms_tac ctxt sels THEN HEADGOAL (rtac refl);
2.37
2.38 +fun mk_primcorec_code_of_ctr_case_tac ctxt defs ctr_thm =
2.39 + HEADGOAL (REPEAT o rtac @{thm eq_ifI}) THEN
2.40 + mk_primcorec_prelude ctxt defs (ctr_thm RS trans) THEN
2.41 + REPEAT_DETERM_N 2 (HEADGOAL
2.42 + (asm_simp_tac (ss_only @{thms if_True if_False not_False_eq_True} ctxt)));
2.43 +
2.44 +fun mk_primcorec_code_of_ctr_tac ctxt defs ctr_thms =
2.45 + unfold_thms_tac ctxt defs THEN
2.46 + EVERY (map (mk_primcorec_code_of_ctr_case_tac ctxt []) ctr_thms);
2.47 +
2.48 +fun mk_primcorec_code_tac ctxt raw collapses =
2.49 + HEADGOAL (rtac (raw RS trans)) THEN unfold_thms_tac ctxt @{thms split_ifs} THEN
2.50 + Method.intros_tac @{thms conjI impI} [] THEN
2.51 + REPEAT (HEADGOAL (rtac refl ORELSE' (etac notE THEN' atac) ORELSE'
2.52 + eresolve_tac (maps (fn thm => [thm, thm RS sym]) collapses)));
2.53 +
2.54 end;