*Subject*: [isabelle] Problem with schematic variables, subst and flex-flex pairs*From*: Peter Lammich <peter.lammich at uni-muenster.de>*Date*: Thu, 18 Sep 2008 15:02:37 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <20080917141644.6hu70p1740ck8cc4@webmail.pdx.edu>*References*: <48D119CE.4070504@uni-muenster.de> <20080917141644.6hu70p1740ck8cc4@webmail.pdx.edu>*User-agent*: Thunderbird 2.0.0.14 (X11/20080421)

Consider the following subgoal 1. "!!x y a b. f ((x = y) = (a = b)) = ?P x y a b" now, I do: apply (subst (1 3) eq_commute) and get: goal (1 subgoal): 1. !!x y a b. f ((y = x) = (b = a)) = ?P6 x x x y y y a a a b b b flex-flex pairs: %x y a b. ?P6 x x x y y y a a a b b b =?= %x y a b. ?P4 x x y y a a b b

1. !!x y a b. f ((y = x) = (b = a)) = ?P x y a b

Regards and thanks in advance for any help, Peter Brian Huffman wrote:

Quoting Peter Lammich <peter.lammich at uni-muenster.de>:Hi all, I cannot figure out how to write apply (subst theorem) in the form: apply (tactic {* ... *})Hi Peter, Here is a silly example: lemma "(x = y) = (a = b)" apply (subst (1 3) eq_commute) -- New subgoal is "(y = x) = (b = a)"Note that there are three places that the eq_commute rule could applyto this subgoal; the optional (1 3) argument to "subst" says to applythe rule to the first and third, but not the second.You can get the same result with:apply (tactic {* EqSubst.eqsubst_tac @{context} [1,3] [ at {thmeq_commute}] 1 *})(The "1" at the end just says that the tactic should be applied to thefirst subgoal.)If you use [0] as the occL argument, this corresponds to the defaultbehavior of subst where the optional argument is omitted. (There is acomment in eqsubst.ML to this effect.) So the following are equivalent:apply (subst eq_commute)apply (tactic {* EqSubst.eqsubst_tac @{context} [0] [ at {thmeq_commute}] 1 *})Hope this helps. - BrianThe file Provers/eqsubst.thy seems to define this method, but it lacks documentation in the isabelle reference manual, the chapter on substitution there describes "stac" instead, which is not quite the same. Maybe my question reduces to the stupid question: What to fill in for the parameters of "fun eqsubst_tac ctxt occL thms i th", when I want to use it inside an: apply (tactic {* ... *}) ? Regards and thanks in advance for any help, Peter

**Follow-Ups**:**Re: [isabelle] Problem with schematic variables, subst and flex-flex pairs***From:*Lucas Dixon

**Re: [isabelle] Problem with schematic variables, subst and flex-flex pairs***From:*Jeremy Dawson

**References**:**[isabelle] subst translated to ML-level ?***From:*Peter Lammich

**Re: [isabelle] subst translated to ML-level ?***From:*Brian Huffman

- Previous by Date: Re: [isabelle] subst translated to ML-level ?
- Next by Date: Re: [isabelle] Problem with schematic variables, subst and flex-flex pairs
- Previous by Thread: Re: [isabelle] subst translated to ML-level ?
- Next by Thread: Re: [isabelle] Problem with schematic variables, subst and flex-flex pairs
- Cl-isabelle-users September 2008 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