Email Gateway (Aug 17 2022 at 13:28): Email Gateway (Aug 17 2022 at 13:28):From: Michael Norrish <Michael.Norrish@nicta.com.au>
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.
Email Gateway (Aug 17 2022 at 13:28):From: Konrad Slind <slind@cs.utah.edu>
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.
Email Gateway (Aug 17 2022 at 13:28):From: Michael Norrish <Michael.Norrish@nicta.com.au>
While we're about it, the following also fails, generating an
impossible termination condition. (HOL4 gets this right, Konrad will
be pleased to hear.)
recdef align_tt "measure size"
"align_tt char_tt = 1"
"align_tt short_tt = 2"
"align_tt int_tt = 4"
"align_tt long_tt = 4"
"align_tt ptr_tt = 4"
"align_tt (array_tt ty n) = align_tt ty"
"align_tt (struct_tt []) = 0"
"align_tt (struct_tt (ty#tys)) = foldr (\<lambda>ty n. max (align_tt ty) n)
tys (align_tt ty)"
Michael.
Email Gateway (Aug 17 2022 at 13:45):From: Michael Norrish <Michael.Norrish@nicta.com.au>
Alexander Krauss writes:
I still don't understand why list_all on its own didn't work, but
when I combined list_all with map it did work. Anyway, thanks for the
help in finding a workaround.
Michael.
Email Gateway (Aug 17 2022 at 13:45):From: Gerwin Klein <gerwin.klein@nicta.com.au>
I just checked the library: that is because there is a congruence rule for
map, but none for list_all.
In the example with "list_all id (map ..)" the "id" probably made it simple
enough to deal with.
Cheers,
Gerwin
Last updated: May 03 2024 at 08:18 UTC