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