# Theory AT

section "Attack Trees"
theory AT
imports MC
begin

text ‹Attack Trees are an intuitive and practical formal method to analyse and quantify
attacks on security and privacy. They are very useful to identify the steps an attacker
takes through a system when approaching the attack goal. Here, we provide
a proof calculus to analyse concrete attacks using a notion of attack validity.
We define a state based semantics with Kripke models and the temporal logic
CTL 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
with respect to the model.›

subsection "Attack Tree datatype"
text ‹The following datatype definition @{text ‹attree›} defines attack trees.
The simplest case of an attack tree is a base attack.
The principal idea is that base attacks are defined by a pair of
state sets representing the initial states and the {\it attack property}
-- a set of states characterized by the fact that this property holds
in them.
Attacks can also be combined as the conjunction or disjunction of other attacks.
The operator @{text ‹⊕⇩∨›} creates or-trees and @{text ‹⊕⇩∧›} creates and-trees.
And-attack trees @{text ‹l ⊕⇩∧ s›} and or-attack trees @{text ‹l ⊕⇩∨ s›}
combine lists of attack trees $l$ either conjunctively or disjunctively and
consist of a list of sub-attacks -- again attack trees.›
datatype ('s :: state) attree = BaseAttack "('s set) * ('s set)" ("𝒩⇘(_)⇙") |
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
by an attack goal, by breaking it down into a series of sub-attacks. This
proceeding corresponds to a process of {\it refinement}. Therefore, as part of
the attack tree calculus, we provide a notion of attack tree refinement.

The relation @{text ‹refines_to›} "constructs" the attack tree. Here the above
defined attack vectors are used to define how nodes in an attack tree
can be expanded into more detailed (refined) attack sequences. This
process of refinement @{text "⊑"} allows to eventually reach a fully detailed
attack that can then be proved using @{text "⊢"}.›
inductive refines_to :: "[('s :: state) attree, 's attree] ⇒ bool" ("_ ⊑ _" [40] 40)
where
refI: "⟦  A = ((l @ [ 𝒩⇘(si',si'')⇙] @ l'')⊕⇩∧⇗(si,si''')⇖ );
A' = (l' ⊕⇩∧⇗(si',si'')⇖);
A'' = (l @ l' @ l'' ⊕⇩∧⇗(si,si''')⇖)
⟧ ⟹ A ⊑ A''"|
ref_or: "⟦ as ≠ []; ∀ A' ∈ set(as). (A  ⊑ A') ∧ attack A = s ⟧ ⟹ A ⊑ (as ⊕⇩∨⇗s⇖)" |
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
attacks that are feasible in a model. The general model we provide is
a Kripke structure, i.e., a set of states and a generic state transition.
Thus, feasible steps in the model are single steps of the state transition.
We call them valid base attacks.
The composition of sequences of valid base attacks into and-attacks yields
again valid attacks if the base attacks line up with respect to the states
in the state transition. If there are different valid attacks for the same
attack goal starting from the same initial state set, these can be
summarized in an or-attack.
More precisely, the different cases of the validity predicate are distinguished
by pattern matching over the attack tree structure.
\begin{itemize}
\item A  base attack @{text ‹𝒩(s0,s1)›} is  valid if from all
states in the pre-state set @{text ‹s0›} we can get with a single step of the
state transition relation to a state in the post-state set ‹s1›. Note,
that it is sufficient for a post-state to exist for each pre-state. After all,
we are aiming to validate attacks, that is, possible attack paths to some
state 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}
The proof calculus is thus completely described by one recursive function. ›
fun is_attack_tree :: "[('s :: state) attree] ⇒ bool"  ("⊢_" [40] 40)
where
att_base:  "(⊢ 𝒩⇘s⇙) = ( (∀ x ∈ (fst s). (∃ y ∈ (snd s). x  →⇩i y )))" |
att_and: "(⊢(As ⊕⇩∧⇗s⇖)) =
(case As of
[] ⇒ (fst s ⊆ snd s)
| [a] ⇒ ( ⊢ a ∧ attack a = s)
| (a # l) ⇒ (( ⊢ a) ∧ (fst(attack a) = fst s) ∧
(⊢(l ⊕⇩∧⇗(snd(attack a),snd(s))⇖))))" |
att_or: "(⊢(As ⊕⇩∨⇗s⇖)) =
(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 ⊕⇩∨⇗(fst s - fst(attack a), snd s)⇖))))"
text ‹Since the definition is constructive, code can be generated directly from it, here
into 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] ⊕⇩∧⇗s⇖)"
proof -
show " ⊢([a] ⊕⇩∧⇗s⇖)" 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] : " ⊢([] ⊕⇩∧⇗(s', s'')⇖) ⟶ s' ⊆ s''"

