Quelle  AT.thy

section "Attack Trees"
theory AT
imports MC 
begin

text ‹Attack Trees are an intuitive and practical formal method to analyse and quantify
  on security and privacy. They are very useful to identify the steps an attacker
  through a system when approaching the attack goal. Here, we provide
  proof calculus to analyse concrete attacks using a notion of attack validity.
  define a state based semantics with Kripke models and the temporal logic
  in the proof assistant Isabelle cite‹"npw:02"› using its Higher Order Logic
 HOL). We prove the correctness and completeness (adequacy) of Attack Trees in Isabelle
  respect to the model.›

subsection "Attack Tree datatype"
text ‹The following datatype definition @{text ‹attree›} defines attack trees.
  simplest case of an attack tree is a base attack.
  principal idea is that base attacks are defined by a pair of
  sets representing the initial states and the {\it attack property}
 - a set of states characterized by the fact that this property holds
  them.
  can also be combined as the conjunction or disjunction of other attacks.
  operator @{text ‹⊕_\∨›} creates or-trees and @{text ‹⊕_\∧›} creates and-trees.
 -attack trees @{text ‹l ⊕_\∧ s›} and or-attack trees @{text ‹l ⊕_\∨ s›}
  lists of attack trees $l$ either conjunctively or disjunctively and
  of a list of sub-attacks -- again attack trees.›
datatype ('s :: state) attree = BaseAttack "('s set) * ('s set)" (‹N_{_)}›) |
                  AndAttack "('s attree) list" "('s set) * ('s set)" (‹_ ⊕_\∧^_)› 60) | 
                  OrAttack  "('s attree) list" "('s set) * ('s set)" (‹_ ⊕_\∨^_)› 61)

primrec attack :: "('s :: state) attree ==> ('s set) * ('s set)"
  where 
"attack (BaseAttack b) = b"|
"attack (AndAttack as s) = s"  | 
"attack (OrAttack as s) = s"

subsection ‹Attack Tree refinement›
text ‹When we develop an attack tree, we proceed from an abstract attack, given
  an attack goal, by breaking it down into a series of sub-attacks. This
  corresponds to a process of {\it refinement}. Therefore, as part of
  attack tree calculus, we provide a notion of attack tree refinement.

  relation @{text ‹refines_to›} "constructs" the attack tree. Here the above
  attack vectors are used to define how nodes in an attack tree
  be expanded into more detailed (refined) attack sequences. This
  of refinement @{text "⊑"} allows to eventually reach a fully detailed
  that can then be proved using @{text "⊨"}.›
inductive refines_to :: "[('s :: state) attree, 's attree] ==> bool" (‹_ ⊑ _› [40] 40)
where 
refI: "[ A = ((l @ [ N_si',si'')] @ l'')⊕_\<and>^si,si''') );
          A' = (l' ⊕_\<and>^si',si''));
          A'' = (l @ l' @ l'' ⊕_\<and>^si,si'''))
        ] ==> A ⊑ A''"| 
ref_or: "[ as ≠ []; ∀ A' ∈ set(as). (A ⊑ A') ∧ attack A = s ] ==> A ⊑ (as ⊕_\<or>)" |
ref_trans: "[ A ⊑ A'; A' ⊑ A'' ] ==> A ⊑ A''"|
ref_refl : "A ⊑ A"


subsection ‹Validity of Attack Trees›
text ‹A valid attack, intuitively, is one which is fully refined into fine-grained
  that are feasible in a model. The general model we provide is
  Kripke structure, i.e., a set of states and a generic state transition.
 , feasible steps in the model are single steps of the state transition.
  call them valid base attacks.
  composition of sequences of valid base attacks into and-attacks yields
  valid attacks if the base attacks line up with respect to the states
  the state transition. If there are different valid attacks for the same
  goal starting from the same initial state set, these can be
  in an or-attack.
  precisely, the different cases of the validity predicate are distinguished
  pattern matching over the attack tree structure.
 begin{itemize}
 item A base attack @{text ‹N(s0,s1)›} is valid if from all
  in the pre-state set @{text ‹s0›} we can get with a single step of the
  transition relation to a state in the post-state set ‹s1›. Note,
  it is sufficient for a post-state to exist for each pre-state. After all,
  are aiming to validate attacks, that is, possible attack paths to some
  that fulfills the attack property.
 item An and-attack @{text ‹As ⊕_\∧ (s0,s1)›} is a valid attack
 if either of the following cases holds:
 \begin{itemize}
 \item empty attack sequence @{text ‹As›}: in this case
 all pre-states in @{text ‹s0›} must already be attack states
 in @{text ‹s1›}, i.e., @{text ‹s0 ⊆ s1›};
 \item attack sequence @{text ‹As›} is singleton: in this case, the
 singleton element attack @{text ‹a›} in @{text ‹[a]›},
 must be a valid attack and it must be an attack with pre-state
 @{text ‹s0›} and post-state @{text ‹s1›};
 \item otherwise, @{text ‹As›} must be a list matching @{text ‹a # l›} for
 some attack @{text ‹a›} and tail of attack list @{text ‹l›} such that
 @{text ‹a›} is a valid attack with pre-state identical to the overall
 pre-state @{text ‹s0›} and the goal of the tail @{text ‹l›} is
 @{text ‹s1›} the goal of the overall attack. The pre-state of the
 attack represented by @{text ‹l›} is @{text ‹snd(attack a)›} since this is
 the post-state set of the first step @{text ‹a›}.
 end{itemize}
 \item An or-attack @{text ‹As ⊕_\∨(s0,s1)›} is a valid attack
 if either of the following cases holds:
 \begin{itemize}
 \item the empty attack case is identical to the and-attack above:
 @{text ‹s0 ⊆ s1›};
 \item attack sequence @{text ‹As›} is singleton: in this case, the
 singleton element attack @{text ‹a›}
 must be a valid attack and
 its pre-state must include the overall attack pre-state set @{text ‹s0›}
 (since @{text ‹a›} is singleton in the or) while the post-state of
 @{text ‹a›} needs to be included in the global attack goal @{text ‹s1›};
 \item otherwise, @{text ‹As›} must be a list @{text ‹a # l›} for
 an attack @{text ‹a›} and a list @{text ‹l›} of alternative attacks.
 The pre-states can be just a subset of @{text ‹s0›} (since there are
 other attacks in @{text ‹l›} that can cover the rest) and the goal
 states @{text ‹snd(attack a)›} need to lie all in the overall goal
 state @{text ‹set s1›}. The other or-attacks in @{text ‹l›} need
 to cover only the pre-states @{text ‹fst s - fst(attack a)›}
 (where @{text ‹-›} is set difference) and have the same goal @{text ‹snd s›}.
 \end{itemize}
 end{itemize}
  proof calculus is thus completely described by one recursive function. ›
fun is_attack_tree :: "[('s :: state) attree] ==> bool"  (‹⊨_› [40] 40) 
where 
att_base:  "(⊨ N) = ( (∀ x ∈ (fst s). (∃ y ∈ (snd s). x →_i y )))" |
att_and: "(⊨(As ⊕_\<and>)) =
               (case As of
                  [] ==> (fst s ⊆ snd s)
                | [a] ==> ( ⊨ a ∧ attack a = s)
                | (a # l) ==> (( ⊨ a) ∧ (fst(attack a) = fst s) ∧
                            (⊨(l ⊕_\<and>^{snd(attack a),snd(s))}))))" |
att_or: "(⊨(As ⊕_\<or>)) =
               (case As of
                  [] ==> (fst s ⊆ snd s)
                | [a] ==> ( ⊨ a ∧ (fst(attack a) 🪙 fst s) ∧ (snd(attack a) ⊆ snd s))
                | (a # l) ==> (( ⊨ a) ∧ fst(attack a) ⊆ fst s ∧
                              snd(attack a) ⊆ snd s ∧
                       ( ⊨(l ⊕_\<or>^{fst s - fst(attack a), snd s)}))))" 
