# HG changeset patch
# User huffman
# Date 1315411378 25200
# Node ID a92f65e174cf3aa7d1f9490cfe102497455a0b48
# Parent  e0da66339e472045450d41508bba1b57b04221c9
avoid using legacy theorem names

diff -r e0da66339e47 -r a92f65e174cf src/HOL/Algebra/IntRing.thy
--- a/src/HOL/Algebra/IntRing.thy	Wed Sep 07 14:58:40 2011 +0200
+++ b/src/HOL/Algebra/IntRing.thy	Wed Sep 07 09:02:58 2011 -0700
@@ -35,8 +35,8 @@
   apply (rule abelian_groupI, simp_all)
   defer 1
   apply (rule comm_monoidI, simp_all)
- apply (rule zadd_zmult_distrib)
-apply (fast intro: zadd_zminus_inverse2)
+ apply (rule left_distrib)
+apply (fast intro: left_minus)
 done
 
 (*
@@ -298,7 +298,7 @@
   from this obtain x 
       where "1 = x * p" by best
   from this [symmetric]
-      have "p * x = 1" by (subst zmult_commute)
+      have "p * x = 1" by (subst mult_commute)
   hence "\<bar>p * x\<bar> = 1" by simp
   hence "\<bar>p\<bar> = 1" by (rule abs_zmult_eq_1)
   from this and prime
diff -r e0da66339e47 -r a92f65e174cf src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Wed Sep 07 14:58:40 2011 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Wed Sep 07 09:02:58 2011 -0700
@@ -1818,7 +1818,7 @@
 
 lemma INTEG_cring: "cring INTEG"
   by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
-    zadd_zminus_inverse2 zadd_zmult_distrib)
+    left_minus left_distrib)
 
 lemma INTEG_id_eval:
   "UP_pre_univ_prop INTEG INTEG id"
diff -r e0da66339e47 -r a92f65e174cf src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy
--- a/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy	Wed Sep 07 14:58:40 2011 +0200
+++ b/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy	Wed Sep 07 09:02:58 2011 -0700
@@ -77,10 +77,10 @@
 boogie_vc max (examine: L_14_5c L_14_5b L_14_5a) 
 proof boogie_cases
   case L_14_5c
-  thus ?case by (metis less_le_not_le zle_add1_eq_le zless_linear)
+  thus ?case by (metis less_le_not_le zle_add1_eq_le less_linear)
 next
   case L_14_5b
-  thus ?case by (metis less_le_not_le xt1(10) zle_linear zless_add1_eq)
+  thus ?case by (metis less_le_not_le xt1(10) linorder_linear zless_add1_eq)
 next
   case L_14_5a
   note max0 = `max0 = array 0`
diff -r e0da66339e47 -r a92f65e174cf src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Wed Sep 07 14:58:40 2011 +0200
+++ b/src/HOL/Code_Numeral.thy	Wed Sep 07 09:02:58 2011 -0700
@@ -274,7 +274,7 @@
   then have "int ((nat_of k div 2) * 2 + nat_of k mod 2) = int (nat_of k)" 
     by simp
   then have "int (nat_of k) = int (nat_of k div 2) * 2 + int (nat_of k mod 2)" 
-    unfolding int_mult zadd_int [symmetric] by simp
+    unfolding of_nat_mult of_nat_add by simp
   then show ?thesis by (auto simp add: int_of_def mult_ac)
 qed
 
diff -r e0da66339e47 -r a92f65e174cf src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Wed Sep 07 14:58:40 2011 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Sep 07 09:02:58 2011 -0700
@@ -295,7 +295,7 @@
         unfolding real_sqrt_mult[of _ "pow2 (?E mod 2)"] real_sqrt_abs2 by auto
       also have "\<dots> < pow2 (?E div 2) * 2"
         by (rule mult_strict_left_mono, auto intro: E_mod_pow)
-      also have "\<dots> = pow2 (?E div 2 + 1)" unfolding zadd_commute[of _ 1] pow2_add1 by auto
+      also have "\<dots> = pow2 (?E div 2 + 1)" unfolding add_commute[of _ 1] pow2_add1 by auto
       finally show ?thesis by auto
     qed
     finally show ?thesis
diff -r e0da66339e47 -r a92f65e174cf src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Wed Sep 07 14:58:40 2011 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Sep 07 09:02:58 2011 -0700
@@ -1318,7 +1318,7 @@
     also have "\<dots> = (j dvd (- (c*x - ?e)))"
     by (simp only: dvd_minus_iff)
   also have "\<dots> = (j dvd (c* (- x)) + ?e)"
-    apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus zadd_ac zminus_zadd_distrib)
+    apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus add_ac minus_add_distrib)
     by (simp add: algebra_simps)
   also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
     using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
@@ -1330,7 +1330,7 @@
     also have "\<dots> = (j dvd (- (c*x - ?e)))"
     by (simp only: dvd_minus_iff)
   also have "\<dots> = (j dvd (c* (- x)) + ?e)"
-    apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus zadd_ac zminus_zadd_distrib)
+    apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus add_ac minus_add_distrib)
     by (simp add: algebra_simps)
   also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
     using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
diff -r e0da66339e47 -r a92f65e174cf src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Wed Sep 07 14:58:40 2011 +0200
+++ b/src/HOL/GCD.thy	Wed Sep 07 09:02:58 2011 -0700
@@ -485,16 +485,16 @@
 done
 
 lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n"
-by (metis gcd_red_int mod_add_self1 zadd_commute)
+by (metis gcd_red_int mod_add_self1 add_commute)
 
 lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n"
-by (metis gcd_add1_int gcd_commute_int zadd_commute)
+by (metis gcd_add1_int gcd_commute_int add_commute)
 
 lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n"
 by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat)
 
 lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n"
-by (metis gcd_commute_int gcd_red_int mod_mult_self1 zadd_commute)
+by (metis gcd_commute_int gcd_red_int mod_mult_self1 add_commute)
 
 
 (* to do: differences, and all variations of addition rules
@@ -1030,8 +1030,7 @@
       apply (subst mod_div_equality [of m n, symmetric])
       (* applying simp here undoes the last substitution!
          what is procedure cancel_div_mod? *)
-      apply (simp only: field_simps zadd_int [symmetric]
-        zmult_int [symmetric])
+      apply (simp only: field_simps of_nat_add of_nat_mult)
       done
 qed
 
@@ -1237,7 +1236,7 @@
 
 lemma lcm_altdef_int [code]: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
   by (simp add: lcm_int_def lcm_nat_def zdiv_int
-    zmult_int [symmetric] gcd_int_def)
+    of_nat_mult gcd_int_def)
 
 lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
   unfolding lcm_nat_def
diff -r e0da66339e47 -r a92f65e174cf src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Wed Sep 07 14:58:40 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Wed Sep 07 09:02:58 2011 -0700
@@ -93,7 +93,7 @@
   have even_minus_odd:"\<And>x y. even x \<Longrightarrow> odd (y::int) \<Longrightarrow> odd (x - y)" using assms by auto
   have odd_minus_even:"\<And>x y. odd x \<Longrightarrow> even (y::int) \<Longrightarrow> odd (x - y)" using assms by auto
   show ?thesis unfolding even_nat_def unfolding card_eq_setsum and lem4[THEN sym] and *[unfolded card_eq_setsum]
-    unfolding card_eq_setsum[THEN sym] apply (rule odd_minus_even) unfolding zadd_int[THEN sym] apply(rule odd_plus_even)
+    unfolding card_eq_setsum[THEN sym] apply (rule odd_minus_even) unfolding of_nat_add apply(rule odd_plus_even)
     apply(rule assms(7)[unfolded even_nat_def]) unfolding int_mult by auto qed
 
 subsection {* The odd/even result for faces of complete vertices, generalized. *}
diff -r e0da66339e47 -r a92f65e174cf src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Sep 07 14:58:40 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Sep 07 09:02:58 2011 -0700
@@ -4590,7 +4590,7 @@
   hence "b : affine hull S1" using rel_interior_subset hull_subset[of S2] ** by auto
   hence "b : S1" using T_def b_def by auto
   hence False using b_def assms unfolding rel_frontier_def by auto
-} ultimately show ?thesis using zless_le by auto
+} ultimately show ?thesis using less_le by auto
 qed
 
 
diff -r e0da66339e47 -r a92f65e174cf src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Wed Sep 07 14:58:40 2011 +0200
+++ b/src/HOL/Number_Theory/Primes.thy	Wed Sep 07 09:02:58 2011 -0700
@@ -174,7 +174,7 @@
     EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
   unfolding prime_int_altdef dvd_def
   apply auto
-  by(metis div_mult_self1_is_id div_mult_self2_is_id int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos zless_le)
+  by(metis div_mult_self1_is_id div_mult_self2_is_id int_div_less_self int_one_le_iff_zero_less zero_less_mult_pos less_le)
 
 lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
     n > 0 --> (p dvd x^n --> p dvd x)"
@@ -220,7 +220,7 @@
   "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
 proof
   assume "?L" thus "?R"
-    by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef zless_le)
+    by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef less_le)
 next
     assume "?R" thus "?L" by (clarsimp simp:Ball_def) (metis dvdI not_prime_eq_prod_int)
 qed
