Email Gateway (Aug 22 2022 at 09:52): Email Gateway (Aug 22 2022 at 09:52):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Isar experts,
I am looking for a counterpart to schematic_lemma which I can use inside proof blocks.
With schematic_lemma, one can construct parts of the lemma statement by careful
application of rules. I am now looking for something similar that could be used inside a
proof.
Here's a simplified example. I have a predicate foo :: "exp => nat => bool" which is
closed under increasing the second argument.
lemma foo_mono: "foo exp k ==> k <= m ==> foo exp m"
For the various constants of type exp, I have a bunch of syntax-directed rules that allow
me to "compute" a number from the syntactic structure of exp. I am currently using this as
follows:
schematic_lemma l: "foo a_very_large_expression ?k"
apply(rule syntactic_analysis_rules)+
done
However, the structure of the computed l is pretty ugly. I'd like the lemma to actually be
something of the following form. Of course, this is easy to derive.
lemma "foo a_very_large_expression (245 * x + 7 * y + 3)"
apply(rule l[THEN foo_mono])
apply simp
done
Now, I'm trying to write the two lemmas in one:
lemma "foo a_very_large_expression (245 * x + 7 * y + 3)"
proof -
have "foo a_very_large_expression ?k" by(rule syntactic_analysis_rules)+
thus ?thesis by(rule foo_mono) simp
qed
Unfortunately, I cannot write ?k like that here. My feeling is that this should somehow be
doable with guess, but I have not managed to get there. Is my intuition correct? Has
anyone done this already where I can have glimpse at?
Best,
Andreas
Email Gateway (Aug 22 2022 at 09:52):From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Andreas,
Well you can not state it in a Isar proof, but with apply you can
generate such subgoals:
notepad
begin
have "foo a_very_large_expression (245 * x + 7 * y + 3)"
apply (rule foo_mono)
apply (rule syntactic_analysis_rules)+ []
apply simp
done
end
(This is how usually derivative_eq_intros is applied.)
Of course this gets complicated when (rule syntactic_analysis_rules)+ is
more difficult...
An alternative may be to use contexts?
Email Gateway (Aug 22 2022 at 09:52):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Johannes,
Thanks, I know too well how to generate such goals in apply style. Meanwhile, I found out
how to do it in forward-reasoning style with guess inside a proof block.
lemma start: "[| TERM x; foo x m; foo x m ==> thesis |] ==> thesis" by assumption
notepad begin
have "TERM a_very_large_expression" by(simp add: term_def)
then guess by(rule start)(rule syntactic_analysis_rules)+
then have "foo a_very_large_expression (245 * x + 7 * y + 3)" by(rule foo_mono) simp
end
Of course, the computation performed by the syntactic_analysis_rules cannot be written in
Isar, but that's fine. The TERM expression is only needed to instantiate the expression in
the start rule. By slightly changing the start rule, I can even obtain an abbreviation for
the compound term as an equation during the guess step (without ever having to write it
down :-) ).
Best,
Andreas
PS: Contexts are of not much help here. I can use them to hide the name of the schematic
lemma and factor out additional assumptions, but that's about it.
Email Gateway (Aug 22 2022 at 10:13):From: Makarius <makarius@sketis.net>
Does it mean everything works out, or are there pending questions?
Almost arbitrary tricks may be played. The standard Isar policies merely
try to make non-sense hard.
BTW, the canonical proof for "TERM x" is "." -- is is considered vacuous
within Isabelle/Pure.
Makarius
Email Gateway (Aug 22 2022 at 10:26):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Makarius,
No, this seems to serve my purposes, although I would prefer not having to add the TERM
marker manually.
Andreas
Last updated: Apr 24 2024 at 04:17 UTC