X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Fmemory_struct.ma;h=9d6da1a7fbdbb0c26763db31be047888b1537833;hb=17c6ac2888a1f30aee059f5cf6b8872bb4f3ab61;hp=6bfec7846e937910f3c0294bbf9d652f1c456565;hpb=9f580d9bf8f6ba6950b252f587166e95bc8fb1a8;p=helm.git diff --git a/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma b/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma index 6bfec7846..9d6da1a7f 100755 --- a/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma +++ b/helm/software/matita/contribs/ng_assembly/freescale/memory_struct.ma @@ -13,18 +13,14 @@ (**************************************************************************) (* ********************************************************************** *) -(* Progetto FreeScale *) +(* Progetto FreeScale *) (* *) -(* Sviluppato da: *) -(* Cosimo Oliboni, oliboni@cs.unibo.it *) +(* Sviluppato da: Cosimo Oliboni, oliboni@cs.unibo.it *) +(* 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/aux_bases.ma". +include "freescale/oct.ma". include "freescale/byte8.ma". (* **************************** *) @@ -37,18 +33,6 @@ ninductive memory_type : Type ≝ | MEM_READ_WRITE: memory_type | MEM_OUT_OF_BOUND: memory_type. -ndefinition memory_type_ind : ΠP:memory_type → Prop.P MEM_READ_ONLY → P MEM_READ_WRITE → P MEM_OUT_OF_BOUND → Πm:memory_type.P m ≝ -λP:memory_type → Prop.λp:P MEM_READ_ONLY.λp1:P MEM_READ_WRITE.λp2:P MEM_OUT_OF_BOUND.λm:memory_type. - match m with [ MEM_READ_ONLY ⇒ p | MEM_READ_WRITE ⇒ p1 | MEM_OUT_OF_BOUND ⇒ p2 ]. - -ndefinition memory_type_rec : ΠP:memory_type → Set.P MEM_READ_ONLY → P MEM_READ_WRITE → P MEM_OUT_OF_BOUND → Πm:memory_type.P m ≝ -λP:memory_type → Set.λp:P MEM_READ_ONLY.λp1:P MEM_READ_WRITE.λp2:P MEM_OUT_OF_BOUND.λm:memory_type. - match m with [ MEM_READ_ONLY ⇒ p | MEM_READ_WRITE ⇒ p1 | MEM_OUT_OF_BOUND ⇒ p2 ]. - -ndefinition memory_type_rect : ΠP:memory_type → Type.P MEM_READ_ONLY → P MEM_READ_WRITE → P MEM_OUT_OF_BOUND → Πm:memory_type.P m ≝ -λP:memory_type → Type.λp:P MEM_READ_ONLY.λp1:P MEM_READ_WRITE.λp2:P MEM_OUT_OF_BOUND.λm:memory_type. - match m with [ MEM_READ_ONLY ⇒ p | MEM_READ_WRITE ⇒ p1 | MEM_OUT_OF_BOUND ⇒ p2 ]. - (* **************** *) (* TIPO ARRAY DA 16 *) (* **************** *) @@ -59,27 +43,6 @@ array_16T : T → T → T → T → T → T → T → T → T → T → T → T → T → T → T → T → Array16T T. -ndefinition Array16T_ind - : ΠT:Type.ΠP:Array16T T → Prop. - (Πt,t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15.P (array_16T T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15)) → Πa:Array16T T.P a ≝ -λT:Type.λP:Array16T T → Prop. -λf:Πt,t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15.P (array_16T T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15).λa:Array16T T. - match a with [ array_16T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 ⇒ f t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 ]. - -ndefinition Array16T_rec - : ΠT:Type.ΠP:Array16T T → Set. - (Πt,t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15.P (array_16T T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15)) → Πa:Array16T T.P a ≝ -λT:Type.λP:Array16T T → Set. -λf:Πt,t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15.P (array_16T T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15).λa:Array16T T. - match a with [ array_16T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 ⇒ f t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 ]. - -ndefinition Array16T_rect - : ΠT:Type.ΠP:Array16T T → Type. - (Πt,t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15.P (array_16T T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15)) → Πa:Array16T T.P a ≝ -λT:Type.λP:Array16T T → Type. -λf:Πt,t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15.P (array_16T T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15).λa:Array16T T. - match a with [ array_16T t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 ⇒ f t t1 t2 t3 t4 t5 t6 t7 t8 t9 t10 t11 t12 t13 t14 t15 ]. - (* abbiamo gia' gli esadecimali come tipo induttivo quindi: *) (* posso definire un getter a matrice sull'array *) ndefinition getn_array16T ≝ @@ -341,27 +304,6 @@ ninductive Array8T (T:Type) : Type ≝ array_8T : T → T → T → T → T → T → T → T → Array8T T. -ndefinition Array8T_ind - : ΠT:Type.ΠP:Array8T T → Prop. - (Πt,t1,t2,t3,t4,t5,t6,t7.P (array_8T T t t1 t2 t3 t4 t5 t6 t7)) → Πa:Array8T T.P a ≝ -λT:Type.λP:Array8T T → Prop. -λf:Πt,t1,t2,t3,t4,t5,t6,t7.P (array_8T T t t1 t2 t3 t4 t5 t6 t7).λa:Array8T T. - match a with [ array_8T t t1 t2 t3 t4 t5 t6 t7 ⇒ f t t1 t2 t3 t4 t5 t6 t7 ]. - -ndefinition Array8T_rec - : ΠT:Type.ΠP:Array8T T → Set. - (Πt,t1,t2,t3,t4,t5,t6,t7.P (array_8T T t t1 t2 t3 t4 t5 t6 t7)) → Πa:Array8T T.P a ≝ -λT:Type.λP:Array8T T → Set. -λf:Πt,t1,t2,t3,t4,t5,t6,t7.P (array_8T T t t1 t2 t3 t4 t5 t6 t7).λa:Array8T T. - match a with [ array_8T t t1 t2 t3 t4 t5 t6 t7 ⇒ f t t1 t2 t3 t4 t5 t6 t7 ]. - -ndefinition Array8T_rect - : ΠT:Type.ΠP:Array8T T → Type. - (Πt,t1,t2,t3,t4,t5,t6,t7.P (array_8T T t t1 t2 t3 t4 t5 t6 t7)) → Πa:Array8T T.P a ≝ -λT:Type.λP:Array8T T → Type. -λf:Πt,t1,t2,t3,t4,t5,t6,t7.P (array_8T T t t1 t2 t3 t4 t5 t6 t7).λa:Array8T T. - match a with [ array_8T t t1 t2 t3 t4 t5 t6 t7 ⇒ f t t1 t2 t3 t4 t5 t6 t7 ]. - (* abbiamo gia' gli ottali come tipo induttivo quindi: *) (* posso definire un getter a matrice sull'array *) ndefinition getn_array8T ≝