# [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.