--- a/src/ZF/Arith.ML Mon Aug 07 10:29:04 2000 +0200
+++ b/src/ZF/Arith.ML Mon Aug 07 10:29:54 2000 +0200
@@ -39,7 +39,6 @@
by (rtac (natify_def RS def_Vrecursor RS trans) 1);
by Auto_tac;
qed "natify_succ";
-Addsimps [natify_succ];
Goal "natify(0) = 0";
by (rtac (natify_def RS def_Vrecursor RS trans) 1);
@@ -55,14 +54,14 @@
Goal "natify(x) : nat";
by (eps_ind_tac "x" 1);
by (case_tac "EX z. x1 = succ(z)" 1);
-by (auto_tac (claset(), simpset() addsimps [natify_non_succ]));
+by (auto_tac (claset(), simpset() addsimps [natify_succ, natify_non_succ]));
qed "natify_in_nat";
AddIffs [natify_in_nat];
AddTCs [natify_in_nat];
Goal "n : nat ==> natify(n) = n";
by (induct_tac "n" 1);
-by Auto_tac;
+by (auto_tac (claset(), simpset() addsimps [natify_succ]));
qed "natify_ident";
Addsimps [natify_ident];
@@ -180,7 +179,7 @@
(*Must simplify BEFORE the induction: else we get a critical pair*)
Goal "succ(m) #- succ(n) = m #- n";
-by (simp_tac (simpset() addsimps [diff_def]) 1);
+by (simp_tac (simpset() addsimps [natify_succ, diff_def]) 1);
by (res_inst_tac [("x1","n")] (natify_in_nat RS nat_induct) 1);
by Auto_tac;
qed "diff_succ_succ";
@@ -208,13 +207,17 @@
(*Natify has weakened this law, compared with the older approach*)
Goal "0 #+ m = natify(m)";
by (asm_simp_tac (simpset() addsimps [add_def]) 1);
-qed "add_0";
+qed "add_0_natify";
Goal "succ(m) #+ n = succ(m #+ n)";
-by (asm_simp_tac (simpset() addsimps [add_def]) 1);
+by (asm_simp_tac (simpset() addsimps [natify_succ, add_def]) 1);
qed "add_succ";
-Addsimps [add_0, add_succ];
+Addsimps [add_0_natify, add_succ];
+
+Goal "m: nat ==> 0 #+ m = m";
+by (Asm_simp_tac 1);
+qed "add_0";
(*Associative law for addition*)
Goal "(m #+ n) #+ k = m #+ (n #+ k)";
@@ -234,7 +237,7 @@
Goalw [add_def] "m #+ succ(n) = succ(m #+ n)";
by (res_inst_tac [("n","natify(m)")] nat_induct 1);
-by Auto_tac;
+by (auto_tac (claset(), simpset() addsimps [natify_succ]));
qed "add_succ_right";
Addsimps [add_0_right_natify, add_succ_right];
@@ -272,20 +275,150 @@
by Auto_tac;
qed "add_left_cancel_natify";
-Goal "[| k #+ m = k #+ n; m:nat; n:nat |] ==> m = n";
-by (dtac add_left_cancel_natify 1);
-by Auto_tac;
+Goal "[| i = j; i #+ m = j #+ n; m:nat; n:nat |] ==> m = n";
+by (force_tac (claset() addSDs [add_left_cancel_natify], simpset()) 1);
qed "add_left_cancel";
+(*Thanks to Sten Agerholm*)
+Goal "k#+m le k#+n ==> natify(m) le natify(n)";
+by (res_inst_tac [("P", "natify(k)#+m le natify(k)#+n")] rev_mp 1);
+by (res_inst_tac [("n","natify(k)")] nat_induct 2);
+by Auto_tac;
+qed "add_le_elim1_natify";
-(*** Multiplication ***)
+Goal "[| k#+m le k#+n; m: nat; n: nat |] ==> m le n";
+by (dtac add_le_elim1_natify 1);
+by Auto_tac;
+qed "add_le_elim1";
+
+Goal "k#+m < k#+n ==> natify(m) < natify(n)";
+by (res_inst_tac [("P", "natify(k)#+m < natify(k)#+n")] rev_mp 1);
+by (res_inst_tac [("n","natify(k)")] nat_induct 2);
+by Auto_tac;
+qed "add_lt_elim1_natify";
+
+Goal "[| k#+m < k#+n; m: nat; n: nat |] ==> m < n";
+by (dtac add_lt_elim1_natify 1);
+by Auto_tac;
+qed "add_lt_elim1";
+
+
+(*** Monotonicity of Addition ***)
+
+(*strict, in 1st argument; proof is by rule induction on 'less than'.
+ Still need j:nat, for consider j = omega. Then we can have i<omega,
+ which is the same as i:nat, but natify(j)=0, so the conclusion fails.*)
+Goal "[| i<j; j:nat |] ==> i#+k < j#+k";
+by (ftac lt_nat_in_nat 1);
+by (assume_tac 1);
+by (etac succ_lt_induct 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [leI])));
+qed "add_lt_mono1";
+
+(*strict, in both arguments*)
+Goal "[| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
+by (rtac (add_lt_mono1 RS lt_trans) 1);
+by (REPEAT (assume_tac 1));
+by (EVERY [stac add_commute 1,
+ stac add_commute 1,
+ rtac add_lt_mono1 1]);
+by (REPEAT (assume_tac 1));
+qed "add_lt_mono";
+
+(*A [clumsy] way of lifting < monotonicity to le monotonicity *)
+val lt_mono::ford::prems = Goal
+ "[| !!i j. [| i<j; j:k |] ==> f(i) < f(j); \
+\ !!i. i:k ==> Ord(f(i)); \
+\ i le j; j:k \
+\ |] ==> f(i) le f(j)";
+by (cut_facts_tac prems 1);
+by (blast_tac (le_cs addSIs [lt_mono,ford] addSEs [leE]) 1);
+qed "Ord_lt_mono_imp_le_mono";
+
+(*le monotonicity, 1st argument*)
+Goal "[| i le j; j: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 "[| 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 (assume_tac 1));
+by (EVERY [stac add_commute 1,
+ stac add_commute 1,
+ rtac add_le_mono1 1]);
+by (REPEAT (assume_tac 1));
+qed "add_le_mono";
+
+(** Subtraction is the inverse of addition. **)
+
+Goal "(n#+m) #- n = natify(m)";
+by (subgoal_tac "(natify(n) #+ m) #- natify(n) = natify(m)" 1);
+by (res_inst_tac [("n","natify(n)")] nat_induct 2);
+by Auto_tac;
+qed "diff_add_inverse";
+
+Goal "(m#+n) #- n = natify(m)";
+by (simp_tac (simpset() addsimps [inst "m" "m" add_commute,
+ diff_add_inverse]) 1);
+qed "diff_add_inverse2";
+
+Goal "(k#+m) #- (k#+n) = m #- n";
+by (subgoal_tac "(natify(k) #+ natify(m)) #- (natify(k) #+ natify(n)) = \
+\ natify(m) #- natify(n)" 1);
+by (res_inst_tac [("n","natify(k)")] nat_induct 2);
+by Auto_tac;
+qed "diff_cancel";
+
+Goal "(m#+k) #- (n#+k) = m #- n";
+by (simp_tac (simpset() addsimps [inst "n" "k" add_commute, diff_cancel]) 1);
+qed "diff_cancel2";
+
+Goal "n #- (n#+m) = 0";
+by (subgoal_tac "natify(n) #- (natify(n) #+ natify(m)) = 0" 1);
+by (res_inst_tac [("n","natify(n)")] nat_induct 2);
+by Auto_tac;
+qed "diff_add_0";
+
+
+(** Lemmas for the CancelNumerals simproc **)
+
+Goal "(u #+ m = u #+ n) <-> (0 #+ m = natify(n))";
+by Auto_tac;
+by (blast_tac (claset() addDs [add_left_cancel_natify]) 1);
+by (asm_full_simp_tac (simpset() addsimps [add_def]) 1);
+qed "eq_add_iff";
+
+Goal "(u #+ m < u #+ n) <-> (0 #+ m < natify(n))";
+by (auto_tac (claset(), simpset() addsimps [add_lt_elim1_natify]));
+by (dtac add_lt_mono1 1);
+by (auto_tac (claset(), simpset() addsimps [inst "m" "u" add_commute]));
+qed "less_add_iff";
+
+Goal "((u #+ m) #- (u #+ n)) = ((0 #+ m) #- n)";
+by (asm_simp_tac (simpset() addsimps [diff_cancel]) 1);
+qed "diff_add_eq";
+
+(*To tidy up the result of a simproc. Only the RHS will be simplified.*)
+Goal "u = u' ==> (t==u) == (t==u')";
+by Auto_tac;
+qed "eq_cong2";
+
+Goal "u <-> u' ==> (t==u) == (t==u')";
+by Auto_tac;
+qed "iff_cong2";
+
+
+(*** Multiplication [the simprocs need these laws] ***)
Goal "0 #* m = 0";
by (simp_tac (simpset() addsimps [mult_def]) 1);
qed "mult_0";
Goal "succ(m) #* n = n #+ (m #* n)";
-by (simp_tac (simpset() addsimps [add_def, mult_def, raw_mult_type]) 1);
+by (simp_tac (simpset() addsimps [add_def, mult_def, natify_succ,
+ raw_mult_type]) 1);
qed "mult_succ";
Addsimps [mult_0, mult_succ];
@@ -300,7 +433,7 @@
Goal "m #* succ(n) = m #+ (m #* n)";
by (subgoal_tac "natify(m) #* succ(natify(n)) = \
\ natify(m) #+ (natify(m) #* natify(n))" 1);
-by (full_simp_tac (simpset() addsimps [add_def, mult_def]) 1);
+by (full_simp_tac (simpset() addsimps [natify_succ, add_def, mult_def]) 1);
by (res_inst_tac [("n","natify(m)")] nat_induct 1);
by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac)));
qed "mult_succ_right";
@@ -366,474 +499,3 @@
val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
-(*** Difference ***)
-
-Goal "m #- m = 0";
-by (subgoal_tac "natify(m) #- natify(m) = 0" 1);
-by (rtac (natify_in_nat RS nat_induct) 2);
-by Auto_tac;
-qed "diff_self_eq_0";
-
-(**Addition is the inverse of subtraction**)
-
-(*We need m:nat even if we replace the RHS by natify(m), for consider e.g.
- n=2, m=omega; then n + (m-n) = 2 + (0-2) = 2 ~= 0 = natify(m).*)
-Goal "[| n le m; m:nat |] ==> n #+ (m#-n) = m";
-by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
-by (etac rev_mp 1);
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by Auto_tac;
-qed "add_diff_inverse";
-
-Goal "[| n le m; m:nat |] ==> (m#-n) #+ n = m";
-by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
-by (asm_simp_tac (simpset() addsimps [add_commute, add_diff_inverse]) 1);
-qed "add_diff_inverse2";
-
-(*Proof is IDENTICAL to that of add_diff_inverse*)
-Goal "[| n le m; m:nat |] ==> succ(m) #- n = succ(m#-n)";
-by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
-by (etac rev_mp 1);
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "diff_succ";
-
-Goal "[| m: nat; n: nat |] ==> 0 < (n #- m) <-> m<n";
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS Asm_simp_tac);
-qed "zero_less_diff";
-Addsimps [zero_less_diff];
-
-
-(** Subtraction is the inverse of addition. **)
-
-Goal "(n#+m) #- n = natify(m)";
-by (subgoal_tac "(natify(n) #+ m) #- natify(n) = natify(m)" 1);
-by (res_inst_tac [("n","natify(n)")] nat_induct 2);
-by Auto_tac;
-qed "diff_add_inverse";
-
-Goal "(m#+n) #- n = natify(m)";
-by (simp_tac (simpset() addsimps [inst "m" "m" add_commute,
- diff_add_inverse]) 1);
-qed "diff_add_inverse2";
-
-Goal "(k#+m) #- (k#+n) = m #- n";
-by (subgoal_tac "(natify(k) #+ natify(m)) #- (natify(k) #+ natify(n)) = \
-\ natify(m) #- natify(n)" 1);
-by (res_inst_tac [("n","natify(k)")] nat_induct 2);
-by Auto_tac;
-qed "diff_cancel";
-
-Goal "(m#+k) #- (n#+k) = m #- n";
-by (simp_tac (simpset() addsimps [inst "n" "k" add_commute, diff_cancel]) 1);
-qed "diff_cancel2";
-
-Goal "n #- (n#+m) = 0";
-by (subgoal_tac "natify(n) #- (natify(n) #+ natify(m)) = 0" 1);
-by (res_inst_tac [("n","natify(n)")] nat_induct 2);
-by Auto_tac;
-qed "diff_add_0";
-
-(** Difference distributes over multiplication **)
-
-Goal "(m #- n) #* k = (m #* k) #- (n #* k)";
-by (subgoal_tac "(natify(m) #- natify(n)) #* natify(k) = \
-\ (natify(m) #* natify(k)) #- (natify(n) #* natify(k))" 1);
-by (res_inst_tac [("m","natify(m)"),("n","natify(n)")] diff_induct 2);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [diff_cancel])));
-qed "diff_mult_distrib" ;
-
-Goal "k #* (m #- n) = (k #* m) #- (k #* n)";
-by (simp_tac
- (simpset() addsimps [inst "m" "k" mult_commute, diff_mult_distrib]) 1);
-qed "diff_mult_distrib2";
-
-
-(*** Remainder ***)
-
-(*We need m:nat even with natify*)
-Goal "[| 0<n; n le m; m:nat |] ==> m #- n < m";
-by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
-by (etac rev_mp 1);
-by (etac rev_mp 1);
-by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_le_self])));
-qed "div_termination";
-
-val div_rls = (*for mod and div*)
- nat_typechecks @
- [Ord_transrec_type, apply_funtype, div_termination RS ltD,
- nat_into_Ord, not_lt_iff_le RS iffD1];
-
-val div_ss = simpset() addsimps [div_termination RS ltD,
- not_lt_iff_le RS iffD2];
-
-Goalw [raw_mod_def] "[| m:nat; n:nat |] ==> raw_mod (m, n) : nat";
-by (rtac Ord_transrec_type 1);
-by (auto_tac(claset(), simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff]));
-by (REPEAT (ares_tac div_rls 1));
-qed "raw_mod_type";
-
-Goalw [mod_def] "m mod n : nat";
-by (simp_tac (simpset() addsimps [mod_def, raw_mod_type]) 1);
-qed "mod_type";
-AddTCs [mod_type];
-AddIffs [mod_type];
-
-
-(** Aribtrary definitions for division by zero. Useful to simplify
- certain equations **)
-
-Goalw [div_def] "a div 0 = 0";
-by (rtac (raw_div_def RS def_transrec RS trans) 1);
-by (Asm_simp_tac 1);
-qed "DIVISION_BY_ZERO_DIV"; (*NOT for adding to default simpset*)
-
-Goalw [mod_def] "a mod 0 = natify(a)";
-by (rtac (raw_mod_def RS def_transrec RS trans) 1);
-by (Asm_simp_tac 1);
-qed "DIVISION_BY_ZERO_MOD"; (*NOT for adding to default simpset*)
-
-fun div_undefined_case_tac s i =
- case_tac s i THEN
- asm_full_simp_tac
- (simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff]) (i+1) THEN
- asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_DIV,
- DIVISION_BY_ZERO_MOD]) i;
-
-Goal "m<n ==> raw_mod (m,n) = m";
-by (rtac (raw_mod_def RS def_transrec RS trans) 1);
-by (asm_simp_tac (simpset() addsimps [div_termination RS ltD]) 1);
-qed "raw_mod_less";
-
-Goal "[| m<n; n : nat |] ==> m mod n = m";
-by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [mod_def, raw_mod_less]) 1);
-qed "mod_less";
-
-Goal "[| 0<n; n le m; m:nat |] ==> raw_mod (m, n) = raw_mod (m#-n, n)";
-by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
-by (rtac (raw_mod_def RS def_transrec RS trans) 1);
-by (asm_simp_tac div_ss 1);
-by (Blast_tac 1);
-qed "raw_mod_geq";
-
-Goal "[| n le m; m:nat |] ==> m mod n = (m#-n) mod n";
-by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
-by (div_undefined_case_tac "n=0" 1);
-by (asm_simp_tac (simpset() addsimps [mod_def, raw_mod_geq]) 1);
-qed "mod_geq";
-
-Addsimps [mod_less];
-
-
-(*** Division ***)
-
-Goalw [raw_div_def] "[| m:nat; n:nat |] ==> raw_div (m, n) : nat";
-by (rtac Ord_transrec_type 1);
-by (auto_tac(claset(), simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff]));
-by (REPEAT (ares_tac div_rls 1));
-qed "raw_div_type";
-
-Goalw [div_def] "m div n : nat";
-by (simp_tac (simpset() addsimps [div_def, raw_div_type]) 1);
-qed "div_type";
-AddTCs [div_type];
-AddIffs [div_type];
-
-Goal "m<n ==> raw_div (m,n) = 0";
-by (rtac (raw_div_def RS def_transrec RS trans) 1);
-by (asm_simp_tac (simpset() addsimps [div_termination RS ltD]) 1);
-qed "raw_div_less";
-
-Goal "[| m<n; n : nat |] ==> m div n = 0";
-by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
-by (asm_simp_tac (simpset() addsimps [div_def, raw_div_less]) 1);
-qed "div_less";
-
-Goal "[| 0<n; n le m; m:nat |] ==> raw_div(m,n) = succ(raw_div(m#-n, n))";
-by (subgoal_tac "n ~= 0" 1);
-by (Blast_tac 2);
-by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
-by (rtac (raw_div_def RS def_transrec RS trans) 1);
-by (asm_simp_tac div_ss 1);
-qed "raw_div_geq";
-
-Goal "[| 0<n; n le m; m:nat |] ==> m div n = succ ((m#-n) div n)";
-by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
-by (asm_simp_tac (simpset() addsimps [div_def, raw_div_geq]) 1);
-qed "div_geq";
-
-Addsimps [div_less, div_geq];
-
-
-(*A key result*)
-Goal "[| m: nat; n: nat |] ==> (m div n)#*n #+ m mod n = m";
-by (div_undefined_case_tac "n=0" 1);
-by (etac complete_induct 1);
-by (case_tac "x<n" 1);
-(*case n le x*)
-by (asm_full_simp_tac
- (simpset() addsimps [not_lt_iff_le, add_assoc, mod_geq,
- div_termination RS ltD, add_diff_inverse]) 2);
-(*case x<n*)
-by (Asm_simp_tac 1);
-val lemma = result();
-
-Goal "(m div n)#*n #+ m mod n = natify(m)";
-by (subgoal_tac
- "(natify(m) div natify(n))#*natify(n) #+ natify(m) mod natify(n) = \
-\ natify(m)" 1);
-by (stac lemma 2);
-by Auto_tac;
-qed "mod_div_equality_natify";
-
-Goal "m: nat ==> (m div n)#*n #+ m mod n = m";
-by (asm_simp_tac (simpset() addsimps [mod_div_equality_natify]) 1);
-qed "mod_div_equality";
-
-
-(*** Further facts about mod (mainly for mutilated chess board) ***)
-
-Goal "[| 0<n; m:nat; n:nat |] \
-\ ==> succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))";
-by (etac complete_induct 1);
-by (excluded_middle_tac "succ(x)<n" 1);
-(* case succ(x) < n *)
-by (asm_simp_tac (simpset() addsimps [nat_le_refl RS lt_trans,
- succ_neq_self]) 2);
-by (asm_simp_tac (simpset() addsimps [ltD RS mem_imp_not_eq]) 2);
-(* case n le succ(x) *)
-by (asm_full_simp_tac (simpset() addsimps [mod_geq, not_lt_iff_le]) 1);
-by (etac leE 1);
-(*equality case*)
-by (asm_full_simp_tac (simpset() addsimps [diff_self_eq_0]) 2);
-by (asm_simp_tac (simpset() addsimps [mod_geq, div_termination RS ltD,
- diff_succ]) 1);
-val lemma = result();
-
-Goal "n:nat ==> \
-\ succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))";
-by (case_tac "n=0" 1);
-by (asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_MOD]) 1);
-by (subgoal_tac
- "natify(succ(m)) mod n = \
-\ (if succ(natify(m) mod n) = n then 0 else succ(natify(m) mod n))" 1);
-by (stac natify_succ 2);
-by (rtac lemma 2);
-by (auto_tac(claset(),
- simpset() delsimps [natify_succ]
- addsimps [nat_into_Ord RS Ord_0_lt_iff]));
-qed "mod_succ";
-
-Goal "[| 0<n; n:nat |] ==> m mod n < n";
-by (subgoal_tac "natify(m) mod n < n" 1);
-by (res_inst_tac [("i","natify(m)")] complete_induct 2);
-by (case_tac "x<n" 3);
-(*case x<n*)
-by (Asm_simp_tac 3);
-(*case n le x*)
-by (asm_full_simp_tac
- (simpset() addsimps [mod_geq, not_lt_iff_le, div_termination RS ltD]) 3);
-by Auto_tac;
-qed "mod_less_divisor";
-
-Goal "b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
-by (subgoal_tac "k mod 2: 2" 1);
-by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2);
-by (dtac ltD 1);
-by Auto_tac;
-qed "mod2_cases";
-
-Goal "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 (auto_tac (claset(), simpset() addsimps [mod_succ]));
-qed "mod2_succ_succ";
-
-Addsimps [mod2_succ_succ];
-
-Goal "(m#+m) mod 2 = 0";
-by (subgoal_tac "(natify(m)#+natify(m)) mod 2 = 0" 1);
-by (res_inst_tac [("n","natify(m)")] nat_induct 2);
-by Auto_tac;
-qed "mod2_add_self";
-
-Addsimps [mod2_add_self];
-
-
-(**** Additional theorems about "le" ****)
-
-Goal "m:nat ==> m le (m #+ n)";
-by (induct_tac "m" 1);
-by (ALLGOALS Asm_simp_tac);
-qed "add_le_self";
-
-Goal "m:nat ==> m le (n #+ m)";
-by (stac add_commute 1);
-by (etac add_le_self 1);
-qed "add_le_self2";
-
-(*** Monotonicity of Addition ***)
-
-(*strict, in 1st argument; proof is by rule induction on 'less than'.
- Still need j:nat, for consider j = omega. Then we can have i<omega,
- which is the same as i:nat, but natify(j)=0, so the conclusion fails.*)
-Goal "[| i<j; j:nat |] ==> i#+k < j#+k";
-by (ftac lt_nat_in_nat 1);
-by (assume_tac 1);
-by (etac succ_lt_induct 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [leI])));
-qed "add_lt_mono1";
-
-(*strict, in both arguments*)
-Goal "[| i<j; k<l; j:nat; l:nat |] ==> i#+k < j#+l";
-by (rtac (add_lt_mono1 RS lt_trans) 1);
-by (REPEAT (assume_tac 1));
-by (EVERY [stac add_commute 1,
- stac add_commute 1,
- rtac add_lt_mono1 1]);
-by (REPEAT (assume_tac 1));
-qed "add_lt_mono";
-
-(*A [clumsy] way of lifting < monotonicity to le monotonicity *)
-val lt_mono::ford::prems = Goal
- "[| !!i j. [| i<j; j:k |] ==> f(i) < f(j); \
-\ !!i. i:k ==> Ord(f(i)); \
-\ i le j; j:k \
-\ |] ==> f(i) le f(j)";
-by (cut_facts_tac prems 1);
-by (blast_tac (le_cs addSIs [lt_mono,ford] addSEs [leE]) 1);
-qed "Ord_lt_mono_imp_le_mono";
-
-(*le monotonicity, 1st argument*)
-Goal "[| i le j; j: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 "[| 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 (assume_tac 1));
-by (EVERY [stac add_commute 1,
- stac add_commute 1,
- rtac add_le_mono1 1]);
-by (REPEAT (assume_tac 1));
-qed "add_le_mono";
-
-(*** Monotonicity of Multiplication ***)
-
-Goal "[| i le j; j:nat |] ==> (i#*k) le (j#*k)";
-by (subgoal_tac "natify(i)#*natify(k) le j#*natify(k)" 1);
-by (ftac lt_nat_in_nat 2);
-by (res_inst_tac [("n","natify(k)")] nat_induct 3);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_le_mono])));
-qed "mult_le_mono1";
-
-(* le monotonicity, BOTH arguments*)
-Goal "[| 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 (assume_tac 1));
-by (EVERY [stac mult_commute 1,
- stac mult_commute 1,
- rtac mult_le_mono1 1]);
-by (REPEAT (assume_tac 1));
-qed "mult_le_mono";
-
-(*strict, in 1st argument; proof is by induction on k>0.
- I can't see how to relax the typing conditions.*)
-Goal "[| i<j; 0<k; j:nat; k:nat |] ==> k#*i < k#*j";
-by (etac zero_lt_natE 1);
-by (ftac lt_nat_in_nat 2);
-by (ALLGOALS Asm_simp_tac);
-by (induct_tac "x" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono])));
-qed "mult_lt_mono2";
-
-Goal "[| i<j; 0<k; j:nat; k:nat |] ==> i#*k < j#*k";
-by (asm_simp_tac (simpset() addsimps [mult_lt_mono2,
- inst "n" "k" mult_commute]) 1);
-qed "mult_lt_mono1";
-
-Goal "m#+n = 0 <-> natify(m)=0 & natify(n)=0";
-by (subgoal_tac "natify(m) #+ natify(n) = 0 <-> natify(m)=0 & natify(n)=0" 1);
-by (res_inst_tac [("n","natify(m)")] natE 2);
- by (res_inst_tac [("n","natify(n)")] natE 4);
-by Auto_tac;
-qed "add_eq_0_iff";
-AddIffs [add_eq_0_iff];
-
-Goal "0 < m#*n <-> 0 < natify(m) & 0 < natify(n)";
-by (subgoal_tac "0 < natify(m)#*natify(n) <-> \
-\ 0 < natify(m) & 0 < natify(n)" 1);
-by (res_inst_tac [("n","natify(m)")] natE 2);
- by (res_inst_tac [("n","natify(n)")] natE 4);
- by (res_inst_tac [("n","natify(n)")] natE 3);
-by Auto_tac;
-qed "zero_lt_mult_iff";
-
-Goal "m#*n = 1 <-> natify(m)=1 & natify(n)=1";
-by (subgoal_tac "natify(m) #* natify(n) = 1 <-> natify(m)=1 & natify(n)=1" 1);
-by (res_inst_tac [("n","natify(m)")] natE 2);
- by (res_inst_tac [("n","natify(n)")] natE 4);
-by Auto_tac;
-qed "mult_eq_1_iff";
-AddIffs [zero_lt_mult_iff, mult_eq_1_iff];
-
-(*Cancellation law for division*)
-Goal "[| 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);
-by (asm_simp_tac (simpset() addsimps [div_less, zero_lt_mult_iff,
- mult_lt_mono2]) 2);
-by (asm_full_simp_tac
- (simpset() addsimps [not_lt_iff_le,
- zero_lt_mult_iff, le_refl RS mult_le_mono, div_geq,
- diff_mult_distrib2 RS sym,
- div_termination RS ltD]) 1);
-qed "div_cancel";
-
-Goal "[| 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);
-by (excluded_middle_tac "x<n" 1);
-by (asm_simp_tac (simpset() addsimps [mod_less, zero_lt_mult_iff,
- mult_lt_mono2]) 2);
-by (asm_full_simp_tac
- (simpset() addsimps [not_lt_iff_le,
- zero_lt_mult_iff, le_refl RS mult_le_mono, mod_geq,
- diff_mult_distrib2 RS sym,
- div_termination RS ltD]) 1);
-qed "mult_mod_distrib";
-
-(*Lemma for gcd*)
-Goal "m = m#*n ==> natify(n)=1 | m=0";
-by (subgoal_tac "m: nat" 1);
-by (etac ssubst 2);
-by (rtac disjCI 1);
-by (dtac sym 1);
-by (rtac Ord_linear_lt 1 THEN REPEAT_SOME (ares_tac [nat_into_Ord,nat_1I]));
-by (dtac (nat_into_Ord RS Ord_0_lt RSN (2,mult_lt_mono2)) 3);
-by Auto_tac;
-by (subgoal_tac "m #* n = 0" 1);
-by (stac (mult_natify2 RS sym) 2);
-by (auto_tac (claset(), simpset() delsimps [mult_natify2]));
-qed "mult_eq_self_implies_10";
-
-(*Thanks to Sten Agerholm*)
-Goal "[| k#+m le k#+n; m: nat; n: nat |] ==> m le n";
-by (res_inst_tac [("P", "natify(k)#+m le natify(k)#+n")] rev_mp 1);
-by (res_inst_tac [("n","natify(k)")] nat_induct 2);
-by Auto_tac;
-qed "add_le_elim1";
-
-Goal "[| m<n; n: nat |] ==> EX k: nat. n = succ(m#+k)";
-by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
-by (etac rev_mp 1);
-by (induct_tac "n" 1);
-by (ALLGOALS (simp_tac (simpset() addsimps [le_iff])));
-by (blast_tac (claset() addSEs [leE]
- addSIs [add_0_right RS sym, add_succ_right RS sym]) 1);
-qed_spec_mp "less_imp_Suc_add";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ArithSimp.ML Mon Aug 07 10:29:54 2000 +0200
@@ -0,0 +1,406 @@
+(* Title: ZF/ArithSimp.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 2000 University of Cambridge
+
+Arithmetic with simplification
+*)
+
+
+Addsimprocs ArithData.nat_cancel;
+
+
+(*** Difference ***)
+
+Goal "m #- m = 0";
+by (subgoal_tac "natify(m) #- natify(m) = 0" 1);
+by (rtac (natify_in_nat RS nat_induct) 2);
+by Auto_tac;
+qed "diff_self_eq_0";
+
+(**Addition is the inverse of subtraction**)
+
+(*We need m:nat even if we replace the RHS by natify(m), for consider e.g.
+ n=2, m=omega; then n + (m-n) = 2 + (0-2) = 2 ~= 0 = natify(m).*)
+Goal "[| n le m; m:nat |] ==> n #+ (m#-n) = m";
+by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
+by (etac rev_mp 1);
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by Auto_tac;
+qed "add_diff_inverse";
+
+Goal "[| n le m; m:nat |] ==> (m#-n) #+ n = m";
+by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
+by (asm_simp_tac (simpset() addsimps [add_commute, add_diff_inverse]) 1);
+qed "add_diff_inverse2";
+
+(*Proof is IDENTICAL to that of add_diff_inverse*)
+Goal "[| n le m; m:nat |] ==> succ(m) #- n = succ(m#-n)";
+by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
+by (etac rev_mp 1);
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "diff_succ";
+
+Goal "[| m: nat; n: nat |] ==> 0 < (n #- m) <-> m<n";
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (ALLGOALS Asm_simp_tac);
+qed "zero_less_diff";
+Addsimps [zero_less_diff];
+
+
+(** Difference distributes over multiplication **)
+
+Goal "(m #- n) #* k = (m #* k) #- (n #* k)";
+by (subgoal_tac "(natify(m) #- natify(n)) #* natify(k) = \
+\ (natify(m) #* natify(k)) #- (natify(n) #* natify(k))" 1);
+by (res_inst_tac [("m","natify(m)"),("n","natify(n)")] diff_induct 2);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [diff_cancel])));
+qed "diff_mult_distrib" ;
+
+Goal "k #* (m #- n) = (k #* m) #- (k #* n)";
+by (simp_tac
+ (simpset() addsimps [inst "m" "k" mult_commute, diff_mult_distrib]) 1);
+qed "diff_mult_distrib2";
+
+
+(*** Remainder ***)
+
+(*We need m:nat even with natify*)
+Goal "[| 0<n; n le m; m:nat |] ==> m #- n < m";
+by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
+by (etac rev_mp 1);
+by (etac rev_mp 1);
+by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_le_self])));
+qed "div_termination";
+
+val div_rls = (*for mod and div*)
+ nat_typechecks @
+ [Ord_transrec_type, apply_funtype, div_termination RS ltD,
+ nat_into_Ord, not_lt_iff_le RS iffD1];
+
+val div_ss = simpset() addsimps [div_termination RS ltD,
+ not_lt_iff_le RS iffD2];
+
+Goalw [raw_mod_def] "[| m:nat; n:nat |] ==> raw_mod (m, n) : nat";
+by (rtac Ord_transrec_type 1);
+by (auto_tac(claset(), simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff]));
+by (REPEAT (ares_tac div_rls 1));
+qed "raw_mod_type";
+
+Goalw [mod_def] "m mod n : nat";
+by (simp_tac (simpset() addsimps [mod_def, raw_mod_type]) 1);
+qed "mod_type";
+AddTCs [mod_type];
+AddIffs [mod_type];
+
+
+(** Aribtrary definitions for division by zero. Useful to simplify
+ certain equations **)
+
+Goalw [div_def] "a div 0 = 0";
+by (rtac (raw_div_def RS def_transrec RS trans) 1);
+by (Asm_simp_tac 1);
+qed "DIVISION_BY_ZERO_DIV"; (*NOT for adding to default simpset*)
+
+Goalw [mod_def] "a mod 0 = natify(a)";
+by (rtac (raw_mod_def RS def_transrec RS trans) 1);
+by (Asm_simp_tac 1);
+qed "DIVISION_BY_ZERO_MOD"; (*NOT for adding to default simpset*)
+
+fun div_undefined_case_tac s i =
+ case_tac s i THEN
+ asm_full_simp_tac
+ (simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff]) (i+1) THEN
+ asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO_DIV,
+ DIVISION_BY_ZERO_MOD]) i;
+
+Goal "m<n ==> raw_mod (m,n) = m";
+by (rtac (raw_mod_def RS def_transrec RS trans) 1);
+by (asm_simp_tac (simpset() addsimps [div_termination RS ltD]) 1);
+qed "raw_mod_less";
+
+Goal "[| m<n; n : nat |] ==> m mod n = m";
+by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
+by (asm_simp_tac (simpset() addsimps [mod_def, raw_mod_less]) 1);
+qed "mod_less";
+
+Goal "[| 0<n; n le m; m:nat |] ==> raw_mod (m, n) = raw_mod (m#-n, n)";
+by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
+by (rtac (raw_mod_def RS def_transrec RS trans) 1);
+by (asm_simp_tac div_ss 1);
+by (Blast_tac 1);
+qed "raw_mod_geq";
+
+Goal "[| n le m; m:nat |] ==> m mod n = (m#-n) mod n";
+by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
+by (div_undefined_case_tac "n=0" 1);
+by (asm_simp_tac (simpset() addsimps [mod_def, raw_mod_geq]) 1);
+qed "mod_geq";
+
+Addsimps [mod_less];
+
+
+(*** Division ***)
+
+Goalw [raw_div_def] "[| m:nat; n:nat |] ==> raw_div (m, n) : nat";
+by (rtac Ord_transrec_type 1);
+by (auto_tac(claset(), simpset() addsimps [nat_into_Ord RS Ord_0_lt_iff]));
+by (REPEAT (ares_tac div_rls 1));
+qed "raw_div_type";
+
+Goalw [div_def] "m div n : nat";
+by (simp_tac (simpset() addsimps [div_def, raw_div_type]) 1);
+qed "div_type";
+AddTCs [div_type];
+AddIffs [div_type];
+
+Goal "m<n ==> raw_div (m,n) = 0";
+by (rtac (raw_div_def RS def_transrec RS trans) 1);
+by (asm_simp_tac (simpset() addsimps [div_termination RS ltD]) 1);
+qed "raw_div_less";
+
+Goal "[| m<n; n : nat |] ==> m div n = 0";
+by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
+by (asm_simp_tac (simpset() addsimps [div_def, raw_div_less]) 1);
+qed "div_less";
+
+Goal "[| 0<n; n le m; m:nat |] ==> raw_div(m,n) = succ(raw_div(m#-n, n))";
+by (subgoal_tac "n ~= 0" 1);
+by (Blast_tac 2);
+by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
+by (rtac (raw_div_def RS def_transrec RS trans) 1);
+by (asm_simp_tac div_ss 1);
+qed "raw_div_geq";
+
+Goal "[| 0<n; n le m; m:nat |] ==> m div n = succ ((m#-n) div n)";
+by (ftac lt_nat_in_nat 1 THEN etac nat_succI 1);
+by (asm_simp_tac (simpset() addsimps [div_def, raw_div_geq]) 1);
+qed "div_geq";
+
+Addsimps [div_less, div_geq];
+
+
+(*A key result*)
+Goal "[| m: nat; n: nat |] ==> (m div n)#*n #+ m mod n = m";
+by (div_undefined_case_tac "n=0" 1);
+by (etac complete_induct 1);
+by (case_tac "x<n" 1);
+(*case n le x*)
+by (asm_full_simp_tac
+ (simpset() addsimps [not_lt_iff_le, add_assoc, mod_geq,
+ div_termination RS ltD, add_diff_inverse]) 2);
+(*case x<n*)
+by (Asm_simp_tac 1);
+val lemma = result();
+
+Goal "(m div n)#*n #+ m mod n = natify(m)";
+by (subgoal_tac
+ "(natify(m) div natify(n))#*natify(n) #+ natify(m) mod natify(n) = \
+\ natify(m)" 1);
+by (stac lemma 2);
+by Auto_tac;
+qed "mod_div_equality_natify";
+
+Goal "m: nat ==> (m div n)#*n #+ m mod n = m";
+by (asm_simp_tac (simpset() addsimps [mod_div_equality_natify]) 1);
+qed "mod_div_equality";
+
+
+(*** Further facts about mod (mainly for mutilated chess board) ***)
+
+Goal "[| 0<n; m:nat; n:nat |] \
+\ ==> succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))";
+by (etac complete_induct 1);
+by (excluded_middle_tac "succ(x)<n" 1);
+(* case succ(x) < n *)
+by (asm_simp_tac (simpset() addsimps [nat_le_refl RS lt_trans,
+ succ_neq_self]) 2);
+by (asm_simp_tac (simpset() addsimps [ltD RS mem_imp_not_eq]) 2);
+(* case n le succ(x) *)
+by (asm_full_simp_tac (simpset() addsimps [mod_geq, not_lt_iff_le]) 1);
+by (etac leE 1);
+(*equality case*)
+by (asm_full_simp_tac (simpset() addsimps [diff_self_eq_0]) 2);
+by (asm_simp_tac (simpset() addsimps [mod_geq, div_termination RS ltD,
+ diff_succ]) 1);
+val lemma = result();
+
+Goal "n:nat ==> \
+\ succ(m) mod n = (if succ(m mod n) = n then 0 else succ(m mod n))";
+by (case_tac "n=0" 1);
+by (asm_simp_tac (simpset() addsimps [natify_succ, DIVISION_BY_ZERO_MOD]) 1);
+by (subgoal_tac
+ "natify(succ(m)) mod n = \
+\ (if succ(natify(m) mod n) = n then 0 else succ(natify(m) mod n))" 1);
+by (stac natify_succ 2);
+by (rtac lemma 2);
+by (auto_tac(claset(),
+ simpset() delsimps [natify_succ]
+ addsimps [nat_into_Ord RS Ord_0_lt_iff]));
+qed "mod_succ";
+
+Goal "[| 0<n; n:nat |] ==> m mod n < n";
+by (subgoal_tac "natify(m) mod n < n" 1);
+by (res_inst_tac [("i","natify(m)")] complete_induct 2);
+by (case_tac "x<n" 3);
+(*case x<n*)
+by (Asm_simp_tac 3);
+(*case n le x*)
+by (asm_full_simp_tac
+ (simpset() addsimps [mod_geq, not_lt_iff_le, div_termination RS ltD]) 3);
+by Auto_tac;
+qed "mod_less_divisor";
+
+Goal "b<2 ==> k mod 2 = b | k mod 2 = (if b=1 then 0 else 1)";
+by (subgoal_tac "k mod 2: 2" 1);
+by (asm_simp_tac (simpset() addsimps [mod_less_divisor RS ltD]) 2);
+by (dtac ltD 1);
+by Auto_tac;
+qed "mod2_cases";
+
+Goal "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 (auto_tac (claset(), simpset() addsimps [mod_succ]));
+qed "mod2_succ_succ";
+
+Addsimps [mod2_succ_succ];
+
+Goal "(m#+m#+n) mod 2 = n mod 2";
+by (subgoal_tac "(natify(m)#+natify(m)#+n) mod 2 = n mod 2" 1);
+by (res_inst_tac [("n","natify(m)")] nat_induct 2);
+by Auto_tac;
+qed "mod2_add_more";
+
+Goal "(m#+m) mod 2 = 0";
+by (cut_inst_tac [("n","0")] mod2_add_more 1);
+by Auto_tac;
+qed "mod2_add_self";
+
+Addsimps [mod2_add_more, mod2_add_self];
+
+
+(**** Additional theorems about "le" ****)
+
+Goal "m:nat ==> m le (m #+ n)";
+by (induct_tac "m" 1);
+by (ALLGOALS Asm_simp_tac);
+qed "add_le_self";
+
+Goal "m:nat ==> m le (n #+ m)";
+by (stac add_commute 1);
+by (etac add_le_self 1);
+qed "add_le_self2";
+
+(*** Monotonicity of Multiplication ***)
+
+Goal "[| i le j; j:nat |] ==> (i#*k) le (j#*k)";
+by (subgoal_tac "natify(i)#*natify(k) le j#*natify(k)" 1);
+by (ftac lt_nat_in_nat 2);
+by (res_inst_tac [("n","natify(k)")] nat_induct 3);
+by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [add_le_mono])));
+qed "mult_le_mono1";
+
+(* le monotonicity, BOTH arguments*)
+Goal "[| 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 (assume_tac 1));
+by (EVERY [stac mult_commute 1,
+ stac mult_commute 1,
+ rtac mult_le_mono1 1]);
+by (REPEAT (assume_tac 1));
+qed "mult_le_mono";
+
+(*strict, in 1st argument; proof is by induction on k>0.
+ I can't see how to relax the typing conditions.*)
+Goal "[| i<j; 0<k; j:nat; k:nat |] ==> k#*i < k#*j";
+by (etac zero_lt_natE 1);
+by (ftac lt_nat_in_nat 2);
+by (ALLGOALS Asm_simp_tac);
+by (induct_tac "x" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [add_lt_mono])));
+qed "mult_lt_mono2";
+
+Goal "[| i<j; 0<k; j:nat; k:nat |] ==> i#*k < j#*k";
+by (asm_simp_tac (simpset() addsimps [mult_lt_mono2,
+ inst "n" "k" mult_commute]) 1);
+qed "mult_lt_mono1";
+
+Goal "m#+n = 0 <-> natify(m)=0 & natify(n)=0";
+by (subgoal_tac "natify(m) #+ natify(n) = 0 <-> natify(m)=0 & natify(n)=0" 1);
+by (res_inst_tac [("n","natify(m)")] natE 2);
+ by (res_inst_tac [("n","natify(n)")] natE 4);
+by Auto_tac;
+qed "add_eq_0_iff";
+AddIffs [add_eq_0_iff];
+
+Goal "0 < m#*n <-> 0 < natify(m) & 0 < natify(n)";
+by (subgoal_tac "0 < natify(m)#*natify(n) <-> \
+\ 0 < natify(m) & 0 < natify(n)" 1);
+by (res_inst_tac [("n","natify(m)")] natE 2);
+ by (res_inst_tac [("n","natify(n)")] natE 4);
+ by (res_inst_tac [("n","natify(n)")] natE 3);
+by Auto_tac;
+qed "zero_lt_mult_iff";
+
+Goal "m#*n = 1 <-> natify(m)=1 & natify(n)=1";
+by (subgoal_tac "natify(m) #* natify(n) = 1 <-> natify(m)=1 & natify(n)=1" 1);
+by (res_inst_tac [("n","natify(m)")] natE 2);
+ by (res_inst_tac [("n","natify(n)")] natE 4);
+by Auto_tac;
+qed "mult_eq_1_iff";
+AddIffs [zero_lt_mult_iff, mult_eq_1_iff];
+
+(*Cancellation law for division*)
+Goal "[| 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);
+by (asm_simp_tac (simpset() addsimps [div_less, zero_lt_mult_iff,
+ mult_lt_mono2]) 2);
+by (asm_full_simp_tac
+ (simpset() addsimps [not_lt_iff_le,
+ zero_lt_mult_iff, le_refl RS mult_le_mono, div_geq,
+ diff_mult_distrib2 RS sym,
+ div_termination RS ltD]) 1);
+qed "div_cancel";
+
+Goal "[| 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);
+by (excluded_middle_tac "x<n" 1);
+by (asm_simp_tac (simpset() addsimps [mod_less, zero_lt_mult_iff,
+ mult_lt_mono2]) 2);
+by (asm_full_simp_tac
+ (simpset() addsimps [not_lt_iff_le,
+ zero_lt_mult_iff, le_refl RS mult_le_mono, mod_geq,
+ diff_mult_distrib2 RS sym,
+ div_termination RS ltD]) 1);
+qed "mult_mod_distrib";
+
+(*Lemma for gcd*)
+Goal "m = m#*n ==> natify(n)=1 | m=0";
+by (subgoal_tac "m: nat" 1);
+by (etac ssubst 2);
+by (rtac disjCI 1);
+by (dtac sym 1);
+by (rtac Ord_linear_lt 1 THEN REPEAT_SOME (ares_tac [nat_into_Ord,nat_1I]));
+by (dtac (nat_into_Ord RS Ord_0_lt RSN (2,mult_lt_mono2)) 3);
+by Auto_tac;
+by (subgoal_tac "m #* n = 0" 1);
+by (stac (mult_natify2 RS sym) 2);
+by (auto_tac (claset(), simpset() delsimps [mult_natify2]));
+qed "mult_eq_self_implies_10";
+
+Goal "[| m<n; n: nat |] ==> EX k: nat. n = succ(m#+k)";
+by (ftac lt_nat_in_nat 1 THEN assume_tac 1);
+by (etac rev_mp 1);
+by (induct_tac "n" 1);
+by (ALLGOALS (simp_tac (simpset() addsimps [le_iff])));
+by (blast_tac (claset() addSEs [leE]
+ addSIs [add_0_right RS sym, add_succ_right RS sym]) 1);
+qed_spec_mp "less_imp_succ_add";
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ArithSimp.thy Mon Aug 07 10:29:54 2000 +0200
@@ -0,0 +1,11 @@
+(* Title: ZF/ArithSimp.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 2000 University of Cambridge
+
+Arithmetic with simplification
+*)
+
+theory ArithSimp = Arith
+files "arith_data.ML":
+end
--- a/src/ZF/CardinalArith.thy Mon Aug 07 10:29:04 2000 +0200
+++ b/src/ZF/CardinalArith.thy Mon Aug 07 10:29:54 2000 +0200
@@ -6,7 +6,7 @@
Cardinal Arithmetic
*)
-CardinalArith = Cardinal + OrderArith + Arith + Finite +
+CardinalArith = Cardinal + OrderArith + ArithSimp + Finite +
consts
InfCard :: i=>o
--- a/src/ZF/Integ/Bin.ML Mon Aug 07 10:29:04 2000 +0200
+++ b/src/ZF/Integ/Bin.ML Mon Aug 07 10:29:54 2000 +0200
@@ -105,7 +105,7 @@
by (ALLGOALS (asm_simp_tac (simpset() addsimps zadd_ac)));
qed "integ_of_succ";
-Goal "w: bin ==> integ_of(bin_pred(w)) = $~ ($#1) $+ integ_of(w)";
+Goal "w: bin ==> integ_of(bin_pred(w)) = $- ($#1) $+ integ_of(w)";
by (etac bin.induct 1);
by (Simp_tac 1);
by (Simp_tac 1);
@@ -118,7 +118,7 @@
(*** bin_minus: (unary!) negation of binary integers ***)
-Goal "w: bin ==> integ_of(bin_minus(w)) = $~ integ_of(w)";
+Goal "w: bin ==> integ_of(bin_minus(w)) = $- integ_of(w)";
by (etac bin.induct 1);
by (Simp_tac 1);
by (Simp_tac 1);
@@ -238,6 +238,41 @@
qed "bin_mult_BIT0";
+(** Simplification rules with integer constants **)
+
+Goal "#0 $+ z = intify(z)";
+by (Simp_tac 1);
+qed "zadd_0_intify";
+
+Goal "z $+ #0 = intify(z)";
+by (Simp_tac 1);
+qed "zadd_0_right_intify";
+
+Addsimps [zadd_0_intify, zadd_0_right_intify];
+
+Goal "#1 $* z = intify(z)";
+by (Simp_tac 1);
+qed "zmult_1_intify";
+
+Goal "z $* #1 = intify(z)";
+by (stac zmult_commute 1);
+by (Simp_tac 1);
+qed "zmult_1_right_intify";
+
+Addsimps [zmult_1_intify, zmult_1_right_intify];
+
+Goal "#0 $* z = #0";
+by (Simp_tac 1);
+qed "zmult_0";
+
+Goal "z $* #0 = #0";
+by (stac zmult_commute 1);
+by (Simp_tac 1);
+qed "zmult_0_right";
+
+Addsimps [zmult_0, zmult_0_right];
+
+
(*Delete the original rewrites, with their clumsy conditional expressions*)
Delsimps [bin_succ_BIT, bin_pred_BIT, bin_minus_BIT,
NCons_Pls, NCons_Min, bin_adder_BIT, bin_mult_BIT];
--- a/src/ZF/Integ/Bin.thy Mon Aug 07 10:29:04 2000 +0200
+++ b/src/ZF/Integ/Bin.thy Mon Aug 07 10:29:54 2000 +0200
@@ -41,7 +41,7 @@
primrec
integ_of_Pls "integ_of (Pls) = $# 0"
- integ_of_Min "integ_of (Min) = $~($#1)"
+ integ_of_Min "integ_of (Min) = $-($#1)"
integ_of_BIT "integ_of (w BIT b) = $#b $+ integ_of(w) $+ integ_of(w)"
(** recall that cond(1,b,c)=b and cond(0,b,c)=0 **)
--- a/src/ZF/Integ/Int.ML Mon Aug 07 10:29:04 2000 +0200
+++ b/src/ZF/Integ/Int.ML Mon Aug 07 10:29:54 2000 +0200
@@ -6,10 +6,10 @@
The integers as equivalence classes over nat*nat.
Could also prove...
-"znegative(z) ==> $# zmagnitude(z) = $~ z"
+"znegative(z) ==> $# zmagnitude(z) = $- z"
"~ znegative(z) ==> $# zmagnitude(z) = z"
-$< is a linear ordering
$+ and $* are monotonic wrt $<
+[| m: nat; n: nat; n le m |] ==> $# (m #- n) = ($#m) $- ($#n)
*)
AddSEs [quotientE];
@@ -50,14 +50,10 @@
AddSIs [intrelI];
AddSEs [intrelE];
-val eqa::eqb::prems = goal Arith.thy
- "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2 |] ==> x1 #+ y3 = x3 #+ y1";
-by (res_inst_tac [("k","x2")] add_left_cancel 1);
-by (rtac (add_left_commute RS trans) 1);
-by Auto_tac;
-by (stac eqb 1);
-by (rtac (add_left_commute RS trans) 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps [eqa, add_left_commute])));
+Goal "[| x1 #+ y2 = x2 #+ y1; x2 #+ y3 = x3 #+ y2 |] ==> x1 #+ y3 = x3 #+ y1";
+by (rtac sym 1);
+by (REPEAT (etac add_left_cancel 1));
+by (ALLGOALS Asm_simp_tac);
qed "int_trans_lemma";
Goalw [equiv_def, refl_def, sym_def, trans_def]
@@ -123,7 +119,7 @@
by (simp_tac (simpset() addsimps [int_of_def]) 1);
qed "int_of_natify";
-Goal "$~ (intify(m)) = $~ m";
+Goal "$- (intify(m)) = $- m";
by (simp_tac (simpset() addsimps [zminus_def]) 1);
qed "zminus_intify";
@@ -140,6 +136,17 @@
qed "zadd_intify2";
Addsimps [zadd_intify1, zadd_intify2];
+(** Subtraction **)
+
+Goal "intify(x) $- y = x $- y";
+by (simp_tac (simpset() addsimps [zdiff_def]) 1);
+qed "zdiff_intify1";
+
+Goal "x $- intify(y) = x $- y";
+by (simp_tac (simpset() addsimps [zdiff_def]) 1);
+qed "zdiff_intify2";
+Addsimps [zdiff_intify1, zdiff_intify2];
+
(** Multiplication **)
Goal "intify(x) $* y = x $* y";
@@ -151,6 +158,17 @@
qed "zmult_intify2";
Addsimps [zmult_intify1, zmult_intify2];
+(** Orderings **)
+
+Goal "intify(x) $< y <-> x $< y";
+by (simp_tac (simpset() addsimps [zless_def]) 1);
+qed "zless_intify1";
+
+Goal "x $< intify(y) <-> x $< y";
+by (simp_tac (simpset() addsimps [zless_def]) 1);
+qed "zless_intify2";
+Addsimps [zless_intify1, zless_intify2];
+
(**** zminus: unary negation on int ****)
@@ -168,7 +186,7 @@
by (typecheck_tac (tcset() addTCs [zminus_ize UN_equiv_class_type]));
qed "raw_zminus_type";
-Goalw [zminus_def] "$~z : int";
+Goalw [zminus_def] "$-z : int";
by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type]) 1);
qed "zminus_type";
AddIffs [zminus_type];
@@ -182,13 +200,13 @@
by (auto_tac (claset() addDs [eq_intrelD], simpset() addsimps add_ac));
qed "raw_zminus_inject";
-Goalw [zminus_def] "$~z = $~w ==> intify(z) = intify(w)";
+Goalw [zminus_def] "$-z = $-w ==> intify(z) = intify(w)";
by (blast_tac (claset() addSDs [raw_zminus_inject]) 1);
qed "zminus_inject_intify";
AddSDs [zminus_inject_intify];
-Goal "[| $~z = $~w; z: int; w: int |] ==> z=w";
+Goal "[| $-z = $-w; z: int; w: int |] ==> z=w";
by Auto_tac;
qed "zminus_inject";
@@ -200,7 +218,7 @@
Goalw [zminus_def]
"[| x: nat; y: nat |] \
-\ ==> $~ (intrel``{<x,y>}) = intrel `` {<y,x>}";
+\ ==> $- (intrel``{<x,y>}) = intrel `` {<y,x>}";
by (asm_simp_tac (simpset() addsimps [raw_zminus, image_intrel_int]) 1);
qed "zminus";
@@ -208,18 +226,18 @@
by (auto_tac (claset(), simpset() addsimps [raw_zminus]));
qed "raw_zminus_zminus";
-Goal "$~ ($~ z) = intify(z)";
+Goal "$- ($- z) = intify(z)";
by (simp_tac (simpset() addsimps [zminus_def, raw_zminus_type,
raw_zminus_zminus]) 1);
qed "zminus_zminus_intify";
-Goalw [int_of_def] "$~ ($#0) = $#0";
+Goalw [int_of_def] "$- ($#0) = $#0";
by (simp_tac (simpset() addsimps [zminus]) 1);
qed "zminus_0";
Addsimps [zminus_zminus_intify, zminus_0];
-Goal "z : int ==> $~ ($~ z) = z";
+Goal "z : int ==> $- ($- z) = z";
by (Asm_simp_tac 1);
qed "zminus_zminus";
@@ -232,20 +250,21 @@
by (dres_inst_tac [("psi", "?lhs=?rhs")] asm_rl 1);
by (dres_inst_tac [("psi", "?lhs<?rhs")] asm_rl 1);
by (force_tac (claset(),
- simpset() addsimps [add_le_self2 RS le_imp_not_lt]) 1);
+ simpset() addsimps [add_le_self2 RS le_imp_not_lt,
+ natify_succ]) 1);
qed "not_znegative_int_of";
Addsimps [not_znegative_int_of];
AddSEs [not_znegative_int_of RS notE];
-Goalw [znegative_def, int_of_def] "znegative($~ $# succ(n))";
-by (asm_simp_tac (simpset() addsimps [zminus]) 1);
+Goalw [znegative_def, int_of_def] "znegative($- $# succ(n))";
+by (asm_simp_tac (simpset() addsimps [zminus, natify_succ]) 1);
by (blast_tac (claset() addIs [nat_0_le]) 1);
qed "znegative_zminus_int_of";
Addsimps [znegative_zminus_int_of];
-Goalw [znegative_def, int_of_def] "~ znegative($~ $# n) ==> natify(n)=0";
+Goalw [znegative_def, int_of_def] "~ znegative($- $# n) ==> natify(n)=0";
by (asm_full_simp_tac (simpset() addsimps [zminus, image_singleton_iff]) 1);
by (dres_inst_tac [("x","0")] spec 1);
by (auto_tac(claset(),
@@ -263,7 +282,7 @@
by (asm_simp_tac (simpset() addsimps [int_of_eq]) 1);
qed "natify_int_of_eq";
-Goalw [zmagnitude_def] "zmagnitude($~ $# n) = natify(n)";
+Goalw [zmagnitude_def] "zmagnitude($- $# n) = natify(n)";
by (rtac the_equality 1);
by (auto_tac((claset() addSDs [not_znegative_imp_zero, natify_int_of_eq],
simpset())
@@ -300,17 +319,12 @@
Goalw [int_def, znegative_def, int_of_def]
- "[| z: int; znegative(z) |] ==> EX n:nat. z = $~ ($# succ(n))";
-by (auto_tac(claset() addSDs [less_imp_Suc_add],
+ "[| z: int; znegative(z) |] ==> EX n:nat. z = $- ($# succ(n))";
+by (auto_tac(claset() addSDs [less_imp_succ_add],
simpset() addsimps [zminus, image_singleton_iff]));
-by (rename_tac "m n j k" 1);
-by (subgoal_tac "j #+ succ(m #+ k) = j #+ n" 1);
-by (rotate_tac ~2 2);
-by (asm_full_simp_tac (simpset() addsimps add_ac) 2);
-by (blast_tac (claset() addSDs [add_left_cancel]) 1);
qed "zneg_int_of";
-Goal "[| z: int; znegative(z) |] ==> $# (zmagnitude(z)) = $~ z";
+Goal "[| z: int; znegative(z) |] ==> $# (zmagnitude(z)) = $- z";
by (dtac zneg_int_of 1);
by Auto_tac;
qed "zneg_mag";
@@ -367,26 +381,28 @@
Goalw [int_def,int_of_def] "z : int ==> raw_zadd ($#0,z) = z";
by (auto_tac (claset(), simpset() addsimps [raw_zadd]));
-qed "raw_zadd_0";
+qed "raw_zadd_int0";
Goal "$#0 $+ z = intify(z)";
-by (asm_simp_tac (simpset() addsimps [zadd_def, raw_zadd_0]) 1);
-qed "zadd_0_intify";
-Addsimps [zadd_0_intify];
+by (asm_simp_tac (simpset() addsimps [zadd_def, raw_zadd_int0]) 1);
+qed "zadd_int0_intify";
+Addsimps [zadd_int0_intify];
Goal "z: int ==> $#0 $+ z = z";
by (Asm_simp_tac 1);
-qed "zadd_0";
+qed "zadd_int0";
Goalw [int_def]
- "[| z: int; w: int |] ==> $~ raw_zadd(z,w) = raw_zadd($~ z, $~ w)";
+ "[| z: int; w: int |] ==> $- raw_zadd(z,w) = raw_zadd($- z, $- w)";
by (auto_tac (claset(), simpset() addsimps [zminus,raw_zadd]));
qed "raw_zminus_zadd_distrib";
-Goal "$~ (z $+ w) = $~ z $+ $~ w";
+Goal "$- (z $+ w) = $- z $+ $- w";
by (simp_tac (simpset() addsimps [zadd_def, raw_zminus_zadd_distrib]) 1);
qed "zminus_zadd_distrib";
+Addsimps [zminus_zadd_distrib];
+
Goalw [int_def] "[| z: int; w: int |] ==> raw_zadd(z,w) = raw_zadd(w,z)";
by (auto_tac (claset(), simpset() addsimps raw_zadd::add_ac));
qed "raw_zadd_commute";
@@ -418,35 +434,32 @@
by (asm_simp_tac (simpset() addsimps [zadd]) 1);
qed "int_of_add";
-Goalw [int_def,int_of_def] "z : int ==> raw_zadd (z, $~ z) = $#0";
+Goalw [int_def,int_of_def] "z : int ==> raw_zadd (z, $- z) = $#0";
by (auto_tac (claset(), simpset() addsimps [zminus, raw_zadd, add_commute]));
qed "raw_zadd_zminus_inverse";
-Goal "z $+ ($~ z) = $#0";
+Goal "z $+ ($- z) = $#0";
by (simp_tac (simpset() addsimps [zadd_def]) 1);
by (stac (zminus_intify RS sym) 1);
by (rtac (intify_in_int RS raw_zadd_zminus_inverse) 1);
qed "zadd_zminus_inverse";
-Goal "($~ z) $+ z = $#0";
+Goal "($- z) $+ z = $#0";
by (simp_tac (simpset() addsimps [zadd_commute, zadd_zminus_inverse]) 1);
qed "zadd_zminus_inverse2";
Goal "z $+ $#0 = intify(z)";
-by (rtac ([zadd_commute, zadd_0_intify] MRS trans) 1);
-qed "zadd_0_right_intify";
-Addsimps [zadd_0_right_intify];
+by (rtac ([zadd_commute, zadd_int0_intify] MRS trans) 1);
+qed "zadd_int0_right_intify";
+Addsimps [zadd_int0_right_intify];
Goal "z:int ==> z $+ $#0 = z";
by (Asm_simp_tac 1);
-qed "zadd_0_right";
+qed "zadd_int0_right";
Addsimps [zadd_zminus_inverse, zadd_zminus_inverse2];
-(*Need properties of $- ??? Or use $- just as an abbreviation?
- [| m: nat; n: nat; n le m |] ==> $# (m #- n) = ($#m) $- ($#n)
-*)
(**** zmult: multiplication on int ****)
@@ -456,15 +469,14 @@
\ split(%x1 y1. split(%x2 y2. \
\ intrel``{<x1#*x2 #+ y1#*y2, x1#*y2 #+ y1#*x2>}, p2), p1))";
by (rtac (equiv_intrel RS congruent2_commuteI) 1);
-by Safe_tac;
-by (ALLGOALS Asm_simp_tac);
+by Auto_tac;
(*Proof that zmult is congruent in one argument*)
-by (asm_simp_tac
- (simpset() addsimps add_ac @ [add_mult_distrib_left RS sym]) 2);
-by (asm_simp_tac
- (simpset() addsimps [add_assoc RS sym, add_mult_distrib_left RS sym]) 2);
-(*Proof that zmult is commutative on representatives*)
-by (asm_simp_tac (simpset() addsimps mult_ac@add_ac) 1);
+by (rename_tac "x y" 1);
+by (forw_inst_tac [("t", "%u. x#*u")] (sym RS subst_context) 1);
+by (dres_inst_tac [("t", "%u. y#*u")] subst_context 1);
+by (REPEAT (etac add_left_cancel 1));
+by (asm_simp_tac (simpset() addsimps [add_mult_distrib_left]) 1);
+by Auto_tac;
qed "zmult_congruent2";
@@ -498,25 +510,25 @@
Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#0,z) = $#0";
by (auto_tac (claset(), simpset() addsimps [raw_zmult]));
-qed "raw_zmult_0";
+qed "raw_zmult_int0";
Goal "$#0 $* z = $#0";
-by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_0]) 1);
-qed "zmult_0";
-Addsimps [zmult_0];
+by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_int0]) 1);
+qed "zmult_int0";
+Addsimps [zmult_int0];
Goalw [int_def,int_of_def] "z : int ==> raw_zmult ($#1,z) = z";
by (auto_tac (claset(), simpset() addsimps [raw_zmult]));
-qed "raw_zmult_1";
+qed "raw_zmult_int1";
Goal "$#1 $* z = intify(z)";
-by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_1]) 1);
-qed "zmult_1_intify";
-Addsimps [zmult_1_intify];
+by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_int1]) 1);
+qed "zmult_int1_intify";
+Addsimps [zmult_int1_intify];
Goal "z : int ==> $#1 $* z = z";
by (Asm_simp_tac 1);
-qed "zmult_1";
+qed "zmult_int1";
Goalw [int_def] "[| z: int; w: int |] ==> raw_zmult(z,w) = raw_zmult(w,z)";
by (auto_tac (claset(), simpset() addsimps [raw_zmult] @ add_ac @ mult_ac));
@@ -527,18 +539,18 @@
qed "zmult_commute";
Goalw [int_def]
- "[| z: int; w: int |] ==> raw_zmult($~ z, w) = $~ raw_zmult(z, w)";
+ "[| z: int; w: int |] ==> raw_zmult($- z, w) = $- raw_zmult(z, w)";
by (auto_tac (claset(), simpset() addsimps [zminus, raw_zmult] @ add_ac));
qed "raw_zmult_zminus";
-Goal "($~ z) $* w = $~ (z $* w)";
+Goal "($- z) $* w = $- (z $* w)";
by (simp_tac (simpset() addsimps [zmult_def, raw_zmult_zminus]) 1);
by (stac (zminus_intify RS sym) 1 THEN rtac raw_zmult_zminus 1);
by Auto_tac;
qed "zmult_zminus";
Addsimps [zmult_zminus];
-Goal "($~ z) $* ($~ w) = (z $* w)";
+Goal "($- z) $* ($- w) = (z $* w)";
by (stac zmult_zminus 1);
by (stac zmult_commute 1 THEN stac zmult_zminus 1);
by (simp_tac (simpset() addsimps [zmult_commute])1);
@@ -588,3 +600,230 @@
[int_of_type, zminus_type, zmagnitude_type, zadd_type, zmult_type];
+(*** Subtraction laws ***)
+
+Goal "$#0 $- x = $-x";
+by (simp_tac (simpset() addsimps [zdiff_def]) 1);
+qed "zdiff_int0";
+
+Goal "x $- $#0 = intify(x)";
+by (simp_tac (simpset() addsimps [zdiff_def]) 1);
+qed "zdiff_int0_right";
+
+Goal "x $- x = $#0";
+by (simp_tac (simpset() addsimps [zdiff_def]) 1);
+qed "zdiff_self";
+
+Addsimps [zdiff_int0, zdiff_int0_right, zdiff_self];
+
+
+Goalw [zdiff_def] "(z1 $- z2) $* w = (z1 $* w) $- (z2 $* w)";
+by (stac zadd_zmult_distrib 1);
+by (simp_tac (simpset() addsimps [zmult_zminus]) 1);
+qed "zdiff_zmult_distrib";
+
+val zmult_commute'= inst "z" "w" zmult_commute;
+
+Goal "w $* (z1 $- z2) = (w $* z1) $- (w $* z2)";
+by (simp_tac (simpset() addsimps [zmult_commute',zdiff_zmult_distrib]) 1);
+qed "zdiff_zmult_distrib2";
+
+Goal "x $+ (y $- z) = (x $+ y) $- z";
+by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
+qed "zadd_zdiff_eq";
+
+Goal "(x $- y) $+ z = (x $+ z) $- y";
+by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
+qed "zdiff_zadd_eq";
+
+
+(*** "Less Than" ***)
+
+(*"Less than" is a linear ordering*)
+Goalw [int_def, zless_def, znegative_def, zdiff_def]
+ "[| z: int; w: int |] ==> z$<w | z=w | w$<z";
+by Auto_tac;
+by (asm_full_simp_tac
+ (simpset() addsimps [zadd, zminus, image_iff, Bex_def]) 1);
+by (res_inst_tac [("i", "xb#+ya"), ("j", "xc #+ y")] Ord_linear_lt 1);
+by (ALLGOALS (force_tac (claset() addSDs [spec],
+ simpset() addsimps add_ac)));
+qed "zless_linear_lemma";
+
+Goal "z$<w | intify(z)=intify(w) | w$<z";
+by (cut_inst_tac [("z"," intify(z)"),("w"," intify(w)")] zless_linear_lemma 1);
+by Auto_tac;
+qed "zless_linear";
+
+Goal "~ (z$<z)";
+by (auto_tac (claset(),
+ simpset() addsimps [zless_def, znegative_def, int_of_def]));
+by (rotate_tac 2 1);
+by Auto_tac;
+qed "zless_not_refl";
+AddIffs [zless_not_refl];
+
+(*This lemma allows direct proofs of other <-properties*)
+Goalw [zless_def, znegative_def, zdiff_def, int_def]
+ "[| w $< z; w: int; z: int |] ==> (EX n. z = w $+ $#(succ(n)))";
+by (auto_tac (claset() addSDs [less_imp_succ_add],
+ simpset() addsimps [zadd, zminus, int_of_def]));
+by (res_inst_tac [("x","k")] exI 1);
+by (etac add_left_cancel 1);
+by Auto_tac;
+qed "zless_imp_succ_zadd_lemma";
+
+Goal "w $< z ==> (EX n. w $+ $#(succ(n)) = intify(z))";
+by (subgoal_tac "intify(w) $< intify(z)" 1);
+by (dres_inst_tac [("w","intify(w)")] zless_imp_succ_zadd_lemma 1);
+by Auto_tac;
+qed "zless_imp_succ_zadd";
+
+Goalw [zless_def, znegative_def, zdiff_def, int_def]
+ "w : int ==> w $< w $+ $# succ(n)";
+by (auto_tac (claset(),
+ simpset() addsimps [zadd, zminus, int_of_def, image_iff]));
+by (res_inst_tac [("x","0")] exI 1);
+by Auto_tac;
+qed "zless_succ_zadd_lemma";
+
+Goal "w $< w $+ $# succ(n)";
+by (cut_facts_tac [intify_in_int RS zless_succ_zadd_lemma] 1);
+by Auto_tac;
+qed "zless_succ_zadd";
+
+Goal "w $< z <-> (EX n. w $+ $#(succ(n)) = intify(z))";
+by (rtac iffI 1);
+by (etac zless_imp_succ_zadd 1);
+by Auto_tac;
+by (cut_inst_tac [("w","w"),("n","n")] zless_succ_zadd 1);
+by Auto_tac;
+qed "zless_iff_succ_zadd";
+
+Goalw [zless_def, znegative_def, zdiff_def, int_def]
+ "[| x $< y; y $< z; x: int; y : int; z: int |] ==> x $< z";
+by (auto_tac (claset(),
+ simpset() addsimps [zadd, zminus, int_of_def, image_iff]));
+by (rename_tac "x1 x2 y1 y2" 1);
+by (res_inst_tac [("x","x1#+x2")] exI 1);
+by (res_inst_tac [("x","y1#+y2")] exI 1);
+by (auto_tac (claset(), simpset() addsimps [add_lt_mono]));
+by (rtac sym 1);
+by (REPEAT (etac add_left_cancel 1));
+by Auto_tac;
+qed "zless_trans_lemma";
+
+Goal "[| x $< y; y $< z |] ==> x $< z";
+by (subgoal_tac "intify(x) $< intify(z)" 1);
+by (res_inst_tac [("y", "intify(y)")] zless_trans_lemma 2);
+by Auto_tac;
+qed "zless_trans";
+
+
+Goalw [zle_def] "z $<= z";
+by Auto_tac;
+qed "zle_refl";
+
+Goalw [zle_def] "[| x $<= y; y $<= x |] ==> x=y";
+by (blast_tac (claset() addDs [zless_trans]) 1);
+qed "zle_anti_sym";
+
+Goalw [zle_def] "[| x $<= y; y $<= z |] ==> x $<= z";
+by (blast_tac (claset() addIs [zless_trans]) 1);
+qed "zle_trans";
+
+
+(*** More subtraction laws (for zcompare_rls): useful? ***)
+
+Goal "(x $- y) $- z = x $- (y $+ z)";
+by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
+qed "zdiff_zdiff_eq";
+
+Goal "x $- (y $- z) = (x $+ z) $- y";
+by (simp_tac (simpset() addsimps zdiff_def::zadd_ac) 1);
+qed "zdiff_zdiff_eq2";
+
+Goalw [zless_def, zdiff_def] "(x$-y $< z) <-> (x $< z $+ y)";
+by (simp_tac (simpset() addsimps zadd_ac) 1);
+qed "zdiff_zless_iff";
+
+Goalw [zless_def, zdiff_def] "(x $< z$-y) <-> (x $+ y $< z)";
+by (simp_tac (simpset() addsimps zadd_ac) 1);
+qed "zless_zdiff_iff";
+
+Goalw [zdiff_def] "[| x: int; z: int |] ==> (x$-y = z) <-> (x = z $+ y)";
+by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
+qed "zdiff_eq_iff";
+
+Goalw [zdiff_def] "[| x: int; z: int |] ==> (x = z$-y) <-> (x $+ y = z)";
+by (auto_tac (claset(), simpset() addsimps [zadd_assoc]));
+qed "eq_zdiff_iff";
+
+(**Could not prove these!
+Goalw [zle_def] "[| x: int; z: int |] ==> (x$-y $<= z) <-> (x $<= z $+ y)";
+by (asm_simp_tac (simpset() addsimps [zdiff_eq_iff, zless_zdiff_iff]) 1);
+by Auto_tac;
+qed "zdiff_zle_iff";
+
+Goalw [zle_def] "(x $<= z$-y) <-> (x $+ y $<= z)";
+by (simp_tac (simpset() addsimps [zdiff_zless_iff]) 1);
+qed "zle_zdiff_iff";
+**)
+
+
+(*** Monotonicity/cancellation results that could allow instantiation
+ of the CancelNumerals simprocs ***)
+
+Goal "[| w: int; w': int |] ==> (z $+ w' = z $+ w) <-> (w' = w)";
+by Safe_tac;
+by (dres_inst_tac [("t", "%x. x $+ ($-z)")] subst_context 1);
+by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
+qed "zadd_left_cancel";
+
+Goal "(z $+ w' = z $+ w) <-> intify(w') = intify(w)";
+by (rtac iff_trans 1);
+by (rtac zadd_left_cancel 2);
+by Auto_tac;
+qed "zadd_left_cancel_intify";
+
+Addsimps [zadd_left_cancel_intify];
+
+Goal "[| w: int; w': int |] ==> (w' $+ z = w $+ z) <-> (w' = w)";
+by Safe_tac;
+by (dres_inst_tac [("t", "%x. x $+ ($-z)")] subst_context 1);
+by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1);
+qed "zadd_right_cancel";
+
+Goal "(w' $+ z = w $+ z) <-> intify(w') = intify(w)";
+by (rtac iff_trans 1);
+by (rtac zadd_right_cancel 2);
+by Auto_tac;
+qed "zadd_right_cancel_intify";
+
+Addsimps [zadd_right_cancel_intify];
+
+
+Goal "(w' $+ z $< w $+ z) <-> (w' $< w)";
+by (simp_tac (simpset() addsimps [zdiff_zless_iff RS iff_sym]) 1);
+by (simp_tac (simpset() addsimps [zdiff_def, zadd_assoc]) 1);
+qed "zadd_right_cancel_zless";
+
+Goal "(z $+ w' $< z $+ w) <-> (w' $< w)";
+by (simp_tac (simpset() addsimps [inst "z" "z" zadd_commute,
+ zadd_right_cancel_zless]) 1);
+qed "zadd_left_cancel_zless";
+
+Addsimps [zadd_right_cancel_zless, zadd_left_cancel_zless];
+
+
+Goal "(w' $+ z $<= w $+ z) <-> (intify(w') $<= intify(w))";
+by (simp_tac (simpset() addsimps [zle_def]) 1);
+qed "zadd_right_cancel_zle";
+
+Goal "(z $+ w' $<= z $+ w) <-> (intify(w') $<= intify(w))";
+by (simp_tac (simpset() addsimps [inst "z" "z" zadd_commute,
+ zadd_right_cancel_zle]) 1);
+qed "zadd_left_cancel_zle";
+
+Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle];
+
--- a/src/ZF/Integ/Int.thy Mon Aug 07 10:29:04 2000 +0200
+++ b/src/ZF/Integ/Int.thy Mon Aug 07 10:29:54 2000 +0200
@@ -6,7 +6,7 @@
The integers as equivalence classes over nat*nat.
*)
-Int = EquivClass + Arith +
+Int = EquivClass + ArithSimp +
constdefs
intrel :: i
@@ -25,8 +25,8 @@
raw_zminus :: i=>i
"raw_zminus(z) == UN <x,y>: z. intrel``{<y,x>}"
- zminus :: i=>i ("$~ _" [80] 80)
- "$~ z == raw_zminus (intify(z))"
+ zminus :: i=>i ("$- _" [80] 80)
+ "$- z == raw_zminus (intify(z))"
znegative :: i=>o
"znegative(z) == EX x y. x<y & y:nat & <x,y>:z"
@@ -34,7 +34,7 @@
zmagnitude :: i=>i
"zmagnitude(z) ==
THE m. m : nat & ((~ znegative(z) & z = $# m) |
- (znegative(z) & $~ z = $# m))"
+ (znegative(z) & $- z = $# m))"
raw_zmult :: [i,i]=>i
(*Cannot use UN<x1,y2> here or in zadd because of the form of congruent2.
@@ -61,6 +61,9 @@
zless :: [i,i]=>o (infixl "$<" 50)
"z1 $< z2 == znegative(z1 $- z2)"
+ zle :: [i,i]=>o (infixl "$<=" 50)
+ "z1 $<= z2 == z1 $< z2 | z1=z2"
+
(*div and mod await definitions!*)
consts
"$'/" :: [i,i]=>i (infixl 70)
--- a/src/ZF/IsaMakefile Mon Aug 07 10:29:04 2000 +0200
+++ b/src/ZF/IsaMakefile Mon Aug 07 10:29:54 2000 +0200
@@ -26,7 +26,8 @@
FOL:
@cd $(SRC)/FOL; $(ISATOOL) make FOL
-$(OUT)/ZF: $(OUT)/FOL AC.ML AC.thy Arith.ML Arith.thy Bool.ML Bool.thy \
+$(OUT)/ZF: $(OUT)/FOL AC.ML AC.thy Arith.ML Arith.thy Bool.ML \
+ arith_data.ML ArithSimp.thy ArithSimp.ML Bool.thy \
Cardinal.ML Cardinal.thy CardinalArith.ML CardinalArith.thy \
Cardinal_AC.ML Cardinal_AC.thy Datatype.ML Datatype.thy Epsilon.ML \
Epsilon.thy Finite.ML Finite.thy Fixedpt.ML Fixedpt.thy Inductive.ML \
--- a/src/ZF/List.ML Mon Aug 07 10:29:04 2000 +0200
+++ b/src/ZF/List.ML Mon Aug 07 10:29:54 2000 +0200
@@ -308,16 +308,12 @@
Goal "[| xs: list(nat); ys: list(nat) |] ==> \
\ list_add(xs@ys) = list_add(ys) #+ list_add(xs)";
by (induct_tac "xs" 1);
-by (ALLGOALS
- (asm_simp_tac (simpset() addsimps [add_0_right, add_assoc RS sym])));
-by (rtac (add_commute RS subst_context) 1);
-by (REPEAT (ares_tac [refl, list_add_type] 1));
+by (ALLGOALS Asm_simp_tac);
qed "list_add_app";
Goal "l: list(nat) ==> list_add(rev(l)) = list_add(l)";
by (induct_tac "l" 1);
-by (ALLGOALS
- (asm_simp_tac (simpset() addsimps [list_add_app, add_0_right])));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps [list_add_app])));
qed "list_add_rev";
Goal "ls: list(list(nat)) ==> list_add(flat(ls)) = list_add(map(list_add,ls))";
--- a/src/ZF/List.thy Mon Aug 07 10:29:04 2000 +0200
+++ b/src/ZF/List.thy Mon Aug 07 10:29:54 2000 +0200
@@ -10,7 +10,7 @@
although complicating its derivation.
*)
-List = Datatype + Arith +
+List = Datatype + ArithSimp +
consts
list :: i=>i
--- a/src/ZF/ROOT.ML Mon Aug 07 10:29:04 2000 +0200
+++ b/src/ZF/ROOT.ML Mon Aug 07 10:29:54 2000 +0200
@@ -18,6 +18,8 @@
(*Add user sections for inductive/datatype definitions*)
use "thy_syntax";
+use "~~/src/Provers/Arith/cancel_numerals.ML";
+
use_thy "ZF";
use "Tools/typechk";
use_thy "mono";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/arith_data.ML Mon Aug 07 10:29:54 2000 +0200
@@ -0,0 +1,256 @@
+(* Title: ZF/arith_data.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 2000 University of Cambridge
+
+Arithmetic simplification: cancellation of common terms
+*)
+
+signature ARITH_DATA =
+sig
+ val nat_cancel: simproc list
+end;
+
+structure ArithData: ARITH_DATA =
+struct
+
+val iT = Ind_Syntax.iT;
+
+val zero = Const("0", iT);
+val succ = Const("succ", iT --> iT);
+fun mk_succ t = succ $ t;
+val one = mk_succ zero;
+
+(*Not FOLogic.mk_binop, since it calls fastype_of, which can fail*)
+fun mk_binop_i c (t,u) = Const (c, [iT,iT] ---> iT) $ t $ u;
+fun mk_binrel_i c (t,u) = Const (c, [iT,iT] ---> oT) $ t $ u;
+
+val mk_plus = mk_binop_i "Arith.add";
+
+(*Thus mk_sum[t] yields t+#0; longer sums don't have a trailing zero*)
+fun mk_sum [] = zero
+ | mk_sum [t,u] = mk_plus (t, u)
+ | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+
+(*this version ALWAYS includes a trailing zero*)
+fun long_mk_sum [] = zero
+ | long_mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
+
+val dest_plus = FOLogic.dest_bin "Arith.add" iT;
+
+(* dest_sum *)
+
+fun dest_sum (Const("0",_)) = []
+ | dest_sum (Const("succ",_) $ t) = one :: dest_sum t
+ | dest_sum (Const("Arith.add",_) $ t $ u) = dest_sum t @ dest_sum u
+ | dest_sum tm = [tm];
+
+(*Apply the given rewrite (if present) just once*)
+fun gen_trans_tac th2 None = all_tac
+ | gen_trans_tac th2 (Some th) = ALLGOALS (rtac (th RS th2));
+
+(*Use <-> or = depending on the type of t*)
+fun mk_eq_iff(t,u) =
+ if fastype_of t = iT then FOLogic.mk_eq(t,u)
+ else FOLogic.mk_iff(t,u);
+
+
+fun add_chyps chyps ct = Drule.list_implies (map cprop_of chyps, ct);
+
+fun prove_conv name tacs sg hyps (t,u) =
+ if t aconv u then None
+ else
+ let val ct = add_chyps hyps
+ (cterm_of sg (FOLogic.mk_Trueprop (mk_eq_iff(t, u))))
+ in Some
+ (hyps MRS
+ (prove_goalw_cterm_nocheck [] ct
+ (fn prems => cut_facts_tac prems 1 :: tacs)))
+ handle ERROR =>
+ (warning
+ ("Cancellation failed: no typing information? (" ^ name ^ ")");
+ None)
+ end;
+
+fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;
+fun prep_pat s = Thm.read_cterm (Theory.sign_of (the_context ()))
+ (s, TypeInfer.anyT ["logic"]);
+val prep_pats = map prep_pat;
+
+
+(*** Use CancelNumerals simproc without binary numerals,
+ just for cancellation ***)
+
+val mk_times = mk_binop_i "Arith.mult";
+
+fun mk_prod [] = one
+ | mk_prod [t] = t
+ | mk_prod (t :: ts) = if t = one then mk_prod ts
+ else mk_times (t, mk_prod ts);
+
+val dest_times = FOLogic.dest_bin "Arith.mult" iT;
+
+fun dest_prod t =
+ let val (t,u) = dest_times t
+ in dest_prod t @ dest_prod u end
+ handle TERM _ => [t];
+
+(*Dummy version: the only arguments are 0 and 1*)
+fun mk_coeff (0, t) = zero
+ | mk_coeff (1, t) = t
+ | mk_coeff _ = raise TERM("mk_coeff", []);
+
+(*Dummy version: the "coefficient" is always 1.
+ In the result, the factors are sorted terms*)
+fun dest_coeff t = (1, mk_prod (sort Term.term_ord (dest_prod t)));
+
+(*Find first coefficient-term THAT MATCHES u*)
+fun find_first_coeff past u [] = raise TERM("find_first_coeff", [])
+ | find_first_coeff past u (t::terms) =
+ let val (n,u') = dest_coeff t
+ in if u aconv u' then (n, rev past @ terms)
+ else find_first_coeff (t::past) u terms
+ end
+ handle TERM _ => find_first_coeff (t::past) u terms;
+
+
+(*Simplify #1*n and n*#1 to n*)
+val add_0s = [add_0_natify, add_0_right_natify];
+val add_succs = [add_succ, add_succ_right];
+val mult_1s = [mult_1_natify, mult_1_right_natify];
+val tc_rules = [natify_in_nat, add_type, diff_type, mult_type];
+val natifys = [natify_0, natify_ident, add_natify1, add_natify2,
+ add_natify1, add_natify2, diff_natify1, diff_natify2];
+
+(*Final simplification: cancel + and **)
+fun simplify_meta_eq rules =
+ mk_meta_eq o
+ simplify (FOL_ss addeqcongs[eq_cong2,iff_cong2]
+ delsimps iff_simps (*these could erase the whole rule!*)
+ addsimps rules)
+
+val final_rules = add_0s @ mult_1s @ [mult_0, mult_0_right];
+
+structure CancelNumeralsCommon =
+ struct
+ val mk_sum = mk_sum
+ val dest_sum = dest_sum
+ val mk_coeff = mk_coeff
+ val dest_coeff = dest_coeff
+ val find_first_coeff = find_first_coeff []
+ val norm_tac_ss1 = ZF_ss addsimps add_0s@add_succs@mult_1s@add_ac
+ val norm_tac_ss2 = ZF_ss addsimps add_ac@mult_ac@tc_rules@natifys
+ val norm_tac = ALLGOALS (asm_simp_tac norm_tac_ss1)
+ THEN ALLGOALS (asm_simp_tac norm_tac_ss2)
+ val numeral_simp_tac_ss = ZF_ss addsimps add_0s@tc_rules@natifys
+ val numeral_simp_tac = ALLGOALS (asm_simp_tac numeral_simp_tac_ss)
+ val simplify_meta_eq = simplify_meta_eq final_rules
+ end;
+
+
+structure EqCancelNumerals = CancelNumeralsFun
+ (open CancelNumeralsCommon
+ val prove_conv = prove_conv "nateq_cancel_numerals"
+ val mk_bal = FOLogic.mk_eq
+ val dest_bal = FOLogic.dest_bin "op =" iT
+ val bal_add1 = eq_add_iff RS iff_trans
+ val bal_add2 = eq_add_iff RS iff_trans
+ val trans_tac = gen_trans_tac iff_trans
+);
+
+structure LessCancelNumerals = CancelNumeralsFun
+ (open CancelNumeralsCommon
+ val prove_conv = prove_conv "natless_cancel_numerals"
+ val mk_bal = mk_binrel_i "Ordinal.op <"
+ val dest_bal = FOLogic.dest_bin "Ordinal.op <" iT
+ val bal_add1 = less_add_iff RS iff_trans
+ val bal_add2 = less_add_iff RS iff_trans
+ val trans_tac = gen_trans_tac iff_trans
+);
+
+structure DiffCancelNumerals = CancelNumeralsFun
+ (open CancelNumeralsCommon
+ val prove_conv = prove_conv "natdiff_cancel_numerals"
+ val mk_bal = mk_binop_i "Arith.diff"
+ val dest_bal = FOLogic.dest_bin "Arith.diff" iT
+ val bal_add1 = diff_add_eq RS trans
+ val bal_add2 = diff_add_eq RS trans
+ val trans_tac = gen_trans_tac trans
+);
+
+
+val nat_cancel =
+ map prep_simproc
+ [("nateq_cancel_numerals",
+ prep_pats ["l #+ m = n", "l = m #+ n",
+ "l #* m = n", "l = m #* n",
+ "succ(m) = n", "m = succ(n)"],
+ EqCancelNumerals.proc),
+ ("natless_cancel_numerals",
+ prep_pats ["l #+ m < n", "l < m #+ n",
+ "l #* m < n", "l < m #* n",
+ "succ(m) < n", "m < succ(n)"],
+ LessCancelNumerals.proc),
+ ("natdiff_cancel_numerals",
+ prep_pats ["(l #+ m) #- n", "l #- (m #+ n)",
+ "(l #* m) #- n", "l #- (m #* n)",
+ "succ(m) #- n", "m #- succ(n)"],
+ DiffCancelNumerals.proc)];
+
+end;
+
+(*examples:
+print_depth 22;
+set timing;
+set trace_simp;
+fun test s = (Goal s; by (Asm_simp_tac 1));
+
+test "x #+ y = x #+ z";
+test "y #+ x = x #+ z";
+test "x #+ y #+ z = x #+ z";
+test "y #+ (z #+ x) = z #+ x";
+test "x #+ y #+ z = (z #+ y) #+ (x #+ w)";
+test "x#*y #+ z = (z #+ y) #+ (y#*x #+ w)";
+
+test "x #+ succ(y) = x #+ z";
+test "x #+ succ(y) = succ(z #+ x)";
+test "succ(x) #+ succ(y) #+ z = succ(z #+ y) #+ succ(x #+ w)";
+
+test "(x #+ y) #- (x #+ z) = w";
+test "(y #+ x) #- (x #+ z) = dd";
+test "(x #+ y #+ z) #- (x #+ z) = dd";
+test "(y #+ (z #+ x)) #- (z #+ x) = dd";
+test "(x #+ y #+ z) #- ((z #+ y) #+ (x #+ w)) = dd";
+test "(x#*y #+ z) #- ((z #+ y) #+ (y#*x #+ w)) = dd";
+
+(*BAD occurrence of natify*)
+test "(x #+ succ(y)) #- (x #+ z) = dd";
+
+test "x #* y2 #+ y #* x2 = y #* x2 #+ x #* y2";
+
+test "(x #+ succ(y)) #- (succ(z #+ x)) = dd";
+test "(succ(x) #+ succ(y) #+ z) #- (succ(z #+ y) #+ succ(x #+ w)) = dd";
+
+(*use of typing information*)
+test "x : nat ==> x #+ y = x";
+test "x : nat --> x #+ y = x";
+test "x : nat ==> x #+ y < x";
+test "x : nat ==> x < y#+x";
+
+(*fails: no typing information isn't visible*)
+test "x #+ y = x";
+
+test "x #+ y < x #+ z";
+test "y #+ x < x #+ z";
+test "x #+ y #+ z < x #+ z";
+test "y #+ z #+ x < x #+ z";
+test "y #+ (z #+ x) < z #+ x";
+test "x #+ y #+ z < (z #+ y) #+ (x #+ w)";
+test "x#*y #+ z < (z #+ y) #+ (y#*x #+ w)";
+
+test "x #+ succ(y) < x #+ z";
+test "x #+ succ(y) < succ(z #+ x)";
+test "succ(x) #+ succ(y) #+ z < succ(z #+ y) #+ succ(x #+ w)";
+
+test "x #+ succ(y) le succ(z #+ x)";
+*)
--- a/src/ZF/ex/BinEx.ML Mon Aug 07 10:29:04 2000 +0200
+++ b/src/ZF/ex/BinEx.ML Mon Aug 07 10:29:54 2000 +0200
@@ -26,12 +26,12 @@
by (Simp_tac 1); (*300 msec*)
result();
-Goal "$~ #65745 = #-65745";
+Goal "$- #65745 = #-65745";
by (Simp_tac 1); (*80 msec*)
result();
(* negation of ~54321 *)
-Goal "$~ #-54321 = #54321";
+Goal "$- #-54321 = #54321";
by (Simp_tac 1); (*90 msec*)
result();
--- a/src/ZF/ex/Limit.ML Mon Aug 07 10:29:04 2000 +0200
+++ b/src/ZF/ex/Limit.ML Mon Aug 07 10:29:54 2000 +0200
@@ -1345,13 +1345,8 @@
by (asm_simp_tac (simpset() addsimps[diff_self_eq_0]) 1);
qed "e_less_eq";
-(* ARITH_CONV proves the following in HOL. Would like something similar
- in Isabelle/ZF. *)
-
Goal "succ(m#+n)#-m = succ(natify(n))";
-by (asm_simp_tac
- (simpset() delsimps [add_succ_right]
- addsimps [add_succ_right RS sym, diff_add_inverse]) 1);
+by (Asm_simp_tac 1);
val lemma_succ_sub = result();
Goalw [e_less_def]
@@ -1364,7 +1359,7 @@
qed "add1";
Goal "[| m le n; n: nat |] ==> EX k: nat. n = m #+ k";
-by (dtac less_imp_Suc_add 1);
+by (dtac less_imp_succ_add 1);
by Auto_tac;
val lemma_le_exists = result();
@@ -1725,7 +1720,7 @@
by (auto_tac (claset() addIs [e_gr_e_less_split_add], simpset()));
qed "eps_split_add_right_rev";
-(* Arithmetic, little support in Isabelle/ZF. *)
+(* Arithmetic *)
val [prem1,prem2,prem3,prem4] = Goal
"[| n le k; k le m; \
@@ -1734,13 +1729,12 @@
by (rtac (prem1 RS le_exists) 1);
by (simp_tac (simpset() addsimps [prem2 RS lt_nat_in_nat, prem4]) 2);
by (rtac ([prem1,prem2] MRS le_trans RS le_exists) 1);
+by (rtac prem4 2);
by (rtac prem3 1);
by (assume_tac 2);
by (assume_tac 2);
by (cut_facts_tac [prem1,prem2] 1);
-by (Asm_full_simp_tac 1);
-by (etac add_le_elim1 1);
-by (REPEAT (ares_tac prems 1));
+by Auto_tac;
qed "le_exists_lemma";
Goal (* eps_split_left_le *)
--- a/src/ZF/ex/Mutil.ML Mon Aug 07 10:29:04 2000 +0200
+++ b/src/ZF/ex/Mutil.ML Mon Aug 07 10:29:54 2000 +0200
@@ -117,22 +117,22 @@
addEs [mem_irrefl]) 1);
qed "dominoes_tile_matrix";
+Goal "[| x=y; x<y |] ==> P";
+by Auto_tac;
+qed "eq_lt_E";
-Goal "[| m: nat; n: nat; \
-\ t = (succ(m)#+succ(m))*(succ(n)#+succ(n)); \
-\ t' = t - {<0,0>} - {<succ(m#+m), succ(n#+n)>} |] ==> \
-\ t' ~: tiling(domino)";
+Goal "[| m: nat; n: nat; \
+\ t = (succ(m)#+succ(m))*(succ(n)#+succ(n)); \
+\ t' = t - {<0,0>} - {<succ(m#+m), succ(n#+n)>} |] \
+\ ==> t' ~: tiling(domino)";
by (rtac notI 1);
by (dtac tiling_domino_0_1 1);
-by (subgoal_tac "|evnodd(t',0)| < |evnodd(t',1)|" 1);
-by (asm_full_simp_tac (simpset() addsimps [lt_not_refl]) 1);
+by (eres_inst_tac [("x", "|?A|")] eq_lt_E 1);
by (subgoal_tac "t : tiling(domino)" 1);
(*Requires a small simpset that won't move the succ applications*)
by (asm_simp_tac (ZF_ss addsimps [nat_succI, add_type,
dominoes_tile_matrix]) 2);
-by (subgoal_tac "(m#+m)#+(n#+n) = (m#+n)#+(m#+n)" 1);
-by (asm_simp_tac (simpset() addsimps add_ac) 2);
-by (asm_lr_simp_tac
+by (asm_full_simp_tac
(simpset() addsimps [evnodd_Diff, mod2_add_self,
mod2_succ_succ, tiling_domino_0_1 RS sym]) 1);
by (rtac lt_trans 1);
--- a/src/ZF/ex/Primes.thy Mon Aug 07 10:29:04 2000 +0200
+++ b/src/ZF/ex/Primes.thy Mon Aug 07 10:29:54 2000 +0200
@@ -6,7 +6,7 @@
The "divides" relation, the greatest common divisor and Euclid's algorithm
*)
-Primes = Arith +
+Primes = Main +
consts
dvd :: [i,i]=>o (infixl 70)
gcd :: [i,i,i]=>o (* great common divisor *)