src/HOL/Real/HahnBanach/Aux.thy
author wenzelm
Sun Jul 23 12:01:05 2000 +0200 (2000-07-23)
changeset 9408 d3d56e1d2ec1
parent 9394 1ff8a6234c6a
child 9503 3324cbbecef8
permissions -rw-r--r--
classical atts now intro! / intro / intro?;
wenzelm@7566
     1
(*  Title:      HOL/Real/HahnBanach/Aux.thy
wenzelm@7566
     2
    ID:         $Id$
wenzelm@7566
     3
    Author:     Gertrud Bauer, TU Munich
wenzelm@7566
     4
*)
wenzelm@7535
     5
wenzelm@9035
     6
header {* Auxiliary theorems *}
wenzelm@7808
     7
wenzelm@9035
     8
theory Aux = Real + Zorn:
wenzelm@7566
     9
wenzelm@7917
    10
text {* Some existing theorems are declared as extra introduction
wenzelm@9035
    11
or elimination rules, respectively. *}
wenzelm@7917
    12
wenzelm@9408
    13
lemmas [intro?] = isLub_isUb
wenzelm@9408
    14
lemmas [intro?] = chainD 
wenzelm@9035
    15
lemmas chainE2 = chainD2 [elimify]
wenzelm@7917
    16
wenzelm@9035
    17
text_raw {* \medskip *}
wenzelm@9035
    18
text{* Lemmas about sets. *}
wenzelm@7917
    19
bauerg@9379
    20
lemma Int_singletonD: "[| A \\<inter> B = {v}; x \\<in> A; x \\<in> B |] ==> x = v"
wenzelm@9035
    21
  by (fast elim: equalityE)
wenzelm@7917
    22
bauerg@9379
    23
lemma set_less_imp_diff_not_empty: "H < E ==> \\<exists>x0 \\<in> E. x0 \\<notin> H"
bauerg@9379
    24
  by (force simp add: psubset_eq)
wenzelm@7917
    25
wenzelm@9035
    26
text_raw {* \medskip *}
wenzelm@9035
    27
text{* Some lemmas about orders. *}
wenzelm@7535
    28
bauerg@9379
    29
lemma lt_imp_not_eq: "x < (y::'a::order) ==> x \\<noteq> y"
bauerg@9379
    30
  by (simp add: order_less_le)
wenzelm@7917
    31
wenzelm@7917
    32
lemma le_noteq_imp_less: 
bauerg@9379
    33
  "[| x <= (r::'a::order); x \\<noteq> r |] ==> x < r"
wenzelm@9035
    34
proof -
bauerg@9379
    35
  assume "x <= r" and ne:"x \\<noteq> r"
wenzelm@9035
    36
  hence "x < r | x = r" by (simp add: order_le_less)
wenzelm@9035
    37
  with ne show ?thesis by simp
wenzelm@9035
    38
qed
wenzelm@7917
    39
wenzelm@9035
    40
text_raw {* \medskip *}
wenzelm@9035
    41
text{* Some lemmas for the reals. *}
wenzelm@7535
    42
wenzelm@9035
    43
lemma real_add_minus_eq: "x - y = (#0::real) ==> x = y"
wenzelm@9035
    44
  by simp
fleuriot@9013
    45
wenzelm@9035
    46
lemma abs_minus_one: "abs (- (#1::real)) = #1" 
wenzelm@9035
    47
  by simp
fleuriot@9013
    48
fleuriot@9013
    49
lemma real_mult_le_le_mono1a: 
wenzelm@9035
    50
  "[| (#0::real) <= z; x <= y |] ==> z * x  <= z * y"
wenzelm@9035
    51
proof -
bauerg@9256
    52
  assume z: "(#0::real) <= z" and "x <= y"
wenzelm@9035
    53
  hence "x < y | x = y" by (force simp add: order_le_less)
wenzelm@9035
    54
  thus ?thesis
wenzelm@9035
    55
  proof (elim disjE) 
wenzelm@9394
    56
    assume "x < y" show ?thesis by  (rule real_mult_le_less_mono2) simp
wenzelm@9035
    57
  next 
wenzelm@9394
    58
    assume "x = y" thus ?thesis by simp
wenzelm@9035
    59
  qed
wenzelm@9035
    60
qed
wenzelm@7656
    61
wenzelm@7808
    62
lemma real_mult_le_le_mono2: 
wenzelm@9035
    63
  "[| (#0::real) <= z; x <= y |] ==> x * z <= y * z"
wenzelm@9035
    64
proof -
wenzelm@9035
    65
  assume "(#0::real) <= z" "x <= y"
wenzelm@9035
    66
  hence "x < y | x = y" by (force simp add: order_le_less)
wenzelm@9035
    67
  thus ?thesis
wenzelm@9035
    68
  proof (elim disjE) 
wenzelm@9394
    69
    assume "x < y" show ?thesis by (rule real_mult_le_less_mono1) simp
wenzelm@9035
    70
  next 
wenzelm@9394
    71
    assume "x = y" thus ?thesis by simp
