Theory LTL.Disjunctive_Normal_Form

(*
    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_union :: "'a fset set ⇒ 'a fset set ⇒ 'a fset set" (infixr ‹∪⇩_m› 65)
  where "A ∪⇩_m B = min_set (A ∪ B)"

definition product_set :: "'a fset set set ⇒ 'a fset set" (‹⨂›)
  where "⨂ X = Finite_Set.fold product {{||}} X"

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


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 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_singleton_singleton:
  "A ⊗ {{|x|}} = finsert x ` A"
  "{{|x|}} ⊗ A = finsert x ` A"
  unfolding product_def by blast+

lemma product_mono:
  "A ⊆ B ⟹ A ⊗ C ⊆ B ⊗ C"
  "B ⊆ C ⟹ A ⊗ B ⊆ A ⊗ C"
  unfolding product_def by auto



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_union_finite:
  "finite A ⟹ finite B ⟹ finite (A ∪⇩_m B)"
  by (simp add: min_union_def min_set_finite)


lemma product_set_infinite[simp]:
  "infinite X ⟹ ⨂ X = {{||}}"
  by (simp add: product_set_def)

lemma min_product_set_infinite[simp]:
  "infinite X ⟹ ⨂⇩_m X = {{||}}"
  by (simp add: min_product_set_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 product_set_thms: Finite_Set.comp_fun_commute product
proof unfold_locales
  have "⋀x y z. x ⊗ (y ⊗ z) = y ⊗ (x ⊗ z)"
    by (simp only: product_assoc[symmetric]) (simp only: product_comm)

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

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 product_set_empty[simp]:
  "⨂ {} = {{||}}"
  "⨂ {{}} = {}"
  "⨂ {{{||}}} = {{||}}"
  by (simp_all add: product_set_def)

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

lemma product_set_code[code]:
  "⨂ (set xs) = fold product (remdups xs) {{||}}"
  by (simp add: product_set_def product_set_thms.fold_set_fold_remdups)

lemma min_product_set_code[code]:
  "⨂⇩_m (set xs) = fold min_product (remdups xs) {{||}}"
  by (simp add: min_product_set_def min_product_set_thms.fold_set_fold_remdups)

lemma product_set_insert[simp]:
  "finite X ⟹ ⨂ (insert x X) = x ⊗ (⨂ (X - {x}))"
  unfolding product_set_def product_set_thms.fold_insert_remove ..

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_set_product_set:
  "⨂⇩_m A = min_set (⨂ A)"
  by (cases "finite A", induction A rule: finite_induct) (simp_all add: min_product_set_def product_set_def, metis min_product_def)


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

lemma min_union_min_set[simp]:
  "min_set (A ∪⇩_m B) = A ∪⇩_m B"
  by (simp add: min_union_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_set_min_product_set[simp]:
  "finite X ⟹ ⨂⇩_m (min_set ` X) = ⨂⇩_m X"
  by (induction X rule: finite_induct) simp_all

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_set_finite:
  "(⋀x. x ∈ X ⟹ finite x) ⟹ finite (⨂ X)"
  by (cases "finite X", rotate_tac, induction X rule: finite_induct) (simp_all add: product_set_def, insert product_finite, blast)

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



subsection ‹Disjunctive Normal Form›

fun dnf :: "'a ltln ⇒ 'a ltln fset set"
where
  "dnf true⇩_n = {{||}}"
| "dnf false⇩_n = {}"
| "dnf (φ and⇩_n ψ) = (dnf φ) ⊗ (dnf ψ)"
| "dnf (φ or⇩_n ψ) = (dnf φ) ∪ (dnf ψ)"
| "dnf φ = {{|φ|}}"

fun min_dnf :: "'a ltln ⇒ 'a ltln fset set"
where
  "min_dnf true⇩_n = {{||}}"
| "min_dnf false⇩_n = {}"
| "min_dnf (φ and⇩_n ψ) = (min_dnf φ) ⊗⇩_m (min_dnf ψ)"
| "min_dnf (φ or⇩_n ψ) = (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:
  "Φ ∈ dnf φ ⟹ fset Φ ⊆ prop_atoms φ"
  by (induction φ arbitrary: Φ) (auto simp: product_def)

lemma min_dnf_prop_atoms:
  "Φ ∈ min_dnf φ ⟹ fset Φ ⊆ prop_atoms φ"
  using dnf_min_set dnf_prop_atoms min_set_subset by blast

lemma min_dnf_atoms_dnf:
  "Φ ∈ min_dnf ψ ⟹ φ ∈ fset Φ ⟹ dnf φ = {{|φ|}}"
proof (induction φ)
  case True_ltln
  then show ?case
    using min_dnf_prop_atoms prop_atoms_notin(1) by blast
next
  case False_ltln
  then show ?case
    using min_dnf_prop_atoms prop_atoms_notin(2) by blast
next
  case (And_ltln φ1 φ2)
  then show ?case
    using min_dnf_prop_atoms prop_atoms_notin(3) by force
next
  case (Or_ltln φ1 φ2)
  then show ?case
    using min_dnf_prop_atoms prop_atoms_notin(4) by force
qed auto

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 φ⇩₁ φ⇩₂)

    then obtain B⇩₁ B⇩₂ where 1: "fset B⇩₁ ⊆ 𝒜 ∧ B⇩₁ ∈ min_dnf φ⇩₁" and 2: "fset B⇩₂ ⊆ 𝒜 ∧ B⇩₂ ∈ min_dnf φ⇩₂"
      by fastforce

    then obtain C where "C |⊆| B⇩₁ |∪| B⇩₂" and "C ∈ min_dnf φ⇩₁ ⊗⇩_m min_dnf φ⇩₂"
      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 φ⇩₁ φ⇩₂)

    {
      assume "𝒜 ⊨⇩_P φ⇩₁"

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

      then obtain C where "C |⊆| B" and "C ∈ min_dnf φ⇩₁ ∪⇩_m min_dnf φ⇩₂"
        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 φ⇩₂"

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

      then obtain C where "C |⊆| B" and "C ∈ min_dnf φ⇩₁ ∪⇩_m min_dnf φ⇩₂"
        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)

  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_ltln⇩_P (abs_ltln⇩_P φ)) = min_dnf φ"
  by (simp add: ltl_prop_equiv_min_dnf[symmetric] Quotient3_ltln⇩_P rep_abs_rsp_left)


