# HG changeset patch
# User nipkow
# Date 1258118056 -3600
# Node ID eb8b9c8a3662d2522d313f32054a4359c3ff04a5
# Parent  fc1af67532334c0e9f10cdd96e9f70baf50a8ee4# Parent  a4179bf442d14991bbb340f47bb95b986727b403
merged

diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/Algebra/IntRing.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -12,26 +12,6 @@
 
 subsection {* Some properties of @{typ int} *}
 
-lemma dvds_imp_abseq:
-  "\<lbrakk>l dvd k; k dvd l\<rbrakk> \<Longrightarrow> abs l = abs (k::int)"
-apply (subst abs_split, rule conjI)
- apply (clarsimp, subst abs_split, rule conjI)
-  apply (clarsimp)
-  apply (cases "k=0", simp)
-  apply (cases "l=0", simp)
-  apply (simp add: zdvd_anti_sym)
- apply clarsimp
- apply (cases "k=0", simp)
- apply (simp add: zdvd_anti_sym)
-apply (clarsimp, subst abs_split, rule conjI)
- apply (clarsimp)
- apply (cases "l=0", simp)
- apply (simp add: zdvd_anti_sym)
-apply (clarsimp)
-apply (subgoal_tac "-l = -k", simp)
-apply (intro zdvd_anti_sym, simp+)
-done
-
 lemma abseq_imp_dvd:
   assumes a_lk: "abs l = abs (k::int)"
   shows "l dvd k"
@@ -55,7 +35,7 @@
 lemma dvds_eq_abseq:
   "(l dvd k \<and> k dvd l) = (abs l = abs (k::int))"
 apply rule
- apply (simp add: dvds_imp_abseq)
+ apply (simp add: zdvd_antisym_abs)
 apply (rule conjI)
  apply (simp add: abseq_imp_dvd)+
 done
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/Algebra/Lattice.thy
--- a/src/HOL/Algebra/Lattice.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/Algebra/Lattice.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -18,7 +18,7 @@
 locale weak_partial_order = equivalence L for L (structure) +
   assumes le_refl [intro, simp]:
       "x \<in> carrier L ==> x \<sqsubseteq> x"
-    and weak_le_anti_sym [intro]:
+    and weak_le_antisym [intro]:
       "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x .= y"
     and le_trans [trans]:
       "[| x \<sqsubseteq> y; y \<sqsubseteq> z; x \<in> carrier L; y \<in> carrier L; z \<in> carrier L |] ==> x \<sqsubseteq> z"
@@ -636,7 +636,7 @@
   fix s
   assume sup: "least L s (Upper L {x, y, z})"
   show "x \<squnion> (y \<squnion> z) .= s"
-  proof (rule weak_le_anti_sym)
+  proof (rule weak_le_antisym)
     from sup L show "x \<squnion> (y \<squnion> z) \<sqsubseteq> s"
       by (fastsimp intro!: join_le elim: least_Upper_above)
   next
@@ -877,7 +877,7 @@
   fix i
   assume inf: "greatest L i (Lower L {x, y, z})"
   show "x \<sqinter> (y \<sqinter> z) .= i"
-  proof (rule weak_le_anti_sym)
+  proof (rule weak_le_antisym)
     from inf L show "i \<sqsubseteq> x \<sqinter> (y \<sqinter> z)"
       by (fastsimp intro!: meet_le elim: greatest_Lower_below)
   next
@@ -1089,11 +1089,11 @@
   assumes eq_is_equal: "op .= = op ="
 begin
 
-declare weak_le_anti_sym [rule del]
+declare weak_le_antisym [rule del]
 
-lemma le_anti_sym [intro]:
+lemma le_antisym [intro]:
   "[| x \<sqsubseteq> y; y \<sqsubseteq> x; x \<in> carrier L; y \<in> carrier L |] ==> x = y"
