# HG changeset patch
# User blanchet
# Date 1379520760 -7200
# Node ID 7d32f33d340d141e40944a3f6b8fc274021468ae
# Parent  e1b039dada7bd3bfbd9cf4615ebeb2d1fa6fcd4a
tuned tactics

diff -r e1b039dada7b -r 7d32f33d340d src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Wed Sep 18 17:36:47 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML	Wed Sep 18 18:12:40 2013 +0200
@@ -134,7 +134,6 @@
   HEADGOAL (rtac uexhaust THEN'
     EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases));
 
-(* TODO: More precise "simp_thms"; get rid of "blast_tac" *)
 fun mk_split_tac ctxt uexhaust cases injectss distinctsss =
   HEADGOAL (rtac uexhaust) THEN
   ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
diff -r e1b039dada7b -r 7d32f33d340d src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Sep 18 17:36:47 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Wed Sep 18 18:12:40 2013 +0200
@@ -717,7 +717,7 @@
     (* try to prove (automatically generated) tautologies by ourselves *)
     val exclss'' = exclss'
       |> map (map (apsnd
-        (`(try (fn t => Goal.prove lthy [] [] t (mk_primcorec_taut_tac lthy |> K))))));
+        (`(try (fn t => Goal.prove lthy [] [] t (mk_primcorec_assumption_tac lthy |> K))))));
     val taut_thmss = map (map (apsnd (the o fst)) o filter (is_some o fst o snd)) exclss'';
     val (obligation_idxss, obligationss) = exclss''
       |> map (map (apsnd (rpair [] o snd)) o filter (is_none o fst o snd))
diff -r e1b039dada7b -r 7d32f33d340d src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Wed Sep 18 17:36:47 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML	Wed Sep 18 18:12:40 2013 +0200
@@ -8,13 +8,13 @@
 signature BNF_FP_REC_SUGAR_TACTICS =
 sig
   val mk_primcorec_code_tac: Proof.context -> thm -> thm list -> tactic
-  val mk_primcorec_code_of_ctr_tac: Proof.context -> thm list -> tactic
+  val mk_primcorec_code_of_ctr_tac: Proof.context -> int list -> thm list -> tactic
   val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic
   val mk_primcorec_ctr_or_sel_tac: Proof.context -> thm list -> thm -> int -> int ->
     thm list list list -> thm list -> thm list -> thm list -> tactic
   val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
     tactic
-  val mk_primcorec_taut_tac: Proof.context -> tactic
+  val mk_primcorec_assumption_tac: Proof.context -> tactic
   val mk_primrec_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> tactic
 end;
 
@@ -30,10 +30,8 @@
   unfold_thms_tac ctxt (@{thms id_def split o_def fst_conv snd_conv} @ map_comps @ map_idents) THEN
   HEADGOAL (rtac refl);
 
-fun mk_primcorec_taut_tac ctxt =
-  HEADGOAL (etac FalseE) ORELSE
-  unfold_thms_tac ctxt @{thms de_Morgan_conj de_Morgan_disj not_not not_False_eq_True} THEN
-  HEADGOAL (SOLVE o REPEAT o (atac ORELSE' resolve_tac @{thms disjI1 disjI2 conjI TrueI}));
+fun mk_primcorec_assumption_tac ctxt =
+  HEADGOAL (blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt));
 
 fun mk_primcorec_same_case_tac m =
   HEADGOAL (if m = 0 then rtac TrueI
@@ -41,7 +39,7 @@
 
 fun mk_primcorec_different_case_tac ctxt excl =
   unfold_thms_tac ctxt @{thms not_not not_False_eq_True} THEN
-  HEADGOAL (rtac excl THEN_ALL_NEW SELECT_GOAL (mk_primcorec_taut_tac ctxt));
+  HEADGOAL (rtac excl THEN_ALL_NEW SELECT_GOAL (mk_primcorec_assumption_tac ctxt));
 
 fun mk_primcorec_cases_tac ctxt k m exclsss =
   let val n = length exclsss in
@@ -67,14 +65,14 @@
   HEADGOAL (rtac (collapse RS sym RS trans) THEN' rtac disc THEN' REPEAT_DETERM_N m o atac) THEN
   unfold_thms_tac ctxt sels THEN HEADGOAL (rtac refl);
 
-fun mk_primcorec_code_of_ctr_case_tac ctxt defs ctr_thm =
+fun mk_primcorec_code_of_ctr_case_tac ctxt m ctr_thm =
   HEADGOAL (REPEAT o rtac @{thm eq_ifI}) THEN
-  mk_primcorec_prelude ctxt defs (ctr_thm RS trans) THEN
-  REPEAT_DETERM_N 2 (HEADGOAL
-    (asm_simp_tac (ss_only @{thms if_True if_False not_False_eq_True} ctxt)));
+  mk_primcorec_prelude ctxt [] (ctr_thm RS trans) THEN
+  REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt) THEN
+  HEADGOAL (asm_simp_tac (ss_only @{thms if_True if_False not_False_eq_True} ctxt));
 
-fun mk_primcorec_code_of_ctr_tac ctxt ctr_thms =
-  EVERY (map (mk_primcorec_code_of_ctr_case_tac ctxt []) ctr_thms);
+fun mk_primcorec_code_of_ctr_tac ctxt ms ctr_thms =
+  EVERY (map2 (mk_primcorec_code_of_ctr_case_tac ctxt) ms ctr_thms);
 
 fun mk_primcorec_code_tac ctxt raw collapses =
   HEADGOAL (rtac (raw RS trans)) THEN unfold_thms_tac ctxt @{thms split_ifs} THEN