# Theory MC

section "Kripke structures and CTL"

text ‹We apply Kripke structures and CTL to model state based systems and analyse properties under
dynamic state changes. Snapshots of systems are the states on which we define a state transition.
Temporal logic is then employed to express security and privacy properties.›
theory MC
imports Main
begin

subsection "Lemmas to support least and greatest fixpoints"

lemma predtrans_empty:
assumes "mono (τ :: 'a set  'a set)"
shows " i. (τ ^^ i) ({})  (τ ^^(i + 1))({})"
using assms funpow_decreasing le_add1 by blast

lemma ex_card: "finite S   n:: nat. card S = n"
by simp

lemma less_not_le: "(x:: nat) < y; y  x  False"
by arith

lemma infchain_outruns_all:
assumes "finite (UNIV :: 'a set)"
and "i :: nat. ((τ :: 'a set  'a set)^^ i) ({}:: 'a set)  (τ ^^ (i + 1)) {}"
shows "j :: nat. i :: nat. j < card ((τ ^^ i) {})"
proof (rule allI, induct_tac j)
show "i. 0 < card ((τ ^^ i) {})" using assms
by (metis bot.not_eq_extremum card_gt_0_iff finite_subset subset_UNIV)
next show "j n. i. n < card ((τ ^^ i) {})
i. Suc n < card ((τ ^^ i) {})"
proof -
fix j n
assume a: "i. n < card ((τ ^^ i) {})"
obtain i where "n < card ((τ ^^ i) {})"
using a by blast
thus " i. Suc n < card ((τ ^^ i) {})" using assms
by (meson finite_subset le_less_trans le_simps(3) psubset_card_mono subset_UNIV)
qed
qed

lemma no_infinite_subset_chain:
assumes "finite (UNIV :: 'a set)"
and    "mono (τ :: ('a set  'a set))"
and    "i :: nat. ((τ :: 'a set  'a set) ^^ i) {}  (τ ^^ (i + (1 :: nat))) ({} :: 'a set)"
shows   "False"
text ‹Proof idea: since @{term "UNIV"} is finite, we have from @{text ‹ex_card›} that there is
an n with @{term "card UNIV = n"}. Now, use @{text ‹infchain_outruns_all›} to show as
@{term " i :: nat. card UNIV < card ((τ ^^ i) {})"}.
Since all sets are subsets of @{term "UNIV"}, we also have
@{term "card ((τ ^^ i) {})  card UNIV"}:
Contradiction!, i.e. proof of False  ›
proof -
have a: " (j :: nat). ( (i :: nat). (j :: nat) < card((τ ^^ i)({} :: 'a set)))" using assms
by (erule_tac τ = τ in infchain_outruns_all)
hence b: " (n :: nat). card(UNIV :: 'a set) = n" using assms
by (erule_tac S = UNIV in ex_card)
from this obtain n where c: "card(UNIV :: 'a set) = n" by (erule exE)
hence   d: "i. card UNIV < card ((τ ^^ i) {})" using a
by (drule_tac x = "card UNIV" in spec)
from this obtain i where e: "card (UNIV :: 'a set) < card ((τ ^^ i) {})"
by (erule exE)
hence f: "(card((τ ^^ i){}))  (card (UNIV :: 'a set))" using assms
apply (erule_tac A = "((τ ^^ i){})" in Finite_Set.card_mono)
by (rule subset_UNIV)
thus "False" using e
by (erule_tac y = "card((τ ^^ i){})" in less_not_le)
qed

lemma finite_fixp:
assumes "finite(UNIV :: 'a set)"
and "mono (τ :: ('a set  'a set))"
shows " i. (τ ^^ i) ({}) = (τ ^^(i + 1))({})"
text ‹Proof idea:
with @{text predtrans_empty} we know

@{term " i. (τ ^^ i){}  (τ ^^(i + 1))({})"} (1).

