5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 nominal_datatype trm = |
7 nominal_datatype trm = |
8 Var "name" |
8 Var "name" |
9 | App "trm" "trm" |
9 | App "trm" "trm" |
10 | Lam x::"name" t::"trm" binds x in t |
10 | Lam x::"name" t::"trm" binds (set) x in t |
11 | Let p::"pat" "trm" t::"trm" binds "bn p" in t |
11 | Let p::"pat" "trm" t::"trm" binds (set) "f p" in t |
12 and pat = |
12 and pat = |
13 PNil |
13 PN |
14 | PVar "name" |
14 | PS "name" |
15 | PTup "pat" "pat" |
15 | PD "name" "name" |
16 binder |
16 binder |
17 bn::"pat \<Rightarrow> atom list" |
17 f::"pat \<Rightarrow> atom set" |
18 where |
18 where |
19 "bn PNil = []" |
19 "f PN = {}" |
20 | "bn (PVar x) = [atom x]" |
20 | "f (PD x y) = {atom x, atom y}" |
21 | "bn (PTup p1 p2) = bn p1 @ bn p2" |
21 | "f (PS x) = {atom x}" |
22 |
22 |
23 thm trm_pat.eq_iff |
|
24 thm trm_pat.distinct |
23 thm trm_pat.distinct |
25 thm trm_pat.induct |
24 thm trm_pat.induct |
26 thm trm_pat.strong_induct[no_vars] |
|
27 thm trm_pat.exhaust |
25 thm trm_pat.exhaust |
28 thm trm_pat.strong_exhaust[no_vars] |
|
29 thm trm_pat.fv_defs |
26 thm trm_pat.fv_defs |
30 thm trm_pat.bn_defs |
27 thm trm_pat.bn_defs |
31 thm trm_pat.perm_simps |
28 thm trm_pat.perm_simps |
32 thm trm_pat.eq_iff |
29 thm trm_pat.eq_iff |
33 thm trm_pat.fv_bn_eqvt |
30 thm trm_pat.fv_bn_eqvt |
34 thm trm_pat.size |
31 thm trm_pat.size_eqvt |
35 |
|
36 (* Nominal_Abs test *) |
|
37 |
|
38 lemma alpha_res_alpha_set: |
|
39 "(bs, x) \<approx>res op = supp p (cs, y) \<longleftrightarrow> |
|
40 (bs \<inter> supp x, x) \<approx>set op = supp p (cs \<inter> supp y, y)" |
|
41 using alpha_abs_set_abs_res alpha_abs_res_abs_set by blast |
|
42 |
|
43 |
|
44 lemma |
|
45 fixes x::"'a::fs" |
|
46 assumes "(supp x - as) \<sharp>* p" |
|
47 and "p \<bullet> x = y" |
|
48 and "p \<bullet> (as \<inter> supp x) = bs \<inter> supp y" |
|
49 shows "(as, x) \<approx>res (op =) supp p (bs, y)" |
|
50 using assms |
|
51 unfolding alpha_res_alpha_set |
|
52 unfolding alphas |
|
53 apply simp |
|
54 apply rule |
|
55 apply (rule trans) |
|
56 apply (rule supp_perm_eq[symmetric, of _ p]) |
|
57 apply(subst supp_finite_atom_set) |
|
58 apply (metis finite_Diff finite_supp) |
|
59 apply (simp add: fresh_star_def) |
|
60 apply blast |
|
61 apply(perm_simp) |
|
62 apply(simp) |
|
63 done |
|
64 |
|
65 lemma |
|
66 fixes x::"'a::fs" |
|
67 assumes "(supp x - as) \<sharp>* p" |
|
68 and "p \<bullet> x = y" |
|
69 and "p \<bullet> as = bs" |
|
70 shows "(as, x) \<approx>set (op =) supp p (bs, y)" |
|
71 using assms |
|
72 unfolding alphas |
|
73 apply simp |
|
74 apply (rule trans) |
|
75 apply (rule supp_perm_eq[symmetric, of _ p]) |
|
76 apply(subst supp_finite_atom_set) |
|
77 apply (metis finite_Diff finite_supp) |
|
78 apply(simp) |
|
79 apply(perm_simp) |
|
80 apply(simp) |
|
81 done |
|
82 |
|
83 lemma |
|
84 fixes x::"'a::fs" |
|
85 assumes "(supp x - set as) \<sharp>* p" |
|
86 and "p \<bullet> x = y" |
|
87 and "p \<bullet> as = bs" |
|
88 shows "(as, x) \<approx>lst (op =) supp p (bs, y)" |
|
89 using assms |
|
90 unfolding alphas |
|
91 apply simp |
|
92 apply (rule trans) |
|
93 apply (rule supp_perm_eq[symmetric, of _ p]) |
|
94 apply(subst supp_finite_atom_set) |
|
95 apply (metis finite_Diff finite_supp) |
|
96 apply(simp) |
|
97 apply(perm_simp) |
|
98 apply(simp) |
|
99 done |
|
100 |
32 |
101 |
33 |
102 end |
34 end |
103 |
35 |
104 |
36 |