(* Title: HOL/Nitpick_Examples/Core_Nits.thy
Author: Jasmin Blanchette, TU Muenchen
Copyright 2009
Examples featuring Nitpick's functional core.
*)
header {* Examples Featuring Nitpick's Functional Core *}
theory Core_Nits
imports Main
begin
nitpick_params [sat_solver = MiniSatJNI, max_threads = 1, timeout = 60 s]
subsection {* Curry in a Hurry *}
lemma "(\f x y. (curry o split) f x y) = (\f x y. (\x. x) f x y)"
nitpick [card = 1\4, expect = none]
nitpick [card = 100, expect = none, timeout = none]
by auto
lemma "(\f p. (split o curry) f p) = (\f p. (\x. x) f p)"
nitpick [card = 2]
nitpick [card = 1\4, expect = none]
nitpick [card = 10, expect = none]
by auto
lemma "split (curry f) = f"
nitpick [card = 1\4, expect = none]
nitpick [card = 10, expect = none]
nitpick [card = 40, expect = none]
by auto
lemma "curry (split f) = f"
nitpick [card = 1\4, expect = none]
nitpick [card = 40, expect = none]
by auto
lemma "(split o curry) f = f"
nitpick [card = 1\4, expect = none]
nitpick [card = 40, expect = none]
by auto
lemma "(curry o split) f = f"
nitpick [card = 1\4, expect = none]
nitpick [card = 1000, expect = none]
by auto
lemma "(split o curry) f = (\x. x) f"
nitpick [card = 1\4, expect = none]
nitpick [card = 40, expect = none]
by auto
lemma "(curry o split) f = (\x. x) f"
nitpick [card = 1\4, expect = none]
nitpick [card = 40, expect = none]
by auto
lemma "((split o curry) f) p = ((\x. x) f) p"
nitpick [card = 1\4, expect = none]
nitpick [card = 40, expect = none]
by auto
lemma "((curry o split) f) x = ((\x. x) f) x"
nitpick [card = 1\4, expect = none]
nitpick [card = 1000, expect = none]
by auto
lemma "((curry o split) f) x y = ((\x. x) f) x y"
nitpick [card = 1\4, expect = none]
nitpick [card = 1000, expect = none]
by auto
lemma "split o curry = (\x. x)"
nitpick [card = 1\4, expect = none]
nitpick [card = 40, expect = none]
apply (rule ext)+
by auto
lemma "curry o split = (\x. x)"
nitpick [card = 1\4, expect = none]
nitpick [card = 100, expect = none]
apply (rule ext)+
by auto
lemma "split (\x y. f (x, y)) = f"
nitpick [card = 1\4, expect = none]
nitpick [card = 40, expect = none]
by auto
subsection {* Representations *}
lemma "\f. f = (\x. x) \ f y = y"
nitpick [expect = none]
by auto
lemma "(\g. \x. g (f x) = x) \ (\y. \x. y = f x)"
nitpick [card 'a = 35, card 'b = 34, expect = genuine]
nitpick [card = 1\15, mono, expect = none]
oops
lemma "\f. f = (\x. x) \ f y \ y"
nitpick [card = 1, expect = genuine]
nitpick [card = 2, expect = genuine]
nitpick [card = 5, expect = genuine]
oops
lemma "P (\x. x)"
nitpick [card = 1, expect = genuine]
nitpick [card = 5, expect = genuine]
oops
lemma "{(a\'a\'a, b\'b)}^-1 = {(b, a)}"
nitpick [card = 1\6, expect = none]
nitpick [card = 20, expect = none]
by auto
lemma "fst (a, b) = a"
nitpick [card = 1\20, expect = none]
by auto
lemma "\P. P = Id"
nitpick [card = 1\4, expect = none]
by auto
lemma "(a\'a\'b, a) \ Id\<^sup>*"
nitpick [card = 1\3, expect = none]
by auto
lemma "(a\'a\'a, a) \ Id\<^sup>* \ {(a, b)}\<^sup>*"
nitpick [card = 1\6, expect = none]
by auto
lemma "Id (a, a)"
nitpick [card = 1\100, expect = none]
by (auto simp: Id_def Collect_def)
lemma "Id ((a\'a, b\'a), (a, b))"
nitpick [card = 1\10, expect = none]
by (auto simp: Id_def Collect_def)
lemma "UNIV (x\'a\'a)"
nitpick [card = 1\50, expect = none]
sorry
lemma "{} = A - A"
nitpick [card = 1\100, expect = none]
by auto
lemma "g = Let (A \ B)"
nitpick [card = 1, expect = none]
nitpick [card = 2, expect = genuine]
nitpick [card = 20, expect = genuine]
oops
lemma "(let a_or_b = A \ B in a_or_b \ \ a_or_b)"
nitpick [expect = none]
by auto
lemma "A \ B"
nitpick [card = 100, expect = genuine]
oops
lemma "A = {b}"
nitpick [card = 100, expect = genuine]
oops
lemma "{a, b} = {b}"
nitpick [card = 100, expect = genuine]
oops
lemma "(a\'a\'a, a\'a\'a) \ R"
nitpick [card = 1, expect = genuine]
nitpick [card = 2, expect = genuine]
nitpick [card = 4, expect = genuine]
nitpick [card = 20, expect = genuine]
nitpick [card = 10, dont_box, expect = genuine]
oops
lemma "f (g\'a\'a) = x"
nitpick [card = 3, expect = genuine]
nitpick [card = 3, dont_box, expect = genuine]
nitpick [card = 5, expect = genuine]
nitpick [card = 10, expect = genuine]
oops
lemma "f (a, b) = x"
nitpick [card = 3, expect = genuine]
nitpick [card = 10, expect = genuine]
nitpick [card = 16, expect = genuine]
nitpick [card = 30, expect = genuine]
oops
lemma "f (a, a) = f (c, d)"
nitpick [card = 4, expect = genuine]
nitpick [card = 20, expect = genuine]
oops
lemma "(x\'a) = (\a. \b. \c. if c then a else b) x x True"
nitpick [card = 2, expect = none]
by auto
lemma "\F. F a b = G a b"
nitpick [card = 3, expect = none]
by auto
lemma "f = split"
nitpick [card = 1, expect = none]
nitpick [card = 2, expect = genuine]
oops
lemma "(A\'a\'a, B\'a\'a) \ R \ (A, B) \ R"
nitpick [card = 20, expect = none]
by auto
lemma "(A, B) \ R \ (\C. (A, C) \ R \ (C, B) \ R) \
A = B \ (A, B) \ R \ (\C. (A, C) \ R \ (C, B) \ R)"
nitpick [card = 1\50, expect = none]
by auto
lemma "f = (\x\'a\'b. x)"
nitpick [card = 3, expect = genuine]
nitpick [card = 4, expect = genuine]
nitpick [card = 8, expect = genuine]
oops
subsection {* Quantifiers *}
lemma "x = y"
nitpick [card 'a = 1, expect = none]
nitpick [card 'a = 2, expect = genuine]
nitpick [card 'a = 100, expect = genuine]
nitpick [card 'a = 1000, expect = genuine]
oops
lemma "\x. x = y"
nitpick [card 'a = 1, expect = none]
nitpick [card 'a = 2, expect = genuine]
nitpick [card 'a = 100, expect = genuine]
nitpick [card 'a = 1000, expect = genuine]
oops
lemma "\x\'a \ bool. x = y"
nitpick [card 'a = 1, expect = genuine]
nitpick [card 'a = 2, expect = genuine]
nitpick [card 'a = 100, expect = genuine]
nitpick [card 'a = 1000, expect = genuine]
oops
lemma "\x\'a \ bool. x = y"
nitpick [card 'a = 1\10, expect = none]
by auto
lemma "\x y\'a \ bool. x = y"
nitpick [card = 1\40, expect = none]
by auto
lemma "\x. \y. f x y = f x (g x)"
nitpick [card = 1\5, expect = none]
by auto
lemma "\u. \v. \w. \x. f u v w x = f u (g u) w (h u w)"
nitpick [card = 1\5, expect = none]
by auto
lemma "\u. \v. \w. \x. f u v w x = f u (g u w) w (h u)"
nitpick [card = 1\2, expect = genuine]
nitpick [card = 3, expect = genuine]
oops
lemma "\u. \v. \w. \x. \y. \z.
f u v w x y z = f u (g u) w (h u w) y (k u w y)"
nitpick [card = 1\2, expect = none]
nitpick [card = 3, expect = none]
nitpick [card = 4, expect = none]
sorry
lemma "\u. \v. \w. \x. \y. \z.
f u v w x y z = f u (g u) w (h u w y) y (k u w y)"
nitpick [card = 1\2, expect = genuine]
oops
lemma "\u. \v. \w. \x. \y. \z.
f u v w x y z = f u (g u w) w (h u w) y (k u w y)"
nitpick [card = 1\2, expect = genuine]
oops
lemma "\u\'a \ 'b. \v\'c. \w\'d. \x\'e \ 'f.
f u v w x = f u (g u) w (h u w)"
nitpick [card = 1\2, expect = none]
sorry
lemma "\u\'a \ 'b. \v\'c. \w\'d. \x\'e \ 'f.
f u v w x = f u (g u w) w (h u)"
nitpick [card = 1\2, dont_box, expect = genuine]
oops
lemma "\u\'a \ 'b. \v\'c. \w\'d. \x\'e \ 'f.
f u v w x = f u (g u) w (h u w)"
nitpick [card = 1\2, dont_box, expect = none]
sorry
lemma "\u\'a \ 'b. \v\'c. \w\'d. \x\'e \ 'f.
f u v w x = f u (g u w) w (h u)"
nitpick [card = 1\2, dont_box, expect = genuine]
oops
lemma "\x. if (\y. x = y) then False else True"
nitpick [card = 1, expect = genuine]
nitpick [card = 2\5, expect = none]
oops
lemma "\x\'a\'b. if (\y. x = y) then False else True"
nitpick [card = 1, expect = genuine]
nitpick [card = 2, expect = none]
oops
lemma "\x. if (\y. x = y) then True else False"
nitpick [expect = none]
sorry
lemma "\x\'a\'b. if (\y. x = y) then True else False"
nitpick [expect = none]
sorry
lemma "(\ (\x. P x)) \ (\x. \ P x)"
nitpick [expect = none]
by auto
lemma "(\ \ (\x. P x)) \ (\ (\x. \ P x))"
nitpick [expect = none]
by auto
lemma "(\x\'a. \y. P x y) \ (\x\'a \ 'a. \y. P y x)"
nitpick [card 'a = 1, expect = genuine]
nitpick [card 'a = 2, expect = genuine]
nitpick [card 'a = 3, expect = genuine]
nitpick [card 'a = 4, expect = genuine]
nitpick [card 'a = 5, expect = genuine]
oops
lemma "\x. if x = y then (\y. y = x \ y \ x)
else (\y. y = (x, x) \ y \ (x, x))"
nitpick [expect = none]
by auto
lemma "\x. if x = y then (\y. y = x \ y \ x)
else (\y. y = (x, x) \ y \ (x, x))"
nitpick [expect = none]
by auto
lemma "let x = (\x. P x) in if x then x else \ x"
nitpick [expect = none]
by auto
lemma "let x = (\x\'a \ 'b. P x) in if x then x else \ x"
nitpick [expect = none]
by auto
subsection {* Schematic Variables *}
lemma "x = ?x"
nitpick [expect = none]
by auto
lemma "\x. x = ?x"
nitpick [expect = genuine]
oops
lemma "\x. x = ?x"
nitpick [expect = none]
by auto
lemma "\x\'a \