author  urbanc 
Sun, 04 Dec 2005 12:40:39 +0100  
changeset 18348  b5d7649f8aca 
parent 18345  d37fb71754fe 
child 18378  35fba71ec6ef 
permissions  rwrr 
18263
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset

1 
(* $Id$ *) 
18106  2 

3 
theory sn 

4 
imports lam_substs Accessible_Part 

5 
begin 

6 

18269  7 
text {* Strong Normalisation proof from the Proofs and Types book *} 
18106  8 

9 
section {* Beta Reduction *} 

10 

18313  11 

18106  12 
lemma subst_rename[rule_format]: 
13 
shows "c\<sharp>t1 \<longrightarrow> (t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2])" 

18313  14 
apply(nominal_induct t1 avoiding: a c t2 rule: lam_induct) 
15 
apply(auto simp add: calc_atm fresh_atm abs_fresh) 

18106  16 
done 
17 

18313  18 
lemma forget: 
19 
assumes a: "a\<sharp>t1" 

20 
shows "t1[a::=t2] = t1" 

21 
using a 

22 
apply (nominal_induct t1 avoiding: a t2 rule: lam_induct) 

23 
apply(auto simp add: abs_fresh fresh_atm) 

18106  24 
done 
25 

18313  26 
lemma fresh_fact: 
27 
fixes a::"name" 

28 
assumes a: "a\<sharp>t1" 

29 
and b: "a\<sharp>t2" 

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

31 
using a b 

32 
apply(nominal_induct t1 avoiding: a b t2 rule: lam_induct) 

33 
apply(auto simp add: abs_fresh fresh_atm) 

18106  34 
done 
35 

36 
lemma subs_lemma: 

18313  37 
assumes a: "x\<noteq>y" 
38 
and b: "x\<sharp>L" 

39 
shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" 

40 
using a b 

41 
by (nominal_induct M avoiding: x y N L rule: lam_induct) 

42 
(auto simp add: fresh_fact forget) 

18106  43 

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

18313  45 
apply(nominal_induct t avoiding: x rule: lam_induct) 
18106  46 
apply(simp_all add: fresh_atm) 
47 
done 

48 

49 
consts 

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

51 
syntax 

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

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

54 
translations 

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

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

57 
inductive Beta 

58 
intros 

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

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

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

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

63 

64 
lemma eqvt_beta: 

65 
fixes pi :: "name prm" 

66 
and t :: "lam" 

67 
and s :: "lam" 

18313  68 
assumes a: "t\<longrightarrow>\<^isub>\<beta>s" 
69 
shows "(pi\<bullet>t)\<longrightarrow>\<^isub>\<beta>(pi\<bullet>s)" 

70 
using a by (induct, auto) 

18106  71 

18313  72 
lemma beta_induct[consumes 1, case_names b1 b2 b3 b4]: 
73 
fixes P :: "'a::fs_name\<Rightarrow>lam \<Rightarrow> lam \<Rightarrow>bool" 

18106  74 
and t :: "lam" 
75 
and s :: "lam" 

76 
and x :: "'a::fs_name" 

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

18313  78 
and a1: "\<And>t s1 s2 x. s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (App s1 t) (App s2 t)" 
79 
and a2: "\<And>t s1 s2 x. s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (App t s1) (App t s2)" 

80 
and a3: "\<And>a s1 s2 x. a\<sharp>x \<Longrightarrow> s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<And>z. P z s1 s2) \<Longrightarrow> P x (Lam [a].s1) (Lam [a].s2)" 

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

82 
shows "P x t s" 

83 
proof  

84 
from a have "\<And>(pi::name prm) x. P x (pi\<bullet>t) (pi\<bullet>s)" 

85 
proof (induct) 

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

87 
next 

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

89 
next 

90 
case (b3 a s1 s2) 

91 
have j1: "s1 \<longrightarrow>\<^isub>\<beta> s2" by fact 

