(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
definition nta (h) (a): relation4 genv lenv term term ≝
- λG,L,T,U. â¦\83G,Lâ¦\84 ⊢ ⓝU.T ![h,a].
+ λG,L,T,U. â\9dªG,Lâ\9d« ⊢ ⓝU.T ![h,a].
interpretation "native type assignment (term)"
'Colon h a G L T U = (nta h a G L T U).
(* Basic_1: was by definition: ty3_sort *)
(* Basic_2A1: was by definition: nta_sort ntaa_sort *)
-lemma nta_sort (h) (a) (G) (L): â\88\80s. â¦\83G,Lâ¦\84 ⊢ ⋆s :[h,a] ⋆(⫯[h]s).
+lemma nta_sort (h) (a) (G) (L): â\88\80s. â\9dªG,Lâ\9d« ⊢ ⋆s :[h,a] ⋆(⫯[h]s).
#h #a #G #L #s /2 width=3 by cnv_sort, cnv_cast, cpms_sort/
qed.
lemma nta_bind_cnv (h) (a) (G) (K):
- â\88\80V. â¦\83G,Kâ¦\84 ⊢ V ![h,a] →
- â\88\80I,T,U. â¦\83G,K.â\93\91{I}Vâ¦\84 ⊢ T :[h,a] U →
- â\88\80p. â¦\83G,Kâ¦\84 â\8a¢ â\93\91{p,I}V.T :[h,a] â\93\91{p,I}V.U.
+ â\88\80V. â\9dªG,Kâ\9d« ⊢ V ![h,a] →
+ â\88\80I,T,U. â\9dªG,K.â\93\91[I]Vâ\9d« ⊢ T :[h,a] U →
+ â\88\80p. â\9dªG,Kâ\9d« â\8a¢ â\93\91[p,I]V.T :[h,a] â\93\91[p,I]V.U.
#h #a #G #K #V #HV #I #T #U #H #p
elim (cnv_inv_cast … H) -H #X #HU #HT #HUX #HTX
/3 width=5 by cnv_bind, cnv_cast, cpms_bind_dx/
(* Basic_2A1: was by definition: nta_cast *)
lemma nta_cast (h) (a) (G) (L):
- â\88\80T,U. â¦\83G,Lâ¦\84 â\8a¢ T :[h,a] U â\86\92 â¦\83G,Lâ¦\84 ⊢ ⓝU.T :[h,a] U.
+ â\88\80T,U. â\9dªG,Lâ\9d« â\8a¢ T :[h,a] U â\86\92 â\9dªG,Lâ\9d« ⊢ ⓝU.T :[h,a] U.
#h #a #G #L #T #U #H
elim (cnv_inv_cast … H) #X #HU #HT #HUX #HTX
/3 width=3 by cnv_cast, cpms_eps/
(* Basic_1: was by definition: ty3_cast *)
lemma nta_cast_old (h) (a) (G) (L):
- â\88\80T0,T1. â¦\83G,Lâ¦\84 ⊢ T0 :[h,a] T1 →
- â\88\80T2. â¦\83G,Lâ¦\84 â\8a¢ T1 :[h,a] T2 â\86\92 â¦\83G,Lâ¦\84 ⊢ ⓝT1.T0 :[h,a] ⓝT2.T1.
+ â\88\80T0,T1. â\9dªG,Lâ\9d« ⊢ T0 :[h,a] T1 →
+ â\88\80T2. â\9dªG,Lâ\9d« â\8a¢ T1 :[h,a] T2 â\86\92 â\9dªG,Lâ\9d« ⊢ ⓝT1.T0 :[h,a] ⓝT2.T1.
#h #a #G #L #T0 #T1 #H1 #T2 #H2
elim (cnv_inv_cast … H1) #X1 #_ #_ #HTX1 #HTX01
elim (cnv_inv_cast … H2) #X2 #_ #_ #HTX2 #HTX12
(* Basic inversion lemmas ***************************************************)
lemma nta_inv_gref_sn (h) (a) (G) (L):
- â\88\80X2,l. â¦\83G,Lâ¦\84 ⊢ §l :[h,a] X2 → ⊥.
+ â\88\80X2,l. â\9dªG,Lâ\9d« ⊢ §l :[h,a] X2 → ⊥.
#h #a #G #L #X2 #l #H
elim (cnv_inv_cast … H) -H #X #_ #H #_ #_
elim (cnv_inv_gref … H)
(* Basic_forward lemmas *****************************************************)
lemma nta_fwd_cnv_sn (h) (a) (G) (L):
- â\88\80T,U. â¦\83G,Lâ¦\84 â\8a¢ T :[h,a] U â\86\92 â¦\83G,Lâ¦\84 ⊢ T ![h,a].
+ â\88\80T,U. â\9dªG,Lâ\9d« â\8a¢ T :[h,a] U â\86\92 â\9dªG,Lâ\9d« ⊢ T ![h,a].
#h #a #G #L #T #U #H
elim (cnv_inv_cast … H) -H #X #_ #HT #_ #_ //
qed-.
(* Note: this is nta_fwd_correct_cnv *)
lemma nta_fwd_cnv_dx (h) (a) (G) (L):
- â\88\80T,U. â¦\83G,Lâ¦\84 â\8a¢ T :[h,a] U â\86\92 â¦\83G,Lâ¦\84 ⊢ U ![h,a].
+ â\88\80T,U. â\9dªG,Lâ\9d« â\8a¢ T :[h,a] U â\86\92 â\9dªG,Lâ\9d« ⊢ U ![h,a].
#h #a #G #L #T #U #H
elim (cnv_inv_cast … H) -H #X #HU #_ #_ #_ //
qed-.