freescale porting, work in progress

diff --git a/helm/software/matita/contribs/ng_assembly/depends b/helm/software/matita/contribs/ng_assembly/depends
index 0cc002df4c8279ab8331e10292d3e198d306057f..be208f0d6fee9f10680782026f4cee88ba6e4cee 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/depends
+++ b/helm/software/matita/contribs/ng_assembly/depends
@@ -4,7 +4,7 @@ freescale/memory_bits.ma freescale/memory_trees.ma
 common/prod_lemmas.ma common/prod.ma num/bool_lemmas.ma
 num/bool.ma common/theory.ma
 freescale/table_HCS08_tests.ma freescale/opcode.ma freescale/table_HCS08.ma
-compiler/preast_tree.ma common/string.ma compiler/ast_type.ma
+compiler/preast_tree.ma common/string.ma compiler/ast_type.ma num/word32.ma
 freescale/multivm.ma freescale/load_write.ma
 common/ascii_lemmas1.ma common/ascii.ma
 common/nat_to_num.ma common/nat.ma num/word32.ma
@@ -28,7 +28,7 @@ freescale/table_RS08_tests.ma freescale/opcode.ma freescale/table_RS08.ma
 freescale/translation.ma common/option.ma freescale/table_HC05.ma freescale/table_HC08.ma freescale/table_HCS08.ma freescale/table_RS08.ma
 freescale/memory_abs.ma freescale/memory_bits.ma freescale/memory_func.ma freescale/memory_trees.ma
 num/word32_lemmas.ma num/word16_lemmas.ma num/word32.ma
-test_errori.ma num/exadecim.ma num/exadecim_lemmas.ma
+test_errori.ma 
 freescale/memory_struct.ma num/byte8.ma num/oct.ma
 freescale/model.ma freescale/status.ma
 freescale/table_HC05.ma common/list.ma freescale/opcode_base.ma

diff --git a/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma
index 08f88acfd62088f3b3bdd991b66eb03b872a510a..be8b1665f7c6488bdfc64b67009b22832c7d18e4 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/bitrigesim_lemmas.ma
@@ -855,3 +855,690 @@ nlemma eq_to_eqbit : ∀t1,t2.t1 = t2 → eq_bit t1 t2 = true.
  ##| ##32: napply eq_to_eqbit32
  ##]
 nqed.
