src/CTT/Arith.thy
author blanchet
Mon May 19 23:43:53 2014 +0200 (2014-05-19)
changeset 57008 10f68b83b474
parent 39159 0dec18004e75
child 58318 f95754ca7082
permissions -rw-r--r--
use E 1.8's auto scheduler option
     1 (*  Title:      CTT/Arith.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1991  University of Cambridge
     4 *)
     5 
     6 header {* Elementary arithmetic *}
     7 
     8 theory Arith
     9 imports Bool
    10 begin
    11 
    12 subsection {* Arithmetic operators and their definitions *}
    13 
    14 definition
    15   add :: "[i,i]=>i"   (infixr "#+" 65) where
    16   "a#+b == rec(a, b, %u v. succ(v))"
    17 
    18 definition
    19   diff :: "[i,i]=>i"   (infixr "-" 65) where
    20   "a-b == rec(b, a, %u v. rec(v, 0, %x y. x))"
    21 
    22 definition
    23   absdiff :: "[i,i]=>i"   (infixr "|-|" 65) where
    24   "a|-|b == (a-b) #+ (b-a)"
    25 
    26 definition
    27   mult :: "[i,i]=>i"   (infixr "#*" 70) where
    28   "a#*b == rec(a, 0, %u v. b #+ v)"
    29 
    30 definition
    31   mod :: "[i,i]=>i"   (infixr "mod" 70) where
    32   "a mod b == rec(a, 0, %u v. rec(succ(v) |-| b, 0, %x y. succ(v)))"
    33 
    34 definition
    35   div :: "[i,i]=>i"   (infixr "div" 70) where
    36   "a div b == rec(a, 0, %u v. rec(succ(u) mod b, succ(v), %x y. v))"
    37 
    38 
    39 notation (xsymbols)
    40   mult  (infixr "#\<times>" 70)
    41 
    42 notation (HTML output)
    43   mult (infixr "#\<times>" 70)
    44 
    45 
    46 lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def
    47 
    48 
    49 subsection {* Proofs about elementary arithmetic: addition, multiplication, etc. *}
    50 
    51 (** Addition *)
    52 
    53 (*typing of add: short and long versions*)
    54 
    55 lemma add_typing: "[| a:N;  b:N |] ==> a #+ b : N"
    56 apply (unfold arith_defs)
    57 apply (tactic "typechk_tac []")
    58 done
    59 
    60 lemma add_typingL: "[| a=c:N;  b=d:N |] ==> a #+ b = c #+ d : N"
    61 apply (unfold arith_defs)
    62 apply (tactic "equal_tac []")
    63 done
    64 
    65 
    66 (*computation for add: 0 and successor cases*)
    67 
    68 lemma addC0: "b:N ==> 0 #+ b = b : N"
    69 apply (unfold arith_defs)
    70 apply (tactic "rew_tac []")
    71 done
    72 
    73 lemma addC_succ: "[| a:N;  b:N |] ==> succ(a) #+ b = succ(a #+ b) : N"
    74 apply (unfold arith_defs)
    75 apply (tactic "rew_tac []")
    76 done
    77 
    78 
    79 (** Multiplication *)
    80 
    81 (*typing of mult: short and long versions*)
    82 
    83 lemma mult_typing: "[| a:N;  b:N |] ==> a #* b : N"
    84 apply (unfold arith_defs)
    85 apply (tactic {* typechk_tac [@{thm add_typing}] *})
    86 done
    87 
    88 lemma mult_typingL: "[| a=c:N;  b=d:N |] ==> a #* b = c #* d : N"
    89 apply (unfold arith_defs)
    90 apply (tactic {* equal_tac [@{thm add_typingL}] *})
    91 done
    92 
    93 (*computation for mult: 0 and successor cases*)
    94 
    95 lemma multC0: "b:N ==> 0 #* b = 0 : N"
    96 apply (unfold arith_defs)
    97 apply (tactic "rew_tac []")
    98 done
    99 
   100 lemma multC_succ: "[| a:N;  b:N |] ==> succ(a) #* b = b #+ (a #* b) : N"
   101 apply (unfold arith_defs)
   102 apply (tactic "rew_tac []")
   103 done
   104 
   105 
   106 (** Difference *)
   107 
   108 (*typing of difference*)
   109 
   110 lemma diff_typing: "[| a:N;  b:N |] ==> a - b : N"
   111 apply (unfold arith_defs)
   112 apply (tactic "typechk_tac []")
   113 done
   114 
   115 lemma diff_typingL: "[| a=c:N;  b=d:N |] ==> a - b = c - d : N"
   116 apply (unfold arith_defs)
   117 apply (tactic "equal_tac []")
   118 done
   119 
   120 
   121 (*computation for difference: 0 and successor cases*)
   122 
   123 lemma diffC0: "a:N ==> a - 0 = a : N"
   124 apply (unfold arith_defs)
   125 apply (tactic "rew_tac []")
   126 done
   127 
   128 (*Note: rec(a, 0, %z w.z) is pred(a). *)
   129 
   130 lemma diff_0_eq_0: "b:N ==> 0 - b = 0 : N"
   131 apply (unfold arith_defs)
   132 apply (tactic {* NE_tac @{context} "b" 1 *})
   133 apply (tactic "hyp_rew_tac []")
   134 done
   135 
   136 
   137 (*Essential to simplify FIRST!!  (Else we get a critical pair)
   138   succ(a) - succ(b) rewrites to   pred(succ(a) - b)  *)
   139 lemma diff_succ_succ: "[| a:N;  b:N |] ==> succ(a) - succ(b) = a - b : N"
   140 apply (unfold arith_defs)
   141 apply (tactic "hyp_rew_tac []")
   142 apply (tactic {* NE_tac @{context} "b" 1 *})
   143 apply (tactic "hyp_rew_tac []")
   144 done
   145 
   146 
   147 subsection {* Simplification *}
   148 
   149 lemmas arith_typing_rls = add_typing mult_typing diff_typing
   150   and arith_congr_rls = add_typingL mult_typingL diff_typingL
   151 lemmas congr_rls = arith_congr_rls intrL2_rls elimL_rls
   152 
   153 lemmas arithC_rls =
   154   addC0 addC_succ
   155   multC0 multC_succ
   156   diffC0 diff_0_eq_0 diff_succ_succ
   157 
   158 ML {*
   159 
   160 structure Arith_simp_data: TSIMP_DATA =
   161   struct
   162   val refl              = @{thm refl_elem}
   163   val sym               = @{thm sym_elem}
   164   val trans             = @{thm trans_elem}
   165   val refl_red          = @{thm refl_red}
   166   val trans_red         = @{thm trans_red}
   167   val red_if_equal      = @{thm red_if_equal}
   168   val default_rls       = @{thms arithC_rls} @ @{thms comp_rls}
   169   val routine_tac       = routine_tac (@{thms arith_typing_rls} @ @{thms routine_rls})
   170   end
   171 
   172 structure Arith_simp = TSimpFun (Arith_simp_data)
   173 
   174 local val congr_rls = @{thms congr_rls} in
   175 
   176 fun arith_rew_tac prems = make_rew_tac
   177     (Arith_simp.norm_tac(congr_rls, prems))
   178 
   179 fun hyp_arith_rew_tac prems = make_rew_tac
   180     (Arith_simp.cond_norm_tac(prove_cond_tac, congr_rls, prems))
   181 
   182 end
   183 *}
   184 
   185 
   186 subsection {* Addition *}
   187 
   188 (*Associative law for addition*)
   189 lemma add_assoc: "[| a:N;  b:N;  c:N |] ==> (a #+ b) #+ c = a #+ (b #+ c) : N"
   190 apply (tactic {* NE_tac @{context} "a" 1 *})
   191 apply (tactic "hyp_arith_rew_tac []")
   192 done
   193 
   194 
   195 (*Commutative law for addition.  Can be proved using three inductions.
   196   Must simplify after first induction!  Orientation of rewrites is delicate*)
   197 lemma add_commute: "[| a:N;  b:N |] ==> a #+ b = b #+ a : N"
   198 apply (tactic {* NE_tac @{context} "a" 1 *})
   199 apply (tactic "hyp_arith_rew_tac []")
   200 apply (tactic {* NE_tac @{context} "b" 2 *})
   201 apply (rule sym_elem)
   202 apply (tactic {* NE_tac @{context} "b" 1 *})
   203 apply (tactic "hyp_arith_rew_tac []")
   204 done
   205 
   206 
   207 subsection {* Multiplication *}
   208 
   209 (*right annihilation in product*)
   210 lemma mult_0_right: "a:N ==> a #* 0 = 0 : N"
   211 apply (tactic {* NE_tac @{context} "a" 1 *})
   212 apply (tactic "hyp_arith_rew_tac []")
   213 done
   214 
   215 (*right successor law for multiplication*)
   216 lemma mult_succ_right: "[| a:N;  b:N |] ==> a #* succ(b) = a #+ (a #* b) : N"
   217 apply (tactic {* NE_tac @{context} "a" 1 *})
   218 apply (tactic {* hyp_arith_rew_tac [@{thm add_assoc} RS @{thm sym_elem}] *})
   219 apply (assumption | rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+
   220 done
   221 
   222 (*Commutative law for multiplication*)
   223 lemma mult_commute: "[| a:N;  b:N |] ==> a #* b = b #* a : N"
   224 apply (tactic {* NE_tac @{context} "a" 1 *})
   225 apply (tactic {* hyp_arith_rew_tac [@{thm mult_0_right}, @{thm mult_succ_right}] *})
   226 done
   227 
   228 (*addition distributes over multiplication*)
   229 lemma add_mult_distrib: "[| a:N;  b:N;  c:N |] ==> (a #+ b) #* c = (a #* c) #+ (b #* c) : N"
   230 apply (tactic {* NE_tac @{context} "a" 1 *})
   231 apply (tactic {* hyp_arith_rew_tac [@{thm add_assoc} RS @{thm sym_elem}] *})
   232 done
   233 
   234 (*Associative law for multiplication*)
   235 lemma mult_assoc: "[| a:N;  b:N;  c:N |] ==> (a #* b) #* c = a #* (b #* c) : N"
   236 apply (tactic {* NE_tac @{context} "a" 1 *})
   237 apply (tactic {* hyp_arith_rew_tac [@{thm add_mult_distrib}] *})
   238 done
   239 
   240 
   241 subsection {* Difference *}
   242 
   243 text {*
   244 Difference on natural numbers, without negative numbers
   245   a - b = 0  iff  a<=b    a - b = succ(c) iff a>b   *}
   246 
   247 lemma diff_self_eq_0: "a:N ==> a - a = 0 : N"
   248 apply (tactic {* NE_tac @{context} "a" 1 *})
   249 apply (tactic "hyp_arith_rew_tac []")
   250 done
   251 
   252 
   253 lemma add_0_right: "[| c : N; 0 : N; c : N |] ==> c #+ 0 = c : N"
   254   by (rule addC0 [THEN [3] add_commute [THEN trans_elem]])
   255 
   256 (*Addition is the inverse of subtraction: if b<=x then b#+(x-b) = x.
   257   An example of induction over a quantified formula (a product).
   258   Uses rewriting with a quantified, implicative inductive hypothesis.*)
   259 schematic_lemma add_diff_inverse_lemma:
   260   "b:N ==> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)"
   261 apply (tactic {* NE_tac @{context} "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 @{context} "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 schematic_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 @{context} "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 schematic_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 @{context} "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 @{context} "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 @{context} "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