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_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 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:
  "Φ ∈ dnf φ ⟹ fset Φ ⊆ prop_atoms φ"
  by (induction φ arbitrary: Φ) (auto simp: product_def, blast+)

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 φ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 Orn_empty[simp]:
  "Orn {} = False_ltln"
  by (metis empty_fold_graphE finite.emptyI fold_graph_Orn)

lemma Andn_empty[simp]:
  "Andn {} = True_ltln"
  by (metis empty_fold_graphE finite.emptyI fold_graph_Andn)

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 Andn} and @{const Orn} is the same as folding over the individual DNFs.›

lemma Andn_dnf:
  "finite Φ ⟹ dnf (Andn Φ) = Finite_Set.fold (λφ. (⊗) (dnf φ)) {{||}} Φ"
proof (drule fold_graph_Andn, 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 Orn_dnf:
  "finite Φ ⟹ dnf (Orn Φ) = Finite_Set.fold (λφ. (∪) (dnf φ)) {} Φ"
proof (drule fold_graph_Orn, 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 Andn} and @{const Orn} are injective on finite sets.›

lemma Andn_inj:
  "inj_on Andn {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 (Andn x)" and 2: "fold_graph And_ltln True_ltln y (Andn y)"
    using fold_graph_Andn by blast+

  assume "Andn x = Andn 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 Orn_inj:
  "inj_on Orn {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 (Orn x)" and 2: "fold_graph Or_ltln False_ltln y (Orn y)"
    using fold_graph_Orn by blast+

  assume "Orn x = Orn 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 Andn} and @{const Orn} can be expressed using quantifiers.›

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

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 truen = {[]}"
| "list_dnf falsen = {}"
| "list_dnf (φ andn ψ) = (list_dnf φ) ⊗l (list_dnf ψ)"
| "list_dnf (φ orn ψ) = (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 add: notin_fset, simp add: product_singleton_singleton)

lemma fold_union:
  "Finite_Set.fold (λx. (∪) {x}) {} (fset x) = fset x"
  by (induction x) (simp_all add: notin_fset comp_fun_idem.fold_insert_idem comp_fun_idem_insert)

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 simp: notin_fset)+

    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 (Andn ` fset ` min_dnf φ)"
    using min_dnf_finite by blast

  have 2: "inj_on Andn (fset ` min_dnf φ)"
    by (metis (mono_tags, lifting) Andn_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 Orn_dnf[OF 1]
    unfolding fold_image[OF 2]
    unfolding fold_image[OF 3]
    unfolding comp_def
    unfolding Andn_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