Theory LTL.LTL

(*
Author:   Salomon Sickert
Author:   Benedikt Seidl
Author:   Alexander Schimpf (original entry: CAVA/LTL.thy)
Author:   Stephan Merz (original entry: Stuttering_Equivalence/PLTL.thy)
*)

section ‹Linear Temporal Logic›

theory LTL
imports
Main "HOL-Library.Omega_Words_Fun"
begin

text ‹This theory provides a formalisation of linear temporal logic. It provides three variants:
\begin{enumerate}
\item LTL with syntactic sugar. This variant is the semantic reference and the included parser
generates ASTs of this datatype.
\item LTL in negation normal form without syntactic sugar. This variant is used by the included
rewriting engine and is used for the translation to automata (implemented in other entries).
\item LTL in restricted negation normal form without the rather uncommon operators weak until''
and strong release''. It is used by the formalization of Gerth's algorithm.
\item PLTL. A variant with a reduced set of operators.
\end{enumerate}
This theory subsumes (and partly reuses) the existing formalisation found in LTL\_to\_GBA and
Stuttering\_Equivalence and unifies them.›

subsection ‹LTL with Syntactic Sugar›

text ‹In this section, we provide a formulation of LTL with explicit syntactic sugar deeply embedded.
This formalization serves as a reference semantics.›

subsubsection ‹Syntax›

