freescale porting, work in progress

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

diff --git a/helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma
index 2bb6c0b24c00df969d64e8307699d6c3e64a01f2..5f42bbc7bc22401e8c01f34dd5cf76b0ed63bd0a 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma
@@ -143,20 +143,14 @@ nlemma symmetric_plusw32_dc_dc : ∀dw1,dw2,c.plus_w32_dc_dc dw1 dw2 c = plus_w3
  nelim dw2;
  #w3; #w4;
  nchange with (
-  match plus_w16_dc_dc w2 w4 c with
-   [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with
-    [ pair h c' ⇒ pair … 〈h.l〉 c' ]] =
-  match plus_w16_dc_dc w4 w2 c with
-   [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with
-    [ pair h c' ⇒ pair … 〈h.l〉 c' ]]);
+  match plus_w16_dc_dc w2 w4 c with [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with [ pair h c' ⇒ pair … 〈h.l〉 c' ]] =
+  match plus_w16_dc_dc w4 w2 c with [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with [ pair h c' ⇒ pair … 〈h.l〉 c' ]]);
  nrewrite > (symmetric_plusw16_dc_dc w4 w2 c);
  ncases (plus_w16_dc_dc w2 w4 c);
  #w5; #c1;
  nchange with (
-  match plus_w16_dc_dc w1 w3 c1 with
-   [ pair h c' ⇒ pair … 〈h.w5〉 c' ] =
-  match plus_w16_dc_dc w3 w1 c1 with
-   [ pair h c' ⇒ pair … 〈h.w5〉 c' ]);
+  match plus_w16_dc_dc w1 w3 c1 with [ pair h c' ⇒ pair … 〈h.w5〉 c' ] =
+  match plus_w16_dc_dc w3 w1 c1 with [ pair h c' ⇒ pair … 〈h.w5〉 c' ]);
  nrewrite > (symmetric_plusw16_dc_dc w1 w3 c1);
  napply refl_eq.
 nqed.
@@ -168,10 +162,8 @@ nlemma symmetric_plusw32_dc_d : ∀dw1,dw2,c.plus_w32_dc_d dw1 dw2 c = plus_w32_
  nelim dw2;
  #w3; #w4;
  nchange with (
-  match plus_w16_dc_dc w2 w4 c with
-   [ pair l c ⇒ 〈plus_w16_dc_d w1 w3 c.l〉 ] =
-  match plus_w16_dc_dc w4 w2 c with
-   [ pair l c ⇒ 〈plus_w16_dc_d w3 w1 c.l〉 ]);
+  match plus_w16_dc_dc w2 w4 c with [ pair l c ⇒ 〈plus_w16_dc_d w1 w3 c.l〉 ] =
+  match plus_w16_dc_dc w4 w2 c with [ pair l c ⇒ 〈plus_w16_dc_d w3 w1 c.l〉 ]);
  nrewrite > (symmetric_plusw16_dc_dc w4 w2 c);
  ncases (plus_w16_dc_dc w2 w4 c);
  #w5; #c1;
@@ -201,20 +193,14 @@ nlemma symmetric_plusw32_d_dc : ∀dw1,dw2.plus_w32_d_dc dw1 dw2 = plus_w32_d_dc
  nelim dw2;
  #w3; #w4;
  nchange with (
-  match plus_w16_d_dc w2 w4 with
-   [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with
-    [ pair h c' ⇒ pair … 〈h.l〉 c' ]] =
-  match plus_w16_d_dc w4 w2 with
-   [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with
-    [ pair h c' ⇒ pair … 〈h.l〉 c' ]]);
+  match plus_w16_d_dc w2 w4 with [ pair l c ⇒ match plus_w16_dc_dc w1 w3 c with [ pair h c' ⇒ pair … 〈h.l〉 c' ]] =
+  match plus_w16_d_dc w4 w2 with [ pair l c ⇒ match plus_w16_dc_dc w3 w1 c with [ pair h c' ⇒ pair … 〈h.l〉 c' ]]);
  nrewrite > (symmetric_plusw16_d_dc w4 w2);
  ncases (plus_w16_d_dc w2 w4);
  #w5; #c;
  nchange with (
-  match plus_w16_dc_dc w1 w3 c with
-   [ pair h c' ⇒ pair … 〈h.w5〉 c' ] =
-  match plus_w16_dc_dc w3 w1 c with
-   [ pair h c' ⇒ pair … 〈h.w5〉 c' ]);
+  match plus_w16_dc_dc w1 w3 c with [ pair h c' ⇒ pair … 〈h.w5〉 c' ] =
+  match plus_w16_dc_dc w3 w1 c with [ pair h c' ⇒ pair … 〈h.w5〉 c' ]);
  nrewrite > (symmetric_plusw16_dc_dc w1 w3 c);
  napply refl_eq.
 nqed.
