X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=matita%2Fcontribs%2Fassembly%2Ffreescale%2Fmemory_struct.ma;fp=matita%2Fcontribs%2Fassembly%2Ffreescale%2Fmemory_struct.ma;h=88323ac2d96891a3fefa54fa5399ac28e5ab4612;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/matita/contribs/assembly/freescale/memory_struct.ma b/matita/contribs/assembly/freescale/memory_struct.ma new file mode 100644 index 000000000..88323ac2d --- /dev/null +++ b/matita/contribs/assembly/freescale/memory_struct.ma @@ -0,0 +1,650 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* ********************************************************************** *) +(* Progetto FreeScale *) +(* *) +(* Sviluppato da: *) +(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* *) +(* Questo materiale fa parte della tesi: *) +(* "Formalizzazione Interattiva dei Microcontroller a 8bit FreeScale" *) +(* *) +(* data ultima modifica 15/11/2007 *) +(* ********************************************************************** *) + +include "freescale/translation.ma". + +(* **************************** *) +(* TIPI PER I MODULI DI MEMORIA *) +(* **************************** *) + +(* tipi di memoria:RAM/ROM/non installata *) +inductive memory_type : Type ≝ + MEM_READ_ONLY: memory_type +| MEM_READ_WRITE: memory_type +| MEM_OUT_OF_BOUND: memory_type. + +(* **************** *) +(* TIPO ARRAY DA 16 *) +(* **************** *) + +(* definizione di un array omogeneo di dimensione 16 *) +inductive Prod16T (T:Type) : Type ≝ +array_16T : T → T → T → T → T → T → T → T → + T → T → T → T → T → T → T → T → + Prod16T T. + +(* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) +(* posso definire un getter a matrice sull'array *) +definition getn_array16T ≝ +λn:exadecim.λT:Type.λp:Prod16T T. + match p with + [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒ + match n with + [ x0 ⇒ e00 | x1 ⇒ e01 | x2 ⇒ e02 | x3 ⇒ e03 | x4 ⇒ e04 | x5 ⇒ e05 | x6 ⇒ e06 | x7 ⇒ e07 + | x8 ⇒ e08 | x9 ⇒ e09 | xA ⇒ e10 | xB ⇒ e11 | xC ⇒ e12 | xD ⇒ e13 | xE ⇒ e14 | xF ⇒ e15 + ]]. + +(* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) +(* posso definire un setter a matrice sull'array *) +definition setn_array16T ≝ +λn:exadecim.λT:Type.λp:Prod16T T.λv:T. + match p with + [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒ + match n with + [ x0 ⇒ array_16T T v e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x1 ⇒ array_16T T e00 v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x2 ⇒ array_16T T e00 e01 v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x3 ⇒ array_16T T e00 e01 e02 v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x4 ⇒ array_16T T e00 e01 e02 e03 v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x5 ⇒ array_16T T e00 e01 e02 e03 e04 v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x6 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x7 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v e08 e09 e10 e11 e12 e13 e14 e15 + | x8 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v e09 e10 e11 e12 e13 e14 e15 + | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v e10 e11 e12 e13 e14 e15 + | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v e11 e12 e13 e14 e15 + | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v e12 e13 e14 e15 + | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v e13 e14 e15 + | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v e14 e15 + | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v e15 + | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 v + ]]. + +(* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) +(* posso definire un setter multiplo [m,n] a matrice sull'array *) +definition setmn_array16T ≝ +λm,n:exadecim.λT:Type.λp:Prod16T T.λv:T. + match p with + [ array_16T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 ⇒ + match m with + [ x0 ⇒ match n with + [ x0 ⇒ array_16T T v e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x1 ⇒ array_16T T v v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x2 ⇒ array_16T T v v v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x3 ⇒ array_16T T v v v v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x4 ⇒ array_16T T v v v v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x5 ⇒ array_16T T v v v v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x6 ⇒ array_16T T v v v v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x7 ⇒ array_16T T v v v v v v v v e08 e09 e10 e11 e12 e13 e14 e15 + | x8 ⇒ array_16T T v v v v v v v v v e09 e10 e11 e12 e13 e14 e15 + | x9 ⇒ array_16T T v v v v v v v v v v e10 e11 e12 e13 e14 e15 + | xA ⇒ array_16T T v v v v v v v v v v v e11 e12 e13 e14 e15 + | xB ⇒ array_16T T v v v v v v v v v v v v e12 e13 e14 e15 + | xC ⇒ array_16T T v v v v v v v v v v v v v e13 e14 e15 + | xD ⇒ array_16T T v v v v v v v v v v v v v v e14 e15 + | xE ⇒ array_16T T v v v v v v v v v v v v v v v e15 + | xF ⇒ array_16T T v v v v v v v v v v v v v v v v ] + | x1 ⇒ match n with + [ x0 ⇒ p + | x1 ⇒ array_16T T e00 v e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x2 ⇒ array_16T T e00 v v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x3 ⇒ array_16T T e00 v v v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x4 ⇒ array_16T T e00 v v v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x5 ⇒ array_16T T e00 v v v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x6 ⇒ array_16T T e00 v v v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x7 ⇒ array_16T T e00 v v v v v v v e08 e09 e10 e11 e12 e13 e14 e15 + | x8 ⇒ array_16T T e00 v v v v v v v v e09 e10 e11 e12 e13 e14 e15 + | x9 ⇒ array_16T T e00 v v v v v v v v v e10 e11 e12 e13 e14 e15 + | xA ⇒ array_16T T e00 v v v v v v v v v v e11 e12 e13 e14 e15 + | xB ⇒ array_16T T e00 v v v v v v v v v v v e12 e13 e14 e15 + | xC ⇒ array_16T T e00 v v v v v v v v v v v v e13 e14 e15 + | xD ⇒ array_16T T e00 v v v v v v v v v v v v v e14 e15 + | xE ⇒ array_16T T e00 v v v v v v v v v v v v v v e15 + | xF ⇒ array_16T T e00 v v v v v v v v v v v v v v v ] + | x2 ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p + | x2 ⇒ array_16T T e00 e01 v e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x3 ⇒ array_16T T e00 e01 v v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x4 ⇒ array_16T T e00 e01 v v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x5 ⇒ array_16T T e00 e01 v v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x6 ⇒ array_16T T e00 e01 v v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x7 ⇒ array_16T T e00 e01 v v v v v v e08 e09 e10 e11 e12 e13 e14 e15 + | x8 ⇒ array_16T T e00 e01 v v v v v v v e09 e10 e11 e12 e13 e14 e15 + | x9 ⇒ array_16T T e00 e01 v v v v v v v v e10 e11 e12 e13 e14 e15 + | xA ⇒ array_16T T e00 e01 v v v v v v v v v e11 e12 e13 e14 e15 + | xB ⇒ array_16T T e00 e01 v v v v v v v v v v e12 e13 e14 e15 + | xC ⇒ array_16T T e00 e01 v v v v v v v v v v v e13 e14 e15 + | xD ⇒ array_16T T e00 e01 v v v v v v v v v v v v e14 e15 + | xE ⇒ array_16T T e00 e01 v v v v v v v v v v v v v e15 + | xF ⇒ array_16T T e00 e01 v v v v v v v v v v v v v v ] + | x3 ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p + | x3 ⇒ array_16T T e00 e01 e02 v e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x4 ⇒ array_16T T e00 e01 e02 v v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x5 ⇒ array_16T T e00 e01 e02 v v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x6 ⇒ array_16T T e00 e01 e02 v v v v e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x7 ⇒ array_16T T e00 e01 e02 v v v v v e08 e09 e10 e11 e12 e13 e14 e15 + | x8 ⇒ array_16T T e00 e01 e02 v v v v v v e09 e10 e11 e12 e13 e14 e15 + | x9 ⇒ array_16T T e00 e01 e02 v v v v v v v e10 e11 e12 e13 e14 e15 + | xA ⇒ array_16T T e00 e01 e02 v v v v v v v v e11 e12 e13 e14 e15 + | xB ⇒ array_16T T e00 e01 e02 v v v v v v v v v e12 e13 e14 e15 + | xC ⇒ array_16T T e00 e01 e02 v v v v v v v v v v e13 e14 e15 + | xD ⇒ array_16T T e00 e01 e02 v v v v v v v v v v v e14 e15 + | xE ⇒ array_16T T e00 e01 e02 v v v v v v v v v v v v e15 + | xF ⇒ array_16T T e00 e01 e02 v v v v v v v v v v v v v ] + | x4 ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p + | x4 ⇒ array_16T T e00 e01 e02 e03 v e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x5 ⇒ array_16T T e00 e01 e02 e03 v v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x6 ⇒ array_16T T e00 e01 e02 e03 v v v e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x7 ⇒ array_16T T e00 e01 e02 e03 v v v v e08 e09 e10 e11 e12 e13 e14 e15 + | x8 ⇒ array_16T T e00 e01 e02 e03 v v v v v e09 e10 e11 e12 e13 e14 e15 + | x9 ⇒ array_16T T e00 e01 e02 e03 v v v v v v e10 e11 e12 e13 e14 e15 + | xA ⇒ array_16T T e00 e01 e02 e03 v v v v v v v e11 e12 e13 e14 e15 + | xB ⇒ array_16T T e00 e01 e02 e03 v v v v v v v v e12 e13 e14 e15 + | xC ⇒ array_16T T e00 e01 e02 e03 v v v v v v v v v e13 e14 e15 + | xD ⇒ array_16T T e00 e01 e02 e03 v v v v v v v v v v e14 e15 + | xE ⇒ array_16T T e00 e01 e02 e03 v v v v v v v v v v v e15 + | xF ⇒ array_16T T e00 e01 e02 e03 v v v v v v v v v v v v ] + | x5 ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p + | x5 ⇒ array_16T T e00 e01 e02 e03 e04 v e06 e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x6 ⇒ array_16T T e00 e01 e02 e03 e04 v v e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x7 ⇒ array_16T T e00 e01 e02 e03 e04 v v v e08 e09 e10 e11 e12 e13 e14 e15 + | x8 ⇒ array_16T T e00 e01 e02 e03 e04 v v v v e09 e10 e11 e12 e13 e14 e15 + | x9 ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v e10 e11 e12 e13 e14 e15 + | xA ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v e11 e12 e13 e14 e15 + | xB ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v v e12 e13 e14 e15 + | xC ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v v v e13 e14 e15 + | xD ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v v v v e14 e15 + | xE ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v v v v v e15 + | xF ⇒ array_16T T e00 e01 e02 e03 e04 v v v v v v v v v v v ] + | x6 ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p + | x6 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v e07 e08 e09 e10 e11 e12 e13 e14 e15 + | x7 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v e08 e09 e10 e11 e12 e13 e14 e15 + | x8 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v e09 e10 e11 e12 e13 e14 e15 + | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v e10 e11 e12 e13 e14 e15 + | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v e11 e12 e13 e14 e15 + | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v v e12 e13 e14 e15 + | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v v v e13 e14 e15 + | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v v v v e14 e15 + | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v v v v v e15 + | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 v v v v v v v v v v ] + | x7 ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p + | x7 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v e08 e09 e10 e11 e12 e13 e14 e15 + | x8 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v e09 e10 e11 e12 e13 e14 e15 + | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v e10 e11 e12 e13 e14 e15 + | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v e11 e12 e13 e14 e15 + | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v v e12 e13 e14 e15 + | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v e13 e14 e15 + | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v v e14 e15 + | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v v v e15 + | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 v v v v v v v v v ] + | x8 ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p + | x8 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v e09 e10 e11 e12 e13 e14 e15 + | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v e10 e11 e12 e13 e14 e15 + | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v e11 e12 e13 e14 e15 + | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v e12 e13 e14 e15 + | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v e13 e14 e15 + | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v v e14 e15 + | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v v v e15 + | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 v v v v v v v v ] + | x9 ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p + | x8 ⇒ p + | x9 ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v e10 e11 e12 e13 e14 e15 + | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v e11 e12 e13 e14 e15 + | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v e12 e13 e14 e15 + | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v e13 e14 e15 + | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v v e14 e15 + | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v v v e15 + | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 v v v v v v v ] + | xA ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p + | x8 ⇒ p | x9 ⇒ p + | xA ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v e11 e12 e13 e14 e15 + | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v e12 e13 e14 e15 + | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v e13 e14 e15 + | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v v e14 e15 + | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v v v e15 + | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 v v v v v v ] + | xB ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p + | x8 ⇒ p | x9 ⇒ p | xA ⇒ p + | xB ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v e12 e13 e14 e15 + | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v e13 e14 e15 + | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v v e14 e15 + | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v v v e15 + | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 v v v v v ] + | xC ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p + | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p + | xC ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v e13 e14 e15 + | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v e14 e15 + | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v v e15 + | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 v v v v ] + | xD ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p + | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p + | xD ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v e14 e15 + | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v v e15 + | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 v v v ] + | xE ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p + | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p | xD ⇒ p + | xE ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v e15 + | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 v v ] + | xF ⇒ match n with + [ x0 ⇒ p | x1 ⇒ p | x2 ⇒ p | x3 ⇒ p | x4 ⇒ p | x5 ⇒ p | x6 ⇒ p | x7 ⇒ p + | x8 ⇒ p | x9 ⇒ p | xA ⇒ p | xB ⇒ p | xC ⇒ p | xD ⇒ p | xE ⇒ p + | xF ⇒ array_16T T e00 e01 e02 e03 e04 e05 e06 e07 e08 e09 e10 e11 e12 e13 e14 v ] + ]]. + +(* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) +(* posso definire un setter composto [m+1,n-1] a matrice sull'array *) +(* NB: obbiettivo evitare l'overflow *) +definition setmn_array16T_succ_pred ≝ +λm,n:exadecim.λT:Type.λp:Prod16T T.λv:T. + match lt_ex m xF with + [ true ⇒ match gt_ex n x0 with + [ true ⇒ setmn_array16T (succ_ex m) (pred_ex n) T p v + | false ⇒ p + ] + | false ⇒ p + ]. + +(* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) +(* posso definire un setter composto [m+1,F] a matrice sull'array *) +(* NB: obbiettivo evitare l'overflow *) +definition setmn_array16T_succ ≝ +λm:exadecim.λT:Type.λp:Prod16T T.λv:T. + match lt_ex m xF with + [ true ⇒ setmn_array16T (succ_ex m) xF T p v + | false ⇒ p + ]. + +(* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) +(* posso definire un setter composto [0,n-1] a matrice sull'array *) +(* NB: obbiettivo evitare l'overflow *) +definition setmn_array16T_pred ≝ +λn:exadecim.λT:Type.λp:Prod16T T.λv:T. + match gt_ex n x0 with + [ true ⇒ setmn_array16T x0 (pred_ex n) T p v + | false ⇒ p + ]. + +(* ************************** *) +(* TIPO BYTE COME INSIEME BIT *) +(* ************************** *) + +(* definizione di un byte come 8 bit *) +inductive Prod8T (T:Type) : Type ≝ +array_8T : T → T → T → T → T → T → T → T → + Prod8T T. + +(* abbiamo gia' gli ottali come tipo induttivo quindi: *) +(* posso definire un getter a matrice sull'array *) +definition getn_array8T ≝ +λn:oct.λT:Type.λp:Prod8T T. + match p with + [ array_8T e07 e06 e05 e04 e03 e02 e01 e00 ⇒ + match n with + [ o0 ⇒ e00 | o1 ⇒ e01 | o2 ⇒ e02 | o3 ⇒ e03 | o4 ⇒ e04 | o5 ⇒ e05 | o6 ⇒ e06 | o7 ⇒ e07 ]]. + +(* abbiamo gia' gli ottali come tipo induttivo quindi: *) +(* posso definire un setter a matrice sull'array *) +definition setn_array8T ≝ +λn:oct.λT:Type.λp:Prod8T T.λv:T. + match p with + [ array_8T e07 e06 e05 e04 e03 e02 e01 e00 ⇒ + match n with + [ o0 ⇒ array_8T T e07 e06 e05 e04 e03 e02 e01 v + | o1 ⇒ array_8T T e07 e06 e05 e04 e03 e02 v e00 + | o2 ⇒ array_8T T e07 e06 e05 e04 e03 v e01 e00 + | o3 ⇒ array_8T T e07 e06 e05 e04 v e02 e01 e00 + | o4 ⇒ array_8T T e07 e06 e05 v e03 e02 e01 e00 + | o5 ⇒ array_8T T e07 e06 v e04 e03 e02 e01 e00 + | o6 ⇒ array_8T T e07 v e05 e04 e03 e02 e01 e00 + | o7 ⇒ array_8T T v e06 e05 e04 e03 e02 e01 e00 + ]]. + +(* lettura byte *) +definition byte8_of_bits ≝ +λp:Prod8T bool. + match p with + [ array_8T e07 e06 e05 e04 e03 e02 e01 e00 ⇒ + mk_byte8 + (or_ex (match e07 with [ true ⇒ x8 | false ⇒ x0 ]) + (or_ex (match e06 with [ true ⇒ x4 | false ⇒ x0 ]) + (or_ex (match e05 with [ true ⇒ x2 | false ⇒ x0 ]) + (match e04 with [ true ⇒ x1 | false ⇒ x0 ])))) + (or_ex (match e03 with [ true ⇒ x8 | false ⇒ x0 ]) + (or_ex (match e02 with [ true ⇒ x4 | false ⇒ x0 ]) + (or_ex (match e01 with [ true ⇒ x2 | false ⇒ x0 ]) + (match e00 with [ true ⇒ x1 | false ⇒ x0 ])))) ]. + +(* scrittura byte *) +definition bits_of_byte8 ≝ +λp:byte8. + match b8h p with + [ x0 ⇒ match b8l p with + [ x0 ⇒ array_8T bool false false false false false false false false + | x1 ⇒ array_8T bool false false false false false false false true + | x2 ⇒ array_8T bool false false false false false false true false + | x3 ⇒ array_8T bool false false false false false false true true + | x4 ⇒ array_8T bool false false false false false true false false + | x5 ⇒ array_8T bool false false false false false true false true + | x6 ⇒ array_8T bool false false false false false true true false + | x7 ⇒ array_8T bool false false false false false true true true + | x8 ⇒ array_8T bool false false false false true false false false + | x9 ⇒ array_8T bool false false false false true false false true + | xA ⇒ array_8T bool false false false false true false true false + | xB ⇒ array_8T bool false false false false true false true true + | xC ⇒ array_8T bool false false false false true true false false + | xD ⇒ array_8T bool false false false false true true false true + | xE ⇒ array_8T bool false false false false true true true false + | xF ⇒ array_8T bool false false false false true true true true ] + | x1 ⇒ match b8l p with + [ x0 ⇒ array_8T bool false false false true false false false false + | x1 ⇒ array_8T bool false false false true false false false true + | x2 ⇒ array_8T bool false false false true false false true false + | x3 ⇒ array_8T bool false false false true false false true true + | x4 ⇒ array_8T bool false false false true false true false false + | x5 ⇒ array_8T bool false false false true false true false true + | x6 ⇒ array_8T bool false false false true false true true false + | x7 ⇒ array_8T bool false false false true false true true true + | x8 ⇒ array_8T bool false false false true true false false false + | x9 ⇒ array_8T bool false false false true true false false true + | xA ⇒ array_8T bool false false false true true false true false + | xB ⇒ array_8T bool false false false true true false true true + | xC ⇒ array_8T bool false false false true true true false false + | xD ⇒ array_8T bool false false false true true true false true + | xE ⇒ array_8T bool false false false true true true true false + | xF ⇒ array_8T bool false false false true true true true true ] + | x2 ⇒ match b8l p with + [ x0 ⇒ array_8T bool false false true false false false false false + | x1 ⇒ array_8T bool false false true false false false false true + | x2 ⇒ array_8T bool false false true false false false true false + | x3 ⇒ array_8T bool false false true false false false true true + | x4 ⇒ array_8T bool false false true false false true false false + | x5 ⇒ array_8T bool false false true false false true false true + | x6 ⇒ array_8T bool false false true false false true true false + | x7 ⇒ array_8T bool false false true false false true true true + | x8 ⇒ array_8T bool false false true false true false false false + | x9 ⇒ array_8T bool false false true false true false false true + | xA ⇒ array_8T bool false false true false true false true false + | xB ⇒ array_8T bool false false true false true false true true + | xC ⇒ array_8T bool false false true false true true false false + | xD ⇒ array_8T bool false false true false true true false true + | xE ⇒ array_8T bool false false true false true true true false + | xF ⇒ array_8T bool false false true false true true true true ] + | x3 ⇒ match b8l p with + [ x0 ⇒ array_8T bool false false true true false false false false + | x1 ⇒ array_8T bool false false true true false false false true + | x2 ⇒ array_8T bool false false true true false false true false + | x3 ⇒ array_8T bool false false true true false false true true + | x4 ⇒ array_8T bool false false true true false true false false + | x5 ⇒ array_8T bool false false true true false true false true + | x6 ⇒ array_8T bool false false true true false true true false + | x7 ⇒ array_8T bool false false true true false true true true + | x8 ⇒ array_8T bool false false true true true false false false + | x9 ⇒ array_8T bool false false true true true false false true + | xA ⇒ array_8T bool false false true true true false true false + | xB ⇒ array_8T bool false false true true true false true true + | xC ⇒ array_8T bool false false true true true true false false + | xD ⇒ array_8T bool false false true true true true false true + | xE ⇒ array_8T bool false false true true true true true false + | xF ⇒ array_8T bool false false true true true true true true ] + | x4 ⇒ match b8l p with + [ x0 ⇒ array_8T bool false true false false false false false false + | x1 ⇒ array_8T bool false true false false false false false true + | x2 ⇒ array_8T bool false true false false false false true false + | x3 ⇒ array_8T bool false true false false false false true true + | x4 ⇒ array_8T bool false true false false false true false false + | x5 ⇒ array_8T bool false true false false false true false true + | x6 ⇒ array_8T bool false true false false false true true false + | x7 ⇒ array_8T bool false true false false false true true true + | x8 ⇒ array_8T bool false true false false true false false false + | x9 ⇒ array_8T bool false true false false true false false true + | xA ⇒ array_8T bool false true false false true false true false + | xB ⇒ array_8T bool false true false false true false true true + | xC ⇒ array_8T bool false true false false true true false false + | xD ⇒ array_8T bool false true false false true true false true + | xE ⇒ array_8T bool false true false false true true true false + | xF ⇒ array_8T bool false true false false true true true true ] + | x5 ⇒ match b8l p with + [ x0 ⇒ array_8T bool false true false true false false false false + | x1 ⇒ array_8T bool false true false true false false false true + | x2 ⇒ array_8T bool false true false true false false true false + | x3 ⇒ array_8T bool false true false true false false true true + | x4 ⇒ array_8T bool false true false true false true false false + | x5 ⇒ array_8T bool false true false true false true false true + | x6 ⇒ array_8T bool false true false true false true true false + | x7 ⇒ array_8T bool false true false true false true true true + | x8 ⇒ array_8T bool false true false true true false false false + | x9 ⇒ array_8T bool false true false true true false false true + | xA ⇒ array_8T bool false true false true true false true false + | xB ⇒ array_8T bool false true false true true false true true + | xC ⇒ array_8T bool false true false true true true false false + | xD ⇒ array_8T bool false true false true true true false true + | xE ⇒ array_8T bool false true false true true true true false + | xF ⇒ array_8T bool false true false true true true true true ] + | x6 ⇒ match b8l p with + [ x0 ⇒ array_8T bool false true true false false false false false + | x1 ⇒ array_8T bool false true true false false false false true + | x2 ⇒ array_8T bool false true true false false false true false + | x3 ⇒ array_8T bool false true true false false false true true + | x4 ⇒ array_8T bool false true true false false true false false + | x5 ⇒ array_8T bool false true true false false true false true + | x6 ⇒ array_8T bool false true true false false true true false + | x7 ⇒ array_8T bool false true true false false true true true + | x8 ⇒ array_8T bool false true true false true false false false + | x9 ⇒ array_8T bool false true true false true false false true + | xA ⇒ array_8T bool false true true false true false true false + | xB ⇒ array_8T bool false true true false true false true true + | xC ⇒ array_8T bool false true true false true true false false + | xD ⇒ array_8T bool false true true false true true false true + | xE ⇒ array_8T bool false true true false true true true false + | xF ⇒ array_8T bool false true true false true true true true ] + | x7 ⇒ match b8l p with + [ x0 ⇒ array_8T bool false true true true false false false false + | x1 ⇒ array_8T bool false true true true false false false true + | x2 ⇒ array_8T bool false true true true false false true false + | x3 ⇒ array_8T bool false true true true false false true true + | x4 ⇒ array_8T bool false true true true false true false false + | x5 ⇒ array_8T bool false true true true false true false true + | x6 ⇒ array_8T bool false true true true false true true false + | x7 ⇒ array_8T bool false true true true false true true true + | x8 ⇒ array_8T bool false true true true true false false false + | x9 ⇒ array_8T bool false true true true true false false true + | xA ⇒ array_8T bool false true true true true false true false + | xB ⇒ array_8T bool false true true true true false true true + | xC ⇒ array_8T bool false true true true true true false false + | xD ⇒ array_8T bool false true true true true true false true + | xE ⇒ array_8T bool false true true true true true true false + | xF ⇒ array_8T bool false true true true true true true true ] + | x8 ⇒ match b8l p with + [ x0 ⇒ array_8T bool true false false false false false false false + | x1 ⇒ array_8T bool true false false false false false false true + | x2 ⇒ array_8T bool true false false false false false true false + | x3 ⇒ array_8T bool true false false false false false true true + | x4 ⇒ array_8T bool true false false false false true false false + | x5 ⇒ array_8T bool true false false false false true false true + | x6 ⇒ array_8T bool true false false false false true true false + | x7 ⇒ array_8T bool true false false false false true true true + | x8 ⇒ array_8T bool true false false false true false false false + | x9 ⇒ array_8T bool true false false false true false false true + | xA ⇒ array_8T bool true false false false true false true false + | xB ⇒ array_8T bool true false false false true false true true + | xC ⇒ array_8T bool true false false false true true false false + | xD ⇒ array_8T bool true false false false true true false true + | xE ⇒ array_8T bool true false false false true true true false + | xF ⇒ array_8T bool true false false false true true true true ] + | x9 ⇒ match b8l p with + [ x0 ⇒ array_8T bool true false false true false false false false + | x1 ⇒ array_8T bool true false false true false false false true + | x2 ⇒ array_8T bool true false false true false false true false + | x3 ⇒ array_8T bool true false false true false false true true + | x4 ⇒ array_8T bool true false false true false true false false + | x5 ⇒ array_8T bool true false false true false true false true + | x6 ⇒ array_8T bool true false false true false true true false + | x7 ⇒ array_8T bool true false false true false true true true + | x8 ⇒ array_8T bool true false false true true false false false + | x9 ⇒ array_8T bool true false false true true false false true + | xA ⇒ array_8T bool true false false true true false true false + | xB ⇒ array_8T bool true false false true true false true true + | xC ⇒ array_8T bool true false false true true true false false + | xD ⇒ array_8T bool true false false true true true false true + | xE ⇒ array_8T bool true false false true true true true false + | xF ⇒ array_8T bool true false false true true true true true ] + | xA ⇒ match b8l p with + [ x0 ⇒ array_8T bool true false true false false false false false + | x1 ⇒ array_8T bool true false true false false false false true + | x2 ⇒ array_8T bool true false true false false false true false + | x3 ⇒ array_8T bool true false true false false false true true + | x4 ⇒ array_8T bool true false true false false true false false + | x5 ⇒ array_8T bool true false true false false true false true + | x6 ⇒ array_8T bool true false true false false true true false + | x7 ⇒ array_8T bool true false true false false true true true + | x8 ⇒ array_8T bool true false true false true false false false + | x9 ⇒ array_8T bool true false true false true false false true + | xA ⇒ array_8T bool true false true false true false true false + | xB ⇒ array_8T bool true false true false true false true true + | xC ⇒ array_8T bool true false true false true true false false + | xD ⇒ array_8T bool true false true false true true false true + | xE ⇒ array_8T bool true false true false true true true false + | xF ⇒ array_8T bool true false true false true true true true ] + | xB ⇒ match b8l p with + [ x0 ⇒ array_8T bool true false true true false false false false + | x1 ⇒ array_8T bool true false true true false false false true + | x2 ⇒ array_8T bool true false true true false false true false + | x3 ⇒ array_8T bool true false true true false false true true + | x4 ⇒ array_8T bool true false true true false true false false + | x5 ⇒ array_8T bool true false true true false true false true + | x6 ⇒ array_8T bool true false true true false true true false + | x7 ⇒ array_8T bool true false true true false true true true + | x8 ⇒ array_8T bool true false true true true false false false + | x9 ⇒ array_8T bool true false true true true false false true + | xA ⇒ array_8T bool true false true true true false true false + | xB ⇒ array_8T bool true false true true true false true true + | xC ⇒ array_8T bool true false true true true true false false + | xD ⇒ array_8T bool true false true true true true false true + | xE ⇒ array_8T bool true false true true true true true false + | xF ⇒ array_8T bool true false true true true true true true ] + | xC ⇒ match b8l p with + [ x0 ⇒ array_8T bool true true false false false false false false + | x1 ⇒ array_8T bool true true false false false false false true + | x2 ⇒ array_8T bool true true false false false false true false + | x3 ⇒ array_8T bool true true false false false false true true + | x4 ⇒ array_8T bool true true false false false true false false + | x5 ⇒ array_8T bool true true false false false true false true + | x6 ⇒ array_8T bool true true false false false true true false + | x7 ⇒ array_8T bool true true false false false true true true + | x8 ⇒ array_8T bool true true false false true false false false + | x9 ⇒ array_8T bool true true false false true false false true + | xA ⇒ array_8T bool true true false false true false true false + | xB ⇒ array_8T bool true true false false true false true true + | xC ⇒ array_8T bool true true false false true true false false + | xD ⇒ array_8T bool true true false false true true false true + | xE ⇒ array_8T bool true true false false true true true false + | xF ⇒ array_8T bool true true false false true true true true ] + | xD ⇒ match b8l p with + [ x0 ⇒ array_8T bool true true false true false false false false + | x1 ⇒ array_8T bool true true false true false false false true + | x2 ⇒ array_8T bool true true false true false false true false + | x3 ⇒ array_8T bool true true false true false false true true + | x4 ⇒ array_8T bool true true false true false true false false + | x5 ⇒ array_8T bool true true false true false true false true + | x6 ⇒ array_8T bool true true false true false true true false + | x7 ⇒ array_8T bool true true false true false true true true + | x8 ⇒ array_8T bool true true false true true false false false + | x9 ⇒ array_8T bool true true false true true false false true + | xA ⇒ array_8T bool true true false true true false true false + | xB ⇒ array_8T bool true true false true true false true true + | xC ⇒ array_8T bool true true false true true true false false + | xD ⇒ array_8T bool true true false true true true false true + | xE ⇒ array_8T bool true true false true true true true false + | xF ⇒ array_8T bool true true false true true true true true ] + | xE ⇒ match b8l p with + [ x0 ⇒ array_8T bool true true true false false false false false + | x1 ⇒ array_8T bool true true true false false false false true + | x2 ⇒ array_8T bool true true true false false false true false + | x3 ⇒ array_8T bool true true true false false false true true + | x4 ⇒ array_8T bool true true true false false true false false + | x5 ⇒ array_8T bool true true true false false true false true + | x6 ⇒ array_8T bool true true true false false true true false + | x7 ⇒ array_8T bool true true true false false true true true + | x8 ⇒ array_8T bool true true true false true false false false + | x9 ⇒ array_8T bool true true true false true false false true + | xA ⇒ array_8T bool true true true false true false true false + | xB ⇒ array_8T bool true true true false true false true true + | xC ⇒ array_8T bool true true true false true true false false + | xD ⇒ array_8T bool true true true false true true false true + | xE ⇒ array_8T bool true true true false true true true false + | xF ⇒ array_8T bool true true true false true true true true ] + | xF ⇒ match b8l p with + [ x0 ⇒ array_8T bool true true true true false false false false + | x1 ⇒ array_8T bool true true true true false false false true + | x2 ⇒ array_8T bool true true true true false false true false + | x3 ⇒ array_8T bool true true true true false false true true + | x4 ⇒ array_8T bool true true true true false true false false + | x5 ⇒ array_8T bool true true true true false true false true + | x6 ⇒ array_8T bool true true true true false true true false + | x7 ⇒ array_8T bool true true true true false true true true + | x8 ⇒ array_8T bool true true true true true false false false + | x9 ⇒ array_8T bool true true true true true false false true + | xA ⇒ array_8T bool true true true true true false true false + | xB ⇒ array_8T bool true true true true true false true true + | xC ⇒ array_8T bool true true true true true true false false + | xD ⇒ array_8T bool true true true true true true false true + | xE ⇒ array_8T bool true true true true true true true false + | xF ⇒ array_8T bool true true true true true true true true ] + ]. + +(* ********************** *) +(* TEOREMI/LEMMMI/ASSIOMI *) +(* ********************** *) + +(* check *) +lemma ok_byte8_of_bits_bits_of_byte8 : + ∀b. + byte8_of_bits (bits_of_byte8 b) = b. + intros; + elim b; elim e; elim e1; + reflexivity. +qed. + +(* check *) +lemma ok_bits_of_byte8_byte8_of_bits : + ∀b7,b6,b5,b4,b3,b2,b1,b0. + bits_of_byte8 (byte8_of_bits (array_8T bool b7 b6 b5 b4 b3 b2 b1 b0)) + = array_8T bool b7 b6 b5 b4 b3 b2 b1 b0. + intros; + elim b0; elim b1; elim b2; elim b3; elim b4; elim b5; elim b6; elim b7; + reflexivity. +qed.