author | haftmann |
Sat, 15 Mar 2014 08:31:33 +0100 | |
changeset 56154 | f0a927235162 |
parent 48985 | 5386df44a037 |
child 58860 | fee7cfa69c50 |
permissions | -rw-r--r-- |
16417 | 1 |
theory Functions imports Main begin |
10294 | 2 |
|
3 |
||
4 |
text{* |
|
5 |
@{thm[display] id_def[no_vars]} |
|
6 |
\rulename{id_def} |
|
7 |
||
8 |
@{thm[display] o_def[no_vars]} |
|
9 |
\rulename{o_def} |
|
10 |
||
11 |
@{thm[display] o_assoc[no_vars]} |
|
12 |
\rulename{o_assoc} |
|
13 |
*} |
|
14 |
||
15 |
text{* |
|
16 |
@{thm[display] fun_upd_apply[no_vars]} |
|
17 |
\rulename{fun_upd_apply} |
|
18 |
||
19 |
@{thm[display] fun_upd_upd[no_vars]} |
|
20 |
\rulename{fun_upd_upd} |
|
21 |
*} |
|
22 |
||
23 |
||
24 |
text{* |
|
25 |
definitions of injective, surjective, bijective |
|
26 |
||
27 |
@{thm[display] inj_on_def[no_vars]} |
|
28 |
\rulename{inj_on_def} |
|
29 |
||
30 |
@{thm[display] surj_def[no_vars]} |
|
31 |
\rulename{surj_def} |
|
32 |
||
33 |
@{thm[display] bij_def[no_vars]} |
|
34 |
\rulename{bij_def} |
|
35 |
*} |
|
36 |
||
37 |
||
38 |
||
39 |
text{* |
|
40 |
possibly interesting theorems about inv |
|
41 |
*} |
|
42 |
||
43 |
text{* |
|
44 |
@{thm[display] inv_f_f[no_vars]} |
|
45 |
\rulename{inv_f_f} |
|
46 |
||
47 |
@{thm[display] inj_imp_surj_inv[no_vars]} |
|
48 |
\rulename{inj_imp_surj_inv} |
|
49 |
||
50 |
@{thm[display] surj_imp_inj_inv[no_vars]} |
|
51 |
\rulename{surj_imp_inj_inv} |
|
52 |
||
53 |
@{thm[display] surj_f_inv_f[no_vars]} |
|
54 |
\rulename{surj_f_inv_f} |
|
55 |
||
56 |
@{thm[display] bij_imp_bij_inv[no_vars]} |
|
57 |
\rulename{bij_imp_bij_inv} |
|
58 |
||
59 |
@{thm[display] inv_inv_eq[no_vars]} |
|
60 |
\rulename{inv_inv_eq} |
|
61 |
||
62 |
@{thm[display] o_inv_distrib[no_vars]} |
|
63 |
\rulename{o_inv_distrib} |
|
64 |
*} |
|
65 |
||
66 |
text{* |
|
67 |
small sample proof |
|
68 |
||
69 |
@{thm[display] ext[no_vars]} |
|
70 |
\rulename{ext} |
|
71 |
||
39795 | 72 |
@{thm[display] fun_eq_iff[no_vars]} |
73 |
\rulename{fun_eq_iff} |
|
10294 | 74 |
*} |
75 |
||
76 |
lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)"; |
|
39795 | 77 |
apply (simp add: fun_eq_iff inj_on_def) |
10294 | 78 |
apply (auto) |
79 |
done |
|
80 |
||
81 |
text{* |
|
82 |
\begin{isabelle} |
|
83 |
inj\ f\ \isasymLongrightarrow \ (f\ \isasymcirc \ g\ =\ f\ \isasymcirc \ h)\ =\ (g\ =\ h)\isanewline |
|
84 |
\ 1.\ \isasymforall x\ y.\ f\ x\ =\ f\ y\ \isasymlongrightarrow \ x\ =\ y\ \isasymLongrightarrow \isanewline |
|
85 |
\ \ \ \ (\isasymforall x.\ f\ (g\ x)\ =\ f\ (h\ x))\ =\ (\isasymforall x.\ g\ x\ =\ h\ x) |
|
86 |
\end{isabelle} |
|
87 |
*} |
|
88 |
||
89 |
||
90 |
text{*image, inverse image*} |
|
91 |
||
92 |
text{* |
|
93 |
@{thm[display] image_def[no_vars]} |
|
94 |
\rulename{image_def} |
|
95 |
*} |
|
96 |
||
97 |
text{* |
|
98 |
@{thm[display] image_Un[no_vars]} |
|
99 |
\rulename{image_Un} |
|
100 |
*} |
|
101 |
||
102 |
text{* |
|
56154
f0a927235162
more complete set of lemmas wrt. image and composition
haftmann
parents:
48985
diff
changeset
|
103 |
@{thm[display] image_comp[no_vars]} |
f0a927235162
more complete set of lemmas wrt. image and composition
haftmann
parents:
48985
diff
changeset
|
104 |
\rulename{image_comp} |
10294 | 105 |
|
106 |
@{thm[display] image_Int[no_vars]} |
|
107 |
\rulename{image_Int} |
|
108 |
||
109 |
@{thm[display] bij_image_Compl_eq[no_vars]} |
|
110 |
\rulename{bij_image_Compl_eq} |
|
111 |
*} |
|
112 |
||
113 |
||
114 |
text{* |
|
115 |
illustrates Union as well as image |
|
116 |
*} |
|
10849 | 117 |
|
10839 | 118 |
lemma "f`A \<union> g`A = (\<Union>x\<in>A. {f x, g x})" |
10849 | 119 |
by blast |
10294 | 120 |
|
10839 | 121 |
lemma "f ` {(x,y). P x y} = {f(x,y) | x y. P x y}" |
10849 | 122 |
by blast |
10294 | 123 |
|
124 |
text{*actually a macro!*} |
|
125 |
||
10839 | 126 |
lemma "range f = f`UNIV" |
10849 | 127 |
by blast |
10294 | 128 |
|
129 |
||
130 |
text{* |
|
131 |
inverse image |
|
132 |
*} |
|
133 |
||
134 |
text{* |
|
135 |
@{thm[display] vimage_def[no_vars]} |
|
136 |
\rulename{vimage_def} |
|
137 |
||
138 |
@{thm[display] vimage_Compl[no_vars]} |
|
139 |
\rulename{vimage_Compl} |
|
140 |
*} |
|
141 |
||
142 |
||
143 |
end |