lemma att_and_empty2: " ⊢([] ⊕⇩∧⇗(s, s)⇖)"

lemma att_or_empty[rule_format] : " ⊢([] ⊕⇩∨⇗(s', s'')⇖) ⟶ s' ⊆ s''"

lemma att_or_empty_back[rule_format]: " s' ⊆ s'' ⟶  ⊢([] ⊕⇩∨⇗(s', s'')⇖)"

lemma att_or_empty_rev: assumes "⊢(l ⊕⇩∨⇗(s, s')⇖)" and "¬(s ⊆ s')" shows "l ≠ []"
using assms att_or_empty by blast

lemma att_or_empty2: "⊢([] ⊕⇩∨⇗(s, s)⇖)"

lemma att_andD1: " ⊢(x1 # x2 ⊕⇩∧⇗s⇖) ⟹ ⊢ 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 ⊕⇩∧⇗s⇖) ⟶ ⊢ (x2 ⊕⇩∧⇗(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 ⊕⇩∧⇗s⇖) ⟹ ⊢ (x2 ⊕⇩∧⇗(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 ⊕⇩∧⇗x⇖) ⟶ xa ∈ fst (attack (x1 # x2a ⊕⇩∧⇗x⇖))
⟶ xa ∈ fst (attack x1)"
by (induction x2a, (subst att_and, simp)+)

lemma att_orD1: " ⊢(x1 # x2 ⊕⇩∨⇗x⇖) ⟹ ⊢ x1"
by (case_tac x2, (subst (asm) att_or, simp)+)

lemma att_or_snd_hd: " ⊢(a # list ⊕⇩∨⇗(aa, b)⇖) ⟹ snd(attack a) ⊆ b"
by (case_tac list,  (subst (asm) att_or, simp)+)

lemma att_or_singleton[rule_format]:
" ⊢([x1] ⊕⇩∨⇗x⇖) ⟶ ⊢([] ⊕⇩∨⇗(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 ⊕⇩∨⇗x⇖) ⟶  ⊢ (x2 ⊕⇩∨⇗(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 ⊕⇩∨⇗x⇖) ⟶ (∀ 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] ⊕⇩∨⇗x⇖)  ⟹ fst x ⊆ fst(attack x1)"
by (subst (asm) att_or, simp)+