-  using weak_le_anti_sym unfolding eq_is_equal .
+  using weak_le_antisym unfolding eq_is_equal .
 
 lemma lless_eq:
   "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y & x \<noteq> y"
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/Algebra/Sylow.thy
--- a/src/HOL/Algebra/Sylow.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/Algebra/Sylow.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -344,7 +344,7 @@
 done
 
 lemma (in sylow_central) card_H_eq: "card(H) = p^a"
-by (blast intro: le_anti_sym lemma_leq1 lemma_leq2)
+by (blast intro: le_antisym lemma_leq1 lemma_leq2)
 
 lemma (in sylow) sylow_thm: "\<exists>H. subgroup H G & card(H) = p^a"
 apply (cut_tac lemma_A1, clarify)
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/Algebra/UnivPoly.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -811,7 +811,7 @@
 lemma deg_eqI:
   "[| !!m. n < m ==> coeff P p m = \<zero>;
       !!n. n ~= 0 ==> coeff P p n ~= \<zero>; p \<in> carrier P |] ==> deg R p = n"
-by (fast intro: le_anti_sym deg_aboveI deg_belowI)
+by (fast intro: le_antisym deg_aboveI deg_belowI)
 
 text {* Degree and polynomial operations *}
 
@@ -826,11 +826,11 @@
 
 lemma deg_monom [simp]:
   "[| a ~= \<zero>; a \<in> carrier R |] ==> deg R (monom P a n) = n"
-  by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI)
+  by (fastsimp intro: le_antisym deg_aboveI deg_belowI)
 
 lemma deg_const [simp]:
   assumes R: "a \<in> carrier R" shows "deg R (monom P a 0) = 0"
-proof (rule le_anti_sym)
+proof (rule le_antisym)
   show "deg R (monom P a 0) <= 0" by (rule deg_aboveI) (simp_all add: R)
 next
   show "0 <= deg R (monom P a 0)" by (rule deg_belowI) (simp_all add: R)
@@ -838,7 +838,7 @@
 
 lemma deg_zero [simp]:
   "deg R \<zero>\<^bsub>P\<^esub> = 0"
-proof (rule le_anti_sym)
+proof (rule le_antisym)
   show "deg R \<zero>\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all
 next
   show "0 <= deg R \<zero>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all
@@ -846,7 +846,7 @@
 
 lemma deg_one [simp]:
   "deg R \<one>\<^bsub>P\<^esub> = 0"
-proof (rule le_anti_sym)
+proof (rule le_antisym)
   show "deg R \<one>\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all
 next
   show "0 <= deg R \<one>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all
@@ -854,7 +854,7 @@
 
 lemma deg_uminus [simp]:
   assumes R: "p \<in> carrier P" shows "deg R (\<ominus>\<^bsub>P\<^esub> p) = deg R p"
-proof (rule le_anti_sym)
+proof (rule le_antisym)
   show "deg R (\<ominus>\<^bsub>P\<^esub> p) <= deg R p" by (simp add: deg_aboveI deg_aboveD R)
 next
   show "deg R p <= deg R (\<ominus>\<^bsub>P\<^esub> p)"
@@ -878,7 +878,7 @@
 lemma deg_smult [simp]:
   assumes R: "a \<in> carrier R" "p \<in> carrier P"
   shows "deg R (a \<odot>\<^bsub>P\<^esub> p) = (if a = \<zero> then 0 else deg R p)"
-proof (rule le_anti_sym)
+proof (rule le_antisym)
   show "deg R (a \<odot>\<^bsub>P\<^esub> p) <= (if a = \<zero> then 0 else deg R p)"
     using R by (rule deg_smult_ring)
 next
@@ -920,7 +920,7 @@
 lemma deg_mult [simp]:
   "[| p ~= \<zero>\<^bsub>P\<^esub>; q ~= \<zero>\<^bsub>P\<^esub>; p \<in> carrier P; q \<in> carrier P |] ==>
   deg R (p \<otimes>\<^bsub>P\<^esub> q) = deg R p + deg R q"
