diff -r bf4f7571407f -r b711b0af178e src/HOL/ex/Refute_Examples.thy
--- a/src/HOL/ex/Refute_Examples.thy	Fri Oct 12 21:37:00 2007 +0200
+++ b/src/HOL/ex/Refute_Examples.thy	Fri Oct 12 22:00:47 2007 +0200
@@ -23,7 +23,7 @@
   refute [satsolver="dpll"] 2  -- {* ... and specify a subgoal at the same time *}
 oops
 
-(******************************************************************************)
+(*****************************************************************************)
 
 subsection {* Examples and Test Cases *}
 
@@ -66,7 +66,7 @@
   refute
 oops
 
-(******************************************************************************)
+(*****************************************************************************)
 
 subsubsection {* Predicate logic *}
 
@@ -82,7 +82,7 @@
   refute
 oops
 
-(******************************************************************************)
+(*****************************************************************************)
 
 subsubsection {* Equality *}
 
@@ -116,7 +116,7 @@
   refute
 oops
 
-(******************************************************************************)
+(*****************************************************************************)
 
 subsubsection {* First-Order Logic *}
 
@@ -210,7 +210,7 @@
   refute
 oops
 
-(******************************************************************************)
+(*****************************************************************************)
 
 subsubsection {* Higher-Order Logic *}
 
@@ -311,7 +311,7 @@
   apply (fast intro: ext)
 done
 
-(******************************************************************************)
+(*****************************************************************************)
 
 subsubsection {* Meta-logic *}
 
@@ -343,7 +343,7 @@
   refute
 oops
 
-(******************************************************************************)
+(*****************************************************************************)
 
 subsubsection {* Schematic variables *}
 
@@ -374,7 +374,7 @@
   apply simp
 done
 
-(******************************************************************************)
+(*****************************************************************************)
 
 subsubsection {* Sets *}
 
@@ -419,7 +419,7 @@
   refute
 oops
 
-(******************************************************************************)
+(*****************************************************************************)
 
 subsubsection {* arbitrary *}
 
@@ -439,7 +439,7 @@
   refute
 oops
 
-(******************************************************************************)
+(*****************************************************************************)
 
 subsubsection {* The *}
 
@@ -463,7 +463,7 @@
   refute
 oops
 
-(******************************************************************************)
+(*****************************************************************************)
 
 subsubsection {* Eps *}
 
@@ -488,7 +488,7 @@
   apply (auto simp add: someI)
 done
 
-(******************************************************************************)
+(*****************************************************************************)
 
 subsubsection {* Subtypes (typedef), typedecl *}
 
@@ -510,7 +510,7 @@
   refute
 oops
 
-(******************************************************************************)
+(*****************************************************************************)
 
 subsubsection {* Inductive datatypes *}
 
@@ -518,6 +518,8 @@
   not generate certain axioms for recursion operators.  Without these
   axioms, refute may find spurious countermodels. *}
 
+ML {* val Refute_Examples_qnd = !quick_and_dirty; reset quick_and_dirty; *}
+
 text {* unit *}
 
 lemma "P (x::unit)"
@@ -532,6 +534,11 @@
   refute
 oops
 
+lemma "unit_rec u x = u"
+  refute
+  apply simp
+done
+
 lemma "P (unit_rec u x)"
   refute
 oops
@@ -558,6 +565,16 @@
   refute
 oops
 
+lemma "option_rec n s None = n"
+  refute
+  apply simp
+done
+
+lemma "option_rec n s (Some x) = s x"
+  refute [maxsize=4]
+  apply simp
+done
+
 lemma "P (option_rec n s x)"
   refute
 oops
@@ -576,7 +593,7 @@
   refute
 oops
 
-lemma "P (x,y)"
+lemma "P (x, y)"
   refute
 oops
 
@@ -592,6 +609,11 @@
   refute
 oops
 
+lemma "prod_rec p (a, b) = p a b"
+  refute [maxsize=2]
+  apply simp
+oops
+
 lemma "P (prod_rec p x)"
   refute
 oops
@@ -622,6 +644,16 @@
   refute
 oops
 
+lemma "sum_rec l r (Inl x) = l x"
+  refute [maxsize=3]
+  apply simp
+done
+
+lemma "sum_rec l r (Inr x) = r x"
+  refute [maxsize=3]
+  apply simp
+done
+
 lemma "P (sum_rec l r x)"
   refute
 oops
@@ -646,6 +678,20 @@
   refute
 oops
 
+lemma "P B"
+  refute
+oops
+
+lemma "T1_rec a b A = a"
+  refute
+  apply simp
+done
+
+lemma "T1_rec a b B = b"
+  refute
+  apply simp
+done
+
 lemma "P (T1_rec a b x)"
   refute
 oops
