Re: [isabelle] check phases



On Wed, 30 Jul 2014, Lars Noschinski wrote:

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.

Reading this description twice, I would say it should work, but there might be fine points to be observed.

I still need to read your paper from the Isabelle workshop -- it is already printed out and on the top of the stack.


	Makarius




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