Email Gateway (Aug 18 2022 at 10:24): Email Gateway (Aug 18 2022 at 10:24):From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
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?
Thanks for any help
Jeremy
Email Gateway (Aug 18 2022 at 10:25):From: Brian Huffman <brianh@cs.pdx.edu>
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.
Last updated: May 03 2024 at 04:19 UTC