18106

1 


2 
theory sn


3 
imports lam_substs Accessible_Part


4 
begin


5 


6 
(* Strong normalisation according to the P&T book by Girard et al *)


7 


8 
section {* Beta Reduction *}


9 


10 
lemma subst_rename[rule_format]:


11 
fixes c :: "name"


12 
and a :: "name"


13 
and t1 :: "lam"


14 
and t2 :: "lam"


15 
shows "c\<sharp>t1 \<longrightarrow> (t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2])"


16 
apply(nominal_induct t1 rule: lam_induct)


17 
apply(auto simp add: calc_atm fresh_atm fresh_prod abs_fresh)


18 
done


19 


20 
lemma forget[rule_format]:


21 
shows "a\<sharp>t1 \<longrightarrow> t1[a::=t2] = t1"


22 
apply (nominal_induct t1 rule: lam_induct)


23 
apply(auto simp add: abs_fresh fresh_atm fresh_prod)


24 
done


25 


26 
lemma fresh_fact[rule_format]:


27 
fixes b :: "name"


28 
and a :: "name"


29 
and t1 :: "lam"


30 
and t2 :: "lam"


31 
shows "a\<sharp>t1\<longrightarrow>a\<sharp>t2\<longrightarrow>a\<sharp>(t1[b::=t2])"


32 
apply(nominal_induct t1 rule: lam_induct)


33 
apply(auto simp add: abs_fresh fresh_prod fresh_atm)


34 
done


35 


36 
lemma subs_lemma:


37 
fixes x::"name"


38 
and y::"name"


39 
and L::"lam"


40 
and M::"lam"


41 
and N::"lam"


42 
shows "x\<noteq>y\<longrightarrow>x\<sharp>L\<longrightarrow>M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]"


43 
apply(nominal_induct M rule: lam_induct)


44 
apply(auto simp add: fresh_fact forget fresh_prod fresh_atm)


45 
done


46 


47 
lemma id_subs: "t[x::=Var x] = t"


48 
apply(nominal_induct t rule: lam_induct)


49 
apply(simp_all add: fresh_atm)


50 
done


51 


52 
consts


53 
Beta :: "(lam\<times>lam) set"


54 
syntax


55 
"_Beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80)


56 
"_Beta_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80)


57 
translations


58 
"t1 \<longrightarrow>\<^isub>\<beta> t2" \<rightleftharpoons> "(t1,t2) \<in> Beta"


59 
"t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" \<rightleftharpoons> "(t1,t2) \<in> Beta\<^sup>*"


60 
inductive Beta


61 
intros


62 
b1[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)"


63 
b2[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)"


64 
b3[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [(a::name)].s2)"


65 
b4[intro!]: "(App (Lam [(a::name)].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])"


66 


67 
lemma eqvt_beta:


68 
fixes pi :: "name prm"


69 
and t :: "lam"


70 
and s :: "lam"


71 
shows "t\<longrightarrow>\<^isub>\<beta>s \<Longrightarrow> (pi\<bullet>t)\<longrightarrow>\<^isub>\<beta>(pi\<bullet>s)"


72 
apply(erule Beta.induct)


73 
apply(auto)


74 
done


75 


76 
lemma beta_induct_aux[rule_format]:


77 
fixes P :: "lam \<Rightarrow> lam \<Rightarrow>'a::fs_name\<Rightarrow>bool"


78 
and t :: "lam"


79 
and s :: "lam"


80 
assumes a: "t\<longrightarrow>\<^isub>\<beta>s"


81 
and a1: "\<And>x t s1 s2.


82 
s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App s1 t) (App s2 t) x"


83 
and a2: "\<And>x t s1 s2.


84 
s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App t s1) (App t s2) x"


85 
and a3: "\<And>x (a::name) s1 s2.


86 
a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (Lam [a].s1) (Lam [a].s2) x"


87 
and a4: "\<And>x (a::name) t1 s1. a\<sharp>(s1,x) \<Longrightarrow> P (App (Lam [a].t1) s1) (t1[a::=s1]) x"


88 
shows "\<forall>x (pi::name prm). P (pi\<bullet>t) (pi\<bullet>s) x"


89 
using a


90 
proof (induct)


91 
case b1 thus ?case using a1 by (simp, blast intro: eqvt_beta)


92 
next


93 
case b2 thus ?case using a2 by (simp, blast intro: eqvt_beta)


94 
next


95 
case (b3 a s1 s2)


96 
assume j1: "s1 \<longrightarrow>\<^isub>\<beta> s2"


97 
assume j2: "\<forall>x (pi::name prm). P (pi\<bullet>s1) (pi\<bullet>s2) x"


98 
show ?case


99 
proof (simp, intro strip)


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


101 
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"


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


103 
then obtain c::"name"


104 
where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>x" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"


105 
by (force simp add: fresh_prod fresh_atm)


106 
have x: "P (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s2)) x"


107 
using a3 f2 j1 j2 by (simp, blast intro: eqvt_beta)


108 
have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3


109 
by (simp add: lam.inject alpha)


110 
have alpha2: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s2))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s2))" using f1 f3


111 
by (simp add: lam.inject alpha)


112 
show " P (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (Lam [(pi\<bullet>a)].(pi\<bullet>s2)) x"


