# Theory Rewriting

theory Rewriting
imports LTL Extended_Nat
(*
Author:   Salomon Sickert
Author:   Benedikt Seidl
Author:   Alexander Schimpf (original entry: CAVA/LTL_Rewrite.thy)
*)

section ‹Rewrite Rules for LTL Simplification›

theory Rewriting
imports
LTL "HOL-Library.Extended_Nat"
begin

text ‹This theory provides rewrite rules for the simplification of LTL formulas. It supports:
\begin{itemize}
\item Constants Removal
\item @{const Next_ltln}-Normalisation
\item Modal Simplification (based on pure eventual, pure universal, or suspendable formulas)
\item Syntactic Implication Checking
\end{itemize}
It reuses parts of LTL\_Rewrite.thy (CAVA, LTL\_TO\_GBA). Furthermore, some rules were taken from
\cite{DBLP:conf/cav/SomenziB00} and \cite{DBLP:conf/tacas/BabiakKRS12}. All functions are defined for @{type ltln}.›

subsection ‹Constant Eliminating Constructors›

definition mk_and
where
"mk_and x y ≡ case x of false⇩n ⇒ false⇩n | true⇩n ⇒ y | _ ⇒ (case y of false⇩n ⇒ false⇩n | true⇩n ⇒ x | _ ⇒ x and⇩n y)"

definition mk_or
where
"mk_or x y ≡ case x of false⇩n ⇒ y | true⇩n ⇒ true⇩n | _ ⇒ (case y of true⇩n ⇒ true⇩n | false⇩n ⇒ x | _ ⇒ x or⇩n y)"

fun remove_strong_ops
where
"remove_strong_ops (x U⇩n y) = remove_strong_ops y"
| "remove_strong_ops (x M⇩n y) = x and⇩n y"
| "remove_strong_ops (x or⇩n y) = remove_strong_ops x or⇩n remove_strong_ops y"
| "remove_strong_ops x = x"

fun remove_weak_ops
where
"remove_weak_ops (x R⇩n y) = remove_weak_ops y"
| "remove_weak_ops (x W⇩n y) = x or⇩n y"
| "remove_weak_ops (x and⇩n y) = remove_weak_ops x and⇩n remove_weak_ops y"
| "remove_weak_ops x = x"

definition mk_finally
where
"mk_finally x ≡ case x of true⇩n ⇒ true⇩n | false⇩n ⇒ false⇩n | _ ⇒ F⇩n (remove_strong_ops x)"

definition mk_globally
where
"mk_globally x ≡ case x of true⇩n ⇒ true⇩n | false⇩n ⇒ false⇩n | _ ⇒ G⇩n (remove_weak_ops x)"

definition mk_until
where
"mk_until x y ≡ case x of false⇩n ⇒ y
| true⇩n ⇒ mk_finally y
| _ ⇒ (case y of true⇩n ⇒ true⇩n | false⇩n ⇒ false⇩n | _ ⇒ x U⇩n y)"

definition mk_release
where
"mk_release x y ≡ case x of true⇩n ⇒ y
| false⇩n ⇒ mk_globally y
| _ ⇒ (case y of true⇩n ⇒ true⇩n | false⇩n ⇒ false⇩n | _ ⇒ x R⇩n y)"

definition mk_weak_until
where
"mk_weak_until x y ≡ case y of true⇩n ⇒ true⇩n
| false⇩n ⇒ mk_globally x
| _ ⇒ (case x of true⇩n ⇒ true⇩n | false⇩n ⇒ y | _ ⇒ x W⇩n y)"

definition mk_strong_release
where
"mk_strong_release x y ≡ case y of false⇩n ⇒ false⇩n
| true⇩n ⇒ mk_finally x
| _ ⇒ (case x of true⇩n ⇒ y | false⇩n ⇒ false⇩n | _ ⇒ x M⇩n y)"

definition mk_next
where
"mk_next x ≡ case x of true⇩n ⇒ true⇩n | false⇩n ⇒ false⇩n | _ ⇒ X⇩n x"

definition mk_next_pow ("X⇩n''")
where
"mk_next_pow n x ≡ case x of true⇩n ⇒ true⇩n | false⇩n ⇒ false⇩n | _ ⇒ (Next_ltln ^^ n) x"

lemma mk_and_semantics [simp]:
"w ⊨⇩n mk_and x y ⟷ w ⊨⇩n x and⇩n y"
unfolding mk_and_def by (cases x; cases y; simp)

lemma mk_or_semantics [simp]:
"w ⊨⇩n mk_or x y ⟷ w ⊨⇩n x or⇩n y"
unfolding mk_or_def by (cases x; cases y; simp)

lemma remove_strong_ops_sound [simp]:
"w ⊨⇩n F⇩n (remove_strong_ops y) ⟷ w ⊨⇩n F⇩n y"
by (induction y arbitrary: w) (auto; force)+

lemma remove_weak_ops_sound [simp]:
"w ⊨⇩n G⇩n (remove_weak_ops y) ⟷ w ⊨⇩n G⇩n y"
by (induction y arbitrary: w) (auto; force)+

lemma mk_finally_semantics [simp]:
"w ⊨⇩n mk_finally x ⟷ w ⊨⇩n F⇩n x"
by (simp add: mk_finally_def del: semantics_ltln.simps(8,9) remove_strong_ops.simps split: ltln.splits)

lemma mk_globally_semantics [simp]:
"w ⊨⇩n mk_globally x ⟷ w ⊨⇩n G⇩n x"
by (simp add: mk_globally_def del: semantics_ltln.simps(8,9) remove_weak_ops.simps split: ltln.splits)

lemma mk_until_semantics [simp]:
"w ⊨⇩n mk_until x y ⟷ w ⊨⇩n x U⇩n y"
proof (cases x)
case (True_ltln)
show ?thesis
unfolding True_ltln mk_until_def
by (cases y) auto
next
case (False_ltln)
thus ?thesis
by (force simp: mk_until_def)
qed (cases y; force simp: mk_until_def)+

lemma mk_release_semantics [simp]:
"w ⊨⇩n mk_release x y ⟷ w ⊨⇩n x R⇩n y"
proof (cases x)
case (False_ltln)
thus ?thesis
unfolding False_ltln mk_release_def
by (cases y) auto
next
case (True_ltln)
thus ?thesis
by (force simp: mk_release_def)
qed (cases y; force simp: mk_release_def)+

lemma mk_weak_until_semantics [simp]:
"w ⊨⇩n mk_weak_until x y ⟷ w ⊨⇩n x W⇩n y"
proof (cases y)
case (False_ltln)
thus ?thesis
unfolding False_ltln mk_weak_until_def
by (cases x) auto
next
case (True_ltln)
thus ?thesis
by (force simp: mk_weak_until_def)
qed (cases x; force simp: mk_weak_until_def)+

lemma mk_strong_release_semantics [simp]:
"w ⊨⇩n mk_strong_release x y ⟷ w ⊨⇩n x M⇩n y"
proof (cases y)
case (True_ltln)
show ?thesis
unfolding True_ltln mk_strong_release_def
by (cases x) auto
next
case (False_ltln)
thus ?thesis
by (force simp: mk_strong_release_def)
qed (cases x; force simp: mk_strong_release_def)+