+
+nlemma decidable_bit1 : ∀x:bitrigesim.decidable (t00 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##1: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit2 : ∀x:bitrigesim.decidable (t01 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##2: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit3 : ∀x:bitrigesim.decidable (t02 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##3: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit4 : ∀x:bitrigesim.decidable (t03 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##4: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit5 : ∀x:bitrigesim.decidable (t04 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##5: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit6 : ∀x:bitrigesim.decidable (t05 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##6: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit7 : ∀x:bitrigesim.decidable (t06 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##7: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit8 : ∀x:bitrigesim.decidable (t07 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##8: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit9 : ∀x:bitrigesim.decidable (t08 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##9: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit10 : ∀x:bitrigesim.decidable (t09 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##10: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit11 : ∀x:bitrigesim.decidable (t0A = x).
+ #x; nnormalize; nelim x;
+ ##[ ##11: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit12 : ∀x:bitrigesim.decidable (t0B = x).
+ #x; nnormalize; nelim x;
+ ##[ ##12: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit13 : ∀x:bitrigesim.decidable (t0C = x).
+ #x; nnormalize; nelim x;
+ ##[ ##13: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit14 : ∀x:bitrigesim.decidable (t0D = x).
+ #x; nnormalize; nelim x;
+ ##[ ##14: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit15 : ∀x:bitrigesim.decidable (t0E = x).
+ #x; nnormalize; nelim x;
+ ##[ ##15: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit16 : ∀x:bitrigesim.decidable (t0F = x).
+ #x; nnormalize; nelim x;
+ ##[ ##16: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit17 : ∀x:bitrigesim.decidable (t10 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##17: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit18 : ∀x:bitrigesim.decidable (t11 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##18: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit19 : ∀x:bitrigesim.decidable (t12 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##19: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit20 : ∀x:bitrigesim.decidable (t13 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##20: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit21 : ∀x:bitrigesim.decidable (t14 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##21: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit22 : ∀x:bitrigesim.decidable (t15 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##22: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit23 : ∀x:bitrigesim.decidable (t16 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##23: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit24 : ∀x:bitrigesim.decidable (t17 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##24: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit25 : ∀x:bitrigesim.decidable (t18 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##25: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit26 : ∀x:bitrigesim.decidable (t19 = x).
+ #x; nnormalize; nelim x;
+ ##[ ##26: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit27 : ∀x:bitrigesim.decidable (t1A = x).
+ #x; nnormalize; nelim x;
+ ##[ ##27: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit28 : ∀x:bitrigesim.decidable (t1B = x).
+ #x; nnormalize; nelim x;
+ ##[ ##28: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit29 : ∀x:bitrigesim.decidable (t1C = x).
+ #x; nnormalize; nelim x;
+ ##[ ##29: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit30 : ∀x:bitrigesim.decidable (t1D = x).
+ #x; nnormalize; nelim x;
+ ##[ ##30: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit31 : ∀x:bitrigesim.decidable (t1E = x).
+ #x; nnormalize; nelim x;
+ ##[ ##31: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit32 : ∀x:bitrigesim.decidable (t1F = x).
+ #x; nnormalize; nelim x;
+ ##[ ##32: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bitrigesim_destruct … H)
+ ##]
+nqed.
+
+nlemma decidable_bit : ∀x,y:bitrigesim.decidable (x = y).
+ #x; nnormalize; nelim x;
+ ##[ ##1: napply decidable_bit1
+ ##| ##2: napply decidable_bit2
+ ##| ##3: napply decidable_bit3
+ ##| ##4: napply decidable_bit4
+ ##| ##5: napply decidable_bit5
+ ##| ##6: napply decidable_bit6
+ ##| ##7: napply decidable_bit7
+ ##| ##8: napply decidable_bit8
+ ##| ##9: napply decidable_bit9
+ ##| ##10: napply decidable_bit10
+ ##| ##11: napply decidable_bit11
+ ##| ##12: napply decidable_bit12
+ ##| ##13: napply decidable_bit13
+ ##| ##14: napply decidable_bit14
+ ##| ##15: napply decidable_bit15
+ ##| ##16: napply decidable_bit16
+ ##| ##17: napply decidable_bit17
+ ##| ##18: napply decidable_bit18
+ ##| ##19: napply decidable_bit19
+ ##| ##20: napply decidable_bit20
+ ##| ##21: napply decidable_bit21
+ ##| ##22: napply decidable_bit22
+ ##| ##23: napply decidable_bit23
+ ##| ##24: napply decidable_bit24
+ ##| ##25: napply decidable_bit25
+ ##| ##26: napply decidable_bit26
+ ##| ##27: napply decidable_bit27
+ ##| ##28: napply decidable_bit28
+ ##| ##29: napply decidable_bit29
+ ##| ##30: napply decidable_bit30
+ ##| ##31: napply decidable_bit31
+ ##| ##32: napply decidable_bit32
+ ##]
+nqed.
+
+nlemma neqbit_to_neq1 : ∀t2.eq_bit t00 t2 = false → t00 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##1: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq2 : ∀t2.eq_bit t01 t2 = false → t01 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##2: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq3 : ∀t2.eq_bit t02 t2 = false → t02 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##3: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq4 : ∀t2.eq_bit t03 t2 = false → t03 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##4: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq5 : ∀t2.eq_bit t04 t2 = false → t04 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##5: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq6 : ∀t2.eq_bit t05 t2 = false → t05 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##6: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq7 : ∀t2.eq_bit t06 t2 = false → t06 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##7: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq8 : ∀t2.eq_bit t07 t2 = false → t07 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##8: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq9 : ∀t2.eq_bit t08 t2 = false → t08 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##9: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq10 : ∀t2.eq_bit t09 t2 = false → t09 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##10: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq11 : ∀t2.eq_bit t0A t2 = false → t0A ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##11: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq12 : ∀t2.eq_bit t0B t2 = false → t0B ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##12: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq13 : ∀t2.eq_bit t0C t2 = false → t0C ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##13: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq14 : ∀t2.eq_bit t0D t2 = false → t0D ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##14: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq15 : ∀t2.eq_bit t0E t2 = false → t0E ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##15: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq16 : ∀t2.eq_bit t0F t2 = false → t0F ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##16: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq17 : ∀t2.eq_bit t10 t2 = false → t10 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##17: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq18 : ∀t2.eq_bit t11 t2 = false → t11 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##18: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq19 : ∀t2.eq_bit t12 t2 = false → t12 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##19: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq20 : ∀t2.eq_bit t13 t2 = false → t13 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##20: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq21 : ∀t2.eq_bit t14 t2 = false → t14 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##21: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq22 : ∀t2.eq_bit t15 t2 = false → t15 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##22: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq23 : ∀t2.eq_bit t16 t2 = false → t16 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##23: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq24 : ∀t2.eq_bit t17 t2 = false → t17 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##24: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq25 : ∀t2.eq_bit t18 t2 = false → t18 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##25: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq26 : ∀t2.eq_bit t19 t2 = false → t19 ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##26: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq27 : ∀t2.eq_bit t1A t2 = false → t1A ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##27: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq28 : ∀t2.eq_bit t1B t2 = false → t1B ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##28: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq29 : ∀t2.eq_bit t1C t2 = false → t1C ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##29: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq30 : ∀t2.eq_bit t1D t2 = false → t1D ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##30: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq31 : ∀t2.eq_bit t1E t2 = false → t1E ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##31: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq32 : ∀t2.eq_bit t1F t2 = false → t1F ≠ t2.
+ #t2; ncases t2; nnormalize; #H;
+ ##[ ##32: napply  (bool_destruct … H)
+ ##| ##*: #H1; napply False_ind; napply (bitrigesim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neqbit_to_neq : ∀t1,t2.eq_bit t1 t2 = false → t1 ≠ t2.
+ #t1; nelim t1;
+ ##[ ##1: napply neqbit_to_neq1
+ ##| ##2: napply neqbit_to_neq2
+ ##| ##3: napply neqbit_to_neq3
+ ##| ##4: napply neqbit_to_neq4
+ ##| ##5: napply neqbit_to_neq5
+ ##| ##6: napply neqbit_to_neq6
+ ##| ##7: napply neqbit_to_neq7
+ ##| ##8: napply neqbit_to_neq8
+ ##| ##9: napply neqbit_to_neq9
+ ##| ##10: napply neqbit_to_neq10
+ ##| ##11: napply neqbit_to_neq11
+ ##| ##12: napply neqbit_to_neq12
+ ##| ##13: napply neqbit_to_neq13
+ ##| ##14: napply neqbit_to_neq14
+ ##| ##15: napply neqbit_to_neq15
+ ##| ##16: napply neqbit_to_neq16
+ ##| ##17: napply neqbit_to_neq17
+ ##| ##18: napply neqbit_to_neq18
+ ##| ##19: napply neqbit_to_neq19
+ ##| ##20: napply neqbit_to_neq20
+ ##| ##21: napply neqbit_to_neq21
+ ##| ##22: napply neqbit_to_neq22
+ ##| ##23: napply neqbit_to_neq23
+ ##| ##24: napply neqbit_to_neq24
+ ##| ##25: napply neqbit_to_neq25
+ ##| ##26: napply neqbit_to_neq26
+ ##| ##27: napply neqbit_to_neq27
+ ##| ##28: napply neqbit_to_neq28
+ ##| ##29: napply neqbit_to_neq29
+ ##| ##30: napply neqbit_to_neq30
+ ##| ##31: napply neqbit_to_neq31
+ ##| ##32: napply neqbit_to_neq32
+ ##]
+nqed.
+
+nlemma neq_to_neqbit1 : ∀t2.t00 ≠ t2 → eq_bit t00 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##1: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit2 : ∀t2.t01 ≠ t2 → eq_bit t01 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##2: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit3 : ∀t2.t02 ≠ t2 → eq_bit t02 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##3: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit4 : ∀t2.t03 ≠ t2 → eq_bit t03 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##4: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit5 : ∀t2.t04 ≠ t2 → eq_bit t04 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##5: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit6 : ∀t2.t05 ≠ t2 → eq_bit t05 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##6: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit7 : ∀t2.t06 ≠ t2 → eq_bit t06 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##7: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit8 : ∀t2.t07 ≠ t2 → eq_bit t07 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##8: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit9 : ∀t2.t08 ≠ t2 → eq_bit t08 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##9: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit10 : ∀t2.t09 ≠ t2 → eq_bit t09 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##10: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit11 : ∀t2.t0A ≠ t2 → eq_bit t0A t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##11: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit12 : ∀t2.t0B ≠ t2 → eq_bit t0B t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##12: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit13 : ∀t2.t0C ≠ t2 → eq_bit t0C t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##13: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit14 : ∀t2.t0D ≠ t2 → eq_bit t0D t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##14: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit15 : ∀t2.t0E ≠ t2 → eq_bit t0E t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##15: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit16 : ∀t2.t0F ≠ t2 → eq_bit t0F t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##16: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit17 : ∀t2.t10 ≠ t2 → eq_bit t10 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##17: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit18 : ∀t2.t11 ≠ t2 → eq_bit t11 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##18: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit19 : ∀t2.t12 ≠ t2 → eq_bit t12 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##19: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit20 : ∀t2.t13 ≠ t2 → eq_bit t13 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##20: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit21 : ∀t2.t14 ≠ t2 → eq_bit t14 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##21: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit22 : ∀t2.t15 ≠ t2 → eq_bit t15 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##22: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit23 : ∀t2.t16 ≠ t2 → eq_bit t16 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##23: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit24 : ∀t2.t17 ≠ t2 → eq_bit t17 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##24: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit25 : ∀t2.t18 ≠ t2 → eq_bit t18 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##25: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit26 : ∀t2.t19 ≠ t2 → eq_bit t19 t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##26: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit27 : ∀t2.t1A ≠ t2 → eq_bit t1A t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##27: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit28 : ∀t2.t1B ≠ t2 → eq_bit t1B t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##28: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit29 : ∀t2.t1C ≠ t2 → eq_bit t1C t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##29: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit30 : ∀t2.t1D ≠ t2 → eq_bit t1D t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##30: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit31 : ∀t2.t1E ≠ t2 → eq_bit t1E t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##31: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit32 : ∀t2.t1F ≠ t2 → eq_bit t1F t2 = false.
+ #t2; ncases t2; nnormalize; #H; ##[ ##32: nelim (H (refl_eq …)) ##| ##*: napply refl_eq ##]
+nqed.
+
+nlemma neq_to_neqbit : ∀t1,t2.t1 ≠ t2 → eq_bit t1 t2 = false.
+ #t1; nelim t1;
+ ##[ ##1: napply neq_to_neqbit1
+ ##| ##2: napply neq_to_neqbit2
+ ##| ##3: napply neq_to_neqbit3
+ ##| ##4: napply neq_to_neqbit4
+ ##| ##5: napply neq_to_neqbit5
+ ##| ##6: napply neq_to_neqbit6
+ ##| ##7: napply neq_to_neqbit7
+ ##| ##8: napply neq_to_neqbit8
+ ##| ##9: napply neq_to_neqbit9
+ ##| ##10: napply neq_to_neqbit10
+ ##| ##11: napply neq_to_neqbit11
+ ##| ##12: napply neq_to_neqbit12
+ ##| ##13: napply neq_to_neqbit13
+ ##| ##14: napply neq_to_neqbit14
+ ##| ##15: napply neq_to_neqbit15
+ ##| ##16: napply neq_to_neqbit16
+ ##| ##17: napply neq_to_neqbit17
+ ##| ##18: napply neq_to_neqbit18
+ ##| ##19: napply neq_to_neqbit19
+ ##| ##20: napply neq_to_neqbit20
+ ##| ##21: napply neq_to_neqbit21
+ ##| ##22: napply neq_to_neqbit22
+ ##| ##23: napply neq_to_neqbit23
+ ##| ##24: napply neq_to_neqbit24
+ ##| ##25: napply neq_to_neqbit25
+ ##| ##26: napply neq_to_neqbit26
+ ##| ##27: napply neq_to_neqbit27
+ ##| ##28: napply neq_to_neqbit28
+ ##| ##29: napply neq_to_neqbit29
+ ##| ##30: napply neq_to_neqbit30
+ ##| ##31: napply neq_to_neqbit31
+ ##| ##32: napply neq_to_neqbit32
+ ##]
+nqed.

diff --git a/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma
index 859082d8ed078c268bbbcea6f001806a0531bc0b..07d9c7001ec2df069c3e75661ddb11f0271330b0 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/bool_lemmas.ma
@@ -132,6 +132,36 @@ nlemma eq_to_eqbool : ∀b1,b2.b1 = b2 → eq_bool b1 b2 = true.
  ##]
 nqed.
 
+nlemma decidable_bool : ∀x,y:bool.decidable (x = y).
+ #x; #y;
+ nnormalize;
+ nelim x;
+ nelim y;
+ ##[ ##1,4: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (bool_destruct … H)
+ ##]
+nqed.
+
+nlemma neqbool_to_neq : ∀b1,b2:bool.(eq_bool b1 b2 = false) → (b1 ≠ b2).
+ #b1; #b2;
+ ncases b1;
+ ncases b2;
+ nnormalize;
+ ##[ ##1,4: #H; napply (bool_destruct … H)
+ ##| ##*: #H; #H1; napply (bool_destruct … H1)
+ ##]
+nqed.
+
+nlemma neq_to_neqbool : ∀b1,b2.b1 ≠ b2 → eq_bool b1 b2 = false.
+ #b1; #b2;
+ ncases b1;
+ ncases b2;
+ nnormalize;
+ ##[ ##1,4: #H; nelim (H (refl_eq …))
+ ##| ##*: #H; napply refl_eq
+ ##]
+nqed.
+
 nlemma andb_true_true_l: ∀b1,b2.(b1 ⊗ b2) = true → b1 = true.
  #b1; #b2;
  ncases b1;

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 1d32793cc3e1b724048df8598278c2572fe18047..c71eed49b0d04b0c544878cc749bf9e4f5db5a4e 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/byte8_lemmas.ma
@@ -286,3 +286,69 @@ nlemma eq_to_eqb8 : ∀b1,b2.b1 = b2 → eq_b8 b1 b2 = true.
  nnormalize;
  napply refl_eq.
 nqed.
+
+nlemma decidable_b8_aux1 : ∀e1,e2,e3,e4.e1 ≠ e3 → 〈e1,e2〉 ≠ 〈e3,e4〉.
+ #e1; #e2; #e3; #e4;
+ nnormalize; #H; #H1;
+ napply (H (byte8_destruct_1 … H1)).
+nqed.
+
+nlemma decidable_b8_aux2 : ∀e1,e2,e3,e4.e2 ≠ e4 → 〈e1,e2〉 ≠ 〈e3,e4〉.
+ #e1; #e2; #e3; #e4;
+ nnormalize; #H; #H1;
+ napply (H (byte8_destruct_2 … H1)).
+nqed.
+
+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))
+          ##| ##1: #H1; nrewrite > H; nrewrite > H1;
+                        napply (or_introl … (refl_eq ? 〈e3,e4〉))
+          ##]
+ ##]
+nqed.
+
+nlemma neqb8_to_neq : ∀b1,b2:byte8.(eq_b8 b1 b2 = false) → (b1 ≠ b2).
+ #b1; #b2;
+ nelim b1;
+ nelim 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) …);
+ ##[ ##1: #H1; napply (decidable_b8_aux1 … (neqex_to_neq … H1))
+ ##| ##2: #H1; napply (decidable_b8_aux2 … (neqex_to_neq … H1))
+ ##]
+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)
+          ##| ##1: #H2; nrewrite > H1 in H:(%);
+                   nrewrite > H2;
+                   #H; nelim (H (refl_eq …))
+          ##]
+ ##]
+nqed.
+
+nlemma neq_to_neqb8 : ∀b1,b2.b1 ≠ b2 → eq_b8 b1 b2 = false.
+ #b1; #b2;
+ 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) …);
+ ##[ ##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);
+          nnormalize; napply refl_eq
+ ##]
+nqed.

