18269

1 
(* $Id$ *)

18105

2 

18269

3 
theory weakening

18105

4 
imports "../nominal"


5 
begin


6 


7 
(* WEAKENING EXAMPLE*)


8 


9 
section {* SimplyTyped LambdaCalculus *}


10 
(*======================================*)


11 


12 
atom_decl name


13 


14 
nominal_datatype lam = Var "name"


15 
 App "lam" "lam"


16 
 Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)


17 


18 
datatype ty =


19 
TVar "string"


20 
 TArr "ty" "ty" (infix "\<rightarrow>" 200)


21 


22 
primrec


23 
"pi\<bullet>(TVar s) = TVar s"


24 
"pi\<bullet>(\<tau> \<rightarrow> \<sigma>) = (\<tau> \<rightarrow> \<sigma>)"


25 


26 
lemma perm_ty[simp]:


27 
fixes pi ::"name prm"


28 
and \<tau> ::"ty"


29 
shows "pi\<bullet>\<tau> = \<tau>"


30 
by (cases \<tau>, simp_all)


31 


32 
instance ty :: pt_name


33 
apply(intro_classes)


34 
apply(simp_all)


35 
done


36 


37 
instance ty :: fs_name


38 
apply(intro_classes)


39 
apply(simp add: supp_def)


40 
done


41 


42 
(* valid contexts *)


43 
consts


44 
ctxts :: "((name\<times>ty) list) set"


45 
valid :: "(name\<times>ty) list \<Rightarrow> bool"


46 
translations


47 
"valid \<Gamma>" \<rightleftharpoons> "\<Gamma> \<in> ctxts"


48 
inductive ctxts


49 
intros


50 
v1[intro]: "valid []"


51 
v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)"


52 


53 
lemma eqvt_valid:


54 
fixes pi:: "name prm"


55 
assumes a: "valid \<Gamma>"


56 
shows "valid (pi\<bullet>\<Gamma>)"


57 
using a


58 
apply(induct)


59 
apply(auto simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst])


60 
done


61 


62 
(* typing judgements *)


63 
consts


64 
typing :: "(((name\<times>ty) list)\<times>lam\<times>ty) set"


65 
syntax


66 
"_typing_judge" :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80)


67 
translations


68 
"\<Gamma> \<turnstile> t : \<tau>" \<rightleftharpoons> "(\<Gamma>,t,\<tau>) \<in> typing"


69 


70 
inductive typing


71 
intros


72 
t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>"


73 
t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>"


74 
t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>"


75 


76 
lemma eqvt_typing:


77 
fixes \<Gamma> :: "(name\<times>ty) list"


78 
and t :: "lam"


79 
and \<tau> :: "ty"


80 
and pi:: "name prm"


81 
assumes a: "\<Gamma> \<turnstile> t : \<tau>"


82 
shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : \<tau>"


83 
using a


84 
proof (induct)


85 
case (t1 \<Gamma> \<tau> a)


86 
have "valid (pi\<bullet>\<Gamma>)" by (rule eqvt_valid)


87 
moreover


88 
have "(pi\<bullet>(a,\<tau>))\<in>((pi::name prm)\<bullet>set \<Gamma>)" by (rule pt_set_bij2[OF pt_name_inst, OF at_name_inst])


89 
ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> ((pi::name prm)\<bullet>Var a) : \<tau>"


90 
using typing.intros by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric])


91 
next


92 
case (t3 \<Gamma> \<sigma> \<tau> a t)


93 
moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (rule pt_fresh_bij1[OF pt_name_inst, OF at_name_inst])


94 
ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force


95 
qed (auto)


96 


97 


98 
lemma typing_induct_weak[THEN spec, case_names t1 t2 t3]:

18296

99 
fixes P :: "'a\<Rightarrow>(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>bool"

18105

100 
and \<Gamma> :: "(name\<times>ty) list"


101 
and t :: "lam"


102 
and \<tau> :: "ty"


