28 thm trm_lts.induct[no_vars] |
28 thm trm_lts.induct[no_vars] |
29 thm trm_lts.inducts[no_vars] |
29 thm trm_lts.inducts[no_vars] |
30 thm trm_lts.distinct |
30 thm trm_lts.distinct |
31 thm trm_lts.fv[simplified trm_lts.supp] |
31 thm trm_lts.fv[simplified trm_lts.supp] |
32 |
32 |
33 consts |
33 primrec |
34 permute_bn :: "perm \<Rightarrow> lts \<Rightarrow> lts" |
34 permute_bn_raw |
35 |
35 where |
36 lemma test: |
36 "permute_bn_raw pi (Lnil_raw) = Lnil_raw" |
37 "permute_bn pi (Lnil) = Lnil" |
37 | "permute_bn_raw pi (Lcons_raw a t l) = Lcons_raw (pi \<bullet> a) t (permute_bn_raw pi l)" |
38 "permute_bn pi (Lcons a t l) = Lcons (pi \<bullet> a) t (permute_bn pi l)" |
38 |
39 sorry |
39 quotient_definition |
|
40 "permute_bn :: perm \<Rightarrow> lts \<Rightarrow> lts" |
|
41 is |
|
42 "permute_bn_raw" |
|
43 |
|
44 lemma [quot_respect]: "((op =) ===> alpha_lts_raw ===> alpha_lts_raw) permute_bn_raw permute_bn_raw" |
|
45 apply simp |
|
46 apply clarify |
|
47 apply (erule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.inducts) |
|
48 apply simp_all |
|
49 apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros) |
|
50 apply simp |
|
51 apply (rule alpha_trm_raw_alpha_lts_raw_alpha_bn_raw.intros) |
|
52 apply simp |
|
53 done |
|
54 |
|
55 lemmas permute_bn = permute_bn_raw.simps[quot_lifted] |
40 |
56 |
41 lemma permute_bn_zero: |
57 lemma permute_bn_zero: |
42 "permute_bn 0 a = a" |
58 "permute_bn 0 a = a" |
43 apply(induct a rule: trm_lts.inducts(2)) |
59 apply(induct a rule: trm_lts.inducts(2)) |
44 apply(rule TrueI) |
60 apply(rule TrueI) |
45 apply(simp_all add:test eqvts) |
61 apply(simp_all add:permute_bn eqvts) |
46 done |
62 done |
47 |
63 |
48 lemma permute_bn_add: |
64 lemma permute_bn_add: |
49 "permute_bn (p + q) a = permute_bn p (permute_bn q a)" |
65 "permute_bn (p + q) a = permute_bn p (permute_bn q a)" |
50 oops |
66 oops |
51 |
67 |
52 lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)" |
68 lemma permute_bn_alpha_bn: "alpha_bn lts (permute_bn q lts)" |
53 apply(induct lts rule: trm_lts.inducts(2)) |
69 apply(induct lts rule: trm_lts.inducts(2)) |
54 apply(rule TrueI) |
70 apply(rule TrueI) |
55 apply(simp_all add:test eqvts trm_lts.eq_iff) |
71 apply(simp_all add:permute_bn eqvts trm_lts.eq_iff) |
56 done |
72 done |
57 |
73 |
58 lemma perm_bn: |
74 lemma perm_bn: |
59 "p \<bullet> bn l = bn(permute_bn p l)" |
75 "p \<bullet> bn l = bn(permute_bn p l)" |
60 apply(induct l rule: trm_lts.inducts(2)) |
76 apply(induct l rule: trm_lts.inducts(2)) |
61 apply(rule TrueI) |
77 apply(rule TrueI) |
62 apply(simp_all add:test eqvts) |
78 apply(simp_all add:permute_bn eqvts) |
63 done |
79 done |
64 |
80 |
65 lemma Lt_subst: |
81 lemma Lt_subst: |
66 "supp (Abs (bn lts) trm) \<sharp>* q \<Longrightarrow> (Lt lts trm) = Lt (permute_bn q lts) (q \<bullet> trm)" |
82 "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) |
83 apply (simp only: trm_lts.eq_iff) |
142 apply(simp add: finite_supp) |
158 apply(simp add: finite_supp) |
143 apply(simp add: supp_Abs) |
159 apply(simp add: supp_Abs) |
144 apply(rule finite_Diff) |
160 apply(rule finite_Diff) |
145 apply(simp add: finite_supp) |
161 apply(simp add: finite_supp) |
146 apply(simp add: fresh_star_def fresh_def supp_Abs) |
162 apply(simp add: fresh_star_def fresh_def supp_Abs) |
147 apply(simp add: eqvts test) |
163 apply(simp add: eqvts permute_bn) |
148 apply(rule a5) |
164 apply(rule a5) |
149 apply(simp add: test) |
165 apply(simp add: permute_bn) |
150 apply(rule a6) |
166 apply(rule a6) |
151 apply simp |
167 apply simp |
152 apply simp |
168 apply simp |
153 done |
169 done |
154 then have a: "P1 c (0 \<bullet> t)" by blast |
170 then have a: "P1 c (0 \<bullet> t)" by blast |