4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Notions about functions. |
6 Notions about functions. |
7 *) |
7 *) |
8 |
8 |
9 Fun = Typedef + |
9 theory Fun = Typedef: |
10 |
10 |
11 instance set :: (type) order |
11 instance set :: (type) order |
12 (subset_refl,subset_trans,subset_antisym,psubset_eq) |
12 by (intro_classes, |
13 consts |
13 (assumption | rule subset_refl subset_trans subset_antisym psubset_eq)+) |
14 fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" |
14 |
|
15 constdefs |
|
16 fun_upd :: "('a => 'b) => 'a => 'b => ('a => 'b)" |
|
17 "fun_upd f a b == % x. if x=a then b else f x" |
15 |
18 |
16 nonterminals |
19 nonterminals |
17 updbinds updbind |
20 updbinds updbind |
18 syntax |
21 syntax |
19 "_updbind" :: ['a, 'a] => updbind ("(2_ :=/ _)") |
22 "_updbind" :: "['a, 'a] => updbind" ("(2_ :=/ _)") |
20 "" :: updbind => updbinds ("_") |
23 "" :: "updbind => updbinds" ("_") |
21 "_updbinds" :: [updbind, updbinds] => updbinds ("_,/ _") |
24 "_updbinds":: "[updbind, updbinds] => updbinds" ("_,/ _") |
22 "_Update" :: ['a, updbinds] => 'a ("_/'((_)')" [1000,0] 900) |
25 "_Update" :: "['a, updbinds] => 'a" ("_/'((_)')" [1000,0] 900) |
23 |
26 |
24 translations |
27 translations |
25 "_Update f (_updbinds b bs)" == "_Update (_Update f b) bs" |
28 "_Update f (_updbinds b bs)" == "_Update (_Update f b) bs" |
26 "f(x:=y)" == "fun_upd f x y" |
29 "f(x:=y)" == "fun_upd f x y" |
27 |
|
28 defs |
|
29 fun_upd_def "f(a:=b) == % x. if x=a then b else f x" |
|
30 |
30 |
31 (* Hint: to define the sum of two functions (or maps), use sum_case. |
31 (* Hint: to define the sum of two functions (or maps), use sum_case. |
32 A nice infix syntax could be defined (in Datatype.thy or below) by |
32 A nice infix syntax could be defined (in Datatype.thy or below) by |
33 consts |
33 consts |
34 fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80) |
34 fun_sum :: "('a => 'c) => ('b => 'c) => (('a+'b) => 'c)" (infixr "'(+')"80) |
35 translations |
35 translations |
36 "fun_sum" == "sum_case" |
36 "fun_sum" == sum_case |
37 *) |
37 *) |
38 |
38 |
39 constdefs |
39 constdefs |
40 id :: 'a => 'a |
40 id :: "'a => 'a" |
41 "id == %x. x" |
41 "id == %x. x" |
42 |
42 |
43 o :: ['b => 'c, 'a => 'b, 'a] => 'c (infixl 55) |
43 comp :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixl "o" 55) |
44 "f o g == %x. f(g(x))" |
44 "f o g == %x. f(g(x))" |
45 |
45 |
46 inj_on :: ['a => 'b, 'a set] => bool |
46 text{*compatibility*} |
|
47 lemmas o_def = comp_def |
|
48 |
|
49 syntax (xsymbols) |
|
50 comp :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixl "\<circ>" 55) |
|
51 |
|
52 |
|
53 constdefs |
|
54 inj_on :: "['a => 'b, 'a set] => bool" (*injective*) |
47 "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y" |
55 "inj_on f A == ! x:A. ! y:A. f(x)=f(y) --> x=y" |
48 |
56 |
49 syntax (xsymbols) |
57 text{*A common special case: functions injective over the entire domain type.*} |
50 "op o" :: "['b => 'c, 'a => 'b, 'a] => 'c" (infixl "\\<circ>" 55) |
58 syntax inj :: "('a => 'b) => bool" |
51 |
|
52 syntax |
|
53 inj :: ('a => 'b) => bool (*injective*) |
|
54 |
|
55 translations |
59 translations |
56 "inj f" == "inj_on f UNIV" |
60 "inj f" == "inj_on f UNIV" |
57 |
61 |
58 constdefs |
62 constdefs |
59 surj :: ('a => 'b) => bool (*surjective*) |
63 surj :: "('a => 'b) => bool" (*surjective*) |
60 "surj f == ! y. ? x. y=f(x)" |
64 "surj f == ! y. ? x. y=f(x)" |
61 |
65 |
62 bij :: ('a => 'b) => bool (*bijective*) |
66 bij :: "('a => 'b) => bool" (*bijective*) |
63 "bij f == inj f & surj f" |
67 "bij f == inj f & surj f" |
64 |
68 |
65 |
69 |
66 (*The Pi-operator, by Florian Kammueller*) |
70 |
67 |
71 text{*As a simplification rule, it replaces all function equalities by |
68 constdefs |
72 first-order equalities.*} |
69 Pi :: "['a set, 'a => 'b set] => ('a => 'b) set" |
73 lemma expand_fun_eq: "(f = g) = (! x. f(x)=g(x))" |
70 "Pi A B == {f. ! x. if x:A then f(x) : B(x) else f(x) = arbitrary}" |
74 apply (rule iffI) |
71 |
75 apply (simp (no_asm_simp)) |
72 restrict :: "['a => 'b, 'a set] => ('a => 'b)" |
76 apply (rule ext, simp (no_asm_simp)) |
73 "restrict f A == (%x. if x : A then f x else arbitrary)" |
77 done |
74 |
78 |
75 syntax |
79 lemma apply_inverse: |
76 "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3PI _:_./ _)" 10) |
80 "[| f(x)=u; !!x. P(x) ==> g(f(x)) = x; P(x) |] ==> x=g(u)" |
77 funcset :: "['a set, 'b set] => ('a => 'b) set" (infixr 60) |
81 by auto |
78 "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)" ("(3%_:_./ _)" [0, 0, 3] 3) |
82 |
79 syntax (xsymbols) |
83 |
80 "@lam" :: "[pttrn, 'a set, 'a => 'b] => ('a => 'b)" ("(3\\<lambda>_\\<in>_./ _)" [0, 0, 3] 3) |
84 text{*The Identity Function: @{term id}*} |
81 |
85 lemma id_apply [simp]: "id x = x" |
82 (*Giving funcset an arrow syntax (-> or =>) clashes with many existing theories*) |
86 by (simp add: id_def) |
83 |
87 |
84 syntax (xsymbols) |
88 |
85 "@Pi" :: "[pttrn, 'a set, 'b set] => ('a => 'b) set" ("(3\\<Pi> _\\<in>_./ _)" 10) |
89 subsection{*The Composition Operator: @{term "f \<circ> g"}*} |
86 |
90 |
87 translations |
91 lemma o_apply [simp]: "(f o g) x = f (g x)" |
88 "PI x:A. B" => "Pi A (%x. B)" |
92 by (simp add: comp_def) |
89 "A funcset B" => "Pi A (_K B)" |
93 |
90 "%x:A. f" == "restrict (%x. f) A" |
94 lemma o_assoc: "f o (g o h) = f o g o h" |
91 |
95 by (simp add: comp_def) |
92 constdefs |
96 |
93 compose :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)" |
97 lemma id_o [simp]: "id o g = g" |
94 "compose A g f == %x:A. g (f x)" |
98 by (simp add: comp_def) |
|
99 |
|
100 lemma o_id [simp]: "f o id = f" |
|
101 by (simp add: comp_def) |
|
102 |
|
103 lemma image_compose: "(f o g) ` r = f`(g`r)" |
|
104 by (simp add: comp_def, blast) |
|
105 |
|
106 lemma image_eq_UN: "f`A = (UN x:A. {f x})" |
|
107 by blast |
|
108 |
|
109 lemma UN_o: "UNION A (g o f) = UNION (f`A) g" |
|
110 by (unfold comp_def, blast) |
|
111 |
|
112 text{*Lemma for proving injectivity of representation functions for |
|
113 datatypes involving function types*} |
|
114 lemma inj_fun_lemma: |
|
115 "[| ! x y. g (f x) = g y --> f x = y; g o f = g o fa |] ==> f = fa" |
|
116 by (simp add: comp_def expand_fun_eq) |
|
117 |
|
118 |
|
119 subsection{*The Injectivity Predicate, @{term inj}*} |
|
120 |
|
121 text{*NB: @{term inj} now just translates to @{term inj_on}*} |
|
122 |
|
123 |
|
124 text{*For Proofs in @{text "Tools/datatype_rep_proofs"}*} |
|
125 lemma datatype_injI: |
|
126 "(!! x. ALL y. f(x) = f(y) --> x=y) ==> inj(f)" |
|
127 by (simp add: inj_on_def) |
|
128 |
|
129 lemma injD: "[| inj(f); f(x) = f(y) |] ==> x=y" |
|
130 by (simp add: inj_on_def) |
|
131 |
|
132 (*Useful with the simplifier*) |
|
133 lemma inj_eq: "inj(f) ==> (f(x) = f(y)) = (x=y)" |
|
134 by (force simp add: inj_on_def) |
|
135 |
|
136 lemma inj_o: "[| inj f; f o g = f o h |] ==> g = h" |
|
137 by (simp add: comp_def inj_on_def expand_fun_eq) |
|
138 |
|
139 |
|
140 subsection{*The Predicate @{term inj_on}: Injectivity On A Restricted Domain*} |
|
141 |
|
142 lemma inj_onI: |
|
143 "(!! x y. [| x:A; y:A; f(x) = f(y) |] ==> x=y) ==> inj_on f A" |
|
144 by (simp add: inj_on_def) |
|
145 |
|
146 lemma inj_on_inverseI: "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A" |
|
147 by (auto dest: arg_cong [of concl: g] simp add: inj_on_def) |
|
148 |
|
149 lemma inj_onD: "[| inj_on f A; f(x)=f(y); x:A; y:A |] ==> x=y" |
|
150 by (unfold inj_on_def, blast) |
|
151 |
|
152 lemma inj_on_iff: "[| inj_on f A; x:A; y:A |] ==> (f(x)=f(y)) = (x=y)" |
|
153 by (blast dest!: inj_onD) |
|
154 |
|
155 lemma comp_inj_on: |
|
156 "[| inj_on f A; inj_on g (f`A) |] ==> inj_on (g o f) A" |
|
157 by (simp add: comp_def inj_on_def) |
|
158 |
|
159 lemma inj_on_contraD: "[| inj_on f A; ~x=y; x:A; y:A |] ==> ~ f(x)=f(y)" |
|
160 by (unfold inj_on_def, blast) |
|
161 |
|
162 lemma inj_singleton: "inj (%s. {s})" |
|
163 by (simp add: inj_on_def) |
|
164 |
|
165 lemma subset_inj_on: "[| A<=B; inj_on f B |] ==> inj_on f A" |
|
166 by (unfold inj_on_def, blast) |
|
167 |
|
168 |
|
169 subsection{*The Predicate @{term surj}: Surjectivity*} |
|
170 |
|
171 lemma surjI: "(!! x. g(f x) = x) ==> surj g" |
|
172 apply (simp add: surj_def) |
|
173 apply (blast intro: sym) |
|
174 done |
|
175 |
|
176 lemma surj_range: "surj f ==> range f = UNIV" |
|
177 by (auto simp add: surj_def) |
|
178 |
|
179 lemma surjD: "surj f ==> EX x. y = f x" |
|
180 by (simp add: surj_def) |
|
181 |
|
182 lemma surjE: "surj f ==> (!!x. y = f x ==> C) ==> C" |
|
183 by (simp add: surj_def, blast) |
|
184 |
|
185 lemma comp_surj: "[| surj f; surj g |] ==> surj (g o f)" |
|
186 apply (simp add: comp_def surj_def, clarify) |
|
187 apply (drule_tac x = y in spec, clarify) |
|
188 apply (drule_tac x = x in spec, blast) |
|
189 done |
|
190 |
|
191 |
|
192 |
|
193 subsection{*The Predicate @{term bij}: Bijectivity*} |
|
194 |
|
195 lemma bijI: "[| inj f; surj f |] ==> bij f" |
|
196 by (simp add: bij_def) |
|
197 |
|
198 lemma bij_is_inj: "bij f ==> inj f" |
|
199 by (simp add: bij_def) |
|
200 |
|
201 lemma bij_is_surj: "bij f ==> surj f" |
|
202 by (simp add: bij_def) |
|
203 |
|
204 |
|
205 subsection{*Facts About the Identity Function*} |
|
206 |
|
207 text{*We seem to need both the @{term id} forms and the @{term "\<lambda>x. x"} |
|
208 forms. The latter can arise by rewriting, while @{term id} may be used |
|
209 explicitly.*} |
|
210 |
|
211 lemma image_ident [simp]: "(%x. x) ` Y = Y" |
|
212 by blast |
|
213 |
|
214 lemma image_id [simp]: "id ` Y = Y" |
|
215 by (simp add: id_def) |
|
216 |
|
217 lemma vimage_ident [simp]: "(%x. x) -` Y = Y" |
|
218 by blast |
|
219 |
|
220 lemma vimage_id [simp]: "id -` A = A" |
|
221 by (simp add: id_def) |
|
222 |
|
223 lemma vimage_image_eq: "f -` (f ` A) = {y. EX x:A. f x = f y}" |
|
224 by (blast intro: sym) |
|
225 |
|
226 lemma image_vimage_subset: "f ` (f -` A) <= A" |
|
227 by blast |
|
228 |
|
229 lemma image_vimage_eq [simp]: "f ` (f -` A) = A Int range f" |
|
230 by blast |
|
231 |
|
232 lemma surj_image_vimage_eq: "surj f ==> f ` (f -` A) = A" |
|
233 by (simp add: surj_range) |
|
234 |
|
235 lemma inj_vimage_image_eq: "inj f ==> f -` (f ` A) = A" |
|
236 by (simp add: inj_on_def, blast) |
|
237 |
|
238 lemma vimage_subsetD: "surj f ==> f -` B <= A ==> B <= f ` A" |
|
239 apply (unfold surj_def) |
|
240 apply (blast intro: sym) |
|
241 done |
|
242 |
|
243 lemma vimage_subsetI: "inj f ==> B <= f ` A ==> f -` B <= A" |
|
244 by (unfold inj_on_def, blast) |
|
245 |
|
246 lemma vimage_subset_eq: "bij f ==> (f -` B <= A) = (B <= f ` A)" |
|
247 apply (unfold bij_def) |
|
248 apply (blast del: subsetI intro: vimage_subsetI vimage_subsetD) |
|
249 done |
|
250 |
|
251 lemma image_Int_subset: "f`(A Int B) <= f`A Int f`B" |
|
252 by blast |
|
253 |
|
254 lemma image_diff_subset: "f`A - f`B <= f`(A - B)" |
|
255 by blast |
|
256 |
|
257 lemma inj_on_image_Int: |
|
258 "[| inj_on f C; A<=C; B<=C |] ==> f`(A Int B) = f`A Int f`B" |
|
259 apply (simp add: inj_on_def, blast) |
|
260 done |
|
261 |
|
262 lemma inj_on_image_set_diff: |
|
263 "[| inj_on f C; A<=C; B<=C |] ==> f`(A-B) = f`A - f`B" |
|
264 apply (simp add: inj_on_def, blast) |
|
265 done |
|
266 |
|
267 lemma image_Int: "inj f ==> f`(A Int B) = f`A Int f`B" |
|
268 by (simp add: inj_on_def, blast) |
|
269 |
|
270 lemma image_set_diff: "inj f ==> f`(A-B) = f`A - f`B" |
|
271 by (simp add: inj_on_def, blast) |
|
272 |
|
273 lemma inj_image_mem_iff: "inj f ==> (f a : f`A) = (a : A)" |
|
274 by (blast dest: injD) |
|
275 |
|
276 lemma inj_image_subset_iff: "inj f ==> (f`A <= f`B) = (A<=B)" |
|
277 by (simp add: inj_on_def, blast) |
|
278 |
|
279 lemma inj_image_eq_iff: "inj f ==> (f`A = f`B) = (A = B)" |
|
280 by (blast dest: injD) |
|
281 |
|
282 lemma image_UN: "(f ` (UNION A B)) = (UN x:A.(f ` (B x)))" |
|
283 by blast |
|
284 |
|
285 (*injectivity's required. Left-to-right inclusion holds even if A is empty*) |
|
286 lemma image_INT: |
|
287 "[| inj_on f C; ALL x:A. B x <= C; j:A |] |
|
288 ==> f ` (INTER A B) = (INT x:A. f ` B x)" |
|
289 apply (simp add: inj_on_def, blast) |
|
290 done |
|
291 |
|
292 (*Compare with image_INT: no use of inj_on, and if f is surjective then |
|
293 it doesn't matter whether A is empty*) |
|
294 lemma bij_image_INT: "bij f ==> f ` (INTER A B) = (INT x:A. f ` B x)" |
|
295 apply (simp add: bij_def) |
|
296 apply (simp add: inj_on_def surj_def, blast) |
|
297 done |
|
298 |
|
299 lemma surj_Compl_image_subset: "surj f ==> -(f`A) <= f`(-A)" |
|
300 by (auto simp add: surj_def) |
|
301 |
|
302 lemma inj_image_Compl_subset: "inj f ==> f`(-A) <= -(f`A)" |
|
303 by (auto simp add: inj_on_def) |
|
304 |
|
305 lemma bij_image_Compl_eq: "bij f ==> f`(-A) = -(f`A)" |
|
306 apply (simp add: bij_def) |
|
307 apply (rule equalityI) |
|
308 apply (simp_all (no_asm_simp) add: inj_image_Compl_subset surj_Compl_image_subset) |
|
309 done |
|
310 |
|
311 |
|
312 subsection{*Function Updating*} |
|
313 |
|
314 lemma fun_upd_idem_iff: "(f(x:=y) = f) = (f x = y)" |
|
315 apply (simp add: fun_upd_def, safe) |
|
316 apply (erule subst) |
|
317 apply (rule_tac [2] ext, auto) |
|
318 done |
|
319 |
|
320 (* f x = y ==> f(x:=y) = f *) |
|
321 lemmas fun_upd_idem = fun_upd_idem_iff [THEN iffD2, standard] |
|
322 |
|
323 (* f(x := f x) = f *) |
|
324 declare refl [THEN fun_upd_idem, iff] |
|
325 |
|
326 lemma fun_upd_apply [simp]: "(f(x:=y))z = (if z=x then y else f z)" |
|
327 apply (simp (no_asm) add: fun_upd_def) |
|
328 done |
|
329 |
|
330 (* fun_upd_apply supersedes these two, but they are useful |
|
331 if fun_upd_apply is intentionally removed from the simpset *) |
|
332 lemma fun_upd_same: "(f(x:=y)) x = y" |
|
333 by simp |
|
334 |
|
335 lemma fun_upd_other: "z~=x ==> (f(x:=y)) z = f z" |
|
336 by simp |
|
337 |
|
338 lemma fun_upd_upd [simp]: "f(x:=y,x:=z) = f(x:=z)" |
|
339 by (simp add: expand_fun_eq) |
|
340 |
|
341 lemma fun_upd_twist: "a ~= c ==> (m(a:=b))(c:=d) = (m(c:=d))(a:=b)" |
|
342 by (rule ext, auto) |
|
343 |
|
344 text{*The ML section includes some compatibility bindings and a simproc |
|
345 for function updates, in addition to the usual ML-bindings of theorems.*} |
|
346 ML |
|
347 {* |
|
348 val id_def = thm "id_def"; |
|
349 val inj_on_def = thm "inj_on_def"; |
|
350 val surj_def = thm "surj_def"; |
|
351 val bij_def = thm "bij_def"; |
|
352 val fun_upd_def = thm "fun_upd_def"; |
|
353 |
|
354 val o_def = thm "comp_def"; |
|
355 val injI = thm "inj_onI"; |
|
356 val inj_inverseI = thm "inj_on_inverseI"; |
|
357 val set_cs = claset() delrules [equalityI]; |
|
358 |
|
359 val print_translation = [("Pi", dependent_tr' ("@Pi", "op funcset"))]; |
|
360 |
|
361 (* simplifies terms of the form f(...,x:=y,...,x:=z,...) to f(...,x:=z,...) *) |
|
362 local |
|
363 fun gen_fun_upd None T _ _ = None |
|
364 | gen_fun_upd (Some f) T x y = Some (Const ("Fun.fun_upd",T) $ f $ x $ y) |
|
365 fun dest_fun_T1 (Type (_, T :: Ts)) = T |
|
366 fun find_double (t as Const ("Fun.fun_upd",T) $ f $ x $ y) = |
|
367 let |
|
368 fun find (Const ("Fun.fun_upd",T) $ g $ v $ w) = |
|
369 if v aconv x then Some g else gen_fun_upd (find g) T v w |
|
370 | find t = None |
|
371 in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end |
|
372 |
|
373 val ss = simpset () |
|
374 val fun_upd_prover = K (rtac eq_reflection 1 THEN rtac ext 1 THEN simp_tac ss 1) |
|
375 in |
|
376 val fun_upd2_simproc = |
|
377 Simplifier.simproc (Theory.sign_of (the_context ())) |
|
378 "fun_upd2" ["f(v := w, x := y)"] |
|
379 (fn sg => fn _ => fn t => |
|
380 case find_double t of (T, None) => None |
|
381 | (T, Some rhs) => Some (Tactic.prove sg [] [] (Term.equals T $ t $ rhs) fun_upd_prover)) |
|
382 end; |
|
383 Addsimprocs[fun_upd2_simproc]; |
|
384 |
|
385 val expand_fun_eq = thm "expand_fun_eq"; |
|
386 val apply_inverse = thm "apply_inverse"; |
|
387 val id_apply = thm "id_apply"; |
|
388 val o_apply = thm "o_apply"; |
|
389 val o_assoc = thm "o_assoc"; |
|
390 val id_o = thm "id_o"; |
|
391 val o_id = thm "o_id"; |
|
392 val image_compose = thm "image_compose"; |
|
393 val image_eq_UN = thm "image_eq_UN"; |
|
394 val UN_o = thm "UN_o"; |
|
395 val inj_fun_lemma = thm "inj_fun_lemma"; |
|
396 val datatype_injI = thm "datatype_injI"; |
|
397 val injD = thm "injD"; |
|
398 val inj_eq = thm "inj_eq"; |
|
399 val inj_o = thm "inj_o"; |
|
400 val inj_onI = thm "inj_onI"; |
|
401 val inj_on_inverseI = thm "inj_on_inverseI"; |
|
402 val inj_onD = thm "inj_onD"; |
|
403 val inj_on_iff = thm "inj_on_iff"; |
|
404 val comp_inj_on = thm "comp_inj_on"; |
|
405 val inj_on_contraD = thm "inj_on_contraD"; |
|
406 val inj_singleton = thm "inj_singleton"; |
|
407 val subset_inj_on = thm "subset_inj_on"; |
|
408 val surjI = thm "surjI"; |
|
409 val surj_range = thm "surj_range"; |
|
410 val surjD = thm "surjD"; |
|
411 val surjE = thm "surjE"; |
|
412 val comp_surj = thm "comp_surj"; |
|
413 val bijI = thm "bijI"; |
|
414 val bij_is_inj = thm "bij_is_inj"; |
|
415 val bij_is_surj = thm "bij_is_surj"; |
|
416 val image_ident = thm "image_ident"; |
|
417 val image_id = thm "image_id"; |
|
418 val vimage_ident = thm "vimage_ident"; |
|
419 val vimage_id = thm "vimage_id"; |
|
420 val vimage_image_eq = thm "vimage_image_eq"; |
|
421 val image_vimage_subset = thm "image_vimage_subset"; |
|
422 val image_vimage_eq = thm "image_vimage_eq"; |
|
423 val surj_image_vimage_eq = thm "surj_image_vimage_eq"; |
|
424 val inj_vimage_image_eq = thm "inj_vimage_image_eq"; |
|
425 val vimage_subsetD = thm "vimage_subsetD"; |
|
426 val vimage_subsetI = thm "vimage_subsetI"; |
|
427 val vimage_subset_eq = thm "vimage_subset_eq"; |
|
428 val image_Int_subset = thm "image_Int_subset"; |
|
429 val image_diff_subset = thm "image_diff_subset"; |
|
430 val inj_on_image_Int = thm "inj_on_image_Int"; |
|
431 val inj_on_image_set_diff = thm "inj_on_image_set_diff"; |
|
432 val image_Int = thm "image_Int"; |
|
433 val image_set_diff = thm "image_set_diff"; |
|
434 val inj_image_mem_iff = thm "inj_image_mem_iff"; |
|
435 val inj_image_subset_iff = thm "inj_image_subset_iff"; |
|
436 val inj_image_eq_iff = thm "inj_image_eq_iff"; |
|
437 val image_UN = thm "image_UN"; |
|
438 val image_INT = thm "image_INT"; |
|
439 val bij_image_INT = thm "bij_image_INT"; |
|
440 val surj_Compl_image_subset = thm "surj_Compl_image_subset"; |
|
441 val inj_image_Compl_subset = thm "inj_image_Compl_subset"; |
|
442 val bij_image_Compl_eq = thm "bij_image_Compl_eq"; |
|
443 val fun_upd_idem_iff = thm "fun_upd_idem_iff"; |
|
444 val fun_upd_idem = thm "fun_upd_idem"; |
|
445 val fun_upd_apply = thm "fun_upd_apply"; |
|
446 val fun_upd_same = thm "fun_upd_same"; |
|
447 val fun_upd_other = thm "fun_upd_other"; |
|
448 val fun_upd_upd = thm "fun_upd_upd"; |
|
449 val fun_upd_twist = thm "fun_upd_twist"; |
|
450 *} |
95 |
451 |
96 end |
452 end |
97 |
|
98 ML |
|
99 val print_translation = [("Pi", dependent_tr' ("@Pi", "op funcset"))]; |
|