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