Theory Refute_Examples
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
refute [expect = genuine] 2
refute [expect = genuine]
refute [maxsize = 5, expect = genuine]
refute [satsolver = "cdclite", expect = genuine] 2
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]"
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