src/HOL/Tools/BNF/bnf_gfp_tactics.ML
changeset 56248 67dc9549fa15
parent 56179 6b5c46582260
child 56765 644f0d4820a1
     1.1 --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Fri Mar 21 22:54:16 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML	Sat Mar 22 08:37:43 2014 +0100
     1.3 @@ -204,9 +204,9 @@
     1.4              rtac trans_fun_cong_image_id_id_apply, etac (morE RS arg_cong), atac],
     1.5            CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong))
     1.6              (fn (i, (set_map0, coalg_set)) =>
     1.7 -              EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm UN_cong})),
     1.8 +              EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm SUP_cong})),
     1.9                  etac (morE RS sym RS arg_cong RS trans), atac, rtac set_map0,
    1.10 -                rtac (@{thm UN_simps(10)} RS trans), rtac (refl RS @{thm UN_cong}),
    1.11 +                rtac (@{thm UN_simps(10)} RS trans), rtac (refl RS @{thm SUP_cong}),
    1.12                  ftac coalg_set, atac, dtac set_mp, atac, rtac mp, rtac (mk_conjunctN n i),
    1.13                  REPEAT_DETERM o etac allE, atac, atac])
    1.14              (rev ((1 upto n) ~~ (active_set_map0s ~~ coalg_sets)))])
    1.15 @@ -866,14 +866,14 @@
    1.16            (rec_Suc :: dtor_map :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
    1.17          rtac Un_cong, rtac refl,
    1.18          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 Un_cong))
    1.19 -          (fn i => EVERY' [rtac @{thm UN_cong[OF refl]},
    1.20 +          (fn i => EVERY' [rtac @{thm SUP_cong[OF refl]},
    1.21              REPEAT_DETERM o etac allE, etac (mk_conjunctN n i)]) (n downto 1)])
    1.22        (rec_Sucs ~~ (dtor_maps ~~ set_map0ss))] 1
    1.23    end;
    1.24  
    1.25  fun mk_set_map0_tac col_natural =
    1.26    EVERY' (map rtac [@{thm ext}, o_apply RS trans, sym, o_apply RS trans, @{thm image_UN} RS trans,
    1.27 -    refl RS @{thm UN_cong}, col_natural]) 1;
    1.28 +    refl RS @{thm SUP_cong}, col_natural]) 1;
    1.29  
    1.30  fun mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss =
    1.31    let
    1.32 @@ -964,7 +964,7 @@
    1.33              rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac,
    1.34              CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
    1.35                (fn (active_set_map0, in_Jrel) => EVERY' [rtac ord_eq_le_trans,
    1.36 -                rtac @{thm UN_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]},
    1.37 +                rtac @{thm SUP_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]},
    1.38                  rtac active_set_map0, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least},
    1.39                  dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
    1.40                  dtac @{thm ssubst_mem[OF pair_collapse]},