Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Real/HahnBanach/Aux.thy
changeset 7656 2f18c0ffc348
parent 7566 c5a3f980a7af
child 7808 fd019ac3485f
equal deleted inserted replaced
7655:21b7b0fd41bd 7656:2f18c0ffc348 
     1 (*  Title:      HOL/Real/HahnBanach/Aux.thy
 
     1 (*  Title:      HOL/Real/HahnBanach/Aux.thy
 
     2     ID:         $Id$
 
     2     ID:         $Id$
 
     3     Author:     Gertrud Bauer, TU Munich
 
     3     Author:     Gertrud Bauer, TU Munich
 
     4 *)
 
     4 *)
 
     5 
     5 
     6 theory Aux = Real:;
 
     6 theory Aux = Real + Zorn:;
 
     7 
     7 
     8 theorems case = case_split_thm;  (* FIXME tmp *);
 
     8 lemmas [intro!!] = chainD; 
       
     9 lemmas chainE2 = chainD2 [elimify];
 
       
    10 lemmas [intro!!] = isLub_isUb;
 
     9 
    11 
    10 lemmas CollectE = CollectD [elimify];
 
       
    11 
       
    12 theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y";	    (*  <=  ~=  < *)
 
       
    13   by (simp! add: order_less_le);
 
       
    14 
    12 
    15 lemma le_max1: "x <= max x (y::'a::linorder)";
 
    13 lemma le_max1: "x <= max x (y::'a::linorder)";
 
    16   by (simp add: le_max_iff_disj[of x x y]);
 
    14   by (simp add: le_max_iff_disj[of x x y]);
 
    17 
    15 
    18 lemma le_max2: "y <= max x (y::'a::linorder)"; 
    16 lemma le_max2: "y <= max x (y::'a::linorder)"; 
    22   by (rule order_less_le[RS iffD1, RS conjunct2]);
 
    20   by (rule order_less_le[RS iffD1, RS conjunct2]);
 
    23 
    21 
    24 lemma Int_singletonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v";
 
    22 lemma Int_singletonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v";
 
    25   by (fast elim: equalityE);
 
    23   by (fast elim: equalityE);
 
    26 
    24 
    27 lemmas singletonE = singletonD[elimify];
 
       
    28 
       
    29 lemma real_add_minus_eq: "x - y = 0r ==> x = y";
 
    25 lemma real_add_minus_eq: "x - y = 0r ==> x = y";
 
    30 proof -;
 
    26 proof -;
 
    31   assume "x - y = 0r";
 
    27   assume "x - y = 0r";
 
    32   have "x + - y = x - y"; by simp;
 
    28   have "x + - y = x - y"; by simp;
 
    33   also; have "... = 0r"; .;
 
    29   also; have "... = 0r"; .;
 
    34   finally; have "x + - y = 0r"; .;
 
    30   finally; have "x + - y = 0r"; .;
 
    35   hence "x = - (- y)"; by (rule real_add_minus_eq_minus);
 
    31   hence "x = - (- y)"; by (rule real_add_minus_eq_minus);
 
    36   also; have "... = y"; by (simp!);
 
    32   also; have "... = y"; by simp;
 
    37   finally; show "x = y"; .;
 
    33   finally; show "x = y"; .;
 
    38 qed;
 
    34 qed;
 
    39 
    35 
    40 lemma rabs_minus_one: "rabs (- 1r) = 1r"; 
    36 lemma rabs_minus_one: "rabs (- 1r) = 1r"; 
    41 proof -; 
    37 proof -; 
    42   have "rabs (- 1r) = - (- 1r)"; 
    38   have "rabs (- 1r) = - (- 1r)"; 
    43   proof (rule rabs_minus_eqI2);
 
    39   proof (rule rabs_minus_eqI2);
 
    44     show "-1r < 0r";
 
    40     show "-1r < 0r";
 
    45       by (rule real_minus_zero_less_iff[RS iffD1], simp, rule real_zero_less_one);
 
    41       by (rule real_minus_zero_less_iff[RS iffD1], simp, rule real_zero_less_one);
 
    46   qed;
 
    42   qed;
 
    47   also; have "... = 1r"; by (simp!); 
    43   also; have "... = 1r"; by simp; 
    48   finally; show ?thesis; by (simp!);
 
    44   finally; show ?thesis; by simp;
 
    49 qed;
 
    45 qed;
 
    50 
    46 
    51 axioms real_mult_le_le_mono2: "[| 0r <= z; x <= y |] ==> x * z <= y * z";
 
    47 lemma real_mult_le_le_mono2: "[| 0r <= z; x <= y |] ==> x * z <= y * z";
 
       
    48 proof -;
 
       
    49   assume gz: "0r <= z" and ineq: "x <= y";
 
       
    50   hence "x < y | x = y"; by (force simp add: order_le_less);
 
       
    51   thus ?thesis;
 
       
    52   proof (elim disjE); 
       
    53     assume "x < y"; show ?thesis; by (rule real_mult_le_less_mono1);
 
       
    54   next; 
       
    55     assume "x = y"; 
       
    56     hence "x * z <= y * z"; by simp;
 
       
    57     thus ?thesis; by fast;
 
       
    58   qed;
 
       
    59 qed;
 
    52 
    60 
    53 axioms real_mult_less_le_anti: "[| z < 0r; x <= y |] ==> z * y <= z * x";
 
    61 lemma real_mult_less_le_anti: "[| z < 0r; x <= y |] ==> z * y <= z * x";
 
       
    62 proof -;
 
       
    63   assume lz: "z < 0r" and ineq: "x <= y";
 
       
    64   hence "0r < - z"; by simp;
 
       
    65   hence "0r <= - z"; by (rule real_less_imp_le);
 
       
    66   with ineq; have "(- z) * x <= (- z) * y"; by (simp add: real_mult_le_le_mono1);
 
       
    67   hence  "- (z * x) <= - (z * y)"; by (simp add: real_minus_mult_eq1 [RS sym]);
 
       
    68   thus ?thesis; by simp;
 
       
    69 qed;
 
    54 
    70 
    55 axioms real_mult_less_le_mono: "[| 0r < z; x <= y |] ==> z * x <= z * y";
 
    71 lemma real_mult_less_le_mono: "[| 0r < z; x <= y |] ==> z * x <= z * y";
 
       
    72 proof -; 
       
    73   assume gt: "0r < z" and ineq: "x <= y";
 
       
    74   from gt; have "0r <= z"; by (rule real_less_imp_le);
 
       
    75   thus ?thesis; by (rule real_mult_le_le_mono1); 
       
    76 qed;
 
    56 
    77 
    57 axioms real_mult_diff_distrib: "a * (- x - (y::real)) = - a * x - a * y";
 
    78 lemma real_mult_diff_distrib: "a * (- x - (y::real)) = - a * x - a * y";
 
       
    79 proof -;
 
       
    80   have "- x - (y::real) = - x + - y"; by simp;
 
       
    81   also; have "a * ... = a * - x + a * - y"; by (simp add: real_add_mult_distrib2);
 
       
    82   also; have "... = - a * x - a * y"; 
       
    83     by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1 [RS sym]);
 
       
    84   finally; show ?thesis; .;
 
       
    85 qed;
 
    58 
    86 
    59 axioms real_mult_diff_distrib2: "a * (x - (y::real)) = a * x - a * y";
 
    87 lemma real_mult_diff_distrib2: "a * (x - (y::real)) = a * x - a * y";
 
    60 
    88 proof -; 
    61 lemma less_imp_le: "(x::real) < y ==> x <= y";
 
    89   have "x - (y::real) = x + - y"; by simp;
 
    62   by (simp! only: real_less_imp_le);
 
    90   also; have "a * ... = a * x + a * - y"; by (simp add: real_add_mult_distrib2);
 
       
    91   also; have "... = a * x - a * y";   
       
    92     by (simp add: real_minus_mult_eq2 [RS sym] real_minus_mult_eq1 [RS sym]);
 
       
    93   finally; show ?thesis; .;
 
       
    94 qed;
 
    63 
    95 
    64 lemma le_noteq_imp_less: "[|x <= (r::'a::order); x ~= r |] ==> x < r";
 
    96 lemma le_noteq_imp_less: "[|x <= (r::'a::order); x ~= r |] ==> x < r";
 
    65 proof -;
 
    97 proof -;
 
    66   assume "x <= (r::'a::order)";
 
    98   assume "x <= (r::'a::order)" and ne:"x ~= r";
 
    67   assume "x ~= r";
 
    99   then; have "x < r | x = r"; by (simp add: order_le_less);
 
    68   then; have "x < r | x = r";
 
   100   with ne; show ?thesis; by simp;
 
    69     by (simp! add: order_le_less);
 
       
    70   then; show ?thesis;
 
       
    71     by (simp!);
 
       
    72 qed;
 
   101 qed;
 
    73 
   102 
    74 lemma minus_le: "- (x::real) <= y ==> - y <= x";
 
   103 lemma minus_le: "- (x::real) <= y ==> - y <= x";
 
    75 proof -; 
   104 proof -; 
    76   assume "- x <= y";
 
   105   assume "- x <= y";
 
    78   thus "-y <= x";
 
   107   thus "-y <= x";
 
    79   proof;
 
   108   proof;
 
    80      assume "- x < y"; show ?thesis; 
   109      assume "- x < y"; show ?thesis; 
    81      proof -; 
   110      proof -; 
    82        have "- y < - (- x)"; by (rule real_less_swap_iff [RS iffD1]); 
   111        have "- y < - (- x)"; by (rule real_less_swap_iff [RS iffD1]); 
    83        hence "- y < x"; by (simp!);
 
   112        hence "- y < x"; by simp;
 
    84        thus ?thesis; by (rule real_less_imp_le);
 
   113        thus ?thesis; by (rule real_less_imp_le);
 
    85     qed;
 
   114     qed;
 
    86   next; 
   115   next; 
    87      assume "- x = y"; show ?thesis; by (force!);
 
   116      assume "- x = y"; thus ?thesis; by force;
 
    88   qed;
 
   117   qed;
 
    89 qed;
 
   118 qed;
 
    90 
   119 
    91 lemma rabs_interval_iff_1: "(rabs (x::real) <= r) = (-r <= x & x <= r)";
 
   120 lemma rabs_interval_iff_1: "(rabs (x::real) <= r) = (-r <= x & x <= r)";
 
    92 proof (rule case [of "rabs x = r"]);
 
   121 proof (rule case_split [of "rabs x = r"]);
 
    93   assume  a: "rabs x = r";
 
   122   assume  a: "rabs x = r";
 
    94   show ?thesis; 
   123   show ?thesis; 
    95   proof;
 
   124   proof;
 
    96     assume "rabs x <= r";
 
   125     assume "rabs x <= r";
 
    97     show "- r <= x & x <= r";
 
   126     show "- r <= x & x <= r";
 
    98     proof;
 
   127     proof;
 
    99       have "- x <= rabs x"; by (rule rabs_ge_minus_self);
 
   128       have "- x <= rabs x"; by (rule rabs_ge_minus_self);
 
   100       hence "- x <= r"; by (simp!);
 
   129       with a; have "- x <= r"; by simp;
 
   101       thus "- r <= x"; by (simp! add : minus_le [of "x" "r"]);
 
   130       thus "- r <= x"; by (simp add : minus_le [of "x" "r"]);
 
   102       have "x <= rabs x"; by (rule rabs_ge_self); 
   131       have "x <= rabs x"; by (rule rabs_ge_self); 
   103       thus "x <= r"; by (simp!); 
   132       with a; show "x <= r"; by simp; 
   104     qed;
 
   133     qed;
 
   105   next; 
   134   next; 
   106     assume "- r <= x & x <= r";
 
   135     assume "- r <= x & x <= r";
 
   107     show "rabs x <= r"; by (fast!);
 
   136     with a; show "rabs x <= r"; by fast;
 
   108   qed;
 
   137   qed;
 
   109 next;   
   138 next;   
   110   assume "rabs x ~= r";
 
   139   assume "rabs x ~= r";
 
   111   show ?thesis; 
   140   show ?thesis; 
   112   proof;
 
   141   proof;
 
   122     qed;
 
   151     qed;
 
   123   next;
 
   152   next;
 
   124     assume "- r <= x & x <= r";
 
   153     assume "- r <= x & x <= r";
 
   125     thus "rabs x <= r";
 
   154     thus "rabs x <= r";
 
   126     proof; 
   155     proof; 
   127       assume "- r <= x" "x <= r";
 
   156       assume a: "- r <= x" and "x <= r";
 
   128       show ?thesis; 
   157       show ?thesis; 
   129       proof (rule rabs_disj [RS disjE, of x]);
 
   158       proof (rule rabs_disj [RS disjE, of x]);
 
   130         assume  "rabs x = x";
 
   159         assume "rabs x = x";
 
   131         show ?thesis; by (simp!); 
   160         thus ?thesis; by simp; 
   132       next; 
   161       next; 
   133         assume "rabs x = - x";
 
   162         assume "rabs x = - x";
 
   134         from minus_le [of r x]; show ?thesis; by (simp!);
 
   163         with a minus_le [of r x]; show ?thesis; by simp;
 
   135       qed;
 
   164       qed;
 
   136     qed;
 
   165     qed;
 
   137   qed;
 
   166   qed;
 
   138 qed;
 
   167 qed;
 
   139 
   168 
   140 lemma set_less_imp_diff_not_empty: "H < E ==> EX x0:E. x0 ~: H";
 
   169 
   141 proof- ;
 
   170 lemma real_diff_ineq_swap: "(d::real) - b <= c + a ==> - a - b <= c - d";
 
   142   assume "H < E ";
 
   171 proof -;
 
   143   have le: "H <= E"; by (rule conjunct1 [OF psubset_eq[RS iffD1]]);
 
   172   assume "d - b <= c + (a::real)";
 
   144   have ne: "H ~= E";  by (rule conjunct2 [OF psubset_eq[RS iffD1]]);
 
   173   have "- a - b = d - b + (- d - a)"; by (simp!);
 
   145   with le; show ?thesis; by force;
 
   174   also; have "... <= c + a + (- d - a)"; by (rule real_add_le_mono1);
 
       
   175   also; have "... = c - d"; by (simp!);
 
       
   176   finally; show "- a - b <= c - d"; .;
 
   146 qed;
 
   177 qed;
 
   147 
   178 
   148 
   179 
       
   180 lemma set_less_imp_diff_not_empty: "H < E ==> EX x0:E. x0 ~: H";
 
       
   181  by (force simp add: psubset_eq);
 
       
   182 
       
   183 
   149 end;
 
   184 end;
isabelle