Theory Take_While_Update

theory Take_While_Update imports Tools
begin

(******************************************************************************)
section ‹Extending @{text "Take_While"} with an additional, mutable parameter›
(******************************************************************************)

text‹This theory defines takeW, holds and extract similarly to the other @{text "Take_While"} theory, but removes 
the predecessor parameter and adds a parameter to P and an update function that is applied to this parameter.
In our formalization, the additional parameter is the uinfo field and the update function is the update
on uinfo fields.›

locale TWu =
  fixes P :: "('b ⇒ 'a ⇒ 'a option ⇒ bool)"
  fixes upd :: "('b ⇒ 'a ⇒ 'b)"
begin

subsection‹Definitions›

text‹Apply @{text "upds"} on a sequence›
abbreviation upds :: "'b ⇒ 'a list ⇒ 'b" where
  "upds ≡ foldl upd"

fun upd_opt :: "('b ⇒ 'a option ⇒ 'b)" where
  "upd_opt info (Some hf) = upd info hf"
| "upd_opt info None = info"

text‹holds returns true iff every element of a list, together with its context, satisfies P.›
fun holds :: "'b ⇒ 'a list ⇒ 'a option ⇒ bool"
where
  "holds info (x # y # ys) nxt ⟷ P info x (Some y) ∧ holds (upd info y) (y # ys) nxt"
| "holds info [x] nxt ⟷ P info x nxt"
| "holds info [] nxt ⟷ True"

text‹holds returns the longest prefix of a list for every element, together with its context, satisfies P.›
function takeW :: "'b ⇒ 'a list ⇒ 'a option ⇒ 'a list" where
  "takeW _ [] _ = []"
| "P info x xo ⟹ takeW info [x] xo = [x]"
| "¬ P info x xo ⟹ takeW info [x] xo = []"
| "P info x (Some y) ⟹ takeW info (x # y # xs) xo = x # takeW (upd info y) (y # xs) xo"
| "¬ P info x (Some y) ⟹ takeW info (x # y # xs) xo = []"
apply auto
  by (metis remdups_adj.cases)
termination
  by lexicographic_order

text‹extract returns the last element of a list, or nxt if the list is empty.›
fun "extract" :: "'b ⇒ 'a list ⇒ 'a option ⇒ 'a option"
where
  "extract info (x # y # ys) nxt = (if P info x (Some y) then extract (upd info y) (y # ys) nxt else Some x)"
| "extract info [x] nxt = (if P info x nxt then nxt else (Some x))"
| "extract info [] nxt = nxt"


subsection‹Lemmas›

text ‹Lemmas packing singleton and at least two element cases into a single equation.›

lemma takeW_singleton:
  "takeW info [x] xo = (if P info x xo then [x] else [])"
by (simp)

lemma takeW_two_or_more:
  "takeW info (x # y # zs) xo = (if P info x (Some y) then x # takeW (upd info y) (y # zs) xo else [])"
by (simp)


text ‹Some lemmas for splitting the tail of the list argument.›

text ‹Splitting lemma formulated with if-then-else rather than case.›

