|
2436
|
1 |
theory LetPat
|
|
2454
|
2 |
imports "../Nominal2"
|
|
1596
|
3 |
begin
|
|
|
4 |
|
|
|
5 |
atom_decl name
|
|
|
6 |
|
|
2026
|
7 |
nominal_datatype trm =
|
|
1596
|
8 |
Var "name"
|
|
2026
|
9 |
| App "trm" "trm"
|
|
3029
|
10 |
| Lam x::"name" t::"trm" binds x in t
|
|
|
11 |
| Let p::"pat" "trm" t::"trm" binds "bn p" in t
|
|
2026
|
12 |
and pat =
|
|
3029
|
13 |
PNil
|
|
|
14 |
| PVar "name"
|
|
|
15 |
| PTup "pat" "pat"
|
|
1596
|
16 |
binder
|
|
3029
|
17 |
bn::"pat \<Rightarrow> atom list"
|
|
1596
|
18 |
where
|
|
3029
|
19 |
"bn PNil = []"
|
|
|
20 |
| "bn (PVar x) = [atom x]"
|
|
|
21 |
| "bn (PTup p1 p2) = bn p1 @ bn p2"
|
|
2300
|
22 |
|
|
3029
|
23 |
thm trm_pat.eq_iff
|
|
2436
|
24 |
thm trm_pat.distinct
|
|
2026
|
25 |
thm trm_pat.induct
|
|
3029
|
26 |
thm trm_pat.strong_induct[no_vars]
|
|
2436
|
27 |
thm trm_pat.exhaust
|
|
3029
|
28 |
thm trm_pat.strong_exhaust[no_vars]
|
|
2436
|
29 |
thm trm_pat.fv_defs
|
|
|
30 |
thm trm_pat.bn_defs
|
|
|
31 |
thm trm_pat.perm_simps
|
|
|
32 |
thm trm_pat.eq_iff
|
|
|
33 |
thm trm_pat.fv_bn_eqvt
|
|
3029
|
34 |
thm trm_pat.size
|
|
|
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
|
|
1596
|
100 |
|
2082
0854af516f14
cleaned up a bit the examples; added equivariance to all examples
Christian Urban <urbanc@in.tum.de>
diff
changeset
|
101 |
|
|
1596
|
102 |
end
|
|
|
103 |
|
|
|
104 |
|
|
|
105 |
|