Theory Core_Nits

(*  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⇧*"
nitpick [card = 1-2, expect = none]
by auto

lemma "(a::'a×'a, a) ∈ Id⇧* ∪ {(a, b)}⇧*"
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