equal
deleted
inserted
replaced
48 done |
48 done |
49 |
49 |
50 lemma alpha5_eqvt: |
50 lemma alpha5_eqvt: |
51 "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)" |
51 "xa \<approx>5 y \<Longrightarrow> (x \<bullet> xa) \<approx>5 (x \<bullet> y)" |
52 "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)" |
52 "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)" |
53 "alpha_rbv5 a b c \<Longrightarrow> True" |
53 "alpha_rbv5 a b c \<Longrightarrow> alpha_rbv5 (x \<bullet> a) (x \<bullet> b) (x \<bullet> c)" |
54 apply (induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) |
54 apply (induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) |
55 apply (simp_all add: alpha5_inj) |
55 apply (simp_all add: alpha5_inj permute_eqvt[symmetric]) |
56 apply (erule exE) |
56 apply (erule exE) |
57 apply (rule_tac x="pi" in exI) |
57 apply (rule_tac x="pi" in exI) |
|
58 apply (simp add: alpha_gen) |
58 apply clarify |
59 apply clarify |
59 apply (simp add: alpha_gen fv_rtrm5_rlts_eqvt[symmetric] rbv5_eqvt[symmetric]) |
60 apply (simp add: fv_rtrm5_rlts_eqvt[symmetric] rbv5_eqvt[symmetric]) |
60 apply (subst eqvts[symmetric]) |
61 apply (subst eqvts[symmetric]) |
61 apply (subst eqvts[symmetric]) |
62 apply (subst eqvts[symmetric]) |
|
63 apply (subst permute_eqvt) |
|
64 apply simp |
62 sorry |
65 sorry |
63 |
66 |
64 lemma alpha5_equivp: |
67 lemma alpha5_equivp: |
65 "equivp alpha_rtrm5" |
68 "equivp alpha_rtrm5" |
66 "equivp alpha_rlts" |
69 "equivp alpha_rlts" |