Theory AGM_Logic

(*<*)
―‹ ******************************************************************** 
 * Project         : AGM Theory
 * Version         : 1.0
 *
 * Authors         : Valentin Fouillard, Safouan Taha, Frederic Boulanger
                     and Nicolas Sabouret
 *
 * This file       : AGM logics
 *
 * Copyright (c) 2021 Université Paris Saclay, France
 *
 ******************************************************************************›

theory AGM_Logic

imports Main

begin
(*>*)

section ‹Introduction›

text‹
The 1985 paper by Carlos Alchourrón, Peter Gärdenfors,
and David Makinson (AGM), ``On the Logic of Theory Change: Partial Meet
Contraction and Revision Functions'' \<^cite>‹"alchourron1985logic"› launches a large and
rapidly growing literature that employs formal models and logics to handle changing beliefs of a rational agent
and to take into account new piece of information observed by this agent. 
In 2011, a review book titled "AGM 25 Years: Twenty-Five Years of Research in Belief Change"
was edited to summarize the first twenty five years of works based on AGM 
\<^cite>‹"Ferme2011"›.

According to Google Scholar, the original AGM paper was cited 4000 times! 
This AFP entry is HOL-based and it is a faithful formalization of the logic operators (e.g. contraction, revision, remainder \dots )
axiomatized in the AGM paper. It also contains the proofs of all the theorems stated in the paper that show how these operators combine.
Both proofs of Harper and Levi identities are established.
›

text‹A belief state can be considered as a consistent set of beliefs (logical propositions) closed under logical reasoning.
Belief changes represent the operations that apply on a belief state to remove some of it and/or to add new beliefs (propositions). 
In the latter case, it is possible that other beliefs are affected by these changes (to preserve consistency for example). 
AGM define several postulates to guarantee that such operations preserve consistency meaning that the agent keeps rational. 
Three kinds of operators are defined :
▪ The contraction @{text ‹÷›} : where a proposition is removed from a belief set
▪ The expansion @{text ‹⊕›} : where a proposition is added to a belief set
▪ The revision @{text ‹❙*›} : where a proposition is added to a belief set such that the belief set remains consistent
›

text‹In this AFP entry, there are three theory files: 
▸ The AGM Logic file contains a classification of logics used in the AGM framework.
▸ The AGM Remainder defines a important operator used in the AGM framework.
▸ The AGM Contraction file contains the postulates of the AGM contraction and its relation with the meet contraction.
▸ The AGM Revision file contains the postulates of the AGM revision and its relation with the meet revision.  
›

section ‹Logics›

text‹The AGM framework depends on the underlying logic used to express beliefs. AGM requires at least a Tarskian propositional calculus. 
If this logic is also supra-classical and/or compact, new properties are established and the main theorems of AGM are strengthened. 
To model AGM it is therefore important to start by formalizing this underlying logic and its various extensions. 
We opted for a deep embedding in HOL which required the redefinition of all the logical operators and an axiomatization of their rules. 
This is certainly not efficient in terms of proof but it gives a total control of our formalization and an assurance 
that the logic used has no hidden properties depending on the Isabelle/HOL implementation. 
We use the Isabelle ∗‹locales› feature and we take advantage of the inheritance/extension mechanisms between locales.›


subsection ‹Tarskian Logic›

text ‹
The first locale formalizes a Tarskian logic based on the famous Tarski's consequence operator: @{term ‹Cn(A)›} 
which gives the set of all propositions (❙‹closure›) that can be inferred from the set of propositions @{term ‹A›}, 
Exactly as it is classically axiomatized in the literature, three assumptions of the locale define the consequence operator.
›
locale Tarskian_logic =
fixes Cn::‹'a set ⇒ 'a set›
assumes monotonicity_L:     ‹A ⊆ B ⟹ Cn(A) ⊆ Cn(B)›
    and inclusion_L:        ‹A ⊆ Cn(A)› 
    and transitivity_L:     ‹Cn(Cn(A)) ⊆ Cn(A)›

― ‹
  Short notation for ``@{term ‹φ›} can be inferred from the propositions in @{term ‹A›}''.
›
fixes infer::‹'a set ⇒ 'a ⇒ bool›  (infix ‹⊢› 50)
defines ‹A ⊢ φ ≡ φ ∈ Cn(A)›

