Calculating paths using Isabelle's "value" command

Vote count:

0

I have written a function for extracting the set of paths through a given set of edges, from a given source to a given target, and I would like to test it using Isabelle's value command. Here is my theory:

theory Scratch imports 
  Main 
  "~~/src/HOL/Library/Code_Target_Nat"
begin

type_synonym edge = "nat × nat"

definition paths :: "edge list ⇒ nat ⇒ nat ⇒ nat list set" 
where "paths edges source target ≡ 
  (* The set of paths from source to target, following edges *)
  {p. let n = length p in n > 0 ∧ p ! 0 = source ∧ p!(n - 1) = target ∧ 
  (∀i < n - 1. (p ! i, p ! (i + 1)) ∈ set edges)}"

value "paths [(1,2),(2,3),(1,5),(5,3),(4,5)] 1 3"
(* should be {[1,2,3],[1,5,3]} *)

end

It doesn't work; I get Wellsortedness error: Type nat list not of sort enum. I think the value command is struggling with the fact that it has to quantify over all lists p.

Is there a way to make this work? I tried adding arities nat :: enum and arities list :: (enum) enum, but that didn't help, plus I doubt I'm supposed to do that anyway.

asked 42 secs ago

John Wickerson

331