source: Deliverables/D4.1/Matita/Bool.ma @ 249

Last change on this file since 249 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 
1include "Universes.ma".
2
3ninductive Bool: Type[0] ≝
4  True: Bool
5| False: Bool.
6
7nlet 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   
13notation "hvbox(b ? t : f)"
14  non associative with precedence 83
15  for @{ 'if_then_else $b $t $f }.
16 
17interpretation "If_then_else" 'if_then_else b t f = (if_then_else ? b t f).
18
19ndefinition conjunction ≝
20  λb, c: Bool.
21    match b with
22      [ True ⇒ c
23      | False ⇒ False
24      ].
25   
26nlet rec inclusive_disjunction (b: Bool) (c: Bool) on b ≝
27  match b with
28    [ True ⇒ True
29    | False ⇒ c
30    ].
31
32nlet 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
46nlet 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.