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