Refute_Examples added/fixed
authorwebertj
Thu Mar 11 11:24:54 2004 +0100 (2004-03-11)
changeset 14462e6550f190fe9
parent 14461 fab539f843d9
child 14463 ed09706ecc5d
Refute_Examples added/fixed
src/HOL/ex/ROOT.ML
src/HOL/ex/Refute_Examples.thy
     1.1 --- a/src/HOL/ex/ROOT.ML	Thu Mar 11 03:53:43 2004 +0100
     1.2 +++ b/src/HOL/ex/ROOT.ML	Thu Mar 11 11:24:54 2004 +0100
     1.3 @@ -40,4 +40,4 @@
     1.4  time_use_thy "SVC_Oracle";
     1.5  if_svc_enabled time_use_thy "svc_test";
     1.6  
     1.7 -time_use_thy "Refute_Examples.thy";
     1.8 +time_use_thy "Refute_Examples";
     2.1 --- a/src/HOL/ex/Refute_Examples.thy	Thu Mar 11 03:53:43 2004 +0100
     2.2 +++ b/src/HOL/ex/Refute_Examples.thy	Thu Mar 11 11:24:54 2004 +0100
     2.3 @@ -155,7 +155,7 @@
     2.4  text {* A true statement (also testing names of free and bound variables being identical) *}
     2.5  
     2.6  lemma "(\<forall>x y. P x y \<longrightarrow> P y x) \<longrightarrow> (\<forall>x. P x y) \<longrightarrow> P y x"
     2.7 -  refute [maxsize=5]
     2.8 +  refute [maxsize=2]  (* [maxsize=5] works well with ZChaff *)
     2.9    apply fast
    2.10  done
    2.11  
    2.12 @@ -172,13 +172,13 @@
    2.13  text {* "Every reflexive and symmetric relation is transitive." *}
    2.14  
    2.15  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"
    2.16 -  refute
    2.17 +  (* refute -- works well with ZChaff, but the internal solver is too slow *)
    2.18  oops
    2.19  
    2.20  text {* The "Drinker's theorem" \<dots> *}
    2.21  
    2.22  lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
    2.23 -  refute [maxsize=6]
    2.24 +  refute [maxsize=4]  (* [maxsize=6] works well with ZChaff *)
    2.25    apply (auto simp add: ext)
    2.26  done
    2.27  
    2.28 @@ -262,7 +262,7 @@
    2.29          \<longrightarrow> trans_closure TP P
    2.30          \<longrightarrow> trans_closure TR R
    2.31          \<longrightarrow> (T x y = (TP x y | TR x y))"
    2.32 -  refute
    2.33 +  (* refute -- works well with ZChaff, but the internal solver is too slow *)
    2.34  oops
    2.35  
    2.36  text {* "Every surjective function is invertible." *}
    2.37 @@ -299,7 +299,7 @@
    2.38  done
    2.39  
    2.40  lemma "(\<forall>x. EX!y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
    2.41 -  refute [maxsize=4]
    2.42 +  refute [maxsize=3]  (* [maxsize=4] works well with ZChaff *)
    2.43    apply auto
    2.44      apply (simp add: ex1_implies_ex choice)
    2.45    apply (fast intro: ext)
    2.46 @@ -361,7 +361,7 @@
    2.47  oops
    2.48  
    2.49  lemma "{x. P x} = {y. P y}"
    2.50 -  refute
    2.51 +  refute [maxsize=2]  (* [maxsize=8] works well with ZChaff *)
    2.52    apply simp
    2.53  done
    2.54  
    2.55 @@ -430,7 +430,7 @@
    2.56  oops
    2.57  
    2.58  lemma "Ex P \<longrightarrow> P (The P)"
    2.59 -  refute
    2.60 +  (* refute -- works well with ZChaff, but the internal solver is too slow *)
    2.61  oops
    2.62  
    2.63  subsection {* Eps *}
    2.64 @@ -452,7 +452,7 @@
    2.65  oops
    2.66  
    2.67  lemma "Ex P \<longrightarrow> P (Eps P)"
    2.68 -  refute [maxsize=3]
    2.69 +  refute [maxsize=2]  (* [maxsize=3] works well with ZChaff *)
    2.70    apply (auto simp add: someI)
    2.71  done
    2.72