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