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