Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: csequence_codt.pvs Sprache: Isabelle

Original von: Isabelle^©

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

See HOL/Refute.thy for help.
*)

section \<open>Examples for the 'refute' command\<close>

theory Refute_Examples
imports "HOL-Library.Refute"
begin

refute_params [satsolver = "cdclite"]

lemma "P \ Q"
apply (rule conjI)
refute [expect = genuine] 1  \<comment> \<open>refutes \<^term>\<open>P\<close>\<close>
refute [expect = genuine] 2  \<comment> \<open>refutes \<^term>\<open>Q\<close>\<close>
refute [expect = genuine]    \<comment> \<open>equivalent to 'refute 1'\<close>
  \<comment> \<open>here 'refute 3' would cause an exception, since we only have 2 subgoals\<close>
refute [maxsize = 5, expect = genuine]   \<comment> \<open>we can override parameters ...\<close>
refute [satsolver = "cdclite", expect = genuine] 2
  \<comment> \<open>... and specify a subgoal at the same time\<close>
oops

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

subsection \<open>Examples and Test Cases\<close>

subsubsection \<open>Propositional logic\<close>

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 \<open>Predicate logic\<close>

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 \<open>Equality\<close>

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 \<open>First-Order Logic\<close>

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 \<open>A true statement (also testing names of free and bound variables being identical)\<close>

lemma "(\x y. P x y \ P y x) \ (\x. P x y) \ P y x"
refute [maxsize = 4, expect = none]
by fast

text \<open>"A type has at most 4 elements."\<close>

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 \<open>"Every reflexive and symmetric relation is transitive."\<close>

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 \<open>The "Drinker's theorem" ...\<close>

lemma "\x. f x = g x \ f = g"
refute [maxsize = 4, expect = none]
by (auto simp add: ext)

text \<open>... and an incorrect version of it\<close>

lemma "(\x. f x = g x) \ f = g"
refute [expect = genuine]
oops

text \<open>"Every function has a fixed point."\<close>

lemma "\x. f x = x"
refute [expect = genuine]
oops

text \<open>"Function composition is commutative."\<close>

lemma "f (g x) = g (f x)"
refute [expect = genuine]
oops

text \<open>"Two functions that are equivalent wrt.\ the same predicate 'P' are equal."\<close>

lemma "((P::('a\'b)\bool) f = P g) \ (f x = g x)"
refute [expect = genuine]
oops

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

subsubsection \<open>Higher-Order Logic\<close>

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 \<open>"The transitive closure 'T' of an arbitrary relation 'P' is non-empty."\<close>

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 \<open>"Every surjective function is invertible."\<close>

lemma "(\y. \x. y = f x) \ (\g. \x. g (f x) = x)"
refute [expect = genuine]
oops

text \<open>"Every invertible function is surjective."\<close>

lemma "(\g. \x. g (f x) = x) \ (\y. \x. y = f x)"
refute [expect = genuine]
oops

text \<open>Every point is a fixed point of some function.\<close>

lemma "\f. f x = x"
refute [maxsize = 4, expect = none]
apply (rule_tac x="\x. x" in exI)
by simp

text \<open>Axiom of Choice: first an incorrect version ...\<close>

lemma "(\x. \y. P x y) \ (\!f. \x. P x (f x))"
refute [expect = genuine]
oops

text \<open>... and now two correct ones\<close>

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 \<open>Meta-logic\<close>

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 \<open>Schematic variables\<close>

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

schematic_goal "x = ?y"
refute [expect = none]
by auto

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

subsubsection \<open>Abstractions\<close>

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 \<open>Sets\<close>

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 \<open>undefined\<close>

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 \<open>The\<close>

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 \<open>Eps\<close>

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 \<open>Subtypes (typedef), typedecl\<close>

text \<open>A completely unspecified non-empty subset of \<^typ>\<open>'a\<close>:\<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 \<Rightarrow> 'a) set"
  unfolding T_bij_def by auto

lemma "P (f::(myTdecl myTdef) T_bij)"
refute
oops

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

subsubsection \<open>Inductive datatypes\<close>

text \<open>unit\<close>

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 \<open>option\<close>

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 \<open>*\<close>

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 \<open>+\<close>

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 \<open>Non-recursive datatypes\<close>

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 \<open>Recursive datatypes\<close>

text \<open>nat\<close>

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]
\<comment> \<open>\<^term>\<open>Suc\<close> is a partial function (regardless of the size
      of the model), hence \<^term>\<open>P Suc\<close> is undefined and no
      model will be found\<close>
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 \<open>'a list\<close>

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 \<open>Examples involving special functions\<close>

lemma "card x = 0"
refute [expect = potential]
oops

lemma "finite x"
refute \<comment> \<open>no finite countermodel exists\<close>
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 \<open>Type classes and overloading\<close>

text \<open>A type class without axioms:\<close>

class classA

lemma "P (x::'a::classA)"
refute [expect = genuine]
oops

text \<open>An axiom with a type variable (denoting types which have at least two elements):\<close>

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 \<open>A type class for which a constant is defined:\<close>

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 \<open>A type class with multiple superclasses:\<close>

class classE = classC + classD

lemma "P (x::'a::classE)"
refute [expect = genuine]
oops

text \<open>OFCLASS:\<close>

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 \<open>Overloading:\<close>

consts inverse :: "'a \ 'a"

overloading inverse_bool \<equiv> "inverse :: bool \<Rightarrow> bool"
begin
  definition "inverse (b::bool) \ \ b"
end

overloading inverse_set \<equiv> "inverse :: 'a set \<Rightarrow> 'a set"
begin
  definition "inverse (S::'a set) \ -S"
end

overloading inverse_pair \<equiv> "inverse :: 'a \<times> 'b \<Rightarrow> 'a \<times> '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 \<open>Structured proofs\<close>

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

¤ Dauer der Verarbeitung: 0.26 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.