103 
assumes a: "\<Gamma> \<turnstile> t : \<tau>"

18296

104 
and a1: "\<And>\<Gamma> (a::name) \<tau> x. valid \<Gamma> \<Longrightarrow> (a,\<tau>) \<in> set \<Gamma> \<Longrightarrow> P x \<Gamma> (Var a) \<tau>"


105 
and a2: "\<And>\<Gamma> \<tau> \<sigma> t1 t2 x.


106 
\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<Longrightarrow> (\<And>z. P z \<Gamma> t1 (\<tau>\<rightarrow>\<sigma>)) \<Longrightarrow> \<Gamma> \<turnstile> t2 : \<tau> \<Longrightarrow> (\<And>z. P z \<Gamma> t2 \<tau>)


107 
\<Longrightarrow> P x \<Gamma> (App t1 t2) \<sigma>"


108 
and a3: "\<And>(a::name) \<Gamma> \<tau> \<sigma> t x.


109 
a\<sharp>\<Gamma> \<Longrightarrow> ((a,\<tau>) # \<Gamma>) \<turnstile> t : \<sigma> \<Longrightarrow> (\<And>z. P z ((a,\<tau>)#\<Gamma>) t \<sigma>)


110 
\<Longrightarrow> P x \<Gamma> (Lam [a].t) (\<tau>\<rightarrow>\<sigma>)"


111 
shows "\<forall>x. P x \<Gamma> t \<tau>"

18105

112 
using a by (induct, simp_all add: a1 a2 a3)


113 


114 
lemma typing_induct_aux[rule_format]:

18296

115 
fixes P :: "'a::fs_name \<Rightarrow> (name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>bool"

18105

116 
and \<Gamma> :: "(name\<times>ty) list"


117 
and t :: "lam"


118 
and \<tau> :: "ty"


119 
assumes a: "\<Gamma> \<turnstile> t : \<tau>"

18296

120 
and a1: "\<And>\<Gamma> (a::name) \<tau> x. valid \<Gamma> \<Longrightarrow> (a,\<tau>) \<in> set \<Gamma> \<Longrightarrow> P x \<Gamma> (Var a) \<tau>"


121 
and a2: "\<And>\<Gamma> \<tau> \<sigma> t1 t2 x.


122 
\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<Longrightarrow> (\<And>z. P z \<Gamma> t1 (\<tau>\<rightarrow>\<sigma>)) \<Longrightarrow> \<Gamma> \<turnstile> t2 : \<tau> \<Longrightarrow> (\<And>z. P z \<Gamma> t2 \<tau>)


123 
\<Longrightarrow> P x \<Gamma> (App t1 t2) \<sigma>"


124 
and a3: "\<And>(a::name) \<Gamma> \<tau> \<sigma> t x.


125 
a\<sharp>x \<Longrightarrow> a\<sharp>\<Gamma> \<Longrightarrow> ((a,\<tau>) # \<Gamma>) \<turnstile> t : \<sigma> \<Longrightarrow> (\<And>z. P z ((a,\<tau>)#\<Gamma>) t \<sigma>)


126 
\<Longrightarrow> P x \<Gamma> (Lam [a].t) (\<tau>\<rightarrow>\<sigma>)"


127 
shows "\<forall>(pi::name prm) (x::'a::fs_name). P x (pi\<bullet>\<Gamma>) (pi\<bullet>t) \<tau>"

18105

128 
using a


129 
proof (induct)


130 
case (t1 \<Gamma> \<tau> a)


131 
have j1: "valid \<Gamma>" by fact


132 
have j2: "(a,\<tau>)\<in>set \<Gamma>" by fact


133 
show ?case


134 
proof (intro strip, simp)


135 
fix pi::"name prm" and x::"'a::fs_name"


136 
from j1 have j3: "valid (pi\<bullet>\<Gamma>)" by (rule eqvt_valid)


137 
from j2 have "pi\<bullet>(a,\<tau>)\<in>pi\<bullet>(set \<Gamma>)" by (simp only: pt_set_bij[OF pt_name_inst, OF at_name_inst])


138 
hence j4: "(pi\<bullet>a,\<tau>)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: pt_list_set_pi[OF pt_name_inst])

18296

139 
show "P x (pi\<bullet>\<Gamma>) (Var (pi\<bullet>a)) \<tau>" using a1 j3 j4 by force

18105

140 
qed


141 
next


142 
case (t2 \<Gamma> \<sigma> \<tau> t1 t2)


143 
thus ?case using a2 by (simp, blast intro: eqvt_typing)


144 
next


145 
case (t3 \<Gamma> \<sigma> \<tau> a t)


146 
have k1: "a\<sharp>\<Gamma>" by fact


147 
have k2: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact

18296

148 
have k3: "\<forall>(pi::name prm) (x::'a::fs_name). P x (pi \<bullet>((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma>" by fact

18105

149 
show ?case


150 
proof (intro strip, simp)


151 
fix pi::"name prm" and x::"'a::fs_name"


152 
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)"


153 
by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1)