lemma or_att_fst_sup0[rule_format]: "x2 ≠ [] ⟶ (∀ x. (⊢ ((x2 ⊕⇩∨⇗x⇖):: ('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 ⊕⇩∨⇗x⇖):: ('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.
⊢([] ⊕⇩∧⇗x⇖) ⟶
(∀xa::'a∈fst (attack ([] ⊕⇩∧⇗x⇖)). ∃y::'a. y ∈ snd (attack ([] ⊕⇩∧⇗x⇖)) ∧ 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 ⊕⇩∧⇗x⇖)) ⟶
((∀xa::'a∈fst (attack (x2a ⊕⇩∧⇗x⇖)). ∃y::'a. y ∈ snd (attack (x2a ⊕⇩∧⇗x⇖)) ∧ 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 ⊕⇩∧⇗x⇖)) ⟶
(∀xa::'a∈fst (attack (x1 # x2a ⊕⇩∧⇗x⇖)).
(∃y::'a. y ∈ snd (attack (x1 # x2a ⊕⇩∧⇗x⇖)) ∧ (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 ⊕⇩∧⇗x⇖) ⟶
(∀xa::'a∈fst (attack (x2a ⊕⇩∧⇗x⇖)).
∃y::'a. y ∈ snd (attack (x2a ⊕⇩∧⇗x⇖)) ∧ 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 ⊕⇩∧⇗x⇖) ⟹
∀x::'a set × 'a set.
⊢(x2a ⊕⇩∧⇗x⇖) ⟶
(∀xa::'a∈fst (attack (x2a ⊕⇩∧⇗x⇖)). ∃y::'a. y ∈ snd (attack (x2a ⊕⇩∧⇗x⇖)) ∧ xa →⇩i* y) ⟹
∀xa::'a∈fst (attack (x1 # x2a ⊕⇩∧⇗x⇖)). ∃y::'a. y ∈ snd (attack (x1 # x2a ⊕⇩∧⇗x⇖)) ∧ 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
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))"

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›}.

First, we proof a number of lemmas needed for both directions before we
show 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"

lemma nth_app_eq1_rev:   "i < length sla ⟹  sla ! i = (sla @ sl) ! i"

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

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 ⊕⇩∧⇗x⇖))"
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 ⊕⇩∧⇗x⇖)) = snd (attack (x2a ⊕⇩∧⇗(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 ⟹ ⊢ 𝒩⇘(y1, y)⇙ ⟹⊢ 𝒩⇘(y0, y)⇙"

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 @ [𝒩⇘(si', si'')⇙] @ l'' ⊕⇩∧⇗(si, si''')⇖) ⟹
A' = (l' ⊕⇩∧⇗(si', si'')⇖) ⟹ A'' = (l @ l' @ l'' ⊕⇩∧⇗(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 ⊕⇩∨⇗s⇖)"
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  "⊢𝒩⇘(x, xa)⇙ ⟹ ⊢𝒩⇘(x, xc)⇙"
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
lemma @{text ‹att_elem_seq0›}.

There 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"
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)›}.

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

subsubsection "Lemma @{text ‹Compl_step1›}"
lemma Compl_step1:
"Kripke {s :: ('s :: state). ∃ i ∈ I. (i →⇩i* s)} I  ⊢ EF s
⟹ ∀ x ∈ I. ∃ y ∈ s. x →⇩i* y"

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).  ⊢ 𝒩⇘(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). ⊢𝒩⇘(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). ⊢𝒩⇘(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
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).  ⊢ 𝒩⇘(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).  ⊢ 𝒩⇘((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). ⊢𝒩⇘(sl ! i, sl ! (i + (1)))⇙))"
have a: "∃ lI. set lI = {x::'s ∈ I. x ∉ s} ∧ nodup_all lI"
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). ⊢𝒩⇘(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). ⊢𝒩⇘(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). ⊢𝒩⇘(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: "⊢([] ⊕⇩∨⇗({}, 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 ⊕⇩∨⇗(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 ⊕⇩∨⇗(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 ⊕⇩∨⇗(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)]",
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)]"
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. 𝒩⇘((x1 # a # list) ! i, (a # list) ! i)⇙)
[0..<length list] @
[𝒩⇘((x1 # a # list) ! length list, (a # list) ! length list)⇙] =
aa # listb ⟶ 𝒩⇘((x1, a))⇙ = aa"
by (subst map_fst, assumption, simp)

lemma step_lem2b[rule_format]: "0 = length list ⟹ map (λi. 𝒩⇘((x1 # a # list) ! i, (a # list) ! i)⇙)
[0..<length list] @
[𝒩⇘((x1 # a # list) ! length list, (a # list) ! length list)⇙] =
aa # listb ⟶ 𝒩⇘((x1, a))⇙ = aa"
by simp

lemma step_lem2: "map (λi. 𝒩⇘((x1 # a # list) ! i, (a # list) ! i)⇙)
[0..<length list] @
[𝒩⇘((x1 # a # list) ! length list, (a # list) ! length list)⇙] =
aa # listb ⟹ 𝒩⇘((x1, a))⇙ = aa"
proof (case_tac "length list", rule step_lem2b, erule sym, assumption)
show "⋀nat.
map (λi. 𝒩⇘((x1 # a # list) ! i, (a # list) ! i)⇙) [0..<length list] @
[𝒩⇘((x1 # a # list) ! length list, (a # list) ! length list)⇙] =
aa # listb ⟹
length list = Suc nat ⟹ 𝒩⇘(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. ⊢𝒩⇘(Sji ! i, Sji ! Suc i)⇙) ⟶
⊢ (map (λi. 𝒩⇘(Sji ! i, Sji ! Suc i)⇙)
[0..<length (Sji) - Suc (0)] ⊕⇩∧⇗(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. ⊢𝒩⇘((aa # list) ! i, list ! i)⇙) ⟶
⊢(map (λi. 𝒩⇘((aa # list) ! i, list ! i)⇙) [0..<length list] ⊕⇩∧⇗(aa, s)⇖) ⟹
Sji = aa # list ⟹
(aa # list) ! length list = s ⟹
∀i<Suc (length list). ⊢𝒩⇘((a # aa # list) ! i, (aa # list) ! i)⇙ ⟹
case map (λi. 𝒩⇘((a # aa # list) ! i, (aa # list) ! i)⇙) [0..<length list] @
[𝒩⇘((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 ⊕⇩∧⇗(snd (attack aa), snd (a, s))⇖)"
proof (case_tac "map (λi. 𝒩⇘((a # aa # list) ! i, (aa # list) ! i)⇙) [0..<length list] @
[𝒩⇘((a # aa # list) ! length list, s)⇙]", simp, clarify, simp)
fix ab lista
have *: "tl (map (λi. 𝒩⇘((a # aa # list) ! i, (aa # list) ! i)⇙) [0..<length list])
=  (map (λi. 𝒩⇘((aa # list) ! i, (list) ! i)⇙) [0..<(length list - 1)])"
if "list ≠ []"
apply (subgoal_tac "tl (map (λi. 𝒩⇘((a # aa # list) ! i, (aa # list) ! i)⇙) [0..<length list])
=  (map (λi. 𝒩⇘((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. ⊢𝒩⇘((aa # list) ! i, list ! i)⇙) ⟶
⊢(map (λi. 𝒩⇘((aa # list) ! i, list ! i)⇙)
[0..<length list] ⊕⇩∧⇗(aa, list ! (length list - Suc 0))⇖) ⟹
Sji = aa # list ⟹
∀i<Suc (length list). ⊢𝒩⇘((a # aa # list) ! i, (aa # list) ! i)⇙ ⟹
map (λi. 𝒩⇘((a # aa # list) ! i, (aa # list) ! i)⇙) [0..<length list] @
[𝒩⇘((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 ⊕⇩∧⇗(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).  ⊢ 𝒩⇘((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). ⊢𝒩⇘(Sj ! j ! i, Sj ! j ! (i + (1)))⇙))"
show    "∃A::'s attree. ⊢A ∧ attack A = (I, s)"
apply (rule_tac x =
"[([] ⊕⇩∨⇗({x. x ∈ I ∧ x ∈ s}, s)⇖),
([[ 𝒩⇘((Sj ! j) ! i, (Sj ! j) ! (i + (1)))⇙.
i ← [0..<(length (Sj ! j)-(1))]] ⊕⇩∧⇗(({lI ! j},s))⇖. j ← [0..<(length Sj)]]
⊕⇩∨⇗({x. x ∈ I ∧ x ∉ s},s)⇖)] ⊕⇩∨⇗(I, s)⇖" in exI)
proof
show  "⊢([[] ⊕⇩∨⇗({x::'s ∈ I. x ∈ s}, s)⇖,
map (λj.
((map (λi. 𝒩⇘(Sj ! j ! i, Sj ! j ! (i + (1)))⇙)
[0..<length (Sj ! j) - (1)]) ⊕⇩∧⇗({lI ! j}, s)⇖))
[0..<length Sj] ⊕⇩∨⇗({x::'s ∈ I. x ∉ s}, s)⇖] ⊕⇩∨⇗(I, s)⇖)"
proof -
have g: "I - {x::'s ∈ I. x ∈ s} = {x::'s ∈ I. x ∉ s}" by blast
thus "⊢([[] ⊕⇩∨⇗({x::'s ∈ I. x ∈ s}, s)⇖,
(map (λj.
((map (λi. 𝒩⇘(Sj ! j ! i, Sj ! j ! (i + (1)))⇙)
[0..<length (Sj ! j) - (1)]) ⊕⇩∧⇗({lI ! j}, s)⇖))
[0..<length Sj]) ⊕⇩∨⇗({x::'s ∈ I. x ∉ s}, s)⇖] ⊕⇩∨⇗(I, s)⇖)"
apply (subst att_or, simp)
proof
show "I - {x ∈ I. x ∈ s} = {x ∈ I. x ∉ s} ⟹ ⊢([] ⊕⇩∨⇗({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. 𝒩⇘(Sj ! j ! i, Sj ! j ! Suc i)⇙) [0..<length (Sj ! j) - Suc 0]) ⊕⇩∧⇗({lI ! j}, s)⇖))
[0..<length Sj] ⊕⇩∨⇗({x ∈ I. x ∉ s}, s)⇖] ⊕⇩∨⇗({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. 𝒩⇘(Sj ! j ! i, Sj ! j ! Suc i)⇙)
[0..<length (Sj ! j) - Suc (0)]) ⊕⇩∧⇗({lI ! j}, s)⇖))
[0..<length Sj] !
i) ∧
(attack
(map (λj.
((map (λi. 𝒩⇘(Sj ! j ! i, Sj ! j ! Suc i)⇙)
[0..<length (Sj ! j) - Suc (0)]) ⊕⇩∧⇗({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. 𝒩⇘(Sj ! i ! ia, Sj ! i ! Suc ia)⇙)
[0..<length (Sj ! i) - Suc (0)] ⊕⇩∧⇗({lI ! i}, s)⇖)"
proof -
fix i :: nat
assume a1: "i < length lI"
have "∀n. ⊢map (λna. 𝒩⇘(Sj ! n ! na, Sj ! n ! Suc na)⇙) [0..< length (Sj ! n) - 1] ⊕⇩∧⇗(Sj ! n ! 0, Sj ! n ! (length (Sj ! n) - 1))⇖ ∨ ¬ n < length Sj"
then show "⊢map (λn. 𝒩⇘(Sj ! i ! n, Sj ! i ! Suc n)⇙) [0..< length (Sj ! i) - Suc 0] ⊕⇩∧⇗({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
⟹ ∃ (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))) ⟹
¬ (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))
⟹ attack A = (I,s)
⟹ ¬ (⊢ A)"
using AT_EF by blast

end