diff --git a/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma
index ccfbdd73c0437f3daa1c86d01907dfc7e3ba009e..47847434eb909921c312e8f7c383433cfa530972 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/exadecim_lemmas.ma
@@ -461,3 +461,33 @@ nlemma eq_to_eqex : ∀e1,e2.e1 = e2 → eq_ex e1 e2 = true.
  ##| ##*: #H; napply (exadecim_destruct … H)
  ##]
 nqed.
+
+nlemma decidable_ex : ∀x,y:exadecim.decidable (x = y).
+ #x; #y;
+ nnormalize;
+ nelim x;
+ nelim y;
+ ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (exadecim_destruct … H)
+ ##]
+nqed.
+
+nlemma neqex_to_neq : ∀e1,e2:exadecim.(eq_ex e1 e2 = false) → (e1 ≠ e2).
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
+ nnormalize;
+ ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; napply (bool_destruct … H)
+ ##| ##*: #H; #H1; napply (exadecim_destruct … H1)
+ ##]
+nqed.
+
+nlemma neq_to_neqex : ∀e1,e2.e1 ≠ e2 → eq_ex e1 e2 = false.
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
+ nnormalize;
+ ##[ ##1,18,35,52,69,86,103,120,137,154,171,188,205,222,239,256: #H; nelim (H (refl_eq …))
+ ##| ##*: #H; napply refl_eq
+ ##]
+nqed.

