diff --git a/thys/Belief_Revision/AGM_Contraction.thy b/thys/Belief_Revision/AGM_Contraction.thy
--- a/thys/Belief_Revision/AGM_Contraction.thy
+++ b/thys/Belief_Revision/AGM_Contraction.thy
@@ -1,674 +1,674 @@
 (*<*)
 \<comment>\<open> ******************************************************************** 
  * Project         : AGM Theory
  * Version         : 1.0
  *
  * Authors         : Valentin Fouillard, Safouan Taha, Frederic Boulanger
                      and Nicolas Sabouret
  *
  * This file       : AGM contraction
  *
  * Copyright (c) 2021 Université Paris Saclay, France
  *
  * All rights reserved.
  *
  ******************************************************************************\<close>
 
 theory AGM_Contraction
 
 imports AGM_Logic AGM_Remainder
 
 begin
 (*>*)
 
 section \<open>Contractions\<close>
 text\<open>The first operator of belief change of the AGM framework is contraction. This operator consist to remove 
 a sentence @{term \<open>\<phi>\<close>} from a belief set @{term \<open>K\<close>} in such a way that @{term \<open>K\<close>} no longer imply @{term \<open>\<phi>\<close>}.
 
 In the following we will first axiomatize such operators at different levels of logics (Tarskian, supraclassical and compact) 
 and then we will give constructions satisfying these axioms. The following graph summarizes all equivalences we established:
 
 \includegraphics[width=\textwidth]{"graph_locales.pdf"}
 
 We will use the extension feature of locales in Isabelle/HOL to incrementally define the contraction 
 operator as shown by blue arrows in the previous figure. Then, using the interpretation feature of locales, we will prove the equivalence between
 descriptive and constructive approaches at each level depending on the adopted logics (black arrows).    
 \<close>
 
 subsection\<open>AGM contraction postulates\<close>
 text\<open>
 The operator of contraction is denoted by the symbol @{text \<open>\<div>\<close>} and respects the six following conditions :
 \<^item> @{text \<open>contract_closure\<close>} : a belief set @{term \<open>K\<close>} contracted by @{term \<open>\<phi>\<close>} should be logically closed
 \<^item> @{text \<open>contract_inclusion\<close>} : a contracted set @{term \<open>K\<close>} should be a subset of the original one
 \<^item> @{text \<open>contract_vacuity\<close>} : if @{term \<open>\<phi>\<close>} is not included in a set @{term \<open>K\<close>} then the contraction of @{term \<open>K\<close>} by @{term \<open>\<phi>\<close>} involves no change at all
 \<^item> @{text \<open>contract_success\<close>} : if a set @{term \<open>K\<close>} is contracted by @{term \<open>\<phi>\<close>} then @{term \<open>K\<close>} does not imply @{term \<open>\<phi>\<close>}
 \<^item> @{text \<open>contract_recovery\<close>}: all propositions removed in a set @{term \<open>K\<close>} by contraction of @{term \<open>\<phi>\<close>} will be recovered by expansion of @{term \<open>\<phi>\<close>}
 \<^item> @{text \<open>contract_extensionality\<close>} : Extensionality guarantees that the logic of contraction is extensional in the sense of allowing logically 
 quivalent sentences to be freely substituted for each other\<close>
 locale AGM_Contraction = Tarskian_logic +
 fixes contraction::\<open>'a set \<Rightarrow> 'a \<Rightarrow> 'a set\<close> (infix \<open>\<div>\<close> 55)
 assumes contract_closure:        \<open>K = Cn(A) \<Longrightarrow> K \<div> \<phi> = Cn(K \<div> \<phi>)\<close> 
     and contract_inclusion:      \<open>K = Cn(A) \<Longrightarrow> K \<div> \<phi> \<subseteq> K\<close>
     and contract_vacuity:        \<open>K = Cn(A) \<Longrightarrow> \<phi> \<notin> K \<Longrightarrow> K \<div> \<phi> = K\<close>
     and contract_success:        \<open>K = Cn(A) \<Longrightarrow> \<phi> \<notin> Cn({}) \<Longrightarrow> \<phi> \<notin> K \<div> \<phi>\<close>
     and contract_recovery:       \<open>K = Cn(A) \<Longrightarrow> K \<subseteq> ((K \<div> \<phi>) \<oplus> \<phi>)\<close>
     and contract_extensionality: \<open>K = Cn(A) \<Longrightarrow> Cn({\<phi>}) = Cn({\<psi>}) \<Longrightarrow> K \<div> \<phi> = K \<div> \<psi>\<close>
 
 
 text\<open>
 A full contraction is defined by two more postulates to rule the conjunction. We base on a supraclassical logic.
 \<^item> @{text \<open>contract_conj_overlap\<close>} : An element in both @{text \<open>K \<div> \<phi>\<close>}  and  @{text \<open>K \<div> \<psi>\<close>}  is also an element of  @{text \<open>K \<div> (\<phi> \<and> \<psi>)\<close>}
 \<^item> @{text \<open>contract_conj_inclusion\<close>} : If @{term \<open>\<phi>\<close>} not in @{text \<open>K \<div> (\<phi> \<and> \<psi>)\<close>}  then all elements removed by this contraction are also removed from @{text \<open>K \<div> \<phi>\<close>}\<close>
 locale AGM_FullContraction = AGM_Contraction + Supraclassical_logic +
   assumes contract_conj_overlap:   \<open>K = Cn(A) \<Longrightarrow> (K \<div> \<phi>) \<inter> (K \<div> \<psi>) \<subseteq> (K \<div> (\<phi> .\<and>. \<psi>))\<close>
       and contract_conj_inclusion: \<open>K = Cn(A) \<Longrightarrow> \<phi> \<notin> (K \<div> (\<phi> .\<and>. \<psi>)) \<Longrightarrow> ((K \<div> (\<phi> .\<and>. \<psi>) \<subseteq> (K \<div> \<phi>)))\<close>
 
 begin 
 \<comment> \<open>two important lemmas/corollaries that can replace the two assumptions @{text \<open>contract_conj_overlap\<close>} and @{text \<open>contract_conj_inclusion\<close>}\<close>
 text\<open>@{text \<open>contract_conj_overlap_variant\<close>} does not need \<open>\<psi>\<close> to occur in the left side! \<close>
 corollary contract_conj_overlap_variant:  \<open>K = Cn(A) \<Longrightarrow> (K \<div> \<phi>) \<inter> Cn({\<phi>}) \<subseteq> (K \<div> (\<phi> .\<and>. \<psi>))\<close>
 proof -
   assume a:\<open>K = Cn(A)\<close>
   { assume b:\<open>K \<turnstile> \<phi>\<close> and c:\<open>K \<turnstile> \<psi>\<close> 
     hence d:\<open>K \<div> (\<phi> .\<and>. \<psi>) = K \<div> (\<phi> .\<and>. ((.\<not> \<phi>) .\<or>. \<psi>))\<close> 
       apply(rule_tac contract_extensionality[OF a]) 
       using conj_overlap[of _ \<phi> \<psi>] by (simp add: Cn_same)
     have e:\<open>K \<inter> Cn {\<phi>} \<subseteq> K \<div> (.\<not> \<phi> .\<or>. \<psi>)\<close> 
     proof(safe)
       fix \<chi>
       assume f:\<open>\<chi> \<in> K\<close> and g:\<open>\<chi> \<in> Cn {\<phi>}\<close>
       have \<open>K \<div> (.\<not> \<phi> .\<or>. \<psi>) \<turnstile> (.\<not> \<phi> .\<or>. \<psi>) .\<longrightarrow>. \<chi>\<close>
         by (metis a contract_recovery expansion_def f impI_PL infer_def subset_eq)
       hence \<open>K \<div> (.\<not> \<phi> .\<or>. \<psi>) \<turnstile> .\<not> \<phi> .\<longrightarrow>. \<chi>\<close>
         by (meson disjI1_PL imp_trans inclusion_L infer_def insert_subset validD_L valid_imp_PL)
       with g show \<open>\<chi> \<in> K \<div> (.\<not> \<phi> .\<or>. \<psi>)\<close>
         by (metis a contract_closure disjE_PL ex_mid_PL infer_def validD_L valid_imp_PL)
     qed
     have ?thesis 
       unfolding d using e contract_conj_overlap[OF a, of \<phi> \<open>(.\<not> \<phi> .\<or>. \<psi>)\<close>] a contract_inclusion by force 
   }
   then show ?thesis
     apply (cases \<open>\<not> K \<turnstile> \<phi> \<or> \<not> K \<turnstile> \<psi>\<close>)  
     by (metis IntE a assumption_L conjE1_PL conjE2_PL contract_inclusion contract_vacuity subsetD subsetI) blast
 qed 
 
 text\<open>@{text \<open>contract_conj_inclusion_variant\<close>}: Everything retained in @{text \<open>K \<div> (\<phi> \<and> \<psi>)\<close>} is retained in @{text \<open>K \<div> \<psi>\<close>}\<close>
 corollary contract_conj_inclusion_variant : \<open>K = Cn(A) \<Longrightarrow> (K \<div> (\<phi> .\<and>. \<psi>) \<subseteq> (K \<div> \<phi>)) \<or> (K \<div> (\<phi> .\<and>. \<psi>) \<subseteq> (K \<div> \<psi>))\<close>
 proof -
   assume a:\<open>K = Cn(A)\<close>
   { assume d:\<open>\<phi> \<in> (K \<div> (\<phi> .\<and>. \<psi>)) \<and> \<psi> \<in> (K \<div> (\<phi> .\<and>. \<psi>))\<close> 
     hence \<open>\<phi> .\<and>. \<psi> \<in> (K \<div> (\<phi> .\<and>. \<psi>))\<close> 
       using Supraclassical_logic.conjI_PL Supraclassical_logic_axioms a contract_closure by fastforce
     with d have ?thesis
       by (metis (no_types, lifting) Supraclassical_logic.valid_conj_PL Supraclassical_logic_axioms 
                 Tarskian_logic.valid_expansion Tarskian_logic_axioms a contract_closure contract_inclusion 
                 contract_recovery contract_success dual_order.trans expansion_def)     
   }
   then show ?thesis 
     by (metis a conj_com_Cn contract_conj_inclusion contract_extensionality)
 qed
 
 end
 
 subsection \<open>Partial meet contraction definition\<close>
 
 text\<open>A partial meet contraction of @{term \<open>K\<close>} by @{term \<open>\<phi>\<close>} is the intersection of some sets that not imply @{term \<open>\<phi>\<close>}.
 We define these sets as the "remainders" @{text \<open>(K .\<bottom>. \<phi>\<close>}.
 The function of selection @{term \<open>\<gamma>\<close>} select the best set of the remainders that do not imply @{term \<open>\<phi>\<close>}.
 This function respect these postulates :
 \<^item> @{text \<open>is_selection\<close>} : if there exist some set that do not imply @{term \<open>\<phi>\<close>} then the function selection @{term \<open>\<gamma>\<close>} is a subset of these sets
 \<^item> @{text \<open>tautology_selection\<close>} : if there is no set that do not imply @{term \<open>\<phi>\<close>} then the result of the selection function is @{term \<open>K\<close>}
 \<^item> @{text nonempty_selection} : An empty selection function do not exist
 \<^item> @{text extensional_selection} : Two proposition with the same closure have the same selection function\<close>
 locale PartialMeetContraction = Tarskian_logic +
 
 fixes selection::\<open>'a set \<Rightarrow> 'a  \<Rightarrow> 'a set set\<close> (\<open>\<gamma>\<close>)
 assumes is_selection:          \<open>K = Cn(A) \<Longrightarrow> (K .\<bottom>. \<phi>) \<noteq> {} \<Longrightarrow> \<gamma> K \<phi> \<subseteq> (K .\<bottom>. \<phi>)\<close>
 assumes tautology_selection:   \<open>K = Cn(A) \<Longrightarrow> (K .\<bottom>. \<phi>) = {} \<Longrightarrow> \<gamma> K \<phi> = {K}\<close>
 assumes nonempty_selection:    \<open>K = Cn(A) \<Longrightarrow> \<gamma> K \<phi> \<noteq> {}\<close>
 assumes extensional_selection: \<open>K = Cn(A) \<Longrightarrow> Cn({\<phi>}) = Cn({\<psi>}) \<Longrightarrow> \<gamma> K \<phi> = \<gamma> K \<psi>\<close>
 
 \<comment> \<open>extensionality seems very hard to implement for a constructive approach, 
 one basic implementation will be to ignore @{term \<open>A\<close>} and @{term \<open>\<phi>\<close>} 
 and only base on @{text \<open>A .\<bottom>. \<phi>\<close>} that 
 is already proved as extensional (lemma @{text \<open>remainder_extensionality\<close>})\<close> 
 
 begin
 
 text \<open>A partial meet is the intersection of set of selected element.\<close>
 definition (in Tarskian_logic) meet_contraction::\<open>'a set \<Rightarrow> ('a set \<Rightarrow> 'a  \<Rightarrow> 'a set set) \<Rightarrow> 'a \<Rightarrow> 'a set\<close> (\<open>_ \<div>\<^bsub>_\<^esub> _\<close> [60,50,60]55)
   where mc: \<open>(A \<div>\<^bsub>\<gamma>\<^esub> \<phi>) \<equiv> \<Inter>(\<gamma> A \<phi>)\<close>
 
 text \<open>Following this definition 4 postulates of AGM can be proved on a partial meet contraction:
 \<^item> @{text \<open>contract_inclusion\<close>}
 \<^item> @{text \<open> contract_vacuity\<close>}
 \<^item> @{text \<open> contract_closure\<close>}
 \<^item> @{text \<open> contract_extensionality\<close>}\<close>
 
 text \<open>@{text \<open>pmc_inclusion\<close> } :a partial meet contraction is a subset of the contracted set\<close>
 lemma pmc_inclusion: \<open>K = Cn(A) \<Longrightarrow> K \<div>\<^bsub>\<gamma>\<^esub> \<phi> \<subseteq> K\<close>
   apply (cases \<open>(K .\<bottom>. \<phi>) = {}\<close>, simp_all add: mc tautology_selection) 
   by (meson Inf_less_eq in_mono is_selection nonempty_selection rem_inclusion)
 
 text\<open>@{text \<open>pmc_vacuity\<close>} :  if @{term \<open>\<phi>\<close>} is not included in a set @{term \<open>K\<close>} then the partial meet contraction of @{term \<open>K\<close>} by @{term \<open>\<phi>\<close>} involves not change at all\<close>
 lemma pmc_vacuity: \<open>K = Cn(A) \<Longrightarrow> \<not> K \<turnstile> \<phi> \<Longrightarrow> K \<div>\<^bsub>\<gamma>\<^esub> \<phi> = K\<close> 
   unfolding mc nonconsequence_remainder
   by (metis Inf_superset_mono Un_absorb1 cInf_singleton insert_not_empty is_selection mc nonconsequence_remainder pmc_inclusion sup_commute)
 
 text\<open>@{text \<open>pmc_closure\<close>} : a partial meet contraction is logically closed\<close>
 lemma pmc_closure: \<open>K = Cn(A) \<Longrightarrow> (K \<div>\<^bsub>\<gamma>\<^esub> \<phi>) = Cn(K \<div>\<^bsub>\<gamma>\<^esub> \<phi>)\<close> 
 proof (rule subset_antisym, simp_all add:inclusion_L mc transitivity_L, goal_cases)
   case 1
   have \<open>\<Inter>(\<gamma> (Cn A) \<phi>) = \<Inter>{Cn(B)|B. B \<in> \<gamma> (Cn A) \<phi>}\<close> 
     by auto (metis idempotency_L insert_absorb insert_iff insert_subset is_selection rem_closure tautology_selection)+
   from Cn_Inter[OF this] show ?case by blast
 qed
 
 text \<open>@{text \<open>pmc_extensionality\<close>} : Extensionality guarantees that the logic of contraction is extensional in the sense of allowing logically equivalent sentences to be freely substituted for each other\<close>
 lemma pmc_extensionality: \<open>K = Cn(A) \<Longrightarrow> Cn({\<phi>}) = Cn({\<psi>}) \<Longrightarrow> K \<div>\<^bsub>\<gamma>\<^esub> \<phi> = K \<div>\<^bsub>\<gamma>\<^esub> \<psi>\<close>
   by (metis extensional_selection mc)
 
 text \<open>@{text \<open>pmc_tautology\<close>} : if @{term \<open>\<phi>\<close>} is a tautology then the partial meet contraction of @{term \<open>K\<close>} by @{term \<open>\<phi>\<close>} is @{term \<open>K\<close>}\<close>
 lemma pmc_tautology: \<open>K = Cn(A) \<Longrightarrow> \<tturnstile> \<phi> \<Longrightarrow>  K \<div>\<^bsub>\<gamma>\<^esub> \<phi> = K\<close> 
   by (simp add: mc taut2emptyrem tautology_selection)
 
 text\<open>@{text \<open>completion\<close>} is a an operator that can build an equivalent selection from an existing one\<close>
 definition (in Tarskian_logic) completion::\<open>('a set \<Rightarrow> 'a  \<Rightarrow> 'a set set) \<Rightarrow> 'a set \<Rightarrow> 'a  \<Rightarrow> 'a set set\<close> (\<open>*\<close>)
   where \<open>* \<gamma> A \<phi> \<equiv> if (A .\<bottom>. \<phi>) = {} then {A} else {B. B \<in> A .\<bottom>. \<phi> \<and> \<Inter> (\<gamma> A \<phi>) \<subseteq> B}\<close>
 
 
 lemma selection_completion: "K = Cn(A) \<Longrightarrow> \<gamma> K \<phi> \<subseteq> * \<gamma> K \<phi>" 
   using completion_def is_selection tautology_selection by fastforce
 
 lemma (in Tarskian_logic) completion_completion: "K = Cn(A) \<Longrightarrow> * (* \<gamma>) K \<phi> = * \<gamma> K \<phi>"
   by (auto simp add:completion_def)
 
 lemma pmc_completion: \<open>K = Cn(A) \<Longrightarrow> K \<div>\<^bsub>*\<gamma>\<^esub> \<phi> = K \<div>\<^bsub>\<gamma>\<^esub> \<phi>\<close>
   apply(auto simp add: mc completion_def tautology_selection)
   by (metis Inter_lower equals0D in_mono is_selection)
 
 end
 
 text\<open>A transitively relational meet contraction is a partial meet contraction using a binary relation between the elements of the selection function\<close>
 text\<open>A relation is : 
 \<^item> transitive (@{text \<open>trans_rel\<close>})
 \<^item> non empty (there is always an element  preferred to the others (@{text \<open>nonempty_rel\<close>}))\<close>
 
 text\<open>A selection function @{term \<open>\<gamma>\<^sub>T\<^sub>R\<close>} is transitively relational @{text \<open>rel_sel\<close>} with the following condition :
 \<^item> If the the remainders @{text \<open>K .\<bottom>. \<phi>\<close>} is empty then the selection function return @{term \<open>K\<close>}
 \<^item> Else the selection function return a non empty transitive relation on the remainders\<close>
 locale TransitivelyRelationalMeetContraction =  Tarskian_logic +
 
 fixes relation::\<open>'a set \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool\<close> (\<open>_ \<preceq>\<^bsub>_\<^esub> _\<close> [60,50,60]55)
 assumes trans_rel: \<open>K = Cn(A) \<Longrightarrow> B \<preceq>\<^bsub>K\<^esub> C \<Longrightarrow> C \<preceq>\<^bsub>K\<^esub> D \<Longrightarrow> B \<preceq>\<^bsub>K\<^esub> D\<close>
 assumes nonempty_rel: \<open>K = Cn(A) \<Longrightarrow> (K .\<bottom>. \<phi>) \<noteq> {} \<Longrightarrow> \<exists>B\<in>(K .\<bottom>. \<phi>). (\<forall>C\<in>(K .\<bottom>. \<phi>). C \<preceq>\<^bsub>K\<^esub> B)\<close> \<comment> \<open>pas clair dans la litterrature\<close>
 
 fixes rel_sel::\<open>'a set \<Rightarrow> 'a  \<Rightarrow> 'a set set\<close> (\<open>\<gamma>\<^sub>T\<^sub>R\<close>) 
 defines rel_sel: \<open>\<gamma>\<^sub>T\<^sub>R K \<phi> \<equiv> if (K .\<bottom>. \<phi>) = {} then {K} 
                                               else {B. B\<in>(K .\<bottom>. \<phi>) \<and> (\<forall>C\<in>(K .\<bottom>. \<phi>). C \<preceq>\<^bsub>K\<^esub> B)}\<close>
 
 begin
 
 text\<open>A transitively relational selection function respect the partial meet contraction postulates.\<close>
 sublocale PartialMeetContraction where selection = \<gamma>\<^sub>T\<^sub>R
   apply(unfold_locales)
      apply(simp_all add: rel_sel) 
    using nonempty_rel apply blast
   using remainder_extensionality by blast
 
 end
 
 text\<open>A full meet contraction is a limiting case of the partial meet contraction where if the remainders are not empty then
 the selection function return all the remainders (as defined by @{text \<open>full_sel\<close>}\<close>
 locale FullMeetContraction = Tarskian_logic +
 
 fixes full_sel::\<open>'a set \<Rightarrow> 'a  \<Rightarrow> 'a set set\<close> (\<open>\<gamma>\<^sub>F\<^sub>C\<close>) 
 defines full_sel: \<open>\<gamma>\<^sub>F\<^sub>C K \<phi> \<equiv> if K .\<bottom>. \<phi> = {} then {K} else K .\<bottom>. \<phi>\<close>
 
 begin
 
 
 text\<open>A full selection and a relation ? is a transitively relational meet contraction postulates.\<close>
 sublocale TransitivelyRelationalMeetContraction where relation = \<open>\<lambda> K A B. True\<close> and rel_sel=\<gamma>\<^sub>F\<^sub>C
   by (unfold_locales, auto simp add:full_sel, rule eq_reflection, simp) 
 
 end
 
 subsection\<open>Equivalence of partial meet contraction and AGM contraction\<close>
 
 
 locale PMC_SC = PartialMeetContraction + Supraclassical_logic + Compact_logic 
 
 begin
 
 text \<open>In a context of a supraclassical and a compact logic the two remaining postulates of AGM contraction :
 \<^item> @{text \<open>contract_recovery\<close>}
 \<^item> @{text \<open>contract_success\<close>}
 can be proved on a partial meet contraction.\<close>
 
 text\<open>@{text \<open>pmc_recovery\<close>} : all proposition removed by a partial meet contraction of @{term \<open>\<phi>\<close>} will be recovered by the expansion of @{term \<open>\<phi>\<close>}\<close>
 
 \<comment> \<open>recovery requires supraclassicality\<close>
 lemma pmc_recovery: \<open>K = Cn(A) \<Longrightarrow> K \<subseteq> ((K \<div>\<^bsub>\<gamma>\<^esub> \<phi>) \<oplus> \<phi>)\<close>  
   apply(cases \<open>(K .\<bottom>. \<phi>) = {}\<close>, simp_all (no_asm) add:mc expansion_def) 
   using inclusion_L tautology_selection apply fastforce
   proof -
     assume a:\<open>K = Cn(A)\<close> and b:\<open>K .\<bottom>. \<phi> \<noteq> {}\<close>
     { fix \<psi>
       assume d:\<open>K \<turnstile> \<psi>\<close>
       have \<open>\<phi> .\<longrightarrow>. \<psi> \<in> \<Inter>(\<gamma> K \<phi>)\<close> 
         using is_selection[OF a b] 
         by auto (metis a d infer_def rem_closure remainder_recovery subsetD)
     }
     with a b show \<open>K \<subseteq> Cn (insert \<phi> (\<Inter> (\<gamma> K \<phi>)))\<close>
       by (metis (no_types, lifting) Un_commute assumption_L imp_PL infer_def insert_is_Un subsetI)
   qed
 
 text \<open>@{text \<open>pmc_success\<close>} : a partial meet contraction of @{term \<open>K\<close>} by @{term \<open>\<phi>\<close>} not imply @{term \<open>\<phi>\<close>}\<close>
 \<comment> \<open>success requires compacteness\<close>
 lemma pmc_success: \<open>K = Cn(A) \<Longrightarrow> \<phi> \<notin> Cn({}) \<Longrightarrow> \<phi> \<notin> K \<div>\<^bsub>\<gamma>\<^esub> \<phi>\<close>
 proof
   assume a:\<open>K = Cn(A)\<close> and b:\<open>\<phi> \<notin> Cn({})\<close> and c:\<open>\<phi> \<in> K \<div>\<^bsub>\<gamma>\<^esub> \<phi>\<close>
   from c show False unfolding mc
   proof(cases \<open>K .\<bottom>. \<phi> = {K}\<close>)
     case True
     then show ?thesis
       by (meson assumption_L c nonconsequence_remainder pmc_inclusion[OF a] subsetD)
   next
     case False
     hence \<open>\<forall>B\<in>K .\<bottom>. \<phi>. \<phi> \<notin> B\<close> using assumption_L rem by auto
     moreover have \<open>K .\<bottom>. \<phi> \<noteq> {}\<close> using b emptyrem2taut validD_L by blast
     ultimately show ?thesis 
       using b c mc nonempty_selection[OF a] validD_L emptyrem2taut is_selection[OF a]
       by (metis Inter_iff bot.extremum_uniqueI subset_iff)
   qed
 qed
 
 text\<open>As a partial meet contraction has been proven to respect all postulates of AGM contraction 
 the equivalence between the both are straightforward\<close>
 sublocale AGM_Contraction where contraction = \<open>\<lambda>A \<phi>. A \<div>\<^bsub>\<gamma>\<^esub> \<phi>\<close>
   using pmc_closure pmc_inclusion pmc_vacuity 
         pmc_success pmc_recovery pmc_extensionality
         expansion_def idempotency_L infer_def
   by (unfold_locales) metis+
 
 end
 
 
 locale AGMC_SC = AGM_Contraction + Supraclassical_logic + Compact_logic
 
 begin
 
 text \<open>obs 2.5 page 514\<close>
 definition AGM_selection::\<open>'a set \<Rightarrow> 'a  \<Rightarrow> 'a set set\<close> (\<open>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<close>)
   where AGM_sel: \<open>\<gamma>\<^sub>A\<^sub>G\<^sub>M A \<phi> \<equiv> if A .\<bottom>. \<phi> = {} then {A} else {B. B \<in> A .\<bottom>. \<phi> \<and> A \<div> \<phi> \<subseteq> B}\<close> 
 
 text\<open>The selection function @{term \<open>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<close>} respect the partial meet contraction postulates\<close>
 sublocale PartialMeetContraction where selection = \<gamma>\<^sub>A\<^sub>G\<^sub>M
 proof(unfold_locales, unfold AGM_sel, simp_all, goal_cases)
   case (1 K A \<phi>) \<comment> \<open>@{text \<open>non_emptiness\<close>} of selection requires a compact logic\<close>
   then show ?case  using upper_remainder[of \<open>K \<div> \<phi>\<close> K \<phi>] contract_success[OF 1(1)]
     by (metis contract_closure contract_inclusion infer_def taut2emptyrem valid_def)
 next
   case (2 K A \<phi> \<psi>)
   then show ?case
     by (metis (mono_tags, lifting) contract_extensionality Collect_cong remainder_extensionality)
 qed 
 
 text \<open>@{text \<open>contraction_is_pmc\<close>} : an AGM contraction is equivalent to a partial met contraction using the selection function \<open>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<close>\<close>
 lemma contraction_is_pmc: \<open>K = Cn(A) \<Longrightarrow> K \<div> \<phi> = K \<div>\<^bsub>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<^esub> \<phi>\<close> \<comment> \<open>requires a supraclassical logic\<close>
 proof
   assume a:\<open>K = Cn(A)\<close>
   show \<open>K \<div> \<phi> \<subseteq> K \<div>\<^bsub>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<^esub> \<phi>\<close> 
     using contract_inclusion[OF a] by (auto simp add:mc AGM_sel) 
 next
   assume a:\<open>K = Cn(A)\<close>
   show \<open>K \<div>\<^bsub>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<^esub> \<phi> \<subseteq> K \<div> \<phi>\<close>
   proof (cases \<open>\<tturnstile> \<phi>\<close>)
     case True
     hence \<open>K .\<bottom>. \<phi> = {}\<close>
       using nonconsequence_remainder taut2emptyrem by auto
     then show ?thesis 
       apply(simp_all add:mc AGM_sel) 
       by (metis a emptyrem2taut contract_closure contract_recovery valid_expansion)
   next  
     case validFalse:False
     then show ?thesis 
     proof (cases \<open>K \<turnstile> \<phi>\<close>)
       case True
       hence b:\<open>K .\<bottom>. \<phi> \<noteq> {}\<close>
         using emptyrem2taut validFalse by blast
       have d:\<open>\<psi> \<in> K \<Longrightarrow> \<phi> .\<longrightarrow>. \<psi> \<in> K \<div> \<phi>\<close> for \<psi> 
         using Supraclassical_logic.impI_PL Supraclassical_logic_axioms a contract_closure contract_recovery expansion_def by fastforce
       { fix \<psi>
         assume e:\<open>\<psi> \<in> K \<close> and f:\<open>\<psi> \<notin> K \<div> \<phi>\<close>
         have \<open>(\<psi> .\<longrightarrow>. \<phi>) .\<longrightarrow>. \<phi> \<notin> K \<div> \<phi>\<close> 
           using imp_recovery2[of \<open>K \<div> \<phi>\<close> \<phi> \<psi>] a contract_closure d e f by auto
         hence g:\<open>\<not> (K \<div> \<phi>) \<union> {\<psi> .\<longrightarrow>. \<phi>} \<turnstile> \<phi>\<close> 
           using a contract_closure impI_PL by fastforce
         then obtain B where h:\<open>(K \<div> \<phi>) \<union> {\<psi> .\<longrightarrow>. \<phi>} \<subseteq> B\<close> and i:\<open>B \<in> K .\<bottom>. \<phi>\<close>  
           using upper_remainder[of \<open>(K \<div> \<phi>) \<union> {\<psi> .\<longrightarrow>. \<phi>}\<close> K \<phi>] a True contract_inclusion idempotency_L impI2 by auto
         hence j:\<open>\<psi> \<notin> Cn(B)\<close>
           by (metis (no_types, lifting) CollectD mp_PL Un_insert_right a infer_def insert_subset rem rem_closure)
         have \<open>\<psi> \<notin>  K \<div>\<^bsub>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<^esub> \<phi>\<close> 
           apply(simp add:mc AGM_sel b, rule_tac x=B in exI)
           by (meson Tarskian_logic.assumption_L Tarskian_logic_axioms h i j le_sup_iff)
       }
       then show ?thesis 
         using a pmc_inclusion by fastforce
     next
       case False
       hence \<open>K .\<bottom>. \<phi> = {K}\<close>
         using nonconsequence_remainder taut2emptyrem by auto
       then show ?thesis 
         using False a contract_vacuity idempotency_L pmc_vacuity by auto
     qed
   qed
 qed
 
 lemma contraction_with_completion: \<open>K = Cn(A) \<Longrightarrow> K \<div> \<phi> = K \<div>\<^bsub>* \<gamma>\<^sub>A\<^sub>G\<^sub>M\<^esub> \<phi>\<close>
   by (simp add: contraction_is_pmc pmc_completion)
 
 end
 
 (* in case of doubt uncomment one of these\<in>
 sublocale AGMC_SC \<subseteq> PMC_SC where selection = \<gamma>\<^sub>A\<^sub>G\<^sub>M\<^sub>C 
   by (unfold_locales)
 
 sublocale PMC_SC \<subseteq> AGMC_SC where contraction = \<open>\<lambda>A \<phi>. A \<div>\<^bsub>\<gamma>\<^esub> \<phi>\<close>
   by (unfold_locales)
 *)
 
 locale TRMC_SC = TransitivelyRelationalMeetContraction + PMC_SC where selection = \<gamma>\<^sub>T\<^sub>R
 
 begin
 text \<open>A transitively relational selection function respect conjuctive overlap.\<close>
 lemma rel_sel_conj_overlap: \<open>K = Cn(A) \<Longrightarrow> \<gamma>\<^sub>T\<^sub>R K (\<phi> .\<and>. \<psi>) \<subseteq> \<gamma>\<^sub>T\<^sub>R K \<phi> \<union> \<gamma>\<^sub>T\<^sub>R K \<psi>\<close>
 proof(intro subsetI) 
   fix B
   assume a:\<open>K = Cn(A)\<close> and b:\<open>B \<in> \<gamma>\<^sub>T\<^sub>R K (\<phi> .\<and>. \<psi>)\<close>
   show \<open>B \<in> \<gamma>\<^sub>T\<^sub>R K \<phi> \<union> \<gamma>\<^sub>T\<^sub>R K \<psi>\<close> (is ?A)
   proof(cases \<open>\<tturnstile> \<phi> \<or> \<tturnstile> \<psi> \<or> \<not> K \<turnstile> \<phi> \<or> \<not> K \<turnstile> \<psi>\<close>, elim disjE)
     assume \<open>\<tturnstile> \<phi>\<close>
     hence c:\<open>Cn({\<phi> .\<and>. \<psi>}) = Cn({\<psi>})\<close> 
       using conj_equiv valid_Cn_equiv valid_def by blast
     from b show ?A 
       by (metis Un_iff a c extensional_selection)
   next
     assume \<open>\<tturnstile> \<psi>\<close>
     hence c:\<open>Cn({\<phi> .\<and>. \<psi>}) = Cn({\<phi>})\<close> 
       by (simp add: Cn_conj_bis Cn_same validD_L)
     from b show ?A 
       by (metis Un_iff a c extensional_selection)
   next
     assume \<open>\<not> K \<turnstile> \<phi>\<close>
     then show ?A
       by (metis UnI1 a b conjE1_PL is_selection nonconsequence_remainder nonempty_selection tautology_selection subset_singletonD)
   next
     assume \<open>\<not> K \<turnstile> \<psi>\<close>
     then show ?A
       by (metis UnI2 a b conjE2_PL is_selection nonconsequence_remainder nonempty_selection tautology_selection subset_singletonD)
   next
     assume d:\<open>\<not> (\<tturnstile> \<phi> \<or> \<tturnstile> \<psi> \<or> \<not> K \<turnstile> \<phi> \<or> \<not> K \<turnstile> \<psi>)\<close>
     hence h:\<open>K .\<bottom>. \<phi>  \<noteq> {}\<close> and i:\<open>K .\<bottom>. \<psi> \<noteq> {}\<close> and j:\<open>K .\<bottom>. (\<phi> .\<and>. \<psi>) \<noteq> {}\<close> and k:"K \<turnstile> \<phi> .\<and>. \<psi>"
       using d emptyrem2taut valid_conj_PL apply auto
       by (meson Supraclassical_logic.conjI_PL Supraclassical_logic_axioms d)
     show ?A 
       using remainder_conj[OF a k] b h i j rel_sel by auto
   qed
 qed
 
 text\<open>A transitively relational meet contraction respect conjuctive overlap.\<close>
 lemma trmc_conj_overlap: \<open>K = Cn(A) \<Longrightarrow> (K \<div>\<^bsub>\<gamma>\<^sub>T\<^sub>R\<^esub> \<phi>) \<inter> (K \<div>\<^bsub>\<gamma>\<^sub>T\<^sub>R\<^esub> \<psi>) \<subseteq> (K \<div>\<^bsub>\<gamma>\<^sub>T\<^sub>R\<^esub> (\<phi> .\<and>. \<psi>))\<close>
   unfolding mc using rel_sel_conj_overlap by blast
 
 text\<open>A transitively relational selection function respect conjuctive inclusion\<close>
 lemma rel_sel_conj_inclusion: \<open>K = Cn(A) \<Longrightarrow> \<gamma>\<^sub>T\<^sub>R K (\<phi> .\<and>. \<psi>) \<inter> (K .\<bottom>. \<phi>) \<noteq> {} \<Longrightarrow> \<gamma>\<^sub>T\<^sub>R K \<phi> \<subseteq> \<gamma>\<^sub>T\<^sub>R K (\<phi> .\<and>. \<psi>)\<close>
 proof(intro subsetI) 
   fix B
   assume a:\<open>K = Cn(A)\<close> and b:\<open>\<gamma>\<^sub>T\<^sub>R K (\<phi> .\<and>. \<psi>) \<inter> (K .\<bottom>. \<phi>) \<noteq> {}\<close> and c:\<open>B \<in> \<gamma>\<^sub>T\<^sub>R K \<phi>\<close>
   show \<open>B \<in> \<gamma>\<^sub>T\<^sub>R K (\<phi> .\<and>. \<psi>)\<close> (is ?A)
   proof(cases \<open>\<tturnstile> \<phi> \<or> \<tturnstile> \<psi> \<or> \<not> K \<turnstile> \<phi> \<or> \<not> K \<turnstile> \<psi>\<close>, auto)
     assume \<open>\<tturnstile> \<phi>\<close>
     then show ?A 
       using b taut2emptyrem by auto
   next
     assume \<open>\<tturnstile> \<psi>\<close>
     hence \<open>Cn({\<phi> .\<and>. \<psi>}) = Cn({\<phi>})\<close>
       by (simp add: Cn_conj_bis Cn_same validD_L)
     then show ?A 
       using a c extensional_selection by blast  
   next
     assume d:\<open>\<phi> \<notin> Cn K\<close>
     with d show ?A
       by (metis Int_emptyI Tarskian_logic.nonconsequence_remainder Tarskian_logic_axioms a b c idempotency_L 
                 inf_bot_right is_selection nonempty_selection singletonD subset_singletonD)
   next
     assume d:\<open>\<psi> \<notin> Cn K\<close>
     hence e:\<open>(\<phi> .\<and>. \<psi>) \<notin> Cn K\<close> 
       by (meson Supraclassical_logic.conjE2_PL Supraclassical_logic_axioms)
     hence f:\<open>\<gamma>\<^sub>T\<^sub>R K (\<phi> .\<and>. \<psi>) = {K}\<close>
       by (metis Tarskian_logic.nonconsequence_remainder Tarskian_logic_axioms a insert_not_empty is_selection 
                 nonempty_selection subset_singletonD)
     with b have g:\<open>(K .\<bottom>. \<phi>) = {K}\<close> 
       unfolding nonconsequence_remainder[symmetric] using rem by auto
     with d f show ?A
       using a c is_selection by fastforce
   next
     assume d:\<open>\<not> \<tturnstile> \<phi>\<close> and e:\<open>\<not> \<tturnstile> \<psi>\<close> and f:\<open>\<phi> \<in> Cn K\<close> and g:\<open>\<psi> \<in> Cn K\<close>
     hence h:\<open>K .\<bottom>. \<phi>  \<noteq> {}\<close> and i:\<open>K .\<bottom>. \<psi> \<noteq> {}\<close> and j:\<open>K .\<bottom>. (\<phi> .\<and>. \<psi>) \<noteq> {}\<close> and k:"K \<turnstile> \<phi> .\<and>. \<psi>"
       using e d emptyrem2taut valid_conj_PL apply auto
       by (meson Supraclassical_logic.conjI_PL Supraclassical_logic_axioms f g)
     have o:\<open>B \<in> K .\<bottom>. \<phi> \<Longrightarrow> B \<in> K .\<bottom>. (\<phi> .\<and>. \<psi>)\<close> for B
       using a k remainder_conj by auto
     from b obtain B' where l:\<open>B' \<in> K .\<bottom>. (\<phi> .\<and>. \<psi>)\<close> and m:\<open>\<forall>C\<in>K .\<bottom>. (\<phi> .\<and>. \<psi>). C \<preceq>\<^bsub>K\<^esub> B'\<close> and n:\<open>\<phi> \<notin> B'\<close>
       apply (auto simp add:mc rel_sel j)
       using assumption_L rem by force
     have p:\<open>B' \<in> K .\<bottom>. \<phi>\<close> 
       apply(simp add: rem)
       by (metis (no_types, lifting) Supraclassical_logic.conjE1_PL Supraclassical_logic_axioms 
                 Tarskian_logic.rem Tarskian_logic_axioms a l mem_Collect_eq n rem_closure)
     from c show ?A 
       apply (simp add:rel_sel o j h)
       using m p trans_rel a by blast
   qed
 qed
 
 text\<open>A transitively relational meet contraction respect conjuctive inclusion\<close>
 lemma trmc_conj_inclusion: \<open>K = Cn(A) \<Longrightarrow> \<phi> \<notin> (K \<div>\<^bsub>\<gamma>\<^sub>T\<^sub>R\<^esub> (\<phi> .\<and>. \<psi>)) \<Longrightarrow> ((K \<div>\<^bsub>\<gamma>\<^sub>T\<^sub>R\<^esub> (\<phi> .\<and>. \<psi>) \<subseteq> (K \<div>\<^bsub>\<gamma>\<^sub>T\<^sub>R\<^esub> \<phi>)))\<close>
 proof -
   assume a:\<open>K = Cn(A)\<close> and b:\<open>\<phi> \<notin> (K \<div>\<^bsub>\<gamma>\<^sub>T\<^sub>R\<^esub> (\<phi> .\<and>. \<psi>))\<close>
   then obtain B where c:\<open>B \<in> \<gamma>\<^sub>T\<^sub>R K (\<phi> .\<and>. \<psi>)\<close> and d:\<open>\<not> B \<turnstile> \<phi>\<close> apply(simp add:mc) 
     by (metis b emptyrem2taut is_selection pmc_tautology rem_closure subset_iff validD_L valid_conj_PL)
   hence \<open>B \<in> (K .\<bottom>. \<phi>)\<close>
     using remainder_recovery_bis[OF a _ d, of \<open>\<phi> .\<and>. \<psi>\<close>]
-    by (metis (no_types, hide_lams) a conj_PL emptyrem2taut insert_not_empty is_selection 
-                                    nonconsequence_remainder subsetD taut2emptyrem)
+    by (metis (no_types, opaque_lifting) a conj_PL emptyrem2taut insert_not_empty is_selection 
+                                         nonconsequence_remainder subsetD taut2emptyrem)
   with c have e:\<open>\<gamma>\<^sub>T\<^sub>R K (\<phi> .\<and>. \<psi>) \<inter> (K .\<bottom>. \<phi>) \<noteq> {}\<close> by blast
   then show \<open>((K \<div>\<^bsub>\<gamma>\<^sub>T\<^sub>R\<^esub> (\<phi> .\<and>. \<psi>) \<subseteq> (K \<div>\<^bsub>\<gamma>\<^sub>T\<^sub>R\<^esub> \<phi>)))\<close> 
     unfolding mc using rel_sel_conj_inclusion[OF a e] by blast
 qed
 
 text\<open>As a transitively relational meet contraction has been proven to respect all postulates of AGM full contraction 
 the equivalence between the both are straightforward\<close>
 sublocale AGM_FullContraction where contraction = \<open>\<lambda>A \<phi>. A  \<div>\<^bsub>\<gamma>\<^sub>T\<^sub>R\<^esub> \<phi>\<close>
   using trmc_conj_inclusion trmc_conj_overlap
   by (unfold_locales, simp_all)
 
 end
 
                                     
 locale AGMFC_SC = AGM_FullContraction + AGMC_SC 
 
 begin
 
 text\<open>An AGM relation is defined as ?\<close>
 definition AGM_relation::\<open>'a set \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool\<close> 
   where AGM_rel: \<open>AGM_relation C K B  \<equiv> (C = K \<and> B = K) \<or> (  (\<exists>\<phi>. K \<turnstile> \<phi> \<and> C \<in> K .\<bottom>. \<phi>)
                                                             \<and> (\<exists>\<phi>. K \<turnstile> \<phi> \<and> B \<in> K .\<bottom>. \<phi> \<and>  K \<div> \<phi> \<subseteq> B)
                                                             \<and> (\<forall>\<phi>. (K \<turnstile> \<phi> \<and> C \<in> K .\<bottom>. \<phi> \<and> B \<in> K .\<bottom>. \<phi> \<and> K \<div> \<phi> \<subseteq> C) \<longrightarrow> K \<div> \<phi> \<subseteq> B))\<close>
 text\<open>An AGM relational selection is defined as a function that return @{term \<open>K\<close>} if the remainders of @{text \<open>K .\<bottom>. \<phi>\<close>} is empty and
 the best element of the remainders according to an AGM relation\<close>
 definition AGM_relational_selection::\<open>'a set \<Rightarrow> 'a  \<Rightarrow> 'a set set\<close> (\<open>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<^sub>T\<^sub>R\<close>)
   where AGM_rel_sel: \<open>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<^sub>T\<^sub>R  K \<phi> \<equiv> if (K .\<bottom>. \<phi>) = {} 
                                    then {K} 
                                    else {B. B\<in>(K .\<bottom>. \<phi>) \<and> (\<forall>C\<in>(K .\<bottom>. \<phi>). AGM_relation C K B)}\<close>
 
 lemma AGM_rel_sel_completion: \<open>K = Cn(A) \<Longrightarrow> \<gamma>\<^sub>A\<^sub>G\<^sub>M\<^sub>T\<^sub>R K \<phi> = * \<gamma>\<^sub>A\<^sub>G\<^sub>M K \<phi>\<close> 
   apply (unfold AGM_rel_sel, simp add:completion_def split: if_splits)
 proof(auto simp add:AGM_sel)
   fix S B C
   assume a:\<open>S \<in> Cn(A) .\<bottom>. \<phi>\<close> and b:\<open>B \<in> Cn(A) .\<bottom>. \<phi>\<close> and c:\<open>\<Inter> {B \<in> Cn(A) .\<bottom>. \<phi>. Cn(A) \<div> \<phi> \<subseteq> B} \<subseteq> B\<close> 
      and d:\<open>C \<in> Cn(A) .\<bottom>. \<phi>\<close>
   hence e:\<open>\<phi> \<notin>  Cn(A) \<div> \<phi>\<close> 
     using Tarskian_logic.taut2emptyrem Tarskian_logic_axioms contract_success by fastforce
   show \<open>AGM_relation C (Cn(A)) B\<close>
   proof(cases \<open>\<phi> \<in> Cn(A)\<close>)
     case True
     { fix \<psi>
       assume \<open>Cn A \<div> \<psi> \<subseteq> C\<close> 
       hence \<open>Cn A \<div> (\<phi> .\<and>. \<psi>) \<subseteq> Cn A \<div> \<phi>\<close> 
         using contract_conj_inclusion_variant[of \<open>Cn(A)\<close> A \<phi> \<psi>]
         by (metis (mono_tags, lifting) assumption_L contract_conj_inclusion d mem_Collect_eq rem subset_iff)
     } note f = this
     { fix \<psi> \<phi>'
       assume g:\<open>\<psi> \<in> Cn A \<div> \<phi>'\<close> and h:\<open>B \<in> Cn A .\<bottom>. \<phi>'\<close> and j:\<open>Cn A \<div> \<phi>' \<subseteq> C\<close> and i:\<open>\<psi> \<notin> B\<close> 
       hence \<open>\<phi>' .\<or>. \<psi> \<in> Cn A \<div> \<phi>'\<close>
         using Supraclassical_logic.disjI2_PL Supraclassical_logic_axioms contract_closure by fastforce
       hence k:\<open>\<phi>' .\<or>. \<psi> \<in> Cn A \<div> \<phi>\<close> 
         using contract_conj_overlap_variant[of \<open>Cn(A)\<close> A \<phi>' \<phi>] f[OF j]
         by (metis IntI Supraclassical_logic.disjI1_PL Supraclassical_logic_axioms conj_com_Cn 
                   contract_extensionality inclusion_L singletonI subsetD) 
       hence l:\<open>Cn A \<div> \<phi> \<subseteq> B\<close> using c by auto
       from k l have m:\<open>\<phi>' .\<or>. \<psi> \<in> B\<close> and n:\<open>B =Cn(B)\<close> 
         using b rem_closure by blast+
       have \<open>B \<union> {\<psi>} \<turnstile> \<phi>'\<close> using g h i
         by (simp add:rem) (metis contract_inclusion insertI1 insert_subsetI psubsetI subsetD subset_insertI)
       with n m have  \<open>B \<turnstile> \<phi>'\<close>
         by (metis Cn_equiv assumption_L disjE_PL disj_com equiv_PL imp_PL)
       with h have False 
         using assumption_L rem by auto
     } note g = this
     with True show ?thesis 
       apply(unfold AGM_rel, rule_tac disjI2)
       using d b c by (auto simp add:AGM_rel idempotency_L del:subsetI) blast+
   next
     case False
     then show ?thesis
       by (metis AGM_rel b d idempotency_L infer_def nonconsequence_remainder singletonD)
     qed
 next
   fix S B \<psi>
   assume a:\<open>S \<in> Cn(A) .\<bottom>. \<phi>\<close> and b:\<open>B \<in> Cn(A) .\<bottom>. \<phi>\<close> and c:\<open>\<forall>C\<in>Cn A .\<bottom>. \<phi>. AGM_relation C (Cn A) B\<close> 
      and d:\<open>\<forall>C'. C' \<in> Cn A .\<bottom>. \<phi> \<and> Cn A \<div> \<phi> \<subseteq> C' \<longrightarrow> \<psi> \<in> C'\<close>
   then show \<open>\<psi> \<in> B\<close>
     unfolding AGM_rel
     by (metis (no_types, lifting) AGM_sel empty_Collect_eq insert_Diff insert_not_empty 
               nonconsequence_remainder nonempty_selection singletonD)
 qed
 
 text\<open>A transitively relational selection and an AGM relation is a transitively relational meet contraction\<close>
 sublocale TransitivelyRelationalMeetContraction where relation = AGM_relation and rel_sel = \<open>\<gamma>\<^sub>A\<^sub>G\<^sub>M\<^sub>T\<^sub>R\<close>
 proof(unfold_locales, simp_all (no_asm) only:atomize_eq, goal_cases)
   case a:(1 K A C B' B) \<comment> \<open>Very difficult proof requires litterature and high automation of isabelle!\<close>
   from a(2,3) show ?case 
     unfolding AGM_rel apply(elim disjE conjE, simp_all) 
   proof(intro disjI2 allI impI, elim exE conjE, goal_cases)
     case (1 \<psi> _ _ \<phi>)
     have b:\<open>B \<in> K .\<bottom>. (\<phi> .\<and>. \<psi>)\<close> and c:\<open>B' \<in> K .\<bottom>. (\<phi> .\<and>. \<psi>)\<close> and d:\<open>C \<in> K .\<bottom>. (\<phi> .\<and>. \<psi>)\<close>
       using remainder_conj[OF a(1)] 1 conjI_PL by auto
     hence e:\<open>K \<div> (\<phi> .\<and>. \<psi>) \<subseteq> B\<close> 
       using contract_conj_inclusion_variant[OF a(1), of \<phi>  \<psi>] 
       by (meson "1"(1) "1"(12) "1"(16) "1"(2) "1"(3) "1"(8) Supraclassical_logic.conj_PL 
                 Supraclassical_logic_axioms dual_order.trans)
     { fix \<chi>
       assume f:\<open>\<chi> \<in> K \<div> \<psi>\<close>
       have \<open>\<psi> .\<or>. \<chi> \<in> (K \<div> \<psi>) \<inter> Cn {\<psi>}\<close> 
         by (metis Int_iff Supraclassical_logic.disjI1_PL Supraclassical_logic.disjI2_PL Supraclassical_logic_axioms 
                   f a(1) contract_closure in_mono inclusion_L singletonI)
       hence g:\<open>\<psi> .\<or>. \<chi> \<in> B\<close> 
         using contract_conj_overlap_variant[OF a(1), of \<psi>] 
         by (metis AGM_Contraction.contract_extensionality AGM_Contraction_axioms a(1) conj_com_Cn e in_mono)
       have \<open>\<psi> .\<longrightarrow>. \<chi> \<in> B\<close>
         by (metis a(1) "1"(10) "1"(15) "1"(16) assumption_L f in_mono infer_def rem_closure rem_inclusion remainder_recovery)
       with g have \<open>\<chi> \<in> B\<close>
         by (metis 1(15) a(1) disjE_PL infer_def order_refl rem_closure validD_L valid_Cn_imp)
     }
     then show ?case by blast
   qed
 next
   case (2 K A \<phi>) 
   hence \<open>* \<gamma>\<^sub>A\<^sub>G\<^sub>M  K \<phi> \<noteq> {}\<close> 
     using nonempty_selection[OF 2(1), of \<phi>] selection_completion[OF 2(1), of \<phi>] by blast
   then show ?case
     using AGM_rel_sel_completion[OF 2(1), of \<phi>] AGM_rel_sel 2(1,2) by force
 next
   case (3 K \<phi>)
   then show ?case using AGM_rel_sel_completion AGM_rel_sel by simp
 qed 
 
 \<comment> \<open>ça marche tout seul! ==> Je ne vois pas où sont utilisés ces lemmas\<close>
 lemmas fullcontraction_is_pmc = contraction_is_pmc
 lemmas fullcontraction_is_trmc = contraction_with_completion
 
 end
 
 
 locale FMC_SC = FullMeetContraction + TRMC_SC
 
 begin
 
 lemma full_meet_weak1: \<open>K = Cn(A) \<Longrightarrow> K \<turnstile> \<phi> \<Longrightarrow> (K \<div>\<^bsub>\<gamma>\<^sub>F\<^sub>C\<^esub> \<phi>) = K \<inter> Cn({.\<not> \<phi>})\<close>
 proof(intro subset_antisym Int_greatest)
   assume a:\<open>K = Cn(A)\<close> and b:\<open>K \<turnstile> \<phi>\<close> 
   then show \<open> (K \<div>\<^bsub>\<gamma>\<^sub>F\<^sub>C\<^esub> \<phi>) \<subseteq> K\<close> 
     by (simp add: Inf_less_eq full_sel mc rem_inclusion)
 next 
   assume a:\<open>K = Cn(A)\<close> and b:\<open>K \<turnstile> \<phi>\<close>   
   show \<open>(K \<div>\<^bsub>\<gamma>\<^sub>F\<^sub>C\<^esub> \<phi>) \<subseteq> Cn({.\<not> \<phi>})\<close>
   proof
     fix \<psi>
     assume c:\<open>\<psi> \<in> (K \<div>\<^bsub>\<gamma>\<^sub>F\<^sub>C\<^esub> \<phi>)\<close>
     { assume \<open>\<not> {.\<not> \<phi>} \<turnstile> \<psi>\<close>
       hence \<open>\<not> {.\<not> \<psi>} \<turnstile> \<phi>\<close>
         by (metis Un_insert_right insert_is_Un not_PL notnot_PL)
       hence \<open>\<not> {\<phi> .\<or>. .\<not> \<psi>} \<turnstile> \<phi>\<close>
         by (metis assumption_L disjI2_PL singleton_iff transitivity2_L)
       then obtain B where d:\<open>{\<phi> .\<or>. .\<not> \<psi>} \<subseteq> B\<close> and e:\<open>B \<in> K .\<bottom>. \<phi>\<close>
         by (metis a b disjI1_PL empty_subsetI idempotency_L infer_def insert_subset upper_remainder)
       hence f:\<open>\<not> \<psi> \<in> B\<close> 
         by (metis (no_types, lifting) CollectD assumption_L insert_subset disj_notE_PL rem)
       hence \<open>\<not> \<psi> \<in> (K \<div>\<^bsub>\<gamma>\<^sub>F\<^sub>C\<^esub> \<phi>)\<close>
         using e mc full_sel by auto
     }
     then show \<open>\<psi> \<in> Cn({.\<not> \<phi>})\<close>
       using c infer_def by blast
   qed 
 next 
   assume a:\<open>K = Cn(A)\<close> and b:\<open>K \<turnstile> \<phi>\<close>   
   show \<open>K \<inter> Cn({.\<not> \<phi>}) \<subseteq> (K \<div>\<^bsub>\<gamma>\<^sub>F\<^sub>C\<^esub> \<phi>)\<close>
   proof(safe)
     fix \<psi>
     assume c:\<open>\<psi> \<in> K\<close> and d: \<open>\<psi> \<in> Cn {.\<not> \<phi>}\<close>
     have e:\<open>B \<turnstile> .\<not> \<phi> .\<longrightarrow>. \<psi>\<close> for B
       by (simp add: d validD_L valid_imp_PL)
     { fix B
       assume f:\<open>B \<in> K .\<bottom>. \<phi>\<close>
       hence \<open>B \<turnstile> \<phi> .\<longrightarrow>. \<psi>\<close>
         using a assumption_L c remainder_recovery by auto
       then have f:\<open>B \<turnstile> \<psi>\<close> using d e
         using disjE_PL ex_mid_PL by blast 
     }
     then show \<open>\<psi> \<in> (K \<div>\<^bsub>\<gamma>\<^sub>F\<^sub>C\<^esub> \<phi>)\<close>
       apply(simp_all add:mc c full_sel)
       using a rem_closure by blast
   qed
 qed
 
 lemma full_meet_weak2:\<open>K = Cn(A) \<Longrightarrow> K \<turnstile> \<phi> \<Longrightarrow> Cn((K \<div>\<^bsub>\<gamma>\<^sub>F\<^sub>C\<^esub> \<phi>) \<union> {.\<not> \<phi>}) = Cn({.\<not> \<phi>})\<close>
   unfolding full_meet_weak1 
   by (metis Cn_union idempotency_L inf.cobounded2 sup.absorb_iff2 sup_commute)
 
 end
 
 end
diff --git a/thys/Belief_Revision/AGM_Logic.thy b/thys/Belief_Revision/AGM_Logic.thy
--- a/thys/Belief_Revision/AGM_Logic.thy
+++ b/thys/Belief_Revision/AGM_Logic.thy
@@ -1,480 +1,480 @@
 (*<*)
 \<comment>\<open> ******************************************************************** 
  * 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
  *
  ******************************************************************************\<close>
 
 theory AGM_Logic
 
 imports Main
 
 begin
 (*>*)
 
 section \<open>Introduction\<close>
 
 text\<open>
 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.
 \<close>
 
 text\<open>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 :
 \<^item> The contraction @{text \<open>\<div>\<close>} : where a proposition is removed from a belief set
 \<^item> The expansion @{text \<open>\<oplus>\<close>} : where a proposition is added to a belief set
 \<^item> The revision @{text \<open>\<^bold>*\<close>} : where a proposition is added to a belief set such that the belief set remains consistent
 \<close>
 
 text\<open>In this AFP entry, there are three theory files: 
 \<^enum> The AGM Logic file contains a classification of logics used in the AGM framework.
 \<^enum> The AGM Remainder defines a important operator used in the AGM framework.
 \<^enum> The AGM Contraction file contains the postulates of the AGM contraction and its relation with the meet contraction.
 \<^enum> The AGM Revision file contains the postulates of the AGM revision and its relation with the meet revision.  
 \<close>
 
 section \<open>Logics\<close>
 
 text\<open>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 \<^emph>\<open>locales\<close> feature and we take advantage of the inheritance/extension mechanisms between locales.\<close>
 
 
 subsection \<open>Tarskian Logic\<close>
 
 text \<open>
 The first locale formalizes a Tarskian logic based on the famous Tarski's consequence operator: @{term \<open>Cn(A)\<close>} 
 which gives the set of all propositions (\<^bold>\<open>closure\<close>) that can be inferred from the set of propositions @{term \<open>A\<close>}, 
 Exactly as it is classically axiomatized in the literature, three assumptions of the locale define the consequence operator.
 \<close>
 locale Tarskian_logic =
 fixes Cn::\<open>'a set \<Rightarrow> 'a set\<close>
 assumes monotonicity_L:     \<open>A \<subseteq> B \<Longrightarrow> Cn(A) \<subseteq> Cn(B)\<close>
     and inclusion_L:        \<open>A \<subseteq> Cn(A)\<close> 
     and transitivity_L:     \<open>Cn(Cn(A)) \<subseteq> Cn(A)\<close>
 
 \<comment> \<open>
   Short notation for ``@{term \<open>\<phi>\<close>} can be inferred from the propositions in @{term \<open>A\<close>}''.
 \<close>
 fixes infer::\<open>'a set \<Rightarrow> 'a \<Rightarrow> bool\<close>  (infix \<open>\<turnstile>\<close> 50)
 defines \<open>A \<turnstile> \<phi> \<equiv> \<phi> \<in> Cn(A)\<close>
 
 \<comment> \<open>
   @{term \<open>\<phi>\<close>} is valid (a tautology) if it can be inferred from nothing.
 \<close>
 fixes valid::\<open>'a \<Rightarrow> bool\<close>            (\<open>\<tturnstile>\<close>)
 defines \<open>\<tturnstile> \<phi> \<equiv> {} \<turnstile> \<phi>\<close>
 
 \<comment> \<open>
   @{term \<open>A \<oplus> \<phi>\<close>} is all that can be infered from  @{term \<open>A\<close>} and  @{term \<open>\<phi>\<close>}.
 \<close>
 fixes expansion::\<open>'a set \<Rightarrow> 'a \<Rightarrow> 'a set\<close> (infix \<open>\<oplus>\<close> 57)
 defines \<open>A \<oplus> \<phi> \<equiv> Cn(A \<union> {\<phi>})\<close>
 
 begin 
 
 lemma idempotency_L: \<open>Cn(Cn(A)) = Cn(A)\<close>
   by (simp add: inclusion_L transitivity_L subset_antisym)
 
 lemma assumption_L: \<open>\<phi> \<in> A \<Longrightarrow> A \<turnstile> \<phi>\<close>
   using inclusion_L infer_def by blast 
 
 lemma validD_L: \<open>\<tturnstile> \<phi> \<Longrightarrow> \<phi> \<in> Cn(A)\<close>
   using monotonicity_L valid_def infer_def by fastforce
 
 lemma valid_expansion: \<open>K = Cn(A) \<Longrightarrow> \<tturnstile> \<phi> \<Longrightarrow> K \<oplus> \<phi> = K\<close>
   by (simp add: idempotency_L insert_absorb validD_L valid_def expansion_def)
 
 lemma transitivity2_L:
   assumes \<open>\<forall>\<phi> \<in> B. A \<turnstile> \<phi>\<close>
       and \<open>B \<turnstile> \<psi>\<close>
     shows \<open>A \<turnstile> \<psi>\<close>
 proof -
   from assms(1) have \<open>B \<subseteq> Cn(A)\<close> by (simp add: infer_def subsetI)
   hence \<open>Cn(B) \<subseteq> Cn(A)\<close>  using idempotency_L monotonicity_L by blast
   moreover from assms(2) have \<open>\<psi> \<in> Cn(B)\<close> by (simp add: infer_def)
   ultimately show ?thesis using infer_def by blast
 qed
 
 lemma Cn_same: \<open>(Cn(A) = Cn(B)) \<longleftrightarrow> (\<forall>C. A \<subseteq> Cn(C) \<longleftrightarrow> B \<subseteq> Cn(C))\<close>
 proof
   { assume h:\<open>Cn(A) = Cn(B)\<close>
     from h have \<open>\<forall>\<phi> \<in> B. A \<turnstile> \<phi>\<close> 
       by (simp add: Tarskian_logic.assumption_L Tarskian_logic_axioms infer_def)
     moreover from h[symmetric] have \<open>\<forall>\<phi> \<in> A. B \<turnstile> \<phi>\<close>
       by (simp add: Tarskian_logic.assumption_L Tarskian_logic_axioms infer_def)
     ultimately have \<open>\<forall>C. A \<subseteq> Cn(C) \<longleftrightarrow> B \<subseteq> Cn(C)\<close>
       using h idempotency_L inclusion_L monotonicity_L by blast
   } thus \<open>Cn(A) = Cn(B) \<Longrightarrow> \<forall>C. (A \<subseteq> Cn(C)) = (B \<subseteq> Cn(C))\<close> .
 next
   { assume h:\<open>\<forall>C. (A \<subseteq> Cn(C)) = (B \<subseteq> Cn(C))\<close>
     from h have \<open>(A \<subseteq> Cn(A)) = (B \<subseteq> Cn(A))\<close> and \<open>(A \<subseteq> Cn(B)) = (B \<subseteq> Cn(B))\<close> by simp+
     hence \<open>B \<subseteq> Cn(A)\<close> and \<open>A \<subseteq> Cn(B)\<close> by (simp add: inclusion_L)+
     hence \<open>Cn(A) = Cn(B)\<close>
       using idempotency_L monotonicity_L by blast
   } thus \<open>(\<forall>C. (A \<subseteq> Cn(C)) = (B \<subseteq> Cn(C))) \<Longrightarrow> Cn(A) = Cn(B)\<close> .
 qed
 
 \<comment> \<open>
 The closure of the union of two consequence closures.
 \<close>
 lemma Cn_union: \<open>Cn(Cn(A) \<union> Cn(B)) = Cn(A \<union> B)\<close>
 proof
   have \<open>Cn(Cn(A) \<union> Cn(B)) \<subseteq> Cn(Cn (A \<union> B))\<close> by (simp add: monotonicity_L)
   thus \<open>Cn(Cn(A) \<union> Cn(B)) \<subseteq> Cn(A \<union> B)\<close> by (simp add: idempotency_L)
 next
   have \<open>(A \<union> B) \<subseteq> (Cn(A) \<union> Cn(B))\<close> using inclusion_L by blast
   thus \<open>Cn(A \<union> B) \<subseteq> Cn(Cn(A) \<union> Cn(B))\<close> by (simp add: monotonicity_L)
 qed
 
 \<comment> \<open>
 The closure of an infinite union of consequence closures.
 \<close>
 lemma Cn_Union: \<open>Cn(\<Union>{Cn(B)|B. P B}) = Cn(\<Union>{B. P B})\<close> (is \<open>?A = ?B\<close>)
 proof
   have \<open>?A \<subseteq> Cn ?B\<close>
     apply(rule monotonicity_L, rule Union_least, auto) 
     by (metis Sup_upper in_mono mem_Collect_eq monotonicity_L)
   then show \<open>?A \<subseteq> ?B\<close>
     by (simp add: idempotency_L)
 next
   show \<open>?B \<subseteq> ?A\<close> 
     by (metis (mono_tags, lifting) Union_subsetI inclusion_L mem_Collect_eq monotonicity_L)
 qed
 
 \<comment> \<open>
 The intersection of two closures is closed.
 \<close>
 lemma Cn_inter: \<open>K = Cn(A) \<inter> Cn(B) \<Longrightarrow> K = Cn(K)\<close>
 proof -
   { fix K assume h:\<open>K = Cn(A) \<inter> Cn(B)\<close>
     from h have \<open>K \<subseteq> Cn(A)\<close> and \<open>K \<subseteq> Cn(B)\<close> by simp+
     hence \<open>Cn(K) \<subseteq> Cn(A)\<close> and \<open>Cn(K) \<subseteq> Cn(B)\<close> using idempotency_L monotonicity_L by blast+
     hence \<open>Cn(K) \<subseteq> Cn(A) \<inter> Cn(B)\<close> by simp
     with h have \<open>K = Cn(K)\<close> by (simp add: inclusion_L subset_antisym)
   } thus \<open>K = Cn(A) \<inter> Cn(B) \<Longrightarrow> K = Cn(K)\<close> .
 qed
 
 \<comment> \<open>
 An infinite intersection of closures is closed.
 \<close>
 lemma Cn_Inter: \<open>K = \<Inter>{Cn(B)|B. P B} \<Longrightarrow> K = Cn(K)\<close>
 proof -
   { fix K assume h:\<open>K = \<Inter>{Cn(B)|B. P B}\<close>
     from h have \<open>\<forall>B. P B \<longrightarrow> K \<subseteq> Cn(B)\<close> by blast
     hence \<open>\<forall>B. P B \<longrightarrow> Cn(K) \<subseteq> Cn(B)\<close> using idempotency_L monotonicity_L by blast
     hence \<open>Cn(K) \<subseteq> \<Inter>{Cn(B)|B. P B}\<close> by blast
     with h have \<open>K = Cn(K)\<close> by (simp add: inclusion_L subset_antisym)
   } thus \<open>K = \<Inter>{Cn(B)|B. P B} \<Longrightarrow> K = Cn(K)\<close> .
 qed
 
 end
 
 subsection \<open>Supraclassical Logic\<close>
 
 text \<open>
 A Tarskian logic has only one abstract operator catching the notion of consequence. A basic case of such a logic is a \<^bold>\<open>Supraclassical\<close> logic that 
 is a logic with all classical propositional operators (e.g. conjunction (\<open>\<and>\<close>), implication(\<open>\<longrightarrow>\<close>), negation (\<open>\<not>\<close>) \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. \<open>.\<and>.\<close> 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.
 \<close>
 
 locale Supraclassical_logic = Tarskian_logic +
 
 fixes true_PL::   \<open>'a\<close>             (\<open>\<top>\<close>)
   and false_PL::  \<open>'a\<close>             (\<open>\<bottom>\<close>)
   and imp_PL::    \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infix \<open>.\<longrightarrow>.\<close> 55)
   and not_PL::    \<open>'a \<Rightarrow> 'a\<close>       (\<open>.\<not>\<close>)  
   and conj_PL::   \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infix \<open>.\<and>.\<close> 55)
   and disj_PL::   \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infix \<open>.\<or>.\<close> 55)
   and equiv_PL::  \<open>'a \<Rightarrow> 'a \<Rightarrow> 'a\<close> (infix \<open>.\<longleftrightarrow>.\<close> 55)
 
 assumes true_PL:     \<open>A \<turnstile> \<top>\<close>
 
     and false_PL:    \<open>{\<bottom>} \<turnstile> p\<close>
 
     and impI_PL:     \<open>A \<union> {p} \<turnstile> q \<Longrightarrow> A \<turnstile> (p .\<longrightarrow>. q)\<close>
     and mp_PL:       \<open>A \<turnstile> p .\<longrightarrow>. q \<Longrightarrow> A \<turnstile> p \<Longrightarrow> A \<turnstile> q\<close>
 
     and notI_PL:     \<open>A \<turnstile> p .\<longrightarrow>. \<bottom> \<Longrightarrow> A \<turnstile> .\<not> p\<close>
     and notE_PL:     \<open>A \<turnstile> .\<not> p \<Longrightarrow> A \<turnstile> (p .\<longrightarrow>. \<bottom>)\<close>
 
     and conjI_PL:    \<open>A \<turnstile> p \<Longrightarrow> A \<turnstile> q \<Longrightarrow> A \<turnstile> (p .\<and>. q)\<close>
     and conjE1_PL:   \<open>A \<turnstile> p .\<and>. q \<Longrightarrow> A \<turnstile> p\<close>
     and conjE2_PL:   \<open>A \<turnstile> p .\<and>. q \<Longrightarrow> A \<turnstile> q\<close>
 
     and disjI1_PL:   \<open>A \<turnstile> p \<Longrightarrow> A \<turnstile> (p .\<or>. q)\<close>
     and disjI2_PL:   \<open>A \<turnstile> q \<Longrightarrow> A \<turnstile> (p .\<or>. q)\<close>
     and disjE_PL:    \<open>A \<turnstile> p .\<or>. q \<Longrightarrow> A \<turnstile> p .\<longrightarrow>. r \<Longrightarrow> A \<turnstile> q.\<longrightarrow>. r \<Longrightarrow> A \<turnstile> r\<close>
 
     and equivI_PL:   \<open>A \<turnstile> p .\<longrightarrow>. q \<Longrightarrow> A \<turnstile> q .\<longrightarrow>. p \<Longrightarrow> A \<turnstile> (p .\<longleftrightarrow>. q)\<close>
     and equivE1_PL:  \<open>A \<turnstile> p .\<longleftrightarrow>. q \<Longrightarrow> A \<turnstile> p .\<longrightarrow>. q\<close>
     and equivE2_PL:  \<open>A \<turnstile> p .\<longleftrightarrow>. q \<Longrightarrow> A \<turnstile> q .\<longrightarrow>. p\<close>
 
 \<comment> \<open>non intuitionistic rules\<close>
     and absurd_PL:   \<open>A \<turnstile> .\<not> (.\<not> p) \<Longrightarrow> A \<turnstile> p\<close>
     and ex_mid_PL:   \<open>A \<turnstile> p .\<or>. (.\<not> p)\<close>
 
 begin 
 
 text \<open>In the following, we will first retrieve the classical logic operators semantics coming from previous introduction and elimination rules\<close>
 
 lemma non_consistency:
   assumes \<open>A \<turnstile> .\<not> p\<close>
       and \<open>A \<turnstile> p\<close>
     shows \<open>A \<turnstile> q\<close>
   by (metis assms(1) assms(2) false_PL mp_PL notE_PL singleton_iff transitivity2_L)
 
 \<comment> \<open>this direct result brings directly many remarkable properties of implication (i.e. transitivity)\<close>
 lemma imp_PL: \<open>A \<turnstile> p .\<longrightarrow>. q \<longleftrightarrow> A \<union> {p} \<turnstile> q\<close>
   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: \<open>A \<turnstile> .\<not> p \<longleftrightarrow> A \<union> {p} \<turnstile> \<bottom>\<close>
   using notE_PL notI_PL imp_PL by blast
 
 \<comment> \<open>Classical logic result\<close>
 lemma notnot_PL: \<open>A \<turnstile> .\<not> (.\<not> p) \<longleftrightarrow> A \<turnstile> p\<close>
   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: \<open>A \<turnstile> p .\<and>. q \<longleftrightarrow> (A \<turnstile> p \<and> A \<turnstile> q)\<close>
   using conjE1_PL conjE2_PL conjI_PL by blast 
 
 lemma disj_PL: \<open>A \<turnstile> p .\<or>. q \<longleftrightarrow> A \<union> {.\<not> p} \<turnstile> q\<close>
 proof
   assume a:\<open>A \<turnstile> p .\<or>. q\<close>
   have b:\<open>A \<turnstile> p .\<longrightarrow>. (.\<not> p .\<longrightarrow>. q)\<close> 
     by (intro impI_PL) (meson Un_iff assumption_L insertI1 non_consistency)
   have c:\<open>A \<turnstile> q .\<longrightarrow>. (.\<not> p .\<longrightarrow>. q)\<close> 
     by (simp add: assumption_L impI_PL)
   from a b c have \<open>A \<turnstile> .\<not> p .\<longrightarrow>. q\<close>
     by (erule_tac disjE_PL) simp_all
   then show \<open>A \<union> {.\<not> p} \<turnstile> q\<close> 
     using imp_PL by blast
 next 
   assume a:\<open>A \<union> {.\<not> p} \<turnstile> q\<close>
   hence b:\<open>A \<turnstile> .\<not> p .\<longrightarrow>. q\<close> by (simp add: impI_PL)
   then show \<open>A \<turnstile> p .\<or>. q\<close> 
     apply(rule_tac disjE_PL[OF ex_mid_PL, of A p \<open>p .\<or>. q\<close>]) 
     by (auto simp add: assumption_L disjI2_PL disjI1_PL impI_PL imp_PL) 
 qed
 
 lemma equiv_PL:\<open>A \<turnstile> p .\<longleftrightarrow>. q \<longleftrightarrow> (A \<union> {p} \<turnstile> q \<and> A \<union> {q} \<turnstile> p)\<close>
   using imp_PL equivE1_PL equivE2_PL equivI_PL by blast
 
 corollary valid_imp_PL:  \<open>\<tturnstile> (p .\<longrightarrow>. q) = ({p} \<turnstile> q)\<close>
       and valid_not_PL:  \<open>\<tturnstile> (.\<not> p) = ({p} \<turnstile> \<bottom>)\<close>
       and valid_conj_PL: \<open>\<tturnstile> (p .\<and>. q) = (\<tturnstile> p \<and> \<tturnstile> q)\<close>
       and valid_disj_PL: \<open>\<tturnstile> (p .\<or>. q) = ({.\<not> p} \<turnstile> q)\<close>
       and valid_equiv_PL:\<open>\<tturnstile> (p .\<longleftrightarrow>. q) = ({p} \<turnstile> q \<and> {q} \<turnstile> p)\<close>
   using imp_PL not_PL conj_PL disj_PL equiv_PL valid_def by auto
 
 text\<open>Second, we will combine each logical operator with the consequence operator \<open>Cn\<close>: it is a trick to profit from set theory to get many essential 
 lemmas without complex inferences\<close>
 declare infer_def[simp]
 
 lemma nonemptyCn: \<open>Cn(A) \<noteq> {}\<close>
   using true_PL by auto
 
 lemma Cn_true: \<open>Cn({\<top>}) = Cn({})\<close>
   using Cn_same true_PL by auto
 
 lemma Cn_false: \<open>Cn({\<bottom>}) = UNIV\<close> 
   using false_PL by auto
 
 lemma Cn_imp:     \<open>A \<turnstile> (p .\<longrightarrow>. q) \<longleftrightarrow> Cn({q}) \<subseteq> Cn(A \<union> {p})\<close> 
   and Cn_imp_bis: \<open>A \<turnstile> (p .\<longrightarrow>. q) \<longleftrightarrow> Cn(A \<union> {q}) \<subseteq> Cn(A \<union> {p})\<close> 
   using Cn_same imp_PL idempotency_L inclusion_L infer_def subset_insertI by force+
 
 lemma Cn_not: \<open>A \<turnstile> .\<not> p \<longleftrightarrow> Cn(A \<union> {p}) = UNIV\<close>
   using Cn_false Cn_imp notE_PL not_PL by fastforce
 
 lemma Cn_conj: \<open>A \<turnstile> (p .\<and>. q) \<longleftrightarrow> Cn({p}) \<union> Cn({q}) \<subseteq> Cn(A)\<close>
   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: \<open>Cn({p .\<and>. q}) = Cn({p, q})\<close> 
   by (unfold Cn_same)
      (meson Supraclassical_logic.conj_PL Supraclassical_logic_axioms insert_subset)
 
 lemma Cn_disj:     \<open>A \<turnstile> (p .\<or>. q) \<longleftrightarrow> Cn({q}) \<subseteq> Cn(A \<union> {.\<not> p})\<close>
   and Cn_disj_bis: \<open>A \<turnstile> (p .\<or>. q) \<longleftrightarrow> Cn(A \<union> {q}) \<subseteq> Cn(A \<union> {.\<not> p})\<close>
   using disj_PL Cn_same imp_PL idempotency_L inclusion_L infer_def subset_insertI by force+
 
 lemma Cn_equiv: \<open>A \<turnstile> (p .\<longleftrightarrow>. q) \<longleftrightarrow> Cn(A \<union> {p}) = Cn(A \<union> {q})\<close>
   by (metis Cn_imp_bis equivE1_PL equivE2_PL equivI_PL set_eq_subset)
 
 corollary valid_nonemptyCn: \<open>Cn({}) \<noteq> {}\<close>
       and valid_Cn_imp:     \<open>\<tturnstile> (p .\<longrightarrow>. q) \<longleftrightarrow> Cn({q}) \<subseteq> Cn({p})\<close> 
       and valid_Cn_not:     \<open>\<tturnstile> (.\<not> p) \<longleftrightarrow> Cn({p}) = UNIV\<close>
       and valid_Cn_conj:    \<open>\<tturnstile> (p .\<and>. q) \<longleftrightarrow> Cn({p}) \<union> Cn({q}) \<subseteq> Cn({})\<close>
       and valid_Cn_disj:    \<open>\<tturnstile> (p .\<or>. q) \<longleftrightarrow> Cn({q}) \<subseteq> Cn({.\<not> p})\<close>
       and valid_Cn_equiv:   \<open>\<tturnstile> (p .\<longleftrightarrow>. q) \<longleftrightarrow> Cn({p}) = Cn({q})\<close>
   using nonemptyCn Cn_imp Cn_not Cn_conj Cn_disj Cn_equiv valid_def by auto
 
 \<comment> \<open>Finally, we group additional lemmas that were essential in further proofs\<close>
 lemma consistency: \<open>Cn({p}) \<inter> Cn({.\<not> p}) = Cn({})\<close>
 proof
   { fix q
     assume \<open>{p} \<turnstile> q\<close> and \<open>{.\<not> p} \<turnstile> q\<close>
     hence "{} \<turnstile> p .\<longrightarrow>. q" and "{} \<turnstile> (.\<not> p) .\<longrightarrow>. q" 
       using impI_PL by auto
     hence \<open>{} \<turnstile> q\<close> 
       using ex_mid_PL by (rule_tac disjE_PL[where p=p and q=\<open>.\<not> p\<close>]) blast   
   }
   then show \<open>Cn({p}) \<inter> Cn({.\<not> p}) \<subseteq> Cn({})\<close> by (simp add: subset_iff)
 next
   show \<open>Cn({}) \<subseteq> Cn({p}) \<inter> Cn({.\<not> p})\<close> by (simp add: monotonicity_L)
 qed
 
-lemma Cn_notnot: \<open>Cn({.\<not> (.\<not> \<phi>)}) = Cn({\<phi>})\<close> 
-  by (metis (no_types, hide_lams) notnot_PL valid_Cn_equiv valid_equiv_PL) 
+lemma Cn_notnot: \<open>Cn({.\<not> (.\<not> \<phi>)}) = Cn({\<phi>})\<close>
+  by (metis (no_types, opaque_lifting) notnot_PL valid_Cn_equiv valid_equiv_PL)
 
 lemma conj_com: \<open>A \<turnstile> p .\<and>. q \<longleftrightarrow> A \<turnstile> q .\<and>. p\<close>
   using conj_PL by auto
 
 lemma conj_com_Cn: \<open>Cn({p .\<and>. q}) = Cn({q .\<and>. p})\<close>
   by (simp add: Cn_conj_bis insert_commute) 
 
 lemma disj_com: \<open>A \<turnstile> p .\<or>. q \<longleftrightarrow> A \<turnstile> q .\<or>. p\<close>
 proof -
   { fix p q
     have \<open>A \<turnstile> p .\<or>. q \<Longrightarrow> A \<turnstile> q .\<or>. p\<close>
       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: \<open>Cn({p .\<or>. q}) = Cn({q .\<or>. p})\<close>
   unfolding Cn_same using disj_com by simp
 
 lemma imp_contrapos: \<open>A \<turnstile> p .\<longrightarrow>. q \<longleftrightarrow> A \<turnstile> .\<not> q .\<longrightarrow>. .\<not> p\<close>
   by (metis Cn_not Un_insert_left Un_insert_right imp_PL notnot_PL)
 
 lemma equiv_negation: \<open>A \<turnstile> p .\<longleftrightarrow>. q \<longleftrightarrow> A \<turnstile> .\<not> p .\<longleftrightarrow>. .\<not> q\<close>
   using equivE1_PL equivE2_PL equivI_PL imp_contrapos by blast
 
 lemma imp_trans: \<open>A \<turnstile> p .\<longrightarrow>.q \<Longrightarrow> A \<turnstile> q .\<longrightarrow>.r \<Longrightarrow> A \<turnstile> p .\<longrightarrow>.r\<close>
   using Cn_imp_bis by auto
 
 lemma imp_recovery0: \<open>A \<turnstile> p .\<or>. (p .\<longrightarrow>. q)\<close>
   apply(subst disj_PL, subst imp_contrapos)
   using assumption_L impI_PL by auto
 
 lemma imp_recovery1: \<open>A \<union> {p .\<longrightarrow>. q} \<turnstile> p \<Longrightarrow> A \<turnstile> p\<close>
   using disjE_PL[OF imp_recovery0, of A p p q] assumption_L imp_PL by auto
 
 lemma imp_recovery2: \<open>A \<turnstile> p .\<longrightarrow>. q \<Longrightarrow> A \<turnstile> (q .\<longrightarrow>. p) .\<longrightarrow>. p \<Longrightarrow> A \<turnstile> q\<close>
   using imp_PL imp_recovery1 imp_trans by blast
 
 lemma impI2: \<open>A \<turnstile> q \<Longrightarrow> A \<turnstile> p .\<longrightarrow>. q\<close> 
   by (meson assumption_L impI_PL in_mono sup_ge1 transitivity2_L)
 
 lemma conj_equiv: \<open>A \<turnstile> p \<Longrightarrow> A \<turnstile> ((p .\<and>. q) .\<longleftrightarrow>. q)\<close>
   by (metis Un_insert_right assumption_L conjE2_PL conjI_PL equiv_PL impI2 imp_PL insertI1 sup_bot.right_neutral)
 
 lemma conj_imp: \<open>A \<turnstile> (p .\<and>. q) .\<longrightarrow>. r \<longleftrightarrow> A \<turnstile> p .\<longrightarrow>. (q .\<longrightarrow>. r)\<close>
 proof
   assume "A \<turnstile> (p .\<and>. q) .\<longrightarrow>. r"
   then have "Cn (A \<union> {r}) \<subseteq> Cn (A \<union> {p, q})"
     by (metis (no_types) Cn_conj_bis Cn_imp_bis Cn_union Un_insert_right sup_bot.right_neutral)
   then show \<open>A \<turnstile> p .\<longrightarrow>. (q .\<longrightarrow>. r)\<close>
     by (metis Un_insert_right impI_PL inclusion_L infer_def insert_commute insert_subset subset_eq sup_bot.right_neutral)
 next
    assume "A \<turnstile> p .\<longrightarrow>. (q .\<longrightarrow>. r)"
   then have "A \<union> {p} \<union> {q} \<turnstile> r"
     using imp_PL by auto
   then show "A \<turnstile> (p .\<and>. q) .\<longrightarrow>. 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: \<open>A \<turnstile> (p .\<and>. q) .\<longrightarrow>. r \<Longrightarrow> A \<turnstile> (p .\<and>. .\<not> q) .\<longrightarrow>. r \<Longrightarrow> A \<turnstile> p .\<longrightarrow>. r\<close> 
   by (meson conj_imp disjE_PL ex_mid_PL imp_PL)
 
 lemma disj_notE_PL: \<open>A \<turnstile> q \<Longrightarrow> A \<turnstile> p .\<or>. .\<not> q \<Longrightarrow> A \<turnstile> p\<close>
   using Cn_imp Cn_imp_bis Cn_not disjE_PL notnot_PL by blast
 
 lemma disj_not_impE_PL: \<open>A \<turnstile> (p .\<or>. q) .\<longrightarrow>. r \<Longrightarrow> A \<turnstile> (p .\<or>. .\<not> q) .\<longrightarrow>. r \<Longrightarrow> A \<turnstile> r\<close> 
   by (metis Un_insert_right disjE_PL disj_PL disj_com ex_mid_PL insert_commute sup_bot.right_neutral)
 
 lemma imp_conj: \<open>A \<turnstile> p .\<longrightarrow>. q \<Longrightarrow> A \<turnstile> r .\<longrightarrow>. s \<Longrightarrow> A \<turnstile> (p .\<and>. r) .\<longrightarrow>. (q .\<and>. s)\<close>
   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: \<open>A \<turnstile> (p .\<and>. q) \<longleftrightarrow> A \<turnstile> (p .\<and>. ((.\<not> p) .\<or>. q))\<close>
   by (meson conj_PL disjI2_PL disj_com disj_notE_PL)
 
 lemma morgan: \<open>A \<turnstile> .\<not> (p .\<and>. q) \<longleftrightarrow> A \<turnstile> (.\<not> p) .\<or>. (.\<not> q)\<close>
   by (meson conj_imp disj_PL disj_com imp_PL imp_contrapos notE_PL notI_PL)
 
 lemma conj_superexpansion1: \<open>A \<turnstile> .\<not> (p .\<and>. q) .\<and>. .\<not> p \<longleftrightarrow> A \<turnstile> .\<not> p\<close>
   using conj_PL disjI1_PL morgan by auto
 
 lemma conj_superexpansion2: \<open>A \<turnstile> (p .\<or>. q) .\<and>. p \<longleftrightarrow> A \<turnstile> p\<close>
   using conj_PL disjI1_PL by auto
 
 end
 
 subsection \<open>Compact Logic\<close>
 text\<open>If the logic is compact, which means that any result is based on a finite set of hypothesis\<close>
 locale Compact_logic = Tarskian_logic +
   assumes compactness_L: \<open>A \<turnstile> \<phi> \<Longrightarrow> (\<exists>A'. A'\<subseteq> A \<and> finite A' \<and> A'\<turnstile> \<phi>)\<close>
 
 begin
 
 text \<open>Very important lemma preparing the application of the Zorn's lemma. It states that in a compact logic, we can not deduce \<open>\<phi>\<close>
 if we accumulate an infinity of hypothesis groups which locally do not deduce phi\<close>
 lemma chain_closure: \<open>\<not> \<tturnstile> \<phi> \<Longrightarrow> subset.chain {B. \<not> B \<turnstile> \<phi>} C \<Longrightarrow> \<not> \<Union>C \<turnstile> \<phi>\<close> 
 proof                                    
   assume a:\<open>subset.chain {B. \<not> B \<turnstile> \<phi>} C\<close> and b:\<open>\<not> \<tturnstile> \<phi>\<close> and \<open>\<Union> C \<turnstile> \<phi>\<close>
   then obtain A' where c:\<open>A'\<subseteq> \<Union> C\<close> and d:\<open>finite A'\<close>  and e:\<open>A' \<turnstile> \<phi>\<close> using compactness_L by blast
   define f where f:\<open>f \<equiv> \<lambda>a. SOME B. B \<in> C \<and> a \<in> B\<close>
   have g:\<open>finite (f ` A')\<close> using f d by simp
   have h:\<open>(f ` A') \<subseteq> C\<close> 
     unfolding f by auto (metis (mono_tags, lifting) Union_iff c someI_ex subset_eq)
   have i:\<open>subset.chain {B. \<not> B \<turnstile> \<phi>} (f ` A')\<close> using a h
     using a h by (meson subsetD subset_chain_def subset_trans)
   have \<open>A' \<noteq> {} \<Longrightarrow> \<Union> (f ` A') \<in> {B. \<not> B \<turnstile> \<phi>}\<close> using g i 
     by (meson Union_in_chain image_is_empty subset_chain_def subset_eq)
   hence j:\<open>A' \<noteq> {} \<Longrightarrow> \<not> \<Union>(f ` A') \<turnstile> \<phi>\<close> by simp
   have \<open>A' \<subseteq> \<Union>(f ` A')\<close> 
     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