# HG changeset patch
# User webertj
# Date 1078947371 -3600
# Node ID 5c4a1e96efd6c8015c7a5fa93c82193a38277e08
# Parent  8a8330bef1f88e8a1e48737c144aa5bc8d3347d1
Updated examples

diff -r 8a8330bef1f8 -r 5c4a1e96efd6 src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Wed Mar 10 20:31:47 2004 +0100
+++ b/src/HOL/ex/Refute_Examples.thy	Wed Mar 10 20:36:11 2004 +0100
@@ -12,7 +12,7 @@
 
 section {* 'refute': General usage *}
 
-lemma "P"
+lemma "P x"
   refute
 oops
 
@@ -21,12 +21,14 @@
   refute 1  -- {* refutes @{term "P"} *}
   refute 2  -- {* refutes @{term "Q"} *}
   refute    -- {* equivalent to 'refute 1' *}
-  -- {* here 'refute 3' would cause an exception, since we only have 2 subgoals *}
-  refute [maxsize=5]     -- {* we can override parameters \<dots> *}
-  refute [satformat="cnf"] 2  -- {* \<dots> and specify a subgoal at the same time *}
+    -- {* here 'refute 3' would cause an exception, since we only have 2 subgoals *}
+  refute [maxsize=5]           -- {* we can override parameters \<dots> *}
+  refute [satsolver="dpll"] 2  -- {* \<dots> and specify a subgoal at the same time *}
 oops
 
-section {* Examples / Test cases *}
+refute_params
+
+section {* Examples and Test Cases *}
 
 subsection {* Propositional logic *}
 
@@ -69,11 +71,7 @@
 
 subsection {* Predicate logic *}
 
-lemma "P x"
-  refute
-oops
-
-lemma "P a b c d"
+lemma "P x y z"
   refute
 oops
 
@@ -81,6 +79,10 @@
   refute
 oops
 
+lemma "P (f (f x)) \<longrightarrow> P x \<longrightarrow> P (f x)"
+  refute
+oops
+
 subsection {* Equality *}
 
 lemma "P = True"
@@ -153,12 +155,16 @@
 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=6]
+  refute [maxsize=5]
   apply fast
 done
 
 text {* "A type has at most 3 elements." *}
 
+lemma "a=b | a=c | a=d | b=c | b=d | c=d"
+  refute
+oops
+
 lemma "\<forall>a b c d. a=b | a=c | a=d | b=c | b=d | c=d"
   refute
 oops
@@ -172,7 +178,7 @@
 text {* The "Drinker's theorem" \<dots> *}
 
 lemma "\<exists>x. f x = g x \<longrightarrow> f = g"
-  refute
+  refute [maxsize=6]
   apply (auto simp add: ext)
 done
 
@@ -224,6 +230,18 @@
   refute
 oops
 
+lemma "P All"
+  refute
+oops
+
+lemma "P Ex"
+  refute
+oops
+
+lemma "P Ex1"
+  refute
+oops
+
 text {* "The transitive closure 'T' of an arbitrary relation 'P' is non-empty." *}
 
 constdefs
@@ -235,7 +253,6 @@
   "trans_closure P Q == (subset Q P) & (trans P) & (ALL R. subset Q R \<longrightarrow> trans R \<longrightarrow> subset P R)"
 
 lemma "trans_closure T P \<longrightarrow> (\<exists>x y. T x y)"
-  apply (unfold trans_closure_def subset_def trans_def)
   refute
 oops
 
@@ -245,7 +262,6 @@
         \<longrightarrow> trans_closure TP P
         \<longrightarrow> trans_closure TR R
         \<longrightarrow> (T x y = (TP x y | TR x y))"
-  apply (unfold trans_closure_def trans_def subset_def)
   refute
 oops
 
@@ -264,7 +280,7 @@
 text {* Every point is a fixed point of some function. *}
 
 lemma "\<exists>f. f x = x"
-  refute [maxsize=5]
+  refute [maxsize=4]
   apply (rule_tac x="\<lambda>x. x" in exI)
   apply simp
 done
@@ -278,12 +294,12 @@
 text {* \<dots> and now two correct ones *}
 
 lemma "(\<forall>x. \<exists>y. P x y) \<longrightarrow> (\<exists>f. \<forall>x. P x (f x))"
-  refute
+  refute [maxsize=5]
   apply (simp add: choice)
 done
 
 lemma "(\<forall>x. EX!y. P x y) \<longrightarrow> (EX!f. \<forall>x. P x (f x))"
-  refute [maxsize=5]
+  refute [maxsize=4]
   apply auto
     apply (simp add: ex1_implies_ex choice)
   apply (fast intro: ext)
@@ -353,22 +369,94 @@
   refute
 oops
 
+lemma "P op:"
+  refute
+oops
+
+lemma "P (op: x)"
+  refute
+oops
+
+lemma "P Collect"
+  refute
+oops
+
 lemma "A Un B = A Int B"
