Stream: Beginner Questions

Topic: Nitpick and exceptions

Adrián Doña Mateo (Aug 15 2022 at 12:31):

I've defined a basic rooted tree datatype and a function that, given a list of indices, recovers a subtree from a larger tree.

datatype tree = Node (subtrees: "tree list")

abbreviation Leaf :: tree where
"Leaf ≡ Node []"

fun subtree :: "tree ⇒ nat list ⇒ tree" ("_ !t _" [59,60]59) where
"t !t [] = t" |
"t !t (i#xs) = subtrees (t !t xs) ! i"

value "Leaf !t []" (* Leaf *)
value "Node [Node [Leaf, Leaf, Leaf], Leaf, Node [Leaf]] !t [0]"    (* Node [Leaf, Leaf, Leaf] *)
value "Node [Node [Leaf, Leaf, Leaf], Leaf, Node [Leaf]] !t [2,0]"  (* Leaf *)
value "Node [Node [Leaf, Leaf, Leaf], Leaf, Node [Leaf]] !t [1]"    (* Leaf *)
value "Node [Node [Leaf, Leaf, Leaf], Leaf, Node [Leaf]] !t [0,2]"  (* Leaf *)

lemma subtree_exists_imp: "Node ts !t xs @ [i] = Node us ⟹ i < length ts"
  try

The function subtree raises an exception whenever the list of indices is not valid within the given tree. I would like to prove the lemma at the bottom, essentially saying that if !t doesn't raise an exception then at least the last index is within the limits of the tree. However, Nitpick somehow thinks that the following is a counterexample:

  Free variables:
    i = 1
    ts = [Leaf]
    us = [Leaf]
    xs = []

when in fact Node [Leaf] !t [] @ [1] raises an exception and so cannot be equal to Node [Leaf].
Is there a way of rephrasing the lemma or the definition of subtree that would make this work?

Mathias Fleury (Aug 24 2022 at 07:51):

I believe that the issue is that nitpick works with total functions. In your case "[] ! 0" is undefined, so it can take any value. The only way I can think of is making the function total for example by making it return Some/None

Wolfgang Jeltsch (Aug 25 2022 at 22:45):

In your case "[] ! 0" is undefined, so it can take any value.

That’s not just an issue with Nitpick, but a fundamental feature of Isabelle. Every Isabelle function is total, and the morally partial ones just aren’t specified for those arguments that lie outside their moral domains.

Last updated: Dec 21 2024 at 16:20 UTC