inserted Id: lines
authorpaulson
Mon Aug 16 18:41:32 1999 +0200 (1999-08-16)
changeset 72194e3f386c2e37
parent 7218 bfa767b4dc51
child 7220 da6f387ca482
inserted Id: lines
src/HOL/Real/Hyperreal/Filter.ML
src/HOL/Real/Hyperreal/Filter.thy
src/HOL/Real/Hyperreal/Zorn.ML
src/HOL/Real/Hyperreal/Zorn.thy
src/HOL/Real/Lubs.ML
src/HOL/Real/Lubs.thy
src/HOL/Real/PNat.ML
src/HOL/Real/PNat.thy
src/HOL/Real/PRat.ML
src/HOL/Real/PRat.thy
src/HOL/Real/PReal.ML
src/HOL/Real/PReal.thy
src/HOL/Real/RComplete.ML
src/HOL/Real/RComplete.thy
src/HOL/Real/ROOT.ML
src/HOL/Real/Real.ML
src/HOL/Real/Real.thy
src/HOL/Real/RealAbs.ML
src/HOL/Real/RealAbs.thy
src/HOL/Real/RealDef.ML
src/HOL/Real/RealDef.thy
src/HOL/Real/RealPow.ML
src/HOL/Real/RealPow.thy
     1.1 --- a/src/HOL/Real/Hyperreal/Filter.ML	Mon Aug 16 18:41:06 1999 +0200
     1.2 +++ b/src/HOL/Real/Hyperreal/Filter.ML	Mon Aug 16 18:41:32 1999 +0200
     1.3 @@ -1,4 +1,5 @@
     1.4  (*  Title       : Filter.ML
     1.5 +    ID          : $Id$
     1.6      Author      : Jacques D. Fleuriot
     1.7      Copyright   : 1998  University of Cambridge
     1.8      Description : Filters and Ultrafilter
     2.1 --- a/src/HOL/Real/Hyperreal/Filter.thy	Mon Aug 16 18:41:06 1999 +0200
     2.2 +++ b/src/HOL/Real/Hyperreal/Filter.thy	Mon Aug 16 18:41:32 1999 +0200
     2.3 @@ -1,4 +1,5 @@
     2.4  (*  Title       : Filter.thy
     2.5 +    ID          : $Id$
     2.6      Author      : Jacques D. Fleuriot
     2.7      Copyright   : 1998  University of Cambridge
     2.8      Description : Filters and Ultrafilters
     3.1 --- a/src/HOL/Real/Hyperreal/Zorn.ML	Mon Aug 16 18:41:06 1999 +0200
     3.2 +++ b/src/HOL/Real/Hyperreal/Zorn.ML	Mon Aug 16 18:41:32 1999 +0200
     3.3 @@ -1,11 +1,10 @@
     3.4  (*  Title       : Zorn.ML
     3.5 +    ID          : $Id$
     3.6      Author      : Jacques D. Fleuriot
     3.7      Copyright   : 1998  University of Cambridge
     3.8      Description : Zorn's Lemma -- adapted proofs from lcp's ZF/Zorn.ML
     3.9  *) 
    3.10  
    3.11 -open Zorn;
    3.12 -
    3.13  (*---------------------------------------------------------------
    3.14        Section 1.  Mathematical Preamble 
    3.15   ---------------------------------------------------------------*)
     4.1 --- a/src/HOL/Real/Hyperreal/Zorn.thy	Mon Aug 16 18:41:06 1999 +0200
     4.2 +++ b/src/HOL/Real/Hyperreal/Zorn.thy	Mon Aug 16 18:41:32 1999 +0200
     4.3 @@ -1,4 +1,5 @@
     4.4  (*  Title       : Zorn.thy
     4.5 +    ID          : $Id$
     4.6      Author      : Jacques D. Fleuriot
     4.7      Copyright   : 1998  University of Cambridge
     4.8      Description : Zorn's Lemma -- See lcp's Zorn.thy in ZF
     5.1 --- a/src/HOL/Real/Lubs.ML	Mon Aug 16 18:41:06 1999 +0200
     5.2 +++ b/src/HOL/Real/Lubs.ML	Mon Aug 16 18:41:32 1999 +0200
     5.3 @@ -1,12 +1,11 @@
     5.4  (*  Title       : Lubs.ML
     5.5 +    ID          : $Id$
     5.6      Author      : Jacques D. Fleuriot
     5.7      Copyright   : 1998  University of Cambridge
     5.8      Description : Completeness of the reals. A few of the 
     5.9                    definitions suggested by James Margetson
    5.10  *) 
    5.11  
    5.12 -open Lubs;
    5.13 -
    5.14  (*------------------------------------------------------------------------
    5.15                          Rules for *<= and <=*
    5.16   ------------------------------------------------------------------------*)
     6.1 --- a/src/HOL/Real/Lubs.thy	Mon Aug 16 18:41:06 1999 +0200
     6.2 +++ b/src/HOL/Real/Lubs.thy	Mon Aug 16 18:41:32 1999 +0200
     6.3 @@ -1,4 +1,5 @@
     6.4  (*  Title       : Lubs.thy
     6.5 +    ID          : $Id$
     6.6      Author      : Jacques D. Fleuriot
     6.7      Copyright   : 1998  University of Cambridge
     6.8      Description : Upper bounds, lubs definitions
     7.1 --- a/src/HOL/Real/PNat.ML	Mon Aug 16 18:41:06 1999 +0200
     7.2 +++ b/src/HOL/Real/PNat.ML	Mon Aug 16 18:41:32 1999 +0200
     7.3 @@ -1,12 +1,11 @@
     7.4  (*  Title       : PNat.ML
     7.5 +    ID          : $Id$
     7.6      Author      : Jacques D. Fleuriot
     7.7      Copyright   : 1998  University of Cambridge
     7.8      Description : The positive naturals -- proofs 
     7.9                  : mainly as in Nat.thy
    7.10  *)
    7.11  
    7.12 -open PNat;
    7.13 -
    7.14  Goal "mono(%X. {1} Un (Suc``X))";
    7.15  by (REPEAT (ares_tac [monoI, subset_refl, image_mono, Un_mono] 1));
    7.16  qed "pnat_fun_mono";
     8.1 --- a/src/HOL/Real/PNat.thy	Mon Aug 16 18:41:06 1999 +0200
     8.2 +++ b/src/HOL/Real/PNat.thy	Mon Aug 16 18:41:32 1999 +0200
     8.3 @@ -1,4 +1,5 @@
     8.4  (*  Title       : PNat.thy
     8.5 +    ID          : $Id$
     8.6      Author      : Jacques D. Fleuriot
     8.7      Copyright   : 1998  University of Cambridge
     8.8      Description : The positive naturals
     9.1 --- a/src/HOL/Real/PRat.ML	Mon Aug 16 18:41:06 1999 +0200
     9.2 +++ b/src/HOL/Real/PRat.ML	Mon Aug 16 18:41:32 1999 +0200
     9.3 @@ -1,18 +1,16 @@
     9.4  (*  Title       : PRat.ML
     9.5 +    ID          : $Id$
     9.6      Author      : Jacques D. Fleuriot
     9.7      Copyright   : 1998  University of Cambridge
     9.8      Description : The positive rationals
     9.9  *) 
    9.10  
    9.11 -open PRat;
    9.12 -
    9.13  Delrules [equalityI];
    9.14  
    9.15  (*** Many theorems similar to those in Integ.thy ***)
    9.16  (*** Proving that ratrel is an equivalence relation ***)
    9.17  
    9.18 -Goal
    9.19 -    "[| (x1::pnat) * y2 = x2 * y1; x2 * y3 = x3 * y2 |] \
    9.20 +Goal "[| (x1::pnat) * y2 = x2 * y1; x2 * y3 = x3 * y2 |] \
    9.21  \            ==> x1 * y3 = x3 * y1";        
    9.22  by (res_inst_tac [("k1","y2")] (pnat_mult_cancel1 RS iffD1) 1);
    9.23  by (auto_tac (claset(), simpset() addsimps [pnat_mult_assoc RS sym]));
    9.24 @@ -155,8 +153,7 @@
    9.25  by (auto_tac (claset(),simpset() addsimps [pnat_mult_assoc RS sym]));
    9.26  qed "prat_add_congruent2_lemma";
    9.27  
    9.28 -Goal 
    9.29 -    "congruent2 ratrel (%p1 p2.                  \
    9.30 +Goal "congruent2 ratrel (%p1 p2.                  \
    9.31  \         split (%x1 y1. split (%x2 y2. ratrel^^{(x1*y2 + x2*y1, y1*y2)}) p2) p1)";
    9.32  by (rtac (equiv_ratrel RS congruent2_commuteI) 1);
    9.33  by Safe_tac;
    9.34 @@ -451,8 +448,7 @@
    9.35  by (auto_tac (claset(),simpset() addsimps prat_add_ac));
    9.36  qed "prat_add_less2_mono1";
    9.37  
    9.38 -Goal  
    9.39 -      "!!(q1::prat). q1 < q2 ==> x + q1 < x + q2";
    9.40 +Goal "!!(q1::prat). q1 < q2 ==> x + q1 < x + q2";
    9.41  by (auto_tac (claset() addIs [prat_add_less2_mono1],
    9.42      simpset() addsimps [prat_add_commute]));
    9.43  qed "prat_add_less2_mono2";
    9.44 @@ -509,16 +505,14 @@
    9.45  by (asm_full_simp_tac (simpset() addsimps pnat_mult_ac) 1);
    9.46  qed "prat_linear";
    9.47  
    9.48 -Goal
    9.49 -    "!!(q1::prat). [| q1 < q2 ==> P;  q1 = q2 ==> P; \
    9.50 +Goal "!!(q1::prat). [| q1 < q2 ==> P;  q1 = q2 ==> P; \
    9.51  \          q2 < q1 ==> P |] ==> P";
    9.52  by (cut_inst_tac [("q1.0","q1"),("q2.0","q2")] prat_linear 1);
    9.53  by Auto_tac;
    9.54  qed "prat_linear_less2";
    9.55  
    9.56  (* Gleason p. 120 -- 9-2.6 (iv) *)
    9.57 -Goal 
    9.58 - "!!(q1::prat). [| q1 < q2; qinv(q1) = qinv(q2) |] ==> P";
    9.59 +Goal "!!(q1::prat). [| q1 < q2; qinv(q1) = qinv(q2) |] ==> P";
    9.60  by (cut_inst_tac [("x","qinv (q2)"),("q1.0","q1"),
    9.61     ("q2.0","q2")] prat_mult_less2_mono1 1);
    9.62  by (assume_tac 1);
    9.63 @@ -526,8 +520,7 @@
    9.64  by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
    9.65  qed "lemma1_qinv_prat_less";
    9.66  
    9.67 -Goal 
    9.68 - "!!(q1::prat). [| q1 < q2; qinv(q1) < qinv(q2) |] ==> P";
    9.69 +Goal "!!(q1::prat). [| q1 < q2; qinv(q1) < qinv(q2) |] ==> P";
    9.70  by (cut_inst_tac [("x","qinv (q2)"),("q1.0","q1"),
    9.71     ("q2.0","q2")] prat_mult_less2_mono1 1);
    9.72  by (assume_tac 1);
    9.73 @@ -539,8 +532,7 @@
    9.74      [prat_less_not_refl]));
    9.75  qed "lemma2_qinv_prat_less";
    9.76  
    9.77 -Goal 
    9.78 -      "!!(q1::prat). q1 < q2  ==> qinv (q2) < qinv (q1)";
    9.79 +Goal "!!(q1::prat). q1 < q2  ==> qinv (q2) < qinv (q1)";
    9.80  by (res_inst_tac [("q2.0","qinv q1"),
    9.81           ("q1.0","qinv q2")] prat_linear_less2 1);
    9.82  by (auto_tac (claset() addEs [lemma1_qinv_prat_less,
    9.83 @@ -693,8 +685,7 @@
    9.84      simpset() addsimps [prat_mult_commute]));
    9.85  qed "prat_mult_le2_mono1";
    9.86  
    9.87 -Goal 
    9.88 -      "!!(q1::prat). q1 <= q2  ==> qinv (q2) <= qinv (q1)";
    9.89 +Goal "!!(q1::prat). q1 <= q2  ==> qinv (q2) <= qinv (q1)";
    9.90  by (dtac prat_le_imp_less_or_eq 1);
    9.91  by (Step_tac 1);
    9.92  by (auto_tac (claset() addSIs [prat_le_refl,
    10.1 --- a/src/HOL/Real/PRat.thy	Mon Aug 16 18:41:06 1999 +0200
    10.2 +++ b/src/HOL/Real/PRat.thy	Mon Aug 16 18:41:32 1999 +0200
    10.3 @@ -1,4 +1,5 @@
    10.4  (*  Title       : PRat.thy
    10.5 +    ID          : $Id$
    10.6      Author      : Jacques D. Fleuriot
    10.7      Copyright   : 1998  University of Cambridge
    10.8      Description : The positive rationals
    11.1 --- a/src/HOL/Real/PReal.ML	Mon Aug 16 18:41:06 1999 +0200
    11.2 +++ b/src/HOL/Real/PReal.ML	Mon Aug 16 18:41:32 1999 +0200
    11.3 @@ -1,4 +1,5 @@
    11.4  (*  Title       : PReal.ML
    11.5 +    ID          : $Id$
    11.6      Author      : Jacques D. Fleuriot
    11.7      Copyright   : 1998  University of Cambridge
    11.8      Description : The positive reals as Dedekind sections of positive
    11.9 @@ -8,8 +9,6 @@
   11.10  
   11.11  claset_ref() := claset() delWrapper "bspec";
   11.12  
   11.13 -open PReal;
   11.14 -
   11.15  Goal "inj_on Abs_preal preal";
   11.16  by (rtac inj_on_inverseI 1);
   11.17  by (etac Abs_preal_inverse 1);
    12.1 --- a/src/HOL/Real/PReal.thy	Mon Aug 16 18:41:06 1999 +0200
    12.2 +++ b/src/HOL/Real/PReal.thy	Mon Aug 16 18:41:32 1999 +0200
    12.3 @@ -1,4 +1,5 @@
    12.4 -(*   Title       : PReal.thy
    12.5 +(*  Title       : PReal.thy
    12.6 +    ID          : $Id$
    12.7      Author      : Jacques D. Fleuriot
    12.8      Copyright   : 1998  University of Cambridge
    12.9      Description : The positive reals as Dedekind sections of positive
    13.1 --- a/src/HOL/Real/RComplete.ML	Mon Aug 16 18:41:06 1999 +0200
    13.2 +++ b/src/HOL/Real/RComplete.ML	Mon Aug 16 18:41:32 1999 +0200
    13.3 @@ -1,4 +1,5 @@
    13.4  (*  Title       : RComplete.thy
    13.5 +    ID          : $Id$
    13.6      Author      : Jacques D. Fleuriot
    13.7      Copyright   : 1998  University of Cambridge
    13.8      Description : Completeness theorems for positive
    14.1 --- a/src/HOL/Real/RComplete.thy	Mon Aug 16 18:41:06 1999 +0200
    14.2 +++ b/src/HOL/Real/RComplete.thy	Mon Aug 16 18:41:32 1999 +0200
    14.3 @@ -1,4 +1,5 @@
    14.4  (*  Title       : RComplete.thy
    14.5 +    ID          : $Id$
    14.6      Author      : Jacques D. Fleuriot
    14.7      Copyright   : 1998  University of Cambridge
    14.8      Description : Completeness theorems for positive
    15.1 --- a/src/HOL/Real/ROOT.ML	Mon Aug 16 18:41:06 1999 +0200
    15.2 +++ b/src/HOL/Real/ROOT.ML	Mon Aug 16 18:41:32 1999 +0200
    15.3 @@ -14,3 +14,4 @@
    15.4  time_use_thy "RealAbs";
    15.5  time_use_thy "RComplete";
    15.6  time_use_thy "Hyperreal/Filter";
    15.7 +time_use_thy "Hyperreal/HyperDef";
    16.1 --- a/src/HOL/Real/Real.ML	Mon Aug 16 18:41:06 1999 +0200
    16.2 +++ b/src/HOL/Real/Real.ML	Mon Aug 16 18:41:32 1999 +0200
    16.3 @@ -1,4 +1,5 @@
    16.4  (*  Title:       HOL/Real/Real.ML
    16.5 +    ID:          $Id$
    16.6      Author:      Lawrence C. Paulson
    16.7                   Jacques D. Fleuriot
    16.8      Copyright:   1998  University of Cambridge
    17.1 --- a/src/HOL/Real/Real.thy	Mon Aug 16 18:41:06 1999 +0200
    17.2 +++ b/src/HOL/Real/Real.thy	Mon Aug 16 18:41:32 1999 +0200
    17.3 @@ -1,4 +1,5 @@
    17.4  (*  Title:       Real/Real.thy
    17.5 +    ID          : $Id$
    17.6      Author:      Lawrence C. Paulson
    17.7                   Jacques D. Fleuriot
    17.8      Copyright:   1998  University of Cambridge
    18.1 --- a/src/HOL/Real/RealAbs.ML	Mon Aug 16 18:41:06 1999 +0200
    18.2 +++ b/src/HOL/Real/RealAbs.ML	Mon Aug 16 18:41:32 1999 +0200
    18.3 @@ -1,4 +1,5 @@
    18.4  (*  Title       : RealAbs.ML
    18.5 +    ID          : $Id$
    18.6      Author      : Jacques D. Fleuriot
    18.7      Copyright   : 1998  University of Cambridge
    18.8      Description : Absolute value function for the reals
    19.1 --- a/src/HOL/Real/RealAbs.thy	Mon Aug 16 18:41:06 1999 +0200
    19.2 +++ b/src/HOL/Real/RealAbs.thy	Mon Aug 16 18:41:32 1999 +0200
    19.3 @@ -1,4 +1,5 @@
    19.4  (*  Title       : RealAbs.thy
    19.5 +    ID          : $Id$
    19.6      Author      : Jacques D. Fleuriot
    19.7      Copyright   : 1998  University of Cambridge
    19.8      Description : Absolute value function for the reals
    20.1 --- a/src/HOL/Real/RealDef.ML	Mon Aug 16 18:41:06 1999 +0200
    20.2 +++ b/src/HOL/Real/RealDef.ML	Mon Aug 16 18:41:32 1999 +0200
    20.3 @@ -1,4 +1,5 @@
    20.4  (*  Title       : Real/RealDef.ML
    20.5 +    ID          : $Id$
    20.6      Author      : Jacques D. Fleuriot
    20.7      Copyright   : 1998  University of Cambridge
    20.8      Description : The reals
    21.1 --- a/src/HOL/Real/RealDef.thy	Mon Aug 16 18:41:06 1999 +0200
    21.2 +++ b/src/HOL/Real/RealDef.thy	Mon Aug 16 18:41:32 1999 +0200
    21.3 @@ -1,4 +1,5 @@
    21.4  (*  Title       : Real/RealDef.thy
    21.5 +    ID          : $Id$
    21.6      Author      : Jacques D. Fleuriot
    21.7      Copyright   : 1998  University of Cambridge
    21.8      Description : The reals
    22.1 --- a/src/HOL/Real/RealPow.ML	Mon Aug 16 18:41:06 1999 +0200
    22.2 +++ b/src/HOL/Real/RealPow.ML	Mon Aug 16 18:41:32 1999 +0200
    22.3 @@ -1,4 +1,5 @@
    22.4  (*  Title       : RealPow.ML
    22.5 +    ID          : $Id$
    22.6      Author      : Jacques D. Fleuriot  
    22.7      Copyright   : 1998  University of Cambridge
    22.8      Description : Natural Powers of reals theory
    23.1 --- a/src/HOL/Real/RealPow.thy	Mon Aug 16 18:41:06 1999 +0200
    23.2 +++ b/src/HOL/Real/RealPow.thy	Mon Aug 16 18:41:32 1999 +0200
    23.3 @@ -1,4 +1,5 @@
    23.4  (*  Title       : RealPow.thy
    23.5 +    ID          : $Id$
    23.6      Author      : Jacques D. Fleuriot  
    23.7      Copyright   : 1998  University of Cambridge
    23.8      Description : Natural powers theory