constdefs: proper order;
authorwenzelm
Thu Apr 22 12:11:17 2004 +0200 (2004-04-22)
changeset 146530848ab6fe5fc
parent 14652 5ddbdbadba06
child 14654 aad262a36014
constdefs: proper order;
src/HOL/Complex/NSCA.thy
src/HOL/Complex/NSComplex.thy
src/HOL/Hyperreal/NSA.thy
src/HOL/Induct/SList.thy
src/HOL/MicroJava/BV/Typing_Framework.thy
src/HOL/MicroJava/Comp/DefsComp.thy
src/HOL/Real/HahnBanach/Bounds.thy
src/HOL/Real/Lubs.thy
src/HOL/UNITY/UNITY.thy
src/ZF/Trancl.thy
src/ZF/Zorn.thy
     1.1 --- a/src/HOL/Complex/NSCA.thy	Thu Apr 22 11:02:22 2004 +0200
     1.2 +++ b/src/HOL/Complex/NSCA.thy	Thu Apr 22 12:11:17 2004 +0200
     1.3 @@ -9,6 +9,9 @@
     1.4  
     1.5  constdefs
     1.6  
     1.7 +   CInfinitesimal  :: "hcomplex set"
     1.8 +   "CInfinitesimal == {x. \<forall>r \<in> Reals. 0 < r --> hcmod x < r}"
     1.9 +
    1.10      capprox    :: "[hcomplex,hcomplex] => bool"  (infixl "@c=" 50)  
    1.11        --{*the ``infinitely close'' relation*}
    1.12        "x @c= y == (x - y) \<in> CInfinitesimal"     
    1.13 @@ -17,9 +20,6 @@
    1.14     SComplex  :: "hcomplex set"
    1.15     "SComplex == {x. \<exists>r. x = hcomplex_of_complex r}"
    1.16  
    1.17 -   CInfinitesimal  :: "hcomplex set"
    1.18 -   "CInfinitesimal == {x. \<forall>r \<in> Reals. 0 < r --> hcmod x < r}"
    1.19 -
    1.20     CFinite :: "hcomplex set"
    1.21     "CFinite == {x. \<exists>r \<in> Reals. hcmod x < r}"
    1.22  
     2.1 --- a/src/HOL/Complex/NSComplex.thy	Thu Apr 22 11:02:22 2004 +0200
     2.2 +++ b/src/HOL/Complex/NSComplex.thy	Thu Apr 22 12:11:17 2004 +0200
     2.3 @@ -86,16 +86,16 @@
     2.4    hcis :: "hypreal => hcomplex"
     2.5    "hcis a == Abs_hcomplex(UN X:Rep_hypreal(a). hcomplexrel `` {%n. cis (X n)})"
     2.6  
     2.7 -  (* abbreviation for r*(cos a + i sin a) *)
     2.8 -  hrcis :: "[hypreal, hypreal] => hcomplex"
     2.9 -  "hrcis r a == hcomplex_of_hypreal r * hcis a"
    2.10 -
    2.11    (*----- injection from hyperreals -----*)
    2.12  
    2.13    hcomplex_of_hypreal :: "hypreal => hcomplex"
    2.14    "hcomplex_of_hypreal r == Abs_hcomplex(UN X:Rep_hypreal(r).
    2.15  			       hcomplexrel `` {%n. complex_of_real (X n)})"
    2.16  
    2.17 +  (* abbreviation for r*(cos a + i sin a) *)
    2.18 +  hrcis :: "[hypreal, hypreal] => hcomplex"
    2.19 +  "hrcis r a == hcomplex_of_hypreal r * hcis a"
    2.20 +
    2.21    (*------------ e ^ (x + iy) ------------*)
    2.22  
    2.23    hexpi :: "hcomplex => hcomplex"
     3.1 --- a/src/HOL/Hyperreal/NSA.thy	Thu Apr 22 11:02:22 2004 +0200
     3.2 +++ b/src/HOL/Hyperreal/NSA.thy	Thu Apr 22 12:11:17 2004 +0200
     3.3 @@ -20,6 +20,10 @@
     3.4    HInfinite :: "hypreal set"
     3.5     "HInfinite == {x. \<forall>r \<in> Reals. r < abs x}"
     3.6  
     3.7 +  (* infinitely close *)
     3.8 +  approx :: "[hypreal, hypreal] => bool"    (infixl "@=" 50)
     3.9 +   "x @= y       == (x + -y) \<in> Infinitesimal"
    3.10 +
    3.11    (* standard part map *)
    3.12    st        :: "hypreal => hypreal"
    3.13     "st           == (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"
    3.14 @@ -30,10 +34,6 @@
    3.15    galaxy    :: "hypreal => hypreal set"
    3.16     "galaxy x     == {y. (x + -y) \<in> HFinite}"
    3.17  
    3.18 -  (* infinitely close *)
    3.19 -  approx :: "[hypreal, hypreal] => bool"    (infixl "@=" 50)
    3.20 -   "x @= y       == (x + -y) \<in> Infinitesimal"
    3.21 -
    3.22  
    3.23  defs (overloaded)
    3.24  
     4.1 --- a/src/HOL/Induct/SList.thy	Thu Apr 22 11:02:22 2004 +0200
     4.2 +++ b/src/HOL/Induct/SList.thy	Thu Apr 22 12:11:17 2004 +0200
     4.3 @@ -79,16 +79,14 @@
     4.4    "Cons"       :: "['a, 'a list] => 'a list"           (infixr "#" 65)
     4.5     "x#xs == Abs_List(CONS (Leaf x)(Rep_List xs))"
     4.6  
     4.7 -  list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b"
     4.8 -   "list_case a f xs == list_rec xs a (%x xs r. f x xs)"
     4.9 -
    4.10    (* list Recursion -- the trancl is Essential; see list.ML *)
    4.11 -
    4.12 -
    4.13    list_rec  :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"
    4.14     "list_rec l c d ==
    4.15        List_rec(Rep_List l) c (%x y r. d(inv Leaf x)(Abs_List y) r)"
    4.16  
    4.17 +  list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b"
    4.18 +   "list_case a f xs == list_rec xs a (%x xs r. f x xs)"
    4.19 +
    4.20  (* list Enumeration *)
    4.21  consts
    4.22    "[]"      :: "'a list"                            ("[]")
    4.23 @@ -178,14 +176,14 @@
    4.24    "rev xs   == list_rec xs [] (%x xs xsa. xsa @ [x])"
    4.25  
    4.26  (* miscellaneous definitions *)
    4.27 -  zip       :: "'a list * 'b list => ('a*'b) list"
    4.28 -  "zip      == zipWith  (%s. s)"
    4.29 -
    4.30    zipWith   :: "['a * 'b => 'c, 'a list * 'b list] => 'c list"
    4.31    "zipWith f S == (list_rec (fst S)  (%T.[])
    4.32                              (%x xs r. %T. if null T then [] 
    4.33                                            else f(x,hd T) # r(tl T)))(snd(S))"
    4.34  
    4.35 +  zip       :: "'a list * 'b list => ('a*'b) list"
    4.36 +  "zip      == zipWith  (%s. s)"
    4.37 +
    4.38    unzip     :: "('a*'b) list => ('a list * 'b list)"
    4.39    "unzip    == foldr(% (a,b)(c,d).(a#c,b#d))([],[])"
    4.40  
     5.1 --- a/src/HOL/MicroJava/BV/Typing_Framework.thy	Thu Apr 22 11:02:22 2004 +0200
     5.2 +++ b/src/HOL/MicroJava/BV/Typing_Framework.thy	Thu Apr 22 12:11:17 2004 +0200
     5.3 @@ -21,15 +21,15 @@
     5.4   stables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
     5.5  "stables r step ss == !p<size ss. stable r step ss p"
     5.6  
     5.7 + wt_step ::
     5.8 +"'s ord \<Rightarrow> 's \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
     5.9 +"wt_step r T step ts ==
    5.10 + !p<size(ts). ts!p ~= T & stable r step ts p"
    5.11 +
    5.12   is_bcv :: "'s ord \<Rightarrow> 's \<Rightarrow> 's step_type 
    5.13             \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> ('s list \<Rightarrow> 's list) \<Rightarrow> bool"  
    5.14  "is_bcv r T step n A bcv == !ss : list n A.
    5.15     (!p<n. (bcv ss)!p ~= T) =
    5.16     (? ts: list n A. ss <=[r] ts & wt_step r T step ts)"
    5.17  
    5.18 - wt_step ::
    5.19 -"'s ord \<Rightarrow> 's \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
    5.20 -"wt_step r T step ts ==
    5.21 - !p<size(ts). ts!p ~= T & stable r step ts p"
    5.22 -
    5.23  end
     6.1 --- a/src/HOL/MicroJava/Comp/DefsComp.thy	Thu Apr 22 11:02:22 2004 +0200
     6.2 +++ b/src/HOL/MicroJava/Comp/DefsComp.thy	Thu Apr 22 12:11:17 2004 +0200
     6.3 @@ -26,8 +26,6 @@
     6.4      "gmb G cn si \<equiv> snd(snd(the(method (G,cn) si)))"
     6.5    gis :: "jvm_method \<Rightarrow> bytecode"
     6.6      "gis \<equiv> fst \<circ> snd \<circ> snd"
     6.7 -  glvs :: "java_mb \<Rightarrow> State.locals \<Rightarrow> locvars"
     6.8 -    "glvs jmb loc \<equiv> map (the\<circ>loc) (gjmb_plns jmb)"
     6.9  
    6.10  (* jmb = aus einem JavaMaethodBody *)
    6.11    gjmb_pns  :: "java_mb \<Rightarrow> vname list"     "gjmb_pns \<equiv> fst"
    6.12 @@ -36,6 +34,9 @@
    6.13    gjmb_res  :: "java_mb \<Rightarrow> expr"           "gjmb_res \<equiv> snd\<circ>snd\<circ>snd"
    6.14    gjmb_plns :: "java_mb \<Rightarrow> vname list"
    6.15      "gjmb_plns \<equiv> \<lambda>jmb. gjmb_pns jmb @ map fst (gjmb_lvs jmb)"
    6.16 +
    6.17 +  glvs :: "java_mb \<Rightarrow> State.locals \<Rightarrow> locvars"
    6.18 +    "glvs jmb loc \<equiv> map (the\<circ>loc) (gjmb_plns jmb)"
    6.19    
    6.20  lemmas gdefs = gx_def gh_def gl_def gmb_def gis_def glvs_def
    6.21  lemmas gjmbdefs = gjmb_pns_def gjmb_lvs_def gjmb_blk_def gjmb_res_def gjmb_plns_def
     7.1 --- a/src/HOL/Real/HahnBanach/Bounds.thy	Thu Apr 22 11:02:22 2004 +0200
     7.2 +++ b/src/HOL/Real/HahnBanach/Bounds.thy	Thu Apr 22 12:11:17 2004 +0200
     7.3 @@ -14,13 +14,13 @@
     7.4  
     7.5  lemmas [elim?] = lub.least lub.upper
     7.6  
     7.7 +constdefs
     7.8 +  the_lub :: "'a::order set \<Rightarrow> 'a"
     7.9 +  "the_lub A \<equiv> The (lub A)"
    7.10 +
    7.11  syntax (xsymbols)
    7.12    the_lub :: "'a::order set \<Rightarrow> 'a"    ("\<Squnion>_" [90] 90)
    7.13  
    7.14 -constdefs
    7.15 -  the_lub :: "'a::order set \<Rightarrow> 'a"
    7.16 -  "\<Squnion>A \<equiv> The (lub A)"
    7.17 -
    7.18  lemma the_lub_equality [elim?]:
    7.19    includes lub
    7.20    shows "\<Squnion>A = (x::'a::order)"
     8.1 --- a/src/HOL/Real/Lubs.thy	Thu Apr 22 11:02:22 2004 +0200
     8.2 +++ b/src/HOL/Real/Lubs.thy	Thu Apr 22 12:11:17 2004 +0200
     8.3 @@ -21,12 +21,12 @@
     8.4    leastP      :: "['a =>bool,'a::ord] => bool"
     8.5      "leastP P x == (P x & x <=* Collect P)"
     8.6  
     8.7 +  isUb        :: "['a set, 'a set, 'a::ord] => bool"
     8.8 +    "isUb R S x   == S *<= x & x: R"
     8.9 +
    8.10    isLub       :: "['a set, 'a set, 'a::ord] => bool"
    8.11      "isLub R S x  == leastP (isUb R S) x"
    8.12  
    8.13 -  isUb        :: "['a set, 'a set, 'a::ord] => bool"
    8.14 -    "isUb R S x   == S *<= x & x: R"
    8.15 -
    8.16    ubs         :: "['a set, 'a::ord set] => 'a set"
    8.17      "ubs R S      == Collect (isUb R S)"
    8.18  
     9.1 --- a/src/HOL/UNITY/UNITY.thy	Thu Apr 22 11:02:22 2004 +0200
     9.2 +++ b/src/HOL/UNITY/UNITY.thy	Thu Apr 22 12:11:17 2004 +0200
     9.3 @@ -18,6 +18,9 @@
     9.4    by blast
     9.5  
     9.6  constdefs
     9.7 +  Acts :: "'a program => ('a * 'a)set set"
     9.8 +    "Acts F == (%(init, acts, allowed). acts) (Rep_Program F)"
     9.9 +
    9.10    constrains :: "['a set, 'a set] => 'a program set"  (infixl "co"     60)
    9.11      "A co B == {F. \<forall>act \<in> Acts F. act``A \<subseteq> B}"
    9.12  
    9.13 @@ -32,9 +35,6 @@
    9.14    Init :: "'a program => 'a set"
    9.15      "Init F == (%(init, acts, allowed). init) (Rep_Program F)"
    9.16  
    9.17 -  Acts :: "'a program => ('a * 'a)set set"
    9.18 -    "Acts F == (%(init, acts, allowed). acts) (Rep_Program F)"
    9.19 -
    9.20    AllowedActs :: "'a program => ('a * 'a)set set"
    9.21      "AllowedActs F == (%(init, acts, allowed). allowed) (Rep_Program F)"
    9.22  
    10.1 --- a/src/ZF/Trancl.thy	Thu Apr 22 11:02:22 2004 +0200
    10.2 +++ b/src/ZF/Trancl.thy	Thu Apr 22 12:11:17 2004 +0200
    10.3 @@ -16,9 +16,6 @@
    10.4    irrefl   :: "[i,i]=>o"
    10.5      "irrefl(A,r) == ALL x: A. <x,x> ~: r"
    10.6  
    10.7 -  equiv    :: "[i,i]=>o"
    10.8 -    "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"
    10.9 -
   10.10    sym      :: "i=>o"
   10.11      "sym(r) == ALL x y. <x,y>: r --> <y,x>: r"
   10.12  
   10.13 @@ -41,6 +38,10 @@
   10.14    trancl  :: "i=>i"  ("(_^+)" [100] 100)  (*transitive closure*)
   10.15      "r^+ == r O r^*"
   10.16  
   10.17 +  equiv    :: "[i,i]=>o"
   10.18 +    "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"
   10.19 +
   10.20 +
   10.21  subsection{*General properties of relations*}
   10.22  
   10.23  subsubsection{*irreflexivity*}
    11.1 --- a/src/ZF/Zorn.thy	Thu Apr 22 11:02:22 2004 +0200
    11.2 +++ b/src/ZF/Zorn.thy	Thu Apr 22 12:11:17 2004 +0200
    11.3 @@ -19,12 +19,12 @@
    11.4    chain      :: "i=>i"
    11.5     "chain(A)      == {F \<in> Pow(A). \<forall>X\<in>F. \<forall>Y\<in>F. X<=Y | Y<=X}"
    11.6  
    11.7 +  super      :: "[i,i]=>i"
    11.8 +   "super(A,c)    == {d \<in> chain(A). c<=d & c\<noteq>d}"
    11.9 +
   11.10    maxchain   :: "i=>i"
   11.11     "maxchain(A)   == {c \<in> chain(A). super(A,c)=0}"
   11.12  
   11.13 -  super      :: "[i,i]=>i"
   11.14 -   "super(A,c)    == {d \<in> chain(A). c<=d & c\<noteq>d}"
   11.15 -
   11.16  
   11.17  constdefs
   11.18    increasing :: "i=>i"