diff -r ab88297f1a56 -r 32a83e3ad5a4 arith.ML --- 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 (m-n)+n = m::nat"; +val [prem] = goal Arith.thy "[| ~ m 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));