# Theory Configuration_Traces

(*
Title:      Configuration_Traces.thy
Author:     Diego Marmsoler
*)
section "A Theory of Dynamic Architectures"
text ‹
The following theory formalizes configuration traces~\<^cite>‹"Marmsoler2016a" and "Marmsoler2016"› as a model for dynamic architectures.
Since configuration traces may be finite as well as infinite, the theory depends on Lochbihler's theory of co-inductive lists~\<^cite>‹"Lochbihler2010"›.
›
theory Configuration_Traces
imports Coinductive.Coinductive_List
begin
text ‹
In the following we first provide some preliminary results for natural numbers, extended natural numbers, and lazy lists.
Then, we introduce a locale @text{dynamic\_architectures} which introduces basic definitions and corresponding properties for dynamic architectures.
›

subsection "Natural Numbers"
text ‹
We provide one additional property for natural numbers.
›
lemma boundedGreatest:
assumes "P (i::nat)"
and "∀n' > n. ¬ P n'"
shows "∃i'≤n. P i' ∧ (∀n'. P n' ⟶ n'≤i')"
proof -
have "P (i::nat) ⟹ n≥i ⟹ ∀n' > n. ¬ P n' ⟹ (∃i'≤n. P i' ∧ (∀n'≤n. P n' ⟶ n'≤i'))"
proof (induction n)
case 0
then show ?case by auto
next
case (Suc n)
then show ?case
proof cases
assume "i = Suc n"
then show ?thesis using Suc.prems by auto
next
assume "¬(i = Suc n)"
thus ?thesis
proof cases
assume "P (Suc n)"
thus ?thesis by auto
next
assume "¬ P (Suc n)"
with Suc.prems have "∀n' > n. ¬ P n'" using Suc_lessI by blast
moreover from ‹¬(i = Suc n)› have "i ≤ n" and "P i" using Suc.prems by auto
ultimately obtain i' where "i'≤n ∧ P i' ∧ (∀n'≤n. P n' ⟶ n' ≤ i')" using Suc.IH by blast
hence "i' ≤ n" and "P i'" and "(∀n'≤n. P n' ⟶ n' ≤ i')" by auto
thus ?thesis by (metis le_SucI le_Suc_eq)
qed
qed
qed
moreover have "n≥i"
proof (rule ccontr)
assume "¬ (n ≥ i)"
hence "n < i" by arith
thus False using assms by blast
qed
ultimately obtain i' where "i'≤n" and "P i'" and "∀n'≤n. P n' ⟶ n' ≤ i'" using assms by blast
with assms have "∀n'. P n' ⟶ n' ≤ i'" using not_le_imp_less by blast
with ‹i' ≤ n› and ‹P i'› show ?thesis by auto
qed

subsection "Extended Natural Numbers"
text ‹
We provide one simple property for the \emph{strict} order over extended natural numbers.
›
lemma enat_min:
assumes "m ≥ enat n'"
and "enat n < m - enat n'"
shows "enat n + enat n' < m"

subsection "Lazy Lists"
text ‹
In the following we provide some additional notation and properties for lazy lists.
›
notation LNil ("[]⇩l")
notation LCons (infixl "#⇩l" 60)
notation lappend (infixl "@⇩l" 60)

lemma lnth_lappend[simp]:
assumes "lfinite xs"
and "¬ lnull ys"
shows "lnth (xs @⇩l ys) (the_enat (llength xs)) = lhd ys"
proof -
from assms have "∃k. llength xs = enat k" using lfinite_conv_llength_enat by auto
then obtain k where "llength xs = enat k" by blast
hence "lnth (xs @⇩l ys) (the_enat (llength xs)) = lnth ys 0"
using lnth_lappend2[of xs k k ys] by simp
with assms show ?thesis using lnth_0_conv_lhd by simp
qed

lemma lfilter_ltake:
assumes "∀(n::nat)≤llength xs. n≥i ⟶ (¬ P (lnth xs n))"
shows "lfilter P xs = lfilter P (ltake i xs)"
proof -
have "lfilter P xs = lfilter P ((ltake i xs) @⇩l (ldrop i xs))"
using lappend_ltake_ldrop[of "(enat i)" xs] by simp
hence "lfilter P xs = (lfilter P ((ltake i) xs)) @⇩l (lfilter P (ldrop i xs))" by simp
show ?thesis
proof cases
assume "enat i ≤ llength xs"

have "∀x<llength (ldrop i xs). ¬ P (lnth (ldrop i xs) x)"
proof (rule allI)
fix x show "enat x < llength (ldrop (enat i) xs) ⟶ ¬ P (lnth (ldrop (enat i) xs) x)"
proof
assume "enat x < llength (ldrop (enat i) xs)"
moreover have "llength (ldrop (enat i) xs) = llength xs - enat i"
using llength_ldrop[of "enat i"] by simp
ultimately have "enat x < llength xs - enat i" by simp
with ‹enat i ≤ llength xs› have "enat x + enat i < llength xs"
using enat_min[of i "llength xs" x] by simp
moreover have "enat i + enat x = enat x + enat i" by simp
ultimately have "enat i + enat x < llength xs" by arith
hence "i + x < llength xs" by simp
hence "lnth (ldrop i xs) x = lnth xs (x + the_enat i)" using lnth_ldrop[of "enat i" "x" xs] by simp
moreover have "x + i ≥ i" by simp
with assms ‹i + x < llength xs› have "¬ P (lnth xs (x + the_enat i))"
ultimately show "¬ P (lnth (ldrop i xs) x)" using assms by simp
qed
qed
hence "lfilter P (ldrop i xs) = []⇩l" by (metis diverge_lfilter_LNil in_lset_conv_lnth)
with ‹lfilter P xs = (lfilter P ((ltake i) xs)) @⇩l (lfilter P (ldrop i xs))›
show "lfilter P xs = lfilter P (ltake i xs)" by simp
next
assume "¬ enat i ≤ llength xs"
hence "enat i > llength xs" by simp
hence "ldrop i xs = []⇩l" by simp
hence "lfilter P (ldrop i xs) = []⇩l" using lfilter_LNil[of P] by arith
with ‹lfilter P xs = (lfilter P ((ltake i) xs)) @⇩l (lfilter P (ldrop i xs))›
show "lfilter P xs = lfilter P (ltake i xs)" by simp
qed
qed

