src/HOL/Library/Pocklington.thy
changeset 30224 79136ce06bdb
parent 30042 31039ee583fa
child 30242 aea5d7fa7ef5
     1.1 --- a/src/HOL/Library/Pocklington.thy	Tue Mar 03 12:14:52 2009 +1100
     1.2 +++ b/src/HOL/Library/Pocklington.thy	Tue Mar 03 17:05:18 2009 +0100
     1.3 @@ -142,10 +142,10 @@
     1.4    shows "[x * y = x' * y'] (mod n)"
     1.5  proof-
     1.6    have "(x * y) mod n = (x mod n) * (y mod n) mod n"  
     1.7 -    by (simp add: mod_mult1_eq'[of x y n] mod_mult1_eq[of "x mod n" y n])
     1.8 +    by (simp add: mod_mult_left_eq[of x y n] mod_mult_right_eq[of "x mod n" y n])
     1.9    also have "\<dots> = (x' mod n) * (y' mod n) mod n" using xx'[unfolded modeq_def] yy'[unfolded modeq_def] by simp  
    1.10    also have "\<dots> = (x' * y') mod n"
    1.11 -    by (simp add: mod_mult1_eq'[of x' y' n] mod_mult1_eq[of "x' mod n" y' n])
    1.12 +    by (simp add: mod_mult_left_eq[of x' y' n] mod_mult_right_eq[of "x' mod n" y' n])
    1.13    finally show ?thesis unfolding modeq_def . 
    1.14  qed
    1.15  
    1.16 @@ -296,7 +296,7 @@
    1.17    from cong_solve[OF an] obtain x where x: "[a*x = b] (mod n)" by blast
    1.18    let ?x = "x mod n"
    1.19    from x have th: "[a * ?x = b] (mod n)"
    1.20 -    by (simp add: modeq_def mod_mult1_eq[of a x n])
    1.21 +    by (simp add: modeq_def mod_mult_right_eq[of a x n])
    1.22    from mod_less_divisor[ of n x] nz th have Px: "?P ?x" by simp
    1.23    {fix y assume Py: "y < n" "[a * y = b] (mod n)"
    1.24      from Py(2) th have "[a * y = a*?x] (mod n)" by (simp add: modeq_def)
    1.25 @@ -753,10 +753,10 @@
    1.26  next
    1.27    case (Suc n) 
    1.28    have "(x mod m)^(Suc n) mod m = ((x mod m) * (((x mod m) ^ n) mod m)) mod m" 
    1.29 -    by (simp add: mod_mult1_eq[symmetric])
    1.30 +    by (simp add: mod_mult_right_eq[symmetric])
    1.31    also have "\<dots> = ((x mod m) * (x^n mod m)) mod m" using Suc.hyps by simp
    1.32    also have "\<dots> = x^(Suc n) mod m"
    1.33 -    by (simp add: mod_mult1_eq'[symmetric] mod_mult1_eq[symmetric])
    1.34 +    by (simp add: mod_mult_left_eq[symmetric] mod_mult_right_eq[symmetric])
    1.35    finally show ?case .
    1.36  qed
    1.37  
    1.38 @@ -891,9 +891,9 @@
    1.39      hence "[(a^?o)^?q * (a^?r) = 1] (mod n)" 
    1.40        by (simp add: modeq_def power_mult[symmetric] power_add[symmetric])
    1.41      hence th: "[a^?r = 1] (mod n)"
    1.42 -      using eqo mod_mult1_eq'[of "(a^?o)^?q" "a^?r" n]
    1.43 +      using eqo mod_mult_left_eq[of "(a^?o)^?q" "a^?r" n]
    1.44        apply (simp add: modeq_def del: One_nat_def)
    1.45 -      by (simp add: mod_mult1_eq'[symmetric])
    1.46 +      by (simp add: mod_mult_left_eq[symmetric])
    1.47      {assume r: "?r = 0" hence ?rhs by (simp add: dvd_eq_mod_eq_0)}
    1.48      moreover
    1.49      {assume r: "?r \<noteq> 0"