7 |
7 |
8 nominal_datatype lam = |
8 nominal_datatype lam = |
9 Var "name" |
9 Var "name" |
10 | App "lam" "lam" |
10 | App "lam" "lam" |
11 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) |
11 | Lam x::"name" l::"lam" bind x in l ("Lam [_]. _" [100, 100] 100) |
|
12 |
|
13 |
|
14 text {* free name function - returns an atom list *} |
|
15 |
|
16 nominal_primrec |
|
17 frees_lst :: "lam \<Rightarrow> atom list" |
|
18 where |
|
19 "frees_lst (Var x) = [atom x]" |
|
20 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
|
21 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
|
22 unfolding eqvt_def frees_lst_graph_def |
|
23 apply (rule, perm_simp, rule) |
|
24 apply(rule TrueI) |
|
25 apply(rule_tac y="x" in lam.exhaust) |
|
26 apply(auto) |
|
27 apply (erule Abs_lst1_fcb) |
|
28 apply(simp add: supp_removeAll fresh_def) |
|
29 apply(drule supp_eqvt_at) |
|
30 apply(simp add: finite_supp) |
|
31 apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def) |
|
32 done |
|
33 |
|
34 termination |
|
35 by lexicographic_order |
|
36 |
|
37 text {* a small test lemma *} |
|
38 lemma shows "supp t = set (frees_lst t)" |
|
39 by (induct t rule: frees_lst.induct) (simp_all add: lam.supp supp_at_base) |
|
40 |
|
41 text {* free name function - returns an atom set *} |
12 |
42 |
13 nominal_primrec (invariant "\<lambda>x (y::atom set). finite y") |
43 nominal_primrec (invariant "\<lambda>x (y::atom set). finite y") |
14 frees_set :: "lam \<Rightarrow> atom set" |
44 frees_set :: "lam \<Rightarrow> atom set" |
15 where |
45 where |
16 "frees_set (Var x) = {atom x}" |
46 "frees_set (Var x) = {atom x}" |
28 apply(erule fresh_eqvt_at) |
58 apply(erule fresh_eqvt_at) |
29 apply(simp_all add: finite_supp eqvt_at_def eqvts) |
59 apply(simp_all add: finite_supp eqvt_at_def eqvts) |
30 done |
60 done |
31 |
61 |
32 termination |
62 termination |
33 by (relation "measure size") (auto simp add: lam.size) |
63 by lexicographic_order |
34 |
64 |
35 lemma "frees_set t = supp t" |
65 lemma "frees_set t = supp t" |
36 by (induct rule: frees_set.induct) (simp_all add: lam.supp supp_at_base) |
66 by (induct rule: frees_set.induct) (simp_all add: lam.supp supp_at_base) |
37 |
67 |
38 lemma fresh_fun_eqvt_app3: |
68 lemma fresh_fun_eqvt_app3: |
39 assumes a: "eqvt f" |
69 assumes a: "eqvt f" |
40 and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" |
70 and b: "a \<sharp> x" "a \<sharp> y" "a \<sharp> z" |
41 shows "a \<sharp> f x y z" |
71 shows "a \<sharp> f x y z" |
42 using fresh_fun_eqvt_app[OF a b(1)] a b |
72 using fresh_fun_eqvt_app[OF a b(1)] a b |
43 by (metis fresh_fun_app) |
73 by (metis fresh_fun_app) |
|
74 |
|
75 |
|
76 text {* A test with a locale and an interpretation. *} |
44 |
77 |
45 locale test = |
78 locale test = |
46 fixes f1::"name \<Rightarrow> ('a::pt)" |
79 fixes f1::"name \<Rightarrow> ('a::pt)" |
47 and f2::"lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a::pt)" |
80 and f2::"lam \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a::pt)" |
48 and f3::"name \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> ('a::pt)" |
81 and f3::"name \<Rightarrow> lam \<Rightarrow> 'a \<Rightarrow> ('a::pt)" |
76 apply (simp add: eqvt_at_def) |
109 apply (simp add: eqvt_at_def) |
77 apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def]) |
110 apply (simp add: permute_fun_app_eq eq[unfolded eqvt_def]) |
78 done |
111 done |
79 |
112 |
80 termination |
113 termination |
81 by (relation "measure size") (auto simp add: lam.size) |
114 by lexicographic_order |
82 |
|
83 thm f.simps |
|
84 |
115 |
85 end |
116 end |
86 |
|
87 |
|
88 thm test.f.simps |
|
89 thm test.f.simps[simplified test_def] |
|
90 |
|
91 thm test_def |
|
92 |
117 |
93 interpretation hei: test |
118 interpretation hei: test |
94 "%n. (1 :: nat)" |
119 "%n. (1 :: nat)" |
95 "%t1 t2 r1 r2. (r1 + r2)" |
120 "%t1 t2 r1 r2. (r1 + r2)" |
96 "%n t r. r + 1" |
121 "%n t r. r + 1" |
97 apply default |
122 apply default |
98 apply (auto simp add: pure_fresh supp_Pair) |
123 apply (auto simp add: pure_fresh supp_Pair) |
99 apply (simp_all add: fresh_def supp_def permute_fun_def permute_pure)[3] |
124 apply (simp_all add: fresh_def supp_def permute_fun_def permute_pure)[3] |
100 apply (simp_all add: eqvt_def permute_fun_def permute_pure) |
125 apply (simp_all add: eqvt_def permute_fun_def permute_pure) |
101 done |
126 done |
102 |
|
103 thm hei.f.simps |
|
104 |
|
105 inductive |
|
106 triv :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
|
107 where |
|
108 Var: "triv (Var x) n" |
|
109 | App: "\<lbrakk>triv t1 n; triv t2 n\<rbrakk> \<Longrightarrow> triv (App t1 t2) n" |
|
110 |
|
111 lemma |
|
112 "p \<bullet> (triv t x) = triv (p \<bullet> t) (p \<bullet> x)" |
|
113 unfolding triv_def |
|
114 apply(perm_simp) |
|
115 apply(rule refl) |
|
116 oops |
|
117 (*apply(perm_simp)*) |
|
118 |
|
119 ML {* |
|
120 Inductive.the_inductive @{context} "Lambda.triv" |
|
121 *} |
|
122 |
|
123 thm triv_def |
|
124 |
|
125 equivariance triv |
|
126 nominal_inductive triv avoids Var: "{}::name set" |
|
127 apply(auto simp add: fresh_star_def) |
|
128 done |
|
129 |
|
130 inductive |
|
131 triv2 :: "lam \<Rightarrow> nat \<Rightarrow> bool" |
|
132 where |
|
133 Var1: "triv2 (Var x) 0" |
|
134 | Var2: "triv2 (Var x) (n + n)" |
|
135 | Var3: "triv2 (Var x) n" |
|
136 |
|
137 equivariance triv2 |
|
138 nominal_inductive triv2 . |
|
139 |
|
140 |
127 |
141 text {* height function *} |
128 text {* height function *} |
142 |
129 |
143 nominal_primrec |
130 nominal_primrec |
144 height :: "lam \<Rightarrow> int" |
131 height :: "lam \<Rightarrow> int" |
154 apply (erule Abs_lst1_fcb) |
141 apply (erule Abs_lst1_fcb) |
155 apply(simp_all add: fresh_def pure_supp eqvt_at_def) |
142 apply(simp_all add: fresh_def pure_supp eqvt_at_def) |
156 done |
143 done |
157 |
144 |
158 termination |
145 termination |
159 by (relation "measure size") (simp_all add: lam.size) |
146 by lexicographic_order |
160 |
147 |
161 thm height.simps |
148 thm height.simps |
162 |
149 |
163 |
150 |
164 text {* free name function - returns atom lists *} |
|
165 |
|
166 nominal_primrec |
|
167 frees_lst :: "lam \<Rightarrow> atom list" |
|
168 where |
|
169 "frees_lst (Var x) = [atom x]" |
|
170 | "frees_lst (App t1 t2) = frees_lst t1 @ frees_lst t2" |
|
171 | "frees_lst (Lam [x]. t) = removeAll (atom x) (frees_lst t)" |
|
172 unfolding eqvt_def frees_lst_graph_def |
|
173 apply (rule, perm_simp, rule) |
|
174 apply(rule TrueI) |
|
175 apply(rule_tac y="x" in lam.exhaust) |
|
176 apply(auto) |
|
177 apply (erule Abs_lst1_fcb) |
|
178 apply(simp add: supp_removeAll fresh_def) |
|
179 apply(drule supp_eqvt_at) |
|
180 apply(simp add: finite_supp) |
|
181 apply(auto simp add: fresh_def supp_removeAll eqvts eqvt_at_def) |
|
182 done |
|
183 |
|
184 termination |
|
185 by (relation "measure size") (simp_all add: lam.size) |
|
186 |
|
187 text {* a small test lemma *} |
|
188 lemma shows "supp t = set (frees_lst t)" |
|
189 by (induct t rule: frees_lst.induct) (simp_all add: lam.supp supp_at_base) |
|
190 |
|
191 text {* capture - avoiding substitution *} |
151 text {* capture - avoiding substitution *} |
192 |
152 |
193 nominal_primrec |
153 nominal_primrec |
194 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
154 subst :: "lam \<Rightarrow> name \<Rightarrow> lam \<Rightarrow> lam" ("_ [_ ::= _]" [90, 90, 90] 90) |
195 where |
155 where |
211 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya") |
171 apply(subgoal_tac "(atom x \<rightleftharpoons> atom xa) \<bullet> ya = ya") |
212 apply(simp add: eqvt_at_def) |
172 apply(simp add: eqvt_at_def) |
213 apply(simp_all add: swap_fresh_fresh) |
173 apply(simp_all add: swap_fresh_fresh) |
214 done |
174 done |
215 |
175 |
216 termination |
176 declare lam.size[simp] |
217 by (relation "measure (\<lambda>(t,_,_). size t)") (simp_all add: lam.size) |
177 |
|
178 termination |
|
179 by lexicographic_order |
218 |
180 |
219 lemma subst_eqvt[eqvt]: |
181 lemma subst_eqvt[eqvt]: |
220 shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]" |
182 shows "(p \<bullet> t[x ::= s]) = (p \<bullet> t)[(p \<bullet> x) ::= (p \<bullet> s)]" |
221 by (induct t x s rule: subst.induct) (simp_all) |
183 by (induct t x s rule: subst.induct) (simp_all) |
222 |
184 |
333 also have "\<dots> \<longrightarrow>1 ((y \<leftrightarrow> x) \<bullet> t2)[y ::= s2]" using fs a by (auto simp add: One.eqvt) |
295 also have "\<dots> \<longrightarrow>1 ((y \<leftrightarrow> x) \<bullet> t2)[y ::= s2]" using fs a by (auto simp add: One.eqvt) |
334 also have "\<dots> = t2[x ::= s2]" using fs by (simp add: subst_rename[symmetric]) |
296 also have "\<dots> = t2[x ::= s2]" using fs by (simp add: subst_rename[symmetric]) |
335 finally show "App (Lam [x].t1) s1 \<longrightarrow>1 t2[x ::= s2]" by simp |
297 finally show "App (Lam [x].t1) s1 \<longrightarrow>1 t2[x ::= s2]" by simp |
336 qed |
298 qed |
337 |
299 |
338 |
|
339 |
|
340 section {* Locally Nameless Terms *} |
300 section {* Locally Nameless Terms *} |
341 |
301 |
342 nominal_datatype ln = |
302 nominal_datatype ln = |
343 LNBnd nat |
303 LNBnd nat |
344 | LNVar name |
304 | LNVar name |
371 by (case_tac "x \<in> set xs") (auto simp add: fresh_star_def fresh_def supp_lookup_in supp_lookup_notin) |
331 by (case_tac "x \<in> set xs") (auto simp add: fresh_star_def fresh_def supp_lookup_in supp_lookup_notin) |
372 |
332 |
373 lemma lookup_eqvt[eqvt]: |
333 lemma lookup_eqvt[eqvt]: |
374 shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
334 shows "(p \<bullet> lookup xs n x) = lookup (p \<bullet> xs) (p \<bullet> n) (p \<bullet> x)" |
375 by (induct xs arbitrary: n) (simp_all add: permute_pure) |
335 by (induct xs arbitrary: n) (simp_all add: permute_pure) |
|
336 |
|
337 text {* Function that translates lambda-terms into locally nameless terms *} |
376 |
338 |
377 nominal_primrec (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y") |
339 nominal_primrec (invariant "\<lambda>(_, xs) y. atom ` set xs \<sharp>* y") |
378 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
340 trans :: "lam \<Rightarrow> name list \<Rightarrow> ln" |
379 where |
341 where |
380 "trans (Var x) xs = lookup xs 0 x" |
342 "trans (Var x) xs = lookup xs 0 x" |
395 apply (rule finite_supp) |
357 apply (rule finite_supp) |
396 apply (auto simp add: supp_Pair fresh_def supp_Cons supp_at_base)[1] |
358 apply (auto simp add: supp_Pair fresh_def supp_Cons supp_at_base)[1] |
397 apply (simp add: eqvt_at_def swap_fresh_fresh) |
359 apply (simp add: eqvt_at_def swap_fresh_fresh) |
398 done |
360 done |
399 |
361 |
400 |
362 termination |
401 termination |
363 by lexicographic_order |
402 by (relation "measure (size o fst)") (simp_all add: lam.size) |
364 |
|
365 text {* count bound-variable occurences *} |
403 |
366 |
404 nominal_primrec |
367 nominal_primrec |
405 cbvs :: "lam \<Rightarrow> name list \<Rightarrow> nat" |
368 cbvs :: "lam \<Rightarrow> name list \<Rightarrow> nat" |
406 where |
369 where |
407 "cbvs (Var x) xs = (if x \<in> set xs then 1 else 0)" |
370 "cbvs (Var x) xs = (if x \<in> set xs then 1 else 0)" |
408 | "cbvs (App t1 t2) xs = (cbvs t1 xs) + (cbvs t2 xs)" |
371 | "cbvs (App t1 t2) xs = (cbvs t1 xs) + (cbvs t2 xs)" |
409 | "atom x \<sharp> xs \<Longrightarrow> cbvs (Lam [x]. t) xs = (cbvs t (x # xs))" |
372 | "atom x \<sharp> xs \<Longrightarrow> cbvs (Lam [x]. t) xs = cbvs t (x # xs)" |
410 apply(simp add: eqvt_def cbvs_graph_def) |
373 apply(simp add: eqvt_def cbvs_graph_def) |
411 apply(rule, perm_simp, rule) |
374 apply(rule, perm_simp, rule) |
412 apply(simp_all) |
375 apply(simp_all) |
413 apply(case_tac x) |
376 apply(case_tac x) |
414 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
377 apply(rule_tac y="a" and c="b" in lam.strong_exhaust) |
484 apply (simp add: eqvt_at_def) |
448 apply (simp add: eqvt_at_def) |
485 apply (metis atom_name_def swap_fresh_fresh fresh_at_list) |
449 apply (metis atom_name_def swap_fresh_fresh fresh_at_list) |
486 done |
450 done |
487 |
451 |
488 termination |
452 termination |
489 by (relation "measure (\<lambda>(t,_). size t)") (simp_all add: lam.size) |
453 by lexicographic_order |
490 |
454 |
491 lemma transdb_eqvt[eqvt]: |
455 lemma transdb_eqvt[eqvt]: |
492 "p \<bullet> transdb t l = transdb (p \<bullet>t) (p \<bullet>l)" |
456 "p \<bullet> transdb t l = transdb (p \<bullet>t) (p \<bullet>l)" |
493 apply (nominal_induct t avoiding: l p rule: lam.strong_induct) |
457 apply (nominal_induct t avoiding: l p rule: lam.strong_induct) |
494 apply (simp add: vindex_eqvt) |
458 apply (simp add: vindex_eqvt) |
654 apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app) |
619 apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app) |
655 apply (simp add: eqvt_def permute_fun_app_eq) |
620 apply (simp add: eqvt_def permute_fun_app_eq) |
656 done |
621 done |
657 |
622 |
658 termination |
623 termination |
659 by (relation "measure (\<lambda>(_,t). size t)") (simp_all add: lam.size) |
624 by lexicographic_order |
660 |
625 |
661 nominal_primrec |
626 nominal_primrec |
662 trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option" |
627 trans2 :: "lam \<Rightarrow> atom list \<Rightarrow> db option" |
663 where |
628 where |
664 "trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))" |
629 "trans2 (Var x) xs = (index xs 0 (atom x) \<guillemotright>= (\<lambda>n. Some (DBVar n)))" |