30 nominal_primrec |
30 nominal_primrec |
31 subst_name_list :: "name \<Rightarrow> (name \<times> name) list \<Rightarrow> name" |
31 subst_name_list :: "name \<Rightarrow> (name \<times> name) list \<Rightarrow> name" |
32 where |
32 where |
33 "subst_name_list a [] = a" |
33 "subst_name_list a [] = a" |
34 | "subst_name_list a ((b, c)#xs) = (if (a = b) then c else (subst_name_list a xs))" |
34 | "subst_name_list a ((b, c)#xs) = (if (a = b) then c else (subst_name_list a xs))" |
|
35 apply(simp add: eqvt_def subst_name_list_graph_aux_def) |
|
36 apply(simp) |
35 apply(auto) |
37 apply(auto) |
36 apply(subgoal_tac "\<And>p x r. subst_name_list_graph x r \<Longrightarrow> subst_name_list_graph (p \<bullet> x) (p \<bullet> r)") |
|
37 unfolding eqvt_def |
|
38 apply(simp only: permute_fun_def) |
|
39 apply(rule allI) |
|
40 apply(rule ext) |
|
41 apply(rule ext) |
|
42 apply(simp only: permute_bool_def) |
|
43 apply(rule iffI) |
|
44 apply(drule_tac x="p" in meta_spec) |
|
45 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
|
46 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
|
47 apply(simp) |
|
48 apply(drule_tac x="-p" in meta_spec) |
|
49 apply(drule_tac x="x" in meta_spec) |
|
50 apply(drule_tac x="xa" in meta_spec) |
|
51 apply(simp) |
|
52 apply(erule subst_name_list_graph.induct) |
|
53 apply(perm_simp) |
|
54 apply(rule subst_name_list_graph.intros) |
|
55 apply(perm_simp) |
|
56 apply(rule subst_name_list_graph.intros) |
|
57 apply(simp) |
|
58 apply(rule_tac y="b" in list.exhaust) |
38 apply(rule_tac y="b" in list.exhaust) |
59 by(auto) |
39 by(auto) |
60 |
40 |
61 termination (eqvt) |
41 termination (eqvt) |
62 by (lexicographic_order) |
42 by (lexicographic_order) |
179 | "(\<oplus>\<onesuperior>{xg})[x::=\<onesuperior>y] = \<oplus>\<onesuperior>{(xg[x::=\<onesuperior>\<twosuperior>y])}" |
159 | "(\<oplus>\<onesuperior>{xg})[x::=\<onesuperior>y] = \<oplus>\<onesuperior>{(xg[x::=\<onesuperior>\<twosuperior>y])}" |
180 | "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (\<infinity>a?<b>\<onesuperior>.P)[x::=\<onesuperior>y] = \<infinity>(a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])" |
160 | "\<lbrakk>atom b \<sharp> (x, y)\<rbrakk> \<Longrightarrow> (\<infinity>a?<b>\<onesuperior>.P)[x::=\<onesuperior>y] = \<infinity>(a[x:::=y])?<b>\<onesuperior>.(P[x::=\<onesuperior>y])" |
181 | "(succ\<onesuperior>)[x::=\<onesuperior>y] = succ\<onesuperior>" |
161 | "(succ\<onesuperior>)[x::=\<onesuperior>y] = succ\<onesuperior>" |
182 using [[simproc del: alpha_lst]] |
162 using [[simproc del: alpha_lst]] |
183 apply(auto simp add: piMix_distinct piMix_eq_iff) |
163 apply(auto simp add: piMix_distinct piMix_eq_iff) |
184 apply(subgoal_tac "\<And>p x r. subsGuard_mix_subsList_mix_subs_mix_graph x r \<Longrightarrow> subsGuard_mix_subsList_mix_subs_mix_graph (p \<bullet> x) (p \<bullet> r)") |
164 apply(simp add: eqvt_def subsGuard_mix_subsList_mix_subs_mix_graph_aux_def) |
185 unfolding eqvt_def |
|
186 apply(rule allI) |
|
187 apply(simp only: permute_fun_def) |
|
188 apply(rule ext) |
|
189 apply(rule ext) |
|
190 apply(simp only: permute_bool_def) |
|
191 apply(rule iffI) |
|
192 apply(drule_tac x="p" in meta_spec) |
|
193 apply(drule_tac x="- p \<bullet> x" in meta_spec) |
|
194 apply(drule_tac x="- p \<bullet> xa" in meta_spec) |
|
195 apply(simp) |
|
196 apply(drule_tac x="-p" in meta_spec) |
|
197 apply(drule_tac x="x" in meta_spec) |
|
198 apply(drule_tac x="xa" in meta_spec) |
|
199 apply(simp) |
|
200 --"Equivariance" |
|
201 apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.induct) |
|
202 apply(simp (no_asm_use) only: eqvts) |
|
203 apply(subst testrr) |
|
204 apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases) |
|
205 apply(blast)+ |
|
206 apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros) |
|
207 apply(simp) |
|
208 apply(simp (no_asm_use) only: eqvts) |
|
209 apply(subst testrr) |
|
210 apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases) |
|
211 apply(blast)+ |
|
212 apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros) |
|
213 apply(simp only: atom_eqvt[symmetric] Pair_eqvt[symmetric] fresh_eqvt[symmetric] permute_bool_def) |
|
214 apply(simp) |
|
215 apply(simp (no_asm_use) only: eqvts) |
|
216 apply(subst testrr) |
|
217 apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases) |
|
218 apply(blast)+ |
|
219 apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros) |
|
220 apply(simp) |
|
221 apply(simp (no_asm_use) only: eqvts) |
|
222 apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros) |
|
223 apply(simp (no_asm_use) only: eqvts) |
|
224 apply(subst testl) |
|
225 apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases) |
|
226 apply(blast)+ |
|
227 apply(subst testlr) |
|
228 apply(rotate_tac 2) |
|
229 apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases) |
|
230 apply(blast)+ |
|
231 apply(perm_simp) |
|
232 apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros) |
|
233 apply(blast) |
|
234 apply(blast) |
|
235 apply(simp (no_asm_use) only: eqvts) |
|
236 apply(subst testrr) |
|
237 apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases) |
|
238 apply(blast)+ |
|
239 apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros) |
|
240 apply(simp only: atom_eqvt[symmetric] Pair_eqvt[symmetric] fresh_eqvt[symmetric] permute_bool_def) |
|
241 apply(simp) |
|
242 apply(simp (no_asm_use) only: eqvts) |
|
243 apply(subst testrr) |
|
244 apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases) |
|
245 apply(blast)+ |
|
246 apply(subst testrr) |
|
247 apply(rotate_tac 2) |
|
248 apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases) |
|
249 apply(blast)+ |
|
250 apply(perm_simp) |
|
251 apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros) |
|
252 apply(blast) |
|
253 apply(blast) |
|
254 apply(simp (no_asm_use) only: eqvts) |
|
255 apply(subst testrr) |
|
256 apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases) |
|
257 apply(blast)+ |
|
258 apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros) |
|
259 apply(blast) |
|
260 apply(simp (no_asm_use) only: eqvts) |
|
261 apply(subst testlr) |
|
262 apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases) |
|
263 apply(blast)+ |
|
264 apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros) |
|
265 apply(blast) |
|
266 apply(simp (no_asm_use) only: eqvts) |
|
267 apply(subst testrr) |
|
268 apply(erule subsGuard_mix_subsList_mix_subs_mix_graph.cases) |
|
269 apply(blast)+ |
|
270 apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros) |
|
271 apply(simp only: atom_eqvt[symmetric] Pair_eqvt[symmetric] fresh_eqvt[symmetric] permute_bool_def) |
|
272 apply(blast) |
|
273 apply(perm_simp) |
|
274 apply(rule subsGuard_mix_subsList_mix_subs_mix_graph.intros) |
|
275 --"Covered all cases" |
165 --"Covered all cases" |
276 apply(case_tac x) |
166 apply(case_tac x) |
277 apply(simp) |
167 apply(simp) |
278 apply(case_tac a) |
168 apply(case_tac a) |
279 apply(simp) |
169 apply(simp) |
396 apply(simp add: finite_supp) |
286 apply(simp add: finite_supp) |
397 apply(simp) |
287 apply(simp) |
398 apply(simp add: eqvt_at_def) |
288 apply(simp add: eqvt_at_def) |
399 apply(drule_tac x="(b \<leftrightarrow> ba)" in spec) |
289 apply(drule_tac x="(b \<leftrightarrow> ba)" in spec) |
400 apply(simp) |
290 apply(simp) |
|
291 apply (simp only: meta_eq_to_obj_eq[OF subs_mix_def, symmetric, unfolded fun_eq_iff]) |
|
292 apply(rename_tac b P ba xa ya Pa) |
|
293 apply (subgoal_tac "eqvt_at (\<lambda>(a, b, c). subs_mix a b c) (P, xa, ya)") |
|
294 apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (P, xa, ya)))") |
|
295 apply (thin_tac "eqvt_at subsGuard_mix_subsList_mix_subs_mix_sumC (Inr (Inr (Pa, xa, ya)))") |
|
296 prefer 2 |
|
297 apply (simp only: eqvt_at_def subs_mix_def) |
|
298 apply rule |
|
299 apply(simp (no_asm)) |
|
300 apply (subst testrr) |
|
301 apply (simp add: subsGuard_mix_subsList_mix_subs_mix_sumC_def) |
|
302 apply (simp add: THE_default_def) |
|
303 apply (case_tac "Ex1 (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya))))") |
|
304 apply simp_all[2] |
|
305 apply auto[1] |
|
306 apply (erule_tac x="x" in allE) |
|
307 apply simp |
|
308 apply (thin_tac "\<forall>p\<Colon>perm. |
|
309 p \<bullet> The (subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (P, xa, ya)))) = |
|
310 (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
311 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x |
|
312 then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
313 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> P, p \<bullet> xa, p \<bullet> ya))) x |
|
314 else Inr (Inr undefined))") |
|
315 apply (thin_tac "\<forall>p\<Colon>perm. |
|
316 p \<bullet> (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
317 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x |
|
318 then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
319 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (Pa, xa, ya))) x |
|
320 else Inr (Inr undefined)) = |
|
321 (if \<exists>!x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
322 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x |
|
323 then THE x\<Colon>guardedTerm_mix + sumList_mix + piMix. |
|
324 subsGuard_mix_subsList_mix_subs_mix_graph (Inr (Inr (p \<bullet> Pa, p \<bullet> xa, p \<bullet> ya))) x |
|
325 else Inr (Inr undefined))") |
|
326 apply (thin_tac "atom b \<sharp> (xa, ya)") |
|
327 apply (thin_tac "atom ba \<sharp> (xa, ya)") |
|
328 apply (thin_tac "[[atom b]]lst. P = [[atom ba]]lst. Pa") |
|
329 apply(cases rule: subsGuard_mix_subsList_mix_subs_mix_graph.cases) |
|
330 apply assumption |
|
331 apply (metis Inr_not_Inl) |
|
332 apply (metis Inr_not_Inl) |
|
333 apply (metis Inr_not_Inl) |
|
334 apply (metis Inr_inject Inr_not_Inl) |
|
335 apply (metis Inr_inject Inr_not_Inl) |
|
336 apply (rule_tac x="<\<nu>a>\<onesuperior>Sum_Type.Projr |
|
337 (Sum_Type.Projr |
|
338 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI) |
|
339 apply clarify |
|
340 apply (rule the1_equality) |
|
341 apply blast apply assumption |
|
342 apply (rule_tac x="Sum_Type.Projr |
|
343 (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y))))) \<parallel>\<onesuperior> |
|
344 Sum_Type.Projr |
|
345 (Sum_Type.Projr (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Q, xb, y)))))" in exI) |
|
346 apply clarify |
|
347 apply (rule the1_equality) |
|
348 apply blast apply assumption |
|
349 apply (rule_tac x="[(a[xb:::=y])\<frown>\<onesuperior>(bb[xb:::=y])]Sum_Type.Projr |
|
350 (Sum_Type.Projr |
|
351 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inr (Pb, xb, y)))))" in exI) |
|
352 apply clarify |
|
353 apply (rule the1_equality) |
|
354 apply blast apply assumption |
|
355 apply (rule_tac x="\<oplus>\<onesuperior>{Sum_Type.Projl |
|
356 (Sum_Type.Projr |
|
357 (subsGuard_mix_subsList_mix_subs_mix_sum (Inr (Inl (xg, xb, y)))))}" in exI) |
|
358 apply clarify |
|
359 apply (rule the1_equality) |
|
360 apply blast apply assumption |
|
361 apply (rule_tac x="\<infinity>(a[xb:::=y])?<bb>\<onesuperior>.Sum_Type.Projr |
|
362 (Sum_Type.Projr |
|
363 (subsGuard_mix_subsList_mix_subs_mix_sum |
|
364 (Inr (Inr (Pb, xb, y)))))" in exI) |
|
365 apply clarify |
|
366 apply (rule the1_equality) |
|
367 apply blast apply assumption |
|
368 apply (rule_tac x="succ\<onesuperior>" in exI) |
|
369 apply clarify |
|
370 apply (rule the1_equality) |
|
371 apply blast apply assumption |
|
372 apply simp |
|
373 (* Here the only real goal compatibility is left *) |
|
374 apply (erule Abs_lst1_fcb) |
|
375 apply (simp_all add: Abs_fresh_iff fresh_fun_eqvt_app) |
|
376 apply (subgoal_tac "atom ba \<sharp> (\<lambda>(a, x, y). subs_mix a x y) (P, xa, ya)") |
|
377 apply simp |
|
378 apply (erule fresh_eqvt_at) |
|
379 apply(simp add: finite_supp) |
|
380 apply(simp) |
|
381 apply(simp add: eqvt_at_def) |
|
382 apply(drule_tac x="(b \<leftrightarrow> ba)" in spec) |
|
383 apply(simp) |
401 done |
384 done |
402 |
385 |
403 termination (eqvt) |
386 termination (eqvt) |
404 by (lexicographic_order) |
387 by (lexicographic_order) |
405 |
388 |