doc-src/TutorialI/Types/Numbers.thy
author wenzelm
Fri Aug 27 12:40:20 2010 +0200 (2010-08-27)
changeset 38767 d8da44a8dd25
parent 37216 3165bc303f66
child 44048 64f574163ca2
permissions -rw-r--r--
proper context for various Thy_Output options, via official configuration options in ML and Isar;
haftmann@27376
     1
theory Numbers
haftmann@27376
     2
imports Complex_Main
haftmann@27376
     3
begin
paulson@10603
     4
wenzelm@36745
     5
ML "Pretty.margin_default := 64"
wenzelm@38767
     6
declare [[thy_output_indent = 0]]  (*we don't want 5 for listing theorems*)
paulson@10603
     7
paulson@10603
     8
text{*
paulson@10603
     9
paulson@10603
    10
numeric literals; default simprules; can re-orient
paulson@10603
    11
*}
paulson@10603
    12
wenzelm@11711
    13
lemma "2 * m = m + m"
paulson@10880
    14
txt{*
paulson@10880
    15
@{subgoals[display,indent=0,margin=65]}
paulson@10880
    16
*};
paulson@10603
    17
oops
paulson@10603
    18
paulson@10880
    19
consts h :: "nat \<Rightarrow> nat"
paulson@10880
    20
recdef h "{}"
wenzelm@11711
    21
"h i = (if i = 3 then 2 else i)"
paulson@10880
    22
paulson@10603
    23
text{*
wenzelm@11711
    24
@{term"h 3 = 2"}
paulson@10880
    25
@{term"h i  = i"}
paulson@10880
    26
*}
paulson@10603
    27
paulson@10880
    28
text{*
paulson@10603
    29
@{thm[display] numeral_0_eq_0[no_vars]}
paulson@10603
    30
\rulename{numeral_0_eq_0}
paulson@10603
    31
paulson@10603
    32
@{thm[display] numeral_1_eq_1[no_vars]}
paulson@10603
    33
\rulename{numeral_1_eq_1}
paulson@10603
    34
paulson@10603
    35
@{thm[display] add_2_eq_Suc[no_vars]}
paulson@10603
    36
\rulename{add_2_eq_Suc}
paulson@10603
    37
paulson@10603
    38
@{thm[display] add_2_eq_Suc'[no_vars]}
paulson@10603
    39
\rulename{add_2_eq_Suc'}
paulson@10603
    40
paulson@10603
    41
@{thm[display] add_assoc[no_vars]}
paulson@10603
    42
\rulename{add_assoc}
paulson@10603
    43
paulson@10603
    44
@{thm[display] add_commute[no_vars]}
paulson@10603
    45
\rulename{add_commute}
paulson@10603
    46
paulson@10603
    47
@{thm[display] add_left_commute[no_vars]}
paulson@10603
    48
\rulename{add_left_commute}
paulson@10603
    49
paulson@10603
    50
these form add_ac; similarly there is mult_ac
paulson@10603
    51
*}
paulson@10603
    52
paulson@10603
    53
lemma "Suc(i + j*l*k + m*n) = f (n*m + i + k*j*l)"
paulson@10880
    54
txt{*
paulson@10880
    55
@{subgoals[display,indent=0,margin=65]}
paulson@10880
    56
*};
paulson@10603
    57
apply (simp add: add_ac mult_ac)
paulson@10880
    58
txt{*
paulson@10880
    59
@{subgoals[display,indent=0,margin=65]}
paulson@10880
    60
*};
paulson@10603
    61
oops
paulson@10603
    62
paulson@10603
    63
text{*
paulson@10603
    64
paulson@10603
    65
@{thm[display] div_le_mono[no_vars]}
paulson@10603
    66
\rulename{div_le_mono}
paulson@10603
    67
paulson@10603
    68
@{thm[display] diff_mult_distrib[no_vars]}
paulson@10603
    69
\rulename{diff_mult_distrib}
paulson@10603
    70
paulson@10603
    71
@{thm[display] mod_mult_distrib[no_vars]}
paulson@10603
    72
\rulename{mod_mult_distrib}
paulson@10603
    73
paulson@10603
    74
@{thm[display] nat_diff_split[no_vars]}
paulson@10603
    75
\rulename{nat_diff_split}
paulson@10603
    76
*}
paulson@10603
    77
paulson@10603
    78
paulson@12156
    79
lemma "(n - 1) * (n + 1) = n * n - (1::nat)"
wenzelm@12843
    80
apply (clarsimp split: nat_diff_split iff del: less_Suc0)
paulson@12156
    81
 --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@12156
    82
apply (subgoal_tac "n=0", force, arith)
paulson@12156
    83
done
paulson@12156
    84
paulson@12156
    85
wenzelm@11711
    86
lemma "(n - 2) * (n + 2) = n * n - (4::nat)"
paulson@12156
    87
apply (simp split: nat_diff_split, clarify)
paulson@11480
    88
 --{* @{subgoals[display,indent=0,margin=65]} *}
paulson@11480
    89
apply (subgoal_tac "n=0 | n=1", force, arith)
paulson@10603
    90
done
paulson@10603
    91
paulson@10603
    92
text{*
paulson@10603
    93
@{thm[display] mod_if[no_vars]}
paulson@10603
    94
\rulename{mod_if}
paulson@10603
    95
paulson@10603
    96
@{thm[display] mod_div_equality[no_vars]}
paulson@10603
    97
\rulename{mod_div_equality}
paulson@10603
    98
paulson@10603
    99
paulson@10603
   100
@{thm[display] div_mult1_eq[no_vars]}
paulson@10603
   101
\rulename{div_mult1_eq}
paulson@10603
   102
nipkow@30224
   103
@{thm[display] mod_mult_right_eq[no_vars]}
nipkow@30224
   104
\rulename{mod_mult_right_eq}
paulson@10603
   105
paulson@10603
   106
@{thm[display] div_mult2_eq[no_vars]}
paulson@10603
   107
\rulename{div_mult2_eq}
paulson@10603
   108
paulson@10603
   109
@{thm[display] mod_mult2_eq[no_vars]}
paulson@10603
   110
\rulename{mod_mult2_eq}
paulson@10603
   111
paulson@10603
   112
@{thm[display] div_mult_mult1[no_vars]}
paulson@10603
   113
\rulename{div_mult_mult1}
paulson@10603
   114
haftmann@27658
   115
@{thm[display] div_by_0 [no_vars]}
haftmann@27658
   116
\rulename{div_by_0}
paulson@10603
   117
haftmann@27658
   118
@{thm[display] mod_by_0 [no_vars]}
haftmann@27658
   119
\rulename{mod_by_0}
paulson@10603
   120
nipkow@33750
   121
@{thm[display] dvd_antisym[no_vars]}
nipkow@33750
   122
\rulename{dvd_antisym}
paulson@10603
   123
paulson@10603
   124
@{thm[display] dvd_add[no_vars]}
paulson@10603
   125
\rulename{dvd_add}
paulson@10603
   126
paulson@10603
   127
For the integers, I'd list a few theorems that somehow involve negative 
paulson@13757
   128
numbers.*}
paulson@10603
   129
paulson@13757
   130
paulson@13757
   131
text{*
paulson@10603
   132
Division, remainder of negatives
paulson@10603
   133
paulson@10603
   134
paulson@10603
   135
@{thm[display] pos_mod_sign[no_vars]}
paulson@10603
   136
\rulename{pos_mod_sign}
paulson@10603
   137
paulson@10603
   138
@{thm[display] pos_mod_bound[no_vars]}
paulson@10603
   139
\rulename{pos_mod_bound}
paulson@10603
   140
paulson@10603
   141
@{thm[display] neg_mod_sign[no_vars]}
paulson@10603
   142
\rulename{neg_mod_sign}
paulson@10603
   143
paulson@10603
   144
@{thm[display] neg_mod_bound[no_vars]}
paulson@10603
   145
\rulename{neg_mod_bound}
paulson@10603
   146
paulson@10603
   147
@{thm[display] zdiv_zadd1_eq[no_vars]}
paulson@10603
   148
\rulename{zdiv_zadd1_eq}
paulson@10603
   149
nipkow@30224
   150
@{thm[display] mod_add_eq[no_vars]}
nipkow@30224
   151
\rulename{mod_add_eq}
paulson@10603
   152
paulson@10603
   153
@{thm[display] zdiv_zmult1_eq[no_vars]}
paulson@10603
   154
\rulename{zdiv_zmult1_eq}
paulson@10603
   155
paulson@10603
   156
@{thm[display] zmod_zmult1_eq[no_vars]}
paulson@10603
   157
\rulename{zmod_zmult1_eq}
paulson@10603
   158
paulson@10603
   159
@{thm[display] zdiv_zmult2_eq[no_vars]}
paulson@10603
   160
\rulename{zdiv_zmult2_eq}
paulson@10603
   161
paulson@10603
   162
@{thm[display] zmod_zmult2_eq[no_vars]}
paulson@10603
   163
\rulename{zmod_zmult2_eq}
paulson@10603
   164
*}  
paulson@10603
   165
paulson@11174
   166
lemma "abs (x+y) \<le> abs x + abs (y :: int)"
paulson@10880
   167
by arith
paulson@10880
   168
wenzelm@11711
   169
lemma "abs (2*x) = 2 * abs (x :: int)"
paulson@16585
   170
by (simp add: abs_if) 
paulson@11174
   171
paulson@13757
   172
paulson@13757
   173
text {*Induction rules for the Integers
paulson@13757
   174
paulson@13757
   175
@{thm[display] int_ge_induct[no_vars]}
paulson@13757
   176
\rulename{int_ge_induct}
paulson@13757
   177
paulson@13757
   178
@{thm[display] int_gr_induct[no_vars]}
paulson@13757
   179
\rulename{int_gr_induct}
paulson@13757
   180
paulson@13757
   181
@{thm[display] int_le_induct[no_vars]}
paulson@13757
   182
\rulename{int_le_induct}
paulson@13757
   183
paulson@13757
   184
@{thm[display] int_less_induct[no_vars]}
paulson@13757
   185
\rulename{int_less_induct}
paulson@13757
   186
*}  
paulson@13757
   187
paulson@14400
   188
text {*FIELDS
paulson@10764
   189
paulson@14295
   190
@{thm[display] dense[no_vars]}
paulson@14295
   191
\rulename{dense}
paulson@10603
   192
paulson@14288
   193
@{thm[display] times_divide_eq_right[no_vars]}
paulson@14288
   194
\rulename{times_divide_eq_right}
paulson@10764
   195
paulson@14288
   196
@{thm[display] times_divide_eq_left[no_vars]}
paulson@14288
   197
\rulename{times_divide_eq_left}
paulson@10764
   198
paulson@14288
   199
@{thm[display] divide_divide_eq_right[no_vars]}
paulson@14288
   200
\rulename{divide_divide_eq_right}
paulson@10764
   201
paulson@14288
   202
@{thm[display] divide_divide_eq_left[no_vars]}
paulson@14288
   203
\rulename{divide_divide_eq_left}
paulson@10764
   204
paulson@14295
   205
@{thm[display] minus_divide_left[no_vars]}
paulson@14295
   206
\rulename{minus_divide_left}
paulson@10764
   207
paulson@14295
   208
@{thm[display] minus_divide_right[no_vars]}
paulson@14295
   209
\rulename{minus_divide_right}
paulson@10764
   210
paulson@10764
   211
This last NOT a simprule
paulson@10764
   212
paulson@14295
   213
@{thm[display] add_divide_distrib[no_vars]}
paulson@14295
   214
\rulename{add_divide_distrib}
paulson@10764
   215
*}
paulson@10603
   216
wenzelm@11711
   217
lemma "3/4 < (7/8 :: real)"
paulson@11174
   218
by simp 
paulson@11174
   219
wenzelm@11711
   220
lemma "P ((3/4) * (8/15 :: real))"
paulson@11174
   221
txt{*
paulson@11174
   222
@{subgoals[display,indent=0,margin=65]}
paulson@11174
   223
*};
paulson@11174
   224
apply simp 
paulson@11174
   225
txt{*
paulson@11174
   226
@{subgoals[display,indent=0,margin=65]}
paulson@11174
   227
*};
paulson@11174
   228
oops
paulson@11174
   229
wenzelm@11711
   230
lemma "(3/4) * (8/15) < (x :: real)"
paulson@11174
   231
txt{*
paulson@11174
   232
@{subgoals[display,indent=0,margin=65]}
paulson@11174
   233
*};
paulson@11174
   234
apply simp 
paulson@11174
   235
txt{*
paulson@11174
   236
@{subgoals[display,indent=0,margin=65]}
paulson@11174
   237
*};
paulson@11174
   238
oops
paulson@11174
   239
paulson@14400
   240
text{*
paulson@14400
   241
Ring and Field
paulson@14400
   242
paulson@14400
   243
Requires a field, or else an ordered ring
paulson@14400
   244
paulson@14400
   245
@{thm[display] mult_eq_0_iff[no_vars]}
paulson@14400
   246
\rulename{mult_eq_0_iff}
paulson@14400
   247
paulson@14400
   248
@{thm[display] mult_cancel_right[no_vars]}
paulson@14400
   249
\rulename{mult_cancel_right}
paulson@23504
   250
paulson@23504
   251
@{thm[display] mult_cancel_left[no_vars]}
paulson@23504
   252
\rulename{mult_cancel_left}
paulson@14400
   253
*}
paulson@14400
   254
paulson@14400
   255
text{*
paulson@14400
   256
effect of show sorts on the above
paulson@23504
   257
wenzelm@32834
   258
@{thm[display,show_sorts] mult_cancel_left[no_vars]}
paulson@23504
   259
\rulename{mult_cancel_left}
paulson@14400
   260
*}
paulson@14400
   261
paulson@14400
   262
text{*
paulson@14400
   263
absolute value
paulson@14400
   264
paulson@14400
   265
@{thm[display] abs_mult[no_vars]}
paulson@14400
   266
\rulename{abs_mult}
paulson@14400
   267
paulson@14400
   268
@{thm[display] abs_le_iff[no_vars]}
paulson@14400
   269
\rulename{abs_le_iff}
paulson@14400
   270
paulson@14400
   271
@{thm[display] abs_triangle_ineq[no_vars]}
paulson@14400
   272
\rulename{abs_triangle_ineq}
paulson@14400
   273
paulson@14400
   274
@{thm[display] power_add[no_vars]}
paulson@14400
   275
\rulename{power_add}
paulson@14400
   276
paulson@14400
   277
@{thm[display] power_mult[no_vars]}
paulson@14400
   278
\rulename{power_mult}
paulson@14400
   279
paulson@14400
   280
@{thm[display] power_abs[no_vars]}
paulson@14400
   281
\rulename{power_abs}
paulson@14400
   282
paulson@14400
   283
paulson@14400
   284
*}
paulson@11174
   285
paulson@11174
   286
paulson@10603
   287
end