--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Thu Dec 19 20:07:06 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Thu Dec 19 21:49:30 2013 +0100
@@ -97,7 +97,6 @@
fun distinct_in_prems_tac distincts =
eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac;
-(* TODO: reduce code duplication with selector tactic above *)
fun mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m f_ctr =
let
val splits' =
@@ -116,12 +115,24 @@
(TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))))
end;
-(* TODO: implement "exhaustive" (maybe_exh) *)
-fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms f_ctrs maybe_exh =
- EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms) ms
- f_ctrs) THEN
- IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN
- HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI)));
+fun rulify_exhaust n = funpow (n - 1) (fn thm => thm RS @{thm Meson.make_pos_rule'});
+
+fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms f_ctrs
+ maybe_exhaust =
+ let
+ val n = length ms;
+ val (ms', f_ctrs') =
+ (case maybe_exhaust of
+ NONE => (ms, f_ctrs)
+ | SOME exhaust =>
+ (ms |> split_last ||> K [n - 1] |> op @,
+ f_ctrs |> split_last ||> (fn thm => [rulify_exhaust n exhaust RS thm]) |> op @));
+ in
+ EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)
+ ms' f_ctrs') THEN
+ IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN
+ HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI)))
+ end;
fun mk_primcorec_code_of_raw_code_tac ctxt distincts splits raw =
HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN'