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?

Konrad.

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

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

consts
  wf_tag :: "typ_tag \<Rightarrow> bool"

lemma[simp]: "t \<in> set tyl \<longrightarrow> size t < Suc (typ_tag_list_size
tyl)"
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.