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