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