-  apply (unfold Un_def Int_def)
   refute
 oops
 
 lemma "(A Int B) Un C = (A Un C) Int B"
-  apply (unfold Un_def Int_def)
   refute
 oops
 
 lemma "Ball A P \<longrightarrow> Bex A P"
-  apply (unfold Ball_def Bex_def)
+  refute
+oops
+
+subsection {* arbitrary *}
+
+lemma "arbitrary"
+  refute
+oops
+
+lemma "P arbitrary"
+  refute
+oops
+
+lemma "arbitrary x"
+  refute
+oops
+
+lemma "arbitrary arbitrary"
+  refute
+oops
+
+subsection {* The *}
+
+lemma "The P"
+  refute
+oops
+
+lemma "P The"
   refute
 oops
 
-subsection {* (Inductive) Datatypes *}
+lemma "P (The P)"
+  refute
+oops
+
+lemma "(THE x. x=y) = z"
+  refute
+oops
+
+lemma "Ex P \<longrightarrow> P (The P)"
+  refute
+oops
+
+subsection {* Eps *}
+
+lemma "Eps P"
+  refute
+oops
+
+lemma "P Eps"
+  refute
+oops
+
+lemma "P (Eps P)"
+  refute
+oops
+
+lemma "(SOME x. x=y) = z"
+  refute
+oops
+
+lemma "Ex P \<longrightarrow> P (Eps P)"
+  refute [maxsize=3]
+  apply (auto simp add: someI)
+done
+
+subsection {* Inductive datatypes *}
 
 subsubsection {* unit *}
 
@@ -384,40 +472,71 @@
   refute
 oops
 
+subsubsection {* option *}
+
+lemma "P (x::'a option)"
+  refute
+oops
+
+lemma "\<forall>x::'a option. P x"
+  refute
+oops
+
+lemma "P (Some x)"
+  refute
+oops
+
 subsubsection {* * *}
 
 lemma "P (x::'a*'b)"
+  refute
 oops
 
 lemma "\<forall>x::'a*'b. P x"
+  refute
 oops
 
 lemma "P (x,y)"
+  refute
 oops
 
 lemma "P (fst x)"
+  refute
 oops
 
 lemma "P (snd x)"
+  refute
+oops
+
+lemma "P Pair"
+  refute
 oops
 
 subsubsection {* + *}
 
 lemma "P (x::'a+'b)"
+  refute
 oops
 
 lemma "\<forall>x::'a+'b. P x"
+  refute
 oops
 
 lemma "P (Inl x)"
+  refute
 oops
 
 lemma "P (Inr x)"
+  refute
+oops
+
+lemma "P Inl"
+  refute
 oops
 
 subsubsection {* Non-recursive datatypes *}
 
-datatype T1 = C1
+datatype T1 = A | B
 
 lemma "P (x::T1)"
   refute
@@ -427,36 +546,28 @@
   refute
 oops
 
-lemma "P C"
-oops
-
-datatype T2 = C2 T1
-
-lemma "P (x::T2)"
+lemma "P A"
   refute
 oops
 
-lemma "\<forall>x::T2. P x"
+datatype 'a T2 = C T1 | D 'a
+
+lemma "P (x::'a T2)"
   refute
 oops
 
-lemma "P (C2 C1)"
-oops
-
-lemma "P (C2 x)"
-oops
-
-datatype 'a T3 = C3 'a
-
-lemma "P (x::'a T3)"
+lemma "\<forall>x::'a T2. P x"
   refute
 oops
 
-lemma "\<forall>x::'a T3. P x"
+lemma "P D"
   refute
 oops
 
-lemma "P (C3 x)"
+datatype ('a,'b) T3 = E "'a \<Rightarrow> 'b"
+
+lemma "P E"
+  refute
 oops
 
 subsubsection {* Recursive datatypes *}
@@ -464,11 +575,9 @@
 datatype Nat = Zero | Suc Nat
 
 lemma "P (x::Nat)"
-  refute
 oops
 
 lemma "\<forall>x::Nat. P x"
-  refute
 oops
 
 lemma "P (Suc Zero)"
@@ -477,11 +586,9 @@
 datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
 
 lemma "P (x::'a BinTree)"
-  refute
 oops
 
 lemma "\<forall>x::'a BinTree. P x"
-  refute
 oops
 
 subsubsection {* Mutually recursive datatypes *}
@@ -490,19 +597,15 @@
      and 'a bexp = Equal "'a aexp" "'a aexp"
 
 lemma "P (x::'a aexp)"
-  refute
 oops
 
 lemma "\<forall>x::'a aexp. P x"
-  refute
 oops
 
 lemma "P (x::'a bexp)"
-  refute
 oops
 
 lemma "\<forall>x::'a bexp. P x"
-  refute
 oops
 
 lemma "P (ITE (Equal (Number x) (Number y)) (Number x) (Number y))"