Theory Refute_Examples

theory Refute_Examples
imports Refute
(*  Title:      HOL/ex/Refute_Examples.thy
    Author:     Tjark Weber
    Copyright   2003-2007

See HOL/Refute.thy for help.
*)

header {* Examples for the 'refute' command *}

theory Refute_Examples
imports "~~/src/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 "EX! 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) --> (EX! 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 "EX! P. P"
refute [expect = none]
by auto

lemma "EX! 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 == (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]
oops

text {* "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]
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) --> (EX!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. 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]
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 == (op ==)) ==> False"
refute [expect = genuine]
oops

lemma "(x == (op ==>)) ==> False"
refute [expect = genuine]
oops

(*****************************************************************************)

subsubsection {* Schematic variables *}

schematic_lemma "?P"
refute [expect = none]
by auto

schematic_lemma "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 op:"
refute
oops

lemma "P (op: x)"
refute
oops

lemma "P Collect"
refute
oops

lemma "A Un B = A Int B"
refute
oops

lemma "(A Int B) Un C = (A Un C) Int 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 {* 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]
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

datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"

lemma "P (x::'a BinTree)"
refute [expect = potential]
oops

lemma "∀x::'a BinTree. P x"
refute [expect = potential]
oops

lemma "P (Node (Leaf x) (Leaf y))"
refute [expect = potential]
oops

lemma "rec_BinTree 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 simp

lemma "rec_BinTree l n (Node x y) = n x y (rec_BinTree l n x) (rec_BinTree l n y)"
refute [maxsize = 1, expect = none]
by simp

lemma "P (rec_BinTree l n x)"
refute [expect = potential]
oops

lemma "P (case x of Leaf a => l a | Node a b => n a b)"
refute [expect = potential]
oops

text {* 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]
oops

lemma "∀x::'a aexp. P x"
refute [expect = potential]
oops

lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"
refute [expect = potential]
oops

lemma "P (x::'a bexp)"
refute [expect = potential]
oops

lemma "∀x::'a bexp. P x"
refute [expect = potential]
oops

lemma "rec_aexp_bexp_1 number ite equal (Number x) = number x"
refute [maxsize = 1, expect = none]
by simp

lemma "rec_aexp_bexp_1 number ite equal (ITE x y z) = ite x y z (rec_aexp_bexp_2 number ite equal x) (rec_aexp_bexp_1 number ite equal y) (rec_aexp_bexp_1 number ite equal z)"
refute [maxsize = 1, expect = none]
by simp

lemma "P (rec_aexp_bexp_1 number ite equal x)"
refute [expect = potential]
oops

lemma "P (case x of Number a => number a | ITE b a1 a2 => ite b a1 a2)"
refute [expect = potential]
oops

lemma "rec_aexp_bexp_2 number ite equal (Equal x y) = equal x y (rec_aexp_bexp_1 number ite equal x) (rec_aexp_bexp_1 number ite equal y)"
refute [maxsize = 1, expect = none]
by simp

lemma "P (rec_aexp_bexp_2 number ite equal x)"
refute [expect = potential]
oops

lemma "P (case x of Equal a1 a2 => equal a1 a2)"
refute [expect = potential]
oops

datatype X = A | B X | C Y
     and Y = D X | E Y | F

lemma "P (x::X)"
refute [expect = potential]
oops

lemma "P (y::Y)"
refute [expect = potential]
oops

lemma "P (B (B A))"
refute [expect = potential]
oops

lemma "P (B (C F))"
refute [expect = potential]
oops

lemma "P (C (D A))"
refute [expect = potential]
oops

lemma "P (C (E F))"
refute [expect = potential]
oops

lemma "P (D (B A))"
refute [expect = potential]
oops

lemma "P (D (C F))"
refute [expect = potential]
oops

lemma "P (E (D A))"
refute [expect = potential]
oops

lemma "P (E (E F))"
refute [expect = potential]
oops

