--- 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) = (w<z | w=z)";
+by (simp_tac (simpset() addsimps [zless_add_nat1_eq]) 1);
+qed "zless_add1_eq";
+
+Goal "(w + #1 <= z) = (w<z)";
+by (simp_tac (simpset() addsimps [add_nat1_zle_eq]) 1);
+qed "add1_zle_eq";
+Addsimps [add1_zle_eq];
+
+
+(** Simplification rules for comparison of binary numbers (Norbert Voelker) **)
+
+(** Equals (=) **)
-Addsimps [integ_of_bin_add RS sym,
- integ_of_bin_minus RS sym,
- integ_of_bin_mult RS sym,
+Goalw [iszero_def]
+ "(integ_of x = integ_of y) \
+\ = iszero(integ_of (bin_add x (bin_minus y)))";
+by (simp_tac (simpset() addsimps
+ (zcompare_rls @ [integ_of_add, integ_of_minus])) 1);
+qed "eq_integ_of_eq";
+
+Goalw [iszero_def] "iszero (integ_of PlusSign)";
+by (Simp_tac 1);
+qed "iszero_integ_of_Plus";
+
+Goalw [iszero_def] "~ iszero(integ_of MinusSign)";
+by (Simp_tac 1);
+qed "nonzero_integ_of_Minus";
+
+Goalw [iszero_def]
+ "iszero (integ_of (Bcons w x)) = (~x & iszero (integ_of w))";
+by (Simp_tac 1);
+by (int_case_tac "integ_of w" 1);
+by (ALLGOALS (asm_simp_tac
+ (simpset() addsimps (zcompare_rls @
+ [zminus_zadd_distrib RS sym,
+ add_znat]))));
+qed "iszero_integ_of_Bcons";
+
+
+(** Less-than (<) **)
+
+Goalw [zless_def,zdiff_def]
+ "integ_of x < integ_of y \
+\ = znegative (integ_of (bin_add x (bin_minus y)))";
+by (simp_tac (simpset() addsimps bin_mult_simps) 1);
+qed "less_integ_of_eq_zneg";
+
+Goal "~ znegative (integ_of PlusSign)";
+by (Simp_tac 1);
+qed "not_neg_integ_of_Plus";
+
+Goal "znegative (integ_of MinusSign)";
+by (Simp_tac 1);
+qed "neg_integ_of_Minus";
+
+Goal "znegative (integ_of (Bcons w x)) = znegative (integ_of w)";
+by (Asm_simp_tac 1);
+by (int_case_tac "integ_of w" 1);
+by (ALLGOALS (asm_simp_tac
+ (simpset() addsimps ([add_znat, znegative_eq_less_0,
+ symmetric zdiff_def] @
+ zcompare_rls))));
+qed "neg_integ_of_Bcons";
+
+
+(** Less-than-or-equals (<=) **)
+
+Goal "(integ_of x <= integ_of y) = (~ integ_of y < integ_of x)";
+by (simp_tac (simpset() addsimps [zle_def]) 1);
+qed "le_integ_of_eq_not_less";
+
+
+(*Hide the binary representation of integer constants*)
+Delsimps [succ_Bcons, pred_Bcons, min_Bcons, add_Bcons, mult_Bcons,
+ integ_of_Plus, integ_of_Minus, integ_of_Bcons,
+ norm_Plus, norm_Minus, norm_Bcons];
+
+(*Add simplification of arithmetic operations on integer constants*)
+Addsimps [integ_of_add RS sym,
+ integ_of_minus RS sym,
+ integ_of_mult RS sym,
bin_succ_Bcons1,bin_succ_Bcons0,
bin_pred_Bcons1,bin_pred_Bcons0,
bin_minus_Bcons1,bin_minus_Bcons0,
@@ -184,89 +316,17 @@
norm_Bcons_Minus_0,norm_Bcons_Minus_1,
norm_Bcons_Bcons];
-
-(** Simplification rules for comparison of binary numbers (Norbert Voelker) **)
-
-Addsimps [zadd_assoc];
-
-Goal "(integ_of_bin x = integ_of_bin y) \
-\ = (integ_of_bin (bin_add x (bin_minus y)) = $# 0)";
- by (simp_tac (HOL_ss addsimps
- [integ_of_bin_add, integ_of_bin_minus,zdiff_def]) 1);
- by (rtac iffI 1);
- by (etac ssubst 1);
- by (rtac zadd_zminus_inverse 1);
- by (dres_inst_tac [("f","(% z. z + integ_of_bin y)")] arg_cong 1);
- by (asm_full_simp_tac
- (HOL_ss addsimps[zadd_assoc,zadd_0,zadd_0_right,
- zadd_zminus_inverse2]) 1);
-val iob_eq_eq_diff_0 = result();
-
-Goal "(integ_of_bin PlusSign = $# 0) = True";
- by (stac iob_Plus 1); by (Simp_tac 1);
-val iob_Plus_eq_0 = result();
-
-Goal "(integ_of_bin MinusSign = $# 0) = False";
- by (stac iob_Minus 1);
- by (Simp_tac 1);
-val iob_Minus_not_eq_0 = result();
-
-Goal "(integ_of_bin (Bcons w x) = $# 0) = (~x & integ_of_bin w = $# 0)";
- by (stac iob_Bcons 1);
- by (case_tac "x" 1);
- by (ALLGOALS Asm_simp_tac);
- by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [integ_of_bin_add])));
- by (ALLGOALS(int_case_tac "integ_of_bin w"));
- by (ALLGOALS(asm_simp_tac
- (simpset() addsimps[zminus_zadd_distrib RS sym,
- znat_add RS sym])));
- by (rtac notI 1);
- (*Add Suc(Suc(n + n)) to both sides*)
- by (dres_inst_tac [("f","(% z. z + $# Suc (Suc (n + n)))")] arg_cong 1);
- by (Asm_full_simp_tac 1);
-val iob_Bcons_eq_0 = result();
+(*... and simplification of relational operations*)
+Addsimps [eq_integ_of_eq, iszero_integ_of_Plus, nonzero_integ_of_Minus,
+ iszero_integ_of_Bcons,
+ less_integ_of_eq_zneg,
+ not_neg_integ_of_Plus, neg_integ_of_Minus, neg_integ_of_Bcons,
+ le_integ_of_eq_not_less];
-Goalw [zless_def,zdiff_def]
- "integ_of_bin x < integ_of_bin y \
-\ = (integ_of_bin (bin_add x (bin_minus y)) < $# 0)";
- by (Simp_tac 1);
-val iob_less_eq_diff_lt_0 = result();
-
-Goal "(integ_of_bin PlusSign < $# 0) = False";
- by (stac iob_Plus 1); by (Simp_tac 1);
-val iob_Plus_not_lt_0 = result();
-
-Goal "(integ_of_bin MinusSign < $# 0) = True";
- by (stac iob_Minus 1); by (Simp_tac 1);
-val iob_Minus_lt_0 = result();
+Goalw [zdiff_def]
+ "integ_of v - integ_of w = integ_of(bin_add v (bin_minus w))";
+by (Simp_tac 1);
+qed "diff_integ_of_eq";
-Goal "(integ_of_bin (Bcons w x) < $# 0) = (integ_of_bin w < $# 0)";
- by (stac iob_Bcons 1);
- by (case_tac "x" 1);
- by (ALLGOALS Asm_simp_tac);
- by (ALLGOALS(asm_simp_tac (HOL_ss addsimps [integ_of_bin_add])));
- by (ALLGOALS(int_case_tac "integ_of_bin w"));
- by (ALLGOALS(asm_simp_tac
- (simpset() addsimps[zminus_zadd_distrib RS sym,
- znat_add RS sym])));
- by (stac (zadd_zminus_inverse RS sym) 1);
- by (rtac zadd_zless_mono1 1);
- by (Simp_tac 1);
-val iob_Bcons_lt_0 = result();
-
-Goal "integ_of_bin x <= integ_of_bin y \
-\ = ( integ_of_bin (bin_add x (bin_minus y)) < $# 0 \
-\ | integ_of_bin (bin_add x (bin_minus y)) = $# 0)";
-by (simp_tac (HOL_ss addsimps
- [zle_eq_zless_or_eq,iob_less_eq_diff_lt_0,zdiff_def
- ,iob_eq_eq_diff_0,integ_of_bin_minus,integ_of_bin_add]) 1);
-val iob_le_diff_lt_0_or_eq_0 = result();
-
-Delsimps [zless_eq_less, zle_eq_le, zadd_assoc, znegative_zminus_znat,
- not_znegative_znat, zero_zless_Suc_pos, negative_zless_0,
- negative_zle_0, not_zle_0_negative, not_znat_zless_negative,
- zminus_zless_zminus, zminus_zle_zminus, negative_eq_positive];
-
-Addsimps [zdiff_def, iob_eq_eq_diff_0, iob_less_eq_diff_lt_0,
- iob_le_diff_lt_0_or_eq_0, iob_Plus_eq_0, iob_Minus_not_eq_0,
- iob_Bcons_eq_0, iob_Plus_not_lt_0, iob_Minus_lt_0, iob_Bcons_lt_0];
+(*... and finally subtraction*)
+Addsimps [diff_integ_of_eq];
--- a/src/HOL/Integ/Bin.thy Tue Sep 15 15:04:07 1998 +0200
+++ b/src/HOL/Integ/Bin.thy Tue Sep 15 15:06:29 1998 +0200
@@ -33,7 +33,7 @@
| Bcons bin bool
consts
- integ_of_bin :: bin=>int
+ 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;
--- 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<z ==> ? 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<z2; z2<z3 |] ==> 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<zsuc(z)";
-by (rtac zless_zadd_Suc 1);
-qed "zlessI";
-
-val zless_zsucI = zlessI RSN (2,zless_trans);
-
Goal "!!w::int. z<w ==> ~w<z";
-by (safe_tac (claset() addSDs [zless_eq_zadd_Suc]));
+by (safe_tac (claset() addSDs [zless_iff_Suc_zadd RS iffD1]));
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
by Safe_tac;
by (asm_full_simp_tac (simpset() addsimps ([znat_def, zadd])) 1);
@@ -590,9 +460,10 @@
(* z<z ==> R *)
bind_thm ("zless_irrefl", (zless_not_refl RS notE));
+AddSEs [zless_irrefl];
Goal "z<w ==> 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<n)";
+by (simp_tac (simpset() addsimps [less_iff_Suc_add, zless_iff_Suc_zadd,
+ add_znat]) 1);
+qed "zless_eq_less";
+Addsimps [zless_eq_less];
+
(*** Properties of <= ***)
-Goalw [zless_def, znegative_def, zdiff_def, znat_def]
- "($#m < $#n) = (m<n)";
-by (simp_tac
- (simpset() addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
-by (fast_tac (claset() addIs [add_commute] addSEs [less_add_eq_less]) 1);
-qed "zless_eq_less";
-
Goalw [zle_def, le_def] "($#m <= $#n) = (m<=n)";
-by (simp_tac (simpset() addsimps [zless_eq_less]) 1);
+by (Simp_tac 1);
qed "zle_eq_le";
+Addsimps [zle_eq_le];
Goalw [zle_def] "~(w<z) ==> 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<w | z=w ==> z <=(w::int)";
+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 "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<z | w=z)";
+by (auto_tac (claset(),
+ simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc,
+ add_znat]));
+by (cut_inst_tac [("m","n")] znat_Suc 1);
+by (exhaust_tac "n" 1);
+auto();
+by (full_simp_tac (simpset() addsimps zadd_ac) 1);
+by (asm_full_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
+qed "zless_add_nat1_eq";
+
+
+Goal "(w + $# 1 <= z) = (w<z)";
+by (simp_tac (simpset() addsimps [zle_def, zless_add_nat1_eq]) 1);
+by (auto_tac (claset() addIs [zle_anti_sym] addEs [zless_asym],
+ simpset() addsimps [symmetric zle_def]));
+qed "add_nat1_zle_eq";
+
(*** Monotonicity results ***)
Goal "!!z::int. v < 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];
+
+
--- 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. x<y & (x,y::nat):Rep_Integ(Z)"
@@ -32,19 +33,13 @@
"zmagnitude(Z) == Abs_Integ(UN p:Rep_Integ(Z).
split (%x y. intrel^^{((y-x) + (x-y),0)}) p)"
- zpred :: int=>int
- "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<Z2 == znegative(Z1 - Z2)"
--- a/src/HOL/ex/BinEx.ML Tue Sep 15 15:04:07 1998 +0200
+++ b/src/HOL/ex/BinEx.ML Tue Sep 15 15:06:29 1998 +0200
@@ -1,6 +1,8 @@
(*** Examples of performing binary arithmetic by simplification ***)
+(** Addition **)
+
Goal "#13 + #19 = #32";
by (Simp_tac 1);
result();
@@ -17,14 +19,19 @@
by (Simp_tac 1);
result();
-Goal "$~ #65745 = #~65745";
+(** Negation **)
+
+Goal "- #65745 = #~65745";
by (Simp_tac 1);
result();
-Goal "$~ #~54321 = #54321";
+Goal "- #~54321 = #54321";
by (Simp_tac 1);
result();
+
+(** Multiplication **)
+
Goal "#13 * #19 = #247";
by (Simp_tac 1);
result();
--- a/src/HOL/ex/IntRingDefs.thy Tue Sep 15 15:04:07 1998 +0200
+++ b/src/HOL/ex/IntRingDefs.thy Tue Sep 15 15:06:29 1998 +0200
@@ -7,9 +7,9 @@
Most of it has been defined and shown already.
*)
-IntRingDefs = Integ + Ring +
+IntRingDefs = Main + Ring +
instance int :: zero
-defs zero_int_def "zero::int == $# 0"
+defs zero_int_def "zero::int == #0"
end