[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,
-john


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. *}
definition
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"

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


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

definition
   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 .
qed






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