src/HOL/ex/BinEx.thy
author wenzelm
Thu, 30 May 2013 20:38:50 +0200
changeset 52252 81fcc11d8c65
parent 45615 c05e8209a3aa
child 58410 6d46ad54a2ab
permissions -rw-r--r--
minor tuning -- more linebreaks;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5545
9117a0e2bf31 added correctness proofs for arithmetic
paulson
parents: 5199
diff changeset
     1
(*  Title:      HOL/ex/BinEx.thy
9117a0e2bf31 added correctness proofs for arithmetic
paulson
parents: 5199
diff changeset
     2
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
9117a0e2bf31 added correctness proofs for arithmetic
paulson
parents: 5199
diff changeset
     3
    Copyright   1998  University of Cambridge
9117a0e2bf31 added correctness proofs for arithmetic
paulson
parents: 5199
diff changeset
     4
*)
9117a0e2bf31 added correctness proofs for arithmetic
paulson
parents: 5199
diff changeset
     5
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
     6
header {* Binary arithmetic examples *}
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
     7
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
     8
theory BinEx
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
     9
imports Complex_Main
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
    10
begin
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
    11
14113
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    12
subsection {* Regression Testing for Cancellation Simprocs *}
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    13
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    14
lemma "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    15
apply simp  oops
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    16
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    17
lemma "2*u = (u::int)"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    18
apply simp  oops
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    19
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    20
lemma "(i + j + 12 + (k::int)) - 15 = y"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    21
apply simp  oops
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    22
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    23
lemma "(i + j + 12 + (k::int)) - 5 = y"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    24
apply simp  oops
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    25
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    26
lemma "y - b < (b::int)"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    27
apply simp  oops
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    28
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    29
lemma "y - (3*b + c) < (b::int) - 2*c"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    30
apply simp  oops
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    31
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    32
lemma "(2*x - (u*v) + y) - v*3*u = (w::int)"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    33
apply simp  oops
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    34
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    35
lemma "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    36
apply simp  oops
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    37
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    38
lemma "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    39
apply simp  oops
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    40
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    41
lemma "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    42
apply simp  oops
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    43
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    44
lemma "(i + j + 12 + (k::int)) = u + 15 + y"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    45
apply simp  oops
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    46
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    47
lemma "(i + j*2 + 12 + (k::int)) = j + 5 + y"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    48
apply simp  oops
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    49
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    50
lemma "2*y + 3*z + 6*w + 2*y + 3*z + 2*u = 2*y' + 3*z' + 6*w' + 2*y' + 3*z' + u + (vv::int)"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    51
apply simp  oops
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    52
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    53
lemma "a + -(b+c) + b = (d::int)"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    54
apply simp  oops
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    55
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    56
lemma "a + -(b+c) - b = (d::int)"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    57
apply simp  oops
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    58
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    59
(*negative numerals*)
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    60
lemma "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    61
apply simp  oops
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    62
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    63
lemma "(i + j + -3 + (k::int)) < u + 5 + y"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    64
apply simp  oops
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    65
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    66
lemma "(i + j + 3 + (k::int)) < u + -6 + y"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    67
apply simp  oops
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    68
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    69
lemma "(i + j + -12 + (k::int)) - 15 = y"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    70
apply simp  oops
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    71
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    72
lemma "(i + j + 12 + (k::int)) - -15 = y"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    73
apply simp  oops
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    74
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    75
lemma "(i + j + -12 + (k::int)) - -15 = y"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    76
apply simp  oops
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    77
14124
883c38e2d4c0 Added some regression testing for simprocs
paulson
parents: 14113
diff changeset
    78
lemma "- (2*i) + 3  + (2*i + 4) = (0::int)"
883c38e2d4c0 Added some regression testing for simprocs
paulson
parents: 14113
diff changeset
    79
apply simp  oops
883c38e2d4c0 Added some regression testing for simprocs
paulson
parents: 14113
diff changeset
    80
883c38e2d4c0 Added some regression testing for simprocs
paulson
parents: 14113
diff changeset
    81
14113
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    82
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    83
subsection {* Arithmetic Method Tests *}
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    84
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    85
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    86
lemma "!!a::int. [| a <= b; c <= d; x+y<z |] ==> a+c <= b+d"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    87
by arith
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    88
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    89
lemma "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    90
by arith
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    91
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    92
lemma "!!a::int. [| a < b; c < d |] ==> a+c+ 1 < b+d"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    93
by arith
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    94
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    95
lemma "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    96
by arith
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    97
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    98
lemma "!!a::int. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
    99
