1 theory ExLetRec |
1 theory ExLetRec |
2 imports "Parser" |
2 imports "Parser" |
3 begin |
3 begin |
|
4 |
4 |
5 |
5 text {* example 3 or example 5 from Terms.thy *} |
6 text {* example 3 or example 5 from Terms.thy *} |
6 |
7 |
7 atom_decl name |
8 atom_decl name |
8 |
9 |
9 ML {* val _ = recursive := true *} |
10 ML {* val _ = recursive := true *} |
|
11 ML {* val _ = alpha_type := AlphaLst *} |
10 nominal_datatype trm = |
12 nominal_datatype trm = |
11 Vr "name" |
13 Vr "name" |
12 | Ap "trm" "trm" |
14 | Ap "trm" "trm" |
13 | Lm x::"name" t::"trm" bind x in t |
15 | Lm x::"name" t::"trm" bind x in t |
14 | Lt a::"lts" t::"trm" bind "bn a" in t |
16 | Lt a::"lts" t::"trm" bind "bn a" in t |
16 Lnil |
18 Lnil |
17 | Lcons "name" "trm" "lts" |
19 | Lcons "name" "trm" "lts" |
18 binder |
20 binder |
19 bn |
21 bn |
20 where |
22 where |
21 "bn Lnil = {}" |
23 "bn Lnil = []" |
22 | "bn (Lcons x t l) = {atom x} \<union> (bn l)" |
24 | "bn (Lcons x t l) = (atom x) # (bn l)" |
23 |
25 |
24 thm trm_lts.fv |
26 thm trm_lts.fv |
25 thm trm_lts.eq_iff |
27 thm trm_lts.eq_iff |
26 thm trm_lts.bn |
28 thm trm_lts.bn |
27 thm trm_lts.perm |
29 thm trm_lts.perm |
28 thm trm_lts.induct |
30 thm trm_lts.induct |
29 thm trm_lts.distinct |
31 thm trm_lts.distinct |
|
32 thm trm_lts.supp |
30 thm trm_lts.fv[simplified trm_lts.supp] |
33 thm trm_lts.fv[simplified trm_lts.supp] |
31 |
34 |
32 (* why is this not in HOL simpset? *) |
35 (* why is this not in HOL simpset? *) |
33 lemma set_sub: "{a, b} - {b} = {a} - {b}" |
36 lemma set_sub: "{a, b} - {b} = {a} - {b}" |
34 by auto |
37 by auto |
35 |
38 |
36 lemma lets_bla: |
39 lemma lets_bla: |
37 "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))" |
40 "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))" |
38 apply (simp add: trm_lts.eq_iff alpha_gen2 set_sub) |
41 by (simp add: trm_lts.eq_iff alphas2 set_sub) |
39 done |
|
40 |
42 |
41 lemma lets_ok: |
43 lemma lets_ok: |
42 "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))" |
44 "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))" |
43 apply (simp add: trm_lts.eq_iff) |
45 apply (simp add: trm_lts.eq_iff) |
44 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
46 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
45 apply (simp_all add: alpha_gen2 fresh_star_def eqvts) |
47 apply (simp_all add: alphas2 fresh_star_def eqvts) |
46 done |
48 done |
47 |
49 |
48 lemma lets_ok3: |
50 lemma lets_ok3: |
49 "x \<noteq> y \<Longrightarrow> |
51 "x \<noteq> y \<Longrightarrow> |
50 (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
52 (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
65 (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
67 (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
66 (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))" |
68 (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))" |
67 apply (simp add: alphas trm_lts.eq_iff fresh_star_def) |
69 apply (simp add: alphas trm_lts.eq_iff fresh_star_def) |
68 done |
70 done |
69 |
71 |
|
72 lemma lets_ok4: |
|
73 "(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) = |
|
74 (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr y) (Vr x)))" |
|
75 apply (simp add: alphas trm_lts.eq_iff) |
|
76 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
77 apply (simp add: atom_eqvt fresh_star_def) |
|
78 done |
70 |
79 |
71 end |
80 end |
72 |
81 |
73 |
82 |
74 |
83 |