subsection ‹Folding of ‹and⇩_n› and ‹or⇩_n› over Finite Sets›

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

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

lemma fold_graph_And⇩_n:
  "finite Φ ⟹ fold_graph And_ltln True_ltln Φ (And⇩_n Φ)"
  unfolding And⇩_n_def by (rule someI2_ex[OF finite_imp_fold_graph])

lemma fold_graph_Or⇩_n:
  "finite Φ ⟹ fold_graph Or_ltln False_ltln Φ (Or⇩_n Φ)"
  unfolding Or⇩_n_def by (rule someI2_ex[OF finite_imp_fold_graph])

lemma Or⇩_n_empty[simp]:
  "Or⇩_n {} = False_ltln"
  by (metis empty_fold_graphE finite.emptyI fold_graph_Or⇩_n)

lemma And⇩_n_empty[simp]:
  "And⇩_n {} = True_ltln"
  by (metis empty_fold_graphE finite.emptyI fold_graph_And⇩_n)

interpretation dnf_union_thms: Finite_Set.comp_fun_commute "λφ. (∪) (f φ)"
  by unfold_locales fastforce

interpretation dnf_product_thms: Finite_Set.comp_fun_commute "λφ. (⊗) (f φ)"
  by unfold_locales (simp add: product_set_thms.comp_fun_commute)

― ‹Copied from locale @{locale comp_fun_commute}›
lemma fold_graph_finite:
  assumes "fold_graph f z A y"
  shows "finite A"
  using assms by induct simp_all


text ‹Taking the DNF of @{const And⇩_n} and @{const Or⇩_n} is the same as folding over the individual DNFs.›

lemma And⇩_n_dnf:
  "finite Φ ⟹ dnf (And⇩_n Φ) = Finite_Set.fold (λφ. (⊗) (dnf φ)) {{||}} Φ"
proof (drule fold_graph_And⇩_n, induction rule: fold_graph.induct)
  case (insertI x A y)

  then have "finite A"
    using fold_graph_finite by fast

  then show ?case
    using insertI by auto
qed simp

lemma Or⇩_n_dnf:
  "finite Φ ⟹ dnf (Or⇩_n Φ) = Finite_Set.fold (λφ. (∪) (dnf φ)) {} Φ"
