1.1 --- a/src/HOL/ex/BinEx.thy Fri Oct 05 21:50:37 2001 +0200
1.2 +++ b/src/HOL/ex/BinEx.thy Fri Oct 05 21:52:39 2001 +0200
1.3 @@ -12,75 +12,75 @@
1.4
1.5 text {* Addition *}
1.6
1.7 -lemma "(#13::int) + #19 = #32"
1.8 +lemma "(# 13::int) + # 19 = # 32"
1.9 by simp
1.10
1.11 -lemma "(#1234::int) + #5678 = #6912"
1.12 +lemma "(# 1234::int) + # 5678 = # 6912"
1.13 by simp
1.14
1.15 -lemma "(#1359::int) + #-2468 = #-1109"
1.16 +lemma "(# 1359::int) + # -2468 = # -1109"
1.17 by simp
1.18
1.19 -lemma "(#93746::int) + #-46375 = #47371"
1.20 +lemma "(# 93746::int) + # -46375 = # 47371"
1.21 by simp
1.22
1.23
1.24 text {* \medskip Negation *}
1.25
1.26 -lemma "- (#65745::int) = #-65745"
1.27 +lemma "- (# 65745::int) = # -65745"
1.28 by simp
1.29
1.30 -lemma "- (#-54321::int) = #54321"
1.31 +lemma "- (# -54321::int) = # 54321"
1.32 by simp
1.33
1.34
1.35 text {* \medskip Multiplication *}
1.36
1.37 -lemma "(#13::int) * #19 = #247"
1.38 +lemma "(# 13::int) * # 19 = # 247"
1.39 by simp
1.40
1.41 -lemma "(#-84::int) * #51 = #-4284"
1.42 +lemma "(# -84::int) * # 51 = # -4284"
1.43 by simp
1.44
1.45 -lemma "(#255::int) * #255 = #65025"
1.46 +lemma "(# 255::int) * # 255 = # 65025"
1.47 by simp
1.48
1.49 -lemma "(#1359::int) * #-2468 = #-3354012"
1.50 +lemma "(# 1359::int) * # -2468 = # -3354012"
1.51 by simp
1.52
1.53 -lemma "(#89::int) * #10 \<noteq> #889"
1.54 +lemma "(# 89::int) * # 10 \<noteq> # 889"
1.55 by simp
1.56
1.57 -lemma "(#13::int) < #18 - #4"
1.58 +lemma "(# 13::int) < # 18 - # 4"
1.59 by simp
1.60
1.61 -lemma "(#-345::int) < #-242 + #-100"
1.62 +lemma "(# -345::int) < # -242 + # -100"
1.63 by simp
1.64
1.65 -lemma "(#13557456::int) < #18678654"
1.66 +lemma "(# 13557456::int) < # 18678654"
1.67 by simp
1.68
1.69 -lemma "(#999999::int) \<le> (#1000001 + #1) - #2"
1.70 +lemma "(# 999999::int) \<le> (# 1000001 + Numeral1) - # 2"
1.71 by simp
1.72
1.73 -lemma "(#1234567::int) \<le> #1234567"
1.74 +lemma "(# 1234567::int) \<le> # 1234567"
1.75 by simp
1.76
1.77
1.78 text {* \medskip Quotient and Remainder *}
1.79
1.80 -lemma "(#10::int) div #3 = #3"
1.81 +lemma "(# 10::int) div # 3 = # 3"
1.82 by simp
1.83
1.84 -lemma "(#10::int) mod #3 = #1"
1.85 +lemma "(# 10::int) mod # 3 = Numeral1"
1.86 by simp
1.87
1.88 text {* A negative divisor *}
1.89
1.90 -lemma "(#10::int) div #-3 = #-4"
1.91 +lemma "(# 10::int) div # -3 = # -4"
1.92 by simp
1.93
1.94 -lemma "(#10::int) mod #-3 = #-2"
1.95 +lemma "(# 10::int) mod # -3 = # -2"
1.96 by simp
1.97
1.98 text {*
1.99 @@ -88,50 +88,50 @@
1.100 convention but not with the hardware of most computers}
1.101 *}
1.102
1.103 -lemma "(#-10::int) div #3 = #-4"
1.104 +lemma "(# -10::int) div # 3 = # -4"
1.105 by simp
1.106
1.107 -lemma "(#-10::int) mod #3 = #2"
1.108 +lemma "(# -10::int) mod # 3 = # 2"
1.109 by simp
1.110
1.111 text {* A negative dividend \emph{and} divisor *}
1.112
1.113 -lemma "(#-10::int) div #-3 = #3"
1.114 +lemma "(# -10::int) div # -3 = # 3"
1.115 by simp
1.116
1.117 -lemma "(#-10::int) mod #-3 = #-1"
1.118 +lemma "(# -10::int) mod # -3 = # -1"
1.119 by simp
1.120
1.121 text {* A few bigger examples *}
1.122
1.123 -lemma "(#8452::int) mod #3 = #1"
1.124 +lemma "(# 8452::int) mod # 3 = Numeral1"
1.125 by simp
1.126
1.127 -lemma "(#59485::int) div #434 = #137"
1.128 +lemma "(# 59485::int) div # 434 = # 137"
1.129 by simp
1.130
1.131 -lemma "(#1000006::int) mod #10 = #6"
1.132 +lemma "(# 1000006::int) mod # 10 = # 6"
1.133 by simp
1.134
1.135
1.136 text {* \medskip Division by shifting *}
1.137
1.138 -lemma "#10000000 div #2 = (#5000000::int)"
1.139 +lemma "# 10000000 div # 2 = (# 5000000::int)"
1.140 by simp
1.141
1.142 -lemma "#10000001 mod #2 = (#1::int)"
1.143 +lemma "# 10000001 mod # 2 = (Numeral1::int)"
1.144 by simp
1.145
1.146 -lemma "#10000055 div #32 = (#312501::int)"
1.147 +lemma "# 10000055 div # 32 = (# 312501::int)"
1.148 by simp
1.149
1.150 -lemma "#10000055 mod #32 = (#23::int)"
1.151 +lemma "# 10000055 mod # 32 = (# 23::int)"
1.152 by simp
1.153
1.154 -lemma "#100094 div #144 = (#695::int)"
1.155 +lemma "# 100094 div # 144 = (# 695::int)"
1.156 by simp
1.157
1.158 -lemma "#100094 mod #144 = (#14::int)"
1.159 +lemma "# 100094 mod # 144 = (# 14::int)"
1.160 by simp
1.161
1.162
1.163 @@ -139,95 +139,95 @@
1.164
1.165 text {* Successor *}
1.166
1.167 -lemma "Suc #99999 = #100000"
1.168 +lemma "Suc # 99999 = # 100000"
1.169 by (simp add: Suc_nat_number_of)
1.170 -- {* not a default rewrite since sometimes we want to have @{text "Suc #nnn"} *}
1.171
1.172
1.173 text {* \medskip Addition *}
1.174
1.175 -lemma "(#13::nat) + #19 = #32"
1.176 +lemma "(# 13::nat) + # 19 = # 32"
1.177 by simp
1.178
1.179 -lemma "(#1234::nat) + #5678 = #6912"
1.180 +lemma "(# 1234::nat) + # 5678 = # 6912"
1.181 by simp
1.182
1.183 -lemma "(#973646::nat) + #6475 = #980121"
1.184 +lemma "(# 973646::nat) + # 6475 = # 980121"
1.185 by simp
1.186
1.187
1.188 text {* \medskip Subtraction *}
1.189
1.190 -lemma "(#32::nat) - #14 = #18"
1.191 +lemma "(# 32::nat) - # 14 = # 18"
1.192 by simp
1.193
1.194 -lemma "(#14::nat) - #15 = #0"
1.195 +lemma "(# 14::nat) - # 15 = Numeral0"
1.196 by simp
1.197
1.198 -lemma "(#14::nat) - #1576644 = #0"
1.199 +lemma "(# 14::nat) - # 1576644 = Numeral0"
1.200 by simp
1.201
1.202 -lemma "(#48273776::nat) - #3873737 = #44400039"
1.203 +lemma "(# 48273776::nat) - # 3873737 = # 44400039"
1.204 by simp
1.205
1.206
1.207 text {* \medskip Multiplication *}
1.208
1.209 -lemma "(#12::nat) * #11 = #132"
1.210 +lemma "(# 12::nat) * # 11 = # 132"
1.211 by simp
1.212
1.213 -lemma "(#647::nat) * #3643 = #2357021"
1.214 +lemma "(# 647::nat) * # 3643 = # 2357021"
1.215 by simp
1.216
1.217
1.218 text {* \medskip Quotient and Remainder *}
1.219
1.220 -lemma "(#10::nat) div #3 = #3"
1.221 +lemma "(# 10::nat) div # 3 = # 3"
1.222 by simp
1.223
1.224 -lemma "(#10::nat) mod #3 = #1"
1.225 +lemma "(# 10::nat) mod # 3 = Numeral1"
1.226 by simp
1.227
1.228 -lemma "(#10000::nat) div #9 = #1111"
1.229 +lemma "(# 10000::nat) div # 9 = # 1111"
1.230 by simp
1.231
1.232 -lemma "(#10000::nat) mod #9 = #1"
1.233 +lemma "(# 10000::nat) mod # 9 = Numeral1"
1.234 by simp
1.235
1.236 -lemma "(#10000::nat) div #16 = #625"
1.237 +lemma "(# 10000::nat) div # 16 = # 625"
1.238 by simp
1.239
1.240 -lemma "(#10000::nat) mod #16 = #0"
1.241 +lemma "(# 10000::nat) mod # 16 = Numeral0"
1.242 by simp
1.243
1.244
1.245 text {* \medskip Testing the cancellation of complementary terms *}
1.246
1.247 -lemma "y + (x + -x) = (#0::int) + y"
1.248 +lemma "y + (x + -x) = (Numeral0::int) + y"
1.249 by simp
1.250
1.251 -lemma "y + (-x + (- y + x)) = (#0::int)"
1.252 +lemma "y + (-x + (- y + x)) = (Numeral0::int)"
1.253 by simp
1.254
1.255 -lemma "-x + (y + (- y + x)) = (#0::int)"
1.256 +lemma "-x + (y + (- y + x)) = (Numeral0::int)"
1.257 by simp
1.258
1.259 -lemma "x + (x + (- x + (- x + (- y + - z)))) = (#0::int) - y - z"
1.260 +lemma "x + (x + (- x + (- x + (- y + - z)))) = (Numeral0::int) - y - z"
1.261 by simp
1.262
1.263 -lemma "x + x - x - x - y - z = (#0::int) - y - z"
1.264 +lemma "x + x - x - x - y - z = (Numeral0::int) - y - z"
1.265 by simp
1.266
1.267 -lemma "x + y + z - (x + z) = y - (#0::int)"
1.268 +lemma "x + y + z - (x + z) = y - (Numeral0::int)"
1.269 by simp
1.270
1.271 -lemma "x + (y + (y + (y + (-x + -x)))) = (#0::int) + y - x + y + y"
1.272 +lemma "x + (y + (y + (y + (-x + -x)))) = (Numeral0::int) + y - x + y + y"
1.273 by simp
1.274
1.275 -lemma "x + (y + (y + (y + (-y + -x)))) = y + (#0::int) + y"
1.276 +lemma "x + (y + (y + (y + (-y + -x)))) = y + (Numeral0::int) + y"
1.277 by simp
1.278
1.279 -lemma "x + y - x + z - x - y - z + x < (#1::int)"
1.280 +lemma "x + y - x + z - x - y - z + x < (Numeral1::int)"
1.281 by simp
1.282
1.283
1.284 @@ -302,7 +302,7 @@
1.285 apply simp_all
1.286 done
1.287
1.288 -lemma normal_Pls_eq_0: "w \<in> normal ==> (w = Pls) = (number_of w = (#0::int))"
1.289 +lemma normal_Pls_eq_0: "w \<in> normal ==> (w = Pls) = (number_of w = (Numeral0::int))"
1.290 apply (erule normal.induct)
1.291 apply auto
1.292 done