# Theory Sequence

(*  Title:       A Definitional Encoding of TLA in Isabelle/HOL
Authors:     Gudmund Grov <ggrov at inf.ed.ac.uk>
Stephan Merz <Stephan.Merz at loria.fr>
Year:        2011
Maintainer:  Gudmund Grov <ggrov at inf.ed.ac.uk>
*)

section ‹(Infinite) Sequences›

theory Sequence
imports Main
begin

text ‹
Lamport's Temporal Logic of Actions (TLA) is a linear-time temporal logic,
and its semantics is defined over infinite sequence of states, which we
simply represent by the type ‹'a seq›, defined as an abbreviation
for the type ‹nat ⇒ 'a›, where ‹'a› is the type of sequence
elements.

This theory defines some useful notions about such sequences, and in particular
concepts related to stuttering (finite repetitions of states), which are
important for the semantics of TLA. We identify a finite sequence with an
infinite sequence that ends in infinite stuttering. In this way, we avoid the
complications of having to handle both finite and infinite sequences of states:
see e.g. Devillers et al \cite{Devillers97} who discuss several variants of
representing possibly infinite sequences in HOL, Isabelle and PVS.
›

type_synonym 'a seq = "nat ⇒ 'a"

subsection "Some operators on sequences"

text ‹Some general functions on sequences are provided›

definition first :: "'a seq ⇒ 'a"
where "first s ≡ s 0"

definition second :: "('a seq) ⇒ 'a"
where "second s ≡ s 1"

definition suffix :: "'a seq ⇒ nat ⇒ 'a seq" (infixl "|⇩s" 60)
where "s |⇩s i ≡ λ n. s (n+i)"

definition tail :: "'a seq ⇒ 'a seq"
where "tail s ≡ s |⇩s 1"

definition
app :: "'a ⇒ ('a seq) ⇒ ('a seq)" (infixl "##" 60)
where
"s ## σ  ≡ λ n. if n=0 then s else σ (n - 1)"

text ‹
‹s |⇩s i› returns the suffix of sequence @{term s} from
index @{term i}.  @{term first} returns the first element of a sequence
while  @{term second} returns the second element. @{term tail} returns the
sequence starting at the second element. @{term "s ## σ"} prefixes the
sequence @{term σ} by element @{term s}.
›

subsubsection "Properties of @{term first} and @{term second}"

lemma first_tail_second: "first(tail s) = second s"
by (simp add: first_def second_def tail_def suffix_def)

subsubsection "Properties of @{term suffix}"

lemma suffix_first: "first (s |⇩s n) = s n"
by (auto simp add: suffix_def first_def)

lemma suffix_second: "second (s |⇩s n) = s (Suc n)"
by (auto simp add: suffix_def second_def)

lemma suffix_plus: "s |⇩s n |⇩s m = s |⇩s (m + n)"

lemma suffix_commute: "((s |⇩s n) |⇩s m) = ((s |⇩s m) |⇩s n)"

lemma suffix_plus_com: "s |⇩s m |⇩s n = s |⇩s (m + n)"
proof -
have "s |⇩s n |⇩s m = s |⇩s (m + n)" by (rule suffix_plus)
thus "s |⇩s m |⇩s n = s |⇩s (m + n)" by (simp add: suffix_commute)
qed

lemma suffix_zero[simp]: "s |⇩s 0 = s"
by (simp add: suffix_def)

lemma suffix_tail: "s |⇩s 1 = tail s"
by (simp add: tail_def)

lemma tail_suffix_suc: "s |⇩s (Suc n) = tail (s |⇩s n)"
by (simp add: suffix_def tail_def)

subsubsection "Properties of  @{term app}"

lemma seq_app_second: "(s ## σ) 1 = σ 0"
by (simp add: app_def)

lemma seq_app_first: "(s ## σ) 0 = s"
by (simp add: app_def)

lemma seq_app_first_tail: "(first s) ## (tail s) = s"
proof (rule ext)
fix x
show "(first s ## tail s) x = s x"
by (simp add: first_def app_def suffix_def tail_def)
qed

lemma seq_app_tail: "tail (x ## s) = s"
by (simp add: app_def tail_def suffix_def)

lemma seq_app_greater_than_zero: "n > 0 ⟹ (s ## σ) n = σ (n - 1)"
by (simp add: app_def)

subsection "Finite and Empty Sequences"

text‹
We identify finite and empty sequences and prove lemmas about them.
›

definition fin :: "('a seq) ⇒ bool"
where "fin s ≡ ∃ i. ∀ j ≥ i. s j = s i"

abbreviation inf :: "('a seq) ⇒ bool"
where "inf s ≡ ¬(fin s)"

definition last :: "('a seq) ⇒ nat"
where "last s ≡ LEAST i. (∀ j ≥ i. s j = s i)"

definition laststate :: "('a seq) ⇒ 'a"
where "laststate s ≡ s (last s)"

definition emptyseq :: "('a seq) ⇒ bool"
where "emptyseq ≡ λ s. ∀ i. s i = s 0"

abbreviation notemptyseq :: "('a seq) ⇒ bool"
where "notemptyseq s ≡ ¬(emptyseq s)"

text ‹
Predicate @{term fin} holds if there is an element
in the sequence such that all subsequent elements are identical,
i.e. the sequence is finite. @{term "last s"} returns the smallest index
from which on all elements of a finite sequence @{term s} are identical. Note that
if ‹s› is not finite then an arbitrary number is returned.
@{term laststate} returns the last element of a finite sequence. We assume
that the sequence is finite when using  @{term last} and  @{term laststate}.
Predicate @{term emptyseq} identifies empty sequences -- i.e. all states in
the sequence are identical to the initial one, while @{term notemptyseq} holds
if the given sequence is not empty.
›

subsubsection "Properties of @{term emptyseq}"

lemma empty_is_finite: assumes "emptyseq s" shows "fin s"
using assms by (auto simp: fin_def emptyseq_def)

lemma empty_suffix_is_empty: assumes H: "emptyseq s" shows "emptyseq (s |⇩s n)"
proof (clarsimp simp: emptyseq_def)
fix i
from H have "(s |⇩s n) i = s 0" by (simp add: emptyseq_def suffix_def)
moreover
from H have "(s |⇩s n) 0 = s 0" by (simp add: emptyseq_def suffix_def)
ultimately
show "(s |⇩s n) i = (s |⇩s n) 0" by simp
qed

lemma suc_empty: assumes H1: "emptyseq (s |⇩s m)" shows "emptyseq (s |⇩s (Suc m))"
proof -
from H1 have "emptyseq ((s |⇩s m) |⇩s 1)" by (rule empty_suffix_is_empty)
thus ?thesis by (simp add: suffix_plus)
qed

lemma empty_suffix_exteq: assumes H:"emptyseq s" shows "(s |⇩s n) m = s m"
proof (unfold suffix_def)
from H have "s (m+n) = s 0" by (simp add: emptyseq_def)
moreover
from H have "s m = s 0" by (simp add: emptyseq_def)
ultimately show "s (m + n) = s m" by simp
qed

lemma empty_suffix_eq: assumes H: "emptyseq s" shows "(s |⇩s n) = s"
proof (rule ext)
fix m
from H show "(s |⇩s n) m = s m" by (rule empty_suffix_exteq)
qed

lemma seq_empty_all: assumes H: "emptyseq s" shows "s i = s j"
proof -
from H have "s i = s 0" by (simp add: emptyseq_def)
moreover
from H have "s j = s 0" by (simp add: emptyseq_def)
ultimately
show ?thesis by simp
qed

subsubsection "Properties of @{term last} and @{term laststate}"

lemma fin_stut_after_last: assumes H: "fin s" shows "∀j ≥ last s. s j = s (last s)"
proof (clarify)
fix j
assume j: "j ≥ last s"
from H obtain i where "∀j ≥ i. s j = s i" (is "?P i") by (auto simp: fin_def)
hence "?P (last s)" unfolding last_def by (rule LeastI)
with j show "s j = s (last s)" by blast
qed

subsection "Stuttering Invariance"

text ‹
This subsection provides functions for removing stuttering
steps of sequences, i.e. we formalise Lamports ‹♮› operator.
Our formal definition is close to that of Wahab in the PVS prover.

The key novelty with the @{term "Sequence"} theory, is the treatment of
stuttering invariance, which enables verification of stuttering invariance of
the operators derived using it. Such proofs require comparing sequences
up to stuttering. Here, Lamport's \cite{Lamport94} method is used to
mechanise the equality of sequences up to stuttering: he defines
the ‹♮› operator, which collapses a sequence by removing
all stuttering steps, except possibly infinite stuttering at the end of the sequence.
These are left unchanged.
›

definition nonstutseq :: "('a seq) ⇒ bool"
where "nonstutseq s ≡ ∀ i. s i = s (Suc i) ⟶ (∀ j > i. s i = s j)"

definition stutstep :: "('a seq) ⇒ nat ⇒ bool"
where "stutstep s n ≡ (s n = s (Suc n))"

definition nextnat :: "('a seq) ⇒ nat"
where "nextnat s ≡ if emptyseq s then 0 else LEAST i. s i ≠ s 0"

definition nextsuffix :: "('a seq) ⇒ ('a seq)"
where "nextsuffix s ≡ s |⇩s (nextnat s)"

fun "next" :: "nat ⇒ ('a seq) ⇒ ('a seq)" where
"next 0 = id"
| "next (Suc n) = nextsuffix o (next n)"

definition collapse :: "('a seq) ⇒ ('a seq)" ("♮")
where "♮ s ≡ λ n. (next n s) 0"

text ‹
Predicate @{term nonstutseq} identifies sequences without any
stuttering steps -- except possibly for infinite stuttering at the end.
Further, @{term "stutstep s n"} is a predicate which holds if the element
after @{term "s n"} is equal to @{term "s n"}, i.e. @{term "Suc n"} is
a stuttering step.
@{term "collapse s"} formalises Lamports  @{term "♮"}
operator. It returns the first state of the result of @{term "next n s"}.
@{term "next n s"} finds suffix of the $n^{th}$ change. Hence the first
element, which @{term "♮ s"} returns, is the state after the $n^{th}$
change.  @{term "next n s"} is defined by primitive recursion on
@{term "n"} using function composition of function @{term nextsuffix}. E.g.
@{term "next 3 s"} equals @{term "nextsuffix (nextsuffix (nextsuffix s))"}.
@{term "nextsuffix s"} returns the suffix of the sequence starting at the
next changing state. It uses @{term "nextnat"} to obtain this. All the real
computation is done in this function. Firstly, an empty sequence will obviously
not contain any changes, and ‹0› is therefore returned. In this case
@{term "nextsuffix"} behaves like the identify function. If the sequence is not
empty then the smallest number @{term "i"} such that @{term "s i"} is different
from the initial state is returned. This is achieved by @{term "Least"}.
›

subsubsection "Properties of @{term nonstutseq}"

lemma seq_empty_is_nonstut:
assumes H: "emptyseq s" shows "nonstutseq s"
using H by (auto simp: nonstutseq_def seq_empty_all)

lemma notempty_exist_nonstut:
assumes H: "¬ emptyseq (s |⇩s m)" shows "∃ i. s i ≠ s m ∧ i > m"
using H proof (auto simp: emptyseq_def suffix_def)
fix i
assume i: "s (i + m) ≠ s m"
hence "i ≠ 0" by (intro notI, simp)
with i show ?thesis by auto
qed

subsubsection "Properties of @{term nextnat}"

lemma nextnat_le_unch: assumes H: "n < nextnat s" shows "s n = s 0"
proof (cases "emptyseq s")
assume "emptyseq s"
hence "nextnat s = 0" by (simp add: nextnat_def)
with H show ?thesis by auto
next
assume "¬ emptyseq s"
hence a1: "nextnat s = (LEAST i. s i ≠ s 0)" by (simp add: nextnat_def)
show ?thesis
proof (rule ccontr)
assume a2: "s n ≠ s 0" (is "?P n")
hence "(LEAST i. s i ≠ s 0) ≤ n" by (rule Least_le)
hence "¬(n < (LEAST i. s i ≠ s 0))" by auto
also from H a1 have "n < (LEAST i. s i ≠ s 0)" by simp
ultimately show False by auto
qed
qed

lemma stutnempty:
assumes H: "¬ stutstep s n" shows "¬ emptyseq (s |⇩s n)"
proof (unfold emptyseq_def suffix_def)
from H have "s (Suc n) ≠ s n" by (auto simp add: stutstep_def)
hence "s (1+n) ≠ s (0+n)" by simp
thus "¬(∀ i. s (i+n) = s (0+n))" by blast
qed

lemma notstutstep_nexnat1:
assumes H: "¬ stutstep s n" shows "nextnat (s |⇩s n) = 1"
proof -
from H have h': "nextnat (s |⇩s n) = (LEAST i. (s |⇩s n) i ≠ (s |⇩s n) 0)"
by (auto simp add: nextnat_def stutnempty)
from H have "s (Suc n) ≠ s n" by (auto simp add: stutstep_def)
hence "(s |⇩s n) 1 ≠ (s |⇩s n) 0" (is "?P 1") by (auto simp add: suffix_def)
hence "Least ?P ≤ 1" by (rule Least_le)
hence g1: "Least ?P = 0 ∨ Least ?P = 1" by auto
with h' have g1': "nextnat (s |⇩s n) = 0 ∨ nextnat (s |⇩s n) = 1" by auto
also have "nextnat (s |⇩s n) ≠ 0"
proof -
from H have "¬ emptyseq (s |⇩s n)" by (rule stutnempty)
then obtain i where "(s |⇩s n) i ≠  (s |⇩s n) 0" by (auto simp add: emptyseq_def)
hence "(s |⇩s n) (LEAST i. (s |⇩s n) i ≠ (s |⇩s n) 0) ≠ (s |⇩s n) 0" by (rule LeastI)
with h' have g2: "(s |⇩s n) (nextnat (s |⇩s n)) ≠ (s |⇩s n) 0" by auto
show "(nextnat (s |⇩s n)) ≠ 0"
proof
assume "(nextnat (s |⇩s n)) = 0"
with g2 show "False" by simp
qed
qed
ultimately show  "nextnat (s |⇩s n) = 1" by auto
qed

lemma stutstep_notempty_notempty:
assumes h1: "emptyseq (s |⇩s Suc n)" (is "emptyseq ?sn")
and h2: "stutstep s n"
shows "emptyseq (s |⇩s n)" (is "emptyseq ?s")
proof (auto simp: emptyseq_def)
fix k
show "?s k = ?s 0"
proof (cases k)
assume "k = 0" thus ?thesis by simp
next
fix m
assume k: "k = Suc m"
hence "?s k = ?sn m" by (simp add: suffix_def)
also from h1 have "... = ?sn 0" by (simp add: emptyseq_def)
also from h2 have "... = s n" by (simp add: suffix_def stutstep_def)
finally show ?thesis by (simp add: suffix_def)
qed
qed

lemma stutstep_empty_suc:
assumes "stutstep s n"
shows "emptyseq (s |⇩s Suc n) = emptyseq (s |⇩s n)"
using assms by (auto elim: stutstep_notempty_notempty suc_empty)

lemma stutstep_notempty_sucnextnat:
assumes h1: "¬ emptyseq  (s |⇩s n)" and h2: "stutstep s n"
shows "(nextnat (s |⇩s n)) = Suc (nextnat (s |⇩s (Suc n)))"
proof -
from h2 have g1: "¬(s (0+n) ≠ s (Suc n))" (is "¬ ?P 0") by (auto simp add: stutstep_def)
from h1 obtain i where "s (i+n) ≠ s n" by (auto simp: emptyseq_def suffix_def)
with h2 have g2: "s (i+n) ≠ s (Suc n)" (is "?P i") by (simp add: stutstep_def)
from g2 g1 have "(LEAST n. ?P n) = Suc (LEAST n. ?P (Suc n))" by (rule Least_Suc)
from g2 g1 have "(LEAST i. s (i+n) ≠ s (Suc n)) = Suc (LEAST i. s ((Suc i)+n) ≠ s (Suc n))"
by (rule Least_Suc)
hence G1: "(LEAST i. s (i+n) ≠ s (Suc n)) = Suc (LEAST i. s (i+Suc n) ≠ s (Suc n))" by auto
from h1 h2 have "¬ emptyseq  (s |⇩s Suc n)" by (simp add: stutstep_empty_suc)
hence "nextnat (s |⇩s Suc n) = (LEAST i. (s |⇩s Suc n) i ≠ (s |⇩s Suc n) 0)"
by (auto simp add: nextnat_def)
hence g1: "nextnat (s |⇩s Suc n) = (LEAST i. s (i+(Suc n)) ≠ s (Suc n))"
by (simp add: suffix_def)
from h1 have  "nextnat (s |⇩s n) = (LEAST i. (s |⇩s n) i ≠ (s |⇩s n) 0)"
by (auto simp add: nextnat_def)
hence g2: "nextnat (s |⇩s n) = (LEAST i. s (i+n) ≠ s n)" by (simp add: suffix_def)
with h2 have g2': "nextnat (s |⇩s n) = (LEAST i. s (i+n) ≠ s (Suc n))"
by (auto simp add: stutstep_def)
from G1 g1 g2' show ?thesis by auto
qed

lemma nextnat_empty_neq: assumes H: "¬ emptyseq s" shows "s (nextnat s) ≠ s 0"
proof -
from H have a1: "nextnat s =  (LEAST i. s i ≠ s 0)" by (simp add: nextnat_def)
from H obtain i where "s i ≠ s 0" by (auto simp: emptyseq_def)
hence "s (LEAST i. s i ≠ s 0) ≠ s 0" by (rule LeastI)
with a1 show ?thesis by auto
qed

lemma nextnat_empty_gzero: assumes H: "¬ emptyseq s" shows "nextnat s > 0"
proof -
from H have a1: "s (nextnat s) ≠ s 0" by (rule nextnat_empty_neq)
have "nextnat s ≠ 0"
proof
assume "nextnat s = 0"
with a1 show "False" by simp
qed
thus "nextnat s > 0" by simp
qed

subsubsection "Properties of @{term nextsuffix}"

lemma empty_nextsuffix:
assumes H: "emptyseq s" shows "nextsuffix s = s"
using H by (simp add: nextsuffix_def nextnat_def)

lemma empty_nextsuffix_id:
assumes H: "emptyseq s" shows "nextsuffix s = id s"
using H by (simp add: empty_nextsuffix)

lemma notstutstep_nextsuffix1:
assumes H: "¬ stutstep s n" shows "nextsuffix (s |⇩s n) = s |⇩s (Suc n)"
proof (unfold nextsuffix_def)
show "(s |⇩s n |⇩s (nextnat (s |⇩s n))) =  s |⇩s (Suc n)"
proof -
from H have  "nextnat (s |⇩s n) = 1" by (rule notstutstep_nexnat1)
hence "(s |⇩s n |⇩s (nextnat (s |⇩s n))) = s |⇩s n |⇩s 1" by auto
thus ?thesis by (simp add: suffix_def)
qed
qed

subsubsection "Properties of @{term next}"

lemma next_suc_suffix: "next (Suc n) s = nextsuffix (next n s)"
by simp

lemma next_suffix_com: "nextsuffix (next n s) = (next n (nextsuffix s))"
by (induct n, auto)

lemma next_plus: "next (m+n) s = next m (next n s)"
by (induct m, auto)

lemma next_empty: assumes H: "emptyseq s" shows "next n s = s"
proof (induct n)
from H show "next 0 s = s" by auto
next
fix n
assume a1: "next n s = s"
have "next (Suc n) s = nextsuffix (next n s)" by auto
with a1 have "next (Suc n) s = nextsuffix s" by simp
with H show "next (Suc n) s = s"
by (simp add: nextsuffix_def nextnat_def)
qed

lemma notempty_nextnotzero:
assumes H: "¬emptyseq s" shows "(next (Suc 0) s) 0 ≠ s 0"
proof -
from H have g1: "s (nextnat s) ≠ s 0" by (rule nextnat_empty_neq)
have "next (Suc 0) s = nextsuffix s" by auto
hence "(next (Suc 0) s) 0 =  s (nextnat s)" by (simp add: nextsuffix_def suffix_def)
with g1 show ?thesis by simp
qed

lemma next_ex_id: "∃ i. s i = (next m s) 0"
proof -
have "∃ i. (s |⇩s i) = (next m s)"
proof (induct m)
have "s |⇩s 0 = next 0 s" by simp
thus "∃ i. (s |⇩s i) = (next 0 s)" ..
next
fix m
assume a1: "∃ i. (s |⇩s i) = (next m s)"
then obtain i where a1': "(s |⇩s i) = (next m s)" ..
have "next (Suc m) s = nextsuffix (next m s)" by auto
hence "next (Suc m) s = (next m s) |⇩s (nextnat (next m s))" by (simp add: nextsuffix_def)
hence "∃ i. next (Suc m) s = (next m s) |⇩s i" ..
then obtain j where "next (Suc m) s = (next m s) |⇩s j" ..
with a1' have "next (Suc m) s = (s |⇩s i) |⇩s j" by simp
hence "next (Suc m) s = (s |⇩s (j+i))" by (simp add: suffix_plus)
hence "(s |⇩s (j+i)) = next (Suc m) s" by simp
thus "∃ i. (s |⇩s i) = (next (Suc m) s)" ..
qed
then obtain i where "(s |⇩s i) = (next m s)" ..
hence "(s |⇩s i) 0 = (next m s) 0" by auto
hence "s i = (next m s) 0" by (auto simp add: suffix_def)
thus ?thesis ..
qed

subsubsection "Properties of @{term collapse}"

lemma emptyseq_collapse_eq: assumes A1: "emptyseq s" shows "♮ s = s"
proof (unfold collapse_def, rule ext)
fix n
from A1 have "next n s = s" by (rule next_empty)
moreover
from A1 have "s n = s 0" by (simp add: emptyseq_def)
ultimately
show "(next n s) 0 = s n" by simp
qed

lemma empty_collapse_empty:
assumes H: "emptyseq s" shows "emptyseq (♮ s)"
using H by (simp add: emptyseq_collapse_eq)

lemma collapse_empty_empty:
assumes H: "emptyseq (♮ s)" shows "emptyseq s"
proof (rule ccontr)
assume a1: "¬emptyseq s"
from H have "∀ i. (next i s) 0 = s 0" by (simp add: collapse_def emptyseq_def)
moreover
from a1 have "(next (Suc 0) s) 0 ≠ s 0" by (rule notempty_nextnotzero)
ultimately show "False" by blast
qed

lemma collapse_empty_iff_empty [simp]: "emptyseq (♮ s) = emptyseq s"
by (auto elim: empty_collapse_empty collapse_empty_empty)

subsection "Similarity of Sequences"

text‹
Since adding or removing stuttering steps does not change the validity
of a stuttering-invarant formula, equality is often too strong,
and the weaker equality \emph{up to stuttering} is sufficient.
This is often called \emph{similarity} ($\approx$)
of sequences in the literature, and is required to
show that logical operators are stuttering invariant. This
is mechanised as:
›

definition seqsimilar :: "('a seq) ⇒ ('a seq) ⇒ bool" (infixl "≈" 50)
where "σ ≈ τ ≡ (♮ σ) = (♮ τ)"

subsubsection "Properties of @{term seqsimilar}"

lemma seqsim_refl [iff]: "s ≈ s"
by (simp add: seqsimilar_def)

lemma seqsim_sym: assumes H: "s ≈ t" shows "t ≈ s"
using H by (simp add: seqsimilar_def)

lemma seqeq_imp_sim: assumes H: "s = t" shows "s ≈ t"
using H by simp

lemma seqsim_trans [trans]: assumes h1: "s ≈ t" and h2: "t ≈ z" shows "s ≈ z"
using assms by (simp add: seqsimilar_def)

theorem sim_first: assumes H: "s ≈ t" shows "first s = first t"
proof -
from H have "(♮ s) 0 = (♮ t) 0" by (simp add: seqsimilar_def)
thus ?thesis by (simp add: collapse_def first_def)
qed

lemmas sim_first2 = sim_first[unfolded first_def]

lemma tail_sim_second: assumes H: "tail s ≈ tail t" shows "second s = second t"
proof -
from H have "first (tail s) = first (tail t)" by (simp add: sim_first)
thus "second s = second t" by (simp add: first_tail_second)
qed