lemma mk_next_semantics [simp]:
"w ⊨⇩n mk_next x ⟷ w ⊨⇩n X⇩n x"
unfolding mk_next_def by (cases x; auto)

lemma mk_next_pow_semantics [simp]:
"w ⊨⇩n mk_next_pow i x ⟷ suffix i w ⊨⇩n x"
by (induction i arbitrary: w; cases x)
(auto simp: mk_next_pow_def)

lemma mk_next_pow_simp [simp, code_unfold]:
"mk_next_pow 0 x = x"
"mk_next_pow 1 x = mk_next x"
by (cases x; simp add: mk_next_pow_def mk_next_def)+

subsection ‹Constant Propagation›

fun is_constant :: "'a ltln ⇒ bool"
where
"is_constant true⇩n = True"
| "is_constant false⇩n = True"
| "is_constant _ = False"

lemma is_constant_constructorsI:
"is_constant x ⟹ is_constant y ⟹ is_constant (mk_and x y)"
"¬is_constant x ⟹ ¬is_constant y ⟹ ¬is_constant (mk_and x y)"
"is_constant x ⟹ is_constant y ⟹ is_constant (mk_or x y)"
"¬is_constant x ⟹ ¬is_constant y ⟹ ¬is_constant (mk_or x y)"
"is_constant x ⟹  is_constant (mk_finally x)"
"¬is_constant x ⟹  ¬is_constant (mk_finally x)"
"is_constant x ⟹ is_constant (mk_globally x)"
"¬is_constant x ⟹  ¬is_constant (mk_globally x)"
"is_constant x ⟹ is_constant (mk_until y x)"
"¬is_constant x ⟹ ¬is_constant (mk_until y x)"
"is_constant x ⟹ is_constant (mk_release y x)"
"¬is_constant x ⟹ ¬is_constant (mk_release y x)"
"is_constant x ⟹ is_constant y ⟹ is_constant (mk_weak_until x y)"
"¬is_constant x ⟹ ¬is_constant y ⟹ ¬is_constant (mk_weak_until x y)"
"is_constant x ⟹ is_constant y ⟹ is_constant (mk_strong_release x y)"
"¬is_constant x ⟹ ¬is_constant y ⟹ ¬is_constant (mk_strong_release x y)"
"is_constant x ⟹ is_constant (mk_next x)"
"¬is_constant x ⟹ ¬is_constant (mk_next x)"
"is_constant x ⟹ is_constant (mk_next_pow n x)"
by (cases x; cases y; simp add: mk_and_def mk_or_def mk_finally_def mk_globally_def mk_until_def mk_release_def mk_weak_until_def mk_strong_release_def mk_next_def mk_next_pow_def)+

lemma is_constant_constructors_simps:
"mk_next_pow n x = false⇩n ⟷ x = false⇩n"
"mk_next_pow n x = true⇩n ⟷ x = true⇩n"
"is_constant (mk_next_pow n x) ⟷ is_constant x"
by (induction n) (cases x; simp add: mk_next_pow_def)+

lemma is_constant_constructors_simps2:
"is_constant (mk_and x y) ⟷ (x = true⇩n ∧ y = true⇩n ∨ x = false⇩n ∨ y = false⇩n)"
"is_constant (mk_or x y) ⟷ (x = false⇩n ∧ y = false⇩n ∨ x = true⇩n ∨ y = true⇩n)"
"is_constant (mk_finally x) ⟷ is_constant x"
"is_constant (mk_globally x) ⟷ is_constant x"
"is_constant (mk_until y x) ⟷ is_constant x"
"is_constant (mk_release y x) ⟷ is_constant x"
"is_constant (mk_next x) ⟷ is_constant x"
by ((cases x; cases y; simp add: mk_and_def),
(cases x; cases y; simp add: mk_or_def),
(meson is_constant_constructorsI)+)

lemma is_constant_constructors_simps3:
"is_constant (mk_weak_until x y) ⟷ (x = false⇩n ∧ y = false⇩n ∨ x = true⇩n ∨ y = true⇩n)"
"is_constant (mk_strong_release x y) ⟷ (x = true⇩n ∧ y = true⇩n ∨ x = false⇩n ∨ y = false⇩n)"
by (cases x; cases y; simp add: mk_weak_until_def mk_strong_release_def is_constant_constructors_simps2)+

lemma is_constant_semantics:
"is_constant φ ⟹ ((∀w. w ⊨⇩n φ) ∨ ¬(∃w. w ⊨⇩n φ))"
by (cases φ) auto

lemma until_constant_simp:
"is_constant ψ ⟹ w ⊨⇩n φ U⇩n ψ ⟷ w ⊨⇩n ψ"
by (cases ψ) auto

lemma release_constant_simp:
"is_constant ψ ⟹ w ⊨⇩n φ R⇩n ψ ⟷ w ⊨⇩n ψ"
by (cases ψ) auto

lemma mk_next_pow_dist:
"mk_next_pow (i + j) φ = mk_next_pow i (mk_next_pow j φ)"
by (cases j; simp) (cases φ; simp add: mk_next_pow_def funpow_add; simp add: funpow_swap1)

lemma mk_next_pow_until:
"suffix (min i j) w ⊨⇩n (mk_next_pow (i - j) φ) U⇩n (mk_next_pow (j - i) ψ) ⟷ w ⊨⇩n (mk_next_pow i φ) U⇩n (mk_next_pow j ψ)"

lemma mk_next_pow_release:
"suffix (min i j) w ⊨⇩n (mk_next_pow (i - j) φ) R⇩n (mk_next_pow (j - i) ψ) ⟷ w ⊨⇩n (mk_next_pow i φ) R⇩n (mk_next_pow j ψ)"

subsection ‹X-Normalisation›

text ‹The following rewrite functions pulls the X-operator up in the syntax tree. This preprocessing
step enables the removal of X-operators in front of suspendable formulas. Furthermore constants are
removed as far as possible.›

fun the_enat_0 :: "enat ⇒ nat"
where
"the_enat_0 i = i"
| "the_enat_0 ∞ = 0"

lemma the_enat_0_simp [simp]:
"the_enat_0 0 = 0"
"the_enat_0 1 = 1"
by (simp add: zero_enat_def one_enat_def)+

fun combine :: "('a ltln ⇒ 'a ltln ⇒ 'a ltln) ⇒ ('a ltln * enat) ⇒ ('a ltln * enat) ⇒ ('a ltln * enat)"
where
"combine binop (φ, i) (ψ, j) = (
let
χ = binop (mk_next_pow (the_enat_0 (i - j)) φ) (mk_next_pow (the_enat_0 (j - i)) ψ)
in
(χ, if is_constant χ then ∞ else min i j))"