― ‹
  @{term ‹φ›} is valid (a tautology) if it can be inferred from nothing.
›
fixes valid::‹'a ⇒ bool›            (‹⊩›)
defines ‹⊩ φ ≡ {} ⊢ φ›

― ‹
  @{term ‹A ⊕ φ›} is all that can be infered from  @{term ‹A›} and  @{term ‹φ›}.
›
fixes expansion::‹'a set ⇒ 'a ⇒ 'a set› (infix ‹⊕› 57)
defines ‹A ⊕ φ ≡ Cn(A ∪ {φ})›

begin 

lemma idempotency_L: ‹Cn(Cn(A)) = Cn(A)›
  by (simp add: inclusion_L transitivity_L subset_antisym)

lemma assumption_L: ‹φ ∈ A ⟹ A ⊢ φ›
  using inclusion_L infer_def by blast 

lemma validD_L: ‹⊩ φ ⟹ φ ∈ Cn(A)›
  using monotonicity_L valid_def infer_def by fastforce

lemma valid_expansion: ‹K = Cn(A) ⟹ ⊩ φ ⟹ K ⊕ φ = K›
  by (simp add: idempotency_L insert_absorb validD_L valid_def expansion_def)

lemma transitivity2_L:
  assumes ‹∀φ ∈ B. A ⊢ φ›
      and ‹B ⊢ ψ›
    shows ‹A ⊢ ψ›
proof -
  from assms(1) have ‹B ⊆ Cn(A)› by (simp add: infer_def subsetI)
  hence ‹Cn(B) ⊆ Cn(A)›  using idempotency_L monotonicity_L by blast
  moreover from assms(2) have ‹ψ ∈ Cn(B)› by (simp add: infer_def)
  ultimately show ?thesis using infer_def by blast
qed

lemma Cn_same: ‹(Cn(A) = Cn(B)) ⟷ (∀C. A ⊆ Cn(C) ⟷ B ⊆ Cn(C))›
proof
  { assume h:‹Cn(A) = Cn(B)›
    from h have ‹∀φ ∈ B. A ⊢ φ› 
      by (simp add: Tarskian_logic.assumption_L Tarskian_logic_axioms infer_def)
    moreover from h[symmetric] have ‹∀φ ∈ A. B ⊢ φ›
      by (simp add: Tarskian_logic.assumption_L Tarskian_logic_axioms infer_def)
    ultimately have ‹∀C. A ⊆ Cn(C) ⟷ B ⊆ Cn(C)›
      using h idempotency_L inclusion_L monotonicity_L by blast
  } thus ‹Cn(A) = Cn(B) ⟹ ∀C. (A ⊆ Cn(C)) = (B ⊆ Cn(C))› .
next
  { assume h:‹∀C. (A ⊆ Cn(C)) = (B ⊆ Cn(C))›
    from h have ‹(A ⊆ Cn(A)) = (B ⊆ Cn(A))› and ‹(A ⊆ Cn(B)) = (B ⊆ Cn(B))› by simp+
    hence ‹B ⊆ Cn(A)› and ‹A ⊆ Cn(B)› by (simp add: inclusion_L)+
    hence ‹Cn(A) = Cn(B)›
      using idempotency_L monotonicity_L by blast
  } thus ‹(∀C. (A ⊆ Cn(C)) = (B ⊆ Cn(C))) ⟹ Cn(A) = Cn(B)› .
qed

― ‹
The closure of the union of two consequence closures.
›
lemma Cn_union: ‹Cn(Cn(A) ∪ Cn(B)) = Cn(A ∪ B)›
proof
  have ‹Cn(Cn(A) ∪ Cn(B)) ⊆ Cn(Cn (A ∪ B))› by (simp add: monotonicity_L)
  thus ‹Cn(Cn(A) ∪ Cn(B)) ⊆ Cn(A ∪ B)› by (simp add: idempotency_L)
next
  have ‹(A ∪ B) ⊆ (Cn(A) ∪ Cn(B))› using inclusion_L by blast
  thus ‹Cn(A ∪ B) ⊆ Cn(Cn(A) ∪ Cn(B))› by (simp add: monotonicity_L)
qed

