src/HOL/Import/HOLLightReal.thy
author nipkow
Mon Jan 30 21:49:41 2012 +0100 (2012-01-30)
changeset 46372 6fa9cdb8b850
parent 45051 c478d1876371
child 46783 3e89a5cab8d7
permissions -rw-r--r--
added "'a rel"
     1 (*  Title:      HOL/Import/HOLLightReal.thy
     2     Author:     Cezary Kaliszyk
     3 *)
     4 
     5 header {* Compatibility theorems for HOL Light reals *}
     6 
     7 theory HOLLightReal imports Real begin
     8 
     9 lemma REAL_OF_NUM_MAX:
    10   "max (real (m :: nat)) (real n) = real (max m n)"
    11   by simp
    12 
    13 lemma REAL_OF_NUM_MIN:
    14   "min (real (m :: nat)) (real n) = real (min m n)"
    15   by simp
    16 
    17 lemma REAL_POLY_NEG_CLAUSES:
    18   "(\<forall>(x :: real). - x = - 1 * x) \<and> (\<forall>(x :: real) y. x - y = x + - 1 * y)"
    19   by simp
    20 
    21 lemma REAL_MUL_AC:
    22   "(m :: real) * n = n * m \<and> m * n * p = m * (n * p) \<and> m * (n * p) = n * (m * p)"
    23   by simp
    24 
    25 lemma REAL_EQ_ADD_LCANCEL_0:
    26   "((x :: real) + y = x) = (y = 0)"
    27   by simp
    28 
    29 lemma REAL_EQ_ADD_RCANCEL_0:
    30   "((x :: real) + y = y) = (x = 0)"
    31   by simp
    32 
    33 lemma REAL_LT_ANTISYM:
    34   "\<not> ((x :: real) < y \<and> y < x)"
    35   by simp
    36 
    37 lemma REAL_LET_ANTISYM:
    38   "\<not> ((x :: real) \<le> y \<and> y < x)"
    39   by simp
    40 
    41 lemma REAL_LT_NEGTOTAL:
    42   "(x :: real) = 0 \<or> 0 < x \<or> 0 < - x"
    43   by auto
    44 
    45 lemma REAL_LT_ADDNEG:
    46   "((y :: real) < x + - z) = (y + z < x)"
    47   by auto
    48 
    49 lemma REAL_LT_ADDNEG2:
    50   "((x :: real) + - y < z) = (x < z + y)"
    51   by auto
    52 
    53 lemma REAL_LT_ADD1:
    54   "(x :: real) \<le> y \<longrightarrow> x < y + 1"
    55   by simp
    56 
    57 lemma REAL_SUB_ADD2:
    58   "(y :: real) + (x - y) = x"
    59   by simp
    60 
    61 lemma REAL_ADD_SUB:
    62   "(x :: real) + y - x = y"
    63   by simp
    64 
    65 lemma REAL_NEG_EQ:
    66   "(- (x :: real) = y) = (x = - y)"
    67   by auto
    68 
    69 lemma REAL_LE_ADDR:
    70   "((x :: real) \<le> x + y) = (0 \<le> y)"
    71   by simp
    72 
    73 lemma REAL_LE_ADDL:
    74   "((y :: real) \<le> x + y) = (0 \<le> x)"
    75   by simp
    76 
    77 lemma REAL_LT_ADDR:
    78   "((x :: real) < x + y) = (0 < y)"
    79   by simp
    80 
    81 lemma REAL_LT_ADDL:
    82   "((y :: real) < x + y) = (0 < x)"
    83   by simp
    84 
    85 lemma REAL_SUB_SUB:
    86   "(x :: real) - y - x = - y"
    87   by simp
    88 
    89 lemma REAL_SUB_LNEG:
    90   "- (x :: real) - y = - (x + y)"
    91   by simp
    92 
    93 lemma REAL_SUB_NEG2:
    94   "- (x :: real) - - y = y - x"
    95   by simp
    96 
    97 lemma REAL_SUB_TRIANGLE:
    98   "(a :: real) - b + (b - c) = a - c"
    99   by simp
   100 
   101 lemma REAL_SUB_SUB2:
   102   "(x :: real) - (x - y) = y"
   103   by simp
   104 
   105 lemma REAL_ADD_SUB2:
   106   "(x :: real) - (x + y) = - y"
   107   by simp
   108 
   109 lemma REAL_POS_NZ:
   110   "0 < (x :: real) \<longrightarrow> x \<noteq> 0"
   111   by simp
   112 
   113 lemma REAL_DIFFSQ:
   114   "((x :: real) + y) * (x - y) = x * x - y * y"
   115   by (simp add: comm_semiring_1_class.normalizing_semiring_rules(7) right_distrib mult_diff_mult)
   116 
   117 lemma REAL_ABS_TRIANGLE_LE:
   118   "abs (x :: real) + abs (y - x) \<le> z \<longrightarrow> abs y \<le> z"
   119   by auto
   120 
   121 lemma REAL_ABS_TRIANGLE_LT:
   122   "abs (x :: real) + abs (y - x) < z \<longrightarrow> abs y < z"
   123   by auto
   124 
   125 lemma REAL_ABS_REFL:
   126   "(abs (x :: real) = x) = (0 \<le> x)"
   127   by auto
   128 
   129 lemma REAL_ABS_BETWEEN:
   130   "(0 < (d :: real) \<and> x - d < y \<and> y < x + d) = (abs (y - x) < d)"
   131   by auto
   132 
   133 lemma REAL_ABS_BOUND:
   134   "abs ((x :: real) - y) < d \<longrightarrow> y < x + d"
   135   by auto
   136 
   137 lemma REAL_ABS_STILLNZ:
   138   "abs ((x :: real) - y) < abs y \<longrightarrow> x \<noteq> 0"
   139   by auto
   140 
   141 lemma REAL_ABS_CASES:
   142   "(x :: real) = 0 \<or> 0 < abs x"
   143   by simp
   144 
   145 lemma REAL_ABS_BETWEEN1:
   146   "(x :: real) < z \<and> abs (y - x) < z - x \<longrightarrow> y < z"
   147   by auto
   148 
   149 lemma REAL_ABS_SIGN:
   150   "abs ((x :: real) - y) < y \<longrightarrow> 0 < x"
   151   by auto
   152 
   153 lemma REAL_ABS_SIGN2:
   154   "abs ((x :: real) - y) < - y \<longrightarrow> x < 0"
   155   by auto
   156 
   157 lemma REAL_ABS_CIRCLE:
   158   "abs (h :: real) < abs y - abs x \<longrightarrow> abs (x + h) < abs y"
   159   by auto
   160 
   161 lemma REAL_BOUNDS_LT:
   162   "(- (k :: real) < x \<and> x < k) = (abs x < k)"
   163   by auto
   164 
   165 lemma REAL_MIN_MAX:
   166   "min (x :: real) y = - max (- x) (- y)"
   167   by auto
   168 
   169 lemma REAL_MAX_MIN:
   170   "max (x :: real) y = - min (- x) (- y)"
   171   by auto
   172 
   173 lemma REAL_MAX_MAX:
   174   "(x :: real) \<le> max x y \<and> y \<le> max x y"
   175   by simp
   176 
   177 lemma REAL_MIN_MIN:
   178   "min (x :: real) y \<le> x \<and> min x y \<le> y"
   179   by simp
   180 
   181 lemma REAL_MAX_ACI:
   182   "max (x :: real) y = max y x \<and>
   183    max (max x y) z = max x (max y z) \<and>
   184    max x (max y z) = max y (max x z) \<and> max x x = x \<and> max x (max x y) = max x y"
   185   by auto
   186 
   187 
   188 lemma REAL_MIN_ACI:
   189   "min (x :: real) y = min y x \<and>
   190    min (min x y) z = min x (min y z) \<and>
   191    min x (min y z) = min y (min x z) \<and> min x x = x \<and> min x (min x y) = min x y"
   192   by auto
   193 
   194 lemma REAL_EQ_MUL_RCANCEL:
   195   "((x :: real) * z = y * z) = (x = y \<or> z = 0)"
   196   by auto
   197 
   198 lemma REAL_MUL_LINV_UNIQ:
   199   "(x :: real) * y = 1 \<longrightarrow> inverse y = x"
   200   by (metis inverse_inverse_eq inverse_unique)
   201 
   202 lemma REAL_DIV_RMUL:
   203   "(y :: real) \<noteq> 0 \<longrightarrow> x / y * y = x"
   204   by simp
   205 
   206 lemma REAL_DIV_LMUL:
   207   "(y :: real) \<noteq> 0 \<longrightarrow> y * (x / y) = x"
   208   by simp
   209 
   210 lemma REAL_LT_IMP_NZ:
   211   "0 < (x :: real) \<longrightarrow> x \<noteq> 0"
   212   by simp
   213 
   214 lemma REAL_LT_LCANCEL_IMP:
   215   "0 < (x :: real) \<and> x * y < x * z \<longrightarrow> y < z"
   216   by (auto simp add: mult_less_cancel_left_disj not_less_iff_gr_or_eq)
   217 
   218 lemma REAL_LT_RCANCEL_IMP:
   219   "0 < (z :: real) \<and> x * z < y * z \<longrightarrow> x < y"
   220   by (auto simp add: mult_less_cancel_left_disj not_less_iff_gr_or_eq)
   221 
   222 lemma REAL_MUL_POS_LE:
   223   "(0 \<le> (x :: real) * y) = (x = 0 \<or> y = 0 \<or> 0 < x \<and> 0 < y \<or> x < 0 \<and> y < 0)"
   224   by (metis less_eq_real_def mult_eq_0_iff zero_le_mult_iff)
   225 
   226 lemma REAL_EQ_RDIV_EQ:
   227   "0 < (z :: real) \<longrightarrow> (x = y / z) = (x * z = y)"
   228   by auto
   229 
   230 lemma REAL_EQ_LDIV_EQ:
   231   "0 < (z :: real) \<longrightarrow> (x / z = y) = (x = y * z)"
   232   by auto
   233 
   234 lemma REAL_SUB_INV:
   235   "(x :: real) \<noteq> 0 \<and> y \<noteq> 0 \<longrightarrow> inverse x - inverse y = (y - x) / (x * y)"
   236   by (simp add: division_ring_inverse_diff divide_real_def)
   237 
   238 lemma REAL_DOWN:
   239   "0 < (d :: real) \<longrightarrow> (\<exists>e>0. e < d)"
   240   by (intro impI exI[of _ "d / 2"]) simp
   241 
   242 lemma REAL_POW_MONO_LT:
   243   "1 < (x :: real) \<and> m < n \<longrightarrow> x ^ m < x ^ n"
   244   by simp
   245 
   246 lemma REAL_POW_MONO:
   247   "1 \<le> (x :: real) \<and> m \<le> n \<longrightarrow> x ^ m \<le> x ^ n"
   248   by (cases "m < n", cases "x = 1") auto
   249 
   250 lemma REAL_EQ_LCANCEL_IMP:
   251   "(z :: real) \<noteq> 0 \<and> z * x = z * y \<longrightarrow> x = y"
   252   by auto
   253 
   254 lemma REAL_LE_DIV:
   255   "0 \<le> (x :: real) \<and> 0 \<le> y \<longrightarrow> 0 \<le> x / y"
   256   by (simp add: zero_le_divide_iff)
   257 
   258 lemma REAL_10: "(1::real) \<noteq> 0"
   259   by simp
   260 
   261 lemma REAL_ADD_ASSOC: "(x::real) + (y + z) = x + y + z"
   262   by simp
   263 
   264 lemma REAL_MUL_ASSOC: "(x::real) * (y * z) = x * y * z"
   265   by simp
   266 
   267 lemma REAL_ADD_LINV:  "-x + x = (0::real)"
   268   by simp
   269 
   270 lemma REAL_MUL_LINV: "x \<noteq> (0::real) \<Longrightarrow> inverse x * x = 1"
   271   by simp
   272 
   273 lemma REAL_LT_TOTAL: "((x::real) = y) \<or> x < y \<or> y < x"
   274   by auto
   275 
   276 lemma real_lte: "((x::real) \<le> y) = (\<not>(y < x))"
   277   by auto
   278 
   279 lemma real_of_num: "((0::real) = 0) \<and> (!n. real (Suc n) = real n + 1)"
   280   by (simp add: real_of_nat_Suc)
   281 
   282 lemma abs: "abs (x::real) = (if 0 \<le> x then x else -x)"
   283   by (simp add: abs_if)
   284 
   285 lemma pow: "(!x::real. x ^ 0 = 1) \<and> (!x::real. \<forall>n. x ^ (Suc n) = x * x ^ n)"
   286   by simp
   287 
   288 lemma REAL_POLY_CLAUSES:
   289   "(\<forall>(x :: real) y z. x + (y + z) = x + y + z) \<and>
   290    (\<forall>(x :: real) y. x + y = y + x) \<and>
   291    (\<forall>(x :: real). 0 + x = x) \<and>
   292    (\<forall>(x :: real) y z. x * (y * z) = x * y * z) \<and>
   293    (\<forall>(x :: real) y. x * y = y * x) \<and>
   294    (\<forall>(x :: real). 1 * x = x) \<and>
   295    (\<forall>(x :: real). 0 * x = 0) \<and>
   296    (\<forall>(x :: real) y z. x * (y + z) = x * y + x * z) \<and>
   297    (\<forall>(x :: real). x ^ 0 = 1) \<and> (\<forall>(x :: real) n. x ^ Suc n = x * x ^ n)"
   298   by (auto simp add: right_distrib)
   299 
   300 lemma REAL_COMPLETE:
   301   "(\<exists>(x :: real). P x) \<and> (\<exists>(M :: real). \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
   302    (\<exists>M. (\<forall>x. P x \<longrightarrow> x \<le> M) \<and>
   303           (\<forall>M'. (\<forall>x. P x \<longrightarrow> x \<le> M') \<longrightarrow> M \<le> M'))"
   304   using complete_real[unfolded Ball_def, of "Collect P"] by auto
   305 
   306 lemma REAL_COMPLETE_SOMEPOS:
   307   "(\<exists>(x :: real). P x \<and> 0 \<le> x) \<and> (\<exists>M. \<forall>x. P x \<longrightarrow> x \<le> M) \<longrightarrow>
   308    (\<exists>M. (\<forall>x. P x \<longrightarrow> x \<le> M) \<and>
   309           (\<forall>M'. (\<forall>x. P x \<longrightarrow> x \<le> M') \<longrightarrow> M \<le> M'))"
   310   using REAL_COMPLETE by auto
   311 
   312 lemma REAL_ADD_AC:
   313   "(m :: real) + n = n + m \<and> m + n + p = m + (n + p) \<and> m + (n + p) = n + (m + p)"
   314   by simp
   315 
   316 lemma REAL_LE_RNEG:
   317   "((x :: real) \<le> - y) = (x + y \<le> 0)"
   318   by auto
   319 
   320 lemma REAL_LE_NEGTOTAL:
   321   "0 \<le> (x :: real) \<or> 0 \<le> - x"
   322   by auto
   323 
   324 lemma DEF_real_sgn:
   325   "sgn = (\<lambda>u. if (0 :: real) < u then 1 else if u < 0 then - 1 else 0)"
   326   by (simp add: ext)
   327 
   328 end