# [isabelle] proofterms incomplete wrt beta reduction

Hello,
I have a question about the proofterms of Isabelle. Consider the
proof of the theorem HOL.trans. Expanded, say using
ML {*
fun expand_proof thm =
let
val {prop, der=(_, prf), sign, ...} = rep_thm thm

` val prf' = Reconstruct.reconstruct_proof sign prop
``(Proofterm.strip_thm prf)
` val prf'' = Reconstruct.expand_proof sign [("", None)] prf'
in
prf''
end
*}
ML {* PolyML.print_depth 100 *}
ML {* expand_proof (thm "HOL.trans") *}
this is long, but basically it amounts to:
\("H" : r = s)
\("H2" : s = t)
HOL.subst s t (\x. r = x) H2 H
Now, HOL.subst has the form
s = t ==> P s ==> P t
So after the first 4 applications above we are left with
(\x. r = x) s ==> (\x. t = x) t
But H has the form r = s, which is beta equivalent, but certainly not
equal to (\x. r=x) s. This beta conversion is undocumented.
It is thus difficult, when translating these proof terms,
to know with precision when to apply beta reduction and when not to.

`I realize there is no beta axiom, as in HOL Light. Is there a
``general way
`to tell when beta reduction should be applied? Currently I apply it

`wildly everywhere I can and it seems to work most of the time, but
``I'd like
`to be precise about it.
Thanks,
Sean

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