― ‹
The closure of an infinite union of consequence closures.
›
lemma Cn_Union: ‹Cn(⋃{Cn(B)|B. P B}) = Cn(⋃{B. P B})› (is ‹?A = ?B›)
proof
  have ‹?A ⊆ Cn ?B›
    apply(rule monotonicity_L, rule Union_least, auto) 
    by (metis Sup_upper in_mono mem_Collect_eq monotonicity_L)
  then show ‹?A ⊆ ?B›
    by (simp add: idempotency_L)
next
  show ‹?B ⊆ ?A› 
    by (metis (mono_tags, lifting) Union_subsetI inclusion_L mem_Collect_eq monotonicity_L)
qed

― ‹
The intersection of two closures is closed.
›
lemma Cn_inter: ‹K = Cn(A) ∩ Cn(B) ⟹ K = Cn(K)›
proof -
  { fix K assume h:‹K = Cn(A) ∩ Cn(B)›
    from h have ‹K ⊆ Cn(A)› and ‹K ⊆ Cn(B)› by simp+
    hence ‹Cn(K) ⊆ Cn(A)› and ‹Cn(K) ⊆ Cn(B)› using idempotency_L monotonicity_L by blast+
    hence ‹Cn(K) ⊆ Cn(A) ∩ Cn(B)› by simp
    with h have ‹K = Cn(K)› by (simp add: inclusion_L subset_antisym)
  } thus ‹K = Cn(A) ∩ Cn(B) ⟹ K = Cn(K)› .
qed

― ‹
An infinite intersection of closures is closed.
›
lemma Cn_Inter: ‹K = ⋂{Cn(B)|B. P B} ⟹ K = Cn(K)›
proof -
  { fix K assume h:‹K = ⋂{Cn(B)|B. P B}›
    from h have ‹∀B. P B ⟶ K ⊆ Cn(B)› by blast
    hence ‹∀B. P B ⟶ Cn(K) ⊆ Cn(B)› using idempotency_L monotonicity_L by blast
    hence ‹Cn(K) ⊆ ⋂{Cn(B)|B. P B}› by blast
    with h have ‹K = Cn(K)› by (simp add: inclusion_L subset_antisym)
  } thus ‹K = ⋂{Cn(B)|B. P B} ⟹ K = Cn(K)› .
qed

end

subsection ‹Supraclassical Logic›

text ‹
A Tarskian logic has only one abstract operator catching the notion of consequence. A basic case of such a logic is a ❙‹Supraclassical› logic that 
is a logic with all classical propositional operators (e.g. conjunction (‹∧›), implication(‹⟶›), negation (‹¬›) \dots ) together with their classical semantics.

We define a new locale. In order to distinguish the propositional operators of our supraclassical logic from those of Isabelle/HOL, we use dots (e.g. ‹.∧.› stands for conjunction). 
We axiomatize the introduction and elimination rules of each operator as it is commonly established in the classical literature. As explained before, 
we give priority to a complete control of our logic instead of an efficient shallow embedding in Isabelle/HOL.
›

locale Supraclassical_logic = Tarskian_logic +

fixes true_PL::   ‹'a›             (‹⊤›)
  and false_PL::  ‹'a›             (‹⊥›)
  and imp_PL::    ‹'a ⇒ 'a ⇒ 'a› (infix ‹.⟶.› 55)
  and not_PL::    ‹'a ⇒ 'a›       (‹.¬›)  
  and conj_PL::   ‹'a ⇒ 'a ⇒ 'a› (infix ‹.∧.› 55)
  and disj_PL::   ‹'a ⇒ 'a ⇒ 'a› (infix ‹.∨.› 55)
  and equiv_PL::  ‹'a ⇒ 'a ⇒ 'a› (infix ‹.⟷.› 55)

