src/HOL/Tools/BNF/bnf_gfp_tactics.ML
changeset 57983 6edc3529bb4e
parent 57806 8e74998e04b8
child 58445 86b5b02ef33a
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -103,7 +103,7 @@
     1.4  val ord_eq_le_trans = @{thm ord_eq_le_trans};
     1.5  val ordIso_ordLeq_trans = @{thm ordIso_ordLeq_trans};
     1.6  val snd_convol_fun_cong_sym = @{thm snd_convol[unfolded convol_def]} RS fun_cong RS sym;
     1.7 -val sum_weak_case_cong = @{thm sum.weak_case_cong};
     1.8 +val sum_case_cong_weak = @{thm sum.case_cong_weak};
     1.9  val trans_fun_cong_image_id_id_apply = @{thm trans[OF fun_cong[OF image_id] id_apply]};
    1.10  val Collect_splitD_set_mp = @{thm Collect_splitD[OF set_mp]};
    1.11  val rev_bspec = Drule.rotate_prems 1 bspec;
    1.12 @@ -430,7 +430,7 @@
    1.13          CONJ_WRAP' (fn rv_Cons => EVERY' [REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
    1.14            CONJ_WRAP' (fn i' => EVERY' [dtac (mk_conjunctN n i'), etac exE, rtac exI,
    1.15              rtac (@{thm append_Cons} RS arg_cong RS trans), rtac (rv_Cons RS trans),
    1.16 -            if n = 1 then K all_tac else etac (sum_weak_case_cong RS trans),
    1.17 +            if n = 1 then K all_tac else etac (sum_case_cong_weak RS trans),
    1.18              rtac (mk_sum_caseN n i RS trans), atac])
    1.19            ks])
    1.20          rv_Conss)
    1.21 @@ -565,7 +565,7 @@
    1.22                rtac (rev_mp OF [rv_last, impI]), etac exE, rtac (isNode_def RS iffD2),
    1.23                rtac exI, rtac conjI,
    1.24                if n = 1 then rtac refl
    1.25 -              else etac (sum_weak_case_cong RS trans) THEN' rtac (mk_sum_caseN n i),
    1.26 +              else etac (sum_case_cong_weak RS trans) THEN' rtac (mk_sum_caseN n i),
    1.27                CONJ_WRAP' (fn (set_map0, (set_Lev, set_image_Lev)) =>
    1.28                  EVERY' [rtac (set_map0 RS trans), rtac equalityI, rtac @{thm image_subsetI},
    1.29                    rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
    1.30 @@ -603,7 +603,7 @@
    1.31          CONVERSION (Conv.top_conv
    1.32            (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
    1.33          if n = 1 then K all_tac
    1.34 -        else (rtac (sum_weak_case_cong RS trans) THEN'
    1.35 +        else (rtac (sum_case_cong_weak RS trans) THEN'
    1.36            rtac (mk_sum_caseN n i) THEN' rtac (mk_sum_caseN n i RS trans)),
    1.37          rtac (map_comp_id RS trans), rtac (map_cong0 OF replicate m refl),
    1.38          EVERY' (map3 (fn i' => fn to_sbd_inj => fn from_to_sbd =>
    1.39 @@ -628,7 +628,7 @@
    1.40              CONVERSION (Conv.top_conv
    1.41                (K (Conv.try_conv (Conv.rewr_conv (rv_Cons RS eq_reflection)))) ctxt),
    1.42              if n = 1 then K all_tac
    1.43 -            else rtac sum_weak_case_cong THEN' rtac (mk_sum_caseN n i' RS trans),
    1.44 +            else rtac sum_case_cong_weak THEN' rtac (mk_sum_caseN n i' RS trans),
    1.45              SELECT_GOAL (unfold_thms_tac ctxt [from_to_sbd]), rtac refl])
    1.46          ks to_sbd_injs from_to_sbds)];
    1.47    in