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 nipkow
Thu, 13 Apr 2000 10:30:28 +0200
changeset 8698 8812dad6ef12
parent 6920 c912740c3545
child 9297 bafe45732b10
permissions -rw-r--r--
made mod_less_divisor a simplification rule.

(*  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 = Main +

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