Theory Disjunctive_Normal_Form

theory Disjunctive_Normal_Form
imports Equivalence_Relations FSet
(*
    Author:   Benedikt Seidl
    Author:   Salomon Sickert
    License:  BSD
*)

section ‹Disjunctive Normal Form of LTL formulas›

theory Disjunctive_Normal_Form
imports
  LTL Equivalence_Relations "HOL-Library.FSet"
begin

text ‹
  We use the propositional representation of LTL formulas to define
  the minimal disjunctive normal form of our formulas. For this purpose
  we define the minimal product ‹⊗m› and union ‹∪m›.
  In the end we show that for a set ‹𝒜› of literals,
  @{term "𝒜 ⊨P φ"} if, and only if, there exists a subset
  of ‹𝒜› in the minimal DNF of ‹φ›.
›


subsection ‹Definition of Minimum Sets›

definition (in ord) min_set :: "'a set ⇒ 'a set" where
  "min_set X = {y ∈ X. ∀x ∈ X. x ≤ y ⟶ x = y}"

lemma min_set_iff:
  "x ∈ min_set X ⟷ x ∈ X ∧ (∀y ∈ X. y ≤ x ⟶ y = x)"
  unfolding min_set_def by blast

lemma min_set_subset:
  "min_set X ⊆ X"
  by (auto simp: min_set_def)

lemma min_set_idem[simp]:
  "min_set (min_set X) = min_set X"
  by (auto simp: min_set_def)

lemma min_set_empty[simp]:
  "min_set {} = {}"
  using min_set_subset by blast

lemma min_set_singleton[simp]:
  "min_set {x} = {x}"
  by (auto simp: min_set_def)

lemma min_set_finite:
  "finite X ⟹ finite (min_set X)"
  by (simp add: min_set_def)

lemma min_set_obtains_helper:
  "A ∈ B ⟹ ∃C. C |⊆| A ∧ C ∈ min_set B"
proof (induction "fcard A" arbitrary: A rule: less_induct)
  case less

  then have "(∀A'. A' ∉ B ∨ ¬ A' |⊆| A ∨ A' = A) ∨ (∃A'. A' |⊆| A ∧ A' ∈ min_set B)"
    by (metis (no_types) dual_order.trans order.not_eq_order_implies_strict pfsubset_fcard_mono)

  then show ?case
    using less.prems min_set_def by auto
qed

lemma min_set_obtains:
  assumes "A ∈ B"
  obtains C where "C |⊆| A" and "C ∈ min_set B"
  using min_set_obtains_helper assms by metis



subsection ‹Minimal operators on sets›

definition product :: "'a fset set ⇒ 'a fset set ⇒ 'a fset set" (infixr "⊗" 65)
  where "A ⊗ B = {a |∪| b | a b. a ∈ A ∧ b ∈ B}"

definition min_product :: "'a fset set ⇒ 'a fset set ⇒ 'a fset set" (infixr "⊗m" 65)
  where "A ⊗m B = min_set (A ⊗ B)"

definition min_product_set :: "'a fset set set ⇒ 'a fset set" ("⨂m")
  where "⨂m X = Finite_Set.fold min_product {{||}} X"

definition min_union :: "'a fset set ⇒ 'a fset set ⇒ 'a fset set" (infixr "∪m" 65)
  where "A ∪m B = min_set (A ∪ B)"


lemma min_product_idem[simp]:
  "A ⊗m A = min_set A"
  by (auto simp: min_product_def product_def min_set_def) fastforce

lemma min_union_idem[simp]:
  "A ∪m A = min_set A"
  by (simp add: min_union_def)


lemma product_empty[simp]:
  "A ⊗ {} = {}"
  "{} ⊗ A = {}"
  by (simp_all add: product_def)

lemma min_product_empty[simp]:
  "A ⊗m {} = {}"
  "{} ⊗m A = {}"
  by (simp_all add: min_product_def)

