equal
deleted
inserted
replaced
155 print_theorems |
155 print_theorems |
156 |
156 |
157 lemma alpha5_rfv: |
157 lemma alpha5_rfv: |
158 "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)" |
158 "(t \<approx>5 s \<Longrightarrow> fv_rtrm5 t = fv_rtrm5 s)" |
159 "(l \<approx>l m \<Longrightarrow> (fv_rlts l = fv_rlts m \<and> fv_rbv5 l = fv_rbv5 m))" |
159 "(l \<approx>l m \<Longrightarrow> (fv_rlts l = fv_rlts m \<and> fv_rbv5 l = fv_rbv5 m))" |
160 "(alpha_rbv5 0 b c \<Longrightarrow> fv_rbv5 b = fv_rbv5 c)" |
160 "(alpha_rbv5 p b c \<Longrightarrow> fv_rbv5 (p \<bullet> b) = fv_rbv5 c)" |
161 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) |
161 apply(induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) |
162 apply(simp_all add: eqvts) |
162 apply(simp_all add: eqvts) |
|
163 thm alpha5_inj |
163 apply(simp add: alpha_gen) |
164 apply(simp add: alpha_gen) |
164 apply(clarify) |
165 apply(clarify) |
165 apply(simp) |
166 apply(simp) |
166 sorry |
167 sorry |
167 |
168 |
230 lemmas bv5[simp] = rbv5.simps[quot_lifted] |
231 lemmas bv5[simp] = rbv5.simps[quot_lifted] |
231 lemmas fv_trm5_bv5[simp] = fv_rtrm5_fv_rbv5.simps[quot_lifted] |
232 lemmas fv_trm5_bv5[simp] = fv_rtrm5_fv_rbv5.simps[quot_lifted] |
232 lemmas fv_lts[simp] = fv_rlts.simps[quot_lifted] |
233 lemmas fv_lts[simp] = fv_rlts.simps[quot_lifted] |
233 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
234 lemmas alpha5_INJ = alpha5_inj[unfolded alpha_gen, quot_lifted, folded alpha_gen] |
234 |
235 |
|
236 lemma lets_bla: |
|
237 "x \<noteq> z \<Longrightarrow> y \<noteq> z \<Longrightarrow> x \<noteq> y \<Longrightarrow>(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) = (Lt5 (Lcons x (Vr5 z) Lnil) (Vr5 x))" |
|
238 apply (simp only: alpha5_INJ) |
|
239 apply (simp only: bv5) |
|
240 apply simp |
|
241 apply (rule_tac x="(z \<leftrightarrow> y)" in exI) |
|
242 apply (simp_all add: alpha_gen) |
|
243 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ eqvts) |
|
244 done |
|
245 |
235 lemma lets_ok: |
246 lemma lets_ok: |
236 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
247 "(Lt5 (Lcons x (Vr5 x) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
237 thm alpha5_INJ |
248 thm alpha5_INJ |
238 apply (simp only: alpha5_INJ) |
249 apply (simp only: alpha5_INJ) |
239 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
250 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |