(* Implementation of search in a quadtree - for naive quadtree *)
fun search_quadtree:: "nat quadtree ⇒ nat ⇒ bool" where
  "search_quadtree (Leaf a) b = (if a = b then True else False)" |
  "search_quadtree (Node l1 l2 l3 l4 a) b = (if a = b then True
                                             else search_quadtree l1 b ∨
                                                  search_quadtree l2 b ∨
                                                  search_quadtree l3 b ∨
                                                  search_quadtree l4 b)"

(* Return the data in the node of a quadtree *)
fun datain_quadtree:: "nat quadtree ⇒ nat" where
  "datain_quadtree (Leaf a) = a" |
  "datain_quadtree (Node l1 l2 l3 l4 a) = a"

(* Create a function that returns a set of elements in the quadtree *)
fun quadtree_set:: "nat quadtree ⇒ nat set ⇒ nat set" where
  "quadtree_set (Leaf a) as = {a} ∪ as" |
  "quadtree_set (Node l1 l2 l3 l4 a) as = {a} ∪
                                          {datain_quadtree l1} ∪
                                          {datain_quadtree l2} ∪
                                          {datain_quadtree l3} ∪
                                          {datain_quadtree l4} ∪
                                          as"

(* Create a function that returns a set of elements in that tree *)
lemma "search_quadtree quadtree a' ⟹ True ⟷ a' ∈ quadtree_set (quadtree) {}"

Auto Quickcheck found a counterexample:
  quadtree = Node (Leaf 1) (Leaf 1) (Leaf 1) (Node (Leaf 0) (Leaf 0) (Leaf 0) (Leaf 0) 1) 1
  a' = 0
Evaluated terms:
  True = True
  a' ∈ quadtree_set quadtree {} = False