Email Gateway (Aug 18 2022 at 11:01): Email Gateway (Aug 18 2022 at 11:01):From: Dave Cunningham <dc04@doc.ic.ac.uk>
Is it possible to delete an assumption from the current subgoal? While
unnecessary, I sometimes find this useful while proving in proof general
if the list of assumptions gets too big. Maybe this makes the proof
space smaller while using the automatic methods too? I've been doing
apply(erule_tac ?x="blah" in discard_assumption)
where I've previously proved "discard_assumption" as
[| ?x ; ?y |] ==> ?y
but I'm assuming this is a bad idea. Isabelle certainly warns about it.
Is there a better way?
thanks
Email Gateway (Aug 18 2022 at 11:01):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Dave Cunningham wrote:
Dave,
I can't see why it is a bad idea, except for the fact that your
"discard_assumption"
is in fact thin_rl, already in Isabelle.
In fact the tactic thin_tac does exactly what you have done
tactic.ML:fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;
You say "Isabelle certainly warns about it" but I don't get such a
warning, what does it say?
regards,
Jeremy
Email Gateway (Aug 18 2022 at 11:02):From: Dave Cunningham <dc04@doc.ic.ac.uk>
where I've previously proved "discard_assumption" as
[| ?x ; ?y |] ==> ?y
I can't see why it is a bad idea, except for the fact that your
"discard_assumption"
is in fact thin_rl, already in Isabelle.
In fact the tactic thin_tac does exactly what you have done
tactic.ML:fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;
awesome, it seems i can just go
apply(thin_tac "blah") to make "blah" disappear from the assumptions!
You say "Isabelle certainly warns about it" but I don't get such a warning,
what does it say?
ah i just looked again and noticed i was doing (for some unknown reason):
lemma discard_assumption: "[| ?x ; ?y |] ==> ?y"
which produced the message:
[Isabelle] ### Goal statement contains unbound schematic variable(s): ?y, ?x
Which is what I was seeing as i was skipping through all my definitions
up to the main proof i'm working on.
Replacing them with x and y made it go away. However now I don't need
it anymore, anyway :)
thanks
Email Gateway (Aug 18 2022 at 11:02):From: "Mark A. Hillebrand" <mah@dfki.de>
Hi,
There is thin_tac, describe in Section 3.3.2 "Manipulating
assumptions" of the Isabelle Reference Manual (-> isatool doc ref).
Best regards,
Mark
Last updated: Nov 21 2024 at 12:39 UTC