# HG changeset patch
# User wenzelm
# Date 1085842253 -7200
# Node ID 44d92c12b255d8b295d5d566d2131f97094bb6b2
# Parent  b1fcade3880be2e3aefe0bdd1be2b299af2b725d
updated;

diff -r b1fcade3880b -r 44d92c12b255 src/HOL/Import/HOL/HOL4Base.thy
--- a/src/HOL/Import/HOL/HOL4Base.thy	Sat May 29 16:47:06 2004 +0200
+++ b/src/HOL/Import/HOL/HOL4Base.thy	Sat May 29 16:50:53 2004 +0200
@@ -186,7 +186,7 @@
 (ALL (e0::'a) e1::'a. (case False of True => e0 | False => e1) = e1)"
   by (import bool bool_case_thm)
 
-lemma bool_case_ID: "ALL x b. (case b of True => x | False => x) = x"
+lemma bool_case_ID: "ALL x b. (case b of True => x | _ => x) = x"
   by (import bool bool_case_ID)
 
 lemma boolAxiom: "ALL e0 e1. EX x. x True = e0 & x False = e1"
@@ -842,10 +842,39 @@
 
 constdefs
   SIMP_REC_REL :: "(nat => 'a) => 'a => ('a => 'a) => nat => bool" 
-  "SIMP_REC_REL == %fun x f n. fun 0 = x & (ALL m<n. fun (Suc m) = f (fun m))"
-
-lemma SIMP_REC_REL: "ALL fun x f n.
-   SIMP_REC_REL fun x f n = (fun 0 = x & (ALL m<n. fun (Suc m) = f (fun m)))"
+  "(op ==::((nat => 'a) => 'a => ('a => 'a) => nat => bool)
+        => ((nat => 'a) => 'a => ('a => 'a) => nat => bool) => prop)
+ (SIMP_REC_REL::(nat => 'a) => 'a => ('a => 'a) => nat => bool)
+ (%(fun::nat => 'a) (x::'a) (f::'a => 'a) n::nat.
+     (op &::bool => bool => bool)
+      ((op =::'a => 'a => bool) (fun (0::nat)) x)
+      ((All::(nat => bool) => bool)
+        (%m::nat.
+            (op -->::bool => bool => bool) ((op <::nat => nat => bool) m n)
+             ((op =::'a => 'a => bool) (fun ((Suc::nat => nat) m))
+               (f (fun m))))))"
+
+lemma SIMP_REC_REL: "(All::((nat => 'a) => bool) => bool)
+ (%fun::nat => 'a.
+     (All::('a => bool) => bool)
+      (%x::'a.
+          (All::(('a => 'a) => bool) => bool)
+           (%f::'a => 'a.
+               (All::(nat => bool) => bool)
+                (%n::nat.
+                    (op =::bool => bool => bool)
+                     ((SIMP_REC_REL::(nat => 'a)
+                                     => 'a => ('a => 'a) => nat => bool)
+                       fun x f n)
+                     ((op &::bool => bool => bool)
+                       ((op =::'a => 'a => bool) (fun (0::nat)) x)
+                       ((All::(nat => bool) => bool)
+                         (%m::nat.
+                             (op -->::bool => bool => bool)
+                              ((op <::nat => nat => bool) m n)
+                              ((op =::'a => 'a => bool)
+                                (fun ((Suc::nat => nat) m))
+                                (f (fun m))))))))))"
   by (import prim_rec SIMP_REC_REL)
 
 lemma SIMP_REC_EXISTS: "ALL x f n. EX fun. SIMP_REC_REL fun x f n"
@@ -1074,7 +1103,17 @@
 lemma LESS_OR_EQ_ADD: "ALL (n::nat) m::nat. n < m | (EX p::nat. n = p + m)"
   by (import arithmetic LESS_OR_EQ_ADD)
 
-lemma WOP: "ALL P::nat => bool. Ex P --> (EX n::nat. P n & (ALL m<n. ~ P m))"
+lemma WOP: "(All::((nat => bool) => bool) => bool)
+ (%P::nat => bool.
+     (op -->::bool => bool => bool) ((Ex::(nat => bool) => bool) P)
+      ((Ex::(nat => bool) => bool)
+        (%n::nat.
+            (op &::bool => bool => bool) (P n)
+             ((All::(nat => bool) => bool)
+               (%m::nat.
+                   (op -->::bool => bool => bool)
+                    ((op <::nat => nat => bool) m n)
+                    ((Not::bool => bool) (P m)))))))"
   by (import arithmetic WOP)
 
 lemma INV_PRE_LESS: "ALL m. 0 < m --> (ALL n. (PRE m < PRE n) = (m < n))"
@@ -2474,7 +2513,17 @@
 lemma MAP_EQ_NIL: "ALL l f. (map f l = []) = (l = []) & ([] = map f l) = (l = [])"
   by (import list MAP_EQ_NIL)
 
-lemma EVERY_EL: "ALL l P. list_all P l = (ALL n<length l. P (EL n l))"
+lemma EVERY_EL: "(All::('a list => bool) => bool)
+ (%l::'a list.
+     (All::(('a => bool) => bool) => bool)
+      (%P::'a => bool.
+          (op =::bool => bool => bool)
+           ((list_all::('a => bool) => 'a list => bool) P l)
+           ((All::(nat => bool) => bool)
+             (%n::nat.
+                 (op -->::bool => bool => bool)
+                  ((op <::nat => nat => bool) n ((size::'a list => nat) l))
+                  (P ((EL::nat => 'a list => 'a) n l))))))"
   by (import list EVERY_EL)
 
 lemma EVERY_CONJ: "ALL l. list_all (%x. P x & Q x) l = (list_all P l & list_all Q l)"
@@ -2584,9 +2633,27 @@
    zip l1 (map f2 l2) = map (%p. (fst p, f2 (snd p))) (zip l1 l2)"
   by (import list ZIP_MAP)
 
-lemma MEM_ZIP: "ALL l1 l2 p.
-   length l1 = length l2 -->
-   p mem zip l1 l2 = (EX n<length l1. p = (EL n l1, EL n l2))"
+lemma MEM_ZIP: "(All::('a list => bool) => bool)
+ (%l1::'a list.
+     (All::('b list => bool) => bool)
+      (%l2::'b list.
+          (All::('a * 'b => bool) => bool)
+           (%p::'a * 'b.
+               (op -->::bool => bool => bool)
+                ((op =::nat => nat => bool) ((size::'a list => nat) l1)
+                  ((size::'b list => nat) l2))
+                ((op =::bool => bool => bool)
+                  ((op mem::'a * 'b => ('a * 'b) list => bool) p
+                    ((zip::'a list => 'b list => ('a * 'b) list) l1 l2))
+                  ((Ex::(nat => bool) => bool)
+                    (%n::nat.
+                        (op &::bool => bool => bool)
+                         ((op <::nat => nat => bool) n
+                           ((size::'a list => nat) l1))
+                         ((op =::'a * 'b => 'a * 'b => bool) p
+                           ((Pair::'a => 'b => 'a * 'b)
+                             ((EL::nat => 'a list => 'a) n l1)
+                             ((EL::nat => 'b list => 'b) n l2)))))))))"
   by (import list MEM_ZIP)
 
 lemma EL_ZIP: "ALL l1 l2 n.
@@ -2599,7 +2666,17 @@
    (ALL f. map2 f l1 l2 = map (split f) (zip l1 l2))"
   by (import list MAP2_ZIP)
 
-lemma MEM_EL: "ALL l x. x mem l = (EX n<length l. x = EL n l)"
+lemma MEM_EL: "(All::('a list => bool) => bool)
+ (%l::'a list.
+     (All::('a => bool) => bool)
+      (%x::'a.
+          (op =::bool => bool => bool) ((op mem::'a => 'a list => bool) x l)
+           ((Ex::(nat => bool) => bool)
+             (%n::nat.
+                 (op &::bool => bool => bool)
+                  ((op <::nat => nat => bool) n ((size::'a list => nat) l))
+                  ((op =::'a => 'a => bool) x
+                    ((EL::nat => 'a list => 'a) n l))))))"
   by (import list MEM_EL)
 
 lemma LAST_CONS: "(ALL x::'a. last [x] = x) &
@@ -3378,9 +3455,22 @@
           s = GSPEC (%n. (f n, n < CARD s)))"
   by (import pred_set FINITE_ISO_NUM)
 
-lemma FINITE_WEAK_ENUMERATE: "ALL x::'a => bool.
-   FINITE x =
-   (EX (f::nat => 'a) b::nat. ALL e::'a. IN e x = (EX n<b. e = f n))"
+lemma FINITE_WEAK_ENUMERATE: "(All::(('a => bool) => bool) => bool)
+ (%x::'a => bool.
+     (op =::bool => bool => bool) ((FINITE::('a => bool) => bool) x)
+      ((Ex::((nat => 'a) => bool) => bool)
+        (%f::nat => 'a.
+            (Ex::(nat => bool) => bool)
+             (%b::nat.
+                 (All::('a => bool) => bool)
+                  (%e::'a.
+                      (op =::bool => bool => bool)
+                       ((IN::'a => ('a => bool) => bool) e x)
+                       ((Ex::(nat => bool) => bool)
+                         (%n::nat.
+                             (op &::bool => bool => bool)
+                              ((op <::nat => nat => bool) n b)
+                              ((op =::'a => 'a => bool) e (f n)))))))))"
   by (import pred_set FINITE_WEAK_ENUMERATE)
 
 constdefs
@@ -4282,16 +4372,51 @@
    n <= length l --> (ALL f. BUTLASTN n (map f l) = map f (BUTLASTN n l))"
   by (import rich_list BUTLASTN_MAP)
 
-lemma ALL_EL_LASTN: "ALL P l. list_all P l --> (ALL m<=length l. list_all P (LASTN m l))"
+lemma ALL_EL_LASTN: "(All::(('a => bool) => bool) => bool)
+ (%P::'a => bool.
+     (All::('a list => bool) => bool)
+      (%l::'a list.
+          (op -->::bool => bool => bool)
+           ((list_all::('a => bool) => 'a list => bool) P l)
+           ((All::(nat => bool) => bool)
+             (%m::nat.
+                 (op -->::bool => bool => bool)
+                  ((op <=::nat => nat => bool) m ((size::'a list => nat) l))
+                  ((list_all::('a => bool) => 'a list => bool) P
+                    ((LASTN::nat => 'a list => 'a list) m l))))))"
   by (import rich_list ALL_EL_LASTN)
 
-lemma ALL_EL_BUTLASTN: "ALL P l. list_all P l --> (ALL m<=length l. list_all P (BUTLASTN m l))"
+lemma ALL_EL_BUTLASTN: "(All::(('a => bool) => bool) => bool)
+ (%P::'a => bool.
+     (All::('a list => bool) => bool)
+      (%l::'a list.
+          (op -->::bool => bool => bool)
+           ((list_all::('a => bool) => 'a list => bool) P l)
+           ((All::(nat => bool) => bool)
+             (%m::nat.
+                 (op -->::bool => bool => bool)
+                  ((op <=::nat => nat => bool) m ((size::'a list => nat) l))
+                  ((list_all::('a => bool) => 'a list => bool) P
+                    ((BUTLASTN::nat => 'a list => 'a list) m l))))))"
   by (import rich_list ALL_EL_BUTLASTN)
 
 lemma LENGTH_FIRSTN: "ALL n l. n <= length l --> length (FIRSTN n l) = n"
   by (import rich_list LENGTH_FIRSTN)
 
-lemma FIRSTN_FIRSTN: "ALL m l. m <= length l --> (ALL n<=m. FIRSTN n (FIRSTN m l) = FIRSTN n l)"
+lemma FIRSTN_FIRSTN: "(All::(nat => bool) => bool)
+ (%m::nat.
+     (All::('a list => bool) => bool)
+      (%l::'a list.
+          (op -->::bool => bool => bool)
+           ((op <=::nat => nat => bool) m ((size::'a list => nat) l))
+           ((All::(nat => bool) => bool)
+             (%n::nat.
+                 (op -->::bool => bool => bool)
+                  ((op <=::nat => nat => bool) n m)
+                  ((op =::'a list => 'a list => bool)
+                    ((FIRSTN::nat => 'a list => 'a list) n
+                      ((FIRSTN::nat => 'a list => 'a list) m l))
+                    ((FIRSTN::nat => 'a list => 'a list) n l))))))"
   by (import rich_list FIRSTN_FIRSTN)
 
 lemma LENGTH_BUTFIRSTN: "ALL n l. n <= length l --> length (BUTFIRSTN n l) = length l - n"
@@ -4500,10 +4625,32 @@
    list_all P l --> (ALL m k. m + k <= length l --> list_all P (SEG m k l))"
   by (import rich_list ALL_EL_SEG)
 
-lemma ALL_EL_FIRSTN: "ALL P l. list_all P l --> (ALL m<=length l. list_all P (FIRSTN m l))"
+lemma ALL_EL_FIRSTN: "(All::(('a => bool) => bool) => bool)
+ (%P::'a => bool.
+     (All::('a list => bool) => bool)
+      (%l::'a list.
+          (op -->::bool => bool => bool)
+           ((list_all::('a => bool) => 'a list => bool) P l)
+           ((All::(nat => bool) => bool)
+             (%m::nat.
+                 (op -->::bool => bool => bool)
+                  ((op <=::nat => nat => bool) m ((size::'a list => nat) l))
+                  ((list_all::('a => bool) => 'a list => bool) P
+                    ((FIRSTN::nat => 'a list => 'a list) m l))))))"
   by (import rich_list ALL_EL_FIRSTN)
 
-lemma ALL_EL_BUTFIRSTN: "ALL P l. list_all P l --> (ALL m<=length l. list_all P (BUTFIRSTN m l))"
+lemma ALL_EL_BUTFIRSTN: "(All::(('a => bool) => bool) => bool)
+ (%P::'a => bool.
+     (All::('a list => bool) => bool)
+      (%l::'a list.
+          (op -->::bool => bool => bool)
+           ((list_all::('a => bool) => 'a list => bool) P l)
+           ((All::(nat => bool) => bool)
+             (%m::nat.
+                 (op -->::bool => bool => bool)
+                  ((op <=::nat => nat => bool) m ((size::'a list => nat) l))
+                  ((list_all::('a => bool) => 'a list => bool) P
+                    ((BUTFIRSTN::nat => 'a list => 'a list) m l))))))"
   by (import rich_list ALL_EL_BUTFIRSTN)
 
 lemma SOME_EL_SEG: "ALL m k l.
diff -r b1fcade3880b -r 44d92c12b255 src/HOL/Import/HOL/HOL4Real.thy
--- a/src/HOL/Import/HOL/HOL4Real.thy	Sat May 29 16:47:06 2004 +0200
+++ b/src/HOL/Import/HOL/HOL4Real.thy	Sat May 29 16:50:53 2004 +0200
@@ -682,9 +682,28 @@
 lemma SUM_0: "ALL m n. real.sum (m, n) (%r. 0) = 0"
   by (import real SUM_0)
 
-lemma SUM_PERMUTE_0: "ALL n p.
-   (ALL y<n. EX! x. x < n & p x = y) -->
-   (ALL f. real.sum (0, n) (%n. f (p n)) = real.sum (0, n) f)"
+lemma SUM_PERMUTE_0: "(All::(nat => bool) => bool)
+ (%n::nat.
+     (All::((nat => nat) => bool) => bool)
+      (%p::nat => nat.
+          (op -->::bool => bool => bool)
+           ((All::(nat => bool) => bool)
+             (%y::nat.
+                 (op -->::bool => bool => bool)
+                  ((op <::nat => nat => bool) y n)
+                  ((Ex1::(nat => bool) => bool)
+                    (%x::nat.
+                        (op &::bool => bool => bool)
+                         ((op <::nat => nat => bool) x n)
+                         ((op =::nat => nat => bool) (p x) y)))))
+           ((All::((nat => real) => bool) => bool)
+             (%f::nat => real.
+                 (op =::real => real => bool)
+                  ((real.sum::nat * nat => (nat => real) => real)
+                    ((Pair::nat => nat => nat * nat) (0::nat) n)
+                    (%n::nat. f (p n)))
+                  ((real.sum::nat * nat => (nat => real) => real)
+                    ((Pair::nat => nat => nat * nat) (0::nat) n) f)))))"
   by (import real SUM_PERMUTE_0)
 
 lemma SUM_CANCEL: "ALL f n d. real.sum (n, d) (%n. f (Suc n) - f n) = f (n + d) - f n"
@@ -1442,7 +1461,18 @@
 lemma MONO_SUC: "ALL f. seq.mono f = ((ALL x. f x <= f (Suc x)) | (ALL n. f (Suc n) <= f n))"
   by (import seq MONO_SUC)
 
-lemma MAX_LEMMA: "ALL (s::nat => real) N::nat. EX k::real. ALL n<N. abs (s n) < k"
+lemma MAX_LEMMA: "(All::((nat => real) => bool) => bool)
+ (%s::nat => real.
+     (All::(nat => bool) => bool)
+      (%N::nat.
+          (Ex::(real => bool) => bool)
+           (%k::real.
+               (All::(nat => bool) => bool)
+                (%n::nat.
+                    (op -->::bool => bool => bool)
+                     ((op <::nat => nat => bool) n N)
+                     ((op <::real => real => bool)
+                       ((abs::real => real) (s n)) k)))))"
   by (import seq MAX_LEMMA)
 
 lemma SEQ_BOUNDED: "ALL s. bounded (mr1, nat_ge) s = (EX k. ALL n. abs (s n) < k)"
@@ -5785,9 +5815,46 @@
 
 constdefs
   fine :: "(real => real) => (nat => real) * (nat => real) => bool" 
-  "fine == %g (D, p). ALL n<dsize D. D (Suc n) - D n < g (p n)"
-
-lemma fine: "ALL g D p. fine g (D, p) = (ALL n<dsize D. D (Suc n) - D n < g (p n))"
+  "(op ==::((real => real) => (nat => real) * (nat => real) => bool)
+        => ((real => real) => (nat => real) * (nat => real) => bool)
+           => prop)
+ (fine::(real => real) => (nat => real) * (nat => real) => bool)
+ (%g::real => real.
+     (split::((nat => real) => (nat => real) => bool)
+             => (nat => real) * (nat => real) => bool)
+      (%(D::nat => real) p::nat => real.
+          (All::(nat => bool) => bool)
+           (%n::nat.
+               (op -->::bool => bool => bool)
+                ((op <::nat => nat => bool) n
+                  ((dsize::(nat => real) => nat) D))
+                ((op <::real => real => bool)
+                  ((op -::real => real => real) (D ((Suc::nat => nat) n))
+                    (D n))
+                  (g (p n))))))"
+
+lemma fine: "(All::((real => real) => bool) => bool)
+ (%g::real => real.
+     (All::((nat => real) => bool) => bool)
+      (%D::nat => real.
+          (All::((nat => real) => bool) => bool)
+           (%p::nat => real.
+               (op =::bool => bool => bool)
+                ((fine::(real => real)
+                        => (nat => real) * (nat => real) => bool)
+                  g ((Pair::(nat => real)
+                            => (nat => real)
+                               => (nat => real) * (nat => real))
+                      D p))
+                ((All::(nat => bool) => bool)
+                  (%n::nat.
+                      (op -->::bool => bool => bool)
+                       ((op <::nat => nat => bool) n
+                         ((dsize::(nat => real) => nat) D))
+                       ((op <::real => real => bool)
+                         ((op -::real => real => real)
+                           (D ((Suc::nat => nat) n)) (D n))
+                         (g (p n))))))))"
   by (import transc fine)
 
 constdefs
diff -r b1fcade3880b -r 44d92c12b255 src/HOL/Import/HOL/HOL4Vec.thy
--- a/src/HOL/Import/HOL/HOL4Vec.thy	Sat May 29 16:47:06 2004 +0200
+++ b/src/HOL/Import/HOL/HOL4Vec.thy	Sat May 29 16:50:53 2004 +0200
@@ -256,7 +256,20 @@
 lemma BIT0: "ALL x. bit 0 (WORD [x]) = x"
   by (import word_base BIT0)
 
-lemma WSEG_BIT: "ALL n. RES_FORALL (PWORDLEN n) (%w. ALL k<n. WSEG 1 k w = WORD [bit k w])"
+lemma WSEG_BIT: "(All::(nat => bool) => bool)
+ (%n::nat.
+     (RES_FORALL::('a word => bool) => ('a word => bool) => bool)
+      ((PWORDLEN::nat => 'a word => bool) n)
+      (%w::'a word.
+          (All::(nat => bool) => bool)
+           (%k::nat.
+               (op -->::bool => bool => bool)
+                ((op <::nat => nat => bool) k n)
+                ((op =::'a word => 'a word => bool)
+                  ((WSEG::nat => nat => 'a word => 'a word) (1::nat) k w)
+                  ((WORD::'a list => 'a word)
+                    ((op #::'a => 'a list => 'a list)
+                      ((bit::nat => 'a word => 'a) k w) ([]::'a list)))))))"
   by (import word_base WSEG_BIT)
 
 lemma BIT_WSEG: "ALL n.
@@ -295,14 +308,38 @@
 specification (WCAT) WCAT_DEF: "ALL l1 l2. WCAT (WORD l1, WORD l2) = WORD (l1 @ l2)"
   by (import word_base WCAT_DEF)
 
-lemma WORD_PARTITION: "(ALL n::nat.
-    RES_FORALL (PWORDLEN n)
-     (%w::'a word. ALL m<=n. WCAT (WSPLIT m w) = w)) &
-(ALL (n::nat) m::nat.
-    RES_FORALL (PWORDLEN n)
-     (%w1::'a word.
-         RES_FORALL (PWORDLEN m)
-          (%w2::'a word. WSPLIT m (WCAT (w1, w2)) = (w1, w2))))"
+lemma WORD_PARTITION: "(op &::bool => bool => bool)
+ ((All::(nat => bool) => bool)
+   (%n::nat.
+       (RES_FORALL::('a word => bool) => ('a word => bool) => bool)
+        ((PWORDLEN::nat => 'a word => bool) n)
+        (%w::'a word.
+            (All::(nat => bool) => bool)
+             (%m::nat.
+                 (op -->::bool => bool => bool)
+                  ((op <=::nat => nat => bool) m n)
+                  ((op =::'a word => 'a word => bool)
+                    ((WCAT::'a word * 'a word => 'a word)
+                      ((WSPLIT::nat => 'a word => 'a word * 'a word) m w))
+                    w)))))
+ ((All::(nat => bool) => bool)
+   (%n::nat.
+       (All::(nat => bool) => bool)
+        (%m::nat.
+            (RES_FORALL::('a word => bool) => ('a word => bool) => bool)
+             ((PWORDLEN::nat => 'a word => bool) n)
+             (%w1::'a word.
+                 (RES_FORALL::('a word => bool)
+                              => ('a word => bool) => bool)
+                  ((PWORDLEN::nat => 'a word => bool) m)
+                  (%w2::'a word.
+                      (op =::'a word * 'a word => 'a word * 'a word => bool)
+                       ((WSPLIT::nat => 'a word => 'a word * 'a word) m
+                         ((WCAT::'a word * 'a word => 'a word)
+                           ((Pair::'a word => 'a word => 'a word * 'a word)
+                             w1 w2)))
+                       ((Pair::'a word => 'a word => 'a word * 'a word) w1
+                         w2))))))"
   by (import word_base WORD_PARTITION)
 
 lemma WCAT_ASSOC: "ALL w1 w2 w3. WCAT (w1, WCAT (w2, w3)) = WCAT (WCAT (w1, w2), w3)"
@@ -320,11 +357,25 @@
                                    (wm1 = wm2 & wn1 = wn2)))))"
   by (import word_base WCAT_11)
 
-lemma WSPLIT_PWORDLEN: "ALL n.
-   RES_FORALL (PWORDLEN n)
-    (%w. ALL m<=n.
-            IN (fst (WSPLIT m w)) (PWORDLEN (n - m)) &
-            IN (snd (WSPLIT m w)) (PWORDLEN m))"
+lemma WSPLIT_PWORDLEN: "(All::(nat => bool) => bool)
+ (%n::nat.
+     (RES_FORALL::('a word => bool) => ('a word => bool) => bool)
+      ((PWORDLEN::nat => 'a word => bool) n)
+      (%w::'a word.
+          (All::(nat => bool) => bool)
+           (%m::nat.
+               (op -->::bool => bool => bool)
+                ((op <=::nat => nat => bool) m n)
+                ((op &::bool => bool => bool)
+                  ((IN::'a word => ('a word => bool) => bool)
+                    ((fst::'a word * 'a word => 'a word)
+                      ((WSPLIT::nat => 'a word => 'a word * 'a word) m w))
+                    ((PWORDLEN::nat => 'a word => bool)
+                      ((op -::nat => nat => nat) n m)))
+                  ((IN::'a word => ('a word => bool) => bool)
+                    ((snd::'a word * 'a word => 'a word)
+                      ((WSPLIT::nat => 'a word => 'a word * 'a word) m w))
+                    ((PWORDLEN::nat => 'a word => bool) m))))))"
   by (import word_base WSPLIT_PWORDLEN)
 
 lemma WCAT_PWORDLEN: "ALL n1.
@@ -347,17 +398,54 @@
             WSEG m2 k2 (WSEG m1 k1 w) = WSEG m2 (k1 + k2) w)"
   by (import word_base WSEG_WSEG)
 
-lemma WSPLIT_WSEG: "ALL n.
-   RES_FORALL (PWORDLEN n)
-    (%w. ALL k<=n. WSPLIT k w = (WSEG (n - k) k w, WSEG k 0 w))"
+lemma WSPLIT_WSEG: "(All::(nat => bool) => bool)
+ (%n::nat.
+     (RES_FORALL::('a word => bool) => ('a word => bool) => bool)
+      ((PWORDLEN::nat => 'a word => bool) n)
+      (%w::'a word.
+          (All::(nat => bool) => bool)
+           (%k::nat.
+               (op -->::bool => bool => bool)
+                ((op <=::nat => nat => bool) k n)
+                ((op =::'a word * 'a word => 'a word * 'a word => bool)
+                  ((WSPLIT::nat => 'a word => 'a word * 'a word) k w)
+                  ((Pair::'a word => 'a word => 'a word * 'a word)
+                    ((WSEG::nat => nat => 'a word => 'a word)
+                      ((op -::nat => nat => nat) n k) k w)
+                    ((WSEG::nat => nat => 'a word => 'a word) k (0::nat)
+                      w))))))"
   by (import word_base WSPLIT_WSEG)
 
-lemma WSPLIT_WSEG1: "ALL n.
-   RES_FORALL (PWORDLEN n)
-    (%w. ALL k<=n. fst (WSPLIT k w) = WSEG (n - k) k w)"
+lemma WSPLIT_WSEG1: "(All::(nat => bool) => bool)
+ (%n::nat.
+     (RES_FORALL::('a word => bool) => ('a word => bool) => bool)
+      ((PWORDLEN::nat => 'a word => bool) n)
+      (%w::'a word.
+          (All::(nat => bool) => bool)
+           (%k::nat.
+               (op -->::bool => bool => bool)
+                ((op <=::nat => nat => bool) k n)
+                ((op =::'a word => 'a word => bool)
+                  ((fst::'a word * 'a word => 'a word)
+                    ((WSPLIT::nat => 'a word => 'a word * 'a word) k w))
+                  ((WSEG::nat => nat => 'a word => 'a word)
+                    ((op -::nat => nat => nat) n k) k w)))))"
   by (import word_base WSPLIT_WSEG1)
 
-lemma WSPLIT_WSEG2: "ALL n. RES_FORALL (PWORDLEN n) (%w. ALL k<=n. snd (WSPLIT k w) = WSEG k 0 w)"
+lemma WSPLIT_WSEG2: "(All::(nat => bool) => bool)
+ (%n::nat.
+     (RES_FORALL::('a word => bool) => ('a word => bool) => bool)
+      ((PWORDLEN::nat => 'a word => bool) n)
+      (%w::'a word.
+          (All::(nat => bool) => bool)
+           (%k::nat.
+               (op -->::bool => bool => bool)
+                ((op <=::nat => nat => bool) k n)
+                ((op =::'a word => 'a word => bool)
+                  ((snd::'a word * 'a word => 'a word)
+                    ((WSPLIT::nat => 'a word => 'a word * 'a word) k w))
+                  ((WSEG::nat => nat => 'a word => 'a word) k (0::nat)
+                    w)))))"
   by (import word_base WSPLIT_WSEG2)
 
 lemma WCAT_WSEG_WSEG: "ALL n.
@@ -416,10 +504,27 @@
                     bit k (WCAT (w1, w2)) = bit (k - n2) w1))"
   by (import word_base BIT_WCAT_FST)
 
-lemma BIT_WCAT_SND: "ALL n1 n2.
-   RES_FORALL (PWORDLEN n1)
-    (%w1. RES_FORALL (PWORDLEN n2)
-           (%w2. ALL k<n2. bit k (WCAT (w1, w2)) = bit k w2))"
+lemma BIT_WCAT_SND: "(All::(nat => bool) => bool)
+ (%n1::nat.
+     (All::(nat => bool) => bool)
+      (%n2::nat.
+          (RES_FORALL::('a word => bool) => ('a word => bool) => bool)
+           ((PWORDLEN::nat => 'a word => bool) n1)
+           (%w1::'a word.
+               (RES_FORALL::('a word => bool) => ('a word => bool) => bool)
+                ((PWORDLEN::nat => 'a word => bool) n2)
+                (%w2::'a word.
+                    (All::(nat => bool) => bool)
+                     (%k::nat.
+                         (op -->::bool => bool => bool)
+                          ((op <::nat => nat => bool) k n2)
+                          ((op =::'a => 'a => bool)
+                            ((bit::nat => 'a word => 'a) k
+                              ((WCAT::'a word * 'a word => 'a word)
+                                ((Pair::'a word
+  => 'a word => 'a word * 'a word)
+                                  w1 w2)))
+                            ((bit::nat => 'a word => 'a) k w2)))))))"
   by (import word_base BIT_WCAT_SND)
 
 lemma BIT_WCAT1: "ALL n. RES_FORALL (PWORDLEN n) (%w. ALL b. bit n (WCAT (WORD [b], w)) = b)"
@@ -449,10 +554,23 @@
                     WCAT (WSEG (m + k - n2) 0 w1, WSEG (n2 - k) k w2)))"
   by (import word_base WSEG_WCAT_WSEG)
 
-lemma BIT_EQ_IMP_WORD_EQ: "ALL n.
-   RES_FORALL (PWORDLEN n)
-    (%w1. RES_FORALL (PWORDLEN n)
-           (%w2. (ALL k<n. bit k w1 = bit k w2) --> w1 = w2))"
+lemma BIT_EQ_IMP_WORD_EQ: "(All::(nat => bool) => bool)
+ (%n::nat.
+     (RES_FORALL::('a word => bool) => ('a word => bool) => bool)
+      ((PWORDLEN::nat => 'a word => bool) n)
+      (%w1::'a word.
+          (RES_FORALL::('a word => bool) => ('a word => bool) => bool)
+           ((PWORDLEN::nat => 'a word => bool) n)
+           (%w2::'a word.
+               (op -->::bool => bool => bool)
+                ((All::(nat => bool) => bool)
+                  (%k::nat.
+                      (op -->::bool => bool => bool)
+                       ((op <::nat => nat => bool) k n)
+                       ((op =::'a => 'a => bool)
+                         ((bit::nat => 'a word => 'a) k w1)
+                         ((bit::nat => 'a word => 'a) k w2))))
+                ((op =::'a word => 'a word => bool) w1 w2))))"
   by (import word_base BIT_EQ_IMP_WORD_EQ)
 
 ;end_setup
@@ -586,11 +704,29 @@
                  m + k <= n --> oper (WSEG m k w) = WSEG m k (oper w)))"
   by (import word_bitop PBITOP_WSEG)
 
-lemma PBITOP_BIT: "RES_FORALL PBITOP
- (%oper.
-     ALL n.
-        RES_FORALL (PWORDLEN n)
-         (%w. ALL k<n. oper (WORD [bit k w]) = WORD [bit k (oper w)]))"
+lemma PBITOP_BIT: "(RES_FORALL::(('a word => 'b word) => bool)
+             => (('a word => 'b word) => bool) => bool)
+ (PBITOP::('a word => 'b word) => bool)
+ (%oper::'a word => 'b word.
+     (All::(nat => bool) => bool)
+      (%n::nat.
+          (RES_FORALL::('a word => bool) => ('a word => bool) => bool)
+           ((PWORDLEN::nat => 'a word => bool) n)
+           (%w::'a word.
+               (All::(nat => bool) => bool)
+                (%k::nat.
+                    (op -->::bool => bool => bool)
+                     ((op <::nat => nat => bool) k n)
+                     ((op =::'b word => 'b word => bool)
+                       (oper
+                         ((WORD::'a list => 'a word)
+                           ((op #::'a => 'a list => 'a list)
+                             ((bit::nat => 'a word => 'a) k w)
+                             ([]::'a list))))
+                       ((WORD::'b list => 'b word)
+                         ((op #::'b => 'b list => 'b list)
+                           ((bit::nat => 'b word => 'b) k (oper w))
+                           ([]::'b list))))))))"
   by (import word_bitop PBITOP_BIT)
 
 consts
@@ -669,9 +805,21 @@
 lemma WMAP_0: "ALL x. WMAP x (WORD []) = WORD []"
   by (import word_bitop WMAP_0)
 
-lemma WMAP_BIT: "ALL n.
-   RES_FORALL (PWORDLEN n)
-    (%w. ALL k<n. ALL f. bit k (WMAP f w) = f (bit k w))"
+lemma WMAP_BIT: "(All::(nat => bool) => bool)
+ (%n::nat.
+     (RES_FORALL::('a word => bool) => ('a word => bool) => bool)
+      ((PWORDLEN::nat => 'a word => bool) n)
+      (%w::'a word.
+          (All::(nat => bool) => bool)
+           (%k::nat.
+               (op -->::bool => bool => bool)
+                ((op <::nat => nat => bool) k n)
+                ((All::(('a => 'b) => bool) => bool)
+                  (%f::'a => 'b.
+                      (op =::'b => 'b => bool)
+                       ((bit::nat => 'b word => 'b) k
+                         ((WMAP::('a => 'b) => 'a word => 'b word) f w))
+                       (f ((bit::nat => 'a word => 'a) k w)))))))"
   by (import word_bitop WMAP_BIT)
 
 lemma WMAP_WSEG: "ALL n.
@@ -696,9 +844,20 @@
 specification (FORALLBITS) FORALLBITS_DEF: "ALL P l. FORALLBITS P (WORD l) = list_all P l"
   by (import word_bitop FORALLBITS_DEF)
 
-lemma FORALLBITS: "ALL n.
-   RES_FORALL (PWORDLEN n)
-    (%w. ALL P. FORALLBITS P w = (ALL k<n. P (bit k w)))"
+lemma FORALLBITS: "(All::(nat => bool) => bool)
+ (%n::nat.
+     (RES_FORALL::('a word => bool) => ('a word => bool) => bool)
+      ((PWORDLEN::nat => 'a word => bool) n)
+      (%w::'a word.
+          (All::(('a => bool) => bool) => bool)
+           (%P::'a => bool.
+               (op =::bool => bool => bool)
+                ((FORALLBITS::('a => bool) => 'a word => bool) P w)
+                ((All::(nat => bool) => bool)
+                  (%k::nat.
+                      (op -->::bool => bool => bool)
+                       ((op <::nat => nat => bool) k n)
+                       (P ((bit::nat => 'a word => 'a) k w)))))))"
   by (import word_bitop FORALLBITS)
 
 lemma FORALLBITS_WSEG: "ALL n.
@@ -724,9 +883,20 @@
 lemma NOT_FORALLBITS: "ALL P w. (~ FORALLBITS P w) = EXISTSABIT (Not o P) w"
   by (import word_bitop NOT_FORALLBITS)
 
-lemma EXISTSABIT: "ALL n.
-   RES_FORALL (PWORDLEN n)
-    (%w. ALL P. EXISTSABIT P w = (EX k<n. P (bit k w)))"
+lemma EXISTSABIT: "(All::(nat => bool) => bool)
+ (%n::nat.
+     (RES_FORALL::('a word => bool) => ('a word => bool) => bool)
+      ((PWORDLEN::nat => 'a word => bool) n)
+      (%w::'a word.
+          (All::(('a => bool) => bool) => bool)
+           (%P::'a => bool.
+               (op =::bool => bool => bool)
+                ((EXISTSABIT::('a => bool) => 'a word => bool) P w)
+                ((Ex::(nat => bool) => bool)
+                  (%k::nat.
+                      (op &::bool => bool => bool)
+                       ((op <::nat => nat => bool) k n)
+                       (P ((bit::nat => 'a word => 'a) k w)))))))"
   by (import word_bitop EXISTSABIT)
 
 lemma EXISTSABIT_WSEG: "ALL n.
@@ -927,7 +1097,16 @@
 lemma VB_BV: "ALL x. VB (BV x) = x"
   by (import bword_num VB_BV)
 
-lemma BV_VB: "ALL x<2. BV (VB x) = x"
+lemma BV_VB: "(All::(nat => bool) => bool)
+ (%x::nat.
+     (op -->::bool => bool => bool)
+      ((op <::nat => nat => bool) x
+        ((number_of::bin => nat)
+          ((op BIT::bin => bool => bin)
+            ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+            (False::bool))))
+      ((op =::nat => nat => bool) ((BV::bool => nat) ((VB::nat => bool) x))
+        x))"
   by (import bword_num BV_VB)
 
 lemma NBWORD_BNVAL: "ALL n. RES_FORALL (PWORDLEN n) (%w. NBWORD n (BNVAL w) = w)"
@@ -945,11 +1124,28 @@
 lemma WSPLIT_NBWORD_0: "ALL n m. m <= n --> WSPLIT m (NBWORD n 0) = (NBWORD (n - m) 0, NBWORD m 0)"
   by (import bword_num WSPLIT_NBWORD_0)
 
-lemma EQ_NBWORD0_SPLIT: "ALL n.
-   RES_FORALL (PWORDLEN n)
-    (%w. ALL m<=n.
-            (w = NBWORD n 0) =
-            (WSEG (n - m) m w = NBWORD (n - m) 0 & WSEG m 0 w = NBWORD m 0))"
+lemma EQ_NBWORD0_SPLIT: "(All::(nat => bool) => bool)
+ (%n::nat.
+     (RES_FORALL::(bool word => bool) => (bool word => bool) => bool)
+      ((PWORDLEN::nat => bool word => bool) n)
+      (%w::bool word.
+          (All::(nat => bool) => bool)
+           (%m::nat.
+               (op -->::bool => bool => bool)
+                ((op <=::nat => nat => bool) m n)
+                ((op =::bool => bool => bool)
+                  ((op =::bool word => bool word => bool) w
+                    ((NBWORD::nat => nat => bool word) n (0::nat)))
+                  ((op &::bool => bool => bool)
+                    ((op =::bool word => bool word => bool)
+                      ((WSEG::nat => nat => bool word => bool word)
+                        ((op -::nat => nat => nat) n m) m w)
+                      ((NBWORD::nat => nat => bool word)
+                        ((op -::nat => nat => nat) n m) (0::nat)))
+                    ((op =::bool word => bool word => bool)
+                      ((WSEG::nat => nat => bool word => bool word) m
+                        (0::nat) w)
+                      ((NBWORD::nat => nat => bool word) m (0::nat))))))))"
   by (import bword_num EQ_NBWORD0_SPLIT)
 
 lemma NBWORD_MOD: "ALL n m. NBWORD n (m mod 2 ^ n) = NBWORD n m"
@@ -1071,13 +1267,41 @@
                  <= 1))"
   by (import bword_arith ADD_BV_BNVAL_LESS_EQ1)
 
-lemma ACARRY_EQ_ADD_DIV: "ALL n.
-   RES_FORALL (PWORDLEN n)
-    (%w1. RES_FORALL (PWORDLEN n)
-           (%w2. ALL k<n.
-                    BV (ACARRY k w1 w2 cin) =
-                    (BNVAL (WSEG k 0 w1) + BNVAL (WSEG k 0 w2) + BV cin) div
-                    2 ^ k))"
+lemma ACARRY_EQ_ADD_DIV: "(All::(nat => bool) => bool)
+ (%n::nat.
+     (RES_FORALL::(bool word => bool) => (bool word => bool) => bool)
+      ((PWORDLEN::nat => bool word => bool) n)
+      (%w1::bool word.
+          (RES_FORALL::(bool word => bool) => (bool word => bool) => bool)
+           ((PWORDLEN::nat => bool word => bool) n)
+           (%w2::bool word.
+               (All::(nat => bool) => bool)
+                (%k::nat.
+                    (op -->::bool => bool => bool)
+                     ((op <::nat => nat => bool) k n)
+                     ((op =::nat => nat => bool)
+                       ((BV::bool => nat)
+                         ((ACARRY::nat
+                                   => bool word
+=> bool word => bool => bool)
+                           k w1 w2 (cin::bool)))
+                       ((op div::nat => nat => nat)
+                         ((op +::nat => nat => nat)
+                           ((op +::nat => nat => nat)
+                             ((BNVAL::bool word => nat)
+                               ((WSEG::nat => nat => bool word => bool word)
+                                 k (0::nat) w1))
+                             ((BNVAL::bool word => nat)
+                               ((WSEG::nat => nat => bool word => bool word)
+                                 k (0::nat) w2)))
+                           ((BV::bool => nat) cin))
+                         ((op ^::nat => nat => nat)
+                           ((number_of::bin => nat)
+                             ((op BIT::bin => bool => bin)
+                               ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                                 (True::bool))
+                               (False::bool)))
+                           k)))))))"
   by (import bword_arith ACARRY_EQ_ADD_DIV)
 
 lemma ADD_WORD_SPLIT: "ALL n1 n2.
diff -r b1fcade3880b -r 44d92c12b255 src/HOL/Import/HOL/HOL4Word32.thy
--- a/src/HOL/Import/HOL/HOL4Word32.thy	Sat May 29 16:47:06 2004 +0200
+++ b/src/HOL/Import/HOL/HOL4Word32.thy	Sat May 29 16:50:53 2004 +0200
@@ -500,7 +500,19 @@
 lemma TWO_COMP_ONE_COMP_QT: "ALL a. EQUIV (TWO_COMP a) (ONE_COMP a + AONE)"
   by (import word32 TWO_COMP_ONE_COMP_QT)
 
-lemma BIT_EQUIV_THM: "ALL x xa. (ALL xb<WL. bit xb x = bit xb xa) = EQUIV x xa"
+lemma BIT_EQUIV_THM: "(All::(nat => bool) => bool)
+ (%x::nat.
+     (All::(nat => bool) => bool)
+      (%xa::nat.
+          (op =::bool => bool => bool)
+           ((All::(nat => bool) => bool)
+             (%xb::nat.
+                 (op -->::bool => bool => bool)
+                  ((op <::nat => nat => bool) xb (WL::nat))
+                  ((op =::bool => bool => bool)
+                    ((bit::nat => nat => bool) xb x)
+                    ((bit::nat => nat => bool) xb xa))))
+           ((EQUIV::nat => nat => bool) x xa)))"
   by (import word32 BIT_EQUIV_THM)
 
 lemma BITS_SUC2: "ALL n a. BITS (Suc n) 0 a = SLICE (Suc n) (Suc n) a + BITS n 0 a"
@@ -548,9 +560,29 @@
 lemma COMP0_def: "COMP0 = ONE_COMP 0"
   by (import word32 COMP0_def)
 
-lemma BITWISE_THM2: "ALL y oper a b.
-   (ALL x<WL. oper (bit x a) (bit x b) = bit x y) =
-   EQUIV (BITWISE WL oper a b) y"
+lemma BITWISE_THM2: "(All::(nat => bool) => bool)
+ (%y::nat.
+     (All::((bool => bool => bool) => bool) => bool)
+      (%oper::bool => bool => bool.
+          (All::(nat => bool) => bool)
+           (%a::nat.
+               (All::(nat => bool) => bool)
+                (%b::nat.
+                    (op =::bool => bool => bool)
+                     ((All::(nat => bool) => bool)
+                       (%x::nat.
+                           (op -->::bool => bool => bool)
+                            ((op <::nat => nat => bool) x (WL::nat))
+                            ((op =::bool => bool => bool)
+                              (oper ((bit::nat => nat => bool) x a)
+                                ((bit::nat => nat => bool) x b))
+                              ((bit::nat => nat => bool) x y))))
+                     ((EQUIV::nat => nat => bool)
+                       ((BITWISE::nat
+                                  => (bool => bool => bool)
+                                     => nat => nat => nat)
+                         (WL::nat) oper a b)
+                       y)))))"
   by (import word32 BITWISE_THM2)
 
 lemma OR_ASSOC_QT: "ALL a b c. EQUIV (OR a (OR b c)) (OR (OR a b) c)"
diff -r b1fcade3880b -r 44d92c12b255 src/HOL/Import/HOL/real.imp
--- a/src/HOL/Import/HOL/real.imp	Sat May 29 16:47:06 2004 +0200
+++ b/src/HOL/Import/HOL/real.imp	Sat May 29 16:50:53 2004 +0200
@@ -25,7 +25,7 @@
   "sumc" > "HOL4Real.real.sumc"
   "sum_def" > "HOL4Real.real.sum_def"
   "sum" > "HOL4Real.real.sum"
-  "real_sub" > "OrderedGroup.compare_rls_1"
+  "real_sub" > "OrderedGroup.diff_def"
   "real_of_num" > "HOL4Compat.real_of_num"
   "real_lte" > "HOL4Compat.real_lte"
   "real_lt" > "HOL.linorder_not_le"