Theory Combinators

(*<*)
theory Combinators
imports
  Programs
begin

(*>*)
section‹ More combinators\label{sec:combinators} ›

text‹

Extra combinators:
 ▪ ‹prog.select› shows how we can handle arbitrary choice
 ▪ ‹prog.while› combinator expresses all tail-recursive computations. Its condition is a pure value.

›

setup ‹Sign.mandatory_path "prog"›

definition select :: "'v set ⇒ ('s, 'v) prog" where
  "select X = (⨆x∈X. prog.return x)"

context
  notes [[function_internals]]
begin

partial_function (lfp) while :: "('k ⇒ ('s, 'k + 'v) prog) ⇒ 'k ⇒ ('s, 'v) prog" where
  "while c k = c k ⤜ (λrv. case rv of Inl k' ⇒ while c k' | Inr v ⇒ prog.return v)"

end

abbreviation loop :: "('s, unit) prog ⇒ ('s, 'w) prog" where
  "loop P ≡ prog.while (λ(). P ⪢ prog.return (Inl ())) ()"

abbreviation guardM :: "bool ⇒ ('s, unit) prog" where
  "guardM b ≡ if b then ⊥ else prog.return ()"

abbreviation unlessM :: "bool ⇒ ('s, unit) prog ⇒ ('s, unit) prog" where
  "unlessM b c ≡ if b then prog.return () else c"

abbreviation whenM :: "bool ⇒ ('s, unit) prog ⇒ ('s, unit) prog" where
  "whenM b c ≡ if b then c else prog.return ()"

definition app :: "('a ⇒ ('s, unit) prog) ⇒ 'a list ⇒ ('s, unit) prog" where ―‹ Haskell's ‹mapM_› ›
  "app f xs = foldr (λx m. f x ⪢ m) xs (prog.return ())"

definition set_app :: "('a ⇒ ('s, unit) prog) ⇒ 'a set ⇒ ('s, unit) prog" where
  "set_app f =
    prog.while (λX. if X = {} then prog.return (Inr ())
                              else prog.select X ⤜ (λx. f x ⪢ prog.return (Inl (X - {x}))))"

primrec foldM :: "('b ⇒ 'a ⇒ ('s, 'b) prog) ⇒ 'b ⇒ 'a list ⇒ ('s, 'b) prog" where
  "foldM f b [] = prog.return b"
| "foldM f b (x # xs) = do {
     b' ← f b x;
     foldM f b' xs
   }"

primrec fold_mapM :: "('a ⇒ ('s, 'b) prog) ⇒ 'a list ⇒ ('s, 'b list) prog" where
  "fold_mapM f [] = prog.return []"
| "fold_mapM f (x # xs) = do {
     y ← f x;
     ys ← fold_mapM f xs;
     prog.return (y # ys)
   }"

setup ‹Sign.mandatory_path "select"›

lemma empty:
  shows "prog.select {} = ⊥"
by (simp add: prog.select_def)

lemma singleton:
  shows "prog.select {x} = prog.return x"
by (simp add: prog.select_def)

lemma monotone:
  shows "mono prog.select"
by (simp add: monoI prog.select_def SUP_subset_mono)

lemmas strengthen[strg] = st_monotone[OF prog.select.monotone]
lemmas mono = monotoneD[OF prog.select.monotone, of P Q for P Q]
lemmas mono2mono[cont_intro, partial_function_mono] = monotone2monotone[OF prog.select.monotone, simplified, of orda P for orda P]

lemma Sup:
  shows "prog.select (⋃X) = (⨆x∈X. prog.select x)"
by (simp add: prog.select_def flip: SUP_UNION)

lemma mcont:
  shows "mcont ⋃ (⊆) Sup (≤) prog.select"
by (simp add: mcontI contI prog.select.monotone prog.select.Sup)

lemmas mcont2mcont[cont_intro] = mcont2mcont[OF prog.select.mcont, of supa orda P for supa orda P]

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "return"›

lemma select_le:
  assumes "x ∈ X"
  shows "prog.return x ≤ prog.select X"
by (simp add: assms prog.select_def SUP_upper)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "bind"›

lemma selectL:
  shows "prog.select X ⤜ g = (⨆x∈X. g x)"
