379 apply simp |
379 apply simp |
380 apply (simp add: flip_def) |
380 apply (simp add: flip_def) |
381 apply (simp add: fresh_Pair_elim fresh_at_base) |
381 apply (simp add: fresh_Pair_elim fresh_at_base) |
382 done |
382 done |
383 |
383 |
|
384 lemma distinct_swapequal: "\<forall>p q. p \<bullet> l \<noteq> q \<bullet> r \<Longrightarrow> \<not>swapequal l r xs" |
|
385 apply (induct xs rule:swapequal.induct) |
|
386 apply simp |
|
387 apply metis |
|
388 apply (simp add: fresh_Pair_elim) |
|
389 apply (subgoal_tac "\<forall>(p\<Colon>perm) q\<Colon>perm. p \<bullet> (hl \<leftrightarrow> x) \<bullet> l \<noteq> q \<bullet> (hr \<leftrightarrow> x) \<bullet> r") |
|
390 apply simp |
|
391 apply (intro allI) |
|
392 apply (drule_tac x="p + (hl \<leftrightarrow> x)" in spec) |
|
393 apply (drule_tac x="q + (hr \<leftrightarrow> x)" in spec) |
|
394 apply simp |
|
395 done |
|
396 |
|
397 lemma swapequal_app: "(swapequal l1 l2 xs \<and> swapequal r1 r2 xs) = swapequal (App l1 r1) (App l2 r2) xs" |
|
398 apply (induct xs arbitrary: l1 l2 r1 r2) |
|
399 apply simp |
|
400 apply (case_tac a) |
|
401 apply simp |
|
402 apply (rule_tac x="(l1, l2, r1, r2, aa, b, xs)" and ?'a="name" in obtain_fresh) |
|
403 apply (simp add: fresh_Pair_elim) |
|
404 apply (subst swapequal.simps) apply (simp add: fresh_Pair) apply auto[1] |
|
405 apply (subst swapequal.simps) apply (simp add: fresh_Pair lam.fresh) apply auto[1] |
|
406 apply simp |
|
407 done |
|
408 |
|
409 lemma [simp]: "distinct (map fst xs) \<Longrightarrow> distinct xs" |
|
410 by (induct xs) auto |
|
411 |
|
412 lemma [simp]: |
|
413 "atom x \<sharp> xs \<Longrightarrow> x \<notin> fst ` set xs" |
|
414 "atom x \<sharp> xs \<Longrightarrow> x \<notin> snd ` set xs" |
|
415 apply (induct xs) |
|
416 apply simp_all |
|
417 apply (case_tac [!] a) |
|
418 apply (simp_all add: fresh_Cons fresh_Pair fresh_at_base) |
|
419 done |
|
420 |
384 lemma aux_alphaish: |
421 lemma aux_alphaish: |
385 assumes "distinct (map fst xs @ map snd xs)" |
422 assumes "distinct (map fst xs @ map snd xs)" |
386 shows "aux x y xs \<longleftrightarrow> swapequal x y xs" |
423 shows "aux x y xs \<longleftrightarrow> swapequal x y xs" |
387 using assms |
424 using assms |
388 apply (induct xs x y rule: aux_induct) |
425 apply (induct xs x y rule: aux_induct) |
389 apply (simp add: lookup_swapequal) |
426 apply (simp add: lookup_swapequal) |
390 prefer 8 |
427 apply (simp, rule distinct_swapequal, simp) |
|
428 apply (simp, rule distinct_swapequal, simp) |
|
429 apply (simp, rule distinct_swapequal, simp) |
|
430 apply (simp add: swapequal_app) |
|
431 apply (simp, rule distinct_swapequal, simp) |
|
432 apply (simp, rule distinct_swapequal, simp) |
|
433 apply (simp, rule distinct_swapequal, simp) |
391 apply (simp add: fresh_Pair_elim lam.fresh fresh_at_base) |
434 apply (simp add: fresh_Pair_elim lam.fresh fresh_at_base) |
392 apply (elim conjE) |
435 apply (elim conjE) |
393 apply (simp add: fresh_Pair_elim lam.fresh fresh_at_base) |
436 apply (simp add: fresh_Pair_elim lam.fresh fresh_at_base) |
394 apply (subgoal_tac "x \<notin> fst ` set xs \<and> |
437 apply (subgoal_tac "x \<notin> fst ` set xs \<and> |
395 x \<notin> snd ` set xs \<and> y \<notin> snd ` set xs \<and> y \<notin> fst ` set xs") |
438 x \<notin> snd ` set xs \<and> y \<notin> snd ` set xs \<and> y \<notin> fst ` set xs") |
396 apply (simp) |
439 apply (simp) |
397 apply (subst swapequal_lambda) |
440 apply (subst swapequal_lambda) |
398 apply auto[1] |
441 apply auto[2] |
399 sorry |
442 apply simp |
|
443 done |
400 |
444 |
401 lemma |
445 lemma |
402 "aux x y [] \<longleftrightarrow> (x = y)" |
446 "aux x y [] \<longleftrightarrow> (x = y)" |
403 by (simp_all add: supp_Nil aux_alphaish) |
447 by (simp_all add: supp_Nil aux_alphaish) |
404 |
448 |