freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / bool_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
deleted file mode 100755 (executable)
index bcb09a2..0000000
--- a/helm/software/matita/contribs/ng_assembly/freescale/bool_lemmas.ma
+++ /dev/null
@@ -1,174 +0,0 @@
-(**************************************************************************)
-(*       ___                                                              *)
-(*      ||M||                                                             *)
-(*      ||A||       A project by Andrea Asperti                           *)
-(*      ||T||                                                             *)
-(*      ||I||       Developers:                                           *)
-(*      ||T||         The HELM team.                                      *)
-(*      ||A||         http://helm.cs.unibo.it                             *)
-(*      \   /                                                             *)
-(*       \ /        This file is distributed under the terms of the       *)
-(*        v         GNU General Public License Version 2                  *)
-(*                                                                        *)
-(**************************************************************************)
-
-(* ********************************************************************** *)
-(*                          Progetto FreeScale                            *)
-(*                                                                        *)
-(*   Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it                   *)
-(*     Cosimo Oliboni, oliboni@cs.unibo.it                                *)
-(*                                                                        *)
-(* ********************************************************************** *)
-
-include "freescale/theory.ma".
-include "freescale/bool.ma".
-
-(* ******** *)
-(* BOOLEANI *)
-(* ******** *)
-
-ndefinition bool_destruct_aux ≝
-Πb1,b2:bool.ΠP:Prop.b1 = b2 →
- match b1 with
-  [ true ⇒ match b2 with [ true ⇒ P → P | false ⇒ P ]
-  | false ⇒ match b2 with [ true ⇒ P | false ⇒ P → P ]
-  ].
-
-ndefinition bool_destruct : bool_destruct_aux.
- #b1; #b2; #P;
- nelim b1;
- nelim b2;
- nnormalize;
- #H;
- ##[ ##2: napply False_ind;
-          nchange with (match true with [ true ⇒ False | false ⇒ True]);
-          nrewrite > H;
-          nnormalize;
-          napply I
- ##| ##3: napply False_ind;
-          nchange with (match true with [ true ⇒ False | false ⇒ True]);
-          nrewrite < H;
-          nnormalize;
-          napply I
- ##| ##1,4: napply (λx:P.x)
- ##]
-nqed.
-
-nlemma symmetric_eqbool : symmetricT bool bool eq_bool.
- #b1; #b2;
- nelim b1;
- nelim b2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma symmetric_andbool : symmetricT bool bool and_bool.
- #b1; #b2;
- nelim b1;
- nelim b2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma associative_andbool : ∀b1,b2,b3.((b1 ⊗ b2) ⊗ b3) = (b1 ⊗ (b2 ⊗ b3)).
- #b1; #b2; #b3;
- nelim b1;
- nelim b2;
- nelim b3;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma symmetric_orbool : symmetricT bool bool or_bool.
- #b1; #b2;
- nelim b1;
- nelim b2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma associative_orbool : ∀b1,b2,b3.((b1 ⊕ b2) ⊕ b3) = (b1 ⊕ (b2 ⊕ b3)).
- #b1; #b2; #b3;
- nelim b1;
- nelim b2;
- nelim b3;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma symmetric_xorbool : symmetricT bool bool xor_bool.
- #b1; #b2;
- nelim b1;
- nelim b2;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma associative_xorbool : ∀b1,b2,b3.((b1 ⊙ b2) ⊙ b3) = (b1 ⊙ (b2 ⊙ b3)).
- #b1; #b2; #b3;
- nelim b1;
- nelim b2;
- nelim b3;
- nnormalize;
- napply refl_eq.
-nqed.
-
-nlemma eqbool_to_eq : ∀b1,b2:bool.(eq_bool b1 b2 = true) → (b1 = b2).
- #b1; #b2;
- ncases b1;
- ncases b2;
- nnormalize;
- ##[ ##1,4: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true.
- #b1; #b2;
- ncases b1;
- ncases b2;
- nnormalize;
- ##[ ##1,4: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true.
- #b1; #b2;
- ncases b1;
- ncases b2;
- nnormalize;
- ##[ ##1,2: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma andb_true_true_r: ∀b1,b2.(b1 ⊗ b2) = true → b2 = true.
- #b1; #b2;
- ncases b1;
- ncases b2;
- nnormalize;
- ##[ ##1,3: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma orb_false_false_l : ∀b1,b2:bool.(b1 ⊕ b2) = false → b1 = false.
- #b1; #b2;
- ncases b1;
- ncases b2;
- nnormalize;
- ##[ ##4: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.
-
-nlemma orb_false_false_r : ∀b1,b2:bool.(b1 ⊕ b2) = false → b2 = false.
- #b1; #b2;
- ncases b1;
- ncases b2;
- nnormalize;
- ##[ ##4: #H; napply refl_eq
- ##| ##*: #H; napply (bool_destruct … H)
- ##]
-nqed.