header {* Iterators over Lists *}
theory ListIterator
imports Main
begin
subsection {* Left folding *}
fun foldli where
"foldli [] c f σ = σ"
| "foldli (x#xs) c f σ =
(if c σ then foldli xs c f (f x σ) else σ)"
lemma foldli_not_cond [simp] :
"¬(c σ) ==>foldli xs c f σ = σ"
by (cases xs, simp_all)
lemma foldli_cong [fundef_cong]:
assumes "l = l'" "σ = σ'" "c = c'"
and ff': "!!σ x. [| x ∈ set l'; c' σ |] ==> f x σ = f' x σ"
shows "foldli l c f σ = foldli l' c' f' σ'"
unfolding assms using ff'
by(induct l' arbitrary: σ') auto
text {* Notice that @{term foldli} is a generalisation of folding that respects the abortion condition. *}
lemma foldli_foldl :
"foldli xs (λ_. True) f σ = foldl (λσ x. f x σ) σ xs"
by (induct xs arbitrary: σ) simp_all
lemma foldli_append :
"foldli (xs1 @ xs2) c f σ =
foldli xs2 c f (foldli xs1 c f σ)"
by (induct xs1 arbitrary: σ, simp_all)
lemma foldli_concat :
"foldli (concat xs) c f σ =
foldli xs c (λx. foldli x c f) σ"
by (induct xs arbitrary: σ, simp_all add: foldli_append)
lemma foldli_map :
"foldli (map f1 xs) c f2 σ =
foldli xs c (f2 o f1) σ"
by (induct xs arbitrary: σ, simp_all)
lemma foldli_snoc :
"foldli (xs @ [x]) c f σ =
(if c (foldli xs c f σ) then
f x (foldli xs c f σ) else (foldli xs c f σ))"
by (induct xs arbitrary: σ, simp_all)
subsection {* right fold *}
definition foldri :: "'x list => ('σ => bool) => ('x => 'σ => 'σ) => 'σ => 'σ" where
"foldri l = foldli (rev l)"
lemma foldri_simp[simp] :
"foldri [] c f σ = σ"
"foldri (l@[x]) c f σ = (if c σ then foldri l c f (f x σ) else σ)"
unfolding foldri_def by simp_all
lemma foldri_simp_Cons[simp] :
"foldri (x # l) c f σ = (if (c (foldri l c f σ)) then f x (foldri l c f σ) else (foldri l c f σ))"
unfolding foldri_def by (simp add: foldli_append)
lemma foldri_code[code] :
"foldri [] c f σ = σ"
"foldri (x # l) c f σ = (let σ' = foldri l c f σ in if c σ' then f x σ' else σ')"
by simp_all
lemma foldri_not_cond [simp] :
"¬(c σ) ==>foldri xs c f σ = σ"
unfolding foldri_def by simp
lemma foldri_cong [fundef_cong]:
assumes "l = l'" "σ = σ'" "c = c'"
and ff': "!!σ x. [| x ∈ set l'; c' σ |] ==> f x σ = f' x σ"
shows "foldri l c f σ = foldri l' c' f' σ'"
unfolding assms using ff'
by(induct l' arbitrary: σ') auto
text {* Notice that @{term foldli} is a generalisation of folding that respects the abortion condition. *}
lemma foldri_foldr :
"foldri xs (λ_. True) f σ = foldr (λx σ. f x σ) xs σ"
by (induct xs arbitrary: σ) simp_all
lemma foldri_append :
"foldri (xs1 @ xs2) c f σ =
foldri xs1 c f (foldri xs2 c f σ)"
unfolding foldri_def
by (simp add: foldli_append)
lemma foldri_concat :
"foldri (concat xs) c f σ =
foldri xs c (λx. foldri x c f) σ"
unfolding foldri_def
by (simp add: rev_concat foldli_concat foldli_map o_def)
lemma foldri_map :
"foldri (map f1 xs) c f2 σ =
foldri xs c (f2 o f1) σ"
unfolding foldri_def
by (simp add: rev_map foldli_map)
end