*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] cut_inst_tac and insert*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Fri, 20 Apr 2007 09:18:38 -0700*Cc*: Jeremy Dawson <Jeremy.Dawson at rsise.anu.edu.au>*In-reply-to*: <46231455.7010404@rsise.anu.edu.au>*References*: <044933B9-73BD-4075-8B6D-60DEFCC44D29@klebermass.de> <Pine.LNX.4.63.0704021105240.24191@atbroy100.informatik.tu-muenchen.de> <46231455.7010404@rsise.anu.edu.au>*User-agent*: KMail/1.8

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

**References**:**Re: [isabelle] can anyone explain this?***From:*Makarius

**[isabelle] cut_inst_tac and insert***From:*Jeremy Dawson

- Previous by Date: [isabelle] PhD position at INRIA
- Next by Date: [isabelle] 2nd CFP: VERIFY'07 - 4th International Verification Workshop
- Previous by Thread: [isabelle] cut_inst_tac and insert
- Next by Thread: [isabelle] odd type error message
- Cl-isabelle-users April 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list