# HG changeset patch
# User wenzelm
# Date 1082628677 -7200
# Node ID 0848ab6fe5fc46008cb2bb6b379082b27858a95b
# Parent  5ddbdbadba0636d09f282bc4382b47335abce584
constdefs: proper order;

diff -r 5ddbdbadba06 -r 0848ab6fe5fc src/HOL/Complex/NSCA.thy
--- a/src/HOL/Complex/NSCA.thy	Thu Apr 22 11:02:22 2004 +0200
+++ b/src/HOL/Complex/NSCA.thy	Thu Apr 22 12:11:17 2004 +0200
@@ -9,6 +9,9 @@
 
 constdefs
 
+   CInfinitesimal  :: "hcomplex set"
+   "CInfinitesimal == {x. \<forall>r \<in> Reals. 0 < r --> hcmod x < r}"
+
     capprox    :: "[hcomplex,hcomplex] => bool"  (infixl "@c=" 50)  
       --{*the ``infinitely close'' relation*}
       "x @c= y == (x - y) \<in> CInfinitesimal"     
@@ -17,9 +20,6 @@
    SComplex  :: "hcomplex set"
    "SComplex == {x. \<exists>r. x = hcomplex_of_complex r}"
 
-   CInfinitesimal  :: "hcomplex set"
-   "CInfinitesimal == {x. \<forall>r \<in> Reals. 0 < r --> hcmod x < r}"
-
    CFinite :: "hcomplex set"
    "CFinite == {x. \<exists>r \<in> Reals. hcmod x < r}"
 
diff -r 5ddbdbadba06 -r 0848ab6fe5fc src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Thu Apr 22 11:02:22 2004 +0200
+++ b/src/HOL/Complex/NSComplex.thy	Thu Apr 22 12:11:17 2004 +0200
@@ -86,16 +86,16 @@
   hcis :: "hypreal => hcomplex"
   "hcis a == Abs_hcomplex(UN X:Rep_hypreal(a). hcomplexrel `` {%n. cis (X n)})"
 
-  (* abbreviation for r*(cos a + i sin a) *)
-  hrcis :: "[hypreal, hypreal] => hcomplex"
-  "hrcis r a == hcomplex_of_hypreal r * hcis a"
-
   (*----- injection from hyperreals -----*)
 
   hcomplex_of_hypreal :: "hypreal => hcomplex"
   "hcomplex_of_hypreal r == Abs_hcomplex(UN X:Rep_hypreal(r).
 			       hcomplexrel `` {%n. complex_of_real (X n)})"
 
+  (* abbreviation for r*(cos a + i sin a) *)
+  hrcis :: "[hypreal, hypreal] => hcomplex"
+  "hrcis r a == hcomplex_of_hypreal r * hcis a"
+
   (*------------ e ^ (x + iy) ------------*)
 
   hexpi :: "hcomplex => hcomplex"
diff -r 5ddbdbadba06 -r 0848ab6fe5fc src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Thu Apr 22 11:02:22 2004 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Thu Apr 22 12:11:17 2004 +0200
@@ -20,6 +20,10 @@
   HInfinite :: "hypreal set"
    "HInfinite == {x. \<forall>r \<in> Reals. r < abs x}"
 
+  (* infinitely close *)
+  approx :: "[hypreal, hypreal] => bool"    (infixl "@=" 50)
+   "x @= y       == (x + -y) \<in> Infinitesimal"
+
   (* standard part map *)
   st        :: "hypreal => hypreal"
    "st           == (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"
@@ -30,10 +34,6 @@
   galaxy    :: "hypreal => hypreal set"
    "galaxy x     == {y. (x + -y) \<in> HFinite}"
 
-  (* infinitely close *)
-  approx :: "[hypreal, hypreal] => bool"    (infixl "@=" 50)
-   "x @= y       == (x + -y) \<in> Infinitesimal"
-
 
 defs (overloaded)
 
diff -r 5ddbdbadba06 -r 0848ab6fe5fc src/HOL/Induct/SList.thy
--- a/src/HOL/Induct/SList.thy	Thu Apr 22 11:02:22 2004 +0200
+++ b/src/HOL/Induct/SList.thy	Thu Apr 22 12:11:17 2004 +0200
@@ -79,16 +79,14 @@
   "Cons"       :: "['a, 'a list] => 'a list"           (infixr "#" 65)
    "x#xs == Abs_List(CONS (Leaf x)(Rep_List xs))"
 
-  list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b"
-   "list_case a f xs == list_rec xs a (%x xs r. f x xs)"
-
   (* list Recursion -- the trancl is Essential; see list.ML *)
-
-
   list_rec  :: "['a list, 'b, ['a, 'a list, 'b]=>'b] => 'b"
    "list_rec l c d ==
       List_rec(Rep_List l) c (%x y r. d(inv Leaf x)(Abs_List y) r)"
 