154 
then obtain c::"name"


155 
where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>t)" and f4: "c\<sharp>(pi\<bullet>\<Gamma>)"


156 
by (force simp add: fresh_prod at_fresh[OF at_name_inst])


157 
from k1 have k1a: "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)"


158 
by (simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst]


159 
pt_rev_pi[OF pt_name_inst, OF at_name_inst])


160 
have l1: "(([(c,pi\<bullet>a)]@pi)\<bullet>\<Gamma>) = (pi\<bullet>\<Gamma>)" using f4 k1a


161 
by (simp only: pt2[OF pt_name_inst], rule pt_fresh_fresh[OF pt_name_inst, OF at_name_inst])

18296

162 
have "\<forall>x. P x (([(c,pi\<bullet>a)]@pi)\<bullet>((a,\<tau>)#\<Gamma>)) (([(c,pi\<bullet>a)]@pi)\<bullet>t) \<sigma>" using k3 by force


163 
hence l2: "\<forall>x. P x ((c, \<tau>)#(pi\<bullet>\<Gamma>)) (([(c,pi\<bullet>a)]@pi)\<bullet>t) \<sigma>" using f1 l1

18105

164 
by (force simp add: pt2[OF pt_name_inst] at_calc[OF at_name_inst] split: if_splits)


165 
have "(([(c,pi\<bullet>a)]@pi)\<bullet>((a,\<tau>)#\<Gamma>)) \<turnstile> (([(c,pi\<bullet>a)]@pi)\<bullet>t) : \<sigma>" using k2 by (rule eqvt_typing)


166 
hence l3: "((c, \<tau>)#(pi\<bullet>\<Gamma>)) \<turnstile> (([(c,pi\<bullet>a)]@pi)\<bullet>t) : \<sigma>" using l1 f1


167 
by (force simp add: pt2[OF pt_name_inst] at_calc[OF at_name_inst] split: if_splits)

18296

168 
have l4: "P x (pi\<bullet>\<Gamma>) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>t)) (\<tau> \<rightarrow> \<sigma>)" using f2 f4 l2 l3 a3 by auto

18105

169 
have alpha: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t))" using f1 f3


170 
by (simp add: lam.inject alpha)

18296

171 
show "P x (pi\<bullet>\<Gamma>) (Lam [(pi\<bullet>a)].(pi\<bullet>t)) (\<tau> \<rightarrow> \<sigma>)" using l4 alpha

18105

172 
by (simp only: pt2[OF pt_name_inst])


173 
qed


174 
qed


175 

18296

176 
lemma typing_induct[consumes 1, case_names t1 t2 t3]:


177 
fixes P :: "'a::fs_name\<Rightarrow>(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>bool"

18105

178 
and \<Gamma> :: "(name\<times>ty) list"


179 
and t :: "lam"


