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