equal
deleted
inserted
replaced
140 assumes a: "(\<Delta>@[(x,T')]@\<Gamma>) \<turnstile> e : T" |
140 assumes a: "(\<Delta>@[(x,T')]@\<Gamma>) \<turnstile> e : T" |
141 and b: "\<Gamma> \<turnstile> e' : T'" |
141 and b: "\<Gamma> \<turnstile> e' : T'" |
142 shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T" |
142 shows "(\<Delta>@\<Gamma>) \<turnstile> e[x::=e'] : T" |
143 using a b |
143 using a b |
144 proof (nominal_induct \<Gamma>'\<equiv>"\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct) |
144 proof (nominal_induct \<Gamma>'\<equiv>"\<Delta>@[(x,T')]@\<Gamma>" e T avoiding: x e' \<Delta> rule: typing.strong_induct) |
145 case (t_Var \<Gamma>' y T x e' \<Delta>) |
145 case (t_Var y T x e' \<Delta>) |
146 then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)" |
146 then have a1: "valid (\<Delta>@[(x,T')]@\<Gamma>)" |
147 and a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)" |
147 and a2: "(y,T) \<in> set (\<Delta>@[(x,T')]@\<Gamma>)" |
148 and a3: "\<Gamma> \<turnstile> e' : T'" by simp_all |
148 and a3: "\<Gamma> \<turnstile> e' : T'" by simp_all |
149 from a1 have a4: "valid (\<Delta>@\<Gamma>)" by (rule valid_insert) |
149 from a1 have a4: "valid (\<Delta>@\<Gamma>)" by (rule valid_insert) |
150 { assume eq: "x=y" |
150 { assume eq: "x=y" |