diff --git a/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma
index 6f651b8428b3f12fe41f5b7d970fc076720c3329..dc7e96f8909985aefaaf55e26058195590488a25 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma
@@ -121,3 +121,33 @@ nlemma eq_to_eqoct : ∀n1,n2.n1 = n2 → eq_oct n1 n2 = true.
  ##| ##*: #H; napply (oct_destruct … H)
  ##]
 nqed.
+
+nlemma decidable_oct : ∀x,y:oct.decidable (x = y).
+ #x; #y;
+ nnormalize;
+ nelim x;
+ nelim y;
+ ##[ ##1,10,19,28,37,46,55,64: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (oct_destruct … H)
+ ##]
+nqed.
+
+nlemma neqoct_to_neq : ∀n1,n2.eq_oct n1 n2 = false → n1 ≠ n2.
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
+ nnormalize;
+ ##[ ##1,10,19,28,37,46,55,64: #H; napply (bool_destruct … H)
+ ##| ##*: #H; #H1; napply (oct_destruct … H1)
+ ##]
+nqed.
+
+nlemma neq_to_neqoct : ∀n1,n2.n1 ≠ n2 → eq_oct n1 n2 = false.
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
+ nnormalize;
+ ##[ ##1,10,19,28,37,46,55,64: #H; nelim (H (refl_eq …))
+ ##| ##*: #H; napply refl_eq
+ ##]
+nqed.

