src/HOL/BNF/Tools/bnf_comp_tactics.ML
changeset 51782 84e7225f5ab6
parent 51766 f19a4d0ab1bf
child 51798 ad3a241def73
     1.1 --- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Thu Apr 25 18:27:26 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML	Thu Apr 25 19:18:20 2013 +0200
     1.3 @@ -205,13 +205,9 @@
     1.4       rtac Card_order_ctwo THEN'
     1.5       (TRY o (rtac @{thm Cinfinite_csum} THEN' rtac disjI1) THEN' rtac (hd Fbd_Cinfs) ORELSE'
     1.6         rtac (hd Fbd_Cinfs)) THEN'
     1.7 -     rtac disjI1 THEN'
     1.8 -     TRY o rtac csum_Cnotzero2 THEN'
     1.9 -     rtac ctwo_Cnotzero THEN'
    1.10       rtac Gbd_Card_order THEN'
    1.11       rtac @{thm cexp_cprod} THEN'
    1.12 -     TRY o rtac csum_Cnotzero2 THEN'
    1.13 -     rtac ctwo_Cnotzero) 1
    1.14 +     rtac @{thm Card_order_csum}) 1
    1.15    end;
    1.16  
    1.17  val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def SUP_def
    1.18 @@ -300,13 +296,6 @@
    1.19    else all_tac) THEN
    1.20    (rtac @{thm csum_com} THEN'
    1.21    rtac bd_Card_order THEN'
    1.22 -  rtac disjI1 THEN'
    1.23 -  rtac csum_Cnotzero2 THEN'
    1.24 -  rtac ctwo_Cnotzero THEN'
    1.25 -  rtac disjI1 THEN'
    1.26 -  rtac csum_Cnotzero2 THEN'
    1.27 -  TRY o rtac csum_Cnotzero1 THEN'
    1.28 -  rtac Cnotzero_UNIV THEN'
    1.29    rtac @{thm ordLeq_ordIso_trans} THEN'
    1.30    rtac @{thm cexp_mono1} THEN'
    1.31    rtac ctrans THEN'
    1.32 @@ -322,14 +311,9 @@
    1.33    ((rtac Card_order_ctwo THEN' rtac @{thm ordLeq_refl}) ORELSE'
    1.34      (rtac Card_order_csum THEN' rtac ordLeq_csum2)) THEN'
    1.35    rtac Card_order_ctwo THEN'
    1.36 -  rtac disjI1 THEN'
    1.37 -  rtac csum_Cnotzero2 THEN'
    1.38 -  TRY o rtac csum_Cnotzero1 THEN'
    1.39 -  rtac Cnotzero_UNIV THEN'
    1.40    rtac bd_Card_order THEN'
    1.41    rtac @{thm cexp_cprod_ordLeq} THEN'
    1.42 -  TRY o rtac csum_Cnotzero2 THEN'
    1.43 -  rtac ctwo_Cnotzero THEN'
    1.44 +  resolve_tac @{thms Card_order_csum Card_order_ctwo} THEN'
    1.45    rtac @{thm Cinfinite_cprod2} THEN'
    1.46    TRY o rtac csum_Cnotzero1 THEN'
    1.47    rtac Cnotzero_UNIV THEN'
    1.48 @@ -374,8 +358,7 @@
    1.49    (rtac ordLeq_csum2 THEN'
    1.50    (rtac Card_order_csum ORELSE' rtac card_of_Card_order)) 1) ORELSE
    1.51    (rtac ordLeq_csum2 THEN' rtac Card_order_ctwo) 1) THEN
    1.52 -  (rtac disjI1 THEN' TRY o rtac csum_Cnotzero2 THEN' rtac ctwo_Cnotzero
    1.53 -   THEN' rtac bd_Card_order) 1;
    1.54 +  (rtac bd_Card_order) 1;
    1.55  
    1.56  
    1.57  
    1.58 @@ -399,13 +382,7 @@
    1.59        FIRST' [rtac card_of_Card_order, rtac Card_order_csum])
    1.60      ordIso_transitive @{thm csum_assoc} @{thm csum_com} @{thm csum_cong}
    1.61      src dest THEN'
    1.62 -  rtac bd_Card_order THEN'
    1.63 -  rtac disjI1 THEN'
    1.64 -  TRY o rtac csum_Cnotzero2 THEN'
    1.65 -  rtac ctwo_Cnotzero THEN'
    1.66 -  rtac disjI1 THEN'
    1.67 -  TRY o rtac csum_Cnotzero2 THEN'
    1.68 -  rtac ctwo_Cnotzero) 1;
    1.69 +  rtac bd_Card_order) 1;
    1.70  
    1.71  fun mk_map_wpull_tac comp_in_alt inner_map_wpulls outer_map_wpull =
    1.72    (rtac (@{thm wpull_cong} OF (replicate 3 comp_in_alt)) THEN' rtac outer_map_wpull) 1 THEN