src/ZF/Arith.ML
 author clasohm Thu Sep 16 12:20:38 1993 +0200 (1993-09-16) changeset 0 a5a9c433f639 child 6 8ce8c4d13d4d permissions -rw-r--r--
Initial revision
```     1 (*  Title: 	ZF/arith.ML
```
```     2     ID:         \$Id\$
```
```     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
```
```     4     Copyright   1992  University of Cambridge
```
```     5
```
```     6 For arith.thy.  Arithmetic operators and their definitions
```
```     7
```
```     8 Proofs about elementary arithmetic: addition, multiplication, etc.
```
```     9
```
```    10 Could prove def_rec_0, def_rec_succ...
```
```    11 *)
```
```    12
```
```    13 open Arith;
```
```    14
```
```    15 (*"Difference" is subtraction of natural numbers.
```
```    16   There are no negative numbers; we have
```
```    17      m #- n = 0  iff  m<=n   and     m #- n = succ(k) iff m>n.
```
```    18   Also, rec(m, 0, %z w.z) is pred(m).
```
```    19 *)
```
```    20
```
```    21 (** rec -- better than nat_rec; the succ case has no type requirement! **)
```
```    22
```
```    23 val rec_trans = rec_def RS def_transrec RS trans;
```
```    24
```
```    25 goal Arith.thy "rec(0,a,b) = a";
```
```    26 by (rtac rec_trans 1);
```
```    27 by (rtac nat_case_0 1);
```
```    28 val rec_0 = result();
```
```    29
```
```    30 goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))";
```
```    31 val rec_ss = ZF_ss
```
```    32       addcongs (mk_typed_congs Arith.thy [("b", "[i,i]=>i")])
```
```    33       addrews [nat_case_succ, nat_succI];
```
```    34 by (rtac rec_trans 1);
```
```    35 by (SIMP_TAC rec_ss 1);
```
```    36 val rec_succ = result();
```
```    37
```
```    38 val major::prems = goal Arith.thy
```
```    39     "[| n: nat;  \
```
```    40 \       a: C(0);  \
```
```    41 \       !!m z. [| m: nat;  z: C(m) |] ==> b(m,z): C(succ(m))  \
```
```    42 \    |] ==> rec(n,a,b) : C(n)";
```
```    43 by (rtac (major RS nat_induct) 1);
```
```    44 by (ALLGOALS
```
```    45     (ASM_SIMP_TAC (ZF_ss addrews (prems@[rec_0,rec_succ]))));
```
```    46 val rec_type = result();
```
```    47
```
```    48 val prems = goalw Arith.thy [rec_def]
```
```    49     "[| n=n';  a=a';  !!m z. b(m,z)=b'(m,z)  \
```
```    50 \    |] ==> rec(n,a,b)=rec(n',a',b')";
```
```    51 by (SIMP_TAC (ZF_ss addcongs [transrec_cong,nat_case_cong]
```
```    52 		    addrews (prems RL [sym])) 1);
```
```    53 val rec_cong = result();
```
```    54
```
```    55 val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat];
```
```    56
```
```    57 val nat_ss = ZF_ss addcongs [nat_case_cong,rec_cong]
```
```    58 	       	   addrews ([rec_0,rec_succ] @ nat_typechecks);
```
```    59
```
```    60
```
```    61 (** Addition **)
```
```    62
```
```    63 val add_type = prove_goalw Arith.thy [add_def]
```
```    64     "[| m:nat;  n:nat |] ==> m #+ n : nat"
```
```    65  (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
```
```    66
```
```    67 val add_0 = prove_goalw Arith.thy [add_def]
```
```    68     "0 #+ n = n"
```
```    69  (fn _ => [ (rtac rec_0 1) ]);
```
```    70
```
```    71 val add_succ = prove_goalw Arith.thy [add_def]
```
```    72     "succ(m) #+ n = succ(m #+ n)"
```
```    73  (fn _=> [ (rtac rec_succ 1) ]);
```
```    74
```
```    75 (** Multiplication **)
```
```    76
```
```    77 val mult_type = prove_goalw Arith.thy [mult_def]
```
```    78     "[| m:nat;  n:nat |] ==> m #* n : nat"
```
```    79  (fn prems=>
```
```    80   [ (typechk_tac (prems@[add_type]@nat_typechecks@ZF_typechecks)) ]);
```
```    81
```
```    82 val mult_0 = prove_goalw Arith.thy [mult_def]
```
```    83     "0 #* n = 0"
```
```    84  (fn _ => [ (rtac rec_0 1) ]);
```
```    85
```
```    86 val mult_succ = prove_goalw Arith.thy [mult_def]
```
```    87     "succ(m) #* n = n #+ (m #* n)"
```
```    88  (fn _ => [ (rtac rec_succ 1) ]);
```
```    89
```
```    90 (** Difference **)
```
```    91
```
```    92 val diff_type = prove_goalw Arith.thy [diff_def]
```
```    93     "[| m:nat;  n:nat |] ==> m #- n : nat"
```
```    94  (fn prems=> [ (typechk_tac (prems@nat_typechecks@ZF_typechecks)) ]);
```
```    95
```
```    96 val diff_0 = prove_goalw Arith.thy [diff_def]
```
```    97     "m #- 0 = m"
```
```    98  (fn _ => [ (rtac rec_0 1) ]);
```
```    99
```
```   100 val diff_0_eq_0 = prove_goalw Arith.thy [diff_def]
```
```   101     "n:nat ==> 0 #- n = 0"
```
```   102  (fn [prem]=>
```
```   103   [ (rtac (prem RS nat_induct) 1),
```
```   104     (ALLGOALS (ASM_SIMP_TAC nat_ss)) ]);
```
```   105
```
```   106 (*Must simplify BEFORE the induction!!  (Else we get a critical pair)
```
```   107   succ(m) #- succ(n)   rewrites to   pred(succ(m) #- n)  *)
```
```   108 val diff_succ_succ = prove_goalw Arith.thy [diff_def]
```
```   109     "[| m:nat;  n:nat |] ==> succ(m) #- succ(n) = m #- n"
```
```   110  (fn prems=>
```
```   111   [ (ASM_SIMP_TAC (nat_ss addrews prems) 1),
```
```   112     (nat_ind_tac "n" prems 1),
```
```   113     (ALLGOALS (ASM_SIMP_TAC (nat_ss addrews prems))) ]);
```
```   114
```
```   115 val prems = goal Arith.thy
```
```   116     "[| m:nat;  n:nat |] ==> m #- n : succ(m)";
```
```   117 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
```
```   118 by (resolve_tac prems 1);
```
```   119 by (resolve_tac prems 1);
```
```   120 by (etac succE 3);
```
```   121 by (ALLGOALS
```
```   122     (ASM_SIMP_TAC
```
```   123      (nat_ss addrews (prems@[diff_0,diff_0_eq_0,diff_succ_succ]))));
```
```   124 val diff_leq = result();
```
```   125
```
```   126 (*** Simplification over add, mult, diff ***)
```
```   127
```
```   128 val arith_typechecks = [add_type, mult_type, diff_type];
```
```   129 val arith_rews = [add_0, add_succ,
```
```   130 		  mult_0, mult_succ,
```
```   131 		  diff_0, diff_0_eq_0, diff_succ_succ];
```
```   132
```
```   133 val arith_congs = mk_congs Arith.thy ["op #+", "op #-", "op #*"];
```
```   134
```
```   135 val arith_ss = nat_ss addcongs arith_congs
```
```   136                       addrews  (arith_rews@arith_typechecks);
```
```   137
```
```   138 (*** Addition ***)
```
```   139
```
```   140 (*Associative law for addition*)
```
```   141 val add_assoc = prove_goal Arith.thy
```
```   142     "m:nat ==> (m #+ n) #+ k = m #+ (n #+ k)"
```
```   143  (fn prems=>
```
```   144   [ (nat_ind_tac "m" prems 1),
```
```   145     (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
```
```   146
```
```   147 (*The following two lemmas are used for add_commute and sometimes
```
```   148   elsewhere, since they are safe for rewriting.*)
```
```   149 val add_0_right = prove_goal Arith.thy
```
```   150     "m:nat ==> m #+ 0 = m"
```
```   151  (fn prems=>
```
```   152   [ (nat_ind_tac "m" prems 1),
```
```   153     (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
```
```   154
```
```   155 val add_succ_right = prove_goal Arith.thy
```
```   156     "m:nat ==> m #+ succ(n) = succ(m #+ n)"
```
```   157  (fn prems=>
```
```   158   [ (nat_ind_tac "m" prems 1),
```
```   159     (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
```
```   160
```
```   161 (*Commutative law for addition*)
```
```   162 val add_commute = prove_goal Arith.thy
```
```   163     "[| m:nat;  n:nat |] ==> m #+ n = n #+ m"
```
```   164  (fn prems=>
```
```   165   [ (nat_ind_tac "n" prems 1),
```
```   166     (ALLGOALS
```
```   167      (ASM_SIMP_TAC
```
```   168       (arith_ss addrews (prems@[add_0_right, add_succ_right])))) ]);
```
```   169
```
```   170 (*Cancellation law on the left*)
```
```   171 val [knat,eqn] = goal Arith.thy
```
```   172     "[| k:nat;  k #+ m = k #+ n |] ==> m=n";
```
```   173 by (rtac (eqn RS rev_mp) 1);
```
```   174 by (nat_ind_tac "k" [knat] 1);
```
```   175 by (ALLGOALS (SIMP_TAC arith_ss));
```
```   176 by (fast_tac ZF_cs 1);
```
```   177 val add_left_cancel = result();
```
```   178
```
```   179 (*** Multiplication ***)
```
```   180
```
```   181 (*right annihilation in product*)
```
```   182 val mult_0_right = prove_goal Arith.thy
```
```   183     "m:nat ==> m #* 0 = 0"
```
```   184  (fn prems=>
```
```   185   [ (nat_ind_tac "m" prems 1),
```
```   186     (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems)))  ]);
```
```   187
```
```   188 (*right successor law for multiplication*)
```
```   189 val mult_succ_right = prove_goal Arith.thy
```
```   190     "[| m:nat;  n:nat |] ==> m #* succ(n) = m #+ (m #* n)"
```
```   191  (fn prems=>
```
```   192   [ (nat_ind_tac "m" prems 1),
```
```   193     (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))),
```
```   194        (*The final goal requires the commutative law for addition*)
```
```   195     (REPEAT (ares_tac (prems@[refl,add_commute]@ZF_congs@arith_congs) 1))  ]);
```
```   196
```
```   197 (*Commutative law for multiplication*)
```
```   198 val mult_commute = prove_goal Arith.thy
```
```   199     "[| m:nat;  n:nat |] ==> m #* n = n #* m"
```
```   200  (fn prems=>
```
```   201   [ (nat_ind_tac "m" prems 1),
```
```   202     (ALLGOALS (ASM_SIMP_TAC
```
```   203 	       (arith_ss addrews (prems@[mult_0_right, mult_succ_right])))) ]);
```
```   204
```
```   205 (*addition distributes over multiplication*)
```
```   206 val add_mult_distrib = prove_goal Arith.thy
```
```   207     "[| m:nat;  k:nat |] ==> (m #+ n) #* k = (m #* k) #+ (n #* k)"
```
```   208  (fn prems=>
```
```   209   [ (nat_ind_tac "m" prems 1),
```
```   210     (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews ([add_assoc RS sym]@prems)))) ]);
```
```   211
```
```   212 (*Distributive law on the left; requires an extra typing premise*)
```
```   213 val add_mult_distrib_left = prove_goal Arith.thy
```
```   214     "[| m:nat;  n:nat;  k:nat |] ==> k #* (m #+ n) = (k #* m) #+ (k #* n)"
```
```   215  (fn prems=>
```
```   216       let val mult_commute' = read_instantiate [("m","k")] mult_commute
```
```   217           val ss = arith_ss addrews ([mult_commute',add_mult_distrib]@prems)
```
```   218       in [ (SIMP_TAC ss 1) ]
```
```   219       end);
```
```   220
```
```   221 (*Associative law for multiplication*)
```
```   222 val mult_assoc = prove_goal Arith.thy
```
```   223     "[| m:nat;  n:nat;  k:nat |] ==> (m #* n) #* k = m #* (n #* k)"
```
```   224  (fn prems=>
```
```   225   [ (nat_ind_tac "m" prems 1),
```
```   226     (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews (prems@[add_mult_distrib])))) ]);
```
```   227
```
```   228
```
```   229 (*** Difference ***)
```
```   230
```
```   231 val diff_self_eq_0 = prove_goal Arith.thy
```
```   232     "m:nat ==> m #- m = 0"
```
```   233  (fn prems=>
```
```   234   [ (nat_ind_tac "m" prems 1),
```
```   235     (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews prems))) ]);
```
```   236
```
```   237 (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
```
```   238 val notless::prems = goal Arith.thy
```
```   239     "[| ~m:n;  m:nat;  n:nat |] ==> n #+ (m#-n) = m";
```
```   240 by (rtac (notless RS rev_mp) 1);
```
```   241 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
```
```   242 by (resolve_tac prems 1);
```
```   243 by (resolve_tac prems 1);
```
```   244 by (ALLGOALS (ASM_SIMP_TAC
```
```   245 	      (arith_ss addrews (prems@[succ_mem_succ_iff, Ord_0_mem_succ,
```
```   246 				  naturals_are_ordinals]))));
```
```   247 val add_diff_inverse = result();
```
```   248
```
```   249
```
```   250 (*Subtraction is the inverse of addition. *)
```
```   251 val [mnat,nnat] = goal Arith.thy
```
```   252     "[| m:nat;  n:nat |] ==> (n#+m) #-n = m";
```
```   253 by (rtac (nnat RS nat_induct) 1);
```
```   254 by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat])));
```
```   255 val diff_add_inverse = result();
```
```   256
```
```   257 val [mnat,nnat] = goal Arith.thy
```
```   258     "[| m:nat;  n:nat |] ==> n #- (n#+m) = 0";
```
```   259 by (rtac (nnat RS nat_induct) 1);
```
```   260 by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mnat])));
```
```   261 val diff_add_0 = result();
```
```   262
```
```   263
```
```   264 (*** Remainder ***)
```
```   265
```
```   266 (*In ordinary notation: if 0<n and n<=m then m-n < m *)
```
```   267 val prems = goal Arith.thy
```
```   268     "[| 0:n; ~ m:n;  m:nat;  n:nat |] ==> m #- n : m";
```
```   269 by (cut_facts_tac prems 1);
```
```   270 by (etac rev_mp 1);
```
```   271 by (etac rev_mp 1);
```
```   272 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
```
```   273 by (resolve_tac prems 1);
```
```   274 by (resolve_tac prems 1);
```
```   275 by (ALLGOALS (ASM_SIMP_TAC
```
```   276 	      (nat_ss addrews (prems@[diff_leq,diff_succ_succ]))));
```
```   277 val div_termination = result();
```
```   278
```
```   279 val div_rls =
```
```   280     [Ord_transrec_type, apply_type, div_termination, if_type] @
```
```   281     nat_typechecks;
```
```   282
```
```   283 (*Type checking depends upon termination!*)
```
```   284 val prems = goalw Arith.thy [mod_def]
```
```   285     "[| 0:n;  m:nat;  n:nat |] ==> m mod n : nat";
```
```   286 by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
```
```   287 val mod_type = result();
```
```   288
```
```   289 val div_ss = ZF_ss addrews [naturals_are_ordinals,div_termination];
```
```   290
```
```   291 val prems = goal Arith.thy "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m mod n = m";
```
```   292 by (rtac (mod_def RS def_transrec RS trans) 1);
```
```   293 by (SIMP_TAC (div_ss addrews prems) 1);
```
```   294 val mod_less = result();
```
```   295
```
```   296 val prems = goal Arith.thy
```
```   297     "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m mod n = (m#-n) mod n";
```
```   298 by (rtac (mod_def RS def_transrec RS trans) 1);
```
```   299 by (SIMP_TAC (div_ss addrews prems) 1);
```
```   300 val mod_geq = result();
```
```   301
```
```   302 (*** Quotient ***)
```
```   303
```
```   304 (*Type checking depends upon termination!*)
```
```   305 val prems = goalw Arith.thy [div_def]
```
```   306     "[| 0:n;  m:nat;  n:nat |] ==> m div n : nat";
```
```   307 by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
```
```   308 val div_type = result();
```
```   309
```
```   310 val prems = goal Arith.thy
```
```   311     "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m div n = 0";
```
```   312 by (rtac (div_def RS def_transrec RS trans) 1);
```
```   313 by (SIMP_TAC (div_ss addrews prems) 1);
```
```   314 val div_less = result();
```
```   315
```
```   316 val prems = goal Arith.thy
```
```   317     "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m div n = succ((m#-n) div n)";
```
```   318 by (rtac (div_def RS def_transrec RS trans) 1);
```
```   319 by (SIMP_TAC (div_ss addrews prems) 1);
```
```   320 val div_geq = result();
```
```   321
```
```   322 (*Main Result.*)
```
```   323 val prems = goal Arith.thy
```
```   324     "[| 0:n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m";
```
```   325 by (res_inst_tac [("i","m")] complete_induct 1);
```
```   326 by (resolve_tac prems 1);
```
```   327 by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1);
```
```   328 by (ALLGOALS
```
```   329     (ASM_SIMP_TAC
```
```   330      (arith_ss addrews ([mod_type,div_type] @ prems @
```
```   331         [mod_less,mod_geq, div_less, div_geq,
```
```   332 	 add_assoc, add_diff_inverse, div_termination]))));
```
```   333 val mod_div_equality = result();
```
```   334
```
```   335
```
```   336 (**** Additional theorems about "less than" ****)
```
```   337
```
```   338 val [mnat,nnat] = goal Arith.thy
```
```   339     "[| m:nat;  n:nat |] ==> ~ (m #+ n) : n";
```
```   340 by (rtac (mnat RS nat_induct) 1);
```
```   341 by (ALLGOALS (ASM_SIMP_TAC (arith_ss addrews [mem_not_refl])));
```
```   342 by (rtac notI 1);
```
```   343 by (etac notE 1);
```
```   344 by (etac (succI1 RS Ord_trans) 1);
```
```   345 by (rtac (nnat RS naturals_are_ordinals) 1);
```
```   346 val add_not_less_self = result();
```
```   347
```
```   348 val [mnat,nnat] = goal Arith.thy
```
```   349     "[| m:nat;  n:nat |] ==> m : succ(m #+ n)";
```
```   350 by (rtac (mnat RS nat_induct) 1);
```
```   351 (*May not simplify even with ZF_ss because it would expand m:succ(...) *)
```
```   352 by (rtac (add_0 RS ssubst) 1);
```
```   353 by (rtac (add_succ RS ssubst) 2);
```
```   354 by (REPEAT (ares_tac [nnat, Ord_0_mem_succ, succ_mem_succI,
```
```   355 		      naturals_are_ordinals, nat_succI, add_type] 1));
```
```   356 val add_less_succ_self = result();
```