--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Import/HOL_Light/HOLLightReal.thy Sat Mar 03 21:51:38 2012 +0100
@@ -0,0 +1,329 @@
+(* Title: HOL/Import/HOLLightReal.thy
+ Author: Cezary Kaliszyk
+*)
+
+header {* Compatibility theorems for HOL Light reals *}
+
+theory HOLLightReal imports Real begin
+
+lemma REAL_OF_NUM_MAX:
+ "max (real (m :: nat)) (real n) = real (max m n)"
+ by simp
+
+lemma REAL_OF_NUM_MIN:
+ "min (real (m :: nat)) (real n) = real (min m n)"
+ by simp
+
+lemma REAL_POLY_NEG_CLAUSES:
+ "(\<forall>(x :: real). - x = - 1 * x) \<and> (\<forall>(x :: real) y. x - y = x + - 1 * y)"
+ by simp
+
+lemma REAL_MUL_AC:
+ "(m :: real) * n = n * m \<and> m * n * p = m * (n * p) \<and> m * (n * p) = n * (m * p)"
+ by simp
+
+lemma REAL_EQ_ADD_LCANCEL_0:
+ "((x :: real) + y = x) = (y = 0)"
+ by simp
+
+lemma REAL_EQ_ADD_RCANCEL_0:
+ "((x :: real) + y = y) = (x = 0)"
+ by simp
+
+lemma REAL_LT_ANTISYM:
+ "\<not> ((x :: real) < y \<and> y < x)"
+ by simp
+
+lemma REAL_LET_ANTISYM:
+ "\<not> ((x :: real) \<le> y \<and> y < x)"
+ by simp
+
+lemma REAL_LT_NEGTOTAL:
+ "(x :: real) = 0 \<or> 0 < x \<or> 0 < - x"
+ by auto
+
+lemma REAL_LT_ADDNEG:
+ "((y :: real) < x + - z) = (y + z < x)"
+ by auto
+
+lemma REAL_LT_ADDNEG2:
+ "((x :: real) + - y < z) = (x < z + y)"
+ by auto
+
+lemma REAL_LT_ADD1:
+ "(x :: real) \<le> y \<longrightarrow> x < y + 1"
+ by simp
+
+lemma REAL_SUB_ADD2:
+ "(y :: real) + (x - y) = x"
+ by simp
+
+lemma REAL_ADD_SUB:
+ "(x :: real) + y - x = y"
+ by simp
+
+lemma REAL_NEG_EQ:
+ "(- (x :: real) = y) = (x = - y)"
+ by auto
+
+lemma REAL_LE_ADDR:
+ "((x :: real) \<le> x + y) = (0 \<le> y)"
+ by simp
+
+lemma REAL_LE_ADDL:
+ "((y :: real) \<le> x + y) = (0 \<le> x)"
+ by simp
+
+lemma REAL_LT_ADDR:
+ "((x :: real) < x + y) = (0 < y)"
+ by simp
+
+lemma REAL_LT_ADDL:
+ "((y :: real) < x + y) = (0 < x)"
+ by simp
+
+lemma REAL_SUB_SUB:
+ "(x :: real) - y - x = - y"
+ by simp
+
+lemma REAL_SUB_LNEG:
+ "- (x :: real) - y = - (x + y)"
+ by simp
+
+lemma REAL_SUB_NEG2:
+ "- (x :: real) - - y = y - x"
+ by simp
+
+lemma REAL_SUB_TRIANGLE:
+ "(a :: real) - b + (b - c) = a - c"
+ by simp
+
+lemma REAL_SUB_SUB2:
+ "(x :: real) - (x - y) = y"
+ by simp
+
+lemma REAL_ADD_SUB2:
+ "(x :: real) - (x + y) = - y"
+ by simp
+
+lemma REAL_POS_NZ:
+ "0 < (x :: real) \<longrightarrow> x \<noteq> 0"
+ by simp
+
+lemma REAL_DIFFSQ:
+ "((x :: real) + y) * (x - y) = x * x - y * y"
+ by (simp add: comm_semiring_1_class.normalizing_semiring_rules(7) right_distrib mult_diff_mult)
+
+lemma REAL_ABS_TRIANGLE_LE:
+ "abs (x :: real) + abs (y - x) \<le> z \<longrightarrow> abs y \<le> z"
+ by auto
+
+lemma REAL_ABS_TRIANGLE_LT:
+ "abs (x :: real) + abs (y - x) < z \<longrightarrow> abs y < z"
+ by auto
+
+lemma REAL_ABS_REFL:
+ "(abs (x :: real) = x) = (0 \<le> x)"
+ by auto
+
+lemma REAL_ABS_BETWEEN:
+ "(0 < (d :: real) \<and> x - d < y \<and> y < x + d) = (abs (y - x) < d)"
+ by auto
+
+lemma REAL_ABS_BOUND:
+ "abs ((x :: real) - y) < d \<longrightarrow> y < x + d"
+ by auto
+
+lemma REAL_ABS_STILLNZ:
+ "abs ((x :: real) - y) < abs y \<longrightarrow> x \<noteq> 0"
+ by auto
+
+lemma REAL_ABS_CASES:
+ "(x :: real) = 0 \<or> 0 < abs x"
+ by simp
+
+lemma REAL_ABS_BETWEEN1:
+ "(x :: real) < z \<and> abs (y - x) < z - x \<longrightarrow> y < z"
+ by auto
+
+lemma REAL_ABS_SIGN:
+ "abs ((x :: real) - y) < y \<longrightarrow> 0 < x"
+ by auto
+
+lemma REAL_ABS_SIGN2:
+ "abs ((x :: real) - y) < - y \<longrightarrow> x < 0"
+ by auto
+
+lemma REAL_ABS_CIRCLE:
+ "abs (h :: real) < abs y - abs x \<longrightarrow> abs (x + h) < abs y"
+ by auto
+
+lemma REAL_BOUNDS_LT:
+ "(- (k :: real) < x \<and> x < k) = (abs x < k)"
+ by auto
+
+lemma REAL_MIN_MAX:
+ "min (x :: real) y = - max (- x) (- y)"
+ by auto
+
+lemma REAL_MAX_MIN:
+ "max (x :: real) y = - min (- x) (- y)"
+ by auto
+
+lemma REAL_MAX_MAX:
+ "(x :: real) \<le> max x y \<and> y \<le> max x y"
+ by simp
+
+lemma REAL_MIN_MIN:
+ "min (x :: real) y \<le> x \<and> min x y \<le> y"
+ by simp
+
+lemma REAL_MAX_ACI:
+ "max (x :: real) y = max y x \<and>
+ max (max x y) z = max x (max y z) \<and>
+ max x (max y z) = max y (max x z) \<and> max x x = x \<and> max x (max x y) = max x y"
+ by auto
+
+
+lemma REAL_MIN_ACI:
+ "min (x :: real) y = min y x \<and>
+ min (min x y) z = min x (min y z) \<and>
+ min x (min y z) = min y (min x z) \<and> min x x = x \<and> min x (min x y) = min x y"
+ by auto
+
+lemma REAL_EQ_MUL_RCANCEL:
+ "((x :: real) * z = y * z) = (x = y \<or> z = 0)"
+ by auto
+
+lemma REAL_MUL_LINV_UNIQ:
+ "(x :: real) * y = 1 \<longrightarrow> inverse y = x"
+ by (metis inverse_inverse_eq inverse_unique)
+
+lemma REAL_DIV_RMUL:
+ "(y :: real) \<noteq> 0 \<longrightarrow> x / y * y = x"
+ by simp
+
+lemma REAL_DIV_LMUL:
+ "(y :: real) \<noteq> 0 \<longrightarrow> y * (x / y) = x"
+ by simp
+
+lemma REAL_LT_IMP_NZ:
+ "0 < (x :: real) \<longrightarrow> x \<noteq> 0"
+ by simp
+
+lemma REAL_LT_LCANCEL_IMP:
+ "0 < (x :: real) \<and> x * y < x * z \<longrightarrow> y < z"
+ by (auto simp add: mult_less_cancel_left_disj not_less_iff_gr_or_eq)
+
+lemma REAL_LT_RCANCEL_IMP:
+ "0 < (z :: real) \<and> x * z < y * z \<longrightarrow> x < y"
+ by (auto simp add: mult_less_cancel_left_disj not_less_iff_gr_or_eq)
+
+lemma REAL_MUL_POS_LE:
+ "(0 \<le> (x :: real) * y) = (x = 0 \<or> y = 0 \<or> 0 < x \<and> 0 < y \<or> x < 0 \<and> y < 0)"
+ by (metis less_eq_real_def mult_eq_0_iff zero_le_mult_iff)
+
+lemma REAL_EQ_RDIV_EQ:
+ "0 < (z :: real) \<longrightarrow> (x = y / z) = (x * z = y)"
+ by auto
+
+lemma REAL_EQ_LDIV_EQ:
+ "0 < (z :: real) \<longrightarrow> (x / z = y) = (x = y * z)"
+ by auto
+
+lemma REAL_SUB_INV:
+ "(x :: real) \<noteq> 0 \<and> y \<noteq> 0 \<longrightarrow> inverse x - inverse y = (y - x) / (x * y)"
+ by (simp add: division_ring_inverse_diff divide_real_def)
+
+lemma REAL_DOWN:
+ "0 < (d :: real) \<longrightarrow> (\<exists>e>0. e < d)"
+ by (intro impI exI[of _ "d / 2"]) simp
+
+lemma REAL_POW_MONO_LT:
+ "1 < (x :: real) \<and> m < n \<longrightarrow> x ^ m < x ^ n"
+ by simp
+
+lemma REAL_POW_MONO:
+ "1 \<le> (x :: real) \<and> m \<le> n \<longrightarrow> x ^ m \<le> x ^ n"
+ by (cases "m < n", cases "x = 1") auto
+
+lemma REAL_EQ_LCANCEL_IMP:
+ "(z :: real) \<noteq> 0 \<and> z * x = z * y \<longrightarrow> x = y"
+ by auto
+
+lemma REAL_LE_DIV:
+ "0 \<le> (x :: real) \<and> 0 \<le> y \<longrightarrow> 0 \<le> x / y"
+ by (simp add: zero_le_divide_iff)
+
+lemma REAL_10: "(1::real) \<noteq> 0"
+ by simp
+
+lemma REAL_ADD_ASSOC: "(x::real) + (y + z) = x + y + z"
+ by simp
+
+lemma REAL_MUL_ASSOC: "(x::real) * (y * z) = x * y * z"
+ by simp
+
+lemma REAL_ADD_LINV: "-x + x = (0::real)"
+ by simp
+
+lemma REAL_MUL_LINV: "x \<noteq> (0::real) \<Longrightarrow> inverse x * x = 1"
+ by simp
+
+lemma REAL_LT_TOTAL: "((x::real) = y) \<or> x < y \<or> y < x"
+ by auto
+
+lemma real_lte: "((x::real) \<le> y) = (\<not>(y < x))"
+ by auto
+
+lemma real_of_num: "((0::real) = 0) \<and> (!n. real (Suc n) = real n + 1)"
+ by (simp add: real_of_nat_Suc)
+
+lemma abs: "abs (x::real) = (if 0 \<le> x then x else -x)"
+ by (simp add: abs_if)
+
+lemma pow: "(!x::real. x ^ 0 = 1) \<and> (!x::real. \<forall>n. x ^ (Suc n) = x * x ^ n)"
+ by simp
+
+lemma REAL_POLY_CLAUSES:
+ "(\<forall>(x :: real) y z. x + (y + z) = x + y + z) \<and>
+ (\<forall>(x :: real) y. x + y = y + x) \<and>
+ (\<forall>(x :: real). 0 + x = x) \<and>
+ (\<forall>(x :: real) y z. x * (y * z) = x * y * z) \<and>
+ (\<forall>(x :: real) y. x * y = y * x) \<and>
+ (\<forall>(x :: real). 1 * x = x) \<and>
+ (\<forall>(x :: real). 0 * x = 0) \<and>
+ (\<forall>(x :: real) y z. x * (y + z) = x * y + x * z) \<and>
+ (\<forall>(x :: real). x ^ 0 = 1) \<and> (\<forall>(x :: real) n. x ^ Suc n = x * x ^ n)"
+ by (auto simp add: right_distrib)
+
+lemma REAL_COMPLETE:
+ "(\<exists>(x :: real). P x) \<and> (\<exists>(M :: real). \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
+ (\<exists>M. (\<forall>x. P x \<longrightarrow> x \<le> M) \<and>
+ (\<forall>M'. (\<forall>x. P x \<longrightarrow> x \<le> M') \<longrightarrow> M \<le> M'))"
+ using complete_real[unfolded Ball_def, of "Collect P"] by auto
+
+lemma REAL_COMPLETE_SOMEPOS:
+ "(\<exists>(x :: real). P x \<and> 0 \<le> x) \<and> (\<exists>M. \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
+ (\<exists>M. (\<forall>x. P x \<longrightarrow> x \<le> M) \<and>
+ (\<forall>M'. (\<forall>x. P x \<longrightarrow> x \<le> M') \<longrightarrow> M \<le> M'))"
+ using REAL_COMPLETE by auto
+
+lemma REAL_ADD_AC:
+ "(m :: real) + n = n + m \<and> m + n + p = m + (n + p) \<and> m + (n + p) = n + (m + p)"
+ by simp
+
+lemma REAL_LE_RNEG:
+ "((x :: real) \<le> - y) = (x + y \<le> 0)"
+ by auto
+
+lemma REAL_LE_NEGTOTAL:
+ "0 \<le> (x :: real) \<or> 0 \<le> - x"
+ by auto
+
+lemma DEF_real_sgn:
+ "sgn = (\<lambda>u. if (0 :: real) < u then 1 else if u < 0 then - 1 else 0)"
+ by (simp add: ext)
+
+end
+