Quelle  LTL.thy

(*
    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                               (‹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 φ)"
  by (auto simp add: Iff_ltlc_def)

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')"
  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) ⊨<sub>c</sub> 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 ⊨<sub>c</sub> φ = 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 = inj_on_subset[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) ⊨<sub>c</sub> 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 (φ₁ and_n φ₂) U_n ψ ⟷ w ⊨_n (φ₁ U_n ψ) and_n (φ₂ U_n ψ)"
proof
  assume "w ⊨_n φ₁ U_n ψ and_n φ₂ U_n ψ"

  then obtain i1 i2 where "suffix i1 w ⊨_n ψ ∧ (∀j<i1. suffix j w ⊨_n φ₁)" and "suffix i2 w ⊨_n ψ ∧ (∀j<i2. suffix j w ⊨_n φ₂)"
    by auto

  then have "suffix (min i1 i2) w ⊨_n ψ ∧ (∀j<min i1 i2. suffix j w ⊨_n φ₁ and_n φ₂)"
    by (simp add: min_def)

  then show "w ⊨_n (φ₁ and_n φ₂) U_n ψ"
    by force
qed auto

lemma until_or_right_distrib:
  "w ⊨_n φ U_n (ψ₁ or_n ψ₂) ⟷ w ⊨_n (φ U_n ψ₁) or_n (φ U_n ψ₂)"
  by auto

lemma release_and_right_distrib:
  "w ⊨_n φ R_n (ψ₁ and_n ψ₂) ⟷ w ⊨_n (φ R_n ψ₁) and_n (φ R_n ψ₂)"
  by auto

lemma release_or_left_distrib:
  "w ⊨_n (φ₁ or_n φ₂) R_n ψ ⟷ w ⊨_n (φ₁ R_n ψ) or_n (φ₂ 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 (ψ₁ and_n ψ₂) ⟷ w ⊨_n (φ M_n ψ₁) and_n (φ M_n ψ₂)"
proof
  assume "w ⊨_n (φ M_n ψ₁) and_n (φ M_n ψ₂)"

  then obtain i1 i2 where "suffix i1 w ⊨_n φ ∧ (∀j≤i1. suffix j w ⊨_n ψ₁)" and "suffix i2 w ⊨_n φ ∧ (∀j≤i2. suffix j w ⊨_n ψ₂)"
    by auto

  then have "suffix (min i1 i2) w ⊨_n φ ∧ (∀j≤min i1 i2. suffix j w ⊨_n ψ₁ and_n ψ₂)"
    by (simp add: min_def)

  then show "w ⊨_n φ M_n (ψ₁ and_n ψ₂)"
    by force
qed auto

lemma strong_release_or_left_distrib:
  "w ⊨_n (φ₁ or_n φ₂) M_n ψ ⟷ w ⊨_n (φ₁ M_n ψ) or_n (φ₂ M_n ψ)"
  by auto

lemma weak_until_and_left_distrib:
  "w ⊨_n (φ₁ and_n φ₂) W_n ψ ⟷ w ⊨_n (φ₁ W_n ψ) and_n (φ₂ W_n ψ)"
  by auto

lemma weak_until_or_right_distrib:
  "w ⊨_n φ W_n (ψ₁ or_n ψ₂) ⟷ w ⊨_n (φ W_n ψ₁) or_n (φ W_n ψ₂)"
  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 ψ)"
  by auto (metis ab_semigroup_add_class.add_ac(1) add.left_commute)

lemma FG_suffix:
  "suffix i w ⊨_n F_n (G_n ψ) ⟷ w ⊨_n F_n (G_n ψ)"
  by (auto simp: algebra_simps) (metis add.commute add.left_commute)

lemma GF_Inf_many:
  "w ⊨_n G_n (F_n φ) ⟷ (∃_\<infinity> 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 φ) ⟷ (∀_\<infinity> 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:
  "(∀_\<infinity>i::nat. P i) ⟷ (∀_\<infinity>i. P (i + j))"
  by (simp add: cofinite_eq_sequentially)

lemma INFM_nat_add:
  "(∃_\<infinity>i::nat. P i) ⟷ (∃_\<infinity>i. P (i + j))"
  using MOST_nat_add not_MOST not_INFM by blast


lemma FG_suffix_G:
  "w ⊨_n F_n (G_n φ) ==> ∀_\<infinity>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 "∀_\<infinity>i. suffix i w ⊨_n G_n φ"
    unfolding FG_Alm_all .
qed

