wneuper/isa: doc-src/TutorialI/Types/Numbers.thy@729a36e469ec

     1 (* ID:         $Id$ *)

     2 theory Numbers = Real:

     4 ML "Pretty.setmargin 64"

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

     7 text{*

     9 numeric literals; default simprules; can re-orient

    10 *}

    12 lemma "#2 * m = m + m"

    13 txt{*

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

    15 *};

    16 oops

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

    19 recdef h "{}"

    20 "h i = (if i = #3 then #2 else i)"

    22 text{*

    23 @{term"h #3 = #2"}

    24 @{term"h i  = i"}

    25 *}

    27 text{*

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

    29 \rulename{numeral_0_eq_0}

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

    32 \rulename{numeral_1_eq_1}

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

    35 \rulename{add_2_eq_Suc}

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

    38 \rulename{add_2_eq_Suc'}

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

    41 \rulename{add_assoc}

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

    44 \rulename{add_commute}

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

    47 \rulename{add_left_commute}

    49 these form add_ac; similarly there is mult_ac

    50 *}

    52 lemma "Suc(i + j*l*k + m*n) = f (n*m + i + k*j*l)"

    53 txt{*

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

    55 *};

    56 apply (simp add: add_ac mult_ac)

    57 txt{*

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

    59 *};

    60 oops

    62 text{*

    63 @{thm[display] mult_le_mono[no_vars]}

    64 \rulename{mult_le_mono}

    66 @{thm[display] mult_less_mono1[no_vars]}

    67 \rulename{mult_less_mono1}

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

    70 \rulename{div_le_mono}

    72 @{thm[display] add_mult_distrib[no_vars]}

    73 \rulename{add_mult_distrib}

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

    76 \rulename{diff_mult_distrib}

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

    79 \rulename{mod_mult_distrib}

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

    82 \rulename{nat_diff_split}

    83 *}

    86 lemma "(n-1)*(n+1) = n*n - 1"

    87 apply (simp split: nat_diff_split)

    88 done

    90 text{*

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

    92 \rulename{mod_if}

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

    95 \rulename{mod_div_equality}

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

    99 \rulename{div_mult1_eq}

   101 @{thm[display] mod_mult1_eq[no_vars]}

   102 \rulename{mod_mult1_eq}

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

   105 \rulename{div_mult2_eq}

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

   108 \rulename{mod_mult2_eq}

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

   111 \rulename{div_mult_mult1}

   113 @{thm[display] DIVISION_BY_ZERO_DIV[no_vars]}

   114 \rulename{DIVISION_BY_ZERO_DIV}

   116 @{thm[display] DIVISION_BY_ZERO_MOD[no_vars]}

   117 \rulename{DIVISION_BY_ZERO_MOD}

   119 @{thm[display] dvd_anti_sym[no_vars]}

   120 \rulename{dvd_anti_sym}

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

   123 \rulename{dvd_add}

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

   126 numbers.

   128 Division, remainder of negatives

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

   132 \rulename{pos_mod_sign}

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

   135 \rulename{pos_mod_bound}

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

   138 \rulename{neg_mod_sign}

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

   141 \rulename{neg_mod_bound}

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

   144 \rulename{zdiv_zadd1_eq}

   146 @{thm[display] zmod_zadd1_eq[no_vars]}

   147 \rulename{zmod_zadd1_eq}

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

   150 \rulename{zdiv_zmult1_eq}

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

   153 \rulename{zmod_zmult1_eq}

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

   156 \rulename{zdiv_zmult2_eq}

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

   159 \rulename{zmod_zmult2_eq}

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

   162 \rulename{abs_mult}

   163 *}

   165 lemma "\<lbrakk>abs x < a; abs y < b\<rbrakk> \<Longrightarrow> abs x + abs y < (a + b :: int)"

   166 by arith

   168 text {*REALS

   170 @{thm[display] realpow_abs[no_vars]}

   171 \rulename{realpow_abs}

   173 @{thm[display] real_dense[no_vars]}

   174 \rulename{real_dense}

   176 @{thm[display] realpow_abs[no_vars]}

   177 \rulename{realpow_abs}

   179 @{thm[display] real_times_divide1_eq[no_vars]}

   180 \rulename{real_times_divide1_eq}

   182 @{thm[display] real_times_divide2_eq[no_vars]}

   183 \rulename{real_times_divide2_eq}

   185 @{thm[display] real_divide_divide1_eq[no_vars]}

   186 \rulename{real_divide_divide1_eq}

   188 @{thm[display] real_divide_divide2_eq[no_vars]}

   189 \rulename{real_divide_divide2_eq}

   191 @{thm[display] real_minus_divide_eq[no_vars]}

   192 \rulename{real_minus_divide_eq}

   194 @{thm[display] real_divide_minus_eq[no_vars]}

   195 \rulename{real_divide_minus_eq}

   197 This last NOT a simprule

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

   200 \rulename{real_add_divide_distrib}

   201 *}

   203 end

author	paulson
	Fri, 12 Jan 2001 16:10:56 +0100
changeset 10880	729a36e469ec
parent 10777	a5a6255748c3
child 11174	96a533d300a6
permissions	-rw-r--r--