src/ZF/arith.ML
changeset 25 3ac1c0c0016e
parent 14 1c0926788772
child 127 eec6bb9c58ea
equal deleted inserted replaced
24:f3d4ff75d9f2 25:3ac1c0c0016e
    40 by (rtac (major RS nat_induct) 1);
    40 by (rtac (major RS nat_induct) 1);
    41 by (ALLGOALS
    41 by (ALLGOALS
    42     (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
    42     (asm_simp_tac (ZF_ss addsimps (prems@[rec_0,rec_succ]))));
    43 val rec_type = result();
    43 val rec_type = result();
    44 
    44 
    45 val nat_typechecks = [rec_type,nat_0I,nat_1I,nat_succI,Ord_nat];
    45 val nat_le_refl = naturals_are_ordinals RS le_refl;
    46 
    46 
    47 val nat_ss = ZF_ss addsimps ([rec_0,rec_succ] @ nat_typechecks);
    47 val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat];
       
    48 
       
    49 val nat_simps = [rec_0, rec_succ, not_lt0, nat_0_le, le0_iff, succ_le_iff,
       
    50 		 nat_le_refl];
       
    51 
       
    52 val nat_ss = ZF_ss addsimps (nat_simps @ nat_typechecks);
    48 
    53 
    49 
    54 
    50 (** Addition **)
    55 (** Addition **)
    51 
    56 
    52 val add_type = prove_goalw Arith.thy [add_def]
    57 val add_type = prove_goalw Arith.thy [add_def]
    99  (fn prems=>
   104  (fn prems=>
   100   [ (asm_simp_tac (nat_ss addsimps prems) 1),
   105   [ (asm_simp_tac (nat_ss addsimps prems) 1),
   101     (nat_ind_tac "n" prems 1),
   106     (nat_ind_tac "n" prems 1),
   102     (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
   107     (ALLGOALS (asm_simp_tac (nat_ss addsimps prems))) ]);
   103 
   108 
   104 (*The conclusion is equivalent to m#-n <= m *)
       
   105 val prems = goal Arith.thy 
   109 val prems = goal Arith.thy 
   106     "[| m:nat;  n:nat |] ==> m #- n : succ(m)";
   110     "[| m:nat;  n:nat |] ==> m #- n le m";
   107 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   111 by (rtac (prems MRS diff_induct) 1);
   108 by (resolve_tac prems 1);
   112 by (etac leE 3);
   109 by (resolve_tac prems 1);
       
   110 by (etac succE 3);
       
   111 by (ALLGOALS
   113 by (ALLGOALS
   112     (asm_simp_tac
   114     (asm_simp_tac
   113      (nat_ss addsimps (prems @ [succ_iff, diff_0, diff_0_eq_0, 
   115      (nat_ss addsimps (prems @ [le_iff, diff_0, diff_0_eq_0, 
   114 				diff_succ_succ]))));
   116 				diff_succ_succ, naturals_are_ordinals]))));
   115 val diff_less_succ = result();
   117 val diff_le_self = result();
   116 
   118 
   117 (*** Simplification over add, mult, diff ***)
   119 (*** Simplification over add, mult, diff ***)
   118 
   120 
   119 val arith_typechecks = [add_type, mult_type, diff_type];
   121 val arith_typechecks = [add_type, mult_type, diff_type];
   120 val arith_rews = [add_0, add_succ,
   122 val arith_simps = [add_0, add_succ,
   121 		  mult_0, mult_succ,
   123 		   mult_0, mult_succ,
   122 		  diff_0, diff_0_eq_0, diff_succ_succ];
   124 		   diff_0, diff_0_eq_0, diff_succ_succ];
   123 
   125 
   124 val arith_ss = nat_ss addsimps (arith_rews@arith_typechecks);
   126 val arith_ss = nat_ss addsimps (arith_simps@arith_typechecks);
   125 
   127 
   126 (*** Addition ***)
   128 (*** Addition ***)
   127 
   129 
   128 (*Associative law for addition*)
   130 (*Associative law for addition*)
   129 val add_assoc = prove_goal Arith.thy 
   131 val add_assoc = prove_goal Arith.thy 
   221     "m:nat ==> m #- m = 0"
   223     "m:nat ==> m #- m = 0"
   222  (fn prems=>
   224  (fn prems=>
   223   [ (nat_ind_tac "m" prems 1),
   225   [ (nat_ind_tac "m" prems 1),
   224     (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
   226     (ALLGOALS (asm_simp_tac (arith_ss addsimps prems))) ]);
   225 
   227 
   226 (*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
   228 (*Addition is the inverse of subtraction*)
   227 val notless::prems = goal Arith.thy
   229 goal Arith.thy "!!m n. [| n le m;  m:nat |] ==> n #+ (m#-n) = m";
   228     "[| ~m:n;  m:nat;  n:nat |] ==> n #+ (m#-n) = m";
   230 by (forward_tac [lt_nat_in_nat] 1);
   229 by (rtac (notless RS rev_mp) 1);
   231 be nat_succI 1;
       
   232 by (etac rev_mp 1);
   230 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   233 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   231 by (resolve_tac prems 1);
   234 by (ALLGOALS (asm_simp_tac arith_ss));
   232 by (resolve_tac prems 1);
       
   233 by (ALLGOALS (asm_simp_tac
       
   234 	      (arith_ss addsimps (prems@[succ_mem_succ_iff, nat_0_in_succ,
       
   235 					 naturals_are_ordinals]))));
       
   236 val add_diff_inverse = result();
   235 val add_diff_inverse = result();
   237 
       
   238 
   236 
   239 (*Subtraction is the inverse of addition. *)
   237 (*Subtraction is the inverse of addition. *)
   240 val [mnat,nnat] = goal Arith.thy
   238 val [mnat,nnat] = goal Arith.thy
   241     "[| m:nat;  n:nat |] ==> (n#+m) #-n = m";
   239     "[| m:nat;  n:nat |] ==> (n#+m) #-n = m";
   242 by (rtac (nnat RS nat_induct) 1);
   240 by (rtac (nnat RS nat_induct) 1);
   250 val diff_add_0 = result();
   248 val diff_add_0 = result();
   251 
   249 
   252 
   250 
   253 (*** Remainder ***)
   251 (*** Remainder ***)
   254 
   252 
   255 (*In ordinary notation: if 0<n and n<=m then m-n < m *)
   253 goal Arith.thy "!!m n. [| 0<n;  n le m;  m:nat |] ==> m #- n < m";
   256 goal Arith.thy "!!m n. [| 0:n; ~ m:n;  m:nat;  n:nat |] ==> m #- n : m";
   254 by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
   257 by (etac rev_mp 1);
   255 by (etac rev_mp 1);
   258 by (etac rev_mp 1);
   256 by (etac rev_mp 1);
   259 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   257 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
   260 by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_less_succ,diff_succ_succ])));
   258 by (ALLGOALS (asm_simp_tac (nat_ss addsimps [diff_le_self,diff_succ_succ])));
   261 val div_termination = result();
   259 val div_termination = result();
   262 
   260 
   263 val div_rls =
   261 val div_rls =	(*for mod and div*)
   264     [Ord_transrec_type, apply_type, div_termination, if_type] @ 
   262     nat_typechecks @
   265     nat_typechecks;
   263     [Ord_transrec_type, apply_type, div_termination RS ltD, if_type,
       
   264      naturals_are_ordinals, not_lt_iff_le RS iffD1];
       
   265 
       
   266 val div_ss = ZF_ss addsimps [naturals_are_ordinals, div_termination RS ltD,
       
   267 			     not_lt_iff_le RS iffD2];
   266 
   268 
   267 (*Type checking depends upon termination!*)
   269 (*Type checking depends upon termination!*)
   268 val prems = goalw Arith.thy [mod_def]
   270 goalw Arith.thy [mod_def] "!!m n. [| 0<n;  m:nat;  n:nat |] ==> m mod n : nat";
   269     "[| 0:n;  m:nat;  n:nat |] ==> m mod n : nat";
   271 by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
   270 by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
       
   271 val mod_type = result();
   272 val mod_type = result();
   272 
   273 
   273 val div_ss = ZF_ss addsimps [naturals_are_ordinals,div_termination];
   274 goal Arith.thy "!!m n. [| 0<n;  m<n |] ==> m mod n = m";
   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);
   275 by (rtac (mod_def RS def_transrec RS trans) 1);
   277 by (simp_tac (div_ss addsimps prems) 1);
   276 by (asm_simp_tac div_ss 1);
   278 val mod_less = result();
   277 val mod_less = result();
   279 
   278 
   280 val prems = goal Arith.thy
   279 goal Arith.thy "!!m n. [| 0<n;  n le m;  m:nat |] ==> m mod n = (m#-n) mod n";
   281     "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m mod n = (m#-n) mod n";
   280 by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
   282 by (rtac (mod_def RS def_transrec RS trans) 1);
   281 by (rtac (mod_def RS def_transrec RS trans) 1);
   283 by (simp_tac (div_ss addsimps prems) 1);
   282 by (asm_simp_tac div_ss 1);
   284 val mod_geq = result();
   283 val mod_geq = result();
   285 
   284 
   286 (*** Quotient ***)
   285 (*** Quotient ***)
   287 
   286 
   288 (*Type checking depends upon termination!*)
   287 (*Type checking depends upon termination!*)
   289 val prems = goalw Arith.thy [div_def]
   288 goalw Arith.thy [div_def]
   290     "[| 0:n;  m:nat;  n:nat |] ==> m div n : nat";
   289     "!!m n. [| 0<n;  m:nat;  n:nat |] ==> m div n : nat";
   291 by (REPEAT (ares_tac (prems @ div_rls) 1 ORELSE etac Ord_trans 1));
   290 by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
   292 val div_type = result();
   291 val div_type = result();
   293 
   292 
   294 val prems = goal Arith.thy
   293 goal Arith.thy "!!m n. [| 0<n;  m<n |] ==> m div n = 0";
   295     "[| 0:n;  m:n;  m:nat;  n:nat |] ==> m div n = 0";
       
   296 by (rtac (div_def RS def_transrec RS trans) 1);
   294 by (rtac (div_def RS def_transrec RS trans) 1);
   297 by (simp_tac (div_ss addsimps prems) 1);
   295 by (asm_simp_tac div_ss 1);
   298 val div_less = result();
   296 val div_less = result();
   299 
   297 
   300 val prems = goal Arith.thy
   298 goal Arith.thy
   301     "[| 0:n;  ~m:n;  m:nat;  n:nat |] ==> m div n = succ((m#-n) div n)";
   299  "!!m n. [| 0<n;  n le m;  m:nat |] ==> m div n = succ((m#-n) div n)";
       
   300 by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
   302 by (rtac (div_def RS def_transrec RS trans) 1);
   301 by (rtac (div_def RS def_transrec RS trans) 1);
   303 by (simp_tac (div_ss addsimps prems) 1);
   302 by (asm_simp_tac div_ss 1);
   304 val div_geq = result();
   303 val div_geq = result();
   305 
   304 
   306 (*Main Result.*)
   305 (*Main Result.*)
   307 val prems = goal Arith.thy
   306 goal Arith.thy
   308     "[| 0:n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m";
   307     "!!m n. [| 0<n;  m:nat;  n:nat |] ==> (m div n)#*n #+ m mod n = m";
   309 by (res_inst_tac [("i","m")] complete_induct 1);
   308 by (etac complete_induct 1);
   310 by (resolve_tac prems 1);
   309 by (res_inst_tac [("Q","x<n")] (excluded_middle RS disjE) 1);
   311 by (res_inst_tac [("Q","x:n")] (excluded_middle RS disjE) 1);
   310 (*case x<n*)
   312 by (ALLGOALS 
   311 by (asm_simp_tac (arith_ss addsimps [mod_less, div_less]) 2);
   313     (asm_simp_tac
   312 (*case n le x*)
   314      (arith_ss addsimps ([mod_type,div_type] @ prems @
   313 by (asm_full_simp_tac
   315         [mod_less,mod_geq, div_less, div_geq,
   314      (arith_ss addsimps [not_lt_iff_le, naturals_are_ordinals,
   316 	 add_assoc, add_diff_inverse, div_termination]))));
   315 			 mod_geq, div_geq, add_assoc,
       
   316 			 div_termination RS ltD, add_diff_inverse]) 1);
   317 val mod_div_equality = result();
   317 val mod_div_equality = result();
   318 
   318 
   319 
   319 
   320 (**** Additional theorems about "less than" ****)
   320 (**** Additional theorems about "le" ****)
   321 
   321 
   322 val [mnat,nnat] = goal Arith.thy
   322 goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m le m #+ n";
   323     "[| m:nat;  n:nat |] ==> ~ (m #+ n) : n";
   323 by (etac nat_induct 1);
   324 by (rtac (mnat RS nat_induct) 1);
   324 by (ALLGOALS (asm_simp_tac arith_ss));
   325 by (ALLGOALS (asm_simp_tac (arith_ss addsimps [mem_not_refl])));
   325 val add_le_self = result();
   326 by (rtac notI 1);
   326 
   327 by (etac notE 1);
   327 goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m le n #+ m";
   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, nat_0_in_succ, succ_mem_succI, 
       
   339 		      naturals_are_ordinals, nat_succI, add_type] 1));
       
   340 val add_less_succ_self = result();
       
   341 
       
   342 goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m <= m #+ n";
       
   343 by (rtac (add_less_succ_self RS member_succD) 1);
       
   344 by (REPEAT (ares_tac [naturals_are_ordinals, add_type] 1));
       
   345 val add_leq_self = result();
       
   346 
       
   347 goal Arith.thy "!!m n. [| m:nat;  n:nat |] ==> m <= n #+ m";
       
   348 by (rtac (add_commute RS ssubst) 1);
   328 by (rtac (add_commute RS ssubst) 1);
   349 by (REPEAT (ares_tac [add_leq_self] 1));
   329 by (REPEAT (ares_tac [add_le_self] 1));
   350 val add_leq_self2 = result();
   330 val add_le_self2 = result();
   351 
   331 
   352 (** Monotonicity of addition **)
   332 (** Monotonicity of addition **)
   353 
   333 
   354 (*strict, in 1st argument*)
   334 (*strict, in 1st argument*)
   355 goal Arith.thy "!!i j k. [| i:j; j:nat |] ==> i#+k : j#+k";
   335 goal Arith.thy "!!i j k. [| i<j; j:nat; k:nat |] ==> i#+k < j#+k";
   356 by (etac succ_less_induct 1);
   336 by (forward_tac [lt_nat_in_nat] 1);
   357 by (ALLGOALS (asm_simp_tac (arith_ss addsimps [succ_iff])));
   337 ba 1;
   358 val add_less_mono1 = result();
   338 by (etac succ_lt_induct 1);
       
   339 by (ALLGOALS (asm_simp_tac (arith_ss addsimps [leI])));
       
   340 val add_lt_mono1 = result();
   359 
   341 
   360 (*strict, in both arguments*)
   342 (*strict, in both arguments*)
   361 goal Arith.thy "!!i j k l. [| i:j; k:l; j:nat; l:nat |] ==> i#+k : j#+l";
   343 goal Arith.thy "!!i j k l. [| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
   362 by (rtac (add_less_mono1 RS Ord_trans) 1);
   344 by (rtac (add_lt_mono1 RS lt_trans) 1);
   363 by (REPEAT_FIRST (ares_tac [add_type, naturals_are_ordinals]));
   345 by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
   364 by (EVERY [rtac (add_commute RS ssubst) 1,
   346 by (EVERY [rtac (add_commute RS ssubst) 1,
   365 	   rtac (add_commute RS ssubst) 3,
   347 	   rtac (add_commute RS ssubst) 3,
   366 	   rtac add_less_mono1 5]);
   348 	   rtac add_lt_mono1 5]);
   367 by (REPEAT (ares_tac [Ord_nat RSN (3,Ord_trans)] 1));
   349 by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
   368 val add_less_mono = result();
   350 val add_lt_mono = result();
   369 
   351 
   370 (*A [clumsy] way of lifting < monotonictity to <= monotonicity *)
   352 (*A [clumsy] way of lifting < monotonicity to le monotonicity *)
   371 val less_mono::ford::prems = goal Ord.thy
   353 val lt_mono::ford::prems = goal Ord.thy
   372      "[| !!i j. [| i:j; j:k |] ==> f(i) : f(j);	\
   354      "[| !!i j. [| i<j; j:k |] ==> f(i) < f(j);	\
   373 \        !!i. i:k ==> f(i):k;			\
   355 \        !!i. i:k ==> Ord(f(i));		\
   374 \        i<=j;  i:k;  j:k;  Ord(k)		\
   356 \        i le j;  j:k				\
   375 \     |] ==> f(i) <= f(j)";
   357 \     |] ==> f(i) le f(j)";
   376 by (cut_facts_tac prems 1);
   358 by (cut_facts_tac prems 1);
   377 by (rtac member_succD 1);
   359 by (fast_tac (lt_cs addSIs [lt_mono,ford] addSEs [leE]) 1);
   378 by (dtac member_succI 1);
   360 val Ord_lt_mono_imp_le_mono = result();
   379 by (fast_tac (ZF_cs addSIs [less_mono]) 3);
   361 
   380 by (REPEAT (ares_tac [ford,Ord_in_Ord] 1));
   362 (*le monotonicity, 1st argument*)
   381 val Ord_less_mono_imp_mono = result();
       
   382 
       
   383 (*<=, in 1st argument*)
       
   384 goal Arith.thy
   363 goal Arith.thy
   385     "!!i j k. [| i<=j; i:nat; j:nat; k:nat |] ==> i#+k <= j#+k";
   364     "!!i j k. [| i le j; j:nat; k:nat |] ==> i#+k le j#+k";
   386 by (res_inst_tac [("f", "%j.j#+k")] Ord_less_mono_imp_mono 1);
   365 by (res_inst_tac [("f", "%j.j#+k")] Ord_lt_mono_imp_le_mono 1);
   387 by (REPEAT (ares_tac [add_less_mono1, add_type, Ord_nat] 1));
   366 by (REPEAT (ares_tac [add_lt_mono1, add_type RS naturals_are_ordinals] 1));
   388 val add_mono1 = result();
   367 val add_le_mono1 = result();
   389 
   368 
   390 (*<=, in both arguments*)
   369 (* le monotonicity, BOTH arguments*)
   391 goal Arith.thy
   370 goal Arith.thy
   392     "!!i j k. [| i<=j; k<=l; i:nat; j:nat; k:nat; l:nat |] ==> i#+k <= j#+l";
   371     "!!i j k. [| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l";
   393 by (rtac (add_mono1 RS subset_trans) 1);
   372 by (rtac (add_le_mono1 RS le_trans) 1);
   394 by (REPEAT (assume_tac 1));
   373 by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
   395 by (EVERY [rtac (add_commute RS ssubst) 1,
   374 by (EVERY [rtac (add_commute RS ssubst) 1,
   396 	   rtac (add_commute RS ssubst) 3,
   375 	   rtac (add_commute RS ssubst) 3,
   397 	   rtac add_mono1 5]);
   376 	   rtac add_le_mono1 5]);
   398 by (REPEAT (assume_tac 1));
   377 by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
   399 val add_mono = result();
   378 val add_le_mono = result();