tuned;
authorwenzelm
Thu Aug 08 23:52:55 2002 +0200 (2002-08-08)
changeset 134871291c6375c29
parent 13486 54464ea94d6f
child 13488 a246d390f033
tuned;
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Hyperreal/HyperNat.thy
src/HOL/Integ/IntDef.thy
src/HOL/Real/PRat.thy
src/HOL/Real/RealDef.thy
src/ZF/arith_data.ML
     1.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Thu Aug 08 23:51:24 2002 +0200
     1.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Thu Aug 08 23:52:55 2002 +0200
     1.3 @@ -3,12 +3,12 @@
     1.4      Author      : Jacques D. Fleuriot
     1.5      Copyright   : 1998  University of Cambridge
     1.6      Description : Construction of hyperreals using ultrafilters
     1.7 -*) 
     1.8 +*)
     1.9  
    1.10  HyperDef = Filter + Real +
    1.11  
    1.12 -consts 
    1.13 - 
    1.14 +consts
    1.15 +
    1.16      FreeUltrafilterNat   :: nat set set    ("\\<U>")
    1.17  
    1.18  defs
    1.19 @@ -19,10 +19,10 @@
    1.20  
    1.21  constdefs
    1.22      hyprel :: "((nat=>real)*(nat=>real)) set"
    1.23 -    "hyprel == {p. ? X Y. p = ((X::nat=>real),Y) & 
    1.24 +    "hyprel == {p. ? X Y. p = ((X::nat=>real),Y) &
    1.25                     {n::nat. X(n) = Y(n)}: FreeUltrafilterNat}"
    1.26  
    1.27 -typedef hypreal = "UNIV//hyprel"   (Equiv.quotient_def)
    1.28 +typedef hypreal = "UNIV//hyprel"   (quotient_def)
    1.29  
    1.30  instance
    1.31     hypreal  :: {ord, zero, one, plus, times, minus, inverse}
    1.32 @@ -38,24 +38,24 @@
    1.33    hypreal_minus_def
    1.34    "- P == Abs_hypreal(UN X: Rep_hypreal(P). hyprel``{%n::nat. - (X n)})"
    1.35  
    1.36 -  hypreal_diff_def 
    1.37 +  hypreal_diff_def
    1.38    "x - y == x + -(y::hypreal)"
    1.39  
    1.40    hypreal_inverse_def
    1.41 -  "inverse P == Abs_hypreal(UN X: Rep_hypreal(P). 
    1.42 +  "inverse P == Abs_hypreal(UN X: Rep_hypreal(P).
    1.43                      hyprel``{%n. if X n = 0 then 0 else inverse (X n)})"
    1.44  
    1.45    hypreal_divide_def
    1.46    "P / Q::hypreal == P * inverse Q"
    1.47 -  
    1.48 +
    1.49  constdefs
    1.50  
    1.51 -  hypreal_of_real  :: real => hypreal                 
    1.52 +  hypreal_of_real  :: real => hypreal
    1.53    "hypreal_of_real r         == Abs_hypreal(hyprel``{%n::nat. r})"
    1.54  
    1.55    omega   :: hypreal   (*an infinite number = [<1,2,3,...>] *)
    1.56    "omega == Abs_hypreal(hyprel``{%n::nat. real (Suc n)})"
    1.57 -    
    1.58 +
    1.59    epsilon :: hypreal   (*an infinitesimal number = [<1,1/2,1/3,...>] *)
    1.60    "epsilon == Abs_hypreal(hyprel``{%n::nat. inverse (real (Suc n))})"
    1.61  
    1.62 @@ -63,24 +63,22 @@
    1.63    omega   :: hypreal   ("\\<omega>")
    1.64    epsilon :: hypreal   ("\\<epsilon>")
    1.65  
    1.66 -  
    1.67 -defs 
    1.68  
    1.69 -  hypreal_add_def  
    1.70 +defs
    1.71 +
    1.72 +  hypreal_add_def
    1.73    "P + Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
    1.74                  hyprel``{%n::nat. X n + Y n})"
    1.75  
    1.76 -  hypreal_mult_def  
    1.77 +  hypreal_mult_def
    1.78    "P * Q == Abs_hypreal(UN X:Rep_hypreal(P). UN Y:Rep_hypreal(Q).
    1.79                  hyprel``{%n::nat. X n * Y n})"
    1.80  
    1.81    hypreal_less_def
    1.82 -  "P < (Q::hypreal) == EX X Y. X: Rep_hypreal(P) & 
    1.83 -                               Y: Rep_hypreal(Q) & 
    1.84 +  "P < (Q::hypreal) == EX X Y. X: Rep_hypreal(P) &
    1.85 +                               Y: Rep_hypreal(Q) &
    1.86                                 {n::nat. X n < Y n} : FreeUltrafilterNat"
    1.87    hypreal_le_def
    1.88 -  "P <= (Q::hypreal) == ~(Q < P)" 
    1.89 +  "P <= (Q::hypreal) == ~(Q < P)"
    1.90  
    1.91  end
    1.92 - 
    1.93 -
     2.1 --- a/src/HOL/Hyperreal/HyperNat.thy	Thu Aug 08 23:51:24 2002 +0200
     2.2 +++ b/src/HOL/Hyperreal/HyperNat.thy	Thu Aug 08 23:52:55 2002 +0200
     2.3 @@ -12,13 +12,13 @@
     2.4      "hypnatrel == {p. EX X Y. p = ((X::nat=>nat),Y) & 
     2.5                         {n::nat. X(n) = Y(n)} : FreeUltrafilterNat}"
     2.6  
     2.7 -typedef hypnat = "UNIV//hypnatrel"              (Equiv.quotient_def)
     2.8 +typedef hypnat = "UNIV//hypnatrel"              (quotient_def)
     2.9  
    2.10  instance
    2.11     hypnat  :: {ord, zero, one, plus, times, minus}
    2.12  
    2.13  consts
    2.14 -  "whn"       :: hypnat               ("whn")  
    2.15 +  whn       :: hypnat
    2.16  
    2.17  constdefs
    2.18  
     3.1 --- a/src/HOL/Integ/IntDef.thy	Thu Aug 08 23:51:24 2002 +0200
     3.2 +++ b/src/HOL/Integ/IntDef.thy	Thu Aug 08 23:52:55 2002 +0200
     3.3 @@ -12,7 +12,7 @@
     3.4    "intrel == {p. EX x1 y1 x2 y2. p=((x1::nat,y1),(x2,y2)) & x1+y2 = x2+y1}"
     3.5  
     3.6  typedef (Integ)
     3.7 -  int = "UNIV//intrel"            (Equiv.quotient_def)
     3.8 +  int = "UNIV//intrel"            (quotient_def)
     3.9  
    3.10  instance
    3.11    int :: {ord, zero, one, plus, times, minus}
     4.1 --- a/src/HOL/Real/PRat.thy	Thu Aug 08 23:51:24 2002 +0200
     4.2 +++ b/src/HOL/Real/PRat.thy	Thu Aug 08 23:52:55 2002 +0200
     4.3 @@ -11,7 +11,7 @@
     4.4      ratrel   ::  "((pnat * pnat) * (pnat * pnat)) set"
     4.5      "ratrel  ==  {p. ? x1 y1 x2 y2. p=((x1::pnat,y1),(x2,y2)) & x1*y2 = x2*y1}" 
     4.6  
     4.7 -typedef prat = "UNIV//ratrel"          (Equiv.quotient_def)
     4.8 +typedef prat = "UNIV//ratrel"          (quotient_def)
     4.9  
    4.10  instance
    4.11     prat  :: {ord,plus,times}
     5.1 --- a/src/HOL/Real/RealDef.thy	Thu Aug 08 23:51:24 2002 +0200
     5.2 +++ b/src/HOL/Real/RealDef.thy	Thu Aug 08 23:52:55 2002 +0200
     5.3 @@ -15,7 +15,7 @@
     5.4    "realrel == {p. EX x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}" 
     5.5  
     5.6  typedef (REAL)
     5.7 -  real = "UNIV//realrel"  (Equiv.quotient_def)
     5.8 +  real = "UNIV//realrel"  (quotient_def)
     5.9  
    5.10  
    5.11  instance
     6.1 --- a/src/ZF/arith_data.ML	Thu Aug 08 23:51:24 2002 +0200
     6.2 +++ b/src/ZF/arith_data.ML	Thu Aug 08 23:52:55 2002 +0200
     6.3 @@ -13,7 +13,7 @@
     6.4    (*tools for use in similar applications*)
     6.5    val gen_trans_tac: thm -> thm option -> tactic
     6.6    val prove_conv: string -> tactic list -> Sign.sg ->
     6.7 -                  thm list -> term * term -> thm option
     6.8 +                  thm list -> string list -> term * term -> thm option
     6.9    val simplify_meta_eq: thm list -> thm -> thm
    6.10    (*debugging*)
    6.11    structure EqCancelNumeralsData   : CANCEL_NUMERALS_DATA
    6.12 @@ -68,13 +68,13 @@
    6.13  
    6.14  fun add_chyps chyps ct = Drule.list_implies (map cprop_of chyps, ct);
    6.15  
    6.16 -fun prove_conv name tacs sg hyps (t,u) =
    6.17 +fun prove_conv name tacs sg hyps xs (t,u) =
    6.18    if t aconv u then None
    6.19    else
    6.20    let val hyps' = filter (not o is_eq_thm) hyps
    6.21        val goal = Logic.list_implies (map (#prop o Thm.rep_thm) hyps',
    6.22          FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
    6.23 -  in Some (hyps' MRS Tactic.prove sg [] [] goal (K (EVERY tacs)))
    6.24 +  in Some (hyps' MRS Tactic.prove sg xs [] goal (K (EVERY tacs)))
    6.25        handle ERROR_MESSAGE msg =>
    6.26          (warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); None)
    6.27    end;