[isabelle] Defining infinite streams recursively


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.


theory fun_let
imports Main

-- "Represent infinite streams as nat-indexed functions"
types 'a strm = "nat => 'a"

-- "Appends a finite list of elements to the front of a stream"
   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. *}

   foo_1 :: "nat strm" where
  "foo_1 i = (strm_append [1] foo_1) i"

   foo_2 :: "nat strm" where
  "foo_2 i = ((let q = (0::nat) in strm_append [1] foo_2) i)"


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.