--- a/src/HOL/Integ/Equiv.ML Tue Nov 18 09:45:45 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-
-(* legacy ML bindings *)
-
-val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";
-val UN_constant_eq = thm "UN_constant_eq";
-val UN_equiv_class = thm "UN_equiv_class";
-val UN_equiv_class2 = thm "UN_equiv_class2";
-val UN_equiv_class_inject = thm "UN_equiv_class_inject";
-val UN_equiv_class_type = thm "UN_equiv_class_type";
-val UN_equiv_class_type2 = thm "UN_equiv_class_type2";
-val Union_quotient = thm "Union_quotient";
-val comp_equivI = thm "comp_equivI";
-val congruent2I = thm "congruent2I";
-val congruent2_commuteI = thm "congruent2_commuteI";
-val congruent2_def = thm "congruent2_def";
-val congruent2_implies_congruent = thm "congruent2_implies_congruent";
-val congruent2_implies_congruent_UN = thm "congruent2_implies_congruent_UN";
-val congruent_def = thm "congruent_def";
-val eq_equiv_class = thm "eq_equiv_class";
-val eq_equiv_class_iff = thm "eq_equiv_class_iff";
-val equiv_class_eq = thm "equiv_class_eq";
-val equiv_class_eq_iff = thm "equiv_class_eq_iff";
-val equiv_class_nondisjoint = thm "equiv_class_nondisjoint";
-val equiv_class_self = thm "equiv_class_self";
-val equiv_class_subset = thm "equiv_class_subset";
-val equiv_comp_eq = thm "equiv_comp_eq";
-val equiv_def = thm "equiv_def";
-val equiv_imp_dvd_card = thm "equiv_imp_dvd_card";
-val equiv_type = thm "equiv_type";
-val finite_equiv_class = thm "finite_equiv_class";
-val finite_quotient = thm "finite_quotient";
-val quotientE = thm "quotientE";
-val quotientI = thm "quotientI";
-val quotient_def = thm "quotient_def";
-val quotient_disj = thm "quotient_disj";
-val refl_comp_subset = thm "refl_comp_subset";
-val subset_equiv_class = thm "subset_equiv_class";
-val sym_trans_comp_subset = thm "sym_trans_comp_subset";
--- a/src/HOL/Integ/Equiv.thy Tue Nov 18 09:45:45 2003 +0100
+++ b/src/HOL/Integ/Equiv.thy Tue Nov 18 11:01:52 2003 +0100
@@ -270,4 +270,46 @@
apply (simp_all add: Union_quotient equiv_type finite_quotient)
done
+ML
+{*
+
+(* legacy ML bindings *)
+
+val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";
+val UN_constant_eq = thm "UN_constant_eq";
+val UN_equiv_class = thm "UN_equiv_class";
+val UN_equiv_class2 = thm "UN_equiv_class2";
+val UN_equiv_class_inject = thm "UN_equiv_class_inject";
+val UN_equiv_class_type = thm "UN_equiv_class_type";
+val UN_equiv_class_type2 = thm "UN_equiv_class_type2";
+val Union_quotient = thm "Union_quotient";
+val comp_equivI = thm "comp_equivI";
+val congruent2I = thm "congruent2I";
+val congruent2_commuteI = thm "congruent2_commuteI";
+val congruent2_def = thm "congruent2_def";
+val congruent2_implies_congruent = thm "congruent2_implies_congruent";
+val congruent2_implies_congruent_UN = thm "congruent2_implies_congruent_UN";
+val congruent_def = thm "congruent_def";
+val eq_equiv_class = thm "eq_equiv_class";
+val eq_equiv_class_iff = thm "eq_equiv_class_iff";
+val equiv_class_eq = thm "equiv_class_eq";
+val equiv_class_eq_iff = thm "equiv_class_eq_iff";
+val equiv_class_nondisjoint = thm "equiv_class_nondisjoint";
+val equiv_class_self = thm "equiv_class_self";
+val equiv_class_subset = thm "equiv_class_subset";
+val equiv_comp_eq = thm "equiv_comp_eq";
+val equiv_def = thm "equiv_def";
+val equiv_imp_dvd_card = thm "equiv_imp_dvd_card";
+val equiv_type = thm "equiv_type";
+val finite_equiv_class = thm "finite_equiv_class";
+val finite_quotient = thm "finite_quotient";
+val quotientE = thm "quotientE";
+val quotientI = thm "quotientI";
+val quotient_def = thm "quotient_def";
+val quotient_disj = thm "quotient_disj";
+val refl_comp_subset = thm "refl_comp_subset";
+val subset_equiv_class = thm "subset_equiv_class";
+val sym_trans_comp_subset = thm "sym_trans_comp_subset";
+*}
+
end
--- a/src/HOL/Integ/IntArith.ML Tue Nov 18 09:45:45 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,221 +0,0 @@
-(* Title: HOL/Integ/IntArith.ML
- ID: $Id$
- Authors: Larry Paulson and Tobias Nipkow
-*)
-
-
-Goal "x - - y = x + (y::int)";
-by (Simp_tac 1);
-qed "int_diff_minus_eq";
-Addsimps [int_diff_minus_eq];
-
-Goal "abs(abs(x::int)) = abs(x)";
-by (arith_tac 1);
-qed "abs_abs";
-Addsimps [abs_abs];
-
-Goal "abs(-(x::int)) = abs(x)";
-by (arith_tac 1);
-qed "abs_minus";
-Addsimps [abs_minus];
-
-Goal "abs(x+y) <= abs(x) + abs(y::int)";
-by (arith_tac 1);
-qed "triangle_ineq";
-
-
-(*** Intermediate value theorems ***)
-
-Goal "(ALL i<n::nat. abs(f(i+1) - f i) <= 1) --> \
-\ f 0 <= k --> k <= f n --> (EX i <= n. f i = (k::int))";
-by (induct_tac "n" 1);
- by (Asm_simp_tac 1);
-by (strip_tac 1);
-by (etac impE 1);
- by (Asm_full_simp_tac 1);
-by (eres_inst_tac [("x","n")] allE 1);
-by (Asm_full_simp_tac 1);
-by (case_tac "k = f(n+1)" 1);
- by (Force_tac 1);
-by (etac impE 1);
- by (asm_full_simp_tac (simpset() addsimps [zabs_def]
- addsplits [split_if_asm]) 1);
-by (blast_tac (claset() addIs [le_SucI]) 1);
-val lemma = result();
-
-bind_thm("nat0_intermed_int_val", ObjectLogic.rulify_no_asm lemma);
-
-Goal "[| !i. m <= i & i < n --> abs(f(i + 1::nat) - f i) <= 1; m < n; \
-\ f m <= k; k <= f n |] ==> ? i. m <= i & i <= n & f i = (k::int)";
-by (cut_inst_tac [("n","n-m"),("f", "%i. f(i+m)"),("k","k")]lemma 1);
-by (Asm_full_simp_tac 1);
-by (etac impE 1);
- by (strip_tac 1);
- by (eres_inst_tac [("x","i+m")] allE 1);
- by (arith_tac 1);
-by (etac exE 1);
-by (res_inst_tac [("x","i+m")] exI 1);
-by (arith_tac 1);
-qed "nat_intermed_int_val";
-
-
-(*** Some convenient biconditionals for products of signs ***)
-
-Goal "[| (0::int) < i; 0 < j |] ==> 0 < i*j";
-by (dtac zmult_zless_mono1 1);
-by Auto_tac;
-qed "zmult_pos";
-
-Goal "[| i < (0::int); j < 0 |] ==> 0 < i*j";
-by (dtac zmult_zless_mono1_neg 1);
-by Auto_tac;
-qed "zmult_neg";
-
-Goal "[| (0::int) < i; j < 0 |] ==> i*j < 0";
-by (dtac zmult_zless_mono1_neg 1);
-by Auto_tac;
-qed "zmult_pos_neg";
-
-Goal "((0::int) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)";
-by (auto_tac (claset(),
- simpset() addsimps [order_le_less, linorder_not_less,
- zmult_pos, zmult_neg]));
-by (ALLGOALS (rtac ccontr));
-by (auto_tac (claset(),
- simpset() addsimps [order_le_less, linorder_not_less]));
-by (ALLGOALS (etac rev_mp));
-by (ALLGOALS (dtac zmult_pos_neg THEN' assume_tac));
-by (auto_tac (claset() addDs [order_less_not_sym],
- simpset() addsimps [zmult_commute]));
-qed "int_0_less_mult_iff";
-
-Goal "((0::int) <= x*y) = (0 <= x & 0 <= y | x <= 0 & y <= 0)";
-by (auto_tac (claset(),
- simpset() addsimps [order_le_less, linorder_not_less,
- int_0_less_mult_iff]));
-qed "int_0_le_mult_iff";
-
-Goal "(x*y < (0::int)) = (0 < x & y < 0 | x < 0 & 0 < y)";
-by (auto_tac (claset(),
- simpset() addsimps [int_0_le_mult_iff,
- linorder_not_le RS sym]));
-by (auto_tac (claset() addDs [order_less_not_sym],
- simpset() addsimps [linorder_not_le]));
-qed "zmult_less_0_iff";
-
-Goal "(x*y <= (0::int)) = (0 <= x & y <= 0 | x <= 0 & 0 <= y)";
-by (auto_tac (claset() addDs [order_less_not_sym],
- simpset() addsimps [int_0_less_mult_iff,
- linorder_not_less RS sym]));
-qed "zmult_le_0_iff";
-
-Goal "abs (x * y) = abs x * abs (y::int)";
-by (simp_tac (simpset () delsimps [thm "number_of_reorient"] addsplits [zabs_split]
- addsplits [zabs_split]
- addsimps [zmult_less_0_iff, zle_def]) 1);
-qed "abs_mult";
-
-Goal "(abs x = 0) = (x = (0::int))";
-by (simp_tac (simpset () addsplits [zabs_split]) 1);
-qed "abs_eq_0";
-AddIffs [abs_eq_0];
-
-Goal "(0 < abs x) = (x ~= (0::int))";
-by (simp_tac (simpset () addsplits [zabs_split]) 1);
-by (arith_tac 1);
-qed "zero_less_abs_iff";
-AddIffs [zero_less_abs_iff];
-
-Goal "0 <= x * (x::int)";
-by (subgoal_tac "(- x) * x <= 0" 1);
- by (Asm_full_simp_tac 1);
-by (simp_tac (HOL_basic_ss addsimps [zmult_le_0_iff]) 1);
-by Auto_tac;
-qed "square_nonzero";
-Addsimps [square_nonzero];
-AddIs [square_nonzero];
-
-
-(*** Products and 1, by T. M. Rasmussen ***)
-
-Goal "(m = m*(n::int)) = (n = 1 | m = 0)";
-by Auto_tac;
-by (subgoal_tac "m*1 = m*n" 1);
-by (dtac (zmult_cancel1 RS iffD1) 1);
-by Auto_tac;
-qed "zmult_eq_self_iff";
-
-Goal "[| 1 < m; 1 < n |] ==> 1 < m*(n::int)";
-by (res_inst_tac [("y","1*n")] order_less_trans 1);
-by (rtac zmult_zless_mono1 2);
-by (ALLGOALS Asm_simp_tac);
-qed "zless_1_zmult";
-
-Goal "[| 0 < n; n ~= 1 |] ==> 1 < (n::int)";
-by (arith_tac 1);
-val lemma = result();
-
-Goal "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)";
-by Auto_tac;
-by (case_tac "m=1" 1);
-by (case_tac "n=1" 2);
-by (case_tac "m=1" 4);
-by (case_tac "n=1" 5);
-by Auto_tac;
-by distinct_subgoals_tac;
-by (subgoal_tac "1<m*n" 1);
-by (Asm_full_simp_tac 1);
-by (rtac zless_1_zmult 1);
-by (ALLGOALS (rtac lemma));
-by Auto_tac;
-by (subgoal_tac "0<m*n" 1);
-by (Asm_simp_tac 2);
-by (dtac (int_0_less_mult_iff RS iffD1) 1);
-by Auto_tac;
-qed "pos_zmult_eq_1_iff";
-
-Goal "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))";
-by (case_tac "0<m" 1);
-by (asm_simp_tac (simpset() addsimps [pos_zmult_eq_1_iff]) 1);
-by (case_tac "m=0" 1);
-by (asm_simp_tac (simpset () delsimps [thm "number_of_reorient"]) 1);
-by (subgoal_tac "0 < -m" 1);
-by (arith_tac 2);
-by (dres_inst_tac [("n","-n")] pos_zmult_eq_1_iff 1);
-by Auto_tac;
-qed "zmult_eq_1_iff";
-
-
-(*** More about nat ***)
-
-Goal "[| (0::int) <= z; 0 <= z' |] ==> nat (z+z') = nat z + nat z'";
-by (rtac (inj_int RS injD) 1);
-by (asm_simp_tac (simpset() addsimps [zadd_int RS sym]) 1);
-qed "nat_add_distrib";
-
-Goal "[| (0::int) <= z'; z' <= z |] ==> nat (z-z') = nat z - nat z'";
-by (rtac (inj_int RS injD) 1);
-by (asm_simp_tac (simpset() addsimps [zdiff_int RS sym, nat_le_eq_zle]) 1);
-qed "nat_diff_distrib";
-
-Goal "(0::int) <= z ==> nat (z*z') = nat z * nat z'";
-by (case_tac "0 <= z'" 1);
-by (asm_full_simp_tac (simpset() addsimps [zmult_le_0_iff]) 2);
-by (rtac (inj_int RS injD) 1);
-by (asm_simp_tac (simpset() addsimps [zmult_int RS sym,
- int_0_le_mult_iff]) 1);
-qed "nat_mult_distrib";
-
-Goal "z <= (0::int) ==> nat(z*z') = nat(-z) * nat(-z')";
-by (rtac trans 1);
-by (rtac nat_mult_distrib 2);
-by Auto_tac;
-qed "nat_mult_distrib_neg";
-
-Goal "nat (abs (w * z)) = nat (abs w) * nat (abs z)";
-by (case_tac "z=0 | w=0" 1);
-by Auto_tac;
-by (simp_tac (simpset() addsimps [zabs_def, nat_mult_distrib RS sym,
- nat_mult_distrib_neg RS sym, zmult_less_0_iff]) 1);
-by (arith_tac 1);
-qed "nat_abs_mult_distrib";
--- a/src/HOL/Integ/IntArith.thy Tue Nov 18 09:45:45 2003 +0100
+++ b/src/HOL/Integ/IntArith.thy Tue Nov 18 11:01:52 2003 +0100
@@ -1,12 +1,87 @@
+(* Title: HOL/Integ/IntArith.thy
+ ID: $Id$
+ Authors: Larry Paulson and Tobias Nipkow
+*)
header {* Integer arithmetic *}
theory IntArith = Bin
-files ("int_arith1.ML") ("int_arith2.ML"):
+files ("int_arith1.ML"):
use "int_arith1.ML"
setup int_arith_setup
-use "int_arith2.ML"
+
+lemma zle_diff1_eq [simp]: "(w <= z - (1::int)) = (w<(z::int))"
+by arith
+
+lemma zle_add1_eq_le [simp]: "(w < z + 1) = (w<=(z::int))"
+by arith
+
+lemma zadd_left_cancel0 [simp]: "(z = z + w) = (w = (0::int))"
+by arith
+
+subsection{*Results about @{term nat}*}
+
+lemma nonneg_eq_int: "[| 0 <= z; !!m. z = int m ==> P |] ==> P"
+by (blast dest: nat_0_le sym)
+
+lemma nat_eq_iff: "(nat w = m) = (if 0 <= w then w = int m else m=0)"
+by auto
+
+lemma nat_eq_iff2: "(m = nat w) = (if 0 <= w then w = int m else m=0)"
+by auto
+
+lemma nat_less_iff: "0 <= w ==> (nat w < m) = (w < int m)"
+apply (rule iffI)
+apply (erule nat_0_le [THEN subst])
+apply (simp_all del: zless_int add: zless_int [symmetric])
+done
+
+lemma int_eq_iff: "(int m = z) = (m = nat z & 0 <= z)"
+by (auto simp add: nat_eq_iff2)
+
+
+(*Users don't want to see (int 0), int(Suc 0) or w + - z*)
+declare Zero_int_def [symmetric, simp]
+declare One_int_def [symmetric, simp]
+
+text{*cooper.ML refers to this theorem*}
+lemmas zdiff_def_symmetric = zdiff_def [symmetric, simp]
+
+lemma nat_0: "nat 0 = 0"
+by (simp add: nat_eq_iff)
+
+lemma nat_1: "nat 1 = Suc 0"
+by (subst nat_eq_iff, simp)
+
+lemma nat_2: "nat 2 = Suc (Suc 0)"
+by (subst nat_eq_iff, simp)
+
+lemma nat_less_eq_zless: "0 <= w ==> (nat w < nat z) = (w<z)"
+apply (case_tac "neg z")
+apply (auto simp add: nat_less_iff)
+apply (auto intro: zless_trans simp add: neg_eq_less_0 zle_def)
+done
+
+lemma nat_le_eq_zle: "0 < w | 0 <= z ==> (nat w <= nat z) = (w<=z)"
+by (auto simp add: linorder_not_less [symmetric] zless_nat_conj)
+
+subsection{*@{term abs}: Absolute Value, as an Integer*}
+
+(* Simpler: use zabs_def as rewrite rule
+ but arith_tac is not parameterized by such simp rules
+*)
+
+lemma zabs_split: "P(abs(i::int)) = ((0 <= i --> P i) & (i < 0 --> P(-i)))"
+by (simp add: zabs_def)
+
+lemma zero_le_zabs [iff]: "0 <= abs (z::int)"
+by (simp add: zabs_def)
+
+
+text{*This simplifies expressions of the form @{term "int n = z"} where
+ z is an integer literal.*}
+declare int_eq_iff [of _ "number_of v", standard, simp]
declare zabs_split [arith_split]
@@ -18,7 +93,7 @@
by simp
lemma split_nat[arith_split]:
- "P(nat(i::int)) = ((ALL n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
+ "P(nat(i::int)) = ((\<forall>n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))"
(is "?P = (?L & ?R)")
proof (cases "i < 0")
case True thus ?thesis by simp
@@ -69,8 +144,7 @@
apply(rule int_ge_induct[of "k + 1"])
using gr apply arith
apply(rule base)
-apply(rule step)
- apply simp+
+apply (rule step, simp+)
done
theorem int_le_induct[consumes 1,case_names base step]:
@@ -105,9 +179,216 @@
apply(rule int_le_induct[of _ "k - 1"])
using less apply arith
apply(rule base)
-apply(rule step)
- apply simp+
+apply (rule step, simp+)
+done
+
+subsection{*Simple Equations*}
+
+lemma int_diff_minus_eq [simp]: "x - - y = x + (y::int)"
+by simp
+
+lemma abs_abs [simp]: "abs(abs(x::int)) = abs(x)"
+by arith
+
+lemma abs_minus [simp]: "abs(-(x::int)) = abs(x)"
+by arith
+
+lemma triangle_ineq: "abs(x+y) <= abs(x) + abs(y::int)"
+by arith
+
+
+subsection{*Intermediate value theorems*}
+
+lemma int_val_lemma:
+ "(\<forall>i<n::nat. abs(f(i+1) - f i) \<le> 1) -->
+ f 0 \<le> k --> k \<le> f n --> (\<exists>i \<le> n. f i = (k::int))"
+apply (induct_tac "n")
+ apply (simp (no_asm_simp))
+apply (intro strip)
+apply (erule impE, simp)
+apply (erule_tac x = n in allE, simp)
+apply (case_tac "k = f (n+1) ")
+ apply force
+apply (erule impE)
+ apply (simp add: zabs_def split add: split_if_asm)
+apply (blast intro: le_SucI)
+done
+
+lemmas nat0_intermed_int_val = int_val_lemma [rule_format (no_asm)]
+
+lemma nat_intermed_int_val:
+ "[| \<forall>i. m \<le> i & i < n --> abs(f(i + 1::nat) - f i) \<le> 1; m < n;
+ f m \<le> k; k \<le> f n |] ==> ? i. m \<le> i & i \<le> n & f i = (k::int)"
+apply (cut_tac n = "n-m" and f = "%i. f (i+m) " and k = k
+ in int_val_lemma)
+apply simp
+apply (erule impE)
+ apply (intro strip)
+ apply (erule_tac x = "i+m" in allE, arith)
+apply (erule exE)
+apply (rule_tac x = "i+m" in exI, arith)
+done
+
+
+subsection{*Some convenient biconditionals for products of signs*}
+
+lemma zmult_pos: "[| (0::int) < i; 0 < j |] ==> 0 < i*j"
+by (drule zmult_zless_mono1, auto)
+
+lemma zmult_neg: "[| i < (0::int); j < 0 |] ==> 0 < i*j"
+by (drule zmult_zless_mono1_neg, auto)
+
+lemma zmult_pos_neg: "[| (0::int) < i; j < 0 |] ==> i*j < 0"
+by (drule zmult_zless_mono1_neg, auto)
+
+lemma int_0_less_mult_iff: "((0::int) < x*y) = (0 < x & 0 < y | x < 0 & y < 0)"
+apply (auto simp add: order_le_less linorder_not_less zmult_pos zmult_neg)
+apply (rule_tac [!] ccontr)
+apply (auto simp add: order_le_less linorder_not_less)
+apply (erule_tac [!] rev_mp)
+apply (drule_tac [!] zmult_pos_neg)
+apply (auto dest: order_less_not_sym simp add: zmult_commute)
+done
+
+lemma int_0_le_mult_iff: "((0::int) \<le> x*y) = (0 \<le> x & 0 \<le> y | x \<le> 0 & y \<le> 0)"
+by (auto simp add: order_le_less linorder_not_less int_0_less_mult_iff)
+
+lemma zmult_less_0_iff: "(x*y < (0::int)) = (0 < x & y < 0 | x < 0 & 0 < y)"
+by (auto simp add: int_0_le_mult_iff linorder_not_le [symmetric])
+
+lemma zmult_le_0_iff: "(x*y \<le> (0::int)) = (0 \<le> x & y \<le> 0 | x \<le> 0 & 0 \<le> y)"
+by (auto dest: order_less_not_sym simp add: int_0_less_mult_iff linorder_not_less [symmetric])
+
+lemma abs_mult: "abs (x * y) = abs x * abs (y::int)"
+by (simp del: number_of_reorient split
+ add: zabs_split split add: zabs_split add: zmult_less_0_iff zle_def)
+
+lemma abs_eq_0 [iff]: "(abs x = 0) = (x = (0::int))"
+by (simp split add: zabs_split)
+
+lemma zero_less_abs_iff [iff]: "(0 < abs x) = (x ~= (0::int))"
+by (simp split add: zabs_split, arith)
+
+(* THIS LOOKS WRONG: [intro]*)
+lemma square_nonzero [simp]: "0 \<le> x * (x::int)"
+apply (subgoal_tac " (- x) * x \<le> 0")
+ apply simp
+apply (simp only: zmult_le_0_iff, auto)
+done
+
+
+subsection{*Products and 1, by T. M. Rasmussen*}
+
+lemma zmult_eq_self_iff: "(m = m*(n::int)) = (n = 1 | m = 0)"
+apply auto
+apply (subgoal_tac "m*1 = m*n")
+apply (drule zmult_cancel1 [THEN iffD1], auto)
done
+lemma zless_1_zmult: "[| 1 < m; 1 < n |] ==> 1 < m*(n::int)"
+apply (rule_tac y = "1*n" in order_less_trans)
+apply (rule_tac [2] zmult_zless_mono1)
+apply (simp_all (no_asm_simp))
+done
+
+lemma pos_zmult_eq_1_iff: "0 < (m::int) ==> (m * n = 1) = (m = 1 & n = 1)"
+apply auto
+apply (case_tac "m=1")
+apply (case_tac [2] "n=1")
+apply (case_tac [4] "m=1")
+apply (case_tac [5] "n=1", auto)
+apply (tactic"distinct_subgoals_tac")
+apply (subgoal_tac "1<m*n", simp)
+apply (rule zless_1_zmult, arith)
+apply (subgoal_tac "0<n", arith)
+apply (subgoal_tac "0<m*n")
+apply (drule int_0_less_mult_iff [THEN iffD1], auto)
+done
+
+lemma zmult_eq_1_iff: "(m*n = (1::int)) = ((m = 1 & n = 1) | (m = -1 & n = -1))"
+apply (case_tac "0<m")
+apply (simp (no_asm_simp) add: pos_zmult_eq_1_iff)
+apply (case_tac "m=0")
+apply (simp (no_asm_simp) del: number_of_reorient)
+apply (subgoal_tac "0 < -m")
+apply (drule_tac n = "-n" in pos_zmult_eq_1_iff, auto)
+done
+
+
+subsection{*More about nat*}
+
+lemma nat_add_distrib:
+ "[| (0::int) \<le> z; 0 \<le> z' |] ==> nat (z+z') = nat z + nat z'"
+apply (rule inj_int [THEN injD])
+apply (simp (no_asm_simp) add: zadd_int [symmetric])
+done
+
+lemma nat_diff_distrib:
+ "[| (0::int) \<le> z'; z' \<le> z |] ==> nat (z-z') = nat z - nat z'"
+apply (rule inj_int [THEN injD])
+apply (simp (no_asm_simp) add: zdiff_int [symmetric] nat_le_eq_zle)
+done
+
+lemma nat_mult_distrib: "(0::int) \<le> z ==> nat (z*z') = nat z * nat z'"
+apply (case_tac "0 \<le> z'")
+apply (rule inj_int [THEN injD])
+apply (simp (no_asm_simp) add: zmult_int [symmetric] int_0_le_mult_iff)
+apply (simp add: zmult_le_0_iff)
+done
+
+lemma nat_mult_distrib_neg: "z \<le> (0::int) ==> nat(z*z') = nat(-z) * nat(-z')"
+apply (rule trans)
+apply (rule_tac [2] nat_mult_distrib, auto)
+done
+
+lemma nat_abs_mult_distrib: "nat (abs (w * z)) = nat (abs w) * nat (abs z)"
+apply (case_tac "z=0 | w=0")
+apply (auto simp add: zabs_def nat_mult_distrib [symmetric]
+ nat_mult_distrib_neg [symmetric] zmult_less_0_iff)
+done
+
+ML
+{*
+val zle_diff1_eq = thm "zle_diff1_eq";
+val zle_add1_eq_le = thm "zle_add1_eq_le";
+val nonneg_eq_int = thm "nonneg_eq_int";
+val nat_eq_iff = thm "nat_eq_iff";
+val nat_eq_iff2 = thm "nat_eq_iff2";
+val nat_less_iff = thm "nat_less_iff";
+val int_eq_iff = thm "int_eq_iff";
+val nat_0 = thm "nat_0";
+val nat_1 = thm "nat_1";
+val nat_2 = thm "nat_2";
+val nat_less_eq_zless = thm "nat_less_eq_zless";
+val nat_le_eq_zle = thm "nat_le_eq_zle";
+val zabs_split = thm "zabs_split";
+val zero_le_zabs = thm "zero_le_zabs";
+
+val int_diff_minus_eq = thm "int_diff_minus_eq";
+val abs_abs = thm "abs_abs";
+val abs_minus = thm "abs_minus";
+val triangle_ineq = thm "triangle_ineq";
+val nat_intermed_int_val = thm "nat_intermed_int_val";
+val zmult_pos = thm "zmult_pos";
+val zmult_neg = thm "zmult_neg";
+val zmult_pos_neg = thm "zmult_pos_neg";
+val int_0_less_mult_iff = thm "int_0_less_mult_iff";
+val int_0_le_mult_iff = thm "int_0_le_mult_iff";
+val zmult_less_0_iff = thm "zmult_less_0_iff";
+val zmult_le_0_iff = thm "zmult_le_0_iff";
+val abs_mult = thm "abs_mult";
+val abs_eq_0 = thm "abs_eq_0";
+val zero_less_abs_iff = thm "zero_less_abs_iff";
+val square_nonzero = thm "square_nonzero";
+val zmult_eq_self_iff = thm "zmult_eq_self_iff";
+val zless_1_zmult = thm "zless_1_zmult";
+val pos_zmult_eq_1_iff = thm "pos_zmult_eq_1_iff";
+val zmult_eq_1_iff = thm "zmult_eq_1_iff";
+val nat_add_distrib = thm "nat_add_distrib";
+val nat_diff_distrib = thm "nat_diff_distrib";
+val nat_mult_distrib = thm "nat_mult_distrib";
+val nat_mult_distrib_neg = thm "nat_mult_distrib_neg";
+val nat_abs_mult_distrib = thm "nat_abs_mult_distrib";
+*}
+
end
-
--- a/src/HOL/Integ/IntDef.ML Tue Nov 18 09:45:45 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,580 +0,0 @@
-(* Title: IntDef.ML
- ID: $Id$
- Authors: Lawrence C Paulson, Cambridge University Computer Laboratory
- Copyright 1993 University of Cambridge
-
-The integers as equivalence classes over nat*nat.
-*)
-
-
-Goalw [intrel_def] "(((x1,y1),(x2,y2)): intrel) = (x1+y2 = x2+y1)";
-by (Blast_tac 1);
-qed "intrel_iff";
-
-Goalw [intrel_def, equiv_def, refl_def, sym_def, trans_def]
- "equiv UNIV intrel";
-by Auto_tac;
-qed "equiv_intrel";
-
-bind_thm ("equiv_intrel_iff",
- [equiv_intrel, UNIV_I, UNIV_I] MRS eq_equiv_class_iff);
-
-Goalw [Integ_def,intrel_def,quotient_def]
- "intrel``{(x,y)}:Integ";
-by (Fast_tac 1);
-qed "intrel_in_integ";
-
-Goal "inj_on Abs_Integ Integ";
-by (rtac inj_on_inverseI 1);
-by (etac Abs_Integ_inverse 1);
-qed "inj_on_Abs_Integ";
-
-Addsimps [equiv_intrel_iff, inj_on_Abs_Integ RS inj_on_iff,
- intrel_iff, intrel_in_integ, Abs_Integ_inverse];
-
-Goal "inj(Rep_Integ)";
-by (rtac inj_inverseI 1);
-by (rtac Rep_Integ_inverse 1);
-qed "inj_Rep_Integ";
-
-
-(** int: the injection from "nat" to "int" **)
-
-Goal "inj int";
-by (rtac injI 1);
-by (rewtac int_def);
-by (dtac (inj_on_Abs_Integ RS inj_onD) 1);
-by (REPEAT (rtac intrel_in_integ 1));
-by (dtac eq_equiv_class 1);
-by (rtac equiv_intrel 1);
-by (Fast_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [intrel_def]) 1);
-qed "inj_int";
-
-
-(**** zminus: unary negation on Integ ****)
-
-Goalw [congruent_def, intrel_def]
- "congruent intrel (%(x,y). intrel``{(y,x)})";
-by (auto_tac (claset(), simpset() addsimps add_ac));
-qed "zminus_congruent";
-
-Goalw [zminus_def]
- "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})";
-by (simp_tac (simpset() addsimps
- [equiv_intrel RS UN_equiv_class, zminus_congruent]) 1);
-qed "zminus";
-
-(*Every integer can be written in the form Abs_Integ(...) *)
-val [prem] = Goal "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P";
-by (res_inst_tac [("x1","z")]
- (rewrite_rule [Integ_def] Rep_Integ RS quotientE) 1);
-by (dres_inst_tac [("f","Abs_Integ")] arg_cong 1);
-by (res_inst_tac [("p","x")] PairE 1);
-by (rtac prem 1);
-by (asm_full_simp_tac (simpset() addsimps [Rep_Integ_inverse]) 1);
-qed "eq_Abs_Integ";
-
-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(%z::int. -z)";
-by (rtac injI 1);
-by (dres_inst_tac [("f","uminus")] arg_cong 1);
-by (Asm_full_simp_tac 1);
-qed "inj_zminus";
-
-Goalw [int_def, Zero_int_def] "- 0 = (0::int)";
-by (simp_tac (simpset() addsimps [zminus]) 1);
-qed "zminus_0";
-Addsimps [zminus_0];
-
-
-(**** neg: the test for negative integers ****)
-
-
-Goalw [neg_def, int_def] "~ neg(int n)";
-by (Simp_tac 1);
-qed "not_neg_int";
-
-Goalw [neg_def, int_def] "neg(- (int (Suc n)))";
-by (simp_tac (simpset() addsimps [zminus]) 1);
-qed "neg_zminus_int";
-
-Addsimps [neg_zminus_int, not_neg_int];
-
-
-(**** zadd: addition on Integ ****)
-
-Goalw [zadd_def]
- "Abs_Integ(intrel``{(x1,y1)}) + Abs_Integ(intrel``{(x2,y2)}) = \
-\ Abs_Integ(intrel``{(x1+x2, y1+y2)})";
-by (asm_simp_tac (simpset() addsimps [UN_UN_split_split_eq]) 1);
-by (stac (equiv_intrel RS UN_equiv_class2) 1);
-by (auto_tac (claset(), simpset() addsimps [congruent2_def]));
-qed "zadd";
-
-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);
-by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps add_ac @ [zadd]) 1);
-qed "zadd_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 [zadd, add_assoc]) 1);
-qed "zadd_assoc";
-
-(*For AC rewriting*)
-Goal "(x::int)+(y+z)=y+(x+z)";
-by(rtac ([zadd_assoc,zadd_commute] MRS
- read_instantiate[("f","op +")](thm"mk_left_commute")) 1);
-qed "zadd_left_commute";
-
-(*Integer addition is an AC operator*)
-bind_thms ("zadd_ac", [zadd_assoc,zadd_commute,zadd_left_commute]);
-
-Goalw [int_def] "(int m) + (int n) = int (m + n)";
-by (simp_tac (simpset() addsimps [zadd]) 1);
-qed "zadd_int";
-
-Goal "(int m) + (int n + z) = int (m + n) + z";
-by (simp_tac (simpset() addsimps [zadd_int, zadd_assoc RS sym]) 1);
-qed "zadd_int_left";
-
-Goal "int (Suc m) = 1 + (int m)";
-by (simp_tac (simpset() addsimps [One_int_def, zadd_int]) 1);
-qed "int_Suc";
-
-(*also for the instance declaration int :: plus_ac0*)
-Goalw [Zero_int_def, int_def] "(0::int) + z = z";
-by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps [zadd]) 1);
-qed "zadd_0";
-Addsimps [zadd_0];
-
-Goal "z + (0::int) = z";
-by (rtac ([zadd_commute, zadd_0] MRS trans) 1);
-qed "zadd_0_right";
-Addsimps [zadd_0_right];
-
-Goalw [int_def, Zero_int_def] "z + (- z) = (0::int)";
-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";
-
-Goal "(- z) + z = (0::int)";
-by (rtac (zadd_commute RS trans) 1);
-by (rtac zadd_zminus_inverse 1);
-qed "zadd_zminus_inverse2";
-
-Addsimps [zadd_zminus_inverse, zadd_zminus_inverse2];
-
-Goal "z + (- z + w) = (w::int)";
-by (simp_tac (simpset() addsimps [zadd_assoc RS sym, zadd_0]) 1);
-qed "zadd_zminus_cancel";
-
-Goal "(-z) + (z + w) = (w::int)";
-by (simp_tac (simpset() addsimps [zadd_assoc RS sym, zadd_0]) 1);
-qed "zminus_zadd_cancel";
-
-Addsimps [zadd_zminus_cancel, zminus_zadd_cancel];
-
-Goal "(0::int) - x = -x";
-by (simp_tac (simpset() addsimps [zdiff_def]) 1);
-qed "zdiff0";
-
-Goal "x - (0::int) = x";
-by (simp_tac (simpset() addsimps [zdiff_def]) 1);
-qed "zdiff0_right";
-
-Goal "x - x = (0::int)";
-by (simp_tac (simpset() addsimps [zdiff_def, Zero_int_def]) 1);
-qed "zdiff_self";
-
-Addsimps [zdiff0, zdiff0_right, zdiff_self];
-
-
-(** Lemmas **)
-
-Goal "(z::int) + v = z' + v' ==> z + (v + w) = z' + (v' + w)";
-by (asm_simp_tac (simpset() addsimps [zadd_assoc RS sym]) 1);
-qed "zadd_assoc_cong";
-
-Goal "(z::int) + (v + w) = v + (z + w)";
-by (REPEAT (ares_tac [zadd_commute RS zadd_assoc_cong] 1));
-qed "zadd_assoc_swap";
-
-
-(**** zmult: multiplication on Integ ****)
-
-(*Congruence property for multiplication*)
-Goal "congruent2 intrel \
-\ (%p1 p2. (%(x1,y1). (%(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 (ALLGOALS Clarify_tac);
-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 (rename_tac "x1 x2 y1 y2 z1 z2" 1);
-by (rtac ([equiv_intrel, intrel_iff RS iffD2] MRS equiv_class_eq) 1);
-by (asm_full_simp_tac (simpset() addsimps [intrel_def]) 1);
-by (subgoal_tac
- "x1*z1 + y2*z1 = y1*z1 + x2*z1 & x1*z2 + y2*z2 = y1*z2 + x2*z2" 1);
-by (asm_simp_tac (simpset() addsimps [add_mult_distrib RS sym]) 2);
-by (arith_tac 1);
-qed "zmult_congruent2";
-
-Goalw [zmult_def]
- "Abs_Integ((intrel``{(x1,y1)})) * Abs_Integ((intrel``{(x2,y2)})) = \
-\ Abs_Integ(intrel `` {(x1*x2 + y1*y2, x1*y2 + y1*x2)})";
-by (asm_simp_tac
- (simpset() addsimps [UN_UN_split_split_eq, zmult_congruent2,
- equiv_intrel RS UN_equiv_class2]) 1);
-qed "zmult";
-
-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::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);
-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);
-qed "zmult_assoc";
-
-(*For AC rewriting*)
-Goal "(z1::int)*(z2*z3) = z2*(z1*z3)";
-by(rtac ([zmult_assoc,zmult_commute] MRS
- read_instantiate[("f","op *")](thm"mk_left_commute")) 1);
-qed "zmult_left_commute";
-
-(*Integer multiplication is an AC operator*)
-bind_thms ("zmult_ac", [zmult_assoc, zmult_commute, zmult_left_commute]);
-
-Goal "((z1::int) + z2) * w = (z1 * w) + (z2 * w)";
-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","w")] eq_Abs_Integ 1);
-by (asm_simp_tac
- (simpset() addsimps [add_mult_distrib2, zadd, zmult] @
- add_ac @ mult_ac) 1);
-qed "zadd_zmult_distrib";
-
-val zmult_commute'= inst "z" "w" zmult_commute;
-
-Goal "w * (- z) = - (w * (z::int))";
-by (simp_tac (simpset() addsimps [zmult_commute', zmult_zminus]) 1);
-qed "zmult_zminus_right";
-
-Goal "(w::int) * (z1 + z2) = (w * z1) + (w * z2)";
-by (simp_tac (simpset() addsimps [zmult_commute',zadd_zmult_distrib]) 1);
-qed "zadd_zmult_distrib2";
-
-Goalw [zdiff_def] "((z1::int) - z2) * w = (z1 * w) - (z2 * w)";
-by (stac zadd_zmult_distrib 1);
-by (simp_tac (simpset() addsimps [zmult_zminus]) 1);
-qed "zdiff_zmult_distrib";
-
-Goal "(w::int) * (z1 - z2) = (w * z1) - (w * z2)";
-by (simp_tac (simpset() addsimps [zmult_commute',zdiff_zmult_distrib]) 1);
-qed "zdiff_zmult_distrib2";
-
-bind_thms ("int_distrib",
- [zadd_zmult_distrib, zadd_zmult_distrib2, zdiff_zmult_distrib, zdiff_zmult_distrib2]);
-
-Goalw [int_def] "(int m) * (int n) = int (m * n)";
-by (simp_tac (simpset() addsimps [zmult]) 1);
-qed "zmult_int";
-
-Goalw [Zero_int_def, int_def] "0 * z = (0::int)";
-by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps [zmult]) 1);
-qed "zmult_0";
-Addsimps [zmult_0];
-
-Goalw [One_int_def, int_def] "(1::int) * z = z";
-by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by (asm_simp_tac (simpset() addsimps [zmult]) 1);
-qed "zmult_1";
-Addsimps [zmult_1];
-
-Goal "z * 0 = (0::int)";
-by (rtac ([zmult_commute, zmult_0] MRS trans) 1);
-qed "zmult_0_right";
-Addsimps [zmult_0_right];
-
-Goal "z * (1::int) = z";
-by (rtac ([zmult_commute, zmult_1] MRS trans) 1);
-qed "zmult_1_right";
-Addsimps [zmult_1_right];
-
-
-(* Theorems about less and less_equal *)
-
-(*This lemma allows direct proofs of other <-properties*)
-Goalw [zless_def, neg_def, zdiff_def, int_def]
- "(w < z) = (EX n. z = w + int(Suc n))";
-by (res_inst_tac [("z","z")] eq_Abs_Integ 1);
-by (res_inst_tac [("z","w")] eq_Abs_Integ 1);
-by (Clarify_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [zadd, zminus]) 1);
-by (safe_tac (claset() addSDs [less_imp_Suc_add]));
-by (res_inst_tac [("x","k")] exI 1);
-by (ALLGOALS (asm_full_simp_tac (simpset() addsimps add_ac)));
-qed "zless_iff_Suc_zadd";
-
-Goal "z < z + int (Suc n)";
-by (auto_tac (claset(),
- simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc,
- zadd_int]));
-qed "zless_zadd_Suc";
-
-Goal "[| z1<z2; z2<z3 |] ==> z1 < (z3::int)";
-by (auto_tac (claset(),
- simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc,
- zadd_int]));
-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 [int_def, zadd]) 1);
-qed "zless_not_sym";
-
-(* [| n<m; ~P ==> m<n |] ==> P *)
-bind_thm ("zless_asym", zless_not_sym RS swap);
-
-Goal "!!z::int. ~ z<z";
-by (resolve_tac [zless_asym RS notI] 1);
-by (REPEAT (assume_tac 1));
-qed "zless_not_refl";
-
-(* z<z ==> R *)
-bind_thm ("zless_irrefl", zless_not_refl RS notE);
-AddSEs [zless_irrefl];
-
-
-(*"Less than" is a linear ordering*)
-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);
-by Safe_tac;
-by (asm_full_simp_tac
- (simpset() addsimps [zadd, zminus, Image_iff, Bex_def]) 1);
-by (res_inst_tac [("m1", "x+ya"), ("n1", "xa+y")] (less_linear RS disjE) 1);
-by (ALLGOALS (force_tac (claset(), simpset() addsimps add_ac)));
-qed "zless_linear";
-
-Goal "!!w::int. (w ~= z) = (w<z | z<w)";
-by (cut_facts_tac [zless_linear] 1);
-by (Blast_tac 1);
-qed "int_neq_iff";
-
-(*** eliminates ~= in premises ***)
-bind_thm("int_neqE", int_neq_iff RS iffD1 RS disjE);
-
-Goal "(int m = int n) = (m = n)";
-by (fast_tac (claset() addSEs [inj_int RS injD]) 1);
-qed "int_int_eq";
-AddIffs [int_int_eq];
-
-Goal "(int n = 0) = (n = 0)";
-by (simp_tac (simpset() addsimps [Zero_int_def]) 1);
-qed "int_eq_0_conv";
-Addsimps [int_eq_0_conv];
-
-Goal "(int m < int n) = (m<n)";
-by (simp_tac (simpset() addsimps [less_iff_Suc_add, zless_iff_Suc_zadd,
- zadd_int]) 1);
-qed "zless_int";
-Addsimps [zless_int];
-
-Goal "~ (int k < 0)";
-by (simp_tac (simpset() addsimps [Zero_int_def]) 1);
-qed "int_less_0_conv";
-Addsimps [int_less_0_conv];
-
-Goal "(0 < int n) = (0 < n)";
-by (simp_tac (simpset() addsimps [Zero_int_def]) 1);
-qed "zero_less_int_conv";
-Addsimps [zero_less_int_conv];
-
-
-(*** Properties of <= ***)
-
-Goalw [zle_def, le_def] "(int m <= int n) = (m<=n)";
-by (Simp_tac 1);
-qed "zle_int";
-Addsimps [zle_int];
-
-Goal "(0 <= int n)";
-by (simp_tac (simpset() addsimps [Zero_int_def]) 1);
-qed "zero_zle_int";
-Addsimps [zero_zle_int];
-
-Goal "(int n <= 0) = (n = 0)";
-by (simp_tac (simpset() addsimps [Zero_int_def]) 1);
-qed "int_le_0_conv";
-Addsimps [int_le_0_conv];
-
-Goalw [zle_def] "z <= w ==> z < w | z=(w::int)";
-by (cut_facts_tac [zless_linear] 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)";
-by (cut_facts_tac [zless_linear] 1);
-by (blast_tac (claset() addEs [zless_asym]) 1);
-qed "zless_or_eq_imp_zle";
-
-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 "int_le_less";
-
-Goal "w <= (w::int)";
-by (simp_tac (simpset() addsimps [int_le_less]) 1);
-qed "zle_refl";
-
-(* Axiom 'linorder_linear' of class 'linorder': *)
-Goal "(z::int) <= w | w <= z";
-by (simp_tac (simpset() addsimps [int_le_less]) 1);
-by (cut_facts_tac [zless_linear] 1);
-by (Blast_tac 1);
-qed "zle_linear";
-
-(* Axiom 'order_trans of class 'order': *)
-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,
- blast_tac (claset() addIs [zless_trans])]);
-qed "zle_trans";
-
-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_asym])]);
-qed "zle_anti_sym";
-
-(* Axiom 'order_less_le' of class 'order': *)
-Goal "((w::int) < z) = (w <= z & w ~= z)";
-by (simp_tac (simpset() addsimps [zle_def, int_neq_iff]) 1);
-by (blast_tac (claset() addSEs [zless_asym]) 1);
-qed "int_less_le";
-
-
-(*** 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, symmetric Zero_int_def]));
-qed "zdiff_eq_eq";
-
-Goalw [zdiff_def] "(x = z-y) = (x + (y::int) = z)";
-by (auto_tac (claset(),
- simpset() addsimps [zadd_assoc, symmetric Zero_int_def]));
-qed "eq_zdiff_eq";
-
-(*This list of rewrites simplifies (in)equalities by bringing subtractions
- to the top and then moving negative terms to the other side.
- Use with zadd_ac*)
-bind_thms ("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]);
-
-
-(** Cancellation laws **)
-
-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 symmetric Zero_int_def ::
- 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];
-
-
-(** For the cancellation simproc.
- The idea is to cancel like terms on opposite sides by subtraction **)
-
-Goal "(x::int) - y = x' - y' ==> (x<y) = (x'<y')";
-by (asm_simp_tac (simpset() addsimps [zless_def]) 1);
-qed "zless_eqI";
-
-Goal "(x::int) - y = x' - y' ==> (y<=x) = (y'<=x')";
-by (dtac zless_eqI 1);
-by (asm_simp_tac (simpset() addsimps [zle_def]) 1);
-qed "zle_eqI";
-
-Goal "(x::int) - y = x' - y' ==> (x=y) = (x'=y')";
-by Safe_tac;
-by (ALLGOALS
- (asm_full_simp_tac (simpset() addsimps [eq_zdiff_eq, zdiff_eq_eq])));
-qed "zeq_eqI";
-
--- a/src/HOL/Integ/IntDef.thy Tue Nov 18 09:45:45 2003 +0100
+++ b/src/HOL/Integ/IntDef.thy Tue Nov 18 11:01:52 2003 +0100
@@ -6,52 +6,652 @@
The integers as equivalence classes over nat*nat.
*)
-IntDef = Equiv + NatArith +
+theory IntDef = Equiv + NatArith:
constdefs
intrel :: "((nat * nat) * (nat * nat)) set"
"intrel == {p. EX x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
typedef (Integ)
- int = "UNIV//intrel" (quotient_def)
+ int = "UNIV//intrel"
+ by (auto simp add: quotient_def)
-instance
- int :: {ord, zero, one, plus, times, minus}
+instance int :: ord ..
+instance int :: zero ..
+instance int :: one ..
+instance int :: plus ..
+instance int :: times ..
+instance int :: minus ..
defs
- zminus_def
+ zminus_def:
"- Z == Abs_Integ(UN (x,y):Rep_Integ(Z). intrel``{(y,x)})"
constdefs
- int :: nat => int
+ int :: "nat => int"
"int m == Abs_Integ(intrel `` {(m,0)})"
- neg :: int => bool
+ neg :: "int => bool"
"neg(Z) == EX x y. x<y & (x,y::nat):Rep_Integ(Z)"
(*For simplifying equalities*)
- iszero :: int => bool
+ iszero :: "int => bool"
"iszero z == z = (0::int)"
defs (*of overloaded constants*)
- Zero_int_def "0 == int 0"
- One_int_def "1 == int 1"
+ Zero_int_def: "0 == int 0"
+ One_int_def: "1 == int 1"
- zadd_def
+ zadd_def:
"z + w ==
Abs_Integ(UN (x1,y1):Rep_Integ(z). UN (x2,y2):Rep_Integ(w).
intrel``{(x1+x2, y1+y2)})"
- zdiff_def "z - (w::int) == z + (-w)"
+ zdiff_def: "z - (w::int) == z + (-w)"
- zless_def "z<w == neg(z - w)"
+ zless_def: "z<w == neg(z - w)"
- zle_def "z <= (w::int) == ~(w < z)"
+ zle_def: "z <= (w::int) == ~(w < z)"
- zmult_def
+ zmult_def:
"z * w ==
Abs_Integ(UN (x1,y1):Rep_Integ(z). UN (x2,y2):Rep_Integ(w).
intrel``{(x1*x2 + y1*y2, x1*y2 + y1*x2)})"
+lemma intrel_iff [simp]: "(((x1,y1),(x2,y2)): intrel) = (x1+y2 = x2+y1)"
+by (unfold intrel_def, blast)
+
+lemma equiv_intrel: "equiv UNIV intrel"
+by (unfold intrel_def equiv_def refl_def sym_def trans_def, auto)
+
+lemmas equiv_intrel_iff =
+ eq_equiv_class_iff [OF equiv_intrel UNIV_I UNIV_I, simp]
+
+lemma intrel_in_integ [simp]: "intrel``{(x,y)}:Integ"
+by (unfold Integ_def intrel_def quotient_def, fast)
+
+lemma inj_on_Abs_Integ: "inj_on Abs_Integ Integ"
+apply (rule inj_on_inverseI)
+apply (erule Abs_Integ_inverse)
+done
+
+declare inj_on_Abs_Integ [THEN inj_on_iff, simp]
+ Abs_Integ_inverse [simp]
+
+lemma inj_Rep_Integ: "inj(Rep_Integ)"
+apply (rule inj_on_inverseI)
+apply (rule Rep_Integ_inverse)
+done
+
+
+(** int: the injection from "nat" to "int" **)
+
+lemma inj_int: "inj int"
+apply (rule inj_onI)
+apply (unfold int_def)
+apply (drule inj_on_Abs_Integ [THEN inj_onD])
+apply (rule intrel_in_integ)+
+apply (drule eq_equiv_class)
+apply (rule equiv_intrel, fast)
+apply (simp add: intrel_def)
+done
+
+
+subsection{*zminus: unary negation on Integ*}
+
+lemma zminus_congruent: "congruent intrel (%(x,y). intrel``{(y,x)})"
+apply (unfold congruent_def intrel_def)
+apply (auto simp add: add_ac)
+done
+
+lemma zminus: "- Abs_Integ(intrel``{(x,y)}) = Abs_Integ(intrel `` {(y,x)})"
+by (simp add: zminus_def equiv_intrel [THEN UN_equiv_class] zminus_congruent)
+
+(*Every integer can be written in the form Abs_Integ(...) *)
+lemma eq_Abs_Integ:
+ "(!!x y. z = Abs_Integ(intrel``{(x,y)}) ==> P) ==> P"
+apply (rule_tac x1=z in Rep_Integ [unfolded Integ_def, THEN quotientE])
+apply (drule_tac f = Abs_Integ in arg_cong)
+apply (rule_tac p = x in PairE)
+apply (simp add: Rep_Integ_inverse)
+done
+
+lemma zminus_zminus [simp]: "- (- z) = (z::int)"
+apply (rule_tac z = z in eq_Abs_Integ)
+apply (simp (no_asm_simp) add: zminus)
+done
+
+lemma inj_zminus: "inj(%z::int. -z)"
+apply (rule inj_onI)
+apply (drule_tac f = uminus in arg_cong, simp)
+done
+
+lemma zminus_0 [simp]: "- 0 = (0::int)"
+by (simp add: int_def Zero_int_def zminus)
+
+
+subsection{*neg: the test for negative integers*}
+
+
+lemma not_neg_int [simp]: "~ neg(int n)"
+by (simp add: neg_def int_def)
+
+lemma neg_zminus_int [simp]: "neg(- (int (Suc n)))"
+by (simp add: neg_def int_def zminus)
+
+
+subsection{*zadd: addition on Integ*}
+
+lemma zadd:
+ "Abs_Integ(intrel``{(x1,y1)}) + Abs_Integ(intrel``{(x2,y2)}) =
+ Abs_Integ(intrel``{(x1+x2, y1+y2)})"
+apply (simp add: zadd_def UN_UN_split_split_eq)
+apply (subst equiv_intrel [THEN UN_equiv_class2])
+apply (auto simp add: congruent2_def)
+done
+
+lemma zminus_zadd_distrib [simp]: "- (z + w) = (- z) + (- w::int)"
+apply (rule_tac z = z in eq_Abs_Integ)
+apply (rule_tac z = w in eq_Abs_Integ)
+apply (simp (no_asm_simp) add: zminus zadd)
+done
+
+lemma zadd_commute: "(z::int) + w = w + z"
+apply (rule_tac z = z in eq_Abs_Integ)
+apply (rule_tac z = w in eq_Abs_Integ)
+apply (simp (no_asm_simp) add: add_ac zadd)
+done
+
+lemma zadd_assoc: "((z1::int) + z2) + z3 = z1 + (z2 + z3)"
+apply (rule_tac z = z1 in eq_Abs_Integ)
+apply (rule_tac z = z2 in eq_Abs_Integ)
+apply (rule_tac z = z3 in eq_Abs_Integ)
+apply (simp (no_asm_simp) add: zadd add_assoc)
+done
+
+(*For AC rewriting*)
+lemma zadd_left_commute: "x + (y + z) = y + ((x + z)::int)"
+ apply (rule mk_left_commute [of "op +"])
+ apply (rule zadd_assoc)
+ apply (rule zadd_commute)
+ done
+
+(*Integer addition is an AC operator*)
+lemmas zadd_ac = zadd_assoc zadd_commute zadd_left_commute
+
+lemma zadd_int: "(int m) + (int n) = int (m + n)"
+by (simp add: int_def zadd)
+
+lemma zadd_int_left: "(int m) + (int n + z) = int (m + n) + z"
+by (simp add: zadd_int zadd_assoc [symmetric])
+
+lemma int_Suc: "int (Suc m) = 1 + (int m)"
+by (simp add: One_int_def zadd_int)
+
+(*also for the instance declaration int :: plus_ac0*)
+lemma zadd_0 [simp]: "(0::int) + z = z"
+apply (unfold Zero_int_def int_def)
+apply (rule_tac z = z in eq_Abs_Integ)
+apply (simp (no_asm_simp) add: zadd)
+done
+
+lemma zadd_0_right [simp]: "z + (0::int) = z"
+by (rule trans [OF zadd_commute zadd_0])
+
+lemma zadd_zminus_inverse [simp]: "z + (- z) = (0::int)"
+apply (unfold int_def Zero_int_def)
+apply (rule_tac z = z in eq_Abs_Integ)
+apply (simp (no_asm_simp) add: zminus zadd add_commute)
+done
+
+lemma zadd_zminus_inverse2 [simp]: "(- z) + z = (0::int)"
+apply (rule zadd_commute [THEN trans])
+apply (rule zadd_zminus_inverse)
+done
+
+lemma zadd_zminus_cancel [simp]: "z + (- z + w) = (w::int)"
+by (simp add: zadd_assoc [symmetric] zadd_0)
+
+lemma zminus_zadd_cancel [simp]: "(-z) + (z + w) = (w::int)"
+by (simp add: zadd_assoc [symmetric] zadd_0)
+
+lemma zdiff0 [simp]: "(0::int) - x = -x"
+by (simp add: zdiff_def)
+
+lemma zdiff0_right [simp]: "x - (0::int) = x"
+by (simp add: zdiff_def)
+
+lemma zdiff_self [simp]: "x - x = (0::int)"
+by (simp add: zdiff_def Zero_int_def)
+
+
+(** Lemmas **)
+
+lemma zadd_assoc_cong: "(z::int) + v = z' + v' ==> z + (v + w) = z' + (v' + w)"
+by (simp add: zadd_assoc [symmetric])
+
+lemma zadd_assoc_swap: "(z::int) + (v + w) = v + (z + w)"
+by (rule zadd_commute [THEN zadd_assoc_cong])
+
+
+subsection{*zmult: multiplication on Integ*}
+
+(*Congruence property for multiplication*)
+lemma zmult_congruent2: "congruent2 intrel
+ (%p1 p2. (%(x1,y1). (%(x2,y2).
+ intrel``{(x1*x2 + y1*y2, x1*y2 + y1*x2)}) p2) p1)"
+apply (rule equiv_intrel [THEN congruent2_commuteI])
+apply (rule_tac [2] p=w in PairE)
+apply (force simp add: add_ac mult_ac, clarify)
+apply (simp (no_asm_simp) del: equiv_intrel_iff add: add_ac mult_ac)
+apply (rename_tac x1 x2 y1 y2 z1 z2)
+apply (rule equiv_class_eq [OF equiv_intrel intrel_iff [THEN iffD2]])
+apply (simp add: intrel_def)
+apply (subgoal_tac "x1*z1 + y2*z1 = y1*z1 + x2*z1 & x1*z2 + y2*z2 = y1*z2 + x2*z2", arith)
+apply (simp add: add_mult_distrib [symmetric])
+done
+
+lemma zmult:
+ "Abs_Integ((intrel``{(x1,y1)})) * Abs_Integ((intrel``{(x2,y2)})) =
+ Abs_Integ(intrel `` {(x1*x2 + y1*y2, x1*y2 + y1*x2)})"
+apply (unfold zmult_def)
+apply (simp (no_asm_simp) add: UN_UN_split_split_eq zmult_congruent2 equiv_intrel [THEN UN_equiv_class2])
+done
+
+lemma zmult_zminus: "(- z) * w = - (z * (w::int))"
+apply (rule_tac z = z in eq_Abs_Integ)
+apply (rule_tac z = w in eq_Abs_Integ)
+apply (simp (no_asm_simp) add: zminus zmult add_ac)
+done
+
+lemma zmult_commute: "(z::int) * w = w * z"
+apply (rule_tac z = z in eq_Abs_Integ)
+apply (rule_tac z = w in eq_Abs_Integ)
+apply (simp (no_asm_simp) add: zmult add_ac mult_ac)
+done
+
+lemma zmult_assoc: "((z1::int) * z2) * z3 = z1 * (z2 * z3)"
+apply (rule_tac z = z1 in eq_Abs_Integ)
+apply (rule_tac z = z2 in eq_Abs_Integ)
+apply (rule_tac z = z3 in eq_Abs_Integ)
+apply (simp (no_asm_simp) add: add_mult_distrib2 zmult add_ac mult_ac)
+done
+
+(*For AC rewriting*)
+lemma zmult_left_commute: "x * (y * z) = y * ((x * z)::int)"
+ apply (rule mk_left_commute [of "op *"])
+ apply (rule zmult_assoc)
+ apply (rule zmult_commute)
+ done
+
+(*Integer multiplication is an AC operator*)
+lemmas zmult_ac = zmult_assoc zmult_commute zmult_left_commute
+
+lemma zadd_zmult_distrib: "((z1::int) + z2) * w = (z1 * w) + (z2 * w)"
+apply (rule_tac z = z1 in eq_Abs_Integ)
+apply (rule_tac z = z2 in eq_Abs_Integ)
+apply (rule_tac z = w in eq_Abs_Integ)
+apply (simp add: add_mult_distrib2 zadd zmult add_ac mult_ac)
+done
+
+lemma zmult_zminus_right: "w * (- z) = - (w * (z::int))"
+by (simp add: zmult_commute [of w] zmult_zminus)
+
+lemma zadd_zmult_distrib2: "(w::int) * (z1 + z2) = (w * z1) + (w * z2)"
+by (simp add: zmult_commute [of w] zadd_zmult_distrib)
+
+lemma zdiff_zmult_distrib: "((z1::int) - z2) * w = (z1 * w) - (z2 * w)"
+apply (unfold zdiff_def)
+apply (subst zadd_zmult_distrib)
+apply (simp add: zmult_zminus)
+done
+
+lemma zdiff_zmult_distrib2: "(w::int) * (z1 - z2) = (w * z1) - (w * z2)"
+by (simp add: zmult_commute [of w] zdiff_zmult_distrib)
+
+lemmas int_distrib =
+ zadd_zmult_distrib zadd_zmult_distrib2
+ zdiff_zmult_distrib zdiff_zmult_distrib2
+
+lemma zmult_int: "(int m) * (int n) = int (m * n)"
+by (simp add: int_def zmult)
+
+lemma zmult_0 [simp]: "0 * z = (0::int)"
+apply (unfold Zero_int_def int_def)
+apply (rule_tac z = z in eq_Abs_Integ)
+apply (simp (no_asm_simp) add: zmult)
+done
+
+lemma zmult_1 [simp]: "(1::int) * z = z"
+apply (unfold One_int_def int_def)
+apply (rule_tac z = z in eq_Abs_Integ)
+apply (simp (no_asm_simp) add: zmult)
+done
+
+lemma zmult_0_right [simp]: "z * 0 = (0::int)"
+by (rule trans [OF zmult_commute zmult_0])
+
+lemma zmult_1_right [simp]: "z * (1::int) = z"
+by (rule trans [OF zmult_commute zmult_1])
+
+
+(* Theorems about less and less_equal *)
+
+(*This lemma allows direct proofs of other <-properties*)
+lemma zless_iff_Suc_zadd:
+ "(w < z) = (EX n. z = w + int(Suc n))"
+apply (unfold zless_def neg_def zdiff_def int_def)
+apply (rule_tac z = z in eq_Abs_Integ)
+apply (rule_tac z = w in eq_Abs_Integ, clarify)
+apply (simp add: zadd zminus)
+apply (safe dest!: less_imp_Suc_add)
+apply (rule_tac x = k in exI)
+apply (simp_all add: add_ac)
+done
+
+lemma zless_zadd_Suc: "z < z + int (Suc n)"
+by (auto simp add: zless_iff_Suc_zadd zadd_assoc zadd_int)
+
+lemma zless_trans: "[| z1<z2; z2<z3 |] ==> z1 < (z3::int)"
+by (auto simp add: zless_iff_Suc_zadd zadd_assoc zadd_int)
+
+lemma zless_not_sym: "!!w::int. z<w ==> ~w<z"
+apply (safe dest!: zless_iff_Suc_zadd [THEN iffD1])
+apply (rule_tac z = z in eq_Abs_Integ, safe)
+apply (simp add: int_def zadd)
+done
+
+(* [| n<m; ~P ==> m<n |] ==> P *)
+lemmas zless_asym = zless_not_sym [THEN swap, standard]
+
+lemma zless_not_refl: "!!z::int. ~ z<z"
+apply (rule zless_asym [THEN notI])
+apply (assumption+)
+done
+
+(* z<z ==> R *)
+lemmas zless_irrefl = zless_not_refl [THEN notE, standard, elim!]
+
+
+(*"Less than" is a linear ordering*)
+lemma zless_linear:
+ "z<w | z=w | w<(z::int)"
+apply (unfold zless_def neg_def zdiff_def)
+apply (rule_tac z = z in eq_Abs_Integ)
+apply (rule_tac z = w in eq_Abs_Integ, safe)
+apply (simp add: zadd zminus Image_iff Bex_def)
+apply (rule_tac m1 = "x+ya" and n1 = "xa+y" in less_linear [THEN disjE])
+apply (force simp add: add_ac)+
+done
+
+lemma int_neq_iff: "!!w::int. (w ~= z) = (w<z | z<w)"
+by (cut_tac zless_linear, blast)
+
+(*** eliminates ~= in premises ***)
+lemmas int_neqE = int_neq_iff [THEN iffD1, THEN disjE, standard]
+
+lemma int_int_eq [iff]: "(int m = int n) = (m = n)"
+by (fast elim!: inj_int [THEN injD])
+
+lemma int_eq_0_conv [simp]: "(int n = 0) = (n = 0)"
+by (simp add: Zero_int_def)
+
+lemma zless_int [simp]: "(int m < int n) = (m<n)"
+by (simp add: less_iff_Suc_add zless_iff_Suc_zadd zadd_int)
+
+lemma int_less_0_conv [simp]: "~ (int k < 0)"
+by (simp add: Zero_int_def)
+
+lemma zero_less_int_conv [simp]: "(0 < int n) = (0 < n)"
+by (simp add: Zero_int_def)
+
+
+(*** Properties of <= ***)
+
+lemma zle_int [simp]: "(int m <= int n) = (m<=n)"
+by (simp add: zle_def le_def)
+
+lemma zero_zle_int [simp]: "(0 <= int n)"
+by (simp add: Zero_int_def)
+
+lemma int_le_0_conv [simp]: "(int n <= 0) = (n = 0)"
+by (simp add: Zero_int_def)
+
+lemma zle_imp_zless_or_eq: "z <= w ==> z < w | z=(w::int)"
+apply (unfold zle_def)
+apply (cut_tac zless_linear)
+apply (blast elim: zless_asym)
+done
+
+lemma zless_or_eq_imp_zle: "z<w | z=w ==> z <= (w::int)"
+apply (unfold zle_def)
+apply (cut_tac zless_linear)
+apply (blast elim: zless_asym)
+done
+
+lemma int_le_less: "(x <= (y::int)) = (x < y | x=y)"
+apply (rule iffI)
+apply (erule zle_imp_zless_or_eq)
+apply (erule zless_or_eq_imp_zle)
+done
+
+lemma zle_refl: "w <= (w::int)"
+by (simp add: int_le_less)
+
+(* Axiom 'linorder_linear' of class 'linorder': *)
+lemma zle_linear: "(z::int) <= w | w <= z"
+apply (simp add: int_le_less)
+apply (cut_tac zless_linear, blast)
+done
+
+(* Axiom 'order_trans of class 'order': *)
+lemma zle_trans: "[| i <= j; j <= k |] ==> i <= (k::int)"
+apply (drule zle_imp_zless_or_eq)
+apply (drule zle_imp_zless_or_eq)
+apply (rule zless_or_eq_imp_zle)
+apply (blast intro: zless_trans)
+done
+
+lemma zle_anti_sym: "[| z <= w; w <= z |] ==> z = (w::int)"
+apply (drule zle_imp_zless_or_eq)
+apply (drule zle_imp_zless_or_eq)
+apply (blast elim: zless_asym)
+done
+
+(* Axiom 'order_less_le' of class 'order': *)
+lemma int_less_le: "((w::int) < z) = (w <= z & w ~= z)"
+apply (simp add: zle_def int_neq_iff)
+apply (blast elim!: zless_asym)
+done
+
+
+(*** Subtraction laws ***)
+
+lemma zadd_zdiff_eq: "x + (y - z) = (x + y) - (z::int)"
+by (simp add: zdiff_def zadd_ac)
+
+lemma zdiff_zadd_eq: "(x - y) + z = (x + z) - (y::int)"
+by (simp add: zdiff_def zadd_ac)
+
+lemma zdiff_zdiff_eq: "(x - y) - z = x - (y + (z::int))"
+by (simp add: zdiff_def zadd_ac)
+
+lemma zdiff_zdiff_eq2: "x - (y - z) = (x + z) - (y::int)"
+by (simp add: zdiff_def zadd_ac)
+
+lemma zdiff_zless_eq: "(x-y < z) = (x < z + (y::int))"
+apply (unfold zless_def zdiff_def)
+apply (simp add: zadd_ac)
+done
+
+lemma zless_zdiff_eq: "(x < z-y) = (x + (y::int) < z)"
+apply (unfold zless_def zdiff_def)
+apply (simp add: zadd_ac)
+done
+
+lemma zdiff_zle_eq: "(x-y <= z) = (x <= z + (y::int))"
+apply (unfold zle_def)
+apply (simp add: zless_zdiff_eq)
+done
+
+lemma zle_zdiff_eq: "(x <= z-y) = (x + (y::int) <= z)"
+apply (unfold zle_def)
+apply (simp add: zdiff_zless_eq)
+done
+
+lemma zdiff_eq_eq: "(x-y = z) = (x = z + (y::int))"
+by (auto simp add: zdiff_def zadd_assoc Zero_int_def [symmetric])
+
+lemma eq_zdiff_eq: "(x = z-y) = (x + (y::int) = z)"
+by (auto simp add: zdiff_def zadd_assoc Zero_int_def [symmetric])
+
+(*This list of rewrites simplifies (in)equalities by bringing subtractions
+ to the top and then moving negative terms to the other side.
+ Use with zadd_ac*)
+lemmas zcompare_rls =
+ zdiff_def [symmetric]
+ 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
+
+
+(** Cancellation laws **)
+
+lemma zadd_left_cancel [simp]: "!!w::int. (z + w' = z + w) = (w' = w)"
+apply safe
+apply (drule_tac f = "%x. x + (-z) " in arg_cong)
+apply (simp add: Zero_int_def [symmetric] zadd_ac)
+done
+
+lemma zadd_right_cancel [simp]: "!!z::int. (w' + z = w + z) = (w' = w)"
+by (simp add: zadd_ac)
+
+
+(** For the cancellation simproc.
+ The idea is to cancel like terms on opposite sides by subtraction **)
+
+lemma zless_eqI: "(x::int) - y = x' - y' ==> (x<y) = (x'<y')"
+by (simp add: zless_def)
+
+lemma zle_eqI: "(x::int) - y = x' - y' ==> (y<=x) = (y'<=x')"
+apply (drule zless_eqI)
+apply (simp (no_asm_simp) add: zle_def)
+done
+
+lemma zeq_eqI: "(x::int) - y = x' - y' ==> (x=y) = (x'=y')"
+apply safe
+apply (simp_all add: eq_zdiff_eq zdiff_eq_eq)
+done
+
+ML
+{*
+val int_def = thm "int_def";
+val neg_def = thm "neg_def";
+val iszero_def = thm "iszero_def";
+val Zero_int_def = thm "Zero_int_def";
+val One_int_def = thm "One_int_def";
+val zadd_def = thm "zadd_def";
+val zdiff_def = thm "zdiff_def";
+val zless_def = thm "zless_def";
+val zle_def = thm "zle_def";
+val zmult_def = thm "zmult_def";
+
+val intrel_iff = thm "intrel_iff";
+val equiv_intrel = thm "equiv_intrel";
+val equiv_intrel_iff = thm "equiv_intrel_iff";
+val intrel_in_integ = thm "intrel_in_integ";
+val inj_on_Abs_Integ = thm "inj_on_Abs_Integ";
+val inj_Rep_Integ = thm "inj_Rep_Integ";
+val inj_int = thm "inj_int";
+val zminus_congruent = thm "zminus_congruent";
+val zminus = thm "zminus";
+val eq_Abs_Integ = thm "eq_Abs_Integ";
+val zminus_zminus = thm "zminus_zminus";
+val inj_zminus = thm "inj_zminus";
+val zminus_0 = thm "zminus_0";
+val not_neg_int = thm "not_neg_int";
+val neg_zminus_int = thm "neg_zminus_int";
+val zadd = thm "zadd";
+val zminus_zadd_distrib = thm "zminus_zadd_distrib";
+val zadd_commute = thm "zadd_commute";
+val zadd_assoc = thm "zadd_assoc";
+val zadd_left_commute = thm "zadd_left_commute";
+val zadd_ac = thms "zadd_ac";
+val zadd_int = thm "zadd_int";
+val zadd_int_left = thm "zadd_int_left";
+val int_Suc = thm "int_Suc";
+val zadd_0 = thm "zadd_0";
+val zadd_0_right = thm "zadd_0_right";
+val zadd_zminus_inverse = thm "zadd_zminus_inverse";
+val zadd_zminus_inverse2 = thm "zadd_zminus_inverse2";
+val zadd_zminus_cancel = thm "zadd_zminus_cancel";
+val zminus_zadd_cancel = thm "zminus_zadd_cancel";
+val zdiff0 = thm "zdiff0";
+val zdiff0_right = thm "zdiff0_right";
+val zdiff_self = thm "zdiff_self";
+val zadd_assoc_cong = thm "zadd_assoc_cong";
+val zadd_assoc_swap = thm "zadd_assoc_swap";
+val zmult_congruent2 = thm "zmult_congruent2";
+val zmult = thm "zmult";
+val zmult_zminus = thm "zmult_zminus";
+val zmult_commute = thm "zmult_commute";
+val zmult_assoc = thm "zmult_assoc";
+val zmult_left_commute = thm "zmult_left_commute";
+val zmult_ac = thms "zmult_ac";
+val zadd_zmult_distrib = thm "zadd_zmult_distrib";
+val zmult_zminus_right = thm "zmult_zminus_right";
+val zadd_zmult_distrib2 = thm "zadd_zmult_distrib2";
+val zdiff_zmult_distrib = thm "zdiff_zmult_distrib";
+val zdiff_zmult_distrib2 = thm "zdiff_zmult_distrib2";
+val int_distrib = thms "int_distrib";
+val zmult_int = thm "zmult_int";
+val zmult_0 = thm "zmult_0";
+val zmult_1 = thm "zmult_1";
+val zmult_0_right = thm "zmult_0_right";
+val zmult_1_right = thm "zmult_1_right";
+val zless_iff_Suc_zadd = thm "zless_iff_Suc_zadd";
+val zless_zadd_Suc = thm "zless_zadd_Suc";
+val zless_trans = thm "zless_trans";
+val zless_not_sym = thm "zless_not_sym";
+val zless_asym = thm "zless_asym";
+val zless_not_refl = thm "zless_not_refl";
+val zless_irrefl = thm "zless_irrefl";
+val zless_linear = thm "zless_linear";
+val int_neq_iff = thm "int_neq_iff";
+val int_neqE = thm "int_neqE";
+val int_int_eq = thm "int_int_eq";
+val int_eq_0_conv = thm "int_eq_0_conv";
+val zless_int = thm "zless_int";
+val int_less_0_conv = thm "int_less_0_conv";
+val zero_less_int_conv = thm "zero_less_int_conv";
+val zle_int = thm "zle_int";
+val zero_zle_int = thm "zero_zle_int";
+val int_le_0_conv = thm "int_le_0_conv";
+val zle_imp_zless_or_eq = thm "zle_imp_zless_or_eq";
+val zless_or_eq_imp_zle = thm "zless_or_eq_imp_zle";
+val int_le_less = thm "int_le_less";
+val zle_refl = thm "zle_refl";
+val zle_linear = thm "zle_linear";
+val zle_trans = thm "zle_trans";
+val zle_anti_sym = thm "zle_anti_sym";
+val int_less_le = thm "int_less_le";
+val zadd_zdiff_eq = thm "zadd_zdiff_eq";
+val zdiff_zadd_eq = thm "zdiff_zadd_eq";
+val zdiff_zdiff_eq = thm "zdiff_zdiff_eq";
+val zdiff_zdiff_eq2 = thm "zdiff_zdiff_eq2";
+val zdiff_zless_eq = thm "zdiff_zless_eq";
+val zless_zdiff_eq = thm "zless_zdiff_eq";
+val zdiff_zle_eq = thm "zdiff_zle_eq";
+val zle_zdiff_eq = thm "zle_zdiff_eq";
+val zdiff_eq_eq = thm "zdiff_eq_eq";
+val eq_zdiff_eq = thm "eq_zdiff_eq";
+val zcompare_rls = thms "zcompare_rls";
+val zadd_left_cancel = thm "zadd_left_cancel";
+val zadd_right_cancel = thm "zadd_right_cancel";
+val zless_eqI = thm "zless_eqI";
+val zle_eqI = thm "zle_eqI";
+val zeq_eqI = thm "zeq_eqI";
+*}
+
end
--- a/src/HOL/Integ/IntPower.ML Tue Nov 18 09:45:45 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-(* Title: IntPower.thy
- ID: $Id$
- Author: Thomas M. Rasmussen
- Copyright 2000 University of Cambridge
-
-Integer powers
-*)
-
-
-Goal "((x::int) mod m)^y mod m = x^y mod m";
-by (induct_tac "y" 1);
-by Auto_tac;
-by (rtac (zmod_zmult1_eq RS trans) 1);
-by (Asm_simp_tac 1);
-by (rtac (zmod_zmult_distrib RS sym) 1);
-qed "zpower_zmod";
-
-Goal "1^y = (1::int)";
-by (induct_tac "y" 1);
-by Auto_tac;
-qed "zpower_1";
-Addsimps [zpower_1];
-
-Goal "(x*z)^y = ((x^y)*(z^y)::int)";
-by (induct_tac "y" 1);
-by Auto_tac;
-qed "zpower_zmult_distrib";
-
-Goal "x^(y+z) = ((x^y)*(x^z)::int)";
-by (induct_tac "y" 1);
-by Auto_tac;
-qed "zpower_zadd_distrib";
-
-Goal "(x^y)^z = (x^(y*z)::int)";
-by (induct_tac "y" 1);
-by Auto_tac;
-by (stac zpower_zmult_distrib 1);
-by (stac zpower_zadd_distrib 1);
-by (Asm_simp_tac 1);
-qed "zpower_zpower";
-
-
-(*** Logical equivalences for inequalities ***)
-
-Goal "(x^n = 0) = (x = (0::int) & 0<n)";
-by (induct_tac "n" 1);
-by Auto_tac;
-qed "zpower_eq_0_iff";
-Addsimps [zpower_eq_0_iff];
-
-Goal "(0 < (abs x)^n) = (x ~= (0::int) | n=0)";
-by (induct_tac "n" 1);
-by (auto_tac (claset(), simpset() addsimps [int_0_less_mult_iff]));
-qed "zero_less_zpower_abs_iff";
-Addsimps [zero_less_zpower_abs_iff];
-
-Goal "(0::int) <= (abs x)^n";
-by (induct_tac "n" 1);
-by (auto_tac (claset(), simpset() addsimps [int_0_le_mult_iff]));
-qed "zero_le_zpower_abs";
-Addsimps [zero_le_zpower_abs];
--- a/src/HOL/Integ/IntPower.thy Tue Nov 18 09:45:45 2003 +0100
+++ b/src/HOL/Integ/IntPower.thy Tue Nov 18 11:01:52 2003 +0100
@@ -6,13 +6,66 @@
Integer powers
*)
-IntPower = IntDiv +
+theory IntPower = IntDiv:
-instance
- int :: {power}
+instance int :: power ..
primrec
- power_0 "p ^ 0 = 1"
- power_Suc "p ^ (Suc n) = (p::int) * (p ^ n)"
+ power_0: "p ^ 0 = 1"
+ power_Suc: "p ^ (Suc n) = (p::int) * (p ^ n)"
+
+
+lemma zpower_zmod: "((x::int) mod m)^y mod m = x^y mod m"
+apply (induct_tac "y", auto)
+apply (rule zmod_zmult1_eq [THEN trans])
+apply (simp (no_asm_simp))
+apply (rule zmod_zmult_distrib [symmetric])
+done
+
+lemma zpower_1 [simp]: "1^y = (1::int)"
+by (induct_tac "y", auto)
+
+lemma zpower_zmult_distrib: "(x*z)^y = ((x^y)*(z^y)::int)"
+by (induct_tac "y", auto)
+
+lemma zpower_zadd_distrib: "x^(y+z) = ((x^y)*(x^z)::int)"
+by (induct_tac "y", auto)
+
+lemma zpower_zpower: "(x^y)^z = (x^(y*z)::int)"
+apply (induct_tac "y", auto)
+apply (subst zpower_zmult_distrib)
+apply (subst zpower_zadd_distrib)
+apply (simp (no_asm_simp))
+done
+
+
+(*** Logical equivalences for inequalities ***)
+
+lemma zpower_eq_0_iff [simp]: "(x^n = 0) = (x = (0::int) & 0<n)"
+by (induct_tac "n", auto)
+
+lemma zero_less_zpower_abs_iff [simp]:
+ "(0 < (abs x)^n) = (x \<noteq> (0::int) | n=0)"
+apply (induct_tac "n")
+apply (auto simp add: int_0_less_mult_iff)
+done
+
+lemma zero_le_zpower_abs [simp]: "(0::int) <= (abs x)^n"
+apply (induct_tac "n")
+apply (auto simp add: int_0_le_mult_iff)
+done
+
+ML
+{*
+val zpower_zmod = thm "zpower_zmod";
+val zpower_1 = thm "zpower_1";
+val zpower_zmult_distrib = thm "zpower_zmult_distrib";
+val zpower_zadd_distrib = thm "zpower_zadd_distrib";
+val zpower_zpower = thm "zpower_zpower";
+val zpower_eq_0_iff = thm "zpower_eq_0_iff";
+val zero_less_zpower_abs_iff = thm "zero_less_zpower_abs_iff";
+val zero_le_zpower_abs = thm "zero_le_zpower_abs";
+*}
end
+
--- a/src/HOL/Integ/cooper_proof.ML Tue Nov 18 09:45:45 2003 +0100
+++ b/src/HOL/Integ/cooper_proof.ML Tue Nov 18 11:01:52 2003 +0100
@@ -44,7 +44,7 @@
(*-----------------------------------------------------------------*)
val presburger_ss = simpset_of (theory "Presburger")
- addsimps [zdiff_def] delsimps [symmetric zdiff_def];
+ addsimps [zdiff_def] delsimps [thm"zdiff_def_symmetric"];
val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
(*Theorems that will be used later for the proofgeneration*)
@@ -52,7 +52,7 @@
val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0";
val unity_coeff_ex = thm "unity_coeff_ex";
-(* Thorems for proving the adjustment of the coeffitients*)
+(* Theorems for proving the adjustment of the coefficients*)
val ac_lt_eq = thm "ac_lt_eq";
val ac_eq_eq = thm "ac_eq_eq";
@@ -68,7 +68,7 @@
val qe_exI = thm "qe_exI";
val qe_ALLI = thm "qe_ALLI";
-(*Modulo D property for Pminusinf an Plusinf *)
+(*Modulo D property for Pminusinf and Plusinf *)
val fm_modd_minf = thm "fm_modd_minf";
val not_dvd_modd_minf = thm "not_dvd_modd_minf";
val dvd_modd_minf = thm "dvd_modd_minf";
@@ -77,7 +77,7 @@
val not_dvd_modd_pinf = thm "not_dvd_modd_pinf";
val dvd_modd_pinf = thm "dvd_modd_pinf";
-(* the minusinfinity proprty*)
+(* the minusinfinity property*)
val fm_eq_minf = thm "fm_eq_minf";
val neq_eq_minf = thm "neq_eq_minf";
@@ -87,7 +87,7 @@
val not_dvd_eq_minf = thm "not_dvd_eq_minf";
val dvd_eq_minf = thm "dvd_eq_minf";
-(* the Plusinfinity proprty*)
+(* the Plusinfinity property*)
val fm_eq_pinf = thm "fm_eq_pinf";
val neq_eq_pinf = thm "neq_eq_pinf";
--- a/src/HOL/Integ/int_arith2.ML Tue Nov 18 09:45:45 2003 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-(* Title: HOL/Integ/int_arith2.ML
- ID: $Id$
- Authors: Larry Paulson and Tobias Nipkow
-*)
-
-Goal "(w <= z - (1::int)) = (w<(z::int))";
-by (arith_tac 1);
-qed "zle_diff1_eq";
-Addsimps [zle_diff1_eq];
-
-Goal "(w < z + 1) = (w<=(z::int))";
-by (arith_tac 1);
-qed "zle_add1_eq_le";
-Addsimps [zle_add1_eq_le];
-
-Goal "(z = z + w) = (w = (0::int))";
-by (arith_tac 1);
-qed "zadd_left_cancel0";
-Addsimps [zadd_left_cancel0];
-
-
-(* nat *)
-
-val [major,minor] = Goal "[| 0 <= z; !!m. z = int m ==> P |] ==> P";
-by (rtac (major RS nat_0_le RS sym RS minor) 1);
-qed "nonneg_eq_int";
-
-Goal "(nat w = m) = (if 0 <= w then w = int m else m=0)";
-by Auto_tac;
-qed "nat_eq_iff";
-
-Goal "(m = nat w) = (if 0 <= w then w = int m else m=0)";
-by Auto_tac;
-qed "nat_eq_iff2";
-
-Goal "0 <= w ==> (nat w < m) = (w < int m)";
-by (rtac iffI 1);
-by (asm_full_simp_tac
- (simpset() delsimps [zless_int] addsimps [zless_int RS sym]) 2);
-by (etac (nat_0_le RS subst) 1);
-by (Simp_tac 1);
-qed "nat_less_iff";
-
-Goal "(int m = z) = (m = nat z & 0 <= z)";
-by (auto_tac (claset(), simpset() addsimps [nat_eq_iff2]));
-qed "int_eq_iff";
-
-
-(*Users don't want to see (int 0), int(Suc 0) or w + - z*)
-Addsimps (map symmetric [Zero_int_def, One_int_def, zdiff_def]);
-
-Goal "nat 0 = 0";
-by (simp_tac (simpset() addsimps [nat_eq_iff]) 1);
-qed "nat_0";
-
-Goal "nat 1 = Suc 0";
-by (stac nat_eq_iff 1);
-by (Simp_tac 1);
-qed "nat_1";
-
-Goal "nat 2 = Suc (Suc 0)";
-by (stac nat_eq_iff 1);
-by (Simp_tac 1);
-qed "nat_2";
-
-Goal "0 <= w ==> (nat w < nat z) = (w<z)";
-by (case_tac "neg z" 1);
-by (auto_tac (claset(), simpset() addsimps [nat_less_iff]));
-by (auto_tac (claset() addIs [zless_trans],
- simpset() addsimps [neg_eq_less_0, zle_def]));
-qed "nat_less_eq_zless";
-
-Goal "0 < w | 0 <= z ==> (nat w <= nat z) = (w<=z)";
-by (auto_tac (claset(),
- simpset() addsimps [linorder_not_less RS sym,
- zless_nat_conj]));
-qed "nat_le_eq_zle";
-
-(*** abs: absolute value, as an integer ****)
-
-(* Simpler: use zabs_def as rewrite rule;
- but arith_tac is not parameterized by such simp rules
-*)
-
-Goalw [zabs_def]
- "P(abs(i::int)) = ((0 <= i --> P i) & (i < 0 --> P(-i)))";
-by (Simp_tac 1);
-qed "zabs_split";
-
-Goal "0 <= abs (z::int)";
-by (simp_tac (simpset() addsimps [zabs_def]) 1);
-qed "zero_le_zabs";
-AddIffs [zero_le_zabs];
-
-
-(*Not sure why this simprule is required!*)
-Addsimps [inst "z" "number_of ?v" int_eq_iff];
-
-(*continued in IntArith.ML ...*)
--- a/src/HOL/IsaMakefile Tue Nov 18 09:45:45 2003 +0100
+++ b/src/HOL/IsaMakefile Tue Nov 18 11:01:52 2003 +0100
@@ -86,11 +86,11 @@
Hilbert_Choice.thy Hilbert_Choice_lemmas.ML HOL.ML \
HOL.thy HOL_lemmas.ML Inductive.thy Integ/Bin.ML Integ/Bin.thy \
Integ/cooper_dec.ML Integ/cooper_proof.ML \
- Integ/Equiv.ML Integ/Equiv.thy Integ/Int_lemmas.ML Integ/Int.thy \
- Integ/IntArith.ML Integ/IntArith.thy Integ/IntDef.ML Integ/IntDef.thy \
- Integ/IntDiv.thy Integ/IntPower.ML Integ/IntPower.thy \
+ Integ/Equiv.thy Integ/Int_lemmas.ML Integ/Int.thy \
+ Integ/IntArith.thy Integ/IntDef.thy \
+ Integ/IntDiv.thy Integ/IntPower.thy \
Integ/nat_bin.ML Integ/NatBin.thy Integ/NatSimprocs.ML \
- Integ/NatSimprocs.thy Integ/int_arith1.ML Integ/int_arith2.ML \
+ Integ/NatSimprocs.thy Integ/int_arith1.ML \
Integ/int_factor_simprocs.ML Integ/nat_simprocs.ML \
Integ/Presburger.thy Integ/presburger.ML Integ/qelim.ML \
Lfp.ML Lfp.thy List.ML List.thy Main.ML Main.thy Map.thy Nat.ML \
--- a/src/HOL/Tools/Presburger/cooper_proof.ML Tue Nov 18 09:45:45 2003 +0100
+++ b/src/HOL/Tools/Presburger/cooper_proof.ML Tue Nov 18 11:01:52 2003 +0100
@@ -44,7 +44,7 @@
(*-----------------------------------------------------------------*)
val presburger_ss = simpset_of (theory "Presburger")
- addsimps [zdiff_def] delsimps [symmetric zdiff_def];
+ addsimps [zdiff_def] delsimps [thm"zdiff_def_symmetric"];
val cboolT = ctyp_of (sign_of HOL.thy) HOLogic.boolT;
(*Theorems that will be used later for the proofgeneration*)
@@ -52,7 +52,7 @@
val zdvd_iff_zmod_eq_0 = thm "zdvd_iff_zmod_eq_0";
val unity_coeff_ex = thm "unity_coeff_ex";
-(* Thorems for proving the adjustment of the coeffitients*)
+(* Theorems for proving the adjustment of the coefficients*)
val ac_lt_eq = thm "ac_lt_eq";
val ac_eq_eq = thm "ac_eq_eq";
@@ -68,7 +68,7 @@
val qe_exI = thm "qe_exI";
val qe_ALLI = thm "qe_ALLI";
-(*Modulo D property for Pminusinf an Plusinf *)
+(*Modulo D property for Pminusinf and Plusinf *)
val fm_modd_minf = thm "fm_modd_minf";
val not_dvd_modd_minf = thm "not_dvd_modd_minf";
val dvd_modd_minf = thm "dvd_modd_minf";
@@ -77,7 +77,7 @@
val not_dvd_modd_pinf = thm "not_dvd_modd_pinf";
val dvd_modd_pinf = thm "dvd_modd_pinf";
-(* the minusinfinity proprty*)
+(* the minusinfinity property*)
val fm_eq_minf = thm "fm_eq_minf";
val neq_eq_minf = thm "neq_eq_minf";
@@ -87,7 +87,7 @@
val not_dvd_eq_minf = thm "not_dvd_eq_minf";
val dvd_eq_minf = thm "dvd_eq_minf";
-(* the Plusinfinity proprty*)
+(* the Plusinfinity property*)
val fm_eq_pinf = thm "fm_eq_pinf";
val neq_eq_pinf = thm "neq_eq_pinf";