|
1 theory Local_Contexts |
|
2 imports "../Nominal2" |
|
3 begin |
|
4 |
|
5 text {* |
|
6 This theory, contributed by Tjark Weber, contains examples |
|
7 and test cases that illustrate the useof Nominal2 in local |
|
8 contexts (locales, type classes, etc.). |
|
9 |
|
10 As a running example, we use a variant of the untyped lambda-calculus |
|
11 whose lambda-binder binds lists of names, rather than single names. |
|
12 *} |
|
13 |
|
14 atom_decl name |
|
15 |
|
16 nominal_datatype lam = Var name |
|
17 | App lam lam ("_ \<cdot> _" [110,110] 110) |
|
18 | Lam xs::"name list" t::lam binds xs in t ("Lam _. _" [100,100] 100) |
|
19 |
|
20 locale name_subst = |
|
21 fixes name_subst :: "name \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> lam" |
|
22 assumes name_subst_eqvt [eqvt]: |
|
23 "p \<bullet> name_subst x xs t = name_subst (p \<bullet> x) (p \<bullet> xs) (p \<bullet> t)" |
|
24 and name_subst_fresh: "supp xs \<sharp>* t \<Longrightarrow> supp xs \<sharp>* name_subst x xs t" |
|
25 |
|
26 lemma set_map_atom_eq_supp: "set (map atom xs) = supp xs" |
|
27 by (metis List.finite_set image_set supp_finite_set_at_base supp_set) |
|
28 |
|
29 lemma atom_image_set_eq_supp: "atom ` set xs = supp xs" |
|
30 by (metis image_set set_map_atom_eq_supp) |
|
31 |
|
32 nominal_primrec (in name_subst) |
|
33 subst :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [120,120,120] 120) |
|
34 where |
|
35 "(Var x)[xs::=t] = name_subst x xs t" |
|
36 | "(s \<cdot> t)[xs::=u] = s[xs::=u] \<cdot> t[xs::=u]" |
|
37 | "\<lbrakk>supp xs \<sharp>* ys; supp xs \<sharp>* u\<rbrakk> \<Longrightarrow> (Lam xs. t)[ys::=u] = Lam xs. t[ys::=u]" |
|
38 apply auto |
|
39 -- {* 3 subgoals *} |
|
40 -- {* eqvt *} |
|
41 apply (unfold eqvt_def subst_graph_def subst_graph_aux_def) |
|
42 apply (rule, perm_simp, rule) |
|
43 -- {* exhaustion *} |
|
44 apply (rule_tac y=a and c="(aa, b)" in lam.strong_exhaust) |
|
45 apply auto |
|
46 apply (metis atom_image_set_eq_supp fresh_star_Pair) |
|
47 -- {* well-defined (compatibility) *} |
|
48 apply (rename_tac xs' ys u t') |
|
49 apply (erule Abs_lst_fcb2) |
|
50 apply (metis Abs_fresh_star(3) subset_refl) |
|
51 apply (metis fresh_star_Pair set_map_atom_eq_supp) |
|
52 apply (metis fresh_star_Pair set_map_atom_eq_supp) |
|
53 apply (auto simp add: eqvt_at_def) |
|
54 apply (metis Pair_eqvt perm_supp_eq) |
|
55 apply (metis Pair_eqvt perm_supp_eq) |
|
56 done |
|
57 |
|
58 termination (in name_subst) (eqvt) by lexicographic_order |
|
59 |
|
60 inductive (in name_subst) beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infix "\<longrightarrow>\<^sub>\<beta>" 90) |
|
61 where |
|
62 redex: "supp xs \<sharp>* u \<Longrightarrow> (Lam xs. t) \<cdot> u \<longrightarrow>\<^sub>\<beta> t[xs::=u]" |
|
63 | "s \<longrightarrow>\<^sub>\<beta> s' \<Longrightarrow> s \<cdot> t \<longrightarrow>\<^sub>\<beta> s' \<cdot> t" |
|
64 | "t \<longrightarrow>\<^sub>\<beta> t' \<Longrightarrow> s \<cdot> t \<longrightarrow>\<^sub>\<beta> s \<cdot> t'" |
|
65 |
|
66 equivariance (in name_subst) beta |
|
67 |
|
68 |
|
69 lemma lam_bound_fresh: "supp xs \<sharp>* (Lam xs. t)" |
|
70 by (simp add: atom_image_set_eq_supp fresh_star_def) |
|
71 |
|
72 |
|
73 lemma (in name_subst) subst_fresh: "supp xs \<sharp>* u \<Longrightarrow> supp xs \<sharp>* t[xs::=u]" |
|
74 apply (nominal_induct t avoiding: xs u rule: lam.strong_induct) |
|
75 apply (simp_all add: atom_image_set_eq_supp) |
|
76 apply (metis name_subst_fresh) |
|
77 apply (metis fresh_star_def lam.fresh(2)) |
|
78 apply (simp add: fresh_star_def) |
|
79 done |
|
80 |
|
81 nominal_inductive (in name_subst) beta |
|
82 avoids |
|
83 redex: xs |
|
84 apply (auto simp add: fresh_star_Pair) |
|
85 apply (metis atom_image_set_eq_supp fresh_star_def lam.fresh(2) lam_bound_fresh) |
|
86 apply (simp add: atom_image_set_eq_supp subst_fresh) |
|
87 done |
|
88 |
|
89 end |