helm/software/matita/contribs/ng_assembly/emulator/opcodes/opcode_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/HC05_opcode_lemmas.ma".
  24 include "emulator/opcodes/HC05_instr_mode_lemmas.ma".
  25 include "emulator/opcodes/HC08_opcode_lemmas.ma".
  26 include "emulator/opcodes/HC08_instr_mode_lemmas.ma".
  27 include "emulator/opcodes/HCS08_opcode_lemmas.ma".
  28 include "emulator/opcodes/RS08_opcode_lemmas.ma".
  29 include "emulator/opcodes/RS08_instr_mode_lemmas.ma".
  30 include "emulator/opcodes/IP2022_opcode_lemmas.ma".
  31 include "emulator/opcodes/IP2022_instr_mode_lemmas.ma".
  32 include "emulator/opcodes/opcode.ma".
  33
  34 nlemma eq_to_eqop : ∀m.∀n1,n2.(n1 = n2) → (eq_op m n1 n2 = true).
  35  #m; nelim m;
  36  ##[ ##1: napply eq_to_eqHC05op
  37  ##| ##2: napply eq_to_eqHC08op
  38  ##| ##3: napply eq_to_eqHCS08op
  39  ##| ##4: napply eq_to_eqRS08op
  40  ##| ##5: napply eq_to_eqIP2022op
  41  ##]
  42 nqed.
  43
  44 nlemma neqop_to_neq : ∀m.∀n1,n2.(eq_op m n1 n2 = false) → (n1 ≠ n2).
  45  #m; nelim m;
  46  ##[ ##1: napply neqHC05op_to_neq
  47  ##| ##2: napply neqHC08op_to_neq
  48  ##| ##3: napply neqHCS08op_to_neq
  49  ##| ##4: napply neqRS08op_to_neq
  50  ##| ##5: napply neqIP2022op_to_neq
  51  ##]
  52 nqed.
  53
  54 nlemma eqop_to_eq : ∀m.∀n1,n2.(eq_op m n1 n2 = true) → (n1 = n2).
  55  #m; nelim m;
  56  ##[ ##1: napply eqHC05op_to_eq
  57  ##| ##2: napply eqHC08op_to_eq
  58  ##| ##3: napply eqHCS08op_to_eq
  59  ##| ##4: napply eqRS08op_to_eq
  60  ##| ##5: napply eqIP2022op_to_eq
  61  ##]
  62 nqed.
  63
  64 nlemma neq_to_neqop : ∀m.∀n1,n2.(n1 ≠ n2) → (eq_op m n1 n2 = false).
  65  #m; nelim m;
  66  ##[ ##1: napply neq_to_neqHC05op
  67  ##| ##2: napply neq_to_neqHC08op
  68  ##| ##3: napply neq_to_neqHCS08op
  69  ##| ##4: napply neq_to_neqRS08op
  70  ##| ##5: napply neq_to_neqIP2022op
  71  ##]
  72 nqed.
  73
  74 nlemma decidable_op : ∀m.∀x,y:aux_op_type m.decidable (x = y).
  75  #m; nelim m;
  76  ##[ ##1: napply decidable_HC05op
  77  ##| ##2: napply decidable_HC08op
  78  ##| ##3: napply decidable_HCS08op
  79  ##| ##4: napply decidable_RS08op
  80  ##| ##5: napply decidable_IP2022op
  81  ##]
  82 nqed.
  83
  84 nlemma symmetric_eqop : ∀m.symmetricT (aux_op_type m) bool (eq_op m).
  85  #m; nelim m;
  86  ##[ ##1: napply symmetric_eqHC05op
  87  ##| ##2: napply symmetric_eqHC08op
  88  ##| ##3: napply symmetric_eqHCS08op
  89  ##| ##4: napply symmetric_eqRS08op
  90  ##| ##5: napply symmetric_eqIP2022op
  91  ##]
  92 nqed.
  93
  94 nlemma eq_to_eqim : ∀m.∀n1,n2.(n1 = n2) → (eq_im m n1 n2 = true).
  95  #m; nelim m;
  96  ##[ ##1: napply eq_to_eqHC05im
  97  ##| ##2: napply eq_to_eqHC08im
  98  ##| ##3: napply eq_to_eqHC08im
  99  ##| ##4: napply eq_to_eqRS08im
 100  ##| ##5: napply eq_to_eqIP2022im
 101  ##]
 102 nqed.
 103
 104 nlemma neqim_to_neq : ∀m.∀n1,n2.(eq_im m n1 n2 = false) → (n1 ≠ n2).
 105  #m; nelim m;
 106  ##[ ##1: napply neqHC05im_to_neq
 107  ##| ##2: napply neqHC08im_to_neq
 108  ##| ##3: napply neqHC08im_to_neq
 109  ##| ##4: napply neqRS08im_to_neq
 110  ##| ##5: napply neqIP2022im_to_neq
 111  ##]
 112 nqed.
 113
 114 nlemma eqim_to_eq : ∀m.∀n1,n2.(eq_im m n1 n2 = true) → (n1 = n2).
 115  #m; nelim m;
 116  ##[ ##1: napply eqHC05im_to_eq
 117  ##| ##2: napply eqHC08im_to_eq
 118  ##| ##3: napply eqHC08im_to_eq
 119  ##| ##4: napply eqRS08im_to_eq
 120  ##| ##5: napply eqIP2022im_to_eq
 121  ##]
 122 nqed.
 123
 124 nlemma neq_to_neqim : ∀m.∀n1,n2.(n1 ≠ n2) → (eq_im m n1 n2 = false).
 125  #m; nelim m;
 126  ##[ ##1: napply neq_to_neqHC05im
 127  ##| ##2: napply neq_to_neqHC08im
 128  ##| ##3: napply neq_to_neqHC08im
 129  ##| ##4: napply neq_to_neqRS08im
 130  ##| ##5: napply neq_to_neqIP2022im
 131  ##]
 132 nqed.
 133
 134 nlemma decidable_im : ∀m.∀x,y:aux_im_type m.decidable (x = y).
 135  #m; nelim m;
 136  ##[ ##1: napply decidable_HC05im
 137  ##| ##2: napply decidable_HC08im
 138  ##| ##3: napply decidable_HC08im
 139  ##| ##4: napply decidable_RS08im
 140  ##| ##5: napply decidable_IP2022im
 141  ##]
 142 nqed.
 143
 144 nlemma symmetric_eqim : ∀m.symmetricT (aux_im_type m) bool (eq_im m).
 145  #m; nelim m;
 146  ##[ ##1: napply symmetric_eqHC05im
 147  ##| ##2: napply symmetric_eqHC08im
 148  ##| ##3: napply symmetric_eqHC08im
 149  ##| ##4: napply symmetric_eqRS08im
 150  ##| ##5: napply symmetric_eqIP2022im
 151  ##]
 152 nqed.