# Theory Refutations

chapter ‹Refutations›
theory Refutations imports Maximal_Consistent_Sets begin
section ‹Rearranging Refutations›
locale Refutations =
fixes refute :: ‹'a list ⇒ bool›
assumes refute_struct: ‹⋀A B. refute A ⟹ set A ⊆ set B ⟹ refute B›
begin
theorem refute_split:
assumes ‹set A ⊆ set B ∪ X› ‹refute A›
shows ‹∃C. set C ⊆ X ∧ refute (B @ C)›
using struct_split[where P=refute] refute_struct assms by blast
corollary refute_split1:
assumes ‹set A ⊆ {q} ∪ X› ‹refute A›
shows ‹∃C. set C ⊆ X ∧ refute (q # C)›
using assms refute_split[where B=‹[q]›] by simp
end
section ‹MCSs and Refutability›
locale Refutations_MCS = Refutations + MCS_Base +
assumes consistent_refute: ‹⋀S. consistent S = (∄S'. set S' ⊆ S ∧ refute S')›
begin
theorem MCS_refute:
assumes ‹consistent S› ‹maximal S›
shows ‹p ∉ S ⟷ (∃S'. set S' ⊆ S ∧ refute (p # S'))›
proof
assume ‹p ∉ S›
then show ‹∃S'. set S' ⊆ S ∧ refute (p # S')›
using assms refute_split1 consistent_refute unfolding maximal_def by metis
next
assume ‹∃S'. set S' ⊆ S ∧ refute (p # S')›
then show ‹p ∉ S›
using assms consistent_refute by fastforce
qed
end
end