-proof (rule le_anti_sym)
+proof (rule le_antisym)
   assume "p \<in> carrier P" " q \<in> carrier P"
   then show "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q" by (rule deg_mult_ring)
 next
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/Algebra/poly/UnivPoly2.thy
--- a/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -557,7 +557,7 @@
 lemma deg_eqI:
   "[| !!m. n < m ==> coeff p m = 0;
       !!n. n ~= 0 ==> coeff p n ~= 0|] ==> deg p = n"
-by (fast intro: le_anti_sym deg_aboveI deg_belowI)
+by (fast intro: le_antisym deg_aboveI deg_belowI)
 
 (* Degree and polynomial operations *)
 
@@ -571,11 +571,11 @@
 
 lemma deg_monom [simp]:
   "a ~= 0 ==> deg (monom a n::'a::ring up) = n"
-by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI)
+by (fastsimp intro: le_antisym deg_aboveI deg_belowI)
 
 lemma deg_const [simp]:
   "deg (monom (a::'a::ring) 0) = 0"
-proof (rule le_anti_sym)
+proof (rule le_antisym)
   show "deg (monom a 0) <= 0" by (rule deg_aboveI) simp
 next
   show "0 <= deg (monom a 0)" by (rule deg_belowI) simp
@@ -583,7 +583,7 @@
 
 lemma deg_zero [simp]:
   "deg 0 = 0"
-proof (rule le_anti_sym)
+proof (rule le_antisym)
   show "deg 0 <= 0" by (rule deg_aboveI) simp
 next
   show "0 <= deg 0" by (rule deg_belowI) simp
@@ -591,7 +591,7 @@
 
 lemma deg_one [simp]:
   "deg 1 = 0"
-proof (rule le_anti_sym)
+proof (rule le_antisym)
   show "deg 1 <= 0" by (rule deg_aboveI) simp
 next
   show "0 <= deg 1" by (rule deg_belowI) simp
@@ -612,7 +612,7 @@
 
 lemma deg_uminus [simp]:
   "deg (-p::('a::ring) up) = deg p"
-proof (rule le_anti_sym)
+proof (rule le_antisym)
   show "deg (- p) <= deg p" by (simp add: deg_aboveI deg_aboveD)
 next
   show "deg p <= deg (- p)" 
@@ -626,7 +626,7 @@
 
 lemma deg_smult [simp]:
   "deg ((a::'a::domain) *s p) = (if a = 0 then 0 else deg p)"
-proof (rule le_anti_sym)
+proof (rule le_antisym)
   show "deg (a *s p) <= (if a = 0 then 0 else deg p)" by (rule deg_smult_ring)
 next
   show "(if a = 0 then 0 else deg p) <= deg (a *s p)"
@@ -657,7 +657,7 @@
 
 lemma deg_mult [simp]:
   "[| (p::'a::domain up) ~= 0; q ~= 0|] ==> deg (p * q) = deg p + deg q"
-proof (rule le_anti_sym)
+proof (rule le_antisym)
   show "deg (p * q) <= deg p + deg q" by (rule deg_mult_ring)
 next
   let ?s = "(%i. coeff p i * coeff q (deg p + deg q - i))"
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -2344,7 +2344,7 @@
 lemma card_bij_eq:
   "[|inj_on f A; f ` A \<subseteq> B; inj_on g B; g ` B \<subseteq> A;
      finite A; finite B |] ==> card A = card B"
-by (auto intro: le_anti_sym card_inj_on_le)
+by (auto intro: le_antisym card_inj_on_le)
 
 
 subsubsection {* Cardinality of products *}
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/GCD.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -312,13 +312,13 @@
   by (insert gcd_zero_int [of m n], insert gcd_ge_0_int [of m n], arith)
 
 lemma gcd_commute_nat: "gcd (m::nat) n = gcd n m"
-  by (rule dvd_anti_sym, auto)
+  by (rule dvd_antisym, auto)
 
 lemma gcd_commute_int: "gcd (m::int) n = gcd n m"
   by (auto simp add: gcd_int_def gcd_commute_nat)
 
 lemma gcd_assoc_nat: "gcd (gcd (k::nat) m) n = gcd k (gcd m n)"