by arith
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   100
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   101
lemma "!!a::int. [| a+b < i+j; a<b; i<j |] ==> a+a - - -1 < j+j - 3"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   102
by arith
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   103
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   104
lemma "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   105
by arith
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   106
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   107
lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   108
      ==> a <= l"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   109
by arith
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   110
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   111
lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   112
      ==> a+a+a+a <= l+l+l+l"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   113
by arith
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   114
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   115
lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   116
      ==> a+a+a+a+a <= l+l+l+l+i"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   117
by arith
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   118
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   119
lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   120
      ==> a+a+a+a+a+a <= l+l+l+l+i+l"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   121
by arith
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   122
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   123
lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   124
      ==> 6*a <= 5*l+i"
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   125
by arith
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   126
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   127
7b3513ba0f86 Fixing a simproc bug
paulson
parents: 13491
diff changeset
   128
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   129
subsection {* The Integers *}
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   130
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   131
text {* Addition *}
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   132
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   133
lemma "(13::int) + 19 = 32"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   134
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   135
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   136
lemma "(1234::int) + 5678 = 6912"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   137
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   138
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   139
lemma "(1359::int) + -2468 = -1109"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   140
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   141
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   142
lemma "(93746::int) + -46375 = 47371"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   143
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   144
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   145
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   146
text {* \medskip Negation *}
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   147
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   148
lemma "- (65745::int) = -65745"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   149
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   150
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   151
lemma "- (-54321::int) = 54321"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   152
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   153
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   154
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   155
text {* \medskip Multiplication *}
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   156
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   157
lemma "(13::int) * 19 = 247"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   158
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   159
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   160
lemma "(-84::int) * 51 = -4284"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   161
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   162
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   163
lemma "(255::int) * 255 = 65025"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   164
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   165
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   166
lemma "(1359::int) * -2468 = -3354012"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   167
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   168
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   169
lemma "(89::int) * 10 \<noteq> 889"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   170
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   171
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   172
lemma "(13::int) < 18 - 4"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   173
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   174
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   175
lemma "(-345::int) < -242 + -100"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   176
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   177
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   178
lemma "(13557456::int) < 18678654"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   179
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   180
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   181
lemma "(999999::int) \<le> (1000001 + 1) - 2"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   182
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   183
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   184
lemma "(1234567::int) \<le> 1234567"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   185
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   186
15965
f422f8283491 Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents: 15013
diff changeset
   187
text{*No integer overflow!*}
f422f8283491 Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents: 15013
diff changeset
   188
lemma "1234567 * (1234567::int) < 1234567*1234567*1234567"
f422f8283491 Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents: 15013
diff changeset
   189
  by simp
f422f8283491 Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents: 15013
diff changeset
   190
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   191
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   192
text {* \medskip Quotient and Remainder *}
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   193
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   194
lemma "(10::int) div 3 = 3"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   195
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   196
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   197
lemma "(10::int) mod 3 = 1"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   198
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   199
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   200
text {* A negative divisor *}
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   201
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   202
lemma "(10::int) div -3 = -4"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   203
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   204
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   205
lemma "(10::int) mod -3 = -2"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   206
  by simp