diff --git a/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma
index 8d3bdf5d3d685efa6f03f236f4957585fbac4e0f..d32aa0f3e83321a3f3ca587424a15c1782f1a51a 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/quatern_lemmas.ma
@@ -93,3 +93,33 @@ nlemma eq_to_eqqu : ∀n1,n2.n1 = n2 → eq_qu n1 n2 = true.
  ##| ##*: #H; napply (quatern_destruct … H)
  ##]
 nqed.
+
+nlemma decidable_qu : ∀x,y:quatern.decidable (x = y).
+ #x; #y;
+ nnormalize;
+ nelim x;
+ nelim y;
+ ##[ ##1,6,11,16: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (quatern_destruct … H)
+ ##]
+nqed.
+
+nlemma neqqu_to_neq : ∀n1,n2.eq_qu n1 n2 = false → n1 ≠ n2.
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
+ nnormalize;
+ ##[ ##1,6,11,16: #H; napply (bool_destruct … H)
+ ##| ##*: #H; #H1; napply (quatern_destruct … H1)
+ ##]
+nqed.
+
+nlemma neq_to_neqqu : ∀n1,n2.n1 ≠ n2 → eq_qu n1 n2 = false.
+ #n1; #n2;
+ ncases n1;
+ ncases n2;
+ nnormalize;
+ ##[ ##1,6,11,16: #H; nelim (H (refl_eq …))
+ ##| ##*: #H; napply refl_eq
+ ##]
+nqed.

