matita/matita/contribs/ng_assembly/emulator/opcodes/pseudo_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: Ing. Cosimo Oliboni, oliboni@cs.unibo.it              *)
  19 (*   Sviluppo: 2008-2010                                                  *)
  20 (*                                                                        *)
  21 (* ********************************************************************** *)
  22
  23 include "emulator/opcodes/Freescale_pseudo_lemmas.ma".
  24 include "emulator/opcodes/Freescale_instr_mode_lemmas.ma".
  25 include "emulator/opcodes/IP2022_pseudo_lemmas.ma".
  26 include "emulator/opcodes/IP2022_instr_mode_lemmas.ma".
  27 include "emulator/opcodes/pseudo.ma".
  28
  29 nlemma eq_to_eqpseudo : ∀m.∀n1,n2.(n1 = n2) → (eq_pseudo m n1 n2 = true).
  30  #m; nelim m;
  31  ##[ ##1,2,3,4: napply eq_to_eqFreescalepseudo
  32  ##| ##5: napply eq_to_eqIP2022pseudo
  33  ##]
  34 nqed.
  35
  36 nlemma neqpseudo_to_neq : ∀m.∀n1,n2.(eq_pseudo m n1 n2 = false) → (n1 ≠ n2).
  37  #m; nelim m;
  38  ##[ ##1,2,3,4: napply neqFreescalepseudo_to_neq
  39  ##| ##5: napply neqIP2022pseudo_to_neq
  40  ##]
  41 nqed.
  42
  43 nlemma eqpseudo_to_eq : ∀m.∀n1,n2.(eq_pseudo m n1 n2 = true) → (n1 = n2).
  44  #m; nelim m;
  45  ##[ ##1,2,3,4: napply eqFreescalepseudo_to_eq
  46  ##| ##5: napply eqIP2022pseudo_to_eq
  47  ##]
  48 nqed.
  49
  50 nlemma neq_to_neqpseudo : ∀m.∀n1,n2.(n1 ≠ n2) → (eq_pseudo m n1 n2 = false).
  51  #m; nelim m;
  52  ##[ ##1,2,3,4: napply neq_to_neqFreescalepseudo
  53  ##| ##5: napply neq_to_neqIP2022pseudo
  54  ##]
  55 nqed.
  56
  57 nlemma decidable_pseudo : ∀m.∀x,y:aux_pseudo_type m.decidable (x = y).
  58  #m; nelim m;
  59  ##[ ##1,2,3,4: napply decidable_Freescalepseudo
  60  ##| ##5: napply decidable_IP2022pseudo
  61  ##]
  62 nqed.
  63
  64 nlemma symmetric_eqpseudo : ∀m.symmetricT (aux_pseudo_type m) bool (eq_pseudo m).
  65  #m; nelim m;
  66  ##[ ##1,2,3,4: napply symmetric_eqFreescalepseudo
  67  ##| ##5: napply symmetric_eqIP2022pseudo
  68  ##]
  69 nqed.
  70
  71 nlemma eq_to_eqim : ∀m.∀n1,n2.(n1 = n2) → (eq_im m n1 n2 = true).
  72  #m; nelim m;
  73  ##[ ##1,2,3,4: napply eq_to_eqFreescaleim
  74  ##| ##5: napply eq_to_eqIP2022im
  75  ##]
  76 nqed.
  77
  78 nlemma neqim_to_neq : ∀m.∀n1,n2.(eq_im m n1 n2 = false) → (n1 ≠ n2).
  79  #m; nelim m;
  80  ##[ ##1,2,3,4: napply neqFreescaleim_to_neq
  81  ##| ##5: napply neqIP2022im_to_neq
  82  ##]
  83 nqed.
  84
  85 nlemma eqim_to_eq : ∀m.∀n1,n2.(eq_im m n1 n2 = true) → (n1 = n2).
  86  #m; nelim m;
  87  ##[ ##1,2,3,4: napply eqFreescaleim_to_eq
  88  ##| ##5: napply eqIP2022im_to_eq
  89  ##]
  90 nqed.
  91
  92 nlemma neq_to_neqim : ∀m.∀n1,n2.(n1 ≠ n2) → (eq_im m n1 n2 = false).
  93  #m; nelim m;
  94  ##[ ##1,2,3,4: napply neq_to_neqFreescaleim
  95  ##| ##5: napply neq_to_neqIP2022im
  96  ##]
  97 nqed.
  98
  99 nlemma decidable_im : ∀m.∀x,y:aux_im_type m.decidable (x = y).
 100  #m; nelim m;
 101  ##[ ##1,2,3,4: napply decidable_Freescaleim
 102  ##| ##5: napply decidable_IP2022im
 103  ##]
 104 nqed.
 105
 106 nlemma symmetric_eqim : ∀m.symmetricT (aux_im_type m) bool (eq_im m).
 107  #m; nelim m;
 108  ##[ ##1,2,3,4: napply symmetric_eqFreescaleim
 109  ##| ##5: napply symmetric_eqIP2022im
 110  ##]
 111 nqed.