Quelle  MC.thy

section "Kripke structures and CTL"

text ‹We apply Kripke structures and CTL to model state based systems and analyse properties under
  state changes. Snapshots of systems are the states on which we define a state transition.
  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:
  @{text predtrans_empty} we know

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

  we can additionally show

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

  can get the goal together with equalityI
 {text "⊆ + 🪙 ⟶ ="}.
  prove (1) we observe that
 {term "(τ ^^ i)({}) 🪙 (τ ^^(i + 1))({})"}
  be inferred from
 {term "¬((τ ^^ i)({}) ⊆ (τ ^^(i + 1))({}))"}
  (1).
 , 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
  infix notation @{text ‹I →_i I'›} to denote that system state @{text ‹I›} and @{text ‹I'›}
  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.
  definition of the inductive relation is given by a set of specific rules which are,
 , part of an application like infrastructures. Branching time temporal logic CTL
  defined in general over Kripke structures with arbitrary state transitions and can later
  applied to suitable theories, like infrastructures.
  on the generic state transition @{text ‹→›} of the type class state, the CTL-operators
  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›}
  formula @{text ‹f›} is always true (@{text ‹G›} stands for `globally'). It can be defined
  the Tarski fixpoint theory by applying the greatest fixpoint operator. In a similar way,
  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
  a Kripke structure M can be stated as: the initial states of the Kripke
  init M need to be contained in the set of all states states M that
  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