Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Arith_Examples.thy   Sprache: Isabelle

Original von: 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, arith_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, arith_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, arith_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", arith_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

¤ Dauer der Verarbeitung: 0.16 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

in der Quellcodebibliothek suchen




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.


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik