Re: [isabelle] recdef woes



nipkow at in.tum.de writes:
> >  "wf_tag (struct_tt tyl) = (\<not> null tyl \<and> (\<forall> t \<in> set tyl. wf_tag t))"
 
> I assume this clause is giving you trouble?
> And this lemma is meant to help?
 
> > lemma[simp]: "t \<in> set tyl \<longrightarrow> size t < Suc (typ_tag_list_size tyl)"

Yes. 
 
> If yes, maybe you could reformulate it using list_all and include a
> congruence rule for list_all (see the Tutorial on Advanced forms of
> recursion). 


> Something like this:

> xs = ys ==> (!!x. x : set ys ==> f x = g x) ==> list_all f xs = list_all g ys

There must be some sort of congruences already in there because 

   list_all id (map wf_tag tys) 

works.

The fact that "list_all wf_tag tys" doesn't work is just mysterious.

> >  "align_tt (struct_tt (ty#tys)) = foldr (\<lambda>ty n. max (align_tt ty) n)
> >                                          tys (align_tt ty)"
 
> This is similar. I assume HOL4 gets it right because Konrad has
> included a congruence rule for foldr by default?

I suppose.  But again, Isabelle must be doing something along these
lines itself because the similar looking

  foldr max (map align_tt tys) (align_tt ty)

works. 

Michael.

 






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