312 apply(perm_simp) |
312 apply(perm_simp) |
313 using assms |
313 using assms |
314 apply(simp) |
314 apply(simp) |
315 done |
315 done |
316 |
316 |
|
317 lemma abs_rename_set1: |
|
318 fixes x::"'a::fs" |
|
319 assumes "(p \<bullet> b) \<sharp> x" |
|
320 shows "\<exists>y. [{b}]set. x = [{p \<bullet> b}]set. y" |
|
321 apply(rule_tac x="(b \<rightleftharpoons> (p \<bullet> b)) \<bullet> x" in exI) |
|
322 apply(subst Abs_swap1[where a="b" and b="p \<bullet> b"]) |
|
323 apply(simp) |
|
324 using assms |
|
325 apply(simp add: fresh_def) |
|
326 apply(perm_simp) |
|
327 apply(simp) |
|
328 done |
|
329 |
|
330 lemma yy: |
|
331 assumes "finite bs" |
|
332 and "bs \<inter> p \<bullet> bs = {}" |
|
333 shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> bs \<union> (p \<bullet> bs)" |
|
334 using assms |
|
335 apply(induct) |
|
336 apply(simp add: permute_set_eq) |
|
337 apply(rule_tac x="0" in exI) |
|
338 apply(simp add: supp_perm) |
|
339 apply(perm_simp) |
|
340 apply(drule meta_mp) |
|
341 apply(auto)[1] |
|
342 apply(erule exE) |
|
343 apply(simp) |
|
344 apply(case_tac "q \<bullet> x = p \<bullet> x") |
|
345 apply(rule_tac x="q" in exI) |
|
346 apply(auto)[1] |
|
347 apply(rule_tac x="((q \<bullet> x) \<rightleftharpoons> (p \<bullet> x)) + q" in exI) |
|
348 apply(subgoal_tac "p \<bullet> x \<notin> p \<bullet> F") |
|
349 apply(subgoal_tac "q \<bullet> x \<notin> p \<bullet> F") |
|
350 apply(simp add: swap_set_not_in) |
|
351 apply(rule subset_trans) |
|
352 apply(rule supp_plus_perm) |
|
353 apply(simp) |
|
354 apply(rule conjI) |
|
355 apply(simp add: supp_swap) |
|
356 defer |
|
357 apply(auto)[1] |
|
358 apply(erule conjE)+ |
|
359 apply(drule sym) |
|
360 apply(auto)[1] |
|
361 apply(simp add: mem_permute_iff) |
|
362 apply(simp add: mem_permute_iff) |
|
363 apply(auto)[1] |
|
364 apply(simp add: supp_perm) |
|
365 apply(auto)[1] |
|
366 done |
|
367 |
|
368 lemma zz: |
|
369 fixes bs::"atom list" |
|
370 assumes "set bs \<inter> (set (p \<bullet> bs)) = {}" |
|
371 shows "\<exists>q. q \<bullet> bs = p \<bullet> bs \<and> supp q \<subseteq> (set bs) \<union> (set (p \<bullet> bs))" |
|
372 sorry |
|
373 |
|
374 lemma abs_rename_set2: |
|
375 fixes x::"'a::fs" |
|
376 assumes "(p \<bullet> bs) \<sharp>* x" "bs \<inter> p \<bullet> bs ={}" "finite bs" |
|
377 shows "\<exists>y. [bs]set. x = [p \<bullet> bs]set. y" |
|
378 using yy assms |
|
379 apply - |
|
380 apply(drule_tac x="bs" in meta_spec) |
|
381 apply(drule_tac x="p" in meta_spec) |
|
382 apply(auto) |
|
383 apply(rule_tac x="q \<bullet> x" in exI) |
|
384 apply(subgoal_tac "(q \<bullet> ([bs]set. x)) = [bs]set. x") |
|
385 apply(simp add: permute_Abs) |
|
386 apply(rule supp_perm_eq) |
|
387 apply(rule fresh_star_supp_conv) |
|
388 apply(simp add: fresh_star_def) |
|
389 apply(simp add: Abs_fresh_iff) |
|
390 apply(auto) |
|
391 done |
|
392 |
317 lemma abs_rename_list: |
393 lemma abs_rename_list: |
318 fixes x::"'a::fs" |
394 fixes x::"'a::fs" |
319 assumes "b' \<sharp> x" "sort_of b = sort_of b'" |
395 assumes "b' \<sharp> x" "sort_of b = sort_of b'" |
320 shows "\<exists>y. [[b]]lst. x = [[b']]lst. y" |
396 shows "\<exists>y. [[b]]lst. x = [[b']]lst. y" |
321 apply(rule_tac x="(b \<rightleftharpoons> b') \<bullet> x" in exI) |
397 apply(rule_tac x="(b \<rightleftharpoons> b') \<bullet> x" in exI) |
325 apply(simp add: fresh_def) |
401 apply(simp add: fresh_def) |
326 apply(perm_simp) |
402 apply(perm_simp) |
327 using assms |
403 using assms |
328 apply(simp) |
404 apply(simp) |
329 done |
405 done |
|
406 |
|
407 lemma abs_rename_list2: |
|
408 fixes x::"'a::fs" |
|
409 assumes "(set (p \<bullet> bs)) \<sharp>* x" "(set bs) \<inter> (set (p \<bullet> bs)) ={}" |
|
410 shows "\<exists>y. [bs]lst. x = [p \<bullet> bs]lst. y" |
|
411 using zz assms |
|
412 apply - |
|
413 apply(drule_tac x="bs" in meta_spec) |
|
414 apply(drule_tac x="p" in meta_spec) |
|
415 apply(auto simp add: set_eqvt) |
|
416 apply(rule_tac x="q \<bullet> x" in exI) |
|
417 apply(subgoal_tac "(q \<bullet> ([bs]lst. x)) = [bs]lst. x") |
|
418 apply(simp) |
|
419 apply(rule supp_perm_eq) |
|
420 apply(rule fresh_star_supp_conv) |
|
421 apply(simp add: fresh_star_def) |
|
422 apply(simp add: Abs_fresh_iff) |
|
423 apply(auto) |
|
424 done |
|
425 |
330 |
426 |
331 lemma test3: |
427 lemma test3: |
332 fixes c::"'a::fs" |
428 fixes c::"'a::fs" |
333 assumes a: "y = Let2 x1 x2 trm1 trm2" |
429 assumes a: "y = Let2 x1 x2 trm1 trm2" |
334 and b: "\<forall>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<longrightarrow> P" |
430 and b: "\<forall>x1 x2 trm1 trm2. {atom x1, atom x2} \<sharp>* c \<and> y = Let2 x1 x2 trm1 trm2 \<longrightarrow> P" |
336 using b[simplified a] |
432 using b[simplified a] |
337 apply - |
433 apply - |
338 apply(subgoal_tac "\<exists>q::perm. (q \<bullet> {atom x1, atom x2}) \<sharp>* (c, x1, x2, trm1, trm2)") |
434 apply(subgoal_tac "\<exists>q::perm. (q \<bullet> {atom x1, atom x2}) \<sharp>* (c, x1, x2, trm1, trm2)") |
339 apply(erule exE) |
435 apply(erule exE) |
340 apply(perm_simp) |
436 apply(perm_simp) |
|
437 apply(simp only: foo.eq_iff) |
341 apply(drule_tac x="q \<bullet> x1" in spec) |
438 apply(drule_tac x="q \<bullet> x1" in spec) |
342 apply(drule_tac x="q \<bullet> x2" in spec) |
439 apply(drule_tac x="q \<bullet> x2" in spec) |
343 apply(simp only: foo.eq_iff) |
|
344 apply(simp) |
440 apply(simp) |
345 apply(erule mp) |
441 apply(erule mp) |
346 apply(rule conjI) |
442 apply(rule conjI) |
347 apply(simp add: fresh_star_prod) |
443 apply(simp add: fresh_star_prod) |
348 apply(rule conjI) |
444 apply(rule conjI) |
349 prefer 2 |
445 apply(simp add: atom_eqvt[symmetric]) |
350 apply(rule abs_rename_list) |
446 apply(subst (2) permute_list.simps(1)[where p="q", symmetric]) |
351 apply(simp add: fresh_star_prod) |
447 apply(subst permute_list.simps(2)[symmetric]) |
352 apply(simp add: fresh_star_def) |
448 apply(subst permute_list.simps(2)[symmetric]) |
353 apply(simp) |
449 apply(rule abs_rename_list2) |
354 apply(case_tac "x1=x2") |
450 apply(simp add: atom_eqvt fresh_star_prod) |
355 apply(simp) |
451 apply(simp add: atom_eqvt fresh_star_prod fresh_star_def fresh_Pair fresh_def supp_Pair supp_at_base) |
356 apply(subst Abs_swap2[where a="atom x2" and b="atom (q \<bullet> x2)"]) |
452 apply(simp add: atom_eqvt[symmetric]) |
357 apply(simp) |
453 apply(subst (2) permute_list.simps(1)[where p="q", symmetric]) |
358 apply(simp add: fresh_star_def) |
454 apply(subst permute_list.simps(2)[symmetric]) |
359 apply(simp add: fresh_def supp_Pair) |
455 apply(rule abs_rename_list2) |
360 apply(simp) |
456 apply(simp add: atom_eqvt fresh_star_prod) |
361 apply(rule exI) |
457 apply(simp add: atom_eqvt fresh_star_prod fresh_star_def fresh_Pair fresh_def supp_Pair supp_at_base) |
362 apply(rule refl) |
458 apply(simp add: atom_eqvt[symmetric]) |
363 apply(subst Abs_swap2[where a="atom x2" and b="atom (q \<bullet> x2)"]) |
459 apply(simp add: atom_eqvt fresh_star_prod fresh_star_def fresh_Pair fresh_def supp_Pair supp_at_base) |
364 apply(simp) |
460 sorry |
365 apply(simp add: fresh_star_def) |
|
366 apply(simp add: fresh_def supp_Pair) |
|
367 apply(simp) |
|
368 apply(simp add: flip_def[symmetric] atom_eqvt) |
|
369 apply(subgoal_tac "q \<bullet> x2 \<noteq> x1") |
|
370 apply(simp) |
|
371 apply(subst Abs_swap2[where a="atom x1" and b="atom (q \<bullet> x1)"]) |
|
372 apply(simp) |
|
373 apply(subgoal_tac " atom (q \<bullet> x1) \<notin> supp ((x2 \<leftrightarrow> q \<bullet> x2) \<bullet> trm1)") |
|
374 apply(simp add: fresh_star_def) |
|
375 apply(simp add: fresh_star_def) |
|
376 apply(simp add: fresh_def supp_Pair) |
|
377 apply(erule conjE)+ |
|
378 apply(rule_tac p="(x2 \<leftrightarrow> q \<bullet> x2)" in permute_boolE) |
|
379 apply(simp add: mem_eqvt Not_eqvt atom_eqvt supp_eqvt) |
|
380 apply(subgoal_tac "q \<bullet> x2 \<noteq> q \<bullet> x1") |
|
381 apply(subgoal_tac "x2 \<noteq> q \<bullet> x1") |
|
382 apply(simp) |
|
383 apply(simp add: supp_at_base) |
|
384 apply(simp) |
|
385 apply(simp) |
|
386 apply(rule exI) |
|
387 apply(rule refl) |
|
388 apply(simp add: fresh_star_def) |
|
389 apply(simp add: fresh_def supp_Pair) |
|
390 apply(simp add: supp_at_base) |
|
391 apply(rule at_set_avoiding3[where x="()", simplified]) |
|
392 apply(simp) |
|
393 apply(simp add: finite_supp) |
|
394 apply(simp add: finite_supp) |
|
395 apply(simp add: fresh_star_def fresh_Unit) |
|
396 done |
|
397 |
461 |
398 lemma test4: |
462 lemma test4: |
399 fixes c::"'a::fs" |
463 fixes c::"'a::fs" |
400 assumes a: "y = Let2 x1 x2 trm1 trm2" |
464 assumes a: "y = Let2 x1 x2 trm1 trm2" |
401 and b: "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P" |
465 and b: "\<And>x1 x2 trm1 trm2. \<lbrakk>{atom x1, atom x2} \<sharp>* c; y = Let2 x1 x2 trm1 trm2\<rbrakk> \<Longrightarrow> P" |