equal
deleted
inserted
replaced
43 apply(simp_all add: union_eqvt Diff_eqvt) |
43 apply(simp_all add: union_eqvt Diff_eqvt) |
44 apply(simp_all add: permute_set_eq atom_eqvt) |
44 apply(simp_all add: permute_set_eq atom_eqvt) |
45 done |
45 done |
46 |
46 |
47 lemma alpha_eqvt: |
47 lemma alpha_eqvt: |
48 "t1 \<approx>ki s1 \<Longrightarrow> (pi \<bullet> t1) \<approx>ki (pi \<bullet> s1)" |
48 "(t1 \<approx>ki s1 \<longrightarrow> (p \<bullet> t1) \<approx>ki (p \<bullet> s1)) \<and> |
49 "t2 \<approx>ty s2 \<Longrightarrow> (pi \<bullet> t2) \<approx>ty (pi \<bullet> s2)" |
49 (t2 \<approx>ty s2 \<longrightarrow> (p \<bullet> t2) \<approx>ty (p \<bullet> s2)) \<and> |
50 "t3 \<approx>tr s3 \<Longrightarrow> (pi \<bullet> t3) \<approx>tr (pi \<bullet> s3)" |
50 (t3 \<approx>tr s3 \<longrightarrow> (p \<bullet> t3) \<approx>tr (p \<bullet> s3))" |
51 apply(induct rule: alpha_rkind_alpha_rty_alpha_rtrm.inducts) |
51 apply(rule alpha_rkind_alpha_rty_alpha_rtrm.induct) |
52 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm.intros) |
|
53 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj) |
52 apply (simp_all add: alpha_rkind_alpha_rty_alpha_rtrm_inj) |
54 apply (erule alpha_gen_compose_eqvt) |
53 apply (erule alpha_gen_compose_eqvt) |
55 apply (simp_all add: rfv_eqvt eqvts atom_eqvt) |
54 apply (simp_all add: rfv_eqvt eqvts atom_eqvt) |
56 apply (erule alpha_gen_compose_eqvt) |
55 apply (erule alpha_gen_compose_eqvt) |
57 apply (simp_all add: rfv_eqvt eqvts atom_eqvt) |
56 apply (simp_all add: rfv_eqvt eqvts atom_eqvt) |