section {* Interuptible Fold *}
theory Foldi
imports Main
begin
subsection {* Left folding *}
primrec 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 ∘ 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)
lemma foldli_snoc_id[simp]: "foldli l (λ_. True) (λx l. l@[x]) l0 = l0@l"
by (induct l arbitrary: l0) (auto)
lemma foldli_foldli_prod_conv:
"foldli l2 ctd (λi. foldli l1 ctd (f i)) s = foldli (List.product l2 l1) ctd (λ(i,j). f i j) s"
(is "?lhs=?rhs")
proof -
have [simp]: "foldli (map (Pair a) l) ctd (λ(x, y). f x y) s = foldli l ctd (f a) s"
for a l s
apply (induction l arbitrary: s)
by (auto simp:)
show ?thesis
by (induction l2 arbitrary: l1 s) (auto simp: foldli_append)
qed
lemma fold_fold_prod_conv: "fold (λi. fold (f i) l1) l2 s = fold (λ(i,j). f i j) (List.product l2 l1) s"
using foldli_foldli_prod_conv[of l2 "λ_. True" l1 f s]
by (simp add: foldli_foldl foldl_conv_fold)
subsection {* Right folding *}
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 ∘ f1) σ"
unfolding foldri_def
by (simp add: rev_map foldli_map)
lemma foldri_cons_id[simp]: "foldri l (λ_. True) (λx l. x#l) [] = l"
by (induct l) (auto)
end