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
contradiction point that
@{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).
If we can additionally show
@{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) {}"
by (simp add: assms(2) lfp_Kleene_iter)
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)))"
by (simp add: EF_def)
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"
proof (simp add: EF_def)
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"
by (simp add: EF_lem1 assms)
lemma EF_lem2a: assumes "x ∈ f" shows "x ∈ EF f"
by (simp add: EF_lem1 assms)
lemma EF_lem2c: assumes "x ∉ f" shows "x ∈ EF (- f)"
by (simp add: EF_lem1 assms)
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"
proof (simp add: state_transition_refl_def)
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"
by (simp add: EF_step_step)
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::'a∈s. x →⇩i* y}) ⟹ ∃y::'a∈s. 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. (∃i∈I. 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"
proof (simp add: AG_def)
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"
proof (simp add: state_transition_refl_def)
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. (∃i∈I. i →⇩i* sa) ∧ sa ∈ AG s}" and
a2: "I ⊆ {sa::'s. (∃i∈I. i →⇩i* sa) ∧ sa ∈ EF (- s)}"
show "False"
proof -
have a3: "{sa::'s. (∃i∈I. i →⇩i* sa) ∧ sa ∈ AG s} ∩
{sa::'s. (∃i∈I. i →⇩i* sa) ∧ sa ∈ EF (- s)} = {}"
proof -
have "(? x. x ∈ {sa::'s. (∃i∈I. i →⇩i* sa) ∧ sa ∈ AG s} ∧
x ∈ {sa::'s. (∃i∈I. i →⇩i* sa) ∧ sa ∈ EF (- s)}) ⟹ False"
proof -
assume a4: "(? x. x ∈ {sa::'s. (∃i∈I. i →⇩i* sa) ∧ sa ∈ AG s} ∧
x ∈ {sa::'s. (∃i∈I. i →⇩i* sa) ∧ sa ∈ EF (- s)})"
from a4 obtain x where a5: "x ∈ {sa::'s. (∃i∈I. i →⇩i* sa) ∧ sa ∈ AG s} ∧
x ∈ {sa::'s. (∃i∈I. 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. (∃i∈I. i →⇩i* sa) ∧ sa ∈ AG s} ∩
{sa::'s. (∃i∈I. 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)"
by (auto simp add: check_def)
end