...

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 83abb181625a358691467fb24c84df24a477ac84..5bfd406b5296052c5ca36c161a0f683706f6648a 100755 (executable)
--- 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 adafa40f3f3e59ac6e3f6cccc753b3fc557e4eea..e91ff5f65183a323bef6e04b2c7ca10ce1a0cf6b 100755 (executable)
--- 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 4ae8093d1b00a3aa3ace848b0e3fe3b0fa0d9852..fc374d9ab6e6d8530045268548d169b89a3b6dbf 100755 (executable)
--- 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 b20d2e8145e2796411035267bde0a777a03c22d5..e6d42deedfdf536cc7c6bcf25a315423057c4842 100755 (executable)
--- 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