replaced swap by contrapos_np;
authorwenzelm
Thu Jan 05 22:29:55 2006 +0100 (2006-01-05)
changeset 185855d379fe2eb74
parent 18584 0fde75d34f8d
child 18586 588e80289658
replaced swap by contrapos_np;
src/HOL/Bali/TypeSafe.thy
src/HOL/Hyperreal/NthRoot.thy
src/HOL/Hyperreal/Poly.thy
src/HOL/Hyperreal/SEQ.thy
src/HOL/Hyperreal/Transcendental.thy
src/HOL/Library/Zorn.thy
     1.1 --- a/src/HOL/Bali/TypeSafe.thy	Thu Jan 05 22:29:53 2006 +0100
     1.2 +++ b/src/HOL/Bali/TypeSafe.thy	Thu Jan 05 22:29:55 2006 +0100
     1.3 @@ -169,7 +169,7 @@
     1.4  lemma conf_fits: "G,s\<turnstile>v\<Colon>\<preceq>T \<Longrightarrow> G,s\<turnstile>v fits T"
     1.5  apply (unfold fits_def)
     1.6  apply clarify
     1.7 -apply (erule swap, simp (no_asm_use))
     1.8 +apply (erule contrapos_np, simp (no_asm_use))
     1.9  apply (drule conf_RefTD)
    1.10  apply auto
    1.11  done
     2.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Thu Jan 05 22:29:53 2006 +0100
     2.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Thu Jan 05 22:29:55 2006 +0100
     2.3 @@ -107,7 +107,7 @@
     2.4  
     2.5  lemma not_isUb_less_ex:
     2.6       "~ isUb (UNIV::real set) S u ==> \<exists>x \<in> S. u < x"
     2.7 -apply (rule ccontr, erule swap)
     2.8 +apply (rule ccontr, erule contrapos_np)
     2.9  apply (rule setleI [THEN isUbI])
    2.10  apply (auto simp add: linorder_not_less [symmetric])
    2.11  done
     3.1 --- a/src/HOL/Hyperreal/Poly.thy	Thu Jan 05 22:29:53 2006 +0100
     3.2 +++ b/src/HOL/Hyperreal/Poly.thy	Thu Jan 05 22:29:55 2006 +0100
     3.3 @@ -497,7 +497,7 @@
     3.4  lemma poly_roots_finite: "(poly p \<noteq> poly []) =
     3.5        (\<exists>N j. \<forall>x. poly p x = 0 --> (\<exists>n. (n::nat) < N & x = j n))"
     3.6  apply safe
     3.7 -apply (erule swap, rule ext)
     3.8 +apply (erule contrapos_np, rule ext)
     3.9  apply (rule ccontr)
    3.10  apply (clarify dest!: poly_roots_finite_lemma)
    3.11  apply (clarify dest!: real_finite_lemma)
    3.12 @@ -717,7 +717,7 @@
    3.13  apply simp 
    3.14  apply (induct_tac "n")
    3.15  apply (simp del: pmult_Cons pexp_Suc)
    3.16 -apply (erule_tac Pa = "poly q a = 0" in swap)
    3.17 +apply (erule_tac Q = "poly q a = 0" in contrapos_np)
    3.18  apply (simp add: poly_add poly_cmult)
    3.19  apply (rule pexp_Suc [THEN ssubst])
    3.20  apply (rule ccontr)
    3.21 @@ -857,8 +857,8 @@
    3.22  apply (erule_tac V = "\<forall>r. r divides pderiv p = r divides pderiv ([- a, 1] %^ Suc n *** q)" in thin_rl)
    3.23  apply (unfold divides_def)
    3.24  apply (simp (no_asm) add: poly_pderiv_mult poly_pderiv_exp_prime fun_eq poly_add poly_mult del: pmult_Cons pexp_Suc)
    3.25 -apply (rule swap, assumption)
    3.26 -apply (rotate_tac 3, erule swap)
    3.27 +apply (rule contrapos_np, assumption)
    3.28 +apply (rotate_tac 3, erule contrapos_np)
    3.29  apply (simp del: pmult_Cons pexp_Suc, safe)
    3.30  apply (rule_tac x = "inverse (real (Suc n)) %* (qa +++ -- (pderiv q))" in exI)
    3.31  apply (subgoal_tac "poly ([-a, 1] %^ n *** q) = poly ([-a, 1] %^ n *** ([-a, 1] *** (inverse (real (Suc n)) %* (qa +++ -- (pderiv q))))) ")
     4.1 --- a/src/HOL/Hyperreal/SEQ.thy	Thu Jan 05 22:29:53 2006 +0100
     4.2 +++ b/src/HOL/Hyperreal/SEQ.thy	Thu Jan 05 22:29:55 2006 +0100
     4.3 @@ -436,7 +436,7 @@
     4.4  apply (auto intro!: lessI [THEN less_imp_le] dest!: less_imp_Suc_add)
     4.5  apply (induct_tac "ka")
     4.6  apply (auto intro: order_trans)
     4.7 -apply (erule swap) 
     4.8 +apply (erule contrapos_np)
     4.9  apply (induct_tac "k")
    4.10  apply (auto intro: order_trans)
    4.11  done
     5.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Thu Jan 05 22:29:53 2006 +0100
     5.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Thu Jan 05 22:29:55 2006 +0100
     5.3 @@ -1624,7 +1624,7 @@
     5.4       "[| -1 \<le> y; y \<le> 1 |] ==> EX! x. -(pi/2) \<le> x & x \<le> pi/2 & (sin x = y)"
     5.5  apply (rule ccontr)
     5.6  apply (subgoal_tac "\<forall>x. (- (pi/2) \<le> x & x \<le> pi/2 & (sin x = y)) = (0 \<le> (x + pi/2) & (x + pi/2) \<le> pi & (cos (x + pi/2) = -y))")
     5.7 -apply (erule swap)
     5.8 +apply (erule contrapos_np)
     5.9  apply (simp del: minus_sin_cos_eq [symmetric])
    5.10  apply (cut_tac y="-y" in cos_total, simp) apply simp 
    5.11  apply (erule ex1E)
     6.1 --- a/src/HOL/Library/Zorn.thy	Thu Jan 05 22:29:53 2006 +0100
     6.2 +++ b/src/HOL/Library/Zorn.thy	Thu Jan 05 22:29:55 2006 +0100
     6.3 @@ -53,7 +53,7 @@
     6.4    apply (unfold succ_def)
     6.5    apply (rule split_if [THEN iffD2])
     6.6    apply (auto simp add: super_def maxchain_def psubset_def)
     6.7 -  apply (rule swap, assumption)
     6.8 +  apply (rule contrapos_np, assumption)
     6.9    apply (rule someI2, blast+)
    6.10    done
    6.11