proof (drule fold_graph_Or⇩_n, induction rule: fold_graph.induct)
  case (insertI x A y)

  then have "finite A"
    using fold_graph_finite by fast

  then show ?case
    using insertI by auto
qed simp


text ‹@{const And⇩_n} and @{const Or⇩_n} are injective on finite sets.›

lemma And⇩_n_inj:
  "inj_on And⇩_n {s. finite s}"
proof (standard, simp)
  fix x y :: "'a ltln set"
  assume "finite x" and "finite y"

  then have 1: "fold_graph And_ltln True_ltln x (And⇩_n x)" and 2: "fold_graph And_ltln True_ltln y (And⇩_n y)"
    using fold_graph_And⇩_n by blast+

  assume "And⇩_n x = And⇩_n y"

  with 1 show "x = y"
  proof (induction rule: fold_graph.induct)
    case emptyI
    then show ?case
      using 2 fold_graph.cases by force
  next
    case (insertI x A y)
    with 2 show ?case
    proof (induction arbitrary: x A y rule: fold_graph.induct)
      case (insertI x A y)
      then show ?case
        by (metis fold_graph.cases insertI1 ltln.distinct(7) ltln.inject(3))
    qed blast
  qed
qed

lemma Or⇩_n_inj:
  "inj_on Or⇩_n {s. finite s}"
proof (standard, simp)
  fix x y :: "'a ltln set"
  assume "finite x" and "finite y"

  then have 1: "fold_graph Or_ltln False_ltln x (Or⇩_n x)" and 2: "fold_graph Or_ltln False_ltln y (Or⇩_n y)"
    using fold_graph_Or⇩_n by blast+

  assume "Or⇩_n x = Or⇩_n y"

  with 1 show "x = y"
  proof (induction rule: fold_graph.induct)
    case emptyI
    then show ?case
      using 2 fold_graph.cases by force
  next
    case (insertI x A y)
    with 2 show ?case
    proof (induction arbitrary: x A y rule: fold_graph.induct)
      case (insertI x A y)
      then show ?case
        by (metis fold_graph.cases insertI1 ltln.distinct(27) ltln.inject(4))
    qed blast
  qed
qed


text ‹The semantics of @{const And⇩_n} and @{const Or⇩_n} can be expressed using quantifiers.›

lemma And⇩_n_semantics:
  "finite Φ ⟹ w ⊨⇩_n And⇩_n Φ ⟷ (∀φ ∈ Φ. 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_And⇩_n[OF ‹finite Φ›] by simp
qed

lemma Or⇩_n_semantics:
  "finite Φ ⟹ w ⊨⇩_n Or⇩_n Φ ⟷ (∃φ ∈ Φ. 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_Or⇩_n[OF ‹finite Φ›] by simp
qed

lemma And⇩_n_prop_semantics:
  "finite Φ ⟹ 𝒜 ⊨⇩_P And⇩_n Φ ⟷ (∀φ ∈ Φ. 𝒜 ⊨⇩_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_And⇩_n[OF ‹finite Φ›] by simp
qed

lemma Or⇩_n_prop_semantics:
  "finite Φ ⟹ 𝒜 ⊨⇩_P Or⇩_n Φ ⟷ (∃φ ∈ Φ. 𝒜 ⊨⇩_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_Or⇩_n[OF ‹finite Φ›] by simp
qed

lemma Or⇩_n_And⇩_n_image_semantics:
  assumes "finite 𝒜" and "⋀Φ. Φ ∈ 𝒜 ⟹ finite Φ"
  shows "w ⊨⇩_n Or⇩_n (And⇩_n ` 𝒜) ⟷ (∃Φ ∈ 𝒜. ∀φ ∈ Φ. w ⊨⇩_n φ)"
proof -
  have "w ⊨⇩_n Or⇩_n (And⇩_n ` 𝒜) ⟷ (∃Φ ∈ 𝒜. w ⊨⇩_n And⇩_n Φ)"
    using Or⇩_n_semantics assms by auto
  then show ?thesis
    using And⇩_n_semantics assms by fast
qed

lemma Or⇩_n_And⇩_n_image_prop_semantics:
  assumes "finite 𝒜" and "⋀Φ. Φ ∈ 𝒜 ⟹ finite Φ"
  shows "ℐ ⊨⇩_P Or⇩_n (And⇩_n ` 𝒜) ⟷ (∃Φ ∈ 𝒜. ∀φ ∈ Φ. ℐ ⊨⇩_P φ)"
