Quelle Arith_Examples.thy Sprache: Isabelle

(*  Title:  HOL/ex/Arith_Examples.thy
    Author: Tjark Weber
*)

section \<open>Arithmetic\<close>

theory Arith_Examples
imports Main
begin

text \<open>
  The \<open>arith\<close> method is used frequently throughout the Isabelle
  distribution.  This file merely contains some additional tests and special
  corner cases.  Some rather technical remarks:

  \<^ML>\<open>Lin_Arith.simple_tac\<close> is a very basic version of the tactic.  It performs no
  meta-to-object-logic conversion, and only some splitting of operators.
  \<^ML>\<open>Lin_Arith.tac\<close> performs meta-to-object-logic conversion, full
  splitting of operators, and NNF normalization of the goal.  The \<open>arith\<close>
  method combines them both, and tries other methods (e.g.~\<open>presburger\<close>)
  as well.  This is the one that you should use in your proofs!

  An \<open>arith\<close>-based simproc is available as well (see \<^ML>\<open>Lin_Arith.simproc\<close>), which---for performance
  reasons---however does even less splitting than \<^ML>\<open>Lin_Arith.simple_tac\<close>
  at the moment (namely inequalities only).  (On the other hand, it
  does take apart conjunctions, which \<^ML>\<open>Lin_Arith.simple_tac\<close> currently
  does not do.)
\<close>

subsection \<open>Splitting of Operators: \<^term>\<open>max\<close>, \<^term>\<open>min\<close>, \<^term>\<open>abs\<close>,
           \<^term>\<open>minus\<close>, \<^term>\<open>nat\<close>, \<^term>\<open>modulo\<close>,
           \<^term>\<open>divide\<close>\<close>

lemma "(i::nat) <= max i j"
  by linarith

lemma "(i::int) <= max i j"
  by linarith

lemma "min i j <= (i::nat)"
  by linarith

lemma "min i j <= (i::int)"
  by linarith

lemma "min (i::nat) j <= max i j"
  by linarith

lemma "min (i::int) j <= max i j"
  by linarith

lemma "min (i::nat) j + max i j = i + j"
  by linarith

lemma "min (i::int) j + max i j = i + j"
  by linarith

lemma "(i::nat) < j ==> min i j < max i j"
  by linarith

lemma "(i::int) < j ==> min i j < max i j"
  by linarith

lemma "(0::int) <= \i\"
  by linarith

lemma "(i::int) <= \i\"
  by linarith

lemma "\\i::int\\ = \i\"
  by linarith

text \<open>Also testing subgoals with bound variables.\<close>

lemma "!!x. (x::nat) <= y ==> x - y = 0"
  by linarith

lemma "!!x. (x::nat) - y = 0 ==> x <= y"
  by linarith

lemma "!!x. ((x::nat) <= y) = (x - y = 0)"
  by linarith

lemma "[| (x::nat) < y; d < 1 |] ==> x - y = d"
  by linarith

lemma "[| (x::nat) < y; d < 1 |] ==> x - y - x = d - x"
  by linarith

lemma "(x::int) < y ==> x - y < 0"
  by linarith

lemma "nat (i + j) <= nat i + nat j"
  by linarith

lemma "i < j ==> nat (i - j) = 0"
  by linarith

lemma "(i::nat) mod 0 = i"
  using split_mod [of _ _ 0, linarith_split]
    \<comment> \<open>rule \<^text>\<open>split_mod\<close> is only declared by default for numerals\<close>
  by linarith

lemma "(i::nat) mod 1 = 0"
  (* rule split_mod is only declared by default for numerals *)
  using split_mod [of _ _ 1, linarith_split]
    \<comment> \<open>rule \<^text>\<open>split_mod\<close> is only declared by default for numerals\<close>
  by linarith

lemma "(i::nat) mod 42 <= 41"
  by linarith

lemma "(i::int) mod 0 = i"
  using split_zmod [of _ _ 0, linarith_split]
    \<comment> \<open>rule \<^text>\<open>split_zmod\<close> is only declared by default for numerals\<close>
  by linarith