5545
9117a0e2bf31 added correctness proofs for arithmetic
paulson
parents: 5199
diff changeset
   207
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   208
text {*
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   209
  A negative dividend\footnote{The definition agrees with mathematical
15965
f422f8283491 Use of IntInf.int instead of int in most numeric simprocs; avoids
paulson
parents: 15013
diff changeset
   210
  convention and with ML, but not with the hardware of most computers}
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   211
*}
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   212
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   213
lemma "(-10::int) div 3 = -4"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   214
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   215
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   216
lemma "(-10::int) mod 3 = 2"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   217
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   218
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   219
text {* A negative dividend \emph{and} divisor *}
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   220
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   221
lemma "(-10::int) div -3 = 3"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   222
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   223
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   224
lemma "(-10::int) mod -3 = -1"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   225
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   226
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   227
text {* A few bigger examples *}
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   228
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   229
lemma "(8452::int) mod 3 = 1"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   230
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   231
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   232
lemma "(59485::int) div 434 = 137"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   233
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   234
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   235
lemma "(1000006::int) mod 10 = 6"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   236
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   237
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   238
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   239
text {* \medskip Division by shifting *}
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   240
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   241
lemma "10000000 div 2 = (5000000::int)"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   242
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   243
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   244
lemma "10000001 mod 2 = (1::int)"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   245
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   246
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   247
lemma "10000055 div 32 = (312501::int)"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   248
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   249
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   250
lemma "10000055 mod 32 = (23::int)"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   251
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   252
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   253
lemma "100094 div 144 = (695::int)"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   254
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   255
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   256
lemma "100094 mod 144 = (14::int)"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   257
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   258
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   259
12613
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   260
text {* \medskip Powers *}
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   261
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   262
lemma "2 ^ 10 = (1024::int)"
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   263
  by simp
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   264
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   265
lemma "-3 ^ 7 = (-2187::int)"
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   266
  by simp
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   267
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   268
lemma "13 ^ 7 = (62748517::int)"
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   269
  by simp
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   270
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   271
lemma "3 ^ 15 = (14348907::int)"
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   272
  by simp
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   273
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   274
lemma "-5 ^ 11 = (-48828125::int)"
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   275
  by simp
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   276
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   277
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   278
subsection {* The Natural Numbers *}
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   279
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   280
text {* Successor *}
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   281
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   282
lemma "Suc 99999 = 100000"
45615
c05e8209a3aa remove outdated comment
huffman
parents: 31066
diff changeset
   283
  by simp
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   284
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   285
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   286
text {* \medskip Addition *}
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   287
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   288
lemma "(13::nat) + 19 = 32"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   289
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   290
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   291
lemma "(1234::nat) + 5678 = 6912"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   292
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   293
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   294
lemma "(973646::nat) + 6475 = 980121"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   295
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   296
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   297
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   298
text {* \medskip Subtraction *}
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   299
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   300
lemma "(32::nat) - 14 = 18"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   301
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   302
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   303
lemma "(14::nat) - 15 = 0"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   304
  by simp
5545
9117a0e2bf31 added correctness proofs for arithmetic
paulson
parents: 5199
diff changeset
   305
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   306
lemma "(14::nat) - 1576644 = 0"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   307
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   308
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   309
lemma "(48273776::nat) - 3873737 = 44400039"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   310
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   311
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   312
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   313
text {* \medskip Multiplication *}
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   314
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   315
lemma "(12::nat) * 11 = 132"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   316
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   317
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   318
lemma "(647::nat) * 3643 = 2357021"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   319
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   320
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   321
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   322
text {* \medskip Quotient and Remainder *}
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   323
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   324
lemma "(10::nat) div 3 = 3"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   325
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   326
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   327
lemma "(10::nat) mod 3 = 1"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   328
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   329
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   330
lemma "(10000::nat) div 9 = 1111"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   331
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   332
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   333
lemma "(10000::nat) mod 9 = 1"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   334
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   335
11704
3c50a2cd6f00 * sane numerals (stage 2): plain "num" syntax (removed "#");
wenzelm
parents: 11701
diff changeset
   336
lemma "(10000::nat) div 16 = 625"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   337
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   338
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   339
lemma "(10000::nat) mod 16 = 0"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   340
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   341
5545
9117a0e2bf31 added correctness proofs for arithmetic
paulson
parents: 5199
diff changeset
   342
12613
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   343
text {* \medskip Powers *}
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   344
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   345
lemma "2 ^ 12 = (4096::nat)"
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   346
  by simp
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   347
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   348
lemma "3 ^ 10 = (59049::nat)"
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   349
  by simp
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   350
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   351
lemma "12 ^ 7 = (35831808::nat)"
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   352
  by simp
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   353
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   354
lemma "3 ^ 14 = (4782969::nat)"
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   355
  by simp
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   356
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   357
lemma "5 ^ 11 = (48828125::nat)"
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   358
  by simp
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   359
279facb4253a Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
paulson
parents: 11868
diff changeset
   360
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   361
text {* \medskip Testing the cancellation of complementary terms *}
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   362
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   363
lemma "y + (x + -x) = (0::int) + y"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   364
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   365
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   366
lemma "y + (-x + (- y + x)) = (0::int)"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   367
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   368
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   369
lemma "-x + (y + (- y + x)) = (0::int)"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   370
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   371
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   372
lemma "x + (x + (- x + (- x + (- y + - z)))) = (0::int) - y - z"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   373
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   374
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   375
lemma "x + x - x - x - y - z = (0::int) - y - z"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   376
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   377
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   378
lemma "x + y + z - (x + z) = y - (0::int)"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   379
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   380
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   381
lemma "x + (y + (y + (y + (-x + -x)))) = (0::int) + y - x + y + y"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   382
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   383
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   384
lemma "x + (y + (y + (y + (-y + -x)))) = y + (0::int) + y"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   385
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   386
11868
56db9f3a6b3e Numerals now work for the integers: the binary numerals for 0 and 1 rewrite
paulson
parents: 11704
diff changeset
   387
