47 |
47 |
48 lemma permute_bn_add: |
48 lemma permute_bn_add: |
49 "permute_bn (p + q) a = permute_bn p (permute_bn q a)" |
49 "permute_bn (p + q) a = permute_bn p (permute_bn q a)" |
50 oops |
50 oops |
51 |
51 |
52 lemma Lt_subst: |
52 lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)" |
53 "supp (Abs (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)" |
53 apply(induct lts rule: trm_lts.inducts(2)) |
54 sorry |
54 apply(rule TrueI) |
|
55 apply(simp_all add:test eqvts trm_lts.eq_iff) |
|
56 done |
55 |
57 |
56 lemma perm_bn: |
58 lemma perm_bn: |
57 "p \<bullet> bn l = bn(permute_bn p l)" |
59 "p \<bullet> bn l = bn(permute_bn p l)" |
58 apply(induct l rule: trm_lts.inducts(2)) |
60 apply(induct l rule: trm_lts.inducts(2)) |
59 apply(rule TrueI) |
61 apply(rule TrueI) |
60 apply(simp_all add:test eqvts) |
62 apply(simp_all add:test eqvts) |
61 done |
63 done |
|
64 |
|
65 lemma Lt_subst: |
|
66 "supp (Abs (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)" |
|
67 apply (simp only: trm_lts.eq_iff) |
|
68 apply (rule_tac x="q" in exI) |
|
69 apply (simp add: alphas) |
|
70 apply (simp add: permute_bn_alpha_bn) |
|
71 apply (simp add: perm_bn[symmetric]) |
|
72 apply (simp add: eqvts[symmetric]) |
|
73 apply (simp add: supp_Abs) |
|
74 apply (simp add: trm_lts.supp) |
|
75 apply (rule supp_perm_eq[symmetric]) |
|
76 apply (subst supp_finite_atom_set) |
|
77 apply (rule finite_Diff) |
|
78 apply (simp add: finite_supp) |
|
79 apply (assumption) |
|
80 done |
|
81 |
62 |
82 |
63 lemma fin_bn: |
83 lemma fin_bn: |
64 "finite (bn l)" |
84 "finite (bn l)" |
65 apply(induct l rule: trm_lts.inducts(2)) |
85 apply(induct l rule: trm_lts.inducts(2)) |
66 apply(simp_all add:test eqvts) |
86 apply(simp_all add:test eqvts) |