-  apply (rule dvd_anti_sym)
+  apply (rule dvd_antisym)
   apply (blast intro: dvd_trans)+
 done
 
@@ -339,23 +339,18 @@
 lemma gcd_unique_nat: "(d::nat) dvd a \<and> d dvd b \<and>
     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
   apply auto
-  apply (rule dvd_anti_sym)
+  apply (rule dvd_antisym)
   apply (erule (1) gcd_greatest_nat)
   apply auto
 done
 
 lemma gcd_unique_int: "d >= 0 & (d::int) dvd a \<and> d dvd b \<and>
     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
-  apply (case_tac "d = 0")
-  apply force
-  apply (rule iffI)
-  apply (rule zdvd_anti_sym)
-  apply arith
-  apply (subst gcd_pos_int)
-  apply clarsimp
-  apply (drule_tac x = "d + 1" in spec)
-  apply (frule zdvd_imp_le)
-  apply (auto intro: gcd_greatest_int)
+apply (case_tac "d = 0")
+ apply simp
+apply (rule iffI)
+ apply (rule zdvd_antisym_nonneg)
+ apply (auto intro: gcd_greatest_int)
 done
 
 lemma gcd_proj1_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> gcd x y = x"
@@ -417,7 +412,7 @@
   by (auto intro: coprime_dvd_mult_int)
 
 lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
-  apply (rule dvd_anti_sym)
+  apply (rule dvd_antisym)
   apply (rule gcd_greatest_nat)
   apply (rule_tac n = k in coprime_dvd_mult_nat)
   apply (simp add: gcd_assoc_nat)
@@ -1381,11 +1376,11 @@
 
 lemma lcm_unique_nat: "(a::nat) dvd d \<and> b dvd d \<and>
     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