proof -
  have "ℐ ⊨⇩_P Or⇩_n (And⇩_n ` 𝒜) ⟷ (∃Φ ∈ 𝒜. ℐ ⊨⇩_P And⇩_n Φ)"
    using Or⇩_n_prop_semantics assms by blast
  then show ?thesis
    using And⇩_n_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 𝒜 = Or⇩_n (And⇩_n ` fset ` 𝒜)"

lemma ltln_of_dnf_semantics:
  assumes "finite 𝒜"
  shows "w ⊨⇩_n ltln_of_dnf 𝒜 ⟷ (∃Φ ∈ 𝒜. ∀φ. φ |∈| Φ ⟶ w ⊨⇩_n φ)"
proof -
  have "w ⊨⇩_n ltln_of_dnf 𝒜 ⟷ (∃Φ ∈ fset ` 𝒜. ∀φ ∈ Φ. w ⊨⇩_n φ)"
    unfolding ltln_of_dnf_def
  proof (rule Or⇩_n_And⇩_n_image_semantics)
    show "finite (fset ` 𝒜)"
      using assms by blast
  next
    show "⋀Φ. Φ ∈ fset ` 𝒜 ⟹ finite Φ"
      by auto
  qed

  then show ?thesis
    by (metis image_iff)
qed

lemma ltln_of_dnf_prop_semantics:
  assumes "finite 𝒜"
  shows "ℐ ⊨⇩_P ltln_of_dnf 𝒜 ⟷ (∃Φ ∈ 𝒜. ∀φ. φ |∈| Φ ⟶ ℐ ⊨⇩_P φ)"
proof -
  have "ℐ ⊨⇩_P ltln_of_dnf 𝒜 ⟷ (∃Φ ∈ fset ` 𝒜. ∀φ ∈ Φ. ℐ ⊨⇩_P φ)"
    unfolding ltln_of_dnf_def
  proof (rule Or⇩_n_And⇩_n_image_prop_semantics)
    show "finite (fset ` 𝒜)"
      using assms by blast
  next
    show "⋀Φ. Φ ∈ fset ` 𝒜 ⟹ finite Φ"
      by auto
  qed

  then show ?thesis
    by (metis image_iff)
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 subset_eq)
  also have "… ⟷ 𝒜 ⊨⇩_P φ"
    using min_dnf_iff_prop_assignment_subset by blast
  finally show "𝒜 ⊨⇩_P ltln_of_dnf (min_dnf φ) = 𝒜 ⊨⇩_P φ" .
qed

lemma min_dnf_ltln_of_dnf[simp]:
  "min_dnf (ltln_of_dnf (min_dnf φ)) = min_dnf φ"
  using ltl_prop_equiv_min_dnf ltln_of_dnf_prop_equiv by blast


subsection ‹Substitution in DNF formulas›

definition subst_clause :: "'a ltln fset ⇒ ('a ltln ⇀ 'a ltln) ⇒ 'a ltln fset set"
where
  "subst_clause Φ m = ⨂⇩_m {min_dnf (subst φ m) | φ. φ ∈ fset Φ}"

definition subst_dnf :: "'a ltln fset set ⇒ ('a ltln ⇀ 'a ltln) ⇒ 'a ltln fset set"
where
  "subst_dnf 𝒜 m = (⋃Φ ∈ 𝒜. subst_clause Φ m)"

lemma subst_clause_empty[simp]:
  "subst_clause {||} m = {{||}}"
  by (simp add: subst_clause_def)

lemma subst_dnf_empty[simp]:
  "subst_dnf {} m = {}"
  by (simp add: subst_dnf_def)

lemma subst_clause_inner_finite:
  "finite {min_dnf (subst φ m) | φ. φ ∈ Φ}" if "finite Φ"
  using that by simp

lemma subst_clause_finite:
  "finite (subst_clause Φ m)"
  unfolding subst_clause_def
  by (auto intro: min_dnf_finite min_product_set_finite)

lemma subst_dnf_finite:
  "finite 𝒜 ⟹ finite (subst_dnf 𝒜 m)"
  unfolding subst_dnf_def using subst_clause_finite by blast

lemma subst_dnf_mono:
  "𝒜 ⊆ ℬ ⟹ subst_dnf 𝒜 m ⊆ subst_dnf ℬ m"
  unfolding subst_dnf_def by blast

