1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/TutorialI/Types/Numbers.thy	Wed Dec 06 11:47:21 2000 +0100
     1.3 @@ -0,0 +1,179 @@
     1.4 +(* ID:         $Id$ *)
     1.5 +theory Numbers = Main:
     1.6 +
     1.7 +ML "Pretty.setmargin 64"
     1.8 +
     1.9 +
    1.10 +text{*
    1.11 +
    1.12 +numeric literals; default simprules; can re-orient
    1.13 +*}
    1.14 +
    1.15 +lemma "#2 * m = m + m"
    1.16 +oops
    1.17 +
    1.18 +text{*
    1.19 +proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{0}}\isanewline
    1.20 +\isanewline
    1.21 +goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
    1.22 +{\isacharparenleft}{\isacharhash}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m\isanewline
    1.23 +\ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}{\isacharhash}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m
    1.24 +
    1.25 +
    1.26 +@{thm[display] numeral_0_eq_0[no_vars]}
    1.27 +\rulename{numeral_0_eq_0}
    1.28 +
    1.29 +@{thm[display] numeral_1_eq_1[no_vars]}
    1.30 +\rulename{numeral_1_eq_1}
    1.31 +
    1.32 +@{thm[display] add_2_eq_Suc[no_vars]}
    1.33 +\rulename{add_2_eq_Suc}
    1.34 +
    1.35 +@{thm[display] add_2_eq_Suc'[no_vars]}
    1.36 +\rulename{add_2_eq_Suc'}
    1.37 +
    1.38 +@{thm[display] add_assoc[no_vars]}
    1.39 +\rulename{add_assoc}
    1.40 +
    1.41 +@{thm[display] add_commute[no_vars]}
    1.42 +\rulename{add_commute}
    1.43 +
    1.44 +@{thm[display] add_left_commute[no_vars]}
    1.45 +\rulename{add_left_commute}
    1.46 +
    1.47 +these form add_ac; similarly there is mult_ac
    1.48 +*}
    1.49 +
    1.50 +lemma "Suc(i + j*l*k + m*n) = f (n*m + i + k*j*l)"
    1.51 +apply (simp add: add_ac mult_ac)
    1.52 +oops
    1.53 +
    1.54 +text{*
    1.55 +proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{0}}\isanewline
    1.56 +\isanewline
    1.57 +goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
    1.58 +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
    1.59 +\ {\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}
    1.60 +
    1.61 +proof\ {\isacharparenleft}prove{\isacharparenright}{\isacharcolon}\ step\ {\isadigit{1}}\isanewline
    1.62 +\isanewline
    1.63 +goal\ {\isacharparenleft}lemma{\isacharparenright}{\isacharcolon}\isanewline
    1.64 +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
    1.65 +\ {\isadigit{1}}{\isachardot}\ Suc\ {\isacharparenleft}i\ {\isacharplus}\ {\isacharparenleft}m\ {\isacharasterisk}\ n\ {\isacharplus}\ j\ {\isacharasterisk}\ {\isacharparenleft}k\ {\isacharasterisk}\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
    1.66 +\ \ \ \ f\ {\isacharparenleft}i\ {\isacharplus}\ {\isacharparenleft}m\ {\isacharasterisk}\ n\ {\isacharplus}\ j\ {\isacharasterisk}\ {\isacharparenleft}k\ {\isacharasterisk}\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}
    1.67 +*}
    1.68 +
    1.69 +text{*
    1.70 +
    1.71 +@{thm[display] mult_le_mono[no_vars]}
    1.72 +\rulename{mult_le_mono}
    1.73 +
    1.74 +@{thm[display] mult_less_mono1[no_vars]}
    1.75 +\rulename{mult_less_mono1}
    1.76 +
    1.77 +@{thm[display] div_le_mono[no_vars]}
    1.78 +\rulename{div_le_mono}
    1.79 +
    1.80 +@{thm[display] add_mult_distrib[no_vars]}
    1.81 +\rulename{add_mult_distrib}
    1.82 +
    1.83 +@{thm[display] diff_mult_distrib[no_vars]}
    1.84 +\rulename{diff_mult_distrib}
    1.85 +
    1.86 +@{thm[display] mod_mult_distrib[no_vars]}
    1.87 +\rulename{mod_mult_distrib}
    1.88 +
    1.89 +@{thm[display] nat_diff_split[no_vars]}
    1.90 +\rulename{nat_diff_split}
    1.91 +*}
    1.92 +
    1.93 +
    1.94 +lemma "(n-1)*(n+1) = n*n - 1"
    1.95 +apply (simp split: nat_diff_split)
    1.96 +done
    1.97 +
    1.98 +text{*
    1.99 +@{thm[display] mod_if[no_vars]}
   1.100 +\rulename{mod_if}
   1.101 +
   1.102 +@{thm[display] mod_div_equality[no_vars]}
   1.103 +\rulename{mod_div_equality}
   1.104 +
   1.105 +
   1.106 +@{thm[display] div_mult1_eq[no_vars]}
   1.107 +\rulename{div_mult1_eq}
   1.108 +
   1.109 +@{thm[display] mod_mult1_eq[no_vars]}
   1.110 +\rulename{mod_mult1_eq}
   1.111 +
   1.112 +@{thm[display] div_mult2_eq[no_vars]}
   1.113 +\rulename{div_mult2_eq}
   1.114 +
   1.115 +@{thm[display] mod_mult2_eq[no_vars]}
   1.116 +\rulename{mod_mult2_eq}
   1.117 +
   1.118 +@{thm[display] div_mult_mult1[no_vars]}
   1.119 +\rulename{div_mult_mult1}
   1.120 +
   1.121 +@{thm[display] DIVISION_BY_ZERO_DIV[no_vars]}
   1.122 +\rulename{DIVISION_BY_ZERO_DIV}
   1.123 +
   1.124 +@{thm[display] DIVISION_BY_ZERO_MOD[no_vars]}
   1.125 +\rulename{DIVISION_BY_ZERO_MOD}
   1.126 +
   1.127 +@{thm[display] dvd_anti_sym[no_vars]}
   1.128 +\rulename{dvd_anti_sym}
   1.129 +
   1.130 +@{thm[display] dvd_add[no_vars]}
   1.131 +\rulename{dvd_add}
   1.132 +
   1.133 +For the integers, I'd list a few theorems that somehow involve negative 
   1.134 +numbers.  
   1.135 +
   1.136 +Division, remainder of negatives
   1.137 +
   1.138 +
   1.139 +@{thm[display] pos_mod_sign[no_vars]}
   1.140 +\rulename{pos_mod_sign}
   1.141 +
   1.142 +@{thm[display] pos_mod_bound[no_vars]}
   1.143 +\rulename{pos_mod_bound}
   1.144 +
   1.145 +@{thm[display] neg_mod_sign[no_vars]}
   1.146 +\rulename{neg_mod_sign}
   1.147 +
   1.148 +@{thm[display] neg_mod_bound[no_vars]}
   1.149 +\rulename{neg_mod_bound}
   1.150 +
   1.151 +@{thm[display] zdiv_zadd1_eq[no_vars]}
   1.152 +\rulename{zdiv_zadd1_eq}
   1.153 +
   1.154 +@{thm[display] zmod_zadd1_eq[no_vars]}
   1.155 +\rulename{zmod_zadd1_eq}
   1.156 +
   1.157 +@{thm[display] zdiv_zmult1_eq[no_vars]}
   1.158 +\rulename{zdiv_zmult1_eq}
   1.159 +
   1.160 +@{thm[display] zmod_zmult1_eq[no_vars]}
   1.161 +\rulename{zmod_zmult1_eq}
   1.162 +
   1.163 +@{thm[display] zdiv_zmult2_eq[no_vars]}
   1.164 +\rulename{zdiv_zmult2_eq}
   1.165 +
   1.166 +@{thm[display] zmod_zmult2_eq[no_vars]}
   1.167 +\rulename{zmod_zmult2_eq}
   1.168 +
   1.169 +@{thm[display] abs_mult[no_vars]}
   1.170 +\rulename{abs_mult}
   1.171 +*}  
   1.172 +
   1.173 +(*NO REALS YET;  Needs HOL-Real as parent
   1.174 +For the reals, perhaps just a few results to indicate what is there.
   1.175 +
   1.176 +@{thm[display] realpow_abs[no_vars]}
   1.177 +\rulename{realpow_abs}
   1.178 +
   1.179 +More once rinv (the most important constant) is sorted.
   1.180 +*)  
   1.181 +
   1.182 +end