]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/ng_assembly/num/bool.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / ng_assembly / num / bool.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* ********************************************************************** *)
16 (*                          Progetto FreeScale                            *)
17 (*                                                                        *)
18 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
19 (*   Sviluppo: 2008-2010                                                  *)
20 (*                                                                        *)
21 (* ********************************************************************** *)
22
23 include "common/theory.ma".
24
25 (* ******** *)
26 (* BOOLEANI *)
27 (* ******** *)
28
29 ninductive bool : Type ≝ 
30   true : bool
31 | false : bool.
32
33 (* operatori booleani *)
34
35 ndefinition eq_bool ≝
36 λb1,b2:bool.match b1 with
37  [ true ⇒ match b2 with [ true ⇒ true | false ⇒ false ]
38  | false ⇒ match b2 with [ true ⇒ false | false ⇒ true ]
39  ].
40
41 ndefinition not_bool ≝
42 λb:bool.match b with [ true ⇒ false | false ⇒ true ].
43
44 ndefinition and_bool ≝
45 λb1,b2:bool.match b1 with
46  [ true ⇒ b2 | false ⇒ false ].
47
48 ndefinition or_bool ≝
49 λb1,b2:bool.match b1 with
50  [ true ⇒ true | false ⇒ b2 ].
51
52 ndefinition xor_bool ≝
53 λb1,b2:bool.match b1 with
54  [ true ⇒ not_bool b2
55  | false ⇒ b2 ].
56
57 (* \ominus *)
58 notation "hvbox(⊖ a)" non associative with precedence 36
59  for @{ 'not_bool $a }.
60 interpretation "not_bool" 'not_bool x = (not_bool x).
61
62 (* \otimes *)
63 notation "hvbox(a break ⊗ b)" left associative with precedence 35
64  for @{ 'and_bool $a $b }.
65 interpretation "and_bool" 'and_bool x y = (and_bool x y).
66
67 (* \oplus *)
68 notation "hvbox(a break ⊕ b)" left associative with precedence 34
69  for @{ 'or_bool $a $b }.
70 interpretation "or_bool" 'or_bool x y = (or_bool x y).
71
72 (* \odot *)
73 notation "hvbox(a break ⊙ b)" left associative with precedence 33
74  for @{ 'xor_bool $a $b }.
75 interpretation "xor_bool" 'xor_bool x y = (xor_bool x y).
76
77 ndefinition boolRelation : Type → Type ≝
78 λA:Type.A → A → bool.