Email Gateway (Aug 22 2022 at 09:00): Email Gateway (Aug 22 2022 at 09:00):From: scott constable <sdconsta@syr.edu>
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
Email Gateway (Aug 22 2022 at 09:01):From: Peter Lammich <lammich@in.tum.de>
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.
There is a subst_tac in AFP/Automatic_Refinement/Lib/Refine_Util.
Unfortunately, those things are unlikely to end up in the official
Isabelle Release, as apply-style reasoning is considered ancient style,
and the official philosophy seems to be trying to abandon all
apply-style reasoning in favour of Isar-proofs.
For the domain of verification condition generation/discharging, and
program synthesis, however, I'm not yet aware of viable Isar
alternatives. However, Lars Noschinski has done some initial work there.
For subst_tac, you can either include the Refine_Util-theory, or use the
following code snippet:
ML ‹
local
(* Substitution with dynamic instantiation of parameters.
By Lars Noschinski. *)
fun eqsubst_tac' ctxt asm =
if asm then EqSubst.eqsubst_asm_tac ctxt else EqSubst.eqsubst_tac
ctxt
fun subst_method inst_tac tac =
Args.goal_spec --
Scan.lift (Args.mode "asm" -- Scan.optional (Args.parens
(Scan.repeat Parse.nat)) [0]) --
Scan.optional (Scan.lift
(Parse.and_list1
(Args.var -- (Args.$$$ "=" |-- Parse.!!!
Args.name_inner_syntax)) --|
Args.$$$ "in")) [] --
Attrib.thms >>
(fn (((quant, (asm, occL)), insts), thms) => fn ctxt => METHOD
(fn facts =>
if null insts then
quant (Method.insert_tac facts THEN' tac ctxt asm occL thms)
else
(case thms of
[thm] => quant (
Method.insert_tac facts THEN' inst_tac ctxt asm occL
insts thm)
| _ => error "Cannot have instantiations with multiple
rules")));
in
fun eqsubst_inst_tac ctxt asm occL insts thm =
Subgoal.FOCUS (
fn {context=ctxt,...} => let
val ctxt' = ctxt |> Proof_Context.set_mode
Proof_Context.mode_schematic (* FIXME !? *)
val thm' = thm |> Rule_Insts.read_instantiate ctxt' insts []
in eqsubst_tac' ctxt asm occL [thm'] 1 end
) ctxt
val eqsubst_inst_meth = subst_method eqsubst_inst_tac eqsubst_tac'
end
›
setup ‹ Method.setup @{binding subst_tac} eqsubst_inst_meth
"single-step substitution (dynamic instantiation)"›
Hope this helps,
Andreas
Von: cl-isabelle-users-bounces@lists.cam.ac.uk [cl-isabelle-users-bounces@lists.cam.ac.uk]" im Auftrag von "scott constable [sdconsta@syr.edu]
Gesendet: Dienstag, 3. März 2015 18:09
An: isabelle-users@cl.cam.ac.uk
Cc: Akash Waran
Betreff: [isabelle] Capturing Bound Variables with substHi 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
Email Gateway (Aug 22 2022 at 09:01):From: Lochbihler Andreas <andreas.lochbihler@inf.ethz.ch>
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
Email Gateway (Aug 22 2022 at 09:01):From: scott constable <sdconsta@syr.edu>
Worked like a charm. Thanks so much!
~Scott Constable
Email Gateway (Aug 22 2022 at 09:01):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
On 4 Mar 2015, at 9:46 pm, Peter Lammich <lammich@in.tum.de> wrote:
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.
There is a subst_tac in AFP/Automatic_Refinement/Lib/Refine_Util.
Unfortunately, those things are unlikely to end up in the official
Isabelle Release, as apply-style reasoning is considered ancient style,
and the official philosophy seems to be trying to abandon all
apply-style reasoning in favour of Isar-proofs.
I don’t agree with that. First of all, apply-style is Isar as well, it’s just not structured proof. The actually ancient proof style is ML script, pasted manually from your editor into the ML top-level in a shell ;-) Second, there are quite a few situations where apply style is entirely adequate.
Structured proof is nicer and more readable for many, maybe even most situations, but not for everything.
For the domain of verification condition generation/discharging, and
program synthesis, however, I'm not yet aware of viable Isar
alternatives.
Precisely :-)
Regarding subst_tac, the upcoming Eisbach will have a few language mechanisms that should make it easier to treat name bindings more nicely and naturally (and to further reduce long apply scripts). It’s not quite there yet, but Dan is working on it.
Cheers,
Gerwin
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Apr 24 2024 at 12:33 UTC