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