489 lemma type_substitution_aux: |
489 lemma type_substitution_aux: |
490 assumes a: "(\<Delta>@[(x,T')]@\<Gamma>) \<turnstile> e : T" |
490 assumes a: "(\<Delta>@[(x,T')]@\<Gamma>) \<turnstile> e : T" |
491 and b: "\<Gamma> \<turnstile> e' : T'" |
491 and b: "\<Gamma> \<turnstile> e' : T'" |
492 shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T" |
492 shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T" |
493 using a b |
493 using a b |
494 proof (nominal_induct \<Gamma>'\<equiv>"\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct) |
494 proof (nominal_induct "\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct) |
495 case (t_VAR y T x e' \<Delta>) |
495 case (t_VAR y T x e' \<Delta>) |
496 then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)" |
496 then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)" |
497 and a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)" |
497 and a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)" |
498 and a3: "\<Gamma> \<turnstile> e' : T'" by simp_all |
498 and a3: "\<Gamma> \<turnstile> e' : T'" . |
499 from a1 have a4: "valid (\<Delta>@\<Gamma>)" by (rule valid_insert) |
499 from a1 have a4: "valid (\<Delta>@\<Gamma>)" by (rule valid_insert) |
500 { assume eq: "x=y" |
500 { assume eq: "x=y" |
501 from a1 a2 have "T=T'" using eq by (auto intro: context_unique) |
501 from a1 a2 have "T=T'" using eq by (auto intro: context_unique) |
502 with a3 have "\<Delta>@\<Gamma> \<turnstile> VAR y[x::=e'] : T" using eq a4 by (auto intro: weakening) |
502 with a3 have "\<Delta>@\<Gamma> \<turnstile> VAR y[x::=e'] : T" using eq a4 by (auto intro: weakening) |
503 } |
503 } |