helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.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:                                                         *)
  19 (*   Cosimo Oliboni, oliboni@cs.unibo.it                                  *)
  20 (*                                                                        *)
  21 (* Questo materiale fa parte della tesi:                                  *)
  22 (*   "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale"   *)
  23 (*                                                                        *)
  24 (*                    data ultima modifica 15/11/2007                     *)
  25 (* ********************************************************************** *)
  26
  27 include "freescale/theory.ma".
  28 include "freescale/bool.ma".
  29
  30 (* ******** *)
  31 (* BOOLEANI *)
  32 (* ******** *)
  33
  34 ndefinition bool_destruct :
  35  Πb1,b2:bool.ΠP:Prop.b1 = b2 →
  36  match b1 with
  37   [ true ⇒ match b2 with [ true ⇒ P → P | false ⇒ P ]
  38   | false ⇒ match b2 with [ true ⇒ P | false ⇒ P → P ]
  39   ].
  40  #b1; #b2; #P;
  41  nelim b1;
  42  nelim b2;
  43  nnormalize;
  44  #H;
  45  ##[ ##2: napply (False_ind ??);
  46           nchange with (match true with [ true ⇒ False | false ⇒ True]);
  47           nrewrite > H;
  48           nnormalize;
  49           napply I
  50  ##| ##3: napply (False_ind ??);
  51           nchange with (match true with [ true ⇒ False | false ⇒ True]);
  52           nrewrite < H;
  53           nnormalize;
  54           napply I
  55  ##| ##1,4: napply (λx:P.x)
  56  ##]
  57 nqed.
  58
  59 nlemma symmetric_eqbool : symmetricT bool bool eq_bool.
  60  #b1; #b2;
  61  nelim b1;
  62  nelim b2;
  63  nnormalize;
  64  napply (refl_eq ??).
  65 nqed.
  66
  67 nlemma symmetric_andbool : symmetricT bool bool and_bool.
  68  #b1; #b2;
  69  nelim b1;
  70  nelim b2;
  71  nnormalize;
  72  napply (refl_eq ??).
  73 nqed.
  74
  75 nlemma associative_andbool : ∀b1,b2,b3.((b1 ⊗ b2) ⊗ b3) = (b1 ⊗ (b2 ⊗ b3)).
  76  #b1; #b2; #b3;
  77  nelim b1;
  78  nelim b2;
  79  nelim b3;
  80  nnormalize;
  81  napply (refl_eq ??).
  82 nqed.
  83
  84 nlemma symmetric_orbool : symmetricT bool bool or_bool.
  85  #b1; #b2;
  86  nelim b1;
  87  nelim b2;
  88  nnormalize;
  89  napply (refl_eq ??).
  90 nqed.
  91
  92 nlemma associative_orbool : ∀b1,b2,b3.((b1 ⊕ b2) ⊕ b3) = (b1 ⊕ (b2 ⊕ b3)).
  93  #b1; #b2; #b3;
  94  nelim b1;
  95  nelim b2;
  96  nelim b3;
  97  nnormalize;
  98  napply (refl_eq ??).
  99 nqed.
 100
 101 nlemma symmetric_xorbool : symmetricT bool bool xor_bool.
 102  #b1; #b2;
 103  nelim b1;
 104  nelim b2;
 105  nnormalize;
 106  napply (refl_eq ??).
 107 nqed.
 108
 109 nlemma associative_orbool : ∀b1,b2,b3.((b1 ⊙ b2) ⊙ b3) = (b1 ⊙ (b2 ⊙ b3)).
 110  #b1; #b2; #b3;
 111  nelim b1;
 112  nelim b2;
 113  nelim b3;
 114  nnormalize;
 115  napply (refl_eq ??).
 116 nqed.
 117
 118 nlemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2).
 119  #b1; #b2; #H;
 120  nletin K ≝ (bool_destruct ?? (b1 = b2) H);
 121  nelim b1 in K:(%) ⊢ %;
 122  nelim b2;
 123  nnormalize;
 124  ##[ ##2,3: #H; napply H
 125  ##| ##1,4: #H; napply (refl_eq ??)
 126  ##]
 127 nqed.
 128
 129 nlemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true.
 130  #b1; #b2; #H;
 131  nletin K ≝ (bool_destruct ?? (eq_bool b1 b2 = true) H);
 132  nelim b1 in K:(%) ⊢ %;
 133  nelim b2;
 134  nnormalize;
 135  ##[ ##2,3: #H; napply H
 136  ##| ##1,4: #H; napply (refl_eq ??)
 137  ##]
 138 nqed.
 139
 140 nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true.
 141  #b1; #b2; #H;
 142  nletin K ≝ (bool_destruct ?? (b1 = true) H);
 143  nelim b1 in K:(%) ⊢ %;
 144  nelim b2;
 145  nnormalize;
 146  ##[ ##3,4: #H; napply H
 147  ##| ##1,2: #H; napply (refl_eq ??)
 148  ##]
 149 nqed.
 150
 151 nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true.
 152  #b1; #b2; #H;
 153  nletin K ≝ (bool_destruct ?? (b2 = true) H);
 154  nelim b1 in K:(%) ⊢ %;
 155  nelim b2;
 156  nnormalize;
 157  ##[ ##2,4: #H; napply H
 158  ##| ##1,3: #H; napply (refl_eq ??)
 159  ##]
 160 nqed.
 161
 162 nlemma orb_false_false_l : ∀b1,b2:bool.(b1 ⊕ b2) = false → b1 = false.
 163  #b1; #b2; #H;
 164  nletin K ≝ (bool_destruct ?? (b1 = false) H);
 165  nelim b1 in K:(%) ⊢ %;
 166  nelim b2;
 167  nnormalize;
 168  ##[ ##1,2,3: #H; napply H
 169  ##| ##4: #H; napply (refl_eq ??)
 170  ##]
 171 nqed.
 172
 173 nlemma orb_false_false_r : ∀b1,b2:bool.(b1 ⊕ b2) = false → b2 = false.
 174  #b1; #b2; #H;
 175  nletin K ≝ (bool_destruct ?? (b2 = false) H);
 176  nelim b1 in K:(%) ⊢ %;
 177  nelim b2;
 178  nnormalize;
 179  ##[ ##1,2,3: #H; napply H
 180  ##| ##4: #H; napply (refl_eq ??)
 181  ##]
 182 nqed.