lemma takeW_split_tail:
  "takeW info (x # xs) nxt =
     (if xs = []
      then (if P info x nxt then [x] else [])
      else (if P info x (Some (hd xs)) then x # takeW (upd info (hd xs)) xs nxt else []))"
by (cases xs, auto)

lemma extract_split_tail:
  "extract info (x # xs) nxt =
     (case xs of
          [] ⇒ (if P info x nxt then nxt else (Some x))
        | (y # ys) ⇒ (if P info x (Some y) then extract (upd info y) (y # ys) nxt else Some x))"
by (cases xs, auto)

lemma holds_split_tail:
  "holds info (x # xs) nxt ⟷
      (case xs of
          [] ⇒ P info x nxt
        | (y # ys) ⇒ P info x (Some y) ∧ holds (upd info y) (y # ys) nxt)"
by (cases xs, auto)

lemma holds_Cons_P:
  "holds info (x # xs) nxt ⟹ ∃y . P info x y"
by (cases xs, auto)

lemma holds_Cons_holds:
  "holds info (x # xs) nxt ⟹ holds (upd_opt info (head xs)) xs nxt"
by (cases xs, auto)

lemmas tail_splitting_lemmas =
  extract_split_tail holds_split_tail

text ‹Interaction between @{term holds}, @{term takeWhile}, and @{term extract}.›
declare if_split_asm [split]

lemma holds_takeW_extract: "holds info (takeW info xs nxt) (extract info xs nxt)"
apply(induction info xs nxt rule: takeW.induct)
apply auto
subgoal for info x y ys
  apply(cases "ys")
  apply(simp_all)
  done
done

text ‹Interaction of @{term holds}, @{term takeWhile}, and @{term extract}
with @{term append}.›

lemma holds_append:
  "holds info (xs @ ys) nxt =
   (case ys of [] ⇒ holds info xs nxt | x # _ ⇒ 
     holds info xs (Some x) ∧ 
     (case xs of [] ⇒ holds info ys nxt 
                | _ ⇒ holds (upds info (tl xs@[x])) ys nxt))"
  by(induction info xs nxt rule: takeW.induct)
    (auto split: list.split)

lemma upds_snoc: "upds uinfo (xs@[x]) = upd (upds uinfo xs) x" 
  by simp


lemma takeW_prefix:
  "prefix (takeW info l nxt) l"
by (induction info l nxt rule: takeW.induct) auto

lemma takeW_set: "t ∈ set (TWu.takeW P upd info l nxt) ⟹ t ∈ set l"
by(auto intro: takeW_prefix elim: set_prefix)

lemma holds_implies_takeW_is_identity:
  "holds info l nxt ⟹ takeW info l nxt = l"
by (induction info l nxt rule: takeW.induct) auto

(*even stronger...*)
lemma holds_takeW_is_identity[simp]:
  "takeW info l nxt = l ⟷ holds info l nxt"
  by (induction info l nxt rule: takeW.induct) auto


lemma takeW_takeW_extract:
  "takeW info (takeW info l nxt) (extract info l nxt)
 = takeW info l nxt"
using holds_takeW_extract holds_implies_takeW_is_identity
  by blast

(******************************************************************************)
subsubsection ‹Holds unfolding›
(******************************************************************************)
text ‹This section contains various lemmas that show how one can deduce P info' x' nxt' for some of
        info' x' nxt' out of a list l, for which we know that holds info l nxt is true.›

lemma holds_set_list: "⟦holds info l nxt; x ∈ set l⟧ ⟹ ∃ p y . P p x y"
  apply(induction info l nxt rule: TWu.takeW.induct[where ?Pa="P"]) by auto

lemma holds_set_list_no_update: "⟦holds info l nxt; x ∈ set l; ⋀a b. upd a b = a⟧ ⟹ ∃ y . P info x y"
  apply(induction info l nxt rule: TWu.takeW.induct[where ?Pa="P"]) by auto

lemma holds_unfold: "holds info l None ⟹
  l = [] ∨
  (∃ x . l = [x] ∧ P info x None) ∨
  (∃ x y ys . l = (x#y#ys) ∧ P info x (Some y) ∧ holds (upd info y) (y#ys) None)"
  by auto (meson holds.elims(2))

lemma holds_unfold_prexnxt': (*weakened!*)
  "⟦holds info l nxt; l = (zs@(x1#x2#xs)); zs ≠ []⟧
 ⟹ P (upds info ((tl zs)@[x1])) x1 (Some x2)"
  apply(cases zs) apply simp
  apply(simp only: TWu.holds_append)
  by auto

lemma holds_suffix:
  "⟦holds info l nxt; suffix l' l⟧ ⟹ ∃ info'. holds info' l' nxt"
  apply(cases l')
  by(auto simp add: suffix_def TWu.holds_append list.case_eq_if)

lemma holds_unfold_prelnil:
  "⟦holds info l nxt; l = (zs@(x1#[])); zs ≠ []⟧
 ⟹ P (upds info ((tl zs)@[x1])) x1 nxt"
  apply(cases zs) 
   subgoal by simp
  by(simp only: TWu.holds_append) auto


(******************************************************************************)
subsubsection ‹Update shifted›
(******************************************************************************)
text‹Usually, the update has already been applied to the head of the list. Hence, when given a list
to apply updates to (and a successor, i.e., the first element that comes after the list), we remove 
the first element of the list and add the successor. We apply the updates on the resulting list.›

fun upd_shifted :: "('b ⇒ 'a list ⇒ 'a ⇒ 'b)" where
  "upd_shifted uinfo (x#xs) nxt = upds uinfo (xs@[nxt])"
| "upd_shifted uinfo [] nxt = uinfo"


text‹This lemma is useful when there is an intermediate hop field hf of interest.›
lemma holds_intermediate:
  assumes "holds uinfo p nxt" "p = pre @ hf # post"
  shows "holds (upd_shifted uinfo pre hf) (hf # post) nxt"
using assms proof(induction pre arbitrary: p uinfo hf)
  case Nil
  then show ?case using assms by auto
next
  case induct_asm: (Cons a prev) 
  show ?case
  proof(cases prev)
    case Nil
    then have "holds (upd uinfo hf) (hf # post) nxt" 
      using induct_asm by simp
    then show ?thesis 
      using induct_asm Nil by auto
  next
    case cons_asm: (Cons b list)
    then have "holds (upd uinfo b) (b # list @ hf # post) nxt" 
      using induct_asm(2-3) by auto 
    then show ?thesis
      using induct_asm(1)
      by (simp add: cons_asm)
  qed
qed

lemma holds_intermediate_ex:
  assumes "holds uinfo hfs nxt" "hf ∈ set hfs"
  shows "∃pre post . holds (upd_shifted uinfo pre hf) (hf # post) nxt ∧ hfs = pre @ hf # post"
  using assms holds_intermediate
  by (meson split_list) 


end

end