Theory ImplHelper

(*  Title:       Tools for executable specifications
    ID:
    Author:      Peter Lammich <peter.lammich@uni-muenster.de>
    Maintainer:  Peter Lammich <peter.lammich@uni-muenster.de>
*)

section "Tools for executable specifications"

theory ImplHelper
imports Main
begin

subsection "Searching in Lists"
  
text ‹ Given a function @{term "f :: 's ⇒ 'a option"} and a list @{term "l :: 's list"}, return the result of the first element @{term "e∈set l"} with @{term "f e ≠ None"}.
  The functional code snippet @{term "first_that f l"} corresponds to the imperative code snippet: {\em for e in l do \{ if f e $\neq$ None then return Some (f e) \}; return None }
›
  
primrec first_that :: "('s ⇒ 'a option) ⇒ 's list ⇒ 'a option" where
  "first_that f [] = None"
| "first_that f (e#w) = (case f e of None ⇒ first_that f w | Some a ⇒ Some a)"

lemma first_thatE1: "first_that f l = Some a ⟹ ∃e∈set l. f e = Some a"
  apply (induct l)
  subgoal by simp
  subgoal for aa l by (cases "f aa") auto
  done

lemma first_thatE2: "first_that f l = None ⟹ ∀e∈set l. f e = None"
  apply (induct l)
  subgoal by simp
  subgoal for aa l by (cases "f aa") auto
  done
 
lemmas first_thatE = first_thatE1 first_thatE2

lemma first_thatI1: "e∈set l ∧ f e = Some a ⟹ ∃a'. first_that f l = Some a'"
  by (cases "first_that f l") (auto dest: first_thatE2)
  
lemma first_thatI2: "∀e∈set l. f e = None ⟹ first_that f l = None"
  by (cases "first_that f l") (auto dest: first_thatE1)

lemmas first_thatI = first_thatI1 first_thatI2

end