*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Defining finite list functions recursively*From*: John Matthews <matthews at galois.com>*Date*: Wed, 11 Jun 2008 21:46:08 -0700

Thanks in advance, -john section "Auxiliary function and lemma"

definition

"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)

lemma nth_cons_cong[fundef_cong]: "\<lbrakk>i = i'; i' = 0 \<Longrightarrow> x = x';

(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

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

**Follow-Ups**:**Re: [isabelle] Defining finite list functions recursively***From:*Alexander Krauss

- Previous by Date: Re: [isabelle] Converting fixed variables to ?-wildcards
- Next by Date: Re: [isabelle] Defining finite list functions recursively
- Previous by Thread: Re: [isabelle] Converting fixed variables to ?-wildcards
- Next by Thread: Re: [isabelle] Defining finite list functions recursively
- Cl-isabelle-users June 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list