equal
deleted
inserted
replaced
46 apply (induct x and l) |
46 apply (induct x and l) |
47 apply (simp_all add: eqvts atom_eqvt) |
47 apply (simp_all add: eqvts atom_eqvt) |
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> (p \<bullet> xa) \<approx>5 (p \<bullet> y)) \<and> |
52 "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)" |
52 (xb \<approx>l ya \<longrightarrow> (p \<bullet> xb) \<approx>l (p \<bullet> ya)) \<and> |
53 "alpha_rbv5 a b c \<Longrightarrow> alpha_rbv5 (x \<bullet> a) (x \<bullet> b) (x \<bullet> c)" |
53 (alpha_rbv5 a b c \<longrightarrow> alpha_rbv5 (p \<bullet> a) (p \<bullet> b) (p \<bullet> c))" |
54 apply (induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) |
54 apply (tactic {* alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} @{context} 1 *}) |
55 apply (simp_all add: alpha5_inj permute_eqvt[symmetric]) |
|
56 apply (erule exE) |
|
57 apply (rule_tac x="x \<bullet> pi" in exI) |
|
58 apply (erule conjE)+ |
|
59 apply (rule conjI) |
|
60 apply (erule alpha_gen_compose_eqvt) |
|
61 apply (simp_all add: eqvts) |
|
62 apply (simp add: permute_eqvt[symmetric]) |
|
63 apply (subst eqvts[symmetric]) |
|
64 apply (simp add: eqvts) |
|
65 done |
55 done |
66 |
56 |
67 lemma alpha5_equivp: |
57 lemma alpha5_equivp: |
68 "equivp alpha_rtrm5" |
58 "equivp alpha_rtrm5" |
69 "equivp alpha_rlts" |
59 "equivp alpha_rlts" |