(* Title: HOL/ex/Refute_Examples.thy Author: Tjark Weber Copyright 2003-2007 See HOL/Refute.thy for help. *) section ‹Examples for the 'refute' command› theory Refute_Examples imports "HOL-Library.Refute" begin refute_params [satsolver = "cdclite"] lemma "P ∧ Q" apply (rule conjI) refute [expect = genuine] 1 ― ‹refutes @{term "P"}› refute [expect = genuine] 2 ― ‹refutes @{term "Q"}› refute [expect = genuine] ― ‹equivalent to 'refute 1'› ― ‹here 'refute 3' would cause an exception, since we only have 2 subgoals› refute [maxsize = 5, expect = genuine] ― ‹we can override parameters ...› refute [satsolver = "cdclite", expect = genuine] 2 ― ‹... and specify a subgoal at the same time› oops (*****************************************************************************) subsection ‹Examples and Test Cases› subsubsection ‹Propositional logic› lemma "True" refute [expect = none] by auto lemma "False" refute [expect = genuine] oops lemma "P" refute [expect = genuine] oops lemma "~ P" refute [expect = genuine] oops lemma "P & Q" refute [expect = genuine] oops lemma "P | Q" refute [expect = genuine] oops lemma "P ⟶ Q" refute [expect = genuine] oops lemma "(P::bool) = Q" refute [expect = genuine] oops lemma "(P | Q) ⟶ (P & Q)" refute [expect = genuine] oops (*****************************************************************************) subsubsection ‹Predicate logic› lemma "P x y z" refute [expect = genuine] oops lemma "P x y ⟶ P y x" refute [expect = genuine] oops lemma "P (f (f x)) ⟶ P x ⟶ P (f x)" refute [expect = genuine] oops (*****************************************************************************) subsubsection ‹Equality› lemma "P = True" refute [expect = genuine] oops lemma "P = False" refute [expect = genuine] oops lemma "x = y" refute [expect = genuine] oops lemma "f x = g x" refute [expect = genuine] oops lemma "(f::'a⇒'b) = g" refute [expect = genuine] oops lemma "(f::('d⇒'d)⇒('c⇒'d)) = g" refute [expect = genuine] oops lemma "distinct [a, b]" (* refute *) apply simp refute [expect = genuine] oops (*****************************************************************************) subsubsection ‹First-Order Logic› lemma "∃x. P x" refute [expect = genuine] oops lemma "∀x. P x" refute [expect = genuine] oops lemma "∃!x. P x" refute [expect = genuine] oops lemma "Ex P" refute [expect = genuine] oops lemma "All P" refute [expect = genuine] oops lemma "Ex1 P" refute [expect = genuine] oops lemma "(∃x. P x) ⟶ (∀x. P x)" refute [expect = genuine] oops lemma "(∀x. ∃y. P x y) ⟶ (∃y. ∀x. P x y)" refute [expect = genuine] oops lemma "(∃x. P x) ⟶ (∃!x. P x)" refute [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" refute [maxsize = 4, expect = none] by fast text ‹"A type has at most 4 elements."› lemma "a=b | a=c | a=d | a=e | b=c | b=d | b=e | c=d | c=e | d=e" refute [expect = genuine] oops lemma "∀a b c d e. a=b | a=c | a=d | a=e | b=c | b=d | b=e | c=d | c=e | d=e" refute [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" refute [expect = genuine] oops text ‹The "Drinker's theorem" ...› lemma "∃x. f x = g x ⟶ f = g" refute [maxsize = 4, expect = none] by (auto simp add: ext) text ‹... and an incorrect version of it› lemma "(∃x. f x = g x) ⟶ f = g" refute [expect = genuine] oops text ‹"Every function has a fixed point."› lemma "∃x. f x = x" refute [expect = genuine] oops text ‹"Function composition is commutative."› lemma "f (g x) = g (f x)" refute [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)" refute [expect = genuine] oops (*****************************************************************************) subsubsection ‹Higher-Order Logic› lemma "∃P. P" refute [expect = none] by auto lemma "∀P. P" refute [expect = genuine] oops lemma "∃!P. P" refute [expect = none] by auto lemma "∃!P. P x" refute [expect = genuine] oops lemma "P Q | Q x" refute [expect = genuine] oops lemma "x ≠ All" refute [expect = genuine] oops lemma "x ≠ Ex" refute [expect = genuine] oops lemma "x ≠ Ex1" refute [expect = genuine] oops text ‹"The transitive closure 'T' of an arbitrary relation 'P' 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)" refute [expect = genuine] oops text ‹"Every surjective function is invertible."› lemma "(∀y. ∃x. y = f x) ⟶ (∃g. ∀x. g (f x) = x)" refute [expect = genuine] oops text ‹"Every invertible function is surjective."› lemma "(∃g. ∀x. g (f x) = x) ⟶ (∀y. ∃x. y = f x)" refute [expect = genuine] oops text ‹Every point is a fixed point of some function.› lemma "∃f. f x = x" refute [maxsize = 4, expect = none] apply (rule_tac x="λx. x" in exI) by simp text ‹Axiom of Choice: first an incorrect version ...› lemma "(∀x. ∃y. P x y) ⟶ (∃!f. ∀x. P x (f x))" refute [expect = genuine] oops text ‹... and now two correct ones› lemma "(∀x. ∃y. P x y) ⟶ (∃f. ∀x. P x (f x))" refute [maxsize = 4, expect = none] by (simp add: choice) lemma "(∀x. ∃!y. P x y) ⟶ (∃!f. ∀x. P x (f x))" refute [maxsize = 2, expect = none] apply auto apply (simp add: ex1_implies_ex choice) by (fast intro: ext) (*****************************************************************************) subsubsection ‹Meta-logic› lemma "!!x. P x" refute [expect = genuine] oops lemma "f x == g x" refute [expect = genuine] oops lemma "P ⟹ Q" refute [expect = genuine] oops lemma "⟦ P; Q; R ⟧ ⟹ S" refute [expect = genuine] oops lemma "(x == Pure.all) ⟹ False" refute [expect = genuine] oops lemma "(x == (==)) ⟹ False" refute [expect = genuine] oops lemma "(x == (⟹)) ⟹ False" refute [expect = genuine] oops (*****************************************************************************) subsubsection ‹Schematic variables› schematic_goal "?P" refute [expect = none] by auto schematic_goal "x = ?y" refute [expect = none] by auto (******************************************************************************) subsubsection ‹Abstractions› lemma "(λx. x) = (λx. y)" refute [expect = genuine] oops lemma "(λf. f x) = (λf. True)" refute [expect = genuine] oops lemma "(λx. x) = (λy. y)" refute by simp (*****************************************************************************) subsubsection ‹Sets› lemma "P (A::'a set)" refute oops lemma "P (A::'a set set)" refute oops lemma "{x. P x} = {y. P y}" refute by simp lemma "x ∈ {x. P x}" refute oops lemma "P (∈)" refute oops lemma "P ((∈) x)" refute oops lemma "P Collect" refute oops lemma "A ∪ B = A ∩ B" refute oops lemma "(A ∩ B) ∪ C = (A ∪ C) ∩ B" refute oops lemma "Ball A P ⟶ Bex A P" refute oops (*****************************************************************************) subsubsection ‹undefined› lemma "undefined" refute [expect = genuine] oops lemma "P undefined" refute [expect = genuine] oops lemma "undefined x" refute [expect = genuine] oops lemma "undefined undefined" refute [expect = genuine] oops (*****************************************************************************) subsubsection ‹The› lemma "The P" refute [expect = genuine] oops lemma "P The" refute [expect = genuine] oops lemma "P (The P)" refute [expect = genuine] oops lemma "(THE x. x=y) = z" refute [expect = genuine] oops lemma "Ex P ⟶ P (The P)" refute [expect = genuine] oops (*****************************************************************************) subsubsection ‹Eps› lemma "Eps P" refute [expect = genuine] oops lemma "P Eps" refute [expect = genuine] oops lemma "P (Eps P)" refute [expect = genuine] oops lemma "(SOME x. x=y) = z" refute [expect = genuine] oops lemma "Ex P ⟶ P (Eps P)" refute [maxsize = 3, expect = none] by (auto simp add: someI) (*****************************************************************************) 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" refute 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)" refute oops (*****************************************************************************) subsubsection ‹Inductive datatypes› text ‹unit› lemma "P (x::unit)" refute [expect = genuine] oops lemma "∀x::unit. P x" refute [expect = genuine] oops lemma "P ()" refute [expect = genuine] oops lemma "P (case x of () ⇒ u)" refute [expect = genuine] oops text ‹option› lemma "P (x::'a option)" refute [expect = genuine] oops lemma "∀x::'a option. P x" refute [expect = genuine] oops lemma "P None" refute [expect = genuine] oops lemma "P (Some x)" refute [expect = genuine] oops lemma "P (case x of None ⇒ n | Some u ⇒ s u)" refute [expect = genuine] oops text ‹*› lemma "P (x::'a*'b)" refute [expect = genuine] oops lemma "∀x::'a*'b. P x" refute [expect = genuine] oops lemma "P (x, y)" refute [expect = genuine] oops lemma "P (fst x)" refute [expect = genuine] oops lemma "P (snd x)" refute [expect = genuine] oops lemma "P Pair" refute [expect = genuine] oops lemma "P (case x of Pair a b ⇒ p a b)" refute [expect = genuine] oops text ‹+› lemma "P (x::'a+'b)" refute [expect = genuine] oops lemma "∀x::'a+'b. P x" refute [expect = genuine] oops lemma "P (Inl x)" refute [expect = genuine] oops lemma "P (Inr x)" refute [expect = genuine] oops lemma "P Inl" refute [expect = genuine] oops lemma "P (case x of Inl a ⇒ l a | Inr b ⇒ r b)" refute [expect = genuine] oops text ‹Non-recursive datatypes› datatype T1 = A | B lemma "P (x::T1)" refute [expect = genuine] oops lemma "∀x::T1. P x" refute [expect = genuine] oops lemma "P A" refute [expect = genuine] oops lemma "P B" refute [expect = genuine] oops lemma "rec_T1 a b A = a" refute [expect = none] by simp lemma "rec_T1 a b B = b" refute [expect = none] by simp lemma "P (rec_T1 a b x)" refute [expect = genuine] oops lemma "P (case x of A ⇒ a | B ⇒ b)" refute [expect = genuine] oops datatype 'a T2 = C T1 | D 'a lemma "P (x::'a T2)" refute [expect = genuine] oops lemma "∀x::'a T2. P x" refute [expect = genuine] oops lemma "P D" refute [expect = genuine] oops lemma "rec_T2 c d (C x) = c x" refute [maxsize = 4, expect = none] by simp lemma "rec_T2 c d (D x) = d x" refute [maxsize = 4, expect = none] by simp lemma "P (rec_T2 c d x)" refute [expect = genuine] oops lemma "P (case x of C u ⇒ c u | D v ⇒ d v)" refute [expect = genuine] oops datatype ('a,'b) T3 = E "'a ⇒ 'b" lemma "P (x::('a,'b) T3)" refute [expect = genuine] oops lemma "∀x::('a,'b) T3. P x" refute [expect = genuine] oops lemma "P E" refute [expect = genuine] oops lemma "rec_T3 e (E x) = e x" refute [maxsize = 2, expect = none] by simp lemma "P (rec_T3 e x)" refute [expect = genuine] oops lemma "P (case x of E f ⇒ e f)" refute [expect = genuine] oops text ‹Recursive datatypes› text ‹nat› lemma "P (x::nat)" refute [expect = potential] oops lemma "∀x::nat. P x" refute [expect = potential] oops lemma "P (Suc 0)" refute [expect = potential] oops lemma "P Suc" refute [maxsize = 3, expect = none] ― ‹@{term Suc} is a partial function (regardless of the size of the model), hence @{term "P Suc"} is undefined and no model will be found› oops lemma "rec_nat zero suc 0 = zero" refute [expect = none] by simp lemma "rec_nat zero suc (Suc x) = suc x (rec_nat zero suc x)" refute [maxsize = 2, expect = none] by simp lemma "P (rec_nat zero suc x)" refute [expect = potential] oops lemma "P (case x of 0 ⇒ zero | Suc n ⇒ suc n)" refute [expect = potential] oops text ‹'a list› lemma "P (xs::'a list)" refute [expect = potential] oops lemma "∀xs::'a list. P xs" refute [expect = potential] oops lemma "P [x, y]" refute [expect = potential] oops lemma "rec_list nil cons [] = nil" refute [maxsize = 3, expect = none] by simp lemma "rec_list nil cons (x#xs) = cons x xs (rec_list nil cons xs)" refute [maxsize = 2, expect = none] by simp lemma "P (rec_list nil cons xs)" refute [expect = potential] oops lemma "P (case x of Nil ⇒ nil | Cons a b ⇒ cons a b)" refute [expect = potential] oops lemma "(xs::'a list) = ys" refute [expect = potential] oops lemma "a # xs = b # xs" refute [expect = potential] oops datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList lemma "P (x::BitList)" refute [expect = potential] oops lemma "∀x::BitList. P x" refute [expect = potential] oops lemma "P (Bit0 (Bit1 BitListNil))" refute [expect = potential] oops lemma "rec_BitList nil bit0 bit1 BitListNil = nil" refute [maxsize = 4, expect = none] by simp lemma "rec_BitList nil bit0 bit1 (Bit0 xs) = bit0 xs (rec_BitList nil bit0 bit1 xs)" refute [maxsize = 2, expect = none] by simp lemma "rec_BitList nil bit0 bit1 (Bit1 xs) = bit1 xs (rec_BitList nil bit0 bit1 xs)" refute [maxsize = 2, expect = none] by simp lemma "P (rec_BitList nil bit0 bit1 x)" refute [expect = potential] oops (*****************************************************************************) subsubsection ‹Examples involving special functions› lemma "card x = 0" refute [expect = potential] oops lemma "finite x" refute ― ‹no finite countermodel exists› oops lemma "(x::nat) + y = 0" refute [expect = potential] oops lemma "(x::nat) = x + x" refute [expect = potential] oops lemma "(x::nat) - y + y = x" refute [expect = potential] oops lemma "(x::nat) = x * x" refute [expect = potential] oops lemma "(x::nat) < x + y" refute [expect = potential] oops lemma "xs @ [] = ys @ []" refute [expect = potential] oops lemma "xs @ ys = ys @ xs" refute [expect = potential] oops (*****************************************************************************) subsubsection ‹Type classes and overloading› text ‹A type class without axioms:› class classA lemma "P (x::'a::classA)" refute [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)" refute [expect = genuine] oops lemma "∃x y. (x::'a::classC) ≠ y" (* refute [expect = none] FIXME *) oops 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)" refute [expect = genuine] oops text ‹A type class with multiple superclasses:› class classE = classC + classD lemma "P (x::'a::classE)" refute [expect = genuine] oops text ‹OFCLASS:› lemma "OFCLASS('a::type, type_class)" refute [expect = none] by intro_classes lemma "OFCLASS('a::classC, type_class)" refute [expect = none] by intro_classes lemma "OFCLASS('a::type, classC_class)" refute [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" refute [expect = genuine] oops lemma "P (inverse (S::'a set))" refute [expect = genuine] oops lemma "P (inverse (p::'a×'b))" refute [expect = genuine] oops text ‹Structured proofs› lemma "x = y" proof cases assume "x = y" show ?thesis refute [expect = none] refute [no_assms, expect = genuine] refute [no_assms = false, expect = none] oops refute_params [satsolver = "auto"] end