92 
have j2: "\<And>x (pi::name prm). P x (pi\<bullet>s1) (pi\<bullet>s2)" by fact 

93 
show ?case 

94 
proof (simp) 

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

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

97 
then obtain c::"name" 

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

99 
by (force simp add: fresh_prod fresh_atm) 

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

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

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

103 
by (simp add: lam.inject alpha) 

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

105 
by (simp add: lam.inject alpha) 

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

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

108 
qed 

109 
next 

110 
case (b4 a s1 s2) 

111 
show ?case 

112 
proof (simp add: subst_eqvt) 

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

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

115 
then obtain c::"name" 

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

117 
by (force simp add: fresh_prod fresh_atm) 

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

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

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

121 
by (simp add: lam.inject alpha) 

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

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

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

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

126 
qed 

127 
qed 

128 
hence "P x (([]::name prm)\<bullet>t) (([]::name prm)\<bullet>s)" by blast 

129 
thus ?thesis by simp 

130 
qed 

18106  131 

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

133 
apply(erule Beta.induct) 

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

135 
done 

18313  136 

18106  137 
lemma beta_abs: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'\<Longrightarrow>\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''" 
138 
apply(ind_cases "Lam [a].t \<longrightarrow>\<^isub>\<beta> t'") 

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

140 
apply(auto simp add: alpha) 

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

142 
apply(rule conjI) 

143 
apply(rule sym) 

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

145 
apply(simp) 

146 
apply(rule pt_name3) 

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

148 
apply(rule conjI) 

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

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

151 
apply(force intro!: eqvt_beta) 

152 
done 

153 

18313  154 
lemma beta_subst: 
18106  155 
assumes a: "M \<longrightarrow>\<^isub>\<beta> M'" 
156 
shows "M[x::=N]\<longrightarrow>\<^isub>\<beta> M'[x::=N]" 

157 
using a 

18313  158 
apply(nominal_induct M M' avoiding: x N rule: beta_induct) 
159 
apply(auto simp add: fresh_atm subs_lemma) 

18106  160 
done 
161 

162 
datatype ty = 

163 
TVar "string" 

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

165 

166 
primrec 

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

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

169 

170 
lemma perm_ty[simp]: 

171 
fixes pi ::"name prm" 

172 
and \<tau> ::"ty" 

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

174 
by (cases \<tau>, simp_all) 

175 

176 
lemma fresh_ty: 

177 
fixes a ::"name" 

178 
and \<tau> ::"ty" 

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

180 
by (simp add: fresh_def supp_def) 

181 

182 
instance ty :: pt_name 

183 
apply(intro_classes) 

184 
apply(simp_all) 

185 
done 

186 

187 
instance ty :: fs_name 

188 
apply(intro_classes) 

189 
apply(simp add: supp_def) 

190 
done 

191 

192 
(* valid contexts *) 

193 

194 
consts 

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

196 
primrec 

197 
"dom_ty [] = []" 

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

199 

200 
consts 

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

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

203 
translations 

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

205 
inductive ctxts 

206 
intros 

207 
v1[intro]: "valid []" 

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

209 

210 
lemma valid_eqvt: 

211 
fixes pi:: "name prm" 

212 
assumes a: "valid \<Gamma>" 

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

214 
using a 

215 
apply(induct) 

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

217 
done 

218 

219 
(* typing judgements *) 

220 

221 
lemma fresh_context[rule_format]: 

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

223 
and a :: "name" 

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

225 
apply(induct_tac \<Gamma>) 

226 
apply(auto simp add: fresh_prod fresh_list_cons fresh_atm) 

227 
done 

228 

229 
lemma valid_elim: 

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

231 
and pi:: "name prm" 

232 
and a :: "name" 

233 
and \<tau> :: "ty" 

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

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

236 
done 

237 

238 
lemma valid_unicity[rule_format]: 

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

240 
apply(induct_tac \<Gamma>) 

241 
apply(auto dest!: valid_elim fresh_context) 

242 
done 

243 

244 
consts 

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

246 
syntax 

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

248 
translations 

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

250 

251 
inductive typing 

252 
intros 

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

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

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

256 

18313  257 
lemma eqvt_typing: 
18106  258 
fixes \<Gamma> :: "(name\<times>ty) list" 
259 
and t :: "lam" 

260 
and \<tau> :: "ty" 

261 
and pi:: "name prm" 

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

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

264 
using a 

265 
proof (induct) 

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

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

268 
moreover 

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

18313  270 
ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> ((pi::name prm)\<bullet>Var a) : \<tau>" 
271 
using typing.intros by (force simp add: pt_list_set_pi[OF pt_name_inst, symmetric]) 

18106  272 
next 
273 
case (t3 \<Gamma> \<sigma> \<tau> a t) 

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

18313  275 
ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) :\<tau>\<rightarrow>\<sigma>" by force 
18106  276 
qed (auto) 
277 

