equal
deleted
inserted
replaced
501 apply (auto simp add: supp_at_base)[1] |
501 apply (auto simp add: supp_at_base)[1] |
502 apply (simp only: fv_lam_raw.simps) |
502 apply (simp only: fv_lam_raw.simps) |
503 apply simp |
503 apply simp |
504 apply (rule conjI) |
504 apply (rule conjI) |
505 apply clarify |
505 apply clarify |
506 sorry |
506 oops |
507 |
507 |
508 thm supp_at_base |
|
509 lemma new_eqvt[eqvt]: "p \<bullet> (new s) = new (p \<bullet> s)" |
508 lemma new_eqvt[eqvt]: "p \<bullet> (new s) = new (p \<bullet> s)" |
510 sorry |
509 oops |
511 |
510 |
512 lemma subst_var_raw_eqvt[eqvt]: "p \<bullet> (subst_raw t y s) = subst_raw (p \<bullet> t) (p \<bullet> y) (p \<bullet> s)" |
511 lemma subst_var_raw_eqvt[eqvt]: "p \<bullet> (subst_raw t y s) = subst_raw (p \<bullet> t) (p \<bullet> y) (p \<bullet> s)" |
513 apply (induct t arbitrary: p y s) |
512 apply (induct t arbitrary: p y s) |
514 apply simp_all |
513 apply simp_all |
515 apply(perm_simp) |
514 apply(perm_simp) |
516 apply simp |
515 oops |
517 sorry |
|
518 |
516 |
519 lemma subst_id: "alpha_lam_raw (subst_raw x d (Var_raw d)) x" |
517 lemma subst_id: "alpha_lam_raw (subst_raw x d (Var_raw d)) x" |
520 apply (induct x arbitrary: d) |
518 apply (induct x arbitrary: d) |
521 apply (simp_all add: alpha_lam_raw.intros) |
519 apply (simp_all add: alpha_lam_raw.intros) |
522 apply (rule alpha_lam_raw.intros) |
520 apply (rule alpha_lam_raw.intros) |
552 apply (induct c arbitrary: a b y) |
550 apply (induct c arbitrary: a b y) |
553 apply (simp add: equivp_reflp[OF lam_equivp]) |
551 apply (simp add: equivp_reflp[OF lam_equivp]) |
554 apply (simp add: alpha_lam_raw.intros) |
552 apply (simp add: alpha_lam_raw.intros) |
555 apply simp |
553 apply simp |
556 apply (rule alpha_lam_raw.intros) |
554 apply (rule alpha_lam_raw.intros) |
|
555 apply (rule_tac x="((new (insert (atom y) (fv_lam_raw a \<union> fv_lam_raw c) - |
|
556 {atom name}))\<leftrightarrow>(new (insert (atom y) (fv_lam_raw b \<union> fv_lam_raw c) - |
|
557 {atom name})))" in exI) |
|
558 apply (simp only: alphas) |
|
559 apply (tactic {* split_conj_tac 1 *}) |
|
560 prefer 3 |
557 sorry |
561 sorry |
558 |
562 |
559 lemma [quot_respect]: |
563 lemma [quot_respect]: |
560 "(alpha_lam_raw ===> op = ===> alpha_lam_raw ===> alpha_lam_raw) subst_raw subst_raw" |
564 "(alpha_lam_raw ===> op = ===> alpha_lam_raw ===> alpha_lam_raw) subst_raw subst_raw" |
561 proof (intro fun_relI, simp) |
565 proof (intro fun_relI, simp) |
574 apply simp |
578 apply simp |
575 apply (rule alpha_lam_raw.intros) |
579 apply (rule alpha_lam_raw.intros) |
576 apply (rule_tac x ="(x \<leftrightarrow> (new (insert (atom y) (fv_lam_raw s \<union> fv_lam_raw t) - |
580 apply (rule_tac x ="(x \<leftrightarrow> (new (insert (atom y) (fv_lam_raw s \<union> fv_lam_raw t) - |
577 {atom x})))" in exI) |
581 {atom x})))" in exI) |
578 apply (simp only: alphas) |
582 apply (simp only: alphas) |
579 apply simp |
|
580 sorry |
583 sorry |
581 |
584 |
582 lemmas subst_simps = subst_raw.simps(1-2)[quot_lifted,no_vars] |
585 lemmas subst_simps = subst_raw.simps(1-2)[quot_lifted,no_vars] |
583 simp3[quot_lifted,simplified lam.supp,simplified fresh_def[symmetric], no_vars] |
586 simp3[quot_lifted,simplified lam.supp,simplified fresh_def[symmetric], no_vars] |
584 |
587 |