228 apply(simp) |
228 apply(simp) |
229 done |
229 done |
230 |
230 |
231 lemma alpha_equivp: |
231 lemma alpha_equivp: |
232 shows "equivp alpha" |
232 shows "equivp alpha" |
233 apply(rule equivpI) |
233 apply(rule equivpI) |
234 unfolding reflp_def symp_def transp_def |
234 unfolding reflp_def symp_def transp_def |
235 apply(auto intro: alpha_refl alpha_sym alpha_trans) |
235 apply(auto intro: alpha_refl alpha_sym alpha_trans) |
236 done |
236 done |
237 |
237 |
238 lemma alpha_rfv: |
238 lemma alpha_rfv: |
239 shows "t \<approx> s \<Longrightarrow> rfv t = rfv s" |
239 shows "t \<approx> s \<Longrightarrow> rfv t = rfv s" |
240 apply(induct rule: alpha.induct) |
240 apply(induct rule: alpha.induct) |
241 apply(simp) |
241 apply(simp_all) |
242 apply(simp) |
242 done |
243 apply(simp) |
|
244 done |
|
245 |
243 |
246 |
244 |
247 quotient_type lam = rlam / alpha |
245 quotient_type lam = rlam / alpha |
248 by (rule alpha_equivp) |
246 by (rule alpha_equivp) |
249 |
247 |
375 (* should they lift automatically *) |
373 (* should they lift automatically *) |
376 lemma lam_inject [simp]: |
374 lemma lam_inject [simp]: |
377 shows "(Var a = Var b) = (a = b)" |
375 shows "(Var a = Var b) = (a = b)" |
378 and "(App t1 t2 = App s1 s2) = (t1 = s1 \<and> t2 = s2)" |
376 and "(App t1 t2 = App s1 s2) = (t1 = s1 \<and> t2 = s2)" |
379 apply(lifting rlam.inject(1) rlam.inject(2)) |
377 apply(lifting rlam.inject(1) rlam.inject(2)) |
|
378 apply(regularize) |
|
379 prefer 2 |
|
380 apply(regularize) |
|
381 prefer 2 |
380 apply(auto) |
382 apply(auto) |
381 apply(drule alpha.cases) |
383 apply(drule alpha.cases) |
382 apply(simp_all) |
384 apply(simp_all) |
383 apply(simp add: alpha.a1) |
385 apply(simp add: alpha.a1) |
384 apply(drule alpha.cases) |
386 apply(drule alpha.cases) |
395 and "\<not>(rVar nam \<approx> rLam nam' rlam')" |
397 and "\<not>(rVar nam \<approx> rLam nam' rlam')" |
396 and "\<not>(rLam nam' rlam' \<approx> rVar nam)" |
398 and "\<not>(rLam nam' rlam' \<approx> rVar nam)" |
397 and "\<not>(rApp rlam1 rlam2 \<approx> rLam nam' rlam')" |
399 and "\<not>(rApp rlam1 rlam2 \<approx> rLam nam' rlam')" |
398 and "\<not>(rLam nam' rlam' \<approx> rApp rlam1 rlam2)" |
400 and "\<not>(rLam nam' rlam' \<approx> rApp rlam1 rlam2)" |
399 apply auto |
401 apply auto |
400 apply(erule alpha.cases) |
402 apply (erule alpha.cases) |
401 apply simp_all |
403 apply (simp_all only: rlam.distinct) |
402 apply(erule alpha.cases) |
404 apply (erule alpha.cases) |
403 apply simp_all |
405 apply (simp_all only: rlam.distinct) |
404 apply(erule alpha.cases) |
406 apply (erule alpha.cases) |
405 apply simp_all |
407 apply (simp_all only: rlam.distinct) |
406 apply(erule alpha.cases) |
408 apply (erule alpha.cases) |
407 apply simp_all |
409 apply (simp_all only: rlam.distinct) |
408 apply(erule alpha.cases) |
410 apply (erule alpha.cases) |
409 apply simp_all |
411 apply (simp_all only: rlam.distinct) |
410 apply(erule alpha.cases) |
412 apply (erule alpha.cases) |
411 apply simp_all |
413 apply (simp_all only: rlam.distinct) |
412 done |
414 done |
413 |
415 |
414 lemma lam_distinct[simp]: |
416 lemma lam_distinct[simp]: |
415 shows "Var nam \<noteq> App lam1' lam2'" |
417 shows "Var nam \<noteq> App lam1' lam2'" |
416 and "App lam1' lam2' \<noteq> Var nam" |
418 and "App lam1' lam2' \<noteq> Var nam" |