lemma subst_clause_min_set[simp]:
  "min_set (subst_clause Φ m) = subst_clause Φ m"
  unfolding subst_clause_def by simp

lemma subst_clause_finsert[simp]:
  "subst_clause (finsert φ Φ) m = (min_dnf (subst φ m)) ⊗⇩_m (subst_clause Φ m)"
proof -
  have "{min_dnf (subst ψ m) | ψ. ψ ∈ fset (finsert φ Φ)}
    = insert (min_dnf (subst φ m)) {min_dnf (subst ψ m) | ψ. ψ ∈ fset Φ}"
    by auto

  then show ?thesis
    by (simp add: subst_clause_def)
qed

lemma subst_clause_funion[simp]:
  "subst_clause (Φ |∪| Ψ) m = (subst_clause Φ m) ⊗⇩_m (subst_clause Ψ m)"
proof (induction Ψ)
  case (insert x F)
  then show ?case
    using min_product_set_thms.fun_left_comm by fastforce
qed simp


text ‹For the proof of correctness, we redefine the @{const product} operator on lists.›

definition list_product :: "'a list set ⇒ 'a list set ⇒ 'a list set" (infixl ‹⊗⇩_l› 65)
where
  "A ⊗⇩_l B = {a @ b | a b. a ∈ A ∧ b ∈ B}"

lemma list_product_fset_of_list[simp]:
  "fset_of_list ` (A ⊗⇩_l B) = (fset_of_list ` A) ⊗ (fset_of_list ` B)"
  unfolding list_product_def product_def image_def by fastforce

lemma list_product_finite:
  "finite A ⟹ finite B ⟹ finite (A ⊗⇩_l B)"
  unfolding list_product_def by (simp add: finite_image_set2)

lemma list_product_iff:
  "x ∈ A ⊗⇩_l B ⟷ (∃a b. a ∈ A ∧ b ∈ B ∧ x = a @ b)"
  unfolding list_product_def by blast

lemma list_product_assoc[simp]:
  "A ⊗⇩_l (B ⊗⇩_l C) = A ⊗⇩_l B ⊗⇩_l C"
  unfolding set_eq_iff list_product_iff by fastforce


text ‹Furthermore, we introduct DNFs where the clauses are represented as lists.›

fun list_dnf :: "'a ltln ⇒ 'a ltln list set"
where
  "list_dnf true⇩_n = {[]}"
| "list_dnf false⇩_n = {}"
| "list_dnf (φ and⇩_n ψ) = (list_dnf φ) ⊗⇩_l (list_dnf ψ)"
| "list_dnf (φ or⇩_n ψ) = (list_dnf φ) ∪ (list_dnf ψ)"
| "list_dnf φ = {[φ]}"

definition list_dnf_to_dnf :: "'a list set ⇒ 'a fset set"
where
  "list_dnf_to_dnf X = fset_of_list ` X"

lemma list_dnf_to_dnf_list_dnf[simp]:
  "list_dnf_to_dnf (list_dnf φ) = dnf φ"
  by (induction φ) (simp_all add: list_dnf_to_dnf_def image_Un)

lemma list_dnf_finite:
  "finite (list_dnf φ)"
  by (induction φ) (simp_all add: list_product_finite)


text ‹We use this to redefine @{const subst_clause} and @{const subst_dnf} on list DNFs.›

definition subst_clause' :: "'a ltln list ⇒ ('a ltln ⇀ 'a ltln) ⇒ 'a ltln list set"
where
  "subst_clause' Φ m = fold (λφ acc. acc ⊗⇩_l list_dnf (subst φ m)) Φ {[]}"

definition subst_dnf' :: "'a ltln list set ⇒ ('a ltln ⇀ 'a ltln) ⇒ 'a ltln list set"
where
  "subst_dnf' 𝒜 m = (⋃Φ ∈ 𝒜. subst_clause' Φ m)"