113 
using x alpha1 alpha2 by (simp only: pt_name2)


114 
qed


115 
next


116 
case (b4 a s1 s2)


117 
show ?case


118 
proof (simp add: subst_eqvt, intro strip)


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


120 
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)"


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


122 
then obtain c::"name"


123 
where f1: "c\<noteq>(pi\<bullet>a)" and f2: "c\<sharp>(pi\<bullet>s2,x)" and f3: "c\<sharp>(pi\<bullet>s1)" and f4: "c\<sharp>(pi\<bullet>s2)"


124 
by (force simp add: fresh_prod fresh_atm)


125 
have x: "P (App (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (pi\<bullet>s2)) ((([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)]) x"


126 
using a4 f2 by (blast intro!: eqvt_beta)


127 
have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3


128 
by (simp add: lam.inject alpha)


129 
have alpha2: "(([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)] = (pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)]"


130 
using f3 by (simp only: subst_rename[symmetric] pt_name2)


131 
show "P (App (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (pi\<bullet>s2)) ((pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)]) x"


132 
using x alpha1 alpha2 by (simp only: pt_name2)


133 
qed


134 
qed


135 


136 
lemma beta_induct[case_names b1 b2 b3 b4]:


137 
fixes P :: "lam \<Rightarrow> lam \<Rightarrow>'a::fs_name\<Rightarrow>bool"


138 
and t :: "lam"


139 
and s :: "lam"


140 
and x :: "'a::fs_name"


141 
assumes a: "t\<longrightarrow>\<^isub>\<beta>s"


142 
and a1: "\<And>x t s1 s2.


143 
s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App s1 t) (App s2 t) x"


144 
and a2: "\<And>x t s1 s2.


145 
s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App t s1) (App t s2) x"


146 
and a3: "\<And>x (a::name) s1 s2.


147 
a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (Lam [a].s1) (Lam [a].s2) x"


148 
and a4: "\<And>x (a::name) t1 s1.


149 
a\<sharp>(s1,x) \<Longrightarrow> P (App (Lam [a].t1) s1) (t1[a::=s1]) x"


150 
shows "P t s x"


151 
using a a1 a2 a3 a4


152 
by (auto intro!: beta_induct_aux[of "t" "s" "P" "[]" "x", simplified])


153 


154 
lemma supp_beta: "t\<longrightarrow>\<^isub>\<beta> s\<Longrightarrow>(supp s)\<subseteq>((supp t)::name set)"


155 
apply(erule Beta.induct)


156 
apply(auto intro!: simp add: abs_supp lam.supp subst_supp)


157 
done


158 
lemma beta_abs: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'\<Longrightarrow>\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''"


159 
apply(ind_cases "Lam [a].t \<longrightarrow>\<^isub>\<beta> t'")


160 
apply(auto simp add: lam.distinct lam.inject)


161 
apply(auto simp add: alpha)


162 
apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI)


163 
apply(rule conjI)


164 
apply(rule sym)


165 
apply(rule pt_bij2[OF pt_name_inst, OF at_name_inst])


166 
apply(simp)


167 
apply(rule pt_name3)


168 
apply(simp add: at_ds5[OF at_name_inst])


169 
apply(rule conjI)


170 
apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] calc_atm)


171 
apply(force dest!: supp_beta simp add: fresh_def)


172 
apply(force intro!: eqvt_beta)


173 
done


174 


175 
lemma beta_subst[rule_format]:


176 
assumes a: "M \<longrightarrow>\<^isub>\<beta> M'"


177 
shows "M[x::=N]\<longrightarrow>\<^isub>\<beta> M'[x::=N]"


178 
using a


