# HG changeset patch
# User blanchet
# Date 1347909210 -7200
# Node ID b017e1dbc77c1c6291a62ceb58d8aa7362444ca2
# Parent  6d05b8452cf31ae001f3f1b1c1bce0bf36382f5c
clean unfolding of prod and sum sets

diff -r 6d05b8452cf3 -r b017e1dbc77c src/HOL/Codatatype/BNF_FP.thy
--- a/src/HOL/Codatatype/BNF_FP.thy	Mon Sep 17 21:13:30 2012 +0200
+++ b/src/HOL/Codatatype/BNF_FP.thy	Mon Sep 17 21:13:30 2012 +0200
@@ -123,14 +123,17 @@
 "\<exists>y. (\<exists>x\<in>A. y = F x) \<and> z \<in> y \<Longrightarrow> z \<in> \<Union>{y. \<exists>x\<in>A. y = {y. \<exists>y'\<in>F x. y = y'}}"
 by blast
 
-lemma induct_set_step: "\<lbrakk>B \<in> A; c \<in> f B\<rbrakk> \<Longrightarrow> \<exists>C. (\<exists>a \<in> A. C = f a) \<and> c \<in> C"
-apply (rule exI)
-apply (rule conjI)
- apply (rule bexI)
-  apply (rule refl)
- apply assumption
-apply assumption
-done
+lemma mem_compreh_eq_iff:
+"z \<in> {y. \<exists>x\<in>Axx. y = f x} = (\<exists> x. x \<in> Axx & z \<in> {f x})"
+by blast
+
+lemma ex_mem_singleton: "(\<exists>y. y \<in> A \<and> y \<in> {x}) = (x \<in> A)"
+by simp
+
+lemma induct_set_step:
+"\<lbrakk>b \<in> A; c \<in> F b\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> A \<and> c \<in> F x"
+"\<lbrakk>B \<in> A; c \<in> f B\<rbrakk> \<Longrightarrow> \<exists>C. (\<exists>a \<in> A. C = f a) \<and>c \<in> C"
+by blast+
 
 ML_file "Tools/bnf_fp_util.ML"
 ML_file "Tools/bnf_fp_sugar_tactics.ML"