18313  278 
lemma typing_induct[consumes 1, case_names t1 t2 t3]: 
279 
fixes P :: "'a::fs_name\<Rightarrow>(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>bool" 

18106  280 
and \<Gamma> :: "(name\<times>ty) list" 
281 
and t :: "lam" 

282 
and \<tau> :: "ty" 

283 
and x :: "'a::fs_name" 

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

18313  285 
and a1: "\<And>\<Gamma> (a::name) \<tau> x. valid \<Gamma> \<Longrightarrow> (a,\<tau>) \<in> set \<Gamma> \<Longrightarrow> P x \<Gamma> (Var a) \<tau>" 
286 
and a2: "\<And>\<Gamma> \<tau> \<sigma> t1 t2 x. 

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

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

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

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

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

292 
proof  

293 
from a have "\<And>(pi::name prm) x. P x (pi\<bullet>\<Gamma>) (pi\<bullet>t) \<tau>" 

294 
proof (induct) 

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

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

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

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

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

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

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

302 
next 

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

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

305 
next 

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

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

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

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

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

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

312 
then obtain c::"name" 

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

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

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

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

317 
pt_rev_pi[OF pt_name_inst, OF at_name_inst]) 

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

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

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

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

322 
by (force simp add: pt2[OF pt_name_inst] at_calc[OF at_name_inst]) 

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

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

325 
by (force simp add: pt2[OF pt_name_inst] at_calc[OF at_name_inst]) 

326 
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 

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

328 
by (simp add: lam.inject alpha) 

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

330 
by (simp only: pt2[OF pt_name_inst], simp) 

331 
qed 

332 
hence "P x (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>t) \<tau>" by blast 

333 
thus "P x \<Gamma> t \<tau>" by simp 

334 
qed 

18106  335 

336 
constdefs 

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

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

339 

18313  340 
lemma weakening: 
341 
assumes a: "\<Gamma>1 \<turnstile> t : \<sigma>" 

342 
and b: "valid \<Gamma>2" 

343 
and c: "\<Gamma>1 \<lless> \<Gamma>2" 

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

345 
using a b c 

346 
apply(nominal_induct \<Gamma>1 t \<sigma> avoiding: \<Gamma>2 rule: typing_induct) 

18106  347 
apply(auto simp add: sub_def) 
18313  348 
(* FIXME: before using metaconnectives and the new induction *) 
349 
(* method, this was completely automatic *) 

350 
apply(atomize) 

351 
apply(auto) 

18106  352 
done 
353 

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

355 
apply(induct_tac \<Gamma>) 

356 
apply(auto) 

357 
done 

358 

359 
lemma free_vars: 

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

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

362 
using a 

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

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

365 
done 

366 

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

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

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

370 
done 

371 

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

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

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

375 
done 

376 

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

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

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

18313  380 
apply(drule_tac pi="[(a,aa)]::name prm" in eqvt_typing) 
18106  381 
apply(simp) 
382 
apply(subgoal_tac "([(a,aa)]::name prm)\<bullet>\<Gamma> = \<Gamma>")(*A*) 

