author  paulson 
Fri, 12 Jan 2001 16:05:12 +0100  
changeset 10877  6417de2029b0 
parent 10846  623141a08705 
child 10958  fd582f0d649b 
permissions  rwrr 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

1 
theory Forward = Primes: 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

2 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

3 
text{*\noindent 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

4 
Forward proof material: of, OF, THEN, simplify, rule_format. 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

5 
*} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

6 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

7 
text{*\noindent 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

8 
SKIP most developments... 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

9 
*} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

10 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

11 
(** Commutativity **) 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

12 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

13 
lemma is_gcd_commute: "is_gcd k m n = is_gcd k n m" 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

14 
apply (auto simp add: is_gcd_def); 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

15 
done 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

16 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

17 
lemma gcd_commute: "gcd(m,n) = gcd(n,m)" 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

18 
apply (rule is_gcd_unique) 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

19 
apply (rule is_gcd) 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

20 
apply (subst is_gcd_commute) 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

21 
apply (simp add: is_gcd) 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

22 
done 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

23 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

24 
lemma gcd_1 [simp]: "gcd(m,1) = 1" 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

25 
apply (simp) 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

26 
done 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

27 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

28 
lemma gcd_1_left [simp]: "gcd(1,m) = 1" 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

29 
apply (simp add: gcd_commute [of 1]) 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

30 
done 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

31 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

32 
text{*\noindent 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

33 
as far as HERE. 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

34 
*} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

35 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

36 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

37 
text {* 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

38 
@{thm[display] gcd_1} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

39 
\rulename{gcd_1} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

40 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

41 
@{thm[display] gcd_1_left} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

42 
\rulename{gcd_1_left} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

43 
*}; 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

44 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

45 
text{*\noindent 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

46 
SKIP THIS PROOF 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

47 
*} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

48 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

49 
lemma gcd_mult_distrib2: "k * gcd(m,n) = gcd(k*m, k*n)" 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

50 
apply (induct_tac m n rule: gcd.induct) 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

51 
apply (case_tac "n=0") 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

52 
apply (simp) 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

53 
apply (case_tac "k=0") 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

54 
apply (simp_all add: mod_geq gcd_non_0 mod_mult_distrib2) 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

55 
done 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

56 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

57 
text {* 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

58 
@{thm[display] gcd_mult_distrib2} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

59 
\rulename{gcd_mult_distrib2} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

60 
*}; 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

61 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

62 
text{*\noindent 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

63 
of, simplified 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

64 
*} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

65 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

66 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

67 
lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1]; 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

68 
lemmas gcd_mult_1 = gcd_mult_0 [simplified]; 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

69 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

70 
text {* 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

71 
@{thm[display] gcd_mult_distrib2 [of _ 1]} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

72 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

73 
@{thm[display] gcd_mult_0} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

74 
\rulename{gcd_mult_0} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

75 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

76 
@{thm[display] gcd_mult_1} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

77 
\rulename{gcd_mult_1} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

78 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

79 
@{thm[display] sym} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

80 
\rulename{sym} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

81 
*}; 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

82 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

83 
lemmas gcd_mult = gcd_mult_1 [THEN sym]; 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

84 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

85 
lemmas gcd_mult = gcd_mult_distrib2 [of k 1, simplified, THEN sym]; 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

86 
(*better in one step!*) 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

87 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

88 
text {* 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

89 
more legible 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

90 
*}; 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

91 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

92 
lemma gcd_mult [simp]: "gcd(k, k*n) = k" 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

93 
by (rule gcd_mult_distrib2 [of k 1, simplified, THEN sym]) 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

94 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

95 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

96 
lemmas gcd_self = gcd_mult [of k 1, simplified]; 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

97 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

98 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

99 
text {* 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

100 
Rules handy with THEN 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

101 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

102 
@{thm[display] iffD1} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

103 
\rulename{iffD1} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

104 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

105 
@{thm[display] iffD2} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

106 
\rulename{iffD2} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

107 
*}; 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

108 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

109 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

110 
text {* 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

111 
again: more legible 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

112 
*}; 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

113 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

114 
lemma gcd_self [simp]: "gcd(k,k) = k" 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

115 
by (rule gcd_mult [of k 1, simplified]) 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

116 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

117 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

118 
lemma relprime_dvd_mult: 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

