[isabelle] term_uncheck and abbreviation folding



Hello,

I've run into a situation where the last uncheck phase returns
abbreviations folded differently than what's shown in the final
output. An example:

setup
{*
  let fun out l x = let val _ = writeln (l ^ ": " ^ (@{make_string} x)) in x end
  in Context.theory_map (Syntax_Phases.term_uncheck 100 "test" (fn _
=> map (out "uncheck"))) end
*}

ML {* Syntax_Phases.print_checks @{context} *}

term "surj f"
term "~ surj f"

Thet print_checks command shows that the 'test' uncheck phase is the
last one to happen. The first term command displays "uncheck: Const
("Fun.surj", "('b ⇒ 'a) ⇒ HOL.bool") $ Free ("f", "'b ⇒ 'a")", showing
that the surj abbreviation was successfully folded by the last uncheck
phase that wasn't 'test'. The second term command, however, outputs
"uncheck: Const ("HOL.not_equal", "'a Set.set ⇒ 'a Set.set ⇒
HOL.bool") $ (Const ("Set.range", "('b ⇒ 'a) ⇒ 'a Set.set") $ Free
("f", "'b ⇒ 'a")) $ Const ("Set.UNIV", "'a Set.set")". It appears that
instead of folding the surj abbreviation, it decided to fold the
not_equal abbreviation, which then prevented it from folding surj. Of
course, that's just guesswork on my part. What remains is that
something does successfully fold the surj abbreviation, as the final
result in the output panel is "~ surj f", but that transformation
appears to happen after the last uncheck phase.

So my questions are:

1. Is this the way it's intended to work?
2. If it is, is there any way to do transformations (like
check/uncheck) on the final terms as they appear in the output?
3. As an aside, which abbreviation takes priority when there a
conflict as in the case of surj? I haven't been able to find anything
about it in the reference manual.

Thanks in advance,
 Julian




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