life without 'metis'
authorblanchet
Mon Mar 03 12:48:20 2014 +0100 (2014-03-03)
changeset 55866a6fa341a6d66
parent 55865 3be27c07e36d
child 55867 79b915f26533
life without 'metis'
src/HOL/BNF_Cardinal_Arithmetic.thy
src/HOL/BNF_Comp.thy
     1.1 --- a/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Mar 03 12:48:20 2014 +0100
     1.2 +++ b/src/HOL/BNF_Cardinal_Arithmetic.thy	Mon Mar 03 12:48:20 2014 +0100
     1.3 @@ -351,13 +351,13 @@
     1.4  by (blast intro: cinfinite_cprod2 Card_order_cprod)
     1.5  
     1.6  lemma cprod_cong: "\<lbrakk>p1 =o r1; p2 =o r2\<rbrakk> \<Longrightarrow> p1 *c p2 =o r1 *c r2"
     1.7 -by (metis cprod_mono ordIso_iff_ordLeq)
     1.8 +unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono)
     1.9  
    1.10  lemma cprod_cong1: "\<lbrakk>p1 =o r1\<rbrakk> \<Longrightarrow> p1 *c p2 =o r1 *c p2"
    1.11 -by (metis cprod_mono1 ordIso_iff_ordLeq)
    1.12 +unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono1)
    1.13  
    1.14  lemma cprod_cong2: "p2 =o r2 \<Longrightarrow> q *c p2 =o q *c r2"
    1.15 -by (metis cprod_mono2 ordIso_iff_ordLeq)
    1.16 +unfolding ordIso_iff_ordLeq by (blast intro: cprod_mono2)
    1.17  
    1.18  lemma cprod_com: "p1 *c p2 =o p2 *c p1"
    1.19  by (simp only: cprod_def card_of_Times_commute)
     2.1 --- a/src/HOL/BNF_Comp.thy	Mon Mar 03 12:48:20 2014 +0100
     2.2 +++ b/src/HOL/BNF_Comp.thy	Mon Mar 03 12:48:20 2014 +0100
     2.3 @@ -134,10 +134,15 @@
     2.4    unfolding id_bnf_comp_def by unfold_locales auto
     2.5  
     2.6  lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
     2.7 -by (metis csum_absorb2' ordIso_transitive ordLeq_refl)
     2.8 +apply (erule ordIso_transitive)
     2.9 +apply (frule csum_absorb2')
    2.10 +apply (erule ordLeq_refl)
    2.11 +by simp
    2.12  
    2.13  lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r"
    2.14 -by (metis cprod_infinite ordIso_transitive)
    2.15 +apply (erule ordIso_transitive)
    2.16 +apply (rule cprod_infinite)
    2.17 +by simp
    2.18  
    2.19  ML_file "Tools/BNF/bnf_comp_tactics.ML"
    2.20  ML_file "Tools/BNF/bnf_comp.ML"