Theory LTL_FGXU

(*
    Author:      Salomon Sickert
    License:     BSD
*)

section ‹LTL (in Negation-Normal-Form, FGXU-Syntax)›

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

text ‹Inspired/Based on schimpf/LTL›

subsection ‹Syntax›

datatype (vars: 'a) ltl  =
    LTLTrue                       (‹true›)
  | LTLFalse                      (‹false›)
  | LTLProp 'a                    (‹p'(_')›)
  | LTLPropNeg 'a                 (‹np'(_')› [86] 85)
  | LTLAnd "'a ltl" "'a ltl"      (‹_ and _› [83,83] 82)
  | LTLOr "'a ltl" "'a ltl"       (‹_ or _› [82,82] 81)
  | LTLNext "'a ltl"              (‹X _› [88] 87)
  | LTLGlobal (theG: "'a ltl")    (‹G _› [85] 84)
  | LTLFinal "'a ltl"             (‹F _› [84] 83)
  | LTLUntil "'a ltl" "'a ltl"    (‹_ U _› [87,87] 86)


subsection ‹Semantics›

fun ltl_semantics :: "['a set word, 'a ltl] ⇒ bool" (infix ‹⊨› 80)
where
  "w ⊨ true = True"
| "w ⊨ false = False"
| "w ⊨ p(q) = (q ∈ w 0)"
| "w ⊨ np(q) = (q ∉ w 0)"
| "w ⊨ φ and ψ = (w ⊨ φ ∧ w ⊨ ψ)"
| "w ⊨ φ or ψ = (w ⊨ φ ∨ w ⊨ ψ)"
| "w ⊨ X φ = (suffix 1 w ⊨ φ)"
| "w ⊨ G φ = (∀k. suffix k w ⊨ φ)"
| "w ⊨ F φ = (∃k. suffix k w ⊨ φ)"
| "w ⊨ φ U ψ = (∃k. suffix k w ⊨ ψ ∧ (∀j < k. suffix j w ⊨ φ))"

fun ltl_prop_entailment :: "['a ltl set, 'a ltl] ⇒ bool" (infix ‹⊨P› 80)
where
  "𝒜 ⊨P true = True"
| "𝒜 ⊨P false = False"
| "𝒜 ⊨P φ and ψ = (𝒜 ⊨P φ ∧ 𝒜 ⊨P ψ)"
| "𝒜 ⊨P φ or ψ = (𝒜 ⊨P φ ∨ 𝒜 ⊨P ψ)"
| "𝒜 ⊨P φ = (φ ∈ 𝒜)"

subsubsection ‹Properties›

lemma LTL_G_one_step_unfolding:
  "w ⊨ G φ ⟷ (w ⊨ φ ∧ w ⊨ X (G φ))"
  (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs
  hence "w ⊨ φ"
    using suffix_0[of w] ltl_semantics.simps(8)[of w φ] by metis
  moreover
  from ‹?lhs› have "w ⊨ X (G φ)"
    by simp
  ultimately
  show ?rhs by simp
next
  assume ?rhs
  hence "w ⊨ X (G φ)" by simp
  hence "∀k. suffix (k + 1) w ⊨ φ" by force
  hence "∀k > 0. suffix k w ⊨ φ"
    by (metis Suc_eq_plus1 gr0_implies_Suc)
  moreover
  from ‹?rhs› have "(suffix 0 w) ⊨ φ" by simp
  ultimately
  show ?lhs
    using neq0_conv ltl_semantics.simps(8)[of w φ] by blast
qed

lemma LTL_F_one_step_unfolding:
  "w ⊨ F φ ⟷ (w ⊨ φ ∨ w ⊨ X (F φ))"
  (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs
  then obtain k where "suffix k w ⊨ φ" by fastforce
  thus ?rhs by (cases k) auto
next
  assume ?rhs
  thus ?lhs
    using suffix_0[of w] suffix_suffix[of _ 1 w] by (metis ltl_semantics.simps(7) ltl_semantics.simps(9))
qed

lemma LTL_U_one_step_unfolding:
  "w ⊨ φ U ψ ⟷ (w ⊨ ψ ∨ (w ⊨ φ ∧ w ⊨ X (φ U ψ)))"
  (is "?lhs ⟷ ?rhs")
proof
  assume ?lhs
  then obtain k where "suffix k w ⊨ ψ" and "∀j<k. suffix j w ⊨ φ"
    by force
  thus ?rhs
    by (cases k) auto
next
  assume ?rhs
  thus ?lhs
  proof (cases "w ⊨ ψ")
    case False
      hence "w ⊨ φ ∧ w ⊨ X (φ U ψ)"
        using ‹?rhs› by blast
      obtain k where "suffix k (suffix 1 w) ⊨ ψ" and "∀j<k. suffix j (suffix 1 w) ⊨ φ"
        using False ‹?rhs› by force
      moreover
      {
        fix j assume "j < 1 + k"
        hence "suffix j w ⊨ φ"
          using ‹w ⊨ φ ∧ w ⊨ X (φ U ψ)› ‹∀j<k. suffix j (suffix 1 w) ⊨ φ›[unfolded suffix_suffix]
          by (cases j) simp+
      }
      ultimately
      show ?thesis
        by auto
  qed force
qed

lemma LTL_GF_infinitely_many_suffixes:
  "w ⊨ G (F φ) = (∃∞i. suffix i w ⊨ φ)"
  (is "?lhs = ?rhs")
proof
  let ?S = "{i | i j. suffix (i + j) w ⊨ φ}"
  let ?S' = "{i + j | i j. suffix (i + j) w ⊨ φ}"

  assume ?lhs
  hence "infinite ?S"
    by auto
  moreover
  have "∀s ∈ ?S. ∃s' ∈ ?S'. s ≤ s'"
    by fastforce
  ultimately
  have "infinite ?S'"
    using infinite_nat_iff_unbounded_le le_trans by meson
  moreover
  have "?S' = {k | k. suffix k w ⊨ φ}"
    using monoid_add_class.add.left_neutral by metis
  ultimately
  have "infinite {k | k. suffix k w ⊨ φ}"
    by metis
  thus ?rhs unfolding Inf_many_def by force
next
  assume ?rhs
  {
    fix i
    from ‹?rhs› obtain k where "i ≤ k" and "suffix k w ⊨ φ"
      using INFM_nat_le[of "λn. suffix n w ⊨ φ"] by blast
    then obtain j where "k = i + j"
      using le_iff_add[of i k] by fast
    hence "suffix j (suffix i w) ⊨ φ"
      using ‹suffix k w ⊨ φ› suffix_suffix by fastforce
    hence "suffix i w ⊨ F φ" by auto
  }
  thus ?lhs by auto
qed

lemma LTL_FG_almost_all_suffixes:
  "w ⊨ F G φ = (∀∞i. suffix i w ⊨ φ)"
  (is "?lhs = ?rhs")
proof
  let ?S = "{k. ¬ suffix k w ⊨ φ}"

  assume ?lhs
  then obtain i where "suffix i w ⊨ G φ"
    by fastforce
  hence "⋀j. j ≥ i ⟹ (suffix j w ⊨ φ)"
    using le_iff_add[of i] by auto
  hence "⋀j. ¬suffix j w ⊨ φ ⟹ j < i"
    using le_less_linear by blast
  hence "?S ⊆ {k. k < i}"
    by blast
  hence "finite ?S"
    using finite_subset by fast
  thus ?rhs
    unfolding Alm_all_def Inf_many_def by presburger
next
  assume ?rhs
  obtain S where S_def: "S = {k. ¬ suffix k w ⊨ φ}" by blast
  hence "finite S"
    using ‹?rhs› unfolding Alm_all_def Inf_many_def by fast
  then obtain i where "i = Max S" by blast
  {
    fix j
    assume "i < j"
    hence "j ∉ S"
      using ‹i = Max S› Max.coboundedI[OF ‹finite S›] less_le_not_le by blast
    hence "suffix j w ⊨ φ" using S_def by fast
  }
  hence "∀j > i. (suffix j w ⊨ φ)" by simp
  hence "suffix (Suc i) w ⊨ G φ" by auto
  thus ?lhs
    using ltl_semantics.simps(9)[of w "G φ"] by blast
qed

lemma LTL_FG_suffix:
  "(suffix i w) ⊨ F (G φ) = w ⊨ F (G φ)"
proof -
  have "(∃m. ∀n≥m. suffix n w ⊨ φ) = (∃m. ∀n≥m. suffix n (suffix i w) ⊨ φ)" (is "?l = ?r")
  proof
    assume ?r
    then obtain m where "∀n≥m. suffix n (suffix i w) ⊨ φ"
      by blast
    hence "∀n≥i+m. suffix n w ⊨ φ"
      unfolding suffix_suffix by (metis le_iff_add add_leE add_le_cancel_left)
    thus ?l
      by auto
  qed (metis suffix_suffix trans_le_add2)
  thus ?thesis
    unfolding LTL_FG_almost_all_suffixes MOST_nat_le ..
qed

lemma LTL_GF_suffix:
  "(suffix i w) ⊨ G (F φ) = w ⊨ G (F φ)"
proof -
  have "(∀m. ∃n≥m. suffix n w ⊨ φ) = (∀m. ∃n≥m. suffix n (suffix i w) ⊨ φ)" (is "?l = ?r")
  proof
    assume ?l
    thus ?r
      by (metis suffix_suffix add_leE add_le_cancel_left le_Suc_ex)
  qed (metis suffix_suffix trans_le_add2)
  thus ?thesis
    unfolding LTL_GF_infinitely_many_suffixes INFM_nat_le ..
qed

lemma LTL_suffix_G:
  "w ⊨ G φ ⟹ suffix i w ⊨ G φ"
  using suffix_0 suffix_suffix by (induction i) simp_all

lemma LTL_prop_entailment_monotonI[intro]:
  "S ⊨P φ ⟹ S ⊆ S' ⟹ S' ⊨P φ"
  by (induction rule: ltl_prop_entailment.induct) auto

lemma ltl_models_equiv_prop_entailment:
  "w ⊨ φ = {χ. w ⊨ χ} ⊨P φ"
  by (induction φ) auto

subsubsection ‹Limit Behaviour of the G-operator›

abbreviation Only_G
where
  "Only_G S ≡ ∀x ∈ S. ∃y. x = G y"

lemma ltl_G_stabilize:
  assumes "finite 𝒢"
  assumes "Only_G 𝒢"
  obtains i where "⋀χ j. χ ∈ 𝒢 ⟹ suffix i w ⊨ χ = suffix (i + j) w ⊨ χ"
proof -
  have "finite 𝒢 ⟹ Only_G 𝒢 ⟹ ∃i. ∀χ ∈ 𝒢. ∀j. suffix i w ⊨ χ = suffix (i + j) w ⊨ χ"
  proof (induction rule: finite_induct)
    case (insert χ 𝒢)
      then obtain i1  where "⋀χ j. χ ∈ 𝒢 ⟹ suffix i1 w ⊨ χ = suffix (i1 + j) w ⊨ χ"
        by blast
      moreover
      from insert obtain ψ where "χ = G ψ"
        by blast
      have "∃i. ∀j. suffix i w ⊨ G ψ = suffix (i + j) w ⊨ G ψ"
        by (metis LTL_suffix_G plus_nat.add_0 suffix_0 suffix_suffix)
      then obtain i2 where "⋀j. suffix i2 w ⊨ χ = suffix (i2 + j) w ⊨ χ"
        unfolding ‹χ = G ψ› by blast
      ultimately
      have "⋀χ' j. χ' ∈ 𝒢 ∪ {χ} ⟹ suffix (i1 + i2) w ⊨ χ' = suffix (i1 + i2 + j) w ⊨ χ'"
        unfolding Un_iff singleton_iff by (metis add.commute add.left_commute)
      thus ?case
        by blast
  qed simp
  with assms obtain i where "⋀χ j. χ ∈ 𝒢 ⟹ suffix i w ⊨ χ = suffix (i + j) w ⊨ χ"
    by blast
  thus ?thesis
    using that by blast
qed

lemma ltl_G_stabilize_property:
  assumes "finite 𝒢"
  assumes "Only_G 𝒢"
  assumes "⋀χ j. χ ∈ 𝒢 ⟹ suffix i w ⊨ χ = suffix (i + j) w ⊨ χ"
  assumes "G ψ ∈ 𝒢 ∩ {χ. w ⊨ F χ}"
  shows "suffix i w ⊨ G ψ"
proof -
  obtain j where "suffix j w ⊨ G ψ"
    using assms by fastforce
  thus "suffix i w ⊨ G ψ"
    by (cases "i ≤ j", insert assms, unfold le_iff_add, blast,
        metis (erased, lifting) LTL_suffix_G ‹suffix j w ⊨ G ψ› le_add_diff_inverse nat_le_linear suffix_suffix)
qed

subsection ‹Subformulae›

subsubsection ‹Propositions›

fun propos :: "'a ltl ⇒'a ltl set"
where
  "propos true = {}"
| "propos false = {}"
| "propos (φ and ψ) = propos φ ∪ propos ψ"
| "propos (φ or ψ) = propos φ ∪ propos ψ"
| "propos φ = {φ}"

fun nested_propos :: "'a ltl ⇒'a ltl set"
where
  "nested_propos true = {}"
| "nested_propos false = {}"
| "nested_propos (φ and ψ) = nested_propos φ ∪ nested_propos ψ"
| "nested_propos (φ or ψ) = nested_propos φ ∪ nested_propos ψ"
| "nested_propos (F φ) = {F φ} ∪ nested_propos φ"
| "nested_propos (G φ) = {G φ} ∪ nested_propos φ"
| "nested_propos (X φ) = {X φ} ∪ nested_propos φ"
| "nested_propos (φ U ψ) = {φ U ψ} ∪ nested_propos φ ∪ nested_propos ψ"
| "nested_propos φ = {φ}"

lemma finite_propos:
  "finite (propos φ)" "finite (nested_propos φ)"
  by (induction φ) simp+

lemma propos_subset:
  "propos φ ⊆ nested_propos φ"
  by (induction φ) auto

lemma LTL_prop_entailment_restrict_to_propos:
  "S ⊨P φ = (S ∩ propos φ) ⊨P φ"
  by (induction φ) auto

lemma propos_foldl:
  assumes "⋀x y. propos (f x y) = propos x ∪ propos y"
  shows "⋃{propos y |y. y = i ∨ y ∈ set xs} = propos (foldl f i xs)"
proof (induction xs rule: rev_induct)
  case (snoc x xs)
    have "⋃{propos y |y. y = i ∨ y ∈ set (xs@[x])} = ⋃{propos y |y. y = i ∨ y ∈ set xs} ∪ propos x"
      by auto
    also
    have "… = propos (foldl f i xs) ∪ propos x"
      using snoc by auto
    also
    have "… = propos (foldl f i (xs@[x]))"
      using assms by simp
    finally
    show ?case .
qed simp

subsubsection ‹G-Subformulae›

text ‹Notation for paper: mathds{G}›

fun G_nested_propos :: "'a ltl ⇒'a ltl set" (‹G›)
where
  "G (φ and ψ) = G φ ∪ G ψ"
| "G (φ or ψ) = G φ ∪ G ψ"
| "G (F φ) = G φ"
| "G (G φ) = G φ ∪ {G φ}"
| "G (X φ) = G φ"
| "G (φ U ψ) = G φ ∪ G ψ"
| "G φ = {}"

lemma G_nested_finite:
  "finite (G φ)"
  by (induction φ) auto

lemma G_nested_propos_alt_def:
  "G φ = nested_propos φ ∩ {ψ. (∃x. ψ = G x)}"
  by (induction φ) auto

lemma G_nested_propos_Only_G:
  "Only_G (G φ)"
  unfolding G_nested_propos_alt_def by blast

lemma G_not_in_G:
  "G φ ∉ G φ"
proof -
  have "⋀χ. χ ∈ G φ ⟹ size φ ≥ size χ"
    by (induction φ) fastforce+
  thus ?thesis
    by fastforce
qed

lemma G_subset_G:
  "ψ ∈ G φ ⟹ G ψ ⊆ G φ"
  "G ψ ∈ G φ ⟹ G ψ ⊆ G φ"
  by (induction φ) auto

lemma 𝒢_properties:
  assumes "𝒢 ⊆ G φ"
  shows 𝒢_finite: "finite 𝒢" and 𝒢_elements: "Only_G 𝒢"
  using assms G_nested_finite G_nested_propos_alt_def by (blast dest: finite_subset)+

subsection ‹Propositional Implication and Equivalence›

definition ltl_prop_implies :: "['a ltl, 'a ltl] ⇒ bool" (infix ‹⟶P› 75)
where
  "φ ⟶P ψ ≡ ∀𝒜. 𝒜 ⊨P φ ⟶ 𝒜 ⊨P ψ"

definition ltl_prop_equiv :: "['a ltl, 'a ltl] ⇒ bool" (infix ‹≡P› 75)
where
  "φ ≡P ψ ≡ ∀𝒜. 𝒜 ⊨P φ ⟷ 𝒜 ⊨P ψ"

lemma ltl_prop_implies_equiv:
  "φ ⟶P ψ ∧ ψ ⟶P φ ⟷ φ ≡P ψ"
  unfolding ltl_prop_implies_def ltl_prop_equiv_def by meson

lemma ltl_prop_equiv_equivp:
  "equivp (≡P)"
  by (blast intro: equivpI[of "(≡P)", simplified transp_def symp_def reflp_def ltl_prop_equiv_def])

lemma [trans]:
  "φ ≡P ψ ⟹ ψ ≡P χ ⟹ φ ≡P χ"
  using ltl_prop_equiv_equivp[THEN equivp_transp] .

subsubsection ‹Quotient Type for Propositional Equivalence›

quotient_type 'a ltl_prop_equiv_quotient = "'a ltl" / "(≡P)"
  morphisms Rep Abs
  by (simp add: ltl_prop_equiv_equivp)

type_synonym 'a ltlP = "'a ltl_prop_equiv_quotient"

instantiation ltl_prop_equiv_quotient :: (type) equal begin

lift_definition ltl_prop_equiv_quotient_eq_test :: "'a ltlP ⇒ 'a ltlP ⇒ bool" is "λx y. x ≡P y"
  by (metis ltl_prop_equiv_quotient.abs_eq_iff)

definition
  eq: "equal_class.equal ≡ ltl_prop_equiv_quotient_eq_test"

instance
  by (standard; simp add: eq ltl_prop_equiv_quotient_eq_test.rep_eq, metis Quotient_ltl_prop_equiv_quotient Quotient_rel_rep)

end

lemma ltlP_abs_rep: "Abs (Rep φ) = φ"
  by (meson Quotient3_abs_rep Quotient3_ltl_prop_equiv_quotient)

lift_definition ltl_prop_entails_abs :: "'a ltl set ⇒ 'a ltlP ⇒ bool" (‹_ ↑⊨P _›) is "(⊨P)"
  by (simp add: ltl_prop_equiv_def)

lift_definition ltl_prop_implies_abs :: "'a ltlP ⇒ 'a ltlP ⇒ bool" (‹_ ↑⟶P _›) is "(⟶P)"
  by (simp add: ltl_prop_equiv_def ltl_prop_implies_def)

subsubsection ‹Propositional Equivalence implies LTL Equivalence›

lemma ltl_prop_implication_implies_ltl_implication:
  "w ⊨ φ ⟹ φ ⟶P ψ ⟹ w ⊨ ψ"
  using [[unfold_abs_def = false]]
  unfolding ltl_prop_implies_def ltl_models_equiv_prop_entailment by simp

lemma ltl_prop_equiv_implies_ltl_equiv:
  "φ ≡P ψ ⟹ w ⊨ φ = w ⊨ ψ"
  using ltl_prop_implication_implies_ltl_implication ltl_prop_implies_equiv by blast

subsection ‹Substitution›

fun subst :: "'a ltl ⇒ ('a ltl ⇀ 'a ltl) ⇒ 'a ltl"
where
  "subst true m = true"
| "subst false m = false"
| "subst (φ and ψ) m = subst φ m and subst ψ m"
| "subst (φ or ψ) m = subst φ m or subst ψ m"
| "subst φ m = (case m φ of Some φ' ⇒ φ' | None ⇒ φ)"

text ‹Based on Uwe Schoening's Translation Lemma (Logic for CS, p. 54)›

lemma ltl_prop_equiv_subst_S:
  "S ⊨P subst φ m = ((S - dom m) ∪ {χ | χ χ'. χ ∈ dom m ∧ m χ = Some χ' ∧ S ⊨P χ'}) ⊨P φ"
  by (induction φ) (auto split: option.split)

lemma subst_respects_ltl_prop_entailment:
  "φ ⟶P ψ ⟹ subst φ m ⟶P subst ψ m"
  "φ ≡P ψ ⟹ subst φ m ≡P subst ψ m"
  unfolding ltl_prop_equiv_def ltl_prop_implies_def ltl_prop_equiv_subst_S by blast+

lemma subst_respects_ltl_prop_entailment_generalized:
  "(⋀𝒜. (⋀x. x ∈ S ⟹ 𝒜 ⊨P x) ⟹ 𝒜 ⊨P y) ⟹ (⋀x. x ∈ S ⟹ 𝒜 ⊨P subst x m) ⟹ 𝒜 ⊨P subst y m"
  unfolding ltl_prop_equiv_subst_S by simp

lemma decomposable_function_subst:
  "⟦f true = true; f false = false; ⋀φ ψ. f (φ and ψ) = f φ and f ψ; ⋀φ ψ. f (φ or ψ) = f φ or f ψ⟧ ⟹ f φ = subst φ (λχ. Some (f χ))"
  by (induction φ) auto

subsection ‹Additional Operators›

subsubsection ‹And›

lemma foldl_LTLAnd_prop_entailment:
  "S ⊨P foldl LTLAnd i xs = (S ⊨P i ∧ (∀y ∈ set xs. S ⊨P y))"
  by (induction xs arbitrary: i) auto

fun And :: "'a ltl list ⇒ 'a ltl"
where
  "And [] = true"
| "And (x#xs) = foldl LTLAnd x xs"

lemma And_prop_entailment:
  "S ⊨P And xs = (∀x ∈ set xs. S ⊨P x)"
  using foldl_LTLAnd_prop_entailment by (cases xs) auto

lemma And_propos:
  "propos (And xs) = ⋃{propos x| x. x ∈ set xs}"
proof (cases xs)
  case Nil
    thus ?thesis by simp
next
  case (Cons x xs)
    thus ?thesis
      using propos_foldl[of LTLAnd x] by auto
qed

lemma And_semantics:
  "w ⊨ And xs = (∀x ∈ set xs. w ⊨ x)"
proof -
  have And_propos': "⋀x. x ∈ set xs ⟹ propos x ⊆ propos (And xs)"
    using And_propos by blast

  have "w ⊨ And xs = {χ. χ ∈ propos (And xs) ∧ w ⊨ χ} ⊨P (And xs)"
    using ltl_models_equiv_prop_entailment LTL_prop_entailment_restrict_to_propos by blast
  also
  have "… = (∀x ∈ set xs. {χ. χ ∈ propos (And xs) ∧ w ⊨ χ} ⊨P x)"
    using And_prop_entailment by auto
  also
  have "… = (∀x ∈ set xs. {χ. χ ∈ propos x ∧ w ⊨ χ} ⊨P x)"
    using LTL_prop_entailment_restrict_to_propos And_propos' by blast
  also
  have "… = (∀x ∈ set xs. w ⊨ x)"
    using ltl_models_equiv_prop_entailment LTL_prop_entailment_restrict_to_propos by blast
  finally
  show ?thesis .
qed

lemma And_append_syntactic:
  "xs ≠ [] ⟹ And (xs @ ys) = And ((And xs)#ys)"
  by (induction xs rule: list_nonempty_induct) simp+

lemma And_append_S:
  "S ⊨P And (xs @ ys) = S ⊨P And xs and And ys"
  using And_prop_entailment[of S] by auto

lemma And_append:
  "And (xs @ ys) ≡P And xs and And ys"
  unfolding ltl_prop_equiv_def using And_append_S by blast

subsubsection ‹Lifted Variant›

lift_definition and_abs :: "'a ltlP ⇒ 'a ltlP ⇒ 'a ltlP" (‹_ ↑and _›) is "λx y. x and y"
  unfolding ltl_prop_equiv_def by simp

fun And_abs :: "'a ltlP list ⇒ 'a ltlP" (‹↑And›)
where
  "↑And xs = foldl and_abs (Abs true) xs"

lemma foldl_LTLAnd_prop_entailment_abs:
  "S ↑⊨P foldl and_abs i xs = (S ↑⊨P i ∧ (∀y∈set xs. S ↑⊨P y))"
  by (induction xs arbitrary: i)
     (simp_all add: and_abs_def ltl_prop_entails_abs.abs_eq, metis ltl_prop_entails_abs.rep_eq)

lemma And_prop_entailment_abs:
  "S ↑⊨P ↑And xs = (∀x ∈ set xs. S ↑⊨P x)"
  by (simp add: foldl_LTLAnd_prop_entailment_abs ltl_prop_entails_abs.abs_eq)

lemma and_abs_conjunction:
  "S ↑⊨P φ ↑and ψ ⟷ S ↑⊨P φ ∧ S ↑⊨P ψ"
  by (metis and_abs.abs_eq ltlP_abs_rep ltl_prop_entailment.simps(3) ltl_prop_entails_abs.abs_eq)

subsubsection ‹Or›

lemma foldl_LTLOr_prop_entailment:
  "S ⊨P foldl LTLOr i xs = (S ⊨P i ∨ (∃y ∈ set xs. S ⊨P y))"
  by (induction xs arbitrary: i) auto

fun Or :: "'a ltl list ⇒ 'a ltl"
where
  "Or [] = false"
| "Or (x#xs) = foldl LTLOr x xs"

lemma Or_prop_entailment:
  "S ⊨P Or xs = (∃x ∈ set xs. S ⊨P x)"
  using foldl_LTLOr_prop_entailment by (cases xs) auto

lemma Or_propos:
  "propos (Or xs) = ⋃{propos x| x. x ∈ set xs}"
proof (cases xs)
  case Nil
    thus ?thesis by simp
next
  case (Cons x xs)
    thus ?thesis
      using propos_foldl[of LTLOr x] by auto
qed

lemma Or_semantics:
  "w ⊨ Or xs = (∃x ∈ set xs. w ⊨ x)"
proof -
  have Or_propos': "⋀x. x ∈ set xs ⟹ propos x ⊆ propos (Or xs)"
    using Or_propos by blast

  have "w ⊨ Or xs = {χ. χ ∈ propos (Or xs) ∧ w ⊨ χ} ⊨P (Or xs)"
    using ltl_models_equiv_prop_entailment LTL_prop_entailment_restrict_to_propos by blast
  also
  have "… = (∃x ∈ set xs. {χ. χ ∈ propos (Or xs) ∧ w ⊨ χ} ⊨P x)"
    using Or_prop_entailment by auto
  also
  have "… = (∃x ∈ set xs. {χ. χ ∈ propos x ∧ w ⊨ χ} ⊨P x)"
    using LTL_prop_entailment_restrict_to_propos Or_propos' by blast
  also
  have "… = (∃x ∈ set xs. w ⊨ x)"
    using ltl_models_equiv_prop_entailment LTL_prop_entailment_restrict_to_propos by blast
  finally
  show ?thesis .
qed

lemma Or_append_syntactic:
  "xs ≠ [] ⟹ Or (xs @ ys) = Or ((Or xs)#ys)"
  by (induction xs rule: list_nonempty_induct) simp+

lemma Or_append_S:
  "S ⊨P Or (xs @ ys) = S ⊨P Or xs or Or ys"
  using Or_prop_entailment[of S] by auto

lemma Or_append:
  "Or (xs @ ys) ≡P Or xs or Or ys"
  unfolding ltl_prop_equiv_def using Or_append_S by blast

subsubsection ‹$eval_G$›

― ‹Partly evaluate a formula by only considering G-subformulae›

fun evalG
where
  "evalG S (φ and ψ) = evalG S φ and evalG S ψ"
| "evalG S (φ or ψ) = evalG S φ or evalG S ψ"
| "evalG S (G φ) = (if G φ ∈ S then true else false)"
| "evalG S φ = φ"

― ‹Syntactic Properties›

lemma evalG_And_map:
  "evalG S (And xs) = And (map (evalG S) xs)"
proof (induction xs rule: rev_induct)
  case (snoc x xs)
    thus ?case
      by (cases xs) simp+
qed simp

lemma evalG_Or_map:
  "evalG S (Or xs) = Or (map (evalG S) xs)"
proof (induction xs rule: rev_induct)
  case (snoc x xs)
    thus ?case
      by (cases xs) simp+
qed simp

lemma evalG_G_nested:
  "G (evalG 𝒢 φ) ⊆ G φ"
  by (induction φ) (simp_all, blast+)

lemma evalG_subst:
  "evalG S φ = subst φ (λχ. Some (evalG S χ))"
  by (induction φ) simp_all

― ‹Semantic Properties›

lemma evalG_prop_entailment:
  "S ⊨P evalG S φ ⟷ S ⊨P φ"
  by (induction φ, auto)

lemma evalG_respectfulness:
  "φ ⟶P ψ ⟹ evalG S φ ⟶P evalG S ψ"
  "φ ≡P ψ ⟹ evalG S φ ≡P evalG S ψ"
  using subst_respects_ltl_prop_entailment evalG_subst by metis+

lemma evalG_respectfulness_generalized:
  "(⋀𝒜. (⋀x. x ∈ S ⟹ 𝒜 ⊨P x) ⟹ 𝒜 ⊨P y) ⟹ (⋀x. x ∈ S ⟹ 𝒜 ⊨P evalG P x) ⟹ 𝒜 ⊨P evalG P y"
  using subst_respects_ltl_prop_entailment_generalized[of S y 𝒜] evalG_subst[of P] by metis

lift_definition evalG_abs :: "'a ltl set ⇒ 'a ltlP ⇒ 'a ltlP" (‹↑evalG›) is evalG
  by (insert evalG_respectfulness(2))

subsection ‹Finite Quotient Set›

text ‹If we restrict formulas to a finite set of propositions, the set of quotients of these is finite›

lemma Rep_Abs_prop_entailment[simp]:
  "A ⊨P Rep (Abs φ) = A ⊨P φ"
  using Quotient3_ltl_prop_equiv_quotient[THEN rep_abs_rsp]
  by (auto simp add: ltl_prop_equiv_def)

fun sat_models :: "'a ltl_prop_equiv_quotient ⇒ 'a ltl set set"
where
  "sat_models a = {A. A ⊨P Rep(a)}"

lemma sat_models_invariant:
  "A ∈ sat_models (Abs φ) = A ⊨P φ"
  using Rep_Abs_prop_entailment by auto

lemma sat_models_inj:
  "inj sat_models"
  using Quotient3_ltl_prop_equiv_quotient[THEN Quotient3_rel_rep]
  by (auto simp add: ltl_prop_equiv_def inj_on_def)

lemma sat_models_finite_image:
  assumes "finite P"
  shows "finite (sat_models ` {Abs φ | φ. nested_propos φ ⊆ P})"
proof -
  have "sat_models (Abs φ) = {A ∪ B | A B. A ⊆ P ∧ A ⊨P φ ∧ B ⊆ UNIV - P}" (is "?lhs = ?rhs")
    if "nested_propos φ ⊆ P" for φ
  proof
    have "⋀A B. A ∈ sat_models (Abs φ) ⟹ A ∪ B ∈ sat_models (Abs φ)"
      unfolding sat_models_invariant by blast
    moreover
    have "{A | A. A ⊆ P ∧ A ⊨P φ} ⊆ sat_models (Abs φ)"
      using sat_models_invariant by fast
    ultimately
    show "?rhs ⊆ ?lhs"
      by blast
  next
    have "propos φ ⊆ P"
      using that propos_subset by blast
    have "A ∈ {A ∪ B | A B. A ⊆ P ∧ A ⊨P φ ∧ B ⊆ UNIV - P}"
      if "A ∈ sat_models (Abs φ)" for A
    proof (standard, goal_cases prems)
      case prems
        then have "A ⊨P φ"
          using that sat_models_invariant by blast
        then obtain C D where "C = (A ∩ P)" and "D = A - P" and "A = C ∪ D"
          by blast
        then have "C ⊨P φ" and "C ⊆ P" and "D ⊆ UNIV - P"
          using ‹A ⊨P φ› LTL_prop_entailment_restrict_to_propos ‹propos φ ⊆ P› by blast+
        then have "C ∪ D ∈ {A ∪ B | A B. A ⊆ P ∧ A ⊨P φ ∧ B ⊆ UNIV - P}"
          by blast
        thus ?case
          using ‹A = C ∪ D› by simp
    qed
    thus "?lhs ⊆ ?rhs"
      by blast
  qed
  hence Equal: "{sat_models (Abs φ) | φ. nested_propos φ ⊆ P} = {{A ∪ B | A B. A ⊆ P ∧ A ⊨P φ ∧ B ⊆ UNIV - P} | φ. nested_propos φ ⊆ P}"
    by (metis (lifting, no_types))

  have Finite: "finite {{A ∪ B | A B. A ⊆ P ∧ A ⊨P φ ∧ B ⊆ UNIV - P} | φ. nested_propos φ ⊆ P}"
  proof -
    let ?map = "λP S. {A ∪ B | A B. A ∈ S ∧ B ⊆ UNIV - P}"
    obtain S' where S'_def: "S' = {{A ∪ B | A B. A ⊆ P ∧ A ⊨P φ ∧ B ⊆ UNIV - P} | φ. nested_propos φ ⊆ P}"
      by blast
    obtain S where S_def: "S = {{A | A. A ⊆ P ∧ A ⊨P φ} | φ. nested_propos φ ⊆ P}"
      by blast

    ― ‹Prove S and ?map applied to it is finite›
    hence "S ⊆ Pow (Pow P)"
      by blast
    hence "finite S"
      using ‹finite P› finite_Pow_iff infinite_super by fast
    hence "finite {?map P A | A. A ∈ S}"
      by fastforce

    ― ‹Prove that S' can be embedded into S using ?map›

    have "S' ⊆ {?map P A | A. A ∈ S}"
    proof
      fix A
      assume "A ∈ S'"
      then obtain φ where "nested_propos φ ⊆ P"
        and "A = {A ∪ B | A B. A ⊆ P ∧ A ⊨P φ ∧ B ⊆ UNIV - P}"
        using S'_def by blast
      then have "?map P {A | A. A ⊆ P ∧ A ⊨P φ} = A"
        by simp
      moreover
      have "{A | A. A ⊆ P ∧ A ⊨P φ} ∈ S"
        using ‹nested_propos φ ⊆ P› S_def by auto
      ultimately
      show "A ∈ {?map P A | A. A ∈ S}"
        by blast
    qed

    show ?thesis
      using rev_finite_subset[OF ‹finite {?map P A | A. A ∈ S}› ‹S' ⊆ {?map P A | A. A ∈ S}›]
      unfolding S'_def .
  qed

  have Finite2: "finite {sat_models (Abs φ) | φ. nested_propos φ ⊆ P}"
    unfolding Equal using Finite by blast
  have Equal2: "sat_models ` {Abs φ | φ. nested_propos φ ⊆ P} = {sat_models (Abs φ) | φ. nested_propos φ ⊆ P}"
    by blast

  show ?thesis
    unfolding Equal2 using Finite2 by blast
qed

lemma ltl_prop_equiv_quotient_restricted_to_P_finite:
  assumes "finite P"
  shows "finite {Abs φ | φ. nested_propos φ ⊆ P}"
proof -
  have "inj_on sat_models {Abs φ |φ. nested_propos φ ⊆ P}"
    using sat_models_inj subset_inj_on by auto
  thus ?thesis
    using finite_imageD[OF sat_models_finite_image[OF assms]] by fast
qed

locale lift_ltl_transformer =
  fixes
    f :: "'a ltl ⇒ 'b ⇒ 'a ltl"
  assumes
    respectfulness: "φ ≡P ψ ⟹ f φ ν ≡P f ψ ν"
  assumes
    nested_propos_bounded: "nested_propos (f φ ν) ⊆ nested_propos φ"
begin

lift_definition f_abs :: "'a ltlP ⇒ 'b ⇒ 'a ltlP" is f
  using respectfulness .

lift_definition f_foldl_abs :: "'a ltlP ⇒ 'b list ⇒ 'a ltlP" is "foldl f"
proof -
  fix φ ψ :: "'a ltl" fix w :: "'b list" assume "φ ≡P ψ"
  thus "foldl f φ w ≡P foldl f ψ w"
    using respectfulness by (induction w arbitrary: φ ψ) simp+
qed

lemma f_foldl_abs_alt_def:
  "f_foldl_abs (Abs φ) w = foldl f_abs (Abs φ) w"
  by (induction w rule: rev_induct) (unfold f_foldl_abs.abs_eq foldl.simps foldl_append, (metis f_abs.abs_eq)+)

definition abs_reach :: "'a ltl_prop_equiv_quotient ⇒ 'a ltl_prop_equiv_quotient set"
where
  "abs_reach Φ = {foldl f_abs Φ w |w. True}"

lemma finite_abs_reach:
  "finite (abs_reach (Abs φ))"
proof -
  {
    fix w
    have "nested_propos (foldl f φ w) ⊆ nested_propos φ"
      by (induction w arbitrary: φ) (simp, metis foldl_Cons nested_propos_bounded subset_trans)
  }
  hence "abs_reach (Abs φ) ⊆ {Abs χ | χ. nested_propos χ ⊆ nested_propos φ}"
    unfolding abs_reach_def f_foldl_abs_alt_def[symmetric] f_foldl_abs.abs_eq by blast
  thus ?thesis
    using ltl_prop_equiv_quotient_restricted_to_P_finite finite_propos
    by (blast dest: finite_subset)
qed

end

end