--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Thu Jan 09 15:08:24 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Thu Jan 09 15:49:19 2014 +0100
@@ -9,7 +9,7 @@
sig
val mk_primcorec_assumption_tac: Proof.context -> thm list -> int -> tactic
val mk_primcorec_code_of_raw_code_tac: Proof.context -> thm list -> thm list -> thm -> tactic
- val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
+ val mk_primcorec_ctr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
tactic
val mk_primcorec_disc_iff_tac: Proof.context -> string list -> thm -> thm -> thm list list ->
@@ -31,7 +31,6 @@
val atomize_conjL = @{thm atomize_conjL};
val falseEs = @{thms not_TrueE FalseE};
-val Let_def = @{thm Let_def};
val neq_eq_eq_contradict = @{thm neq_eq_eq_contradict};
val split_if = @{thm split_if};
val split_if_asm = @{thm split_if_asm};
@@ -72,8 +71,8 @@
end;
fun mk_primcorec_assumption_tac ctxt discIs =
- SELECT_GOAL (unfold_thms_tac ctxt
- @{thms not_not not_False_eq_True not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN
+ SELECT_GOAL (unfold_thms_tac ctxt @{thms fst_conv snd_conv not_not not_False_eq_True
+ not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN
SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE'
eresolve_tac falseEs ORELSE'
resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE'
@@ -81,27 +80,33 @@
etac notE THEN' atac ORELSE'
etac disjE))));
-fun mk_primcorec_same_case_tac m =
+val ss_fst_snd_conv = simpset_of (ss_only @{thms fst_conv snd_conv} @{context});
+
+fun case_atac ctxt = simp_tac (put_simpset ss_fst_snd_conv ctxt);
+
+fun same_case_tac ctxt m =
HEADGOAL (if m = 0 then rtac TrueI
- else REPEAT_DETERM_N (m - 1) o (rtac conjI THEN' atac) THEN' atac);
+ else REPEAT_DETERM_N (m - 1) o (rtac conjI THEN' case_atac ctxt) THEN' case_atac ctxt);
-fun mk_primcorec_different_case_tac ctxt m excl =
- HEADGOAL (if m = 0 then mk_primcorec_assumption_tac ctxt []
- else dtac excl THEN' (REPEAT_DETERM_N (m - 1) o atac) THEN' mk_primcorec_assumption_tac ctxt []);
+fun different_case_tac ctxt m excl =
+ HEADGOAL (if m = 0 then
+ mk_primcorec_assumption_tac ctxt []
+ else
+ dtac excl THEN' (REPEAT_DETERM_N (m - 1) o case_atac ctxt) THEN'
+ mk_primcorec_assumption_tac ctxt []);
-fun mk_primcorec_cases_tac ctxt k m exclsss =
+fun cases_tac ctxt k m exclsss =
let val n = length exclsss in
- EVERY (map (fn [] => if k = n then all_tac else mk_primcorec_same_case_tac m
- | [excl] => mk_primcorec_different_case_tac ctxt m excl)
+ EVERY (map (fn [] => if k = n then all_tac else same_case_tac ctxt m
+ | [excl] => different_case_tac ctxt m excl)
(take k (nth exclsss (k - 1))))
end;
-fun mk_primcorec_prelude ctxt defs thm =
- unfold_thms_tac ctxt defs THEN HEADGOAL (rtac thm) THEN
- unfold_thms_tac ctxt @{thms Let_def split};
+fun prelude_tac ctxt defs thm =
+ unfold_thms_tac ctxt defs THEN HEADGOAL (rtac thm) THEN unfold_thms_tac ctxt unfold_lets;
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;
+ prelude_tac ctxt defs disc_corec THEN cases_tac ctxt k m exclsss;
fun mk_primcorec_disc_iff_tac ctxt frees fun_exhaust fun_disc fun_discss disc_excludes =
HEADGOAL (rtac iffI THEN'
@@ -119,8 +124,8 @@
fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms map_idents map_comps fun_sel k m
exclsss =
- mk_primcorec_prelude ctxt defs (fun_sel RS trans) THEN
- mk_primcorec_cases_tac ctxt k m exclsss THEN
+ prelude_tac ctxt defs (fun_sel RS trans) THEN
+ cases_tac ctxt k m exclsss THEN
HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' rtac ext ORELSE'
eresolve_tac falseEs ORELSE'
resolve_tac split_connectI ORELSE'
@@ -129,9 +134,9 @@
eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
etac notE THEN' atac ORELSE'
(CHANGED o SELECT_GOAL (unfold_thms_tac ctxt
- (@{thms id_def o_def split_def sum.cases} @ map_comps @ map_idents)))));
+ (@{thms fst_conv snd_conv id_def o_def split_def sum.cases} @ map_comps @ map_idents)))));
-fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse disc_fun_opt sel_funs =
+fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs =
HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN'
(the_default (K all_tac) (Option.map rtac disc_fun_opt)) THEN' REPEAT_DETERM_N m o atac) THEN
unfold_thms_tac ctxt (unfold_lets @ sel_funs) THEN HEADGOAL (rtac refl);
@@ -148,13 +153,13 @@
end
| _ => split);
-fun mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m fun_ctr =
+fun raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m fun_ctr =
let
val splits' =
map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits)
in
HEADGOAL (REPEAT o (resolve_tac (splits' @ split_connectI))) THEN
- mk_primcorec_prelude ctxt [] (fun_ctr RS trans) THEN
+ prelude_tac ctxt [] (fun_ctr RS trans) THEN
HEADGOAL ((REPEAT_DETERM_N m o mk_primcorec_assumption_tac ctxt discIs) THEN'
SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
(rtac refl ORELSE' atac ORELSE'
@@ -183,7 +188,7 @@
||> (fn thm => [rulify_nchotomy n nchotomy RS thm] handle THM _ => [thm])
|> op @));
in
- EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)
+ EVERY (map2 (raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)
ms' fun_ctrs') THEN
IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN
HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI)))
@@ -191,7 +196,7 @@
fun mk_primcorec_code_of_raw_code_tac ctxt distincts splits raw =
HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN'
- SELECT_GOAL (unfold_thms_tac ctxt [Let_def]) THEN' REPEAT_DETERM o
+ SELECT_GOAL (unfold_thms_tac ctxt unfold_lets) THEN' REPEAT_DETERM o
(rtac refl ORELSE' atac ORELSE'
resolve_tac split_connectI ORELSE'
Splitter.split_tac (split_if :: splits) ORELSE'