179 
apply(nominal_induct M M' rule: beta_induct)


180 
apply(auto simp add: fresh_prod fresh_atm subs_lemma)


181 
done


182 


183 
instance nat :: fs_name


184 
apply(intro_classes)


185 
apply(simp_all add: supp_def perm_nat_def)


186 
done


187 


188 
datatype ty =


189 
TVar "string"


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


191 


192 
primrec


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


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


195 


196 
lemma perm_ty[simp]:


197 
fixes pi ::"name prm"


198 
and \<tau> ::"ty"


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


200 
by (cases \<tau>, simp_all)


201 


202 
lemma fresh_ty:


203 
fixes a ::"name"


204 
and \<tau> ::"ty"


205 
shows "a\<sharp>\<tau>"


206 
by (simp add: fresh_def supp_def)


207 


208 
instance ty :: pt_name


209 
apply(intro_classes)


210 
apply(simp_all)


211 
done


212 


213 
instance ty :: fs_name


214 
apply(intro_classes)


215 
apply(simp add: supp_def)


216 
done


217 


218 
(* valid contexts *)


219 


220 
consts


221 
"dom_ty" :: "(name\<times>ty) list \<Rightarrow> (name list)"


222 
primrec


223 
"dom_ty [] = []"


224 
"dom_ty (x#\<Gamma>) = (fst x)#(dom_ty \<Gamma>)"


225 


226 
consts


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


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


229 
translations


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


231 
inductive ctxts


232 
intros


233 
v1[intro]: "valid []"


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


235 


236 
lemma valid_eqvt:


237 
fixes pi:: "name prm"


238 
assumes a: "valid \<Gamma>"


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


240 
using a


241 
apply(induct)


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


243 
done


244 


245 
(* typing judgements *)


246 


247 
lemma fresh_context[rule_format]:


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


249 
and a :: "name"


250 
shows "a\<sharp>\<Gamma>\<longrightarrow>\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)"


251 
apply(induct_tac \<Gamma>)


252 
apply(auto simp add: fresh_prod fresh_list_cons fresh_atm)


253 
done


254 


255 
lemma valid_elim:


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


257 
and pi:: "name prm"


258 
and a :: "name"


259 
and \<tau> :: "ty"


260 
shows "valid ((a,\<tau>)#\<Gamma>) \<Longrightarrow> valid \<Gamma> \<and> a\<sharp>\<Gamma>"


261 
apply(ind_cases "valid ((a,\<tau>)#\<Gamma>)", simp)


262 
done


263 


264 
lemma valid_unicity[rule_format]:


265 
shows "valid \<Gamma>\<longrightarrow>(c,\<sigma>)\<in>set \<Gamma>\<longrightarrow>(c,\<tau>)\<in>set \<Gamma>\<longrightarrow>\<sigma>=\<tau>"


266 
apply(induct_tac \<Gamma>)


267 
apply(auto dest!: valid_elim fresh_context)


268 
done


269 


270 
consts


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


272 
syntax


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


274 
translations


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


276 


277 
inductive typing


278 
intros


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


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


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


282 


283 
lemma typing_eqvt:


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


285 
and t :: "lam"


286 
and \<tau> :: "ty"


287 
and pi:: "name prm"


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


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


290 
using a


291 
proof (induct)


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


293 
have "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt)


294 
moreover


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


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


297 
using typing.intros by (auto simp add: pt_list_set_pi[OF pt_name_inst])


298 
next


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


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


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


302 
using typing.intros by (force)


303 
qed (auto)


304 


305 
lemma typing_induct_aux[rule_format]:


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


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


308 
and t :: "lam"


309 
and \<tau> :: "ty"


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


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


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


313 
\<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)


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


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


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


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


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


319 
using a


320 
proof (induct)


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


322 
assume j1: "valid \<Gamma>"


323 
assume j2: "(a,\<tau>)\<in>set \<Gamma>"


324 
show ?case


325 
proof (intro strip, simp)


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


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


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


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


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


331 
qed


332 
next


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


334 
thus ?case using a2 by (simp, blast intro: typing_eqvt)


335 
next


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


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


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


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


340 
show ?case


341 
proof (intro strip, simp)


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


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


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


345 
then obtain c::"name"


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


347 
by (force simp add: fresh_prod fresh_atm)


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


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


350 
pt_rev_pi[OF pt_name_inst, OF at_name_inst])


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


352 
by (simp only: pt_name2, rule pt_fresh_fresh[OF pt_name_inst, OF at_name_inst])


353 
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


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


355 
by (force simp add: pt_name2 calc_atm split: if_splits)


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


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


358 
by (force simp add: pt_name2 calc_atm split: if_splits)


359 
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


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


361 
by (simp add: lam.inject alpha)


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


363 
by (simp only: pt_name2)


364 
qed


365 
qed


366 


367 
lemma typing_induct[case_names t1 t2 t3]:


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


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


370 
and t :: "lam"


371 
and \<tau> :: "ty"


372 
and x :: "'a::fs_name"


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


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


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


376 
\<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)


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


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


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


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


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


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


383 


384 
constdefs


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


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


387 


388 
lemma weakening[rule_format]:


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


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


391 
using a


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


393 
apply(auto simp add: sub_def)


394 
done


395 


396 
lemma in_ctxt[rule_format]: "(a,\<tau>)\<in>set \<Gamma> \<longrightarrow> (a\<in>set(dom_ty \<Gamma>))"


397 
apply(induct_tac \<Gamma>)


398 
apply(auto)


399 
done


400 


401 
lemma free_vars:


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


403 
shows " (supp t)\<subseteq>set(dom_ty \<Gamma>)"


404 
using a


405 
apply(nominal_induct \<Gamma> t \<tau> rule: typing_induct)


406 
apply(auto simp add: lam.supp abs_supp supp_atm in_ctxt)


407 
done


408 


409 
lemma t1_elim: "\<Gamma> \<turnstile> Var a : \<tau> \<Longrightarrow> valid \<Gamma> \<and> (a,\<tau>) \<in> set \<Gamma>"


410 
apply(ind_cases "\<Gamma> \<turnstile> Var a : \<tau>")


411 
apply(auto simp add: lam.inject lam.distinct)


412 
done


413 


414 
lemma t2_elim: "\<Gamma> \<turnstile> App t1 t2 : \<sigma> \<Longrightarrow> \<exists>\<tau>. (\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<and> \<Gamma> \<turnstile> t2 : \<tau>)"


415 
apply(ind_cases "\<Gamma> \<turnstile> App t1 t2 : \<sigma>")


416 
apply(auto simp add: lam.inject lam.distinct)


417 
done


418 


419 
lemma t3_elim: "\<lbrakk>\<Gamma> \<turnstile> Lam [a].t : \<sigma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> \<exists>\<tau> \<tau>'. \<sigma>=\<tau>\<rightarrow>\<tau>' \<and> ((a,\<tau>)#\<Gamma>) \<turnstile> t : \<tau>'"


