|
5545
|
1 |
(* Title: HOL/ex/BinEx.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 1998 University of Cambridge
|
|
5199
|
5 |
|
|
5545
|
6 |
Definition of normal form for proving that binary arithmetic on
|
|
|
7 |
ormalized operands yields normalized results.
|
|
|
8 |
|
|
|
9 |
Normal means no leading 0s on positive numbers and no leading 1s on negatives.
|
|
|
10 |
*)
|
|
|
11 |
|
|
|
12 |
BinEx = Bin +
|
|
|
13 |
|
|
|
14 |
consts normal :: bin set
|
|
|
15 |
|
|
|
16 |
inductive "normal"
|
|
|
17 |
intrs
|
|
|
18 |
|
|
|
19 |
Pls "Pls: normal"
|
|
|
20 |
|
|
|
21 |
Min "Min: normal"
|
|
|
22 |
|
|
|
23 |
BIT_F "[| w: normal; w ~= Pls |] ==> w BIT False : normal"
|
|
|
24 |
|
|
|
25 |
BIT_T "[| w: normal; w ~= Min |] ==> w BIT True : normal"
|
|
|
26 |
|
|
|
27 |
end
|