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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and