avoid using legacy theorem names
authorhuffman
Wed Sep 07 09:02:58 2011 -0700 (2011-09-07)
changeset 44821a92f65e174cf
parent 44797 e0da66339e47
child 44822 2690b6de5021
avoid using legacy theorem names
src/HOL/Algebra/IntRing.thy
src/HOL/Algebra/UnivPoly.thy
src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy
src/HOL/Code_Numeral.thy
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/Cooper.thy
src/HOL/GCD.thy
src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy
src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
src/HOL/Number_Theory/Primes.thy
src/HOL/Number_Theory/UniqueFactorization.thy
src/HOL/Old_Number_Theory/Fib.thy
src/HOL/Old_Number_Theory/Legacy_GCD.thy
src/HOL/Old_Number_Theory/WilsonRuss.thy
src/HOL/Word/Misc_Numeric.thy
src/HOL/Word/Word.thy
     1.1 --- a/src/HOL/Algebra/IntRing.thy	Wed Sep 07 14:58:40 2011 +0200
     1.2 +++ b/src/HOL/Algebra/IntRing.thy	Wed Sep 07 09:02:58 2011 -0700
     1.3 @@ -35,8 +35,8 @@
     1.4    apply (rule abelian_groupI, simp_all)
     1.5    defer 1
     1.6    apply (rule comm_monoidI, simp_all)
     1.7 - apply (rule zadd_zmult_distrib)
     1.8 -apply (fast intro: zadd_zminus_inverse2)
     1.9 + apply (rule left_distrib)
    1.10 +apply (fast intro: left_minus)
    1.11  done
    1.12  
    1.13  (*
    1.14 @@ -298,7 +298,7 @@
    1.15    from this obtain x 
    1.16        where "1 = x * p" by best
    1.17    from this [symmetric]
    1.18 -      have "p * x = 1" by (subst zmult_commute)
    1.19 +      have "p * x = 1" by (subst mult_commute)
    1.20    hence "\<bar>p * x\<bar> = 1" by simp
    1.21    hence "\<bar>p\<bar> = 1" by (rule abs_zmult_eq_1)
    1.22    from this and prime
     2.1 --- a/src/HOL/Algebra/UnivPoly.thy	Wed Sep 07 14:58:40 2011 +0200
     2.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Wed Sep 07 09:02:58 2011 -0700
     2.3 @@ -1818,7 +1818,7 @@
     2.4  
     2.5  lemma INTEG_cring: "cring INTEG"
     2.6    by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
     2.7 -    zadd_zminus_inverse2 zadd_zmult_distrib)
     2.8 +    left_minus left_distrib)
     2.9  
    2.10  lemma INTEG_id_eval:
    2.11    "UP_pre_univ_prop INTEG INTEG id"
     3.1 --- a/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy	Wed Sep 07 14:58:40 2011 +0200
     3.2 +++ b/src/HOL/Boogie/Examples/Boogie_Max_Stepwise.thy	Wed Sep 07 09:02:58 2011 -0700
     3.3 @@ -77,10 +77,10 @@
     3.4  boogie_vc max (examine: L_14_5c L_14_5b L_14_5a) 
     3.5  proof boogie_cases
     3.6    case L_14_5c
     3.7 -  thus ?case by (metis less_le_not_le zle_add1_eq_le zless_linear)
     3.8 +  thus ?case by (metis less_le_not_le zle_add1_eq_le less_linear)
     3.9  next
    3.10    case L_14_5b
    3.11 -  thus ?case by (metis less_le_not_le xt1(10) zle_linear zless_add1_eq)
    3.12 +  thus ?case by (metis less_le_not_le xt1(10) linorder_linear zless_add1_eq)
    3.13  next
    3.14    case L_14_5a
    3.15    note max0 = `max0 = array 0`
     4.1 --- a/src/HOL/Code_Numeral.thy	Wed Sep 07 14:58:40 2011 +0200
     4.2 +++ b/src/HOL/Code_Numeral.thy	Wed Sep 07 09:02:58 2011 -0700
     4.3 @@ -274,7 +274,7 @@
     4.4    then have "int ((nat_of k div 2) * 2 + nat_of k mod 2) = int (nat_of k)" 
     4.5      by simp
     4.6    then have "int (nat_of k) = int (nat_of k div 2) * 2 + int (nat_of k mod 2)" 
     4.7 -    unfolding int_mult zadd_int [symmetric] by simp
     4.8 +    unfolding of_nat_mult of_nat_add by simp
     4.9    then show ?thesis by (auto simp add: int_of_def mult_ac)
    4.10  qed
    4.11  
     5.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Wed Sep 07 14:58:40 2011 +0200
     5.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Sep 07 09:02:58 2011 -0700
     5.3 @@ -295,7 +295,7 @@
     5.4          unfolding real_sqrt_mult[of _ "pow2 (?E mod 2)"] real_sqrt_abs2 by auto
     5.5        also have "\<dots> < pow2 (?E div 2) * 2"
     5.6          by (rule mult_strict_left_mono, auto intro: E_mod_pow)
     5.7 -      also have "\<dots> = pow2 (?E div 2 + 1)" unfolding zadd_commute[of _ 1] pow2_add1 by auto
     5.8 +      also have "\<dots> = pow2 (?E div 2 + 1)" unfolding add_commute[of _ 1] pow2_add1 by auto
     5.9        finally show ?thesis by auto
    5.10      qed
    5.11      finally show ?thesis
     6.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Wed Sep 07 14:58:40 2011 +0200
     6.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Sep 07 09:02:58 2011 -0700
     6.3 @@ -1318,7 +1318,7 @@
     6.4      also have "\<dots> = (j dvd (- (c*x - ?e)))"
     6.5      by (simp only: dvd_minus_iff)
     6.6    also have "\<dots> = (j dvd (c* (- x)) + ?e)"
     6.7 -    apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus zadd_ac zminus_zadd_distrib)
     6.8 +    apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus add_ac minus_add_distrib)
     6.9      by (simp add: algebra_simps)
    6.10    also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
    6.11      using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
    6.12 @@ -1330,7 +1330,7 @@
    6.13      also have "\<dots> = (j dvd (- (c*x - ?e)))"
    6.14      by (simp only: dvd_minus_iff)
    6.15    also have "\<dots> = (j dvd (c* (- x)) + ?e)"
    6.16 -    apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus zadd_ac zminus_zadd_distrib)
    6.17 +    apply (simp only: minus_mult_right[symmetric] minus_mult_left[symmetric] diff_minus add_ac minus_add_distrib)
    6.18      by (simp add: algebra_simps)
    6.19    also have "\<dots> = Ifm bbs ((- x)#bs) (Dvd j (CN 0 c e))"
    6.20      using numbound0_I[OF nb, where bs="bs" and b="x" and b'="- x"]
     7.1 --- a/src/HOL/GCD.thy	Wed Sep 07 14:58:40 2011 +0200
     7.2 +++ b/src/HOL/GCD.thy	Wed Sep 07 09:02:58 2011 -0700
     7.3 @@ -485,16 +485,16 @@
     7.4  done
     7.5  
     7.6  lemma gcd_add1_int [simp]: "gcd ((m::int) + n) n = gcd m n"
     7.7 -by (metis gcd_red_int mod_add_self1 zadd_commute)
     7.8 +by (metis gcd_red_int mod_add_self1 add_commute)
     7.9  
    7.10  lemma gcd_add2_int [simp]: "gcd m ((m::int) + n) = gcd m n"
    7.11 -by (metis gcd_add1_int gcd_commute_int zadd_commute)
    7.12 +by (metis gcd_add1_int gcd_commute_int add_commute)
    7.13  
    7.14  lemma gcd_add_mult_nat: "gcd (m::nat) (k * m + n) = gcd m n"
    7.15  by (metis mod_mult_self3 gcd_commute_nat gcd_red_nat)
    7.16  
    7.17  lemma gcd_add_mult_int: "gcd (m::int) (k * m + n) = gcd m n"
    7.18 -by (metis gcd_commute_int gcd_red_int mod_mult_self1 zadd_commute)
    7.19 +by (metis gcd_commute_int gcd_red_int mod_mult_self1 add_commute)
    7.20  
    7.21  
    7.22  (* to do: differences, and all variations of addition rules
    7.23 @@ -1030,8 +1030,7 @@
    7.24        apply (subst mod_div_equality [of m n, symmetric])
    7.25        (* applying simp here undoes the last substitution!
    7.26           what is procedure cancel_div_mod? *)
    7.27 -      apply (simp only: field_simps zadd_int [symmetric]
    7.28 -        zmult_int [symmetric])
    7.29 +      apply (simp only: field_simps of_nat_add of_nat_mult)
    7.30        done
    7.31  qed
    7.32  
    7.33 @@ -1237,7 +1236,7 @@
    7.34  
    7.35  lemma lcm_altdef_int [code]: "lcm (a::int) b = (abs a) * (abs b) div gcd a b"
    7.36    by (simp add: lcm_int_def lcm_nat_def zdiv_int
    7.37 -    zmult_int [symmetric] gcd_int_def)
    7.38 +    of_nat_mult gcd_int_def)
    7.39  
    7.40  lemma prod_gcd_lcm_nat: "(m::nat) * n = gcd m n * lcm m n"
    7.41    unfolding lcm_nat_def
     8.1 --- a/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Wed Sep 07 14:58:40 2011 +0200
     8.2 +++ b/src/HOL/Multivariate_Analysis/Brouwer_Fixpoint.thy	Wed Sep 07 09:02:58 2011 -0700
     8.3 @@ -93,7 +93,7 @@
     8.4    have even_minus_odd:"\<And>x y. even x \<Longrightarrow> odd (y::int) \<Longrightarrow> odd (x - y)" using assms by auto
     8.5    have odd_minus_even:"\<And>x y. odd x \<Longrightarrow> even (y::int) \<Longrightarrow> odd (x - y)" using assms by auto
     8.6    show ?thesis unfolding even_nat_def unfolding card_eq_setsum and lem4[THEN sym] and *[unfolded card_eq_setsum]
     8.7 -    unfolding card_eq_setsum[THEN sym] apply (rule odd_minus_even) unfolding zadd_int[THEN sym] apply(rule odd_plus_even)
     8.8 +    unfolding card_eq_setsum[THEN sym] apply (rule odd_minus_even) unfolding of_nat_add apply(rule odd_plus_even)
     8.9      apply(rule assms(7)[unfolded even_nat_def]) unfolding int_mult by auto qed
    8.10  
    8.11  subsection {* The odd/even result for faces of complete vertices, generalized. *}
     9.1 --- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Sep 07 14:58:40 2011 +0200
     9.2 +++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Sep 07 09:02:58 2011 -0700
     9.3 @@ -4590,7 +4590,7 @@
     9.4    hence "b : affine hull S1" using rel_interior_subset hull_subset[of S2] ** by auto
     9.5    hence "b : S1" using T_def b_def by auto
     9.6    hence False using b_def assms unfolding rel_frontier_def by auto
     9.7 -} ultimately show ?thesis using zless_le by auto
     9.8 +} ultimately show ?thesis using less_le by auto
     9.9  qed
    9.10  
    9.11  
    10.1 --- a/src/HOL/Number_Theory/Primes.thy	Wed Sep 07 14:58:40 2011 +0200
    10.2 +++ b/src/HOL/Number_Theory/Primes.thy	Wed Sep 07 09:02:58 2011 -0700
    10.3 @@ -174,7 +174,7 @@
    10.4      EX m k. n = m * k & 1 < m & m < n & 1 < k & k < n"
    10.5    unfolding prime_int_altdef dvd_def
    10.6    apply auto
    10.7 -  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)
    10.8 +  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)
    10.9  
   10.10  lemma prime_dvd_power_nat [rule_format]: "prime (p::nat) -->
   10.11      n > 0 --> (p dvd x^n --> p dvd x)"
   10.12 @@ -220,7 +220,7 @@
   10.13    "prime (p::int) \<longleftrightarrow> p > 1 \<and> (\<forall>n \<in> {1<..<p}. ~ n dvd p)" (is "?L = ?R")
   10.14  proof
   10.15    assume "?L" thus "?R"
   10.16 -    by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef zless_le)
   10.17 +    by (clarsimp simp: prime_gt_1_int) (metis int_one_le_iff_zero_less prime_int_altdef less_le)
   10.18  next
   10.19      assume "?R" thus "?L" by (clarsimp simp:Ball_def) (metis dvdI not_prime_eq_prod_int)
   10.20  qed
   10.21 @@ -272,7 +272,7 @@
   10.22  lemma primes_coprime_int: "prime (p::int) \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   10.23    apply (rule prime_imp_coprime_int, assumption)
   10.24    apply (unfold prime_int_altdef)
   10.25 -  apply (metis int_one_le_iff_zero_less zless_le)
   10.26 +  apply (metis int_one_le_iff_zero_less less_le)
   10.27  done
   10.28  
   10.29  lemma primes_imp_powers_coprime_nat: "prime (p::nat) \<Longrightarrow> prime q \<Longrightarrow> p ~= q \<Longrightarrow> coprime (p^m) (q^n)"
    11.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Sep 07 14:58:40 2011 +0200
    11.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Sep 07 09:02:58 2011 -0700
    11.3 @@ -766,7 +766,7 @@
    11.4  lemma multiplicity_dvd'_int: "(0::int) < x \<Longrightarrow> 0 <= y \<Longrightarrow>
    11.5      \<forall>p. prime p \<longrightarrow> multiplicity p x \<le> multiplicity p y \<Longrightarrow> x dvd y"
    11.6  by (metis eq_imp_le gcd_lcm_complete_lattice_nat.top_greatest int_eq_0_conv multiplicity_dvd_int
    11.7 -          multiplicity_nonprime_int nat_int transfer_nat_int_relations(4) zless_le)
    11.8 +          multiplicity_nonprime_int nat_int transfer_nat_int_relations(4) less_le)
    11.9  
   11.10  lemma dvd_multiplicity_eq_nat: "0 < (x::nat) \<Longrightarrow> 0 < y \<Longrightarrow>
   11.11      (x dvd y) = (ALL p. multiplicity p x <= multiplicity p y)"
    12.1 --- a/src/HOL/Old_Number_Theory/Fib.thy	Wed Sep 07 14:58:40 2011 +0200
    12.2 +++ b/src/HOL/Old_Number_Theory/Fib.thy	Wed Sep 07 09:02:58 2011 -0700
    12.3 @@ -87,7 +87,7 @@
    12.4     else fib (Suc n) * fib (Suc n) + 1)"
    12.5    apply (rule int_int_eq [THEN iffD1]) 
    12.6    apply (simp add: fib_Cassini_int)
    12.7 -  apply (subst zdiff_int [symmetric]) 
    12.8 +  apply (subst of_nat_diff)
    12.9     apply (insert fib_Suc_gr_0 [of n], simp_all)
   12.10    done
   12.11  
    13.1 --- a/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Wed Sep 07 14:58:40 2011 +0200
    13.2 +++ b/src/HOL/Old_Number_Theory/Legacy_GCD.thy	Wed Sep 07 09:02:58 2011 -0700
    13.3 @@ -699,7 +699,7 @@
    13.4  lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd m n = zgcd (k * m) (k * n)"
    13.5    by (simp del: minus_mult_right [symmetric]
    13.6        add: minus_mult_right nat_mult_distrib zgcd_def abs_if
    13.7 -          mult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric])
    13.8 +          mult_less_0_iff gcd_mult_distrib2 [symmetric] of_nat_mult)
    13.9  
   13.10  lemma zgcd_zmult_distrib2_abs: "zgcd (k * m) (k * n) = abs k * zgcd m n"
   13.11    by (simp add: abs_if zgcd_zmult_distrib2)
    14.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Wed Sep 07 14:58:40 2011 +0200
    14.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Wed Sep 07 09:02:58 2011 -0700
    14.3 @@ -122,7 +122,7 @@
    14.4  lemma inv_inv_aux: "5 \<le> p ==>
    14.5      nat (p - 2) * nat (p - 2) = Suc (nat (p - 1) * nat (p - 3))"
    14.6    apply (subst int_int_eq [symmetric])
    14.7 -  apply (simp add: zmult_int [symmetric])
    14.8 +  apply (simp add: of_nat_mult)
    14.9    apply (simp add: left_diff_distrib right_diff_distrib)
   14.10    done
   14.11  
    15.1 --- a/src/HOL/Word/Misc_Numeric.thy	Wed Sep 07 14:58:40 2011 +0200
    15.2 +++ b/src/HOL/Word/Misc_Numeric.thy	Wed Sep 07 09:02:58 2011 -0700
    15.3 @@ -312,7 +312,7 @@
    15.4    apply safe
    15.5     apply (simp add: dvd_eq_mod_eq_0 [symmetric])
    15.6     apply (drule le_iff_add [THEN iffD1])
    15.7 -   apply (force simp: zpower_zadd_distrib)
    15.8 +   apply (force simp: power_add)
    15.9    apply (rule mod_pos_pos_trivial)
   15.10     apply (simp)
   15.11    apply (rule power_strict_increasing)
    16.1 --- a/src/HOL/Word/Word.thy	Wed Sep 07 14:58:40 2011 +0200
    16.2 +++ b/src/HOL/Word/Word.thy	Wed Sep 07 09:02:58 2011 -0700
    16.3 @@ -1257,7 +1257,7 @@
    16.4          word_of_int_Ex [of b] 
    16.5          word_of_int_Ex [of c]
    16.6    by (auto simp: word_of_int_hom_syms [symmetric]
    16.7 -                 zadd_0_right add_commute add_assoc add_left_commute
    16.8 +                 add_0_right add_commute add_assoc add_left_commute
    16.9                   mult_commute mult_assoc mult_left_commute
   16.10                   left_distrib right_distrib)
   16.11    
   16.12 @@ -4219,7 +4219,7 @@
   16.13    apply (rule rotater_eqs)
   16.14    apply (simp add: word_size nat_mod_distrib)
   16.15    apply (rule int_eq_0_conv [THEN iffD1])
   16.16 -  apply (simp only: zmod_int zadd_int [symmetric])
   16.17 +  apply (simp only: zmod_int of_nat_add)
   16.18    apply (simp add: rdmods)
   16.19    done
   16.20