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 @@ -43,18 +43,19 @@
     1.4  
     1.5  val inst_spurious_fs_tac = PRIMITIVE o inst_spurious_fs;
     1.6  
     1.7 -fun mk_set_rhs set_lhs T =
     1.8 +fun mk_set_rhs def T =
     1.9    let
    1.10 -    val Type (_, Ts0) = domain_type (fastype_of set_lhs);
    1.11 +    val lhs = snd (Logic.dest_equals (prop_of def));
    1.12 +    val Type (_, Ts0) = domain_type (fastype_of lhs);
    1.13      val Type (_, Ts) = domain_type T;
    1.14    in
    1.15 -    Term.subst_atomic_types (Ts0 ~~ Ts) set_lhs
    1.16 +    Term.subst_atomic_types (Ts0 ~~ Ts) lhs
    1.17    end;
    1.18  
    1.19 -val mk_fsts_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm fsts_def[abs_def]})));
    1.20 -val mk_snds_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm snds_def[abs_def]})));
    1.21 -val mk_setl_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm sum_setl_def[abs_def]})));
    1.22 -val mk_setr_rhs = mk_set_rhs (snd (Logic.dest_equals (prop_of @{thm sum_setr_def[abs_def]})));
    1.23 +val mk_fsts_rhs = mk_set_rhs @{thm fsts_def[abs_def]};
    1.24 +val mk_snds_rhs = mk_set_rhs @{thm snds_def[abs_def]};
    1.25 +val mk_setl_rhs = mk_set_rhs @{thm sum_setl_def[abs_def]};
    1.26 +val mk_setr_rhs = mk_set_rhs @{thm sum_setr_def[abs_def]};
    1.27  
    1.28  (* TODO: Put this in "Balanced_Tree" *)
    1.29  fun balanced_tree_middle n = n div 2;
    1.30 @@ -66,14 +67,14 @@
    1.31    let
    1.32      fun unf_prod 0 f = f
    1.33        | unf_prod 1 f = f
    1.34 -      | unf_prod m (t1 $ (t2 $ (t3 $ (t4 $ Const (_, T1) $ (t5 $ Const (_, T2) $ t6))))
    1.35 -          $ (t7 $ f $ g)) =
    1.36 +      | unf_prod m (t1 $ (t2 $ (t3 $ (t4 $ Const (@{const_name fsts}, T1) $
    1.37 +          (t5 $ Const (@{const_name snds}, T2) $ t6)))) $ (t7 $ f $ g)) =
    1.38          t1 $ (t2 $ (t3 $ (t4 $ mk_fsts_rhs T1 $ (t5 $ mk_snds_rhs T2 $ t6))))
    1.39            $ (t7 $ f $ unf_prod (m - 1) g)
    1.40        | unf_prod _ f = f;
    1.41      fun unf_sum [m] f = unf_prod m f
    1.42 -      | unf_sum ms (t1 $ (t2 $ (t3 $ (t4 $ Const (_, T1) $ (t5 $ Const (_, T2) $ t6))))
    1.43 -          $ (t7 $ f $ g)) =
    1.44 +      | unf_sum ms (t1 $ (t2 $ (t3 $ (t4 $ Const (@{const_name sum_setl}, T1) $
    1.45 +          (t5 $ Const (@{const_name sum_setr}, T2) $ t6)))) $ (t7 $ f $ g)) =
    1.46          let val (ms1, ms2) = chop (balanced_tree_middle (length ms)) ms in
    1.47            t1 $ (t2 $ (t3 $ (t4 $ mk_setl_rhs T1 $ (t5 $ mk_setr_rhs T2 $ t6))))
    1.48              $ (t7 $ unf_sum ms1 f $ unf_sum ms2 g)
    1.49 @@ -136,18 +137,11 @@
    1.50  
    1.51  val maybe_singletonI_tac = atac ORELSE' rtac @{thm singletonI};
    1.52  
    1.53 -fun mk_induct_prem_prem_endgame_tac _ 0 = maybe_singletonI_tac
    1.54 -  | mk_induct_prem_prem_endgame_tac ctxt qq =
    1.55 -    REPEAT_DETERM_N qq o
    1.56 -      (SELECT_GOAL (Local_Defs.unfold_tac ctxt
    1.57 -         @{thms trans[OF Union_iff bex_simps(6)] mem_compreh_eq_iff ex_mem_singleton}) THEN'
    1.58 -       eresolve_tac @{thms induct_set_step}) THEN' maybe_singletonI_tac;
    1.59 -
    1.60 -fun gen_UN_comprehI_tac UnI = REPEAT_DETERM o resolve_tac @{thms mem_UN_comprehI} THEN' rtac UnI;
    1.61 -
    1.62 -fun gen_UnIN_tac 1 1 = REPEAT_DETERM o resolve_tac @{thms mem_UN_comprehI'}
    1.63 -  | gen_UnIN_tac _ 1 = gen_UN_comprehI_tac @{thm UnI1} THEN' gen_UnIN_tac 1 1
    1.64 -  | gen_UnIN_tac n k = gen_UN_comprehI_tac @{thm UnI2} THEN' gen_UnIN_tac (n - 1) (k - 1);
    1.65 +fun solve_prem_prem_tac ctxt =
    1.66 +  SELECT_GOAL (Local_Defs.unfold_tac ctxt
    1.67 +    @{thms Un_iff eq_UN_compreh_Un mem_Collect_eq mem_UN_compreh_eq}) THEN'
    1.68 +  REPEAT o (etac @{thm rev_bexI} ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
    1.69 +  (atac ORELSE' rtac refl ORELSE' rtac @{thm singletonI});
    1.70  
    1.71  val induct_prem_prem_thms =
    1.72    @{thms SUP_empty Sup_empty Sup_insert UN_compreh_bex_eq_empty UN_compreh_bex_eq_singleton
    1.73 @@ -160,7 +154,7 @@
    1.74      [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,
    1.75       SELECT_GOAL (Local_Defs.unfold_tac ctxt
    1.76         (pre_set_defs @ set_natural's @ induct_prem_prem_thms)),
    1.77 -     gen_UnIN_tac pp jj, mk_induct_prem_prem_endgame_tac ctxt qq]) (rev ppjjqqkks)) 1;
    1.78 +     solve_prem_prem_tac ctxt]) (rev ppjjqqkks)) 1;
    1.79  
    1.80  fun mk_induct_discharge_prem_tac ctxt nn n set_natural's pre_set_defs m k ppjjqqkks =
    1.81    let val r = length ppjjqqkks in