src/HOL/Real/HahnBanach/Aux.thy
changeset 7566 c5a3f980a7af
parent 7535 599d3414b51d
child 7656 2f18c0ffc348
     1.1 --- a/src/HOL/Real/HahnBanach/Aux.thy	Tue Sep 21 17:30:55 1999 +0200
     1.2 +++ b/src/HOL/Real/HahnBanach/Aux.thy	Tue Sep 21 17:31:20 1999 +0200
     1.3 @@ -1,16 +1,31 @@
     1.4 +(*  Title:      HOL/Real/HahnBanach/Aux.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Gertrud Bauer, TU Munich
     1.7 +*)
     1.8  
     1.9 -theory Aux = Main + Real:;
    1.10 +theory Aux = Real:;
    1.11  
    1.12 +theorems case = case_split_thm;  (* FIXME tmp *);
    1.13 +
    1.14 +lemmas CollectE = CollectD [elimify];
    1.15  
    1.16  theorem [trans]: "[| (x::'a::order) <= y; x ~= y |] ==> x < y";	    (*  <=  ~=  < *)
    1.17 -  by (asm_simp add: order_less_le);
    1.18 +  by (simp! add: order_less_le);
    1.19 +
    1.20 +lemma le_max1: "x <= max x (y::'a::linorder)";
    1.21 +  by (simp add: le_max_iff_disj[of x x y]);
    1.22 +
    1.23 +lemma le_max2: "y <= max x (y::'a::linorder)"; 
    1.24 +  by (simp add: le_max_iff_disj[of y x y]);
    1.25  
    1.26  lemma lt_imp_not_eq: "x < (y::'a::order) ==> x ~= y"; 
    1.27    by (rule order_less_le[RS iffD1, RS conjunct2]);
    1.28  
    1.29 -lemma Int_singeltonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v";
    1.30 +lemma Int_singletonD: "[| A Int B = {v}; x:A; x:B |] ==> x = v";
    1.31    by (fast elim: equalityE);
    1.32  
    1.33 +lemmas singletonE = singletonD[elimify];
    1.34 +
    1.35  lemma real_add_minus_eq: "x - y = 0r ==> x = y";
    1.36  proof -;
    1.37    assume "x - y = 0r";
    1.38 @@ -18,7 +33,7 @@
    1.39    also; have "... = 0r"; .;
    1.40    finally; have "x + - y = 0r"; .;
    1.41    hence "x = - (- y)"; by (rule real_add_minus_eq_minus);
    1.42 -  also; have "... = y"; by asm_simp;
    1.43 +  also; have "... = y"; by (simp!);
    1.44    finally; show "x = y"; .;
    1.45  qed;
    1.46  
    1.47 @@ -29,8 +44,8 @@
    1.48      show "-1r < 0r";
    1.49        by (rule real_minus_zero_less_iff[RS iffD1], simp, rule real_zero_less_one);
    1.50    qed;
    1.51 -  also; have "... = 1r"; by asm_simp; 
    1.52 -  finally; show ?thesis; by asm_simp;
    1.53 +  also; have "... = 1r"; by (simp!); 
    1.54 +  finally; show ?thesis; by (simp!);
    1.55  qed;
    1.56  
    1.57  axioms real_mult_le_le_mono2: "[| 0r <= z; x <= y |] ==> x * z <= y * z";
    1.58 @@ -39,21 +54,21 @@
    1.59  
    1.60  axioms real_mult_less_le_mono: "[| 0r < z; x <= y |] ==> z * x <= z * y";
    1.61  
    1.62 -axioms real_mult_diff_distrib: "a * (- x - y) = - a * x - a * y";
    1.63 +axioms real_mult_diff_distrib: "a * (- x - (y::real)) = - a * x - a * y";
    1.64  
    1.65 -axioms real_mult_diff_distrib2: "a * (x - y) = a * x - a * y";
    1.66 +axioms real_mult_diff_distrib2: "a * (x - (y::real)) = a * x - a * y";
    1.67  
    1.68  lemma less_imp_le: "(x::real) < y ==> x <= y";
    1.69 -  by (asm_simp only: real_less_imp_le);
    1.70 +  by (simp! only: real_less_imp_le);
    1.71  
    1.72  lemma le_noteq_imp_less: "[|x <= (r::'a::order); x ~= r |] ==> x < r";
    1.73  proof -;
    1.74    assume "x <= (r::'a::order)";
    1.75    assume "x ~= r";
    1.76    then; have "x < r | x = r";
    1.77 -    by (asm_simp add: order_le_less);
    1.78 +    by (simp! add: order_le_less);
    1.79    then; show ?thesis;
    1.80 -    by asm_simp;
    1.81 +    by (simp!);
    1.82  qed;
    1.83  
    1.84  lemma minus_le: "- (x::real) <= y ==> - y <= x";
    1.85 @@ -65,11 +80,11 @@
    1.86       assume "- x < y"; show ?thesis; 
    1.87       proof -; 
    1.88         have "- y < - (- x)"; by (rule real_less_swap_iff [RS iffD1]); 
    1.89 -       hence "- y < x"; by asm_simp;
    1.90 +       hence "- y < x"; by (simp!);
    1.91         thus ?thesis; by (rule real_less_imp_le);
    1.92      qed;
    1.93    next; 
    1.94 -     assume "- x = y"; show ?thesis; by force;
    1.95 +     assume "- x = y"; show ?thesis; by (force!);
    1.96    qed;
    1.97  qed;
    1.98  
    1.99 @@ -82,14 +97,14 @@
   1.100      show "- r <= x & x <= r";
   1.101      proof;
   1.102        have "- x <= rabs x"; by (rule rabs_ge_minus_self);
   1.103 -      hence "- x <= r"; by asm_simp;
   1.104 -      thus "- r <= x"; by (asm_simp add : minus_le [of "x" "r"]);
   1.105 +      hence "- x <= r"; by (simp!);
   1.106 +      thus "- r <= x"; by (simp! add : minus_le [of "x" "r"]);
   1.107        have "x <= rabs x"; by (rule rabs_ge_self); 
   1.108 -      thus "x <= r"; by asm_simp; 
   1.109 +      thus "x <= r"; by (simp!); 
   1.110      qed;
   1.111    next; 
   1.112      assume "- r <= x & x <= r";
   1.113 -    show "rabs x <= r";  by fast;  
   1.114 +    show "rabs x <= r"; by (fast!);
   1.115    qed;
   1.116  next;   
   1.117    assume "rabs x ~= r";
   1.118 @@ -113,10 +128,10 @@
   1.119        show ?thesis; 
   1.120        proof (rule rabs_disj [RS disjE, of x]);
   1.121          assume  "rabs x = x";
   1.122 -        show ?thesis; by asm_simp; 
   1.123 +        show ?thesis; by (simp!); 
   1.124        next; 
   1.125          assume "rabs x = - x";
   1.126 -        from minus_le [of r x]; show ?thesis; by asm_simp;
   1.127 +        from minus_le [of r x]; show ?thesis; by (simp!);
   1.128        qed;
   1.129      qed;
   1.130    qed;