equal
deleted
inserted
replaced
68 where |
68 where |
69 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
69 a1: "a = b \<Longrightarrow> (rVar a) \<approx> (rVar b)" |
70 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
70 | a2: "\<lbrakk>t1 \<approx> t2; s1 \<approx> s2\<rbrakk> \<Longrightarrow> rApp t1 s1 \<approx> rApp t2 s2" |
71 | a3: "\<exists>pi::name prm. (rfv t - {a} = rfv s - {b} \<and> (rfv t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s \<and> (pi \<bullet> a) = b) |
71 | a3: "\<exists>pi::name prm. (rfv t - {a} = rfv s - {b} \<and> (rfv t - {a})\<sharp>* pi \<and> (pi \<bullet> t) \<approx> s \<and> (pi \<bullet> a) = b) |
72 \<Longrightarrow> rLam a t \<approx> rLam b s" |
72 \<Longrightarrow> rLam a t \<approx> rLam b s" |
|
73 |
|
74 |
|
75 |
73 |
76 |
74 (* should be automatic with new version of eqvt-machinery *) |
77 (* should be automatic with new version of eqvt-machinery *) |
75 lemma alpha_eqvt: |
78 lemma alpha_eqvt: |
76 fixes pi::"name prm" |
79 fixes pi::"name prm" |
77 shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)" |
80 shows "t \<approx> s \<Longrightarrow> (pi \<bullet> t) \<approx> (pi \<bullet> s)" |
571 thm hom.simps |
574 thm hom.simps |
572 |
575 |
573 lemma term1_hom_rsp: |
576 lemma term1_hom_rsp: |
574 "\<lbrakk>(alpha ===> alpha ===> op =) f_app f_app; ((op = ===> alpha) ===> op =) f_lam f_lam\<rbrakk> |
577 "\<lbrakk>(alpha ===> alpha ===> op =) f_app f_app; ((op = ===> alpha) ===> op =) f_lam f_lam\<rbrakk> |
575 \<Longrightarrow> (alpha ===> op =) (term1_hom f_var f_app f_lam) (term1_hom f_var f_app f_lam)" |
578 \<Longrightarrow> (alpha ===> op =) (term1_hom f_var f_app f_lam) (term1_hom f_var f_app f_lam)" |
|
579 apply(simp) |
|
580 apply(rule allI)+ |
|
581 apply(rule impI) |
|
582 apply(erule alpha.induct) |
|
583 apply(auto)[1] |
|
584 apply(auto)[1] |
|
585 apply(simp) |
|
586 apply(erule conjE)+ |
|
587 apply(erule exE)+ |
|
588 apply(erule conjE)+ |
|
589 apply(clarify) |
576 sorry |
590 sorry |
577 |
591 |
578 lemma hom: " |
592 lemma hom: " |
579 \<forall>f_var. \<forall>f_app \<in> Respects(alpha ===> alpha ===> op =). |
593 \<forall>f_var. \<forall>f_app \<in> Respects(alpha ===> alpha ===> op =). |
580 \<forall>f_lam \<in> Respects((op = ===> alpha) ===> op =). |
594 \<forall>f_lam \<in> Respects((op = ===> alpha) ===> op =). |