Theory Automatic_Refinement.Foldi

(*  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