CODEWITHSUNDEEP
isabelle
user2813637
user2813637

Reputation: 23

Proving a simple lemma about trees in Isabelle

I am brand new to Isabelle. I have a simple tree datatype and a function getTree. getTree uses a boolean list to control its traversal of the tree (it goes left for false and right for true). When it gets to the end of the list, it returns the remaining subtree. If it reaches a leaf before reaching the end of the list, it returns that leaf. I want to show that if getTree returns a leaf using some list ys, then it will return the same leaf using (ys @ bs) (once you get to a leaf, the remaining list doesn't matter).

All of my attempts to prove this have failed. If anyone has any suggestions, I would be very grateful.

Here is the code:

datatype 'a tree = 
  Leaf 'a |
  Node 'a "'a tree" "'a tree"

fun getTree :: "'a tree ⇒ bool list ⇒ 'a tree" where
  "getTree (Leaf x) ys = (Leaf x)" |
  "getTree r [] = r" |
  "getTree (Node x l r) (False # ys) = getTree l ys" |
  "getTree (Node x l r) (True # ys) = getTree r ys"

lemma: "getTree t ys = Leaf a ==> getTree t (ys @ bs) = Leaf a"

Upvotes: 1

Views: 152

Answers (1)

fabian.immler
fabian.immler

Reputation: 71

When you define a function via "fun", Isabelle generates an induction rule according to the recursive structure of the definition. Here you can make use of getTree.induct:

by (induct t ys rule: getTree.induct) simp_all

Upvotes: 3

Related Questions