# HG changeset patch
# User webertj
# Date 1079000694 -3600
# Node ID e6550f190fe9698d167ec6d657da1c1a5d564a54
# Parent  fab539f843d996ab6b09829c045d807a7e69fb76
Refute_Examples added/fixed

diff -r fab539f843d9 -r e6550f190fe9 src/HOL/ex/ROOT.ML
--- a/src/HOL/ex/ROOT.ML	Thu Mar 11 03:53:43 2004 +0100
+++ b/src/HOL/ex/ROOT.ML	Thu Mar 11 11:24:54 2004 +0100
@@ -40,4 +40,4 @@
 time_use_thy "SVC_Oracle";
 if_svc_enabled time_use_thy "svc_test";
 
-time_use_thy "Refute_Examples.thy";
+time_use_thy "Refute_Examples";
diff -r fab539f843d9 -r e6550f190fe9 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Thu Mar 11 03:53:43 2004 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Thu Mar 11 11:24:54 2004 +0100
@@ -155,7 +155,7 @@
 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 [maxsize=5]
+  refute [maxsize=2]  (* [maxsize=5] works well with ZChaff *)
   apply fast
 done
 
@@ -172,13 +172,13 @@
 text {* "Every reflexive and symmetric relation is transitive." *}
 
 lemma "\<lbrakk> \<forall>x. P x x; \<forall>x y. P x y \<longrightarrow> P y x \<rbrakk> \<Longrightarrow> P x y \<longrightarrow> P y z \<longrightarrow> P x z"
-  refute
+  (* refute -- works well with ZChaff, but the internal solver is too slow *)
 oops
 
 text {* The "Drinker's theorem" \<dots> *}
 
 lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
-  refute [maxsize=6]
+  refute [maxsize=4]  (* [maxsize=6] works well with ZChaff *)
   apply (auto simp add: ext)
 done
 
@@ -262,7 +262,7 @@
         \<longrightarrow> trans_closure TP P
         \<longrightarrow> trans_closure TR R
         \<longrightarrow> (T x y = (TP x y | TR x y))"
-  refute
+  (* refute -- works well with ZChaff, but the internal solver is too slow *)
 oops
 
 text {* "Every surjective function is invertible." *}
@@ -299,7 +299,7 @@
 done
 
 lemma "(\<forall>x. EX!y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
-  refute [maxsize=4]
+  refute [maxsize=3]  (* [maxsize=4] works well with ZChaff *)
   apply auto
     apply (simp add: ex1_implies_ex choice)
   apply (fast intro: ext)
@@ -361,7 +361,7 @@
 oops
 
 lemma "{x. P x} = {y. P y}"
-  refute
+  refute [maxsize=2]  (* [maxsize=8] works well with ZChaff *)
   apply simp
 done
 
@@ -430,7 +430,7 @@
 oops
 
 lemma "Ex P \<longrightarrow> P (The P)"
-  refute
+  (* refute -- works well with ZChaff, but the internal solver is too slow *)
 oops
 
 subsection {* Eps *}
@@ -452,7 +452,7 @@
 oops
 
 lemma "Ex P \<longrightarrow> P (Eps P)"
-  refute [maxsize=3]
+  refute [maxsize=2]  (* [maxsize=3] works well with ZChaff *)
   apply (auto simp add: someI)
 done