106 overloading |
106 overloading |
107 perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" (unchecked) |
107 perm_lam \<equiv> "perm :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" (unchecked) |
108 begin |
108 begin |
109 |
109 |
110 quotient_definition |
110 quotient_definition |
111 "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" |
111 "perm_lam :: 'x prm \<Rightarrow> lam \<Rightarrow> lam" |
112 as |
112 as |
113 "perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam" |
113 "perm::'x prm \<Rightarrow> rlam \<Rightarrow> rlam" |
114 |
114 |
115 end |
115 end |
116 |
|
117 (* lemmas that need to be lifted *) |
|
118 lemma pi_var_eqvt1: |
|
119 fixes pi::"'x prm" |
|
120 shows "(pi \<bullet> rVar a) \<approx> rVar (pi \<bullet> a)" |
|
121 by (simp add: alpha_refl) |
|
122 |
|
123 lemma pi_var_eqvt2: |
|
124 fixes pi::"'x prm" |
|
125 shows "(pi \<bullet> rVar a) = rVar (pi \<bullet> a)" |
|
126 by (simp) |
|
127 |
|
128 lemma pi_app_eqvt1: |
|
129 fixes pi::"'x prm" |
|
130 shows "(pi \<bullet> rApp t1 t2) \<approx> rApp (pi \<bullet> t1) (pi \<bullet> t2)" |
|
131 by (simp add: alpha_refl) |
|
132 |
|
133 lemma pi_app_eqvt2: |
|
134 fixes pi::"'x prm" |
|
135 shows "(pi \<bullet> rApp t1 t2) = rApp (pi \<bullet> t1) (pi \<bullet> t2)" |
|
136 by (simp) |
|
137 |
|
138 lemma pi_lam_eqvt1: |
|
139 fixes pi::"'x prm" |
|
140 shows "(pi \<bullet> rLam a t) \<approx> rLam (pi \<bullet> a) (pi \<bullet> t)" |
|
141 by (simp add: alpha_refl) |
|
142 |
|
143 lemma pi_lam_eqvt2: |
|
144 fixes pi::"'x prm" |
|
145 shows "(pi \<bullet> rLam a t) = rLam (pi \<bullet> a) (pi \<bullet> t)" |
|
146 by (simp add: alpha) |
|
147 |
|
148 |
116 |
149 lemma real_alpha: |
117 lemma real_alpha: |
150 assumes a: "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s" |
118 assumes a: "t = [(a,b)]\<bullet>s" "a\<sharp>[b].s" |
151 shows "Lam a t = Lam b s" |
119 shows "Lam a t = Lam b s" |
152 using a |
120 using a |
187 apply (auto) |
155 apply (auto) |
188 apply (erule alpha.cases) |
156 apply (erule alpha.cases) |
189 apply (simp_all add: rlam.inject alpha_refl) |
157 apply (simp_all add: rlam.inject alpha_refl) |
190 done |
158 done |
191 |
159 |
192 lemma pi_var1: |
160 |
193 fixes pi::"'x prm" |
161 lemma lam_induct: |
|
162 "\<lbrakk>\<And>name. P (Var name); |
|
163 \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2); |
|
164 \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> |
|
165 \<Longrightarrow> P lam" |
|
166 by (lifting rlam.induct) |
|
167 |
|
168 lemma perm_lam [simp]: |
|
169 fixes pi::"'a prm" |
194 shows "pi \<bullet> Var a = Var (pi \<bullet> a)" |
170 shows "pi \<bullet> Var a = Var (pi \<bullet> a)" |
195 by (lifting pi_var_eqvt1) |
171 and "pi \<bullet> App t1 t2 = App (pi \<bullet> t1) (pi \<bullet> t2)" |
196 |
172 and "pi \<bullet> Lam a t = Lam (pi \<bullet> a) (pi \<bullet> t)" |
197 lemma pi_var2: |
173 apply(lifting perm_rlam.simps) |
198 fixes pi::"'x prm" |
174 done |
199 shows "pi \<bullet> Var a = Var (pi \<bullet> a)" |
175 |
200 by (lifting pi_var_eqvt2) |
176 instance lam::pt_name |
201 |
177 apply(default) |
202 |
178 apply(induct_tac [!] x rule: lam_induct) |
203 lemma pi_app: |
179 apply(simp_all add: pt_name2 pt_name3) |
204 fixes pi::"'x prm" |
180 done |
205 shows "pi \<bullet> App t1 t2 = App (pi \<bullet> t1) (pi \<bullet> t2)" |
181 |
206 by (lifting pi_app_eqvt2) |
182 lemma fv_lam [simp]: |
207 |
|
208 lemma pi_lam: |
|
209 fixes pi::"'x prm" |
|
210 shows "pi \<bullet> Lam a t = Lam (pi \<bullet> a) (pi \<bullet> t)" |
|
211 by (lifting pi_lam_eqvt2) |
|
212 |
|
213 lemma fv_var: |
|
214 shows "fv (Var a) = {a}" |
183 shows "fv (Var a) = {a}" |
215 by (lifting rfv_var) |
184 and "fv (App t1 t2) = fv t1 \<union> fv t2" |
216 |
185 and "fv (Lam a t) = fv t - {a}" |
217 lemma fv_app: |
186 apply(lifting rfv_var rfv_app rfv_lam) |
218 shows "fv (App t1 t2) = fv t1 \<union> fv t2" |
187 done |
219 by (lifting rfv_app) |
188 |
220 |
|
221 lemma fv_lam: |
|
222 shows "fv (Lam a t) = fv t - {a}" |
|
223 by (lifting rfv_lam) |
|
224 |
189 |
225 lemma a1: |
190 lemma a1: |
226 "a = b \<Longrightarrow> Var a = Var b" |
191 "a = b \<Longrightarrow> Var a = Var b" |
227 by (lifting a1) |
192 by (lifting a1) |
228 |
193 |
258 "(App t1 t2 = App s1 s2) = (t1 = s1 \<and> t2 = s2)" |
223 "(App t1 t2 = App s1 s2) = (t1 = s1 \<and> t2 = s2)" |
259 sorry |
224 sorry |
260 |
225 |
261 lemma var_supp1: |
226 lemma var_supp1: |
262 shows "(supp (Var a)) = ((supp a)::name set)" |
227 shows "(supp (Var a)) = ((supp a)::name set)" |
263 apply(simp add: supp_def pi_var1 var_inject) |
228 apply(simp add: supp_def var_inject) |
264 done |
229 done |
265 |
230 |
266 lemma var_supp: |
231 lemma var_supp: |
267 shows "(supp (Var a)) = {a::name}" |
232 shows "(supp (Var a)) = {a::name}" |
268 using var_supp1 |
233 using var_supp1 |
269 apply(simp add: supp_atm) |
234 apply(simp add: supp_atm) |
270 done |
235 done |
271 |
236 |
272 lemma app_supp: |
237 lemma app_supp: |
273 shows "supp (App t1 t2) = (supp t1) \<union> ((supp t2)::name set)" |
238 shows "supp (App t1 t2) = (supp t1) \<union> ((supp t2)::name set)" |
274 apply(simp only: supp_def pi_app app_inject) |
239 apply(simp only: perm_lam supp_def app_inject) |
275 apply(simp add: Collect_imp_eq Collect_neg_eq) |
240 apply(simp add: Collect_imp_eq Collect_neg_eq) |
276 done |
241 done |
277 |
242 |
278 lemma lam_supp: |
243 lemma lam_supp: |
279 shows "supp (Lam x t) = ((supp ([x].t))::name set)" |
244 shows "supp (Lam x t) = ((supp ([x].t))::name set)" |
280 apply(simp add: supp_def pi_lam) |
245 apply(simp add: supp_def) |
281 sorry |
246 sorry |
282 |
247 |
283 lemma lam_induct: |
|
284 "\<lbrakk>\<And>name. P (Var name); |
|
285 \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2); |
|
286 \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> |
|
287 \<Longrightarrow> P lam" |
|
288 by (lifting rlam.induct) |
|
289 |
|
290 instance lam::pt_name |
|
291 apply(default) |
|
292 apply(induct_tac x rule: lam_induct) |
|
293 apply(simp add: pi_var1) |
|
294 apply(simp add: pi_app) |
|
295 apply(simp add: pi_lam) |
|
296 apply(induct_tac x rule: lam_induct) |
|
297 apply(simp add: pi_var1 pt_name2) |
|
298 apply(simp add: pi_app) |
|
299 apply(simp add: pi_lam pt_name2) |
|
300 apply(induct_tac x rule: lam_induct) |
|
301 apply(simp add: pi_var1 pt_name3) |
|
302 apply(simp add: pi_app) |
|
303 apply(simp add: pi_lam pt_name3) |
|
304 done |
|
305 |
248 |
306 instance lam::fs_name |
249 instance lam::fs_name |
307 apply(default) |
250 apply(default) |
308 apply(induct_tac x rule: lam_induct) |
251 apply(induct_tac x rule: lam_induct) |
309 apply(simp add: var_supp) |
252 apply(simp add: var_supp) |
326 proof - |
269 proof - |
327 have "\<And>(pi::name prm) a. P a (pi \<bullet> lam)" |
270 have "\<And>(pi::name prm) a. P a (pi \<bullet> lam)" |
328 proof (induct lam rule: lam_induct) |
271 proof (induct lam rule: lam_induct) |
329 case (1 name pi) |
272 case (1 name pi) |
330 show "P a (pi \<bullet> Var name)" |
273 show "P a (pi \<bullet> Var name)" |
331 apply (simp only: pi_var1) |
274 apply (simp) |
332 apply (rule a1) |
275 apply (rule a1) |
333 done |
276 done |
334 next |
277 next |
335 case (2 lam1 lam2 pi) |
278 case (2 lam1 lam2 pi) |
336 have b1: "\<And>(pi::name prm) a. P a (pi \<bullet> lam1)" by fact |
279 have b1: "\<And>(pi::name prm) a. P a (pi \<bullet> lam1)" by fact |
337 have b2: "\<And>(pi::name prm) a. P a (pi \<bullet> lam2)" by fact |
280 have b2: "\<And>(pi::name prm) a. P a (pi \<bullet> lam2)" by fact |
338 show "P a (pi \<bullet> App lam1 lam2)" |
281 show "P a (pi \<bullet> App lam1 lam2)" |
339 apply (simp only: pi_app) |
282 apply (simp) |
340 apply (rule a2) |
283 apply (rule a2) |
341 apply (rule b1) |
284 apply (rule b1) |
342 apply (rule b2) |
285 apply (rule b2) |
343 done |
286 done |
344 next |
287 next |
359 using fr |
302 using fr |
360 apply(simp add: fresh_lam) |
303 apply(simp add: fresh_lam) |
361 apply(simp add: fresh_lam) |
304 apply(simp add: fresh_lam) |
362 done |
305 done |
363 show "P a (pi \<bullet> Lam name lam)" |
306 show "P a (pi \<bullet> Lam name lam)" |
364 apply (simp add: pi_lam) |
307 apply (simp) |
365 apply(subst eq[symmetric]) |
308 apply(subst eq[symmetric]) |
366 using p |
309 using p |
367 apply(simp only: pi_lam pt_name2 swap_simps) |
310 apply(simp only: perm_lam pt_name2 swap_simps) |
368 done |
311 done |
369 qed |
312 qed |
370 then have "P a (([]::name prm) \<bullet> lam)" by blast |
313 then have "P a (([]::name prm) \<bullet> lam)" by blast |
371 then show "P a lam" by simp |
314 then show "P a lam" by simp |
372 qed |
315 qed |
475 (\<forall>l r. hom (App l r) = f_app l r (hom l) (hom r)) \<and> |
418 (\<forall>l r. hom (App l r) = f_app l r (hom l) (hom r)) \<and> |
476 (\<forall>x a. hom (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))" |
419 (\<forall>x a. hom (Lam a x) = f_lam (\<lambda>b. ([(a,b)] \<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))" |
477 apply (lifting hom) |
420 apply (lifting hom) |
478 done |
421 done |
479 |
422 |
480 thm bex_reg_eqv_range[OF identity_equivp, of "alpha"] |
423 (* test test |
|
424 lemma raw_hom_correct: |
|
425 assumes f1: "f_var \<in> Respects (op= ===> op=)" |
|
426 and f2: "f_app \<in> Respects (alpha ===> alpha ===> op= ===> op= ===> op=)" |
|
427 and f3: "f_lam \<in> Respects ((op= ===> alpha) ===> (op= ===> op=) ===> op=)" |
|
428 shows "\<exists>!hom\<in>Respects (alpha ===> op =). |
|
429 ((\<forall>x. hom (rVar x) = f_var x) \<and> |
|
430 (\<forall>l r. hom (rApp l r) = f_app l r (hom l) (hom r)) \<and> |
|
431 (\<forall>x a. hom (rLam a x) = f_lam (\<lambda>b. ([(a,b)]\<bullet> x)) (\<lambda>b. hom ([(a,b)] \<bullet> x))))" |
|
432 unfolding Bex1_def |
|
433 apply(rule ex1I) |
|
434 sorry |
|
435 *) |
481 |
436 |
482 |
437 |
483 end |
438 end |
484 |
439 |