Quelle  Core_Nits.thy   Sprache: Isabelle

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

Examples featuring Nitpick's functional core.
*)

section ‹Examples Featuring Nitpick's Functional Core\

theory Core_Nits
imports Main
begin

nitpick_params [verbose, card = 1-6, unary_ints, max_potential = 0,
                sat_solver = MiniSat, max_threads = 1, timeout = 240]

subsection ‹Curry in a Hurry›

lemma "(\f x y. (curry o case_prod) f x y) = (\f x y. (\x. x) f x y)"
nitpick [card = 1-12, expect = none]
by auto

lemma "(\f p. (case_prod o curry) f p) = (\f p. (\x. x) f p)"
nitpick [card = 1-12, expect = none]
by auto

lemma "case_prod (curry f) = f"
nitpick [card = 1-12, expect = none]
by auto

lemma "curry (case_prod f) = f"
nitpick [card = 1-12, expect = none]
by auto

lemma "case_prod (\x y. f (x, y)) = f"
nitpick [card = 1-12, 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 = 25, card 'b = 24, expect = genuine]
nitpick [card = 1-10, mono, expect = none]
oops

lemma "\f. f = (\x. x) \ f y \ y"
nitpick [card = 1, expect = genuine]
oops

lemma "P (\x. x)"
nitpick [card = 1, expect = genuine]
oops

lemma "{(a::'a\'a, b::'b)}\ = {(b, a)}"
nitpick [card = 1-12, expect = none]
by auto

lemma "fst (a, b) = a"
nitpick [card = 1-20, expect = none]
by auto

lemma "\P. P = Id"
nitpick [card = 1-20, expect = none]
by auto

lemma "(a::'a\'b, a) \ Id\<^sup>*"
nitpick [card = 1-2, expect = none]
by auto

lemma "(a::'a\'a, a) \ Id\<^sup>* \ {(a, b)}\<^sup>*"
nitpick [card = 1-4, expect = none]
by auto

lemma "(a, a) \ Id"
nitpick [card = 1-50, expect = none]
by (auto simp: Id_def)

lemma "((a::'a, b::'a), (a, b)) \ Id"
nitpick [card = 1-10, expect = none]
by (auto simp: Id_def)

lemma "(x::'a\'a) \ UNIV"
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 = 12, 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 = 50, expect = genuine]
oops

lemma "(a::'a\'a, a::'a\'a) \ R"
nitpick [card = 1, expect = genuine]
nitpick [card = 10, expect = genuine]
nitpick [card = 5, dont_box, expect = genuine]
oops

lemma "f (g::'a\'a) = x"
nitpick [card = 3, dont_box, expect = genuine]
nitpick [card = 8, expect = genuine]
oops

lemma "f (a, b) = x"
nitpick [card = 10, expect = genuine]
oops

lemma "f (a, a) = f (c, d)"
nitpick [card = 10, expect = genuine]
oops

lemma "(x::'a) = (\a. \b. \c. if c then a else b) x x True"
nitpick [card = 1-10, expect = none]
by auto

lemma "\F. F a b = G a b"
nitpick [card = 2, expect = none]
by auto

lemma "f = case_prod"
nitpick [card = 2, expect = genuine]
oops

lemma "(A::'a\'a, B::'a\'a) \ R \ (A, B) \ R"
nitpick [card = 15, 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-25, expect = none]
by auto

lemma "f = (\x::'a\'b. x)"
nitpick [card = 8, expect = genuine]
oops

subsection ‹Quantifiers›

