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_aux ≝
  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
  41 ndefinition bool_destruct : bool_destruct_aux.
  42  #b1; #b2; #P;
  43  nelim b1;
  44  nelim b2;
  45  nnormalize;
  46  #H;
  47  ##[ ##2: napply (False_ind ??);
  48           nchange with (match true with [ true ⇒ False | false ⇒ True]);
  49           nrewrite > H;
  50           nnormalize;
  51           napply I
  52  ##| ##3: napply (False_ind ??);
  53           nchange with (match true with [ true ⇒ False | false ⇒ True]);
  54           nrewrite < H;
  55           nnormalize;
  56           napply I
  57  ##| ##1,4: napply (λx:P.x)
  58  ##]
  59 nqed.
  60
  61 nlemma symmetric_eqbool : symmetricT bool bool eq_bool.
  62  #b1; #b2;
  63  nelim b1;
  64  nelim b2;
  65  nnormalize;
  66  napply (refl_eq ??).
  67 nqed.
  68
  69 nlemma symmetric_andbool : symmetricT bool bool and_bool.
  70  #b1; #b2;
  71  nelim b1;
  72  nelim b2;
  73  nnormalize;
  74  napply (refl_eq ??).
  75 nqed.
  76
  77 nlemma associative_andbool : ∀b1,b2,b3.((b1 ⊗ b2) ⊗ b3) = (b1 ⊗ (b2 ⊗ b3)).
  78  #b1; #b2; #b3;
  79  nelim b1;
  80  nelim b2;
  81  nelim b3;
  82  nnormalize;
  83  napply (refl_eq ??).
  84 nqed.
  85
  86 nlemma symmetric_orbool : symmetricT bool bool or_bool.
  87  #b1; #b2;
  88  nelim b1;
  89  nelim b2;
  90  nnormalize;
  91  napply (refl_eq ??).
  92 nqed.
  93
  94 nlemma associative_orbool : ∀b1,b2,b3.((b1 ⊕ b2) ⊕ b3) = (b1 ⊕ (b2 ⊕ b3)).
  95  #b1; #b2; #b3;
  96  nelim b1;
  97  nelim b2;
  98  nelim b3;
  99  nnormalize;
 100  napply (refl_eq ??).
 101 nqed.
 102
 103 nlemma symmetric_xorbool : symmetricT bool bool xor_bool.
 104  #b1; #b2;
 105  nelim b1;
 106  nelim b2;
 107  nnormalize;
 108  napply (refl_eq ??).
 109 nqed.
 110
 111 nlemma associative_orbool : ∀b1,b2,b3.((b1 ⊙ b2) ⊙ b3) = (b1 ⊙ (b2 ⊙ b3)).
 112  #b1; #b2; #b3;
 113  nelim b1;
 114  nelim b2;
 115  nelim b3;
 116  nnormalize;
 117  napply (refl_eq ??).
 118 nqed.
 119
 120 nlemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2).
 121  #b1; #b2;
 122  ncases b1;
 123  ncases b2;
 124  nnormalize;
 125  ##[ ##1,4: #H; napply (refl_eq ??)
 126  ##| ##*: #H; napply (bool_destruct ??? H)
 127  ##]
 128 nqed.
 129
 130 nlemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true.
 131  #b1; #b2;
 132  ncases b1;
 133  ncases b2;
 134  nnormalize;
 135  ##[ ##1,4: #H; napply (refl_eq ??)
 136  ##| ##*: #H; napply (bool_destruct ??? H)
 137  ##]
 138 nqed.
 139
 140 nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true.
 141  #b1; #b2;
 142  ncases b1;
 143  ncases b2;
 144  nnormalize;
 145  ##[ ##1,2: #H; napply (refl_eq ??)
 146  ##| ##*: #H; napply (bool_destruct ??? H)
 147  ##]
 148 nqed.
 149
 150 nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true.
 151  #b1; #b2;
 152  ncases b1;
 153  ncases b2;
 154  nnormalize;
 155  ##[ ##1,3: #H; napply (refl_eq ??)
 156  ##| ##*: #H; napply (bool_destruct ??? H)
 157  ##]
 158 nqed.
 159
 160 nlemma orb_false_false_l : ∀b1,b2:bool.(b1 ⊕ b2) = false → b1 = false.
 161  #b1; #b2;
 162  ncases b1;
 163  ncases b2;
 164  nnormalize;
 165  ##[ ##4: #H; napply (refl_eq ??)
 166  ##| ##*: #H; napply (bool_destruct ??? H)
 167  ##]
 168 nqed.
 169
 170 nlemma orb_false_false_r : ∀b1,b2:bool.(b1 ⊕ b2) = false → b2 = false.
 171  #b1; #b2;
 172  ncases b1;
 173  ncases b2;
 174  nnormalize;
 175  ##[ ##4: #H; napply (refl_eq ??)
 176  ##| ##*: #H; napply (bool_destruct ??? H)
 177  ##]
 178 nqed.