# HG changeset patch
# User blanchet
# Date 1409777225 -7200
# Node ID 86a374caeb8213d3b9e741cd2f1796b38532cb2f
# Parent  2ec97d9c1e830416c4f6ddfdb9826ed6f37114c0
improved new countability tactic

diff -r 2ec97d9c1e83 -r 86a374caeb82 src/HOL/Library/bnf_lfp_countable.ML
--- a/src/HOL/Library/bnf_lfp_countable.ML	Wed Sep 03 22:47:05 2014 +0200
+++ b/src/HOL/Library/bnf_lfp_countable.ML	Wed Sep 03 22:47:05 2014 +0200
@@ -23,8 +23,7 @@
 
 fun nchotomy_tac nchotomy =
   HEADGOAL (rtac (nchotomy RS @{thm all_reg[rotated]}) THEN'
-    CHANGED_PROP o REPEAT_ALL_NEW (match_tac [allI, impI]) THEN'
-    CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac [exE, disjE]));
+    REPEAT_ALL_NEW (match_tac [allI, impI]) THEN' REPEAT_ALL_NEW (ematch_tac [exE, disjE]));
 
 fun meta_spec_mp_tac 0 = K all_tac
   | meta_spec_mp_tac depth =
@@ -36,15 +35,17 @@
 
 val same_ctr_simps =
   @{thms sum_encode_eq prod_encode_eq sum.inject prod.inject to_nat_split snd_conv simp_thms};
+val distinct_ctrs_simps = @{thms sum_encode_eq sum.inject sum.distinct simp_thms};
 
-fun same_ctr_tac ctxt injects recs map_comps' inj_map_strongs' =
-  HEADGOAL (asm_full_simp_tac (ss_only (injects @ recs @ map_comps' @ same_ctr_simps) ctxt) THEN'
-    REPEAT_DETERM o CHANGED_PROP o REPEAT_ALL_NEW (ematch_tac (conjE :: inj_map_strongs'))
-    THEN_ALL_NEW use_induction_hypothesis_tac);
+fun same_ctr_tac ctxt injects recs map_congs' inj_map_strongs' =
+  HEADGOAL (asm_full_simp_tac
+      (ss_only (injects @ recs @ map_congs' @ same_ctr_simps) ctxt) THEN_MAYBE'
+    TRY o REPEAT_ALL_NEW (rtac conjI) THEN_ALL_NEW
+    REPEAT_ALL_NEW (eresolve_tac (conjE :: inj_map_strongs')) THEN_ALL_NEW
+    use_induction_hypothesis_tac);
 
 fun distinct_ctrs_tac ctxt recs =
-  HEADGOAL (asm_full_simp_tac (ss_only (recs @
-    @{thms sum_encode_eq sum.inject sum.distinct simp_thms}) ctxt));
+  HEADGOAL (asm_full_simp_tac (ss_only (recs @ distinct_ctrs_simps) ctxt));
 
 fun mk_encode_injective_tac ctxt n nchotomy injects recs map_comps' inj_map_strongs' =
   let val ks = 1 upto n in
@@ -120,7 +121,7 @@
     let
       fun not_datatype s = error (quote s ^ " is not a new-style datatype");
       fun not_mutually_recursive ss =
-        error ("{" ^ commas ss ^ "} are not mutually recursive new-style datatypes");
+        error (commas ss ^ " are not mutually recursive new-style datatypes");
 
       fun lfp_sugar_of s =
         (case fp_sugar_of ctxt s of