author | urbanc |
Fri, 04 Jan 2008 09:34:11 +0100 | |
changeset 25831 | 7711d60a5293 |
parent 24899 | 08865bb87098 |
child 25867 | c24395ea4e71 |
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 |
||
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
11 |
lemma subst_rename: |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
12 |
assumes a: "c\<sharp>t1" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
13 |
shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
14 |
using a |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
15 |
by (nominal_induct t1 avoiding: a c t2 rule: lam.induct) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
16 |
(auto simp add: calc_atm fresh_atm abs_fresh) |
18106 | 17 |
|
18313 | 18 |
lemma forget: |
19 |
assumes a: "a\<sharp>t1" |
|
20 |
shows "t1[a::=t2] = t1" |
|
21 |
using a |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
22 |
by (nominal_induct t1 avoiding: a t2 rule: lam.induct) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
23 |
(auto simp add: abs_fresh fresh_atm) |
18106 | 24 |
|
18313 | 25 |
lemma fresh_fact: |
26 |
fixes a::"name" |
|
23970 | 27 |
assumes a: "a\<sharp>t1" "a\<sharp>t2" |
22540 | 28 |
shows "a\<sharp>t1[b::=t2]" |
23970 | 29 |
using a |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
30 |
by (nominal_induct t1 avoiding: a b t2 rule: lam.induct) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
31 |
(auto simp add: abs_fresh fresh_atm) |
18106 | 32 |
|
22540 | 33 |
lemma fresh_fact': |
34 |
fixes a::"name" |
|
35 |
assumes a: "a\<sharp>t2" |
|
36 |
shows "a\<sharp>t1[a::=t2]" |
|
37 |
using a |
|
38 |
by (nominal_induct t1 avoiding: a t2 rule: lam.induct) |
|
39 |
(auto simp add: abs_fresh fresh_atm) |
|
40 |
||
18383 | 41 |
lemma subst_lemma: |
18313 | 42 |
assumes a: "x\<noteq>y" |
43 |
and b: "x\<sharp>L" |
|
44 |
shows "M[x::=N][y::=L] = M[y::=L][x::=N[y::=L]]" |
|
45 |
using a b |
|
18659
2ff0ae57431d
changes to make use of the new induction principle proved by
urbanc
parents:
18654
diff
changeset
|
46 |
by (nominal_induct M avoiding: x y N L rule: lam.induct) |
18313 | 47 |
(auto simp add: fresh_fact forget) |
18106 | 48 |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
49 |
lemma id_subs: |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
50 |
shows "t[x::=Var x] = t" |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
51 |
by (nominal_induct t avoiding: x rule: lam.induct) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
52 |
(simp_all add: fresh_atm) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
53 |
|
23142 | 54 |
lemma psubst_subst: |
55 |
assumes h:"c\<sharp>\<theta>" |
|
56 |
shows "(\<theta><t>)[c::=s] = ((c,s)#\<theta>)<t>" |
|
57 |
using h |
|
58 |
by (nominal_induct t avoiding: \<theta> c s rule: lam.induct) |
|
59 |
(auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh') |
|
60 |
||
23760 | 61 |
inductive |
23142 | 62 |
Beta :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<longrightarrow>\<^isub>\<beta> _" [80,80] 80) |
22271 | 63 |
where |
23970 | 64 |
b1[intro!]: "s1 \<longrightarrow>\<^isub>\<beta> s2 \<Longrightarrow> App s1 t \<longrightarrow>\<^isub>\<beta> App s2 t" |
65 |
| b2[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> App t s1 \<longrightarrow>\<^isub>\<beta> App t s2" |
|
66 |
| b3[intro!]: "s1\<longrightarrow>\<^isub>\<beta>s2 \<Longrightarrow> Lam [a].s1 \<longrightarrow>\<^isub>\<beta> Lam [a].s2" |
|
67 |
| b4[intro!]: "a\<sharp>s2 \<Longrightarrow> App (Lam [a].s1) s2\<longrightarrow>\<^isub>\<beta> (s1[a::=s2])" |
|
22538
3ccb92dfb5e9
tuned proofs (taking full advantage of nominal_inductive)
urbanc
parents:
22531
diff
changeset
|
68 |
|
22730
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22650
diff
changeset
|
69 |
equivariance Beta |
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22650
diff
changeset
|
70 |
|
22538
3ccb92dfb5e9
tuned proofs (taking full advantage of nominal_inductive)
urbanc
parents:
22531
diff
changeset
|
71 |
nominal_inductive Beta |
22540 | 72 |
by (simp_all add: abs_fresh fresh_fact') |
18106 | 73 |
|
25831 | 74 |
lemma beta_preserves_fresh: |
75 |
fixes a::"name" |
|
18378 | 76 |
assumes a: "t\<longrightarrow>\<^isub>\<beta> s" |
25831 | 77 |
shows "a\<sharp>t \<Longrightarrow> a\<sharp>s" |
18378 | 78 |
using a |
25831 | 79 |
apply(nominal_induct t s avoiding: a rule: Beta.strong_induct) |
80 |
apply(auto simp add: abs_fresh fresh_fact fresh_atm) |
|
81 |
done |
|
18378 | 82 |
|
23970 | 83 |
lemma beta_abs: |
25831 | 84 |
assumes a: "Lam [a].t\<longrightarrow>\<^isub>\<beta> t'" |
23970 | 85 |
shows "\<exists>t''. t'=Lam [a].t'' \<and> t\<longrightarrow>\<^isub>\<beta> t''" |
25831 | 86 |
proof - |
87 |
have "a\<sharp>Lam [a].t" by (simp add: abs_fresh) |
|
88 |
with a have "a\<sharp>t'" by (simp add: beta_preserves_fresh) |
|
89 |
with a show ?thesis |
|
90 |
by (cases rule: Beta.strong_cases[where a="a" and aa="a"]) |
|
91 |
(auto simp add: lam.inject abs_fresh alpha) |
|
92 |
qed |
|
18106 | 93 |
|
18313 | 94 |
lemma beta_subst: |
18106 | 95 |
assumes a: "M \<longrightarrow>\<^isub>\<beta> M'" |
96 |
shows "M[x::=N]\<longrightarrow>\<^isub>\<beta> M'[x::=N]" |
|
97 |
using a |
|
23142 | 98 |
by (nominal_induct M M' avoiding: x N rule: Beta.strong_induct) |
99 |
(auto simp add: fresh_atm subst_lemma fresh_fact) |
|
18106 | 100 |
|
18383 | 101 |
section {* types *} |
102 |
||
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
103 |
nominal_datatype ty = |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
104 |
TVar "nat" |
18106 | 105 |
| TArr "ty" "ty" (infix "\<rightarrow>" 200) |
106 |
||
23142 | 107 |
lemma perm_ty: |
18106 | 108 |
fixes pi ::"name prm" |
109 |
and \<tau> ::"ty" |
|
110 |
shows "pi\<bullet>\<tau> = \<tau>" |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
111 |
by (nominal_induct \<tau> rule: ty.induct) |
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
112 |
(simp_all add: perm_nat_def) |
18106 | 113 |
|
114 |
lemma fresh_ty: |
|
115 |
fixes a ::"name" |
|
116 |
and \<tau> ::"ty" |
|
117 |
shows "a\<sharp>\<tau>" |
|
23142 | 118 |
by (simp add: fresh_def perm_ty supp_def) |
119 |
||
120 |
(* domain of a typing context *) |
|
121 |
||
122 |
fun |
|
123 |
"dom_ty" :: "(name\<times>ty) list \<Rightarrow> (name list)" |
|
124 |
where |
|
125 |
"dom_ty [] = []" |
|
126 |
| "dom_ty ((x,\<tau>)#\<Gamma>) = (x)#(dom_ty \<Gamma>)" |
|
127 |
||
18106 | 128 |
|
129 |
(* valid contexts *) |
|
130 |
||
23760 | 131 |
inductive |
23142 | 132 |
valid :: "(name\<times>ty) list \<Rightarrow> bool" |
22271 | 133 |
where |
134 |
v1[intro]: "valid []" |
|
135 |
| v2[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk>\<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" |
|
18106 | 136 |
|
22538
3ccb92dfb5e9
tuned proofs (taking full advantage of nominal_inductive)
urbanc
parents:
22531
diff
changeset
|
137 |
equivariance valid |
18106 | 138 |
|
23760 | 139 |
inductive_cases valid_elim[elim]: "valid ((a,\<tau>)#\<Gamma>)" |
23142 | 140 |
|
18106 | 141 |
(* typing judgements *) |
142 |
||
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
143 |
lemma fresh_context: |
18106 | 144 |
fixes \<Gamma> :: "(name\<times>ty)list" |
145 |
and a :: "name" |
|
18378 | 146 |
assumes a: "a\<sharp>\<Gamma>" |
147 |
shows "\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)" |
|
148 |
using a |
|
23970 | 149 |
by (induct \<Gamma>) |
150 |
(auto simp add: fresh_prod fresh_list_cons fresh_atm) |
|
18106 | 151 |
|
23760 | 152 |
inductive |
23142 | 153 |
typing :: "(name\<times>ty) list\<Rightarrow>lam\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ : _" [60,60,60] 60) |
22271 | 154 |
where |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22542
diff
changeset
|
155 |
t1[intro]: "\<lbrakk>valid \<Gamma>; (a,\<tau>)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var a : \<tau>" |
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22542
diff
changeset
|
156 |
| t2[intro]: "\<lbrakk>\<Gamma> \<turnstile> t1 : \<tau>\<rightarrow>\<sigma>; \<Gamma> \<turnstile> t2 : \<tau>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App t1 t2 : \<sigma>" |
22271 | 157 |
| t3[intro]: "\<lbrakk>a\<sharp>\<Gamma>;((a,\<tau>)#\<Gamma>) \<turnstile> t : \<sigma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [a].t : \<tau>\<rightarrow>\<sigma>" |
18106 | 158 |
|
22730
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22650
diff
changeset
|
159 |
equivariance typing |
8bcc8809ed3b
nominal_inductive no longer proves equivariance.
berghofe
parents:
22650
diff
changeset
|
160 |
|
22538
3ccb92dfb5e9
tuned proofs (taking full advantage of nominal_inductive)
urbanc
parents:
22531
diff
changeset
|
161 |
nominal_inductive typing |
3ccb92dfb5e9
tuned proofs (taking full advantage of nominal_inductive)
urbanc
parents:
22531
diff
changeset
|
162 |
by (simp_all add: abs_fresh fresh_ty) |
18106 | 163 |
|
21107
e69c0e82955a
new file for defining functions in the lambda-calculus
urbanc
parents:
19972
diff
changeset
|
164 |
abbreviation |
22650
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22542
diff
changeset
|
165 |
"sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" ("_ \<subseteq> _" [60,60] 60) |
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22542
diff
changeset
|
166 |
where |
0c5b22076fb3
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
urbanc
parents:
22542
diff
changeset
|
167 |
"\<Gamma>1 \<subseteq> \<Gamma>2 \<equiv> \<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow> (a,\<sigma>)\<in>set \<Gamma>2" |
18106 | 168 |
|
169 |
subsection {* some facts about beta *} |
|
170 |
||
171 |
constdefs |
|
172 |
"NORMAL" :: "lam \<Rightarrow> bool" |
|
173 |
"NORMAL t \<equiv> \<not>(\<exists>t'. t\<longrightarrow>\<^isub>\<beta> t')" |
|
174 |
||
18383 | 175 |
lemma NORMAL_Var: |
176 |
shows "NORMAL (Var a)" |
|
177 |
proof - |
|
178 |
{ assume "\<exists>t'. (Var a) \<longrightarrow>\<^isub>\<beta> t'" |
|
179 |
then obtain t' where "(Var a) \<longrightarrow>\<^isub>\<beta> t'" by blast |
|
180 |
hence False by (cases, auto) |
|
181 |
} |
|
182 |
thus "NORMAL (Var a)" by (force simp add: NORMAL_def) |
|
183 |
qed |
|
184 |
||
23970 | 185 |
inductive |
186 |
SN :: "lam \<Rightarrow> bool" |
|
187 |
where |
|
188 |
SN_intro: "(\<And>t'. t \<longrightarrow>\<^isub>\<beta> t' \<Longrightarrow> SN t') \<Longrightarrow> SN t" |
|
189 |
||
190 |
lemma SN_elim: |
|
191 |
assumes a: "SN M" |
|
192 |
shows "(\<forall>M. (\<forall>N. M \<longrightarrow>\<^isub>\<beta> N \<longrightarrow> P N)\<longrightarrow> P M) \<longrightarrow> P M" |
|
193 |
using a |
|
194 |
by (induct rule: SN.SN.induct) (blast) |
|
195 |
||
196 |
lemma SN_preserved: |
|
197 |
assumes a: "SN t1" "t1\<longrightarrow>\<^isub>\<beta> t2" |
|
198 |
shows "SN t2" |
|
199 |
using a |
|
200 |
by (cases) (auto) |
|
18106 | 201 |
|
23970 | 202 |
lemma double_SN_aux: |
203 |
assumes a: "SN a" |
|
204 |
and b: "SN b" |
|
205 |
and hyp: "\<And>x z. |
|
24899 | 206 |
\<lbrakk>\<And>y. x \<longrightarrow>\<^isub>\<beta> y \<Longrightarrow> SN y; \<And>y. x \<longrightarrow>\<^isub>\<beta> y \<Longrightarrow> P y z; |
207 |
\<And>u. z \<longrightarrow>\<^isub>\<beta> u \<Longrightarrow> SN u; \<And>u. z \<longrightarrow>\<^isub>\<beta> u \<Longrightarrow> P x u\<rbrakk> \<Longrightarrow> P x z" |
|
23970 | 208 |
shows "P a b" |
209 |
proof - |
|
210 |
from a |
|
211 |
have r: "\<And>b. SN b \<Longrightarrow> P a b" |
|
212 |
proof (induct a rule: SN.SN.induct) |
|
213 |
case (SN_intro x) |
|
214 |
note SNI' = SN_intro |
|
215 |
have "SN b" by fact |
|
216 |
thus ?case |
|
217 |
proof (induct b rule: SN.SN.induct) |
|
218 |
case (SN_intro y) |
|
219 |
show ?case |
|
220 |
apply (rule hyp) |
|
221 |
apply (erule SNI') |
|
222 |
apply (erule SNI') |
|
223 |
apply (rule SN.SN_intro) |
|
224 |
apply (erule SN_intro)+ |
|
225 |
done |
|
226 |
qed |
|
227 |
qed |
|
228 |
from b show ?thesis by (rule r) |
|
229 |
qed |
|
18106 | 230 |
|
23970 | 231 |
lemma double_SN[consumes 2]: |
232 |
assumes a: "SN a" |
|
233 |
and b: "SN b" |
|
234 |
and c: "\<And>x z. \<lbrakk>\<And>y. x \<longrightarrow>\<^isub>\<beta> y \<Longrightarrow> P y z; \<And>u. z \<longrightarrow>\<^isub>\<beta> u \<Longrightarrow> P x u\<rbrakk> \<Longrightarrow> P x z" |
|
235 |
shows "P a b" |
|
236 |
using a b c |
|
237 |
apply(rule_tac double_SN_aux) |
|
238 |
apply(assumption)+ |
|
239 |
apply(blast) |
|
18106 | 240 |
done |
241 |
||
242 |
section {* Candidates *} |
|
243 |
||
22440
7e4f4f19002f
deleted function for defining candidates and used nominal_primrec instead
urbanc
parents:
22420
diff
changeset
|
244 |
consts |
18106 | 245 |
RED :: "ty \<Rightarrow> lam set" |
22440
7e4f4f19002f
deleted function for defining candidates and used nominal_primrec instead
urbanc
parents:
22420
diff
changeset
|
246 |
|
7e4f4f19002f
deleted function for defining candidates and used nominal_primrec instead
urbanc
parents:
22420
diff
changeset
|
247 |
nominal_primrec |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
248 |
"RED (TVar X) = {t. SN(t)}" |
22440
7e4f4f19002f
deleted function for defining candidates and used nominal_primrec instead
urbanc
parents:
22420
diff
changeset
|
249 |
"RED (\<tau>\<rightarrow>\<sigma>) = {t. \<forall>u. (u\<in>RED \<tau> \<longrightarrow> (App t u)\<in>RED \<sigma>)}" |
23970 | 250 |
by (rule TrueI)+ |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
251 |
|
24899 | 252 |
(* neutral terms *) |
18106 | 253 |
constdefs |
254 |
NEUT :: "lam \<Rightarrow> bool" |
|
23970 | 255 |
"NEUT t \<equiv> (\<exists>a. t = Var a) \<or> (\<exists>t1 t2. t = App t1 t2)" |
18106 | 256 |
|
257 |
(* a slight hack to get the first element of applications *) |
|
23970 | 258 |
(* this is needed to get (SN t) from SN (App t s) *) |
23760 | 259 |
inductive |
23142 | 260 |
FST :: "lam\<Rightarrow>lam\<Rightarrow>bool" (" _ \<guillemotright> _" [80,80] 80) |
22271 | 261 |
where |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
262 |
fst[intro!]: "(App t s) \<guillemotright> t" |
18106 | 263 |
|
24899 | 264 |
consts |
265 |
fst_app_aux::"lam\<Rightarrow>lam option" |
|
266 |
||
267 |
nominal_primrec |
|
268 |
"fst_app_aux (Var a) = None" |
|
269 |
"fst_app_aux (App t1 t2) = Some t1" |
|
270 |
"fst_app_aux (Lam [x].t) = None" |
|
271 |
apply(finite_guess)+ |
|
272 |
apply(rule TrueI)+ |
|
273 |
apply(simp add: fresh_none) |
|
274 |
apply(fresh_guess)+ |
|
275 |
done |
|
276 |
||
277 |
definition |
|
278 |
fst_app_def[simp]: "fst_app t = the (fst_app_aux t)" |
|
279 |
||
23970 | 280 |
lemma SN_of_FST_of_App: |
281 |
assumes a: "SN (App t s)" |
|
24899 | 282 |
shows "SN (fst_app (App t s))" |
23970 | 283 |
using a |
284 |
proof - |
|
285 |
from a have "\<forall>z. (App t s \<guillemotright> z) \<longrightarrow> SN z" |
|
286 |
by (induct rule: SN.SN.induct) |
|
287 |
(blast elim: FST.cases intro: SN_intro) |
|
24899 | 288 |
then have "SN t" by blast |
289 |
then show "SN (fst_app (App t s))" by simp |
|
23970 | 290 |
qed |
18106 | 291 |
|
18383 | 292 |
section {* Candidates *} |
293 |
||
18106 | 294 |
constdefs |
18383 | 295 |
"CR1" :: "ty \<Rightarrow> bool" |
23970 | 296 |
"CR1 \<tau> \<equiv> \<forall>t. (t\<in>RED \<tau> \<longrightarrow> SN t)" |
18106 | 297 |
|
18383 | 298 |
"CR2" :: "ty \<Rightarrow> bool" |
299 |
"CR2 \<tau> \<equiv> \<forall>t t'. (t\<in>RED \<tau> \<and> t \<longrightarrow>\<^isub>\<beta> t') \<longrightarrow> t'\<in>RED \<tau>" |
|
18106 | 300 |
|
18383 | 301 |
"CR3_RED" :: "lam \<Rightarrow> ty \<Rightarrow> bool" |
302 |
"CR3_RED t \<tau> \<equiv> \<forall>t'. t\<longrightarrow>\<^isub>\<beta> t' \<longrightarrow> t'\<in>RED \<tau>" |
|
18106 | 303 |
|
18383 | 304 |
"CR3" :: "ty \<Rightarrow> bool" |
305 |
"CR3 \<tau> \<equiv> \<forall>t. (NEUT t \<and> CR3_RED t \<tau>) \<longrightarrow> t\<in>RED \<tau>" |
|
18106 | 306 |
|
18383 | 307 |
"CR4" :: "ty \<Rightarrow> bool" |
308 |
"CR4 \<tau> \<equiv> \<forall>t. (NEUT t \<and> NORMAL t) \<longrightarrow>t\<in>RED \<tau>" |
|
18106 | 309 |
|
23970 | 310 |
lemma CR3_implies_CR4: |
311 |
assumes a: "CR3 \<tau>" |
|
312 |
shows "CR4 \<tau>" |
|
313 |
using a by (auto simp add: CR3_def CR3_RED_def CR4_def NORMAL_def) |
|
18106 | 314 |
|
23970 | 315 |
(* sub_induction in the arrow-type case for the next proof *) |
316 |
lemma sub_induction: |
|
317 |
assumes a: "SN(u)" |
|
318 |
and b: "u\<in>RED \<tau>" |
|
319 |
and c1: "NEUT t" |
|
320 |
and c2: "CR2 \<tau>" |
|
321 |
and c3: "CR3 \<sigma>" |
|
322 |
and c4: "CR3_RED t (\<tau>\<rightarrow>\<sigma>)" |
|
323 |
shows "(App t u)\<in>RED \<sigma>" |
|
324 |
using a b |
|
325 |
proof (induct) |
|
326 |
fix u |
|
327 |
assume as: "u\<in>RED \<tau>" |
|
328 |
assume ih: " \<And>u'. \<lbrakk>u \<longrightarrow>\<^isub>\<beta> u'; u' \<in> RED \<tau>\<rbrakk> \<Longrightarrow> App t u' \<in> RED \<sigma>" |
|
329 |
have "NEUT (App t u)" using c1 by (auto simp add: NEUT_def) |
|
330 |
moreover |
|
331 |
have "CR3_RED (App t u) \<sigma>" unfolding CR3_RED_def |
|
332 |
proof (intro strip) |
|
333 |
fix r |
|
334 |
assume red: "App t u \<longrightarrow>\<^isub>\<beta> r" |
|
335 |
moreover |
|
336 |
{ assume "\<exists>t'. t \<longrightarrow>\<^isub>\<beta> t' \<and> r = App t' u" |
|
337 |
then obtain t' where a1: "t \<longrightarrow>\<^isub>\<beta> t'" and a2: "r = App t' u" by blast |
|
338 |
have "t'\<in>RED (\<tau>\<rightarrow>\<sigma>)" using c4 a1 by (simp add: CR3_RED_def) |
|
339 |
then have "App t' u\<in>RED \<sigma>" using as by simp |
|
340 |
then have "r\<in>RED \<sigma>" using a2 by simp |
|
341 |
} |
|
342 |
moreover |
|
343 |
{ assume "\<exists>u'. u \<longrightarrow>\<^isub>\<beta> u' \<and> r = App t u'" |
|
344 |
then obtain u' where b1: "u \<longrightarrow>\<^isub>\<beta> u'" and b2: "r = App t u'" by blast |
|
345 |
have "u'\<in>RED \<tau>" using as b1 c2 by (auto simp add: CR2_def) |
|
346 |
with ih have "App t u' \<in> RED \<sigma>" using b1 by simp |
|
347 |
then have "r\<in>RED \<sigma>" using b2 by simp |
|
348 |
} |
|
349 |
moreover |
|
350 |
{ assume "\<exists>x t'. t = Lam [x].t'" |
|
351 |
then obtain x t' where "t = Lam [x].t'" by blast |
|
352 |
then have "NEUT (Lam [x].t')" using c1 by simp |
|
353 |
then have "False" by (simp add: NEUT_def) |
|
354 |
then have "r\<in>RED \<sigma>" by simp |
|
355 |
} |
|
356 |
ultimately show "r \<in> RED \<sigma>" by (cases) (auto simp add: lam.inject) |
|
357 |
qed |
|
358 |
ultimately show "App t u \<in> RED \<sigma>" using c3 by (simp add: CR3_def) |
|
359 |
qed |
|
18106 | 360 |
|
23970 | 361 |
(* properties of the candiadates *) |
18383 | 362 |
lemma RED_props: |
363 |
shows "CR1 \<tau>" and "CR2 \<tau>" and "CR3 \<tau>" |
|
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
364 |
proof (nominal_induct \<tau> rule: ty.induct) |
18611 | 365 |
case (TVar a) |
366 |
{ case 1 show "CR1 (TVar a)" by (simp add: CR1_def) |
|
367 |
next |
|
23970 | 368 |
case 2 show "CR2 (TVar a)" by (auto intro: SN_preserved simp add: CR2_def) |
18611 | 369 |
next |
23970 | 370 |
case 3 show "CR3 (TVar a)" by (auto intro: SN_intro simp add: CR3_def CR3_RED_def) |
18611 | 371 |
} |
18599
e01112713fdc
changed PRO_RED proof to conform with the new induction rules
urbanc
parents:
18383
diff
changeset
|
372 |
next |
18611 | 373 |
case (TArr \<tau>1 \<tau>2) |
374 |
{ case 1 |
|
375 |
have ih_CR3_\<tau>1: "CR3 \<tau>1" by fact |
|
376 |
have ih_CR1_\<tau>2: "CR1 \<tau>2" by fact |
|
23970 | 377 |
show "CR1 (\<tau>1 \<rightarrow> \<tau>2)" unfolding CR1_def |
378 |
proof (simp, intro strip) |
|
18611 | 379 |
fix t |
380 |
assume a: "\<forall>u. u \<in> RED \<tau>1 \<longrightarrow> App t u \<in> RED \<tau>2" |
|
23970 | 381 |
from ih_CR3_\<tau>1 have "CR4 \<tau>1" by (simp add: CR3_implies_CR4) |
18611 | 382 |
moreover |
383 |
have "NEUT (Var a)" by (force simp add: NEUT_def) |
|
384 |
moreover |
|
385 |
have "NORMAL (Var a)" by (rule NORMAL_Var) |
|
386 |
ultimately have "(Var a)\<in> RED \<tau>1" by (simp add: CR4_def) |
|
387 |
with a have "App t (Var a) \<in> RED \<tau>2" by simp |
|
388 |
hence "SN (App t (Var a))" using ih_CR1_\<tau>2 by (simp add: CR1_def) |
|
24899 | 389 |
thus "SN(t)" by (auto dest: SN_of_FST_of_App) |
18611 | 390 |
qed |
391 |
next |
|
392 |
case 2 |
|
393 |
have ih_CR1_\<tau>1: "CR1 \<tau>1" by fact |
|
394 |
have ih_CR2_\<tau>2: "CR2 \<tau>2" by fact |
|
23970 | 395 |
show "CR2 (\<tau>1 \<rightarrow> \<tau>2)" unfolding CR2_def |
396 |
proof (simp, intro strip) |
|
18611 | 397 |
fix t1 t2 u |
398 |
assume "(\<forall>u. u \<in> RED \<tau>1 \<longrightarrow> App t1 u \<in> RED \<tau>2) \<and> t1 \<longrightarrow>\<^isub>\<beta> t2" |
|
399 |
and "u \<in> RED \<tau>1" |
|
400 |
hence "t1 \<longrightarrow>\<^isub>\<beta> t2" and "App t1 u \<in> RED \<tau>2" by simp_all |
|
23970 | 401 |
thus "App t2 u \<in> RED \<tau>2" using ih_CR2_\<tau>2 by (auto simp add: CR2_def) |
18611 | 402 |
qed |
403 |
next |
|
404 |
case 3 |
|
405 |
have ih_CR1_\<tau>1: "CR1 \<tau>1" by fact |
|
406 |
have ih_CR2_\<tau>1: "CR2 \<tau>1" by fact |
|
407 |
have ih_CR3_\<tau>2: "CR3 \<tau>2" by fact |
|
23970 | 408 |
show "CR3 (\<tau>1 \<rightarrow> \<tau>2)" unfolding CR3_def |
409 |
proof (simp, intro strip) |
|
18611 | 410 |
fix t u |
411 |
assume a1: "u \<in> RED \<tau>1" |
|
412 |
assume a2: "NEUT t \<and> CR3_RED t (\<tau>1 \<rightarrow> \<tau>2)" |
|
23970 | 413 |
have "SN(u)" using a1 ih_CR1_\<tau>1 by (simp add: CR1_def) |
414 |
then show "(App t u)\<in>RED \<tau>2" using ih_CR2_\<tau>1 ih_CR3_\<tau>2 a1 a2 by (blast intro: sub_induction) |
|
18611 | 415 |
qed |
416 |
} |
|
18383 | 417 |
qed |
23970 | 418 |
|
419 |
(* not as simple as on paper, because of the stronger double_SN induction *) |
|
420 |
lemma abs_RED: |
|
421 |
assumes asm: "\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>" |
|
422 |
shows "Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)" |
|
18106 | 423 |
proof - |
23970 | 424 |
have b1: "SN t" |
425 |
proof - |
|
426 |
have "Var x\<in>RED \<tau>" |
|
427 |
proof - |
|
428 |
have "CR4 \<tau>" by (simp add: RED_props CR3_implies_CR4) |
|
429 |
moreover |
|
430 |
have "NEUT (Var x)" by (auto simp add: NEUT_def) |
|
431 |
moreover |
|
432 |
have "NORMAL (Var x)" by (auto elim: Beta.cases simp add: NORMAL_def) |
|
433 |
ultimately show "Var x\<in>RED \<tau>" by (simp add: CR4_def) |
|
434 |
qed |
|
435 |
then have "t[x::=Var x]\<in>RED \<sigma>" using asm by simp |
|
436 |
then have "t\<in>RED \<sigma>" by (simp add: id_subs) |
|
437 |
moreover |
|
438 |
have "CR1 \<sigma>" by (simp add: RED_props) |
|
439 |
ultimately show "SN t" by (simp add: CR1_def) |
|
440 |
qed |
|
441 |
show "Lam [x].t\<in>RED (\<tau>\<rightarrow>\<sigma>)" |
|
442 |
proof (simp, intro strip) |
|
443 |
fix u |
|
444 |
assume b2: "u\<in>RED \<tau>" |
|
445 |
then have b3: "SN u" using RED_props by (auto simp add: CR1_def) |
|
446 |
show "App (Lam [x].t) u \<in> RED \<sigma>" using b1 b3 b2 asm |
|
447 |
proof(induct t u rule: double_SN) |
|
448 |
fix t u |
|
449 |
assume ih1: "\<And>t'. \<lbrakk>t \<longrightarrow>\<^isub>\<beta> t'; u\<in>RED \<tau>; \<forall>s\<in>RED \<tau>. t'[x::=s]\<in>RED \<sigma>\<rbrakk> \<Longrightarrow> App (Lam [x].t') u \<in> RED \<sigma>" |
|
450 |
assume ih2: "\<And>u'. \<lbrakk>u \<longrightarrow>\<^isub>\<beta> u'; u'\<in>RED \<tau>; \<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>\<rbrakk> \<Longrightarrow> App (Lam [x].t) u' \<in> RED \<sigma>" |
|
451 |
assume as1: "u \<in> RED \<tau>" |
|
452 |
assume as2: "\<forall>s\<in>RED \<tau>. t[x::=s]\<in>RED \<sigma>" |
|
453 |
have "CR3_RED (App (Lam [x].t) u) \<sigma>" unfolding CR3_RED_def |
|
454 |
proof(intro strip) |
|
455 |
fix r |
|
456 |
assume red: "App (Lam [x].t) u \<longrightarrow>\<^isub>\<beta> r" |
|
457 |
moreover |
|
458 |
{ assume "\<exists>t'. t \<longrightarrow>\<^isub>\<beta> t' \<and> r = App (Lam [x].t') u" |
|
459 |
then obtain t' where a1: "t \<longrightarrow>\<^isub>\<beta> t'" and a2: "r = App (Lam [x].t') u" by blast |
|
460 |
have "App (Lam [x].t') u\<in>RED \<sigma>" using ih1 a1 as1 as2 |
|
461 |
apply(auto) |
|
462 |
apply(drule_tac x="t'" in meta_spec) |
|
463 |
apply(simp) |
|
464 |
apply(drule meta_mp) |
|
465 |
apply(auto) |
|
466 |
apply(drule_tac x="s" in bspec) |
|
467 |
apply(simp) |
|
468 |
apply(subgoal_tac "CR2 \<sigma>") |
|
469 |
apply(unfold CR2_def)[1] |
|
470 |
apply(drule_tac x="t[x::=s]" in spec) |
|
471 |
apply(drule_tac x="t'[x::=s]" in spec) |
|
472 |
apply(simp add: beta_subst) |
|
473 |
apply(simp add: RED_props) |
|
474 |
done |
|
475 |
then have "r\<in>RED \<sigma>" using a2 by simp |
|
476 |
} |
|
477 |
moreover |
|
478 |
{ assume "\<exists>u'. u \<longrightarrow>\<^isub>\<beta> u' \<and> r = App (Lam [x].t) u'" |
|
479 |
then obtain u' where b1: "u \<longrightarrow>\<^isub>\<beta> u'" and b2: "r = App (Lam [x].t) u'" by blast |
|
480 |
have "App (Lam [x].t) u'\<in>RED \<sigma>" using ih2 b1 as1 as2 |
|
481 |
apply(auto) |
|
482 |
apply(drule_tac x="u'" in meta_spec) |
|
483 |
apply(simp) |
|
484 |
apply(drule meta_mp) |
|
485 |
apply(subgoal_tac "CR2 \<tau>") |
|
486 |
apply(unfold CR2_def)[1] |
|
487 |
apply(drule_tac x="u" in spec) |
|
488 |
apply(drule_tac x="u'" in spec) |
|
489 |
apply(simp) |
|
490 |
apply(simp add: RED_props) |
|
491 |
apply(simp) |
|
492 |
done |
|
493 |
then have "r\<in>RED \<sigma>" using b2 by simp |
|
494 |
} |
|
495 |
moreover |
|
496 |
{ assume "r = t[x::=u]" |
|
497 |
then have "r\<in>RED \<sigma>" using as1 as2 by auto |
|
498 |
} |
|
499 |
ultimately show "r \<in> RED \<sigma>" |
|
500 |
apply(cases) |
|
501 |
apply(auto simp add: lam.inject) |
|
502 |
apply(drule beta_abs) |
|
503 |
apply(auto simp add: alpha subst_rename) |
|
18106 | 504 |
done |
505 |
qed |
|
23970 | 506 |
moreover |
507 |
have "NEUT (App (Lam [x].t) u)" unfolding NEUT_def by (auto) |
|
508 |
ultimately show "App (Lam [x].t) u \<in> RED \<sigma>" using RED_props by (simp add: CR3_def) |
|
18106 | 509 |
qed |
510 |
qed |
|
23970 | 511 |
qed |
18106 | 512 |
|
22420 | 513 |
abbreviation |
514 |
mapsto :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> bool" ("_ maps _ to _" [55,55,55] 55) |
|
515 |
where |
|
516 |
"\<theta> maps x to e\<equiv> (lookup \<theta> x) = e" |
|
517 |
||
518 |
abbreviation |
|
519 |
closes :: "(name\<times>lam) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" ("_ closes _" [55,55] 55) |
|
520 |
where |
|
521 |
"\<theta> closes \<Gamma> \<equiv> \<forall>x T. ((x,T) \<in> set \<Gamma> \<longrightarrow> (\<exists>t. \<theta> maps x to t \<and> t \<in> RED T))" |
|
21107
e69c0e82955a
new file for defining functions in the lambda-calculus
urbanc
parents:
19972
diff
changeset
|
522 |
|
18106 | 523 |
lemma all_RED: |
22420 | 524 |
assumes a: "\<Gamma> \<turnstile> t : \<tau>" |
525 |
and b: "\<theta> closes \<Gamma>" |
|
526 |
shows "\<theta><t> \<in> RED \<tau>" |
|
18345 | 527 |
using a b |
23142 | 528 |
proof(nominal_induct avoiding: \<theta> rule: typing.strong_induct) |
529 |
case (t3 a \<Gamma> \<sigma> t \<tau> \<theta>) --"lambda case" |
|
530 |
have ih: "\<And>\<theta>. \<theta> closes ((a,\<sigma>)#\<Gamma>) \<Longrightarrow> \<theta><t> \<in> RED \<tau>" by fact |
|
531 |
have \<theta>_cond: "\<theta> closes \<Gamma>" by fact |
|
23393 | 532 |
have fresh: "a\<sharp>\<Gamma>" "a\<sharp>\<theta>" by fact+ |
24899 | 533 |
from ih have "\<forall>s\<in>RED \<sigma>. ((a,s)#\<theta>)<t> \<in> RED \<tau>" using fresh \<theta>_cond fresh_context by simp |
534 |
then have "\<forall>s\<in>RED \<sigma>. \<theta><t>[a::=s] \<in> RED \<tau>" using fresh by (simp add: psubst_subst) |
|
23970 | 535 |
then have "Lam [a].(\<theta><t>) \<in> RED (\<sigma> \<rightarrow> \<tau>)" by (simp only: abs_RED) |
23142 | 536 |
then show "\<theta><(Lam [a].t)> \<in> RED (\<sigma> \<rightarrow> \<tau>)" using fresh by simp |
537 |
qed auto |
|
18345 | 538 |
|
23142 | 539 |
section {* identity substitution generated from a context \<Gamma> *} |
540 |
fun |
|
18382 | 541 |
"id" :: "(name\<times>ty) list \<Rightarrow> (name\<times>lam) list" |
23142 | 542 |
where |
18382 | 543 |
"id [] = []" |
23142 | 544 |
| "id ((x,\<tau>)#\<Gamma>) = (x,Var x)#(id \<Gamma>)" |
18382 | 545 |
|
23142 | 546 |
lemma id_maps: |
547 |
shows "(id \<Gamma>) maps a to (Var a)" |
|
548 |
by (induct \<Gamma>) (auto) |
|
18382 | 549 |
|
550 |
lemma id_fresh: |
|
551 |
fixes a::"name" |
|
552 |
assumes a: "a\<sharp>\<Gamma>" |
|
553 |
shows "a\<sharp>(id \<Gamma>)" |
|
554 |
using a |
|
23142 | 555 |
by (induct \<Gamma>) |
556 |
(auto simp add: fresh_list_nil fresh_list_cons) |
|
18382 | 557 |
|
558 |
lemma id_apply: |
|
22420 | 559 |
shows "(id \<Gamma>)<t> = t" |
23970 | 560 |
by (nominal_induct t avoiding: \<Gamma> rule: lam.induct) |
561 |
(auto simp add: id_maps id_fresh) |
|
18382 | 562 |
|
23142 | 563 |
lemma id_closes: |
22420 | 564 |
shows "(id \<Gamma>) closes \<Gamma>" |
18383 | 565 |
apply(auto) |
23142 | 566 |
apply(simp add: id_maps) |
22420 | 567 |
apply(subgoal_tac "CR3 T") --"A" |
23970 | 568 |
apply(drule CR3_implies_CR4) |
18382 | 569 |
apply(simp add: CR4_def) |
22420 | 570 |
apply(drule_tac x="Var x" in spec) |
18383 | 571 |
apply(force simp add: NEUT_def NORMAL_Var) |
22418
49e2d9744ae1
major update of the nominal package; there is now an infrastructure
urbanc
parents:
22271
diff
changeset
|
572 |
--"A" |
18383 | 573 |
apply(rule RED_props) |
18382 | 574 |
done |
575 |
||
18383 | 576 |
lemma typing_implies_RED: |
23142 | 577 |
assumes a: "\<Gamma> \<turnstile> t : \<tau>" |
18383 | 578 |
shows "t \<in> RED \<tau>" |
579 |
proof - |
|
22420 | 580 |
have "(id \<Gamma>)<t>\<in>RED \<tau>" |
18383 | 581 |
proof - |
23142 | 582 |
have "(id \<Gamma>) closes \<Gamma>" by (rule id_closes) |
18383 | 583 |
with a show ?thesis by (rule all_RED) |
584 |
qed |
|
585 |
thus"t \<in> RED \<tau>" by (simp add: id_apply) |
|
586 |
qed |
|
587 |
||
588 |
lemma typing_implies_SN: |
|
23142 | 589 |
assumes a: "\<Gamma> \<turnstile> t : \<tau>" |
18383 | 590 |
shows "SN(t)" |
591 |
proof - |
|
592 |
from a have "t \<in> RED \<tau>" by (rule typing_implies_RED) |
|
593 |
moreover |
|
594 |
have "CR1 \<tau>" by (rule RED_props) |
|
595 |
ultimately show "SN(t)" by (simp add: CR1_def) |
|
596 |
qed |
|
18382 | 597 |
|
598 |
end |