text ‹Since the definition is constructive, code can be generated directly from it, here
  the programming language Scala.›
export_code is_attack_tree in Scala    

subsection "Lemmas for Attack Tree validity"
lemma att_and_one: assumes "⊨ a" and  "attack a = s"
  shows  "⊨([a] ⊕_\<and>)"
proof -
  show " ⊨([a] ⊕_\<and>)" using assms
    by (subst att_and, simp del: att_and att_or)
qed

declare is_attack_tree.simps[simp del]
  
lemma att_and_empty[rule_format] : " ⊨([] ⊕_\<and>^{s', s'')}) ⟶ s' ⊆ s''"
  by (simp add: is_attack_tree.simps(2))

lemma att_and_empty2: " ⊨([] ⊕_\<and>^{s, s)})"
  by (simp add: is_attack_tree.simps(2))

lemma att_or_empty[rule_format] : " ⊨([] ⊕_\<or>^{s', s'')}) ⟶ s' ⊆ s''"
  by (simp add: is_attack_tree.simps(3))

lemma att_or_empty_back[rule_format]: " s' ⊆ s'' ⟶ ⊨([] ⊕_\<or>^{s', s'')})"
  by (simp add: is_attack_tree.simps(3))

lemma att_or_empty_rev: assumes "⊨(l ⊕_\<or>^{s, s')})" and "¬(s ⊆ s')" shows "l ≠ []"    
  using assms att_or_empty by blast

lemma att_or_empty2: "⊨([] ⊕_\<or>^{s, s)})"
  by (simp add: att_or_empty_back)

lemma att_andD1: " ⊨(x1 # x2 ⊕_\<and>) ==> ⊨ x1"
  by (metis (no_types, lifting) is_attack_tree.simps(2) list.exhaust list.simps(4) list.simps(5))

lemma att_and_nonemptyD2[rule_format]: 
       "(x2 ≠ [] ⟶ ⊨(x1 # x2 ⊕_\<and>) ⟶ ⊨ (x2 ⊕_\<and>^{snd(attack x1),snd s)}))" 
  by (metis (no_types, lifting) is_attack_tree.simps(2) list.exhaust list.simps(5)) 

lemma att_andD2 : " ⊨(x1 # x2 ⊕_\<and>) ==> ⊨ (x2 ⊕_\<and>^{snd(attack x1),snd s)})" 
  by (metis (mono_tags, lifting) att_and_empty2 att_and_nonemptyD2 is_attack_tree.simps(2) list.simps(4) list.simps(5))
    
lemma att_and_fst_lem[rule_format]: 
   "⊨(x1 # x2a ⊕_\<and>) ⟶ xa ∈ fst (attack (x1 # x2a ⊕_\<and>))
                     ⟶ xa ∈ fst (attack x1)"  
  by (induction x2a, (subst att_and, simp)+)

lemma att_orD1: " ⊨(x1 # x2 ⊕_\<or>) ==> ⊨ x1"
  by (case_tac x2, (subst (asm) att_or, simp)+)
    
lemma att_or_snd_hd: " ⊨(a # list ⊕_\<or>^{aa, b)}) ==> snd(attack a) ⊆ b"
  by (case_tac list,  (subst (asm) att_or, simp)+)
 
lemma att_or_singleton[rule_format]: 
   " ⊨([x1] ⊕_\<or>) ⟶ ⊨([] ⊕_\<or>^{fst x - fst (attack x1), snd x)})" 
  by (subst att_or, simp, rule impI, rule att_or_empty_back, blast)

lemma att_orD2[rule_format]: 
     " ⊨(x1 # x2 ⊕_\<or>) ⟶ ⊨ (x2 ⊕_\<or>^{fst x - fst(attack x1), snd x)})"
  by (case_tac x2, simp add: att_or_singleton, simp, subst att_or, simp)

lemma att_or_snd_att[rule_format]: "∀ x. ⊨ (x2 ⊕_\<or>) ⟶ (∀ a ∈ (set x2). snd(attack a) ⊆ snd x )" 
proof (induction x2)
  case Nil
  then show ?case by (simp add: att_or)
next
  case (Cons a x2)
  then show ?case using att_orD2 att_or_snd_hd by fastforce
qed

lemma singleton_or_lem: " ⊨([x1] ⊕_\<or>) ==> fst x ⊆ fst(attack x1)"
  by (subst (asm) att_or, simp)+

