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;
 120  ncases b1;
 121  ncases b2;
 122  nnormalize;
 123  ##[ ##1,4: #H; napply (refl_eq ??)
 124  ##| ##*: #H; napply (bool_destruct ??? H)
 125  ##]
 126 nqed.
 127
 128 nlemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true.
 129  #b1; #b2;
 130  ncases b1;
 131  ncases b2;
 132  nnormalize;
 133  ##[ ##1,4: #H; napply (refl_eq ??)
 134  ##| ##*: #H; napply (bool_destruct ??? H)
 135  ##]
 136 nqed.
 137
 138 nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true.
 139  #b1; #b2;
 140  ncases b1;
 141  ncases b2;
 142  nnormalize;
 143  ##[ ##1,2: #H; napply (refl_eq ??)
 144  ##| ##*: #H; napply (bool_destruct ??? H)
 145  ##]
 146 nqed.
 147
 148 nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true.
 149  #b1; #b2;
 150  ncases b1;
 151  ncases b2;
 152  nnormalize;
 153  ##[ ##1,3: #H; napply (refl_eq ??)
 154  ##| ##*: #H; napply (bool_destruct ??? H)
 155  ##]
 156 nqed.
 157
 158 nlemma orb_false_false_l : ∀b1,b2:bool.(b1 ⊕ b2) = false → b1 = false.
 159  #b1; #b2;
 160  ncases b1;
 161  ncases b2;
 162  nnormalize;
 163  ##[ ##4: #H; napply (refl_eq ??)
 164  ##| ##*: #H; napply (bool_destruct ??? H)
 165  ##]
 166 nqed.
 167
 168 nlemma orb_false_false_r : ∀b1,b2:bool.(b1 ⊕ b2) = false → b2 = false.
 169  #b1; #b2;
 170  ncases b1;
 171  ncases b2;
 172  nnormalize;
 173  ##[ ##4: #H; napply (refl_eq ??)
 174  ##| ##*: #H; napply (bool_destruct ??? H)
 175  ##]
 176 nqed.