src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML
changeset 49328 a1c10b46fecd
parent 49305 8241f21d104b
child 49366 3edd1c90f6e6
     1.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Wed Sep 12 11:38:22 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Wed Sep 12 11:39:05 2012 +0200
     1.3 @@ -143,6 +143,7 @@
     1.4  val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;
     1.5  val ssubst_id = @{thm ssubst[of _ _ "%x. x"]};
     1.6  val subst_id = @{thm subst[of _ _ "%x. x"]};
     1.7 +val sum_case_weak_cong = @{thm sum_case_weak_cong};
     1.8  val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
     1.9  
    1.10  fun mk_coalg_set_tac coalg_def =
    1.11 @@ -701,7 +702,7 @@
    1.12          CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
    1.13            CONJ_WRAP' (fn i' => EVERY' [dtac (mk_conjunctN n i'), etac exE, rtac exI,
    1.14              rtac (@{thm append_Cons} RS arg_cong RS trans),
    1.15 -            rtac (rv_Cons RS trans), etac (@{thm sum_case_cong} RS arg_cong RS trans),
    1.16 +            rtac (rv_Cons RS trans), etac (sum_case_weak_cong RS arg_cong RS trans),
    1.17              rtac (mk_sum_casesN n i RS arg_cong RS trans), atac])
    1.18            ks])
    1.19          rv_Conss)
    1.20 @@ -873,7 +874,7 @@
    1.21                rtac exI, rtac conjI,
    1.22                (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
    1.23                else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN'
    1.24 -                etac (@{thm sum_case_cong} RS trans) THEN' rtac (mk_sum_casesN n i)),
    1.25 +                etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
    1.26                EVERY' (map2 (fn set_natural => fn set_rv_Lev =>
    1.27                  EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans),
    1.28                    rtac trans_fun_cong_image_id_id_apply,
    1.29 @@ -897,7 +898,7 @@
    1.30                rtac exI, rtac conjI,
    1.31                (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
    1.32                else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN'
    1.33 -                etac (@{thm sum_case_cong} RS trans) THEN' rtac (mk_sum_casesN n i)),
    1.34 +                etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
    1.35                EVERY' (map2 (fn set_natural => fn set_rv_Lev =>
    1.36                  EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans),
    1.37                    rtac trans_fun_cong_image_id_id_apply,
    1.38 @@ -946,13 +947,13 @@
    1.39        ((map_comp_id, (map_cong, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
    1.40        EVERY' [rtac ballI, rtac sym, rtac trans, rtac strT_def,
    1.41          rtac (@{thm if_P} RS
    1.42 -          (if n = 1 then map_arg_cong else @{thm sum_case_cong}) RS trans),
    1.43 +          (if n = 1 then map_arg_cong else sum_case_weak_cong) RS trans),
    1.44          rtac (@{thm list.size(3)} RS arg_cong RS trans RS equalityD2 RS set_mp),
    1.45          rtac Lev_0, rtac @{thm singletonI},
    1.46          CONVERSION (Conv.top_conv
    1.47            (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
    1.48          if n = 1 then K all_tac
    1.49 -        else (rtac (@{thm sum_case_cong} RS trans) THEN'
    1.50 +        else (rtac (sum_case_weak_cong RS trans) THEN'
    1.51            rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)),
    1.52          rtac (map_comp_id RS trans), rtac (map_cong OF replicate m refl),
    1.53          EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
    1.54 @@ -990,7 +991,7 @@
    1.55              CONVERSION (Conv.top_conv
    1.56                (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
    1.57              if n = 1 then K all_tac
    1.58 -            else rtac @{thm sum_case_cong} THEN' rtac (mk_sum_casesN n i' RS trans),
    1.59 +            else rtac sum_case_weak_cong THEN' rtac (mk_sum_casesN n i' RS trans),
    1.60              SELECT_GOAL (Local_Defs.unfold_tac ctxt [from_to_sbd]), rtac refl,
    1.61              rtac refl])
    1.62          ks to_sbd_injs from_to_sbds)];