1 theory Abs |
1 theory Abs |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "../QuotProd" |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../QuotMain" "../QuotProd" |
3 begin |
3 begin |
4 |
4 |
5 (* lemmas that should be in Nominal \<dots>\<dots>must be cleaned *) |
5 (* the next three lemmas that should be in Nominal \<dots>\<dots>must be cleaned *) |
|
6 lemma ball_image: |
|
7 shows "(\<forall>x \<in> p \<bullet> S. P x) = (\<forall>x \<in> S. P (p \<bullet> x))" |
|
8 apply(auto) |
|
9 apply(drule_tac x="p \<bullet> x" in bspec) |
|
10 apply(simp add: mem_permute_iff) |
|
11 apply(simp) |
|
12 apply(drule_tac x="(- p) \<bullet> x" in bspec) |
|
13 apply(rule_tac p1="p" in mem_permute_iff[THEN iffD1]) |
|
14 apply(simp) |
|
15 apply(simp) |
|
16 done |
|
17 |
6 lemma fresh_star_plus: |
18 lemma fresh_star_plus: |
7 fixes p q::perm |
19 fixes p q::perm |
8 shows "\<lbrakk>a \<sharp>* p; a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)" |
20 shows "\<lbrakk>a \<sharp>* p; a \<sharp>* q\<rbrakk> \<Longrightarrow> a \<sharp>* (p + q)" |
9 unfolding fresh_star_def |
21 unfolding fresh_star_def |
10 by (simp add: fresh_plus_perm) |
22 by (simp add: fresh_plus_perm) |
11 |
23 |
12 |
|
13 lemma fresh_star_permute_iff: |
24 lemma fresh_star_permute_iff: |
14 shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
25 shows "(p \<bullet> a) \<sharp>* (p \<bullet> x) \<longleftrightarrow> a \<sharp>* x" |
15 apply(simp add: fresh_star_def) |
26 apply(simp add: fresh_star_def) |
16 apply(auto) |
27 apply(simp add: ball_image) |
17 apply(drule_tac x="p \<bullet> xa" in bspec) |
|
18 apply(unfold mem_def permute_fun_def)[1] |
|
19 apply(simp add: eqvts del: permute_eqvt) |
|
20 apply(simp add: fresh_permute_iff) |
28 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 mem_permute_iff[THEN iffD1]) |
|
25 apply(simp) |
|
26 apply(simp) |
|
27 done |
29 done |
28 |
30 |
29 fun |
31 fun |
30 alpha_gen |
32 alpha_gen |
31 where |
33 where |
32 alpha_gen[simp del]: |
34 alpha_gen[simp del]: |
33 "(alpha_gen (bs, x) R f pi (cs, y)) \<longleftrightarrow> (f x - bs = f y - cs) \<and> ((f x - bs) \<sharp>* pi) \<and> (R (pi \<bullet> x) y)" |
35 "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow> f x - bs = f y - cs \<and> (f x - bs) \<sharp>* pi \<and> R (pi \<bullet> x) y" |
34 |
36 |
35 notation |
37 notation |
36 alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100) |
38 alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100) |
37 |
39 |
38 lemma [mono]: "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2" |
40 lemma [mono]: "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2" |
127 apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt) |
129 apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt) |
128 apply(subst permute_eqvt[symmetric]) |
130 apply(subst permute_eqvt[symmetric]) |
129 apply(simp) |
131 apply(simp) |
130 done |
132 done |
131 |
133 |
132 |
|
133 fun |
134 fun |
134 alpha_abs |
135 alpha_abs |
135 where |
136 where |
136 "alpha_abs (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))" |
137 "alpha_abs (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))" |
137 |
138 |
169 |
170 |
170 quotient_type 'a abs = "(atom set \<times> 'a::pt)" / "alpha_abs" |
171 quotient_type 'a abs = "(atom set \<times> 'a::pt)" / "alpha_abs" |
171 apply(rule equivpI) |
172 apply(rule equivpI) |
172 unfolding reflp_def symp_def transp_def |
173 unfolding reflp_def symp_def transp_def |
173 apply(simp_all) |
174 apply(simp_all) |
|
175 (* refl *) |
174 apply(clarify) |
176 apply(clarify) |
175 apply(rule exI) |
177 apply(rule exI) |
176 apply(rule alpha_gen_refl) |
178 apply(rule alpha_gen_refl) |
177 apply(simp) |
179 apply(simp) |
|
180 (* symm *) |
178 apply(clarify) |
181 apply(clarify) |
179 apply(rule exI) |
182 apply(rule exI) |
180 apply(rule alpha_gen_sym) |
183 apply(rule alpha_gen_sym) |
181 apply(assumption) |
184 apply(assumption) |
182 apply(clarsimp) |
185 apply(clarsimp) |
|
186 (* trans *) |
183 apply(clarify) |
187 apply(clarify) |
184 apply(rule exI) |
188 apply(rule exI) |
185 apply(rule alpha_gen_trans) |
189 apply(rule alpha_gen_trans) |
186 apply(assumption) |
190 apply(assumption) |
187 apply(assumption) |
191 apply(assumption) |