|
(* 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_JNI,
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
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤
|
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.
|