lemma "x + y - x + z - x - y - z + x < (1::int)"
11024
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   388
  by simp
23bf8d787b04 converted to new-style theories;
wenzelm
parents: 9297
diff changeset
   389
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   390
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   391
subsection{*Real Arithmetic*}
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   392
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   393
subsubsection {*Addition *}
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   394
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   395
lemma "(1359::real) + -2468 = -1109"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   396
by simp
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   397
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   398
lemma "(93746::real) + -46375 = 47371"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   399
by simp
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   400
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   401
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   402
subsubsection {*Negation *}
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   403
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   404
lemma "- (65745::real) = -65745"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   405
by simp
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   406
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   407
lemma "- (-54321::real) = 54321"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   408
by simp
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   409
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   410
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   411
subsubsection {*Multiplication *}
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   412
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   413
lemma "(-84::real) * 51 = -4284"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   414
by simp
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   415
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   416
lemma "(255::real) * 255 = 65025"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   417
by simp
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   418
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   419
lemma "(1359::real) * -2468 = -3354012"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   420
by simp
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   421
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   422
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   423
subsubsection {*Inequalities *}
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   424
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   425
lemma "(89::real) * 10 \<noteq> 889"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   426
by simp
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   427
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   428
lemma "(13::real) < 18 - 4"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   429
by simp
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   430
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   431
lemma "(-345::real) < -242 + -100"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   432
by simp
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   433
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   434
lemma "(13557456::real) < 18678654"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   435
by simp
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   436
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   437
lemma "(999999::real) \<le> (1000001 + 1) - 2"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   438
by simp
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   439
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   440
lemma "(1234567::real) \<le> 1234567"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   441
by simp
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   442
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   443
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   444
subsubsection {*Powers *}
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   445
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   446
lemma "2 ^ 15 = (32768::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   447
by simp
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   448
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   449
lemma "-3 ^ 7 = (-2187::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   450
by simp
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   451
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   452
lemma "13 ^ 7 = (62748517::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   453
by simp
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   454
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   455
lemma "3 ^ 15 = (14348907::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   456
by simp
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   457
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   458
lemma "-5 ^ 11 = (-48828125::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   459
by simp
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   460
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   461
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   462
subsubsection {*Tests *}
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   463
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   464
lemma "(x + y = x) = (y = (0::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   465
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   466
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   467
lemma "(x + y = y) = (x = (0::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   468
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   469
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   470
lemma "(x + y = (0::real)) = (x = -y)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   471
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   472
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   473
lemma "(x + y = (0::real)) = (y = -x)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   474
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   475
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   476
lemma "((x + y) < (x + z)) = (y < (z::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   477
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   478
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   479
lemma "((x + z) < (y + z)) = (x < (y::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   480
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   481
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   482
lemma "(\<not> x < y) = (y \<le> (x::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   483
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   484
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   485
lemma "\<not> (x < y \<and> y < (x::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   486
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   487
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   488
lemma "(x::real) < y ==> \<not> y < x"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   489
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   490
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   491
lemma "((x::real) \<noteq> y) = (x < y \<or> y < x)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   492
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   493
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   494
lemma "(\<not> x \<le> y) = (y < (x::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   495
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   496
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   497
lemma "x \<le> y \<or> y \<le> (x::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   498
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   499
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   500
lemma "x \<le> y \<or> y < (x::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   501
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   502
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   503
lemma "x < y \<or> y \<le> (x::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   504
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   505
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   506
lemma "x \<le> (x::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   507
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   508
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   509
lemma "((x::real) \<le> y) = (x < y \<or> x = y)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   510
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   511
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   512
lemma "((x::real) \<le> y \<and> y \<le> x) = (x = y)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   513
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   514
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   515
lemma "\<not>(x < y \<and> y \<le> (x::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   516
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   517
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   518
lemma "\<not>(x \<le> y \<and> y < (x::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   519
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   520
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   521
lemma "(-x < (0::real)) = (0 < x)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   522
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   523
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   524
lemma "((0::real) < -x) = (x < 0)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   525
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   526
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   527
lemma "(-x \<le> (0::real)) = (0 \<le> x)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   528
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   529
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   530
lemma "((0::real) \<le> -x) = (x \<le> 0)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   531
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   532
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   533
lemma "(x::real) = y \<or> x < y \<or> y < x"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   534
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   535
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   536
lemma "(x::real) = 0 \<or> 0 < x \<or> 0 < -x"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   537
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   538
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   539
lemma "(0::real) \<le> x \<or> 0 \<le> -x"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   540
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   541
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   542
lemma "((x::real) + y \<le> x + z) = (y \<le> z)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   543
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   544
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   545
lemma "((x::real) + z \<le> y + z) = (x \<le> y)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   546
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   547
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   548
lemma "(w::real) < x \<and> y < z ==> w + y < x + z"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   549
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   550
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   551
lemma "(w::real) \<le> x \<and> y \<le> z ==> w + y \<le> x + z"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   552
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   553
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   554
lemma "(0::real) \<le> x \<and> 0 \<le> y ==> 0 \<le> x + y"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   555
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   556
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   557
lemma "(0::real) < x \<and> 0 < y ==> 0 < x + y"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   558
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   559
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   560
lemma "(-x < y) = (0 < x + (y::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   561
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   562
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   563
lemma "(x < -y) = (x + y < (0::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   564
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   565
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   566
lemma "(y < x + -z) = (y + z < (x::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   567
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   568
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   569
lemma "(x + -y < z) = (x < z + (y::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   570
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   571
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   572
lemma "x \<le> y ==> x < y + (1::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   573
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   574
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   575
lemma "(x - y) + y = (x::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   576
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   577
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   578
lemma "y + (x - y) = (x::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   579
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   580
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   581
lemma "x - x = (0::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   582
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   583
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   584
lemma "(x - y = 0) = (x = (y::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   585
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   586
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   587
lemma "((0::real) \<le> x + x) = (0 \<le> x)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   588
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   589
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   590
lemma "(-x \<le> x) = ((0::real) \<le> x)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   591
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   592
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   593
lemma "(x \<le> -x) = (x \<le> (0::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   594
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   595
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   596
lemma "(-x = (0::real)) = (x = 0)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   597
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   598
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   599
lemma "-(x - y) = y - (x::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   600
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   601
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   602
lemma "((0::real) < x - y) = (y < x)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   603
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   604
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   605
lemma "((0::real) \<le> x - y) = (y \<le> x)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   606
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   607
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   608
lemma "(x + y) - x = (y::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   609
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   610
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   611
lemma "(-x = y) = (x = (-y::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   612
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   613
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   614
lemma "x < (y::real) ==> \<not>(x = y)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   615
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   616
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   617
lemma "(x \<le> x + y) = ((0::real) \<le> y)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   618
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   619
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   620
lemma "(y \<le> x + y) = ((0::real) \<le> x)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   621
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   622
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   623
lemma "(x < x + y) = ((0::real) < y)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   624
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   625
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   626
lemma "(y < x + y) = ((0::real) < x)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   627
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   628
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   629
lemma "(x - y) - x = (-y::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   630
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   631
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   632
lemma "(x + y < z) = (x < z - (y::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   633
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   634
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   635
lemma "(x - y < z) = (x < z + (y::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   636
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   637
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   638
lemma "(x < y - z) = (x + z < (y::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   639
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   640
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   641
lemma "(x \<le> y - z) = (x + z \<le> (y::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   642
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   643
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   644
lemma "(x - y \<le> z) = (x \<le> z + (y::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   645
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   646
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   647
lemma "(-x < -y) = (y < (x::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   648
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   649
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   650
lemma "(-x \<le> -y) = (y \<le> (x::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   651
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   652
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   653
lemma "(a + b) - (c + d) = (a - c) + (b - (d::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   654
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   655
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   656
lemma "(0::real) - x = -x"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   657
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   658
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   659
lemma "x - (0::real) = x"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   660
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   661
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   662
lemma "w \<le> x \<and> y < z ==> w + y < x + (z::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   663
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   664
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   665
lemma "w < x \<and> y \<le> z ==> w + y < x + (z::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   666
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   667
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   668
lemma "(0::real) \<le> x \<and> 0 < y ==> 0 < x + (y::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   669
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   670
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   671
lemma "(0::real) < x \<and> 0 \<le> y ==> 0 < x + y"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   672
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   673
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   674
lemma "-x - y = -(x + (y::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   675
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   676
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   677
lemma "x - (-y) = x + (y::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   678
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   679
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   680
lemma "-x - -y = y - (x::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   681
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   682
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   683
lemma "(a - b) + (b - c) = a - (c::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   684
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   685
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   686
lemma "(x = y - z) = (x + z = (y::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   687
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   688
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   689
lemma "(x - y = z) = (x = z + (y::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   690
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   691
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   692
lemma "x - (x - y) = (y::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   693
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   694
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   695
lemma "x - (x + y) = -(y::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   696
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   697
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   698
lemma "x = y ==> x \<le> (y::real)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   699
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   700
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   701
lemma "(0::real) < x ==> \<not>(x = 0)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   702
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   703
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   704
lemma "(x + y) * (x - y) = (x * x) - (y * y)"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   705
  oops
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   706
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   707
lemma "(-x = -y) = (x = (y::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   708
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   709
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   710
lemma "(-x < -y) = (y < (x::real))"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   711
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   712
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   713
lemma "!!a::real. a \<le> b ==> c \<le> d ==> x + y < z ==> a + c \<le> b + d"
31066
972c870da225 explicit method linarith
haftmann
parents: 28952
diff changeset
   714
