1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 17 21:13:30 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 17 21:13:30 2012 +0200
     1.3 @@ -13,9 +13,8 @@
     1.4    val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
     1.5      tactic
     1.6    val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
     1.7 -  val mk_induct_tac: Proof.context -> int list -> int list list ->
     1.8 -    ((int * int) * (int * int)) list list list -> thm list -> thm -> thm list -> thm list list ->
     1.9 -    tactic
    1.10 +  val mk_induct_tac: Proof.context -> int list -> int list list -> int list list list -> thm list ->
    1.11 +    thm -> thm list -> thm list list -> tactic
    1.12    val mk_inject_tac: Proof.context -> thm -> thm -> tactic
    1.13    val mk_iter_like_tac: thm list -> thm list -> thm list -> thm -> thm -> Proof.context -> tactic
    1.14  end;
    1.15 @@ -43,53 +42,6 @@
    1.16  
    1.17  val inst_spurious_fs_tac = PRIMITIVE o inst_spurious_fs;
    1.18  
    1.19 -fun mk_set_rhs def T =
    1.20 -  let
    1.21 -    val lhs = snd (Logic.dest_equals (prop_of def));
    1.22 -    val Type (_, Ts0) = domain_type (fastype_of lhs);
    1.23 -    val Type (_, Ts) = domain_type T;
    1.24 -  in
    1.25 -    Term.subst_atomic_types (Ts0 ~~ Ts) lhs
    1.26 -  end;
    1.27 -
    1.28 -val mk_fsts_rhs = mk_set_rhs @{thm fsts_def[abs_def]};
    1.29 -val mk_snds_rhs = mk_set_rhs @{thm snds_def[abs_def]};
    1.30 -val mk_setl_rhs = mk_set_rhs @{thm sum_setl_def[abs_def]};
    1.31 -val mk_setr_rhs = mk_set_rhs @{thm sum_setr_def[abs_def]};
    1.32 -
    1.33 -(* TODO: Put this in "Balanced_Tree" *)
    1.34 -fun balanced_tree_middle n = n div 2;
    1.35 -
    1.36 -val sum_prod_sel_defs =
    1.37 -  @{thms fsts_def[abs_def] snds_def[abs_def] sum_setl_def[abs_def] sum_setr_def[abs_def]};
    1.38 -
    1.39 -fun unfold_sum_prod_sets ctxt ms thm =
    1.40 -  let
    1.41 -    fun unf_prod 0 f = f
    1.42 -      | unf_prod 1 f = f
    1.43 -      | unf_prod m (t1 $ (t2 $ (t3 $ (t4 $ Const (@{const_name fsts}, T1) $
    1.44 -          (t5 $ Const (@{const_name snds}, T2) $ t6)))) $ (t7 $ f $ g)) =
    1.45 -        t1 $ (t2 $ (t3 $ (t4 $ mk_fsts_rhs T1 $ (t5 $ mk_snds_rhs T2 $ t6))))
    1.46 -          $ (t7 $ f $ unf_prod (m - 1) g)
    1.47 -      | unf_prod _ f = f;
    1.48 -    fun unf_sum [m] f = unf_prod m f
    1.49 -      | unf_sum ms (t1 $ (t2 $ (t3 $ (t4 $ Const (@{const_name sum_setl}, T1) $
    1.50 -          (t5 $ Const (@{const_name sum_setr}, T2) $ t6)))) $ (t7 $ f $ g)) =
    1.51 -        let val (ms1, ms2) = chop (balanced_tree_middle (length ms)) ms in
    1.52 -          t1 $ (t2 $ (t3 $ (t4 $ mk_setl_rhs T1 $ (t5 $ mk_setr_rhs T2 $ t6))))
    1.53 -            $ (t7 $ unf_sum ms1 f $ unf_sum ms2 g)
    1.54 -        end
    1.55 -      | unf_sum _ f = f;
    1.56 -
    1.57 -    val P = prop_of thm;
    1.58 -    val P' = Logic.dest_equals P ||> unf_sum ms;
    1.59 -    val goal = Logic.mk_implies (P, Logic.mk_equals P');
    1.60 -  in
    1.61 -    Skip_Proof.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
    1.62 -      Local_Defs.unfold_tac ctxt sum_prod_sel_defs THEN atac 1)
    1.63 -    OF [thm]
    1.64 -  end;
    1.65 -
    1.66  fun mk_case_tac ctxt n k m case_def ctr_def unf_fld =
    1.67    Local_Defs.unfold_tac ctxt [case_def, ctr_def, unf_fld] THEN
    1.68    (rtac (mk_sum_casesN_balanced n k RS ssubst) THEN'
    1.69 @@ -137,44 +89,42 @@
    1.70  
    1.71  val maybe_singletonI_tac = atac ORELSE' rtac @{thm singletonI};
    1.72  
    1.73 -fun solve_prem_prem_tac ctxt =
    1.74 -  SELECT_GOAL (Local_Defs.unfold_tac ctxt
    1.75 -    @{thms Un_iff eq_UN_compreh_Un mem_Collect_eq mem_UN_compreh_eq}) THEN'
    1.76 -  REPEAT o (etac @{thm rev_bexI} ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
    1.77 -  (atac ORELSE' rtac refl ORELSE' rtac @{thm singletonI});
    1.78 +val solve_prem_prem_tac =
    1.79 +  REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
    1.80 +    hyp_subst_tac ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
    1.81 +  (rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI});
    1.82  
    1.83  val induct_prem_prem_thms =
    1.84    @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex_eq_empty UN_compreh_bex_eq_singleton
    1.85 -      UN_insert Un_assoc Un_empty_left Un_empty_right Union_Un_distrib collect_def[abs_def] fst_conv
    1.86 -      image_def o_apply snd_conv snd_prod_fun sum.cases sup_bot_right fst_map_pair map_pair_simp
    1.87 -      sum_map.simps};
    1.88 +      UN_insert Un_assoc Un_empty_left Un_empty_right Un_iff Union_Un_distrib collect_def[abs_def]
    1.89 +      eq_UN_compreh_Un fst_conv image_def o_apply snd_conv snd_prod_fun sum.cases sup_bot_right
    1.90 +      fst_map_pair map_pair_simp mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps
    1.91 +      sum_set_simps};
    1.92  
    1.93 -fun mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs =
    1.94 -  EVERY' (maps (fn ((pp, jj), (qq, kk)) =>
    1.95 -    [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
    1.96 +fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs =
    1.97 +  EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
    1.98       SELECT_GOAL (Local_Defs.unfold_tac ctxt
    1.99         (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
   1.100 -     solve_prem_prem_tac ctxt]) (rev ppjjqqkks)) 1;
   1.101 +     solve_prem_prem_tac]) (rev kks)) 1;
   1.102  
   1.103 -fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjqqkks =
   1.104 -  let val r = length ppjjqqkks in
   1.105 +fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k kks =
   1.106 +  let val r = length kks in
   1.107      EVERY' [select_prem_tac n (rotate_tac 1) k, rotate_tac ~1, hyp_subst_tac,
   1.108        REPEAT_DETERM_N m o (dtac meta_spec THEN' rotate_tac ~1)] 1 THEN
   1.109      EVERY [REPEAT_DETERM_N r
   1.110          (rotate_tac ~1 1 THEN dtac meta_mp 1 THEN rotate_tac 1 1 THEN prefer_tac 2),
   1.111        if r > 0 then PRIMITIVE Raw_Simplifier.norm_hhf else all_tac, atac 1,
   1.112 -      mk_induct_leverage_prem_prems_tac ctxt nn ppjjqqkks set_natural's pre_set_defs]
   1.113 +      mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs]
   1.114    end;
   1.115  
   1.116 -fun mk_induct_tac ctxt ns mss ppjjqqkksss ctr_defs fld_induct' set_natural's pre_set_defss =
   1.117 +fun mk_induct_tac ctxt ns mss kkss ctr_defs fld_induct' set_natural's pre_set_defss =
   1.118    let
   1.119      val nn = length ns;
   1.120      val n = Integer.sum ns;
   1.121 -    val pre_set_defss' = map2 (map o unfold_sum_prod_sets ctxt) mss pre_set_defss;
   1.122    in
   1.123      Local_Defs.unfold_tac ctxt ctr_defs THEN rtac fld_induct' 1 THEN inst_spurious_fs_tac ctxt THEN
   1.124      EVERY (map4 (EVERY oooo map3 o mk_induct_discharge_prem_tac ctxt nn n set_natural's)
   1.125 -      pre_set_defss' mss (unflat mss (1 upto n)) ppjjqqkksss)
   1.126 +      pre_set_defss mss (unflat mss (1 upto n)) kkss)
   1.127    end;
   1.128  
   1.129  end;