lemma Alm_all_GF_F:
  "∀_\<infinity>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 ψ"
    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 G_n (F_n ψ)"
  proof (cases "w ⊨_n G_n (F_n ψ)")
    case False
    then have "¬ (∃_\<infinity>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:
  "∀_\<infinity>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 "∀_\<infinity>j. suffix (i + j) w ⊨_n G_n ψ"
    using FG_suffix_G[of "suffix i w"] suffix_suffix
    by fastforce
  then have "¬ (∃_\<infinity>j. ¬ suffix j w ⊨_n G_n ψ)"
    using MOST_nat_add[of "λi. suffix i w ⊨_n G_n ψ" i]
    by (simp add: algebra_simps)
  then have "finite {i. ¬ suffix i w ⊨_n G_n ψ}"
    by (simp add: INFM_iff_infinite)

  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 ψ)"
| "ltlr_to_ltln (X_r φ) = X_n (ltlr_to_ltln φ)"
| "ltlr_to_ltln (φ U_r ψ) = (ltlr_to_ltln φ) U_n (ltlr_to_ltln ψ)"
| "ltlr_to_ltln (φ R_r ψ) = (ltlr_to_ltln φ) R_n (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 not_r
where
  "not_r true_r = false_r"
| "not_r false_r = true_r"
| "not_r prop_r(a) = nprop_r(a)"
| "not_r nprop_r(a) = prop_r(a)"
| "not_r (φ and_r ψ) = (not_r φ) or_r (not_r ψ)"
| "not_r (φ or_r ψ) = (not_r φ) and_r (not_r ψ)"
| "not_r (X_r φ) = X_r (not_r φ)"
| "not_r (φ U_r ψ) = (not_r φ) R_r (not_r ψ)"
| "not_r (φ R_r ψ) = (not_r φ) U_r (not_r ψ)"

lemma not_{r_semantics} [simp]:
  "w ⊨_r not_r φ ⟷ ¬ w ⊨_r φ"
  by (induction φ arbitrary: w) auto


subsubsection ‹Subformulas›

fun subfrmlsr :: "'a ltlr ==> 'a ltlr set"
where
  "subfrmlsr (φ and_r ψ) = {φ and_r ψ} ∪ subfrmlsr φ ∪ subfrmlsr ψ"
| "subfrmlsr (φ or_r ψ) = {φ or_r ψ} ∪ subfrmlsr φ ∪ subfrmlsr ψ"
| "subfrmlsr (φ U_r ψ) = {φ U_r ψ} ∪ subfrmlsr φ ∪ subfrmlsr ψ"
| "subfrmlsr (φ R_r ψ) = {φ R_r ψ} ∪ subfrmlsr φ ∪ subfrmlsr ψ"
| "subfrmlsr (X_r φ) = {X_r φ} ∪ 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 φ U_r ψ ⟷ (ξ ⊨_r ψ or_r (φ and_r (X_r (φ U_r ψ))))"
  by (metis ltln_expand_Until ltlr_to_ltln.simps(5-8) ltlr_to_ltln_semantics)

lemma ltlr_expand_Release:
  "ξ ⊨_r φ R_r ψ ⟷ (ξ ⊨_r ψ and_r (φ or_r (X_r (φ R_r ψ))))"
  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                       (‹false_p›)
  | Atom_ltlp "'a ==> bool"           (‹atom_p'(_')›)
  | Implies_ltlp "'a pltl" "'a pltl" (‹_ implies_p _› [81,81] 80)
  | Next_ltlp "'a pltl"              (‹X_p _› [88] 87)
  | Until_ltlp "'a pltl" "'a pltl"   (‹_ U_p _› [84,84] 83)

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

definition Not_ltlp (‹not_p _› [85] 85)
where
  "not_p φ ≡ φ implies_p false_p"

definition True_ltlp (‹true_p›)
where
  "true_p ≡ not_p false_p"

definition Or_ltlp (‹_ or_p _› [81,81] 80)
where
  "φ or_p ψ ≡ (not_p φ) implies_p ψ"

definition And_ltlp (‹_ and_p _› [82,82] 81)
where
  "φ and_p ψ ≡ not_p ((not_p φ) or_p (not_p ψ))"

definition Eventually_ltlp (‹F_p _› [88] 87)
where
  "F_p φ ≡ true_p U_p φ"

definition Always_ltlp (‹G_p _› [88] 87)
where
  "G_p φ ≡ not_p (F_p (not_p φ))"

definition Release_ltlp (‹_ R_p _› [84,84] 83)
where
  "φ R_p ψ ≡ not_p ((not_p φ) U_p (not_p ψ))"

