Theory Refutations

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

chapter ‹Refutations›

theory Refutations imports Maximal_Consistent_Sets begin

lemma split_finite_sets:
  assumes ‹finite A› ‹finite B›
    and ‹A ⊆ B ∪ S›
  shows ‹∃B' C. finite C ∧ A = B' ∪ C ∧ B' = A ∩ B ∧ C ⊆ S›
  using assms subset_UnE by auto

lemma split_list:
  assumes ‹set A ⊆ set B ∪ S›
  shows ‹∃B' C. set (B' @ C) = set A ∧ set B' = set A ∩ set B ∧ set C ⊆ S›
  using assms split_finite_sets[where A=‹set A› and B=‹set B› and S=S]
  by (metis List.finite_set finite_Un finite_list set_append)

section ‹Rearranging Refutations›

locale Refutations =
  fixes refute :: ‹'fm list ⇒ bool›
  assumes refute_set: ‹⋀A B. refute A ⟹ set A = set B ⟹ refute B›
begin

theorem refute_split:
  assumes ‹set A ⊆ set B ∪ X› ‹refute A›
  shows ‹∃B' C. set B' = set A ∩ set B ∧ set C ⊆ X ∧ refute (B' @ C)›
  using assms refute_set split_list[where A=A and B=B] by metis

corollary refute_split1:
  assumes ‹set A ⊆ {q} ∪ X› ‹refute A› ‹q ∈ set A›
  shows ‹∃C. set C ⊆ X ∧ refute (q # C)›
  using assms refute_split[where A=A and X=X and B=‹[q]›] refute_set by auto

end

section ‹MCSs and Refutability›

locale Refutations_MCS = MCS_Base + Refutations +
  assumes consistent_refute: ‹⋀S. consistent S ⟷ (∀A. set A ⊆ S ⟶ ¬ refute A)›
begin

theorem MCS_refute:
  assumes ‹consistent S› ‹maximal S›
  shows ‹p ∉ S ⟷ (∃A. set A ⊆ S ∧ refute (p # A))›
proof safe
  assume ‹p ∉ S›
  then obtain B where B: ‹set B ⊆ {p} ∪ S› ‹p ∈ set B› ‹refute B›
    using assms unfolding consistent_refute maximal_def by blast
  moreover have ‹set (p # removeAll p B) = set B›
    using B(2) by auto
  ultimately have ‹refute (p # removeAll p B)›
    using refute_set by metis
  then show ‹∃A. set A ⊆ S ∧ refute (p # A)›
    using B(1) by (metis Diff_subset_conv set_removeAll)
next
  fix A
  assume ‹set A ⊆ S› ‹refute (p # A)› ‹p ∈ S›
  then show False
    using assms unfolding consistent_refute
    by (metis (no_types, lifting) insert_subsetI list.simps(15))
qed

end

end