(no commit message)

[helm.git] / helm / software / matita / contribs / ng_assembly / num / byte8_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma
index c71eed49b0d04b0c544878cc749bf9e4f5db5a4e..10a100965499406152a732ea05e3748a25e342f0 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma
@@ -16,7 +16,7 @@
 (*                          Progetto FreeScale                            *)
 (*                                                                        *)
 (*   Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
-(*   Ultima modifica: 05/08/2009                                          *)
+(*   Sviluppo: 2008-2010                                                  *)
 (*                                                                        *)
 (* ********************************************************************** *)
 
@@ -143,20 +143,14 @@ nlemma symmetric_plusb8_dc_dc : ∀b1,b2,c.plus_b8_dc_dc b1 b2 c = plus_b8_dc_dc
  nelim b2;
  #e3; #e4;
  nchange with (
-  match plus_ex_dc_dc e2 e4 c with
-   [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with
-    [ pair h c' ⇒ pair … 〈h,l〉 c' ]] =
-  match plus_ex_dc_dc e4 e2 c with
-   [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with
-    [ pair h c' ⇒ pair … 〈h,l〉 c' ]]);
+  match plus_ex_dc_dc e2 e4 c with [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with [ pair h c' ⇒ pair … 〈h,l〉 c' ]] =
+  match plus_ex_dc_dc e4 e2 c with [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with [ pair h c' ⇒ pair … 〈h,l〉 c' ]]);
  nrewrite > (symmetric_plusex_dc_dc e4 e2 c);
  ncases (plus_ex_dc_dc e2 e4 c);
  #e5; #c1;
  nchange with (
-  match plus_ex_dc_dc e1 e3 c1 with
-   [ pair h c' ⇒ pair … 〈h,e5〉 c' ] =
-  match plus_ex_dc_dc e3 e1 c1 with
-   [ pair h c' ⇒ pair … 〈h,e5〉 c' ]);
+  match plus_ex_dc_dc e1 e3 c1 with [ pair h c' ⇒ pair … 〈h,e5〉 c' ] =
+  match plus_ex_dc_dc e3 e1 c1 with [ pair h c' ⇒ pair … 〈h,e5〉 c' ]);
  nrewrite > (symmetric_plusex_dc_dc e1 e3 c1);
  napply refl_eq.
 nqed.
@@ -168,10 +162,8 @@ nlemma symmetric_plusb8_dc_d : ∀b1,b2,c.plus_b8_dc_d b1 b2 c = plus_b8_dc_d b2
  nelim b2;
  #e3; #e4;
  nchange with (
-  match plus_ex_dc_dc e2 e4 c with
-   [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] =
-  match plus_ex_dc_dc e4 e2 c with
-   [ pair l c ⇒ 〈plus_ex_dc_d e3 e1 c,l〉 ]);
+  match plus_ex_dc_dc e2 e4 c with [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] =
+  match plus_ex_dc_dc e4 e2 c with [ pair l c ⇒ 〈plus_ex_dc_d e3 e1 c,l〉 ]);
  nrewrite > (symmetric_plusex_dc_dc e4 e2 c);
  ncases (plus_ex_dc_dc e2 e4 c);
  #e5; #c1;
@@ -201,20 +193,14 @@ nlemma symmetric_plusb8_d_dc : ∀b1,b2.plus_b8_d_dc b1 b2 = plus_b8_d_dc b2 b1.
  nelim b2;
  #e3; #e4;
  nchange with (
-  match plus_ex_d_dc e2 e4 with
-   [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with
-    [ pair h c' ⇒ pair … 〈h,l〉 c' ]] =
-  match plus_ex_d_dc e4 e2 with
-   [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with
-    [ pair h c' ⇒ pair … 〈h,l〉 c' ]]);
+  match plus_ex_d_dc e2 e4 with [ pair l c ⇒ match plus_ex_dc_dc e1 e3 c with [ pair h c' ⇒ pair … 〈h,l〉 c' ]] =
+  match plus_ex_d_dc e4 e2 with [ pair l c ⇒ match plus_ex_dc_dc e3 e1 c with [ pair h c' ⇒ pair … 〈h,l〉 c' ]]);
  nrewrite > (symmetric_plusex_d_dc e4 e2);
  ncases (plus_ex_d_dc e2 e4);
  #e5; #c;
  nchange with (
-  match plus_ex_dc_dc e1 e3 c with
-   [ pair h c' ⇒ pair … 〈h,e5〉 c' ] =
-  match plus_ex_dc_dc e3 e1 c with
-   [ pair h c' ⇒ pair … 〈h,e5〉 c' ]);
+  match plus_ex_dc_dc e1 e3 c with [ pair h c' ⇒ pair … 〈h,e5〉 c' ] =
+  match plus_ex_dc_dc e3 e1 c with [ pair h c' ⇒ pair … 〈h,e5〉 c' ]);
  nrewrite > (symmetric_plusex_dc_dc e1 e3 c);
  napply refl_eq.
 nqed.
