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: "ymin_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. xA. 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. xaA  {y  B. xB. 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)

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 φ1 m 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 φ1 m 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 φ1 m 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)

  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 "w n ltln_of_dnf 𝒜  (Φ  fset ` 𝒜. φ  Φ. w n φ)"
    unfolding ltln_of_dnf_def
  proof (rule Orn_Andn_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 Orn_Andn_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 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 "asubst_dnf' A m. bsubst_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 (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