lemma min_union_empty[simp]:
  "A ∪m {} = min_set A"
  "{} ∪m A = min_set A"
  by (simp_all add: min_union_def)

lemma min_product_set_empty[simp]:
  "⨂m {} = {{||}}"
  by (simp add: min_product_set_def)

lemma product_empty_singleton[simp]:
  "A ⊗ {{||}} = A"
  "{{||}} ⊗ A = A"
  by (simp_all add: product_def)

lemma min_product_empty_singleton[simp]:
  "A ⊗m {{||}} = min_set A"
  "{{||}} ⊗m A = min_set A"
  by (simp_all add: min_product_def)


lemma product_comm:
  "A ⊗ B = B ⊗ A"
  unfolding product_def by blast

lemma min_product_comm:
  "A ⊗m B = B ⊗m A"
  unfolding min_product_def
  by (simp add: product_comm)

lemma min_union_comm:
  "A ∪m B = B ∪m A"
  unfolding min_union_def
  by (simp add: sup.commute)


lemma product_iff:
  "x ∈ A ⊗ B ⟷ (∃a ∈ A. ∃b ∈ B. x = a |∪| b)"
  unfolding product_def by blast

lemma min_product_iff:
  "x ∈ A ⊗m B ⟷ (∃a ∈ A. ∃b ∈ B. x = a |∪| b) ∧ (∀a ∈ A. ∀b ∈ B. a |∪| b |⊆| x ⟶ a |∪| b = x)"
  unfolding min_product_def min_set_iff product_iff product_def by blast

lemma min_union_iff:
  "x ∈ A ∪m B ⟷ x ∈ A ∪ B ∧ (∀a ∈ A. a |⊆| x ⟶ a = x) ∧ (∀b ∈ B. b |⊆| x ⟶ b = x)"
  unfolding min_union_def min_set_iff by blast


lemma min_set_min_product_helper:
  "x ∈ (min_set A) ⊗m B ⟷ x ∈ A ⊗m B"