datatype (atoms_ltlc: 'a) ltlc =
True_ltlc                               ("true⇩c")
| False_ltlc                              ("false⇩c")
| Prop_ltlc 'a                            ("prop⇩c'(_')")
| Not_ltlc "'a ltlc"                      ("not⇩c _" [85] 85)
| And_ltlc "'a ltlc" "'a ltlc"            ("_ and⇩c _" [82,82] 81)
| Or_ltlc "'a ltlc" "'a ltlc"             ("_ or⇩c _" [81,81] 80)
| Implies_ltlc "'a ltlc" "'a ltlc"        ("_ implies⇩c _" [81,81] 80)
| Next_ltlc "'a ltlc"                     ("X⇩c _" [88] 87)
| Final_ltlc "'a ltlc"                    ("F⇩c _" [88] 87)
| Global_ltlc "'a ltlc"                   ("G⇩c _" [88] 87)
| Until_ltlc "'a ltlc" "'a ltlc"          ("_ U⇩c _" [84,84] 83)
| Release_ltlc "'a ltlc" "'a ltlc"        ("_ R⇩c _" [84,84] 83)
| WeakUntil_ltlc "'a ltlc" "'a ltlc"      ("_ W⇩c _" [84,84] 83)
| StrongRelease_ltlc "'a ltlc" "'a ltlc"  ("_ M⇩c _" [84,84] 83)

definition Iff_ltlc ("_ iff⇩c _" [81,81] 80)
where
"φ iff⇩c ψ ≡ (φ implies⇩c ψ) and⇩c (ψ implies⇩c φ)"

subsubsection ‹Semantics›

primrec semantics_ltlc :: "['a set word, 'a ltlc] ⇒ bool" ("_ ⊨⇩c _" [80,80] 80)
where
"ξ ⊨⇩c true⇩c = True"
| "ξ ⊨⇩c false⇩c = False"
| "ξ ⊨⇩c prop⇩c(q) = (q∈ξ 0)"
| "ξ ⊨⇩c not⇩c φ = (¬ ξ ⊨⇩c φ)"
| "ξ ⊨⇩c φ and⇩c ψ = (ξ ⊨⇩c φ ∧ ξ ⊨⇩c ψ)"
| "ξ ⊨⇩c φ or⇩c ψ = (ξ ⊨⇩c φ ∨ ξ ⊨⇩c ψ)"
| "ξ ⊨⇩c φ implies⇩c ψ = (ξ ⊨⇩c φ ⟶ ξ ⊨⇩c ψ)"
| "ξ ⊨⇩c X⇩c φ = (suffix 1 ξ ⊨⇩c φ)"
| "ξ ⊨⇩c F⇩c φ = (∃i. suffix i ξ ⊨⇩c φ)"
| "ξ ⊨⇩c G⇩c φ = (∀i. suffix i ξ ⊨⇩c φ)"
| "ξ ⊨⇩c φ U⇩c ψ = (∃i. suffix i ξ ⊨⇩c ψ ∧ (∀j<i. suffix j ξ ⊨⇩c φ))"
| "ξ ⊨⇩c φ R⇩c ψ = (∀i. suffix i ξ ⊨⇩c ψ ∨ (∃j<i. suffix j ξ ⊨⇩c φ))"
| "ξ ⊨⇩c φ W⇩c ψ = (∀i. suffix i ξ ⊨⇩c φ ∨ (∃j≤i. suffix j ξ ⊨⇩c ψ))"
| "ξ ⊨⇩c φ M⇩c ψ = (∃i. suffix i ξ ⊨⇩c φ ∧ (∀j≤i. suffix j ξ ⊨⇩c ψ))"

lemma semantics_ltlc_sugar [simp]:
"ξ ⊨⇩c φ iff⇩c ψ = (ξ ⊨⇩c φ ⟷ ξ ⊨⇩c ψ)"
"ξ ⊨⇩c F⇩c φ = ξ ⊨⇩c (true⇩c U⇩c φ)"
"ξ ⊨⇩c G⇩c φ = ξ ⊨⇩c (false⇩c R⇩c φ)"

definition "language_ltlc φ ≡ {ξ. ξ ⊨⇩c φ}"

lemma language_ltlc_negate[simp]:
"language_ltlc (not⇩c φ) = - language_ltlc φ"
unfolding language_ltlc_def by auto

lemma ltl_true_or_con[simp]:
"ξ ⊨⇩c prop⇩c(p) or⇩c (not⇩c prop⇩c(p))"
by auto

lemma ltl_false_true_con[simp]:
"ξ ⊨⇩c not⇩c true⇩c ⟷ ξ ⊨⇩c false⇩c"
by auto

lemma ltl_Next_Neg_con[simp]:
"ξ ⊨⇩c X⇩c (not⇩c φ) ⟷ ξ ⊨⇩c not⇩c X⇩c φ"
by auto

― ‹The connection between dual operators›

lemma ltl_Until_Release_con:
"ξ ⊨⇩c φ R⇩c ψ ⟷ (¬ ξ ⊨⇩c (not⇩c φ) U⇩c (not⇩c ψ))"
"ξ ⊨⇩c φ U⇩c ψ ⟷ (¬ ξ ⊨⇩c (not⇩c φ) R⇩c (not⇩c ψ))"
by auto

lemma ltl_WeakUntil_StrongRelease_con:
"ξ ⊨⇩c φ W⇩c ψ ⟷ (¬ ξ ⊨⇩c (not⇩c φ) M⇩c (not⇩c ψ))"
"ξ ⊨⇩c φ M⇩c ψ ⟷ (¬ ξ ⊨⇩c (not⇩c φ) W⇩c (not⇩c ψ))"
by auto

― ‹The connection between weak and strong operators›

lemma ltl_Release_StrongRelease_con:
"ξ ⊨⇩c φ R⇩c ψ ⟷ ξ ⊨⇩c (φ M⇩c ψ) or⇩c (G⇩c ψ)"
"ξ ⊨⇩c φ M⇩c ψ ⟷ ξ ⊨⇩c (φ R⇩c ψ) and⇩c (F⇩c φ)"
proof safe
assume asm: "ξ ⊨⇩c φ R⇩c ψ"

show "ξ ⊨⇩c (φ M⇩c ψ) or⇩c (G⇩c ψ)"
proof (cases "ξ ⊨⇩c G⇩c ψ")
case False

then obtain i where "¬ suffix i ξ ⊨⇩c ψ" and "∀j<i. suffix j ξ ⊨⇩c ψ"
using exists_least_iff[of "λi. ¬ suffix i ξ ⊨⇩c ψ"] by force

then show ?thesis
using asm by force
qed simp
next
assume asm: "ξ ⊨⇩c (φ R⇩c ψ) and⇩c (F⇩c φ)"

then show "ξ ⊨⇩c φ M⇩c ψ"
proof (cases "ξ ⊨⇩c F⇩c φ")
case True

then obtain i where "suffix i ξ ⊨⇩c φ" and "∀j<i. ¬ suffix j ξ ⊨⇩c φ"
using exists_least_iff[of "λi. suffix i ξ ⊨⇩c φ"] by force

then show ?thesis
using asm by force
qed simp
qed (unfold semantics_ltlc.simps; insert not_less, blast)+

lemma ltl_Until_WeakUntil_con:
"ξ ⊨⇩c φ U⇩c ψ ⟷ ξ ⊨⇩c (φ W⇩c ψ) and⇩c (F⇩c ψ)"
"ξ ⊨⇩c φ W⇩c ψ ⟷ ξ ⊨⇩c (φ U⇩c ψ) or⇩c (G⇩c φ)"
proof safe
assume asm: "ξ ⊨⇩c (φ W⇩c ψ) and⇩c (F⇩c ψ)"

then show "ξ ⊨⇩c φ U⇩c ψ"
proof (cases "ξ ⊨⇩c F⇩c ψ")
case True

then obtain i where "suffix i ξ ⊨⇩c ψ" and "∀j<i. ¬ suffix j ξ ⊨⇩c ψ"
using exists_least_iff[of "λi. suffix i ξ ⊨⇩c ψ"] by force

then show ?thesis
using asm by force
qed simp
next
assume asm: "ξ ⊨⇩c φ W⇩c ψ"

then show "ξ ⊨⇩c (φ U⇩c ψ) or⇩c (G⇩c φ)"
proof (cases "ξ ⊨⇩c G⇩c φ")
case False

then obtain i where "¬ suffix i ξ ⊨⇩c φ" and "∀j<i. suffix j ξ ⊨⇩c φ"
using exists_least_iff[of "λi. ¬ suffix i ξ ⊨⇩c φ"] by force

then show ?thesis
using asm by force
qed simp
qed (unfold semantics_ltlc.simps; insert not_less, blast)+

lemma ltl_StrongRelease_Until_con:
"ξ ⊨⇩c φ M⇩c ψ ⟷ ξ ⊨⇩c ψ U⇩c (φ and⇩c ψ)"
using order.order_iff_strict by auto

lemma ltl_WeakUntil_Release_con:
"ξ ⊨⇩c φ R⇩c ψ ⟷ ξ ⊨⇩c ψ W⇩c (φ and⇩c ψ)"
by (meson ltl_Release_StrongRelease_con(1) ltl_StrongRelease_Until_con ltl_Until_WeakUntil_con(2) semantics_ltlc.simps(6))

definition "pw_eq_on S w w' ≡ ∀i. w i ∩ S = w' i ∩ S"

lemma pw_eq_on_refl[simp]: "pw_eq_on S w w"
and pw_eq_on_sym: "pw_eq_on S w w' ⟹ pw_eq_on S w' w"
and pw_eq_on_trans[trans]: "⟦pw_eq_on S w w'; pw_eq_on S w' w''⟧ ⟹ pw_eq_on S w w''"
unfolding pw_eq_on_def by auto

lemma pw_eq_on_suffix:
"pw_eq_on S w w' ⟹ pw_eq_on S (suffix k w) (suffix k w')"

lemma pw_eq_on_subset:
"S ⊆ S' ⟹ pw_eq_on S' w w' ⟹ pw_eq_on S w w'"

lemma ltlc_eq_on_aux:
"pw_eq_on (atoms_ltlc φ) w w' ⟹ w ⊨⇩c φ ⟹ w' ⊨⇩c φ"
proof (induction φ arbitrary: w w')
case Until_ltlc
thus ?case
by simp (meson Un_upper1 Un_upper2 pw_eq_on_subset pw_eq_on_suffix)
next
case Release_ltlc
thus ?case
by simp (metis Un_upper1 pw_eq_on_subset pw_eq_on_suffix sup_commute)
next
case WeakUntil_ltlc
thus ?case
by simp (meson pw_eq_on_subset pw_eq_on_suffix sup.cobounded1 sup_ge2)
next
case StrongRelease_ltlc
thus ?case
by simp (metis Un_upper1 pw_eq_on_subset pw_eq_on_suffix pw_eq_on_sym sup_ge2)
next
case (And_ltlc φ ψ)
thus ?case
by simp (meson Un_upper1 inf_sup_ord(4) pw_eq_on_subset)
next
case (Or_ltlc φ ψ)
thus ?case
by simp (meson Un_upper2 pw_eq_on_subset sup_ge1)
next
case (Implies_ltlc φ ψ)
thus ?case
by simp (meson Un_upper1 Un_upper2 pw_eq_on_subset[of "atoms_ltlc _" "atoms_ltlc φ ∪ atoms_ltlc ψ"]  pw_eq_on_sym)
qed (auto simp add: pw_eq_on_def; metis suffix_nth)+

lemma ltlc_eq_on:
"pw_eq_on (atoms_ltlc φ) w w' ⟹ w ⊨⇩c φ ⟷ w' ⊨⇩c φ"
using ltlc_eq_on_aux pw_eq_on_sym by blast

lemma suffix_comp: "(λi. f (suffix k w i)) = suffix k (f o w)"
by auto

lemma suffix_range: "⋃(range ξ) ⊆ APs ⟹ ⋃(range (suffix k ξ)) ⊆ APs"
by auto

lemma map_semantics_ltlc_aux:
assumes "inj_on f APs"
assumes "⋃(range w) ⊆ APs"
assumes "atoms_ltlc φ ⊆ APs"
shows "w ⊨⇩c φ ⟷ (λi. f  w i) ⊨⇩c map_ltlc f φ"
using assms(2,3)
proof (induction φ arbitrary: w)
case (Prop_ltlc x)
thus ?case   using assms(1)
next
case (Next_ltlc φ)
show ?case
using Next_ltlc(1)[of "suffix 1 w", unfolded suffix_comp comp_def] Next_ltlc(2,3) apply simp
by (metis Next_ltlc.prems(1) One_nat_def ‹⟦⋃(range (suffix 1 w)) ⊆ APs; atoms_ltlc φ ⊆ APs⟧ ⟹ suffix 1 w ⊨⇩c φ = suffix 1 (λx. f  w x) ⊨⇩c map_ltlc f φ› suffix_range)
next
case (Final_ltlc φ)
thus ?case
using Final_ltlc(1)[of "suffix _ _", unfolded suffix_comp comp_def, OF suffix_range] by fastforce
next
case (Global_ltlc)
thus ?case
using Global_ltlc(1)[of "suffix _ w", unfolded suffix_comp comp_def, OF suffix_range] by fastforce
next
case (Until_ltlc)
thus ?case
using Until_ltlc(1,2)[of "suffix _ w", unfolded suffix_comp comp_def, OF suffix_range] by fastforce
next
case (Release_ltlc)
thus ?case
using Release_ltlc(1,2)[of "suffix _ w", unfolded suffix_comp comp_def, OF suffix_range] by fastforce
next
case (WeakUntil_ltlc)
thus ?case
using WeakUntil_ltlc(1,2)[of "suffix _ w", unfolded suffix_comp comp_def, OF suffix_range] by fastforce
next
case (StrongRelease_ltlc)
thus ?case
using StrongRelease_ltlc(1,2)[of "suffix _ w", unfolded suffix_comp comp_def, OF suffix_range] by fastforce
qed simp+

definition "map_props f APs ≡ {i. ∃p∈APs. f p = Some i}"

lemma map_semantics_ltlc:
assumes INJ: "inj_on f (dom f)" and DOM: "atoms_ltlc φ ⊆ dom f"
shows "ξ ⊨⇩c φ ⟷ (map_props f o ξ) ⊨⇩c map_ltlc (the o f) φ"
proof -
let ?ξr = "λi. ξ i ∩ atoms_ltlc φ"
let ?ξr' = "λi. ξ i ∩ dom f"

have 1: "⋃(range ?ξr) ⊆ atoms_ltlc φ" by auto

have INJ_the_dom: "inj_on (the o f) (dom f)"
using assms
by (auto simp: inj_on_def domIff)
note 2 = subset_inj_on[OF this DOM]

have 3: "(λi. (the o f)  ?ξr' i) = map_props f o ξ" using DOM INJ
apply (auto intro!: ext simp: map_props_def domIff image_iff)
by (metis Int_iff domI option.sel)

have "ξ ⊨⇩c φ ⟷ ?ξr ⊨⇩c φ"
apply (rule ltlc_eq_on)
apply (auto simp: pw_eq_on_def)
done
also from map_semantics_ltlc_aux[OF 2 1 subset_refl]
have "… ⟷ (λi. (the o f)  ?ξr i) ⊨⇩c map_ltlc (the o f) φ" .
also have "… ⟷ (λi. (the o f)  ?ξr' i) ⊨⇩c map_ltlc (the o f) φ"
apply (rule ltlc_eq_on) using DOM INJ
apply (auto simp: pw_eq_on_def ltlc.set_map domIff image_iff)
by (metis Int_iff contra_subsetD domD domI inj_on_eq_iff option.sel)
also note 3
finally show ?thesis .
qed

lemma map_semantics_ltlc_inv:
assumes INJ: "inj_on f (dom f)" and DOM: "atoms_ltlc φ ⊆ dom f"
shows "ξ ⊨⇩c map_ltlc (the o f) φ ⟷ (λi. (the o f) - ξ i) ⊨⇩c φ"
using map_semantics_ltlc[OF assms]
apply simp
apply (intro ltlc_eq_on)
apply (auto simp add: pw_eq_on_def ltlc.set_map map_props_def)
by (metis DOM comp_apply contra_subsetD domD option.sel vimage_eq)

subsection ‹LTL in Negation Normal Form›

text ‹We define a type of LTL formula in negation normal form (NNF).›

subsubsection ‹Syntax›

datatype (atoms_ltln: 'a) ltln  =
True_ltln                               ("true⇩n")
| False_ltln                              ("false⇩n")
| Prop_ltln 'a                            ("prop⇩n'(_')")
| Nprop_ltln 'a                           ("nprop⇩n'(_')")
| And_ltln "'a ltln" "'a ltln"            ("_ and⇩n _" [82,82] 81)
| Or_ltln "'a ltln" "'a ltln"             ("_ or⇩n _" [84,84] 83)
| Next_ltln "'a ltln"                     ("X⇩n _" [88] 87)
| Until_ltln "'a ltln" "'a ltln"          ("_ U⇩n _" [84,84] 83)
| Release_ltln "'a ltln" "'a ltln"        ("_ R⇩n _" [84,84] 83)
| WeakUntil_ltln "'a ltln" "'a ltln"      ("_ W⇩n _" [84,84] 83)
| StrongRelease_ltln "'a ltln" "'a ltln"  ("_ M⇩n _" [84,84] 83)

abbreviation finally⇩n :: "'a ltln ⇒ 'a ltln" ("F⇩n _" [88] 87)
where
"F⇩n φ ≡ true⇩n U⇩n φ"

notation (input) finally⇩n ("♢⇩n _" [88] 87)

abbreviation globally⇩n :: "'a ltln ⇒ 'a ltln" ("G⇩n _" [88] 87)
where
"G⇩n φ ≡ false⇩n R⇩n φ"

notation (input) globally⇩n ("□⇩n _" [88] 87)

subsubsection ‹Semantics›

primrec semantics_ltln :: "['a set word, 'a ltln] ⇒ bool" ("_ ⊨⇩n _" [80,80] 80)
where
"ξ ⊨⇩n true⇩n = True"
| "ξ ⊨⇩n false⇩n = False"
| "ξ ⊨⇩n prop⇩n(q) = (q ∈ ξ 0)"
| "ξ ⊨⇩n nprop⇩n(q) = (q ∉ ξ 0)"
| "ξ ⊨⇩n φ and⇩n ψ = (ξ ⊨⇩n φ ∧ ξ ⊨⇩n ψ)"
| "ξ ⊨⇩n φ or⇩n ψ = (ξ ⊨⇩n φ ∨ ξ ⊨⇩n ψ)"
| "ξ ⊨⇩n X⇩n φ = (suffix 1 ξ ⊨⇩n φ)"
| "ξ ⊨⇩n φ U⇩n ψ = (∃i. suffix i ξ ⊨⇩n ψ ∧ (∀j<i. suffix j ξ ⊨⇩n φ))"
| "ξ ⊨⇩n φ R⇩n ψ = (∀i. suffix i ξ ⊨⇩n ψ ∨ (∃j<i. suffix j ξ ⊨⇩n φ))"
| "ξ ⊨⇩n φ W⇩n ψ = (∀i. suffix i ξ ⊨⇩n φ ∨ (∃j≤i. suffix j ξ ⊨⇩n ψ))"
| "ξ ⊨⇩n φ M⇩n ψ = (∃i. suffix i ξ ⊨⇩n φ ∧ (∀j≤i. suffix j ξ ⊨⇩n ψ))"

definition "language_ltln φ ≡ {ξ. ξ ⊨⇩n φ}"

lemma semantics_ltln_ite_simps[simp]:
"w ⊨⇩n (if P then true⇩n else false⇩n) = P"
"w ⊨⇩n (if P then false⇩n else true⇩n) = (¬P)"
by simp_all

subsubsection ‹Conversion›

fun ltlc_to_ltln' :: "bool ⇒ 'a ltlc ⇒ 'a ltln"
where
"ltlc_to_ltln' False true⇩c = true⇩n"
| "ltlc_to_ltln' False false⇩c = false⇩n"
| "ltlc_to_ltln' False prop⇩c(q) = prop⇩n(q)"
| "ltlc_to_ltln' False (φ and⇩c ψ) = (ltlc_to_ltln' False φ) and⇩n (ltlc_to_ltln' False ψ)"
| "ltlc_to_ltln' False (φ or⇩c ψ) = (ltlc_to_ltln' False φ) or⇩n (ltlc_to_ltln' False ψ)"
| "ltlc_to_ltln' False (φ implies⇩c ψ) = (ltlc_to_ltln' True φ) or⇩n (ltlc_to_ltln' False ψ)"
| "ltlc_to_ltln' False (F⇩c φ) = true⇩n U⇩n (ltlc_to_ltln' False φ)"
| "ltlc_to_ltln' False (G⇩c φ) = false⇩n R⇩n (ltlc_to_ltln' False φ)"
| "ltlc_to_ltln' False (φ U⇩c ψ) = (ltlc_to_ltln' False φ) U⇩n (ltlc_to_ltln' False ψ)"
| "ltlc_to_ltln' False (φ R⇩c ψ) = (ltlc_to_ltln' False φ) R⇩n (ltlc_to_ltln' False ψ)"
| "ltlc_to_ltln' False (φ W⇩c ψ) = (ltlc_to_ltln' False φ) W⇩n (ltlc_to_ltln' False ψ)"
| "ltlc_to_ltln' False (φ M⇩c ψ) = (ltlc_to_ltln' False φ) M⇩n (ltlc_to_ltln' False ψ)"
| "ltlc_to_ltln' True true⇩c = false⇩n"
| "ltlc_to_ltln' True false⇩c = true⇩n"
| "ltlc_to_ltln' True prop⇩c(q) = nprop⇩n(q)"
| "ltlc_to_ltln' True (φ and⇩c ψ) = (ltlc_to_ltln' True φ) or⇩n (ltlc_to_ltln' True ψ)"
| "ltlc_to_ltln' True (φ or⇩c ψ) = (ltlc_to_ltln' True φ) and⇩n (ltlc_to_ltln' True ψ)"
| "ltlc_to_ltln' True (φ implies⇩c ψ) = (ltlc_to_ltln' False φ) and⇩n (ltlc_to_ltln' True ψ)"
| "ltlc_to_ltln' True (F⇩c φ) = false⇩n R⇩n (ltlc_to_ltln' True φ)"
| "ltlc_to_ltln' True (G⇩c φ) = true⇩n U⇩n (ltlc_to_ltln' True φ)"
| "ltlc_to_ltln' True (φ U⇩c ψ) = (ltlc_to_ltln' True φ) R⇩n (ltlc_to_ltln' True ψ)"
| "ltlc_to_ltln' True (φ R⇩c ψ) = (ltlc_to_ltln' True φ) U⇩n (ltlc_to_ltln' True ψ)"
| "ltlc_to_ltln' True (φ W⇩c ψ) = (ltlc_to_ltln' True φ) M⇩n (ltlc_to_ltln' True ψ)"
| "ltlc_to_ltln' True (φ M⇩c ψ) = (ltlc_to_ltln' True φ) W⇩n (ltlc_to_ltln' True ψ)"
| "ltlc_to_ltln' b (not⇩c φ) = ltlc_to_ltln' (¬ b) φ"
| "ltlc_to_ltln' b (X⇩c φ) = X⇩n (ltlc_to_ltln' b φ)"

fun ltlc_to_ltln :: "'a ltlc ⇒ 'a ltln"
where
"ltlc_to_ltln φ = ltlc_to_ltln' False φ"

fun ltln_to_ltlc :: "'a ltln ⇒ 'a ltlc"
where
"ltln_to_ltlc true⇩n = true⇩c"
| "ltln_to_ltlc false⇩n = false⇩c"
| "ltln_to_ltlc prop⇩n(q) = prop⇩c(q)"
| "ltln_to_ltlc nprop⇩n(q) = not⇩c (prop⇩c(q))"
| "ltln_to_ltlc (φ and⇩n ψ) = (ltln_to_ltlc φ and⇩c ltln_to_ltlc ψ)"
| "ltln_to_ltlc (φ or⇩n ψ) = (ltln_to_ltlc φ or⇩c ltln_to_ltlc ψ)"
| "ltln_to_ltlc (X⇩n φ) = (X⇩c ltln_to_ltlc φ)"
| "ltln_to_ltlc (φ U⇩n ψ) = (ltln_to_ltlc φ U⇩c ltln_to_ltlc ψ)"
| "ltln_to_ltlc (φ R⇩n ψ) = (ltln_to_ltlc φ R⇩c ltln_to_ltlc ψ)"
| "ltln_to_ltlc (φ W⇩n ψ) = (ltln_to_ltlc φ W⇩c ltln_to_ltlc ψ)"
| "ltln_to_ltlc (φ M⇩n ψ) = (ltln_to_ltlc φ M⇩c ltln_to_ltlc ψ)"

lemma ltlc_to_ltln'_correct:
"w ⊨⇩n (ltlc_to_ltln' True φ) ⟷ ¬ w ⊨⇩c φ"
"w ⊨⇩n (ltlc_to_ltln' False φ) ⟷ w ⊨⇩c φ"
"size (ltlc_to_ltln' True φ) ≤ 2 * size φ"
"size (ltlc_to_ltln' False φ) ≤ 2 * size φ"
by (induction φ arbitrary: w) simp+

lemma ltlc_to_ltln_semantics [simp]:
"w ⊨⇩n ltlc_to_ltln φ ⟷ w ⊨⇩c φ"
using ltlc_to_ltln'_correct by auto

lemma ltlc_to_ltln_size:
"size (ltlc_to_ltln φ) ≤ 2 * size φ"
using ltlc_to_ltln'_correct by simp

lemma ltln_to_ltlc_semantics [simp]:
"w ⊨⇩c ltln_to_ltlc φ ⟷ w ⊨⇩n φ"
by (induction φ arbitrary: w) simp+

lemma ltlc_to_ltln_atoms:
"atoms_ltln (ltlc_to_ltln φ) = atoms_ltlc φ"
proof -
have "atoms_ltln (ltlc_to_ltln' True φ) = atoms_ltlc φ"
"atoms_ltln (ltlc_to_ltln' False φ) = atoms_ltlc φ"
by (induction φ) simp+
thus ?thesis
by simp
qed

subsubsection ‹Negation›

fun not⇩n
where
"not⇩n true⇩n = false⇩n"
| "not⇩n false⇩n = true⇩n"
| "not⇩n prop⇩n(a) = nprop⇩n(a)"
| "not⇩n nprop⇩n(a) = prop⇩n(a)"
| "not⇩n (φ and⇩n ψ) = (not⇩n φ) or⇩n (not⇩n ψ)"
| "not⇩n (φ or⇩n ψ) = (not⇩n φ) and⇩n (not⇩n ψ)"
| "not⇩n (X⇩n φ) = X⇩n (not⇩n φ)"
| "not⇩n (φ U⇩n ψ) = (not⇩n φ) R⇩n (not⇩n ψ)"
| "not⇩n (φ R⇩n ψ) = (not⇩n φ) U⇩n (not⇩n ψ)"
| "not⇩n (φ W⇩n ψ) = (not⇩n φ) M⇩n (not⇩n ψ)"
| "not⇩n (φ M⇩n ψ) = (not⇩n φ) W⇩n (not⇩n ψ)"

lemma not⇩n_semantics[simp]:
"w ⊨⇩n not⇩n φ ⟷ ¬ w ⊨⇩n φ"
by (induction φ arbitrary: w) auto

lemma not⇩n_size:
"size (not⇩n φ) = size φ"
by (induction φ) auto

subsubsection ‹Subformulas›

fun subfrmlsn :: "'a ltln ⇒ 'a ltln set"
where
"subfrmlsn (φ and⇩n ψ) = {φ and⇩n ψ} ∪ subfrmlsn φ ∪ subfrmlsn ψ"
| "subfrmlsn (φ or⇩n ψ) = {φ or⇩n ψ} ∪ subfrmlsn φ ∪ subfrmlsn ψ"
| "subfrmlsn (X⇩n φ) = {X⇩n φ} ∪ subfrmlsn φ"
| "subfrmlsn (φ U⇩n ψ) = {φ U⇩n ψ} ∪ subfrmlsn φ ∪ subfrmlsn ψ"
| "subfrmlsn (φ R⇩n ψ) = {φ R⇩n ψ} ∪ subfrmlsn φ ∪ subfrmlsn ψ"
| "subfrmlsn (φ W⇩n ψ) = {φ W⇩n ψ} ∪ subfrmlsn φ ∪ subfrmlsn ψ"
| "subfrmlsn (φ M⇩n ψ) = {φ M⇩n ψ} ∪ subfrmlsn φ ∪ subfrmlsn ψ"
| "subfrmlsn φ = {φ}"

lemma subfrmlsn_id[simp]:
"φ ∈ subfrmlsn φ"
by (induction φ) auto

lemma subfrmlsn_finite:
"finite (subfrmlsn φ)"
by (induction φ) auto

lemma subfrmlsn_card:
"card (subfrmlsn φ) ≤ size φ"
by (induction φ) (simp_all add: card_insert_if subfrmlsn_finite, (meson add_le_mono card_Un_le dual_order.trans le_SucI)+)

lemma subfrmlsn_subset:
"ψ ∈ subfrmlsn φ ⟹ subfrmlsn ψ ⊆ subfrmlsn φ"
by (induction φ) auto

lemma subfrmlsn_size:
"ψ ∈ subfrmlsn φ ⟹ size ψ < size φ ∨ ψ = φ"
by (induction φ) auto

abbreviation
"size_set S ≡ sum (λx. 2 * size x + 1) S"

lemma size_set_diff:
"finite S ⟹ S' ⊆ S ⟹ size_set (S - S') = size_set S - size_set S'"
using sum_diff_nat finite_subset by metis

subsubsection ‹Constant Folding›

lemma U_consts[intro, simp]:
"w ⊨⇩n φ U⇩n true⇩n"
"¬ (w ⊨⇩n φ U⇩n false⇩n)"
"(w ⊨⇩n false⇩n U⇩n φ) = (w ⊨⇩n φ)"
by force+

lemma R_consts[intro, simp]:
"w ⊨⇩n φ R⇩n true⇩n"
"¬ (w ⊨⇩n φ R⇩n false⇩n)"
"(w ⊨⇩n true⇩n R⇩n φ) = (w ⊨⇩n φ)"
by force+

lemma W_consts[intro, simp]:
"w ⊨⇩n true⇩n W⇩n φ"
"w ⊨⇩n φ W⇩n true⇩n"
"(w ⊨⇩n false⇩n W⇩n φ) = (w ⊨⇩n φ)"
"(w ⊨⇩n φ W⇩n false⇩n) = (w ⊨⇩n G⇩n φ)"
by force+

lemma M_consts[intro, simp]:
"¬ (w ⊨⇩n false⇩n M⇩n φ)"
"¬ (w ⊨⇩n φ M⇩n false⇩n)"
"(w ⊨⇩n true⇩n M⇩n φ) = (w ⊨⇩n φ)"
"(w ⊨⇩n φ M⇩n true⇩n) = (w ⊨⇩n F⇩n φ)"
by force+

subsubsection ‹Distributivity›

lemma until_and_left_distrib:
"w ⊨⇩n (φ⇩1 and⇩n φ⇩2) U⇩n ψ ⟷ w ⊨⇩n (φ⇩1 U⇩n ψ) and⇩n (φ⇩2 U⇩n ψ)"
proof
assume "w ⊨⇩n φ⇩1 U⇩n ψ and⇩n φ⇩2 U⇩n ψ"

then obtain i1 i2 where "suffix i1 w ⊨⇩n ψ ∧ (∀j<i1. suffix j w ⊨⇩n φ⇩1)" and "suffix i2 w ⊨⇩n ψ ∧ (∀j<i2. suffix j w ⊨⇩n φ⇩2)"
by auto

then have "suffix (min i1 i2) w ⊨⇩n ψ ∧ (∀j<min i1 i2. suffix j w ⊨⇩n φ⇩1 and⇩n φ⇩2)"

then show "w ⊨⇩n (φ⇩1 and⇩n φ⇩2) U⇩n ψ"
by force
qed auto

lemma until_or_right_distrib:
"w ⊨⇩n φ U⇩n (ψ⇩1 or⇩n ψ⇩2) ⟷ w ⊨⇩n (φ U⇩n ψ⇩1) or⇩n (φ U⇩n ψ⇩2)"
by auto

lemma release_and_right_distrib:
"w ⊨⇩n φ R⇩n (ψ⇩1 and⇩n ψ⇩2) ⟷ w ⊨⇩n (φ R⇩n ψ⇩1) and⇩n (φ R⇩n ψ⇩2)"
by auto

lemma release_or_left_distrib:
"w ⊨⇩n (φ⇩1 or⇩n φ⇩2) R⇩n ψ ⟷ w ⊨⇩n (φ⇩1 R⇩n ψ) or⇩n (φ⇩2 R⇩n ψ)"
by (metis not⇩n.simps(6) not⇩n.simps(9) not⇩n_semantics until_and_left_distrib)

lemma strong_release_and_right_distrib:
"w ⊨⇩n φ M⇩n (ψ⇩1 and⇩n ψ⇩2) ⟷ w ⊨⇩n (φ M⇩n ψ⇩1) and⇩n (φ M⇩n ψ⇩2)"
proof
assume "w ⊨⇩n (φ M⇩n ψ⇩1) and⇩n (φ M⇩n ψ⇩2)"

then obtain i1 i2 where "suffix i1 w ⊨⇩n φ ∧ (∀j≤i1. suffix j w ⊨⇩n ψ⇩1)" and "suffix i2 w ⊨⇩n φ ∧ (∀j≤i2. suffix j w ⊨⇩n ψ⇩2)"
by auto

then have "suffix (min i1 i2) w ⊨⇩n φ ∧ (∀j≤min i1 i2. suffix j w ⊨⇩n ψ⇩1 and⇩n ψ⇩2)"

then show "w ⊨⇩n φ M⇩n (ψ⇩1 and⇩n ψ⇩2)"
by force
qed auto

lemma strong_release_or_left_distrib:
"w ⊨⇩n (φ⇩1 or⇩n φ⇩2) M⇩n ψ ⟷ w ⊨⇩n (φ⇩1 M⇩n ψ) or⇩n (φ⇩2 M⇩n ψ)"
by auto

lemma weak_until_and_left_distrib:
"w ⊨⇩n (φ⇩1 and⇩n φ⇩2) W⇩n ψ ⟷ w ⊨⇩n (φ⇩1 W⇩n ψ) and⇩n (φ⇩2 W⇩n ψ)"
by auto

lemma weak_until_or_right_distrib:
"w ⊨⇩n φ W⇩n (ψ⇩1 or⇩n ψ⇩2) ⟷ w ⊨⇩n (φ W⇩n ψ⇩1) or⇩n (φ W⇩n ψ⇩2)"
by (metis not⇩n.simps(10) not⇩n.simps(6) not⇩n_semantics strong_release_and_right_distrib)

lemma next_until_distrib:
"w ⊨⇩n X⇩n (φ U⇩n ψ) ⟷ w ⊨⇩n (X⇩n φ) U⇩n (X⇩n ψ)"
by auto

lemma next_release_distrib:
"w ⊨⇩n X⇩n (φ R⇩n ψ) ⟷ w ⊨⇩n (X⇩n φ) R⇩n (X⇩n ψ)"
by auto

lemma next_weak_until_distrib:
"w ⊨⇩n X⇩n (φ W⇩n ψ) ⟷ w ⊨⇩n (X⇩n φ) W⇩n (X⇩n ψ)"
by auto

lemma next_strong_release_distrib:
"w ⊨⇩n X⇩n (φ M⇩n ψ) ⟷ w ⊨⇩n (X⇩n φ) M⇩n (X⇩n ψ)"
by auto

subsubsection ‹Nested operators›

lemma finally_until[simp]:
"w ⊨⇩n F⇩n (φ U⇩n ψ) ⟷ w ⊨⇩n F⇩n ψ"
by auto force

lemma globally_release[simp]:
"w ⊨⇩n G⇩n (φ R⇩n ψ) ⟷ w ⊨⇩n G⇩n ψ"
by auto force

lemma globally_weak_until[simp]:
"w ⊨⇩n G⇩n (φ W⇩n ψ) ⟷ w ⊨⇩n G⇩n (φ or⇩n ψ)"
by auto force

lemma finally_strong_release[simp]:
"w ⊨⇩n F⇩n (φ M⇩n ψ) ⟷ w ⊨⇩n F⇩n (φ and⇩n ψ)"
by auto force

subsubsection ‹Weak and strong operators›

lemma ltln_weak_strong:
"w ⊨⇩n φ W⇩n ψ ⟷ w ⊨⇩n (G⇩n φ) or⇩n (φ U⇩n ψ)"
"w ⊨⇩n φ R⇩n ψ ⟷ w ⊨⇩n (G⇩n ψ) or⇩n (φ M⇩n ψ)"
proof auto
fix i
assume "∀i. suffix i w ⊨⇩n φ ∨ (∃j≤i. suffix j w ⊨⇩n ψ)"
and "∀i. suffix i w ⊨⇩n ψ ⟶ (∃j<i. ¬ suffix j w ⊨⇩n φ)"

then show "suffix i w ⊨⇩n φ"
by (induction i rule: less_induct) force
next
fix i k
assume "∀j≤i. ¬ suffix j w ⊨⇩n ψ"
and "suffix k w ⊨⇩n ψ"
and "∀j<k. suffix j w ⊨⇩n φ"

then show "suffix i w ⊨⇩n φ"
by (cases "i < k") simp_all
next
fix i
assume "∀i. suffix i w ⊨⇩n ψ ∨ (∃j<i. suffix j w ⊨⇩n φ)"
and "∀i. suffix i w ⊨⇩n φ ⟶ (∃j≤i. ¬ suffix j w ⊨⇩n ψ)"

then show "suffix i w ⊨⇩n ψ"
by (induction i rule: less_induct) force
next
fix i k
assume "∀j<i. ¬ suffix j w ⊨⇩n φ"
and "suffix k w ⊨⇩n φ"
and "∀j≤k. suffix j w ⊨⇩n ψ"

then show "suffix i w ⊨⇩n ψ"
by (cases "i ≤ k") simp_all
qed

lemma ltln_strong_weak:
"w ⊨⇩n φ U⇩n ψ ⟷ w ⊨⇩n (F⇩n ψ) and⇩n (φ W⇩n ψ)"
"w ⊨⇩n φ M⇩n ψ ⟷ w ⊨⇩n (F⇩n φ) and⇩n (φ R⇩n ψ)"
by (metis ltln_weak_strong not⇩n.simps(1,5,8-11) not⇩n_semantics)+

lemma ltln_strong_to_weak:
"w ⊨⇩n φ U⇩n ψ ⟹ w ⊨⇩n φ W⇩n ψ"
"w ⊨⇩n φ M⇩n ψ ⟹ w ⊨⇩n φ R⇩n ψ"
using ltln_weak_strong by simp_all blast+

lemma ltln_weak_to_strong:
"⟦w ⊨⇩n φ W⇩n ψ; ¬ w ⊨⇩n G⇩n φ⟧ ⟹ w ⊨⇩n φ U⇩n ψ"
"⟦w ⊨⇩n φ W⇩n ψ; w ⊨⇩n F⇩n ψ⟧ ⟹ w ⊨⇩n φ U⇩n ψ"
"⟦w ⊨⇩n φ R⇩n ψ; ¬ w ⊨⇩n G⇩n ψ⟧ ⟹ w ⊨⇩n φ M⇩n ψ"
"⟦w ⊨⇩n φ R⇩n ψ; w ⊨⇩n F⇩n φ⟧ ⟹ w ⊨⇩n φ M⇩n ψ"
unfolding ltln_weak_strong[of w φ ψ] by auto

lemma ltln_StrongRelease_to_Until:
"w ⊨⇩n φ M⇩n ψ ⟷ w ⊨⇩n ψ U⇩n (φ and⇩n ψ)"
using order.order_iff_strict by auto

lemma ltln_Release_to_WeakUntil:
"w ⊨⇩n φ R⇩n ψ ⟷ w ⊨⇩n ψ W⇩n (φ and⇩n ψ)"
by (meson ltln_StrongRelease_to_Until ltln_weak_strong semantics_ltln.simps(6))

lemma ltln_WeakUntil_to_Release:
"w ⊨⇩n φ W⇩n ψ ⟷ w ⊨⇩n ψ R⇩n (φ or⇩n ψ)"
by (metis ltln_StrongRelease_to_Until not⇩n.simps(6,9,10) not⇩n_semantics)

lemma ltln_Until_to_StrongRelease:
"w ⊨⇩n φ U⇩n ψ ⟷ w ⊨⇩n ψ M⇩n (φ or⇩n ψ)"
by (metis ltln_Release_to_WeakUntil not⇩n.simps(6,8,11) not⇩n_semantics)

subsubsection ‹GF and FG semantics›

lemma GF_suffix:
"suffix i w ⊨⇩n G⇩n (F⇩n ψ) ⟷ w ⊨⇩n G⇩n (F⇩n ψ)"

lemma FG_suffix:
"suffix i w ⊨⇩n F⇩n (G⇩n ψ) ⟷ w ⊨⇩n F⇩n (G⇩n ψ)"

lemma GF_Inf_many:
"w ⊨⇩n G⇩n (F⇩n φ) ⟷ (∃⇩∞ i. suffix i w ⊨⇩n φ)"
unfolding INFM_nat_le
by simp (blast dest: le_Suc_ex intro: le_add1)

lemma FG_Alm_all:
"w ⊨⇩n F⇩n (G⇩n φ) ⟷ (∀⇩∞ i. suffix i w ⊨⇩n φ)"
unfolding MOST_nat_le
by simp (blast dest: le_Suc_ex intro: le_add1)

(* TODO: move to Infinite_Set.thy ?? *)
"(∀⇩∞i::nat. P i) ⟷ (∀⇩∞i. P (i + j))"

"(∃⇩∞i::nat. P i) ⟷ (∃⇩∞i. P (i + j))"
using MOST_nat_add not_MOST not_INFM by blast

lemma FG_suffix_G:
"w ⊨⇩n F⇩n (G⇩n φ) ⟹ ∀⇩∞i. suffix i w ⊨⇩n G⇩n φ"
proof -
assume "w ⊨⇩n F⇩n (G⇩n φ)"
then have "w ⊨⇩n F⇩n (G⇩n (G⇩n φ))"
by (meson globally_release semantics_ltln.simps(8))
then show "∀⇩∞i. suffix i w  ⊨⇩n G⇩n φ"
unfolding FG_Alm_all .
qed

lemma Alm_all_GF_F:
"∀⇩∞i. suffix i w ⊨⇩n G⇩n (F⇩n ψ) ⟷ suffix i w ⊨⇩n F⇩n ψ"
unfolding MOST_nat
proof standard+
fix i :: nat
assume "suffix i w ⊨⇩n G⇩n (F⇩n ψ)"
then show "suffix i w ⊨⇩n F⇩n ψ"
unfolding GF_Inf_many INFM_nat by fastforce
next
fix i :: nat
assume suffix: "suffix i w ⊨⇩n F⇩n ψ"
assume max: "i > Max {i. suffix i w ⊨⇩n ψ}"

with suffix obtain j where "j ≥ i" and j_suffix: "suffix j w ⊨⇩n ψ"

with max have j_max: "j > Max {i. suffix i w ⊨⇩n ψ}"
by fastforce

show "suffix i w ⊨⇩n G⇩n (F⇩n ψ)"
proof (cases "w ⊨⇩n G⇩n (F⇩n ψ)")
case False
then have "¬ (∃⇩∞i. suffix i w ⊨⇩n ψ)"
unfolding GF_Inf_many by simp
then have "finite {i. suffix i w ⊨⇩n ψ}"
then have "∀i>Max {i. suffix i w ⊨⇩n ψ}. ¬ suffix i w ⊨⇩n ψ"
using Max_ge not_le by auto
then show ?thesis
using j_suffix j_max by blast
qed force
qed

lemma Alm_all_FG_G:
"∀⇩∞i. suffix i w ⊨⇩n F⇩n (G⇩n ψ) ⟷ suffix i w ⊨⇩n G⇩n ψ"
unfolding MOST_nat
proof standard+
fix i :: nat
assume "suffix i w ⊨⇩n G⇩n ψ"
then show "suffix i w ⊨⇩n F⇩n (G⇩n ψ)"
unfolding FG_Alm_all INFM_nat by fastforce
next
fix i :: nat
assume suffix: "suffix i w ⊨⇩n F⇩n (G⇩n ψ)"
assume max: "i > Max {i. ¬ suffix i w ⊨⇩n G⇩n ψ}"

with suffix have "∀⇩∞j. suffix (i + j) w ⊨⇩n G⇩n ψ"
using FG_suffix_G[of "suffix i w"] suffix_suffix
by fastforce
then have "¬ (∃⇩∞j. ¬ suffix j w ⊨⇩n G⇩n ψ)"
using MOST_nat_add[of "λi. suffix i w ⊨⇩n G⇩n ψ" i]
then have "finite {i. ¬ suffix i w ⊨⇩n G⇩n ψ}"

with max show "suffix i w ⊨⇩n G⇩n ψ"
using Max_ge leD by blast
qed

subsubsection ‹Expansion›

lemma ltln_expand_Until:
"ξ ⊨⇩n φ U⇩n ψ ⟷ (ξ ⊨⇩n ψ or⇩n (φ and⇩n (X⇩n (φ U⇩n ψ))))"
(is "?lhs = ?rhs")
proof
assume ?lhs
then obtain i where "suffix i ξ ⊨⇩n ψ"
and "∀j<i. suffix j ξ ⊨⇩n φ"
by auto
thus ?rhs
by (cases i) auto
next
assume ?rhs
show ?lhs
proof (cases "ξ ⊨⇩n ψ")
case False
then have "ξ ⊨⇩n φ" and "ξ ⊨⇩n X⇩n (φ U⇩n ψ)"
using ‹?rhs› by auto
thus ?lhs
using less_Suc_eq_0_disj suffix_singleton_suffix by force
qed force
qed

lemma ltln_expand_Release:
"ξ ⊨⇩n φ R⇩n ψ ⟷ (ξ ⊨⇩n ψ and⇩n (φ or⇩n (X⇩n (φ R⇩n ψ))))"
(is "?lhs = ?rhs")
proof
assume ?lhs
thus ?rhs
using less_Suc_eq_0_disj by force
next
assume ?rhs

{
fix i
assume "¬ suffix i ξ ⊨⇩n ψ"
then have "∃j<i. suffix j ξ ⊨⇩n φ"
using ‹?rhs› by (cases i) force+
}

thus ?lhs
by auto
qed

lemma ltln_expand_WeakUntil:
"ξ ⊨⇩n φ W⇩n ψ ⟷ (ξ ⊨⇩n ψ or⇩n (φ and⇩n (X⇩n (φ W⇩n ψ))))"
(is "?lhs = ?rhs")
proof
assume ?lhs
thus ?rhs
by (metis ltln_expand_Release ltln_expand_Until ltln_weak_strong(1) semantics_ltln.simps(2,5,6,7))
next
assume ?rhs

{
fix i
assume "¬ suffix i ξ ⊨⇩n φ"
then have "∃j≤i. suffix j ξ ⊨⇩n ψ"
using ‹?rhs› by (cases i) force+
}

thus ?lhs
by auto
qed

lemma ltln_expand_StrongRelease:
"ξ ⊨⇩n φ M⇩n ψ ⟷ (ξ ⊨⇩n ψ and⇩n (φ or⇩n (X⇩n (φ M⇩n ψ))))"
(is "?lhs = ?rhs")
proof
assume ?lhs
then obtain i where "suffix i ξ ⊨⇩n φ"
and "∀j≤i. suffix j ξ ⊨⇩n ψ"
by auto
thus ?rhs
by (cases i) auto
next
assume ?rhs
show ?lhs
proof (cases "ξ ⊨⇩n φ")
case True
thus ?lhs
using ‹?rhs› ltln_expand_WeakUntil by fastforce
next
case False
thus ?lhs
by (metis ‹?rhs› ltln_expand_WeakUntil not⇩n.simps(5,6,7,11) not⇩n_semantics)
qed
qed

lemma ltln_Release_alterdef:
"w ⊨⇩n φ R⇩n ψ ⟷ w ⊨⇩n (G⇩n ψ) or⇩n (ψ U⇩n (φ and⇩n ψ))"
proof (cases "∃i. ¬suffix i w ⊨⇩n ψ")
case True
define i where "i ≡ Least (λi. ¬suffix i w ⊨⇩n ψ)"
have "⋀j. j < i ⟹ suffix j w ⊨⇩n ψ" and "¬ suffix i w ⊨⇩n ψ"
using True LeastI not_less_Least unfolding i_def by fast+
hence *: "∀i. suffix i w ⊨⇩n ψ ∨ (∃j<i. suffix j w ⊨⇩n φ) ⟹ (∃i. (suffix i w ⊨⇩n ψ ∧ suffix i w ⊨⇩n φ) ∧ (∀j<i. suffix j w ⊨⇩n ψ))"
by fastforce
hence "∃i. (suffix i w ⊨⇩n ψ ∧ suffix i w ⊨⇩n φ) ∧ (∀j<i. suffix j w ⊨⇩n ψ) ⟹ (∀i. suffix i w ⊨⇩n ψ ∨ (∃j<i. suffix j w ⊨⇩n φ))"
using linorder_cases by blast
thus ?thesis
using True * by auto
qed auto

subsection ‹LTL in restricted Negation Normal Form›

text ‹Some algorithms do not handle the operators W and M,
hence we also provide a datatype without these two operators.›

subsubsection ‹Syntax›

datatype (atoms_ltlr: 'a) ltlr =
True_ltlr                               ("true⇩r")
| False_ltlr                              ("false⇩r")
| Prop_ltlr 'a                            ("prop⇩r'(_')")
| Nprop_ltlr 'a                           ("nprop⇩r'(_')")
| And_ltlr "'a ltlr" "'a ltlr"            ("_ and⇩r _" [82,82] 81)
| Or_ltlr "'a ltlr" "'a ltlr"             ("_ or⇩r _" [84,84] 83)
| Next_ltlr "'a ltlr"                     ("X⇩r _" [88] 87)
| Until_ltlr "'a ltlr" "'a ltlr"          ("_ U⇩r _" [84,84] 83)
| Release_ltlr "'a ltlr" "'a ltlr"        ("_ R⇩r _" [84,84] 83)

subsubsection ‹Semantics›

primrec semantics_ltlr :: "['a set word, 'a ltlr] ⇒ bool" ("_ ⊨⇩r _" [80,80] 80)
where
"ξ ⊨⇩r true⇩r = True"
| "ξ ⊨⇩r false⇩r = False"
| "ξ ⊨⇩r prop⇩r(q) = (q ∈ ξ 0)"
| "ξ ⊨⇩r nprop⇩r(q) = (q ∉ ξ 0)"
| "ξ ⊨⇩r φ and⇩r ψ = (ξ ⊨⇩r φ ∧ ξ ⊨⇩r ψ)"
| "ξ ⊨⇩r φ or⇩r ψ = (ξ ⊨⇩r φ ∨ ξ ⊨⇩r ψ)"
| "ξ ⊨⇩r X⇩r φ = (suffix 1 ξ ⊨⇩r φ)"
| "ξ ⊨⇩r φ U⇩r ψ = (∃i. suffix i ξ ⊨⇩r ψ ∧ (∀j<i. suffix j ξ ⊨⇩r φ))"
| "ξ ⊨⇩r φ R⇩r ψ = (∀i. suffix i ξ ⊨⇩r ψ ∨ (∃j<i. suffix j ξ ⊨⇩r φ))"

subsubsection ‹Conversion›

fun ltln_to_ltlr :: "'a ltln ⇒ 'a ltlr"
where
"ltln_to_ltlr true⇩n = true⇩r"
| "ltln_to_ltlr false⇩n = false⇩r"
| "ltln_to_ltlr prop⇩n(a) = prop⇩r(a)"
| "ltln_to_ltlr nprop⇩n(a) = nprop⇩r(a)"
| "ltln_to_ltlr (φ and⇩n ψ) = (ltln_to_ltlr φ) and⇩r (ltln_to_ltlr ψ)"
| "ltln_to_ltlr (φ or⇩n ψ) = (ltln_to_ltlr φ) or⇩r (ltln_to_ltlr ψ)"
| "ltln_to_ltlr (X⇩n φ) = X⇩r (ltln_to_ltlr φ)"
| "ltln_to_ltlr (φ U⇩n ψ) = (ltln_to_ltlr φ) U⇩r (ltln_to_ltlr ψ)"
| "ltln_to_ltlr (φ R⇩n ψ) = (ltln_to_ltlr φ) R⇩r (ltln_to_ltlr ψ)"
| "ltln_to_ltlr (φ W⇩n ψ) = (ltln_to_ltlr ψ) R⇩r ((ltln_to_ltlr φ) or⇩r (ltln_to_ltlr ψ))"
| "ltln_to_ltlr (φ M⇩n ψ) = (ltln_to_ltlr ψ) U⇩r ((ltln_to_ltlr φ) and⇩r (ltln_to_ltlr ψ))"

fun ltlr_to_ltln :: "'a ltlr ⇒ 'a ltln"
where
"ltlr_to_ltln true⇩r = true⇩n"
| "ltlr_to_ltln false⇩r = false⇩n"
| "ltlr_to_ltln prop⇩r(a) = prop⇩n(a)"
| "ltlr_to_ltln nprop⇩r(a) = nprop⇩n(a)"
| "ltlr_to_ltln (φ and⇩r ψ) = (ltlr_to_ltln φ) and⇩n (ltlr_to_ltln ψ)"
| "ltlr_to_ltln (φ or⇩r ψ) = (ltlr_to_ltln φ) or⇩n (ltlr_to_ltln