doc-src/TutorialI/Sets/Functions.thy
author wenzelm
Wed Jul 25 12:38:54 2012 +0200 (2012-07-25)
changeset 48497 ba61aceaa18a
parent 42637 381fdcab0f36
child 48611 b34ff75c23a7
permissions -rw-r--r--
some updates on "Building a repository version of Isabelle";
     1 theory Functions imports Main begin
     2 
     3 ML "Pretty.margin_default := 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 text{*
    69 small sample proof
    70 
    71 @{thm[display] ext[no_vars]}
    72 \rulename{ext}
    73 
    74 @{thm[display] fun_eq_iff[no_vars]}
    75 \rulename{fun_eq_iff}
    76 *}
    77 
    78 lemma "inj f \<Longrightarrow> (f o g = f o h) = (g = h)";
    79   apply (simp add: fun_eq_iff inj_on_def)
    80   apply (auto)
    81   done
    82 
    83 text{*
    84 \begin{isabelle}
    85 inj\ f\ \isasymLongrightarrow \ (f\ \isasymcirc \ g\ =\ f\ \isasymcirc \ h)\ =\ (g\ =\ h)\isanewline
    86 \ 1.\ \isasymforall x\ y.\ f\ x\ =\ f\ y\ \isasymlongrightarrow \ x\ =\ y\ \isasymLongrightarrow \isanewline
    87 \ \ \ \ (\isasymforall x.\ f\ (g\ x)\ =\ f\ (h\ x))\ =\ (\isasymforall x.\ g\ x\ =\ h\ x)
    88 \end{isabelle}
    89 *}
    90  
    91 
    92 text{*image, inverse image*}
    93 
    94 text{*
    95 @{thm[display] image_def[no_vars]}
    96 \rulename{image_def}
    97 *}
    98 
    99 text{*
   100 @{thm[display] image_Un[no_vars]}
   101 \rulename{image_Un}
   102 *}
   103 
   104 text{*
   105 @{thm[display] image_compose[no_vars]}
   106 \rulename{image_compose}
   107 
   108 @{thm[display] image_Int[no_vars]}
   109 \rulename{image_Int}
   110 
   111 @{thm[display] bij_image_Compl_eq[no_vars]}
   112 \rulename{bij_image_Compl_eq}
   113 *}
   114 
   115 
   116 text{*
   117 illustrates Union as well as image
   118 *}
   119 
   120 lemma "f`A \<union> g`A = (\<Union>x\<in>A. {f x, g x})"
   121 by blast
   122 
   123 lemma "f ` {(x,y). P x y} = {f(x,y) | x y. P x y}"
   124 by blast
   125 
   126 text{*actually a macro!*}
   127 
   128 lemma "range f = f`UNIV"
   129 by blast
   130 
   131 
   132 text{*
   133 inverse image
   134 *}
   135 
   136 text{*
   137 @{thm[display] vimage_def[no_vars]}
   138 \rulename{vimage_def}
   139 
   140 @{thm[display] vimage_Compl[no_vars]}
   141 \rulename{vimage_Compl}
   142 *}
   143 
   144 
   145 end