src/CTT/Arith.thy
changeset 19761 5cd82054c2c6
parent 17441 5b5feca0344a
child 19762 957bcf55c98f
     1.1 --- a/src/CTT/Arith.thy	Fri Jun 02 16:06:19 2006 +0200
     1.2 +++ b/src/CTT/Arith.thy	Fri Jun 02 18:15:38 2006 +0200
     1.3 @@ -4,16 +4,13 @@
     1.4      Copyright   1991  University of Cambridge
     1.5  *)
     1.6  
     1.7 -header {* Arithmetic operators and their definitions *}
     1.8 +header {* Elementary arithmetic *}
     1.9  
    1.10  theory Arith
    1.11  imports Bool
    1.12  begin
    1.13  
    1.14 -text {*
    1.15 -  Proves about elementary arithmetic: addition, multiplication, etc.
    1.16 -  Tests definitions and simplifier.
    1.17 -*}
    1.18 +subsection {* Arithmetic operators and their definitions *}
    1.19  
    1.20  consts
    1.21    "#+"  :: "[i,i]=>i"   (infixr 65)
    1.22 @@ -37,6 +34,426 @@
    1.23    mod_def:     "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
    1.24    div_def:     "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
    1.25  
    1.26 -ML {* use_legacy_bindings (the_context ()) *}
    1.27 +lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def
    1.28 +
    1.29 +
    1.30 +subsection {* Proofs about elementary arithmetic: addition, multiplication, etc. *}
    1.31 +
    1.32 +(** Addition *)
    1.33 +
    1.34 +(*typing of add: short and long versions*)
    1.35 +
    1.36 +lemma add_typing: "[| a:N;  b:N |] ==> a #+ b : N"
    1.37 +apply (unfold arith_defs)
    1.38 +apply (tactic "typechk_tac []")
    1.39 +done
    1.40 +
    1.41 +lemma add_typingL: "[| a=c:N;  b=d:N |] ==> a #+ b = c #+ d : N"
    1.42 +apply (unfold arith_defs)
    1.43 +apply (tactic "equal_tac []")
    1.44 +done
    1.45 +
    1.46 +
    1.47 +(*computation for add: 0 and successor cases*)
    1.48 +
    1.49 +lemma addC0: "b:N ==> 0 #+ b = b : N"
    1.50 +apply (unfold arith_defs)
    1.51 +apply (tactic "rew_tac []")
    1.52 +done
    1.53 +
    1.54 +lemma addC_succ: "[| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N"
    1.55 +apply (unfold arith_defs)
    1.56 +apply (tactic "rew_tac []")
    1.57 +done
    1.58 +
    1.59 +
    1.60 +(** Multiplication *)
    1.61 +
    1.62 +(*typing of mult: short and long versions*)
    1.63 +
    1.64 +lemma mult_typing: "[| a:N;  b:N |] ==> a #* b : N"
    1.65 +apply (unfold arith_defs)
    1.66 +apply (tactic {* typechk_tac [thm "add_typing"] *})
    1.67 +done
    1.68 +
    1.69 +lemma mult_typingL: "[| a=c:N;  b=d:N |] ==> a #* b = c #* d : N"
    1.70 +apply (unfold arith_defs)
    1.71 +apply (tactic {* equal_tac [thm "add_typingL"] *})
    1.72 +done
    1.73 +
    1.74 +(*computation for mult: 0 and successor cases*)
    1.75 +
    1.76 +lemma multC0: "b:N ==> 0 #* b = 0 : N"
    1.77 +apply (unfold arith_defs)
    1.78 +apply (tactic "rew_tac []")
    1.79 +done
    1.80 +
    1.81 +lemma multC_succ: "[| a:N;  b:N |] ==> succ(a) #* b = b #+ (a #* b) : N"
    1.82 +apply (unfold arith_defs)
    1.83 +apply (tactic "rew_tac []")
    1.84 +done
    1.85 +
    1.86 +
    1.87 +(** Difference *)
    1.88 +
    1.89 +(*typing of difference*)
    1.90 +
    1.91 +lemma diff_typing: "[| a:N;  b:N |] ==> a - b : N"
    1.92 +apply (unfold arith_defs)
    1.93 +apply (tactic "typechk_tac []")
    1.94 +done
    1.95 +
    1.96 +lemma diff_typingL: "[| a=c:N;  b=d:N |] ==> a - b = c - d : N"
    1.97 +apply (unfold arith_defs)
    1.98 +apply (tactic "equal_tac []")
    1.99 +done
   1.100 +
   1.101 +
   1.102 +(*computation for difference: 0 and successor cases*)
   1.103 +
   1.104 +lemma diffC0: "a:N ==> a - 0 = a : N"
   1.105 +apply (unfold arith_defs)
   1.106 +apply (tactic "rew_tac []")
   1.107 +done
   1.108 +
   1.109 +(*Note: rec(a, 0, %z w.z) is pred(a). *)
   1.110 +
   1.111 +lemma diff_0_eq_0: "b:N ==> 0 - b = 0 : N"
   1.112 +apply (unfold arith_defs)
   1.113 +apply (tactic {* NE_tac "b" 1 *})
   1.114 +apply (tactic "hyp_rew_tac []")
   1.115 +done
   1.116 +
   1.117 +
   1.118 +(*Essential to simplify FIRST!!  (Else we get a critical pair)
   1.119 +  succ(a) - succ(b) rewrites to   pred(succ(a) - b)  *)
   1.120 +lemma diff_succ_succ: "[| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N"
   1.121 +apply (unfold arith_defs)
   1.122 +apply (tactic "hyp_rew_tac []")
   1.123 +apply (tactic {* NE_tac "b" 1 *})
   1.124 +apply (tactic "hyp_rew_tac []")
   1.125 +done
   1.126 +
   1.127 +
   1.128 +subsection {* Simplification *}
   1.129 +
   1.130 +lemmas arith_typing_rls = add_typing mult_typing diff_typing
   1.131 +  and arith_congr_rls = add_typingL mult_typingL diff_typingL
   1.132 +lemmas congr_rls = arith_congr_rls intrL2_rls elimL_rls
   1.133 +
   1.134 +lemmas arithC_rls =
   1.135 +  addC0 addC_succ
   1.136 +  multC0 multC_succ
   1.137 +  diffC0 diff_0_eq_0 diff_succ_succ
   1.138 +
   1.139 +ML {*
   1.140 +
   1.141 +structure Arith_simp_data: TSIMP_DATA =
   1.142 +  struct
   1.143 +  val refl              = thm "refl_elem"
   1.144 +  val sym               = thm "sym_elem"
   1.145 +  val trans             = thm "trans_elem"
   1.146 +  val refl_red          = thm "refl_red"
   1.147 +  val trans_red         = thm "trans_red"
   1.148 +  val red_if_equal      = thm "red_if_equal"
   1.149 +  val default_rls       = thms "arithC_rls" @ thms "comp_rls"
   1.150 +  val routine_tac       = routine_tac (thms "arith_typing_rls" @ thms "routine_rls")
   1.151 +  end
   1.152 +
   1.153 +structure Arith_simp = TSimpFun (Arith_simp_data)
   1.154 +
   1.155 +local val congr_rls = thms "congr_rls" in
   1.156 +
   1.157 +fun arith_rew_tac prems = make_rew_tac
   1.158 +    (Arith_simp.norm_tac(congr_rls, prems))
   1.159 +
   1.160 +fun hyp_arith_rew_tac prems = make_rew_tac
   1.161 +    (Arith_simp.cond_norm_tac(prove_cond_tac, congr_rls, prems))
   1.162  
   1.163  end
   1.164 +*}
   1.165 +
   1.166 +
   1.167 +subsection {* Addition *}
   1.168 +
   1.169 +(*Associative law for addition*)
   1.170 +lemma add_assoc: "[| a:N;  b:N;  c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N"
   1.171 +apply (tactic {* NE_tac "a" 1 *})
   1.172 +apply (tactic "hyp_arith_rew_tac []")
   1.173 +done
   1.174 +
   1.175 +
   1.176 +(*Commutative law for addition.  Can be proved using three inductions.
   1.177 +  Must simplify after first induction!  Orientation of rewrites is delicate*)
   1.178 +lemma add_commute: "[| a:N;  b:N |] ==> a #+ b = b #+ a : N"
   1.179 +apply (tactic {* NE_tac "a" 1 *})
   1.180 +apply (tactic "hyp_arith_rew_tac []")
   1.181 +apply (tactic {* NE_tac "b" 2 *})
   1.182 +apply (rule sym_elem)
   1.183 +apply (tactic {* NE_tac "b" 1 *})
   1.184 +apply (tactic "hyp_arith_rew_tac []")
   1.185 +done
   1.186 +
   1.187 +
   1.188 +subsection {* Multiplication *}
   1.189 +
   1.190 +(*right annihilation in product*)
   1.191 +lemma mult_0_right: "a:N ==> a #* 0 = 0 : N"
   1.192 +apply (tactic {* NE_tac "a" 1 *})
   1.193 +apply (tactic "hyp_arith_rew_tac []")
   1.194 +done
   1.195 +
   1.196 +(*right successor law for multiplication*)
   1.197 +lemma mult_succ_right: "[| a:N;  b:N |] ==> a #* succ(b) = a #+ (a #* b) : N"
   1.198 +apply (tactic {* NE_tac "a" 1 *})
   1.199 +apply (tactic {* hyp_arith_rew_tac [thm "add_assoc" RS thm "sym_elem"] *})
   1.200 +apply (assumption | rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+
   1.201 +done
   1.202 +
   1.203 +(*Commutative law for multiplication*)
   1.204 +lemma mult_commute: "[| a:N;  b:N |] ==> a #* b = b #* a : N"
   1.205 +apply (tactic {* NE_tac "a" 1 *})
   1.206 +apply (tactic {* hyp_arith_rew_tac [thm "mult_0_right", thm "mult_succ_right"] *})
   1.207 +done
   1.208 +
   1.209 +(*addition distributes over multiplication*)
   1.210 +lemma add_mult_distrib: "[| a:N;  b:N;  c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N"
   1.211 +apply (tactic {* NE_tac "a" 1 *})
   1.212 +apply (tactic {* hyp_arith_rew_tac [thm "add_assoc" RS thm "sym_elem"] *})
   1.213 +done
   1.214 +
   1.215 +(*Associative law for multiplication*)
   1.216 +lemma mult_assoc: "[| a:N;  b:N;  c:N |] ==> (a #* b) #* c = a #* (b #* c) : N"
   1.217 +apply (tactic {* NE_tac "a" 1 *})
   1.218 +apply (tactic {* hyp_arith_rew_tac [thm "add_mult_distrib"] *})
   1.219 +done
   1.220 +
   1.221 +
   1.222 +subsection {* Difference *}
   1.223 +
   1.224 +text {*
   1.225 +Difference on natural numbers, without negative numbers
   1.226 +  a - b = 0  iff  a<=b    a - b = succ(c) iff a>b   *}
   1.227 +
   1.228 +lemma diff_self_eq_0: "a:N ==> a - a = 0 : N"
   1.229 +apply (tactic {* NE_tac "a" 1 *})
   1.230 +apply (tactic "hyp_arith_rew_tac []")
   1.231 +done
   1.232 +
   1.233 +
   1.234 +lemma add_0_right: "[| c : N; 0 : N; c : N |] ==> c #+ 0 = c : N"
   1.235 +  by (rule addC0 [THEN [3] add_commute [THEN trans_elem]])
   1.236 +
   1.237 +(*Addition is the inverse of subtraction: if b<=x then b#+(x-b) = x.
   1.238 +  An example of induction over a quantified formula (a product).
   1.239 +  Uses rewriting with a quantified, implicative inductive hypothesis.*)
   1.240 +lemma add_diff_inverse_lemma: "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)"
   1.241 +apply (tactic {* NE_tac "b" 1 *})
   1.242 +(*strip one "universal quantifier" but not the "implication"*)
   1.243 +apply (rule_tac [3] intr_rls)
   1.244 +(*case analysis on x in
   1.245 +    (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *)
   1.246 +apply (tactic {* NE_tac "x" 4 *}, tactic "assume_tac 4")
   1.247 +(*Prepare for simplification of types -- the antecedent succ(u)<=x *)
   1.248 +apply (rule_tac [5] replace_type)
   1.249 +apply (rule_tac [4] replace_type)
   1.250 +apply (tactic "arith_rew_tac []")
   1.251 +(*Solves first 0 goal, simplifies others.  Two sugbgoals remain.
   1.252 +  Both follow by rewriting, (2) using quantified induction hyp*)
   1.253 +apply (tactic "intr_tac []") (*strips remaining PRODs*)
   1.254 +apply (tactic {* hyp_arith_rew_tac [thm "add_0_right"] *})
   1.255 +apply assumption
   1.256 +done
   1.257 +
   1.258 +
   1.259 +(*Version of above with premise   b-a=0   i.e.    a >= b.
   1.260 +  Using ProdE does not work -- for ?B(?a) is ambiguous.
   1.261 +  Instead, add_diff_inverse_lemma states the desired induction scheme
   1.262 +    the use of RS below instantiates Vars in ProdE automatically. *)
   1.263 +lemma add_diff_inverse: "[| a:N;  b:N;  b-a = 0 : N |] ==> b #+ (a-b) = a : N"
   1.264 +apply (rule EqE)
   1.265 +apply (rule add_diff_inverse_lemma [THEN ProdE, THEN ProdE])
   1.266 +apply (assumption | rule EqI)+
   1.267 +done
   1.268 +
   1.269 +
   1.270 +subsection {* Absolute difference *}
   1.271 +
   1.272 +(*typing of absolute difference: short and long versions*)
   1.273 +
   1.274 +lemma absdiff_typing: "[| a:N;  b:N |] ==> a |-| b : N"
   1.275 +apply (unfold arith_defs)
   1.276 +apply (tactic "typechk_tac []")
   1.277 +done
   1.278 +
   1.279 +lemma absdiff_typingL: "[| a=c:N;  b=d:N |] ==> a |-| b = c |-| d : N"
   1.280 +apply (unfold arith_defs)
   1.281 +apply (tactic "equal_tac []")
   1.282 +done
   1.283 +
   1.284 +lemma absdiff_self_eq_0: "a:N ==> a |-| a = 0 : N"
   1.285 +apply (unfold absdiff_def)
   1.286 +apply (tactic {* arith_rew_tac [thm "diff_self_eq_0"] *})
   1.287 +done
   1.288 +
   1.289 +lemma absdiffC0: "a:N ==> 0 |-| a = a : N"
   1.290 +apply (unfold absdiff_def)
   1.291 +apply (tactic "hyp_arith_rew_tac []")
   1.292 +done
   1.293 +
   1.294 +
   1.295 +lemma absdiff_succ_succ: "[| a:N;  b:N |] ==> succ(a) |-| succ(b)  =  a |-| b : N"
   1.296 +apply (unfold absdiff_def)
   1.297 +apply (tactic "hyp_arith_rew_tac []")
   1.298 +done
   1.299 +
   1.300 +(*Note how easy using commutative laws can be?  ...not always... *)
   1.301 +lemma absdiff_commute: "[| a:N;  b:N |] ==> a |-| b = b |-| a : N"
   1.302 +apply (unfold absdiff_def)
   1.303 +apply (rule add_commute)
   1.304 +apply (tactic {* typechk_tac [thm "diff_typing"] *})
   1.305 +done
   1.306 +
   1.307 +(*If a+b=0 then a=0.   Surprisingly tedious*)
   1.308 +lemma add_eq0_lemma: "[| a:N;  b:N |] ==> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)"
   1.309 +apply (tactic {* NE_tac "a" 1 *})
   1.310 +apply (rule_tac [3] replace_type)
   1.311 +apply (tactic "arith_rew_tac []")
   1.312 +apply (tactic "intr_tac []") (*strips remaining PRODs*)
   1.313 +apply (rule_tac [2] zero_ne_succ [THEN FE])
   1.314 +apply (erule_tac [3] EqE [THEN sym_elem])
   1.315 +apply (tactic {* typechk_tac [thm "add_typing"] *})
   1.316 +done
   1.317 +
   1.318 +(*Version of above with the premise  a+b=0.
   1.319 +  Again, resolution instantiates variables in ProdE *)
   1.320 +lemma add_eq0: "[| a:N;  b:N;  a #+ b = 0 : N |] ==> a = 0 : N"
   1.321 +apply (rule EqE)
   1.322 +apply (rule add_eq0_lemma [THEN ProdE])
   1.323 +apply (rule_tac [3] EqI)
   1.324 +apply (tactic "typechk_tac []")
   1.325 +done
   1.326 +
   1.327 +(*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
   1.328 +lemma absdiff_eq0_lem:
   1.329 +    "[| a:N;  b:N;  a |-| b = 0 : N |] ==>
   1.330 +     ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)"
   1.331 +apply (unfold absdiff_def)
   1.332 +apply (tactic "intr_tac []")
   1.333 +apply (tactic eqintr_tac)
   1.334 +apply (rule_tac [2] add_eq0)
   1.335 +apply (rule add_eq0)
   1.336 +apply (rule_tac [6] add_commute [THEN trans_elem])
   1.337 +apply (tactic {* typechk_tac [thm "diff_typing"] *})
   1.338 +done
   1.339 +
   1.340 +(*if  a |-| b = 0  then  a = b
   1.341 +  proof: a-b=0 and b-a=0, so b = a+(b-a) = a+0 = a*)
   1.342 +lemma absdiff_eq0: "[| a |-| b = 0 : N;  a:N;  b:N |] ==> a = b : N"
   1.343 +apply (rule EqE)
   1.344 +apply (rule absdiff_eq0_lem [THEN SumE])
   1.345 +apply (tactic "TRYALL assume_tac")
   1.346 +apply (tactic eqintr_tac)
   1.347 +apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem])
   1.348 +apply (rule_tac [3] EqE, tactic "assume_tac 3")
   1.349 +apply (tactic {* hyp_arith_rew_tac [thm "add_0_right"] *})
   1.350 +done
   1.351 +
   1.352 +
   1.353 +subsection {* Remainder and Quotient *}
   1.354 +
   1.355 +(*typing of remainder: short and long versions*)
   1.356 +
   1.357 +lemma mod_typing: "[| a:N;  b:N |] ==> a mod b : N"
   1.358 +apply (unfold mod_def)
   1.359 +apply (tactic {* typechk_tac [thm "absdiff_typing"] *})
   1.360 +done
   1.361 +
   1.362 +lemma mod_typingL: "[| a=c:N;  b=d:N |] ==> a mod b = c mod d : N"
   1.363 +apply (unfold mod_def)
   1.364 +apply (tactic {* equal_tac [thm "absdiff_typingL"] *})
   1.365 +done
   1.366 +
   1.367 +
   1.368 +(*computation for  mod : 0 and successor cases*)
   1.369 +
   1.370 +lemma modC0: "b:N ==> 0 mod b = 0 : N"
   1.371 +apply (unfold mod_def)
   1.372 +apply (tactic {* rew_tac [thm "absdiff_typing"] *})
   1.373 +done
   1.374 +
   1.375 +lemma modC_succ:
   1.376 +"[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N"
   1.377 +apply (unfold mod_def)
   1.378 +apply (tactic {* rew_tac [thm "absdiff_typing"] *})
   1.379 +done
   1.380 +
   1.381 +
   1.382 +(*typing of quotient: short and long versions*)
   1.383 +
   1.384 +lemma div_typing: "[| a:N;  b:N |] ==> a div b : N"
   1.385 +apply (unfold div_def)
   1.386 +apply (tactic {* typechk_tac [thm "absdiff_typing", thm "mod_typing"] *})
   1.387 +done
   1.388 +
   1.389 +lemma div_typingL: "[| a=c:N;  b=d:N |] ==> a div b = c div d : N"
   1.390 +apply (unfold div_def)
   1.391 +apply (tactic {* equal_tac [thm "absdiff_typingL", thm "mod_typingL"] *})
   1.392 +done
   1.393 +
   1.394 +lemmas div_typing_rls = mod_typing div_typing absdiff_typing
   1.395 +
   1.396 +
   1.397 +(*computation for quotient: 0 and successor cases*)
   1.398 +
   1.399 +lemma divC0: "b:N ==> 0 div b = 0 : N"
   1.400 +apply (unfold div_def)
   1.401 +apply (tactic {* rew_tac [thm "mod_typing", thm "absdiff_typing"] *})
   1.402 +done
   1.403 +
   1.404 +lemma divC_succ:
   1.405 + "[| a:N;  b:N |] ==> succ(a) div b =
   1.406 +     rec(succ(a) mod b, succ(a div b), %x y. a div b) : N"
   1.407 +apply (unfold div_def)
   1.408 +apply (tactic {* rew_tac [thm "mod_typing"] *})
   1.409 +done
   1.410 +
   1.411 +
   1.412 +(*Version of above with same condition as the  mod  one*)
   1.413 +lemma divC_succ2: "[| a:N;  b:N |] ==>
   1.414 +     succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N"
   1.415 +apply (rule divC_succ [THEN trans_elem])
   1.416 +apply (tactic {* rew_tac (thms "div_typing_rls" @ [thm "modC_succ"]) *})
   1.417 +apply (tactic {* NE_tac "succ (a mod b) |-|b" 1 *})
   1.418 +apply (tactic {* rew_tac [thm "mod_typing", thm "div_typing", thm "absdiff_typing"] *})
   1.419 +done
   1.420 +
   1.421 +(*for case analysis on whether a number is 0 or a successor*)
   1.422 +lemma iszero_decidable: "a:N ==> rec(a, inl(eq), %ka kb. inr(<ka, eq>)) :
   1.423 +                      Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
   1.424 +apply (tactic {* NE_tac "a" 1 *})
   1.425 +apply (rule_tac [3] PlusI_inr)
   1.426 +apply (rule_tac [2] PlusI_inl)
   1.427 +apply (tactic eqintr_tac)
   1.428 +apply (tactic "equal_tac []")
   1.429 +done
   1.430 +
   1.431 +(*Main Result.  Holds when b is 0 since   a mod 0 = a     and    a div 0 = 0  *)
   1.432 +lemma mod_div_equality: "[| a:N;  b:N |] ==> a mod b  #+  (a div b) #* b = a : N"
   1.433 +apply (tactic {* NE_tac "a" 1 *})
   1.434 +apply (tactic {* arith_rew_tac (thms "div_typing_rls" @
   1.435 +  [thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *})
   1.436 +apply (rule EqE)
   1.437 +(*case analysis on   succ(u mod b)|-|b  *)
   1.438 +apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE])
   1.439 +apply (erule_tac [3] SumE)
   1.440 +apply (tactic {* hyp_arith_rew_tac (thms "div_typing_rls" @
   1.441 +  [thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *})
   1.442 +(*Replace one occurence of  b  by succ(u mod b).  Clumsy!*)
   1.443 +apply (rule add_typingL [THEN trans_elem])
   1.444 +apply (erule EqE [THEN absdiff_eq0, THEN sym_elem])
   1.445 +apply (rule_tac [3] refl_elem)
   1.446 +apply (tactic {* hyp_arith_rew_tac (thms "div_typing_rls") *})
   1.447 +done
   1.448 +
   1.449 +end