@@ -226,10 +212,8 @@ nlemma symmetric_plusb8_d_d : ∀b1,b2.plus_b8_d_d b1 b2 = plus_b8_d_d b2 b1.
  nelim b2;
  #e3; #e4;
  nchange with (
-  match plus_ex_d_dc e2 e4 with
-   [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] =
-  match plus_ex_d_dc e4 e2 with
-   [ pair l c ⇒ 〈plus_ex_dc_d e3 e1 c,l〉 ]);
+  match plus_ex_d_dc e2 e4 with [ pair l c ⇒ 〈plus_ex_dc_d e1 e3 c,l〉 ] =
+  match plus_ex_d_dc e4 e2 with [ pair l c ⇒ 〈plus_ex_dc_d e3 e1 c,l〉 ]);
  nrewrite > (symmetric_plusex_d_dc e4 e2);
  ncases (plus_ex_d_dc e2 e4);
  #e5; #c;
@@ -303,12 +287,12 @@ nlemma decidable_b8 : ∀x,y:byte8.decidable (x = y).
  #x; nelim x; #e1; #e2;
  #y; nelim y; #e3; #e4;
  nnormalize;
- napply (or_elim (e1 = e3) (e1 ≠ e3) ? (decidable_ex e1 e3) …);
- ##[ ##2: #H; napply (or_intror … (decidable_b8_aux1 e1 e2 e3 e4 H))
- ##| ##1: #H; napply (or_elim (e2 = e4) (e2 ≠ e4) ? (decidable_ex e2 e4) …);
-          ##[ ##2: #H1; napply (or_intror … (decidable_b8_aux2 e1 e2 e3 e4 H1))
+ napply (or2_elim (e1 = e3) (e1 ≠ e3) ? (decidable_ex e1 e3) …);
+ ##[ ##2: #H; napply (or2_intro2 … (decidable_b8_aux1 e1 e2 e3 e4 H))
+ ##| ##1: #H; napply (or2_elim (e2 = e4) (e2 ≠ e4) ? (decidable_ex e2 e4) …);
+          ##[ ##2: #H1; napply (or2_intro2 … (decidable_b8_aux2 e1 e2 e3 e4 H1))
           ##| ##1: #H1; nrewrite > H; nrewrite > H1;
-                        napply (or_introl … (refl_eq ? 〈e3,e4〉))
+                        napply (or2_intro1 … (refl_eq ? 〈e3,e4〉))
           ##]
  ##]
 nqed.
@@ -320,7 +304,7 @@ nlemma neqb8_to_neq : ∀b1,b2:byte8.(eq_b8 b1 b2 = false) → (b1 ≠ b2).
  #e1; #e2; #e3; #e4;
  nchange with ((((eq_ex e3 e1) ⊗ (eq_ex e4 e2)) = false) → ?);
  #H;
- napply (or_elim ((eq_ex e3 e1) = false) ((eq_ex e4 e2) = false) ? (andb_false … H) …);
+ napply (or2_elim ((eq_ex e3 e1) = false) ((eq_ex e4 e2) = false) ? (andb_false2 … H) …);
  ##[ ##1: #H1; napply (decidable_b8_aux1 … (neqex_to_neq … H1))
  ##| ##2: #H1; napply (decidable_b8_aux2 … (neqex_to_neq … H1))
  ##]
@@ -329,10 +313,10 @@ nqed.
 nlemma byte8_destruct : ∀e1,e2,e3,e4.〈e1,e2〉 ≠ 〈e3,e4〉 → e1 ≠ e3 ∨ e2 ≠ e4.
  #e1; #e2; #e3; #e4;
  nnormalize; #H;
- napply (or_elim (e1 = e3) (e1 ≠ e3) ? (decidable_ex e1 e3) …);
- ##[ ##2: #H1; napply (or_introl … H1)
- ##| ##1: #H1; napply (or_elim (e2 = e4) (e2 ≠ e4) ? (decidable_ex e2 e4) …);
-          ##[ ##2: #H2; napply (or_intror … H2)
+ napply (or2_elim (e1 = e3) (e1 ≠ e3) ? (decidable_ex e1 e3) …);
+ ##[ ##2: #H1; napply (or2_intro1 … H1)
+ ##| ##1: #H1; napply (or2_elim (e2 = e4) (e2 ≠ e4) ? (decidable_ex e2 e4) …);
+          ##[ ##2: #H2; napply (or2_intro2 … H2)
           ##| ##1: #H2; nrewrite > H1 in H:(%);
                    nrewrite > H2;
                    #H; nelim (H (refl_eq …))
@@ -345,7 +329,7 @@ nlemma neq_to_neqb8 : ∀b1,b2.b1 ≠ b2 → eq_b8 b1 b2 = false.
  nelim b1; #e1; #e2;
  nelim b2; #e3; #e4;
  #H; nchange with (((eq_ex e1 e3) ⊗ (eq_ex e2 e4)) = false);
- napply (or_elim (e1 ≠ e3) (e2 ≠ e4) ? (byte8_destruct … H) …);
+ napply (or2_elim (e1 ≠ e3) (e2 ≠ e4) ? (byte8_destruct … H) …);
  ##[ ##1: #H1; nrewrite > (neq_to_neqex … H1); nnormalize; napply refl_eq
  ##| ##2: #H1; nrewrite > (neq_to_neqex … H1);
           nrewrite > (symmetric_andbool (eq_ex e1 e3) false);