Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/ex/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 16.11.2025 mit Größe 14 kB

Quellcode-Bibliothek BinEx.thy Interaktion und
PortierbarkeitIsabelle

(*  Title:      HOL/ex/BinEx.thy
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge
*)

section \<open>Binary arithmetic examples\<close>

theory BinEx
imports Complex_Main
begin

subsection \<open>Regression Testing for Cancellation Simprocs\<close>

lemma "l + 2 + 2 + 2 + (l + 2) + (oo + 2) = (uu::int)"
apply simp  oops

lemma "2*u = (u::int)"
apply simp  oops

lemma "(i + j + 12 + (k::int)) - 15 = y"
apply simp  oops

lemma "(i + j + 12 + (k::int)) - 5 = y"
apply simp  oops

lemma "y - b < (b::int)"
apply simp  oops

lemma "y - (3*b + c) < (b::int) - 2*c"
apply simp  oops

lemma "(2*x - (u*v) + y) - v*3*u = (w::int)"
apply simp  oops

lemma "(2*x*u*v + (u*v)*4 + y) - v*u*4 = (w::int)"
apply simp  oops

lemma "(2*x*u*v + (u*v)*4 + y) - v*u = (w::int)"
apply simp  oops

lemma "u*v - (x*u*v + (u*v)*4 + y) = (w::int)"
apply simp  oops

lemma "(i + j + 12 + (k::int)) = u + 15 + y"
apply simp  oops

lemma "(i + j*2 + 12 + (k::int)) = j + 5 + y"
apply simp  oops

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)"
apply simp  oops

lemma "a + -(b+c) + b = (d::int)"
apply simp  oops

lemma "a + -(b+c) - b = (d::int)"
apply simp  oops

(*negative numerals*)
lemma "(i + j + -2 + (k::int)) - (u + 5 + y) = zz"
apply simp  oops

lemma "(i + j + -3 + (k::int)) < u + 5 + y"
apply simp  oops

lemma "(i + j + 3 + (k::int)) < u + -6 + y"
apply simp  oops

lemma "(i + j + -12 + (k::int)) - 15 = y"
apply simp  oops

lemma "(i + j + 12 + (k::int)) - -15 = y"
apply simp  oops

lemma "(i + j + -12 + (k::int)) - -15 = y"
apply simp  oops

lemma "- (2*i) + 3 + (2*i + 4) = (0::int)"
apply simp  oops

