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 @@ -137,6 +137,18 @@
     1.4  lemma ex_mem_singleton: "(\<exists>y. y \<in> A \<and> y \<in> {x}) = (x \<in> A)"
     1.5  by simp
     1.6  
     1.7 +lemma prod_set_simps:
     1.8 +"fsts (x, y) = {x}"
     1.9 +"snds (x, y) = {y}"
    1.10 +unfolding fsts_def snds_def by simp+
    1.11 +
    1.12 +lemma sum_set_simps:
    1.13 +"sum_setl (Inl x) = {x}"
    1.14 +"sum_setl (Inr x) = {}"
    1.15 +"sum_setr (Inl x) = {}"
    1.16 +"sum_setr (Inr x) = {x}"
    1.17 +unfolding sum_setl_def sum_setr_def by simp+
    1.18 +
    1.19  lemma induct_set_step:
    1.20  "\<lbrakk>b \<in> A; c \<in> F b\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> A \<and> c \<in> F x"
    1.21  "\<lbrakk>B \<in> A; c \<in> f B\<rbrakk> \<Longrightarrow> \<exists>C. (\<exists>a \<in> A. C = f a) \<and>c \<in> C"

     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 @@ -590,25 +590,13 @@
     2.4                  HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
     2.5                    (map2 (curry (op $)) phis vs)));
     2.6  
     2.7 -            fun mk_raw_prem_prems_indices pprems =
     2.8 -              let
     2.9 -                fun has_index kk (_, (kk', _)) = kk' = kk;
    2.10 -                val buckets = Library.partition_list has_index 1 nn pprems;
    2.11 -                val pps = map length buckets;
    2.12 -              in
    2.13 -                map (fn pprem as (xysets, (kk, _)) =>
    2.14 -                  ((nth pps (kk - 1), find_index (curry (op =) pprem) (nth buckets (kk - 1)) + 1),
    2.15 -                   (length xysets, kk))) pprems
    2.16 -              end;
    2.17 -
    2.18 -            val ppjjqqkksss = map (map (mk_raw_prem_prems_indices o #2)) raw_premss;
    2.19 -val _ = tracing ("val ppjjqqkksss = " ^ PolyML.makestring ppjjqqkksss) (*###*)
    2.20 +            val kksss = map (map (map (fst o snd) o #2)) raw_premss;
    2.21  
    2.22              val fld_induct' = fp_induct OF (map mk_sumEN_tupled_balanced mss);
    2.23  
    2.24              val induct_thm =
    2.25                Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
    2.26 -                mk_induct_tac ctxt ns mss ppjjqqkksss (flat ctr_defss) fld_induct'
    2.27 +                mk_induct_tac ctxt ns mss kksss (flat ctr_defss) fld_induct'
    2.28                    nested_set_natural's pre_set_defss)
    2.29                |> singleton (Proof_Context.export names_lthy lthy)
    2.30            in

     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 @@ -13,9 +13,8 @@
     3.4    val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
     3.5      tactic
     3.6    val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
     3.7 -  val mk_induct_tac: Proof.context -> int list -> int list list ->
     3.8 -    ((int * int) * (int * int)) list list list -> thm list -> thm -> thm list -> thm list list ->
     3.9 -    tactic
    3.10 +  val mk_induct_tac: Proof.context -> int list -> int list list -> int list list list -> thm list ->
    3.11 +    thm -> thm list -> thm list list -> tactic
    3.12    val mk_inject_tac: Proof.context -> thm -> thm -> tactic
    3.13    val mk_iter_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic
    3.14  end;
    3.15 @@ -43,53 +42,6 @@
    3.16  
    3.17  val inst_spurious_fs_tac = PRIMITIVE o inst_spurious_fs;
    3.18  
    3.19 -fun mk_set_rhs def T =
    3.20 -  let
    3.21 -    val lhs = snd (Logic.dest_equals (prop_of def));
    3.22 -    val Type (_, Ts0) = domain_type (fastype_of lhs);
    3.23 -    val Type (_, Ts) = domain_type T;
    3.24 -  in
    3.25 -    Term.subst_atomic_types (Ts0 ~~ Ts) lhs
    3.26 -  end;
    3.27 -
    3.28 -val mk_fsts_rhs = mk_set_rhs @{thm fsts_def[abs_def]};
    3.29 -val mk_snds_rhs = mk_set_rhs @{thm snds_def[abs_def]};
    3.30 -val mk_setl_rhs = mk_set_rhs @{thm sum_setl_def[abs_def]};
    3.31 -val mk_setr_rhs = mk_set_rhs @{thm sum_setr_def[abs_def]};
    3.32 -
    3.33 -(* TODO: Put this in "Balanced_Tree" *)
    3.34 -fun balanced_tree_middle n = n div 2;
    3.35 -
    3.36 -val sum_prod_sel_defs =
    3.37 -  @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
    3.38 -
    3.39 -fun unfold_sum_prod_sets ctxt ms thm =
    3.40 -  let
    3.41 -    fun unf_prod 0 f = f
    3.42 -      | unf_prod 1 f = f
    3.43 -      | unf_prod m (t1 $ (t2 $ (t3 $ (t4 $ Const (@{const_name fsts}, T1) $
    3.44 -          (t5 $ Const (@{const_name snds}, T2) $ t6)))) $ (t7 $ f $ g)) =
    3.45 -        t1 $ (t2 $ (t3 $ (t4 $ mk_fsts_rhs T1 $ (t5 $ mk_snds_rhs T2 $ t6))))
    3.46 -          $ (t7 $ f $ unf_prod (m - 1) g)
    3.47 -      | unf_prod _ f = f;
    3.48 -    fun unf_sum [m] f = unf_prod m f
    3.49 -      | unf_sum ms (t1 $ (t2 $ (t3 $ (t4 $ Const (@{const_name sum_setl}, T1) $
    3.50 -          (t5 $ Const (@{const_name sum_setr}, T2) $ t6)))) $ (t7 $ f $ g)) =
    3.51 -        let val (ms1, ms2) = chop (balanced_tree_middle (length ms)) ms in
    3.52 -          t1 $ (t2 $ (t3 $ (t4 $ mk_setl_rhs T1 $ (t5 $ mk_setr_rhs T2 $ t6))))
    3.53 -            $ (t7 $ unf_sum ms1 f $ unf_sum ms2 g)
    3.54 -        end
    3.55 -      | unf_sum _ f = f;
    3.56 -
    3.57 -    val P = prop_of thm;
    3.58 -    val P' = Logic.dest_equals P ||> unf_sum ms;
    3.59 -    val goal = Logic.mk_implies (P, Logic.mk_equals P');
    3.60 -  in
    3.61 -    Skip_Proof.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
    3.62 -      Local_Defs.unfold_tac ctxt sum_prod_sel_defs THEN atac 1)
    3.63 -    OF [thm]
    3.64 -  end;
    3.65 -
    3.66  fun mk_case_tac ctxt n k m case_def ctr_def unf_fld =
    3.67    Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN
    3.68    (rtac (mk_sum_casesN_balanced n k RS ssubst) THEN'
    3.69 @@ -137,44 +89,42 @@
    3.70  
    3.71  val maybe_singletonI_tac = atac ORELSE' rtac @{thm singletonI};
    3.72  
    3.73 -fun solve_prem_prem_tac ctxt =
    3.74 -  SELECT_GOAL (Local_Defs.unfold_tac ctxt
    3.75 -    @{thms Un_iff eq_UN_compreh_Un mem_Collect_eq mem_UN_compreh_eq}) THEN'
    3.76 -  REPEAT o (etac @{thm rev_bexI} ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
    3.77 -  (atac ORELSE' rtac refl ORELSE' rtac @{thm singletonI});
    3.78 +val solve_prem_prem_tac =
    3.79 +  REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
    3.80 +    hyp_subst_tac ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
    3.81 +  (rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI});
    3.82  
    3.83  val induct_prem_prem_thms =
    3.84    @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex_eq_empty UN_compreh_bex_eq_singleton
    3.85 -      UN_insert Un_assoc Un_empty_left Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv
    3.86 -      image_def o_apply snd_conv snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp
    3.87 -      sum_map.simps};
    3.88 +      UN_insert Un_assoc Un_empty_left Un_empty_right Un_iff Union_Un_distrib collect_def[abs_def]
    3.89 +      eq_UN_compreh_Un fst_conv image_def o_apply snd_conv snd_prod_fun sum.cases sup_bot_right
    3.90 +      fst_map_pair map_pair_simp mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps
    3.91 +      sum_set_simps};
    3.92  
    3.93 -fun mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs =
    3.94 -  EVERY' (maps (fn ((pp, jj), (qq, kk)) =>
    3.95 -    [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
    3.96 +fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs =
    3.97 +  EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
    3.98       SELECT_GOAL (Local_Defs.unfold_tac ctxt
    3.99         (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
   3.100 -     solve_prem_prem_tac ctxt]) (rev ppjjqqkks)) 1;
   3.101 +     solve_prem_prem_tac]) (rev kks)) 1;
   3.102  
   3.103 -fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjqqkks =
   3.104 -  let val r = length ppjjqqkks in
   3.105 +fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k kks =
   3.106 +  let val r = length kks in
   3.107      EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,
   3.108        REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN
   3.109      EVERY [REPEAT_DETERM_N r
   3.110          (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2),
   3.111        if r > 0 then PRIMITIVE Raw_Simplifier.norm_hhf else all_tac, atac 1,
   3.112 -      mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs]
   3.113 +      mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs]
   3.114    end;
   3.115  
   3.116 -fun mk_induct_tac ctxt ns mss ppjjqqkksss ctr_defs fld_induct' set_natural's pre_set_defss =
   3.117 +fun mk_induct_tac ctxt ns mss kkss ctr_defs fld_induct' set_natural's pre_set_defss =
   3.118    let
   3.119      val nn = length ns;
   3.120      val n = Integer.sum ns;
   3.121 -    val pre_set_defss' = map2 (map o unfold_sum_prod_sets ctxt) mss pre_set_defss;
   3.122    in
   3.123      Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN inst_spurious_fs_tac ctxt THEN
   3.124      EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's)
   3.125 -      pre_set_defss' mss (unflat mss (1 upto n)) ppjjqqkksss)
   3.126 +      pre_set_defss mss (unflat mss (1 upto n)) kkss)
   3.127    end;
   3.128  
   3.129  end;