diff -r 5e0570ea8b70 -r 5ea12dfd9393 arith.ML --- a/arith.ML Fri Mar 18 20:33:32 1994 +0100 +++ b/arith.ML Tue Mar 22 08:25:30 1994 +0100 @@ -51,14 +51,20 @@ 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. Must simplify after first induction! - Orientation of rewrites is delicate*) +(*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" + (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]; + + (*** Multiplication ***) (*right annihilation in product*) @@ -66,13 +72,9 @@ (fn _ => [nat_ind_tac "m" 1, ALLGOALS(asm_simp_tac arith_ss)]); (*right Sucessor law for multiplication*) -val mult_Suc_right = prove_goal Arith.thy - "m * Suc(n) = m + (m * n)" - (fn _ => - [nat_ind_tac "m" 1, - ALLGOALS(asm_simp_tac(arith_ss addsimps [add_assoc RS sym])), - (*The final goal requires the commutative law for addition*) - stac add_commute 1, rtac refl 1]); +val mult_Suc_right = prove_goal Arith.thy "m * Suc(n) = m + (m * n)" + (fn _ => [nat_ind_tac "m" 1, + ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]); val arith_ss = arith_ss addsimps [mult_0_right,mult_Suc_right]; @@ -83,13 +85,19 @@ (*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_assoc]))]); + ALLGOALS(asm_simp_tac (arith_ss addsimps add_ac))]); + +val arith_ss = arith_ss addsimps [add_mult_distrib]; (*Associative law for multiplication*) -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 addsimps [add_mult_distrib]))]); +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" + (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]; (*** Difference ***) @@ -97,7 +105,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) = m::nat"; +val [prem] = goal Arith.thy "[| ~ m (m-n)+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)); @@ -153,10 +161,10 @@ goal Arith.thy "!!m. 0 (m div n)*n + m mod n = m"; by (res_inst_tac [("n","m")] less_induct 1); by (rename_tac "k" 1); (*Variable name used in line below*) -by (res_inst_tac [("Q","k m<=n::nat"; by(nat_ind_tac "k" 1); -by(ALLGOALS(simp_tac arith_ss)); +by(ALLGOALS(asm_full_simp_tac arith_ss)); by(fast_tac (HOL_cs addDs [Suc_leD]) 1); val plus_leD1 = result() RS mp;