assumes true_PL:     ‹A ⊢ ⊤›

    and false_PL:    ‹{⊥} ⊢ p›

    and impI_PL:     ‹A ∪ {p} ⊢ q ⟹ A ⊢ (p .⟶. q)›
    and mp_PL:       ‹A ⊢ p .⟶. q ⟹ A ⊢ p ⟹ A ⊢ q›

    and notI_PL:     ‹A ⊢ p .⟶. ⊥ ⟹ A ⊢ .¬ p›
    and notE_PL:     ‹A ⊢ .¬ p ⟹ A ⊢ (p .⟶. ⊥)›

    and conjI_PL:    ‹A ⊢ p ⟹ A ⊢ q ⟹ A ⊢ (p .∧. q)›
    and conjE1_PL:   ‹A ⊢ p .∧. q ⟹ A ⊢ p›
    and conjE2_PL:   ‹A ⊢ p .∧. q ⟹ A ⊢ q›

    and disjI1_PL:   ‹A ⊢ p ⟹ A ⊢ (p .∨. q)›
    and disjI2_PL:   ‹A ⊢ q ⟹ A ⊢ (p .∨. q)›
    and disjE_PL:    ‹A ⊢ p .∨. q ⟹ A ⊢ p .⟶. r ⟹ A ⊢ q.⟶. r ⟹ A ⊢ r›

    and equivI_PL:   ‹A ⊢ p .⟶. q ⟹ A ⊢ q .⟶. p ⟹ A ⊢ (p .⟷. q)›
    and equivE1_PL:  ‹A ⊢ p .⟷. q ⟹ A ⊢ p .⟶. q›
    and equivE2_PL:  ‹A ⊢ p .⟷. q ⟹ A ⊢ q .⟶. p›

― ‹non intuitionistic rules›
    and absurd_PL:   ‹A ⊢ .¬ (.¬ p) ⟹ A ⊢ p›
    and ex_mid_PL:   ‹A ⊢ p .∨. (.¬ p)›

begin 

text ‹In the following, we will first retrieve the classical logic operators semantics coming from previous introduction and elimination rules›

lemma non_consistency:
  assumes ‹A ⊢ .¬ p›
      and ‹A ⊢ p›
    shows ‹A ⊢ q›
  by (metis assms(1) assms(2) false_PL mp_PL notE_PL singleton_iff transitivity2_L)

― ‹this direct result brings directly many remarkable properties of implication (i.e. transitivity)›
lemma imp_PL: ‹A ⊢ p .⟶. q ⟷ A ∪ {p} ⊢ q›
  apply (intro iffI impI_PL)
   apply(rule mp_PL[where p=p], meson UnI1 assumption_L transitivity2_L)
  using assumption_L by auto

lemma not_PL: ‹A ⊢ .¬ p ⟷ A ∪ {p} ⊢ ⊥›
  using notE_PL notI_PL imp_PL by blast

― ‹Classical logic result›
lemma notnot_PL: ‹A ⊢ .¬ (.¬ p) ⟷ A ⊢ p›
  apply(rule iffI, simp add:absurd_PL) 
  by (meson mp_PL notE_PL Un_upper1 Un_upper2 assumption_L infer_def monotonicity_L not_PL singletonI subsetD)

lemma conj_PL: ‹A ⊢ p .∧. q ⟷ (A ⊢ p ∧ A ⊢ q)›
  using conjE1_PL conjE2_PL conjI_PL by blast 

lemma disj_PL: ‹A ⊢ p .∨. q ⟷ A ∪ {.¬ p} ⊢ q›
proof
  assume a:‹A ⊢ p .∨. q›
  have b:‹A ⊢ p .⟶. (.¬ p .⟶. q)› 
    by (intro impI_PL) (meson Un_iff assumption_L insertI1 non_consistency)
  have c:‹A ⊢ q .⟶. (.¬ p .⟶. q)› 
    by (simp add: assumption_L impI_PL)
  from a b c have ‹A ⊢ .¬ p .⟶. q›
    by (erule_tac disjE_PL) simp_all
  then show ‹A ∪ {.¬ p} ⊢ q› 
    using imp_PL by blast
next 
  assume a:‹A ∪ {.¬ p} ⊢ q›
  hence b:‹A ⊢ .¬ p .⟶. q› by (simp add: impI_PL)
  then show ‹A ⊢ p .∨. q› 
    apply(rule_tac disjE_PL[OF ex_mid_PL, of A p ‹p .∨. q›]) 
    by (auto simp add: assumption_L disjI2_PL disjI1_PL impI_PL imp_PL) 
qed

lemma equiv_PL:‹A ⊢ p .⟷. q ⟷ (A ∪ {p} ⊢ q ∧ A ∪ {q} ⊢ p)›
  using imp_PL equivE1_PL equivE2_PL equivI_PL by blast

