1 theory ExLet |
1 theory ExLet |
2 imports "../Parser" "../../Attic/Prove" |
2 imports "../NewParser" "../../Attic/Prove" |
3 begin |
3 begin |
4 |
4 |
5 text {* example 3 or example 5 from Terms.thy *} |
5 text {* example 3 or example 5 from Terms.thy *} |
6 |
6 |
7 atom_decl name |
7 atom_decl name |
8 |
8 |
9 ML {* val _ = recursive := false *} |
|
10 ML {* val _ = alpha_type := AlphaLst *} |
|
11 nominal_datatype trm = |
9 nominal_datatype trm = |
12 Vr "name" |
10 Vr "name" |
13 | Ap "trm" "trm" |
11 | Ap "trm" "trm" |
14 | Lm x::"name" t::"trm" bind x in t |
12 | Lm x::"name" t::"trm" bind_set x in t |
15 | Lt a::"lts" t::"trm" bind "bn a" in t |
13 | Lt a::"lts" t::"trm" bind "bn a" in t |
16 (*| L a::"lts" t1::"trm" t2::"trm" bind "bn a" in t1, bind "bn a" in t2*) |
14 (*| L a::"lts" t1::"trm" t2::"trm" bind "bn a" in t1, bind "bn a" in t2*) |
17 and lts = |
15 and lts = |
18 Lnil |
16 Lnil |
19 | Lcons "name" "trm" "lts" |
17 | Lcons "name" "trm" "lts" |
50 |
48 |
51 lemma [quot_respect]: "((op =) ===> alpha_lts_raw ===> alpha_lts_raw) permute_bn_raw permute_bn_raw" |
49 lemma [quot_respect]: "((op =) ===> alpha_lts_raw ===> alpha_lts_raw) permute_bn_raw permute_bn_raw" |
52 apply simp |
50 apply simp |
53 apply clarify |
51 apply clarify |
54 apply (erule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.inducts) |
52 apply (erule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.inducts) |
|
53 apply (rule TrueI)+ |
55 apply simp_all |
54 apply simp_all |
56 apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros) |
55 apply (rule_tac [!] alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros) |
57 apply simp |
56 apply simp_all |
58 apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros) |
|
59 apply simp |
|
60 done |
57 done |
61 |
58 |
62 lemmas permute_bn = permute_bn_raw.simps[quot_lifted] |
59 lemmas permute_bn = permute_bn_raw.simps[quot_lifted] |
63 |
60 |
64 lemma permute_bn_zero: |
61 lemma permute_bn_zero: |
65 "permute_bn 0 a = a" |
62 "permute_bn 0 a = a" |
66 apply(induct a rule: trm_lts.inducts(2)) |
63 apply(induct a rule: trm_lts.inducts(2)) |
67 apply(rule TrueI) |
64 apply(rule TrueI)+ |
68 apply(simp_all add:permute_bn eqvts) |
65 apply(simp_all add:permute_bn) |
69 done |
66 done |
70 |
67 |
71 lemma permute_bn_add: |
68 lemma permute_bn_add: |
72 "permute_bn (p + q) a = permute_bn p (permute_bn q a)" |
69 "permute_bn (p + q) a = permute_bn p (permute_bn q a)" |
73 oops |
70 oops |
74 |
71 |
75 lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)" |
72 lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)" |
76 apply(induct lts rule: trm_lts.inducts(2)) |
73 apply(induct lts rule: trm_lts.inducts(2)) |
77 apply(rule TrueI) |
74 apply(rule TrueI)+ |
78 apply(simp_all add:permute_bn eqvts trm_lts.eq_iff) |
75 apply(simp_all add:permute_bn eqvts trm_lts.eq_iff) |
79 done |
76 done |
80 |
77 |
81 lemma perm_bn: |
78 lemma perm_bn: |
82 "p \<bullet> bn l = bn(permute_bn p l)" |
79 "p \<bullet> bn l = bn(permute_bn p l)" |
83 apply(induct l rule: trm_lts.inducts(2)) |
80 apply(induct l rule: trm_lts.inducts(2)) |
84 apply(rule TrueI) |
81 apply(rule TrueI)+ |
85 apply(simp_all add:permute_bn eqvts) |
82 apply(simp_all add:permute_bn eqvts) |
86 done |
83 done |
87 |
84 |
88 lemma fv_perm_bn: |
85 lemma fv_perm_bn: |
89 "fv_bn l = fv_bn (permute_bn p l)" |
86 "fv_bn l = fv_bn (permute_bn p l)" |
90 apply(induct l rule: trm_lts.inducts(2)) |
87 apply(induct l rule: trm_lts.inducts(2)) |
91 apply(rule TrueI) |
88 apply(rule TrueI)+ |
92 apply(simp_all add:permute_bn eqvts) |
89 apply(simp_all add:permute_bn eqvts) |
93 done |
90 done |
94 |
|
95 lemma fv_fv_bn: |
|
96 "fv_bn l - set (bn l) = fv_lts l - set (bn l)" |
|
97 apply(induct l rule: trm_lts.inducts(2)) |
|
98 apply(rule TrueI) |
|
99 apply(simp_all add:permute_bn eqvts) |
|
100 by blast |
|
101 |
91 |
102 lemma Lt_subst: |
92 lemma Lt_subst: |
103 "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)" |
93 "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)" |
104 apply (simp only: trm_lts.eq_iff) |
94 apply (simp add: trm_lts.eq_iff permute_bn_alpha_bn) |
105 apply (rule_tac x="q" in exI) |
95 apply (rule_tac x="q" in exI) |
106 apply (simp add: alphas) |
96 apply (simp add: alphas) |
107 apply (simp add: permute_bn_alpha_bn) |
|
108 apply (simp add: perm_bn[symmetric]) |
97 apply (simp add: perm_bn[symmetric]) |
109 apply (simp add: eqvts[symmetric]) |
98 apply (simp add: eqvts[symmetric]) |
110 apply (simp add: supp_abs) |
99 apply (simp add: supp_abs) |
111 apply (simp add: trm_lts.supp) |
100 apply (simp add: trm_lts.supp) |
112 apply (rule supp_perm_eq[symmetric]) |
101 apply (rule supp_perm_eq[symmetric]) |
202 |
191 |
203 lemma lets_ok: |
192 lemma lets_ok: |
204 "(Lt (Lcons x (Vr y) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))" |
193 "(Lt (Lcons x (Vr y) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))" |
205 apply (simp add: trm_lts.eq_iff) |
194 apply (simp add: trm_lts.eq_iff) |
206 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
195 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
207 apply (simp_all add: alphas) |
196 apply (simp_all add: alphas eqvts supp_at_base fresh_star_def) |
208 apply (simp add: fresh_star_def eqvts) |
|
209 done |
197 done |
210 |
198 |
211 lemma lets_ok3: |
199 lemma lets_ok3: |
212 "x \<noteq> y \<Longrightarrow> |
200 "x \<noteq> y \<Longrightarrow> |
213 (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
201 (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |