*To*: scott constable <sdconsta at syr.edu>, "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Capturing Bound Variables with subst*From*: "Lochbihler Andreas" <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 3 Mar 2015 20:22:19 +0000*Accept-language*: de-DE, de-CH, en-US*Cc*: Akash Waran <awaran at syr.edu>*In-reply-to*: <CADYF24fa4HZsUi8yE3xswRRW=NTbc1CNMQ-Qsx_nRkvnCAhTjA@mail.gmail.com>*References*: <CADYF24fa4HZsUi8yE3xswRRW=NTbc1CNMQ-Qsx_nRkvnCAhTjA@mail.gmail.com>*Thread-index*: AQHQVdUQYNSdgSEbj0Ky6LC8y6e5pp0LMsxc*Thread-topic*: [isabelle] Capturing Bound Variables with subst

Dear Scott, In Isabelle2014, the instantiation attributes "of" and "where" support a "for" clause. This allows you to generalise over the variables in the instantiation expressions. For example, in the theorem whileLoop_add_inv [where M="\<lambda> (n', _). ptr_val n'" and I ="\<lambda> n' _. n' < p" for p] the variable p is a schematic again, which the normal subst method can then unify with the parameter of the goal. In most cases, this is sufficient. Unfortunatelz, there is no subst_tac method that would allow you to refer to the parameters of the goal as the old-style tactic emulations *rule_tac. Hope this helps, Andreas ________________________________________ Von: cl-isabelle-users-bounces at lists.cam.ac.uk [cl-isabelle-users-bounces at lists.cam.ac.uk]" im Auftrag von "scott constable [sdconsta at syr.edu] Gesendet: Dienstag, 3. März 2015 18:09 An: isabelle-users at cl.cam.ac.uk Cc: Akash Waran Betreff: [isabelle] Capturing Bound Variables with subst Hi All, I'm currently trying to simplify a subgoal via a substitution. What I would like to do is the following: apply (subst whileLoop_add_inv [where M="\<lambda> (n', _). ptr_val n'" and I ="\<lambda> n' _. n' < p"]) The problem is that "p" is bound by all (!!) to the entire scope of the current subgoal, and subst apparently cannot express instantiations that refer to such bound variables. The other alternative is to use an erule_tac applied to subst. But I cannot figure out a way to invoke this rule while also defining the schematic variables required by the rule whileLoop_add_inv. So it looks like I need something like a "subst_tac", which is not currently a feature of Isabelle/HOL. Is there a way around this? Many thanks in advance, ~Scott Constable

**Follow-Ups**:**Re: [isabelle] Capturing Bound Variables with subst***From:*scott constable

**Re: [isabelle] Capturing Bound Variables with subst***From:*Peter Lammich

**References**:**[isabelle] Capturing Bound Variables with subst***From:*scott constable

- Previous by Date: Re: [isabelle] [isabelle-dev] What is this 3 levels of lambda calculi?
- Next by Date: [isabelle] Rearranging equations before taking limits
- Previous by Thread: [isabelle] Capturing Bound Variables with subst
- Next by Thread: Re: [isabelle] Capturing Bound Variables with subst
- Cl-isabelle-users March 2015 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