# Theory Refutations

```(*
Title:  Refutations and Maximal Consistent Sets
Author: Asta Halkjær From
*)

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