# Theory Derivations

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

chapter ‹Derivations›

theory Derivations imports Maximal_Consistent_Sets begin

section ‹Rearranging Assumptions›

locale Derivations =
fixes derive :: ‹'a list ⇒ 'a ⇒ bool›
assumes derive_struct: ‹⋀A B p. derive A p ⟹ set A ⊆ set B ⟹ derive B p›
begin

theorem derive_split:
assumes ‹set A ⊆ set B ∪ X› ‹derive A p›
shows ‹∃C. set C ⊆ X ∧ derive (B @ C) p›
using struct_split[where P=‹λA. derive A p›] derive_struct assms by blast

corollary derive_split1:
assumes ‹set A ⊆ {q} ∪ X› ‹derive A p›
shows ‹∃C. set C ⊆ X ∧ derive (q # C) p›
using assms derive_split[where B=‹[q]›] by simp

end

section ‹MCSs and Deriving Falsity›

locale Derivations_MCS = Derivations + MCS_Base +
fixes fls
assumes consistent_derive_fls: ‹⋀S. consistent S = (∄S'. set S' ⊆ S ∧ derive S' fls)›
begin

theorem MCS_derive_fls:
assumes ‹consistent S› ‹maximal S›
shows ‹p ∉ S ⟷ (∃S'. set S' ⊆ S ∧ derive (p # S') fls)›
proof
assume ‹p ∉ S›
then show ‹∃S'. set S' ⊆ S ∧ derive (p # S') fls›
using assms derive_split1 consistent_derive_fls unfolding maximal_def by metis
next
assume ‹∃S'. set S' ⊆ S ∧ derive (p # S') fls›
then show ‹p ∉ S›
using assms consistent_derive_fls by fastforce
qed

end

section ‹MCSs and Derivability›

locale Derivations_MCS_Cut = Derivations_MCS +
assumes derive_assm: ‹⋀A p. p ∈ set A ⟹ derive A p›
and derive_cut: ‹⋀A B p q. derive A p ⟹ derive (p # B) q ⟹ derive (A @ B) q›
begin

theorem MCS_derive:
assumes ‹consistent S› ‹maximal S›
shows ‹p ∈ S ⟷ (∃S'. set S' ⊆ S ∧ derive S' p)›
proof
assume ‹p ∈ S›
then show ‹∃S'. set S' ⊆ S ∧ derive S' p›
using derive_assm by (metis List.set_insert empty_set empty_subsetI insert_subset singletonI)
next
assume ‹∃A. set A ⊆ S ∧ derive A p›
then obtain A where A: ‹set A ⊆ S› ‹derive A p›
by blast
have ‹consistent ({p} ∪ S)›
unfolding consistent_derive_fls
proof safe
fix B
assume B: ‹set B ⊆ {p} ∪ S› ‹derive B fls›
then obtain C where C: ‹derive (p # C) fls› ‹set C ⊆ S›
using derive_split1 by blast
then have ‹derive (A @ C) fls›
using A derive_cut by blast
then show False
using A(1) B(1) C assms(1) consistent_derive_fls by simp
qed
then show ‹p ∈ S›
using assms unfolding maximal_def by auto
qed

end

end
```