diff --git a/thys/Belief_Revision/AGM_Contraction.thy b/thys/Belief_Revision/AGM_Contraction.thy
new file mode 100755
--- /dev/null
+++ b/thys/Belief_Revision/AGM_Contraction.thy
@@ -0,0 +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)
+  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
new file mode 100755
--- /dev/null
+++ b/thys/Belief_Revision/AGM_Logic.thy
@@ -0,0 +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 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
+
+
diff --git a/thys/Belief_Revision/AGM_Remainder.thy b/thys/Belief_Revision/AGM_Remainder.thy
new file mode 100644
--- /dev/null
+++ b/thys/Belief_Revision/AGM_Remainder.thy
@@ -0,0 +1,167 @@
+(*<*)
+\<comment>\<open> ******************************************************************** 
+ * Project         : AGM Theory
+ * Version         : 1.0
+ *
+ * Authors         : Valentin Fouillard, Safouan Taha, Frederic Boulanger
+                     and Nicolas Sabouret
+ *
+ * This file       : AGM Remainders
+ *
+ * Copyright (c) 2021 Université Paris Saclay, France
+ *
+ ******************************************************************************\<close>
+
+theory AGM_Remainder
+
+imports AGM_Logic
+
+begin
+
+(*>*)
+
+
+
+section \<open>Remainders\<close>
+
+text\<open>In AGM, one important feature is to eliminate some proposition from a set of propositions by ensuring 
+that the set of retained clauses is maximal and that nothing among these clauses allows to retrieve the eliminated proposition\<close>
+
+subsection \<open>Remainders in a Tarskian logic\<close>
+text \<open>In a general context of a Tarskian logic, we consider a descriptive definition (by comprehension)\<close>
+context Tarskian_logic
+
+begin
+definition remainder::\<open>'a set \<Rightarrow> 'a \<Rightarrow> 'a set set\<close> (infix \<open>.\<bottom>.\<close> 55)
+  where rem: \<open>A .\<bottom>. \<phi> \<equiv> {B. B \<subseteq> A \<and> \<not> B \<turnstile> \<phi> \<and> (\<forall>B'\<subseteq> A. B \<subset> B' \<longrightarrow> B' \<turnstile> \<phi>)}\<close> 
+
+lemma rem_inclusion: \<open>B \<in> A .\<bottom>. \<phi> \<Longrightarrow> B \<subseteq> A\<close> 
+  by (auto simp add:rem split:if_splits) 
+
+lemma rem_closure: "K = Cn(A) \<Longrightarrow> B \<in> K .\<bottom>. \<phi> \<Longrightarrow> B = Cn(B)"
+  apply(cases \<open>K .\<bottom>. \<phi> = {}\<close>, simp)
+  by (simp add:rem infer_def) (metis idempotency_L inclusion_L monotonicity_L psubsetI)
+
+lemma remainder_extensionality: \<open>Cn({\<phi>}) = Cn({\<psi>}) \<Longrightarrow> A .\<bottom>. \<phi> = A .\<bottom>. \<psi>\<close> 
+  unfolding rem infer_def apply safe 
+  by (simp_all add: Cn_same) blast+
+
+lemma nonconsequence_remainder: \<open>A .\<bottom>. \<phi> = {A} \<longleftrightarrow> \<not> A \<turnstile> \<phi>\<close>
+  unfolding rem by auto                           
+
+\<comment> \<open>As we will see further, the other direction requires compactness!\<close>
+lemma taut2emptyrem: \<open>\<tturnstile> \<phi> \<Longrightarrow> A .\<bottom>. \<phi> = {}\<close>
+  unfolding rem by (simp add: infer_def validD_L)
+
+end
+
+subsection \<open>Remainders in a supraclassical logic\<close>
+text\<open>In case of a supraclassical logic, remainders get impressive properties\<close>
+context Supraclassical_logic
+
+begin
+
+\<comment> \<open>As an effect of being maximal, a remainder keeps the eliminated proposition in its propositions hypothesis\<close>
+lemma remainder_recovery: \<open>K = Cn(A) \<Longrightarrow> K \<turnstile> \<psi> \<Longrightarrow> B \<in> K .\<bottom>. \<phi> \<Longrightarrow> B \<turnstile> \<phi> .\<longrightarrow>. \<psi>\<close> 
+proof -
+  { fix \<psi> and B
+    assume  a:\<open>K = Cn(A)\<close> and c:\<open>\<psi> \<in> K\<close> and d:\<open>B \<in> K .\<bottom>. \<phi>\<close> and e:\<open>\<phi> .\<longrightarrow>. \<psi> \<notin> Cn(B)\<close>
+    with a have f:\<open>\<phi> .\<longrightarrow>. \<psi> \<in> K\<close> using impI2 infer_def by blast
+    with d e have \<open>\<phi> \<in> Cn(B \<union> {\<phi> .\<longrightarrow>. \<psi>})\<close> 
+      apply (simp add:rem, elim conjE)
+      by (metis dual_order.order_iff_strict inclusion_L insert_subset)
+    with d have False using rem imp_recovery1 
+      by (metis (no_types, lifting) CollectD infer_def)
+  }
+  thus \<open>K = Cn(A) \<Longrightarrow> K \<turnstile> \<psi> \<Longrightarrow> B \<in> K .\<bottom>. \<phi> \<Longrightarrow> B \<turnstile> \<phi> .\<longrightarrow>. \<psi>\<close>
+    using idempotency_L by auto
+qed
+
+\<comment> \<open>When you remove some proposition \<open>\<phi>\<close> several other propositions can be lost. 
+An important lemma states that the resulting remainder is also a remainder of any lost proposition\<close>
+lemma remainder_recovery_bis: \<open>K = Cn(A) \<Longrightarrow> K \<turnstile> \<psi> \<Longrightarrow> \<not> B \<turnstile> \<psi> \<Longrightarrow> B \<in> K .\<bottom>. \<phi> \<Longrightarrow> B \<in> K .\<bottom>. \<psi>\<close>
+proof-
+  assume a:\<open>K = Cn(A)\<close> and b:\<open>\<not> B \<turnstile> \<psi>\<close> and c:\<open>B \<in> K .\<bottom>. \<phi>\<close> and d:\<open>K \<turnstile> \<psi>\<close>
+  hence d:\<open>B \<turnstile> \<phi> .\<longrightarrow>. \<psi>\<close> using remainder_recovery by simp
+  with c show \<open>B \<in> K .\<bottom>. \<psi>\<close>
+    by (simp add:rem) (meson b dual_order.trans infer_def insert_subset monotonicity_L mp_PL order_refl psubset_imp_subset)
+qed
+
+corollary remainder_recovery_imp: \<open>K = Cn(A) \<Longrightarrow> K \<turnstile> \<psi> \<Longrightarrow> \<tturnstile> (\<psi> .\<longrightarrow>. \<phi>) \<Longrightarrow> B \<in> K .\<bottom>. \<phi> \<Longrightarrow> B \<in> K .\<bottom>. \<psi>\<close>
+  apply(rule remainder_recovery_bis, simp_all)
+  by (simp add:rem) (meson infer_def mp_PL validD_L)
+
+\<comment> \<open>If we integrate back the eliminated proposition into the remainder, we retrieve the original set!\<close>
+lemma remainder_expansion: \<open>K = Cn(A) \<Longrightarrow> K \<turnstile> \<psi> \<Longrightarrow> \<not> B \<turnstile> \<psi> \<Longrightarrow> B \<in> K .\<bottom>. \<phi> \<Longrightarrow> B \<oplus> \<psi> = K\<close>
+proof 
+  assume a:\<open>K = Cn(A)\<close> and b:\<open>K \<turnstile> \<psi>\<close> and c:\<open>\<not> B \<turnstile> \<psi>\<close> and d:\<open>B \<in> K .\<bottom>. \<phi>\<close>
+  then show \<open>B \<oplus> \<psi> \<subseteq> K\<close>
+    by (metis Un_insert_right expansion_def idempotency_L infer_def insert_subset 
+              monotonicity_L rem_inclusion sup_bot.right_neutral)
+next
+  assume a:\<open>K = Cn(A)\<close> and b:\<open>K \<turnstile> \<psi>\<close> and c:\<open>\<not> B \<turnstile> \<psi>\<close> and d:\<open>B \<in> K .\<bottom>. \<phi>\<close>
+  { fix \<chi>
+    assume \<open>\<chi> \<in> K\<close>
+    hence e:\<open>B \<turnstile> \<phi> .\<longrightarrow>.\<chi>\<close> using remainder_recovery[OF a _ d, of \<chi>] assumption_L by blast 
+    have \<open>\<psi> \<in> K\<close> using a b idempotency_L infer_def by blast
+    hence f:\<open>B \<union> {\<psi>} \<turnstile> \<phi>\<close> using b c d apply(simp add:rem)
+      by (meson inclusion_L insert_iff insert_subsetI less_le_not_le subset_iff) 
+    from e f have \<open>B \<union> {\<psi>} \<turnstile> \<chi>\<close> using imp_PL imp_trans by blast
+  }
+  then show \<open>K \<subseteq> B \<oplus> \<psi>\<close> 
+    by (simp add: expansion_def subsetI)
+qed
+
+text\<open>To eliminate a conjunction, we only need to remove one side\<close>
+lemma remainder_conj: \<open>K = Cn(A) \<Longrightarrow> K \<turnstile> \<phi> .\<and>. \<psi> \<Longrightarrow> K .\<bottom>. (\<phi> .\<and>. \<psi>) = (K .\<bottom>. \<phi>) \<union> (K .\<bottom>. \<psi>)\<close>
+  apply(intro subset_antisym Un_least subsetI, simp add:rem)
+    apply (meson conj_PL infer_def)
+   using remainder_recovery_imp[of K A \<open>\<phi> .\<and>. \<psi>\<close> \<phi>] 
+   apply (meson assumption_L conjE1_PL singletonI subsetI valid_imp_PL)
+  using remainder_recovery_imp[of K A \<open>\<phi> .\<and>. \<psi>\<close> \<psi>]
+  by (meson assumption_L conjE2_PL singletonI subsetI valid_imp_PL)
+
+end
+
+subsection \<open>Remainders in a compact logic\<close>
+text\<open>In case of a supraclassical logic, remainders get impressive properties\<close>
+context Compact_logic
+begin
+
+text \<open>The following lemma is the Lindembaum's lemma requiring the Zorn's lemma (already available in standard Isabelle/HOL). 
+  For more details, please refer to the book "Theory of logical calculi" @{cite wojcicki2013theory}. 
+This very important lemma states that we can get a maximal set (remainder \<open>B'\<close>) starting from any set 
+\<open>B\<close> if this latter does not infer the proposition \<open>\<phi>\<close> we want to eliminate\<close>
+lemma upper_remainder: \<open>B \<subseteq> A \<Longrightarrow> \<not> B \<turnstile> \<phi> \<Longrightarrow> \<exists>B'. B \<subseteq> B' \<and>  B' \<in> A .\<bottom>. \<phi>\<close> 
+proof -
+  assume a:\<open>B \<subseteq> A\<close> and b:\<open>\<not> B \<turnstile> \<phi>\<close>
+  have c:\<open>\<not> \<tturnstile> \<phi>\<close>
+    using b infer_def validD_L by blast
+  define \<B> where "\<B> \<equiv> {B'. B \<subseteq> B' \<and> B' \<subseteq> A \<and> \<not> B' \<turnstile> \<phi>}"
+  have d:\<open>subset.chain \<B> C \<Longrightarrow> subset.chain {B. \<not> B \<turnstile> \<phi>} C\<close> for C
+    unfolding \<B>_def
+    by (simp add: le_fun_def less_eq_set_def subset_chain_def)
+  have e:\<open>C \<noteq> {} \<Longrightarrow> subset.chain \<B> C \<Longrightarrow> B \<subseteq> \<Union> C\<close> for C 
+    by (metis (no_types, lifting) \<B>_def subset_chain_def less_eq_Sup mem_Collect_eq subset_iff)
+  { fix C
+    assume f:\<open>C \<noteq> {}\<close> and g:\<open>subset.chain \<B> C\<close> 
+    have \<open>\<Union> C \<in> \<B>\<close>
+      using \<B>_def  e[OF f g] chain_closure[OF c d[OF g]] 
+      by simp (metis (no_types, lifting) CollectD Sup_least Sup_subset_mono g subset.chain_def subset_trans)
+  } note f=this 
+  have \<open>subset.chain \<B> C \<Longrightarrow> \<exists>U\<in>\<B>. \<forall>X\<in>C. X \<subseteq> U\<close> for C
+    apply (cases \<open>C \<noteq> {}\<close>) 
+     apply (meson Union_upper f) 
+    using \<B>_def a b by blast
+  with subset_Zorn[OF this, simplified] obtain B' where f:\<open>B'\<in> \<B> \<and> (\<forall>X\<in>\<B>. B' \<subseteq> X \<longrightarrow> X = B')\<close> by auto
+  then show ?thesis 
+    by (simp add:rem \<B>_def, rule_tac x=B' in exI) (metis psubsetE subset_trans)
+qed
+
+\<comment> \<open>An immediate corollary ruling tautologies\<close>
+corollary emptyrem2taut: \<open>A .\<bottom>. \<phi> = {} \<Longrightarrow> \<tturnstile> \<phi>\<close>
+  by (metis bot.extremum empty_iff upper_remainder valid_def)
+
+end
+
+end
diff --git a/thys/Belief_Revision/AGM_Revision.thy b/thys/Belief_Revision/AGM_Revision.thy
new file mode 100755
--- /dev/null
+++ b/thys/Belief_Revision/AGM_Revision.thy
@@ -0,0 +1,236 @@
+(*<*)
+\<comment>\<open> ******************************************************************** 
+ * Project         : AGM Theory
+ * Version         : 1.0
+ *
+ * Authors         : Valentin Fouillard, Safouan Taha, Frederic Boulanger
+                     and Nicolas Sabouret
+ *
+ * This file       : AGM revision
+ *
+ * Copyright (c) 2021 Université Paris Saclay, France
+ *
+ ******************************************************************************\<close>
+
+theory AGM_Revision
+
+imports AGM_Contraction
+
+begin
+(*>*)
+
+section \<open>Revisions\<close>
+text \<open>The third operator of belief change introduce by the AGM framework is the revision. In revision a sentence 
+@{term \<open>\<phi>\<close>} is added to the belief set  @{term \<open>K\<close>} in such a way that other sentences 
+of @{term \<open>K\<close>} are removed if needed so that @{term \<open>K\<close>} is consistent\<close>
+
+subsection \<open>AGM revision postulates\<close>
+
+text \<open>The revision operator is denoted by the symbol @{text \<open>\<^bold>*\<close>} and respect the following conditions :
+\<^item> @{text \<open>revis_closure\<close>} : a belief set @{term \<open>K\<close>} revised by @{term \<open>\<phi>\<close>} should be logically closed
+\<^item> @{text \<open>revis_inclusion\<close>} : a belief set @{term \<open>K\<close>} revised by @{term \<open>\<phi>\<close>} should be a subset of @{term \<open>K\<close>} expanded by @{term \<open>\<phi>\<close>}
+\<^item> @{text \<open>revis_vacuity\<close>} : if @{text \<open>\<not>\<phi>\<close>} is not in @{term \<open>K\<close>} then the revision of @{term \<open>K\<close>} by @{term \<open>\<phi>\<close>} is equivalent of the expansion of @{term \<open>K\<close>} by @{term \<open>\<phi>\<close>}
+\<^item> @{text \<open>revis_success\<close>} : a belief set @{term \<open>K\<close>} revised by @{term \<open>\<phi>\<close>} should contain @{term \<open>\<phi>\<close>}
+\<^item> @{text \<open>revis_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
+\<^item> @{text \<open>revis_consistency\<close>} : a belief set @{term \<open>K\<close>} revised by @{term \<open>\<phi>\<close>} is consistent if @{term \<open>\<phi>\<close>} is consistent\<close>
+locale AGM_Revision = Supraclassical_logic +
+
+fixes revision:: \<open>'a set \<Rightarrow> 'a \<Rightarrow> 'a set\<close> (infix \<open>\<^bold>*\<close> 55)
+
+assumes revis_closure:        \<open>K = Cn(A) \<Longrightarrow> K \<^bold>* \<phi> = Cn(K \<^bold>* \<phi>)\<close>
+    and revis_inclusion:      \<open>K = Cn(A) \<Longrightarrow> K \<^bold>* \<phi> \<subseteq> K \<oplus> \<phi>\<close>
+    and revis_vacuity:        \<open>K = Cn(A) \<Longrightarrow> .\<not> \<phi> \<notin> K \<Longrightarrow> K \<oplus> \<phi> \<subseteq> K \<^bold>* \<phi>\<close>
+    and revis_success:        \<open>K = Cn(A) \<Longrightarrow> \<phi> \<in> K \<^bold>* \<phi>\<close>
+    and revis_extensionality: \<open>K = Cn(A) \<Longrightarrow> Cn({\<phi>}) = Cn({\<psi>}) \<Longrightarrow> K \<^bold>* \<phi> = K \<^bold>* \<psi>\<close>
+    and revis_consistency:    \<open>K = Cn(A) \<Longrightarrow> .\<not> \<phi> \<notin> Cn({})  \<Longrightarrow> \<bottom> \<notin> K \<^bold>* \<phi>\<close>
+
+text\<open>A full revision is defined by two more postulates :
+\<^item> @{text \<open>revis_superexpansion\<close>} : An element of @{text \<open> K \<^bold>* (\<phi> .\<and>. \<psi>)\<close>} is also an element of @{term \<open>K\<close>} revised by @{term \<open>\<phi>\<close>} and expanded by @{term \<open>\<psi>\<close>}
+\<^item> @{text \<open>revis_subexpansion\<close>} : An element of @{text \<open>(K \<^bold>* \<phi>) \<oplus> \<psi>\<close>} is also an element of @{term \<open>K\<close>} revised by @{text \<open>\<phi> .\<and>. \<psi>\<close>} if @{text \<open>(K \<^bold>* \<phi>)\<close>} do not imply @{text \<open>\<not> \<psi>\<close>}
+\<close>
+locale AGM_FullRevision = AGM_Revision + 
+  assumes revis_superexpansion: \<open>K = Cn(A) \<Longrightarrow> K \<^bold>* (\<phi> .\<and>. \<psi>) \<subseteq> (K \<^bold>* \<phi>) \<oplus> \<psi>\<close>
+      and revis_subexpansion:   \<open>K = Cn(A) \<Longrightarrow> .\<not> \<psi> \<notin> (K \<^bold>* \<phi>) \<Longrightarrow> (K \<^bold>* \<phi>) \<oplus> \<psi> \<subseteq> K \<^bold>* (\<phi> .\<and>. \<psi>)\<close>
+
+begin
+
+\<comment> \<open>important lemmas/corollaries that can replace the previous assumptions\<close>
+corollary revis_superexpansion_ext : \<open>K = Cn(A) \<Longrightarrow> (K \<^bold>* \<phi>) \<inter> (K \<^bold>* \<psi>) \<subseteq> (K \<^bold>* (\<phi> .\<or>. \<psi>))\<close>
+proof(intro subsetI, elim IntE)
+  fix \<chi>
+  assume a:\<open>K = Cn(A)\<close> and b:\<open>\<chi> \<in> (K \<^bold>* \<phi>)\<close> and c:\<open>\<chi> \<in> (K \<^bold>* \<psi>)\<close>
+  have \<open> Cn({(\<phi>' .\<or>. \<psi>') .\<and>. \<phi>'}) = Cn({\<phi>'})\<close> for \<phi>' \<psi>' 
+    using conj_superexpansion2 by (simp add: Cn_same)
+  hence d:\<open>K \<^bold>* \<phi>' \<subseteq> (K \<^bold>* (\<phi>' .\<or>. \<psi>')) \<oplus> \<phi>'\<close> for \<phi>' \<psi>'
+    using revis_superexpansion[OF a, of \<open>\<phi>' .\<or>. \<psi>'\<close> \<phi>'] revis_extensionality a by metis
+  hence \<open>\<phi> .\<longrightarrow>. \<chi> \<in> (K \<^bold>* (\<phi> .\<or>. \<psi>))\<close> and \<open>\<psi> .\<longrightarrow>. \<chi> \<in> (K \<^bold>* (\<phi> .\<or>. \<psi>))\<close> 
+    using d[of \<phi> \<psi>] d[of \<psi> \<phi>] revis_extensionality[OF a disj_com_Cn, of \<psi> \<phi>]  
+    using imp_PL a b c expansion_def revis_closure by fastforce+
+  then show  c:\<open>\<chi> \<in> (K \<^bold>* (\<phi> .\<or>. \<psi>))\<close>
+    using disjE_PL a revis_closure revis_success by fastforce
+qed
+
+end
+
+subsection \<open>Relation of AGM revision and AGM contraction \<close>
+
+text\<open>The AGM contraction of @{term \<open>K\<close>} by @{term \<open>\<phi>\<close>} can be defined as the AGM revision of @{term \<open>K\<close>} by @{text \<open>\<not>\<phi>\<close>}
+intersect with @{term \<open>K\<close>} (to remove @{text \<open>\<not>\<phi>\<close>} from K revised). This definition is known as Harper identity @{cite "Harper1976"}\<close>
+sublocale AGM_Revision \<subseteq> AGM_Contraction where contraction = \<open>\<lambda>K \<phi>. K \<inter> (K \<^bold>* .\<not> \<phi>)\<close> 
+proof(unfold_locales, goal_cases)
+  case closure:(1 K A \<phi>)
+  then show ?case
+    by (metis Cn_inter revis_closure)
+next
+  case inclusion:(2 K A \<phi>)
+  then show ?case by blast
+next
+  case vacuity:(3 K A \<phi>)
+  hence \<open>.\<not> (.\<not> \<phi>) \<notin> K\<close>
+    using absurd_PL infer_def by blast
+  hence \<open>K \<subseteq> (K \<^bold>* .\<not> \<phi>)\<close> 
+    using revis_vacuity[where \<phi>=\<open>.\<not> \<phi>\<close>] expansion_def inclusion_L vacuity(1) by fastforce 
+  then show ?case 
+    by fast
+next
+  case success:(4 K A \<phi>)
+  hence \<open>.\<not> (.\<not> \<phi>) \<notin> Cn({})\<close>
+    using infer_def notnot_PL by blast
+  hence a:\<open>\<bottom> \<notin> K \<^bold>* (.\<not> \<phi>)\<close>
+    by (simp add: revis_consistency success(1))
+  have \<open>.\<not> \<phi> \<in>  K \<^bold>* (.\<not> \<phi>)\<close>      
+    by (simp add: revis_success success(1))
+  with a have \<open>\<phi> \<notin>  K \<^bold>* (.\<not> \<phi>)\<close>
+    using infer_def non_consistency revis_closure success(1) by blast
+  then show ?case
+    by simp
+next
+  case recovery:(5 K A \<phi>)
+  show ?case 
+  proof
+    fix \<psi>
+    assume a:\<open>\<psi> \<in> K\<close>
+    hence b:\<open>\<phi> .\<longrightarrow>. \<psi> \<in> K\<close> using impI2 recovery by auto 
+    have \<open>.\<not> \<psi> .\<longrightarrow>. .\<not> \<phi> \<in> K \<^bold>* .\<not> \<phi>\<close>
+      using impI2 recovery revis_closure revis_success by fastforce
+    hence \<open>\<phi> .\<longrightarrow>. \<psi> \<in> K \<^bold>* .\<not> \<phi>\<close>
+      using imp_contrapos recovery revis_closure by fastforce
+    with b show \<open>\<psi> \<in> Cn (K \<inter> (K \<^bold>* .\<not> \<phi>) \<union> {\<phi>})\<close>
+      by (meson Int_iff Supraclassical_logic.imp_PL Supraclassical_logic_axioms inclusion_L subsetD)
+  qed
+next
+  case extensionality:(6 K A \<phi> \<psi>)
+  hence \<open>Cn({.\<not> \<phi>}) = Cn({.\<not> \<psi>})\<close> 
+    using  equiv_negation[of \<open>{}\<close> \<phi> \<psi>] valid_Cn_equiv valid_def by auto
+  hence \<open>(K \<^bold>* .\<not> \<phi>) = (K \<^bold>* .\<not> \<psi>)\<close>
+    using extensionality(1) revis_extensionality by blast
+  then show ?case by simp
+qed
+
+
+locale AGMC_S = AGM_Contraction + Supraclassical_logic
+
+text\<open>The AGM revision of @{term \<open>K\<close>} by @{term \<open>\<phi>\<close>} can be defined as the AGM contraction of @{term \<open>K\<close>} by @{text \<open>\<not>\<phi>\<close>}
+followed by an expansion by @{term \<open>\<phi>\<close>}. This definition is known as Levi identity @{cite "Levi1977SubjunctivesDA"}.\<close>
+sublocale AGMC_S \<subseteq> AGM_Revision where revision = \<open>\<lambda>K \<phi>. (K \<div> .\<not> \<phi>) \<oplus> \<phi>\<close>
+proof(unfold_locales, goal_cases)
+  case closure:(1 K A \<phi>)
+  then show ?case
+    by (simp add: expansion_def idempotency_L)
+next
+  case inclusion:(2 K A \<phi>)
+  have "K \<div> .\<not> \<phi> \<subseteq> K \<union> {\<phi>}"
+    using contract_inclusion inclusion by auto
+  then show ?case
+      by (simp add: expansion_def monotonicity_L)
+next
+  case vacuity:(3 K A \<phi>)
+  then show ?case
+    by (simp add: contract_vacuity expansion_def)
+next
+  case success:(4 K A \<phi>)
+  then show ?case
+    using assumption_L expansion_def by auto
+next
+  case extensionality:(5 K A \<phi> \<psi>)
+  hence \<open>Cn({.\<not> \<phi>}) = Cn({.\<not> \<psi>})\<close> 
+    using  equiv_negation[of \<open>{}\<close> \<phi> \<psi>] valid_Cn_equiv valid_def by auto
+  hence \<open>(K \<div> .\<not> \<phi>) = (K \<div> .\<not> \<psi>)\<close>
+    using contract_extensionality extensionality(1) by blast
+  then show ?case
+    by (metis Cn_union expansion_def extensionality(2))
+next
+  case consistency:(6 K A \<phi>)
+  then show ?case
+    by (metis contract_closure contract_success expansion_def infer_def not_PL)
+qed
+
+text\<open>The relationship between AGM full revision and  AGM full contraction is the same as the relation between AGM revison and AGM contraction\<close>
+sublocale AGM_FullRevision \<subseteq> AGM_FullContraction where contraction = \<open>\<lambda>K \<phi>. K \<inter> (K \<^bold>* .\<not> \<phi>)\<close> 
+proof(unfold_locales, goal_cases)
+  case conj_overlap:(1 K A \<phi> \<psi>)
+  have a:\<open>Cn({.\<not> (\<phi> .\<and>. \<psi>)}) = Cn({(.\<not> \<phi>) .\<or>. (.\<not> \<psi>)})\<close>
+    using Cn_same morgan by simp
+  show ?case (is ?A) 
+    using revis_superexpansion_ext[OF conj_overlap(1), of \<open>.\<not> \<phi>\<close> \<open>.\<not> \<psi>\<close>] 
+          revis_extensionality[OF conj_overlap(1) a] by auto
+next
+  case conj_inclusion:(2 K A \<phi> \<psi>)
+  have a:\<open>Cn({.\<not> (\<phi> .\<and>. \<psi>) .\<and>. .\<not> \<phi>}) = Cn({.\<not> \<phi>})\<close>
+    using conj_superexpansion1 by (simp add: Cn_same)
+  from conj_inclusion show ?case
+  proof(cases \<open>\<phi> \<in> K\<close>)
+    case True
+    hence b:\<open>.\<not> (.\<not> \<phi>) \<notin> K \<^bold>* .\<not> (\<phi> .\<and>. \<psi>)\<close>
+      using absurd_PL  conj_inclusion revis_closure by fastforce
+    show ?thesis
+      using revis_subexpansion[OF conj_inclusion(1) b] revis_extensionality[OF conj_inclusion(1) a] 
+             expansion_def inclusion_L by fastforce
+  next
+    case False
+    then show ?thesis
+      by (simp add: conj_inclusion(1) contract_vacuity)
+  qed
+qed
+
+
+locale AGMFC_S = AGM_FullContraction + AGMC_S
+
+sublocale AGMFC_S \<subseteq> AGM_FullRevision where revision = \<open>\<lambda>K \<phi>. (K \<div> .\<not> \<phi>) \<oplus> \<phi>\<close>
+proof(unfold_locales, safe, goal_cases)
+  case super:(1 K A \<phi> \<psi> \<chi>)
+  hence a:\<open>(\<phi> .\<and>. \<psi>) .\<longrightarrow>. \<chi> \<in> Cn(Cn(A) \<div> .\<not> (\<phi> .\<and>. \<psi>))\<close> 
+    using Supraclassical_logic.imp_PL Supraclassical_logic_axioms expansion_def by fastforce
+  have b:\<open>(\<phi> .\<and>. \<psi>) .\<longrightarrow>. \<chi> \<in> Cn({.\<not> (\<phi> .\<and>. \<psi>)})\<close>
+    by (meson Supraclassical_logic.imp_recovery0 Supraclassical_logic.valid_disj_PL Supraclassical_logic_axioms)
+  have c:\<open>(\<phi> .\<and>. \<psi>) .\<longrightarrow>. \<chi> \<in> Cn(A) \<div> (.\<not> (\<phi> .\<and>. \<psi>) .\<and>. .\<not> \<phi>)\<close> 
+    using contract_conj_overlap_variant[of \<open>Cn(A)\<close> A \<open>.\<not> (\<phi> .\<and>. \<psi>)\<close> \<open>.\<not> \<phi>\<close>] a b
+    using AGM_Contraction.contract_closure AGM_FullContraction_axioms AGM_FullContraction_def by fastforce
+  have d:\<open>Cn({.\<not> (\<phi> .\<and>. \<psi>) .\<and>. .\<not> \<phi>}) = Cn({.\<not> \<phi>})\<close>
+    using conj_superexpansion1 by (simp add: Cn_same)
+  hence e:\<open>(\<phi> .\<and>. \<psi>) .\<longrightarrow>. \<chi> \<in> Cn(A) \<div> .\<not> \<phi>\<close> 
+    using AGM_Contraction.contract_extensionality[OF _ _ d] c
+          AGM_FullContraction_axioms AGM_FullContraction_def by fastforce
+  hence f:\<open>\<phi> .\<longrightarrow>. (\<psi> .\<longrightarrow>. \<chi>) \<in> Cn(A) \<div> .\<not> \<phi>\<close> 
+    using conj_imp AGM_Contraction.contract_closure AGM_FullContraction_axioms AGM_FullContraction_def conj_imp by fastforce
+  then show ?case
+    by (metis assumption_L expansion_def imp_PL infer_def)
+next
+  case sub:(2 K A \<psi> \<phi> \<chi>)
+  hence a:\<open>\<phi> .\<longrightarrow>. (\<psi> .\<longrightarrow>. \<chi>) \<in> Cn(A) \<div> .\<not> \<phi>\<close>
+    by (metis AGMC_S.axioms(1) AGMC_S_axioms AGM_Contraction.contract_closure expansion_def impI_PL infer_def revis_closure)
+  have b:\<open>Cn({.\<not> (\<phi> .\<and>. \<psi>) .\<and>. .\<not> \<phi>}) = Cn({.\<not> \<phi>})\<close>
+    using conj_superexpansion1 by (simp add: Cn_same)
+  have c:\<open>.\<not> (\<phi> .\<and>. \<psi>) \<notin> Cn A \<div> (.\<not> \<phi>)\<close>
+    using sub(1) by (metis assumption_L conj_imp expansion_def imp_PL infer_def not_PL)
+  have c:\<open>Cn(A) \<div> .\<not> \<phi> \<subseteq> Cn(A) \<div> (.\<not> (\<phi> .\<and>. \<psi>))\<close>
+    using contract_conj_inclusion[of \<open>Cn(A)\<close> A \<open>.\<not> (\<phi> .\<and>. \<psi>)\<close> \<open>.\<not> \<phi>\<close>] 
+    by (metis AGM_Contraction.contract_extensionality AGM_FullContraction.axioms(1) AGM_FullContraction_axioms b c)
+  then show ?case 
+    by (metis a assumption_L conj_imp expansion_def imp_PL in_mono infer_def) 
+qed
+
+
+end
+
+
diff --git a/thys/Belief_Revision/ROOT b/thys/Belief_Revision/ROOT
new file mode 100644
--- /dev/null
+++ b/thys/Belief_Revision/ROOT
@@ -0,0 +1,15 @@
+chapter AFP
+
+session "Belief_Revision" (AFP) = HOL +
+  options [timeout=600]
+  theories
+     AGM_Logic 
+     AGM_Contraction 
+     AGM_Revision 
+     AGM_Remainder
+   document_files
+    "root.tex"
+    "adb-long.bib"
+    "root.bib"
+    "graph_locales.pdf"
+
diff --git a/thys/Belief_Revision/document/adb-long.bib b/thys/Belief_Revision/document/adb-long.bib
new file mode 100644
--- /dev/null
+++ b/thys/Belief_Revision/document/adb-long.bib
@@ -0,0 +1,80 @@
+% $Id: adb-long.bib 6518 2010-01-24 14:18:10Z brucker $
+@PREAMBLE{ {\providecommand{\ac}[1]{\textsc{#1}} } 
+	 # {\providecommand{\acs}[1]{\textsc{#1}} } 
+	 # {\providecommand{\acf}[1]{\textsc{#1}} } 
+	 # {\providecommand{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } 
+	 # {\providecommand{\leanTAP}{\mbox{\sf lean\it\TAP}} } 
+	 # {\providecommand{\holz}{\textsc{hol-z}} } 
+	 # {\providecommand{\holocl}{\textsc{hol-ocl}} } 
+	 # {\providecommand{\isbn}{\textsc{isbn}} } 
+         # {\providecommand{\Cpp}{C++} } 
+         # {\providecommand{\Specsharp}{Spec\#} } 
+	 # {\providecommand{\doi}[1]{\href{http://dx.doi.org/#1}{doi:
+	   {\urlstyle{rm}\nolinkurl{#1}}}}} }
+@STRING{conf-tphols="\acs{tphols}" }
+@STRING{iso	= {International Organization for Standardization} }
+@STRING{j-ar	= "Journal of Automated Reasoning" }
+@STRING{j-cacm	= "Communications of the \acs{acm}" }
+@STRING{j-acta-informatica =  "Acta Informatica" }
+@STRING{j-sosym	= "Software and Systems Modeling" }
+@STRING{j-sttt	= "International Journal on Software Tools for Technology" }
+@STRING{j-ist	= "Information and Software Technology" }
+@STRING{j-toplas= "\acs{acm} Transactions on Programming Languages and
+		  Systems" }
+@STRING{j-tosem	= "\acs{acm} Transactions on Software Engineering and
+		  Methodology" }
+@STRING{j-eceasst="Electronic Communications of the \acs{easst}" }
+@STRING{j-fac	= "Formal Aspects of Computing" }
+@STRING{j-ucs	= "Journal of Universal Computer Science" }
+@STRING{j-sl	= "Journal of Symbolic Logic" }
+@STRING{j-fp	= "Journal of Functional Programming" }
+@STRING{j-tkde	= {\acs{ieee} Transaction on Knowledge and Data Engineering} }
+@STRING{j-tse	= {\acs{ieee} Transaction on Software Engineering} }
+@STRING{j-entcs	= {Electronic Notes in Theoretical Computer Science} }
+@STRING{s-lnai  = "Lecture Notes in Computer Science" }
+@STRING{s-lncs  = "Lecture Notes in Computer Science" }
+@STRING{s-lnbip = "Lecture Notes in Business Information Processing" }
+@String{j-computer = "Computer"}
+@String{j-tissec = "\acs{acm} Transactions on Information and System Security"}
+@STRING{omg	= {Object Management Group} }
+@STRING{j-ipl   = {Information Processing Letters} }
+@STRING{j-login	= ";login: the USENIX Association newsletter" }
+
+@STRING{PROC = "Proceedings of the " }
+
+
+% Publisher:
+% ==========
+@STRING{pub-awl	= {Addison-Wesley Longman, Inc.} }
+@STRING{pub-awl:adr={Reading, MA, \acs{usa}} }
+@STRING{pub-springer={Springer-Verlag} }
+@STRING{pub-springer:adr={Heidelberg} }
+@STRING{pub-cup	= {Cambridge University Press} }
+@STRING{pub-cup:adr={New York, \acs{ny}, \acs{usa}} }
+@STRING{pub-mit	= {\acs{mit} Press} }
+@STRING{pub-mit:adr={Cambridge, Massachusetts} }
+@STRING{pub-springer-ny={Springer-Verlag} }
+,
+@STRING{pub-springer-netherlands={Springer Netherlands} }
+@STRING{pub-springer-netherlands:adr={} }
+@STRING{pub-springer-ny:adr={New York, \acs{ny}, \acs{usa}} }
+@STRING{pub-springer-london={Springer-Verlag} }
+@STRING{pub-springer-london:adr={London} }
+@STRING{pub-ieee= {\acs{ieee} Computer Society} }
+@STRING{pub-ieee:adr={Los Alamitos, \acs{ca}, \acs{usa}} }
+@STRING{pub-prentice={Prentice Hall, Inc.} }
+@STRING{pub-prentice:adr={Upper Saddle River, \acs{nj}, \acs{usa}} }
+@STRING{pub-acm	= {\acs{acm} Press} }
+@STRING{pub-acm:adr={New York, \acs{ny} \acs{usa}} }
+@STRING{pub-oxford={Oxford University Press, Inc.} }
+@STRING{pub-oxford:adr={New York, \acs{ny}, \acs{usa}} }
+@STRING{pub-kluwer={Kluwer Academic Publishers} }
+@STRING{pub-kluwer:adr={Dordrecht} }
+@STRING{pub-elsevier={Elsevier Science Publishers} }
+@STRING{pub-elsevier:adr={Amsterdam} }
+@STRING{pub-north={North-Holland Publishing Co.} }
+@STRING{pub-north:adr={Nijmegen, The Netherlands} }
+@STRING{pub-ios	= {\textsc{ios} Press} }
+@STRING{pub-ios:adr={Amsterdam, The Netherlands} }
+@STRING{pub-heise={Heise Zeitschriften Verlag} }
+@STRING{pub-heise:adr={Hannover, Germany} }
diff --git a/thys/Belief_Revision/document/graph_locales.pdf b/thys/Belief_Revision/document/graph_locales.pdf
new file mode 100755
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..de82b63fc62377704afc6b23a3a81da12b89981e
GIT binary patch
literal 13771
zc$|fM1yo!~vv3IR?l!mum>JyNEx0>_J40{?4uL?>;1b+|y9Rf6w-5p$3GVR2?!NEs
z+kNl+bIzUauBxu8F1tPF)X=?_lx797aiP%l<oC4oH1uSnfB`^&lbJ1wpdh;<#L)_B
z4d8f!sIg1i*h3+%?9%q8P>3YN+{pqWER5m?b%mHZpm=7q>nX&pNTYQeYVRAE6iJMe
z0@3V^;Jp=UMKQ%3{iqi4tl92w?+2%3^}OyTUvdSNJLpNc$olUN#8u=TZ){~x#mwuB
zo6~~nrc&hn?jLS{A7buoz`j5Eb(<aBr!DADdJtNkoi%V#!t9kbH`MCgXWT<6f+oz1
z+eT{sD$F;8#3?wkZzBF%wOl-10y!Lv6B(5A%OqSG7is&<QMoA#p`HPSL$}>o%<9#M
zO3O~b@uSs`gG0lk8&2QyhklW()3KRN<c&SfetRWqifn(<fV&qSKIRpq*$-E~RnYw4
zujYa}9=@Bw=L7bb++<!i%oLr1_kwK!K|lG_)@zyQVgrYC7}8zYOi?)%vIcZtN_@p{
zJy~*=kFrRiJ1wo)Tl?8j1}VbuP*v>ZAL#$K>gFlP-^5i?TYJ^MD03@qaDQ?2w)5tK
zJb$U<V<YA7aC^UO7o|i6itQ-7yXv|tRR$xxcacmn!e5vPq6;hxWNSCQGT>m4aWlf-
z3OR@8XV6I`yoze@zLY-9dXw2-S~V1pz)k!!oVlw)l7l;9h<q*3*S+N-m!N{A4SE)V
z6H35veRA~yYnSd7d&OJsRig$n=N$@3rkBx)j1nGx#@;E=xBLedT@7svW4=ycW=MkU
zp0?bsNkqG)@Gw%S6qs|U#<t9hhyItXE@FZ(K;$)C#TDnp%ZjTZTt;nR#^%@FQvyJ_
zaeazHg#IG_7+#DGs=0SB<jk_P!XT*x#d{^Rl!wAHbXN&^yIhj~Gu&HAe90JkR~*@#
z995Jk3+s5ul-4i*;`NEo7#g)q$zAY^SmmworFItmQP})Ziinap%u3AkNk)Oi*1nD6
zd$&finOqb`verz)FT_QiB5PkX8^K4GJK|=+(jdt$=|1ago%hB=^q1wF4KGcHWJy$W
zisG!>4@BOCqt)enMB50iQbn#+SL}yGSeAfXZ)}1K?;Ko|KG}&3^yVORj+XZD_ew$N
z%JIDfbFw#Kr}f>V@wsxzn)+itG%m&?%6Wl+^jBT1gKmen8FY;=7|B&91`e)`Sl;z7
zefmmFlE0ouIrHj+s|fOI4jiVh?ny>t@utajQl#~_E0gWz2X#3bkp-9pp2+RdGE2*^
zqx1%CS0cmR&h5uI=j(q28Sf#}BJLy*YQJqLBmz2j36qNnXKDg;#0!U@LDS?(=D|+*
z#L_6f*qo=-=}5`t3r&Jw4{P?kng|4$SoiNIzbnb&uy1*Z71DNCW`Cl)P6|a!mJ$`O
znOdCmw7?KmkfV1AUbLNZ$F-U^<7i{(axXPHpaLZIXo`G3F6kYtad~M9?P*a7*Hb7U
z&`@B=DNG-oB}Zs$DxT`cV3Mhir)lq&UrZcXmiH9xeno;Cx}eJ!i0L3h)VbOZqdS+{
z@Pj8obwV~Bw|lppB<aJtCe6uVTPn($13a-vY*4)S?ZY9V!EO4Dj0x733$bDqJ{Dnv
zSE3$v)X!aNaZ(nXJ-pWr798_Buig{u+Fn`_NTaETDDNc6z8DI%5Xyit>Ay-#spl&j
zGur^bP>E6@cLlUi)Dr%P&18Oyo^nY&SwgG!Gj8fy(tMZI+~QK6g8?}LqRg`HN*z&6
zedE>C7RQ=SEg6H=Or&Zabx>xai);igP&yd%ld|TLA8Lfb#h6C%#WP_+Z>Si`pz!sy
z$W}TWY5%A%km*_Grh>uMAYJ#XC>R^`vQ>smJh|H4yvLi2rifdz!bm(9(w{8g?U@Dj
zE1+G`Oh8BVi^-t_y$>qIv#{bblZblGVhVxx`F%pbX=gg(Gz;Cjxz=>ijVU%(!oyEz
zuJWcKNb}U4@&Vl2Ufi~|3@k22*#r)=)JmbpP0^#gbKWK%zBkK;5q3m!dz=#!i*Ed7
zUlocNXKWTU^~FH)3pxSgI?~+9#RHhDwe?`b3DX+6an}PhzRUrkWtr=I?s@jz(ap5n
z#Hny)6>2u31G^={pw~BWYEBO^c};j1<9Uu&0I4wKbE-sw($pxmY8-%D*;`NvAHHl>
zfBj!sYKP^{-pWS(?rf4wQ`cr3o%q#2P+IRhmX0u%uB6Pl@eWv>7cDaSmhr*e9N&^E
z;rP+0s^}I{AJ}$juTtSXkrHXwJel2&Uz{gbTM~mMrt=UH0%Em>8Yicc;6g0pJ>#{~
z&ori(Vbh;$Tv<cfrN~Kh5rhzDiDNiAk+d$1W56;UcgSvtS|w93XKS+E?>pT{^ACJ_
zDq0HM2%H|427}g4jD*IbQpCrLY1&Nnf%}b6|AqvMm%M97@CwcQlQf|n9(b@8ZLnbF
z5y2aJp*Josz2OU`!SM*>(k2E7@D4Z@JG5I7Rm`{ONC^sFacD|4<;%9~u?aqUZ?GAN
z_@*?7?^145<nr*YFpqS*UM4FPted}P+NX^EfO51BL%@kxqjsRGdrQ9GhucYdqs)Q8
z5jjrRXq6v~OLKz(Ih*s}2=o{>X#MK77oGSKa<@t|wr)P*$YoMOvA;<aoG3Cfq$y;L
z6FCQ`i%!eYjN!iDMMM_L>LYtV1p5;EYa2``lgUYxi`4W=sSO}5K9g@&KsEKJLqVxY
z$&9HiT~?hi#4ozuus*ZOLS{*!7!>zTnSF<1niLPTGVY)FV{?1gYdKbjJ-_Q(@MysN
zrPUjGZ!J6<y}1jTNqM<nA-T{N9^|^J*)VTw#0&OetfQ(IuJyKA9qlTcMK1(e0h<$W
zXW!3+s@WmdudImqw~*GsHwi2=RAR<o-n_`bgS$Ttrm)@LBL6ZrUsP{Vd(e_wVOuvG
zbc`QJ$D$YfaJT&~_wa(OMtNkr;#C-RQc%XSr$s~tdZhe_|I938&RwFBGdlVX3&Fm=
zJk3|j+La$6aGB;ty2goDapG0*3pO&|1R;G;x!~7hzxEf9VrM@CPWlrWhnSPCBPi^3
zRmV^%NRBQZkqFqS6)-QL^m3@4`GpnYX+@tgMQ}N-M8aqkx9ufQfsd|c><cHfn#rKI
zuA(oegafCD^WEWWRB)mWmBg3@4&!EH9zv>h{nuV9OlG&J%uaBPj{Hy?V=|hEegiGW
zf$}O7uj~se3#RhVPiRpXDN|v3@x4vaONmgHi6fXHxX@!4@2yast>-l=Bh-IMOYuQM
zM74`f`J5Vp8Ob5#Gm6|?a=yKDMLBtfTZ95}wD{|4^)!3FjiGS-bu9yP@N)hK$n~$g
z8u$NkSNjVO0)RL<z?^@-xvhEo_~L2S{4VhyWl0#NNwpY6Q&b6qa~8+Jd5I9m85?3U
z84@Cj5MnW?NI?QNw|p_B85CjmfsT2^2oHv`>@5IS6h><3X7L=x&OqC+a)Iu%x5onE
zpwt5X^mVDqWyst8%ln@mk1ayqv-mZO4rWVA)r*v^J{^q&^~&-iDfEUFJp5jvY(FKT
z+U2D(anPZ_Up(=s#rjDTqPsxksCToOdpLp9&4v3(XmPfsrkZE$(Mmj8S)5EDE%>2p
zs)WTAiP#+vqG&DMJ2p+OXHSDkywt|&eF{D7iNygg#~cmlOQ1j0UjAyvU2%PER=DR0
zPhTuSqcR^|Bv`&v2#%$n_YXf36vrV5mx$Z9bnSaVwbN?h-6TZR;V~cBvlxTjtt>;f
zDbo>+WV_4V<Ju-&HbaUN9Vtg&+n1JMrl3@dso=pI9_x(!6K!H}v|KfB=y5(uWSo+r
z@whDVeR=*w6q_TC92E-^@s*mRp{M-mqgDMRlQH5Dss-he3$_h;GkLZTTQ@lkdqNT8
z8P?Ko4zt(~Ys__#_Ea8^7M-MnB#EcIF#%hpGC$-`oOn-6PiPV35%4yPc}iz7hYmjy
z!c+Df?)ul@`mC#9Y@JdW5I2IY2JaQ|ZOqrLv=amdg?I;!CdIkU9=%U^U(rTkml;IK
zeF$O0UY2VabQ)xBLP2ErKko{N>pew$ed_ai+;UpnQCuZ$JeG)8qTlUN4yQmQ&b%De
zJs?d`LRV|Rs~++LeY6&B=J5shPZ}l9+b!5xH&}sltMcndKN~G`BiXI>M04v+avS`E
z2P*G<zPf(>?a@$F-+C^$va&r5Ed!6EA18K}Nn@{AQ$c>q8r7b|a|xAc8qlx3$e}wY
zu5SI7u@p&3eA5YAZ<f?wS*oj<1&LM8*m}l5-ddo7irFKpQ-ca-e=!|jjr3ch(p~Hk
zo7XA`7Mz2=u=oCs8aYW!QcWD7#61YrA@IKr&p9-wzOZl0FDgF6L-YyKO;MyDk?;&z
zj3lPm0=`O7kNO=(Op%Rs`>uOIEoJ1>drAAIwL!7^_<DSKvx1Ry0fhrqnSEuT;-w-c
zNxx-+qr}S~WTZZ6pYAoFH_Gd`#D?IKbgC9fFP#jVND-{E40U~Q&(@pUe#?n>bY7OP
zaZ;6~`Z;IJ^_bPH<1`r#Lx29r8u!6WABy*`1Z^T;RaU;Q_TN3SP~aE%6{Fi$4ay>}
z1~vNH4x}QQFJ%$afhu3sx7j*poS;gGM^AA2gp4~OD-WE`eIzu$W0p>^c}N~KiB6>m
zF4b%F<&&S9&&({K$gQjGm<jOAF^`l1`tY~D?;m$YPD|IA{}j;!J5k}$EC1`fZ}fZ&
zI8>zEURNrZENErw5Iyt?KkYu^OQ%`vt$g?jc(LfDXb^5Js9y}Vb*+YYo|0e)$G(?;
zZ<g61@RiFC2D8r#gyshjd6f*avN$GkmtlZUJEEVyk>LvQ4%iA_kk0z}{6S{`C;Bs~
z#enB%b^b3hN0p*EYP_#E*2XaPY53OIX1)X@$jxD3lhwgjnU>44H_F#H!-23Cy5-_=
zh<$^u@`7~d2OB4r0w`FMlMo|1tiAdEUSgyO|2cEIHLvEutxB2j`q7;6=&#=0)p!$i
zV!wuMlj<}U)CiJTlfgpL2c#OGbsUimwZ-ME?$M;+b(5`>kFeE%lM6yd&SZ>$ok*v!
zRX%rqX<aQjD~BA=Ua1G1^BNaQJ%)$kS#G#r)^d&thCtn9iZCKN2Ic#t=K8O5Stop`
zwv`(Asz^1wY_+>Mpe(&`Y6Mtd;m9m<eRS}-sSF2oh#H*W4E+vA;n?h!gLJTZIa$*T
zJ!<_X;CQ`Q+CKU<PDbuU!U`es*RRfLMg$)V<I)+eyi<FQ+*lSC?Gc88_<^qb7J12i
zaw&x$a(b>ZjHFd-SdUyMQR}mE2EN%4n3+K;1bLPOXNOBc#bcVrW9`LUy*k$P+tRLW
zRHPhQ2kvNGj`s8pnA{_5R1@zKLX|U%+FH~JeyYOb%=&6Y4^q7{vT>O-0I*wQ?iqcF
zR!C#pA9qwuBy>Ba)s3*y%9&9&6iB`3_jOI*A@F*|!W4eeJkxJ!Zks-T6zJ~OBBi6<
zo^ugFY}f4WW_QWarC6E0cSsRgw@mYrin<RB){-7Z7jqnpFRjYWyC;{C6z6A5%0pUq
z<V6eFhPse_2<wRs;$VS=Oa)4I147jq&Dwavc{76!b9lYoahEJU1roY{GU5bBM(2@Q
z%=-5VhSwKS48qXR2IY}9monY}q0mFA@aa5QpNMy1hqi2JhP62tZ{q-@e%qomyQn>V
z>(S%=4h51(gMlZg#%@;aDn|CS_=dp&Sg;d#&;%<K=1-u0w5-iKogk~UX!hjeJ`^LG
zoqD2AA5aF@13N0C1Ib`e?be!TL(dk-GxsVjRIY&~&@>U!sNu{md0NUt>169j1w{)^
z!7|fx{;aQ9n!ePRA$=%PQpqnBzBIL2H1=iMyXY%Be{sVcvsC$A7NFBdn5D4uKt+fs
znugf1t9_C_1gz0{Wj1D0!rv}DH(Ds5X!BvPuz-#sf!`P`1GUU7E}M1#{$}6X-H$&r
zu5YEd<dir89`O}*pAjlk)wg+8BPfhG*K{#S4fO}HSC(o3+9DfXm44a6NyXJ`gEVeL
zo!f8IUch^F=||f`-|utl9t8`O!CEO7pxsel%T>fx%xQsXOtsE4W(%XsA5m+-L-Q2a
z#(@jvj-+HKwBsGJ^#MNGIA}aW;R=+#+<|-?&MuQZaOa1+Fk5pEau6=TkT;Hit>+if
z58Y@}1EpNJv7c;&w>CED+D{%3r^{4C1q@Dw75z^j-;IkVWH%(bwXFiJ{2$|>&H-qj
z?@=|rIH<@?+{4#>V7=G9(Yh%*<Bu-5Sc}9b3hs~(XFg8M%umNnm`=#Rm^a}`nG9gE
zkFOs=_TZ=b5%Lz-lGjvFldBKeDs%EML_6a*?-7=}csuUiG=?REv$FL~Vmv0lDK4G1
z+CyAo*l56~e1Y&m%@Ags1$6=`vWx79nsqX21?)sD!ZTlk*Iovbd<?!MA4BIM-B8~t
z<UWmnZMdUtsk73&iS*er!*-4BSY$#*iHLmOikv1<47xryq}*St$;Y@{dcQ^4n!2{D
z@w$*?(_iA|c6Cq8#FElEv?wfl7NmcDlO2rDluBY4NYTAf<J0hl94U)%DQnFkmvDUI
zt9JH8`@v7_Jj&W?r^hOk9b~_LzZhW-EY#FjDD+tiv{>lX^yy9f*+ac{^>XgQtRwoN
z7G0fE#hGMk`GZ+LR5gi<+k%d>sIUrl6tD!1U4CqthY87K=6k;I2C+~bJybhU3lYzw
zkq6A{xd1+l<Oh+dls)J7+PN5dX7s3i$dRJaXk}aOAzyhjlk4@O(LM{&7@p0i;4@b^
zFQW))?bnF6<DZm&unTQMmvixV5yRG0Hu`XFEoi5T{g8{S%X0`*7p0Xa1+>F!JdS%<
zp}Z$ozk}h(4aoIhYzmJ4PF#fBAP>Xm;k?0H_Ul9cmle8G8{cm^6&S<b;#pTPCZ89~
z=&8wKlecxN)=R@(g$xS9<Ggu`!g<brw^2|`_jn7HPs6Ggg`)`Ve*cmmUYOwRselO*
zvY!nW7yV%)#CYZBy%@8eN2`j-CY14sRx*sSCWRW5pdu+=NzrmPDQ1)8Jy;N8#9R=C
zQL(A|AqTOR0^w}3DBRq8QA}V~T@6(531_)aBxW!hV>dkv=YVa}I`PBHIb<SoR|~ur
z2gP4e@d>R_w?8t1Z|x7Y=-4Y0HjbPZ;w-kY$4ExIdsECfY|t#nCG8pIjL-<<bpj!G
z#X%bSU+@?QRcaw#U{3B4cCJ?U44ze9u-oqLZ`U{SKHs)R&)<h_5c&I5J@US<zJ@h+
z#U|^KI2mN`^Xg6k=~b`}CHB<N>+^pUacuI7aq=t`eYFg7^VO>e#bXF$VoL0#t&)=?
zP!KP`Jl!3Xr<6My3MapwOu{6;#u^X5@hu(=7ko!n6OuGr=7_<gTh2-CGKc3A{sV6~
z<SM$n`xy6Ku5+6p@eyO0fXJMsoE+<5w)KoBxJKG5-bCX8uZg5iE}E4Nzd`8YN@n9;
z`)V)A0a?avb9^VDX}c798J!v!N}@EB3y+R@V`NxgSjPsL*vmxZTGjMu&}Oab8vNE;
zkTJ}+T-8i>7gg9wC}?oBlhW3ev3w&&S!JB(Hyvr5VLx|>PP_Kur?Z~A9JBFv1ulj(
zwB9hLmH}iCLq_2Q48z$}TLr*lvR9Z0K!ksyr%}@<Rq|3@7vpuOmxXbR$#gM?%e4Iz
z{=)6gMc>!8q(sT4MS=~kk4`B?P6opMj|~s#_UEYDzn7%&x1`nvZrxPBeF|h>vTAm9
zg-4D^s82&npNW%==qcQ4TZ$wuU;9~l#&={n|2mTR)m+AVD-YgGbibv^1oZQz$vE^r
z&yH~fE^A0As>J~Q>&z&&lf;azVjlV!QA38DT34!Yv4Py}lX12Q26*)oq-4Jfr*<db
z{q?N*IhTpjWx6s-J-0CdCo<20>tY+F71pV?zRq>e+w!T+wUgdu^v~CBd*k>lGaS;!
zD_YIpb5|CM5)FNnyvBD~z%oXD?~P+td?xv{PX}!7XXulw^;o~;7k^XAK$oq@jHpQi
z@tsZj)?``+ISYzpP>8D~`@qw&wpf^ssDHFFdL{7Akxxe%pI}iZ<3<P(lVUei$j5(w
zhd%R`e0hz_IZaIE1D+anjH05P95D5a?4zy1wmT6Ea*AYhxzTJYkzGNo+>tDNJ)WFM
zpk1!$80s+N^@(Vz^@4a*QI&~VU`5xSs(5yDcjNv<<C?DLsa+*LUTj8gZNSK#%UCLh
z-HqL67G*WtT(73WaPv_TS!O2OT2|;c`P##HW<P$8bhYp1>K==^BN*gwkXCZnF_PX4
z*7nHVZr-u0)1(rsAee(%Pb*#-e&E*4L|*+(+3|3I=6iAfjlJB@b0zG&(;F(pA%3HA
zL$+#SdXld`J>cimaZdTGeWR?rNZD60*I%D)+|(s_r;58Vb1yeGJVEg6H`b1+04BL$
zh?n!R$@bP6)-(o1i)Zns>D!t!wL6n<QMJEcGn8T^&R7H%oB{&w!jEUQnkG)inmp(}
zRqRDIn{d(}Cg>(BOege83Jnx4y;lS~)~5J*tus4WH!U!~!ToXKd7?+LdWFc*dQ&}3
zwU$Hhq5-d5!{X3XET*tkyTv%oJ^K25p^L&BuB9X3#PmBe@A2UVu=WP?xNO7kc<VCb
zKDNquy`|;x7X8@3L8eo$TFsa$nO>iB*|dp)sGeXx?(-DZ8={gkI*guo=8M4gp+vp!
z9I5B_1uEIghi@qme>jVNgykp0dL!Bn%S`^^+uL-uu`wt!(Ff+UygoJ`KQoe@<lrxQ
z03G|hed-1A;o$US2cm{C_9H>RpQ|F9dEXQbJt~(z1qKLT_HWlz!@{A~LV?{84;#w@
z+1{QT1SFVBI*q@&TKwR2sf`NeXyYwf4b5pX6lCk?wm!dn!_77Kg@4ptSO#oYeEQW!
zigl*oXa=muI^vG>n*A++F^h4~5IPe}58Azp6ZBk<Sh&QcC)mEQQ;nff!V0q!36H~{
zQ1<_}RT~dC&yiX5IgS9#W%~V^P$b^_4X88x+WEAhh+%b=-Vc!3$NV_f44KAYYQJwF
zO5E{95Kh)>QvQw_?UY_@<r%bfPi9FIjh@3?)wI;wWT-Ym?$JAeu<Az?;0+cd!_a{o
z5TV=2z9`RpQ8i3!o0JM*h|0yc)blmeTjeG(;<h%c_|_@h{}6mz{`jNeLHl~nmb{wa
zGMK$dt|@#jQd`%(1&$~gIQqTn1d6JlRQEmdduMZKTu@Y$p~AZwR1*%mv4oyMA5KS%
zP=b`R9rEb(S!1b7Aib;quTY_AFH-k@9jlEl9ZG4EKAiZJ`0^>+1l(gqTjjE|W;Lw>
zdquv~?t=W3u^{^L?~`Y?H=Ke~DO~4uOTkDLS##EC2nH|0G#2{4&7|+XZsz6Q4rD!4
zpz(3O4cc|ToUP;*vO8Qk9V(geQ}NvwjGtYvsSX~xa&vMkb2)VL{4I-s+H`TpZ}SD6
zJ-*5K+U(5kB{4g{Y>;wgUw(WJk8=iSDyNS+wWlW2Sqp7>`=#A-fln!E-HC2Lwf0v7
z&Bw@|ff$gA|7vH#mx=cK?31$FA|U&@lh9+NpcZQXhqxH`(3DR*o>}|ny(zM12!69x
zlg@9zvzo5T!vohOMCk+e@Mr<!SKsbC^0EV~MFRbz1?YrW+~w1a!e|Q-<{ibZQFA|*
zm~<1(uuTPpV^R#Bb{zdC05-oMT4~xZw)V1vt`KzV?yptD`rHDI3uZ1+Xyn*Ru-)27
zw9UL->8XZFZY1B+I~kM;n?w8eA;Rhiw02;yPVG|jsMUOp`NwNusv#SdVaHXMtGSse
z2BT(p2E>5|IMK3`u2EBCn))?A{o#J&k-zF_esI}o{m1>@=l!+xN9y}3+asaI3cbUn
zmaQyA(@|JM=ZTTWhxM{d8Fk))FG;a&7sClGn1wDSGAX_4Je4}lwz`kkTy{L`^nP_>
z4fo6?$xC6kx;R5vV|wu>CVa3mItfdgU2E?h1td;m-OU1}V?J}L5SZ(pk4_b3Z!}(p
z78&yn=5P9Y-HjPB>E9UKh!1;x<IQ+MIL!0O_ZR#%kpx0FvBh<Wy8$!hrFDf>(43j&
zZ(5Ujpb^>T{>*LGM?|0kL&34r1NM3t=iS}$(T-Z+Sv5{s3Oz5b(4lu9p7H<?SvqUS
z`FQ`W=&a0-gW)fy(vEGCU*6-L(i^AfzD>1a;gn<lQm@i=$GW<!@+RQTc!$(_W!ltZ
z&*WnXZLr3>^(}(;AgcEt;Ls0=ZRAwsjQ14eOwVufBPJ|Xtu4^nu(czxh@pO8LJjxh
zD>S{VBnV6I_~p{+g6p*AF)Eb8GQBPjPjmQS`{sO5Fa?|JRv!jOvdNcy7mhH6TyM$K
zH+$tqj}>xImQ6Cxs_kOWs-fPdYfG06g2!D41KyXaE3dlwd}G~+qKarf#-Vw5t8oct
zAJ7^&#!O{o=y8wib2Jd?CSVJOBPvHpMKGU_o^pCGN@5c6<%N@TD;A%Ih6OwECSoEc
zqag~3_!12q9QvM<6i;`dp<6FnjKZZD?3^Y~M9X)Xo5y)fQU8j4neB#Z-?rbcnBGGW
zL;1ZUe}Av}S3zSw`^{}x3{pE{Oq<baN5#WXd!Tp~jGG=a?}7Kt7sFeHpPn`c2Va$H
z+p8|VUgm(@=H6*GCXcp)S-4KqLK`&%PlsXGemVom()8St7IsgR(^g{MJjKcdQFN*W
zSYcF|(~gfri$^YH+Bu4TC<xu#9;@~X1}StAU?1#Fs<HgyIG6!4Hy|OeC~R&)u*Rph
zqaP7wF1*Sj*C}{097nj}bu9cno2fC|KgiI}f5*w#=kU^g^UhDjuhSB^;o4k`8Oz6v
ztWCk7trsE%DIXR+;FX8jZ#WX{Z|koV{<iq8jXmeB@uWw|<vah>k1|?igAx>&FEK4g
zJp}PGV-~V?Z0Ap34+YC27lkJlqD+$w{L1S)n0$B{@a4rvzi?-{f}3v8btvlRf)}%{
z982uqy^3_mDj-Qa7>x^7+lIdI#si&wrw9ayFf|L>$n9MziM!EMNsc^^rd330HJqE|
zCL(+y8TTO-Yjtwe>D;OU2!mpd^o{73@!!pov#`)d=t(?4U1=%&VIW(g>-KS@><1xM
z#o6`uQbYl75!i$}7y|`%i}O3ya|o;&L;!Q$<A^2<>g;2oLYF-hHb3uOvzpY?V!tKX
z$&viTjp~hjvt6?f_5L(5T<6T)zgK*=G%B4i{>5VOTcHjCo|Tw3K}c;^5<IN#<VScR
z-2+qi-(6aQO@@qH1@y8W{fsIHn=txb`k%<G;{pDk;+6wa2HX(2RA9%soK_AN{4cv%
z?VJpB+Z;y>8^Of)PGoaJ%-5b{3Ajxz?}q}VbP)Z|7CsV?t(^QMt?b_*wieWBjSgJt
zgSjOVU-fP@nfngkeu-j5pVdD02DN&L7h>cnR1M$u`e&#ayJ!36Nzf3gvFBDkVb*20
zx{=PWQ2lnSlWxt#w9Qb`4|nu*zw&l9jdb=yQP_FgoX1g%7*9>Ym5g2^{GP_hARPDJ
z>S?mxZJ$EjVM0b^<Cn1+Yz}snF4;e6vPFizfLslf7@^FGg<g0Ee$UM?G%Ehcg@X&2
zKy5Yx7)_#g(3iE2vTWqC`#F)g8ve|5zUz&r42V^OZdH+pcrdYR)UcfjLw?u4V^Fpl
zYIENG3~TGcZ{v1YL7Mp^X~oI=PW$#-=*LRaEdQ&$#TZm4J!;hC)uuZC$MpMVFl2+~
zo)lpsUQBO<A;BIr)=LT`FIeP!`bCUBlK%U*brSBT%H1Q(M953iF-d=!43RIxh#m@+
z<i8#f9+2KwHOQ=|=R289OBk<?x1Il*jw`yJn<n^9+;wnfaLJ$JQbZSWPdI;#&}4K+
z5h3klLM&}=f*bAKpAWMlA>A~CbS|A@7eXwJ75%{sZXC%^`YHk22-J;1W8cygJDn>>
z#Zs3Wg2`kQ*ZN_boN#AB-IuSAfyk5^XT2@u_1$CPph-5RhY9oh4|Z_1*kyF*Tn=j!
zAyX=k3tK0TP)5d%{1a!N8~`6z1yMX|%4X~IyR1sw%CqR3pF|W^y;GHJ`r~bq0f+rq
zCq*uuLV8wdcdR>V{#NH{SCxo6okL#|wte4+f86LkKnN%f_FZP0cDJ~BJu0<8gigh9
zwUJ<{gnexHCL!}q(A#a5fi`?eY2F1JO!>>5j7sXak1M9Sq`_iVxHH4aQR4T(m0l?X
zVQGryc7ogSk6!_+L12RIM$BuZ?y}$9W<D(IV~bYU!;4|RmGe8hj;LU~Wd<{gNBEhu
z2VG=qfT$gaAl{xtu+?JR4>7jL!_D>0gsa2rfon=mm@${JqGb&Sot3hgefs@UXyxX&
za$yDI0ugI0^g}ciq7IcoWoyN&;N$m_5@zi6y+mLP57DozABiXM7HEF+_F%`T$%wAx
zwC`aqV?-e9=eXL)<)PGiQW%wXlU+3HhkBLQ^ORK~Yz=7YC^%BxYU;?S0rW%9X^|!I
zxkXV8in@_|hsa3o=FBlpV^A34#kn8s25IBRl|_}__EaPbj%k$wKVX;VccaN|XE2Y(
zAFtvwkH%rIn&Iz7CftUi*kL{J;Lpd`u8QH$$4%WS<Im$VY?O5)?8V-FWX=%%JlkH}
zE$!O=QvhF?mS?|AgEumIfiiPydKSl_nT`nS<wLQtHBzW{Ln9}bOz0H4dB|Oxi&yvP
z>*5kFMn%l}aEYS_YlUJ~8K7ckopHzOQ1I~Gl)b5zzQp*CWIC~e+Sf-;Q5x{+$@MoY
zMbace4uK}EK&__y9=b8FFBcJL-@fgB{fhULhtu_R)K{U_ts+<k2Tq-;NL)tcA(IsL
zwvm#-M-lcmxVEmPZXxmkoQnkbcMdS7KLO@a=H?0#AE-%#j#Ne7U`VB_PLL+oH%h)_
zML)5Q%Md#cU;M;RVnBiS`CKONi)^t&nn;j&uBG~lesWk%DE=5L`dBwgfFu$e4Xcua
ztU--hQ;LjeDdo56c>=u{>W_%Es=xX#O!AuxD&!(IqeEq@+6z?isU*|yRlW8Uf~PK$
z5d!QE<<FL<fi-MmJQdcF+#`9n`X1jH^>TDcrZU7wrk#DP`81vE^K*rW?0a19U>@U>
z=aU(StuGpHNhfuztCPc!xDb{_k#1M|lV90kh6We!-lf*ELnZ6+B&5YFMuM@ITUm+F
zBrRm%oZnRphQKz4iSrDr+o09wc?VjbE>hiahb?~^B*D20d@)Xpj&G~epz#J<kC#My
zd}ESAT(4=4Qi@4|hHq@j+EdN(=R15B*Sk_}l1U~$M!w5$)>BDaIS23F=nhZMFYRA*
zFWHS0+kKVOm`G#Q2$>QtD9*@vGf1#4#>Zxr!4H>KO-J^AS5i;UP5ely8NZ-*2yI$C
z?RU(!A1bmLIosyZKm%ni0uHrlO?=&q(O3ljpmlG|mtVf|;kqEq+|)&ukTb1aLT5~5
z(?_7+P01>j4Go_x==Ji%$cRj_{9Io2i4_eeDjjD|^wMA>T!{o7YCeg+1FiUV+8}tg
zCswGCx)28Bz^Jf?_4^g;oiXj5pgTo@B*O7^u_}eXtLzqpFTltaRSnMeD`UZ+9$P`$
zMnn_VPeKtZWSCp{l5f<q$kSSH<&z)_Cb725W$~`VS`pJz%hr|6ABn49%GgUjARP30
zP9QMr#~?_#B5hgDW%1-xtdt<Y3=?MS!^u2UpR-dE&S|uMg^t=W89B-@I*>Hb9JJx3
zD;4ap_9fd#;TJ~=I&y^G&t}04v&v|v4>!Z@C|xbNz$GnI-V~sVQ2i*gW;(SfyKu~(
zKq7BMAHc%W@_qGM335cjJ|&(*aH@XGB5eF_mhoui?UmMDxyHh>T3syo0LPuHBFC=Q
z%lYTxMy8mM&ldvuI?mE5rq}jFTUc{Kj_uX6G&K)mrAcVl-}Q`x$SR;@Qn8jKxc&!I
zIR{&ebKH&vZ~0ktdw_k>bab2~yXWK@tbCLlJwHa|HOjd-sUa$LYJM~l7LBS7uy}+d
zb>*vNn&fh+E-YiBJQ&^uanh+~?JttJFBpET$U5L^%Al*he|e>PS1zf6<n>XtlBrBK
za%(^K)wiMx^b%jwwD3=*Yzp5?tqWZU=@Y8LMx~B+RWROn<k}U888Y#ejyFF#2<uh?
z>o+Ggr-X|~)Mi~8TJ}~D7M5$M%D8_<+Kvj=+9V^D9jlk>DK|+5wP~@9CGI%4xqKWI
zkL)L~mnjj(wjCkk52w%9-bAXkX)n*vmo|0xO|>gc-_K2Xffq-T^2uMNXP7s%$%NUz
z_4h5a+KU9N06Kq~%!r(%M<?a%l|Wn%2^EnahltadVei}k8Np60GOgo@F>n0Ty+aS7
zB@3D!wsTDV(9&&<wUYNm7n$3*!ne?n!-US{7R3Pg<H~}P&#|}ihEC_1KLq9m-uc1f
z%HPT#eXi^zarT1`sJyQE5tTM^DmNzb@Nk*dnG~1yNDKQp_Or0A8_r@{r@`3#9iqS{
zxc$)kV=m?~dTZWU#mCLitf9{vT9(Z*9lXn2&T!0_;g}v|mYA4l5wPJE*9D&?`oftp
zLNO}%>+UBzB=l};vDQ1y1MEfYmN5+{M1K$ig<$z-0=Hp{FsjI_KNI0bo%ed1+yCs?
z_8X09uWnbISYK~f{F${aG<s2#W99M7vCwRx-%#=A=gH6Jtq5;i^eIWcm--@!r*AD<
zE*kK!o|h@vu+7jf6l$h(JCZE+ep_Q$AAqhRZoMZbP5u0SvbNfTM%~3}tv%OgsZ}1)
zU}d2@)2_eyQ=FML90QJR`VU(cR%k(RyQNNGyR?4SytVVexola_?aj2y=TOvP1JvIF
zd>eW_d0tJv4TVYYGy<uaV+}Q(CfDk22)$io(i!TWkP==7H|Tf$Bw(3_b5ibZs^>43
z(1d~_`P3LS*|Eksoh}XYah^Hg+XseC*VK1P?uDB4;}*kQnknLi?+X(OVG<gMT#6L!
zBShf?V>C9mfKc~|iVN=%OgqHVVe{qTP>>GcNO^Mhb_P6Xtc9pVx2mdvbn|0JJt_AG
zo1PK#>$&>so2`x$ofj~w2>e(;%wNiMGrn=wv@N47#yKx&56-2j!Eml4Ws{6>>qzm{
zq+nB;mT1YgI7Uh8CcRG)v0Y{%G%0pilrR=w1hzH5V#;^J5aa=TC6lPAv3H|#G9vgh
z{6N<tz8tKq|4X+F_g{@MynI05e}Fvy-7TZx<qTn$c5;MDLfp(<ZJeP_u750*O&uWY
z;$qJq7DXE~h^r~o#>r9L)X@#)xtqqy4Zw-=2cfvQlczo_7bgdRl>^8D0C50;06rc*
zLv}f+slAQ4n4^_F1OP-~7jrX*I6?t@KrR&aXIak+Rxk*J!Y*OzEDN!*vW7nILt$5k
zLL9UJyud%%OWW8(z<}rW9yJtU;s2a~_h0=!oIvpZr!(6yUe2)xh$eL@9Gd){x=Kog
z6^qE49uS3Ly$s9Coj_u3A>l&M>~}8L2;UNMEEzYO(Ct~T|I2`<zp}&WLNLwzo8H97
zhXYb>L}7Qf8jI!6#6?NI>25-jF2!pbY&6*(KNr~vRPP8b*z!74m&{ivuh`xh`;K(D
zF>u`K9QAkykcY7g*ODsXXeQZQ6Ws{T^|<-%>6GrZa@%|CI8ewx;H*2rlE&9-CKWne
zgJ;oimos_wXyqUTD-QV8c8^Dp$YipZF{>kqQuGqJ_ySE6we=wNuUx#i<G9YBT~OIL
zvjP>i;=3-pLw5xkow{PvXslSd9$pyP7~GU|v0;#Y#rG_;%I#F*%nD|B#3_H^vpw21
zemmEh=zGq-X)-6GA2cVDBz&OK)T;S-Mp6C{;!$;=f}<VKZCHL&^bFJ>qYubXILPh^
zrw>?-E4-AURC~n3$bW!SQG3LB8bf!B1HyP{&)HFl-+s^TXEf0YkRIjK{?+3-BsyYX
z`iXy_lSAYTwsiLr-3~g~`@cjh-~SSr?CS1j(C3AQt2^WmsJN*c<PXgM6`wY)Zcqtp
zQ`hIXQ#Ac+&iS;^wy}U(yXo_A0RcQ<Fo1`L2f)k00pRB5{__C=0US?jE-vmrpQl&`
zKhc4o=$_Zl^QV0%&vTx?V9$I0i}snv^ZdVfJnws+|DER(4a&3Z|H5<ea{T!`t)F%I
z1NX$s5al0f3E=r73D`B9G#zc8V;jKx&#ZV-<v;e51_Ai~g$Ml&|HK^d$A%}KuU(zY
z)ge%Q_Scfq>>3bHsNw(E_7AVTHnn>Ga(zx=&Oh4h)F5t7?ylw#H^3hv)Yz3E7B;5O
zmEl<cH|WW1d|*R%8CNHF=O-@ePriKel=CwSb1!xY^{0yP#>O0?CL_)+2Y^2LSy-4|
z;z_|L32uPr|6!>8U7f%EF+;-1{rMPwy8Nm5{2~0=<$ulp$1ynmxev&$VFR^?2ue#y
zO9O$NoIoJ=Q<;47D3AyEG(N$=Pa_9N_>YnW)&KKsI=XsK<I{lvK*Rqs1L&Vha{ezi
zdkW2e8VcpVEd}_Ssh+*BU}NE?5BP)XdHL5#|9+l-%8)R9D!EQpf6DsPGbrpT&Jag2
z^XKIFQ+>c6`a8PY+yD6meB!O*4z;&&d{zqlFQfgfvr^(ISDym$Z|33w|79*7;Xi`N
z!rdJ5AH2k0<^=ym_Y~EfPjGJTzn*6t$Di;&%=`ocOFfMoPrUvR^`x`pQzd7V<Oe@f
zaDe&199$e=FbfdO00c5H{Y_0zSBNDF5CGyv0siL$;O64u-~w0z{)B<RTs%+5`vc<$
z_zxY3@1HO*ClBX8U?4CrFYw=Vd|dye19AR~4g}%?g8l{L{`X!m=&5}C6UNE=Z#pgz
z&%a<ipnucx@cc_I_~{k<PZ$UA?>a+WO`l%5uFw8fxABHNnUr14$>}Nb{)#6#M@uIF
zi0iL~BtRb^2;}1A;^gGu0CPx4b8(0Rc|j6l;+$YHE?yo^9$t``Fv|a*<T=D8oy;Yy
zA?9{&?hXKU9x$)8lms6)w-~n=ABPy2S4@&uoR622SBj7Ospw0h{PAixb%p-ndJxBx
N*HGx_q*SC){vT`C=^Ow6

diff --git a/thys/Belief_Revision/document/root.bib b/thys/Belief_Revision/document/root.bib
new file mode 100644
--- /dev/null
+++ b/thys/Belief_Revision/document/root.bib
@@ -0,0 +1,615 @@
+@article{adam2009logical,
+  title={A logical formalization of the OCC theory of emotions},
+  author={Adam, Carole and Herzig, Andreas and Longin, Dominique},
+  journal={Synthese},
+  volume={168},
+  number={2},
+  pages={201--248},
+  year={2009},
+  publisher={Springer}
+}
+
+@inproceedings{dastani2012logic,
+  title={A logic of emotions: from appraisal to coping.},
+  author={Dastani, Mehdi and Lorini, Emiliano},
+  booktitle={AAMAS},
+  pages={1133--1140},
+  year={2012}
+}
+
+@article{walmsley2016cognitive,
+  title={Cognitive biases in visual pilots' weather-related decision making},
+  author={Walmsley, Stephen and Gilbey, Andrew},
+  journal={Applied Cognitive Psychology},
+  volume={30},
+  number={4},
+  pages={532--543},
+  year={2016},
+  publisher={Wiley Online Library}
+}
+
+@incollection{hoffman1998can,
+  title={How can expertise be defined? Implications of research from cognitive psychology},
+  author={Hoffman, Robert R},
+  booktitle={Exploring expertise},
+  pages={81--100},
+  year={1998},
+  publisher={Springer}
+}
+
+@TECHREPORT{BEA,
+  title={BEA f-cp090601},
+  institution={Bureau d’Enquêtes et d’Analyses pour la sécurité de l’aviation civile},
+  year={2012}}
+  
+@inbook{gardenfors1995,
+author = {Gärdenfors, Peter and Rott, Hans},
+year = {1995},
+month = {04},
+pages = {35-132},
+title = {Belief Revision},
+volume = {4},
+_isbn = {0198537913},
+journal = {Handbook of Logic in Artificial Intelligence and Logic Programming}
+}
+  
+  
+@TECHREPORT{Wassermann00analgorithm,
+    author = {Renata Wassermann},
+    title = {An Algorithm for Belief Revision},
+    _institution = {In Proceedings of the Seventh International Conference on Principles of Knowledge Representation and Reasoning (KR2000)},
+    year = {2000}
+}
+  
+@article{REITER198757,
+title = "A theory of diagnosis from first principles",
+journal = "Artificial Intelligence",
+volume = "32",
+number = "1",
+pages = "57 - 95",
+year = "1987",
+_issn = "0004-3702",
+_doi = "https://doi.org/10.1016/0004-3702(87)90062-2",
+_url = "http://www.sciencedirect.com/science/article/pii/0004370287900622",
+author = "Raymond Reiter",
+abstract = "Suppose one is given a description of a system, together with an observation of the system's behaviour which conflicts with the way the system is meant to behave. The diagnostic problem is to determine those components of the system which, when assumed to be functioning abnormally, will explain the discrepancy between the observed and correct system behaviour. We propose a general theory for this problem. The theory requires only that the system be described in a suitable logic. Moreover, there are many such suitable logics, e.g. first-order, temporal, dynamic, etc. As a result, the theory accommodates diagnostic reasoning in a wide variety of practical settings, including digital and analogue circuits, medicine, and database updates. The theory leads to an algorithm for computing all diagnoses, and to various results concerning principles of measurement for discriminating among competing diagnoses. Finally, the theory reveals close connections between diagnostic reasoning and nonmonotonic reasoning."
+}
+
+
+@article{liffiton2008algorithms,
+  title={Algorithms for computing minimal unsatisfiable subsets of constraints},
+  author={Liffiton, Mark H and Sakallah, Karem A},
+  journal={Journal of Automated Reasoning},
+  volume={40},
+  number={1},
+  pages={1--33},
+  year={2008},
+  publisher={Springer}
+}
+
+@article {Tversky1124,
+	author = {Tversky, Amos and Kahneman, Daniel},
+	title = {Judgment under Uncertainty: Heuristics and Biases},
+	volume = {185},
+	number = {4157},
+	pages = {1124--1131},
+	year = {1974},
+	_doi = {10.1126/science.185.4157.1124},
+	publisher = {American Association for the Advancement of Science},
+	abstract = {This article described three heuristics that are employed in making judgements under uncertainty: (i) representativeness, which is usually employed when people are asked to judge the probability that an object or event A belongs to class or process B; (ii) availability of instances or scenarios, which is often employed when people are asked to assess the frequency of a class or the plausibility of a particular development; and (iii) adjustment from an anchor, which is usually employed in numerical prediction when a relevant value is available. These heuristics are highly economical and usually effective, but they lead to systematic and predictable errors. A better understanding of these heuristics and of the biases to which they lead could improve judgements and decisions in situations of uncertainty.},
+	issn = {0036-8075},
+	_URL = {https://science.sciencemag.org/content/185/4157/1124},
+	_eprint = {https://science.sciencemag.org/content/185/4157/1124.full.pdf},
+	journal = {Science}
+}
+
+
+@book{Todd1999,
+author = {Todd, Peter and Czerlinski, Jean and Davis, Jennifer and Gigerenzer, Gerd and Goldstein, Daniel and Goodie, Adam and Hertwig, Ralph and Hoffrage, Ulrich and Laskey, Kathryn and Martignon, Laura and Miller, Geoffrey},
+year = {1999},
+month = {01},
+pages = {},
+title = {Simple Heuristics That Make Us Smart}
+}
+
+
+@ARTICLE{Dimara2020,
+
+  author={E. {Dimara} and S. {Franconeri} and C. {Plaisant} and A. {Bezerianos} and P. {Dragicevic}},
+
+  journal={IEEE Transactions on Visualization and Computer Graphics}, 
+
+  title={A Task-Based Taxonomy of Cognitive Biases for Information Visualization}, 
+
+  year={2020},
+
+  volume={26},
+
+  number={2},
+
+  pages={1413-1432},
+
+  _doi={10.1109/TVCG.2018.2872577}}
+
+
+
+@article{Goldszlagier2015,
+author = {Goldszlagier, Julien},
+year = {2015},
+month = {01},
+pages = {507},
+title = {L'effet d'ancrage ou l'apport de la psychologie cognitive à l'étude de la décision judiciaire},
+volume = {N° 4},
+journal = {Les Cahiers de la Justice},
+_doi = {10.3917/cdlj.1504.0507}
+}
+
+@article{Sullivan2018,
+  title={Cognitive bias in clinical medicine},
+  author={O’Sullivan, ED and Schofield, SJ},
+  journal={JR Coll Physicians Edinb},
+  volume={48},
+  number={3},
+  pages={225--32},
+  year={2018}
+}
+
+@article{mynatt1977confirmation,
+  title={Confirmation bias in a simulated research environment: An experimental study of scientific inference},
+  author={Mynatt, Clifford R and Doherty, Michael E and Tweney, Ryan D},
+  journal={Quarterly Journal of Experimental Psychology},
+  volume={29},
+  number={1},
+  pages={85--95},
+  year={1977},
+  publisher={SAGE Publications Sage UK: London, England}
+}
+
+
+
+@article{nickerson1998confirmation,
+  title={Confirmation bias: A ubiquitous phenomenon in many guises},
+  author={Nickerson, Raymond S},
+  journal={Review of general psychology},
+  volume={2},
+  number={2},
+  pages={175--220},
+  year={1998},
+  publisher={SAGE Publications Sage CA: Los Angeles, CA}
+}
+
+
+@article{murata2015influence,
+  title={Influence of cognitive biases in distorting decision making and leading to critical unfavorable incidents},
+  author={Murata, Atsuo and Nakamura, Tomoko and Karwowski, Waldemar},
+  journal={Safety},
+  volume={1},
+  number={1},
+  pages={44--58},
+  year={2015},
+  publisher={Multidisciplinary Digital Publishing Institute}
+}
+
+
+@article{takano1999psychological,
+  title={Psychological biases affecting human cognitive performance in dynamic operational environments},
+  author={Takano, Kenichi and Reason, James},
+  journal={Journal of Nuclear Science and Technology},
+  volume={36},
+  number={11},
+  pages={1041--1051},
+  year={1999},
+  publisher={Taylor \& Francis}
+}
+
+
+@article{alchourron1985logic,
+  title={On the logic of theory change: Partial meet contraction and revision functions},
+  author={Alchourr{\'o}n, Carlos E and G{\"a}rdenfors, Peter and Makinson, David},
+  journal={The journal of symbolic logic},
+  volume={50},
+  number={2},
+  pages={510--530},
+  year={1985},
+  publisher={Cambridge University Press}
+}
+
+@article{tsoukias2008decision,
+  title={From decision theory to decision aiding methodology},
+  author={Tsouki{\`a}s, Alexis},
+  journal={European Journal of Operational Research},
+  volume={187},
+  number={1},
+  pages={138--161},
+  year={2008},
+  publisher={Elsevier}
+}
+
+@article{davidsson2002agent,
+  title={Agent based social simulation: A computer science view},
+  author={Davidsson, Paul},
+  journal={Journal of artificial societies and social simulation},
+  volume={5},
+  number={1},
+  year={2002}
+}
+
+@article{voinson2015beyond,
+  title={Beyond rational decision-making: modelling the influence of cognitive biases on the dynamics of vaccination coverage},
+  author={Voinson, Marina and Billiard, Sylvain and Alvergne, Alexandra},
+  journal={PloS one},
+  volume={10},
+  number={11},
+  year={2015},
+  publisher={Public Library of Science}
+}
+
+
+@article{kulick2003modeling,
+  title={Modeling Adversaries and Related Cognitive Biases},
+  author={Kulick, Jonathan and Davis, Paul K},
+  journal={Modeling Adversaries and Related Cognitive Biases},
+  year={2003},
+  publisher={RAND Corporation}
+}
+
+
+@inproceedings{arnaud2017role,
+  TITLE = {{The role of cognitive biases in reactions to bushfires}},
+  AUTHOR = {Arnaud, Ma{\"e}l and Adam, Carole and Dugdale, Julie},
+  _URL = {https://halshs.archives-ouvertes.fr/halshs-02116079},
+  BOOKTITLE = {{ISCRAM}},
+  ADDRESS = {Albi, France},
+  YEAR = {2017},
+  MONTH = May,
+  KEYWORDS = {Multi-agent modelling ; social simulation ; cognitive biases ; BDI paradigm ; Victoria bushfires},
+  PDF = {https://halshs.archives-ouvertes.fr/halshs-02116079/file/ISCRAM17_cog_bias-author-version.pdf},
+  HAL_ID = {halshs-02116079},
+  HAL_VERSION = {v1},
+}
+
+@article{CESCHI2019188,
+title = {Dimensions of decision-making: An evidence-based classification of heuristics and biases},
+journal = {Personality and Individual Differences},
+volume = {146},
+pages = {188-200},
+year = {2019},
+issn = {0191-8869},
+_doi = {https://doi.org/10.1016/j.paid.2018.07.033},
+_url = {https://www.sciencedirect.com/science/article/pii/S0191886918304288},
+author = {Andrea Ceschi and Arianna Costantini and Riccardo Sartori and Joshua Weller and Annamaria {Di Fabio}},
+keywords = {Heuristics and Biases, Decision-Making, Individual differences, Mindware gaps, Positive Illusions, Negativity effect, Anchoring and Adjustment},
+abstract = {Traditionally, studies examining decision-making heuristics and biases (H&B) have focused on aggregate effects using between-subjects designs in order to demonstrate violations of rationality. Although H&B are often studied in isolation from others, emerging research has suggested that stable and reliable individual differences in rational thought exist, and similarity in performance across tasks are related, which may suggest an underlying phenotypic structure of decision-making skills. Though numerous theoretical and empirical classifications have been offered, results have been mixed. The current study aimed to clarify this research question. Participants (N = 289) completed a battery of 17 H&B tasks, assessed with a within-subjects design, that we selected based on a review of prior empirical and theoretical taxonomies. Exploratory and confirmatory analyses yielded a solution that suggested that these biases conform to a model composed of three dimensions: Mindware gaps, Valuation biases (i.e., Positive Illusions and Negativity effect), and Anchoring and Adjustment. We discuss these findings in relation to proposed taxonomies and existing studies on individual differences in decision-making.}
+}
+
+
+@article{novaes,
+author = {Novaes, Catarina and Veluwenkamp, Herman},
+year = {2016},
+month = {12},
+pages = {},
+title = {Reasoning Biases, Non-Monotonic Logics and Belief Revision},
+volume = {83},
+journal = {Theoria},
+_doi = {10.1111/theo.12108}
+}
+
+@article{Ferme2011,
+author = {Fermé, Eduardo and Hansson, Sven Ove},
+year = {2011},
+month = {04},
+pages = {295-331},
+title = {AGM 25 Years: Twenty-Five Years of Research in Belief Change},
+volume = {40},
+journal = {Journal of Philosophical Logic},
+_doi = {10.2307/41487515}
+}
+
+@article{macleod1986attentional,
+  title={Attentional bias in emotional disorders.},
+  author={MacLeod, Colin and Mathews, Andrew and Tata, Philip},
+  journal={Journal of abnormal psychology},
+  volume={95},
+  number={1},
+  pages={15},
+  year={1986},
+  publisher={American Psychological Association}
+}
+
+@inbook{staw_1996, place={Cambridge}, series={Cambridge Series on Judgment and Decision Making}, title={The escalation of commitment: An update and appraisal}, _doi={10.1017/CBO9780511584169.011}, booktitle={Organizational Decision Making}, publisher={Cambridge University Press}, author={Staw, Barry M.}, editor={Shapira, ZurEditor}, year={1996}, pages={191–215}, collection={Cambridge Series on Judgment and Decision Making}}
+
+@inproceedings{conversy:hal-01089633,
+  TITLE = {{L'accident du vol AF447 Rio-Paris, un cas d'{\'e}tude pour la recherche en IHM}},
+  AUTHOR = {Conversy, St{\'e}phane and al.},
+  _URL = {https://hal.archives-ouvertes.fr/hal-01089633},
+  BOOKTITLE = {{IHM'14, 26e conf{\'e}rence francophone sur l'Interaction Homme-Machine}},
+  _ADDRESS = {Lille, France},
+  PUBLISHER = {{ACM}},
+  PAGES = {60-69},
+  YEAR = {2014},
+  MONTH = Oct,
+  KEYWORDS = {Models of HCI ; Aviation ; Accident},
+  PDF = {https://hal.archives-ouvertes.fr/hal-01089633v2/file/p60-conversy.pdf},
+  HAL_ID = {hal-01089633},
+  HAL_VERSION = {v2},
+}
+
+@article{postman1965short,
+  title={Short-term temporal changes in free recall},
+  author={Postman, Leo and Phillips, Laura W},
+  journal={Quarterly journal of experimental psychology},
+  volume={17},
+  number={2},
+  pages={132--138},
+  year={1965},
+  publisher={Taylor \& Francis}
+}
+
+@article{moore2008trouble,
+  title={The trouble with overconfidence.},
+  author={Moore, Don A and Healy, Paul J},
+  journal={Psychological review},
+  volume={115},
+  number={2},
+  pages={502},
+  year={2008},
+  publisher={American Psychological Association}
+}
+
+@book{kahneman2011thinking,
+  title={Thinking, fast and slow},
+  author={Kahneman, Daniel},
+  year={2011},
+  publisher={Macmillan}
+}
+
+@article{Stanovich1998,
+author = {Stanovich, Keith and West, Richard},
+year = {1998},
+month = {07},
+pages = {193-230},
+title = {Cognitive Ability and Variation in Selection Task Performance},
+volume = {4},
+journal = {Thinking and Reasoning},
+doi = {10.1080/135467898394139}
+}
+
+@article{Mcelroy2007,
+author = {Mcelroy, Todd and Dowd, Keith},
+year = {2007},
+month = {02},
+pages = {48-53},
+title = {Susceptibility to anchoring effects: How openness-to-experience influences responses to anchoring cues},
+volume = {2},
+journal = {Judgment and Decision Making}
+}
+
+@article{Oreg2009,
+author = {Oreg, Shaul and Bayazit, Mahmut},
+year = {2009},
+month = {09},
+pages = {175-193},
+title = {Prone to Bias: Development of a Bias Taxonomy From an Individual Differences Perspective},
+volume = {13},
+journal = {Review of General Psychology},
+doi = {10.1037/a0015656}
+}
+
+@article{Slugosky1993,
+author = {Ben R. Slugoski and Heather A. Shields and Kim A. Dawson},
+title ={Relation of Conditional Reasoning to Heuristic Processing},
+journal = {Personality and Social Psychology Bulletin},
+volume = {19},
+number = {2},
+pages = {158-166},
+year = {1993},
+doi = {10.1177/0146167293192004},
+
+URL = { 
+        https://doi.org/10.1177/0146167293192004
+    
+},
+eprint = { 
+        https://doi.org/10.1177/0146167293192004
+    
+}
+,
+    abstract = { Wyer and Srull have proposed that a tendency to treat conditional relationships between events as if they were biconditional underlies a number of familiar biases in human social judgment. This hypothesis was tested in a factor-analytic study in which 111 subjects completed seven measures of heuristic use and three measures of conditional reasoning. A principal components analysis of the measures revealed two main factors, corresponding to an availability dimension and a representativeness dimension. There was no evidence for the hypothesis that the disposition to infer "Y is X" given "X is Y" underlies either dimension, although one measure of conditional reasoning, Wason's selection task, was related to both. This result is discussed in terms of Evans's two-stage (heuristic/analytic processing) model of reasoning. }
+}
+
+@article{Weaver2012,
+author = {Weaver, Elise A. and Stewart, Thomas R.},
+title = {Dimensions of Judgment: Factor Analysis of Individual Differences},
+journal = {Journal of Behavioral Decision Making},
+volume = {25},
+number = {4},
+pages = {402-413},
+keywords = {judgment, individual differences, reasoning, problem solving, probability, cognitive ability, performance},
+doi = {https://doi.org/10.1002/bdm.748},
+url = {https://onlinelibrary.wiley.com/doi/abs/10.1002/bdm.748},
+eprint = {https://onlinelibrary.wiley.com/doi/pdf/10.1002/bdm.748},
+abstract = {ABSTRACT In this paper, we explore a pattern of individual differences in performance on judgment tasks. One hundred participants completed a battery of standard judgment tasks, including multiple cue judgment and tasks based on the “heuristics and biases” and problem-solving literature. Participants also completed tests of fluid and crystallized intelligence, forward digit span memory, and multiple cue probability learning. Confirmatory factor analyses indicated a two-factor structure underlying performance on these tasks and tests. The two moderately correlated factors reflected a distinction between tasks requiring accurate judgments based on multiple cues (correspondence tasks) and those requiring coherent judgments (coherence tasks), in which probabilities are compared and combined. Measures of fluid and crystallized intelligence and forward digit span memory were correlated with both factors but were more associated with correspondence than with coherence. Copyright © 2011 John Wiley \& Sons, Ltd.},
+year = {2012}
+}
+
+
+@article{TEOVANOVIC201575,
+title = "Individual differences in cognitive biases: Evidence against one-factor theory of rationality",
+journal = "Intelligence",
+volume = "50",
+pages = "75 - 86",
+year = "2015",
+issn = "0160-2896",
+doi = "https://doi.org/10.1016/j.intell.2015.02.008",
+url = "http://www.sciencedirect.com/science/article/pii/S0160289615000380",
+author = "Predrag Teovanović and Goran Knežević and Lazar Stankov",
+keywords = "Cognitive biases, Rationality, Judgment and decision making, Intelligence, Factor analysis",
+abstract = "In this paper we seek to gain an improved understanding of the structure of cognitive biases and their relationship with measures of intelligence and relevant non-cognitive constructs. We report on the outcomes of a study based on a heterogeneous set of seven cognitive biases — anchoring effect, belief bias, overconfidence bias, hindsight bias, base rate neglect, outcome bias and sunk cost effect. New scales for the assessment of these biases were administered to 243 undergraduate students along with measures of fluid (Gf) and crystallized (Gc) intelligence, a Cognitive Reflection Test (CRT), Openness/Intellect (O/I) scale and Need for Cognition (NFC) scale. The expected experimental results were confirmed — i.e., each normatively irrelevant variable significantly influenced participants' responses. Also, with the exception of hindsight bias, all cognitive biases showed satisfactory reliability estimates (αs>.70). However, correlations among the cognitive bias measures were low (rs<.20). Although exploratory factor analysis produced two factors, their robustness was doubtful. Cognitive bias measures were also relatively independent (rs<.25) from the Gf, Gc, CRT, O/I and NFC and they define separate latent factors. This pattern of results suggests that a major part of the reliable variance of cognitive bias tasks is unique, and implies that a one-factor model of rational behavior is not plausible."
+}
+
+@inproceedings{Arnott2001ATO,
+  title={A Taxonomy of Decision Biases},
+  author={D. Arnott},
+  year={2001}
+}
+
+
+@article{Carter2007,
+author = {Carter, Craig and Kaufmann, Lutz and Michel, Alex},
+year = {2007},
+month = {09},
+pages = {},
+title = {Behavioral Supply Management: A Taxonomy of Judgment and Decision-Making Biases},
+volume = {37},
+journal = {International Journal of Physical Distribution \& Logistics Management},
+doi = {10.1108/09600030710825694}
+}
+
+
+@article{Zhang2002,
+author = {Zhang, Jiajie and Patel, Vimla and Johnson, Todd and Shortliffe, Edward},
+year = {2002},
+month = {02},
+pages = {934-8},
+title = {Toward a cognitive taxonomy of medical errors},
+journal = {Proceedings / AMIA ... Annual Symposium. AMIA Symposium}
+}
+
+
+@book{bratman1987intention,
+  title={Intention, plans, and practical reason},
+  author={Bratman, Michael and others},
+  volume={10},
+  year={1987},
+  publisher={Harvard University Press Cambridge, MA}
+}
+
+@article{Herzig2016,
+author = {Herzig, Andreas and Lorini, Emiliano and Perrussel, Laurent and Xiao, Zhanhao},
+year = {2016},
+month = {10},
+pages = {},
+title = {BDI Logics for BDI Architectures: Old Problems, New Perspectives},
+volume = {31},
+journal = {KI - Künstliche Intelligenz},
+doi = {10.1007/s13218-016-0457-5}
+}
+
+
+@article{cohen1990intention,
+  title={Intention is choice with commitment},
+  author={Cohen, Philip R and Levesque, Hector J},
+  journal={Artificial intelligence},
+  volume={42},
+  number={2-3},
+  pages={213--261},
+  year={1990},
+  publisher={Elsevier}
+}
+
+@inproceedings{Rao1991ModelingRA,
+  title={Modeling Rational Agents within a BDI-Architecture},
+  author={Anand Srinivasa Rao and M. Georgeff},
+  booktitle={KR},
+  year={1991}
+}
+
+@article{Shoham2009LogicalTO,
+  title={Logical Theories of Intention and the Database Perspective},
+  author={Y. Shoham},
+  journal={Journal of Philosophical Logic},
+  year={2009},
+  volume={38},
+  pages={633-647}
+}
+
+@inproceedings{arnaud:hal-01561962,
+  TITLE = {{Les limites du BDI pour rendre compte du comportement humain en situation de crise}},
+  AUTHOR = {Arnaud, Ma{\"e}l and Adam, Carole and Dugdale, Julie},
+  URL = {https://hal.archives-ouvertes.fr/hal-01561962},
+  BOOKTITLE = {{Rencontres des Jeunes Chercheurs en Intelligence Artificielle (RJCIA 2017)}},
+  ADDRESS = {Caen, France},
+  YEAR = {2017},
+  MONTH = Jul,
+  PDF = {https://hal.archives-ouvertes.fr/hal-01561962/file/Arnaud_RJCIA_2017.pdf},
+  HAL_ID = {hal-01561962},
+  HAL_VERSION = {v1},
+}
+  
+  
+@article{MAKINSON1997,
+author = {MAKINSON, DAVID},
+title = {Screened revision},
+journal = {Theoria},
+volume = {63},
+number = {1‐2},
+pages = {14-23},
+doi = {https://doi.org/10.1111/j.1755-2567.1997.tb00737.x},
+url = {https://onlinelibrary.wiley.com/doi/abs/10.1111/j.1755-2567.1997.tb00737.x},
+eprint = {https://onlinelibrary.wiley.com/doi/pdf/10.1111/j.1755-2567.1997.tb00737.x},
+year = {1997}
+}
+
+@article{Feme1999,
+author = {Fermé, Eduardo and Hansson, Sven Ove},
+year = {1999},
+month = {11},
+pages = {331-342},
+title = {Selective Revision.},
+volume = {63},
+journal = {Studia Logica},
+doi = {10.1023/A:1005294718935}
+}
+
+@article{Hansson1997,
+author = { Sven   Hansson },
+title = {Semi-revision},
+journal = {Journal of Applied Non-Classical Logics},
+volume = {7},
+number = {1-2},
+pages = {151-175},
+year  = {1997},
+publisher = {Taylor & Francis},
+doi = {10.1080/11663081.1997.10510904},
+
+URL = { 
+        https://doi.org/10.1080/11663081.1997.10510904
+    
+},
+eprint = { 
+        https://doi.org/10.1080/11663081.1997.10510904
+    
+}
+
+}
+
+@article{Levi1977SubjunctivesDA,
+  title={Subjunctives, dispositions and chances},
+  author={I. Levi},
+  journal={Synthese},
+  year={1977},
+  volume={34},
+  pages={303-335}
+}
+
+@article{Harper1976,
+ ISSN = {02708647},
+ URL = {http://www.jstor.org/stable/192397},
+ author = {William L. Harper},
+ journal = {PSA: Proceedings of the Biennial Meeting of the Philosophy of Science Association},
+ pages = {462--494},
+ publisher = {[University of Chicago Press, Springer, Philosophy of Science Association]},
+ title = {Rational Conceptual Change},
+ volume = {1976},
+ year = {1976}
+}
+
+@book{wojcicki2013theory,
+  title={Theory of logical calculi: basic theory of consequence operations},
+  author={W{\'o}jcicki, Ryszard},
+  volume={199},
+  year={2013},
+  publisher={Springer Science \& Business Media}
+}
+
+
diff --git a/thys/Belief_Revision/document/root.tex b/thys/Belief_Revision/document/root.tex
new file mode 100644
--- /dev/null
+++ b/thys/Belief_Revision/document/root.tex
@@ -0,0 +1,81 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage{isabelle,isabellesym}
+\usepackage{graphicx}
+\graphicspath {{figures/}}
+
+% further packages required for unusual symbols (see also
+% isabellesym.sty), use only when needed
+
+
+\usepackage{latexsym}
+\usepackage{amssymb}
+  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
+  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
+  %\<triangleq>, \<yen>, \<lozenge>
+
+%\usepackage[greek,english]{babel}
+  %option greek for \<euro>
+  %option english (default language) for \<guillemotleft>, \<guillemotright>
+
+%\usepackage[latin1]{inputenc}
+  %for \<onesuperior>, \<onequarter>, \<twosuperior>, \<onehalf>,
+  %\<threesuperior>, \<threequarters>, \<degree>
+
+%\usepackage[only,bigsqcap]{stmaryrd}
+  %for \<Sqinter>
+
+%\usepackage{eufrak}
+  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
+
+%\usepackage{textcomp}
+  %for \<cent>, \<currency>
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+\begin{document}
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+\title{Belief Revision Theory}
+\author{ Valentin Fouillard \and Safouan TAHA \and Frederic Boulanger \and Nicolas Sabouret}
+\maketitle
+
+\newpage
+
+\begin{abstract}
+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” 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.
+
+This  HOL-based  AFP entry is a faithful formalization of the AGM operators (e.g. contraction, revision, remainder ...) axiomatized in the original 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.
+\end{abstract}
+
+\newpage
+
+\tableofcontents
+
+\newpage
+
+\includegraphics{session_graph.pdf}
+
+\newpage
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+\bibliographystyle{abbrv}
+\bibliography{adb-long,root}
+
+\end{document}
+
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff --git a/thys/ROOTS b/thys/ROOTS
--- a/thys/ROOTS
+++ b/thys/ROOTS
@@ -1,629 +1,630 @@
 ADS_Functor
 AI_Planning_Languages_Semantics
 AODV
 AVL-Trees
 AWN
 Abortable_Linearizable_Modules
 Abs_Int_ITP2012
 Abstract-Hoare-Logics
 Abstract-Rewriting
 Abstract_Completeness
 Abstract_Soundness
 Adaptive_State_Counting
 Affine_Arithmetic
 Aggregation_Algebras
 Akra_Bazzi
 Algebraic_Numbers
 Algebraic_VCs
 Allen_Calculus
 Amicable_Numbers
 Amortized_Complexity
 AnselmGod
 Applicative_Lifting
 Approximation_Algorithms
 Architectural_Design_Patterns
 Aristotles_Assertoric_Syllogistic
 Arith_Prog_Rel_Primes
 ArrowImpossibilityGS
 Attack_Trees
 Auto2_HOL
 Auto2_Imperative_HOL
 AutoFocus-Stream
 Automated_Stateful_Protocol_Verification
 Automatic_Refinement
 AxiomaticCategoryTheory
 BDD
 BNF_CC
 BNF_Operations
 BTree
 Banach_Steinhaus
+Belief_Revision
 Bell_Numbers_Spivey
 BenOr_Kozen_Reif
 Berlekamp_Zassenhaus
 Bernoulli
 Bertrands_Postulate
 Bicategory
 BinarySearchTree
 Binding_Syntax_Theory
 Binomial-Heaps
 Binomial-Queues
 BirdKMP
 Blue_Eyes
 Bondy
 Boolean_Expression_Checkers
 Bounded_Deducibility_Security
 Buchi_Complementation
 Budan_Fourier
 Buffons_Needle
 Buildings
 BytecodeLogicJmlTypes
 C2KA_DistributedSystems
 CAVA_Automata
 CAVA_LTL_Modelchecker
 CCS
 CISC-Kernel
 CRDT
 CSP_RefTK
 CYK
 CZH_Elementary_Categories
 CZH_Foundations
 CZH_Universal_Constructions
 CakeML
 CakeML_Codegen
 Call_Arity
 Card_Equiv_Relations
 Card_Multisets
 Card_Number_Partitions
 Card_Partitions
 Cartan_FP
 Case_Labeling
 Catalan_Numbers
 Category
 Category2
 Category3
 Cauchy
 Cayley_Hamilton
 Certification_Monads
 Chandy_Lamport
 Chord_Segments
 Circus
 Clean
 ClockSynchInst
 Closest_Pair_Points
 CofGroups
 Coinductive
 Coinductive_Languages
 Collections
 Combinatorics_Words
 Combinatorics_Words_Graph_Lemma
 Combinatorics_Words_Lyndon
 Comparison_Sort_Lower_Bound
 Compiling-Exceptions-Correctly
 Complete_Non_Orders
 Completeness
 Complex_Bounded_Operators
 Complex_Geometry
 Complx
 ComponentDependencies
 ConcurrentGC
 ConcurrentIMP
 Concurrent_Ref_Alg
 Concurrent_Revisions
 Conditional_Simplification
 Conditional_Transfer_Rule
 Consensus_Refined
 Constructive_Cryptography
 Constructive_Cryptography_CM
 Constructor_Funs
 Containers
 CoreC++
 Core_DOM
 Core_SC_DOM
 Correctness_Algebras
 Count_Complex_Roots
 CryptHOL
 CryptoBasedCompositionalProperties
 Cubic_Quartic_Equations
 DFS_Framework
 DOM_Components
 DPT-SAT-Solver
 DataRefinementIBP
 Datatype_Order_Generator
 Decl_Sem_Fun_PL
 Decreasing-Diagrams
 Decreasing-Diagrams-II
 Deep_Learning
 Delta_System_Lemma
 Density_Compiler
 Dependent_SIFUM_Refinement
 Dependent_SIFUM_Type_Systems
 Depth-First-Search
 Derangements
 Deriving
 Descartes_Sign_Rule
 Design_Theory
 Dict_Construction
 Differential_Dynamic_Logic
 Differential_Game_Logic
 Dijkstra_Shortest_Path
 Diophantine_Eqns_Lin_Hom
 Dirichlet_L
 Dirichlet_Series
 DiscretePricing
 Discrete_Summation
 DiskPaxos
 Dominance_CHK
 DynamicArchitectures
 Dynamic_Tables
 E_Transcendental
 Echelon_Form
 EdmondsKarp_Maxflow
 Efficient-Mergesort
 Elliptic_Curves_Group_Law
 Encodability_Process_Calculi
 Epistemic_Logic
 Ergodic_Theory
 Error_Function
 Euler_MacLaurin
 Euler_Partition
 Example-Submission
 Extended_Finite_State_Machine_Inference
 Extended_Finite_State_Machines
 FFT
 FLP
 FOL-Fitting
 FOL_Axiomatic
 FOL_Harrison
 FOL_Seq_Calc1
 Factored_Transition_System_Bounding
 Falling_Factorial_Sum
 Farkas
 FeatherweightJava
 Featherweight_OCL
 Fermat3_4
 FileRefinement
 FinFun
 Finger-Trees
 Finite-Map-Extras
 Finite_Automata_HF
 Finitely_Generated_Abelian_Groups
 First_Order_Terms
 First_Welfare_Theorem
 Fishburn_Impossibility
 Fisher_Yates
 Flow_Networks
 Floyd_Warshall
 Flyspeck-Tame
 FocusStreamsCaseStudies
 Forcing
 Formal_Puiseux_Series
 Formal_SSA
 Formula_Derivatives
 Fourier
 Free-Boolean-Algebra
 Free-Groups
 Fresh_Identifiers
 FunWithFunctions
 FunWithTilings
 Functional-Automata
 Functional_Ordered_Resolution_Prover
 Furstenberg_Topology
 GPU_Kernel_PL
 Gabow_SCC
 GaleStewart_Games
 Game_Based_Crypto
 Gauss-Jordan-Elim-Fun
 Gauss_Jordan
 Gauss_Sums
 Gaussian_Integers
 GenClock
 General-Triangle
 Generalized_Counting_Sort
 Generic_Deriving
 Generic_Join
 GewirthPGCProof
 Girth_Chromatic
 GoedelGod
 Goedel_HFSet_Semantic
 Goedel_HFSet_Semanticless
 Goedel_Incompleteness
 Goodstein_Lambda
 GraphMarkingIBP
 Graph_Saturation
 Graph_Theory
 Green
 Groebner_Bases
 Groebner_Macaulay
 Gromov_Hyperbolicity
 Grothendieck_Schemes
 Group-Ring-Module
 HOL-CSP
 HOLCF-Prelude
 HRB-Slicing
 Heard_Of
 Hello_World
 HereditarilyFinite
 Hermite
 Hermite_Lindemann
 Hidden_Markov_Models
 Higher_Order_Terms
 Hoare_Time
 Hood_Melville_Queue
 HotelKeyCards
 Huffman
 Hybrid_Logic
 Hybrid_Multi_Lane_Spatial_Logic
 Hybrid_Systems_VCs
 HyperCTL
 IEEE_Floating_Point
 IFC_Tracking
 IMAP-CRDT
 IMO2019
 IMP2
 IMP2_Binary_Heap
 IMP_Compiler
 IP_Addresses
 Imperative_Insertion_Sort
 Impossible_Geometry
 Incompleteness
 Incredible_Proof_Machine
 Inductive_Confidentiality
 Inductive_Inference
 InfPathElimination
 InformationFlowSlicing
 InformationFlowSlicing_Inter
 Integration
 Interpreter_Optimizations
 Interval_Arithmetic_Word32
 Intro_Dest_Elim
 Iptables_Semantics
 Irrational_Series_Erdos_Straus
 Irrationality_J_Hancl
 IsaGeoCoq
 Isabelle_C
 Isabelle_Marries_Dirac
 Isabelle_Meta_Model
 Jacobson_Basic_Algebra
 Jinja
 JinjaDCI
 JinjaThreads
 JiveDataStoreModel
 Jordan_Hoelder
 Jordan_Normal_Form
 KAD
 KAT_and_DRA
 KBPs
 KD_Tree
 Key_Agreement_Strong_Adversaries
 Kleene_Algebra
 Knot_Theory
 Knuth_Bendix_Order
 Knuth_Morris_Pratt
 Koenigsberg_Friendship
 Kruskal
 Kuratowski_Closure_Complement
 LLL_Basis_Reduction
 LLL_Factorization
 LOFT
 LTL
 LTL_Master_Theorem
 LTL_Normal_Form
 LTL_to_DRA
 LTL_to_GBA
 Lam-ml-Normalization
 LambdaAuth
 LambdaMu
 Lambda_Free_EPO
 Lambda_Free_KBOs
 Lambda_Free_RPOs
 Lambert_W
 Landau_Symbols
 Laplace_Transform
 Latin_Square
 LatticeProperties
 Launchbury
 Laws_of_Large_Numbers
 Lazy-Lists-II
 Lazy_Case
 Lehmer
 Lifting_Definition_Option
 Lifting_the_Exponent
 LightweightJava
 LinearQuantifierElim
 Linear_Inequalities
 Linear_Programming
 Linear_Recurrences
 Liouville_Numbers
 List-Index
 List-Infinite
 List_Interleaving
 List_Inversions
 List_Update
 LocalLexing
 Localization_Ring
 Locally-Nameless-Sigma
 Logging_Independent_Anonymity
 Lowe_Ontological_Argument
 Lower_Semicontinuous
 Lp
 Lucas_Theorem
 MFMC_Countable
 MFODL_Monitor_Optimized
 MFOTL_Monitor
 MSO_Regex_Equivalence
 Markov_Models
 Marriage
 Mason_Stothers
 Matrices_for_ODEs
 Matrix
 Matrix_Tensor
 Matroids
 Max-Card-Matching
 Median_Of_Medians_Selection
 Menger
 Mereology
 Mersenne_Primes
 Metalogic_ProofChecker
 MiniML
 MiniSail
 Minimal_SSA
 Minkowskis_Theorem
 Minsky_Machines
 Modal_Logics_for_NTS
 Modular_Assembly_Kit_Security
 Modular_arithmetic_LLL_and_HNF_algorithms
 Monad_Memo_DP
 Monad_Normalisation
 MonoBoolTranAlgebra
 MonoidalCategory
 Monomorphic_Monad
 MuchAdoAboutTwo
 Multi_Party_Computation
 Multirelations
 Myhill-Nerode
 Name_Carrying_Type_Inference
 Nash_Williams
 Nat-Interval-Logic
 Native_Word
 Nested_Multisets_Ordinals
 Network_Security_Policy_Verification
 Neumann_Morgenstern_Utility
 No_FTL_observers
 Nominal2
 Noninterference_CSP
 Noninterference_Concurrent_Composition
 Noninterference_Generic_Unwinding
 Noninterference_Inductive_Unwinding
 Noninterference_Ipurge_Unwinding
 Noninterference_Sequential_Composition
 NormByEval
 Nullstellensatz
 Octonions
 OpSets
 Open_Induction
 Optics
 Optimal_BST
 Orbit_Stabiliser
 Order_Lattice_Props
 Ordered_Resolution_Prover
 Ordinal
 Ordinal_Partitions
 Ordinals_and_Cardinals
 Ordinary_Differential_Equations
 PAC_Checker
 PCF
 PLM
 POPLmark-deBruijn
 PSemigroupsConvolution
 Padic_Ints
 Pairing_Heap
 Paraconsistency
 Parity_Game
 Partial_Function_MR
 Partial_Order_Reduction
 Password_Authentication_Protocol
 Pell
 Perfect-Number-Thm
 Perron_Frobenius
 Physical_Quantities
 Pi_Calculus
 Pi_Transcendental
 Planarity_Certificates
 Poincare_Bendixson
 Poincare_Disc
 Polynomial_Factorization
 Polynomial_Interpolation
 Polynomials
 Pop_Refinement
 Posix-Lexing
 Possibilistic_Noninterference
 Power_Sum_Polynomials
 Pratt_Certificate
 Presburger-Automata
 Prim_Dijkstra_Simple
 Prime_Distribution_Elementary
 Prime_Harmonic_Series
 Prime_Number_Theorem
 Priority_Queue_Braun
 Priority_Search_Trees
 Probabilistic_Noninterference
 Probabilistic_Prime_Tests
 Probabilistic_System_Zoo
 Probabilistic_Timed_Automata
 Probabilistic_While
 Program-Conflict-Analysis
 Progress_Tracking
 Projective_Geometry
 Projective_Measurements
 Promela
 Proof_Strategy_Language
 PropResPI
 Propositional_Proof_Systems
 Prpu_Maxflow
 PseudoHoops
 Psi_Calculi
 Ptolemys_Theorem
 Public_Announcement_Logic
 QHLProver
 QR_Decomposition
 Quantales
 Quaternions
 Quick_Sort_Cost
 RIPEMD-160-SPARK
 ROBDD
 RSAPSS
 Ramsey-Infinite
 Random_BSTs
 Random_Graph_Subgraph_Threshold
 Randomised_BSTs
 Randomised_Social_Choice
 Rank_Nullity_Theorem
 Real_Impl
 Recursion-Addition
 Recursion-Theory-I
 Refine_Imperative_HOL
 Refine_Monadic
 RefinementReactive
 Regex_Equivalence
 Regression_Test_Selection
 Regular-Sets
 Regular_Algebras
 Relation_Algebra
 Relational-Incorrectness-Logic
 Relational_Disjoint_Set_Forests
 Relational_Forests
 Relational_Method
 Relational_Minimum_Spanning_Trees
 Relational_Paths
 Rep_Fin_Groups
 Residuated_Lattices
 Resolution_FOL
 Rewriting_Z
 Ribbon_Proofs
 Robbins-Conjecture
 Robinson_Arithmetic
 Root_Balanced_Tree
 Routing
 Roy_Floyd_Warshall
 SATSolverVerification
 SC_DOM_Components
 SDS_Impossibility
 SIFPL
 SIFUM_Type_Systems
 SPARCv8
 Safe_Distance
 Safe_OCL
 Saturation_Framework
 Saturation_Framework_Extensions
 Schutz_Spacetime
 Secondary_Sylow
 Security_Protocol_Refinement
 Selection_Heap_Sort
 SenSocialChoice
 Separata
 Separation_Algebra
 Separation_Logic_Imperative_HOL
 SequentInvertibility
 Shadow_DOM
 Shadow_SC_DOM
 Shivers-CFA
 ShortestPath
 Show
 Sigma_Commit_Crypto
 Signature_Groebner
 Simpl
 Simple_Firewall
 Simplex
 Skew_Heap
 Skip_Lists
 Slicing
 Sliding_Window_Algorithm
 Smith_Normal_Form
 Smooth_Manifolds
 Sort_Encodings
 Source_Coding_Theorem
 SpecCheck
 Special_Function_Bounds
 Splay_Tree
 Sqrt_Babylonian
 Stable_Matching
 Statecharts
 Stateful_Protocol_Composition_and_Typing
 Stellar_Quorums
 Stern_Brocot
 Stewart_Apollonius
 Stirling_Formula
 Stochastic_Matrices
 Stone_Algebras
 Stone_Kleene_Relation_Algebras
 Stone_Relation_Algebras
 Store_Buffer_Reduction
 Stream-Fusion
 Stream_Fusion_Code
 Strong_Security
 Sturm_Sequences
 Sturm_Tarski
 Stuttering_Equivalence
 Subresultants
 Subset_Boolean_Algebras
 SumSquares
 Sunflowers
 SuperCalc
 Surprise_Paradox
 Symmetric_Polynomials
 Syntax_Independent_Logic
 Szpilrajn
 TESL_Language
 TLA
 Tail_Recursive_Functions
 Tarskis_Geometry
 Taylor_Models
 Three_Circles
 Timed_Automata
 Topological_Semantics
 Topology
 TortoiseHare
 Transcendence_Series_Hancl_Rucki
 Transformer_Semantics
 Transition_Systems_and_Automata
 Transitive-Closure
 Transitive-Closure-II
 Treaps
 Tree-Automata
 Tree_Decomposition
 Triangle
 Trie
 Twelvefold_Way
 Tycon
 Types_Tableaus_and_Goedels_God
 Types_To_Sets_Extension
 UPF
 UPF_Firewall
 UTP
 Universal_Turing_Machine
 UpDown_Scheme
 Valuation
 Van_der_Waerden
 VectorSpace
 VeriComp
 Verified-Prover
 Verified_SAT_Based_AI_Planning
 VerifyThis2018
 VerifyThis2019
 Vickrey_Clarke_Groves
 Virtual_Substitution
 VolpanoSmith
 WHATandWHERE_Security
 WOOT_Strong_Eventual_Consistency
 WebAssembly
 Weighted_Path_Order
 Weight_Balanced_Trees
 Well_Quasi_Orders
 Winding_Number_Eval
 Word_Lib
 WorkerWrapper
 XML
 ZFC_in_HOL
 Zeta_3_Irrational
 Zeta_Function
 pGCL