lemma fst_combine:
"fst (combine binop (φ, i) (ψ, j)) = binop (mk_next_pow (the_enat_0 (i - j)) φ) (mk_next_pow (the_enat_0 (j - i)) ψ)"
unfolding combine.simps by (meson fstI)

abbreviation to_ltln :: "('a ltln * enat) ⇒ 'a ltln"
where
"to_ltln x ≡ mk_next_pow (the_enat_0 (snd x)) (fst x)"

fun rewrite_X_enat :: "'a ltln ⇒ ('a ltln * enat)"
where
"rewrite_X_enat true⇩n = (true⇩n, ∞)"
| "rewrite_X_enat false⇩n = (false⇩n, ∞)"
| "rewrite_X_enat prop⇩n(a) = (prop⇩n(a), 0)"
| "rewrite_X_enat nprop⇩n(a) = (nprop⇩n(a), 0)"
| "rewrite_X_enat (φ and⇩n ψ) = combine mk_and (rewrite_X_enat φ) (rewrite_X_enat ψ)"
| "rewrite_X_enat (φ or⇩n ψ) = combine mk_or (rewrite_X_enat φ) (rewrite_X_enat ψ)"
| "rewrite_X_enat (φ U⇩n ψ) = combine mk_until (rewrite_X_enat φ) (rewrite_X_enat ψ)"
| "rewrite_X_enat (φ R⇩n ψ) = combine mk_release (rewrite_X_enat φ) (rewrite_X_enat ψ)"
| "rewrite_X_enat (φ W⇩n ψ) = combine mk_weak_until (rewrite_X_enat φ) (rewrite_X_enat ψ)"
| "rewrite_X_enat (φ M⇩n ψ) = combine mk_strong_release (rewrite_X_enat φ) (rewrite_X_enat ψ)"
| "rewrite_X_enat (X⇩n φ) = (λ(φ, n). (φ, eSuc n)) (rewrite_X_enat φ)"

definition
"rewrite_X φ = to_ltln (rewrite_X_enat φ)"

lemma combine_infinity_invariant:
assumes "i = ∞ ⟷ is_constant x"
assumes "j = ∞ ⟷ is_constant y"
shows "combine mk_and (x, i) (y, j) = (z, k) ⟹ (k = ∞ ⟷ is_constant z)"
and "combine mk_or (x, i) (y, j) = (z, k) ⟹ (k = ∞ ⟷ is_constant z)"
and "combine mk_until (x, i) (y, j) = (z, k) ⟹ (k = ∞ ⟷ is_constant z)"
and "combine mk_release (x, i) (y, j) = (z, k) ⟹ (k = ∞ ⟷ is_constant z)"
and "combine mk_weak_until (x, i) (y, j) = (z, k) ⟹ (k = ∞ ⟷ is_constant z)"
and "combine mk_strong_release (x, i) (y, j) = (z, k) ⟹ (k = ∞ ⟷ is_constant z)"
by (cases i; cases j; simp add: assms Let_def; force intro: is_constant_constructorsI)+

lemma combine_and_or_semantics:
assumes "i = ∞ ⟷ is_constant φ"
assumes "j = ∞ ⟷ is_constant ψ"
shows "w ⊨⇩n to_ltln (combine mk_and (φ, i) (ψ, j)) ⟷ w ⊨⇩n to_ltln (φ, i) and⇩n to_ltln (ψ, j)"
and "w ⊨⇩n to_ltln (combine mk_or (φ, i) (ψ, j)) ⟷ w ⊨⇩n to_ltln (φ, i) or⇩n to_ltln (ψ, j)"
by ((cases i; cases j; simp add: min_def is_constant_constructors_simps is_constant_constructors_simps2 assms),
(cases ψ; insert assms; auto),
(cases φ; insert assms; auto),
(blast elim!: is_constant.elims))+

lemma combine_until_release_semantics:
assumes "i = ∞ ⟷ is_constant φ"
assumes "j = ∞ ⟷ is_constant ψ"
shows "w ⊨⇩n to_ltln (combine mk_until (φ, i) (ψ, j)) ⟷ w ⊨⇩n to_ltln (φ, i) U⇩n to_ltln (ψ, j)"
and "w ⊨⇩n to_ltln (combine mk_release (φ, i) (ψ, j)) ⟷ w ⊨⇩n to_ltln (φ, i) R⇩n to_ltln (ψ, j)"
by ((cases i; cases j; simp add: is_constant_constructors_simps is_constant_constructors_simps2
until_constant_simp release_constant_simp mk_next_pow_until mk_next_pow_release del: semantics_ltln.simps),
(blast dest: is_constant_semantics),
(cases ψ; simp add: assms),
(cases φ; insert assms; auto simp: add.commute))+

(* TODO this proof is a bit slow and could be optimized *)
lemma combine_weak_until_strong_release_semantics:
assumes "i = ∞ ⟷ is_constant φ"
assumes "j = ∞ ⟷ is_constant ψ"
shows "w ⊨⇩n to_ltln (combine mk_weak_until (φ, i) (ψ, j)) ⟷ w ⊨⇩n to_ltln (φ, i) W⇩n to_ltln (ψ, j)"
and "w ⊨⇩n to_ltln (combine mk_strong_release (φ, i) (ψ, j)) ⟷ w ⊨⇩n to_ltln (φ, i) M⇩n to_ltln (ψ, j)"
by ((cases i; cases j; simp add: min_def is_constant_constructors_simps is_constant_constructors_simps3 del: semantics_ltln.simps),
(cases φ; simp add: assms),
(cases ψ; insert assms; auto simp: add.commute))+

lemma rewrite_X_enat_infinity_invariant:
"snd (rewrite_X_enat φ) = ∞ ⟷ is_constant (fst (rewrite_X_enat φ))"
proof (induction φ)
case (And_ltln φ ψ)
thus ?case
by (simp add: combine_infinity_invariant[OF And_ltln(1,2), unfolded prod.collapse])
next
case (Or_ltln φ ψ)
thus ?case
by (simp add: combine_infinity_invariant[OF Or_ltln(1,2), unfolded prod.collapse])
next
case (Until_ltln φ ψ)
thus ?case
by (simp add: combine_infinity_invariant[OF Until_ltln(1,2), unfolded prod.collapse])
next
case (Release_ltln φ ψ)
thus ?case
by (simp add: combine_infinity_invariant[OF Release_ltln(1,2), unfolded prod.collapse])
next
case (WeakUntil_ltln φ ψ)
thus ?case
by (simp add: combine_infinity_invariant[OF WeakUntil_ltln(1,2), unfolded prod.collapse])
next
case (StrongRelease_ltln φ ψ)
thus ?case
by (simp add: combine_infinity_invariant[OF StrongRelease_ltln(1,2), unfolded prod.collapse])
next
case (Next_ltln φ)
thus ?case
by (simp add: split_def) (metis eSuc_infinity eSuc_inject)
qed auto

