Quelle Pattern_Nits.thy Sprache: Isabelle

(*  Title:      HOL/Nitpick_Examples/Pattern_Nits.thy
    Author:     Jasmin Blanchette, TU Muenchen
    Copyright   2009-2011

Examples featuring Nitpick's "destroy_constrs" optimization.
*)

section \<open>Examples Featuring Nitpick's \textit{destroy\_constrs} Optimization\<close>

theory Pattern_Nits
imports Main
begin

nitpick_params [verbose, card = 8, max_potential = 0, sat_solver = MiniSat,
                max_threads = 1, timeout = 240]

lemma "x = (case u of () \ y)"
nitpick [expect = genuine]
oops

lemma "x = (case b of True \ x | False \ y)"
nitpick [expect = genuine]
oops

lemma "x = (case p of (x, y) \ y)"
nitpick [expect = genuine]
oops

lemma "x = (case n of 0 \ x | Suc n \ n)"
nitpick [expect = genuine]
oops

lemma "x = (case opt of None \ x | Some y \ y)"
nitpick [expect = genuine]
oops

lemma "x = (case xs of [] \ x | y # ys \ y)"
nitpick [expect = genuine]
oops

lemma "x = (case xs of
              [] \<Rightarrow> x
            | y # ys \<Rightarrow>
              (case ys of
                 [] \<Rightarrow> x
               | z # zs \<Rightarrow>
                 (case z of
                    None \<Rightarrow> x
                  | Some p \<Rightarrow>
                    (case p of
                       (a, b) \<Rightarrow> b))))"
nitpick [expect = genuine]
oops

fun f1 where
"f1 x () = x"

lemma "x = f1 y u"
nitpick [expect = genuine]
oops

fun f2 where
"f2 x _ True = x" |
"f2 _ y False = y"

lemma "x = f2 x y b"
nitpick [expect = genuine]
oops

fun f3 where
"f3 (_, y) = y"

lemma "x = f3 p"
nitpick [expect = genuine]
oops

fun f4 where
"f4 x 0 = x" |
"f4 _ (Suc n) = n"

lemma "x = f4 x n"
nitpick [expect = genuine]
oops

fun f5 where
"f5 x None = x" |
"f5 _ (Some y) = y"

lemma "x = f5 x opt"
nitpick [expect = genuine]
oops

fun f6 where
"f6 x [] = x" |
"f6 _ (y # ys) = y"

lemma "x = f6 x xs"
nitpick [expect = genuine]
oops

fun f7 where
"f7 _ (y # Some (a, b) # zs) = b" |
"f7 x (y # None # zs) = x" |
"f7 x [y] = x" |
"f7 x [] = x"

lemma "x = f7 x xs"
nitpick [expect = genuine]
oops

lemma "u = ()"
nitpick [expect = none]
sorry

lemma "\y. (b::bool) = y"
nitpick [expect = none]
sorry

lemma "\x y. p = (x, y)"
nitpick [expect = none]
sorry

lemma "\x. n = Suc x"
nitpick [expect = genuine]
oops

lemma "\y. x = Some y"
nitpick [expect = genuine]
oops

lemma "\y ys. xs = y # ys"
nitpick [expect = genuine]
oops

lemma "\y a b zs. x = y # Some (a, b) # zs"
nitpick [expect = genuine]
oops

end

quality99%

¤ 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.