author  wenzelm 
Sun, 20 May 2018 22:04:46 +0200  
changeset 68238  eb57621568bb 
parent 67406  23307fd33906 
permissions  rwrr 
55159
608c157d743d
Replacing the theory Library/Binomial by Number_Theory/Binomial
paulson <lp15@cam.ac.uk>
parents:
48985
diff
changeset

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

2 

67406  3 
text\<open>\noindent 
10846
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. 
67406  5 
\<close> 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

6 

67406  7 
text\<open>\noindent 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

8 
SKIP most developments... 
67406  9 
\<close> 
10846
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" 
58860  14 
apply (auto simp add: is_gcd_def) 
10958  15 
done 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

16 

25261  17 
lemma gcd_commute: "gcd m n = gcd n m" 
10958  18 
apply (rule is_gcd_unique) 
19 
apply (rule is_gcd) 

20 
apply (subst is_gcd_commute) 

21 
apply (simp add: is_gcd) 

22 
done 

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

23 

25261  24 
lemma gcd_1 [simp]: "gcd m (Suc 0) = Suc 0" 
10958  25 
apply simp 
26 
done 

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

27 

25261  28 
lemma gcd_1_left [simp]: "gcd (Suc 0) m = Suc 0" 
11711  29 
apply (simp add: gcd_commute [of "Suc 0"]) 
10958  30 
done 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

31 

67406  32 
text\<open>\noindent 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

33 
as far as HERE. 
67406  34 
\<close> 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

35 

67406  36 
text\<open>\noindent 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

37 
SKIP THIS PROOF 
67406  38 
\<close> 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

39 

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

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

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

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

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

47 

67406  48 
text \<open> 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

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

50 
\rulename{gcd_mult_distrib2} 
67406  51 
\<close> 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

52 

67406  53 
text\<open>\noindent 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

54 
of, simplified 
67406  55 
\<close> 
10846
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 

68238  58 
lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1] for k 
58860  59 
lemmas gcd_mult_1 = gcd_mult_0 [simplified] 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

60 

14403  61 
lemmas where1 = gcd_mult_distrib2 [where m=1] 
62 

63 
lemmas where2 = gcd_mult_distrib2 [where m=1 and k=1] 

64 

68238  65 
lemmas where3 = gcd_mult_distrib2 [where m=1 and k="j+k"] for j k 
14403  66 

67406  67 
text \<open> 
14403  68 
example using ``of'': 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

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

70 

14403  71 
example using ``where'': 
72 
@{thm[display] gcd_mult_distrib2 [where m=1]} 

73 

74 
example using ``where'', ``and'': 

75 
@{thm[display] gcd_mult_distrib2 [where m=1 and k="j+k"]} 

76 

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

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

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

79 

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

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

81 
\rulename{gcd_mult_1} 
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 
@{thm[display] sym} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

84 
\rulename{sym} 
67406  85 
\<close> 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

86 

58860  87 
lemmas gcd_mult0 = gcd_mult_1 [THEN sym] 
13550  88 
(*not quite right: we need ?k but this gives k*) 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

89 

68238  90 
lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym] for k 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

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

92 

67406  93 
text \<open> 
13550  94 
more legible, and variables properly generalized 
67406  95 
\<close> 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

96 

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

98 
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

99 

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

100 

68238  101 
lemmas gcd_self0 = gcd_mult [of k 1, simplified] for k 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

102 

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

103 

67406  104 
text \<open> 
25264  105 
@{thm[display] gcd_mult} 
106 
\rulename{gcd_mult} 

107 

108 
@{thm[display] gcd_self0} 

109 
\rulename{gcd_self0} 

67406  110 
\<close> 
25264  111 

67406  112 
text \<open> 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

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

114 

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

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

116 
\rulename{iffD1} 
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 
@{thm[display] iffD2} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

119 
\rulename{iffD2} 
67406  120 
\<close> 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

121 

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

122 

67406  123 
text \<open> 
13550  124 
again: more legible, and variables properly generalized 
67406  125 
\<close> 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

126 

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

128 
by (rule gcd_mult [of k 1, simplified]) 
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 

67406  131 
text\<open> 
10958  132 
NEXT SECTION: Methods for Forward Proof 
133 

134 
NEW 

135 

136 
theorem arg_cong, useful in forward steps 

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

138 
\rulename{arg_cong} 

67406  139 
\<close> 
10958  140 