420 
apply(ind_cases "\<Gamma> \<turnstile> Lam [a].t : \<sigma>")


421 
apply(auto simp add: lam.distinct lam.inject alpha)


422 
apply(drule_tac pi="[(a,aa)]::name prm" in typing_eqvt)


423 
apply(simp)


424 
apply(subgoal_tac "([(a,aa)]::name prm)\<bullet>\<Gamma> = \<Gamma>")(*A*)


425 
apply(force simp add: calc_atm)


426 
(*A*)


427 
apply(force intro!: pt_fresh_fresh[OF pt_name_inst, OF at_name_inst])


428 
done


429 


430 
lemma typing_valid:


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


432 
shows "valid \<Gamma>"


433 
using a by (induct, auto dest!: valid_elim)


434 


435 
lemma ty_subs[rule_format]:


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


437 
and t1 ::"lam"


438 
and t2 ::"lam"


439 
and \<tau> ::"ty"


440 
and \<sigma> ::"ty"


441 
and c ::"name"


442 
shows "((c,\<sigma>)#\<Gamma>) \<turnstile> t1:\<tau>\<longrightarrow> \<Gamma>\<turnstile> t2:\<sigma>\<longrightarrow> \<Gamma> \<turnstile> t1[c::=t2]:\<tau>"


443 
proof(nominal_induct t1 rule: lam_induct)


444 
case (Var \<Gamma> \<sigma> \<tau> c t2 a)


445 
show ?case


446 
proof(intro strip)


447 
assume a1: "\<Gamma> \<turnstile>t2:\<sigma>"


448 
assume a2: "((c,\<sigma>)#\<Gamma>) \<turnstile> Var a:\<tau>"


449 
hence a21: "(a,\<tau>)\<in>set((c,\<sigma>)#\<Gamma>)" and a22: "valid((c,\<sigma>)#\<Gamma>)" by (auto dest: t1_elim)


450 
from a22 have a23: "valid \<Gamma>" and a24: "c\<sharp>\<Gamma>" by (auto dest: valid_elim)


451 
from a24 have a25: "\<not>(\<exists>\<tau>. (c,\<tau>)\<in>set \<Gamma>)" by (rule fresh_context)


452 
show "\<Gamma>\<turnstile>(Var a)[c::=t2] : \<tau>"


453 
proof (cases "a=c", simp_all)


454 
assume case1: "a=c"


455 
show "\<Gamma> \<turnstile> t2:\<tau>" using a1


456 
proof (cases "\<sigma>=\<tau>")


457 
assume "\<sigma>=\<tau>" thus ?thesis using a1 by simp


458 
next


459 
assume a3: "\<sigma>\<noteq>\<tau>"


460 
show ?thesis


461 
proof (rule ccontr)


462 
from a3 a21 have "(a,\<tau>)\<in>set \<Gamma>" by force


463 
with case1 a25 show False by force


464 
qed


465 
qed


466 
next


467 
assume case2: "a\<noteq>c"


468 
with a21 have a26: "(a,\<tau>)\<in>set \<Gamma>" by force


469 
from a23 a26 show "\<Gamma> \<turnstile> Var a:\<tau>" by force


470 
qed


471 
qed


472 
next


473 
case (App \<Gamma> \<sigma> \<tau> c t2 s1 s2)


474 
show ?case


475 
proof (intro strip, simp)


476 
assume b1: "\<Gamma> \<turnstile>t2:\<sigma>"


477 
assume b2: " ((c,\<sigma>)#\<Gamma>)\<turnstile>App s1 s2 : \<tau>"


478 
hence "\<exists>\<tau>'. (((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau> \<and> ((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>')" by (rule t2_elim)


479 
then obtain \<tau>' where b3a: "((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau>" and b3b: "((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>'" by force


480 
show "\<Gamma> \<turnstile> App (s1[c::=t2]) (s2[c::=t2]) : \<tau>"


481 
using b1 b3a b3b App by (rule_tac \<tau>="\<tau>'" in t2, auto)


482 
qed


483 
next


484 
case (Lam \<Gamma> \<sigma> \<tau> c t2 a s)


485 
assume "a\<sharp>(\<Gamma>,\<sigma>,\<tau>,c,t2)"


486 
hence f1: "a\<sharp>\<Gamma>" and f2: "a\<noteq>c" and f2': "c\<sharp>a" and f3: "a\<sharp>t2" and f4: "a\<sharp>((c,\<sigma>)#\<Gamma>)"


487 
by (auto simp add: fresh_atm fresh_prod fresh_list_cons)


488 
show ?case using f2 f3


489 
proof(intro strip, simp)


490 
assume c1: "((c,\<sigma>)#\<Gamma>)\<turnstile>Lam [a].s : \<tau>"


491 
hence "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<turnstile> s : \<tau>2" using f4 by (auto dest: t3_elim)


492 
then obtain \<tau>1 \<tau>2 where c11: "\<tau>=\<tau>1\<rightarrow>\<tau>2" and c12: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<turnstile> s : \<tau>2" by force


493 
from c12 have "valid ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>)" by (rule typing_valid)


494 
hence ca: "valid \<Gamma>" and cb: "a\<sharp>\<Gamma>" and cc: "c\<sharp>\<Gamma>"


