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