Email Gateway (Aug 22 2022 at 09:20): Email Gateway (Aug 22 2022 at 09:20):From: Lars Hupel <hupel@in.tum.de>
I have an introduction rule which has a lot of premises. These premises
also have some assumptions. It is very tedious to fix all the variables
and assume all the assumptions over and over again, so I decided to
investigate whether I can leverage Isar's 'case' notation for proofs
using this rule.
My first attempt was to start my proof like this:
lemmas irule_cases = irulesI[case_names a b c d e]
proof (cases rule: irule_cases)
This works out almost as I expected. I can write down
case a
show ...
...
next
case b
show ...
However, the schematic variable '?case' does not exist. In other
situations, I can just use 'show ?thesis', but this is not applicable here.
Strangely enough, this is what 'print_cases' prints:
cases:
a:
let "?case" = "is_fmap ?rs"
But the variable is just not there, which can be confirmed via
'Query/Print Context'.
I've browsed through the Isar reference and found the attribute
'case_conclusion':
lemmas irule_cases =
irulesI[case_names a b c d e,
case_conclusion a foo, ...]
Now, 'print_cases' claims that '?foo' exists, but it doesn't.
Now, if I change the initial proof step to use 'induct' instead of
'cases', I get the '?case' variable. However, I would argue, that using
'induct' for this situation feels even more unnatural than using 'cases'.
In §6.6.1 of the Isar reference, it is stated about the 'case' command
that "Term bindings may be covered as well, notably ?case for the main
conclusion." I haven't found anything about when exactly '?case' is
present or absent.
Cheers
Lars
Email Gateway (Aug 22 2022 at 09:20):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Lars,
I don't know the design choices for cases, as I have not implemented them, but here are my
comments: cases assumes that you give it a conventional case analysis rules. These rules
do not change the conclusion, so cases has some point in not providing any term
abbreviations for the conclusions. Anyway, you are trying to use sophisticated proof
methods just to benefit from a certain side effect. I used to do that regularly, too (and
sometimes still do, but much less).
I guess that it should be fairly easy to implement your own method that does nothing but
applying a rule and setting up the cases. The infrastructure should be all there.
Andreas
Email Gateway (Aug 22 2022 at 09:20):From: Lars Noschinski <noschinl@in.tum.de>
After looking at the code a bit I was wondering, how the cases method
manages to not declare the term bindings -- the term bindings are
present in the cases and I could not find an obvious flag or similar
which would hide the term bindings.
Does anybody know how this is achieved?
-- Lars
Email Gateway (Aug 22 2022 at 09:20):From: Makarius <makarius@sketis.net>
Indeed. Proof methods can always produce cases as they see fit, cf.
existing uses of METHOD_CASES and type cases_tactic. These things have
been slightly tuned and cleaned up for Isabelle2015, as part of the
integration of Eisbach.
Nonetheless, proof method definitions with cases are rare in practice.
It requires some care and sometimes technical tricks to get material from
the internal goal state into the proof text, without breaking down normal
Isar principles of proof composition.
One example that is not from the "cases" and "induct" family is
"eventually_elim" in ~~/src/HOL/Filter.thy (in Isabelle2015-RC1). It uses
some basic tools to compose cases from module Rule_Cases, which is also
the basis for the other cases methods.
Makarius
Email Gateway (Aug 22 2022 at 09:20):From: Makarius <makarius@sketis.net>
Things really happen in ~~/src/Pure/Isar/proof_context.ML at his point:
fun case_result c ctxt =
let
val Rule_Cases.Case {fixes, ...} = c;
val (ts, ctxt') = ctxt |> fold_map fix fixes;
val Rule_Cases.Case {assumes, binds, cases, ...} = Rule_Cases.apply ts c;
in
ctxt'
|> bind_terms (map drop_schematic binds)
|> update_cases true (map (apsnd SOME) cases)
|> pair (assumes, (binds, cases))
end;
val apply_case = apfst fst oo case_result;
Later on in proof.ML, apply_case is turned into Proof.invoke_case, which
is the Isabelle/ML definition of the Isar command 'case'.
The drop_schematic above drops term bindings that happen to contain
left-over schematic variables, i.e. have not been properly determined by
other means (further instantiation by the proof method etc.).
It is a classic Isar principle that proof text (and cases are part of
that) cannot be schematic. When implementing these things about 15 years
ago, I kept it rather simple by leaving schematic parts for informative
purposes until the last moment. Something similar happens for schematic
type variables, e.g. due to hidden polymorphism.
So instead of halting and catching fire due to schematic variables
somewhere, things only fail late for situations where the user insists to
make use of uninstantiated proof context elements. Note that the user may
also choose to ignore the debatable case definitions, and proceed by other
means.
Today, we have higher ambitions in comfort (also IDE support). I am
trying to revisit all this for some years already, but again did not
manage for Isabelle2015.
Makarius
Email Gateway (Aug 22 2022 at 09:21):From: Lars Noschinski <noschinl@in.tum.de>
On 22.04.2015 14:54, Makarius wrote:
On Wed, 22 Apr 2015, Lars Noschinski wrote:
After looking at the code a bit I was wondering, how the cases method
manages to not declare the term bindings -- the term bindings are
present in the cases and I could not find an obvious flag or similar
which would hide the term bindings.Things really happen in ~~/src/Pure/Isar/proof_context.ML at his point:
fun case_result c ctxt =
let
val Rule_Cases.Case {fixes, ...} = c;
val (ts, ctxt') = ctxt |> fold_map fix fixes;
val Rule_Cases.Case {assumes, binds, cases, ...} =
Rule_Cases.apply ts c;
in
ctxt'
|> bind_terms (map drop_schematic binds)
|> update_cases true (map (apsnd SOME) cases)
|> pair (assumes, (binds, cases))
end;val apply_case = apfst fst oo case_result;
[...]
The drop_schematic above drops term bindings that happen to contain
left-over schematic variables, i.e. have not been properly determined
by other means (further instantiation by the proof method etc.).
Oh, so that's indeed done by this mechanism. Thanks for the explanation.
(I was sure I had constructed a situation where "cases" produced
non-schematic bindings before, but was apparently not careful enough).
-- Lars
Email Gateway (Aug 22 2022 at 09:21):From: Lars Hupel <hupel@in.tum.de>
The problem is that the 'cases' method doesn't instantiate the rule
before setting up the cases, as opposed to what 'induct' does. If I write
proof (cases rule: foo[where ...])
I get the '?case' bindings.
I completely understand why Isar text can't be schematic, which is why
I'm wondering whether the 'cases' method can be changed to perform
matching before setting up the cases.
Cheers
Lars
Last updated: Nov 21 2024 at 12:39 UTC