Quelle  Refute_Examples.thy

(*  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›:\<close>

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