src/HOL/ex/Refute_Examples.thy

--- a/src/HOL/ex/Refute_Examples.thy	Wed Jan 03 22:59:30 2007 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Thu Jan 04 00:12:30 2007 +0100
@@ -1,7 +1,7 @@
 (*  Title:      HOL/ex/Refute_Examples.thy
     ID:         $Id$
     Author:     Tjark Weber
-    Copyright   2003-2005
+    Copyright   2003-2007
 *)
 
 (* See 'HOL/Refute.thy' for help. *)
@@ -24,6 +24,8 @@
   refute [satsolver="dpll"] 2  -- {* ... and specify a subgoal at the same time *}
 oops
 
+(******************************************************************************)
+
 section {* Examples and Test Cases *}
 
 subsection {* Propositional logic *}
@@ -65,6 +67,8 @@
   refute
 oops
 
+(******************************************************************************)
+
 subsection {* Predicate logic *}
 
 lemma "P x y z"
@@ -79,6 +83,8 @@
   refute
 oops
 
+(******************************************************************************)
+
 subsection {* Equality *}
 
 lemma "P = True"
@@ -111,6 +117,8 @@
   refute
 oops
 
+(******************************************************************************)
+
 subsection {* First-Order Logic *}
 
 lemma "\<exists>x. P x"
@@ -203,6 +211,8 @@
   refute
 oops
 
+(******************************************************************************)
+
 subsection {* Higher-Order Logic *}
 
 lemma "\<exists>P. P"
@@ -227,15 +237,15 @@
   refute
 oops
 
-lemma "P All"
+lemma "x \<noteq> All"
   refute
 oops
 
-lemma "P Ex"
+lemma "x \<noteq> Ex"
   refute
 oops
 
-lemma "P Ex1"
+lemma "x \<noteq> Ex1"
   refute
 oops
 
@@ -302,6 +312,8 @@
   apply (fast intro: ext)
 done
 
+(******************************************************************************)
+
 subsection {* Meta-logic *}
 
 lemma "!!x. P x"
@@ -320,6 +332,20 @@
   refute
 oops
 
+lemma "(x == all) \<Longrightarrow> False"
+  refute
+oops
+
+lemma "(x == (op ==)) \<Longrightarrow> False"
+  refute
+oops
+
+lemma "(x == (op \<Longrightarrow>)) \<Longrightarrow> False"
+  refute
+oops
+
+(******************************************************************************)
+
 subsection {* Schematic variables *}
 
 lemma "?P"
@@ -332,6 +358,8 @@
   apply auto
 done
 
+(******************************************************************************)
+
 subsection {* Abstractions *}
 
 lemma "(\<lambda>x. x) = (\<lambda>x. y)"
@@ -347,6 +375,8 @@
   apply simp
 done
 
+(******************************************************************************)
+
 subsection {* Sets *}
 
 lemma "P (A::'a set)"
@@ -390,6 +420,8 @@
   refute
 oops
 
+(******************************************************************************)
+
 subsection {* arbitrary *}
 
 lemma "arbitrary"
@@ -408,6 +440,8 @@
   refute
 oops
 
+(******************************************************************************)
+
 subsection {* The *}
 
 lemma "The P"
@@ -430,6 +464,8 @@
   refute
 oops
 
+(******************************************************************************)
+
 subsection {* Eps *}
 
 lemma "Eps P"
@@ -968,11 +1004,11 @@
   refute
 oops
 
-lemma "a @ [] = b @ []"
+lemma "xs @ [] = ys @ []"
   refute
 oops
 
-lemma "a @ b = b @ a"
+lemma "xs @ ys = ys @ xs"
   refute
 oops
 
@@ -1000,7 +1036,7 @@
   refute
 oops
 
-text {* The axiom of this type class does not contain any type variables, but is internally converted into one that does: *}
+text {* The axiom of this type class does not contain any type variables: *}
 
 axclass classB
   classB_ax: "P | ~ P"