Last change
on this file since 234 was
234,
checked in by mulligan, 10 years ago

Division and modulus implemented. All necessary orders on naturals
completed. More operations on bitvectors (and general operations that
apply to all vectors) implemented.

File size:
1.3 KB

Line  

1  include "List.ma". 

2  include "Vector.ma". 

3  include "Nat.ma". 

4  include "Bool.ma". 

5  

6  ndefinition BitVector ≝ λn: Nat. Vector Bool n. 

7  ndefinition Bit ≝ BitVector (S Z). 

8  ndefinition Nibble ≝ BitVector (S (S (S (S Z)))). 

9  ndefinition Byte7 ≝ BitVector (S (S (S (S (S (S (S Z))))))). 

10  ndefinition Byte ≝ BitVector (S (S (S (S (S (S (S (S Z)))))))). 

11  ndefinition Word ≝ BitVector (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S Z)))))))))))))))). 

12  

13  ndefinition zero ≝ 

14  λn: Nat. 

15  replicate Bool n False. 

16  

17  ndefinition conjunction ≝ 

18  λn: Nat. 

19  λb: BitVector n. 

20  λc: BitVector n. 

21  zip Bool Bool Bool n conjunction b c. 

22  

23  ndefinition inclusive_disjunction ≝ 

24  λn: Nat. 

25  λb: BitVector n. 

26  λc: BitVector n. 

27  zip Bool Bool Bool n inclusive_disjunction b c. 

28  

29  ndefinition exclusive_disjunction ≝ 

30  λn: Nat. 

31  λb: BitVector n. 

32  λc: BitVector n. 

33  zip Bool Bool Bool n exclusive_disjunction b c. 

34  

35  ndefinition complement ≝ 

36  λn: Nat. 

37  λb: BitVector n. 

38  map Bool Bool n (negation) b. 

39  

40  ndefinition divide_with_remainder ≝ 

41  λm, n: Nat. 

42  mk_Cartesian Nat Nat (m ÷ n) (modulus m n). 

43  

44  nlet rec bitvector_of_nat_aux (n: Nat): List Nat ≝ 

45  let div_rem ≝ divide_with_remainder n (S (S Z)) in 

46  let div ≝ first Nat Nat div_rem in 

47  let rem ≝ second Nat Nat div_rem in 

48  Empty Nat. 

Note: See
TracBrowser
for help on using the repository browser.