wenzelm@9035
    72
  qed
wenzelm@9035
    73
qed
wenzelm@7535
    74
wenzelm@7808
    75
lemma real_mult_less_le_anti: 
wenzelm@9035
    76
  "[| z < (#0::real); x <= y |] ==> z * y <= z * x"
wenzelm@9035
    77
proof -
wenzelm@9035
    78
  assume "z < #0" "x <= y"
wenzelm@9035
    79
  hence "#0 < - z" by simp
wenzelm@9035
    80
  hence "#0 <= - z" by (rule real_less_imp_le)
wenzelm@9035
    81
  hence "x * (- z) <= y * (- z)" 
wenzelm@9035
    82
    by (rule real_mult_le_le_mono2)
wenzelm@9035
    83
  hence  "- (x * z) <= - (y * z)" 
wenzelm@9035
    84
    by (simp only: real_minus_mult_eq2)
wenzelm@9035
    85
  thus ?thesis by (simp only: real_mult_commute)
wenzelm@9035
    86
qed
fleuriot@9013
    87
fleuriot@9013
    88
lemma real_mult_less_le_mono: 
wenzelm@9035
    89
  "[| (#0::real) < z; x <= y |] ==> z * x <= z * y"
wenzelm@9035
    90
proof - 
wenzelm@9035
    91
  assume "#0 < z" "x <= y"
wenzelm@9035
    92
  have "#0 <= z" by (rule real_less_imp_le)
wenzelm@9035
    93
  hence "x * z <= y * z" 
wenzelm@9035
    94
    by (rule real_mult_le_le_mono2)
wenzelm@9035
    95
  thus ?thesis by (simp only: real_mult_commute)
wenzelm@9035
    96
qed
fleuriot@9013
    97
wenzelm@9394
    98
lemma real_rinv_gt_zero1: "#0 < x ==> #0 < rinv x"
wenzelm@9394
    99
proof - 
wenzelm@9394
   100
  assume "#0 < x"
wenzelm@9394
   101
  have "0 < x" by simp
wenzelm@9394
   102
  hence "0 < rinv x" by (rule real_rinv_gt_zero)
wenzelm@9394
   103
  thus ?thesis by simp
wenzelm@9394
   104
qed
wenzelm@7535
   105
bauerg@9379
   106
lemma real_mult_inv_right1: "x \\<noteq> #0 ==> x*rinv(x) = #1"
wenzelm@9394
   107
  by simp
fleuriot@9013
   108
bauerg@9379
   109
lemma real_mult_inv_left1: "x \\<noteq> #0 ==> rinv(x) * x = #1"
wenzelm@9394
   110
  by simp
fleuriot@9013
   111
fleuriot@9013
   112
lemma real_le_mult_order1a: 
wenzelm@9394
   113
  "[| (#0::real) <= x; #0 <= y |] ==> #0 <= x * y"
wenzelm@9035
   114
proof -
wenzelm@9035
   115
  assume "#0 <= x" "#0 <= y"
wenzelm@9394
   116
  have "[|0 <= x; 0 <= y|] ==> 0 <= x * y"  
wenzelm@9394
   117
    by (rule real_le_mult_order)
wenzelm@9394
   118
  thus ?thesis by (simp!)
wenzelm@9035
   119
qed
wenzelm@7535
   120
wenzelm@7808
   121
lemma real_mult_diff_distrib: 
wenzelm@9035
   122
  "a * (- x - (y::real)) = - a * x - a * y"
wenzelm@9035
   123
proof -
wenzelm@9035
   124
  have "- x - y = - x + - y" by simp
wenzelm@9035
   125
  also have "a * ... = a * - x + a * - y" 
wenzelm@9035
   126
    by (simp only: real_add_mult_distrib2)
wenzelm@9035
   127
  also have "... = - a * x - a * y" 
wenzelm@9394
   128
    by simp
wenzelm@9035
   129
  finally show ?thesis .
wenzelm@9035
   130
qed
wenzelm@7535
   131
wenzelm@9035
   132
lemma real_mult_diff_distrib2: "a * (x - (y::real)) = a * x - a * y"
wenzelm@9035
   133
proof - 
wenzelm@9035
   134
  have "x - y = x + - y" by simp
wenzelm@9035
   135
  also have "a * ... = a * x + a * - y" 
wenzelm@9035
   136
    by (simp only: real_add_mult_distrib2)
wenzelm@9035
   137
  also have "... = a * x - a * y"   
wenzelm@9394
   138
    by simp
wenzelm@9035
   139
  finally show ?thesis .
wenzelm@9035
   140
qed
wenzelm@7535
   141
wenzelm@9035
   142
lemma real_minus_le: "- (x::real) <= y ==> - y <= x"
wenzelm@9035
   143
  by simp
wenzelm@7535
   144
wenzelm@7808
   145
lemma real_diff_ineq_swap: 
wenzelm@9394
   146
    "(d::real) - b <= c + a ==> - a - b <= c - d"
wenzelm@9035
   147
  by simp
wenzelm@7535
   148
wenzelm@9035
   149
end