--- a/src/HOL/Integ/Bin.ML Wed Sep 23 10:17:11 1998 +0200
+++ b/src/HOL/Integ/Bin.ML Wed Sep 23 10:25:37 1998 +0200
@@ -25,10 +25,6 @@
"NCons Min True = Min"
(fn _ => [(Simp_tac 1)]);
-qed_goal "NCons_BIT" Bin.thy
- "NCons (w BIT x) b = (w BIT x) BIT b"
- (fn _ => [(Simp_tac 1)]);
-
qed_goal "bin_succ_1" Bin.thy
"bin_succ(w BIT True) = (bin_succ w) BIT False"
(fn _ => [(Simp_tac 1)]);
@@ -136,7 +132,7 @@
by (simp_tac (simpset() addsimps bin_add_simps) 1);
by (rtac allI 1);
by (induct_tac "w" 1);
-by (ALLGOALS (asm_simp_tac (simpset() addsimps (bin_add_simps @ zadd_ac))));
+by (ALLGOALS (asm_simp_tac (simpset() addsimps bin_add_simps @ zadd_ac)));
qed_spec_mp "integ_of_add";
val bin_mult_simps = [zmult_zminus, integ_of_minus, integ_of_add];
@@ -147,8 +143,7 @@
by (simp_tac (simpset() addsimps bin_mult_simps) 1);
by (simp_tac (simpset() addsimps bin_mult_simps) 1);
by (asm_simp_tac
- (simpset() addsimps (bin_mult_simps @ [zadd_zmult_distrib] @
- zadd_ac)) 1);
+ (simpset() addsimps bin_mult_simps @ [zadd_zmult_distrib] @ zadd_ac) 1);
qed "integ_of_mult";
@@ -218,13 +213,13 @@
qed "add1_zle_eq";
Addsimps [add1_zle_eq];
-Goal "znegative x = (x < #0)";
-by (simp_tac (simpset() addsimps [znegative_eq_less_nat0]) 1);
-qed "znegative_eq_less_0";
+Goal "neg x = (x < #0)";
+by (simp_tac (simpset() addsimps [neg_eq_less_nat0]) 1);
+qed "neg_eq_less_0";
-Goal "(~znegative x) = ($# 0 <= x)";
-by (simp_tac (simpset() addsimps [not_znegative_eq_ge_nat0]) 1);
-qed "not_znegative_eq_ge_0";
+Goal "(~neg x) = ($# 0 <= x)";
+by (simp_tac (simpset() addsimps [not_neg_eq_ge_nat0]) 1);
+qed "not_neg_eq_ge_0";
@@ -252,9 +247,9 @@
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]))));
+ (simpset() addsimps zcompare_rls @
+ [zminus_zadd_distrib RS sym,
+ add_nat])));
qed "iszero_integ_of_BIT";
@@ -262,25 +257,24 @@
Goalw [zless_def,zdiff_def]
"integ_of x < integ_of y \
-\ = znegative (integ_of (bin_add x (bin_minus y)))";
+\ = neg (integ_of (bin_add x (bin_minus y)))";
by (simp_tac (simpset() addsimps bin_mult_simps) 1);
-qed "less_integ_of_eq_zneg";
+qed "less_integ_of_eq_neg";
-Goal "~ znegative (integ_of Pls)";
+Goal "~ neg (integ_of Pls)";
by (Simp_tac 1);
qed "not_neg_integ_of_Pls";
-Goal "znegative (integ_of Min)";
+Goal "neg (integ_of Min)";
by (Simp_tac 1);
qed "neg_integ_of_Min";
-Goal "znegative (integ_of (w BIT x)) = znegative (integ_of w)";
+Goal "neg (integ_of (w BIT x)) = neg (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_nat0,
- symmetric zdiff_def] @
- zcompare_rls))));
+ (simpset() addsimps [add_nat, neg_eq_less_nat0,
+ symmetric zdiff_def] @ zcompare_rls)));
qed "neg_integ_of_BIT";
@@ -290,11 +284,12 @@
by (simp_tac (simpset() addsimps [zle_def]) 1);
qed "le_integ_of_eq_not_less";
+(*Delete the original rewrites, with their clumsy conditional expressions*)
+Delsimps [succ_BIT, pred_BIT, minus_BIT,
+ NCons_Pls, NCons_Min, add_BIT, mult_BIT];
(*Hide the binary representation of integer constants*)
-Delsimps [succ_BIT, pred_BIT, minus_BIT, add_BIT, mult_BIT,
- integ_of_Pls, integ_of_Min, integ_of_BIT,
- norm_Pls, norm_Min, NCons];
+Delsimps [integ_of_Pls, integ_of_Min, integ_of_BIT];
(*Add simplification of arithmetic operations on integer constants*)
Addsimps [integ_of_add RS sym,
@@ -313,7 +308,7 @@
(*... and simplification of relational operations*)
Addsimps [eq_integ_of_eq, iszero_integ_of_Pls, nonzero_integ_of_Min,
iszero_integ_of_BIT,
- less_integ_of_eq_zneg,
+ less_integ_of_eq_neg,
not_neg_integ_of_Pls, neg_integ_of_Min, neg_integ_of_BIT,
le_integ_of_eq_not_less];
@@ -329,7 +324,7 @@
(** Simplification of inequalities involving numerical constants **)
Goal "(w <= z + #1) = (w<=z | w = z + #1)";
-by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq, zless_add1_eq]) 1);
+by (simp_tac (simpset() addsimps [integ_le_less, zless_add1_eq]) 1);
qed "zle_add1_eq";
Goal "(w <= z - #1) = (w<z)";
@@ -360,7 +355,7 @@
qed "zless_imp_zless_zadd1";
Goal "(w < z + #1) = (w<=z)";
-by (simp_tac (simpset() addsimps [zless_add1_eq, zle_eq_zless_or_eq]) 1);
+by (simp_tac (simpset() addsimps [zless_add1_eq, integ_le_less]) 1);
qed "zle_add1_eq_le";
Addsimps [zle_add1_eq_le];
@@ -378,10 +373,10 @@
by (full_simp_tac (simpset() addsimps zadd_ac) 1);
qed "zless_zadd_imp_zless";
-(*LOOPS as a simprule!*)
+(*LOOPS as a simprule! Analogous to Suc_lessD*)
Goal "w + #1 < z ==> w < z";
-bd zless_zadd_imp_zless 1;
-ba 2;
+by (dtac zless_zadd_imp_zless 1);
+by (assume_tac 2);
by (Simp_tac 1);
qed "zless_zadd1_imp_zless";
--- a/src/HOL/Integ/Bin.thy Wed Sep 23 10:17:11 1998 +0200
+++ b/src/HOL/Integ/Bin.thy Wed Sep 23 10:25:37 1998 +0200
@@ -43,9 +43,9 @@
(*NCons inserts a bit, suppressing leading 0s and 1s*)
primrec
- norm_Pls "NCons Pls b = (if b then (Pls BIT b) else Pls)"
- norm_Min "NCons Min b = (if b then Min else (Min BIT b))"
- NCons "NCons (w' BIT x') b = (w' BIT x') BIT b"
+ NCons_Pls "NCons Pls b = (if b then (Pls BIT b) else Pls)"
+ NCons_Min "NCons Min b = (if b then Min else (Min BIT b))"
+ NCons_BIT "NCons (w BIT x) b = (w BIT x) BIT b"
primrec
integ_of_Pls "integ_of Pls = $# 0"
@@ -89,7 +89,7 @@
primrec
mult_Pls "bin_mult Pls w = Pls"
mult_Min "bin_mult Min w = bin_minus w"
- mult_BIT "bin_mult (v BIT x) w =
+ mult_BIT "bin_mult (v BIT x) w =
(if x then (bin_add (NCons (bin_mult v w) False) w)
else (NCons (bin_mult v w) False))"
@@ -141,9 +141,13 @@
fun dest_bin tm =
let
- fun bin_of (Const ("Pls", _)) = []
- | bin_of (Const ("Min", _)) = [~1]
- | bin_of (Const ("op BIT", _) $ bs $ b) = dest_bit b :: bin_of bs
+ (*We consider both "spellings", since Min might be declared elsewhere*)
+ fun bin_of (Const ("Pls", _)) = []
+ | bin_of (Const ("bin.Pls", _)) = []
+ | bin_of (Const ("Min", _)) = [~1]
+ | bin_of (Const ("bin.Min", _)) = [~1]
+ | bin_of (Const ("op BIT", _) $ bs $ b) = dest_bit b :: bin_of bs
+ | bin_of (Const ("bin.op BIT", _) $ bs $ b) = dest_bit b :: bin_of bs
| bin_of _ = raise Match;
fun int_of [] = 0
--- a/src/HOL/Integ/IntDef.ML Wed Sep 23 10:17:11 1998 +0200
+++ b/src/HOL/Integ/IntDef.ML Wed Sep 23 10:25:37 1998 +0200
@@ -81,11 +81,11 @@
qed "inj_Rep_Integ";
-(** znat: the injection from nat to Integ **)
+(** nat: the injection from nat to Integ **)
-Goal "inj(znat)";
+Goal "inj(nat)";
by (rtac injI 1);
-by (rewtac znat_def);
+by (rewtac nat_def);
by (dtac (inj_on_Abs_Integ RS inj_onD) 1);
by (REPEAT (rtac intrel_in_integ 1));
by (dtac eq_equiv_class 1);
@@ -93,7 +93,7 @@
by (Fast_tac 1);
by Safe_tac;
by (Asm_full_simp_tac 1);
-qed "inj_znat";
+qed "inj_nat";
(**** zminus: unary negation on Integ ****)
@@ -137,26 +137,26 @@
by (Asm_full_simp_tac 1);
qed "inj_zminus";
-Goalw [znat_def] "- ($# 0) = $# 0";
+Goalw [nat_def] "- ($# 0) = $# 0";
by (simp_tac (simpset() addsimps [zminus]) 1);
qed "zminus_nat0";
Addsimps [zminus_nat0];
-(**** znegative: the test for negative integers ****)
+(**** neg: the test for negative integers ****)
-Goalw [znegative_def, znat_def] "~ znegative($# n)";
+Goalw [neg_def, nat_def] "~ neg($# n)";
by (Simp_tac 1);
by Safe_tac;
-qed "not_znegative_znat";
+qed "not_neg_nat";
-Goalw [znegative_def, znat_def] "znegative(- $# Suc(n))";
+Goalw [neg_def, nat_def] "neg(- $# Suc(n))";
by (simp_tac (simpset() addsimps [zminus]) 1);
-qed "znegative_zminus_znat";
+qed "neg_zminus_nat";
-Addsimps [znegative_zminus_znat, not_znegative_znat];
+Addsimps [neg_zminus_nat, not_neg_nat];
(**** zadd: addition on Integ ****)
@@ -194,7 +194,7 @@
Goal "(z::int) + w = w + z";
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 (add_ac @ [zadd])) 1);
+by (asm_simp_tac (simpset() addsimps add_ac @ [zadd]) 1);
qed "zadd_commute";
Goal "((z1::int) + z2) + z3 = z1 + (z2 + z3)";
@@ -214,15 +214,15 @@
(*Integer addition is an AC operator*)
val zadd_ac = [zadd_assoc,zadd_commute,zadd_left_commute];
-Goalw [znat_def] "($#m) + ($#n) = $# (m + n)";
+Goalw [nat_def] "($#m) + ($#n) = $# (m + n)";
by (simp_tac (simpset() addsimps [zadd]) 1);
-qed "add_znat";
+qed "add_nat";
Goal "$# (Suc m) = $# 1 + ($# m)";
-by (simp_tac (simpset() addsimps [add_znat]) 1);
-qed "znat_Suc";
+by (simp_tac (simpset() addsimps [add_nat]) 1);
+qed "nat_Suc";
-Goalw [znat_def] "$# 0 + z = z";
+Goalw [nat_def] "$# 0 + z = z";
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
by (asm_simp_tac (simpset() addsimps [zadd]) 1);
qed "zadd_nat0";
@@ -232,7 +232,7 @@
by (rtac zadd_nat0 1);
qed "zadd_nat0_right";
-Goalw [znat_def] "z + (- z) = $# 0";
+Goalw [nat_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_nat";
@@ -309,28 +309,28 @@
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);
+by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
qed "zmult_zminus";
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);
+by (asm_simp_tac (simpset() addsimps [zminus, zmult] @ add_ac) 1);
qed "zmult_zminus_zminus";
Goal "(z::int) * w = w * z";
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 ([zmult] @ add_ac @ mult_ac)) 1);
+by (asm_simp_tac (simpset() addsimps [zmult] @ add_ac @ mult_ac) 1);
qed "zmult_commute";
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);
by (res_inst_tac [("z","z3")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps ([add_mult_distrib2,zmult] @
- add_ac @ mult_ac)) 1);
+by (asm_simp_tac (simpset() addsimps [add_mult_distrib2,zmult] @
+ add_ac @ mult_ac) 1);
qed "zmult_assoc";
(*For AC rewriting*)
@@ -348,8 +348,8 @@
by (res_inst_tac [("z","z2")] eq_Abs_Integ 1);
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
by (asm_simp_tac
- (simpset() addsimps ([add_mult_distrib2, zadd, zmult] @
- add_ac @ mult_ac)) 1);
+ (simpset() addsimps [add_mult_distrib2, zadd, zmult] @
+ add_ac @ mult_ac) 1);
qed "zadd_zmult_distrib";
val zmult_commute'= read_instantiate [("z","w")] zmult_commute;
@@ -362,12 +362,12 @@
by (simp_tac (simpset() addsimps [zmult_commute',zadd_zmult_distrib]) 1);
qed "zadd_zmult_distrib2";
-Goalw [znat_def] "$# 0 * z = $# 0";
+Goalw [nat_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";
-Goalw [znat_def] "$# 1 * z = z";
+Goalw [nat_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";
@@ -393,7 +393,7 @@
(* Theorems about less and less_equal *)
(*This lemma allows direct proofs of other <-properties*)
-Goalw [zless_def, znegative_def, zdiff_def, znat_def]
+Goalw [zless_def, neg_def, zdiff_def, nat_def]
"(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);
@@ -407,24 +407,24 @@
Goal "z < z + $# (Suc n)";
by (auto_tac (claset(),
simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc,
- add_znat]));
+ add_nat]));
qed "zless_zadd_Suc";
Goal "[| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
by (auto_tac (claset(),
simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc,
- add_znat]));
+ add_nat]));
qed "zless_trans";
Goal "!!w::int. z<w ==> ~w<z";
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);
+by (asm_full_simp_tac (simpset() addsimps [nat_def, zadd]) 1);
qed "zless_not_sym";
(* [| n<m; ~P ==> m<n |] ==> P *)
-bind_thm ("zless_asym", (zless_not_sym RS swap));
+bind_thm ("zless_asym", zless_not_sym RS swap);
Goal "!!z::int. ~ z<z";
by (resolve_tac [zless_asym RS notI] 1);
@@ -444,7 +444,7 @@
(*"Less than" is a linear ordering*)
-Goalw [zless_def, znegative_def, zdiff_def]
+Goalw [zless_def, neg_def, zdiff_def]
"z<w | z=w | w<(z::int)";
by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
@@ -464,13 +464,13 @@
bind_thm("int_neqE", int_neq_iff RS iffD1 RS disjE);
Goal "($# m = $# n) = (m = n)";
-by (fast_tac (claset() addSEs [inj_znat RS injD]) 1);
-qed "znat_znat_eq";
-AddIffs [znat_znat_eq];
+by (fast_tac (claset() addSEs [inj_nat RS injD]) 1);
+qed "nat_nat_eq";
+AddIffs [nat_nat_eq];
Goal "($#m < $#n) = (m<n)";
by (simp_tac (simpset() addsimps [less_iff_Suc_add, zless_iff_Suc_zadd,
- add_znat]) 1);
+ add_nat]) 1);
qed "zless_eq_less";
Addsimps [zless_eq_less];
@@ -513,10 +513,10 @@
Goal "(x <= (y::int)) = (x < y | x=y)";
by (REPEAT(ares_tac [iffI, zless_or_eq_imp_zle, zle_imp_zless_or_eq] 1));
-qed "zle_eq_zless_or_eq";
+qed "integ_le_less";
Goal "w <= (w::int)";
-by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq]) 1);
+by (simp_tac (simpset() addsimps [integ_le_less]) 1);
qed "zle_refl";
Goalw [zle_def] "z < w ==> z <= (w::int)";
@@ -527,7 +527,7 @@
(* Axiom 'linorder_linear' of class 'linorder': *)
Goal "(z::int) <= w | w <= z";
-by (simp_tac (simpset() addsimps [zle_eq_zless_or_eq]) 1);
+by (simp_tac (simpset() addsimps [integ_le_less]) 1);
by (cut_facts_tac [zless_linear] 1);
by (Blast_tac 1);
qed "zle_linear";
@@ -567,19 +567,19 @@
(*** Subtraction laws ***)
Goal "x + (y - z) = (x + y) - (z::int)";
-by (simp_tac (simpset() addsimps (zdiff_def::zadd_ac)) 1);
+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);
+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);
+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);
+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))";
@@ -636,10 +636,10 @@
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);
+ add_nat]));
+by (cut_inst_tac [("m","n")] nat_Suc 1);
by (exhaust_tac "n" 1);
-auto();
+by Auto_tac;
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";
--- a/src/HOL/Integ/IntDef.thy Wed Sep 23 10:17:11 1998 +0200
+++ b/src/HOL/Integ/IntDef.thy Wed Sep 23 10:25:37 1998 +0200
@@ -23,11 +23,11 @@
constdefs
- znat :: nat => int ("$# _" [80] 80)
+ nat :: nat => int ("$# _" [80] 80)
"$# m == Abs_Integ(intrel ^^ {(m,0)})"
- znegative :: int => bool
- "znegative(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)"
+ neg :: int => bool
+ "neg(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)"
(*For simplifying equalities*)
iszero :: int => bool
@@ -41,7 +41,7 @@
zdiff_def "Z1 - Z2 == Z1 + -(Z2::int)"
- zless_def "Z1<Z2 == znegative(Z1 - Z2)"
+ zless_def "Z1<Z2 == neg(Z1 - Z2)"
zle_def "Z1 <= (Z2::int) == ~(Z2 < Z1)"
--- a/src/HOL/Integ/Integ.ML Wed Sep 23 10:17:11 1998 +0200
+++ b/src/HOL/Integ/Integ.ML Wed Sep 23 10:25:37 1998 +0200
@@ -6,43 +6,42 @@
Type "int" is a linear order
*)
-Goal "(w<z) = znegative(w-z)";
+Goal "(w<z) = neg(w-z)";
by (simp_tac (simpset() addsimps [zless_def]) 1);
-qed "zless_eq_znegative";
+qed "zless_eq_neg";
Goal "(w=z) = iszero(w-z)";
by (simp_tac (simpset() addsimps [iszero_def, zdiff_eq_eq]) 1);
qed "eq_eq_iszero";
-Goal "(w<=z) = (~ znegative(z-w))";
+Goal "(w<=z) = (~ neg(z-w))";
by (simp_tac (simpset() addsimps [zle_def, zless_def]) 1);
-qed "zle_eq_not_znegative";
+qed "zle_eq_not_neg";
(*This list of rewrites simplifies (in)equalities by subtracting the RHS
from the LHS, then using the cancellation simproc. Use with zadd_ac.*)
val zcompare_0_rls =
- [zdiff_def, zless_eq_znegative, eq_eq_iszero, zle_eq_not_znegative];
-
+ [zdiff_def, zless_eq_neg, eq_eq_iszero, zle_eq_not_neg];
(*** Monotonicity results ***)
Goal "(v+z < w+z) = (v < (w::int))";
-by (full_simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
+by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
qed "zadd_right_cancel_zless";
Goal "(z+v < z+w) = (v < (w::int))";
-by (full_simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
+by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
qed "zadd_left_cancel_zless";
Addsimps [zadd_right_cancel_zless, zadd_left_cancel_zless];
Goal "(v+z <= w+z) = (v <= (w::int))";
-by (full_simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
+by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
qed "zadd_right_cancel_zle";
Goal "(z+v <= z+w) = (v <= (w::int))";
-by (full_simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
+by (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
qed "zadd_left_cancel_zle";
Addsimps [zadd_right_cancel_zle, zadd_left_cancel_zle];
@@ -67,39 +66,35 @@
(*** Comparison laws ***)
Goal "(- x < - y) = (y < (x::int))";
-by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
+by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
qed "zminus_zless_zminus";
Addsimps [zminus_zless_zminus];
Goal "(- x <= - y) = (y <= (x::int))";
-by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
+by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
qed "zminus_zle_zminus";
Addsimps [zminus_zle_zminus];
(** The next several equations can make the simplifier loop! **)
Goal "(x < - y) = (y < - (x::int))";
-by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
+by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
qed "zless_zminus";
Goal "(- x < y) = (- y < (x::int))";
-by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
+by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
qed "zminus_zless";
Goal "(x <= - y) = (y <= - (x::int))";
-by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
+by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
qed "zle_zminus";
Goal "(- x <= y) = (- y <= (x::int))";
-by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
+by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
qed "zminus_zle";
-Goal "$#0 < $# Suc n";
-by (Simp_tac 1);
-qed "zero_zless_Suc";
-
Goal "- $# Suc n < $# 0";
-by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
+by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
qed "negative_zless_0";
Goal "- $# Suc n < $# m";
@@ -109,11 +104,11 @@
AddIffs [negative_zless];
Goal "- $# n <= $#0";
-by (simp_tac (simpset() addsimps (zcompare_0_rls @ zadd_ac)) 1);
+by (simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac) 1);
qed "negative_zle_0";
Goal "- $# n <= $# m";
-by (simp_tac (simpset() addsimps (add_znat::(zcompare_0_rls @ zadd_ac))) 1);
+by (simp_tac (simpset() addsimps add_nat :: zcompare_0_rls @ zadd_ac) 1);
qed "negative_zle";
AddIffs [negative_zle];
@@ -129,67 +124,76 @@
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";
+qed "nat_zle_neg";
Goal "~($# n < - $# m)";
by (simp_tac (simpset() addsimps [symmetric zle_def]) 1);
-qed "not_znat_zless_negative";
+qed "not_nat_zless_negative";
Goal "(- $# n = $# m) = (n = 0 & m = 0)";
by (rtac iffI 1);
-by (rtac (znat_zle_znegative RS iffD1) 1);
+by (rtac (nat_zle_neg RS iffD1) 1);
by (dtac sym 1);
by (ALLGOALS Asm_simp_tac);
qed "negative_eq_positive";
-Addsimps [negative_eq_positive, not_znat_zless_negative];
+Addsimps [negative_eq_positive, not_nat_zless_negative];
+
+Goal "(w <= z) = (EX n. z = w + $# n)";
+by (auto_tac (claset(),
+ simpset() addsimps [zless_iff_Suc_zadd, integ_le_less]));
+by (ALLGOALS (full_simp_tac (simpset() addsimps zcompare_0_rls @ zadd_ac)));
+by (ALLGOALS (full_simp_tac (simpset() addsimps [iszero_def])));
+by (blast_tac (claset() addIs [Suc_pred RS sym]) 1);
+qed "zle_iff_zadd";
+
+
+Goalw [zdiff_def,zless_def] "neg x = (x < $# 0)";
+by Auto_tac;
+qed "neg_eq_less_nat0";
+
+Goalw [zle_def] "(~neg x) = ($# 0 <= x)";
+by (simp_tac (simpset() addsimps [neg_eq_less_nat0]) 1);
+qed "not_neg_eq_ge_nat0";
-Goalw [zdiff_def,zless_def] "znegative x = (x < $# 0)";
-by Auto_tac;
-qed "znegative_eq_less_nat0";
+(**** nat_of: magnitide of an integer, as a natural number ****)
-Goalw [zle_def] "(~znegative x) = ($# 0 <= x)";
-by (simp_tac (simpset() addsimps [znegative_eq_less_nat0]) 1);
-qed "not_znegative_eq_ge_nat0";
-
-(**** zmagnitude: magnitide of an integer, as a natural number ****)
+Goalw [nat_of_def] "nat_of($# n) = n";
+by Auto_tac;
+qed "nat_of_nat";
-Goalw [zmagnitude_def] "zmagnitude($# n) = n";
-by Auto_tac;
-qed "zmagnitude_znat";
-
-Goalw [zmagnitude_def] "zmagnitude(- $# n) = n";
+Goalw [nat_of_def] "nat_of(- $# n) = n";
by Auto_tac;
-qed "zmagnitude_zminus_znat";
+qed "nat_of_zminus_nat";
-Addsimps [zmagnitude_znat, zmagnitude_zminus_znat];
+Addsimps [nat_of_nat, nat_of_zminus_nat];
-Goal "~ znegative z ==> $# (zmagnitude z) = z";
-by (dtac (not_znegative_eq_ge_nat0 RS iffD1) 1);
+Goal "~ neg z ==> $# (nat_of z) = z";
+by (dtac (not_neg_eq_ge_nat0 RS iffD1) 1);
by (dtac zle_imp_zless_or_eq 1);
by (auto_tac (claset(), simpset() addsimps [zless_iff_Suc_zadd]));
-qed "not_zneg_mag";
+qed "not_neg_nat_of";
-Goal "znegative x ==> ? n. x = - $# Suc n";
+Goal "neg x ==> ? n. x = - $# Suc n";
by (auto_tac (claset(),
- simpset() addsimps [znegative_eq_less_nat0, zless_iff_Suc_zadd,
+ simpset() addsimps [neg_eq_less_nat0, zless_iff_Suc_zadd,
zdiff_eq_eq RS sym, zdiff_def]));
-qed "znegativeD";
+qed "negD";
-Goal "znegative z ==> $# (zmagnitude z) = -z";
-bd znegativeD 1;
+Goal "neg z ==> $# (nat_of z) = -z";
+by (dtac negD 1);
by Auto_tac;
-qed "zneg_mag";
+qed "neg_nat_of";
(* a case theorem distinguishing positive and negative int *)
val prems = Goal "[|!! n. P ($# n); !! n. P (- $# Suc n) |] ==> P z";
-by (case_tac "znegative z" 1);
-by (blast_tac (claset() addSDs [znegativeD] addSIs prems) 1);
-be (not_zneg_mag RS subst) 1;
-brs prems 1;
+by (case_tac "neg z" 1);
+by (blast_tac (claset() addSDs [negD] addSIs prems) 1);
+by (etac (not_neg_nat_of RS subst) 1);
+by (resolve_tac prems 1);
qed "int_cases";
fun int_case_tac x = res_inst_tac [("z",x)] int_cases;
--- a/src/HOL/Integ/Integ.thy Wed Sep 23 10:17:11 1998 +0200
+++ b/src/HOL/Integ/Integ.thy Wed Sep 23 10:25:37 1998 +0200
@@ -12,7 +12,7 @@
instance int :: linorder (zle_linear)
constdefs
- zmagnitude :: int => nat
- "zmagnitude(Z) == @m. Z = $# m | -Z = $# m"
+ nat_of :: int => nat
+ "nat_of(Z) == @m. Z = $# m | -Z = $# m"
end