lemma "P (C (D (C F)))"
refute [expect = potential]
oops

lemma "rec_X_Y_1 a b c d e f A = a"
refute [maxsize = 3, expect = none]
by simp

lemma "rec_X_Y_1 a b c d e f (B x) = b x (rec_X_Y_1 a b c d e f x)"
refute [maxsize = 1, expect = none]
by simp

lemma "rec_X_Y_1 a b c d e f (C y) = c y (rec_X_Y_2 a b c d e f y)"
refute [maxsize = 1, expect = none]
by simp

lemma "rec_X_Y_2 a b c d e f (D x) = d x (rec_X_Y_1 a b c d e f x)"
refute [maxsize = 1, expect = none]
by simp

lemma "rec_X_Y_2 a b c d e f (E y) = e y (rec_X_Y_2 a b c d e f y)"
refute [maxsize = 1, expect = none]
by simp

lemma "rec_X_Y_2 a b c d e f F = f"
refute [maxsize = 3, expect = none]
by simp

lemma "P (rec_X_Y_1 a b c d e f x)"
refute [expect = potential]
oops

lemma "P (rec_X_Y_2 a b c d e f y)"
refute [expect = potential]
oops

text {* 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]
oops

lemma "P (CX None)"
refute [expect = potential]
oops

lemma "P (CX (Some (CX None)))"
refute [expect = potential]
oops

lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (CX x) = cx x (rec_XOpt_2 cx dx n1 s1 n2 s2 x)"
refute [maxsize = 1, expect = none]
by simp

lemma "rec_XOpt_1 cx dx n1 s1 n2 s2 (DX x) = dx x (λb. rec_XOpt_3 cx dx n1 s1 n2 s2 (x b))"
refute [maxsize = 1, expect = none]
by simp

lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 None = n1"
refute [maxsize = 2, expect = none]
by simp

lemma "rec_XOpt_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
refute [maxsize = 1, expect = none]
by simp

lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 None = n2"
refute [maxsize = 2, expect = none]
by simp

lemma "rec_XOpt_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
refute [maxsize = 1, expect = none]
by simp

lemma "P (rec_XOpt_1 cx dx n1 s1 n2 s2 x)"
refute [expect = potential]
oops

lemma "P (rec_XOpt_2 cx dx n1 s1 n2 s2 x)"
refute [expect = potential]
oops

lemma "P (rec_XOpt_3 cx dx n1 s1 n2 s2 x)"
refute [expect = potential]
oops

datatype 'a YOpt = CY "('a => 'a YOpt) option"

lemma "P (x::'a YOpt)"
refute [expect = potential]
oops

lemma "P (CY None)"
refute [expect = potential]
oops

lemma "P (CY (Some (λa. CY None)))"
refute [expect = potential]
oops

lemma "rec_YOpt_1 cy n s (CY x) = cy x (rec_YOpt_2 cy n s x)"
refute [maxsize = 1, expect = none]
by simp

lemma "rec_YOpt_2 cy n s None = n"
refute [maxsize = 2, expect = none]
by simp

lemma "rec_YOpt_2 cy n s (Some x) = s x (λa. rec_YOpt_1 cy n s (x a))"
refute [maxsize = 1, expect = none]
by simp

lemma "P (rec_YOpt_1 cy n s x)"
refute [expect = potential]
oops

lemma "P (rec_YOpt_2 cy n s x)"
refute [expect = potential]
oops

datatype Trie = TR "Trie list"

lemma "P (x::Trie)"
refute [expect = potential]
oops

lemma "∀x::Trie. P x"
refute [expect = potential]
oops

lemma "P (TR [TR []])"
refute [expect = potential]
oops

lemma "rec_Trie_1 tr nil cons (TR x) = tr x (rec_Trie_2 tr nil cons x)"
refute [maxsize = 1, expect = none]
by simp

lemma "rec_Trie_2 tr nil cons [] = nil"
refute [maxsize = 3, expect = none]
by simp

