Theory Refute_Examples

theory Refute_Examples
imports Refute
`(*  Title:      HOL/ex/Refute_Examples.thy    Author:     Tjark Weber    Copyright   2003-2007See HOL/Refute.thy for help.*)header {* Examples for the 'refute' command *}theory Refute_Examplesimports "~~/src/HOL/Library/Refute"beginrefute_params [satsolver = "dpll"]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 = "dpll", 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 autolemma "False"refute [expect = genuine]oopslemma "P"refute [expect = genuine]oopslemma "~ P"refute [expect = genuine]oopslemma "P & Q"refute [expect = genuine]oopslemma "P | Q"refute [expect = genuine]oopslemma "P --> Q"refute [expect = genuine]oopslemma "(P::bool) = Q"refute [expect = genuine]oopslemma "(P | Q) --> (P & Q)"refute [expect = genuine]oops(*****************************************************************************)subsubsection {* Predicate logic *}lemma "P x y z"refute [expect = genuine]oopslemma "P x y --> P y x"refute [expect = genuine]oopslemma "P (f (f x)) --> P x --> P (f x)"refute [expect = genuine]oops(*****************************************************************************)subsubsection {* Equality *}lemma "P = True"refute [expect = genuine]oopslemma "P = False"refute [expect = genuine]oopslemma "x = y"refute [expect = genuine]oopslemma "f x = g x"refute [expect = genuine]oopslemma "(f::'a=>'b) = g"refute [expect = genuine]oopslemma "(f::('d=>'d)=>('c=>'d)) = g"refute [expect = genuine]oopslemma "distinct [a, b]"(* refute *)apply simprefute [expect = genuine]oops(*****************************************************************************)subsubsection {* First-Order Logic *}lemma "∃x. P x"refute [expect = genuine]oopslemma "∀x. P x"refute [expect = genuine]oopslemma "EX! x. P x"refute [expect = genuine]oopslemma "Ex P"refute [expect = genuine]oopslemma "All P"refute [expect = genuine]oopslemma "Ex1 P"refute [expect = genuine]oopslemma "(∃x. P x) --> (∀x. P x)"refute [expect = genuine]oopslemma "(∀x. ∃y. P x y) --> (∃y. ∀x. P x y)"refute [expect = genuine]oopslemma "(∃x. P x) --> (EX! x. P x)"refute [expect = genuine]oopstext {* 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 fasttext {* "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]oopslemma "∀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]oopstext {* "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]oopstext {* 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]oopstext {* "Every function has a fixed point." *}lemma "∃x. f x = x"refute [expect = genuine]oopstext {* "Function composition is commutative." *}lemma "f (g x) = g (f x)"refute [expect = genuine]oopstext {* "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 autolemma "∀P. P"refute [expect = genuine]oopslemma "EX! P. P"refute [expect = none]by autolemma "EX! P. P x"refute [expect = genuine]oopslemma "P Q | Q x"refute [expect = genuine]oopslemma "x ≠ All"refute [expect = genuine]oopslemma "x ≠ Ex"refute [expect = genuine]oopslemma "x ≠ Ex1"refute [expect = genuine]oopstext {* "The transitive closure 'T' of an arbitrary relation 'P' is non-empty." *}definition "trans" :: "('a => 'a => bool) => bool" where  "trans P == (ALL 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 == (ALL 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) & (ALL R. subset Q R --> trans R --> subset P R)"lemma "trans_closure T P --> (∃x y. T x y)"refute [expect = genuine]oopstext {* "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))"refute [expect = genuine]oopstext {* "Every surjective function is invertible." *}lemma "(∀y. ∃x. y = f x) --> (∃g. ∀x. g (f x) = x)"refute [expect = genuine]oopstext {* "Every invertible function is surjective." *}lemma "(∃g. ∀x. g (f x) = x) --> (∀y. ∃x. y = f x)"refute [expect = genuine]oopstext {* 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 simptext {* Axiom of Choice: first an incorrect version ... *}lemma "(∀x. ∃y. P x y) --> (EX!f. ∀x. P x (f x))"refute [expect = genuine]oopstext {* ... 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. EX!y. P x y) --> (EX!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]oopslemma "f x == g x"refute [expect = genuine]oopslemma "P ==> Q"refute [expect = genuine]oopslemma "[| P; Q; R |] ==> S"refute [expect = genuine]oopslemma "(x == all) ==> False"refute [expect = genuine]oopslemma "(x == (op ==)) ==> False"refute [expect = genuine]oopslemma "(x == (op ==>)) ==> False"refute [expect = genuine]oops(*****************************************************************************)subsubsection {* Schematic variables *}schematic_lemma "?P"refute [expect = none]by autoschematic_lemma "x = ?y"refute [expect = none]by auto(******************************************************************************)subsubsection {* Abstractions *}lemma "(λx. x) = (λx. y)"refute [expect = genuine]oopslemma "(λf. f x) = (λf. True)"refute [expect = genuine]oopslemma "(λx. x) = (λy. y)"refuteby simp(*****************************************************************************)subsubsection {* Sets *}lemma "P (A::'a set)"refuteoopslemma "P (A::'a set set)"refuteoopslemma "{x. P x} = {y. P y}"refuteby simplemma "x : {x. P x}"refuteoopslemma "P op:"refuteoopslemma "P (op: x)"refuteoopslemma "P Collect"refuteoopslemma "A Un B = A Int B"refuteoopslemma "(A Int B) Un C = (A Un C) Int B"refuteoopslemma "Ball A P --> Bex A P"refuteoops(*****************************************************************************)subsubsection {* undefined *}lemma "undefined"refute [expect = genuine]oopslemma "P undefined"refute [expect = genuine]oopslemma "undefined x"refute [expect = genuine]oopslemma "undefined undefined"refute [expect = genuine]oops(*****************************************************************************)subsubsection {* The *}lemma "The P"refute [expect = genuine]oopslemma "P The"refute [expect = genuine]oopslemma "P (The P)"refute [expect = genuine]oopslemma "(THE x. x=y) = z"refute [expect = genuine]oopslemma "Ex P --> P (The P)"refute [expect = genuine]oops(*****************************************************************************)subsubsection {* Eps *}lemma "Eps P"refute [expect = genuine]oopslemma "P Eps"refute [expect = genuine]oopslemma "P (Eps P)"refute [expect = genuine]oopslemma "(SOME x. x=y) = z"refute [expect = genuine]oopslemma "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 autolemma "(x::'a myTdef) = y"refuteoopstypedecl myTdecldefinition "T_bij = {(f::'a=>'a). ∀y. ∃!x. f x = y}"typedef 'a T_bij = "T_bij :: ('a => 'a) set"  unfolding T_bij_def by autolemma "P (f::(myTdecl myTdef) T_bij)"refuteoops(*****************************************************************************)subsubsection {* Inductive datatypes *}text {* With @{text quick_and_dirty} set, the datatype package does  not generate certain axioms for recursion operators.  Without these  axioms, Refute may find spurious countermodels. *}text {* unit *}lemma "P (x::unit)"refute [expect = genuine]oopslemma "∀x::unit. P x"refute [expect = genuine]oopslemma "P ()"refute [expect = genuine]oopslemma "unit_rec u x = u"refute [expect = none]by simplemma "P (unit_rec u x)"refute [expect = genuine]oopslemma "P (case x of () => u)"refute [expect = genuine]oopstext {* option *}lemma "P (x::'a option)"refute [expect = genuine]oopslemma "∀x::'a option. P x"refute [expect = genuine]oopslemma "P None"refute [expect = genuine]oopslemma "P (Some x)"refute [expect = genuine]oopslemma "option_rec n s None = n"refute [expect = none]by simplemma "option_rec n s (Some x) = s x"refute [maxsize = 4, expect = none]by simplemma "P (option_rec n s x)"refute [expect = genuine]oopslemma "P (case x of None => n | Some u => s u)"refute [expect = genuine]oopstext {* * *}lemma "P (x::'a*'b)"refute [expect = genuine]oopslemma "∀x::'a*'b. P x"refute [expect = genuine]oopslemma "P (x, y)"refute [expect = genuine]oopslemma "P (fst x)"refute [expect = genuine]oopslemma "P (snd x)"refute [expect = genuine]oopslemma "P Pair"refute [expect = genuine]oopslemma "prod_rec p (a, b) = p a b"refute [maxsize = 2, expect = none]by simplemma "P (prod_rec p x)"refute [expect = genuine]oopslemma "P (case x of Pair a b => p a b)"refute [expect = genuine]oopstext {* + *}lemma "P (x::'a+'b)"refute [expect = genuine]oopslemma "∀x::'a+'b. P x"refute [expect = genuine]oopslemma "P (Inl x)"refute [expect = genuine]oopslemma "P (Inr x)"refute [expect = genuine]oopslemma "P Inl"refute [expect = genuine]oopslemma "sum_rec l r (Inl x) = l x"refute [maxsize = 3, expect = none]by simplemma "sum_rec l r (Inr x) = r x"refute [maxsize = 3, expect = none]by simplemma "P (sum_rec l r x)"refute [expect = genuine]oopslemma "P (case x of Inl a => l a | Inr b => r b)"refute [expect = genuine]oopstext {* Non-recursive datatypes *}datatype T1 = A | Blemma "P (x::T1)"refute [expect = genuine]oopslemma "∀x::T1. P x"refute [expect = genuine]oopslemma "P A"refute [expect = genuine]oopslemma "P B"refute [expect = genuine]oopslemma "T1_rec a b A = a"refute [expect = none]by simplemma "T1_rec a b B = b"refute [expect = none]by simplemma "P (T1_rec a b x)"refute [expect = genuine]oopslemma "P (case x of A => a | B => b)"refute [expect = genuine]oopsdatatype 'a T2 = C T1 | D 'alemma "P (x::'a T2)"refute [expect = genuine]oopslemma "∀x::'a T2. P x"refute [expect = genuine]oopslemma "P D"refute [expect = genuine]oopslemma "T2_rec c d (C x) = c x"refute [maxsize = 4, expect = none]by simplemma "T2_rec c d (D x) = d x"refute [maxsize = 4, expect = none]by simplemma "P (T2_rec c d x)"refute [expect = genuine]oopslemma "P (case x of C u => c u | D v => d v)"refute [expect = genuine]oopsdatatype ('a,'b) T3 = E "'a => 'b"lemma "P (x::('a,'b) T3)"refute [expect = genuine]oopslemma "∀x::('a,'b) T3. P x"refute [expect = genuine]oopslemma "P E"refute [expect = genuine]oopslemma "T3_rec e (E x) = e x"refute [maxsize = 2, expect = none]by simplemma "P (T3_rec e x)"refute [expect = genuine]oopslemma "P (case x of E f => e f)"refute [expect = genuine]oopstext {* Recursive datatypes *}text {* nat *}lemma "P (x::nat)"refute [expect = potential]oopslemma "∀x::nat. P x"refute [expect = potential]oopslemma "P (Suc 0)"refute [expect = potential]oopslemma "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 *}oopslemma "nat_rec zero suc 0 = zero"refute [expect = none]by simplemma "nat_rec zero suc (Suc x) = suc x (nat_rec zero suc x)"refute [maxsize = 2, expect = none]by simplemma "P (nat_rec zero suc x)"refute [expect = potential]oopslemma "P (case x of 0 => zero | Suc n => suc n)"refute [expect = potential]oopstext {* 'a list *}lemma "P (xs::'a list)"refute [expect = potential]oopslemma "∀xs::'a list. P xs"refute [expect = potential]oopslemma "P [x, y]"refute [expect = potential]oopslemma "list_rec nil cons [] = nil"refute [maxsize = 3, expect = none]by simplemma "list_rec nil cons (x#xs) = cons x xs (list_rec nil cons xs)"refute [maxsize = 2, expect = none]by simplemma "P (list_rec nil cons xs)"refute [expect = potential]oopslemma "P (case x of Nil => nil | Cons a b => cons a b)"refute [expect = potential]oopslemma "(xs::'a list) = ys"refute [expect = potential]oopslemma "a # xs = b # xs"refute [expect = potential]oopsdatatype BitList = BitListNil | Bit0 BitList | Bit1 BitListlemma "P (x::BitList)"refute [expect = potential]oopslemma "∀x::BitList. P x"refute [expect = potential]oopslemma "P (Bit0 (Bit1 BitListNil))"refute [expect = potential]oopslemma "BitList_rec nil bit0 bit1 BitListNil = nil"refute [maxsize = 4, expect = none]by simplemma "BitList_rec nil bit0 bit1 (Bit0 xs) = bit0 xs (BitList_rec nil bit0 bit1 xs)"refute [maxsize = 2, expect = none]by simplemma "BitList_rec nil bit0 bit1 (Bit1 xs) = bit1 xs (BitList_rec nil bit0 bit1 xs)"refute [maxsize = 2, expect = none]by simplemma "P (BitList_rec nil bit0 bit1 x)"refute [expect = potential]oopsdatatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"lemma "P (x::'a BinTree)"refute [expect = potential]oopslemma "∀x::'a BinTree. P x"refute [expect = potential]oopslemma "P (Node (Leaf x) (Leaf y))"refute [expect = potential]oopslemma "BinTree_rec l n (Leaf x) = l x"  refute [maxsize = 1, expect = none]  (* The "maxsize = 1" tests are a bit pointless: for some formulae     below, refute will find no countermodel simply because this     size makes involved terms undefined.  Unfortunately, any     larger size already takes too long. *)by simplemma "BinTree_rec l n (Node x y) = n x y (BinTree_rec l n x) (BinTree_rec l n y)"refute [maxsize = 1, expect = none]by simplemma "P (BinTree_rec l n x)"refute [expect = potential]oopslemma "P (case x of Leaf a => l a | Node a b => n a b)"refute [expect = potential]oopstext {* 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)"refute [expect = potential]oopslemma "∀x::'a aexp. P x"refute [expect = potential]oopslemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"refute [expect = potential]oopslemma "P (x::'a bexp)"refute [expect = potential]oopslemma "∀x::'a bexp. P x"refute [expect = potential]oopslemma "aexp_bexp_rec_1 number ite equal (Number x) = number x"refute [maxsize = 1, expect = none]by simplemma "aexp_bexp_rec_1 number ite equal (ITE x y z) = ite x y z (aexp_bexp_rec_2 number ite equal x) (aexp_bexp_rec_1 number ite equal y) (aexp_bexp_rec_1 number ite equal z)"refute [maxsize = 1, expect = none]by simplemma "P (aexp_bexp_rec_1 number ite equal x)"refute [expect = potential]oopslemma "P (case x of Number a => number a | ITE b a1 a2 => ite b a1 a2)"refute [expect = potential]oopslemma "aexp_bexp_rec_2 number ite equal (Equal x y) = equal x y (aexp_bexp_rec_1 number ite equal x) (aexp_bexp_rec_1 number ite equal y)"refute [maxsize = 1, expect = none]by simplemma "P (aexp_bexp_rec_2 number ite equal x)"refute [expect = potential]oopslemma "P (case x of Equal a1 a2 => equal a1 a2)"refute [expect = potential]oopsdatatype X = A | B X | C Y     and Y = D X | E Y | Flemma "P (x::X)"refute [expect = potential]oopslemma "P (y::Y)"refute [expect = potential]oopslemma "P (B (B A))"refute [expect = potential]oopslemma "P (B (C F))"refute [expect = potential]oopslemma "P (C (D A))"refute [expect = potential]oopslemma "P (C (E F))"refute [expect = potential]oopslemma "P (D (B A))"refute [expect = potential]oopslemma "P (D (C F))"refute [expect = potential]oopslemma "P (E (D A))"refute [expect = potential]oopslemma "P (E (E F))"refute [expect = potential]oopslemma "P (C (D (C F)))"refute [expect = potential]oopslemma "X_Y_rec_1 a b c d e f A = a"refute [maxsize = 3, expect = none]by simplemma "X_Y_rec_1 a b c d e f (B x) = b x (X_Y_rec_1 a b c d e f x)"refute [maxsize = 1, expect = none]by simplemma "X_Y_rec_1 a b c d e f (C y) = c y (X_Y_rec_2 a b c d e f y)"refute [maxsize = 1, expect = none]by simplemma "X_Y_rec_2 a b c d e f (D x) = d x (X_Y_rec_1 a b c d e f x)"refute [maxsize = 1, expect = none]by simplemma "X_Y_rec_2 a b c d e f (E y) = e y (X_Y_rec_2 a b c d e f y)"refute [maxsize = 1, expect = none]by simplemma "X_Y_rec_2 a b c d e f F = f"refute [maxsize = 3, expect = none]by simplemma "P (X_Y_rec_1 a b c d e f x)"refute [expect = potential]oopslemma "P (X_Y_rec_2 a b c d e f y)"refute [expect = potential]oopstext {* Other datatype examples *}text {* Indirect recursion is implemented via mutual recursion. *}datatype XOpt = CX "XOpt option" | DX "bool => XOpt option"lemma "P (x::XOpt)"refute [expect = potential]oopslemma "P (CX None)"refute [expect = potential]oopslemma "P (CX (Some (CX None)))"refute [expect = potential]oopslemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (CX x) = cx x (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"refute [maxsize = 1, expect = none]by simplemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (DX x) = dx x (λb. XOpt_rec_3 cx dx n1 s1 n2 s2 (x b))"refute [maxsize = 1, expect = none]by simplemma "XOpt_rec_2 cx dx n1 s1 n2 s2 None = n1"refute [maxsize = 2, expect = none]by simplemma "XOpt_rec_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"refute [maxsize = 1, expect = none]by simplemma "XOpt_rec_3 cx dx n1 s1 n2 s2 None = n2"refute [maxsize = 2, expect = none]by simplemma "XOpt_rec_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"refute [maxsize = 1, expect = none]by simplemma "P (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"refute [expect = potential]oopslemma "P (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"refute [expect = potential]oopslemma "P (XOpt_rec_3 cx dx n1 s1 n2 s2 x)"refute [expect = potential]oopsdatatype 'a YOpt = CY "('a => 'a YOpt) option"lemma "P (x::'a YOpt)"refute [expect = potential]oopslemma "P (CY None)"refute [expect = potential]oopslemma "P (CY (Some (λa. CY None)))"refute [expect = potential]oopslemma "YOpt_rec_1 cy n s (CY x) = cy x (YOpt_rec_2 cy n s x)"refute [maxsize = 1, expect = none]by simplemma "YOpt_rec_2 cy n s None = n"refute [maxsize = 2, expect = none]by simplemma "YOpt_rec_2 cy n s (Some x) = s x (λa. YOpt_rec_1 cy n s (x a))"refute [maxsize = 1, expect = none]by simplemma "P (YOpt_rec_1 cy n s x)"refute [expect = potential]oopslemma "P (YOpt_rec_2 cy n s x)"refute [expect = potential]oopsdatatype Trie = TR "Trie list"lemma "P (x::Trie)"refute [expect = potential]oopslemma "∀x::Trie. P x"refute [expect = potential]oopslemma "P (TR [TR []])"refute [expect = potential]oopslemma "Trie_rec_1 tr nil cons (TR x) = tr x (Trie_rec_2 tr nil cons x)"refute [maxsize = 1, expect = none]by simplemma "Trie_rec_2 tr nil cons [] = nil"refute [maxsize = 3, expect = none]by simplemma "Trie_rec_2 tr nil cons (x#xs) = cons x xs (Trie_rec_1 tr nil cons x) (Trie_rec_2 tr nil cons xs)"refute [maxsize = 1, expect = none]by simplemma "P (Trie_rec_1 tr nil cons x)"refute [expect = potential]oopslemma "P (Trie_rec_2 tr nil cons x)"refute [expect = potential]oopsdatatype InfTree = Leaf | Node "nat => InfTree"lemma "P (x::InfTree)"refute [expect = potential]oopslemma "∀x::InfTree. P x"refute [expect = potential]oopslemma "P (Node (λn. Leaf))"refute [expect = potential]oopslemma "InfTree_rec leaf node Leaf = leaf"refute [maxsize = 2, expect = none]by simplemma "InfTree_rec leaf node (Node x) = node x (λn. InfTree_rec leaf node (x n))"refute [maxsize = 1, expect = none]by simplemma "P (InfTree_rec leaf node x)"refute [expect = potential]oopsdatatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a => 'a lambda"lemma "P (x::'a lambda)"refute [expect = potential]oopslemma "∀x::'a lambda. P x"refute [expect = potential]oopslemma "P (Lam (λa. Var a))"refute [expect = potential]oopslemma "lambda_rec var app lam (Var x) = var x"refute [maxsize = 1, expect = none]by simplemma "lambda_rec var app lam (App x y) = app x y (lambda_rec var app lam x) (lambda_rec var app lam y)"refute [maxsize = 1, expect = none]by simplemma "lambda_rec var app lam (Lam x) = lam x (λa. lambda_rec var app lam (x a))"refute [maxsize = 1, expect = none]by simplemma "P (lambda_rec v a l x)"refute [expect = potential]oopstext {* Taken from "Inductive datatypes in HOL", p.8: *}datatype ('a, 'b) T = C "'a => bool" | D "'b list"datatype 'c U = E "('c, 'c U) T"lemma "P (x::'c U)"refute [expect = potential]oopslemma "∀x::'c U. P x"refute [expect = potential]oopslemma "P (E (C (λa. True)))"refute [expect = potential]oopslemma "U_rec_1 e c d nil cons (E x) = e x (U_rec_2 e c d nil cons x)"refute [maxsize = 1, expect = none]by simplemma "U_rec_2 e c d nil cons (C x) = c x"refute [maxsize = 1, expect = none]by simplemma "U_rec_2 e c d nil cons (D x) = d x (U_rec_3 e c d nil cons x)"refute [maxsize = 1, expect = none]by simplemma "U_rec_3 e c d nil cons [] = nil"refute [maxsize = 2, expect = none]by simplemma "U_rec_3 e c d nil cons (x#xs) = cons x xs (U_rec_1 e c d nil cons x) (U_rec_3 e c d nil cons xs)"refute [maxsize = 1, expect = none]by simplemma "P (U_rec_1 e c d nil cons x)"refute [expect = potential]oopslemma "P (U_rec_2 e c d nil cons x)"refute [expect = potential]oopslemma "P (U_rec_3 e c d nil cons x)"refute [expect = potential]oops(*****************************************************************************)subsubsection {* Records *}(*TODO: make use of pair types, rather than typedef, for record types*)record ('a, 'b) point =  xpos :: 'a  ypos :: 'blemma "(x::('a, 'b) point) = y"refuteoopsrecord ('a, 'b, 'c) extpoint = "('a, 'b) point" +  ext :: 'clemma "(x::('a, 'b, 'c) extpoint) = y"refuteoops(*****************************************************************************)subsubsection {* Inductively defined sets *}inductive_set arbitrarySet :: "'a set"where  "undefined : arbitrarySet"lemma "x : arbitrarySet"refuteoopsinductive_set evenCard :: "'a set set"where  "{} : evenCard"| "[| S : evenCard; x ∉ S; y ∉ S; x ≠ y |] ==> S ∪ {x, y} : evenCard"lemma "S : evenCard"refuteoopsinductive_set  even :: "nat set"  and odd  :: "nat set"where  "0 : even"| "n : even ==> Suc n : odd"| "n : odd ==> Suc n : even"lemma "n : odd"(* refute *)  (* TODO: there seems to be an issue here with undefined terms                       because of the recursive datatype "nat" *)oopsconsts 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"(* refute [expect = genuine] -- {* finds a model of size 2 *}   NO LONGER WORKS since "lfp"'s interpreter is disabled *)oops(*****************************************************************************)subsubsection {* Examples involving special functions *}lemma "card x = 0"refuteoopslemma "finite x"refute -- {* no finite countermodel exists *}oopslemma "(x::nat) + y = 0"refute [expect = potential]oopslemma "(x::nat) = x + x"refute [expect = potential]oopslemma "(x::nat) - y + y = x"refute [expect = potential]oopslemma "(x::nat) = x * x"refute [expect = potential]oopslemma "(x::nat) < x + y"refute [expect = potential]oopslemma "xs @ [] = ys @ []"refute [expect = potential]oopslemma "xs @ ys = ys @ xs"refute [expect = potential]oopslemma "f (lfp f) = lfp f"refuteoopslemma "f (gfp f) = gfp f"refuteoopslemma "lfp f = gfp f"refuteoops(*****************************************************************************)subsubsection {* Type classes and overloading *}text {* A type class without axioms: *}class classAlemma "P (x::'a::classA)"refute [expect = genuine]oopstext {* 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]oopslemma "∃x y. (x::'a::classC) ≠ y"(* refute [expect = none] FIXME *)oopstext {* 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]oopstext {* A type class with multiple superclasses: *}class classE = classC + classDlemma "P (x::'a::classE)"refute [expect = genuine]oopstext {* OFCLASS: *}lemma "OFCLASS('a::type, type_class)"refute [expect = none]by intro_classeslemma "OFCLASS('a::classC, type_class)"refute [expect = none]by intro_classeslemma "OFCLASS('a::type, classC_class)"refute [expect = genuine]oopstext {* Overloading: *}consts inverse :: "'a => 'a"defs (overloaded)  inverse_bool: "inverse (b::bool)   == ~ b"  inverse_set : "inverse (S::'a set) == -S"  inverse_pair: "inverse p           == (inverse (fst p), inverse (snd p))"lemma "inverse b"refute [expect = genuine]oopslemma "P (inverse (S::'a set))"refute [expect = genuine]oopslemma "P (inverse (p::'a×'b))"refute [expect = genuine]oopstext {* 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]oopsrefute_params [satsolver = "auto"]end`