author  wenzelm 
Sat, 05 Apr 2014 15:03:40 +0200  
changeset 56421  1ffd7eaa778b 
parent 48985  5386df44a037 
child 57512  cc97b347b301 
permissions  rwrr 
27376  1 
theory Numbers 
2 
imports Complex_Main 

3 
begin 

10603  4 

5 
text{* 

6 

7 
numeric literals; default simprules; can reorient 

8 
*} 

9 

11711  10 
lemma "2 * m = m + m" 
10880  11 
txt{* 
12 
@{subgoals[display,indent=0,margin=65]} 

13 
*}; 

10603  14 
oops 
15 

44048  16 
fun h :: "nat \<Rightarrow> nat" where 
11711  17 
"h i = (if i = 3 then 2 else i)" 
10880  18 

10603  19 
text{* 
11711  20 
@{term"h 3 = 2"} 
10880  21 
@{term"h i = i"} 
22 
*} 

10603  23 

10880  24 
text{* 
10603  25 
@{thm[display] numeral_1_eq_1[no_vars]} 
26 
\rulename{numeral_1_eq_1} 

27 

28 
@{thm[display] add_2_eq_Suc[no_vars]} 

29 
\rulename{add_2_eq_Suc} 

30 

31 
@{thm[display] add_2_eq_Suc'[no_vars]} 

32 
\rulename{add_2_eq_Suc'} 

33 

34 
@{thm[display] add_assoc[no_vars]} 

35 
\rulename{add_assoc} 

36 

37 
@{thm[display] add_commute[no_vars]} 

38 
\rulename{add_commute} 

39 

40 
@{thm[display] add_left_commute[no_vars]} 

41 
\rulename{add_left_commute} 

42 

43 
these form add_ac; similarly there is mult_ac 

44 
*} 

45 

46 
lemma "Suc(i + j*l*k + m*n) = f (n*m + i + k*j*l)" 

10880  47 
txt{* 
48 
@{subgoals[display,indent=0,margin=65]} 

49 
*}; 

10603  50 
apply (simp add: add_ac mult_ac) 
10880  51 
txt{* 
52 
@{subgoals[display,indent=0,margin=65]} 

53 
*}; 

10603  54 
oops 
55 

56 
text{* 

57 

58 
@{thm[display] div_le_mono[no_vars]} 

59 
\rulename{div_le_mono} 

60 

61 
@{thm[display] diff_mult_distrib[no_vars]} 

62 
\rulename{diff_mult_distrib} 

63 

47183  64 
@{thm[display] mult_mod_left[no_vars]} 
65 
\rulename{mult_mod_left} 

10603  66 

67 
@{thm[display] nat_diff_split[no_vars]} 

68 
\rulename{nat_diff_split} 

69 
*} 

70 

71 

12156
d2758965362e
newstyle numerals without leading #, along with generic 0 and 1
paulson
parents:
11711
diff
changeset

72 
lemma "(n  1) * (n + 1) = n * n  (1::nat)" 
12843
50bd380e6675
iff del: less_Suc0  luckily this does NOT affect the printed text;
wenzelm
parents:
12156
diff
changeset

73 
apply (clarsimp split: nat_diff_split iff del: less_Suc0) 
12156
d2758965362e
newstyle numerals without leading #, along with generic 0 and 1
paulson
parents:
11711
diff
changeset

74 
{* @{subgoals[display,indent=0,margin=65]} *} 
d2758965362e
newstyle numerals without leading #, along with generic 0 and 1
paulson
parents:
11711
diff
changeset

75 
apply (subgoal_tac "n=0", force, arith) 
d2758965362e
newstyle numerals without leading #, along with generic 0 and 1
paulson
parents:
11711
diff
changeset

76 
done 
d2758965362e
newstyle numerals without leading #, along with generic 0 and 1
paulson
parents:
11711
diff
changeset

77 

d2758965362e
newstyle numerals without leading #, along with generic 0 and 1
paulson
parents:
11711
diff
changeset

78 

11711  79 
lemma "(n  2) * (n + 2) = n * n  (4::nat)" 
12156
d2758965362e
newstyle numerals without leading #, along with generic 0 and 1
paulson
parents:
11711
diff
changeset

80 
apply (simp split: nat_diff_split, clarify) 
11480  81 
{* @{subgoals[display,indent=0,margin=65]} *} 
82 
apply (subgoal_tac "n=0  n=1", force, arith) 

10603  83 
done 
84 

85 
text{* 

86 
@{thm[display] mod_if[no_vars]} 

87 
\rulename{mod_if} 

88 

89 
@{thm[display] mod_div_equality[no_vars]} 

90 
\rulename{mod_div_equality} 

91 

92 

93 
@{thm[display] div_mult1_eq[no_vars]} 

94 
\rulename{div_mult1_eq} 

95 

30224  96 
@{thm[display] mod_mult_right_eq[no_vars]} 
97 
\rulename{mod_mult_right_eq} 

10603  98 

99 
@{thm[display] div_mult2_eq[no_vars]} 

100 
\rulename{div_mult2_eq} 

101 

102 
@{thm[display] mod_mult2_eq[no_vars]} 

103 
\rulename{mod_mult2_eq} 

104 

105 
@{thm[display] div_mult_mult1[no_vars]} 

106 
\rulename{div_mult_mult1} 

107 

27658  108 
@{thm[display] div_by_0 [no_vars]} 
109 
\rulename{div_by_0} 

10603  110 

27658  111 
@{thm[display] mod_by_0 [no_vars]} 
112 
\rulename{mod_by_0} 

10603  113 

33750  114 
@{thm[display] dvd_antisym[no_vars]} 
115 
\rulename{dvd_antisym} 

10603  116 

117 
@{thm[display] dvd_add[no_vars]} 

118 
\rulename{dvd_add} 

119 

120 
For the integers, I'd list a few theorems that somehow involve negative 

13757  121 
numbers.*} 
10603  122 

13757  123 

124 
text{* 

10603  125 
Division, remainder of negatives 
126 

127 

128 
@{thm[display] pos_mod_sign[no_vars]} 

129 
\rulename{pos_mod_sign} 

130 

131 
@{thm[display] pos_mod_bound[no_vars]} 

132 
\rulename{pos_mod_bound} 

133 

134 
@{thm[display] neg_mod_sign[no_vars]} 

135 
\rulename{neg_mod_sign} 

136 

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

138 
\rulename{neg_mod_bound} 

139 

140 
@{thm[display] zdiv_zadd1_eq[no_vars]} 

141 
\rulename{zdiv_zadd1_eq} 

142 

30224  143 
@{thm[display] mod_add_eq[no_vars]} 
144 
\rulename{mod_add_eq} 

10603  145 

146 
@{thm[display] zdiv_zmult1_eq[no_vars]} 

147 
\rulename{zdiv_zmult1_eq} 

148 

47183  149 
@{thm[display] mod_mult_right_eq[no_vars]} 
150 
\rulename{mod_mult_right_eq} 

10603  151 

152 
@{thm[display] zdiv_zmult2_eq[no_vars]} 

153 
\rulename{zdiv_zmult2_eq} 

154 

155 
@{thm[display] zmod_zmult2_eq[no_vars]} 

156 
\rulename{zmod_zmult2_eq} 

157 
*} 

158 

11174  159 
lemma "abs (x+y) \<le> abs x + abs (y :: int)" 
10880  160 
by arith 
161 

11711  162 
lemma "abs (2*x) = 2 * abs (x :: int)" 
16585  163 
by (simp add: abs_if) 
11174  164 

13757  165 

166 
text {*Induction rules for the Integers 

167 

168 
@{thm[display] int_ge_induct[no_vars]} 

169 
\rulename{int_ge_induct} 

170 

171 
@{thm[display] int_gr_induct[no_vars]} 

172 
\rulename{int_gr_induct} 

173 

174 
@{thm[display] int_le_induct[no_vars]} 

175 
\rulename{int_le_induct} 

176 

177 
@{thm[display] int_less_induct[no_vars]} 

178 
\rulename{int_less_induct} 

179 
*} 

180 

14400  181 
text {*FIELDS 
10764  182 

14295  183 
@{thm[display] dense[no_vars]} 
184 
\rulename{dense} 

10603  185 

14288  186 
@{thm[display] times_divide_eq_right[no_vars]} 
187 
\rulename{times_divide_eq_right} 

10764  188 

14288  189 
@{thm[display] times_divide_eq_left[no_vars]} 
190 
\rulename{times_divide_eq_left} 

10764  191 

14288  192 
@{thm[display] divide_divide_eq_right[no_vars]} 
193 
\rulename{divide_divide_eq_right} 

10764  194 

14288  195 
@{thm[display] divide_divide_eq_left[no_vars]} 
196 
\rulename{divide_divide_eq_left} 

10764  197 

14295  198 
@{thm[display] minus_divide_left[no_vars]} 
199 
\rulename{minus_divide_left} 

10764  200 

14295  201 
@{thm[display] minus_divide_right[no_vars]} 
202 
\rulename{minus_divide_right} 

10764  203 

204 
This last NOT a simprule 

205 

14295  206 
@{thm[display] add_divide_distrib[no_vars]} 
207 
\rulename{add_divide_distrib} 

10764  208 
*} 
10603  209 

11711  210 
lemma "3/4 < (7/8 :: real)" 
11174  211 
by simp 
212 

11711  213 
lemma "P ((3/4) * (8/15 :: real))" 
11174  214 
txt{* 
215 
@{subgoals[display,indent=0,margin=65]} 

216 
*}; 

217 
apply simp 

218 
txt{* 

219 
@{subgoals[display,indent=0,margin=65]} 

220 
*}; 

221 
oops 

222 

11711  223 
lemma "(3/4) * (8/15) < (x :: real)" 
11174  224 
txt{* 
225 
@{subgoals[display,indent=0,margin=65]} 

226 
*}; 

227 
apply simp 

228 
txt{* 

229 
@{subgoals[display,indent=0,margin=65]} 

230 
*}; 

231 
oops 

232 

14400  233 
text{* 
234 
Ring and Field 

235 

236 
Requires a field, or else an ordered ring 

237 

238 
@{thm[display] mult_eq_0_iff[no_vars]} 

239 
\rulename{mult_eq_0_iff} 

240 

241 
@{thm[display] mult_cancel_right[no_vars]} 

242 
\rulename{mult_cancel_right} 

23504  243 

244 
@{thm[display] mult_cancel_left[no_vars]} 

245 
\rulename{mult_cancel_left} 

14400  246 
*} 
247 

248 
text{* 

249 
effect of show sorts on the above 

23504  250 

32834  251 
@{thm[display,show_sorts] mult_cancel_left[no_vars]} 
23504  252 
\rulename{mult_cancel_left} 
14400  253 
*} 
254 

255 
text{* 

256 
absolute value 

257 

258 
@{thm[display] abs_mult[no_vars]} 

259 
\rulename{abs_mult} 

260 

261 
@{thm[display] abs_le_iff[no_vars]} 

262 
\rulename{abs_le_iff} 

263 

264 
@{thm[display] abs_triangle_ineq[no_vars]} 

265 
\rulename{abs_triangle_ineq} 

266 

267 
@{thm[display] power_add[no_vars]} 

268 
\rulename{power_add} 

269 

270 
@{thm[display] power_mult[no_vars]} 

271 
\rulename{power_mult} 

272 

273 
@{thm[display] power_abs[no_vars]} 

274 
\rulename{power_abs} 

275 

276 

277 
*} 

11174  278 

279 

10603  280 
end 