Re: [isabelle] cut_inst_tac and insert



On Sunday 15 April 2007 23:14, Jeremy Dawson wrote:
> I have a goal of the form
>   1. !!a list.
>            ... list ...
> When I do
> apply (tactic "(cut_inst_tac [(\"x\", \"n\"), (\"y\", \"size list\")]
>      linorder_less_linear 1)") ;
> the goal becomes
>      n < length list | n = length list | length list < n ==> (as before)
> but if instead I do
>    apply (insert linorder_less_linear [where x = "n" and y = "size list"])
> I get
>   !!a lista.
>            n < size list | n = size list | size list < n |]
>         ==> (as before, but with list replaces by lista)
> Why is this?  Is it possible (using Isar) to stop this happening?

Hi Jeremy,

I have also run into this problem with the insert tactic. I believe the 
explanation for its behavior has to do with the scoping of variable names, 
and the distinction between bound and free variables. In your subgoal, "a" 
and "list" are bound variables (bound by the "!!" meta-quantifier) and "n" is 
a free variable. Proof General should show this distinction by coloring the 
names differently.

When you instantiate linorder_less_linear [where x = "n" and y = "size list"], 
the "where" attribute knows nothing about the variables bound within your 
subgoal, so both "n" and "list" are treated as free variables. When the lemma 
containing the free variable "list" is inserted, Isabelle conveniently 
renames the bound variable "list" to "lista" to avoid a name clash.

On the other hand, cut_inst_tac does know about the variables bound within 
your subgoal, so in this case "list" refers to the variable bound in the 
subgoal instead of a new free variable. By the way, instead of

apply (tactic "(cut_inst_tac [(\"x\", \"n\"), (\"y\", \"size list\")] 
linorder_less_linear 1)")

you can also use

apply (cut_tac x=n and y="size list" in linorder_less_linear)

Hope this helps.

- Brian





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