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