corollary valid_imp_PL:  ‹⊩ (p .⟶. q) = ({p} ⊢ q)›
      and valid_not_PL:  ‹⊩ (.¬ p) = ({p} ⊢ ⊥)›
      and valid_conj_PL: ‹⊩ (p .∧. q) = (⊩ p ∧ ⊩ q)›
      and valid_disj_PL: ‹⊩ (p .∨. q) = ({.¬ p} ⊢ q)›
      and valid_equiv_PL:‹⊩ (p .⟷. q) = ({p} ⊢ q ∧ {q} ⊢ p)›
  using imp_PL not_PL conj_PL disj_PL equiv_PL valid_def by auto

text‹Second, we will combine each logical operator with the consequence operator ‹Cn›: it is a trick to profit from set theory to get many essential 
lemmas without complex inferences›
declare infer_def[simp]

lemma nonemptyCn: ‹Cn(A) ≠ {}›
  using true_PL by auto

lemma Cn_true: ‹Cn({⊤}) = Cn({})›
  using Cn_same true_PL by auto

lemma Cn_false: ‹Cn({⊥}) = UNIV› 
  using false_PL by auto

lemma Cn_imp:     ‹A ⊢ (p .⟶. q) ⟷ Cn({q}) ⊆ Cn(A ∪ {p})› 
  and Cn_imp_bis: ‹A ⊢ (p .⟶. q) ⟷ Cn(A ∪ {q}) ⊆ Cn(A ∪ {p})› 
  using Cn_same imp_PL idempotency_L inclusion_L infer_def subset_insertI by force+

lemma Cn_not: ‹A ⊢ .¬ p ⟷ Cn(A ∪ {p}) = UNIV›
  using Cn_false Cn_imp notE_PL not_PL by fastforce

lemma Cn_conj: ‹A ⊢ (p .∧. q) ⟷ Cn({p}) ∪ Cn({q}) ⊆ Cn(A)›
  apply(intro iffI conjI_PL, frule conjE1_PL, frule conjE2_PL) 
  using Cn_same Un_insert_right bot.extremum idempotency_L inclusion_L by auto

lemma Cn_conj_bis: ‹Cn({p .∧. q}) = Cn({p, q})› 
  by (unfold Cn_same)
     (meson Supraclassical_logic.conj_PL Supraclassical_logic_axioms insert_subset)

lemma Cn_disj:     ‹A ⊢ (p .∨. q) ⟷ Cn({q}) ⊆ Cn(A ∪ {.¬ p})›
  and Cn_disj_bis: ‹A ⊢ (p .∨. q) ⟷ Cn(A ∪ {q}) ⊆ Cn(A ∪ {.¬ p})›
  using disj_PL Cn_same imp_PL idempotency_L inclusion_L infer_def subset_insertI by force+

lemma Cn_equiv: ‹A ⊢ (p .⟷. q) ⟷ Cn(A ∪ {p}) = Cn(A ∪ {q})›
  by (metis Cn_imp_bis equivE1_PL equivE2_PL equivI_PL set_eq_subset)

corollary valid_nonemptyCn: ‹Cn({}) ≠ {}›
      and valid_Cn_imp:     ‹⊩ (p .⟶. q) ⟷ Cn({q}) ⊆ Cn({p})› 
      and valid_Cn_not:     ‹⊩ (.¬ p) ⟷ Cn({p}) = UNIV›
      and valid_Cn_conj:    ‹⊩ (p .∧. q) ⟷ Cn({p}) ∪ Cn({q}) ⊆ Cn({})›
      and valid_Cn_disj:    ‹⊩ (p .∨. q) ⟷ Cn({q}) ⊆ Cn({.¬ p})›
      and valid_Cn_equiv:   ‹⊩ (p .⟷. q) ⟷ Cn({p}) = Cn({q})›
  using nonemptyCn Cn_imp Cn_not Cn_conj Cn_disj Cn_equiv valid_def by auto

― ‹Finally, we group additional lemmas that were essential in further proofs›
lemma consistency: ‹Cn({p}) ∩ Cn({.¬ p}) = Cn({})›
proof
  { fix q
    assume ‹{p} ⊢ q› and ‹{.¬ p} ⊢ q›
    hence "{} ⊢ p .⟶. q" and "{} ⊢ (.¬ p) .⟶. q" 
      using impI_PL by auto
    hence ‹{} ⊢ q› 
      using ex_mid_PL by (rule_tac disjE_PL[where p=p and q=‹.¬ p›]) blast   
  }
  then show ‹Cn({p}) ∩ Cn({.¬ p}) ⊆ Cn({})› by (simp add: subset_iff)
