Email Gateway (Aug 19 2022 at 16:32): Email Gateway (Aug 19 2022 at 16:32):From: Lars Hupel <hupel@in.tum.de>
(My apologies for the somewhat mysterious subject line.)
I was wondering whether it'd make sense to unify the mechanisms behind
"inductive_cases", "inductive_simps", "fun_cases" etc.; namely, commands
which prove some theorems on the spot, but apart from binding them to a
name, have no further side effects on the theory.
My main motivation for this is that, sometimes, I need "ad hoc"
elimination rules, and since "inductive_cases" doesn't work in proof
blocks, I end up with the rather awkward pattern of declaring them
outside the proof and hiding them afterwards again. My initial thought
was to make a variant of the command which works in a proof block (c.f.
"lemmas" vs "note", "interpretation" vs "interpret"), but if
Isabelle/HOL doesn't need more of one things, it's keywords.
So, here's my proposal: Instead of an "inductive_cases" command, have an
"inductive_cases" attribute. It could be used like this:
lemmas fooE[elim] = [[inductive_cases "R (T x) (T y)"]]
or this:
then have "R a b"
using [[inductive_cases "R (T x) (T y)"]]
This would already work out of the box by declaring a "rule_attribute"
which ignores its incoming "thm" argument.
Is that something people would be interested in?
(NB: What follows are some technical details which would probably belong
to [isabelle-dev], but I don't want to split this thread.)
Cheers
Lars
Making my case for "inductive_cases" is easy, because I could implement
it with the existing tools, because it always proves a single theorem.
If we want to be fully general though, it gets more complicated, because
the current "attribute" mechanism doesn't allow to return more than one
theorem.
Looking at how attributes are implemented, I found this:
type attribute =
Context.generic * thm -> Context.generic option * thm option
Modifying this to return a "thm list option" would certainly allow
multiple theorems. To make it easy to use, one could create a new "smart
constructor" for that type, e.g.
val ad_hoc_proof_attribute: (Context.generic -> thm list) -> attribute
which leaves the incoming context untouched and ignores the incoming
theorem.
I couldn't predict what more needed to be changed, so I decided to
"apply some pressure and see what starts wobbling". I changed the type
in "more_thm.ML". Then, the tricky bit is "apply_attributes", which is
in some way a glorified fold left over a list of attributes. There, I
ran into a problem: suppose we have
thm _[inductive_cases "...", simp]
In this case, the first part of the attribute sequence might produce
more than theorem, which means that the second part needs to be applied
to all of them. Peter pointed out to me that we already have precendent
for that:
thm foo.intros[simp]
... works in exactly the same way: "simp" is applied to all theorems in
"foo.intros" (this is handled in "Isar/attrib.ML"). However, so far the
full "attribute pipeline" only transformed one pair of theorem and
context into another pair of theorem and context, and now it would need
to deal with potentially multiple and traverse them in some manner
(Depth first? Breadth first? That choice matters for non-commutative
attributes, e.g. [simp, simplified]).
I have attached a patch which _only_ attempts to change the definition
in "more_thm.ML" and fix what breaks in "global_theory.ML" and
"Isar/proof_context.ML" (in both files only minor changes were needed).
A bit more thought is required for "Isar/attrib.ML", where I aborted my
exploration.
patch
Email Gateway (Aug 19 2022 at 16:34):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Lars,
I understand that your proposal is more general than the proof method ind_cases, but could
you comment on how they relate to each other?
Andreas
Email Gateway (Aug 19 2022 at 16:35):From: Lars Hupel <hupel@in.tum.de>
Hi,
I understand that your proposal is more general than the proof method
ind_cases, but could you comment on how they relate to each other?
I actually didn't know about that proof method, but it looks similar.
The difference is that I would actually need to spell out the rule I
want, and then continue to prove it with that method. With my proposal,
you just get the theorem generated on the spot, without having to spell
it out. It's very nice in proofs where you obtain variables. From my
current work:
obtain x1 x2
where "x = x1 $ x2"
and "rs, compile rs ⊢ x1 ≈ t1"
and "rs, compile rs ⊢ x2 ≈ t2"
by (auto elim: [[summon_ind_cases "rs, compile rs ⊢ x ≈ t1 $$ t2"]])
I could have expressed that equally well with
inductive_cases need_to_make_up_a_name: "rs, compile rs ..."
lemma ...
proof ...
obtain ...
by (auto elim: ...)
qed
hide_fact ...
The reason why I prefer an attribute over a command is that I don't need
to make up a name for something which only makes sense in the context of
a particular proof. Here, the "compile rs" is an artifact from the lemma
I'm proving. Another reason is that I think attributes are vastly
underrated – as opposed to commands, they can be used uniformly in a lot
of different situations.
I have attached a working example of that "summon_ind_cases" attribute.
(As an aside, I realize that my handling of variables is not canonical
here; presumably, I need to parse "for" fixes as well. Grepping the
sources for occurrences of "Parse.for_fixes" didn't reveal any canonical
use cases, though.)
Cheers
Lars
Summon.thy
Email Gateway (Aug 19 2022 at 16:35):From: Lars Hupel <hupel@in.tum.de>
Lars just pointed out another candidate: "case_of_simps",
"simps_of_case". With my proposal, one could write
thm foo_case = [[case_of_simps foo.simps]]
note foo_case = [[case_of_simps foo.simps]]
instead of using the specialized command
case_of_simps foo_case: foo.simps
This attribute could be implemented right now, but not "simps_of_case",
because the latter would need to return multiple theorems.
Email Gateway (Aug 19 2022 at 16:35):From: Peter Lammich <lammich@in.tum.de>
I would appreciate an attribute [[inductive_cases <term>]] instead of
the command.
Last updated: Apr 26 2024 at 01:06 UTC