Re: [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]&quot; im Auftrag von &quot;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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.