src/HOL/ex/Refute_Examples.thy

     -- {* here 'refute 3' would cause an exception, since we only have 2 subgoals *}
   refute [maxsize=5]           -- {* we can override parameters ... *}
   refute [satsolver="dpll"] 2  -- {* ... and specify a subgoal at the same time *}
 oops
 
-refute_params
+refute_params [satsolver="dpll"]
 
 section {* Examples and Test Cases *}
 
 subsection {* Propositional logic *}
 

 oops
 
 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=2]  (* [maxsize=5] works well with ZChaff *)
+  refute
   apply fast
 done
 
 text {* "A type has at most 3 elements." *}
 

 oops
 
 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 -- works well with ZChaff, but the internal solver is too slow *)
+  refute
 oops
 
 text {* The "Drinker's theorem" ... *}
 
 lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
-  refute [maxsize=4]  (* [maxsize=6] works well with ZChaff *)
+  refute
   apply (auto simp add: ext)
 done
 
 text {* ... and an incorrect version of it *}
 

 
 lemma "(\<forall>x y. (P x y | R x y) \<longrightarrow> T x y) \<longrightarrow> trans T \<longrightarrow> (\<forall>Q. (\<forall>x y. (P x y | R x y) \<longrightarrow> Q x y) \<longrightarrow> trans Q \<longrightarrow> subset T Q)
         \<longrightarrow> trans_closure TP P
         \<longrightarrow> trans_closure TR R
         \<longrightarrow> (T x y = (TP x y | TR x y))"
-  (* refute -- works well with ZChaff, but the internal solver is too slow *)
+  refute
 oops
 
 text {* "Every surjective function is invertible." *}
 
 lemma "(\<forall>y. \<exists>x. y = f x) \<longrightarrow> (\<exists>g. \<forall>x. g (f x) = x)"

 oops
 
 text {* Every point is a fixed point of some function. *}
 
 lemma "\<exists>f. f x = x"
-  refute [maxsize=4]
+  refute [maxsize=5]
   apply (rule_tac x="\<lambda>x. x" in exI)
   apply simp
 done
 
 text {* Axiom of Choice: first an incorrect version ... *}

 oops
 
 text {* ... and now two correct ones *}
 
 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
-  refute [maxsize=5]
+  refute
   apply (simp add: choice)
 done
 
 lemma "(\<forall>x. EX!y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
-  refute [maxsize=3]  (* [maxsize=4] works well with ZChaff *)
+  refute
   apply auto
     apply (simp add: ex1_implies_ex choice)
   apply (fast intro: ext)
 done
 

 lemma "P (A::'a set set)"
   refute
 oops
 
 lemma "{x. P x} = {y. P y}"
-  refute [maxsize=2]  (* [maxsize=8] works well with ZChaff *)
+  refute
   apply simp
 done
 
 lemma "x : {x. P x}"
   refute

 lemma "(THE x. x=y) = z"
   refute
 oops
 
 lemma "Ex P \<longrightarrow> P (The P)"
-  (* refute -- works well with ZChaff, but the internal solver is too slow *)
+  refute
 oops
 
 subsection {* Eps *}
 
 lemma "Eps P"

 lemma "(SOME x. x=y) = z"
   refute
 oops
 
 lemma "Ex P \<longrightarrow> P (Eps P)"
-  refute [maxsize=2]  (* [maxsize=3] works well with ZChaff *)
+  refute [maxsize=3]
   apply (auto simp add: someI)
 done
 
 subsection {* Inductive datatypes *}