-  by (auto intro: dvd_anti_sym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat)
+  by (auto intro: dvd_antisym lcm_least_nat lcm_dvd1_nat lcm_dvd2_nat)
 
 lemma lcm_unique_int: "d >= 0 \<and> (a::int) dvd d \<and> b dvd d \<and>
     (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
-  by (auto intro: dvd_anti_sym [transferred] lcm_least_int)
+  by (auto intro: dvd_antisym [transferred] lcm_least_int)
 
 lemma lcm_proj2_if_dvd_nat [simp]: "(x::nat) dvd y \<Longrightarrow> lcm x y = y"
   apply (rule sym)
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/Hoare/Arith2.thy
--- a/src/HOL/Hoare/Arith2.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/Hoare/Arith2.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -58,7 +58,7 @@
   apply (frule cd_nnn)
   apply (rule some_equality [symmetric])
   apply (blast dest: cd_le)
-  apply (blast intro: le_anti_sym dest: cd_le)
+  apply (blast intro: le_antisym dest: cd_le)
   done
 
 lemma gcd_swap: "gcd m n = gcd n m"
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/Import/HOL/arithmetic.imp
--- a/src/HOL/Import/HOL/arithmetic.imp	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/Import/HOL/arithmetic.imp	Fri Nov 13 14:14:16 2009 +0100
@@ -191,7 +191,7 @@
   "LESS_EQ_ADD_SUB" > "Nat.add_diff_assoc"
   "LESS_EQ_ADD" > "Nat.le_add1"
   "LESS_EQ_0" > "Nat.le_0_eq"
-  "LESS_EQUAL_ANTISYM" > "Nat.le_anti_sym"
+  "LESS_EQUAL_ANTISYM" > "Nat.le_antisym"
   "LESS_EQUAL_ADD" > "HOL4Base.arithmetic.LESS_EQUAL_ADD"
   "LESS_EQ" > "Nat.le_simps_3"
   "LESS_DIV_EQ_ZERO" > "Divides.div_less"
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/Import/HOL/divides.imp
--- a/src/HOL/Import/HOL/divides.imp	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/Import/HOL/divides.imp	Fri Nov 13 14:14:16 2009 +0100
@@ -16,7 +16,7 @@
   "DIVIDES_MULT" > "Divides.dvd_mult2"
   "DIVIDES_LE" > "Divides.dvd_imp_le"
   "DIVIDES_FACT" > "HOL4Base.divides.DIVIDES_FACT"
-  "DIVIDES_ANTISYM" > "Divides.dvd_anti_sym"
+  "DIVIDES_ANTISYM" > "Divides.dvd_antisym"
   "DIVIDES_ADD_2" > "HOL4Base.divides.DIVIDES_ADD_2"
   "DIVIDES_ADD_1" > "Ring_and_Field.dvd_add"
   "ALL_DIVIDES_0" > "Divides.dvd_0_right"
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/Int.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -1986,15 +1986,18 @@
 
 subsection {* The divides relation *}
 
-lemma zdvd_anti_sym:
-    "0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)"
+lemma zdvd_antisym_nonneg:
+    "0 <= m ==> 0 <= n ==> m dvd n ==> n dvd m ==> m = (n::int)"
   apply (simp add: dvd_def, auto)
-  apply (simp add: mult_assoc zero_less_mult_iff zmult_eq_1_iff)
+  apply (auto simp add: mult_assoc zero_le_mult_iff zmult_eq_1_iff)
   done
 
-lemma zdvd_dvd_eq: assumes "a \<noteq> 0" and "(a::int) dvd b" and "b dvd a" 
+lemma zdvd_antisym_abs: assumes "(a::int) dvd b" and "b dvd a" 
   shows "\<bar>a\<bar> = \<bar>b\<bar>"
-proof-
+proof cases
+  assume "a = 0" with assms show ?thesis by simp
+next
+  assume "a \<noteq> 0"
   from `a dvd b` obtain k where k:"b = a*k" unfolding dvd_def by blast 
   from `b dvd a` obtain k' where k':"a = b*k'" unfolding dvd_def by blast 
   from k k' have "a = a*k*k'" by simp
@@ -2326,7 +2329,7 @@
 
 lemmas zle_refl = order_refl [of "w::int", standard]
 lemmas zle_trans = order_trans [where 'a=int and x="i" and y="j" and z="k", standard]
-lemmas zle_anti_sym = order_antisym [of "z::int" "w", standard]
+lemmas zle_antisym = order_antisym [of "z::int" "w", standard]
 lemmas zle_linear = linorder_linear [of "z::int" "w", standard]
 lemmas zless_linear = linorder_less_linear [where 'a = int]
 
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/Library/Abstract_Rat.thy
--- a/src/HOL/Library/Abstract_Rat.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/Library/Abstract_Rat.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -206,7 +206,7 @@
       apply simp
       apply algebra
       done
-    from zdvd_dvd_eq[OF bz coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
+    from zdvd_antisym_abs[OF coprime_dvd_mult_int[OF gcd1(2) raw_dvd(2)]
       coprime_dvd_mult_int[OF gcd1(4) raw_dvd(4)]]
       have eq1: "b = b'" using pos by arith  
       with eq have "a = a'" using pos by simp
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/Matrix/Matrix.thy
--- a/src/HOL/Matrix/Matrix.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/Matrix/Matrix.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -873,7 +873,7 @@
 have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+
 from th show ?thesis 
 apply (auto)
-apply (rule le_anti_sym)
+apply (rule le_antisym)
 apply (subst nrows_le)
 apply (simp add: singleton_matrix_def, auto)
 apply (subst RepAbs_matrix)
@@ -889,7 +889,7 @@
 have th: "\<not> (\<forall>m. m \<le> j)" "\<exists>n. \<not> n \<le> i" by arith+
 from th show ?thesis 
 apply (auto)
-apply (rule le_anti_sym)
+apply (rule le_antisym)
 apply (subst ncols_le)
 apply (simp add: singleton_matrix_def, auto)
 apply (subst RepAbs_matrix)
@@ -1004,7 +1004,7 @@
   apply (subst foldseq_almostzero[of _ j])
   apply (simp add: prems)+
   apply (auto)
-  apply (metis comm_monoid_add.mult_1 le_anti_sym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
+  apply (metis comm_monoid_add.mult_1 le_antisym le_diff_eq not_neg_nat zero_le_imp_of_nat zle_int)
   done
 
 lemma mult_matrix_ext:
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/Nat.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -596,7 +596,7 @@
 lemma le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::nat)"
   by (rule order_trans)
 
-lemma le_anti_sym: "[| m \<le> n; n \<le> m |] ==> m = (n::nat)"
+lemma le_antisym: "[| m \<le> n; n \<le> m |] ==> m = (n::nat)"
   by (rule antisym)
 
 lemma nat_less_le: "((m::nat) < n) = (m \<le> n & m \<noteq> n)"
@@ -1611,14 +1611,14 @@
 lemma nat_dvd_1_iff_1 [simp]: "m dvd (1::nat) \<longleftrightarrow> m = 1"
 by (simp add: dvd_def)
 
-lemma dvd_anti_sym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
+lemma dvd_antisym: "[| m dvd n; n dvd m |] ==> m = (n::nat)"
   unfolding dvd_def
   by (force dest: mult_eq_self_implies_10 simp add: mult_assoc mult_eq_1_iff)
 
 text {* @{term "op dvd"} is a partial order *}
 
 interpretation dvd: order "op dvd" "\<lambda>n m \<Colon> nat. n dvd m \<and> \<not> m dvd n"
-  proof qed (auto intro: dvd_refl dvd_trans dvd_anti_sym)
+  proof qed (auto intro: dvd_refl dvd_trans dvd_antisym)
 
 lemma dvd_diff_nat[simp]: "[| k dvd m; k dvd n |] ==> k dvd (m-n :: nat)"
 unfolding dvd_def
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -844,7 +844,7 @@
     mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
   shows "x = y"
 
-  apply (rule dvd_anti_sym)
+  apply (rule dvd_antisym)
   apply (auto intro: multiplicity_dvd'_nat) 
 done
 
@@ -854,7 +854,7 @@
     mult_eq [simp]: "!!p. prime p \<Longrightarrow> multiplicity p x = multiplicity p y"
   shows "x = y"
 
-  apply (rule dvd_anti_sym [transferred])
+  apply (rule dvd_antisym [transferred])
   apply (auto intro: multiplicity_dvd'_int) 
 done
 
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/Old_Number_Theory/IntPrimes.thy
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -204,7 +204,7 @@
     apply (case_tac [2] "0 \<le> ka")
   apply (metis zdvd_mult_div_cancel dvd_refl dvd_mult_left zmult_commute zrelprime_zdvd_zmult)
   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)
-  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)
+  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)
   apply (metis dvd_triv_left)
   done
 
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/Old_Number_Theory/Legacy_GCD.thy
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -23,7 +23,7 @@
 text {* Uniqueness *}
 
 lemma is_gcd_unique: "is_gcd a b m \<Longrightarrow> is_gcd a b n \<Longrightarrow> m = n"
-  by (simp add: is_gcd_def) (blast intro: dvd_anti_sym)
+  by (simp add: is_gcd_def) (blast intro: dvd_antisym)
 
 text {* Connection to divides relation *}
 
@@ -156,7 +156,7 @@
   by (auto intro: relprime_dvd_mult dvd_mult2)
 
 lemma gcd_mult_cancel: "gcd k n = 1 ==> gcd (k * m) n = gcd m n"
-  apply (rule dvd_anti_sym)
+  apply (rule dvd_antisym)
    apply (rule gcd_greatest)
     apply (rule_tac n = k in relprime_dvd_mult)
      apply (simp add: gcd_assoc)
@@ -223,7 +223,7 @@
   assume H: "d dvd a" "d dvd b" "\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d"
   from H(3)[rule_format] gcd_dvd1[of a b] gcd_dvd2[of a b] 
   have th: "gcd a b dvd d" by blast
-  from dvd_anti_sym[OF th gcd_greatest[OF H(1,2)]]  show "d = gcd a b" by blast 
+  from dvd_antisym[OF th gcd_greatest[OF H(1,2)]]  show "d = gcd a b" by blast 
 qed
 
 lemma gcd_eq: assumes H: "\<forall>d. d dvd x \<and> d dvd y \<longleftrightarrow> d dvd u \<and> d dvd v"
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/Old_Number_Theory/Pocklington.thy
--- a/src/HOL/Old_Number_Theory/Pocklington.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -935,7 +935,7 @@
           p: "prime p" "p dvd m" by blast
         from dvd_trans[OF p(2) m(1)] p(1) H have "p = n" by blast
         with p(2) have "n dvd m"  by simp
-        hence "m=n"  using dvd_anti_sym[OF m(1)] by simp }
+        hence "m=n"  using dvd_antisym[OF m(1)] by simp }
       with n1 have "prime n"  unfolding prime_def by auto }
     ultimately have ?thesis using n by blast}
   ultimately       show ?thesis by auto
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/Old_Number_Theory/Primes.thy
--- a/src/HOL/Old_Number_Theory/Primes.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/Old_Number_Theory/Primes.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -97,7 +97,7 @@
 text {* Elementary theory of divisibility *}
 lemma divides_ge: "(a::nat) dvd b \<Longrightarrow> b = 0 \<or> a \<le> b" unfolding dvd_def by auto
 lemma divides_antisym: "(x::nat) dvd y \<and> y dvd x \<longleftrightarrow> x = y"
