# HG changeset patch # User paulson # Date 1069149712 -3600 # Node ID 79f7d3451b1ed25cc6205d8853bd566f1b4439b4 # Parent 9bd184c007f00055965b75f441222e142d90af7d conversion of ML to Isar scripts diff -r 9bd184c007f0 -r 79f7d3451b1e src/HOL/Integ/Equiv.ML --- 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"; diff -r 9bd184c007f0 -r 79f7d3451b1e src/HOL/Integ/Equiv.thy --- 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 diff -r 9bd184c007f0 -r 79f7d3451b1e src/HOL/Integ/IntArith.ML --- 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 \ -\ 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 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"; diff -r 9bd184c007f0 -r 79f7d3451b1e src/HOL/Integ/IntArith.thy --- 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 (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 \ P n) & (i < 0 \ P 0))" + "P(nat(i::int)) = ((\n. i = int n \ P n) & (i < 0 \ 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: + "(\i 1) --> + f 0 \ k --> k \ f n --> (\i \ 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: + "[| \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)" +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) \ x*y) = (0 \ x & 0 \ y | x \ 0 & y \ 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 \ (0::int)) = (0 \ x & y \ 0 | x \ 0 & 0 \ 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 \ x * (x::int)" +apply (subgoal_tac " (- x) * x \ 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 z; 0 \ 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) \ z'; z' \ 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) \ z ==> nat (z*z') = nat z * nat z'" +apply (case_tac "0 \ 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 \ (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 - diff -r 9bd184c007f0 -r 79f7d3451b1e src/HOL/Integ/IntDef.ML --- 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 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 m P *) -bind_thm ("zless_asym", zless_not_sym RS swap); - -Goal "!!z::int. ~ 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 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 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'<=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"; - diff -r 9bd184c007f0 -r 79f7d3451b1e src/HOL/Integ/IntDef.thy --- 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 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 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 z1 < (z3::int)" +by (auto simp add: zless_iff_Suc_zadd zadd_assoc zadd_int) + +lemma zless_not_sym: "!!w::int. z ~w m P *) +lemmas zless_asym = zless_not_sym [THEN swap, standard] + +lemma zless_not_refl: "!!z::int. ~ z R *) +lemmas zless_irrefl = zless_not_refl [THEN notE, standard, elim!] + + +(*"Less than" is a linear ordering*) +lemma zless_linear: + "z 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 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'<=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 diff -r 9bd184c007f0 -r 79f7d3451b1e src/HOL/Integ/IntPower.ML --- 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 (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 + diff -r 9bd184c007f0 -r 79f7d3451b1e src/HOL/Integ/cooper_proof.ML --- 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"; diff -r 9bd184c007f0 -r 79f7d3451b1e src/HOL/Integ/int_arith2.ML --- 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 (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 ...*) diff -r 9bd184c007f0 -r 79f7d3451b1e src/HOL/IsaMakefile --- 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 \ diff -r 9bd184c007f0 -r 79f7d3451b1e src/HOL/Tools/Presburger/cooper_proof.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";