(* 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 split) f x y) = (λf x y. (λx. x) f x y)" nitpick [card = 1-12, expect = none] by auto lemma "(λf p. (split o curry) f p) = (λf p. (λx. x) f p)" nitpick [card = 1-12, expect = none] by auto lemma "split (curry f) = f" nitpick [card = 1-12, expect = none] by auto lemma "curry (split f) = f" nitpick [card = 1-12, expect = none] by auto lemma "split (λ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 = split" 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_lemma "x = ?x" nitpick [expect = none] by auto schematic_lemma "∀x. x = ?x" nitpick [expect = genuine] oops schematic_lemma "∃x. x = ?x" nitpick [expect = none] by auto schematic_lemma "∃x::'a => 'b. x = ?x" nitpick [expect = none] by auto schematic_lemma "∀x. ?x = ?y" nitpick [expect = none] by auto schematic_lemma "∃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