renamed lemmas "anti_sym" -> "antisym"
authornipkow
Fri Nov 13 14:14:04 2009 +0100 (2009-11-13)
changeset 33657a4179bf442d1
parent 33648 555e5358b8c9
child 33658 eb8b9c8a3662
renamed lemmas "anti_sym" -> "antisym"
src/HOL/Algebra/IntRing.thy
src/HOL/Algebra/Lattice.thy
src/HOL/Algebra/Sylow.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Algebra/poly/UnivPoly2.thy
src/HOL/Finite_Set.thy
src/HOL/GCD.thy
src/HOL/Hoare/Arith2.thy
src/HOL/Import/HOL/arithmetic.imp
src/HOL/Import/HOL/divides.imp
src/HOL/Int.thy
src/HOL/Library/Abstract_Rat.thy
src/HOL/Matrix/Matrix.thy
src/HOL/Nat.thy
src/HOL/Number_Theory/UniqueFactorization.thy
src/HOL/Old_Number_Theory/IntPrimes.thy
src/HOL/Old_Number_Theory/Legacy_GCD.thy
src/HOL/Old_Number_Theory/Pocklington.thy
src/HOL/Old_Number_Theory/Primes.thy
src/HOL/Probability/Borel.thy
src/HOL/Probability/Measure.thy
src/HOL/RealDef.thy
src/HOL/SupInf.thy
src/HOL/ex/LocaleTest2.thy
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Thu Nov 12 14:32:21 2009 -0800
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Fri Nov 13 14:14:04 2009 +0100
     1.3 @@ -12,26 +12,6 @@
     1.4  
     1.5  subsection {* Some properties of @{typ int} *}
     1.6  
     1.7 -lemma dvds_imp_abseq:
     1.8 -  "\<lbrakk>l dvd k; k dvd l\<rbrakk> \<Longrightarrow> abs l = abs (k::int)"
     1.9 -apply (subst abs_split, rule conjI)
    1.10 - apply (clarsimp, subst abs_split, rule conjI)
    1.11 -  apply (clarsimp)
    1.12 -  apply (cases "k=0", simp)
    1.13 -  apply (cases "l=0", simp)
    1.14 -  apply (simp add: zdvd_anti_sym)
    1.15 - apply clarsimp
    1.16 - apply (cases "k=0", simp)
    1.17 - apply (simp add: zdvd_anti_sym)
    1.18 -apply (clarsimp, subst abs_split, rule conjI)
    1.19 - apply (clarsimp)
    1.20 - apply (cases "l=0", simp)
    1.21 - apply (simp add: zdvd_anti_sym)
    1.22 -apply (clarsimp)
    1.23 -apply (subgoal_tac "-l = -k", simp)
    1.24 -apply (intro zdvd_anti_sym, simp+)
    1.25 -done
    1.26 -
    1.27  lemma abseq_imp_dvd:
    1.28    assumes a_lk: "abs l = abs (k::int)"
    1.29    shows "l dvd k"
    1.30 @@ -55,7 +35,7 @@
    1.31  lemma dvds_eq_abseq:
    1.32    "(l dvd k \<and> k dvd l) = (abs l = abs (k::int))"
    1.33  apply rule
    1.34 - apply (simp add: dvds_imp_abseq)
    1.35 + apply (simp add: zdvd_antisym_abs)
    1.36  apply (rule conjI)
    1.37   apply (simp add: abseq_imp_dvd)+
    1.38  done
     2.1 --- a/src/HOL/Algebra/Lattice.thy	Thu Nov 12 14:32:21 2009 -0800
     2.2 +++ b/src/HOL/Algebra/Lattice.thy	Fri Nov 13 14:14:04 2009 +0100
     2.3 @@ -18,7 +18,7 @@
     2.4  locale weak_partial_order = equivalence L for L (structure) +
     2.5    assumes le_refl [intro, simp]:
     2.6        "x \<in> carrier L ==> x \<sqsubseteq> x"
     2.7 -    and weak_le_anti_sym [intro]:
     2.8 +    and weak_le_antisym [intro]:
     2.9        "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y"
    2.10      and le_trans [trans]:
    2.11        "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
    2.12 @@ -636,7 +636,7 @@
    2.13    fix s
    2.14    assume sup: "least L s (Upper L {x, y, z})"
    2.15    show "x \<squnion> (y \<squnion> z) .= s"
    2.16 -  proof (rule weak_le_anti_sym)
    2.17 +  proof (rule weak_le_antisym)
    2.18      from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
    2.19        by (fastsimp intro!: join_le elim: least_Upper_above)
    2.20    next
    2.21 @@ -877,7 +877,7 @@
    2.22    fix i
    2.23    assume inf: "greatest L i (Lower L {x, y, z})"
    2.24    show "x \<sqinter> (y \<sqinter> z) .= i"
    2.25 -  proof (rule weak_le_anti_sym)
    2.26 +  proof (rule weak_le_antisym)
    2.27      from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
    2.28        by (fastsimp intro!: meet_le elim: greatest_Lower_below)
    2.29    next
    2.30 @@ -1089,11 +1089,11 @@
    2.31    assumes eq_is_equal: "op .= = op ="
    2.32  begin
    2.33  
    2.34 -declare weak_le_anti_sym [rule del]
    2.35 +declare weak_le_antisym [rule del]
    2.36  
    2.37 -lemma le_anti_sym [intro]:
    2.38 +lemma le_antisym [intro]:
    2.39    "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
    2.40 -  using weak_le_anti_sym unfolding eq_is_equal .
    2.41 +  using weak_le_antisym unfolding eq_is_equal .
    2.42  
    2.43  lemma lless_eq:
    2.44    "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y & x \<noteq> y"
     3.1 --- a/src/HOL/Algebra/Sylow.thy	Thu Nov 12 14:32:21 2009 -0800
     3.2 +++ b/src/HOL/Algebra/Sylow.thy	Fri Nov 13 14:14:04 2009 +0100
     3.3 @@ -344,7 +344,7 @@
     3.4  done
     3.5  
     3.6  lemma (in sylow_central) card_H_eq: "card(H) = p^a"
     3.7 -by (blast intro: le_anti_sym lemma_leq1 lemma_leq2)
     3.8 +by (blast intro: le_antisym lemma_leq1 lemma_leq2)
     3.9  
    3.10  lemma (in sylow) sylow_thm: "\<exists>H. subgroup H G & card(H) = p^a"
    3.11  apply (cut_tac lemma_A1, clarify)
     4.1 --- a/src/HOL/Algebra/UnivPoly.thy	Thu Nov 12 14:32:21 2009 -0800
     4.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Fri Nov 13 14:14:04 2009 +0100
     4.3 @@ -811,7 +811,7 @@
     4.4  lemma deg_eqI:
     4.5    "[| !!m. n < m ==> coeff P p m = \<zero>;
     4.6        !!n. n ~= 0 ==> coeff P p n ~= \<zero>; p \<in> carrier P |] ==> deg R p = n"
     4.7 -by (fast intro: le_anti_sym deg_aboveI deg_belowI)
     4.8 +by (fast intro: le_antisym deg_aboveI deg_belowI)
     4.9  
    4.10  text {* Degree and polynomial operations *}
    4.11  
    4.12 @@ -826,11 +826,11 @@
    4.13  
    4.14  lemma deg_monom [simp]:
    4.15    "[| a ~= \<zero>; a \<in> carrier R |] ==> deg R (monom P a n) = n"
    4.16 -  by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI)
    4.17 +  by (fastsimp intro: le_antisym deg_aboveI deg_belowI)
    4.18  
    4.19  lemma deg_const [simp]:
    4.20    assumes R: "a \<in> carrier R" shows "deg R (monom P a 0) = 0"
    4.21 -proof (rule le_anti_sym)
    4.22 +proof (rule le_antisym)
    4.23    show "deg R (monom P a 0) <= 0" by (rule deg_aboveI) (simp_all add: R)
    4.24  next
    4.25    show "0 <= deg R (monom P a 0)" by (rule deg_belowI) (simp_all add: R)
    4.26 @@ -838,7 +838,7 @@
    4.27  
    4.28  lemma deg_zero [simp]:
    4.29    "deg R \<zero>\<^bsub>P\<^esub> = 0"
    4.30 -proof (rule le_anti_sym)
    4.31 +proof (rule le_antisym)
    4.32    show "deg R \<zero>\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all
    4.33  next
    4.34    show "0 <= deg R \<zero>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all
    4.35 @@ -846,7 +846,7 @@
    4.36  
    4.37  lemma deg_one [simp]:
    4.38    "deg R \<one>\<^bsub>P\<^esub> = 0"
    4.39 -proof (rule le_anti_sym)
    4.40 +proof (rule le_antisym)
    4.41    show "deg R \<one>\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all
    4.42  next
    4.43    show "0 <= deg R \<one>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all
    4.44 @@ -854,7 +854,7 @@
    4.45  
    4.46  lemma deg_uminus [simp]:
    4.47    assumes R: "p \<in> carrier P" shows "deg R (\<ominus>\<^bsub>P\<^esub> p) = deg R p"
    4.48 -proof (rule le_anti_sym)
    4.49 +proof (rule le_antisym)
    4.50    show "deg R (\<ominus>\<^bsub>P\<^esub> p) <= deg R p" by (simp add: deg_aboveI deg_aboveD R)
    4.51  next
    4.52    show "deg R p <= deg R (\<ominus>\<^bsub>P\<^esub> p)"
    4.53 @@ -878,7 +878,7 @@
    4.54  lemma deg_smult [simp]:
    4.55    assumes R: "a \<in> carrier R" "p \<in> carrier P"
    4.56    shows "deg R (a \<odot>\<^bsub>P\<^esub> p) = (if a = \<zero> then 0 else deg R p)"
    4.57 -proof (rule le_anti_sym)
    4.58 +proof (rule le_antisym)
    4.59    show "deg R (a \<odot>\<^bsub>P\<^esub> p) <= (if a = \<zero> then 0 else deg R p)"
    4.60      using R by (rule deg_smult_ring)
    4.61  next
    4.62 @@ -920,7 +920,7 @@
    4.63  lemma deg_mult [simp]:
    4.64    "[| p ~= \<zero>\<^bsub>P\<^esub>; q ~= \<zero>\<^bsub>P\<^esub>; p \<in> carrier P; q \<in> carrier P |] ==>
    4.65    deg R (p \<otimes>\<^bsub>P\<^esub> q) = deg R p + deg R q"
    4.66 -proof (rule le_anti_sym)
    4.67 +proof (rule le_antisym)
    4.68    assume "p \<in> carrier P" " q \<in> carrier P"
    4.69    then show "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q" by (rule deg_mult_ring)
    4.70  next
     5.1 --- a/src/HOL/Algebra/poly/UnivPoly2.thy	Thu Nov 12 14:32:21 2009 -0800
     5.2 +++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Nov 13 14:14:04 2009 +0100
     5.3 @@ -557,7 +557,7 @@
     5.4  lemma deg_eqI:
     5.5    "[| !!m. n < m ==> coeff p m = 0;
     5.6        !!n. n ~= 0 ==> coeff p n ~= 0|] ==> deg p = n"
     5.7 -by (fast intro: le_anti_sym deg_aboveI deg_belowI)
     5.8 +by (fast intro: le_antisym deg_aboveI deg_belowI)
     5.9  
    5.10  (* Degree and polynomial operations *)
    5.11  
    5.12 @@ -571,11 +571,11 @@
    5.13  
    5.14  lemma deg_monom [simp]:
    5.15    "a ~= 0 ==> deg (monom a n::'a::ring up) = n"
    5.16 -by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI)
    5.17 +by (fastsimp intro: le_antisym deg_aboveI deg_belowI)
    5.18  
    5.19  lemma deg_const [simp]:
    5.20    "deg (monom (a::'a::ring) 0) = 0"
    5.21 -proof (rule le_anti_sym)
    5.22 +proof (rule le_antisym)
    5.23    show "deg (monom a 0) <= 0" by (rule deg_aboveI) simp
    5.24  next
    5.25    show "0 <= deg (monom a 0)" by (rule deg_belowI) simp
    5.26 @@ -583,7 +583,7 @@
    5.27  
    5.28  lemma deg_zero [simp]:
    5.29    "deg 0 = 0"
    5.30 -proof (rule le_anti_sym)
    5.31 +proof (rule le_antisym)
    5.32    show "deg 0 <= 0" by (rule deg_aboveI) simp
    5.33  next
    5.34    show "0 <= deg 0" by (rule deg_belowI) simp
    5.35 @@ -591,7 +591,7 @@
    5.36  
    5.37  lemma deg_one [simp]:
    5.38    "deg 1 = 0"
    5.39 -proof (rule le_anti_sym)
    5.40 +proof (rule le_antisym)
    5.41    show "deg 1 <= 0" by (rule deg_aboveI) simp
    5.42  next
    5.43    show "0 <= deg 1" by (rule deg_belowI) simp
    5.44 @@ -612,7 +612,7 @@
    5.45  
    5.46  lemma deg_uminus [simp]:
    5.47    "deg (-p::('a::ring) up) = deg p"
    5.48 -proof (rule le_anti_sym)
    5.49 +proof (rule le_antisym)
    5.50    show "deg (- p) <= deg p" by (simp add: deg_aboveI deg_aboveD)
    5.51  next
    5.52    show "deg p <= deg (- p)" 
    5.53 @@ -626,7 +626,7 @@
    5.54  
    5.55  lemma deg_smult [simp]:
    5.56    "deg ((a::'a::domain) *s p) = (if a = 0 then 0 else deg p)"
    5.57 -proof (rule le_anti_sym)
    5.58 +proof (rule le_antisym)
    5.59    show "deg (a *s p) <= (if a = 0 then 0 else deg p)" by (rule deg_smult_ring)
    5.60  next
    5.61    show "(if a = 0 then 0 else deg p) <= deg (a *s p)"
    5.62 @@ -657,7 +657,7 @@
    5.63  
    5.64  lemma deg_mult [simp]:
    5.65    "[| (p::'a::domain up) ~= 0; q ~= 0|] ==> deg (p * q) = deg p + deg q"
    5.66 -proof (rule le_anti_sym)
    5.67 +proof (rule le_antisym)
    5.68    show "deg (p * q) <= deg p + deg q" by (rule deg_mult_ring)
    5.69  next
    5.70    let ?s = "(%i. coeff p i * coeff q (deg p + deg q - i))"
     6.1 --- a/src/HOL/Finite_Set.thy	Thu Nov 12 14:32:21 2009 -0800
     6.2 +++ b/src/HOL/Finite_Set.thy	Fri Nov 13 14:14:04 2009 +0100
     6.3 @@ -2344,7 +2344,7 @@
     6.4  lemma card_bij_eq:
     6.5    "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
     6.6       finite A; finite B |] ==> card A = card B"
     6.7 -by (auto intro: le_anti_sym card_inj_on_le)
     6.8 +by (auto intro: le_antisym card_inj_on_le)
     6.9  
    6.10  
    6.11  subsubsection {* Cardinality of products *}
     7.1 --- a/src/HOL/GCD.thy	Thu Nov 12 14:32:21 2009 -0800
     7.2 +++ b/src/HOL/GCD.thy	Fri Nov 13 14:14:04 2009 +0100
     7.3 @@ -312,13 +312,13 @@
     7.4    by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
     7.5  
     7.6  lemma gcd_commute_nat: "gcd (m::nat) n = gcd n m"
     7.7 -  by (rule dvd_anti_sym, auto)
     7.8 +  by (rule dvd_antisym, auto)
     7.9  
    7.10  lemma gcd_commute_int: "gcd (m::int) n = gcd n m"
    7.11    by (auto simp add: gcd_int_def gcd_commute_nat)
    7.12  
    7.13  lemma gcd_assoc_nat: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)"
    7.14 -  apply (rule dvd_anti_sym)
    7.15 +  apply (rule dvd_antisym)
    7.16    apply (blast intro: dvd_trans)+
    7.17  done
    7.18  
    7.19 @@ -339,23 +339,18 @@
    7.20  lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>
    7.21      (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
    7.22    apply auto
    7.23 -  apply (rule dvd_anti_sym)
    7.24 +  apply (rule dvd_antisym)
    7.25    apply (erule (1) gcd_greatest_nat)
    7.26    apply auto
    7.27  done
    7.28  
    7.29  lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>
    7.30      (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
    7.31 -  apply (case_tac "d = 0")
    7.32 -  apply force
    7.33 -  apply (rule iffI)
    7.34 -  apply (rule zdvd_anti_sym)
    7.35 -  apply arith
    7.36 -  apply (subst gcd_pos_int)
    7.37 -  apply clarsimp
    7.38 -  apply (drule_tac x = "d + 1" in spec)
    7.39 -  apply (frule zdvd_imp_le)
    7.40 -  apply (auto intro: gcd_greatest_int)
    7.41 +apply (case_tac "d = 0")
    7.42 + apply simp
    7.43 +apply (rule iffI)
    7.44 + apply (rule zdvd_antisym_nonneg)
    7.45 + apply (auto intro: gcd_greatest_int)
    7.46  done
    7.47  
    7.48  lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
    7.49 @@ -417,7 +412,7 @@
    7.50    by (auto intro: coprime_dvd_mult_int)
    7.51  
    7.52  lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
    7.53 -  apply (rule dvd_anti_sym)
    7.54 +  apply (rule dvd_antisym)
    7.55    apply (rule gcd_greatest_nat)
    7.56    apply (rule_tac n = k in coprime_dvd_mult_nat)
    7.57    apply (simp add: gcd_assoc_nat)
    7.58 @@ -1381,11 +1376,11 @@
    7.59  
    7.60  lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and>
    7.61      (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
    7.62 -  by (auto intro: dvd_anti_sym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat)
    7.63 +  by (auto intro: dvd_antisym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat)
    7.64  
    7.65  lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
    7.66      (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
    7.67 -  by (auto intro: dvd_anti_sym [transferred] lcm_least_int)
    7.68 +  by (auto intro: dvd_antisym [transferred] lcm_least_int)
    7.69  
    7.70  lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
    7.71    apply (rule sym)
     8.1 --- a/src/HOL/Hoare/Arith2.thy	Thu Nov 12 14:32:21 2009 -0800
     8.2 +++ b/src/HOL/Hoare/Arith2.thy	Fri Nov 13 14:14:04 2009 +0100
     8.3 @@ -58,7 +58,7 @@
     8.4    apply (frule cd_nnn)
     8.5    apply (rule some_equality [symmetric])
     8.6    apply (blast dest: cd_le)
     8.7 -  apply (blast intro: le_anti_sym dest: cd_le)
     8.8 +  apply (blast intro: le_antisym dest: cd_le)
     8.9    done
    8.10  
    8.11  lemma gcd_swap: "gcd m n = gcd n m"
     9.1 --- a/src/HOL/Import/HOL/arithmetic.imp	Thu Nov 12 14:32:21 2009 -0800
     9.2 +++ b/src/HOL/Import/HOL/arithmetic.imp	Fri Nov 13 14:14:04 2009 +0100
     9.3 @@ -191,7 +191,7 @@
     9.4    "LESS_EQ_ADD_SUB" > "Nat.add_diff_assoc"
     9.5    "LESS_EQ_ADD" > "Nat.le_add1"
     9.6    "LESS_EQ_0" > "Nat.le_0_eq"
     9.7 -  "LESS_EQUAL_ANTISYM" > "Nat.le_anti_sym"
     9.8 +  "LESS_EQUAL_ANTISYM" > "Nat.le_antisym"
     9.9    "LESS_EQUAL_ADD" > "HOL4Base.arithmetic.LESS_EQUAL_ADD"
    9.10    "LESS_EQ" > "Nat.le_simps_3"
    9.11    "LESS_DIV_EQ_ZERO" > "Divides.div_less"
    10.1 --- a/src/HOL/Import/HOL/divides.imp	Thu Nov 12 14:32:21 2009 -0800
    10.2 +++ b/src/HOL/Import/HOL/divides.imp	Fri Nov 13 14:14:04 2009 +0100
    10.3 @@ -16,7 +16,7 @@
    10.4    "DIVIDES_MULT" > "Divides.dvd_mult2"
    10.5    "DIVIDES_LE" > "Divides.dvd_imp_le"
    10.6    "DIVIDES_FACT" > "HOL4Base.divides.DIVIDES_FACT"
    10.7 -  "DIVIDES_ANTISYM" > "Divides.dvd_anti_sym"
    10.8 +  "DIVIDES_ANTISYM" > "Divides.dvd_antisym"
    10.9    "DIVIDES_ADD_2" > "HOL4Base.divides.DIVIDES_ADD_2"
   10.10    "DIVIDES_ADD_1" > "Ring_and_Field.dvd_add"
   10.11    "ALL_DIVIDES_0" > "Divides.dvd_0_right"
    11.1 --- a/src/HOL/Int.thy	Thu Nov 12 14:32:21 2009 -0800
    11.2 +++ b/src/HOL/Int.thy	Fri Nov 13 14:14:04 2009 +0100
    11.3 @@ -1986,15 +1986,18 @@
    11.4  
    11.5  subsection {* The divides relation *}
    11.6  
    11.7 -lemma zdvd_anti_sym:
    11.8 -    "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
    11.9 +lemma zdvd_antisym_nonneg:
   11.10 +    "0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)"
   11.11    apply (simp add: dvd_def, auto)
   11.12 -  apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff)
   11.13 +  apply (auto simp add: mult_assoc zero_le_mult_iff zmult_eq_1_iff)
   11.14    done
   11.15  
   11.16 -lemma zdvd_dvd_eq: assumes "a \<noteq> 0" and "(a::int) dvd b" and "b dvd a" 
   11.17 +lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a" 
   11.18    shows "\<bar>a\<bar> = \<bar>b\<bar>"
   11.19 -proof-
   11.20 +proof cases
   11.21 +  assume "a = 0" with assms show ?thesis by simp
   11.22 +next
   11.23 +  assume "a \<noteq> 0"
   11.24    from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast 
   11.25    from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast 
   11.26    from k k' have "a = a*k*k'" by simp
   11.27 @@ -2326,7 +2329,7 @@
   11.28  
   11.29  lemmas zle_refl = order_refl [of "w::int", standard]
   11.30  lemmas zle_trans = order_trans [where 'a=int and x="i" and y="j" and z="k", standard]
   11.31 -lemmas zle_anti_sym = order_antisym [of "z::int" "w", standard]
   11.32 +lemmas zle_antisym = order_antisym [of "z::int" "w", standard]
   11.33  lemmas zle_linear = linorder_linear [of "z::int" "w", standard]
   11.34  lemmas zless_linear = linorder_less_linear [where 'a = int]
   11.35  
    12.1 --- a/src/HOL/Library/Abstract_Rat.thy	Thu Nov 12 14:32:21 2009 -0800
    12.2 +++ b/src/HOL/Library/Abstract_Rat.thy	Fri Nov 13 14:14:04 2009 +0100
    12.3 @@ -206,7 +206,7 @@
    12.4        apply simp
    12.5        apply algebra
    12.6        done
    12.7 -    from zdvd_dvd_eq[OF bz coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
    12.8 +    from zdvd_antisym_abs[OF coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
    12.9        coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]]
   12.10        have eq1: "b = b'" using pos by arith  
   12.11        with eq have "a = a'" using pos by simp
    13.1 --- a/src/HOL/Matrix/Matrix.thy	Thu Nov 12 14:32:21 2009 -0800
    13.2 +++ b/src/HOL/Matrix/Matrix.thy	Fri Nov 13 14:14:04 2009 +0100
    13.3 @@ -873,7 +873,7 @@
    13.4  have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+
    13.5  from th show ?thesis 
    13.6  apply (auto)
    13.7 -apply (rule le_anti_sym)
    13.8 +apply (rule le_antisym)
    13.9  apply (subst nrows_le)
   13.10  apply (simp add: singleton_matrix_def, auto)
   13.11  apply (subst RepAbs_matrix)
   13.12 @@ -889,7 +889,7 @@
   13.13  have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+
   13.14  from th show ?thesis 
   13.15  apply (auto)
   13.16 -apply (rule le_anti_sym)
   13.17 +apply (rule le_antisym)
   13.18  apply (subst ncols_le)
   13.19  apply (simp add: singleton_matrix_def, auto)
   13.20  apply (subst RepAbs_matrix)
   13.21 @@ -1004,7 +1004,7 @@
   13.22    apply (subst foldseq_almostzero[of _ j])
   13.23    apply (simp add: prems)+
   13.24    apply (auto)
   13.25 -  apply (metis comm_monoid_add.mult_1 le_anti_sym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
   13.26 +  apply (metis comm_monoid_add.mult_1 le_antisym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
   13.27    done
   13.28  
   13.29  lemma mult_matrix_ext:
    14.1 --- a/src/HOL/Nat.thy	Thu Nov 12 14:32:21 2009 -0800
    14.2 +++ b/src/HOL/Nat.thy	Fri Nov 13 14:14:04 2009 +0100
    14.3 @@ -596,7 +596,7 @@
    14.4  lemma le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::nat)"
    14.5    by (rule order_trans)
    14.6  
    14.7 -lemma le_anti_sym: "[| m \<le> n; n \<le> m |] ==> m = (n::nat)"
    14.8 +lemma le_antisym: "[| m \<le> n; n \<le> m |] ==> m = (n::nat)"
    14.9    by (rule antisym)
   14.10  
   14.11  lemma nat_less_le: "((m::nat) < n) = (m \<le> n & m \<noteq> n)"
   14.12 @@ -1611,14 +1611,14 @@
   14.13  lemma nat_dvd_1_iff_1 [simp]: "m dvd (1::nat) \<longleftrightarrow> m = 1"
   14.14  by (simp add: dvd_def)
   14.15  
   14.16 -lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
   14.17 +lemma dvd_antisym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
   14.18    unfolding dvd_def
   14.19    by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
   14.20  
   14.21  text {* @{term "op dvd"} is a partial order *}
   14.22  
   14.23  interpretation dvd: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
   14.24 -  proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
   14.25 +  proof qed (auto intro: dvd_refl dvd_trans dvd_antisym)
   14.26  
   14.27  lemma dvd_diff_nat[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
   14.28  unfolding dvd_def
    15.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Thu Nov 12 14:32:21 2009 -0800
    15.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Fri Nov 13 14:14:04 2009 +0100
    15.3 @@ -844,7 +844,7 @@
    15.4      mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
    15.5    shows "x = y"
    15.6  
    15.7 -  apply (rule dvd_anti_sym)
    15.8 +  apply (rule dvd_antisym)
    15.9    apply (auto intro: multiplicity_dvd'_nat) 
   15.10  done
   15.11  
   15.12 @@ -854,7 +854,7 @@
   15.13      mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
   15.14    shows "x = y"
   15.15  
   15.16 -  apply (rule dvd_anti_sym [transferred])
   15.17 +  apply (rule dvd_antisym [transferred])
   15.18    apply (auto intro: multiplicity_dvd'_int) 
   15.19  done
   15.20  
    16.1 --- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Thu Nov 12 14:32:21 2009 -0800
    16.2 +++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Fri Nov 13 14:14:04 2009 +0100
    16.3 @@ -204,7 +204,7 @@
    16.4      apply (case_tac [2] "0 \<le> ka")
    16.5    apply (metis zdvd_mult_div_cancel dvd_refl dvd_mult_left zmult_commute zrelprime_zdvd_zmult)
    16.6    apply (metis abs_dvd_iff abs_of_nonneg zadd_0 zgcd_0_left zgcd_commute zgcd_zadd_zmult zgcd_zdvd_zgcd_zmult zgcd_zmult_distrib2_abs zmult_1_right zmult_commute)
    16.7 -  apply (metis mult_le_0_iff  zdvd_mono zdvd_mult_cancel dvd_triv_left zero_le_mult_iff zle_anti_sym zle_linear zle_refl zmult_commute zrelprime_zdvd_zmult)
    16.8 +  apply (metis mult_le_0_iff  zdvd_mono zdvd_mult_cancel dvd_triv_left zero_le_mult_iff zle_antisym zle_linear zle_refl zmult_commute zrelprime_zdvd_zmult)
    16.9    apply (metis dvd_triv_left)
   16.10    done
   16.11  
    17.1 --- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Thu Nov 12 14:32:21 2009 -0800
    17.2 +++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Fri Nov 13 14:14:04 2009 +0100
    17.3 @@ -23,7 +23,7 @@
    17.4  text {* Uniqueness *}
    17.5  
    17.6  lemma is_gcd_unique: "is_gcd a b m \<Longrightarrow> is_gcd a b n \<Longrightarrow> m = n"
    17.7 -  by (simp add: is_gcd_def) (blast intro: dvd_anti_sym)
    17.8 +  by (simp add: is_gcd_def) (blast intro: dvd_antisym)
    17.9  
   17.10  text {* Connection to divides relation *}
   17.11  
   17.12 @@ -156,7 +156,7 @@
   17.13    by (auto intro: relprime_dvd_mult dvd_mult2)
   17.14  
   17.15  lemma gcd_mult_cancel: "gcd k n = 1 ==> gcd (k * m) n = gcd m n"
   17.16 -  apply (rule dvd_anti_sym)
   17.17 +  apply (rule dvd_antisym)
   17.18     apply (rule gcd_greatest)
   17.19      apply (rule_tac n = k in relprime_dvd_mult)
   17.20       apply (simp add: gcd_assoc)
   17.21 @@ -223,7 +223,7 @@
   17.22    assume H: "d dvd a" "d dvd b" "\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d"
   17.23    from H(3)[rule_format] gcd_dvd1[of a b] gcd_dvd2[of a b] 
   17.24    have th: "gcd a b dvd d" by blast
   17.25 -  from dvd_anti_sym[OF th gcd_greatest[OF H(1,2)]]  show "d = gcd a b" by blast 
   17.26 +  from dvd_antisym[OF th gcd_greatest[OF H(1,2)]]  show "d = gcd a b" by blast 
   17.27  qed
   17.28  
   17.29  lemma gcd_eq: assumes H: "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd u \<and> d dvd v"
    18.1 --- a/src/HOL/Old_Number_Theory/Pocklington.thy	Thu Nov 12 14:32:21 2009 -0800
    18.2 +++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Fri Nov 13 14:14:04 2009 +0100
    18.3 @@ -935,7 +935,7 @@
    18.4            p: "prime p" "p dvd m" by blast
    18.5          from dvd_trans[OF p(2) m(1)] p(1) H have "p = n" by blast
    18.6          with p(2) have "n dvd m"  by simp
    18.7 -        hence "m=n"  using dvd_anti_sym[OF m(1)] by simp }
    18.8 +        hence "m=n"  using dvd_antisym[OF m(1)] by simp }
    18.9        with n1 have "prime n"  unfolding prime_def by auto }
   18.10      ultimately have ?thesis using n by blast}
   18.11    ultimately       show ?thesis by auto
    19.1 --- a/src/HOL/Old_Number_Theory/Primes.thy	Thu Nov 12 14:32:21 2009 -0800
    19.2 +++ b/src/HOL/Old_Number_Theory/Primes.thy	Fri Nov 13 14:14:04 2009 +0100
    19.3 @@ -97,7 +97,7 @@
    19.4  text {* Elementary theory of divisibility *}
    19.5  lemma divides_ge: "(a::nat) dvd b \<Longrightarrow> b = 0 \<or> a \<le> b" unfolding dvd_def by auto
    19.6  lemma divides_antisym: "(x::nat) dvd y \<and> y dvd x \<longleftrightarrow> x = y"
    19.7 -  using dvd_anti_sym[of x y] by auto
    19.8 +  using dvd_antisym[of x y] by auto
    19.9  
   19.10  lemma divides_add_revr: assumes da: "(d::nat) dvd a" and dab:"d dvd (a + b)"
   19.11    shows "d dvd b"
    20.1 --- a/src/HOL/Probability/Borel.thy	Thu Nov 12 14:32:21 2009 -0800
    20.2 +++ b/src/HOL/Probability/Borel.thy	Fri Nov 13 14:14:04 2009 +0100
    20.3 @@ -73,7 +73,7 @@
    20.4      with w have "real(Suc(natceiling(inverse(g w - f w)))) > inverse(g w - f w)"
    20.5        by (metis lessI order_le_less_trans real_natceiling_ge real_of_nat_less_iff)       hence "inverse(real(Suc(natceiling(inverse(g w - f w)))))
    20.6               < inverse(inverse(g w - f w))" 
    20.7 -      by (metis less_iff_diff_less_0 less_imp_inverse_less linorder_neqE_ordered_idom nz positive_imp_inverse_positive real_le_anti_sym real_less_def w)
    20.8 +      by (metis less_iff_diff_less_0 less_imp_inverse_less linorder_neqE_ordered_idom nz positive_imp_inverse_positive real_le_antisym real_less_def w)
    20.9      hence "inverse(real(Suc(natceiling(inverse(g w - f w))))) < g w - f w"
   20.10        by (metis inverse_inverse_eq order_less_le_trans real_le_refl) 
   20.11      thus "\<exists>n. f w \<le> g w - inverse(real(Suc n))" using w
    21.1 --- a/src/HOL/Probability/Measure.thy	Thu Nov 12 14:32:21 2009 -0800
    21.2 +++ b/src/HOL/Probability/Measure.thy	Fri Nov 13 14:14:04 2009 +0100
    21.3 @@ -356,7 +356,7 @@
    21.4      by (metis add_commute le_add_diff_inverse nat_less_le)
    21.5    thus ?thesis
    21.6      by (auto simp add: disjoint_family_def)
    21.7 -      (metis insert_absorb insert_subset le_SucE le_anti_sym not_leE) 
    21.8 +      (metis insert_absorb insert_subset le_SucE le_antisym not_leE) 
    21.9  qed
   21.10  
   21.11  
    22.1 --- a/src/HOL/RealDef.thy	Thu Nov 12 14:32:21 2009 -0800
    22.2 +++ b/src/HOL/RealDef.thy	Fri Nov 13 14:14:04 2009 +0100
    22.3 @@ -321,7 +321,7 @@
    22.4  apply (auto intro: real_le_lemma)
    22.5  done
    22.6  
    22.7 -lemma real_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::real)"
    22.8 +lemma real_le_antisym: "[| z \<le> w; w \<le> z |] ==> z = (w::real)"
    22.9  by (cases z, cases w, simp add: real_le)
   22.10  
   22.11  lemma real_trans_lemma:
   22.12 @@ -347,8 +347,8 @@
   22.13  proof
   22.14    fix u v :: real
   22.15    show "u < v \<longleftrightarrow> u \<le> v \<and> \<not> v \<le> u" 
   22.16 -    by (auto simp add: real_less_def intro: real_le_anti_sym)
   22.17 -qed (assumption | rule real_le_refl real_le_trans real_le_anti_sym)+
   22.18 +    by (auto simp add: real_less_def intro: real_le_antisym)
   22.19 +qed (assumption | rule real_le_refl real_le_trans real_le_antisym)+
   22.20  
   22.21  (* Axiom 'linorder_linear' of class 'linorder': *)
   22.22  lemma real_le_linear: "(z::real) \<le> w | w \<le> z"
    23.1 --- a/src/HOL/SupInf.thy	Thu Nov 12 14:32:21 2009 -0800
    23.2 +++ b/src/HOL/SupInf.thy	Fri Nov 13 14:14:04 2009 +0100
    23.3 @@ -118,7 +118,7 @@
    23.4    shows "(!!x. x \<in> X \<Longrightarrow> x \<le> a) 
    23.5          \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y) \<Longrightarrow> Sup X = a"
    23.6    by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb
    23.7 -        insert_not_empty real_le_anti_sym)
    23.8 +        insert_not_empty real_le_antisym)
    23.9  
   23.10  lemma Sup_le:
   23.11    fixes S :: "real set"
   23.12 @@ -317,7 +317,7 @@
   23.13    fixes a :: real
   23.14    shows "(!!x. x \<in> X \<Longrightarrow> a \<le> x) \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> y \<le> x) \<Longrightarrow> y \<le> a) \<Longrightarrow> Inf X = a"
   23.15    by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel
   23.16 -        insert_absorb insert_not_empty real_le_anti_sym)
   23.17 +        insert_absorb insert_not_empty real_le_antisym)
   23.18  
   23.19  lemma Inf_ge: 
   23.20    fixes S :: "real set"
   23.21 @@ -397,7 +397,7 @@
   23.22    fixes S :: "real set"
   23.23    shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
   23.24  by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le
   23.25 -          real_le_anti_sym real_le_linear)
   23.26 +          real_le_antisym real_le_linear)
   23.27  
   23.28  lemma Inf_finite_gt_iff: 
   23.29    fixes S :: "real set"
    24.1 --- a/src/HOL/ex/LocaleTest2.thy	Thu Nov 12 14:32:21 2009 -0800
    24.2 +++ b/src/HOL/ex/LocaleTest2.thy	Fri Nov 13 14:14:04 2009 +0100
    24.3 @@ -29,7 +29,7 @@
    24.4  locale dpo =
    24.5    fixes le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>" 50)
    24.6    assumes refl [intro, simp]: "x \<sqsubseteq> x"
    24.7 -    and anti_sym [intro]: "[| x \<sqsubseteq> y; y \<sqsubseteq> x |] ==> x = y"
    24.8 +    and antisym [intro]: "[| x \<sqsubseteq> y; y \<sqsubseteq> x |] ==> x = y"
    24.9      and trans [trans]: "[| x \<sqsubseteq> y; y \<sqsubseteq> z |] ==> x \<sqsubseteq> z"
   24.10  
   24.11  begin
   24.12 @@ -87,7 +87,7 @@
   24.13    assume inf: "is_inf x y i"
   24.14    assume inf': "is_inf x y i'"
   24.15    show ?thesis
   24.16 -  proof (rule anti_sym)
   24.17 +  proof (rule antisym)
   24.18      from inf' show "i \<sqsubseteq> i'"
   24.19      proof (rule is_inf_greatest)
   24.20        from inf show "i \<sqsubseteq> x" ..
   24.21 @@ -159,7 +159,7 @@
   24.22    assume sup: "is_sup x y s"
   24.23    assume sup': "is_sup x y s'"
   24.24    show ?thesis
   24.25 -  proof (rule anti_sym)
   24.26 +  proof (rule antisym)
   24.27      from sup show "s \<sqsubseteq> s'"
   24.28      proof (rule is_sup_least)
   24.29        from sup' show "x \<sqsubseteq> s'" ..
   24.30 @@ -457,7 +457,7 @@
   24.31      moreover
   24.32      { assume c: "x \<sqsubseteq> y | x \<sqsubseteq> z"
   24.33        from c have "?l = x"
   24.34 -        by (metis (*anti_sym*) (*c*) (*circular*) (*join_assoc*)(* join_commute *) join_connection2 (*join_left*) join_related2 meet_connection(* meet_related2*) total trans)
   24.35 +        by (metis (*antisym*) (*c*) (*circular*) (*join_assoc*)(* join_commute *) join_connection2 (*join_left*) join_related2 meet_connection(* meet_related2*) total trans)
   24.36        also from c have "... = ?r"
   24.37          by (metis join_commute join_related2 meet_connection meet_related2 total)
   24.38        finally have "?l = ?r" . }