@@ -668,6 +714,16 @@
   refute
 oops
 
+lemma "T2_rec c d (C x) = c x"
+  refute [maxsize=4]
+  apply simp
+done
+
+lemma "T2_rec c d (D x) = d x"
+  refute [maxsize=4]
+  apply simp
+done
+
 lemma "P (T2_rec c d x)"
   refute
 oops
@@ -690,6 +746,11 @@
   refute
 oops
 
+lemma "T3_rec e (E x) = e x"
+  refute [maxsize=2]
+  apply simp
+done
+
 lemma "P (T3_rec e x)"
   refute
 oops
@@ -720,6 +781,16 @@
                 model will be found *}
 oops
 
+lemma "nat_rec zero suc 0 = zero"
+  refute
+  apply simp
+done
+
+lemma "nat_rec zero suc (Suc x) = suc x (nat_rec zero suc x)"
+  refute [maxsize=2]
+  apply simp
+done
+
 lemma "P (nat_rec zero suc x)"
   refute
 oops
@@ -742,6 +813,16 @@
   refute
 oops
 
+lemma "list_rec nil cons [] = nil"
+  refute [maxsize=3]
+  apply simp
+done
+
+lemma "list_rec nil cons (x#xs) = cons x xs (list_rec nil cons xs)"
+  refute [maxsize=2]
+  apply simp
+done
+
 lemma "P (list_rec nil cons xs)"
   refute
 oops
@@ -758,6 +839,39 @@
   refute
 oops
 
+datatype BitList = BitListNil | Bit0 BitList | Bit1 BitList
+
+lemma "P (x::BitList)"
+  refute
+oops
+
+lemma "\<forall>x::BitList. P x"
+  refute
+oops
+
+lemma "P (Bit0 (Bit1 BitListNil))"
+  refute
+oops
+
+lemma "BitList_rec nil bit0 bit1 BitListNil = nil"
+  refute [maxsize=4]
+  apply simp
+done
+
+lemma "BitList_rec nil bit0 bit1 (Bit0 xs) = bit0 xs (BitList_rec nil bit0 bit1 xs)"
+  refute [maxsize=2]
+  apply simp
+done
+
+lemma "BitList_rec nil bit0 bit1 (Bit1 xs) = bit1 xs (BitList_rec nil bit0 bit1 xs)"
+  refute [maxsize=2]
+  apply simp
+done
+
+lemma "P (BitList_rec nil bit0 bit1 x)"
+  refute
+oops
+
 datatype 'a BinTree = Leaf 'a | Node "'a BinTree" "'a BinTree"
 
 lemma "P (x::'a BinTree)"
@@ -772,6 +886,19 @@
   refute
 oops
 
+lemma "BinTree_rec l n (Leaf x) = l x"
+  refute [maxsize=1]  (* The "maxsize=1" tests are a bit pointless: for some formulae
+                         below, refute will find no countermodel simply because this
+                         size makes involved terms undefined.  Unfortunately, any
+                         larger size already takes too long. *)
+  apply simp
+done
+
+lemma "BinTree_rec l n (Node x y) = n x y (BinTree_rec l n x) (BinTree_rec l n y)"
+  refute [maxsize=1]
+  apply simp
+done
+
 lemma "P (BinTree_rec l n x)"
   refute
 oops
@@ -805,6 +932,16 @@
   refute
 oops
 
+lemma "aexp_bexp_rec_1 number ite equal (Number x) = number x"
+  refute [maxsize=1]
+  apply simp
+done
+
+lemma "aexp_bexp_rec_1 number ite equal (ITE x y z) = ite x y z (aexp_bexp_rec_2 number ite equal x) (aexp_bexp_rec_1 number ite equal y) (aexp_bexp_rec_1 number ite equal z)"
+  refute [maxsize=1]
+  apply simp
+done
+
 lemma "P (aexp_bexp_rec_1 number ite equal x)"
   refute
 oops
@@ -813,6 +950,11 @@
   refute
 oops
 
+lemma "aexp_bexp_rec_2 number ite equal (Equal x y) = equal x y (aexp_bexp_rec_1 number ite equal x) (aexp_bexp_rec_1 number ite equal y)"
+  refute [maxsize=1]
+  apply simp
+done
+
 lemma "P (aexp_bexp_rec_2 number ite equal x)"
   refute
 oops
@@ -821,8 +963,188 @@
   refute
 oops
 
