avoided duplicate lemma
authorblanchet
Wed Sep 12 11:39:05 2012 +0200 (2012-09-12)
changeset 49328a1c10b46fecd
parent 49327 541d818d2ff3
child 49329 82452dc63ed5
avoided duplicate lemma
src/HOL/Codatatype/BNF_GFP.thy
src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML
     1.1 --- a/src/HOL/Codatatype/BNF_GFP.thy	Wed Sep 12 11:38:22 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/BNF_GFP.thy	Wed Sep 12 11:39:05 2012 +0200
     1.3 @@ -321,9 +321,6 @@
     1.4  lemma list_rec_Cons: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
     1.5  by auto
     1.6  
     1.7 -lemma sum_case_cong: "p = q \<Longrightarrow> sum_case f g p = sum_case f g q"
     1.8 -by simp
     1.9 -
    1.10  lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
    1.11  by simp
    1.12  
     2.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Wed Sep 12 11:38:22 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp_tactics.ML	Wed Sep 12 11:39:05 2012 +0200
     2.3 @@ -143,6 +143,7 @@
     2.4  val snd_convol_fun_cong_sym = @{thm snd_convol} RS fun_cong RS sym;
     2.5  val ssubst_id = @{thm ssubst[of _ _ "%x. x"]};
     2.6  val subst_id = @{thm subst[of _ _ "%x. x"]};
     2.7 +val sum_case_weak_cong = @{thm sum_case_weak_cong};
     2.8  val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
     2.9  
    2.10  fun mk_coalg_set_tac coalg_def =
    2.11 @@ -701,7 +702,7 @@
    2.12          CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
    2.13            CONJ_WRAP' (fn i' => EVERY' [dtac (mk_conjunctN n i'), etac exE, rtac exI,
    2.14              rtac (@{thm append_Cons} RS arg_cong RS trans),
    2.15 -            rtac (rv_Cons RS trans), etac (@{thm sum_case_cong} RS arg_cong RS trans),
    2.16 +            rtac (rv_Cons RS trans), etac (sum_case_weak_cong RS arg_cong RS trans),
    2.17              rtac (mk_sum_casesN n i RS arg_cong RS trans), atac])
    2.18            ks])
    2.19          rv_Conss)
    2.20 @@ -873,7 +874,7 @@
    2.21                rtac exI, rtac conjI,
    2.22                (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
    2.23                else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN'
    2.24 -                etac (@{thm sum_case_cong} RS trans) THEN' rtac (mk_sum_casesN n i)),
    2.25 +                etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
    2.26                EVERY' (map2 (fn set_natural => fn set_rv_Lev =>
    2.27                  EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans),
    2.28                    rtac trans_fun_cong_image_id_id_apply,
    2.29 @@ -897,7 +898,7 @@
    2.30                rtac exI, rtac conjI,
    2.31                (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
    2.32                else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN'
    2.33 -                etac (@{thm sum_case_cong} RS trans) THEN' rtac (mk_sum_casesN n i)),
    2.34 +                etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
    2.35                EVERY' (map2 (fn set_natural => fn set_rv_Lev =>
    2.36                  EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans),
    2.37                    rtac trans_fun_cong_image_id_id_apply,
    2.38 @@ -946,13 +947,13 @@
    2.39        ((map_comp_id, (map_cong, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
    2.40        EVERY' [rtac ballI, rtac sym, rtac trans, rtac strT_def,
    2.41          rtac (@{thm if_P} RS
    2.42 -          (if n = 1 then map_arg_cong else @{thm sum_case_cong}) RS trans),
    2.43 +          (if n = 1 then map_arg_cong else sum_case_weak_cong) RS trans),
    2.44          rtac (@{thm list.size(3)} RS arg_cong RS trans RS equalityD2 RS set_mp),
    2.45          rtac Lev_0, rtac @{thm singletonI},
    2.46          CONVERSION (Conv.top_conv
    2.47            (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
    2.48          if n = 1 then K all_tac
    2.49 -        else (rtac (@{thm sum_case_cong} RS trans) THEN'
    2.50 +        else (rtac (sum_case_weak_cong RS trans) THEN'
    2.51            rtac (mk_sum_casesN n i) THEN' rtac (mk_sum_casesN n i RS trans)),
    2.52          rtac (map_comp_id RS trans), rtac (map_cong OF replicate m refl),
    2.53          EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
    2.54 @@ -990,7 +991,7 @@
    2.55              CONVERSION (Conv.top_conv
    2.56                (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
    2.57              if n = 1 then K all_tac
    2.58 -            else rtac @{thm sum_case_cong} THEN' rtac (mk_sum_casesN n i' RS trans),
    2.59 +            else rtac sum_case_weak_cong THEN' rtac (mk_sum_casesN n i' RS trans),
    2.60              SELECT_GOAL (Local_Defs.unfold_tac ctxt [from_to_sbd]), rtac refl,
    2.61              rtac refl])
    2.62          ks to_sbd_injs from_to_sbds)];