Last change
on this file since 256 was
246,
checked in by mulligan, 9 years ago

Added physical file (Arithmetic) for arithmetic on bit vectors, and
added sparse bitvector trie for modelling 8051 memory.

File size:
1009 bytes

Line  

1  include "Universes.ma". 

2  

3  ninductive Bool: Type[0] ≝ 

4  True: Bool 

5   False: Bool. 

6  

7  nlet rec if_then_else (A: Type[0]) (b: Bool) (t: A) (f: A) on b ≝ 

8  match b with 

9  [ True ⇒ t 

10   False ⇒ f 

11  ]. 

12  

13  notation "hvbox(b ? t : f)" 

14  non associative with precedence 83 

15  for @{ 'if_then_else $b $t $f }. 

16  

17  interpretation "If_then_else" 'if_then_else b t f = (if_then_else ? b t f). 

18  

19  ndefinition conjunction ≝ 

20  λb, c: Bool. 

21  match b with 

22  [ True ⇒ c 

23   False ⇒ False 

24  ]. 

25  

26  nlet rec inclusive_disjunction (b: Bool) (c: Bool) on b ≝ 

27  match b with 

28  [ True ⇒ True 

29   False ⇒ c 

30  ]. 

31  

32  nlet rec exclusive_disjunction (b: Bool) (c: Bool) on b ≝ 

33  match b with 

34  [ True ⇒ 

35  match c with 

36  [ False ⇒ True 

37   True ⇒ False 

38  ] 

39   False ⇒ 

40  match c with 

41  [ False ⇒ False 

42   True ⇒ True 

43  ] 

44  ]. 

45  

46  nlet rec negation (b: Bool) on b ≝ 

47  match b with 

48  [ True ⇒ False 

49   False ⇒ True 

50  ]. 

51  

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