lemma or_att_fst_sup0[rule_format]: "x2 ≠ [] ⟶ (∀ x. (⊨ ((x2 ⊕_\<or>):: ('s :: state) attree)) ⟶
                      ((∪ y::'s attree∈ set x2. fst (attack y)) 🪙 fst(x))) "
proof (induction x2)
  case Nil
  then show ?case by simp
next
  case (Cons a x2)
  then show ?case using att_orD2 singleton_or_lem by fastforce
qed

lemma or_att_fst_sup: 
    assumes "(⊨ ((x1 # x2 ⊕_\<or>):: ('s :: state) attree))"
    shows   "((∪ y::'s attree∈ set (x1 # x2). fst (attack y)) 🪙 fst(x))"
  by (rule or_att_fst_sup0, simp, rule assms)

text ‹The lemma @{text ‹att_elem_seq›} is the main lemma for Correctness.
 It shows that for a given attack tree x1, for each element in the set of start sets
 of the first attack, we can reach in zero or more steps a state in the states in which
 the attack is successful (the final attack state @{text ‹snd(attack x1)›}).
 This proof is a big alternative to an earlier version of the proof with
 @{text ‹first_step›} etc that mapped first on a sequence of sets of states.›
lemma att_elem_seq[rule_format]: "⊨ x1 ⟶ (∀ x ∈ fst(attack x1).
                     (∃ y. y ∈ snd(attack x1) ∧ x →_i* y))"
  text ‹First attack tree induction›
proof (induction x1)
  case (BaseAttack x)
  then show ?case
    by (metis AT.att_base EF_step EF_step_star_rev attack.simps(1))
next
  case (AndAttack x1a x2)
  then show ?case
    apply (rule_tac x = x2 in spec)
    apply (subgoal_tac "(∀ x1aa::'a attree.
                              x1aa ∈ set x1a ⟶
                               ⊨x1aa ⟶
                               (∀x::'a∈fst (attack x1aa). ∃y::'a. y ∈ snd (attack x1aa) ∧ x →_i* y))")
     apply (rule mp)
      prefer 2
      apply (rotate_tac -1)
      apply assumption
    text ‹Induction for @{text ‹∧›}: the manual instantiation seems tedious but in the @{text ‹∧›}
 case necessary to get the right induction hypothesis.›
  proof (rule_tac list = "x1a" in list.induct)
    text ‹The @{text ‹∧›} induction empty case›
    show "(∀x1aa::'a attree.
           x1aa ∈ set [] ⟶
           ⊨x1aa ⟶ (∀x::'a∈fst (attack x1aa). ∃y::'a. y ∈ snd (attack x1aa) ∧ x →_i* y)) ⟶
       (∀x::'a set × 'a set.
           ⊨([] ⊕_\<and>) ⟶
           (∀xa::'a∈fst (attack ([] ⊕_\<and>)). ∃y::'a. y ∈ snd (attack ([] ⊕_\<and>)) ∧ xa →_i* y))"
      using att_and_empty state_transition_refl_def by fastforce
    text ‹The @{text ‹∧›} induction case nonempty›
  next show "∧(x1a::'a attree list) (x2::'a set × 'a set) (x1::'a attree) (x2a::'a attree list).
       (∧x1aa::'a attree.
           (x1aa ∈ set x1a) ==>
           ((⊨x1aa) ⟶ (∀x::'a∈fst (attack x1aa). ∃y::'a. y ∈ snd (attack x1aa) ∧ x →_i* y))) ==>
       ∀x1aa::'a attree.
          (x1aa ∈ set x1a) ⟶
          (⊨x1aa) ⟶ ((∀x::'a∈fst (attack x1aa). ∃y::'a. y ∈ snd (attack x1aa) ∧ x →_i* y)) ==>
       (∀x1aa::'a attree.
           (x1aa ∈ set x2a) ⟶
           (⊨x1aa) ⟶ (∀x::'a∈fst (attack x1aa). ∃y::'a. y ∈ snd (attack x1aa) ∧ x →_i* y)) ⟶
       (∀x::'a set × 'a set.
           (⊨(x2a ⊕_\<and>)) ⟶
           ((∀xa::'a∈fst (attack (x2a ⊕_\<and>)). ∃y::'a. y ∈ snd (attack (x2a ⊕_\<and>)) ∧ xa →_i* y))) ==>
       ((∀x1aa::'a attree.
           (x1aa ∈ set (x1 # x2a)) ⟶
           (⊨x1aa) ⟶ ((∀x::'a∈fst (attack x1aa). ∃y::'a. y ∈ snd (attack x1aa) ∧ x →_i* y))) ⟶
       (∀x::'a set × 'a set.
          ( ⊨(x1 # x2a ⊕_\<and>)) ⟶
           (∀xa::'a∈fst (attack (x1 # x2a ⊕_\<and>)).
               (∃y::'a. y ∈ snd (attack (x1 # x2a ⊕_\<and>)) ∧ (xa →_i* y)))))"
      apply (rule impI, rule allI, rule impI)
      text ‹Set free the Induction Hypothesis: this is necessary to provide the grounds for specific
 instantiations in the step.›
      apply (subgoal_tac "(∀x::'a set × 'a set.
                             ⊨(x2a ⊕_\<and>) ⟶
                             (∀xa::'a∈fst (attack (x2a ⊕_\<and>)).
                              ∃y::'a. y ∈ snd (attack (x2a ⊕_\<and>)) ∧ xa →_i* y))")
       prefer 2
       apply simp
      text ‹The following induction step for @{text ‹∧›} needs a number of manual instantiations
 so that the proof is not found automatically. In the subsequent case for @{text ‹∨›},
 sledgehammer finds the proof.›
    proof -
      show "∧(x1a::'a attree list) (x2::'a set × 'a set) (x1::'a attree) (x2a::'a attree list) x::'a set × 'a set.
       ∀x1aa::'a attree.
          x1aa ∈ set (x1 # x2a) ⟶
          ⊨x1aa ⟶ (∀x::'a∈fst (attack x1aa). ∃y::'a. y ∈ snd (attack x1aa) ∧ x →_i* y) ==>
       ⊨(x1 # x2a ⊕_\<and>) ==>
       ∀x::'a set × 'a set.
          ⊨(x2a ⊕_\<and>) ⟶
          (∀xa::'a∈fst (attack (x2a ⊕_\<and>)). ∃y::'a. y ∈ snd (attack (x2a ⊕_\<and>)) ∧ xa →_i* y) ==>
       ∀xa::'a∈fst (attack (x1 # x2a ⊕_\<and>)). ∃y::'a. y ∈ snd (attack (x1 # x2a ⊕_\<and>)) ∧ xa →_i* y"
        apply (rule ballI)
        apply (rename_tac xa)
        text ‹Prepare the steps›
        apply (drule_tac x = "(snd(attack x1), snd x)" in spec)
        apply (rotate_tac -1)
        apply (erule impE)
         apply (erule att_andD2)
        text ‹Premise for x1›
        apply (drule_tac x = x1 in spec)
        apply (drule mp)
         apply simp
        apply (drule mp)
         apply (erule att_andD1)
        text ‹Instantiate first step for xa›
        apply (rotate_tac -1)
        apply (drule_tac x = xa in bspec)
         apply (erule att_and_fst_lem, assumption)
        apply (erule exE)
        apply (erule conjE)
        text ‹Take this y and put it as first into the second part›
        apply (drule_tac x = y in bspec)
         apply simp
        apply (erule exE)
        apply (erule conjE)
        text ‹Bind the first @{text ‹xa →_i* y›} and second @{text ‹y →_i* ya›} together for solution›
        apply (rule_tac x = ya in exI)
        apply (rule conjI)
         apply simp
        by (simp add: state_transition_refl_def)
    qed
  qed auto
next
  case (OrAttack x1a x2)
  then show ?case
  proof (induction x1a arbitrary: x2)
    case Nil
    then show ?case
      by (metis EF_lem2a EF_step_star_rev att_or_empty attack.simps(3) subsetD surjective_pairing)
  next
    case (Cons a x1a)
    then show ?case
      by (smt DiffI att_orD1 att_orD2 att_or_snd_att attack.simps(3) insert_iff list.set(2) prod.sel(1) snd_conv subset_iff) 
  qed
qed

  
lemma att_elem_seq0: "⊨ x1 ==> (∀ x ∈ fst(attack x1).
                     (∃ y. y ∈ snd(attack x1) ∧ x →_i* y))"
  by (simp add: att_elem_seq)
          
subsection ‹Valid refinements›
definition valid_ref :: "[('s :: state) attree, 's attree] ==> bool" (‹_ ⊑_V _› 50)
  where
"A ⊑_V A' ≡ ( (A ⊑ A') ∧ ⊨ A')"

definition ref_validity :: "[('s :: state) attree] ==> bool" (‹⊨_V _› 50)
  where
"⊨_V A ≡ (∃ A'. (A ⊑_V A'))"

lemma ref_valI: " A ⊑ A'==> ⊨ A' ==> ⊨_V A"
  using ref_validity_def valid_ref_def by blast

section "Correctness and Completeness"
text ‹This section presents the main theorems of Correctness and Completeness
 between AT and Kripke, essentially:

 {text ‹⊨ (init K, p) ≡ K ⊨ EF p›}.

 , we proof a number of lemmas needed for both directions before we
  the Correctness theorem followed by the Completeness theorem.
 ›    
subsection ‹Lemma for Correctness and Completeness›
lemma nth_app_eq[rule_format]: 
              "∀ sl x. sl ≠ [] ⟶ sl ! (length sl - Suc (0)) = x
              ⟶ (l @ sl) ! (length l + length sl - Suc (0)) = x"    
  by (induction l) auto

lemma nth_app_eq1[rule_format]: "i < length sla ==> (sla @ sl) ! i = sla ! i"
  by (simp add: nth_append)

lemma nth_app_eq1_rev:   "i < length sla ==> sla ! i = (sla @ sl) ! i"
  by (simp add: nth_append)

lemma nth_app_eq2[rule_format]: "∀ sl i. length sla ≤ i ∧ i < length (sla @ sl)
                     ⟶ (sla @ sl) ! i = sl ! (i - (length sla))"
  by (simp add: nth_append)


lemma tl_ne_ex[rule_format]: "l ≠ [] ⟶ (? x . l = x # (tl l))"
  by (induction l, auto)


lemma tl_nempty_lngth[rule_format]: "tl sl ≠ [] ⟶ 2 ≤ length(sl)"
  using le_less by fastforce
  
lemma list_app_one_length: "length l = n ==> (l @ [s]) ! n = s"
  by (erule subst, simp)
  
lemma tl_lem1[rule_format]: "l ≠ [] ⟶ tl l = [] ⟶ length l = 1"
  by (induction l, simp+)

lemma nth_tl_length[rule_format]: "tl sl ≠ [] ⟶
      tl sl ! (length (tl sl) - Suc (0)) = sl ! (length sl - Suc (0))" 
  by (induction sl, simp+)

lemma nth_tl_length1[rule_format]: "tl sl ≠ [] ⟶
      tl sl ! n = sl ! (n + 1)" 
  by (induction sl, simp+)
   
lemma ineq1: "i < length sla - n ==>
       (0) ≤ n ==> i < length sla"  
by simp

lemma ineq2[rule_format]: "length sla ≤ i ⟶ i + (1) - length sla = i - length sla + 1"
by arith

lemma ineq3: "tl sl ≠ [] ==> length sla ≤ i ==> i < length (sla @ tl sl) - (1)
              ==> i - length sla + (1) < length sl - (1)"    
by simp

lemma tl_eq1[rule_format]: "sl ≠ [] ⟶ tl sl ! (0) = sl ! Suc (0)"  
  by (induction sl, simp+)

lemma tl_eq2[rule_format]: "tl sl = [] ⟶ sl ! (0) = sl ! (length sl - (1))"
  by (induction sl, simp+)

lemma tl_eq3[rule_format]: "tl sl ≠ [] ⟶
    tl sl ! (length sl - Suc (Suc (0))) = sl ! (length sl - Suc (0))"    
  by (induction sl, simp+)

lemma nth_app_eq3: assumes "tl sl ≠ []"
  shows "(sla @ tl sl) ! (length (sla @ tl sl) - (1)) = sl ! (length sl - (1))"
  using assms nth_app_eq nth_tl_length by fastforce 

lemma not_empty_ex: "A ≠ {} ==> ? x. x ∈ A"
by force

lemma fst_att_eq: "(fst x # sl) ! (0) = fst (attack (al ⊕_\<and>))"
by simp

lemma list_eq1[rule_format]: "sl ≠ [] ⟶
     (fst x # sl) ! (length (fst x # sl) - (1)) = sl ! (length sl - (1))"
  by (induction sl, auto)

lemma attack_eq1: "snd (attack (x1 # x2a ⊕_\<and>)) = snd (attack (x2a ⊕_\<and>^{snd (attack x1), snd x)}))"
by simp

lemma fst_lem1[rule_format]: "∀ (a:: 's set) b (c :: 's set) d. (a, c) = (b, d) ⟶ a = b"
by auto

lemma fst_eq1: "(sla ! (0), y) = attack x1 ==>
       sla ! (0) = fst (attack x1)"
  by (rule_tac c = y and d = "snd(attack x1)" in fst_lem1, simp)
    
lemma base_att_lem1: " y0 ⊆ y1 ==> ⊨ N_{y1, y)} ==>⊨ N_{y0, y)}"
  by (simp add: att_base, blast)

lemma ref_pres_att: "A ⊑ A' ==> attack A = attack A'"
proof (erule refines_to.induct)
  show "∧(A::'a attree) (l::'a attree list) (si'::'a set) (si''::'a set) (l''::'a attree list) (si::'a set)
       (si'''::'a set) (A'::'a attree) (l'::'a attree list) A''::'a attree.
       A = (l @ [N_{si', si'')}] @ l'' ⊕_\<and>^{si, si''')}) ==>
       A' = (l' ⊕_\<and>^{si', si'')}) ==> A'' = (l @ l' @ l'' ⊕_\<and>^{si, si''')}) ==> attack A = attack A''"
    by simp
next show "∧(as::'a attree list) (A::'a attree) (s::'a set × 'a set).
       as ≠ [] ==>
       (∀A'::'a attree∈ (set as). ((A ⊑ A') ∧ (attack A = attack A')) ∧ attack A = s) ==>
       attack A = attack (as ⊕_\<or>)"
    using last_in_set by auto
next show "∧(A::'a attree) (A'::'a attree) A''::'a attree.
       A ⊑ A' ==> attack A = attack A' ==> A' ⊑ A'' ==> attack A' = attack A'' ==> attack A = attack A''"
    by simp
next show "∧A::'a attree. attack A = attack A" by (rule refl)
qed

lemma  base_subset: 
    assumes "xa ⊆ xc"
    shows  "⊨N_{x, xa)} ==> ⊨N_{x, xc)}" 
proof (simp add: att_base)
  show " ∀x::'a∈x. ∃xa::'a∈xa. x →_i xa ==> ∀x::'a∈x. ∃xa::'a∈xc. x →_i xa"
    by (meson assms in_mono)
qed

subsection "Correctness Theorem"
text ‹Proof with induction over the definition of EF using the main
  @{text ‹att_elem_seq0›}.

  is also a second version of Correctness for valid refinements.›

theorem AT_EF: assumes " ⊨ (A :: ('s :: state) attree)"
               and  "attack A = (I,s)"
               shows "Kripke {s :: ('s :: state). ∃ i ∈ I. (i →_i* s)} (I :: ('s :: state)set) ⊨ EF s"
proof (simp add:check_def)
  show "I ⊆ {sa::('s :: state). (∃i::'s∈I. i →_i* sa) ∧ sa ∈ EF s}" 
  proof (rule subsetI, rule CollectI, rule conjI, simp add: state_transition_refl_def)
    show "∧x::'s. x ∈ I ==> ∃i::'s∈I. (i, x) ∈ {(x::'s, y::'s). x →_i y}^*"
    by (rule_tac x = x in bexI, simp)
next show "∧x::'s. x ∈ I ==> x ∈ EF s" using assms
  proof -
    have a: "∀ x ∈ I. ∃ y ∈ s. x →_i* y" using assms
    proof -
      have "∀x::'s∈fst (attack A). ∃y::'s. y ∈ snd (attack A) ∧ x →_i* y"
        by (rule att_elem_seq0, rule assms)
      thus " ∀x::'s∈I. ∃y::'s∈s. x →_i* y" using assms
      by force  
    qed
    thus "∧x::'s. x ∈ I ==> x ∈ EF s" 
    proof -
      fix x
      assume b: "x ∈ I"
      have "∃y::'s∈s::('s :: state) set. x →_i* y" 
        by (rule_tac x = x and A = I in bspec, rule a, rule b)
      from this obtain y where "y ∈ s" and "x →_i* y" by (erule bexE)
      thus "x ∈ EF s" 
       by (erule_tac f = s in EF_step_star)
   qed  
  qed
 qed
qed

theorem ATV_EF: "[ ⊨_V A; (I,s) = attack A ] ==>
 (Kripke {s. ∃ i ∈ I. (i →_i* s) } I ⊨ EF s)"
  by (metis (full_types) AT_EF ref_pres_att ref_validity_def valid_ref_def) 
    
subsection "Completeness Theorem"
text ‹This section contains the completeness direction, informally:

 {text ‹⊨ EF s ==> ∃ A. ⊨ A ∧ attack A = (I,s)›}.

  main theorem is presented last since its
  just summarises a number of main lemmas @{text ‹Compl_step1, Compl_step2,
 , Compl_step4›} which are presented first together with other
  lemmas.›

subsubsection "Lemma @{text ‹Compl_step1›}"
lemma Compl_step1: 
"Kripke {s :: ('s :: state). ∃ i ∈ I. (i →_i* s)} I ⊨ EF s
\<Longrightarrow> ∀ x ∈ I. ∃ y ∈ s. x →_i* y"
  by (simp add: EF_step_star_rev valEF_E)

subsubsection "Lemma @{text ‹Compl_step2›}"
text ‹First, we prove some auxiliary lemmas.›
lemma rtrancl_imp_singleton_seq2: "x →_i* y ==>
          x = y ∨ (∃ s. s ≠ [] ∧ (tl s ≠ []) ∧ s ! 0 = x ∧ s ! (length s - 1) = y ∧
               (∀ i < (length s - 1). (s ! i) →_i (s ! (Suc i))))"

  unfolding state_transition_refl_def
proof (induction rule: rtrancl_induct)
  case base
  then show ?case
    by simp
next
  case (step y z)
  show ?case
    using step.IH
  proof (elim disjE exE conjE)
    assume "x=y"
    with step.hyps show ?case
      by (force intro!: exI [where x="[y,z]"])
  next
    show "∧s. [s ≠ []; tl s ≠ []; s ! 0 = x;
          s ! (length s - 1) = y;
          ∀i<length s - 1.
             s ! i →_i s ! Suc i]
         ==> x = z ∨
             (∃s. s ≠ [] ∧
                  tl s ≠ [] ∧ s ! 0 = x ∧
                  s ! (length s - 1) = z ∧
                  (∀i<length s - 1. s ! i →_i s ! Suc i))"
      apply (rule disjI2)
      apply (rule_tac x="s @ [z]" in exI)
      apply (auto simp: nth_append)
      by (metis One_nat_def Suc_lessI diff_Suc_1 mem_Collect_eq old.prod.case step.hyps(2))
  qed
qed

lemma tl_nempty_length[rule_format]: "s ≠ [] ⟶ tl s ≠ [] ⟶ 0 < length s - 1"
  by (induction s, simp+)

lemma tl_nempty_length2[rule_format]: "s ≠ [] ⟶ tl s ≠ [] ⟶ Suc 0 < length s"
  by (induction s, simp+)

lemma length_last[rule_format]: "(l @ [x]) ! (length (l @ [x]) - 1) = x"
  by (induction l, simp+)

lemma Compl_step2: "∀ x ∈ I. ∃ y ∈ s. x →_i* y ==>
                   ( ∀ x ∈ I. x ∈ s ∨ (∃ (sl :: ((('s :: state) set)list)).
                  (sl ≠ []) ∧ (tl sl ≠ []) ∧
                 (sl ! 0, sl ! (length sl - 1)) = ({x},s) ∧
                 (∀ i < (length sl - 1). ⊨ N_{sl ! i,sl ! (i+1) )}
                         )))"
proof (rule ballI, drule_tac x = x in bspec, assumption, erule bexE)
  fix x y
  assume a: "x ∈ I" and b: "y ∈ s" and  c: "x →_i* y"
  show "x ∈ s ∨
       (∃sl::'s set list.
           sl ≠ [] ∧
           tl sl ≠ [] ∧
           (sl ! (0), sl ! (length sl - (1))) = ({x}, s) ∧
           (∀i<length sl - (1). ⊨N_{sl ! i, sl ! (i + (1)))}))"
  proof -
    have d : "x = y ∨
       (∃s'. s' ≠ [] ∧
           tl s' ≠ [] ∧
           s' ! (0) = x ∧
           s' ! (length s' - (1)) = y ∧ (∀i<length s' - (1). s' ! i →_i s' ! Suc i))"
      using c rtrancl_imp_singleton_seq2 by blast
    thus "x ∈ s ∨
       (∃sl::'s set list.
           sl ≠ [] ∧
           tl sl ≠ [] ∧
           (sl ! (0), sl ! (length sl - (1))) = ({x}, s) ∧
           (∀i<length sl - (1). ⊨N_{sl ! i, sl ! (i + (1)))}))"
      apply (rule disjE)
      using b apply blast
      apply (rule disjI2, elim conjE exE)
      apply (rule_tac x = "[{s' ! j}. j ← [0..<(length s' - 1)]] @ [s]" in exI)
      apply (auto simp: nth_append)
        apply (metis AT.att_base Suc_lessD fst_conv prod.sel(2) singletonD singletonI)
       apply (metis AT.att_base Suc_lessI b fst_conv prod.sel(2) singletonD)
      using tl_nempty_length2 by blast
  qed
qed

subsubsection "Lemma @{text ‹Compl_step3›}"
text ‹First, we need a few lemmas.›
lemma map_hd_lem[rule_format] : "n > 0 ⟶ (f 0 # map (λi. f i) [1..<n]) = map (λi. f i) [0..<n]"    
  by (simp add : hd_map upt_rec)

lemma map_Suc_lem[rule_format] : "n > 0 ⟶ map (λ i:: nat. f i)[1..<n] =
                                  map (λ i:: nat. f(Suc i))[0..<(n - 1)]"
proof -
  have "(f 0 # map (λn. f (Suc n)) [0..<n - 1] = f 0 # map f [1..<n]) = (map (λn. f (Suc n)) [0..<n - 1] = map f [1..<n])"
    by blast
  then show ?thesis
    by (metis Suc_pred' map_hd_lem map_upt_Suc)
qed

lemma forall_ex_fun: "finite S ==> (∀ x ∈ S. (∃ y. P y x)) ⟶ (∃ f. ∀ x ∈ S. P (f x) x)"
proof (induction rule: finite.induct)
  case emptyI
  then show ?case 
    by simp
next
  case (insertI F x)
  then show ?case
  proof (clarify)
    assume d: "(∀x::'a∈insert x F. ∃y::'b. P y x)"
    have "(∀x::'a∈F. ∃y::'b. P y x)" 
      using d by blast
    then obtain f where f: "∀x::'a∈F. P (f x) x" 
      using insertI.IH by blast 
    from d obtain y where "P y x" by blast
    thus "(∃f::'a ==> 'b. ∀x::'a∈insert x F. P (f x) x)" using f 
      by (rule_tac x = "λ z. if z = x then y else f z" in exI, simp)
  qed
qed

primrec nodup :: "['a, 'a list] ==> bool"
  where 
    nodup_nil: "nodup a [] = True" |
    nodup_step: "nodup a (x # ls) = (if x = a then (a ∉ (set ls)) else nodup a ls)"

definition nodup_all:: "'a list ==> bool"
  where
    "nodup_all l ≡ ∀ x ∈ set l. nodup x l"

lemma nodup_all_lem[rule_format]: 
  "nodup_all (x1 # a # l) ⟶ (insert x1 (insert a (set l)) - {x1}) = insert a (set l)"
  by (induction l, (simp add: nodup_all_def)+)

lemma nodup_all_tl[rule_format]: "nodup_all (x # l) ⟶ nodup_all l"  
  by (induction l, (simp add: nodup_all_def)+)

lemma finite_nodup: "finite I ==> ∃ l. set l = I ∧ nodup_all l"
proof (induction rule: finite.induct)
  case emptyI
  then show ?case
    by (simp add: nodup_all_def)
next
  case (insertI A a)
  then show ?case
    by (metis insertE insert_absorb list.simps(15) nodup_all_def nodup_step)
qed

lemma Compl_step3: "I ≠ {} ==> finite I ==>
     ( ∀ x ∈ I. x ∈ s ∨ (∃ (sl :: ((('s :: state) set)list)).
                  (sl ≠ []) ∧ (tl sl ≠ []) ∧
                 (sl ! 0, sl ! (length sl - 1)) = ({x},s) ∧
                 (∀ i < (length sl - 1). ⊨ N_{sl ! i,sl ! (i+1) )}
                         )) ==>
     (∃ lI. set lI = {x :: 's :: state. x ∈ I ∧ x ∉ s} ∧ (∃ Sj :: ((('s :: state) set)list) list.
               length Sj = length lI ∧ nodup_all lI ∧
            (∀ j < length Sj. (((Sj ! j) ≠ []) ∧ (tl (Sj ! j) ≠ []) ∧
                 ((Sj ! j) ! 0, (Sj ! j) ! (length (Sj ! j) - 1)) = ({lI ! j},s) ∧
                 (∀ i < (length (Sj ! j) - 1). ⊨ N_{(Sj ! j) ! i, (Sj ! j) ! (i+1) )}
                         ))))))"  
proof -
  assume i: "I ≠ {}" and f: "finite I" and
      fa: "∀x::'s∈I.
       x ∈ s ∨
       (∃sl::'s set list.
           sl ≠ [] ∧
           tl sl ≠ [] ∧
           (sl ! (0), sl ! (length sl - (1))) = ({x}, s) ∧
           (∀i<length sl - (1). ⊨N_{sl ! i, sl ! (i + (1)))}))"
  have a: "∃ lI. set lI = {x::'s ∈ I. x ∉ s} ∧ nodup_all lI"
    by (simp add: f finite_nodup)
  from this obtain lI where b: "set lI = {x::'s ∈ I. x ∉ s} ∧ nodup_all lI"
    by (erule exE)
  thus "∃lI::'s list.
       set lI = {x::'s ∈ I. x ∉ s} ∧
       (∃Sj::'s set list list.
           length Sj = length lI ∧
           nodup_all lI ∧
           (∀j<length Sj.
               Sj ! j ≠ [] ∧
               tl (Sj ! j) ≠ [] ∧
               (Sj ! j ! (0), Sj ! j ! (length (Sj ! j) - (1))) = ({lI ! j}, s) ∧
               (∀i<length (Sj ! j) - (1). ⊨N_{Sj ! j ! i, Sj ! j ! (i + (1)))})))"
    apply (rule_tac x = lI in exI)
    apply (rule conjI)
     apply (erule conjE, assumption)
  proof -
    have c:  "∀ x ∈ set(lI). (∃ sl::'s set list.
              sl ≠ [] ∧
              tl sl ≠ [] ∧
              (sl ! (0), sl ! (length sl - (1))) = ({x}, s) ∧
              (∀i<length sl - (1). ⊨N_{sl ! i, sl ! (i + (1)))}))"
      using b fa by fastforce
    thus "∃Sj::'s set list list.
       length Sj = length lI ∧
       nodup_all lI ∧
       (∀j<length Sj.
           Sj ! j ≠ [] ∧
           tl (Sj ! j) ≠ [] ∧
           (Sj ! j ! (0), Sj ! j ! (length (Sj ! j) - (1))) = ({lI ! j}, s) ∧
           (∀i<length (Sj ! j) - (1). ⊨N_{Sj ! j ! i, Sj ! j ! (i + (1)))}))"
      apply (subgoal_tac "finite (set lI)")
       apply (rotate_tac -1)
       apply (drule forall_ex_fun)
       apply (drule mp)
        apply assumption
       apply (erule exE)
       apply (rule_tac x = "[f (lI ! j). j ← [0..<(length lI)]]" in exI)
       apply simp
       apply (insert b)
       apply (erule conjE, assumption)
      apply (rule_tac A = "set lI" and B = I in finite_subset)
       apply blast
      by (rule f)
  qed
qed

subsubsection ‹Lemma @{text ‹Compl_step4›}›
text ‹Again, we need some additional lemmas first.›
lemma list_one_tl_empty[rule_format]: "length l = Suc (0 :: nat) ⟶ tl l = []"
  by (induction l, simp+)

lemma list_two_tl_not_empty[rule_format]: "∀ list. length l = Suc (Suc (length list)) ⟶ tl l ≠ []"  
  by (induction l, simp+, force)

lemma or_empty: "⊨([] ⊕_\<or>^{{}, s)})" by (simp add: att_or)

text ‹Note, this is not valid for any l, i.e., @{text ‹⊨ l ⊕_\∨^{{}, s)}›} is not a theorem.›
lemma list_or_upt[rule_format]:
 "∀ l . lI ≠ [] ⟶ length l = length lI ⟶ nodup_all lI ⟶
  (∀ i < length lI. (⊨ (l ! i)) ∧ (attack (l ! i) = ({lI ! i}, s)))
                ⟶ ( ⊨ (l ⊕_\<or>^{set lI, s)}))"     
proof (induction lI, simp, clarify)
  fix x1 x2 l
  show "∀l::'a attree list.
          x2 ≠ [] ⟶
          length l = length x2 ⟶
          nodup_all x2 ⟶
          (∀i<length x2. ⊨(l ! i) ∧ attack (l ! i) = ({x2 ! i}, s)) ⟶ ⊨(l ⊕_\<or>^{set x2, s)}) ==>
       x1 # x2 ≠ [] ==>
       length l = length (x1 # x2) ==>
       nodup_all (x1 # x2) ==>
       ∀i<length (x1 # x2). ⊨(l ! i) ∧ attack (l ! i) = ({(x1 # x2) ! i}, s) ==> ⊨(l ⊕_\<or>^{set (x1 # x2), s)})"
    apply (case_tac x2, simp, subst att_or, case_tac l, simp+)
    text ‹Case @{text ‹∀i<Suc (Suc (length list)). ⊨l ! i ∧ attack (l ! i) = ({(x1 # a # list) ! i}, s) ==>
 x2 = a # list ==> ⊨l ⊕_\∨^{insert x1 (insert a (set list)), s)}›}›
    apply (subst att_or, case_tac l, simp, clarify, simp, rename_tac lista, case_tac lista, simp+)
    text ‹Remaining conjunct of three conditions: @{text ‹ ⊨aa ∧
 fst (attack aa) ⊆ insert x1 (insert a (set list)) ∧
 snd (attack aa) ⊆ s ∧ ⊨ab # listb ⊕_\∨^{insert x1 (insert a (set list)) - fst (attack aa), s)}›}›
    apply (rule conjI)
    text ‹First condition @{text ‹ ⊨aa›}›
     apply (drule_tac x = 0 in spec, drule mp, simp, (erule conjE)+, simp, rule conjI)
    text ‹Second condition @{text ‹fst (attack aa) ⊆ insert x1 (insert a (set list))›}›
     apply (drule_tac x = 0 in spec, drule mp, simp, erule conjE, simp)
    text ‹The remaining conditions

 @{text ‹snd (attack aa) ⊆ s ∧ ⊨ab # listb ⊕_\∨^{insert x1 (insert a (set list)) - fst (attack aa), s)}›}
 
 are solved automatically!›
    by (metis Suc_mono add.right_neutral add_Suc_right list.size(4) nodup_all_lem nodup_all_tl nth_Cons_0 nth_Cons_Suc order_refl prod.sel(1) prod.sel(2) zero_less_Suc)
qed

lemma app_tl_empty_hd[rule_format]: "tl (l @ [a]) = [] ⟶ hd (l @ [a]) = a"
  by (induction l) auto
       
lemma tl_hd_empty[rule_format]: "tl (l @ [a]) = [] ⟶ l = []"
  by (induction l) auto

lemma tl_hd_not_empty[rule_format]: "tl (l @ [a]) ≠ [] ⟶ l ≠ []"
  by (induction l) auto
  
lemma app_tl_empty_length[rule_format]: "tl (map f [0..<length l] @ [a]) = []
                                        ==> l = []"
  by (drule tl_hd_empty, simp)

lemma not_empty_hd_fst[rule_format]: "l ≠ [] ⟶ hd(l @ [a]) = l ! 0"
  by (induction l) auto
  
lemma app_tl_hd_list[rule_format]: "tl (map f [0..<length l] @ [a]) ≠ []
                             ==> hd(map f [0..<length l] @ [a]) = (map f [0..<length l]) ! 0"
  by (drule tl_hd_not_empty, erule not_empty_hd_fst)

lemma tl_app_in[rule_format]: "l ≠ [] ⟶
   map f [0..<(length l - (Suc 0:: nat))] @ [f(length l - (Suc 0 :: nat))] = map f [0..<length l]"    
  by (induction l) auto

lemma map_fst[rule_format]: "n > 0 ⟶ map f [0..<n] = f 0 # (map f [1..<n])"
  by (induction n) auto

lemma step_lem[rule_format]:  "l ≠ [] ==>
       tl (map (λ i. f((x1 # a # l) ! i)((a # l) ! i)) [0..<length l]) =
       map (λi. f((a # l) ! i)(l ! i)) [0..<length l - (1)]"
proof (simp)
  assume l: "l ≠ []"
    have a: "map (λi. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l] =
                 (f(x1)(a) # (map (λi. f ((a # l) ! i) (l ! i)) [0..<(length l - 1)]))"
    proof -
      have b : "map (λi. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l] =
                     f ((x1 # a # l) ! 0) ((a # l) ! 0) #
                     (map (λi. f ((x1 # a # l) ! i) ((a # l) ! i)) [1..<length l])"
        by (rule map_fst, simp, rule l)
      have c: "map (λi. f ((x1 # a # l) ! i) ((a # l) ! i)) [Suc (0)..<length l] =
                map (λi. f ((x1 # a # l) ! Suc i) ((a # l) ! Suc i)) [(0)..<(length l - 1)]"
        by (subgoal_tac "[Suc (0)..<length l] = map Suc [0..<(length l - 1)]", 
             simp, simp add: map_Suc_upt l)
      thus "map (λi. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l] =
             f x1 a # map (λi. f ((a # l) ! i) (l ! i)) [0..<length l - (1)]"
         by (simp add: b c)
    qed
    thus "l ≠ [] ==>
    tl (map (λi. f ((x1 # a # l) ! i) ((a # l) ! i)) [0..<length l]) =
    map (λi. f ((a # l) ! i) (l ! i)) [0..<length l - Suc (0)]" 
      by (subst a, simp)
  qed

lemma step_lem2a[rule_format]: "0 < length list ==> map (λi. N_{(x1 # a # list) ! i, (a # list) ! i)})
        [0..<length list] @
       [N_{(x1 # a # list) ! length list, (a # list) ! length list)}] =
       aa # listb ⟶ N_{(x1, a))} = aa"
  by (subst map_fst, assumption, simp)

lemma step_lem2b[rule_format]: "0 = length list ==> map (λi. N_{(x1 # a # list) ! i, (a # list) ! i)})
        [0..<length list] @
       [N_{(x1 # a # list) ! length list, (a # list) ! length list)}] =
       aa # listb ⟶ N_{(x1, a))} = aa"
by simp

lemma step_lem2: "map (λi. N_{(x1 # a # list) ! i, (a # list) ! i)})
        [0..<length list] @
       [N_{(x1 # a # list) ! length list, (a # list) ! length list)}] =
       aa # listb ==> N_{(x1, a))} = aa"
proof (case_tac "length list", rule step_lem2b, erule sym, assumption)
  show "∧nat.
       map (λi. N_{(x1 # a # list) ! i, (a # list) ! i)}) [0..<length list] @
       [N_{(x1 # a # list) ! length list, (a # list) ! length list)}] =
       aa # listb ==>
       length list = Suc nat ==> N_{x1, a)} = aa"
    by (rule_tac list = list in step_lem2a, simp)
qed

lemma base_list_and[rule_format]: "Sji ≠ [] ⟶ tl Sji ≠ [] ⟶
         (∀ li. Sji ! (0) = li ⟶
        Sji! (length (Sji) - 1) = s ⟶
       (∀i<length (Sji) - 1. ⊨N_{Sji ! i, Sji ! Suc i)}) ⟶
       ⊨ (map (λi. N_{Sji ! i, Sji ! Suc i)})
          [0..<length (Sji) - Suc (0)] ⊕_\<and>^{li, s)}))"
proof (induction Sji)
  case Nil
  then show ?case by simp
next
  case (Cons a Sji)
  then show ?case 
    apply (subst att_and, case_tac Sji, simp, simp)
    apply (rule impI)+
  proof -
    fix aa list
    show "list ≠ [] ⟶
       list ! (length list - Suc 0) = s ⟶
       (∀i<length list. ⊨N_{(aa # list) ! i, list ! i)}) ⟶
       ⊨(map (λi. N_{(aa # list) ! i, list ! i)}) [0..<length list] ⊕_\<and>^{aa, s)}) ==>
       Sji = aa # list ==>
       (aa # list) ! length list = s ==>
       ∀i<Suc (length list). ⊨N_{(a # aa # list) ! i, (aa # list) ! i)} ==>
       case map (λi. N_{(a # aa # list) ! i, (aa # list) ! i)}) [0..<length list] @
            [N_{(a # aa # list) ! length list, s)}] of
       [] ==> fst (a, s) ⊆ snd (a, s) | [aa] ==> ⊨aa ∧ attack aa = (a, s)
       | aa # ab # list ==>
           ⊨aa ∧ fst (attack aa) = fst (a, s) ∧ ⊨(ab # list ⊕_\<and>^{snd (attack aa), snd (a, s))})"
    proof (case_tac "map (λi. N_{(a # aa # list) ! i, (aa # list) ! i)}) [0..<length list] @
            [N_{(a # aa # list) ! length list, s)}]", simp, clarify, simp)
      fix ab lista
      have *: "tl (map (λi. N_{(a # aa # list) ! i, (aa # list) ! i)}) [0..<length list])
                    = (map (λi. N_{(aa # list) ! i, (list) ! i)}) [0..<(length list - 1)])"
        if "list ≠ []"
        apply (subgoal_tac "tl (map (λi. N_{(a # aa # list) ! i, (aa # list) ! i)}) [0..<length list])
                    = (map (λi. N_{(aa # list) ! i, (list) ! i)}) [0..<(length list - 1)])")
         apply blast
        apply (subst step_lem [OF that])
        apply simp
        done
      show "list ≠ [] ⟶
       (∀i<length list. ⊨N_{(aa # list) ! i, list ! i)}) ⟶
       ⊨(map (λi. N_{(aa # list) ! i, list ! i)})
          [0..<length list] ⊕_\<and>^{aa, list ! (length list - Suc 0))}) ==>
       Sji = aa # list ==>
       ∀i<Suc (length list). ⊨N_{(a # aa # list) ! i, (aa # list) ! i)} ==>
       map (λi. N_{(a # aa # list) ! i, (aa # list) ! i)}) [0..<length list] @
       [N_{(a # aa # list) ! length list, (aa # list) ! length list)}] =
       ab # lista ==>
       s = (aa # list) ! length list ==>
       case lista of [] ==> ⊨ab ∧ attack ab = (a, (aa # list) ! length list)
       | aba # lista ==>
           ⊨ab ∧ fst (attack ab) = a ∧ ⊨(aba # lista ⊕_\<and>^{snd (attack ab), (aa # list) ! length list)})"
        apply (auto simp: split: list.split)
           apply (metis (no_types, lifting) app_tl_hd_list length_greater_0_conv list.sel(1) list.sel(3) list.simps(3) list.simps(8) list.size(3) map_fst nth_Cons_0 self_append_conv2 upt_0 zero_less_Suc)
          apply (metis (no_types, lifting) app_tl_hd_list attack.simps(1) fst_conv length_greater_0_conv list.sel(1) list.sel(3) list.simps(3) list.simps(8) list.size(3) map_fst nth_Cons_0 self_append_conv2 upt_0)
         apply (metis (mono_tags, lifting) app_tl_hd_list attack.simps(1) fst_conv length_greater_0_conv list.sel(1) list.sel(3) list.simps(3) list.simps(8) list.size(3) map_fst nth_Cons_0 self_append_conv2 upt_0)
        by (smt * One_nat_def app_tl_hd_list attack.simps(1) length_greater_0_conv list.sel(1) list.sel(3) list.simps(3) list.simps(8) list.size(3) map_fst nth_Cons_0 nth_Cons_pos self_append_conv2 snd_conv tl_app_in tl_append2 upt_0)
    qed
  qed
qed

lemma Compl_step4: "I ≠ {} ==> finite I ==> ¬ I ⊆ s ==>
(∃ lI. set lI = {x. x ∈ I ∧ x ∉ s} ∧ (∃ Sj :: ((('s :: state) set)list) list.
               length Sj = length lI ∧ nodup_all lI ∧
            (∀ j < length Sj. (((Sj ! j) ≠ []) ∧ (tl (Sj ! j) ≠ []) ∧
                 ((Sj ! j) ! 0, (Sj ! j) ! (length (Sj ! j) - 1)) = ({lI ! j},s) ∧
                 (∀ i < (length (Sj ! j) - 1). ⊨ N_{(Sj ! j) ! i, (Sj ! j) ! (i+1) )}
                         )))))
 ==> ∃ (A :: ('s :: state) attree). ⊨ A ∧ attack A = (I,s)"
proof (erule exE, erule conjE, erule exE, erule conjE)
  fix lI Sj
  assume  a: "I ≠ {}" and b: "finite I" and c: "¬ I ⊆ s"
    and d: "set lI = {x::'s ∈ I. x ∉ s}" and e: "length Sj = length lI"
    and f: "nodup_all lI ∧
              (∀j<length Sj. Sj ! j ≠ [] ∧
                             tl (Sj ! j) ≠ [] ∧
           (Sj ! j ! (0), Sj ! j ! (length (Sj ! j) - (1))) = ({lI ! j}, s) ∧
           (∀i<length (Sj ! j) - (1). ⊨N_{Sj ! j ! i, Sj ! j ! (i + (1)))}))"
  show    "∃A::'s attree. ⊨A ∧ attack A = (I, s)"
    apply (rule_tac x = 
        "[([] ⊕_\<or>^{{x. x ∈ I ∧ x ∈ s}, s)}),
    ([[ N_{(Sj ! j) ! i, (Sj ! j) ! (i + (1)))}.
      i ← [0..<(length (Sj ! j)-(1))]] ⊕_\<and>^{({lI ! j},s))}. j ← [0..<(length Sj)]]
     ⊕_\<or>^{{x. x ∈ I ∧ x ∉ s},s)})] ⊕_\<or>^{I, s)}" in exI)
  proof 
    show  "⊨([[] ⊕_\<or>^{{x::'s ∈ I. x ∈ s}, s)},
       map (λj.
               ((map (λi. N_{Sj ! j ! i, Sj ! j ! (i + (1)))})
                [0..<length (Sj ! j) - (1)]) ⊕_\<and>^{{lI ! j}, s)}))
       [0..<length Sj] ⊕_\<or>^{{x::'s ∈ I. x ∉ s}, s)}] ⊕_\<or>^{I, s)})"
    proof -
      have g: "I - {x::'s ∈ I. x ∈ s} = {x::'s ∈ I. x ∉ s}" by blast
      thus "⊨([[] ⊕_\<or>^{{x::'s ∈ I. x ∈ s}, s)},
       (map (λj.
               ((map (λi. N_{Sj ! j ! i, Sj ! j ! (i + (1)))})
                [0..<length (Sj ! j) - (1)]) ⊕_\<and>^{{lI ! j}, s)}))
       [0..<length Sj]) ⊕_\<or>^{{x::'s ∈ I. x ∉ s}, s)}] ⊕_\<or>^{I, s)})"
        apply (subst att_or, simp)
      proof 
        show "I - {x ∈ I. x ∈ s} = {x ∈ I. x ∉ s} ==> ⊨([] ⊕_\<or>^{{x ∈ I. x ∈ s}, s)})"
          by (metis (no_types, lifting) CollectD att_or_empty_back subsetI)
      next show "I - {x ∈ I. x ∈ s} = {x ∈ I. x ∉ s} ==>
    ⊨([map (λj. ((map (λi. N_{Sj ! j ! i, Sj ! j ! Suc i)}) [0..<length (Sj ! j) - Suc 0]) ⊕_\<and>^{{lI ! j}, s)}))
        [0..<length Sj] ⊕_\<or>^{{x ∈ I. x ∉ s}, s)}] ⊕_\<or>^{{x ∈ I. x ∉ s}, s)})"
          text ‹Use lemma @{text ‹list_or_upt›} to distribute attack validity over list lI›
        proof (erule ssubst, subst att_or, simp, rule subst, rule d, rule_tac lI = lI in list_or_upt)
          show "lI ≠ []"
            using c d by auto 
        next show "∧i.
       i < length lI ==>
       ⊨(map (λj.
                 ((map (λi. N_{Sj ! j ! i, Sj ! j ! Suc i)})
                  [0..<length (Sj ! j) - Suc (0)]) ⊕_\<and>^{{lI ! j}, s)}))
          [0..<length Sj] !
         i) ∧
       (attack
        (map (λj.
                 ((map (λi. N_{Sj ! j ! i, Sj ! j ! Suc i)})
                  [0..<length (Sj ! j) - Suc (0)]) ⊕_\<and>^{{lI ! j}, s)}))
          [0..<length Sj] !
         i) =
       ({lI ! i}, s))"
          proof (simp add: a b c d e f)
            show "∧i.
                i < length lI ==>
                ⊨(map (λia. N_{Sj ! i ! ia, Sj ! i ! Suc ia)})
                [0..<length (Sj ! i) - Suc (0)] ⊕_\<and>^{{lI ! i}, s)})"
            proof -
              fix i :: nat
              assume a1: "i < length lI"
              have "∀n. ⊨map (λna. N_{Sj ! n ! na, Sj ! n ! Suc na)}) [0..< length (Sj ! n) - 1] ⊕_\<and>^{Sj ! n ! 0, Sj ! n ! (length (Sj ! n) - 1))} ∨ ¬ n < length Sj"
                by (metis (no_types) One_nat_def add.right_neutral add_Suc_right base_list_and f)
              then show "⊨map (λn. N_{Sj ! i ! n, Sj ! i ! Suc n)}) [0..< length (Sj ! i) - Suc 0] ⊕_\<and>^{{lI ! i}, s)}"
                using a1 by (metis (no_types) One_nat_def e f)
            qed
          qed
        qed (auto simp add: e f)
      qed
    qed
  qed auto
qed

subsubsection ‹Main Theorem Completeness›
theorem Completeness: "I ≠ {} ==> finite I ==>
Kripke {s :: ('s :: state). ∃ i ∈ I. (i →_i* s)} (I :: ('s :: state)set) ⊨ EF s
\<Longrightarrow> ∃ (A :: ('s :: state) attree). ⊨ A ∧ attack A = (I,s)"
proof (case_tac "I ⊆ s")
  show "I ≠ {} ==> finite I ==>
    Kripke {s::'s. ∃i::'s∈I. i →_i* s} I ⊨ EF s ==> I ⊆ s ==> ∃A::'s attree. ⊨A ∧ attack A = (I, s)"
    using att_or_empty_back attack.simps(3) by blast
next 
  show "I ≠ {} ==> finite I ==>
    Kripke {s::'s. ∃i::'s∈I. i →_i* s} I ⊨ EF s ==> ¬ I ⊆ s
   ==> ∃A::'s attree. ⊨A ∧ attack A = (I, s)"
    by (iprover intro: Compl_step1 Compl_step2 Compl_step3 Compl_step4 elim: )
qed

subsubsection ‹Contrapositions of Correctness and Completeness›   
lemma contrapos_compl: 
  "I ≠ {} ==> finite I ==>
  (¬ (∃ (A :: ('s :: state) attree). ⊨ A ∧ attack A = (I, - s))) ==>
\<not> (Kripke {s. ∃i∈I. i →_i* s} I ⊨ EF (- s))"
  using Completeness by auto

lemma contrapos_corr:   
"(¬(Kripke {s :: ('s :: state). ∃ i ∈ I. (i →_i* s)} I ⊨ EF s))
\<Longrightarrow> attack A = (I,s)
\<Longrightarrow> ¬ (⊨ A)"
  using AT_EF by blast

end