|
1 theory Finite_Alpha |
|
2 imports "../Nominal2" |
|
3 begin |
|
4 |
|
5 lemma |
|
6 assumes "(supp x - as) \<sharp>* p" |
|
7 and "p \<bullet> x = y" |
|
8 and "p \<bullet> as = bs" |
|
9 shows "(as, x) \<approx>set (op =) supp p (bs, y)" |
|
10 using assms unfolding alphas |
|
11 by (metis Diff_eqvt atom_set_perm_eq supp_eqvt) |
|
12 |
|
13 lemma |
|
14 assumes "(supp x - set as) \<sharp>* p" |
|
15 and "p \<bullet> x = y" |
|
16 and "p \<bullet> as = bs" |
|
17 shows "(as, x) \<approx>lst (op =) supp p (bs, y)" |
|
18 using assms unfolding alphas |
|
19 by (metis Diff_eqvt atom_set_perm_eq supp_eqvt supp_of_atom_list) |
|
20 |
|
21 lemma |
|
22 assumes "(supp x - as) \<sharp>* p" |
|
23 and "p \<bullet> x = y" |
|
24 and "p \<bullet> (as \<inter> supp x) = bs \<inter> supp y" |
|
25 and "finite (supp x)" |
|
26 shows "(as, x) \<approx>res (op =) supp p (bs, y)" |
|
27 using assms |
|
28 unfolding alpha_res_alpha_set |
|
29 unfolding alphas |
|
30 apply simp |
|
31 apply rule |
|
32 apply (rule trans) |
|
33 apply (rule supp_perm_eq[symmetric, of _ p]) |
|
34 apply (simp add: supp_finite_atom_set fresh_star_def) |
|
35 apply blast |
|
36 apply (simp add: eqvts) |
|
37 apply (simp add: fresh_star_def) |
|
38 apply blast |
|
39 done |
|
40 |
|
41 lemma |
|
42 assumes "(as, x) \<approx>res (op =) supp p (bs, y)" |
|
43 shows "(supp x - as) \<sharp>* p" |
|
44 and "p \<bullet> (as \<inter> supp x) = bs \<inter> supp y" |
|
45 and "p \<bullet> x = y" |
|
46 using assms |
|
47 apply - |
|
48 prefer 3 |
|
49 apply (auto simp add: alphas)[2] |
|
50 unfolding alpha_res_alpha_set |
|
51 unfolding alphas |
|
52 by blast |
|
53 |
|
54 (* On the raw level *) |
|
55 |
|
56 atom_decl name |
|
57 |
|
58 nominal_datatype lam = |
|
59 Var "name" |
|
60 | App "lam" "lam" |
|
61 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
|
62 |
|
63 thm alpha_lam_raw.intros(3)[unfolded alphas, simplified] |
|
64 |
|
65 lemma alpha_fv: "alpha_lam_raw l r \<Longrightarrow> fv_lam_raw l = fv_lam_raw r" |
|
66 by (induct rule: alpha_lam_raw.induct) (simp_all add: alphas) |
|
67 |
|
68 lemma finite_fv_raw: "finite (fv_lam_raw l)" |
|
69 by (induct rule: lam_raw.induct) (simp_all add: supp_at_base) |
|
70 |
|
71 lemma "(fv_lam_raw l - {atom n}) \<sharp>* p \<Longrightarrow> alpha_lam_raw (p \<bullet> l) r \<Longrightarrow> |
|
72 fv_lam_raw l - {atom n} = fv_lam_raw r - {atom (p \<bullet> n)}" |
|
73 apply (rule trans) |
|
74 apply (rule supp_perm_eq[symmetric]) |
|
75 apply (subst supp_finite_atom_set) |
|
76 apply (rule finite_Diff) |
|
77 apply (rule finite_fv_raw) |
|
78 apply assumption |
|
79 apply (simp add: eqvts) |
|
80 apply (subst alpha_fv) |
|
81 apply assumption |
|
82 apply (rule) |
|
83 done |
|
84 |
|
85 (* For the res binding *) |
|
86 |
|
87 nominal_datatype ty2 = |
|
88 Var2 "name" |
|
89 | Fun2 "ty2" "ty2" |
|
90 |
|
91 nominal_datatype tys2 = |
|
92 All2 xs::"name fset" ty::"ty2" binds (set+) xs in ty |
|
93 |
|
94 lemma alpha_fv': "alpha_tys2_raw l r \<Longrightarrow> fv_tys2_raw l = fv_tys2_raw r" |
|
95 by (induct rule: alpha_tys2_raw.induct) (simp_all add: alphas) |
|
96 |
|
97 lemma finite_fv_raw': "finite (fv_tys2_raw l)" |
|
98 by (induct rule: tys2_raw.induct) (simp_all add: supp_at_base finite_supp) |
|
99 |
|
100 thm alpha_tys2_raw.intros[unfolded alphas, simplified] |
|
101 |
|
102 lemma "(supp x - atom ` (fset as)) \<sharp>* p \<Longrightarrow> p \<bullet> (x :: tys2) = y \<Longrightarrow> |
|
103 p \<bullet> (atom ` (fset as) \<inter> supp x) = atom ` (fset bs) \<inter> supp y \<Longrightarrow> |
|
104 supp x - atom ` (fset as) = supp y - atom ` (fset bs)" |
|
105 apply (rule trans) |
|
106 apply (rule supp_perm_eq[symmetric]) |
|
107 apply (subst supp_finite_atom_set) |
|
108 apply (rule finite_Diff) |
|
109 apply (rule finite_supp) |
|
110 apply assumption |
|
111 apply (simp add: eqvts) |
|
112 apply blast |
|
113 done |
|
114 |
|
115 end |