lemma seqsimilarI:
assumes 1: "first s = first t" and 2: "nextsuffix s ≈ nextsuffix t"
shows "s ≈ t"
unfolding seqsimilar_def collapse_def
proof
fix n
show "next n s 0 = next n t 0"
proof (cases n)
assume "n = 0"
with 1 show ?thesis by (simp add: first_def)
next
fix m
assume m: "n = Suc m"
from 2 have "next m (nextsuffix s) 0 =  next m (nextsuffix t) 0"
unfolding seqsimilar_def collapse_def by (rule fun_cong)
with m show ?thesis by (simp add: next_suffix_com)
qed
qed

lemma seqsim_empty_empty:
assumes H1: "s ≈ t" and H2: "emptyseq s" shows "emptyseq t"
proof -
from H2 have "emptyseq (♮ s)" by simp
with H1 have "emptyseq (♮ t)" by (simp add: seqsimilar_def)
thus ?thesis by simp
qed

lemma seqsim_empty_iff_empty:
assumes H: "s ≈ t" shows "emptyseq s = emptyseq t"
proof
assume "emptyseq s" with H show "emptyseq t" by (rule seqsim_empty_empty)
next
assume t: "emptyseq t"
from H have "t ≈ s" by (rule seqsim_sym)
from this t show "emptyseq s" by (rule seqsim_empty_empty)
qed

lemma seq_empty_eq:
assumes H1: "s 0 = t 0" and H2: "emptyseq s" and H3: "emptyseq t"
shows "s = t"
proof (rule ext)
fix n
from assms have "t n = s n" by (auto simp: emptyseq_def)
thus "s n = t n" by simp
qed

lemma seqsim_notstutstep:
assumes H: "¬ (stutstep s n)" shows "(s |⇩s (Suc n)) ≈ nextsuffix (s |⇩s n)"
using H by (simp add: notstutstep_nextsuffix1)

lemma stut_nextsuf_suc:
assumes H: "stutstep s n" shows "nextsuffix (s |⇩s n) = nextsuffix (s |⇩s (Suc n))"
proof (cases "emptyseq (s |⇩s n)")
case True
hence g1: "nextsuffix (s |⇩s n) = (s |⇩s n)" by (simp add: nextsuffix_def nextnat_def)
from True have g2: "nextsuffix (s |⇩s Suc n) = (s |⇩s Suc n)"
by (simp add: suc_empty nextsuffix_def nextnat_def)
have "(s |⇩s n) = (s |⇩s Suc n)"
proof
fix x
from True have "s (x + n) = s (0 + n)" "s (Suc x + n) = s (0 + n)"
unfolding emptyseq_def suffix_def by (blast+)
thus "(s |⇩s n) x = (s |⇩s Suc n) x" by (simp add: suffix_def)
qed
with g1 g2 show ?thesis by auto
next
case False
with H have "(nextnat (s |⇩s n)) = Suc (nextnat (s |⇩s Suc n))"
by (simp add: stutstep_notempty_sucnextnat)
thus ?thesis
by (simp add: nextsuffix_def suffix_plus)
qed

lemma seqsim_suffix_seqsim:
assumes H: "s ≈ t" shows "nextsuffix s ≈ nextsuffix t"
unfolding seqsimilar_def collapse_def
proof
fix n
from H have "(next (Suc n) s) 0 = (next (Suc n) t) 0"
unfolding seqsimilar_def collapse_def by (rule fun_cong)
thus "next n (nextsuffix s) 0 = next n (nextsuffix t) 0"
by (simp add: next_suffix_com)
qed

lemma seqsim_stutstep:
assumes H: "stutstep s n" shows "(s |⇩s (Suc n)) ≈ (s |⇩s n)" (is "?sn ≈ ?s")
unfolding seqsimilar_def collapse_def
proof
fix m
show "next m (s |⇩s Suc n) 0 = next m (s |⇩s n) 0"
proof (cases m)
assume "m=0"
with H show ?thesis by (simp add: suffix_def stutstep_def)
next
fix k
assume m: "m = Suc k"
with H  have "next m (s |⇩s Suc n) = next k (nextsuffix  (s |⇩s n))"
by (simp add: stut_nextsuf_suc next_suffix_com)
moreover from m have "next m (s |⇩s n) = next k (nextsuffix  (s |⇩s n))"
by (simp add: next_suffix_com)
ultimately show "next m (s |⇩s Suc n) 0 = next m (s |⇩s n) 0" by simp
qed
qed

lemma addfeqstut: "stutstep ((first t) ## t) 0"
by (simp add: first_def stutstep_def app_def suffix_def)

lemma addfeqsim: "((first t) ## t) ≈ t"
proof -
have "stutstep ((first t) ## t) 0" by (rule addfeqstut)
hence "(((first t) ## t) |⇩s (Suc 0)) ≈ (((first t) ## t) |⇩s 0)" by (rule seqsim_stutstep)
hence "tail ((first t) ## t) ≈ ((first t) ## t)" by (simp add: suffix_def tail_def)
hence "t ≈ ((first t) ## t)" by (simp add: tail_def app_def suffix_def)
thus ?thesis by (rule seqsim_sym)
qed

assumes H: "first s = second s" shows "s ≈ tail s"
proof -
have g1: "(first s) ## (tail s) = s" by (rule seq_app_first_tail)
from H have "(first s) = first (tail s)"
by (simp add: first_def second_def tail_def suffix_def)
hence "(first s) ## (tail s) ≈ (tail s)" by (simp add: addfeqsim)
with g1 show ?thesis by simp
qed

lemma app_seqsimilar:
assumes h1: "s ≈ t" shows "(x ## s) ≈ (x ## t)"
proof (cases "stutstep (x ## s) 0")
case True
from h1 have "first s = first t" by (rule sim_first)
with True have a2: "stutstep (x ## t) 0"
by (simp add: stutstep_def first_def app_def)
from True have "((x ## s) |⇩s (Suc 0)) ≈ ((x ## s) |⇩s 0)" by (rule seqsim_stutstep)
hence "tail (x ## s) ≈ (x ## s)" by (simp add: tail_def suffix_def)
hence g1: "s ≈ (x ## s)" by (simp add: app_def tail_def suffix_def)
from a2 have "((x ## t) |⇩s (Suc 0)) ≈ ((x ## t) |⇩s 0)" by (rule seqsim_stutstep)
hence "tail (x ## t) ≈ (x ## t)" by (simp add: tail_def suffix_def)
hence g2: "t ≈ (x ## t)" by (simp add: app_def tail_def suffix_def)
from h1 g2 have "s ≈ (x ## t)" by (rule seqsim_trans)
from this[THEN seqsim_sym] g1 show "(x ## s) ≈ (x ## t)"
by (rule seqsim_sym[OF seqsim_trans])
next
case False
from h1 have "first s = first t" by (rule sim_first)
with False have a2: "¬ stutstep (x ## t) 0"
by (simp add: stutstep_def first_def app_def)
from False have "((x ## s) |⇩s (Suc 0)) ≈ nextsuffix ((x ## s) |⇩s 0)"
by (rule seqsim_notstutstep)
hence "(tail (x ## s)) ≈ nextsuffix (x ## s)"
by (simp add: tail_def)
hence g1: "s ≈ nextsuffix (x ## s)" by (simp add: seq_app_tail)
from a2 have "((x ## t) |⇩s (Suc 0)) ≈ nextsuffix ((x ## t) |⇩s 0)"
by (rule seqsim_notstutstep)
hence "(tail (x ## t)) ≈ nextsuffix (x ## t)" by (simp add: tail_def)
hence g2: "t ≈ nextsuffix (x ## t)" by (simp add: seq_app_tail)
with h1 have "s ≈ nextsuffix (x ## t)" by (rule seqsim_trans)
from this[THEN seqsim_sym] g1 have g3: "nextsuffix (x ## s) ≈ nextsuffix (x ## t)"
by (rule seqsim_sym[OF seqsim_trans])
have "first (x ## s) = first (x ## t)" by (simp add: first_def app_def)
from this g3 show ?thesis by (rule seqsimilarI)
qed

text ‹
If two sequences are similar then for any suffix of one of them there
exists a similar suffix of the other one. We will prove a stronger
result below.
›

lemma simstep_disj1: assumes H: "s ≈ t" shows "∃ m. ((s |⇩s n) ≈ (t |⇩s m))"
proof (induct n)
from H have "((s |⇩s 0) ≈ (t |⇩s 0))" by auto
thus "∃ m. ((s |⇩s 0) ≈ (t |⇩s m))" ..
next
fix n
assume "∃ m. ((s |⇩s n) ≈ (t |⇩s m))"
then obtain m where a1': "(s |⇩s n) ≈ (t |⇩s m)" ..
show "∃ m. ((s |⇩s (Suc n)) ≈ (t |⇩s m))"
proof (cases "stutstep s n")
case True
hence "(s |⇩s (Suc n)) ≈ (s |⇩s n)" by (rule seqsim_stutstep)
from this a1' have "((s |⇩s (Suc n)) ≈ (t |⇩s m))" by (rule seqsim_trans)
thus ?thesis ..
next
case False
hence "(s |⇩s (Suc n)) ≈ nextsuffix (s |⇩s n)" by (rule seqsim_notstutstep)
moreover
from a1' have "nextsuffix (s |⇩s n) ≈ nextsuffix (t |⇩s m)"
by (simp add: seqsim_suffix_seqsim)
ultimately have "(s |⇩s (Suc n)) ≈ nextsuffix (t |⇩s m)" by (rule seqsim_trans)
hence "(s |⇩s (Suc n)) ≈ t |⇩s (m + (nextnat (t |⇩s m)))"
by (simp add: nextsuffix_def suffix_plus_com)
thus "∃ m. (s |⇩s (Suc n)) ≈ t |⇩s m" ..
qed
qed

lemma nextnat_le_seqsim:
assumes n: "n < nextnat s" shows "s ≈ (s |⇩s n)"
proof (cases "emptyseq s")
case True   ― ‹case impossible›
with n show ?thesis by (simp add: nextnat_def)
next
case False
from n show ?thesis
proof (induct n)
show "s ≈ (s |⇩s 0)" by simp
next
fix n
assume a2: "n < nextnat s ⟹ s ≈ (s |⇩s n)" and a3: "Suc n < nextnat s"
from a3 have g1: "s (Suc n) = s 0" by (rule nextnat_le_unch)
from a3 have a3': "n < nextnat s" by simp
hence "s n = s 0" by (rule nextnat_le_unch)
with g1 have "stutstep s n" by (simp add: stutstep_def)
hence g2: "(s |⇩s n) ≈ (s |⇩s (Suc n))" by (rule seqsim_stutstep[THEN seqsim_sym])
with a3' a2 show "s ≈ (s |⇩s (Suc n))" by (auto elim: seqsim_trans)
qed
qed

lemma seqsim_prev_nextnat: "s ≈ s |⇩s ((nextnat s) - 1)"
proof (cases "emptyseq s")
case True
hence "s |⇩s ((nextnat s)-(1::nat)) = s |⇩s 0" by (simp add: nextnat_def)
thus ?thesis by simp
next
case False
hence "nextnat s > 0" by (rule nextnat_empty_gzero)
thus ?thesis by (simp add: nextnat_le_seqsim)
qed

text ‹
Given a suffix ‹s |⇩s n› of some sequence ‹s› that is
similar to some suffix ‹t |⇩s m› of sequence ‹t›, there
exists some suffix ‹t |⇩s m'› of ‹t› such that
‹s |⇩s n› and ‹t |⇩s m'› are similar and also
‹s |⇩s (n+1)› is similar to either ‹t |⇩s m'› or to
‹t |⇩s (m'+1)›.
›

lemma seqsim_suffix_suc:
assumes H: "s |⇩s n ≈ t |⇩s m"
shows "∃m'. s |⇩s n ≈ t |⇩s m' ∧ ((s |⇩s Suc n ≈ t |⇩s Suc m') ∨ (s |⇩s Suc n ≈ t |⇩s m'))"
proof (cases "stutstep s n")
case True
hence "s |⇩s Suc n ≈ s |⇩s n" by (rule seqsim_stutstep)
from this H have "s |⇩s Suc n ≈ t |⇩s m" by (rule seqsim_trans)
with H show ?thesis by blast
next
case False
hence "¬ emptyseq (s |⇩s n)" by (rule stutnempty)
with H have a2: "¬ emptyseq (t |⇩s m)" by (simp add: seqsim_empty_iff_empty)
hence g4: "nextsuffix (t |⇩s m) = (t |⇩s m) |⇩s Suc (nextnat (t |⇩s m) - 1)"
by (simp add: nextnat_empty_gzero nextsuffix_def)
have g3: "(t |⇩s m) ≈ (t |⇩s m) |⇩s (nextnat (t |⇩s m) - 1)"
by (rule seqsim_prev_nextnat)
with H have G1: "s |⇩s n ≈ (t |⇩s m) |⇩s (nextnat (t |⇩s m) - 1)"
by (rule seqsim_trans)
from False have G1': "(s |⇩s Suc n) = nextsuffix (s |⇩s n)"
by (rule notstutstep_nextsuffix1[THEN sym])
from H have "nextsuffix (s |⇩s n) ≈ nextsuffix (t |⇩s m)"
by (rule seqsim_suffix_seqsim)
with G1 G1' g4
have "s |⇩s n ≈ t |⇩s (m + (nextnat (t |⇩s m) - 1))
∧ s |⇩s (Suc n) ≈ t |⇩s Suc (m + (nextnat (t |⇩s m) - 1))"
by (simp add: suffix_plus_com)
thus ?thesis by blast
qed

text ‹
The following main result about similar sequences shows that if
‹s ≈ t› holds then for any suffix ‹s |⇩s n› of ‹s›
there exists a suffix ‹t |⇩s m› such that
\begin{itemize}
\item ‹s |⇩s n› and ‹t |⇩s m› are similar, and
\item ‹s |⇩s (n+1)› is similar to either ‹t |⇩s (m+1)›
or ‹t |⇩s m›.
\end{itemize}
The idea is to pick the largest ‹m› such that ‹s |⇩s n ≈ t |⇩s m›
(or some such ‹m› if ‹s |⇩s n› is empty).
›

theorem sim_step:
assumes H: "s ≈ t"
shows "∃ m. s |⇩s n ≈ t |⇩s m ∧
((s |⇩s Suc n ≈ t |⇩s Suc m) ∨ (s |⇩s Suc n ≈ t |⇩s m))"
(is "∃m. ?Sim n m")
proof (induct n)
from H have "s |⇩s 0 ≈ t |⇩s 0" by simp
thus "∃ m. ?Sim 0 m" by (rule seqsim_suffix_suc)
next
fix n
assume "∃ m. ?Sim n m"
hence "∃k. s |⇩s Suc n ≈ t |⇩s k" by blast
thus "∃ m. ?Sim (Suc n) m" by (blast dest: seqsim_suffix_suc)
qed

end


# Theory Intensional

(*  Title:       A Definitional Encoding of TLA in Isabelle/HOL
Authors:     Gudmund Grov <ggrov at inf.ed.ac.uk>
Stephan Merz <Stephan.Merz at loria.fr>
Year:        2011
Maintainer:  Gudmund Grov <ggrov at inf.ed.ac.uk>
*)

section ‹Representing Intensional Logic›

theory Intensional
imports Main
begin

text‹
In higher-order logic, every proof rule has a corresponding tautology, i.e.
the \emph{deduction theorem} holds. Isabelle/HOL implements this since object-level
implication ($\longrightarrow$) and meta-level entailment ($\Longrightarrow$)
commute, viz. the proof rule ‹impI:› @{thm impI}.
However, the deduction theorem does not hold for
most modal and temporal logics \cite[page 95]{Lamport02}\cite{Merz98}.
For example $A \vdash \Box A$ holds, meaning that if $A$ holds in any world, then
it always holds. However, $\vdash A \longrightarrow \Box A$, stating that
$A$ always holds if it initially holds, is not valid.

Merz  \cite{Merz98} overcame this problem by creating an
@{term Intensional} logic. It exploits Isabelle's
axiomatic type class feature  \cite{Wenzel00b} by creating a type
class @{term world}, which provides Skolem constants to associate formulas
with the world they hold in. The class is trivial, not requiring any axioms.
›

class world
text ‹
@{term world} is a type class of possible worlds. It is a subclass
of all HOL types @{term type}. No axioms are provided, since its only
purpose is to avoid silly use of the @{term Intensional} syntax.
›

subsection‹Abstract Syntax and Definitions›

type_synonym ('w,'a) expr = "'w ⇒ 'a"
type_synonym  'w form = "('w, bool) expr"

