1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Sun Oct 20 22:51:21 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Sun Oct 20 23:29:49 2013 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  signature BNF_FP_REC_SUGAR_TACTICS =
     1.5  sig
     1.6    val mk_primcorec_assumption_tac: Proof.context -> thm list -> int -> tactic
     1.7 -  val mk_primcorec_code_of_raw_code_tac: Proof.context -> thm list -> thm -> tactic
     1.8 +  val mk_primcorec_code_of_raw_code_tac: Proof.context -> thm list -> thm list -> thm -> tactic
     1.9    val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
    1.10    val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
    1.11      tactic
    1.12 @@ -26,6 +26,7 @@
    1.13  open BNF_Tactics
    1.14  
    1.15  val falseEs = @{thms not_TrueE FalseE};
    1.16 +val Let_def = @{thm Let_def};
    1.17  val neq_eq_eq_contradict = @{thm neq_eq_eq_contradict};
    1.18  val split_if = @{thm split_if};
    1.19  val split_if_asm = @{thm split_if_asm};
    1.20 @@ -86,7 +87,7 @@
    1.21  fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs =
    1.22    HEADGOAL (rtac ((if null sel_fs then collapse else collapse RS sym) RS trans) THEN'
    1.23      (the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN
    1.24 -  unfold_thms_tac ctxt (@{thm Let_def} :: sel_fs) THEN HEADGOAL (rtac refl);
    1.25 +  unfold_thms_tac ctxt (Let_def :: sel_fs) THEN HEADGOAL (rtac refl);
    1.26  
    1.27  fun inst_split_eq ctxt split =
    1.28    (case prop_of split of
    1.29 @@ -100,6 +101,9 @@
    1.30      end
    1.31    | _ => split);
    1.32  
    1.33 +fun distinct_in_prems_tac distincts =
    1.34 +  eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac;
    1.35 +
    1.36  (* TODO: reduce code duplication with selector tactic above *)
    1.37  fun mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m f_ctr =
    1.38    let
    1.39 @@ -111,10 +115,11 @@
    1.40      HEADGOAL ((REPEAT_DETERM_N m o mk_primcorec_assumption_tac ctxt discIs) THEN'
    1.41        SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
    1.42        (rtac refl ORELSE' atac ORELSE'
    1.43 -       resolve_tac (@{thm Code.abort_def} :: splits' @ split_connectI) ORELSE'
    1.44 +       resolve_tac (@{thm Code.abort_def} :: split_connectI) ORELSE'
    1.45 +       Splitter.split_tac (split_if :: splits) ORELSE'
    1.46         Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
    1.47         mk_primcorec_assumption_tac ctxt discIs ORELSE'
    1.48 -       eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
    1.49 +       distinct_in_prems_tac distincts ORELSE'
    1.50         (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))))
    1.51    end;
    1.52  
    1.53 @@ -124,13 +129,14 @@
    1.54    IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN
    1.55      HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI)));
    1.56  
    1.57 -fun mk_primcorec_code_of_raw_code_tac ctxt splits raw =
    1.58 +fun mk_primcorec_code_of_raw_code_tac ctxt distincts splits raw =
    1.59    HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN'
    1.60 -    SELECT_GOAL (unfold_thms_tac ctxt @{thms Let_def}) THEN' REPEAT_DETERM o
    1.61 -    (rtac refl ORELSE'
    1.62 -     (TRY o rtac sym) THEN' atac ORELSE'
    1.63 +    SELECT_GOAL (unfold_thms_tac ctxt [Let_def]) THEN' REPEAT_DETERM o
    1.64 +    (rtac refl ORELSE' atac ORELSE'
    1.65       resolve_tac split_connectI ORELSE'
    1.66       Splitter.split_tac (split_if :: splits) ORELSE'
    1.67 +     distinct_in_prems_tac distincts ORELSE'
    1.68 +     rtac sym THEN' atac ORELSE'
    1.69       etac notE THEN' atac));
    1.70  
    1.71  end;