--- 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}"
--- 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"
--- 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)
--- 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))([],[])"
--- 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
--- 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
--- 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)"
--- 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)"
--- 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)"
--- 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*}
--- 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"