by linarith
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   715
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   716
lemma "!!a::real. a < b ==> c < d ==> a - d \<le> b + (-c)"
31066
972c870da225 explicit method linarith
haftmann
parents: 28952
diff changeset
   717
by linarith
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   718
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   719
lemma "!!a::real. a \<le> b ==> b + b \<le> c ==> a + a \<le> c"
31066
972c870da225 explicit method linarith
haftmann
parents: 28952
diff changeset
   720
by linarith
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   721
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   722
lemma "!!a::real. a + b \<le> i + j ==> a \<le> b ==> i \<le> j ==> a + a \<le> j + j"
31066
972c870da225 explicit method linarith
haftmann
parents: 28952
diff changeset
   723
by linarith
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   724
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   725
lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j"
31066
972c870da225 explicit method linarith
haftmann
parents: 28952
diff changeset
   726
by linarith
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   727
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   728
lemma "!!a::real. a + b + c \<le> i + j + k \<and> a \<le> b \<and> b \<le> c \<and> i \<le> j \<and> j \<le> k --> a + a + a \<le> k + k + k"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   729
by arith
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   730
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   731
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   732
    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l"
31066
972c870da225 explicit method linarith
haftmann
parents: 28952
diff changeset
   733
by linarith
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   734
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   735
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   736
    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l"
