--- 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 *}