src/Doc/Tutorial/Types/Numbers.thy
author wenzelm
Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421 1ffd7eaa778b
parent 48985 5386df44a037
child 57512 cc97b347b301
permissions -rw-r--r--
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27376
ffe9b958bada adjusted import
haftmann
parents: 23504
diff changeset
     1
theory Numbers
ffe9b958bada adjusted import
haftmann
parents: 23504
diff changeset
     2
imports Complex_Main
ffe9b958bada adjusted import
haftmann
parents: 23504
diff changeset
     3
begin
10603
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
     4
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
     5
text{*
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
     6
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
     7
numeric literals; default simprules; can re-orient
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
     8
*}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
     9
11711
ecdfd237ffee fixed numerals;
wenzelm
parents: 11480
diff changeset
    10
lemma "2 * m = m + m"
10880
729a36e469ec updated for new version of numerics.tex
paulson
parents: 10777
diff changeset
    11
txt{*
729a36e469ec updated for new version of numerics.tex
paulson
parents: 10777
diff changeset
    12
@{subgoals[display,indent=0,margin=65]}
729a36e469ec updated for new version of numerics.tex
paulson
parents: 10777
diff changeset
    13
*};
10603
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    14
oops
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    15
44048
64f574163ca2 removed old recdef and types usage
nipkow
parents: 38767
diff changeset
    16
fun h :: "nat \<Rightarrow> nat" where
11711
ecdfd237ffee fixed numerals;
wenzelm
parents: 11480
diff changeset
    17
"h i = (if i = 3 then 2 else i)"
10880
729a36e469ec updated for new version of numerics.tex
paulson
parents: 10777
diff changeset
    18
10603
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    19
text{*
11711
ecdfd237ffee fixed numerals;
wenzelm
parents: 11480
diff changeset
    20
@{term"h 3 = 2"}
10880
729a36e469ec updated for new version of numerics.tex
paulson
parents: 10777
diff changeset
    21
@{term"h i  = i"}
729a36e469ec updated for new version of numerics.tex
paulson
parents: 10777
diff changeset
    22
*}
10603
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    23
10880
729a36e469ec updated for new version of numerics.tex
paulson
parents: 10777
diff changeset
    24
