author  paulson 
Mon, 22 Oct 2001 11:54:22 +0200  
changeset 11868  56db9f3a6b3e 
parent 11701  3d51fbf81c17 
child 13183  c7290200b3f4 
permissions  rwrr 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

1 
(* Title: HOL/NumberTheory/IntPrimes.thy 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

2 
ID: $Id$ 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

3 
Author: Thomas M. Rasmussen 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

4 
Copyright 2000 University of Cambridge 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

5 
*) 
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

6 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

7 
header {* Divisibility and prime numbers (on integers) *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

8 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

9 
theory IntPrimes = Primes: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

10 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

11 
text {* 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

12 
The @{text dvd} relation, GCD, Euclid's extended algorithm, primes, 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

13 
congruences (all on the Integers). Comparable to theory @{text 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

14 
Primes}, but @{text dvd} is included here as it is not present in 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

15 
main HOL. Also includes extended GCD and congruences not present in 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

16 
@{text Primes}. 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

17 
*} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

18 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

19 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

20 
subsection {* Definitions *} 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

21 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

22 
consts 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

23 
xzgcda :: "int * int * int * int * int * int * int * int => int * int * int" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

24 
xzgcd :: "int => int => int * int * int" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

25 
zprime :: "int set" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

26 
zcong :: "int => int => int => bool" ("(1[_ = _] '(mod _'))") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

27 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

28 
recdef xzgcda 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

29 
"measure ((\<lambda>(m, n, r', r, s', s, t', t). nat r) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

30 
:: int * int * int * int *int * int * int * int => nat)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

31 
"xzgcda (m, n, r', r, s', s, t', t) = 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

