Re: [isabelle] recdef woes



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

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

Tobias





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