equal
deleted
inserted
replaced
52 (xb \<approx>l ya \<longrightarrow> (p \<bullet> xb) \<approx>l (p \<bullet> ya)) \<and> |
52 (xb \<approx>l ya \<longrightarrow> (p \<bullet> xb) \<approx>l (p \<bullet> ya)) \<and> |
53 (alpha_rbv5 a b c \<longrightarrow> alpha_rbv5 (p \<bullet> a) (p \<bullet> b) (p \<bullet> c))" |
53 (alpha_rbv5 a b c \<longrightarrow> alpha_rbv5 (p \<bullet> a) (p \<bullet> b) (p \<bullet> c))" |
54 apply (tactic {* alpha_eqvt_tac @{thm alpha_rtrm5_alpha_rlts_alpha_rbv5.induct} @{thms alpha5_inj permute_rtrm5_permute_rlts.simps} @{context} 1 *}) |
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 done |
55 done |
56 |
56 |
|
57 lemma alpha5_reflp: |
|
58 "y \<approx>5 y \<and> (x \<approx>l x \<and> alpha_rbv5 0 x x)" |
|
59 apply (rule rtrm5_rlts.induct) |
|
60 apply (simp_all add: alpha5_inj) |
|
61 apply (rule_tac x="0::perm" in exI) |
|
62 apply (simp add: eqvts alpha_gen fresh_star_def fresh_zero_perm) |
|
63 done |
|
64 |
|
65 lemma alpha5_symp: |
|
66 "(a \<approx>5 b \<longrightarrow> a \<approx>5 b) \<and> |
|
67 (x \<approx>l y \<longrightarrow> y \<approx>l x) \<and> |
|
68 (alpha_rbv5 p x y \<longrightarrow> alpha_rbv5 (-p) y x)" |
|
69 apply (rule alpha_rtrm5_alpha_rlts_alpha_rbv5.induct) |
|
70 apply (simp_all add: alpha5_inj) |
|
71 sorry |
|
72 |
57 lemma alpha5_equivp: |
73 lemma alpha5_equivp: |
58 "equivp alpha_rtrm5" |
74 "equivp alpha_rtrm5" |
59 "equivp alpha_rlts" |
75 "equivp alpha_rlts" |
|
76 "equivp (alpha_rbv5 p)" |
60 sorry |
77 sorry |
61 |
78 |
62 quotient_type |
79 quotient_type |
63 trm5 = rtrm5 / alpha_rtrm5 |
80 trm5 = rtrm5 / alpha_rtrm5 |
64 and |
81 and |