383 
apply(force simp add: calc_atm) 

384 
(*A*) 

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

386 
done 

387 

388 
lemma typing_valid: 

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

390 
shows "valid \<Gamma>" 

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

392 

393 
lemma ty_subs[rule_format]: 

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

395 
and t1 ::"lam" 

396 
and t2 ::"lam" 

397 
and \<tau> ::"ty" 

398 
and \<sigma> ::"ty" 

399 
and c ::"name" 

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

18313  401 
proof(nominal_induct t1 avoiding: \<Gamma> \<sigma> \<tau> c t2 rule: lam_induct) 
402 
case (Var a) 

18106  403 
show ?case 
404 
proof(intro strip) 

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

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

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

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

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

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

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

412 
assume case1: "a=c" 

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

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

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

416 
next 

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

418 
show ?thesis 

419 
proof (rule ccontr) 

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

421 
with case1 a25 show False by force 

422 
qed 

423 
qed 

424 
next 

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

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

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

428 
qed 

429 
qed 

430 
next 

18313  431 
case (App s1 s2) 
18106  432 
show ?case 
433 
proof (intro strip, simp) 

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

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

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

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

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

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

440 
qed 

441 
next 

18313  442 
case (Lam a s) 
443 
have "a\<sharp>\<Gamma>" "a\<sharp>\<sigma>" "a\<sharp>\<tau>" "a\<sharp>c" "a\<sharp>t2" by fact 

18106  444 
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>)" 
445 
by (auto simp add: fresh_atm fresh_prod fresh_list_cons) 

446 
show ?case using f2 f3 

447 
proof(intro strip, simp) 

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

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

450 
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 

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

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

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

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

455 
proof  

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

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

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

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

460 
qed 

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

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

463 
proof  

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

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

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

467 
qed 

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

469 
using c11 Lam c14 c81 f1 by force 

470 
qed 

471 
qed 

472 

473 
lemma subject[rule_format]: 

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

475 
and t1 ::"lam" 

476 
and t2 ::"lam" 

477 
and \<tau> ::"ty" 

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

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

480 
using a 

18313  481 
proof (nominal_induct t1 t2 avoiding: \<Gamma> \<tau> rule: beta_induct, auto) 
482 
case (b1 t s1 s2) 

483 
have i: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1:\<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact 

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

18106  485 
hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> t : \<sigma>)" by (rule t2_elim) 
486 
then obtain \<sigma> where a1: "\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> t : \<sigma>" by force 

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

488 
next 

18313  489 
case (b2 t s1 s2) 
490 
have i: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact 

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

18106  492 
hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s1 : \<sigma>)" by (rule t2_elim) 
493 
then obtain \<sigma> where a1: "\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s1 : \<sigma>" by force 

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

495 
next 

18313  496 
case (b3 a s1 s2) 
497 
have f: "a\<sharp>\<Gamma>" and "a\<sharp>\<tau>" by fact+ 

498 
have i: "\<And>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" by fact 

18106  499 
assume "\<Gamma> \<turnstile> Lam [a].s1 : \<tau>" 
500 
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) 

501 
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 

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

503 
next 

18313  504 
case (b4 a s1 s2) 
505 
have f: "a\<sharp>\<Gamma>" by fact 

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

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

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

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

511 
qed 

512 

513 
lemma subject[rule_format]: 

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

515 
and t1 ::"lam" 

516 
and t2 ::"lam" 

517 
and \<tau> ::"ty" 

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

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

520 
using a 

18313  521 
apply(nominal_induct t1 t2 avoiding: \<Gamma> \<tau> rule: beta_induct) 
522 
apply(auto dest!: t2_elim t3_elim intro: ty_subs) 

18106  523 
done 
524 

525 
subsection {* some facts about beta *} 

526 

527 
constdefs 

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

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

530 

531 
constdefs 

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

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

534 

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

536 
apply(simp add: SN_def) 

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

