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