# [isabelle] Record simplification

Hello All,
I am working on a graph algorithm proof, and i am trying to use a Record
definition of a graph:
types 'a edge = "'a set"
record 'a pre_graph =
Verts :: "'a set"
Edges :: "'a edge set"
types ('a,'b) forest = "('a,'b) pre_graph_scheme set"
Yet I get many errors with trivial simplification commands such as:
constdefs start_forest :: "('a, 'b) pre_graph_scheme ==> ('a,'b) forest"
"start_forest H == { (|Verts={v},Edges={} |) | v. v: (Verts H) }"
....
lemma ....
apply (simp add: start_forest_def)
What is the problem with my definition?
P.S: When using a naive product definition for a graph, these problems don't
occur.
Thanks
Benny

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*