31066
972c870da225 explicit method linarith
haftmann
parents: 28952
diff changeset
   737
by linarith
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   738
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   739
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   740
    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i"
31066
972c870da225 explicit method linarith
haftmann
parents: 28952
diff changeset
   741
by linarith
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   742
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   743
lemma "!!a::real. a + b + c + d \<le> i + j + k + l ==> a \<le> b ==> b \<le> c
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   744
    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a + a \<le> l + l + l + l + i + l"
31066
972c870da225 explicit method linarith
haftmann
parents: 28952
diff changeset
   745
by linarith
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   746
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   747
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   748
subsection{*Complex Arithmetic*}
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   749
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   750
lemma "(1359 + 93746*ii) - (2468 + 46375*ii) = -1109 + 47371*ii"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   751
by simp
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   752
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   753
lemma "- (65745 + -47371*ii) = -65745 + 47371*ii"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   754
by simp
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   755
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   756
text{*Multiplication requires distributive laws.  Perhaps versions instantiated
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   757
to literal constants should be added to the simpset.*}
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   758
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   759
lemma "(1 + ii) * (1 - ii) = 2"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   760
by (simp add: ring_distribs)
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   761
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   762
lemma "(1 + 2*ii) * (1 + 3*ii) = -5 + 5*ii"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   763
by (simp add: ring_distribs)
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   764
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   765
lemma "(-84 + 255*ii) + (51 * 255*ii) = -84 + 13260 * ii"
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   766
by (simp add: ring_distribs)
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   767
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   768
text{*No inequalities or linear arithmetic: the complex numbers are unordered!*}
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   769
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   770
text{*No powers (not supported yet)*}
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 20807
diff changeset
   771
5545
9117a0e2bf31 added correctness proofs for arithmetic
paulson
parents: 5199
diff changeset
   772
end