9 ML {* val _ = recursive := false *} |
9 ML {* val _ = recursive := false *} |
10 nominal_datatype trm = |
10 nominal_datatype trm = |
11 Vr "name" |
11 Vr "name" |
12 | Ap "trm" "trm" |
12 | Ap "trm" "trm" |
13 | Lm x::"name" t::"trm" bind x in t |
13 | Lm x::"name" t::"trm" bind x in t |
14 | Lt a::"lts" t::"trm" bind "bv a" in t |
14 | Lt a::"lts" t::"trm" bind "bn a" in t |
15 and lts = |
15 and lts = |
16 Nil |
16 Lnil |
17 | Cons "name" "trm" "lts" |
17 | Lcons "name" "trm" "lts" |
18 binder |
18 binder |
19 bn |
19 bn |
20 where |
20 where |
21 "bn Nil = {}" |
21 "bn Lnil = {}" |
22 | "bn (Cons x t l) = {atom x} \<union> (bn l)" |
22 | "bn (Lcons x t l) = {atom x} \<union> (bn l)" |
23 |
23 |
24 thm trm_lts.fv |
24 thm trm_lts.fv |
25 thm trm_lts.eq_iff |
25 thm trm_lts.eq_iff |
26 thm trm_lts.bn |
26 thm trm_lts.bn |
27 thm trm_lts.perm |
27 thm trm_lts.perm |
28 thm trm_lts.induct |
28 thm trm_lts.induct |
29 thm trm_lts.distinct |
29 thm trm_lts.distinct |
30 thm trm_lts.fv[simplified trm_lts.supp] |
30 thm trm_lts.fv[simplified trm_lts.supp] |
31 |
31 |
|
32 lemma lets_bla: |
|
33 "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt (Lcons x (Vr y) Lnil) (Vr x)) \<noteq> (Lt (Lcons x (Vr z) Lnil) (Vr x))" |
|
34 by (simp add: trm_lts.eq_iff) |
|
35 |
|
36 lemma lets_ok: |
|
37 "(Lt (Lcons x (Vr y) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))" |
|
38 apply (simp add: trm_lts.eq_iff) |
|
39 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
40 apply (simp_all add: alphas) |
|
41 apply (simp add: fresh_star_def eqvts) |
|
42 done |
|
43 |
|
44 lemma lets_ok3: |
|
45 "x \<noteq> y \<Longrightarrow> |
|
46 (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
|
47 (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))" |
|
48 apply (simp add: alphas trm_lts.eq_iff) |
|
49 done |
|
50 |
|
51 |
|
52 lemma lets_not_ok1: |
|
53 "(Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) = |
|
54 (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))" |
|
55 apply (simp add: alphas trm_lts.eq_iff) |
|
56 apply (rule_tac x="0::perm" in exI) |
|
57 apply (simp add: fresh_star_def eqvts) |
|
58 apply blast |
|
59 done |
|
60 |
|
61 lemma lets_nok: |
|
62 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
|
63 (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
|
64 (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))" |
|
65 apply (simp add: alphas trm_lts.eq_iff fresh_star_def) |
|
66 done |
|
67 |
|
68 |
32 end |
69 end |
33 |
70 |
34 |
71 |
35 |
72 |