next
  show ‹Cn({}) ⊆ Cn({p}) ∩ Cn({.¬ p})› by (simp add: monotonicity_L)
qed

lemma Cn_notnot: ‹Cn({.¬ (.¬ φ)}) = Cn({φ})›
  by (metis (no_types, opaque_lifting) notnot_PL valid_Cn_equiv valid_equiv_PL)

lemma conj_com: ‹A ⊢ p .∧. q ⟷ A ⊢ q .∧. p›
  using conj_PL by auto

lemma conj_com_Cn: ‹Cn({p .∧. q}) = Cn({q .∧. p})›
  by (simp add: Cn_conj_bis insert_commute) 

lemma disj_com: ‹A ⊢ p .∨. q ⟷ A ⊢ q .∨. p›
proof -
  { fix p q
    have ‹A ⊢ p .∨. q ⟹ A ⊢ q .∨. p›
      apply(erule disjE_PL) 
      using assumption_L disjI2_PL disjI1_PL impI_PL by auto 
  }
  then show ?thesis by auto
qed

lemma disj_com_Cn: ‹Cn({p .∨. q}) = Cn({q .∨. p})›
  unfolding Cn_same using disj_com by simp

lemma imp_contrapos: ‹A ⊢ p .⟶. q ⟷ A ⊢ .¬ q .⟶. .¬ p›
  by (metis Cn_not Un_insert_left Un_insert_right imp_PL notnot_PL)

lemma equiv_negation: ‹A ⊢ p .⟷. q ⟷ A ⊢ .¬ p .⟷. .¬ q›
  using equivE1_PL equivE2_PL equivI_PL imp_contrapos by blast

lemma imp_trans: ‹A ⊢ p .⟶.q ⟹ A ⊢ q .⟶.r ⟹ A ⊢ p .⟶.r›
  using Cn_imp_bis by auto

lemma imp_recovery0: ‹A ⊢ p .∨. (p .⟶. q)›
  apply(subst disj_PL, subst imp_contrapos)
  using assumption_L impI_PL by auto

lemma imp_recovery1: ‹A ∪ {p .⟶. q} ⊢ p ⟹ A ⊢ p›
  using disjE_PL[OF imp_recovery0, of A p p q] assumption_L imp_PL by auto

lemma imp_recovery2: ‹A ⊢ p .⟶. q ⟹ A ⊢ (q .⟶. p) .⟶. p ⟹ A ⊢ q›
  using imp_PL imp_recovery1 imp_trans by blast

lemma impI2: ‹A ⊢ q ⟹ A ⊢ p .⟶. q› 
  by (meson assumption_L impI_PL in_mono sup_ge1 transitivity2_L)

lemma conj_equiv: ‹A ⊢ p ⟹ A ⊢ ((p .∧. q) .⟷. q)›
  by (metis Un_insert_right assumption_L conjE2_PL conjI_PL equiv_PL impI2 imp_PL insertI1 sup_bot.right_neutral)

lemma conj_imp: ‹A ⊢ (p .∧. q) .⟶. r ⟷ A ⊢ p .⟶. (q .⟶. r)›
proof
  assume "A ⊢ (p .∧. q) .⟶. r"
  then have "Cn (A ∪ {r}) ⊆ Cn (A ∪ {p, q})"
    by (metis (no_types) Cn_conj_bis Cn_imp_bis Cn_union Un_insert_right sup_bot.right_neutral)
  then show ‹A ⊢ p .⟶. (q .⟶. r)›
    by (metis Un_insert_right impI_PL inclusion_L infer_def insert_commute insert_subset subset_eq sup_bot.right_neutral)
next
   assume "A ⊢ p .⟶. (q .⟶. r)"
  then have "A ∪ {p} ∪ {q} ⊢ r"
    using imp_PL by auto
  then show "A ⊢ (p .∧. q) .⟶. r"
    by (metis (full_types) Cn_conj_bis Cn_union impI_PL infer_def insert_is_Un sup_assoc)