+datatype X = A | B X | C Y
+     and Y = D X | E Y | F
+
+lemma "P (x::X)"
+  refute
+oops
+
+lemma "P (y::Y)"
+  refute
+oops
+
+lemma "P (B (B A))"
+  refute
+oops
+
+lemma "P (B (C F))"
+  refute
+oops
+
+lemma "P (C (D A))"
+  refute
+oops
+
+lemma "P (C (E F))"
+  refute
+oops
+
+lemma "P (D (B A))"
+  refute
+oops
+
+lemma "P (D (C F))"
+  refute
+oops
+
+lemma "P (E (D A))"
+  refute
+oops
+
+lemma "P (E (E F))"
+  refute
+oops
+
+lemma "P (C (D (C F)))"
+  refute
+oops
+
+lemma "X_Y_rec_1 a b c d e f A = a"
+  refute [maxsize=3]
+  apply simp
+done
+
+lemma "X_Y_rec_1 a b c d e f (B x) = b x (X_Y_rec_1 a b c d e f x)"
+  refute [maxsize=1]
+  apply simp
+done
+
+lemma "X_Y_rec_1 a b c d e f (C y) = c y (X_Y_rec_2 a b c d e f y)"
+  refute [maxsize=1]
+  apply simp
+done
+
+lemma "X_Y_rec_2 a b c d e f (D x) = d x (X_Y_rec_1 a b c d e f x)"
+  refute [maxsize=1]
+  apply simp
+done
+
+lemma "X_Y_rec_2 a b c d e f (E y) = e y (X_Y_rec_2 a b c d e f y)"
+  refute [maxsize=1]
+  apply simp
+done
+
+lemma "X_Y_rec_2 a b c d e f F = f"
+  refute [maxsize=3]
+  apply simp
+done
+
+lemma "P (X_Y_rec_1 a b c d e f x)"
+  refute
+oops
+
+lemma "P (X_Y_rec_2 a b c d e f y)"
+  refute
+oops
+
 text {* Other datatype examples *}
 
