|
1 (* "$Id$" *) |
|
2 (* *) |
|
3 (* Formalisation of the chapter *) |
|
4 (* Logical Relations and a Case Study in Equivalence *) |
|
5 (* Checking *) |
|
6 (* by Crary. *) |
|
7 (* Formalisation by Julien Narboux and Christian Urban*) |
|
8 |
|
9 theory Crary |
|
10 imports "Nominal" |
|
11 begin |
|
12 |
|
13 atom_decl name |
|
14 |
|
15 nominal_datatype ty = TBase |
|
16 | TUnit |
|
17 | Arrow "ty" "ty" ("_\<rightarrow>_" [100,100] 100) |
|
18 |
|
19 nominal_datatype trm = Unit |
|
20 | Var "name" |
|
21 | Lam "\<guillemotleft>name\<guillemotright>trm" ("Lam [_]._" [100,100] 100) |
|
22 | App "trm" "trm" |
|
23 | Const "nat" |
|
24 |
|
25 (* FIXME: the next lemma needs to be in Nominal.thy *) |
|
26 lemma eq_eqvt: |
|
27 fixes pi::"name prm" |
|
28 and x::"'a::pt_name" |
|
29 shows "pi\<bullet>(x=y) = (pi\<bullet>x=pi\<bullet>y)" |
|
30 apply(simp add: perm_bool perm_bij) |
|
31 done |
|
32 |
|
33 lemma in_eqvt: |
|
34 fixes pi::"name prm" |
|
35 and x::"'a::pt_name" |
|
36 assumes "x\<in>X" |
|
37 shows "pi\<bullet>x \<in> pi\<bullet>X" |
|
38 using assms by (perm_simp add: pt_set_bij1a[OF pt_name_inst, OF at_name_inst]) |
|
39 |
|
40 lemma set_eqvt: |
|
41 fixes pi::"name prm" |
|
42 and xs::"('a::pt_name) list" |
|
43 shows "pi\<bullet>(set xs) = set (pi\<bullet>xs)" |
|
44 by (perm_simp add: pt_list_set_pi[OF pt_name_inst]) |
|
45 |
|
46 (* End of library *) |
|
47 |
|
48 lemma perm_ty[simp]: |
|
49 fixes T::"ty" |
|
50 and pi::"name prm" |
|
51 shows "pi\<bullet>T = T" |
|
52 by (induct T rule: ty.induct_weak) (simp_all) |
|
53 |
|
54 lemma fresh_ty[simp]: |
|
55 fixes x::"name" |
|
56 and T::"ty" |
|
57 shows "x\<sharp>T" |
|
58 by (simp add: fresh_def supp_def) |
|
59 |
|
60 lemma ty_cases: |
|
61 fixes T::ty |
|
62 shows "(\<exists> T1 T2. T=T1\<rightarrow>T2) \<or> T=TUnit \<or> T=TBase" |
|
63 apply (induct T rule:ty.induct_weak) |
|
64 apply (auto) |
|
65 done |
|
66 |
|
67 text {* Size Functions *} |
|
68 |
|
69 instance ty :: size .. |
|
70 |
|
71 nominal_primrec |
|
72 "size (TBase) = 1" |
|
73 "size (TUnit) = 1" |
|
74 "size (T1\<rightarrow>T2) = size T1 + size T2" |
|
75 by (rule TrueI)+ |
|
76 |
|
77 instance trm :: size .. |
|
78 |
|
79 nominal_primrec |
|
80 "size (Unit) = 1" |
|
81 "size (Var x) = 1" |
|
82 "size (Lam [x].t) = size t + 1" |
|
83 "size (App t1 t2) = size t1 + size t2" |
|
84 "size (Const n) = 1" |
|
85 apply(finite_guess add: fs_name1 perm_nat_def)+ |
|
86 apply(perm_full_simp add: perm_nat_def) |
|
87 apply(simp add: fs_name1) |
|
88 apply(rule TrueI)+ |
|
89 apply(simp add: fresh_nat)+ |
|
90 apply(fresh_guess add: fs_name1 perm_nat_def)+ |
|
91 done |
|
92 |
|
93 lemma ty_size_greater_zero[simp]: |
|
94 fixes T::"ty" |
|
95 shows "size T > 0" |
|
96 by (nominal_induct rule:ty.induct) (simp_all) |
|
97 |
|
98 text {* valid contexts *} |
|
99 |
|
100 inductive2 |
|
101 valid :: "(name \<times> 'a::pt_name) list \<Rightarrow> bool" |
|
102 where |
|
103 v_nil[intro]: "valid []" |
|
104 | v_cons[intro]: "\<lbrakk>valid \<Gamma>;a\<sharp>\<Gamma>\<rbrakk> \<Longrightarrow> valid ((a,\<sigma>)#\<Gamma>)" |
|
105 |
|
106 lemma valid_eqvt: |
|
107 fixes pi:: "name prm" |
|
108 assumes a: "valid \<Gamma>" |
|
109 shows "valid (pi\<bullet>\<Gamma>)" |
|
110 using a |
|
111 by (induct) (auto simp add: fresh_bij) |
|
112 |
|
113 inductive_cases2 |
|
114 valid_cons_elim_auto[elim]:"valid ((x,T)#\<Gamma>)" |
|
115 |
|
116 text {* typing judgements for trms *} |
|
117 |
|
118 inductive2 |
|
119 typing :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" (" _ \<turnstile> _ : _ " [60,60,60] 60) |
|
120 where |
|
121 t_Var[intro]: "\<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> Var x : T" |
|
122 | t_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> e1 : T1\<rightarrow>T2; \<Gamma> \<turnstile> e2 : T1\<rbrakk>\<Longrightarrow> \<Gamma> \<turnstile> App e1 e2 : T2" |
|
123 | t_Lam[intro]: "\<lbrakk>x\<sharp>\<Gamma>; (x,T1)#\<Gamma> \<turnstile> t : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x].t : T1\<rightarrow>T2" |
|
124 | t_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n : TBase" |
|
125 | t_Unit[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Unit : TUnit" |
|
126 |
|
127 lemma typing_valid: |
|
128 assumes "\<Gamma> \<turnstile> t : T" |
|
129 shows "valid \<Gamma>" |
|
130 using assms |
|
131 by (induct) (auto) |
|
132 |
|
133 lemma typing_eqvt : |
|
134 fixes pi::"name prm" |
|
135 assumes "\<Gamma> \<turnstile> t : T" |
|
136 shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>t) : T" |
|
137 using assms |
|
138 apply(induct) |
|
139 apply(auto simp add: fresh_bij set_eqvt valid_eqvt) |
|
140 apply(rule t_Var) |
|
141 apply(drule valid_eqvt) |
|
142 apply(assumption) |
|
143 apply(drule in_eqvt) |
|
144 apply(simp add: set_eqvt) |
|
145 done |
|
146 |
|
147 text {* Inversion lemmas for the typing judgment *} |
|
148 |
|
149 declare trm.inject [simp add] |
|
150 declare ty.inject [simp add] |
|
151 |
|
152 inductive_cases2 t_Lam_elim_auto[elim]: "\<Gamma> \<turnstile> Lam [x].t : T" |
|
153 inductive_cases2 t_Var_elim_auto[elim]: "\<Gamma> \<turnstile> Var x : T" |
|
154 inductive_cases2 t_App_elim_auto[elim]: "\<Gamma> \<turnstile> App x y : T" |
|
155 inductive_cases2 t_Const_elim_auto[elim]: "\<Gamma> \<turnstile> Const n : T" |
|
156 inductive_cases2 t_Unit_elim_auto[elim]: "\<Gamma> \<turnstile> Unit : TUnit" |
|
157 |
|
158 declare trm.inject [simp del] |
|
159 declare ty.inject [simp del] |
|
160 |
|
161 lemma typing_induct_strong |
|
162 [consumes 1, case_names t_Var t_App t_Lam t_Const t_Unit]: |
|
163 fixes P::"'a::fs_name \<Rightarrow> (name\<times>ty) list \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow>bool" |
|
164 and x :: "'a::fs_name" |
|
165 assumes a: "\<Gamma> \<turnstile> e : T" |
|
166 and a1: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x,T)\<in>set \<Gamma>\<rbrakk> \<Longrightarrow> P c \<Gamma> (Var x) T" |
|
167 and a2: "\<And>\<Gamma> e1 T1 T2 e2 c. |
|
168 \<lbrakk>\<Gamma> \<turnstile> e1 : T1\<rightarrow>T2 ; \<And>c. P c \<Gamma> e1 (T1\<rightarrow>T2); \<Gamma> \<turnstile> e2 : T1 ; \<And>c. P c \<Gamma> e2 T1\<rbrakk> |
|
169 \<Longrightarrow> P c \<Gamma> (App e1 e2) T2" |
|
170 and a3: "\<And>x \<Gamma> T1 t T2 c. |
|
171 \<lbrakk>x\<sharp>(\<Gamma>,c); (x,T1)#\<Gamma> \<turnstile> t : T2 ; \<And>c. P c ((x,T1)#\<Gamma>) t T2\<rbrakk> |
|
172 \<Longrightarrow> P c \<Gamma> (Lam [x].t) (T1\<rightarrow>T2)" |
|
173 and a4: "\<And>\<Gamma> n c. valid \<Gamma> \<Longrightarrow> P c \<Gamma> (Const n) TBase" |
|
174 and a5: "\<And>\<Gamma> c. valid \<Gamma> \<Longrightarrow> P c \<Gamma> Unit TUnit" |
|
175 shows "P c \<Gamma> e T" |
|
176 proof - |
|
177 from a have "\<And>(pi::name prm) c. P c (pi\<bullet>\<Gamma>) (pi\<bullet>e) T" |
|
178 proof (induct) |
|
179 case (t_Var \<Gamma> x T pi c) |
|
180 have "valid \<Gamma>" by fact |
|
181 then have "valid (pi\<bullet>\<Gamma>)" by (simp only: valid_eqvt) |
|
182 moreover |
|
183 have "(x,T)\<in>set \<Gamma>" by fact |
|
184 then have "pi\<bullet>(x,T)\<in>pi\<bullet>(set \<Gamma>)" by (simp only: pt_set_bij[OF pt_name_inst, OF at_name_inst]) |
|
185 then have "(pi\<bullet>x,T)\<in>set (pi\<bullet>\<Gamma>)" by (simp add: set_eqvt) |
|
186 ultimately show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Var x)) T" using a1 by simp |
|
187 next |
|
188 case (t_App \<Gamma> e1 T1 T2 e2 pi c) |
|
189 thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(App e1 e2)) T2" using a2 by (simp, blast intro: typing_eqvt) |
|
190 next |
|
191 case (t_Lam x \<Gamma> T1 t T2 pi c) |
|
192 obtain y::"name" where fs: "y\<sharp>(pi\<bullet>x,pi\<bullet>\<Gamma>,pi\<bullet>t,c)" by (erule exists_fresh[OF fs_name1]) |
|
193 let ?sw = "[(pi\<bullet>x,y)]" |
|
194 let ?pi' = "?sw@pi" |
|
195 have f0: "x\<sharp>\<Gamma>" by fact |
|
196 have f1: "(pi\<bullet>x)\<sharp>(pi\<bullet>\<Gamma>)" using f0 by (simp add: fresh_bij) |
|
197 have f2: "y\<sharp>?pi'\<bullet>\<Gamma>" by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp) |
|
198 have pr1: "(x,T1)#\<Gamma> \<turnstile> t : T2" by fact |
|
199 then have "(?pi'\<bullet>((x,T1)#\<Gamma>)) \<turnstile> (?pi'\<bullet>t) : T2" by (simp only: typing_eqvt) |
|
200 moreover |
|
201 have ih1: "\<And>c. P c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>t) T2" by fact |
|
202 ultimately have "P c (?pi'\<bullet>\<Gamma>) (Lam [y].(?pi'\<bullet>t)) (T1\<rightarrow>T2)" using fs f2 a3 |
|
203 by (simp add: calc_atm) |
|
204 then have "P c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>t))) (T1\<rightarrow>T2)" |
|
205 by (simp del: append_Cons add: calc_atm pt_name2) |
|
206 moreover have "(?sw\<bullet>pi\<bullet>\<Gamma>) = (pi\<bullet>\<Gamma>)" |
|
207 by (rule perm_fresh_fresh) (simp_all add: fs f1) |
|
208 moreover have "(?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>t))) = Lam [(pi\<bullet>x)].(pi\<bullet>t)" |
|
209 by (rule perm_fresh_fresh) (simp_all add: fs f1 fresh_atm abs_fresh) |
|
210 ultimately show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Lam [x].t)) (T1\<rightarrow>T2)" |
|
211 by simp |
|
212 next |
|
213 case (t_Const \<Gamma> n pi c) |
|
214 thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>(Const n)) (TBase)" using a4 by (simp, blast intro: valid_eqvt) |
|
215 next |
|
216 case (t_Unit \<Gamma> pi c) |
|
217 thus "P c (pi\<bullet>\<Gamma>) (pi\<bullet>Unit) (TUnit)" using a5 by (simp, blast intro: valid_eqvt) |
|
218 qed |
|
219 then have "P c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>e) T" by blast |
|
220 then show "P c \<Gamma> e T" by simp |
|
221 qed |
|
222 |
|
223 text {* capture-avoiding substitution *} |
|
224 |
|
225 fun |
|
226 lookup :: "(name\<times>trm) list \<Rightarrow> name \<Rightarrow> trm" |
|
227 where |
|
228 "lookup [] X = Var X" |
|
229 "lookup ((Y,T)#\<theta>) X = (if X=Y then T else lookup \<theta> X)" |
|
230 |
|
231 lemma lookup_eqvt: |
|
232 fixes pi::"name prm" |
|
233 and \<theta>::"(name\<times>trm) list" |
|
234 and X::"name" |
|
235 shows "pi\<bullet>(lookup \<theta> X) = lookup (pi\<bullet>\<theta>) (pi\<bullet>X)" |
|
236 by (induct \<theta>) |
|
237 (auto simp add: perm_bij) |
|
238 |
|
239 lemma lookup_fresh: |
|
240 fixes z::"name" |
|
241 assumes "z\<sharp>\<theta>" "z\<sharp>x" |
|
242 shows "z \<sharp>lookup \<theta> x" |
|
243 using assms |
|
244 by (induct rule: lookup.induct) (auto simp add: fresh_list_cons) |
|
245 |
|
246 lemma lookup_fresh': |
|
247 assumes "z\<sharp>\<theta>" |
|
248 shows "lookup \<theta> z = Var z" |
|
249 using assms |
|
250 by (induct rule: lookup.induct) |
|
251 (auto simp add: fresh_list_cons fresh_prod fresh_atm) |
|
252 |
|
253 consts |
|
254 psubst :: "(name\<times>trm) list \<Rightarrow> trm \<Rightarrow> trm" ("_<_>" [60,100] 100) |
|
255 |
|
256 nominal_primrec |
|
257 "\<theta><(Var x)> = (lookup \<theta> x)" |
|
258 "\<theta><(App t1 t2)> = App (\<theta><t1>) (\<theta><t2>)" |
|
259 "x\<sharp>\<theta> \<Longrightarrow> \<theta><(Lam [x].t)> = Lam [x].(\<theta><t>)" |
|
260 "\<theta><(Const n)> = Const n" |
|
261 "\<theta><(Unit)> = Unit" |
|
262 apply(finite_guess add: fs_name1 lookup_eqvt)+ |
|
263 apply(perm_full_simp) |
|
264 apply(simp add: fs_name1) |
|
265 apply(rule TrueI)+ |
|
266 apply(simp add: abs_fresh)+ |
|
267 apply(fresh_guess add: fs_name1 lookup_eqvt)+ |
|
268 done |
|
269 |
|
270 abbreviation |
|
271 subst :: "trm \<Rightarrow> name \<Rightarrow> trm \<Rightarrow> trm" ("_[_::=_]" [100,100,100] 100) |
|
272 where |
|
273 "t[x::=t'] \<equiv> ([(x,t')])<t>" |
|
274 |
|
275 lemma subst[simp]: |
|
276 shows "(Var x)[y::=t'] = (if x=y then t' else (Var x))" |
|
277 and "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])" |
|
278 and "x\<sharp>(y,t') \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])" |
|
279 and "Const n[y::=t'] = Const n" |
|
280 and "Unit [y::=t'] = Unit" |
|
281 by (simp_all add: fresh_list_cons fresh_list_nil) |
|
282 |
|
283 lemma subst_eqvt: |
|
284 fixes pi::"name prm" |
|
285 and t::"trm" |
|
286 shows "pi\<bullet>(t[x::=t']) = (pi\<bullet>t)[(pi\<bullet>x)::=(pi\<bullet>t')]" |
|
287 by (nominal_induct t avoiding: x t' rule: trm.induct) |
|
288 (perm_simp add: fresh_bij)+ |
|
289 |
|
290 lemma subst_rename: |
|
291 fixes c::"name" |
|
292 and t1::"trm" |
|
293 assumes a: "c\<sharp>t1" |
|
294 shows "t1[a::=t2] = ([(c,a)]\<bullet>t1)[c::=t2]" |
|
295 using a |
|
296 apply(nominal_induct t1 avoiding: a c t2 rule: trm.induct) |
|
297 apply(simp add: trm.inject calc_atm fresh_atm abs_fresh perm_nat_def)+ |
|
298 done |
|
299 |
|
300 lemma fresh_psubst: |
|
301 fixes z::"name" |
|
302 and t::"trm" |
|
303 assumes "z\<sharp>t" "z\<sharp>\<theta>" |
|
304 shows "z\<sharp>(\<theta><t>)" |
|
305 using assms |
|
306 by (nominal_induct t avoiding: z \<theta> t rule: trm.induct) |
|
307 (auto simp add: abs_fresh lookup_fresh) |
|
308 |
|
309 lemma fresh_subst'': |
|
310 fixes z::"name" |
|
311 and t1::"trm" |
|
312 and t2::"trm" |
|
313 assumes "z\<sharp>t2" |
|
314 shows "z\<sharp>t1[z::=t2]" |
|
315 using assms |
|
316 by (nominal_induct t1 avoiding: t2 z rule: trm.induct) |
|
317 (auto simp add: abs_fresh fresh_nat fresh_atm) |
|
318 |
|
319 lemma fresh_subst': |
|
320 fixes z::"name" |
|
321 and t1::"trm" |
|
322 and t2::"trm" |
|
323 assumes "z\<sharp>[y].t1" "z\<sharp>t2" |
|
324 shows "z\<sharp>t1[y::=t2]" |
|
325 using assms |
|
326 by (nominal_induct t1 avoiding: y t2 z rule: trm.induct) |
|
327 (auto simp add: abs_fresh fresh_nat fresh_atm) |
|
328 |
|
329 lemma fresh_subst: |
|
330 fixes z::"name" |
|
331 and t1::"trm" |
|
332 and t2::"trm" |
|
333 assumes "z\<sharp>t1" "z\<sharp>t2" |
|
334 shows "z\<sharp>t1[y::=t2]" |
|
335 using assms fresh_subst' |
|
336 by (auto simp add: abs_fresh) |
|
337 |
|
338 lemma fresh_psubst_simpl: |
|
339 assumes "x\<sharp>t" |
|
340 shows "(x,u)#\<theta><t> = \<theta><t>" |
|
341 using assms |
|
342 proof (nominal_induct t avoiding: x u \<theta> rule: trm.induct) |
|
343 case (Lam y t x u) |
|
344 have fs: "y\<sharp>\<theta>" "y\<sharp>x" "y\<sharp>u" by fact |
|
345 moreover have "x\<sharp> Lam [y].t" by fact |
|
346 ultimately have "x\<sharp>t" by (simp add: abs_fresh fresh_atm) |
|
347 moreover have ih:"\<And>n T. n\<sharp>t \<Longrightarrow> ((n,T)#\<theta>)<t> = \<theta><t>" by fact |
|
348 ultimately have "(x,u)#\<theta><t> = \<theta><t>" by auto |
|
349 moreover have "(x,u)#\<theta><Lam [y].t> = Lam [y]. ((x,u)#\<theta><t>)" using fs |
|
350 by (simp add: fresh_list_cons fresh_prod) |
|
351 moreover have " \<theta><Lam [y].t> = Lam [y]. (\<theta><t>)" using fs by simp |
|
352 ultimately show "(x,u)#\<theta><Lam [y].t> = \<theta><Lam [y].t>" by auto |
|
353 qed (auto simp add: fresh_atm abs_fresh) |
|
354 |
|
355 text {* Equivalence (defined) *} |
|
356 |
|
357 inductive2 |
|
358 equiv_def :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ == _ : _" [60,60] 60) |
|
359 where |
|
360 Q_Refl[intro]: "\<Gamma> \<turnstile> t : T \<Longrightarrow> \<Gamma> \<turnstile> t == t : T" |
|
361 | Q_Symm[intro]: "\<Gamma> \<turnstile> t == s : T \<Longrightarrow> \<Gamma> \<turnstile> s == t : T" |
|
362 | Q_Trans[intro]: "\<lbrakk>\<Gamma> \<turnstile> s == t : T; \<Gamma> \<turnstile> t == u : T\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s == u : T" |
|
363 | Q_Abs[intro]: "\<lbrakk>x\<sharp>\<Gamma>; (x,T1)#\<Gamma> \<turnstile> s2 == t2 : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Lam [x]. s2 == Lam [x]. t2 : T1 \<rightarrow> T2" |
|
364 | Q_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> s1 == t1 : T1 \<rightarrow> T2 ; \<Gamma> \<turnstile> s2 == t2 : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App s1 s2 == App t1 t2 : T2" |
|
365 | Q_Beta[intro]: "\<lbrakk>x\<sharp>(\<Gamma>,s2,t2); (x,T1)#\<Gamma> \<turnstile> s12 == t12 : T2 ; \<Gamma> \<turnstile> s2 == t2 : T1\<rbrakk> |
|
366 \<Longrightarrow> \<Gamma> \<turnstile> App (Lam [x]. s12) s2 == t12[x::=t2] : T2" |
|
367 | Q_Ext[intro]: "\<lbrakk>x\<sharp>(\<Gamma>,s,t); (x,T1)#\<Gamma> \<turnstile> App s (Var x) == App t (Var x) : T2\<rbrakk> |
|
368 \<Longrightarrow> \<Gamma> \<turnstile> s == t : T1 \<rightarrow> T2" |
|
369 |
|
370 lemma equiv_def_valid: |
|
371 assumes "\<Gamma> \<turnstile> t == s : T" |
|
372 shows "valid \<Gamma>" |
|
373 using assms by (induct,auto elim:typing_valid) |
|
374 |
|
375 lemma equiv_def_eqvt: |
|
376 fixes pi::"name prm" |
|
377 assumes a: "\<Gamma> \<turnstile> s == t : T" |
|
378 shows "(pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) == (pi\<bullet>t) : T" |
|
379 using a |
|
380 apply(induct) |
|
381 apply(auto intro: typing_eqvt valid_eqvt simp add: fresh_bij subst_eqvt) |
|
382 apply(rule_tac x="pi\<bullet>x" in Q_Ext) |
|
383 apply(simp add: fresh_bij)+ |
|
384 done |
|
385 |
|
386 lemma equiv_def_strong_induct |
|
387 [consumes 1, case_names Q_Refl Q_Symm Q_Trans Q_Abs Q_App Q_Beta Q_Ext]: |
|
388 fixes c::"'a::fs_name" |
|
389 assumes a0: "\<Gamma> \<turnstile> s == t : T" |
|
390 and a1: "\<And>\<Gamma> t T c. \<Gamma> \<turnstile> t : T \<Longrightarrow> P c \<Gamma> t t T" |
|
391 and a2: "\<And>\<Gamma> t s T c. \<lbrakk>\<Gamma> \<turnstile> t == s : T; \<And>d. P d \<Gamma> t s T\<rbrakk> \<Longrightarrow> P c \<Gamma> s t T" |
|
392 and a3: "\<And>\<Gamma> s t T u c. |
|
393 \<lbrakk>\<Gamma> \<turnstile> s == t : T; \<And>d. P d \<Gamma> s t T; \<Gamma> \<turnstile> t == u : T; \<And>d. P d \<Gamma> t u T\<rbrakk> |
|
394 \<Longrightarrow> P c \<Gamma> s u T" |
|
395 and a4: "\<And>x \<Gamma> T1 s2 t2 T2 c. \<lbrakk>x\<sharp>\<Gamma>; x\<sharp>c; (x,T1)#\<Gamma> \<turnstile> s2 == t2 : T2; \<And>d. P d ((x,T1)#\<Gamma>) s2 t2 T2\<rbrakk> |
|
396 \<Longrightarrow> P c \<Gamma> (Lam [x].s2) (Lam [x].t2) (T1\<rightarrow>T2)" |
|
397 and a5: "\<And>\<Gamma> s1 t1 T1 T2 s2 t2 c. |
|
398 \<lbrakk>\<Gamma> \<turnstile> s1 == t1 : T1\<rightarrow>T2; \<And>d. P d \<Gamma> s1 t1 (T1\<rightarrow>T2); |
|
399 \<Gamma> \<turnstile> s2 == t2 : T1; \<And>d. P d \<Gamma> s2 t2 T1\<rbrakk> \<Longrightarrow> P c \<Gamma> (App s1 s2) (App t1 t2) T2" |
|
400 and a6: "\<And>x \<Gamma> T1 s12 t12 T2 s2 t2 c. |
|
401 \<lbrakk>x\<sharp>(\<Gamma>,s2,t2); x\<sharp>c; (x,T1)#\<Gamma> \<turnstile> s12 == t12 : T2; \<And>d. P d ((x,T1)#\<Gamma>) s12 t12 T2; |
|
402 \<Gamma> \<turnstile> s2 == t2 : T1; \<And>d. P d \<Gamma> s2 t2 T1\<rbrakk> |
|
403 \<Longrightarrow> P c \<Gamma> (App (Lam [x].s12) s2) (t12[x::=t2]) T2" |
|
404 and a7: "\<And>x \<Gamma> s t T1 T2 c. |
|
405 \<lbrakk>x\<sharp>(\<Gamma>,s,t); (x,T1)#\<Gamma> \<turnstile> App s (Var x) == App t (Var x) : T2; |
|
406 \<And>d. P d ((x,T1)#\<Gamma>) (App s (Var x)) (App t (Var x)) T2\<rbrakk> |
|
407 \<Longrightarrow> P c \<Gamma> s t (T1\<rightarrow>T2)" |
|
408 shows "P c \<Gamma> s t T" |
|
409 proof - |
|
410 from a0 have "\<And>(pi::name prm) c. P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) T" |
|
411 proof(induct) |
|
412 case (Q_Refl \<Gamma> t T pi c) |
|
413 then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>t) (pi\<bullet>t) T" using a1 by (simp add: typing_eqvt) |
|
414 next |
|
415 case (Q_Symm \<Gamma> t s T pi c) |
|
416 then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) T" using a2 by (simp only: equiv_def_eqvt) |
|
417 next |
|
418 case (Q_Trans \<Gamma> s t T u pi c) |
|
419 then show " P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>u) T" using a3 by (blast intro: equiv_def_eqvt) |
|
420 next |
|
421 case (Q_App \<Gamma> s1 t1 T1 T2 s2 t2 pi c) |
|
422 then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>App s1 s2) (pi\<bullet>App t1 t2) T2" using a5 |
|
423 by (simp, blast intro: equiv_def_eqvt) |
|
424 next |
|
425 case (Q_Ext x \<Gamma> s t T1 T2 pi c) |
|
426 then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (T1\<rightarrow>T2)" using a7 |
|
427 apply - |
|
428 apply(simp) |
|
429 apply(rule_tac x="pi\<bullet>x" in a7) |
|
430 apply(simp add: fresh_bij) |
|
431 apply(drule equiv_def_eqvt) |
|
432 apply(simp)+ |
|
433 done |
|
434 next |
|
435 case (Q_Abs x \<Gamma> T1 s2 t2 T2 pi c) |
|
436 obtain y::"name" where fs: "y\<sharp>(pi\<bullet>x,pi\<bullet>s2,pi\<bullet>t2,pi\<bullet>\<Gamma>,c)" by (rule exists_fresh[OF fs_name1]) |
|
437 let ?sw="[(pi\<bullet>x,y)]" |
|
438 let ?pi'="?sw@pi" |
|
439 have f1: "x\<sharp>\<Gamma>" by fact |
|
440 have f2: "(pi\<bullet>x)\<sharp>(pi\<bullet>\<Gamma>)" using f1 by (simp add: fresh_bij) |
|
441 have f3: "y\<sharp>?pi'\<bullet>\<Gamma>" using f1 by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp) |
|
442 have pr1: "(x,T1)#\<Gamma> \<turnstile> s2 == t2 : T2" by fact |
|
443 then have "?pi'\<bullet>((x,T1)#\<Gamma>) \<turnstile> (?pi'\<bullet>s2) == (?pi'\<bullet>t2) : T2" by (rule equiv_def_eqvt) |
|
444 then have "((y,T1)#(?pi'\<bullet>\<Gamma>)) \<turnstile> (?pi'\<bullet>s2) == (?pi'\<bullet>t2) : T2" by (simp add: calc_atm) |
|
445 moreover |
|
446 have ih1: "\<And>c. P c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>s2) (?pi'\<bullet>t2) T2" by fact |
|
447 then have "\<And>c. P c ((y,T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>s2) (?pi'\<bullet>t2) T2" by (simp add: calc_atm) |
|
448 ultimately have "P c (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>Lam [x].s2) (?pi'\<bullet>Lam [x].t2) (T1\<rightarrow>T2)" using a4 f3 fs |
|
449 by (simp add: calc_atm) |
|
450 then have "P c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>Lam [(pi\<bullet>x)].(pi\<bullet>s2)) (?sw\<bullet>Lam [(pi\<bullet>x)].(pi\<bullet>t2)) (T1\<rightarrow>T2)" |
|
451 by (simp del: append_Cons add: calc_atm pt_name2) |
|
452 moreover have "(?sw\<bullet>(pi\<bullet>\<Gamma>)) = (pi\<bullet>\<Gamma>)" |
|
453 by (rule perm_fresh_fresh) (simp_all add: fs f2) |
|
454 moreover have "(?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>s2))) = Lam [(pi\<bullet>x)].(pi\<bullet>s2)" |
|
455 by (rule perm_fresh_fresh) (simp_all add: fs f2 abs_fresh) |
|
456 moreover have "(?sw\<bullet>(Lam [(pi\<bullet>x)].(pi\<bullet>t2))) = Lam [(pi\<bullet>x)].(pi\<bullet>t2)" |
|
457 by (rule perm_fresh_fresh) (simp_all add: fs f2 abs_fresh) |
|
458 ultimately have "P c (pi\<bullet>\<Gamma>) (Lam [(pi\<bullet>x)].(pi\<bullet>s2)) (Lam [(pi\<bullet>x)].(pi\<bullet>t2)) (T1\<rightarrow>T2)" by simp |
|
459 then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>Lam [x].s2) (pi\<bullet>Lam [x].t2) (T1\<rightarrow>T2)" by simp |
|
460 next |
|
461 case (Q_Beta x \<Gamma> s2 t2 T1 s12 t12 T2 pi c) |
|
462 obtain y::"name" where fs: "y\<sharp>(pi\<bullet>x,pi\<bullet>s12,pi\<bullet>t12,pi\<bullet>s2,pi\<bullet>t2,pi\<bullet>\<Gamma>,c)" |
|
463 by (rule exists_fresh[OF fs_name1]) |
|
464 let ?sw="[(pi\<bullet>x,y)]" |
|
465 let ?pi'="?sw@pi" |
|
466 have f1: "x\<sharp>(\<Gamma>,s2,t2)" by fact |
|
467 have f2: "(pi\<bullet>x)\<sharp>(pi\<bullet>(\<Gamma>,s2,t2))" using f1 by (simp add: fresh_bij) |
|
468 have f3: "y\<sharp>(?pi'\<bullet>(\<Gamma>,s2,t2))" using f1 |
|
469 by (auto simp add: pt_name2 fresh_left calc_atm perm_pi_simp fresh_prod) |
|
470 have pr1: "(x,T1)#\<Gamma> \<turnstile> s12 == t12 : T2" by fact |
|
471 then have "?pi'\<bullet>((x,T1)#\<Gamma>) \<turnstile> (?pi'\<bullet>s12) == (?pi'\<bullet>t12) : T2" by (rule equiv_def_eqvt) |
|
472 then have "((y,T1)#(?pi'\<bullet>\<Gamma>)) \<turnstile> (?pi'\<bullet>s12) == (?pi'\<bullet>t12) : T2" by (simp add: calc_atm) |
|
473 moreover |
|
474 have ih1: "\<And>c. P c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>s12) (?pi'\<bullet>t12) T2" by fact |
|
475 then have "\<And>c. P c ((y,T1)#(?pi'\<bullet>\<Gamma>)) (?pi'\<bullet>s12) (?pi'\<bullet>t12) T2" by (simp add: calc_atm) |
|
476 moreover |
|
477 have pr2: "\<Gamma> \<turnstile> s2 == t2 : T1" by fact |
|
478 then have "(?pi'\<bullet>\<Gamma>) \<turnstile> (?pi'\<bullet>s2) == (?pi'\<bullet>t2) : T1" by (rule equiv_def_eqvt) |
|
479 moreover |
|
480 have ih2: "\<And>c. P c (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>s2) (?pi'\<bullet>t2) T1" by fact |
|
481 ultimately have "P c (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>(App (Lam [x].s12) s2)) (?pi'\<bullet>(t12[x::=t2])) T2" |
|
482 using a6 f3 fs by (simp add: subst_eqvt calc_atm) |
|
483 then have "P c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>(App (Lam [(pi\<bullet>x)].(pi\<bullet>s12)) (pi\<bullet>s2))) |
|
484 (?sw\<bullet>((pi\<bullet>t12)[(pi\<bullet>x)::=(pi\<bullet>t2)])) T2" |
|
485 by (simp del: append_Cons add: calc_atm pt_name2 subst_eqvt) |
|
486 moreover have "(?sw\<bullet>(pi\<bullet>\<Gamma>)) = (pi\<bullet>\<Gamma>)" |
|
487 by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified]) |
|
488 moreover have "(?sw\<bullet>(App (Lam [(pi\<bullet>x)].(pi\<bullet>s12)) (pi\<bullet>s2))) = App (Lam [(pi\<bullet>x)].(pi\<bullet>s12)) (pi\<bullet>s2)" |
|
489 by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified] abs_fresh) |
|
490 moreover have "(?sw\<bullet>((pi\<bullet>t12)[(pi\<bullet>x)::=(pi\<bullet>t2)])) = ((pi\<bullet>t12)[(pi\<bullet>x)::=(pi\<bullet>t2)])" |
|
491 by (rule perm_fresh_fresh) |
|
492 (simp_all add: fs[simplified] f2[simplified] fresh_subst fresh_subst'') |
|
493 ultimately have "P c (pi\<bullet>\<Gamma>) (App (Lam [(pi\<bullet>x)].(pi\<bullet>s12)) (pi\<bullet>s2)) ((pi\<bullet>t12)[(pi\<bullet>x)::=(pi\<bullet>t2)]) T2" |
|
494 by simp |
|
495 then show "P c (pi\<bullet>\<Gamma>) (pi\<bullet>App (Lam [x].s12) s2) (pi\<bullet>t12[x::=t2]) T2" by (simp add: subst_eqvt) |
|
496 qed |
|
497 then have "P c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>s) (([]::name prm)\<bullet>t) T" by blast |
|
498 then show "P c \<Gamma> s t T" by simp |
|
499 qed |
|
500 |
|
501 text {* Weak head reduction *} |
|
502 |
|
503 inductive2 |
|
504 whr_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<leadsto> _" [80,80] 80) |
|
505 where |
|
506 QAR_Beta[intro]: "App (Lam [x]. t12) t2 \<leadsto> t12[x::=t2]" |
|
507 | QAR_App[intro]: "t1 \<leadsto> t1' \<Longrightarrow> App t1 t2 \<leadsto> App t1' t2" |
|
508 |
|
509 declare trm.inject [simp add] |
|
510 declare ty.inject [simp add] |
|
511 |
|
512 inductive_cases2 whr_Gen[elim]: "t \<leadsto> t'" |
|
513 inductive_cases2 whr_Lam[elim]: "Lam [x].t \<leadsto> t'" |
|
514 inductive_cases2 whr_App_Lam[elim]: "App (Lam [x].t12) t2 \<leadsto> t" |
|
515 inductive_cases2 whr_Var[elim]: "Var x \<leadsto> t" |
|
516 inductive_cases2 whr_Const[elim]: "Const n \<leadsto> t" |
|
517 inductive_cases2 whr_App[elim]: "App p q \<leadsto> t" |
|
518 inductive_cases2 whr_Const_Right[elim]: "t \<leadsto> Const n" |
|
519 inductive_cases2 whr_Var_Right[elim]: "t \<leadsto> Var x" |
|
520 inductive_cases2 whr_App_Right[elim]: "t \<leadsto> App p q" |
|
521 |
|
522 declare trm.inject [simp del] |
|
523 declare ty.inject [simp del] |
|
524 |
|
525 text {* Weak head normalization *} |
|
526 |
|
527 abbreviation |
|
528 nf :: "trm \<Rightarrow> bool" ("_ \<leadsto>|" [100] 100) |
|
529 where |
|
530 "t\<leadsto>| \<equiv> \<not>(\<exists> u. t \<leadsto> u)" |
|
531 |
|
532 inductive2 |
|
533 whn_def :: "trm\<Rightarrow>trm\<Rightarrow>bool" ("_ \<Down> _" [80,80] 80) |
|
534 where |
|
535 QAN_Reduce[intro]: "\<lbrakk>s \<leadsto> t; t \<Down> u\<rbrakk> \<Longrightarrow> s \<Down> u" |
|
536 | QAN_Normal[intro]: "t\<leadsto>| \<Longrightarrow> t \<Down> t" |
|
537 |
|
538 lemma whr_eqvt: |
|
539 fixes pi::"name prm" |
|
540 assumes a: "t \<leadsto> t'" |
|
541 shows "(pi\<bullet>t) \<leadsto> (pi\<bullet>t')" |
|
542 using a |
|
543 apply(induct) |
|
544 apply(auto simp add: subst_eqvt fresh_bij) |
|
545 done |
|
546 |
|
547 lemma whn_eqvt: |
|
548 fixes pi::"name prm" |
|
549 assumes a: "t \<Down> t'" |
|
550 shows "(pi\<bullet>t) \<Down> (pi\<bullet>t')" |
|
551 using a |
|
552 apply(induct) |
|
553 apply(rule QAN_Reduce) |
|
554 apply(rule whr_eqvt) |
|
555 apply(assumption)+ |
|
556 apply(rule QAN_Normal) |
|
557 apply(auto) |
|
558 apply(drule_tac pi="rev pi" in whr_eqvt) |
|
559 apply(perm_simp) |
|
560 done |
|
561 |
|
562 text {* Algorithmic term equivalence and algorithmic path equivalence *} |
|
563 |
|
564 inductive2 |
|
565 alg_equiv :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ <=> _ : _" [60,60] 60) |
|
566 and |
|
567 alg_path_equiv :: "(name\<times>ty) list\<Rightarrow>trm\<Rightarrow>trm\<Rightarrow>ty\<Rightarrow>bool" ("_ \<turnstile> _ \<leftrightarrow> _ : _" [60,60] 60) |
|
568 where |
|
569 QAT_Base[intro]: "\<lbrakk>s \<Down> p; t \<Down> q; \<Gamma> \<turnstile> p \<leftrightarrow> q : TBase \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s <=> t : TBase" |
|
570 | QAT_Arrow[intro]: "\<lbrakk>x\<sharp>\<Gamma>; x\<sharp>s; x\<sharp>t; (x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> App t (Var x) : T2\<rbrakk> |
|
571 \<Longrightarrow> \<Gamma> \<turnstile> s <=> t : T1 \<rightarrow> T2" |
|
572 | QAT_One[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> s <=> t : TUnit" |
|
573 | QAP_Var[intro]: "\<lbrakk>valid \<Gamma>;(x,T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> Var x \<leftrightarrow> Var x : T" |
|
574 | QAP_App[intro]: "\<lbrakk>\<Gamma> \<turnstile> p \<leftrightarrow> q : T1 \<rightarrow> T2; \<Gamma> \<turnstile> s <=> t : T1 \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> App p s \<leftrightarrow> App q t : T2" |
|
575 | QAP_Const[intro]: "valid \<Gamma> \<Longrightarrow> \<Gamma> \<turnstile> Const n \<leftrightarrow> Const n : TBase" |
|
576 |
|
577 lemma alg_equiv_alg_path_equiv_eqvt: |
|
578 fixes pi::"name prm" |
|
579 shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) <=> (pi\<bullet>t) : T" |
|
580 and "\<Gamma> \<turnstile> p \<leftrightarrow> q : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>p) \<leftrightarrow> (pi\<bullet>q) : T" |
|
581 apply(induct rule: alg_equiv_alg_path_equiv.inducts) |
|
582 apply(auto intro: whn_eqvt simp add: fresh_bij valid_eqvt) |
|
583 apply(rule_tac x="pi\<bullet>x" in QAT_Arrow) |
|
584 apply(auto simp add: fresh_bij) |
|
585 apply(rule QAP_Var) |
|
586 apply(simp add: valid_eqvt) |
|
587 apply(simp add: pt_list_set_pi[OF pt_name_inst, symmetric]) |
|
588 apply(perm_simp add: pt_set_bij1a[OF pt_name_inst, OF at_name_inst]) |
|
589 done |
|
590 |
|
591 lemma alg_equiv_alg_path_equiv_strong_induct |
|
592 [case_names QAT_Base QAT_Arrow QAT_One QAP_Var QAP_App QAP_Const]: |
|
593 fixes c::"'a::fs_name" |
|
594 assumes a1: "\<And>s p t q \<Gamma> c. \<lbrakk>s \<Down> p; t \<Down> q; \<Gamma> \<turnstile> p \<leftrightarrow> q : TBase; \<And>d. P2 d \<Gamma> p q TBase\<rbrakk> |
|
595 \<Longrightarrow> P1 c \<Gamma> s t TBase" |
|
596 and a2: "\<And>x \<Gamma> s t T1 T2 c. |
|
597 \<lbrakk>x\<sharp>\<Gamma>; x\<sharp>s; x\<sharp>t; x\<sharp>c; (x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> App t (Var x) : T2; |
|
598 \<And>d. P1 d ((x,T1)#\<Gamma>) (App s (Var x)) (App t (Var x)) T2\<rbrakk> |
|
599 \<Longrightarrow> P1 c \<Gamma> s t (T1\<rightarrow>T2)" |
|
600 and a3: "\<And>\<Gamma> s t c. valid \<Gamma> \<Longrightarrow> P1 c \<Gamma> s t TUnit" |
|
601 and a4: "\<And>\<Gamma> x T c. \<lbrakk>valid \<Gamma>; (x,T) \<in> set \<Gamma>\<rbrakk> \<Longrightarrow> P2 c \<Gamma> (Var x) (Var x) T" |
|
602 and a5: "\<And>\<Gamma> p q T1 T2 s t c. |
|
603 \<lbrakk>\<Gamma> \<turnstile> p \<leftrightarrow> q : T1\<rightarrow>T2; \<And>d. P2 d \<Gamma> p q (T1\<rightarrow>T2); \<Gamma> \<turnstile> s <=> t : T1; \<And>d. P1 d \<Gamma> s t T1\<rbrakk> |
|
604 \<Longrightarrow> P2 c \<Gamma> (App p s) (App q t) T2" |
|
605 and a6: "\<And>\<Gamma> n c. valid \<Gamma> \<Longrightarrow> P2 c \<Gamma> (Const n) (Const n) TBase" |
|
606 shows "(\<Gamma> \<turnstile> s <=> t : T \<longrightarrow>P1 c \<Gamma> s t T) \<and> (\<Gamma>' \<turnstile> s' \<leftrightarrow> t' : T' \<longrightarrow> P2 c \<Gamma>' s' t' T')" |
|
607 proof - |
|
608 have "(\<Gamma> \<turnstile> s <=> t : T \<longrightarrow> (\<forall>c (pi::name prm). P1 c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) T)) \<and> |
|
609 (\<Gamma>' \<turnstile> s' \<leftrightarrow> t' : T' \<longrightarrow> (\<forall>c (pi::name prm). P2 c (pi\<bullet>\<Gamma>') (pi\<bullet>s') (pi\<bullet>t') T'))" |
|
610 proof(induct rule: alg_equiv_alg_path_equiv.induct) |
|
611 case (QAT_Base s q t p \<Gamma>) |
|
612 then show "\<forall>c (pi::name prm). P1 c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) TBase" |
|
613 apply(auto) |
|
614 apply(rule_tac p="pi\<bullet>q" and q="pi\<bullet>p" in a1) |
|
615 apply(simp_all add: whn_eqvt alg_equiv_alg_path_equiv_eqvt) |
|
616 done |
|
617 next |
|
618 case (QAT_Arrow x \<Gamma> s t T1 T2) |
|
619 show ?case |
|
620 proof (rule allI, rule allI) |
|
621 fix c::"'a::fs_name" and pi::"name prm" |
|
622 obtain y::"name" where fs: "y\<sharp>(pi\<bullet>s,pi\<bullet>t,pi\<bullet>\<Gamma>,c)" by (rule exists_fresh[OF fs_name1]) |
|
623 let ?sw="[(pi\<bullet>x,y)]" |
|
624 let ?pi'="?sw@pi" |
|
625 have f0: "x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact |
|
626 then have f1: "x\<sharp>(\<Gamma>,s,t)" by simp |
|
627 have f2: "(pi\<bullet>x)\<sharp>(pi\<bullet>(\<Gamma>,s,t))" using f1 by (simp add: fresh_bij) |
|
628 have f3: "y\<sharp>?pi'\<bullet>(\<Gamma>,s,t)" using f1 |
|
629 by (simp only: pt_name2 fresh_left, auto simp add: perm_pi_simp calc_atm) |
|
630 then have f3': "y\<sharp>?pi'\<bullet>\<Gamma>" "y\<sharp>?pi'\<bullet>s" "y\<sharp>?pi'\<bullet>t" by (auto simp add: fresh_prod) |
|
631 have pr1: "(x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> App t (Var x) : T2" by fact |
|
632 then have "(?pi'\<bullet>((x,T1)#\<Gamma>)) \<turnstile> (?pi'\<bullet>(App s (Var x))) <=> (?pi'\<bullet>(App t (Var x))) : T2" |
|
633 by (simp only: alg_equiv_alg_path_equiv_eqvt) |
|
634 then have "(y,T1)#(?pi'\<bullet>\<Gamma>) \<turnstile> (App (?pi'\<bullet>s) (Var y)) <=> (App (?pi'\<bullet>t) (Var y)) : T2" |
|
635 by (simp add: calc_atm) |
|
636 moreover |
|
637 have ih1: "\<forall>c (pi::name prm). P1 c (pi\<bullet>((x,T1)#\<Gamma>)) (pi\<bullet>App s (Var x)) (pi\<bullet>App t (Var x)) T2" |
|
638 by fact |
|
639 then have "\<And>c. P1 c (?pi'\<bullet>((x,T1)#\<Gamma>)) (?pi'\<bullet>App s (Var x)) (?pi'\<bullet>App t (Var x)) T2" |
|
640 by auto |
|
641 then have "\<And>c. P1 c ((y,T1)#(?pi'\<bullet>\<Gamma>)) (App (?pi'\<bullet>s) (Var y)) (App (?pi'\<bullet>t) (Var y)) T2" |
|
642 by (simp add: calc_atm) |
|
643 ultimately have "P1 c (?pi'\<bullet>\<Gamma>) (?pi'\<bullet>s) (?pi'\<bullet>t) (T1\<rightarrow>T2)" using a2 f3' fs by simp |
|
644 then have "P1 c (?sw\<bullet>pi\<bullet>\<Gamma>) (?sw\<bullet>pi\<bullet>s) (?sw\<bullet>pi\<bullet>t) (T1\<rightarrow>T2)" |
|
645 by (simp del: append_Cons add: calc_atm pt_name2) |
|
646 moreover have "(?sw\<bullet>(pi\<bullet>\<Gamma>)) = (pi\<bullet>\<Gamma>)" |
|
647 by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified]) |
|
648 moreover have "(?sw\<bullet>(pi\<bullet>s)) = (pi\<bullet>s)" |
|
649 by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified]) |
|
650 moreover have "(?sw\<bullet>(pi\<bullet>t)) = (pi\<bullet>t)" |
|
651 by (rule perm_fresh_fresh) (simp_all add: fs[simplified] f2[simplified]) |
|
652 ultimately show "P1 c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) (T1\<rightarrow>T2)" by (simp) |
|
653 qed |
|
654 next |
|
655 case (QAT_One \<Gamma> s t) |
|
656 then show "\<forall>c (pi::name prm). P1 c (pi\<bullet>\<Gamma>) (pi\<bullet>s) (pi\<bullet>t) TUnit" |
|
657 by (auto intro!: a3 simp add: valid_eqvt) |
|
658 next |
|
659 case (QAP_Var \<Gamma> x T) |
|
660 then show "\<forall>c (pi::name prm). P2 c (pi \<bullet> \<Gamma>) (pi \<bullet> Var x) (pi \<bullet> Var x) T" |
|
661 apply(auto intro!: a4 simp add: valid_eqvt) |
|
662 apply(simp add: pt_list_set_pi[OF pt_name_inst, symmetric]) |
|
663 apply(perm_simp add: pt_set_bij1a[OF pt_name_inst, OF at_name_inst]) |
|
664 done |
|
665 next |
|
666 case (QAP_App \<Gamma> p q T1 T2 s t) |
|
667 then show "\<forall>c (pi::name prm). P2 c (pi\<bullet>\<Gamma>) (pi\<bullet>App p s) (pi\<bullet>App q t) T2" |
|
668 by (auto intro!: a5 simp add: alg_equiv_alg_path_equiv_eqvt) |
|
669 next |
|
670 case (QAP_Const \<Gamma> n) |
|
671 then show "\<forall>c (pi::name prm). P2 c (pi\<bullet>\<Gamma>) (pi\<bullet>Const n) (pi\<bullet>Const n) TBase" |
|
672 by (auto intro!: a6 simp add: valid_eqvt) |
|
673 qed |
|
674 then have "(\<Gamma> \<turnstile> s <=> t : T \<longrightarrow> P1 c (([]::name prm)\<bullet>\<Gamma>) (([]::name prm)\<bullet>s) (([]::name prm)\<bullet>t) T) \<and> |
|
675 (\<Gamma>' \<turnstile> s' \<leftrightarrow> t' : T' \<longrightarrow> P2 c (([]::name prm)\<bullet>\<Gamma>') (([]::name prm)\<bullet>s') (([]::name prm)\<bullet>t') T')" |
|
676 by blast |
|
677 then show ?thesis by simp |
|
678 qed |
|
679 |
|
680 (* post-processing of the strong induction principle *) |
|
681 (* extracts the strong_inducts-version from strong_induct *) |
|
682 |
|
683 setup {* |
|
684 PureThy.add_thmss |
|
685 [(("alg_equiv_alg_path_equiv_strong_inducts", |
|
686 ProjectRule.projects (ProofContext.init (the_context())) [1,2] |
|
687 (thm "alg_equiv_alg_path_equiv_strong_induct")), [])] #> snd |
|
688 *} |
|
689 |
|
690 declare trm.inject [simp add] |
|
691 declare ty.inject [simp add] |
|
692 |
|
693 inductive_cases2 whn_inv_auto[elim]: "t \<Down> t'" |
|
694 |
|
695 inductive_cases2 alg_equiv_Base_inv_auto[elim]: "\<Gamma> \<turnstile> s<=>t : TBase" |
|
696 inductive_cases2 alg_equiv_Arrow_inv_auto[elim]: "\<Gamma> \<turnstile> s<=>t : T1 \<rightarrow> T2" |
|
697 |
|
698 inductive_cases2 alg_path_equiv_Base_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : TBase" |
|
699 inductive_cases2 alg_path_equiv_Unit_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : TUnit" |
|
700 inductive_cases2 alg_path_equiv_Arrow_inv_auto[elim]: "\<Gamma> \<turnstile> s\<leftrightarrow>t : T1 \<rightarrow> T2" |
|
701 |
|
702 inductive_cases2 alg_path_equiv_Var_left_inv_auto[elim]: "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T" |
|
703 inductive_cases2 alg_path_equiv_Var_left_inv_auto'[elim]: "\<Gamma> \<turnstile> Var x \<leftrightarrow> t : T'" |
|
704 inductive_cases2 alg_path_equiv_Var_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T" |
|
705 inductive_cases2 alg_path_equiv_Var_right_inv_auto'[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Var x : T'" |
|
706 inductive_cases2 alg_path_equiv_Const_left_inv_auto[elim]: "\<Gamma> \<turnstile> Const n \<leftrightarrow> t : T" |
|
707 inductive_cases2 alg_path_equiv_Const_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> Const n : T" |
|
708 inductive_cases2 alg_path_equiv_App_left_inv_auto[elim]: "\<Gamma> \<turnstile> App p s \<leftrightarrow> t : T" |
|
709 inductive_cases2 alg_path_equiv_App_right_inv_auto[elim]: "\<Gamma> \<turnstile> s \<leftrightarrow> App q t : T" |
|
710 inductive_cases2 alg_path_equiv_Lam_left_inv_auto[elim]: "\<Gamma> \<turnstile> Lam[x].s \<leftrightarrow> t : T" |
|
711 inductive_cases2 alg_path_equiv_Lam_right_inv_auto[elim]: "\<Gamma> \<turnstile> t \<leftrightarrow> Lam[x].s : T" |
|
712 |
|
713 declare trm.inject [simp del] |
|
714 declare ty.inject [simp del] |
|
715 |
|
716 text {* Subcontext. *} |
|
717 |
|
718 abbreviation |
|
719 "sub" :: "(name\<times>ty) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" (" _ \<lless> _ " [55,55] 55) |
|
720 where |
|
721 "\<Gamma>1 \<lless> \<Gamma>2 \<equiv> (\<forall>a \<sigma>. (a,\<sigma>)\<in>set \<Gamma>1 \<longrightarrow> (a,\<sigma>)\<in>set \<Gamma>2) \<and> valid \<Gamma>2" |
|
722 |
|
723 lemma alg_equiv_valid: |
|
724 shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> valid \<Gamma>" and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> valid \<Gamma>" |
|
725 by (induct rule : alg_equiv_alg_path_equiv.inducts, auto) |
|
726 |
|
727 lemma algorithmic_monotonicity: |
|
728 fixes \<Gamma>':: "(name\<times>ty) list" |
|
729 shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> \<Gamma>\<lless>\<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s <=> t : T" |
|
730 and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> \<Gamma>\<lless>\<Gamma>' \<Longrightarrow> \<Gamma>' \<turnstile> s \<leftrightarrow> t : T" |
|
731 proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: \<Gamma>' rule: alg_equiv_alg_path_equiv_strong_inducts) |
|
732 case (QAT_Arrow x \<Gamma> s t T1 T2 \<Gamma>') |
|
733 have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact |
|
734 have h1:"(x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> App t (Var x) : T2" by fact |
|
735 have h2:"\<Gamma>\<lless>\<Gamma>'" by fact |
|
736 have ih:"\<And>\<Gamma>'. \<lbrakk>(x,T1)#\<Gamma> \<lless> \<Gamma>'\<rbrakk> \<Longrightarrow> \<Gamma>' \<turnstile> App s (Var x) <=> App t (Var x) : T2" by fact |
|
737 have "x\<sharp>\<Gamma>'" by fact |
|
738 then have sub:"(x,T1)#\<Gamma> \<lless> (x,T1)#\<Gamma>'" using h2 by auto |
|
739 then have "(x,T1)#\<Gamma>' \<turnstile> App s (Var x) <=> App t (Var x) : T2" using ih by auto |
|
740 then show "\<Gamma>' \<turnstile> s <=> t : T1\<rightarrow>T2" using sub fs by auto |
|
741 qed (auto) |
|
742 |
|
743 text {* Logical equivalence. *} |
|
744 |
|
745 function log_equiv :: "((name\<times>ty) list \<Rightarrow> trm \<Rightarrow> trm \<Rightarrow> ty \<Rightarrow> bool)" |
|
746 ("_ \<turnstile> _ is _ : _" [60,60,60,60] 60) |
|
747 where |
|
748 "\<Gamma> \<turnstile> s is t : TUnit = valid \<Gamma>" |
|
749 | "\<Gamma> \<turnstile> s is t : TBase = \<Gamma> \<turnstile> s <=> t : TBase" |
|
750 | "\<Gamma> \<turnstile> s is t : (T1 \<rightarrow> T2) = (valid \<Gamma> \<and> (\<forall>\<Gamma>' s' t'. \<Gamma>\<lless>\<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T1 \<longrightarrow> (\<Gamma>' \<turnstile> (App s s') is (App t t') : T2)))" |
|
751 apply (auto simp add: ty.inject) |
|
752 apply (subgoal_tac "(\<exists> T1 T2. b=T1 \<rightarrow> T2) \<or> b=TUnit \<or> b=TBase" ) |
|
753 apply (force) |
|
754 apply (rule ty_cases) |
|
755 done |
|
756 |
|
757 termination |
|
758 apply(relation "measure (\<lambda>(_,_,_,T). size T)") |
|
759 apply(auto) |
|
760 done |
|
761 |
|
762 lemma log_equiv_valid: |
|
763 assumes "\<Gamma> \<turnstile> s is t : T" |
|
764 shows "valid \<Gamma>" |
|
765 using assms |
|
766 by (induct rule: log_equiv.induct,auto elim: alg_equiv_valid) |
|
767 |
|
768 lemma logical_monotonicity : |
|
769 fixes T::ty |
|
770 assumes "\<Gamma> \<turnstile> s is t : T" "\<Gamma>\<lless>\<Gamma>'" |
|
771 shows "\<Gamma>' \<turnstile> s is t : T" |
|
772 using assms |
|
773 proof (induct arbitrary: \<Gamma>' rule: log_equiv.induct) |
|
774 case (2 \<Gamma> s t \<Gamma>') |
|
775 then show "\<Gamma>' \<turnstile> s is t : TBase" using algorithmic_monotonicity by auto |
|
776 next |
|
777 case (3 \<Gamma> s t T1 T2 \<Gamma>') |
|
778 have h1:"\<Gamma> \<turnstile> s is t : T1\<rightarrow>T2" by fact |
|
779 have h2:"\<Gamma>\<lless>\<Gamma>'" by fact |
|
780 { |
|
781 fix \<Gamma>'' s' t' |
|
782 assume "\<Gamma>'\<lless>\<Gamma>''" "\<Gamma>'' \<turnstile> s' is t' : T1" |
|
783 then have "\<Gamma>'' \<turnstile> (App s s') is (App t t') : T2" using h1 h2 by auto |
|
784 } |
|
785 then show "\<Gamma>' \<turnstile> s is t : T1\<rightarrow>T2" using h2 by auto |
|
786 qed (auto) |
|
787 |
|
788 lemma forget: |
|
789 fixes x::"name" |
|
790 and L::"trm" |
|
791 assumes a: "x\<sharp>L" |
|
792 shows "L[x::=P] = L" |
|
793 using a |
|
794 by (nominal_induct L avoiding: x P rule: trm.induct) |
|
795 (auto simp add: fresh_atm abs_fresh) |
|
796 |
|
797 lemma subst_fun_eq: |
|
798 fixes u::trm |
|
799 assumes h:"[x].t1 = [y].t2" |
|
800 shows "t1[x::=u] = t2[y::=u]" |
|
801 proof - |
|
802 { |
|
803 assume "x=y" and "t1=t2" |
|
804 then have ?thesis using h by simp |
|
805 } |
|
806 moreover |
|
807 { |
|
808 assume h1:"x \<noteq> y" and h2:"t1=[(x,y)] \<bullet> t2" and h3:"x \<sharp> t2" |
|
809 then have "([(x,y)] \<bullet> t2)[x::=u] = t2[y::=u]" by (simp add: subst_rename) |
|
810 then have ?thesis using h2 by simp |
|
811 } |
|
812 ultimately show ?thesis using alpha h by blast |
|
813 qed |
|
814 |
|
815 lemma psubst_empty[simp]: |
|
816 shows "[]<t> = t" |
|
817 by (nominal_induct t rule: trm.induct) (auto simp add: fresh_list_nil) |
|
818 |
|
819 lemma psubst_subst_psubst: |
|
820 assumes h:"c \<sharp> \<theta>" |
|
821 shows "\<theta><t>[c::=s] = (c,s)#\<theta><t>" |
|
822 using h |
|
823 apply(nominal_induct t avoiding: \<theta> c s rule: trm.induct) |
|
824 apply(auto simp add: fresh_list_cons fresh_atm forget lookup_fresh lookup_fresh' fresh_psubst) |
|
825 done |
|
826 |
|
827 lemma subst_fresh_simpl: |
|
828 assumes "x\<sharp>\<theta>" |
|
829 shows "\<theta><Var x> = Var x" |
|
830 using assms |
|
831 by (induct \<theta> arbitrary: x, auto simp add:fresh_list_cons fresh_prod fresh_atm) |
|
832 |
|
833 lemma psubst_subst_propagate: |
|
834 assumes "x\<sharp>\<theta>" |
|
835 shows "\<theta><t[x::=u]> = \<theta><t>[x::=\<theta><u>]" |
|
836 using assms |
|
837 proof (nominal_induct t avoiding: x u \<theta> rule: trm.induct) |
|
838 case (Var n x u \<theta>) |
|
839 { assume "x=n" |
|
840 moreover have "x\<sharp>\<theta>" by fact |
|
841 ultimately have "\<theta><Var n[x::=u]> = \<theta><Var n>[x::=\<theta><u>]" using subst_fresh_simpl by auto |
|
842 } |
|
843 moreover |
|
844 { assume h:"x\<noteq>n" |
|
845 then have "x\<sharp>Var n" by (auto simp add: fresh_atm) |
|
846 moreover have "x\<sharp>\<theta>" by fact |
|
847 ultimately have "x\<sharp>\<theta><Var n>" using fresh_psubst by blast |
|
848 then have " \<theta><Var n>[x::=\<theta><u>] = \<theta><Var n>" using forget by auto |
|
849 then have "\<theta><Var n[x::=u]> = \<theta><Var n>[x::=\<theta><u>]" using h by auto |
|
850 } |
|
851 ultimately show ?case by auto |
|
852 next |
|
853 case (Lam n t x u \<theta>) |
|
854 have fs:"n\<sharp>x" "n\<sharp>u" "n\<sharp>\<theta>" "x\<sharp>\<theta>" by fact |
|
855 have ih:"\<And> y s \<theta>. y\<sharp>\<theta> \<Longrightarrow> ((\<theta><(t[y::=s])>) = ((\<theta><t>)[y::=(\<theta><s>)]))" by fact |
|
856 have "\<theta> <(Lam [n].t)[x::=u]> = \<theta><Lam [n]. (t [x::=u])>" using fs by auto |
|
857 then have "\<theta> <(Lam [n].t)[x::=u]> = Lam [n]. \<theta><t [x::=u]>" using fs by auto |
|
858 moreover have "\<theta><t[x::=u]> = \<theta><t>[x::=\<theta><u>]" using ih fs by blast |
|
859 ultimately have "\<theta> <(Lam [n].t)[x::=u]> = Lam [n].(\<theta><t>[x::=\<theta><u>])" by auto |
|
860 moreover have "Lam [n].(\<theta><t>[x::=\<theta><u>]) = (Lam [n].\<theta><t>)[x::=\<theta><u>]" using fs fresh_psubst by auto |
|
861 ultimately have "\<theta><(Lam [n].t)[x::=u]> = (Lam [n].\<theta><t>)[x::=\<theta><u>]" using fs by auto |
|
862 then show "\<theta><(Lam [n].t)[x::=u]> = \<theta><Lam [n].t>[x::=\<theta><u>]" using fs by auto |
|
863 qed (auto) |
|
864 |
|
865 lemma fresh_subst_fresh: |
|
866 assumes "a\<sharp>e" |
|
867 shows "a\<sharp>t[a::=e]" |
|
868 using assms |
|
869 by (nominal_induct t avoiding: a e rule: trm.induct) |
|
870 (auto simp add: fresh_atm abs_fresh fresh_nat) |
|
871 |
|
872 lemma path_equiv_implies_nf: |
|
873 assumes "\<Gamma> \<turnstile> s \<leftrightarrow> t : T" |
|
874 shows "s \<leadsto>|" and "t \<leadsto>|" |
|
875 using assms |
|
876 by (induct rule: alg_equiv_alg_path_equiv.inducts (2)) (simp, auto) |
|
877 |
|
878 lemma path_equiv_implies_nf: |
|
879 shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> True" |
|
880 and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> s \<leadsto>|" |
|
881 "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> t \<leadsto>|" |
|
882 apply (induct rule: alg_equiv_alg_path_equiv.inducts) |
|
883 apply auto |
|
884 done |
|
885 |
|
886 lemma main_lemma: |
|
887 shows "\<Gamma> \<turnstile> s is t : T \<Longrightarrow> \<Gamma> \<turnstile> s <=> t : T" and "\<Gamma> \<turnstile> p \<leftrightarrow> q : T \<Longrightarrow> \<Gamma> \<turnstile> p is q : T" |
|
888 proof (nominal_induct T arbitrary: \<Gamma> s t p q rule:ty.induct) |
|
889 case (Arrow T1 T2) |
|
890 { |
|
891 case (1 \<Gamma> s t) |
|
892 have ih1:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s is t : T2 \<Longrightarrow> \<Gamma> \<turnstile> s <=> t : T2" by fact |
|
893 have ih2:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s \<leftrightarrow> t : T1 \<Longrightarrow> \<Gamma> \<turnstile> s is t : T1" by fact |
|
894 have h:"\<Gamma> \<turnstile> s is t : T1\<rightarrow>T2" by fact |
|
895 obtain x::name where fs:"x\<sharp>(\<Gamma>,s,t)" by (erule exists_fresh[OF fs_name1]) |
|
896 have "valid \<Gamma>" using h log_equiv_valid by auto |
|
897 then have v:"valid ((x,T1)#\<Gamma>)" using fs by auto |
|
898 then have "(x,T1)#\<Gamma> \<turnstile> Var x \<leftrightarrow> Var x : T1" by auto |
|
899 then have "(x,T1)#\<Gamma> \<turnstile> Var x is Var x : T1" using ih2 by auto |
|
900 then have "(x,T1)#\<Gamma> \<turnstile> App s (Var x) is App t (Var x) : T2" using h v by auto |
|
901 then have "(x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> App t (Var x) : T2" using ih1 by auto |
|
902 then show "\<Gamma> \<turnstile> s <=> t : T1\<rightarrow>T2" using fs by (auto simp add: fresh_prod) |
|
903 next |
|
904 case (2 \<Gamma> p q) |
|
905 have h:"\<Gamma> \<turnstile> p \<leftrightarrow> q : T1\<rightarrow>T2" by fact |
|
906 have ih1:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s \<leftrightarrow> t : T2 \<Longrightarrow> \<Gamma> \<turnstile> s is t : T2" by fact |
|
907 have ih2:"\<And>\<Gamma> s t. \<Gamma> \<turnstile> s is t : T1 \<Longrightarrow> \<Gamma> \<turnstile> s <=> t : T1" by fact |
|
908 { |
|
909 fix \<Gamma>' s t |
|
910 assume "\<Gamma>\<lless>\<Gamma>'" and hl:"\<Gamma>' \<turnstile> s is t : T1" |
|
911 then have "\<Gamma>' \<turnstile> p \<leftrightarrow> q : T1 \<rightarrow> T2" using h algorithmic_monotonicity by auto |
|
912 moreover have "\<Gamma>' \<turnstile> s <=> t : T1" using ih2 hl by auto |
|
913 ultimately have "\<Gamma>' \<turnstile> App p s \<leftrightarrow> App q t : T2" by auto |
|
914 then have "\<Gamma>' \<turnstile> App p s is App q t : T2" using ih1 by auto |
|
915 } |
|
916 moreover have "valid \<Gamma>" using h alg_equiv_valid by auto |
|
917 ultimately show "\<Gamma> \<turnstile> p is q : T1\<rightarrow>T2" by auto |
|
918 } |
|
919 next |
|
920 case TBase |
|
921 { case 2 |
|
922 have h:"\<Gamma> \<turnstile> s \<leftrightarrow> t : TBase" by fact |
|
923 then have "s \<leadsto>|" and "t \<leadsto>|" using path_equiv_implies_nf by auto |
|
924 then have "s \<Down> s" and "t \<Down> t" by auto |
|
925 then have "\<Gamma> \<turnstile> s <=> t : TBase" using h by auto |
|
926 then show "\<Gamma> \<turnstile> s is t : TBase" by auto |
|
927 } |
|
928 qed (auto elim:alg_equiv_valid) |
|
929 |
|
930 corollary corollary_main: |
|
931 assumes "\<Gamma> \<turnstile> s \<leftrightarrow> t : T" |
|
932 shows "\<Gamma> \<turnstile> s <=> t : T" |
|
933 using assms main_lemma by blast |
|
934 |
|
935 lemma algorithmic_symmetry_aux: |
|
936 shows "(\<Gamma> \<turnstile> s <=> t : T \<longrightarrow> \<Gamma> \<turnstile> t <=> s : T) \<and> (\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<longrightarrow> \<Gamma> \<turnstile> t \<leftrightarrow> s : T)" |
|
937 by (rule alg_equiv_alg_path_equiv.induct,auto) |
|
938 |
|
939 lemma algorithmic_symmetry: |
|
940 assumes "\<Gamma> \<turnstile> s <=> t : T" |
|
941 shows "\<Gamma> \<turnstile> t <=> s : T" |
|
942 using assms by (simp add: algorithmic_symmetry_aux) |
|
943 |
|
944 lemma algorithmic_path_symmetry: |
|
945 assumes "\<Gamma> \<turnstile> s \<leftrightarrow> t : T" |
|
946 shows "\<Gamma> \<turnstile> t \<leftrightarrow> s : T" |
|
947 using assms by (simp add: algorithmic_symmetry_aux) |
|
948 |
|
949 lemma red_unicity : |
|
950 assumes "x \<leadsto> a" "x \<leadsto> b" |
|
951 shows "a=b" |
|
952 using assms |
|
953 apply (induct arbitrary: b) |
|
954 apply (erule whr_App_Lam) |
|
955 apply (clarify) |
|
956 apply (rule subst_fun_eq) |
|
957 apply (force) |
|
958 apply (force) |
|
959 apply (erule whr_App) |
|
960 apply (blast)+ |
|
961 done |
|
962 |
|
963 lemma nf_unicity : |
|
964 assumes "x \<Down> a" "x \<Down> b" |
|
965 shows "a=b" |
|
966 using assms |
|
967 proof (induct arbitrary: b) |
|
968 case (QAN_Reduce x t a b) |
|
969 have h:"x \<leadsto> t" "t \<Down> a" by fact |
|
970 have ih:"\<And>b. t \<Down> b \<Longrightarrow> a = b" by fact |
|
971 have "x \<Down> b" by fact |
|
972 then obtain t' where "x \<leadsto> t'" and hl:"t' \<Down> b" using h by auto |
|
973 then have "t=t'" using h red_unicity by auto |
|
974 then show "a=b" using ih hl by auto |
|
975 qed (auto) |
|
976 |
|
977 lemma Q_eqvt : |
|
978 fixes pi:: "(name \<times> name) list" |
|
979 shows "\<Gamma> \<turnstile> s <=> t : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) <=> (pi\<bullet>t) : T" |
|
980 and "\<Gamma> \<turnstile> s \<leftrightarrow> t : T \<Longrightarrow> (pi\<bullet>\<Gamma>) \<turnstile> (pi\<bullet>s) \<leftrightarrow> (pi\<bullet>t) : T" |
|
981 using assms |
|
982 proof (induct rule:alg_equiv_alg_path_equiv.inducts) |
|
983 case (QAP_Var \<Gamma> x T) |
|
984 then have "pi\<bullet>(x,T) \<in> (pi\<bullet>(set \<Gamma>))" using in_eqvt by blast |
|
985 then have "(pi\<bullet>x,T) \<in> (set (pi\<bullet>\<Gamma>))" using set_eqvt perm_ty by auto |
|
986 moreover have "valid \<Gamma>" by fact |
|
987 ultimately show ?case using valid_eqvt by auto |
|
988 next |
|
989 case (QAT_Arrow x \<Gamma> s t T1 T2) |
|
990 then have h:"((pi\<bullet>x)\<sharp>(pi\<bullet>\<Gamma>))" "((pi\<bullet>x)\<sharp>(pi\<bullet>s))" "((pi\<bullet>x)\<sharp>(pi\<bullet>t))" using fresh_bij by auto |
|
991 have "(pi\<bullet>((x,T1)#\<Gamma>)) \<turnstile> pi \<bullet> (App s (Var x)) <=> pi \<bullet> (App t (Var x)) : T2" by fact |
|
992 then have "(pi\<bullet>((x,T1)#\<Gamma>)) \<turnstile> (App (pi\<bullet>s) (Var (pi\<bullet>x))) <=> (App (pi\<bullet>t) (Var (pi\<bullet>x))) : T2" by auto |
|
993 moreover have "pi\<bullet>((x,T1)#\<Gamma>) = (pi\<bullet>x,pi\<bullet>T1)#(pi\<bullet>\<Gamma>)" by auto |
|
994 ultimately have "((pi\<bullet>x,T1)#(pi\<bullet>\<Gamma>)) \<turnstile> (App (pi\<bullet>s) (Var (pi\<bullet>x))) <=> (App (pi\<bullet>t) (Var (pi\<bullet>x))) : T2" using perm_ty by auto |
|
995 then show ?case using h by auto |
|
996 qed (auto elim:whn_eqvt valid_eqvt) |
|
997 |
|
998 (* FIXME this lemma should not be here I am reinventing the wheel I guess *) |
|
999 |
|
1000 lemma perm_basic[simp]: |
|
1001 fixes x y ::name |
|
1002 shows "[(x,y)]\<bullet>y = x" |
|
1003 using assms using calc_atm by perm_simp |
|
1004 |
|
1005 lemma Q_Arrow_strong_inversion: |
|
1006 assumes fs:"x\<sharp>\<Gamma>" "x\<sharp>t" "x\<sharp>u" and h:"\<Gamma> \<turnstile> t <=> u : T1\<rightarrow>T2" |
|
1007 shows "(x,T1)#\<Gamma> \<turnstile> App t (Var x) <=> App u (Var x) : T2" |
|
1008 proof - |
|
1009 obtain y where fs2:"y\<sharp>\<Gamma>" "y\<sharp>u" "y\<sharp>t" and "(y,T1)#\<Gamma> \<turnstile> App t (Var y) <=> App u (Var y) : T2" using h by auto |
|
1010 then have "([(x,y)]\<bullet>((y,T1)#\<Gamma>)) \<turnstile> [(x,y)]\<bullet> App t (Var y) <=> [(x,y)]\<bullet> App u (Var y) : T2" using Q_eqvt by blast |
|
1011 then show ?thesis using fs fs2 by (perm_simp) |
|
1012 qed |
|
1013 |
|
1014 lemma fresh_context[rule_format]: |
|
1015 fixes \<Gamma> :: "(name\<times>ty)list" |
|
1016 and a :: "name" |
|
1017 assumes "a\<sharp>\<Gamma>" |
|
1018 shows "\<not>(\<exists>\<tau>::ty. (a,\<tau>)\<in>set \<Gamma>)" |
|
1019 using assms by(induct \<Gamma>, auto simp add: fresh_prod fresh_list_cons fresh_atm) |
|
1020 |
|
1021 lemma type_unicity_in_context: |
|
1022 fixes \<Gamma> :: "(name\<times>ty)list" |
|
1023 and pi:: "name prm" |
|
1024 and a :: "name" |
|
1025 and \<tau> :: "ty" |
|
1026 assumes "valid \<Gamma>" and "(x,T1) \<in> set \<Gamma>" and "(x,T2) \<in> set \<Gamma>" |
|
1027 shows "T1=T2" |
|
1028 using assms by (induct \<Gamma>, auto dest!: fresh_context) |
|
1029 |
|
1030 (* |
|
1031 |
|
1032 Warning: This lemma is false. |
|
1033 |
|
1034 lemma algorithmic_type_unicity: |
|
1035 shows "\<lbrakk> \<Gamma> \<turnstile> s <=> t : T ; \<Gamma> \<turnstile> s <=> u : T' \<rbrakk> \<Longrightarrow> T = T'" |
|
1036 and "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'" |
|
1037 |
|
1038 Here is the counter example : |
|
1039 \<Gamma> \<turnstile> Const n <=> Const n : Tbase and \<Gamma> \<turnstile> Const n <=> Const n : TUnit |
|
1040 |
|
1041 *) |
|
1042 |
|
1043 lemma algorithmic_path_type_unicity: |
|
1044 shows "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> s \<leftrightarrow> u : T' \<rbrakk> \<Longrightarrow> T = T'" |
|
1045 proof (induct arbitrary: u T' rule:alg_equiv_alg_path_equiv.inducts(2) [of _ _ _ _ _ "%a b c d . True" ]) |
|
1046 case (QAP_Var \<Gamma> x T u T') |
|
1047 have "\<Gamma> \<turnstile> Var x \<leftrightarrow> u : T'" by fact |
|
1048 then have "u=Var x" and "(x,T') \<in> set \<Gamma>" by auto |
|
1049 moreover have "valid \<Gamma>" "(x,T) \<in> set \<Gamma>" by fact |
|
1050 ultimately show "T=T'" using type_unicity_in_context by auto |
|
1051 next |
|
1052 case (QAP_App \<Gamma> p q T1 T2 s t u T2') |
|
1053 have ih:"\<And>u T. \<Gamma> \<turnstile> p \<leftrightarrow> u : T \<Longrightarrow> T1\<rightarrow>T2 = T" by fact |
|
1054 have "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T2'" by fact |
|
1055 then obtain r t T1' where "u = App r t" "\<Gamma> \<turnstile> p \<leftrightarrow> r : T1' \<rightarrow> T2'" by auto |
|
1056 then have "T1\<rightarrow>T2 = T1' \<rightarrow> T2'" by auto |
|
1057 then show "T2=T2'" using ty.inject by auto |
|
1058 qed (auto) |
|
1059 |
|
1060 lemma algorithmic_transitivity: |
|
1061 shows "\<lbrakk> \<Gamma> \<turnstile> s <=> t : T ; \<Gamma> \<turnstile> t <=> u : T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s <=> u : T" |
|
1062 and "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> t \<leftrightarrow> u : T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s \<leftrightarrow> u : T" |
|
1063 proof (nominal_induct \<Gamma> s t T and \<Gamma> s t T avoiding: u rule: alg_equiv_alg_path_equiv_strong_inducts) |
|
1064 case (QAT_Base s p t q \<Gamma> u) |
|
1065 have h:"s \<Down> p" "t \<Down> q" by fact |
|
1066 have ih:"\<And>u. \<Gamma> \<turnstile> q \<leftrightarrow> u : TBase \<Longrightarrow> \<Gamma> \<turnstile> p \<leftrightarrow> u : TBase" by fact |
|
1067 have "\<Gamma> \<turnstile> t <=> u : TBase" by fact |
|
1068 then obtain r q' where hl:"t \<Down> q'" "u \<Down> r" "\<Gamma> \<turnstile> q' \<leftrightarrow> r : TBase" by auto |
|
1069 moreover have eq:"q=q'" using nf_unicity hl h by auto |
|
1070 ultimately have "\<Gamma> \<turnstile> p \<leftrightarrow> r : TBase" using ih by auto |
|
1071 then show "\<Gamma> \<turnstile> s <=> u : TBase" using hl h by auto |
|
1072 next |
|
1073 case (QAT_Arrow x \<Gamma> s t T1 T2 u) |
|
1074 have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact |
|
1075 moreover have h:"\<Gamma> \<turnstile> t <=> u : T1\<rightarrow>T2" by fact |
|
1076 moreover then obtain y where "y\<sharp>\<Gamma>" "y\<sharp>t" "y\<sharp>u" and "(y,T1)#\<Gamma> \<turnstile> App t (Var y) <=> App u (Var y) : T2" by auto |
|
1077 moreover have fs2:"x\<sharp>u" by fact |
|
1078 ultimately have "(x,T1)#\<Gamma> \<turnstile> App t (Var x) <=> App u (Var x) : T2" using Q_Arrow_strong_inversion by blast |
|
1079 moreover have ih:"\<And> v. (x,T1)#\<Gamma> \<turnstile> App t (Var x) <=> v : T2 \<Longrightarrow> (x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> v : T2" by fact |
|
1080 ultimately have "(x,T1)#\<Gamma> \<turnstile> App s (Var x) <=> App u (Var x) : T2" by auto |
|
1081 then show "\<Gamma> \<turnstile> s <=> u : T1\<rightarrow>T2" using fs fs2 by auto |
|
1082 next |
|
1083 case (QAP_App \<Gamma> p q T1 T2 s t u) |
|
1084 have h1:"\<Gamma> \<turnstile> p \<leftrightarrow> q : T1\<rightarrow>T2" by fact |
|
1085 have ih1:"\<And>u. \<Gamma> \<turnstile> q \<leftrightarrow> u : T1\<rightarrow>T2 \<Longrightarrow> \<Gamma> \<turnstile> p \<leftrightarrow> u : T1\<rightarrow>T2" by fact |
|
1086 have "\<Gamma> \<turnstile> s <=> t : T1" by fact |
|
1087 have ih2:"\<And>u. \<Gamma> \<turnstile> t <=> u : T1 \<Longrightarrow> \<Gamma> \<turnstile> s <=> u : T1" by fact |
|
1088 have "\<Gamma> \<turnstile> App q t \<leftrightarrow> u : T2" by fact |
|
1089 then obtain r T1' v where ha:"\<Gamma> \<turnstile> q \<leftrightarrow> r : T1'\<rightarrow>T2" and hb:"\<Gamma> \<turnstile> t <=> v : T1'" and eq:"u = App r v" by auto |
|
1090 moreover have "\<Gamma> \<turnstile> q \<leftrightarrow> p : T1\<rightarrow>T2" using h1 algorithmic_path_symmetry by auto |
|
1091 ultimately have "T1'\<rightarrow>T2 = T1\<rightarrow>T2" using algorithmic_path_type_unicity by auto |
|
1092 then have "T1' = T1" using ty.inject by auto |
|
1093 then have "\<Gamma> \<turnstile> s <=> v : T1" "\<Gamma> \<turnstile> p \<leftrightarrow> r : T1\<rightarrow>T2" using ih1 ih2 ha hb by auto |
|
1094 then show "\<Gamma> \<turnstile> App p s \<leftrightarrow> u : T2" using eq by auto |
|
1095 qed (auto) |
|
1096 |
|
1097 lemma algorithmic_weak_head_closure: |
|
1098 shows "\<lbrakk>\<Gamma> \<turnstile> s <=> t : T ; s' \<leadsto> s; t' \<leadsto> t\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s' <=> t' : T" |
|
1099 by (nominal_induct \<Gamma> s t T avoiding: s' t' |
|
1100 rule: alg_equiv_alg_path_equiv_strong_inducts(1) [of _ _ _ _ "%a b c d e. True"]) |
|
1101 (auto) |
|
1102 |
|
1103 lemma logical_symmetry: |
|
1104 assumes "\<Gamma> \<turnstile> s is t : T" |
|
1105 shows "\<Gamma> \<turnstile> t is s : T" |
|
1106 using assms by (nominal_induct arbitrary: \<Gamma> s t rule:ty.induct, auto simp add: algorithmic_symmetry) |
|
1107 |
|
1108 lemma logical_transitivity: |
|
1109 assumes "\<Gamma> \<turnstile> s is t : T" "\<Gamma> \<turnstile> t is u : T" |
|
1110 shows "\<Gamma> \<turnstile> s is u : T" |
|
1111 using assms |
|
1112 proof (nominal_induct arbitrary: \<Gamma> s t u rule:ty.induct) |
|
1113 case TBase |
|
1114 then show "\<Gamma> \<turnstile> s is u : TBase" by (auto elim: algorithmic_transitivity) |
|
1115 next |
|
1116 case (Arrow T1 T2 \<Gamma> s t u) |
|
1117 have h1:"\<Gamma> \<turnstile> s is t : T1 \<rightarrow> T2" by fact |
|
1118 have h2:"\<Gamma> \<turnstile> t is u : T1 \<rightarrow> T2" by fact |
|
1119 have ih1:"\<And>\<Gamma> s t u. \<lbrakk>\<Gamma> \<turnstile> s is t : T1; \<Gamma> \<turnstile> t is u : T1\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s is u : T1" by fact |
|
1120 have ih2:"\<And>\<Gamma> s t u. \<lbrakk>\<Gamma> \<turnstile> s is t : T2; \<Gamma> \<turnstile> t is u : T2\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s is u : T2" by fact |
|
1121 { |
|
1122 fix \<Gamma>' s' u' |
|
1123 assume hsub:"\<Gamma>\<lless>\<Gamma>'" and hl:"\<Gamma>' \<turnstile> s' is u' : T1" |
|
1124 then have "\<Gamma>' \<turnstile> u' is s' : T1" using logical_symmetry by blast |
|
1125 then have "\<Gamma>' \<turnstile> u' is u' : T1" using ih1 hl by blast |
|
1126 then have "\<Gamma>' \<turnstile> App t u' is App u u' : T2" using h2 hsub by auto |
|
1127 moreover have "\<Gamma>' \<turnstile> App s s' is App t u' : T2" using h1 hsub hl by auto |
|
1128 ultimately have "\<Gamma>' \<turnstile> App s s' is App u u' : T2" using ih2 by blast |
|
1129 } |
|
1130 moreover have "valid \<Gamma>" using h1 alg_equiv_valid by auto |
|
1131 ultimately show "\<Gamma> \<turnstile> s is u : T1 \<rightarrow> T2" by auto |
|
1132 qed (auto) |
|
1133 |
|
1134 lemma logical_weak_head_closure: |
|
1135 assumes "\<Gamma> \<turnstile> s is t : T" "s' \<leadsto> s" "t' \<leadsto> t" |
|
1136 shows "\<Gamma> \<turnstile> s' is t' : T" |
|
1137 using assms |
|
1138 apply (nominal_induct arbitrary: \<Gamma> s t s' t' rule:ty.induct) |
|
1139 apply (auto simp add: algorithmic_weak_head_closure) |
|
1140 apply (blast) |
|
1141 done |
|
1142 |
|
1143 lemma logical_weak_head_closure': |
|
1144 assumes "\<Gamma> \<turnstile> s is t : T" "s' \<leadsto> s" |
|
1145 shows "\<Gamma> \<turnstile> s' is t : T" |
|
1146 using assms |
|
1147 proof (nominal_induct arbitrary: \<Gamma> s t s' rule:ty.induct) |
|
1148 case (TBase \<Gamma> s t s') |
|
1149 then show ?case by force |
|
1150 next |
|
1151 case (TUnit \<Gamma> s t s') |
|
1152 then show ?case by auto |
|
1153 next |
|
1154 case (Arrow T1 T2 \<Gamma> s t s') |
|
1155 have h1:"s' \<leadsto> s" by fact |
|
1156 have ih:"\<And>\<Gamma> s t s'. \<lbrakk>\<Gamma> \<turnstile> s is t : T2; s' \<leadsto> s\<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s' is t : T2" by fact |
|
1157 have h2:"\<Gamma> \<turnstile> s is t : T1\<rightarrow>T2" by fact |
|
1158 then have hb:"\<forall>\<Gamma>' s' t'. \<Gamma>\<lless>\<Gamma>' \<longrightarrow> \<Gamma>' \<turnstile> s' is t' : T1 \<longrightarrow> (\<Gamma>' \<turnstile> (App s s') is (App t t') : T2)" by auto |
|
1159 { |
|
1160 fix \<Gamma>' s2 t2 |
|
1161 assume "\<Gamma>\<lless>\<Gamma>'" and "\<Gamma>' \<turnstile> s2 is t2 : T1" |
|
1162 then have "\<Gamma>' \<turnstile> (App s s2) is (App t t2) : T2" using hb by auto |
|
1163 moreover have "(App s' s2) \<leadsto> (App s s2)" using h1 by auto |
|
1164 ultimately have "\<Gamma>' \<turnstile> App s' s2 is App t t2 : T2" using ih by auto |
|
1165 } |
|
1166 moreover have "valid \<Gamma>" using h2 log_equiv_valid by auto |
|
1167 ultimately show "\<Gamma> \<turnstile> s' is t : T1\<rightarrow>T2" by auto |
|
1168 qed |
|
1169 |
|
1170 abbreviation |
|
1171 log_equiv_subst :: "(name\<times>ty) list \<Rightarrow> (name\<times>trm) list \<Rightarrow> (name\<times>trm) list \<Rightarrow> (name\<times>ty) list \<Rightarrow> bool" |
|
1172 ("_ \<turnstile> _ is _ over _" [60,60] 60) |
|
1173 where |
|
1174 "\<Gamma>' \<turnstile> \<gamma> is \<delta> over \<Gamma> \<equiv> valid \<Gamma>' \<and> (\<forall> x T. (x,T) \<in> set \<Gamma> \<longrightarrow> \<Gamma>' \<turnstile> \<gamma><Var x> is \<delta><Var x> : T)" |
|
1175 |
|
1176 lemma logical_pseudo_reflexivity: |
|
1177 assumes "\<Gamma>' \<turnstile> t is s over \<Gamma>" |
|
1178 shows "\<Gamma>' \<turnstile> s is s over \<Gamma>" |
|
1179 proof - |
|
1180 have "\<Gamma>' \<turnstile> t is s over \<Gamma>" by fact |
|
1181 moreover then have "\<Gamma>' \<turnstile> s is t over \<Gamma>" using logical_symmetry by blast |
|
1182 ultimately show "\<Gamma>' \<turnstile> s is s over \<Gamma>" using logical_transitivity by blast |
|
1183 qed |
|
1184 |
|
1185 lemma logical_subst_monotonicity : |
|
1186 fixes \<Gamma>::"(name\<times>ty) list" |
|
1187 and \<Gamma>'::"(name\<times>ty) list" |
|
1188 and \<Gamma>''::"(name\<times>ty) list" |
|
1189 assumes "\<Gamma>' \<turnstile> s is t over \<Gamma>" "\<Gamma>'\<lless>\<Gamma>''" |
|
1190 shows "\<Gamma>'' \<turnstile> s is t over \<Gamma>" |
|
1191 using assms logical_monotonicity by blast |
|
1192 |
|
1193 lemma equiv_subst_ext : |
|
1194 assumes h1:"\<Gamma>' \<turnstile> \<gamma> is \<delta> over \<Gamma>" and h2:"\<Gamma>' \<turnstile> s is t : T" and fs:"x\<sharp>\<Gamma>" |
|
1195 shows "\<Gamma>' \<turnstile> (x,s)#\<gamma> is (x,t)#\<delta> over (x,T)#\<Gamma>" |
|
1196 using assms |
|
1197 proof - |
|
1198 { |
|
1199 fix y U |
|
1200 assume "(y,U) \<in> set ((x,T)#\<Gamma>)" |
|
1201 moreover |
|
1202 { |
|
1203 assume "(y,U) \<in> set [(x,T)]" |
|
1204 then have "\<Gamma>' \<turnstile> (x,s)#\<gamma><Var y> is (x,t)#\<delta><Var y> : U" by auto |
|
1205 } |
|
1206 moreover |
|
1207 { |
|
1208 assume hl:"(y,U) \<in> set \<Gamma>" |
|
1209 then have "\<not> y\<sharp>\<Gamma>" by (induct \<Gamma>) (auto simp add: fresh_list_cons fresh_atm fresh_prod) |
|
1210 then have hf:"x\<sharp> Var y" using fs by (auto simp add: fresh_atm) |
|
1211 then have "(x,s)#\<gamma><Var y> = \<gamma><Var y>" "(x,t)#\<delta><Var y> = \<delta><Var y>" using fresh_psubst_simpl by blast+ |
|
1212 moreover have "\<Gamma>' \<turnstile> \<gamma><Var y> is \<delta><Var y> : U" using h1 hl by auto |
|
1213 ultimately have "\<Gamma>' \<turnstile> (x,s)#\<gamma><Var y> is (x,t)#\<delta><Var y> : U" by auto |
|
1214 } |
|
1215 ultimately have "\<Gamma>' \<turnstile> (x,s)#\<gamma><Var y> is (x,t)#\<delta><Var y> : U" by auto |
|
1216 } |
|
1217 moreover have "valid \<Gamma>'" using h2 log_equiv_valid by blast |
|
1218 ultimately show "\<Gamma>' \<turnstile> (x,s)#\<gamma> is (x,t)#\<delta> over (x,T)#\<Gamma>" by auto |
|
1219 qed |
|
1220 |
|
1221 theorem fundamental_theorem: |
|
1222 assumes "\<Gamma> \<turnstile> t : T" "\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" |
|
1223 shows "\<Gamma>' \<turnstile> \<gamma><t> is \<theta><t> : T" |
|
1224 using assms |
|
1225 proof (nominal_induct avoiding:\<Gamma>' \<gamma> \<theta> rule: typing_induct_strong) |
|
1226 case (t_Lam x \<Gamma> T1 t2 T2 \<Gamma>' \<gamma> \<theta>) |
|
1227 have fs:"x\<sharp>\<gamma>" "x\<sharp>\<theta>" "x\<sharp>\<Gamma>" by fact |
|
1228 have h:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact |
|
1229 have ih:"\<And> \<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><t2> is \<theta><t2> : T2" by fact |
|
1230 { |
|
1231 fix \<Gamma>'' s' t' |
|
1232 assume "\<Gamma>'\<lless>\<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T1" |
|
1233 then have "\<Gamma>'' \<turnstile> \<gamma> is \<theta> over \<Gamma>" using logical_subst_monotonicity h by blast |
|
1234 then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma> is (x,t')#\<theta> over (x,T1)#\<Gamma>" using equiv_subst_ext hl fs by blast |
|
1235 then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma><t2> is (x,t')#\<theta><t2> : T2" using ih by auto |
|
1236 then have "\<Gamma>''\<turnstile>\<gamma><t2>[x::=s'] is \<theta><t2>[x::=t'] : T2" using psubst_subst_psubst fs by simp |
|
1237 moreover have "App (Lam [x].\<gamma><t2>) s' \<leadsto> \<gamma><t2>[x::=s']" by auto |
|
1238 moreover have "App (Lam [x].\<theta><t2>) t' \<leadsto> \<theta><t2>[x::=t']" by auto |
|
1239 ultimately have "\<Gamma>''\<turnstile> App (Lam [x].\<gamma><t2>) s' is App (Lam [x].\<theta><t2>) t' : T2" |
|
1240 using logical_weak_head_closure by auto |
|
1241 } |
|
1242 moreover have "valid \<Gamma>'" using h by auto |
|
1243 ultimately show "\<Gamma>' \<turnstile> \<gamma><Lam [x].t2> is \<theta><Lam [x].t2> : T1\<rightarrow>T2" using fs by auto |
|
1244 qed (auto) |
|
1245 |
|
1246 |
|
1247 theorem fundamental_theorem_2: |
|
1248 assumes h1: "\<Gamma> \<turnstile> s == t : T" |
|
1249 and h2: "\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" |
|
1250 shows "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><t> : T" |
|
1251 using h1 h2 |
|
1252 proof (nominal_induct \<Gamma> s t T avoiding: \<Gamma>' \<gamma> \<theta> rule: equiv_def_strong_induct) |
|
1253 case (Q_Refl \<Gamma> t T \<Gamma>' \<gamma> \<theta>) |
|
1254 have "\<Gamma> \<turnstile> t : T" by fact |
|
1255 moreover have "\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact |
|
1256 ultimately show "\<Gamma>' \<turnstile> \<gamma><t> is \<theta><t> : T" using fundamental_theorem by blast |
|
1257 next |
|
1258 case (Q_Symm \<Gamma> t s T \<Gamma>' \<gamma> \<theta>) |
|
1259 have "\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact |
|
1260 moreover have ih:"\<And> \<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><t> is \<theta><s> : T" by fact |
|
1261 ultimately show "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><t> : T" using logical_symmetry by blast |
|
1262 next |
|
1263 case (Q_Trans \<Gamma> s t T u \<Gamma>' \<gamma> \<theta>) |
|
1264 have ih1:"\<And> \<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><s> is \<theta><t> : T" by fact |
|
1265 have ih2:"\<And> \<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><t> is \<theta><u> : T" by fact |
|
1266 have h:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact |
|
1267 then have "\<Gamma>' \<turnstile> \<theta> is \<theta> over \<Gamma>" using logical_pseudo_reflexivity by auto |
|
1268 then have "\<Gamma>' \<turnstile> \<theta><t> is \<theta><u> : T" using ih2 by auto |
|
1269 moreover have "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><t> : T" using ih1 h by auto |
|
1270 ultimately show "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><u> : T" using logical_transitivity by blast |
|
1271 next |
|
1272 case (Q_Abs x \<Gamma> T1 s2 t2 T2 \<Gamma>' \<gamma> \<theta>) |
|
1273 have fs:"x\<sharp>\<Gamma>" by fact |
|
1274 have fs2: "x\<sharp>\<gamma>" "x\<sharp>\<theta>" by fact |
|
1275 have h1:"(x,T1)#\<Gamma> \<turnstile> s2 == t2 : T2" by fact |
|
1276 have h2:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact |
|
1277 have ih:"\<And>\<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><s2> is \<theta><t2> : T2" by fact |
|
1278 { |
|
1279 fix \<Gamma>'' s' t' |
|
1280 assume "\<Gamma>'\<lless>\<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T1" |
|
1281 then have "\<Gamma>'' \<turnstile> \<gamma> is \<theta> over \<Gamma>" using h2 logical_subst_monotonicity by blast |
|
1282 then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma> is (x,t')#\<theta> over (x,T1)#\<Gamma>" using equiv_subst_ext hl fs by blast |
|
1283 then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma><s2> is (x,t')#\<theta><t2> : T2" using ih by blast |
|
1284 then have "\<Gamma>''\<turnstile> \<gamma><s2>[x::=s'] is \<theta><t2>[x::=t'] : T2" using fs2 psubst_subst_psubst by auto |
|
1285 moreover have "App (Lam [x]. \<gamma><s2>) s' \<leadsto> \<gamma><s2>[x::=s']" |
|
1286 and "App (Lam [x].\<theta><t2>) t' \<leadsto> \<theta><t2>[x::=t']" by auto |
|
1287 ultimately have "\<Gamma>'' \<turnstile> App (Lam [x]. \<gamma><s2>) s' is App (Lam [x].\<theta><t2>) t' : T2" |
|
1288 using logical_weak_head_closure by auto |
|
1289 } |
|
1290 moreover have "valid \<Gamma>'" using h2 by auto |
|
1291 ultimately have "\<Gamma>' \<turnstile> Lam [x].\<gamma><s2> is Lam [x].\<theta><t2> : T1\<rightarrow>T2" by auto |
|
1292 then show "\<Gamma>' \<turnstile> \<gamma><Lam [x].s2> is \<theta><Lam [x].t2> : T1\<rightarrow>T2" using fs2 by auto |
|
1293 next |
|
1294 case (Q_App \<Gamma> s1 t1 T1 T2 s2 t2 \<Gamma>' \<gamma> \<theta>) |
|
1295 then show "\<Gamma>' \<turnstile> \<gamma><App s1 s2> is \<theta><App t1 t2> : T2" by auto |
|
1296 next |
|
1297 case (Q_Beta x \<Gamma> T1 s12 t12 T2 s2 t2 \<Gamma>' \<gamma> \<theta>) |
|
1298 have h:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact |
|
1299 have fs:"x\<sharp>\<Gamma>" by fact |
|
1300 have fs2:"x\<sharp>\<gamma>" "x\<sharp>\<theta>" by fact |
|
1301 have ih1:"\<And>\<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><s2> is \<theta><t2> : T1" by fact |
|
1302 have ih2:"\<And>\<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><s12> is \<theta><t12> : T2" by fact |
|
1303 have "\<Gamma>' \<turnstile> \<gamma><s2> is \<theta><t2> : T1" using ih1 h by auto |
|
1304 then have "\<Gamma>' \<turnstile> (x,\<gamma><s2>)#\<gamma> is (x,\<theta><t2>)#\<theta> over (x,T1)#\<Gamma>" using equiv_subst_ext h fs by blast |
|
1305 then have "\<Gamma>' \<turnstile> (x,\<gamma><s2>)#\<gamma><s12> is (x,\<theta><t2>)#\<theta><t12> : T2" using ih2 by auto |
|
1306 then have "\<Gamma>' \<turnstile> \<gamma><s12>[x::=\<gamma><s2>] is \<theta><t12>[x::=\<theta><t2>] : T2" using fs2 psubst_subst_psubst by auto |
|
1307 then have "\<Gamma>' \<turnstile> \<gamma><s12>[x::=\<gamma><s2>] is \<theta><t12[x::=t2]> : T2" using fs2 psubst_subst_propagate by auto |
|
1308 moreover have "App (Lam [x].\<gamma><s12>) (\<gamma><s2>) \<leadsto> \<gamma><s12>[x::=\<gamma><s2>]" by auto |
|
1309 ultimately have "\<Gamma>' \<turnstile> App (Lam [x].\<gamma><s12>) (\<gamma><s2>) is \<theta><t12[x::=t2]> : T2" |
|
1310 using logical_weak_head_closure' by auto |
|
1311 then show "\<Gamma>' \<turnstile> \<gamma><App (Lam [x].s12) s2> is \<theta><t12[x::=t2]> : T2" using fs2 by simp |
|
1312 next |
|
1313 case (Q_Ext x \<Gamma> s t T1 T2 \<Gamma>' \<gamma> \<theta>) |
|
1314 have h2:"\<Gamma>' \<turnstile> \<gamma> is \<theta> over \<Gamma>" by fact |
|
1315 have fs:"x\<sharp>\<Gamma>" "x\<sharp>s" "x\<sharp>t" by fact |
|
1316 have ih:"\<And>\<Gamma>' \<gamma> \<theta>. \<Gamma>' \<turnstile> \<gamma> is \<theta> over (x,T1)#\<Gamma> \<Longrightarrow> \<Gamma>' \<turnstile> \<gamma><App s (Var x)> is \<theta><App t (Var x)> : T2" |
|
1317 by fact |
|
1318 { |
|
1319 fix \<Gamma>'' s' t' |
|
1320 assume hsub:"\<Gamma>'\<lless>\<Gamma>''" and hl:"\<Gamma>''\<turnstile> s' is t' : T1" |
|
1321 then have "\<Gamma>'' \<turnstile> \<gamma> is \<theta> over \<Gamma>" using h2 logical_subst_monotonicity by blast |
|
1322 then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma> is (x,t')#\<theta> over (x,T1)#\<Gamma>" using equiv_subst_ext hl fs by blast |
|
1323 then have "\<Gamma>'' \<turnstile> (x,s')#\<gamma><App s (Var x)> is (x,t')#\<theta><App t (Var x)> : T2" using ih by blast |
|
1324 then have "\<Gamma>'' \<turnstile> App (((x,s')#\<gamma>)<s>) (((x,s')#\<gamma>)<(Var x)>) is App ((x,t')#\<theta><t>) ((x,t')#\<theta><(Var x)>) : T2" by auto |
|
1325 then have "\<Gamma>'' \<turnstile> App ((x,s')#\<gamma><s>) s' is App ((x,t')#\<theta><t>) t' : T2" by auto |
|
1326 then have "\<Gamma>'' \<turnstile> App (\<gamma><s>) s' is App (\<theta><t>) t' : T2" using fs fresh_psubst_simpl by auto |
|
1327 } |
|
1328 moreover have "valid \<Gamma>'" using h2 by auto |
|
1329 ultimately show "\<Gamma>' \<turnstile> \<gamma><s> is \<theta><t> : T1\<rightarrow>T2" by auto |
|
1330 qed |
|
1331 |
|
1332 theorem completeness: |
|
1333 assumes "\<Gamma> \<turnstile> s == t : T" |
|
1334 shows "\<Gamma> \<turnstile> s <=> t : T" |
|
1335 using assms |
|
1336 proof - |
|
1337 { |
|
1338 fix x T |
|
1339 assume "(x,T) \<in> set \<Gamma>" "valid \<Gamma>" |
|
1340 then have "\<Gamma> \<turnstile> Var x is Var x : T" using main_lemma by blast |
|
1341 } |
|
1342 moreover have "valid \<Gamma>" using equiv_def_valid assms by auto |
|
1343 ultimately have "\<Gamma> \<turnstile> [] is [] over \<Gamma>" by auto |
|
1344 then have "\<Gamma> \<turnstile> []<s> is []<t> : T" using fundamental_theorem_2 assms by blast |
|
1345 then have "\<Gamma> \<turnstile> s is t : T" by simp |
|
1346 then show "\<Gamma> \<turnstile> s <=> t : T" using main_lemma by simp |
|
1347 qed |
|
1348 |
|
1349 (* Soundness is left as an exercise - like in the book*) |
|
1350 |
|
1351 (* |
|
1352 theorem soundness: |
|
1353 shows "\<lbrakk> \<Gamma> \<turnstile> s <=> t : T ; \<Gamma> \<turnstile> t : T ; \<Gamma> \<turnstile> s : T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s == t : T" |
|
1354 and "\<lbrakk> \<Gamma> \<turnstile> s \<leftrightarrow> t : T ; \<Gamma> \<turnstile> t : T ; \<Gamma> \<turnstile> s : T \<rbrakk> \<Longrightarrow> \<Gamma> \<turnstile> s == t : T" |
|
1355 *) |
|
1356 |
|
1357 end |
|
1358 |