equal
deleted
inserted
replaced
1 theory ExLetRec |
1 theory ExLetRec |
2 imports "../Parser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 |
5 |
6 text {* example 3 or example 5 from Terms.thy *} |
6 text {* example 3 or example 5 from Terms.thy *} |
7 |
7 |
8 atom_decl name |
8 atom_decl name |
9 |
9 |
10 ML {* val _ = recursive := true *} |
|
11 ML {* val _ = alpha_type := AlphaLst *} |
|
12 nominal_datatype trm = |
10 nominal_datatype trm = |
13 Vr "name" |
11 Vr "name" |
14 | Ap "trm" "trm" |
12 | Ap "trm" "trm" |
15 | Lm x::"name" t::"trm" bind x in t |
13 | Lm x::"name" t::"trm" bind_set x in t |
16 | Lt a::"lts" t::"trm" bind "bn a" in t |
14 | Lt a::"lts" t::"trm" bind "bn a" in a t |
17 and lts = |
15 and lts = |
18 Lnil |
16 Lnil |
19 | Lcons "name" "trm" "lts" |
17 | Lcons "name" "trm" "lts" |
20 binder |
18 binder |
21 bn |
19 bn |
36 lemma set_sub: "{a, b} - {b} = {a} - {b}" |
34 lemma set_sub: "{a, b} - {b} = {a} - {b}" |
37 by auto |
35 by auto |
38 |
36 |
39 lemma lets_bla: |
37 lemma lets_bla: |
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 "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))" |
41 by (simp add: trm_lts.eq_iff alphas2 set_sub) |
39 by (simp add: trm_lts.eq_iff alphas2 set_sub supp_at_base) |
42 |
40 |
43 lemma lets_ok: |
41 lemma lets_ok: |
44 "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))" |
42 "(Lt (Lcons x (Vr x) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))" |
45 apply (simp add: trm_lts.eq_iff) |
43 apply (simp add: trm_lts.eq_iff) |
46 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
44 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
47 apply (simp_all add: alphas2 fresh_star_def eqvts) |
45 apply (simp_all add: alphas2 fresh_star_def eqvts supp_at_base) |
48 done |
46 done |
49 |
47 |
50 lemma lets_ok3: |
48 lemma lets_ok3: |
51 "x \<noteq> y \<Longrightarrow> |
49 "x \<noteq> y \<Longrightarrow> |
52 (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
50 (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
70 done |
68 done |
71 |
69 |
72 lemma lets_ok4: |
70 lemma lets_ok4: |
73 "(Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) = |
71 "(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)))" |
72 (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) |
73 apply (simp add: alphas trm_lts.eq_iff supp_at_base) |
76 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
74 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
77 apply (simp add: atom_eqvt fresh_star_def) |
75 apply (simp add: atom_eqvt fresh_star_def) |
78 done |
76 done |
79 |
77 |
80 end |
78 end |