Re: [isabelle] Reasoning with the option type



I am not very experienced, but I looked at your proof.
It seems very long, and there are lots of apparently unnecessary
assumptions that float in and out.  I came up with the attached,
which is rather shorter.  I did not see how the use of the
option type introduces any complication here.  Hopefully I did
not misunderstand something important.

						- Gene Stark


On 04/27/2015 11:55 PM, Alfio Martini wrote:
> Dear Isabelle Users,
> 
> In a previous thread (Isabelle: A logic of partial functions?) I asked
> some questions about the use of the constant "undefined" when
> dealing with partial functions, which  have to be made total according
> to the foundations of Isabelle.
> 
> The long thread about my difficulties with Sledgehammer made
> me realize that my definition was not general enough. And after
> looking into the very well written tutorial on Code Generation, I
> was convinced that I had to deal with the option type.
> 
> I'm  also very grateful to all that reply my original messages with
> many insightful and helpful observations.
> So, if some novice is interested I include here (my) proof of the
> total correctness of that sum algorithm.
> 
> I only ask the evaluation of some more experienced user, if
> this is the correct way to reason  with the option type. It looks
> a bit clumsy.
> 
> The thy file is attached. Many thanks for any remarks!
> 
> Best!
> 

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


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.