# Theory LTL.Disjunctive_Normal_Form

```(*
Author:   Benedikt Seidl
Author:   Salomon Sickert
*)

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)"

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"

lemma product_empty[simp]:
"A ⊗ {} = {}"
"{} ⊗ A = {}"

lemma min_product_empty[simp]:
"A ⊗⇩m {} = {}"
"{} ⊗⇩m A = {}"

lemma min_union_empty[simp]:
"A ∪⇩m {} = min_set A"
"{} ∪⇩m A = min_set A"

lemma product_empty_singleton[simp]:
"A ⊗ {{||}} = A"
"{{||}} ⊗ A = A"

lemma min_product_empty_singleton[simp]:
"A ⊗⇩m {{||}} = min_set A"
"{{||}} ⊗⇩m A = min_set A"

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)"

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)"

lemma product_set_infinite[simp]:
"infinite X ⟹ ⨂ X = {{||}}"

lemma min_product_set_infinite[simp]:
"infinite X ⟹ ⨂⇩m X = {{||}}"

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

lemma min_union_comm:
"A ∪⇩m B = B ∪⇩m A"
unfolding min_union_def

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]

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"

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"

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

lemma product_set_empty[simp]:
"⨂ {} = {{||}}"
"⨂ {{}} = {}"
"⨂ {{{||}}} = {{||}}"

lemma min_product_set_empty[simp]:
"⨂⇩m {} = {{||}}"
"⨂⇩m {{}} = {}"
"⨂⇩m {{{||}}} = {{||}}"

lemma product_set_code[code]:
"⨂ (set xs) = fold product (remdups xs) {{||}}"

lemma min_product_set_code[code]:
"⨂⇩m (set xs) = fold min_product (remdups xs) {{||}}"

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"

lemma min_union_min_set[simp]:
"min_set (A ∪⇩m B) = A ∪⇩m B"

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 φ"

lemma min_dnf_Abs_fset[simp]:
"fset (Abs_fset (min_dnf φ)) = min_dnf φ"

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 B⇩1 B⇩2 where 1: "fset B⇩1 ⊆ 𝒜 ∧ B⇩1 ∈ min_dnf φ⇩1" and 2: "fset B⇩2 ⊆ 𝒜 ∧ B⇩2 ∈ min_dnf φ⇩2"
by fastforce

then obtain C where "C |⊆| B⇩1 |∪| B⇩2" 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

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 φ)"

― ‹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 = {{||}}"

lemma subst_dnf_empty[simp]:
"subst_dnf {} m = {}"

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
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 = {[]}"

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

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)

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

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
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
```