text ‹The intention is that @{typ 'a} will be used for unlifted
types (class @{term type}), while @{typ 'w} is lifted (class @{term world}).
›

definition Valid :: "('w::world) form ⇒ bool"
where "Valid A ≡ ∀w. A w"

definition const :: "'a ⇒ ('w::world, 'a) expr"
where unl_con: "const c w ≡ c"

definition lift :: "['a ⇒ 'b, ('w::world, 'a) expr] ⇒ ('w,'b) expr"
where unl_lift: "lift f x w ≡ f (x w)"

definition lift2 :: "['a ⇒ 'b ⇒ 'c, ('w::world,'a) expr, ('w,'b) expr] ⇒ ('w,'c) expr"
where unl_lift2: "lift2 f x y w ≡ f (x w) (y w)"

definition lift3 :: "['a ⇒ 'b => 'c ⇒ 'd, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr] ⇒ ('w,'d) expr"
where unl_lift3: "lift3 f x y z w ≡ f (x w) (y w) (z w)"

definition lift4 :: "['a ⇒ 'b => 'c ⇒ 'd ⇒ 'e, ('w::world,'a) expr, ('w,'b) expr, ('w,'c) expr,('w,'d) expr] ⇒ ('w,'e) expr"
where unl_lift4: "lift4 f x y z zz w ≡ f (x w) (y w) (z w) (zz w)"

text ‹
@{term "Valid F"} asserts that the lifted formula @{term F} holds everywhere.
@{term const} allows lifting of a constant, while @{term lift} through
@{term lift4} allow functions with arity 1--4 to be lifted. (Note that there
is no way to define a generic lifting operator for functions of arbitrary arity.)
›

definition RAll :: "('a ⇒ ('w::world) form) ⇒ 'w form"  (binder "Rall " 10)
where unl_Rall: "(Rall x. A x) w ≡ ∀x. A x w"

definition REx :: "('a ⇒ ('w::world) form) ⇒ 'w form"  (binder "Rex " 10)
where unl_Rex: "(Rex x. A x) w ≡ ∃x. A x w"

definition REx1 :: "('a ⇒ ('w::world) form) ⇒ 'w form"  (binder "Rex! " 10)
where unl_Rex1: "(Rex! x. A x) w ≡ ∃!x. A x w"

text ‹
@{term RAll}, @{term REx} and @{term REx1} introduces rigid'' quantification
over values (of non-world types) within intensional'' formulas. @{term RAll}
is universal quantification, @{term REx} is existential quantifcation.
@{term REx1} requires unique existence.
›

text ‹
We declare the unlifting rules'' as rewrite rules that will be applied
automatically.
›

lemmas intensional_rews[simp] =
unl_con unl_lift unl_lift2 unl_lift3 unl_lift4
unl_Rall unl_Rex unl_Rex1

subsection‹Concrete Syntax›

nonterminal
lift and liftargs

text‹
The non-terminal @{term lift} represents lifted expressions. The idea is to use
Isabelle's macro mechanism to convert between the concrete and abstract syntax.
›

syntax
""            :: "id ⇒ lift"                          ("_")
""            :: "longid ⇒ lift"                      ("_")
""            :: "var ⇒ lift"                         ("_")
"_applC"      :: "[lift, cargs] ⇒ lift"               ("(1_/ _)" [1000, 1000] 999)
""            :: "lift ⇒ lift"                        ("'(_')")
"_lambda"     :: "[idts, 'a] ⇒ lift"                  ("(3%_./ _)" [0, 3] 3)
"_constrain"  :: "[lift, type] ⇒ lift"                ("(_::_)" [4, 0] 3)
""            :: "lift ⇒ liftargs"                    ("_")
"_liftargs"   :: "[lift, liftargs] ⇒ liftargs"        ("_,/ _")
"_Valid"      :: "lift ⇒ bool"                        ("(⊢ _)" 5)
"_holdsAt"    :: "['a, lift] ⇒ bool"                  ("(_ ⊨ _)" [100,10] 10)

(* Syntax for lifted expressions outside the scope of ⊢ or ⊨.*)
"LIFT"        :: "lift ⇒ 'a"                          ("LIFT _")

(* generic syntax for lifted constants and functions *)
"_const"      :: "'a ⇒ lift"                          ("(#_)" [1000] 999)
"_lift"       :: "['a, lift] ⇒ lift"                  ("(_<_>)" [1000] 999)
"_lift2"      :: "['a, lift, lift] ⇒ lift"            ("(_<_,/ _>)" [1000] 999)
"_lift3"      :: "['a, lift, lift, lift] ⇒ lift"      ("(_<_,/ _,/ _>)" [1000] 999)
"_lift4"      :: "['a, lift, lift, lift,lift] ⇒ lift"      ("(_<_,/ _,/ _,/ _>)" [1000] 999)

(* concrete syntax for common infix functions: reuse same symbol *)
"_liftEqu"    :: "[lift, lift] ⇒ lift"                ("(_ =/ _)" [50,51] 50)
"_liftNeq"    :: "[lift, lift] ⇒ lift"                (infixl "≠" 50)
"_liftNot"    :: "lift ⇒ lift"                        ("¬ _" [90] 90)
"_liftAnd"    :: "[lift, lift] ⇒ lift"                (infixr "∧" 35)
"_liftOr"     :: "[lift, lift] ⇒ lift"                (infixr "∨" 30)
"_liftImp"    :: "[lift, lift] ⇒ lift"                (infixr "⟶" 25)
"_liftIf"     :: "[lift, lift, lift] ⇒ lift"          ("(if (_)/ then (_)/ else (_))" 10)
"_liftPlus"   :: "[lift, lift] ⇒ lift"                ("(_ +/ _)" [66,65] 65)
"_liftMinus"  :: "[lift, lift] ⇒ lift"                ("(_ -/ _)" [66,65] 65)
"_liftTimes"  :: "[lift, lift] ⇒ lift"                ("(_ */ _)" [71,70] 70)
"_liftDiv"    :: "[lift, lift] ⇒ lift"                ("(_ div _)" [71,70] 70)
"_liftMod"    :: "[lift, lift] ⇒ lift"                ("(_ mod _)" [71,70] 70)
"_liftLess"   :: "[lift, lift] ⇒ lift"                ("(_/ < _)"  [50, 51] 50)
"_liftLeq"    :: "[lift, lift] ⇒ lift"                ("(_/ ≤ _)" [50, 51] 50)
"_liftMem"    :: "[lift, lift] ⇒ lift"                ("(_/ ∈ _)" [50, 51] 50)
"_liftNotMem" :: "[lift, lift] ⇒ lift"                ("(_/ ∉ _)" [50, 51] 50)
"_liftFinset" :: "liftargs => lift"                    ("{(_)}")
(** TODO: syntax for lifted collection / comprehension **)
"_liftPair"   :: "[lift,liftargs] ⇒ lift"                   ("(1'(_,/ _'))")
(* infix syntax for list operations *)
"_liftCons" :: "[lift, lift] ⇒ lift"                  ("(_ #/ _)" [65,66] 65)
"_liftApp"  :: "[lift, lift] ⇒ lift"                  ("(_ @/ _)" [65,66] 65)
"_liftList" :: "liftargs ⇒ lift"                      ("[(_)]")

(* Rigid quantification (syntax level) *)
"_ARAll"  :: "[idts, lift] ⇒ lift"                    ("(3! _./ _)" [0, 10] 10)
"_AREx"   :: "[idts, lift] ⇒ lift"                    ("(3? _./ _)" [0, 10] 10)
"_AREx1"  :: "[idts, lift] ⇒ lift"                    ("(3?! _./ _)" [0, 10] 10)
"_RAll"       :: "[idts, lift] ⇒ lift"                ("(3∀_./ _)" [0, 10] 10)
"_REx"        :: "[idts, lift] ⇒ lift"                ("(3∃_./ _)" [0, 10] 10)
"_REx1"       :: "[idts, lift] ⇒ lift"                ("(3∃!_./ _)" [0, 10] 10)

translations
"_const"        ⇌  "CONST const"

translations
"_lift"         ⇌ "CONST lift"
"_lift2"        ⇌ "CONST lift2"
"_lift3"        ⇌ "CONST lift3"
"_lift4"        ⇌ "CONST lift4"
"_Valid"        ⇌ "CONST Valid"

translations
"_RAll x A"     ⇌ "Rall x. A"
"_REx x A"      ⇌ "Rex x. A"
"_REx1 x A"     ⇌ "Rex! x. A"

translations
"_ARAll"        ⇀  "_RAll"
"_AREx"         ⇀ "_REx"
"_AREx1"        ⇀ "_REx1"

"w ⊨ A"        ⇀ "A w"
"LIFT A"        ⇀ "A::_⇒_"

translations
"_liftEqu"      ⇌ "_lift2 (=)"
"_liftNeq u v"  ⇌ "_liftNot (_liftEqu u v)"
"_liftNot"      ⇌ "_lift (CONST Not)"
"_liftAnd"      ⇌ "_lift2 (&)"
"_liftOr"       ⇌ "_lift2 ((|) )"
"_liftImp"      ⇌ "_lift2 (-->)"
"_liftIf"       ⇌ "_lift3 (CONST If)"
"_liftPlus"     ⇌ "_lift2 (+)"
"_liftMinus"    ⇌ "_lift2 (-)"
"_liftTimes"    ⇌ "_lift2 (*)"
"_liftDiv"      ⇌ "_lift2 (div)"
"_liftMod"      ⇌ "_lift2 (mod)"
"_liftLess"     ⇌ "_lift2 (<)"
"_liftLeq"      ⇌ "_lift2 (<=)"
"_liftMem"      ⇌ "_lift2 (:)"
"_liftNotMem x xs"             ⇌ "_liftNot (_liftMem x xs)"

translations
"_liftFinset (_liftargs x xs)" ⇌ "_lift2 (CONST insert) x (_liftFinset xs)"
"_liftFinset x"                ⇌ "_lift2 (CONST insert) x (_const (CONST Set.empty))"
"_liftPair x (_liftargs y z)"  ⇌ "_liftPair x (_liftPair y z)"
"_liftPair"                    ⇌ "_lift2 (CONST Pair)"
"_liftCons"                    ⇌ "_lift2 (CONST Cons)"
"_liftApp"                     ⇌ "_lift2 (@)"
"_liftList (_liftargs x xs)"   ⇌ "_liftCons x (_liftList xs)"
"_liftList x"                  ⇌ "_liftCons x (_const [])"

"w ⊨ ¬ A" ↽ "_liftNot A w"
"w ⊨ A ∧ B" ↽ "_liftAnd A B w"
"w ⊨ A ∨ B" ↽ "_liftOr A B w"
"w ⊨ A ⟶ B" ↽ "_liftImp A B w"
"w ⊨ u = v" ↽ "_liftEqu u v w"
"w ⊨ ∀x. A" ↽ "_RAll x A w"
"w ⊨ ∃x. A" ↽ "_REx x A w"
"w ⊨ ∃!x. A" ↽ "_REx1 x A w"

syntax (ASCII)
"_Valid"      :: "lift ⇒ bool"                        ("(|- _)" 5)
"_holdsAt"    :: "['a, lift] ⇒ bool"                  ("(_ |= _)" [100,10] 10)
"_liftNeq"    :: "[lift, lift] ⇒ lift"                ("(_ ~=/ _)" [50,51] 50)
"_liftNot"    :: "lift ⇒ lift"                        ("(~ _)" [90] 90)
"_liftAnd"    :: "[lift, lift] ⇒ lift"                ("(_ &/ _)" [36,35] 35)
"_liftOr"     :: "[lift, lift] ⇒ lift"                ("(_ |/ _)" [31,30] 30)
"_liftImp"    :: "[lift, lift] ⇒ lift"                ("(_ -->/ _)" [26,25] 25)
"_liftLeq"    :: "[lift, lift] ⇒ lift"                ("(_/ <= _)" [50, 51] 50)
"_liftMem"    :: "[lift, lift] ⇒ lift"                ("(_/ : _)" [50, 51] 50)
"_liftNotMem" :: "[lift, lift] ⇒ lift"                ("(_/ ~: _)" [50, 51] 50)
"_RAll" :: "[idts, lift] ⇒ lift"                      ("(3ALL _./ _)" [0, 10] 10)
"_REx"  :: "[idts, lift] ⇒ lift"                      ("(3EX _./ _)" [0, 10] 10)
"_REx1" :: "[idts, lift] ⇒ lift"                      ("(3EX! _./ _)" [0, 10] 10)

subsection ‹Lemmas and Tactics›

lemma intD[dest]: "⊢ A ⟹ w ⊨ A"
proof -
assume a:"⊢ A"
from a have "∀w. w ⊨ A" by (auto simp add: Valid_def)
thus ?thesis ..
qed

lemma intI [intro!]: assumes P1:"(⋀ w. w ⊨ A)" shows "⊢ A"
using assms by (auto simp: Valid_def)

text‹
Basic unlifting introduces a parameter @{term w} and applies basic rewrites, e.g
@{term "⊢ F = G"} becomes @{term "F w = G w"} and @{term "⊢ F ⟶ G"} becomes
@{term "F w ⟶ G w"}.
›

method_setup int_unlift = ‹
Scan.succeed (fn ctxt => SIMPLE_METHOD'
(resolve_tac ctxt @{thms intI} THEN' rewrite_goal_tac ctxt @{thms intensional_rews}))
› "method to unlift and followed by intensional rewrites"

lemma inteq_reflection: assumes P1: "⊢ x=y" shows  "(x ≡ y)"
proof -
from P1 have P2: "∀w. x w = y w" by (unfold Valid_def unl_lift2)
hence P3:"x=y" by blast
thus "x ≡ y" by (rule "eq_reflection")
qed

lemma int_simps:
"⊢ (x=x) = #True"
"⊢ (¬ #True) = #False"
"⊢ (¬ #False) = #True"
"⊢ (¬¬ P) = P"
"⊢ ((¬ P) = P) = #False"
"⊢ (P = (¬P)) = #False"
"⊢ (P ≠ Q) = (P = (¬ Q))"
"⊢ (#True=P) = P"
"⊢ (P=#True) = P"
"⊢ (#True ⟶ P) = P"
"⊢ (#False ⟶ P) = #True"
"⊢ (P ⟶ #True) = #True"
"⊢ (P ⟶ P) = #True"
"⊢ (P ⟶ #False) = (¬P)"
"⊢ (P ⟶ ~P) = (¬P)"
"⊢ (P ∧ #True) = P"
"⊢ (#True ∧ P) = P"
"⊢ (P ∧ #False) = #False"
"⊢ (#False ∧ P) = #False"
"⊢ (P ∧ P) = P"
"⊢ (P ∧ ~P) = #False"
"⊢ (¬P ∧ P) = #False"
"⊢ (P ∨ #True) = #True"
"⊢ (#True ∨ P) = #True"
"⊢ (P ∨ #False) = P"
"⊢ (#False ∨ P) = P"
"⊢ (P ∨ P) = P"
"⊢ (P ∨ ¬P) = #True"
"⊢ (¬P ∨ P) = #True"
"⊢ (∀ x. P) = P"
"⊢ (∃ x. P) = P"
by auto

lemmas intensional_simps[simp] = int_simps[THEN inteq_reflection]

method_setup int_rewrite = ‹
Scan.succeed (fn ctxt => SIMPLE_METHOD' (rewrite_goal_tac ctxt @{thms intensional_simps}))
› "rewrite method at intensional level"

lemma Not_Rall: "⊢ (¬(∀ x. F x)) = (∃ x. ¬F x)"
by auto

lemma Not_Rex: "⊢ (¬(∃ x. F x)) = (∀ x. ¬F x)"
by auto

lemma TrueW [simp]: "⊢ #True"
by auto

lemma int_eq: "⊢ X = Y ⟹ X = Y"
by (auto simp: inteq_reflection)

lemma int_iffI:
assumes "⊢ F ⟶ G" and "⊢ G ⟶ F"
shows "⊢ F = G"
using assms by force

lemma int_iffD1: assumes h: "⊢ F = G" shows "⊢ F ⟶ G"
using h by auto

lemma int_iffD2: assumes h: "⊢ F = G" shows "⊢ G ⟶ F"
using h by auto

lemma lift_imp_trans:
assumes "⊢ A ⟶ B" and "⊢ B ⟶ C"
shows "⊢ A ⟶ C"
using assms by force

lemma lift_imp_neg: assumes "⊢ A ⟶ B" shows "⊢ ¬B ⟶ ¬A"
using assms by auto

lemma lift_and_com:  "⊢ (A ∧ B) = (B ∧ A)"
by auto

end


# Theory Semantics

(*  Title:       A Definitional Encoding of TLA in Isabelle/HOL
Authors:     Gudmund Grov <ggrov at inf.ed.ac.uk>
Stephan Merz <Stephan.Merz at loria.fr>
Year:        2011
Maintainer:  Gudmund Grov <ggrov at inf.ed.ac.uk>
*)

section ‹Semantics›

theory Semantics
imports Sequence Intensional
begin

text ‹
This theory mechanises a \emph{shallow} embedding of \tlastar{} using the
‹Sequence› and ‹Intensional› theories. A shallow embedding
represents \tlastar{} using Isabelle/HOL predicates, while a \emph{deep}
embedding would represent \tlastar{} formulas and pre-formulas as mutually
inductive datatypes\footnote{See e.g. \cite{Wildmoser04} for a discussion
about deep vs. shallow embeddings in Isabelle/HOL.}.
The choice of a shallow over a deep embedding is motivated by the following
factors: a shallow embedding is usually less involved, and existing Isabelle
theories and tools can be applied more directly to enhance automation; due to
the lifting in the ‹Intensional› theory, a shallow embedding can reuse
standard logical operators, whilst a deep embedding requires a different
set of operators for both formulas and pre-formulas. Finally, since our
target is system verification rather than proving meta-properties of \tlastar{},
which requires a deep embedding, a shallow embedding is more fit for purpose.
›

subsection "Types of Formulas"

text ‹
To mechanise the \tlastar{} semantics, the following
type abbreviations are used:
›

type_synonym ('a,'b) formfun = "'a seq ⇒ 'b"
type_synonym 'a formula = "('a,bool) formfun"
type_synonym ('a,'b) stfun = "'a ⇒ 'b"
type_synonym 'a stpred = "('a,bool) stfun"

instance
"fun" :: (type,type) world ..

instance
"prod" :: (type,type) world ..

text ‹
Pair and function are instantiated to be of type class world.
This allows use of the lifted intensional logic for formulas, and
standard logical connectives can therefore be used.
›

subsection "Semantics of TLA*"

text ‹The semantics of \tlastar{} is defined.›

definition always :: "('a::world) formula ⇒ 'a formula"
where "always F ≡ λ s. ∀ n. (s |⇩s n) ⊨ F"

definition nexts :: "('a::world) formula ⇒ 'a formula"
where "nexts F ≡ λ s. (tail s) ⊨ F"

definition before :: "('a::world,'b) stfun ⇒ ('a,'b) formfun"
where "before f ≡ λ s. (first s) ⊨ f"

definition after :: "('a::world,'b) stfun ⇒ ('a,'b) formfun"
where "after f ≡ λ s. (second s) ⊨ f"

definition unch  :: "('a::world,'b) stfun ⇒ 'a formula"
where "unch v ≡ λ s. s ⊨ (after v) = (before v)"

definition action :: "('a::world) formula ⇒ ('a,'b) stfun ⇒ 'a formula"
where "action P v ≡ λ s. ∀ i. ((s |⇩s i) ⊨ P) ∨ ((s |⇩s i) ⊨ unch v)"

subsubsection "Concrete Syntax"

text‹This is the concrete syntax for the (abstract) operators above.›

syntax
"_always" :: "lift ⇒ lift" ("(□_)" [90] 90)
"_nexts" :: "lift ⇒ lift" ("(○_)" [90] 90)
"_action" :: "[lift,lift] ⇒ lift" ("(□[_]'_(_))" [20,1000] 90)
"_before"    :: "lift ⇒ lift"  ("($_)" [100] 99) "_after" :: "lift ⇒ lift" ("(_$)" [100] 99)
"_prime"     :: "lift ⇒ lift"  ("(_)" [100] 99)
"_unch"     :: "lift ⇒ lift"  ("(Unchanged _)" [100] 99)
"TEMP"  :: "lift ⇒ 'b" ("(TEMP _)")

syntax (ASCII)
"_always" :: "lift ⇒ lift" ("([]_)" [90] 90)
"_nexts" :: "lift ⇒ lift" ("(Next _)" [90] 90)
"_action" :: "[lift,lift] ⇒ lift" ("([][_]'_(_))" [20,1000] 90)

translations
"_always" ⇌ "CONST always"
"_nexts" ⇌ "CONST nexts"
"_action" ⇌ "CONST action"
"_before"    ⇌ "CONST before"
"_after"     ⇌ "CONST after"
"_prime"     ⇀ "CONST after"
"_unch"     ⇌ "CONST unch"
"TEMP F" ⇀ "(F:: (nat ⇒ _) ⇒ _)"

subsection "Abbreviations"

text ‹Some standard temporal abbreviations, with their concrete syntax.›

definition actrans :: "('a::world) formula ⇒ ('a,'b) stfun ⇒ 'a formula"
where "actrans P v ≡ TEMP(P ∨ unch v)"

definition eventually :: "('a::world) formula ⇒ 'a formula"
where "eventually F ≡ LIFT(¬□(¬F))"

definition angle_action :: "('a::world) formula ⇒ ('a,'b) stfun ⇒ 'a formula"
where "angle_action P v ≡ LIFT(¬□[¬P]_v)"

definition angle_actrans :: "('a::world) formula ⇒ ('a,'b) stfun ⇒ 'a formula"
where "angle_actrans P v ≡ TEMP (¬ actrans (LIFT(¬P)) v)"

definition leadsto :: "('a::world) formula ⇒ 'a formula ⇒ 'a formula"
where "leadsto P Q ≡ LIFT □(P ⟶ eventually Q)"

subsubsection "Concrete Syntax"

syntax (ASCII)
"_actrans" :: "[lift,lift] ⇒ lift" ("([_]'_(_))"  [20,1000] 90)
"_eventually" :: "lift ⇒ lift" ("(<>_)" [90] 90)
"_angle_action" :: "[lift,lift] ⇒ lift" ("(<><_>'_(_))" [20,1000] 90)
"_angle_actrans" :: "[lift,lift] ⇒ lift" ("(<_>'_(_))" [20,1000] 90)
"_leadsto" :: "[lift,lift] ⇒ lift" ("(_ ~> _)" [26,25] 25)

syntax
"_eventually" :: "lift ⇒ lift" ("(◇_)" [90] 90)
"_angle_action" :: "[lift,lift] ⇒ lift" ("(◇⟨_⟩'_(_))" [20,1000] 90)
"_angle_actrans" :: "[lift,lift] ⇒ lift" ("(⟨_⟩'_(_))" [20,1000] 90)
"_leadsto" :: "[lift,lift] ⇒ lift" ("(_ ↝ _)" [26,25] 25)

translations
"_actrans" ⇌ "CONST actrans"
"_eventually" ⇌ "CONST eventually"
"_angle_action" ⇌ "CONST angle_action"
"_angle_actrans" ⇌ "CONST angle_actrans"

subsection "Properties of Operators"

text ‹The following lemmas show that these operators have the expected semantics.›

lemma eventually_defs: "(w ⊨ ◇ F) = (∃ n. (w |⇩s n) ⊨ F)"
by (simp add: eventually_def always_def)

lemma angle_action_defs: "(w ⊨ ◇⟨P⟩_v) = (∃ i. ((w |⇩s i) ⊨ P) ∧ ((w |⇩s i) ⊨ v$≠$v))"
by (simp add: angle_action_def action_def unch_def)

lemma unch_defs: "(w ⊨ Unchanged v) = (((second w) ⊨ v) = ((first w) ⊨ v))"
by (simp add: unch_def before_def nexts_def after_def tail_def suffix_def first_def second_def)

lemma linalw:
assumes h1: "a ≤ b" and h2: "(w |⇩s a) ⊨ □A"
shows "(w |⇩s b) ⊨ □A"
proof (clarsimp simp: always_def)
fix n
from h1 obtain k where g1: "b = a + k" by (auto simp: le_iff_add)
with h2 show "(w |⇩s b |⇩s n) ⊨ A" by (auto simp: always_def suffix_plus ac_simps)
qed

subsection "Invariance Under Stuttering"

text ‹
A key feature of \tlastar{} is that specification at different abstraction
levels can be compared. The soundness of this relies on the stuttering invariance
of formulas. Since the embedding is shallow, it cannot be shown that a generic
\tlastar{} formula is stuttering invariant. However, this section will show that
each operator is stuttering invariant or preserves stuttering invariance in an
appropriate sense, which can be used to show stuttering invariance
for given specifications.

Formula ‹F› is stuttering invariant if for any two similar behaviours
(i.e., sequences of states), ‹F› holds in one iff it holds in the other.
The definition is generalised to arbitrary expressions, and not just predicates.
›

definition stutinv :: "('a,'b) formfun ⇒ bool"
where "stutinv F ≡ ∀ σ τ. σ ≈ τ ⟶ (σ ⊨ F) = (τ ⊨ F)"

text‹
The requirement for stuttering invariance is too strong for pre-formulas.
For example, an action formula specifies a relation between the first two states
of a behaviour, and will rarely be satisfied by a stuttering step. This is why
pre-formulas are protected'' by (square or angle) brackets in \tlastar{}:
the only place a pre-formula ‹P› can be used is inside an action:
‹□[P]_v›.
To show that ‹□[P]_v› is stuttering invariant, is must be shown that a
slightly weaker predicate holds for @{term P}. For example, if @{term P} contains
a term of the form ‹○○Q›, then it is not a well-formed pre-formula, thus
‹□[P]_v› is not stuttering invariant. This weaker version of
stuttering invariance has been named \emph{near stuttering invariance}.
›

definition nstutinv :: "('a,'b) formfun ⇒ bool"
where "nstutinv P ≡ ∀ σ τ. (first σ = first τ) ∧ (tail σ) ≈ (tail τ) ⟶ (σ ⊨ P) = (τ ⊨ P)"

syntax
"_stutinv" :: "lift ⇒ bool" ("(STUTINV _)" [40] 40)
"_nstutinv" :: "lift ⇒ bool" ("(NSTUTINV _)" [40] 40)

translations
"_stutinv" ⇌ "CONST stutinv"
"_nstutinv" ⇌ "CONST nstutinv"

text ‹
Predicate @{term "stutinv F"} formalises stuttering invariance for
formula @{term F}. That is if two sequences are similar @{term "s ≈ t"} (equal up
to stuttering) then the validity of @{term F} under both @{term s} and @{term t}
are equivalent. Predicate @{term "nstutinv P"} should be read as \emph{nearly
stuttering invariant} -- and is required for some stuttering invariance proofs.
›

lemma stutinv_strictly_stronger:
assumes h: "STUTINV F" shows "NSTUTINV F"
unfolding nstutinv_def
proof (clarify)
fix s t :: "nat ⇒ 'a"
assume a1: "first s = first t" and a2: "(tail s) ≈ (tail t)"
have "s ≈ t"
proof -
have tg1: "(first s) ## (tail s) = s" by (rule seq_app_first_tail)
have tg2: "(first t) ## (tail t) = t" by (rule seq_app_first_tail)
with a1 have tg2': "(first s) ## (tail t) = t" by simp
from a2 have "(first s) ## (tail s) ≈ (first s) ## (tail t)" by (rule app_seqsimilar)
with tg1 tg2' show ?thesis by simp
qed
with h show "(s ⊨ F) = (t ⊨ F)" by (simp add: stutinv_def)
qed

subsubsection "Properties of @{term stutinv}"

text ‹
This subsection proves stuttering invariance, preservation of stuttering invariance
and introduction of stuttering invariance for different formulas.
First, state predicates are stuttering invariant.
›

theorem stut_before: "STUTINV $F" proof (clarsimp simp: stutinv_def) fix s t :: "'a seq" assume a1: "s ≈ t" hence "(first s) = (first t)" by (rule sim_first) thus "(s ⊨$F) = (t ⊨ $F)" by (simp add: before_def) qed lemma nstut_after: "NSTUTINV F$"
proof (clarsimp simp: nstutinv_def)
fix s t :: "'a seq"
assume a1: "tail s ≈ tail t"
thus "(s ⊨ F$) = (t ⊨ F$)" by (simp add: after_def tail_sim_second)
qed

text‹The always operator preserves stuttering invariance.›

theorem stut_always: assumes H:"STUTINV F" shows "STUTINV □F"
proof (clarsimp simp: stutinv_def)
fix s t :: "'a seq"
assume a2: "s ≈ t"
show "(s ⊨ (□ F)) = (t ⊨ (□ F))"
proof
assume a1: "t ⊨ □ F"
show "s ⊨ □ F"
proof (clarsimp simp: always_def)
fix n
from a2[THEN sim_step] obtain m where m: "s |⇩s n ≈ t |⇩s m" by blast
from a1 have "(t |⇩s m) ⊨ F" by (simp add: always_def)
with H m show "(s |⇩s n) ⊨ F" by (simp add: stutinv_def)
qed
next
assume a1: "s ⊨ (□ F)"
show "t ⊨ (□ F)"
proof (clarsimp simp: always_def)
fix n
from a2[THEN seqsim_sym, THEN sim_step] obtain m where m: "t |⇩s n ≈ s |⇩s m" by blast
from a1 have "(s |⇩s m) ⊨ F" by (simp add: always_def)
with H m show "(t |⇩s n) ⊨ F" by (simp add: stutinv_def)
qed
qed
qed

text ‹
Assuming that formula @{term P} is nearly suttering invariant
then ‹□[P]_v› will be stuttering invariant.
›

lemma stut_action_lemma:
assumes H: "NSTUTINV P" and st: "s ≈ t" and P: "t ⊨ □[P]_v"
shows "s ⊨ □[P]_v"
proof (clarsimp simp: action_def)
fix n
assume "¬ ((s |⇩s n) ⊨ Unchanged v)"
hence v: "v (s (Suc n)) ≠ v (s n)"
by (simp add: unch_defs first_def second_def suffix_def)
from st[THEN sim_step] obtain m where
a2': "s |⇩s n ≈ t |⇩s m
∧ (s |⇩s Suc n ≈ t |⇩s Suc m ∨ s |⇩s Suc n ≈ t |⇩s m)" ..
hence g1: "(s |⇩s n ≈ t |⇩s m)" by simp
hence g1'': "first (s |⇩s n) = first (t |⇩s m)" by (simp add: sim_first)
hence g1': "s n = t m" by (simp add: suffix_def first_def)
from a2' have g2: "s |⇩s Suc n ≈ t |⇩s Suc m ∨ s |⇩s Suc n ≈ t |⇩s m" by simp
from P have a1': "((t |⇩s m) ⊨ P) ∨ ((t |⇩s m) ⊨ Unchanged v)" by (simp add: action_def)
from g2 show "(s |⇩s n) ⊨ P"
proof
assume "s |⇩s Suc n ≈ t |⇩s m"
hence "first (s |⇩s Suc n) = first (t |⇩s m)" by (simp add: sim_first)
hence "s (Suc n) = t m" by (simp add: suffix_def first_def)
with g1' v show ?thesis by simp  ― ‹by contradiction›
next
assume a3: "s |⇩s Suc n ≈ t |⇩s Suc m"
hence "first (s |⇩s Suc n) = first (t |⇩s Suc m)" by (simp add: sim_first)
hence a3': "s (Suc n) = t (Suc m)" by (simp add: suffix_def first_def)
from a1' show ?thesis
proof
assume "(t |⇩s m) ⊨ Unchanged v"
hence "v (t (Suc m)) = v (t m)"
by (simp add: unch_defs first_def second_def suffix_def)
with g1' a3' v show ?thesis by simp  ― ‹again, by contradiction›
next
assume a4: "(t |⇩s m) ⊨ P"
from a3 have "tail (s |⇩s n) ≈ tail (t |⇩s m)" by (simp add: tail_def suffix_plus)
with H g1'' a4 show ?thesis by (auto simp: nstutinv_def)
qed
qed
qed

theorem stut_action: assumes H: "NSTUTINV P" shows "STUTINV □[P]_v"
proof (clarsimp simp: stutinv_def)
fix s t :: "'a seq"
assume st: "s ≈ t"
show "(s ⊨ □[P]_v) = (t ⊨ □[P]_v)"
proof
assume "t ⊨ □[P]_v"
with H st show "s ⊨ □[P]_v" by (rule stut_action_lemma)
next
assume "s ⊨ □[P]_v"
with H st[THEN seqsim_sym] show "t ⊨ □[P]_v" by (rule stut_action_lemma)
qed
qed

text ‹
The lemmas below shows that propositional and predicate operators
preserve stuttering invariance.
›

lemma stut_and: "⟦STUTINV F;STUTINV G⟧ ⟹ STUTINV (F ∧ G)"
by (simp add: stutinv_def)

lemma stut_or: "⟦STUTINV F;STUTINV G⟧ ⟹ STUTINV (F ∨ G)"
by (simp add: stutinv_def)

lemma stut_imp: "⟦STUTINV F;STUTINV G⟧ ⟹ STUTINV (F ⟶ G)"
by (simp add: stutinv_def)

lemma stut_eq: "⟦STUTINV F;STUTINV G⟧ ⟹ STUTINV (F = G)"
by (simp add: stutinv_def)

lemma stut_noteq: "⟦STUTINV F;STUTINV G⟧ ⟹ STUTINV (F ≠ G)"
by (simp add: stutinv_def)

lemma stut_not: "STUTINV F ⟹ STUTINV (¬ F)"
by (simp add: stutinv_def)

lemma stut_all: "(⋀x. STUTINV (F x)) ⟹ STUTINV (∀ x. F x)"
by (simp add: stutinv_def)

lemma stut_ex: "(⋀x. STUTINV (F x)) ⟹ STUTINV (∃ x. F x)"
by (simp add: stutinv_def)

lemma stut_const: "STUTINV #c"
by (simp add: stutinv_def)

lemma stut_fun1: "STUTINV X ⟹ STUTINV (f <X>)"
by (simp add: stutinv_def)

lemma stut_fun2: "⟦STUTINV X;STUTINV Y⟧ ⟹ STUTINV (f <X,Y>)"
by (simp add: stutinv_def)

lemma stut_fun3: "⟦STUTINV X;STUTINV Y;STUTINV Z⟧ ⟹ STUTINV (f <X,Y,Z>)"
by (simp add: stutinv_def)

lemma stut_fun4: "⟦STUTINV X;STUTINV Y;STUTINV Z; STUTINV W⟧ ⟹ STUTINV (f <X,Y,Z,W>)"
by (simp add: stutinv_def)

lemma stut_plus: "⟦STUTINV x;STUTINV y⟧ ⟹ STUTINV (x+y)"
by (simp add: stutinv_def)

subsubsection "Properties of @{term nstutinv}"

text ‹
This subsection shows analogous properties about near stuttering
invariance.

If a formula @{term F} is stuttering invariant then ‹○F› is
nearly stuttering invariant.
›

lemma nstut_nexts: assumes H: "STUTINV F" shows "NSTUTINV ○F"
using H by (simp add: stutinv_def nstutinv_def nexts_def)

text ‹
The lemmas below shows that propositional and predicate operators
preserves near stuttering invariance.
›

lemma nstut_and: "⟦NSTUTINV F;NSTUTINV G⟧ ⟹ NSTUTINV (F ∧ G)"
by (auto simp: nstutinv_def)

lemma nstut_or: "⟦NSTUTINV F;NSTUTINV G⟧ ⟹ NSTUTINV (F ∨ G)"
by (auto simp: nstutinv_def)

lemma nstut_imp: "⟦NSTUTINV F;NSTUTINV G⟧ ⟹ NSTUTINV (F ⟶ G)"
by (auto simp: nstutinv_def)

lemma nstut_eq: "⟦NSTUTINV F; NSTUTINV G⟧ ⟹ NSTUTINV (F = G)"
by (force simp: nstutinv_def)

lemma nstut_not: "NSTUTINV F ⟹ NSTUTINV (¬ F)"
by (auto simp: nstutinv_def)

lemma nstut_noteq: "⟦NSTUTINV F; NSTUTINV G⟧ ⟹ NSTUTINV (F ≠ G)"
by (simp add: nstut_eq nstut_not)

lemma nstut_all: "(⋀x. NSTUTINV (F x)) ⟹ NSTUTINV (∀ x. F x)"
by (auto simp: nstutinv_def)

lemma nstut_ex: "(⋀x. NSTUTINV (F x)) ⟹ NSTUTINV (∃ x. F x)"
by (auto simp: nstutinv_def)

lemma nstut_const: "NSTUTINV #c"
by (auto simp: nstutinv_def)

lemma nstut_fun1: "NSTUTINV X ⟹ NSTUTINV (f <X>)"
by (force simp: nstutinv_def)

lemma nstut_fun2: "⟦NSTUTINV X; NSTUTINV Y⟧ ⟹ NSTUTINV (f <X,Y>)"
by (force simp: nstutinv_def)

lemma nstut_fun3: "⟦NSTUTINV X; NSTUTINV Y; NSTUTINV Z⟧ ⟹ NSTUTINV (f <X,Y,Z>)"
by (force simp: nstutinv_def)

lemma nstut_fun4: "⟦NSTUTINV X; NSTUTINV Y; NSTUTINV Z; NSTUTINV W⟧ ⟹ NSTUTINV (f <X,Y,Z,W>)"
by (force simp: nstutinv_def)

lemma nstut_plus: "⟦NSTUTINV x;NSTUTINV y⟧ ⟹ NSTUTINV (x+y)"
by (simp add: nstut_fun2)

subsubsection "Abbreviations"

text ‹
We show the obvious fact that the same properties holds for abbreviated
operators.
›

lemmas nstut_before = stut_before[THEN stutinv_strictly_stronger]

lemma nstut_unch: "NSTUTINV (Unchanged v)"
proof (unfold unch_def)
have g1: "NSTUTINV v$" by (rule nstut_after) have "NSTUTINV$v" by (rule stut_before[THEN stutinv_strictly_stronger])
with g1 show "NSTUTINV (v$=$v)" by (rule nstut_eq)
qed

text‹
Formulas ‹[P]_v› are not \tlastar{} formulas by themselves,
but we need to reason about them when they appear wrapped
inside ‹□[-]_v›. We only require that it preserves nearly
stuttering invariance. Observe that ‹[P]_v› trivially holds for
a stuttering step, so it cannot be stuttering invariant.
›

lemma nstut_actrans: "NSTUTINV P ⟹ NSTUTINV [P]_v"
by (simp add: actrans_def nstut_unch nstut_or)

lemma stut_eventually: "STUTINV F ⟹ STUTINV ◇F"
by (simp add: eventually_def stut_not stut_always)

lemma stut_leadsto: "⟦STUTINV F; STUTINV G⟧ ⟹ STUTINV (F ↝ G)"
by (simp add: leadsto_def stut_always stut_eventually stut_imp)

lemma stut_angle_action: "NSTUTINV P ⟹ STUTINV ◇⟨P⟩_v"
by (simp add: angle_action_def nstut_not stut_action stut_not)

lemma nstut_angle_acttrans: "NSTUTINV P ⟹ NSTUTINV ⟨P⟩_v"
by (simp add: angle_actrans_def nstut_not nstut_actrans)

lemmas stutinvs = stut_before stut_always stut_action
stut_and stut_or stut_imp stut_eq stut_noteq stut_not
stut_all stut_ex stut_eventually stut_leadsto stut_angle_action stut_const
stut_fun1 stut_fun2 stut_fun3 stut_fun4

lemmas nstutinvs =  nstut_after nstut_nexts nstut_actrans
nstut_unch nstut_and nstut_or nstut_imp nstut_eq nstut_noteq nstut_not
nstut_all nstut_ex nstut_angle_acttrans stutinv_strictly_stronger
nstut_fun1 nstut_fun2 nstut_fun3 nstut_fun4 stutinvs[THEN stutinv_strictly_stronger]

lemmas bothstutinvs = stutinvs nstutinvs

end


# Theory PreFormulas

(*  Title:       A Definitional Encoding of TLA in Isabelle/HOL
Authors:     Gudmund Grov <ggrov at inf.ed.ac.uk>
Stephan Merz <Stephan.Merz at loria.fr>
Year:        2011
Maintainer:  Gudmund Grov <ggrov at inf.ed.ac.uk>
*)

section "Reasoning about PreFormulas"

theory PreFormulas
imports Semantics
begin

text‹
Semantic separation of formulas and pre-formulas requires a deep embedding.
We introduce a syntactically distinct notion of validity, written ‹|~ A›,
for pre-formulas. Although it is semantically identical to ‹⊢ A›, it
helps users distinguish pre-formulas from formulas in \tlastar{} proofs.
›

definition PreValid :: "('w::world) form ⇒ bool"
where "PreValid A ≡ ∀ w. w ⊨ A"

syntax
"_PreValid"      :: "lift ⇒ bool"     ("(|~ _)" 5)

translations
"_PreValid"  ⇌ "CONST PreValid"

lemma prefD[dest]: "|~ A ⟹ w ⊨ A"
by (simp add: PreValid_def)

lemma prefI[intro!]: "(⋀ w. w ⊨ A) ⟹ |~ A"
by (simp add: PreValid_def)

method_setup pref_unlift = ‹
Scan.succeed (fn ctxt => SIMPLE_METHOD'
(resolve_tac ctxt @{thms prefI} THEN' rewrite_goal_tac ctxt @{thms intensional_rews}))
› "int_unlift for PreFormulas"

lemma prefeq_reflection: assumes P1: "|~ x=y" shows  "(x ≡ y)"
using P1 by (intro eq_reflection) force

lemma pref_True[simp]: "|~ #True"
by auto

lemma pref_eq: "|~ X = Y ⟹ X = Y"
by (auto simp: prefeq_reflection)

lemma pref_iffI:
assumes "|~ F ⟶ G" and "|~ G ⟶ F"
shows "|~ F = G"
using assms by force

lemma pref_iffD1: assumes "|~ F = G" shows "|~ F ⟶ G"
using assms by auto

lemma pref_iffD2: assumes "|~ F = G" shows "|~ G ⟶ F"
using assms by auto

lemma unl_pref_imp:
assumes "|~ F ⟶ G" shows "⋀ w. w ⊨ F ⟹ w ⊨ G"
using assms by auto

lemma pref_imp_trans:
assumes "|~ F ⟶ G" and "|~ G ⟶ H"
shows "|~ F ⟶ H"
using assms by force

subsection "Lemmas about ‹Unchanged›"

text ‹
Many of the \tlastar{} axioms only require a state function witness
which leaves the state space unchanged. An obvious witness is the
@{term id} function. The lemmas require that the given formula is
invariant under stuttering.
›

lemma pre_id_unch: assumes h: "stutinv F"
shows "|~ F ∧ Unchanged id ⟶ ○F"
proof (pref_unlift, clarify)
fix s
assume a1: "s ⊨ F" and  a2: "s ⊨ Unchanged id"
from a2 have "(id (second s) = id (first s))" by (simp add: unch_defs)
hence "s ≈ (tail s)" by (simp add: addfirststut)
with h a1 have "(tail s) ⊨ F" by (simp add: stutinv_def)
thus "s ⊨ ○F" by (unfold nexts_def)
qed

lemma pre_ex_unch:
assumes h: "stutinv F"
shows "∃(v::'a::world ⇒ 'a). ( |~ F ∧ Unchanged v ⟶ ○F)"
using pre_id_unch[OF h] by blast

lemma unch_pair: "|~ Unchanged (x,y) = (Unchanged x ∧ Unchanged y)"
by (auto simp: unch_def before_def after_def nexts_def)

lemmas unch_eq1 = unch_pair[THEN pref_eq]
lemmas unch_eq2 = unch_pair[THEN prefeq_reflection]

lemma angle_actrans_sem: "|~ ⟨F⟩_v = (F ∧ v$≠$v)"
by (auto simp: angle_actrans_def actrans_def unch_def)

lemmas angle_actrans_sem_eq = angle_actrans_sem[THEN pref_eq]

subsection "Lemmas about ‹after›"

lemma after_const: "|~ (#c) = #c"
by (auto simp: nexts_def before_def after_def)

lemma after_fun1: "|~ f<x> = f<x>"
by (auto simp: nexts_def before_def after_def)

lemma after_fun2: "|~ f<x,y> = f <x,y>"
by (auto simp: nexts_def before_def after_def)

lemma after_fun3: "|~ f<x,y,z> = f <x,y,z>"
by (auto simp: nexts_def before_def after_def)

lemma after_fun4: "|~ f<x,y,z,zz> = f <x,y,z,zz>"
by (auto simp: nexts_def before_def after_def)

lemma after_forall: "|~ (∀ x. P x) = (∀ x. (P x))"
by (auto simp: nexts_def before_def after_def)

lemma after_exists: "|~ (∃ x. P x) = (∃ x. (P x))"
by (auto simp: nexts_def before_def after_def)

lemma after_exists1: "|~ (∃! x. P x) = (∃! x. (P x))"
by (auto simp: nexts_def before_def after_def)

lemmas all_after = after_const after_fun1 after_fun2 after_fun3 after_fun4
after_forall after_exists after_exists1

lemmas all_after_unl = all_after[THEN prefD]
lemmas all_after_eq = all_after[THEN prefeq_reflection]

subsection "Lemmas about ‹before›"

lemma before_const: "⊢ $(#c) = #c" by (auto simp: before_def) lemma before_fun1: "⊢$(f<x>) = f <$x>" by (auto simp: before_def) lemma before_fun2: "⊢$(f<x,y>) = f <$x,$y>"
by (auto simp: before_def)

lemma before_fun3: "⊢ $(f<x,y,z>) = f <$x,$y,$z>"
by (auto simp: before_def)

lemma before_fun4: "⊢ $(f<x,y,z,zz>) = f <$x,$y,$z,$zz>" by (auto simp: before_def) lemma before_forall: "⊢$(∀ x. P x) = (∀ x. $(P x))" by (auto simp: before_def) lemma before_exists: "⊢$(∃ x. P x) = (∃ x. $(P x))" by (auto simp: before_def) lemma before_exists1: "⊢$(∃! x. P x) = (∃! x. $(P x))" by (auto simp: before_def) lemmas all_before = before_const before_fun1 before_fun2 before_fun3 before_fun4 before_forall before_exists before_exists1 lemmas all_before_unl = all_before[THEN intD] lemmas all_before_eq = all_before[THEN inteq_reflection] subsection "Some general properties" lemma angle_actrans_conj: "|~ (⟨F ∧ G⟩_v) = (⟨F⟩_v ∧ ⟨G⟩_v)" by (auto simp: angle_actrans_def actrans_def unch_def) lemma angle_actrans_disj: "|~ (⟨F ∨ G⟩_v) = (⟨F⟩_v ∨ ⟨G⟩_v)" by (auto simp: angle_actrans_def actrans_def unch_def) lemma int_eq_true: "⊢ P ⟹ ⊢ P = #True" by auto lemma pref_eq_true: "|~ P ⟹ |~ P = #True" by auto subsection "Unlifting attributes and methods" text ‹Attribute which unlifts an intensional formula or preformula› ML ‹ fun unl_rewr ctxt thm = let val unl = (thm RS @{thm intD}) handle THM _ => (thm RS @{thm prefD}) handle THM _ => thm val rewr = rewrite_rule ctxt @{thms intensional_rews} in unl |> rewr end; › attribute_setup unlifted = ‹ Scan.succeed (Thm.rule_attribute [] (unl_rewr o Context.proof_of)) › "unlift intensional formulas" attribute_setup unlift_rule = ‹ Scan.succeed (Thm.rule_attribute [] (Context.proof_of #> (fn ctxt => Object_Logic.rulify ctxt o unl_rewr ctxt))) › "unlift and rulify intensional formulas" text ‹ Attribute which turns an intensional formula or preformula into a rewrite rule. Formulas ‹F› that are not equalities are turned into ‹F ≡ #True›. › ML ‹ fun int_rewr thm = (thm RS @{thm inteq_reflection}) handle THM _ => (thm RS @{thm prefeq_reflection}) handle THM _ => ((thm RS @{thm int_eq_true}) RS @{thm inteq_reflection}) handle THM _ => ((thm RS @{thm pref_eq_true}) RS @{thm prefeq_reflection}); › attribute_setup simp_unl = ‹ Attrib.add_del (Thm.declaration_attribute (fn th => Simplifier.map_ss (Simplifier.add_simp (int_rewr th)))) (K (NONE, NONE)) (* note only adding -- removing is ignored *) › "add thm unlifted from rewrites from intensional formulas or preformulas" attribute_setup int_rewrite = ‹Scan.succeed (Thm.rule_attribute [] (fn _ => int_rewr))› "produce rewrites from intensional formulas or preformulas" end  # Theory Rules (* Title: A Definitional Encoding of TLA in Isabelle/HOL Authors: Gudmund Grov <ggrov at inf.ed.ac.uk> Stephan Merz <Stephan.Merz at loria.fr> Year: 2011 Maintainer: Gudmund Grov <ggrov at inf.ed.ac.uk> *) section "A Proof System for TLA* " theory Rules imports PreFormulas begin text‹ We prove soundness of the proof system of \tlastar{}, from which the system verification rules from Lamport's original TLA paper will be derived. This theory is still state-independent, thus state-dependent enableness proofs, required for proofs based on fairness assumptions, and flexible quantification, are not discussed here. The \tlastar{} paper \cite{Merz99} suggest both a \emph{hetereogeneous} and a \emph{homogenous} proof system for \tlastar{}. The homogeneous version eliminates the auxiliary definitions from the ‹Preformula› theory, creating a single provability relation. This axiomatisation is based on the fact that a pre-formula can only be used via the ‹sq› rule. In a nutshell, ‹sq› is applied to ‹pax1› to ‹pax5›, and ‹nex›, ‹pre› and ‹pmp› are changed to accommodate this. It is argued that while the hetereogenous version is easier to understand, the homogenous system avoids the introduction of an auxiliary provability relation. However, the price to pay is that reasoning about pre-formulas (in particular, actions) has to be performed in the scope of temporal operators such as ‹□[P]_v›, which is notationally quite heavy, We prefer here the heterogeneous approach, which exposes the pre-formulas and lets us use standard HOL rules more directly. › subsection "The Basic Axioms" theorem fmp: assumes "⊢ F" and "⊢ F ⟶ G" shows "⊢ G" using assms[unlifted] by auto theorem pmp: assumes "|~ F" and "|~ F ⟶ G" shows "|~ G" using assms[unlifted] by auto theorem sq: assumes "|~ P" shows "⊢ □[P]_v" using assms[unlifted] by (auto simp: action_def) theorem pre: assumes "⊢ F" shows "|~ F" using assms by auto theorem nex: assumes h1: "⊢ F" shows "|~ ○F" using assms by (auto simp: nexts_def) theorem ax0: "⊢ # True" by auto theorem ax1: "⊢ □F ⟶ F" proof (clarsimp simp: always_def) fix w assume "∀n. (w |⇩s n) ⊨ F" hence "(w |⇩s 0) ⊨ F" .. thus "w ⊨ F" by simp qed theorem ax2: "⊢ □F ⟶ □[□F]_v" by (auto simp: always_def action_def suffix_plus) theorem ax3: assumes H: "|~ F ∧ Unchanged v ⟶ ○F" shows "⊢ □[F ⟶ ○F]_v ⟶ (F ⟶ □F)" proof (clarsimp simp: always_def) fix w n assume a1: "w ⊨ □[F ⟶ ○F]_v" and a2: "w ⊨ F" show "(w |⇩s n) ⊨ F" proof (induct n) from a2 show "(w |⇩s 0) ⊨ F" by simp next fix m assume a3: "(w |⇩s m) ⊨ F" with a1 H[unlifted] show "(w |⇩s (Suc m)) ⊨ F" by (auto simp: nexts_def action_def tail_suffix_suc) qed qed theorem ax4: "⊢ □[P ⟶ Q]_v ⟶ (□[P]_v ⟶ □[Q]_v)" by (force simp: action_def) theorem ax5: "⊢ □[v ≠$v]_v"
by (auto simp: action_def unch_def)

theorem pax0: "|~ # True"
by auto

theorem pax1 [simp_unl]: "|~ (○¬F) = (¬○F)"
by (auto simp: nexts_def)

theorem pax2: "|~ ○(F ⟶ G) ⟶ (○F ⟶ ○G)"
by (auto simp: nexts_def)

theorem pax3: "|~ □F ⟶ ○□F"
by (auto simp: always_def nexts_def tail_def suffix_plus)

theorem pax4: "|~ □[P]_v = ([P]_v ∧ ○□[P]_v)"
proof (auto)
fix w
assume "w ⊨ □[P]_v"
from this[unfolded action_def] have "((w |⇩s 0) ⊨ P) ∨ ((w |⇩s 0) ⊨ Unchanged v)" ..
thus "w ⊨ [P]_v" by (simp add: actrans_def)
next
fix w
assume "w ⊨ □[P]_v"
thus "w ⊨ ○□[P]_v" by (auto simp: nexts_def action_def tail_def suffix_plus)
next
fix w
assume 1: "w ⊨ [P]_v" and 2: "w ⊨ ○□[P]_v"
show "w ⊨ □[P]_v"
proof (auto simp: action_def)
fix i
assume 3: "¬ ((w |⇩s i) ⊨ Unchanged v)"
show "(w |⇩s i) ⊨ P"
proof (cases i)
assume "i = 0"
with 1 3 show ?thesis by (simp add: actrans_def)
next
fix j
assume "i = Suc j"
with 2 3 show ?thesis by (auto simp: nexts_def action_def tail_def suffix_plus)
qed
qed
qed

theorem pax5: "|~ ○□F ⟶ □[○F]_v"
by (auto simp: nexts_def always_def action_def tail_def suffix_plus)

text ‹
Theorem to show that universal quantification distributes over the always
operator. Since the \tlastar{} paper only addresses the propositional fragment,
this theorem does not appear there.
›

theorem allT:  "⊢ (∀x. □(F x)) = (□(∀x. F x))"
by (auto simp: always_def)

theorem allActT:  "⊢ (∀x. □[F x]_v) = (□[(∀x. F x)]_v)"
by (force simp: action_def)

subsection "Derived Theorems"

text‹
This section includes some derived theorems based on the axioms, taken
from the \tlastar{} paper~\cite{Merz99}. We mimic the proofs given there
and avoid semantic reasoning whenever possible.

The ‹alw› theorem of~\cite{Merz99} states that if F holds
in all worlds then it always holds, i.e. $F \vDash \Box F$. However,
the derivation of this theorem (using the proof rules above)
relies on access of the set of free variables (FV), which is not
available in a shallow encoding.

However, we can prove a similar rule ‹alw2› using an additional
hypothesis @{term "|~ F ∧ Unchanged v ⟶ ○F"}.
›

theorem alw2:
assumes h1: "⊢ F" and h2: "|~ F ∧ Unchanged v ⟶ ○F"
shows "⊢ □F"
proof -
from h1 have g2: "|~ ○F" by (rule nex)
hence g3: "|~ F ⟶ ○F" by auto
hence g4:"⊢ □[(F ⟶ ○F)]_v" by (rule sq)
from h2 have "⊢ □[(F ⟶ ○F)]_v ⟶ F ⟶ □F" by (rule ax3)
with g4[unlifted] have g5: "⊢ F ⟶ □F" by auto
with h1[unlifted] show ?thesis by auto
qed

text‹
Similar theorem, assuming that @{term "F"} is stuttering invariant.
›

theorem alw3:
assumes h1: "⊢ F" and h2: "stutinv F"
shows "⊢ □F"
proof -
from h2 have "|~ F ∧ Unchanged id ⟶ ○F"  by (rule pre_id_unch)
with h1 show ?thesis by (rule alw2)
qed

text‹
In a deep embedding, we could prove that all (proper) \tlastar{}
formulas are stuttering invariant and then get rid of the second
hypothesis of rule ‹alw3›. In fact, the rule is even true
for pre-formulas, as shown by the following rule, whose proof relies
on semantical reasoning.
›
theorem alw: assumes H1: "⊢ F" shows "⊢ □F"
using H1 by (auto simp: always_def)

theorem alw_valid_iff_valid: "(⊢ □F) = (⊢ F)"
proof
assume "⊢ □F"
from this ax1 show "⊢ F" by (rule fmp)
qed (rule alw)

text ‹
\cite{Merz99} proves the following theorem using the deduction theorem of
\tlastar{}: ‹(⊢ F ⟹ ⊢ G) ⟹ ⊢ []F ⟶ G›, which can only be
proved by induction on the formula structure, in a deep embedding.
›

theorem T1[simp_unl]: "⊢ □□F = []F"
proof (auto simp: always_def suffix_plus)
fix w n
assume "∀m k. (w |⇩s (k+m)) ⊨ F"
hence "(w |⇩s (n+0)) ⊨ F" by blast
thus "(w |⇩s n) ⊨ F" by simp
qed

theorem T2[simp_unl]: "⊢ □□[P]_v = □[P]_v"
proof -
have 1: "|~ □[P]_v ⟶ ○□[P]_v" using pax4 by force
hence "⊢ □[□[P]_v ⟶ ○□[P]_v]_v" by (rule sq)
moreover
have "⊢ □[ □[P]_v ⟶ ○□[P]_v ]_v ⟶ □[P]_v ⟶ □□[P]_v"
by (rule ax3) (auto elim: 1[unlift_rule])
moreover
have "⊢ □□[P]_v ⟶ □[P]_v" by (rule ax1)
ultimately show ?thesis by force
qed

theorem T3[simp_unl]: "⊢ □[[P]_v]_v = □[P]_v"
proof -
have "|~ P ⟶ [P]_v" by (auto simp: actrans_def)
hence "⊢ □[(P ⟶ [P]_v)]_v" by (rule sq)
with ax4 have "⊢ □[P]_v ⟶ □[[P]_v]_v" by force
moreover
have "|~ [P]_v ⟶ v≠ $v ⟶ P" by (auto simp: unch_def actrans_def) hence "⊢ □[[P]_v ⟶ v≠$v ⟶ P]_v" by (rule sq)
with ax5 have "⊢ □[[P]_v]_v ⟶ □[P]_v" by (force intro: ax4[unlift_rule])
ultimately show ?thesis by force
qed

theorem M2:
assumes h: "|~ F ⟶ G"
shows "⊢ □[F]_v ⟶ □[G]_v"
using sq[OF h] ax4 by force

theorem N1:
assumes h: "⊢ F ⟶ G"
shows "|~ ○F ⟶ ○G"
by (rule pmp[OF nex[OF h] pax2])

theorem T4: "⊢ □[P]_v ⟶ □[[P]_v]_w"
proof -
have "⊢ □□[P]_v ⟶ □[□□[P]_v]_w" by (rule ax2)
moreover
from pax4 have "|~ □□[P]_v ⟶ [P]_v" unfolding T2[int_rewrite] by force
hence "⊢ □[□□[P]_v]_w ⟶ □[[P]_v]_w" by (rule M2)
ultimately show ?thesis unfolding T2[int_rewrite] by (rule lift_imp_trans)
qed

theorem T5: "⊢ □[[P]_w]_v ⟶ □[[P]_v]_w"
proof -
have "|~ [[P]_w]_v ⟶ [[P]_v]_w" by (auto simp: actrans_def)
hence "⊢ □[[[P]_w]_v]_w ⟶ □[[[P]_v]_w]_w" by (rule M2)
with T4 show ?thesis unfolding T3[int_rewrite] by (rule lift_imp_trans)
qed

theorem T6: "⊢ □F ⟶ □[○F]_v"
proof -
from ax1 have "|~ ○(□F ⟶ F)" by (rule nex)
with pax2 have "|~ ○□F ⟶ ○F" by force
with pax3 have "|~ □F ⟶ ○F" by (rule pref_imp_trans)
hence "⊢ □[□F]_v ⟶ □[○F]_v" by (rule M2)
with ax2 show ?thesis by (rule lift_imp_trans)
qed

theorem T7:
assumes h: "|~ F ∧ Unchanged v ⟶ ○F"
shows "|~ (F ∧ ○□F) = □F"
proof -
have "⊢ □[○F ⟶ F ⟶ ○F]_v" by (rule sq) auto
with ax4 have "⊢ □[○F]_v ⟶ □[(F ⟶ ○F)]_v" by force
with ax3[OF h, unlifted] have "⊢ □[○F]_v ⟶ (F ⟶ □F)" by force
with pax5 have "|~ F ∧ ○□F ⟶ □F" by force
with ax1[of "TEMP F",unlifted] pax3[of "TEMP F",unlifted] show ?thesis by force
qed

theorem T8: "|~ ○(F ∧ G) = (○F ∧ ○G)"
proof -
have "|~ ○(F ∧ G) ⟶ ○F" by (rule N1) auto
moreover
have "|~ ○(F ∧ G) ⟶ ○G" by (rule N1) auto
moreover
have "⊢ F ⟶ G ⟶ F ∧ G" by auto
from nex[OF this] have "|~ ○F ⟶ ○G ⟶ ○(F ∧ G)"
by (force intro: pax2[unlift_rule])
ultimately show ?thesis by force
qed

lemma T9: "|~ □[A]_v ⟶ [A]_v"
using pax4 by force

theorem H1:
assumes h1: "⊢ □[P]_v" and h2: "⊢ □[P ⟶ Q]_v"
shows "⊢ □[Q]_v"
using assms ax4[unlifted] by force

theorem H2: assumes h1: "⊢ F" shows "⊢ □[F]_v"
using h1 by (blast dest: pre sq)

theorem H3:
assumes h1: "⊢ □[P ⟶ Q]_v" and h2: "⊢ □[Q ⟶ R]_v"
shows "⊢ □[P ⟶ R]_v"
proof -
have "|~ (P ⟶ Q) ⟶ (Q ⟶ R) ⟶ (P ⟶ R)" by auto
hence "⊢ □[(P ⟶ Q) ⟶ (Q ⟶ R) ⟶ (P ⟶ R)]_v" by (rule sq)
with h1 have "⊢ □[(Q ⟶ R) ⟶ (P ⟶ R)]_v" by (rule H1)
with h2 show ?thesis by (rule H1)
qed

theorem H4: "⊢ □[[P]_v ⟶ P]_v"
proof -
have "|~ v ≠ $v ⟶ ([P]_v ⟶ P)" by (auto simp: unch_def actrans_def) hence "⊢ □[v ≠$v ⟶ ([P]_v ⟶ P)]_v" by (rule sq)
with ax5 show ?thesis by (rule H1)
qed

theorem H5: "⊢ □[□F ⟶ ○□F]_v"
by (rule pax3[THEN sq])

subsection "Some other useful derived theorems"

theorem P1: "|~ □F ⟶ ○F"
proof -
have "|~ ○□F ⟶ ○F" by (rule N1[OF ax1])
with pax3 show ?thesis by (rule pref_imp_trans)
qed

theorem P2: "|~ □F ⟶ F ∧ ○F"
using ax1[of F] P1[of F] by force

theorem P4: "⊢ □F ⟶ □[F]_v"
proof -
have "⊢ □[□F]_v ⟶ □[F]_v" by (rule M2[OF pre[OF ax1]])
with ax2 show ?thesis by (rule lift_imp_trans)
qed

theorem P5: "⊢ □[P]_v ⟶ □[□[P]_v]_w"
proof -
have "⊢ □□[P]_v ⟶ □[□[P]_v]_w" by (rule P4)
thus ?thesis by (unfold T2[int_rewrite])
qed

theorem M0: "⊢ □F ⟶ □[F ⟶ ○F]_v"
proof -
from P1 have "|~ □F ⟶ F ⟶ ○F" by force
hence "⊢ □[□F]_v ⟶ □[F ⟶ ○F]_v" by (rule M2)
with ax2 show ?thesis by (rule lift_imp_trans)
qed

theorem M1: "⊢ □F ⟶ □[F ∧ ○F]_v"
proof -
have "|~ □F ⟶ F ∧ ○F" by (rule P2)
hence "⊢ □[□F]_v ⟶ □[F ∧ ○F]_v" by (rule M2)
with ax2 show ?thesis by (rule lift_imp_trans)
qed

theorem M3: assumes h: "⊢ F" shows "⊢ □[○F]_v"
using alw[OF h] T6 by (rule fmp)

lemma M4: "⊢ □[○(F ∧ G) = (○F ∧ ○G)]_v"
by (rule sq[OF T8])

theorem M5: "⊢ □[ □[P]_v ⟶ ○□[P]_v ]_w"
proof (rule sq)
show "|~ □[P]_v ⟶ ○□[P]_v" by (auto simp: pax4[unlifted])
qed

theorem M6: "⊢ □[F ∧ G]_v ⟶ □[F]_v ∧ □[G]_v"
proof -
have "⊢ □[F ∧ G]_v ⟶ □[F]_v" by (rule M2) auto
moreover
have "⊢ □[F ∧ G]_v ⟶ □[G]_v" by (rule M2) auto
ultimately show ?thesis by force
qed

theorem M7: "⊢ □[F]_v ∧ □[G]_v ⟶ □[F ∧ G]_v"
proof -
have "|~ F ⟶ G ⟶ F ∧ G" by auto
hence "⊢ □[F]_v ⟶ □[G ⟶ F ∧ G]_v" by (rule M2)
with ax4 show ?thesis by force
qed

theorem M8: "⊢ □[F ∧ G]_v = (□[F]_v ∧ □[G]_v)"
by (rule int_iffI[OF M6 M7])

theorem M9: "|~ □F ⟶ F ∧ ○□F"
using pre[OF ax1[of "F"]] pax3[of "F"] by force

theorem M10:
assumes h: "|~ F ∧ Unchanged v ⟶ ○F"
shows "|~ F ∧ ○□F ⟶ □F"
using T7[OF h] by auto

theorem M11:
assumes h: "|~ [A]_f ⟶ [B]_g"
shows "⊢ □[A]_f ⟶ □[B]_g"
proof -
from h have "⊢ □[[A]_f]_g ⟶ □[[B]_g]_g" by (rule M2)
with T4 show ?thesis by force
qed

theorem M12: "⊢ (□[A]_f ∧ □[B]_g) = □[[A]_f ∧ [B]_g]_(f,g)"
proof -
have "⊢ □[A]_f ∧ □[B]_g ⟶ □[[A]_f ∧ [B]_g]_(f,g)"
by (auto simp: M8[int_rewrite] elim: T4[unlift_rule])
moreover
have "|~ [[A]_f ∧ [B]_g]_(f,g) ⟶ [A]_f"
by (auto simp: actrans_def unch_def all_before_eq all_after_eq)
hence "⊢ □[[A]_f ∧ [B]_g]_(f,g) ⟶ □[A]_f" by (rule M11)
moreover
have "|~ [[A]_f ∧ [B]_g]_(f,g) ⟶ [B]_g"
by (auto simp: actrans_def unch_def all_before_eq all_after_eq)
hence "⊢ □[[A]_f ∧ [B]_g]_(f,g) ⟶ □[B]_g"
by (rule M11)
ultimately show ?thesis by force
qed

text ‹
We now derive Lamport's 6 simple temporal logic rules (STL1)-(STL6) \cite{Lamport94}.
Firstly, STL1 is the same as @{thm alw} derived above.
›

lemmas STL1 = alw

text ‹
STL2 and STL3 have also already been derived.
›

lemmas STL2 = ax1

lemmas STL3 = T1

text ‹
As with the derivation of @{thm alw}, a purely syntactic derivation of
(STL4) relies on an additional argument -- either using ‹Unchanged›
or ‹STUTINV›.
›

theorem STL4_2:
assumes h1: "⊢ F ⟶ G" and h2: "|~ G ∧ Unchanged v ⟶ ○G"
shows "⊢ □F ⟶ □G"
proof -
from ax1[of F] h1 have "⊢ □F ⟶ G" by (rule lift_imp_trans)
moreover
from h1 have "|~ ○F ⟶ ○G" by (rule N1)
hence "|~ ○F ⟶ G ⟶ ○G" by auto
hence "⊢ □[○F]_v ⟶ □[G ⟶ ○G]_v" by (rule M2)
with T6 have "⊢ □F ⟶ □[G ⟶ ○G]_v" by (rule lift_imp_trans)
moreover
from h2 have "⊢ □[G ⟶ ○G]_v ⟶ G ⟶ □G" by (rule ax3)
ultimately
show ?thesis by force
qed

lemma STL4_3:
assumes h1: "⊢ F ⟶ G" and h2: "STUTINV G"
shows "⊢ □F ⟶ □G"
using h1 h2[THEN pre_id_unch] by (rule STL4_2)

text ‹Of course, the original rule can be derived semantically›

lemma STL4: assumes h: "⊢ F ⟶ G" shows "⊢ □F ⟶ □G"
using h by (force simp: always_def)

text ‹Dual rule for ‹◇››

lemma STL4_eve: assumes h: "⊢ F ⟶ G" shows "⊢ ◇F ⟶ ◇G"
using h by (force simp: eventually_defs)

text‹
Similarly, a purely syntactic derivation of (STL5) requires extra hypotheses.
›

theorem STL5_2:
assumes h1: "|~ F ∧ Unchanged f ⟶ ○F"
and h2: "|~ G ∧ Unchanged g ⟶ ○G"
shows "⊢ □(F ∧ G) = (□F ∧ □G)"
proof (rule int_iffI)
have "⊢ F ∧ G ⟶ F" by auto
from this h1 have "⊢ □(F ∧ G) ⟶ □F" by (rule STL4_2)
moreover
have "⊢ F ∧ G ⟶ G" by auto
from this h2 have "⊢ □(F ∧ G) ⟶ □G" by (rule STL4_2)
ultimately show "⊢ □(F ∧ G) ⟶ □F ∧ □G" by force
next
have "|~ Unchanged (f,g) ⟶ Unchanged f ∧ Unchanged g" by (auto simp: unch_defs)
with h1[unlifted] h2[unlifted] T8[of F G, unlifted]
have h3: "|~ (F ∧ G) ∧ Unchanged (f,g) ⟶ ○(F ∧ G)" by force
from ax1[of F] ax1[of G] have "⊢ □F ∧ □G ⟶ F ∧ G" by force
moreover
from ax2[of F] ax2[of G] have "⊢ □F ∧ □G ⟶ □[□F]_(f,g) ∧ □[□G]_(f,g)" by force
with M8 have "⊢ □F ∧ □G ⟶ □[□F ∧ □G]_(f,g)" by force
moreover
from P1[of F] P1[of G] have "|~ □F ∧ □G ⟶ F ∧ G ⟶ ○(F ∧ G)"
unfolding T8[int_rewrite] by force
hence "⊢ □[ □F ∧ □G ]_(f,g) ⟶ □[F ∧ G ⟶ ○(F ∧ G)]_(f,g)" by (rule M2)
from this ax3[OF h3] have "⊢ □[ □F ∧ □G ]_(f,g) ⟶ F ∧ G ⟶ □(F ∧ G)"
by (rule lift_imp_trans)
ultimately show "⊢ □F ∧ □G ⟶ □(F ∧ G)" by force
qed

theorem STL5_21:
assumes h1: "stutinv F" and h2: "stutinv G"
shows "⊢ □(F ∧ G) = (□F ∧ □G)"
using h1[THEN pre_id_unch] h2[THEN pre_id_unch] by (rule STL5_2)

text ‹We also derive STL5 semantically.›

lemma STL5: "⊢ □(F ∧ G) = (□F ∧ □G)"
by (auto simp: always_def)

text ‹Elimination rule corresponding to ‹STL5› in unlifted form.›

lemma box_conjE:
assumes "s ⊨ □F" and "s ⊨ □G" and "s ⊨ □(F ∧ G) ⟹ P"
shows "P"
using assms by (auto simp: STL5[unlifted])

lemma box_thin:
assumes h1: "s ⊨ □F" and h2: "PROP W"
shows "PROP W"
using h2 .

text ‹Finally, we derive STL6 (only semantically)›

lemma STL6: "⊢ ◇□(F ∧ G) = (◇□F ∧ ◇□G)"
proof auto
fix w
assume a1: "w ⊨ ◇□F" and  a2: "w ⊨ ◇□G"
from a1 obtain nf where nf: "(w |⇩s nf) ⊨ □F" by (auto simp: eventually_defs)
from a2 obtain ng where ng: "(w |⇩s ng) ⊨ □G" by (auto simp: eventually_defs)
let ?n = "max nf ng"
have "nf ≤ ?n" by simp
from this nf have "(w |⇩s ?n) ⊨ □F" by (rule linalw)
moreover
have "ng ≤ ?n" by simp
from this ng have "(w |⇩s ?n) ⊨ □G" by (rule linalw)
ultimately
have "(w |⇩s ?n) ⊨ □(F ∧ G)" by (rule box_conjE)
thus "w ⊨ ◇□(F ∧ G)" by (auto simp: eventually_defs)
next
fix w
assume h: "w ⊨ ◇□(F ∧ G)"
have "⊢ F ∧ G ⟶ F" by auto
hence "⊢ ◇□(F ∧ G) ⟶ ◇□F" by (rule STL4_eve[OF STL4])
with h show "w ⊨ ◇□F" by auto
next
fix w
assume h: "w ⊨ ◇□(F ∧ G)"
have "⊢ F ∧ G ⟶ G" by auto
hence "⊢ ◇□(F ∧ G) ⟶ ◇□G" by (rule STL4_eve[OF STL4])
with h show "w ⊨ ◇□G" by auto
qed

lemma MM0: "⊢ □(F ⟶ G) ⟶ □F ⟶ □G"
proof -
have "⊢ □(F ∧ (F ⟶ G)) ⟶ □G" by (rule STL4) auto
thus ?thesis by (auto simp: STL5[int_rewrite])
qed

lemma MM1: assumes h: "⊢ F = G" shows "⊢ □F = □G"
by (auto simp: h[int_rewrite])

theorem MM2: "⊢ □A ∧ □(B ⟶ C) ⟶ □(A ∧ B ⟶ C)"
proof -
have "⊢ □(A ∧ (B ⟶ C)) ⟶ □(A ∧ B ⟶ C)" by (rule STL4) auto
thus ?thesis by (auto simp: STL5[int_rewrite])
qed

theorem MM3: "⊢ □¬A ⟶ □(A ∧ B ⟶ C)"
by (rule STL4) auto

theorem MM4[simp_unl]: "⊢ □#F = #F"
proof (cases "F")
assume "F"
hence 1: "⊢ #F" by auto
hence "⊢ □#F" by (rule alw)
with 1 show ?thesis by force
next
assume "¬F"
hence 1: "⊢ ¬ #F" by auto
from ax1 have "⊢ ¬ #F ⟶ ¬ □#F" by (rule lift_imp_neg)
with 1 show ?thesis by force
qed

theorem MM4b[simp_unl]: "⊢ □¬#F = ¬#F"
proof -
have "⊢ ¬#F = #(¬F)" by auto
hence "⊢ □¬#F = □#(¬F)" by (rule MM1)
thus ?thesis by auto
qed

theorem MM5: "⊢ □F ∨ □G ⟶ □(F ∨ G)"
proof -
have "⊢ □F ⟶ □(F ∨ G)" by (rule STL4) auto
moreover
have "⊢ □G ⟶ □(F ∨ G)" by (rule STL4) auto
ultimately show ?thesis by force
qed

theorem MM6: "⊢ □F ∨ □G ⟶ □(□F ∨ □G)"
proof -
have "⊢ □□F ∨ □□G ⟶ □(□F ∨ □G)" by (rule MM5)
thus ?thesis by simp
qed

lemma MM10:
assumes h: "|~ F = G" shows "⊢ □[F]_v = □[G]_v"
by (auto simp: h[int_rewrite])

lemma MM9:
assumes h: "⊢ F = G" shows "⊢ □[F]_v = □[G]_v"
by (rule MM10[OF pre[OF h]])

theorem MM11: "⊢ □[¬(P ∧ Q)]_v ⟶ □[P]_v ⟶ □[P ∧ ¬Q]_v"
proof -
have "⊢ □[¬(P ∧ Q)]_v ⟶ □[P ⟶ P ∧ ¬Q]_v" by (rule M2) auto
from this ax4 show ?thesis by (rule lift_imp_trans)
qed

theorem MM12[simp_unl]: "⊢ □[□[P]_v]_v = □[P]_v"
proof (rule int_iffI)
have "|~ □[P]_v ⟶ [P]_v" by (auto simp: pax4[unlifted])
hence "⊢ □[□[P]_v]_v ⟶ □[[P]_v]_v" by (rule M2)
thus "⊢ □[□[P]_v]_v ⟶ □[P]_v" by (unfold T3[int_rewrite])
next
have "⊢ □□[P]_v ⟶ □[□□[P]_v]_v" by (rule ax2)
thus "⊢ □[P]_v ⟶ □[□[P]_v]_v" by auto
qed

subsection "Theorems about the eventually operator"

― ‹rules to push negation inside modal operators, sometimes useful for rewriting›
theorem dualization:
"⊢ ¬□F = ◇¬F"
"⊢ ¬◇F = □¬F"
"⊢ ¬□[A]_v = ◇⟨¬A⟩_v"
"⊢ ¬◇⟨A⟩_v = □[¬A]_v"
unfolding eventually_def angle_action_def by simp_all

lemmas dualization_rew = dualization[int_rewrite]
lemmas dualization_unl = dualization[unlifted]

theorem E1: "⊢ ◇(F ∨ G) = (◇F ∨ ◇G)"
proof -
have "⊢ □¬(F ∨ G) = □(¬F ∧ ¬G)" by (rule MM1) auto
thus ?thesis unfolding eventually_def STL5[int_rewrite] by force
qed

theorem E3: "⊢ F ⟶ ◇F"
unfolding eventually_def by (force dest: ax1[unlift_rule])

theorem E4: "⊢ □F ⟶ ◇F"
by (rule lift_imp_trans[OF ax1 E3])

theorem E5: "⊢ □F ⟶ □◇F"
proof -
have "⊢ □□F ⟶ □◇F" by (rule STL4[OF E4])
thus ?thesis by simp
qed

theorem E6:  "⊢ □F ⟶ ◇□F"
using E4[of "TEMP □F"] by simp

theorem E7:
assumes h: "|~ ¬F ∧ Unchanged v ⟶ ○¬F"
shows      "|~ ◇F ⟶ F ∨ ○◇F"
proof -
from h have "|~ ¬F ∧ ○□¬F ⟶ □¬F" by (rule M10)
thus ?thesis by (auto simp: eventually_def)
qed

theorem E8: "⊢ ◇(F ⟶ G) ⟶ □F ⟶ ◇G"
proof -
have "⊢ □(F ∧ ¬G) ⟶ □¬(F ⟶ G)" by (rule STL4) auto
thus ?thesis unfolding eventually_def STL5[int_rewrite] by auto
qed

theorem E9: "⊢ □(F ⟶ G) ⟶ ◇F ⟶ ◇G"
proof -
have "⊢ □(F ⟶ G) ⟶ □(¬G ⟶ ¬F)" by (rule STL4) auto
with MM0[of "TEMP ¬G" "TEMP ¬F"] show ?thesis unfolding eventually_def by force
qed

theorem E10[simp_unl]: "⊢ ◇◇F = ◇F"
by (simp add: eventually_def)

theorem E22:
assumes h: "⊢ F = G"
shows "⊢ ◇F = ◇G"
by (auto simp: h[int_rewrite])

theorem E15[simp_unl]: "⊢ ◇#F = #F"
by (simp add: eventually_def)

theorem E15b[simp_unl]: "⊢ ◇¬#F = ¬#F"
by (simp add: eventually_def)

theorem E16: "⊢ ◇□F ⟶ ◇F"
by (rule STL4_eve[OF ax1])

text ‹An action version of STL6›

lemma STL6_act: "⊢ ◇(□[F]_v ∧ □[G]_w) = (◇□[F]_v ∧ ◇□[G]_w)"
proof -
have "⊢ (◇□(□[F]_v ∧ □[G]_w)) = ◇(□□[F]_v ∧ □□[G]_w)" by (rule E22[OF STL5])
thus ?thesis by (auto simp: STL6[int_rewrite])
qed

lemma SE1: "⊢ □F ∧ ◇G ⟶ ◇(□F ∧ G)"
proof -
have "⊢ □¬(□F ∧ G) ⟶ □(□F ⟶ ¬G)" by (rule STL4) auto
with MM0 show ?thesis by (force simp: eventually_def)
qed

lemma SE2: "⊢ □F ∧ ◇G ⟶ ◇(F ∧ G)"
proof -
have "⊢ □F ∧ G ⟶ F ∧ G" by (auto elim: ax1[unlift_rule])
hence "⊢ ◇(□F ∧ G) ⟶ ◇(F ∧ G)" by (rule STL4_eve)
with SE1 show ?thesis by (rule lift_imp_trans)
qed

lemma SE3: "⊢ □F ∧ ◇G ⟶ ◇(G ∧ F)"
proof -
have "⊢ ◇(F ∧ G) ⟶ ◇(G ∧ F)" by (rule STL4_eve) auto
with SE2 show ?thesis by (rule lift_imp_trans)
qed

lemma SE4:
assumes h1: "s ⊨ □F" and  h2: "s ⊨ ◇G" and  h3: "⊢ □F ∧ G ⟶ H"
shows "s ⊨ ◇H"
using h1 h2 h3[THEN STL4_eve] SE1 by force

theorem E17: "⊢ □◇□F ⟶ □◇F"
by (rule STL4[OF STL4_eve[OF ax1]])

theorem E18: "⊢ □◇□F ⟶ ◇□F"
by (rule ax1)

theorem E19: "⊢ ◇□F ⟶ □◇□F"
proof -
have "⊢ (□F ∧ ¬□F) = #False" by auto
hence "⊢ ◇□(□F ∧ ¬□F) = ◇□#False" by (rule E22[OF MM1])
thus ?thesis unfolding STL6[int_rewrite] by (auto simp: eventually_def)
qed

theorem E20: "⊢ ◇□F ⟶ □◇F"
by (rule lift_imp_trans[OF E19 E17])

theorem E21[simp_unl]: "⊢ □◇□F = ◇□F"
by (rule int_iffI[OF E18 E19])

theorem E27[simp_unl]: "⊢ ◇□◇F = □◇F"
using E21 unfolding eventually_def by force

lemma E28: "⊢ ◇□F ∧ □◇G ⟶ □◇(F ∧ G)"
proof -
have "⊢ ◇□(□F ∧ ◇G) ⟶ ◇□◇(F ∧ G)" by (rule STL4_eve[OF STL4[OF SE2]])
thus ?thesis by (simp add: STL6[int_rewrite])
qed

lemma E23: "|~ ○F ⟶ ◇F"
using P1 by (force simp: eventually_def)

lemma E24: "⊢ ◇□Q ⟶ □[◇Q]_v"
by (rule lift_imp_trans[OF E20 P4])

lemma E25: "⊢ ◇⟨A⟩_v ⟶ ◇A"
using P4 by (force simp: eventually_def angle_action_def)

lemma E26: "⊢ □◇⟨A⟩_v ⟶ □◇A"
by (rule STL4[OF E25])

lemma allBox: "(s ⊨ □(∀x. F x)) = (∀x. s ⊨ □(F x))"
unfolding allT[unlifted] ..

lemma E29: "|~ ○◇F ⟶ ◇F"
unfolding eventually_def using pax3 by force

lemma E30:
assumes h1: "⊢ F ⟶ □F" and h2: "⊢ ◇F"
shows "⊢ ◇□F"
using h2 h1[THEN STL4_eve] by (rule fmp)

lemma E31: "⊢ □(F ⟶ □F) ∧ ◇F ⟶ ◇□F"
proof -
have "⊢ □(F ⟶ □F) ∧ ◇F ⟶ ◇(□(F ⟶ □F) ∧ F)" by (rule SE1)
moreover
have "⊢ □(F ⟶ □F) ∧ F ⟶ □F" using ax1[of "TEMP F ⟶ □F"] by auto
hence "⊢ ◇(□(F ⟶ □F) ∧ F) ⟶ ◇□F" by (rule STL4_eve)
ultimately show ?thesis by (rule lift_imp_trans)
qed

lemma allActBox: "(s ⊨ □[(∀x. F x)]_v) = (∀x. s ⊨ □[(F x)]_v)"
unfolding allActT[unlifted] ..

theorem exEE: "⊢ (∃x. ◇(F x)) = ◇(∃x. F x)"
proof -
have "⊢ ¬(∃ x. ◇(F x)) = ¬◇(∃ x. F x)"
by (auto simp: eventually_def Not_Rex[int_rewrite] allBox)
thus ?thesis by force
qed

theorem exActE: "⊢ (∃x. ◇⟨F x⟩_v) = ◇⟨(∃x. F x)⟩_v"
proof -
have "⊢ ¬(∃x. ◇⟨F x⟩_v) = ¬◇⟨(∃x. F x)⟩_v"
by (auto simp: angle_action_def Not_Rex[int_rewrite] allActBox)
thus ?thesis by force
qed

theorem LT1: "⊢ F ↝ F"
unfolding leadsto_def by (rule alw[OF E3])

theorem LT2: assumes h: "⊢ F ⟶ G" shows "⊢ F ⟶ ◇G"
by (rule lift_imp_trans[OF h E3])

theorem LT3: assumes h: "⊢ F ⟶ G" shows "⊢ F ↝ G"
unfolding leadsto_def by (rule alw[OF LT2[OF h]])

theorem LT4: "⊢ F ⟶ (F ↝ G) ⟶ ◇G"
unfolding leadsto_def using ax1[of "TEMP F ⟶ ◇G"] by auto

theorem LT5: "⊢ □(F ⟶ ◇G) ⟶ ◇F ⟶ ◇G"
using E9[of "F" "TEMP ◇G"] by simp

theorem LT6: "⊢ ◇F ⟶ (F ↝ G) ⟶ ◇G"
unfolding leadsto_def using LT5[of "F" "G"] by auto

theorem LT9[simp_unl]: "⊢ □(F ↝ G) = (F ↝ G)"
by (auto simp: leadsto_def)

theorem LT7: "⊢ □◇F ⟶ (F ↝ G) ⟶ □◇G"
proof -
have "⊢ □◇F ⟶ □((F ↝ G) ⟶ ◇G)" by (rule STL4[OF LT6])
from lift_imp_trans[OF this MM0] show ?thesis by simp
qed

theorem LT8: "⊢ □◇G ⟶ (F ↝ G)"
unfolding leadsto_def by (rule STL4) auto

theorem LT13: "⊢ (F ↝ G) ⟶ (G ↝ H) ⟶ (F ↝ H)"
proof -
have "⊢ ◇G ⟶ (G ↝ H) ⟶ ◇H" by (rule LT6)
hence "⊢ □(F ⟶ ◇G) ⟶ □((G ↝ H) ⟶ (F ⟶ ◇H))" by (intro STL4) auto
from lift_imp_trans[OF this MM0] show ?thesis by (simp add: leadsto_def)
qed

theorem LT11: "⊢ (F ↝ G) ⟶ (F ↝ (G ∨ H))"
proof -
have "⊢ G ↝ (G ∨ H)" by (rule LT3) auto
with LT13[of "F" "G" "TEMP (G ∨ H)"] show ?thesis by force
qed

theorem LT12: "⊢ (F ↝ H) ⟶  (F ↝ (G ∨ H))"
proof -
have "⊢ H ↝ (G ∨ H)" by (rule LT3) auto
with LT13[of "F" "H" "TEMP (G ∨ H)"] show ?thesis by force
qed

theorem LT14: "⊢ ((F ∨ G) ↝ H) ⟶ (F ↝ H)"
unfolding leadsto_def by (rule STL4) auto

theorem LT15: "⊢ ((F ∨ G) ↝ H) ⟶ (G ↝ H)"
unfolding leadsto_def by (rule STL4) auto

theorem LT16: "⊢ (F ↝ H) ⟶ (G ↝ H) ⟶ ((F ∨ G) ↝ H)"
proof -
have "⊢ □(F ⟶ ◇H) ⟶ □((G ⟶ ◇H) ⟶ (F ∨ G ⟶ ◇H))" by (rule STL4) auto
from lift_imp_trans[OF this MM0] show ?thesis by (unfold leadsto_def)
qed

theorem LT17: "⊢ ((F ∨ G) ↝ H) = ((F ↝ H) ∧ (G ↝ H))"
by (auto elim: LT14[unlift_rule] LT15[unlift_rule]
LT16[unlift_rule])

theorem LT10:
assumes h: "⊢ (F ∧ ¬G) ↝ G"
shows "⊢ F ↝ G"
proof -
from h have "⊢ ((F ∧ ¬G) ∨ G) ↝ G"
by (auto simp: LT17[int_rewrite] LT1[int_rewrite])
moreover
have "⊢ F ↝ ((F ∧ ¬G) ∨ G)" by (rule LT3, auto)
ultimately
show ?thesis by (force elim: LT13[unlift_rule])
qed

theorem LT18: "⊢ (A ↝ (B ∨ C)) ⟶ (B ↝ D) ⟶ (C ↝ D) ⟶ (A ↝ D)"
proof -
have "⊢ (B ↝ D) ⟶ (C ↝ D) ⟶ ((B ∨ C) ↝ D)" by (rule LT16)
thus ?thesis by (force elim: LT13[unlift_rule])
qed

theorem LT19: "⊢ (A ↝ (D ∨ B)) ⟶ (B ↝ D) ⟶ (A ↝ D)"
using LT18[of "A" "D" "B" "D"] LT1[of "D"] by force

theorem LT20: "⊢ (A ↝ (B ∨ D)) ⟶ (B ↝ D) ⟶ (A ↝ D)"
using LT18[of "A" "B" "D" "D"] LT1[of "D"] by force

theorem LT21: "⊢ ((∃x. F x) ↝ G) = (∀x. (F x ↝ G))"
proof -
have "⊢ □((∃x. F x) ⟶ ◇G) = □(∀x. (F x ⟶ ◇G))" by (rule MM1) auto
thus ?thesis by (unfold leadsto_def allT[int_rewrite])
qed

theorem LT22: "⊢ (F ↝ (G ∨ H)) ⟶ □¬G ⟶ (F ↝ H)"
proof -
have "⊢ □¬G ⟶ (G ↝ H)" unfolding leadsto_def by (rule STL4) auto
thus ?thesis by (force elim: LT20[unlift_rule])
qed

lemma LT23: "|~ (P ⟶ ○Q) ⟶ (P ⟶ ◇Q)"
by (auto dest: E23[unlift_rule])

theorem LT24: "⊢ □I ⟶ ((P ∧ I) ↝ Q) ⟶ P ↝ Q"
proof -
have "⊢ □I ⟶ □((P ∧ I ⟶ ◇Q) ⟶ (P ⟶ ◇Q))" by (rule STL4) auto
from lift_imp_trans[OF this MM0] show ?thesis by (unfold leadsto_def)
qed

theorem LT25[simp_unl]: "⊢ (F ↝ #False) = □¬F"
unfolding leadsto_def proof (rule MM1)
show "⊢ (F ⟶ ◇#False) = ¬F" by simp
qed

lemma LT28:
assumes h: "|~ P ⟶ ○P ∨ ○Q"
shows "|~ (P ⟶ ○P) ∨ ◇Q"
using h E23[of Q] by force

lemma LT29:
assumes h1: "|~ P ⟶ ○P ∨ ○Q" and   h2: "|~ P ∧ Unchanged v ⟶ ○P"
shows "⊢ P ⟶ □P ∨ ◇Q"
proof -
from h1[THEN LT28] have "|~ □¬Q ⟶ (P ⟶ ○P)" unfolding eventually_def by auto
hence "⊢ □[□¬Q]_v ⟶ □[P ⟶ ○P]_v" by (rule M2)
moreover
have "⊢ ¬◇Q ⟶ □[□¬Q]_v" unfolding dualization_rew by (rule ax2)
moreover
note ax3[OF h2]
ultimately
show ?thesis by force
qed

lemma LT30:
assumes h: "|~ P ∧ N ⟶ ○P ∨ ○Q"
shows "|~ N ⟶ (P ⟶ ○P) ∨ ◇Q"
using h E23 by force

lemma LT31:
assumes h1: "|~ P ∧ N ⟶ ○P ∨ ○Q" and h2: "|~ P ∧ Unchanged v ⟶ ○P"
shows"⊢ □N ⟶ P ⟶ □P ∨ ◇Q"
proof -
from h1[THEN LT30] have "|~ N ⟶ □¬Q ⟶ P ⟶ ○P" unfolding eventually_def by auto
hence "⊢ □[N ⟶ □¬Q ⟶ P ⟶ ○P]_v" by (rule sq)
hence "⊢ □[N]_v ⟶ □[□¬Q]_v ⟶ □[P ⟶ ○P]_v"
by (force intro: ax4[unlift_rule])
with P4 have "⊢ □N ⟶ □[□¬Q]_v ⟶ □[P ⟶ ○P]_v" by (rule lift_imp_trans)
moreover
have "⊢ ¬◇Q ⟶ □[□¬Q]_v" unfolding dualization_rew by (rule ax2)
moreover
note ax3[OF h2]
ultimately
show ?thesis by force
qed

lemma LT33: "⊢ ((#P ∧ F) ↝ G) = (#P ⟶ (F ↝ G))"
by (cases "P", auto simp: leadsto_def)

lemma AA1: "⊢ □[#False]_v ⟶ ¬◇⟨Q⟩_v"
unfolding dualization_rew by (rule M2) auto

lemma AA2: "⊢ □[P]_v ∧ ◇⟨Q⟩_v ⟶ ◇⟨P ∧ Q⟩_v"
proof -
have "⊢ □[P ⟶ ~(P ∧ Q) ⟶ ¬Q]_v" by (rule sq) (auto simp: actrans_def)
hence "⊢ □[P]_v ⟶ □[~(P ∧ Q)]_v ⟶ □[¬Q]_v"
by (force intro: ax4[unlift_rule])
thus ?thesis by (auto simp: angle_action_def)
qed

lemma AA3: "⊢ □P ∧ □[P ⟶ Q]_v ∧ ◇⟨A⟩_v ⟶ ◇Q"
proof -
have "⊢ □P ∧ □[P ⟶ Q]_v ⟶ □[P ∧ (P ⟶ Q)]_v"
by (auto dest: P4[unlift_rule] simp: M8[int_rewrite])
moreover
have "⊢ □[P ∧ (P ⟶ Q)]_v ⟶ □[Q]_v" by (rule M2) auto
ultimately have "⊢ □P ∧ □[P ⟶ Q]_v ⟶ □[Q]_v" by (rule lift_imp_trans)
moreover
have "⊢ ◇(Q ∧ A) ⟶ ◇Q" by (rule STL4_eve) auto
hence "⊢ ◇⟨Q ∧ A⟩_v ⟶ ◇Q" by (force dest: E25[unlift_rule])
with AA2 have "⊢ □[Q]_v ∧ ◇⟨A⟩_v ⟶ ◇Q" by (rule lift_imp_trans)
ultimately show ?thesis by force
qed

lemma AA4: "⊢ ◇⟨⟨A⟩_v⟩_w ⟶ ◇⟨⟨A⟩_w⟩_v"
unfolding angle_action_def angle_actrans_def using T5 by force

lemma AA7: assumes h: "|~ F ⟶ G" shows "⊢ ◇⟨F⟩_v ⟶ ◇⟨G⟩_v"
proof -
from h have "⊢ □[¬G]_v ⟶ □[¬F]_v" by (intro M2) auto
thus ?thesis unfolding angle_action_def by force
qed

lemma AA6: "⊢ □[P ⟶ Q]_v ∧ ◇⟨P⟩_v ⟶ ◇⟨Q⟩_v"
proof -
have "⊢ ◇⟨(P ⟶ Q) ∧ P⟩_v ⟶ ◇⟨Q⟩_v" by (rule AA7) auto
with AA2 show ?thesis by (rule lift_imp_trans)
qed

lemma AA8: "⊢ □[P]_v ∧ ◇⟨A⟩_v ⟶ ◇⟨□[P]_v ∧ A⟩_v"
proof -
have "⊢ □[□[P]_v]_v ∧ ◇⟨A⟩_v ⟶ ◇⟨□[P]_v ∧ A⟩_v" by (rule AA2)
with P5 show ?thesis by force
qed

lemma AA9: "⊢ □[P]_v ∧ ◇⟨A⟩_v ⟶ ◇⟨[P]_v ∧ A⟩_v"
proof -
have "⊢ □[[P]_v]_v ∧ ◇⟨A⟩_v ⟶ ◇⟨[P]_v ∧ A⟩_v" by (rule AA2)
thus ?thesis by simp
qed

lemma AA10: "⊢ ¬(□[P]_v ∧ ◇⟨¬P⟩_v)"
unfolding angle_action_def by auto

lemma AA11: "⊢ ¬◇⟨v$=$v⟩_v"
unfolding dualization_rew by (rule ax5)

lemma AA15: "⊢ ◇⟨P ∧ Q⟩_v ⟶ ◇⟨P⟩_v"
by (rule AA7) auto

lemma AA16: "⊢ ◇⟨P ∧ Q⟩_v ⟶ ◇⟨Q⟩_v"
by (rule AA7) auto

lemma AA13: "⊢ ◇⟨P⟩_v ⟶ ◇⟨v$≠$v⟩_v"
proof -
have "⊢ □[v$≠$v]_v ∧ ◇⟨P⟩_v ⟶ ◇⟨v$≠$v ∧ P⟩_v" by (rule AA2)
hence "⊢ ◇⟨P⟩_v ⟶ ◇⟨v$≠$v ∧ P⟩_v" by (simp add: ax5[int_rewrite])
from this AA15 show ?thesis by (rule lift_imp_trans)
qed

lemma AA14: "⊢ ◇⟨P ∨ Q⟩_v = (◇⟨P⟩_v ∨ ◇⟨Q⟩_v)"
proof -
have "⊢ □[¬(P ∨ Q)]_v = □[¬P ∧ ¬Q]_v" by (rule MM10) auto
hence "⊢ □[¬(P ∨ Q)]_v = (□[¬P]_v ∧ □[¬Q]_v)" by (unfold M8[int_rewrite])
thus ?thesis unfolding angle_action_def by auto
qed

lemma AA17: "⊢ ◇⟨[P]_v ∧ A⟩_v ⟶ ◇⟨P ∧ A⟩_v"
proof -
have "⊢ □[v$≠$v ∧ ¬(P ∧ A)]_v ⟶ □[¬([P]_v ∧ A)]_v"
by (rule M2) (auto simp: actrans_def unch_def)
with ax5[of "v"] show ?thesis
unfolding angle_action_def M8[int_rewrite] by force
qed

lemma AA19: "⊢ □P ∧ ◇⟨A⟩_v ⟶ ◇⟨P ∧ A⟩_v"
using P4 by (force intro: AA2[unlift_rule])

lemma AA20:
assumes h1: "|~ P ⟶ ○P ∨ ○Q"
and  h2: "|~ P ∧ A ⟶ ○Q"
and  h3: "|~ P ∧ Unchanged w ⟶ ○P"
shows "⊢ □(□P ⟶ ◇⟨A⟩_v) ⟶ (P ↝ Q)"
proof -
from h2 E23 have "|~ P ∧ A ⟶ ◇Q" by force
hence "⊢ ◇⟨P ∧ A⟩_v ⟶ ◇⟨◇Q⟩_v" by (rule AA7)
with E25[of "TEMP ◇Q" "v"] have "⊢ ◇⟨P ∧ A⟩_v ⟶ ◇Q" by force
with AA19 have "⊢ □P ∧ ◇⟨A⟩_v ⟶ ◇Q" by (rule lift_imp_trans)
with LT29[OF h1 h3] have "⊢ (□P ⟶ ◇⟨A⟩_v) ⟶ (P ⟶ ◇Q)" by force
thus ?thesis unfolding leadsto_def by (rule STL4)
qed

lemma AA21: "|~ ◇⟨○F⟩_v ⟶ ○◇F"
using pax5[of "TEMP ¬F" "v"] unfolding angle_action_def eventually_def by auto

theorem AA24[simp_unl]: "⊢ ◇⟨⟨P⟩_f⟩_f = ◇⟨P⟩_f"
unfolding angle_action_def angle_actrans_def by simp

lemma AA22:
assumes h1: "|~ P ∧ N ⟶ ○P ∨ ○Q"
and  h2: "|~ P ∧ N ∧ ⟨A⟩_v ⟶ ○Q"
and  h3: "|~ P ∧ Unchanged w ⟶ ○P"
shows "⊢ □N ∧ □(□P ⟶ ◇⟨A⟩_v) ⟶ (P ↝ Q)"
proof -
from h2 have "|~ ⟨(N ∧ P) ∧ A⟩_v ⟶ ○Q" by (auto simp: angle_actrans_sem[int_rewrite])
from pref_imp_trans[OF this E23] have "⊢ ◇⟨⟨(N ∧ P) ∧ A⟩_v⟩_v ⟶ ◇⟨◇Q⟩_v" by (rule AA7)
hence "⊢ ◇⟨(N ∧ P) ∧ A⟩_v ⟶ ◇Q" by (force dest: E25[unlift_rule])
with AA19 have "⊢ □(N ∧ P) ∧ ◇⟨A⟩_v ⟶ ◇Q" by (rule lift_imp_trans)
hence "⊢ □N ∧ □P ∧ ◇⟨A⟩_v ⟶ ◇Q" by (auto simp: STL5[int_rewrite])
with LT31[OF h1 h3] have "⊢ □N ∧ (□P ⟶ ◇⟨A⟩_v) ⟶ (P ⟶ ◇Q)" by force
hence "⊢ □(□N ∧ (□P ⟶ ◇⟨A⟩_v)) ⟶ □(P ⟶ ◇Q)" by (rule STL4)
thus ?thesis by (simp add: leadsto_def STL5[int_rewrite])
qed

lemma AA23:
assumes "|~ P ∧ N ⟶ ○P ∨ ○Q"
and  "|~ P ∧ N ∧ ⟨A⟩_v ⟶ ○Q"
and  "|~ P ∧ Unchanged w ⟶ ○P"
shows "⊢ □N ∧ □◇⟨A⟩_v ⟶ (P ↝ Q)"
proof -
have "⊢ □◇⟨A⟩_v ⟶ □(□P ⟶ ◇⟨A⟩_v)" by (rule STL4) auto
with AA22[OF assms] show ?thesis by force
qed

lemma AA25:
assumes h: "|~ ⟨P⟩_v ⟶ ⟨Q⟩_w"
shows "⊢ ◇⟨P⟩_v ⟶ ◇⟨Q⟩_w"
proof -
from h have "⊢ ◇⟨⟨P⟩_v⟩_v ⟶ ◇⟨⟨P⟩_w⟩_v"
by (intro AA7) (auto simp: angle_actrans_def actrans_def)
with AA4 have "⊢ ◇⟨P⟩_v ⟶ ◇⟨⟨P⟩_v⟩_w" by force
from this AA7[OF h] have "⊢ ◇⟨P⟩_v ⟶ ◇⟨⟨Q⟩_w⟩_w" by (rule lift_imp_trans)
thus ?thesis by simp
qed

lemma AA26:
assumes h: "|~ ⟨A⟩_v = ⟨B⟩_w"
shows "⊢ ◇⟨A⟩_v = ◇⟨B⟩_w"
proof -
from h have "|~ ⟨A⟩_v ⟶ ⟨B⟩_w" by auto
hence "⊢ ◇⟨A⟩_v ⟶ ◇⟨B⟩_w" by (rule AA25)
moreover
from h have "|~ ⟨B⟩_w ⟶ ⟨A⟩_v" by auto
hence "⊢ ◇⟨B⟩_w ⟶ ◇⟨A⟩_v" by (rule AA25)
ultimately
show ?thesis by force
qed

theorem AA28[simp_unl]: "⊢ ◇◇⟨A⟩_v = ◇⟨A⟩_v"
unfolding eventually_def angle_action_def by simp

theorem AA29: "⊢ □[N]_v ∧ □◇⟨A⟩_v ⟶ □◇⟨N ∧ A⟩_v"
proof -
have "⊢ □(□[N]_v ∧ ◇⟨A⟩_v) ⟶ □◇⟨N ∧ A⟩_v" by (rule STL4[OF AA2])
thus ?thesis by (simp add: STL5[int_rewrite])
qed

theorem AA30[simp_unl]: "⊢ ◇⟨◇⟨P⟩_f⟩_f = ◇⟨P⟩_f"
unfolding angle_action_def by simp

theorem AA31: "⊢ ◇⟨○F⟩_v ⟶ ◇F"
using pref_imp_trans[OF AA21 E29] by auto

lemma AA32[simp_unl]: "⊢ □◇□[A]_v = ◇□[A]_v"
using E21[of "TEMP □[A]_v"] by simp

lemma AA33[simp_unl]: "⊢ ◇□◇⟨A⟩_v = □◇⟨A⟩_v"
using E27[of "TEMP ◇⟨A⟩_v"] by simp

subsection "Lemmas about the next operator"

lemma N2: assumes h: "⊢ F = G" shows "|~ ○F = ○G"
by (simp add: h[int_rewrite])

lemmas next_and = T8

lemma next_or: "|~ ○(F ∨ G) = (○F ∨ ○G)"
proof (rule pref_iffI)
have "|~ ○((F ∨ G) ∧ ¬F) ⟶ ○G" by (rule N1) auto
thus "|~ ○(F ∨ G) ⟶ ○F ∨ ○G" by (auto simp: T8[int_rewrite])
next
have "|~ ○F ⟶ ○(F ∨ G)" by (rule N1) auto
moreover have "|~ ○G ⟶ ○(F ∨ G)" by (rule N1) auto
ultimately show "|~ ○F ∨ ○G ⟶ ○(F ∨ G)" by force
qed

lemma next_imp: "|~ ○(F ⟶ G) = (○F ⟶ ○G)"
proof (rule pref_iffI)
have "|~ ○G ⟶ ○(F ⟶ G)" by (rule N1) auto
moreover have "|~ ○¬F ⟶ ○(F ⟶ G)" by (rule N1) auto
ultimately show "|~ (○F ⟶ ○G) ⟶ ○(F ⟶ G)" by force
qed (rule pax2)

lemmas next_not = pax1

lemma next_eq: "|~ ○(F = G) = (○F = ○G)"
proof -
have "|~ ○(F = G) = ○((F ⟶ G) ∧ (G ⟶ F))" by (rule N2) auto
from this[int_rewrite] show ?thesis
by (auto simp: next_and[int_rewrite] next_imp[int_rewrite])
qed

lemma next_noteq: "|~ ○(F ≠ G) = (○F ≠ ○G)"
by (simp add: next_eq[int_rewrite])

lemma next_const[simp_unl]: "|~ ○#P = #P"
proof (cases "P")
assume "P"
hence 1: "⊢ #P" by auto
hence "|~ ○#P" by (rule nex)
with 1 show ?thesis by force
next
assume "¬P"
hence 1: "⊢ ¬#P" by auto
hence "|~ ○¬#P" by (rule nex)
with 1 show ?thesis by force
qed

text ‹
The following are proved semantically because they are essentially
first-order theorems.
›
lemma next_fun1: "|~ ○f<x> = f<○x>"
by (auto simp: nexts_def)

lemma next_fun2: "|~ ○f<x,y> = f<○x,○y>"
by (auto simp: nexts_def)

lemma next_fun3: "|~ ○f<x,y,z> = f<○x,○y,○z>"
by (auto simp: nexts_def)

lemma next_fun4: "|~ ○f<x,y,z,zz> = f<○x,○y,○z,○zz>"
by (auto simp: nexts_def)

lemma next_forall: "|~ ○(∀ x. P x) = (∀ x. ○ P x)"
by (auto simp: nexts_def)

lemma next_exists: "|~ ○(∃ x. P x) = (∃ x. ○ P x)"
by (auto simp: nexts_def)

lemma next_exists1: "|~ ○(∃! x. P x) = (∃! x. ○ P x)"
by (auto simp: nexts_def)

text ‹
Rewrite rules to push the next'' operator inward over connectives.
(Note that axiom ‹pax1› and theorem ‹next_const› are anyway active
as rewrite rules.)
›
lemmas next_commutes[int_rewrite] =
next_and next_or next_imp next_eq
next_fun1 next_fun2 next_fun3 next_fun4
next_forall next_exists next_exists1

lemmas ifs_eq[int_rewrite] = after_fun3 next_fun3 before_fun3

lemmas next_always = pax3

lemma t1: "|~ ○$x = x$"
by (simp add: before_def after_def nexts_def first_tail_second)

text ‹
Theorem ‹next_eventually› should not be used "blindly".
›
lemma next_eventually:
assumes h: "stutinv F"
shows "|~ ◇F ⟶ ¬F ⟶ ○◇F"
proof -
from h have 1: "stutinv (TEMP ¬F)" by (rule stut_not)
have "|~ □¬F = (¬F ∧ ○□¬F)" unfolding T7[OF pre_id_unch[OF 1], int_rewrite] by simp
thus ?thesis by (auto simp: eventually_def)
qed

lemma next_action: "|~ □[P]_v ⟶ ○□[P]_v"
using pax4[of P v] by auto

subsection "Higher Level Derived Rules"

text ‹
In most verification tasks the low-level rules discussed above are not used directly.
Here, we derive some higher-level rules more suitable for verification. In particular,
variants of Lamport's rules ‹TLA1›, ‹TLA2›, ‹INV1› and ‹INV2›
are derived, where ‹|~› is used where appropriate.
›

theorem TLA1:
assumes H: "|~ P ∧ Unchanged f ⟶ ○P"
shows "⊢ □P = (P ∧ □[P ⟶ ○P]_f)"
proof (rule int_iffI)
from ax1[of P] M0[of P f] show "⊢ □P ⟶ P ∧ □[P ⟶ ○P]_f" by force
next
from ax3[OF H] show "⊢ P ∧ □[P ⟶ ○P]_f ⟶ □P" by auto
qed

theorem TLA2:
assumes h1: "⊢ P ⟶ Q"
and h2: "|~ P ∧ ○P ∧ [A]_f ⟶ [B]_g"
shows "⊢ □P ∧ □[A]_f ⟶ □Q ∧ □[B]_g"
proof -
from h2 have "⊢ □[P ∧ ○P ∧ [A]_f]_g ⟶ □[[B]_g]_g" by (rule M2)
hence "⊢ □[P ∧ ○P]_g ∧ □[[A]_f]_g ⟶ □[B]_g" by (auto simp add: M8[int_rewrite])
with M1[of P g] T4[of A f g] have "⊢ □P ∧ □[A]_f ⟶ □[B]_g" by force
with h1[THEN STL4] show ?thesis by force
qed

theorem INV1:
assumes H: "|~ I ∧ [N]_f ⟶ ○I"
shows "⊢ I ∧ □[N]_f ⟶ □I"
proof -
from H have "|~ [N]_f ⟶ I ⟶ ○I" by auto
hence "⊢ □[[N]_f]_f ⟶ □[I ⟶ ○I]_f" by (rule M2)
moreover
from H have "|~ I ∧ Unchanged f ⟶ ○I" by (auto simp: actrans_def)
hence "⊢ □[I ⟶ ○I]_f ⟶ I ⟶ □I" by (rule ax3)
ultimately show ?thesis by force
qed

theorem INV2: "⊢ □I ⟶ □[N]_f = □[N ∧ I ∧ ○I]_f"
proof -
from M1[of I f] have "⊢ □I ⟶ (□[N]_f = □[N]_f ∧ □[I ∧ ○I]_f)" by auto
thus ?thesis by (auto simp: M8[int_rewrite])
qed

lemma R1:
assumes H: "|~ Unchanged w ⟶ Unchanged v"
shows "⊢ □[F]_w ⟶ □[F]_v"
proof -
from H have "|~ [F]_w ⟶ [F]_v" by (auto simp: actrans_def)
thus ?thesis by (rule M11)
qed

theorem invmono:
assumes h1: "⊢ I ⟶ P"
and h2: "|~ P ∧ [N]_f ⟶ ○P"
shows "⊢ I ∧ □[N]_f ⟶ □P"
using h1 INV1[OF h2] by force

theorem preimpsplit:
assumes "|~ I ∧ N ⟶ Q"
and "|~ I ∧ Unchanged v ⟶ Q"
shows "|~ I ∧ [N]_v ⟶ Q"
using assms[unlift_rule] by (auto simp: actrans_def)

theorem refinement1:
assumes h1: "⊢ P ⟶ Q"
and h2: "|~ I ∧ ○I ∧ [A]_f ⟶ [B]_g"
shows "⊢ P ∧ □I ∧ □[A]_f ⟶ Q ∧ □[B]_g"
proof -
have "⊢ I ⟶ #True" by simp
from this h2 have "⊢ □I ∧ □[A]_f ⟶ □#True ∧ □[B]_g" by (rule TLA2)
with h1 show ?thesis by force
qed

theorem inv_join:
assumes "⊢ P ⟶ □Q" and "⊢ P ⟶ □R"
shows "⊢ P ⟶ □(Q ∧ R)"
using assms[unlift_rule] unfolding STL5[int_rewrite] by force

lemma inv_cases: "⊢ □(A ⟶ B) ∧ □(¬A ⟶ B) ⟶ □B"
proof -
have "⊢ □((A ⟶ B) ∧ (¬A ⟶ B)) ⟶ □B" by (rule STL4) auto
thus ?thesis by (simp add: STL5[int_rewrite])
qed

end


# Theory Liveness

(*  Title:       A Definitional Encoding of TLA in Isabelle/HOL
Authors:     Gudmund Grov <ggrov at inf.ed.ac.uk>
Stephan Merz <Stephan.Merz at loria.fr>
Year:        2011
Maintainer:  Gudmund Grov <ggrov at inf.ed.ac.uk>
*)

section "Liveness"

theory Liveness
imports Rules
begin

text‹This theory derives proof rules for liveness properties.›

definition enabled :: "'a formula ⇒ 'a formula"
where "enabled F ≡ λ s. ∃ t. ((first s) ## t) ⊨ F"

syntax "_Enabled" :: "lift ⇒ lift" ("(Enabled _)" [90] 90)

translations "_Enabled" ⇌ "CONST enabled"

definition WeakF :: "('a::world) formula ⇒ ('a,'b) stfun ⇒ 'a formula"
where "WeakF F v ≡ TEMP ◇□Enabled ⟨F⟩_v ⟶ □◇⟨F⟩_v"

definition StrongF :: "('a::world) formula ⇒ ('a,'b) stfun ⇒ 'a formula"
where "StrongF F v ≡ TEMP □◇Enabled ⟨F⟩_v ⟶ □◇⟨F⟩_v"

text‹
Lamport's TLA defines the above notions for actions.
In \tlastar{}, (pre-)formulas generalise TLA's actions and the above
definition is the natural generalisation of enabledness to pre-formulas.
In particular, we have chosen to define ‹enabled› such that it
yields itself a temporal formula, although its value really just depends
on the first state of the sequence it is evaluated over.
Then, the definitions of weak and strong fairness are exactly as in TLA.
›

syntax
"_WF" :: "[lift,lift] ⇒ lift" ("(WF'(_')'_(_))"  [20,1000] 90)
"_SF" :: "[lift,lift] ⇒ lift" ("(SF'(_')'_(_))"  [20,1000] 90)
"_WFsp" :: "[lift,lift] ⇒ lift" ("(WF '(_')'_(_))"  [20,1000] 90)
"_SFsp" :: "[lift,lift] ⇒ lift" ("(SF '(_')'_(_))"  [20,1000] 90)

translations
"_WF" ⇌ "CONST WeakF"
"_SF" ⇌ "CONST StrongF"
"_WFsp" ⇀ "CONST WeakF"
"_SFsp" ⇀ "CONST StrongF"

subsection "Properties of @{term enabled}"

theorem enabledI: "⊢ F ⟶ Enabled F"
proof (clarsimp)
fix w
assume "w ⊨ F"
with seq_app_first_tail[of w] have "((first w) ## tail w) ⊨ F" by simp
thus "w ⊨ Enabled F" by (auto simp: enabled_def)
qed

theorem enabledE:
assumes "s ⊨ Enabled F" and "⋀u. (first s ## u) ⊨ F ⟹ Q"
shows "Q"
using assms unfolding enabled_def by blast

lemma enabled_mono:
assumes "w ⊨ Enabled F" and "⊢ F ⟶ G"
shows "w ⊨ Enabled G"
using assms[unlifted] unfolding enabled_def by blast

lemma Enabled_disj1: "⊢ Enabled F ⟶ Enabled (F ∨ G)"
by (auto simp: enabled_def)

lemma  Enabled_disj2: "⊢ Enabled F ⟶ Enabled (G ∨ F)"
by (auto simp: enabled_def)

lemma  Enabled_conj1: "⊢ Enabled (F ∧ G) ⟶ Enabled F"
by (auto simp: enabled_def)

lemma  Enabled_conj2: "⊢ Enabled (G ∧ F) ⟶ Enabled F"
by (auto simp: enabled_def)

lemma Enabled_disjD: "⊢ Enabled (F ∨ G) ⟶ Enabled F ∨ Enabled G"
by (auto simp: enabled_def)

lemma Enabled_disj: "⊢ Enabled (F ∨ G) = (Enabled F ∨ Enabled G)"
by (auto simp: enabled_def)

lemmas enabled_disj_rew = Enabled_disj[int_rewrite]

lemma Enabled_ex: "⊢ Enabled (∃ x. F x) = (∃ x. Enabled (F x))"
by (force simp: enabled_def)

subsection "Fairness Properties"

lemma WF_alt: "⊢ WF(A)_v = (□◇¬Enabled ⟨A⟩_v ∨ □◇⟨A⟩_v)"
proof -
have "⊢ WF(A)_v = (¬◇□ Enabled ⟨A⟩_v ∨ □◇⟨A⟩_v)" by (auto simp: WeakF_def)
thus ?thesis by (simp add: dualization_rew)
qed

lemma SF_alt: "⊢ SF(A)_v = (◇□¬Enabled ⟨A⟩_v ∨ □◇⟨A⟩_v)"
proof -
have "⊢ SF(A)_v = (¬□◇ Enabled ⟨A⟩_v ∨ □◇⟨A⟩_v)" by (auto simp: StrongF_def)
thus ?thesis by (simp add: dualization_rew)
qed

lemma alwaysWFI: "⊢ WF(A)_v ⟶ □WF(A)_v"
unfolding WF_alt[int_rewrite] by (rule MM6)

theorem WF_always[simp_unl]: "⊢ □WF(A)_v = WF(A)_v"
by (rule int_iffI[OF ax1 alwaysWFI])

theorem WF_eventually[simp_unl]: "⊢ ◇WF(A)_v = WF(A)_v"
proof -
have 1: "⊢ ¬WF(A)_v = (◇□Enabled ⟨A⟩_v ∧ ¬ □◇⟨A⟩_v)"
by (auto simp: WeakF_def)
have "⊢ □¬WF(A)_v = ¬WF(A)_v"
by (simp add: 1[int_rewrite] STL5[int_rewrite] dualization_rew)
thus ?thesis
by (auto simp: eventually_def)
qed

lemma alwaysSFI: "⊢ SF(A)_v ⟶ □SF(A)_v"
proof -
have "⊢ □◇□¬Enabled ⟨A⟩_v ∨ □◇⟨A⟩_v ⟶ □(□◇□¬Enabled ⟨A⟩_v ∨ □◇⟨A⟩_v)"
by (rule MM6)
thus ?thesis unfolding SF_alt[int_rewrite] by simp
qed

theorem SF_always[simp_unl]: "⊢ □SF(A)_v = SF(A)_v"
by (rule int_iffI[OF ax1 alwaysSFI])

theorem SF_eventually[simp_unl]: "⊢ ◇SF(A)_v = SF(A)_v"
proof -
have 1: "⊢ ¬SF(A)_v = (□◇Enabled ⟨A⟩_v ∧ ¬ □◇⟨A⟩_v)"
by (auto simp: StrongF_def)
have "⊢ □¬SF(A)_v = ¬SF(A)_v"
by (simp add: 1[int_rewrite] STL5[int_rewrite] dualization_rew)
thus ?thesis
by (auto simp: eventually_def)
qed

theorem SF_imp_WF: "⊢ SF (A)_v ⟶ WF (A)_v"
unfolding WeakF_def StrongF_def by (auto dest: E20[unlift_rule])

lemma enabled_WFSF: "⊢ □Enabled ⟨F⟩_v ⟶ (WF(F)_v = SF(F)_v)"
proof -
have "⊢ □Enabled ⟨F⟩_v ⟶ ◇□Enabled ⟨F⟩_v" by (rule E3)
hence "⊢ □Enabled ⟨F⟩_v ⟶ WF(F)_v ⟶ SF(F)_v" by (auto simp: WeakF_def StrongF_def)
moreover
have "⊢ □Enabled ⟨F⟩_v ⟶ □◇Enabled ⟨F⟩_v" by (rule STL4[OF E3])
hence "⊢ □Enabled ⟨F⟩_v ⟶ SF(F)_v ⟶ WF(F)_v" by (auto simp: WeakF_def StrongF_def)
ultimately show ?thesis by force
qed

theorem WF1_general:
assumes h1: "|~ P ∧ N ⟶ ○P ∨ ○Q"
and h2: "|~ P ∧ N ∧ ⟨A⟩_v ⟶ ○Q"
and h3: "⊢ P ∧ N ⟶ Enabled ⟨A⟩_v"
and h4: "|~ P ∧ Unchanged w ⟶ ○P"
shows "⊢ □N ∧ WF(A)_v ⟶ (P ↝ Q)"
proof -
have "⊢ □(□N ∧ WF(A)_v) ⟶ □(□P ⟶ ◇⟨A⟩_v)"
proof (rule STL4)
have "⊢ □(P ∧ N) ⟶ ◇□Enabled ⟨A⟩_v" by (rule lift_imp_trans[OF h3[THEN STL4] E3])
hence "⊢ □P ∧ □N ∧ WF(A)_v ⟶ □◇⟨A⟩_v" by (auto simp: WeakF_def STL5[int_rewrite])
with ax1[of "TEMP ◇⟨A⟩_v"] show "⊢ □N ∧ WF(A)_v ⟶ □P ⟶ ◇⟨A⟩_v" by force
qed
hence "⊢ □N ∧ WF(A)_v ⟶ □(□P ⟶ ◇⟨A⟩_v)"
by (simp add: STL5[int_rewrite])
with AA22[OF h1 h2 h4] show ?thesis by force
qed

text ‹Lamport's version of the rule is derived as a special case.›

theorem WF1:
assumes h1: "|~ P ∧ [N]_v ⟶ ○P ∨ ○Q"
and h2: "|~ P ∧ ⟨N ∧ A⟩_v ⟶ ○Q"
and h3: "⊢ P ⟶ Enabled ⟨A⟩_v"
and h4: "|~ P ∧ Unchanged v ⟶ ○P"
shows "⊢ □[N]_v ∧ WF(A)_v ⟶ (P ↝ Q)"
proof -
have "⊢ □□[N]_v ∧ WF(A)_v ⟶ (P ↝ Q)"
proof (rule WF1_general)
from h1 T9[of N v] show "|~ P ∧ □[N]_v ⟶ ○P ∨ ○Q" by force
next
from T9[of N v] have "|~ P ∧ □[N]_v ∧ ⟨A⟩_v ⟶ P ∧ ⟨N ∧ A⟩_v"
by (auto simp: actrans_def angle_actrans_def)
from this h2 show "|~ P ∧ □[N]_v ∧ ⟨A⟩_v ⟶ ○Q" by (rule pref_imp_trans)
next
from h3 T9[of N v] show "⊢ P ∧ □[N]_v ⟶ Enabled ⟨A⟩_v" by force
qed (rule h4)
thus ?thesis by simp
qed

text ‹
The corresponding rule for strong fairness has an additional hypothesis
‹□F›, which is typically a conjunction of other fairness properties
used to prove that the helpful action eventually becomes enabled.
›

theorem SF1_general:
assumes h1: "|~ P ∧ N ⟶ ○P ∨ ○Q"
and h2: "|~ P ∧ N ∧ ⟨A⟩_v ⟶ ○Q"
and h3: "⊢ □P ∧ □N ∧ □F ⟶ ◇Enabled ⟨A⟩_v"
and h4: "|~ P ∧ Unchanged w ⟶ ○P"
shows "⊢ □N ∧ SF(A)_v ∧ □F ⟶ (P ↝ Q)"
proof -
have "⊢ □(□N ∧ SF(A)_v ∧ □F) ⟶ □(□P ⟶ ◇⟨A⟩_v)"
proof (rule STL4)
have "⊢ □(□P ∧ □N ∧ □F) ⟶ □◇Enabled ⟨A⟩_v" by (rule STL4[OF h3])
hence "⊢ □P ∧ □N ∧ □F ∧ SF(A)_v ⟶ □◇⟨A⟩_v" by (auto simp: StrongF_def STL5[int_rewrite])
with ax1[of "TEMP ◇⟨A⟩_v"] show "⊢ □N ∧ SF(A)_v ∧ □F ⟶ □P ⟶ ◇⟨A⟩_v" by force
qed
hence "⊢ □N ∧ SF(A)_v ∧ □F ⟶ □(□P ⟶ ◇⟨A⟩_v)"
by (simp add: STL5[int_rewrite])
with AA22[OF h1 h2 h4] show ?thesis by force
qed

theorem SF1:
assumes h1: "|~ P ∧ [N]_v ⟶ ○P ∨ ○Q"
and h2: "|~ P ∧ ⟨N ∧ A⟩_v ⟶ ○Q"
and h3: "⊢ □P ∧ □[N]_v ∧ □F ⟶ ◇Enabled ⟨A⟩_v"
and h4: "|~ P ∧ Unchanged v ⟶ ○P"
shows "⊢ □[N]_v ∧ SF(A)_v ∧ □F ⟶ (P ↝ Q)"
proof -
have "⊢ □□[N]_v ∧ SF(A)_v ∧ □F ⟶ (P ↝ Q)"
proof (rule SF1_general)
from h1 T9[of N v] show "|~ P ∧ □[N]_v ⟶ ○P ∨ ○Q" by force
next
from T9[of N v] have "|~ P ∧ □[N]_v ∧ ⟨A⟩_v ⟶ P ∧ ⟨N ∧ A⟩_v"
by (auto simp: actrans_def angle_actrans_def)
from this h2 show "|~ P ∧ □[N]_v ∧ ⟨A⟩_v ⟶ ○Q" by (rule pref_imp_trans)
next
from h3 show "⊢ □P ∧ □□[N]_v ∧ □F ⟶ ◇Enabled ⟨A⟩_v" by simp
qed (rule h4)
thus ?thesis by simp
qed

text ‹
Lamport proposes the following rule as an introduction rule for ‹WF› formulas.
›

theorem WF2:
assumes h1: "|~ ⟨N ∧ B⟩_f ⟶ ⟨M⟩_g"
and h2: "|~ P ∧ ○P ∧ ⟨N ∧ A⟩_f ⟶ B"
and h3: "⊢ P ∧ Enabled ⟨M⟩_g ⟶ Enabled ⟨A⟩_f"
and h4: "⊢ □[N ∧ ¬B]_f ∧ WF(A)_f ∧ □F ∧ ◇□Enabled ⟨M⟩_g ⟶ ◇□P"
shows "⊢ □[N]_f ∧ WF(A)_f ∧ □F ⟶ WF(M)_g"
proof -
have "⊢ □[N]_f ∧ WF(A)_f ∧ □F ∧ ◇□Enabled ⟨M⟩_g ∧ ¬□◇⟨M⟩_g ⟶ □◇⟨M⟩_g"
proof -
have 1: "⊢ □[N]_f ∧ WF(A)_f ∧ □F ∧ ◇□Enabled ⟨M⟩_g ∧ ¬□◇⟨M⟩_g ⟶ ◇□P"
proof -
have A: "⊢ □[N]_f ∧ WF(A)_f ∧ □F ∧ ◇□Enabled ⟨M⟩_g ∧ ¬□◇⟨M⟩_g ⟶
□(□[N]_f ∧ WF(A)_f ∧ □F) ∧ ◇□(◇□Enabled ⟨M⟩_g ∧ □[¬M]_g)"
unfolding STL6[int_rewrite] (* important to do this before STL5 is applied *)
by (auto simp: STL5[int_rewrite] dualization_rew)
have B: "⊢ □(□[N]_f ∧ WF(A)_f ∧ □F) ∧ ◇□(◇□Enabled ⟨M⟩_g ∧ □[¬M]_g) ⟶
◇((□[N]_f ∧ WF(A)_f ∧ □F) ∧ □(◇□Enabled ⟨M⟩_g ∧ □[¬M]_g))"
by (rule SE2)
from lift_imp_trans[OF A B]
have "⊢ □[N]_f ∧ WF(A)_f ∧ □F ∧ ◇□Enabled ⟨M⟩_g ∧ ¬□◇⟨M⟩_g ⟶
◇((□[N]_f ∧ WF(A)_f ∧ □F) ∧ (◇□Enabled ⟨M⟩_g ∧ □[¬M]_g))"
by (simp add: STL5[int_rewrite])
moreover
from h1 have "|~ [N]_f ⟶ [¬M]_g ⟶ [N ∧ ¬B]_f" by (auto simp: actrans_def angle_actrans_def)
hence "⊢ □[[N]_f]_f ⟶ □[[¬M]_g ⟶ [N ∧ ¬B]_f]_f" by (rule M2)
from lift_imp_trans[OF this ax4] have "⊢ □[N]_f ∧ □[¬M]_g ⟶ □[N ∧ ¬B]_f"
by (force intro: T4[unlift_rule])
with h4 have "⊢ (□[N]_f ∧ WF(A)_f ∧ □F) ∧ (◇□Enabled ⟨M⟩_g ∧ □[¬M]_g) ⟶ ◇□P"
by force
from STL4_eve[OF this]
have "⊢ ◇((□[N]_f ∧ WF(A)_f ∧ □F) ∧ (◇□Enabled ⟨M⟩_g ∧ □[¬M]_g)) ⟶ ◇□P" by simp
ultimately
show ?thesis by (rule lift_imp_trans)
qed
have 2: "⊢ □[N]_f ∧ WF(A)_f ∧ ◇□Enabled ⟨M⟩_g ∧ ◇□P ⟶ □◇⟨M⟩_g"
proof -
have A: "⊢ ◇□P ∧ ◇□Enabled ⟨M⟩_g ∧ WF(A)_f ⟶ □◇⟨A⟩_f"
using h3[THEN STL4, THEN STL4_eve] by (auto simp: STL6[int_rewrite] WeakF_def)
have B: "⊢ □[N]_f ∧ ◇□P ∧  □◇⟨A⟩_f ⟶ □◇⟨M⟩_g"
proof -
from M1[of P f] have "⊢ □P ∧ □◇⟨N ∧ A⟩_f ⟶ □◇⟨(P ∧ ○P) ∧ (N ∧ A)⟩_f"
by (force intro: AA29[unlift_rule])
hence "⊢ ◇□(□P ∧ □◇⟨N ∧ A⟩_f) ⟶ ◇□□◇⟨(P ∧ ○P) ∧ (N ∧ A)⟩_f"
by (rule STL4_eve[OF STL4])
hence "⊢ ◇□P ∧ □◇⟨N ∧ A⟩_f ⟶ □◇⟨(P ∧ ○P) ∧ (N ∧ A)⟩_f"
by (simp add: STL6[int_rewrite])
with AA29[of N f A]
have B1: "⊢ □[N]_f ∧ ◇□P ∧  □◇⟨A⟩_f ⟶ □◇⟨(P ∧ ○P) ∧ (N ∧ A)⟩_f" by force
from h2 have "|~ ⟨(P ∧ ○P) ∧ (N ∧ A)⟩_f ⟶ ⟨N ∧ B⟩_f"
by (auto simp: angle_actrans_sem[unlifted])
from B1 this[THEN AA25, THEN STL4] have "⊢ □[N]_f ∧ ◇□P ∧  □◇⟨A⟩_f ⟶ □◇⟨N ∧ B⟩_f"
by (rule lift_imp_trans)
moreover
have "⊢ □◇⟨N ∧ B⟩_f ⟶ □◇⟨M⟩_g" by (rule h1[THEN AA25, THEN STL4])
ultimately show ?thesis by (rule lift_imp_trans)
qed
from A B show ?thesis by force
qed
from 1 2 show ?thesis by force
qed
thus ?thesis by (auto simp: WeakF_def)
qed

text ‹
Lamport proposes an analogous theorem for introducing strong fairness, and its
proof is very similar, in fact, it was obtained by copy and paste, with minimal
modifications.
›

theorem SF2:
assumes h1: "|~ ⟨N ∧ B⟩_f ⟶ ⟨M⟩_g"
and h2: "|~ P ∧ ○P ∧ ⟨N ∧ A⟩_f ⟶ B"
and h3: "⊢ P ∧ Enabled ⟨M⟩_g ⟶ Enabled ⟨A⟩_f"
and h4: "⊢ □[N ∧ ¬B]_f ∧ SF(A)_f ∧ □F ∧ □◇Enabled ⟨M⟩_g ⟶ ◇□P"
shows "⊢ □[N]_f ∧ SF(A)_f ∧ □F ⟶ SF(M)_g"
proof -
have "⊢ □[N]_f ∧ SF(A)_f ∧ □F ∧ □◇Enabled ⟨M⟩_g ∧ ¬□◇⟨M⟩_g ⟶ □◇⟨M⟩_g"
proof -
have 1: "⊢ □[N]_f ∧ SF(A)_f ∧ □F ∧ □◇Enabled ⟨M⟩_g ∧ ¬□◇⟨M⟩_g ⟶ ◇□P"
proof -
have A: "⊢ □[N]_f ∧ SF(A)_f ∧ □F ∧ □◇Enabled ⟨M⟩_g ∧ ¬□◇⟨M⟩_g ⟶
□(□[N]_f ∧ SF(A)_f ∧ □F) ∧ ◇□(□◇Enabled ⟨M⟩_g ∧ □[¬M]_g)"
unfolding STL6[int_rewrite] (* important to do this before STL5 is applied *)
by (auto simp: STL5[int_rewrite] dualization_rew)
have B: "⊢ □(□[N]_f ∧ SF(A)_f ∧ □F) ∧ ◇□(□◇Enabled ⟨M⟩_g ∧ □[¬M]_g) ⟶
◇((□[N]_f ∧ SF(A)_f ∧ □F) ∧ □(□◇Enabled ⟨M⟩_g ∧ □[¬M]_g))"
by (rule SE2)
from lift_imp_trans[OF A B]
have "⊢ □[N]_f ∧ SF(A)_f ∧ □F ∧ □◇Enabled ⟨M⟩_g ∧ ¬□◇⟨M⟩_g ⟶
◇((□[N]_f ∧ SF(A)_f ∧ □F) ∧ (□◇Enabled ⟨M⟩_g ∧ □[¬M]_g))"
by (simp add: STL5[int_rewrite])
moreover
from h1 have "|~ [N]_f ⟶ [¬M]_g ⟶ [N ∧ ¬B]_f" by (auto simp: actrans_def angle_actrans_def)
hence "⊢ □[[N]_f]_f ⟶ □[[¬M]_g ⟶ [N ∧ ¬B]_f]_f" by (rule M2)
from lift_imp_trans[OF this ax4] have "⊢ □[N]_f ∧ □[¬M]_g ⟶ □[N ∧ ¬B]_f"
by (force intro: T4[unlift_rule])
with h4 have "⊢ (□[N]_f ∧ SF(A)_f ∧ □F) ∧ (□◇Enabled ⟨M⟩_g ∧ □[¬M]_g) ⟶ ◇□P"
by force
from STL4_eve[OF this]
have "⊢ ◇((□[N]_f ∧ SF(A)_f ∧ □F) ∧ (□◇Enabled ⟨M⟩_g ∧ □[¬M]_g)) ⟶ ◇□P" by simp
ultimately
show ?thesis by (rule lift_imp_trans)
qed
have 2: "⊢ □[N]_f ∧ SF(A)_f ∧ □◇Enabled ⟨M⟩_g ∧ ◇□P ⟶ □◇⟨M⟩_g"
proof -
have "⊢ □◇(P ∧ Enabled ⟨M⟩_g) ∧ SF(A)_f ⟶ □◇⟨A⟩_f"
using h3[THEN STL4_eve, THEN STL4] by (auto simp: StrongF_def)
with E28 have A: "⊢ ◇□P ∧ □◇Enabled ⟨M⟩_g ∧ SF(A)_f ⟶ □◇⟨A⟩_f"
by force
have B: "⊢ □[N]_f ∧ ◇□P ∧  □◇⟨A⟩_f ⟶ □◇⟨M⟩_g"
proof -
from M1[of P f] have "⊢ □P ∧ □◇⟨N ∧ A⟩_f ⟶ □◇⟨(P ∧ ○P) ∧ (N ∧ A)⟩_f"
by (force intro: AA29[unlift_rule])
hence "⊢ ◇□(□P ∧ □◇⟨N ∧ A⟩_f) ⟶ ◇□□◇⟨(P ∧ ○P) ∧ (N ∧ A)⟩_f"
by (rule STL4_eve[OF STL4])
hence "⊢ ◇□P ∧ □◇⟨N ∧ A⟩_f ⟶ □◇⟨(P ∧ ○P) ∧ (N ∧ A)⟩_f"
by (simp add: STL6[int_rewrite])
with AA29[of N f A]
have B1: "⊢ □[N]_f ∧ ◇□P ∧  □◇⟨A⟩_f ⟶ □◇⟨(P ∧ ○P) ∧ (N ∧ A)⟩_f" by force
from h2 have "|~ ⟨(P ∧ ○P) ∧ (N ∧ A)⟩_f ⟶ ⟨N ∧ B⟩_f"
by (auto simp: angle_actrans_sem[unlifted])
from B1 this[THEN AA25, THEN STL4] have "⊢ □[N]_f ∧ ◇□P ∧  □◇⟨A⟩_f ⟶ □◇⟨N ∧ B⟩_f"
by (rule lift_imp_trans)
moreover
have "⊢ □◇⟨N ∧ B⟩_f ⟶ □◇⟨M⟩_g" by (rule h1[THEN AA25, THEN STL4])
ultimately show ?thesis by (rule lift_imp_trans)
qed
from A B show ?thesis by force
qed
from 1 2 show ?thesis by force
qed
thus ?thesis by (auto simp: StrongF_def)
qed

text ‹This is the lattice rule from TLA›

assumes h1: "wf r"
and h2: "⋀x. ⊢ F x ↝ (G ∨ (∃y. #((y,x) ∈ r) ∧ F y))"
shows       "⊢ F x ↝ G"
using h1
proof (rule wf_induct)
fix x
assume ih: "∀y. (y, x) ∈ r ⟶ (⊢ F y ↝ G)"
show "⊢ F x ↝ G"
proof -
from ih have "⊢ (∃y. #((y,x) ∈ r) ∧ F y) ↝ G"
by (force simp: LT21[int_rewrite] LT33[int_rewrite])
with h2 show ?thesis by (force intro: LT19[unlift_rule])
qed
qed

subsection "Stuttering Invariance"

theorem stut_Enabled: "STUTINV Enabled ⟨F⟩_v"
by (auto simp: enabled_def stutinv_def dest!: sim_first)

theorem stut_WF: "NSTUTINV F ⟹ STUTINV WF(F)_v"
by (auto simp: WeakF_def stut_Enabled bothstutinvs)

theorem stut_SF: "NSTUTINV F ⟹ STUTINV SF(F)_v"
by (auto simp: StrongF_def stut_Enabled bothstutinvs)

lemmas livestutinv = stut_WF stut_SF stut_Enabled

end


# Theory State

(*  Title:       A Definitional Encoding of TLA in Isabelle/HOL
Authors:     Gudmund Grov <ggrov at inf.ed.ac.uk>
Stephan Merz <Stephan.Merz at loria.fr>
Year:        2011
Maintainer:  Gudmund Grov <ggrov at inf.ed.ac.uk>
*)

section ‹Representing state in TLA*›

theory State
imports Liveness
begin

text‹
We adopt the hidden state appraoch, as used in the existing
Isabelle/HOL TLA embedding \cite{Merz98}. This approach is also used
in \cite{Ehmety01}.
Here, a state space is defined by its projections, and everything else is
unknown. Thus, a variable is a projection of the state space, and has the same
type as a state function. Moreover, strong typing is achieved, since the projection
function may have any result type. To achieve this, the state space is represented
by an undefined type, which is an instance of the ‹world› class to enable
use with the ‹Intensional› theory.
›

typedecl state

instance state :: world ..

type_synonym 'a statefun = "(state,'a) stfun"
type_synonym statepred  = "bool statefun"
type_synonym 'a tempfun = "(state,'a) formfun"
type_synonym temporal = "state formula"

text ‹
Formalizing type state would require formulas to be tagged with
their underlying state space and would result in a system that is
much harder to use. (Unlike Hoare logic or Unity, TLA has quantification
over state variables, and therefore one usually works with different
state spaces within a single specification.) Instead, state is just
an anonymous type whose only purpose is to provide Skolem constants.
Moreover, we do not define a type of state variables separate from that
of arbitrary state functions, again in order to simplify the definition
of flexible quantification later on. Nevertheless, we need to distinguish
state variables, mainly to define the enabledness of actions. The user
identifies (tuples of) base'' state variables in a specification via the
meta predicate'' ‹basevars›, which is defined here.
›

definition stvars    :: "'a statefun ⇒ bool"
where basevars_def:  "stvars ≡ surj"

syntax
"PRED"    :: "lift ⇒ 'a"                          ("PRED _")
"_stvars" :: "lift ⇒ bool"                        ("basevars _")

translations
"PRED P"   ⇀  "(P::state => _)"
"_stvars"  ⇌  "CONST stvars"

text ‹
Base variables may be assigned arbitrary (type-correct) values.
In the following lemma, note that ‹vs› may be a tuple of variables.
The correct identification of base variables is up to the user who must
take care not to introduce an inconsistency. For example, @{term "basevars (x,x)"}
would definitely be inconsistent.
›

lemma basevars: "basevars vs ⟹ ∃u. vs u = c"
proof (unfold basevars_def surj_def)
assume "∀y. ∃x. y = vs x"
then obtain x where "c = vs x" by blast
thus "∃u. vs u = c" by blast
qed

lemma baseE:
assumes H1: "basevars v" and H2:"⋀x. v x = c ⟹ Q"
shows "Q"
using H1[THEN basevars] H2 by auto

text ‹A variant written for sequences rather than single states.›
lemma first_baseE:
assumes H1: "basevars v" and H2: "⋀x. v (first x) = c ⟹ Q"
shows "Q"
using H1[THEN basevars] H2 by (force simp: first_def)

lemma base_pair1:
assumes h: "basevars (x,y)"
shows "basevars x"
proof (auto simp: basevars_def)
fix c
from h[THEN basevars] obtain s where "(LIFT (x,y)) s = (c, arbitrary)" by auto
thus "c ∈ range x" by auto
qed

lemma base_pair2:
assumes h: "basevars (x,y)"
shows "basevars y"
proof (auto simp: basevars_def)
fix d
from h[THEN basevars] obtain s where "(LIFT (x,y)) s = (arbitrary, d)" by auto
thus "d ∈ range y" by auto
qed

lemma base_pair: "basevars (x,y) ⟹ basevars x ∧ basevars y"
by (auto elim: base_pair1 base_pair2)

text ‹
Since the @{typ unit} type has just one value, any state function of unit type
satisfies the predicate ‹basevars›. The following theorem can sometimes
be useful because it gives a trivial solution for ‹basevars› premises.
›

lemma unit_base: "basevars (v::state ⇒ unit)"
by (auto simp: basevars_def)

text ‹
A pair of the form ‹(x,x)› will generally not satisfy the predicate
‹basevars› -- except for pathological cases such as ‹x::unit›.
›
lemma
fixes x :: "state ⇒ bool"
assumes h1: "basevars (x,x)"
shows "False"
proof -
from h1 have "∃u. (LIFT (x,x)) u = (False,True)" by (rule basevars)
thus False by auto
qed

lemma
fixes x :: "state ⇒ nat"
assumes h1: "basevars (x,x)"
shows "False"
proof -
from h1 have "∃u. (LIFT (x,x)) u = (0,1)" by (rule basevars)
thus False by auto
qed

text ‹
The following theorem reduces the reasoning about the existence of a
state sequence satisfiyng an enabledness predicate to finding a suitable
value ‹c› at the successor state for the base variables of the
specification. This rule is intended for reasoning about standard TLA
specifications, where ‹Enabled› is applied to actions, not arbitrary
pre-formulas.
›
lemma base_enabled:
assumes h1: "basevars vs"
and h2: "⋀u. vs (first u) = c ⟹ ((first s) ## u) ⊨ F"
shows "s ⊨ Enabled F"
using h1 proof (rule first_baseE)
fix t
assume "vs (first t) = c"
hence "((first s) ## t) ⊨ F" by (rule h2)
thus "s ⊨ Enabled F" unfolding enabled_def by blast
qed

subsection "Temporal Quantifiers"

text‹
In \cite{Lamport94}, Lamport gives a stuttering invariant definition
of quantification over (flexible) variables. It relies on similarity
of two sequences (as supported in our @{theory TLA.Sequence} theory), and
equivalence of two sequences up to a variable (the bound variable).
However, sequence equaivalence up to a variable, requires state
equaivalence up to a variable. Our state representation above does not
support this, hence we cannot encode Lamport's definition in our theory.
Thus, we need to axiomatise quantification over (flexible) variables.
Note that with a state representation supporting this, our theory should
allow such an encoding.
›

consts
EEx        :: "('a statefun ⇒ temporal) ⇒ temporal"       (binder "Eex " 10)
AAll       :: "('a statefun ⇒ temporal) ⇒ temporal"       (binder "Aall " 10)

syntax
"_EEx"     :: "[idts, lift] => lift"                ("(3∃∃ _./ _)" [0,10] 10)
"_AAll"    :: "[idts, lift] => lift"                ("(3∀∀ _./ _)" [0,10] 10)
translations
"_EEx v A"  ==   "Eex v. A"
"_AAll v A" ==   "Aall v. A"

axiomatization where
eexI: "⊢ F x ⟶ (∃∃ x. F x)"
and  eexE: "⟦s ⊨ (∃∃ x. F x) ; basevars vs; (!! x. ⟦ basevars (x,vs); s ⊨ F x ⟧ ⟹ s ⊨ G)⟧
⟹ (s ⊨ G)"
and  all_def: "⊢ (∀∀ x. F x) = (¬(∃∃ x. ¬(F x)))"
and  eexSTUT: "STUTINV F x ⟹ STUTINV (∃∃ x. F x)"
and  history: "⊢ (I ∧ □[A]_v) = (∃∃ h. ($h = ha) ∧ I ∧ □[A ∧ h$=hb]_(h,v))"

lemmas eexI_unl = eexI[unlift_rule] ― ‹@{text "w ⊨ F x ⟹ w ⊨ (∃∃ x. F x)"}›

text ‹
‹tla_defs› can be used to unfold TLA definitions into lowest predicate level.
This is particularly useful for reasoning about enabledness of formulas.
›
lemmas tla_defs = unch_def before_def after_def first_def second_def suffix_def
tail_def nexts_def app_def angle_actrans_def actrans_def

end


# Theory Even

(*  Title:       A Definitional Encoding of TLA in Isabelle/HOL
Authors:     Gudmund Grov <ggrov at inf.ed.ac.uk>
Stephan Merz <Stephan.Merz at loria.fr>
Year:        2011
Maintainer:  Gudmund Grov <ggrov at inf.ed.ac.uk>
*)

section ‹A simple illustrative example›

theory Even
imports State
begin

text‹
A trivial example illustrating invariant proofs in the logic, and how
Isabelle/HOL can help with specification. It proves that ‹x› is
always even in a program where ‹x› is initialized as 0 and
always incremented by 2.
›

inductive_set
Even :: "nat set"
where
even_zero: "0 ∈ Even"
| even_step: "n ∈ Even ⟹ Suc (Suc n) ∈ Even"

locale Program =
fixes x :: "state ⇒ nat"
and init :: "temporal"
and act :: "temporal"
and phi :: "temporal"
defines "init ≡ TEMP $x = # 0" and "act ≡ TEMP x = Suc<Suc<$x>>"
and "phi ≡ TEMP init ∧ □[act]_x"

lemma (in Program) stutinvprog: "STUTINV phi"
by (auto simp: phi_def init_def act_def stutinvs nstutinvs)

lemma  (in Program) inveven: "⊢ phi ⟶ □($x ∈ # Even)" unfolding phi_def proof (rule invmono) show "⊢ init ⟶$x ∈ #Even"
by (auto simp: init_def even_zero)
next
show "|~ $x ∈ #Even ∧ [act]_x ⟶ ○($x ∈ #Even)"
by (auto simp: act_def even_step tla_defs)
qed

end


# Theory Inc

(*  Title:       A Definitional Encoding of TLA in Isabelle/HOL
Authors:     Gudmund Grov <ggrov at inf.ed.ac.uk>
Stephan Merz <Stephan.Merz at loria.fr>
Year:        2011
Maintainer:  Gudmund Grov <ggrov at inf.ed.ac.uk>
*)

section ‹Lamport's Inc example›

theory Inc
imports State
begin

text‹
This example illustrates use of the embedding by mechanising
the running example of Lamports original TLA paper \cite{Lamport94}.
›

datatype pcount = a | b | g

locale Firstprogram =
fixes x :: "state ⇒ nat"
and y :: "state ⇒ nat"
and init :: "temporal"
and m1  :: "temporal"
and m2 :: "temporal"
and phi :: "temporal"
and Live :: "temporal"
defines "init ≡ TEMP $x = # 0 ∧$y = # 0"
and "m1 ≡ TEMP x = Suc<$x> ∧ y =$y"
and "m2 ≡ TEMP y = Suc<$y> ∧ x =$x"
and "Live ≡ TEMP WF(m1)_(x,y) ∧ WF(m2)_(x,y)"
and "phi ≡ TEMP (init ∧ □[m1 ∨ m2]_(x,y) ∧ Live)"
assumes bvar: "basevars (x,y)"

lemma (in Firstprogram) "STUTINV phi"
by (auto simp: phi_def init_def m1_def m2_def Live_def stutinvs nstutinvs livestutinv)

lemma (in Firstprogram) enabled_m1: "⊢ Enabled ⟨m1⟩_(x,y)"
proof (clarify)
fix s
show "s ⊨ Enabled ⟨m1⟩_(x,y)"
by (rule base_enabled[OF bvar]) (auto simp: m1_def tla_defs)
qed

lemma (in Firstprogram) enabled_m2: "⊢ Enabled ⟨m2⟩_(x,y)"
proof (clarify)
fix s
show "s ⊨ Enabled ⟨m2⟩_(x,y)"
by (rule base_enabled[OF bvar]) (auto simp: m2_def tla_defs)
qed

locale Secondprogram = Firstprogram +
fixes sem :: "state ⇒ nat"
and pc1 :: "state ⇒ pcount"
and pc2 :: "state ⇒ pcount"
and vars
and initPsi :: "temporal"
and alpha1 :: "temporal"
and alpha2 :: "temporal"
and beta1 :: "temporal"
and beta2 :: "temporal"
and gamma1 :: "temporal"
and gamma2 :: "temporal"
and n1 :: "temporal"
and n2 :: "temporal"
and Live2 :: "temporal"
and psi :: "temporal"
and I :: "temporal"
defines "vars ≡ LIFT (x,y,sem,pc1,pc2)"
and "initPsi ≡ TEMP $pc1 = # a ∧$pc2 = # a ∧ $x = # 0 ∧$y = # 0 ∧ $sem = # 1" and "alpha1 ≡ TEMP$pc1 =#a ∧ # 0 < $sem ∧ pc1$ = #b ∧ sem$=$sem - # 1 ∧ Unchanged (x,y,pc2)"
and "alpha2 ≡ TEMP $pc2 =#a ∧ # 0 <$sem ∧ pc2 = #b ∧ sem$=$sem - # 1 ∧ Unchanged (x,y,pc1)"
and "beta1 ≡ TEMP $pc1 =#b ∧ pc1 = #g ∧ x = Suc<$x> ∧ Unchanged (`