Re: [isabelle] recdef woes

nipkow at 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)"

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


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)




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