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