lemma "(i::int) mod 1 = 0"
  using split_zmod [of _ _ "1", linarith_split]
    \<comment> \<open>rule \<^text>\<open>split_zmod\<close> is only declared by default for numerals\<close>
  by linarith

lemma "(i::int) mod 42 <= 41"
  by linarith

lemma "-(i::int) * 1 = 0 ==> i = 0"
  by linarith

lemma "[| (0::int) < \i\; \i\ * 1 < \i\ * j |] ==> 1 < \i\ * j"
  by linarith

subsection \<open>Meta-Logic\<close>

lemma "x < Suc y == x <= y"
  by linarith

lemma "((x::nat) == z ==> x ~= y) ==> x ~= y | z ~= y"
  by linarith

subsection \<open>Various Other Examples\<close>

lemma "(x < Suc y) = (x <= y)"
  by linarith

lemma "[| (x::nat) < y; y < z |] ==> x < z"
  by linarith

lemma "(x::nat) < y & y < z ==> x < z"
  by linarith

text \<open>This example involves no arithmetic at all, but is solved by
  preprocessing (i.e. NNF normalization) alone.\<close>

lemma "(P::bool) = Q ==> Q = P"
  by linarith

lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> min (x::nat) y = 0"
  by linarith

lemma "[| P = (x = 0); (~P) = (y = 0) |] ==> max (x::nat) y = x + y"
  by linarith

lemma "[| (x::nat) ~= y; a + 2 = b; a < y; y < b; a < x; x < b |] ==> False"
  by linarith

lemma "[| (x::nat) > y; y > z; z > x |] ==> False"
  by linarith

lemma "(x::nat) - 5 > y ==> y < x"
  by linarith

lemma "(x::nat) ~= 0 ==> 0 < x"
  by linarith

lemma "[| (x::nat) ~= y; x <= y |] ==> x < y"
  by linarith

lemma "[| (x::nat) < y; P (x - y) |] ==> P 0"
  by linarith

lemma "(x - y) - (x::nat) = (x - x) - y"
  by linarith

lemma "[| (a::nat) < b; c < d |] ==> (a - b) = (c - d)"
  by linarith

lemma "((a::nat) - (b - (c - (d - e)))) = (a - (b - (c - (d - e))))"
  by linarith

lemma "(n < m & m < n') | (n < m & m = n') | (n < n' & n' < m) |
  (n = n' & n' < m) | (n = m & m < n') |
  (n' < m & m < n) | (n' < m & m = n) |
  (n' < n & n < m) | (n' = n & n < m) | (n' = m & m < n) |
  (m < n & n < n') | (m < n & n' = n) | (m < n' & n' < n) |
  (m = n & n < n') | (m = n' & n' < n) |
  (n' = m & m = (n::nat))"
(* FIXME: this should work in principle, but is extremely slow because     *)
(*        preprocessing negates the goal and tries to compute its negation *)
(*        normal form, which creates lots of separate cases for this       *)
(*        disjunction of conjunctions                                      *)
(* by (tactic {* Lin_Arith.tac 1 *}) *)
oops

lemma "2 * (x::nat) ~= 1"
(* FIXME: this is beyond the scope of the decision procedure at the moment, *)
(*        because its negation is satisfiable in the rationals?             *)
(* by (tactic {* Lin_Arith.simple_tac 1 *}) *)
oops

text \<open>Constants.\<close>

lemma "(0::nat) < 1"
  by linarith

lemma "(0::int) < 1"
  by linarith

lemma "(47::nat) + 11 < 8 * 15"
  by linarith

lemma "(47::int) + 11 < 8 * 15"
  by linarith

text \<open>Splitting of inequalities of different type.\<close>

lemma "[| (a::nat) ~= b; (i::int) ~= j; a < 2; b < 2 |] ==>
  a + b <= nat (max \<bar>i\<bar> \<bar>j\<bar>)"
  by linarith

text \<open>Again, but different order.\<close>

lemma "[| (i::int) ~= j; (a::nat) ~= b; a < 2; b < 2 |] ==>
  a + b <= nat (max \<bar>i\<bar> \<bar>j\<bar>)"
  by linarith

end

quality100%

¤ Dauer der Verarbeitung: 0.11 Sekunden (vorverarbeitet) ¤

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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.