538 
apply(auto) 

539 
done 

540 

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

542 
apply(simp add: SN_def) 

543 
apply(rule accI) 

544 
apply(auto) 

545 
done 

546 

547 

548 
section {* Candidates *} 

549 

550 
consts 

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

552 
primrec 

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

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

555 

556 
constdefs 

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

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

559 

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

561 
consts 

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

563 
syntax 

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

565 
translations 

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

567 
inductive FST 

568 
intros 

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

570 

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

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

573 
apply(simp add: lam.inject) 

574 
done 

575 

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

577 
apply(simp add: SN_def) 

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

579 
apply(force) 

580 
(*A*) 

581 
apply(erule acc_induct) 

582 
apply(clarify) 

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

584 
apply(clarify) 

585 
apply(rule accI) 

586 
apply(auto intro: b1) 

587 
done 

588 

589 
constdefs 

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

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

592 

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

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

595 

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

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

598 

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

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

601 

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

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

604 

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

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

607 
apply(blast) 

608 
done 

609 

610 
lemma sub_ind: 

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

612 
apply(simp add: SN_def) 

613 
apply(erule acc_induct) 

614 
apply(auto) 

615 
apply(simp add: CR3_def) 

616 
apply(rotate_tac 5) 

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

618 
apply(drule mp) 

619 
apply(rule conjI) 

620 
apply(force simp only: NEUT_def) 

621 
apply(simp (no_asm) add: CR3_RED_def) 

622 
apply(clarify) 

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

624 
apply(simp_all add: lam.inject) 

625 
apply(simp only: CR3_RED_def) 

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

627 
apply(simp) 

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

629 
apply(simp) 

630 
apply(drule mp) 

631 
apply(simp (no_asm_use) add: CR2_def) 

632 
apply(blast) 

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

634 
apply(force) 

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

636 
done 

637 

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

639 
apply(induct_tac \<tau>) 

640 
apply(auto) 

641 
(* atom types *) 

642 
(* C1 *) 

643 
apply(simp add: CR1_def) 

644 
(* C2 *) 

645 
apply(simp add: CR2_def) 

646 
apply(clarify) 

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

648 
apply(assumption)+ 

649 
(* C3 *) 

650 
apply(simp add: CR3_def CR3_RED_def) 

651 
apply(clarify) 

652 
apply(rule qq2) 

653 
apply(assumption) 

654 
(* arrow types *) 

655 
(* C1 *) 

656 
apply(simp (no_asm) add: CR1_def) 

657 
apply(clarify) 

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

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

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

661 
apply(simp) 

662 
apply(simp add: CR1_def) 

663 
apply(rotate_tac 1) 

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

665 
apply(simp) 

666 
apply(drule qq3) 

667 
apply(assumption) 

668 
(*C*) 

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

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

671 
apply(drule mp) 

672 
apply(clarify) 

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

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

675 
(*A*) 

676 
apply(simp (no_asm) only: NEUT_def) 

677 
apply(rule disjCI) 

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

679 
apply(simp (no_asm)) 

680 
(* C2 *) 

681 
apply(simp (no_asm) add: CR2_def) 

682 
apply(clarify) 

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

684 
apply(simp) 

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

686 
apply(simp (no_asm_use) only: CR2_def) 

687 
apply(blast) 

688 
(*X*) 

689 
apply(force intro!: b1) 

690 
(* C3 *) 

691 
apply(unfold CR3_def) 

692 
apply(rule allI) 

693 
apply(rule impI) 

694 
apply(erule conjE) 

695 
apply(simp (no_asm)) 

696 
apply(rule allI) 

697 
apply(rule impI) 

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

699 
apply(fold CR3_def) 

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

701 
apply(simp) 

702 
(*Z*) 

703 
apply(simp add: CR1_def) 

704 
done 

705 

706 
lemma double_acc_aux: 

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

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

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

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

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

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

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

714 
shows "P a b" 

715 
proof  

716 
from a_acc 

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

718 
proof (induct a rule: acc.induct) 

719 
case (accI x) 

720 
note accI' = accI 

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

722 
thus ?case 

723 
proof (induct b rule: acc.induct) 

724 
case (accI y) 

725 
show ?case 

726 
apply (rule hyp) 

727 
apply (erule accI') 

728 
apply (erule accI') 

729 
apply (rule acc.accI) 

730 
apply (erule accI) 

731 
apply (erule accI) 

732 
apply (erule accI) 

733 
done 

734 
qed 

735 
qed 

736 
from b_acc show ?thesis by (rule r) 

737 
qed 

738 

739 
lemma double_acc: 

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

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

742 
apply(assumption)+ 

743 
apply(blast) 

744 
done 

745 

18263
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset

746 
lemma abs_RED: "(\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>)\<longrightarrow>Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)" 
18106  747 
apply(simp) 
748 
apply(clarify) 

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

750 
apply(erule rev_mp) 

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

752 
apply(erule rev_mp) 

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

754 
apply(assumption) 

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

756 
apply(simp add: CR1_def SN_def) 

757 
(*A*) 

758 
apply(force simp add: RED_props) 

759 
apply(simp) 

760 
apply(clarify) 

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

762 
apply(simp add: CR3_def) 

763 
apply(rotate_tac 6) 

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

765 
apply(drule mp) 

766 
apply(rule conjI) 

767 
apply(force simp add: NEUT_def) 

768 
apply(simp add: CR3_RED_def) 

769 
apply(clarify) 

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

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

772 
apply(drule beta_abs) 

773 
apply(auto) 

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

775 
apply(simp) 

776 
apply(drule mp) 

777 
apply(clarify) 

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

779 
apply(assumption) 

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

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

782 
apply(simp (no_asm_use) add: CR2_def) 

783 
apply(blast) 

784 
(*C*) 

785 
apply(force simp add: RED_props) 

786 
(*B*) 

787 
apply(force intro!: beta_subst) 

788 
apply(assumption) 

789 
apply(rotate_tac 3) 

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

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

792 
apply(simp) 

793 
(*D*) 

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

795 
apply(simp (no_asm_use) add: CR2_def) 

796 
apply(blast) 

797 
(*E*) 

798 
apply(force simp add: RED_props) 

799 
apply(simp add: alpha) 

800 
apply(erule disjE) 

801 
apply(force) 

802 
apply(auto) 

803 
apply(simp add: subst_rename) 

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

805 
apply(assumption) 

806 
(*B*) 

807 
apply(force simp add: RED_props) 

808 
(*1*) 

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

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

811 
apply(drule CR3_CR4) 

812 
apply(simp add: CR4_def) 

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

814 
apply(drule mp) 

815 
apply(rule conjI) 

816 
apply(force simp add: NEUT_def) 

817 
apply(simp add: NORMAL_def) 

818 
apply(clarify) 

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

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

821 
apply(force simp add: RED_props) 

822 
apply(simp add: id_subs) 

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

824 
apply(simp add: CR1_def SN_def) 

825 
(*3*) 

826 
apply(force simp add: RED_props) 

827 
done 

828 

18263
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset

829 
lemma fresh_domain[rule_format]: "a\<sharp>\<theta>\<longrightarrow>a\<notin>set(domain \<theta>)" 
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset

830 
apply(induct_tac \<theta>) 
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset

831 
apply(auto simp add: fresh_prod fresh_list_cons fresh_atm) 
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset

832 
done 
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset

833 

7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset

834 
lemma fresh_at[rule_format]: "a\<in>set(domain \<theta>) \<longrightarrow> c\<sharp>\<theta>\<longrightarrow>c\<sharp>(\<theta><a>)" 
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset

835 
apply(induct_tac \<theta>) 
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset

836 
apply(auto simp add: fresh_prod fresh_list_cons) 
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset

837 
done 
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset

838 

18345  839 
lemma psubst_subst[rule_format]: "c\<sharp>\<theta>\<longrightarrow> (t[<\<theta>>])[c::=s] = t[<((c,s)#\<theta>)>]" 
18313  840 
apply(nominal_induct t avoiding: \<theta> c s rule: lam_induct) 
18263
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset

841 
apply(auto dest: fresh_domain) 
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset

842 
apply(drule fresh_at) 
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset

843 
apply(assumption) 
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset

844 
apply(rule forget) 
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset

845 
apply(assumption) 
18313  846 
apply(subgoal_tac "a\<sharp>((c,s)#\<theta>)")(*A*) 
847 
apply(simp) 

18263
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset

848 
(*A*) 
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset

849 
apply(simp add: fresh_list_cons fresh_prod) 
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset

850 
done 
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset

851 

18345  852 
thm fresh_context 
853 

18106  854 
lemma all_RED: 
18345  855 
assumes a: "\<Gamma>\<turnstile>t:\<tau>" 
856 
and b: "\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>) \<longrightarrow> (a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)" 

857 
shows "t[<\<theta>>]\<in>RED \<tau>" 

858 
using a b 

859 
proof(nominal_induct t avoiding: \<Gamma> \<tau> \<theta> rule: lam_induct) 

860 
case (Lam a t) "lambda case" 

861 
have ih: "\<And>\<Gamma> \<tau> \<theta>. \<Gamma> \<turnstile> t:\<tau> \<Longrightarrow> 

862 
(\<forall>c \<sigma>. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and> \<theta><c>\<in>RED \<sigma>) 

863 
\<Longrightarrow> t[<\<theta>>]\<in>RED \<tau>" 

864 
and \<theta>_cond: "\<forall>c \<sigma>. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and> \<theta><c>\<in>RED \<sigma>" 

865 
and fresh: "a\<sharp>\<Gamma>" "a\<sharp>\<theta>" 

866 
and "\<Gamma> \<turnstile> Lam [a].t:\<tau>" by fact 

867 
hence "\<exists>\<tau>1 \<tau>2. \<tau>=\<tau>1\<rightarrow>\<tau>2 \<and> ((a,\<tau>1)#\<Gamma>)\<turnstile>t:\<tau>2" using t3_elim fresh by simp 

868 
then obtain \<tau>1 \<tau>2 where \<tau>_inst: "\<tau>=\<tau>1\<rightarrow>\<tau>2" and typing: "((a,\<tau>1)#\<Gamma>)\<turnstile>t:\<tau>2" by blast 

869 
from ih have "\<forall>s\<in>RED \<tau>1. t[<\<theta>>][a::=s] \<in> RED \<tau>2" using fresh typing \<theta>_cond 

870 
by (force dest: fresh_context simp add: psubst_subst) 

871 
hence "(Lam [a].(t[<\<theta>>])) \<in> RED (\<tau>1 \<rightarrow> \<tau>2)" by (simp only: abs_RED) 

872 
thus "(Lam [a].t)[<\<theta>>] \<in> RED \<tau>" using fresh \<tau>_inst by simp 

873 
qed (force dest!: t1_elim t2_elim)+ 

874 

875 
lemma all_RED: 

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

877 
and b: "\<And>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>) \<Longrightarrow> (a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)" 

878 
shows "t[<\<theta>>]\<in>RED \<tau>" 

879 
using a b 

18313  880 
apply(nominal_induct t avoiding: \<Gamma> \<tau> \<theta> rule: lam_induct) 
18106  881 
(* Variables *) 
882 
apply(force dest: t1_elim) 

883 
(* Applications *) 

18313  884 
apply(atomize) 
885 
apply(force dest!: t2_elim) 

18345  886 
(* Abstractions *) 
887 
apply(auto dest!: t3_elim simp only: psubst_Lam) 

18313  888 
apply(rule abs_RED[THEN mp]) 
18348  889 
apply(force dest: fresh_context simp add: psubst_subst) 
18345  890 
done 