32 
(if r \<le> 0 then (r', s', t') 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

33 
else xzgcda (m, n, r, r' mod r, s, s'  (r' div r) * s, t, t'  (r' div r) * t))" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

34 
(hints simp: pos_mod_bound) 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

35 

9943  36 
constdefs 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

37 
zgcd :: "int * int => int" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

38 
"zgcd == \<lambda>(x,y). int (gcd (nat (abs x), nat (abs y)))" 
9943  39 

9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

40 
defs 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

41 
xzgcd_def: "xzgcd m n == xzgcda (m, n, m, n, 1, 0, 0, 1)" 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

42 
zprime_def: "zprime == {p. 1 < p \<and> (\<forall>m. m dvd p > m = 1 \<or> m = p)}" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

43 
zcong_def: "[a = b] (mod m) == m dvd (a  b)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

44 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

45 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

46 
lemma zabs_eq_iff: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

47 
"(abs (z::int) = w) = (z = w \<and> 0 <= z \<or> z = w \<and> z < 0)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

48 
apply (auto simp add: zabs_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

49 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

50 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

51 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

52 
text {* \medskip @{term gcd} lemmas *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

53 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

54 
lemma gcd_add1_eq: "gcd (m + k, k) = gcd (m + k, m)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

55 
apply (simp add: gcd_commute) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

56 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

57 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

58 
lemma gcd_diff2: "m \<le> n ==> gcd (n, n  m) = gcd (n, m)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

59 
apply (subgoal_tac "n = m + (n  m)") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

60 
apply (erule ssubst, rule gcd_add1_eq) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

61 
apply simp 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

62 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

63 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

64 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

65 
subsection {* Divides relation *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

66 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

67 
lemma zdvd_0_right [iff]: "(m::int) dvd 0" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

68 
apply (unfold dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

69 
apply (blast intro: zmult_0_right [symmetric]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

70 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

71 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

72 
lemma zdvd_0_left [iff]: "(0 dvd (m::int)) = (m = 0)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

73 
apply (unfold dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

74 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

75 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

76 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

77 
lemma zdvd_1_left [iff]: "1 dvd (m::int)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

78 
apply (unfold dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

79 
apply simp 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

80 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

81 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

82 
lemma zdvd_refl [simp]: "m dvd (m::int)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

83 
apply (unfold dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

84 
apply (blast intro: zmult_1_right [symmetric]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

85 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

86 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

87 
lemma zdvd_trans: "m dvd n ==> n dvd k ==> m dvd (k::int)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

88 
apply (unfold dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

89 
apply (blast intro: zmult_assoc) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

90 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

91 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

92 
lemma zdvd_zminus_iff: "(m dvd n) = (m dvd (n::int))" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

93 
apply (unfold dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

94 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

95 
apply (rule_tac [!] x = "k" in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

96 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

97 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

98 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

99 
lemma zdvd_zminus2_iff: "(m dvd n) = (m dvd (n::int))" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

100 
apply (unfold dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

101 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

102 
apply (rule_tac [!] x = "k" in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

103 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

104 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

105 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

106 
lemma zdvd_anti_sym: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

107 
"0 < m ==> 0 < n ==> m dvd n ==> n dvd m ==> m = (n::int)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

108 
apply (unfold dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

109 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

110 
apply (simp add: zmult_assoc zmult_eq_self_iff int_0_less_mult_iff zmult_eq_1_iff) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

111 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

112 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

113 
lemma zdvd_zadd: "k dvd m ==> k dvd n ==> k dvd (m + n :: int)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

114 
apply (unfold dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

115 
apply (blast intro: zadd_zmult_distrib2 [symmetric]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

116 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

117 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

118 
lemma zdvd_zdiff: "k dvd m ==> k dvd n ==> k dvd (m  n :: int)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

119 
apply (unfold dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

120 
apply (blast intro: zdiff_zmult_distrib2 [symmetric]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

121 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

122 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

123 
lemma zdvd_zdiffD: "k dvd m  n ==> k dvd n ==> k dvd (m::int)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

124 
apply (subgoal_tac "m = n + (m  n)") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

125 
apply (erule ssubst) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

126 
apply (blast intro: zdvd_zadd) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

127 
apply simp 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

128 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

129 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

130 
lemma zdvd_zmult: "k dvd (n::int) ==> k dvd m * n" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

131 
apply (unfold dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

132 
apply (blast intro: zmult_left_commute) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

133 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

134 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

135 
lemma zdvd_zmult2: "k dvd (m::int) ==> k dvd m * n" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

136 
apply (subst zmult_commute) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

137 
apply (erule zdvd_zmult) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

138 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

139 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

140 
lemma [iff]: "(k::int) dvd m * k" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

141 
apply (rule zdvd_zmult) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

142 
apply (rule zdvd_refl) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

143 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

144 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

145 
lemma [iff]: "(k::int) dvd k * m" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

146 
apply (rule zdvd_zmult2) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

147 
apply (rule zdvd_refl) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

148 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

149 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

150 
lemma zdvd_zmultD2: "j * k dvd n ==> j dvd (n::int)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

151 
apply (unfold dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

152 
apply (simp add: zmult_assoc) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

153 
apply blast 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

154 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

155 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

156 
lemma zdvd_zmultD: "j * k dvd n ==> k dvd (n::int)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

157 
apply (rule zdvd_zmultD2) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

158 
apply (subst zmult_commute) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

159 
apply assumption 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

160 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

161 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

162 
lemma zdvd_zmult_mono: "i dvd m ==> j dvd (n::int) ==> i * j dvd m * n" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

163 
apply (unfold dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

164 
apply clarify 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

165 
apply (rule_tac x = "k * ka" in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

166 
apply (simp add: zmult_ac) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

167 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

168 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

169 
lemma zdvd_reduce: "(k dvd n + k * m) = (k dvd (n::int))" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

170 
apply (rule iffI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

171 
apply (erule_tac [2] zdvd_zadd) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

172 
apply (subgoal_tac "n = (n + k * m)  k * m") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

173 
apply (erule ssubst) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

174 
apply (erule zdvd_zdiff) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

175 
apply simp_all 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

176 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

177 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

178 
lemma zdvd_zmod: "f dvd m ==> f dvd (n::int) ==> f dvd m mod n" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

179 
apply (unfold dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

180 
apply (auto simp add: zmod_zmult_zmult1) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

181 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

182 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

183 
lemma zdvd_zmod_imp_zdvd: "k dvd m mod n ==> k dvd n ==> k dvd (m::int)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

184 
apply (subgoal_tac "k dvd n * (m div n) + m mod n") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

185 
apply (simp add: zmod_zdiv_equality [symmetric]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

186 
apply (simp add: zdvd_zadd zdvd_zmult2) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

187 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

188 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

189 
lemma zdvd_iff_zmod_eq_0: "(k dvd n) = (n mod (k::int) = 0)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

190 
apply (unfold dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

191 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

192 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

193 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

194 
lemma zdvd_not_zless: "0 < m ==> m < n ==> \<not> n dvd (m::int)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

195 
apply (unfold dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

196 
apply auto 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

197 
apply (subgoal_tac "0 < n") 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

198 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

199 
apply (blast intro: zless_trans) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

200 
apply (simp add: int_0_less_mult_iff) 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

201 
apply (subgoal_tac "n * k < n * 1") 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

202 
apply (drule zmult_zless_cancel1 [THEN iffD1]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

203 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

204 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

205 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

206 
lemma int_dvd_iff: "(int m dvd z) = (m dvd nat (abs z))" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

207 
apply (auto simp add: dvd_def nat_abs_mult_distrib) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

208 
apply (auto simp add: nat_eq_iff zabs_eq_iff) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

209 
apply (rule_tac [2] x = "(int k)" in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

210 
apply (auto simp add: zmult_int [symmetric]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

211 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

212 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

213 
lemma dvd_int_iff: "(z dvd int m) = (nat (abs z) dvd m)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

214 
apply (auto simp add: dvd_def zabs_def zmult_int [symmetric]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

215 
apply (rule_tac [3] x = "nat k" in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

216 
apply (rule_tac [2] x = "(int k)" in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

217 
apply (rule_tac x = "nat (k)" in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

218 
apply (cut_tac [3] k = m in int_less_0_conv) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

219 
apply (cut_tac k = m in int_less_0_conv) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

220 
apply (auto simp add: int_0_le_mult_iff zmult_less_0_iff 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

221 
nat_mult_distrib [symmetric] nat_eq_iff2) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

222 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

223 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

224 
lemma nat_dvd_iff: "(nat z dvd m) = (if 0 \<le> z then (z dvd int m) else m = 0)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

225 
apply (auto simp add: dvd_def zmult_int [symmetric]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

226 
apply (rule_tac x = "nat k" in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

227 
apply (cut_tac k = m in int_less_0_conv) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

228 
apply (auto simp add: int_0_le_mult_iff zmult_less_0_iff 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

229 
nat_mult_distrib [symmetric] nat_eq_iff2) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

230 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

231 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

232 
lemma zminus_dvd_iff [iff]: "(z dvd w) = (z dvd (w::int))" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

233 
apply (auto simp add: dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

234 
apply (rule_tac [!] x = "k" in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

235 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

236 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

237 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

238 
lemma dvd_zminus_iff [iff]: "(z dvd w) = (z dvd (w::int))" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

239 
apply (auto simp add: dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

240 
apply (drule zminus_equation [THEN iffD1]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

241 
apply (rule_tac [!] x = "k" in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

242 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

243 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

244 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

245 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

246 
subsection {* Euclid's Algorithm and GCD *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

247 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

248 
lemma zgcd_0 [simp]: "zgcd (m, 0) = abs m" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

249 
apply (simp add: zgcd_def zabs_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

250 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

251 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

252 
lemma zgcd_0_left [simp]: "zgcd (0, m) = abs m" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

253 
apply (simp add: zgcd_def zabs_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

254 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

255 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

256 
lemma zgcd_zminus [simp]: "zgcd (m, n) = zgcd (m, n)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

257 
apply (simp add: zgcd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

258 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

259 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

260 
lemma zgcd_zminus2 [simp]: "zgcd (m, n) = zgcd (m, n)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

261 
apply (simp add: zgcd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

262 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

263 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

264 
lemma zgcd_non_0: "0 < n ==> zgcd (m, n) = zgcd (n, m mod n)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

265 
apply (frule_tac b = n and a = m in pos_mod_sign) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

266 
apply (simp add: zgcd_def zabs_def nat_mod_distrib) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

267 
apply (cut_tac a = "m" and b = n in zmod_zminus1_eq_if) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

268 
apply (auto simp add: gcd_non_0 nat_mod_distrib [symmetric] zmod_zminus1_eq_if) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

269 
apply (frule_tac a = m in pos_mod_bound) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

270 
apply (simp add: nat_diff_distrib) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

271 
apply (rule gcd_diff2) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

272 
apply (simp add: nat_le_eq_zle) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

273 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

274 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

275 
lemma zgcd_eq: "zgcd (m, n) = zgcd (n, m mod n)" 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

276 
apply (tactic {* zdiv_undefined_case_tac "n = 0" 1 *}) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

277 
apply (auto simp add: linorder_neq_iff zgcd_non_0) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

278 
apply (cut_tac m = "m" and n = "n" in zgcd_non_0) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

279 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

280 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

281 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

282 
lemma zgcd_1 [simp]: "zgcd (m, 1) = 1" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

283 
apply (simp add: zgcd_def zabs_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

284 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

285 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

286 
lemma zgcd_0_1_iff [simp]: "(zgcd (0, m) = 1) = (abs m = 1)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

287 
apply (simp add: zgcd_def zabs_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

288 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

289 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

290 
lemma zgcd_zdvd1 [iff]: "zgcd (m, n) dvd m" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

291 
apply (simp add: zgcd_def zabs_def int_dvd_iff) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

292 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

293 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

294 
lemma zgcd_zdvd2 [iff]: "zgcd (m, n) dvd n" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

295 
apply (simp add: zgcd_def zabs_def int_dvd_iff) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

296 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

297 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

298 
lemma zgcd_greatest_iff: "k dvd zgcd (m, n) = (k dvd m \<and> k dvd n)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

299 
apply (simp add: zgcd_def zabs_def int_dvd_iff dvd_int_iff nat_dvd_iff) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

300 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

301 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

302 
lemma zgcd_commute: "zgcd (m, n) = zgcd (n, m)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

303 
apply (simp add: zgcd_def gcd_commute) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

304 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

305 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

306 
lemma zgcd_1_left [simp]: "zgcd (1, m) = 1" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

307 
apply (simp add: zgcd_def gcd_1_left) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

308 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

309 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

310 
lemma zgcd_assoc: "zgcd (zgcd (k, m), n) = zgcd (k, zgcd (m, n))" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

311 
apply (simp add: zgcd_def gcd_assoc) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

312 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

313 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

314 
lemma zgcd_left_commute: "zgcd (k, zgcd (m, n)) = zgcd (m, zgcd (k, n))" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

315 
apply (rule zgcd_commute [THEN trans]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

316 
apply (rule zgcd_assoc [THEN trans]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

317 
apply (rule zgcd_commute [THEN arg_cong]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

318 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

319 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

320 
lemmas zgcd_ac = zgcd_assoc zgcd_commute zgcd_left_commute 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

321 
 {* addition is an ACoperator *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

322 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

323 
lemma zgcd_zmult_distrib2: "0 \<le> k ==> k * zgcd (m, n) = zgcd (k * m, k * n)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

324 
apply (simp del: zmult_zminus_right 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

325 
add: zmult_zminus_right [symmetric] nat_mult_distrib zgcd_def zabs_def 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

326 
zmult_less_0_iff gcd_mult_distrib2 [symmetric] zmult_int [symmetric]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

327 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

328 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

329 
lemma zgcd_zmult_distrib2_abs: "zgcd (k * m, k * n) = abs k * zgcd (m, n)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

330 
apply (simp add: zabs_def zgcd_zmult_distrib2) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

331 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

332 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

333 
lemma zgcd_self [simp]: "0 \<le> m ==> zgcd (m, m) = m" 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

334 
apply (cut_tac k = m and m = "1" and n = "1" in zgcd_zmult_distrib2) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

335 
apply simp_all 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

336 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

337 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

338 
lemma zgcd_zmult_eq_self [simp]: "0 \<le> k ==> zgcd (k, k * n) = k" 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

339 
apply (cut_tac k = k and m = "1" and n = n in zgcd_zmult_distrib2) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

340 
apply simp_all 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

341 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

342 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

343 
lemma zgcd_zmult_eq_self2 [simp]: "0 \<le> k ==> zgcd (k * n, k) = k" 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

344 
apply (cut_tac k = k and m = n and n = "1" in zgcd_zmult_distrib2) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

345 
apply simp_all 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

346 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

347 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

348 
lemma aux: "zgcd (n, k) = 1 ==> k dvd m * n ==> 0 \<le> m ==> k dvd m" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

349 
apply (subgoal_tac "m = zgcd (m * n, m * k)") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

350 
apply (erule ssubst, rule zgcd_greatest_iff [THEN iffD2]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

351 
apply (simp_all add: zgcd_zmult_distrib2 [symmetric] int_0_le_mult_iff) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

352 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

353 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

354 
lemma zrelprime_zdvd_zmult: "zgcd (n, k) = 1 ==> k dvd m * n ==> k dvd m" 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

355 
apply (case_tac "0 \<le> m") 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

356 
apply (blast intro: aux) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

357 
apply (subgoal_tac "k dvd m") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

358 
apply (rule_tac [2] aux) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

359 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

360 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

361 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

362 
lemma zprime_imp_zrelprime: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

363 
"p \<in> zprime ==> \<not> p dvd n ==> zgcd (n, p) = 1" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

364 
apply (unfold zprime_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

365 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

366 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

367 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

368 
lemma zless_zprime_imp_zrelprime: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

369 
"p \<in> zprime ==> 0 < n ==> n < p ==> zgcd (n, p) = 1" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

370 
apply (erule zprime_imp_zrelprime) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

371 
apply (erule zdvd_not_zless) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

372 
apply assumption 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

373 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

374 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

375 
lemma zprime_zdvd_zmult: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

376 
"0 \<le> (m::int) ==> p \<in> zprime ==> p dvd m * n ==> p dvd m \<or> p dvd n" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

377 
apply safe 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

378 
apply (rule zrelprime_zdvd_zmult) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

379 
apply (rule zprime_imp_zrelprime) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

380 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

381 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

382 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

383 
lemma zgcd_zadd_zmult [simp]: "zgcd (m + n * k, n) = zgcd (m, n)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

384 
apply (rule zgcd_eq [THEN trans]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

385 
apply (simp add: zmod_zadd1_eq) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

386 
apply (rule zgcd_eq [symmetric]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

387 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

388 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

389 
lemma zgcd_zdvd_zgcd_zmult: "zgcd (m, n) dvd zgcd (k * m, n)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

390 
apply (simp add: zgcd_greatest_iff) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

391 
apply (blast intro: zdvd_trans) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

392 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

393 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

394 
lemma zgcd_zmult_zdvd_zgcd: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

395 
"zgcd (k, n) = 1 ==> zgcd (k * m, n) dvd zgcd (m, n)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

396 
apply (simp add: zgcd_greatest_iff) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

397 
apply (rule_tac n = k in zrelprime_zdvd_zmult) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

398 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

399 
apply (simp add: zmult_commute) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

400 
apply (subgoal_tac "zgcd (k, zgcd (k * m, n)) = zgcd (k * m, zgcd (k, n))") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

401 
apply simp 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

402 
apply (simp (no_asm) add: zgcd_ac) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

403 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

404 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

405 
lemma zgcd_zmult_cancel: "zgcd (k, n) = 1 ==> zgcd (k * m, n) = zgcd (m, n)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

406 
apply (simp add: zgcd_def nat_abs_mult_distrib gcd_mult_cancel) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

407 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

408 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

409 
lemma zgcd_zgcd_zmult: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

410 
"zgcd (k, m) = 1 ==> zgcd (n, m) = 1 ==> zgcd (k * n, m) = 1" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

411 
apply (simp (no_asm_simp) add: zgcd_zmult_cancel) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

412 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

413 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

414 
lemma zdvd_iff_zgcd: "0 < m ==> (m dvd n) = (zgcd (n, m) = m)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

415 
apply safe 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

416 
apply (rule_tac [2] n = "zgcd (n, m)" in zdvd_trans) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

417 
apply (rule_tac [3] zgcd_zdvd1) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

418 
apply simp_all 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

419 
apply (unfold dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

420 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

421 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

422 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

423 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

424 
subsection {* Congruences *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

425 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

426 
lemma zcong_1 [simp]: "[a = b] (mod 1)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

427 
apply (unfold zcong_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

428 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

429 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

430 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

431 
lemma zcong_refl [simp]: "[k = k] (mod m)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

432 
apply (unfold zcong_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

433 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

434 
done 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

435 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

436 
lemma zcong_sym: "[a = b] (mod m) = [b = a] (mod m)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

437 
apply (unfold zcong_def dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

438 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

439 
apply (rule_tac [!] x = "k" in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

440 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

441 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

442 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

443 
lemma zcong_zadd: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

444 
"[a = b] (mod m) ==> [c = d] (mod m) ==> [a + c = b + d] (mod m)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

445 
apply (unfold zcong_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

446 
apply (rule_tac s = "(a  b) + (c  d)" in subst) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

447 
apply (rule_tac [2] zdvd_zadd) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

448 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

449 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

450 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

451 
lemma zcong_zdiff: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

452 
"[a = b] (mod m) ==> [c = d] (mod m) ==> [a  c = b  d] (mod m)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

453 
apply (unfold zcong_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

454 
apply (rule_tac s = "(a  b)  (c  d)" in subst) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

455 
apply (rule_tac [2] zdvd_zdiff) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

456 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

457 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

458 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

459 
lemma zcong_trans: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

460 
"[a = b] (mod m) ==> [b = c] (mod m) ==> [a = c] (mod m)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

461 
apply (unfold zcong_def dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

462 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

463 
apply (rule_tac x = "k + ka" in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

464 
apply (simp add: zadd_ac zadd_zmult_distrib2) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

465 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

466 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

467 
lemma zcong_zmult: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

468 
"[a = b] (mod m) ==> [c = d] (mod m) ==> [a * c = b * d] (mod m)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

469 
apply (rule_tac b = "b * c" in zcong_trans) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

470 
apply (unfold zcong_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

471 
apply (rule_tac s = "c * (a  b)" in subst) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

472 
apply (rule_tac [3] s = "b * (c  d)" in subst) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

473 
prefer 4 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

474 
apply (blast intro: zdvd_zmult) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

475 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

476 
apply (blast intro: zdvd_zmult) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

477 
apply (simp_all add: zdiff_zmult_distrib2 zmult_commute) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

478 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

479 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

480 
lemma zcong_scalar: "[a = b] (mod m) ==> [a * k = b * k] (mod m)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

481 
apply (rule zcong_zmult) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

482 
apply simp_all 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

483 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

484 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

485 
lemma zcong_scalar2: "[a = b] (mod m) ==> [k * a = k * b] (mod m)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

486 
apply (rule zcong_zmult) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

487 
apply simp_all 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

488 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

489 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

490 
lemma zcong_zmult_self: "[a * m = b * m] (mod m)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

491 
apply (unfold zcong_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

492 
apply (rule zdvd_zdiff) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

493 
apply simp_all 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

494 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

495 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

496 
lemma zcong_square: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

497 
"p \<in> zprime ==> 0 < a ==> [a * a = 1] (mod p) 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

498 
==> [a = 1] (mod p) \<or> [a = p  1] (mod p)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

499 
apply (unfold zcong_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

500 
apply (rule zprime_zdvd_zmult) 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

501 
apply (rule_tac [3] s = "a * a  1 + p * (1  a)" in subst) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

502 
prefer 4 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

503 
apply (simp add: zdvd_reduce) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

504 
apply (simp_all add: zdiff_zmult_distrib zmult_commute zdiff_zmult_distrib2) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

505 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

506 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

507 
lemma zcong_cancel: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

508 
"0 \<le> m ==> 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

509 
zgcd (k, m) = 1 ==> [a * k = b * k] (mod m) = [a = b] (mod m)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

510 
apply safe 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

511 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

512 
apply (blast intro: zcong_scalar) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

513 
apply (case_tac "b < a") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

514 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

515 
apply (subst zcong_sym) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

516 
apply (unfold zcong_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

517 
apply (rule_tac [!] zrelprime_zdvd_zmult) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

518 
apply (simp_all add: zdiff_zmult_distrib) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

519 
apply (subgoal_tac "m dvd ((a * k  b * k))") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

520 
apply (simp add: zminus_zdiff_eq) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

521 
apply (subst zdvd_zminus_iff) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

522 
apply assumption 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

523 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

524 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

525 
lemma zcong_cancel2: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

526 
"0 \<le> m ==> 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

527 
zgcd (k, m) = 1 ==> [k * a = k * b] (mod m) = [a = b] (mod m)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

528 
apply (simp add: zmult_commute zcong_cancel) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

529 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

530 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

531 
lemma zcong_zgcd_zmult_zmod: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

532 
"[a = b] (mod m) ==> [a = b] (mod n) ==> zgcd (m, n) = 1 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

533 
==> [a = b] (mod m * n)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

534 
apply (unfold zcong_def dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

535 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

536 
apply (subgoal_tac "m dvd n * ka") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

537 
apply (subgoal_tac "m dvd ka") 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

538 
apply (case_tac [2] "0 \<le> ka") 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

539 
prefer 3 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

540 
apply (subst zdvd_zminus_iff [symmetric]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

541 
apply (rule_tac n = n in zrelprime_zdvd_zmult) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

542 
apply (simp add: zgcd_commute) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

543 
apply (simp add: zmult_commute zdvd_zminus_iff) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

544 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

545 
apply (rule_tac n = n in zrelprime_zdvd_zmult) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

546 
apply (simp add: zgcd_commute) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

547 
apply (simp add: zmult_commute) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

548 
apply (auto simp add: dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

549 
apply (blast intro: sym) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

550 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

551 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

552 
lemma zcong_zless_imp_eq: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

553 
"0 \<le> a ==> 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

554 
a < m ==> 0 \<le> b ==> b < m ==> [a = b] (mod m) ==> a = b" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

555 
apply (unfold zcong_def dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

556 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

557 
apply (drule_tac f = "\<lambda>z. z mod m" in arg_cong) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

558 
apply (cut_tac z = a and w = b in zless_linear) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

559 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

560 
apply (subgoal_tac [2] "(a  b) mod m = a  b") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

561 
apply (rule_tac [3] mod_pos_pos_trivial) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

562 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

563 
apply (subgoal_tac "(m + (a  b)) mod m = m + (a  b)") 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

564 
apply (rule_tac [2] mod_pos_pos_trivial) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

565 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

566 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

567 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

568 
lemma zcong_square_zless: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

569 
"p \<in> zprime ==> 0 < a ==> a < p ==> 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

570 
[a * a = 1] (mod p) ==> a = 1 \<or> a = p  1" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

571 
apply (cut_tac p = p and a = a in zcong_square) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

572 
apply (simp add: zprime_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

573 
apply (auto intro: zcong_zless_imp_eq) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

574 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

575 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

576 
lemma zcong_not: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

577 
"0 < a ==> a < m ==> 0 < b ==> b < a ==> \<not> [a = b] (mod m)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

578 
apply (unfold zcong_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

579 
apply (rule zdvd_not_zless) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

580 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

581 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

582 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

583 
lemma zcong_zless_0: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

584 
"0 \<le> a ==> a < m ==> [a = 0] (mod m) ==> a = 0" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

585 
apply (unfold zcong_def dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

586 
apply auto 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

587 
apply (subgoal_tac "0 < m") 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

588 
apply (rotate_tac 1) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

589 
apply (simp add: int_0_le_mult_iff) 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

590 
apply (subgoal_tac "m * k < m * 1") 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

591 
apply (drule zmult_zless_cancel1 [THEN iffD1]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

592 
apply (auto simp add: linorder_neq_iff) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

593 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

594 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

595 
lemma zcong_zless_unique: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

596 
"0 < m ==> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

597 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

598 
apply (subgoal_tac [2] "[b = y] (mod m)") 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

599 
apply (case_tac [2] "b = 0") 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

600 
apply (case_tac [3] "y = 0") 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

601 
apply (auto intro: zcong_trans zcong_zless_0 zcong_zless_imp_eq order_less_le 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

602 
simp add: zcong_sym) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

603 
apply (unfold zcong_def dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

604 
apply (rule_tac x = "a mod m" in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

605 
apply (auto simp add: pos_mod_sign pos_mod_bound) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

606 
apply (rule_tac x = "(a div m)" in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

607 
apply (cut_tac a = a and b = m in zmod_zdiv_equality) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

608 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

609 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

610 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

611 
lemma zcong_iff_lin: "([a = b] (mod m)) = (\<exists>k. b = a + m * k)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

612 
apply (unfold zcong_def dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

613 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

614 
apply (rule_tac [!] x = "k" in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

615 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

616 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

617 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

618 
lemma zgcd_zcong_zgcd: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

619 
"0 < m ==> 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

620 
zgcd (a, m) = 1 ==> [a = b] (mod m) ==> zgcd (b, m) = 1" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

621 
apply (auto simp add: zcong_iff_lin) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

622 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

623 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

624 
lemma aux: "a = c ==> b = d ==> a  b = c  (d::int)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

625 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

626 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

627 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

628 
lemma aux: "a  b = (m::int) * (a div m  b div m) + (a mod m  b mod m)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

629 
apply (rule_tac "s" = "(m * (a div m) + a mod m)  (m * (b div m) + b mod m)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

630 
in trans) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

631 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

632 
apply (simp add: zdiff_zmult_distrib2) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

633 
apply (rule aux) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

634 
apply (rule_tac [!] zmod_zdiv_equality) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

635 
done 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

636 

11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

637 
lemma zcong_zmod: "[a = b] (mod m) = [a mod m = b mod m] (mod m)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

638 
apply (unfold zcong_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

639 
apply (rule_tac t = "a  b" in ssubst) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

640 
apply (rule_tac "m" = "m" in aux) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

641 
apply (rule trans) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

642 
apply (rule_tac [2] k = m and m = "a div m  b div m" in zdvd_reduce) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

643 
apply (simp add: zadd_commute) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

644 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

645 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

646 
lemma zcong_zmod_eq: "0 < m ==> [a = b] (mod m) = (a mod m = b mod m)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

647 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

648 
apply (rule_tac m = m in zcong_zless_imp_eq) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

649 
prefer 5 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

650 
apply (subst zcong_zmod [symmetric]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

651 
apply (simp_all add: pos_mod_bound pos_mod_sign) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

652 
apply (unfold zcong_def dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

653 
apply (rule_tac x = "a div m  b div m" in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

654 
apply (rule_tac m1 = m in aux [THEN trans]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

655 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

656 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

657 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

658 
lemma zcong_zminus [iff]: "[a = b] (mod m) = [a = b] (mod m)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

659 
apply (auto simp add: zcong_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

660 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

661 

11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

662 
lemma zcong_zero [iff]: "[a = b] (mod 0) = (a = b)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

663 
apply (auto simp add: zcong_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

664 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

665 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

666 
lemma "[a = b] (mod m) = (a mod m = b mod m)" 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

667 
apply (tactic {* zdiv_undefined_case_tac "m = 0" 1 *}) 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

668 
apply (case_tac "0 < m") 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

669 
apply (simp add: zcong_zmod_eq) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

670 
apply (rule_tac t = m in zminus_zminus [THEN subst]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

671 
apply (subst zcong_zminus) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

672 
apply (subst zcong_zmod_eq) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

673 
apply arith 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

674 
oops  {* FIXME: finish this proof? *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

675 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

676 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

677 
subsection {* Modulo *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

678 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

679 
lemma zmod_zdvd_zmod: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

680 
"0 < (m::int) ==> m dvd b ==> (a mod b mod m) = (a mod m)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

681 
apply (unfold dvd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

682 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

683 
apply (subst zcong_zmod_eq [symmetric]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

684 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

685 
apply (subst zcong_iff_lin) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

686 
apply (rule_tac x = "k * (a div (m * k))" in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

687 
apply (subst zadd_commute) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

688 
apply (subst zmult_assoc [symmetric]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

689 
apply (rule_tac zmod_zdiv_equality) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

690 
apply assumption 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

691 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

692 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

693 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

694 
subsection {* Extended GCD *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

695 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

696 
declare xzgcda.simps [simp del] 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

697 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

698 
lemma aux1: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

699 
"zgcd (r', r) = k > 0 < r > 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

700 
(\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn))" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

701 
apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

702 
z = s and aa = t' and ab = t in xzgcda.induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

703 
apply (subst zgcd_eq) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

704 
apply (subst xzgcda.simps) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

705 
apply auto 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

706 
apply (case_tac "r' mod r = 0") 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

707 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

708 
apply (frule_tac a = "r'" in pos_mod_sign) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

709 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

710 
apply arith 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

711 
apply (rule exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

712 
apply (rule exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

713 
apply (subst xzgcda.simps) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

714 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

715 
apply (simp add: zabs_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

716 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

717 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

718 
lemma aux2: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

719 
"(\<exists>sn tn. xzgcda (m, n, r', r, s', s, t', t) = (k, sn, tn)) > 0 < r > 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

720 
zgcd (r', r) = k" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

721 
apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

722 
z = s and aa = t' and ab = t in xzgcda.induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

723 
apply (subst zgcd_eq) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

724 
apply (subst xzgcda.simps) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

725 
apply (auto simp add: linorder_not_le) 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

726 
apply (case_tac "r' mod r = 0") 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

727 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

728 
apply (frule_tac a = "r'" in pos_mod_sign) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

729 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

730 
apply arith 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

731 
apply (erule_tac P = "xzgcda ?u = ?v" in rev_mp) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

732 
apply (subst xzgcda.simps) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

733 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

734 
apply (simp add: zabs_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

735 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

736 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

737 
lemma xzgcd_correct: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

738 
"0 < n ==> (zgcd (m, n) = k) = (\<exists>s t. xzgcd m n = (k, s, t))" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

739 
apply (unfold xzgcd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

740 
apply (rule iffI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

741 
apply (rule_tac [2] aux2 [THEN mp, THEN mp]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

742 
apply (rule aux1 [THEN mp, THEN mp]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

743 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

744 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

745 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

746 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

747 
text {* \medskip @{term xzgcd} linear *} 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

748 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

749 
lemma aux: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

750 
"(a  r * b) * m + (c  r * d) * (n::int) = 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

751 
(a * m + c * n)  r * (b * m + d * n)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

752 
apply (simp add: zdiff_zmult_distrib zadd_zmult_distrib2 zmult_assoc) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

753 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

754 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

755 
lemma aux: 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

756 
"r' = s' * m + t' * n ==> r = s * m + t * n 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

757 
==> (r' mod r) = (s'  (r' div r) * s) * m + (t'  (r' div r) * t) * (n::int)" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

758 
apply (rule trans) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

759 
apply (rule_tac [2] aux [symmetric]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

760 
apply simp 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

761 
apply (subst eq_zdiff_eq) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

762 
apply (rule trans [symmetric]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

763 
apply (rule_tac b = "s * m + t * n" in zmod_zdiv_equality) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

764 
apply (simp add: zmult_commute) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

765 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

766 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

767 
lemma order_le_neq_implies_less: "(x::'a::order) \<le> y ==> x \<noteq> y ==> x < y" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

768 
by (rule iffD2 [OF order_less_le conjI]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

769 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

770 
lemma xzgcda_linear [rule_format]: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

771 
"0 < r > xzgcda (m, n, r', r, s', s, t', t) = (rn, sn, tn) > 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

772 
r' = s' * m + t' * n > r = s * m + t * n > rn = sn * m + tn * n" 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

773 
apply (rule_tac u = m and v = n and w = r' and x = r and y = s' and 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

774 
z = s and aa = t' and ab = t in xzgcda.induct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

775 
apply (subst xzgcda.simps) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

776 
apply (simp (no_asm)) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

777 
apply (rule impI)+ 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

778 
apply (case_tac "r' mod r = 0") 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

779 
apply (simp add: xzgcda.simps) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

780 
apply clarify 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

781 
apply (subgoal_tac "0 < r' mod r") 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

782 
apply (rule_tac [2] order_le_neq_implies_less) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

783 
apply (rule_tac [2] pos_mod_sign) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

784 
apply (cut_tac m = m and n = n and r' = r' and r = r and s' = s' and 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

785 
s = s and t' = t' and t = t in aux) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

786 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

787 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

788 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

789 
lemma xzgcd_linear: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

790 
"0 < n ==> xzgcd m n = (r, s, t) ==> r = s * m + t * n" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

791 
apply (unfold xzgcd_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

792 
apply (erule xzgcda_linear) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

793 
apply assumption 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

794 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

795 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

796 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

797 
lemma zgcd_ex_linear: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

798 
"0 < n ==> zgcd (m, n) = k ==> (\<exists>s t. k = s * m + t * n)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

799 
apply (simp add: xzgcd_correct) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

800 
apply safe 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

801 
apply (rule exI)+ 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

802 
apply (erule xzgcd_linear) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

803 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

804 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

805 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

806 
lemma zcong_lineq_ex: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

807 
"0 < n ==> zgcd (a, n) = 1 ==> \<exists>x. [a * x = 1] (mod n)" 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

808 
apply (cut_tac m = a and n = n and k = "1" in zgcd_ex_linear) 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

809 
apply safe 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

810 
apply (rule_tac x = s in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

811 
apply (rule_tac b = "s * a + t * n" in zcong_trans) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

812 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

813 
apply simp 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

814 
apply (unfold zcong_def) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

815 
apply (simp (no_asm) add: zmult_commute zdvd_zminus_iff) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

816 
done 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

817 

7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

818 
lemma zcong_lineq_unique: 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

819 
"0 < n ==> 
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

820 
zgcd (a, n) = 1 ==> \<exists>!x. 0 \<le> x \<and> x < n \<and> [a * x = b] (mod n)" 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

821 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

822 
apply (rule_tac [2] zcong_zless_imp_eq) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

823 
apply (tactic {* stac (thm "zcong_cancel2" RS sym) 6 *}) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

824 
apply (rule_tac [8] zcong_trans) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

825 
apply (simp_all (no_asm_simp)) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

826 
prefer 2 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

827 
apply (simp add: zcong_sym) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

828 
apply (cut_tac a = a and n = n in zcong_lineq_ex) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

829 
apply auto 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

830 
apply (rule_tac x = "x * b mod n" in exI) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

831 
apply safe 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

832 
apply (simp_all (no_asm_simp) add: pos_mod_bound pos_mod_sign) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

833 
apply (subst zcong_zmod) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

834 
apply (subst zmod_zmult1_eq [symmetric]) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

835 
apply (subst zcong_zmod [symmetric]) 
11868
56db9f3a6b3e
Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents:
11701
diff
changeset

836 
apply (subgoal_tac "[a * x * b = 1 * b] (mod n)") 
11049
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

837 
apply (rule_tac [2] zcong_zmult) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

838 
apply (simp_all add: zmult_assoc) 
7eef34adb852
HOLNumberTheory: converted to newstyle format and proper document setup;
wenzelm
parents:
10147
diff
changeset

839 
done 
9508
4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

840 

4d01dbf6ded7
Chinese Remainder Theorem, Wilsons Theorem, etc., by T M Masmussen
paulson
parents:
diff
changeset

841 
end 