proof
  fix x
  assume "x ∈ (min_set A) ⊗m B"

  then obtain a b where "a ∈ min_set A" and "b ∈ B" and "x = a |∪| b" and 1: "∀a ∈ min_set A. ∀b ∈ B. a |∪| b |⊆| x ⟶ a |∪| b = x"
    unfolding min_product_iff by blast

  moreover

  {
    fix a' b'
    assume "a' ∈ A" and "b' ∈ B" and "a' |∪| b' |⊆| x"

    then obtain a'' where "a'' |⊆| a'" and "a'' ∈ min_set A"
      using min_set_obtains by metis

    then have "a'' |∪| b' = x"
      by (metis (full_types) 1 ‹b' ∈ B› ‹a' |∪| b' |⊆| x› dual_order.trans le_sup_iff)

    then have "a' |∪| b' = x"
      using ‹a' |∪| b' |⊆| x› ‹a'' |⊆| a'› by blast
  }

  ultimately show "x ∈ A ⊗m B"
    by (metis min_product_iff min_set_iff)
next
  fix x
  assume "x ∈ A ⊗m B"

  then have 1: "x ∈ A ⊗ B" and "∀y ∈ A ⊗ B. y |⊆| x ⟶ y = x"
    unfolding min_product_def min_set_iff by simp+

  then have 2: "∀y∈min_set A ⊗ B. y |⊆| x ⟶ y = x"
    by (metis product_iff min_set_iff)

  then have "x ∈ min_set A ⊗ B"
    by (metis 1 funion_mono min_set_obtains order_refl product_iff)

  then show "x ∈ min_set A ⊗m B"
    by (simp add: 2 min_product_def min_set_iff)
qed

lemma min_set_min_product[simp]:
  "(min_set A) ⊗m B = A ⊗m B"
  "A ⊗m (min_set B) = A ⊗m B"
  using min_product_comm min_set_min_product_helper by blast+

lemma min_set_min_union[simp]:
  "(min_set A) ∪m B = A ∪m B"
  "A ∪m (min_set B) = A ∪m B"
proof (unfold min_union_def min_set_def, safe)
  show "⋀x xa xb. ⟦∀xa∈{y ∈ A. ∀x∈A. x |⊆| y ⟶ x = y} ∪ B. xa |⊆| x ⟶ xa = x; x ∈ B; xa |⊆| x; xb |∈| x; xa ∈ A⟧ ⟹ xb |∈| xa"
    by (metis (mono_tags) UnCI dual_order.trans fequalityI min_set_def min_set_obtains)
next
  show "⋀x xa xb. ⟦∀xa∈A ∪ {y ∈ B. ∀x∈B. x |⊆| y ⟶ x = y}. xa |⊆| x ⟶ xa = x; x ∈ A; xa |⊆| x; xb |∈| x; xa ∈ B⟧ ⟹ xb |∈| xa"
    by (metis (mono_tags) UnCI dual_order.trans fequalityI min_set_def min_set_obtains)
qed blast+


lemma product_assoc[simp]:
  "(A ⊗ B) ⊗ C = A ⊗ (B ⊗ C)"
proof (unfold product_def, safe)
  fix a b c
  assume "a ∈ A" and "c ∈ C" and "b ∈ B"
  then have "b |∪| c ∈ {b |∪| c |b c. b ∈ B ∧ c ∈ C}"
    by blast
  then show "∃a' bc. a |∪| b |∪| c = a' |∪| bc ∧ a' ∈ A ∧ bc ∈ {b |∪| c |b c. b ∈ B ∧ c ∈ C}"
    using `a ∈ A` by (metis (no_types) inf_sup_aci(5) sup_left_commute)
qed (metis (mono_tags, lifting) mem_Collect_eq sup_assoc)


lemma min_product_assoc[simp]:
  "(A ⊗m B) ⊗m C = A ⊗m (B ⊗m C)"
  unfolding min_product_def[of A B] min_product_def[of B C]
  by simp (simp add: min_product_def)

lemma min_union_assoc[simp]:
  "(A ∪m B) ∪m C = A ∪m (B ∪m C)"
  unfolding min_union_def[of A B] min_union_def[of B C]
  by simp (simp add: min_union_def sup_assoc)


lemma min_product_comp:
  "a ∈ A ⟹ b ∈ B ⟹ ∃c. c |⊆| (a |∪| b) ∧ c ∈ A ⊗m B"
  by (metis (mono_tags, lifting) mem_Collect_eq min_product_def product_def min_set_obtains)

lemma min_union_comp:
  "a ∈ A ⟹ ∃c. c |⊆| a ∧ c ∈ A ∪m B"
  by (metis Un_iff min_set_obtains min_union_def)


interpretation min_product_set_thms: Finite_Set.comp_fun_idem min_product
proof unfold_locales
  have "⋀x y z. x ⊗m (y ⊗m z) = y ⊗m (x ⊗m z)"
    by (simp only: min_product_assoc[symmetric]) (simp only: min_product_comm)

  then show "⋀x y. (⊗m) y ∘ (⊗m) x = (⊗m) x ∘ (⊗m) y"
    by fastforce
next
  have "⋀x y. x ⊗m (x ⊗m y) = x ⊗m y"
    by (simp add: min_product_assoc[symmetric])

  then show "⋀x. (⊗m) x ∘ (⊗m) x = (⊗m) x"
    by fastforce
qed


interpretation min_union_set_thms: Finite_Set.comp_fun_idem min_union
proof unfold_locales
  have "⋀x y z. x ∪m (y ∪m z) = y ∪m (x ∪m z)"
    by (simp only: min_union_assoc[symmetric]) (simp only: min_union_comm)

  then show "⋀x y. (∪m) y ∘ (∪m) x = (∪m) x ∘ (∪m) y"
    by fastforce
next
  have "⋀x y. x ∪m (x ∪m y) = x ∪m y"
    by (simp add: min_union_assoc[symmetric])

  then show "⋀x. (∪m) x ∘ (∪m) x = (∪m) x"
    by fastforce
qed

lemma min_product_set_insert[simp]:
  "finite X ⟹ ⨂m (insert x X) = x ⊗m (⨂m X)"
  unfolding min_product_set_def min_product_set_thms.fold_insert_idem ..

lemma min_product_subseteq:
  "x ∈ A ⊗m B ⟹ ∃a. a |⊆| x ∧ a ∈ A"
  by (metis funion_upper1 min_product_iff)

lemma min_product_set_subseteq:
  "finite X ⟹ x ∈ ⨂m X ⟹ A ∈ X ⟹ ∃a ∈ A. a |⊆| x"
  by (induction X rule: finite_induct) (blast, metis finite_insert insert_absorb min_product_set_insert min_product_subseteq)


lemma min_product_min_set[simp]:
  "min_set (A ⊗m B) = A ⊗m B"
  by (simp add: min_product_def)

lemma min_product_set_min_set[simp]:
  "finite X ⟹ min_set (⨂m X) = ⨂m X"
  by (induction X rule: finite_induct) (auto simp add: min_product_set_def min_set_iff)

lemma min_union_min_set[simp]:
  "min_set (A ∪m B) = A ∪m B"
  by (simp add: min_union_def)


lemma min_product_set_union[simp]:
  "finite X ⟹ finite Y ⟹ ⨂m (X ∪ Y) = (⨂m X) ⊗m (⨂m Y)"
  by (induction X rule: finite_induct) simp_all


lemma product_finite:
  "finite A ⟹ finite B ⟹ finite (A ⊗ B)"
  by (simp add: product_def finite_image_set2)

lemma min_product_finite:
  "finite A ⟹ finite B ⟹ finite (A ⊗m B)"
  by (metis min_product_def product_finite min_set_finite)

lemma min_product_set_finite:
  "finite X ⟹ (⋀x. x ∈ X ⟹ finite x) ⟹ finite (⨂m X)"
  by (induction X rule: finite_induct) (simp_all add: min_product_set_def, insert min_product_finite, blast)

lemma min_union_finite:
  "finite A ⟹ finite B ⟹ finite (A ∪m B)"
  by (simp add: min_union_def min_set_finite)



subsection ‹Disjunctive Normal Form›

fun dnf :: "'a ltln ⇒ 'a ltln fset set"
where
  "dnf truen = {{||}}"
| "dnf falsen = {}"
| "dnf (φ andn ψ) = (dnf φ) ⊗ (dnf ψ)"
| "dnf (φ orn ψ) = (dnf φ) ∪ (dnf ψ)"
| "dnf φ = {{|φ|}}"

fun min_dnf :: "'a ltln ⇒ 'a ltln fset set"
where
  "min_dnf truen = {{||}}"
| "min_dnf falsen = {}"
| "min_dnf (φ andn ψ) = (min_dnf φ) ⊗m (min_dnf ψ)"
| "min_dnf (φ orn ψ) = (min_dnf φ) ∪m (min_dnf ψ)"
| "min_dnf φ = {{|φ|}}"

lemma dnf_min_set:
  "min_dnf φ = min_set (dnf φ)"
  by (induction φ) (simp_all, simp_all only: min_product_def min_union_def)

lemma dnf_finite:
  "finite (dnf φ)"
  by (induction φ) (auto simp: product_finite)

lemma min_dnf_finite:
  "finite (min_dnf φ)"
  by (induction φ) (auto simp: min_product_finite min_union_finite)

lemma dnf_Abs_fset[simp]:
  "fset (Abs_fset (dnf φ)) = dnf φ"
  by (simp add: dnf_finite Abs_fset_inverse)

lemma min_dnf_Abs_fset[simp]:
  "fset (Abs_fset (min_dnf φ)) = min_dnf φ"
  by (simp add: min_dnf_finite Abs_fset_inverse)

lemma dnf_prop_atoms:
  "A ∈ dnf φ ⟹ fset A ⊆ prop_atoms φ"
  by (induction φ arbitrary: A) (auto simp: product_def, blast+)

lemma min_dnf_prop_atoms:
  "A ∈ min_dnf φ ⟹ fset A ⊆ prop_atoms φ"
  by (induction φ arbitrary: A) (simp_all add: min_product_iff min_union_iff, fastforce+)

lemma min_dnf_min_set[simp]:
  "min_set (min_dnf φ) = min_dnf φ"
  by (induction φ) (simp_all add: min_set_def min_product_def min_union_def, blast+)


lemma min_dnf_iff_prop_assignment_subset:
  "𝒜 ⊨P φ ⟷ (∃B. fset B ⊆ 𝒜 ∧ B ∈ min_dnf φ)"
proof
  assume "𝒜 ⊨P φ"

  then show "∃B. fset B ⊆ 𝒜 ∧ B ∈ min_dnf φ"
  proof (induction φ arbitrary: 𝒜)
    case (And_ltln φ1 φ2)

    then obtain B1 B2 where 1: "fset B1 ⊆ 𝒜 ∧ B1 ∈ min_dnf φ1" and 2: "fset B2 ⊆ 𝒜 ∧ B2 ∈ min_dnf φ2"
      by fastforce

    then obtain C where "C |⊆| B1 |∪| B2" and "C ∈ min_dnf φ1m min_dnf φ2"
      using min_product_comp by metis

    then show ?case
      by (metis 1 2 le_sup_iff min_dnf.simps(3) sup.absorb_iff1 sup_fset.rep_eq)
  next
    case (Or_ltln φ1 φ2)

    {
      assume "𝒜 ⊨P φ1"

      then obtain B where 1: "fset B ⊆ 𝒜 ∧ B ∈ min_dnf φ1"
        using Or_ltln by fastforce

      then obtain C where "C |⊆| B" and "C ∈ min_dnf φ1m min_dnf φ2"
        using min_union_comp by metis

      then have ?case
        by (metis 1 dual_order.trans less_eq_fset.rep_eq min_dnf.simps(4))
    }

    moreover

    {
      assume "𝒜 ⊨P φ2"

      then obtain B where 2: "fset B ⊆ 𝒜 ∧ B ∈ min_dnf φ2"
        using Or_ltln by fastforce

      then obtain C where "C |⊆| B" and "C ∈ min_dnf φ1m min_dnf φ2"
        using min_union_comp min_union_comm by metis

      then have ?case
        by (metis 2 dual_order.trans less_eq_fset.rep_eq min_dnf.simps(4))
    }

    ultimately show ?case
      using Or_ltln.prems by auto
  qed simp_all
next
  assume "∃B. fset B ⊆ 𝒜 ∧ B ∈ min_dnf φ"

  then obtain B where "fset B ⊆ 𝒜" and "B ∈ min_dnf φ"
    by auto

  then have "fset B ⊨P φ"
    by (induction φ arbitrary: B) (auto simp: min_set_def min_product_def product_def min_union_def, blast+)

  then show "𝒜 ⊨P φ"
    using ‹fset B ⊆ 𝒜› by blast
qed


lemma ltl_prop_implies_min_dnf:
  "φ ⟶P ψ = (∀A ∈ min_dnf φ. ∃B ∈ min_dnf ψ. B |⊆| A)"
  by (meson less_eq_fset.rep_eq ltl_prop_implies_def min_dnf_iff_prop_assignment_subset order_refl dual_order.trans)

lemma ltl_prop_equiv_min_dnf:
  "φ ∼P ψ = (min_dnf φ = min_dnf ψ)"
proof
  assume "φ ∼P ψ"

  then have "⋀x. x ∈ min_set (min_dnf φ) ⟷ x ∈ min_set (min_dnf ψ)"
    unfolding ltl_prop_implies_equiv ltl_prop_implies_min_dnf min_set_iff
    by fastforce

  then show "min_dnf φ = min_dnf ψ"
    by auto
qed (simp add: ltl_prop_equiv_def min_dnf_iff_prop_assignment_subset)

lemma min_dnf_rep_abs[simp]:
  "min_dnf (rep_ltlnP (abs_ltlnP φ)) = min_dnf φ"
  by (simp add: ltl_prop_equiv_min_dnf[symmetric] Quotient3_ltlnP rep_abs_rsp_left)


subsection ‹Folding of ‹andn› and ‹orn› over Finite Sets›

definition Andn :: "'a ltln set ⇒ 'a ltln"
where
  "Andn Φ ≡ SOME φ. fold_graph And_ltln True_ltln Φ φ"

definition Orn :: "'a ltln set ⇒ 'a ltln"
where
  "Orn Φ ≡ SOME φ. fold_graph Or_ltln False_ltln Φ φ"

lemma fold_graph_Andn:
  "finite Φ ⟹ fold_graph And_ltln True_ltln Φ (Andn Φ)"
  unfolding Andn_def by (rule someI2_ex[OF finite_imp_fold_graph])

lemma fold_graph_Orn:
  "finite Φ ⟹ fold_graph Or_ltln False_ltln Φ (Orn Φ)"
  unfolding Orn_def by (rule someI2_ex[OF finite_imp_fold_graph])

lemma Andn_semantics:
  "finite Φ ⟹ w ⊨n Andn Φ ⟷ (∀φ ∈ Φ. w ⊨n φ)"
proof -
  assume "finite Φ"
  have "⋀ψ. fold_graph And_ltln True_ltln Φ ψ ⟹ w ⊨n ψ ⟷ (∀φ ∈ Φ. w ⊨n φ)"
    by (rule fold_graph.induct) auto
  then show ?thesis
    using fold_graph_Andn[OF ‹finite Φ›] by simp
qed

lemma Orn_semantics:
  "finite Φ ⟹ w ⊨n Orn Φ ⟷ (∃φ ∈ Φ. w ⊨n φ)"
proof -
  assume "finite Φ"
  have "⋀ψ. fold_graph Or_ltln False_ltln Φ ψ ⟹ w ⊨n ψ ⟷ (∃φ ∈ Φ. w ⊨n φ)"
    by (rule fold_graph.induct) auto
  then show ?thesis
    using fold_graph_Orn[OF ‹finite Φ›] by simp
qed

lemma Andn_prop_semantics:
  "finite Φ ⟹ 𝒜 ⊨P Andn Φ ⟷ (∀φ ∈ Φ. 𝒜 ⊨P φ)"
proof -
  assume "finite Φ"
  have "⋀ψ. fold_graph And_ltln True_ltln Φ ψ ⟹ 𝒜 ⊨P ψ ⟷ (∀φ ∈ Φ. 𝒜 ⊨P φ)"
    by (rule fold_graph.induct) auto
  then show ?thesis
    using fold_graph_Andn[OF ‹finite Φ›] by simp
qed

lemma Orn_prop_semantics:
  "finite Φ ⟹ 𝒜 ⊨P Orn Φ ⟷ (∃φ ∈ Φ. 𝒜 ⊨P φ)"
proof -
  assume "finite Φ"
  have "⋀ψ. fold_graph Or_ltln False_ltln Φ ψ ⟹ 𝒜 ⊨P ψ ⟷ (∃φ ∈ Φ. 𝒜 ⊨P φ)"
    by (rule fold_graph.induct) auto
  then show ?thesis
    using fold_graph_Orn[OF ‹finite Φ›] by simp
qed

lemma Orn_Andn_image_semantics:
  assumes "finite 𝒜" and "⋀Φ. Φ ∈ 𝒜 ⟹ finite Φ"
  shows "w ⊨n Orn (Andn ` 𝒜) ⟷ (∃Φ ∈ 𝒜. ∀φ ∈ Φ. w ⊨n φ)"
proof -
  have "w ⊨n Orn (Andn ` 𝒜) ⟷ (∃Φ ∈ 𝒜. w ⊨n Andn Φ)"
    using Orn_semantics assms by auto
  then show ?thesis
    using Andn_semantics assms by fast
qed

lemma Orn_Andn_image_prop_semantics:
  assumes "finite 𝒜" and "⋀Φ. Φ ∈ 𝒜 ⟹ finite Φ"
  shows "ℐ ⊨P Orn (Andn ` 𝒜) ⟷ (∃Φ ∈ 𝒜. ∀φ ∈ Φ. ℐ ⊨P φ)"
proof -
  have "ℐ ⊨P Orn (Andn ` 𝒜) ⟷ (∃Φ ∈ 𝒜. ℐ ⊨P Andn Φ)"
    using Orn_prop_semantics assms by blast
  then show ?thesis
    using Andn_prop_semantics assms by metis
qed


subsection ‹DNF to LTL conversion›

definition ltln_of_dnf :: "'a ltln fset set ⇒ 'a ltln"
where
  "ltln_of_dnf 𝒜 = Orn (Andn ` fset ` 𝒜)"

lemma ltln_of_dnf_semantics:
  assumes "finite 𝒜"
  shows "w ⊨n ltln_of_dnf 𝒜 ⟷ (∃Φ ∈ 𝒜. ∀φ. φ |∈| Φ ⟶ w ⊨n φ)"
proof -
  have "finite (fset ` 𝒜)"
    using assms by blast

  then have "w ⊨n ltln_of_dnf 𝒜 ⟷ (∃Φ ∈ fset ` 𝒜. ∀φ ∈ Φ. w ⊨n φ)"
    unfolding ltln_of_dnf_def using Orn_Andn_image_semantics by fastforce

  then show ?thesis
    by (metis image_iff notin_fset)
qed

lemma ltln_of_dnf_prop_semantics:
  assumes "finite 𝒜"
  shows "ℐ ⊨P ltln_of_dnf 𝒜 ⟷ (∃Φ ∈ 𝒜. ∀φ. φ |∈| Φ ⟶ ℐ ⊨P φ)"
proof -
  have "finite (fset ` 𝒜)"
    using assms by blast

  then have "ℐ ⊨P ltln_of_dnf 𝒜 ⟷ (∃Φ ∈ fset ` 𝒜. ∀φ ∈ Φ. ℐ ⊨P φ)"
    unfolding ltln_of_dnf_def using Orn_Andn_image_prop_semantics by fastforce

  then show ?thesis
    by (metis image_iff notin_fset)
qed

lemma ltln_of_dnf_prop_equiv:
  "ltln_of_dnf (min_dnf φ) ∼P φ"
  unfolding ltl_prop_equiv_def
proof
  fix 𝒜
  have "𝒜 ⊨P ltln_of_dnf (min_dnf φ) ⟷ (∃Φ ∈ min_dnf φ. ∀φ. φ |∈| Φ ⟶ 𝒜 ⊨P φ)"
    using ltln_of_dnf_prop_semantics min_dnf_finite by metis
  also have "… ⟷ (∃Φ ∈ min_dnf φ. fset Φ ⊆ 𝒜)"
    by (metis min_dnf_prop_atoms prop_atoms_entailment_iff notin_fset subset_eq)
  also have "… ⟷ 𝒜 ⊨P φ"
    using min_dnf_iff_prop_assignment_subset by blast
  finally show "𝒜 ⊨P ltln_of_dnf (min_dnf φ) = 𝒜 ⊨P φ" .
qed

end