diff -r 6d05b8452cf3 -r b017e1dbc77c src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 17 21:13:30 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 17 21:13:30 2012 +0200
@@ -602,6 +602,7 @@
               end;
 
             val ppjjqqkksss = map (map (mk_raw_prem_prems_indices o #2)) raw_premss;
+val _ = tracing ("val ppjjqqkksss = " ^ PolyML.makestring ppjjqqkksss) (*###*)
 
             val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
 
diff -r 6d05b8452cf3 -r b017e1dbc77c src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 17 21:13:30 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 17 21:13:30 2012 +0200
@@ -43,6 +43,52 @@
 
 val inst_spurious_fs_tac = PRIMITIVE o inst_spurious_fs;
 
+fun mk_set_rhs set_lhs T =
+  let
+    val Type (_, Ts0) = domain_type (fastype_of set_lhs);
+    val Type (_, Ts) = domain_type T;
+  in
+    Term.subst_atomic_types (Ts0 ~~ Ts) set_lhs
+  end;
+
+val mk_fsts_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm fsts_def[abs_def]})));
+val mk_snds_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm snds_def[abs_def]})));
+val mk_setl_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm sum_setl_def[abs_def]})));
+val mk_setr_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm sum_setr_def[abs_def]})));
+
+(* TODO: Put this in "Balanced_Tree" *)
+fun balanced_tree_middle n = n div 2;
+
+val sum_prod_sel_defs =
+  @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
+
+fun unfold_sum_prod_sets ctxt ms thm =
+  let
+    fun unf_prod 0 f = f
+      | unf_prod 1 f = f
+      | unf_prod m (t1 $ (t2 $ (t3 $ (t4 $ Const (_, T1) $ (t5 $ Const (_, T2) $ t6))))
+          $ (t7 $ f $ g)) =
+        t1 $ (t2 $ (t3 $ (t4 $ mk_fsts_rhs T1 $ (t5 $ mk_snds_rhs T2 $ t6))))
+          $ (t7 $ f $ unf_prod (m - 1) g)
+      | unf_prod _ f = f;
+    fun unf_sum [m] f = unf_prod m f
+      | unf_sum ms (t1 $ (t2 $ (t3 $ (t4 $ Const (_, T1) $ (t5 $ Const (_, T2) $ t6))))
+          $ (t7 $ f $ g)) =
+        let val (ms1, ms2) = chop (balanced_tree_middle (length ms)) ms in
+          t1 $ (t2 $ (t3 $ (t4 $ mk_setl_rhs T1 $ (t5 $ mk_setr_rhs T2 $ t6))))
+            $ (t7 $ unf_sum ms1 f $ unf_sum ms2 g)
+        end
+      | unf_sum _ f = f;
+
+    val P = prop_of thm;
+    val P' = Logic.dest_equals P ||> unf_sum ms;
+    val goal = Logic.mk_implies (P, Logic.mk_equals P');
+  in
+    Skip_Proof.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
+      Local_Defs.unfold_tac ctxt sum_prod_sel_defs THEN atac 1)
+    OF [thm]
+  end;
+
 fun mk_case_tac ctxt n k m case_def ctr_def unf_fld =
   Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN
   (rtac (mk_sum_casesN_balanced n k RS ssubst) THEN'
@@ -88,14 +134,14 @@
   Local_Defs.unfold_tac ctxt @{thms id_def} THEN
   TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
 
-(* TODO: Get rid of "auto_tac" (or at least use a naked context) *)
+val maybe_singletonI_tac = atac ORELSE' rtac @{thm singletonI};
 
-fun mk_induct_prem_prem_endgame_tac _ 0 = atac ORELSE' rtac @{thm singletonI}
+fun mk_induct_prem_prem_endgame_tac _ 0 = maybe_singletonI_tac
   | mk_induct_prem_prem_endgame_tac ctxt qq =
     REPEAT_DETERM_N qq o
-      (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
-       etac @{thm induct_set_step}) THEN'
-    atac ORELSE' SELECT_GOAL (auto_tac ctxt);
+      (SELECT_GOAL (Local_Defs.unfold_tac ctxt
+         @{thms trans[OF Union_iff bex_simps(6)] mem_compreh_eq_iff ex_mem_singleton}) THEN'
+       eresolve_tac @{thms induct_set_step}) THEN' maybe_singletonI_tac;
 
 fun gen_UN_comprehI_tac UnI = REPEAT_DETERM o resolve_tac @{thms mem_UN_comprehI} THEN' rtac UnI;
 
@@ -109,19 +155,12 @@
       image_def o_apply snd_conv snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp
       sum_map.simps};
 
-(* These rules interfere with the "set_natural'" properties of "sum" and "prod", so we explicitly
-   delay them. *)
-val induct_prem_prem_thms_delayed =
-  @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
-
 fun mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs =
   EVERY' (maps (fn ((pp, jj), (qq, kk)) =>
     [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
      SELECT_GOAL (Local_Defs.unfold_tac ctxt
        (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
-     SELECT_GOAL (Local_Defs.unfold_tac ctxt
-       (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
-     gen_UnIN_tac pp jj THEN' mk_induct_prem_prem_endgame_tac ctxt qq]) (rev ppjjqqkks)) 1;
+     gen_UnIN_tac pp jj, mk_induct_prem_prem_endgame_tac ctxt qq]) (rev ppjjqqkks)) 1;
 
 fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjqqkks =
   let val r = length ppjjqqkks in
@@ -137,10 +176,11 @@
   let
     val nn = length ns;
     val n = Integer.sum ns;
+    val pre_set_defss' = map2 (map o unfold_sum_prod_sets ctxt) mss pre_set_defss;
   in
     Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN inst_spurious_fs_tac ctxt THEN
     EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's)
-      pre_set_defss mss (unflat mss (1 upto n)) ppjjqqkksss)
+      pre_set_defss' mss (unflat mss (1 upto n)) ppjjqqkksss)
   end;
 
 end;