lemma lfilter_lfinite[simp]:
assumes "lfinite (lfilter P t)"
and "¬ lfinite t"
shows "∃n. ∀n'>n. ¬ P (lnth t n')"
proof -
from assms have "finite {n. enat n < llength t ∧ P (lnth t n)}" using lfinite_lfilter by auto
then obtain k
where sset: "{n. enat n < llength t ∧ P (lnth t n)} ⊆ {n. n<k ∧ enat n < llength t ∧ P (lnth t n)}"
using finite_nat_bounded[of "{n. enat n < llength t ∧ P (lnth t n)}"] by auto
show ?thesis
proof (rule ccontr)
assume "¬(∃n. ∀n'>n. ¬ P (lnth t n'))"
hence "∀n. ∃n'>n. P (lnth t n')" by simp
then obtain n' where "n'>k" and "P (lnth t n')" by auto
moreover from ‹¬ lfinite t› have "n' < llength t" by (simp add: not_lfinite_llength)
ultimately have "n' ∉ {n. n<k ∧ enat n < llength t ∧ P (lnth t n)}" and
"n'∈{n. enat n < llength t ∧ P (lnth t n)}" by auto
with sset show False by auto
qed
qed

subsection "Specifying Dynamic Architectures"
text ‹
In the following we formalize dynamic architectures in terms of configuration traces, i.e., sequences of architecture configurations.
Moreover, we introduce definitions for operations to support the specification of configuration traces.
›
typedecl cnf
type_synonym trace = "nat ⇒ cnf"
consts arch:: "trace set"

type_synonym cta = "trace ⇒ nat ⇒ bool"

subsubsection "Implication"

definition imp :: "cta ⇒ cta ⇒ cta" (infixl "⟶⇧c" 10)
where "γ ⟶⇧c γ' ≡ λ t n. γ t n ⟶ γ' t n"

declare imp_def[simp]

lemma impI[intro!]:
fixes t n
assumes "γ t n ⟹ γ' t n"
shows "(γ ⟶⇧c γ') t n" using assms by simp

lemma impE[elim!]:
fixes t n
assumes "(γ ⟶⇧c γ') t n" and "γ t n" and "γ' t n ⟹ γ'' t n"
shows "γ'' t n" using assms by simp

subsubsection "Disjunction"

definition disj :: "cta ⇒ cta ⇒ cta" (infixl "∨⇧c" 15)
where "γ ∨⇧c γ' ≡ λ t n. γ t n ∨ γ' t n"

declare disj_def[simp]

lemma disjI1[intro]:
assumes "γ t n"
shows "(γ ∨⇧c γ') t n" using assms by simp

lemma disjI2[intro]:
assumes "γ' t n"
shows "(γ ∨⇧c γ') t n" using assms by simp

lemma disjE[elim!]:
assumes "(γ ∨⇧c γ') t n"
and "γ t n ⟹ γ'' t n"
and "γ' t n ⟹ γ'' t n"
shows "γ'' t n" using assms by auto

subsubsection "Conjunction"

definition conj :: "cta ⇒ cta ⇒ cta" (infixl "∧⇧c" 20)
where "γ ∧⇧c γ' ≡ λ t n. γ t n ∧ γ' t n"

declare conj_def[simp]

lemma conjI[intro!]:
fixes n
assumes "γ t n" and "γ' t n"
shows "(γ ∧⇧c γ') t n" using assms by simp

lemma conjE[elim!]:
fixes n
assumes "(γ ∧⇧c γ') t n" and "γ t n ⟹ γ' t n ⟹ γ'' t n"
shows "γ'' t n" using assms by simp

subsubsection "Negation"

definition neg :: "cta ⇒ cta" ("¬⇧c _" [19] 19)
where "¬⇧c γ ≡ λ t n. ¬ γ t n"

declare neg_def[simp]

lemma negI[intro!]:
assumes "γ t n ⟹ False"
shows "(¬⇧c γ) t n" using assms by auto

lemma negE[elim!]:
assumes "(¬⇧c γ) t n"
and "γ t n"
shows "γ' t n" using assms by simp

subsubsection "Quantifiers"

definition all :: "('a ⇒ cta)
⇒ cta" (binder "∀⇩c" 10)
where "all P ≡ λt n. (∀y. (P y t n))"

declare all_def[simp]

lemma allI[intro!]:
assumes "⋀x. γ x t n"
shows "(∀⇩cx. γ x) t n" using assms by simp

lemma allE[elim!]:
fixes n
assumes "(∀⇩cx. γ x) t n" and "γ x t n ⟹ γ' t n"
shows "γ' t n" using assms by simp

definition ex :: "('a ⇒ cta)
⇒ cta" (binder "∃⇩c" 10)
where "ex P ≡ λt n. (∃y. (P y t n))"

declare ex_def[simp]

lemma exI[intro!]:
assumes "γ x t n"
shows "(∃⇩cx. γ x) t n" using assms HOL.exI by simp

lemma exE[elim!]:
assumes "(∃⇩cx. γ x) t n" and "⋀x. γ x t n ⟹ γ' t n"
shows "γ' t n" using assms HOL.exE by auto

subsubsection "Atomic Assertions"
text ‹
First we provide rules for basic behavior assertions.
›

definition ca :: "(cnf ⇒ bool) ⇒ cta"
where "ca φ ≡ λ t n. φ (t n)"

lemma caI[intro]:
fixes n
assumes "φ (t n)"
shows "(ca φ) t n" using assms ca_def by simp

lemma caE[elim]:
fixes n
assumes "(ca φ) t n"
shows "φ (t n)" using assms ca_def by simp

subsubsection "Next Operator"

definition nxt :: "cta ⇒ cta" ("○⇩c(_)" 24)
where "○⇩c(γ) ≡ λ(t::(nat ⇒ cnf)) n. γ t (Suc n)"

subsubsection "Eventually Operator"

definition evt :: "cta ⇒ cta" ("◇⇩c(_)" 23)
where "◇⇩c(γ) ≡ λ(t::(nat ⇒ cnf)) n. ∃n'≥n. γ t n'"

subsubsection "Globally Operator"

definition glob :: "cta ⇒ cta" ("□⇩c(_)" 22)
where "□⇩c(γ) ≡ λ(t::(nat ⇒ cnf)) n. ∀n'≥n. γ t n'"

lemma globI[intro!]:
fixes n'
assumes "∀n≥n'. γ t n"
shows "(□⇩c(γ)) t n'" using assms glob_def by simp

lemma globE[elim!]:
fixes n n'
assumes "(□⇩c(γ)) t n" and "n'≥n"
shows "γ t n'" using assms glob_def by simp

subsubsection "Until Operator"

definition until :: "cta ⇒ cta ⇒ cta" (infixl "𝔘⇩c" 21)
where "γ' 𝔘⇩c γ ≡ λ(t::(nat ⇒ cnf)) n. ∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n')"

lemma untilI[intro]:
fixes n
assumes "∃n''≥n. γ t n'' ∧ (∀n'≥n. n'<n'' ⟶ γ' t n')"
shows "(γ' 𝔘⇩c γ) t n" using assms until_def by simp

lemma untilE[elim]:
fixes n
assumes "(γ' 𝔘⇩c γ) t n"
shows "∃n''≥n. γ t n'' ∧ (∀n'≥n. n'<n'' ⟶ γ' t n')" using assms until_def by simp

subsubsection "Weak Until"

definition wuntil :: "cta ⇒ cta ⇒ cta" (infixl "𝔚⇩c" 20)
where "γ' 𝔚⇩c γ ≡ γ' 𝔘⇩c γ ∨⇧c □⇩c(γ')"

lemma wUntilI[intro]:
fixes n
assumes "(∃n''≥n. γ t n'' ∧ (∀n'≥n. n'<n'' ⟶ γ' t n')) ∨ (∀n'≥n. γ' t n')"
shows "(γ' 𝔚⇩c γ) t n" using assms wuntil_def by auto

lemma wUntilE[elim]:
fixes n n'
assumes "(γ' 𝔚⇩c γ) t n"
shows "(∃n''≥n. γ t n'' ∧ (∀n'≥n. n'<n'' ⟶ γ' t n')) ∨ (∀n'≥n. γ' t n')"
proof -
from assms have "(γ' 𝔘⇩c γ ∨⇧c □⇩c(γ')) t n" using wuntil_def by simp
hence "(γ' 𝔘⇩c γ) t n ∨ (□⇩c(γ')) t n" by simp
thus ?thesis
proof
assume "(γ' 𝔘⇩c γ) t n"
hence "∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n')" by auto
thus ?thesis by auto
next
assume "(□⇩cγ') t n"
hence "∀n'≥n. γ' t n'" by auto
thus ?thesis by auto
qed
qed

lemma wUntil_Glob:
assumes "(γ' 𝔚⇩c γ) t n"
and "(□⇩c(γ' ⟶⇧c γ'')) t n"
shows "(γ'' 𝔚⇩c γ) t n"
proof
from assms(1) have "(∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n')) ∨ (∀n'≥n. γ' t n')" using wUntilE by simp
thus "(∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ'' t n')) ∨ (∀n'≥n. γ'' t n')"
proof
assume "∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n')"
show "(∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ'' t n')) ∨ (∀n'≥n. γ'' t n')"
proof -
from ‹∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ' t n')› obtain n'' where "n''≥n" and "γ t n''" and a1: "∀n'≥n. n' < n'' ⟶ γ' t n'" by auto
moreover have "∀n'≥n. n' < n'' ⟶ γ'' t n'"
proof
fix n'
show "n'≥n ⟶ n'< n'' ⟶ γ'' t n'"
proof (rule HOL.impI[OF HOL.impI])
assume "n'≥n" and "n'<n''"
with assms(2) have "(γ' ⟶⇧c γ'') t n'" using globE by simp
hence "γ' t n' ⟶ γ'' t n'" using impE by auto
moreover from a1 ‹n'≥n› ‹n'<n''› have "γ' t n'" by simp
ultimately show "γ'' t n'" by simp
qed
qed
ultimately show ?thesis by auto
qed
next
assume a1: "∀n'≥n. γ' t n'"
have "∀n'≥n. γ'' t n'"
proof
fix n'
show "n'≥n ⟶ γ'' t n'"
proof
assume "n'≥n"
with assms(2) have "(γ' ⟶⇧c γ'') t n'" using globE by simp
hence "γ' t n' ⟶ γ'' t n'" using impE by auto
moreover from a1 ‹n'≥n› have "γ' t n'" by simp
ultimately show "γ'' t n'" by simp
qed
qed
thus "(∃n''≥n. γ t n'' ∧ (∀n'≥n. n' < n'' ⟶ γ'' t n')) ∨ (∀n'≥n. γ'' t n')" by simp
qed
qed

subsection "Dynamic Components"
text ‹
To support the specification of patterns over dynamic architectures we provide a locale for dynamic components.
It takes the following type parameters:
\begin{itemize}
\item id: a type for component identifiers
\item cmp: a type for components
\item cnf: a type for architecture configurations
\end{itemize}
›
locale dynamic_component =
fixes tCMP :: "'id ⇒ cnf ⇒ 'cmp" ("σ⇘_⇙(_)" [0,110]60)
and active :: "'id ⇒ cnf ⇒ bool" ("∥_∥⇘_⇙" [0,110]60)
begin

text ‹
The locale requires two parameters:
\begin{itemize}
\item @{term tCMP} is an operator to obtain a component with a certain identifier from an architecture configuration.
\item @{term active} is a predicate to assert whether a certain component is activated within an architecture configuration.
\end{itemize}
›

