3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 nominal_datatype trm = |
7 nominal_datatype trm = |
8 Var "name" |
8 Vr "name" |
9 | App "trm" "trm" |
9 | Ap "trm" "trm" |
10 | Lam x::"name" t::"trm" binds x in t |
10 | Lm x::"name" t::"trm" binds (set) x in t |
11 | Let as::"assn" t::"trm" binds "bn as" in t |
11 | Lt a::"lts" t::"trm" binds "bn a" in a t |
12 | Let_rec as::"assn" t::"trm" binds "bn as" in as t |
12 and lts = |
13 and assn = |
13 Lnil |
14 ANil |
14 | Lcons "name" "trm" "lts" |
15 | ACons "name" "trm" "assn" |
|
16 binder |
15 binder |
17 bn |
16 bn |
18 where |
17 where |
19 "bn (ANil) = []" |
18 "bn Lnil = []" |
20 | "bn (ACons x t as) = (atom x) # (bn as)" |
19 | "bn (Lcons x t l) = (atom x) # (bn l)" |
21 |
|
22 thm trm_assn.eq_iff |
|
23 thm trm_assn.supp |
|
24 |
|
25 ML {* |
|
26 @{term Trueprop} ; |
|
27 @{const_name HOL.eq} |
|
28 *} |
|
29 |
|
30 thm trm_assn.fv_defs |
|
31 thm trm_assn.eq_iff |
|
32 thm trm_assn.bn_defs |
|
33 thm trm_assn.perm_simps |
|
34 thm trm_assn.induct |
|
35 thm trm_assn.distinct |
|
36 |
20 |
37 |
21 |
38 |
22 thm trm_lts.fv_defs |
39 section {* Tests *} |
23 thm trm_lts.eq_iff |
|
24 thm trm_lts.bn_defs |
|
25 thm trm_lts.perm_simps |
|
26 thm trm_lts.induct |
|
27 thm trm_lts.distinct |
40 |
28 |
41 |
29 |
42 (* why is this not in HOL simpset? *) |
|
43 (* |
|
44 lemma set_sub: "{a, b} - {b} = {a} - {b}" |
|
45 by auto |
|
46 |
|
47 lemma lets_bla: |
|
48 "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))" |
|
49 apply (auto simp add: trm_lts.eq_iff alphas set_sub supp_at_base) |
|
50 done |
|
51 |
|
52 lemma lets_ok: |
|
53 "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))" |
|
54 apply (simp add: trm_lts.eq_iff) |
|
55 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
56 apply (simp_all add: alphas fresh_star_def eqvts supp_at_base) |
|
57 done |
|
58 |
|
59 lemma lets_ok3: |
|
60 "x \<noteq> y \<Longrightarrow> |
|
61 (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
|
62 (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))" |
|
63 apply (simp add: alphas trm_lts.eq_iff) |
|
64 done |
|
65 |
|
66 |
|
67 lemma lets_not_ok1: |
|
68 "x \<noteq> y \<Longrightarrow> |
|
69 (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
|
70 (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))" |
|
71 apply (simp add: alphas trm_lts.eq_iff) |
|
72 done |
|
73 |
|
74 lemma lets_nok: |
|
75 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
|
76 (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
|
77 (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))" |
|
78 apply (simp add: alphas trm_lts.eq_iff fresh_star_def) |
|
79 done |
|
80 |
|
81 lemma lets_ok4: |
|
82 "(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) = |
|
83 (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr y) (Vr x)))" |
|
84 apply (simp add: alphas trm_lts.eq_iff supp_at_base) |
|
85 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
86 apply (simp add: atom_eqvt fresh_star_def) |
|
87 done |
|
88 *) |
|
89 end |
30 end |
90 |
31 |
91 |
32 |
92 |
33 |