--- a/src/ZF/Arith.ML Mon Jun 22 15:53:24 1998 +0200
+++ b/src/ZF/Arith.ML Mon Jun 22 17:12:27 1998 +0200
@@ -22,12 +22,12 @@
val rec_trans = rec_def RS def_transrec RS trans;
-goal Arith.thy "rec(0,a,b) = a";
+Goal "rec(0,a,b) = a";
by (rtac rec_trans 1);
by (rtac nat_case_0 1);
qed "rec_0";
-goal Arith.thy "rec(succ(m),a,b) = b(m, rec(m,a,b))";
+Goal "rec(succ(m),a,b) = b(m, rec(m,a,b))";
by (rtac rec_trans 1);
by (Simp_tac 1);
qed "rec_succ";
@@ -47,7 +47,7 @@
Addsimps [rec_type, nat_0_le, nat_le_refl];
val nat_typechecks = [rec_type, nat_0I, nat_1I, nat_succI, Ord_nat];
-goal Arith.thy "!!k. [| 0<k; k: nat |] ==> EX j: nat. k = succ(j)";
+Goal "!!k. [| 0<k; k: nat |] ==> EX j: nat. k = succ(j)";
by (etac rev_mp 1);
by (etac nat_induct 1);
by (Simp_tac 1);
@@ -198,11 +198,11 @@
Addsimps [mult_0_right, mult_succ_right];
-goal Arith.thy "!!n. n:nat ==> 1 #* n = n";
+Goal "!!n. n:nat ==> 1 #* n = n";
by (Asm_simp_tac 1);
qed "mult_1";
-goal Arith.thy "!!n. n:nat ==> n #* 1 = n";
+Goal "!!n. n:nat ==> n #* 1 = n";
by (Asm_simp_tac 1);
qed "mult_1_right";
@@ -255,7 +255,7 @@
(ALLGOALS (asm_simp_tac (simpset() addsimps prems))) ]);
(*Addition is the inverse of subtraction*)
-goal Arith.thy "!!m n. [| n le m; m:nat |] ==> n #+ (m#-n) = m";
+Goal "!!m n. [| n le m; m:nat |] ==> n #+ (m#-n) = m";
by (forward_tac [lt_nat_in_nat] 1);
by (etac nat_succI 1);
by (etac rev_mp 1);
@@ -264,7 +264,7 @@
qed "add_diff_inverse";
(*Proof is IDENTICAL to that above*)
-goal Arith.thy "!!m n. [| n le m; m:nat |] ==> succ(m) #- n = succ(m#-n)";
+Goal "!!m n. [| n le m; m:nat |] ==> succ(m) #- n = succ(m#-n)";
by (forward_tac [lt_nat_in_nat] 1);
by (etac nat_succI 1);
by (etac rev_mp 1);
@@ -280,19 +280,19 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mnat])));
qed "diff_add_inverse";
-goal Arith.thy
+Goal
"!!m n. [| m:nat; n:nat |] ==> (m#+n) #- n = m";
by (res_inst_tac [("m1","m")] (add_commute RS ssubst) 1);
by (REPEAT (ares_tac [diff_add_inverse] 1));
qed "diff_add_inverse2";
-goal Arith.thy
+Goal
"!!k. [| k:nat; m: nat; n: nat |] ==> (k#+m) #- (k#+n) = m #- n";
by (nat_ind_tac "k" [] 1);
by (ALLGOALS Asm_simp_tac);
qed "diff_cancel";
-goal Arith.thy
+Goal
"!!n. [| k:nat; m: nat; n: nat |] ==> (m#+k) #- (n#+k) = m #- n";
val add_commute_k = read_instantiate [("n","k")] add_commute;
by (asm_simp_tac (simpset() addsimps [add_commute_k, diff_cancel]) 1);
@@ -306,13 +306,13 @@
(** Difference distributes over multiplication **)
-goal Arith.thy
+Goal
"!!m n. [| m:nat; n: nat; k:nat |] ==> (m #- n) #* k = (m #* k) #- (n #* k)";
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_cancel])));
qed "diff_mult_distrib" ;
-goal Arith.thy
+Goal
"!!m. [| m:nat; n: nat; k:nat |] ==> k #* (m #- n) = (k #* m) #- (k #* n)";
val mult_commute_k = read_instantiate [("m","k")] mult_commute;
by (asm_simp_tac (simpset() addsimps
@@ -321,7 +321,7 @@
(*** Remainder ***)
-goal Arith.thy "!!m n. [| 0<n; n le m; m:nat |] ==> m #- n < m";
+Goal "!!m n. [| 0<n; n le m; m:nat |] ==> m #- n < m";
by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
by (etac rev_mp 1);
by (etac rev_mp 1);
@@ -338,16 +338,16 @@
not_lt_iff_le RS iffD2];
(*Type checking depends upon termination!*)
-goalw Arith.thy [mod_def] "!!m n. [| 0<n; m:nat; n:nat |] ==> m mod n : nat";
+Goalw [mod_def] "!!m n. [| 0<n; m:nat; n:nat |] ==> m mod n : nat";
by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
qed "mod_type";
-goal Arith.thy "!!m n. [| 0<n; m<n |] ==> m mod n = m";
+Goal "!!m n. [| 0<n; m<n |] ==> m mod n = m";
by (rtac (mod_def RS def_transrec RS trans) 1);
by (asm_simp_tac div_ss 1);
qed "mod_less";
-goal Arith.thy "!!m n. [| 0<n; n le m; m:nat |] ==> m mod n = (m#-n) mod n";
+Goal "!!m n. [| 0<n; n le m; m:nat |] ==> m mod n = (m#-n) mod n";
by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
by (rtac (mod_def RS def_transrec RS trans) 1);
by (asm_simp_tac div_ss 1);
@@ -358,17 +358,17 @@
(*** Quotient ***)
(*Type checking depends upon termination!*)
-goalw Arith.thy [div_def]
+Goalw [div_def]
"!!m n. [| 0<n; m:nat; n:nat |] ==> m div n : nat";
by (REPEAT (ares_tac div_rls 1 ORELSE etac lt_trans 1));
qed "div_type";
-goal Arith.thy "!!m n. [| 0<n; m<n |] ==> m div n = 0";
+Goal "!!m n. [| 0<n; m<n |] ==> m div n = 0";
by (rtac (div_def RS def_transrec RS trans) 1);
by (asm_simp_tac div_ss 1);
qed "div_less";
-goal Arith.thy
+Goal
"!!m n. [| 0<n; n le m; m:nat |] ==> m div n = succ((m#-n) div n)";
by (forward_tac [lt_nat_in_nat] 1 THEN etac nat_succI 1);
by (rtac (div_def RS def_transrec RS trans) 1);
@@ -378,7 +378,7 @@
Addsimps [div_type, div_less, div_geq];
(*A key result*)
-goal Arith.thy
+Goal
"!!m n. [| 0<n; m:nat; n:nat |] ==> (m div n)#*n #+ m mod n = m";
by (etac complete_induct 1);
by (excluded_middle_tac "x<n" 1);
@@ -392,7 +392,7 @@
(*** Further facts about mod (mainly for mutilated checkerboard ***)
-goal Arith.thy
+Goal
"!!m n. [| 0<n; m:nat; n:nat |] ==> \
\ succ(m) mod n = if(succ(m mod n) = n, 0, succ(m mod n))";
by (etac complete_induct 1);
@@ -410,7 +410,7 @@
by (asm_simp_tac (simpset() addsimps [mod_less, diff_self_eq_0]) 1);
qed "mod_succ";
-goal Arith.thy "!!m n. [| 0<n; m:nat; n:nat |] ==> m mod n < n";
+Goal "!!m n. [| 0<n; m:nat; n:nat |] ==> m mod n < n";
by (etac complete_induct 1);
by (excluded_middle_tac "x<n" 1);
(*case x<n*)
@@ -422,7 +422,7 @@
qed "mod_less_divisor";
-goal Arith.thy
+Goal
"!!k b. [| k: nat; b<2 |] ==> k mod 2 = b | k mod 2 = if(b=1,0,1)";
by (subgoal_tac "k mod 2: 2" 1);
by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2);
@@ -431,13 +431,13 @@
by (Blast_tac 1);
qed "mod2_cases";
-goal Arith.thy "!!m. m:nat ==> succ(succ(m)) mod 2 = m mod 2";
+Goal "!!m. m:nat ==> succ(succ(m)) mod 2 = m mod 2";
by (subgoal_tac "m mod 2: 2" 1);
by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2);
by (asm_simp_tac (simpset() addsimps [mod_succ] setloop Step_tac) 1);
qed "mod2_succ_succ";
-goal Arith.thy "!!m. m:nat ==> (m#+m) mod 2 = 0";
+Goal "!!m. m:nat ==> (m#+m) mod 2 = 0";
by (etac nat_induct 1);
by (simp_tac (simpset() addsimps [mod_less]) 1);
by (asm_simp_tac (simpset() addsimps [mod2_succ_succ, add_succ_right]) 1);
@@ -446,12 +446,12 @@
(**** Additional theorems about "le" ****)
-goal Arith.thy "!!m n. [| m:nat; n:nat |] ==> m le m #+ n";
+Goal "!!m n. [| m:nat; n:nat |] ==> m le m #+ n";
by (etac nat_induct 1);
by (ALLGOALS Asm_simp_tac);
qed "add_le_self";
-goal Arith.thy "!!m n. [| m:nat; n:nat |] ==> m le n #+ m";
+Goal "!!m n. [| m:nat; n:nat |] ==> m le n #+ m";
by (stac add_commute 1);
by (REPEAT (ares_tac [add_le_self] 1));
qed "add_le_self2";
@@ -459,7 +459,7 @@
(*** Monotonicity of Addition ***)
(*strict, in 1st argument; proof is by rule induction on 'less than'*)
-goal Arith.thy "!!i j k. [| i<j; j:nat; k:nat |] ==> i#+k < j#+k";
+Goal "!!i j k. [| i<j; j:nat; k:nat |] ==> i#+k < j#+k";
by (forward_tac [lt_nat_in_nat] 1);
by (assume_tac 1);
by (etac succ_lt_induct 1);
@@ -467,7 +467,7 @@
qed "add_lt_mono1";
(*strict, in both arguments*)
-goal Arith.thy "!!i j k l. [| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
+Goal "!!i j k l. [| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
by (rtac (add_lt_mono1 RS lt_trans) 1);
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat] 1));
by (EVERY [stac add_commute 1,
@@ -487,14 +487,14 @@
qed "Ord_lt_mono_imp_le_mono";
(*le monotonicity, 1st argument*)
-goal Arith.thy
+Goal
"!!i j k. [| i le j; j:nat; k:nat |] ==> i#+k le j#+k";
by (res_inst_tac [("f", "%j. j#+k")] Ord_lt_mono_imp_le_mono 1);
by (REPEAT (ares_tac [add_lt_mono1, add_type RS nat_into_Ord] 1));
qed "add_le_mono1";
(* le monotonicity, BOTH arguments*)
-goal Arith.thy
+Goal
"!!i j k. [| i le j; k le l; j:nat; l:nat |] ==> i#+k le j#+l";
by (rtac (add_le_mono1 RS le_trans) 1);
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
@@ -506,14 +506,14 @@
(*** Monotonicity of Multiplication ***)
-goal Arith.thy "!!i j k. [| i le j; j:nat; k:nat |] ==> i#*k le j#*k";
+Goal "!!i j k. [| i le j; j:nat; k:nat |] ==> i#*k le j#*k";
by (forward_tac [lt_nat_in_nat] 1);
by (nat_ind_tac "k" [] 2);
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_le_mono])));
qed "mult_le_mono1";
(* le monotonicity, BOTH arguments*)
-goal Arith.thy
+Goal
"!!i j k. [| i le j; k le l; j:nat; l:nat |] ==> i#*k le j#*l";
by (rtac (mult_le_mono1 RS le_trans) 1);
by (REPEAT (eresolve_tac [asm_rl, lt_nat_in_nat, nat_succI] 1));
@@ -524,7 +524,7 @@
qed "mult_le_mono";
(*strict, in 1st argument; proof is by induction on k>0*)
-goal Arith.thy "!!i j k. [| i<j; 0<k; j:nat; k:nat |] ==> k#*i < k#*j";
+Goal "!!i j k. [| i<j; 0<k; j:nat; k:nat |] ==> k#*i < k#*j";
by (etac zero_lt_natE 1);
by (forward_tac [lt_nat_in_nat] 2);
by (ALLGOALS Asm_simp_tac);
@@ -532,20 +532,20 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono])));
qed "mult_lt_mono2";
-goal thy "!!k. [| i<j; 0<k; i:nat; j:nat; k:nat |] ==> i#*k < j#*k";
+Goal "!!k. [| i<j; 0<k; i:nat; j:nat; k:nat |] ==> i#*k < j#*k";
by (asm_simp_tac (simpset() addsimps [mult_lt_mono2, mult_commute]) 1);
qed "mult_lt_mono1";
-goal Arith.thy "!!k. [| m: nat; n: nat |] ==> 0 < m#*n <-> 0<m & 0<n";
+Goal "!!k. [| m: nat; n: nat |] ==> 0 < m#*n <-> 0<m & 0<n";
by (best_tac (claset() addEs [natE] addss (simpset())) 1);
qed "zero_lt_mult_iff";
-goal Arith.thy "!!k. [| m: nat; n: nat |] ==> m#*n = 1 <-> m=1 & n=1";
+Goal "!!k. [| m: nat; n: nat |] ==> m#*n = 1 <-> m=1 & n=1";
by (best_tac (claset() addEs [natE] addss (simpset())) 1);
qed "mult_eq_1_iff";
(*Cancellation law for division*)
-goal Arith.thy
+Goal
"!!k. [| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> (k#*m) div (k#*n) = m div n";
by (eres_inst_tac [("i","m")] complete_induct 1);
by (excluded_middle_tac "x<n" 1);
@@ -558,7 +558,7 @@
div_termination RS ltD]) 1);
qed "div_cancel";
-goal Arith.thy
+Goal
"!!k. [| 0<n; 0<k; k:nat; m:nat; n:nat |] ==> \
\ (k#*m) mod (k#*n) = k #* (m mod n)";
by (eres_inst_tac [("i","m")] complete_induct 1);
@@ -576,7 +576,7 @@
val mono_lemma = (nat_into_Ord RS Ord_0_lt) RSN (2,mult_lt_mono2);
-goal Arith.thy "!!m n. [| m = m#*n; m: nat; n: nat |] ==> n=1 | m=0";
+Goal "!!m n. [| m = m#*n; m: nat; n: nat |] ==> n=1 | m=0";
by (rtac disjCI 1);
by (dtac sym 1);
by (rtac Ord_linear_lt 1 THEN REPEAT_SOME (ares_tac [nat_into_Ord,nat_1I]));
@@ -587,7 +587,7 @@
(*Thanks to Sten Agerholm*)
-goal Arith.thy (* add_le_elim1 *)
+Goal (* add_le_elim1 *)
"!!m n k. [|m#+n le m#+k; m:nat; n:nat; k:nat|] ==> n le k";
by (etac rev_mp 1);
by (eres_inst_tac [("n","n")] nat_induct 1);