lemma "x = y"
nitpick [card 'a = 1, expect = none]
nitpick [card 'a = 100, expect = genuine]
oops

lemma "\x. x = y"
nitpick [card 'a = 1, expect = none]
nitpick [card 'a = 100, expect = genuine]
oops

lemma "\x::'a \ bool. x = y"
nitpick [card 'a = 1, expect = genuine]
nitpick [card 'a = 100, expect = genuine]
oops

lemma "\x::'a \ bool. x = y"
nitpick [card 'a = 1-15, expect = none]
by auto

lemma "\x y::'a \ bool. x = y"
nitpick [card = 1-15, expect = none]
by auto

lemma "\x. \y. f x y = f x (g x)"
nitpick [card = 1-4, 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-4, expect = none]
by auto

lemma "\u. \v. \w. \x. f u v w x = f u (g u w) w (h u)"
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]
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. \y. P x y) \ (\x::'a \ 'a. \y. P y x)"
nitpick [card 'a = 1, 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›

schematic_goal "x = ?x"
nitpick [expect = none]
by auto

schematic_goal "\x. x = ?x"
nitpick [expect = genuine]
oops

schematic_goal "\x. x = ?x"
nitpick [expect = none]
by auto

schematic_goal "\x::'a \ 'b. x = ?x"
nitpick [expect = none]
by auto

schematic_goal "\x. ?x = ?y"
nitpick [expect = none]
by auto

schematic_goal "\x. ?x = ?y"
nitpick [expect = none]
by auto

subsection ‹Known Constants›

lemma "x \ Pure.all \ False"
nitpick [card = 1, expect = genuine]
nitpick [card = 1, box "('a \ prop) \ prop", expect = genuine]
nitpick [card = 6, expect = genuine]
oops

lemma "\x. f x y = f x y"
nitpick [expect = none]
oops

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

lemma "Pure.all (\x. Trueprop (f x y = f x y)) \ Trueprop True"
nitpick [expect = none]
by auto

lemma "Pure.all (\x. Trueprop (f x y = f x y)) \ Trueprop False"
nitpick [expect = genuine]
oops

lemma "I = (\x. x) \ Pure.all P \ Pure.all (\x. P (I x))"
nitpick [expect = none]
by auto

lemma "x \ (\) \ False"
nitpick [card = 1, expect = genuine]
oops

lemma "P x \ P x"
nitpick [card = 1-10, expect = none]
by auto

lemma "P x \ Q x \ P x = Q x"
nitpick [card = 1-10, expect = none]
by auto

lemma "P x = Q x \ P x \ Q x"
nitpick [card = 1-10, expect = none]
by auto

lemma "x \ (\) \ False"
nitpick [expect = genuine]
oops

lemma "I \ (\x. x) \ ((\) x) \ (\y. ((\) x (I y)))"
nitpick [expect = none]
by auto

lemma "P x \ P x"
nitpick [card = 1-10, expect = none]
by auto

lemma "True \ True" "False \ True" "False \ False"
nitpick [expect = none]
by auto

lemma "True \ False"
nitpick [expect = genuine]
oops

lemma "x = Not"
nitpick [expect = genuine]
oops

lemma "I = (\x. x) \ Not = (\x. Not (I x))"
nitpick [expect = none]
by auto

lemma "x = True"
nitpick [expect = genuine]
oops

lemma "x = False"
nitpick [expect = genuine]
oops

lemma "x = undefined"
nitpick [expect = genuine]
oops

lemma "(False, ()) = undefined \ ((), False) = undefined"
nitpick [expect = genuine]
oops

lemma "undefined = undefined"
nitpick [expect = none]
by auto

lemma "f undefined = f undefined"
nitpick [expect = none]
by auto

lemma "f undefined = g undefined"
nitpick [card = 33, expect = genuine]
oops

lemma "\!x. x = undefined"
nitpick [card = 15, expect = none]
by auto

lemma "x = All \ False"
nitpick [card = 1, dont_box, expect = genuine]
oops

lemma "\x. f x y = f x y"
nitpick [expect = none]
oops

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

lemma "All (\x. f x y = f x y) = True"
nitpick [expect = none]
by auto

lemma "All (\x. f x y = f x y) = False"
nitpick [expect = genuine]
oops

lemma "x = Ex \ False"
nitpick [card = 1, dont_box, expect = genuine]
oops

lemma "\x. f x y = f x y"
nitpick [expect = none]
oops

lemma "\x. f x y = f y x"
nitpick [expect = none]
oops

lemma "Ex (\x. f x y = f x y) = True"
nitpick [expect = none]
by auto

lemma "Ex (\x. f x y = f y x) = True"
nitpick [expect = none]
by auto

lemma "Ex (\x. f x y = f x y) = False"
nitpick [expect = genuine]
oops

lemma "Ex (\x. f x y \ f x y) = False"
nitpick [expect = none]
by auto

lemma "I = (\x. x) \ Ex P = Ex (\x. P (I x))"
nitpick [expect = none]
by auto

lemma "x = y \ y = x"
nitpick [expect = none]
by auto

lemma "x = y \ f x = f y"
nitpick [expect = none]
by auto

lemma "x = y \ y = z \ x = z"
nitpick [expect = none]
by auto

lemma "I = (\x. x) \ (\) = (\x. (\) (I x))"
      "I = (\x. x) \ (\) = (\x y. x \ (I y))"
nitpick [expect = none]
by auto

lemma "(a \ b) = (\ (\ a \ \ b))"
nitpick [expect = none]
by auto

lemma "a \ b \ a" "a \ b \ b"
nitpick [expect = none]
by auto

lemma "(\) = (\x. (\) x)" "((\) ) = (\x y. x \ y)"
nitpick [expect = none]
by auto

lemma "((if a then b else c) = d) = ((a \ (b = d)) \ (\ a \ (c = d)))"
nitpick [expect = none]
by auto

lemma "(if a then b else c) = (THE d. (a \ (d = b)) \ (\ a \ (d = c)))"
nitpick [expect = none]
by auto

lemma "fst (x, y) = x"
nitpick [expect = none]
by (simp add: fst_def)

lemma "snd (x, y) = y"
nitpick [expect = none]
by (simp add: snd_def)

lemma "fst (x::'a\'b, y) = x"
nitpick [expect = none]
by (simp add: fst_def)

lemma "snd (x::'a\'b, y) = y"
nitpick [expect = none]
by (simp add: snd_def)

lemma "fst (x, y::'a\'b) = x"
nitpick [expect = none]
by (simp add: fst_def)

lemma "snd (x, y::'a\'b) = y"
nitpick [expect = none]
by (simp add: snd_def)

lemma "fst (x::'a\'b, y) = x"
nitpick [expect = none]
by (simp add: fst_def)

lemma "snd (x::'a\'b, y) = y"
nitpick [expect = none]
by (simp add: snd_def)

lemma "fst (x, y::'a\'b) = x"
nitpick [expect = none]
by (simp add: fst_def)

lemma "snd (x, y::'a\'b) = y"
nitpick [expect = none]
by (simp add: snd_def)

lemma "I = (\x. x) \ fst = (\x. fst (I x))"
nitpick [expect = none]
by auto

lemma "fst (x, y) = snd (y, x)"
nitpick [expect = none]
by auto

lemma "(x, x) \ Id"
nitpick [expect = none]
by auto

lemma "(x, y) \ Id \ x = y"
nitpick [expect = none]
by auto

lemma "I = (\x. x) \ Id = {x. I x \ Id}"
nitpick [expect = none]
by auto

lemma "{} = {x. False}"
nitpick [expect = none]
by (metis empty_def)

lemma "x \ {}"
nitpick [expect = genuine]
oops

lemma "{a, b} = {b}"
nitpick [expect = genuine]
oops

lemma "{a, b} \ {b}"
nitpick [expect = genuine]
oops

lemma "{a} = {b}"
nitpick [expect = genuine]
oops

lemma "{a} \ {b}"
nitpick [expect = genuine]
oops

lemma "{a, b, c} = {c, b, a}"
nitpick [expect = none]
by auto

lemma "UNIV = {x. True}"
nitpick [expect = none]
by (simp only: UNIV_def)

lemma "x \ UNIV \ True"
nitpick [expect = none]
by (simp only: UNIV_def mem_Collect_eq)

lemma "x \ UNIV"
nitpick [expect = genuine]
oops

lemma "I = (\x. x) \ (\) = (\x. ((\) (I x)))"
nitpick [expect = none]
apply (rule ext)
apply (rule ext)
by simp

lemma "insert = (\x y. insert x (y \ y))"
nitpick [expect = none]
by simp

lemma "I = (\x. x) \ trancl = (\x. trancl (I x))"
nitpick [card = 1-2, expect = none]
by auto

lemma "rtrancl = (\x. rtrancl x \ {(y, y)})"
nitpick [card = 1-3, expect = none]
apply (rule ext)
by auto

lemma "(x, x) \ rtrancl {(y, y)}"
nitpick [expect = none]
by auto

lemma "((x, x), (x, x)) \ rtrancl {}"
nitpick [card = 1-5, expect = none]
by auto

lemma "I = (\x. x) \ (\) = (\x. (\) (I x))"
nitpick [card = 1-5, expect = none]
by auto

lemma "a \ A \ a \ (A \ B)" "b \ B \ b \ (A \ B)"
nitpick [expect = none]
by auto

lemma "I = (\x. x) \ (\) = (\x. (\) (I x))"
nitpick [card = 1-5, expect = none]
by auto

lemma "a \ A \ a \ (A \ B)" "b \ B \ b \ (A \ B)"
nitpick [card = 1-5, expect = none]
by auto

lemma "x \ ((A::'a set) - B) \ x \ A \ x \ B"
nitpick [card = 1-5, expect = none]
by auto

lemma "I = (\x. x) \ (\) = (\x. (\) (I x))"
nitpick [card = 1-5, expect = none]
by auto

lemma "A \ B \ (\a \ A. a \ B) \ (\b \ B. b \ A)"
nitpick [card = 1-5, expect = none]
by auto

lemma "A \ B \ \a \ A. a \ B"
nitpick [card = 1-5, expect = none]
by auto

lemma "A \ B \ A \ B"
nitpick [card = 5, expect = genuine]
oops

lemma "A \ B \ A \ B"
nitpick [expect = none]
by auto

lemma "I = (\x::'a set. x) \ uminus = (\x. uminus (I x))"
nitpick [card = 1-7, expect = none]
by auto

lemma "A \ - A = UNIV"
nitpick [expect = none]
by auto

lemma "A \ - A = {}"
nitpick [expect = none]
by auto

lemma "A = -(A::'a set)"
nitpick [card 'a = 10, expect = genuine]
oops

lemma "finite A"
nitpick [expect = none]
oops

lemma "finite A \ finite B"
nitpick [expect = none]
oops

lemma "All finite"
nitpick [expect = none]
oops

subsection ‹The and Eps›

lemma "x = The"
nitpick [card = 5, expect = genuine]
oops

lemma "\x. x = The"
nitpick [card = 1-3]
by auto

lemma "P x \ (\y. P y \ y = x) \ The P = x"
nitpick [expect = none]
by auto

lemma "P x \ P y \ x \ y \ The P = z"
nitpick [expect = genuine]
oops

lemma "P x \ P y \ x \ y \ The P = x \ The P = y"
nitpick [card = 2, expect = none]
nitpick [card = 3-5, expect = genuine]
oops

lemma "P x \ P (The P)"
nitpick [card = 1-2, expect = none]
nitpick [card = 8, expect = genuine]
oops

lemma "(\x. \ P x) \ The P = y"
nitpick [expect = genuine]
oops

lemma "I = (\x. x) \ The = (\x. The (I x))"
nitpick [card = 1-5, expect = none]
by auto

lemma "x = Eps"
nitpick [card = 5, expect = genuine]
oops

lemma "\x. x = Eps"
nitpick [card = 1-3, expect = none]
by auto

lemma "P x \ (\y. P y \ y = x) \ Eps P = x"
nitpick [expect = none]
by auto

lemma "P x \ P y \ x \ y \ Eps P = z"
nitpick [expect = genuine]
apply auto
oops

lemma "P x \ P (Eps P)"
nitpick [card = 1-8, expect = none]
by (metis exE_some)

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

lemma "P (Eps P)"
nitpick [expect = genuine]
oops

lemma "Eps (\x. x \ P) \ (P::nat set)"
nitpick [expect = genuine]
oops

lemma "\ P (Eps P)"
nitpick [expect = genuine]
oops

lemma "\ (P :: nat \ bool) (Eps P)"
nitpick [expect = genuine]
oops

lemma "P \ bot \ P (Eps P)"
nitpick [expect = none]
sorry

lemma "(P :: nat \ bool) \ bot \ P (Eps P)"
nitpick [expect = none]
sorry

lemma "P (The P)"
nitpick [expect = genuine]
oops

lemma "(P :: nat \ bool) (The P)"
nitpick [expect = genuine]
oops

lemma "\ P (The P)"
nitpick [expect = genuine]
oops

lemma "\ (P :: nat \ bool) (The P)"
nitpick [expect = genuine]
oops

lemma "The P \ x"
nitpick [expect = genuine]
oops

lemma "The P \ (x::nat)"
nitpick [expect = genuine]
oops

lemma "P x \ P (The P)"
nitpick [expect = genuine]
oops

lemma "P (x::nat) \ P (The P)"
nitpick [expect = genuine]
oops

lemma "P = {x} \ (THE x. x \ P) \ P"
nitpick [expect = none]
oops

lemma "P = {x::nat} \ (THE x. x \ P) \ P"
nitpick [expect = none]
oops

consts Q :: 'a

lemma "Q (Eps Q)"
nitpick [expect = genuine]
oops

lemma "(Q :: nat \ bool) (Eps Q)"
nitpick [expect = none] (* unfortunate *)
oops

lemma "\ (Q :: nat \ bool) (Eps Q)"
nitpick [expect = genuine]
oops

lemma "\ (Q :: nat \ bool) (Eps Q)"
nitpick [expect = genuine]
oops

lemma "(Q::'a \ bool) \ bot \ (Q::'a \ bool) (Eps Q)"
nitpick [expect = none]
sorry

lemma "(Q::nat \ bool) \ bot \ (Q::nat \ bool) (Eps Q)"
nitpick [expect = none]
sorry

lemma "Q (The Q)"
nitpick [expect = genuine]
oops

lemma "(Q::nat \ bool) (The Q)"
nitpick [expect = genuine]
oops

lemma "\ Q (The Q)"
nitpick [expect = genuine]
oops

lemma "\ (Q::nat \ bool) (The Q)"
nitpick [expect = genuine]
oops

lemma "The Q \ x"
nitpick [expect = genuine]
oops

lemma "The Q \ (x::nat)"
nitpick [expect = genuine]
oops

lemma "Q x \ Q (The Q)"
nitpick [expect = genuine]
oops

lemma "Q (x::nat) \ Q (The Q)"
nitpick [expect = genuine]
oops

lemma "Q = (\x::'a. x = a) \ (Q::'a \ bool) (The Q)"
nitpick [expect = none]
sorry

lemma "Q = (\x::nat. x = a) \ (Q::nat \ bool) (The Q)"
nitpick [expect = none]
sorry

nitpick_params [max_potential = 1]

lemma "(THE j. j > Suc 2 \ j \ 3) \ 0"
nitpick [card nat = 2, expect = potential]
nitpick [card nat = 6, expect = potential] (* unfortunate *)
oops

lemma "(THE j. j > Suc 2 \ j \ 4) = x \ x \ 0"
nitpick [card nat = 2, expect = potential]
nitpick [card nat = 6, expect = none]
sorry

lemma "(THE j. j > Suc 2 \ j \ 4) = x \ x = 4"
nitpick [card nat = 2, expect = potential]
nitpick [card nat = 6, expect = none]
sorry

lemma "(THE j. j > Suc 2 \ j \ 5) = x \ x = 4"
nitpick [card nat = 6, expect = genuine]
oops

lemma "(THE j. j > Suc 2 \ j \ 5) = x \ x = 4 \ x = 5"
nitpick [card nat = 6, expect = genuine]
oops

lemma "(SOME j. j > Suc 2 \ j \ 3) \ 0"
nitpick [card nat = 2, expect = potential]
nitpick [card nat = 6, expect = genuine]
oops

lemma "(SOME j. j > Suc 2 \ j \ 4) = x \ x \ 0"
nitpick [card nat = 2, expect = potential]
nitpick [card nat = 6, expect = none]
oops

lemma "(SOME j. j > Suc 2 \ j \ 4) = x \ x = 4"
nitpick [card nat = 2, expect = potential]
nitpick [card nat = 6, expect = none]
sorry

lemma "(SOME j. j > Suc 2 \ j \ 5) = x \ x = 4"
nitpick [card nat = 6, expect = genuine]
oops

lemma "(SOME j. j > Suc 2 \ j \ 5) = x \ x = 4 \ x = 5"
nitpick [card nat = 6, expect = none]
sorry

nitpick_params [max_potential = 0]

subsection ‹Destructors and Recursors›

lemma "(x::'a) = (case True of True \ x | False \ x)"
nitpick [card = 2, expect = none]
by auto

lemma "x = (case (x, y) of (x', y') \ x')"
nitpick [expect = none]
sorry

end