src/HOL/ex/Quickcheck_Examples.thy

avoiding direct references to numeral presentation

(*  Title:      HOL/ex/Quickcheck_Examples.thy
    ID:         $Id$
    Author:     Stefan Berghofer
    Copyright   2004 TU Muenchen
*)

header {* Examples for the 'quickcheck' command *}

theory Quickcheck_Examples imports Main begin

text {*
The 'quickcheck' command allows to find counterexamples by evaluating
formulae under an assignment of free variables to random values.
In contrast to 'refute', it can deal with inductive datatypes,
but cannot handle quantifiers.
*}

subsection {* Lists *}

theorem "map g (map f xs) = map (g o f) xs"
  quickcheck
  oops

theorem "map g (map f xs) = map (f o g) xs"
  quickcheck
  oops

theorem "rev (xs @ ys) = rev ys @ rev xs"
  quickcheck
  oops

theorem "rev (xs @ ys) = rev xs @ rev ys"
  quickcheck
  oops

theorem "rev (rev xs) = xs"
  quickcheck
  oops

theorem "rev xs = xs"
  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
  "occurs a [] = 0"
  "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)"

consts
  del1 :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
primrec
  "del1 a [] = []"
  "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))"

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
  oops

lemma "xs ~= [] \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
  quickcheck
    -- {* Also wrong.*}
  oops

lemma "0 < occurs a xs \<longrightarrow> Suc (occurs a (del1 a xs)) = occurs a xs"
  quickcheck
  apply (induct_tac xs)  
  apply auto
    -- {* Correct! *}
  done

consts
  replace :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
primrec
  "replace a b [] = []"
  "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) 
                            else (x#(replace a b xs)))"

lemma "occurs a xs = occurs b (replace a b xs)"
  quickcheck
  -- {* Wrong. Precondition needed.*}
  oops

lemma "occurs b xs = 0 \<or> a=b \<longrightarrow> occurs a xs = occurs b (replace a b xs)"
  quickcheck
  apply (induct_tac xs)  
  apply auto
  done


subsection {* Trees *}

datatype 'a tree = Twig |  Leaf 'a | Branch "'a tree" "'a tree"

consts
  leaves :: "'a tree \<Rightarrow> 'a list"
primrec
  "leaves Twig = []"
  "leaves (Leaf a) = [a]"
  "leaves (Branch l r) = (leaves l) @ (leaves r)"

consts
  plant :: "'a list \<Rightarrow> 'a tree"
primrec
  "plant [] = Twig "
  "plant (x#xs) = Branch (Leaf x) (plant xs)"

consts
  mirror :: "'a tree \<Rightarrow> 'a tree"
primrec
  "mirror (Twig) = Twig "
  "mirror (Leaf a) = Leaf a "
  "mirror (Branch l r) = Branch (mirror r) (mirror l)"

theorem "plant (rev (leaves xt)) = mirror xt"
  quickcheck
    --{* Wrong! *} 
  oops

theorem "plant((leaves xt) @ (leaves yt)) = Branch xt yt"
  quickcheck
    --{* Wrong! *} 
  oops

datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree"

consts
  inOrder :: "'a ntree \<Rightarrow> 'a list"
primrec
  "inOrder (Tip a)= [a]"
  "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)"

consts
  root :: "'a ntree \<Rightarrow> 'a"
primrec
  "root (Tip a) = a"
  "root (Node f x y) = f"

theorem "hd(inOrder xt) = root xt"
  quickcheck
    --{* Wrong! *} 
  oops

end