8 |
8 |
9 nominal_datatype lam = Var "name" |
9 nominal_datatype lam = Var "name" |
10 | App "lam" "lam" |
10 | App "lam" "lam" |
11 | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
11 | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100) |
12 |
12 |
|
13 consts |
|
14 depth :: "lam \<Rightarrow> nat" |
13 |
15 |
14 constdefs |
16 nominal_primrec |
15 depth_Var :: "name \<Rightarrow> nat" |
17 "depth (Var x) = 1" |
16 "depth_Var \<equiv> \<lambda>(a::name). 1" |
18 "depth (App t1 t2) = (max (depth t1) (depth t2)) + 1" |
17 |
19 "depth (Lam [a].t) = (depth t) + 1" |
18 depth_App :: "lam \<Rightarrow> lam \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" |
20 apply(finite_guess add: perm_nat_def)+ |
19 "depth_App \<equiv> \<lambda>_ _ n1 n2. (max n1 n2)+1" |
21 apply(rule TrueI)+ |
20 |
22 apply(simp add: fresh_nat) |
21 depth_Lam :: "name \<Rightarrow> lam \<Rightarrow> nat \<Rightarrow> nat" |
23 apply(fresh_guess add: perm_nat_def)+ |
22 "depth_Lam \<equiv> \<lambda>_ _ n. n+1" |
24 done |
23 |
|
24 depth_lam :: "lam \<Rightarrow> nat" |
|
25 "depth_lam t \<equiv> (lam_rec depth_Var depth_App depth_Lam) t" |
|
26 |
|
27 lemma fin_supp_depth_lam: |
|
28 shows "finite ((supp depth_Var)::name set)" |
|
29 and "finite ((supp depth_Lam)::name set)" |
|
30 and "finite ((supp depth_App)::name set)" |
|
31 by (finite_guess add: depth_Var_def depth_Lam_def depth_App_def perm_nat_def)+ |
|
32 |
|
33 lemma fcb_depth_lam: |
|
34 fixes a::"name" |
|
35 shows "a\<sharp>(depth_Lam a t n)" |
|
36 by (simp add: fresh_nat) |
|
37 |
|
38 lemma depth_lam: |
|
39 shows "depth_lam (Var a) = 1" |
|
40 and "depth_lam (App t1 t2) = (max (depth_lam t1) (depth_lam t2))+1" |
|
41 and "depth_lam (Lam [a].t) = (depth_lam t)+1" |
|
42 apply - |
|
43 apply(unfold depth_lam_def) |
|
44 apply(rule trans) |
|
45 apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified]) |
|
46 apply(simp_all add: fin_supp_depth_lam supp_unit) |
|
47 apply(simp add: fcb_depth_lam) |
|
48 apply(simp add: depth_Var_def) |
|
49 apply(rule trans) |
|
50 apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified]) |
|
51 apply(simp_all add: fin_supp_depth_lam supp_unit) |
|
52 apply(simp add: fcb_depth_lam) |
|
53 apply(simp add: depth_App_def) |
|
54 apply(rule trans) |
|
55 apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified]) |
|
56 apply(simp_all add: fin_supp_depth_lam supp_unit) |
|
57 apply(simp add: fcb_depth_lam) |
|
58 apply(simp add: depth_Var_def, fresh_guess add: perm_nat_def) |
|
59 apply(simp add: depth_App_def, fresh_guess add: perm_nat_def) |
|
60 apply(simp add: depth_Lam_def, fresh_guess add: perm_nat_def) |
|
61 apply(simp add: depth_Lam_def) |
|
62 done |
|
63 |
25 |
64 text {* capture-avoiding substitution *} |
26 text {* capture-avoiding substitution *} |
65 constdefs |
|
66 subst_Var :: "name \<Rightarrow>lam \<Rightarrow> name \<Rightarrow> lam" |
|
67 "subst_Var b t \<equiv> \<lambda>a. (if a=b then t else (Var a))" |
|
68 |
|
69 subst_App :: "name \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam" |
|
70 "subst_App b t \<equiv> \<lambda>_ _ r1 r2. App r1 r2" |
|
71 |
27 |
72 subst_Lam :: "name \<Rightarrow> lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam" |
|
73 "subst_Lam b t \<equiv> \<lambda>a _ r. Lam [a].r" |
|
74 |
|
75 abbreviation |
|
76 subst_syn :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 900) where |
|
77 "t'[b::=t] \<equiv> (lam_rec (subst_Var b t) (subst_App b t) (subst_Lam b t)) t'" |
|
78 |
|
79 (* FIXME: this lemma needs to be in Nominal.thy *) |
|
80 lemma eq_eqvt: |
28 lemma eq_eqvt: |
81 fixes pi::"name prm" |
29 fixes pi::"name prm" |
82 and x::"'a::pt_name" |
30 and x::"'a::pt_name" |
83 shows "pi\<bullet>(x=y) = ((pi\<bullet>x)=(pi\<bullet>y))" |
31 shows "pi\<bullet>(x=y) = ((pi\<bullet>x)=(pi\<bullet>y))" |
84 apply(simp add: perm_bool perm_bij) |
32 apply(simp add: perm_bool perm_bij) |
85 done |
33 done |
86 |
34 |
87 lemma fin_supp_subst: |
35 consts |
88 shows "finite ((supp (subst_Var b t))::name set)" |
36 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [100,100,100] 100) |
89 and "finite ((supp (subst_Lam b t))::name set)" |
|
90 and "finite ((supp (subst_App b t))::name set)" |
|
91 apply - |
|
92 apply(finite_guess add: subst_Var_def perm_if eq_eqvt fs_name1) |
|
93 apply(finite_guess add: subst_Lam_def fs_name1) |
|
94 apply(finite_guess add: subst_App_def fs_name1) |
|
95 done |
|
96 |
37 |
97 lemma fcb_subst: |
38 nominal_primrec |
98 fixes a::"name" |
39 "(Var x)[y::=t'] = (if x=y then t' else (Var x))" |
99 shows "a\<sharp>(subst_Lam b t) a t' r" |
40 "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])" |
100 by (simp add: subst_Lam_def abs_fresh) |
41 "x\<sharp>(y,t') \<Longrightarrow> (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])" |
101 |
42 apply(finite_guess add: eq_eqvt perm_if fs_name1)+ |
102 lemma subst[simp]: |
43 apply(rule TrueI)+ |
103 shows "(Var a)[b::=t] = (if a=b then t else (Var a))" |
44 apply(simp add: abs_fresh) |
104 and "(App t1 t2)[b::=t] = App (t1[b::=t]) (t2[b::=t])" |
45 apply(fresh_guess add: eq_eqvt perm_if fs_name1)+ |
105 and "a\<sharp>(b,t) \<Longrightarrow> (Lam [a].t1)[b::=t] = Lam [a].(t1[b::=t])" |
|
106 and "\<lbrakk>a\<noteq>b; a\<sharp>t\<rbrakk> \<Longrightarrow> (Lam [a].t1)[b::=t] = Lam [a].(t1[b::=t])" |
|
107 and "\<lbrakk>a\<sharp>b; a\<sharp>t\<rbrakk> \<Longrightarrow> (Lam [a].t1)[b::=t] = Lam [a].(t1[b::=t])" |
|
108 apply - |
|
109 apply(rule trans) |
|
110 apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified]) |
|
111 apply(simp add: fs_name1 fin_supp_subst)+ |
|
112 apply(simp add: fcb_subst) |
|
113 apply(simp add: subst_Var_def) |
|
114 apply(rule trans) |
|
115 apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified]) |
|
116 apply(simp add: fs_name1 fin_supp_subst)+ |
|
117 apply(simp add: fcb_subst) |
|
118 apply(simp add: subst_App_def) |
|
119 apply(rule trans) |
|
120 apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified]) |
|
121 apply(simp add: fs_name1 fin_supp_subst)+ |
|
122 apply(simp add: fcb_subst) |
|
123 apply(fresh_guess add: subst_Var_def perm_if eq_eqvt fs_name1) |
|
124 apply(fresh_guess add: subst_App_def fs_name1) |
|
125 apply(fresh_guess add: subst_Lam_def fs_name1) |
|
126 apply(simp add: subst_Lam_def) |
|
127 apply(rule trans) |
|
128 apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified]) |
|
129 apply(simp add: fs_name1 fin_supp_subst)+ |
|
130 apply(simp add: fcb_subst) |
|
131 apply(fresh_guess add: subst_Var_def perm_if eq_eqvt fs_name1 fresh_atm) |
|
132 apply(fresh_guess add: subst_App_def fs_name1 fresh_atm) |
|
133 apply(fresh_guess add: subst_Lam_def fs_name1 fresh_atm) |
|
134 apply(simp add: subst_Lam_def) |
|
135 apply(rule trans) |
|
136 apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified]) |
|
137 apply(simp add: fs_name1 fin_supp_subst)+ |
|
138 apply(simp add: fcb_subst) |
|
139 apply(fresh_guess add: subst_Var_def perm_if eq_eqvt fs_name1) |
|
140 apply(fresh_guess add: subst_App_def fs_name1) |
|
141 apply(fresh_guess add: subst_Lam_def fs_name1) |
|
142 apply(simp add: subst_Lam_def) |
|
143 done |
46 done |
144 |
47 |
145 lemma subst_eqvt[simp]: |
48 lemma subst_eqvt[simp]: |
146 fixes pi:: "name prm" |
49 fixes pi:: "name prm" |
147 and t1:: "lam" |
50 and t1:: "lam" |
187 apply(induct \<theta>) |
89 apply(induct \<theta>) |
188 apply(auto) |
90 apply(auto) |
189 apply(perm_simp)+ |
91 apply(perm_simp)+ |
190 done |
92 done |
191 |
93 |
192 constdefs |
94 consts |
193 psubst_Var :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam" |
95 psubst :: "lam \<Rightarrow> (name\<times>lam) list \<Rightarrow> lam" ("_[<_>]" [100,100] 900) |
194 "psubst_Var \<theta> \<equiv> \<lambda>a. (if a\<in>set (domain \<theta>) then \<theta><a> else (Var a))" |
|
195 |
|
196 psubst_App :: "(name\<times>lam) list \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam" |
|
197 "psubst_App \<theta> \<equiv> \<lambda>_ _ r1 r2. App r1 r2" |
|
198 |
96 |
199 psubst_Lam :: "(name\<times>lam) list \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam \<Rightarrow> lam" |
97 nominal_primrec |
200 "psubst_Lam \<theta> \<equiv> \<lambda>a _ r. Lam [a].r" |
98 "(Var x)[<\<theta>>] = (if x\<in>set (domain \<theta>) then \<theta><x> else (Var x))" |
201 |
99 "(App t1 t2)[<\<theta>>] = App (t1[<\<theta>>]) (t2[<\<theta>>])" |
202 abbreviation |
100 "x\<sharp>\<theta>\<Longrightarrow>(Lam [x].t)[<\<theta>>] = Lam [x].(t[<\<theta>>])" |
203 psubst_lam :: "lam \<Rightarrow> (name\<times>lam) list \<Rightarrow> lam" ("_[<_>]" [100,100] 900) where |
101 apply(finite_guess add: domain_eqvt apply_sss_eqvt fs_name1)+ |
204 "t[<\<theta>>] \<equiv> (lam_rec (psubst_Var \<theta>) (psubst_App \<theta>) (psubst_Lam \<theta>)) t" |
102 apply(rule TrueI)+ |
205 |
103 apply(simp add: abs_fresh) |
206 lemma fin_supp_psubst: |
104 apply(fresh_guess add: domain_eqvt apply_sss_eqvt fs_name1)+ |
207 shows "finite ((supp (psubst_Var \<theta>))::name set)" |
|
208 and "finite ((supp (psubst_Lam \<theta>))::name set)" |
|
209 and "finite ((supp (psubst_App \<theta>))::name set)" |
|
210 apply - |
|
211 apply(finite_guess add: fs_name1 psubst_Var_def domain_eqvt apply_sss_eqvt) |
|
212 apply(finite_guess add: fs_name1 psubst_Lam_def) |
|
213 apply(finite_guess add: fs_name1 psubst_App_def) |
|
214 done |
|
215 |
|
216 lemma fcb_psubst_Lam: |
|
217 shows "x\<sharp>(psubst_Lam \<theta>) x t r" |
|
218 by (simp add: psubst_Lam_def abs_fresh) |
|
219 |
|
220 lemma psubst[simp]: |
|
221 shows "(Var a)[<\<theta>>] = (if a\<in>set (domain \<theta>) then \<theta><a> else (Var a))" |
|
222 and "(App t1 t2)[<\<theta>>] = App (t1[<\<theta>>]) (t2[<\<theta>>])" |
|
223 and "a\<sharp>\<theta> \<Longrightarrow> (Lam [a].t1)[<\<theta>>] = Lam [a].(t1[<\<theta>>])" |
|
224 apply(rule trans) |
|
225 apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified]) |
|
226 apply(simp add: fin_supp_psubst fs_name1)+ |
|
227 apply(simp add: fcb_psubst_Lam) |
|
228 apply(simp add: psubst_Var_def) |
|
229 apply(rule trans) |
|
230 apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified]) |
|
231 apply(simp add: fin_supp_psubst fs_name1)+ |
|
232 apply(simp add: fcb_psubst_Lam) |
|
233 apply(simp add: psubst_App_def) |
|
234 apply(rule trans) |
|
235 apply(rule lam.recs[where P="\<lambda>_. True" and z="()", simplified]) |
|
236 apply(simp add: fin_supp_psubst fs_name1)+ |
|
237 apply(simp add: fcb_psubst_Lam) |
|
238 apply(fresh_guess add: psubst_Var_def domain_eqvt apply_sss_eqvt fs_name1) |
|
239 apply(fresh_guess add: psubst_App_def fs_name1) |
|
240 apply(fresh_guess add: psubst_Lam_def fs_name1) |
|
241 apply(simp add: psubst_Lam_def) |
|
242 done |
105 done |
243 |
106 |
244 end |
107 end |