11711  141 
lemma "2 \<le> u \<Longrightarrow> u*m \<noteq> Suc(u*n)" 
12390  142 
apply (intro notI) 
67406  143 
txt\<open> 
10958  144 
before using arg_cong 
145 
@{subgoals[display,indent=0,margin=65]} 

67406  146 
\<close> 
10958  147 
apply (drule_tac f="\<lambda>x. x mod u" in arg_cong) 
67406  148 
txt\<open> 
10958  149 
after using arg_cong 
150 
@{subgoals[display,indent=0,margin=65]} 

67406  151 
\<close> 
10958  152 
apply (simp add: mod_Suc) 
153 
done 

154 

67406  155 
text\<open> 
10958  156 
have just used this rule: 
157 
@{thm[display] mod_Suc[no_vars]} 

158 
\rulename{mod_Suc} 

159 

160 
@{thm[display] mult_le_mono1[no_vars]} 

161 
\rulename{mult_le_mono1} 

67406  162 
\<close> 
10958  163 

164 

67406  165 
text\<open> 
10958  166 
example of "insert" 
67406  167 
\<close> 
10958  168 

55159
608c157d743d
Replacing the theory Library/Binomial by Number_Theory/Binomial
paulson <lp15@cam.ac.uk>
parents:
48985
diff
changeset

169 
lemma relprime_dvd_mult: 
25261  170 
"\<lbrakk> gcd k n = 1; k dvd m*n \<rbrakk> \<Longrightarrow> k dvd m" 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

171 
apply (insert gcd_mult_distrib2 [of m k n]) 
67406  172 
txt\<open>@{subgoals[display,indent=0,margin=65]}\<close> 
10958  173 
apply simp 
67406  174 
txt\<open>@{subgoals[display,indent=0,margin=65]}\<close> 
58860  175 
apply (erule_tac t="m" in ssubst) 
10958  176 
apply simp 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

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

178 

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

179 

67406  180 
text \<open> 
25264  181 
@{thm[display] relprime_dvd_mult} 
182 
\rulename{relprime_dvd_mult} 

183 

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

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

185 

64242
93c6f0da5c70
more standardized theorem names for facts involving the div and mod identity
haftmann
parents:
58860
diff
changeset

186 
@{thm[display] div_mult_mod_eq} 
93c6f0da5c70
more standardized theorem names for facts involving the div and mod identity
haftmann
parents:
58860
diff
changeset

187 
\rulename{div_mult_mod_eq} 
67406  188 
\<close> 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

189 

11407  190 
(*MOVED to Force.thy, which now depends only on Divides.thy 
191 
lemma div_mult_self_is_m: "0<n \<Longrightarrow> (m*n) div n = (m::nat)" 

192 
*) 

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

193 

58860  194 
lemma relprime_dvd_mult_iff: "gcd k n = 1 \<Longrightarrow> (k dvd m*n) = (k dvd m)" 
27658  195 
by (auto intro: relprime_dvd_mult elim: dvdE) 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

196 

58860  197 
lemma relprime_20_81: "gcd 20 81 = 1" 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

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

199 

67406  200 
text \<open> 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

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

202 

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

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

204 
\rulename{relprime_dvd_mult} 
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 
@{thm[display] relprime_dvd_mult [OF relprime_20_81]} 
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

207 

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

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

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

210 

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

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

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

213 

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

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

215 

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

216 
@{thm[display] dvd_add [OF _ dvd_refl]} 
67406  217 
\<close> 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

218 

58860  219 
lemma "\<lbrakk>(z::int) < 37; 66 < 2*z; z*z \<noteq> 1225; Q(34); Q(36)\<rbrakk> \<Longrightarrow> Q(z)" 
11711  220 
apply (subgoal_tac "z = 34 \<or> z = 36") 
67406  221 
txt\<open> 
10958  222 
the tactic leaves two subgoals: 
223 
@{subgoals[display,indent=0,margin=65]} 

67406  224 
\<close> 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

225 
apply blast 
11711  226 
apply (subgoal_tac "z \<noteq> 35") 
67406  227 
txt\<open> 
10958  228 
the tactic leaves two subgoals: 
229 
@{subgoals[display,indent=0,margin=65]} 

67406  230 
\<close> 
10846
623141a08705
reformatting, and splitting the end of "Primes" to create "Forward"
paulson
parents:
diff
changeset

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

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

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

234 

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

235 

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

236 
end 