doc-src/TutorialI/Types/Numbers.thy
 author nipkow Wed Dec 06 13:22:58 2000 +0100 (2000-12-06) changeset 10608 620647438780 parent 10603 539735ddaea9 child 10764 329d5f4aa43c permissions -rw-r--r--
*** empty log message ***
```     1 (* ID:         \$Id\$ *)
```
```     2 theory Numbers = Main:
```
```     3
```
```     4 ML "Pretty.setmargin 64"
```
```     5
```
```     6
```
```     7 text{*
```
```     8
```
```     9 numeric literals; default simprules; can re-orient
```
```    10 *}
```
```    11
```
```    12 lemma "#2 * m = m + m"
```
```    13 oops
```
```    14
```
```    15 text{*
```
```    16 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{0}}\isanewline
```
```    17 \isanewline
```
```    18 goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
```
```    19 {\isacharparenleft}{\isacharhash}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m\isanewline
```
```    20 \ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}{\isacharhash}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m
```
```    21
```
```    22
```
```    23 @{thm[display] numeral_0_eq_0[no_vars]}
```
```    24 \rulename{numeral_0_eq_0}
```
```    25
```
```    26 @{thm[display] numeral_1_eq_1[no_vars]}
```
```    27 \rulename{numeral_1_eq_1}
```
```    28
```
```    29 @{thm[display] add_2_eq_Suc[no_vars]}
```
```    30 \rulename{add_2_eq_Suc}
```
```    31
```
```    32 @{thm[display] add_2_eq_Suc'[no_vars]}
```
```    33 \rulename{add_2_eq_Suc'}
```
```    34
```
```    35 @{thm[display] add_assoc[no_vars]}
```
```    36 \rulename{add_assoc}
```
```    37
```
```    38 @{thm[display] add_commute[no_vars]}
```
```    39 \rulename{add_commute}
```
```    40
```
```    41 @{thm[display] add_left_commute[no_vars]}
```
```    42 \rulename{add_left_commute}
```
```    43
```
```    44 these form add_ac; similarly there is mult_ac
```
```    45 *}
```
```    46
```
```    47 lemma "Suc(i + j*l*k + m*n) = f (n*m + i + k*j*l)"
```
```    48 apply (simp add: add_ac mult_ac)
```
```    49 oops
```
```    50
```
```    51 text{*
```
```    52 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{0}}\isanewline
```
```    53 \isanewline
```
```    54 goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
```
```    55 Suc\ {\isacharparenleft}i\ {\isacharplus}\ j\ {\isacharasterisk}\ l\ {\isacharasterisk}\ k\ {\isacharplus}\ m\ {\isacharasterisk}\ n{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}n\ {\isacharasterisk}\ m\ {\isacharplus}\ i\ {\isacharplus}\ k\ {\isacharasterisk}\ j\ {\isacharasterisk}\ l{\isacharparenright}\isanewline
```
```    56 \ {\isadigit{1}}{\isachardot}\ Suc\ {\isacharparenleft}i\ {\isacharplus}\ j\ {\isacharasterisk}\ l\ {\isacharasterisk}\ k\ {\isacharplus}\ m\ {\isacharasterisk}\ n{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}n\ {\isacharasterisk}\ m\ {\isacharplus}\ i\ {\isacharplus}\ k\ {\isacharasterisk}\ j\ {\isacharasterisk}\ l{\isacharparenright}
```
```    57
```
```    58 proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline
```
```    59 \isanewline
```
```    60 goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
```
```    61 Suc\ {\isacharparenleft}i\ {\isacharplus}\ j\ {\isacharasterisk}\ l\ {\isacharasterisk}\ k\ {\isacharplus}\ m\ {\isacharasterisk}\ n{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}n\ {\isacharasterisk}\ m\ {\isacharplus}\ i\ {\isacharplus}\ k\ {\isacharasterisk}\ j\ {\isacharasterisk}\ l{\isacharparenright}\isanewline
```
```    62 \ {\isadigit{1}}{\isachardot}\ Suc\ {\isacharparenleft}i\ {\isacharplus}\ {\isacharparenleft}m\ {\isacharasterisk}\ n\ {\isacharplus}\ j\ {\isacharasterisk}\ {\isacharparenleft}k\ {\isacharasterisk}\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
```
```    63 \ \ \ \ f\ {\isacharparenleft}i\ {\isacharplus}\ {\isacharparenleft}m\ {\isacharasterisk}\ n\ {\isacharplus}\ j\ {\isacharasterisk}\ {\isacharparenleft}k\ {\isacharasterisk}\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}
```
```    64 *}
```
```    65
```
```    66 text{*
```
```    67
```
```    68 @{thm[display] mult_le_mono[no_vars]}
```
```    69 \rulename{mult_le_mono}
```
```    70
```
```    71 @{thm[display] mult_less_mono1[no_vars]}
```
```    72 \rulename{mult_less_mono1}
```
```    73
```
```    74 @{thm[display] div_le_mono[no_vars]}
```
```    75 \rulename{div_le_mono}
```
```    76
```
```    77 @{thm[display] add_mult_distrib[no_vars]}
```
```    78 \rulename{add_mult_distrib}
```
```    79
```
```    80 @{thm[display] diff_mult_distrib[no_vars]}
```
```    81 \rulename{diff_mult_distrib}
```
```    82
```
```    83 @{thm[display] mod_mult_distrib[no_vars]}
```
```    84 \rulename{mod_mult_distrib}
```
```    85
```
```    86 @{thm[display] nat_diff_split[no_vars]}
```
```    87 \rulename{nat_diff_split}
```
```    88 *}
```
```    89
```
```    90
```
```    91 lemma "(n-1)*(n+1) = n*n - 1"
```
```    92 apply (simp split: nat_diff_split)
```
```    93 done
```
```    94
```
```    95 text{*
```
```    96 @{thm[display] mod_if[no_vars]}
```
```    97 \rulename{mod_if}
```
```    98
```
```    99 @{thm[display] mod_div_equality[no_vars]}
```
```   100 \rulename{mod_div_equality}
```
```   101
```
```   102
```
```   103 @{thm[display] div_mult1_eq[no_vars]}
```
```   104 \rulename{div_mult1_eq}
```
```   105
```
```   106 @{thm[display] mod_mult1_eq[no_vars]}
```
```   107 \rulename{mod_mult1_eq}
```
```   108
```
```   109 @{thm[display] div_mult2_eq[no_vars]}
```
```   110 \rulename{div_mult2_eq}
```
```   111
```
```   112 @{thm[display] mod_mult2_eq[no_vars]}
```
```   113 \rulename{mod_mult2_eq}
```
```   114
```
```   115 @{thm[display] div_mult_mult1[no_vars]}
```
```   116 \rulename{div_mult_mult1}
```
```   117
```
```   118 @{thm[display] DIVISION_BY_ZERO_DIV[no_vars]}
```
```   119 \rulename{DIVISION_BY_ZERO_DIV}
```
```   120
```
```   121 @{thm[display] DIVISION_BY_ZERO_MOD[no_vars]}
```
```   122 \rulename{DIVISION_BY_ZERO_MOD}
```
```   123
```
```   124 @{thm[display] dvd_anti_sym[no_vars]}
```
```   125 \rulename{dvd_anti_sym}
```
```   126
```
```   127 @{thm[display] dvd_add[no_vars]}
```
```   128 \rulename{dvd_add}
```
```   129
```
```   130 For the integers, I'd list a few theorems that somehow involve negative
```
```   131 numbers.
```
```   132
```
```   133 Division, remainder of negatives
```
```   134
```
```   135
```
```   136 @{thm[display] pos_mod_sign[no_vars]}
```
```   137 \rulename{pos_mod_sign}
```
```   138
```
```   139 @{thm[display] pos_mod_bound[no_vars]}
```
```   140 \rulename{pos_mod_bound}
```
```   141
```
```   142 @{thm[display] neg_mod_sign[no_vars]}
```
```   143 \rulename{neg_mod_sign}
```
```   144
```
```   145 @{thm[display] neg_mod_bound[no_vars]}
```
```   146 \rulename{neg_mod_bound}
```
```   147
```
```   148 @{thm[display] zdiv_zadd1_eq[no_vars]}
```
```   149 \rulename{zdiv_zadd1_eq}
```
```   150
```
```   151 @{thm[display] zmod_zadd1_eq[no_vars]}
```
```   152 \rulename{zmod_zadd1_eq}
```
```   153
```
```   154 @{thm[display] zdiv_zmult1_eq[no_vars]}
```
```   155 \rulename{zdiv_zmult1_eq}
```
```   156
```
```   157 @{thm[display] zmod_zmult1_eq[no_vars]}
```
```   158 \rulename{zmod_zmult1_eq}
```
```   159
```
```   160 @{thm[display] zdiv_zmult2_eq[no_vars]}
```
```   161 \rulename{zdiv_zmult2_eq}
```
```   162
```
```   163 @{thm[display] zmod_zmult2_eq[no_vars]}
```
```   164 \rulename{zmod_zmult2_eq}
```
```   165
```
```   166 @{thm[display] abs_mult[no_vars]}
```
```   167 \rulename{abs_mult}
```
```   168 *}
```
```   169
```
```   170 (*NO REALS YET;  Needs HOL-Real as parent
```
```   171 For the reals, perhaps just a few results to indicate what is there.
```
```   172
```
```   173 @{thm[display] realpow_abs[no_vars]}
```
```   174 \rulename{realpow_abs}
```
```   175
```
```   176 More once rinv (the most important constant) is sorted.
```
```   177 *)
```
```   178
```
```   179 end
```