@@ -272,7 +272,7 @@
 lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   apply (rule prime_imp_coprime_int, assumption)
   apply (unfold prime_int_altdef)
-  apply (metis int_one_le_iff_zero_less zless_le)
+  apply (metis int_one_le_iff_zero_less less_le)
 done
 
 lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
diff -r e0da66339e47 -r a92f65e174cf src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Sep 07 14:58:40 2011 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Sep 07 09:02:58 2011 -0700
@@ -766,7 +766,7 @@
 lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
     \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
 by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv multiplicity_dvd_int
-          multiplicity_nonprime_int nat_int transfer_nat_int_relations(4) zless_le)
+          multiplicity_nonprime_int nat_int transfer_nat_int_relations(4) less_le)
 
 lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
     (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
diff -r e0da66339e47 -r a92f65e174cf src/HOL/Old_Number_Theory/Fib.thy
--- a/src/HOL/Old_Number_Theory/Fib.thy	Wed Sep 07 14:58:40 2011 +0200
+++ b/src/HOL/Old_Number_Theory/Fib.thy	Wed Sep 07 09:02:58 2011 -0700
@@ -87,7 +87,7 @@
    else fib (Suc n) * fib (Suc n) + 1)"
   apply (rule int_int_eq [THEN iffD1]) 
   apply (simp add: fib_Cassini_int)
-  apply (subst zdiff_int [symmetric]) 
+  apply (subst of_nat_diff)
    apply (insert fib_Suc_gr_0 [of n], simp_all)
   done
 
diff -r e0da66339e47 -r a92f65e174cf src/HOL/Old_Number_Theory/Legacy_GCD.thy
--- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Wed Sep 07 14:58:40 2011 +0200
+++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Wed Sep 07 09:02:58 2011 -0700
@@ -699,7 +699,7 @@
 lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd m n = zgcd (k * m) (k * n)"
   by (simp del: minus_mult_right [symmetric]
       add: minus_mult_right nat_mult_distrib zgcd_def abs_if
-          mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
+          mult_less_0_iff gcd_mult_distrib2 [symmetric] of_nat_mult)
 
 lemma zgcd_zmult_distrib2_abs: "zgcd (k * m) (k * n) = abs k * zgcd m n"
   by (simp add: abs_if zgcd_zmult_distrib2)
diff -r e0da66339e47 -r a92f65e174cf src/HOL/Old_Number_Theory/WilsonRuss.thy
--- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Wed Sep 07 14:58:40 2011 +0200
+++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Wed Sep 07 09:02:58 2011 -0700
@@ -122,7 +122,7 @@
 lemma inv_inv_aux: "5 \<le> p ==>
     nat (p - 2) * nat (p - 2) = Suc (nat (p - 1) * nat (p - 3))"
   apply (subst int_int_eq [symmetric])
-  apply (simp add: zmult_int [symmetric])
+  apply (simp add: of_nat_mult)
   apply (simp add: left_diff_distrib right_diff_distrib)
   done
 
diff -r e0da66339e47 -r a92f65e174cf src/HOL/Word/Misc_Numeric.thy
--- a/src/HOL/Word/Misc_Numeric.thy	Wed Sep 07 14:58:40 2011 +0200
+++ b/src/HOL/Word/Misc_Numeric.thy	Wed Sep 07 09:02:58 2011 -0700
@@ -312,7 +312,7 @@
   apply safe
    apply (simp add: dvd_eq_mod_eq_0 [symmetric])
    apply (drule le_iff_add [THEN iffD1])
-   apply (force simp: zpower_zadd_distrib)
+   apply (force simp: power_add)
   apply (rule mod_pos_pos_trivial)
    apply (simp)
   apply (rule power_strict_increasing)
diff -r e0da66339e47 -r a92f65e174cf src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Sep 07 14:58:40 2011 +0200
+++ b/src/HOL/Word/Word.thy	Wed Sep 07 09:02:58 2011 -0700
@@ -1257,7 +1257,7 @@
         word_of_int_Ex [of b] 
         word_of_int_Ex [of c]
   by (auto simp: word_of_int_hom_syms [symmetric]
-                 zadd_0_right add_commute add_assoc add_left_commute
+                 add_0_right add_commute add_assoc add_left_commute
                  mult_commute mult_assoc mult_left_commute
                  left_distrib right_distrib)
   
@@ -4219,7 +4219,7 @@
   apply (rule rotater_eqs)
   apply (simp add: word_size nat_mod_distrib)
   apply (rule int_eq_0_conv [THEN iffD1])
-  apply (simp only: zmod_int zadd_int [symmetric])
+  apply (simp only: zmod_int of_nat_add)
   apply (simp add: rdmods)
   done