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?
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
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\")]
you can also use
apply (cut_tac x=n and y="size list" in linorder_less_linear)
Hope this helps.
This archive was generated by a fusion of
Pipermail (Mailman edition) and