@{term " i.  (τ ^^ i)({})  (τ ^^(i + 1))({})"} (2),

we can get the goal together with equalityI
@{text "⊆ + ⊇ ⟶ ="}.
To prove (1) we observe that
@{term "(τ ^^ i)({})  (τ ^^(i + 1))({})"}
can be inferred from
@{term "¬((τ ^^ i)({})  (τ ^^(i + 1))({}))"}
and (1).
Finally, the latter is solved directly by @{text ‹no_infinite_subset_chain›}.›
proof -
have a: "i. (τ ^^ i) ({}:: 'a set)  (τ ^^ (i + (1))) {}"
by(rule predtrans_empty, rule assms(2))
have a3: "¬ ( i :: nat. (τ ^^ i) {}  (τ ^^(i + 1)) {})"
by (rule notI, rule no_infinite_subset_chain, (rule assms)+)
hence b: "( i :: nat. ¬((τ ^^ i) {}  (τ ^^(i + 1)) {}))" using assms a3
by blast
thus " i. (τ ^^ i) ({}) = (τ ^^(i + 1))({})" using a
by blast
qed

lemma predtrans_UNIV:
assumes "mono (τ :: ('a set  'a set))"
shows " i. (τ ^^ i) (UNIV)  (τ ^^(i + 1))(UNIV)"
proof (rule allI, induct_tac i)
show "(τ ^^ ((0) + (1))) UNIV  (τ ^^ (0)) UNIV"
by simp
next show "(i) n.
(τ ^^ (n + (1))) UNIV  (τ ^^ n) UNIV  (τ ^^ (Suc n + (1))) UNIV  (τ ^^ Suc n) UNIV"
proof -
fix i n
assume a: "(τ ^^ (n + (1))) UNIV  (τ ^^ n) UNIV"
have "(τ ((τ ^^ n) UNIV))  (τ ((τ ^^ (n + (1 :: nat))) UNIV))" using assms a
by (rule monoE)
thus "(τ ^^ (Suc n + (1))) UNIV  (τ ^^ Suc n) UNIV" by simp
qed
qed

lemma Suc_less_le: "x < (y - n)  x  (y - (Suc n))"
by simp

