# Theory Extra

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

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"

(*

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 (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
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
apply (rule_tac x="f xa" in exI)
apply simp
apply simp
using d
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.
*)

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")
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 (subst FIXME_fiddle1[where Y=X])
apply blast
apply auto
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)
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
apply clarsimp

apply (case_tac "xa ∈ set list")
apply clarsimp
apply rule
apply (auto dest: transD)
apply (auto dest: symD transD)

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)
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))"
next
show "wf ?wfr" by (blast intro: wf_finite_psubset Int_lower2 [THEN  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)
unfolding partition_aux_body_def
apply clarsimp
apply (case_tac a)
apply simp
apply (case_tac "partition_split r aa list")

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.
*)

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"

lemma S5nD[dest]: "S5n M ⟹ equiv (worlds M) (relations M a)"

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 ⊨ (❙K⇩a φ) = (∀w' ∈ relations M a  {w}. M, w' ⊨ φ)"
| "M, w ⊨ (❙C⇘as⇙ φ) = (∀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 ((⋃i∈is. f i)⇧+)"
proof(rule equivI)
from E is_nempty show "refl_on A ((⋃i∈is. 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 ((⋃i∈is. f i)⇧+)"
apply -
apply (rule sym_trancl)
unfolding equiv_def sym_def by blast
show "trans  ((⋃i∈is. 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 ⊨ ❙K⇩a (Kand φ ψ)"
assumes p: "M, w ⊨ φ"
shows "M, w ⊨ ❙C⇘as⇙ ψ"
(*<*)
proof -
{ fix w' assume ww': "(w, w') ∈ (⋃x∈set 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
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
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) ∈ (⋃a∈as. relations M a)⇧+"
shows "(f u, f v) ∈ (⋃a∈as. 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') ∈ (⋃a∈as. relations M' a)⇧+"
obtains v where "f v = v'" and "(u, v) ∈ (⋃a∈as. relations M a)⇧+"
(*<*)
proof -
assume E: "⋀v. ⟦f v = v'; (u, v) ∈ (⋃a∈as. relations M a)⇧+⟧ ⟹ thesis"

from fuv' have as_nempty: "as ≠ {}" by auto
from fuv' have "∃v. f v = v' ∧ (u, v) ∈ (⋃a∈as. 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') ∈ (⋃a∈as. relations M' a)⇧+"
and v'w': "(v', w') ∈ (⋃a∈as. relations M' a)" by fast+
from step
obtain v where vv': "f v = v'"
and uv: "(u, v) ∈ (⋃a∈as. 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) ∈ (⋃a∈as. 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') ∈ (⋃x∈set as. relations M' x)⇧+"
with M s u
obtain v where uv:  "(u, v) ∈ (⋃x∈set 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) ∈ (⋃x∈set as. relations M x)⇧+"
with s have "(f u, f v) ∈ (⋃x∈set 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.
*)

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.
*)

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 "❙K⇩a φ"} 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') ∈ (⋃a∈set 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
"jkbpT⇘0⇙ T     = { tInit s |s. s ∈ set envInit }"
| "jkbpT⇘Suc n⇙ T = { t ↝ envTrans eact aact (tLast t) |t eact aact.
t ∈ jkbpT⇘n⇙ 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. jkbpT⇘n⇙ 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') ∈ (⋃a∈as. 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)
using tT traces
apply (auto)

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

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

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 ‹jkbpC⇩n› of
\emph{(canonical) temporal slices} similarly to @{term "jkbpT⇘n⇙"}:

›

fun jkbpCn :: "nat ⇒ 's Trace set"(*<*)("jkbpC⇘_⇙")(*>*) where
"jkbpC⇘0⇙      = { tInit s |s. s ∈ set envInit }"
| "jkbpC⇘Suc n⇙ = { t ↝ envTrans eact aact (tLast t) |t eact aact.
t ∈ jkbpC⇘n⇙ ∧ eact ∈ set (envAction (tLast t))
∧ (∀a. aact a ∈ set (jAction (mkM jkbpC⇘n⇙) t a)) }"

abbreviation MCn :: "nat ⇒ ('a, 'p, 's Trace) KripkeStructure"(*<*)("MC⇘_⇙")(*>*) where
"MC⇘n⇙ ≡ mkM jkbpC⇘n⇙"
(*<*)

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. jkbpC⇘n⇙"

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 (MC⇘n⇙) 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 ∈ jkbpC⇘n⇙"
shows "jAction MC t = jAction MC⇘n⇙ t"
(*<*)
using assms
by - (rule sync_jview_jAction_eq, auto iff: jkbpC_traces_of_length)

(*>*)
text‹›

lemma jkbpTn_jkbpCn_represents: "jkbpT⇘n⇙ jkbpC = jkbpC⇘n⇙"
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"

(* 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.
*)

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)"
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"

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"

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
apply (drule acts'[OF indhyp, symmetric])
apply auto
done
finally show ?case
apply (auto iff: jkbpC_traces_of_length)
done
qed
hence "∀t∈jkbpCn n. actJP jp t = jAction (MCn n) t"
apply clarsimp
apply (rule acts')
apply (auto iff: jkbpC_traces_of_length)
done
hence "∀t∈jkbpCn 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)
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
"jkbpCS⇘n⇙ ≡ simf  jkbpC⇘n⇙"

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

abbreviation MCSn :: "nat ⇒ ('a, 'p, 'ss) KripkeStructure"(*<*)("MCS⇘_⇙")(*>*) where
"MCS⇘n⇙ ≡ mkKripke jkbpCS⇘n⇙ 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"
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"
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.

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="t↝s" 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]
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))"
(*>*)

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 ≡ ⋃x∈xs. 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
apply auto
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
apply simp
apply (rule disjI1)
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
apply auto
apply (subgoal_tac "nodeAbs  set (succs xd) ⊆ nodeAbs  (⋃x∈{x. isNode x ∧ memb x S}. set (succs x))")
defer
apply auto
apply (subgoal_tac "nodeAbs xc ∈ nodeAbs  set (succs xd)")
defer
apply auto
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 (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
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))"
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
apply auto
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
apply auto
apply (rule_tac x=xb in image_eqI)
apply auto
apply auto
apply (auto iff: ins_eq)
done
(* by (auto simp add: reachable_def ins_eq set_of_def cong: conj_cong) *)
qed

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 (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
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.
*)

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

"⟦ 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

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 (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
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)

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
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)
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 (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="t↝s", 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
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
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.
*
* 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"
(*>*)

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

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

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

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

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])

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
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"

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
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
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
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"
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"
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`