Theory Refute_Nits

(*  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

datatype 'a T2 = C T1 | D 'a

lemma "P (x::'a T2)"
nitpick [expect = genuine]
oops

lemma "∀x::'a T2. P x"
nitpick [expect = genuine]
oops

lemma "P D"
nitpick [expect = genuine]
oops

lemma "rec_T2 c d (C x) = c x"
nitpick [expect = none]
apply simp
done

lemma "rec_T2 c d (D x) = d x"
nitpick [expect = none]
apply simp
done

lemma "P (rec_T2 c d x)"
nitpick [expect = genuine]
oops

lemma "P (case x of C u ⇒ c u | D v ⇒ d v)"
nitpick [expect = genuine]
oops

datatype ('a, 'b) T3 = E "'a ⇒ 'b"

lemma "P (x::('a, 'b) T3)"
nitpick [expect = genuine]
oops

lemma "∀x::('a, 'b) T3. P x"
nitpick [expect = genuine]
oops

lemma "P E"
nitpick [expect = genuine]
oops

lemma "rec_T3 e (E x) = e x"
nitpick [card = 1-4, expect = none]
apply simp
done

lemma "P (rec_T3 e x)"
nitpick [expect = genuine]
oops

lemma "P (case x of E f ⇒ e f)"
nitpick [expect = genuine]
oops

text ‹Recursive datatypes›

text ‹nat›

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

lemma "∀x::nat. P x"
nitpick [expect = genuine]
oops

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

lemma "P Suc"
nitpick [card = 1-7, expect = none]
oops

lemma "rec_nat zero suc 0 = zero"
nitpick [expect = none]
apply simp
done

lemma "rec_nat zero suc (Suc x) = suc x (rec_nat zero suc x)"
nitpick [expect = none]
apply simp
done

lemma "P (rec_nat zero suc x)"
nitpick [expect = genuine]
oops

lemma "P (case x of 0 ⇒ zero | Suc n ⇒ suc n)"
nitpick [expect = genuine]
oops

text ‹'a list›

lemma "P (xs::'a list)"
nitpick [expect = genuine]
oops

lemma "∀xs::'a list. P xs"
nitpick [expect = genuine]
oops

lemma "P [x, y]"
nitpick [expect = genuine]
oops

lemma "rec_list nil cons [] = nil"
nitpick [card = 1-5, expect = none]
apply simp
done

lemma "rec_list nil cons (x#xs) = cons x xs (rec_list nil cons xs)"
nitpick [card = 1-5, expect = none]
apply simp
done

lemma "P (rec_list nil cons xs)"
nitpick [expect = genuine]
oops

lemma "P (case x of Nil ⇒ nil | Cons a b ⇒ cons a b)"
nitpick [expect = genuine]
oops

lemma "(xs::'a list) = ys"
nitpick [expect = genuine]
oops

lemma "a # xs = b # xs"
nitpick [expect = genuine]
oops

datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList

lemma "P (x::BitList)"
nitpick [expect = genuine]
oops

lemma "∀x::BitList. P x"
nitpick [expect = genuine]
oops

lemma "P (Bit0 (Bit1 BitListNil))"
nitpick [expect = genuine]
oops

lemma "rec_BitList nil bit0 bit1 BitListNil = nil"
nitpick [expect = none]
apply simp
done

lemma "rec_BitList nil bit0 bit1 (Bit0 xs) = bit0 xs (rec_BitList nil bit0 bit1 xs)"
nitpick [expect = none]
apply simp
done

lemma "rec_BitList nil bit0 bit1 (Bit1 xs) = bit1 xs (rec_BitList nil bit0 bit1 xs)"
nitpick [expect = none]
apply simp
done

lemma "P (rec_BitList nil bit0 bit1 x)"
nitpick [expect = genuine]
oops

datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"

lemma "P (x::'a BinTree)"
nitpick [expect = genuine]
oops

lemma "∀x::'a BinTree. P x"
nitpick [expect = genuine]
oops

lemma "P (Node (Leaf x) (Leaf y))"
nitpick [expect = genuine]
oops

lemma "rec_BinTree l n (Leaf x) = l x"
nitpick [expect = none]
apply simp
done

lemma "rec_BinTree l n (Node x y) = n x y (rec_BinTree l n x) (rec_BinTree l n y)"
nitpick [card = 1-5, expect = none]
apply simp
done

lemma "P (rec_BinTree l n x)"
nitpick [expect = genuine]
oops

lemma "P (case x of Leaf a ⇒ l a | Node a b ⇒ n a b)"
nitpick [expect = genuine]
oops

text ‹Mutually recursive datatypes›

datatype 'a aexp = Number 'a | ITE "'a bexp" "'a aexp" "'a aexp"
 and 'a bexp = Equal "'a aexp" "'a aexp"

lemma "P (x::'a aexp)"
nitpick [expect = genuine]
oops

lemma "∀x::'a aexp. P x"
nitpick [expect = genuine]
oops

lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"
nitpick [expect = genuine]
oops

lemma "P (x::'a bexp)"
nitpick [expect = genuine]
oops

lemma "∀x::'a bexp. P x"
nitpick [expect = genuine]
oops

lemma "rec_aexp number ite equal (Number x) = number x"
nitpick [card = 1-3, expect = none]
apply simp
done

lemma "rec_aexp number ite equal (ITE x y z) = ite x y z (rec_bexp number ite equal x) (rec_aexp number ite equal y) (rec_aexp number ite equal z)"
nitpick [card = 1-3, expect = none]
apply simp
done

lemma "P (rec_aexp number ite equal x)"
nitpick [expect = genuine]
oops

lemma "P (case x of Number a ⇒ number a | ITE b a1 a2 ⇒ ite b a1 a2)"
nitpick [expect = genuine]
oops

lemma "rec_bexp number ite equal (Equal x y) = equal x y (rec_aexp number ite equal x) (rec_aexp number ite equal y)"
nitpick [card = 1-3, expect = none]
apply simp
done

lemma "P (rec_bexp number ite equal x)"
nitpick [expect = genuine]
oops

lemma "P (case x of Equal a1 a2 ⇒ equal a1 a2)"
nitpick [expect = genuine]
oops

datatype X = A | B X | C Y and Y = D X | E Y | F

lemma "P (x::X)"
nitpick [expect = genuine]
oops

lemma "P (y::Y)"
nitpick [expect = genuine]
oops

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

lemma "P (B (C F))"
nitpick [expect = genuine]
oops

lemma "P (C (D A))"
nitpick [expect = genuine]
oops

lemma "P (C (E F))"
nitpick [expect = genuine]
oops

lemma "P (D (B A))"
nitpick [expect = genuine]
oops

lemma "P (D (C F))"
nitpick [expect = genuine]
oops

lemma "P (E (D A))"
nitpick [expect = genuine]
oops

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

lemma "P (C (D (C F)))"
nitpick [expect = genuine]
oops

lemma "rec_X a b c d e f A = a"
nitpick [card = 1-5, expect = none]
apply simp
done

lemma "rec_X a b c d e f (B x) = b x (rec_X a b c d e f x)"
nitpick [card = 1-5, expect = none]
apply simp
done

lemma "rec_X a b c d e f (C y) = c y (rec_Y a b c d e f y)"
nitpick [card = 1-5, expect = none]
apply simp
done

lemma "rec_Y a b c d e f (D x) = d x (rec_X a b c d e f x)"
nitpick [card = 1-5, expect = none]
apply simp
done

lemma "rec_Y a b c d e f (E y) = e y (rec_Y a b c d e f y)"
nitpick [card = 1-5, expect = none]
apply simp
done

lemma "rec_Y a b c d e f F = f"
nitpick [card = 1-5, expect = none]
apply simp
done

lemma "P (rec_X a b c d e f x)"
nitpick [expect = genuine]
oops

lemma "P (rec_Y a b c d e f y)"
nitpick [expect = genuine]
oops

text ‹Other datatype examples›

text ‹Indirect recursion is implemented via mutual recursion.›

datatype XOpt = CX "XOpt option" | DX "bool ⇒ XOpt option"

lemma "P (x::XOpt)"
nitpick [expect = genuine]
oops

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

lemma "P (CX (Some (CX None)))"
nitpick [expect = genuine]
oops

lemma "P (rec_X cx dx n1 s1 n2 s2 x)"
nitpick [expect = genuine]
oops

datatype 'a YOpt = CY "('a ⇒ 'a YOpt) option"

lemma "P (x::'a YOpt)"
nitpick [expect = genuine]
oops

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

lemma "P (CY (Some (λa. CY None)))"
nitpick [expect = genuine]
oops

datatype Trie = TR "Trie list"

lemma "P (x::Trie)"
nitpick [expect = genuine]
oops

lemma "∀x::Trie. P x"
nitpick [expect = genuine]
oops

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

datatype InfTree = Leaf | Node "nat ⇒ InfTree"

lemma "P (x::InfTree)"
nitpick [expect = genuine]
oops

lemma "∀x::InfTree. P x"
nitpick [expect = genuine]
oops

lemma "P (Node (λn. Leaf))"
nitpick [expect = genuine]
oops

lemma "rec_InfTree leaf node Leaf = leaf"
nitpick [card = 1-3, expect = none]
apply simp
done

lemma "rec_InfTree leaf node (Node g) = node ((λInfTree. (InfTree, rec_InfTree leaf node InfTree)) ∘ g)"
nitpick [card = 1-3, expect = none]
apply simp
done

lemma "P (rec_InfTree leaf node x)"
nitpick [expect = genuine]
oops

datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a ⇒ 'a lambda"

lemma "P (x::'a lambda)"
nitpick [expect = genuine]
oops

lemma "∀x::'a lambda. P x"
nitpick [expect = genuine]
oops

lemma "P (Lam (λa. Var a))"
nitpick [card = 1-5, expect = none]
nitpick [card 'a = 4, card "'a lambda" = 5, expect = genuine]
oops

lemma "rec_lambda var app lam (Var x) = var x"
nitpick [card = 1-3, expect = none]
apply simp
done

lemma "rec_lambda var app lam (App x y) = app x y (rec_lambda var app lam x) (rec_lambda var app lam y)"
nitpick [card = 1-3, expect = none]
apply simp
done

lemma "rec_lambda var app lam (Lam x) = lam ((λlambda. (lambda, rec_lambda var app lam lambda)) ∘ x)"
nitpick [card = 1-3, expect = none]
apply simp
done

lemma "P (rec_lambda v a l x)"
nitpick [expect = genuine]
oops

text ‹Taken from "Inductive datatypes in HOL", p. 8:›

datatype (dead 'a, 'b) T = C "'a ⇒ bool" | D "'b list"
datatype 'c U = E "('c, 'c U) T"

lemma "P (x::'c U)"
nitpick [expect = genuine]
oops

lemma "∀x::'c U. P x"
nitpick [expect = genuine]
oops

lemma "P (E (C (λa. True)))"
nitpick [expect = genuine]
oops

subsubsection ‹Records›

record ('a, 'b) point =
  xpos :: 'a
  ypos :: 'b

lemma "(x::('a, 'b) point) = y"
nitpick [expect = genuine]
oops

record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
  ext :: 'c

lemma "(x::('a, 'b, 'c) extpoint) = y"
nitpick [expect = genuine]
oops

subsubsection ‹Inductively Defined Sets›

inductive_set undefinedSet :: "'a set" where
"undefined ∈ undefinedSet"

lemma "x ∈ undefinedSet"
nitpick [expect = genuine]
oops

inductive_set evenCard :: "'a set set"
where
"{} ∈ evenCard" |
"⟦S ∈ evenCard; x ∉ S; y ∉ S; x ≠ y⟧ ⟹ S ∪ {x, y} ∈ evenCard"

lemma "S ∈ evenCard"
nitpick [expect = genuine]
oops

inductive_set
even :: "nat set"
and odd :: "nat set"
where
"0 ∈ even" |
"n ∈ even ⟹ Suc n ∈ odd" |
"n ∈ odd ⟹ Suc n ∈ even"

lemma "n ∈ odd"
nitpick [expect = genuine]
oops

consts f :: "'a ⇒ 'a"

inductive_set a_even :: "'a set" and a_odd :: "'a set" where
"undefined ∈ a_even" |
"x ∈ a_even ⟹ f x ∈ a_odd" |
"x ∈ a_odd ⟹ f x ∈ a_even"

lemma "x ∈ a_odd"
nitpick [expect = genuine]
oops

subsubsection ‹Examples Involving Special Functions›

lemma "card x = 0"
nitpick [expect = genuine]
oops

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

lemma "xs @ [] = ys @ []"
nitpick [expect = genuine]
oops

lemma "xs @ ys = ys @ xs"
nitpick [expect = genuine]
oops

lemma "f (lfp f) = lfp f"
nitpick [card = 2, expect = genuine]
oops

lemma "f (gfp f) = gfp f"
nitpick [card = 2, expect = genuine]
oops

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

subsubsection ‹Axiomatic Type Classes and Overloading›

text ‹A type class without axioms:›

class classA

lemma "P (x::'a::classA)"
nitpick [expect = genuine]
oops

text ‹An axiom with a type variable (denoting types which have at least two elements):›

class classC =
  assumes classC_ax: "∃x y. x ≠ y"

lemma "P (x::'a::classC)"
nitpick [expect = genuine]
oops

lemma "∃x y. (x::'a::classC) ≠ y"
nitpick [expect = none]
sorry

text ‹A type class for which a constant is defined:›

class classD =
  fixes classD_const :: "'a ⇒ 'a"
  assumes classD_ax: "classD_const (classD_const x) = classD_const x"

lemma "P (x::'a::classD)"
nitpick [expect = genuine]
oops

text ‹A type class with multiple superclasses:›

class classE = classC + classD

lemma "P (x::'a::classE)"
nitpick [expect = genuine]
oops

text ‹OFCLASS:›

lemma "OFCLASS('a::type, type_class)"
nitpick [expect = none]
apply intro_classes
done

lemma "OFCLASS('a::classC, type_class)"
nitpick [expect = none]
apply intro_classes
done

lemma "OFCLASS('a::type, classC_class)"
nitpick [expect = genuine]
oops

text ‹Overloading:›

consts inverse :: "'a ⇒ 'a"

overloading inverse_bool ≡ "inverse :: bool ⇒ bool"
begin
  definition "inverse (b::bool) ≡ ¬ b"
end

overloading inverse_set ≡ "inverse :: 'a set ⇒ 'a set"
begin
  definition "inverse (S::'a set) ≡ -S"
end

overloading inverse_pair ≡ "inverse :: 'a × 'b ⇒ 'a × 'b"
begin
  definition "inverse_pair p ≡ (inverse (fst p), inverse (snd p))"
end

lemma "inverse b"
nitpick [expect = genuine]
oops

lemma "P (inverse (S::'a set))"
nitpick [expect = genuine]
oops

lemma "P (inverse (p::'a×'b))"
nitpick [expect = genuine]
oops

end