# HG changeset patch
# User bulwahn
# Date 1317027440 -7200
# Node ID 54c4e12bb5e032a4811ffcdf96b27e12670d61e7
# Parent  f00e52acbd42d1546aa4a48b39374e807428351e
adding an example with inductive predicates to quickcheck narrowing examples

diff -r f00e52acbd42 -r 54c4e12bb5e0 src/HOL/ex/Quickcheck_Narrowing_Examples.thy
--- a/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Mon Sep 26 10:30:37 2011 +0200
+++ b/src/HOL/ex/Quickcheck_Narrowing_Examples.thy	Mon Sep 26 10:57:20 2011 +0200
@@ -111,6 +111,19 @@
 oops
 *)
 
+subsection {* Simple examples with inductive predicates *}
+
+inductive even where
+  "even 0" |
+  "even n ==> even (Suc (Suc n))"
+
+code_pred even .
+
+lemma "even (n - 2) ==> even n"
+quickcheck[narrowing, expect = counterexample]
+oops
+
+
 subsection {* AVL Trees *}
 
 datatype 'a tree = ET |  MKT 'a "'a tree" "'a tree" nat