# HG changeset patch
# User berghofe
# Date 1199989508 -3600
# Node ID 1bd12187a96e4f87038044b55ab2403ca76a858c
# Parent  0ba401ddbaed49eb82affaed6062de75bb7f2195
New example involving functions.

diff -r 0ba401ddbaed -r 1bd12187a96e src/HOL/ex/Quickcheck_Examples.thy
--- a/src/HOL/ex/Quickcheck_Examples.thy	Thu Jan 10 19:24:23 2008 +0100
+++ b/src/HOL/ex/Quickcheck_Examples.thy	Thu Jan 10 19:25:08 2008 +0100
@@ -41,6 +41,22 @@
   quickcheck
   oops
 
+text {* An example involving functions inside other data structures *}
+
+consts app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a"
+
+primrec
+  "app [] x = x"
+  "app (f # fs) x = app fs (f x)"
+
+lemma "app (fs @ gs) x = app gs (app fs x)"
+  quickcheck
+  by (induct fs arbitrary: x) simp_all
+
+lemma "app (fs @ gs) x = app fs (app gs x)"
+  quickcheck
+  oops
+
 consts
   occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"
 primrec
@@ -53,7 +69,7 @@
   "del1 a [] = []"
   "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
 
-(* A lemma, you'd think to be true from our experience with delAll*)
+text {* A lemma, you'd think to be true from our experience with delAll *}
 lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
   -- {* Wrong. Precondition needed.*}
   quickcheck