1 theory Lambda_Exec |
|
2 imports Name_Exec |
|
3 begin |
|
4 |
|
5 nominal_datatype lam = |
|
6 Var "name" |
|
7 | App "lam" "lam" |
|
8 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
|
9 |
|
10 nominal_primrec |
|
11 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
|
12 where |
|
13 "(Var x)[y ::= s] = (if x = y then s else (Var x))" |
|
14 | "(App t1 t2)[y ::= s] = App (t1[y ::= s]) (t2[y ::= s])" |
|
15 | "atom x \<sharp> (y, s) \<Longrightarrow> (Lam [x]. t)[y ::= s] = Lam [x].(t[y ::= s])" |
|
16 proof auto |
|
17 fix a b :: lam and aa :: name and P |
|
18 assume "\<And>x y s. a = Var x \<and> aa = y \<and> b = s \<Longrightarrow> P" |
|
19 "\<And>t1 t2 y s. a = App t1 t2 \<and> aa = y \<and> b = s \<Longrightarrow> P" |
|
20 "\<And>x y s t. \<lbrakk>atom x \<sharp> (y, s); a = Lam [x]. t \<and> aa = y \<and> b = s\<rbrakk> \<Longrightarrow> P" |
|
21 then show "P" |
|
22 by (rule_tac y="a" and c="(aa, b)" in lam.strong_exhaust) |
|
23 (blast, blast, simp add: fresh_star_def) |
|
24 next |
|
25 fix x :: name and t and xa :: name and ya sa ta |
|
26 assume *: "eqvt_at subst_sumC (t, ya, sa)" |
|
27 "atom x \<sharp> (ya, sa)" "atom xa \<sharp> (ya, sa)" |
|
28 "[[atom x]]lst. t = [[atom xa]]lst. ta" |
|
29 then show "[[atom x]]lst. subst_sumC (t, ya, sa) = [[atom xa]]lst. subst_sumC (ta, ya, sa)" |
|
30 apply - |
|
31 apply (erule Abs_lst1_fcb) |
|
32 apply(simp (no_asm) add: Abs_fresh_iff) |
|
33 apply(drule_tac a="atom xa" in fresh_eqvt_at) |
|
34 apply(simp add: finite_supp) |
|
35 apply(simp_all add: fresh_Pair_elim Abs_fresh_iff Abs1_eq_iff) |
|
36 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya") |
|
37 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> sa = sa") |
|
38 apply(simp add: atom_eqvt eqvt_at_def) |
|
39 apply(rule perm_supp_eq, simp add: supp_swap fresh_star_def fresh_Pair)+ |
|
40 done |
|
41 next |
|
42 show "eqvt subst_graph" unfolding eqvt_def subst_graph_def |
|
43 by (rule, perm_simp, rule) |
|
44 qed |
|
45 |
|
46 termination (eqvt) by lexicographic_order |
|
47 |
|
48 datatype ln = |
|
49 LNBnd nat |
|
50 | LNVar name |
|
51 | LNApp ln ln |
|
52 | LNLam ln |
|
53 |
|
54 instantiation ln :: pt begin |
|
55 fun |
|
56 permute_ln |
|
57 where |
|
58 "p \<bullet> LNBnd n = LNBnd (p \<bullet> n)" |
|
59 | "p \<bullet> LNVar v = LNVar (p \<bullet> v)" |
|
60 | "p \<bullet> LNApp d1 d2 = LNApp (p \<bullet> d1) (p \<bullet> d2)" |
|
61 | "p \<bullet> LNLam d = LNLam (p \<bullet> d)" |
|
62 instance |
|
63 by (default, induct_tac [!] x) simp_all |
|
64 end |
|
65 |
|
66 lemmas [eqvt] = permute_ln.simps |
|
67 |
|
68 lemma ln_supports: |
|
69 "supp (n) supports LNBnd n" |
|
70 "supp (v) supports LNVar v" |
|
71 "supp (za, z) supports LNApp z za" |
|
72 "supp (z) supports LNLam z" |
|
73 by (simp_all add: supports_def fresh_def[symmetric]) |
|
74 (perm_simp, simp add: swap_fresh_fresh fresh_Pair)+ |
|
75 |
|
76 instance ln :: fs |
|
77 apply default |
|
78 apply (induct_tac x) |
|
79 apply (rule supports_finite, rule ln_supports, simp add: finite_supp supp_Pair)+ |
|
80 done |
|
81 |
|
82 lemma ln_supp: |
|
83 "supp (LNBnd n) = supp n" |
|
84 "supp (LNVar name) = supp name" |
|
85 "supp (LNApp ln1 ln2) = supp ln1 \<union> supp ln2" |
|
86 "supp (LNLam ln) = supp ln" |
|
87 unfolding supp_Pair[symmetric] |
|
88 by (simp_all add: supp_def) |
|
89 |
|
90 lemma ln_fresh: |
|
91 "x \<sharp> LNBnd n \<longleftrightarrow> True" |
|
92 "x \<sharp> LNVar name \<longleftrightarrow> x \<sharp> name" |
|
93 "x \<sharp> LNApp ln1 ln2 \<longleftrightarrow> x \<sharp> ln1 \<and> x \<sharp> ln2" |
|
94 "x \<sharp> LNLam ln = x \<sharp> ln" |
|
95 unfolding fresh_def |
|
96 by (simp_all add: ln_supp pure_supp) |
|
97 |
|
98 fun |
|
99 lookup :: "name list \<Rightarrow> nat \<Rightarrow> name \<Rightarrow> ln" |
|
100 where |
|
101 "lookup [] n x = LNVar x" |
|
102 | "lookup (y # ys) n x = (if x = y then LNBnd n else (lookup ys (n + 1) x))" |
|
103 |
|
104 lemma supp_lookup: |
|
105 shows "supp (lookup xs n x) \<subseteq> {atom x}" |
|
106 by (induct arbitrary: n rule: lookup.induct) |
|
107 (simp_all add: supp_at_base ln_supp pure_supp) |
|
108 |
|
109 lemma supp_lookup_in: |
|
110 shows "x \<in> set xs \<Longrightarrow> supp (lookup xs n x) = {}" |
|
111 by (induct arbitrary: n rule: lookup.induct) (auto simp add: ln_supp pure_supp) |
|
112 |
|
113 lemma supp_lookup_notin: |
|
114 shows "x \<notin> set xs \<Longrightarrow> supp (lookup xs n x) = {atom x}" |
|
115 by (induct arbitrary: n rule: lookup.induct) (auto simp add: ln_supp pure_supp supp_at_base) |
|
116 |
|
117 lemma supp_lookup_fresh: |
|
118 shows "atom ` set xs \<sharp>* lookup xs n x" |
|
119 by (case_tac "x \<in> set xs") (auto simp add: fresh_star_def fresh_def supp_lookup_in supp_lookup_notin) |
|
120 |
|
121 lemma lookup_eqvt[eqvt]: |
|
122 shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
|
123 by (induct xs arbitrary: n) (simp_all add: permute_pure) |
|
124 |
|
125 nominal_primrec (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y") |
|
126 lam_ln_aux :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
|
127 where |
|
128 "lam_ln_aux (Var x) xs = lookup xs 0 x" |
|
129 | "lam_ln_aux (App t1 t2) xs = LNApp (lam_ln_aux t1 xs) (lam_ln_aux t2 xs)" |
|
130 | "atom x \<sharp> xs \<Longrightarrow> lam_ln_aux (Lam [x]. t) xs = LNLam (lam_ln_aux t (x # xs))" |
|
131 apply (simp add: eqvt_def lam_ln_aux_graph_def) |
|
132 apply (rule, perm_simp, rule) |
|
133 apply (erule lam_ln_aux_graph.induct) |
|
134 apply (auto simp add: ln_supp)[3] |
|
135 apply (simp add: supp_lookup_fresh) |
|
136 apply (simp add: fresh_star_def ln_supp fresh_def) |
|
137 apply (simp add: ln_supp fresh_def fresh_star_def) |
|
138 apply (case_tac x) |
|
139 apply (rule_tac y="a" and c="b" in lam.strong_exhaust) |
|
140 apply (auto simp add: fresh_star_def)[3] |
|
141 apply(simp_all) |
|
142 apply(erule conjE) |
|
143 apply (erule_tac c="xsa" in Abs_lst1_fcb2') |
|
144 apply (simp_all add: fresh_star_def)[2] |
|
145 apply (simp_all add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
|
146 done |
|
147 |
|
148 termination (eqvt) by lexicographic_order |
|
149 |
|
150 definition lam_ln where "lam_ln t \<equiv> lam_ln_aux t []" |
|
151 |
|
152 fun nth_or_def where |
|
153 "nth_or_def [] _ d = d" |
|
154 | "nth_or_def (h # t) 0 d = h" |
|
155 | "nth_or_def (h # t) (Suc n) d = nth_or_def t n d" |
|
156 |
|
157 lemma nth_or_def_eqvt [eqvt]: |
|
158 "p \<bullet> (nth_or_def l n d) = nth_or_def (p \<bullet> l) (p \<bullet> n) (p \<bullet> d)" |
|
159 apply (cases l) |
|
160 apply auto |
|
161 apply (induct n arbitrary: list) |
|
162 apply (auto simp add: permute_pure) |
|
163 apply (case_tac list) |
|
164 apply simp_all |
|
165 done |
|
166 |
|
167 nominal_primrec |
|
168 ln_lam_aux :: "ln \<Rightarrow> name list \<Rightarrow> lam" |
|
169 where |
|
170 "ln_lam_aux (LNBnd n) ns = (nth_or_def (map Var ns) n (Lam [x]. Var x))" |
|
171 | "ln_lam_aux (LNVar v) ns = Var v" |
|
172 | "ln_lam_aux (LNApp l1 l2) ns = App (ln_lam_aux l1 ns) (ln_lam_aux l2 ns)" |
|
173 | "atom x \<sharp> (ns, l) \<Longrightarrow> ln_lam_aux (LNLam l) ns = Lam [x]. (ln_lam_aux l (x # ns))" |
|
174 apply (simp add: eqvt_def ln_lam_aux_graph_def) |
|
175 apply (rule, perm_simp, rule) |
|
176 apply rule |
|
177 apply(auto)[1] |
|
178 apply (rule_tac y="a" in ln.exhaust) |
|
179 apply (auto simp add: fresh_star_def)[4] |
|
180 using obtain_fresh apply metis |
|
181 apply (auto simp add: fresh_Pair_elim) |
|
182 apply (subgoal_tac "Lam [x]. Var x = Lam [xa]. Var xa") |
|
183 apply (simp del: lam.eq_iff) |
|
184 apply (simp add: Abs1_eq_iff lam.fresh fresh_at_base) |
|
185 apply (simp add: Abs1_eq_iff) |
|
186 apply (case_tac "x=xa") |
|
187 apply simp_all |
|
188 apply rule |
|
189 apply (auto simp add: eqvt_at_def swap_fresh_fresh)[1] |
|
190 apply (erule fresh_eqvt_at) |
|
191 apply (simp add: supp_Pair finite_supp) |
|
192 apply (simp add: fresh_Pair fresh_Cons fresh_at_base) |
|
193 done |
|
194 |
|
195 termination (eqvt) |
|
196 by lexicographic_order |
|
197 |
|
198 definition ln_lam where "ln_lam t \<equiv> ln_lam_aux t []" |
|
199 |
|
200 lemma l_fresh_lam_ln_aux: "atom ` set l \<sharp>* lam_ln_aux t l" |
|
201 apply (nominal_induct t avoiding: l rule: lam.strong_induct) |
|
202 apply (simp_all add: fresh_def ln_supp pure_supp) |
|
203 apply (auto simp add: fresh_star_def)[1] |
|
204 apply (case_tac "a = name") |
|
205 apply (auto simp add: supp_lookup_in fresh_def)[1] |
|
206 apply (simp add: fresh_def) |
|
207 using supp_lookup |
|
208 apply (metis (lifting) atom_eq_iff equals0D singletonE supp_lookup_in supp_lookup_notin) |
|
209 apply (simp add: fresh_star_def fresh_def ln_supp)+ |
|
210 done |
|
211 |
|
212 lemma supp_lam_ln_aux: "supp (lam_ln_aux t l) \<subseteq> supp t" |
|
213 proof - |
|
214 have "eqvt lam_ln_aux" unfolding eqvt_def using eqvts_raw by simp |
|
215 then have "supp lam_ln_aux = {}" using supp_fun_eqvt by auto |
|
216 then have "supp (lam_ln_aux t) \<subseteq> supp t" using supp_fun_app by auto |
|
217 then have "supp (lam_ln_aux t l) \<subseteq> supp t \<union> supp l" using supp_fun_app by auto |
|
218 moreover have "\<forall>x \<in> supp l. x \<notin> supp (lam_ln_aux t l)" |
|
219 using l_fresh_lam_ln_aux unfolding fresh_star_def fresh_def |
|
220 by (metis finite_set supp_finite_set_at_base supp_set) |
|
221 ultimately show "supp (lam_ln_aux t l) \<subseteq> supp t" by blast |
|
222 qed |
|
223 |
|
224 lemma lookup_flip: "x \<noteq> y \<Longrightarrow> y \<noteq> a \<Longrightarrow> lookup ((x \<leftrightarrow> a) \<bullet> xs) n y = lookup xs n y" |
|
225 apply (induct xs arbitrary: n) |
|
226 apply simp |
|
227 apply (simp only: Cons_eqvt) |
|
228 apply (simp only: lookup.simps) |
|
229 apply (subgoal_tac "y = (x \<leftrightarrow> a) \<bullet> aa \<longleftrightarrow> y = aa") |
|
230 apply simp |
|
231 by (metis permute_flip_at) |
|
232 |
|
233 lemma lookup_append_flip: "x \<noteq> y \<Longrightarrow> lookup (l @ a # (x \<leftrightarrow> a) \<bullet> xs) n y = lookup (l @ a # xs) n y" |
|
234 by (induct l arbitrary: n) (auto simp add: lookup_flip) |
|
235 |
|
236 lemma lam_ln_aux_flip: "atom x \<sharp> t \<Longrightarrow> lam_ln_aux t (l @ a # (x \<leftrightarrow> a) \<bullet> xs) = lam_ln_aux t (l @ a # xs)" |
|
237 apply (nominal_induct t avoiding: x a xs l rule: lam.strong_induct) |
|
238 apply (simp_all add: lam_ln_aux.eqvt lam.fresh lookup_append_flip fresh_at_base)[2] |
|
239 apply (simp add: lam.fresh fresh_at_base) |
|
240 apply (subst lam_ln_aux.simps) |
|
241 apply (simp add: fresh_Cons fresh_at_base fresh_append) |
|
242 apply (metis atom_eqvt atom_name_def flip_at_base_simps(3) flip_commute fresh_permute_iff) |
|
243 apply (subst lam_ln_aux.simps) |
|
244 apply (simp add: fresh_Cons fresh_at_base fresh_append) |
|
245 apply simp |
|
246 apply (drule_tac x="x" in meta_spec) |
|
247 apply (drule_tac x="a" in meta_spec) |
|
248 apply (drule_tac x="xs" in meta_spec) |
|
249 apply (drule_tac x="name # l" in meta_spec) |
|
250 apply simp |
|
251 done |
|
252 |
|
253 lemma lam_ln_aux4: "lam_ln_aux (Lam [x]. t) xs = LNLam (lam_ln_aux t (x # xs))" |
|
254 apply (rule_tac 'a="name" and x="(xs, x, t)" in obtain_fresh) |
|
255 apply (simp add: fresh_Pair_elim) |
|
256 apply (rule_tac t="Lam [x]. t" and s="Lam [a]. ((x \<leftrightarrow> a) \<bullet> t)" in subst) |
|
257 apply (auto simp add: Abs1_eq_iff lam.fresh flip_def swap_commute)[1] |
|
258 apply simp |
|
259 apply (rule_tac s="(x \<leftrightarrow> a) \<bullet> lam_ln_aux t (x # xs)" in trans) |
|
260 apply (simp add: lam_ln_aux.eqvt) |
|
261 apply (subst lam_ln_aux_flip[of _ _ "[]", simplified]) |
|
262 apply (metis atom_eqvt flip_at_simps(2) fresh_permute_iff) |
|
263 apply rule |
|
264 apply (rule flip_fresh_fresh) |
|
265 apply (simp add: l_fresh_lam_ln_aux[of "x # xs", simplified fresh_star_def, simplified]) |
|
266 apply (simp add: fresh_def) |
|
267 apply (metis set_rev_mp supp_lam_ln_aux) |
|
268 done |
|
269 |
|
270 lemma lookup_in: "n \<notin> set l \<Longrightarrow> lookup l i n = LNVar n" |
|
271 by (induct l arbitrary: i n) simp_all |
|
272 |
|
273 lemma lookup_in2: "n \<in> set l \<Longrightarrow> \<exists>i. lookup l j n = LNBnd i" |
|
274 by (induct l arbitrary: j n) auto |
|
275 |
|
276 lemma lookup_in2': "lookup l j n = LNBnd i \<Longrightarrow> lookup l (Suc j) n = LNBnd (Suc i)" |
|
277 by (induct l arbitrary: j n) auto |
|
278 |
|
279 lemma ln_lam_Var: "ln_lam_aux (lookup l (0\<Colon>nat) n) l = Var n" |
|
280 apply (cases "n \<in> set l") |
|
281 apply (simp_all add: lookup_in) |
|
282 apply (induct l arbitrary: n) |
|
283 apply simp |
|
284 apply (case_tac "a = n") |
|
285 apply (simp_all add: ln_lam_aux.simps(1)[of _ _ "Name 0"] )[2] |
|
286 apply (drule_tac x="n" in meta_spec) |
|
287 apply (frule lookup_in2[of _ _ 0]) |
|
288 apply (erule exE) |
|
289 apply simp |
|
290 apply (frule lookup_in2') |
|
291 apply simp |
|
292 apply (simp_all add: ln_lam_aux.simps(1)[of _ _ "Name 0"] ) |
|
293 done |
|
294 |
|
295 lemma ln_lam_ln_aux: "ln_lam_aux (lam_ln_aux t l) l = t" |
|
296 apply (nominal_induct t avoiding: l rule: lam.strong_induct) |
|
297 apply (simp_all add: ln_lam_Var) |
|
298 apply (subst ln_lam_aux.simps(4)[of name]) |
|
299 apply (simp add: fresh_Pair) |
|
300 apply (subgoal_tac "atom ` set (name # l) \<sharp>* lam_ln_aux lam (name # l)") |
|
301 apply (simp add: fresh_star_def) |
|
302 apply (rule l_fresh_lam_ln_aux) |
|
303 apply simp |
|
304 done |
|
305 |
|
306 fun subst_ln_nat where |
|
307 "subst_ln_nat (LNBnd n) x _ = LNBnd n" |
|
308 | "subst_ln_nat (LNVar v) x n = (if x = v then LNBnd n else LNVar v)" |
|
309 | "subst_ln_nat (LNApp l r) x n = LNApp (subst_ln_nat l x n) (subst_ln_nat r x n)" |
|
310 | "subst_ln_nat (LNLam l) x n = LNLam (subst_ln_nat l x (n + 1))" |
|
311 |
|
312 lemma subst_ln_nat_eqvt[eqvt]: |
|
313 shows "(p \<bullet> subst_ln_nat t x n) = subst_ln_nat (p \<bullet> t) (p \<bullet> x) (p \<bullet> n)" |
|
314 by (induct t arbitrary: n) (simp_all add: permute_pure) |
|
315 |
|
316 lemma supp_subst_ln_nat: |
|
317 "supp (subst_ln_nat t x n) = supp t - {atom x}" |
|
318 by (induct t arbitrary: n) (auto simp add: permute_pure ln_supp pure_supp supp_at_base) |
|
319 |
|
320 lemma fresh_subst_ln_nat: |
|
321 "atom y \<sharp> subst_ln_nat t x n \<longleftrightarrow> y = x \<or> atom y \<sharp> t" |
|
322 unfolding fresh_def supp_subst_ln_nat by auto |
|
323 |
|
324 nominal_primrec |
|
325 lam_ln_ex :: "lam \<Rightarrow> ln" |
|
326 where |
|
327 "lam_ln_ex (Var x) = LNVar x" |
|
328 | "lam_ln_ex (App t1 t2) = LNApp (lam_ln_ex t1) (lam_ln_ex t2)" |
|
329 | "lam_ln_ex (Lam [x]. t) = LNLam (subst_ln_nat (lam_ln_ex t) x 0)" |
|
330 apply (simp add: eqvt_def lam_ln_ex_graph_def) |
|
331 apply (rule, perm_simp, rule) |
|
332 apply rule |
|
333 apply (rule_tac y="x" in lam.exhaust) |
|
334 apply (auto simp add: fresh_star_def)[3] |
|
335 apply(simp_all) |
|
336 apply (erule_tac Abs_lst1_fcb) |
|
337 apply (simp add: fresh_subst_ln_nat) |
|
338 apply (simp add: fresh_subst_ln_nat) |
|
339 apply (erule fresh_eqvt_at) |
|
340 apply (simp add: finite_supp) |
|
341 apply assumption |
|
342 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq |
|
343 subst_ln_nat_eqvt permute_pure) |
|
344 apply simp |
|
345 done |
|
346 |
|
347 termination (eqvt) by lexicographic_order |
|
348 |
|
349 lemma lookup_in3: "lookup l j n = LNBnd i \<Longrightarrow> lookup (l @ l2) j n = LNBnd i" |
|
350 by (induct l arbitrary: j n) auto |
|
351 |
|
352 lemma lookup_in4: "n \<notin> set l \<Longrightarrow> lookup (l @ [n]) j n = LNBnd (length l + j)" |
|
353 by (induct l arbitrary: j n) auto |
|
354 |
|
355 lemma subst_ln_nat_lam_ln_aux: "subst_ln_nat (lam_ln_aux l ns) n (List.length ns) = lam_ln_aux l (ns @ [n])" |
|
356 apply (nominal_induct l avoiding: n ns rule: lam.strong_induct) |
|
357 apply simp defer |
|
358 apply simp |
|
359 apply (simp add: fresh_Nil fresh_Cons fresh_append) |
|
360 apply (drule_tac x="n" in meta_spec) |
|
361 apply (drule_tac x="name # ns" in meta_spec) |
|
362 apply simp |
|
363 apply (case_tac "name \<in> set ns") |
|
364 apply (simp_all add: lookup_in) |
|
365 apply (frule lookup_in2[of _ _ 0]) |
|
366 apply (erule exE) |
|
367 apply (simp add: lookup_in3) |
|
368 apply (simp add: lookup_in4) |
|
369 done |
|
370 |
|
371 lemma lam_ln_ex: "lam_ln_ex t = lam_ln t" |
|
372 apply (induct t rule: lam.induct) |
|
373 apply (simp_all add: lam_ln_def fresh_Nil) |
|
374 by (metis (lifting) list.size(3) self_append_conv2 subst_ln_nat_lam_ln_aux) |
|
375 |
|
376 (* Lambda terms as a code-abstype *) |
|
377 lemma ln_abstype[code abstype]: |
|
378 "ln_lam (lam_ln_ex t) = t" |
|
379 by (simp add: ln_lam_def lam_ln_ex lam_ln_def ln_lam_ln_aux) |
|
380 |
|
381 lemmas [code abstract] = lam_ln_ex.simps |
|
382 |
|
383 (* Equality for lambda-terms *) |
|
384 instantiation lam :: equal begin |
|
385 |
|
386 definition equal_lam_def: "equal_lam a b \<longleftrightarrow> lam_ln_ex a = lam_ln_ex b" |
|
387 |
|
388 instance |
|
389 by default |
|
390 (metis equal_lam_def lam_ln_def lam_ln_ex ln_lam_ln_aux) |
|
391 |
|
392 end |
|
393 |
|
394 (* Execute permutations *) |
|
395 lemmas [code abstract] = lam_ln_ex.eqvt[symmetric] |
|
396 |
|
397 fun subst_ln where |
|
398 "subst_ln (LNBnd n) _ _ = LNBnd n" |
|
399 | "subst_ln (LNVar v) x t = (if x = v then t else LNVar v)" |
|
400 | "subst_ln (LNApp l r) x t = LNApp (subst_ln l x t) (subst_ln r x t)" |
|
401 | "subst_ln (LNLam l) x t = LNLam (subst_ln l x t)" |
|
402 |
|
403 lemma subst_ln_nat_id[simp]: |
|
404 "atom name \<sharp> s \<Longrightarrow> name \<noteq> y \<Longrightarrow> subst_ln_nat s name n = s" |
|
405 by (induct s arbitrary: n) (simp_all add: ln_fresh fresh_at_base) |
|
406 |
|
407 lemma subst_ln_nat_subst_ln_commute: |
|
408 assumes "name \<noteq> y" and "atom name \<sharp> s" |
|
409 shows "subst_ln_nat (subst_ln ln y s) name n = subst_ln (subst_ln_nat ln name n) y s" |
|
410 using assms by (induct ln arbitrary: n) auto |
|
411 |
|
412 lemma supp_lam_ln_ex: "supp (lam_ln_ex t) = supp t" |
|
413 by (induct t rule: lam.induct) (simp_all add: lam.supp ln_supp supp_subst_ln_nat) |
|
414 |
|
415 lemma subst_code[code abstract]: |
|
416 "lam_ln_ex (subst t y s) = subst_ln (lam_ln_ex t) y (lam_ln_ex s)" |
|
417 apply (nominal_induct t avoiding: y s rule: lam.strong_induct) |
|
418 apply simp_all |
|
419 apply (subst subst_ln_nat_subst_ln_commute) |
|
420 apply (simp_all add: fresh_at_base supp_lam_ln_ex fresh_def) |
|
421 done |
|
422 |
|
423 (*definition "I0 \<equiv> Lam [N0]. (Var N0)" |
|
424 definition "I1 \<equiv> Lam [N1]. (Var N1)" |
|
425 definition "ppp = (atom N0 \<rightleftharpoons> atom N1)" |
|
426 definition "pp \<equiv> ppp \<bullet> I1 = I0" |
|
427 |
|
428 export_code pp in SML*) |
|
429 |
|
430 lemma subst_ln_nat_funpow[simp]: |
|
431 "subst_ln_nat ((LNLam^^p) l) x n = (LNLam ^^ p) (subst_ln_nat l x (n + p))" |
|
432 by (induct p arbitrary: n) simp_all |
|
433 |
|
434 (* |
|
435 |
|
436 Tests: |
|
437 |
|
438 fun Umn :: "nat \<Rightarrow> nat \<Rightarrow> lam" |
|
439 where |
|
440 "Umn 0 n = Lam [Name 0]. Var (Name n)" |
|
441 | "Umn (Suc m) n = Lam [Name (Suc m)]. Umn m n" |
|
442 |
|
443 lemma Umn_faster: |
|
444 "lam_ln_ex (Umn m n) = (LNLam ^^ (Suc m)) (if n \<le> m then LNBnd n else LNVar (Name n))" |
|
445 apply (induct m) |
|
446 apply (auto simp add: Umn.simps) |
|
447 apply (simp_all add: Name_def Abs_name_inject le_SucE) |
|
448 apply (erule le_SucE) |
|
449 apply simp_all |
|
450 done |
|
451 |
|
452 definition "Bla = Umn 2 2" |
|
453 |
|
454 definition vara where "vara \<equiv> Lam [N0]. Lam [N1]. (App (Var N1) (App (Umn 2 2) (App (Var N0) (Var N1))))" |
|
455 |
|
456 export_code ln_lam_aux nth_or_def ln_lam subst vara in SML |
|
457 |
|
458 value "(atom N0 \<rightleftharpoons> atom N1) \<bullet> (App (Var N0) (Lam [N1]. (Var N1)))" |
|
459 value "subst ((N0 \<leftrightarrow> N1) \<bullet> (App (Var N0) (Lam [N1]. (Var N1)))) N1 (Var N0)"*) |
|
460 |
|
461 end |
|
462 |
|
463 |
|
464 |
|