+  list_case :: "['b, ['a, 'a list]=>'b, 'a list] => 'b"
+   "list_case a f xs == list_rec xs a (%x xs r. f x xs)"
+
 (* list Enumeration *)
 consts
   "[]"      :: "'a list"                            ("[]")
@@ -178,14 +176,14 @@
   "rev xs   == list_rec xs [] (%x xs xsa. xsa @ [x])"
 
 (* miscellaneous definitions *)
-  zip       :: "'a list * 'b list => ('a*'b) list"
-  "zip      == zipWith  (%s. s)"
-
   zipWith   :: "['a * 'b => 'c, 'a list * 'b list] => 'c list"
   "zipWith f S == (list_rec (fst S)  (%T.[])
                             (%x xs r. %T. if null T then [] 
                                           else f(x,hd T) # r(tl T)))(snd(S))"
 
+  zip       :: "'a list * 'b list => ('a*'b) list"
+  "zip      == zipWith  (%s. s)"
+
   unzip     :: "('a*'b) list => ('a list * 'b list)"
   "unzip    == foldr(% (a,b)(c,d).(a#c,b#d))([],[])"
 
diff -r 5ddbdbadba06 -r 0848ab6fe5fc src/HOL/MicroJava/BV/Typing_Framework.thy
--- a/src/HOL/MicroJava/BV/Typing_Framework.thy	Thu Apr 22 11:02:22 2004 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework.thy	Thu Apr 22 12:11:17 2004 +0200
@@ -21,15 +21,15 @@
  stables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
 "stables r step ss == !p<size ss. stable r step ss p"
 
+ wt_step ::
+"'s ord \<Rightarrow> 's \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
+"wt_step r T step ts ==
+ !p<size(ts). ts!p ~= T & stable r step ts p"
+
  is_bcv :: "'s ord \<Rightarrow> 's \<Rightarrow> 's step_type 
            \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> ('s list \<Rightarrow> 's list) \<Rightarrow> bool"  
 "is_bcv r T step n A bcv == !ss : list n A.
    (!p<n. (bcv ss)!p ~= T) =
    (? ts: list n A. ss <=[r] ts & wt_step r T step ts)"
 
- wt_step ::
-"'s ord \<Rightarrow> 's \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
-"wt_step r T step ts ==
- !p<size(ts). ts!p ~= T & stable r step ts p"
-
 end
diff -r 5ddbdbadba06 -r 0848ab6fe5fc src/HOL/MicroJava/Comp/DefsComp.thy
--- a/src/HOL/MicroJava/Comp/DefsComp.thy	Thu Apr 22 11:02:22 2004 +0200
+++ b/src/HOL/MicroJava/Comp/DefsComp.thy	Thu Apr 22 12:11:17 2004 +0200
@@ -26,8 +26,6 @@
     "gmb G cn si \<equiv> snd(snd(the(method (G,cn) si)))"
   gis :: "jvm_method \<Rightarrow> bytecode"
     "gis \<equiv> fst \<circ> snd \<circ> snd"
-  glvs :: "java_mb \<Rightarrow> State.locals \<Rightarrow> locvars"
-    "glvs jmb loc \<equiv> map (the\<circ>loc) (gjmb_plns jmb)"
 
 (* jmb = aus einem JavaMaethodBody *)
   gjmb_pns  :: "java_mb \<Rightarrow> vname list"     "gjmb_pns \<equiv> fst"
@@ -36,6 +34,9 @@
   gjmb_res  :: "java_mb \<Rightarrow> expr"           "gjmb_res \<equiv> snd\<circ>snd\<circ>snd"
   gjmb_plns :: "java_mb \<Rightarrow> vname list"
     "gjmb_plns \<equiv> \<lambda>jmb. gjmb_pns jmb @ map fst (gjmb_lvs jmb)"
+
+  glvs :: "java_mb \<Rightarrow> State.locals \<Rightarrow> locvars"
+    "glvs jmb loc \<equiv> map (the\<circ>loc) (gjmb_plns jmb)"
   
 lemmas gdefs = gx_def gh_def gl_def gmb_def gis_def glvs_def
 lemmas gjmbdefs = gjmb_pns_def gjmb_lvs_def gjmb_blk_def gjmb_res_def gjmb_plns_def
diff -r 5ddbdbadba06 -r 0848ab6fe5fc src/HOL/Real/HahnBanach/Bounds.thy
--- a/src/HOL/Real/HahnBanach/Bounds.thy	Thu Apr 22 11:02:22 2004 +0200
+++ b/src/HOL/Real/HahnBanach/Bounds.thy	Thu Apr 22 12:11:17 2004 +0200
@@ -14,13 +14,13 @@
 
 lemmas [elim?] = lub.least lub.upper
 
+constdefs
+  the_lub :: "'a::order set \<Rightarrow> 'a"
+  "the_lub A \<equiv> The (lub A)"
+
 syntax (xsymbols)
   the_lub :: "'a::order set \<Rightarrow> 'a"    ("\<Squnion>_" [90] 90)
 
-constdefs
-  the_lub :: "'a::order set \<Rightarrow> 'a"
-  "\<Squnion>A \<equiv> The (lub A)"
-
 lemma the_lub_equality [elim?]:
   includes lub
   shows "\<Squnion>A = (x::'a::order)"
diff -r 5ddbdbadba06 -r 0848ab6fe5fc src/HOL/Real/Lubs.thy
--- a/src/HOL/Real/Lubs.thy	Thu Apr 22 11:02:22 2004 +0200
+++ b/src/HOL/Real/Lubs.thy	Thu Apr 22 12:11:17 2004 +0200
@@ -21,12 +21,12 @@
   leastP      :: "['a =>bool,'a::ord] => bool"
     "leastP P x == (P x & x <=* Collect P)"
 
+  isUb        :: "['a set, 'a set, 'a::ord] => bool"
+    "isUb R S x   == S *<= x & x: R"
+
   isLub       :: "['a set, 'a set, 'a::ord] => bool"
     "isLub R S x  == leastP (isUb R S) x"
 
-  isUb        :: "['a set, 'a set, 'a::ord] => bool"
-    "isUb R S x   == S *<= x & x: R"
-
   ubs         :: "['a set, 'a::ord set] => 'a set"
     "ubs R S      == Collect (isUb R S)"
 
diff -r 5ddbdbadba06 -r 0848ab6fe5fc src/HOL/UNITY/UNITY.thy
--- a/src/HOL/UNITY/UNITY.thy	Thu Apr 22 11:02:22 2004 +0200
+++ b/src/HOL/UNITY/UNITY.thy	Thu Apr 22 12:11:17 2004 +0200
@@ -18,6 +18,9 @@
   by blast
 
 constdefs
+  Acts :: "'a program => ('a * 'a)set set"
+    "Acts F == (%(init, acts, allowed). acts) (Rep_Program F)"
+
   constrains :: "['a set, 'a set] => 'a program set"  (infixl "co"     60)
     "A co B == {F. \<forall>act \<in> Acts F. act``A \<subseteq> B}"
 
@@ -32,9 +35,6 @@
   Init :: "'a program => 'a set"
     "Init F == (%(init, acts, allowed). init) (Rep_Program F)"
 
-  Acts :: "'a program => ('a * 'a)set set"
-    "Acts F == (%(init, acts, allowed). acts) (Rep_Program F)"
-
   AllowedActs :: "'a program => ('a * 'a)set set"
     "AllowedActs F == (%(init, acts, allowed). allowed) (Rep_Program F)"
 
diff -r 5ddbdbadba06 -r 0848ab6fe5fc src/ZF/Trancl.thy
--- a/src/ZF/Trancl.thy	Thu Apr 22 11:02:22 2004 +0200
+++ b/src/ZF/Trancl.thy	Thu Apr 22 12:11:17 2004 +0200
@@ -16,9 +16,6 @@
   irrefl   :: "[i,i]=>o"
     "irrefl(A,r) == ALL x: A. <x,x> ~: r"
 
-  equiv    :: "[i,i]=>o"
-    "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"
-
   sym      :: "i=>o"
     "sym(r) == ALL x y. <x,y>: r --> <y,x>: r"
 
@@ -41,6 +38,10 @@
   trancl  :: "i=>i"  ("(_^+)" [100] 100)  (*transitive closure*)
     "r^+ == r O r^*"
 
+  equiv    :: "[i,i]=>o"
+    "equiv(A,r) == r <= A*A & refl(A,r) & sym(r) & trans(r)"
+
+
 subsection{*General properties of relations*}
 
 subsubsection{*irreflexivity*}
diff -r 5ddbdbadba06 -r 0848ab6fe5fc src/ZF/Zorn.thy
--- a/src/ZF/Zorn.thy	Thu Apr 22 11:02:22 2004 +0200
+++ b/src/ZF/Zorn.thy	Thu Apr 22 12:11:17 2004 +0200
@@ -19,12 +19,12 @@
   chain      :: "i=>i"
    "chain(A)      == {F \<in> Pow(A). \<forall>X\<in>F. \<forall>Y\<in>F. X<=Y | Y<=X}"
 
+  super      :: "[i,i]=>i"
+   "super(A,c)    == {d \<in> chain(A). c<=d & c\<noteq>d}"
+
   maxchain   :: "i=>i"
    "maxchain(A)   == {c \<in> chain(A). super(A,c)=0}"
 
-  super      :: "[i,i]=>i"
-   "super(A,c)    == {d \<in> chain(A). c<=d & c\<noteq>d}"
-
 
 constdefs
   increasing :: "i=>i"