Re: [isabelle] Record simplification



On Wed, 28 Dec 2005 shimonyb at techunix.technion.ac.il wrote:

> 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? 

As Norbert has pointed out already, there seems to be an oddity with the
types of your definition.  Isabelle2004 produces the following message:

  ### Definition of GenTest.start_forest :: "'a pre_graph => 'a pre_graph set"
  ### is strictly less general than the declared type (see "GenTest.start_forest_def")

while Isabelle2005 rejects it outright.


	Makarius





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