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