78 "alpha_abs (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))" |
78 "alpha_abs (bs, x) (cs, y) = (\<exists>p. (bs, x) \<approx>gen (op=) supp p (cs, y))" |
79 |
79 |
80 notation |
80 notation |
81 alpha_abs ("_ \<approx>abs _") |
81 alpha_abs ("_ \<approx>abs _") |
82 |
82 |
83 lemma test1: |
83 lemma alpha_abs_swap: |
84 assumes a1: "a \<notin> (supp x) - bs" |
84 assumes a1: "a \<notin> (supp x) - bs" |
85 and a2: "b \<notin> (supp x) - bs" |
85 and a2: "b \<notin> (supp x) - bs" |
86 shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)" |
86 shows "(bs, x) \<approx>abs ((a \<rightleftharpoons> b) \<bullet> bs, (a \<rightleftharpoons> b) \<bullet> x)" |
87 apply(simp) |
87 apply(simp) |
88 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI) |
88 apply(rule_tac x="(a \<rightleftharpoons> b)" in exI) |
89 apply(simp add: alpha_gen) |
89 apply(simp add: alpha_gen) |
90 apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric]) |
90 apply(simp add: supp_eqvt[symmetric] Diff_eqvt[symmetric]) |
91 apply(simp add: swap_set_fresh[OF a1 a2]) |
91 apply(simp add: swap_set_not_in[OF a1 a2]) |
92 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}") |
92 apply(subgoal_tac "supp (a \<rightleftharpoons> b) \<subseteq> {a, b}") |
93 using a1 a2 |
93 using a1 a2 |
94 apply(simp add: fresh_star_def fresh_def) |
94 apply(simp add: fresh_star_def fresh_def) |
95 apply(blast) |
95 apply(blast) |
96 apply(simp add: supp_swap) |
96 apply(simp add: supp_swap) |
97 done |
97 done |
98 |
98 |
99 fun |
99 fun |
100 s_test |
100 supp_abs_fun |
101 where |
101 where |
102 "s_test (bs, x) = (supp x) - bs" |
102 "supp_abs_fun (bs, x) = (supp x) - bs" |
103 |
103 |
104 lemma s_test_lemma: |
104 lemma supp_abs_fun_lemma: |
105 assumes a: "x \<approx>abs y" |
105 assumes a: "x \<approx>abs y" |
106 shows "s_test x = s_test y" |
106 shows "supp_abs_fun x = supp_abs_fun y" |
107 using a |
107 using a |
108 apply(induct rule: alpha_abs.induct) |
108 apply(induct rule: alpha_abs.induct) |
109 apply(simp add: alpha_gen) |
109 apply(simp add: alpha_gen) |
110 done |
110 done |
111 |
111 |
112 quotient_type 'a abs = "(atom set \<times> 'a::pt)" / "alpha_abs" |
112 quotient_type 'a abs = "(atom set \<times> 'a::pt)" / "alpha_abs" |
113 apply(rule equivpI) |
113 apply(rule equivpI) |
114 unfolding reflp_def symp_def transp_def |
114 unfolding reflp_def symp_def transp_def |
115 apply(simp_all) |
115 apply(simp_all) |
135 as |
135 as |
136 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" |
136 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" |
137 |
137 |
138 lemma [quot_respect]: |
138 lemma [quot_respect]: |
139 shows "((op =) ===> (op =) ===> alpha_abs) Pair Pair" |
139 shows "((op =) ===> (op =) ===> alpha_abs) Pair Pair" |
140 apply(clarsimp) |
140 apply(clarsimp) |
141 apply(rule exI) |
141 apply(rule exI) |
142 apply(rule alpha_gen_refl) |
142 apply(rule alpha_gen_refl) |
143 apply(simp) |
143 apply(simp) |
144 done |
144 done |
145 |
145 |
146 lemma [quot_respect]: |
146 lemma [quot_respect]: |
147 shows "((op =) ===> alpha_abs ===> alpha_abs) permute permute" |
147 shows "((op =) ===> alpha_abs ===> alpha_abs) permute permute" |
148 apply(clarsimp) |
148 apply(clarsimp) |
149 apply(rule exI) |
149 apply(rule exI) |
150 apply(rule alpha_gen_eqvt) |
150 apply(rule alpha_gen_eqvt) |
151 apply(assumption) |
151 apply(assumption) |
152 apply(simp_all add: supp_eqvt) |
152 apply(simp_all add: supp_eqvt) |
153 done |
153 done |
154 |
154 |
155 lemma [quot_respect]: |
155 lemma [quot_respect]: |
156 shows "(alpha_abs ===> (op =)) s_test s_test" |
156 shows "(alpha_abs ===> (op =)) supp_abs_fun supp_abs_fun" |
157 apply(simp add: s_test_lemma) |
157 apply(simp add: supp_abs_fun_lemma) |
158 done |
158 done |
159 |
159 |
160 lemma abs_induct: |
160 lemma abs_induct: |
161 "\<lbrakk>\<And>as (x::'a::pt). P (Abs as x)\<rbrakk> \<Longrightarrow> P t" |
161 "\<lbrakk>\<And>as (x::'a::pt). P (Abs as x)\<rbrakk> \<Longrightarrow> P t" |
162 apply(lifting prod.induct[where 'a="atom set" and 'b="'a"]) |
162 apply(lifting prod.induct[where 'a="atom set" and 'b="'a"]) |
163 done |
163 done |
164 |
164 |
165 instantiation abs :: (pt) pt |
165 instantiation abs :: (pt) pt |
166 begin |
166 begin |
167 |
167 |
168 quotient_definition |
168 quotient_definition |
171 "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)" |
171 "permute:: perm \<Rightarrow> (atom set \<times> 'a::pt) \<Rightarrow> (atom set \<times> 'a::pt)" |
172 |
172 |
173 lemma permute_ABS [simp]: |
173 lemma permute_ABS [simp]: |
174 fixes x::"'a::pt" (* ??? has to be 'a \<dots> 'b does not work *) |
174 fixes x::"'a::pt" (* ??? has to be 'a \<dots> 'b does not work *) |
175 shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)" |
175 shows "(p \<bullet> (Abs as x)) = Abs (p \<bullet> as) (p \<bullet> x)" |
176 apply(lifting permute_prod.simps(1)[where 'a="atom set" and 'b="'a"]) |
176 by (lifting permute_prod.simps(1)[where 'a="atom set" and 'b="'a"]) |
177 done |
|
178 |
177 |
179 instance |
178 instance |
180 apply(default) |
179 apply(default) |
181 apply(induct_tac [!] x rule: abs_induct) |
180 apply(induct_tac [!] x rule: abs_induct) |
182 apply(simp_all) |
181 apply(simp_all) |
183 done |
182 done |
184 |
183 |
185 end |
184 end |
186 |
185 |
187 lemma test1_lifted: |
186 quotient_definition |
|
187 "supp_Abs_fun :: ('a::pt) abs \<Rightarrow> atom \<Rightarrow> bool" |
|
188 as |
|
189 "supp_abs_fun" |
|
190 |
|
191 lemma supp_Abs_fun_simp: |
|
192 shows "supp_Abs_fun (Abs bs x) = (supp x) - bs" |
|
193 by (lifting supp_abs_fun.simps(1)) |
|
194 |
|
195 lemma supp_Abs_fun_eqvt: |
|
196 shows "(p \<bullet> supp_Abs_fun) = supp_Abs_fun" |
|
197 apply(subst permute_fun_def) |
|
198 apply(subst expand_fun_eq) |
|
199 apply(rule allI) |
|
200 apply(induct_tac x rule: abs_induct) |
|
201 apply(simp add: supp_Abs_fun_simp supp_eqvt Diff_eqvt) |
|
202 done |
|
203 |
|
204 lemma supp_Abs_fun_fresh: |
|
205 shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_Abs_fun (Abs bs x)" |
|
206 apply(rule fresh_fun_eqvt_app) |
|
207 apply(simp add: supp_Abs_fun_eqvt) |
|
208 apply(simp) |
|
209 done |
|
210 |
|
211 lemma Abs_swap: |
188 assumes a1: "a \<notin> (supp x) - bs" |
212 assumes a1: "a \<notin> (supp x) - bs" |
189 and a2: "b \<notin> (supp x) - bs" |
213 and a2: "b \<notin> (supp x) - bs" |
190 shows "(Abs bs x) = (Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))" |
214 shows "(Abs bs x) = (Abs ((a \<rightleftharpoons> b) \<bullet> bs) ((a \<rightleftharpoons> b) \<bullet> x))" |
191 using a1 a2 |
215 using a1 a2 by (lifting alpha_abs_swap) |
192 apply(lifting test1) |
|
193 done |
|
194 |
216 |
195 lemma Abs_supports: |
217 lemma Abs_supports: |
196 shows "((supp x) - as) supports (Abs as x)" |
218 shows "((supp x) - as) supports (Abs as x)" |
197 unfolding supports_def |
219 unfolding supports_def |
198 apply(clarify) |
220 apply(clarify) |
199 apply(simp (no_asm)) |
221 apply(simp (no_asm)) |
200 apply(subst test1_lifted[symmetric]) |
222 apply(subst Abs_swap[symmetric]) |
201 apply(simp_all) |
223 apply(simp_all) |
202 done |
224 done |
203 |
225 |
204 quotient_definition |
226 lemma supp_Abs_subset1: |
205 "s_test_lifted :: ('a::pt) abs \<Rightarrow> atom \<Rightarrow> bool" |
227 fixes x::"'a::fs" |
206 as |
228 shows "(supp x) - as \<subseteq> supp (Abs as x)" |
207 "s_test" |
229 apply(simp add: supp_conv_fresh) |
208 |
230 apply(auto) |
209 lemma s_test_lifted_simp: |
231 apply(drule_tac supp_Abs_fun_fresh) |
210 shows "s_test_lifted (Abs bs x) = (supp x) - bs" |
232 apply(simp only: supp_Abs_fun_simp) |
211 apply(lifting s_test.simps(1)) |
233 apply(simp add: fresh_def) |
212 done |
234 apply(simp add: supp_finite_atom_set finite_supp) |
213 |
235 done |
214 lemma s_test_lifted_eqvt: |
236 |
215 shows "(p \<bullet> (s_test_lifted ab)) = s_test_lifted (p \<bullet> ab)" |
237 lemma supp_Abs_subset2: |
216 apply(induct ab rule: abs_induct) |
238 fixes x::"'a::fs" |
217 apply(simp add: s_test_lifted_simp supp_eqvt Diff_eqvt) |
239 shows "supp (Abs as x) \<subseteq> (supp x) - as" |
218 done |
240 apply(rule supp_is_subset) |
219 |
241 apply(rule Abs_supports) |
220 lemma fresh_f_empty_supp: |
242 apply(simp add: finite_supp) |
221 assumes a: "\<forall>p. p \<bullet> f = f" |
243 done |
222 shows "a \<sharp> x \<Longrightarrow> a \<sharp> (f x)" |
|
223 apply(simp add: fresh_def) |
|
224 apply(simp add: supp_def) |
|
225 apply(simp add: permute_fun_app_eq) |
|
226 apply(simp add: a) |
|
227 apply(rule finite_subset) |
|
228 prefer 2 |
|
229 apply(assumption) |
|
230 apply(auto) |
|
231 done |
|
232 |
|
233 |
|
234 lemma s_test_fresh_lemma: |
|
235 shows "(a \<sharp> Abs bs x) \<Longrightarrow> (a \<sharp> s_test_lifted (Abs bs x))" |
|
236 apply(rule fresh_f_empty_supp) |
|
237 apply(rule allI) |
|
238 apply(subst permute_fun_def) |
|
239 apply(simp add: s_test_lifted_eqvt) |
|
240 apply(simp) |
|
241 done |
|
242 |
|
243 |
|
244 lemma supp_finite_set: |
|
245 fixes S::"atom set" |
|
246 assumes "finite S" |
|
247 shows "supp S = S" |
|
248 apply(rule finite_supp_unique) |
|
249 apply(simp add: supports_def) |
|
250 apply(auto simp add: permute_set_eq swap_atom)[1] |
|
251 apply(metis) |
|
252 apply(rule assms) |
|
253 apply(auto simp add: permute_set_eq swap_atom)[1] |
|
254 done |
|
255 |
|
256 lemma s_test_subset: |
|
257 fixes x::"'a::fs" |
|
258 shows "((supp x) - as) \<subseteq> (supp (Abs as x))" |
|
259 apply(rule subsetI) |
|
260 apply(rule contrapos_pp) |
|
261 apply(assumption) |
|
262 unfolding fresh_def[symmetric] |
|
263 thm s_test_fresh_lemma |
|
264 apply(drule_tac s_test_fresh_lemma) |
|
265 apply(simp only: s_test_lifted_simp) |
|
266 apply(simp add: fresh_def) |
|
267 apply(subgoal_tac "finite (supp x - as)") |
|
268 apply(simp add: supp_finite_set) |
|
269 apply(simp add: finite_supp) |
|
270 done |
|
271 |
244 |
272 lemma supp_Abs: |
245 lemma supp_Abs: |
273 fixes x::"'a::fs" |
246 fixes x::"'a::fs" |
274 shows "supp (Abs as x) = (supp x) - as" |
247 shows "supp (Abs as x) = (supp x) - as" |
275 apply(rule subset_antisym) |
248 apply(rule_tac subset_antisym) |
276 apply(rule supp_is_subset) |
249 apply(rule supp_Abs_subset2) |
277 apply(rule Abs_supports) |
250 apply(rule supp_Abs_subset1) |
278 apply(simp add: finite_supp) |
251 done |
279 apply(rule s_test_subset) |
|
280 done |
|
281 |
252 |
282 instance abs :: (fs) fs |
253 instance abs :: (fs) fs |
283 apply(default) |
254 apply(default) |
284 apply(induct_tac x rule: abs_induct) |
255 apply(induct_tac x rule: abs_induct) |
285 apply(simp add: supp_Abs) |
256 apply(simp add: supp_Abs) |
286 apply(simp add: finite_supp) |
257 apply(simp add: finite_supp) |
287 done |
258 done |
288 |
259 |
289 lemma fresh_abs: |
260 lemma Abs_fresh_iff: |
290 fixes x::"'a::fs" |
261 fixes x::"'a::fs" |
291 shows "a \<sharp> Abs bs x = (a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x))" |
262 shows "a \<sharp> Abs bs x = (a \<in> bs \<or> (a \<notin> bs \<and> a \<sharp> x))" |
292 apply(simp add: fresh_def) |
263 apply(simp add: fresh_def) |
293 apply(simp add: supp_Abs) |
264 apply(simp add: supp_Abs) |
294 apply(auto) |
265 apply(auto) |
295 done |
266 done |
296 |
267 |
297 lemma abs_eq: |
268 lemma Abs_eq_iff: |
298 shows "(Abs bs x) = (Abs cs y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
269 shows "(Abs bs x) = (Abs cs y) \<longleftrightarrow> (\<exists>p. (bs, x) \<approx>gen (op =) supp p (cs, y))" |
299 apply(lifting alpha_abs.simps(1)) |
270 by (lifting alpha_abs.simps(1)) |
300 done |
|
301 |
271 |
302 end |
272 end |
303 |
273 |