Email Gateway (Aug 18 2022 at 14:38): Email Gateway (Aug 18 2022 at 14:38):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,
I'm curious whether it is (easily) possible to apply elimination rules
in Isabelle that
eliminate more than one premise.
There is a consumes-flag for cases rules, however, simply doing:
lemma AB_elim[consumes 2]: "[| A; B; Foo => thesis |] ==> thesis"
lemma "[| A; B; C |] ==> Foo"
apply (cases rule: AB_elim)
does not work, and leaves me with three subgoals, the last one being:
[|A; B; C; Foo |] ==> Foo
apply (erule (1) AB_elim) leaves me with one subgoal being:
[| B; C; Foo |] ==> Foo
However, I want something that yields the subgoal:
[| C; Foo |] ==> Foo
and that also works if the A and B are not in order, i.e. for
[| ...; B; ...; A; ... |] ==> Foo
apply (?? AB_elim) shall yield:
[| ...; ...; ...; Foo |] ==> Foo
i.e. removing the matching A and B from the premises.
(I need this for termination and proper behavior of a set of elimination
rules that I apply exhaustively with apply (...)+ ):
Regards and thanks for any hints,
Peter
Email Gateway (Aug 18 2022 at 14:38):From: Brian Huffman <brianh@cs.pdx.edu>
On Thu, Feb 25, 2010 at 10:04 AM, Peter Lammich
<peter.lammich@uni-muenster.de> wrote:
Hi all,
I'm curious whether it is (easily) possible to apply elimination rules in
Isabelle that
eliminate more than one premise.There is a consumes-flag for cases rules, however, simply doing:
lemma AB_elim[consumes 2]: "[| A; B; Foo => thesis |] ==> thesis"
lemma "[| A; B; C |] ==> Foo"
apply (cases rule: AB_elim)does not work, and leaves me with three subgoals, the last one being:
[|A; B; C; Foo |] ==> Fooapply (erule (1) AB_elim) leaves me with one subgoal being:
[| B; C; Foo |] ==> FooHowever, I want something that yields the subgoal:
[| C; Foo |] ==> Foo
Hi Peter,
The "consumes" attribute only has an effect when you are in an
Isar-style proof with chained facts. Here's a situation where it works
as you expect:
lemma "[|A; B; C|] ==> Foo"
proof -
assume "A" and "B" and "C"
then show "Foo"
(* there are now 3 chained facts: "A", "B", "C" *)
apply (cases rule: AB_elim)
Now the first 2 chained facts are matched with rule AB_elim and
disappear. The remaining fact "C" stays in the remaining subgoal,
leaving "[| C; Foo |] ==> Foo".
and that also works if the A and B are not in order, i.e. for
[| ...; B; ...; A; ... |] ==> Foo
apply (?? AB_elim) shall yield:
[| ...; ...; ...; Foo |] ==> Foo
i.e. removing the matching A and B from the premises.
Unfortunately, chained facts can only be matched in the given order
(for efficiency reasons, I believe), so this doesn't really do what
you want.
(I need this for termination and proper behavior of a set of elimination
rules that I apply exhaustively with apply (...)+ ):Regards and thanks for any hints,
Peter
I don't think there is any easy way to accomplish what you want to
do---at least, I don't know of any already-implemented tactic in
Isabelle that does this. I do think such a tactic would be useful,
though; I've wished for it a few times myself.
It might be possible to implement such a tactic in ML. The obvious
approach of trying to generalize eresolve_tac probably won't work,
because eresolve_tac is implemented in terms of Thm.biresolution,
which is part of Isabelle's trusted kernel.
You could probably define this tactic on top of eresolve_tac:
Basically you would do "erule (n)" (which is basically "erule" then
"assumption" n times) followed by n calls to "thin_tac" to eliminate
the extra assumptions from the final proof state. The tricky bit would
be to figure out how to record which assumptions were matched by
"assumption", so you can tell "thin_tac" which ones to get rid of
later.
Unfortunately, most of the development effort now is focused on
Isar-style proofs with chained facts, and not so much on tactics for
apply-style proofs. So I'd say it is unlikely that this feature will
be implemented by the main Isabelle development team. But be sure to
report back if you try to implement this yourself; I'm sure plenty of
people would find it useful.
Email Gateway (Aug 18 2022 at 14:39):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Brian Huffman wrote:
On Thu, Feb 25, 2010 at 10:04 AM, Peter Lammich
<peter.lammich@uni-muenster.de> wrote:Hi all,
I'm curious whether it is (easily) possible to apply elimination rules in
Isabelle that
eliminate more than one premise.[...]
I don't think there is any easy way to accomplish what you want to
do---at least, I don't know of any already-implemented tactic in
Isabelle that does this. I do think such a tactic would be useful,
though; I've wished for it a few times myself.It might be possible to implement such a tactic in ML. The obvious
approach of trying to generalize eresolve_tac probably won't work,
because eresolve_tac is implemented in terms of Thm.biresolution,
which is part of Isabelle's trusted kernel.You could probably define this tactic on top of eresolve_tac:
Basically you would do "erule (n)" (which is basically "erule" then
"assumption" n times) followed by n calls to "thin_tac" to eliminate
the extra assumptions from the final proof state. The tricky bit would
be to figure out how to record which assumptions were matched by
"assumption", so you can tell "thin_tac" which ones to get rid of
later.Brian, Peter, et al,
My solution of this "tricky bit" depends on an idea presented by Konrad
Slind
for HOL at TPHOLs 2002, which was to annotate selected goals (or, more
generally, subterms) _within_ the logic.
Thus for a long time I have used
forget :: "'a => 'a"
forget_def : "forget f == f"
to stop a particular hypothesis being used in asm_simp_tac and
asm_full_simp_tac
For this problem I defined
keep_def : "keep b f == f"
keep :: "bool => 'a => 'a"
val _ = ListPair.app bind_thm (["keepD", "keepI"], [keep_def] RL defDs) ;
val _ = bind_thm ("keepTD", read_instantiate [("b", "True")] keepD) ;
val _ = bind_thm ("keepFD", read_instantiate [("b", "False")] keepD) ;
val _ = bind_thm ("keepF_thin", keepFD RS thin_rl) ;
keepTD ;
val it = "keep True ?P ==> ?P" : Thm.thm
keepFD ;
val it = "keep False ?P ==> ?P" : Thm.thm
keepF_thin ;
val it = "[| keep False ?P; PROP ?W |] ==> PROP ?W" : Thm.thm
(You should change the uses of bind_thm if you're using Isar).
Then the tactic is as follows - it is no doubt rather inefficient, but
seems to work OK.
I've done the analogue of fatac which deletes all matched premises from
remaining subgoals because it's simpler to follow (datac already deleted
the first matched premise, and eatac also matches the conclusion, which
I think is here an additional irrelevant complication).
(* fetac : thm -> int -> int -> tactic
like fatac n but also deletes hypotheses matched *)
fun fetac th n sg st =
let val fth = thin_rl RS (replicate n keepFD MRS th) : thm ;
val subgoal = List.nth (prems_of st, sg - 1) : term ;
(* turn all subgoal hypotheses H into keep ?b H *)
val nhyps = length (Logic.strip_assums_hyp subgoal) ;
val ktac = EVERY' (replicate nhyps (dtac keepI)) : int -> tactic ;
(* then apply ftac fth - see later *)
(* then apply atac n times,
which marks the hypotheses to be deleted with keep False *)
val atacs = EVERY' (replicate n atac) ;
(* treat other instances of keep ?b as keep True, and erase them *)
val ekttac = REPEAT o dtac keepTD : int -> tactic ;
(* delete hypotheses which are (keep False ...) *)
val ekftac = REPEAT o etac keepF_thin : int -> tactic ;
(* combine all the above *)
val ctac = EVERY' [ktac, ftac fth, atacs] THEN_ALL_NEW
(ekttac THEN' ekftac) : int -> tactic ;
in ctac sg st end ;
Unfortunately, most of the development effort now is focused on
Isar-style proofs with chained facts, and not so much on tactics for
apply-style proofs. So I'd say it is unlikely that this feature will
be implemented by the main Isabelle development team. But be sure to
report back if you try to implement this yourself; I'm sure plenty of
people would find it useful.I hope so. Incidentally, on a related topic - sometimes using etac I
_don't_ want the matched premise deleted from the resulting subgoals
(which is why all_dupE is given as an alternative to allE).
To achieve this for any elimination rule, I have
fun mk_dupE thE = zero_var_indexes (rotate_prems ~1
(tacsthm [PRIMITIVE (fn th => th RS cut_rl), atac 1] thE)) ;
thus mk_dupE allE is approximately all_dupE
Regards,
Jeremy
- Brian
Email Gateway (Aug 18 2022 at 14:39):From: Stephan Merz <Stephan.Merz@loria.fr>
I second this request. More precisely, I'd like to be able to annotate a rule such that it is applied by the automatic proof methods only if the first n hypotheses are present in the current proof state. As a simple example, consider bspec, which would make a perfect elimination rule when its two assumptions can be proved by assumption. As others have pointed out, it is not hard to write a tactic that applies a rule only if the first n hypotheses can be proved by assumption, however, I don't know how to make such a tactic work inside auto and friends.
Thanks,
Stephan
Email Gateway (Aug 18 2022 at 14:39):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Stephan Merz wrote:
Stephan,
This is described in Section 10.4 of the Reference Manual. (NOT the
Isar reference manual, the Isabelle Reference Manual).
For bspec, addSD2 is exactly what you want. (or maybe addD2).
Modifying the current claset (or creating a new one) is used by all the
tactics involving the classical reasoning set, eg safe_tac, clarify_tac,
auto_tac, force_tac
Jeremy
Email Gateway (Aug 18 2022 at 14:52):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi Brian,
Many thanks you for your answer.
I adopted your proposal for my needs. However, I ran into a problem that
should also be imminent in your proposal (?).
If there are premises of the form !!x. _==>_, they are counted in nhyps,
however dtac keepI will not unify against them, thus
val ktac = EVERY' (replicate nhyps (dtac keepI)) : int -> tactic ;
produces premises that are doubly-wrapped into keep.
What's the best way around?
Only counting "plain" premises? (How?)
Can keepI be defined to also wrap higher-order premises?
Best,
Peter
Jeremy Dawson schrieb:
Email Gateway (Aug 18 2022 at 14:52):From: Jeremy Dawson <jeremy@rsise.anu.edu.au>
Peter Lammich wrote:
Dear Peter,
I'm not quite sure if I understand you correctly.
Are you talking about the situation where there is a premise (among the
list of premises of a subgoal) of the form !!x. _==>_ ?
(Isn't this rather unusual - could I see an example of how this arises ?)
Certainly, keep, as I defined it, won't wrap around a premise of the form
!!x. _==>_ because such a premise is of type prop, not bool.
Isabelle generally - I think - wasn't intended to work very much with
meta-level stuff, and previously I have found that playing around with
meta-level props instead of object level bools doesn't seem to work as
expected. However to my surprise the attached does seem to work - try
it out and see if it works on your problem example.
Regards,
Jeremy
x
Email Gateway (Aug 18 2022 at 14:53):From: Peter Lammich <peter.lammich@uni-muenster.de>
Dear Peter,
I'm not quite sure if I understand you correctly.
Are you talking about the situation where there is a premise (among
the list of premises of a subgoal) of the form !!x. _==>_ ?
(Isn't this rather unusual - could I see an example of how this arises ?)
Exactly. I ran into this situation, when proving elimination rules
(e.g., on Isar, containing "obtains").
lemma foo:
assumes bla
obtains x where "bar x"
apply -
** You end up with a subgoal something like [| bla; !!x. bar x ==>
thesis |] ==> thesis
Certainly, keep, as I defined it, won't wrap around a premise of the form
!!x. _==>_ because such a premise is of type prop, not bool.
Isabelle generally - I think - wasn't intended to work very much with
meta-level stuff, and previously I have found that playing around with
meta-level props instead of object level bools doesn't seem to work as
expected. However to my surprise the attached does seem to work - try
it out and see if it works on your problem example.
Thank you very much.
I certainly will try it. (For now, I modified the val nhyps=... to only
count plain premises).
Best,
Peter
Regards,
Jeremy
Last updated: Apr 26 2024 at 08:19 UTC