On 26 Mar 2014, at 07:58, Bill Richter <rich...@math.northwestern.edu> wrote:
> Thanks, Konrad! The proof of SYM in the HOL4 manual Description (p 46) is
> fine because the HOL4 SUBST is much more powerful than the HOL Light INST.
> On p 26, SUBST is described by
>
> SUBST : (thm * term)list -> term -> thm -> thm
>
> t[t1 , . . . , tn ] yields t[t1',...,tn']
>
> . where t[t1 , . . . , tn ] denotes a term t with some free
> occurrences of the terms t1,...,tn singled out [...]
>
> The second argument is a template term t[x1 , . . . , xn ] in which
> occurrences of the variable xi (where 1 ≤ i ≤ n) are used to mark the
> places where substitutions with |- ti =ti are to be done.
>
> The template stuff looks pretty clever. I suppose the term t[x1 , . . . , xn
> ] means t with the variable xi replacing each free occurence of ti we want
> replaced by ti'. I think it should say that the variables xi don't occur in
> t.
It should be noted that SUBST, while it has a complex looking parametrisation,
is actually only a slightly optimised version of a special case of Peter
Andrews rule R (see http://plato.stanford.edu/entries/type-theory-church/). The
antecedents of rule R are theorems |- C and|- A = B and the conclusion is |- C’
where C’ is C with exactly one occurrence of A as a sub term replaced by B.
The optimisation is that SUBST lets you do lots of instances of rule R in one
go provided that the subterms you are replacing don’t overlap. It is a special
case, because in rule R, free variables of A and B may be bound at the point of
the occurrence of A in B. So rule R is implicitly taking the universal closure
of the equation A = B. SUBST as implemented in HOL4 and ProofPower at least
does not allow free variables of A and B to become captured (presumably because
in the sequent formulation used in the implementations, you don’t want the
overhead of checking whether the free variables of A and B appear in the
assumption lists).
By the way, I was slightly surprised when trying to check the HOL4
implementation to find that the following call of SUBST does not raise an
exception:
val thm = TAC_PROOF(([], ``(x : unit) = y``),
ONCE_REWRITE_TAC[one] THEN ACCEPT_TAC (REFL ``()``));
SUBST [``v:unit`` |-> thm] ``(\x : unit. x) = (\x.v)`` (REFL `` \x : unit. x
``) ;
but instead returns
val it = |- (\x. x) = (\x. x): thm
The Reference manual suggests that this should fail because the occurrence of x
at the place marked by v is not free. (The analogue in ProofPower raises an
exception).
Regards,
Rob.
------------------------------------------------------------------------------
Start Your Social Network Today - Download eXo Platform
Build your Enterprise Intranet with eXo Platform Software
Java Based Open Source Intranet - Social, Extensible, Cloud Ready
Get Started Now And Turn Your Intranet Into A Collaboration Platform
http://p.sf.net/sfu/ExoPlatform
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
