# HG changeset patch
# User blanchet
# Date 1366728119 -7200
# Node ID b5ff7393642d779f3931892584017f5de41810fc
# Parent  3fc8eb5c0915b79bb49b84517f8a77da1fc92f1a
fix bugs in expand tactic w.r.t. datatypes with "needless" discriminators (e.g. lists with is_Nil instead of ~= Nil)

diff -r 3fc8eb5c0915 -r b5ff7393642d src/HOL/BNF/Tools/bnf_wrap.ML
--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Tue Apr 23 16:30:30 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Tue Apr 23 16:41:59 2013 +0200
@@ -65,6 +65,9 @@
 val safe_elim_attrs = @{attributes [elim!]};
 val simp_attrs = @{attributes [simp]};
 
+val unique_disc_no_def = TrueI; (*arbitrary marker*)
+val alternate_disc_no_def = FalseE; (*arbitrary marker*)
+
 fun pad_list x n xs = xs @ replicate (n - length xs) x;
 
 fun unflat_lookup eq ys zs = map (map (fn x => nth zs (find_index (curry eq x) ys)));
@@ -216,9 +219,6 @@
     val exist_xs_u_eq_ctrs =
       map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (u, xctr))) xctrs xss;
 
-    val unique_disc_no_def = TrueI; (*arbitrary marker*)
-    val alternate_disc_no_def = FalseE; (*arbitrary marker*)
-
     fun alternate_disc_lhs get_udisc k =
       HOLogic.mk_not
         (case nth disc_bindings (k - 1) of
@@ -535,9 +535,9 @@
                   val goal =
                     Library.foldr Logic.list_implies
                       (map5 mk_prems ks udiscs uselss vdiscs vselss, uv_eq);
-
                   val uncollapse_thms =
-                    map (fn NONE => Drule.dummy_thm | SOME thm => thm RS sym) collapse_thm_opts;
+                    map2 (fn NONE => K asm_rl | SOME thm => fn [] => thm | _ => thm RS sym)
+                      collapse_thm_opts uselss;
                 in
                   [Goal.prove_sorry lthy [] [] goal (fn _ =>
                      mk_expand_tac lthy n ms (inst_thm u disc_exhaust_thm)
diff -r 3fc8eb5c0915 -r b5ff7393642d src/HOL/BNF/Tools/bnf_wrap_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_wrap_tactics.ML	Tue Apr 23 16:30:30 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap_tactics.ML	Tue Apr 23 16:41:59 2013 +0200
@@ -67,29 +67,28 @@
       REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac THEN'
       SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl)) 1;
 
-fun mk_expand_tac ctxt
-    n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss disc_excludesss' =
+fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss
+    disc_excludesss' =
   if ms = [0] then
-    rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses RS sym))) 1
+    (rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses))) THEN'
+     TRY o EVERY' [rtac udisc_exhaust, atac, rtac vdisc_exhaust, atac]) 1
   else
-    let
-      val ks = 1 upto n;
-      val maybe_atac = if n = 1 then K all_tac else atac;
-    in
+    let val ks = 1 upto n in
       (rtac udisc_exhaust THEN'
-       EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' => fn uuncollapse =>
-         EVERY' [if m = 0 then K all_tac else rtac (uuncollapse RS trans) THEN' maybe_atac,
+       EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' =>
+           fn uuncollapse =>
+         EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac,
            rtac sym, rtac vdisc_exhaust,
            EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse =>
              EVERY'
                (if k' = k then
-                  if m = 0 then
-                    [hyp_subst_tac, rtac refl]
-                  else
-                    [rtac (vuncollapse RS trans), maybe_atac,
-                     if n = 1 then K all_tac else EVERY' [dtac meta_mp, atac, dtac meta_mp, atac],
-                     REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE,
-                     asm_simp_tac (ss_only [] ctxt)]
+                  [rtac (vuncollapse RS trans), TRY o atac] @
+                  (if m = 0 then
+                     [rtac refl]
+                   else
+                     [if n = 1 then K all_tac else EVERY' [dtac meta_mp, atac, dtac meta_mp, atac],
+                      REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE,
+                      asm_simp_tac (ss_only [] ctxt)])
                 else
                   [dtac (the_single (if k = n then disc_excludes else disc_excludes')),
                    etac (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}),