(* Title: Interuptible Fold Author: Thomas Tuerk <tuerk@in.tum.de> *) 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