Re: [isabelle] Record simplification



Hi,

Apparently I disregarded a warning message in the Isabelle2004 version, I have
done some corrections and found the following works ok:

constdefs
start_forest :: "('a, unit) pre_graph_scheme => ('a,unit) forest"
  "start_forest H == { (| Verts={v},Edges={},...=() |) | v.( 
v: (Verts H))  }"

Thanks
Benny

Quoting Norbert Schirmer <norbert.schirmer at web.de>:

> Hello Benny,
> 
> On Wednesday 28 December 2005 15:47, shimonyb at techunix.technion.ac.il wrote:
> > 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"
> >
> > constdefs start_forest :: "('a, 'b) pre_graph_scheme ==> ('a,'b) forest"
> >  "start_forest H == { (|Verts={v},Edges={} |) | v.   v: (Verts H)  }"
> 
> Your declaration of start_forest is to general. You definition only defines
> "start_forest:: 'a pre_graph => 'a pre_graph set"
> 
> Maybe this is your problem?
> 
> Otherwise send me a concrete lemma which leads to a concrete error message,
> so 
> that I can give you a more concrete answer...
> 
> 
>    Norbert
> 







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