--- a/src/HOL/ex/Refute_Examples.thy Wed May 26 18:06:38 2004 +0200
+++ b/src/HOL/ex/Refute_Examples.thy Wed May 26 18:23:46 2004 +0200
@@ -10,8 +10,6 @@
theory Refute_Examples = Main:
-section {* 'refute': General usage *}
-
lemma "P x"
refute
oops
@@ -26,8 +24,6 @@
refute [satsolver="dpll"] 2 -- {* ... and specify a subgoal at the same time *}
oops
-refute_params [satsolver="dpll"]
-
section {* Examples and Test Cases *}
subsection {* Propositional logic *}
@@ -110,6 +106,7 @@
oops
lemma "distinct [a,b]"
+ refute
apply simp
refute
oops
@@ -155,17 +152,17 @@
text {* A true statement (also testing names of free and bound variables being identical) *}
lemma "(\<forall>x y. P x y \<longrightarrow> P y x) \<longrightarrow> (\<forall>x. P x y) \<longrightarrow> P y x"
- refute
+ refute [maxsize=6]
apply fast
done
-text {* "A type has at most 3 elements." *}
+text {* "A type has at most 4 elements." *}
-lemma "a=b | a=c | a=d | b=c | b=d | c=d"
+lemma "a=b | a=c | a=d | a=e | b=c | b=d | b=e | c=d | c=e | d=e"
refute
oops
-lemma "\<forall>a b c d. a=b | a=c | a=d | b=c | b=d | c=d"
+lemma "\<forall>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
oops
@@ -178,7 +175,7 @@
text {* The "Drinker's theorem" ... *}
lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
- refute
+ refute [maxsize=4]
apply (auto simp add: ext)
done
@@ -262,7 +259,7 @@
\<longrightarrow> trans_closure TP P
\<longrightarrow> trans_closure TR R
\<longrightarrow> (T x y = (TP x y | TR x y))"
- refute
+ refute [satsolver="dpll"]
oops
text {* "Every surjective function is invertible." *}
@@ -280,7 +277,7 @@
text {* Every point is a fixed point of some function. *}
lemma "\<exists>f. f x = x"
- refute [maxsize=5]
+ refute [maxsize=4]
apply (rule_tac x="\<lambda>x. x" in exI)
apply simp
done
@@ -294,12 +291,12 @@
text {* ... and now two correct ones *}
lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
- refute
+ refute [maxsize=4]
apply (simp add: choice)
done
lemma "(\<forall>x. EX!y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
- refute
+ refute [maxsize=2, satsolver="dpll"]
apply auto
apply (simp add: ex1_implies_ex choice)
apply (fast intro: ext)
@@ -456,6 +453,25 @@
apply (auto simp add: someI)
done
+subsection {* Subtypes (typedef), typedecl *}
+
+typedef 'a myTdef = "insert (arbitrary::'a) (arbitrary::'a set)"
+ -- {* a completely unspecified non-empty subset of @{typ "'a"} *}
+ by auto
+
+lemma "(x::'a myTdef) = y"
+ refute [satsolver=dpll]
+oops
+
+typedecl myTdecl
+
+typedef 'a T_bij = "{(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
+ by auto
+
+lemma "P (f::(myTdecl myTdef) T_bij)"
+ refute
+oops
+
subsection {* Inductive datatypes *}
subsubsection {* unit *}
@@ -482,6 +498,10 @@
refute
oops
+lemma "P None"
+ refute
+oops
+
lemma "P (Some x)"
refute
oops
@@ -566,29 +586,50 @@
datatype ('a,'b) T3 = E "'a \<Rightarrow> 'b"
+lemma "P (x::('a,'b) T3)"
+ refute
+oops
+
+lemma "\<forall>x::('a,'b) T3. P x"
+ refute
+oops
+
lemma "P E"
refute
oops
subsubsection {* Recursive datatypes *}
-datatype Nat = Zero | Suc Nat
+lemma "P (x::nat)"
+ refute
+oops
-lemma "P (x::Nat)"
+lemma "\<forall>x::nat. P x"
+ refute
oops
-lemma "\<forall>x::Nat. P x"
+lemma "P (Suc 0)"
+ refute
oops
-lemma "P (Suc Zero)"
+lemma "P Suc"
+ refute -- {* @{term "Suc"} is a partial function (regardless of the size
+ of the model), hence @{term "P Suc"} is undefined, hence no
+ model will be found *}
oops
datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
lemma "P (x::'a BinTree)"
+ refute
oops
lemma "\<forall>x::'a BinTree. P x"
+ refute
+oops
+
+lemma "P (Node (Leaf x) (Leaf y))"
+ refute
oops
subsubsection {* Mutually recursive datatypes *}
@@ -597,30 +638,49 @@
and 'a bexp = Equal "'a aexp" "'a aexp"
lemma "P (x::'a aexp)"
+ refute
oops
lemma "\<forall>x::'a aexp. P x"
+ refute
oops
lemma "P (x::'a bexp)"
+ refute
oops
lemma "\<forall>x::'a bexp. P x"
+ refute
oops
lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"
+ refute
oops
subsubsection {* Other datatype examples *}
-datatype InfTree = Leaf | Node "Nat \<Rightarrow> InfTree"
+datatype InfTree = Leaf | Node "nat \<Rightarrow> InfTree"
lemma "P (x::InfTree)"
+ refute
oops
datatype 'a lambda = Var 'a | App "'a lambda" "'a lambda" | Lam "'a \<Rightarrow> 'a lambda"
-lemma "P (x::'a lambda)"
+lemma "P (x::'a lambda) | P (App x y)"
+ refute
+oops
+
+lemma "(xs::'a list) = ys"
+ refute
+oops
+
+lemma "a # xs = b # xs"
+ refute
+oops
+
+lemma "P [x, y]"
+ refute
oops
end