qed

lemma conj_not_impE_PL: ‹A ⊢ (p .∧. q) .⟶. r ⟹ A ⊢ (p .∧. .¬ q) .⟶. r ⟹ A ⊢ p .⟶. r› 
  by (meson conj_imp disjE_PL ex_mid_PL imp_PL)

lemma disj_notE_PL: ‹A ⊢ q ⟹ A ⊢ p .∨. .¬ q ⟹ A ⊢ p›
  using Cn_imp Cn_imp_bis Cn_not disjE_PL notnot_PL by blast

lemma disj_not_impE_PL: ‹A ⊢ (p .∨. q) .⟶. r ⟹ A ⊢ (p .∨. .¬ q) .⟶. r ⟹ A ⊢ r› 
  by (metis Un_insert_right disjE_PL disj_PL disj_com ex_mid_PL insert_commute sup_bot.right_neutral)

lemma imp_conj: ‹A ⊢ p .⟶. q ⟹ A ⊢ r .⟶. s ⟹ A ⊢ (p .∧. r) .⟶. (q .∧. s)›
  apply(intro impI_PL conjI_PL, unfold imp_PL[symmetric])
  by (meson assumption_L conjE1_PL conjE2_PL imp_trans infer_def insertI1 validD_L valid_imp_PL)+

lemma conj_overlap: ‹A ⊢ (p .∧. q) ⟷ A ⊢ (p .∧. ((.¬ p) .∨. q))›
  by (meson conj_PL disjI2_PL disj_com disj_notE_PL)

lemma morgan: ‹A ⊢ .¬ (p .∧. q) ⟷ A ⊢ (.¬ p) .∨. (.¬ q)›
  by (meson conj_imp disj_PL disj_com imp_PL imp_contrapos notE_PL notI_PL)

lemma conj_superexpansion1: ‹A ⊢ .¬ (p .∧. q) .∧. .¬ p ⟷ A ⊢ .¬ p›
  using conj_PL disjI1_PL morgan by auto

lemma conj_superexpansion2: ‹A ⊢ (p .∨. q) .∧. p ⟷ A ⊢ p›
  using conj_PL disjI1_PL by auto

end

subsection ‹Compact Logic›
text‹If the logic is compact, which means that any result is based on a finite set of hypothesis›
locale Compact_logic = Tarskian_logic +
  assumes compactness_L: ‹A ⊢ φ ⟹ (∃A'. A'⊆ A ∧ finite A' ∧ A'⊢ φ)›

begin

text ‹Very important lemma preparing the application of the Zorn's lemma. It states that in a compact logic, we can not deduce ‹φ›
if we accumulate an infinity of hypothesis groups which locally do not deduce phi›
lemma chain_closure: ‹¬ ⊩ φ ⟹ subset.chain {B. ¬ B ⊢ φ} C ⟹ ¬ ⋃C ⊢ φ› 
proof                                    
  assume a:‹subset.chain {B. ¬ B ⊢ φ} C› and b:‹¬ ⊩ φ› and ‹⋃ C ⊢ φ›
  then obtain A' where c:‹A'⊆ ⋃ C› and d:‹finite A'›  and e:‹A' ⊢ φ› using compactness_L by blast
  define f where f:‹f ≡ λa. SOME B. B ∈ C ∧ a ∈ B›
  have g:‹finite (f ` A')› using f d by simp
  have h:‹(f ` A') ⊆ C› 
    unfolding f by auto (metis (mono_tags, lifting) Union_iff c someI_ex subset_eq)
  have i:‹subset.chain {B. ¬ B ⊢ φ} (f ` A')› using a h
    using a h by (meson subsetD subset_chain_def subset_trans)
  have ‹A' ≠ {} ⟹ ⋃ (f ` A') ∈ {B. ¬ B ⊢ φ}› using g i 
    by (meson Union_in_chain image_is_empty subset_chain_def subset_eq)
  hence j:‹A' ≠ {} ⟹ ¬ ⋃(f ` A') ⊢ φ› by simp
  have ‹A' ⊆ ⋃(f ` A')› 
    unfolding f by auto (metis (no_types, lifting) Union_iff c someI_ex subset_iff)
  with j e b show False
    by (metis infer_def monotonicity_L subsetD valid_def)
qed

end

end