# HG changeset patch
# User blanchet
# Date 1389278959 -3600
# Node ID a4ef9253a0b859161c50c3de8e3c54b2f97cd985
# Parent  a2f4cf3387fc0920f13d5679fcb5bea8513d4c40
strengthened tactics w.r.t. 'lets' and tuples

diff -r a2f4cf3387fc -r a4ef9253a0b8 src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Thu Jan 09 15:08:24 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Thu Jan 09 15:49:19 2014 +0100
@@ -43,8 +43,6 @@
 val sum_prod_thms_set = @{thms UN_compreh_eq_eq} @ sum_prod_thms_set0;
 val sum_prod_thms_rel = @{thms prod_rel_simp sum_rel_simps id_apply};
 
-val ss_if_True_False = simpset_of (ss_only @{thms if_True if_False} @{context});
-
 fun hhf_concl_conv cv ctxt ct =
   (case Thm.term_of ct of
     Const (@{const_name all}, _) $ Abs _ =>
@@ -94,6 +92,7 @@
     iter_unfold_thms) THEN HEADGOAL (rtac refl);
 
 val coiter_unfold_thms = @{thms id_def} @ sum_prod_thms_map;
+val ss_if_True_False = simpset_of (ss_only @{thms if_True if_False} @{context});
 
 fun mk_coiter_tac coiter_defs map_idents ctor_dtor_coiter pre_map_def ctr_def ctxt =
   unfold_thms_tac ctxt (ctr_def :: coiter_defs) THEN
diff -r a2f4cf3387fc -r a4ef9253a0b8 src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 09 15:08:24 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML	Thu Jan 09 15:49:19 2014 +0100
@@ -1112,7 +1112,7 @@
               val sel_thms = map snd (filter (member (op =) sels o fst) sel_alist);
             in
               if prems = [@{term False}] then [] else
-                mk_primcorec_ctr_of_dtr_tac lthy m collapse disc_thm_opt sel_thms
+                mk_primcorec_ctr_tac lthy m collapse disc_thm_opt sel_thms
                 |> K |> Goal.prove_sorry lthy [] [] goal
                 |> Thm.close_derivation
                 |> pair ctr
@@ -1211,7 +1211,6 @@
         val sel_alists = map4 (map ooo prove_sel) corec_specs disc_eqnss excludessss sel_eqnss;
         val disc_thmss = map (map snd o order_list_duplicates o flat) disc_alistss;
         val disc_thmsss' = map (map (map (snd o snd))) disc_alistss;
-        val disc_thmss' = map flat disc_thmsss';
         val sel_thmss = map (map snd o order_list_duplicates) sel_alists;
 
         fun prove_disc_iff ({ctr_specs, ...} : corec_spec) exhaust_thms disc_thmss' disc_thms
diff -r a2f4cf3387fc -r a4ef9253a0b8 src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 09 15:08:24 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML	Thu Jan 09 15:49:19 2014 +0100
@@ -9,7 +9,7 @@
 sig
   val mk_primcorec_assumption_tac: Proof.context -> thm list -> int -> tactic
   val mk_primcorec_code_of_raw_code_tac: Proof.context -> thm list -> thm list -> thm -> tactic
-  val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
+  val mk_primcorec_ctr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
   val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
     tactic
   val mk_primcorec_disc_iff_tac: Proof.context -> string list -> thm -> thm -> thm list list ->
@@ -31,7 +31,6 @@
 
 val atomize_conjL = @{thm atomize_conjL};
 val falseEs = @{thms not_TrueE FalseE};
-val Let_def = @{thm Let_def};
 val neq_eq_eq_contradict = @{thm neq_eq_eq_contradict};
 val split_if = @{thm split_if};
 val split_if_asm = @{thm split_if_asm};
@@ -72,8 +71,8 @@
   end;
 
 fun mk_primcorec_assumption_tac ctxt discIs =
-  SELECT_GOAL (unfold_thms_tac ctxt
-      @{thms not_not not_False_eq_True not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN
+  SELECT_GOAL (unfold_thms_tac ctxt @{thms fst_conv snd_conv not_not not_False_eq_True
+      not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN
     SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE'
     eresolve_tac falseEs ORELSE'
     resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE'
@@ -81,27 +80,33 @@
     etac notE THEN' atac ORELSE'
     etac disjE))));
 
