5 ML "Pretty.margin_default := 64"
6 ML "Thy_Output.indent := 0" (*we don't want 5 for listing theorems*)
10 numeric literals; default simprules; can re-orient
15 @{subgoals[display,indent=0,margin=65]}
19 consts h :: "nat \<Rightarrow> nat"
21 "h i = (if i = 3 then 2 else i)"
29 @{thm[display] numeral_0_eq_0[no_vars]}
30 \rulename{numeral_0_eq_0}
32 @{thm[display] numeral_1_eq_1[no_vars]}
33 \rulename{numeral_1_eq_1}
35 @{thm[display] add_2_eq_Suc[no_vars]}
36 \rulename{add_2_eq_Suc}
38 @{thm[display] add_2_eq_Suc'[no_vars]}
39 \rulename{add_2_eq_Suc'}
41 @{thm[display] add_assoc[no_vars]}
44 @{thm[display] add_commute[no_vars]}
45 \rulename{add_commute}
47 @{thm[display] add_left_commute[no_vars]}
48 \rulename{add_left_commute}
50 these form add_ac; similarly there is mult_ac
53 lemma "Suc(i + j*l*k + m*n) = f (n*m + i + k*j*l)"
55 @{subgoals[display,indent=0,margin=65]}
57 apply (simp add: add_ac mult_ac)
59 @{subgoals[display,indent=0,margin=65]}
65 @{thm[display] div_le_mono[no_vars]}
66 \rulename{div_le_mono}
68 @{thm[display] diff_mult_distrib[no_vars]}
69 \rulename{diff_mult_distrib}
71 @{thm[display] mod_mult_distrib[no_vars]}
72 \rulename{mod_mult_distrib}
74 @{thm[display] nat_diff_split[no_vars]}
75 \rulename{nat_diff_split}
79 lemma "(n - 1) * (n + 1) = n * n - (1::nat)"
80 apply (clarsimp split: nat_diff_split iff del: less_Suc0)
81 --{* @{subgoals[display,indent=0,margin=65]} *}
82 apply (subgoal_tac "n=0", force, arith)
86 lemma "(n - 2) * (n + 2) = n * n - (4::nat)"
87 apply (simp split: nat_diff_split, clarify)
88 --{* @{subgoals[display,indent=0,margin=65]} *}
89 apply (subgoal_tac "n=0 | n=1", force, arith)
93 @{thm[display] mod_if[no_vars]}
96 @{thm[display] mod_div_equality[no_vars]}
97 \rulename{mod_div_equality}
100 @{thm[display] div_mult1_eq[no_vars]}
101 \rulename{div_mult1_eq}
103 @{thm[display] mod_mult_right_eq[no_vars]}
104 \rulename{mod_mult_right_eq}
106 @{thm[display] div_mult2_eq[no_vars]}
107 \rulename{div_mult2_eq}
109 @{thm[display] mod_mult2_eq[no_vars]}
110 \rulename{mod_mult2_eq}
112 @{thm[display] div_mult_mult1[no_vars]}
113 \rulename{div_mult_mult1}
115 @{thm[display] div_by_0 [no_vars]}
118 @{thm[display] mod_by_0 [no_vars]}
121 @{thm[display] dvd_antisym[no_vars]}
122 \rulename{dvd_antisym}
124 @{thm[display] dvd_add[no_vars]}
127 For the integers, I'd list a few theorems that somehow involve negative
132 Division, remainder of negatives
135 @{thm[display] pos_mod_sign[no_vars]}
136 \rulename{pos_mod_sign}
138 @{thm[display] pos_mod_bound[no_vars]}
139 \rulename{pos_mod_bound}
141 @{thm[display] neg_mod_sign[no_vars]}
142 \rulename{neg_mod_sign}
144 @{thm[display] neg_mod_bound[no_vars]}
145 \rulename{neg_mod_bound}
147 @{thm[display] zdiv_zadd1_eq[no_vars]}
148 \rulename{zdiv_zadd1_eq}
150 @{thm[display] mod_add_eq[no_vars]}
151 \rulename{mod_add_eq}
153 @{thm[display] zdiv_zmult1_eq[no_vars]}
154 \rulename{zdiv_zmult1_eq}
156 @{thm[display] zmod_zmult1_eq[no_vars]}
157 \rulename{zmod_zmult1_eq}
159 @{thm[display] zdiv_zmult2_eq[no_vars]}
160 \rulename{zdiv_zmult2_eq}
162 @{thm[display] zmod_zmult2_eq[no_vars]}
163 \rulename{zmod_zmult2_eq}
166 lemma "abs (x+y) \<le> abs x + abs (y :: int)"
169 lemma "abs (2*x) = 2 * abs (x :: int)"
170 by (simp add: abs_if)
173 text {*Induction rules for the Integers
175 @{thm[display] int_ge_induct[no_vars]}
176 \rulename{int_ge_induct}
178 @{thm[display] int_gr_induct[no_vars]}
179 \rulename{int_gr_induct}
181 @{thm[display] int_le_induct[no_vars]}
182 \rulename{int_le_induct}
184 @{thm[display] int_less_induct[no_vars]}
185 \rulename{int_less_induct}
190 @{thm[display] dense[no_vars]}
193 @{thm[display] times_divide_eq_right[no_vars]}
194 \rulename{times_divide_eq_right}
196 @{thm[display] times_divide_eq_left[no_vars]}
197 \rulename{times_divide_eq_left}
199 @{thm[display] divide_divide_eq_right[no_vars]}
200 \rulename{divide_divide_eq_right}
202 @{thm[display] divide_divide_eq_left[no_vars]}
203 \rulename{divide_divide_eq_left}
205 @{thm[display] minus_divide_left[no_vars]}
206 \rulename{minus_divide_left}
208 @{thm[display] minus_divide_right[no_vars]}
209 \rulename{minus_divide_right}
211 This last NOT a simprule
213 @{thm[display] add_divide_distrib[no_vars]}
214 \rulename{add_divide_distrib}
217 lemma "3/4 < (7/8 :: real)"
220 lemma "P ((3/4) * (8/15 :: real))"
222 @{subgoals[display,indent=0,margin=65]}
226 @{subgoals[display,indent=0,margin=65]}
230 lemma "(3/4) * (8/15) < (x :: real)"
232 @{subgoals[display,indent=0,margin=65]}
236 @{subgoals[display,indent=0,margin=65]}
243 Requires a field, or else an ordered ring
245 @{thm[display] mult_eq_0_iff[no_vars]}
246 \rulename{mult_eq_0_iff}
248 @{thm[display] mult_cancel_right[no_vars]}
249 \rulename{mult_cancel_right}
251 @{thm[display] mult_cancel_left[no_vars]}
252 \rulename{mult_cancel_left}
256 effect of show sorts on the above
258 @{thm[display,show_sorts] mult_cancel_left[no_vars]}
259 \rulename{mult_cancel_left}
265 @{thm[display] abs_mult[no_vars]}
268 @{thm[display] abs_le_iff[no_vars]}
269 \rulename{abs_le_iff}
271 @{thm[display] abs_triangle_ineq[no_vars]}
272 \rulename{abs_triangle_ineq}
274 @{thm[display] power_add[no_vars]}
277 @{thm[display] power_mult[no_vars]}
278 \rulename{power_mult}
280 @{thm[display] power_abs[no_vars]}