Re: [isabelle] recdef woes

The context of that recursive call hasn't been tracked. Maybe the
recdef termination condition extractor doesn't know about the
congruence theorem for bounded quantification?


On Nov 30, 2005, at 3:17 PM, Michael Norrish wrote:

  typ_tag = char_tt | short_tt | int_tt | long_tt | ptr_tt
          | struct_tt "typ_tag list" | array_tt "typ_tag" "nat"

  wf_tag :: "typ_tag \<Rightarrow> bool"

lemma[simp]: "t \<in> set tyl \<longrightarrow> size t < Suc (typ_tag_list_size
by (induct_tac tyl,auto)

recdef wf_tag "measure size"
  "wf_tag char_tt = True"
  "wf_tag short_tt = True"
  "wf_tag int_tt = True"
  "wf_tag long_tt = True"
  "wf_tag ptr_tt = True"
"wf_tag (struct_tt tyl) = (\<not> null tyl \<and> (\<forall> t \<in> set tyl.
wf_tag t))"
  "wf_tag (array_tt ty n) = wf_tag ty"

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