--- 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.
--- 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
--- 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.
--- 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)"
--- 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"