lemma rewrite_X_enat_correct:
"w ⊨⇩n φ ⟷ w ⊨⇩n to_ltln (rewrite_X_enat φ)"
proof (induction φ arbitrary: w)
case (And_ltln φ ψ)
thus ?case
using combine_and_or_semantics[OF rewrite_X_enat_infinity_invariant rewrite_X_enat_infinity_invariant] by fastforce
next
case (Or_ltln φ ψ)
thus ?case
using combine_and_or_semantics[OF rewrite_X_enat_infinity_invariant rewrite_X_enat_infinity_invariant] by fastforce
next
case (Until_ltln φ ψ)
thus ?case
unfolding rewrite_X_enat.simps combine_until_release_semantics[OF rewrite_X_enat_infinity_invariant rewrite_X_enat_infinity_invariant, unfolded prod.collapse] by fastforce
next
case (Release_ltln φ ψ)
thus ?case
unfolding rewrite_X_enat.simps combine_until_release_semantics[OF rewrite_X_enat_infinity_invariant rewrite_X_enat_infinity_invariant, unfolded prod.collapse] by fastforce
next
case (WeakUntil_ltln φ ψ)
thus ?case
unfolding rewrite_X_enat.simps combine_weak_until_strong_release_semantics[OF rewrite_X_enat_infinity_invariant rewrite_X_enat_infinity_invariant, unfolded prod.collapse] by fastforce
next
case (StrongRelease_ltln φ ψ)
thus ?case
unfolding rewrite_X_enat.simps combine_weak_until_strong_release_semantics[OF rewrite_X_enat_infinity_invariant rewrite_X_enat_infinity_invariant, unfolded prod.collapse] by fastforce
next
case (Next_ltln φ)
moreover
have " w ⊨⇩n to_ltln (rewrite_X_enat (X⇩n φ)) ⟷ suffix 1 w ⊨⇩n to_ltln (rewrite_X_enat φ)"
by (simp add: split_def; cases "snd (rewrite_X_enat φ) ≠ ∞")
(auto simp: eSuc_def, auto simp: rewrite_X_enat_infinity_invariant eSuc_def dest: is_constant_semantics)
ultimately
show ?case
using semantics_ltln.simps(7) by blast
qed auto

lemma rewrite_X_sound [simp]:
"w ⊨⇩n rewrite_X φ ⟷ w ⊨⇩n φ"
using rewrite_X_enat_correct unfolding rewrite_X_def Let_def by auto

subsection ‹Pure Eventual, Pure Universal, and Suspendable Formulas›

fun pure_eventual :: "'a ltln ⇒ bool"
where
"pure_eventual true⇩n = True"
| "pure_eventual false⇩n = True"
| "pure_eventual (μ and⇩n μ') = (pure_eventual μ ∧ pure_eventual μ')"
| "pure_eventual (μ or⇩n μ') = (pure_eventual μ ∧ pure_eventual μ')"
| "pure_eventual (μ U⇩n μ') = (μ = true⇩n ∨ pure_eventual μ')"
| "pure_eventual (μ R⇩n μ') = (pure_eventual μ ∧ pure_eventual μ')"
| "pure_eventual (μ W⇩n μ') = (pure_eventual μ ∧ pure_eventual μ')"
| "pure_eventual (μ M⇩n μ') = (pure_eventual μ ∧ pure_eventual μ' ∨ μ' = true⇩n)"
| "pure_eventual (X⇩n μ) = pure_eventual μ"
| "pure_eventual _ = False"

fun pure_universal :: "'a ltln ⇒ bool"
where
"pure_universal true⇩n = True"
| "pure_universal false⇩n = True"
| "pure_universal (ν and⇩n ν') = (pure_universal ν ∧ pure_universal ν')"
| "pure_universal (ν or⇩n ν') = (pure_universal ν ∧ pure_universal ν')"
| "pure_universal (ν U⇩n ν') = (pure_universal ν ∧ pure_universal ν')"
| "pure_universal (ν R⇩n ν') = (ν = false⇩n ∨ pure_universal ν')"
| "pure_universal (ν W⇩n ν') = (pure_universal ν ∧ pure_universal ν' ∨ ν' = false⇩n)"
| "pure_universal (ν M⇩n ν') = (pure_universal ν ∧ pure_universal ν')"
| "pure_universal (X⇩n ν) = pure_universal ν"
| "pure_universal _ = False"

fun suspendable :: "'a ltln ⇒ bool"
where
"suspendable true⇩n = True"
| "suspendable false⇩n = True"
| "suspendable (ξ and⇩n ξ') = (suspendable ξ ∧ suspendable ξ')"
| "suspendable (ξ or⇩n ξ') = (suspendable ξ ∧ suspendable ξ')"
| "suspendable (φ U⇩n ξ) = (φ = true⇩n ∧ pure_universal ξ ∨ suspendable ξ)"
| "suspendable (φ R⇩n ξ) = (φ = false⇩n ∧ pure_eventual ξ ∨ suspendable ξ)"
| "suspendable (φ W⇩n ξ) = (suspendable φ ∧ suspendable ξ ∨ pure_eventual φ ∧ ξ = false⇩n)"
| "suspendable (φ M⇩n ξ) = (suspendable φ ∧ suspendable ξ ∨ pure_universal φ ∧ ξ = true⇩n)"
| "suspendable (X⇩n ξ) = suspendable ξ"
| "suspendable _ = False"

