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