author | wenzelm |
Sun, 12 Mar 2017 18:50:02 +0100 | |
changeset 65202 | 187277b77d50 |
parent 64980 | 7dc25cf5793e |
permissions | -rw-r--r-- |
17441 | 1 |
(* Title: CTT/Arith.thy |
1474 | 2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 3 |
Copyright 1991 University of Cambridge |
4 |
*) |
|
5 |
||
60770 | 6 |
section \<open>Elementary arithmetic\<close> |
17441 | 7 |
|
8 |
theory Arith |
|
63505 | 9 |
imports Bool |
17441 | 10 |
begin |
0 | 11 |
|
60770 | 12 |
subsection \<open>Arithmetic operators and their definitions\<close> |
17441 | 13 |
|
63505 | 14 |
definition add :: "[i,i]\<Rightarrow>i" (infixr "#+" 65) |
15 |
where "a#+b \<equiv> rec(a, b, \<lambda>u v. succ(v))" |
|
0 | 16 |
|
63505 | 17 |
definition diff :: "[i,i]\<Rightarrow>i" (infixr "-" 65) |
18 |
where "a-b \<equiv> rec(b, a, \<lambda>u v. rec(v, 0, \<lambda>x y. x))" |
|
19762 | 19 |
|
63505 | 20 |
definition absdiff :: "[i,i]\<Rightarrow>i" (infixr "|-|" 65) |
21 |
where "a|-|b \<equiv> (a-b) #+ (b-a)" |
|
19762 | 22 |
|
63505 | 23 |
definition mult :: "[i,i]\<Rightarrow>i" (infixr "#*" 70) |
24 |
where "a#*b \<equiv> rec(a, 0, \<lambda>u v. b #+ v)" |
|
10467
e6e7205e9e91
x-symbol support for Pi, Sigma, -->, : (membership)
paulson
parents:
3837
diff
changeset
|
25 |
|
63505 | 26 |
definition mod :: "[i,i]\<Rightarrow>i" (infixr "mod" 70) |
27 |
where "a mod b \<equiv> rec(a, 0, \<lambda>u v. rec(succ(v) |-| b, 0, \<lambda>x y. succ(v)))" |
|
19762 | 28 |
|
63505 | 29 |
definition div :: "[i,i]\<Rightarrow>i" (infixr "div" 70) |
30 |
where "a div b \<equiv> rec(a, 0, \<lambda>u v. rec(succ(u) mod b, succ(v), \<lambda>x y. v))" |
|
17441 | 31 |
|
19761 | 32 |
lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def |
33 |
||
34 |
||
60770 | 35 |
subsection \<open>Proofs about elementary arithmetic: addition, multiplication, etc.\<close> |
19761 | 36 |
|
63505 | 37 |
subsubsection \<open>Addition\<close> |
19761 | 38 |
|
63505 | 39 |
text \<open>Typing of \<open>add\<close>: short and long versions.\<close> |
19761 | 40 |
|
58977 | 41 |
lemma add_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #+ b : N" |
63505 | 42 |
unfolding arith_defs by typechk |
19761 | 43 |
|
58977 | 44 |
lemma add_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a #+ b = c #+ d : N" |
63505 | 45 |
unfolding arith_defs by equal |
19761 | 46 |
|
47 |
||
63505 | 48 |
text \<open>Computation for \<open>add\<close>: 0 and successor cases.\<close> |
19761 | 49 |
|
58977 | 50 |
lemma addC0: "b:N \<Longrightarrow> 0 #+ b = b : N" |
63505 | 51 |
unfolding arith_defs by rew |
19761 | 52 |
|
58977 | 53 |
lemma addC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) #+ b = succ(a #+ b) : N" |
63505 | 54 |
unfolding arith_defs by rew |
19761 | 55 |
|
56 |
||
63505 | 57 |
subsubsection \<open>Multiplication\<close> |
19761 | 58 |
|
63505 | 59 |
text \<open>Typing of \<open>mult\<close>: short and long versions.\<close> |
19761 | 60 |
|
58977 | 61 |
lemma mult_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #* b : N" |
63505 | 62 |
unfolding arith_defs by (typechk add_typing) |
19761 | 63 |
|
58977 | 64 |
lemma mult_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a #* b = c #* d : N" |
63505 | 65 |
unfolding arith_defs by (equal add_typingL) |
19761 | 66 |
|
63505 | 67 |
|
68 |
text \<open>Computation for \<open>mult\<close>: 0 and successor cases.\<close> |
|
19761 | 69 |
|
58977 | 70 |
lemma multC0: "b:N \<Longrightarrow> 0 #* b = 0 : N" |
63505 | 71 |
unfolding arith_defs by rew |
19761 | 72 |
|
58977 | 73 |
lemma multC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) #* b = b #+ (a #* b) : N" |
63505 | 74 |
unfolding arith_defs by rew |
19761 | 75 |
|
76 |
||
63505 | 77 |
subsubsection \<open>Difference\<close> |
19761 | 78 |
|
63505 | 79 |
text \<open>Typing of difference.\<close> |
19761 | 80 |
|
58977 | 81 |
lemma diff_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a - b : N" |
63505 | 82 |
unfolding arith_defs by typechk |
19761 | 83 |
|
58977 | 84 |
lemma diff_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a - b = c - d : N" |
63505 | 85 |
unfolding arith_defs by equal |
19761 | 86 |
|
87 |
||
63505 | 88 |
text \<open>Computation for difference: 0 and successor cases.\<close> |
19761 | 89 |
|
58977 | 90 |
lemma diffC0: "a:N \<Longrightarrow> a - 0 = a : N" |
63505 | 91 |
unfolding arith_defs by rew |
19761 | 92 |
|
63505 | 93 |
text \<open>Note: \<open>rec(a, 0, \<lambda>z w.z)\<close> is \<open>pred(a).\<close>\<close> |
19761 | 94 |
|
58977 | 95 |
lemma diff_0_eq_0: "b:N \<Longrightarrow> 0 - b = 0 : N" |
63505 | 96 |
unfolding arith_defs |
97 |
apply (NE b) |
|
98 |
apply hyp_rew |
|
99 |
done |
|
19761 | 100 |
|
63505 | 101 |
text \<open> |
102 |
Essential to simplify FIRST!! (Else we get a critical pair) |
|
103 |
\<open>succ(a) - succ(b)\<close> rewrites to \<open>pred(succ(a) - b)\<close>. |
|
104 |
\<close> |
|
58977 | 105 |
lemma diff_succ_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) - succ(b) = a - b : N" |
63505 | 106 |
unfolding arith_defs |
107 |
apply hyp_rew |
|
108 |
apply (NE b) |
|
109 |
apply hyp_rew |
|
110 |
done |
|
19761 | 111 |
|
112 |
||
60770 | 113 |
subsection \<open>Simplification\<close> |
19761 | 114 |
|
115 |
lemmas arith_typing_rls = add_typing mult_typing diff_typing |
|
116 |
and arith_congr_rls = add_typingL mult_typingL diff_typingL |
|
63505 | 117 |
|
19761 | 118 |
lemmas congr_rls = arith_congr_rls intrL2_rls elimL_rls |
119 |
||
120 |
lemmas arithC_rls = |
|
121 |
addC0 addC_succ |
|
122 |
multC0 multC_succ |
|
123 |
diffC0 diff_0_eq_0 diff_succ_succ |
|
124 |
||
60770 | 125 |
ML \<open> |
63505 | 126 |
structure Arith_simp = TSimpFun( |
127 |
val refl = @{thm refl_elem} |
|
128 |
val sym = @{thm sym_elem} |
|
129 |
val trans = @{thm trans_elem} |
|
130 |
val refl_red = @{thm refl_red} |
|
131 |
val trans_red = @{thm trans_red} |
|
132 |
val red_if_equal = @{thm red_if_equal} |
|
133 |
val default_rls = @{thms arithC_rls comp_rls} |
|
134 |
val routine_tac = routine_tac @{thms arith_typing_rls routine_rls} |
|
135 |
) |
|
19761 | 136 |
|
63505 | 137 |
fun arith_rew_tac ctxt prems = |
138 |
make_rew_tac ctxt (Arith_simp.norm_tac ctxt (@{thms congr_rls}, prems)) |
|
19761 | 139 |
|
63505 | 140 |
fun hyp_arith_rew_tac ctxt prems = |
141 |
make_rew_tac ctxt |
|
142 |
(Arith_simp.cond_norm_tac ctxt (prove_cond_tac ctxt, @{thms congr_rls}, prems)) |
|
60770 | 143 |
\<close> |
19761 | 144 |
|
60770 | 145 |
method_setup arith_rew = \<open> |
58972 | 146 |
Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (arith_rew_tac ctxt ths)) |
60770 | 147 |
\<close> |
58972 | 148 |
|
60770 | 149 |
method_setup hyp_arith_rew = \<open> |
58972 | 150 |
Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (hyp_arith_rew_tac ctxt ths)) |
60770 | 151 |
\<close> |
58972 | 152 |
|
19761 | 153 |
|
60770 | 154 |
subsection \<open>Addition\<close> |
19761 | 155 |
|
63505 | 156 |
text \<open>Associative law for addition.\<close> |
58977 | 157 |
lemma add_assoc: "\<lbrakk>a:N; b:N; c:N\<rbrakk> \<Longrightarrow> (a #+ b) #+ c = a #+ (b #+ c) : N" |
63505 | 158 |
apply (NE a) |
159 |
apply hyp_arith_rew |
|
160 |
done |
|
19761 | 161 |
|
63505 | 162 |
text \<open>Commutative law for addition. Can be proved using three inductions. |
163 |
Must simplify after first induction! Orientation of rewrites is delicate.\<close> |
|
58977 | 164 |
lemma add_commute: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #+ b = b #+ a : N" |
63505 | 165 |
apply (NE a) |
166 |
apply hyp_arith_rew |
|
167 |
apply (rule sym_elem) |
|
168 |
prefer 2 |
|
169 |
apply (NE b) |
|
170 |
prefer 4 |
|
171 |
apply (NE b) |
|
172 |
apply hyp_arith_rew |
|
173 |
done |
|
19761 | 174 |
|
175 |
||
60770 | 176 |
subsection \<open>Multiplication\<close> |
19761 | 177 |
|
63505 | 178 |
text \<open>Right annihilation in product.\<close> |
58977 | 179 |
lemma mult_0_right: "a:N \<Longrightarrow> a #* 0 = 0 : N" |
63505 | 180 |
apply (NE a) |
181 |
apply hyp_arith_rew |
|
182 |
done |
|
19761 | 183 |
|
63505 | 184 |
text \<open>Right successor law for multiplication.\<close> |
58977 | 185 |
lemma mult_succ_right: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #* succ(b) = a #+ (a #* b) : N" |
63505 | 186 |
apply (NE a) |
187 |
apply (hyp_arith_rew add_assoc [THEN sym_elem]) |
|
188 |
apply (assumption | rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+ |
|
189 |
done |
|
19761 | 190 |
|
63505 | 191 |
text \<open>Commutative law for multiplication.\<close> |
58977 | 192 |
lemma mult_commute: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #* b = b #* a : N" |
63505 | 193 |
apply (NE a) |
194 |
apply (hyp_arith_rew mult_0_right mult_succ_right) |
|
195 |
done |
|
19761 | 196 |
|
63505 | 197 |
text \<open>Addition distributes over multiplication.\<close> |
58977 | 198 |
lemma add_mult_distrib: "\<lbrakk>a:N; b:N; c:N\<rbrakk> \<Longrightarrow> (a #+ b) #* c = (a #* c) #+ (b #* c) : N" |
63505 | 199 |
apply (NE a) |
200 |
apply (hyp_arith_rew add_assoc [THEN sym_elem]) |
|
201 |
done |
|
19761 | 202 |
|
63505 | 203 |
text \<open>Associative law for multiplication.\<close> |
58977 | 204 |
lemma mult_assoc: "\<lbrakk>a:N; b:N; c:N\<rbrakk> \<Longrightarrow> (a #* b) #* c = a #* (b #* c) : N" |
63505 | 205 |
apply (NE a) |
206 |
apply (hyp_arith_rew add_mult_distrib) |
|
207 |
done |
|
19761 | 208 |
|
209 |
||
60770 | 210 |
subsection \<open>Difference\<close> |
19761 | 211 |
|
60770 | 212 |
text \<open> |
63505 | 213 |
Difference on natural numbers, without negative numbers |
214 |
\<^item> \<open>a - b = 0\<close> iff \<open>a \<le> b\<close> |
|
215 |
\<^item> \<open>a - b = succ(c)\<close> iff \<open>a > b\<close> |
|
216 |
\<close> |
|
19761 | 217 |
|
58977 | 218 |
lemma diff_self_eq_0: "a:N \<Longrightarrow> a - a = 0 : N" |
63505 | 219 |
apply (NE a) |
220 |
apply hyp_arith_rew |
|
221 |
done |
|
19761 | 222 |
|
223 |
||
58977 | 224 |
lemma add_0_right: "\<lbrakk>c : N; 0 : N; c : N\<rbrakk> \<Longrightarrow> c #+ 0 = c : N" |
19761 | 225 |
by (rule addC0 [THEN [3] add_commute [THEN trans_elem]]) |
226 |
||
63505 | 227 |
text \<open> |
228 |
Addition is the inverse of subtraction: if \<open>b \<le> x\<close> then \<open>b #+ (x - b) = x\<close>. |
|
19761 | 229 |
An example of induction over a quantified formula (a product). |
63505 | 230 |
Uses rewriting with a quantified, implicative inductive hypothesis. |
231 |
\<close> |
|
61337 | 232 |
schematic_goal add_diff_inverse_lemma: |
61391 | 233 |
"b:N \<Longrightarrow> ?a : \<Prod>x:N. Eq(N, b-x, 0) \<longrightarrow> Eq(N, b #+ (x-b), x)" |
63505 | 234 |
apply (NE b) |
235 |
\<comment> \<open>strip one "universal quantifier" but not the "implication"\<close> |
|
236 |
apply (rule_tac [3] intr_rls) |
|
237 |
\<comment> \<open>case analysis on \<open>x\<close> in \<open>succ(u) \<le> x \<longrightarrow> succ(u) #+ (x - succ(u)) = x\<close>\<close> |
|
238 |
prefer 4 |
|
239 |
apply (NE x) |
|
240 |
apply assumption |
|
241 |
\<comment> \<open>Prepare for simplification of types -- the antecedent \<open>succ(u) \<le> x\<close>\<close> |
|
242 |
apply (rule_tac [2] replace_type) |
|
243 |
apply (rule_tac [1] replace_type) |
|
244 |
apply arith_rew |
|
245 |
\<comment> \<open>Solves first 0 goal, simplifies others. Two sugbgoals remain. |
|
246 |
Both follow by rewriting, (2) using quantified induction hyp.\<close> |
|
247 |
apply intr \<comment> \<open>strips remaining \<open>\<Prod>\<close>s\<close> |
|
248 |
apply (hyp_arith_rew add_0_right) |
|
249 |
apply assumption |
|
250 |
done |
|
19761 | 251 |
|
63505 | 252 |
text \<open> |
253 |
Version of above with premise \<open>b - a = 0\<close> i.e. \<open>a \<ge> b\<close>. |
|
254 |
Using @{thm ProdE} does not work -- for \<open>?B(?a)\<close> is ambiguous. |
|
255 |
Instead, @{thm add_diff_inverse_lemma} states the desired induction scheme; |
|
256 |
the use of \<open>THEN\<close> below instantiates Vars in @{thm ProdE} automatically. |
|
257 |
\<close> |
|
58977 | 258 |
lemma add_diff_inverse: "\<lbrakk>a:N; b:N; b - a = 0 : N\<rbrakk> \<Longrightarrow> b #+ (a-b) = a : N" |
63505 | 259 |
apply (rule EqE) |
260 |
apply (rule add_diff_inverse_lemma [THEN ProdE, THEN ProdE]) |
|
261 |
apply (assumption | rule EqI)+ |
|
262 |
done |
|
19761 | 263 |
|
264 |
||
60770 | 265 |
subsection \<open>Absolute difference\<close> |
19761 | 266 |
|
63505 | 267 |
text \<open>Typing of absolute difference: short and long versions.\<close> |
19761 | 268 |
|
58977 | 269 |
lemma absdiff_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a |-| b : N" |
63505 | 270 |
unfolding arith_defs by typechk |
19761 | 271 |
|
58977 | 272 |
lemma absdiff_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a |-| b = c |-| d : N" |
63505 | 273 |
unfolding arith_defs by equal |
19761 | 274 |
|
58977 | 275 |
lemma absdiff_self_eq_0: "a:N \<Longrightarrow> a |-| a = 0 : N" |
63505 | 276 |
unfolding absdiff_def by (arith_rew diff_self_eq_0) |
19761 | 277 |
|
58977 | 278 |
lemma absdiffC0: "a:N \<Longrightarrow> 0 |-| a = a : N" |
63505 | 279 |
unfolding absdiff_def by hyp_arith_rew |
19761 | 280 |
|
58977 | 281 |
lemma absdiff_succ_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) |-| succ(b) = a |-| b : N" |
63505 | 282 |
unfolding absdiff_def by hyp_arith_rew |
19761 | 283 |
|
63505 | 284 |
text \<open>Note how easy using commutative laws can be? ...not always...\<close> |
58977 | 285 |
lemma absdiff_commute: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a |-| b = b |-| a : N" |
63505 | 286 |
unfolding absdiff_def |
287 |
apply (rule add_commute) |
|
288 |
apply (typechk diff_typing) |
|
289 |
done |
|
19761 | 290 |
|
63505 | 291 |
text \<open>If \<open>a + b = 0\<close> then \<open>a = 0\<close>. Surprisingly tedious.\<close> |
64980 | 292 |
schematic_goal add_eq0_lemma: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> ?c : Eq(N,a#+b,0) \<longrightarrow> Eq(N,a,0)" |
63505 | 293 |
apply (NE a) |
294 |
apply (rule_tac [3] replace_type) |
|
295 |
apply arith_rew |
|
296 |
apply intr \<comment> \<open>strips remaining \<open>\<Prod>\<close>s\<close> |
|
297 |
apply (rule_tac [2] zero_ne_succ [THEN FE]) |
|
298 |
apply (erule_tac [3] EqE [THEN sym_elem]) |
|
299 |
apply (typechk add_typing) |
|
300 |
done |
|
19761 | 301 |
|
63505 | 302 |
text \<open> |
303 |
Version of above with the premise \<open>a + b = 0\<close>. |
|
304 |
Again, resolution instantiates variables in @{thm ProdE}. |
|
305 |
\<close> |
|
58977 | 306 |
lemma add_eq0: "\<lbrakk>a:N; b:N; a #+ b = 0 : N\<rbrakk> \<Longrightarrow> a = 0 : N" |
63505 | 307 |
apply (rule EqE) |
308 |
apply (rule add_eq0_lemma [THEN ProdE]) |
|
309 |
apply (rule_tac [3] EqI) |
|
310 |
apply typechk |
|
311 |
done |
|
19761 | 312 |
|
63505 | 313 |
text \<open>Here is a lemma to infer \<open>a - b = 0\<close> and \<open>b - a = 0\<close> from \<open>a |-| b = 0\<close>, below.\<close> |
61337 | 314 |
schematic_goal absdiff_eq0_lem: |
64980 | 315 |
"\<lbrakk>a:N; b:N; a |-| b = 0 : N\<rbrakk> \<Longrightarrow> ?a : Eq(N, a-b, 0) \<times> Eq(N, b-a, 0)" |
63505 | 316 |
apply (unfold absdiff_def) |
317 |
apply intr |
|
318 |
apply eqintr |
|
319 |
apply (rule_tac [2] add_eq0) |
|
320 |
apply (rule add_eq0) |
|
321 |
apply (rule_tac [6] add_commute [THEN trans_elem]) |
|
322 |
apply (typechk diff_typing) |
|
323 |
done |
|
19761 | 324 |
|
63505 | 325 |
text \<open>If \<open>a |-| b = 0\<close> then \<open>a = b\<close> |
326 |
proof: \<open>a - b = 0\<close> and \<open>b - a = 0\<close>, so \<open>b = a + (b - a) = a + 0 = a\<close>. |
|
327 |
\<close> |
|
58977 | 328 |
lemma absdiff_eq0: "\<lbrakk>a |-| b = 0 : N; a:N; b:N\<rbrakk> \<Longrightarrow> a = b : N" |
63505 | 329 |
apply (rule EqE) |
330 |
apply (rule absdiff_eq0_lem [THEN SumE]) |
|
331 |
apply eqintr |
|
332 |
apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem]) |
|
333 |
apply (erule_tac [3] EqE) |
|
334 |
apply (hyp_arith_rew add_0_right) |
|
335 |
done |
|
19761 | 336 |
|
337 |
||
60770 | 338 |
subsection \<open>Remainder and Quotient\<close> |
19761 | 339 |
|
63505 | 340 |
text \<open>Typing of remainder: short and long versions.\<close> |
19761 | 341 |
|
58977 | 342 |
lemma mod_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a mod b : N" |
63505 | 343 |
unfolding mod_def by (typechk absdiff_typing) |
19761 | 344 |
|
58977 | 345 |
lemma mod_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a mod b = c mod d : N" |
63505 | 346 |
unfolding mod_def by (equal absdiff_typingL) |
19761 | 347 |
|
348 |
||
63505 | 349 |
text \<open>Computation for \<open>mod\<close>: 0 and successor cases.\<close> |
19761 | 350 |
|
58977 | 351 |
lemma modC0: "b:N \<Longrightarrow> 0 mod b = 0 : N" |
63505 | 352 |
unfolding mod_def by (rew absdiff_typing) |
19761 | 353 |
|
58977 | 354 |
lemma modC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> |
355 |
succ(a) mod b = rec(succ(a mod b) |-| b, 0, \<lambda>x y. succ(a mod b)) : N" |
|
63505 | 356 |
unfolding mod_def by (rew absdiff_typing) |
19761 | 357 |
|
358 |
||
63505 | 359 |
text \<open>Typing of quotient: short and long versions.\<close> |
19761 | 360 |
|
58977 | 361 |
lemma div_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a div b : N" |
63505 | 362 |
unfolding div_def by (typechk absdiff_typing mod_typing) |
19761 | 363 |
|
58977 | 364 |
lemma div_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a div b = c div d : N" |
63505 | 365 |
unfolding div_def by (equal absdiff_typingL mod_typingL) |
19761 | 366 |
|
367 |
lemmas div_typing_rls = mod_typing div_typing absdiff_typing |
|
368 |
||
369 |
||
63505 | 370 |
text \<open>Computation for quotient: 0 and successor cases.\<close> |
19761 | 371 |
|
58977 | 372 |
lemma divC0: "b:N \<Longrightarrow> 0 div b = 0 : N" |
63505 | 373 |
unfolding div_def by (rew mod_typing absdiff_typing) |
19761 | 374 |
|
58977 | 375 |
lemma divC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> |
376 |
succ(a) div b = rec(succ(a) mod b, succ(a div b), \<lambda>x y. a div b) : N" |
|
63505 | 377 |
unfolding div_def by (rew mod_typing) |
19761 | 378 |
|
379 |
||
63505 | 380 |
text \<open>Version of above with same condition as the \<open>mod\<close> one.\<close> |
58977 | 381 |
lemma divC_succ2: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> |
382 |
succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), \<lambda>x y. a div b) : N" |
|
63505 | 383 |
apply (rule divC_succ [THEN trans_elem]) |
384 |
apply (rew div_typing_rls modC_succ) |
|
385 |
apply (NE "succ (a mod b) |-|b") |
|
386 |
apply (rew mod_typing div_typing absdiff_typing) |
|
387 |
done |
|
19761 | 388 |
|
63505 | 389 |
text \<open>For case analysis on whether a number is 0 or a successor.\<close> |
58977 | 390 |
lemma iszero_decidable: "a:N \<Longrightarrow> rec(a, inl(eq), \<lambda>ka kb. inr(<ka, eq>)) : |
63505 | 391 |
Eq(N,a,0) + (\<Sum>x:N. Eq(N,a, succ(x)))" |
392 |
apply (NE a) |
|
393 |
apply (rule_tac [3] PlusI_inr) |
|
394 |
apply (rule_tac [2] PlusI_inl) |
|
395 |
apply eqintr |
|
396 |
apply equal |
|
397 |
done |
|
19761 | 398 |
|
63505 | 399 |
text \<open>Main Result. Holds when \<open>b\<close> is 0 since \<open>a mod 0 = a\<close> and \<open>a div 0 = 0\<close>.\<close> |
58977 | 400 |
lemma mod_div_equality: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a mod b #+ (a div b) #* b = a : N" |
63505 | 401 |
apply (NE a) |
402 |
apply (arith_rew div_typing_rls modC0 modC_succ divC0 divC_succ2) |
|
403 |
apply (rule EqE) |
|
404 |
\<comment> \<open>case analysis on \<open>succ(u mod b) |-| b\<close>\<close> |
|
405 |
apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE]) |
|
406 |
apply (erule_tac [3] SumE) |
|
407 |
apply (hyp_arith_rew div_typing_rls modC0 modC_succ divC0 divC_succ2) |
|
408 |
\<comment> \<open>Replace one occurrence of \<open>b\<close> by \<open>succ(u mod b)\<close>. Clumsy!\<close> |
|
409 |
apply (rule add_typingL [THEN trans_elem]) |
|
410 |
apply (erule EqE [THEN absdiff_eq0, THEN sym_elem]) |
|
411 |
apply (rule_tac [3] refl_elem) |
|
412 |
apply (hyp_arith_rew div_typing_rls) |
|
413 |
done |
|
19761 | 414 |
|
415 |
end |