text{*
10603
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    25
@{thm[display] numeral_1_eq_1[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    26
\rulename{numeral_1_eq_1}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    27
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    28
@{thm[display] add_2_eq_Suc[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    29
\rulename{add_2_eq_Suc}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    30
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    31
@{thm[display] add_2_eq_Suc'[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    32
\rulename{add_2_eq_Suc'}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    33
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    34
@{thm[display] add_assoc[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    35
\rulename{add_assoc}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    36
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    37
@{thm[display] add_commute[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    38
\rulename{add_commute}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    39
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    40
@{thm[display] add_left_commute[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    41
\rulename{add_left_commute}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    42
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    43
these form add_ac; similarly there is mult_ac
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    44
*}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    45
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    46
lemma "Suc(i + j*l*k + m*n) = f (n*m + i + k*j*l)"
10880
729a36e469ec updated for new version of numerics.tex
paulson
parents: 10777
diff changeset
    47
txt{*
729a36e469ec updated for new version of numerics.tex
paulson
parents: 10777
diff changeset
    48
@{subgoals[display,indent=0,margin=65]}
729a36e469ec updated for new version of numerics.tex
paulson
parents: 10777
diff changeset
    49
*};
10603
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    50
apply (simp add: add_ac mult_ac)
10880
729a36e469ec updated for new version of numerics.tex
paulson
parents: 10777
diff changeset
    51
txt{*
729a36e469ec updated for new version of numerics.tex
paulson
parents: 10777
diff changeset
    52
@{subgoals[display,indent=0,margin=65]}
729a36e469ec updated for new version of numerics.tex
paulson
parents: 10777
diff changeset
    53
*};
10603
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    54
oops
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    55
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    56
text{*
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    57
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    58
@{thm[display] div_le_mono[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    59
\rulename{div_le_mono}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    60
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    61
@{thm[display] diff_mult_distrib[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    62
\rulename{diff_mult_distrib}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    63
47183
f760e15343bc removed references to obsolete theorems
huffman
parents: 44048
diff changeset
    64
@{thm[display] mult_mod_left[no_vars]}
f760e15343bc removed references to obsolete theorems
huffman
parents: 44048
diff changeset
    65
\rulename{mult_mod_left}
10603
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    66
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    67
@{thm[display] nat_diff_split[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    68
\rulename{nat_diff_split}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    69
*}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    70
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    71
12156
d2758965362e new-style numerals without leading #, along with generic 0 and 1
paulson
parents: 11711
diff changeset
    72
lemma "(n - 1) * (n + 1) = n * n - (1::nat)"
12843
50bd380e6675 iff del: less_Suc0 -- luckily this does NOT affect the printed text;
wenzelm
parents: 12156
diff changeset
    73
apply (clarsimp split: nat_diff_split iff del: less_Suc0)
12156
d2758965362e new-style numerals without leading #, along with generic 0 and 1
paulson
parents: 11711
diff changeset
    74
 --{* @{subgoals[display,indent=0,margin=65]} *}
d2758965362e new-style numerals without leading #, along with generic 0 and 1
paulson
parents: 11711
diff changeset
    75
apply (subgoal_tac "n=0", force, arith)
d2758965362e new-style numerals without leading #, along with generic 0 and 1
paulson
parents: 11711
diff changeset
    76
done
d2758965362e new-style numerals without leading #, along with generic 0 and 1
paulson
parents: 11711
diff changeset
    77
d2758965362e new-style numerals without leading #, along with generic 0 and 1
paulson
parents: 11711
diff changeset
    78
11711
ecdfd237ffee fixed numerals;
wenzelm
parents: 11480
diff changeset
    79
lemma "(n - 2) * (n + 2) = n * n - (4::nat)"
12156
d2758965362e new-style numerals without leading #, along with generic 0 and 1
paulson
parents: 11711
diff changeset
    80
apply (simp split: nat_diff_split, clarify)
11480
0fba0357c04c Getting it working again with 1' instead of 1
paulson
parents: 11174
diff changeset
    81
 --{* @{subgoals[display,indent=0,margin=65]} *}
0fba0357c04c Getting it working again with 1' instead of 1
paulson
parents: 11174
diff changeset
    82
apply (subgoal_tac "n=0 | n=1", force, arith)
10603
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    83
done
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    84
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    85
text{*
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    86
@{thm[display] mod_if[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    87
\rulename{mod_if}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    88
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    89
@{thm[display] mod_div_equality[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    90
\rulename{mod_div_equality}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    91
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    92
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    93
@{thm[display] div_mult1_eq[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    94
\rulename{div_mult1_eq}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    95
30224
79136ce06bdb removed and renamed redundant lemmas
nipkow
parents: 30200
diff changeset
    96
@{thm[display] mod_mult_right_eq[no_vars]}
79136ce06bdb removed and renamed redundant lemmas
nipkow
parents: 30200
diff changeset
    97
\rulename{mod_mult_right_eq}
10603
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    98
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
    99
@{thm[display] div_mult2_eq[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   100
\rulename{div_mult2_eq}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   101
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   102
@{thm[display] mod_mult2_eq[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   103
\rulename{mod_mult2_eq}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   104
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   105
@{thm[display] div_mult_mult1[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   106
\rulename{div_mult_mult1}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   107
27658
674496eb5965 (adjusted)
haftmann
parents: 27376
diff changeset
   108
@{thm[display] div_by_0 [no_vars]}
674496eb5965 (adjusted)
haftmann
parents: 27376
diff changeset
   109
\rulename{div_by_0}
10603
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   110
27658
674496eb5965 (adjusted)
haftmann
parents: 27376
diff changeset
   111
@{thm[display] mod_by_0 [no_vars]}
674496eb5965 (adjusted)
haftmann
parents: 27376
diff changeset
   112
\rulename{mod_by_0}
10603
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   113
33750
0a0d6d79d984 anti_sym -> antisym
nipkow
parents: 32834
diff changeset
   114
@{thm[display] dvd_antisym[no_vars]}
0a0d6d79d984 anti_sym -> antisym
nipkow
parents: 32834
diff changeset
   115
\rulename{dvd_antisym}
10603
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   116
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   117
@{thm[display] dvd_add[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   118
\rulename{dvd_add}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   119
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   120
For the integers, I'd list a few theorems that somehow involve negative 
13757
33b84d172c97 new int induction rules
paulson
parents: 12843
diff changeset
   121
numbers.*}
10603
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   122
13757
33b84d172c97 new int induction rules
paulson
parents: 12843
diff changeset
   123
33b84d172c97 new int induction rules
paulson
parents: 12843
diff changeset
   124
text{*
10603
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   125
Division, remainder of negatives
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   126
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   127
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   128
@{thm[display] pos_mod_sign[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   129
\rulename{pos_mod_sign}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   130
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   131
@{thm[display] pos_mod_bound[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   132
\rulename{pos_mod_bound}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   133
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   134
@{thm[display] neg_mod_sign[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   135
\rulename{neg_mod_sign}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   136
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   137
@{thm[display] neg_mod_bound[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   138
\rulename{neg_mod_bound}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   139
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   140
@{thm[display] zdiv_zadd1_eq[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   141
\rulename{zdiv_zadd1_eq}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   142
30224
79136ce06bdb removed and renamed redundant lemmas
nipkow
parents: 30200
diff changeset
   143
@{thm[display] mod_add_eq[no_vars]}
79136ce06bdb removed and renamed redundant lemmas
nipkow
parents: 30200
diff changeset
   144
\rulename{mod_add_eq}
10603
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   145
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   146
@{thm[display] zdiv_zmult1_eq[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   147
\rulename{zdiv_zmult1_eq}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   148
47183
f760e15343bc removed references to obsolete theorems
huffman
parents: 44048
diff changeset
   149
@{thm[display] mod_mult_right_eq[no_vars]}
f760e15343bc removed references to obsolete theorems
huffman
parents: 44048
diff changeset
   150
\rulename{mod_mult_right_eq}
10603
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   151
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   152
@{thm[display] zdiv_zmult2_eq[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   153
\rulename{zdiv_zmult2_eq}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   154
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   155
@{thm[display] zmod_zmult2_eq[no_vars]}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   156
\rulename{zmod_zmult2_eq}
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   157
*}  
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   158
11174
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   159
lemma "abs (x+y) \<le> abs x + abs (y :: int)"
10880
729a36e469ec updated for new version of numerics.tex
paulson
parents: 10777
diff changeset
   160
by arith
729a36e469ec updated for new version of numerics.tex
paulson
parents: 10777
diff changeset
   161
11711
ecdfd237ffee fixed numerals;
wenzelm
parents: 11480
diff changeset
   162
lemma "abs (2*x) = 2 * abs (x :: int)"
16585
02cf78f0afce replacing zabs_def by abs_if
paulson
parents: 16417
diff changeset
   163
by (simp add: abs_if) 
11174
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   164
13757
33b84d172c97 new int induction rules
paulson
parents: 12843
diff changeset
   165
33b84d172c97 new int induction rules
paulson
parents: 12843
diff changeset
   166
text {*Induction rules for the Integers
33b84d172c97 new int induction rules
paulson
parents: 12843
diff changeset
   167
33b84d172c97 new int induction rules
paulson
parents: 12843
diff changeset
   168
@{thm[display] int_ge_induct[no_vars]}
33b84d172c97 new int induction rules
paulson
parents: 12843
diff changeset
   169
\rulename{int_ge_induct}
33b84d172c97 new int induction rules
paulson
parents: 12843
diff changeset
   170
33b84d172c97 new int induction rules
paulson
parents: 12843
diff changeset
   171
@{thm[display] int_gr_induct[no_vars]}
33b84d172c97 new int induction rules
paulson
parents: 12843
diff changeset
   172
\rulename{int_gr_induct}
33b84d172c97 new int induction rules
paulson
parents: 12843
diff changeset
   173
33b84d172c97 new int induction rules
paulson
parents: 12843
diff changeset
   174
@{thm[display] int_le_induct[no_vars]}
33b84d172c97 new int induction rules
paulson
parents: 12843
diff changeset
   175
\rulename{int_le_induct}
33b84d172c97 new int induction rules
paulson
parents: 12843
diff changeset
   176
33b84d172c97 new int induction rules
paulson
parents: 12843
diff changeset
   177
@{thm[display] int_less_induct[no_vars]}
33b84d172c97 new int induction rules
paulson
parents: 12843
diff changeset
   178
\rulename{int_less_induct}
33b84d172c97 new int induction rules
paulson
parents: 12843
diff changeset
   179
*}  
33b84d172c97 new int induction rules
paulson
parents: 12843
diff changeset
   180
14400
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   181
text {*FIELDS
10764
329d5f4aa43c some HOL-Real material
paulson
parents: 10603
diff changeset
   182
14295
7f115e5c5de4 more general lemmas for Ring_and_Field
paulson
parents: 14288
diff changeset
   183
@{thm[display] dense[no_vars]}
7f115e5c5de4 more general lemmas for Ring_and_Field
paulson
parents: 14288
diff changeset
   184
\rulename{dense}
10603
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   185
14288
d149e3cbdb39 Moving some theorems from Real/RealArith0.ML
paulson
parents: 13757
diff changeset
   186
@{thm[display] times_divide_eq_right[no_vars]}
d149e3cbdb39 Moving some theorems from Real/RealArith0.ML
paulson
parents: 13757
diff changeset
   187
\rulename{times_divide_eq_right}
10764
329d5f4aa43c some HOL-Real material
paulson
parents: 10603
diff changeset
   188
14288
d149e3cbdb39 Moving some theorems from Real/RealArith0.ML
paulson
parents: 13757
diff changeset
   189
@{thm[display] times_divide_eq_left[no_vars]}
d149e3cbdb39 Moving some theorems from Real/RealArith0.ML
paulson
parents: 13757
diff changeset
   190
\rulename{times_divide_eq_left}
10764
329d5f4aa43c some HOL-Real material
paulson
parents: 10603
diff changeset
   191
14288
d149e3cbdb39 Moving some theorems from Real/RealArith0.ML
paulson
parents: 13757
diff changeset
   192
@{thm[display] divide_divide_eq_right[no_vars]}
d149e3cbdb39 Moving some theorems from Real/RealArith0.ML
paulson
parents: 13757
diff changeset
   193
\rulename{divide_divide_eq_right}
10764
329d5f4aa43c some HOL-Real material
paulson
parents: 10603
diff changeset
   194
14288
d149e3cbdb39 Moving some theorems from Real/RealArith0.ML
paulson
parents: 13757
diff changeset
   195
@{thm[display] divide_divide_eq_left[no_vars]}
d149e3cbdb39 Moving some theorems from Real/RealArith0.ML
paulson
parents: 13757
diff changeset
   196
\rulename{divide_divide_eq_left}
10764
329d5f4aa43c some HOL-Real material
paulson
parents: 10603
diff changeset
   197
14295
7f115e5c5de4 more general lemmas for Ring_and_Field
paulson
parents: 14288
diff changeset
   198
@{thm[display] minus_divide_left[no_vars]}
7f115e5c5de4 more general lemmas for Ring_and_Field
paulson
parents: 14288
diff changeset
   199
\rulename{minus_divide_left}
10764
329d5f4aa43c some HOL-Real material
paulson
parents: 10603
diff changeset
   200
14295
7f115e5c5de4 more general lemmas for Ring_and_Field
paulson
parents: 14288
diff changeset
   201
@{thm[display] minus_divide_right[no_vars]}
7f115e5c5de4 more general lemmas for Ring_and_Field
paulson
parents: 14288
diff changeset
   202
\rulename{minus_divide_right}
10764
329d5f4aa43c some HOL-Real material
paulson
parents: 10603
diff changeset
   203
329d5f4aa43c some HOL-Real material
paulson
parents: 10603
diff changeset
   204
This last NOT a simprule
329d5f4aa43c some HOL-Real material
paulson
parents: 10603
diff changeset
   205
14295
7f115e5c5de4 more general lemmas for Ring_and_Field
paulson
parents: 14288
diff changeset
   206
@{thm[display] add_divide_distrib[no_vars]}
7f115e5c5de4 more general lemmas for Ring_and_Field
paulson
parents: 14288
diff changeset
   207
\rulename{add_divide_distrib}
10764
329d5f4aa43c some HOL-Real material
paulson
parents: 10603
diff changeset
   208
*}
10603
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   209
11711
ecdfd237ffee fixed numerals;
wenzelm
parents: 11480
diff changeset
   210
lemma "3/4 < (7/8 :: real)"
11174
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   211
by simp 
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   212
11711
ecdfd237ffee fixed numerals;
wenzelm
parents: 11480
diff changeset
   213
lemma "P ((3/4) * (8/15 :: real))"
11174
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   214
txt{*
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   215
@{subgoals[display,indent=0,margin=65]}
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   216
*};
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   217
apply simp 
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   218
txt{*
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   219
@{subgoals[display,indent=0,margin=65]}
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   220
*};
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   221
oops
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   222
11711
ecdfd237ffee fixed numerals;
wenzelm
parents: 11480
diff changeset
   223
lemma "(3/4) * (8/15) < (x :: real)"
11174
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   224
txt{*
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   225
@{subgoals[display,indent=0,margin=65]}
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   226
*};
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   227
apply simp 
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   228
txt{*
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   229
@{subgoals[display,indent=0,margin=65]}
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   230
*};
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   231
oops
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   232
14400
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   233
text{*
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   234
Ring and Field
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   235
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   236
Requires a field, or else an ordered ring
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   237
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   238
@{thm[display] mult_eq_0_iff[no_vars]}
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   239
\rulename{mult_eq_0_iff}
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   240
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   241
@{thm[display] mult_cancel_right[no_vars]}
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   242
\rulename{mult_cancel_right}
23504
2b2323124e8e changes for type class ring_no_zero_divisors
paulson
parents: 23501
diff changeset
   243
2b2323124e8e changes for type class ring_no_zero_divisors
paulson
parents: 23501
diff changeset
   244
@{thm[display] mult_cancel_left[no_vars]}
2b2323124e8e changes for type class ring_no_zero_divisors
paulson
parents: 23501
diff changeset
   245
\rulename{mult_cancel_left}
14400
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   246
*}
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   247
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   248
text{*
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   249
effect of show sorts on the above
23504
2b2323124e8e changes for type class ring_no_zero_divisors
paulson
parents: 23501
diff changeset
   250
32834
a4e0b8d88f28 avoid unsynchronized refs within theory sources;
wenzelm
parents: 30242
diff changeset
   251
@{thm[display,show_sorts] mult_cancel_left[no_vars]}
23504
2b2323124e8e changes for type class ring_no_zero_divisors
paulson
parents: 23501
diff changeset
   252
\rulename{mult_cancel_left}
14400
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   253
*}
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   254
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   255
text{*
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   256
absolute value
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   257
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   258
@{thm[display] abs_mult[no_vars]}
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   259
\rulename{abs_mult}
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   260
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   261
@{thm[display] abs_le_iff[no_vars]}
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   262
\rulename{abs_le_iff}
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   263
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   264
@{thm[display] abs_triangle_ineq[no_vars]}
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   265
\rulename{abs_triangle_ineq}
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   266
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   267
@{thm[display] power_add[no_vars]}
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   268
\rulename{power_add}
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   269
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   270
@{thm[display] power_mult[no_vars]}
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   271
\rulename{power_mult}
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   272
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   273
@{thm[display] power_abs[no_vars]}
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   274
\rulename{power_abs}
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   275
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   276
6069098854b9 new numerics section using type classes
paulson
parents: 14353
diff changeset
   277
*}
11174
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   278
96a533d300a6 revisions in response to comments by Tobias
paulson
parents: 10880
diff changeset
   279
10603
539735ddaea9 theory file for Numbers section
paulson
parents:
diff changeset
   280
end