-  using dvd_anti_sym[of x y] by auto
+  using dvd_antisym[of x y] by auto
 
 lemma divides_add_revr: assumes da: "(d::nat) dvd a" and dab:"d dvd (a + b)"
   shows "d dvd b"
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/Probability/Borel.thy
--- a/src/HOL/Probability/Borel.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/Probability/Borel.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -73,7 +73,7 @@
     with w have "real(Suc(natceiling(inverse(g w - f w)))) > inverse(g w - f w)"
       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)))))
              < inverse(inverse(g w - f w))" 
-      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)
+      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)
     hence "inverse(real(Suc(natceiling(inverse(g w - f w))))) < g w - f w"
       by (metis inverse_inverse_eq order_less_le_trans real_le_refl) 
     thus "\<exists>n. f w \<le> g w - inverse(real(Suc n))" using w
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/Probability/Measure.thy
--- a/src/HOL/Probability/Measure.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/Probability/Measure.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -356,7 +356,7 @@
     by (metis add_commute le_add_diff_inverse nat_less_le)
   thus ?thesis
     by (auto simp add: disjoint_family_def)
-      (metis insert_absorb insert_subset le_SucE le_anti_sym not_leE) 
+      (metis insert_absorb insert_subset le_SucE le_antisym not_leE) 
 qed
 
 
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/RealDef.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -321,7 +321,7 @@
 apply (auto intro: real_le_lemma)
 done
 