119 
"\<lbrakk> gcd(k,n)=1; k dvd m*n \<rbrakk> \<Longrightarrow> k dvd m"; 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

120 
apply (insert gcd_mult_distrib2 [of m k n]) 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

121 
apply (simp) 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

122 
apply (erule_tac t="m" in ssubst); 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

123 
apply (simp) 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

124 
done 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

125 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

126 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

127 
text {* 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

128 
Another example of "insert" 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

129 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

130 
@{thm[display] mod_div_equality} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

131 
\rulename{mod_div_equality} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

132 
*}; 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

133 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

134 
lemma div_mult_self_is_m: 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

135 
"0<n \<Longrightarrow> (m*n) div n = (m::nat)" 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

136 
apply (insert mod_div_equality [of "m*n" n]) 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

137 
apply (simp) 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

138 
done 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

139 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

140 
lemma relprime_dvd_mult_iff: "gcd(k,n)=1 \<Longrightarrow> (k dvd m*n) = (k dvd m)"; 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

141 
by (blast intro: relprime_dvd_mult dvd_trans) 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

142 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

143 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

144 
lemma relprime_20_81: "gcd(#20,#81) = 1"; 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

145 
by (simp add: gcd.simps) 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

146 

10877  147 
text{*example of arg_cong (NEW) 
148 

149 
@{thm[display] arg_cong[no_vars]} 

150 
\rulename{arg_cong} 

151 
*} 

10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

152 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

153 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

154 
text {* 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

155 
Examples of 'OF' 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

156 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

157 
@{thm[display] relprime_dvd_mult} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

158 
\rulename{relprime_dvd_mult} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

159 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

160 
@{thm[display] relprime_dvd_mult [OF relprime_20_81]} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

161 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

162 
@{thm[display] dvd_refl} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

163 
\rulename{dvd_refl} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

164 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

165 
@{thm[display] dvd_add} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

166 
\rulename{dvd_add} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

167 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

168 
@{thm[display] dvd_add [OF dvd_refl dvd_refl]} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

169 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

170 
@{thm[display] dvd_add [OF _ dvd_refl]} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

171 
*}; 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

172 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

173 
lemma "\<lbrakk>(z::int) < #37; #66 < #2*z; z*z \<noteq> #1225; Q(#34); Q(#36)\<rbrakk> \<Longrightarrow> Q(z)"; 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

174 
apply (subgoal_tac "z = #34 \<or> z = #36") 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

175 
apply blast 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

176 
apply (subgoal_tac "z \<noteq> #35") 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

177 
apply arith 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

178 
apply force 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

179 
done 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

180 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

181 
text 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

182 
{* 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

183 
proof\ (prove):\ step\ 1\isanewline 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

184 
\isanewline 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

185 
goal\ (lemma):\isanewline 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

186 
\isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \ \isasymLongrightarrow \ Q\ z\isanewline 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

187 
\ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

188 
\ \ \ \ \ \ \ z\ =\ \#34\ \isasymor \ z\ =\ \#36\isasymrbrakk \isanewline 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

189 
\ \ \ \ \isasymLongrightarrow \ Q\ z\isanewline 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

190 
\ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \isanewline 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

191 
\ \ \ \ \isasymLongrightarrow \ z\ =\ \#34\ \isasymor \ z\ =\ \#36 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

192 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

193 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

194 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

195 
proof\ (prove):\ step\ 3\isanewline 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

196 
\isanewline 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

197 
goal\ (lemma):\isanewline 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

198 
\isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \ \isasymLongrightarrow \ Q\ z\isanewline 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

199 
\ 1.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36;\isanewline 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

200 
\ \ \ \ \ \ \ z\ \isasymnoteq \ \#35\isasymrbrakk \isanewline 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

201 
\ \ \ \ \isasymLongrightarrow \ z\ =\ \#34\ \isasymor \ z\ =\ \#36\isanewline 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

202 
\ 2.\ \isasymlbrakk z\ <\ \#37;\ \#66\ <\ \#2\ *\ z;\ z\ *\ z\ \isasymnoteq \ \#1225;\ Q\ \#34;\ Q\ \#36\isasymrbrakk \isanewline 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

203 
\ \ \ \ \isasymLongrightarrow \ z\ \isasymnoteq \ \#35 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

204 
*} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

205 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

206 

623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

207 
end 