1 theory Abs |
1 theory Abs |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product" |
2 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "../Quotient" "../Quotient_Product" |
3 begin |
3 begin |
4 |
4 |
5 (* the next three lemmas that should be in Nominal \<dots>\<dots>must be cleaned *) |
5 lemma permute_boolI: |
6 |
6 fixes P::"bool" |
|
7 shows "p \<bullet> P \<Longrightarrow> P" |
|
8 apply(simp add: permute_bool_def) |
|
9 done |
|
10 |
|
11 lemma permute_boolE: |
|
12 fixes P::"bool" |
|
13 shows "P \<Longrightarrow> p \<bullet> P" |
|
14 apply(simp add: permute_bool_def) |
|
15 done |
|
16 |
|
17 fun |
|
18 alpha_tst |
|
19 where |
|
20 alpha_tst[simp del]: |
|
21 "alpha_tst (bs, x) R bv bv' fv p (cs, y) \<longleftrightarrow> |
|
22 fv x - bv bs = fv y - bv' cs \<and> |
|
23 (fv x - bv bs) \<sharp>* p \<and> |
|
24 R (p \<bullet> x) y \<and> |
|
25 (p \<bullet> bv bs) = bv' cs" |
|
26 |
|
27 notation |
|
28 alpha_tst ("_ \<approx>tst _ _ _ _ _ _" [100, 100, 100, 100, 100, 100] 100) |
|
29 |
|
30 (* |
|
31 fun |
|
32 alpha_tst_rec |
|
33 where |
|
34 alpha_tst_rec[simp del]: |
|
35 "alpha_tst_rec (bs, x) R1 R2 bv fv p (cs, y) \<longleftrightarrow> |
|
36 fv x - bv bs = fv y - bv cs \<and> |
|
37 (fv x - bv bs) \<sharp>* p \<and> |
|
38 R1 (p \<bullet> x) y \<and> |
|
39 R2 (p \<bullet> bs) cs \<and> |
|
40 (p \<bullet> bv bs) = bv cs" |
|
41 |
|
42 notation |
|
43 alpha_tst_rec ("_ \<approx>tstrec _ _ _ _ _ _" [100, 100, 100, 100, 100, 100] 100) |
|
44 *) |
7 |
45 |
8 fun |
46 fun |
9 alpha_gen |
47 alpha_gen |
10 where |
48 where |
11 alpha_gen[simp del]: |
49 alpha_gen[simp del]: |
12 "alpha_gen (bs, x) R f pi (cs, y) \<longleftrightarrow> |
50 "alpha_gen (bs, x) R fv pi (cs, y) \<longleftrightarrow> |
13 f x - bs = f y - cs \<and> (f x - bs) \<sharp>* pi \<and> R (pi \<bullet> x) y \<and> pi \<bullet> bs = cs" |
51 fv x - bs = fv y - cs \<and> (fv x - bs) \<sharp>* pi \<and> R (pi \<bullet> x) y \<and> pi \<bullet> bs = cs" |
14 |
52 |
15 notation |
53 notation |
16 alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100) |
54 alpha_gen ("_ \<approx>gen _ _ _ _" [100, 100, 100, 100, 100] 100) |
17 |
55 |
18 lemma [mono]: "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2" |
56 fun |
19 by (cases x) (auto simp add: le_fun_def le_bool_def alpha_gen.simps) |
57 alpha_res |
|
58 where |
|
59 alpha_res[simp del]: |
|
60 "alpha_res (bs, x) R fv pi (cs, y) \<longleftrightarrow> |
|
61 fv x - bs = fv y - cs \<and> (fv x - bs) \<sharp>* pi \<and> R (pi \<bullet> x) y" |
|
62 |
|
63 notation |
|
64 alpha_res ("_ \<approx>res _ _ _ _" [100, 100, 100, 100, 100] 100) |
|
65 |
|
66 fun |
|
67 alpha_lst |
|
68 where |
|
69 alpha_lst[simp del]: |
|
70 "alpha_lst (bs, x) R fv pi (cs, y) \<longleftrightarrow> |
|
71 fv x - set bs = fv y - set cs \<and> (fv x - set bs) \<sharp>* pi \<and> R (pi \<bullet> x) y" |
|
72 |
|
73 notation |
|
74 alpha_lst ("_ \<approx>lst _ _ _ _" [100, 100, 100, 100, 100] 100) |
|
75 |
|
76 |
|
77 lemma [mono]: |
|
78 shows "R1 \<le> R2 \<Longrightarrow> alpha_gen x R1 \<le> alpha_gen x R2" |
|
79 and "R1 \<le> R2 \<Longrightarrow> alpha_res x R1 \<le> alpha_res x R2" |
|
80 apply(case_tac [!] x) |
|
81 apply(auto simp add: le_fun_def le_bool_def alpha_gen.simps alpha_res.simps) |
|
82 done |
20 |
83 |
21 lemma alpha_gen_refl: |
84 lemma alpha_gen_refl: |
22 assumes a: "R x x" |
85 assumes a: "R x x" |
23 shows "(bs, x) \<approx>gen R f 0 (bs, x)" |
86 shows "(bs, x) \<approx>gen R fv 0 (bs, x)" |
24 using a by (simp add: alpha_gen fresh_star_def fresh_zero_perm) |
87 using a by (simp add: alpha_gen fresh_star_def fresh_zero_perm) |
25 |
88 |
|
89 lemma alpha_gen_refl_tst: |
|
90 assumes a: "R1 x x" "bv bs = bv' bs" |
|
91 shows "(bs, x) \<approx>tst R1 bv bv' fv 0 (bs, x)" |
|
92 using a |
|
93 apply (simp add: alpha_tst fresh_star_def fresh_zero_perm) |
|
94 done |
|
95 |
|
96 |
26 lemma alpha_gen_sym: |
97 lemma alpha_gen_sym: |
27 assumes a: "(bs, x) \<approx>gen R f p (cs, y)" |
98 assumes a: "(bs, x) \<approx>gen R fv p (cs, y)" |
28 and b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x" |
99 and b: "R (p \<bullet> x) y \<Longrightarrow> R (- p \<bullet> y) x" |
29 shows "(cs, y) \<approx>gen R f (- p) (bs, x)" |
100 shows "(cs, y) \<approx>gen R fv (- p) (bs, x)" |
30 using a b |
101 using a |
31 by (auto simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm) |
102 apply(auto simp add: alpha_gen fresh_star_def fresh_def supp_minus_perm) |
|
103 apply(simp add: b) |
|
104 done |
|
105 |
|
106 lemma alpha_gen_sym_tst: |
|
107 assumes a: "(bs, x) \<approx>tst R1 bv bv' fv p (cs, y)" |
|
108 and b: "R1 (p \<bullet> x) y \<Longrightarrow> R1 (- p \<bullet> y) x" |
|
109 shows "(cs, y) \<approx>tst R1 bv' bv fv (- p) (bs, x)" |
|
110 using a |
|
111 apply(auto simp add: alpha_tst fresh_star_def fresh_def supp_minus_perm) |
|
112 apply(simp add: b) |
|
113 apply(rule_tac p="p" in permute_boolI) |
|
114 apply(simp add: mem_eqvt) |
|
115 apply(rule_tac p="- p" in permute_boolI) |
|
116 apply(simp add: mem_eqvt) |
|
117 apply(rotate_tac 3) |
|
118 apply(drule sym) |
|
119 apply(simp) |
|
120 done |
32 |
121 |
33 lemma alpha_gen_trans: |
122 lemma alpha_gen_trans: |
34 assumes a: "(bs, x) \<approx>gen R f p1 (cs, y)" |
123 assumes a: "(bs, x) \<approx>gen R fv p (cs, y)" |
35 and b: "(cs, y) \<approx>gen R f p2 (ds, z)" |
124 and b: "(cs, y) \<approx>gen R fv q (ds, z)" |
36 and c: "\<lbrakk>R (p1 \<bullet> x) y; R (p2 \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((p2 + p1) \<bullet> x) z" |
125 and c: "\<lbrakk>R (p \<bullet> x) y; R (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R ((q + p) \<bullet> x) z" |
37 shows "(bs, x) \<approx>gen R f (p2 + p1) (ds, z)" |
126 shows "(bs, x) \<approx>gen R fv (q + p) (ds, z)" |
38 using a b c |
127 using a b c |
39 using supp_plus_perm |
128 using supp_plus_perm |
40 apply(simp add: alpha_gen fresh_star_def fresh_def) |
129 apply(simp add: alpha_gen fresh_star_def fresh_def) |
|
130 apply(blast) |
|
131 done |
|
132 |
|
133 lemma alpha_gen_trans_tst: |
|
134 assumes a: "(bs, x) \<approx>tst R1 bv bv' fv p (cs, y)" |
|
135 and b: "(cs, y) \<approx>tst R1 bv' bv'' fv q (ds, z)" |
|
136 and c: "\<lbrakk>R1 (p \<bullet> x) y; R1 (q \<bullet> y) z\<rbrakk> \<Longrightarrow> R1 ((q + p) \<bullet> x) z" |
|
137 shows "(bs, x) \<approx>tst R1 bv bv'' fv (q + p) (ds, z)" |
|
138 using a b c |
|
139 using supp_plus_perm |
|
140 apply(simp add: alpha_tst fresh_star_def fresh_def) |
41 apply(blast) |
141 apply(blast) |
42 done |
142 done |
43 |
143 |
44 lemma alpha_gen_eqvt: |
144 lemma alpha_gen_eqvt: |
45 assumes a: "(bs, x) \<approx>gen R f q (cs, y)" |
145 assumes a: "(bs, x) \<approx>gen R f q (cs, y)" |
52 apply(simp add: permute_eqvt[symmetric]) |
152 apply(simp add: permute_eqvt[symmetric]) |
53 apply(simp add: fresh_star_permute_iff) |
153 apply(simp add: fresh_star_permute_iff) |
54 apply(clarsimp) |
154 apply(clarsimp) |
55 done |
155 done |
56 |
156 |
57 lemma alpha_gen_compose_sym: |
157 lemma alpha_gen_eqvt_tst: |
58 fixes pi |
158 assumes a: "(bs, x) \<approx>tst R1 bv bv' fv q (cs, y)" |
59 assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)" |
159 and b1: "R1 (q \<bullet> x) y \<Longrightarrow> R1 (p \<bullet> (q \<bullet> x)) (p \<bullet> y)" |
60 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
160 and c: "p \<bullet> (fv x) = fv (p \<bullet> x)" |
61 shows "(ab, s) \<approx>gen R f (- pi) (aa, t)" |
161 and d: "p \<bullet> (fv y) = fv (p \<bullet> y)" |
62 using b apply - |
162 and e: "p \<bullet> (bv bs) = bv (p \<bullet> bs)" |
63 apply(simp add: alpha_gen.simps) |
163 and f: "p \<bullet> (bv cs) = bv (p \<bullet> cs)" |
64 apply(erule conjE)+ |
164 and e': "p \<bullet> (bv' bs) = bv' (p \<bullet> bs)" |
65 apply(rule conjI) |
165 and f': "p \<bullet> (bv' cs) = bv' (p \<bullet> cs)" |
66 apply(simp add: fresh_star_def fresh_minus_perm) |
166 shows "(p \<bullet> bs, p \<bullet> x) \<approx>tst R1 bv bv' fv (p \<bullet> q) (p \<bullet> cs, p \<bullet> y)" |
67 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
167 using a b1 |
68 apply simp |
168 apply(simp add: alpha_tst c[symmetric] d[symmetric] |
69 apply(clarify) |
169 e'[symmetric] f'[symmetric] e[symmetric] f[symmetric] Diff_eqvt[symmetric]) |
70 apply(simp) |
170 apply(simp add: permute_eqvt[symmetric]) |
71 apply(rule a) |
171 apply(simp add: fresh_star_permute_iff) |
72 apply assumption |
172 apply(clarsimp) |
73 done |
173 done |
74 |
|
75 lemma alpha_gen_compose_trans: |
|
76 fixes pi pia |
|
77 assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)" |
|
78 and c: "(ab, ta) \<approx>gen R f pia (ac, sa)" |
|
79 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
|
80 shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)" |
|
81 using b c apply - |
|
82 apply(simp add: alpha_gen.simps) |
|
83 apply(erule conjE)+ |
|
84 apply(simp add: fresh_star_plus) |
|
85 apply(drule_tac x="- pia \<bullet> sa" in spec) |
|
86 apply(drule mp) |
|
87 apply(rotate_tac 5) |
|
88 apply(drule_tac pi="- pia" in a) |
|
89 apply(simp) |
|
90 apply(rotate_tac 7) |
|
91 apply(drule_tac pi="pia" in a) |
|
92 apply(simp) |
|
93 done |
|
94 |
|
95 lemma alpha_gen_compose_eqvt: |
|
96 fixes pia |
|
97 assumes b: "(g d, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia (g e, s)" |
|
98 and c: "\<And>y. pi \<bullet> (g y) = g (pi \<bullet> y)" |
|
99 and a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)" |
|
100 shows "(g (pi \<bullet> d), pi \<bullet> t) \<approx>gen R f (pi \<bullet> pia) (g (pi \<bullet> e), pi \<bullet> s)" |
|
101 using b |
|
102 apply - |
|
103 apply(simp add: alpha_gen.simps) |
|
104 apply(erule conjE)+ |
|
105 apply(rule conjI) |
|
106 apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1]) |
|
107 apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric]) |
|
108 apply(rule conjI) |
|
109 apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1]) |
|
110 apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt c[symmetric]) |
|
111 apply(subst permute_eqvt[symmetric]) |
|
112 apply(simp) |
|
113 oops |
|
114 |
174 |
115 fun |
175 fun |
116 alpha_abs |
176 alpha_abs |
117 where |
177 where |
118 "alpha_abs (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))" |
178 "alpha_abs (bs, x) (cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))" |
119 |
179 |
120 notation |
180 notation |
121 alpha_abs ("_ \<approx>abs _") |
181 alpha_abs ("_ \<approx>abs _") |
|
182 |
|
183 fun |
|
184 alpha_abs_tst |
|
185 where |
|
186 "alpha_abs_tst (bv, bs, x) (bv',cs, y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>tst (op=) bv bv' supp p (cs, y))" |
|
187 |
|
188 notation |
|
189 alpha_abs_tst ("_ \<approx>abstst _") |
122 |
190 |
123 lemma alpha_abs_swap: |
191 lemma alpha_abs_swap: |
124 assumes a1: "a \<notin> (supp x) - bs" |
192 assumes a1: "a \<notin> (supp x) - bs" |
125 and a2: "b \<notin> (supp x) - bs" |
193 and a2: "b \<notin> (supp x) - bs" |
126 shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)" |
194 shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)" |
135 apply(simp add: fresh_star_def fresh_def) |
203 apply(simp add: fresh_star_def fresh_def) |
136 apply(blast) |
204 apply(blast) |
137 apply(simp add: supp_swap) |
205 apply(simp add: supp_swap) |
138 done |
206 done |
139 |
207 |
140 lemma alpha_gen_swap_fun: |
208 lemma alpha_abs_tst_swap: |
141 assumes f_eqvt: "\<And>pi. (pi \<bullet> (f x)) = f (pi \<bullet> x)" |
209 assumes a1: "a \<notin> (supp x) - bv bs" |
142 assumes a1: "a \<notin> (f x) - bs" |
210 and a2: "b \<notin> (supp x) - bv bs" |
143 and a2: "b \<notin> (f x) - bs" |
211 shows "(bv, bs, x) \<approx>abstst ((a \<rightleftharpoons> b) \<bullet> bv, (a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)" |
144 shows "\<exists>pi. (bs, x) \<approx>gen (op=) f pi ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)" |
212 apply(simp) |
145 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI) |
213 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI) |
146 apply(simp add: alpha_gen) |
214 unfolding alpha_tst |
147 apply(simp add: f_eqvt[symmetric] Diff_eqvt[symmetric]) |
215 apply(simp) |
|
216 apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric] eqvt_apply[symmetric]) |
148 apply(simp add: swap_set_not_in[OF a1 a2]) |
217 apply(simp add: swap_set_not_in[OF a1 a2]) |
149 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}") |
218 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}") |
150 using a1 a2 |
219 using a1 a2 |
151 apply(simp add: fresh_star_def fresh_def) |
220 apply(simp add: fresh_star_def fresh_def) |
152 apply(blast) |
221 apply(blast) |
153 apply(simp add: supp_swap) |
222 apply(simp add: supp_swap) |
154 done |
223 done |
155 |
224 |
156 fun |
225 fun |
157 supp_abs_fun |
226 supp_abs_fun |
158 where |
227 where |
159 "supp_abs_fun (bs, x) = (supp x) - bs" |
228 "supp_abs_fun (bs, x) = (supp x) - bs" |
|
229 |
|
230 fun |
|
231 supp_abstst_fun::"('b::pt \<Rightarrow> atom set) \<times> 'b \<times> ('a::pt) \<Rightarrow> atom set" |
|
232 where |
|
233 "supp_abstst_fun (bv, bs, x) = (supp x - bv bs)" |
160 |
234 |
161 lemma supp_abs_fun_lemma: |
235 lemma supp_abs_fun_lemma: |
162 assumes a: "x \<approx>abs y" |
236 assumes a: "x \<approx>abs y" |
163 shows "supp_abs_fun x = supp_abs_fun y" |
237 shows "supp_abs_fun x = supp_abs_fun y" |
164 using a |
238 using a |
165 apply(induct rule: alpha_abs.induct) |
239 apply(induct rule: alpha_abs.induct) |
166 apply(simp add: alpha_gen) |
240 apply(simp add: alpha_gen) |
|
241 done |
|
242 |
|
243 lemma supp_abstst_fun_lemma: |
|
244 assumes a: "(bv, bs, x) \<approx>abstst (bv', cs, y)" |
|
245 shows "supp_abstst_fun (bv, bs, x) = supp_abstst_fun (bv', cs, y)" |
|
246 using a |
|
247 apply(induct x\<equiv>"(bv, bs, x)" y\<equiv>"(bv', cs, y)" rule: alpha_abs_tst.induct) |
|
248 apply(simp add: alpha_tst) |
167 done |
249 done |
168 |
250 |
169 quotient_type 'a abs = "(atom set \<times> 'a::pt)" / "alpha_abs" |
251 quotient_type 'a abs = "(atom set \<times> 'a::pt)" / "alpha_abs" |
170 apply(rule equivpI) |
252 apply(rule equivpI) |
171 unfolding reflp_def symp_def transp_def |
253 unfolding reflp_def symp_def transp_def |
188 apply(assumption) |
270 apply(assumption) |
189 apply(assumption) |
271 apply(assumption) |
190 apply(simp) |
272 apply(simp) |
191 done |
273 done |
192 |
274 |
|
275 term "alpha_abs_tst" |
|
276 |
|
277 quotient_type ('a,'b) abs_tst = "(('a \<Rightarrow>atom set) \<times> 'a::pt \<times> 'b::pt)" / "alpha_abs_tst" |
|
278 apply(rule equivpI) |
|
279 unfolding reflp_def symp_def transp_def |
|
280 apply(simp_all) |
|
281 (* refl *) |
|
282 apply(clarify) |
|
283 apply(rule exI) |
|
284 apply(rule alpha_gen_refl_tst) |
|
285 apply(simp) |
|
286 apply(simp) |
|
287 (* symm *) |
|
288 apply(clarify) |
|
289 apply(rule exI) |
|
290 apply(rule alpha_gen_sym_tst) |
|
291 apply(assumption) |
|
292 apply(clarsimp) |
|
293 (* trans *) |
|
294 apply(clarify) |
|
295 apply(rule exI) |
|
296 apply(rule alpha_gen_trans_tst) |
|
297 apply(assumption) |
|
298 apply(assumption) |
|
299 apply(simp) |
|
300 done |
|
301 |
|
302 |
193 quotient_definition |
303 quotient_definition |
194 "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs" |
304 "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs" |
195 is |
305 is |
196 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" |
306 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" |
|
307 |
|
308 fun |
|
309 Pair_tst |
|
310 where |
|
311 "Pair_tst a b c = (a, b, c)" |
|
312 |
|
313 quotient_definition |
|
314 "Abs_tst::('b::pt \<Rightarrow> atom set) \<Rightarrow> 'b \<Rightarrow> ('a::pt) \<Rightarrow> ('b, 'a) abs_tst" |
|
315 is |
|
316 "Pair_tst::('b::pt \<Rightarrow> atom set) \<Rightarrow> 'b \<Rightarrow> ('a::pt) \<Rightarrow> (('b \<Rightarrow> atom set) \<times> 'b \<times> 'a)" |
197 |
317 |
198 lemma [quot_respect]: |
318 lemma [quot_respect]: |
199 shows "((op =) ===> (op =) ===> alpha_abs) Pair Pair" |
319 shows "((op =) ===> (op =) ===> alpha_abs) Pair Pair" |
200 apply(clarsimp) |
320 apply(clarsimp) |
201 apply(rule exI) |
321 apply(rule exI) |
202 apply(rule alpha_gen_refl) |
322 apply(rule alpha_gen_refl) |
203 apply(simp) |
323 apply(simp) |
|
324 done |
|
325 |
|
326 lemma [quot_respect]: |
|
327 shows "((op =) ===> (op =) ===> (op =) ===> alpha_abs_tst) Pair_tst Pair_tst" |
|
328 apply(clarsimp) |
|
329 apply(rule exI) |
|
330 apply(rule alpha_gen_refl_tst) |
|
331 apply(simp_all) |
|
332 done |
|
333 |
|
334 lemma [quot_respect]: |
|
335 shows "((op =) ===> (op =) ===> (op =) ===> alpha_abs_tst) Pair_tst Pair_tst" |
|
336 apply(clarsimp) |
|
337 apply(rule exI) |
|
338 apply(rule alpha_gen_refl_tst) |
|
339 apply(simp_all) |
204 done |
340 done |
205 |
341 |
206 lemma [quot_respect]: |
342 lemma [quot_respect]: |
207 shows "((op =) ===> alpha_abs ===> alpha_abs) permute permute" |
343 shows "((op =) ===> alpha_abs ===> alpha_abs) permute permute" |
208 apply(clarsimp) |
344 apply(clarsimp) |
245 apply(simp_all) |
393 apply(simp_all) |
246 done |
394 done |
247 |
395 |
248 end |
396 end |
249 |
397 |
|
398 instantiation abs_tst :: (pt, pt) pt |
|
399 begin |
|
400 |
|
401 quotient_definition |
|
402 "permute_abs_tst::perm \<Rightarrow> (('a::pt, 'b::pt) abs_tst) \<Rightarrow> ('a, 'b) abs_tst" |
|
403 is |
|
404 "permute:: perm \<Rightarrow> ((('a::pt) \<Rightarrow> atom set) \<times> 'a \<times> 'b::pt) \<Rightarrow> (('a \<Rightarrow> atom set) \<times> 'a \<times> 'b)" |
|
405 |
|
406 lemma permute_ABS_tst [simp]: |
|
407 fixes x::"'a::pt" |
|
408 shows "(p \<bullet> (Abs_tst bv as x)) = Abs_tst (p \<bullet> bv) (p \<bullet> as) (p \<bullet> x)" |
|
409 sorry |
|
410 |
|
411 instance |
|
412 apply(default) |
|
413 apply(induct_tac [!] x rule: abs_tst_induct) |
|
414 apply(simp_all) |
|
415 done |
|
416 |
|
417 end |
|
418 |
250 quotient_definition |
419 quotient_definition |
251 "supp_Abs_fun :: ('a::pt) abs \<Rightarrow> atom \<Rightarrow> bool" |
420 "supp_Abs_fun :: ('a::pt) abs \<Rightarrow> atom \<Rightarrow> bool" |
252 is |
421 is |
253 "supp_abs_fun" |
422 "supp_abs_fun" |
254 |
423 |
|
424 term supp_abstst_fun |
|
425 |
|
426 quotient_definition |
|
427 "supp_Abstst_fun :: ('a::pt, 'b::pt) abs_tst \<Rightarrow> atom \<Rightarrow> bool" |
|
428 is |
|
429 "supp_abstst_fun :: (('a::pt \<Rightarrow> atom \<Rightarrow> bool) \<times> 'a \<times> 'b::pt) \<Rightarrow> atom \<Rightarrow> bool" |
|
430 (* leave out type *) |
|
431 |
255 lemma supp_Abs_fun_simp: |
432 lemma supp_Abs_fun_simp: |
256 shows "supp_Abs_fun (Abs bs x) = (supp x) - bs" |
433 shows "supp_Abs_fun (Abs bs x) = (supp x) - bs" |
257 by (lifting supp_abs_fun.simps(1)) |
434 by (lifting supp_abs_fun.simps(1)) |
|
435 thm supp_abs_fun.simps(1) |
|
436 |
|
437 term supp_Abs_fun |
|
438 term supp_Abstst_fun |
|
439 |
|
440 lemma supp_Abs_tst_fun_simp: |
|
441 fixes bv::"'b::pt \<Rightarrow> atom set" |
|
442 shows "supp_Abstst_fun (Abs_tst bv bs x) = (supp x) - (bv bs)" |
|
443 sorry |
|
444 (* PROBLEM: regularisation fails |
|
445 by (lifting supp_abstst_fun.simps(1)) |
|
446 *) |
|
447 |
258 |
448 |
259 lemma supp_Abs_fun_eqvt [eqvt]: |
449 lemma supp_Abs_fun_eqvt [eqvt]: |
260 shows "(p \<bullet> supp_Abs_fun x) = supp_Abs_fun (p \<bullet> x)" |
450 shows "(p \<bullet> supp_Abs_fun x) = supp_Abs_fun (p \<bullet> x)" |
261 apply(induct_tac x rule: abs_induct) |
451 apply(induct_tac x rule: abs_induct) |
262 apply(simp add: supp_Abs_fun_simp supp_eqvt Diff_eqvt) |
452 apply(simp add: supp_Abs_fun_simp supp_eqvt Diff_eqvt) |
263 done |
453 done |
264 |
454 |
|
455 lemma supp_Abs_test_fun_eqvt [eqvt]: |
|
456 shows "(p \<bullet> supp_Abstst_fun x) = supp_Abstst_fun (p \<bullet> x)" |
|
457 apply(induct_tac x rule: abs_tst_induct) |
|
458 apply(simp add: supp_Abs_tst_fun_simp supp_eqvt Diff_eqvt) |
|
459 apply(simp add: eqvt_apply) |
|
460 done |
|
461 |
265 lemma supp_Abs_fun_fresh: |
462 lemma supp_Abs_fun_fresh: |
266 shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_Abs_fun (Abs bs x)" |
463 shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_Abs_fun (Abs bs x)" |
267 apply(rule fresh_fun_eqvt_app) |
464 apply(rule fresh_fun_eqvt_app) |
268 apply(simp add: eqvts_raw) |
465 apply(simp add: eqvts_raw) |
269 apply(simp) |
466 apply(simp) |
270 done |
467 done |
271 |
468 |
|
469 |
|
470 lemma supp_Abs_tst_fun_fresh: |
|
471 shows "a \<sharp> Abs_tst bv bs x \<Longrightarrow> a \<sharp> supp_Abstst_fun (Abs_tst bv bs x)" |
|
472 apply(rule fresh_fun_eqvt_app) |
|
473 apply(simp add: eqvts_raw) |
|
474 apply(simp) |
|
475 done |
|
476 |
272 lemma Abs_swap: |
477 lemma Abs_swap: |
273 assumes a1: "a \<notin> (supp x) - bs" |
478 assumes a1: "a \<notin> (supp x) - bs" |
274 and a2: "b \<notin> (supp x) - bs" |
479 and a2: "b \<notin> (supp x) - bs" |
275 shows "(Abs bs x) = (Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))" |
480 shows "(Abs bs x) = (Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))" |
276 using a1 a2 by (lifting alpha_abs_swap) |
481 using a1 a2 |
|
482 by (lifting alpha_abs_swap) |
|
483 |
|
484 thm alpha_abs_swap |
|
485 thm alpha_abs_tst_swap |
|
486 |
|
487 lemma Abs_tst_swap: |
|
488 assumes a1: "a \<notin> (supp x) - bv bs" |
|
489 and a2: "b \<notin> (supp x) - bv bs" |
|
490 shows "(Abs_tst bv bs x) = (Abs_tst ((a \<rightleftharpoons> b) \<bullet> bv) ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))" |
|
491 using a1 a2 |
|
492 sorry |
|
493 (* PROBLEM |
|
494 by (lifting alpha_abs_tst_swap) |
|
495 *) |
277 |
496 |
278 lemma Abs_supports: |
497 lemma Abs_supports: |
279 shows "((supp x) - as) supports (Abs as x)" |
498 shows "(supp x - as) supports (Abs as x)" |
280 unfolding supports_def |
499 unfolding supports_def |
281 apply(clarify) |
500 apply(clarify) |
282 apply(simp (no_asm)) |
501 apply(simp (no_asm)) |
283 apply(subst Abs_swap[symmetric]) |
502 apply(subst Abs_swap[symmetric]) |
|
503 apply(simp_all) |
|
504 done |
|
505 |
|
506 lemma Abs_tst_supports: |
|
507 shows "(supp x - bv as) supports (Abs_tst bv as x)" |
|
508 unfolding supports_def |
|
509 apply(clarify) |
|
510 apply(simp (no_asm)) |
|
511 apply(subst Abs_tst_swap[symmetric]) |
284 apply(simp_all) |
512 apply(simp_all) |
285 done |
513 done |
286 |
514 |
287 lemma supp_Abs_subset1: |
515 lemma supp_Abs_subset1: |
288 fixes x::"'a::fs" |
516 fixes x::"'a::fs" |
293 apply(simp only: supp_Abs_fun_simp) |
521 apply(simp only: supp_Abs_fun_simp) |
294 apply(simp add: fresh_def) |
522 apply(simp add: fresh_def) |
295 apply(simp add: supp_finite_atom_set finite_supp) |
523 apply(simp add: supp_finite_atom_set finite_supp) |
296 done |
524 done |
297 |
525 |
|
526 lemma supp_Abs_tst_subset1: |
|
527 fixes x::"'a::fs" |
|
528 shows "(supp x - bv as) \<subseteq> supp (Abs_tst bv as x)" |
|
529 apply(simp add: supp_conv_fresh) |
|
530 apply(auto) |
|
531 apply(drule_tac supp_Abs_tst_fun_fresh) |
|
532 apply(simp only: supp_Abs_tst_fun_simp) |
|
533 apply(simp add: fresh_def) |
|
534 apply(simp add: supp_finite_atom_set finite_supp) |
|
535 done |
|
536 |
298 lemma supp_Abs_subset2: |
537 lemma supp_Abs_subset2: |
299 fixes x::"'a::fs" |
538 fixes x::"'a::fs" |
300 shows "supp (Abs as x) \<subseteq> (supp x) - as" |
539 shows "supp (Abs as x) \<subseteq> (supp x) - as" |
301 apply(rule supp_is_subset) |
540 apply(rule supp_is_subset) |
302 apply(rule Abs_supports) |
541 apply(rule Abs_supports) |
303 apply(simp add: finite_supp) |
542 apply(simp add: finite_supp) |
304 done |
543 done |
305 |
544 |
|
545 lemma supp_Abs_tst_subset2: |
|
546 fixes x::"'a::fs" |
|
547 shows "supp (Abs_tst bv as x) \<subseteq> (supp x - bv as)" |
|
548 apply(rule supp_is_subset) |
|
549 apply(rule Abs_tst_supports) |
|
550 apply(simp add: finite_supp) |
|
551 done |
|
552 |
306 lemma supp_Abs: |
553 lemma supp_Abs: |
307 fixes x::"'a::fs" |
554 fixes x::"'a::fs" |
308 shows "supp (Abs as x) = (supp x) - as" |
555 shows "supp (Abs as x) = (supp x) - as" |
309 apply(rule_tac subset_antisym) |
556 apply(rule_tac subset_antisym) |
310 apply(rule supp_Abs_subset2) |
557 apply(rule supp_Abs_subset2) |
311 apply(rule supp_Abs_subset1) |
558 apply(rule supp_Abs_subset1) |
312 done |
559 done |
313 |
560 |
|
561 lemma supp_Abs_tst: |
|
562 fixes x::"'a::fs" |
|
563 shows "supp (Abs_tst bv as x) = (supp x - bv as)" |
|
564 apply(rule_tac subset_antisym) |
|
565 apply(rule supp_Abs_tst_subset2) |
|
566 apply(rule supp_Abs_tst_subset1) |
|
567 done |
|
568 |
314 instance abs :: (fs) fs |
569 instance abs :: (fs) fs |
315 apply(default) |
570 apply(default) |
316 apply(induct_tac x rule: abs_induct) |
571 apply(induct_tac x rule: abs_induct) |
317 apply(simp add: supp_Abs) |
572 apply(simp add: supp_Abs) |
|
573 apply(simp add: finite_supp) |
|
574 done |
|
575 |
|
576 instance abs_tst :: (pt, fs) fs |
|
577 apply(default) |
|
578 apply(induct_tac x rule: abs_tst_induct) |
|
579 apply(simp add: supp_Abs_tst) |
318 apply(simp add: finite_supp) |
580 apply(simp add: finite_supp) |
319 done |
581 done |
320 |
582 |
321 lemma Abs_fresh_iff: |
583 lemma Abs_fresh_iff: |
322 fixes x::"'a::fs" |
584 fixes x::"'a::fs" |
344 "alpha1 (a, x) (b, y) \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)" |
622 "alpha1 (a, x) (b, y) \<longleftrightarrow> (a = b \<and> x = y) \<or> (a \<noteq> b \<and> x = (a \<rightleftharpoons> b) \<bullet> y \<and> a \<sharp> y)" |
345 |
623 |
346 notation |
624 notation |
347 alpha1 ("_ \<approx>abs1 _") |
625 alpha1 ("_ \<approx>abs1 _") |
348 |
626 |
349 fun |
|
350 alpha2 |
|
351 where |
|
352 "alpha2 (a, x) (b, y) \<longleftrightarrow> (\<exists>c. c \<sharp> (a,b,x,y) \<and> ((c \<rightleftharpoons> a) \<bullet> x) = ((c \<rightleftharpoons> b) \<bullet> y))" |
|
353 |
|
354 notation |
|
355 alpha2 ("_ \<approx>abs2 _") |
|
356 |
|
357 |
|
358 lemma |
627 lemma |
359 assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b" |
628 assumes a: "(a, x) \<approx>abs1 (b, y)" "sort_of a = sort_of b" |
360 shows "({a}, x) \<approx>abs ({b}, y)" |
629 shows "({a}, x) \<approx>abs ({b}, y)" |
361 using a |
630 using a |
362 apply(simp) |
631 apply(simp) |
363 apply(erule disjE) |
632 apply(erule disjE) |
364 apply(simp) |
633 apply(simp) |
365 apply(rule exI) |
634 apply(rule exI) |
366 apply(rule alpha_gen_refl) |
635 apply(rule alpha_gen_refl) |
367 apply(simp) |
636 apply(simp) |
|
637 apply(simp) |
368 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI) |
638 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI) |
369 apply(simp add: alpha_gen) |
639 apply(simp add: alpha_gen) |
370 apply(simp add: fresh_def) |
640 apply(simp add: fresh_def) |
371 apply(rule conjI) |
641 apply(rule conjI) |
372 apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in permute_eq_iff[THEN iffD1]) |
642 apply(rule_tac p1="(a \<rightleftharpoons> b)" in permute_eq_iff[THEN iffD1]) |
373 apply(rule trans) |
643 apply(rule trans) |
374 apply(simp add: Diff_eqvt supp_eqvt) |
644 apply(simp add: Diff_eqvt supp_eqvt) |
375 apply(subst swap_set_not_in) |
645 apply(subst swap_set_not_in) |
376 back |
646 back |
377 apply(simp) |
647 apply(simp) |
378 apply(simp) |
648 apply(simp) |
379 apply(simp add: permute_set_eq) |
649 apply(simp add: permute_set_eq) |
380 apply(simp add: eqvts) |
650 apply(simp add: eqvts) |
381 apply(rule_tac ?p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1]) |
651 apply(rule_tac p1="(a \<rightleftharpoons> b)" in fresh_star_permute_iff[THEN iffD1]) |
382 apply(simp add: permute_self) |
652 apply(simp add: permute_self) |
383 apply(simp add: Diff_eqvt supp_eqvt) |
653 apply(simp add: Diff_eqvt supp_eqvt) |
384 apply(simp add: permute_set_eq) |
654 apply(simp add: permute_set_eq) |
385 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}") |
655 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}") |
386 apply(simp add: fresh_star_def fresh_def) |
656 apply(simp add: fresh_star_def fresh_def) |
699 apply(simp add: image_eqvt) |
951 apply(simp add: image_eqvt) |
700 apply(simp add: atom_eqvt_raw) |
952 apply(simp add: atom_eqvt_raw) |
701 apply(simp add: atom_image_cong) |
953 apply(simp add: atom_image_cong) |
702 done |
954 done |
703 |
955 |
704 lemma swap_atom_image_fresh: "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn" |
956 lemma swap_atom_image_fresh: |
705 apply (simp add: fresh_def) |
957 "\<lbrakk>a \<sharp> atom ` (fn :: ('a :: at_base set)); b \<sharp> atom ` fn\<rbrakk> \<Longrightarrow> (a \<rightleftharpoons> b) \<bullet> fn = fn" |
706 apply (simp add: supp_atom_image) |
958 apply (simp add: fresh_def) |
707 apply (fold fresh_def) |
959 apply (simp add: supp_atom_image) |
708 apply (simp add: swap_fresh_fresh) |
960 apply (fold fresh_def) |
|
961 apply (simp add: swap_fresh_fresh) |
|
962 done |
|
963 |
|
964 |
|
965 (******************************************************) |
|
966 lemma alpha_gen_compose_sym: |
|
967 fixes pi |
|
968 assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R x2 x1) f pi (ab, s)" |
|
969 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
|
970 shows "(ab, s) \<approx>gen R f (- pi) (aa, t)" |
|
971 using b |
|
972 apply - |
|
973 apply(simp add: alpha_gen.simps) |
|
974 apply(erule conjE)+ |
|
975 apply(rule conjI) |
|
976 apply(simp add: fresh_star_def fresh_minus_perm) |
|
977 apply(subgoal_tac "R (- pi \<bullet> s) ((- pi) \<bullet> (pi \<bullet> t))") |
|
978 apply simp |
|
979 apply(clarsimp) |
|
980 apply(rule a) |
|
981 apply assumption |
|
982 done |
|
983 |
|
984 lemma alpha_gen_compose_trans: |
|
985 fixes pi pia |
|
986 assumes b: "(aa, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> (\<forall>x. R x2 x \<longrightarrow> R x1 x)) f pi (ab, ta)" |
|
987 and c: "(ab, ta) \<approx>gen R f pia (ac, sa)" |
|
988 and a: "\<And>pi t s. (R t s \<Longrightarrow> R (pi \<bullet> t) (pi \<bullet> s))" |
|
989 shows "(aa, t) \<approx>gen R f (pia + pi) (ac, sa)" |
|
990 using b c apply - |
|
991 apply(simp add: alpha_gen.simps) |
|
992 apply(erule conjE)+ |
|
993 apply(simp add: fresh_star_plus) |
|
994 apply(drule_tac x="- pia \<bullet> sa" in spec) |
|
995 apply(drule mp) |
|
996 apply(rotate_tac 5) |
|
997 apply(drule_tac pi="- pia" in a) |
|
998 apply(simp) |
|
999 apply(rotate_tac 7) |
|
1000 apply(drule_tac pi="pia" in a) |
|
1001 apply(simp) |
709 done |
1002 done |
710 |
1003 |
711 |
1004 |
712 end |
1005 end |
713 |
1006 |