src/HOL/Import/HOL/HOL4Word32.thy
changeset 14847 44d92c12b255
parent 14516 a183dec876ab
child 15647 b1f486a9c56b
     1.1 --- a/src/HOL/Import/HOL/HOL4Word32.thy	Sat May 29 16:47:06 2004 +0200
     1.2 +++ b/src/HOL/Import/HOL/HOL4Word32.thy	Sat May 29 16:50:53 2004 +0200
     1.3 @@ -500,7 +500,19 @@
     1.4  lemma TWO_COMP_ONE_COMP_QT: "ALL a. EQUIV (TWO_COMP a) (ONE_COMP a + AONE)"
     1.5    by (import word32 TWO_COMP_ONE_COMP_QT)
     1.6  
     1.7 -lemma BIT_EQUIV_THM: "ALL x xa. (ALL xb<WL. bit xb x = bit xb xa) = EQUIV x xa"
     1.8 +lemma BIT_EQUIV_THM: "(All::(nat => bool) => bool)
     1.9 + (%x::nat.
    1.10 +     (All::(nat => bool) => bool)
    1.11 +      (%xa::nat.
    1.12 +          (op =::bool => bool => bool)
    1.13 +           ((All::(nat => bool) => bool)
    1.14 +             (%xb::nat.
    1.15 +                 (op -->::bool => bool => bool)
    1.16 +                  ((op <::nat => nat => bool) xb (WL::nat))
    1.17 +                  ((op =::bool => bool => bool)
    1.18 +                    ((bit::nat => nat => bool) xb x)
    1.19 +                    ((bit::nat => nat => bool) xb xa))))
    1.20 +           ((EQUIV::nat => nat => bool) x xa)))"
    1.21    by (import word32 BIT_EQUIV_THM)
    1.22  
    1.23  lemma BITS_SUC2: "ALL n a. BITS (Suc n) 0 a = SLICE (Suc n) (Suc n) a + BITS n 0 a"
    1.24 @@ -548,9 +560,29 @@
    1.25  lemma COMP0_def: "COMP0 = ONE_COMP 0"
    1.26    by (import word32 COMP0_def)
    1.27  
    1.28 -lemma BITWISE_THM2: "ALL y oper a b.
    1.29 -   (ALL x<WL. oper (bit x a) (bit x b) = bit x y) =
    1.30 -   EQUIV (BITWISE WL oper a b) y"
    1.31 +lemma BITWISE_THM2: "(All::(nat => bool) => bool)
    1.32 + (%y::nat.
    1.33 +     (All::((bool => bool => bool) => bool) => bool)
    1.34 +      (%oper::bool => bool => bool.
    1.35 +          (All::(nat => bool) => bool)
    1.36 +           (%a::nat.
    1.37 +               (All::(nat => bool) => bool)
    1.38 +                (%b::nat.
    1.39 +                    (op =::bool => bool => bool)
    1.40 +                     ((All::(nat => bool) => bool)
    1.41 +                       (%x::nat.
    1.42 +                           (op -->::bool => bool => bool)
    1.43 +                            ((op <::nat => nat => bool) x (WL::nat))
    1.44 +                            ((op =::bool => bool => bool)
    1.45 +                              (oper ((bit::nat => nat => bool) x a)
    1.46 +                                ((bit::nat => nat => bool) x b))
    1.47 +                              ((bit::nat => nat => bool) x y))))
    1.48 +                     ((EQUIV::nat => nat => bool)
    1.49 +                       ((BITWISE::nat
    1.50 +                                  => (bool => bool => bool)
    1.51 +                                     => nat => nat => nat)
    1.52 +                         (WL::nat) oper a b)
    1.53 +                       y)))))"
    1.54    by (import word32 BITWISE_THM2)
    1.55  
    1.56  lemma OR_ASSOC_QT: "ALL a b c. EQUIV (OR a (OR b c)) (OR (OR a b) c)"