Email Gateway (Aug 18 2022 at 11:58): Email Gateway (Aug 18 2022 at 11:58):From: John Matthews <matthews@galois.com>
Hello,
We've run into a problem in having Isabelle automatically prove the
termination of Cryptol infinite streams that we are translating into
Isabelle, when the body of the stream definition uses a let-
expression. Below is a theory that illustrates the problem.
Thanks,
-john
theory fun_let
imports Main
begin
-- "Represent infinite streams as nat-indexed functions"
types 'a strm = "nat => 'a"
-- "Appends a finite list of elements to the front of a stream"
definition
strm_append :: "'a list => 'a strm => 'a strm" where
"strm_append xs ys
= (%n. let l = length xs
in (if n < l then xs ! n else ys (n - l)))"
lemma strm_append_cong[fundef_cong]:
"[| n = n';
xs = xs';
!!k. n = k + length xs ==> ys k = ys' k|]
==> (strm_append xs ys) n = (strm_append xs' ys') n'"
by (cases n', simp_all add: strm_append_def Let_def)
text {* "fun" can automatically prove termination of foo_1, but
not foo_2, even though the only difference between the two is a
let expression. *}
fun
foo_1 :: "nat strm" where
"foo_1 i = (strm_append [1] foo_1) i"
fun
foo_2 :: "nat strm" where
"foo_2 i = ((let q = (0::nat) in strm_append [1] foo_2) i)"
end
Email Gateway (Aug 18 2022 at 11:58):From: Alexander Krauss <krauss@in.tum.de>
Hi John,
\begin{blackmagic}
Here is the rule you need:
lemma let_app_cong[fundef_cong]:
"s = t ==>
(!!a. a = t ==> f a y = g a y)
==> x = y
==> Let s f x = Let t g y"
by auto
\end{blackmagic}
Note how the extra argument y is moved "into" the let.
Alex
Email Gateway (Aug 18 2022 at 12:00):From: John Matthews <matthews@galois.com>
Thanks Alex, I forgot that I also needed to eta-expand the body of the
let-expression.
-john
Last updated: Nov 21 2024 at 12:39 UTC