28 thm trm_assn.supp |
28 thm trm_assn.supp |
29 thm trm_assn.fresh |
29 thm trm_assn.fresh |
30 thm trm_assn.exhaust |
30 thm trm_assn.exhaust |
31 thm trm_assn.strong_exhaust |
31 thm trm_assn.strong_exhaust |
32 |
32 |
33 lemma |
|
34 fixes t::trm |
|
35 and as::assn |
|
36 and c::"'a::fs" |
|
37 assumes a1: "\<And>x c. P1 c (Var x)" |
|
38 and a2: "\<And>t1 t2 c. \<lbrakk>\<And>d. P1 d t1; \<And>d. P1 d t2\<rbrakk> \<Longrightarrow> P1 c (App t1 t2)" |
|
39 and a3: "\<And>x t c. \<lbrakk>{atom x} \<sharp>* c; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Lam x t)" |
|
40 and a4: "\<And>as t c. \<lbrakk>set (bn as) \<sharp>* c; \<And>d. P2 d as; \<And>d. P1 d t\<rbrakk> \<Longrightarrow> P1 c (Let as t)" |
|
41 and a5: "\<And>c. P2 c ANil" |
|
42 and a6: "\<And>x t as c. \<lbrakk>\<And>d. P1 d t; \<And>d. P2 d as\<rbrakk> \<Longrightarrow> P2 c (ACons x t as)" |
|
43 shows "P1 c t" "P2 c as" |
|
44 using assms |
|
45 apply(induction_schema) |
|
46 apply(rule_tac y="t" in trm_assn.strong_exhaust(1)) |
|
47 apply(blast) |
|
48 apply(blast) |
|
49 apply(blast) |
|
50 apply(blast) |
|
51 apply(rule_tac ya="as" in trm_assn.strong_exhaust(2)) |
|
52 apply(blast) |
|
53 apply(blast) |
|
54 apply(relation "measure (sum_case (\<lambda>y. size (snd y)) (\<lambda>z. size (snd z)))") |
|
55 apply(simp_all add: trm_assn.size) |
|
56 done |
|
57 |
|
58 text {* *} |
|
59 |
|
60 |
|
61 (* |
33 (* |
62 proof - |
|
63 have x: "\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t)" |
|
64 and y: "\<And>(p::perm) (c::'a::fs). P2 c (p \<bullet> as)" |
|
65 apply(induct rule: trm_assn.inducts) |
|
66 apply(simp) |
|
67 apply(rule a1) |
|
68 apply(simp) |
|
69 apply(rule a2) |
|
70 apply(assumption) |
|
71 apply(assumption) |
|
72 -- "lam case" |
|
73 apply(simp) |
|
74 apply(subgoal_tac "\<exists>q. (q \<bullet> {atom (p \<bullet> name)}) \<sharp>* c \<and> supp (Lam (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q") |
|
75 apply(erule exE) |
|
76 apply(erule conjE) |
|
77 apply(drule supp_perm_eq[symmetric]) |
|
78 apply(simp) |
|
79 apply(thin_tac "?X = ?Y") |
|
80 apply(rule a3) |
|
81 apply(simp add: atom_eqvt permute_set_eq) |
|
82 apply(simp only: permute_plus[symmetric]) |
|
83 apply(rule at_set_avoiding2) |
|
84 apply(simp add: finite_supp) |
|
85 apply(simp add: finite_supp) |
|
86 apply(simp add: finite_supp) |
|
87 apply(simp add: freshs fresh_star_def) |
|
88 --"let case" |
|
89 apply(simp) |
|
90 thm trm_assn.eq_iff |
|
91 thm eq_iffs |
|
92 apply(subgoal_tac "\<exists>q. (q \<bullet> set (bn (p \<bullet> assn))) \<sharp>* c \<and> supp (Abs_lst (bn (p \<bullet> assn)) (p \<bullet> trm)) \<sharp>* q") |
|
93 apply(erule exE) |
|
94 apply(erule conjE) |
|
95 prefer 2 |
|
96 apply(rule at_set_avoiding2) |
|
97 apply(rule fin_bn) |
|
98 apply(simp add: finite_supp) |
|
99 apply(simp add: finite_supp) |
|
100 apply(simp add: abs_fresh) |
|
101 apply(rule_tac t = "Let (p \<bullet> assn) (p \<bullet> trm)" in subst) |
|
102 prefer 2 |
|
103 apply(rule a4) |
|
104 prefer 4 |
|
105 apply(simp add: eq_iffs) |
|
106 apply(rule conjI) |
|
107 prefer 2 |
|
108 apply(simp add: set_eqvt trm_assn.fv_bn_eqvt) |
|
109 apply(subst permute_plus[symmetric]) |
|
110 apply(blast) |
|
111 prefer 2 |
|
112 apply(simp add: eq_iffs) |
|
113 thm eq_iffs |
|
114 apply(subst permute_plus[symmetric]) |
|
115 apply(blast) |
|
116 apply(simp add: supps) |
|
117 apply(simp add: fresh_star_def freshs) |
|
118 apply(drule supp_perm_eq[symmetric]) |
|
119 apply(simp) |
|
120 apply(simp add: eq_iffs) |
|
121 apply(simp) |
|
122 apply(thin_tac "?X = ?Y") |
|
123 apply(rule a4) |
|
124 apply(simp add: set_eqvt trm_assn.fv_bn_eqvt) |
|
125 apply(subst permute_plus[symmetric]) |
|
126 apply(blast) |
|
127 apply(subst permute_plus[symmetric]) |
|
128 apply(blast) |
|
129 apply(simp add: supps) |
|
130 thm at_set_avoiding2 |
|
131 --"HERE" |
|
132 apply(rule at_set_avoiding2) |
|
133 apply(rule fin_bn) |
|
134 apply(simp add: finite_supp) |
|
135 apply(simp add: finite_supp) |
|
136 apply(simp add: fresh_star_def freshs) |
|
137 apply(rule ballI) |
|
138 apply(simp add: eqvts permute_bn) |
|
139 apply(rule a5) |
|
140 apply(simp add: permute_bn) |
|
141 apply(rule a6) |
|
142 apply simp |
|
143 apply simp |
|
144 done |
|
145 then have a: "P1 c (0 \<bullet> t)" by blast |
|
146 have "P2 c (permute_bn 0 (0 \<bullet> l))" using b' by blast |
|
147 then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all |
|
148 qed |
|
149 *) |
|
150 |
|
151 text {* *} |
|
152 |
|
153 (* |
|
154 |
|
155 primrec |
|
156 permute_bn_raw |
|
157 where |
|
158 "permute_bn_raw pi (Lnil_raw) = Lnil_raw" |
|
159 | "permute_bn_raw pi (Lcons_raw a t l) = Lcons_raw (pi \<bullet> a) t (permute_bn_raw pi l)" |
|
160 |
|
161 quotient_definition |
|
162 "permute_bn :: perm \<Rightarrow> lts \<Rightarrow> lts" |
|
163 is |
|
164 "permute_bn_raw" |
|
165 |
|
166 lemma [quot_respect]: "((op =) ===> alpha_lts_raw ===> alpha_lts_raw) permute_bn_raw permute_bn_raw" |
|
167 apply simp |
|
168 apply clarify |
|
169 apply (erule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.inducts) |
|
170 apply (rule TrueI)+ |
|
171 apply simp_all |
|
172 apply (rule_tac [!] alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros) |
|
173 apply simp_all |
|
174 done |
|
175 |
|
176 lemmas permute_bn = permute_bn_raw.simps[quot_lifted] |
|
177 |
|
178 lemma permute_bn_zero: |
|
179 "permute_bn 0 a = a" |
|
180 apply(induct a rule: trm_lts.inducts(2)) |
|
181 apply(rule TrueI)+ |
|
182 apply(simp_all add:permute_bn) |
|
183 done |
|
184 |
|
185 lemma permute_bn_add: |
|
186 "permute_bn (p + q) a = permute_bn p (permute_bn q a)" |
|
187 oops |
|
188 |
|
189 lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)" |
|
190 apply(induct lts rule: trm_lts.inducts(2)) |
|
191 apply(rule TrueI)+ |
|
192 apply(simp_all add:permute_bn eqvts trm_lts.eq_iff) |
|
193 done |
|
194 |
|
195 lemma perm_bn: |
|
196 "p \<bullet> bn l = bn(permute_bn p l)" |
|
197 apply(induct l rule: trm_lts.inducts(2)) |
|
198 apply(rule TrueI)+ |
|
199 apply(simp_all add:permute_bn eqvts) |
|
200 done |
|
201 |
|
202 lemma fv_perm_bn: |
|
203 "fv_bn l = fv_bn (permute_bn p l)" |
|
204 apply(induct l rule: trm_lts.inducts(2)) |
|
205 apply(rule TrueI)+ |
|
206 apply(simp_all add:permute_bn eqvts) |
|
207 done |
|
208 |
|
209 lemma Lt_subst: |
|
210 "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)" |
|
211 apply (simp add: trm_lts.eq_iff permute_bn_alpha_bn) |
|
212 apply (rule_tac x="q" in exI) |
|
213 apply (simp add: alphas) |
|
214 apply (simp add: perm_bn[symmetric]) |
|
215 apply(rule conjI) |
|
216 apply(drule supp_perm_eq) |
|
217 apply(simp add: abs_eq_iff) |
|
218 apply(simp add: alphas_abs alphas) |
|
219 apply(drule conjunct1) |
|
220 apply (simp add: trm_lts.supp) |
|
221 apply(simp add: supp_abs) |
|
222 apply (simp add: trm_lts.supp) |
|
223 done |
|
224 |
|
225 |
|
226 lemma fin_bn: |
|
227 "finite (set (bn l))" |
|
228 apply(induct l rule: trm_lts.inducts(2)) |
|
229 apply(simp_all add:permute_bn eqvts) |
|
230 done |
|
231 |
|
232 thm trm_lts.inducts[no_vars] |
|
233 |
|
234 lemma |
|
235 fixes t::trm |
|
236 and l::lts |
|
237 and c::"'a::fs" |
|
238 assumes a1: "\<And>name c. P1 c (Vr name)" |
|
239 and a2: "\<And>trm1 trm2 c. \<lbrakk>\<And>d. P1 d trm1; \<And>d. P1 d trm2\<rbrakk> \<Longrightarrow> P1 c (Ap trm1 trm2)" |
|
240 and a3: "\<And>name trm c. \<lbrakk>atom name \<sharp> c; \<And>d. P1 d trm\<rbrakk> \<Longrightarrow> P1 c (Lm name trm)" |
|
241 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)" |
|
242 and a5: "\<And>c. P2 c Lnil" |
|
243 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)" |
|
244 shows "P1 c t" and "P2 c l" |
|
245 proof - |
|
246 have "(\<And>(p::perm) (c::'a::fs). P1 c (p \<bullet> t))" and |
|
247 b': "(\<And>(p::perm) (q::perm) (c::'a::fs). P2 c (permute_bn p (q \<bullet> l)))" |
|
248 apply(induct rule: trm_lts.inducts) |
|
249 apply(simp) |
|
250 apply(rule a1) |
|
251 apply(simp) |
|
252 apply(rule a2) |
|
253 apply(simp) |
|
254 apply(simp) |
|
255 apply(simp) |
|
256 apply(subgoal_tac "\<exists>q. (q \<bullet> (atom (p \<bullet> name))) \<sharp> c \<and> supp (Lm (p \<bullet> name) (p \<bullet> trm)) \<sharp>* q") |
|
257 apply(erule exE) |
|
258 apply(rule_tac t="Lm (p \<bullet> name) (p \<bullet> trm)" |
|
259 and s="q\<bullet> Lm (p \<bullet> name) (p \<bullet> trm)" in subst) |
|
260 apply(rule supp_perm_eq) |
|
261 apply(simp) |
|
262 apply(simp) |
|
263 apply(rule a3) |
|
264 apply(simp add: atom_eqvt) |
|
265 apply(subst permute_plus[symmetric]) |
|
266 apply(blast) |
|
267 apply(rule at_set_avoiding2_atom) |
|
268 apply(simp add: finite_supp) |
|
269 apply(simp add: finite_supp) |
|
270 apply(simp add: fresh_def) |
|
271 apply(simp add: trm_lts.fv[simplified trm_lts.supp]) |
|
272 apply(simp) |
|
273 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") |
|
274 apply(erule exE) |
|
275 apply(erule conjE) |
|
276 thm Lt_subst |
|
277 apply(subst Lt_subst) |
|
278 apply assumption |
|
279 apply(rule a4) |
|
280 apply(simp add:perm_bn[symmetric]) |
|
281 apply(simp add: eqvts) |
|
282 apply (simp add: fresh_star_def fresh_def) |
|
283 apply(rotate_tac 1) |
|
284 apply(drule_tac x="q + p" in meta_spec) |
|
285 apply(simp) |
|
286 apply(rule at_set_avoiding2) |
|
287 apply(rule fin_bn) |
|
288 apply(simp add: finite_supp) |
|
289 apply(simp add: finite_supp) |
|
290 apply(simp add: fresh_star_def fresh_def supp_abs) |
|
291 apply(simp add: eqvts permute_bn) |
|
292 apply(rule a5) |
|
293 apply(simp add: permute_bn) |
|
294 apply(rule a6) |
|
295 apply simp |
|
296 apply simp |
|
297 done |
|
298 then have a: "P1 c (0 \<bullet> t)" by blast |
|
299 have "P2 c (permute_bn 0 (0 \<bullet> l))" using b' by blast |
|
300 then show "P1 c t" and "P2 c l" using a permute_bn_zero by simp_all |
|
301 qed |
|
302 |
|
303 |
|
304 |
|
305 lemma lets_bla: |
34 lemma lets_bla: |
306 "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))" |
35 "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))" |
307 by (simp add: trm_lts.eq_iff) |
36 by (simp add: trm_lts.eq_iff) |
308 |
37 |
309 lemma lets_ok: |
38 lemma lets_ok: |