[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.