definition WeakUntil_ltlp (‹_ W_p _› [84,84] 83)
where
  "φ W_p ψ ≡ ψ R_p (φ or_p ψ)"

definition StrongRelease_ltlp (‹_ M_p _› [84,84] 83)
where
  "φ M_p ψ ≡ ψ U_p (φ and_p ψ)"


subsubsection ‹Semantics›

fun semantics_pltl :: "['a word, 'a pltl] ==> bool" (‹_ ⊨_p _› [80,80] 80)
where
  "w ⊨_p false_p = False"
| "w ⊨_p atom_p(p) = (p (w 0))"
| "w ⊨_p φ implies_p ψ = (w ⊨_p φ ⟶ w ⊨_p ψ)"
| "w ⊨_p X_p φ = (suffix 1 w ⊨_p φ)"
| "w ⊨_p φ U_p ψ = (∃i. suffix i w ⊨_p ψ ∧ (∀j<i. suffix j w ⊨_p φ))"

lemma semantics_pltl_sugar [simp]:
  "w ⊨_p not_p φ = (¬w ⊨_p φ)"
  "w ⊨_p true_p = True"
  "w ⊨_p φ or_p ψ = (w ⊨_p φ ∨ w ⊨_p ψ)"
  "w ⊨_p φ and_p ψ = (w ⊨_p φ ∧ w ⊨_p ψ)"
  "w ⊨_p F_p φ = (∃i. suffix i w ⊨_p φ)"
  "w ⊨_p G_p φ = (∀i. suffix i w ⊨_p φ)"
  "w ⊨_p φ R_p ψ = (∀i. suffix i w ⊨_p ψ ∨ (∃j<i. suffix j w ⊨_p φ))"
  "w ⊨_p φ W_p ψ = (∀i. suffix i w ⊨_p φ ∨ (∃j≤i. suffix j w ⊨_p ψ))"
  "w ⊨_p φ M_p ψ = (∃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 true_c = true_p"
| "ltlc_to_pltl false_c = false_p"
| "ltlc_to_pltl (prop_c(q)) = atom_p((∈) q)"
| "ltlc_to_pltl (not_c φ) = not_p (ltlc_to_pltl φ)"
| "ltlc_to_pltl (φ and_c ψ) = (ltlc_to_pltl φ) and_p (ltlc_to_pltl ψ)"
| "ltlc_to_pltl (φ or_c ψ) = (ltlc_to_pltl φ) or_p (ltlc_to_pltl ψ)"
| "ltlc_to_pltl (φ implies_c ψ) = (ltlc_to_pltl φ) implies_p (ltlc_to_pltl ψ)"
| "ltlc_to_pltl (X_c φ) = X_p (ltlc_to_pltl φ)"
| "ltlc_to_pltl (F_c φ) = F_p (ltlc_to_pltl φ)"
| "ltlc_to_pltl (G_c φ) = G_p (ltlc_to_pltl φ)"
| "ltlc_to_pltl (φ U_c ψ) = (ltlc_to_pltl φ) U_p (ltlc_to_pltl ψ)"
| "ltlc_to_pltl (φ R_c ψ) = (ltlc_to_pltl φ) R_p (ltlc_to_pltl ψ)"
| "ltlc_to_pltl (φ W_c ψ) = (ltlc_to_pltl φ) W_p (ltlc_to_pltl ψ)"
| "ltlc_to_pltl (φ M_c ψ) = (ltlc_to_pltl φ) M_p (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 false_p = {}"
| "atoms_pltl atom_p(p) = {p}"
| "atoms_pltl (φ implies_p ψ) = atoms_pltl φ ∪ atoms_pltl ψ"
| "atoms_pltl (X_p φ) = atoms_pltl φ"
| "atoms_pltl (φ U_p ψ) = atoms_pltl φ ∪ atoms_pltl ψ"

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

lemma atoms_pltl_sugar [simp]:
  "atoms_pltl (not_p φ) = atoms_pltl φ"
  "atoms_pltl true_p = {}"
  "atoms_pltl (φ or_p ψ) = atoms_pltl φ ∪ atoms_pltl ψ"
  "atoms_pltl (φ and_p ψ) = atoms_pltl φ ∪ atoms_pltl ψ"
  "atoms_pltl (F_p φ) = atoms_pltl φ"
  "atoms_pltl (G_p φ) = atoms_pltl φ"
  by (auto simp: Not_ltlp_def True_ltlp_def Or_ltlp_def And_ltlp_def Eventually_ltlp_def Always_ltlp_def)

end