[isabelle] Defining finite list functions recursively

I'm having problems proving termination of the well-founded recursive function xs_strm defined below, and other functions like it.

The termination measure is just less_than, and I've installed appropriate congruence rules. However, the function package generates an unprovable termination condition.

On the other hand, I have been able to manually prove the identical function xs_strm2 below is well-founded by defining it in terms of the wfrec combinator and manually applying the congruence rules. Below are the definitions and lemmas needed to show the problem.

Thanks in advance,

section "Auxiliary function and lemma"

text {*Coerces a finite prefix of an infinite stream (represented as a @{typ "nat \<Rightarrow> 'a"} function) into a finite list. *}
strm_to_list :: "nat \<Rightarrow> (nat \<Rightarrow> 'a) \<Rightarrow> 'a list" where
 "strm_to_list n f = map f [0..<n]"

lemma length_strm_to_list[simp]:
  "length (strm_to_list n f) = n"
by (simp add: strm_to_list_def)

section {* Congruence rules for proving termination of @{term "xs_strm"} below. *}

lemma nth_cons_cong[fundef_cong]:
  "\<lbrakk>i = i';
    i' = 0 \<Longrightarrow> x = x';
\<And>j. i = Suc j \<Longrightarrow> xs ! j = xs' ! j\<rbrakk> \<Longrightarrow>
   (x # xs) ! i = (x' # xs') ! i'"
by (cases i, auto)

lemma nth_out_of_bounds:
  "length xs \<le> n \<Longrightarrow> xs ! n = [] ! (n - length xs)"
apply (induct xs arbitrary: n, auto simp add: nth_list_def)
by (case_tac n, auto)

lemma nth_take_cong[fundef_cong]:
  assumes "i = i'"
      and "n = n'"
      and "i' < n' \<Longrightarrow> xs ! i' = xs' ! i'"
      and "length xs = length xs'"
  shows "(take n xs) ! i = (take n' xs') ! i'"
  (is "?lhs = ?rhs")
using prems apply (cases "i' < n'", auto)
apply (subst nth_out_of_bounds, auto)
by (subst (2) nth_out_of_bounds, auto)

lemma nth_strm_to_list_cong[fundef_cong]:
  "\<lbrakk>n = n';
    i = i';
    i < n \<Longrightarrow> f i' = f' i'\<rbrakk> \<Longrightarrow>
   strm_to_list n f ! i = strm_to_list n' f' ! i'"
apply (simp add: strm_to_list_def)
apply (cases "i' < n'", auto)
apply (subst nth_out_of_bounds, auto)
by (subst (2) nth_out_of_bounds, auto)

section "An unsuccessful attempt to prove termination of the
well-founded function @{term xs_strm} below"

   xs_strm :: "nat \<Rightarrow> nat" where
  "xs_strm i
   = (0 # take 2 (strm_to_list 3 xs_strm)) ! i"
by pat_completeness auto
  apply (relation less_than)
  apply auto
  -- "I am left with an unprovable termination condition"

section "Manually applying congruence rules to prove termination of the
identical function @{term xs_strm2}"

   xs_strm2 :: "nat \<Rightarrow> nat" where
"xs_strm2 = wfrec less_than (\<lambda>R i. (0 # take 2 (strm_to_list 3 R)) ! i)"

lemma def_xs_strm2:
  "xs_strm2 i = (0 # take 2 (strm_to_list 3 xs_strm2)) ! i"
  (is "?lhs = ?rhs")
proof -
  let "?H R i" = "((0::nat) # take 2 (strm_to_list 3 R)) ! i"
  from wfrec[OF wf_less_than, where H="?H" and a=i] xs_strm2_def
  have "?lhs = ?H (cut xs_strm2 less_than i) i" by simp
  also have "\<dots> = ?rhs"
    -- "Manually applying congruence rules here"
    apply (subst nth_cons_cong, simp_all)
    apply (subst nth_take_cong, simp_all)
    apply (subst nth_strm_to_list_cong, simp_all)
    by (simp add: cut_apply)
  finally show ?thesis .

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