author wenzelm
Thu, 13 Jul 2000 11:41:40 +0200
changeset 9297 bafe45732b10
parent 6920 c912740c3545
child 11024 23bf8d787b04
permissions -rw-r--r--

(*  Title:      HOL/ex/BinEx.thy
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

Definition of normal form for proving that binary arithmetic on
normalized operands yields normalized results.

Normal means no leading 0s on positive numbers and no leading 1s on negatives.

BinEx = Main +

consts normal :: bin set
inductive "normal"

    Pls  "Pls: normal"

    Min  "Min: normal"

    BIT_F  "[| w: normal; w ~= Pls |] ==> w BIT False : normal"

    BIT_T  "[| w: normal; w ~= Min |] ==> w BIT True : normal"