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)
    License:  BSD
*)

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                               ("truec")
  | False_ltlc                              ("falsec")
  | Prop_ltlc 'a                            ("propc'(_')")
  | Not_ltlc "'a ltlc"                      ("notc _" [85] 85)
  | And_ltlc "'a ltlc" "'a ltlc"            ("_ andc _" [82,82] 81)
  | Or_ltlc "'a ltlc" "'a ltlc"             ("_ orc _" [81,81] 80)
  | Implies_ltlc "'a ltlc" "'a ltlc"        ("_ impliesc _" [81,81] 80)
  | Next_ltlc "'a ltlc"                     ("Xc _" [88] 87)
  | Final_ltlc "'a ltlc"                    ("Fc _" [88] 87)
  | Global_ltlc "'a ltlc"                   ("Gc _" [88] 87)
  | Until_ltlc "'a ltlc" "'a ltlc"          ("_ Uc _" [84,84] 83)
  | Release_ltlc "'a ltlc" "'a ltlc"        ("_ Rc _" [84,84] 83)
  | WeakUntil_ltlc "'a ltlc" "'a ltlc"      ("_ Wc _" [84,84] 83)
  | StrongRelease_ltlc "'a ltlc" "'a ltlc"  ("_ Mc _" [84,84] 83)

definition Iff_ltlc ("_ iffc _" [81,81] 80)
where
  "φ iffc ψ ≡ (φ impliesc ψ) andc (ψ impliesc φ)"

subsubsection ‹Semantics›

primrec semantics_ltlc :: "['a set word, 'a ltlc] ⇒ bool" ("_ ⊨c _" [80,80] 80)
where
  "ξ ⊨c truec = True"
| "ξ ⊨c falsec = False"
| "ξ ⊨c propc(q) = (q∈ξ 0)"
| "ξ ⊨c notc φ = (¬ ξ ⊨c φ)"
| "ξ ⊨c φ andc ψ = (ξ ⊨c φ ∧ ξ ⊨c ψ)"
| "ξ ⊨c φ orc ψ = (ξ ⊨c φ ∨ ξ ⊨c ψ)"
| "ξ ⊨c φ impliesc ψ = (ξ ⊨c φ ⟶ ξ ⊨c ψ)"
| "ξ ⊨c Xc φ = (suffix 1 ξ ⊨c φ)"
| "ξ ⊨c Fc φ = (∃i. suffix i ξ ⊨c φ)"
| "ξ ⊨c Gc φ = (∀i. suffix i ξ ⊨c φ)"
| "ξ ⊨c φ Uc ψ = (∃i. suffix i ξ ⊨c ψ ∧ (∀j<i. suffix j ξ ⊨c φ))"
| "ξ ⊨c φ Rc ψ = (∀i. suffix i ξ ⊨c ψ ∨ (∃j<i. suffix j ξ ⊨c φ))"
| "ξ ⊨c φ Wc ψ = (∀i. suffix i ξ ⊨c φ ∨ (∃j≤i. suffix j ξ ⊨c ψ))"
| "ξ ⊨c φ Mc ψ = (∃i. suffix i ξ ⊨c φ ∧ (∀j≤i. suffix j ξ ⊨c ψ))"

lemma semantics_ltlc_sugar [simp]:
  "ξ ⊨c φ iffc ψ = (ξ ⊨c φ ⟷ ξ ⊨c ψ)"
  "ξ ⊨c Fc φ = ξ ⊨c (truec Uc φ)"
  "ξ ⊨c Gc φ = ξ ⊨c (falsec Rc φ)"
  by (auto simp add: Iff_ltlc_def)

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

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

lemma ltl_true_or_con[simp]:
  "ξ ⊨c propc(p) orc (notc propc(p))"
  by auto

lemma ltl_false_true_con[simp]:
  "ξ ⊨c notc truec ⟷ ξ ⊨c falsec"
  by auto

lemma ltl_Next_Neg_con[simp]:
  "ξ ⊨c Xc (notc φ) ⟷ ξ ⊨c notc Xc φ"
  by auto

― ‹The connection between dual operators›

lemma ltl_Until_Release_con:
  "ξ ⊨c φ Rc ψ ⟷ (¬ ξ ⊨c (notc φ) Uc (notc ψ))"
  "ξ ⊨c φ Uc ψ ⟷ (¬ ξ ⊨c (notc φ) Rc (notc ψ))"
  by auto

lemma ltl_WeakUntil_StrongRelease_con:
  "ξ ⊨c φ Wc ψ ⟷ (¬ ξ ⊨c (notc φ) Mc (notc ψ))"
  "ξ ⊨c φ Mc ψ ⟷ (¬ ξ ⊨c (notc φ) Wc (notc ψ))"
  by auto

― ‹The connection between weak and strong operators›

lemma ltl_Release_StrongRelease_con:
  "ξ ⊨c φ Rc ψ ⟷ ξ ⊨c (φ Mc ψ) orc (Gc ψ)"
  "ξ ⊨c φ Mc ψ ⟷ ξ ⊨c (φ Rc ψ) andc (Fc φ)"
proof safe
  assume asm: "ξ ⊨c φ Rc ψ"

  show "ξ ⊨c (φ Mc ψ) orc (Gc ψ)"
  proof (cases "ξ ⊨c Gc ψ")
    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 (φ Rc ψ) andc (Fc φ)"

  then show "ξ ⊨c φ Mc ψ"
  proof (cases "ξ ⊨c Fc φ")
    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 φ Uc ψ ⟷ ξ ⊨c (φ Wc ψ) andc (Fc ψ)"
  "ξ ⊨c φ Wc ψ ⟷ ξ ⊨c (φ Uc ψ) orc (Gc φ)"
proof safe
  assume asm: "ξ ⊨c (φ Wc ψ) andc (Fc ψ)"

  then show "ξ ⊨c φ Uc ψ"
  proof (cases "ξ ⊨c Fc ψ")
    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 φ Wc ψ"

  then show "ξ ⊨c (φ Uc ψ) orc (Gc φ)"
  proof (cases "ξ ⊨c Gc φ")
    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 φ Mc ψ ⟷ ξ ⊨c ψ Uc (φ andc ψ)"
  using order.order_iff_strict by auto

lemma ltl_WeakUntil_Release_con:
  "ξ ⊨c φ Rc ψ ⟷ ξ ⊨c ψ Wc (φ andc ψ)"
  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')"
  by (simp add: pw_eq_on_def)

lemma pw_eq_on_subset:
  "S ⊆ S' ⟹ pw_eq_on S' w w' ⟹ pw_eq_on S w w'"
  by (auto simp add: pw_eq_on_def)

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)
      by (simp add: SUP_le_iff inj_on_image_mem_iff)
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                               ("truen")
  | False_ltln                              ("falsen")
  | Prop_ltln 'a                            ("propn'(_')")
  | Nprop_ltln 'a                           ("npropn'(_')")
  | And_ltln "'a ltln" "'a ltln"            ("_ andn _" [82,82] 81)
  | Or_ltln "'a ltln" "'a ltln"             ("_ orn _" [84,84] 83)
  | Next_ltln "'a ltln"                     ("Xn _" [88] 87)
  | Until_ltln "'a ltln" "'a ltln"          ("_ Un _" [84,84] 83)
  | Release_ltln "'a ltln" "'a ltln"        ("_ Rn _" [84,84] 83)
  | WeakUntil_ltln "'a ltln" "'a ltln"      ("_ Wn _" [84,84] 83)
  | StrongRelease_ltln "'a ltln" "'a ltln"  ("_ Mn _" [84,84] 83)

abbreviation finallyn :: "'a ltln ⇒ 'a ltln" ("Fn _" [88] 87)
where
  "Fn φ ≡ truen Un φ"

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

abbreviation globallyn :: "'a ltln ⇒ 'a ltln" ("Gn _" [88] 87)
where
  "Gn φ ≡ falsen Rn φ"

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

subsubsection ‹Semantics›

primrec semantics_ltln :: "['a set word, 'a ltln] ⇒ bool" ("_ ⊨n _" [80,80] 80)
where
  "ξ ⊨n truen = True"
| "ξ ⊨n falsen = False"
| "ξ ⊨n propn(q) = (q ∈ ξ 0)"
| "ξ ⊨n npropn(q) = (q ∉ ξ 0)"
| "ξ ⊨n φ andn ψ = (ξ ⊨n φ ∧ ξ ⊨n ψ)"
| "ξ ⊨n φ orn ψ = (ξ ⊨n φ ∨ ξ ⊨n ψ)"
| "ξ ⊨n Xn φ = (suffix 1 ξ ⊨n φ)"
| "ξ ⊨n φ Un ψ = (∃i. suffix i ξ ⊨n ψ ∧ (∀j<i. suffix j ξ ⊨n φ))"
| "ξ ⊨n φ Rn ψ = (∀i. suffix i ξ ⊨n ψ ∨ (∃j<i. suffix j ξ ⊨n φ))"
| "ξ ⊨n φ Wn ψ = (∀i. suffix i ξ ⊨n φ ∨ (∃j≤i. suffix j ξ ⊨n ψ))"
| "ξ ⊨n φ Mn ψ = (∃i. suffix i ξ ⊨n φ ∧ (∀j≤i. suffix j ξ ⊨n ψ))"

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

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

subsubsection ‹Conversion›

fun ltlc_to_ltln' :: "bool ⇒ 'a ltlc ⇒ 'a ltln"
where
  "ltlc_to_ltln' False truec = truen"
| "ltlc_to_ltln' False falsec = falsen"
| "ltlc_to_ltln' False propc(q) = propn(q)"
| "ltlc_to_ltln' False (φ andc ψ) = (ltlc_to_ltln' False φ) andn (ltlc_to_ltln' False ψ)"
| "ltlc_to_ltln' False (φ orc ψ) = (ltlc_to_ltln' False φ) orn (ltlc_to_ltln' False ψ)"
| "ltlc_to_ltln' False (φ impliesc ψ) = (ltlc_to_ltln' True φ) orn (ltlc_to_ltln' False ψ)"
| "ltlc_to_ltln' False (Fc φ) = truen Un (ltlc_to_ltln' False φ)"
| "ltlc_to_ltln' False (Gc φ) = falsen Rn (ltlc_to_ltln' False φ)"
| "ltlc_to_ltln' False (φ Uc ψ) = (ltlc_to_ltln' False φ) Un (ltlc_to_ltln' False ψ)"
| "ltlc_to_ltln' False (φ Rc ψ) = (ltlc_to_ltln' False φ) Rn (ltlc_to_ltln' False ψ)"
| "ltlc_to_ltln' False (φ Wc ψ) = (ltlc_to_ltln' False φ) Wn (ltlc_to_ltln' False ψ)"
| "ltlc_to_ltln' False (φ Mc ψ) = (ltlc_to_ltln' False φ) Mn (ltlc_to_ltln' False ψ)"
| "ltlc_to_ltln' True truec = falsen"
| "ltlc_to_ltln' True falsec = truen"
| "ltlc_to_ltln' True propc(q) = npropn(q)"
| "ltlc_to_ltln' True (φ andc ψ) = (ltlc_to_ltln' True φ) orn (ltlc_to_ltln' True ψ)"
| "ltlc_to_ltln' True (φ orc ψ) = (ltlc_to_ltln' True φ) andn (ltlc_to_ltln' True ψ)"
| "ltlc_to_ltln' True (φ impliesc ψ) = (ltlc_to_ltln' False φ) andn (ltlc_to_ltln' True ψ)"
| "ltlc_to_ltln' True (Fc φ) = falsen Rn (ltlc_to_ltln' True φ)"
| "ltlc_to_ltln' True (Gc φ) = truen Un (ltlc_to_ltln' True φ)"
| "ltlc_to_ltln' True (φ Uc ψ) = (ltlc_to_ltln' True φ) Rn (ltlc_to_ltln' True ψ)"
| "ltlc_to_ltln' True (φ Rc ψ) = (ltlc_to_ltln' True φ) Un (ltlc_to_ltln' True ψ)"
| "ltlc_to_ltln' True (φ Wc ψ) = (ltlc_to_ltln' True φ) Mn (ltlc_to_ltln' True ψ)"
| "ltlc_to_ltln' True (φ Mc ψ) = (ltlc_to_ltln' True φ) Wn (ltlc_to_ltln' True ψ)"
| "ltlc_to_ltln' b (notc φ) = ltlc_to_ltln' (¬ b) φ"
| "ltlc_to_ltln' b (Xc φ) = Xn (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 truen = truec"
| "ltln_to_ltlc falsen = falsec"
| "ltln_to_ltlc propn(q) = propc(q)"
| "ltln_to_ltlc npropn(q) = notc (propc(q))"
| "ltln_to_ltlc (φ andn ψ) = (ltln_to_ltlc φ andc ltln_to_ltlc ψ)"
| "ltln_to_ltlc (φ orn ψ) = (ltln_to_ltlc φ orc ltln_to_ltlc ψ)"
| "ltln_to_ltlc (Xn φ) = (Xc ltln_to_ltlc φ)"
| "ltln_to_ltlc (φ Un ψ) = (ltln_to_ltlc φ Uc ltln_to_ltlc ψ)"
| "ltln_to_ltlc (φ Rn ψ) = (ltln_to_ltlc φ Rc ltln_to_ltlc ψ)"
| "ltln_to_ltlc (φ Wn ψ) = (ltln_to_ltlc φ Wc ltln_to_ltlc ψ)"
| "ltln_to_ltlc (φ Mn ψ) = (ltln_to_ltlc φ Mc 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 notn
where
  "notn truen = falsen"
| "notn falsen = truen"
| "notn propn(a) = npropn(a)"
| "notn npropn(a) = propn(a)"
| "notn (φ andn ψ) = (notn φ) orn (notn ψ)"
| "notn (φ orn ψ) = (notn φ) andn (notn ψ)"
| "notn (Xn φ) = Xn (notn φ)"
| "notn (φ Un ψ) = (notn φ) Rn (notn ψ)"
| "notn (φ Rn ψ) = (notn φ) Un (notn ψ)"
| "notn (φ Wn ψ) = (notn φ) Mn (notn ψ)"
| "notn (φ Mn ψ) = (notn φ) Wn (notn ψ)"

lemma notn_semantics[simp]:
  "w ⊨n notn φ ⟷ ¬ w ⊨n φ"
  by (induction φ arbitrary: w) auto

lemma notn_size:
  "size (notn φ) = size φ"
  by (induction φ) auto


subsubsection ‹Subformulas›

fun subfrmlsn :: "'a ltln ⇒ 'a ltln set"
where
  "subfrmlsn (φ andn ψ) = {φ andn ψ} ∪ subfrmlsn φ ∪ subfrmlsn ψ"
| "subfrmlsn (φ orn ψ) = {φ orn ψ} ∪ subfrmlsn φ ∪ subfrmlsn ψ"
| "subfrmlsn (Xn φ) = {Xn φ} ∪ subfrmlsn φ"
| "subfrmlsn (φ Un ψ) = {φ Un ψ} ∪ subfrmlsn φ ∪ subfrmlsn ψ"
| "subfrmlsn (φ Rn ψ) = {φ Rn ψ} ∪ subfrmlsn φ ∪ subfrmlsn ψ"
| "subfrmlsn (φ Wn ψ) = {φ Wn ψ} ∪ subfrmlsn φ ∪ subfrmlsn ψ"
| "subfrmlsn (φ Mn ψ) = {φ Mn ψ} ∪ 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 φ Un truen"
  "¬ (w ⊨n φ Un falsen)"
  "(w ⊨n falsen Un φ) = (w ⊨n φ)"
  by force+

lemma R_consts[intro, simp]:
  "w ⊨n φ Rn truen"
  "¬ (w ⊨n φ Rn falsen)"
  "(w ⊨n truen Rn φ) = (w ⊨n φ)"
  by force+

lemma W_consts[intro, simp]:
  "w ⊨n truen Wn φ"
  "w ⊨n φ Wn truen"
  "(w ⊨n falsen Wn φ) = (w ⊨n φ)"
  "(w ⊨n φ Wn falsen) = (w ⊨n Gn φ)"
  by force+

lemma M_consts[intro, simp]:
  "¬ (w ⊨n falsen Mn φ)"
  "¬ (w ⊨n φ Mn falsen)"
  "(w ⊨n truen Mn φ) = (w ⊨n φ)"
  "(w ⊨n φ Mn truen) = (w ⊨n Fn φ)"
  by force+


subsubsection ‹Distributivity›

lemma until_and_left_distrib:
  "w ⊨n (φ1 andn φ2) Un ψ ⟷ w ⊨n (φ1 Un ψ) andn (φ2 Un ψ)"
proof
  assume "w ⊨n φ1 Un ψ andn φ2 Un ψ"

  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 andn φ2)"
    by (simp add: min_def)

  then show "w ⊨n (φ1 andn φ2) Un ψ"
    by force
qed auto

lemma until_or_right_distrib:
  "w ⊨n φ Un (ψ1 orn ψ2) ⟷ w ⊨n (φ Un ψ1) orn (φ Un ψ2)"
  by auto

lemma release_and_right_distrib:
  "w ⊨n φ Rn (ψ1 andn ψ2) ⟷ w ⊨n (φ Rn ψ1) andn (φ Rn ψ2)"
  by auto

lemma release_or_left_distrib:
  "w ⊨n (φ1 orn φ2) Rn ψ ⟷ w ⊨n (φ1 Rn ψ) orn (φ2 Rn ψ)"
  by (metis notn.simps(6) notn.simps(9) notn_semantics until_and_left_distrib)

lemma strong_release_and_right_distrib:
  "w ⊨n φ Mn (ψ1 andn ψ2) ⟷ w ⊨n (φ Mn ψ1) andn (φ Mn ψ2)"
proof
  assume "w ⊨n (φ Mn ψ1) andn (φ Mn ψ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 andn ψ2)"
    by (simp add: min_def)

  then show "w ⊨n φ Mn (ψ1 andn ψ2)"
    by force
qed auto

lemma strong_release_or_left_distrib:
  "w ⊨n (φ1 orn φ2) Mn ψ ⟷ w ⊨n (φ1 Mn ψ) orn (φ2 Mn ψ)"
  by auto

lemma weak_until_and_left_distrib:
  "w ⊨n (φ1 andn φ2) Wn ψ ⟷ w ⊨n (φ1 Wn ψ) andn (φ2 Wn ψ)"
  by auto

lemma weak_until_or_right_distrib:
  "w ⊨n φ Wn (ψ1 orn ψ2) ⟷ w ⊨n (φ Wn ψ1) orn (φ Wn ψ2)"
  by (metis notn.simps(10) notn.simps(6) notn_semantics strong_release_and_right_distrib)


lemma next_until_distrib:
  "w ⊨n Xn (φ Un ψ) ⟷ w ⊨n (Xn φ) Un (Xn ψ)"
  by auto

lemma next_release_distrib:
  "w ⊨n Xn (φ Rn ψ) ⟷ w ⊨n (Xn φ) Rn (Xn ψ)"
  by auto

lemma next_weak_until_distrib:
  "w ⊨n Xn (φ Wn ψ) ⟷ w ⊨n (Xn φ) Wn (Xn ψ)"
  by auto

lemma next_strong_release_distrib:
  "w ⊨n Xn (φ Mn ψ) ⟷ w ⊨n (Xn φ) Mn (Xn ψ)"
  by auto


subsubsection ‹Nested operators›

lemma finally_until[simp]:
  "w ⊨n Fn (φ Un ψ) ⟷ w ⊨n Fn ψ"
  by auto force

lemma globally_release[simp]:
  "w ⊨n Gn (φ Rn ψ) ⟷ w ⊨n Gn ψ"
  by auto force

lemma globally_weak_until[simp]:
  "w ⊨n Gn (φ Wn ψ) ⟷ w ⊨n Gn (φ orn ψ)"
  by auto force

lemma finally_strong_release[simp]:
  "w ⊨n Fn (φ Mn ψ) ⟷ w ⊨n Fn (φ andn ψ)"
  by auto force


subsubsection ‹Weak and strong operators›

lemma ltln_weak_strong:
  "w ⊨n φ Wn ψ ⟷ w ⊨n (Gn φ) orn (φ Un ψ)"
  "w ⊨n φ Rn ψ ⟷ w ⊨n (Gn ψ) orn (φ Mn ψ)"
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 φ Un ψ ⟷ w ⊨n (Fn ψ) andn (φ Wn ψ)"
  "w ⊨n φ Mn ψ ⟷ w ⊨n (Fn φ) andn (φ Rn ψ)"
  by (metis ltln_weak_strong notn.simps(1,5,8-11) notn_semantics)+

lemma ltln_strong_to_weak:
  "w ⊨n φ Un ψ ⟹ w ⊨n φ Wn ψ"
  "w ⊨n φ Mn ψ ⟹ w ⊨n φ Rn ψ"
  using ltln_weak_strong by simp_all blast+

lemma ltln_weak_to_strong:
  "⟦w ⊨n φ Wn ψ; ¬ w ⊨n Gn φ⟧ ⟹ w ⊨n φ Un ψ"
  "⟦w ⊨n φ Wn ψ; w ⊨n Fn ψ⟧ ⟹ w ⊨n φ Un ψ"
  "⟦w ⊨n φ Rn ψ; ¬ w ⊨n Gn ψ⟧ ⟹ w ⊨n φ Mn ψ"
  "⟦w ⊨n φ Rn ψ; w ⊨n Fn φ⟧ ⟹ w ⊨n φ Mn ψ"
  unfolding ltln_weak_strong[of w φ ψ] by auto


lemma ltln_StrongRelease_to_Until:
  "w ⊨n φ Mn ψ ⟷ w ⊨n ψ Un (φ andn ψ)"
  using order.order_iff_strict by auto

lemma ltln_Release_to_WeakUntil:
  "w ⊨n φ Rn ψ ⟷ w ⊨n ψ Wn (φ andn ψ)"
  by (meson ltln_StrongRelease_to_Until ltln_weak_strong semantics_ltln.simps(6))

lemma ltln_WeakUntil_to_Release:
  "w ⊨n φ Wn ψ ⟷ w ⊨n ψ Rn (φ orn ψ)"
  by (metis ltln_StrongRelease_to_Until notn.simps(6,9,10) notn_semantics)

lemma ltln_Until_to_StrongRelease:
  "w ⊨n φ Un ψ ⟷ w ⊨n ψ Mn (φ orn ψ)"
  by (metis ltln_Release_to_WeakUntil notn.simps(6,8,11) notn_semantics)


subsubsection ‹GF and FG semantics›

lemma GF_suffix:
  "suffix i w ⊨n Gn (Fn ψ) ⟷ w ⊨n Gn (Fn ψ)"
  by auto (metis ab_semigroup_add_class.add_ac(1) add.left_commute)

lemma FG_suffix:
  "suffix i w ⊨n Fn (Gn ψ) ⟷ w ⊨n Fn (Gn ψ)"
  by (auto simp: algebra_simps) (metis add.commute add.left_commute)

lemma GF_Inf_many:
  "w ⊨n Gn (Fn φ) ⟷ (∃∞ 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 Fn (Gn φ) ⟷ (∀∞ 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 ?? *)
lemma MOST_nat_add:
  "(∀∞i::nat. P i) ⟷ (∀∞i. P (i + j))"
  by (simp add: cofinite_eq_sequentially)

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


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

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

  with suffix obtain j where "j ≥ i" and j_suffix: "suffix j w ⊨n ψ"
    by simp (blast intro: le_add1)

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

  show "suffix i w ⊨n Gn (Fn ψ)"
  proof (cases "w ⊨n Gn (Fn ψ)")
    case False
    then have "¬ (∃∞i. suffix i w ⊨n ψ)"
      unfolding GF_Inf_many by simp
    then have "finite {i. suffix i w ⊨n ψ}"
      by (simp add: INFM_iff_infinite)
    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 Fn (Gn ψ) ⟷ suffix i w ⊨n Gn ψ"
  unfolding MOST_nat
proof standard+
  fix i :: nat
  assume "suffix i w ⊨n Gn ψ"
  then show "suffix i w ⊨n Fn (Gn ψ)"
    unfolding FG_Alm_all INFM_nat by fastforce
next
  fix i :: nat
  assume suffix: "suffix i w ⊨n Fn (Gn ψ)"
  assume max: "i > Max {i. ¬ suffix i w ⊨n Gn ψ}"

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

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


subsubsection ‹Expansion›

lemma ltln_expand_Until:
  "ξ ⊨n φ Un ψ ⟷ (ξ ⊨n ψ orn (φ andn (Xn (φ Un ψ))))"
  (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 Xn (φ Un ψ)"
      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 φ Rn ψ ⟷ (ξ ⊨n ψ andn (φ orn (Xn (φ Rn ψ))))"
  (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 φ Wn ψ ⟷ (ξ ⊨n ψ orn (φ andn (Xn (φ Wn ψ))))"
  (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 φ Mn ψ ⟷ (ξ ⊨n ψ andn (φ orn (Xn (φ Mn ψ))))"
  (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 notn.simps(5,6,7,11) notn_semantics)
  qed
qed

lemma ltln_Release_alterdef:
  "w ⊨n φ Rn ψ ⟷ w ⊨n (Gn ψ) orn (ψ Un (φ andn ψ))"
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                               ("truer")
  | False_ltlr                              ("falser")
  | Prop_ltlr 'a                            ("propr'(_')")
  | Nprop_ltlr 'a                           ("npropr'(_')")
  | And_ltlr "'a ltlr" "'a ltlr"            ("_ andr _" [82,82] 81)
  | Or_ltlr "'a ltlr" "'a ltlr"             ("_ orr _" [84,84] 83)
  | Next_ltlr "'a ltlr"                     ("Xr _" [88] 87)
  | Until_ltlr "'a ltlr" "'a ltlr"          ("_ Ur _" [84,84] 83)
  | Release_ltlr "'a ltlr" "'a ltlr"        ("_ Rr _" [84,84] 83)


subsubsection ‹Semantics›

primrec semantics_ltlr :: "['a set word, 'a ltlr] ⇒ bool" ("_ ⊨r _" [80,80] 80)
where
  "ξ ⊨r truer = True"
| "ξ ⊨r falser = False"
| "ξ ⊨r propr(q) = (q ∈ ξ 0)"
| "ξ ⊨r npropr(q) = (q ∉ ξ 0)"
| "ξ ⊨r φ andr ψ = (ξ ⊨r φ ∧ ξ ⊨r ψ)"
| "ξ ⊨r φ orr ψ = (ξ ⊨r φ ∨ ξ ⊨r ψ)"
| "ξ ⊨r Xr φ = (suffix 1 ξ ⊨r φ)"
| "ξ ⊨r φ Ur ψ = (∃i. suffix i ξ ⊨r ψ ∧ (∀j<i. suffix j ξ ⊨r φ))"
| "ξ ⊨r φ Rr ψ = (∀i. suffix i ξ ⊨r ψ ∨ (∃j<i. suffix j ξ ⊨r φ))"


subsubsection ‹Conversion›

fun ltln_to_ltlr :: "'a ltln ⇒ 'a ltlr"
where
  "ltln_to_ltlr truen = truer"
| "ltln_to_ltlr falsen = falser"
| "ltln_to_ltlr propn(a) = propr(a)"
| "ltln_to_ltlr npropn(a) = npropr(a)"
| "ltln_to_ltlr (φ andn ψ) = (ltln_to_ltlr φ) andr (ltln_to_ltlr ψ)"
| "ltln_to_ltlr (φ orn ψ) = (ltln_to_ltlr φ) orr (ltln_to_ltlr ψ)"
| "ltln_to_ltlr (Xn φ) = Xr (ltln_to_ltlr φ)"
| "ltln_to_ltlr (φ Un ψ) = (ltln_to_ltlr φ) Ur (ltln_to_ltlr ψ)"
| "ltln_to_ltlr (φ Rn ψ) = (ltln_to_ltlr φ) Rr (ltln_to_ltlr ψ)"
| "ltln_to_ltlr (φ Wn ψ) = (ltln_to_ltlr ψ) Rr ((ltln_to_ltlr φ) orr (ltln_to_ltlr ψ))"
| "ltln_to_ltlr (φ Mn ψ) = (ltln_to_ltlr ψ) Ur ((ltln_to_ltlr φ) andr (ltln_to_ltlr ψ))"

fun ltlr_to_ltln :: "'a ltlr ⇒ 'a ltln"
where
  "ltlr_to_ltln truer = truen"
| "ltlr_to_ltln falser = falsen"
| "ltlr_to_ltln propr(a) = propn(a)"
| "ltlr_to_ltln npropr(a) = npropn(a)"
| "ltlr_to_ltln (φ andr ψ) = (ltlr_to_ltln φ) andn (ltlr_to_ltln ψ)"
| "ltlr_to_ltln (φ orr ψ) = (ltlr_to_ltln φ) orn (ltlr_to_ltln ψ)"
| "ltlr_to_ltln (Xr φ) = Xn (ltlr_to_ltln φ)"
| "ltlr_to_ltln (φ Ur ψ) = (ltlr_to_ltln φ) Un (ltlr_to_ltln ψ)"
| "ltlr_to_ltln (φ Rr ψ) = (ltlr_to_ltln φ) Rn (ltlr_to_ltln ψ)"

lemma ltln_to_ltlr_semantics:
  "w ⊨r ltln_to_ltlr φ ⟷ w ⊨n φ"
  by (induction φ arbitrary: w) (unfold ltln_WeakUntil_to_Release ltln_StrongRelease_to_Until, simp_all)

lemma ltlr_to_ltln_semantics:
  "w ⊨n ltlr_to_ltln φ ⟷ w ⊨r φ"
  by (induction φ arbitrary: w) simp_all


subsubsection ‹Negation›

fun notr
where
  "notr truer = falser"
| "notr falser = truer"
| "notr propr(a) = npropr(a)"
| "notr npropr(a) = propr(a)"
| "notr (φ andr ψ) = (notr φ) orr (notr ψ)"
| "notr (φ orr ψ) = (notr φ) andr (notr ψ)"
| "notr (Xr φ) = Xr (notr φ)"
| "notr (φ Ur ψ) = (notr φ) Rr (notr ψ)"
| "notr (φ Rr ψ) = (notr φ) Ur (notr ψ)"

lemma notr_semantics [simp]:
  "w ⊨r notr φ ⟷ ¬ w ⊨r φ"
  by (induction φ arbitrary: w) auto


subsubsection ‹Subformulas›

fun subfrmlsr :: "'a ltlr ⇒ 'a ltlr set"
where
  "subfrmlsr (φ andr ψ) = {φ andr ψ} ∪ subfrmlsr φ ∪ subfrmlsr ψ"
| "subfrmlsr (φ orr ψ) = {φ orr ψ} ∪ subfrmlsr φ ∪ subfrmlsr ψ"
| "subfrmlsr (φ Ur ψ) = {φ Ur ψ} ∪ subfrmlsr φ ∪ subfrmlsr ψ"
| "subfrmlsr (φ Rr ψ) = {φ Rr ψ} ∪ subfrmlsr φ ∪ subfrmlsr ψ"
| "subfrmlsr (Xr φ) = {Xr φ} ∪ subfrmlsr φ"
| "subfrmlsr x = {x}"

lemma subfrmlsr_id[simp]:
  "φ ∈ subfrmlsr φ"
  by (induction φ) auto

lemma subfrmlsr_finite:
  "finite (subfrmlsr φ)"
  by (induction φ) auto

lemma subfrmlsr_subset:
  "ψ ∈ subfrmlsr φ ⟹ subfrmlsr ψ ⊆ subfrmlsr φ"
  by (induction φ) auto

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


subsubsection ‹Expansion lemmas›

lemma ltlr_expand_Until:
  "ξ ⊨r φ Ur ψ ⟷ (ξ ⊨r ψ orr (φ andr (Xr (φ Ur ψ))))"
  by (metis ltln_expand_Until ltlr_to_ltln.simps(5-8) ltlr_to_ltln_semantics)

lemma ltlr_expand_Release:
  "ξ ⊨r φ Rr ψ ⟷ (ξ ⊨r ψ andr (φ orr (Xr (φ Rr ψ))))"
  by (metis ltln_expand_Release ltlr_to_ltln.simps(5-7,9) ltlr_to_ltln_semantics)




subsection ‹Propositional LTL›

text ‹We define the syntax and semantics of propositional linear-time
    temporal logic PLTL.
    PLTL formulas are built from atomic formulas, propositional connectives,
    and the temporal operators ``next'' and ``until''. The following data
    type definition is parameterized by the type of states over which
    formulas are evaluated.›

subsubsection ‹Syntax›

datatype 'a pltl  =
    False_ltlp                       ("falsep")
  | Atom_ltlp "'a ⇒ bool"           ("atomp'(_')")
  | Implies_ltlp "'a pltl" "'a pltl" ("_ impliesp _" [81,81] 80)
  | Next_ltlp "'a pltl"              ("Xp _" [88] 87)
  | Until_ltlp "'a pltl" "'a pltl"   ("_ Up _" [84,84] 83)

― ‹Further connectives of PLTL can be defined in terms of the existing syntax.›

definition Not_ltlp ("notp _" [85] 85)
where
  "notp φ ≡ φ impliesp falsep"

definition True_ltlp ("truep")
where
  "truep ≡ notp falsep"

definition Or_ltlp ("_ orp _" [81,81] 80)
where
  "φ orp ψ ≡ (notp φ) impliesp ψ"

definition And_ltlp ("_ andp _" [82,82] 81)
where
  "φ andp ψ ≡ notp ((notp φ) orp (notp ψ))"

definition Eventually_ltlp ("Fp _" [88] 87)
where
  "Fp φ ≡ truep Up φ"

definition Always_ltlp ("Gp _" [88] 87)
where
  "Gp φ ≡ notp (Fp (notp φ))"

definition Release_ltlp ("_ Rp _" [84,84] 83)
where
  "φ Rp ψ ≡ notp ((notp φ) Up (notp ψ))"

definition WeakUntil_ltlp ("_ Wp _" [84,84] 83)
where
  "φ Wp ψ ≡ ψ Rp (φ orp ψ)"

definition StrongRelease_ltlp ("_ Mp _" [84,84] 83)
where
  "φ Mp ψ ≡ ψ Up (φ andp ψ)"


subsubsection ‹Semantics›

fun semantics_pltl :: "['a word, 'a pltl] ⇒ bool" ("_ ⊨p _" [80,80] 80)
where
  "w ⊨p falsep = False"
| "w ⊨p atomp(p) = (p (w 0))"
| "w ⊨p φ impliesp ψ = (w ⊨p φ ⟶ w ⊨p ψ)"
| "w ⊨p Xp φ = (suffix 1 w ⊨p φ)"
| "w ⊨p φ Up ψ = (∃i. suffix i w ⊨p ψ ∧ (∀j<i. suffix j w ⊨p φ))"

lemma semantics_pltl_sugar [simp]:
  "w ⊨p notp φ = (¬w ⊨p φ)"
  "w ⊨p truep = True"
  "w ⊨p φ orp ψ = (w ⊨p φ ∨ w ⊨p ψ)"
  "w ⊨p φ andp ψ = (w ⊨p φ ∧ w ⊨p ψ)"
  "w ⊨p Fp φ = (∃i. suffix i w ⊨p φ)"
  "w ⊨p Gp φ = (∀i. suffix i w ⊨p φ)"
  "w ⊨p φ Rp ψ = (∀i. suffix i w ⊨p ψ ∨ (∃j<i. suffix j w ⊨p φ))"
  "w ⊨p φ Wp ψ = (∀i. suffix i w ⊨p φ ∨ (∃j≤i. suffix j w ⊨p ψ))"
  "w ⊨p φ Mp ψ = (∃i. suffix i w ⊨p φ ∧ (∀j≤i. suffix j w ⊨p ψ))"
  by (auto simp: Not_ltlp_def True_ltlp_def Or_ltlp_def And_ltlp_def Eventually_ltlp_def Always_ltlp_def Release_ltlp_def WeakUntil_ltlp_def StrongRelease_ltlp_def) (insert le_neq_implies_less, blast)+

definition "language_ltlp φ ≡ {ξ. ξ ⊨p φ}"


subsubsection ‹Conversion›

fun ltlc_to_pltl :: "'a ltlc ⇒ 'a set pltl"
where
  "ltlc_to_pltl truec = truep"
| "ltlc_to_pltl falsec = falsep"
| "ltlc_to_pltl (propc(q)) = atomp((∈) q)"
| "ltlc_to_pltl (notc φ) = notp (ltlc_to_pltl φ)"
| "ltlc_to_pltl (φ andc ψ) = (ltlc_to_pltl φ) andp (ltlc_to_pltl ψ)"
| "ltlc_to_pltl (φ orc ψ) = (ltlc_to_pltl φ) orp (ltlc_to_pltl ψ)"
| "ltlc_to_pltl (φ impliesc ψ) = (ltlc_to_pltl φ) impliesp (ltlc_to_pltl ψ)"
| "ltlc_to_pltl (Xc φ) = Xp (ltlc_to_pltl φ)"
| "ltlc_to_pltl (Fc φ) = Fp (ltlc_to_pltl φ)"
| "ltlc_to_pltl (Gc φ) = Gp (ltlc_to_pltl φ)"
| "ltlc_to_pltl (φ Uc ψ) = (ltlc_to_pltl φ) Up (ltlc_to_pltl ψ)"
| "ltlc_to_pltl (φ Rc ψ) = (ltlc_to_pltl φ) Rp (ltlc_to_pltl ψ)"
| "ltlc_to_pltl (φ Wc ψ) = (ltlc_to_pltl φ) Wp (ltlc_to_pltl ψ)"
| "ltlc_to_pltl (φ Mc ψ) = (ltlc_to_pltl φ) Mp (ltlc_to_pltl ψ)"

lemma ltlc_to_pltl_semantics [simp]:
  "w ⊨p (ltlc_to_pltl φ) ⟷ w ⊨c φ"
  by (induction φ arbitrary: w) simp_all


subsubsection ‹Atoms›

fun atoms_pltl :: "'a pltl ⇒ ('a ⇒ bool) set"
where
  "atoms_pltl falsep = {}"
| "atoms_pltl atomp(p) = {p}"
| "atoms_pltl (φ impliesp ψ) = atoms_pltl φ ∪ atoms_pltl ψ"
| "atoms_pltl (Xp φ) = atoms_pltl φ"
| "atoms_pltl (φ Up ψ) = atoms_pltl φ ∪ atoms_pltl ψ"

lemma atoms_finite [iff]:
  "finite (atoms_pltl φ)"
  by (induct φ) auto

lemma atoms_pltl_sugar [simp]:
  "atoms_pltl (notp φ) = atoms_pltl φ"
  "atoms_pltl truep = {}"
  "atoms_pltl (φ orp ψ) = atoms_pltl φ ∪ atoms_pltl ψ"
  "atoms_pltl (φ andp ψ) = atoms_pltl φ ∪ atoms_pltl ψ"
  "atoms_pltl (Fp φ) = atoms_pltl φ"
  "atoms_pltl (Gp φ) = atoms_pltl φ"
  by (auto simp: Not_ltlp_def True_ltlp_def Or_ltlp_def And_ltlp_def Eventually_ltlp_def Always_ltlp_def)

end