lemma card_univ_subtract:
assumes "finite (UNIV :: 'a set)" and  "mono τ"
and  "(i :: nat. ((τ :: 'a set  'a set) ^^ (i + (1 :: nat)))(UNIV :: 'a set)  (τ ^^ i) UNIV)"
shows "( i :: nat. card((τ ^^ i) (UNIV ::'a set))  (card (UNIV :: 'a set)) - i)"
proof (rule allI, induct_tac i)
show "card ((τ ^^ (0)) UNIV)  card (UNIV :: 'a set) - (0)" using assms
by (simp)
next show "(i) n.
card ((τ ^^ n) (UNIV :: 'a set))  card (UNIV :: 'a set) - n
card ((τ ^^ Suc n) (UNIV :: 'a set))  card (UNIV :: 'a set) - Suc n" using assms
proof -
fix i n
assume a: "card ((τ ^^ n) (UNIV :: 'a set))  card (UNIV :: 'a set) - n"
have b: "(τ ^^ (n + (1)))(UNIV :: 'a set)  (τ ^^ n) UNIV" using assms
by (erule_tac x = n in spec)
have "card((τ ^^ (n + (1 :: nat)))(UNIV :: 'a set)) < card((τ ^^ n) (UNIV :: 'a set))"
by (rule psubset_card_mono, rule finite_subset, rule subset_UNIV, rule assms(1), rule b)
thus "card ((τ ^^ Suc n) (UNIV :: 'a set))  card (UNIV :: 'a set) - Suc n" using a
by simp
qed
qed

lemma card_UNIV_tau_i_below_zero:
assumes "finite (UNIV :: 'a set)" and "mono τ"
and  "(i :: nat. ((τ :: ('a set  'a set)) ^^ (i + (1 :: nat)))(UNIV :: 'a set)  (τ ^^ i) UNIV)"
shows "card((τ ^^ (card (UNIV ::'a set))) (UNIV ::'a set))  0"
proof -
have "( i :: nat. card((τ ^^ i) (UNIV ::'a set))  (card (UNIV :: 'a set)) - i)" using assms
by (rule card_univ_subtract)
thus "card((τ ^^ (card (UNIV ::'a set))) (UNIV ::'a set))  0"
by (drule_tac x = "card (UNIV ::'a set)" in spec, simp)
qed

lemma finite_card_zero_empty: " finite S; card S  0  S = {}"
by simp

lemma UNIV_tau_i_is_empty:
assumes "finite (UNIV :: 'a set)" and "mono (τ :: ('a set  'a set))"
and   "(i :: nat. ((τ :: 'a set  'a set) ^^ (i + (1 :: nat)))(UNIV :: 'a set)  (τ ^^ i) UNIV)"
shows "(τ ^^ (card (UNIV ::'a set))) (UNIV ::'a set) = {}"
by (meson assms card_UNIV_tau_i_below_zero finite_card_zero_empty finite_subset subset_UNIV)

lemma down_chain_reaches_empty:
assumes "finite (UNIV :: 'a set)" and "mono (τ :: 'a set  'a set)"
and "(i :: nat. ((τ :: 'a set  'a set) ^^ (i + (1 :: nat))) UNIV  (τ ^^ i) UNIV)"
shows " (j :: nat). (τ ^^ j) UNIV = {}"
using UNIV_tau_i_is_empty assms by blast

lemma no_infinite_subset_chain2:
assumes "finite (UNIV :: 'a set)" and "mono (τ :: ('a set  'a set))"
and "i :: nat. (τ ^^ i) UNIV  (τ ^^ (i + (1 :: nat))) UNIV"
shows "False"
proof -
have " j :: nat. (τ ^^ j) UNIV = {}" using assms
by (rule down_chain_reaches_empty)
from this obtain j where a: "(τ ^^ j) UNIV = {}" by (erule exE)
have "(τ ^^ (j + (1))) UNIV  (τ ^^ j) UNIV" using assms
by (erule_tac x = j in spec)
thus False using a by simp
qed

lemma finite_fixp2:
assumes "finite(UNIV :: 'a set)" and "mono (τ :: ('a set  'a set))"
shows " i. (τ ^^ i) UNIV = (τ ^^(i + 1)) UNIV"
proof -
have "i. (τ ^^ (i + (1))) UNIV  (τ ^^ i) UNIV"
by (rule predtrans_UNIV , simp add: assms(2))
moreover have "i. ¬ (τ ^^ (i + (1))) UNIV  (τ ^^ i) UNIV" using assms
proof -
have "¬ ( i :: nat. (τ ^^ i) UNIV  (τ ^^(i + 1)) UNIV)"
using assms(1) assms(2) no_infinite_subset_chain2 by blast
thus "i. ¬ (τ ^^ (i + (1))) UNIV  (τ ^^ i) UNIV" by blast
qed
ultimately show " i. (τ ^^ i) UNIV = (τ ^^(i + 1)) UNIV"
by blast
qed

lemma lfp_loop:
assumes "finite (UNIV :: 'b set)" and "mono (τ :: ('b set  'b set))"
shows " n . lfp τ  = (τ ^^ n) {}"
proof -
have "i. (τ ^^ i) {} = (τ ^^ (i + (1))) {}"  using assms
by (rule finite_fixp)
from this obtain i where " (τ ^^ i) {} = (τ ^^ (i + (1))) {}"
by (erule exE)
hence "(τ ^^ i) {} = (τ ^^ Suc i) {}"
by simp
hence "(τ ^^ Suc i) {} = (τ ^^ i) {}"
by (rule sym)
hence "lfp τ = (τ ^^ i) {}"
thus " n . lfp τ  = (τ ^^ n) {}"
by (rule exI)
qed

text ‹These next two are repeated from the corresponding
theorems in HOL/ZF/Nat.thy for the sake of self-containedness of the exposition.›
lemma Kleene_iter_gpfp:
assumes "mono f" and "p  f p" shows "p  (f^^k) (top::'a::order_top)"
proof(induction k)
case 0 show ?case by simp
next
case Suc
from monoD[OF assms(1) Suc] assms(2)
show ?case by simp
qed

lemma gfp_loop:
assumes "finite (UNIV :: 'b set)"
and "mono (τ :: ('b set  'b set))"
shows " n . gfp τ  = (τ ^^ n)UNIV"
proof -
have " i. (τ ^^ i)(UNIV :: 'b set) = (τ ^^ (i + (1))) UNIV" using assms
by (rule finite_fixp2)
from this obtain i where "(τ ^^ i)UNIV = (τ ^^ (i + (1))) UNIV" by (erule exE)
thus " n . gfp τ  = (τ ^^ n)UNIV" using assms
by (metis Suc_eq_plus1 gfp_Kleene_iter)
qed

subsection ‹Generic type of state with state transition and CTL operators›
text ‹The system states and their transition relation are defined as a class called
@{text ‹state›} containing an abstract constant@{text ‹state_transition›}. It introduces the
syntactic infix notation @{text ‹I →i I'›} to denote that system state @{text ‹I›} and @{text ‹I'›}
are in this relation over an arbitrary (polymorphic) type @{text ‹'a›}.›
class state =
fixes state_transition :: "['a :: type, 'a]  bool"  (infixr "i" 50)

text ‹The above class definition lifts Kripke structures and CTL to a general level.
The definition of the inductive relation is given by a set of specific rules which are,
however, part of an application like infrastructures. Branching time temporal logic CTL
is defined in general over Kripke structures with arbitrary state transitions and can later
be applied to suitable theories, like infrastructures.
Based on the generic state transition @{text ‹→›} of the type class state, the CTL-operators
EX and AX express that property f holds in some or all next states, respectively.›

definition AX where "AX f  {s. {f0. s i f0}  f}"
definition EX' where "EX' f  {s .  f0  f. s i f0 }"

text ‹The CTL formula @{text ‹AG f›} means that on all paths branching from a state @{text ‹s›}
the formula @{text ‹f›} is always true (@{text ‹G›} stands for `globally'). It can be defined
using the Tarski fixpoint theory by applying the greatest fixpoint operator. In a similar way,
the other CTL operators are defined.›
definition AF where "AF f  lfp (λ Z. f  AX Z)"
definition EF where "EF f  lfp (λ Z. f  EX' Z)"
definition AG where "AG f  gfp (λ Z. f  AX Z)"
definition EG where "EG f  gfp (λ Z. f  EX' Z)"
definition AU where "AU f1 f2  lfp(λ Z. f2  (f1  AX Z))"
definition EU where "EU f1 f2  lfp(λ Z. f2  (f1  EX' Z))"
definition AR where "AR f1 f2  gfp(λ Z. f2  (f1  AX Z))"
definition ER where "ER f1 f2  gfp(λ Z. f2  (f1  EX' Z))"

subsection  ‹Kripke structures and Modelchecking›
datatype 'a kripke =
Kripke "'a set" "'a set"

primrec states where "states (Kripke S I) = S"
primrec init where "init (Kripke S I) = I"

text ‹The formal Isabelle definition of what it means that formula f holds
in a Kripke structure M can be stated as: the initial states of the Kripke
structure init M need to be contained in the set of all states states M that
imply f.›
definition check ("_  _" 50)
where "M  f  (init M)  {s  (states M). s  f }"

definition state_transition_refl (infixr "i*" 50)
where "s i* s'  ((s,s')  {(x,y). state_transition x y}*)"

subsection ‹Lemmas for CTL operators›

subsubsection ‹EF lemmas›
lemma EF_lem0: "(x  EF f) = (x  f  EX' (lfp (λZ :: ('a :: state) set. f  EX' Z)))"
proof -
have "lfp (λZ :: ('a :: state) set. f  EX' Z) =
f  (EX' (lfp (λZ :: 'a set. f  EX' Z)))"
by (rule def_lfp_unfold, rule reflexive, unfold mono_def EX'_def, auto)
thus "(x  EF (f :: ('a :: state) set)) = (x  f  EX' (lfp (λZ :: ('a :: state) set. f  EX' Z)))"
qed

lemma EF_lem00: "(EF f) = (f  EX' (lfp (λ Z :: ('a :: state) set. f  EX' Z)))"
by (auto simp: EF_lem0)

lemma EF_lem000: "(EF f) = (f  EX' (EF f))"
by (metis EF_def EF_lem00)

lemma EF_lem1: "x  f  x  (EX' (EF f))  x  EF f"
assume a: "x  f  x  EX' (lfp (λZ::'a set. f  EX' Z))"
show "x  lfp (λZ::'a set. f  EX' Z)"
proof -
have b: "lfp (λZ :: ('a :: state) set. f  EX' Z) =
f  (EX' (lfp (λZ :: ('a :: state) set. f  EX' Z)))"
using EF_def EF_lem00 by blast
thus "x  lfp (λZ::'a set. f  EX' Z)" using a
by (subst b, blast)
qed
qed

lemma EF_lem2b:
assumes "x  (EX' (EF f))"
shows "x  EF f"

lemma EF_lem2a: assumes "x  f" shows "x  EF f"

lemma EF_lem2c: assumes "x  f" shows "x  EF (- f)"

lemma EF_lem2d: assumes "x  EF f" shows "x  f"
using EF_lem1 assms by auto

lemma EF_lem3b: assumes "x  EX' (f  EX' (EF f))" shows "x  (EF f)"
by (metis EF_lem000 EF_lem2b assms)

lemma EX_lem0l: "x  (EX' f)  x  (EX' (f  g))"
by (auto simp: EX'_def)

lemma EX_lem0r: "x  (EX' g)  x  (EX' (f  g))"
by (auto simp: EX'_def)

lemma EX_step: assumes "x  i y" and "y  f" shows "x  EX' f"
using assms by (auto simp: EX'_def)

lemma EF_E[rule_format]: " f. x  (EF f)  x  (f  EX' (EF f))"
using EF_lem000 by blast

lemma EF_step: assumes "x  i y" and "y  f" shows "x  EF f"
using EF_lem3b EX_step assms by blast

lemma EF_step_step: assumes "x  i y" and "y  EF f" shows  "x  EF f"
using EF_lem2b EX_step assms by blast

lemma EF_step_star: " x  i* y; y  f   x  EF f"
show "(x, y)  {(x::'a, y::'a). x i y}*  y  f  x  EF f"
proof (erule converse_rtrancl_induct)
show "y  f  y  EF f"
by (erule EF_lem2a)
next show "ya z::'a. y  f
(ya, z)  {(x,y). x i y}
(z, y)  {(x,y). x i y}*  z  EF f  ya  EF f"
qed
qed

lemma EF_induct: "(a::'a::state)  EF f
mono (λ Z. f  EX' Z)
(x. x  ((λ Z. f  EX' Z)(EF f  {x::'a::state. P x}))  P x)
P a"
by (metis (mono_tags, lifting) EF_def def_lfp_induct_set)

lemma valEF_E: "M  EF f  x  init M  x  EF f"
by (auto simp: check_def)

lemma EF_step_star_rev[rule_format]: "x  EF s   ( y  s.  x  i* y)"
proof (erule EF_induct)
show "mono (λZ::'a set. s  EX' Z)"
by (force simp add: mono_def EX'_def)
next show "x::'a. x  s  EX' (EF s  {x::'a. y::'as. x i* y})  y::'as. x i* y"
apply (erule UnE)
using state_transition_refl_def apply auto[1]
by (auto simp add: EX'_def state_transition_refl_def intro: converse_rtrancl_into_rtrancl)
qed

lemma EF_step_inv: "(I  {sa::'s :: state. (iI. i i* sa)  sa  EF s})
x  I.  y  s. x i* y"
using EF_step_star_rev by fastforce

subsubsection ‹AG lemmas›

lemma AG_in_lem:   "x  AG s  x  s"
by (auto simp add: AG_def gfp_def)

lemma AG_lem1: "x  s  x  (AX (AG s))  x  AG s"
have "gfp (λZ::'a set. s  AX Z) = s  (AX (gfp (λZ::'a set. s  AX Z)))"
by (rule def_gfp_unfold) (auto simp: mono_def AX_def)
then show "x  s  x  AX (gfp (λZ::'a set. s  AX Z))  x  gfp (λZ::'a set. s  AX Z)"
by blast
qed

lemma AG_lem2: "x  AG s  x  (s  (AX (AG s)))"
proof -
have a: "AG s = s  (AX (AG s))"
unfolding AG_def
by (rule def_gfp_unfold) (auto simp: mono_def AX_def)
thus "x  AG s  x  (s  (AX (AG s)))"
by (erule subst)
qed

lemma AG_lem3: "AG s = (s  (AX (AG s)))"
using AG_lem1 AG_lem2 by blast

lemma AG_step: "y i z  y  AG s  z  AG s"
using AG_lem2 AX_def by blast

lemma AG_all_s: " x i* y  x  AG s  y  AG s"
show "(x, y)  {(x,y). x i y}*  x  AG s  y  AG s"
by (erule rtrancl_induct) (auto simp add: AG_step)
qed

lemma AG_imp_notnotEF:
"I  {}  ((Kripke {s.  i  I. (i i* s)} I   AG s))
(¬(Kripke {s.  i  I. (i i* s)} (I :: ('s :: state)set)   EF (- s)))"
proof (rule notI, simp add: check_def)
assume a0: "I  {}" and
a1: "I  {sa::'s. (iI. i i* sa)  sa  AG s}" and
a2: "I  {sa::'s. (iI. i i* sa)  sa  EF (- s)}"
show "False"
proof -
have a3: "{sa::'s. (iI. i i* sa)  sa  AG s}
{sa::'s. (iI. i i* sa)  sa  EF (- s)} = {}"
proof -
have "(? x. x  {sa::'s. (iI. i i* sa)  sa  AG s}
x  {sa::'s. (iI. i i* sa)  sa  EF (- s)})  False"
proof -
assume a4: "(? x. x  {sa::'s. (iI. i i* sa)  sa  AG s}
x  {sa::'s. (iI. i i* sa)  sa  EF (- s)})"
from a4 obtain x where  a5: "x  {sa::'s. (iI. i i* sa)  sa  AG s}
x  {sa::'s. (iI. i i* sa)  sa  EF (- s)}"
by (erule exE)
thus "False"
by (metis (mono_tags, lifting) AG_all_s AG_in_lem ComplD EF_step_star_rev a5 mem_Collect_eq)
qed
thus "{sa::'s. (iI. i i* sa)  sa  AG s}
{sa::'s. (iI. i i* sa)  sa  EF (- s)} = {}"
by blast
qed
moreover have b: "? x. x : I" using a0
by blast
moreover obtain x where "x  I"
using b by blast
ultimately show "False" using a0 a1 a2
by blast
qed
qed

text ‹A simplified way of Modelchecking is given by the following lemma.›
lemma check2_def: "(Kripke S I  f) = (I  S  f)"