[isabelle] recdef woes



I'm using the most recent CVS version of Isabelle, or something very
close to it.  

recdef is making the definition at the bottom of the attached

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

print_theorems (* have a look at wf_tag.simps *)
----------------------------------------------------------------------

in such a way that there is still a check to see if the argument to
wf_tag is in the measure, and if not, giving me back arbitrary.

The little lemma above it doesn't seem to help.   

The wf_tag.induct theorem is also "wrong" because it doesn't allow me
to assume anything about the contents of tyl.

Using

  wf_tag (struct_tt tyl) = (\<not> null tyl \<and> 
                            list_all id (map wf_tag tyl))

works.  Using "list_all wf_tag tyl" doesn't.

No doubt it wouldn't be difficult to recast this as an inductive
definition.

Michael.






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