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
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>
"wf_tag (array_tt ty n) = wf_tag ty"
This archive was generated by a fusion of
Pipermail (Mailman edition) and