diff --git a/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma
index 4570f3291f01fc2231110a80cf90085ba1177184..a9c59de32ac9d21f11f2b4fc247d8ec46a5389fd 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word16_lemmas.ma
@@ -325,3 +325,69 @@ nlemma eq_to_eqw16 : ∀w1,w2.w1 = w2 → eq_w16 w1 w2 = true.
  nnormalize;
  napply refl_eq.
 nqed.
+
+nlemma decidable_w16_aux1 : ∀b1,b2,b3,b4.b1 ≠ b3 → 〈b1:b2〉 ≠ 〈b3:b4〉.
+ #b1; #b2; #b3; #b4;
+ nnormalize; #H; #H1;
+ napply (H (word16_destruct_1 … H1)).
+nqed.
+
+nlemma decidable_w16_aux2 : ∀b1,b2,b3,b4.b2 ≠ b4 → 〈b1:b2〉 ≠ 〈b3:b4〉.
+ #b1; #b2; #b3; #b4;
+ nnormalize; #H; #H1;
+ napply (H (word16_destruct_2 … H1)).
+nqed.
+
+nlemma decidable_w16 : ∀x,y:word16.decidable (x = y).
+ #x; nelim x; #b1; #b2;
+ #y; nelim y; #b3; #b4;
+ nnormalize;
+ napply (or_elim (b1 = b3) (b1 ≠ b3) ? (decidable_b8 b1 b3) …);
+ ##[ ##2: #H; napply (or_intror … (decidable_w16_aux1 b1 b2 b3 b4 H))
+ ##| ##1: #H; napply (or_elim (b2 = b4) (b2 ≠ b4) ? (decidable_b8 b2 b4) …);
+          ##[ ##2: #H1; napply (or_intror … (decidable_w16_aux2 b1 b2 b3 b4 H1))
+          ##| ##1: #H1; nrewrite > H; nrewrite > H1;
+                        napply (or_introl … (refl_eq ? 〈b3:b4〉))
+          ##]
+ ##]
+nqed.
+
+nlemma neqw16_to_neq : ∀w1,w2:word16.(eq_w16 w1 w2 = false) → (w1 ≠ w2).
+ #w1; #w2;
+ nelim w1;
+ nelim w2;
+ #b1; #b2; #b3; #b4;
+ nchange with ((((eq_b8 b3 b1) ⊗ (eq_b8 b4 b2)) = false) → ?);
+ #H;
+ napply (or_elim ((eq_b8 b3 b1) = false) ((eq_b8 b4 b2) = false) ? (andb_false … H) …);
+ ##[ ##1: #H1; napply (decidable_w16_aux1 … (neqb8_to_neq … H1))
+ ##| ##2: #H1; napply (decidable_w16_aux2 … (neqb8_to_neq … H1))
+ ##]
+nqed.
+
+nlemma word16_destruct : ∀b1,b2,b3,b4.〈b1:b2〉 ≠ 〈b3:b4〉 → b1 ≠ b3 ∨ b2 ≠ b4.
+ #b1; #b2; #b3; #b4;
+ nnormalize; #H;
+ napply (or_elim (b1 = b3) (b1 ≠ b3) ? (decidable_b8 b1 b3) …);
+ ##[ ##2: #H1; napply (or_introl … H1)
+ ##| ##1: #H1; napply (or_elim (b2 = b4) (b2 ≠ b4) ? (decidable_b8 b2 b4) …);
+          ##[ ##2: #H2; napply (or_intror … H2)
+          ##| ##1: #H2; nrewrite > H1 in H:(%);
+                   nrewrite > H2;
+                   #H; nelim (H (refl_eq …))
+          ##]
+ ##]
+nqed.
+
+nlemma neq_to_neqw16 : ∀w1,w2.w1 ≠ w2 → eq_w16 w1 w2 = false.
+ #w1; #w2;
+ nelim w1; #b1; #b2;
+ nelim w2; #b3; #b4;
+ #H; nchange with (((eq_b8 b1 b3) ⊗ (eq_b8 b2 b4)) = false);
+ napply (or_elim (b1 ≠ b3) (b2 ≠ b4) ? (word16_destruct … H) …);
+ ##[ ##1: #H1; nrewrite > (neq_to_neqb8 … H1); nnormalize; napply refl_eq
+ ##| ##2: #H1; nrewrite > (neq_to_neqb8 … H1);
+          nrewrite > (symmetric_andbool (eq_b8 b1 b3) false);
+          nnormalize; napply refl_eq
+ ##]
+nqed.

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 98639a64257f3eb82d09654b46ee5b7dab359851..2bb6c0b24c00df969d64e8307699d6c3e64a01f2 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/word32_lemmas.ma
@@ -325,3 +325,69 @@ nlemma eq_to_eqw32 : ∀dw1,dw2.dw1 = dw2 → eq_w32 dw1 dw2 = true.
  nnormalize;
  napply refl_eq.
 nqed.
