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