1 theory Functions imports Main begin |
|
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 |
|
72 @{thm[display] fun_eq_iff[no_vars]} |
|
73 \rulename{fun_eq_iff} |
|
74 *} |
|
75 |
|
76 lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)"; |
|
77 apply (simp add: fun_eq_iff inj_on_def) |
|
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{* |
|
103 @{thm[display] image_compose[no_vars]} |
|
104 \rulename{image_compose} |
|
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 *} |
|
117 |
|
118 lemma "f`A \<union> g`A = (\<Union>x\<in>A. {f x, g x})" |
|
119 by blast |
|
120 |
|
121 lemma "f ` {(x,y). P x y} = {f(x,y) | x y. P x y}" |
|
122 by blast |
|
123 |
|
124 text{*actually a macro!*} |
|
125 |
|
126 lemma "range f = f`UNIV" |
|
127 by blast |
|
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 |
|