Email Gateway (Aug 22 2022 at 15:25): Email Gateway (Aug 22 2022 at 15:25):From: Johan Meier <johan.meier.1@gmail.com>
Hi I have multiple (small and probably naive) questions
First question: can I insert a theorem/fact "literally" into the local
facts(something like HOL.simp_thms(n)) ? (i.e. with something like
back-quotes or with \open \close, like when you reference a local fact
literally)? Or at least more meaningful than for example "note
HOL.simp_thms(4)" ( I'm fine with let's say append_Cons, but
HOL.simp_thms(i) isn't a very meaningful name. Another thing that bothers
me is that HOL.simp_thms could change and, as an example, HOL.simp_thms(7)
isn't the same as before ).
Second question:
In a proof only using apply (i.e. an apply script), when a goal has
assumptions written like this : "asm1 ==> asm2 ==> conclusion"(which often
appears when proving by induction as an intermediate goal), how can I
directly access/use them? Is there something like a literal access like
there is for local facts with back-quotes or "< >"? Or is there a way to
add these assumptions to "assms"? In general, I want to use them in
situations where I have to reference a fact, but with subst in particular.
I know of hypsubst in combination with rot_tac (in case there are more
valid equalities for substitution ) , but it feels a bit awkward ... but
maybe that's just me ... "simp only" sometime does more than what is
specified after "only" (i.e. trivial simplifications) and using "erule
subst" only substitutes in the conclusion.
Just to clarify: I want to use subst instead of simp/auto etc for learning
purposes, that's all.
Third question:
what are the the differences between subst and rewrite (from
"~~/src/HOL/Library/Rewrite")? Is there any documentation on that ? Or can
someone give an example what rewrite can do more than subst ?
Final question: can I tell hypsubst to replace only in the nth position
(i.e. when there is more than one place one can substitute) ? And is it
possible to tell hypsubst to read an equality instead of "a = b" as "b =
a" ?
Thank you in advance!
Email Gateway (Aug 22 2022 at 15:26):From: Lars Hupel <hupel@in.tum.de>
Hi Johan,
First question: can I insert a theorem/fact "literally" into the local
facts(something like HOL.simp_thms(n)) ? (i.e. with something like
back-quotes or with \open \close, like when you reference a local fact
literally)? Or at least more meaningful than for example "note
HOL.simp_thms(4)" ( I'm fine with let's say append_Cons, but
HOL.simp_thms(i) isn't a very meaningful name. Another thing that bothers
me is that HOL.simp_thms could change and, as an example, HOL.simp_thms(7)
isn't the same as before ).
there are multiple possibilities here.
If you're in an "apply" script, you can write
using thm
apply -
This will add the theorem as a premise to the goal state.
If you don't want to refer to it by name, you have little choices. The
closest is "subgoal_tac". It takes a proposition and inserts it into the
goal state. However, you'll get a new goal and have to justify that
proposition. If it's in fact something out of "HOL.simp_thms", that'll
go through with "simp".
Unfortunately, the cartouche (open/close) syntax doesn't work for
anything that is not a fact. That would require combing through the
whole theorem name space, which may be rather slow.
But you might be also interested in "solve_direct", which is a command
that does just that. It presents you all theorems that can solve the
current goal. But in the end, you'll have to refer to the theorem by name.
In most cases, names are rather stable, except for maybe these "theorem
grab bags". I would strongly advise against using "HOL.simp_thms" if you
can avoid it. My usual approach is:
show P
apply simp
Look at the subgoal, call it P'
Second question:
In a proof only using apply (i.e. an apply script), when a goal has
assumptions written like this : "asm1 ==> asm2 ==> conclusion"(which often
appears when proving by induction as an intermediate goal), how can I
directly access/use them? Is there something like a literal access like
there is for local facts with back-quotes or "< >"?
You can use the "subgoal" command. See §7.2, "Subgoal structure" in the
Isar reference manual. There are also some examples that illustrate usage.
Third question:
what are the the differences between subst and rewrite (from
"~~/src/HOL/Library/Rewrite")? Is there any documentation on that ? Or can
someone give an example what rewrite can do more than subst ?
"rewrite" supports a sophisticated matching language that allows you to
specify where in a term you want to rewrite. "subst" only supports
"assumption" or "conclusion" and a numeric index. As far as I
understand, "rewrite" is strictly more powerful than "subst".
However, "rewrite" doesn't seem to be document in the reference manual
so far. But there are some examples:
<https://isabelle.in.tum.de/dist/library/HOL/HOL-ex/Rewrite_Examples.html>
Cheers
Lars
Last updated: Nov 21 2024 at 12:39 UTC