text ‹
The locale provides some general properties about its parameters and introduces six important operators over configuration traces:
\begin{itemize}
\item An operator to extract the behavior of a certain component out of a given configuration trace.
\item An operator to obtain the number of activations of a certain component within a given configuration trace.
\item An operator to obtain the least point in time (before a certain point in time) from which on a certain component is not activated anymore.
\item An operator to obtain the latest point in time where a certain component was activated.
\item Two operators to map time-points between configuration traces and behavior traces.
\end{itemize}
Moreover, the locale provides several properties about the operators and their relationships.
›

lemma nact_active:
fixes t::"nat ⇒ cnf"
and n::nat
and n''
and id
assumes "∥id∥⇘t n⇙"
and "n'' ≥ n"
and "¬ (∃n'≥n. n' < n'' ∧ ∥id∥⇘t n'⇙)"
shows "n=n''"
using assms le_eq_less_or_eq by auto

lemma nact_exists:
fixes t::"nat ⇒ cnf"
assumes "∃i≥n. ∥c∥⇘t i⇙"
shows "∃i≥n. ∥c∥⇘t i⇙ ∧ (∄k. n≤k ∧ k<i ∧ ∥c∥⇘t k⇙)"
proof -
let ?L = "LEAST i. (i≥n ∧ ∥c∥⇘t i⇙)"
from assms have "?L≥n ∧ ∥c∥⇘t ?L⇙" using LeastI[of "λx::nat. (x≥n ∧ ∥c∥⇘t x⇙)"] by auto
moreover have "∄k. n≤k ∧ k<?L ∧ ∥c∥⇘t k⇙" using not_less_Least by auto
ultimately show ?thesis by blast
qed

lemma lActive_least:
assumes "∃i≥n. i < llength t ∧ ∥c∥⇘lnth t i⇙"
shows "∃i≥n. (i < llength t ∧ ∥c∥⇘lnth t i⇙ ∧ (∄k. n≤k ∧ k<i ∧ k<llength t ∧ ∥c∥⇘lnth t k⇙))"
proof -
let ?L = "LEAST i. (i≥n ∧ i < llength t ∧ ∥c∥⇘lnth t i⇙)"
from assms have "?L≥n ∧ ?L < llength t ∧ ∥c∥⇘lnth t ?L⇙"
using LeastI[of "λx::nat.(x≥n ∧ x<llength t ∧ ∥c∥⇘lnth t x⇙)"] by auto
moreover have "∄k. n≤k ∧ k<llength t ∧ k<?L ∧ ∥c∥⇘lnth t k⇙" using not_less_Least by auto
ultimately show ?thesis by blast
qed

subsection "Projection"
text ‹
In the following we introduce an operator which extracts the behavior of a certain component out of a given configuration trace.
›

definition proj:: "'id ⇒ (cnf llist) ⇒ ('cmp llist)" ("π⇘_⇙(_)" [0,110]60)
where "proj c = lmap (λcnf. (σ⇘c⇙(cnf))) ∘ (lfilter (active c))"

lemma proj_lnil [simp,intro]:
"π⇘c⇙([]⇩l) = []⇩l" using proj_def by simp

lemma proj_lnull [simp]:
"π⇘c⇙(t) = []⇩l ⟷ (∀k ∈ lset t. ¬ ∥c∥⇘k⇙)"
proof
assume "π⇘c⇙(t) = []⇩l"
hence "lfilter (active c) t = []⇩l" using proj_def lmap_eq_LNil by auto
thus "∀k ∈ lset t. ¬ ∥c∥⇘k⇙" using lfilter_eq_LNil[of "active c"] by simp
next
assume "∀k∈lset t. ¬ ∥c∥⇘k⇙"
hence "lfilter (active c) t = []⇩l" by simp
thus "π⇘c⇙(t) = []⇩l" using proj_def by simp
qed

lemma proj_LCons [simp]:
"π⇘i⇙(x #⇩l xs) = (if ∥i∥⇘x⇙ then (σ⇘i⇙(x)) #⇩l (π⇘i⇙(xs)) else π⇘i⇙(xs))"
using proj_def by simp

lemma proj_llength[simp]:
"llength (π⇘c⇙(t)) ≤ llength t"
using llength_lfilter_ile proj_def by simp

lemma proj_ltake:
assumes "∀(n'::nat)≤llength t. n'≥n ⟶ (¬ ∥c∥⇘lnth t n'⇙)"
shows "π⇘c⇙(t) = π⇘c⇙(ltake n t)" using lfilter_ltake proj_def assms by (metis comp_apply)

lemma proj_finite_bound:
assumes "lfinite (π⇘c⇙(inf_llist t))"
shows "∃n. ∀n'>n. ¬ ∥c∥⇘t n'⇙"
using assms lfilter_lfinite[of "active c" "inf_llist t"] proj_def by simp

subsubsection "Monotonicity and Continuity"

lemma proj_mcont:
shows "mcont lSup lprefix lSup lprefix (proj c)"
proof -
have "mcont lSup lprefix lSup lprefix (λx. lmap (λcnf. σ⇘c⇙(cnf)) (lfilter (active c) x))"
by simp
moreover have "(λx. lmap (λcnf. σ⇘c⇙(cnf)) (lfilter (active c) x)) =
lmap (λcnf. σ⇘c⇙(cnf)) ∘ lfilter (active c)" by auto
ultimately show ?thesis using proj_def by simp
qed

lemma proj_mcont2mcont:
assumes "mcont lub ord lSup lprefix f"
shows "mcont lub ord lSup lprefix (λx. π⇘c⇙(f x))"
proof -
have "mcont lSup lprefix lSup lprefix (proj c)" using proj_mcont by simp
with assms show ?thesis using llist.mcont2mcont[of lSup lprefix "proj c"] by simp
qed

