Last change
on this file since 234 was
234,
checked in by mulligan, 9 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.