theory SumIntOption
imports Main
begin

function  sumO:: "int \<Rightarrow> int \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int option" where
"sumO  l l f = Some (f l)" |
"n < m \<Longrightarrow> sumO n m f =  (case sumO n (m - 1) f of 
          None \<Rightarrow> None | Some v \<Rightarrow> Some ((f m) + v))"|
"n>m \<Longrightarrow> sumO n m f = None"
by (atomize_elim, auto)
termination sumO
by (relation "measure (\<lambda>(l,u,f). nat ((u+1) - l))")  auto



theorem 
  fixes u::int and l::int
  assumes "l\<le>u"
  shows "sumO l u f = Some (\<Sum> k=l..u. f k)" (is "?P u")
  using assms
    proof (induct u rule: int_ge_induct) 
      show "?P l" by simp
    next
      fix i::int
      assume "l\<le>i" and "?P i"
      show "?P (i+1)"
      proof -
        from `?P i` have "sumO l (i+1) f = Some (f (i+1) + (\<Sum> k=l..i. f k))"
          using `l\<le>i` by simp
        also have "f (i+1) + (\<Sum> k=l..i. f k) = (\<Sum> k=l..i+1. f k)"
        proof -
          have "{l..i+1} = insert (i+1) {l..i}" using `l\<le>i` by auto
          thus ?thesis by simp
        qed
        finally show ?thesis by auto
      qed
    qed

end