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]:


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


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


101 
and t :: "lam"


102 
and \<tau> :: "ty"


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


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


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


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


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


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


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


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


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


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


113 


114 
lemma typing_induct_aux[rule_format]:


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


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


117 
and t :: "lam"


118 
and \<tau> :: "ty"


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


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


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


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


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


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


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


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


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


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])


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


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


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


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])


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


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


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)


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


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)


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


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


173 
qed


174 
qed


175 


176 
lemma typing_induct[case_names t1 t2 t3]:


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


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>"


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


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


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


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


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


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


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


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


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


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]:


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


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


203 
using a


204 
apply(nominal_induct \<Gamma>1 t \<sigma> rule: typing_induct)


205 
apply(auto simp add: sub_def)


206 
done


207 


208 
lemma weakening_version2[rule_format]:


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


210 
and t ::"lam"


211 
and \<tau> ::"ty"


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


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


214 
using a


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


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


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


218 
and "valid \<Gamma>2"


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


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


221 
next


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


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


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


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


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


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


228 
moreover


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


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


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


232 
qed


233 


234 
lemma weakening_version3[rule_format]:


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


236 
and t ::"lam"


237 
and \<tau> ::"ty"


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


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


240 
using a


241 
proof (nominal_induct \<Gamma>1 t \<sigma> rule: typing_induct)


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


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


244 
next


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


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


247 
next


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


249 
have a3: "a\<sharp>\<Gamma>2"


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


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


252 
proof (intro strip)


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


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


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


256 
moreover


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


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


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


260 
qed


261 
qed


262 


263 
lemma weakening_version4[rule_format]:


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


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


266 
using a


267 
proof (nominal_induct \<Gamma>1 t \<sigma> rule: typing_induct)


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


269 
have fc: "a\<sharp>\<Gamma>2"


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


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


272 
proof (intro strip)


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


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


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


276 
moreover


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


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


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


280 
qed


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


282 


283 


284 
(* original induction principle is not strong *)


285 
(* enough  so the simple proof fails *)


286 
lemma weakening_too_weak[rule_format]:


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


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


289 
using a


290 
proof (nominal_induct \<Gamma>1 t \<sigma> rule: typing_induct_weak, auto)


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


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


293 
and "valid \<Gamma>2"


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


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


296 
next


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


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


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


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


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


302 
moreover


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


304 


305 


306 
