(* ITERATED NATIVE TYPE ASSIGNMENT FOR TERMS ********************************)
definition ntas (h) (a) (n) (G) (L): relation term ≝ λT,U.
- â\88\83â\88\83U0. â¦\83G,Lâ¦\84 â\8a¢ U ![h,a] & â¦\83G,Lâ¦\84 â\8a¢ T ![h,a] & â¦\83G,Lâ¦\84 â\8a¢ U â\9e¡*[h] U0 & â¦\83G,Lâ¦\84 ⊢ T ➡*[n,h] U0.
+ â\88\83â\88\83U0. â\9dªG,Lâ\9d« â\8a¢ U ![h,a] & â\9dªG,Lâ\9d« â\8a¢ T ![h,a] & â\9dªG,Lâ\9d« â\8a¢ U â\9e¡*[h] U0 & â\9dªG,Lâ\9d« ⊢ T ➡*[n,h] U0.
interpretation "iterated native type assignment (term)"
'ColonStar h a n G L T U = (ntas h a n G L T U).
(* Basic properties *********************************************************)
lemma ntas_intro (h) (a) (n) (G) (L):
- â\88\80U. â¦\83G,Lâ¦\84 â\8a¢ U ![h,a] â\86\92 â\88\80T. â¦\83G,Lâ¦\84 ⊢ T ![h,a] →
- â\88\80U0. â¦\83G,Lâ¦\84 â\8a¢ U â\9e¡*[h] U0 â\86\92 â¦\83G,Lâ¦\84 â\8a¢ T â\9e¡*[n,h] U0 â\86\92 â¦\83G,Lâ¦\84 ⊢ T :*[h,a,n] U.
+ â\88\80U. â\9dªG,Lâ\9d« â\8a¢ U ![h,a] â\86\92 â\88\80T. â\9dªG,Lâ\9d« ⊢ T ![h,a] →
+ â\88\80U0. â\9dªG,Lâ\9d« â\8a¢ U â\9e¡*[h] U0 â\86\92 â\9dªG,Lâ\9d« â\8a¢ T â\9e¡*[n,h] U0 â\86\92 â\9dªG,Lâ\9d« ⊢ T :*[h,a,n] U.
/2 width=3 by ex4_intro/ qed.
lemma ntas_refl (h) (a) (G) (L):
- â\88\80T. â¦\83G,Lâ¦\84 â\8a¢ T ![h,a] â\86\92 â¦\83G,Lâ¦\84 ⊢ T :*[h,a,0] T.
+ â\88\80T. â\9dªG,Lâ\9d« â\8a¢ T ![h,a] â\86\92 â\9dªG,Lâ\9d« ⊢ T :*[h,a,0] T.
/2 width=3 by ntas_intro/ qed.
lemma ntas_sort (h) (a) (n) (G) (L):
- â\88\80s. â¦\83G,Lâ¦\84 ⊢ ⋆s :*[h,a,n] ⋆((next h)^n s).
+ â\88\80s. â\9dªG,Lâ\9d« ⊢ ⋆s :*[h,a,n] ⋆((next h)^n s).
#h #a #n #G #L #s
/2 width=3 by ntas_intro, cnv_sort, cpms_sort/
qed.
lemma ntas_bind_cnv (h) (a) (n) (G) (K):
- â\88\80V. â¦\83G,Kâ¦\84 ⊢ V ![h,a] →
- â\88\80I,T,U. â¦\83G,K.â\93\91{I}Vâ¦\84 ⊢ T :*[h,a,n] U →
- â\88\80p. â¦\83G,Kâ¦\84 â\8a¢ â\93\91{p,I}V.T :*[h,a,n] â\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,n] U →
+ â\88\80p. â\9dªG,Kâ\9d« â\8a¢ â\93\91[p,I]V.T :*[h,a,n] â\93\91[p,I]V.U.
#h #a #n #G #K #V #HV #I #T #U
* #X #HU #HT #HUX #HTX #p
/3 width=5 by ntas_intro, cnv_bind, cpms_bind_dx/
(* Basic_forward lemmas *****************************************************)
lemma ntas_fwd_cnv_sn (h) (a) (n) (G) (L):
- â\88\80T,U. â¦\83G,Lâ¦\84 â\8a¢ T :*[h,a,n] U â\86\92 â¦\83G,Lâ¦\84 ⊢ T ![h,a].
+ â\88\80T,U. â\9dªG,Lâ\9d« â\8a¢ T :*[h,a,n] U â\86\92 â\9dªG,Lâ\9d« ⊢ T ![h,a].
#h #a #n #G #L #T #U
* #X #_ #HT #_ #_ //
qed-.
(* Note: this is ntas_fwd_correct_cnv *)
lemma ntas_fwd_cnv_dx (h) (a) (n) (G) (L):
- â\88\80T,U. â¦\83G,Lâ¦\84 â\8a¢ T :*[h,a,n] U â\86\92 â¦\83G,Lâ¦\84 ⊢ U ![h,a].
+ â\88\80T,U. â\9dªG,Lâ\9d« â\8a¢ T :*[h,a,n] U â\86\92 â\9dªG,Lâ\9d« ⊢ U ![h,a].
#h #a #n #G #L #T #U
* #X #HU #_ #_ #_ //
qed-.