src/HOL/ex/Quickcheck_Examples.thy
 changeset 25891 1bd12187a96e parent 17388 495c799df31d child 28314 053419cefd3c
1.1 --- a/src/HOL/ex/Quickcheck_Examples.thy	Thu Jan 10 19:24:23 2008 +0100
1.2 +++ b/src/HOL/ex/Quickcheck_Examples.thy	Thu Jan 10 19:25:08 2008 +0100
1.3 @@ -41,6 +41,22 @@
1.4    quickcheck
1.5    oops
1.7 +text {* An example involving functions inside other data structures *}
1.8 +
1.9 +consts app :: "('a \<Rightarrow> 'a) list \<Rightarrow> 'a \<Rightarrow> 'a"
1.10 +
1.11 +primrec
1.12 +  "app [] x = x"
1.13 +  "app (f # fs) x = app fs (f x)"
1.14 +
1.15 +lemma "app (fs @ gs) x = app gs (app fs x)"
1.16 +  quickcheck
1.17 +  by (induct fs arbitrary: x) simp_all
1.18 +
1.19 +lemma "app (fs @ gs) x = app fs (app gs x)"
1.20 +  quickcheck
1.21 +  oops
1.22 +
1.23  consts
1.24    occurs :: "'a \<Rightarrow> 'a list \<Rightarrow> nat"
1.25  primrec
1.26 @@ -53,7 +69,7 @@
1.27    "del1 a [] = []"
1.28    "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"
1.30 -(* A lemma, you'd think to be true from our experience with delAll*)
1.31 +text {* A lemma, you'd think to be true from our experience with delAll *}
1.32  lemma "Suc (occurs a (del1 a xs)) = occurs a xs"
1.33    -- {* Wrong. Precondition needed.*}
1.34    quickcheck