127 apply(rule_tac [!] equivpI) |
127 apply(rule_tac [!] equivpI) |
128 unfolding reflp_def symp_def transp_def |
128 unfolding reflp_def symp_def transp_def |
129 by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:) |
129 by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:) |
130 |
130 |
131 quotient_definition |
131 quotient_definition |
|
132 Abs ("[_]set. _" [60, 60] 60) |
|
133 where |
132 "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_gen" |
134 "Abs::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_gen" |
133 is |
135 is |
134 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" |
136 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" |
135 |
137 |
136 quotient_definition |
138 quotient_definition |
|
139 Abs_res ("[_]res. _" [60, 60] 60) |
|
140 where |
137 "Abs_res::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_res" |
141 "Abs_res::atom set \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_res" |
138 is |
142 is |
139 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" |
143 "Pair::atom set \<Rightarrow> ('a::pt) \<Rightarrow> (atom set \<times> 'a)" |
140 |
144 |
141 quotient_definition |
145 quotient_definition |
|
146 Abs_lst ("[_]lst. _" [60, 60] 60) |
|
147 where |
142 "Abs_lst::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_lst" |
148 "Abs_lst::atom list \<Rightarrow> ('a::pt) \<Rightarrow> 'a abs_lst" |
143 is |
149 is |
144 "Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)" |
150 "Pair::atom list \<Rightarrow> ('a::pt) \<Rightarrow> (atom list \<times> 'a)" |
145 |
151 |
146 lemma [quot_respect]: |
152 lemma [quot_respect]: |
167 |
173 |
168 lemma abs_eq_iff: |
174 lemma abs_eq_iff: |
169 shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)" |
175 shows "Abs bs x = Abs cs y \<longleftrightarrow> (bs, x) \<approx>abs (cs, y)" |
170 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)" |
176 and "Abs_res bs x = Abs_res cs y \<longleftrightarrow> (bs, x) \<approx>abs_res (cs, y)" |
171 and "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)" |
177 and "Abs_lst ds x = Abs_lst hs y \<longleftrightarrow> (ds, x) \<approx>abs_lst (hs, y)" |
172 apply(simp_all add: alphas_abs) |
178 unfolding alphas_abs |
173 apply(lifting alphas_abs) |
179 by (lifting alphas_abs) |
174 done |
|
175 |
180 |
176 instantiation abs_gen :: (pt) pt |
181 instantiation abs_gen :: (pt) pt |
177 begin |
182 begin |
178 |
183 |
179 quotient_definition |
184 quotient_definition |
325 |
330 |
326 lemma aux_fresh: |
331 lemma aux_fresh: |
327 shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_gen (Abs bs x)" |
332 shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_gen (Abs bs x)" |
328 and "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)" |
333 and "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)" |
329 and "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)" |
334 and "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)" |
330 apply(rule_tac [!] fresh_fun_eqvt_app) |
335 by (rule_tac [!] fresh_fun_eqvt_app) |
331 apply(simp_all add: eqvts_raw) |
336 (simp_all add: eqvts_raw) |
332 done |
|
333 |
337 |
334 lemma supp_abs_subset1: |
338 lemma supp_abs_subset1: |
335 assumes a: "finite (supp x)" |
339 assumes a: "finite (supp x)" |
336 shows "(supp x) - as \<subseteq> supp (Abs as x)" |
340 shows "(supp x) - as \<subseteq> supp (Abs as x)" |
337 and "(supp x) - as \<subseteq> supp (Abs_res as x)" |
341 and "(supp x) - as \<subseteq> supp (Abs_res as x)" |
338 and "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)" |
342 and "(supp x) - (set bs) \<subseteq> supp (Abs_lst bs x)" |
339 unfolding supp_conv_fresh |
343 unfolding supp_conv_fresh |
340 apply(auto dest!: aux_fresh) |
344 by (auto dest!: aux_fresh) |
341 apply(simp_all add: fresh_def supp_finite_atom_set a) |
345 (simp_all add: fresh_def supp_finite_atom_set a) |
342 done |
|
343 |
346 |
344 lemma supp_abs_subset2: |
347 lemma supp_abs_subset2: |
345 assumes a: "finite (supp x)" |
348 assumes a: "finite (supp x)" |
346 shows "supp (Abs as x) \<subseteq> (supp x) - as" |
349 shows "supp (Abs as x) \<subseteq> (supp x) - as" |
347 and "supp (Abs_res as x) \<subseteq> (supp x) - as" |
350 and "supp (Abs_res as x) \<subseteq> (supp x) - as" |
348 and "supp (Abs_lst bs x) \<subseteq> (supp x) - (set bs)" |
351 and "supp (Abs_lst bs x) \<subseteq> (supp x) - (set bs)" |
349 apply(rule_tac [!] supp_is_subset) |
352 by (rule_tac [!] supp_is_subset) |
350 apply(simp_all add: abs_supports a) |
353 (simp_all add: abs_supports a) |
351 done |
|
352 |
354 |
353 lemma abs_finite_supp: |
355 lemma abs_finite_supp: |
354 assumes a: "finite (supp x)" |
356 assumes a: "finite (supp x)" |
355 shows "supp (Abs as x) = (supp x) - as" |
357 shows "supp (Abs as x) = (supp x) - as" |
356 and "supp (Abs_res as x) = (supp x) - as" |
358 and "supp (Abs_res as x) = (supp x) - as" |
357 and "supp (Abs_lst bs x) = (supp x) - (set bs)" |
359 and "supp (Abs_lst bs x) = (supp x) - (set bs)" |
358 apply(rule_tac [!] subset_antisym) |
360 by (rule_tac [!] subset_antisym) |
359 apply(simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a]) |
361 (simp_all add: supp_abs_subset1[OF a] supp_abs_subset2[OF a]) |
360 done |
|
361 |
362 |
362 lemma supp_abs: |
363 lemma supp_abs: |
363 fixes x::"'a::fs" |
364 fixes x::"'a::fs" |
364 shows "supp (Abs as x) = (supp x) - as" |
365 shows "supp (Abs as x) = (supp x) - as" |
365 and "supp (Abs_res as x) = (supp x) - as" |
366 and "supp (Abs_res as x) = (supp x) - as" |
366 and "supp (Abs_lst bs x) = (supp x) - (set bs)" |
367 and "supp (Abs_lst bs x) = (supp x) - (set bs)" |
367 apply(rule_tac [!] abs_finite_supp) |
368 by (rule_tac [!] abs_finite_supp) |
368 apply(simp_all add: finite_supp) |
369 (simp_all add: finite_supp) |
369 done |
|
370 |
370 |
371 instance abs_gen :: (fs) fs |
371 instance abs_gen :: (fs) fs |
372 apply(default) |
372 apply(default) |
373 apply(case_tac x rule: abs_exhausts(1)) |
373 apply(case_tac x rule: abs_exhausts(1)) |
374 apply(simp add: supp_abs finite_supp) |
374 apply(simp add: supp_abs finite_supp) |