--- a/src/HOL/Algebra/IntRing.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Algebra/IntRing.thy Fri Nov 13 14:14:04 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
--- a/src/HOL/Algebra/Lattice.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Algebra/Lattice.thy Fri Nov 13 14:14:04 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"
--- a/src/HOL/Algebra/Sylow.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Algebra/Sylow.thy Fri Nov 13 14:14:04 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)
--- a/src/HOL/Algebra/UnivPoly.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Algebra/UnivPoly.thy Fri Nov 13 14:14:04 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
--- a/src/HOL/Algebra/poly/UnivPoly2.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Fri Nov 13 14:14:04 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))"
--- a/src/HOL/Finite_Set.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Finite_Set.thy Fri Nov 13 14:14:04 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 *}
--- a/src/HOL/GCD.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/GCD.thy Fri Nov 13 14:14:04 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)
--- a/src/HOL/Hoare/Arith2.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Hoare/Arith2.thy Fri Nov 13 14:14:04 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"
--- a/src/HOL/Import/HOL/arithmetic.imp Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Import/HOL/arithmetic.imp Fri Nov 13 14:14:04 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"
--- a/src/HOL/Import/HOL/divides.imp Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Import/HOL/divides.imp Fri Nov 13 14:14:04 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"
--- a/src/HOL/Int.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Int.thy Fri Nov 13 14:14:04 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]
--- a/src/HOL/Library/Abstract_Rat.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Library/Abstract_Rat.thy Fri Nov 13 14:14:04 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
--- a/src/HOL/Matrix/Matrix.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Matrix/Matrix.thy Fri Nov 13 14:14:04 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:
--- a/src/HOL/Nat.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Nat.thy Fri Nov 13 14:14:04 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
--- a/src/HOL/Number_Theory/UniqueFactorization.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Fri Nov 13 14:14:04 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
--- a/src/HOL/Old_Number_Theory/IntPrimes.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Old_Number_Theory/IntPrimes.thy Fri Nov 13 14:14:04 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
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy Fri Nov 13 14:14:04 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"
--- a/src/HOL/Old_Number_Theory/Pocklington.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Old_Number_Theory/Pocklington.thy Fri Nov 13 14:14:04 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
--- a/src/HOL/Old_Number_Theory/Primes.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Old_Number_Theory/Primes.thy Fri Nov 13 14:14:04 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"
--- a/src/HOL/Probability/Borel.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Probability/Borel.thy Fri Nov 13 14:14:04 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
--- a/src/HOL/Probability/Measure.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/Probability/Measure.thy Fri Nov 13 14:14:04 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
--- a/src/HOL/RealDef.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/RealDef.thy Fri Nov 13 14:14:04 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"
--- a/src/HOL/SupInf.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/SupInf.thy Fri Nov 13 14:14:04 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"
--- a/src/HOL/ex/LocaleTest2.thy Thu Nov 12 14:32:21 2009 -0800
+++ b/src/HOL/ex/LocaleTest2.thy Fri Nov 13 14:14:04 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" . }