by (simp add: prog.select_def prog.bind.SUPL prog.bind.returnL)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "while"›

lemma bot:
  shows "prog.while ⊥ = ⊥"
by (simp add: fun_eq_iff prog.while.simps prog.bind.botL)

lemma monotone: ―‹ could hope to prove this with a ‹strengthen› rule for \<^const>‹lfp.fixp_fun› ›
  shows "mono (λP. prog.while P s)"
by (rule monoI)
   (induct arbitrary: s rule: prog.while.fixp_induct; simp add: prog.bind.mono le_funD split: sum.split)

lemmas strengthen[strg] = st_monotone[OF prog.while.monotone]
lemmas mono' = monotoneD[OF prog.while.monotone, of P Q for P Q] ―‹ compare with @{thm [source] "prog.while.mono"} ›
lemmas mono2mono[cont_intro, partial_function_mono] = monotone2monotone[OF prog.while.monotone, simplified, of orda P for orda P]

lemma Sup_le:
  shows "(⨆P∈X. prog.while P s) ≤ prog.while (⨆X) s"
by (simp add: SUP_le_iff SupI prog.while.mono')

lemma Inf_le:
  shows "prog.while (⨅X) s ≤ (⨅P∈X. prog.while P s)"
by (simp add: le_INF_iff Inf_lower prog.while.mono')

lemma True_skip_eq_bot:
  shows "prog.while ⟨prog.return (Inl x)⟩ s = ⊥"
by (induct arbitrary: s rule: prog.while.fixp_induct) (simp_all add: prog.bind.returnL)

lemma Inr_eq_return:
  shows "prog.while ⟨prog.return (Inr v)⟩ s = prog.return v"
by (subst prog.while.simps) (simp add: prog.bind.returnL)

lemma kleene_star:
  shows "prog.kleene.star P
       = prog.while (λ_. (P ⪢ prog.return (Inl ())) ⊔ prog.return (Inr ())) ()" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ≤ ?rhs"
  proof(induct rule: prog.kleene.star.fixp_induct[case_names adm bot step])
    case (step P) then show ?case
      by (subst prog.while.simps) (simp add: prog.bind.supL prog.bind.bind prog.bind.mono sup.coboundedI1 prog.bind.returnL)
  qed simp_all
  show "?rhs ≤ ?lhs"
  proof(induct rule: prog.while.fixp_induct[case_names adm bot step])
    case (step k) then show ?case
      by (subst prog.kleene.star.simps) (simp add: prog.bind.supL prog.bind.bind prog.bind.mono prog.bind.returnL le_supI1)
  qed simp_all
qed

lemma invmap_le:
  fixes sf :: "'s ⇒ 't"
  fixes vf :: "'v ⇒ 'w"
  shows "prog.while (λk. prog.invmap sf (map_sum id vf) (c k)) k
      ≤ prog.invmap sf vf (prog.while c k)" (is "?lhs prog.while k ≤ ?rhs k")
proof(rule spec[where x=k],
      induct rule: prog.while.fixp_induct[where P="λR. ∀k. ?lhs R k ≤ ?rhs k", case_names adm bot step])
  case (step k) show ?case
    apply (subst prog.while.simps)
    apply (strengthen ord_to_strengthen(1)[OF step[rule_format]])
    apply (auto intro!: SUPE prog.bind.mono[OF order.refl]
                 split: sum.splits
                  simp: prog.invmap.bind prog.invmap.return
                        prog.invmap.split_vinvmap[where sf=sf and vf="map_sum id vf"]
                        prog.bind.bind prog.bind.return prog.bind.SUPL
                        SUP_upper
                        order.trans[OF _ prog.bind.mono[OF prog.return.rel_le order.refl]])
    done
qed (simp_all add: prog.invmap.bot)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "loop"›

lemma bindL:
  fixes P :: "('s, unit) prog"
  fixes Q :: "('s, 'w) prog"
  shows "prog.loop P ⪢ Q = prog.loop P" (is "?lhs = ?rhs")
proof(rule antisym)
  show "?lhs ≤ ?rhs"
    by (rule prog.while.fixp_induct[where P="λR. R (λ(). P ⪢ prog.return (Inl ())) () ⪢ Q ≤ ?rhs"]; simp add: prog.bind.botL)
       (subst prog.while.simps; simp add: prog.bind.bind prog.bind.mono lambda_unit_futzery prog.bind.returnL)
  show "?rhs ≤ ?lhs"
    by (rule prog.while.fixp_induct[where P="λR. R (λ(). P ⪢ prog.return (Inl ())) () ≤ ?lhs"]; simp)
       (subst prog.while.simps; simp add: prog.bind.bind prog.bind.mono lambda_unit_futzery prog.bind.returnL)
qed

lemma parallel_le:
  shows "prog.loop P ≤ lfp (λR. P ∥ R)"
proof(induct rule: prog.while.fixp_induct[case_names adm bot step])
  case (step k) show ?case
    apply (subst lfp_unfold, simp)
    apply (strengthen ord_to_strengthen[OF prog.bind.parallel_le])
    apply (simp add: prog.bind.bind prog.bind.mono prog.bind.returnL step)
    done
qed simp_all

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "foldM"›

lemma append:
  shows "prog.foldM f b (xs @ ys) = prog.foldM f b xs ⤜ (λb'. prog.foldM f b' ys)"
by (induct xs arbitrary: b) (simp_all add: prog.bind.returnL prog.bind.bind)

setup ‹Sign.parent_path›

lemma foldM_alt_def:
  shows "prog.foldM f b xs = foldr (λx m. prog.bind m (λb. f b x)) (rev xs) (prog.return b)"
by (induct xs arbitrary: b rule: rev_induct) (simp_all add: prog.foldM.append prog.bind.returnR)

setup ‹Sign.mandatory_path "fold_mapM"›

lemma bot:
  shows "prog.fold_mapM ⊥ = (λxs. case xs of [] ⇒ prog.return [] | _ ⇒ ⊥)"
by (simp add: fun_eq_iff prog.bind.botL split: list.split)

lemma append:
  shows "prog.fold_mapM f (xs @ ys)
       = prog.fold_mapM f xs ⤜ (λxs. prog.fold_mapM f ys ⤜ (λys. prog.return (xs @ ys)))"
by (induct xs) (simp_all add: prog.bind.bind prog.bind.returnL prog.bind.returnR)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "app"›

lemma bot:
  shows "prog.app ⊥ = (λxs. case xs of [] ⇒ prog.return () | _ ⇒ ⊥)"
    and "prog.app (λ_. ⊥) = (λxs. case xs of [] ⇒ prog.return () | _ ⇒ ⊥)"
by (simp_all add: fun_eq_iff prog.app_def prog.bind.botL split: list.split)

lemma Nil:
  shows "prog.app f [] = prog.return ()"
by (simp add: prog.app_def)

lemma Cons:
  shows "prog.app f (x # xs) = f x ⪢ prog.app f xs"
by (simp add: prog.app_def)

lemmas simps =
  prog.app.bot
  prog.app.Nil
  prog.app.Cons

lemma append:
  shows "prog.app f (xs @ ys) = prog.app f xs ⪢ prog.app f ys"
by (induct xs arbitrary: ys) (simp_all add: prog.app.simps prog.bind.returnL prog.bind.bind)

lemma monotone:
  shows "mono (λf. prog.app f xs)"
by (induct xs) (simp_all add: prog.app.simps le_fun_def monotone_on_def prog.bind.mono)

lemmas strengthen[strg] = st_monotone[OF prog.app.monotone]
lemmas mono = monotoneD[OF prog.app.monotone]
lemmas mono2mono[cont_intro, partial_function_mono] = monotone2monotone[OF prog.app.monotone, simplified, of orda P for orda P]

lemma Sup_le:
  shows "(⨆f∈X. prog.app f xs) ≤ prog.app (⨆X) xs"
by (simp add: SUP_le_iff SupI prog.app.mono)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "invmap"›

lemma app:
  fixes sf :: "'s ⇒ 't"
  fixes vf :: "'v ⇒ unit"
  shows "prog.invmap sf vf (prog.app f xs)
       = prog.app (λx. prog.sinvmap sf (f x)) xs ⪢ prog.invmap sf vf (prog.return ())"
by (induct xs)
   (simp_all add: prog.app.simps prog.bind.return prog.invmap.bind prog.bind.bind id_def)

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "sinvmap"›

lemma app_le:
  fixes sf :: "'s ⇒ 't"
  fixes vf :: "'v ⇒ unit"
  shows "prog.app (λx. prog.sinvmap sf (f x)) xs ≤ prog.sinvmap sf (prog.app f xs)"
by (simp add: prog.invmap.app prog.invmap.return prog.bind.return
              order.trans[OF _ prog.bind.mono[OF order.refl prog.return.rel_le]])

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "set_app"›

lemma bot:
  shows "X ≠ {} ⟹ prog.set_app ⊥ X = ⊥"
    and "X ≠ {} ⟹ prog.set_app (λ_. ⊥) X = ⊥"
by (simp_all add: prog.set_app_def prog.while.simps prog.bind.bind prog.bind.botL prog.bind.selectL)

lemma empty:
  shows "prog.set_app f {} = prog.return ()"
by (simp add: prog.set_app_def prog.while.simps prog.bind.returnL)

lemma not_empty:
  assumes "X ≠ {}"
  shows "prog.set_app f X = prog.select X ⤜ (λx. f x ⪢ prog.set_app f (X - {x}))"
using assms by (simp add: prog.set_app_def prog.while.simps prog.bind.returnL prog.bind.bind)

lemmas simps =
  prog.set_app.bot
  prog.set_app.empty
  prog.set_app.not_empty

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "app"›

lemma set_app_le:
  assumes "X = set xs"
  assumes "distinct xs"
  shows "prog.app f xs ≤ prog.set_app f X"
using assms
proof(induct xs arbitrary: X)
  case (Cons x xs) then show ?case
    apply (simp add: prog.set_app.simps prog.app.simps)
    apply (strengthen ord_to_strengthen(2)[OF prog.return.select_le[of x]], blast)
    apply (simp add: prog.bind.returnL prog.bind.mono)
    done
qed (simp add: prog.app.simps prog.set_app.simps)

setup ‹Sign.parent_path›

lemma set_app_alt_def:
  assumes "finite X"
  shows "prog.set_app f X = (⨆xs∈{ys. set ys = X ∧ distinct ys}. prog.app f xs)" (is "?lhs = ?rhs")
proof(rule antisym)
  from assms show "?lhs ≤ ?rhs"
  proof(induct rule: finite_remove_induct)
    case (remove X)
    from ‹finite X› ‹X ≠ {}› have *: "{ys. set ys = X - {x} ∧ distinct ys} ≠ {}" for x
      by (simp add: finite_distinct_list)
    from ‹X ≠ {}› show ?case
      apply (clarsimp simp: prog.set_app.simps prog.bind.selectL)
      apply (strengthen ord_to_strengthen[OF remove.hyps(4)], blast)
      apply (fastforce simp: prog.app.simps prog.bind.SUPR_not_empty[OF *] Sup_le_iff
                      intro: rev_SUPI[where x="x # xs" for x xs])
      done
  qed (simp add: prog.set_app.simps prog.app.simps)
  show "?rhs ≤ ?lhs"
    by (simp add: Sup_le_iff prog.app.set_app_le)
qed

setup ‹Sign.parent_path›

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "ag.prog"›

lemma select_sp:
  assumes "⋀s x. ⟦P s; x ∈ X⟧ ⟹ Q x s"
  assumes "⋀v. stable A (P ❙∧ Q v)"
  shows "prog.p2s (prog.select X) ≤ ⦃P⦄, A ⊢ G, ⦃λv. P ❙∧ Q v⦄"
by (clarsimp simp: prog.select_def prog.p2s.Sup spec.interference.cl.bot ag.spec.term.none_inteference)
   (rule ag.pre[OF ag.prog.return[OF assms(2)]]; blast intro: assms(1))

lemma while:
  fixes c :: "'k ⇒ ('s, 'k + 'v) prog"
  assumes c: "⋀k. prog.p2s (c k) ≤ ⦃P k⦄, A ⊢ G, ⦃case_sum I Q⦄"
  assumes IP: "⋀s v. I v s ⟹ P v s"
  assumes sQ: "⋀v. stable A (Q v)"
  shows "prog.p2s (prog.while c k) ≤ ⦃I k⦄, A ⊢ G, ⦃Q⦄"
proof -
  have "prog.p2s (prog.while c k) ≤ ⦃P k⦄, A ⊢ G, ⦃Q⦄"
  proof(induct arbitrary: k rule: prog.while.fixp_induct[case_names adm bot step])
    case (step k) show ?case
      apply (rule ag.prog.bind[OF _ c])
      apply (rule ag.pre_pre[OF ag.prog.case_sum[OF step ag.prog.return[OF sQ]]])
      apply (simp add: IP split: sum.splits)
      done
  qed (simp_all add: ag.prog.galois)
  then show ?thesis
    by (meson IP ag.pre_pre)
qed

lemma app:
  fixes xs :: "'a list"
  fixes f :: "'a ⇒ ('s, unit) prog"
  fixes P :: "'a list ⇒ 's pred"
  assumes "⋀x ys zs. xs = ys @ x # zs ⟹ prog.p2s (f x) ≤ ⦃P ys⦄, A ⊢ G, ⦃λ_. P (ys @ [x])⦄"
  assumes "⋀ys. prefix ys xs ⟹ stable A (P ys)"
  shows "prog.p2s (prog.app f xs) ≤ ⦃P []⦄, A ⊢ G, ⦃λ_. P xs⦄"
using assms
by (induct xs rule: rev_induct;
    fastforce intro: ag.prog.bind ag.prog.return
               simp: prog.app.append prog.bind.returnR prog.app.simps)

lemma app_set:
  fixes X :: "'a set"
  fixes f :: "'a ⇒ ('s, unit) prog"
  fixes P :: "'a set ⇒ 's pred"
  assumes "⋀Y x. ⟦Y ⊆ X; x ∈ X - Y⟧ ⟹ prog.p2s (f x) ≤ ⦃P Y⦄, A ⊢ G, ⦃λ_. P (insert x Y)⦄"
  assumes "⋀Y. Y ⊆ X ⟹ Stability.stable A (P Y)"
  shows "prog.p2s (prog.set_app f X) ≤ ⦃P {}⦄, A ⊢ G, ⦃λ_. P X⦄"
proof -
  have *: "X - (Y - {x}) = insert x (X - Y)" if "Y ⊆ X" and "x ∈ Y" for x and X Y :: "'a set"
    using that by blast
  show ?thesis
    unfolding prog.set_app_def
    apply (rule ag.prog.while[where I="λY s. Y ⊆ X ∧ P (X - Y) s" and Q="⟨P X⟩" and k="X", simplified])
      apply (rename_tac k)
      apply (rule ag.prog.if)
       apply (rule ag.prog.return)
       apply (simp add: assms; fail)
      apply (rule_tac P="λs. k ⊆ X ∧ P (X - k) s" in ag.prog.bind[rotated])
       apply (rule_tac Q="λx s. x ∈ k" in ag.prog.select_sp, assumption)
       apply (simp add: assms(2) stable.conjI stable.const; fail)
      apply (intro ag.gen_asm)
      apply (rule ag.prog.bind[rotated])
       apply (rule assms(1); force)
      apply (rule ag.pre_pre[OF ag.prog.return])
       apply (simp add: assms(2) stable.conjI stable.const; fail)
      using * apply fastforce
     apply force
    apply (simp add: assms(2))
    done
qed

lemma foldM:
  fixes xs :: "'a list"
  fixes f :: "'b ⇒ 'a ⇒ ('s, 'b) prog"
  fixes I :: "'b ⇒ 'a ⇒ 's pred"
  fixes P :: "'b ⇒ 's pred"
  assumes f: "⋀b x. x ∈ set xs ⟹ prog.p2s (f b x) ≤ ⦃I b x⦄, A ⊢ G, ⦃P⦄"
  assumes P: "⋀b x s. ⟦P b s; x ∈ set xs⟧ ⟹ I b x s"
  assumes sP: "⋀b. stable A (P b)"
  shows "prog.p2s (prog.foldM f b xs) ≤ ⦃P b⦄, A ⊢ G, ⦃P⦄"
using f P by (induct xs arbitrary: b) (fastforce intro!: ag.prog.bind intro: ag.pre_pre ag.prog.return[OF sP])+

setup ‹Sign.parent_path›
(*<*)

end
(*>*)