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 "fA \<union> gA = (\<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 = fUNIV"

   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