(* 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
🍋‹P
››
refute [expect = genuine] 2
🍋 ‹refutes
🍋‹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
🍋‹'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]
🍋 ‹🍋‹Suc
› is a partial
function (regardless of the size
of the model),
hence 🍋‹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