180 
and \<tau> :: "ty"


181 
and x :: "'a::fs_name"


182 
assumes a: "\<Gamma> \<turnstile> t : \<tau>"

18296

183 
and a1: "\<And>\<Gamma> (a::name) \<tau> x. valid \<Gamma> \<Longrightarrow> (a,\<tau>) \<in> set \<Gamma> \<Longrightarrow> P x \<Gamma> (Var a) \<tau>"


184 
and a2: "\<And>\<Gamma> \<tau> \<sigma> t1 t2 x.


185 
\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<Longrightarrow> (\<And>z. P z \<Gamma> t1 (\<tau>\<rightarrow>\<sigma>)) \<Longrightarrow> \<Gamma> \<turnstile> t2 : \<tau> \<Longrightarrow> (\<And>z. P z \<Gamma> t2 \<tau>)


186 
\<Longrightarrow> P x \<Gamma> (App t1 t2) \<sigma>"


187 
and a3: "\<And>(a::name) \<Gamma> \<tau> \<sigma> t x.


188 
a\<sharp>x \<Longrightarrow> a\<sharp>\<Gamma> \<Longrightarrow> ((a,\<tau>) # \<Gamma>) \<turnstile> t : \<sigma> \<Longrightarrow> (\<And>z. P z ((a,\<tau>)#\<Gamma>) t \<sigma>)


189 
\<Longrightarrow> P x \<Gamma> (Lam [a].t) (\<tau>\<rightarrow>\<sigma>)"


190 
shows "P x \<Gamma> t \<tau>"


191 
using a a1 a2 a3 typing_induct_aux[of "\<Gamma>" "t" "\<tau>" "P" "x" "[]", simplified] by force

18105

192 


193 


194 
(* Now it comes: The Weakening Lemma *)


195 


196 
constdefs


197 
"sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [80,80] 80)


198 
"\<Gamma>1 \<lless> \<Gamma>2 \<equiv> \<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow> (a,\<sigma>)\<in>set \<Gamma>2"


199 


200 
lemma weakening_version1[rule_format]:

18296

201 
assumes "\<Gamma>1 \<turnstile> t : \<sigma>"


202 
and "valid \<Gamma>2"


203 
and "\<Gamma>1 \<lless> \<Gamma>2"


204 
shows "\<Gamma>2 \<turnstile> t:\<sigma>"


205 
using prems


206 
apply(nominal_induct \<Gamma>1 t \<sigma> fresh: \<Gamma>2 rule: typing_induct)

18105

207 
apply(auto simp add: sub_def)

18296

208 
apply(atomize) (* FIXME: earlier this was completely automatic :o( *)


209 
apply(auto)

18105

210 
done


211 


212 
lemma weakening_version2[rule_format]:


213 
fixes \<Gamma>1::"(name\<times>ty) list"


214 
and t ::"lam"


215 
and \<tau> ::"ty"


216 
assumes a: "\<Gamma>1 \<turnstile> t:\<sigma>"


217 
shows "valid \<Gamma>2 \<longrightarrow> \<Gamma>1 \<lless> \<Gamma>2 \<longrightarrow> \<Gamma>2 \<turnstile> t:\<sigma>"

18296

218 
using prems


219 
proof (nominal_induct \<Gamma>1 t \<sigma> fresh: \<Gamma>2 rule: typing_induct, auto)


220 
case (t1 \<Gamma>1 a \<tau> \<Gamma>2) (* variable case *)

18105

221 
assume "\<Gamma>1 \<lless> \<Gamma>2"


222 
and "valid \<Gamma>2"


223 
and "(a,\<tau>)\<in> set \<Gamma>1"


224 
thus "\<Gamma>2 \<turnstile> Var a : \<tau>" by (force simp add: sub_def)


225 
next

18296

226 
case (t3 a \<Gamma>1 \<tau> \<sigma> t \<Gamma>2) (* lambda case *)

18105

227 
assume a1: "\<Gamma>1 \<lless> \<Gamma>2"


228 
and a2: "valid \<Gamma>2"


229 
and a3: "a\<sharp>\<Gamma>2"

18296

230 
have i: "\<And>\<Gamma>3. valid \<Gamma>3 \<longrightarrow> ((a,\<tau>)#\<Gamma>1) \<lless> \<Gamma>3 \<longrightarrow> \<Gamma>3 \<turnstile> t:\<sigma>" by fact

18105

231 
have "((a,\<tau>)#\<Gamma>1) \<lless> ((a,\<tau>)#\<Gamma>2)" using a1 by (simp add: sub_def)


232 
moreover


233 
have "valid ((a,\<tau>)#\<Gamma>2)" using a2 a3 v2 by force


234 
ultimately have "((a,\<tau>)#\<Gamma>2) \<turnstile> t:\<sigma>" using i by force


235 
with a3 show "\<Gamma>2 \<turnstile> (Lam [a].t) : \<tau> \<rightarrow> \<sigma>" by force


236 
qed


237 


238 
lemma weakening_version3[rule_format]:


239 
fixes \<Gamma>1::"(name\<times>ty) list"


240 
and t ::"lam"


241 
and \<tau> ::"ty"

18296

242 
assumes "\<Gamma>1 \<turnstile> t:\<sigma>"

18105

243 
shows "valid \<Gamma>2 \<longrightarrow> \<Gamma>1 \<lless> \<Gamma>2 \<longrightarrow> \<Gamma>2 \<turnstile> t:\<sigma>"

18296

244 
using prems


245 
proof (nominal_induct \<Gamma>1 t \<sigma> fresh: \<Gamma>2 rule: typing_induct)


246 
case (t1 \<Gamma>1 a \<tau> \<Gamma>2) (* variable case *)

18105

247 
thus "valid \<Gamma>2 \<longrightarrow> \<Gamma>1 \<lless> \<Gamma>2 \<longrightarrow> \<Gamma>2 \<turnstile> Var a : \<tau>" by (force simp add: sub_def)


248 
next

18296

249 
case (t2 \<Gamma>1 \<tau> \<sigma> t1 t2 \<Gamma>2) (* variable case *)

18105

250 
thus "valid \<Gamma>2 \<longrightarrow> \<Gamma>1 \<lless> \<Gamma>2 \<longrightarrow> \<Gamma>2 \<turnstile> App t1 t2 : \<sigma>" by force


251 
next

18296

252 
case (t3 a \<Gamma>1 \<tau> \<sigma> t \<Gamma>2) (* lambda case *)


253 
have a3: "a\<sharp>\<Gamma>2" by fact


254 
have ih: "\<And>\<Gamma>3. valid \<Gamma>3 \<longrightarrow> ((a,\<tau>)#\<Gamma>1) \<lless> \<Gamma>3 \<longrightarrow> \<Gamma>3 \<turnstile> t:\<sigma>" by fact

18105

255 
show "valid \<Gamma>2 \<longrightarrow> \<Gamma>1 \<lless> \<Gamma>2 \<longrightarrow> \<Gamma>2 \<turnstile> (Lam [a].t) : \<tau> \<rightarrow> \<sigma>"


256 
proof (intro strip)


257 
assume a1: "\<Gamma>1 \<lless> \<Gamma>2"


258 
and a2: "valid \<Gamma>2"


259 
have "((a,\<tau>)#\<Gamma>1) \<lless> ((a,\<tau>)#\<Gamma>2)" using a1 by (simp add: sub_def)


260 
moreover


261 
have "valid ((a,\<tau>)#\<Gamma>2)" using a2 a3 v2 by force

18296

262 
ultimately have "((a,\<tau>)#\<Gamma>2) \<turnstile> t:\<sigma>" using ih by force

18105

263 
with a3 show "\<Gamma>2 \<turnstile> (Lam [a].t) : \<tau> \<rightarrow> \<sigma>" by force


264 
qed


265 
qed


266 


267 
lemma weakening_version4[rule_format]:

18296

268 
assumes "\<Gamma>1 \<turnstile> t:\<sigma>"

18105

269 
shows "valid \<Gamma>2 \<longrightarrow> \<Gamma>1 \<lless> \<Gamma>2 \<longrightarrow> \<Gamma>2 \<turnstile> t:\<sigma>"

18296

270 
using prems


271 
proof (nominal_induct \<Gamma>1 t \<sigma> fresh: \<Gamma>2 rule: typing_induct)


272 
case (t3 a \<Gamma>1 \<tau> \<sigma> t \<Gamma>2) (* lambda case *)


273 
have fc: "a\<sharp>\<Gamma>2" by fact


274 
have ih: "\<And>\<Gamma>3. valid \<Gamma>3 \<longrightarrow> ((a,\<tau>)#\<Gamma>1) \<lless> \<Gamma>3 \<longrightarrow> \<Gamma>3 \<turnstile> t:\<sigma>" by fact

18105

275 
show "valid \<Gamma>2 \<longrightarrow> \<Gamma>1 \<lless> \<Gamma>2 \<longrightarrow> \<Gamma>2 \<turnstile> (Lam [a].t) : \<tau> \<rightarrow> \<sigma>"


276 
proof (intro strip)


277 
assume a1: "\<Gamma>1 \<lless> \<Gamma>2"


278 
and a2: "valid \<Gamma>2"


279 
have "((a,\<tau>)#\<Gamma>1) \<lless> ((a,\<tau>)#\<Gamma>2)" using a1 sub_def by simp


280 
moreover


281 
have "valid ((a,\<tau>)#\<Gamma>2)" using a2 fc by force


282 
ultimately have "((a,\<tau>)#\<Gamma>2) \<turnstile> t:\<sigma>" using ih by force


283 
with fc show "\<Gamma>2 \<turnstile> (Lam [a].t) : \<tau> \<rightarrow> \<sigma>" by force


284 
qed


285 
qed (auto simp add: sub_def) (* lam and var case *)


286 


287 


288 
(* original induction principle is not strong *)


289 
(* enough  so the simple proof fails *)


290 
lemma weakening_too_weak[rule_format]:

18296

291 
assumes "\<Gamma>1 \<turnstile> t:\<sigma>"

18105

292 
shows "valid \<Gamma>2 \<longrightarrow> \<Gamma>1 \<lless> \<Gamma>2 \<longrightarrow> \<Gamma>2 \<turnstile> t:\<sigma>"

18296

293 
using prems


294 
proof (induct, auto)


295 
case (t1 \<Gamma>1 \<tau> a) (* variable case *)

18105

296 
assume "\<Gamma>1 \<lless> \<Gamma>2"


297 
and "valid \<Gamma>2"

18296

298 
and "(a,\<tau>) \<in> (set \<Gamma>1)"

18105

299 
thus "\<Gamma>2 \<turnstile> Var a : \<tau>" by (force simp add: sub_def)


300 
next

18296

301 
case (t3 \<Gamma>1 \<tau> \<sigma> a t) (* lambda case *)

18105

302 
assume a1: "\<Gamma>1 \<lless> \<Gamma>2"


303 
and a2: "valid \<Gamma>2"


304 
and i: "\<forall>\<Gamma>3. valid \<Gamma>3 \<longrightarrow> ((a,\<tau>)#\<Gamma>1) \<lless> \<Gamma>3 \<longrightarrow> \<Gamma>3 \<turnstile> t:\<sigma>"


305 
have "((a,\<tau>)#\<Gamma>1) \<lless> ((a,\<tau>)#\<Gamma>2)" using a1 by (simp add: sub_def)


306 
moreover


307 
have "valid ((a,\<tau>)#\<Gamma>2)" using v2 (* fails *)


308 


309 


310 
