Email Gateway (Aug 22 2022 at 19:02): Email Gateway (Aug 22 2022 at 19:02):From: Makarius <makarius@sketis.net>
Maybe you mean literal fact notation (with old-style ASCII back-quotes)
or new-style cartouche syntax.
It allows to project (unique) facts from the current proof context by
giving a term pattern (most users might think they need to give the full
term).
Alternatively, you can study documentation and examples for proof method
"goal_cases" or the command "subgoal". This is moving towards "improper
Isar", but in some applications it is adequate.
Makarius
Email Gateway (Aug 22 2022 at 19:03):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
I actually mean the opposite: the backquote/cartouche notation turns a
term (pattern) into a fact, but I want to turn a fact into a term, so
that I can write something like the following (with «...» being my
temporary notation for the desired conversion):
let "?x + ?y ≤ ?z" = «assms(1)»
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 19:03):From: Makarius <makarius@sketis.net>
This is in conflict with how Isar works: the proof text is turned into
assumptions/goals/facts, but the information flows only forwards in that
direction, not backwards. A fact is somehow opaque to the proof text and
cannot be inspected directly.
The ?case abbreviation of the "induct" family gives the appearance to
allow this, but it is conceptually still the original text statement
that is exposed as term here. (As usual Isar allows a certain degree of
improper use, so this can be stretched a bit further than officially
intended.)
There are other tools to get hold of low-level information, e.g. the
proof method "goal_cases", the command "subgoal", and the Eisbach proof
method "match". All of this is subject to restrictions: proper proof
structure emerges from taking away arbitrary access to internal proof
state information (goals and facts).
Makarius
Email Gateway (Aug 22 2022 at 19:04):From: Dominique Unruh <unruh@ut.ee>
Hi,
my solution is to create a new command letfact, so that you can write, e.g.,
letfact "_ = ?rhs" = Cons
(if Cons is the name of a fact).
The theory that defines this is attached.
I have not tested it besides what is in that theory, so it might be very
buggy (or not work at all).
Also, I don't know if I am doing something unspeakable to Isabelle's
interna here. But I assume Makarius will speak up if I do. :)
Best wishes,
Dominique.
Scratch.thy
Email Gateway (Aug 22 2022 at 19:05):From: Makarius <makarius@sketis.net>
Well, I have already explained that facts (and goals) are conceptually
opaque from the Isar proof text.
Isar proof structure (with its overall benefits of readability and
maintainability) emerges from taking away arbitrary access to internal
state. It has required many years to achieve a certain balance: I have
even refined and revised it in 2015/2016.
Instead of introducing non-Isar commands in Isar, it is better to look
at the concrete applications and find a style of proof that fits to the
high cultural standards of Isar.
Makarius
Email Gateway (Aug 22 2022 at 19:05):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
I think I’ve found such a style for my particular problem, which was
accessing an induction hypothesis and subsequently parts of it as terms.
Consider the following small example:
lemma "(n :: nat) < 2 * n" (is "?P n")
proof (induction n)
case (Suc m)
let "_ < ?double" = "?P m"
oops
The construct (is "?P n") in the first line defines ?P to be the
“shape” of the statement. The ?P m in the let statement further
down is the induction hypothesis (and ?P (Suc m) would be the same as
?case. So I’m effectively using higher-order unification to replace
the ns in the lemma statement with a locally available term. The let
statement then assigns the right-hand side of the induction hypothesis
(2 * m) to the variable ?double, showing that I can turn parts of
the induction hypothesis into terms.
All the best,
Wolfgang
Email Gateway (Aug 22 2022 at 19:05):From: Makarius <makarius@sketis.net>
Great. This is exactly how it was meant to be in classic Isabelle/Isar,
before various add-on were introduced over the years.
The general principle: you write text (terms) and match against it (via
term patterns) -- before mechanical proof tools operate on your terms.
Makarius
Email Gateway (Aug 22 2022 at 19:15):From: Wolfgang Jeltsch <wolfgang-it@jeltsch.info>
Hi!
Say I have a proof method that generates several cases. For each case,
I can access parts of the conclusion via schematic variables. All I have
to do is defining those variables by matching the ?case variable
against a pattern, for example like so:
let "?x + ?y ≤ ?z" = ?case
Now I’d like to do the same thing for case premises. The problem is that
there don’t seem to be analogs of ?case for the premises. That said,
premises can be referred to as facts, of course. Is it possible to get
the statement of a fact as a term, or is there some other way to achieve
what I want?
All the best,
Wolfgang
Last updated: Apr 18 2024 at 20:16 UTC