# Theory Disjunction

```theory Disjunction
imports
Formula
Validity
begin

section ‹Disjunction›

definition Disj :: "('idx,'pred::fs,'act::bn) formula set['idx] ⇒ ('idx,'pred,'act) formula" where
"Disj xset = Not (Conj (map_bset Not xset))"

lemma finite_supp_map_bset_Not [simp]:
assumes "finite (supp xset)"
shows "finite (supp (map_bset Not xset))"
proof -
have "eqvt map_bset" and "eqvt Not"
then have "supp (map_bset Not) = {}"
using supp_fun_eqvt supp_fun_app_eqvt by blast
then have "supp (map_bset Not xset) ⊆ supp xset"
using supp_fun_app by blast
with assms show "finite (supp (map_bset Not xset))"
by (metis finite_subset)
qed

lemma Disj_eqvt [simp]:
assumes "finite (supp xset)"
shows "p ∙ Disj xset = Disj (p ∙ xset)"
using assms unfolding Disj_def by simp

lemma Disj_eq_iff [simp]:
assumes "finite (supp xset1)" and "finite (supp xset2)"
shows "Disj xset1 = Disj xset2 ⟷ xset1 = xset2"
using assms unfolding Disj_def by (metis Conj_eq_iff Not_eq_iff bset.inj_map_strong finite_supp_map_bset_Not)

context nominal_ts
begin

lemma valid_Disj [simp]:
assumes "finite (supp xset)"
shows "P ⊨ Disj xset ⟷ (∃x∈set_bset xset. P ⊨ x)"
using assms by (simp add: Disj_def map_bset.rep_eq)

end

end
```