2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs" "../QuotProd" |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "Abs" "../QuotProd" |
3 begin |
3 begin |
4 |
4 |
5 |
5 |
6 (* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *) |
6 (* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *) |
7 lemma in_permute_iff: |
|
8 shows "(p \<bullet> x) \<in> (p \<bullet> X) \<longleftrightarrow> x \<in> X" |
|
9 apply(unfold mem_def permute_fun_def)[1] |
|
10 apply(simp add: permute_bool_def) |
|
11 done |
|
12 |
|
13 lemma fresh_star_permute_iff: |
|
14 shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
|
15 apply(simp add: fresh_star_def) |
|
16 apply(auto) |
|
17 apply(drule_tac x="p \<bullet> xa" in bspec) |
|
18 apply(unfold mem_def permute_fun_def)[1] |
|
19 apply(simp add: eqvts) |
|
20 apply(simp add: fresh_permute_iff) |
|
21 apply(rule_tac ?p1="- p" in fresh_permute_iff[THEN iffD1]) |
|
22 apply(simp) |
|
23 apply(drule_tac x="- p \<bullet> xa" in bspec) |
|
24 apply(rule_tac ?p1="p" in in_permute_iff[THEN iffD1]) |
|
25 apply(simp) |
|
26 apply(simp) |
|
27 done |
|
28 |
|
29 lemma fresh_plus: |
|
30 fixes p q::perm |
|
31 shows "\<lbrakk>a \<sharp> p; a \<sharp> q\<rbrakk> \<Longrightarrow> a \<sharp> (p + q)" |
|
32 unfolding fresh_def |
|
33 using supp_plus_perm |
|
34 apply(auto) |
|
35 done |
|
36 |
|
37 lemma fresh_star_plus: |
|
38 fixes p q::perm |
|
39 shows "\<lbrakk>a \<sharp>* p; a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)" |
|
40 unfolding fresh_star_def |
|
41 by (simp add: fresh_plus) |
|
42 |
|
43 lemma supp_finite_set: |
7 lemma supp_finite_set: |
44 fixes S::"atom set" |
8 fixes S::"atom set" |
45 assumes "finite S" |
9 assumes "finite S" |
46 shows "supp S = S" |
10 shows "supp S = S" |
47 apply(rule finite_supp_unique) |
11 apply(rule finite_supp_unique) |
189 apply(rule_tac x="0" in exI) |
153 apply(rule_tac x="0" in exI) |
190 apply(rule alpha_gen_refl) |
154 apply(rule alpha_gen_refl) |
191 apply(assumption) |
155 apply(assumption) |
192 done |
156 done |
193 |
157 |
194 lemma fresh_minus_perm: |
|
195 fixes p::perm |
|
196 shows "a \<sharp> (- p) \<longleftrightarrow> a \<sharp> p" |
|
197 apply(simp add: fresh_def) |
|
198 apply(simp only: supp_minus_perm) |
|
199 done |
|
200 |
|
201 lemma alpha_gen_atom_sym: |
|
202 assumes a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
|
203 shows "\<exists>pi. ({atom a}, t) \<approx>gen \<lambda>x1 x2. R x1 x2 \<and> R x2 x1 f pi ({atom b}, s) \<Longrightarrow> |
|
204 \<exists>pi. ({atom b}, s) \<approx>gen R f pi ({atom a}, t)" |
|
205 apply(erule exE) |
|
206 apply(rule_tac x="- pi" in exI) |
|
207 apply(simp add: alpha_gen.simps) |
|
208 apply(erule conjE)+ |
|
209 apply(rule conjI) |
|
210 apply(simp add: fresh_star_def fresh_minus_perm) |
|
211 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
|
212 apply simp |
|
213 apply(rule a) |
|
214 apply assumption |
|
215 done |
|
216 |
|
217 lemma alpha_sym: |
158 lemma alpha_sym: |
218 shows "t \<approx> s \<Longrightarrow> s \<approx> t" |
159 shows "t \<approx> s \<Longrightarrow> s \<approx> t" |
219 apply(induct rule: alpha.induct) |
160 apply(induct rule: alpha.induct) |
220 apply(simp add: a1) |
161 apply(simp add: a1) |
221 apply(simp add: a2) |
162 apply(simp add: a2) |
236 apply(simp_all) |
177 apply(simp_all) |
237 apply(simp add: a2) |
178 apply(simp add: a2) |
238 apply(erule alpha.cases) |
179 apply(erule alpha.cases) |
239 apply(simp_all) |
180 apply(simp_all) |
240 apply(rule a3) |
181 apply(rule a3) |
241 apply(simp add: alpha_gen.simps) |
182 apply(rule alpha_gen_atom_trans) |
242 apply(erule conjE)+ |
183 apply(rule alpha_eqvt) |
243 apply(erule exE)+ |
184 apply(assumption)+ |
244 apply(erule conjE)+ |
|
245 apply(rule_tac x="pia + pi" in exI) |
|
246 apply(simp add: fresh_star_plus) |
|
247 apply(drule_tac x="- pia \<bullet> sa" in spec) |
|
248 apply(drule mp) |
|
249 apply(rotate_tac 7) |
|
250 apply(drule_tac pi="- pia" in alpha_eqvt) |
|
251 apply(simp) |
|
252 apply(rotate_tac 9) |
|
253 apply(drule_tac pi="pia" in alpha_eqvt) |
|
254 apply(simp) |
|
255 done |
185 done |
256 |
186 |
257 lemma alpha_equivp: |
187 lemma alpha_equivp: |
258 shows "equivp alpha" |
188 shows "equivp alpha" |
259 apply(rule equivpI) |
189 apply(rule equivpI) |