I'm trying to define an inductive predicate for some graph calculations:
type_synonym node = nat
type_synonym edge = nat
record graph =
nodes :: "node set"
edges :: "edge set"
source :: "edge ⇒ node"
target :: "edge ⇒ node"
weight :: "edge ⇒ nat"
inductive min_sum where
"edges G = {e} ⟹
weight G e = x ⟹
min_sum G x"
code_pred [show_modes] min_sum .
definition "G1 ≡ ⦇
nodes = {1,2},
edges = {1},
source = (λx. undefined)(1 := 1),
target = (λx. undefined)(1 := 2),
weight = (λx. undefined)(1 := 5)
⦈"
(* Expected result: {5} *)
values "{x. min_sum G1 x}"
Is it possible to make it evaluable? Should I replace set by fset and functions by finite maps? Or replace record by inductive data type? Or there is another solution?
If I want value to work, my (extremely basic) approach is to always let quantifications range over finite or explicit things, and to use definition and fun/primrec instead of inductive and the like. The following works:
definition min_sum :: ‹graph ⇒ nat ⇒ bool› where
‹min_sum G x ≡ ∃e∈(edges G). {e} = edges G ∧ weight G e = x›
value ‹{x∈{1,2,3,4,5,6,7,8,9,10}. min_sum G1 x}›
Note the e∈(edges G) and the x∈{1,2,3,4,5,6,7,8,9,10} where your example code previously had free quantifications over nat.
Generally, lists will also work more often than sets. (And fsets are just slightly abstracted lists...)
But I'm no nerd for Isabelle code gen. So maybe, someone else knows more about the inner workings of this.