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.6  
     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.29  
    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