src/HOL/ex/Refute_Examples.thy

 lemma "(f::('d\<Rightarrow>'d)\<Rightarrow>('c\<Rightarrow>'d)) = g"
   refute
 oops
 
 lemma "distinct [a,b]"
-  refute
+  (*refute*)
   apply simp
   refute
 oops
 
 (*****************************************************************************)

 (*****************************************************************************)
 
 subsubsection {* Sets *}
 
 lemma "P (A::'a set)"
-  refute
+ (* refute *)
 oops
 
 lemma "P (A::'a set set)"
-  refute
+ (* refute *)
 oops
 
 lemma "{x. P x} = {y. P y}"
-  refute
+ (* refute *)
   apply simp
 done
 
 lemma "x : {x. P x}"
-  refute
+ (* refute *)
 oops
 
 lemma "P op:"
-  refute
+ (* refute *)
 oops
 
 lemma "P (op: x)"
-  refute
+ (* refute *)
 oops
 
 lemma "P Collect"
-  refute
+ (* refute *)
 oops
 
 lemma "A Un B = A Int B"
-  refute
+ (* refute *)
 oops
 
 lemma "(A Int B) Un C = (A Un C) Int B"
-  refute
+ (* refute *)
 oops
 
 lemma "Ball A P \<longrightarrow> Bex A P"
-  refute
+ (* refute *)
 oops
 
 (*****************************************************************************)
 
 subsubsection {* undefined *}

 
 typedef (open) 'a myTdef = "myTdef :: 'a set"
   unfolding myTdef_def by auto
 
 lemma "(x::'a myTdef) = y"
-  refute
+ (* refute *)
 oops
 
 typedecl myTdecl
 
 definition "T_bij = {(f::'a\<Rightarrow>'a). \<forall>y. \<exists>!x. f x = y}"
 
 typedef (open) 'a T_bij = "T_bij :: ('a \<Rightarrow> 'a) set"
   unfolding T_bij_def by auto
 
 lemma "P (f::(myTdecl myTdef) T_bij)"
-  refute
+ (* refute *)
 oops
 
 (*****************************************************************************)
 
 subsubsection {* Inductive datatypes *}

 record ('a, 'b) point =
   xpos :: 'a
   ypos :: 'b
 
 lemma "(x::('a, 'b) point) = y"
-  refute
+ (* refute *)
 oops
 
 record ('a, 'b, 'c) extpoint = "('a, 'b) point" +
   ext :: 'c
 
 lemma "(x::('a, 'b, 'c) extpoint) = y"
-  refute
+ (* refute *)
 oops
 
 (*****************************************************************************)
 
 subsubsection {* Inductively defined sets *}

 inductive_set arbitrarySet :: "'a set"
 where
   "undefined : arbitrarySet"
 
 lemma "x : arbitrarySet"
-  refute
+ (* refute *)
 oops
 
 inductive_set evenCard :: "'a set set"
 where
   "{} : evenCard"
 | "\<lbrakk> S : evenCard; x \<notin> S; y \<notin> S; x \<noteq> y \<rbrakk> \<Longrightarrow> S \<union> {x, y} : evenCard"
 
 lemma "S : evenCard"
-  refute
+ (* refute *)
 oops
 
 inductive_set
   even :: "nat set"
   and odd  :: "nat set"

 (*****************************************************************************)
 
 subsubsection {* Examples involving special functions *}
 
 lemma "card x = 0"
-  refute
+ (* refute *)
 oops
 
 lemma "finite x"
-  refute  -- {* no finite countermodel exists *}
+ (* refute *) -- {* no finite countermodel exists *}
 oops
 
 lemma "(x::nat) + y = 0"
   refute
 oops

 lemma "xs @ ys = ys @ xs"
   refute
 oops
 
 lemma "f (lfp f) = lfp f"
-  refute
+ (* refute *)
 oops
 
 lemma "f (gfp f) = gfp f"
-  refute
+ (* refute *)
 oops
 
 lemma "lfp f = gfp f"
-  refute
+ (* refute *)
 oops
 
 (*****************************************************************************)
 
 subsubsection {* Type classes and overloading *}

 lemma "inverse b"
   refute
 oops
 
 lemma "P (inverse (S::'a set))"
-  refute
+ (* refute*)
 oops
 
 lemma "P (inverse (p::'a\<times>'b))"
   refute
 oops

 oops
 
 refute_params [satsolver="auto"]
 
 end
+