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)"