--- a/Arith.ML Tue Mar 22 19:55:29 1994 +0100
+++ b/Arith.ML Sun Mar 27 12:36:39 1994 +0200
@@ -51,18 +51,18 @@
val arith_ss = arith_ss addsimps [add_0_right,add_Suc_right];
(*Associative law for addition*)
-val add_assoc = prove_goal Arith.thy "m + (n + k) = (m + n) + k::nat"
+val add_assoc = prove_goal Arith.thy "(m + n) + k = m + (n + k)::nat"
(fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
(*Commutative law for addition*)
val add_commute = prove_goal Arith.thy "m + n = n + m::nat"
(fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
-val add_right_commute = prove_goal Arith.thy "(x+y)+z=(x+z)+y::nat"
+val add_left_commute = prove_goal Arith.thy "x+(y+z)=y+(x+z)::nat"
(fn _ => [rtac trans 1, rtac add_commute 1, rtac trans 1,
rtac add_assoc 1, rtac (add_commute RS arg_cong) 1]);
-val add_ac = [add_assoc, add_commute, add_right_commute];
+val add_ac = [add_assoc, add_commute, add_left_commute];
(*** Multiplication ***)
@@ -87,17 +87,26 @@
(fn _ => [nat_ind_tac "m" 1,
ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);
-val arith_ss = arith_ss addsimps [add_mult_distrib];
+(*addition distributes over multiplication*)
+val add_mult_distrib = prove_goal Arith.thy "(m + n)*k = (m*k) + (n*k)::nat"
+ (fn _ => [nat_ind_tac "m" 1,
+ ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);
+
+val add_mult_distrib2 = prove_goal Arith.thy "k*(m + n) = (k*m) + (k*n)::nat"
+ (fn _ => [nat_ind_tac "m" 1,
+ ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);
+
+val arith_ss = arith_ss addsimps [add_mult_distrib,add_mult_distrib2];
(*Associative law for multiplication*)
-val mult_assoc = prove_goal Arith.thy "m * (n * k) = (m * n) * k::nat"
+val mult_assoc = prove_goal Arith.thy "(m * n) * k = m * (n * k)::nat"
(fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
-val mult_right_commute = prove_goal Arith.thy "(x*y)*z=(x*z)*y::nat"
+val mult_left_commute = prove_goal Arith.thy "x*(y*z) = y*(x*z)::nat"
(fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1,
rtac mult_assoc 1, rtac (mult_commute RS arg_cong) 1]);
-val mult_ac = [mult_assoc,mult_commute,mult_right_commute];
+val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
(*** Difference ***)
@@ -105,7 +114,7 @@
(fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
-val [prem] = goal Arith.thy "[| ~ m<n |] ==> (m-n)+n = m::nat";
+val [prem] = goal Arith.thy "[| ~ m<n |] ==> n+(m-n) = m::nat";
by (rtac (prem RS rev_mp) 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
by (ALLGOALS(asm_simp_tac arith_ss));
--- a/arith.ML Tue Mar 22 19:55:29 1994 +0100
+++ b/arith.ML Sun Mar 27 12:36:39 1994 +0200
@@ -51,18 +51,18 @@
val arith_ss = arith_ss addsimps [add_0_right,add_Suc_right];
(*Associative law for addition*)
-val add_assoc = prove_goal Arith.thy "m + (n + k) = (m + n) + k::nat"
+val add_assoc = prove_goal Arith.thy "(m + n) + k = m + (n + k)::nat"
(fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
(*Commutative law for addition*)
val add_commute = prove_goal Arith.thy "m + n = n + m::nat"
(fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
-val add_right_commute = prove_goal Arith.thy "(x+y)+z=(x+z)+y::nat"
+val add_left_commute = prove_goal Arith.thy "x+(y+z)=y+(x+z)::nat"
(fn _ => [rtac trans 1, rtac add_commute 1, rtac trans 1,
rtac add_assoc 1, rtac (add_commute RS arg_cong) 1]);
-val add_ac = [add_assoc, add_commute, add_right_commute];
+val add_ac = [add_assoc, add_commute, add_left_commute];
(*** Multiplication ***)
@@ -87,17 +87,26 @@
(fn _ => [nat_ind_tac "m" 1,
ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);
-val arith_ss = arith_ss addsimps [add_mult_distrib];
+(*addition distributes over multiplication*)
+val add_mult_distrib = prove_goal Arith.thy "(m + n)*k = (m*k) + (n*k)::nat"
+ (fn _ => [nat_ind_tac "m" 1,
+ ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);
+
+val add_mult_distrib2 = prove_goal Arith.thy "k*(m + n) = (k*m) + (k*n)::nat"
+ (fn _ => [nat_ind_tac "m" 1,
+ ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]);
+
+val arith_ss = arith_ss addsimps [add_mult_distrib,add_mult_distrib2];
(*Associative law for multiplication*)
-val mult_assoc = prove_goal Arith.thy "m * (n * k) = (m * n) * k::nat"
+val mult_assoc = prove_goal Arith.thy "(m * n) * k = m * (n * k)::nat"
(fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
-val mult_right_commute = prove_goal Arith.thy "(x*y)*z=(x*z)*y::nat"
+val mult_left_commute = prove_goal Arith.thy "x*(y*z) = y*(x*z)::nat"
(fn _ => [rtac trans 1, rtac mult_commute 1, rtac trans 1,
rtac mult_assoc 1, rtac (mult_commute RS arg_cong) 1]);
-val mult_ac = [mult_assoc,mult_commute,mult_right_commute];
+val mult_ac = [mult_assoc,mult_commute,mult_left_commute];
(*** Difference ***)
@@ -105,7 +114,7 @@
(fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]);
(*Addition is the inverse of subtraction: if n<=m then n+(m-n) = m. *)
-val [prem] = goal Arith.thy "[| ~ m<n |] ==> (m-n)+n = m::nat";
+val [prem] = goal Arith.thy "[| ~ m<n |] ==> n+(m-n) = m::nat";
by (rtac (prem RS rev_mp) 1);
by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
by (ALLGOALS(asm_simp_tac arith_ss));
--- a/ex/Qsort.ML Tue Mar 22 19:55:29 1994 +0100
+++ b/ex/Qsort.ML Sun Mar 27 12:36:39 1994 +0200
@@ -6,8 +6,7 @@
Two verifications of Quicksort
*)
-val ss = sorting_ss addsimps [Qsort.qsort_Nil,Qsort.qsort_Cons]
- delsimps [conj_assoc] addsimps conj_ac;
+val ss = sorting_ss addsimps ([Qsort.qsort_Nil,Qsort.qsort_Cons]@conj_comms);
goal Qsort.thy "!x. mset(qsort(le,xs),x) = mset(xs,x)";
by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
--- a/ex/qsort.ML Tue Mar 22 19:55:29 1994 +0100
+++ b/ex/qsort.ML Sun Mar 27 12:36:39 1994 +0200
@@ -6,8 +6,7 @@
Two verifications of Quicksort
*)
-val ss = sorting_ss addsimps [Qsort.qsort_Nil,Qsort.qsort_Cons]
- delsimps [conj_assoc] addsimps conj_ac;
+val ss = sorting_ss addsimps ([Qsort.qsort_Nil,Qsort.qsort_Cons]@conj_comms);
goal Qsort.thy "!x. mset(qsort(le,xs),x) = mset(xs,x)";
by(res_inst_tac[("xs","xs"),("p","le")]Qsort.qsort_ind 1);
--- a/simpdata.ML Tue Mar 22 19:55:29 1994 +0100
+++ b/simpdata.ML Sun Mar 27 12:36:39 1994 +0200
@@ -70,8 +70,8 @@
val conj_assoc = prover "((P&Q)&R) = (P&(Q&R))";
val conj_commute = prover "(P&Q) = (Q&P)";
-val conj_right_commute = prover "((P&Q)&R) = ((P&R)&Q)";
-val conj_ac = [conj_assoc RS sym, conj_commute, conj_right_commute];
+val conj_left_commute = prover "(P&(Q&R)) = (Q&(P&R))";
+val conj_comms = [conj_commute, conj_left_commute];
val if_True = prove_goal HOL.thy "if(True,x,y) = x"
(fn _=>[stac if_def 1, fast_tac (HOL_cs addIs [select_equality]) 1]);