@@ -226,10 +212,8 @@ nlemma symmetric_plusw32_d_d : ∀dw1,dw2.plus_w32_d_d dw1 dw2 = plus_w32_d_d dw
  nelim dw2;
  #w3; #w4;
  nchange with (
-  match plus_w16_d_dc w2 w4 with
-   [ pair l c ⇒ 〈plus_w16_dc_d w1 w3 c.l〉 ] =
-  match plus_w16_d_dc w4 w2 with
-   [ pair l c ⇒ 〈plus_w16_dc_d w3 w1 c.l〉 ]);
+  match plus_w16_d_dc w2 w4 with [ pair l c ⇒ 〈plus_w16_dc_d w1 w3 c.l〉 ] =
+  match plus_w16_d_dc w4 w2 with [ pair l c ⇒ 〈plus_w16_dc_d w3 w1 c.l〉 ]);
  nrewrite > (symmetric_plusw16_d_dc w4 w2);
  ncases (plus_w16_d_dc w2 w4);
  #w5; #c;
@@ -342,12 +326,12 @@ nlemma decidable_w32 : ∀x,y:word32.decidable (x = y).
  #x; nelim x; #w1; #w2;
  #y; nelim y; #w3; #w4;
  nnormalize;
- napply (or_elim (w1 = w3) (w1 ≠ w3) ? (decidable_w16 w1 w3) …);
- ##[ ##2: #H; napply (or_intror … (decidable_w32_aux1 w1 w2 w3 w4 H))
- ##| ##1: #H; napply (or_elim (w2 = w4) (w2 ≠ w4) ? (decidable_w16 w2 w4) …);
-          ##[ ##2: #H1; napply (or_intror … (decidable_w32_aux2 w1 w2 w3 w4 H1))
+ napply (or2_elim (w1 = w3) (w1 ≠ w3) ? (decidable_w16 w1 w3) …);
+ ##[ ##2: #H; napply (or2_intro2 … (decidable_w32_aux1 w1 w2 w3 w4 H))
+ ##| ##1: #H; napply (or2_elim (w2 = w4) (w2 ≠ w4) ? (decidable_w16 w2 w4) …);
+          ##[ ##2: #H1; napply (or2_intro2 … (decidable_w32_aux2 w1 w2 w3 w4 H1))
           ##| ##1: #H1; nrewrite > H; nrewrite > H1;
-                        napply (or_introl … (refl_eq ? 〈w3.w4〉))
+                        napply (or2_intro1 … (refl_eq ? 〈w3.w4〉))
           ##]
  ##]
 nqed.
@@ -359,7 +343,7 @@ nlemma neqw32_to_neq : ∀dw1,dw2:word32.(eq_w32 dw1 dw2 = false) → (dw1 ≠ d
  #w1; #w2; #w3; #w4;
  nchange with ((((eq_w16 w3 w1) ⊗ (eq_w16 w4 w2)) = false) → ?);
  #H;
- napply (or_elim ((eq_w16 w3 w1) = false) ((eq_w16 w4 w2) = false) ? (andb_false … H) …);
+ napply (or2_elim ((eq_w16 w3 w1) = false) ((eq_w16 w4 w2) = false) ? (andb_false2 … H) …);
  ##[ ##1: #H1; napply (decidable_w32_aux1 … (neqw16_to_neq … H1))
  ##| ##2: #H1; napply (decidable_w32_aux2 … (neqw16_to_neq … H1))
  ##]
@@ -368,10 +352,10 @@ nqed.
 nlemma word32_destruct : ∀w1,w2,w3,w4.〈w1.w2〉 ≠ 〈w3.w4〉 → w1 ≠ w3 ∨ w2 ≠ w4.
  #w1; #w2; #w3; #w4;
  nnormalize; #H;
- napply (or_elim (w1 = w3) (w1 ≠ w3) ? (decidable_w16 w1 w3) …);
- ##[ ##2: #H1; napply (or_introl … H1)
- ##| ##1: #H1; napply (or_elim (w2 = w4) (w2 ≠ w4) ? (decidable_w16 w2 w4) …);
-          ##[ ##2: #H2; napply (or_intror … H2)
+ napply (or2_elim (w1 = w3) (w1 ≠ w3) ? (decidable_w16 w1 w3) …);
+ ##[ ##2: #H1; napply (or2_intro1 … H1)
+ ##| ##1: #H1; napply (or2_elim (w2 = w4) (w2 ≠ w4) ? (decidable_w16 w2 w4) …);
+          ##[ ##2: #H2; napply (or2_intro2 … H2)
           ##| ##1: #H2; nrewrite > H1 in H:(%);
                    nrewrite > H2;
                    #H; nelim (H (refl_eq …))
@@ -384,7 +368,7 @@ nlemma neq_to_neqw32 : ∀dw1,dw2.dw1 ≠ dw2 → eq_w32 dw1 dw2 = false.
  nelim dw1; #w1; #w2;
  nelim dw2; #w3; #w4;
  #H; nchange with (((eq_w16 w1 w3) ⊗ (eq_w16 w2 w4)) = false);
- napply (or_elim (w1 ≠ w3) (w2 ≠ w4) ? (word32_destruct … H) …);
+ napply (or2_elim (w1 ≠ w3) (w2 ≠ w4) ? (word32_destruct … H) …);
  ##[ ##1: #H1; nrewrite > (neq_to_neqw16 … H1); nnormalize; napply refl_eq
  ##| ##2: #H1; nrewrite > (neq_to_neqw16 … H1);
           nrewrite > (symmetric_andbool (eq_w16 w1 w3) false);