...

[helm.git] / helm / software / matita / contribs / ng_assembly / freescale / model.ma

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)