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

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

Conjunction, disjunction and 'xorjunction' implemented on bitvectors.
Lots of supporting datatypes. Vectors.ma includes some diabolical
dependent type hackery due to Wilmer.

File size: 1004 bytes
Line 
1include "logic/pts.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    ].
Note: See TracBrowser for help on using the repository browser.