495 
by (auto dest: valid_elim simp add: fresh_list_cons)


496 
from c12 have c14: "((c,\<sigma>)#(a,\<tau>1)#\<Gamma>) \<turnstile> s : \<tau>2"


497 
proof 


498 
have c2: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<lless> ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)


499 
have c3: "valid ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)"


500 
by (rule v2, rule v2, auto simp add: fresh_list_cons fresh_prod ca cb cc f2' fresh_ty)


501 
from c12 c2 c3 show ?thesis by (force intro: weakening)


502 
qed


503 
assume c8: "\<Gamma> \<turnstile> t2 : \<sigma>"


504 
have c81: "((a,\<tau>1)#\<Gamma>)\<turnstile>t2 :\<sigma>"


505 
proof 


506 
have c82: "\<Gamma> \<lless> ((a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def)


507 
have c83: "valid ((a,\<tau>1)#\<Gamma>)" using f1 ca by force


508 
with c8 c82 c83 show ?thesis by (force intro: weakening)


509 
qed


510 
show "\<Gamma> \<turnstile> Lam [a].(s[c::=t2]) : \<tau>"


511 
using c11 Lam c14 c81 f1 by force


512 
qed


513 
qed


514 


515 
lemma subject[rule_format]:


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


517 
and t1 ::"lam"


518 
and t2 ::"lam"


519 
and \<tau> ::"ty"


520 
assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"


521 
shows "(\<Gamma> \<turnstile> t1:\<tau>) \<longrightarrow> (\<Gamma> \<turnstile> t2:\<tau>)"


522 
using a


523 
proof (nominal_induct t1 t2 rule: beta_induct, auto)


524 
case (b1 \<Gamma> \<tau> t s1 s2)


525 
assume i: "\<forall>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>"


526 
assume "\<Gamma> \<turnstile> App s1 t : \<tau>"


527 
hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> t : \<sigma>)" by (rule t2_elim)


528 
then obtain \<sigma> where a1: "\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> t : \<sigma>" by force


529 
thus "\<Gamma> \<turnstile> App s2 t : \<tau>" using i by force


530 
next


531 
case (b2 \<Gamma> \<tau> t s1 s2)


532 
assume i: "\<forall>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>"


533 
assume "\<Gamma> \<turnstile> App t s1 : \<tau>"


534 
hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s1 : \<sigma>)" by (rule t2_elim)


535 
then obtain \<sigma> where a1: "\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s1 : \<sigma>" by force


536 
thus "\<Gamma> \<turnstile> App t s2 : \<tau>" using i by force


537 
next


538 
case (b3 \<Gamma> \<tau> a s1 s2)


539 
assume "a\<sharp>(\<Gamma>,\<tau>)"


540 
hence f: "a\<sharp>\<Gamma>" by (simp add: fresh_prod)


541 
assume i: "\<forall>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>"


542 
assume "\<Gamma> \<turnstile> Lam [a].s1 : \<tau>"


543 
with f have "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#\<Gamma>) \<turnstile> s1 : \<tau>2" by (force dest: t3_elim)


544 
then obtain \<tau>1 \<tau>2 where a1: "\<tau>=\<tau>1\<rightarrow>\<tau>2" and a2: "((a,\<tau>1)#\<Gamma>) \<turnstile> s1 : \<tau>2" by force


545 
thus "\<Gamma> \<turnstile> Lam [a].s2 : \<tau>" using f i by force


546 
next


547 
case (b4 \<Gamma> \<tau> a s1 s2)


548 
have "a\<sharp>(s2,\<Gamma>,\<tau>)" by fact


549 
hence f: "a\<sharp>\<Gamma>" by (simp add: fresh_prod)


550 
assume "\<Gamma> \<turnstile> App (Lam [a].s1) s2 : \<tau>"


551 
hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> (Lam [a].s1) : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s2 : \<sigma>)" by (rule t2_elim)


552 
then obtain \<sigma> where a1: "\<Gamma> \<turnstile> (Lam [(a::name)].s1) : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s2 : \<sigma>" by force


553 
have "((a,\<sigma>)#\<Gamma>) \<turnstile> s1 : \<tau>" using a1 f by (auto dest!: t3_elim)


554 
with a2 show "\<Gamma> \<turnstile> s1[a::=s2] : \<tau>" by (force intro: ty_subs)


555 
qed


556 


557 


558 
lemma subject[rule_format]:


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


560 
and t1 ::"lam"


561 
and t2 ::"lam"


562 
and \<tau> ::"ty"


563 
assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2"


564 
shows "\<Gamma> \<turnstile> t1:\<tau> \<longrightarrow> \<Gamma> \<turnstile> t2:\<tau>"


565 
using a


566 
apply(nominal_induct t1 t2 rule: beta_induct)


567 
apply(auto dest!: t2_elim t3_elim intro: ty_subs simp add: fresh_prod)


568 
done


569 


570 


571 


572 
subsection {* some facts about beta *}


573 


574 
constdefs


575 
"NORMAL" :: "lam \<Rightarrow> bool"


576 
"NORMAL t \<equiv> \<not>(\<exists>t'. t\<longrightarrow>\<^isub>\<beta> t')"


577 


