(* 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