helm/matita/library/datatypes/bool.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/bool/".
  16
  17 inductive bool : Set \def
  18   | true : bool
  19   | false : bool.
  20
  21 definition notb : bool \to bool \def
  22 \lambda b:bool.
  23  match b with
  24  [ true \Rightarrow false
  25  | false \Rightarrow true ].
  26
  27 interpretation "boolean not" 'not x = (cic:/matita/datatypes/bool/notb.con x).
  28
  29 definition andb : bool \to bool \to bool\def
  30 \lambda b1,b2:bool.
  31  match b1 with
  32  [ true \Rightarrow
  33         match b2 with [true \Rightarrow true | false \Rightarrow false]
  34  | false \Rightarrow false ].
  35
  36 interpretation "boolean and" 'and x y = (cic:/matita/datatypes/bool/andb.con x y).
  37
  38 definition orb : bool \to bool \to bool\def
  39 \lambda b1,b2:bool.
  40  match b1 with
  41  [ true \Rightarrow
  42         match b2 with [true \Rightarrow true | false \Rightarrow false]
  43  | false \Rightarrow false ].
  44
  45 interpretation "boolean or" 'or x y = (cic:/matita/datatypes/bool/orb.con x y).
  46
  47 definition if_then_else : bool \to Prop \to Prop \to Prop \def
  48 \lambda b:bool.\lambda P,Q:Prop.
  49 match b with
  50 [ true \Rightarrow P
  51 | false  \Rightarrow Q].
  52
  53 (*CSC: missing notation for if_then_else *)