Email Gateway (Aug 19 2022 at 12:46): Email Gateway (Aug 19 2022 at 12:46):From: Christian Urban <christian.urban@kcl.ac.uk>
Dear All,
We have a question about how to deal conveniently with
Lets in Isar proofs. Some of our definitions contain many
nested lets, as in
definition
"foo f e1 e2 e3 == let (x, y) = e1; (u, v) = e2; (w, k) = e3 in f x y u v w k"
The problem is that we have foo unfolded in our premises, say
lemma
assumes "P (let (x, y) = e1; (u, v) = e2; (w, k) = e3 in f x y u v w k)"
shows "thesis"
We could prove such lemmas with
lemma
assumes "P (let (x, y) = e1; (u, v) = e2; (w, k) = e3 in f x y u v w k)"
shows "thesis"
proof -
from assms
obtain x y u v w k
where "P (f x y u v w k)" and
"(x, y) = e1" and "(u, v) = e2" and "(w, k) = e3" by ...
but we are wondering whether there is a simpler way. Essentially,
we want to avoid having to fix the variables and to avoid to write
the equations explicitly. We rather prefer the way how the cases-construction
works, which automatically fixes variables and puts such equations
into the context, for example
lemma
assumes "P (n:: nat)"
shows "thesis"
proof (cases n)
In this example you have "n = 0" in the "first" case and fix nat/n = Suc nat
in the "second" case. Is there something similar for many nested lets?
If not, how would we have to go about implementing (presumably in ML)
such a construction?
Best wishes,
Christian
Email Gateway (Aug 19 2022 at 12:46):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Christian,
I don't completely understand why this is related to let. A let just introduces an
abbreviation. However, in your example, you are more concerned with patterns such as
tuples, but
let (x, y) = e in f x y
is syntactic sugar for
Let e (prod_case (%x y. f x y))
So, do you also want to introduce variables if there's no pattern-matching involved, such
that "P (let x = e in f x)" gets transformed into "!!x. x = e ==> P (f x)"?
In principle, you can use Isabelle's splitter:
lemma Let_prod_split_asm:
"P (Let e (prod_case f)) = (~ (EX x y. (x, y) = e & ~ P (f x y)))"
by(auto simp add: Let_def prod.split_asm)
lemma Let_split_asm: "P (Let e f) = (~ (EX x. x = e & ~ P (f x)))"
by(auto simp add: Let_def)
lemma
assumes "P (let (x, y) = e1; (u, v) = e2; (w, k) = e3 in f x y u v w k)"
shows "thesis"
using assms
apply -
proof(split Let_prod_split_asm Let_split_asm)+
case (goal1 x y u v w k)
With some ML programming, it should be easy to make this more readable.
Hope this helps,
Andreas
Email Gateway (Aug 19 2022 at 12:46):From: Michael Norrish <Michael.Norrish@nicta.com.au>
You can implement a nice expansion of lets into equations with the simplifier as per Konrad Slimd's and my proof pearl paper in TPHOLs 2005
Michael
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Apr 25 2024 at 12:23 UTC