lemma subst_clause'_finite:
  "finite (subst_clause' Φ m)"
  by (induction Φ rule: rev_induct) (simp_all add: subst_clause'_def list_dnf_finite list_product_finite)

lemma subst_clause'_nil[simp]:
  "subst_clause' [] m = {[]}"
  by (simp add: subst_clause'_def)

lemma subst_clause'_cons[simp]:
  "subst_clause' (xs @ [x]) m = subst_clause' xs m ⊗⇩_l list_dnf (subst x m)"
  by (simp add: subst_clause'_def)

lemma subst_clause'_append[simp]:
  "subst_clause' (A @ B) m = subst_clause' A m ⊗⇩_l subst_clause' B m"
proof (induction B rule: rev_induct)
  case (snoc x xs)
  then show ?case
    by simp (metis append_assoc subst_clause'_cons)
qed(simp add: list_product_def)


lemma subst_dnf'_iff:
  "x ∈ subst_dnf' A m ⟷ (∃Φ ∈ A. x ∈ subst_clause' Φ m)"
  by (simp add: subst_dnf'_def)

lemma subst_dnf'_product:
  "subst_dnf' (A ⊗⇩_l B) m = (subst_dnf' A m) ⊗⇩_l (subst_dnf' B m)" (is "?lhs = ?rhs")
proof (unfold set_eq_iff, safe)
  fix x
  assume "x ∈ ?lhs"

  then obtain Φ where "Φ ∈ A ⊗⇩_l B" and "x ∈ subst_clause' Φ m"
    unfolding subst_dnf'_iff by blast

  then obtain a b where "a ∈ A" and "b ∈ B" and "Φ = a @ b"
    unfolding list_product_def by blast

  then have "x ∈ (subst_clause' a m) ⊗⇩_l (subst_clause' b m)"
    using ‹x ∈ subst_clause' Φ m› by simp

  then obtain a' b' where "a' ∈ subst_clause' a m" and "b' ∈ subst_clause' b m" and "x = a' @ b'"
    unfolding list_product_iff by blast

  then have "a' ∈ subst_dnf' A m" and "b' ∈ subst_dnf' B m"
    unfolding subst_dnf'_iff using ‹a ∈ A› ‹b ∈ B› by auto

  then have "∃a∈subst_dnf' A m. ∃b∈subst_dnf' B m. x = a @ b"
    using ‹x = a' @ b'› by blast

  then show "x ∈ ?rhs"
    unfolding list_product_iff by blast
next
  fix x
  assume "x ∈ ?rhs"

  then obtain a b where "a ∈ subst_dnf' A m" and "b ∈ subst_dnf' B m" and "x = a @ b"
    unfolding list_product_iff by blast

  then obtain a' b' where "a' ∈ A" and "b' ∈ B" and a: "a ∈ subst_clause' a' m" and b: "b ∈ subst_clause' b' m"
    unfolding subst_dnf'_iff by blast

  then have "x ∈ (subst_clause' a' m) ⊗⇩_l (subst_clause' b' m)"
    unfolding list_product_iff using ‹x = a @ b› by blast

  moreover

  have "a' @ b' ∈ A ⊗⇩_l B"
    unfolding list_product_iff using ‹a' ∈ A› ‹b' ∈ B› by blast

  ultimately show "x ∈ ?lhs"
    unfolding subst_dnf'_iff by force
qed

lemma subst_dnf'_list_dnf:
  "subst_dnf' (list_dnf φ) m = list_dnf (subst φ m)"
proof (induction φ)
  case (And_ltln φ1 φ2)
  then show ?case
    by (simp add: subst_dnf'_product)
qed (simp_all add: subst_dnf'_def subst_clause'_def list_product_def)


lemma min_set_Union:
  "finite X ⟹ min_set (⋃ (min_set ` X)) = min_set (⋃ X)" for X :: "'a fset set set"
  by (induction X rule: finite_induct) (force, metis Sup_insert image_insert min_set_min_union min_union_def)

lemma min_set_Union_image:
  "finite X ⟹ min_set (⋃x ∈ X. min_set (f x)) = min_set (⋃x ∈ X. f x)" for f :: "'b ⇒ 'a fset set"
proof -
  assume "finite X"

  then have *: "finite (f ` X)" by auto

  with min_set_Union show ?thesis
    unfolding image_image by fastforce
qed

lemma subst_clause_fset_of_list:
  "subst_clause (fset_of_list Φ) m = min_set (list_dnf_to_dnf (subst_clause' Φ m))"
  unfolding list_dnf_to_dnf_def subst_clause'_def
proof (induction Φ rule: rev_induct)
  case (snoc x xs)
  then show ?case
    by simp (metis (no_types, lifting) dnf_min_set list_dnf_to_dnf_def list_dnf_to_dnf_list_dnf min_product_comm min_product_def min_set_min_product(1))
qed simp

lemma min_set_list_dnf_to_dnf_subst_dnf':
  "finite X ⟹ min_set (list_dnf_to_dnf (subst_dnf' X m)) = min_set (subst_dnf (list_dnf_to_dnf X) m)"
  by (simp add: subst_dnf'_def subst_dnf_def subst_clause_fset_of_list list_dnf_to_dnf_def min_set_Union_image image_Union)

lemma subst_dnf_dnf:
  "min_set (subst_dnf (dnf φ) m) = min_dnf (subst φ m)"
  unfolding dnf_min_set
  unfolding list_dnf_to_dnf_list_dnf[symmetric]
  unfolding subst_dnf'_list_dnf[symmetric]
  unfolding min_set_list_dnf_to_dnf_subst_dnf'[OF list_dnf_finite]
  by simp


text ‹This is almost the lemma we need. However, we need to show that the same holds for @{term "min_dnf φ"}, too.›

lemma fold_product:
  "Finite_Set.fold (λx. (⊗) {{|x|}}) {{||}} (fset x) = {x}"
  by (induction x) (simp_all, simp add: product_singleton_singleton)

lemma fold_union:
  "Finite_Set.fold (λx. (∪) {x}) {} (fset x) = fset x"
  by (induction x) (simp_all add: comp_fun_idem_on.fold_insert_idem[OF comp_fun_idem_insert[unfolded comp_fun_idem_def']])

lemma fold_union_fold_product:
  assumes "finite X" and "⋀Ψ ψ. Ψ ∈ X ⟹ ψ ∈ fset Ψ ⟹ dnf ψ = {{|ψ|}}"
  shows "Finite_Set.fold (λx. (∪) (Finite_Set.fold (λφ. (⊗) (dnf φ)) {{||}} (fset x))) {} X = X" (is "?lhs = X")
proof -
  from assms have "?lhs = Finite_Set.fold (λx. (∪) (Finite_Set.fold (λφ. (⊗) {{|φ|}}) {{||}} (fset x))) {} X"
  proof (induction X rule: finite_induct)
    case (insert Φ X)

    from insert.prems have 1: "⋀Ψ ψ. ⟦Ψ ∈ X; ψ ∈ fset Ψ⟧ ⟹ dnf ψ = {{|ψ|}}"
      by force

    from insert.prems have "Finite_Set.fold (λφ. (⊗) (dnf φ)) {{||}} (fset Φ) = Finite_Set.fold (λφ. (⊗) {{|φ|}}) {{||}} (fset Φ)"
      by (induction Φ) force+

    with insert 1 show ?case
      by simp
  qed simp

  with ‹finite X› show ?thesis
    unfolding fold_product by (metis fset_to_fset fold_union)
qed

lemma dnf_ltln_of_dnf_min_dnf:
  "dnf (ltln_of_dnf (min_dnf φ)) = min_dnf φ"
proof -
  have 1: "finite (And⇩_n ` fset ` min_dnf φ)"
    using min_dnf_finite by blast

  have 2: "inj_on And⇩_n (fset ` min_dnf φ)"
    by (metis (mono_tags, lifting) And⇩_n_inj f_inv_into_f fset inj_onI inj_on_contraD)

  have 3: "inj_on fset (min_dnf φ)"
    by (meson fset_inject inj_onI)

  show ?thesis
    unfolding ltln_of_dnf_def
    unfolding Or⇩_n_dnf[OF 1]
    unfolding fold_image[OF 2]
    unfolding fold_image[OF 3]
    unfolding comp_def
    unfolding And⇩_n_dnf[OF finite_fset]
    by (metis fold_union_fold_product min_dnf_finite min_dnf_atoms_dnf)
qed

lemma min_dnf_subst:
  "min_set (subst_dnf (min_dnf φ) m) = min_dnf (subst φ m)" (is "?lhs = ?rhs")
proof -
  let ?φ' = "ltln_of_dnf (min_dnf φ)"

  have "?lhs = min_set (subst_dnf (dnf ?φ') m)"
    unfolding dnf_ltln_of_dnf_min_dnf ..

  also have "… = min_dnf (subst ?φ' m)"
    unfolding subst_dnf_dnf ..

  also have "… = min_dnf (subst φ m)"
    using ltl_prop_equiv_min_dnf ltln_of_dnf_prop_equiv subst_respects_ltl_prop_entailment(2) by blast

  finally show ?thesis .
qed

end