src/HOL/BNF/Tools/bnf_lfp_tactics.ML
changeset 51782 84e7225f5ab6
parent 51766 f19a4d0ab1bf
child 51798 ad3a241def73
     1.1 --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Thu Apr 25 18:27:26 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML	Thu Apr 25 19:18:20 2013 +0200
     1.3 @@ -312,18 +312,17 @@
     1.4      fun mk_minH_tac (min_alg, in_bd) = EVERY' [rtac @{thm ordIso_ordLeq_trans},
     1.5        rtac @{thm card_of_ordIso_subst}, etac min_alg, rtac @{thm Un_Cinfinite_bound},
     1.6        minG_tac, rtac ctrans, rtac @{thm card_of_image}, rtac ctrans, rtac in_bd, rtac ctrans,
     1.7 -      rtac @{thm cexp_mono1_Cnotzero}, rtac @{thm csum_mono1},
     1.8 +      rtac @{thm cexp_mono1}, rtac @{thm csum_mono1},
     1.9        REPEAT_DETERM_N m o rtac @{thm csum_mono2},
    1.10        CONJ_WRAP_GEN' (rtac @{thm csum_cinfinite_bound}) (K minG_tac) min_algs,
    1.11        REPEAT_DETERM o FIRST'
    1.12 -        [rtac @{thm card_of_Card_order}, rtac @{thm Card_order_csum}, rtac Asuc_Cinfinite],
    1.13 -      rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac bd_Card_order,
    1.14 -      rtac @{thm ordIso_ordLeq_trans}, rtac @{thm cexp_cong1_Cnotzero}, absorbAs_tac,
    1.15 +        [rtac @{thm card_of_Card_order}, rtac @{thm Card_order_csum},
    1.16 +        rtac Asuc_Cinfinite, rtac bd_Card_order],
    1.17 +      rtac @{thm ordIso_ordLeq_trans}, rtac @{thm cexp_cong1}, absorbAs_tac,
    1.18        rtac @{thm csum_absorb1}, rtac Asuc_Cinfinite, rtac @{thm ctwo_ordLeq_Cinfinite},
    1.19        rtac Asuc_Cinfinite, rtac bd_Card_order,
    1.20 -      rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac Asuc_Cnotzero,
    1.21        rtac @{thm ordIso_imp_ordLeq}, rtac @{thm cexp_cprod_ordLeq},
    1.22 -      TRY o rtac @{thm csum_Cnotzero2}, rtac @{thm ctwo_Cnotzero}, rtac suc_Cinfinite,
    1.23 +      resolve_tac @{thms Card_order_csum Card_order_ctwo}, rtac suc_Cinfinite,
    1.24        rtac bd_Cnotzero, rtac @{thm cardSuc_ordLeq}, rtac bd_Card_order, rtac Asuc_Cinfinite];
    1.25    in
    1.26      (rtac induct THEN'
    1.27 @@ -753,8 +752,8 @@
    1.28  fun mk_in_bd_tac sum_Card_order sucbd_Cnotzero incl card_of_min_alg =
    1.29    EVERY' [rtac ctrans, rtac @{thm card_of_mono1}, rtac subsetI, etac rev_mp,
    1.30      rtac incl, rtac ctrans, rtac card_of_min_alg, rtac @{thm cexp_mono2_Cnotzero},
    1.31 -    rtac @{thm cardSuc_ordLeq_cpow}, rtac sum_Card_order, rtac @{thm csum_Cnotzero2},
    1.32 -    rtac @{thm ctwo_Cnotzero}, rtac sucbd_Cnotzero] 1;
    1.33 +    rtac @{thm cardSuc_ordLeq_cpow}, rtac sum_Card_order, rtac @{thm Card_order_csum},
    1.34 +    rtac sucbd_Cnotzero] 1;
    1.35  
    1.36  fun mk_bd_card_order_tac bd_card_orders =
    1.37    (rtac @{thm card_order_cpow} THEN'