+
+nlemma decidable_w32_aux1 : ∀w1,w2,w3,w4.w1 ≠ w3 → 〈w1.w2〉 ≠ 〈w3.w4〉.
+ #w1; #w2; #w3; #w4;
+ nnormalize; #H; #H1;
+ napply (H (word32_destruct_1 … H1)).
+nqed.
+
+nlemma decidable_w32_aux2 : ∀w1,w2,w3,w4.w2 ≠ w4 → 〈w1.w2〉 ≠ 〈w3.w4〉.
+ #w1; #w2; #w3; #w4;
+ nnormalize; #H; #H1;
+ napply (H (word32_destruct_2 … H1)).
+nqed.
+
+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))
+          ##| ##1: #H1; nrewrite > H; nrewrite > H1;
+                        napply (or_introl … (refl_eq ? 〈w3.w4〉))
+          ##]
+ ##]
+nqed.
+
+nlemma neqw32_to_neq : ∀dw1,dw2:word32.(eq_w32 dw1 dw2 = false) → (dw1 ≠ dw2).
+ #dw1; #dw2;
+ nelim dw1;
+ nelim dw2;
+ #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) …);
+ ##[ ##1: #H1; napply (decidable_w32_aux1 … (neqw16_to_neq … H1))
+ ##| ##2: #H1; napply (decidable_w32_aux2 … (neqw16_to_neq … H1))
+ ##]
+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)
+          ##| ##1: #H2; nrewrite > H1 in H:(%);
+                   nrewrite > H2;
+                   #H; nelim (H (refl_eq …))
+          ##]
+ ##]
+nqed.
+
+nlemma neq_to_neqw32 : ∀dw1,dw2.dw1 ≠ dw2 → eq_w32 dw1 dw2 = false.
+ #dw1; #dw2;
+ 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) …);
+ ##[ ##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);
+          nnormalize; napply refl_eq
+ ##]
+nqed.