578 
constdefs


579 
"SN" :: "lam \<Rightarrow> bool"


580 
"SN t \<equiv> t\<in>termi Beta"


581 


582 
lemma qq1: "\<lbrakk>SN(t1);t1\<longrightarrow>\<^isub>\<beta> t2\<rbrakk>\<Longrightarrow>SN(t2)"


583 
apply(simp add: SN_def)


584 
apply(drule_tac a="t2" in acc_downward)


585 
apply(auto)


586 
done


587 


588 
lemma qq2: "(\<forall>t2. t1\<longrightarrow>\<^isub>\<beta>t2 \<longrightarrow> SN(t2))\<Longrightarrow>SN(t1)"


589 
apply(simp add: SN_def)


590 
apply(rule accI)


591 
apply(auto)


592 
done


593 


594 


595 
section {* Candidates *}


596 


597 
consts


598 
RED :: "ty \<Rightarrow> lam set"


599 
primrec


600 
"RED (TVar X) = {t. SN(t)}"


601 
"RED (\<tau>\<rightarrow>\<sigma>) = {t. \<forall>u. (u\<in>RED \<tau> \<longrightarrow> (App t u)\<in>RED \<sigma>)}"


602 


603 
constdefs


604 
NEUT :: "lam \<Rightarrow> bool"


605 
"NEUT t \<equiv> (\<exists>a. t=Var a)\<or>(\<exists>t1 t2. t=App t1 t2)"


606 


607 
(* a slight hack to get the first element of applications *)


608 
consts


609 
FST :: "(lam\<times>lam) set"


610 
syntax


611 
"FST_judge" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<guillemotright> _" [80,80] 80)


612 
translations


613 
"t1 \<guillemotright> t2" \<rightleftharpoons> "(t1,t2) \<in> FST"


614 
inductive FST


615 
intros


616 
fst[intro!]: "(App t s) \<guillemotright> t"


617 


618 
lemma fst_elim[elim!]: "(App t s) \<guillemotright> t' \<Longrightarrow> t=t'"


619 
apply(ind_cases "App t s \<guillemotright> t'")


620 
apply(simp add: lam.inject)


621 
done


622 


623 
lemma qq3: "SN(App t s)\<Longrightarrow>SN(t)"


624 
apply(simp add: SN_def)


625 
apply(subgoal_tac "\<forall>z. (App t s \<guillemotright> z) \<longrightarrow> z\<in>termi Beta")(*A*)


626 
apply(force)


627 
(*A*)


628 
apply(erule acc_induct)


629 
apply(clarify)


630 
apply(ind_cases "x \<guillemotright> z")


631 
apply(clarify)


632 
apply(rule accI)


633 
apply(auto intro: b1)


634 
done


635 


636 
constdefs


637 
"CR1" :: "ty \<Rightarrow> bool"


638 
"CR1 \<tau> \<equiv> \<forall> t. (t\<in>RED \<tau> \<longrightarrow> SN(t))"


639 


640 
"CR2" :: "ty \<Rightarrow> bool"


641 
"CR2 \<tau> \<equiv> \<forall>t t'. ((t\<in>RED \<tau> \<and> t \<longrightarrow>\<^isub>\<beta> t') \<longrightarrow> t'\<in>RED \<tau>)"


642 


643 
"CR3_RED" :: "lam \<Rightarrow> ty \<Rightarrow> bool"


644 
"CR3_RED t \<tau> \<equiv> \<forall>t'. (t\<longrightarrow>\<^isub>\<beta> t' \<longrightarrow> t'\<in>RED \<tau>)"


645 


646 
"CR3" :: "ty \<Rightarrow> bool"


647 
"CR3 \<tau> \<equiv> \<forall>t. (NEUT t \<and> CR3_RED t \<tau>) \<longrightarrow> t\<in>RED \<tau>"


648 


649 
"CR4" :: "ty \<Rightarrow> bool"


650 
"CR4 \<tau> \<equiv> \<forall>t. (NEUT t \<and> NORMAL t) \<longrightarrow>t\<in>RED \<tau>"


651 


652 
lemma CR3_CR4: "CR3 \<tau> \<Longrightarrow> CR4 \<tau>"


653 
apply(simp (no_asm_use) add: CR3_def CR3_RED_def CR4_def NORMAL_def)


654 
apply(blast)


655 
done


656 


657 
lemma sub_ind:


658 
"SN(u)\<Longrightarrow>(u\<in>RED \<tau>\<longrightarrow>(\<forall>t. (NEUT t\<and>CR2 \<tau>\<and>CR3 \<sigma>\<and>CR3_RED t (\<tau>\<rightarrow>\<sigma>))\<longrightarrow>(App t u)\<in>RED \<sigma>))"


659 
apply(simp add: SN_def)


660 
apply(erule acc_induct)


661 
apply(auto)


662 
apply(simp add: CR3_def)


663 
apply(rotate_tac 5)


664 
apply(drule_tac x="App t x" in spec)


665 
apply(drule mp)


666 
apply(rule conjI)


667 
apply(force simp only: NEUT_def)


668 
apply(simp (no_asm) add: CR3_RED_def)


669 
apply(clarify)


670 
apply(ind_cases "App t x \<longrightarrow>\<^isub>\<beta> t'")


