| author | wenzelm |
| Thu, 13 Jul 2000 11:41:40 +0200 | |
| changeset 9297 | bafe45732b10 |
| parent 6920 | c912740c3545 |
| child 11024 | 23bf8d787b04 |
| permissions | -rw-r--r-- |
| paulson@5545 | 1 |
(* Title: HOL/ex/BinEx.thy |
| paulson@5545 | 2 |
ID: $Id$ |
| paulson@5545 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
| paulson@5545 | 4 |
Copyright 1998 University of Cambridge |
| wenzelm@5199 | 5 |
|
| paulson@5545 | 6 |
Definition of normal form for proving that binary arithmetic on |
| wenzelm@9297 | 7 |
normalized operands yields normalized results. |
| paulson@5545 | 8 |
|
| paulson@5545 | 9 |
Normal means no leading 0s on positive numbers and no leading 1s on negatives. |
| paulson@5545 | 10 |
*) |
| paulson@5545 | 11 |
|
| paulson@6920 | 12 |
BinEx = Main + |
| paulson@5545 | 13 |
|
| paulson@5545 | 14 |
consts normal :: bin set |
| paulson@5545 | 15 |
|
| paulson@5545 | 16 |
inductive "normal" |
| paulson@5545 | 17 |
intrs |
| paulson@5545 | 18 |
|
| paulson@5545 | 19 |
Pls "Pls: normal" |
| paulson@5545 | 20 |
|
| paulson@5545 | 21 |
Min "Min: normal" |
| paulson@5545 | 22 |
|
| paulson@5545 | 23 |
BIT_F "[| w: normal; w ~= Pls |] ==> w BIT False : normal" |
| paulson@5545 | 24 |
|
| paulson@5545 | 25 |
BIT_T "[| w: normal; w ~= Min |] ==> w BIT True : normal" |
| paulson@5545 | 26 |
|
| paulson@5545 | 27 |
end |