Theory Blackboard

(*
  Title:      Blackboard.thy
  Author:     Diego Marmsoler
*)
section "A Theory of Blackboard Architectures"
text‹
  In the following, we formalize the specification of the blackboard pattern as described in~cite‹"Marmsoler2018c"›.
›

theory Blackboard
imports Publisher_Subscriber
begin

subsection "Problems and Solutions"
text ‹
  Blackboards work with problems and solutions for them.
›
typedecl PROB
consts sb :: "(PROB × PROB) set"
axiomatization where sbWF: "wf sb"
typedecl SOL
consts solve:: "PROB ⇒ SOL"

subsection "Blackboard Architectures"
text ‹
  In the following, we describe the locale for the blackboard pattern.
›
locale blackboard = publisher_subscriber bbactive bbcmp ksactive kscmp bbrp bbcs kscs ksrp
  for bbactive :: "'bid ⇒ cnf ⇒ bool" (‹∥_∥⇘_⇙› [0,110]60)
    and bbcmp :: "'bid ⇒ cnf ⇒ 'BB" (‹σ⇘_⇙(_)› [0,110]60)
    and ksactive :: "'kid ⇒ cnf ⇒ bool" (‹∥_∥⇘_⇙› [0,110]60)
    and kscmp :: "'kid ⇒ cnf ⇒ 'KS" (‹σ⇘_⇙(_)› [0,110]60)
    and bbrp :: "'BB ⇒ (PROB set) subscription set"
    and bbcs :: "'BB ⇒ (PROB × SOL)"
    and kscs :: "'KS ⇒ (PROB × SOL) set"
    and ksrp :: "'KS ⇒ (PROB set) subscription" +
  fixes bbns :: "'BB ⇒ (PROB × SOL) set"
    and ksns :: "'KS ⇒ (PROB × SOL)"
    and bbop :: "'BB ⇒ PROB"
    and ksop :: "'KS ⇒ PROB set"
    and prob :: "'kid ⇒ PROB"
  assumes
    ks1: "∀p. ∃ks. p=prob ks" ― ‹Component Parameter›
    ― ‹Assertions about component behavior.›
    and bhvbb1: "⋀t t' bId p s. ⟦t ∈ arch⟧ ⟹ pb.eval bId t t' 0
      (□b ([λbb. (p,s)∈bbns bb]b
      ⟶b (◇b [λbb. (p,s) = bbcs bb]b)))"
    and bhvbb2: "⋀t t' bId P q. ⟦t∈arch⟧ ⟹ pb.eval bId t t' 0
      (□b ([λbb. sub P ∈ bbrp bb ∧ q ∈ P]b ⟶b
      (◇b [λbb. q = bbop bb]b)))"
    and bhvbb3: "⋀t t' bId p . ⟦t∈arch⟧ ⟹ pb.eval bId t t' 0
      (□b ([λbb. p = bbop(bb)]b ⟶b
      ([λbb. p=bbop(bb)]b 𝔚b [λbb. (p,solve(p)) = bbcs(bb)]b)))"
    and bhvks1: "⋀t t' kId p P. ⟦t∈arch; p = prob kId⟧ ⟹ sb.eval kId t t' 0
      (□b ([λks. sub P = ksrp ks]b ∧b
      (∀b q. ((sb.pred (q∈P)) ⟶b (◇b ([λks. (q,solve(q)) ∈ kscs ks]b))))
      ⟶b (◇b [λks. (p, solve p) = ksns ks]b)))"
    and bhvks2: "⋀t t' kId p P q. ⟦t ∈ arch;p = prob kId⟧ ⟹ sb.eval kId t t' 0
      (□b [λks. sub P = ksrp ks ∧ q ∈ P ⟶ (q,p) ∈ sb]b)"
    and bhvks3: "⋀t t' kId p. ⟦t∈arch;p = prob kId⟧ ⟹ sb.eval kId t t' 0
      (□b ([λks. p∈ksop ks]b ⟶b (◇b [λks. (∃P. sub P = ksrp ks)]b)))"
    and bhvks4: "⋀t t' kId p P. ⟦t∈arch; p∈P⟧ ⟹ sb.eval kId t t' 0
      (□b ([λks. sub P = ksrp ks]b ⟶b
      ((¬b (∃b P'. (sb.pred (p∈P') ∧b [λks. unsub P' = ksrp ks]b))) 𝔚b
      [λks. (p,solve p) ∈ kscs ks]b)))"

    ― ‹Assertions about component activation.›
    and actks:
      "⋀t n kid p. ⟦t ∈ arch; ∥kid∥⇘t n⇙; p=prob kid; p∈ksop (σ⇘kid⇙(t n))⟧
      ⟹ (∃n'≥n. ∥kid∥⇘t n'⇙ ∧ (p, solve p) = ksns (σ⇘kid⇙(t n')) ∧
      (∀n''≥n. n''<n' ⟶ ∥kid∥⇘t n''⇙))
      ∨ (∀n'≥n. (∥kid∥⇘t n'⇙ ∧ (¬(p, solve p) = ksns (σ⇘kid⇙(t n')))))"

    ― ‹Assertions about connections.›
    and conn1: "⋀k bid. ∥bid∥⇘k⇙
      ⟹ bbns (σ⇘bid⇙(k)) = (⋃kid∈{kid. ∥kid∥⇘k⇙}. {ksns (σ⇘kid⇙(k))})"
    and conn2: "⋀k kid. ∥kid∥⇘k⇙
      ⟹ ksop (σ⇘kid⇙(k)) = (⋃bid∈{bid. ∥bid∥⇘k⇙}. {bbop (σ⇘bid⇙(k))})"
begin
  notation sb.lNAct (‹⟨_ ⇐ _⟩⇘_⇙›)
  notation sb.nxtAct (‹⟨_ → _⟩⇘_⇙›)
  notation pb.lNAct (‹⟨_ ⇐ _⟩⇘_⇙›)
  notation pb.nxtAct (‹⟨_ → _⟩⇘_⇙›)

  subsubsection "Calculus Interpretation"
  text ‹
  \noindent
  @{thm[source] pb.baIA}: @{thm pb.baIA [no_vars]}
›
  text ‹
  \noindent
  @{thm[source] sb.baIA}: @{thm sb.baIA [no_vars]}
›

  subsubsection "Results from Singleton"
  abbreviation "the_bb ≡ the_pb"
  text ‹
  \noindent
  @{thm[source] pb.ts_prop(1)}: @{thm pb.ts_prop(1) [no_vars]}
›
  text ‹
  \noindent
  @{thm[source] pb.ts_prop(2)}: @{thm pb.ts_prop(2) [no_vars]}
›
  subsubsection "Results from Publisher Subscriber"
  text ‹
	\noindent
	@{thm[source] msgDelivery}: @{thm msgDelivery [no_vars]}
›
  lemma conn2_bb:
    fixes k and kid::'kid
    assumes "∥kid∥⇘k⇙"
    shows "bbop (σ⇘the_bb⇙(k))∈ksop (σ⇘kid⇙(k))"
  proof -
    from assms have "ksop (σ⇘kid⇙(k)) = (⋃bid∈{bid. ∥bid∥⇘k⇙}. {bbop (σ⇘bid⇙(k))})" using conn2 by simp
    moreover have "(⋃bid.{bid. ∥bid∥⇘k⇙})={the_bb}" using pb.ts_prop(1) by auto
    hence "(⋃bid∈{bid. ∥bid∥⇘k⇙}. {bbop (σ⇘bid⇙(k))}) = {bbop (σ⇘the_bb⇙(k))}" by auto
    ultimately show ?thesis by simp
  qed

  subsubsection "Knowledge Sources"
  text ‹
    In the following we introduce an abbreviation for knowledge sources which are able to solve a specific problem.
›
  definition sKs:: "PROB ⇒ 'kid" where
    "sKs p ≡ (SOME kid. p = prob kid)"

  lemma sks_prob:
    "p = prob (sKs p)"
  using sKs_def someI_ex[of "λkid. p = prob kid"] ks1 by auto

  subsubsection "Architectural Guarantees"
  text‹
    The following theorem verifies that a problem is eventually solved by the pattern even if no knowledge source exist which can solve the problem on its own.
    It assumes, however, that for every open sub problem, a corresponding knowledge source able to solve the problem will be eventually activated.
›
  lemma pSolved_Ind:
    fixes t and t'::"nat ⇒'BB" and p and t''::"nat ⇒'KS"
    assumes "t∈arch" and
      "∀n. (∃n'≥n. ∥sKs (bbop(σ⇘the_bb⇙(t n)))∥⇘t n'⇙)"
    shows
      "∀n. (∃P. sub P ∈ bbrp(σ⇘the_bb⇙(t n)) ∧ p ∈ P) ⟶
        (∃m≥n. (p,solve(p)) = bbcs (σ⇘the_bb⇙(t m)))" (*\eqref{eq:bb:g}*)
  ― ‹The proof is by well-founded induction over the subproblem relation @{term sb}›
  proof (rule wf_induct[where r=sb])
    ― ‹We first show that the subproblem relation is indeed well-founded ...›
    show "wf sb" by (simp add: sbWF)
  next
    ― ‹... then we show that a problem @{term p} is indeed solved›
    ― ‹if all its sub-problems @{term p'} are eventually solved›
    fix p assume indH: "∀p'. (p', p) ∈ sb ⟶ (∀n. (∃P. sub P ∈ bbrp (σ⇘the_bb⇙(t n)) ∧ p'∈P)
      ⟶ (∃m≥n. (p',solve(p')) = bbcs (σ⇘the_bb⇙(t m))))"
    show "∀n. (∃P. sub P ∈ bbrp (σ⇘the_bb⇙(t n)) ∧ p ∈ P)
      ⟶ (∃m≥n. (p,solve(p)) = bbcs (σ⇘the_bb⇙(t m)))"
    proof
      fix n0 show "(∃P. sub P ∈ bbrp (σ⇘the_bb⇙(t n0)) ∧ p ∈ P) ⟶
      (∃m≥n0. (p,solve(p)) = bbcs (σ⇘the_bb⇙(t m)))"
      proof
        assume "∃P. sub P ∈ bbrp (σ⇘the_bb⇙(t n0)) ∧ p ∈ P"
        moreover have "(∃P. sub P ∈ bbrp (σ⇘the_bb⇙(t n0)) ∧ p ∈ P) ⟶ (∃n'≥n0. p=bbop(σ⇘the_bb⇙(t n')))"
        proof
          assume "∃P. sub P ∈ bbrp (σ⇘the_bb⇙(t n0)) ∧ p ∈ P"
          then obtain P where "sub P ∈ bbrp (σ⇘the_bb⇙(t n0))" and "p ∈ P" by auto
          hence "pb.eval the_bb t t' n0 [λbb. sub P ∈ bbrp bb ∧ p ∈ P]b" using pb.baI by simp
          moreover from pb.globE[OF bhvbb2] have
            "pb.eval the_bb t t' n0 ([λbb. sub P ∈ bbrp bb ∧ p ∈ P]b ⟶b ◇b [λbb. p = bbop bb]b)"
            using ‹t∈arch› by simp
          ultimately have "pb.eval the_bb t t' n0 (◇b [λbb. p = bbop bb]b)" using pb.impE by blast
          then obtain n' where "n'≥n0" and "pb.eval the_bb t t' n' [λbb. p = bbop bb]b"
            using pb.evtE by blast
          hence "p=bbop(σ⇘the_bb⇙(t n'))" using pb.baE by auto
          with ‹n'≥n0› show "∃n'≥n0. p=bbop(σ⇘the_bb⇙(t n'))" by auto
        qed
        ultimately obtain n where "n≥n0" and "p=bbop(σ⇘the_bb⇙(t n))" by auto

        ― ‹Problem p is provided at the output of the blackboard until it is solved›
        ― ‹or forever...›
        from pb.globE[OF bhvbb3] have
          "pb.eval the_bb t t' n ([λ bb. p = bbop(bb)]b ⟶b
          ([λ bb. p=bbop(bb)]b 𝔚b [λbb. (p,solve(p)) = bbcs(bb)]b))"
          using ‹t∈arch› by auto
        moreover from ‹p = bbop (σ⇘the_bb⇙(t n))› have
          "pb.eval the_bb t t' n [λ bb. p=bbop bb]b"
          using ‹t∈arch› pb.baI by simp
        ultimately have "pb.eval the_bb t t' n
          ([λ bb. p=bbop(bb)]b 𝔚b [λ bb. (p,solve(p)) = bbcs(bb)]b)"
          using pb.impE by blast
        hence "pb.eval the_bb t t' n (([λ bb. p=bbop bb]b 𝔘b
          [λ bb. (p,solve(p)) = bbcs bb]b) ∨b (□b [λ bb. p=bbop bb]b))"
          using pb.wuntil_def by simp
        hence "pb.eval the_bb t t' n
          ([λbb. p=bbop bb]b 𝔘b [λbb. (p,solve(p)) = bbcs bb]b) ∨
          (pb.eval the_bb t t' n (□b [λ bb. p=bbop bb]b))"
          using pb.disjE by simp
        thus "∃m≥n0. (p,solve p) = bbcs(σ⇘the_bb⇙(t m))"
        ― ‹We need to consider both cases, the case in which the problem is eventually›
        ― ‹solved and the case in which the problem is always provided as an output›
        proof
          ― ‹First we consider the case in which the problem is eventually solved:›
          assume "pb.eval the_bb t t' n
            ([λbb. p=bbop bb]b 𝔘b [λbb. (p,solve(p)) = bbcs bb]b)"
          hence "∃i≥n. (pb.eval the_bb t t' i
            [λbb. (p,solve(p)) = bbcs bb]b ∧
            (∀k≥n. k<i ⟶ pb.eval the_bb t t' k [λbb. p = bbop bb]b))"
            using ‹t∈arch› pb.untilE by simp
          then obtain i where "i≥n" and
            "pb.eval the_bb t t' i [λbb. (p,solve(p)) = bbcs bb]b" by auto
          hence "(p,solve(p)) = bbcs(σ⇘the_bb⇙(t i))"
            using ‹t∈arch› pb.baEA by auto
          moreover from ‹i≥n› ‹n≥n0› have "i≥n0" by simp
          ultimately show ?thesis by auto
        next
          ― ‹Now we consider the case in which p is always provided at the output›
          ― ‹of the blackboard:›
          assume "pb.eval the_bb t t' n
            (□b [λbb. p=bbop bb]b)"
          hence "∀n'≥n. (pb.eval the_bb t t' n' [λbb. p = bbop bb]b)"
            using ‹t∈arch› pb.globE by auto
          hence outp: "∀n'≥n. (p = bbop (σ⇘the_bb⇙(t n')))"
            using ‹t∈arch› pb.baE by blast

          ― ‹thus, by assumption there exists a KS which is able to solve p and which›
          ― ‹is active at @{text n'}...›
          with assms(2) have "∃n'≥n. ∥sKs p∥⇘t n'⇙" by auto
          then obtain nk where "nk≥n" and "∥sKs p∥⇘t nk⇙" by auto
          ― ‹... and get the problem as its input.›
          moreover from ‹nk≥n› have "p = bbop (σ⇘the_bb⇙(t nk))"
            using outp by simp
          ultimately have "p∈ksop(σ⇘sKs p⇙(t nk))" using conn2_bb[of "sKs p" "t nk"] by simp

          ― ‹thus the ks will either solve the problem or not solve it and›
          ― ‹be activated forever›
          hence "(∃n'≥nk. ∥sKs p∥⇘t n'⇙ ∧
            (p, solve p) = ksns (σ⇘sKs p⇙(t n')) ∧
            (∀n''≥nk. n''<n' ⟶ ∥sKs p∥⇘t n''⇙)) ∨
            (∀n'≥nk. (∥sKs p∥⇘t n'⇙ ∧
            (¬(p, solve p) = ksns (σ⇘sKs p⇙(t n')))))"
            using ‹∥sKs p∥⇘t nk⇙› actks[of t "sKs p"] ‹t∈arch› sks_prob by simp
          thus ?thesis
          proof
            ― ‹if the ks solves it›
            assume "∃n'≥nk. ∥sKs p∥⇘t n'⇙ ∧ (p, solve p) = ksns (σ⇘sKs p⇙t n')
              ∧ (∀n''≥nk. n'' < n' ⟶ ∥sKs p∥⇘t n''⇙)"
            ― ‹it is forwarded to the blackboard›
            then obtain ns where "ns≥nk" and "∥sKs p∥⇘t ns⇙"
              and "(p, solve p) = ksns (σ⇘sKs p⇙t ns)" by auto
            moreover have "⟨sKs p → t⟩⇘ns⇙ = ns"
              by (simp add: ‹∥sKs p∥⇘t ns⇙› sb.nxtAct_active)
            ultimately have
              "(p,solve(p)) ∈ bbns (σ⇘the_bb⇙(t (⟨sKs p → t⟩⇘ns⇙)))"
              using conn1[OF pb.ts_prop(2)] ‹∥sKs p∥⇘t ns⇙› by auto

            ― ‹finally, the blackboard will forward the solution which finishes the proof.›
            with bhvbb1 have "pb.eval the_bb t t' (⟨sKs p → t⟩⇘ns⇙)
              (◇b [λbb. (p, solve p) = bbcs bb]b)"
              using ‹t∈arch› pb.globE pb.impE[of the_bb t t'] by blast
            then obtain nf where "nf≥⟨sKs p → t⟩⇘ns⇙" and
              "pb.eval the_bb t t' nf [λbb. (p, solve p) = bbcs bb]b"
              using ‹t∈arch› pb.evtE[of t t' "⟨sKs p → t⟩⇘ns⇙"] by auto
            hence "(p, solve p) = bbcs (σ⇘the_bb⇙(t nf))"
              using ‹t ∈ arch› pb.baEA by auto
            moreover have "nf≥n0"
            proof -
              from ‹∥sKs p∥⇘t nk⇙› have "⟨sKs p → t⟩⇘nk⇙≥nk"
                using sb.nxtActI by blast
              with ‹⟨sKs p → t⟩⇘ns⇙ = ns› show ?thesis
                using ‹nf≥⟨sKs p → t⟩⇘ns⇙› ‹ns≥nk› ‹nk≥n› ‹n≥n0› by arith
            qed
            ultimately show ?thesis by auto
          next
            ― ‹otherwise, we derive a contradiction›
            assume case_ass: "∀n'≥nk. ∥sKs p∥⇘t n'⇙ ∧ ¬(p, solve p) = ksns (σ⇘sKs p⇙t n')"

            ― ‹first, the KS will eventually register for the subproblems P it requires to solve p...›
            from ‹∥sKs p∥⇘t nk⇙› have "∃i≥0. ∥sKs p∥⇘t i⇙" by auto
            moreover have "⟨sKs p ⇐ t⟩⇘0⇙ ≤ nk" by simp
            ultimately have "sb.eval (sKs p) t t'' nk
              ([λks. p∈ksop ks]b ⟶b (◇b [λks. ∃P. sub P = ksrp ks]b))"
              using sb.globEA[OF _ bhvks3[of t p "sKs p" t'']] ‹t∈arch› sks_prob by simp
            moreover have "sb.eval (sKs p) t t'' nk [λks. p ∈ ksop ks]b"
            proof -
              from ‹∥sKs p∥⇘t nk⇙› have "∃n'≥nk. ∥sKs p∥⇘t n'⇙" by auto
              moreover have "p ∈ ksop (σ⇘sKs p⇙(t (⟨sKs p → t⟩⇘nk⇙)))"
              proof -
                from ‹∥sKs p∥⇘t nk⇙› have "⟨sKs p → t⟩⇘nk⇙=nk"
                  using sb.nxtAct_active by blast
                with ‹p∈ksop(σ⇘sKs p⇙(t nk))› show ?thesis by simp
              qed
              ultimately show ?thesis using sb.baIA[of nk "sKs p" t] by blast
            qed
            ultimately have "sb.eval (sKs p) t t'' nk (◇b [λks. ∃P. sub P = ksrp ks]b)"
              using sb.impE by blast
            then obtain nr where "nr≥⟨sKs p → t⟩⇘nk⇙" and
              "∃i≥nr. ∥sKs p∥⇘t i⇙ ∧
              (∀n''≥⟨sKs p ⇐ t⟩⇘nr⇙. n'' ≤ ⟨sKs p → t⟩⇘nr⇙
              ⟶ sb.eval (sKs p) t t'' n'' [λks. ∃P. sub P = ksrp ks]b) ∨
              ¬ (∃i≥nr. ∥sKs p∥⇘t i⇙) ∧
              sb.eval (sKs p) t t'' nr [λks. ∃P. sub P = ksrp ks]b"
              using ‹∥sKs p∥⇘t nk⇙› sb.evtEA[of nk "sKs p" t] by blast
            moreover from case_ass have "⟨sKs p → t⟩⇘nk⇙≥nk" using sb.nxtActI by blast
            with ‹nr≥⟨sKs p → t⟩⇘nk⇙› have "nr≥nk" by arith
            hence "∃i≥nr. ∥sKs p∥⇘t i⇙" using case_ass by auto
            hence "nr ≤ ⟨sKs p → t⟩⇘nr⇙" using sb.nxtActLe by simp
            moreover have "nr ≥ ⟨sKs p ⇐ t⟩⇘nr⇙" by simp
            ultimately have
              "sb.eval (sKs p) t t'' nr [λks. ∃P. sub P = ksrp ks]b" by blast
            with ‹∃i≥nr. ∥sKs p∥⇘t i⇙› obtain P where
              "sub P = ksrp (σ⇘sKs p⇙(t (⟨sKs p → t⟩⇘nr⇙)))"
              using sb.baEA by blast
            hence "sb.eval (sKs p) t t'' nr [λks. sub P = ksrp ks]b"
              using ‹∃i≥nr. ∥sKs p∥⇘t i⇙› sb.baIA sks_prob by blast

            ― ‹the knowledgesource will eventually get a solution for each required subproblem:›
            moreover have "sb.eval (sKs p) t t'' nr (∀b p'. (sb.pred (p'∈P) ⟶b
              (◇b [λks. (p',solve p') ∈ kscs ks]b)))"
            proof -
              have "∀p'. sb.eval (sKs p) t t'' nr (sb.pred (p'∈P) ⟶b
                (◇b [λks. (p',solve p') ∈ kscs ks]b))"
              proof
                ― ‹by induction hypothesis, the blackboard will eventually provide solutions for subproblems›
                fix p'
                have "sb.eval (sKs p) t t'' nr (sb.pred (p'∈P)) ⟶
                  (sb.eval (sKs p) t t'' nr
                  (◇b [λks. (p',solve p') ∈ kscs ks]b))"
                proof
                  assume "sb.eval (sKs p) t t'' nr (sb.pred (p'∈P))"
                  hence "p' ∈ P" using sb.predE by blast
                  thus "(sb.eval (sKs p) t t'' nr (◇b [λks. (p',solve p') ∈ kscs ks]b))"
                  proof -
                    have "⟨sKs p ⇐ t⟩⇘0⇙ ≤ nr" by simp
                    moreover from ‹∥sKs p∥⇘t nk⇙› have "∃i≥0. ∥sKs p∥⇘t i⇙" by auto
                    ultimately have "sb.eval (sKs p) t t'' nr ([λks. sub P = ksrp ks]b
                      ⟶b ((¬b (∃b P'. (sb.pred (p'∈P') ∧b [λks. unsub P' = ksrp ks]b))) 𝔚b
                      [λks. (p',solve p') ∈ kscs ks]b))"
                      using sb.globEA[OF _ bhvks4[of t p' P "sKs p" t'']]
                      ‹t∈arch› ‹∥sKs p∥⇘t nk⇙› ‹p'∈P› by simp
                    with ‹sb.eval (sKs p) t t'' nr [λks. sub P = ksrp ks]b› have
                      "sb.eval (sKs p) t t'' nr ((¬b (∃b P'. (sb.pred (p'∈P') ∧b
                      [λks. unsub P' = ksrp ks]b))) 𝔚b [λks. (p',solve p') ∈ kscs ks]b)"
                      using sb.impE[of "(sKs p)" t t'' nr "[λks. sub P = ksrp ks]b"] by blast
                    hence "sb.eval (sKs p) t t'' nr ((¬b (∃b P'. (sb.pred (p'∈P') ∧b
                      [λks. unsub P' = ksrp ks]b))) 𝔘b [λks. (p',solve p') ∈ kscs ks]b) ∨
                      sb.eval (sKs p) t t'' nr (□b (¬b (∃b P'. (sb.pred (p'∈P') ∧b
                      [λks. unsub P' = ksrp ks]b))))" using sb.wuntil_def by auto
                    thus "(sb.eval (sKs p) t t'' nr (◇b [λks. (p',solve p') ∈ kscs ks]b))"
                    proof
                      let ?γ'="¬b (∃b P'. (sb.pred (p'∈P') ∧b ([λks. unsub P' = ksrp ks]b)))"
                      let ?γ="[λks. (p',solve p') ∈ kscs ks]b"
                      assume "sb.eval (sKs p) t t'' nr (?γ' 𝔘b ?γ)"
                      with ‹∃i≥nr. ∥sKs p∥⇘t i⇙› obtain n' where "n'≥⟨sKs p → t⟩⇘nr⇙" and
                        lass: "(∃i≥n'. ∥sKs p∥⇘t i⇙) ∧ (∀n''≥⟨sKs p ⇐ t⟩⇘n'⇙. n'' ≤ ⟨sKs p → t⟩⇘n'⇙
                        ⟶ sb.eval (sKs p) t t'' n'' ?γ) ∧
                        (∀n''≥⟨sKs p ⇐ t⟩⇘nr⇙. n'' < ⟨sKs p ⇐ t⟩⇘n'⇙
                        ⟶ sb.eval (sKs p) t t'' n'' ?γ') ∨
                        ¬ (∃i≥n'. ∥sKs p∥⇘t i⇙) ∧ sb.eval (sKs p) t t'' n' ?γ ∧
                        (∀n''≥⟨sKs p ⇐ t⟩⇘nr⇙. n'' < n' ⟶ sb.eval (sKs p) t t'' n'' ?γ')"
                        using sb.untilEA[of nr "sKs p" t t''] ‹∃i≥nr. ∥sKs p∥⇘t i⇙› by blast
                      thus "?thesis"
                      proof cases
                        assume "∃i≥n'. ∥sKs p∥⇘t i⇙"
                        with lass have "∀n''≥⟨sKs p ⇐ t⟩⇘n'⇙. n'' ≤ ⟨sKs p → t⟩⇘n'⇙
                          ⟶ sb.eval (sKs p) t t'' n'' ?γ" by auto
                        moreover have "n'≥⟨sKs p ⇐ t⟩⇘n'⇙" by simp
                        moreover have "n' ≤ ⟨sKs p → t⟩⇘n'⇙"
                          using ‹∃i≥n'. ∥sKs p∥⇘t i⇙› sb.nxtActLe by simp
                        ultimately have "sb.eval (sKs p) t t'' n' ?γ" by simp
                        moreover have "⟨sKs p ⇐ t⟩⇘nr⇙ ≤ n'" using ‹nr ≤ ⟨sKs p → t⟩⇘nr⇙›
                        ‹⟨sKs p ⇐ t⟩⇘nr⇙ ≤ nr› ‹⟨sKs p → t⟩⇘nr⇙ ≤ n'› by linarith
                        ultimately show ?thesis using ‹∃i≥nr. ∥sKs p∥⇘t i⇙› ‹∃i≥n'. ∥sKs p∥⇘t i⇙›
                          ‹n'≥⟨sKs p ⇐ t⟩⇘n'⇙› ‹n' ≤ ⟨sKs p → t⟩⇘n'⇙›
                          sb.evtIA[of nr "sKs p" t n' t'' ?γ] by blast
                      next
                        assume "¬ (∃i≥n'. ∥sKs p∥⇘t i⇙)"
                        with lass have "sb.eval (sKs p) t t'' n' ?γ ∧
                          (∀n''≥⟨sKs p ⇐ t⟩⇘nr⇙. n'' < n' ⟶ sb.eval (sKs p) t t'' n'' ?γ')" by auto
                        moreover have "⟨sKs p ⇐ t⟩⇘nr⇙ ≤ n'"
                          using ‹nr ≤ ⟨sKs p → t⟩⇘nr⇙› ‹⟨sKs p ⇐ t⟩⇘nr⇙ ≤ nr›
                          ‹⟨sKs p → t⟩⇘nr⇙ ≤ n'› by linarith
                        ultimately show ?thesis using ‹∃i≥nr. ∥sKs p∥⇘t i⇙› ‹¬ (∃i≥n'. ∥sKs p∥⇘t i⇙)›
                            sb.evtIA[of nr "sKs p" t n' t'' ?γ] by blast
                      qed
                    next
                      assume cass: "sb.eval (sKs p) t t'' nr
                        (□b (¬b (∃b P'. (sb.pred (p'∈P') ∧b [λks. unsub P' = ksrp ks]b))))"

                      have "sub P = ksrp (σ⇘sKs p⇙(t (⟨sKs p → t⟩⇘nr⇙))) ∧
                        p' ∈ P ⟶ (p', p) ∈ sb"
                      proof -
                        have "∃i≥0. ∥sKs p∥⇘t i⇙" using ‹∃i≥0. ∥sKs p∥⇘t i⇙› by auto
                        moreover have "⟨sKs p ⇐ t⟩⇘0⇙ ≤ (⟨sKs p → t⟩⇘nr⇙)" by simp
                        ultimately have "sb.eval (sKs p) t t'' (⟨sKs p → t⟩⇘nr⇙)
                          [λks. sub P = ksrp ks ∧ p' ∈ P ⟶ (p', p) ∈ sb]b"
                          using sb.globEA[OF _ bhvks2[of t p "sKs p" t'' P]] ‹t ∈ arch› sks_prob by blast
                        moreover from ‹∃i≥nr. ∥sKs p∥⇘t i⇙› have
                          "∥sKs p∥⇘t (⟨sKs p → t⟩⇘nr⇙)⇙" using sb.nxtActI by blast
                        ultimately show ?thesis
                          using sb.baEANow[of "sKs p" t t'' "⟨sKs p → t⟩⇘nr⇙"] by simp
                      qed
                      with ‹p' ∈ P› have "(p', p) ∈ sb"
                        using ‹sub P = ksrp (σ⇘sKs p⇙(t (⟨sKs p → t⟩⇘nr⇙)))›
                        sks_prob by simp
                      moreover from ‹∃i≥nr. ∥sKs p∥⇘t i⇙› have "∥sKs p∥⇘t (⟨sKs p → t⟩⇘nr⇙)⇙"
                        using sb.nxtActI by blast
                        with ‹sub P = ksrp (σ⇘sKs p⇙(t (⟨sKs p → t⟩⇘nr⇙)))›
                          have "sub P ∈ bbrp (σ⇘the_bb⇙(t (⟨sKs p → t⟩⇘nr⇙)))"
                          using conn1A by auto
                      with ‹ p' ∈ P› have "sub P ∈ bbrp (σ⇘the_bb⇙t (⟨sKs p → t⟩⇘nr⇙)) ∧ p' ∈ P" by auto
                      ultimately obtain m where "m≥⟨sKs p → t⟩⇘nr⇙" and "(p', solve p') = bbcs (σ⇘the_bb⇙(t m))"
                        using indH by auto

                      ― ‹and due to the publisher subscriber property,›
                      ― ‹the knowledge source will receive them›
                      moreover have
                        "∄n P. ⟨sKs p → t⟩⇘nr⇙ ≤ n ∧ n ≤ m ∧ ∥sKs p∥⇘t n⇙ ∧
                        unsub P = ksrp (σ⇘sKs p⇙(t n)) ∧ p' ∈ P"
                      proof
                        assume "∃n P'. ⟨sKs p → t⟩⇘nr⇙ ≤ n ∧ n ≤ m ∧ ∥sKs p∥⇘t n⇙ ∧
                          unsub P' = ksrp (σ⇘sKs p⇙(t n)) ∧ p' ∈ P'"
                        then obtain n P' where
                          "∥sKs p∥⇘t n⇙" and "⟨sKs p → t⟩⇘nr⇙ ≤ n" and "n ≤ m" and
                          "unsub P' = ksrp (σ⇘sKs p⇙(t n))" and "p' ∈ P'" by auto
                        hence "sb.eval (sKs p) t t'' n (∃b P'. sb.pred (p'∈P') ∧b
                          [λks. unsub P' = ksrp ks]b)" by blast
                        moreover have "⟨sKs p ⇐ t⟩⇘nr⇙ ≤ n"
                          using ‹nr ≤ ⟨sKs p → t⟩⇘nr⇙› ‹⟨sKs p ⇐ t⟩⇘nr⇙ ≤ nr›
                          ‹⟨sKs p → t⟩⇘nr⇙ ≤ n› by linarith
                        with cass have "sb.eval (sKs p) t t'' n (¬b (∃b P'. (sb.pred (p'∈P')
                          ∧b [λks. unsub P' = ksrp ks]b)))"
                          using sb.globEA[of nr "sKs p" t t''
                          "¬b (∃bP'. sb.pred (p' ∈ P') ∧b [λks. unsub P' = ksrp ks]b)" n]
                          ‹∃i≥nr. ∥sKs p∥⇘t i⇙› by auto
                        ultimately show False using sb.negE by auto
                      qed
                      moreover from ‹∃i≥nr. ∥sKs p∥⇘t i⇙› have
                        "∥sKs p∥⇘t (⟨sKs p → t⟩⇘nr⇙)⇙" using sb.nxtActI by blast
                      moreover have "sub P = ksrp (σ⇘sKs p⇙(t (⟨sKs p → t⟩⇘nr⇙)))"
                        using ‹sub P = ksrp (σ⇘sKs p⇙(t (⟨sKs p → t⟩⇘nr⇙)))› .
                      moreover from ‹m≥⟨sKs p → t⟩⇘nr⇙› have "⟨sKs p → t⟩⇘nr⇙ ≤ m" by simp
                      moreover from ‹∃i≥nr. ∥sKs p∥⇘t i⇙›
                        have "⟨sKs p → t⟩⇘nr⇙≥nr" using sb.nxtActI by blast
                      hence "m≥nk" using ‹⟨sKs p → t⟩⇘nr⇙ ≤ m› ‹⟨sKs p → t⟩⇘nk⇙ ≤ nr›
                        ‹⟨sKs p → t⟩⇘nk⇙ ≥ nk› by simp
                      with case_ass have "∥sKs p∥⇘t m⇙" by simp
                      ultimately have "(p', solve p') ∈ kscs (σ⇘sKs p⇙(t m))"
                        and "∥sKs p∥⇘t m⇙"
                        using ‹t ∈ arch› msgDelivery[of t "sKs p" "⟨sKs p → t⟩⇘nr⇙" P m p' "solve p'"]
                        ‹p' ∈ P› by auto
                      hence "sb.eval (sKs p) t t'' m [λks. (p',solve p') ∈ kscs ks]b"
                        using sb.baIANow by simp
                      moreover have "m ≥ ⟨sKs p ⇐ t⟩⇘m⇙" by simp
                      moreover from ‹∥sKs p∥⇘t m⇙› have "m ≤ ⟨sKs p → t⟩⇘m⇙"
                        using sb.nxtActLe by auto
                      moreover from ‹∃i≥nr. ∥sKs p∥⇘t i⇙› have
                        "⟨sKs p ⇐ t⟩⇘nr⇙ ≤ ⟨sKs p → t⟩⇘nr⇙" by simp
                      with ‹⟨sKs p → t⟩⇘nr⇙ ≤ m› have "⟨sKs p ⇐ t⟩⇘nr⇙ ≤ m" by arith
                      ultimately show "sb.eval (sKs p) t t'' nr
                        (◇b [λks. (p',solve p') ∈ kscs ks]b)"
                        using ‹∃i≥nr. ∥sKs p∥⇘t i⇙› sb.evtIA by blast
                    qed
                  qed
                qed
                thus "sb.eval (sKs p) t t'' nr (sb.pred (p'∈P) ⟶b
                  (◇b [λks. (p',solve p') ∈ kscs ks]b))"
                  using sb.impI by auto
              qed
              thus ?thesis using sb.allI by blast
            qed

            ― ‹Thus, the knowlege source will eventually solve the problem at hand...›
            ultimately have "sb.eval (sKs p) t t'' nr
              ([λks. sub P = ksrp ks]b ∧b
              (∀b q. (sb.pred (q ∈ P) ⟶b ◇b [λks. (q, solve q) ∈ kscs ks]b)))"
              using sb.conjI by simp
            moreover from ‹∃i≥nr. ∥sKs p∥⇘t i⇙› have "∃i≥0. ∥sKs p∥⇘t i⇙" by blast
            hence "sb.eval (sKs p) t t'' nr
              (([λks. sub P = ksrp ks]b ∧b
              (∀b q. (sb.pred (q ∈ P) ⟶b
              ◇b [λks. (q, solve q) ∈ kscs ks]b))) ⟶b
              (◇b [λks. (p, solve p) = ksns ks]b))" using ‹t ∈ arch›
              sb.globEA[OF _ bhvks1[of t p "sKs p" t'' P]] sks_prob by simp
            ultimately have "sb.eval (sKs p) t t'' nr
              (◇b [λks. (p,solve(p))=ksns(ks)]b)"
              using sb.impE[of "sKs p" t t'' nr] by blast

            ― ‹and forward it to the blackboard›
            then obtain ns where "ns≥⟨sKs p → t⟩⇘nr⇙" and
              "(∃i≥ns. ∥sKs p∥⇘t i⇙ ∧
              (∀n''≥⟨sKs p ⇐ t⟩⇘ns⇙. n'' ≤ ⟨sKs p → t⟩⇘ns⇙ ⟶
              sb.eval (sKs p) t t'' n'' [λks. (p,solve(p))=ksns(ks)]b)) ∨
              ¬ (∃i≥ns. ∥sKs p∥⇘t i⇙) ∧
              sb.eval (sKs p) t t'' ns [λks. (p,solve(p))=ksns(ks)]b"
              using sb.evtEA[of nr "sKs p" t] ‹∃i≥nr. ∥sKs p∥⇘t i⇙› by blast
            moreover from ‹⟨sKs p → t⟩⇘nr⇙ ≥ nr› ‹nr≥nk› ‹ns≥⟨sKs p → t⟩⇘nr⇙›
              have "ns≥nk" by arith
            with case_ass have "∃i≥ns. ∥sKs p∥⇘t i⇙" by auto
            moreover have "ns≥⟨sKs p ⇐ t⟩⇘ns⇙" by simp
            moreover from ‹∃i≥ns. ∥sKs p∥⇘t i⇙› have "ns ≤ ⟨sKs p → t⟩⇘ns⇙"
              using sb.nxtActLe by simp
            ultimately have "sb.eval (sKs p) t t'' ns [λks. (p,solve(p))=ksns(ks)]b"
              using sb.evtEA[of nr "sKs p" t] ‹∃i≥nr. ∥sKs p∥⇘t i⇙› by blast
            with ‹∃i≥ns. ∥sKs p∥⇘t i⇙› have
              "(p,solve(p)) = ksns (σ⇘sKs p⇙(t (⟨sKs p → t⟩⇘ns⇙)))"
              using sb.baEA[of ns "sKs p" t t'' "λks. (p, solve p) = ksns ks"] by auto
            moreover from ‹∃i≥ns. ∥sKs p∥⇘t i⇙›
              have "∥sKs p∥⇘t (⟨sKs p → t⟩⇘ns⇙)⇙" using sb.nxtActI by simp
            ultimately have "(p,solve(p)) ∈ bbns (σ⇘the_bb⇙(t (⟨sKs p → t⟩⇘ns⇙)))"
              using conn1[OF pb.ts_prop(2)[of "t (⟨sKs p → t⟩⇘ns⇙)"]] by auto
            hence "pb.eval the_bb t t' ⟨sKs p → t⟩⇘ns⇙ [λbb. (p,solve(p)) ∈ bbns bb]b"
              using ‹t∈arch› pb.baI by simp

            ― ‹finally, the blackboard will forward the solution which finishes the proof.›
            with bhvbb1 have "pb.eval the_bb t t' ⟨sKs p → t⟩⇘ns⇙
              (◇b [λbb. (p, solve p) = bbcs bb]b)"
              using ‹t∈arch› pb.globE pb.impE[of the_bb t t'] by blast
            then obtain nf where "nf≥⟨sKs p → t⟩⇘ns⇙" and
              "pb.eval the_bb t t' nf [λbb. (p, solve p) = bbcs bb]b"
              using ‹t∈arch› pb.evtE[of t t' "⟨sKs p → t⟩⇘ns⇙"] by auto
            hence "(p, solve p) = bbcs (σ⇘the_bb⇙(t nf))"
              using ‹t ∈ arch› pb.baEA by auto
            moreover have "nf≥n0"
            proof -
              from ‹∃n'''≥ns. ∥sKs p∥⇘t n'''⇙› have "⟨sKs p → t⟩⇘ns⇙≥ns"
                using sb.nxtActLe by simp
              moreover from ‹nk≥n› and ‹∥sKs p∥⇘t nk⇙› have "⟨sKs p → t⟩⇘nk⇙≥nk"
                using sb.nxtActI by blast
              ultimately show ?thesis
                using ‹nf≥⟨sKs p → t⟩⇘ns⇙› ‹ns≥⟨sKs p → t⟩⇘nr⇙›
                ‹⟨sKs p → t⟩⇘nr⇙≥nr› ‹nr≥⟨sKs p → t⟩⇘nk⇙› ‹nk≥n› ‹n≥n0› by arith
            qed
            ultimately show ?thesis by auto
          qed
        qed
      qed
    qed
  qed

  theorem pSolved:
    fixes t and t'::"nat ⇒'BB" and t''::"nat ⇒'KS"
    assumes "t∈arch" and
      "∀n. (∃n'≥n. ∥sKs (bbop(σ⇘the_bb⇙(t n)))∥⇘t n'⇙)"
    shows
      "∀n. (∀P. (sub P ∈ bbrp(σ⇘the_bb⇙(t n))
        ⟶ (∀p ∈ P. (∃m≥n. (p,solve(p)) = bbcs (σ⇘the_bb⇙(t m))))))"
    using assms pSolved_Ind by blast
end

end