671 
apply(simp_all add: lam.inject)


672 
apply(simp only: CR3_RED_def)


673 
apply(drule_tac x="s2" in spec)


674 
apply(simp)


675 
apply(drule_tac x="s2" in spec)


676 
apply(simp)


677 
apply(drule mp)


678 
apply(simp (no_asm_use) add: CR2_def)


679 
apply(blast)


680 
apply(drule_tac x="ta" in spec)


681 
apply(force)


682 
apply(auto simp only: NEUT_def lam.inject lam.distinct)


683 
done


684 


685 
lemma RED_props: "CR1 \<tau> \<and> CR2 \<tau> \<and> CR3 \<tau>"


686 
apply(induct_tac \<tau>)


687 
apply(auto)


688 
(* atom types *)


689 
(* C1 *)


690 
apply(simp add: CR1_def)


691 
(* C2 *)


692 
apply(simp add: CR2_def)


693 
apply(clarify)


694 
apply(drule_tac ?t2.0="t'" in qq1)


695 
apply(assumption)+


696 
(* C3 *)


697 
apply(simp add: CR3_def CR3_RED_def)


698 
apply(clarify)


699 
apply(rule qq2)


700 
apply(assumption)


701 
(* arrow types *)


702 
(* C1 *)


703 
apply(simp (no_asm) add: CR1_def)


704 
apply(clarify)


705 
apply(subgoal_tac "NEUT (Var a)")(*A*)


706 
apply(subgoal_tac "(Var a)\<in>RED ty1")(*C*)


707 
apply(drule_tac x="Var a" in spec)


708 
apply(simp)


709 
apply(simp add: CR1_def)


710 
apply(rotate_tac 1)


711 
apply(drule_tac x="App t (Var a)" in spec)


712 
apply(simp)


713 
apply(drule qq3)


714 
apply(assumption)


715 
(*C*)


716 
apply(simp (no_asm_use) add: CR3_def CR3_RED_def)


717 
apply(drule_tac x="Var a" in spec)


718 
apply(drule mp)


719 
apply(clarify)


720 
apply(ind_cases " Var a \<longrightarrow>\<^isub>\<beta> t'")


721 
apply(simp (no_asm_use) add: lam.distinct)+


722 
(*A*)


723 
apply(simp (no_asm) only: NEUT_def)


724 
apply(rule disjCI)


725 
apply(rule_tac x="a" in exI)


726 
apply(simp (no_asm))


727 
(* C2 *)


728 
apply(simp (no_asm) add: CR2_def)


729 
apply(clarify)


730 
apply(drule_tac x="u" in spec)


731 
apply(simp)


732 
apply(subgoal_tac "App t u \<longrightarrow>\<^isub>\<beta> App t' u")(*X*)


733 
apply(simp (no_asm_use) only: CR2_def)


734 
apply(blast)


735 
(*X*)


736 
apply(force intro!: b1)


737 
(* C3 *)


738 
apply(unfold CR3_def)


739 
apply(rule allI)


740 
apply(rule impI)


741 
apply(erule conjE)


742 
apply(simp (no_asm))


743 
apply(rule allI)


744 
apply(rule impI)


745 
apply(subgoal_tac "SN(u)")(*Z*)


746 
apply(fold CR3_def)


747 
apply(drule_tac \<tau>="ty1" and \<sigma>="ty2" in sub_ind)


748 
apply(simp)


749 
(*Z*)


750 
apply(simp add: CR1_def)


751 
done


752 


753 
lemma double_acc_aux:


754 
assumes a_acc: "a \<in> acc r"


755 
and b_acc: "b \<in> acc r"


756 
and hyp: "\<And>x z.


757 
(\<And>y. (y, x) \<in> r \<Longrightarrow> y \<in> acc r) \<Longrightarrow>


758 
(\<And>y. (y, x) \<in> r \<Longrightarrow> P y z) \<Longrightarrow>


759 
(\<And>u. (u, z) \<in> r \<Longrightarrow> u \<in> acc r) \<Longrightarrow>


760 
(\<And>u. (u, z) \<in> r \<Longrightarrow> P x u) \<Longrightarrow> P x z"


761 
shows "P a b"


762 
proof 


763 
from a_acc


764 
have r: "\<And>b. b \<in> acc r \<Longrightarrow> P a b"


765 
proof (induct a rule: acc.induct)


766 
case (accI x)


767 
note accI' = accI


768 
have "b \<in> acc r" .


769 
thus ?case


770 
proof (induct b rule: acc.induct)


771 
case (accI y)


772 
show ?case


773 
apply (rule hyp)


