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