+text {* Indirect recursion is implemented via mutual recursion. *}
+
+datatype XOpt = CX "XOpt option" | DX "bool \<Rightarrow> XOpt option"
+
+lemma "P (x::XOpt)"
+  refute
+oops
+
+lemma "P (CX None)"
+  refute
+oops
+
+lemma "P (CX (Some (CX None)))"
+  refute
+oops
+
+lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (CX x) = cx x (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
+  refute [maxsize=1]
+  apply simp
+done
+
+lemma "XOpt_rec_1 cx dx n1 s1 n2 s2 (DX x) = dx x (\<lambda>b. XOpt_rec_3 cx dx n1 s1 n2 s2 (x b))"
+  refute [maxsize=1]
+  apply simp
+done
+
+lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 None = n1"
+  refute [maxsize=2]
+  apply simp
+done
+
+lemma "XOpt_rec_2 cx dx n1 s1 n2 s2 (Some x) = s1 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
+  refute [maxsize=1]
+  apply simp
+done
+
+lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 None = n2"
+  refute [maxsize=2]
+  apply simp
+done
+
+lemma "XOpt_rec_3 cx dx n1 s1 n2 s2 (Some x) = s2 x (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
+  refute [maxsize=1]
+  apply simp
+done
+
+lemma "P (XOpt_rec_1 cx dx n1 s1 n2 s2 x)"
+  refute
+oops
+
+lemma "P (XOpt_rec_2 cx dx n1 s1 n2 s2 x)"
+  refute
+oops
+
+lemma "P (XOpt_rec_3 cx dx n1 s1 n2 s2 x)"
+  refute
+oops
+
+datatype 'a YOpt = CY "('a \<Rightarrow> 'a YOpt) option"
+
+lemma "P (x::'a YOpt)"
+  refute
+oops
+
+lemma "P (CY None)"
+  refute
+oops
+
+lemma "P (CY (Some (\<lambda>a. CY None)))"
+  refute
+oops
+
+lemma "YOpt_rec_1 cy n s (CY x) = cy x (YOpt_rec_2 cy n s x)"
+  refute [maxsize=1]
+  apply simp
+done
+
+lemma "YOpt_rec_2 cy n s None = n"
+  refute [maxsize=2]
+  apply simp
+done
+
+lemma "YOpt_rec_2 cy n s (Some x) = s x (\<lambda>a. YOpt_rec_1 cy n s (x a))"
+  refute [maxsize=1]
+  apply simp
+done
+
+lemma "P (YOpt_rec_1 cy n s x)"
+  refute
+oops
+
+lemma "P (YOpt_rec_2 cy n s x)"
+  refute
+oops
+
 datatype Trie = TR "Trie list"
 
 lemma "P (x::Trie)"
@@ -837,11 +1159,26 @@
   refute
 oops
 
-lemma "P (Trie_rec_1 a b c x)"
+lemma "Trie_rec_1 tr nil cons (TR x) = tr x (Trie_rec_2 tr nil cons x)"
+  refute [maxsize=1]
+  apply simp
+done
+
+lemma "Trie_rec_2 tr nil cons [] = nil"
+  refute [maxsize=3]
+  apply simp
+done
+
+lemma "Trie_rec_2 tr nil cons (x#xs) = cons x xs (Trie_rec_1 tr nil cons x) (Trie_rec_2 tr nil cons xs)"
+  refute [maxsize=1]
+  apply simp
+done
+
+lemma "P (Trie_rec_1 tr nil cons x)"
   refute
 oops
 
-lemma "P (Trie_rec_2 a b c x)"
+lemma "P (Trie_rec_2 tr nil cons x)"
   refute
 oops
 
@@ -859,6 +1196,16 @@
   refute
 oops
 
+lemma "InfTree_rec leaf node Leaf = leaf"
+  refute [maxsize=2]
+  apply simp
+done
+
+lemma "InfTree_rec leaf node (Node x) = node x (\<lambda>n. InfTree_rec leaf node (x n))"
+  refute [maxsize=1]
+  apply simp
+done
+
 lemma "P (InfTree_rec leaf node x)"
   refute
 oops
@@ -877,6 +1224,21 @@
   refute
 oops
 
+lemma "lambda_rec var app lam (Var x) = var x"
+  refute [maxsize=1]
+  apply simp
+done
+
+lemma "lambda_rec var app lam (App x y) = app x y (lambda_rec var app lam x) (lambda_rec var app lam y)"
+  refute [maxsize=1]
+  apply simp
+done
+
+lemma "lambda_rec var app lam (Lam x) = lam x (\<lambda>a. lambda_rec var app lam (x a))"
+  refute [maxsize=1]
+  apply simp
+done
+
 lemma "P (lambda_rec v a l x)"
   refute
 oops
@@ -898,19 +1260,46 @@
   refute
 oops
 
-lemma "P (U_rec_1 e f g h i x)"
+lemma "U_rec_1 e c d nil cons (E x) = e x (U_rec_2 e c d nil cons x)"
+  refute [maxsize=1]
+  apply simp
+done
+
+lemma "U_rec_2 e c d nil cons (C x) = c x"
+  refute [maxsize=1]
+  apply simp
+done
+
+lemma "U_rec_2 e c d nil cons (D x) = d x (U_rec_3 e c d nil cons x)"
+  refute [maxsize=1]
+  apply simp
+done
+
+lemma "U_rec_3 e c d nil cons [] = nil"
+  refute [maxsize=2]
+  apply simp
+done
+
+lemma "U_rec_3 e c d nil cons (x#xs) = cons x xs (U_rec_1 e c d nil cons x) (U_rec_3 e c d nil cons xs)"
+  refute [maxsize=1]
+  apply simp
+done
+
+lemma "P (U_rec_1 e c d nil cons x)"
   refute
 oops
 
-lemma "P (U_rec_2 e f g h i x)"
+lemma "P (U_rec_2 e c d nil cons x)"
   refute
 oops
 
-lemma "P (U_rec_3 e f g h i x)"
+lemma "P (U_rec_3 e c d nil cons x)"
   refute
 oops
 
-(******************************************************************************)
+ML {* quick_and_dirty := Refute_Examples_qnd; *}
+
+(*****************************************************************************)
 
 subsubsection {* Records *}
 
@@ -931,7 +1320,7 @@
   refute
 oops
 
-(******************************************************************************)
+(*****************************************************************************)
 
 subsubsection {* Inductively defined sets *}
 
@@ -961,10 +1350,25 @@
 | "n : odd \<Longrightarrow> Suc n : even"
 
 lemma "n : odd"
-  (*refute*)  -- {* unfortunately, this little example already takes too long *}
+  (*refute*)  (* TODO: there seems to be an issue here with undefined terms
+                       because of the recursive datatype "nat" *)
 oops
 
-(******************************************************************************)
+consts f :: "'a \<Rightarrow> 'a"
+
+inductive_set
+  a_even :: "'a set"
+  and a_odd :: "'a set"
+where
+  "arbitrary : a_even"
+| "x : a_even \<Longrightarrow> f x : a_odd"
+| "x : a_odd \<Longrightarrow> f x : a_even"
+
+lemma "x : a_odd"
+  refute  -- {* finds a model of size 2, as expected *}
+oops
+
+(*****************************************************************************)
 
 subsubsection {* Examples involving special functions *}
 
@@ -996,6 +1400,7 @@
   refute
 oops
 
+(* TODO: an efficient interpreter for @ is needed here
 lemma "xs @ [] = ys @ []"
   refute
 oops
@@ -1003,6 +1408,7 @@
 lemma "xs @ ys = ys @ xs"
   refute
 oops
+*)
 
 lemma "f (lfp f) = lfp f"
   refute
@@ -1016,7 +1422,7 @@
   refute
 oops
 
-(******************************************************************************)
+(*****************************************************************************)
 
 subsubsection {* Axiomatic type classes and overloading *}