(* 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_JNI, 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)}^-1 = {(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 ≡ (op ≡) ⟹ 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 ≡ (op ⟹) ⟹ False" nitpick [expect = genuine] oops lemma "I ≡ (λx. x) ⟹ (op ⟹ x) ≡ (λy. (op ⟹ 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) ⟹ (op ∧) = (λx. op ∧ (I x))" "I = (λx. x) ⟹ (op ∧) = (λ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 "(op ⟶) = (λx. op⟶ x)" "(op⟶ ) = (λ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) ⟹ op ∈ = (λx. (op ∈ (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) ⟹ op ∪ = (λx. op ∪ (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) ⟹ op ∩ = (λx. op ∩ (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) ⟹ op ⊂ = (λx. op ⊂ (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