equal
deleted
inserted
replaced
1 theory LamEx |
1 theory LamEx |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs" "../QuotProd" |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs" "../QuotProd" |
3 begin |
3 begin |
4 |
|
5 |
|
6 (* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *) |
|
7 (* Currently not used, still needed needed? *) |
|
8 lemma supp_finite_set: |
|
9 fixes S::"atom set" |
|
10 assumes "finite S" |
|
11 shows "supp S = S" |
|
12 apply(rule finite_supp_unique) |
|
13 apply(simp add: supports_def) |
|
14 apply(auto simp add: permute_set_eq swap_atom)[1] |
|
15 apply(metis) |
|
16 apply(rule assms) |
|
17 apply(auto simp add: permute_set_eq swap_atom)[1] |
|
18 done |
|
19 |
|
20 |
4 |
21 atom_decl name |
5 atom_decl name |
22 |
6 |
23 datatype rlam = |
7 datatype rlam = |
24 rVar "name" |
8 rVar "name" |
322 apply clarify |
306 apply clarify |
323 apply (rule alpha_gen_rsp_pre[of "alpha",OF alpha_eqvt]) |
307 apply (rule alpha_gen_rsp_pre[of "alpha",OF alpha_eqvt]) |
324 apply auto |
308 apply auto |
325 done |
309 done |
326 |
310 |
327 (* |
|
328 (* pi_abs would be also sufficient to prove the next lemma *) |
311 (* pi_abs would be also sufficient to prove the next lemma *) |
329 lemma replam_eqvt: "pi \<bullet> (rep_lam x) = rep_lam (pi \<bullet> x)" |
312 lemma replam_eqvt: "pi \<bullet> (rep_lam x) = rep_lam (pi \<bullet> x)" |
330 apply (unfold rep_lam_def) |
313 apply (unfold rep_lam_def) |
331 sorry |
314 sorry |
332 |
315 |
336 apply (simp add: expand_fun_eq alpha_gen.simps Quotient_abs_rep[OF Quotient_lam]) |
319 apply (simp add: expand_fun_eq alpha_gen.simps Quotient_abs_rep[OF Quotient_lam]) |
337 apply (simp add: replam_eqvt) |
320 apply (simp add: replam_eqvt) |
338 apply (simp only: Quotient_abs_rep[OF Quotient_lam]) |
321 apply (simp only: Quotient_abs_rep[OF Quotient_lam]) |
339 apply auto |
322 apply auto |
340 done |
323 done |
341 *) |
324 |
342 |
325 |
343 lemma alpha_prs [quot_preserve]: "(rep_lam ---> rep_lam ---> id) alpha = (op =)" |
326 lemma alpha_prs [quot_preserve]: "(rep_lam ---> rep_lam ---> id) alpha = (op =)" |
344 apply (simp add: expand_fun_eq) |
327 apply (simp add: expand_fun_eq) |
345 apply (simp add: Quotient_rel_rep[OF Quotient_lam]) |
328 apply (simp add: Quotient_rel_rep[OF Quotient_lam]) |
346 done |
329 done |