Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/BinEx.thy
author paulson
Thu, 10 Jun 1999 10:39:38 +0200
changeset 6811 4700ca722bbd
parent 5545 9117a0e2bf31
child 6920 c912740c3545
permissions -rw-r--r--
Always_LeadsTo_pre. Always_LeadsTo_post: new equivalences suggested by Misra

(*  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
ormalized operands yields normalized results.

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

BinEx = Bin +

consts normal :: bin set
  
inductive "normal"
  intrs 

    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"

end
isabelle