wneuper/isa: doc-src/TutorialI/Types/Numbers.thy@403585a89772

     1 theory Numbers

     2 imports Complex_Main

     3 begin

     5 ML "Pretty.margin_default := 64"

     6 ML "ThyOutput.indent := 0"  (*we don't want 5 for listing theorems*)

     8 text{*

    10 numeric literals; default simprules; can re-orient

    11 *}

    13 lemma "2 * m = m + m"

    14 txt{*

    15 @{subgoals[display,indent=0,margin=65]}

    16 *};

    17 oops

    19 consts h :: "nat \<Rightarrow> nat"

    20 recdef h "{}"

    21 "h i = (if i = 3 then 2 else i)"

    23 text{*

    24 @{term"h 3 = 2"}

    25 @{term"h i  = i"}

    26 *}

    28 text{*

    29 @{thm[display] numeral_0_eq_0[no_vars]}

    30 \rulename{numeral_0_eq_0}

    32 @{thm[display] numeral_1_eq_1[no_vars]}

    33 \rulename{numeral_1_eq_1}

    35 @{thm[display] add_2_eq_Suc[no_vars]}

    36 \rulename{add_2_eq_Suc}

    38 @{thm[display] add_2_eq_Suc'[no_vars]}

    39 \rulename{add_2_eq_Suc'}

    41 @{thm[display] add_assoc[no_vars]}

    42 \rulename{add_assoc}

    44 @{thm[display] add_commute[no_vars]}

    45 \rulename{add_commute}

    47 @{thm[display] add_left_commute[no_vars]}

    48 \rulename{add_left_commute}

    50 these form add_ac; similarly there is mult_ac

    51 *}

    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

    63 text{*

    65 @{thm[display] div_le_mono[no_vars]}

    66 \rulename{div_le_mono}

    68 @{thm[display] diff_mult_distrib[no_vars]}

    69 \rulename{diff_mult_distrib}

    71 @{thm[display] mod_mult_distrib[no_vars]}

    72 \rulename{mod_mult_distrib}

    74 @{thm[display] nat_diff_split[no_vars]}

    75 \rulename{nat_diff_split}

    76 *}

    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

    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

    92 text{*

    93 @{thm[display] mod_if[no_vars]}

    94 \rulename{mod_if}

    96 @{thm[display] mod_div_equality[no_vars]}

    97 \rulename{mod_div_equality}

   100 @{thm[display] div_mult1_eq[no_vars]}

   101 \rulename{div_mult1_eq}

   103 @{thm[display] mod_mult_right_eq[no_vars]}

   104 \rulename{mod_mult_right_eq}

   106 @{thm[display] div_mult2_eq[no_vars]}

   107 \rulename{div_mult2_eq}

   109 @{thm[display] mod_mult2_eq[no_vars]}

   110 \rulename{mod_mult2_eq}

   112 @{thm[display] div_mult_mult1[no_vars]}

   113 \rulename{div_mult_mult1}

   115 @{thm[display] div_by_0 [no_vars]}

   116 \rulename{div_by_0}

   118 @{thm[display] mod_by_0 [no_vars]}

   119 \rulename{mod_by_0}

   121 @{thm[display] dvd_antisym[no_vars]}

   122 \rulename{dvd_antisym}

   124 @{thm[display] dvd_add[no_vars]}

   125 \rulename{dvd_add}

   127 For the integers, I'd list a few theorems that somehow involve negative

   128 numbers.*}

   131 text{*

   132 Division, remainder of negatives

   135 @{thm[display] pos_mod_sign[no_vars]}

   136 \rulename{pos_mod_sign}

   138 @{thm[display] pos_mod_bound[no_vars]}

   139 \rulename{pos_mod_bound}

   141 @{thm[display] neg_mod_sign[no_vars]}

   142 \rulename{neg_mod_sign}

   144 @{thm[display] neg_mod_bound[no_vars]}

   145 \rulename{neg_mod_bound}

   147 @{thm[display] zdiv_zadd1_eq[no_vars]}

   148 \rulename{zdiv_zadd1_eq}

   150 @{thm[display] mod_add_eq[no_vars]}

   151 \rulename{mod_add_eq}

   153 @{thm[display] zdiv_zmult1_eq[no_vars]}

   154 \rulename{zdiv_zmult1_eq}

   156 @{thm[display] zmod_zmult1_eq[no_vars]}

   157 \rulename{zmod_zmult1_eq}

   159 @{thm[display] zdiv_zmult2_eq[no_vars]}

   160 \rulename{zdiv_zmult2_eq}

   162 @{thm[display] zmod_zmult2_eq[no_vars]}

   163 \rulename{zmod_zmult2_eq}

   164 *}

   166 lemma "abs (x+y) \<le> abs x + abs (y :: int)"

   167 by arith

   169 lemma "abs (2*x) = 2 * abs (x :: int)"

   170 by (simp add: abs_if)

   173 text {*Induction rules for the Integers

   175 @{thm[display] int_ge_induct[no_vars]}

   176 \rulename{int_ge_induct}

   178 @{thm[display] int_gr_induct[no_vars]}

   179 \rulename{int_gr_induct}

   181 @{thm[display] int_le_induct[no_vars]}

   182 \rulename{int_le_induct}

   184 @{thm[display] int_less_induct[no_vars]}

   185 \rulename{int_less_induct}

   186 *}

   188 text {*FIELDS

   190 @{thm[display] dense[no_vars]}

   191 \rulename{dense}

   193 @{thm[display] times_divide_eq_right[no_vars]}

   194 \rulename{times_divide_eq_right}

   196 @{thm[display] times_divide_eq_left[no_vars]}

   197 \rulename{times_divide_eq_left}

   199 @{thm[display] divide_divide_eq_right[no_vars]}

   200 \rulename{divide_divide_eq_right}

   202 @{thm[display] divide_divide_eq_left[no_vars]}

   203 \rulename{divide_divide_eq_left}

   205 @{thm[display] minus_divide_left[no_vars]}

   206 \rulename{minus_divide_left}

   208 @{thm[display] minus_divide_right[no_vars]}

   209 \rulename{minus_divide_right}

   211 This last NOT a simprule

   213 @{thm[display] add_divide_distrib[no_vars]}

   214 \rulename{add_divide_distrib}

   215 *}

   217 lemma "3/4 < (7/8 :: real)"

   218 by simp

   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

   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

   240 text{*

   241 Ring and Field

   243 Requires a field, or else an ordered ring

   245 @{thm[display] mult_eq_0_iff[no_vars]}

   246 \rulename{mult_eq_0_iff}

   248 @{thm[display] mult_cancel_right[no_vars]}

   249 \rulename{mult_cancel_right}

   251 @{thm[display] mult_cancel_left[no_vars]}

   252 \rulename{mult_cancel_left}

   253 *}

   255 text{*

   256 effect of show sorts on the above

   258 @{thm[display,show_sorts] mult_cancel_left[no_vars]}

   259 \rulename{mult_cancel_left}

   260 *}

   262 text{*

   263 absolute value

   265 @{thm[display] abs_mult[no_vars]}

   266 \rulename{abs_mult}

   268 @{thm[display] abs_le_iff[no_vars]}

   269 \rulename{abs_le_iff}

   271 @{thm[display] abs_triangle_ineq[no_vars]}

   272 \rulename{abs_triangle_ineq}

   274 @{thm[display] power_add[no_vars]}

   275 \rulename{power_add}

   277 @{thm[display] power_mult[no_vars]}

   278 \rulename{power_mult}

   280 @{thm[display] power_abs[no_vars]}

   281 \rulename{power_abs}

   284 *}

   287 end

author	wenzelm
	Sat, 08 May 2010 19:14:13 +0200
changeset 36754	403585a89772
parent 33750	0a0d6d79d984
child 37216	3165bc303f66
permissions	-rw-r--r--