Re: [isabelle] check phases



On 30.07.2014 15:45, Lars Noschinski wrote:
> The invariant I am interested in is the preservation of binders: Given a
> constant c (declared by myself, so no check-phase should know about it)
> and an (unchecked) term t containing c exactly once, then the
> Abs(tractions) in t above c are the same as the abstractions above c in
> Syntax.check_term ctxt t (of course "same" is a bit fuzzy here --
> obviously types and names might change).
>
> Is this a reasonable expectation?
To provide a bit of background: The pat_subst tool we presented at the
Isabelle workshop allows pattern of the form

    at "Suc x" in "{x. _ + HOLE}"

to describe for example the subterm "Suc y" in the term "{y. 1 + (Suc y
+ 1))}" where the "x" in "Suc x" refers to the variable bound in the set
expression. Obviously, the bound variable "x" in the second term and the
free variable "x" in the first term should have the same type.

I achieve that by parsing the terms separatly and calling
Syntax.check_terms on

    ["Suc x", "x :: '?a", "{x :: '?a. _ + HOLE}"

(where ":: '?a" are type constraints added with Type.constraint). Now,
after checking the terms, I need to be able to associate the free
variables which the right bound variables again. If I can expect the
bound variables between root and HOLE to be the same before and after
the check, this is easy.

  -- Lars




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