Session KBPs

Theory Extra

(*<*)
(*
 * Knowledge-based programs.
 * (C)opyright 2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

theory Extra
imports
  "HOL-Library.Option_ord"
  "HOL-Library.Product_Lexorder"
begin

(* Extra lemmas that are not noteworthy. *)

lemma relation_mono:
  " A  C; B  D   A × B  C × D"
  by bestsimp

lemma quotientI2:
  " x  A; X = r `` {x}   X  A // r"
  by (simp add: quotientI)

(*

Concretely enumerate all the agent action functions. Can't be too
abstract here as we want extensionality.

Introduced in the clock view.

*)

definition
  listToFun :: "('a × 'b list) list  ('a  'b) list"
where
  "listToFun xs  foldr (λ(a, acts) M. [ m(a := act) . m  M, act  acts ])
                     xs
                     [(λ_. undefined)]"

lemma listToFun_futz:
  " M  set (listToFun xs); x  fst ` set xs 
      M x  { y |y ys. (x, ys)  set xs  y  set ys}"
  unfolding listToFun_def
  apply (induct xs arbitrary: M)
   apply (simp_all add: split_def)
  apply (case_tac a)
  apply clarsimp
  apply auto
  done

lemma distinct_map_fst:
  " x  fst ` set xs; distinct (map fst xs)   (x, y)  set xs"
  by (induct xs) auto

lemma listToFun_futz_rev:
  " x. M x  (if x  fst ` set xs then { y |y ys. (x, ys)  set xs  y  set ys} else {undefined}); distinct (map fst xs) 
       M  set (listToFun xs)"
proof(induct xs arbitrary: M)
  case Nil thus ?case
    unfolding listToFun_def by simp
next
  case (Cons x xs)
  let ?M' = "M(fst x := undefined)"
  have M': "?M'  set (listToFun xs)"
    apply (rule Cons.hyps)
     prefer 2
     using Cons(3)
     apply simp
    apply (case_tac "xa = fst x")
     using Cons(3)
     apply simp
    apply (case_tac "xa  fst ` set xs")
     apply (cut_tac x=xa in Cons(2))
     apply (cases x)
     apply auto[1]
    apply (cut_tac x=xa in Cons(2))
    apply simp
    done
  then show ?case
    unfolding listToFun_def
    apply (cases x)
    apply simp
    apply (rule bexI[where x="?M'"])
     apply simp_all
    apply (rule_tac x="M a" in image_eqI)
     apply simp
    apply (cut_tac x=a in Cons(2))
    using Cons(3)
    apply clarsimp
    apply (erule disjE)
     apply simp
    apply (auto dest: distinct_map_fst)
    done
qed

definition
  listToFuns :: "('a  'b list)  'a list  ('a  'b) list"
where
  "listToFuns f  listToFun  map (λx. (x, f x))"

lemma map_id_clunky:
  "set xs = UNIV  x  fst ` set (map (λx. (x, f x)) xs)"
  apply (simp only: set_map[symmetric] map_map)
  apply simp
  done

(*

The main result is that we can freely move between representations.

*)

lemma listToFuns_ext:
  assumes xs: "set xs = UNIV"
  assumes d: "distinct xs"
  shows "g  set (listToFuns f xs)  (x. g x  set (f x))"
  unfolding listToFuns_def
  apply simp
  apply rule
   apply clarsimp
   apply (cut_tac x=x in listToFun_futz[where M=g, OF _ map_id_clunky[OF xs]])
    apply simp
   apply clarsimp
  apply (rule listToFun_futz_rev)
   using map_id_clunky[OF xs]
   apply auto[1]
   apply (rule_tac x="f xa" in exI)
    apply simp
   apply simp
  using d
  apply (simp add: distinct_map)
  apply (auto intro: inj_onI)
  done

lemma listToFun_splice:
  assumes xs: "set xs = UNIV"
  assumes d: "distinct xs"
  assumes g: "g  set (listToFuns f xs)"
  assumes h: "h  set (listToFuns f xs)"
  shows "g(x := h x)  set (listToFuns f xs)"
  using g h by (auto iff: listToFuns_ext[OF xs d])
(*<*)

end
(*>*)

Theory List_local

(*
 * Knowledge-based programs.
 * (C)opyright 2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

theory List_local
imports Extra "HOL-Library.While_Combinator"
begin


text‹Partition a list with respect to an equivalence relation.›

text‹First up: split a list according to a relation.›

abbreviation "rel_ext r  { x . r x }"

definition
  partition_split_body :: "('a × 'a  bool)  'a  'a  'a list × 'a list  'a list × 'a list"
where
  [code]: "partition_split_body r x  λy (X', xc).
            if r (x, y) then (X', List.insert y xc) else (List.insert y X', xc)"

definition
  partition_split :: "('a × 'a  bool)  'a  'a list  'a list × 'a list"
where
  [code]: "partition_split r x xs  foldr (partition_split_body r x) xs ([], [])"

lemma partition_split:
  shows "set (fst (partition_split r x xs)) = set xs - (rel_ext r `` {x})"
    and "set (snd (partition_split r x xs)) = set xs  (rel_ext r `` {x})"
proof(induct xs)
  case Nil
  { case 1 with Nil show ?case
      unfolding partition_split_def by simp }
  { case 2 with Nil show ?case
      unfolding partition_split_def by simp }
next
  case (Cons x xs)
  { case 1 with Cons show ?case
      unfolding partition_split_def
      apply simp
      apply (subst partition_split_body_def)
      apply (split prod.split)
      apply clarsimp
      apply rule
       apply clarsimp
      apply clarsimp
      unfolding Image_def
      apply auto
      done }
  { case 2 with Cons show ?case
      unfolding partition_split_def
      apply simp
      apply (subst partition_split_body_def)
      apply (split prod.split)
      apply clarsimp
      apply rule
       apply clarsimp
      apply clarsimp
      done }
qed

lemma partition_split':
  assumes "partition_split r x xs = (xxs', xec)"
  shows "set xxs' = set xs - (rel_ext r `` {x})"
    and "set xec = set xs  (rel_ext r `` {x})"
  using assms partition_split[where r=r and x=x and xs=xs]
  by simp_all

text‹Next, split an list on each of its members. For this to be
unambiguous @{term "r"} must be an equivalence relation.›

definition
  partition_aux_body :: "('a × 'a  bool)  'a list × 'a list list  'a list × 'a list list"
where
  "partition_aux_body  λr (xxs, ecs). case xxs of []  ([], []) | x # xs 
                           let (xxs', xec) = partition_split r x xs
                            in (xxs', (x # xec) # ecs)"

definition
  partition_aux :: "('a × 'a  bool)  'a list  'a list × 'a list list"
where
  [code]: "partition_aux r xs 
             while (Not  List.null  fst) (partition_aux_body r) (xs, [])"

(* FIXME move these. *)

lemma equiv_subseteq_in_sym:
  " r `` X  X;  (x, y)  r; y  X; equiv Y r; X  Y   x  X"
  unfolding equiv_def by (auto dest: symD)

lemma FIXME_refl_on_insert_absorb[simp]:
  " refl_on A r; x  A   insert x (r `` {x}) = r `` {x}"
  by (auto dest: refl_onD)

lemma equiv_subset[intro]:
  " equiv A r; B  A   equiv B (r  B × B)"
  unfolding equiv_def by (auto intro: refl_onI symI transI dest: refl_onD symD transD)

lemma FIXME_fiddle1: " x  Y; X  Y; refl_on Y r   insert x (X  r `` {x}) = (insert x X)  r `` {x}"
  by (auto dest: refl_onD)

lemma FIXME_second_fiddle:
  " (r  Y × Y) `` X  X; refl_on Z r; x  X; X  Y; Y  Z 
      (r  (Y - (X - r `` {x})) × (Y - (X - r `` {x}))) `` {x}
       = (r  X × X) `` {x}"
  by (blast dest: refl_onD)

lemma FIXME_third_fiddle:
  " (r  Y × Y) `` X  X; X  Y; x  X; y  Y - X    ;    r `` {y}  X = {} 
      (r  (Y - (X - r `` {x})) × (Y - (X - r `` {x}))) `` {y}
       = (r  (Y - X) × (Y - X)) `` {y}"
  by auto

lemma partition_aux:
  assumes equiv: "equiv X (rel_ext r)"
      and XZ: "set xs  X"
  shows "fst (partition_aux r xs) = []
        set ` set (snd (partition_aux r xs))
       = (set xs // (rel_ext r  set xs × set xs))"
proof -
  let ?b = "Not  List.null  fst"
  let ?c = "partition_aux_body r"
  let ?r' = "λA. rel_ext r  A × A"
  let ?P1 = "λ(A, B). set A  set xs"
  let ?P2 = "λ(A, B). ?r' (set xs) `` set A  set A"
  let ?P3 = "λ(A, B). set ` set B = ((set xs - set A) // ?r' (set xs - set A))"
  let ?P = "λAB. ?P1 AB  ?P2 AB  ?P3 AB"
  let ?wfr = "inv_image finite_psubset (set  fst)"
  show ?thesis
  unfolding partition_aux_def
  proof(rule while_rule[where P="?P" and r="?wfr"])
    from equiv XZ show "?P (xs, [])" by auto
  next
    fix s assume P: "?P s" and b: "?b s"

    obtain A B where s: "s = (A, B)" by (cases s) blast

    moreover
    from XZ P s have "?P1 (?c (A, B))"
      unfolding partition_aux_body_def
      by (auto simp add: partition_split' split: list.split prod.split)

    moreover
    from equiv XZ P s have "?P2 (?c s)"
      apply (cases A)
      unfolding partition_aux_body_def
      apply simp_all
      subgoal for a as
        apply (cases "partition_split r a as")
        apply (simp add: partition_split')
        unfolding equiv_def
        apply (auto dest: symD transD elim: quotientE)
        done
      done

    moreover
    have "?P3 (?c s)"
    proof -
      from b s obtain x where x: "x  set A" by (cases A) (auto iff: null_def)
      with XZ equiv P b s x
      show ?thesis
      
        unfolding partition_aux_body_def
        apply clarsimp
        apply (erule equivE)
        apply (cases A)
         apply simp
        apply simp
        apply (case_tac "partition_split r a list")
        apply clarsimp
        apply (simp add: partition_split')

        apply (subst FIXME_fiddle1[where Y=X])
           apply blast
          apply auto[1]
         apply blast

        apply rule
         apply clarsimp
         apply rule
          apply (rule_tac x=a in quotientI2)
           apply (blast dest: refl_onD)
          using XZ
          apply (auto dest: refl_onD)[1]
         apply clarsimp
         apply (erule quotientE)
         apply clarsimp
         apply (rule_tac x=xa in quotientI2)
          apply (blast dest: refl_onD)
         apply rule
          apply clarsimp
         apply clarsimp
         apply rule
          apply rule
          apply clarsimp
          apply (cut_tac X="insert a (set list)" and Y="set xs" and x=xa and y=a and r="rel_ext r  set xs × set xs" in equiv_subseteq_in_sym)
          apply simp_all
          using equiv
          apply blast
         apply clarsimp
         apply (cut_tac X="insert a (set list)" and Y="set xs" and x=xa and y=xb and r="rel_ext r  set xs × set xs" in equiv_subseteq_in_sym)
         apply simp_all
         using equiv
         apply blast

        apply (rule subsetI)
        apply (erule quotientE)
        apply (case_tac "xaa = a")
         apply auto[1]
        apply clarsimp

        apply (case_tac "xa  set list")
         apply clarsimp
         apply rule
          apply (auto dest: transD)[1]
         apply (auto dest: symD transD)[1]

        unfolding quotient_def
        apply clarsimp
        apply (erule_tac x=xa in ballE)
         unfolding Image_def
         apply clarsimp
        apply (auto dest: symD transD)  (* SLOW *)
        done
    qed

    ultimately show "?P (?c s)" by auto
  next
    fix s assume P: "?P s" and b: "¬ (?b s)"
    from b have F: "fst s = []"
      apply (cases s)
      apply simp
      apply (case_tac a)
      apply (simp_all add: List.null_def)
      done
    from equiv P F have S: "set ` set (snd s) = (set xs // ?r' (set xs))"
      apply (cases s)
      unfolding Image_def
      apply simp
      done
    from F S show "fst s = []  set ` set (snd s) = (set xs // ?r' (set xs))"
      by (simp add: prod_eqI)
  next
    show "wf ?wfr" by (blast intro: wf_finite_psubset Int_lower2 [THEN [2] wf_subset])
  next
    fix s assume P: "?P s" and b: "?b s"
    from equiv XZ P b have "set (fst (?c s))  set (fst s)"
      apply -
      apply (cases s)
      apply (simp add: Let_def)
      unfolding partition_aux_body_def
      apply clarsimp
      apply (case_tac a)
       apply (simp add: List.null_def)
      apply simp
      apply (case_tac "partition_split r aa list")
      apply (simp add: partition_split')

      unfolding equiv_def
      apply (auto dest: refl_onD)
      done
    thus "(?c s, s)  ?wfr" by auto
  qed
qed

definition
  partition :: "('a × 'a  bool)  'a list  'a list list"
where
  [code]: "partition r xs  snd (partition_aux r xs)"

lemma partition:
  assumes equiv: "equiv X (rel_ext r)"
      and xs: "set xs  X"
  shows "set ` set (partition r xs) = set xs // ((rel_ext r)  set xs × set xs)"
  unfolding partition_def
  using partition_aux[OF equiv xs] by simp

(* **************************************** *)

fun
  odlist_equal :: "'a list  'a list  bool"
where
  "odlist_equal [] [] = True"
| "odlist_equal [] ys = False"
| "odlist_equal xs [] = False"
| "odlist_equal (x # xs) (y # ys) = (x = y  odlist_equal xs ys)"

declare odlist_equal.simps [code]

lemma equal_odlist_equal[simp]:
  " distinct xs; distinct ys; sorted xs; sorted ys 
      odlist_equal xs ys  (xs = ys)"
  by (induct xs ys rule: odlist_equal.induct) (auto)

fun
  difference :: "('a :: linorder) list  'a list  'a list"
where
  "difference [] ys = []"
| "difference xs [] = xs"
| "difference (x # xs) (y # ys) =
     (if x = y then difference xs ys
               else if x < y then x # difference xs (y # ys)
                             else difference (x # xs) ys)"

declare difference.simps [code]

lemma set_difference[simp]:
  " distinct xs; distinct ys; sorted xs; sorted ys 
      set (difference xs ys) = set xs - set ys"
  by (induct xs ys rule: difference.induct) (auto)

lemma distinct_sorted_difference[simp]:
  " distinct xs; distinct ys; sorted xs; sorted ys 
      distinct (difference xs ys)  sorted (difference xs ys)"
  by (induct xs ys rule: difference.induct) (auto)

fun
  intersection :: "('a :: linorder) list  'a list  'a list"
where
  "intersection [] ys = []"
| "intersection xs [] = []"
| "intersection (x # xs) (y # ys) =
     (if x = y then x # intersection xs ys
               else if x < y then intersection xs (y # ys)
                             else intersection (x # xs) ys)"

declare intersection.simps [code]

lemma set_intersection[simp]:
  " distinct xs; distinct ys; sorted xs; sorted ys 
      set (intersection xs ys) = set xs  set ys"
  by (induct xs ys rule: intersection.induct) (auto)

lemma distinct_sorted_intersection[simp]:
  " distinct xs; distinct ys; sorted xs; sorted ys 
      distinct (intersection xs ys)  sorted (intersection xs ys)"
  by (induct xs ys rule: intersection.induct) (auto)

(* This is a variant of zipWith *)
fun
  image :: "('a :: linorder × 'b :: linorder) list  'a list  'b list"
where
  "image [] xs = []"
| "image R []  = []"
| "image ((x, y) # rs) (z # zs) =
     (if x = z then y # image rs (z # zs)
               else if x < z then image rs (z # zs)
                             else image ((x, y) # rs) zs)"

declare image.simps [code]

lemma set_image[simp]:
  " distinct R; distinct xs; sorted R; sorted xs 
      set (image R xs) = set R `` set xs"
  by (induct R xs rule: image.induct) (auto iff: less_eq_prod_def)

(* Extra lemmas that really belong in List.thy *)

lemma sorted_filter[simp]:
  "sorted xs  sorted (filter P xs)"
  by (induct xs) (auto)

lemma map_prod_eq:
  assumes f: "map fst xs = map fst ys"
      and s: "map snd xs = map snd ys"
  shows "xs = ys"
  using assms by (fact pair_list_eqI)

lemma list_choose_hd:
  assumes "x  set xs. P x"
      and "x  set xs"
  shows "P (List.hd xs)"
  using assms by (induct xs arbitrary: x) auto

end

Theory Kripke

(*<*)
(*
 * Knowledge-based programs.
 * (C)opyright 2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

theory Kripke
imports Main
begin
(*>*)

section ‹A modal logic of knowledge›

text‹

\label{sec:kbps-logic-of-knowledge}

We begin with the standard syntax and semantics of the propositional
logic of knowledge based on \emph{Kripke structures}. More extensive
treatments can be found in \citet{Lenzen:1978}, \citet{Chellas:1980},
\citet{Hintikka:1962} and \citet[Chapter~2]{FHMV:1995}.

The syntax includes one knowledge modality per agent, and one for
\emph{common knowledge} amongst a set of agents. It is parameterised
by the type @{typ "'a"} of agents and @{typ "'p"} of propositions.

›

datatype ('a, 'p) Kform
  = Kprop "'p"
  | Knot "('a, 'p) Kform"
  | Kand "('a, 'p) Kform" "('a, 'p) Kform"
  | Kknows "'a" "('a, 'p) Kform"  ("K_ _")
  | Kcknows "'a list" "('a, 'p) Kform" ("C_ _")

text‹

A Kripke structure consists of a set of \emph{worlds} of type @{typ
"'w"}, one \emph{accessibility relation} between worlds for each agent
and a \emph{valuation function} that indicates the truth of a
proposition at a world. This is a very general story that we will
quickly specialise.

›

type_synonym 'w Relation = "('w × 'w) set"

record ('a, 'p, 'w) KripkeStructure =
  worlds :: "'w set"
  relations :: "'a  'w Relation"
  valuation :: "'w  'p  bool"

definition kripke :: "('a, 'p, 'w) KripkeStructure  bool" where
  "kripke M  a. relations M a  worlds M × worlds M"

definition
  mkKripke :: "'w set  ('a  'w Relation)  ('w  'p  bool)
             ('a, 'p, 'w) KripkeStructure"
where
  "mkKripke ws rels val 
      worlds = ws, relations = λa. rels a  ws × ws, valuation = val "
(*<*)

lemma kripkeI[intro]:
  assumes "a. relations M a  worlds M × worlds M"
  shows "kripke M"
  using assms unfolding kripke_def by simp

lemma kripke_rels_worlds[dest]:
  assumes "(w, w')  relations M a"
  assumes M: "kripke M"
  shows "w  worlds M  w'  worlds M"
  using assms unfolding kripke_def by auto

lemma kripke_tc_rels_worlds[dest]:
  assumes R: "(w, w')  (a  as. relations M a)+"
  assumes M: "kripke M"
  shows "w  worlds M  w'  worlds M"
  using assms by (induct rule: trancl_induct) auto

lemma kripke_rels_trc_worlds:
  assumes R: "(w, w')  (a. relations M a)*"
  assumes w: "w  worlds M"
  assumes M: "kripke M"
  assumes W: "W = worlds M"
  shows "w'  W"
  using assms by (induct rule: rtrancl_induct) auto

lemma mkKripke_kripke[intro, simp]:
  "kripke (mkKripke ws rels val)"
  unfolding kripke_def mkKripke_def by clarsimp

lemma mkKripke_simps[simp]:
  "worlds (mkKripke ws rels val) = ws"
  "relations (mkKripke ws rels val) = (λa. rels a  ws × ws)"
  "valuation (mkKripke ws rels val) = val"
  unfolding mkKripke_def by simp_all
(*>*)

text ‹

The standard semantics for knowledge is given by taking the
accessibility relations to be equivalence relations, yielding the
S$5_n$ structures, so-called due to their axiomatisation.

›

definition S5n :: "('a, 'p, 'w) KripkeStructure  bool" where
  "S5n M  a. equiv (worlds M) (relations M a)"
(*<*)

lemma S5nI[intro]: " a. equiv (worlds M) (relations M a)   S5n M"
  by (simp add: S5n_def)

lemma S5nD[dest]: "S5n M  equiv (worlds M) (relations M a)"
  by (simp add: S5n_def)

lemma S5n_kripke[intro]: "S5n M  kripke M"
  by (rule kripkeI, erule equivE[OF S5nD], auto simp add: refl_on_def)

lemma S5n_rels_closed:
  "S5n M  relations M a `` (relations M a `` X)  relations M a `` X"
  apply (drule S5nD[where a=a])
  apply (erule equivE)
  apply (auto dest: refl_onD symD transD)
  done

(*>*)

text‹

Intuitively an agent considers two worlds to be equivalent if it
cannot distinguish between them.

›

subsection‹Satisfaction›

text‹

A formula $\phi$ is satisfied at a world $w$ in Kripke structure $M$
in the following way:›

fun models :: "('a, 'p, 'w) KripkeStructure  'w  ('a, 'p) Kform
            bool" ("(_, _  _)" [80,0,80] 80) where
  "M, w  (Kprop p) = valuation M w p"
| "M, w  (Knot φ) = (¬ M, w  φ)"
| "M, w  (Kand φ ψ) = (M, w  φ  M, w  ψ)"
| "M, w  (Ka φ) = (w'  relations M a `` {w}. M, w'  φ)"
| "M, w  (Cas φ) = (w'  (a  set as. relations M a)+ `` {w}. M, w'  φ)"

text‹

The first three clauses are standard.

The clause for @{term "Kknows a φ"} expresses the idea that an agent
knows @{term "φ"} at world @{term "w"} in structure @{term "M"} iff
@{term "φ"} is true at all worlds it considers possible.

The clause for @{term "Kcknows as φ"} captures what it means for the
set of agents @{term "as"} to commonly know @{term "φ"}; roughly,
everyone knows @{term "φ"} and knows that everyone knows it, and so
forth. Note that the transitive closure and the reflexive-transitive
closure generate the same relation due to the reflexivity of the
agents' accessibility relations; we use the former as it has a more
pleasant induction principle.

›
(*<*)

lemma S5n_rels_eq:
  assumes S5n: "S5n M"
      and ww': "(w, w')  relations M a"
  shows "relations M a `` {w} = relations M a `` {w'}"
  using S5nD[OF S5n] ww' by - (rule equiv_class_eq, blast+)

text‹

A key property of the semantics for common knowledge is that it forms
an equivalence class itself.

›

lemma tc_equiv:
  assumes E: "i. i  is  equiv A (f i)"
      and is_nempty: "is  {}"
  shows "equiv A ((iis. f i)+)"
proof(rule equivI)
  from E is_nempty show "refl_on A ((iis. f i)+)"
    unfolding equiv_def
    apply -
    apply (rule refl_onI)
    apply (rule trancl_Int_subset)
    apply (auto dest: refl_onD refl_onD1 refl_onD2)
    done
  from E show "sym ((iis. f i)+)"
    apply -
    apply (rule sym_trancl)
    unfolding equiv_def sym_def by blast
  show "trans  ((iis. f i)+)" by (rule trans_trancl)
qed

lemma S5n_tc_rels_eq:
  assumes S5n: "S5n M"
      and ww': "(w, w')  (a  as. relations M a)+"
  shows "(a  as. relations M a)+ `` {w} = (a  as. relations M a)+ `` {w'}"
  apply (cases "as = {}")
   apply fastforce
  apply (rule equiv_class_eq[OF _ ww'])
  apply (erule tc_equiv[OF S5nD[OF S5n]])
  done

text‹We can show that the standard S5 properties hold of this semantics:›

lemma S5n_knowledge_generalisation:
  " S5n M; w  worlds M. M, w  φ   M, w  Kknows a φ"
  unfolding S5n_def equiv_def refl_on_def by auto

lemma S5n_knowledge:
  " S5n M; w  worlds M; M, w  Kknows a φ   M, w  φ"
  unfolding S5n_def equiv_def refl_on_def by auto

lemma S5n_positive_introspection:
  " S5n M; w  worlds M; M, w  Kknows a φ   M, w  Kknows a (Kknows a φ)"
  unfolding S5n_def equiv_def by simp (blast dest: transD)

lemma S5n_negative_introspection:
  " S5n M; w  worlds M; M, w  Knot (Kknows a φ) 
      M, w  Kknows a (Knot (Kknows a φ))"
  unfolding S5n_def equiv_def by simp (blast dest: symD transD)
(*>*)

text‹

The relation between knowledge and common knowledge can be understood
as follows, following \citet[\S2.4]{FHMV:1995}. Firstly, that $\phi$
is common knowledge to a set of agents $as$ can be seen as asserting
that everyone in $as$ knows $\phi$ and moreover knows that it is
common knowledge amongst $as$.

›

lemma S5n_common_knowledge_fixed_point:
  assumes S5n: "S5n M"
  assumes w: "w  worlds M"
  assumes a: "a  set as"
  shows "M, w  Kcknows as φ
      M, w  Kand (Kknows a φ) (Kknows a (Kcknows as φ))"
(*<*)
proof
  assume CK: "M, w  Kcknows as φ"
  from S5n a w CK
  have "M, w  Kknows a φ"
   and "M, w  Kknows a (Kcknows as φ)"
    by (auto intro: trancl_into_trancl2)
  then show "M, w  Kand (Kknows a φ) (Kknows a (Kcknows as φ))"
    by simp
next
  assume "M, w  Kand (Kknows a φ) (Kknows a (Kcknows as φ))"
  hence "M, w  (Kknows a (Kcknows as φ))" by simp
  with S5n w show "M, w  (Kcknows as φ)" by (rule S5n_knowledge)
qed

(*>*)
text‹

Secondly we can provide an induction schema for the introduction of
common knowledge: from everyone in $as$ knows that $\phi$ implies
$\phi \land \psi$, and that $\phi$ is satisfied at world $w$, infer
that $\psi$ is common knowledge amongst $as$ at $w$.

›

lemma S5n_common_knowledge_induct:
  assumes S5n: "S5n M"
  assumes w: "w  worlds M"
  assumes E: "a  set as. w  worlds M.
                 M, w  φ  M, w  Ka (Kand φ ψ)"
  assumes p: "M, w  φ"
  shows "M, w  Cas ψ"
(*<*)
proof -
  { fix w' assume ww': "(w, w')  (xset as. relations M x)+"
    from ww' S5n E p w have "M, w'  Kand φ ψ"
      by ( induct rule: trancl_induct
         , simp_all, blast+) }
  thus ?thesis by simp
qed

(* We actually use a simpler variant. *)

lemma S5n_common_knowledge_fixed_point_simpler:
  assumes S5n: "S5n M"
      and w: "w  worlds M"
      and a: "a  set as"
  shows "M, w  Kcknows as φ  M, w  Kknows a (Kcknows as φ)"
proof
  assume CK: "M, w  Kcknows as φ"
  from S5n a w CK show "M, w  Kknows a (Kcknows as φ)"
    by (auto intro: trancl_into_trancl2)
next
  assume "M, w  Kknows a (Kcknows as φ)"
  with S5n w show "M, w  (Kcknows as φ)" by (rule S5n_knowledge)
qed

(*>*)

(* **************************************** *)

subsection ‹Generated models›

text‹

\label{sec:generated_models}

The rest of this section introduces the technical machinery we use to
relate Kripke structures.

Intuitively the truth of a formula at a world depends only on the
worlds that are reachable from it in zero or more steps, using any of
the accessibility relations at each step. Traditionally this result is
called the \emph{generated model property}
\citep[\S3.4]{Chellas:1980}.

Given the model generated by @{term "w"} in @{term "M"}:

›

definition
  gen_model :: "('a, 'p, 'w) KripkeStructure  'w  ('a, 'p, 'w) KripkeStructure"
where
  "gen_model M w 
    let ws' = worlds M  (a. relations M a)* `` {w}
     in  worlds = ws',
          relations = λa. relations M a  (ws' × ws'),
          valuation = valuation M "
(*<*)

lemma gen_model_worldsD[dest]:
  "w'  worlds (gen_model M w)  w'  worlds M"
  unfolding gen_model_def by simp

lemma gen_model_world_refl:
  "w  worlds M  w  worlds (gen_model M w)"
  unfolding gen_model_def by simp

lemma gen_model_rels_worlds[dest]:
  assumes "(w', w'')  relations (gen_model M w) a"
  shows "w'  worlds (gen_model M w)  w''  worlds (gen_model M w)"
  using assms unfolding gen_model_def by simp

lemma gen_model_rels_tc_worlds[dest]:
  assumes "(w', w'')  (a  as. relations (gen_model M w) a)+"
  shows "w''  worlds (gen_model M w)"
  using assms by (induct rule: trancl_induct) auto

lemma gen_model_rels[dest]:
  assumes "(w', w'')  relations (gen_model M w) a"
  shows "(w', w'')  relations M a"
  using assms unfolding gen_model_def by simp

lemma gen_model_worlds:
  "worlds (gen_model M w) = worlds M  (a. relations M a)* `` {w}"
  unfolding gen_model_def by simp

lemma gen_model_tc_rels[dest]:
  assumes M: "kripke M"
      and R: "(w', w'')  (a  as. relations (gen_model M w) a)+"
  shows "(w', w'')  (a  as. relations M a)+"
using R
proof(induct rule: trancl_induct)
  case (base y) with M show ?case by auto
next
  case (step y z)
  with M have "y  worlds (gen_model M w)"
          and "z  worlds (gen_model M w)" by auto
  with M step show ?case by (auto intro: trancl_into_trancl)
qed

lemma gen_model_rels_rev[dest]:
  assumes M: "kripke M"
      and "w'  worlds (gen_model M w)"
      and "(w', w'')  relations M a"
  shows "(w', w'')  relations (gen_model M w) a"
  using assms
  unfolding gen_model_def by (auto intro: rtrancl_into_rtrancl)

lemma gen_model_tc_rels_rev[dest]:
  assumes M: "kripke M"
      and R: "(w', w'')  (a  as. relations M a)+"
      and W: "w'  worlds (gen_model M w)"
  shows "(w', w'')  (a  as. relations (gen_model M w) a)+"
using R W
proof(induct rule: trancl_induct)
  case (base y) with M show ?case by auto
next
  case (step y z)
  with M have "y  worlds (gen_model M w)"
          and "z  worlds (gen_model M w)" by auto
  with M step show ?case by (auto intro: trancl_into_trancl)
qed

lemma gen_model_kripke:
  shows "kripke (gen_model M w)"
  unfolding gen_model_def by auto

(*>*)

text‹

where we take the image of @{term "w"} under the reflexive transitive
closure of the agents' relations, we can show that the satisfaction of
a formula @{term "φ"} at a world @{term "w'"} is preserved, provided
@{term "w'"} is relevant to the world @{term "w"} that the sub-model
is based upon:

›

lemma gen_model_semantic_equivalence:
  assumes M: "kripke M"
  assumes w': "w'  worlds (gen_model M w)"
  shows "M, w'  φ  (gen_model M w), w'  φ"
(*<*)
proof -
  { fix w w' assume "w'  worlds (gen_model M w)"
    hence "M, w'  φ  (gen_model M w), w'  φ"
    proof(induct φ arbitrary: w')
      case (Kknows a f w') show ?case
      proof
        assume lhs: "M, w'  Kknows a f"
        with Kknows show "gen_model M w, w'  Kknows a f" by auto
      next
        assume rhs: "gen_model M w, w'  Kknows a f"
        with M Kknows show "M, w'  Kknows a f"
          by (simp, blast)
      qed
    next
      case (Kcknows as f w') show ?case
      proof
        assume lhs: "M, w'  Kcknows as f"
        with M Kcknows show "gen_model M w, w'  Kcknows as f"
          by (simp, blast)
      next
        assume rhs: "gen_model M w, w'  Kcknows as f"
        with M Kcknows show "M, w'  Kcknows as f"
          by (simp, blast)
      qed
    qed (simp_all add: gen_model_def) }
  with w' show ?thesis by simp
qed
(*>*)

text‹

This is shown by a straightforward structural induction over the
formula @{term "φ"}.

›
(*<*)

lemma gen_model_S5n:
  assumes S5n: "S5n M"
  shows "S5n (gen_model M w)"
proof(intro S5nI equivI)
  show "n. refl_on (worlds (gen_model M w)) (relations (gen_model M w) n)"
    apply (rule equivE[OF S5nD[OF S5n]])
    by - (rule refl_onI, auto simp add: refl_on_def gen_model_def)
  show "n. sym (relations (gen_model M w) n)"
    apply (rule equivE[OF S5nD[OF S5n]])
    by (unfold gen_model_def sym_def, auto)
  show "n. trans (relations (gen_model M w) n)"
    apply (rule equivE[OF S5nD[OF S5n]])
    by - (rule transI, simp add: gen_model_def, unfold trans_def, blast)
qed

text‹

If two models generate the same sub-model for a world, they satisfy
the same formulas at that world.

›

lemma gen_model_eq:
  assumes M: "kripke M"
      and M': "kripke M'"
      and "gen_model M w = gen_model M' w"
      and "w'  worlds (gen_model M' w)"
  shows "M, w'  φ  M', w'  φ"
  using assms gen_model_semantic_equivalence[OF M, where w=w]
              gen_model_semantic_equivalence[OF M', where w=w]
  by auto

text ‹

Our final lemma in this section is technical: it allows us to move
between two Kripke structures that have the same relevant worlds.

›

lemma gen_model_subset_aux:
  assumes R: "a. relations M a  T × T = relations M' a  T × T"
      and T: "(a. relations M a)* `` {t}  T"
  shows "(x. relations M x)* `` {t}  (x. relations M' x)* `` {t}"
proof -
  { fix x assume "(t, x)  (x. relations M x)*"
    hence "(t, x)  (x. relations M' x)*"
    proof(induct rule: rtrancl_induct)
      case (step y z)
      with R T have "(y, z)  (a. relations M' a)"
        by auto (blast dest: rtrancl_trans)
      with step show ?case by (blast intro: rtrancl_trans)
    qed simp }
  thus ?thesis by blast
qed

lemma gen_model_subset:
  assumes M: "kripke M"
      and M': "kripke M'"
      and R: "a. relations M a  T × T = relations M' a  T × T"
      and tMT: "(a. relations M a)* `` {t}  T"
      and tM'T: "(a. relations M' a)* `` {t}  T"
      and tM: "t  worlds M"
      and tM': "t  worlds M'"
      and V: "valuation M = valuation M'"
  shows "gen_model M t = gen_model M' t"
proof -
  from tMT tM'T gen_model_subset_aux[OF R] gen_model_subset_aux[OF R[symmetric]]
  have F: "(a. relations M a)* `` {t} = (a. relations M' a)* `` {t}"
    by - (rule, simp_all)

  from M tMT tM have G: "(a. relations M a)* `` {t}  worlds M"
    by (auto dest: kripke_rels_trc_worlds)
  from M' tM'T tM' have H: "(a. relations M' a)* `` {t}  worlds M'"
    by (auto dest: kripke_rels_trc_worlds)

  from F G H have WORLDS: "worlds (gen_model M t) = worlds (gen_model M' t)"
    unfolding gen_model_def by (auto iff: Int_absorb1)

  have RELATIONS: "a. relations (gen_model M t) a = relations (gen_model M' t) a"
  proof (simp add: Int_absorb1 G H gen_model_def)
    fix a
    { fix a x y
      assume XY: "(x, y)  relations M a  (x. relations M x)* `` {t} × (x. relations M x)* `` {t}"
      from XY tMT
      have "(x, y)  relations M a  T × T" by blast
      with R
      have "(x, y)  relations M' a  T × T" by blast
      with F XY tM'T
      have "(x, y)  relations M' a  (x. relations M' x)* `` {t} × (x. relations M' x)* `` {t}"
        by blast }
    moreover
    { fix a x y
      assume XY: "(x, y)  relations M' a  (x. relations M' x)* `` {t} × (x. relations M' x)* `` {t}"
      from XY tM'T
      have "(x, y)  relations M' a  T × T" by blast
      with R
      have "(x, y)  relations M a  T × T" by blast
      with F XY tMT
      have "(x, y)  relations M a  (x. relations M x)* `` {t} × (x. relations M x)* `` {t}"
        by blast }
    ultimately show "Restr (relations M a) ((x. relations M x)* `` {t}) =
      Restr (relations M' a) ((x. relations M' x)* `` {t})"
    apply -
    apply rule
     apply rule
     apply auto[1]
    apply rule
    apply (case_tac x)
    apply (simp (no_asm_use))
    apply (metis Image_singleton_iff mem_Sigma_iff)
    done
  qed
  from WORLDS RELATIONS V show ?thesis
    unfolding gen_model_def by simp
qed

(*>*)

subsection ‹Simulations›

text‹

\label{sec:kripke-theory-simulations}

A \emph{simulation}, or \emph{p-morphism}, is a mapping from the
worlds of one Kripke structure to another that preserves the truth of
all formulas at related worlds \citep[\S3.4, Ex. 3.60]{Chellas:1980}.
Such a function @{term "f"} must satisfy four properties. Firstly, the
image of the set of worlds of @{term "M"} under @{term "f"} should
equal the set of worlds of @{term "M'"}.

›

definition
  sim_range :: "('a, 'p, 'w1) KripkeStructure
               ('a, 'p, 'w2) KripkeStructure  ('w1  'w2)  bool"
where
  "sim_range M M' f  worlds M' = f ` worlds M
                     (a. relations M' a  worlds M' × worlds M')"

text‹The value of a proposition should be the same at corresponding
worlds:›

definition
  sim_val :: "('a, 'p, 'w1) KripkeStructure
            ('a, 'p, 'w2) KripkeStructure  ('w1  'w2)  bool"
where
  "sim_val M M' f  u  worlds M. valuation M u = valuation M' (f u)"

text‹

If two worlds are related in @{term "M"}, then the simulation
maps them to related worlds in @{term "M'"}; intuitively the
simulation relates enough worlds. We term this the \emph{forward}
property.

›

definition
  sim_f :: "('a, 'p, 'w1) KripkeStructure
          ('a, 'p, 'w2) KripkeStructure  ('w1  'w2)  bool"
where
  "sim_f M M' f 
     a u v. (u, v)  relations M a  (f u, f v)  relations M' a"

text‹

Conversely, if two worlds @{term "f u"} and @{term "v'"} are related
in @{term "M'"}, then there is a pair of related worlds @{term "u"}
and @{term "v"} in @{term "M"} where @{term "f v = v'"}. Intuitively
the simulation makes enough distinctions. We term this the
\emph{reverse} property.

›

definition
  sim_r :: "('a, 'p, 'w1) KripkeStructure
          ('a, 'p, 'w2) KripkeStructure  ('w1  'w2)  bool"
where
  "sim_r M M' f  a. u  worlds M. v'.
              (f u, v')  relations M' a
            (v. (u, v)  relations M a  f v = v')"

definition "sim M M' f  sim_range M M' f  sim_val M M' f
                        sim_f M M' f  sim_r M M' f"
(*<*)

lemma sim_rangeI[intro]:
  " worlds M' = f ` worlds M; (a. relations M' a  worlds M' × worlds M') 
      sim_range M M' f"
  unfolding sim_range_def by simp

lemma sim_valI[intro]:
  "(u. u  worlds M  valuation M u = valuation M' (f u))
    sim_val M M' f"
  unfolding sim_val_def by simp

lemma sim_fI[intro]:
  "(a u v. (u, v)  relations M a  (f u, f v)  relations M' a)
    sim_f M M' f"
  unfolding sim_f_def by simp

lemma sim_fD:
  " (u, v)  relations M a; sim M M' f 
      (f u, f v)  relations M' a"
  unfolding sim_def sim_f_def by blast

lemma sim_rI[intro]:
  "(a u v'.
    u  worlds M; (f u, v')  relations M' a
     (v. (u, v)  relations M a  f v = v'))
   sim_r M M' f"
  unfolding sim_r_def by simp

lemma sim_rD:
  " (f u, v')  relations M' a; sim M M' f; u  worlds M 
      (v. (u, v)  relations M a  f v = v')"
  unfolding sim_def sim_r_def by blast

lemma simI[intro]:
  " sim_range M M' f; sim_val M M' f; sim_f M M' f; sim_r M M' f 
      sim M M' f"
  unfolding sim_def by simp

text‹The identity is a simulation:›

lemma sim_id: "kripke M  sim M M id"
(*<*)
  unfolding sim_def sim_r_def sim_f_def sim_range_def sim_val_def
  by auto
(*>*)

(*>*)

text‹

Due to the common knowledge modality, we need to show the simulation
properties lift through the transitive closure. In particular we can
show that forward simulation is preserved:

›

lemma sim_f_tc:
  assumes s: "sim M M' f"
  assumes uv': "(u, v)  (aas. relations M a)+"
  shows "(f u, f v)  (aas. relations M' a)+"
(*<*)
  using assms
  by - ( induct rule: trancl_induct[OF uv']
       , auto dest: sim_fD intro: trancl_into_trancl )
(*>*)
text‹

Reverse simulation also:

›

lemma sim_r_tc:
  assumes M: "kripke M"
  assumes s: "sim M M' f"
  assumes u: "u  worlds M"
  assumes fuv': "(f u, v')  (aas. relations M' a)+"
  obtains v where "f v = v'" and "(u, v)  (aas. relations M a)+"
(*<*)
proof -
  assume E: "v. f v = v'; (u, v)  (aas. relations M a)+  thesis"

  from fuv' have as_nempty: "as  {}" by auto
  from fuv' have "v. f v = v'  (u, v)  (aas. relations M a)+"
  proof(induct rule: trancl_induct)
    case (base v') with u s as_nempty show ?case
      by (blast dest: sim_rD)
  next
    case (step v' w')
    hence fuv': "(f u, v')  (aas. relations M' a)+"
      and v'w': "(v', w')  (aas. relations M' a)" by fast+
    from step
    obtain v where vv': "f v = v'"
               and uv: "(u, v)  (aas. relations M a)+"
      by blast
    from s v'w' vv' kripke_tc_rels_worlds[OF uv M]
    obtain w where ww': "f w = w'"
               and vw: "(v, w)  (aas. relations M a)"
      by (blast dest: sim_rD)
    from uv vw ww' show ?case by (blast intro: trancl_trans)
  qed
  with E show thesis by blast
qed

lemma sim_f_trc:
  assumes uv': "(u, v)  (a. relations M a)*"
      and s: "sim M M' f"
  shows "(f u, f v)  (a. relations M' a)*"
  using assms
  by - ( induct rule: rtrancl_induct[OF uv']
       , auto dest: sim_fD intro: rtrancl_into_rtrancl )

lemma sim_r_trc:
  assumes s: "sim M M' f"
      and fuv': "(f u, v')  (a. relations M' a)*"
      and M: "kripke M"
      and u: "u  worlds M"
  obtains v
    where "f v = v'"
      and "(u, v)  (a. relations M a)*"
proof -
  assume E: "v. f v = v'; (u, v)  (a. relations M a)*  thesis"
  from fuv' have "v. f v = v'  (u, v)  (a. relations M a)*"
  proof(induct rule: rtrancl_induct)
    case base show ?case by blast
  next
    case (step v' w')
    hence fuv': "(f u, v')  (a. relations M' a)*"
      and v'w': "(v', w')  (a. relations M' a)" by fast+
    from step
    obtain v where vv': "f v = v'"
               and uv: "(u, v)  (a. relations M a)*"
      by blast
    from s v'w' vv' kripke_rels_trc_worlds[OF uv u M]
    obtain w where ww': "f w = w'"
               and vw: "(v, w)  (a. relations M a)"
      by (blast dest: sim_rD)
    from uv vw ww' show ?case by (blast intro: rtrancl_trans)
  qed
  with E show thesis by blast
qed

lemma sim_trc_commute:
  assumes M: "kripke M"
      and s: "sim M M' f"
      and t: "t  worlds M"
  shows "f ` ((a. relations M a)* `` {t})
       = (a. relations M' a)* `` {f t}" (is "?lhs = ?rhs")
proof
  from M s show "?lhs  ?rhs" by (auto intro: sim_f_trc)
next
  from M s t show "?rhs  ?lhs" by (auto elim: sim_r_trc)
qed

lemma sim_kripke: " sim M M' f; kripke M   kripke M'"
  unfolding sim_def sim_range_def by (rule kripkeI, blast)

lemma sim_S5n:
  assumes S5n: "S5n M"
      and sim: "sim M M' f"
  shows "S5n M'"
proof(intro S5nI equivI)
  fix a from S5n sim show "refl_on (worlds M') (relations M' a)"
     using sim_kripke S5n_kripke
     unfolding S5n_def equiv_def sim_def sim_f_def sim_range_def
     by - (rule refl_onI, (simp, blast dest: refl_onD)+)
next
  fix a
  { fix u v assume uv: "(u, v)  relations M' a"
    from sim uv
    obtain u' where uw: "u'  worlds M"
                and fu: "u = f u'"
      unfolding sim_def sim_range_def by bestsimp
    from sim uv fu uw
    obtain v' where u'v': "(u', v')  relations M a"
                and fv: "v = f v'"
      unfolding sim_def sim_r_def sim_range_def by best
    from S5n u'v' have "(v', u')  relations M a"
      unfolding S5n_def equiv_def by (blast dest: symD)
    with sim fu fv have "(v, u)  relations M' a"
      unfolding sim_def sim_f_def by simp }
  thus "sym (relations M' a)" by (blast intro: symI)
next
  fix a
  { fix x y z
    assume xy: "(x, y)  relations M' a"
       and yz: "(y, z)  relations M' a"
    from sim xy
    obtain x' where xw: "x'  worlds M"
                and fx: "x = f x'"
      unfolding sim_def sim_range_def by bestsimp
    from sim xy fx xw
    obtain y' where x'y': "(x', y')  relations M a"
                and fy: "y = f y'"
      unfolding sim_def sim_r_def sim_range_def by best
    from S5n sim yz fy x'y'
    obtain z' where y'z': "(y', z')  relations M a"
                and fz: "z = f z'"
      unfolding sim_def sim_r_def sim_range_def by best
    from S5n x'y' y'z' have "(x', z')  relations M a"
      unfolding S5n_def equiv_def by (blast dest: transD)
    with sim fx fy fz have "(x, z)  relations M' a"
      unfolding sim_def sim_f_def by simp }
  thus "trans (relations M' a)" by (blast intro: transI)
qed

(*>*)
text‹

Finally we establish the key property of simulations, that they
preserve the satisfaction of all formulas in the following way:

›

lemma sim_semantic_equivalence:
  assumes M: "kripke M"
  assumes s: "sim M M' f"
  assumes u: "u  worlds M"
  shows "M, u  φ  M', f u  φ"
(*<*)
using u
proof(induct φ arbitrary: u)
  case (Kknows a ψ u)
  hence u: "u  worlds M" by fast
  show ?case
  proof
    assume lhs: "M, u  Kknows a ψ"
    { fix v' assume "(f u, v')  relations M' a"
      with s u obtain v where uv:  "(u, v)  relations M a"
                          and vv': "f v = v'"
        by (blast dest: sim_rD)
      from lhs uv have "M, v  ψ" by simp
      with kripke_rels_worlds[OF uv M] vv' Kknows
      have "M', v'  ψ" by auto }
    thus "M', f u  Kknows a ψ" by simp
  next
    assume rhs: "M', f u  Kknows a ψ"
    { fix v assume uv: "(u, v)  relations M a"
      with s have "(f u, f v)  relations M' a"
        by (blast dest: sim_fD)
      with rhs have "M', f v  ψ" by simp
      with kripke_rels_worlds[OF uv M] Kknows s
      have "M, v  ψ" by auto }
    thus "M, u  Kknows a ψ" by simp
  qed
next
  case (Kcknows as ψ)
  hence u: "u  worlds M" by fast
  show ?case
  proof
    assume lhs: "M, u  Kcknows as ψ"
    { fix v' assume "(f u, v')  (xset as. relations M' x)+"
      with M s u
      obtain v where uv:  "(u, v)  (xset as. relations M x)+"
                and vv': "f v = v'"
        by (blast intro: sim_r_tc)
      from uv lhs have "M, v  ψ" by simp
      with kripke_tc_rels_worlds[OF uv M] vv' Kcknows
      have "M', v'  ψ" by auto }
    thus "M', f u  Kcknows as ψ" by simp
  next
    assume rhs: "M', f u  Kcknows as ψ"
    { fix v assume uv: "(u, v)  (xset as. relations M x)+"
      with s have "(f u, f v)  (xset as. relations M' x)+"
        by (blast dest: sim_f_tc)
      with rhs have "M', f v  ψ" by simp
      with kripke_tc_rels_worlds[OF uv M] Kcknows s
      have "M, v  ψ" by auto }
    thus "M, u  Kcknows as ψ" by simp
  qed
qed (insert s,
     auto simp add: sim_range_def sim_def sim_val_def)
(*>*)

text‹

The proof is by structural induction over the formula @{term "φ"}. The
knowledge cases appeal to our two simulation preservation lemmas.

\citet{DBLP:journals/toplas/Sangiorgi09} surveys the history of
p-morphisms and the related concept of \emph{bisimulation}.

This is all we need to know about Kripke structures.

›

(*<*)
end
(*>*)

Theory Traces

(*<*)
(*
 * Knowledge-based programs.
 * (C)opyright 2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

theory Traces
imports Main
begin
(*>*)

section‹Traces›

text‹

A \emph{trace} is a non-empty sequence of states. This custom type has
the advantage over the standard HOL list type of providing a more
suitable induction rule. We use these to give a semantics to
knowledge-based programs in \S\ref{sec:kbps-theory-kbps-semantics}.

›

datatype 's Trace = tInit "'s"
                  | tStep "'s Trace" "'s" (infixl "" 65)

fun tFirst :: "'s Trace  's" where
    "tFirst (tInit s) = s"
  | "tFirst (t  s) = tFirst t"

fun tLast :: "'s Trace  's" where
    "tLast (tInit s) = s"
  | "tLast (t  s) = s"
(*<*)

lemma tLast_tInit_comp[simp]: "tLast  tInit = id"
  by (rule ext) simp
(*>*)

text‹

We provide a few of the standard list operations: @{term "tLength"},
@{term "tMap"} and @{term "tZip"}. Our later ease hinges on taking the
length of a trace to be zero-based.

›

fun tLength :: "'s Trace  nat" where
    "tLength (tInit s) = 0"
  | "tLength (t  s) = 1 + tLength t"

(*<*)
lemma tLength_0_conv:
  "(tLength t = 0)  (s. t = tInit s)"
  by (cases t) simp_all

lemma tLength_g0_conv:
  "(tLength t > 0)  (s t'. t = t'  s  tLength t = Suc (tLength t'))"
  by (cases t) simp_all

lemma tLength_Suc:
  "tLength t = Suc n  (s t'. t = t'  s  tLength t' = n)"
  by (cases t) simp_all

lemma trace_induct2[consumes 1, case_names tInit tStep]:
  assumes tLen: "tLength t = tLength t'"
      and tI: "s s'. P (tInit s) (tInit s')"
      and tS: "s s' t t'.  tLength t = tLength t'; P t t' 
                P (t  s) (t'  s')"
  shows "P t t'"
using tLen
proof (induct t arbitrary: t')
  case (tInit s t') with tI show ?case by (auto iff: tLength_0_conv)
next
  case (tStep t s t') with tS show ?case by (cases t') simp_all
qed
(*>*)

fun tMap where
  "tMap f (tInit x) = tInit (f x)"
| "tMap f (xs  x) = tMap f xs  f x"

(*<*)
lemma tLength_tMap[iff]: "tLength (tMap f t) = tLength t"
  by (induct t) simp_all

lemma tMap_is_tInit[iff]: "(tMap f t = tInit s)  (s'. t = tInit s'  f s' = s)"
  by (cases t) simp_all

lemma tInit_is_tMap[iff]: "(tInit s = tMap f t)  (s'. t = tInit s'  f s' = s)"
  by (cases t) auto

lemma tStep_is_tMap_conv[iff]:
 "(tp  s = tMap f t)  (tp' s'. t = tp'  s'  s = f s'  tp = tMap f tp')"
  by (cases t) auto

lemma tMap_is_tStep_conv[iff]:
 "(tMap f t = tp  s)  (tp' s'. t = tp'  s'  s = f s'  tMap f tp' = tp)"
  by (cases t) auto

lemma tMap_eq_imp_tLength_eq:
  assumes "tMap f t = tMap f' t'"
  shows "tLength t = tLength t'"
using assms
proof (induct t arbitrary: t')
  case (tStep tp s t')
  then obtain tp' s' where t': "t' = tp'  s'" by fastforce
  moreover with tStep have "tLength tp' = tLength tp" by simp
  with t' show ?case by simp
qed auto

lemma tMap_tFirst[iff]:
  "tFirst (tMap f t) = f (tFirst t)"
  by (induct t) simp_all

lemma tMap_tLast[iff]:
  "tLast (tMap f t) = f (tLast t)"
  by (induct t) simp_all

lemma tMap_tFirst_inv:
  assumes M: "tMap f t = tMap f' t'"
  shows "f (tFirst t) = f' (tFirst t')"
proof -
  from M have L: "tLength t = tLength t'" by (rule tMap_eq_imp_tLength_eq)
  from L M show ?thesis by (induct rule: trace_induct2, simp_all)
qed

lemma tMap_tLast_inv:
  assumes M: "tMap f t = tMap f' t'"
  shows "f (tLast t) = f' (tLast t')"
proof -
  from M have L: "tLength t = tLength t'" by (rule tMap_eq_imp_tLength_eq)
  from L M show ?thesis by (induct rule: trace_induct2, simp_all)
qed
(*>*)

fun tZip where
  "tZip f (tInit x) (tInit y) = tInit (f x y)"
| "tZip f (xs  x) (ys  y) = tZip f xs ys  f x y"
(*<*)

lemma tLength_tZip[iff]: "tLength xs = tLength ys  tLength (tZip f xs ys) = tLength xs"
  by (induct rule: trace_induct2) simp_all

(*>*)
(*<*)
end
(*>*)

Theory KBPs

(*<*)
(*
 * Knowledge-based programs.
 * (C)opyright 2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

theory KBPs
imports Kripke Traces
begin
(*>*)

section‹Knowledge-based Programs›

text ‹

\label{sec:kbps-theory-kbps-semantics}

A knowledge-based programs (KBPs) encodes the dependency of action on
knowledge by a sequence of guarded commands, and a \emph{joint
knowledge-based program} (JKBP) assigns a KBP to each agent:

›

record ('a, 'p, 'aAct) GC =
  guard  :: "('a, 'p) Kform"
  action :: "'aAct"

type_synonym ('a, 'p, 'aAct) KBP = "('a, 'p, 'aAct) GC list"
type_synonym ('a, 'p, 'aAct) JKBP = "'a  ('a, 'p, 'aAct) KBP"

text‹

We use a list of guarded commands just so we can reuse this definition
and others in algorithmic contexts; we would otherwise use a set as
there is no problem with infinite programs or actions, and we always
ignore the sequential structure.

Intuitively a KBP for an agent cannot directly evaluate the truth of
an arbitrary formula as it may depend on propositions that the agent
has no certainty about. For example, a card-playing agent cannot
determine which cards are in the deck, despite being sure that those
in her hand are not. Conversely agent $a$ can evaluate formulas of the
form @{term "Ka φ"} as these depend only on the worlds the agent thinks
is possible.

Thus we restrict the guards of the JKBP to be boolean combinations of
\emph{subjective} formulas:

›

fun subjective :: "'a  ('a, 'p) Kform  bool" where
  "subjective a (Kprop p)      = False"
| "subjective a (Knot f)       = subjective a f"
| "subjective a (Kand f g)     = (subjective a f  subjective a g)"
| "subjective a (Kknows a' f)  = (a = a')"
| "subjective a (Kcknows as f) = (a  set as)"

text‹

All JKBPs in the following sections are assumed to be subjective.

This syntactic restriction implies the desired semantic property, that
we can evaluate a guard at an arbitrary world that is compatible with
a given observation \citep[\S3]{DBLP:journals/dc/FaginHMV97}.

›

lemma S5n_subjective_eq:
  assumes S5n: "S5n M"
  assumes subj: "subjective a φ"
  assumes ww': "(w, w')  relations M a"
  shows "M, w  φ  M, w'  φ"
(*<*)
using subj ww'
proof(induct φ rule: subjective.induct[case_names Kprop Knot Kand Kknows Kcknows])
  case (Kcknows a as φ)
  hence "(w, w')  (aset as. relations M a)+" by auto
  with Kcknows S5n show ?case by (auto dest: S5n_tc_rels_eq)
qed (auto dest: S5n_rels_eq[OF S5n])

(*>*)
text‹

The proof is by induction over the formula @{term "φ"}, using the
properties of $S5_n$ Kripke structures in the knowledge cases.

We capture the fixed but arbitrary JKBP using a locale, and work in
this context for the rest of this section.

›

locale JKBP =
  fixes jkbp :: "('a, 'p, 'aAct) JKBP"
  assumes subj: "a gc. gc  set (jkbp a)  subjective a (guard gc)"

context JKBP
begin

text‹

The action of the JKBP at a world is the list of all actions that are
enabled at that world:

›

definition jAction :: "('a, 'p, 'w) KripkeStructure  'w  'a  'aAct list"
where "jAction  λM w a. [ action gc. gc  jkbp a, M, w  guard gc ]"

text‹

All of our machinery on Kripke structures lifts from the models
relation of \S\ref{sec:kbps-logic-of-knowledge} through @{term
"jAction"}, due to the subjectivity requirement. In particular, the
KBP for agent $a$ behaves the same at worlds that $a$ cannot
distinguish amongst:

›

lemma S5n_jAction_eq:
  assumes S5n: "S5n M"
  assumes ww': "(w, w')  relations M a"
  shows "jAction M w a = jAction M w' a"
(*<*)
proof -
  { fix gc assume "gc  set (jkbp a)"
    with subj have "subjective a (guard gc)" by auto
    with S5n ww' have "M, w  guard gc = M, w'  guard gc"
      by - (rule S5n_subjective_eq, simp_all) }
  thus ?thesis
    unfolding jAction_def
    by - (rule arg_cong[where f=concat], simp)
qed
(*>*)

text‹

Also the JKBP behaves the same on relevant generated models for all
agents:

›

lemma gen_model_jAction_eq:
  assumes S: "gen_model M w = gen_model M' w"
  assumes w': "w'  worlds (gen_model M' w)"
  assumes M: "kripke M"
  assumes M': "kripke M'"
  shows "jAction M w' = jAction M' w'"
(*<*)
  unfolding jAction_def
  by (auto iff: gen_model_eq[OF M M' S w'])
(*>*)

text‹

Finally, @{term "jAction"} is invariant under simulations:

›

lemma simulation_jAction_eq:
  assumes M: "kripke M"
  assumes sim: "sim M M' f"
  assumes w: "w  worlds M"
  shows "jAction M w = jAction M' (f w)"
(*<*)
  unfolding jAction_def
  using assms by (auto iff: sim_semantic_equivalence)
(*>*)

end

section‹Environments and Views›

text‹

\label{sec:kbps-theory-environments}

The previous section showed how a JKBP can be interpreted statically,
with respect to a fixed Kripke structure. As we also wish to capture
how agents interact, we adopt the \emph{interpreted systems} and
\emph{contexts} of \cite{FHMV:1995}, which we term \emph{environments}
following \cite{Ron:1996}.

A \emph{pre-environment} consists of the following:
\begin{itemize}

\item @{term "envInit"}, an arbitrary set of initial states;

\item The protocol of the environment @{term "envAction"}, which
  depends on the current state;

\item A transition function @{term "envTrans"}, which incorporates the
  environment's action and agents' behaviour into a state change; and

\item A propositional evaluation function @{term "envVal"}.

\end{itemize}
We extend the @{term "JKBP"} locale with these constants:

›

locale PreEnvironment = JKBP jkbp for jkbp :: "('a, 'p, 'aAct) JKBP"
+ fixes envInit :: "'s list"
    and envAction :: "'s  'eAct list"
    and envTrans :: "'eAct  ('a  'aAct)  's  's"
    and envVal :: "'s  'p  bool"

text‹

\label{sec:kbps-views}

We represent the possible evolutions of the system as finite sequences
of states, represented by a left-recursive type @{typ "'s Trace"} with
constructors @{term "tInit s"} and @{term "t  s"}, equipped with
@{term "tFirst"}, @{term "tLast"}, @{term "tLength"} and @{term
"tMap"} functions.

Constructing these traces requires us to determine the agents' actions
at a given state. To do so we need to find an appropriate S$5_n$
structure for interpreting @{term "jkbp"}.

Given that we want the agents to make optimal use of the information
they have access to, we allow these structures to depend on the entire
history of the system, suitably conditioned by what the agents can
observe. We capture this notion of observation with a \emph{view}
\citep{Ron:1996}, which is an arbitrary function of a trace:

›

type_synonym ('s, 'tview) View = "'s Trace  'tview"
type_synonym ('a, 's, 'tview) JointView = "'a  's Trace  'tview"

text‹

\label{sec:kbps-synchrony}

We require views to be \emph{synchronous}, i.e. that agents be able to
tell the time using their view by distinguishing two traces of
different lengths. As we will see in the next section, this guarantees
that the JKBP has an essentially unique implementation.

We extend the @{term "PreEnvironment"} locale with a view:

›

locale PreEnvironmentJView =
  PreEnvironment jkbp envInit envAction envTrans envVal
    for jkbp :: "('a, 'p, 'aAct) JKBP"
    and envInit :: "'s list"
    and envAction :: "'s  'eAct list"
    and envTrans :: "'eAct  ('a  'aAct)  's  's"
    and envVal :: "'s  'p  bool"
+ fixes jview :: "('a, 's, 'tview) JointView"
  assumes sync: "a t t'. jview a t = jview a t'  tLength t = tLength t'"

text‹

The two principle synchronous views are the clock view and the
perfect-recall view which we discuss further in
\S\ref{sec:kbps-theory-views}. We will later derive an agent's
concrete view from an instantaneous observation of the global state in
\S\ref{sec:kbps-environments}.

We build a Kripke structure from a set of traces by relating traces
that yield the same view. To obtain an S$5_n$ structure we also need a
way to evaluate propositions: we apply @{term "envVal"} to the final
state of a trace:

›

definition (in PreEnvironmentJView)
  mkM :: "'s Trace set  ('a, 'p, 's Trace) KripkeStructure"
where
  "mkM T 
       worlds = T,
        relations = λa. { (t, t') . {t, t'}  T  jview a t = jview a t' },
        valuation = envVal  tLast "
(*<*)

context PreEnvironmentJView
begin

lemma mkM_kripke[intro, simp]: "kripke (mkM T)"
  unfolding mkM_def by (rule kripkeI) fastforce

lemma mkM_S5n[intro, simp]: "S5n (mkM T)"
  unfolding mkM_def
  by (intro S5nI equivI)
     (bestsimp intro: equivI refl_onI symI transI)+

lemma mkM_simps[simp]:
  "worlds (mkM T) = T"
  " (t, t')  relations (mkM T) a   jview a t = jview a t'"
  " (t, t')  relations (mkM T) a   t  T"
  " (t, t')  relations (mkM T) a   t'  T"
  "valuation (mkM T) = envVal  tLast"
  unfolding mkM_def by simp_all

lemma mkM_rel_length[simp]:
  assumes tt': "(t, t')  relations (mkM T) a"
  shows "tLength t' = tLength t"
proof -
  from tt' have "jview a t = jview a t'" by simp
  thus ?thesis by (bestsimp dest: sync[rule_format])
qed

(*>*)
text‹

This construction supplants the role of the \emph{local states} of
\citet{FHMV:1995}.

The following section shows how we can canonically interpret the JKBP
with respect to this structure.

›

section‹Canonical Structures›

text‹

\label{sec:kbps-canonical-kripke}

Our goal in this section is to find the canonical set of traces for a
given JKBP in a particular environment. As we will see, this always
exists with respect to synchronous views.

We inductively define an \emph{interpretation} of a JKBP with respect
to an arbitrary set of traces @{term "T"} by constructing a sequence
of sets of traces of increasing length:

›

fun jkbpTn :: "nat  's Trace set  's Trace set"(*<*)("jkbpT⇘_")(*>*) where
  "jkbpT0 T     = { tInit s |s. s  set envInit }"
| "jkbpTSuc n T = { t  envTrans eact aact (tLast t) |t eact aact.
                             t  jkbpTn T  eact  set (envAction (tLast t))
                           (a. aact a  set (jAction (mkM T) t a)) }"

text‹

This model reflects the failure of any agent to provide an action as
failure of the entire system. In general @{term "envTrans"} may
incorporate a scheduler and communication failure models.

The union of this sequence gives us a closure property:

›

definition jkbpT :: "'s Trace set  's Trace set" where
  "jkbpT T  n. jkbpTn T"
(*<*)

lemma jkbpTn_length:
  "t  jkbpTn n T  tLength t = n"
  by (induct n arbitrary: t, auto)

lemma jkbpT_tLength_inv:
  " t  jkbpT T; tLength t = n   t  jkbpTn n T"
  unfolding jkbpT_def
  by (induct n arbitrary: t) (fastforce simp: jkbpTn_length)+

lemma jkbpT_traces_of_length:
   "{ t  jkbpT T . tLength t = n } = jkbpTn n T"
  using jkbpT_tLength_inv
  unfolding jkbpT_def by (bestsimp simp: jkbpTn_length)

(*>*)
text‹

We say that a set of traces @{term "T"} \emph{represents} a JKBP if it
is closed under @{term "jkbpT"}:

›

definition represents :: "'s Trace set  bool" where
  "represents T  jkbpT T = T"
(*<*)

lemma representsI:
  "jkbpT T = T  represents T"
  unfolding represents_def by simp

lemma representsD:
  "represents T  jkbpT T = T"
  unfolding represents_def by simp

(*>*)
text‹

This is the vicious cycle that we break using our assumption that the
view is synchronous. The key property of such views is that the
satisfaction of an epistemic formula is determined by the set of
traces in the model that have the same length. Lifted to @{term
"jAction"}, we have:

›

(*<*)
lemma sync_tLength_eq_trc:
  assumes "(t, t')  (aas. relations (mkM T) a)*"
  shows "tLength t = tLength t'"
  using assms by (induct rule: rtrancl_induct) auto

lemma sync_gen_model_tLength:
  assumes traces: "{ t  T . tLength t = n } = { t  T' . tLength t = n }"
      and tT: "t  { t  T . tLength t = n }"
  shows "gen_model (mkM T) t = gen_model (mkM T') t"
  apply(rule gen_model_subset[where T="{ t  T . tLength t = n }"])
  apply simp_all

  (* t ∈ T and t ∈ T' *)
  prefer 4
  using tT
  apply simp
  prefer 4
  using tT traces
  apply simp

  apply (unfold mkM_def)[1]
  using tT traces
  apply (auto)[1]

  using tT
  apply (auto dest: sync_tLength_eq_trc[where as=UNIV] kripke_rels_trc_worlds)[1]

  using tT traces
  apply (auto dest: sync_tLength_eq_trc[where as=UNIV] kripke_rels_trc_worlds)[1]

  done

(*>*)
lemma sync_jview_jAction_eq:
  assumes traces: "{ t  T . tLength t = n } = { t  T' . tLength t = n }"
  assumes tT: "t  { t  T . tLength t = n }"
  shows "jAction (mkM T) t = jAction (mkM T') t"
(*<*)
  apply (rule gen_model_jAction_eq[where w=t])
  apply (rule sync_gen_model_tLength)
  using assms
  apply (auto intro: gen_model_world_refl)
  done

(*>*)
text‹

This implies that for a synchronous view we can inductively define the
\emph{canonical traces} of a JKBP. These are the traces that a JKBP
generates when it is interpreted with respect to those very same
traces. We do this by constructing the sequence jkbpCn of
\emph{(canonical) temporal slices} similarly to @{term "jkbpTn"}:

›

fun jkbpCn :: "nat  's Trace set"(*<*)("jkbpC⇘_")(*>*) where
  "jkbpC0      = { tInit s |s. s  set envInit }"
| "jkbpCSuc n = { t  envTrans eact aact (tLast t) |t eact aact.
                             t  jkbpCn  eact  set (envAction (tLast t))
                           (a. aact a  set (jAction (mkM jkbpCn) t a)) }"

abbreviation MCn :: "nat  ('a, 'p, 's Trace) KripkeStructure"(*<*)("MC⇘_")(*>*) where
  "MCn  mkM jkbpCn"
(*<*)

lemma jkbpCn_step_inv:
  "t  s  jkbpCn (Suc n)  t  jkbpCn n"
  by (induct n arbitrary: t, (fastforce simp add: Let_def)+)

lemma jkbpCn_length[simp]:
  "t  jkbpCn n  tLength t = n"
  by (induct n arbitrary: t, (fastforce simp add: Let_def)+)

lemma jkbpCn_init_inv[intro]:
  "tInit s  jkbpCn n  s  set envInit"
   by (frule jkbpCn_length) auto

lemma jkbpCn_tFirst_init_inv[intro]:
 "t  jkbpCn n  tFirst t  set envInit"
  by (induct n arbitrary: t) (auto iff: Let_def)

(*>*)
text‹

The canonical set of traces for a JKBP with respect to a joint view is
the set of canonical traces of all lengths.

›

definition jkbpC :: "'s Trace set" where
  "jkbpC  n. jkbpCn"

abbreviation MC :: "('a, 'p, 's Trace) KripkeStructure" where
  "MC  mkM jkbpC"
(*<*)

lemma jkbpCn_jkbpC_subset:
  "jkbpCn n  jkbpC"
  unfolding jkbpC_def by blast

lemma jkbpCn_jkbpC_inc[intro]:
  "t  jkbpCn n  t  jkbpC"
  unfolding jkbpC_def by best

lemma jkbpC_tLength_inv[intro]:
  " t  jkbpC; tLength t = n   t  jkbpCn n"
  unfolding jkbpC_def
  by (induct n arbitrary: t, (fastforce simp add: Let_def)+)

lemma jkbpC_traces_of_length:
   "{ t  jkbpC . tLength t = n } = jkbpCn n"
  unfolding jkbpC_def by bestsimp

lemma jkbpC_prefix_closed[dest]:
  "t  s  jkbpC  t  jkbpC"
  apply (drule jkbpC_tLength_inv)
   apply simp
  apply (auto iff: Let_def jkbpC_def)
  done

lemma jkbpC_init[iff]:
  "tInit s  jkbpC  s  set envInit"
  unfolding jkbpC_def
  apply rule
   apply fast
  apply (subgoal_tac "tInit s  jkbpCn 0")
   apply simp
  apply (rule_tac x=0 in exI)
  apply simp_all
  done

lemma jkbpC_jkbpCn_rels:
  " (u, v)  relations MC a; tLength u = n 
     (u, v)  relations (MCn) a"
  unfolding mkM_def by (fastforce dest: sync[rule_format])

lemma jkbpC_tFirst_init_inv[intro]:
  "t  jkbpC  tFirst t  set envInit"
  unfolding jkbpC_def by blast

(*>*)
text‹

We can show that @{term "jkbpC"} represents the joint knowledge-based
program @{term "jkbp"} with respect to @{term "jview"}:

›

lemma jkbpC_jkbpCn_jAction_eq:
  assumes tCn: "t  jkbpCn"
  shows "jAction MC t = jAction MCn t"
(*<*)
  using assms
  by - (rule sync_jview_jAction_eq, auto iff: jkbpC_traces_of_length)

(*>*)
text‹›

lemma jkbpTn_jkbpCn_represents: "jkbpTn jkbpC = jkbpCn"
  by (induct n) (fastforce simp: Let_def jkbpC_jkbpCn_jAction_eq)+

text‹›

theorem jkbpC_represents: "represents jkbpC"
(*<*)
  using jkbpTn_jkbpCn_represents
  by (simp add: representsI jkbpC_def jkbpT_def)

(*>*)
text‹

We can show uniqueness too, by a similar argument:

›

theorem jkbpC_represents_uniquely:
  assumes repT: "represents T"
  shows "T = jkbpC"
(*<*)
proof -
  { fix n
    have "{ t  T . tLength t = n } = { t  jkbpC . tLength t = n }"
    proof(induct n)
      case 0
      from repT have F: "{t  T. tLength t = 0} = jkbpTn 0 T"
        by - (subst jkbpT_traces_of_length[symmetric], simp add: representsD)
      thus ?case by (simp add: jkbpC_traces_of_length)
    next
      case (Suc n)
      hence indhyp: "{t  T. tLength t = n} = jkbpCn n"
        by (simp add: jkbpC_traces_of_length)

        (* F and H are very similar. *)
      from repT have F: "n. jkbpTn n T = {t  T. tLength t = n}"
        by - (subst jkbpT_traces_of_length[symmetric], simp add: representsD)
      from indhyp F have G: "jkbpTn n T = jkbpCn n"
        by simp
      from repT have H: "n. {t  T. tLength t = n} = {t  jkbpTn n T. tLength t = n}"
        by (subst representsD[OF repT, symmetric], auto iff: jkbpT_traces_of_length jkbpTn_length)
      from F indhyp have ACTS:
        "t. t  jkbpTn n T
           jAction (mkM T) t = jAction (MCn n) t"
        by - (rule sync_jview_jAction_eq[where n="n"], auto)
      show ?case
        apply (auto iff: Let_def ACTS G H jkbpC_traces_of_length)
        apply blast+
        done
    qed }
  thus ?thesis by auto
qed
(*>*)

end (* context PreEnvironmentJView *)

text‹

Thus, at least with synchronous views, we are justified in talking
about \emph{the} representation of a JKBP in a given environment. More
generally these results are also valid for the more general notion of
\emph{provides witnesses} as shown by \citet[Lemma 7.2.4]{FHMV:1995}
and \citet{DBLP:journals/dc/FaginHMV97}: it requires only that if a
subjective knowledge formula is false on a trace then there is a trace
of the same length or less that bears witness to that effect. This is
a useful generalisation in asynchronous settings.

The next section shows how we can construct canonical representations
of JKBPs using automata.

›

(*<*)
end
(*>*)

Theory KBPsAuto

(*<*)
(*
 * Knowledge-based programs.
 * (C)opyright 2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

theory KBPsAuto
imports
  Extra
  KBPs
begin
(*>*)

section‹Automata Synthesis›

text‹

\label{sec:kbps-automata-synthesis}

Our attention now shifts to showing how we can synthesise standard
automata that \emph{implement} a JKBP under certain conditions. We
proceed by defining \emph{incremental views} following
\cite{Ron:1996}, which provide the interface between the system and
these automata. The algorithm itself is presented in
\S\ref{sec:kbps-alg}.

›

subsection‹Incremental views›

text‹

\label{sec:kbps-environments}

Intuitively an agent instantaneously observes the system state, and so
must maintain her view of the system \emph{incrementally}: her new
view must be a function of her current view and some new
observation. We allow this observation to be an arbitrary projection
@{term "envObs a"} of the system state for each agent @{term "a"}:

›

locale Environment =
  PreEnvironment jkbp envInit envAction envTrans envVal
    for jkbp :: "('a, 'p, 'aAct) JKBP"
    and envInit :: "'s list"
    and envAction :: "'s  'eAct list"
    and envTrans :: "'eAct  ('a  'aAct)  's  's"
    and envVal :: "'s  'p  bool"
+ fixes envObs :: "'a  's  'obs"

text‹

An incremental view therefore consists of two functions with these
types:

›

type_synonym ('a, 'obs, 'tv) InitialIncrJointView = "'a  'obs  'tv"
type_synonym ('a, 'obs,  'tv) IncrJointView = "'a  'obs  'tv  'tv"

text‹

These functions are required to commute with their corresponding
trace-based joint view in the obvious way:

›

locale IncrEnvironment =
  Environment jkbp envInit envAction envTrans envVal envObs
+ PreEnvironmentJView jkbp envInit envAction envTrans envVal jview
    for jkbp :: "('a, 'p, 'aAct) JKBP"
    and envInit :: "'s list"
    and envAction :: "'s  'eAct list"
    and envTrans :: "'eAct  ('a  'aAct)  's  's"
    and envVal :: "'s  'p  bool"
    and jview :: "('a, 's, 'tv) JointView"
    and envObs :: "'a  's  'obs"
+ fixes jviewInit :: "('a, 'obs, 'tv) InitialIncrJointView"
  fixes jviewIncr :: "('a, 'obs, 'tv) IncrJointView"
  assumes jviewInit: "a s. jviewInit a (envObs a s) = jview a (tInit s)"
  assumes jviewIncr: "a t s. jview a (t  s)
                             = jviewIncr a (envObs a s) (jview a t)"

text‹

Armed with these definitions, the following sections show that there
are automata that implement a JKBP in a given environment.

›

subsection‹Automata›

text‹

Our implementations of JKBPs take the form of deterministic Moore
automata, where transitions are labelled by observation and states
with the action to be performed. We will use the term \emph{protocols}
interchangeably with automata, following the KBP literature, and adopt
\emph{joint protocols} for the assignment of one such to each agent:

›

record ('obs, 'aAct, 'ps) Protocol =
  pInit :: "'obs  'ps"
  pTrans :: "'obs  'ps  'ps"
  pAct :: "'ps  'aAct list"

type_synonym ('a, 'obs, 'aAct, 'ps) JointProtocol
    = "'a  ('obs, 'aAct, 'ps) Protocol"

context IncrEnvironment
begin

text‹

To ease composition with the system we adopt the function @{term
"pInit"} which maps the initial observation to an initial automaton
state.

\citet{Ron:1996} shows that even non-deterministic JKBPs can be
implemented with deterministic transition functions; intuitively all
relevant uncertainty the agent has about the system must be encoded
into each automaton state, so there is no benefit to doing this
non-deterministically. In contrast we model the non-deterministic
choice of action by making @{term "pAct"} a relation.

Running a protocol on a trace is entirely standard, as is running a
joint protocol, and determining their actions:

›

fun runJP :: "('a, 'obs, 'aAct, 'ps) JointProtocol
            's Trace  'a  'ps"
where
  "runJP jp (tInit s) a = pInit (jp a) (envObs a s)"
| "runJP jp (t  s) a = pTrans (jp a) (envObs a s) (runJP jp t a)"

abbreviation actJP :: "('a, 'obs, 'aAct, 'ps) JointProtocol
                     's Trace  'a  'aAct list" where
  "actJP jp  λt a. pAct (jp a) (runJP jp t a)"

text ‹

Similarly to \S\ref{sec:kbps-canonical-kripke} we will reason about
the set of traces generated by a joint protocol in a fixed
environment:

›

inductive_set
  jpTraces :: "('a, 'obs, 'aAct, 'ps) JointProtocol  's Trace set"
    for jp :: "('a, 'obs, 'aAct, 'ps) JointProtocol"
where
  "s  set envInit  tInit s  jpTraces jp"
| " t  jpTraces jp; eact  set (envAction (tLast t));
     a. aact a  set (actJP jp t a); s = envTrans eact aact (tLast t) 
      t  s  jpTraces jp"
(*<*)

declare jpTraces.intros[intro]

lemma jpTraces_init_inv[dest]:
  "tInit s  jpTraces jp  s  set envInit"
  by (cases rule: jpTraces.cases) auto

lemma jpTraces_step_inv[dest]:
  "t  s  jpTraces jp
     t  jpTraces jp
      (eact  set (envAction (tLast t)).
        (aact. (a. aact a  set (actJP jp t a))
           s = envTrans eact aact (tLast t)))"
  by (cases rule: jpTraces.cases) auto

lemma jpTraces_init_length_inv:
  "t  jpTraces jp  (tLength t = 0)  (s. s  set envInit  t = tInit s)"
  by (induct t) (auto elim: jpTraces.cases)

lemma jpTraces_step_length_inv_aux:
  "t  { t  jpTraces jp . tLength t = Suc n }
     t' s. t = t'  s
             t'  jpTraces jp
             tLength t' = n
             (eact  set (envAction (tLast t')).
               (aact. (a. aact a  set (actJP jp t' a))
                  s = envTrans eact aact (tLast t')))"
  by (induct t arbitrary: n) auto

lemma jpTraces_step_length_inv:
  "{ t  jpTraces jp . tLength t = Suc n }
 = { t  s |eact aact t s. t  { t  jpTraces jp . tLength t = n }
               eact  set (envAction (tLast t))
               (a. aact a  set (actJP jp t a))
               s = envTrans eact aact (tLast t) }"
  apply (rule set_eqI)
  apply rule
   apply (drule jpTraces_step_length_inv_aux)
   apply auto
  done
(*>*)

end (* context IncrEnvironment *)

subsection‹The Implementation Relation›

text‹

\label{sec:kbps-implementation}

With this machinery in hand, we now relate automata with JKBPs. We say
a joint protocol @{term "jp"} \emph{implements} a JKBP when they
perform the same actions on the canonical of traces. Note that the
behaviour of @{term "jp"} on other traces is arbitrary.

›

context IncrEnvironment
begin

definition
  implements :: "('a, 'obs, 'aAct, 'ps) JointProtocol  bool"
where
  "implements jp  (t  jkbpC. set  actJP jp t = set  jAction MC t)"

text‹

Clearly there are environments where the canonical trace set @{term
"jkbpC"} can be generated by actions that differ from those prescribed
by the JKBP. We can show that the \emph{implements} relation is a
stronger requirement than the mere trace-inclusion required by the
\emph{represents} relation of \S\ref{sec:kbps-canonical-kripke}.

›
(*<*)

lemma implementsI[intro]:
  "(t. t  jkbpC  set  actJP jp t = set  jAction MC t)
   implements jp"
  unfolding implements_def by simp

lemma implementsE[elim]:
  assumes impl: "implements jp"
      and tC: "t  jkbpC"
     shows "set  actJP jp t = set  jAction MC t"
  using assms unfolding implements_def by simp

lemma implements_actJP_jAction:
   assumes impl: "implements jp"
       and tCn: "t  jkbpCn n"
  shows "set (actJP jp t a) = set (jAction (MCn n) t a)" (is "?lhs = ?rhs")
proof -
  from tCn have tC: "t  jkbpC" by blast
  hence "?lhs = (set  jAction MC t) a"
    using implementsE[OF impl, symmetric] by auto
  also have "... = set (jAction (MCn n) t a)"
    by (simp add: jkbpC_jkbpCn_jAction_eq[OF tCn])
  finally show ?thesis .
qed

(*>*)
lemma implements_represents:
  assumes impl: "implements jp"
  shows "represents (jpTraces jp)"
(*<*)
proof -
  { fix n
    have "{ t  jpTraces jp . tLength t = n }
        = { t  jkbpC . tLength t = n }"
    proof(induct n)
      case 0 thus ?case
        by (auto dest: jpTraces_init_length_inv iff: jkbpC_traces_of_length)
    next
      case (Suc n)
      hence indhyp: "{t  jpTraces jp . tLength t = n} = jkbpCn n"
        by (simp add: jkbpC_traces_of_length)

      have "{t  jpTraces jp. tLength t = Suc n}
          = {t  s |eact aact t s. t  jkbpCn n
                       eact  set (envAction (tLast t))
                       (a. aact a  set (actJP jp t a))
                       s = envTrans eact aact (tLast t) }"
        using indhyp by (simp add: jpTraces_step_length_inv)
      also have "... = jkbpCn (Suc n)"
        apply (auto iff: Let_def)
        apply (auto iff: implements_actJP_jAction[OF impl, symmetric])
        done
      finally show ?case by (auto iff: jkbpC_traces_of_length)
    qed }
  hence R: "jpTraces jp = jkbpC" by auto
  from R jkbpC_represents
  show "represents (jpTraces jp)" by simp
qed

lemma implements_ind_jkbpC:
  assumes acts: "a n t.
                   {t  jpTraces jp. tLength t = n} = jkbpCn n; t  jkbpCn n 
                   actJP jp t a = jAction MC t a"
  shows "implements jp"
proof -
  let ?T = "jpTraces jp"

  from acts have acts':
      "n t.  {t  jpTraces jp. tLength t = n} = jkbpCn n; t  jkbpCn n 
           actJP jp t = jAction (MCn n) t"
    by (simp only: jkbpC_jkbpCn_jAction_eq)

  from acts have acts':
      "n t.  {t  jpTraces jp. tLength t = n} = jkbpCn n; t  jkbpCn n 
           actJP jp t = jAction (MCn n) t"
    apply -
    apply (rule ext)
    apply simp
    using jkbpC_jkbpCn_jAction_eq
    apply simp
    done

  { fix n
    have "{ t  ?T . tLength t = n } = { t  jkbpC . tLength t = n }"
    proof(induct n)
      case 0 thus ?case
        by (auto dest: jpTraces_init_length_inv iff: jkbpC_traces_of_length)
    next
      case (Suc n)
      hence indhyp: "{t  ?T. tLength t = n} = jkbpCn n"
        by (simp add: jkbpC_traces_of_length)

      have "{t  jpTraces jp. tLength t = Suc n}
          = {t  s |eact aact t s. t  jkbpCn n
                       eact  set (envAction (tLast t))
                       (a. aact a  set (actJP jp t a))
                       s = envTrans eact aact (tLast t) }"
        using indhyp by (simp add: jpTraces_step_length_inv)
      also have "... = jkbpCn (Suc n)"
        apply (auto iff: Let_def)
         apply (drule acts'[OF indhyp, symmetric])
         apply auto[1]
        apply (drule acts'[OF indhyp, symmetric])
        apply auto[1]
        done
      finally show ?case
        apply (auto iff: jkbpC_traces_of_length)
        done
    qed
    hence "tjkbpCn n. actJP jp t = jAction (MCn n) t"
      apply clarsimp
      apply (rule acts')
       apply (auto iff: jkbpC_traces_of_length)
      done
    hence "tjkbpCn n. actJP jp t = jAction MC t"
      apply clarsimp
      by ( rule sync_jview_jAction_eq[where n="n"]
         , auto iff: jkbpC_traces_of_length)
  }
  thus ?thesis
    unfolding implements_def jkbpC_def
    apply clarsimp
    done
qed

(*>*)
text‹

The proof is by a straightfoward induction over the lengths of traces
generated by the joint protocol.

Our final piece of technical machinery allows us to refine automata
definitions: we say that two joint protocols are \emph{behaviourally
equivalent} if the actions they propose coincide for each canonical
trace. The implementation relation is preserved by this relation.

›

definition
  behaviourally_equiv :: "('a, 'obs, 'aAct, 'ps) JointProtocol
                         ('a, 'obs, 'aAct, 'ps') JointProtocol
                         bool"
where
  "behaviourally_equiv jp jp'  t  jkbpC. set  actJP jp t = set  actJP jp' t"

(*<*)
lemma behaviourally_equivI[intro]:
  "(t. t  jkbpC  set  actJP jp t = set  actJP jp' t)
     behaviourally_equiv jp jp'"
  unfolding behaviourally_equiv_def by simp
(*>*)

lemma behaviourally_equiv_implements:
  assumes "behaviourally_equiv jp jp'"
  shows "implements jp  implements jp'"
(*<*)
  using assms unfolding behaviourally_equiv_def implements_def by simp
(*>*)
text‹›

end (* context IncrEnvironment *)

(* **************************************** *)

subsection‹Automata using Equivalence Classes›

text‹

We now show that there is an implementation of every JKBP with respect
to every incremental synchronous view. Intuitively the states of the
automaton for agent @{term "a"} represent the equivalence classes of
traces that @{term "a"} considers possible, and the transitions update
these sets according to her KBP.

›

context IncrEnvironment
begin

definition
  mkAutoEC :: "('a, 'obs, 'aAct, 's Trace set) JointProtocol"
where
  "mkAutoEC  λa.
      pInit = λobs. { t  jkbpC . jviewInit a obs = jview a t },
       pTrans = λobs ps. { t |t t'. t  jkbpC  t'  ps
                                  jview a t = jviewIncr a obs (jview a t') },
       pAct = λps. jAction MC (SOME t. t  ps) a "

text‹

The function SOME› is Hilbert's indefinite description
operator @{term "ε"}, used here to choose an arbitrary trace from the
protocol state.

That this automaton maintains the correct equivalence class on a trace
@{term "t"} follows from an easy induction over @{term "t"}.

›

lemma mkAutoEC_ec:
  assumes "t  jkbpC"
  shows "runJP mkAutoEC t a = { t'  jkbpC . jview a t' = jview a t }"
(*<*)
  using assms
  apply (induct t)
   apply (auto simp add: mkAutoEC_def jviewInit)[1]
  apply simp
  apply (subst mkAutoEC_def)
  apply (auto iff: Let_def jviewIncr)
  done
(*>*)

text‹

We can show that the construction yields an implementation by
appealing to the previous lemma and showing that the @{term "pAct"}
functions coincide.

›

lemma mkAutoEC_implements: "implements mkAutoEC"
(*<*)
  apply (rule implements_ind_jkbpC)
  apply (subst mkAutoEC_def)
  apply simp
  apply (subgoal_tac "t  jkbpC")
   using mkAutoEC_ec
   apply simp
   apply (rule S5n_jAction_eq)
    apply simp_all
    apply (rule_tac a=t in someI2)
     apply simp_all
    unfolding mkM_def
    apply auto
   done
(*>*)

text‹

This definition leans on the canonical trace set jkbpC, and is indeed
effective: we can enumerate all canonical traces and are sure to find
one that has the view we expect. Then it is sufficient to consider
other traces of the same length due to synchrony.  We would need to do
this computation dynamically, as the automaton will (in general) have
an infinite state space.

›

end (* context IncrEnvironment *)

(* **************************************** *)

subsection‹Simulations›

text‹
\label{sec:kbps-theory-automata-env-sims}

Our goal now is to reduce the space required by the automaton
constructed by @{term "mkAutoEC"} by \emph{simulating} the equivalence
classes (\S\ref{sec:kripke-theory-simulations}).

The following locale captures the framework of \citet{Ron:1996}:

›

locale SimIncrEnvironment =
  IncrEnvironment jkbp envInit envAction envTrans envVal jview envObs
                  jviewInit jviewIncr
    for jkbp :: "('a, 'p, 'aAct) JKBP"

    and envInit :: "'s list"
    and envAction :: "'s  'eAct list"
    and envTrans :: "'eAct  ('a  'aAct)  's  's"
    and envVal :: "'s  'p  bool"
    and jview :: "('a, 's, 'tv) JointView"
    and envObs :: "'a  's  'obs"
    and jviewInit :: "('a, 'obs, 'tv) InitialIncrJointView"
    and jviewIncr :: "('a, 'obs, 'tv) IncrJointView"
+ fixes simf :: "'s Trace  'ss"
  fixes simRels :: "'a  'ss Relation"
  fixes simVal :: "'ss  'p  bool"
  assumes simf: "sim MC (mkKripke (simf ` jkbpC) simRels simVal) simf"

context SimIncrEnvironment
begin

text‹

Note that the back tick `› is Isabelle/HOL's relational image
operator. In context it says that @{term "simf"} must be a simulation
from @{term "jkbpC"} to its image under @{term "simf"}.

Firstly we lift our familiar canonical trace sets and Kripke
structures through the simulation.

›

abbreviation jkbpCSn :: "nat  'ss set"(*<*)("jkbpCS⇘_")(*>*) where
  "jkbpCSn  simf ` jkbpCn"

abbreviation jkbpCS :: "'ss set" where
  "jkbpCS  simf ` jkbpC"

abbreviation MCSn :: "nat  ('a, 'p, 'ss) KripkeStructure"(*<*)("MCS⇘_")(*>*) where
  "MCSn  mkKripke jkbpCSn simRels simVal"

abbreviation MCS :: "('a, 'p, 'ss) KripkeStructure" where
  "MCS  mkKripke jkbpCS simRels simVal"
(*<*)
lemma jkbpCSn_jkbpCS_subset:
  "jkbpCSn n  jkbpCS"
  by (rule image_mono[OF jkbpCn_jkbpC_subset])

(*>*)
text‹

We will be often be concerned with the equivalence class of traces
generated by agent @{term "a"}'s view:

›

abbreviation sim_equiv_class :: "'a  's Trace  'ss set" where
  "sim_equiv_class a t  simf ` { t'  jkbpC . jview a t' = jview a t }"

abbreviation jkbpSEC :: "'ss set set" where
  "jkbpSEC  a. sim_equiv_class a ` jkbpC"

text‹

With some effort we can show that the temporal slice of the simulated
structure is adequate for determining the actions of the JKBP. The
proof is tedious and routine, exploiting the sub-model property
(\S\ref{sec:generated_models}).

›
(*<*)

lemma sim_submodel_aux:
  assumes s: "s  worlds (MCSn n)"
  shows "gen_model MCS s = gen_model (MCSn n) s"
proof(rule gen_model_subset[where T="jkbpCSn n"])
  from s show "s  worlds MCS"
    by (simp add: subsetD[OF jkbpCSn_jkbpCS_subset])
  from s show "s  worlds (MCSn n)" by assumption
next
  fix a
  show "relations MCS a  jkbpCSn n × jkbpCSn n
      = relations (MCSn n) a  jkbpCSn n × jkbpCSn n"
    by (simp add: Int_ac Int_absorb1
                  relation_mono[OF jkbpCSn_jkbpCS_subset jkbpCSn_jkbpCS_subset])
next
  from s
  show "(a. relations (MCSn n) a)* `` {s}  jkbpCSn n"
    apply (clarsimp simp del: mkKripke_simps)
    apply (erule kripke_rels_trc_worlds)
    apply auto
    done
next
  from s obtain t
    where st: "s = simf t"
      and tCn: "t  jkbpCn n"
    by fastforce
  from tCn have tC: "t  jkbpC" by blast
  { fix t'
    assume tt': "(t, t')  (a. relations MC a)*"
    from tC tt' have t'C: "t'  jkbpC"
      by - (erule kripke_rels_trc_worlds, simp_all)
    from tCn tt' have t'Len: "tLength t' = n"
      by (auto dest: sync_tLength_eq_trc[where as=UNIV])
    from t'C t'Len have "t'  jkbpCn n"
      by - (erule jkbpC_tLength_inv) }
  hence "(a. relations MC a)* `` {t}  jkbpCn n"
    by clarsimp
  hence "simf ` ((a. relations MC a)* `` {t})  jkbpCSn n"
    by (rule image_mono)
  with st tC
  show "(a. relations MCS a)* `` {s}  jkbpCSn n"
    using sim_trc_commute[OF _ simf, where t=t]
    by simp
qed simp_all
(*>*)

lemma jkbpC_jkbpCSn_jAction_eq:
  assumes tCn: "t  jkbpCn n"
  shows "jAction MC t = jAction (MCSn n) (simf t)"
(*<*) (is "?lhs = ?rhs")
proof -
  have "?lhs = jAction MCS (simf t)"
    by (simp add: simulation_jAction_eq simf jkbpCn_jkbpC_inc[OF tCn])
  also have "... = ?rhs"
    using tCn
    by - ( rule gen_model_jAction_eq[OF sim_submodel_aux, where w="simf t"]
         , auto intro: gen_model_world_refl )
  finally show ?thesis .
qed
(*>*)

end (* context SimIncrEnvironment *)

text‹

It can be shown that a suitable simulation into a finite structure is
adequate to establish the existence of finite-state implementations
\citep[Theorem~2]{Ron:1996}: essentially we apply the simulation to
the states of @{term "mkAutoEC"}. However this result does not make it
clear how the transition function can be incrementally
constructed. One approach is to maintain @{term "jkbpC"} while
extending the automaton, which is quite space inefficient.

Intuitively we would like to compute the possible @{term
"sim_equiv_class"} successors of a given @{term "sim_equiv_class"}
without reference to @{term "jkbpC"}, and this should be possible as
the reachable simulated worlds must contain enough information to
differentiate themselves from every other simulated world (reachable
or not) that represents a trace that is observationally distinct to
their own.

This leads us to asking for some extra functionality of our
simulation, which we do in the following section.

›

subsection‹Automata using simulations›

text_raw‹
\label{sec:kbps-automata-synthesis-alg}

\begin{figure}[hp]
\begin{isabellebody}%
›
locale AlgSimIncrEnvironment =
  SimIncrEnvironment jkbp envInit envAction envTrans envVal
                     jview envObs jviewInit jviewIncr simf simRels simVal
    for jkbp :: "('a, 'p, 'aAct) JKBP"
    and envInit :: "'s list"
    and envAction :: "'s  'eAct list"
    and envTrans :: "'eAct  ('a  'aAct)  's  's"
    and envVal :: "'s  'p  bool"

    and jview :: "('a, 's, 'tv) JointView"
    and envObs :: "'a  's  'obs"
    and jviewInit :: "('a, 'obs, 'tv) InitialIncrJointView"
    and jviewIncr :: "('a, 'obs, 'tv) IncrJointView"

    and simf :: "'s Trace  'ss"
    and simRels :: "'a  'ss Relation"
    and simVal :: "'ss  'p  bool"

+ fixes simAbs :: "'rep  'ss set"

    and simObs :: "'a  'rep  'obs"
    and simInit :: "'a  'obs  'rep"
    and simTrans :: "'a  'rep  'rep list"
    and simAction :: "'a  'rep  'aAct list"

  assumes simInit:
            "a iobs. iobs  envObs a ` set envInit
                    simAbs (simInit a iobs)
                     = simf ` { t'  jkbpC. jview a t' = jviewInit a iobs }"
      and simObs:
            "a ec t. t  jkbpC  simAbs ec = sim_equiv_class a t
                    simObs a ec = envObs a (tLast t)"
      and simAction:
            "a ec t. t  jkbpC  simAbs ec = sim_equiv_class a t
                    set (simAction a ec) = set (jAction MC t a)"
      and simTrans:
            "a ec t. t  jkbpC  simAbs ec = sim_equiv_class a t
                    simAbs ` set (simTrans a ec)
                     = { sim_equiv_class a (t'  s)
                         |t' s. t'  s  jkbpC  jview a t' = jview a t }"
text_raw‹
\end{isabellebody}%
\begin{isamarkuptext}%
\caption{The SimEnvironment› locale extends the @{term
"Environment"} locale with simulation and algorithmic operations. The
backtick `› is Isabelle/HOL's image-of-a-set-under-a-function
operator.}
\label{fig:kbps-theory-auto-SimEnvironment}
\end{isamarkuptext}%
\end{figure}
›

text‹

The locale in Figure~\ref{fig:kbps-theory-auto-SimEnvironment} captures
our extra requirements of a simulation.

Firstly we relate the concrete representation @{typ "'rep"} of
equivalence classes under simulation to differ from the abstract
representation @{typ "'ss set"} using the abstraction function @{term
"simAbs"} \citep{EdR:cup98}; there is no one-size-fits-all concrete
representation, as we will see.

Secondly we ask for a function @{term "simInit a iobs"} that
faithfully generates a representation of the equivalence class of
simulated initial states that are possible for agent @{term "a"} given
the valid initial observation @{term "iobs"}.

Thirdly the @{term "simObs"} function allows us to partition the
results of @{term "simTrans"} according to the recurrent observation
that agent @{term "a"} makes of the equivalence class.

Fourthly, the function @{term "simAction"} computes a list of actions
enabled by the JKBP on a state that concretely represents a canonical
equivalence class.

Finally we expect to compute the list of represented @{term
"sim_equiv_class"} successors of a given @{term "sim_equiv_class"}
using @{term "simTrans"}.

Note that these definitions are stated relative to the environment and
the JKBP, allowing us to treat specialised cases such as broadcast
(\S\ref{sec:kbps-theory-spr-deterministic-protocols} and
\S\ref{sec:kbps-theory-spr-non-deterministic-protocols}).

With these functions in hand, we can define our desired automaton:

›

definition (in AlgSimIncrEnvironment)
  mkAutoSim :: "('a, 'obs, 'aAct, 'rep) JointProtocol"
where
  "mkAutoSim  λa.
      pInit = simInit a,
       pTrans = λobs ec. (SOME ec'. ec'  set (simTrans a ec)
                                   simObs a ec' = obs),
       pAct = simAction a "
(*<*)

context AlgSimIncrEnvironment
begin

lemma jAction_simAbs_cong:
  assumes tC: "t  jkbpC"
      and ec: "simAbs ec = sim_equiv_class a t"
      and ec': "simAbs ec = simAbs ec'"
  shows "set (simAction a ec) = set (simAction a ec')"
  using assms simAction[rule_format, where a=a and t=t] tC by simp

lemma simTrans_simAbs_cong:
  assumes tC: "t  jkbpC"
      and ec: "simAbs ec = sim_equiv_class a t"
      and ec': "simAbs ec = simAbs ec'"
  shows "simAbs ` set (simTrans a ec) = simAbs ` set (simTrans a ec')"
  using assms simTrans[rule_format, where a=a and t=t] tC by simp

lemma mkAutoSim_simps[simp]:
  "pInit (mkAutoSim a) = simInit a"
  "pTrans (mkAutoSim a) = (λobs ec. (SOME ec'. ec'  set (simTrans a ec)  simObs a ec' = obs))"
  "pAct (mkAutoSim a) = simAction a"
  unfolding mkAutoSim_def by simp_all

end (* context AlgSimIncrEnvironment *)

(*>*)
text‹

The automaton faithfully constructs the simulated equivalence class of
the given trace:

›

lemma (in AlgSimIncrEnvironment) mkAutoSim_ec:
  assumes tC: "t  jkbpC"
  shows "simAbs (runJP mkAutoSim t a) = sim_equiv_class a t"
(*<*)
using tC
proof(induct t)
  case (tInit s) thus ?case
    by (simp add: jviewInit[rule_format, symmetric] simInit)
next
  case (tStep t s)
  hence tC: "t  jkbpC" by blast

      from tC tStep
      have F: "simAbs ` set (simTrans a (runJP mkAutoSim t a))
             = { sim_equiv_class a (t'  s)
                 |t' s. t'  s  jkbpC  jview a t' = jview a t}"
        using simTrans[rule_format, where a=a and t=t and ec="runJP mkAutoSim t a"]
        apply clarsimp
        done

      from tStep
      have G: "sim_equiv_class a (t  s)
              { sim_equiv_class a (t'  s)
                |t' s. t'  s  jkbpC  jview a t' = jview a t}"
        by auto

      from F G
      have H: "sim_equiv_class a (t  s)  simAbs ` set (simTrans a (runJP mkAutoSim t a))"
        by simp

      then obtain r
        where R: "r  set (simTrans a (runJP mkAutoSim t a))"
        and S: "simAbs r = sim_equiv_class a (t  s)"
        by auto

  show ?case
  proof(simp, rule someI2)
    from R S tStep tC
    show "r  set (simTrans a (runJP mkAutoSim t a))  simObs a r = envObs a s"
      using simObs[rule_format, where t="ts" and a=a]
      apply clarsimp
      done
  next
    fix x assume x: "x  set (simTrans a (runJP mkAutoSim t a))  simObs a x = envObs a s"

    from x
    have A: "simObs a x = envObs a s" by simp

    from x
    have "simAbs x  simAbs ` set (simTrans a (runJP mkAutoSim t a))" by simp
    with tStep tC
    have "simAbs x  { sim_equiv_class a (t'  s)
                         |t' s. t'  s  jkbpC  jview a t' = jview a t}"
      using simTrans[rule_format, where a=a and t=t] by simp
    then obtain t' s'
      where X: "simAbs x = sim_equiv_class a (t'  s')"
          and Y: "t'  s'  jkbpC"
          and Z: "jview a t' = jview a t"
      by auto

    from A X Y Z
    show "simAbs x = sim_equiv_class a (t  s)"
      using simObs[rule_format, where a=a and t="t's'", symmetric]
      by (simp add: jviewIncr)
  qed
qed

(*>*)
text‹

This follows from a simple induction on @{term "t"}.

The following is a version of the Theorem 2 of \citet{Ron:1996}.

›

theorem (in AlgSimIncrEnvironment) mkAutoSim_implements:
  "implements mkAutoSim"
(*<*)
  apply rule
  apply rule
  apply (auto dest: jkbpCn_jkbpC_inc iff: mkAutoSim_ec simAction)
  done
(*>*)

text‹

The reader may care to contrast these structures with the
\emph{progression structures} of \citet{Ron:1997}, where states
contain entire Kripke structures, and expanding the automaton is
alternated with bisimulation reduction to ensure termination when a
finite-state implementation exists (see \S\ref{sec:kbps-alg-auto-min})
We also use simulations in Appendix~\ref{ch:complexity} to show the
complexity of some related model checking problems.

We now review a simple \emph{depth-first search} (DFS) theory, and an
abstraction of finite maps, before presenting the algorithm for KBP
synthesis.

\FloatBarrier

›

(*<*)
end
(*>*)

Theory DFS

(*  Title:      Presburger-Automata/DFS.thy
    Author:     Toshiaki Nishihara and Yasuhiko Minamide
    Author:     Stefan Berghofer and Alex Krauss, TU Muenchen, 2008-2009
    Author:     Peter Gammie (data refinement futz), 2010
*)

(*<*)
theory DFS
imports Main
begin
(*>*)

subsection‹Generic DFS›

text‹

\label{sec:dfs}

We use a generic DFS to construct the transitions and action function
of the implementation of the JKBP. This theory is largely due to
Stefan Berghofer and Alex Krauss
\citep{DBLP:conf/tphol/BerghoferR09}. All proofs are elided as the
fine details of how we explore the state space are inessential to the
synthesis algorithm.

The DFS itself is defined in the standard tail-recursive way:

›

partial_function (tailrec) gen_dfs where
  "gen_dfs succs ins memb S wl = (case wl of
     []  S
   | (x # xs) 
       if memb x S then gen_dfs succs ins memb S xs
       else gen_dfs succs ins memb (ins x S) (succs x @ xs))"
(*<*)
lemma gen_dfs_simps[code, simp]:
  "gen_dfs succs ins memb S [] = S"
  "gen_dfs succs ins memb S (x # xs) =
    (if memb x S then gen_dfs succs ins memb S xs
     else gen_dfs succs ins memb (ins x S) (succs x @ xs))"
  by (simp_all add: gen_dfs.simps)
(*>*)

text_raw‹
\begin{figure}
\begin{isabellebody}%
›
locale DFS =
  fixes succs :: "'a  'a list"
  and isNode :: "'a  bool"
  and invariant :: "'b  bool"
  and ins :: "'a  'b  'b"
  and memb :: "'a  'b  bool"
  and empt :: 'b
  and nodeAbs :: "'a  'c"
  assumes ins_eq: "x y S.  isNode x; isNode y; invariant S; ¬ memb y S 
                        memb x (ins y S)
                        ((nodeAbs x = nodeAbs y)  memb x S)"
  and succs: "x y.  isNode x; isNode y; nodeAbs x = nodeAbs y 
                        nodeAbs ` set (succs x) = nodeAbs ` set (succs y)"
  and empt: "x. isNode x  ¬ memb x empt"
  and succs_isNode: "x. isNode x  list_all isNode (succs x)"
  and empt_invariant: "invariant empt"
  and ins_invariant: "x S.  isNode x; invariant S; ¬ memb x S 
                         invariant (ins x S)"
  and graph_finite: "finite (nodeAbs ` { x . isNode x})"
text_raw‹
\end{isabellebody}%
\begin{isamarkuptext}%
\caption{The DFS› locale.}
\label{fig:kbps-theory-dfs-locale}
\end{isamarkuptext}%
\end{figure}
›

text‹

The proofs are carried out in the locale of
Figure~\ref{fig:kbps-theory-dfs-locale}, which details our
requirements on the parameters for the DFS to behave as one would
expect. Intuitively we are traversing a graph defined by @{term
"succs"} from some initial work list @{term "wl"}, constructing an
object of type @{typ "'b"} as we go. The function @{term "ins"}
integrates the current node into this construction. The predicate
@{term "isNode"} is invariant over the set of states reachable from
the initial work list, and is respected by @{term "empt"} and @{term
"ins"}. We can also supply an invariant for the constructed object
(@{term "invariant"}). Inside the locale, @{term "dfs"} abbreviates
@{term "gen_dfs"} partially applied to the fixed parameters.

To support our data refinement
(\S\ref{sec:kbps-automata-synthesis-alg}) we also require that the
representation of nodes be adequate via the abstraction function
@{term "nodeAbs"}, which the transition relation @{term "succs"} and
visited predicate @{term "memb"} must respect. To ensure termination
it must be the case that there are only a finite number of states,
though there might be an infinity of representations.

We characterise the DFS traversal using the reflexive
transitive closure operator:

›

definition (in DFS) reachable :: "'a set  'a set" where
  "reachable xs  {(x, y). y  set (succs x)}* `` xs"
(*<*)

context DFS
begin

definition
  "succss xs  xxs. set (succs x)"

definition
  "set_of S  {x. isNode x  memb x S}"

abbreviation
  "dfs  gen_dfs succs ins memb"

definition rel where
  "rel = inv_image finite_psubset (λS. nodeAbs ` {n.  isNode n  ¬ memb n S})"

(* Yuck, something to do with Skolems broke. *)
lemma nodeAbs_subset_grot:
  "invariant S; isNode x; list_all isNode xs; ¬memb x S
      nodeAbs ` {n . isNode n  ¬ memb n (ins x S)}
        nodeAbs ` {n . isNode n  ¬ memb n S}"
  apply rule
   apply (auto simp add: ins_eq cong: conj_cong)
  apply (subgoal_tac "nodeAbs x  nodeAbs ` {n. isNode n  ¬ memb n S}")
   apply (subgoal_tac "nodeAbs x  nodeAbs ` {n. isNode n  nodeAbs n  nodeAbs x  ¬ memb n S}")
    apply blast
   apply rule
   apply (erule imageE) back
   apply auto[1]
  apply auto[1]
  done

lemma psubsetI2: " A  B; x  A; x  B  A  B"
  by (unfold less_le) blast

lemma dfs_induct[consumes 2, case_names base step]:
  assumes S: "invariant S"
  and xs: "list_all isNode xs"
  and I1: "S. invariant S  P S []"
  and I2: "S x xs. invariant S  isNode x  list_all isNode xs 
    (memb x S  P S xs)  (¬ memb x S  P (ins x S) (succs x @ xs))  P S (x # xs)"
  shows "P S xs" using I1 I2 S xs
  apply induction_schema
  apply atomize_elim
  apply (case_tac xs, simp+)
  apply atomize_elim
  apply (rule conjI)
  apply (rule ins_invariant, assumption+)
  apply (rule succs_isNode, assumption)
  apply (relation "rel <*lex*> measure length")
  apply (simp add: wf_lex_prod rel_def)
  apply simp
  apply simp
  apply (rule disjI1)
  apply (simp add: rel_def finite_psubset_def)
  apply (rule conjI)
  apply (erule (3) nodeAbs_subset_grot)
  apply (rule finite_subset[OF _ graph_finite])
  apply auto
  done

lemma visit_subset_dfs: "invariant S  list_all isNode xs 
  isNode y  memb y S  memb y (dfs S xs)"
  by (induct S xs rule: dfs_induct) (simp_all add: ins_eq)

lemma next_subset_dfs: "invariant S  list_all isNode xs 
  x  set xs  memb x (dfs S xs)"
proof (induct S xs rule: dfs_induct)
  case (step S y xs)
  then show ?case
    by (auto simp add: visit_subset_dfs ins_eq ins_invariant succs_isNode)
qed simp

lemma succss_closed_dfs':
  "invariant ys  list_all isNode xs 
   nodeAbs ` succss (set_of ys)  nodeAbs ` (set xs  set_of ys)  nodeAbs ` succss (set_of (dfs ys xs))  nodeAbs ` set_of (dfs ys xs)"
proof(induct ys xs rule: dfs_induct)
  case (base S) thus ?case by simp
next
  case (step S x xs) thus ?case
    apply (auto simp add: succss_def set_of_def cong: conj_cong)
     apply (subgoal_tac "nodeAbs xa  nodeAbs ` (x{x. isNode x  memb x (dfs S xs)}. set (succs x))")
      apply blast
     apply blast
    apply (subgoal_tac "nodeAbs ` (x{xa. isNode xa  memb xa (ins x S)}. set (succs x))  nodeAbs ` (set (succs x)  set xs  {xa. isNode xa  memb xa (ins x S)})")
     apply blast
    apply (auto simp add: ins_eq succss_def set_of_def cong: conj_cong)
    apply (subgoal_tac "xc'. xc'  set (succs x)  nodeAbs xc' = nodeAbs xc")
     apply clarsimp
     apply (rule_tac x=xc' in image_eqI)
      apply simp
     apply simp
    apply (cut_tac x=xd and y=x in succs)
     apply simp_all
    apply (subgoal_tac "nodeAbs xc  nodeAbs ` set (succs x)")
     apply auto[1]
    apply auto[1]
   apply (subgoal_tac "nodeAbs ` set (succs xd)  nodeAbs ` (x{x. isNode x  memb x S}. set (succs x))")
    defer
    apply auto[1]
   apply (subgoal_tac "nodeAbs xc  nodeAbs ` set (succs xd)")
    defer
    apply auto[1]
   apply (subgoal_tac "nodeAbs xc  insert (nodeAbs x) (nodeAbs ` (set xs  {x. isNode x  memb x S}))")
    defer
    apply (erule rev_subsetD)
    apply (erule subset_trans)
    apply blast
   apply auto
   done
qed

lemma succss_closed_dfs: "list_all isNode xs 
  nodeAbs ` succss (set_of (dfs empt xs))  nodeAbs ` set_of (dfs empt xs)"
  apply (rule succss_closed_dfs')
  apply (rule empt_invariant)
  apply assumption
  apply (simp add: succss_def)
  apply (rule subsetI)
  apply clarsimp
  unfolding set_of_def
  using empt
  apply clarsimp
  done

definition
  "succsr  {(x, y). y  set (succs x)}"

theorem succsr_isNode:
  assumes xy: "(x, y)  succsr*"
  shows "isNode x  isNode y" using xy
proof induct
  case (step y z)
  then have "isNode y" by simp
  then have "list_all isNode (succs y)"
    by (rule succs_isNode)
  with step show ?case
    by (simp add: succsr_def list_all_iff)
qed

lemma succss_closed:
  assumes inc: "nodeAbs ` succss X  nodeAbs ` X"
      and X: "X  { x . isNode x }"
  shows "nodeAbs ` reachable X = nodeAbs ` X"
proof
  show "nodeAbs ` X  nodeAbs ` reachable X"
    unfolding reachable_def by auto
next
  show "nodeAbs ` reachable X  nodeAbs ` X"
  proof(unfold reachable_def, auto)
    fix x y
    assume y: "y  X"
    assume "(y, x)  {(x, y). y  set (succs x)}*"
    thus "nodeAbs x  nodeAbs ` X" using y
    proof induct
      case base thus ?case by simp
    next
      case (step r s)
      from X step have "isNode r"
        using succsr_isNode[where x=y and y=r]
        unfolding succsr_def by fastforce
      with inc step show ?case
        apply clarsimp
        apply (subgoal_tac "isNode x")
         apply (cut_tac x=r and y=x in succs)
         apply auto
         apply (subgoal_tac "nodeAbs s  nodeAbs ` set (succs x)")
         using X
         apply (auto simp: succss_def)
         done
     qed
   qed
qed

lemma dfs_isNode:
  assumes S: "invariant S"
      and xs: "list_all isNode xs"
  shows "set_of (dfs S xs)  {x . isNode x}"
  using assms
  by (induct S xs rule: dfs_induct) (auto simp: set_of_def)

lemma reachable_closed_dfs:
  assumes xs: "list_all isNode xs"
  shows "nodeAbs ` reachable (set xs)  nodeAbs ` set_of (dfs empt xs)"
proof -
  from xs have "reachable (set xs)  reachable (set_of (dfs empt xs))"
    apply (unfold reachable_def)
    apply (rule Image_mono)
    apply (auto simp add: set_of_def next_subset_dfs empt_invariant list_all_iff)
    done
  hence "nodeAbs ` reachable (set xs)  nodeAbs ` reachable (set_of (dfs empt xs))"
    by auto
  also from succss_closed_dfs[OF xs] have " = nodeAbs ` set_of (dfs empt xs)"
    apply (rule succss_closed)
    apply (rule dfs_isNode[OF empt_invariant xs])
    done
  finally show ?thesis .
qed

lemma reachable_succs: "reachable (set (succs x))  reachable {x}"
  by (auto simp add: reachable_def intro: converse_rtrancl_into_rtrancl)

lemma dfs_subset_reachable_visit_nodes:
  "invariant ys  list_all isNode xs 
   nodeAbs ` set_of (dfs ys xs)  nodeAbs ` (reachable (set xs)  set_of ys)"
proof(induct ys xs rule: dfs_induct)
  case (step S x xs)
  show ?case
  proof (cases "memb x S")
    case True
    with step show ?thesis by (auto simp add: reachable_def)
  next
    case False
    have "reachable (set (succs x))  reachable {x}"
      by (rule reachable_succs)
    then have "reachable (set (succs x @ xs))  reachable (set (x # xs))"
      by (auto simp add: reachable_def)
    then show ?thesis using step
      apply (auto simp add: reachable_def set_of_def cong: conj_cong)
       apply (subgoal_tac "nodeAbs xa  nodeAbs `
            ({(x, y). y  set (succs x)}* `` set xs 
             {x. isNode x  memb x S})")
        apply auto[1]
       apply auto[1]
      apply (subgoal_tac "nodeAbs xa  nodeAbs `
            ({(x, y). y  set (succs x)}* `` (set (succs x)  set xs) 
             {xa. isNode xa  memb xa (ins x S)})")
       defer
       apply auto[1]
      apply auto[1]
       apply (rule_tac x=xb in image_eqI)
        apply auto[1]
       apply auto[1]
      apply (auto iff: ins_eq)
      done
(* by (auto simp add: reachable_def ins_eq set_of_def cong: conj_cong) *)
  qed
qed (simp add: reachable_def)

theorem dfs_imp_reachable:
  assumes y: "isNode y"
      and xs: "list_all isNode xs"
      and m: "memb y (dfs empt xs)"
  shows "y'. nodeAbs y' = nodeAbs y  y'  reachable (set xs)"
proof -
  from m dfs_subset_reachable_visit_nodes [OF empt_invariant xs] y
  obtain y'
    where "nodeAbs y' = nodeAbs y"
      and "y'  reachable (set xs)"
    by (auto simp add: empt set_of_def)
  thus ?thesis by blast
qed

(*>*)
text‹

We make use of two results about the traversal. Firstly, that some
representation of each reachable node has been incorporated into the
final construction:

›

theorem (in DFS) reachable_imp_dfs:
  assumes y: "isNode y"
      and xs: "list_all isNode xs"
      and m: "y  reachable (set xs)"
  shows "y'. nodeAbs y' = nodeAbs y  memb y' (dfs empt xs)"
(*<*)
  using y m reachable_closed_dfs[OF xs]
  apply (auto simp add: set_of_def)
  apply (drule subsetD[where c="nodeAbs y"])
   apply simp
  apply auto
  done

theorem dfs_invariant' [consumes 2, case_names base step]:
  assumes S: "invariant S"
  and xs: "list_all isNode xs"
  and H: "I S"
  and I: "S x. ¬ memb x S  isNode x  invariant S  I S  I (ins x S)"
  shows "I (dfs S xs)"
proof -
  from S xs H
  have "I (dfs S xs)  invariant (dfs S xs)"
  proof (induct S xs rule: dfs_induct)
    case (step S x xs)
    show ?case
    proof (cases "memb x S")
      case False
      then show ?thesis
        apply simp
        apply (rule step)
        apply assumption
        apply (rule I)
        apply assumption
        apply (rule step)+
        done
    qed (simp add: step)
  qed simp
  then show ?thesis ..
qed

end (* context DFS *)
(*>*)

text‹

Secondly, that if an invariant holds on the initial object then it
holds on the final one:

›

theorem (in DFS) dfs_invariant:
  assumes "invariant S"
  assumes "list_all isNode xs"
  shows "invariant (dfs S xs)"
(*<*)
  using assms
  by (induct S xs rule: dfs_induct) auto
(*>*)

text‹

\FloatBarrier

›

(*<*)
end
(*>*)

Theory MapOps

(*<*)
(*
 * Knowledge-based programs.
 * (C)opyright 2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *)

theory MapOps
imports Main
begin
(*>*)

subsection‹Finite map operations›

text‹

\label{sec:kbps-theory-map-ops}

The algorithm represents an automaton as a pair of maps, which we
capture abstractly with a record and a predicate:

›

record ('m, 'k, 'e) MapOps =
  empty :: "'m"
  lookup :: "'m  'k  'e"
  update :: "'k  'e  'm  'm"

definition
  MapOps :: "('k  'kabs)  'kabs set  ('m, 'k, 'e) MapOps  bool"
where
  "MapOps α d ops 
      (k. α k  d  lookup ops (empty ops) k = None)
     (e k k' M. α k  d  α k'  d
         lookup ops (update ops k e M) k'
          = (if α k' = α k then Some e else lookup ops M k'))"
(*<*)

lemma MapOpsI[intro]:
  " k. α k  d  lookup ops (empty ops) k = None;
     e k k' M.  α k  d; α k'  d  
                 lookup ops (update ops k e M) k'
              = (if α k' = α k then Some e else lookup ops M k') 
      MapOps α d ops"
  unfolding MapOps_def by blast

lemma MapOps_emptyD:
  " α k  d; MapOps α d ops   lookup ops (empty ops) k = None"
  unfolding MapOps_def by simp

lemma MapOps_lookup_updateD:
  " α k  d; α k'  d; MapOps α d ops   lookup ops (update ops k e M) k' = (if α k' = α k then Some e else lookup ops M k')"
  unfolding MapOps_def by simp

(*>*)

text‹

The function @{term "α"} abstracts concrete keys of type @{typ "'k"},
and the parameter @{term "d"} specifies the valid abstract keys.

This approach has the advantage over a locale that we can pass records
to functions, while for a locale we would need to pass the three
functions separately (as in the DFS theory of \S\ref{sec:dfs}).

We use the following function to test for membership in the domain of
the map:

›

definition isSome :: "'a option  bool" where
  "isSome opt  case opt of None  False | Some _  True"
(*<*)

lemma isSome_simps[simp]:
  "x. isSome (Some x)"
  "x. ¬ isSome x  x = None"
  unfolding isSome_def by (auto split: option.split)

lemma isSome_eq:
  "isSome x  (y. x = Some y)"
  unfolding isSome_def by (auto split: option.split)

lemma isSomeE: " isSome x; s. x = Some s  Q   Q"
  unfolding isSome_def by (cases x) auto

end
(*>*)

Theory KBPsAlg

(*<*)
theory KBPsAlg
imports KBPsAuto DFS MapOps
begin
(*>*)

subsection‹An algorithm for automata synthesis›

text‹

\label{sec:kbps-alg}

We now show how to construct the automaton defined by @{term
"mkAutoSim"} (\S\ref{sec:kbps-automata-synthesis-alg}) using the DFS
of \S\ref{sec:dfs}.

From here on we assume that the environment consists of only a finite
set of states:

›

locale FiniteEnvironment =
  Environment jkbp envInit envAction envTrans envVal envObs
    for jkbp :: "('a, 'p, 'aAct) JKBP"
    and envInit :: "('s :: finite) list"
    and envAction :: "'s  'eAct list"
    and envTrans :: "'eAct  ('a  'aAct)  's  's"
    and envVal :: "'s  'p  bool"
    and envObs :: "'a  's  'obs"

text_raw‹
\begin{figure}[p]
\begin{isabellebody}%
›
locale Algorithm =
  FiniteEnvironment jkbp envInit envAction envTrans envVal envObs
+ AlgSimIncrEnvironment jkbp envInit envAction envTrans envVal jview envObs
               jviewInit jviewIncr
               simf simRels simVal simAbs simObs simInit simTrans simAction
    for jkbp :: "('a, 'p, 'aAct) JKBP"
    and envInit :: "('s :: finite) list"
    and envAction :: "'s  'eAct list"
    and envTrans :: "'eAct  ('a  'aAct)  's  's"
    and envVal :: "'s  'p  bool"
    and jview :: "('a, 's, 'tobs) JointView"

    and envObs :: "'a  's  'obs"
    and jviewInit :: "('a, 'obs, 'tobs) InitialIncrJointView"
    and jviewIncr :: "('a, 'obs, 'tobs) IncrJointView"

    and simf :: "'s Trace  'ss :: finite"
    and simRels :: "'a  'ss Relation"
    and simVal :: "'ss  'p  bool"

    and simAbs :: "'rep  'ss set"

    and simObs :: "'a  'rep  'obs"
    and simInit :: "'a  'obs  'rep"
    and simTrans :: "'a  'rep  'rep list"
    and simAction :: "'a  'rep  'aAct list"

+ fixes aOps :: "('ma, 'rep, 'aAct list) MapOps"
    and tOps :: "('mt, 'rep × 'obs, 'rep) MapOps"

  assumes aOps: "MapOps simAbs jkbpSEC aOps"
      and tOps: "MapOps (λk. (simAbs (fst k), snd k)) (jkbpSEC × UNIV) tOps"
text_raw‹
  \end{isabellebody}%
  \caption{The Algorithm› locale.}
  \label{fig:kbps-alg-alg-locale}
\end{figure}
›

text (in Algorithm) ‹

The @{term "Algorithm"} locale, shown in
Figure~\ref{fig:kbps-alg-alg-locale}, also extends the @{term
"AlgSimIncrEnvironment"} locale with a pair of finite map operations:
@{term "aOps"} is used to map automata states to lists of actions, and
@{term "tOps"} handles simulated transitions. In both cases the maps
are only required to work on the abstract domain of simulated
canonical traces. Note also that the space of simulated equivalence
classes of type @{typ "'ss"} must be finite, but there is no
restriction on the representation type @{typ "'rep"}.

We develop the algorithm for a single, fixed agent, which requires us
to define a new locale @{term "AlgorithmForAgent"} that extends Algorithm› with an extra parameter designating the agent:

›

locale AlgorithmForAgent =
  Algorithm jkbp envInit envAction envTrans envVal jview envObs
            jviewInit jviewIncr
            simf simRels simVal simAbs simObs simInit simTrans simAction
            aOps tOps(*<*)
    for jkbp :: "('a, 'p, 'aAct) JKBP"
    and envInit :: "('s :: finite) list"
    and envAction :: "'s  'eAct list"
    and envTrans :: "'eAct  ('a  'aAct)  's  's"
    and envVal :: "'s  'p  bool"
    and jview :: "('a, 's, 'tobs) JointView"

    and envObs :: "'a  's  'obs"
    and jviewInit :: "('a, 'obs, 'tobs) InitialIncrJointView"
    and jviewIncr :: "('a, 'obs, 'tobs) IncrJointView"

    and simf :: "'s Trace  'ss :: finite"
    and simRels :: "'a  'ss Relation"
    and simVal :: "'ss  'p  bool"

    and simAbs :: "'rep  'ss set"

    and simObs :: "'a  'rep  'obs"
    and simInit :: "'a  'obs  'rep"
    and simTrans :: "'a  'rep  'rep list"
    and simAction :: "'a  'rep  'aAct list"

    and aOps :: "('ma, 'rep, 'aAct list) MapOps"
    and tOps :: "('mt, 'rep × 'obs, 'rep) MapOps"
(*>*)

  ― ‹...›
+ fixes a :: "'a"

subsubsection‹DFS operations›

text‹

We represent the automaton under construction using a record:

›

record ('ma, 'mt) AlgState =
  aActs :: "'ma"
  aTrans :: "'mt"

context AlgorithmForAgent
begin

text‹

We instantiate the DFS theory with the following functions.

A node is an equivalence class of represented simulated traces.

›

definition k_isNode :: "'rep  bool" where
  "k_isNode ec  simAbs ec  sim_equiv_class a ` jkbpC"

text‹

The successors of a node are those produced by the simulated
transition function.

›

abbreviation k_succs :: "'rep  'rep list" where
  "k_succs  simTrans a"

text‹

The initial automaton has no transitions and no actions.

›

definition k_empt :: "('ma, 'mt) AlgState" where
  "k_empt   aActs = empty aOps, aTrans = empty tOps "

text‹

We use the domain of the action map to track the set of nodes the DFS
has visited.

›

definition k_memb :: "'rep  ('ma, 'mt) AlgState  bool" where
  "k_memb s A  isSome (lookup aOps (aActs A) s)"

text‹

We integrate a new equivalence class into the automaton by updating
the action and transition maps:

›

definition actsUpdate :: "'rep  ('ma, 'mt) AlgState  'ma" where
  "actsUpdate ec A  update aOps ec (simAction a ec) (aActs A)"

definition transUpdate :: "'rep  'rep  'mt  'mt" where
  "transUpdate ec ec' at  update tOps (ec, simObs a ec') ec' at"

definition k_ins :: "'rep  ('ma, 'mt) AlgState  ('ma, 'mt) AlgState" where
  "k_ins ec A   aActs = actsUpdate ec A,
                   aTrans = foldr (transUpdate ec) (k_succs ec) (aTrans A) "

text‹

The required properties are straightforward to show.

›

(*<*)

lemma k_isNode_cong:
  "simAbs ec' = simAbs ec  k_isNode ec'  k_isNode ec"
  unfolding k_isNode_def by simp

lemma alg_MapOps_empty[simp]:
  "k_isNode ec  lookup aOps (empty aOps) ec = None"
  "k_isNode (fst k)  lookup tOps (empty tOps) k = None"
  unfolding k_isNode_def
  using MapOps_emptyD[OF _ aOps] MapOps_emptyD[OF _ tOps] by blast+

lemma alg_aOps_lookup_update[simp]:
  " k_isNode ec; k_isNode ec'   lookup aOps (update aOps ec e M) ec' = (if simAbs ec' = simAbs ec then Some e else lookup aOps M ec')"
  unfolding k_isNode_def
  using MapOps_lookup_updateD[OF _ _ aOps] by blast

lemma alg_tOps_lookup_update[simp]:
  " k_isNode (fst k); k_isNode (fst k')   lookup tOps (update tOps k e M) k' = (if (simAbs (fst k'), snd k') = (simAbs (fst k), snd k) then Some e else lookup tOps M k')"
  unfolding k_isNode_def
  using MapOps_lookup_updateD[OF _ _ tOps] by blast

lemma k_succs_is_node[intro, simp]:
  assumes x: "k_isNode x"
  shows "list_all k_isNode (k_succs x)"
proof -
  from x obtain t
    where tC: "t  jkbpC"
      and sx: "simAbs x = sim_equiv_class a t"
    unfolding k_isNode_def by blast
  have F: "y. y  set (k_succs x)  simAbs y  simAbs ` set (k_succs x)" by simp
  show ?thesis
    using simTrans[rule_format, where a=a and t=t] tC sx
    unfolding k_isNode_def [abs_def]
    apply (auto iff: list_all_iff)
    apply (frule F)
    apply (auto)
    done
qed

lemma k_memb_empt[simp]:
  "k_isNode x  ¬k_memb x k_empt"
  unfolding k_memb_def k_empt_def by simp

(*>*)

subsubsection‹Algorithm invariant›

text‹

The invariant for the automata construction is straightforward, viz
that at each step of the process the state represents an automaton
that concords with @{term "mkAutoSim"} on the visited equivalence
classes. We also need to know that the state has preserved the @{term
"MapOps"} invariants.

›

definition k_invariant :: "('ma, 'mt) AlgState  bool" where
  "k_invariant A 
      (ec ec'. k_isNode ec  k_isNode ec'  simAbs ec' = simAbs ec
         lookup aOps (aActs A) ec = lookup aOps (aActs A) ec')
     (ec ec' obs. k_isNode ec  k_isNode ec'  simAbs ec' = simAbs ec
         lookup tOps (aTrans A) (ec, obs) = lookup tOps (aTrans A) (ec', obs))
     (ec. k_isNode ec  k_memb ec A
         (acts. lookup aOps (aActs A) ec = Some acts
                    set acts = set (simAction a ec)))
     (ec obs. k_isNode ec  k_memb ec A
               obs  simObs a ` set (simTrans a ec)
         (ec'. lookup tOps (aTrans A) (ec, obs) = Some ec'
                   simAbs ec'  simAbs ` set (simTrans a ec)
                   simObs a ec' = obs))"
(*<*)

lemma k_invariantI[intro]:
  " ec ec'.  k_isNode ec; k_isNode ec'; simAbs ec' = simAbs ec 
        lookup aOps (aActs A) ec = lookup aOps (aActs A) ec';
     ec ec' obs.  k_isNode ec; k_isNode ec'; simAbs ec' = simAbs ec 
        lookup tOps (aTrans A) (ec, obs) = lookup tOps (aTrans A) (ec', obs);
     ec.  k_isNode ec; k_memb ec A 
        acts. lookup aOps (aActs A) ec = Some acts  set acts = set (simAction a ec);
     ec obs ecs'.  k_isNode ec; k_memb ec A; obs  simObs a ` set (simTrans a ec) 
        ec'. lookup tOps (aTrans A) (ec, obs) = Some ec'
                simAbs ec'  simAbs ` set (simTrans a ec)
                simObs a ec' = obs 
   k_invariant A"
  unfolding k_invariant_def by (simp (no_asm_simp))

lemma k_invariantAOD:
  " k_isNode ec; k_isNode ec'; simAbs ec' = simAbs ec; k_invariant A 
      lookup aOps (aActs A) ec = lookup aOps (aActs A) ec'"
  unfolding k_invariant_def by blast

lemma k_invariantTOD:
  " k_isNode ec; k_isNode ec'; simAbs ec' = simAbs ec; k_invariant A 
      lookup tOps (aTrans A) (ec, obs) = lookup tOps (aTrans A) (ec', obs)"
  unfolding k_invariant_def by blast

lemma k_invariantAD:
  " k_isNode ec; k_memb ec A; k_invariant A 
      acts. lookup aOps (aActs A) ec = Some acts  set acts = set (simAction a ec)"
  unfolding k_invariant_def by blast

lemma k_invariantTD:
  " k_isNode ec; k_memb ec A; obs  simObs a ` set (simTrans a ec); k_invariant A 
      ec'. lookup tOps (aTrans A) (ec, obs) = Some ec'
              simAbs ec'  simAbs ` set (simTrans a ec)
              simObs a ec' = obs"
  unfolding k_invariant_def by blast

lemma k_invariant_empt[simp]:
  "k_invariant k_empt"
  apply rule
  apply auto
  apply (auto iff: k_empt_def)
  done

lemma k_invariant_step_new_aux:
  assumes X: "set X  set (k_succs x)"
      and x: "k_isNode x"
      and ec: "k_isNode ec"
      and ec': "simAbs ec'  simAbs ` set X"
      and S: "simAbs ec = simAbs x"
  shows "r. lookup tOps (foldr (transUpdate x) X Y) (ec, simObs a ec') = Some r
            simAbs r  simAbs ` set (k_succs ec)
            simObs a r = simObs a ec'"
using X ec'
proof(induct X arbitrary: Y)
  case Nil thus ?case by simp
next
  case (Cons y ys) show ?case
  proof(cases "simAbs ec' = simAbs y")
    case False with x ec S Cons show ?thesis
      unfolding transUpdate_def
      apply clarsimp
      unfolding k_isNode_def
      apply (erule imageE)+
      apply (cut_tac a=a and t=ta and ec=x and ec'=ec in simTrans_simAbs_cong[symmetric])
      apply simp_all
      done
  next
    case True
    with Cons have F: "simAbs y  simAbs ` set (k_succs x)"
      by auto
    from x obtain t
      where tC: "t  jkbpC"
        and x': "simAbs x = sim_equiv_class a t"
      unfolding k_isNode_def by blast
    from F obtain t' s
      where "simAbs y = sim_equiv_class a (t'  s)"
        and tsC: "t'  s  jkbpC"
        and tt': "jview a t = jview a t'"
      using simTrans[rule_format, where a=a and t=t] tC x' by auto
    with Cons.hyps[where Y11=Y] Cons(2) Cons(3) True S x ec show ?thesis
      unfolding transUpdate_def
      apply auto
      apply (subst simTrans_simAbs_cong[where t=t' and ec'=x])
       apply blast

       using x' tt'
       apply auto[1]

       apply simp

       apply (rule image_eqI[where x=y])
       apply simp
       apply simp
      using simObs[rule_format, where a=a and t="t's"]
      apply simp
      done
  qed
qed

lemma k_invariant_step_new:
  assumes x: "k_isNode x"
      and ec: "k_isNode ec"
      and ec': "ec'  set (k_succs ec)"
      and S: "simAbs ec = simAbs x"
  shows "ec''. lookup tOps (aTrans (k_ins x A)) (ec, simObs a ec') = Some ec''
               simAbs ec''  simAbs ` set (k_succs ec)
               simObs a ec'' = simObs a ec'"
proof -
  from x ec'
  have ec': "simAbs ec'  simAbs ` set (k_succs x)"
    unfolding k_isNode_def
    apply clarsimp
    apply (subst simTrans_simAbs_cong[OF _ _ S, symmetric])
    using S
    apply auto
    done
  thus ?thesis
    using k_invariant_step_new_aux[OF subset_refl x ec _ S, where ec'=ec']
    unfolding k_ins_def
    apply auto
    done
qed

lemma k_invariant_step_old_aux:
  assumes x: "k_isNode x"
      and ec: "k_isNode ec"
      and S: "simAbs ec  simAbs x"
  shows "lookup tOps (foldr (transUpdate x) X Y) (ec, obs)
       = lookup tOps Y (ec, obs)"
proof(induct X)
  case (Cons z zs) with x ec S show ?case
    by (cases "lookup tOps Y (ec, obs)") (simp_all add: transUpdate_def)
qed simp

lemma k_invariant_step_old:
  assumes x: "k_isNode x"
      and ec: "k_isNode ec"
      and S: "simAbs ec  simAbs x"
  shows "lookup tOps (aTrans (k_ins x A)) (ec, obs)
       = lookup tOps (aTrans A) (ec, obs)"
  unfolding k_ins_def
  using k_invariant_step_old_aux[OF x ec S]
  by simp

lemma k_invariant_frame:
  assumes B: "lookup tOps Y (ec, obs) = lookup tOps Y (ec', obs)"
      and x: "k_isNode x"
      and ec: "k_isNode ec"
      and ec': "k_isNode ec'"
      and S: "simAbs ec' = simAbs ec"
  shows "lookup tOps (foldr (transUpdate x) X Y) (ec, obs) = lookup tOps (foldr (transUpdate x) X Y) (ec', obs)"
  apply (induct X)
  unfolding transUpdate_def
   using B
   apply simp
  using x ec ec' S
  apply simp
  done

lemma k_invariant_step[simp]:
  assumes N: "k_isNode x"
      and I: "k_invariant A"
      and M: "¬ k_memb x A"
  shows "k_invariant (k_ins x A)"
(*<*)
proof
  fix ec ec'
  assume ec: "k_isNode ec" and ec': "k_isNode ec'" and X: "simAbs ec' = simAbs ec"
  with N show "lookup aOps (aActs (k_ins x A)) ec = lookup aOps (aActs (k_ins x A)) ec'"
    unfolding k_ins_def actsUpdate_def
    using k_invariantAOD[OF ec ec' X I]
    apply simp
    done
next
  fix ec ec' obs
  assume ec: "k_isNode ec" and ec': "k_isNode ec'" and X: "simAbs ec' = simAbs ec"
  show "lookup tOps (aTrans (k_ins x A)) (ec, obs) = lookup tOps (aTrans (k_ins x A)) (ec', obs)"
    unfolding k_ins_def
    using k_invariant_frame[OF k_invariantTOD[OF ec ec' X I] N ec ec' X]
    apply simp
    done
next
  fix ec obs ecs'
  assume n: "k_isNode ec"
    and ec: "k_memb ec (k_ins x A)"
    and obs: "obs  simObs a ` set (simTrans a ec)"
  show "ec'. lookup tOps (aTrans (k_ins x A)) (ec, obs) = Some ec'
             simAbs ec'  simAbs ` set (k_succs ec)
             simObs a ec' = obs"
  proof(cases "simAbs ec = simAbs x")
    case True with N n obs show ?thesis
      using k_invariant_step_new by auto
  next
    case False with I N n ec obs show ?thesis
      apply (simp add: k_invariant_step_old)
      apply (rule k_invariantTD)
      apply simp_all
      unfolding k_ins_def k_memb_def actsUpdate_def
      apply simp
      done
  qed
next
  fix ec
  assume n: "k_isNode ec"
     and ec: "k_memb ec (k_ins x A)"
  show "acts. lookup aOps (aActs (k_ins x A)) ec = Some acts  set acts = set (simAction a ec)"
  proof(cases "simAbs ec = simAbs x")
    case True with aOps N n show ?thesis
      unfolding k_ins_def actsUpdate_def
      apply clarsimp
      unfolding k_isNode_def
      apply clarsimp
      apply (erule jAction_simAbs_cong)
      apply auto
      done
  next
    case False with aOps N I M n ec show ?thesis
      unfolding k_ins_def actsUpdate_def
      apply simp
      apply (rule k_invariantAD)
      unfolding k_memb_def
      apply simp_all
      done
  qed
qed
(*>*)

(*>*)

text‹

Showing that the invariant holds of @{term "k_empt"} and is respected
by @{term "k_ins"} is routine.

The initial frontier is the partition of the set of initial states
under the initial observation function.

›

definition (in Algorithm) k_frontier :: "'a  'rep list" where
  "k_frontier a  map (simInit a  envObs a) envInit"
(*<*)

lemma k_frontier_is_node[intro, simp]:
  "list_all k_isNode (k_frontier a)"
  unfolding k_frontier_def
  by (auto iff: simInit list_all_iff k_isNode_def jviewInit jviewIncr)
(*>*)

end (* context AlgorithmForAgent *)

text‹

We now instantiate the @{term "DFS"} locale with respect to the @{term
"AlgorithmForAgent"} locale. The instantiated lemmas are given the
mandatory prefix KBPAlg› in the @{term "AlgorithmForAgent"}
locale.

›

sublocale AlgorithmForAgent
        < KBPAlg: DFS k_succs k_isNode k_invariant k_ins k_memb k_empt simAbs

(*<*)
  apply (unfold_locales)
  apply simp_all

  unfolding k_memb_def k_ins_def actsUpdate_def
  using aOps
  apply (auto iff: isSome_eq)[1]

  unfolding k_isNode_def
  apply clarsimp
  apply (erule simTrans_simAbs_cong)
  apply auto
  done
(*>*)

text_raw‹
\begin{figure}
\begin{isabellebody}%
›
definition
  alg_dfs :: "('ma, 'rep, 'aAct list) MapOps
          ('mt, 'rep × 'obs, 'rep) MapOps
          ('rep  'obs)
          ('rep  'rep list)
          ('rep  'aAct list)
          'rep list
          ('ma, 'mt) AlgState"
where
  "alg_dfs aOps tOps simObs simTrans simAction 
    let k_empt =  aActs = empty aOps, aTrans = empty tOps ;
       k_memb = (λs A. isSome (lookup aOps (aActs A) s));
       k_succs = simTrans;
       actsUpdate = λec A. update aOps ec (simAction ec) (aActs A);
       transUpdate = λec ec' at. update tOps (ec, simObs ec') ec' at;
       k_ins = λec A.  aActs = actsUpdate ec A,
                         aTrans = foldr (transUpdate ec) (k_succs ec) (aTrans A) 
     in gen_dfs k_succs k_ins k_memb k_empt"

text‹›

definition
  mkAlgAuto :: "('ma, 'rep, 'aAct list) MapOps
             ('mt, 'rep × 'obs, 'rep) MapOps
             ('a  'rep  'obs)
             ('a  'obs  'rep)
             ('a  'rep  'rep list)
             ('a  'rep  'aAct list)
             ('a  'rep list)
             ('a, 'obs, 'aAct, 'rep) JointProtocol"
where
  "mkAlgAuto aOps tOps simObs simInit simTrans simAction frontier  λa.
    let auto = alg_dfs aOps tOps (simObs a) (simTrans a) (simAction a)
                       (frontier a)
     in  pInit = simInit a,
          pTrans = λobs ec. the (lookup tOps (aTrans auto) (ec, obs)),
          pAct = λec. the (lookup aOps (aActs auto) ec) "

text_raw‹
  \end{isabellebody}%
  \caption{The algorithm. The function @{term "the"} projects a value from the
    @{typ "'a option"} type, diverging on @{term "None"}.}
  \label{fig:kbps-alg-algorithm}
\end{figure}
›
(*<*)
lemma mkAutoSim_simps[simp]:
  "pInit (mkAlgAuto aOps tOps simObs simInit simTrans simAction frontier a) = simInit a"
  "pTrans (mkAlgAuto aOps tOps simObs simInit simTrans simAction frontier a)
 = (λobs ec. the (lookup tOps (aTrans (alg_dfs aOps tOps (simObs a) (simTrans a) (simAction a) (frontier a))) (ec, obs)))"
  "pAct (mkAlgAuto aOps tOps simObs simInit simTrans simAction frontier a)
 = (λec. the (lookup aOps (aActs (alg_dfs aOps tOps (simObs a) (simTrans a) (simAction a) (frontier a))) ec))"
  unfolding mkAlgAuto_def
  apply (simp_all add: Let_def)
  done

(* Later we want to show that a particular DFS implementation does the
right thing. *)

definition
  alg_mk_auto :: "('ma, 'rep, 'aAct list) MapOps
                 ('mt, 'rep × 'obs, 'rep) MapOps
                 ('obs  'rep)
                 ('ma, 'mt) AlgState
                 ('obs, 'aAct, 'rep) Protocol"
where
  "alg_mk_auto aOps tOps simInit k_dfs 
     pInit = simInit,
      pTrans = λobs ec. the (lookup tOps (aTrans k_dfs) (ec, obs)),
      pAct = λec. the (lookup aOps (aActs k_dfs) ec)
    "

(*>*)
context AlgorithmForAgent
begin

text‹

The final algorithm, with the constants inlined, is shown in
Figure~\ref{fig:kbps-alg-algorithm}. The rest of this section shows
its correctness.

Firstly it follows immediately from dfs_invariant› that the
invariant holds of the result of the DFS:

›
(*<*)

abbreviation
  "k_dfs  KBPsAlg.alg_dfs aOps tOps (simObs a) (simTrans a) (simAction a) (k_frontier a)"

(* This is a syntactic nightmare. *)

lemma k_dfs_gen_dfs_unfold[simp]:
  "k_dfs = gen_dfs k_succs k_ins k_memb k_empt (k_frontier a)"
  unfolding alg_dfs_def
  apply (fold k_empt_def k_memb_def actsUpdate_def transUpdate_def)
  apply (simp add: k_ins_def[symmetric])
  done

(*>*)
lemma k_dfs_invariant: "k_invariant k_dfs"
(*<*)
  using KBPAlg.dfs_invariant[where S="k_empt" and xs="k_frontier a"]
  by simp

(*>*)
text‹

Secondly we can see that the set of reachable equivalence classes
coincides with the partition of @{term "jkbpC"} under the simulation
and representation functions:

›

lemma k_reachable:
  "simAbs ` KBPAlg.reachable (set (k_frontier a)) = sim_equiv_class a ` jkbpC"
(*<*)(is "?lhs = ?rhs")
proof
  show "?lhs  ?rhs"
  proof
    fix sx assume "sx  ?lhs"
    then obtain x
      where x: "x  KBPAlg.reachable (set (k_frontier a))"
        and sx: "simAbs x = sx"
      by auto
    hence "x  ({ (x, y). y  set (k_succs x) })*
                 `` set (map (simInit a  envObs a) envInit)"
      unfolding KBPAlg.reachable_def k_frontier_def by simp
    then obtain s iobs
      where R: "(simInit a iobs, x)  ({ (x, y). y  set (k_succs x)})*"
        and sI: "s  set envInit"
        and iobs: "envObs a s = iobs"
      by auto
    from R x have "simAbs x  ?rhs"
    proof(induct arbitrary: sx rule: rtrancl_induct)
      case base
      with sI iobs show ?case by (auto simp: jviewInit simInit)
    next
      case (step x y)
      with sI iobs
      have "simAbs x  sim_equiv_class a ` jkbpC"
        unfolding KBPAlg.reachable_def Image_def k_frontier_def
        by auto
      then obtain t
        where tC: "t  jkbpC"
          and F: "simAbs x = sim_equiv_class a t"
        by auto
      from step
      have "simAbs y  simAbs ` set (k_succs x)" by auto
      thus  ?case
        using simTrans[rule_format, where a=a and t=t] tC F by auto
    qed
    with sx show "sx  ?rhs" by simp
  qed
next
  show "?rhs  ?lhs"
  proof
    fix ec assume "ec  ?rhs"
    then obtain t
      where tC: "t  jkbpC"
        and ec: "ec = sim_equiv_class a t"
      by auto
    thus "ec  ?lhs"
    proof(induct t arbitrary: ec)
      case (tInit s) thus ?case
        unfolding KBPAlg.reachable_def (* FIXME ouch this is touchy *)
        unfolding k_frontier_def
        apply simp
        apply (rule image_eqI[where x="simInit a (envObs a s)"])
         apply (simp add: simInit jviewInit)
        apply (rule ImageI[where a="simInit a (envObs a s)"])
        apply auto
        done
    next
      case (tStep t s)
      hence tsC: "t  s  jkbpC"
        and ec: "ec = sim_equiv_class a (t  s)"
        and "sim_equiv_class a t
            simAbs ` DFS.reachable k_succs (set (k_frontier a))"
        by auto
      then obtain rect
        where rect: "rect  DFS.reachable k_succs (set (k_frontier a))"
          and srect: "simAbs rect = sim_equiv_class a t"
        by auto
      from tsC ec srect
      have "ec  simAbs ` set (simTrans a rect)"
        using simTrans[rule_format, where a=a and t="t" and ec="rect"] srect by auto
      then obtain rec
        where rec: "ec = simAbs rec"
          and F: "rec  set (simTrans a rect)"
        by auto
      from rect obtain rec0
        where rec0: "rec0  set (k_frontier a)"
          and rec0rect: "(rec0, rect)  ({ (x, y). y  set (k_succs x)})*"
        unfolding KBPAlg.reachable_def by auto
      show ?case
        apply -
        apply (rule image_eqI[where x="rec"])
         apply (rule rec)
        unfolding KBPAlg.reachable_def
        apply (rule ImageI[where a="rec0"])
         apply (rule rtrancl_into_rtrancl[where b="rect"])
          apply (rule rec0rect)
         apply clarsimp
         apply (rule F)
         apply (rule rec0)
         done
     qed
   qed
qed
(*>*)
text‹

Left to right follows from an induction on the reflexive, transitive
closure, and right to left by induction over canonical traces.

This result immediately yields the same result at the level of
representations:

›

lemma k_memb_rep:
  assumes N: "k_isNode rec"
  shows "k_memb rec k_dfs"
(*<*)
proof -
  from N obtain rec'
    where r: "rec'  DFS.reachable k_succs (set (k_frontier a))"
      and rec': "simAbs rec = simAbs rec'"
    unfolding k_isNode_def by (auto iff: k_reachable[symmetric])

  from N k_isNode_cong[OF rec', symmetric]
  have N': "k_isNode rec'"
    unfolding k_isNode_def by auto

  show "k_memb rec k_dfs"
    using KBPAlg.reachable_imp_dfs[OF N' k_frontier_is_node r]
    apply clarsimp
    apply (subst k_memb_def)
    apply (subst (asm) k_memb_def)
    using k_invariantAOD[OF N' N rec' k_dfs_invariant, symmetric]
    apply (cut_tac ec=y' and ec'=rec' in k_invariantAOD[OF _ _ _ k_dfs_invariant, symmetric])
     apply simp_all

     apply (cut_tac ec=rec' and ec'=y' in k_isNode_cong)
     apply simp
     using N'
     apply simp
     apply (rule N')
     done
qed
(*>*)

end (* context AlgorithmForAgent *)

text‹

This concludes our agent-specific reasoning; we now show that the
algorithm works for all agents. The following command generalises all
our lemmas in the @{term "AlgorithmForAgent"} to the @{term
"Algorithm"} locale, giving them the mandatory prefix KBP›:

›

sublocale Algorithm
        < KBP: AlgorithmForAgent
            jkbp envInit envAction envTrans envVal jview envObs
            jviewInit jviewIncr simf simRels simVal simAbs simObs
            simInit simTrans simAction aOps tOps a for a
(*<*)
  by unfold_locales
(*>*)

context Algorithm
begin

abbreviation
  "k_mkAlgAuto 
    mkAlgAuto aOps tOps simObs simInit simTrans simAction k_frontier"
(*<*)

lemma k_mkAlgAuto_mkAutoSim_equiv:
  assumes tC: "t  jkbpC"
  shows "simAbs (runJP k_mkAlgAuto t a) = simAbs (runJP mkAutoSim t a)"
using tC
proof(induct t)
  case (tInit s) thus ?case by simp
next
  case (tStep t s)
  hence tC: "t  jkbpC" by blast

  from tStep
  have N: "KBP.k_isNode a (runJP k_mkAlgAuto t a)"
    unfolding KBP.k_isNode_def
    by (simp only: mkAutoSim_ec) auto

  from tStep
  have ect: "simAbs (runJP k_mkAlgAuto t a) = sim_equiv_class a t"
    by (simp only: mkAutoSim_ec) auto

  from tStep
  have "sim_equiv_class a (t  s)  simAbs ` set (simTrans a (runJP k_mkAlgAuto t a))"
    using simTrans[rule_format, where a=a and t=t] tC ect by auto
  then obtain ec
    where ec: "ec  set (simTrans a (runJP k_mkAlgAuto t a))"
      and sec: "simAbs ec = sim_equiv_class a (t  s)"
    by auto

  from tStep
  have F: "envObs a s  simObs a ` set (simTrans a (runJP k_mkAlgAuto t a))"
    using simObs[rule_format, where a=a and t="ts", symmetric] sec ec by auto
  from KBP.k_memb_rep[OF N]
  have E: "KBP.k_memb (runJP k_mkAlgAuto t a) (KBP.k_dfs a)" by blast

  have G: "simAbs (runJP k_mkAlgAuto (t  s) a) = sim_equiv_class a (t  s)"
    using KBP.k_invariantTD[OF N E F KBP.k_dfs_invariant]
    apply (clarsimp simp: jviewIncr)
    using simTrans[rule_format, where a=a and t=t and ec="runJP k_mkAlgAuto t a"] tC ect
    apply (subgoal_tac "simAbs x  simAbs ` set (simTrans a (runJP k_mkAlgAuto t a))")
     apply (clarsimp simp: jviewIncr)
     apply (cut_tac a=a and ec=ec' and t="t'sa" in simObs[rule_format])
      apply (simp add: jviewIncr)
     apply simp
    apply blast
    done

  from tStep show ?case by (simp only: G mkAutoSim_ec)
qed

(*>*)
text‹

Running the automata produced by the DFS on a canonical trace @{term
"t"} yields some representation of the expected equivalence class:

›

lemma k_mkAlgAuto_ec:
  assumes tC: "t  jkbpC"
  shows "simAbs (runJP k_mkAlgAuto t a) = sim_equiv_class a t"
(*<*)
  using k_mkAlgAuto_mkAutoSim_equiv[OF tC] mkAutoSim_ec[OF tC]
  by simp

(*>*)
text‹

This involves an induction over the canonical trace @{term "t"}.

That the DFS and @{term "mkAutoSim"} yield the same actions on
canonical traces follows immediately from this result and the
invariant:

›

lemma k_mkAlgAuto_mkAutoSim_act_eq:
  assumes tC: "t  jkbpC"
  shows "set  actJP k_mkAlgAuto t = set  actJP mkAutoSim t"
(*<*)
proof
  fix a
  let ?ec = "sim_equiv_class a t"
  let ?rec = "runJP k_mkAlgAuto t a"

  from tC have E: "?ec  sim_equiv_class a ` jkbpC"
    by auto

  from tC E have N: "KBP.k_isNode a (runJP k_mkAlgAuto t a)"
    unfolding KBP.k_isNode_def by (simp add: k_mkAlgAuto_ec[OF tC])

  from KBP.k_memb_rep[OF N]
  have E: "KBP.k_memb ?rec (KBP.k_dfs a)" by blast

  obtain acts
    where "lookup aOps (aActs (KBP.k_dfs a)) ?rec = Some acts"
      and "set acts = set (simAction a ?rec)"
    using KBP.k_invariantAD[OF N E KBP.k_dfs_invariant] by blast

  thus "(set  actJP k_mkAlgAuto t) a = (set  actJP mkAutoSim t) a"
    by (auto intro!: jAction_simAbs_cong[OF tC]
               simp: k_mkAlgAuto_ec[OF tC] mkAutoSim_ec[OF tC])
qed
(*>*)

text‹

Therefore these two constructions are behaviourally equivalent, and so
the DFS generates an implementation of @{term "jkbp"} in the given
environment:

›

theorem k_mkAlgAuto_implements: "implements k_mkAlgAuto"
(*<*)
proof -
  have "behaviourally_equiv mkAutoSim k_mkAlgAuto"
    by rule (simp only: k_mkAlgAuto_mkAutoSim_act_eq)
  with mkAutoSim_implements show ?thesis
    by (simp add: behaviourally_equiv_implements)
qed
(*>*)

end (* context Algorithm *)

text‹

Clearly the automata generated by this algorithm are large. We discuss
this issue in \S\ref{sec:kbps-alg-auto-min}.

\FloatBarrier

›

(*<*)
end
(*>*)

Theory ODList

(*<*)
(*
 * Knowledge-based programs.
 * (C)opyright 2011, Peter Gammie, peteg42 at gmail.com.
 * License: BSD
 *
 * Based on Florian Haftmann's DList.thy and Tobias Nipkow's msort proofs.
 *)

theory ODList
imports
  "HOL-Library.Multiset"
  List_local
begin
(*>*)

text‹

Define a type of ordered distinct lists, intended to represent sets.

The advantage of this representation is that it is isomorphic to the
set of finite sets. Conversely it requires the carrier type to be a
linear order.  Note that this representation does not arise from a
quotient on lists: all the unsorted lists are junk.

›

context linorder
begin

text‹

"Absorbing" msort, a variant of Tobias Nipkow's proofs from 1992.

›

fun
  merge :: "'a list  'a list  'a list"
where
  "merge [] ys = ys"
| "merge xs [] = xs"
| "merge (x#xs) (y#ys) =
    (if x = y then merge xs (y#ys)
             else if x < y then x # merge xs (y#ys)
                           else y # merge (x#xs) ys)"

(*<*)
lemma set_merge[simp]:
  "set (merge xs ys) = set (xs @ ys)"
  by (induct xs ys rule: merge.induct) auto

lemma distinct_sorted_merge[simp]:
  " distinct xs; distinct ys; sorted xs; sorted ys 
      distinct (merge xs ys)  sorted (merge xs ys)"
  by (induct xs ys rule: merge.induct) (auto)

lemma mset_merge [simp]:
  " distinct (xs @ ys)   mset (merge xs ys) = mset xs + mset ys"
  by (induct xs ys rule: merge.induct) (simp_all add: ac_simps)
(*>*)

text‹The "absorbing" sort itself.›

fun msort :: "'a list  'a list"
where
  "msort [] = []"
| "msort [x] = [x]"
| "msort xs = merge (msort (take (size xs div 2) xs))
                    (msort (drop (size xs div 2) xs))"

(*<*)
lemma msort_distinct_sorted[simp]:
  "distinct (msort xs)  sorted (msort xs)"
  by (induct xs rule: msort.induct) simp_all

lemma msort_set[simp]:
  "set (msort xs) = set xs"
  by (induct xs rule: msort.induct)
     (simp_all, metis List.set_simps(2) append_take_drop_id set_append) (* thankyou sledgehammer! *)

lemma msort_remdups[simp]:
  "remdups (msort xs) = msort xs"
  by simp

lemma msort_idle[simp]:
  " distinct xs; sorted xs   msort xs = xs"
  by (rule map_sorted_distinct_set_unique[where f=id]) (auto simp: map.id)

lemma mset_msort[simp]:
  "distinct xs  mset (msort xs) = mset xs"
  by (rule iffD1[OF set_eq_iff_mset_eq_distinct]) simp_all

lemma msort_sort[simp]:
  "distinct xs  sort xs = msort xs"
  by (simp add: properties_for_sort)
(*>*)

end (* context linorder *)


section ‹The @{term "odlist"} type›

typedef (overloaded) ('a :: linorder) odlist = "{ x::'a list . sorted x  distinct x }"
  morphisms toList odlist_Abs by (auto iff: sorted.simps(1))

lemma distinct_toList[simp]: "distinct (toList xs)"
  using toList by auto

lemma sorted_toList[simp]: "sorted (toList xs)"
  using toList by auto

text‹

Code generator voodoo: this is the constructor for the abstract type.

›

definition
  ODList :: "('a :: linorder) list  'a odlist"
where
  "ODList  odlist_Abs  msort"

lemma toList_ODList:
  "toList (ODList xs) = msort xs"
  unfolding ODList_def
  by (simp add: odlist_Abs_inverse)

lemma ODList_toList[simp, code abstype]:
  "ODList (toList xs) = xs"
  unfolding ODList_def
  by (cases xs) (simp add: odlist_Abs_inverse)

text‹

Runtime cast from @{typ "'a list"} into @{typ "'a odlist"}. This is
just a renaming of @{term "ODList"} -- names are significant to the
code generator's abstract type machinery.

›

definition
  fromList :: "('a :: linorder) list  'a odlist"
where
  "fromList  ODList"

lemma toList_fromList[code abstract]:
  "toList (fromList xs) = msort xs"
  unfolding fromList_def
  by (simp add: toList_ODList)

subsection‹Basic properties: equality, finiteness›

(*<*)
declare toList_inject[iff]
(*>*)

instantiation odlist :: (linorder) equal
(*<*)
begin

definition [code]:
  "HOL.equal A B  odlist_equal (toList A) (toList B)"

instance
  by standard (simp add: equal_odlist_def)

end
(*>*)

instance odlist :: ("{finite, linorder}") finite
(*<*)
proof
  let ?ol = "UNIV :: 'a odlist set"
  let ?s = "UNIV :: 'a set set"
  have "finite ?s" by simp
  moreover
  have "?ol  range (odlist_Abs  sorted_list_of_set)"
  proof
    fix x show "x  range (odlist_Abs  sorted_list_of_set)"
      apply (cases x)
      apply (rule range_eqI[where x="set (toList x)"])
      apply (clarsimp simp: odlist_Abs_inject sorted_list_of_set_sort_remdups odlist_Abs_inverse distinct_remdups_id)
      done
  qed
  ultimately show "finite ?ol" by (blast intro: finite_surj)
qed
(*>*)

subsection‹Constants›

definition
  empty :: "('a :: linorder) odlist"
where
  "empty  ODList []"

lemma toList_empty[simp, code abstract]:
  "toList empty = []"
  unfolding empty_def by (simp add: toList_ODList)

subsection‹Operations›

subsubsection‹toSet›

definition
  toSet :: "('a :: linorder) odlist  'a set"
where
  "toSet X = set (toList X)"

lemma toSet_empty[simp]:
  "toSet empty = {}"
  unfolding toSet_def empty_def by (simp add: toList_ODList)

lemma toSet_ODList[simp]:
  " distinct xs; sorted xs   toSet (ODList xs) = set xs"
  unfolding toSet_def by (simp add: toList_ODList)

lemma toSet_fromList_set[simp]:
  "toSet (fromList xs) = set xs"
  unfolding toSet_def fromList_def
  by (simp add: toList_ODList)

lemma toSet_inj[intro, simp]: "inj toSet"
  apply (rule injI)
  unfolding toSet_def
  apply (case_tac x)
  apply (case_tac y)
  apply (auto iff: odlist_Abs_inject odlist_Abs_inverse sorted_distinct_set_unique)
  done

lemma toSet_eq_iff:
  "X = Y  toSet X = toSet Y"
  by (blast dest: injD[OF toSet_inj])

subsubsection‹head›

definition
  hd :: "('a :: linorder) odlist  'a"
where
  [code]: "hd  List.hd  toList"

lemma hd_toList: "toList xs = y # ys  ODList.hd xs = y"
  unfolding hd_def by simp

subsubsection‹member›

definition
  member :: "('a :: linorder) odlist  'a  bool"
where
  [code]: "member xs x  List.member (toList xs) x"

lemma member_toSet[iff]:
  "member xs x x  toSet xs"
  unfolding member_def toSet_def by (simp add: in_set_member)

subsubsection‹Filter›

definition
  filter :: "(('a :: linorder)  bool)  'a odlist  'a odlist"
where
  "filter P xs  ODList (List.filter P (toList xs))"

lemma toList_filter[simp, code abstract]:
  "toList (filter P xs) = List.filter P (toList xs)"
  unfolding filter_def by (simp add: toList_ODList)

lemma toSet_filter[simp]:
  "toSet (filter P xs) = { x  toSet xs . P x }"
  unfolding filter_def
  apply simp
  apply (simp add: toSet_def)
  done

subsubsection‹All›

definition
  odlist_all :: "('a :: linorder  bool)  'a odlist  bool"
where
  [code]: "odlist_all P xs  list_all P (toList xs)"

lemma odlist_all_iff:
  "odlist_all P xs  (x  toSet xs. P x)"
  unfolding odlist_all_def toSet_def by (simp only: list_all_iff)

lemma odlist_all_cong [fundef_cong]:
  "xs = ys  (x. x  toSet ys  f x = g x)  odlist_all f xs = odlist_all g ys"
  by (simp add: odlist_all_iff)

subsubsection‹Difference›

definition
  difference :: "('a :: linorder) odlist  'a odlist  'a odlist"
where
  "difference xs ys = ODList (List_local.difference (toList xs) (toList ys))"

lemma toList_difference[simp, code abstract]:
  "toList (difference xs ys) = List_local.difference (toList xs) (toList ys)"
  unfolding difference_def by (simp add: toList_ODList)

lemma toSet_difference[simp]:
  "toSet (difference xs ys) = toSet xs - toSet ys"
  unfolding difference_def
  apply simp
  apply (simp add: toSet_def)
  done

subsubsection‹Intersection›

definition
  intersect :: "('a :: linorder) odlist  'a odlist  'a odlist"
where
  "intersect xs ys = ODList (List_local.intersection (toList xs) (toList ys))"

lemma toList_intersect[simp, code abstract]:
  "toList (intersect xs ys) = List_local.intersection (toList xs) (toList ys)"
  unfolding intersect_def by (simp add: toList_ODList)

lemma toSet_intersect[simp]:
  "toSet (intersect xs ys) = toSet xs  toSet ys"
  unfolding intersect_def
  apply simp
  apply (simp add: toSet_def)
  done

subsubsection‹Union›

definition
  union :: "('a :: linorder) odlist  'a odlist  'a odlist"
where
  "union xs ys = ODList (merge (toList xs) (toList ys))"

lemma toList_union[simp, code abstract]:
  "toList (union xs ys) = merge (toList xs) (toList ys)"
  unfolding union_def by (simp add: toList_ODList)

lemma toSet_union[simp]:
  "toSet (union xs ys) = toSet xs  toSet ys"
  unfolding union_def
  apply simp
  apply (simp add: toSet_def)
  done

definition
  big_union :: "('b  ('a :: linorder) odlist)  'b list  'a odlist"
where
  [code]: "big_union f X  foldr (λa A. ODList.union (f a) A) X ODList.empty"

lemma toSet_big_union[simp]:
  "toSet (big_union f X) = (x  set X. toSet (f x))"
proof -
  { fix X Y
    have "toSet (foldr (λx A. ODList.union (f x) A) X Y) = toSet Y  (x  set X. toSet (f x))"
      by (induct X arbitrary: Y) auto }
   thus ?thesis
     unfolding big_union_def by simp
qed

subsubsection‹Case distinctions›

text‹

We construct ODLists out of lists, so talk in terms of those, not a
one-step constructor we don't use.

›

lemma distinct_sorted_induct [consumes 2, case_names Nil insert]:
  assumes "distinct xs"
  assumes "sorted xs"
  assumes base: "P []"
  assumes step: "x xs.  distinct (x # xs); sorted (x # xs); P xs   P (x # xs)"
  shows "P xs"
using ‹distinct xs ‹sorted xs proof (induct xs)
  case Nil from P [] show ?case .
next
  case (Cons x xs)
  then have "distinct (x # xs)" and "sorted (x # xs)" and "P xs" by (simp_all)
  with step show "P (x # xs)" .
qed

lemma odlist_induct [case_names empty insert, cases type: odlist]:
  assumes empty: "dxs. dxs = empty  P dxs"
  assumes insrt: "dxs x xs.  dxs = fromList (x # xs); distinct (x # xs); sorted (x # xs); P (fromList xs) 
                             P dxs"
  shows "P dxs"
proof (cases dxs)
  case (odlist_Abs xs)
  then have dxs: "dxs = ODList xs" and distinct: "distinct xs" and sorted: "sorted xs"
    by (simp_all add: ODList_def)
  from ‹distinct xs and ‹sorted xs have "P (ODList xs)"
  proof (induct xs rule: distinct_sorted_induct)
    case Nil from empty show ?case by (simp add: empty_def)
  next
    case (insert x xs) thus ?case
      apply -
      apply (rule insrt)
      apply (auto simp: fromList_def)
      done
  qed
  with dxs show "P dxs" by simp
qed

lemma odlist_cases [case_names empty insert, cases type: odlist]:
  assumes empty: "dxs = empty  P"
  assumes insert: "x xs.  dxs = fromList (x # xs); distinct (x # xs); sorted (x # xs) 
                             P"
  shows P
proof (cases dxs)
  case (odlist_Abs xs)
  then have dxs: "dxs = ODList xs" and distinct: "distinct xs" and sorted: "sorted xs"
    by (simp_all add: ODList_def)
  show P proof (cases xs)
    case Nil with dxs have "dxs = empty" by (simp add: empty_def)
    with empty show P .
  next
    case (Cons y ys)
    with dxs distinct sorted insert
    show P by (simp add: fromList_def)
  qed
qed

subsubsection‹Relations›

text‹

Relations, represented as a list of pairs.

›

type_synonym 'a odrelation = "('a × 'a) odlist"

subsubsection‹Image›

text‹

The output of @{term "List_local.image"} is not guaranteed to be
ordered or distinct. Also the relation need not be monomorphic.

›

definition
  image :: "('a :: linorder × 'b :: linorder) odlist  'a odlist  'b odlist"
where
  "image R xs = ODList (List_local.image (toList R) (toList xs))"

lemma toList_image[simp, code abstract]:
  "toList (image R xs) = msort (List_local.image (toList R) (toList xs))"
  unfolding image_def by (simp add: toList_ODList)

lemma toSet_image[simp]:
  "toSet (image R xs) = toSet R `` toSet xs"
  unfolding image_def by (simp add: toSet_def toList_ODList)

subsubsection‹Linear order›

text‹

Lexicographic ordering on lists. Executable, unlike in List.thy.

›

instantiation odlist :: (linorder) linorder
begin
print_context
fun