src/CTT/Arith.thy
author wenzelm
Mon Feb 23 14:50:30 2015 +0100 (2015-02-23)
changeset 59564 fdc03c8daacc
parent 59498 50b60f501b05
child 60770 240563fbf41d
permissions -rw-r--r--
Goal.prove_multi is superseded by the fully general Goal.prove_common;
     1 (*  Title:      CTT/Arith.thy
     2     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     3     Copyright   1991  University of Cambridge
     4 *)
     5 
     6 section {* 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]\<Rightarrow>i"   (infixr "#+" 65) where
    16   "a#+b == rec(a, b, \<lambda>u v. succ(v))"
    17 
    18 definition
    19   diff :: "[i,i]\<Rightarrow>i"   (infixr "-" 65) where
    20   "a-b == rec(b, a, \<lambda>u v. rec(v, 0, \<lambda>x y. x))"
    21 
    22 definition
    23   absdiff :: "[i,i]\<Rightarrow>i"   (infixr "|-|" 65) where
    24   "a|-|b == (a-b) #+ (b-a)"
    25 
    26 definition
    27   mult :: "[i,i]\<Rightarrow>i"   (infixr "#*" 70) where
    28   "a#*b == rec(a, 0, \<lambda>u v. b #+ v)"
    29 
    30 definition
    31   mod :: "[i,i]\<Rightarrow>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]\<Rightarrow>i"   (infixr "div" 70) where
    36   "a div b == rec(a, 0, \<lambda>u v. rec(succ(u) mod b, succ(v), \<lambda>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: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #+ b : N"
    56 apply (unfold arith_defs)
    57 apply typechk
    58 done
    59 
    60 lemma add_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a #+ b = c #+ d : N"
    61 apply (unfold arith_defs)
    62 apply equal
    63 done
    64 
    65 
    66 (*computation for add: 0 and successor cases*)
    67 
    68 lemma addC0: "b:N \<Longrightarrow> 0 #+ b = b : N"
    69 apply (unfold arith_defs)
    70 apply rew
    71 done
    72 
    73 lemma addC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) #+ b = succ(a #+ b) : N"
    74 apply (unfold arith_defs)
    75 apply rew
    76 done
    77 
    78 
    79 (** Multiplication *)
    80 
    81 (*typing of mult: short and long versions*)
    82 
    83 lemma mult_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #* b : N"
    84 apply (unfold arith_defs)
    85 apply (typechk add_typing)
    86 done
    87 
    88 lemma mult_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a #* b = c #* d : N"
    89 apply (unfold arith_defs)
    90 apply (equal add_typingL)
    91 done
    92 
    93 (*computation for mult: 0 and successor cases*)
    94 
    95 lemma multC0: "b:N \<Longrightarrow> 0 #* b = 0 : N"
    96 apply (unfold arith_defs)
    97 apply rew
    98 done
    99 
   100 lemma multC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) #* b = b #+ (a #* b) : N"
   101 apply (unfold arith_defs)
   102 apply rew
   103 done
   104 
   105 
   106 (** Difference *)
   107 
   108 (*typing of difference*)
   109 
   110 lemma diff_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a - b : N"
   111 apply (unfold arith_defs)
   112 apply typechk
   113 done
   114 
   115 lemma diff_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a - b = c - d : N"
   116 apply (unfold arith_defs)
   117 apply equal
   118 done
   119 
   120 
   121 (*computation for difference: 0 and successor cases*)
   122 
   123 lemma diffC0: "a:N \<Longrightarrow> a - 0 = a : N"
   124 apply (unfold arith_defs)
   125 apply rew
   126 done
   127 
   128 (*Note: rec(a, 0, \<lambda>z w.z) is pred(a). *)
   129 
   130 lemma diff_0_eq_0: "b:N \<Longrightarrow> 0 - b = 0 : N"
   131 apply (unfold arith_defs)
   132 apply (NE b)
   133 apply hyp_rew
   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: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) - succ(b) = a - b : N"
   140 apply (unfold arith_defs)
   141 apply hyp_rew
   142 apply (NE b)
   143 apply hyp_rew
   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 ctxt prems = make_rew_tac ctxt
   177   (Arith_simp.norm_tac ctxt (congr_rls, prems))
   178 
   179 fun hyp_arith_rew_tac ctxt prems = make_rew_tac ctxt
   180   (Arith_simp.cond_norm_tac ctxt (prove_cond_tac ctxt, congr_rls, prems))
   181 
   182 end
   183 *}
   184 
   185 method_setup arith_rew = {*
   186   Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (arith_rew_tac ctxt ths))
   187 *}
   188 
   189 method_setup hyp_arith_rew = {*
   190   Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (hyp_arith_rew_tac ctxt ths))
   191 *}
   192 
   193 
   194 subsection {* Addition *}
   195 
   196 (*Associative law for addition*)
   197 lemma add_assoc: "\<lbrakk>a:N; b:N; c:N\<rbrakk> \<Longrightarrow> (a #+ b) #+ c = a #+ (b #+ c) : N"
   198 apply (NE a)
   199 apply hyp_arith_rew
   200 done
   201 
   202 
   203 (*Commutative law for addition.  Can be proved using three inductions.
   204   Must simplify after first induction!  Orientation of rewrites is delicate*)
   205 lemma add_commute: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #+ b = b #+ a : N"
   206 apply (NE a)
   207 apply hyp_arith_rew
   208 apply (rule sym_elem)
   209 prefer 2
   210 apply (NE b)
   211 prefer 4
   212 apply (NE b)
   213 apply hyp_arith_rew
   214 done
   215 
   216 
   217 subsection {* Multiplication *}
   218 
   219 (*right annihilation in product*)
   220 lemma mult_0_right: "a:N \<Longrightarrow> a #* 0 = 0 : N"
   221 apply (NE a)
   222 apply hyp_arith_rew
   223 done
   224 
   225 (*right successor law for multiplication*)
   226 lemma mult_succ_right: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #* succ(b) = a #+ (a #* b) : N"
   227 apply (NE a)
   228 apply (hyp_arith_rew add_assoc [THEN sym_elem])
   229 apply (assumption | rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+
   230 done
   231 
   232 (*Commutative law for multiplication*)
   233 lemma mult_commute: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #* b = b #* a : N"
   234 apply (NE a)
   235 apply (hyp_arith_rew mult_0_right mult_succ_right)
   236 done
   237 
   238 (*addition distributes over multiplication*)
   239 lemma add_mult_distrib: "\<lbrakk>a:N; b:N; c:N\<rbrakk> \<Longrightarrow> (a #+ b) #* c = (a #* c) #+ (b #* c) : N"
   240 apply (NE a)
   241 apply (hyp_arith_rew add_assoc [THEN sym_elem])
   242 done
   243 
   244 (*Associative law for multiplication*)
   245 lemma mult_assoc: "\<lbrakk>a:N; b:N; c:N\<rbrakk> \<Longrightarrow> (a #* b) #* c = a #* (b #* c) : N"
   246 apply (NE a)
   247 apply (hyp_arith_rew add_mult_distrib)
   248 done
   249 
   250 
   251 subsection {* Difference *}
   252 
   253 text {*
   254 Difference on natural numbers, without negative numbers
   255   a - b = 0  iff  a<=b    a - b = succ(c) iff a>b   *}
   256 
   257 lemma diff_self_eq_0: "a:N \<Longrightarrow> a - a = 0 : N"
   258 apply (NE a)
   259 apply hyp_arith_rew
   260 done
   261 
   262 
   263 lemma add_0_right: "\<lbrakk>c : N; 0 : N; c : N\<rbrakk> \<Longrightarrow> c #+ 0 = c : N"
   264   by (rule addC0 [THEN [3] add_commute [THEN trans_elem]])
   265 
   266 (*Addition is the inverse of subtraction: if b<=x then b#+(x-b) = x.
   267   An example of induction over a quantified formula (a product).
   268   Uses rewriting with a quantified, implicative inductive hypothesis.*)
   269 schematic_lemma add_diff_inverse_lemma:
   270   "b:N \<Longrightarrow> ?a : PROD x:N. Eq(N, b-x, 0) --> Eq(N, b #+ (x-b), x)"
   271 apply (NE b)
   272 (*strip one "universal quantifier" but not the "implication"*)
   273 apply (rule_tac [3] intr_rls)
   274 (*case analysis on x in
   275     (succ(u) <= x) --> (succ(u)#+(x-succ(u)) = x) *)
   276 prefer 4
   277 apply (NE x)
   278 apply assumption
   279 (*Prepare for simplification of types -- the antecedent succ(u)<=x *)
   280 apply (rule_tac [2] replace_type)
   281 apply (rule_tac [1] replace_type)
   282 apply arith_rew
   283 (*Solves first 0 goal, simplifies others.  Two sugbgoals remain.
   284   Both follow by rewriting, (2) using quantified induction hyp*)
   285 apply intr (*strips remaining PRODs*)
   286 apply (hyp_arith_rew add_0_right)
   287 apply assumption
   288 done
   289 
   290 
   291 (*Version of above with premise   b-a=0   i.e.    a >= b.
   292   Using ProdE does not work -- for ?B(?a) is ambiguous.
   293   Instead, add_diff_inverse_lemma states the desired induction scheme
   294     the use of RS below instantiates Vars in ProdE automatically. *)
   295 lemma add_diff_inverse: "\<lbrakk>a:N; b:N; b - a = 0 : N\<rbrakk> \<Longrightarrow> b #+ (a-b) = a : N"
   296 apply (rule EqE)
   297 apply (rule add_diff_inverse_lemma [THEN ProdE, THEN ProdE])
   298 apply (assumption | rule EqI)+
   299 done
   300 
   301 
   302 subsection {* Absolute difference *}
   303 
   304 (*typing of absolute difference: short and long versions*)
   305 
   306 lemma absdiff_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a |-| b : N"
   307 apply (unfold arith_defs)
   308 apply typechk
   309 done
   310 
   311 lemma absdiff_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a |-| b = c |-| d : N"
   312 apply (unfold arith_defs)
   313 apply equal
   314 done
   315 
   316 lemma absdiff_self_eq_0: "a:N \<Longrightarrow> a |-| a = 0 : N"
   317 apply (unfold absdiff_def)
   318 apply (arith_rew diff_self_eq_0)
   319 done
   320 
   321 lemma absdiffC0: "a:N \<Longrightarrow> 0 |-| a = a : N"
   322 apply (unfold absdiff_def)
   323 apply hyp_arith_rew
   324 done
   325 
   326 
   327 lemma absdiff_succ_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) |-| succ(b)  =  a |-| b : N"
   328 apply (unfold absdiff_def)
   329 apply hyp_arith_rew
   330 done
   331 
   332 (*Note how easy using commutative laws can be?  ...not always... *)
   333 lemma absdiff_commute: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a |-| b = b |-| a : N"
   334 apply (unfold absdiff_def)
   335 apply (rule add_commute)
   336 apply (typechk diff_typing)
   337 done
   338 
   339 (*If a+b=0 then a=0.   Surprisingly tedious*)
   340 schematic_lemma add_eq0_lemma: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> ?c : PROD u: Eq(N,a#+b,0) .  Eq(N,a,0)"
   341 apply (NE a)
   342 apply (rule_tac [3] replace_type)
   343 apply arith_rew
   344 apply intr (*strips remaining PRODs*)
   345 apply (rule_tac [2] zero_ne_succ [THEN FE])
   346 apply (erule_tac [3] EqE [THEN sym_elem])
   347 apply (typechk add_typing)
   348 done
   349 
   350 (*Version of above with the premise  a+b=0.
   351   Again, resolution instantiates variables in ProdE *)
   352 lemma add_eq0: "\<lbrakk>a:N; b:N; a #+ b = 0 : N\<rbrakk> \<Longrightarrow> a = 0 : N"
   353 apply (rule EqE)
   354 apply (rule add_eq0_lemma [THEN ProdE])
   355 apply (rule_tac [3] EqI)
   356 apply typechk
   357 done
   358 
   359 (*Here is a lemma to infer a-b=0 and b-a=0 from a|-|b=0, below. *)
   360 schematic_lemma absdiff_eq0_lem:
   361   "\<lbrakk>a:N; b:N; a |-| b = 0 : N\<rbrakk> \<Longrightarrow> ?a : SUM v: Eq(N, a-b, 0) . Eq(N, b-a, 0)"
   362 apply (unfold absdiff_def)
   363 apply intr
   364 apply eqintr
   365 apply (rule_tac [2] add_eq0)
   366 apply (rule add_eq0)
   367 apply (rule_tac [6] add_commute [THEN trans_elem])
   368 apply (typechk diff_typing)
   369 done
   370 
   371 (*if  a |-| b = 0  then  a = b
   372   proof: a-b=0 and b-a=0, so b = a+(b-a) = a+0 = a*)
   373 lemma absdiff_eq0: "\<lbrakk>a |-| b = 0 : N; a:N; b:N\<rbrakk> \<Longrightarrow> a = b : N"
   374 apply (rule EqE)
   375 apply (rule absdiff_eq0_lem [THEN SumE])
   376 apply eqintr
   377 apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem])
   378 apply (erule_tac [3] EqE)
   379 apply (hyp_arith_rew add_0_right)
   380 done
   381 
   382 
   383 subsection {* Remainder and Quotient *}
   384 
   385 (*typing of remainder: short and long versions*)
   386 
   387 lemma mod_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a mod b : N"
   388 apply (unfold mod_def)
   389 apply (typechk absdiff_typing)
   390 done
   391 
   392 lemma mod_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a mod b = c mod d : N"
   393 apply (unfold mod_def)
   394 apply (equal absdiff_typingL)
   395 done
   396 
   397 
   398 (*computation for  mod : 0 and successor cases*)
   399 
   400 lemma modC0: "b:N \<Longrightarrow> 0 mod b = 0 : N"
   401 apply (unfold mod_def)
   402 apply (rew absdiff_typing)
   403 done
   404 
   405 lemma modC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow>
   406   succ(a) mod b = rec(succ(a mod b) |-| b, 0, \<lambda>x y. succ(a mod b)) : N"
   407 apply (unfold mod_def)
   408 apply (rew absdiff_typing)
   409 done
   410 
   411 
   412 (*typing of quotient: short and long versions*)
   413 
   414 lemma div_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a div b : N"
   415 apply (unfold div_def)
   416 apply (typechk absdiff_typing mod_typing)
   417 done
   418 
   419 lemma div_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a div b = c div d : N"
   420 apply (unfold div_def)
   421 apply (equal absdiff_typingL mod_typingL)
   422 done
   423 
   424 lemmas div_typing_rls = mod_typing div_typing absdiff_typing
   425 
   426 
   427 (*computation for quotient: 0 and successor cases*)
   428 
   429 lemma divC0: "b:N \<Longrightarrow> 0 div b = 0 : N"
   430 apply (unfold div_def)
   431 apply (rew mod_typing absdiff_typing)
   432 done
   433 
   434 lemma divC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow>
   435   succ(a) div b = rec(succ(a) mod b, succ(a div b), \<lambda>x y. a div b) : N"
   436 apply (unfold div_def)
   437 apply (rew mod_typing)
   438 done
   439 
   440 
   441 (*Version of above with same condition as the  mod  one*)
   442 lemma divC_succ2: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow>
   443   succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), \<lambda>x y. a div b) : N"
   444 apply (rule divC_succ [THEN trans_elem])
   445 apply (rew div_typing_rls modC_succ)
   446 apply (NE "succ (a mod b) |-|b")
   447 apply (rew mod_typing div_typing absdiff_typing)
   448 done
   449 
   450 (*for case analysis on whether a number is 0 or a successor*)
   451 lemma iszero_decidable: "a:N \<Longrightarrow> rec(a, inl(eq), \<lambda>ka kb. inr(<ka, eq>)) :
   452                       Eq(N,a,0) + (SUM x:N. Eq(N,a, succ(x)))"
   453 apply (NE a)
   454 apply (rule_tac [3] PlusI_inr)
   455 apply (rule_tac [2] PlusI_inl)
   456 apply eqintr
   457 apply equal
   458 done
   459 
   460 (*Main Result.  Holds when b is 0 since   a mod 0 = a     and    a div 0 = 0  *)
   461 lemma mod_div_equality: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a mod b #+ (a div b) #* b = a : N"
   462 apply (NE a)
   463 apply (arith_rew div_typing_rls modC0 modC_succ divC0 divC_succ2)
   464 apply (rule EqE)
   465 (*case analysis on   succ(u mod b)|-|b  *)
   466 apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE])
   467 apply (erule_tac [3] SumE)
   468 apply (hyp_arith_rew div_typing_rls modC0 modC_succ divC0 divC_succ2)
   469 (*Replace one occurrence of  b  by succ(u mod b).  Clumsy!*)
   470 apply (rule add_typingL [THEN trans_elem])
   471 apply (erule EqE [THEN absdiff_eq0, THEN sym_elem])
   472 apply (rule_tac [3] refl_elem)
   473 apply (hyp_arith_rew div_typing_rls)
   474 done
   475 
   476 end