(*Tobias's example dated 2015-03-02*)
lemma "(pi * (real u * 2) = pi * (real (xa v) * - 2))"
apply simp oops

subsection \<open>Arithmetic Method Tests\<close>

lemma "!!a::int. [| a <= b; c <= d; x+y a+c <= b+d"
by arith

lemma "!!a::int. [| a < b; c < d |] ==> a-d+ 2 <= b+(-c)"
by arith

lemma "!!a::int. [| a < b; c < d |] ==> a+c+ 1 < b+d"
by arith

lemma "!!a::int. [| a <= b; b+b <= c |] ==> a+a <= c"
by arith

lemma "!!a::int. [| a+b <= i+j; a<=b; i<=j |] ==> a+a <= j+j"
by arith

lemma "!!a::int. [| a+b < i+j; a a+a - - (- 1) < j+j - 3"
by arith

lemma "!!a::int. a+b+c <= i+j+k & a<=b & b<=c & i<=j & j<=k --> a+a+a <= k+k+k"
by arith

lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
      ==> a <= l"
by arith

lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
      ==> a+a+a+a <= l+l+l+l"
by arith

lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
      ==> a+a+a+a+a <= l+l+l+l+i"
by arith

lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
      ==> a+a+a+a+a+a <= l+l+l+l+i+l"
by arith

lemma "!!a::int. [| a+b+c+d <= i+j+k+l; a<=b; b<=c; c<=d; i<=j; j<=k; k<=l |]
      ==> 6*a <= 5*l+i"
by arith

subsection \<open>The Integers\<close>

text \<open>Addition\<close>

lemma "(13::int) + 19 = 32"
  by simp

lemma "(1234::int) + 5678 = 6912"
  by simp

lemma "(1359::int) + -2468 = -1109"
  by simp

lemma "(93746::int) + -46375 = 47371"
  by simp

text \<open>\medskip Negation\<close>

lemma "- (65745::int) = -65745"
  by simp

lemma "- (-54321::int) = 54321"
  by simp

text \<open>\medskip Multiplication\<close>

lemma "(13::int) * 19 = 247"
  by simp

lemma "(-84::int) * 51 = -4284"
  by simp

lemma "(255::int) * 255 = 65025"
  by simp

lemma "(1359::int) * -2468 = -3354012"
  by simp

lemma "(89::int) * 10 \ 889"
  by simp

lemma "(13::int) < 18 - 4"
  by simp

lemma "(-345::int) < -242 + -100"
  by simp

lemma "(13557456::int) < 18678654"
  by simp

lemma "(999999::int) \ (1000001 + 1) - 2"
  by simp

lemma "(1234567::int) \ 1234567"
  by simp

text\<open>No integer overflow!\<close>
lemma "1234567 * (1234567::int) < 1234567*1234567*1234567"
  by simp

text \<open>\medskip Quotient and Remainder\<close>

lemma "(10::int) div 3 = 3"
  by simp

lemma "(10::int) mod 3 = 1"
  by simp

text \<open>A negative divisor\<close>

lemma "(10::int) div -3 = -4"
  by simp

lemma "(10::int) mod -3 = -2"
  by simp

text \<open>
  A negative dividend\footnote{The definition agrees with mathematical
  convention and with ML, but not with the hardware of most computers}
\<close>

lemma "(-10::int) div 3 = -4"
  by simp

lemma "(-10::int) mod 3 = 2"
  by simp

text \<open>A negative dividend \emph{and} divisor\<close>

lemma "(-10::int) div -3 = 3"
  by simp

lemma "(-10::int) mod -3 = -1"
  by simp

text \<open>A few bigger examples\<close>

lemma "(8452::int) mod 3 = 1"
  by simp

lemma "(59485::int) div 434 = 137"
  by simp

lemma "(1000006::int) mod 10 = 6"
  by simp

text \<open>\medskip Division by shifting\<close>

lemma "10000000 div 2 = (5000000::int)"
  by simp

lemma "10000001 mod 2 = (1::int)"
  by simp

lemma "10000055 div 32 = (312501::int)"
  by simp

lemma "10000055 mod 32 = (23::int)"
  by simp

lemma "100094 div 144 = (695::int)"
  by simp

lemma "100094 mod 144 = (14::int)"
  by simp

text \<open>\medskip Powers\<close>

lemma "2 ^ 10 = (1024::int)"
  by simp

lemma "(- 3) ^ 7 = (-2187::int)"
  by simp

lemma "13 ^ 7 = (62748517::int)"
  by simp

lemma "3 ^ 15 = (14348907::int)"
  by simp

lemma "(- 5) ^ 11 = (-48828125::int)"
  by simp

subsection \<open>The Natural Numbers\<close>

text \<open>Successor\<close>

lemma "Suc 99999 = 100000"
  by simp

text \<open>\medskip Addition\<close>

lemma "(13::nat) + 19 = 32"
  by simp

lemma "(1234::nat) + 5678 = 6912"
  by simp

lemma "(973646::nat) + 6475 = 980121"
  by simp

text \<open>\medskip Subtraction\<close>

lemma "(32::nat) - 14 = 18"
  by simp

lemma "(14::nat) - 15 = 0"
  by simp

lemma "(14::nat) - 1576644 = 0"
  by simp

lemma "(48273776::nat) - 3873737 = 44400039"
  by simp

text \<open>\medskip Multiplication\<close>

lemma "(12::nat) * 11 = 132"
  by simp

lemma "(647::nat) * 3643 = 2357021"
  by simp

text \<open>\medskip Quotient and Remainder\<close>

lemma "(10::nat) div 3 = 3"
  by simp

lemma "(10::nat) mod 3 = 1"
  by simp

lemma "(10000::nat) div 9 = 1111"
  by simp

lemma "(10000::nat) mod 9 = 1"
  by simp

lemma "(10000::nat) div 16 = 625"
  by simp

lemma "(10000::nat) mod 16 = 0"
  by simp

text \<open>\medskip Powers\<close>

lemma "2 ^ 12 = (4096::nat)"
  by simp

lemma "3 ^ 10 = (59049::nat)"
  by simp

lemma "12 ^ 7 = (35831808::nat)"
  by simp

lemma "3 ^ 14 = (4782969::nat)"
  by simp

lemma "5 ^ 11 = (48828125::nat)"
  by simp

text \<open>\medskip Testing the cancellation of complementary terms\<close>

lemma "y + (x + -x) = (0::int) + y"
  by simp

lemma "y + (-x + (- y + x)) = (0::int)"
  by simp

lemma "-x + (y + (- y + x)) = (0::int)"
  by simp

lemma "x + (x + (- x + (- x + (- y + - z)))) = (0::int) - y - z"
  by simp

lemma "x + x - x - x - y - z = (0::int) - y - z"
  by simp

lemma "x + y + z - (x + z) = y - (0::int)"
  by simp

lemma "x + (y + (y + (y + (-x + -x)))) = (0::int) + y - x + y + y"
  by simp

lemma "x + (y + (y + (y + (-y + -x)))) = y + (0::int) + y"
  by simp

lemma "x + y - x + z - x - y - z + x < (1::int)"
  by simp

subsection\<open>Real Arithmetic\<close>

subsubsection \<open>Addition\<close>

lemma "(1359::real) + -2468 = -1109"
by simp

lemma "(93746::real) + -46375 = 47371"
by simp

subsubsection \<open>Negation\<close>

lemma "- (65745::real) = -65745"
by simp

lemma "- (-54321::real) = 54321"
by simp

subsubsection \<open>Multiplication\<close>

lemma "(-84::real) * 51 = -4284"
by simp

lemma "(255::real) * 255 = 65025"
by simp

lemma "(1359::real) * -2468 = -3354012"
by simp

subsubsection \<open>Inequalities\<close>

lemma "(89::real) * 10 \ 889"
by simp

lemma "(13::real) < 18 - 4"
by simp

lemma "(-345::real) < -242 + -100"
by simp

lemma "(13557456::real) < 18678654"
by simp

lemma "(999999::real) \ (1000001 + 1) - 2"
by simp

lemma "(1234567::real) \ 1234567"
by simp

subsubsection \<open>Powers\<close>

lemma "2 ^ 15 = (32768::real)"
by simp

lemma "(- 3) ^ 7 = (-2187::real)"
by simp

lemma "13 ^ 7 = (62748517::real)"
by simp

lemma "3 ^ 15 = (14348907::real)"
by simp

lemma "(- 5) ^ 11 = (-48828125::real)"
by simp

subsubsection \<open>Tests\<close>

lemma "(x + y = x) = (y = (0::real))"
by arith

lemma "(x + y = y) = (x = (0::real))"
by arith

lemma "(x + y = (0::real)) = (x = -y)"
by arith

lemma "(x + y = (0::real)) = (y = -x)"
by arith

lemma "((x + y) < (x + z)) = (y < (z::real))"
by arith

lemma "((x + z) < (y + z)) = (x < (y::real))"
by arith

lemma "(\ x < y) = (y \ (x::real))"
by arith

lemma "\ (x < y \ y < (x::real))"
by arith

lemma "(x::real) < y ==> \ y < x"
by arith

lemma "((x::real) \ y) = (x < y \ y < x)"
by arith

lemma "(\ x \ y) = (y < (x::real))"
by arith

lemma "x \ y \ y \ (x::real)"
by arith

lemma "x \ y \ y < (x::real)"
by arith

lemma "x < y \ y \ (x::real)"
by arith

lemma "x \ (x::real)"
by arith

lemma "((x::real) \ y) = (x < y \ x = y)"
by arith

lemma "((x::real) \ y \ y \ x) = (x = y)"
by arith

lemma "\(x < y \ y \ (x::real))"
by arith

lemma "\(x \ y \ y < (x::real))"
by arith

lemma "(-x < (0::real)) = (0 < x)"
by arith

lemma "((0::real) < -x) = (x < 0)"
by arith

lemma "(-x \ (0::real)) = (0 \ x)"
by arith

lemma "((0::real) \ -x) = (x \ 0)"
by arith

lemma "(x::real) = y \ x < y \ y < x"
by arith

lemma "(x::real) = 0 \ 0 < x \ 0 < -x"
by arith

lemma "(0::real) \ x \ 0 \ -x"
by arith

lemma "((x::real) + y \ x + z) = (y \ z)"
by arith

lemma "((x::real) + z \ y + z) = (x \ y)"
by arith

lemma "(w::real) < x \ y < z ==> w + y < x + z"
by arith

lemma "(w::real) \ x \ y \ z ==> w + y \ x + z"
by arith

lemma "(0::real) \ x \ 0 \ y ==> 0 \ x + y"
by arith

lemma "(0::real) < x \ 0 < y ==> 0 < x + y"
by arith

lemma "(-x < y) = (0 < x + (y::real))"
by arith

lemma "(x < -y) = (x + y < (0::real))"
by arith

lemma "(y < x + -z) = (y + z < (x::real))"
by arith

lemma "(x + -y < z) = (x < z + (y::real))"
by arith

lemma "x \ y ==> x < y + (1::real)"
by arith

lemma "(x - y) + y = (x::real)"
by arith

lemma "y + (x - y) = (x::real)"
by arith

lemma "x - x = (0::real)"
by arith

lemma "(x - y = 0) = (x = (y::real))"
by arith

lemma "((0::real) \ x + x) = (0 \ x)"
by arith

lemma "(-x \ x) = ((0::real) \ x)"
by arith

lemma "(x \ -x) = (x \ (0::real))"
by arith

lemma "(-x = (0::real)) = (x = 0)"
by arith

lemma "-(x - y) = y - (x::real)"
by arith

lemma "((0::real) < x - y) = (y < x)"
by arith

lemma "((0::real) \ x - y) = (y \ x)"
by arith

lemma "(x + y) - x = (y::real)"
by arith

lemma "(-x = y) = (x = (-y::real))"
by arith

lemma "x < (y::real) ==> \(x = y)"
by arith

lemma "(x \ x + y) = ((0::real) \ y)"
by arith

lemma "(y \ x + y) = ((0::real) \ x)"
by arith

lemma "(x < x + y) = ((0::real) < y)"
by arith

lemma "(y < x + y) = ((0::real) < x)"
by arith

lemma "(x - y) - x = (-y::real)"
by arith

lemma "(x + y < z) = (x < z - (y::real))"
by arith

lemma "(x - y < z) = (x < z + (y::real))"
by arith

lemma "(x < y - z) = (x + z < (y::real))"
by arith

lemma "(x \ y - z) = (x + z \ (y::real))"
by arith

lemma "(x - y \ z) = (x \ z + (y::real))"
by arith

lemma "(-x < -y) = (y < (x::real))"
by arith

lemma "(-x \ -y) = (y \ (x::real))"
by arith

lemma "(a + b) - (c + d) = (a - c) + (b - (d::real))"
by arith

lemma "(0::real) - x = -x"
by arith

lemma "x - (0::real) = x"
by arith

lemma "w \ x \ y < z ==> w + y < x + (z::real)"
by arith

lemma "w < x \ y \ z ==> w + y < x + (z::real)"
by arith

lemma "(0::real) \ x \ 0 < y ==> 0 < x + (y::real)"
by arith

lemma "(0::real) < x \ 0 \ y ==> 0 < x + y"
by arith

lemma "-x - y = -(x + (y::real))"
by arith

lemma "x - (-y) = x + (y::real)"
by arith

lemma "-x - -y = y - (x::real)"
by arith

lemma "(a - b) + (b - c) = a - (c::real)"
by arith

lemma "(x = y - z) = (x + z = (y::real))"
by arith

lemma "(x - y = z) = (x = z + (y::real))"
by arith

lemma "x - (x - y) = (y::real)"
by arith

lemma "x - (x + y) = -(y::real)"
by arith

lemma "x = y ==> x \ (y::real)"
by arith

lemma "(0::real) < x ==> \(x = 0)"
by arith

lemma "(x + y) * (x - y) = (x * x) - (y * y)"
  oops

lemma "(-x = -y) = (x = (y::real))"
by arith

lemma "(-x < -y) = (y < (x::real))"
by arith

lemma "!!a::real. a \ b ==> c \ d ==> x + y < z ==> a + c \ b + d"
by linarith

lemma "!!a::real. a < b ==> c < d ==> a - d \ b + (-c)"
by linarith

lemma "!!a::real. a \ b ==> b + b \ c ==> a + a \ c"
by linarith

lemma "!!a::real. a + b \ i + j ==> a \ b ==> i \ j ==> a + a \ j + j"
by linarith

lemma "!!a::real. a + b < i + j ==> a < b ==> i < j ==> a + a < j + j"
by linarith

lemma "!!a::real. a + b + c \ i + j + k \ a \ b \ b \ c \ i \ j \ j \ k --> a + a + a \ k + k + k"
by arith

lemma "!!a::real. a + b + c + d \ i + j + k + l ==> a \ b ==> b \ c
    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a \<le> l"
by linarith

lemma "!!a::real. a + b + c + d \ i + j + k + l ==> a \ b ==> b \ c
    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a \<le> l + l + l + l"
by linarith

lemma "!!a::real. a + b + c + d \ i + j + k + l ==> a \ b ==> b \ c
    ==> c \<le> d ==> i \<le> j ==> j \<le> k ==> k \<le> l ==> a + a + a + a + a \<le> l + l + l + l + i"
by linarith

lemma "!!a::real. a + b + c + d \ i + j + k + l ==> a \ b ==> b \ c
    ==> 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"
by linarith

subsection\<open>Complex Arithmetic\<close>

lemma "(1359 + 93746*\) - (2468 + 46375*\) = -1109 + 47371*\"
by simp

lemma "- (65745 + -47371*\) = -65745 + 47371*\"
by simp

text\<open>Multiplication requires distributive laws.  Perhaps versions instantiated
to literal constants should be added to the simpset.\<close>

lemma "(1 + \) * (1 - \) = 2"
by (simp add: ring_distribs)

lemma "(1 + 2*\) * (1 + 3*\) = -5 + 5*\"
by (simp add: ring_distribs)

lemma "(-84 + 255*\) + (51 * 255*\) = -84 + 13260 * \"
by (simp add: ring_distribs)

text\<open>No inequalities or linear arithmetic: the complex numbers are unordered!\<close>

text\<open>No powers (not supported yet)\<close>

end

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.3Bemerkung: Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.