-lemma real_le_anti_sym: "[| z \<le> w; w \<le> z |] ==> z = (w::real)"
+lemma real_le_antisym: "[| z \<le> w; w \<le> z |] ==> z = (w::real)"
 by (cases z, cases w, simp add: real_le)
 
 lemma real_trans_lemma:
@@ -347,8 +347,8 @@
 proof
   fix u v :: real
   show "u < v \<longleftrightarrow> u \<le> v \<and> \<not> v \<le> u" 
-    by (auto simp add: real_less_def intro: real_le_anti_sym)
-qed (assumption | rule real_le_refl real_le_trans real_le_anti_sym)+
+    by (auto simp add: real_less_def intro: real_le_antisym)
+qed (assumption | rule real_le_refl real_le_trans real_le_antisym)+
 
 (* Axiom 'linorder_linear' of class 'linorder': *)
 lemma real_le_linear: "(z::real) \<le> w | w \<le> z"
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/SupInf.thy
--- a/src/HOL/SupInf.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/SupInf.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -118,7 +118,7 @@
   shows "(!!x. x \<in> X \<Longrightarrow> x \<le> a) 
         \<Longrightarrow> (!!y. (!!x. x \<in> X \<Longrightarrow> x \<le> y) \<Longrightarrow> a \<le> y) \<Longrightarrow> Sup X = a"
   by (metis Sup_least Sup_upper add_le_cancel_left diff_add_cancel insert_absorb
-        insert_not_empty real_le_anti_sym)
+        insert_not_empty real_le_antisym)
 
 lemma Sup_le:
   fixes S :: "real set"