774 
apply (erule accI')


775 
apply (erule accI')


776 
apply (rule acc.accI)


777 
apply (erule accI)


778 
apply (erule accI)


779 
apply (erule accI)


780 
done


781 
qed


782 
qed


783 
from b_acc show ?thesis by (rule r)


784 
qed


785 


786 
lemma double_acc:


787 
"\<lbrakk>a \<in> acc r; b \<in> acc r; \<forall>x z. ((\<forall>y. (y, x)\<in>r\<longrightarrow>P y z)\<and>(\<forall>u. (u, z)\<in>r\<longrightarrow>P x u))\<longrightarrow>P x z\<rbrakk>\<Longrightarrow>P a b"


788 
apply(rule_tac r="r" in double_acc_aux)


789 
apply(assumption)+


790 
apply(blast)


791 
done


792 


793 
lemma abs_RED[rule_format]: "(\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>)\<longrightarrow>Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)"


794 
apply(simp)


795 
apply(clarify)


796 
apply(subgoal_tac "t\<in>termi Beta")(*1*)


797 
apply(erule rev_mp)


798 
apply(subgoal_tac "u \<in> RED \<tau>")(*A*)


799 
apply(erule rev_mp)


800 
apply(rule_tac a="t" and b="u" in double_acc)


801 
apply(assumption)


802 
apply(subgoal_tac "CR1 \<tau>")(*A*)


803 
apply(simp add: CR1_def SN_def)


804 
(*A*)


805 
apply(force simp add: RED_props)


806 
apply(simp)


807 
apply(clarify)


808 
apply(subgoal_tac "CR3 \<sigma>")(*B*)


809 
apply(simp add: CR3_def)


810 
apply(rotate_tac 6)


811 
apply(drule_tac x="App(Lam[x].xa ) z" in spec)


812 
apply(drule mp)


813 
apply(rule conjI)


814 
apply(force simp add: NEUT_def)


815 
apply(simp add: CR3_RED_def)


816 
apply(clarify)


817 
apply(ind_cases "App(Lam[x].xa) z \<longrightarrow>\<^isub>\<beta> t'")


818 
apply(auto simp add: lam.inject lam.distinct)


819 
apply(drule beta_abs)


820 
apply(auto)


821 
apply(drule_tac x="t''" in spec)


822 
apply(simp)


823 
apply(drule mp)


824 
apply(clarify)


825 
apply(drule_tac x="s" in bspec)


826 
apply(assumption)


827 
apply(subgoal_tac "xa [ x ::= s ] \<longrightarrow>\<^isub>\<beta> t'' [ x ::= s ]")(*B*)


828 
apply(subgoal_tac "CR2 \<sigma>")(*C*)


829 
apply(simp (no_asm_use) add: CR2_def)


830 
apply(blast)


831 
(*C*)


832 
apply(force simp add: RED_props)


833 
(*B*)


834 
apply(force intro!: beta_subst)


835 
apply(assumption)


836 
apply(rotate_tac 3)


837 
apply(drule_tac x="s2" in spec)


838 
apply(subgoal_tac "s2\<in>RED \<tau>")(*D*)


839 
apply(simp)


840 
(*D*)


841 
apply(subgoal_tac "CR2 \<tau>")(*E*)


842 
apply(simp (no_asm_use) add: CR2_def)


843 
apply(blast)


844 
(*E*)


845 
apply(force simp add: RED_props)


846 
apply(simp add: alpha)


847 
apply(erule disjE)


848 
apply(force)


849 
apply(auto)


850 
apply(simp add: subst_rename)


851 
apply(drule_tac x="z" in bspec)


852 
apply(assumption)


853 
(*B*)


854 
apply(force simp add: RED_props)


855 
(*1*)


856 
apply(drule_tac x="Var x" in bspec)


857 
apply(subgoal_tac "CR3 \<tau>")(*2*)


858 
apply(drule CR3_CR4)


859 
apply(simp add: CR4_def)


860 
apply(drule_tac x="Var x" in spec)


861 
apply(drule mp)


862 
apply(rule conjI)


863 
apply(force simp add: NEUT_def)


864 
apply(simp add: NORMAL_def)


865 
apply(clarify)


866 
apply(ind_cases "Var x \<longrightarrow>\<^isub>\<beta> t'")


867 
apply(auto simp add: lam.inject lam.distinct)


868 
apply(force simp add: RED_props)


869 
apply(simp add: id_subs)


870 
apply(subgoal_tac "CR1 \<sigma>")(*3*)


871 
apply(simp add: CR1_def SN_def)


872 
(*3*)


873 
apply(force simp add: RED_props)


874 
done


875 


876 
lemma all_RED:


877 
"((\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>)\<longrightarrow>(a\<in>set(dom_sss \<theta>)\<and>\<theta><a>\<in>RED \<sigma>))\<and>\<Gamma>\<turnstile>t:\<tau>) \<longrightarrow> (t[<\<theta>>]\<in>RED \<tau>)"


878 
apply(nominal_induct t rule: lam_induct)


879 
(* Variables *)


880 
apply(force dest: t1_elim)


881 
(* Applications *)


882 
apply(auto dest!: t2_elim)


883 
apply(drule_tac x="a" in spec)


884 
apply(drule_tac x="a" in spec)


885 
apply(drule_tac x="\<tau>\<rightarrow>aa" in spec)


886 
apply(drule_tac x="\<tau>" in spec)


887 
apply(drule_tac x="b" in spec)


888 
apply(drule_tac x="b" in spec)


889 
apply(force)


890 
(* Abstractions *)


891 
apply(drule t3_elim)


892 
apply(simp add: fresh_prod)


893 
apply(auto)


894 
apply(drule_tac x="((ab,\<tau>)#a)" in spec)


895 
apply(drule_tac x="\<tau>'" in spec)


896 
apply(drule_tac x="b" in spec)


897 
apply(simp)


898 
(* HERE *)


899 


900 


901 
done


902 
