# HG changeset patch # User paulson # Date 905864789 -7200 # Node ID 22f8331cdf47e6de9ef748e0dca0711211a8cd7c # Parent 85855f65d0c6229b92fea2873e3cb04c4cb22bbd revised treatment of integers diff -r 85855f65d0c6 -r 22f8331cdf47 src/HOL/Integ/Bin.ML --- a/src/HOL/Integ/Bin.ML Tue Sep 15 15:04:07 1998 +0200 +++ b/src/HOL/Integ/Bin.ML Tue Sep 15 15:06:29 1998 +0200 @@ -7,8 +7,6 @@ Arithmetic on binary integers. *) -open Bin; - (** extra rules for bin_succ, bin_pred, bin_add, bin_mult **) qed_goal "norm_Bcons_Plus_0" Bin.thy @@ -55,6 +53,7 @@ "bin_minus(Bcons w False) = Bcons (bin_minus w) False" (fn _ => [(Simp_tac 1)]); + (*** bin_add: binary addition ***) qed_goal "bin_add_Bcons_Bcons11" Bin.thy @@ -66,12 +65,9 @@ "bin_add (Bcons v True) (Bcons w False) = norm_Bcons (bin_add v w) True" (fn _ => [(Simp_tac 1)]); -val lemma = prove_goal HOL.thy "(False = (~P)) = P" - (fn _ => [(Fast_tac 1)]); - qed_goal "bin_add_Bcons_Bcons0" Bin.thy "bin_add (Bcons v False) (Bcons w y) = norm_Bcons (bin_add v w) y" - (fn _ => [(simp_tac (simpset() addsimps [lemma]) 1)]); + (fn _ => [Auto_tac]); qed_goal "bin_add_Bcons_Plus" Bin.thy "bin_add (Bcons v x) PlusSign = Bcons v x" @@ -101,79 +97,215 @@ (**** The carry/borrow functions, bin_succ and bin_pred ****) -(**** integ_of_bin ****) - +(**** integ_of ****) -qed_goal "integ_of_bin_norm_Bcons" Bin.thy - "integ_of_bin(norm_Bcons w b) = integ_of_bin(Bcons w b)" +qed_goal "integ_of_norm_Bcons" Bin.thy + "integ_of(norm_Bcons w b) = integ_of(Bcons w b)" (fn _ =>[(induct_tac "w" 1), - (ALLGOALS Simp_tac) ]); + (ALLGOALS (asm_simp_tac + (simpset() addsimps [zadd_zminus_inverse_nat]))) ]); -qed_goal "integ_of_bin_succ" Bin.thy - "integ_of_bin(bin_succ w) = $#1 + integ_of_bin w" - (fn _ =>[(rtac bin.induct 1), - (ALLGOALS(asm_simp_tac - (simpset() addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]); +val integ_of_norm_Cons_simps = + [zadd_zminus_inverse_nat, integ_of_norm_Bcons] @ zadd_ac; -qed_goal "integ_of_bin_pred" Bin.thy - "integ_of_bin(bin_pred w) = $~ ($#1) + integ_of_bin w" +qed_goal "integ_of_succ" Bin.thy + "integ_of(bin_succ w) = $#1 + integ_of w" (fn _ =>[(rtac bin.induct 1), - (ALLGOALS(asm_simp_tac - (simpset() addsimps (integ_of_bin_norm_Bcons::zadd_ac)))) ]); + (ALLGOALS(asm_simp_tac (simpset() addsimps integ_of_norm_Cons_simps))) ]); + +qed_goal "integ_of_pred" Bin.thy + "integ_of(bin_pred w) = - ($#1) + integ_of w" + (fn _ =>[(rtac bin.induct 1), + (ALLGOALS(asm_simp_tac (simpset() addsimps integ_of_norm_Cons_simps))) ]); -qed_goal "integ_of_bin_minus" Bin.thy - "integ_of_bin(bin_minus w) = $~ (integ_of_bin w)" - (fn _ =>[(rtac bin.induct 1), - (Simp_tac 1), - (Simp_tac 1), - (asm_simp_tac (simpset() - delsimps [pred_Plus,pred_Minus,pred_Bcons] - addsimps [integ_of_bin_succ,integ_of_bin_pred, - zadd_assoc]) 1)]); +Goal "integ_of(bin_minus w) = - (integ_of w)"; +by (rtac bin.induct 1); +by (Simp_tac 1); +by (Simp_tac 1); +by (asm_simp_tac (simpset() + delsimps [pred_Plus,pred_Minus,pred_Bcons] + addsimps [integ_of_succ,integ_of_pred, + zadd_assoc]) 1); +qed "integ_of_minus"; -val bin_add_simps = [add_Plus,add_Minus,bin_add_Bcons_Plus, +val bin_add_simps = [zadd_zminus_inverse_nat, zadd_zminus_inverse_nat2, + bin_add_Bcons_Plus, bin_add_Bcons_Minus,bin_add_Bcons_Bcons, - integ_of_bin_succ, integ_of_bin_pred, - integ_of_bin_norm_Bcons]; -val bin_simps = [iob_Plus,iob_Minus,iob_Bcons]; + integ_of_succ, integ_of_pred, + integ_of_norm_Bcons]; -Goal "! w. integ_of_bin(bin_add v w) = integ_of_bin v + integ_of_bin w"; +Goal "! w. integ_of(bin_add v w) = integ_of v + integ_of w"; by (induct_tac "v" 1); by (simp_tac (simpset() addsimps bin_add_simps) 1); by (simp_tac (simpset() addsimps bin_add_simps) 1); by (rtac allI 1); by (induct_tac "w" 1); -by (asm_simp_tac (simpset() addsimps (bin_add_simps)) 1); -by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1); -by (cut_inst_tac [("P","bool")] True_or_False 1); -by (etac disjE 1); -by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1); -by (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)) 1); -qed_spec_mp "integ_of_bin_add"; +by (ALLGOALS (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac)))); +qed_spec_mp "integ_of_add"; -val bin_mult_simps = [integ_of_bin_minus, integ_of_bin_add, - integ_of_bin_norm_Bcons]; +val bin_mult_simps = [zmult_zminus, + integ_of_minus, integ_of_add, + integ_of_norm_Bcons]; -Goal "integ_of_bin(bin_mult v w) = integ_of_bin v * integ_of_bin w"; + +Goal "integ_of(bin_mult v w) = integ_of v * integ_of w"; by (induct_tac "v" 1); by (simp_tac (simpset() addsimps bin_mult_simps) 1); by (simp_tac (simpset() addsimps bin_mult_simps) 1); -by (cut_inst_tac [("P","bool")] True_or_False 1); -by (etac disjE 1); -by (asm_simp_tac (simpset() addsimps (bin_mult_simps @ [zadd_zmult_distrib])) 2); -by (asm_simp_tac (simpset() addsimps (bin_mult_simps @ [zadd_zmult_distrib] @ +by (asm_simp_tac + (simpset() addsimps (bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac)) 1); -qed "integ_of_bin_mult"; +qed "integ_of_mult"; + +(* #0 = $# 0 *) +bind_thm ("int_eq_nat0", integ_of_Plus); + +Goal "$# 1 = #1"; +by (Simp_tac 1); +qed "int_eq_nat1"; + +Goal "$# 2 = #2"; +by (simp_tac (simpset() addsimps [add_znat]) 1); +qed "int_eq_nat2"; -Delsimps [succ_Bcons,pred_Bcons,min_Bcons,add_Bcons,mult_Bcons, - iob_Plus,iob_Minus,iob_Bcons, - norm_Plus,norm_Minus,norm_Bcons]; +(** Simplification rules with integer constants **) + +Goal "#0 + z = z"; +by (Simp_tac 1); +qed "zadd_0"; + +Goal "z + #0 = z"; +by (Simp_tac 1); +qed "zadd_0_right"; + +Goal "z + (- z) = #0"; +by (simp_tac (simpset() addsimps [zadd_zminus_inverse_nat]) 1); +qed "zadd_zminus_inverse"; + +Goal "(- z) + z = #0"; +by (simp_tac (simpset() addsimps [zadd_zminus_inverse_nat2]) 1); +qed "zadd_zminus_inverse2"; + +Addsimps [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2]; + +Goal "- (#0) = #0"; +by (Simp_tac 1); +qed "zminus_0"; + +Addsimps [zminus_0]; + +Goal "#0 * z = #0"; +by (Simp_tac 1); +qed "zmult_0"; + +Goal "#1 * z = z"; +by (Simp_tac 1); +qed "zmult_1"; + +Goal "#2 * z = z+z"; +by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1); +qed "zmult_2"; + +Goal "z * #0 = #0"; +by (Simp_tac 1); +qed "zmult_0_right"; + +Goal "z * #1 = z"; +by (Simp_tac 1); +qed "zmult_1_right"; + +Goal "z * #2 = z+z"; +by (simp_tac (simpset() addsimps [zadd_zmult_distrib2]) 1); +qed "zmult_2_right"; + +Addsimps [zmult_0, zmult_0_right, + zmult_1, zmult_1_right, + zmult_2, zmult_2_right]; + +Goal "(w < z + #1) = (wint + integ_of :: bin=>int norm_Bcons :: [bin,bool]=>bin bin_succ :: bin=>bin bin_pred :: bin=>bin @@ -49,9 +49,10 @@ norm_Bcons "norm_Bcons (Bcons w' x') b = Bcons (Bcons w' x') b" primrec - iob_Plus "integ_of_bin PlusSign = $#0" - iob_Minus "integ_of_bin MinusSign = $~($#1)" - iob_Bcons "integ_of_bin(Bcons w x) = (if x then $#1 else $#0) + (integ_of_bin w) + (integ_of_bin w)" + integ_of_Plus "integ_of PlusSign = $# 0" + integ_of_Minus "integ_of MinusSign = - ($# 1)" + integ_of_Bcons "integ_of(Bcons w x) = (if x then $# 1 else $# 0) + + (integ_of w) + (integ_of w)" primrec succ_Plus "bin_succ PlusSign = Bcons PlusSign True" @@ -81,8 +82,15 @@ primrec h_Plus "h_bin v x PlusSign = Bcons v x" h_Minus "h_bin v x MinusSign = bin_pred (Bcons v x)" - h_BCons "h_bin v x (Bcons w y) = norm_Bcons (bin_add v (if (x & y) then bin_succ w else w)) (x~=y)" + h_BCons "h_bin v x (Bcons w y) = norm_Bcons + (bin_add v (if (x & y) then bin_succ w else w)) (x~=y)" + +(*For implementing the equality test on integer constants*) +constdefs + iszero :: int => bool + "iszero z == z = $# 0" + end ML @@ -154,7 +162,7 @@ (* translation of integer constant tokens to and from binary *) fun int_tr (*"_Int"*) [t as Free (str, _)] = - (const "integ_of_bin" $ + (const "integ_of" $ (mk_bin str handle ERROR => raise TERM ("int_tr", [t]))) | int_tr (*"_Int"*) ts = raise TERM ("int_tr", ts); @@ -162,5 +170,5 @@ | int_tr' (*"integ_of"*) _ = raise Match; in val parse_translation = [("_Int", int_tr)]; - val print_translation = [("integ_of_bin", int_tr')]; + val print_translation = [("integ_of", int_tr')]; end; diff -r 85855f65d0c6 -r 22f8331cdf47 src/HOL/Integ/Integ.ML --- a/src/HOL/Integ/Integ.ML Tue Sep 15 15:04:07 1998 +0200 +++ b/src/HOL/Integ/Integ.ML Tue Sep 15 15:06:29 1998 +0200 @@ -6,16 +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 < *) -open Integ; - -Delrules [equalityI]; - (*** Proving that intrel is an equivalence relation ***) @@ -121,7 +115,7 @@ val zminus_ize = RSLIST [equiv_intrel, zminus_congruent]; Goalw [zminus_def] - "$~ Abs_Integ(intrel^^{(x,y)}) = Abs_Integ(intrel ^^ {(y,x)})"; + "- Abs_Integ(intrel^^{(x,y)}) = Abs_Integ(intrel ^^ {(y,x)})"; by (res_inst_tac [("f","Abs_Integ")] arg_cong 1); by (simp_tac (simpset() addsimps [intrel_in_integ RS Abs_Integ_inverse,zminus_ize UN_equiv_class]) 1); @@ -137,20 +131,23 @@ by (asm_full_simp_tac (simpset() addsimps [Rep_Integ_inverse]) 1); qed "eq_Abs_Integ"; -Goal "$~ ($~ z) = z"; +Goal "- (- z) = (z::int)"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (asm_simp_tac (simpset() addsimps [zminus]) 1); qed "zminus_zminus"; +Addsimps [zminus_zminus]; -Goal "inj(zminus)"; +Goal "inj(uminus::int=>int)"; by (rtac injI 1); -by (dres_inst_tac [("f","zminus")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps [zminus_zminus]) 1); +by (dres_inst_tac [("f","uminus")] arg_cong 1); +by (Asm_full_simp_tac 1); qed "inj_zminus"; -Goalw [znat_def] "$~ ($#0) = $#0"; +Goalw [znat_def] "- ($# 0) = $# 0"; by (simp_tac (simpset() addsimps [zminus]) 1); -qed "zminus_0"; +qed "zminus_nat0"; + +Addsimps [zminus_nat0]; (**** znegative: the test for negative integers ****) @@ -161,23 +158,15 @@ by Safe_tac; qed "not_znegative_znat"; -Goalw [znegative_def, znat_def] "znegative($~ $# Suc(n))"; +Goalw [znegative_def, znat_def] "znegative(- $# Suc(n))"; by (simp_tac (simpset() addsimps [zminus]) 1); qed "znegative_zminus_znat"; +Addsimps [znegative_zminus_znat, not_znegative_znat]; + (**** zmagnitude: magnitide of an integer, as a natural number ****) -goal Arith.thy "!!n::nat. n - Suc(n+m)=0"; -by (induct_tac "n" 1); -by (ALLGOALS Asm_simp_tac); -qed "diff_Suc_add_0"; - -goal Arith.thy "Suc((n::nat)+m)-n=Suc(m)"; -by (induct_tac "n" 1); -by (ALLGOALS Asm_simp_tac); -qed "diff_Suc_add_inverse"; - Goalw [congruent_def] "congruent intrel (split (%x y. intrel^^{((y-x) + (x-(y::nat)),0)}))"; by Safe_tac; @@ -208,10 +197,12 @@ by (asm_simp_tac (simpset() addsimps [zmagnitude]) 1); qed "zmagnitude_znat"; -Goalw [znat_def] "zmagnitude($~ $# n) = $#n"; +Goalw [znat_def] "zmagnitude(- $# n) = $#n"; by (asm_simp_tac (simpset() addsimps [zmagnitude, zminus]) 1); qed "zmagnitude_zminus_znat"; +Addsimps [zmagnitude_znat, zmagnitude_zminus_znat]; + (**** zadd: addition on Integ ****) @@ -238,16 +229,12 @@ (simpset() addsimps [zadd_ize UN_equiv_class2]) 1); qed "zadd"; -Goalw [znat_def] "$#0 + z = z"; -by (res_inst_tac [("z","z")] eq_Abs_Integ 1); -by (asm_simp_tac (simpset() addsimps [zadd]) 1); -qed "zadd_0"; - -Goal "$~ (z + w) = $~ z + $~ w"; +Goal "- (z + w) = - z + - (w::int)"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (res_inst_tac [("z","w")] eq_Abs_Integ 1); by (asm_simp_tac (simpset() addsimps [zminus,zadd]) 1); qed "zminus_zadd_distrib"; +Addsimps [zminus_zadd_distrib]; Goal "(z::int) + w = w + z"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); @@ -272,24 +259,36 @@ (*Integer addition is an AC operator*) val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute]; -Goalw [znat_def] "$# (m + n) = ($#m) + ($#n)"; +Goalw [znat_def] "($#m) + ($#n) = $# (m + n)"; +by (simp_tac (simpset() addsimps [zadd]) 1); +qed "add_znat"; + +Goal "$# (Suc m) = $# 1 + ($# m)"; +by (simp_tac (simpset() addsimps [add_znat]) 1); +qed "znat_Suc"; + +Goalw [znat_def] "$# 0 + z = z"; +by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (asm_simp_tac (simpset() addsimps [zadd]) 1); -qed "znat_add"; +qed "zadd_nat0"; -Goalw [znat_def] "z + ($~ z) = $#0"; +Goal "z + $# 0 = z"; +by (rtac (zadd_commute RS trans) 1); +by (rtac zadd_nat0 1); +qed "zadd_nat0_right"; + +Goalw [znat_def] "z + (- z) = $# 0"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (asm_simp_tac (simpset() addsimps [zminus, zadd, add_commute]) 1); -qed "zadd_zminus_inverse"; +qed "zadd_zminus_inverse_nat"; -Goal "($~ z) + z = $#0"; +Goal "(- z) + z = $# 0"; by (rtac (zadd_commute RS trans) 1); -by (rtac zadd_zminus_inverse 1); -qed "zadd_zminus_inverse2"; +by (rtac zadd_zminus_inverse_nat 1); +qed "zadd_zminus_inverse_nat2"; -Goal "z + $#0 = z"; -by (rtac (zadd_commute RS trans) 1); -by (rtac zadd_0 1); -qed "zadd_0_right"; +Addsimps [zadd_nat0, zadd_nat0_right, + zadd_zminus_inverse_nat, zadd_zminus_inverse_nat2]; (** Lemmas **) @@ -316,11 +315,11 @@ \ 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 (pair_tac "w" 2); - by (rename_tac "z1 z2" 2); - by Safe_tac; - by (rewtac split_def); - by (simp_tac (simpset() addsimps add_ac@mult_ac) 1); +by (pair_tac "w" 2); +by (rename_tac "z1 z2" 2); +by Safe_tac; +by (rewtac split_def); +by (simp_tac (simpset() addsimps add_ac@mult_ac) 1); by (asm_simp_tac (simpset() delsimps [equiv_intrel_iff] addsimps add_ac@mult_ac) 1); by (rtac (intrelI RS(equiv_intrel RS equiv_class_eq)) 1); @@ -341,24 +340,14 @@ by (simp_tac (simpset() addsimps [zmult_ize UN_equiv_class2]) 1); qed "zmult"; -Goalw [znat_def] "$#0 * z = $#0"; -by (res_inst_tac [("z","z")] eq_Abs_Integ 1); -by (asm_simp_tac (simpset() addsimps [zmult]) 1); -qed "zmult_0"; - -Goalw [znat_def] "$#Suc(0) * z = z"; -by (res_inst_tac [("z","z")] eq_Abs_Integ 1); -by (asm_simp_tac (simpset() addsimps [zmult]) 1); -qed "zmult_1"; - -Goal "($~ z) * w = $~ (z * w)"; +Goal "(- z) * w = - (z * (w::int))"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (res_inst_tac [("z","w")] eq_Abs_Integ 1); by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1); qed "zmult_zminus"; -Goal "($~ z) * ($~ w) = (z * w)"; +Goal "(- z) * (- w) = (z * (w::int))"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (res_inst_tac [("z","w")] eq_Abs_Integ 1); by (asm_simp_tac (simpset() addsimps ([zminus, zmult] @ add_ac)) 1); @@ -370,14 +359,6 @@ by (asm_simp_tac (simpset() addsimps ([zmult] @ add_ac @ mult_ac)) 1); qed "zmult_commute"; -Goal "z * $# 0 = $#0"; -by (rtac ([zmult_commute, zmult_0] MRS trans) 1); -qed "zmult_0_right"; - -Goal "z * $#Suc(0) = z"; -by (rtac ([zmult_commute, zmult_1] MRS trans) 1); -qed "zmult_1_right"; - Goal "((z1::int) * z2) * z3 = z1 * (z2 * z3)"; by (res_inst_tac [("z","z1")] eq_Abs_Integ 1); by (res_inst_tac [("z","z2")] eq_Abs_Integ 1); @@ -406,7 +387,7 @@ val zmult_commute'= read_instantiate [("z","w")] zmult_commute; -Goal "w * ($~ z) = $~ (w * z)"; +Goal "w * (- z) = - (w * (z::int))"; by (simp_tac (simpset() addsimps [zmult_commute', zmult_zminus]) 1); qed "zmult_zminus_right"; @@ -414,167 +395,56 @@ by (simp_tac (simpset() addsimps [zmult_commute',zadd_zmult_distrib]) 1); qed "zadd_zmult_distrib2"; -val zadd_simps = - [zadd_0, zadd_0_right, zadd_zminus_inverse, zadd_zminus_inverse2]; +Goalw [znat_def] "$# 0 * z = $# 0"; +by (res_inst_tac [("z","z")] eq_Abs_Integ 1); +by (asm_simp_tac (simpset() addsimps [zmult]) 1); +qed "zmult_nat0"; -val zminus_simps = [zminus_zminus, zminus_0, zminus_zadd_distrib]; +Goalw [znat_def] "$# 1 * z = z"; +by (res_inst_tac [("z","z")] eq_Abs_Integ 1); +by (asm_simp_tac (simpset() addsimps [zmult]) 1); +qed "zmult_nat1"; -val zmult_simps = [zmult_0, zmult_1, zmult_0_right, zmult_1_right, - zmult_zminus, zmult_zminus_right]; +Goal "z * $# 0 = $# 0"; +by (rtac ([zmult_commute, zmult_nat0] MRS trans) 1); +qed "zmult_nat0_right"; -Addsimps (zadd_simps @ zminus_simps @ zmult_simps @ - [zmagnitude_znat, zmagnitude_zminus_znat]); +Goal "z * $# 1 = z"; +by (rtac ([zmult_commute, zmult_nat1] MRS trans) 1); +qed "zmult_nat1_right"; + +Addsimps [zmult_nat0, zmult_nat0_right, zmult_nat1, zmult_nat1_right]; -(**** Additional Theorems (by Mattolini; proofs mainly by lcp) ****) - -(* Some Theorems about zsuc and zpred *) -Goalw [zsuc_def] "$#(Suc(n)) = zsuc($# n)"; -by (simp_tac (simpset() addsimps [znat_add RS sym]) 1); -qed "znat_Suc"; - -Goalw [zpred_def,zsuc_def,zdiff_def] "$~ zsuc(z) = zpred($~ z)"; -by (Simp_tac 1); -qed "zminus_zsuc"; - -Goalw [zpred_def,zsuc_def,zdiff_def] "$~ zpred(z) = zsuc($~ z)"; -by (Simp_tac 1); -qed "zminus_zpred"; - -Goalw [zsuc_def,zpred_def,zdiff_def] "zpred(zsuc(z)) = z"; -by (simp_tac (simpset() addsimps [zadd_assoc]) 1); -qed "zpred_zsuc"; - -Goalw [zsuc_def,zpred_def,zdiff_def] "zsuc(zpred(z)) = z"; -by (simp_tac (simpset() addsimps [zadd_assoc]) 1); -qed "zsuc_zpred"; - -Goal "(zpred(z)=w) = (z=zsuc(w))"; -by Safe_tac; -by (rtac (zsuc_zpred RS sym) 1); -by (rtac zpred_zsuc 1); -qed "zpred_to_zsuc"; - -Goal "(zsuc(z)=w)=(z=zpred(w))"; -by Safe_tac; -by (rtac (zpred_zsuc RS sym) 1); -by (rtac zsuc_zpred 1); -qed "zsuc_to_zpred"; - -Goal "($~ z = w) = (z = $~ w)"; +Goal "(- z = w) = (z = - (w::int))"; by Safe_tac; by (rtac (zminus_zminus RS sym) 1); by (rtac zminus_zminus 1); qed "zminus_exchange"; -Goal "(zsuc(z)=zsuc(w)) = (z=w)"; -by Safe_tac; -by (dres_inst_tac [("f","zpred")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps [zpred_zsuc]) 1); -qed "bijective_zsuc"; - -Goal "(zpred(z)=zpred(w)) = (z=w)"; -by Safe_tac; -by (dres_inst_tac [("f","zsuc")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps [zsuc_zpred]) 1); -qed "bijective_zpred"; - -(* Additional Theorems about zadd *) - -Goalw [zsuc_def] "zsuc(z) + w = zsuc(z+w)"; -by (simp_tac (simpset() addsimps zadd_ac) 1); -qed "zadd_zsuc"; - -Goalw [zsuc_def] "w + zsuc(z) = zsuc(w+z)"; -by (simp_tac (simpset() addsimps zadd_ac) 1); -qed "zadd_zsuc_right"; - -Goalw [zpred_def,zdiff_def] "zpred(z) + w = zpred(z+w)"; -by (simp_tac (simpset() addsimps zadd_ac) 1); -qed "zadd_zpred"; - -Goalw [zpred_def,zdiff_def] "w + zpred(z) = zpred(w+z)"; -by (simp_tac (simpset() addsimps zadd_ac) 1); -qed "zadd_zpred_right"; - - -(* Additional Theorems about zmult *) - -Goalw [zsuc_def] "zsuc(w) * z = z + w * z"; -by (simp_tac (simpset() addsimps [zadd_zmult_distrib, zadd_commute]) 1); -qed "zmult_zsuc"; - -Goalw [zsuc_def] "z * zsuc(w) = z + w * z"; -by (simp_tac - (simpset() addsimps [zadd_zmult_distrib2, zadd_commute, zmult_commute]) 1); -qed "zmult_zsuc_right"; - -Goalw [zpred_def, zdiff_def] "zpred(w) * z = w * z - z"; -by (simp_tac (simpset() addsimps [zadd_zmult_distrib]) 1); -qed "zmult_zpred"; - -Goalw [zpred_def, zdiff_def] "z * zpred(w) = w * z - z"; -by (simp_tac (simpset() addsimps [zadd_zmult_distrib2, zmult_commute]) 1); -qed "zmult_zpred_right"; - -(* Further Theorems about zsuc and zpred *) -Goal "$#Suc(m) ~= $#0"; -by (simp_tac (simpset() addsimps [inj_znat RS inj_eq]) 1); -qed "znat_Suc_not_znat_Zero"; - -bind_thm ("znat_Zero_not_znat_Suc", (znat_Suc_not_znat_Zero RS not_sym)); - - -Goalw [zsuc_def,znat_def] "w ~= zsuc(w)"; -by (res_inst_tac [("z","w")] eq_Abs_Integ 1); -by (asm_full_simp_tac (simpset() addsimps [zadd]) 1); -qed "n_not_zsuc_n"; - -val zsuc_n_not_n = n_not_zsuc_n RS not_sym; - -Goal "w ~= zpred(w)"; -by Safe_tac; -by (dres_inst_tac [("x","w"),("f","zsuc")] arg_cong 1); -by (asm_full_simp_tac (simpset() addsimps [zsuc_zpred,zsuc_n_not_n]) 1); -qed "n_not_zpred_n"; - -val zpred_n_not_n = n_not_zpred_n RS not_sym; - (* Theorems about less and less_equal *) +(*This lemma allows direct proofs of other <-properties*) Goalw [zless_def, znegative_def, zdiff_def, znat_def] - "w ? n. z = w + $#(Suc(n))"; + "(w < z) = (EX n. z = w + $#(Suc n))"; by (res_inst_tac [("z","z")] eq_Abs_Integ 1); by (res_inst_tac [("z","w")] eq_Abs_Integ 1); -by Safe_tac; +by (Clarify_tac 1); by (asm_full_simp_tac (simpset() addsimps [zadd, zminus]) 1); by (safe_tac (claset() addSDs [less_eq_Suc_add])); by (res_inst_tac [("x","k")] exI 1); -by (asm_full_simp_tac (simpset() addsimps add_ac) 1); -qed "zless_eq_zadd_Suc"; - -Goalw [zless_def, znegative_def, zdiff_def, znat_def] - "z < z + $#(Suc(n))"; -by (res_inst_tac [("z","z")] eq_Abs_Integ 1); -by (Clarify_tac 1); -by (simp_tac (simpset() addsimps [zadd, zminus]) 1); -qed "zless_zadd_Suc"; +by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac))); +qed "zless_iff_Suc_zadd"; Goal "[| z1 z1 < (z3::int)"; -by (safe_tac (claset() addSDs [zless_eq_zadd_Suc])); -by (simp_tac - (simpset() addsimps [zadd_assoc, zless_zadd_Suc, znat_add RS sym]) 1); +by (auto_tac (claset(), + simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, + add_znat])); qed "zless_trans"; -Goalw [zsuc_def] "z ~w R *) bind_thm ("zless_irrefl", (zless_not_refl RS notE)); +AddSEs [zless_irrefl]; Goal "z w ~= (z::int)"; -by (blast_tac (claset() addEs [zless_irrefl]) 1); +by (Blast_tac 1); qed "zless_not_refl2"; @@ -608,19 +479,24 @@ by (auto_tac (claset(), simpset() addsimps add_ac)); qed "zless_linear"; +Goal "($# m = $# n) = (m = n)"; +by (fast_tac (claset() addSEs [inj_znat RS injD]) 1); +qed "znat_znat_eq"; +AddIffs [znat_znat_eq]; + +Goal "($#m < $#n) = (m z<=(w::int)"; by (assume_tac 1); @@ -636,18 +512,14 @@ by (Fast_tac 1); qed "not_zleE"; -Goalw [zle_def] "z < w ==> z <= (w::int)"; -by (blast_tac (claset() addEs [zless_asym]) 1); -qed "zless_imp_zle"; - Goalw [zle_def] "z <= w ==> z < w | z=(w::int)"; by (cut_facts_tac [zless_linear] 1); -by (blast_tac (claset() addEs [zless_irrefl,zless_asym]) 1); +by (blast_tac (claset() addEs [zless_asym]) 1); qed "zle_imp_zless_or_eq"; -Goalw [zle_def] "z z <=(w::int)"; +Goalw [zle_def] "z z <= (w::int)"; by (cut_facts_tac [zless_linear] 1); -by (blast_tac (claset() addEs [zless_irrefl,zless_asym]) 1); +by (blast_tac (claset() addEs [zless_asym]) 1); qed "zless_or_eq_imp_zle"; Goal "(x <= (y::int)) = (x < y | x=y)"; @@ -658,11 +530,22 @@ by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq]) 1); qed "zle_refl"; +Goalw [zle_def] "z < w ==> z <= (w::int)"; +by (blast_tac (claset() addEs [zless_asym]) 1); +qed "zless_imp_zle"; + +Addsimps [zle_refl, zless_imp_zle]; + Goal "[| i <= j; j < k |] ==> i < (k::int)"; by (dtac zle_imp_zless_or_eq 1); by (blast_tac (claset() addIs [zless_trans]) 1); qed "zle_zless_trans"; +Goal "[| i < j; j <= k |] ==> i < (k::int)"; +by (dtac zle_imp_zless_or_eq 1); +by (blast_tac (claset() addIs [zless_trans]) 1); +qed "zless_zle_trans"; + Goal "[| i <= j; j <= k |] ==> i <= (k::int)"; by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq, rtac zless_or_eq_imp_zle, @@ -671,27 +554,53 @@ Goal "[| z <= w; w <= z |] ==> z = (w::int)"; by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq, - blast_tac (claset() addEs [zless_irrefl,zless_asym])]); + blast_tac (claset() addEs [zless_asym])]); qed "zle_anti_sym"; -Goal "!!w::int. z + w' = z + w ==> w' = w"; -by (dres_inst_tac [("f", "%x. x + $~z")] arg_cong 1); +Goal "!!w::int. (z + w' = z + w) = (w' = w)"; +by Safe_tac; +by (dres_inst_tac [("f", "%x. x + -z")] arg_cong 1); by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1); qed "zadd_left_cancel"; +Addsimps [zadd_left_cancel]; + +Goal "!!z::int. (w' + z = w + z) = (w' = w)"; +by (asm_full_simp_tac (simpset() addsimps zadd_ac) 1); +qed "zadd_right_cancel"; + +Addsimps [zadd_right_cancel]; + + +Goal "(w < z + $# 1) = (w v + z < w + z"; -by (safe_tac (claset() addSDs [zless_eq_zadd_Suc])); -by (simp_tac (simpset() addsimps zadd_ac) 1); -by (simp_tac (simpset() addsimps [zadd_assoc RS sym, zless_zadd_Suc]) 1); +by (full_simp_tac (simpset() addsimps (zless_iff_Suc_zadd::zadd_ac)) 1); qed "zadd_zless_mono1"; Goal "!!z::int. (v+z < w+z) = (v < w)"; by (safe_tac (claset() addSEs [zadd_zless_mono1])); -by (dres_inst_tac [("z", "$~z")] zadd_zless_mono1 1); +by (dres_inst_tac [("z", "-z")] zadd_zless_mono1 1); by (asm_full_simp_tac (simpset() addsimps [zadd_assoc]) 1); qed "zadd_left_cancel_zless"; @@ -711,142 +620,176 @@ by (etac zadd_zle_mono1 1); qed "zadd_zle_mono"; -Goal "!!z::int. z<=$#0 ==> w+z <= w"; -by (dres_inst_tac [("z", "w")] zadd_zle_mono1 1); -by (asm_full_simp_tac (simpset() addsimps [zadd_commute]) 1); -qed "zadd_zle_self"; - (**** Comparisons: lemmas and proofs by Norbert Voelker ****) -(** One auxiliary theorem...**) - -Goal "(x = False) = (~ x)"; - by (Blast_tac 1); -qed "eq_False_conv"; - -(** Additional theorems for Integ.thy **) - -Addsimps [zless_eq_less, zle_eq_le, - znegative_zminus_znat, not_znegative_znat]; +Goal "(- x < - y) = (y < (x::int))"; +by (rewrite_goals_tac [zless_def,zdiff_def]); +by (simp_tac (simpset() addsimps zadd_ac) 1); +qed "zminus_zless_zminus"; +Addsimps [zminus_zless_zminus]; -Goal "(x::int) = y ==> x <= y"; - by (etac subst 1); by (rtac zle_refl 1); -qed "zequalD1"; +Goal "(- x <= - y) = (y <= (x::int))"; +by (simp_tac (simpset() addsimps [zle_def, zminus_zless_zminus]) 1); +qed "zminus_zle_zminus"; +Addsimps [zminus_zle_zminus]; -Goal "($~ x < $~ y) = (y < x)"; - by (rewrite_goals_tac [zless_def,zdiff_def]); - by (simp_tac (simpset() addsimps zadd_ac ) 1); -qed "zminus_zless_zminus"; +(** The next several equations can make the simplifier loop! **) -Goal "($~ x <= $~ y) = (y <= x)"; - by (simp_tac (HOL_ss addsimps[zle_def, zminus_zless_zminus]) 1); -qed "zminus_zle_zminus"; - -Goal "(x < $~ y) = (y < $~ x)"; - by (rewrite_goals_tac [zless_def,zdiff_def]); - by (simp_tac (simpset() addsimps zadd_ac ) 1); +Goal "(x < - y) = (y < - (x::int))"; +by (rewrite_goals_tac [zless_def,zdiff_def]); +by (simp_tac (simpset() addsimps zadd_ac ) 1); qed "zless_zminus"; -Goal "($~ x < y) = ($~ y < x)"; - by (rewrite_goals_tac [zless_def,zdiff_def]); - by (simp_tac (simpset() addsimps zadd_ac ) 1); +Goal "(- x < y) = (- y < (x::int))"; +by (rewrite_goals_tac [zless_def,zdiff_def]); +by (simp_tac (simpset() addsimps zadd_ac) 1); qed "zminus_zless"; -Goal "(x <= $~ y) = (y <= $~ x)"; - by (simp_tac (HOL_ss addsimps[zle_def, zminus_zless]) 1); +Goal "(x <= - y) = (y <= - (x::int))"; +by (simp_tac (simpset() addsimps [zle_def, zminus_zless]) 1); qed "zle_zminus"; -Goal "($~ x <= y) = ($~ y <= x)"; - by (simp_tac (HOL_ss addsimps[zle_def, zless_zminus]) 1); +Goal "(- x <= y) = (- y <= (x::int))"; +by (simp_tac (simpset() addsimps [zle_def, zless_zminus]) 1); qed "zminus_zle"; -Goal " $#0 < $# Suc n"; - by (rtac (zero_less_Suc RS (zless_eq_less RS iffD2)) 1); -qed "zero_zless_Suc_pos"; +Goal "- $# Suc n < $# 0"; +by (stac (zminus_nat0 RS sym) 1); +by (stac zminus_zless_zminus 1); +by (Simp_tac 1); +qed "negative_zless_0"; -Goal "($# n= $# m) = (n = m)"; - by (fast_tac (HOL_cs addSEs[inj_znat RS injD]) 1); -qed "znat_znat_eq"; -AddIffs[znat_znat_eq]; +Goal "- $# Suc n < $# m"; +by (rtac (negative_zless_0 RS zless_zle_trans) 1); +by (Simp_tac 1); +qed "negative_zless"; +AddIffs [negative_zless]; -Goal "$~ $# Suc n < $#0"; - by (stac (zminus_0 RS sym) 1); - by (rtac (zminus_zless_zminus RS iffD2) 1); - by (rtac (zero_less_Suc RS (zless_eq_less RS iffD2)) 1); -qed "negative_zless_0"; -Addsimps [zero_zless_Suc_pos, negative_zless_0]; +Goal "- $# n <= $#0"; +by (simp_tac (simpset() addsimps [zminus_zle]) 1); +qed "negative_zle_0"; -Goal "$~ $# n <= $#0"; - by (rtac zless_or_eq_imp_zle 1); - by (induct_tac "n" 1); - by (ALLGOALS Asm_simp_tac); -qed "negative_zle_0"; -Addsimps[negative_zle_0]; +Goal "- $# n <= $# m"; +by (rtac (negative_zle_0 RS zle_trans) 1); +by (Simp_tac 1); +qed "negative_zle"; +AddIffs [negative_zle]; -Goal "~($#0 <= $~ $# Suc n)"; - by (stac zle_zminus 1); - by (Simp_tac 1); +Goal "~($# 0 <= - $# Suc n)"; +by (stac zle_zminus 1); +by (Simp_tac 1); qed "not_zle_0_negative"; -Addsimps[not_zle_0_negative]; +Addsimps [not_zle_0_negative]; -Goal "($# n <= $~ $# m) = (n = 0 & m = 0)"; - by (safe_tac HOL_cs); - by (Simp_tac 3); - by (dtac (zle_zminus RS iffD1) 2); - by (ALLGOALS(dtac (negative_zle_0 RSN(2,zle_trans)))); - by (ALLGOALS Asm_full_simp_tac); +Goal "($# n <= - $# m) = (n = 0 & m = 0)"; +by Safe_tac; +by (Simp_tac 3); +by (dtac (zle_zminus RS iffD1) 2); +by (ALLGOALS (dtac (negative_zle_0 RSN(2,zle_trans)))); +by (ALLGOALS Asm_full_simp_tac); qed "znat_zle_znegative"; -Goal "~($# n < $~ $# Suc m)"; - by (rtac notI 1); by (forward_tac [zless_imp_zle] 1); - by (dtac (znat_zle_znegative RS iffD1) 1); - by (safe_tac HOL_cs); - by (dtac (zless_zminus RS iffD1) 1); - by (Asm_full_simp_tac 1); +Goal "~($# n < - $# m)"; +by (simp_tac (simpset() addsimps [symmetric zle_def]) 1); qed "not_znat_zless_negative"; -Goal "($~ $# n = $# m) = (n = 0 & m = 0)"; - by (rtac iffI 1); - by (rtac (znat_zle_znegative RS iffD1) 1); - by (dtac sym 1); - by (ALLGOALS Asm_simp_tac); +Goal "(- $# n = $# m) = (n = 0 & m = 0)"; +by (rtac iffI 1); +by (rtac (znat_zle_znegative RS iffD1) 1); +by (dtac sym 1); +by (ALLGOALS Asm_simp_tac); qed "negative_eq_positive"; -Addsimps [zminus_zless_zminus, zminus_zle_zminus, - negative_eq_positive, not_znat_zless_negative]; +Addsimps [negative_eq_positive, not_znat_zless_negative]; Goalw [zdiff_def,zless_def] "znegative x = (x < $# 0)"; - by Auto_tac; -qed "znegative_less_0"; +by Auto_tac; +qed "znegative_eq_less_0"; Goalw [zdiff_def,zless_def] "(~znegative x) = ($# 0 <= x)"; - by (stac znegative_less_0 1); - by (safe_tac (HOL_cs addSDs[zleD,not_zleE,zleI]) ); -qed "not_znegative_ge_0"; +by (stac znegative_eq_less_0 1); +by (safe_tac (claset() addSDs [zleD,not_zleE,zleI]) ); +qed "not_znegative_eq_ge_0"; -Goal "znegative x ==> ? n. x = $~ $# Suc n"; - by (dtac (znegative_less_0 RS iffD1 RS zless_eq_zadd_Suc) 1); - by (etac exE 1); - by (rtac exI 1); - by (dres_inst_tac [("f","(% z. z + $~ $# Suc n )")] arg_cong 1); - by (auto_tac(claset(), simpset() addsimps [zadd_assoc])); +Goal "znegative x ==> ? n. x = - $# Suc n"; +by (full_simp_tac (simpset() addsimps [znegative_eq_less_0, + zless_iff_Suc_zadd]) 1); +by (etac exE 1); +by (rtac exI 1); +by (dres_inst_tac [("f","(% z. z + - $# Suc n )")] arg_cong 1); +by (auto_tac(claset(), simpset() addsimps [zadd_assoc])); qed "znegativeD"; Goal "~znegative x ==> ? n. x = $# n"; - by (dtac (not_znegative_ge_0 RS iffD1) 1); - by (dtac zle_imp_zless_or_eq 1); - by (etac disjE 1); - by (dtac zless_eq_zadd_Suc 1); - by Auto_tac; +by (dtac (not_znegative_eq_ge_0 RS iffD1) 1); +by (dtac zle_imp_zless_or_eq 1); +by (etac disjE 1); +by (dtac (zless_iff_Suc_zadd RS iffD1) 1); +by Auto_tac; qed "not_znegativeD"; (* a case theorem distinguishing positive and negative int *) -val prems = Goal "[|!! n. P ($# n); !! n. P ($~ $# Suc n) |] ==> P z"; - by (cut_inst_tac [("P","znegative z")] excluded_middle 1); - by (fast_tac (HOL_cs addSDs[znegativeD,not_znegativeD] addSIs prems) 1); +val prems = Goal "[|!! n. P ($# n); !! n. P (- $# Suc n) |] ==> P z"; +by (cut_inst_tac [("P","znegative z")] excluded_middle 1); +by (fast_tac (claset() addSDs [znegativeD,not_znegativeD] addSIs prems) 1); qed "int_cases"; fun int_case_tac x = res_inst_tac [("z",x)] int_cases; + +(*** Subtraction laws ***) + +Goal "x + (y - z) = (x + y) - (z::int)"; +by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1); +qed "zadd_zdiff_eq"; + +Goal "(x - y) + z = (x + z) - (y::int)"; +by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1); +qed "zdiff_zadd_eq"; + +Goal "(x - y) - z = x - (y + (z::int))"; +by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1); +qed "zdiff_zdiff_eq"; + +Goal "x - (y - z) = (x + z) - (y::int)"; +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::int))"; +by (simp_tac (simpset() addsimps zadd_ac) 1); +qed "zdiff_zless_eq"; + +Goalw [zless_def, zdiff_def] "(x < z-y) = (x + (y::int) < z)"; +by (simp_tac (simpset() addsimps zadd_ac) 1); +qed "zless_zdiff_eq"; + +Goalw [zle_def] "(x-y <= z) = (x <= z + (y::int))"; +by (simp_tac (simpset() addsimps [zless_zdiff_eq]) 1); +qed "zdiff_zle_eq"; + +Goalw [zle_def] "(x <= z-y) = (x + (y::int) <= z)"; +by (simp_tac (simpset() addsimps [zdiff_zless_eq]) 1); +qed "zle_zdiff_eq"; + +Goalw [zdiff_def] "(x-y = z) = (x = z + (y::int))"; +by (auto_tac (claset(), simpset() addsimps [zadd_assoc])); +qed "zdiff_eq_eq"; + +Goalw [zdiff_def] "(x = z-y) = (x + (y::int) = z)"; +by (auto_tac (claset(), simpset() addsimps [zadd_assoc])); +qed "eq_zdiff_eq"; + +(*Use with zadd_ac*) +val zcompare_rls = + [symmetric zdiff_def, + zadd_zdiff_eq, zdiff_zadd_eq, zdiff_zdiff_eq, zdiff_zdiff_eq2, + zdiff_zless_eq, zless_zdiff_eq, zdiff_zle_eq, zle_zdiff_eq, + zdiff_eq_eq, eq_zdiff_eq]; + + +(*These rewrite to $# 0, while from Bin onwards we should rewrite to #0 *) +Delsimps [zadd_zminus_inverse_nat, zadd_zminus_inverse_nat2]; + + diff -r 85855f65d0c6 -r 22f8331cdf47 src/HOL/Integ/Integ.thy --- a/src/HOL/Integ/Integ.thy Tue Sep 15 15:04:07 1998 +0200 +++ b/src/HOL/Integ/Integ.thy Tue Sep 15 15:06:29 1998 +0200 @@ -17,14 +17,15 @@ instance int :: {ord, plus, times, minus} +defs + zminus_def + "- Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{(y,x)}) p)" + constdefs znat :: nat => int ("$# _" [80] 80) "$# m == Abs_Integ(intrel ^^ {(m,0)})" - zminus :: int => int ("$~ _" [80] 80) - "$~ Z == Abs_Integ(UN p:Rep_Integ(Z). split (%x y. intrel^^{(y,x)}) p)" - znegative :: int => bool "znegative(Z) == EX x y. xint - "zpred(Z) == Z - $# Suc(0)" - - zsuc :: int=>int - "zsuc(Z) == Z + $# Suc(0)" - defs zadd_def "Z1 + Z2 == Abs_Integ(UN p1:Rep_Integ(Z1). UN p2:Rep_Integ(Z2). split (%x1 y1. split (%x2 y2. intrel^^{(x1+x2, y1+y2)}) p2) p1)" - zdiff_def "Z1 - Z2 == Z1 + zminus(Z2)" + zdiff_def "Z1 - Z2 == Z1 + -(Z2::int)" zless_def "Z1