@@ -317,7 +317,7 @@
   fixes a :: real
   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"
   by (metis Inf_greatest Inf_lower add_le_cancel_left diff_add_cancel
-        insert_absorb insert_not_empty real_le_anti_sym)
+        insert_absorb insert_not_empty real_le_antisym)
 
 lemma Inf_ge: 
   fixes S :: "real set"
@@ -397,7 +397,7 @@
   fixes S :: "real set"
   shows "finite S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> a \<ge> Inf S \<longleftrightarrow> (\<exists> x \<in> S. a \<ge> x)"
 by (metis Inf_finite_Min Inf_finite_ge_iff Inf_finite_in Min_le
-          real_le_anti_sym real_le_linear)
+          real_le_antisym real_le_linear)
 
 lemma Inf_finite_gt_iff: 
   fixes S :: "real set"
diff -r fc1af6753233 -r eb8b9c8a3662 src/HOL/ex/LocaleTest2.thy
--- a/src/HOL/ex/LocaleTest2.thy	Fri Nov 13 14:03:24 2009 +0100
+++ b/src/HOL/ex/LocaleTest2.thy	Fri Nov 13 14:14:16 2009 +0100
@@ -29,7 +29,7 @@
 locale dpo =
   fixes le :: "['a, 'a] => bool" (infixl "\<sqsubseteq>" 50)
   assumes refl [intro, simp]: "x \<sqsubseteq> x"
-    and anti_sym [intro]: "[| x \<sqsubseteq> y; y \<sqsubseteq> x |] ==> x = y"
+    and antisym [intro]: "[| x \<sqsubseteq> y; y \<sqsubseteq> x |] ==> x = y"
     and trans [trans]: "[| x \<sqsubseteq> y; y \<sqsubseteq> z |] ==> x \<sqsubseteq> z"
 
 begin
@@ -87,7 +87,7 @@
   assume inf: "is_inf x y i"
   assume inf': "is_inf x y i'"
   show ?thesis
-  proof (rule anti_sym)
+  proof (rule antisym)
     from inf' show "i \<sqsubseteq> i'"
     proof (rule is_inf_greatest)
       from inf show "i \<sqsubseteq> x" ..
@@ -159,7 +159,7 @@
   assume sup: "is_sup x y s"
   assume sup': "is_sup x y s'"
   show ?thesis
-  proof (rule anti_sym)
+  proof (rule antisym)
     from sup show "s \<sqsubseteq> s'"
     proof (rule is_sup_least)
       from sup' show "x \<sqsubseteq> s'" ..
@@ -457,7 +457,7 @@
     moreover
     { assume c: "x \<sqsubseteq> y | x \<sqsubseteq> z"
       from c have "?l = x"
-        by (metis (*anti_sym*) (*c*) (*circular*) (*join_assoc*)(* join_commute *) join_connection2 (*join_left*) join_related2 meet_connection(* meet_related2*) total trans)
+        by (metis (*antisym*) (*c*) (*circular*) (*join_assoc*)(* join_commute *) join_connection2 (*join_left*) join_related2 meet_connection(* meet_related2*) total trans)
       also from c have "... = ?r"
         by (metis join_commute join_related2 meet_connection meet_related2 total)
       finally have "?l = ?r" . }