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