|
1 theory ExLet |
|
2 imports "../Parser" "../../Attic/Prove" |
|
3 begin |
|
4 |
|
5 text {* example 3 or example 5 from Terms.thy *} |
|
6 |
|
7 atom_decl name |
|
8 |
|
9 ML {* val _ = recursive := false *} |
|
10 ML {* val _ = alpha_type := AlphaLst *} |
|
11 nominal_datatype trm = |
|
12 Vr "name" |
|
13 | Ap "trm" "trm" |
|
14 | Lm x::"name" t::"trm" bind x in t |
|
15 | 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*) |
|
17 and lts = |
|
18 Lnil |
|
19 | Lcons "name" "trm" "lts" |
|
20 binder |
|
21 bn |
|
22 where |
|
23 "bn Lnil = []" |
|
24 | "bn (Lcons x t l) = (atom x) # (bn l)" |
|
25 |
|
26 |
|
27 thm alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros |
|
28 |
|
29 thm trm_lts.fv |
|
30 thm trm_lts.eq_iff |
|
31 thm trm_lts.bn |
|
32 thm trm_lts.perm |
|
33 thm trm_lts.induct[no_vars] |
|
34 thm trm_lts.inducts[no_vars] |
|
35 thm trm_lts.distinct |
|
36 (*thm trm_lts.supp*) |
|
37 thm trm_lts.fv[simplified trm_lts.supp(1-2)] |
|
38 |
|
39 |
|
40 primrec |
|
41 permute_bn_raw |
|
42 where |
|
43 "permute_bn_raw pi (Lnil_raw) = Lnil_raw" |
|
44 | "permute_bn_raw pi (Lcons_raw a t l) = Lcons_raw (pi \<bullet> a) t (permute_bn_raw pi l)" |
|
45 |
|
46 quotient_definition |
|
47 "permute_bn :: perm \<Rightarrow> lts \<Rightarrow> lts" |
|
48 is |
|
49 "permute_bn_raw" |
|
50 |
|
51 lemma [quot_respect]: "((op =) ===> alpha_lts_raw ===> alpha_lts_raw) permute_bn_raw permute_bn_raw" |
|
52 apply simp |
|
53 apply clarify |
|
54 apply (erule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.inducts) |
|
55 apply simp_all |
|
56 apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros) |
|
57 apply simp |
|
58 apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros) |
|
59 apply simp |
|
60 done |
|
61 |
|
62 lemmas permute_bn = permute_bn_raw.simps[quot_lifted] |
|
63 |
|
64 lemma permute_bn_zero: |
|
65 "permute_bn 0 a = a" |
|
66 apply(induct a rule: trm_lts.inducts(2)) |
|
67 apply(rule TrueI) |
|
68 apply(simp_all add:permute_bn eqvts) |
|
69 done |
|
70 |
|
71 lemma permute_bn_add: |
|
72 "permute_bn (p + q) a = permute_bn p (permute_bn q a)" |
|
73 oops |
|
74 |
|
75 lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)" |
|
76 apply(induct lts rule: trm_lts.inducts(2)) |
|
77 apply(rule TrueI) |
|
78 apply(simp_all add:permute_bn eqvts trm_lts.eq_iff) |
|
79 done |
|
80 |
|
81 lemma perm_bn: |
|
82 "p \<bullet> bn l = bn(permute_bn p l)" |
|
83 apply(induct l rule: trm_lts.inducts(2)) |
|
84 apply(rule TrueI) |
|
85 apply(simp_all add:permute_bn eqvts) |
|
86 done |
|
87 |
|
88 lemma fv_perm_bn: |
|
89 "fv_bn l = fv_bn (permute_bn p l)" |
|
90 apply(induct l rule: trm_lts.inducts(2)) |
|
91 apply(rule TrueI) |
|
92 apply(simp_all add:permute_bn eqvts) |
|
93 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 |
|
102 lemma Lt_subst: |
|
103 "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) |
|
105 apply (rule_tac x="q" in exI) |
|
106 apply (simp add: alphas) |
|
107 apply (simp add: permute_bn_alpha_bn) |
|
108 apply (simp add: perm_bn[symmetric]) |
|
109 apply (simp add: eqvts[symmetric]) |
|
110 apply (simp add: supp_abs) |
|
111 apply (simp add: trm_lts.supp) |
|
112 apply (rule supp_perm_eq[symmetric]) |
|
113 apply (subst supp_finite_atom_set) |
|
114 apply (rule finite_Diff) |
|
115 apply (simp add: finite_supp) |
|
116 apply (assumption) |
|
117 done |
|
118 |
|
119 |
|
120 lemma fin_bn: |
|
121 "finite (set (bn l))" |
|
122 apply(induct l rule: trm_lts.inducts(2)) |
|
123 apply(simp_all add:permute_bn eqvts) |
|
124 done |
|
125 |
|
126 thm trm_lts.inducts[no_vars] |
|
127 |
|
128 lemma |
|
129 fixes t::trm |
|
130 and l::lts |
|
131 and c::"'a::fs" |
|
132 assumes a1: "\<And>name c. P1 c (Vr name)" |
|
133 and a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)" |
|
134 and a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)" |
|
135 and a4: "\<And>lts trm c. \<lbrakk>set (bn lts) \<sharp>* c; \<And>d. P2 d lts; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lt lts trm)" |
|
136 and a5: "\<And>c. P2 c Lnil" |
|
137 and a6: "\<And>name trm lts c. \<lbrakk>\<And>d. P1 d trm; \<And>d. P2 d lts\<rbrakk> \<Longrightarrow> P2 c (Lcons name trm lts)" |
|
138 shows "P1 c t" and "P2 c l" |
|
139 proof - |
|
140 have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and |
|
141 b': "(\<And>(p::perm) (q::perm) (c::'a::fs). P2 c (permute_bn p (q \<bullet> l)))" |
|
142 apply(induct rule: trm_lts.inducts) |
|
143 apply(simp) |
|
144 apply(rule a1) |
|
145 apply(simp) |
|
146 apply(rule a2) |
|
147 apply(simp) |
|
148 apply(simp) |
|
149 apply(simp) |
|
150 apply(subgoal_tac "\<exists>q. (q \<bullet> (atom (p \<bullet> name))) \<sharp> c \<and> supp (Lm (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q") |
|
151 apply(erule exE) |
|
152 apply(rule_tac t="Lm (p \<bullet> name) (p \<bullet> trm)" |
|
153 and s="q\<bullet> Lm (p \<bullet> name) (p \<bullet> trm)" in subst) |
|
154 apply(rule supp_perm_eq) |
|
155 apply(simp) |
|
156 apply(simp) |
|
157 apply(rule a3) |
|
158 apply(simp add: atom_eqvt) |
|
159 apply(subst permute_plus[symmetric]) |
|
160 apply(blast) |
|
161 apply(rule at_set_avoiding2_atom) |
|
162 apply(simp add: finite_supp) |
|
163 apply(simp add: finite_supp) |
|
164 apply(simp add: fresh_def) |
|
165 apply(simp add: trm_lts.fv[simplified trm_lts.supp]) |
|
166 apply(simp) |
|
167 apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> lts))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> lts)) (p \<bullet> trm)) \<sharp>* q") |
|
168 apply(erule exE) |
|
169 apply(erule conjE) |
|
170 apply(subst Lt_subst) |
|
171 apply assumption |
|
172 apply(rule a4) |
|
173 apply(simp add:perm_bn[symmetric]) |
|
174 apply(simp add: eqvts) |
|
175 apply (simp add: fresh_star_def fresh_def) |
|
176 apply(rotate_tac 1) |
|
177 apply(drule_tac x="q + p" in meta_spec) |
|
178 apply(simp) |
|
179 apply(rule at_set_avoiding2) |
|
180 apply(rule fin_bn) |
|
181 apply(simp add: finite_supp) |
|
182 apply(simp add: finite_supp) |
|
183 apply(simp add: fresh_star_def fresh_def supp_abs) |
|
184 apply(simp add: eqvts permute_bn) |
|
185 apply(rule a5) |
|
186 apply(simp add: permute_bn) |
|
187 apply(rule a6) |
|
188 apply simp |
|
189 apply simp |
|
190 done |
|
191 then have a: "P1 c (0 \<bullet> t)" by blast |
|
192 have "P2 c (permute_bn 0 (0 \<bullet> l))" using b' by blast |
|
193 then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all |
|
194 qed |
|
195 |
|
196 |
|
197 |
|
198 lemma lets_bla: |
|
199 "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))" |
|
200 by (simp add: trm_lts.eq_iff) |
|
201 |
|
202 lemma lets_ok: |
|
203 "(Lt (Lcons x (Vr y) Lnil) (Vr x)) = (Lt (Lcons y (Vr y) Lnil) (Vr y))" |
|
204 apply (simp add: trm_lts.eq_iff) |
|
205 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
|
206 apply (simp_all add: alphas) |
|
207 apply (simp add: fresh_star_def eqvts) |
|
208 done |
|
209 |
|
210 lemma lets_ok3: |
|
211 "x \<noteq> y \<Longrightarrow> |
|
212 (Lt (Lcons x (Ap (Vr y) (Vr x)) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
|
213 (Lt (Lcons y (Ap (Vr x) (Vr y)) (Lcons x (Vr x) Lnil)) (Ap (Vr x) (Vr y)))" |
|
214 apply (simp add: alphas trm_lts.eq_iff) |
|
215 done |
|
216 |
|
217 |
|
218 lemma lets_not_ok1: |
|
219 "x \<noteq> y \<Longrightarrow> |
|
220 (Lt (Lcons x (Vr x) (Lcons y (Vr y) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
|
221 (Lt (Lcons y (Vr x) (Lcons x (Vr y) Lnil)) (Ap (Vr x) (Vr y)))" |
|
222 apply (simp add: alphas trm_lts.eq_iff fresh_star_def eqvts) |
|
223 done |
|
224 |
|
225 lemma lets_nok: |
|
226 "x \<noteq> y \<Longrightarrow> x \<noteq> z \<Longrightarrow> z \<noteq> y \<Longrightarrow> |
|
227 (Lt (Lcons x (Ap (Vr z) (Vr z)) (Lcons y (Vr z) Lnil)) (Ap (Vr x) (Vr y))) \<noteq> |
|
228 (Lt (Lcons y (Vr z) (Lcons x (Ap (Vr z) (Vr z)) Lnil)) (Ap (Vr x) (Vr y)))" |
|
229 apply (simp add: alphas trm_lts.eq_iff fresh_star_def) |
|
230 done |
|
231 |
|
232 |
|
233 end |
|
234 |
|
235 |
|
236 |