author | urbanc |
Mon, 28 Nov 2005 05:03:00 +0100 | |
changeset 18269 | 3f36e2165e51 |
parent 18263 | 7f75925498da |
child 18313 | e61d2424863d |
permissions | -rw-r--r-- |
18263
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1 |
(* $Id$ *) |
18106 | 2 |
|
18269 | 3 |
|
4 |
||
18106 | 5 |
theory sn |
6 |
imports lam_substs Accessible_Part |
|
7 |
begin |
|
8 |
||
18269 | 9 |
text {* Strong Normalisation proof from the Proofs and Types book *} |
18106 | 10 |
|
11 |
section {* Beta Reduction *} |
|
12 |
||
13 |
lemma subst_rename[rule_format]: |
|
14 |
fixes c :: "name" |
|
15 |
and a :: "name" |
|
16 |
and t1 :: "lam" |
|
17 |
and t2 :: "lam" |
|
18 |
shows "c\<sharp>t1 \<longrightarrow> (t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2])" |
|
19 |
apply(nominal_induct t1 rule: lam_induct) |
|
20 |
apply(auto simp add: calc_atm fresh_atm fresh_prod abs_fresh) |
|
21 |
done |
|
22 |
||
23 |
lemma forget[rule_format]: |
|
24 |
shows "a\<sharp>t1 \<longrightarrow> t1[a::=t2] = t1" |
|
25 |
apply (nominal_induct t1 rule: lam_induct) |
|
26 |
apply(auto simp add: abs_fresh fresh_atm fresh_prod) |
|
27 |
done |
|
28 |
||
29 |
lemma fresh_fact[rule_format]: |
|
30 |
fixes b :: "name" |
|
31 |
and a :: "name" |
|
32 |
and t1 :: "lam" |
|
33 |
and t2 :: "lam" |
|
34 |
shows "a\<sharp>t1\<longrightarrow>a\<sharp>t2\<longrightarrow>a\<sharp>(t1[b::=t2])" |
|
35 |
apply(nominal_induct t1 rule: lam_induct) |
|
36 |
apply(auto simp add: abs_fresh fresh_prod fresh_atm) |
|
37 |
done |
|
38 |
||
39 |
lemma subs_lemma: |
|
40 |
fixes x::"name" |
|
41 |
and y::"name" |
|
42 |
and L::"lam" |
|
43 |
and M::"lam" |
|
44 |
and N::"lam" |
|
45 |
shows "x\<noteq>y\<longrightarrow>x\<sharp>L\<longrightarrow>M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" |
|
46 |
apply(nominal_induct M rule: lam_induct) |
|
47 |
apply(auto simp add: fresh_fact forget fresh_prod fresh_atm) |
|
48 |
done |
|
49 |
||
50 |
lemma id_subs: "t[x::=Var x] = t" |
|
51 |
apply(nominal_induct t rule: lam_induct) |
|
52 |
apply(simp_all add: fresh_atm) |
|
53 |
done |
|
54 |
||
55 |
consts |
|
56 |
Beta :: "(lam\<times>lam) set" |
|
57 |
syntax |
|
58 |
"_Beta" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80) |
|
59 |
"_Beta_star" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta>\<^sup>* _" [80,80] 80) |
|
60 |
translations |
|
61 |
"t1 \<longrightarrow>\<^isub>\<beta> t2" \<rightleftharpoons> "(t1,t2) \<in> Beta" |
|
62 |
"t1 \<longrightarrow>\<^isub>\<beta>\<^sup>* t2" \<rightleftharpoons> "(t1,t2) \<in> Beta\<^sup>*" |
|
63 |
inductive Beta |
|
64 |
intros |
|
65 |
b1[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App s1 t)\<longrightarrow>\<^isub>\<beta>(App s2 t)" |
|
66 |
b2[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (App t s1)\<longrightarrow>\<^isub>\<beta>(App t s2)" |
|
67 |
b3[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (Lam [a].s1)\<longrightarrow>\<^isub>\<beta> (Lam [(a::name)].s2)" |
|
68 |
b4[intro!]: "(App (Lam [(a::name)].s1) s2)\<longrightarrow>\<^isub>\<beta>(s1[a::=s2])" |
|
69 |
||
70 |
lemma eqvt_beta: |
|
71 |
fixes pi :: "name prm" |
|
72 |
and t :: "lam" |
|
73 |
and s :: "lam" |
|
74 |
shows "t\<longrightarrow>\<^isub>\<beta>s \<Longrightarrow> (pi\<bullet>t)\<longrightarrow>\<^isub>\<beta>(pi\<bullet>s)" |
|
75 |
apply(erule Beta.induct) |
|
76 |
apply(auto) |
|
77 |
done |
|
78 |
||
79 |
lemma beta_induct_aux[rule_format]: |
|
80 |
fixes P :: "lam \<Rightarrow> lam \<Rightarrow>'a::fs_name\<Rightarrow>bool" |
|
81 |
and t :: "lam" |
|
82 |
and s :: "lam" |
|
83 |
assumes a: "t\<longrightarrow>\<^isub>\<beta>s" |
|
84 |
and a1: "\<And>x t s1 s2. |
|
85 |
s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App s1 t) (App s2 t) x" |
|
86 |
and a2: "\<And>x t s1 s2. |
|
87 |
s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App t s1) (App t s2) x" |
|
88 |
and a3: "\<And>x (a::name) s1 s2. |
|
89 |
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" |
|
90 |
and a4: "\<And>x (a::name) t1 s1. a\<sharp>(s1,x) \<Longrightarrow> P (App (Lam [a].t1) s1) (t1[a::=s1]) x" |
|
91 |
shows "\<forall>x (pi::name prm). P (pi\<bullet>t) (pi\<bullet>s) x" |
|
92 |
using a |
|
93 |
proof (induct) |
|
94 |
case b1 thus ?case using a1 by (simp, blast intro: eqvt_beta) |
|
95 |
next |
|
96 |
case b2 thus ?case using a2 by (simp, blast intro: eqvt_beta) |
|
97 |
next |
|
98 |
case (b3 a s1 s2) |
|
99 |
assume j1: "s1 \<longrightarrow>\<^isub>\<beta> s2" |
|
100 |
assume j2: "\<forall>x (pi::name prm). P (pi\<bullet>s1) (pi\<bullet>s2) x" |
|
101 |
show ?case |
|
102 |
proof (simp, intro strip) |
|
103 |
fix pi::"name prm" and x::"'a::fs_name" |
|
104 |
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)" |
|
105 |
by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1) |
|
106 |
then obtain c::"name" |
|
107 |
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)" |
|
108 |
by (force simp add: fresh_prod fresh_atm) |
|
109 |
have x: "P (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s1)) (Lam [c].(([(c,pi\<bullet>a)]@pi)\<bullet>s2)) x" |
|
110 |
using a3 f2 j1 j2 by (simp, blast intro: eqvt_beta) |
|
111 |
have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3 |
|
112 |
by (simp add: lam.inject alpha) |
|
113 |
have alpha2: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s2))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s2))" using f1 f3 |
|
114 |
by (simp add: lam.inject alpha) |
|
115 |
show " P (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (Lam [(pi\<bullet>a)].(pi\<bullet>s2)) x" |
|
116 |
using x alpha1 alpha2 by (simp only: pt_name2) |
|
117 |
qed |
|
118 |
next |
|
119 |
case (b4 a s1 s2) |
|
120 |
show ?case |
|
121 |
proof (simp add: subst_eqvt, intro strip) |
|
122 |
fix pi::"name prm" and x::"'a::fs_name" |
|
123 |
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>s1,pi\<bullet>s2,x)" |
|
124 |
by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1) |
|
125 |
then obtain c::"name" |
|
126 |
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)" |
|
127 |
by (force simp add: fresh_prod fresh_atm) |
|
128 |
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" |
|
129 |
using a4 f2 by (blast intro!: eqvt_beta) |
|
130 |
have alpha1: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>s1))) = (Lam [(pi\<bullet>a)].(pi\<bullet>s1))" using f1 f3 |
|
131 |
by (simp add: lam.inject alpha) |
|
132 |
have alpha2: "(([(c,pi\<bullet>a)]@pi)\<bullet>s1)[c::=(pi\<bullet>s2)] = (pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)]" |
|
133 |
using f3 by (simp only: subst_rename[symmetric] pt_name2) |
|
134 |
show "P (App (Lam [(pi\<bullet>a)].(pi\<bullet>s1)) (pi\<bullet>s2)) ((pi\<bullet>s1)[(pi\<bullet>a)::=(pi\<bullet>s2)]) x" |
|
135 |
using x alpha1 alpha2 by (simp only: pt_name2) |
|
136 |
qed |
|
137 |
qed |
|
138 |
||
139 |
lemma beta_induct[case_names b1 b2 b3 b4]: |
|
140 |
fixes P :: "lam \<Rightarrow> lam \<Rightarrow>'a::fs_name\<Rightarrow>bool" |
|
141 |
and t :: "lam" |
|
142 |
and s :: "lam" |
|
143 |
and x :: "'a::fs_name" |
|
144 |
assumes a: "t\<longrightarrow>\<^isub>\<beta>s" |
|
145 |
and a1: "\<And>x t s1 s2. |
|
146 |
s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App s1 t) (App s2 t) x" |
|
147 |
and a2: "\<And>x t s1 s2. |
|
148 |
s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> (\<forall>z. P s1 s2 z) \<Longrightarrow> P (App t s1) (App t s2) x" |
|
149 |
and a3: "\<And>x (a::name) s1 s2. |
|
150 |
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" |
|
151 |
and a4: "\<And>x (a::name) t1 s1. |
|
152 |
a\<sharp>(s1,x) \<Longrightarrow> P (App (Lam [a].t1) s1) (t1[a::=s1]) x" |
|
153 |
shows "P t s x" |
|
154 |
using a a1 a2 a3 a4 |
|
155 |
by (auto intro!: beta_induct_aux[of "t" "s" "P" "[]" "x", simplified]) |
|
156 |
||
157 |
lemma supp_beta: "t\<longrightarrow>\<^isub>\<beta> s\<Longrightarrow>(supp s)\<subseteq>((supp t)::name set)" |
|
158 |
apply(erule Beta.induct) |
|
159 |
apply(auto intro!: simp add: abs_supp lam.supp subst_supp) |
|
160 |
done |
|
161 |
lemma beta_abs: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'\<Longrightarrow>\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''" |
|
162 |
apply(ind_cases "Lam [a].t \<longrightarrow>\<^isub>\<beta> t'") |
|
163 |
apply(auto simp add: lam.distinct lam.inject) |
|
164 |
apply(auto simp add: alpha) |
|
165 |
apply(rule_tac x="[(a,aa)]\<bullet>s2" in exI) |
|
166 |
apply(rule conjI) |
|
167 |
apply(rule sym) |
|
168 |
apply(rule pt_bij2[OF pt_name_inst, OF at_name_inst]) |
|
169 |
apply(simp) |
|
170 |
apply(rule pt_name3) |
|
171 |
apply(simp add: at_ds5[OF at_name_inst]) |
|
172 |
apply(rule conjI) |
|
173 |
apply(simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] calc_atm) |
|
174 |
apply(force dest!: supp_beta simp add: fresh_def) |
|
175 |
apply(force intro!: eqvt_beta) |
|
176 |
done |
|
177 |
||
178 |
lemma beta_subst[rule_format]: |
|
179 |
assumes a: "M \<longrightarrow>\<^isub>\<beta> M'" |
|
180 |
shows "M[x::=N]\<longrightarrow>\<^isub>\<beta> M'[x::=N]" |
|
181 |
using a |
|
182 |
apply(nominal_induct M M' rule: beta_induct) |
|
183 |
apply(auto simp add: fresh_prod fresh_atm subs_lemma) |
|
184 |
done |
|
185 |
||
186 |
instance nat :: fs_name |
|
187 |
apply(intro_classes) |
|
188 |
apply(simp_all add: supp_def perm_nat_def) |
|
189 |
done |
|
190 |
||
191 |
datatype ty = |
|
192 |
TVar "string" |
|
193 |
| TArr "ty" "ty" (infix "\<rightarrow>" 200) |
|
194 |
||
195 |
primrec |
|
196 |
"pi\<bullet>(TVar s) = TVar s" |
|
197 |
"pi\<bullet>(\<tau> \<rightarrow> \<sigma>) = (\<tau> \<rightarrow> \<sigma>)" |
|
198 |
||
199 |
lemma perm_ty[simp]: |
|
200 |
fixes pi ::"name prm" |
|
201 |
and \<tau> ::"ty" |
|
202 |
shows "pi\<bullet>\<tau> = \<tau>" |
|
203 |
by (cases \<tau>, simp_all) |
|
204 |
||
205 |
lemma fresh_ty: |
|
206 |
fixes a ::"name" |
|
207 |
and \<tau> ::"ty" |
|
208 |
shows "a\<sharp>\<tau>" |
|
209 |
by (simp add: fresh_def supp_def) |
|
210 |
||
211 |
instance ty :: pt_name |
|
212 |
apply(intro_classes) |
|
213 |
apply(simp_all) |
|
214 |
done |
|
215 |
||
216 |
instance ty :: fs_name |
|
217 |
apply(intro_classes) |
|
218 |
apply(simp add: supp_def) |
|
219 |
done |
|
220 |
||
221 |
(* valid contexts *) |
|
222 |
||
223 |
consts |
|
224 |
"dom_ty" :: "(name\<times>ty) list \<Rightarrow> (name list)" |
|
225 |
primrec |
|
226 |
"dom_ty [] = []" |
|
227 |
"dom_ty (x#\<Gamma>) = (fst x)#(dom_ty \<Gamma>)" |
|
228 |
||
229 |
consts |
|
230 |
ctxts :: "((name\<times>ty) list) set" |
|
231 |
valid :: "(name\<times>ty) list \<Rightarrow> bool" |
|
232 |
translations |
|
233 |
"valid \<Gamma>" \<rightleftharpoons> "\<Gamma> \<in> ctxts" |
|
234 |
inductive ctxts |
|
235 |
intros |
|
236 |
v1[intro]: "valid []" |
|
237 |
v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" |
|
238 |
||
239 |
lemma valid_eqvt: |
|
240 |
fixes pi:: "name prm" |
|
241 |
assumes a: "valid \<Gamma>" |
|
242 |
shows "valid (pi\<bullet>\<Gamma>)" |
|
243 |
using a |
|
244 |
apply(induct) |
|
245 |
apply(auto simp add: pt_fresh_bij[OF pt_name_inst, OF at_name_inst]) |
|
246 |
done |
|
247 |
||
248 |
(* typing judgements *) |
|
249 |
||
250 |
lemma fresh_context[rule_format]: |
|
251 |
fixes \<Gamma> :: "(name\<times>ty)list" |
|
252 |
and a :: "name" |
|
253 |
shows "a\<sharp>\<Gamma>\<longrightarrow>\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)" |
|
254 |
apply(induct_tac \<Gamma>) |
|
255 |
apply(auto simp add: fresh_prod fresh_list_cons fresh_atm) |
|
256 |
done |
|
257 |
||
258 |
lemma valid_elim: |
|
259 |
fixes \<Gamma> :: "(name\<times>ty)list" |
|
260 |
and pi:: "name prm" |
|
261 |
and a :: "name" |
|
262 |
and \<tau> :: "ty" |
|
263 |
shows "valid ((a,\<tau>)#\<Gamma>) \<Longrightarrow> valid \<Gamma> \<and> a\<sharp>\<Gamma>" |
|
264 |
apply(ind_cases "valid ((a,\<tau>)#\<Gamma>)", simp) |
|
265 |
done |
|
266 |
||
267 |
lemma valid_unicity[rule_format]: |
|
268 |
shows "valid \<Gamma>\<longrightarrow>(c,\<sigma>)\<in>set \<Gamma>\<longrightarrow>(c,\<tau>)\<in>set \<Gamma>\<longrightarrow>\<sigma>=\<tau>" |
|
269 |
apply(induct_tac \<Gamma>) |
|
270 |
apply(auto dest!: valid_elim fresh_context) |
|
271 |
done |
|
272 |
||
273 |
consts |
|
274 |
typing :: "(((name\<times>ty) list)\<times>lam\<times>ty) set" |
|
275 |
syntax |
|
276 |
"_typing_judge" :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [80,80,80] 80) |
|
277 |
translations |
|
278 |
"\<Gamma> \<turnstile> t : \<tau>" \<rightleftharpoons> "(\<Gamma>,t,\<tau>) \<in> typing" |
|
279 |
||
280 |
inductive typing |
|
281 |
intros |
|
282 |
t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>" |
|
283 |
t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>" |
|
284 |
t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>" |
|
285 |
||
286 |
lemma typing_eqvt: |
|
287 |
fixes \<Gamma> :: "(name\<times>ty) list" |
|
288 |
and t :: "lam" |
|
289 |
and \<tau> :: "ty" |
|
290 |
and pi:: "name prm" |
|
291 |
assumes a: "\<Gamma> \<turnstile> t : \<tau>" |
|
292 |
shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : \<tau>" |
|
293 |
using a |
|
294 |
proof (induct) |
|
295 |
case (t1 \<Gamma> \<tau> a) |
|
296 |
have "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt) |
|
297 |
moreover |
|
298 |
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]) |
|
299 |
ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Var a) : \<tau>" |
|
300 |
using typing.intros by (auto simp add: pt_list_set_pi[OF pt_name_inst]) |
|
301 |
next |
|
302 |
case (t3 \<Gamma> \<sigma> \<tau> a t) |
|
303 |
moreover have "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" by (rule pt_fresh_bij1[OF pt_name_inst, OF at_name_inst]) |
|
304 |
ultimately show "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>Lam [a].t) : \<tau>\<rightarrow>\<sigma>" |
|
305 |
using typing.intros by (force) |
|
306 |
qed (auto) |
|
307 |
||
308 |
lemma typing_induct_aux[rule_format]: |
|
309 |
fixes P :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>'a::fs_name\<Rightarrow>bool" |
|
310 |
and \<Gamma> :: "(name\<times>ty) list" |
|
311 |
and t :: "lam" |
|
312 |
and \<tau> :: "ty" |
|
313 |
assumes a: "\<Gamma> \<turnstile> t : \<tau>" |
|
314 |
and a1: "\<And>x \<Gamma> (a::name) \<tau>. valid \<Gamma> \<Longrightarrow> (a,\<tau>) \<in> set \<Gamma> \<Longrightarrow> P \<Gamma> (Var a) \<tau> x" |
|
315 |
and a2: "\<And>x \<Gamma> \<tau> \<sigma> t1 t2. |
|
316 |
\<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) |
|
317 |
\<Longrightarrow> P \<Gamma> (App t1 t2) \<sigma> x" |
|
318 |
and a3: "\<And>x (a::name) \<Gamma> \<tau> \<sigma> t. |
|
319 |
a\<sharp>x \<Longrightarrow> a\<sharp>\<Gamma> \<Longrightarrow> ((a,\<tau>) # \<Gamma>) \<turnstile> t : \<sigma> \<Longrightarrow> (\<forall>z. P ((a,\<tau>)#\<Gamma>) t \<sigma> z) |
|
320 |
\<Longrightarrow> P \<Gamma> (Lam [a].t) (\<tau>\<rightarrow>\<sigma>) x" |
|
321 |
shows "\<forall>(pi::name prm) (x::'a::fs_name). P (pi\<bullet>\<Gamma>) (pi\<bullet>t) \<tau> x" |
|
322 |
using a |
|
323 |
proof (induct) |
|
324 |
case (t1 \<Gamma> \<tau> a) |
|
325 |
assume j1: "valid \<Gamma>" |
|
326 |
assume j2: "(a,\<tau>)\<in>set \<Gamma>" |
|
327 |
show ?case |
|
328 |
proof (intro strip, simp) |
|
329 |
fix pi::"name prm" and x::"'a::fs_name" |
|
330 |
from j1 have j3: "valid (pi\<bullet>\<Gamma>)" by (rule valid_eqvt) |
|
331 |
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]) |
|
332 |
hence j4: "(pi\<bullet>a,\<tau>)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: pt_list_set_pi[OF pt_name_inst]) |
|
333 |
show "P (pi\<bullet>\<Gamma>) (Var (pi\<bullet>a)) \<tau> x" using a1 j3 j4 by force |
|
334 |
qed |
|
335 |
next |
|
336 |
case (t2 \<Gamma> \<sigma> \<tau> t1 t2) |
|
337 |
thus ?case using a2 by (simp, blast intro: typing_eqvt) |
|
338 |
next |
|
339 |
case (t3 \<Gamma> \<sigma> \<tau> a t) |
|
340 |
have k1: "a\<sharp>\<Gamma>" by fact |
|
341 |
have k2: "((a,\<tau>)#\<Gamma>)\<turnstile>t:\<sigma>" by fact |
|
342 |
have k3: "\<forall>(pi::name prm) (x::'a::fs_name). P (pi \<bullet> ((a,\<tau>)#\<Gamma>)) (pi\<bullet>t) \<sigma> x" by fact |
|
343 |
show ?case |
|
344 |
proof (intro strip, simp) |
|
345 |
fix pi::"name prm" and x::"'a::fs_name" |
|
346 |
have f: "\<exists>c::name. c\<sharp>(pi\<bullet>a,pi\<bullet>t,pi\<bullet>\<Gamma>,x)" |
|
347 |
by (rule at_exists_fresh[OF at_name_inst], simp add: fs_name1) |
|
348 |
then obtain c::"name" |
|
349 |
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>)" |
|
350 |
by (force simp add: fresh_prod fresh_atm) |
|
351 |
from k1 have k1a: "(pi\<bullet>a)\<sharp>(pi\<bullet>\<Gamma>)" |
|
352 |
by (simp add: pt_fresh_left[OF pt_name_inst, OF at_name_inst] |
|
353 |
pt_rev_pi[OF pt_name_inst, OF at_name_inst]) |
|
354 |
have l1: "(([(c,pi\<bullet>a)]@pi)\<bullet>\<Gamma>) = (pi\<bullet>\<Gamma>)" using f4 k1a |
|
355 |
by (simp only: pt_name2, rule pt_fresh_fresh[OF pt_name_inst, OF at_name_inst]) |
|
356 |
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 |
|
357 |
hence l2: "\<forall>x. P ((c, \<tau>)#(pi\<bullet>\<Gamma>)) (([(c,pi\<bullet>a)]@pi)\<bullet>t) \<sigma> x" using f1 l1 |
|
358 |
by (force simp add: pt_name2 calc_atm split: if_splits) |
|
359 |
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) |
|
360 |
hence l3: "((c, \<tau>)#(pi\<bullet>\<Gamma>)) \<turnstile> (([(c,pi\<bullet>a)]@pi)\<bullet>t) : \<sigma>" using l1 f1 |
|
361 |
by (force simp add: pt_name2 calc_atm split: if_splits) |
|
362 |
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 |
|
363 |
have alpha: "(Lam [c].([(c,pi\<bullet>a)]\<bullet>(pi\<bullet>t))) = (Lam [(pi\<bullet>a)].(pi\<bullet>t))" using f1 f3 |
|
364 |
by (simp add: lam.inject alpha) |
|
365 |
show "P (pi\<bullet>\<Gamma>) (Lam [(pi\<bullet>a)].(pi\<bullet>t)) (\<tau> \<rightarrow> \<sigma>) x" using l4 alpha |
|
366 |
by (simp only: pt_name2) |
|
367 |
qed |
|
368 |
qed |
|
369 |
||
370 |
lemma typing_induct[case_names t1 t2 t3]: |
|
371 |
fixes P :: "(name\<times>ty) list \<Rightarrow> lam \<Rightarrow> ty \<Rightarrow>'a::fs_name\<Rightarrow>bool" |
|
372 |
and \<Gamma> :: "(name\<times>ty) list" |
|
373 |
and t :: "lam" |
|
374 |
and \<tau> :: "ty" |
|
375 |
and x :: "'a::fs_name" |
|
376 |
assumes a: "\<Gamma> \<turnstile> t : \<tau>" |
|
377 |
and a1: "\<And>x \<Gamma> (a::name) \<tau>. valid \<Gamma> \<Longrightarrow> (a,\<tau>) \<in> set \<Gamma> \<Longrightarrow> P \<Gamma> (Var a) \<tau> x" |
|
378 |
and a2: "\<And>x \<Gamma> \<tau> \<sigma> t1 t2. |
|
379 |
\<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) |
|
380 |
\<Longrightarrow> P \<Gamma> (App t1 t2) \<sigma> x" |
|
381 |
and a3: "\<And>x (a::name) \<Gamma> \<tau> \<sigma> t. |
|
382 |
a\<sharp>x \<Longrightarrow> a\<sharp>\<Gamma> \<Longrightarrow> ((a,\<tau>) # \<Gamma>) \<turnstile> t : \<sigma> \<Longrightarrow> (\<forall>z. P ((a,\<tau>)#\<Gamma>) t \<sigma> z) |
|
383 |
\<Longrightarrow> P \<Gamma> (Lam [a].t) (\<tau>\<rightarrow>\<sigma>) x" |
|
384 |
shows "P \<Gamma> t \<tau> x" |
|
385 |
using a a1 a2 a3 typing_induct_aux[of "\<Gamma>" "t" "\<tau>" "P" "[]" "x", simplified] by force |
|
386 |
||
387 |
constdefs |
|
388 |
"sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [80,80] 80) |
|
389 |
"\<Gamma>1 \<lless> \<Gamma>2 \<equiv> \<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow> (a,\<sigma>)\<in>set \<Gamma>2" |
|
390 |
||
391 |
lemma weakening[rule_format]: |
|
392 |
assumes a: "\<Gamma>1 \<turnstile> t : \<sigma>" |
|
393 |
shows "valid \<Gamma>2 \<longrightarrow> \<Gamma>1 \<lless> \<Gamma>2 \<longrightarrow> \<Gamma>2 \<turnstile> t:\<sigma>" |
|
394 |
using a |
|
395 |
apply(nominal_induct \<Gamma>1 t \<sigma> rule: typing_induct) |
|
396 |
apply(auto simp add: sub_def) |
|
397 |
done |
|
398 |
||
399 |
lemma in_ctxt[rule_format]: "(a,\<tau>)\<in>set \<Gamma> \<longrightarrow> (a\<in>set(dom_ty \<Gamma>))" |
|
400 |
apply(induct_tac \<Gamma>) |
|
401 |
apply(auto) |
|
402 |
done |
|
403 |
||
404 |
lemma free_vars: |
|
405 |
assumes a: "\<Gamma> \<turnstile> t : \<tau>" |
|
406 |
shows " (supp t)\<subseteq>set(dom_ty \<Gamma>)" |
|
407 |
using a |
|
408 |
apply(nominal_induct \<Gamma> t \<tau> rule: typing_induct) |
|
409 |
apply(auto simp add: lam.supp abs_supp supp_atm in_ctxt) |
|
410 |
done |
|
411 |
||
412 |
lemma t1_elim: "\<Gamma> \<turnstile> Var a : \<tau> \<Longrightarrow> valid \<Gamma> \<and> (a,\<tau>) \<in> set \<Gamma>" |
|
413 |
apply(ind_cases "\<Gamma> \<turnstile> Var a : \<tau>") |
|
414 |
apply(auto simp add: lam.inject lam.distinct) |
|
415 |
done |
|
416 |
||
417 |
lemma t2_elim: "\<Gamma> \<turnstile> App t1 t2 : \<sigma> \<Longrightarrow> \<exists>\<tau>. (\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma> \<and> \<Gamma> \<turnstile> t2 : \<tau>)" |
|
418 |
apply(ind_cases "\<Gamma> \<turnstile> App t1 t2 : \<sigma>") |
|
419 |
apply(auto simp add: lam.inject lam.distinct) |
|
420 |
done |
|
421 |
||
422 |
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>'" |
|
423 |
apply(ind_cases "\<Gamma> \<turnstile> Lam [a].t : \<sigma>") |
|
424 |
apply(auto simp add: lam.distinct lam.inject alpha) |
|
425 |
apply(drule_tac pi="[(a,aa)]::name prm" in typing_eqvt) |
|
426 |
apply(simp) |
|
427 |
apply(subgoal_tac "([(a,aa)]::name prm)\<bullet>\<Gamma> = \<Gamma>")(*A*) |
|
428 |
apply(force simp add: calc_atm) |
|
429 |
(*A*) |
|
430 |
apply(force intro!: pt_fresh_fresh[OF pt_name_inst, OF at_name_inst]) |
|
431 |
done |
|
432 |
||
433 |
lemma typing_valid: |
|
434 |
assumes a: "\<Gamma> \<turnstile> t : \<tau>" |
|
435 |
shows "valid \<Gamma>" |
|
436 |
using a by (induct, auto dest!: valid_elim) |
|
437 |
||
438 |
lemma ty_subs[rule_format]: |
|
439 |
fixes \<Gamma> ::"(name\<times>ty) list" |
|
440 |
and t1 ::"lam" |
|
441 |
and t2 ::"lam" |
|
442 |
and \<tau> ::"ty" |
|
443 |
and \<sigma> ::"ty" |
|
444 |
and c ::"name" |
|
445 |
shows "((c,\<sigma>)#\<Gamma>) \<turnstile> t1:\<tau>\<longrightarrow> \<Gamma>\<turnstile> t2:\<sigma>\<longrightarrow> \<Gamma> \<turnstile> t1[c::=t2]:\<tau>" |
|
446 |
proof(nominal_induct t1 rule: lam_induct) |
|
447 |
case (Var \<Gamma> \<sigma> \<tau> c t2 a) |
|
448 |
show ?case |
|
449 |
proof(intro strip) |
|
450 |
assume a1: "\<Gamma> \<turnstile>t2:\<sigma>" |
|
451 |
assume a2: "((c,\<sigma>)#\<Gamma>) \<turnstile> Var a:\<tau>" |
|
452 |
hence a21: "(a,\<tau>)\<in>set((c,\<sigma>)#\<Gamma>)" and a22: "valid((c,\<sigma>)#\<Gamma>)" by (auto dest: t1_elim) |
|
453 |
from a22 have a23: "valid \<Gamma>" and a24: "c\<sharp>\<Gamma>" by (auto dest: valid_elim) |
|
454 |
from a24 have a25: "\<not>(\<exists>\<tau>. (c,\<tau>)\<in>set \<Gamma>)" by (rule fresh_context) |
|
455 |
show "\<Gamma>\<turnstile>(Var a)[c::=t2] : \<tau>" |
|
456 |
proof (cases "a=c", simp_all) |
|
457 |
assume case1: "a=c" |
|
458 |
show "\<Gamma> \<turnstile> t2:\<tau>" using a1 |
|
459 |
proof (cases "\<sigma>=\<tau>") |
|
460 |
assume "\<sigma>=\<tau>" thus ?thesis using a1 by simp |
|
461 |
next |
|
462 |
assume a3: "\<sigma>\<noteq>\<tau>" |
|
463 |
show ?thesis |
|
464 |
proof (rule ccontr) |
|
465 |
from a3 a21 have "(a,\<tau>)\<in>set \<Gamma>" by force |
|
466 |
with case1 a25 show False by force |
|
467 |
qed |
|
468 |
qed |
|
469 |
next |
|
470 |
assume case2: "a\<noteq>c" |
|
471 |
with a21 have a26: "(a,\<tau>)\<in>set \<Gamma>" by force |
|
472 |
from a23 a26 show "\<Gamma> \<turnstile> Var a:\<tau>" by force |
|
473 |
qed |
|
474 |
qed |
|
475 |
next |
|
476 |
case (App \<Gamma> \<sigma> \<tau> c t2 s1 s2) |
|
477 |
show ?case |
|
478 |
proof (intro strip, simp) |
|
479 |
assume b1: "\<Gamma> \<turnstile>t2:\<sigma>" |
|
480 |
assume b2: " ((c,\<sigma>)#\<Gamma>)\<turnstile>App s1 s2 : \<tau>" |
|
481 |
hence "\<exists>\<tau>'. (((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau> \<and> ((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>')" by (rule t2_elim) |
|
482 |
then obtain \<tau>' where b3a: "((c,\<sigma>)#\<Gamma>)\<turnstile>s1:\<tau>'\<rightarrow>\<tau>" and b3b: "((c,\<sigma>)#\<Gamma>)\<turnstile>s2:\<tau>'" by force |
|
483 |
show "\<Gamma> \<turnstile> App (s1[c::=t2]) (s2[c::=t2]) : \<tau>" |
|
484 |
using b1 b3a b3b App by (rule_tac \<tau>="\<tau>'" in t2, auto) |
|
485 |
qed |
|
486 |
next |
|
487 |
case (Lam \<Gamma> \<sigma> \<tau> c t2 a s) |
|
488 |
assume "a\<sharp>(\<Gamma>,\<sigma>,\<tau>,c,t2)" |
|
489 |
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>)" |
|
490 |
by (auto simp add: fresh_atm fresh_prod fresh_list_cons) |
|
491 |
show ?case using f2 f3 |
|
492 |
proof(intro strip, simp) |
|
493 |
assume c1: "((c,\<sigma>)#\<Gamma>)\<turnstile>Lam [a].s : \<tau>" |
|
494 |
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) |
|
495 |
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 |
|
496 |
from c12 have "valid ((a,\<tau>1)#(c,\<sigma>)#\<Gamma>)" by (rule typing_valid) |
|
497 |
hence ca: "valid \<Gamma>" and cb: "a\<sharp>\<Gamma>" and cc: "c\<sharp>\<Gamma>" |
|
498 |
by (auto dest: valid_elim simp add: fresh_list_cons) |
|
499 |
from c12 have c14: "((c,\<sigma>)#(a,\<tau>1)#\<Gamma>) \<turnstile> s : \<tau>2" |
|
500 |
proof - |
|
501 |
have c2: "((a,\<tau>1)#(c,\<sigma>)#\<Gamma>) \<lless> ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def) |
|
502 |
have c3: "valid ((c,\<sigma>)#(a,\<tau>1)#\<Gamma>)" |
|
503 |
by (rule v2, rule v2, auto simp add: fresh_list_cons fresh_prod ca cb cc f2' fresh_ty) |
|
504 |
from c12 c2 c3 show ?thesis by (force intro: weakening) |
|
505 |
qed |
|
506 |
assume c8: "\<Gamma> \<turnstile> t2 : \<sigma>" |
|
507 |
have c81: "((a,\<tau>1)#\<Gamma>)\<turnstile>t2 :\<sigma>" |
|
508 |
proof - |
|
509 |
have c82: "\<Gamma> \<lless> ((a,\<tau>1)#\<Gamma>)" by (force simp add: sub_def) |
|
510 |
have c83: "valid ((a,\<tau>1)#\<Gamma>)" using f1 ca by force |
|
511 |
with c8 c82 c83 show ?thesis by (force intro: weakening) |
|
512 |
qed |
|
513 |
show "\<Gamma> \<turnstile> Lam [a].(s[c::=t2]) : \<tau>" |
|
514 |
using c11 Lam c14 c81 f1 by force |
|
515 |
qed |
|
516 |
qed |
|
517 |
||
518 |
lemma subject[rule_format]: |
|
519 |
fixes \<Gamma> ::"(name\<times>ty) list" |
|
520 |
and t1 ::"lam" |
|
521 |
and t2 ::"lam" |
|
522 |
and \<tau> ::"ty" |
|
523 |
assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2" |
|
524 |
shows "(\<Gamma> \<turnstile> t1:\<tau>) \<longrightarrow> (\<Gamma> \<turnstile> t2:\<tau>)" |
|
525 |
using a |
|
526 |
proof (nominal_induct t1 t2 rule: beta_induct, auto) |
|
527 |
case (b1 \<Gamma> \<tau> t s1 s2) |
|
528 |
assume i: "\<forall>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" |
|
529 |
assume "\<Gamma> \<turnstile> App s1 t : \<tau>" |
|
530 |
hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> t : \<sigma>)" by (rule t2_elim) |
|
531 |
then obtain \<sigma> where a1: "\<Gamma> \<turnstile> s1 : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> t : \<sigma>" by force |
|
532 |
thus "\<Gamma> \<turnstile> App s2 t : \<tau>" using i by force |
|
533 |
next |
|
534 |
case (b2 \<Gamma> \<tau> t s1 s2) |
|
535 |
assume i: "\<forall>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" |
|
536 |
assume "\<Gamma> \<turnstile> App t s1 : \<tau>" |
|
537 |
hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s1 : \<sigma>)" by (rule t2_elim) |
|
538 |
then obtain \<sigma> where a1: "\<Gamma> \<turnstile> t : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s1 : \<sigma>" by force |
|
539 |
thus "\<Gamma> \<turnstile> App t s2 : \<tau>" using i by force |
|
540 |
next |
|
541 |
case (b3 \<Gamma> \<tau> a s1 s2) |
|
542 |
assume "a\<sharp>(\<Gamma>,\<tau>)" |
|
543 |
hence f: "a\<sharp>\<Gamma>" by (simp add: fresh_prod) |
|
544 |
assume i: "\<forall>\<Gamma> \<tau>. \<Gamma> \<turnstile> s1 : \<tau> \<longrightarrow> \<Gamma> \<turnstile> s2 : \<tau>" |
|
545 |
assume "\<Gamma> \<turnstile> Lam [a].s1 : \<tau>" |
|
546 |
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) |
|
547 |
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 |
|
548 |
thus "\<Gamma> \<turnstile> Lam [a].s2 : \<tau>" using f i by force |
|
549 |
next |
|
550 |
case (b4 \<Gamma> \<tau> a s1 s2) |
|
551 |
have "a\<sharp>(s2,\<Gamma>,\<tau>)" by fact |
|
552 |
hence f: "a\<sharp>\<Gamma>" by (simp add: fresh_prod) |
|
553 |
assume "\<Gamma> \<turnstile> App (Lam [a].s1) s2 : \<tau>" |
|
554 |
hence "\<exists>\<sigma>. (\<Gamma> \<turnstile> (Lam [a].s1) : \<sigma>\<rightarrow>\<tau> \<and> \<Gamma> \<turnstile> s2 : \<sigma>)" by (rule t2_elim) |
|
555 |
then obtain \<sigma> where a1: "\<Gamma> \<turnstile> (Lam [(a::name)].s1) : \<sigma>\<rightarrow>\<tau>" and a2: "\<Gamma> \<turnstile> s2 : \<sigma>" by force |
|
556 |
have "((a,\<sigma>)#\<Gamma>) \<turnstile> s1 : \<tau>" using a1 f by (auto dest!: t3_elim) |
|
557 |
with a2 show "\<Gamma> \<turnstile> s1[a::=s2] : \<tau>" by (force intro: ty_subs) |
|
558 |
qed |
|
559 |
||
560 |
||
561 |
lemma subject[rule_format]: |
|
562 |
fixes \<Gamma> ::"(name\<times>ty) list" |
|
563 |
and t1 ::"lam" |
|
564 |
and t2 ::"lam" |
|
565 |
and \<tau> ::"ty" |
|
566 |
assumes a: "t1\<longrightarrow>\<^isub>\<beta>t2" |
|
567 |
shows "\<Gamma> \<turnstile> t1:\<tau> \<longrightarrow> \<Gamma> \<turnstile> t2:\<tau>" |
|
568 |
using a |
|
569 |
apply(nominal_induct t1 t2 rule: beta_induct) |
|
570 |
apply(auto dest!: t2_elim t3_elim intro: ty_subs simp add: fresh_prod) |
|
571 |
done |
|
572 |
||
573 |
||
574 |
||
575 |
subsection {* some facts about beta *} |
|
576 |
||
577 |
constdefs |
|
578 |
"NORMAL" :: "lam \<Rightarrow> bool" |
|
579 |
"NORMAL t \<equiv> \<not>(\<exists>t'. t\<longrightarrow>\<^isub>\<beta> t')" |
|
580 |
||
581 |
constdefs |
|
582 |
"SN" :: "lam \<Rightarrow> bool" |
|
583 |
"SN t \<equiv> t\<in>termi Beta" |
|
584 |
||
585 |
lemma qq1: "\<lbrakk>SN(t1);t1\<longrightarrow>\<^isub>\<beta> t2\<rbrakk>\<Longrightarrow>SN(t2)" |
|
586 |
apply(simp add: SN_def) |
|
587 |
apply(drule_tac a="t2" in acc_downward) |
|
588 |
apply(auto) |
|
589 |
done |
|
590 |
||
591 |
lemma qq2: "(\<forall>t2. t1\<longrightarrow>\<^isub>\<beta>t2 \<longrightarrow> SN(t2))\<Longrightarrow>SN(t1)" |
|
592 |
apply(simp add: SN_def) |
|
593 |
apply(rule accI) |
|
594 |
apply(auto) |
|
595 |
done |
|
596 |
||
597 |
||
598 |
section {* Candidates *} |
|
599 |
||
600 |
consts |
|
601 |
RED :: "ty \<Rightarrow> lam set" |
|
602 |
primrec |
|
603 |
"RED (TVar X) = {t. SN(t)}" |
|
604 |
"RED (\<tau>\<rightarrow>\<sigma>) = {t. \<forall>u. (u\<in>RED \<tau> \<longrightarrow> (App t u)\<in>RED \<sigma>)}" |
|
605 |
||
606 |
constdefs |
|
607 |
NEUT :: "lam \<Rightarrow> bool" |
|
608 |
"NEUT t \<equiv> (\<exists>a. t=Var a)\<or>(\<exists>t1 t2. t=App t1 t2)" |
|
609 |
||
610 |
(* a slight hack to get the first element of applications *) |
|
611 |
consts |
|
612 |
FST :: "(lam\<times>lam) set" |
|
613 |
syntax |
|
614 |
"FST_judge" :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<guillemotright> _" [80,80] 80) |
|
615 |
translations |
|
616 |
"t1 \<guillemotright> t2" \<rightleftharpoons> "(t1,t2) \<in> FST" |
|
617 |
inductive FST |
|
618 |
intros |
|
619 |
fst[intro!]: "(App t s) \<guillemotright> t" |
|
620 |
||
621 |
lemma fst_elim[elim!]: "(App t s) \<guillemotright> t' \<Longrightarrow> t=t'" |
|
622 |
apply(ind_cases "App t s \<guillemotright> t'") |
|
623 |
apply(simp add: lam.inject) |
|
624 |
done |
|
625 |
||
626 |
lemma qq3: "SN(App t s)\<Longrightarrow>SN(t)" |
|
627 |
apply(simp add: SN_def) |
|
628 |
apply(subgoal_tac "\<forall>z. (App t s \<guillemotright> z) \<longrightarrow> z\<in>termi Beta")(*A*) |
|
629 |
apply(force) |
|
630 |
(*A*) |
|
631 |
apply(erule acc_induct) |
|
632 |
apply(clarify) |
|
633 |
apply(ind_cases "x \<guillemotright> z") |
|
634 |
apply(clarify) |
|
635 |
apply(rule accI) |
|
636 |
apply(auto intro: b1) |
|
637 |
done |
|
638 |
||
639 |
constdefs |
|
640 |
"CR1" :: "ty \<Rightarrow> bool" |
|
641 |
"CR1 \<tau> \<equiv> \<forall> t. (t\<in>RED \<tau> \<longrightarrow> SN(t))" |
|
642 |
||
643 |
"CR2" :: "ty \<Rightarrow> bool" |
|
644 |
"CR2 \<tau> \<equiv> \<forall>t t'. ((t\<in>RED \<tau> \<and> t \<longrightarrow>\<^isub>\<beta> t') \<longrightarrow> t'\<in>RED \<tau>)" |
|
645 |
||
646 |
"CR3_RED" :: "lam \<Rightarrow> ty \<Rightarrow> bool" |
|
647 |
"CR3_RED t \<tau> \<equiv> \<forall>t'. (t\<longrightarrow>\<^isub>\<beta> t' \<longrightarrow> t'\<in>RED \<tau>)" |
|
648 |
||
649 |
"CR3" :: "ty \<Rightarrow> bool" |
|
650 |
"CR3 \<tau> \<equiv> \<forall>t. (NEUT t \<and> CR3_RED t \<tau>) \<longrightarrow> t\<in>RED \<tau>" |
|
651 |
||
652 |
"CR4" :: "ty \<Rightarrow> bool" |
|
653 |
"CR4 \<tau> \<equiv> \<forall>t. (NEUT t \<and> NORMAL t) \<longrightarrow>t\<in>RED \<tau>" |
|
654 |
||
655 |
lemma CR3_CR4: "CR3 \<tau> \<Longrightarrow> CR4 \<tau>" |
|
656 |
apply(simp (no_asm_use) add: CR3_def CR3_RED_def CR4_def NORMAL_def) |
|
657 |
apply(blast) |
|
658 |
done |
|
659 |
||
660 |
lemma sub_ind: |
|
661 |
"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>))" |
|
662 |
apply(simp add: SN_def) |
|
663 |
apply(erule acc_induct) |
|
664 |
apply(auto) |
|
665 |
apply(simp add: CR3_def) |
|
666 |
apply(rotate_tac 5) |
|
667 |
apply(drule_tac x="App t x" in spec) |
|
668 |
apply(drule mp) |
|
669 |
apply(rule conjI) |
|
670 |
apply(force simp only: NEUT_def) |
|
671 |
apply(simp (no_asm) add: CR3_RED_def) |
|
672 |
apply(clarify) |
|
673 |
apply(ind_cases "App t x \<longrightarrow>\<^isub>\<beta> t'") |
|
674 |
apply(simp_all add: lam.inject) |
|
675 |
apply(simp only: CR3_RED_def) |
|
676 |
apply(drule_tac x="s2" in spec) |
|
677 |
apply(simp) |
|
678 |
apply(drule_tac x="s2" in spec) |
|
679 |
apply(simp) |
|
680 |
apply(drule mp) |
|
681 |
apply(simp (no_asm_use) add: CR2_def) |
|
682 |
apply(blast) |
|
683 |
apply(drule_tac x="ta" in spec) |
|
684 |
apply(force) |
|
685 |
apply(auto simp only: NEUT_def lam.inject lam.distinct) |
|
686 |
done |
|
687 |
||
688 |
lemma RED_props: "CR1 \<tau> \<and> CR2 \<tau> \<and> CR3 \<tau>" |
|
689 |
apply(induct_tac \<tau>) |
|
690 |
apply(auto) |
|
691 |
(* atom types *) |
|
692 |
(* C1 *) |
|
693 |
apply(simp add: CR1_def) |
|
694 |
(* C2 *) |
|
695 |
apply(simp add: CR2_def) |
|
696 |
apply(clarify) |
|
697 |
apply(drule_tac ?t2.0="t'" in qq1) |
|
698 |
apply(assumption)+ |
|
699 |
(* C3 *) |
|
700 |
apply(simp add: CR3_def CR3_RED_def) |
|
701 |
apply(clarify) |
|
702 |
apply(rule qq2) |
|
703 |
apply(assumption) |
|
704 |
(* arrow types *) |
|
705 |
(* C1 *) |
|
706 |
apply(simp (no_asm) add: CR1_def) |
|
707 |
apply(clarify) |
|
708 |
apply(subgoal_tac "NEUT (Var a)")(*A*) |
|
709 |
apply(subgoal_tac "(Var a)\<in>RED ty1")(*C*) |
|
710 |
apply(drule_tac x="Var a" in spec) |
|
711 |
apply(simp) |
|
712 |
apply(simp add: CR1_def) |
|
713 |
apply(rotate_tac 1) |
|
714 |
apply(drule_tac x="App t (Var a)" in spec) |
|
715 |
apply(simp) |
|
716 |
apply(drule qq3) |
|
717 |
apply(assumption) |
|
718 |
(*C*) |
|
719 |
apply(simp (no_asm_use) add: CR3_def CR3_RED_def) |
|
720 |
apply(drule_tac x="Var a" in spec) |
|
721 |
apply(drule mp) |
|
722 |
apply(clarify) |
|
723 |
apply(ind_cases " Var a \<longrightarrow>\<^isub>\<beta> t'") |
|
724 |
apply(simp (no_asm_use) add: lam.distinct)+ |
|
725 |
(*A*) |
|
726 |
apply(simp (no_asm) only: NEUT_def) |
|
727 |
apply(rule disjCI) |
|
728 |
apply(rule_tac x="a" in exI) |
|
729 |
apply(simp (no_asm)) |
|
730 |
(* C2 *) |
|
731 |
apply(simp (no_asm) add: CR2_def) |
|
732 |
apply(clarify) |
|
733 |
apply(drule_tac x="u" in spec) |
|
734 |
apply(simp) |
|
735 |
apply(subgoal_tac "App t u \<longrightarrow>\<^isub>\<beta> App t' u")(*X*) |
|
736 |
apply(simp (no_asm_use) only: CR2_def) |
|
737 |
apply(blast) |
|
738 |
(*X*) |
|
739 |
apply(force intro!: b1) |
|
740 |
(* C3 *) |
|
741 |
apply(unfold CR3_def) |
|
742 |
apply(rule allI) |
|
743 |
apply(rule impI) |
|
744 |
apply(erule conjE) |
|
745 |
apply(simp (no_asm)) |
|
746 |
apply(rule allI) |
|
747 |
apply(rule impI) |
|
748 |
apply(subgoal_tac "SN(u)")(*Z*) |
|
749 |
apply(fold CR3_def) |
|
750 |
apply(drule_tac \<tau>="ty1" and \<sigma>="ty2" in sub_ind) |
|
751 |
apply(simp) |
|
752 |
(*Z*) |
|
753 |
apply(simp add: CR1_def) |
|
754 |
done |
|
755 |
||
756 |
lemma double_acc_aux: |
|
757 |
assumes a_acc: "a \<in> acc r" |
|
758 |
and b_acc: "b \<in> acc r" |
|
759 |
and hyp: "\<And>x z. |
|
760 |
(\<And>y. (y, x) \<in> r \<Longrightarrow> y \<in> acc r) \<Longrightarrow> |
|
761 |
(\<And>y. (y, x) \<in> r \<Longrightarrow> P y z) \<Longrightarrow> |
|
762 |
(\<And>u. (u, z) \<in> r \<Longrightarrow> u \<in> acc r) \<Longrightarrow> |
|
763 |
(\<And>u. (u, z) \<in> r \<Longrightarrow> P x u) \<Longrightarrow> P x z" |
|
764 |
shows "P a b" |
|
765 |
proof - |
|
766 |
from a_acc |
|
767 |
have r: "\<And>b. b \<in> acc r \<Longrightarrow> P a b" |
|
768 |
proof (induct a rule: acc.induct) |
|
769 |
case (accI x) |
|
770 |
note accI' = accI |
|
771 |
have "b \<in> acc r" . |
|
772 |
thus ?case |
|
773 |
proof (induct b rule: acc.induct) |
|
774 |
case (accI y) |
|
775 |
show ?case |
|
776 |
apply (rule hyp) |
|
777 |
apply (erule accI') |
|
778 |
apply (erule accI') |
|
779 |
apply (rule acc.accI) |
|
780 |
apply (erule accI) |
|
781 |
apply (erule accI) |
|
782 |
apply (erule accI) |
|
783 |
done |
|
784 |
qed |
|
785 |
qed |
|
786 |
from b_acc show ?thesis by (rule r) |
|
787 |
qed |
|
788 |
||
789 |
lemma double_acc: |
|
790 |
"\<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" |
|
791 |
apply(rule_tac r="r" in double_acc_aux) |
|
792 |
apply(assumption)+ |
|
793 |
apply(blast) |
|
794 |
done |
|
795 |
||
18263
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
796 |
lemma abs_RED: "(\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>)\<longrightarrow>Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)" |
18106 | 797 |
apply(simp) |
798 |
apply(clarify) |
|
799 |
apply(subgoal_tac "t\<in>termi Beta")(*1*) |
|
800 |
apply(erule rev_mp) |
|
801 |
apply(subgoal_tac "u \<in> RED \<tau>")(*A*) |
|
802 |
apply(erule rev_mp) |
|
803 |
apply(rule_tac a="t" and b="u" in double_acc) |
|
804 |
apply(assumption) |
|
805 |
apply(subgoal_tac "CR1 \<tau>")(*A*) |
|
806 |
apply(simp add: CR1_def SN_def) |
|
807 |
(*A*) |
|
808 |
apply(force simp add: RED_props) |
|
809 |
apply(simp) |
|
810 |
apply(clarify) |
|
811 |
apply(subgoal_tac "CR3 \<sigma>")(*B*) |
|
812 |
apply(simp add: CR3_def) |
|
813 |
apply(rotate_tac 6) |
|
814 |
apply(drule_tac x="App(Lam[x].xa ) z" in spec) |
|
815 |
apply(drule mp) |
|
816 |
apply(rule conjI) |
|
817 |
apply(force simp add: NEUT_def) |
|
818 |
apply(simp add: CR3_RED_def) |
|
819 |
apply(clarify) |
|
820 |
apply(ind_cases "App(Lam[x].xa) z \<longrightarrow>\<^isub>\<beta> t'") |
|
821 |
apply(auto simp add: lam.inject lam.distinct) |
|
822 |
apply(drule beta_abs) |
|
823 |
apply(auto) |
|
824 |
apply(drule_tac x="t''" in spec) |
|
825 |
apply(simp) |
|
826 |
apply(drule mp) |
|
827 |
apply(clarify) |
|
828 |
apply(drule_tac x="s" in bspec) |
|
829 |
apply(assumption) |
|
830 |
apply(subgoal_tac "xa [ x ::= s ] \<longrightarrow>\<^isub>\<beta> t'' [ x ::= s ]")(*B*) |
|
831 |
apply(subgoal_tac "CR2 \<sigma>")(*C*) |
|
832 |
apply(simp (no_asm_use) add: CR2_def) |
|
833 |
apply(blast) |
|
834 |
(*C*) |
|
835 |
apply(force simp add: RED_props) |
|
836 |
(*B*) |
|
837 |
apply(force intro!: beta_subst) |
|
838 |
apply(assumption) |
|
839 |
apply(rotate_tac 3) |
|
840 |
apply(drule_tac x="s2" in spec) |
|
841 |
apply(subgoal_tac "s2\<in>RED \<tau>")(*D*) |
|
842 |
apply(simp) |
|
843 |
(*D*) |
|
844 |
apply(subgoal_tac "CR2 \<tau>")(*E*) |
|
845 |
apply(simp (no_asm_use) add: CR2_def) |
|
846 |
apply(blast) |
|
847 |
(*E*) |
|
848 |
apply(force simp add: RED_props) |
|
849 |
apply(simp add: alpha) |
|
850 |
apply(erule disjE) |
|
851 |
apply(force) |
|
852 |
apply(auto) |
|
853 |
apply(simp add: subst_rename) |
|
854 |
apply(drule_tac x="z" in bspec) |
|
855 |
apply(assumption) |
|
856 |
(*B*) |
|
857 |
apply(force simp add: RED_props) |
|
858 |
(*1*) |
|
859 |
apply(drule_tac x="Var x" in bspec) |
|
860 |
apply(subgoal_tac "CR3 \<tau>")(*2*) |
|
861 |
apply(drule CR3_CR4) |
|
862 |
apply(simp add: CR4_def) |
|
863 |
apply(drule_tac x="Var x" in spec) |
|
864 |
apply(drule mp) |
|
865 |
apply(rule conjI) |
|
866 |
apply(force simp add: NEUT_def) |
|
867 |
apply(simp add: NORMAL_def) |
|
868 |
apply(clarify) |
|
869 |
apply(ind_cases "Var x \<longrightarrow>\<^isub>\<beta> t'") |
|
870 |
apply(auto simp add: lam.inject lam.distinct) |
|
871 |
apply(force simp add: RED_props) |
|
872 |
apply(simp add: id_subs) |
|
873 |
apply(subgoal_tac "CR1 \<sigma>")(*3*) |
|
874 |
apply(simp add: CR1_def SN_def) |
|
875 |
(*3*) |
|
876 |
apply(force simp add: RED_props) |
|
877 |
done |
|
878 |
||
18263
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
879 |
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
|
880 |
apply(induct_tac \<theta>) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
881 |
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
|
882 |
done |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
883 |
|
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
884 |
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
|
885 |
apply(induct_tac \<theta>) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
886 |
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
|
887 |
done |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
888 |
|
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
889 |
lemma psubs_subs[rule_format]: "c\<sharp>\<theta>\<longrightarrow> (t[<\<theta>>])[c::=s] = t[<((c,s)#\<theta>)>]" |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
890 |
apply(nominal_induct t rule: lam_induct) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
891 |
apply(auto dest: fresh_domain) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
892 |
apply(drule fresh_at) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
893 |
apply(assumption) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
894 |
apply(rule forget) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
895 |
apply(assumption) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
896 |
apply(subgoal_tac "ab\<sharp>((aa,b)#a)")(*A*) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
897 |
apply(simp add: fresh_prod) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
898 |
(*A*) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
899 |
apply(simp add: fresh_list_cons fresh_prod) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
900 |
done |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
901 |
|
18106 | 902 |
lemma all_RED: |
18263
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
903 |
"\<Gamma>\<turnstile>t:\<tau> \<longrightarrow> (\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>)\<longrightarrow>(a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)) \<longrightarrow> (t[<\<theta>>]\<in>RED \<tau>)" |
18106 | 904 |
apply(nominal_induct t rule: lam_induct) |
905 |
(* Variables *) |
|
906 |
apply(force dest: t1_elim) |
|
907 |
(* Applications *) |
|
18263
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
908 |
apply(clarify) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
909 |
apply(drule t2_elim) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
910 |
apply(erule exE, erule conjE) |
18106 | 911 |
apply(drule_tac x="a" in spec) |
912 |
apply(drule_tac x="a" in spec) |
|
913 |
apply(drule_tac x="\<tau>\<rightarrow>aa" in spec) |
|
914 |
apply(drule_tac x="\<tau>" in spec) |
|
915 |
apply(drule_tac x="b" in spec) |
|
916 |
apply(drule_tac x="b" in spec) |
|
917 |
apply(force) |
|
918 |
(* Abstractions *) |
|
18263
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
919 |
apply(clarify) |
18106 | 920 |
apply(drule t3_elim) |
921 |
apply(simp add: fresh_prod) |
|
18263
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
922 |
apply(erule exE)+ |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
923 |
apply(erule conjE) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
924 |
apply(simp only: fresh_prod psubst_Lam) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
925 |
apply(rule abs_RED[THEN mp]) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
926 |
apply(clarify) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
927 |
apply(drule_tac x="(ab,\<tau>)#a" in spec) |
18106 | 928 |
apply(drule_tac x="\<tau>'" in spec) |
18263
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
929 |
apply(drule_tac x="(ab,s)#b" in spec) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
930 |
apply(simp (no_asm_use)) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
931 |
apply(simp add: split_if) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
932 |
apply(auto) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
933 |
apply(drule fresh_context) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
934 |
apply(simp) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
935 |
apply(simp add: psubs_subs) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
936 |
done |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
937 |
|
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
938 |
lemma all_RED: |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
939 |
"\<Gamma>\<turnstile>t:\<tau> \<longrightarrow> (\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>)\<longrightarrow>(a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)) \<longrightarrow> (t[<\<theta>>]\<in>RED \<tau>)" |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
940 |
apply(nominal_induct t rule: lam_induct) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
941 |
(* Variables *) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
942 |
apply(force dest: t1_elim) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
943 |
(* Applications *) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
944 |
apply(force dest!: t2_elim) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
945 |
(* Abstractions *) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
946 |
apply(auto dest!: t3_elim simp only:) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
947 |
apply(simp add: fresh_prod) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
948 |
apply(simp only: fresh_prod psubst_Lam) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
949 |
apply(rule abs_RED[THEN mp]) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
950 |
apply(force dest: fresh_context simp add: psubs_subs) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
951 |
done |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
952 |
|
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
953 |
lemma all_RED: |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
954 |
"\<Gamma>\<turnstile>t:\<tau> \<longrightarrow> (\<forall>a \<sigma>. (a,\<sigma>)\<in>set(\<Gamma>)\<longrightarrow>(a\<in>set(domain \<theta>)\<and>\<theta><a>\<in>RED \<sigma>)) \<longrightarrow> (t[<\<theta>>]\<in>RED \<tau>)" |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
955 |
proof(nominal_induct t rule: lam_induct) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
956 |
case Var |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
957 |
show ?case by (force dest: t1_elim) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
958 |
next |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
959 |
case App |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
960 |
thus ?case by (force dest!: t2_elim) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
961 |
(* HERE *) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
962 |
next |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
963 |
case (Lam \<Gamma> \<tau> \<theta> a t) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
964 |
have ih: |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
965 |
"\<forall>\<Gamma> \<tau> \<theta>. (\<forall>\<sigma> c. (c,\<sigma>)\<in>set \<Gamma> \<longrightarrow> c\<in>set (domain \<theta>) \<and> \<theta><c>\<in>RED \<sigma>) \<and> \<Gamma> \<turnstile> t : \<tau> \<longrightarrow> t[<\<theta>>]\<in>RED \<tau>" |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
966 |
by fact |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
967 |
have "a\<sharp>(\<Gamma>,\<tau>,\<theta>)" by fact |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
968 |
hence b1: "a\<sharp>\<Gamma>" and b2: "a\<sharp>\<tau>" and b3: "a\<sharp>\<theta>" by (simp_all add: fresh_prod) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
969 |
from b1 have c1: "\<not>(\<exists>\<tau>. (a,\<tau>)\<in>set \<Gamma>)" by (rule fresh_context) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
970 |
show ?case using b1 |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
971 |
proof (auto dest!: t3_elim simp only: psubst_Lam) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
972 |
fix \<sigma>1::"ty" and \<sigma>2::"ty" |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
973 |
assume a1: "((a,\<sigma>1)#\<Gamma>) \<turnstile> t : \<sigma>2" |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
974 |
and a3: "\<forall>(\<sigma>\<Colon>ty) (c\<Colon>name). (c,\<sigma>) \<in> set \<Gamma> \<longrightarrow> c \<in> set (domain \<theta>) \<and> \<theta> <c> \<in> RED \<sigma>" |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
975 |
have "\<forall>s\<in>RED \<sigma>1. (t[<\<theta>>])[a::=s]\<in>RED \<sigma>2" |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
976 |
proof |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
977 |
(* HERE *) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
978 |
|
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
979 |
fix s::"lam" |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
980 |
assume a4: "s \<in> RED \<sigma>1" |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
981 |
from ih have "\<forall>\<sigma> c. (c,\<sigma>)\<in>set ((a,\<sigma>1)#\<Gamma>) \<longrightarrow> c\<in>set (domain ((c,s)#\<theta>)) \<and> (((c,s)#\<theta>)<c>)\<in>RED \<sigma>" |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
982 |
using c1 a4 proof (auto) |
18106 | 983 |
apply(simp) |
18263
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
984 |
apply(rule allI)+ |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
985 |
apply(rule conjI) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
986 |
|
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
987 |
proof (auto) *) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
988 |
have "(((a,\<sigma>1)#\<Gamma>) \<turnstile> t : \<sigma>2) \<longrightarrow> t[<((a,s)#\<theta>)>] \<in> RED \<sigma>2" using Lam a3 b3 |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
989 |
proof(blast dest: fresh_context) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
990 |
|
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
991 |
show "(t[<\<theta>>])[a::=s] \<in> RED \<sigma>2" |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
992 |
|
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
993 |
qed |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
994 |
thus "Lam [a].(t[<\<theta>>]) \<in> RED (\<sigma>1\<rightarrow>\<sigma>2)" by (simp only: abs_RED) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
995 |
qed |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
996 |
qed |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
997 |
|
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
998 |
|
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
999 |
|
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1000 |
|
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1001 |
|
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1002 |
have "(((a,\<sigma>1)#\<Gamma>) \<turnstile> t : \<sigma>2) \<longrightarrow> t[<((a,u)#\<theta>)>] \<in> RED \<sigma>2" using Lam a3 sorry |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1003 |
hence "t[<((a,u)#\<theta>)>] \<in> RED \<sigma>2" using a1 by simp |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1004 |
hence "t[<\<theta>>][a::=u] \<in> RED \<sigma>2" using b3 by (simp add: psubs_subs) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1005 |
show "Lam [a].(t[<\<theta>>]) \<in> RED (\<sigma>1\<rightarrow>\<sigma>2)" |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1006 |
hence "Lam [a].(t[<\<theta>>]) \<in> RED (\<tau>\<rightarrow>\<sigma>)" using a2 abs_RED by force |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1007 |
show "App (Lam [a].(t[<\<theta>>])) u \<in> RED \<sigma>2" |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1008 |
|
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1009 |
|
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1010 |
|
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1011 |
thus ?case using t2_elim |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1012 |
proof(auto, blast) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1013 |
|
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1014 |
qed |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1015 |
|
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1016 |
(* Variables *) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1017 |
apply(force dest: t1_elim) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1018 |
(* Applications *) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1019 |
apply(clarify) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1020 |
apply(drule t2_elim) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1021 |
apply(erule exE, erule conjE) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1022 |
apply(drule_tac x="a" in spec) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1023 |
apply(drule_tac x="a" in spec) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1024 |
apply(drule_tac x="\<tau>\<rightarrow>aa" in spec) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1025 |
apply(drule_tac x="\<tau>" in spec) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1026 |
apply(drule_tac x="b" in spec) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1027 |
apply(drule_tac x="b" in spec) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1028 |
apply(force) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1029 |
(* Abstractions *) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1030 |
apply(clarify) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1031 |
apply(drule t3_elim) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1032 |
apply(simp add: fresh_prod) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1033 |
apply(erule exE)+ |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1034 |
apply(erule conjE) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1035 |
apply(simp only: fresh_prod psubst_Lam) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1036 |
apply(rule abs_RED) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1037 |
apply(auto) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1038 |
apply(drule_tac x="(ab,\<tau>)#a" in spec) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1039 |
apply(drule_tac x="\<tau>'" in spec) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1040 |
apply(drule_tac x="(ab,s)#b" in spec) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1041 |
apply(simp) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1042 |
apply(auto) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1043 |
apply(drule fresh_context) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1044 |
apply(simp) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1045 |
apply(simp add: psubs_subs) |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1046 |
done |
7f75925498da
cleaned up all examples so that they work with the
urbanc
parents:
18106
diff
changeset
|
1047 |
|
18106 | 1048 |
|
1049 |
||
1050 |
done |
|
1051 |