1.1 --- a/src/HOL/Codatatype/BNF_FP.thy	Mon Sep 17 21:13:30 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/BNF_FP.thy	Mon Sep 17 21:13:30 2012 +0200
     1.3 @@ -123,14 +123,17 @@
     1.4  "\<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'}}"
     1.5  by blast
     1.6  
     1.7 -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"
     1.8 -apply (rule exI)
     1.9 -apply (rule conjI)
    1.10 - apply (rule bexI)
    1.11 -  apply (rule refl)
    1.12 - apply assumption
    1.13 -apply assumption
    1.14 -done
    1.15 +lemma mem_compreh_eq_iff:
    1.16 +"z \<in> {y. \<exists>x\<in>Axx. y = f x} = (\<exists> x. x \<in> Axx & z \<in> {f x})"
    1.17 +by blast
    1.18 +
    1.19 +lemma ex_mem_singleton: "(\<exists>y. y \<in> A \<and> y \<in> {x}) = (x \<in> A)"
    1.20 +by simp
    1.21 +
    1.22 +lemma induct_set_step:
    1.23 +"\<lbrakk>b \<in> A; c \<in> F b\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> A \<and> c \<in> F x"
    1.24 +"\<lbrakk>B \<in> A; c \<in> f B\<rbrakk> \<Longrightarrow> \<exists>C. (\<exists>a \<in> A. C = f a) \<and>c \<in> C"
    1.25 +by blast+
    1.26  
    1.27  ML_file "Tools/bnf_fp_util.ML"
    1.28  ML_file "Tools/bnf_fp_sugar_tactics.ML"

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 17 21:13:30 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 17 21:13:30 2012 +0200
     2.3 @@ -602,6 +602,7 @@
     2.4                end;
     2.5  
     2.6              val ppjjqqkksss = map (map (mk_raw_prem_prems_indices o #2)) raw_premss;
     2.7 +val _ = tracing ("val ppjjqqkksss = " ^ PolyML.makestring ppjjqqkksss) (*###*)
     2.8  
     2.9              val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
    2.10  

     3.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 17 21:13:30 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 17 21:13:30 2012 +0200
     3.3 @@ -43,6 +43,52 @@
     3.4  
     3.5  val inst_spurious_fs_tac = PRIMITIVE o inst_spurious_fs;
     3.6  
     3.7 +fun mk_set_rhs set_lhs T =
     3.8 +  let
     3.9 +    val Type (_, Ts0) = domain_type (fastype_of set_lhs);
    3.10 +    val Type (_, Ts) = domain_type T;
    3.11 +  in
    3.12 +    Term.subst_atomic_types (Ts0 ~~ Ts) set_lhs
    3.13 +  end;
    3.14 +
    3.15 +val mk_fsts_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm fsts_def[abs_def]})));
    3.16 +val mk_snds_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm snds_def[abs_def]})));
    3.17 +val mk_setl_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm sum_setl_def[abs_def]})));
    3.18 +val mk_setr_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm sum_setr_def[abs_def]})));
    3.19 +
    3.20 +(* TODO: Put this in "Balanced_Tree" *)
    3.21 +fun balanced_tree_middle n = n div 2;
    3.22 +
    3.23 +val sum_prod_sel_defs =
    3.24 +  @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
    3.25 +
    3.26 +fun unfold_sum_prod_sets ctxt ms thm =
    3.27 +  let
    3.28 +    fun unf_prod 0 f = f
    3.29 +      | unf_prod 1 f = f
    3.30 +      | unf_prod m (t1 $ (t2 $ (t3 $ (t4 $ Const (_, T1) $ (t5 $ Const (_, T2) $ t6))))
    3.31 +          $ (t7 $ f $ g)) =
    3.32 +        t1 $ (t2 $ (t3 $ (t4 $ mk_fsts_rhs T1 $ (t5 $ mk_snds_rhs T2 $ t6))))
    3.33 +          $ (t7 $ f $ unf_prod (m - 1) g)
    3.34 +      | unf_prod _ f = f;
    3.35 +    fun unf_sum [m] f = unf_prod m f
    3.36 +      | unf_sum ms (t1 $ (t2 $ (t3 $ (t4 $ Const (_, T1) $ (t5 $ Const (_, T2) $ t6))))
    3.37 +          $ (t7 $ f $ g)) =
    3.38 +        let val (ms1, ms2) = chop (balanced_tree_middle (length ms)) ms in
    3.39 +          t1 $ (t2 $ (t3 $ (t4 $ mk_setl_rhs T1 $ (t5 $ mk_setr_rhs T2 $ t6))))
    3.40 +            $ (t7 $ unf_sum ms1 f $ unf_sum ms2 g)
    3.41 +        end
    3.42 +      | unf_sum _ f = f;
    3.43 +
    3.44 +    val P = prop_of thm;
    3.45 +    val P' = Logic.dest_equals P ||> unf_sum ms;
    3.46 +    val goal = Logic.mk_implies (P, Logic.mk_equals P');
    3.47 +  in
    3.48 +    Skip_Proof.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
    3.49 +      Local_Defs.unfold_tac ctxt sum_prod_sel_defs THEN atac 1)
    3.50 +    OF [thm]
    3.51 +  end;
    3.52 +
    3.53  fun mk_case_tac ctxt n k m case_def ctr_def unf_fld =
    3.54    Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN
    3.55    (rtac (mk_sum_casesN_balanced n k RS ssubst) THEN'
    3.56 @@ -88,14 +134,14 @@
    3.57    Local_Defs.unfold_tac ctxt @{thms id_def} THEN
    3.58    TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
    3.59  
    3.60 -(* TODO: Get rid of "auto_tac" (or at least use a naked context) *)
    3.61 +val maybe_singletonI_tac = atac ORELSE' rtac @{thm singletonI};
    3.62  
    3.63 -fun mk_induct_prem_prem_endgame_tac _ 0 = atac ORELSE' rtac @{thm singletonI}
    3.64 +fun mk_induct_prem_prem_endgame_tac _ 0 = maybe_singletonI_tac
    3.65    | mk_induct_prem_prem_endgame_tac ctxt qq =
    3.66      REPEAT_DETERM_N qq o
    3.67 -      (SELECT_GOAL (Local_Defs.unfold_tac ctxt @{thms Union_iff bex_simps(6)}) THEN'
    3.68 -       etac @{thm induct_set_step}) THEN'
    3.69 -    atac ORELSE' SELECT_GOAL (auto_tac ctxt);
    3.70 +      (SELECT_GOAL (Local_Defs.unfold_tac ctxt
    3.71 +         @{thms trans[OF Union_iff bex_simps(6)] mem_compreh_eq_iff ex_mem_singleton}) THEN'
    3.72 +       eresolve_tac @{thms induct_set_step}) THEN' maybe_singletonI_tac;
    3.73  
    3.74  fun gen_UN_comprehI_tac UnI = REPEAT_DETERM o resolve_tac @{thms mem_UN_comprehI} THEN' rtac UnI;
    3.75  
    3.76 @@ -109,19 +155,12 @@
    3.77        image_def o_apply snd_conv snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp
    3.78        sum_map.simps};
    3.79  
    3.80 -(* These rules interfere with the "set_natural'" properties of "sum" and "prod", so we explicitly
    3.81 -   delay them. *)
    3.82 -val induct_prem_prem_thms_delayed =
    3.83 -  @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
    3.84 -
    3.85  fun mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs =
    3.86    EVERY' (maps (fn ((pp, jj), (qq, kk)) =>
    3.87      [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
    3.88       SELECT_GOAL (Local_Defs.unfold_tac ctxt
    3.89         (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
    3.90 -     SELECT_GOAL (Local_Defs.unfold_tac ctxt
    3.91 -       (induct_prem_prem_thms_delayed @ induct_prem_prem_thms)),
    3.92 -     gen_UnIN_tac pp jj THEN' mk_induct_prem_prem_endgame_tac ctxt qq]) (rev ppjjqqkks)) 1;
    3.93 +     gen_UnIN_tac pp jj, mk_induct_prem_prem_endgame_tac ctxt qq]) (rev ppjjqqkks)) 1;
    3.94  
    3.95  fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjqqkks =
    3.96    let val r = length ppjjqqkks in
    3.97 @@ -137,10 +176,11 @@
    3.98    let
    3.99      val nn = length ns;
   3.100      val n = Integer.sum ns;
   3.101 +    val pre_set_defss' = map2 (map o unfold_sum_prod_sets ctxt) mss pre_set_defss;
   3.102    in
   3.103      Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN inst_spurious_fs_tac ctxt THEN
   3.104      EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's)
   3.105 -      pre_set_defss mss (unflat mss (1 upto n)) ppjjqqkksss)
   3.106 +      pre_set_defss' mss (unflat mss (1 upto n)) ppjjqqkksss)
   3.107    end;
   3.108  
   3.109  end;