(* Title: HOL/Nitpick_Examples/Refute_Nits.thy Author: Jasmin Blanchette, TU Muenchen Copyright 2009-2011 Refute examples adapted to Nitpick. *) section ‹Refute Examples Adapted to Nitpick› theory Refute_Nits imports Main begin nitpick_params [verbose, card = 1-6, max_potential = 0, sat_solver = MiniSat, max_threads = 1, timeout = 240] lemma "P ∧ Q" apply (rule conjI) nitpick [expect = genuine] 1 nitpick [expect = genuine] 2 nitpick [expect = genuine] nitpick [card = 5, expect = genuine] nitpick [sat_solver = SAT4J, expect = genuine] 2 oops subsection ‹Examples and Test Cases› subsubsection ‹Propositional logic› lemma "True" nitpick [expect = none] apply auto done lemma "False" nitpick [expect = genuine] oops lemma "P" nitpick [expect = genuine] oops lemma "¬ P" nitpick [expect = genuine] oops lemma "P ∧ Q" nitpick [expect = genuine] oops lemma "P ∨ Q" nitpick [expect = genuine] oops lemma "P ⟶ Q" nitpick [expect = genuine] oops lemma "(P::bool) = Q" nitpick [expect = genuine] oops lemma "(P ∨ Q) ⟶ (P ∧ Q)" nitpick [expect = genuine] oops subsubsection ‹Predicate logic› lemma "P x y z" nitpick [expect = genuine] oops lemma "P x y ⟶ P y x" nitpick [expect = genuine] oops lemma "P (f (f x)) ⟶ P x ⟶ P (f x)" nitpick [expect = genuine] oops subsubsection ‹Equality› lemma "P = True" nitpick [expect = genuine] oops lemma "P = False" nitpick [expect = genuine] oops lemma "x = y" nitpick [expect = genuine] oops lemma "f x = g x" nitpick [expect = genuine] oops lemma "(f::'a⇒'b) = g" nitpick [expect = genuine] oops lemma "(f::('d⇒'d)⇒('c⇒'d)) = g" nitpick [expect = genuine] oops lemma "distinct [a, b]" nitpick [expect = genuine] apply simp nitpick [expect = genuine] oops subsubsection ‹First-Order Logic› lemma "∃x. P x" nitpick [expect = genuine] oops lemma "∀x. P x" nitpick [expect = genuine] oops lemma "∃!x. P x" nitpick [expect = genuine] oops lemma "Ex P" nitpick [expect = genuine] oops lemma "All P" nitpick [expect = genuine] oops lemma "Ex1 P" nitpick [expect = genuine] oops lemma "(∃x. P x) ⟶ (∀x. P x)" nitpick [expect = genuine] oops lemma "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)" nitpick [expect = genuine] oops lemma "(∃x. P x) ⟶ (∃!x. P x)" nitpick [expect = genuine] oops text ‹A true statement (also testing names of free and bound variables being identical)› lemma "(∀x y. P x y ⟶ P y x) ⟶ (∀x. P x y) ⟶ P y x" nitpick [expect = none] apply fast done text ‹"A type has at most 4 elements."› lemma "¬ distinct [a, b, c, d, e]" nitpick [expect = genuine] apply simp nitpick [expect = genuine] oops lemma "distinct [a, b, c, d]" nitpick [expect = genuine] apply simp nitpick [expect = genuine] oops text ‹"Every reflexive and symmetric relation is transitive."› lemma "⟦∀x. P x x; ∀x y. P x y ⟶ P y x⟧ ⟹ P x y ⟶ P y z ⟶ P x z" nitpick [expect = genuine] oops text ‹The ``Drinker's theorem''› lemma "∃x. f x = g x ⟶ f = g" nitpick [expect = none] apply (auto simp add: ext) done text ‹And an incorrect version of it› lemma "(∃x. f x = g x) ⟶ f = g" nitpick [expect = genuine] oops text ‹"Every function has a fixed point."› lemma "∃x. f x = x" nitpick [expect = genuine] oops text ‹"Function composition is commutative."› lemma "f (g x) = g (f x)" nitpick [expect = genuine] oops text ‹"Two functions that are equivalent wrt.\ the same predicate 'P' are equal."› lemma "((P::('a⇒'b)⇒bool) f = P g) ⟶ (f x = g x)" nitpick [expect = genuine] oops subsubsection ‹Higher-Order Logic› lemma "∃P. P" nitpick [expect = none] apply auto done lemma "∀P. P" nitpick [expect = genuine] oops lemma "∃!P. P" nitpick [expect = none] apply auto done lemma "∃!P. P x" nitpick [expect = genuine] oops lemma "P Q ∨ Q x" nitpick [expect = genuine] oops lemma "x ≠ All" nitpick [expect = genuine] oops lemma "x ≠ Ex" nitpick [expect = genuine] oops lemma "x ≠ Ex1" nitpick [expect = genuine] oops text ‹``The transitive closure of an arbitrary relation is non-empty.''› definition "trans" :: "('a ⇒ 'a ⇒ bool) ⇒ bool" where "trans P ≡ (∀x y z. P x y ⟶ P y z ⟶ P x z)" definition "subset" :: "('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool" where "subset P Q ≡ (∀x y. P x y ⟶ Q x y)" definition "trans_closure" :: "('a ⇒ 'a ⇒ bool) ⇒ ('a ⇒ 'a ⇒ bool) ⇒ bool" where "trans_closure P Q ≡ (subset Q P) ∧ (trans P) ∧ (∀R. subset Q R ⟶ trans R ⟶ subset P R)" lemma "trans_closure T P ⟶ (∃x y. T x y)" nitpick [expect = genuine] oops text ‹``The union of transitive closures is equal to the transitive closure of unions.''› lemma "(∀x y. (P x y ∨ R x y) ⟶ T x y) ⟶ trans T ⟶ (∀Q. (∀x y. (P x y ∨ R x y) ⟶ Q x y) ⟶ trans Q ⟶ subset T Q) ⟶ trans_closure TP P ⟶ trans_closure TR R ⟶ (T x y = (TP x y ∨ TR x y))" nitpick [expect = genuine] oops text ‹``Every surjective function is invertible.''› lemma "(∀y. ∃x. y = f x) ⟶ (∃g. ∀x. g (f x) = x)" nitpick [expect = genuine] oops text ‹``Every invertible function is surjective.''› lemma "(∃g. ∀x. g (f x) = x) ⟶ (∀y. ∃x. y = f x)" nitpick [expect = genuine] oops text ‹``Every point is a fixed point of some function.''› lemma "∃f. f x = x" nitpick [card = 1-7, expect = none] apply (rule_tac x = "λx. x" in exI) apply simp done text ‹Axiom of Choice: first an incorrect version› lemma "(∀x. ∃y. P x y) ⟶ (∃!f. ∀x. P x (f x))" nitpick [expect = genuine] oops text ‹And now two correct ones› lemma "(∀x. ∃y. P x y) ⟶ (∃f. ∀x. P x (f x))" nitpick [card = 1-4, expect = none] apply (simp add: choice) done lemma "(∀x. ∃!y. P x y) ⟶ (∃!f. ∀x. P x (f x))" nitpick [card = 1-3, expect = none] apply auto apply (simp add: ex1_implies_ex choice) apply (fast intro: ext) done subsubsection ‹Metalogic› lemma "⋀x. P x" nitpick [expect = genuine] oops lemma "f x ≡ g x" nitpick [expect = genuine] oops lemma "P ⟹ Q" nitpick [expect = genuine] oops lemma "⟦P; Q; R⟧ ⟹ S" nitpick [expect = genuine] oops lemma "(x ≡ Pure.all) ⟹ False" nitpick [expect = genuine] oops lemma "(x ≡ (≡)) ⟹ False" nitpick [expect = genuine] oops lemma "(x ≡ (⟹)) ⟹ False" nitpick [expect = genuine] oops subsubsection ‹Schematic Variables› schematic_goal "?P" nitpick [expect = none] apply auto done schematic_goal "x = ?y" nitpick [expect = none] apply auto done subsubsection ‹Abstractions› lemma "(λx. x) = (λx. y)" nitpick [expect = genuine] oops lemma "(λf. f x) = (λf. True)" nitpick [expect = genuine] oops lemma "(λx. x) = (λy. y)" nitpick [expect = none] apply simp done subsubsection ‹Sets› lemma "P (A::'a set)" nitpick [expect = genuine] oops lemma "P (A::'a set set)" nitpick [expect = genuine] oops lemma "{x. P x} = {y. P y}" nitpick [expect = none] apply simp done lemma "x ∈ {x. P x}" nitpick [expect = genuine] oops lemma "P (∈)" nitpick [expect = genuine] oops lemma "P ((∈) x)" nitpick [expect = genuine] oops lemma "P Collect" nitpick [expect = genuine] oops lemma "A Un B = A Int B" nitpick [expect = genuine] oops lemma "(A Int B) Un C = (A Un C) Int B" nitpick [expect = genuine] oops lemma "Ball A P ⟶ Bex A P" nitpick [expect = genuine] oops subsubsection ‹\<^const>‹undefined›› lemma "undefined" nitpick [expect = genuine] oops lemma "P undefined" nitpick [expect = genuine] oops lemma "undefined x" nitpick [expect = genuine] oops lemma "undefined undefined" nitpick [expect = genuine] oops subsubsection ‹\<^const>‹The›› lemma "The P" nitpick [expect = genuine] oops lemma "P The" nitpick [expect = genuine] oops lemma "P (The P)" nitpick [expect = genuine] oops lemma "(THE x. x=y) = z" nitpick [expect = genuine] oops lemma "Ex P ⟶ P (The P)" nitpick [expect = genuine] oops subsubsection ‹\<^const>‹Eps›› lemma "Eps P" nitpick [expect = genuine] oops lemma "P Eps" nitpick [expect = genuine] oops lemma "P (Eps P)" nitpick [expect = genuine] oops lemma "(SOME x. x=y) = z" nitpick [expect = genuine] oops lemma "Ex P ⟶ P (Eps P)" nitpick [expect = none] apply (auto simp add: someI) done subsubsection ‹Operations on Natural Numbers› lemma "(x::nat) + y = 0" nitpick [expect = genuine] oops lemma "(x::nat) = x + x" nitpick [expect = genuine] oops lemma "(x::nat) - y + y = x" nitpick [expect = genuine] oops lemma "(x::nat) = x * x" nitpick [expect = genuine] oops lemma "(x::nat) < x + y" nitpick [card = 1, expect = genuine] oops text ‹×› lemma "P (x::'a×'b)" nitpick [expect = genuine] oops lemma "∀x::'a×'b. P x" nitpick [expect = genuine] oops lemma "P (x, y)" nitpick [expect = genuine] oops lemma "P (fst x)" nitpick [expect = genuine] oops lemma "P (snd x)" nitpick [expect = genuine] oops lemma "P Pair" nitpick [expect = genuine] oops lemma "P (case x of Pair a b ⇒ f a b)" nitpick [expect = genuine] oops subsubsection ‹Subtypes (typedef), typedecl› text ‹A completely unspecified non-empty subset of \<^typ>‹'a›:› definition "myTdef = insert (undefined::'a) (undefined::'a set)" typedef 'a myTdef = "myTdef :: 'a set" unfolding myTdef_def by auto lemma "(x::'a myTdef) = y" nitpick [expect = genuine] oops typedecl myTdecl definition "T_bij = {(f::'a⇒'a). ∀y. ∃!x. f x = y}" typedef 'a T_bij = "T_bij :: ('a ⇒ 'a) set" unfolding T_bij_def by auto lemma "P (f::(myTdecl myTdef) T_bij)" nitpick [expect = genuine] oops subsubsection ‹Inductive Datatypes› text ‹unit› lemma "P (x::unit)" nitpick [expect = genuine] oops lemma "∀x::unit. P x" nitpick [expect = genuine] oops lemma "P ()" nitpick [expect = genuine] oops lemma "P (case x of () ⇒ u)" nitpick [expect = genuine] oops text ‹option› lemma "P (x::'a option)" nitpick [expect = genuine] oops lemma "∀x::'a option. P x" nitpick [expect = genuine] oops lemma "P None" nitpick [expect = genuine] oops lemma "P (Some x)" nitpick [expect = genuine] oops lemma "P (case x of None ⇒ n | Some u ⇒ s u)" nitpick [expect = genuine] oops text ‹+› lemma "P (x::'a+'b)" nitpick [expect = genuine] oops lemma "∀x::'a+'b. P x" nitpick [expect = genuine] oops lemma "P (Inl x)" nitpick [expect = genuine] oops lemma "P (Inr x)" nitpick [expect = genuine] oops lemma "P Inl" nitpick [expect = genuine] oops lemma "P (case x of Inl a ⇒ l a | Inr b ⇒ r b)" nitpick [expect = genuine] oops text ‹Non-recursive datatypes› datatype T1 = A | B lemma "P (x::T1)" nitpick [expect = genuine] oops lemma "∀x::T1. P x" nitpick [expect = genuine] oops lemma "P A" nitpick [expect = genuine] oops lemma "P B" nitpick [expect = genuine] oops lemma "rec_T1 a b A = a" nitpick [expect = none] apply simp done lemma "rec_T1 a b B = b" nitpick [expect = none] apply simp done lemma "P (rec_T1 a b x)" nitpick [expect = genuine] oops lemma "P (case x of A ⇒ a | B ⇒ b)" nitpick [expect = genuine] oops