doc-src/TutorialI/Types/Numbers.thy
author nipkow
Tue Mar 03 17:05:18 2009 +0100 (2009-03-03)
changeset 30224 79136ce06bdb
parent 30200 0db3a35eab01
child 30242 aea5d7fa7ef5
permissions -rw-r--r--
removed and renamed redundant lemmas
     1 theory Numbers
     2 imports Complex_Main
     3 begin
     4 
     5 ML "Pretty.setmargin 64"
     6 ML "ThyOutput.indent := 0"  (*we don't want 5 for listing theorems*)
     7 
     8 text{*
     9 
    10 numeric literals; default simprules; can re-orient
    11 *}
    12 
    13 lemma "2 * m = m + m"
    14 txt{*
    15 @{subgoals[display,indent=0,margin=65]}
    16 *};
    17 oops
    18 
    19 consts h :: "nat \<Rightarrow> nat"
    20 recdef h "{}"
    21 "h i = (if i = 3 then 2 else i)"
    22 
    23 text{*
    24 @{term"h 3 = 2"}
    25 @{term"h i  = i"}
    26 *}
    27 
    28 text{*
    29 @{thm[display] numeral_0_eq_0[no_vars]}
    30 \rulename{numeral_0_eq_0}
    31 
    32 @{thm[display] numeral_1_eq_1[no_vars]}
    33 \rulename{numeral_1_eq_1}
    34 
    35 @{thm[display] add_2_eq_Suc[no_vars]}
    36 \rulename{add_2_eq_Suc}
    37 
    38 @{thm[display] add_2_eq_Suc'[no_vars]}
    39 \rulename{add_2_eq_Suc'}
    40 
    41 @{thm[display] add_assoc[no_vars]}
    42 \rulename{add_assoc}
    43 
    44 @{thm[display] add_commute[no_vars]}
    45 \rulename{add_commute}
    46 
    47 @{thm[display] add_left_commute[no_vars]}
    48 \rulename{add_left_commute}
    49 
    50 these form add_ac; similarly there is mult_ac
    51 *}
    52 
    53 lemma "Suc(i + j*l*k + m*n) = f (n*m + i + k*j*l)"
    54 txt{*
    55 @{subgoals[display,indent=0,margin=65]}
    56 *};
    57 apply (simp add: add_ac mult_ac)
    58 txt{*
    59 @{subgoals[display,indent=0,margin=65]}
    60 *};
    61 oops
    62 
    63 text{*
    64 
    65 @{thm[display] div_le_mono[no_vars]}
    66 \rulename{div_le_mono}
    67 
    68 @{thm[display] diff_mult_distrib[no_vars]}
    69 \rulename{diff_mult_distrib}
    70 
    71 @{thm[display] mod_mult_distrib[no_vars]}
    72 \rulename{mod_mult_distrib}
    73 
    74 @{thm[display] nat_diff_split[no_vars]}
    75 \rulename{nat_diff_split}
    76 *}
    77 
    78 
    79 lemma "(n - 1) * (n + 1) = n * n - (1::nat)"
    80 apply (clarsimp split: nat_diff_split iff del: less_Suc0)
    81  --{* @{subgoals[display,indent=0,margin=65]} *}
    82 apply (subgoal_tac "n=0", force, arith)
    83 done
    84 
    85 
    86 lemma "(n - 2) * (n + 2) = n * n - (4::nat)"
    87 apply (simp split: nat_diff_split, clarify)
    88  --{* @{subgoals[display,indent=0,margin=65]} *}
    89 apply (subgoal_tac "n=0 | n=1", force, arith)
    90 done
    91 
    92 text{*
    93 @{thm[display] mod_if[no_vars]}
    94 \rulename{mod_if}
    95 
    96 @{thm[display] mod_div_equality[no_vars]}
    97 \rulename{mod_div_equality}
    98 
    99 
   100 @{thm[display] div_mult1_eq[no_vars]}
   101 \rulename{div_mult1_eq}
   102 
   103 @{thm[display] mod_mult_right_eq[no_vars]}
   104 \rulename{mod_mult_right_eq}
   105 
   106 @{thm[display] div_mult2_eq[no_vars]}
   107 \rulename{div_mult2_eq}
   108 
   109 @{thm[display] mod_mult2_eq[no_vars]}
   110 \rulename{mod_mult2_eq}
   111 
   112 @{thm[display] div_mult_mult1[no_vars]}
   113 \rulename{div_mult_mult1}
   114 
   115 @{thm[display] div_by_0 [no_vars]}
   116 \rulename{div_by_0}
   117 
   118 @{thm[display] mod_by_0 [no_vars]}
   119 \rulename{mod_by_0}
   120 
   121 @{thm[display] dvd_anti_sym[no_vars]}
   122 \rulename{dvd_anti_sym}
   123 
   124 @{thm[display] dvd_add[no_vars]}
   125 \rulename{dvd_add}
   126 
   127 For the integers, I'd list a few theorems that somehow involve negative 
   128 numbers.*}
   129 
   130 
   131 text{*
   132 Division, remainder of negatives
   133 
   134 
   135 @{thm[display] pos_mod_sign[no_vars]}
   136 \rulename{pos_mod_sign}
   137 
   138 @{thm[display] pos_mod_bound[no_vars]}
   139 \rulename{pos_mod_bound}
   140 
   141 @{thm[display] neg_mod_sign[no_vars]}
   142 \rulename{neg_mod_sign}
   143 
   144 @{thm[display] neg_mod_bound[no_vars]}
   145 \rulename{neg_mod_bound}
   146 
   147 @{thm[display] zdiv_zadd1_eq[no_vars]}
   148 \rulename{zdiv_zadd1_eq}
   149 
   150 @{thm[display] mod_add_eq[no_vars]}
   151 \rulename{mod_add_eq}
   152 
   153 @{thm[display] zdiv_zmult1_eq[no_vars]}
   154 \rulename{zdiv_zmult1_eq}
   155 
   156 @{thm[display] zmod_zmult1_eq[no_vars]}
   157 \rulename{zmod_zmult1_eq}
   158 
   159 @{thm[display] zdiv_zmult2_eq[no_vars]}
   160 \rulename{zdiv_zmult2_eq}
   161 
   162 @{thm[display] zmod_zmult2_eq[no_vars]}
   163 \rulename{zmod_zmult2_eq}
   164 *}  
   165 
   166 lemma "abs (x+y) \<le> abs x + abs (y :: int)"
   167 by arith
   168 
   169 lemma "abs (2*x) = 2 * abs (x :: int)"
   170 by (simp add: abs_if) 
   171 
   172 
   173 text {*Induction rules for the Integers
   174 
   175 @{thm[display] int_ge_induct[no_vars]}
   176 \rulename{int_ge_induct}
   177 
   178 @{thm[display] int_gr_induct[no_vars]}
   179 \rulename{int_gr_induct}
   180 
   181 @{thm[display] int_le_induct[no_vars]}
   182 \rulename{int_le_induct}
   183 
   184 @{thm[display] int_less_induct[no_vars]}
   185 \rulename{int_less_induct}
   186 *}  
   187 
   188 text {*FIELDS
   189 
   190 @{thm[display] dense[no_vars]}
   191 \rulename{dense}
   192 
   193 @{thm[display] times_divide_eq_right[no_vars]}
   194 \rulename{times_divide_eq_right}
   195 
   196 @{thm[display] times_divide_eq_left[no_vars]}
   197 \rulename{times_divide_eq_left}
   198 
   199 @{thm[display] divide_divide_eq_right[no_vars]}
   200 \rulename{divide_divide_eq_right}
   201 
   202 @{thm[display] divide_divide_eq_left[no_vars]}
   203 \rulename{divide_divide_eq_left}
   204 
   205 @{thm[display] minus_divide_left[no_vars]}
   206 \rulename{minus_divide_left}
   207 
   208 @{thm[display] minus_divide_right[no_vars]}
   209 \rulename{minus_divide_right}
   210 
   211 This last NOT a simprule
   212 
   213 @{thm[display] add_divide_distrib[no_vars]}
   214 \rulename{add_divide_distrib}
   215 *}
   216 
   217 lemma "3/4 < (7/8 :: real)"
   218 by simp 
   219 
   220 lemma "P ((3/4) * (8/15 :: real))"
   221 txt{*
   222 @{subgoals[display,indent=0,margin=65]}
   223 *};
   224 apply simp 
   225 txt{*
   226 @{subgoals[display,indent=0,margin=65]}
   227 *};
   228 oops
   229 
   230 lemma "(3/4) * (8/15) < (x :: real)"
   231 txt{*
   232 @{subgoals[display,indent=0,margin=65]}
   233 *};
   234 apply simp 
   235 txt{*
   236 @{subgoals[display,indent=0,margin=65]}
   237 *};
   238 oops
   239 
   240 text{*
   241 Ring and Field
   242 
   243 Requires a field, or else an ordered ring
   244 
   245 @{thm[display] mult_eq_0_iff[no_vars]}
   246 \rulename{mult_eq_0_iff}
   247 
   248 @{thm[display] mult_cancel_right[no_vars]}
   249 \rulename{mult_cancel_right}
   250 
   251 @{thm[display] mult_cancel_left[no_vars]}
   252 \rulename{mult_cancel_left}
   253 *}
   254 
   255 ML{*set show_sorts*}
   256 
   257 text{*
   258 effect of show sorts on the above
   259 
   260 @{thm[display] mult_cancel_left[no_vars]}
   261 \rulename{mult_cancel_left}
   262 *}
   263 
   264 ML{*reset show_sorts*}
   265 
   266 
   267 text{*
   268 absolute value
   269 
   270 @{thm[display] abs_mult[no_vars]}
   271 \rulename{abs_mult}
   272 
   273 @{thm[display] abs_le_iff[no_vars]}
   274 \rulename{abs_le_iff}
   275 
   276 @{thm[display] abs_triangle_ineq[no_vars]}
   277 \rulename{abs_triangle_ineq}
   278 
   279 @{thm[display] power_add[no_vars]}
   280 \rulename{power_add}
   281 
   282 @{thm[display] power_mult[no_vars]}
   283 \rulename{power_mult}
   284 
   285 @{thm[display] power_abs[no_vars]}
   286 \rulename{power_abs}
   287 
   288 
   289 *}
   290 
   291 
   292 end