lemma "rec_Trie_2 tr nil cons (x#xs) = cons x xs (rec_Trie_1 tr nil cons x) (rec_Trie_2 tr nil cons xs)"
refute [maxsize = 1, expect = none]
by simp

lemma "P (rec_Trie_1 tr nil cons x)"
refute [expect = potential]
oops

lemma "P (rec_Trie_2 tr nil cons x)"
refute [expect = potential]
oops

datatype InfTree = Leaf | Node "nat => InfTree"

lemma "P (x::InfTree)"
refute [expect = potential]
oops

lemma "∀x::InfTree. P x"
refute [expect = potential]
oops

lemma "P (Node (λn. Leaf))"
refute [expect = potential]
oops

lemma "rec_InfTree leaf node Leaf = leaf"
refute [maxsize = 2, expect = none]
by simp

lemma "rec_InfTree leaf node (Node x) = node x (λn. rec_InfTree leaf node (x n))"
refute [maxsize = 1, expect = none]
by simp

lemma "P (rec_InfTree leaf node x)"
refute [expect = potential]
oops

datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a => 'a lambda"

lemma "P (x::'a lambda)"
refute [expect = potential]
oops

lemma "∀x::'a lambda. P x"
refute [expect = potential]
oops

lemma "P (Lam (λa. Var a))"
refute [expect = potential]
oops

lemma "rec_lambda var app lam (Var x) = var x"
refute [maxsize = 1, expect = none]
by simp

lemma "rec_lambda var app lam (App x y) = app x y (rec_lambda var app lam x) (rec_lambda var app lam y)"
refute [maxsize = 1, expect = none]
by simp

lemma "rec_lambda var app lam (Lam x) = lam x (λa. rec_lambda var app lam (x a))"
refute [maxsize = 1, expect = none]
by simp

lemma "P (rec_lambda v a l x)"
refute [expect = potential]
oops

text {* 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]
oops

lemma "∀x::'c U. P x"
refute [expect = potential]
oops

lemma "P (E (C (λa. True)))"
refute [expect = potential]
oops

lemma "rec_U_1 e c d nil cons (E x) = e x (rec_U_2 e c d nil cons x)"
refute [maxsize = 1, expect = none]
by simp

lemma "rec_U_2 e c d nil cons (C x) = c x"
refute [maxsize = 1, expect = none]
by simp

lemma "rec_U_2 e c d nil cons (D x) = d x (rec_U_3 e c d nil cons x)"
refute [maxsize = 1, expect = none]
by simp

lemma "rec_U_3 e c d nil cons [] = nil"
refute [maxsize = 2, expect = none]
by simp

lemma "rec_U_3 e c d nil cons (x#xs) = cons x xs (rec_U_1 e c d nil cons x) (rec_U_3 e c d nil cons xs)"
refute [maxsize = 1, expect = none]
by simp

lemma "P (rec_U_1 e c d nil cons x)"
refute [expect = potential]
oops

lemma "P (rec_U_2 e c d nil cons x)"
refute [expect = potential]
oops

lemma "P (rec_U_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 :: 'b

lemma "(x::('a, 'b) point) = y"
refute
oops

record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
  ext :: 'c

lemma "(x::('a, 'b, 'c) extpoint) = y"
refute
oops

(*****************************************************************************)

subsubsection {* Inductively defined sets *}

inductive_set arbitrarySet :: "'a set"
where
  "undefined : arbitrarySet"

lemma "x : arbitrarySet"
refute
oops

inductive_set evenCard :: "'a set set"
where
  "{} : evenCard"
| "[| S : evenCard; x ∉ S; y ∉ S; x ≠ y |] ==> S ∪ {x, y} : evenCard"

lemma "S : evenCard"
refute
oops

inductive_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" *)
oops

consts 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"
refute
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

lemma "f (lfp f) = lfp f"
refute
oops

lemma "f (gfp f) = gfp f"
refute
oops

lemma "lfp f = gfp f"
refute
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"

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]
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