From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 24 Jul 2009 21:25:13 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3623
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0f99c7691f8a418003acea3f7856102c21dcab8d;p=helm.git

...
---

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma b/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma
index 83abb1816..5bfd406b5 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/load_write.ma
@@ -29,18 +29,6 @@ ninductive error_type : Type ≝
 | ILL_FETCH_AD: error_type
 | ILL_EX_AD: error_type.
 
-ndefinition error_type_ind : ΠP:error_type → Prop.P ILL_OP → P ILL_FETCH_AD → P ILL_EX_AD → Πe:error_type.P e ≝
-λP:error_type → Prop.λp:P ILL_OP.λp1:P ILL_FETCH_AD.λp2:P ILL_EX_AD.λe:error_type.
- match e with [ ILL_OP ⇒ p | ILL_FETCH_AD ⇒ p1 | ILL_EX_AD ⇒ p2 ].
-
-ndefinition error_type_rec : ΠP:error_type → Set.P ILL_OP → P ILL_FETCH_AD → P ILL_EX_AD → Πe:error_type.P e ≝
-λP:error_type → Set.λp:P ILL_OP.λp1:P ILL_FETCH_AD.λp2:P ILL_EX_AD.λe:error_type.
- match e with [ ILL_OP ⇒ p | ILL_FETCH_AD ⇒ p1 | ILL_EX_AD ⇒ p2 ].
-
-ndefinition error_type_rect : ΠP:error_type → Type.P ILL_OP → P ILL_FETCH_AD → P ILL_EX_AD → Πe:error_type.P e ≝
-λP:error_type → Type.λp:P ILL_OP.λp1:P ILL_FETCH_AD.λp2:P ILL_EX_AD.λe:error_type.
- match e with [ ILL_OP ⇒ p | ILL_FETCH_AD ⇒ p1 | ILL_EX_AD ⇒ p2 ].
-
 (* un tipo opzione ad hoc
    - errore: interessa solo l'errore
    - ok: interessa info e il nuovo pc
@@ -49,27 +37,6 @@ ninductive fetch_result (A:Type) : Type ≝
   FetchERR : error_type → fetch_result A
 | FetchOK  : A → word16 → fetch_result A.
 
-ndefinition fetch_result_ind
- : ΠA:Type.ΠP:fetch_result A → Prop.(Πn:error_type.P (FetchERR A n)) →
-   (Πa:A.Πn:word16.P (FetchOK A a n)) → Πf:fetch_result A.P f ≝
-λA:Type.λP:fetch_result A → Prop.λf:Πn:error_type.P (FetchERR A n).
-λf1:Πa:A.Πn:word16.P (FetchOK A a n).λf2:fetch_result A.
- match f2 with [ FetchERR n ⇒ f n | FetchOK a n ⇒ f1 a n ].
-
-ndefinition fetch_result_rec
- : ΠA:Type.ΠP:fetch_result A → Set.(Πn:error_type.P (FetchERR A n)) →
-   (Πa:A.Πn:word16.P (FetchOK A a n)) → Πf:fetch_result A.P f ≝
-λA:Type.λP:fetch_result A → Set.λf:Πn:error_type.P (FetchERR A n).
-λf1:Πa:A.Πn:word16.P (FetchOK A a n).λf2:fetch_result A.
- match f2 with [ FetchERR n ⇒ f n | FetchOK a n ⇒ f1 a n ].
-
-ndefinition fetch_result_rect
- : ΠA:Type.ΠP:fetch_result A → Type.(Πn:error_type.P (FetchERR A n)) →
-   (Πa:A.Πn:word16.P (FetchOK A a n)) → Πf:fetch_result A.P f ≝
-λA:Type.λP:fetch_result A → Type.λf:Πn:error_type.P (FetchERR A n).
-λf1:Πa:A.Πn:word16.P (FetchOK A a n).λf2:fetch_result A.
- match f2 with [ FetchERR n ⇒ f n | FetchOK a n ⇒ f1 a n ].
-
 (* **************************** *)
 (* FETCH E ACCESSO ALLA MEMORIA *)
 (* **************************** *)
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/model.ma b/helm/software/matita/contribs/ng_assembly/freescale/model.ma
index adafa40f3..e91ff5f65 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/model.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/model.ma
@@ -36,53 +36,17 @@ ninductive HC08_mcu_model : Type ≝
   MC68HC08AB16A: HC08_mcu_model
   (*..*). 
 
-ndefinition HC08_mcu_model_ind : ΠP:HC08_mcu_model → Prop.P MC68HC08AB16A → Πh:HC08_mcu_model.P h ≝
-λP:HC08_mcu_model → Prop.λp:P MC68HC08AB16A.λh:HC08_mcu_model.
- match h with [ MC68HC08AB16A ⇒ p ].
-
-ndefinition HC08_mcu_model_rec : ΠP:HC08_mcu_model → Set.P MC68HC08AB16A → Πh:HC08_mcu_model.P h ≝
-λP:HC08_mcu_model → Set.λp:P MC68HC08AB16A.λh:HC08_mcu_model.
- match h with [ MC68HC08AB16A ⇒ p ].
-
-ndefinition HC08_mcu_model_rect : ΠP:HC08_mcu_model → Type.P MC68HC08AB16A → Πh:HC08_mcu_model.P h ≝
-λP:HC08_mcu_model → Type.λp:P MC68HC08AB16A.λh:HC08_mcu_model.
- match h with [ MC68HC08AB16A ⇒ p ].
-
 (* modelli di HCS08 *)
 ninductive HCS08_mcu_model : Type ≝
   MC9S08AW60 : HCS08_mcu_model
 | MC9S08GB60 : HCS08_mcu_model
   (*..*).
 
-ndefinition HCS08_mcu_model_ind : ΠP:HCS08_mcu_model → Prop.P MC9S08GB60 → P MC9S08AW60 → Πh:HCS08_mcu_model.P h ≝
-λP:HCS08_mcu_model → Prop.λp:P MC9S08GB60.λp1:P MC9S08AW60.λh:HCS08_mcu_model.
- match h with [ MC9S08GB60 ⇒ p | MC9S08AW60 ⇒ p1 ].
-
-ndefinition HCS08_mcu_model_rec : ΠP:HCS08_mcu_model → Set.P MC9S08GB60 → P MC9S08AW60 → Πh:HCS08_mcu_model.P h ≝
-λP:HCS08_mcu_model → Set.λp:P MC9S08GB60.λp1:P MC9S08AW60.λh:HCS08_mcu_model.
- match h with [ MC9S08GB60 ⇒ p | MC9S08AW60 ⇒ p1 ].
-
-ndefinition HCS08_mcu_model_rect : ΠP:HCS08_mcu_model → Type.P MC9S08GB60 → P MC9S08AW60 → Πh:HCS08_mcu_model.P h ≝
-λP:HCS08_mcu_model → Type.λp:P MC9S08GB60.λp1:P MC9S08AW60.λh:HCS08_mcu_model.
- match h with [ MC9S08GB60 ⇒ p | MC9S08AW60 ⇒ p1 ].
-
 (* modelli di RS08 *)
 ninductive RS08_mcu_model : Type ≝
   MC9RS08KA1 : RS08_mcu_model
 | MC9RS08KA2 : RS08_mcu_model.
 
-ndefinition RS08_mcu_model_ind : ΠP:RS08_mcu_model → Prop.P MC9RS08KA1 → P MC9RS08KA2 → Πr:RS08_mcu_model.P r ≝
-λP:RS08_mcu_model → Prop.λp:P MC9RS08KA1.λp1:P MC9RS08KA2.λr:RS08_mcu_model.
-  match r with [ MC9RS08KA1 ⇒ p | MC9RS08KA2 ⇒ p1 ].
-
-ndefinition RS08_mcu_model_rec : ΠP:RS08_mcu_model → Set.P MC9RS08KA1 → P MC9RS08KA2 → Πr:RS08_mcu_model.P r ≝
-λP:RS08_mcu_model → Set.λp:P MC9RS08KA1.λp1:P MC9RS08KA2.λr:RS08_mcu_model.
-  match r with [ MC9RS08KA1 ⇒ p | MC9RS08KA2 ⇒ p1 ].
-
-ndefinition RS08_mcu_model_rect : ΠP:RS08_mcu_model → Type.P MC9RS08KA1 → P MC9RS08KA2 → Πr:RS08_mcu_model.P r ≝
-λP:RS08_mcu_model → Type.λp:P MC9RS08KA1.λp1:P MC9RS08KA2.λr:RS08_mcu_model.
-  match r with [ MC9RS08KA1 ⇒ p | MC9RS08KA2 ⇒ p1 ].
-
 (* raggruppamento dei modelli *)
 ninductive any_mcu_model : Type ≝
   FamilyHC05  : HC05_mcu_model → any_mcu_model
@@ -90,30 +54,6 @@ ninductive any_mcu_model : Type ≝
 | FamilyHCS08 : HCS08_mcu_model → any_mcu_model
 | FamilyRS08  : RS08_mcu_model → any_mcu_model.
 
-ndefinition any_mcu_model_ind
- : ΠP:any_mcu_model → Prop.(Πn:HC05_mcu_model.P (FamilyHC05 n)) → (Πn:HC08_mcu_model.P (FamilyHC08 n)) →
-   (Πn:HCS08_mcu_model.P (FamilyHCS08 n)) → (Πn:RS08_mcu_model.P (FamilyRS08 n))→Πa:any_mcu_model.P a ≝
-λP:any_mcu_model → Prop.λf:Πn:HC05_mcu_model.P (FamilyHC05 n).λf1:Πn:HC08_mcu_model.P (FamilyHC08 n).
-λf2:Πn:HCS08_mcu_model.P (FamilyHCS08 n).λf3:Πn:RS08_mcu_model.P (FamilyRS08 n).λa:any_mcu_model.
- match a with [ FamilyHC05 n ⇒ f n | FamilyHC08 n ⇒ f1 n
-              | FamilyHCS08 n ⇒ f2 n | FamilyRS08 n ⇒ f3 n ].
-
-ndefinition any_mcu_model_rec
- : ΠP:any_mcu_model → Set.(Πn:HC05_mcu_model.P (FamilyHC05 n)) → (Πn:HC08_mcu_model.P (FamilyHC08 n)) →
-   (Πn:HCS08_mcu_model.P (FamilyHCS08 n)) → (Πn:RS08_mcu_model.P (FamilyRS08 n))→Πa:any_mcu_model.P a ≝
-λP:any_mcu_model → Set.λf:Πn:HC05_mcu_model.P (FamilyHC05 n).λf1:Πn:HC08_mcu_model.P (FamilyHC08 n).
-λf2:Πn:HCS08_mcu_model.P (FamilyHCS08 n).λf3:Πn:RS08_mcu_model.P (FamilyRS08 n).λa:any_mcu_model.
- match a with [ FamilyHC05 n ⇒ f n | FamilyHC08 n ⇒ f1 n
-              | FamilyHCS08 n ⇒ f2 n | FamilyRS08 n ⇒ f3 n ].
-
-ndefinition any_mcu_model_rect
- : ΠP:any_mcu_model → Type.(Πn:HC05_mcu_model.P (FamilyHC05 n)) → (Πn:HC08_mcu_model.P (FamilyHC08 n)) →
-   (Πn:HCS08_mcu_model.P (FamilyHCS08 n)) → (Πn:RS08_mcu_model.P (FamilyRS08 n))→Πa:any_mcu_model.P a ≝
-λP:any_mcu_model → Type.λf:Πn:HC05_mcu_model.P (FamilyHC05 n).λf1:Πn:HC08_mcu_model.P (FamilyHC08 n).
-λf2:Πn:HCS08_mcu_model.P (FamilyHCS08 n).λf3:Πn:RS08_mcu_model.P (FamilyRS08 n).λa:any_mcu_model.
- match a with [ FamilyHC05 n ⇒ f n | FamilyHC08 n ⇒ f1 n
-              | FamilyHCS08 n ⇒ f2 n | FamilyRS08 n ⇒ f3 n ].
-
 (* 
 condizioni errore interne alla MCU
 (Il programma viene caricato dal produttore in ROM o impostato in EEPROM)
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma b/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma
index 4ae8093d1..fc374d9ab 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/multivm.ma
@@ -1131,18 +1131,6 @@ ninductive susp_type : Type ≝
 | STOP_MODE: susp_type
 | WAIT_MODE: susp_type.
 
-ndefinition susp_type_ind : ΠP:susp_type → Prop.P BGND_MODE → P STOP_MODE → P WAIT_MODE → Πs:susp_type.P s ≝
-λP:susp_type → Prop.λp:P BGND_MODE.λp1:P STOP_MODE.λp2:P WAIT_MODE.λs:susp_type.
- match s with [ BGND_MODE ⇒ p | STOP_MODE ⇒ p1 | WAIT_MODE ⇒ p2 ].
-
-ndefinition susp_type_rec : ΠP:susp_type → Set.P BGND_MODE → P STOP_MODE → P WAIT_MODE → Πs:susp_type.P s ≝
-λP:susp_type → Set.λp:P BGND_MODE.λp1:P STOP_MODE.λp2:P WAIT_MODE.λs:susp_type.
- match s with [ BGND_MODE ⇒ p | STOP_MODE ⇒ p1 | WAIT_MODE ⇒ p2 ].
-
-ndefinition susp_type_rect : ΠP:susp_type → Type.P BGND_MODE → P STOP_MODE → P WAIT_MODE → Πs:susp_type.P s ≝
-λP:susp_type → Type.λp:P BGND_MODE.λp1:P STOP_MODE.λp2:P WAIT_MODE.λs:susp_type.
- match s with [ BGND_MODE ⇒ p | STOP_MODE ⇒ p1 | WAIT_MODE ⇒ p2 ].
-
 (* un tipo opzione ad hoc
    - errore: errore+stato (seguira' reset o ??, cmq lo stato non va buttato)
    - sospensione: sospensione+stato (seguira' resume o ??)
@@ -1153,27 +1141,6 @@ ninductive tick_result (A:Type) : Type ≝
 | TickSUSP  : A → susp_type → tick_result A
 | TickOK    : A → tick_result A.
 
-ndefinition tick_result_ind
- : ΠA:Type.ΠP:tick_result A → Prop.(Πa:A.Πn:error_type.P (TickERR A a n)) →
-   (Πa:A.Πn:susp_type.P (TickSUSP A a n)) → (Πa:A.P (TickOK A a))→Πt:tick_result A.P t ≝
-λA:Type.λP:tick_result A → Prop.λf:Πa:A.Πn:error_type.P (TickERR A a n).
-λf1:Πa:A.Πn:susp_type.P (TickSUSP A a n).λf2:Πa:A.P (TickOK A a).λt:tick_result A.
- match t with [ TickERR a n ⇒ f a n | TickSUSP a n ⇒ f1 a n | TickOK a ⇒ f2 a ].
-
-ndefinition tick_result_rec
- : ΠA:Type.ΠP:tick_result A → Set.(Πa:A.Πn:error_type.P (TickERR A a n)) →
-   (Πa:A.Πn:susp_type.P (TickSUSP A a n)) → (Πa:A.P (TickOK A a))→Πt:tick_result A.P t ≝
-λA:Type.λP:tick_result A → Set.λf:Πa:A.Πn:error_type.P (TickERR A a n).
-λf1:Πa:A.Πn:susp_type.P (TickSUSP A a n).λf2:Πa:A.P (TickOK A a).λt:tick_result A.
- match t with [ TickERR a n ⇒ f a n | TickSUSP a n ⇒ f1 a n | TickOK a ⇒ f2 a ].
-
-ndefinition tick_result_rect
- : ΠA:Type.ΠP:tick_result A → Type.(Πa:A.Πn:error_type.P (TickERR A a n)) →
-   (Πa:A.Πn:susp_type.P (TickSUSP A a n)) → (Πa:A.P (TickOK A a))→Πt:tick_result A.P t ≝
-λA:Type.λP:tick_result A → Type.λf:Πa:A.Πn:error_type.P (TickERR A a n).
-λf1:Πa:A.Πn:susp_type.P (TickSUSP A a n).λf2:Πa:A.P (TickOK A a).λt:tick_result A.
- match t with [ TickERR a n ⇒ f a n | TickSUSP a n ⇒ f1 a n | TickOK a ⇒ f2 a ].
-
 (* sostanazialmente simula
    - fetch/decode/execute
    - l'esecuzione e' considerata atomica quindi nel caso di un'instruzione
diff --git a/helm/software/matita/contribs/ng_assembly/freescale/status.ma b/helm/software/matita/contribs/ng_assembly/freescale/status.ma
index b20d2e814..e6d42deed 100755
--- a/helm/software/matita/contribs/ng_assembly/freescale/status.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/status.ma
@@ -165,37 +165,6 @@ nrecord any_status (mcu:mcu_type) (t:memory_impl): Type ≝
  clk_desc : option (Prod5T byte8 (any_opcode mcu) (instr_mode) byte8 word16)
  }.
 
-ndefinition any_status_ind : 
- Πmcu.Πt.ΠP:any_status mcu t → Prop.
- (Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
-  Πn,n1,n2.P (mk_any_status mcu t x n n1 n2)) → Πa:any_status mcu t.P a ≝
-λmcu.λt.λP:any_status mcu t → Prop.
-λf:Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
- Πn,n1,n2.P (mk_any_status mcu t x n n1 n2).λa:any_status mcu t.
- match a with [ mk_any_status x n n1 n2 ⇒ f x n n1 n2 ].
-
-ndefinition any_status_rec : 
- Πmcu.Πt.ΠP:any_status mcu t → Set.
- (Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
-  Πn,n1,n2.P (mk_any_status mcu t x n n1 n2)) → Πa:any_status mcu t.P a ≝
-λmcu.λt.λP:any_status mcu t → Set.
-λf:Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
- Πn,n1,n2.P (mk_any_status mcu t x n n1 n2).λa:any_status mcu t.
- match a with [ mk_any_status x n n1 n2 ⇒ f x n n1 n2 ].
-
-ndefinition any_status_rect : 
- Πmcu.Πt.ΠP:any_status mcu t → Type.
- (Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
-  Πn,n1,n2.P (mk_any_status mcu t x n n1 n2)) → Πa:any_status mcu t.P a ≝
-λmcu.λt.λP:any_status mcu t → Type.
-λf:Πx:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ].
- Πn,n1,n2.P (mk_any_status mcu t x n n1 n2).λa:any_status mcu t.
- match a with [ mk_any_status x n n1 n2 ⇒ f x n n1 n2 ].
-
-ndefinition alu ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status (x:match mcu with [ HC05 ⇒ alu_HC05 | HC08 ⇒ alu_HC08 | HCS08 ⇒ alu_HC08 | RS08 ⇒ alu_RS08 ]) _ _ _ ⇒ x ].
-ndefinition mem_desc ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status _ x _ _ ⇒ x ].     
-ndefinition chk_desc ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status _ _ x _ ⇒ x ].
-ndefinition clk_desc ≝ λmcu.λt.λw:any_status mcu t.match w with [ mk_any_status _ _ _ x ⇒ x ].
 
 (* evitare di mostrare la memoria/descrittore che impalla il visualizzatore *)
 notation > "{hvbox('Alu' ≝ alu ; break 'Clk' ≝ clk)}" non associative with precedence 80