diff --git a/helm/software/matita/contribs/ng_assembly/test_errori.ma b/helm/software/matita/contribs/ng_assembly/test_errori.ma
index 921c1b505a26636a662551ab407f055db1d3c22a..4236c5c6341f7c0b93e878951e88b04880244284 100644 (file)
--- a/helm/software/matita/contribs/ng_assembly/test_errori.ma
+++ b/helm/software/matita/contribs/ng_assembly/test_errori.ma
@@ -1,28 +1,4 @@
 
-(* congettura, come si fa? *)
-include "num/exadecim.ma".
-include "num/exadecim_lemmas.ma".
-
-nlemma decidable_ex_aux1 : ∀x.∀H:x0 = x.(x0 = x) ∨ (x0 ≠ x).
- #x; nelim x;
- ##[ ##1: #H; napply (or_introl … H)
- ##| ##*: #H; nelim (exadecim_destruct … H)
- ##]. nqed.
-
-nlemma decidable_ex0 : ∀x:exadecim.decidable (x0 = x).
- #x;
- nelim x;
- nnormalize;
- napply (Or_ind (x0=x) (x0≠x) ? ? …);
- ##[ ##1: napply (or_introl (x0 = x0) (x0 ≠ x0) (refl_eq …))
- ##| ##*:
- 
- nnormalize;
- nelim x;
- ##[ ##1: nelim y;
-          ##[ ##1: napply (or_introl (? = ?) (? ≠ ?) (refl_eq …))
-          ##| ##*:
-
 (*include "utility/utility.ma".
 
 nlemma fold_right_neList2_aux3 :