kuncar@54149
|
1 |
(* Title: HOL/Lifting_Set.thy
|
kuncar@54149
|
2 |
Author: Brian Huffman and Ondrej Kuncar
|
kuncar@54149
|
3 |
*)
|
kuncar@54149
|
4 |
|
kuncar@54149
|
5 |
header {* Setup for Lifting/Transfer for the set type *}
|
kuncar@54149
|
6 |
|
kuncar@54149
|
7 |
theory Lifting_Set
|
kuncar@54149
|
8 |
imports Lifting
|
kuncar@54149
|
9 |
begin
|
kuncar@54149
|
10 |
|
kuncar@54149
|
11 |
subsection {* Relator and predicator properties *}
|
kuncar@54149
|
12 |
|
blanchet@57280
|
13 |
definition rel_set :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> bool"
|
blanchet@57280
|
14 |
where "rel_set R = (\<lambda>A B. (\<forall>x\<in>A. \<exists>y\<in>B. R x y) \<and> (\<forall>y\<in>B. \<exists>x\<in>A. R x y))"
|
kuncar@54149
|
15 |
|
blanchet@57280
|
16 |
lemma rel_setI:
|
kuncar@54149
|
17 |
assumes "\<And>x. x \<in> A \<Longrightarrow> \<exists>y\<in>B. R x y"
|
kuncar@54149
|
18 |
assumes "\<And>y. y \<in> B \<Longrightarrow> \<exists>x\<in>A. R x y"
|
blanchet@57280
|
19 |
shows "rel_set R A B"
|
blanchet@57280
|
20 |
using assms unfolding rel_set_def by simp
|
kuncar@54149
|
21 |
|
blanchet@57280
|
22 |
lemma rel_setD1: "\<lbrakk> rel_set R A B; x \<in> A \<rbrakk> \<Longrightarrow> \<exists>y \<in> B. R x y"
|
blanchet@57280
|
23 |
and rel_setD2: "\<lbrakk> rel_set R A B; y \<in> B \<rbrakk> \<Longrightarrow> \<exists>x \<in> A. R x y"
|
blanchet@57280
|
24 |
by(simp_all add: rel_set_def)
|
Andreas@55064
|
25 |
|
blanchet@57280
|
26 |
lemma rel_set_conversep [simp]: "rel_set A\<inverse>\<inverse> = (rel_set A)\<inverse>\<inverse>"
|
blanchet@57280
|
27 |
unfolding rel_set_def by auto
|
kuncar@54149
|
28 |
|
blanchet@57280
|
29 |
lemma rel_set_eq [relator_eq]: "rel_set (op =) = (op =)"
|
blanchet@57280
|
30 |
unfolding rel_set_def fun_eq_iff by auto
|
kuncar@54149
|
31 |
|
blanchet@57280
|
32 |
lemma rel_set_mono[relator_mono]:
|
kuncar@54149
|
33 |
assumes "A \<le> B"
|
blanchet@57280
|
34 |
shows "rel_set A \<le> rel_set B"
|
blanchet@57280
|
35 |
using assms unfolding rel_set_def by blast
|
kuncar@54149
|
36 |
|
blanchet@57280
|
37 |
lemma rel_set_OO[relator_distr]: "rel_set R OO rel_set S = rel_set (R OO S)"
|
kuncar@54149
|
38 |
apply (rule sym)
|
kuncar@54149
|
39 |
apply (intro ext, rename_tac X Z)
|
kuncar@54149
|
40 |
apply (rule iffI)
|
kuncar@54149
|
41 |
apply (rule_tac b="{y. (\<exists>x\<in>X. R x y) \<and> (\<exists>z\<in>Z. S y z)}" in relcomppI)
|
blanchet@57280
|
42 |
apply (simp add: rel_set_def, fast)
|
blanchet@57280
|
43 |
apply (simp add: rel_set_def, fast)
|
blanchet@57280
|
44 |
apply (simp add: rel_set_def, fast)
|
kuncar@54149
|
45 |
done
|
kuncar@54149
|
46 |
|
kuncar@54149
|
47 |
lemma Domainp_set[relator_domain]:
|
kuncar@57862
|
48 |
"Domainp (rel_set T) = (\<lambda>A. Ball A (Domainp T))"
|
kuncar@57862
|
49 |
unfolding rel_set_def Domainp_iff[abs_def]
|
kuncar@54149
|
50 |
apply (intro ext)
|
kuncar@54149
|
51 |
apply (rule iffI)
|
kuncar@54149
|
52 |
apply blast
|
kuncar@54149
|
53 |
apply (rename_tac A, rule_tac x="{y. \<exists>x\<in>A. T x y}" in exI, fast)
|
kuncar@54149
|
54 |
done
|
kuncar@54149
|
55 |
|
kuncar@57860
|
56 |
lemma left_total_rel_set[transfer_rule]:
|
blanchet@57280
|
57 |
"left_total A \<Longrightarrow> left_total (rel_set A)"
|
blanchet@57280
|
58 |
unfolding left_total_def rel_set_def
|
kuncar@54149
|
59 |
apply safe
|
kuncar@54149
|
60 |
apply (rename_tac X, rule_tac x="{y. \<exists>x\<in>X. A x y}" in exI, fast)
|
kuncar@54149
|
61 |
done
|
kuncar@54149
|
62 |
|
kuncar@57860
|
63 |
lemma left_unique_rel_set[transfer_rule]:
|
blanchet@57280
|
64 |
"left_unique A \<Longrightarrow> left_unique (rel_set A)"
|
blanchet@57280
|
65 |
unfolding left_unique_def rel_set_def
|
kuncar@54149
|
66 |
by fast
|
kuncar@54149
|
67 |
|
blanchet@57280
|
68 |
lemma right_total_rel_set [transfer_rule]:
|
blanchet@57280
|
69 |
"right_total A \<Longrightarrow> right_total (rel_set A)"
|
blanchet@57280
|
70 |
using left_total_rel_set[of "A\<inverse>\<inverse>"] by simp
|
kuncar@54149
|
71 |
|
blanchet@57280
|
72 |
lemma right_unique_rel_set [transfer_rule]:
|
blanchet@57280
|
73 |
"right_unique A \<Longrightarrow> right_unique (rel_set A)"
|
blanchet@57280
|
74 |
unfolding right_unique_def rel_set_def by fast
|
kuncar@54149
|
75 |
|
blanchet@57280
|
76 |
lemma bi_total_rel_set [transfer_rule]:
|
blanchet@57280
|
77 |
"bi_total A \<Longrightarrow> bi_total (rel_set A)"
|
kuncar@57866
|
78 |
by(simp add: bi_total_alt_def left_total_rel_set right_total_rel_set)
|
kuncar@54149
|
79 |
|
blanchet@57280
|
80 |
lemma bi_unique_rel_set [transfer_rule]:
|
blanchet@57280
|
81 |
"bi_unique A \<Longrightarrow> bi_unique (rel_set A)"
|
blanchet@57280
|
82 |
unfolding bi_unique_def rel_set_def by fast
|
kuncar@54149
|
83 |
|
kuncar@57861
|
84 |
lemma set_relator_eq_onp [relator_eq_onp]:
|
kuncar@57861
|
85 |
"rel_set (eq_onp P) = eq_onp (\<lambda>A. Ball A P)"
|
kuncar@57861
|
86 |
unfolding fun_eq_iff rel_set_def eq_onp_def Ball_def by fast
|
kuncar@54149
|
87 |
|
kuncar@54149
|
88 |
subsection {* Quotient theorem for the Lifting package *}
|
kuncar@54149
|
89 |
|
kuncar@54149
|
90 |
lemma Quotient_set[quot_map]:
|
kuncar@54149
|
91 |
assumes "Quotient R Abs Rep T"
|
blanchet@57280
|
92 |
shows "Quotient (rel_set R) (image Abs) (image Rep) (rel_set T)"
|
kuncar@54149
|
93 |
using assms unfolding Quotient_alt_def4
|
blanchet@57280
|
94 |
apply (simp add: rel_set_OO[symmetric])
|
blanchet@57280
|
95 |
apply (simp add: rel_set_def, fast)
|
kuncar@54149
|
96 |
done
|
kuncar@54149
|
97 |
|
kuncar@54149
|
98 |
subsection {* Transfer rules for the Transfer package *}
|
kuncar@54149
|
99 |
|
kuncar@54149
|
100 |
subsubsection {* Unconditional transfer rules *}
|
kuncar@54149
|
101 |
|
kuncar@54149
|
102 |
context
|
kuncar@54149
|
103 |
begin
|
kuncar@54149
|
104 |
interpretation lifting_syntax .
|
kuncar@54149
|
105 |
|
blanchet@57280
|
106 |
lemma empty_transfer [transfer_rule]: "(rel_set A) {} {}"
|
blanchet@57280
|
107 |
unfolding rel_set_def by simp
|
kuncar@54149
|
108 |
|
kuncar@54149
|
109 |
lemma insert_transfer [transfer_rule]:
|
blanchet@57280
|
110 |
"(A ===> rel_set A ===> rel_set A) insert insert"
|
blanchet@57287
|
111 |
unfolding rel_fun_def rel_set_def by auto
|
kuncar@54149
|
112 |
|
kuncar@54149
|
113 |
lemma union_transfer [transfer_rule]:
|
blanchet@57280
|
114 |
"(rel_set A ===> rel_set A ===> rel_set A) union union"
|
blanchet@57287
|
115 |
unfolding rel_fun_def rel_set_def by auto
|
kuncar@54149
|
116 |
|
kuncar@54149
|
117 |
lemma Union_transfer [transfer_rule]:
|
blanchet@57280
|
118 |
"(rel_set (rel_set A) ===> rel_set A) Union Union"
|
blanchet@57287
|
119 |
unfolding rel_fun_def rel_set_def by simp fast
|
kuncar@54149
|
120 |
|
kuncar@54149
|
121 |
lemma image_transfer [transfer_rule]:
|
blanchet@57280
|
122 |
"((A ===> B) ===> rel_set A ===> rel_set B) image image"
|
blanchet@57287
|
123 |
unfolding rel_fun_def rel_set_def by simp fast
|
kuncar@54149
|
124 |
|
kuncar@54149
|
125 |
lemma UNION_transfer [transfer_rule]:
|
blanchet@57280
|
126 |
"(rel_set A ===> (A ===> rel_set B) ===> rel_set B) UNION UNION"
|
haftmann@57508
|
127 |
unfolding Union_image_eq [symmetric, abs_def] by transfer_prover
|
kuncar@54149
|
128 |
|
kuncar@54149
|
129 |
lemma Ball_transfer [transfer_rule]:
|
blanchet@57280
|
130 |
"(rel_set A ===> (A ===> op =) ===> op =) Ball Ball"
|
blanchet@57287
|
131 |
unfolding rel_set_def rel_fun_def by fast
|
kuncar@54149
|
132 |
|
kuncar@54149
|
133 |
lemma Bex_transfer [transfer_rule]:
|
blanchet@57280
|
134 |
"(rel_set A ===> (A ===> op =) ===> op =) Bex Bex"
|
blanchet@57287
|
135 |
unfolding rel_set_def rel_fun_def by fast
|
kuncar@54149
|
136 |
|
kuncar@54149
|
137 |
lemma Pow_transfer [transfer_rule]:
|
blanchet@57280
|
138 |
"(rel_set A ===> rel_set (rel_set A)) Pow Pow"
|
blanchet@57287
|
139 |
apply (rule rel_funI, rename_tac X Y, rule rel_setI)
|
kuncar@54149
|
140 |
apply (rename_tac X', rule_tac x="{y\<in>Y. \<exists>x\<in>X'. A x y}" in rev_bexI, clarsimp)
|
blanchet@57280
|
141 |
apply (simp add: rel_set_def, fast)
|
kuncar@54149
|
142 |
apply (rename_tac Y', rule_tac x="{x\<in>X. \<exists>y\<in>Y'. A x y}" in rev_bexI, clarsimp)
|
blanchet@57280
|
143 |
apply (simp add: rel_set_def, fast)
|
kuncar@54149
|
144 |
done
|
kuncar@54149
|
145 |
|
blanchet@57280
|
146 |
lemma rel_set_transfer [transfer_rule]:
|
haftmann@57824
|
147 |
"((A ===> B ===> op =) ===> rel_set A ===> rel_set B ===> op =) rel_set rel_set"
|
blanchet@57287
|
148 |
unfolding rel_fun_def rel_set_def by fast
|
kuncar@54149
|
149 |
|
kuncar@55089
|
150 |
lemma bind_transfer [transfer_rule]:
|
blanchet@57280
|
151 |
"(rel_set A ===> (A ===> rel_set B) ===> rel_set B) Set.bind Set.bind"
|
haftmann@57824
|
152 |
unfolding bind_UNION [abs_def] by transfer_prover
|
haftmann@57824
|
153 |
|
haftmann@57824
|
154 |
lemma INF_parametric [transfer_rule]:
|
haftmann@57824
|
155 |
"(rel_set A ===> (A ===> HOL.eq) ===> HOL.eq) INFIMUM INFIMUM"
|
haftmann@57824
|
156 |
unfolding INF_def [abs_def] by transfer_prover
|
haftmann@57824
|
157 |
|
haftmann@57824
|
158 |
lemma SUP_parametric [transfer_rule]:
|
haftmann@57824
|
159 |
"(rel_set R ===> (R ===> HOL.eq) ===> HOL.eq) SUPREMUM SUPREMUM"
|
haftmann@57824
|
160 |
unfolding SUP_def [abs_def] by transfer_prover
|
haftmann@57824
|
161 |
|
kuncar@55089
|
162 |
|
kuncar@54149
|
163 |
subsubsection {* Rules requiring bi-unique, bi-total or right-total relations *}
|
kuncar@54149
|
164 |
|
kuncar@54149
|
165 |
lemma member_transfer [transfer_rule]:
|
kuncar@54149
|
166 |
assumes "bi_unique A"
|
blanchet@57280
|
167 |
shows "(A ===> rel_set A ===> op =) (op \<in>) (op \<in>)"
|
blanchet@57287
|
168 |
using assms unfolding rel_fun_def rel_set_def bi_unique_def by fast
|
kuncar@54149
|
169 |
|
kuncar@54149
|
170 |
lemma right_total_Collect_transfer[transfer_rule]:
|
kuncar@54149
|
171 |
assumes "right_total A"
|
blanchet@57280
|
172 |
shows "((A ===> op =) ===> rel_set A) (\<lambda>P. Collect (\<lambda>x. P x \<and> Domainp A x)) Collect"
|
blanchet@57287
|
173 |
using assms unfolding right_total_def rel_set_def rel_fun_def Domainp_iff by fast
|
kuncar@54149
|
174 |
|
kuncar@54149
|
175 |
lemma Collect_transfer [transfer_rule]:
|
kuncar@54149
|
176 |
assumes "bi_total A"
|
blanchet@57280
|
177 |
shows "((A ===> op =) ===> rel_set A) Collect Collect"
|
blanchet@57287
|
178 |
using assms unfolding rel_fun_def rel_set_def bi_total_def by fast
|
kuncar@54149
|
179 |
|
kuncar@54149
|
180 |
lemma inter_transfer [transfer_rule]:
|
kuncar@54149
|
181 |
assumes "bi_unique A"
|
blanchet@57280
|
182 |
shows "(rel_set A ===> rel_set A ===> rel_set A) inter inter"
|
blanchet@57287
|
183 |
using assms unfolding rel_fun_def rel_set_def bi_unique_def by fast
|
kuncar@54149
|
184 |
|
kuncar@54149
|
185 |
lemma Diff_transfer [transfer_rule]:
|
kuncar@54149
|
186 |
assumes "bi_unique A"
|
blanchet@57280
|
187 |
shows "(rel_set A ===> rel_set A ===> rel_set A) (op -) (op -)"
|
blanchet@57287
|
188 |
using assms unfolding rel_fun_def rel_set_def bi_unique_def
|
kuncar@54149
|
189 |
unfolding Ball_def Bex_def Diff_eq
|
kuncar@54149
|
190 |
by (safe, simp, metis, simp, metis)
|
kuncar@54149
|
191 |
|
kuncar@54149
|
192 |
lemma subset_transfer [transfer_rule]:
|
kuncar@54149
|
193 |
assumes [transfer_rule]: "bi_unique A"
|
blanchet@57280
|
194 |
shows "(rel_set A ===> rel_set A ===> op =) (op \<subseteq>) (op \<subseteq>)"
|
kuncar@54149
|
195 |
unfolding subset_eq [abs_def] by transfer_prover
|
kuncar@54149
|
196 |
|
kuncar@54149
|
197 |
lemma right_total_UNIV_transfer[transfer_rule]:
|
kuncar@54149
|
198 |
assumes "right_total A"
|
blanchet@57280
|
199 |
shows "(rel_set A) (Collect (Domainp A)) UNIV"
|
blanchet@57280
|
200 |
using assms unfolding right_total_def rel_set_def Domainp_iff by blast
|
kuncar@54149
|
201 |
|
kuncar@54149
|
202 |
lemma UNIV_transfer [transfer_rule]:
|
kuncar@54149
|
203 |
assumes "bi_total A"
|
blanchet@57280
|
204 |
shows "(rel_set A) UNIV UNIV"
|
blanchet@57280
|
205 |
using assms unfolding rel_set_def bi_total_def by simp
|
kuncar@54149
|
206 |
|
kuncar@54149
|
207 |
lemma right_total_Compl_transfer [transfer_rule]:
|
kuncar@54149
|
208 |
assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
|
blanchet@57280
|
209 |
shows "(rel_set A ===> rel_set A) (\<lambda>S. uminus S \<inter> Collect (Domainp A)) uminus"
|
kuncar@54149
|
210 |
unfolding Compl_eq [abs_def]
|
kuncar@54149
|
211 |
by (subst Collect_conj_eq[symmetric]) transfer_prover
|
kuncar@54149
|
212 |
|
kuncar@54149
|
213 |
lemma Compl_transfer [transfer_rule]:
|
kuncar@54149
|
214 |
assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A"
|
blanchet@57280
|
215 |
shows "(rel_set A ===> rel_set A) uminus uminus"
|
kuncar@54149
|
216 |
unfolding Compl_eq [abs_def] by transfer_prover
|
kuncar@54149
|
217 |
|
kuncar@54149
|
218 |
lemma right_total_Inter_transfer [transfer_rule]:
|
kuncar@54149
|
219 |
assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "right_total A"
|
blanchet@57280
|
220 |
shows "(rel_set (rel_set A) ===> rel_set A) (\<lambda>S. Inter S \<inter> Collect (Domainp A)) Inter"
|
kuncar@54149
|
221 |
unfolding Inter_eq[abs_def]
|
kuncar@54149
|
222 |
by (subst Collect_conj_eq[symmetric]) transfer_prover
|
kuncar@54149
|
223 |
|
kuncar@54149
|
224 |
lemma Inter_transfer [transfer_rule]:
|
kuncar@54149
|
225 |
assumes [transfer_rule]: "bi_unique A" and [transfer_rule]: "bi_total A"
|
blanchet@57280
|
226 |
shows "(rel_set (rel_set A) ===> rel_set A) Inter Inter"
|
kuncar@54149
|
227 |
unfolding Inter_eq [abs_def] by transfer_prover
|
kuncar@54149
|
228 |
|
kuncar@54149
|
229 |
lemma filter_transfer [transfer_rule]:
|
kuncar@54149
|
230 |
assumes [transfer_rule]: "bi_unique A"
|
blanchet@57280
|
231 |
shows "((A ===> op=) ===> rel_set A ===> rel_set A) Set.filter Set.filter"
|
blanchet@57287
|
232 |
unfolding Set.filter_def[abs_def] rel_fun_def rel_set_def by blast
|
kuncar@54149
|
233 |
|
blanchet@57280
|
234 |
lemma bi_unique_rel_set_lemma:
|
blanchet@57280
|
235 |
assumes "bi_unique R" and "rel_set R X Y"
|
kuncar@54149
|
236 |
obtains f where "Y = image f X" and "inj_on f X" and "\<forall>x\<in>X. R x (f x)"
|
kuncar@54149
|
237 |
proof
|
kuncar@54149
|
238 |
let ?f = "\<lambda>x. THE y. R x y"
|
kuncar@54149
|
239 |
from assms show f: "\<forall>x\<in>X. R x (?f x)"
|
blanchet@57280
|
240 |
apply (clarsimp simp add: rel_set_def)
|
kuncar@54149
|
241 |
apply (drule (1) bspec, clarify)
|
kuncar@54149
|
242 |
apply (rule theI2, assumption)
|
kuncar@54149
|
243 |
apply (simp add: bi_unique_def)
|
kuncar@54149
|
244 |
apply assumption
|
kuncar@54149
|
245 |
done
|
kuncar@54149
|
246 |
from assms show "Y = image ?f X"
|
kuncar@54149
|
247 |
apply safe
|
blanchet@57280
|
248 |
apply (clarsimp simp add: rel_set_def)
|
kuncar@54149
|
249 |
apply (drule (1) bspec, clarify)
|
kuncar@54149
|
250 |
apply (rule image_eqI)
|
kuncar@54149
|
251 |
apply (rule the_equality [symmetric], assumption)
|
kuncar@54149
|
252 |
apply (simp add: bi_unique_def)
|
kuncar@54149
|
253 |
apply assumption
|
blanchet@57280
|
254 |
apply (clarsimp simp add: rel_set_def)
|
kuncar@54149
|
255 |
apply (frule (1) bspec, clarify)
|
kuncar@54149
|
256 |
apply (rule theI2, assumption)
|
kuncar@54149
|
257 |
apply (clarsimp simp add: bi_unique_def)
|
kuncar@54149
|
258 |
apply (simp add: bi_unique_def, metis)
|
kuncar@54149
|
259 |
done
|
kuncar@54149
|
260 |
show "inj_on ?f X"
|
kuncar@54149
|
261 |
apply (rule inj_onI)
|
kuncar@54149
|
262 |
apply (drule f [rule_format])
|
kuncar@54149
|
263 |
apply (drule f [rule_format])
|
kuncar@54149
|
264 |
apply (simp add: assms(1) [unfolded bi_unique_def])
|
kuncar@54149
|
265 |
done
|
kuncar@54149
|
266 |
qed
|
kuncar@54149
|
267 |
|
kuncar@54149
|
268 |
lemma finite_transfer [transfer_rule]:
|
blanchet@57280
|
269 |
"bi_unique A \<Longrightarrow> (rel_set A ===> op =) finite finite"
|
blanchet@57287
|
270 |
by (rule rel_funI, erule (1) bi_unique_rel_set_lemma,
|
kuncar@54149
|
271 |
auto dest: finite_imageD)
|
kuncar@54149
|
272 |
|
kuncar@54149
|
273 |
lemma card_transfer [transfer_rule]:
|
blanchet@57280
|
274 |
"bi_unique A \<Longrightarrow> (rel_set A ===> op =) card card"
|
blanchet@57287
|
275 |
by (rule rel_funI, erule (1) bi_unique_rel_set_lemma, simp add: card_image)
|
kuncar@54149
|
276 |
|
Andreas@55064
|
277 |
lemma vimage_parametric [transfer_rule]:
|
Andreas@55064
|
278 |
assumes [transfer_rule]: "bi_total A" "bi_unique B"
|
blanchet@57280
|
279 |
shows "((A ===> B) ===> rel_set B ===> rel_set A) vimage vimage"
|
Andreas@55064
|
280 |
unfolding vimage_def[abs_def] by transfer_prover
|
Andreas@55064
|
281 |
|
Andreas@55064
|
282 |
lemma setsum_parametric [transfer_rule]:
|
Andreas@55064
|
283 |
assumes "bi_unique A"
|
blanchet@57280
|
284 |
shows "((A ===> op =) ===> rel_set A ===> op =) setsum setsum"
|
blanchet@57287
|
285 |
proof(rule rel_funI)+
|
Andreas@55064
|
286 |
fix f :: "'a \<Rightarrow> 'c" and g S T
|
Andreas@55064
|
287 |
assume fg: "(A ===> op =) f g"
|
blanchet@57280
|
288 |
and ST: "rel_set A S T"
|
Andreas@55064
|
289 |
show "setsum f S = setsum g T"
|
Andreas@55064
|
290 |
proof(rule setsum_reindex_cong)
|
Andreas@55064
|
291 |
let ?f = "\<lambda>t. THE s. A s t"
|
Andreas@55064
|
292 |
show "S = ?f ` T"
|
blanchet@57280
|
293 |
by(blast dest: rel_setD1[OF ST] rel_setD2[OF ST] bi_uniqueDl[OF assms]
|
Andreas@55064
|
294 |
intro: rev_image_eqI the_equality[symmetric] subst[rotated, where P="\<lambda>x. x \<in> S"])
|
Andreas@55064
|
295 |
|
Andreas@55064
|
296 |
show "inj_on ?f T"
|
Andreas@55064
|
297 |
proof(rule inj_onI)
|
Andreas@55064
|
298 |
fix t1 t2
|
Andreas@55064
|
299 |
assume "t1 \<in> T" "t2 \<in> T" "?f t1 = ?f t2"
|
blanchet@57280
|
300 |
from ST `t1 \<in> T` obtain s1 where "A s1 t1" "s1 \<in> S" by(auto dest: rel_setD2)
|
Andreas@55064
|
301 |
hence "?f t1 = s1" by(auto dest: bi_uniqueDl[OF assms])
|
Andreas@55064
|
302 |
moreover
|
blanchet@57280
|
303 |
from ST `t2 \<in> T` obtain s2 where "A s2 t2" "s2 \<in> S" by(auto dest: rel_setD2)
|
Andreas@55064
|
304 |
hence "?f t2 = s2" by(auto dest: bi_uniqueDl[OF assms])
|
Andreas@55064
|
305 |
ultimately have "s1 = s2" using `?f t1 = ?f t2` by simp
|
Andreas@55064
|
306 |
with `A s1 t1` `A s2 t2` show "t1 = t2" by(auto dest: bi_uniqueDr[OF assms])
|
Andreas@55064
|
307 |
qed
|
Andreas@55064
|
308 |
|
Andreas@55064
|
309 |
fix t
|
Andreas@55064
|
310 |
assume "t \<in> T"
|
blanchet@57280
|
311 |
with ST obtain s where "A s t" "s \<in> S" by(auto dest: rel_setD2)
|
Andreas@55064
|
312 |
hence "?f t = s" by(auto dest: bi_uniqueDl[OF assms])
|
blanchet@57287
|
313 |
moreover from fg `A s t` have "f s = g t" by(rule rel_funD)
|
Andreas@55064
|
314 |
ultimately show "g t = f (?f t)" by simp
|
Andreas@55064
|
315 |
qed
|
Andreas@55064
|
316 |
qed
|
Andreas@55064
|
317 |
|
kuncar@54149
|
318 |
end
|
kuncar@54149
|
319 |
|
kuncar@54149
|
320 |
end
|