lemma pure_eventual_left_append:
"pure_eventual μ ⟹ w ⊨⇩n μ ⟹ (u ⌢ w) ⊨⇩n μ"
proof (induction μ arbitrary: u w)
case (Until_ltln μ μ')
moreover
then obtain i where "suffix i w ⊨⇩n μ'"
by auto
hence "μ = true⇩n ⟹ ?case"
by simp (metis suffix_conc_length suffix_suffix)
moreover
have "pure_eventual μ' ⟹ (u ⌢ w) ⊨⇩n μ'"
by (metis ‹suffix i w ⊨⇩n μ'› Until_ltln(2) prefix_suffix)
hence "pure_eventual μ' ⟹ ?case"
by force
ultimately
show ?case
by fastforce
next
case (Release_ltln μ μ')
thus ?case
by (cases "∀i. suffix i w ⊨⇩n μ'"; simp_all)
(metis linear suffix_conc_snd gr0I not_less0 prefix_suffix suffix_0)+
next
case (WeakUntil_ltln μ μ')
thus ?case
by (cases "∀i. suffix i w ⊨⇩n μ'"; simp_all)
(metis zero_le le0 nat_le_linear prefix_suffix suffix_0 suffix_conc_length suffix_conc_snd suffix_subseq_join)+
next
case (StrongRelease_ltln μ μ')
moreover
then obtain i where "suffix i w ⊨⇩n μ and⇩n μ'"
by auto
hence "μ' = true⇩n ⟹ ?case"
by simp (metis suffix_conc_length suffix_suffix)
moreover
have "pure_eventual μ ⟹ pure_eventual μ' ⟹ (u ⌢ w) ⊨⇩n μ and⇩n μ'"
by (metis ‹suffix i w ⊨⇩n μ and⇩n μ'› calculation(1) calculation(2) prefix_suffix semantics_ltln.simps(5))
hence "pure_eventual μ ⟹ pure_eventual μ' ⟹ ?case"
by force
ultimately
show ?case
by fastforce
qed (auto, metis diff_zero le_0_eq not_less_eq_eq suffix_conc_length suffix_conc_snd word_split)

lemma pure_universal_suffix_closed:
"pure_universal ν ⟹ (u ⌢ w) ⊨⇩n ν ⟹ w ⊨⇩n ν"
proof (induction ν arbitrary: u w)
case (Until_ltln ν ν')
hence "∃i. suffix i (u ⌢ w) ⊨⇩n ν' ∧ (∀j<i. suffix j (u ⌢ w) ⊨⇩n ν)"
using semantics_ltln.simps(8) by blast
thus ?case
by simp (metis Until_ltln(1-3) le_0_eq le_eq_less_or_eq le_less_linear prefix_suffix pure_universal.simps(5) suffix_conc_fst suffix_conc_snd)
next
case (Release_ltln ν ν')
moreover
hence "∀i. suffix i (u ⌢ w) ⊨⇩n ν' ∨ (∃j<i. suffix j (u ⌢ w) ⊨⇩n ν)"
by simp
ultimately
show ?case
by simp (metis semantics_ltln.simps(2) not_less0 prefix_suffix suffix_0 suffix_conc_length suffix_suffix)
next
case (WeakUntil_ltln ν ν')
moreover
hence "∀i. suffix i (u ⌢ w) ⊨⇩n ν ∨ (∃j≤i. suffix j (u ⌢ w) ⊨⇩n ν')"
by simp
ultimately
show ?case
by simp (metis (full_types) le_antisym prefix_suffix semantics_ltln.simps(2) suffix_0 suffix_conc_length suffix_suffix zero_le)
next
case (StrongRelease_ltln ν ν')
hence "∃i. suffix i (u ⌢ w) ⊨⇩n ν ∧ (∀j≤i. suffix j (u ⌢ w) ⊨⇩n ν')"
using semantics_ltln.simps(11) by blast
thus ?case
by simp (metis StrongRelease_ltln(1-3) diff_is_0_eq nat_le_linear prefix_conc_length prefix_suffix pure_universal.simps(8) subsequence_length suffix_conc_snd suffix_subseq_join)
next
case (Next_ltln μ)
thus ?case
by (metis prefix_suffix pure_universal.simps(9) semantics_ltln.simps(7) semiring_normalization_rules(24) suffix_conc_length suffix_suffix)
qed auto

lemma suspendable_prefix_invariant:
"suspendable ξ ⟹ (u ⌢ w) ⊨⇩n ξ ⟷ w ⊨⇩n ξ"
proof (induction ξ arbitrary: u w)
case (Until_ltln ξ ξ')
show ?case
proof (cases "suspendable ξ'")
case False
hence "ξ = true⇩n" and "pure_universal ξ'"
using Until_ltln by simp+
thus ?thesis
by (simp; metis (no_types) linear pure_universal_suffix_closed suffix_conc_fst suffix_conc_length suffix_conc_snd suffix_suffix)
qed (simp; metis Until_ltln(2) not_less0 prefix_suffix)
next
case (Release_ltln ξ ξ')
show ?case
proof (cases "suspendable ξ'")
case False
hence "ξ = false⇩n" and "pure_eventual ξ'"
using Release_ltln by simp+
thus ?thesis
by (simp; metis (no_types) le_iff_add add_diff_cancel_left' linear pure_eventual_left_append suffix_0 suffix_conc_fst suffix_conc_snd)
qed (simp; metis Release_ltln(2) not_less0 prefix_suffix)
next
case (WeakUntil_ltln ξ ξ')
show ?case
proof (cases "suspendable ξ ∧ suspendable ξ'")
case False
hence "ξ' = false⇩n" and "pure_eventual ξ"
using WeakUntil_ltln by simp+
thus ?thesis
by (simp; metis (no_types) le_iff_add add_diff_cancel_left' linear pure_eventual_left_append suffix_0 suffix_conc_fst suffix_conc_snd)
qed (simp; metis (full_types) WeakUntil_ltln.IH prefix_suffix)
next
case (StrongRelease_ltln ξ ξ')
show ?case
proof (cases "suspendable ξ ∧ suspendable ξ'")
case False
hence "ξ' = true⇩n" and "pure_universal ξ"
using StrongRelease_ltln by simp+
thus ?thesis
by (simp; metis (no_types) linear pure_universal_suffix_closed suffix_conc_fst suffix_conc_length suffix_conc_snd suffix_suffix)
qed (simp; metis (full_types) StrongRelease_ltln.IH(1) StrongRelease_ltln.IH(2) prefix_suffix)
qed (simp_all, metis prefix_suffix)

theorem pure_eventual_until_simp:
assumes "pure_eventual μ"
shows "w ⊨⇩n φ U⇩n μ ⟷ w ⊨⇩n μ"
proof -
have "⋀i. suffix i w ⊨⇩n μ ⟹ w ⊨⇩n μ"
using pure_eventual_left_append[OF assms] prefix_suffix by metis
thus ?thesis
by force
qed

theorem pure_universal_release_simp:
assumes "pure_universal ν"
shows "w ⊨⇩n φ R⇩n ν ⟷ w ⊨⇩n ν"
proof -
have "⋀i. w ⊨⇩n ν ⟹ suffix i w ⊨⇩n ν"
using pure_universal_suffix_closed[OF assms] prefix_suffix by metis
thus ?thesis
by force
qed

theorem pure_universal_weak_until_simp:
assumes "pure_universal φ" and "pure_universal ψ"
shows "w ⊨⇩n φ W⇩n ψ ⟷ w ⊨⇩n φ or⇩n ψ"
proof -
have "⋀i. w ⊨⇩n φ ⟹ suffix i w ⊨⇩n φ" and "⋀i. w ⊨⇩n ψ ⟹ suffix i w ⊨⇩n ψ"
using assms pure_universal_suffix_closed prefix_suffix by metis+
thus ?thesis
by force
qed

theorem pure_eventual_strong_release_simp:
assumes "pure_eventual φ" and "pure_eventual ψ"
shows "w ⊨⇩n φ M⇩n ψ ⟷ w ⊨⇩n φ and⇩n ψ"
proof -
have "⋀i. suffix i w ⊨⇩n φ ⟹ w ⊨⇩n φ" and "⋀i. suffix i w ⊨⇩n ψ ⟹ w ⊨⇩n ψ"
using assms pure_eventual_left_append prefix_suffix by metis+
thus ?thesis
by force
qed

theorem suspendable_formula_simp:
assumes "suspendable ξ"
shows "w ⊨⇩n X⇩n ξ ⟷ w ⊨⇩n ξ" (is ?t1)
and "w ⊨⇩n φ U⇩n ξ ⟷ w ⊨⇩n ξ" (is ?t2)
and "w ⊨⇩n φ R⇩n ξ ⟷ w ⊨⇩n ξ" (is ?t3)
proof -
have "⋀i. suffix i w ⊨⇩n ξ ⟷ w ⊨⇩n ξ"
using suspendable_prefix_invariant[OF assms] prefix_suffix by metis
thus ?t1 ?t2 ?t3
by force+
qed

theorem suspendable_formula_simp2:
assumes "suspendable φ" and "suspendable ψ"
shows "w ⊨⇩n φ W⇩n ψ ⟷ w ⊨⇩n φ or⇩n ψ" (is ?t1)
and "w ⊨⇩n φ M⇩n ψ ⟷ w ⊨⇩n φ and⇩n ψ" (is ?t2)
proof -
have "⋀i. suffix i w ⊨⇩n φ ⟷ w ⊨⇩n φ" and "⋀i. suffix i w ⊨⇩n ψ ⟷ w ⊨⇩n ψ"
using assms suspendable_prefix_invariant prefix_suffix by metis+
thus ?t1 ?t2
by force+
qed

fun rewrite_modal :: "'a ltln ⇒ 'a ltln"
where
"rewrite_modal true⇩n = true⇩n"
| "rewrite_modal false⇩n = false⇩n"
| "rewrite_modal (φ and⇩n ψ) = (rewrite_modal φ and⇩n rewrite_modal ψ)"
| "rewrite_modal (φ or⇩n ψ) = (rewrite_modal φ or⇩n rewrite_modal ψ)"
| "rewrite_modal (φ U⇩n ψ) = (if pure_eventual ψ ∨ suspendable ψ then rewrite_modal ψ else (rewrite_modal φ U⇩n rewrite_modal ψ))"
| "rewrite_modal (φ R⇩n ψ) = (if pure_universal ψ ∨ suspendable ψ then rewrite_modal ψ else (rewrite_modal φ R⇩n rewrite_modal ψ))"
| "rewrite_modal (φ W⇩n ψ) = (if pure_universal φ ∧ pure_universal ψ ∨ suspendable φ ∧ suspendable ψ then (rewrite_modal φ or⇩n rewrite_modal ψ) else (rewrite_modal φ W⇩n rewrite_modal ψ))"
| "rewrite_modal (φ M⇩n ψ) = (if pure_eventual φ ∧ pure_eventual ψ ∨ suspendable φ ∧ suspendable ψ then (rewrite_modal φ and⇩n rewrite_modal ψ) else (rewrite_modal φ M⇩n rewrite_modal ψ))"
| "rewrite_modal (X⇩n φ) = (if suspendable φ then rewrite_modal φ else X⇩n (rewrite_modal φ))"
| "rewrite_modal φ = φ"

lemma rewrite_modal_sound [simp]:
"w ⊨⇩n rewrite_modal φ ⟷ w ⊨⇩n φ"
proof (induction φ arbitrary: w)
case (Until_ltln φ ψ)
thus ?case
apply (cases "pure_eventual ψ ∨ suspendable ψ")
apply (insert pure_eventual_until_simp[of ψ] suspendable_formula_simp[of ψ])
apply fastforce+
done
next
case (Release_ltln φ ψ)
thus ?case
apply (cases "pure_universal ψ ∨ suspendable ψ")
apply (insert pure_universal_release_simp[of ψ] suspendable_formula_simp[of ψ])
apply fastforce+
done
next
case (WeakUntil_ltln φ ψ)
thus ?case
apply (cases "pure_universal φ ∧ pure_universal ψ ∨ suspendable φ ∧ suspendable ψ")
apply (insert pure_universal_weak_until_simp[of φ ψ] suspendable_formula_simp2[of φ ψ])
apply fastforce+
done
next
case (StrongRelease_ltln φ ψ)
thus ?case
apply (cases "pure_eventual φ ∧ pure_eventual ψ ∨ suspendable φ ∧ suspendable ψ")
apply (insert pure_eventual_strong_release_simp[of φ ψ] suspendable_formula_simp2[of φ ψ])
apply fastforce+
done
next
case (Next_ltln φ)
thus ?case
apply (cases "suspendable φ")
apply (insert suspendable_formula_simp[of φ])
apply fastforce+
done
qed auto

lemma rewrite_modal_size:
"size (rewrite_modal φ) ≤ size φ"
by (induction φ) auto

subsection ‹Syntactical Implication Based Simplification›

inductive syntactical_implies :: "'a ltln ⇒ 'a ltln ⇒ bool" ("_ ⊢⇩s _" [80, 80])
where
"_ ⊢⇩s true⇩n"
| "false⇩n ⊢⇩s _"
| "φ = φ ⟹ φ ⊢⇩s φ"

| "φ ⊢⇩s χ ⟹ (φ and⇩n ψ) ⊢⇩s χ"
| "ψ ⊢⇩s χ ⟹ (φ and⇩n ψ) ⊢⇩s χ"
| "φ ⊢⇩s ψ ⟹ φ ⊢⇩s χ ⟹ φ ⊢⇩s (ψ and⇩n χ)"

| "φ ⊢⇩s ψ ⟹ φ ⊢⇩s (ψ or⇩n χ)"
| "φ ⊢⇩s χ ⟹ φ ⊢⇩s (ψ or⇩n χ)"
| "φ ⊢⇩s χ ⟹ ψ ⊢⇩s χ ⟹ (φ or⇩n ψ) ⊢⇩s χ"

| "φ ⊢⇩s χ ⟹ φ ⊢⇩s (ψ U⇩n χ)"
| "φ ⊢⇩s χ ⟹ ψ ⊢⇩s χ ⟹ (φ U⇩n ψ) ⊢⇩s χ"
| "φ ⊢⇩s χ ⟹ ψ ⊢⇩s ν ⟹ (φ U⇩n ψ) ⊢⇩s (χ U⇩n ν)"

| "χ ⊢⇩s φ ⟹ (ψ R⇩n χ) ⊢⇩s φ"
| "χ ⊢⇩s φ ⟹ χ ⊢⇩s ψ ⟹ χ ⊢⇩s (φ R⇩n ψ)"
| "φ ⊢⇩s χ ⟹ ψ ⊢⇩s ν ⟹ (φ R⇩n ψ) ⊢⇩s (χ R⇩n ν)"

| "(false⇩n R⇩n φ) ⊢⇩s ψ ⟹ (false⇩n R⇩n φ) ⊢⇩s X⇩n ψ"
| "φ ⊢⇩s (true⇩n U⇩n ψ) ⟹ (X⇩n φ) ⊢⇩s (true⇩n U⇩n ψ)"
| "φ ⊢⇩s ψ ⟹ (X⇩n φ) ⊢⇩s (X⇩n ψ)"

lemma syntactical_implies_correct:
"φ ⊢⇩s ψ ⟹ w ⊨⇩n φ ⟹ w ⊨⇩n ψ"
by (induction arbitrary: w rule: syntactical_implies.induct; auto; force)

fun rewrite_syn_imp
where
"rewrite_syn_imp (φ and⇩n ψ) = (
if φ ⊢⇩s ψ then
rewrite_syn_imp φ
else if ψ ⊢⇩s φ then
rewrite_syn_imp ψ
else if φ ⊢⇩s (not⇩n ψ) ∨ ψ ⊢⇩s (not⇩n φ) then
false⇩n
else
mk_and (rewrite_syn_imp φ) (rewrite_syn_imp ψ))"
| "rewrite_syn_imp (φ or⇩n ψ) = (
if φ ⊢⇩s ψ then
rewrite_syn_imp ψ
else if ψ ⊢⇩s φ then
rewrite_syn_imp φ
else if (not⇩n φ) ⊢⇩s ψ ∨ (not⇩n ψ) ⊢⇩s φ then
true⇩n
else
mk_or (rewrite_syn_imp φ) (rewrite_syn_imp ψ))"
| "rewrite_syn_imp (φ U⇩n ψ) = (
if φ ⊢⇩s ψ then
rewrite_syn_imp ψ
else if (not⇩n φ) ⊢⇩s ψ then
mk_finally (rewrite_syn_imp ψ)
else
mk_until (rewrite_syn_imp φ) (rewrite_syn_imp ψ))"
| "rewrite_syn_imp (φ R⇩n ψ) = (
if ψ ⊢⇩s φ then
rewrite_syn_imp ψ
else if ψ ⊢⇩s (not⇩n φ) then
mk_globally (rewrite_syn_imp ψ)
else
mk_release (rewrite_syn_imp φ) (rewrite_syn_imp ψ))"
| "rewrite_syn_imp (X⇩n φ) = mk_next (rewrite_syn_imp φ)"
| "rewrite_syn_imp φ = φ"

lemma rewrite_syn_imp_sound:
"w ⊨⇩n rewrite_syn_imp φ ⟷ w ⊨⇩n φ"
proof (induction φ arbitrary: w)
case And_ltln
thus ?case
by (simp add: Let_def; metis syntactical_implies_correct not⇩n_semantics)
next
case (Or_ltln φ ψ)
moreover
have "(not⇩n φ) ⊢⇩s ψ ⟹ ∀w. w ⊨⇩n φ or⇩n ψ"
by (auto intro: syntactical_implies_correct[of "not⇩n φ"])
moreover
have "(not⇩n ψ) ⊢⇩s φ ⟹ ∀w. w ⊨⇩n φ or⇩n ψ"
by (auto intro: syntactical_implies_correct[of "not⇩n ψ"])
ultimately
show ?case
by (auto intro: syntactical_implies_correct)
next
case (Until_ltln φ ψ)
moreover
have "φ ⊢⇩s ψ ⟹ ?case"
by (force simp add: Until_ltln dest: syntactical_implies_correct)
moreover
{
assume A: "(not⇩n φ) ⊢⇩s ψ" and B: "¬ φ ⊢⇩s ψ"
hence [simp]: "rewrite_syn_imp (φ U⇩n ψ) = mk_finally (rewrite_syn_imp ψ)"
by simp
{
assume "∃i. suffix i w ⊨⇩n ψ"
moreover
define i where "i ≡ LEAST i. suffix i w ⊨⇩n ψ"
ultimately
have "∀j < i. ¬suffix j w ⊨⇩n ψ" and "suffix i w ⊨⇩n ψ"
by (blast dest: not_less_Least , metis LeastI ‹∃i. suffix i w ⊨⇩n ψ› i_def)
hence "∀j < i. suffix j w ⊨⇩n φ" and "suffix i w ⊨⇩n ψ"
using syntactical_implies_correct[OF A] by auto
}
hence ?case
by (simp del: rewrite_syn_imp.simps; unfold Until_ltln(2)) blast
}
ultimately
show ?case
by fastforce
next
case (Release_ltln φ ψ)
moreover
have "ψ ⊢⇩s φ ⟹ ?case"
by (force simp add: Release_ltln dest: syntactical_implies_correct)
moreover
{
assume A: "ψ ⊢⇩s (not⇩n φ)" and B: "¬ ψ ⊢⇩s φ"
hence [simp]: "rewrite_syn_imp (φ R⇩n ψ) = mk_globally (rewrite_syn_imp ψ)"
by simp
{
assume "∃i. ¬suffix i w ⊨⇩n ψ"
moreover
define i where "i ≡ LEAST i. ¬suffix i w ⊨⇩n ψ"
ultimately
have "∀j < i. suffix j w ⊨⇩n ψ" and "¬ suffix i w ⊨⇩n ψ"
by (blast dest: not_less_Least , metis LeastI ‹∃i. ¬suffix i w ⊨⇩n ψ› i_def)
hence "∀j < i. ¬suffix j w ⊨⇩n φ" and "¬ suffix i w ⊨⇩n ψ"
using syntactical_implies_correct[OF A] by auto
}
hence ?case
by (simp del: rewrite_syn_imp.simps; unfold Release_ltln(2)) blast
}
ultimately
show ?case
by fastforce
qed auto

subsection ‹Iterated Rewriting›

fun iterate
where
"iterate f x 0 = x"
| "iterate f x (Suc n) = (let x' = f x in if x = x' then x else iterate f x' n)"

definition
"rewrite_iter_fast φ ≡ iterate (rewrite_modal o rewrite_X) φ (size φ)"

definition
"rewrite_iter_slow φ ≡ iterate (rewrite_syn_imp o rewrite_modal o rewrite_X) φ (size φ)"

text ‹The rewriting functions defined in the previous subsections can be used as-is. However, in the
most cases one wants to iterate these rules until the formula cannot be simplified further.
@{const rewrite_iter_fast} pulls X operators up in the syntax tree and the uses the
"modal" simplification rules. @{const rewrite_iter_slow} additionally tries to simplify the
formula using syntactic implication checking.›

lemma iterate_sound:
assumes "⋀φ. w ⊨⇩n f φ ⟷ w ⊨⇩n φ"
shows "w ⊨⇩n iterate f φ n ⟷ w ⊨⇩n φ"
by (induction n arbitrary: φ; simp add: assms Let_def)

theorem rewrite_iter_fast_sound [simp]:
"w ⊨⇩n rewrite_iter_fast φ ⟷ w ⊨⇩n φ"
using iterate_sound[of _ "rewrite_modal o rewrite_X"]
unfolding comp_def rewrite_modal_sound rewrite_X_sound rewrite_iter_fast_def
by blast

theorem rewrite_iter_slow_sound [simp]:
"w ⊨⇩n rewrite_iter_slow φ ⟷ w ⊨⇩n φ"
using iterate_sound[of _ "rewrite_syn_imp o rewrite_modal o rewrite_X"]
unfolding comp_def rewrite_modal_sound rewrite_X_sound rewrite_syn_imp_sound rewrite_iter_slow_def
by blast

subsection ‹Preservation of atoms›

lemma iterate_atoms:
assumes
"⋀φ. atoms_ltln (f φ) ⊆ atoms_ltln φ"
shows
"atoms_ltln (iterate f φ n) ⊆ atoms_ltln φ"
by (induction n arbitrary: φ) (auto, metis (mono_tags, lifting) assms in_mono)

lemma rewrite_modal_atoms:
"atoms_ltln (rewrite_modal φ) ⊆ atoms_ltln φ"
by (induction φ) auto

lemma mk_and_atoms:
"atoms_ltln (mk_and φ ψ) ⊆ atoms_ltln φ ∪ atoms_ltln ψ"
by (auto simp: mk_and_def split: ltln.splits)

lemma mk_or_atoms:
"atoms_ltln (mk_or φ ψ) ⊆ atoms_ltln φ ∪ atoms_ltln ψ"
by (auto simp: mk_or_def split: ltln.splits)

lemma remove_strong_ops_atoms:
"atoms_ltln (remove_strong_ops φ) ⊆ atoms_ltln φ"
by (induction φ) auto

lemma remove_weak_ops_atoms:
"atoms_ltln (remove_weak_ops φ) ⊆ atoms_ltln φ"
by (induction φ) auto

lemma mk_finally_atoms:
"atoms_ltln (mk_finally φ) ⊆ atoms_ltln φ"
by (auto simp: mk_finally_def split: ltln.splits) (insert remove_strong_ops_atoms, fast+)

lemma mk_globally_atoms:
"atoms_ltln (mk_globally φ) ⊆ atoms_ltln φ"
by (auto simp: mk_globally_def split: ltln.splits) (insert remove_weak_ops_atoms, fast+)

lemma mk_until_atoms:
"atoms_ltln (mk_until φ ψ) ⊆ atoms_ltln φ ∪ atoms_ltln ψ"
by (auto simp: mk_until_def split: ltln.splits) (insert mk_finally_atoms, fastforce+)

lemma mk_release_atoms:
"atoms_ltln (mk_release φ ψ) ⊆ atoms_ltln φ ∪ atoms_ltln ψ"
by (auto simp: mk_release_def split: ltln.splits) (insert mk_globally_atoms, fastforce+)

lemma mk_weak_until_atoms:
"atoms_ltln (mk_weak_until φ ψ) ⊆ atoms_ltln φ ∪ atoms_ltln ψ"
by (auto simp: mk_weak_until_def split: ltln.splits) (insert mk_globally_atoms, fastforce+)

lemma mk_strong_release_atoms:
"atoms_ltln (mk_strong_release φ ψ) ⊆ atoms_ltln φ ∪ atoms_ltln ψ"
by (auto simp: mk_strong_release_def split: ltln.splits) (insert mk_finally_atoms, fastforce+)

lemma mk_next_atoms:
"atoms_ltln (mk_next φ) = atoms_ltln φ"
by (auto simp: mk_next_def split: ltln.splits)

lemma mk_next_pow_atoms:
"atoms_ltln (mk_next_pow n φ) = atoms_ltln φ"
by (induction n) (auto simp: mk_next_pow_def split: ltln.splits)

lemma combine_atoms:
assumes
"⋀φ ψ. atoms_ltln (f φ ψ) ⊆ atoms_ltln φ ∪ atoms_ltln ψ"
shows
"atoms_ltln (fst (combine f x y)) ⊆ atoms_ltln (fst x) ∪ atoms_ltln (fst y)"
by (metis assms fst_combine mk_next_pow_atoms prod.collapse)

lemmas combine_mk_atoms =
combine_atoms[OF mk_and_atoms]
combine_atoms[OF mk_or_atoms]
combine_atoms[OF mk_until_atoms]
combine_atoms[OF mk_release_atoms]
combine_atoms[OF mk_weak_until_atoms]
combine_atoms[OF mk_strong_release_atoms]

lemma rewrite_X_enat_atoms:
"atoms_ltln (fst (rewrite_X_enat φ)) ⊆ atoms_ltln φ"
by (induction φ) (simp_all add: case_prod_beta, insert combine_mk_atoms, fast+)

lemma rewrite_X_atoms:
"atoms_ltln (rewrite_X φ) ⊆ atoms_ltln φ"
by (induction φ) (simp_all add: rewrite_X_def mk_next_pow_atoms case_prod_beta, insert combine_mk_atoms, fast+)

lemma rewrite_syn_imp_atoms:
"atoms_ltln (rewrite_syn_imp φ) ⊆ atoms_ltln φ"
proof (induction φ)
case (And_ltln φ1 φ2)
then show ?case
using mk_and_atoms by simp fast
next
case (Or_ltln φ1 φ2)
then show ?case
using mk_or_atoms by simp fast
next
case (Next_ltln φ)
then show ?case
using mk_next_atoms by simp fast
next
case (Until_ltln φ1 φ2)
then show ?case
using mk_finally_atoms mk_until_atoms by simp fast
next
case (Release_ltln φ1 φ2)
then show ?case
using mk_globally_atoms mk_release_atoms by simp fast
qed simp_all

lemma rewrite_iter_fast_atoms:
"atoms_ltln (rewrite_iter_fast φ) ⊆ atoms_ltln φ"
proof -
have 1: "⋀φ. atoms_ltln (rewrite_modal (rewrite_X φ)) ⊆ atoms_ltln φ"
using rewrite_modal_atoms rewrite_X_atoms by force

show ?thesis
by (simp add: rewrite_iter_fast_def 1 iterate_atoms)
qed

lemma rewrite_iter_slow_atoms:
"atoms_ltln (rewrite_iter_slow φ) ⊆ atoms_ltln φ"
proof -
have 1: "⋀φ. atoms_ltln (rewrite_syn_imp (rewrite_modal (rewrite_X φ))) ⊆ atoms_ltln φ"
using rewrite_syn_imp_atoms rewrite_modal_atoms rewrite_X_atoms by force

show ?thesis
by (simp add: rewrite_iter_slow_def 1 iterate_atoms)
qed

subsection ‹Simplifier›

text ‹We now define a convenience wrapper for the rewriting engine›

datatype mode = Nop | Fast | Slow

fun simplify :: "mode ⇒ 'a ltln ⇒ 'a ltln"
where
"simplify Nop = id"
| "simplify Fast = rewrite_iter_fast"
| "simplify Slow = rewrite_iter_slow"

theorem simplify_correct:
"w ⊨⇩n simplify m φ ⟷ w ⊨⇩n φ"
by (cases m) simp+

lemma simplify_atoms:
"atoms_ltln (simplify m φ) ⊆ atoms_ltln φ"
by (cases m) (insert rewrite_iter_fast_atoms rewrite_iter_slow_atoms, fastforce+)

subsection ‹Code Generation›

code_pred syntactical_implies .

export_code simplify checking

lemma "rewrite_iter_fast (F⇩n (G⇩n (X⇩n prop⇩n(''a'')))) = (F⇩n (G⇩n prop⇩n(''a'')))"
by eval

lemma "rewrite_iter_fast (X⇩n prop⇩n(''a'') U⇩n (X⇩n nprop⇩n(''a''))) = X⇩n (prop⇩n(''a'') U⇩n nprop⇩n(''a''))"
by eval

lemma "rewrite_iter_slow (X⇩n prop⇩n(''a'') U⇩n (X⇩n nprop⇩n(''a''))) = X⇩n (F⇩n nprop⇩n(''a''))"
by eval

end