lemma proj_mono_prefix[simp]:
assumes "lprefix t t'"
shows "lprefix (π⇘c⇙(t)) (π⇘c⇙(t'))"
proof -
from assms have "lprefix (lfilter (active c) t) (lfilter (active c) t')" using lprefix_lfilterI by simp
hence "lprefix (lmap (λcnf. σ⇘c⇙(cnf)) (lfilter (active c) t))
(lmap (λcnf. σ⇘c⇙(cnf)) (lfilter (active c) t'))" using lmap_lprefix by simp
thus ?thesis using proj_def by simp
qed

subsubsection "Finiteness"

lemma proj_finite[simp]:
assumes "lfinite t"
shows "lfinite (π⇘c⇙(t))"
using assms proj_def by simp

lemma proj_finite2:
assumes "∀(n'::nat)≤llength t. n'≥n ⟶ (¬ ∥c∥⇘lnth t n'⇙)"
shows "lfinite (π⇘c⇙(t))" using assms proj_ltake proj_finite by simp

lemma proj_append_lfinite[simp]:
fixes t t'
assumes "lfinite t"
shows "π⇘c⇙(t @⇩l t') = (π⇘c⇙(t)) @⇩l (π⇘c⇙(t'))" (is "?lhs=?rhs")
proof -
have "?lhs = (lmap (λcnf. σ⇘c⇙(cnf)) ∘ (lfilter (active c))) (t @⇩l t')" using proj_def by simp
also have "… = lmap (λcnf. σ⇘c⇙(cnf)) (lfilter (active c) (t @⇩l t'))" by simp
also from assms have "… = lmap (λcnf. σ⇘c⇙(cnf))
((lfilter (active c) t) @⇩l (lfilter (active c) t'))" by simp
also have "… = (@⇩l) (lmap (λcnf. σ⇘c⇙(cnf)) (lfilter (active c) t))
(lmap (λcnf. σ⇘c⇙(cnf)) (lfilter (active c) t'))" using lmap_lappend_distrib by simp
also have "… = ?rhs" using proj_def by simp
finally show ?thesis .
qed

lemma proj_one:
assumes "∃i. i < llength t ∧ ∥c∥⇘lnth t i⇙"
shows "llength (π⇘c⇙(t)) ≥ 1"
proof -
from assms have "∃x∈lset t. ∥c∥⇘x⇙" using lset_conv_lnth by force
hence "¬ lfilter (λk. ∥c∥⇘k⇙) t = []⇩l" using lfilter_eq_LNil[of "(λk. ∥c∥⇘k⇙)"] by blast
hence "¬ π⇘c⇙(t) = []⇩l" using proj_def by fastforce
thus ?thesis by (simp add: ileI1 lnull_def one_eSuc)
qed

subsubsection "Projection not Active"

lemma proj_not_active[simp]:
assumes "enat n < llength t"
and "¬ ∥c∥⇘lnth t n⇙"
shows "π⇘c⇙(ltake (Suc n) t) = π⇘c⇙(ltake n t)" (is "?lhs = ?rhs")
proof -
from assms have "ltake (enat (Suc n)) t = (ltake (enat n) t) @⇩l ((lnth t n) #⇩l []⇩l)"
using ltake_Suc_conv_snoc_lnth by blast
hence "?lhs = π⇘c⇙((ltake (enat n) t) @⇩l ((lnth t n) #⇩l []⇩l))" by simp
moreover have "… = (π⇘c⇙(ltake (enat n) t)) @⇩l (π⇘c⇙((lnth t n) #⇩l []⇩l))" by simp
moreover from assms have "π⇘c⇙((lnth t n) #⇩l []⇩l) = []⇩l" by simp
ultimately show ?thesis by simp
qed

lemma proj_not_active_same:
assumes "enat n ≤ (n'::enat)"
and "¬ lfinite t ∨ n'-1 < llength t"
and "∄k. k≥n ∧ k<n' ∧ k < llength t ∧ ∥c∥⇘lnth t k⇙"
shows "π⇘c⇙(ltake n' t) = π⇘c⇙(ltake n t)"
proof -
have "π⇘c⇙(ltake (n + (n' - n)) t) = π⇘c⇙((ltake n t) @⇩l (ltake (n'-n) (ldrop n t)))"
hence "π⇘c⇙(ltake (n + (n' - n)) t) =
(π⇘c⇙(ltake n t)) @⇩l (π⇘c⇙(ltake (n'-n) (ldrop n t)))" by simp
moreover have "π⇘c⇙(ltake (n'-n) (ldrop n t)) = []⇩l"
proof -
have "∀k∈{lnth (ltake (n' - enat n) (ldrop (enat n) t)) na |
na. enat na < llength (ltake (n' - enat n) (ldrop (enat n) t))}. ¬ ∥c∥⇘k⇙"
proof
fix k assume "k∈{lnth (ltake (n' - enat n) (ldrop (enat n) t)) na |
na. enat na < llength (ltake (n' - enat n) (ldrop (enat n) t))}"
then obtain k' where "enat k' < llength (ltake (n' - enat n) (ldrop (enat n) t))"
and "k=lnth (ltake (n' - enat n) (ldrop (enat n) t)) k'" by auto
have "enat (k' + n) < llength t"
proof -
from ‹enat k' < llength (ltake (n' - enat n) (ldrop (enat n) t))› have "enat k' < n'-n" by simp
hence "enat k' + n < n'" using assms(1) enat_min by auto
show ?thesis
proof cases
assume "lfinite t"
with ‹¬ lfinite t ∨ n'-1 < llength t› have "n'-1<llength t" by simp
hence "n'< eSuc (llength t)" by (metis eSuc_minus_1 enat_minus_mono1 leD leI)
hence "n'≤ llength t" using eSuc_ile_mono ileI1 by blast
with ‹enat k' + n < n'› show ?thesis by (simp add: add.commute)
next
assume "¬ lfinite t"
hence "llength t = ∞" using not_lfinite_llength by auto
thus ?thesis by simp
qed
qed
moreover have "k = lnth t (k' + n)"
proof -
from ‹enat k' < llength (ltake (n' - enat n) (ldrop (enat n) t))›
have "enat k'<n' - enat n" by auto
hence "lnth (ltake (n' - enat n) (ldrop (enat n) t)) k' = lnth (ldrop (enat n) t) k'"
using lnth_ltake[of k' "n' - enat n"] by simp
with ‹enat (k' + n) < llength t› show ?thesis using lnth_ldrop[of n k' t ]
using ‹k = lnth (ltake (n' - enat n) (ldrop (enat n) t)) k'› by (simp add: add.commute)
qed
moreover from ‹enat n ≤ (n'::enat)› have "k' + the_enat n≥n" by auto
moreover from ‹enat k' < llength (ltake (n' - enat n) (ldrop (enat n) t))› have "k' + n<n'"
using assms(1) enat_min by auto
ultimately show "¬ ∥c∥⇘k⇙" using ‹∄k. k≥n ∧ k<n' ∧ k < llength t ∧ ∥c∥⇘lnth t k⇙› by simp
qed
hence "∀k∈lset (ltake (n'-n) (ldrop n t)). ¬ ∥c∥⇘k⇙"
using lset_conv_lnth[of "(ltake (n' - enat n) (ldrop (enat n) t))"] by simp
thus ?thesis using proj_lnull by auto
qed
moreover from assms have "n + (n' - n) = n'"
by (meson enat.distinct(1) enat_add_sub_same enat_diff_cancel_left enat_le_plus_same(1) less_imp_le)
ultimately show ?thesis by simp
qed

subsubsection "Projection Active"

lemma proj_active[simp]:
assumes "enat i < llength t" "∥c∥⇘lnth t i⇙"
shows "π⇘c⇙(ltake (Suc i) t) = (π⇘c⇙(ltake i t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)" (is "?lhs = ?rhs")
proof -
from assms have "ltake (enat (Suc i)) t = (ltake (enat i) t) @⇩l ((lnth t i) #⇩l []⇩l)"
using ltake_Suc_conv_snoc_lnth by blast
hence "?lhs = π⇘c⇙((ltake (enat i) t) @⇩l ((lnth t i) #⇩l []⇩l))" by simp
moreover have "… = (π⇘c⇙(ltake (enat i) t)) @⇩l (π⇘c⇙((lnth t i) #⇩l []⇩l))" by simp
moreover from assms have "π⇘c⇙((lnth t i) #⇩l []⇩l) = (σ⇘c⇙(lnth t i)) #⇩l []⇩l" by simp
ultimately show ?thesis by simp
qed

lemma proj_active_append:
assumes a1: "(n::nat) ≤ i"
and a2: "enat i < (n'::enat)"
and a3: "¬ lfinite t ∨ n'-1 < llength t"
and a4: "∥c∥⇘lnth t i⇙"
and "∀i'. (n ≤ i' ∧ enat i'<n' ∧ i' < llength t ∧ ∥c∥⇘lnth t i'⇙) ⟶ (i' = i)"
shows "π⇘c⇙(ltake n' t) = (π⇘c⇙(ltake n t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)" (is "?lhs = ?rhs")
proof -
have "?lhs = π⇘c⇙(ltake (Suc i) t)"
proof -
from a2 have "Suc i ≤ n'" by (simp add: Suc_ile_eq)
moreover from a3 have "¬ lfinite t ∨ n'-1 < llength t" by simp
moreover have "∄k. enat k≥enat (Suc i) ∧ k<n' ∧ k < llength t ∧ ∥c∥⇘lnth t k⇙"
proof
assume "∃k. enat k≥enat (Suc i) ∧ k<n' ∧ k < llength t ∧ ∥c∥⇘lnth t k⇙"
then obtain k where "enat k≥enat (Suc i)" and "k<n'" and "k < llength t" and "∥c∥⇘lnth t k⇙" by blast
moreover from ‹enat k≥enat (Suc i)› have "enat k≥n"
using assms by (meson dual_order.trans enat_ord_simps(1) le_SucI)
ultimately have "enat k=enat i" using assms using enat_ord_simps(1) by blast
with ‹enat k≥enat (Suc i)› show False by simp
qed
ultimately show ?thesis using proj_not_active_same[of "Suc i" n' t c] by simp
qed
also have "… = (π⇘c⇙(ltake i t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)"
proof -
have "i < llength t"
proof cases
assume "lfinite t"
with a3 have "n'-1 < llength t" by simp
hence "n' ≤ llength t" by (metis eSuc_minus_1 enat_minus_mono1 ileI1 not_le)
with a2 show "enat i < llength t" by simp
next
assume "¬ lfinite t"
thus ?thesis by (metis enat_ord_code(4) llength_eq_infty_conv_lfinite)
qed
with a4 show ?thesis by simp
qed
also have "… = ?rhs"
proof -
from a1 have "enat n ≤ enat i" by simp
moreover from a2 a3 have "¬ lfinite t ∨ enat i-1 < llength t"
using enat_minus_mono1 less_imp_le order.strict_trans1 by blast
moreover have "∄k. k≥n ∧ enat k<enat i ∧ enat k < llength t ∧ ∥c∥⇘lnth t k⇙"
proof
assume "∃k. k≥n ∧ enat k<enat i ∧ enat k < llength t ∧ ∥c∥⇘lnth t k⇙"
then obtain k where "k≥n" and "enat k<enat i" and "enat k < llength t" and "∥c∥⇘lnth t k⇙" by blast
moreover from ‹enat k<enat i› have "enat k<n'" using assms dual_order.strict_trans by blast
ultimately have "enat k=enat i" using assms by simp
with ‹enat k<enat i› show False by simp
qed
ultimately show ?thesis using proj_not_active_same[of n i t c] by simp
qed
finally show ?thesis by simp
qed

subsubsection "Same and not Same"

lemma proj_same_not_active:
assumes "n ≤ n'"
and "enat (n'-1) < llength t"
and "π⇘c⇙(ltake n' t) = π⇘c⇙(ltake n t)"
shows "∄k. k≥n ∧ k<n' ∧ ∥c∥⇘lnth t k⇙"
proof
assume "∃k. k≥n ∧ k<n' ∧ ∥c∥⇘lnth t k⇙"
then obtain i where "i≥n" and "i<n'" and "∥c∥⇘lnth t i⇙" by blast
moreover from ‹enat (n'-1)<llength t› and ‹i<n'› have "i<llength t"
by (metis diff_Suc_1 dual_order.strict_trans enat_ord_simps(2) lessE)
ultimately have "π⇘c⇙(ltake (Suc i) t) =
(π⇘c⇙(ltake i t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)" by simp
moreover from ‹i<n'› have "Suc i ≤ n'" by simp
hence "lprefix(π⇘c⇙(ltake (Suc i) t)) (π⇘c⇙(ltake n' t))" by simp
then obtain "tl" where "π⇘c⇙(ltake n' t) = (π⇘c⇙(ltake (Suc i) t)) @⇩l tl"
using lprefix_conv_lappend by auto
moreover from ‹n≤i› have "lprefix(π⇘c⇙(ltake n t)) (π⇘c⇙(ltake i t))" by simp
hence "lprefix(π⇘c⇙(ltake n t)) (π⇘c⇙(ltake i t))" by simp
then obtain "hd" where "π⇘c⇙(ltake i t) = (π⇘c⇙(ltake n t)) @⇩l hd"
using lprefix_conv_lappend by auto
ultimately have "π⇘c⇙(ltake n' t) =
(((π⇘c⇙(ltake n t)) @⇩l hd) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)) @⇩l tl" by simp
also have "… = ((π⇘c⇙(ltake n t)) @⇩l hd) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l tl)"
using lappend_snocL1_conv_LCons2[of "(π⇘c⇙(ltake n t)) @⇩l hd" "σ⇘c⇙(lnth t i)"] by simp
also have "… = (π⇘c⇙(ltake n t)) @⇩l (hd @⇩l ((σ⇘c⇙(lnth t i)) #⇩l tl))"
using lappend_assoc by auto
also have "π⇘c⇙(ltake n' t) = (π⇘c⇙(ltake n' t)) @⇩l []⇩l" by simp
finally have "(π⇘c⇙(ltake n' t)) @⇩l []⇩l = (π⇘c⇙(ltake n t)) @⇩l (hd @⇩l ((σ⇘c⇙(lnth t i)) #⇩l tl))" .
moreover from assms(3) have "llength (π⇘c⇙(ltake n' t)) = llength (π⇘c⇙(ltake n t))" by simp
ultimately have "lfinite (π⇘c⇙(ltake n' t)) ⟶ []⇩l = hd @⇩l ((σ⇘c⇙(lnth t i)) #⇩l tl)"
using assms(3) lappend_eq_lappend_conv[of "π⇘c⇙(ltake n' t)" "π⇘c⇙(ltake n t)" "[]⇩l"] by simp
moreover have "lfinite (π⇘c⇙(ltake n' t))" by simp
ultimately have "[]⇩l = hd @⇩l ((σ⇘c⇙(lnth t i)) #⇩l tl)" by simp
hence "(σ⇘c⇙(lnth t i)) #⇩l tl = []⇩l" using LNil_eq_lappend_iff by auto
thus False by simp
qed

lemma proj_not_same_active:
assumes "enat n ≤ (n'::enat)"
and "(¬ lfinite t) ∨ n'-1 < llength t"
and "¬(π⇘c⇙(ltake n' t) = π⇘c⇙(ltake n t))"
shows "∃k. k≥n ∧ k<n' ∧ enat k < llength t ∧ ∥c∥⇘lnth t k⇙"
proof (rule ccontr)
assume "¬(∃k. k≥n ∧ k<n' ∧ enat k < llength t ∧ ∥c∥⇘lnth t k⇙)"
have "π⇘c⇙(ltake n' t) = π⇘c⇙(ltake (enat n) t)"
proof cases
assume "lfinite t"
hence "llength t≠∞" by (simp add: lfinite_llength_enat)
hence "enat (the_enat (llength t)) = llength t" by auto
with assms ‹¬ (∃k≥n. k < n' ∧ enat k < llength t ∧ ∥c∥⇘lnth t k⇙)›
show ?thesis using proj_not_active_same[of n n' t c] by simp
next
assume "¬ lfinite t"
with assms ‹¬ (∃k≥n. k < n' ∧ enat k < llength t ∧ ∥c∥⇘lnth t k⇙)›
show ?thesis using proj_not_active_same[of n n' t c] by simp
qed
with assms show False by simp
qed

subsection "Activations"
text ‹
We also introduce an operator to obtain the number of activations of a certain component within a given configuration trace.
›

definition nAct :: "'id ⇒ enat ⇒ (cnf llist) ⇒ enat" ("⟨_ #⇘_⇙_⟩") where
"⟨c #⇘n⇙ t⟩ ≡ llength (π⇘c⇙(ltake n t))"

lemma nAct_0[simp]:
"⟨c #⇘0⇙ t⟩ = 0" by (simp add: nAct_def)

lemma nAct_NIL[simp]:
"⟨c #⇘n⇙ []⇩l⟩ = 0" by (simp add: nAct_def)

lemma nAct_Null:
assumes "llength t ≥ n"
and "⟨c #⇘n⇙ t⟩ = 0"
shows "∀i<n. ¬ ∥c∥⇘lnth t i⇙"
proof -
from assms have "lnull (π⇘c⇙(ltake n t))" using nAct_def lnull_def by simp
hence "π⇘c⇙(ltake n t) = []⇩l" using lnull_def by blast
hence "(∀k∈lset (ltake n t). ¬ ∥c∥⇘k⇙)" by simp
show ?thesis
proof (rule ccontr)
assume "¬ (∀i<n. ¬ ∥c∥⇘lnth t i⇙)"
then obtain i where "i<n" and "∥c∥⇘lnth t i⇙" by blast
moreover have "enat i < llength (ltake n t)  ∧ lnth (ltake n t) i = (lnth t i)"
proof
from ‹llength t ≥ n› have "n = min n (llength t)" using min.orderE by auto
hence "llength (ltake n t) = n" by simp
with ‹i<n› show "enat i < llength (ltake n t)" by auto
from ‹i<n› show "lnth (ltake n t) i = (lnth t i)" using lnth_ltake by auto
qed
hence "(lnth t i ∈ lset (ltake n t))" using in_lset_conv_lnth[of "lnth t i" "ltake n t"] by blast
ultimately show False using ‹(∀k∈lset (ltake n t). ¬ ∥c∥⇘k⇙)› by simp
qed
qed

lemma nAct_ge_one[simp]:
assumes "llength t ≥ n"
and "i < n"
and "∥c∥⇘lnth t i⇙"
shows "⟨c #⇘n⇙ t⟩ ≥ enat 1"
proof (rule ccontr)
assume "¬ (⟨c #⇘n⇙ t⟩ ≥ enat 1)"
hence "⟨c #⇘n⇙ t⟩ < enat 1" by simp
hence "⟨c #⇘n⇙ t⟩ < 1" using enat_1 by simp
hence "⟨c #⇘n⇙ t⟩ = 0" using Suc_ile_eq ‹¬ enat 1 ≤ ⟨c #⇘n⇙ t⟩› zero_enat_def by auto
with ‹llength t ≥ n› have "∀i<n. ¬ ∥c∥⇘lnth t i⇙" using nAct_Null by simp
with assms show False by simp
qed

lemma nAct_finite[simp]:
assumes "n ≠ ∞"
shows "∃n'. ⟨c #⇘n⇙ t⟩ = enat n'"
proof -
from assms have "lfinite (ltake n t)" by simp
hence "lfinite (π⇘c⇙(ltake n t))" by simp
hence "∃n'. llength (π⇘c⇙(ltake n t)) = enat n'" using lfinite_llength_enat[of "π⇘c⇙(ltake n t)"] by simp
thus ?thesis using nAct_def by simp
qed

lemma nAct_enat_the_nat[simp]:
assumes "n ≠ ∞"
shows "enat (the_enat (⟨c #⇘n⇙ t⟩)) = ⟨c #⇘n⇙ t⟩"
proof -
from assms have "⟨c #⇘n⇙ t⟩ ≠ ∞" by simp
thus ?thesis using enat_the_enat by simp
qed

subsubsection "Monotonicity and Continuity"

lemma nAct_mcont:
shows "mcont lSup lprefix Sup (≤) (nAct c n)"
proof -
have "mcont lSup lprefix lSup lprefix (ltake n)" by simp
hence "mcont lSup lprefix lSup lprefix (λt. π⇘c⇙(ltake n t))"
using proj_mcont2mcont[of lSup lprefix "(ltake n)"] by simp
hence "mcont lSup lprefix Sup (≤) (λt. llength (π⇘c⇙(ltake n t)))" by simp
moreover have "nAct c n = (λt. llength (π⇘c⇙(ltake n t)))" using nAct_def by auto
ultimately show ?thesis by simp
qed

lemma nAct_mono:
assumes "n ≤ n'"
shows "⟨c #⇘n⇙ t⟩ ≤ ⟨c #⇘n'⇙ t⟩"
proof -
from assms have "lprefix (ltake n t) (ltake n' t)" by simp
hence "lprefix (π⇘c⇙(ltake n t)) (π⇘c⇙(ltake n' t))" by simp
hence "llength (π⇘c⇙(ltake n t)) ≤ llength (π⇘c⇙(ltake n' t))"
using lprefix_llength_le[of "(π⇘c⇙(ltake n t))"] by simp
thus ?thesis using nAct_def by simp
qed

lemma nAct_strict_mono_back:
assumes "⟨c #⇘n⇙ t⟩ < ⟨c #⇘n'⇙ t⟩"
shows "n < n'"
proof (rule ccontr)
assume "¬ n<n'"
hence "n≥n'" by simp
hence "⟨c #⇘n⇙ t⟩ ≥ ⟨c #⇘n'⇙ t⟩" using nAct_mono by simp
thus False using assms by simp
qed

subsubsection "Not Active"

lemma nAct_not_active[simp]:
fixes n::nat
and n'::nat
and t::"(cnf llist)"
and c::'id
assumes "enat i < llength t"
and "¬ ∥c∥⇘lnth t i⇙"
shows "⟨c #⇘Suc i⇙ t⟩ = ⟨c #⇘i⇙ t⟩"
proof -
from assms have "π⇘c⇙(ltake (Suc i) t) = π⇘c⇙(ltake i t)" by simp
hence "llength (π⇘c⇙(ltake (enat (Suc i)) t)) = llength (π⇘c⇙(ltake i t))" by simp
moreover have "llength (π⇘c⇙(ltake i t)) ≠ ∞"
using llength_eq_infty_conv_lfinite[of "π⇘c⇙(ltake (enat i) t)"] by simp
ultimately have "llength (π⇘c⇙(ltake (Suc i) t)) = llength (π⇘c⇙(ltake i t))"
using the_enat_eSuc by simp
with nAct_def show ?thesis by simp
qed

lemma nAct_not_active_same:
assumes "enat n ≤ (n'::enat)"
and "n'-1 < llength t"
and "∄k. enat k≥n ∧ k<n' ∧ ∥c∥⇘lnth t k⇙"
shows "⟨c #⇘n'⇙ t⟩ = ⟨c #⇘n⇙ t⟩"
using assms proj_not_active_same nAct_def by simp

subsubsection "Active"

lemma nAct_active[simp]:
fixes n::nat
and n'::nat
and t::"(cnf llist)"
and c::'id
assumes "enat i < llength t"
and "∥c∥⇘lnth t i⇙"
shows "⟨c #⇘Suc i⇙ t⟩ = eSuc (⟨c #⇘i⇙ t⟩)"
proof -
from assms have "π⇘c⇙(ltake (Suc i) t) =
(π⇘c⇙(ltake i t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)" by simp
hence "llength (π⇘c⇙(ltake (enat (Suc i)) t)) = eSuc (llength (π⇘c⇙(ltake i t)))"
using plus_1_eSuc one_eSuc by simp
moreover have "llength (π⇘c⇙(ltake i t)) ≠ ∞"
using llength_eq_infty_conv_lfinite[of "π⇘c⇙(ltake (enat i) t)"] by simp
ultimately have "llength (π⇘c⇙(ltake (Suc i) t)) = eSuc (llength (π⇘c⇙(ltake i t)))"
using the_enat_eSuc by simp
with nAct_def show ?thesis by simp
qed

lemma nAct_active_suc:
fixes n::nat
and n'::enat
and t::"(cnf llist)"
and c::'id
assumes "¬ lfinite t ∨ n'-1 < llength t"
and "n ≤ i"
and "enat i < n'"
and "∥c∥⇘lnth t i⇙"
and "∀i'. (n ≤ i' ∧ enat i'<n' ∧ i' < llength t ∧ ∥c∥⇘lnth t i'⇙) ⟶ (i' = i)"
shows "⟨c #⇘n'⇙ t⟩ = eSuc (⟨c #⇘n⇙ t⟩)"
proof -
from assms have "π⇘c⇙(ltake n' t) = (π⇘c⇙(ltake (enat n) t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)"
using proj_active_append[of n i n' t c] by blast
moreover have "llength ((π⇘c⇙(ltake (enat n) t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)) =
eSuc (llength (π⇘c⇙(ltake (enat n) t)))" using one_eSuc eSuc_plus_1 by simp
ultimately show ?thesis using nAct_def by simp
qed

lemma nAct_less:
assumes "enat k < llength t"
and "n ≤ k"
and "k < (n'::enat)"
and "∥c∥⇘lnth t k⇙"
shows "⟨c #⇘n⇙ t⟩ < ⟨c #⇘n'⇙ t⟩"
proof -
have "⟨c #⇘k⇙ t⟩ ≠ ∞" by simp
then obtain en where en_def: "⟨c #⇘k⇙ t⟩ = enat en" by blast
moreover have "eSuc (enat en) ≤ ⟨c #⇘n'⇙ t⟩"
proof -
from assms have "Suc k ≤ n'" using Suc_ile_eq by simp
hence "⟨c #⇘Suc k⇙ t⟩ ≤ ⟨c #⇘n'⇙ t⟩" using nAct_mono by simp
moreover from assms have "⟨c #⇘Suc k⇙ t⟩ = eSuc (⟨c #⇘k⇙ t⟩)" by simp
ultimately have "eSuc (⟨c #⇘k⇙ t⟩) ≤ ⟨c #⇘n'⇙ t⟩" by simp
thus ?thesis using en_def by simp
qed
moreover have "enat en < eSuc (enat en)" by simp
ultimately have "enat en < ⟨c #⇘n'⇙ t⟩" using less_le_trans[of "enat en" "eSuc (enat en)"] by simp
moreover have "⟨c #⇘n⇙ t⟩ ≤ enat en"
proof -
from assms have "⟨c #⇘n⇙ t⟩ ≤ ⟨c #⇘k⇙ t⟩" using nAct_mono by simp
thus ?thesis using en_def by simp
qed
ultimately show ?thesis using le_less_trans[of "⟨c #⇘n⇙ t⟩"] by simp
qed

lemma nAct_less_active:
assumes "n' - 1 < llength t"
and "⟨c #⇘enat n⇙ t⟩ < ⟨c #⇘n'⇙ t⟩"
shows "∃i≥n. i<n' ∧ ∥c∥⇘lnth t i⇙"
proof (rule ccontr)
assume "¬ (∃i≥n. i<n' ∧ ∥c∥⇘lnth t i⇙)"
moreover have "enat n ≤ n'" using assms(2) less_imp_le nAct_strict_mono_back by blast
ultimately have "⟨c #⇘n⇙ t⟩ = ⟨c #⇘n'⇙ t⟩" using ‹n' - 1 < llength t› nAct_not_active_same by simp
thus False using assms by simp
qed

subsubsection "Same and Not Same"

lemma nAct_same_not_active:
assumes "⟨c #⇘n'⇙ inf_llist t⟩ = ⟨c #⇘n⇙ inf_llist t⟩"
shows "∀k≥n. k<n' ⟶ ¬ ∥c∥⇘t k⇙"
proof (rule ccontr)
assume "¬(∀k≥n. k<n' ⟶ ¬ ∥c∥⇘t k⇙)"
then obtain k where "k≥n" and "k<n'" and "∥c∥⇘t k⇙" by blast
hence "⟨c #⇘Suc k⇙ inf_llist t⟩ = eSuc (⟨c #⇘k⇙ inf_llist t⟩)" by simp
moreover have "⟨c #⇘k⇙ inf_llist t⟩≠∞" by simp
ultimately have "⟨c #⇘k⇙ inf_llist t⟩ < ⟨c #⇘Suc k⇙ inf_llist t⟩" by fastforce
moreover from ‹n≤k› have "⟨c #⇘n⇙ inf_llist t⟩ ≤ ⟨c #⇘k⇙ inf_llist t⟩" using nAct_mono by simp
moreover from ‹k<n'› have "Suc k ≤ n'" by (simp add: Suc_ile_eq)
hence "⟨c #⇘Suc k⇙ inf_llist t⟩ ≤ ⟨c #⇘n'⇙ inf_llist t⟩" using nAct_mono by simp
ultimately show False using assms by simp
qed

lemma nAct_not_same_active:
assumes "⟨c #⇘enat n⇙ t⟩ < ⟨c #⇘n'⇙ t⟩"
and "¬ lfinite t ∨ n' - 1 < llength t"
shows "∃(i::nat)≥n. enat i< n' ∧ i<llength t ∧ ∥c∥⇘lnth t i⇙"
proof -
from assms have "llength(π⇘c⇙(ltake n t)) < llength (π⇘c⇙(ltake n' t))" using nAct_def by simp
hence "π⇘c⇙(ltake n' t) ≠ π⇘c⇙(ltake n t)" by auto
moreover from assms have "enat n < n'" using nAct_strict_mono_back[of c "enat n" t n'] by simp
ultimately show ?thesis using proj_not_same_active[of n n' t c] assms by simp
qed

lemma nAct_less_llength_active:
assumes "x < llength (π⇘c⇙(t))"
and "enat x = ⟨c #⇘enat n'⇙ t⟩"
shows "∃(i::nat)≥n'. i<llength t ∧ ∥c∥⇘lnth t i⇙"
proof -
have "llength(π⇘c⇙(ltake n' t)) < llength (π⇘c⇙(t))" using assms(1) assms(2) nAct_def by auto
hence "llength(π⇘c⇙(ltake n' t)) < llength (π⇘c⇙(ltake (llength t) t))" by (simp add: ltake_all)
hence "⟨c #⇘enat n'⇙ t⟩ < ⟨c #⇘llength t⇙ t⟩" using nAct_def by simp
moreover have "¬ lfinite t ∨ llength t - 1 < llength t"
proof (rule Meson.imp_to_disjD[OF HOL.impI])
assume "lfinite t"
hence "llength t ≠ ∞" by (simp add: llength_eq_infty_conv_lfinite)
moreover have "llength t>0"
proof -
from ‹x < llength (π⇘c⇙(t))› have "llength (π⇘c⇙(t))>0" by auto
thus ?thesis using proj_llength order.strict_trans2 by blast
qed
ultimately show "llength t - 1 < llength t" by (metis One_nat_def ‹lfinite t› diff_Suc_less
enat_ord_simps(2) idiff_enat_enat lfinite_conv_llength_enat one_enat_def zero_enat_def)
qed
ultimately show ?thesis using nAct_not_same_active[of c n' t "llength t"] by simp
qed

lemma nAct_exists:
assumes "x < llength (π⇘c⇙(t))"
shows "∃(n'::nat). enat x = ⟨c #⇘n'⇙ t⟩"
proof -
have "x < llength (π⇘c⇙(t)) ⟶ (∃(n'::nat). enat x = ⟨c #⇘n'⇙ t⟩)"
proof (induction x)
case 0
thus ?case by (metis nAct_0 zero_enat_def)
next
case (Suc x)
show ?case
proof
assume "Suc x < llength (π⇘c⇙(t))"
hence "x < llength (π⇘c⇙(t))" using Suc_ile_eq less_imp_le by auto
with Suc.IH obtain n' where "enat x = ⟨c #⇘enat n'⇙ t⟩" by blast
with ‹x < llength (π⇘c⇙(t))› have "∃i≥n'. i < llength t ∧ ∥c∥⇘lnth t i⇙"
using nAct_less_llength_active[of x c t n'] by simp
then obtain i where "i≥n'" and "i<llength t" and "∥c∥⇘lnth t i⇙"
and "∄k. n'≤k ∧ k<i ∧ k<llength t ∧ ∥c∥⇘lnth t k⇙" using lActive_least[of n' t c] by auto
moreover from ‹i<llength t› have "¬ lfinite t ∨ enat (Suc i) - 1 < llength t"
moreover have "enat i < enat (Suc i)" by simp
moreover have "∀i'. (n' ≤ i' ∧ enat i'<enat (Suc i) ∧ i'<llength t ∧ ∥c∥⇘lnth t i'⇙) ⟶ (i' = i)"
proof (rule HOL.impI[THEN HOL.allI])
fix i' assume "n' ≤ i' ∧ enat i'<enat (Suc i) ∧ i'<llength t ∧ ∥c∥⇘lnth t i'⇙"
with ‹∄k. n'≤k ∧ k<i ∧ k<llength t ∧ ∥c∥⇘lnth t k⇙› show "i'=i" by fastforce
qed
ultimately have "⟨c #⇘Suc i⇙ t⟩ = eSuc (⟨c #⇘n'⇙ t⟩)" using nAct_active_suc[of t "Suc i" n' i c] by simp
with ‹enat x = ⟨c #⇘enat n'⇙ t⟩› have "⟨c #⇘Suc i⇙ t⟩ = eSuc (enat x)" by simp
thus "∃n'. enat (Suc x) = ⟨c #⇘enat n'⇙ t⟩" by (metis eSuc_enat)
qed
qed
with assms show ?thesis by simp
qed

subsection "Projection and Activation"
text ‹
In the following we provide some properties about the relationship between the projection and activations operator.
›

lemma nAct_le_proj:
"⟨c #⇘n⇙ t⟩ ≤ llength (π⇘c⇙(t))"
proof -
from nAct_def have "⟨c #⇘n⇙ t⟩ = llength (π⇘c⇙(ltake n t))" by simp
moreover have "llength (π⇘c⇙(ltake n t)) ≤ llength (π⇘c⇙(t))"
proof -
have "lprefix (ltake n t) t" by simp
hence "lprefix (π⇘c⇙(ltake n t)) (π⇘c⇙(t))" by simp
hence "llength (π⇘c⇙(ltake n t)) ≤ llength (π⇘c⇙(t))" using lprefix_llength_le by blast
thus ?thesis by auto
qed
thus ?thesis using nAct_def by simp
qed

lemma proj_nAct:
assumes "(enat n < llength t)"
shows "π⇘c⇙(ltake n t) = ltake (⟨c #⇘n⇙ t⟩) (π⇘c⇙(t))" (is "?lhs = ?rhs")
proof -
have "?lhs = ltake (llength (π⇘c⇙(ltake n t))) (π⇘c⇙(ltake n t))"
using ltake_all[of "π⇘c⇙(ltake n t)" "llength (π⇘c⇙(ltake n t))"] by simp
also have "… = ltake (llength (π⇘c⇙(ltake n t))) ((π⇘c⇙(ltake n t)) @⇩l (π⇘c⇙(ldrop n t)))"
using ltake_lappend1[of "llength (π⇘c⇙(ltake (enat n) t))" "π⇘c⇙(ltake n t)" "(π⇘c⇙(ldrop n t))"] by simp
also have "… = ltake (⟨c #⇘n⇙ t⟩) ((π⇘c⇙(ltake n t)) @⇩l (π⇘c⇙(ldrop n t)))" using nAct_def by simp
also have "… = ltake (⟨c #⇘n⇙ t⟩) (π⇘c⇙((ltake (enat n) t) @⇩l (ldrop n t)))" by simp
also have "… = ltake (⟨c #⇘n⇙ t⟩) (π⇘c⇙(t))" using lappend_ltake_ldrop[of n t] by simp
finally show ?thesis by simp
qed

lemma proj_active_nth:
assumes "enat (Suc i) < llength t" "∥c∥⇘lnth t i⇙"
shows "lnth (π⇘c⇙(t)) (the_enat (⟨c #⇘i⇙ t⟩)) = σ⇘c⇙(lnth t i)"
proof -
from assms have "enat i < llength t" using Suc_ile_eq[of i "llength t"] by auto
with assms have "π⇘c⇙(ltake (Suc i) t) = (π⇘c⇙(ltake i t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)" by simp
moreover have "lnth ((π⇘c⇙(ltake i t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l))
(the_enat (llength (π⇘c⇙(ltake i t)))) = σ⇘c⇙(lnth t i)"
proof -
have "¬ lnull ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)" by simp
moreover have "lfinite (π⇘c⇙(ltake i t))" by simp
ultimately have "lnth ((π⇘c⇙(ltake i t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l))
(the_enat (llength (π⇘c⇙(ltake i t)))) = lhd ((σ⇘c⇙(lnth t i)) #⇩l []⇩l)" by simp
also have "… = σ⇘c⇙(lnth t i)" by simp
finally show "lnth ((π⇘c⇙(ltake i t)) @⇩l ((σ⇘c⇙(lnth t i)) #⇩l []⇩l))
(the_enat (llength (π⇘c⇙(ltake i t)))) = σ⇘c⇙(lnth t i)" by simp
qed
ultimately have "σ⇘c⇙(lnth t i) = lnth (π⇘c⇙(ltake (Suc i) t))
(the_enat (llength (π⇘c⇙(ltake i t))))" by simp
also have "… = lnth (π⇘c⇙(ltake (Suc i) t)) (the_enat (⟨c #⇘i⇙ t⟩))" using nAct_def by simp
also have "… = lnth (ltake (⟨c #⇘Suc i⇙ t⟩) (π⇘c⇙(t))) (the_enat (⟨c #⇘i⇙ t⟩))"
using proj_nAct[of "Suc i" t c] assms by simp
also have "… = lnth (π⇘c⇙(t)) (the_enat (⟨c #⇘i⇙ t⟩))"
proof -
from assms have "⟨c #⇘Suc i⇙ t⟩ = eSuc (⟨c #⇘i⇙ t⟩)" using ‹enat i < llength t› by simp
moreover have "⟨c #⇘i⇙ t⟩ < eSuc (⟨c #⇘i⇙ t⟩)" using iless_Suc_eq[of "the_enat (⟨c #⇘enat i⇙ t⟩)"] by simp
ultimately have "⟨c #⇘i⇙ t⟩ < (⟨c #⇘Suc i⇙ t⟩)" by simp
hence "enat (the_enat (⟨c #⇘Suc i⇙ t⟩)) > enat (the_enat (⟨c #⇘i⇙ t⟩))" by simp
thus ?thesis using lnth_ltake[of "the_enat (⟨c #⇘i⇙ t⟩)" "the_enat (⟨c #⇘enat (Suc i)⇙ t⟩)" "π⇘c⇙(t)"] by simp
qed
finally show ?thesis ..
qed

lemma nAct_eq_proj:
assumes "¬(∃i≥n. ∥c∥⇘lnth t i⇙)"
shows "⟨c #⇘n⇙ t⟩ = llength (π⇘c⇙(t))" (is "?lhs = ?rhs")
proof -
from nAct_def have "?lhs = llength (π⇘c⇙(ltake n t))" by simp
moreover from assms have "∀(n'::nat)≤llength t. n'≥n ⟶ (¬ ∥c∥⇘lnth t n'⇙)" by simp
hence "π⇘c⇙(t) = π⇘c⇙(ltake n t)" using proj_ltake by simp
ultimately show ?thesis by simp
qed

lemma nAct_llength_proj:
assumes "∃i≥n. ∥c∥⇘t i⇙"
shows "llength (π⇘c⇙(inf_llist t)) ≥ eSuc (⟨c #⇘n⇙ inf_llist t⟩)"
proof -
from ‹∃i≥n. ∥c∥⇘t i⇙› obtain i where "i≥n" and "∥c∥⇘t i⇙"
and "¬ (∃k≥n. k < i ∧ k < llength (inf_llist t) ∧ ∥c∥⇘t k⇙)"
using lActive_least[of n "inf_llist t" c] by auto
moreover have "llength (π⇘c⇙(inf_llist t)) ≥ ⟨c #⇘Suc i⇙ inf_llist t⟩" using nAct_le_proj by simp
moreover have "eSuc (⟨c #⇘n⇙ inf_llist t⟩) = ⟨c #⇘Suc i⇙ inf_llist t⟩"
proof -
have "enat (Suc i) < llength (inf_llist t)" by simp
moreover have "i < Suc i" by simp
moreover from ‹¬ (∃k≥n. k < i ∧ k < llength (inf_llist t) ∧ ∥c∥⇘t k⇙)›
have "∀i'. n ≤ i' ∧ i' < Suc i ∧ ∥c∥⇘lnth (inf_llist t) i'⇙ ⟶ i' = i" by fastforce
ultimately show ?thesis using nAct_active_suc ‹i≥n› ‹∥c∥⇘t i⇙› by simp
qed
ultimately show ?thesis by simp
qed

subsection "Least not Active"
text ‹
In the following, we introduce an operator to obtain the least point in time before a certain point in time where a component was deactivated.
›

definition lNAct :: "'id ⇒ (nat ⇒ cnf) ⇒ nat ⇒ nat" ("⟨_ ⇐ _⟩⇘_⇙")
where "⟨c ⇐ t⟩⇘n⇙ ≡ (LEAST n'. n=n' ∨ (n'<n ∧ (∄k. k≥n' ∧ k<n ∧ ∥c∥⇘t k⇙)))"

lemma lNact0[simp]:
"⟨c ⇐ t⟩⇘0⇙ = 0"

lemma lNact_least:
assumes "n=n' ∨ n'<n ∧ (∄k. k≥n' ∧ k<n ∧ ∥c∥⇘t k⇙)"
shows "⟨c ⇐ t⟩⇘n⇙ ≤ n'"
using Least_le[of "λn'. n=n' ∨ (n'<n ∧ (∄k. k≥n' ∧ k<n ∧ ∥c∥⇘t k⇙))" n'] lNAct_def using assms by auto

lemma lNAct_ex: "⟨c ⇐ t⟩⇘n⇙=n ∨ ⟨c ⇐ t⟩⇘n⇙<n ∧ (∄k. k≥⟨c ⇐ t⟩⇘n⇙ ∧ k<n ∧ ∥c∥⇘t k⇙)"
proof -
let ?P="λn'. n=n' ∨ n'<n ∧ (∄k. k≥n' ∧ k<n ∧ ∥c∥⇘t k⇙)"
from lNAct_def have "⟨c ⇐ t⟩⇘n⇙ = (LEAST n'. ?P n')" by simp
moreover have "?P n" by simp
with LeastI have "?P (LEAST n'. ?P n')" .
ultimately show ?thesis by auto
qed

lemma lNact_notActive:
fixes c t n k
assumes "k≥⟨c ⇐ t⟩⇘n⇙"
and "k<n"
shows "¬∥c∥⇘t k⇙"
by (metis assms lNAct_ex leD)

lemma lNactGe:
fixes c t n n'
assumes "n' ≥ ⟨c ⇐ t⟩⇘n⇙"
and "∥c∥⇘t n'⇙"
shows "n' ≥ n"
using assms lNact_notActive leI by blast

lemma lNactLe[simp]:
fixes n n'
shows "⟨c ⇐ t⟩⇘n⇙ ≤ n"
using lNAct_ex less_or_eq_imp_le by blast

lemma lNactLe_nact:
fixes n n'
assumes "n'=n ∨ (n'<n ∧ (∄k. k≥n' ∧ k<n ∧ ∥c∥⇘t k⇙))"
shows "⟨c ⇐ t⟩⇘n⇙ ≤ n'"
using assms lNAct_def Least_le[of "λn'. n=n' ∨ (n'<n ∧ (∄k. k≥n' ∧ k<n ∧ ∥c∥⇘t k⇙))"] by auto

lemma lNact_active:
fixes cid t n
assumes "∀k<n. ∥cid∥⇘t k⇙"
shows "⟨cid ⇐ t⟩⇘n⇙ = n"
using assms lNAct_ex by blast

lemma nAct_mono_back:
fixes c t and n and n'
assumes "⟨c #⇘n'⇙ inf_llist t⟩ ≥ ⟨c #⇘n⇙ inf_llist t⟩"
shows "n'≥⟨c ⇐ t⟩⇘n⇙"
proof cases
assume "⟨c #⇘n'⇙ inf_llist t⟩ = ⟨c #⇘n⇙ inf_llist t⟩"
thus ?thesis
proof cases
assume "n'≥n"
thus ?thesis
by (rule order_trans[OF lNactLe])
next
assume "¬ n'≥n"
hence "n'<n" by simp
with ‹⟨c #⇘n'⇙ inf_llist t⟩ = ⟨c #⇘n⇙ inf_llist t⟩› have "∄k. k≥n' ∧ k<n ∧ ∥c∥⇘t k⇙"
by (metis enat_ord_simps(1) enat_ord_simps(2) nAct_same_not_active)
thus ?thesis using lNactLe_nact by (simp add: ‹n' < n›)
qed
next
assume "¬⟨c #⇘n'⇙ inf_llist t⟩ = ⟨c #⇘n⇙ inf_llist t⟩"
with assms have "⟨c #⇘enat n'⇙ inf_llist t⟩ > ⟨c #⇘enat n⇙ inf_llist t⟩" by simp
hence "n' > n" using nAct_strict_mono_back[of c "enat n" "inf_llist t" "enat n'"] by simp
thus ?thesis by (meson dual_order.strict_implies_order lNactLe le_trans)
qed

lemma nAct_mono_lNact:
assumes "⟨c ⇐ t⟩⇘n⇙ ≤ n'"
shows "⟨c #⇘n⇙ inf_llist t⟩ ≤ ⟨c #⇘n'⇙ inf_llist t⟩"
proof -
have "∄k. k≥⟨c ⇐ t⟩⇘n⇙ ∧ k<n ∧ ∥c∥⇘t k⇙" using lNact_notActive by auto
moreover have "enat n - 1 < llength (inf_llist t)" by (simp add: one_enat_def)
moreover from ‹⟨c ⇐ t⟩⇘n⇙ ≤ n'› have "enat ⟨c ⇐ t⟩⇘n⇙ ≤ enat n" by simp
ultimately have "⟨c #⇘n⇙ inf_llist t⟩=⟨c #⇘⟨c ⇐ t⟩⇘n⇙⇙ inf_llist t⟩" using nAct_not_active_same by simp
thus ?thesis using nAct_mono assms by simp
qed

subsection "Next Active"
text ‹
In the following, we introduce an operator to obtain the next point in time when a component is activated.
›

definition nxtAct :: "'id ⇒ (nat ⇒ cnf) ⇒ nat ⇒ nat" ("⟨_ → _⟩⇘_⇙")
where "⟨c → t⟩⇘n⇙ ≡ (THE n'. n'≥n ∧ ∥c∥⇘t n'⇙ ∧ (∄k. k≥n ∧ k<n' ∧ ∥c∥⇘t k⇙))"

lemma nxtActI:
fixes n::nat
and t::"nat ⇒ cnf"
and c::'id
assumes "∃i≥n. ∥c∥⇘t i⇙"
shows "⟨c → t⟩⇘n⇙ ≥ n ∧ ∥c∥⇘t ⟨c → t⟩⇘n⇙⇙ ∧ (∄k. k≥n ∧ k<⟨c → t⟩⇘n⇙ ∧ ∥c∥⇘t k⇙)"
proof -
let ?P = "THE n'. n'≥n ∧ ∥c∥⇘t n'⇙ ∧ (∄k. k≥n ∧ k<n' ∧ ∥c∥⇘t k⇙)"
from assms obtain i where "i≥n ∧ ∥c∥⇘t i⇙ ∧ (∄k. k≥n ∧ k<i ∧ ∥c∥⇘t k⇙)"
using lActive_least[of n "inf_llist