equal
deleted
inserted
replaced
10 apply(simp add: supp_swap fresh_def) |
10 apply(simp add: supp_swap fresh_def) |
11 done |
11 done |
12 |
12 |
13 atom_decl name |
13 atom_decl name |
14 |
14 |
|
15 thm obtain_atom |
|
16 |
|
17 lemma |
|
18 "(\<forall>thesis. (finite X \<longrightarrow> (\<forall>a. ((a \<notin> X \<and> sort_of a = s) \<longrightarrow> thesis)) \<longrightarrow> thesis)) \<longleftrightarrow> |
|
19 (finite X \<longrightarrow> (\<exists> a. (a \<notin> X \<and> sort_of a = s)))" |
|
20 apply(auto) |
|
21 done |
|
22 |
|
23 |
|
24 |
15 ML {* trace := true *} |
25 ML {* trace := true *} |
16 |
26 |
17 nominal_datatype lam = |
27 nominal_datatype lam = |
18 Var "name" |
28 Var "name" |
19 | App "lam" "lam" |
29 | App "lam" "lam" |
20 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
30 | Lam x::"name" l::"lam" binds x in l ("Lam [_]. _" [100, 100] 100) |
|
31 |
|
32 nominal_datatype environment = |
|
33 Ni |
|
34 | En name closure environment |
|
35 and closure = |
|
36 Clos "lam" "environment" |
|
37 |
|
38 thm environment_closure.exhaust(1) |
|
39 |
|
40 nominal_function |
|
41 env_lookup :: "environment => name => closure" |
|
42 where |
|
43 "env_lookup Ni x = Clos (Var x) Ni" |
|
44 | "env_lookup (En v clos rest) x = (if (v = x) then clos else env_lookup rest x)" |
|
45 apply (auto) |
|
46 apply (simp add: env_lookup_graph_aux_def eqvt_def) |
|
47 by (metis environment_closure.strong_exhaust(1)) |
|
48 |
21 |
49 |
22 lemma |
50 lemma |
23 "Lam [x]. Var x = Lam [y]. Var y" |
51 "Lam [x]. Var x = Lam [y]. Var y" |
24 proof - |
52 proof - |
25 obtain c::name where fresh: "atom c \<sharp> (Lam [x]. Var x, Lam [y]. Var y)" |
53 obtain c::name where fresh: "atom c \<sharp> (Lam [x]. Var x, Lam [y]. Var y)" |
230 nominal_termination (eqvt) by lexicographic_order |
258 nominal_termination (eqvt) by lexicographic_order |
231 |
259 |
232 |
260 |
233 section {* free name function *} |
261 section {* free name function *} |
234 |
262 |
|
263 |
|
264 lemma fresh_removeAll_name: |
|
265 fixes x::"name" |
|
266 and xs:: "name list" |
|
267 shows "atom x \<sharp> (removeAll y xs) \<longleftrightarrow> (atom x \<sharp> xs \<or> x = y)" |
|
268 apply (induct xs) |
|
269 apply(auto simp add: fresh_def supp_Nil supp_Cons supp_at_base) |
|
270 done |
|
271 |
|
272 |
235 text {* first returns an atom list *} |
273 text {* first returns an atom list *} |
236 |
274 |
237 nominal_function |
275 nominal_function |
238 frees_lst :: "lam \<Rightarrow> atom list" |
276 frees_lst :: "lam \<Rightarrow> atom list" |
239 where |
277 where |