-fun mk_primcorec_same_case_tac m =
+val ss_fst_snd_conv = simpset_of (ss_only @{thms fst_conv snd_conv} @{context});
+
+fun case_atac ctxt = simp_tac (put_simpset ss_fst_snd_conv ctxt);
+
+fun same_case_tac ctxt m =
   HEADGOAL (if m = 0 then rtac TrueI
-    else REPEAT_DETERM_N (m - 1) o (rtac conjI THEN' atac) THEN' atac);
+    else REPEAT_DETERM_N (m - 1) o (rtac conjI THEN' case_atac ctxt) THEN' case_atac ctxt);
 
-fun mk_primcorec_different_case_tac ctxt m excl =
-  HEADGOAL (if m = 0 then mk_primcorec_assumption_tac ctxt []
-    else dtac excl THEN' (REPEAT_DETERM_N (m - 1) o atac) THEN' mk_primcorec_assumption_tac ctxt []);
+fun different_case_tac ctxt m excl =
+  HEADGOAL (if m = 0 then
+      mk_primcorec_assumption_tac ctxt []
+    else
+      dtac excl THEN' (REPEAT_DETERM_N (m - 1) o case_atac ctxt) THEN'
+      mk_primcorec_assumption_tac ctxt []);
 
-fun mk_primcorec_cases_tac ctxt k m exclsss =
+fun cases_tac ctxt k m exclsss =
   let val n = length exclsss in
-    EVERY (map (fn [] => if k = n then all_tac else mk_primcorec_same_case_tac m
-        | [excl] => mk_primcorec_different_case_tac ctxt m excl)
+    EVERY (map (fn [] => if k = n then all_tac else same_case_tac ctxt m
+        | [excl] => different_case_tac ctxt m excl)
       (take k (nth exclsss (k - 1))))
   end;
 
-fun mk_primcorec_prelude ctxt defs thm =
-  unfold_thms_tac ctxt defs THEN HEADGOAL (rtac thm) THEN
-  unfold_thms_tac ctxt @{thms Let_def split};
+fun prelude_tac ctxt defs thm =
+  unfold_thms_tac ctxt defs THEN HEADGOAL (rtac thm) THEN unfold_thms_tac ctxt unfold_lets;
 
 fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss =
-  mk_primcorec_prelude ctxt defs disc_corec THEN mk_primcorec_cases_tac ctxt k m exclsss;
+  prelude_tac ctxt defs disc_corec THEN cases_tac ctxt k m exclsss;
 
 fun mk_primcorec_disc_iff_tac ctxt frees fun_exhaust fun_disc fun_discss disc_excludes =
   HEADGOAL (rtac iffI THEN'
@@ -119,8 +124,8 @@
 
 fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms map_idents map_comps fun_sel k m
     exclsss =
-  mk_primcorec_prelude ctxt defs (fun_sel RS trans) THEN
-  mk_primcorec_cases_tac ctxt k m exclsss THEN
+  prelude_tac ctxt defs (fun_sel RS trans) THEN
+  cases_tac ctxt k m exclsss THEN
   HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' rtac ext ORELSE'
     eresolve_tac falseEs ORELSE'
     resolve_tac split_connectI ORELSE'
@@ -129,9 +134,9 @@
     eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
     etac notE THEN' atac ORELSE'
     (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt
-       (@{thms id_def o_def split_def sum.cases} @ map_comps @ map_idents)))));
+       (@{thms fst_conv snd_conv id_def o_def split_def sum.cases} @ map_comps @ map_idents)))));
 
-fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse disc_fun_opt sel_funs =
+fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs =
   HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN'
     (the_default (K all_tac) (Option.map rtac disc_fun_opt)) THEN' REPEAT_DETERM_N m o atac) THEN
   unfold_thms_tac ctxt (unfold_lets @ sel_funs) THEN HEADGOAL (rtac refl);
@@ -148,13 +153,13 @@
     end
   | _ => split);
 
-fun mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m fun_ctr =
+fun raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m fun_ctr =
   let
     val splits' =
       map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits)
   in
     HEADGOAL (REPEAT o (resolve_tac (splits' @ split_connectI))) THEN
-    mk_primcorec_prelude ctxt [] (fun_ctr RS trans) THEN
+    prelude_tac ctxt [] (fun_ctr RS trans) THEN
     HEADGOAL ((REPEAT_DETERM_N m o mk_primcorec_assumption_tac ctxt discIs) THEN'
       SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
       (rtac refl ORELSE' atac ORELSE'
@@ -183,7 +188,7 @@
          ||> (fn thm => [rulify_nchotomy n nchotomy RS thm] handle THM _ => [thm])
          |> op @));
   in
-    EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)
+    EVERY (map2 (raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)
       ms' fun_ctrs') THEN
     IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN
       HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI)))
@@ -191,7 +196,7 @@
 
 fun mk_primcorec_code_of_raw_code_tac ctxt distincts splits raw =
   HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN'
-    SELECT_GOAL (unfold_thms_tac ctxt [Let_def]) THEN' REPEAT_DETERM o
+    SELECT_GOAL (unfold_thms_tac ctxt unfold_lets) THEN' REPEAT_DETERM o
     (rtac refl ORELSE' atac ORELSE'
      resolve_tac split_connectI ORELSE'
      Splitter.split_tac (split_if :: splits) ORELSE'