equal
deleted
inserted
replaced
33 thm trm_lts.distinct |
33 thm trm_lts.distinct |
34 (*thm trm_lts.supp*) |
34 (*thm trm_lts.supp*) |
35 thm trm_lts.fv[simplified trm_lts.supp(1-2)] |
35 thm trm_lts.fv[simplified trm_lts.supp(1-2)] |
36 |
36 |
37 |
37 |
|
38 declare permute_trm_raw_permute_lts_raw.simps[eqvt] |
|
39 declare alpha_gen_eqvt[eqvt] |
|
40 |
|
41 equivariance alpha_trm_raw |
|
42 |
|
43 |
|
44 |
38 primrec |
45 primrec |
39 permute_bn_raw |
46 permute_bn_raw |
40 where |
47 where |
41 "permute_bn_raw pi (Lnil_raw) = Lnil_raw" |
48 "permute_bn_raw pi (Lnil_raw) = Lnil_raw" |
42 | "permute_bn_raw pi (Lcons_raw a t l) = Lcons_raw (pi \<bullet> a) t (permute_bn_raw pi l)" |
49 | "permute_bn_raw pi (Lcons_raw a t l) = Lcons_raw (pi \<bullet> a) t (permute_bn_raw pi l)" |
93 "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)" |
100 "supp (Abs_lst (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)" |
94 apply (simp add: trm_lts.eq_iff permute_bn_alpha_bn) |
101 apply (simp add: trm_lts.eq_iff permute_bn_alpha_bn) |
95 apply (rule_tac x="q" in exI) |
102 apply (rule_tac x="q" in exI) |
96 apply (simp add: alphas) |
103 apply (simp add: alphas) |
97 apply (simp add: perm_bn[symmetric]) |
104 apply (simp add: perm_bn[symmetric]) |
98 apply (simp add: eqvts[symmetric]) |
105 apply(rule conjI) |
99 apply (simp add: supp_abs) |
106 apply(drule supp_perm_eq) |
|
107 apply(simp add: abs_eq_iff) |
|
108 apply(simp add: alphas_abs alphas) |
|
109 apply(drule conjunct1) |
100 apply (simp add: trm_lts.supp) |
110 apply (simp add: trm_lts.supp) |
101 apply (rule supp_perm_eq[symmetric]) |
111 apply(simp add: supp_abs) |
102 apply (subst supp_finite_atom_set) |
112 apply (simp add: trm_lts.supp) |
103 apply (rule finite_Diff) |
|
104 apply (simp add: finite_supp) |
|
105 apply (assumption) |
|
106 done |
113 done |
107 |
114 |
108 |
115 |
109 lemma fin_bn: |
116 lemma fin_bn: |
110 "finite (set (bn l))" |
117 "finite (set (bn l))" |