# HG changeset patch # User paulson # Date 1070616482 -3600 # Node ID 031a5a051bb4e6d453db7726a296f71612e52f21 # Parent 0cb8a9a144d2281d9c328b5f59cb6d4d017f99d0 Converting more of the "real" development to Isar scripts diff -r 0cb8a9a144d2 -r 031a5a051bb4 src/HOL/Hyperreal/HyperDef.ML --- a/src/HOL/Hyperreal/HyperDef.ML Thu Dec 04 21:57:15 2003 +0100 +++ b/src/HOL/Hyperreal/HyperDef.ML Fri Dec 05 10:28:02 2003 +0100 @@ -1047,7 +1047,7 @@ Goal "hypreal_of_real (inverse r) = inverse (hypreal_of_real r)"; by (case_tac "r=0" 1); -by (asm_simp_tac (simpset() addsimps [REAL_DIVIDE_ZERO, INVERSE_ZERO, +by (asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO, INVERSE_ZERO, HYPREAL_INVERSE_ZERO]) 1); by (res_inst_tac [("c1","hypreal_of_real r")] (hypreal_mult_left_cancel RS iffD1) 1); diff -r 0cb8a9a144d2 -r 031a5a051bb4 src/HOL/Hyperreal/Lim.ML --- a/src/HOL/Hyperreal/Lim.ML Thu Dec 04 21:57:15 2003 +0100 +++ b/src/HOL/Hyperreal/Lim.ML Fri Dec 05 10:28:02 2003 +0100 @@ -2043,7 +2043,7 @@ Goal "f a - (f b - f a)/(b - a) * a = \ \ f b - (f b - f a)/(b - a) * (b::real)"; by (case_tac "a = b" 1); -by (asm_full_simp_tac (simpset() addsimps [REAL_DIVIDE_ZERO]) 1); +by (asm_full_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 1); by (res_inst_tac [("c1","b - a")] (real_mult_left_cancel RS iffD1) 1); by (arith_tac 1); by (auto_tac (claset(), diff -r 0cb8a9a144d2 -r 031a5a051bb4 src/HOL/Integ/Int.thy --- a/src/HOL/Integ/Int.thy Thu Dec 04 21:57:15 2003 +0100 +++ b/src/HOL/Integ/Int.thy Fri Dec 05 10:28:02 2003 +0100 @@ -373,7 +373,6 @@ (*Legacy ML bindings, but no longer the structure Int.*) ML {* -val Int_thy = the_context () val zabs_def = thm "zabs_def" val nat_def = thm "nat_def" diff -r 0cb8a9a144d2 -r 031a5a051bb4 src/HOL/Real/RealArith.thy --- a/src/HOL/Real/RealArith.thy Thu Dec 04 21:57:15 2003 +0100 +++ b/src/HOL/Real/RealArith.thy Fri Dec 05 10:28:02 2003 +0100 @@ -1,5 +1,7 @@ theory RealArith = RealArith0 -files "real_arith.ML": +files ("real_arith.ML"): + +use "real_arith.ML" setup real_arith_setup diff -r 0cb8a9a144d2 -r 031a5a051bb4 src/HOL/Real/RealArith0.ML --- a/src/HOL/Real/RealArith0.ML Thu Dec 04 21:57:15 2003 +0100 +++ b/src/HOL/Real/RealArith0.ML Fri Dec 05 10:28:02 2003 +0100 @@ -3,184 +3,36 @@ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1999 University of Cambridge -Assorted facts that need binary literals and the arithmetic decision procedure - -Also, common factor cancellation +Common factor cancellation *) -Goal "x - - y = x + (y::real)"; -by (Simp_tac 1); -qed "real_diff_minus_eq"; -Addsimps [real_diff_minus_eq]; - -(** Division and inverse **) - -Goal "0/x = (0::real)"; -by (simp_tac (simpset() addsimps [real_divide_def]) 1); -qed "real_0_divide"; -Addsimps [real_0_divide]; - -Goal "((0::real) < inverse x) = (0 < x)"; -by (case_tac "x=0" 1); -by (asm_simp_tac (HOL_ss addsimps [INVERSE_ZERO]) 1); -by (auto_tac (claset() addDs [real_inverse_less_0], - simpset() addsimps [linorder_neq_iff, real_inverse_gt_0])); -qed "real_0_less_inverse_iff"; -Addsimps [real_0_less_inverse_iff]; - -Goal "(inverse x < (0::real)) = (x < 0)"; -by (case_tac "x=0" 1); -by (asm_simp_tac (HOL_ss addsimps [INVERSE_ZERO]) 1); -by (auto_tac (claset() addDs [real_inverse_less_0], - simpset() addsimps [linorder_neq_iff, real_inverse_gt_0])); -qed "real_inverse_less_0_iff"; -Addsimps [real_inverse_less_0_iff]; - -Goal "((0::real) <= inverse x) = (0 <= x)"; -by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); -qed "real_0_le_inverse_iff"; -Addsimps [real_0_le_inverse_iff]; - -Goal "(inverse x <= (0::real)) = (x <= 0)"; -by (simp_tac (simpset() addsimps [linorder_not_less RS sym]) 1); -qed "real_inverse_le_0_iff"; -Addsimps [real_inverse_le_0_iff]; - -Goalw [real_divide_def] "x/(0::real) = 0"; -by (stac INVERSE_ZERO 1); -by (Simp_tac 1); -qed "REAL_DIVIDE_ZERO"; - -Goal "inverse (x::real) = 1/x"; -by (simp_tac (simpset() addsimps [real_divide_def]) 1); -qed "real_inverse_eq_divide"; - -Goal "((0::real) < x/y) = (0 < x & 0 < y | x < 0 & y < 0)"; -by (simp_tac (simpset() addsimps [real_divide_def, real_0_less_mult_iff]) 1); -qed "real_0_less_divide_iff"; -Addsimps [inst "x" "number_of ?w" real_0_less_divide_iff]; - -Goal "(x/y < (0::real)) = (0 < x & y < 0 | x < 0 & 0 < y)"; -by (simp_tac (simpset() addsimps [real_divide_def, real_mult_less_0_iff]) 1); -qed "real_divide_less_0_iff"; -Addsimps [inst "x" "number_of ?w" real_divide_less_0_iff]; - -Goal "((0::real) <= x/y) = ((x <= 0 | 0 <= y) & (0 <= x | y <= 0))"; -by (simp_tac (simpset() addsimps [real_divide_def, real_0_le_mult_iff]) 1); -by Auto_tac; -qed "real_0_le_divide_iff"; -Addsimps [inst "x" "number_of ?w" real_0_le_divide_iff]; - -Goal "(x/y <= (0::real)) = ((x <= 0 | y <= 0) & (0 <= x | 0 <= y))"; -by (simp_tac (simpset() addsimps [real_divide_def, real_mult_le_0_iff]) 1); -by Auto_tac; -qed "real_divide_le_0_iff"; -Addsimps [inst "x" "number_of ?w" real_divide_le_0_iff]; - -Goal "(inverse(x::real) = 0) = (x = 0)"; -by (auto_tac (claset(), simpset() addsimps [INVERSE_ZERO])); -qed "real_inverse_zero_iff"; -Addsimps [real_inverse_zero_iff]; - -Goal "(x/y = 0) = (x=0 | y=(0::real))"; -by (auto_tac (claset(), simpset() addsimps [real_divide_def])); -qed "real_divide_eq_0_iff"; -Addsimps [real_divide_eq_0_iff]; - -Goal "h ~= (0::real) ==> h/h = 1"; -by (asm_simp_tac (simpset() addsimps [real_divide_def, real_mult_inv_left]) 1); -qed "real_divide_self_eq"; -Addsimps [real_divide_self_eq]; - - -(**** Factor cancellation theorems for "real" ****) - -(** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =, - but not (yet?) for k*m < n*k. **) -(* unused?? bind_thm ("real_mult_minus_right", real_minus_mult_eq2 RS sym); *) - -Goal "(-y < -x) = ((x::real) < y)"; -by (arith_tac 1); -qed "real_minus_less_minus"; -Addsimps [real_minus_less_minus]; - -Goal "[| i j*k < i*k"; -by (rtac (real_minus_less_minus RS iffD1) 1); -by (auto_tac (claset(), - simpset() delsimps [real_mult_minus_eq2] - addsimps [real_minus_mult_eq2])); -qed "real_mult_less_mono1_neg"; - -Goal "[| i k*j < k*i"; -by (rtac (real_minus_less_minus RS iffD1) 1); -by (auto_tac (claset(), - simpset() delsimps [real_mult_minus_eq1] - addsimps [real_minus_mult_eq1])); -qed "real_mult_less_mono2_neg"; - -Goal "[| i <= j; k <= (0::real) |] ==> j*k <= i*k"; -by (auto_tac (claset(), - simpset() addsimps [order_le_less, real_mult_less_mono1_neg])); -qed "real_mult_le_mono1_neg"; - -Goal "[| i <= j; k <= (0::real) |] ==> k*j <= k*i"; -by (dtac real_mult_le_mono1_neg 1); -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [real_mult_commute]))); -qed "real_mult_le_mono2_neg"; - -Goal "(m*k < n*k) = (((0::real) < k & m m<=n) & (k < 0 --> n<=m))"; -by (simp_tac (simpset() addsimps [linorder_not_less RS sym, - real_mult_less_cancel2]) 1); -qed "real_mult_le_cancel2"; - -Goal "(k*m < k*n) = (((0::real) < k & m m<=n) & (k < 0 --> n<=m))"; -by (simp_tac (simpset() addsimps [linorder_not_less RS sym, - real_mult_less_cancel1]) 1); -qed "real_mult_le_cancel1"; - -Goal "!!k::real. (k*m = k*n) = (k = 0 | m=n)"; -by (case_tac "k=0" 1); -by (auto_tac (claset(), simpset() addsimps [real_mult_left_cancel])); -qed "real_mult_eq_cancel1"; - -Goal "!!k::real. (m*k = n*k) = (k = 0 | m=n)"; -by (case_tac "k=0" 1); -by (auto_tac (claset(), simpset() addsimps [real_mult_right_cancel])); -qed "real_mult_eq_cancel2"; - -Goal "!!k::real. k~=0 ==> (k*m) / (k*n) = (m/n)"; -by (asm_simp_tac - (simpset() addsimps [real_divide_def, real_inverse_distrib]) 1); -by (subgoal_tac "k * m * (inverse k * inverse n) = \ -\ (k * inverse k) * (m * inverse n)" 1); -by (asm_full_simp_tac (simpset() addsimps []) 1); -by (asm_full_simp_tac (HOL_ss addsimps real_mult_ac) 1); -qed "real_mult_div_cancel1"; - -(*For ExtractCommonTerm*) -Goal "(k*m) / (k*n) = (if k = (0::real) then 0 else m/n)"; -by (simp_tac (simpset() addsimps [real_mult_div_cancel1]) 1); -qed "real_mult_div_cancel_disj"; +val real_diff_minus_eq = thm"real_diff_minus_eq"; +val real_0_divide = thm"real_0_divide"; +val real_0_less_inverse_iff = thm"real_0_less_inverse_iff"; +val real_inverse_less_0_iff = thm"real_inverse_less_0_iff"; +val real_0_le_inverse_iff = thm"real_0_le_inverse_iff"; +val real_inverse_le_0_iff = thm"real_inverse_le_0_iff"; +val real_inverse_eq_divide = thm"real_inverse_eq_divide"; +val real_0_less_divide_iff = thm"real_0_less_divide_iff"; +val real_divide_less_0_iff = thm"real_divide_less_0_iff"; +val real_0_le_divide_iff = thm"real_0_le_divide_iff"; +val real_divide_le_0_iff = thm"real_divide_le_0_iff"; +val real_inverse_zero_iff = thm"real_inverse_zero_iff"; +val real_divide_eq_0_iff = thm"real_divide_eq_0_iff"; +val real_divide_self_eq = thm"real_divide_self_eq"; +val real_minus_less_minus = thm"real_minus_less_minus"; +val real_mult_less_mono1_neg = thm"real_mult_less_mono1_neg"; +val real_mult_less_mono2_neg = thm"real_mult_less_mono2_neg"; +val real_mult_le_mono1_neg = thm"real_mult_le_mono1_neg"; +val real_mult_le_mono2_neg = thm"real_mult_le_mono2_neg"; +val real_mult_less_cancel2 = thm"real_mult_less_cancel2"; +val real_mult_le_cancel2 = thm"real_mult_le_cancel2"; +val real_mult_less_cancel1 = thm"real_mult_less_cancel1"; +val real_mult_le_cancel1 = thm"real_mult_le_cancel1"; +val real_mult_eq_cancel1 = thm"real_mult_eq_cancel1"; +val real_mult_eq_cancel2 = thm"real_mult_eq_cancel2"; +val real_mult_div_cancel1 = thm"real_mult_div_cancel1"; +val real_mult_div_cancel_disj = thm"real_mult_div_cancel_disj"; local @@ -466,7 +318,7 @@ Goal "(m/k = n/k) = (k = 0 | m = (n::real))"; by (case_tac "k=0" 1); -by (asm_simp_tac (simpset() addsimps [REAL_DIVIDE_ZERO]) 1); +by (asm_simp_tac (simpset() addsimps [DIVISION_BY_ZERO]) 1); by (asm_simp_tac (simpset() addsimps [real_divide_eq_eq, real_eq_divide_eq, real_mult_eq_cancel2]) 1); qed "real_divide_eq_cancel2"; @@ -474,7 +326,7 @@ Goal "(k/m = k/n) = (k = 0 | m = (n::real))"; by (case_tac "m=0 | n = 0" 1); by (auto_tac (claset(), - simpset() addsimps [REAL_DIVIDE_ZERO, real_divide_eq_eq, + simpset() addsimps [DIVISION_BY_ZERO, real_divide_eq_eq, real_eq_divide_eq, real_mult_eq_cancel1])); qed "real_divide_eq_cancel1"; diff -r 0cb8a9a144d2 -r 031a5a051bb4 src/HOL/Real/RealArith0.thy --- a/src/HOL/Real/RealArith0.thy Thu Dec 04 21:57:15 2003 +0100 +++ b/src/HOL/Real/RealArith0.thy Fri Dec 05 10:28:02 2003 +0100 @@ -3,4 +3,122 @@ setup real_arith_setup +subsection{*Assorted facts that need binary literals and the arithmetic decision procedure*} + +lemma real_diff_minus_eq: "x - - y = x + (y::real)" +by simp +declare real_diff_minus_eq [simp] + +(** Division and inverse **) + +lemma real_0_divide: "0/x = (0::real)" +by (simp add: real_divide_def) +declare real_0_divide [simp] + +lemma real_0_less_inverse_iff: "((0::real) < inverse x) = (0 < x)" +apply (case_tac "x=0") +apply (auto dest: real_inverse_less_0 simp add: linorder_neq_iff real_inverse_gt_0) +done +declare real_0_less_inverse_iff [simp] + +lemma real_inverse_less_0_iff: "(inverse x < (0::real)) = (x < 0)" +apply (case_tac "x=0") +apply (auto dest: real_inverse_less_0 simp add: linorder_neq_iff real_inverse_gt_0) +done +declare real_inverse_less_0_iff [simp] + +lemma real_0_le_inverse_iff: "((0::real) <= inverse x) = (0 <= x)" +by (simp add: linorder_not_less [symmetric]) +declare real_0_le_inverse_iff [simp] + +lemma real_inverse_le_0_iff: "(inverse x <= (0::real)) = (x <= 0)" +by (simp add: linorder_not_less [symmetric]) +declare real_inverse_le_0_iff [simp] + +lemma real_inverse_eq_divide: "inverse (x::real) = 1/x" +by (simp add: real_divide_def) + +lemma real_0_less_divide_iff: "((0::real) < x/y) = (0 < x & 0 < y | x < 0 & y < 0)" +by (simp add: real_divide_def real_0_less_mult_iff) +declare real_0_less_divide_iff [of "number_of w", standard, simp] + +lemma real_divide_less_0_iff: "(x/y < (0::real)) = (0 < x & y < 0 | x < 0 & 0 < y)" +by (simp add: real_divide_def real_mult_less_0_iff) +declare real_divide_less_0_iff [of "number_of w", standard, simp] + +lemma real_0_le_divide_iff: "((0::real) <= x/y) = ((x <= 0 | 0 <= y) & (0 <= x | y <= 0))" +by (simp add: real_divide_def real_0_le_mult_iff, auto) +declare real_0_le_divide_iff [of "number_of w", standard, simp] + +lemma real_divide_le_0_iff: "(x/y <= (0::real)) = ((x <= 0 | y <= 0) & (0 <= x | 0 <= y))" +by (simp add: real_divide_def real_mult_le_0_iff, auto) +declare real_divide_le_0_iff [of "number_of w", standard, simp] + +lemma real_inverse_zero_iff: "(inverse(x::real) = 0) = (x = 0)" + by (rule Ring_and_Field.inverse_nonzero_iff_nonzero) + +lemma real_divide_eq_0_iff: "(x/y = 0) = (x=0 | y=(0::real))" +by (auto simp add: real_divide_def) +declare real_divide_eq_0_iff [simp] + +lemma real_divide_self_eq: "h ~= (0::real) ==> h/h = 1" + by (rule Ring_and_Field.divide_self) + + + +(**** Factor cancellation theorems for "real" ****) + +(** Cancellation laws for k*m < k*n and m*k < n*k, also for <= and =, + but not (yet?) for k*m < n*k. **) + +lemma real_minus_less_minus: "(-y < -x) = ((x::real) < y)" + by (rule Ring_and_Field.neg_less_iff_less) + +lemma real_mult_less_mono1_neg: "[| i j*k < i*k" + by (rule Ring_and_Field.mult_strict_right_mono_neg) + +lemma real_mult_less_mono2_neg: "[| i k*j < k*i" + by (rule Ring_and_Field.mult_strict_left_mono_neg) + +lemma real_mult_le_mono1_neg: "[| i <= j; k <= (0::real) |] ==> j*k <= i*k" + by (rule Ring_and_Field.mult_right_mono_neg) + +lemma real_mult_le_mono2_neg: "[| i <= j; k <= (0::real) |] ==> k*j <= k*i" + by (rule Ring_and_Field.mult_left_mono_neg) + +lemma real_mult_less_cancel2: + "(m*k < n*k) = (((0::real) < k & m m<=n) & (k < 0 --> n<=m))" + by (rule Ring_and_Field.mult_le_cancel_right) + +lemma real_mult_less_cancel1: + "(k*m < k*n) = (((0::real) < k & m m<=n) & (k < 0 --> n<=m))" + by (rule Ring_and_Field.mult_le_cancel_left) + +lemma real_mult_eq_cancel1: "!!k::real. (k*m = k*n) = (k = 0 | m=n)" + by (rule Ring_and_Field.mult_cancel_left) + +lemma real_mult_eq_cancel2: "!!k::real. (m*k = n*k) = (k = 0 | m=n)" + by (rule Ring_and_Field.mult_cancel_right) + +lemma real_mult_div_cancel1: "!!k::real. k~=0 ==> (k*m) / (k*n) = (m/n)" +apply (simp add: real_divide_def real_inverse_distrib) +apply (subgoal_tac "k * m * (inverse k * inverse n) = (k * inverse k) * (m * inverse n) ") +apply simp +apply (simp only: mult_ac) +done + +(*For ExtractCommonTerm*) +lemma real_mult_div_cancel_disj: "(k*m) / (k*n) = (if k = (0::real) then 0 else m/n)" +by (simp add: real_mult_div_cancel1) + + + end