Converting more of the "real" development to Isar scripts

--- 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);

--- 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(),

--- 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"
 

--- 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
 

--- 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 < (0::real) |] ==> 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<j;  k < (0::real) |] ==> 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<n) | (k < 0 & n<m))";
-by (case_tac "k = (0::real)" 1);
-by (auto_tac (claset(),
-              simpset() addsimps [linorder_neq_iff,
-                          real_mult_less_mono1, real_mult_less_mono1_neg]));
-by (auto_tac (claset(),
-              simpset() addsimps [linorder_not_less,
-                                  inst "y1" "m*k" (linorder_not_le RS sym),
-                                  inst "y1" "m" (linorder_not_le RS sym)]));
-by (TRYALL (etac notE));
-by (auto_tac (claset(),
-              simpset() addsimps [order_less_imp_le, real_mult_le_mono1,
-                                            real_mult_le_mono1_neg]));
-qed "real_mult_less_cancel2";
-
-Goal "(m*k <= n*k) = (((0::real) < k --> 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<n) | (k < 0 & n<m))";
-by (simp_tac (simpset() addsimps [inst "z" "k" real_mult_commute,
-                                  real_mult_less_cancel2]) 1);
-qed "real_mult_less_cancel1";
-
-Goal "!!k::real. (k*m <= k*n) = ((0 < k --> 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";
 

--- 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 < (0::real) |] ==> j*k < i*k"
+  by (rule Ring_and_Field.mult_strict_right_mono_neg)
+
+lemma real_mult_less_mono2_neg: "[| i<j;  k < (0::real) |] ==> 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<n) | (k < 0 & n<m))"
+  by (rule Ring_and_Field.mult_less_cancel_right) 
+
+lemma real_mult_le_cancel2:
+     "(m*k <= n*k) = (((0::real) < k --> 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<n) | (k < 0 & n<m))"
+  by (rule Ring_and_Field.mult_less_cancel_left) 
+
+lemma real_mult_le_cancel1:
+     "!!k::real. (k*m <= k*n) = ((0 < k --> 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