diff --git a/thys/ADS_Functor/Merkle_Interface.thy b/thys/ADS_Functor/Merkle_Interface.thy --- a/thys/ADS_Functor/Merkle_Interface.thy +++ b/thys/ADS_Functor/Merkle_Interface.thy @@ -1,299 +1,299 @@ (* Author: Andreas Lochbihler, Digital Asset Author: Ognjen Maric, Digital Asset *) theory Merkle_Interface imports Main "HOL-Library.Conditional_Parametricity" "HOL-Library.Monad_Syntax" begin alias vimage2p = BNF_Def.vimage2p alias Grp = BNF_Def.Grp alias setl = Basic_BNFs.setl alias setr = Basic_BNFs.setr alias fsts = Basic_BNFs.fsts alias snds = Basic_BNFs.snds attribute_setup locale_witness = \Scan.succeed Locale.witness_add\ lemma vimage2p_mono': "R \ S \ vimage2p f g R \ vimage2p f g S" by(auto simp add: vimage2p_def le_fun_def) lemma vimage2p_map_rel_prod: "vimage2p (map_prod f g) (map_prod f' g') (rel_prod A B) = rel_prod (vimage2p f f' A) (vimage2p g g' B)" by(simp add: vimage2p_def prod.rel_map) lemma vimage2p_map_list_all2: "vimage2p (map f) (map g) (list_all2 A) = list_all2 (vimage2p f g A)" by(simp add: vimage2p_def list.rel_map) lemma equivclp_least: assumes le: "r \ s" and s: "equivp s" shows "equivclp r \ s" apply(rule predicate2I) subgoal by(induction rule: equivclp_induct)(auto 4 3 intro: equivp_reflp[OF s] equivp_transp[OF s] equivp_symp[OF s] le[THEN predicate2D]) done lemma reflp_eq_onp: "reflp R \ eq_onp (\x. True) \ R" by(auto simp add: reflp_def eq_onp_def) lemma eq_onpE: assumes "eq_onp P x y" obtains "x = y" "P y" using assms by(auto simp add: eq_onp_def) lemma case_unit_parametric [transfer_rule]: "rel_fun A (rel_fun (=) A) case_unit case_unit" by(simp add: rel_fun_def split: unit.split) (************************************************************) section \Authenticated Data Structures\ (************************************************************) (************************************************************) subsection \Interface\ (************************************************************) (************************************************************) subsubsection \ Types \ (************************************************************) type_synonym ('a\<^sub>m, 'a\<^sub>h) hash = "'a\<^sub>m \ 'a\<^sub>h" \ \Type of hash operation\ type_synonym 'a\<^sub>m blinding_of = "'a\<^sub>m \ 'a\<^sub>m \ bool" type_synonym 'a\<^sub>m merge = "'a\<^sub>m \ 'a\<^sub>m \ 'a\<^sub>m option" \ \ merging that can fail for values with different hashes\ (************************************************************) subsubsection \ Properties \ (************************************************************) locale merkle_interface = fixes h :: "('a\<^sub>m, 'a\<^sub>h) hash" and bo :: "'a\<^sub>m blinding_of" and m :: "'a\<^sub>m merge" assumes merge_respects_hashes: "h a = h b \ (\ab. m a b = Some ab)" and idem: "m a a = Some a" and commute: "m a b = m b a" and assoc: "m a b \ m c = m b c \ m a" and bo_def: "bo a b \ m a b = Some b" begin lemma reflp: "reflp bo" unfolding bo_def by(rule reflpI)(simp add: idem) lemma antisymp: "antisymp bo" unfolding bo_def by(rule antisympI)(simp add: commute) lemma transp: "transp bo" apply(rule transpI) subgoal for x y z using assoc[of x y z] by(simp add: commute bo_def) done lemma hash: "bo \ vimage2p h h (=)" unfolding bo_def by(auto simp add: vimage2p_def merge_respects_hashes) lemma join: "m a b = Some ab \ bo a ab \ bo b ab \ (\u. bo a u \ bo b u \ bo ab u)" unfolding bo_def - by (smt Option.bind_cong bind.bind_lunit commute idem merkle_interface.assoc merkle_interface_axioms) + by (smt (verit) Option.bind_cong bind.bind_lunit commute idem merkle_interface.assoc merkle_interface_axioms) text \The equivalence closure of the blinding relation are the equivalence classes of the hash function (the kernel).\ lemma equivclp_blinding_of: "equivclp bo = vimage2p h h (=)" (is "?lhs = ?rhs") proof(rule antisym) show "?lhs \ ?rhs" by(rule equivclp_least[OF hash])(rule equivp_vimage2p[OF identity_equivp]) show "?rhs \ ?lhs" unfolding vimage2p_def proof(rule predicate2I) fix x y assume "h x = h y" then obtain xy where "m x y = Some xy" unfolding merge_respects_hashes .. hence "bo x xy" "bo y xy" unfolding join by blast+ hence "equivclp bo x xy" "equivclp bo xy y" by(blast)+ thus "equivclp bo x y" by(rule equivclp_trans) qed qed end (************************************************************) subsection \ Auxiliary definitions \ (************************************************************) text \ Directly proving that an interface satisfies the specification of a Merkle interface as given above is difficult. Instead, we provide several layers of auxiliary definitions that can easily be proved layer-by-layer. In particular, proving that an interface on recursive datatypes is a Merkle interface requires induction. As the induction hypothesis only applies to a subset of values of a type, we add auxiliary definitions equipped with an explicit set @{term A} of values to which the definition applies. Once the induction proof is complete, we can typically instantiate @{term A} with @{term UNIV}. In particular, in the induction proof for a layer, we can assume that properties for the earlier layers hold for \<^emph>\all\ values, not just those in the induction hypothesis. \ (************************************************************) subsubsection \ Blinding \ (************************************************************) locale blinding_respects_hashes = fixes h :: "('a\<^sub>m, 'a\<^sub>h) hash" and bo :: "'a\<^sub>m blinding_of" assumes hash: "bo \ vimage2p h h (=)" begin lemma blinding_hash_eq: "bo x y \ h x = h y" by(drule hash[THEN predicate2D])(simp add: vimage2p_def) end locale blinding_of_on = blinding_respects_hashes h bo for A :: "'a\<^sub>m set" and h :: "('a\<^sub>m, 'a\<^sub>h) hash" and bo :: "'a\<^sub>m blinding_of" + assumes refl: "x \ A \ bo x x" and trans: "\ bo x y; bo y z; x \ A \ \ bo x z" and antisym: "\ bo x y; bo y x; x \ A \ \ x = y" begin lemma refl_pointfree: "eq_onp (\x. x \ A) \ bo" by(auto elim!: eq_onpE intro: refl) lemma blinding_respects_hashes: "blinding_respects_hashes h bo" .. lemmas hash = hash lemma trans_pointfree: "eq_onp (\x. x \ A) OO bo OO bo \ bo" by(auto elim!: eq_onpE intro: trans) lemma antisym_pointfree: "inf (eq_onp (\x. x \ A) OO bo) bo\\ \ (=)" by(auto elim!: eq_onpE dest: antisym) end (************************************************************) subsubsection \ Merging \ (************************************************************) text \ In general, we prove the properties of blinding before the properties of merging. Thus, in the following definitions we assume that the blinding properties already hold on @{term UNIV}. The @{term Ball} restricts the argument of the merge operation on which induction will be done. \ locale merge_on = blinding_of_on UNIV h bo for A :: "'a\<^sub>m set" and h :: "('a\<^sub>m, 'a\<^sub>h) hash" and bo :: "'a\<^sub>m blinding_of" and m :: "'a\<^sub>m merge" + assumes join: "\ h a = h b; a \ A \ \ \ab. m a b = Some ab \ bo a ab \ bo b ab \ (\u. bo a u \ bo b u \ bo ab u)" and undefined: "\ h a \ h b; a \ A \ \ m a b = None" begin lemma same: "a \ A \ m a a = Some a" using join[of a a] refl[of a] by(auto 4 3 intro: antisym) lemma blinding_of_antisym_on: "blinding_of_on UNIV h bo" .. lemma transp: "transp bo" by(auto intro: transpI trans) lemmas hash = hash and refl = refl and antisym = antisym[OF _ _ UNIV_I] lemma respects_hashes: "a \ A \ h a = h b \ (\ab. m a b = Some ab)" using join undefined by fastforce lemma join': "a \ A \ \ab. m a b = Some ab \ bo a ab \ bo b ab \ (\u. bo a u \ bo b u \ bo ab u)" using join undefined by (metis (full_types) hash local.antisym option.distinct(1) option.sel predicate2D vimage2p_def) lemma merge_on_subset: "B \ A \ merge_on B h bo m" by unfold_locales (auto dest: same join undefined) end subsection \ Interface equality \ text \ Here, we prove that the auxiliary definitions specify the same interface as the original ones.\ lemma merkle_interface_aux: "merkle_interface h bo m = merge_on UNIV h bo m" (is "?lhs = ?rhs") proof show ?rhs if ?lhs proof interpret merkle_interface h bo m by(fact that) show "bo \ vimage2p h h (=)" by(fact hash) show "bo x x" for x using reflp by(simp add: reflp_def) show "bo x z" if "bo x y" "bo y z" for x y z using transp that by(rule transpD) show "x = y" if "bo x y" "bo y x" for x y using antisymp that by(rule antisympD) show "\ab. m a b = Some ab \ bo a ab \ bo b ab \ (\u. bo a u \ bo b u \ bo ab u)" if "h a = h b" for a b using that by(simp add: merge_respects_hashes join) show "m a b = None" if "h a \ h b" for a b using that by(simp add: merge_respects_hashes) qed show ?lhs if ?rhs proof interpret merge_on UNIV h bo m by(fact that) show eq: "h a = h b \ (\ab. m a b = Some ab)" for a b by(simp add: respects_hashes) show idem: "m a a = Some a" for a by(simp add: same) show commute: "m a b = m b a" for a b using join[of a b] join[of b a] undefined antisym by(cases "m a b") force+ have undefined_partitioned: "m a c = None" if "m a b = None" "m b c = Some bc" for a b c bc using that eq by (metis option.distinct(1) option.exhaust) have merge_twice: "m a b = Some c \ m a c = Some c" for a b c by (simp add: join') show "m a b \ m c = m b c \ m a" for a b c proof(simp split: Option.bind_split; safe) show "None = m a d" if "m a b = None" "m b c = Some d" for d using that by(metis undefined_partitioned merge_twice) show "m c d = None" if "m a b = Some d" "m b c = None" for d using that by(metis commute merge_twice undefined_partitioned) next fix ab bc assume assms: "m a b = Some ab" "m b c = Some bc" then obtain cab and abc where cab: "m c ab = Some cab" and abc: "m a bc = Some abc" using eq[THEN iffD2, OF exI] eq[THEN iffD1] by (metis merge_twice) thus "m c ab = m a bc" using assms by(clarsimp simp add: join')(metis UNIV_I abc cab local.antisym local.trans) qed show "bo a b \ m a b = Some b" for a b using idem join' by auto qed qed lemma merkle_interfaceI [locale_witness]: assumes "merge_on UNIV h bo m" shows "merkle_interface h bo m" using assms unfolding merkle_interface_aux by auto lemma (in merkle_interface) merkle_interfaceD: "merge_on UNIV h bo m" using merkle_interface_aux[of h bo m, symmetric] by simp unfold_locales subsection \ Parametricity rules \ context includes lifting_syntax begin parametric_constant le_fun_parametric[transfer_rule]: le_fun_def parametric_constant vimage2p_parametric[transfer_rule]: vimage2p_def parametric_constant blinding_respects_hashes_parametric_aux: blinding_respects_hashes_def lemma blinding_respects_hashes_parametric [transfer_rule]: "((A1 ===> A2) ===> (A1 ===> A1 ===> (\)) ===> (\)) blinding_respects_hashes blinding_respects_hashes" if [transfer_rule]: "bi_unique A2" "bi_total A1" by(rule blinding_respects_hashes_parametric_aux that le_fun_parametric | simp add: rel_fun_eq)+ parametric_constant blinding_of_on_axioms_parametric [transfer_rule]: blinding_of_on_axioms_def[folded Ball_def, unfolded le_fun_def le_bool_def eq_onp_def relcompp.simps, simplified] parametric_constant blinding_of_on_parametric [transfer_rule]: blinding_of_on_def parametric_constant antisymp_parametric[transfer_rule]: antisymp_def parametric_constant transp_parametric[transfer_rule]: transp_def parametric_constant merge_on_axioms_parametric [transfer_rule]: merge_on_axioms_def parametric_constant merge_on_parametric[transfer_rule]: merge_on_def parametric_constant merkle_interface_parametric[transfer_rule]: merkle_interface_def end end \ No newline at end of file diff --git a/thys/AxiomaticCategoryTheory/AxiomaticCategoryTheory.thy b/thys/AxiomaticCategoryTheory/AxiomaticCategoryTheory.thy --- a/thys/AxiomaticCategoryTheory/AxiomaticCategoryTheory.thy +++ b/thys/AxiomaticCategoryTheory/AxiomaticCategoryTheory.thy @@ -1,679 +1,679 @@ (*<*) theory AxiomaticCategoryTheory imports Main abbrevs f_neg="\<^bold>\" and f_or="\<^bold>\" and f_and="\<^bold>\" and f_impl="\<^bold>\" and f_imp="\<^bold>\" and mequ="\<^bold>\" and f_all="\<^bold>\" and f_exi="\<^bold>\" and f_all2="(\<^bold>\x.)" and f_exi2="(\<^bold>\x.)" and f_kleeneeq="\" and f_primeq="\" and f_comp2="(\)" and f_comp="\" begin (*Begin: some useful parameter settings*) nitpick_params[user_axioms, show_all, format = 2, expect = genuine] (*End: some useful parameter settings*) (*>*) section\Introduction\ text\This document provides a concise overview on the core results of our previous work \cite{C67,R58,C57} on the exploration of axiom systems for category theory. Extending the previous studies we include one further axiomatic theory in our experiments. This additional theory has been suggested by Mac Lane~\cite{MacLane48} in 1948. We show that the axioms proposed by Mac Lane are equivalent to the ones studied in~\cite{R58}, which includes an axioms set suggested by Scott~\cite{Scott79} in the 1970s and another axioms set proposed by Freyd and Scedrov~\cite{FreydScedrov90} in 1990, which we slightly modified in~\cite{R58} to remedy a minor technical issue. The explanations given below are minimal, for more details we refer to the referenced papers, in particular, to~\cite{R58}.\ section\Embedding of Free Logic in HOL\ text\We introduce a shallow semantical embedding of free logic \cite{R58} in Isabelle/HOL. Definite description is omitted, since it is not needed in the studies below and also since the definition provided in \cite{C57} introduces the here undesired commitment that at least one non-existing element of type $i$ is a priori given. We here want to consider this an optional condition.\ typedecl i \ \Type for individuals\ consts fExistence:: "i\bool" ("E") \ \Existence/definedness predicate in free logic\ abbreviation fNot ("\<^bold>\") where "\<^bold>\\ \ \\" abbreviation fImpl (infixr "\<^bold>\" 13) where "\ \<^bold>\ \ \ \ \ \" abbreviation fId (infixr "\<^bold>=" 25) where "l \<^bold>= r \ l = r" abbreviation fAll ("\<^bold>\") where "\<^bold>\\ \ \x. E x \ \ x" abbreviation fAllBi (binder "\<^bold>\" [8]9) where "\<^bold>\x. \ x \ \<^bold>\\" abbreviation fOr (infixr "\<^bold>\" 21) where "\ \<^bold>\ \ \ (\<^bold>\\) \<^bold>\ \" abbreviation fAnd (infixr "\<^bold>\" 22) where "\ \<^bold>\ \ \ \<^bold>\(\<^bold>\\ \<^bold>\ \<^bold>\\)" abbreviation fImpli (infixr "\<^bold>\" 13) where "\ \<^bold>\ \ \ \ \<^bold>\ \" abbreviation fEquiv (infixr "\<^bold>\" 15) where "\ \<^bold>\ \ \ (\ \<^bold>\ \) \<^bold>\ (\ \<^bold>\ \)" abbreviation fEx ("\<^bold>\") where "\<^bold>\\ \ \<^bold>\(\<^bold>\(\y. \<^bold>\(\ y)))" abbreviation fExiBi (binder "\<^bold>\" [8]9) where "\<^bold>\x. \ x \ \<^bold>\\" section\Some Basic Notions in Category Theory\ text \Morphisms in the category are modeled as objects of type $i$. We introduce three partial functions, $dom$ (domain), $cod$ (codomain), and morphism composition ($\cdot$). For composition we assume set-theoretical composition here (i.e., functional composition from right to left). \label{IDMcL}\ consts domain:: "i\i" ("dom _" [108] 109) codomain:: "i\i" ("cod _" [110] 111) composition:: "i\i\i" (infix "\" 110) \ \Kleene Equality\ abbreviation KlEq (infixr "\" 56) where "x \ y \ (E x \<^bold>\ E y) \<^bold>\ x \<^bold>= y" \ \Existing Identity\ abbreviation ExId (infixr "\" 56) where "x \ y \ (E x \<^bold>\ E y \<^bold>\ x \<^bold>= y)" \ \Identity-morphism: see also p.~4. of \cite{FreydScedrov90}.\ abbreviation "ID i \ (\<^bold>\x. E(i\x) \<^bold>\ i\x \ x) \<^bold>\ (\<^bold>\x. E(x\i) \<^bold>\ x\i \ x)" \ \Identity-morphism: Mac Lane's definition, the same as ID except for notion of equality.\ abbreviation "IDMcL \ \ (\<^bold>\\. E(\\\) \<^bold>\ \\\ = \) \<^bold>\ (\<^bold>\\. E(\\\) \<^bold>\ \\\ = \)" \ \The two notions of identity-morphisms are obviously equivalent.\ lemma IDPredicates: "ID \ IDMcL" by auto section\The Axioms Sets studied by Benzm\"uller and Scott \cite{R58}\ subsection\AxiomsSet1\ text\AxiomsSet1 generalizes the notion of a monoid by introducing a partial, strict binary composition operation ``$\cdot$''. The existence of left and right identity elements is addressed in axioms @{term "C\<^sub>i"} and @{term "D\<^sub>i"}. The notions of $dom$ (domain) and $cod$ (codomain) abstract from their common meaning in the context of sets. In category theory we work with just a single type of objects (the type $i$ in our setting) and therefore identity morphisms are employed to suitably characterize their meanings.\ locale AxiomsSet1 = assumes S\<^sub>i: "E(x\y) \<^bold>\ (E x \<^bold>\ E y)" and E\<^sub>i: "E(x\y) \<^bold>\ (E x \<^bold>\ E y \<^bold>\ (\<^bold>\z. z\z \ z \<^bold>\ x\z \ x \<^bold>\ z\y \ y))" and A\<^sub>i: "x\(y\z) \ (x\y)\z" and C\<^sub>i: "\<^bold>\y.\<^bold>\i. ID i \<^bold>\ i\y \ y" and D\<^sub>i: "\<^bold>\x.\<^bold>\j. ID j \<^bold>\ x\j \ x" begin lemma True nitpick [satisfy] oops \ \Consistency\ lemma assumes "\x. \<^bold>\(E x)" shows True nitpick [satisfy] oops \ \Consistency\ lemma assumes "(\x. \<^bold>\(E x)) \ (\x. (E x))" shows True nitpick [satisfy] oops \ \Consistency\ lemma E\<^sub>iImpl: "E(x\y) \<^bold>\ (E x \<^bold>\ E y \<^bold>\ (\<^bold>\z. z\z \ z \<^bold>\ x\z \ x \<^bold>\ z\y \ y))" by (metis A\<^sub>i C\<^sub>i S\<^sub>i) \ \Uniqueness of i and j in the latter two axioms.\ lemma UC\<^sub>i: "\<^bold>\y.\<^bold>\i. ID i \<^bold>\ i\y \ y \<^bold>\ (\<^bold>\j.(ID j \<^bold>\ j\y \ y) \<^bold>\ i \ j)" by (smt (verit) A\<^sub>i C\<^sub>i S\<^sub>i) lemma UD\<^sub>i: "\<^bold>\x.\<^bold>\j. ID j \<^bold>\ x\j \ x \<^bold>\ (\<^bold>\i.(ID i \<^bold>\ x\i \ x) \<^bold>\ j \ i)" by (smt (verit) A\<^sub>i D\<^sub>i S\<^sub>i) \ \But i and j need not to equal.\ lemma "(\C D. (\<^bold>\y. ID (C y) \<^bold>\ (C y)\y \ y) \<^bold>\ (\<^bold>\x. ID (D x) \<^bold>\ x\(D x) \ x) \<^bold>\ \<^bold>\(D \<^bold>= C))" nitpick [satisfy] oops \ \Model found\ lemma "(\x. E x) \<^bold>\ (\C D. (\<^bold>\y. ID(C y) \<^bold>\ (C y)\y \ y) \<^bold>\ (\<^bold>\x. ID(D x) \<^bold>\ x\(D x) \ x) \<^bold>\ \<^bold>\(D \<^bold>= C))" nitpick [satisfy] oops \ \Model found\ end subsection\AxiomsSet2\ text\AxiomsSet2 is developed from AxiomsSet1 by Skolemization of the existentially quantified variables $i$ and $j$ in axioms $C_i$ and $D_i$. We can argue semantically that every model of AxiomsSet1 has such functions. Hence, we get a conservative extension of AxiomsSet1. The strictness axiom $S$ is extended, so that strictness is now also postulated for the new Skolem functions $dom$ and $cod$.\ locale AxiomsSet2 = assumes S\<^sub>i\<^sub>i: "(E(x\y) \<^bold>\ (E x \<^bold>\ E y)) \<^bold>\ (E(dom x) \<^bold>\ E x) \<^bold>\ (E(cod y) \<^bold>\ E y)" and E\<^sub>i\<^sub>i: "E(x\y) \<^bold>\ (E x \<^bold>\ E y \<^bold>\ (\<^bold>\z. z\z \ z \<^bold>\ x\z \ x \<^bold>\ z\y \ y))" and A\<^sub>i\<^sub>i: "x\(y\z) \ (x\y)\z" and C\<^sub>i\<^sub>i: "E y \<^bold>\ (ID(cod y) \<^bold>\ (cod y)\y \ y)" and D\<^sub>i\<^sub>i: "E x \<^bold>\ (ID(dom x) \<^bold>\ x\(dom x) \ x)" begin lemma True nitpick [satisfy] oops \ \Consistency\ lemma assumes "\x. \<^bold>\(E x)" shows True nitpick [satisfy] oops \ \Consistency\ lemma assumes "(\x. \<^bold>\(E x)) \ (\x. (E x))" shows True nitpick [satisfy] oops \ \Consistency\ lemma E\<^sub>i\<^sub>iImpl: "E(x\y) \<^bold>\ (E x \<^bold>\ E y \<^bold>\ (\<^bold>\z. z\z \ z \<^bold>\ x\z \ x \<^bold>\ z\y \ y))" by (metis A\<^sub>i\<^sub>i C\<^sub>i\<^sub>i S\<^sub>i\<^sub>i) lemma domTotal: "E x \<^bold>\ E(dom x)" by (metis D\<^sub>i\<^sub>i S\<^sub>i\<^sub>i) lemma codTotal: "E x \<^bold>\ E(cod x)" by (metis C\<^sub>i\<^sub>i S\<^sub>i\<^sub>i) end subsubsection\AxiomsSet2 entails AxiomsSet1\ context AxiomsSet2 begin lemma S\<^sub>i: "E(x\y) \<^bold>\ (E x \<^bold>\ E y)" using S\<^sub>i\<^sub>i by blast lemma E\<^sub>i: "E(x\y) \<^bold>\ (E x \<^bold>\ E y \<^bold>\ (\<^bold>\z. z\z \ z \<^bold>\ x\z \ x \<^bold>\ z\y \ y))" using E\<^sub>i\<^sub>i by blast lemma A\<^sub>i: "x\(y\z) \ (x\y)\z" using A\<^sub>i\<^sub>i by blast lemma C\<^sub>i: "\<^bold>\y.\<^bold>\i. ID i \<^bold>\ i\y \ y" by (metis C\<^sub>i\<^sub>i S\<^sub>i\<^sub>i) lemma D\<^sub>i: "\<^bold>\x.\<^bold>\j. ID j \<^bold>\ x\j \ x" by (metis D\<^sub>i\<^sub>i S\<^sub>i\<^sub>i) end subsubsection\AxiomsSet1 entails AxiomsSet2 (by semantic means)\ text\By semantic means (Skolemization).\ subsection\AxiomsSet3\ text\In AxiomsSet3 the existence axiom $E_{ii}$ from AxiomsSet2 is simplified by taking advantage of the two new Skolem functions $dom$ and $cod$. The left-to-right direction of existence axiom $E_{iii}$ is implied.\ locale AxiomsSet3 = assumes S\<^sub>i\<^sub>i\<^sub>i: "(E(x\y) \<^bold>\ (E x \<^bold>\ E y)) \<^bold>\ (E(dom x ) \<^bold>\ E x) \<^bold>\ (E(cod y) \<^bold>\ E y)" and E\<^sub>i\<^sub>i\<^sub>i: "E(x\y) \<^bold>\ (dom x \ cod y \<^bold>\ E(cod y))" and A\<^sub>i\<^sub>i\<^sub>i: "x\(y\z) \ (x\y)\z" and C\<^sub>i\<^sub>i\<^sub>i: "E y \<^bold>\ (ID(cod y) \<^bold>\ (cod y)\y \ y)" and D\<^sub>i\<^sub>i\<^sub>i: "E x \<^bold>\ (ID(dom x) \<^bold>\ x\(dom x) \ x)" begin lemma True nitpick [satisfy] oops \ \Consistency\ lemma assumes "\x. \<^bold>\(E x)" shows True nitpick [satisfy] oops \ \Consistency\ lemma assumes "(\x. \<^bold>\(E x)) \ (\x. (E x))" shows True nitpick [satisfy] oops \ \Consistency\ lemma E\<^sub>i\<^sub>i\<^sub>iImpl: "E(x\y) \<^bold>\ (dom x \ cod y \<^bold>\ E(cod y))" by (metis (full_types) A\<^sub>i\<^sub>i\<^sub>i C\<^sub>i\<^sub>i\<^sub>i D\<^sub>i\<^sub>i\<^sub>i S\<^sub>i\<^sub>i\<^sub>i) end subsubsection\AxiomsSet3 entails AxiomsSet2\ context AxiomsSet3 begin lemma S\<^sub>i\<^sub>i: "(E(x\y) \<^bold>\ (E x \<^bold>\ E y)) \<^bold>\ (E(dom x ) \<^bold>\ E x) \<^bold>\ (E(cod y) \<^bold>\ E y)" using S\<^sub>i\<^sub>i\<^sub>i by blast lemma E\<^sub>i\<^sub>i: "E(x\y) \<^bold>\ (E x \<^bold>\ E y \<^bold>\ (\<^bold>\z. z\z \ z \<^bold>\ x\z \ x \<^bold>\ z\y \ y))" by (metis A\<^sub>i\<^sub>i\<^sub>i C\<^sub>i\<^sub>i\<^sub>i D\<^sub>i\<^sub>i\<^sub>i E\<^sub>i\<^sub>i\<^sub>i S\<^sub>i\<^sub>i\<^sub>i) lemma A\<^sub>i\<^sub>i: "x\(y\z) \ (x\y)\z" using A\<^sub>i\<^sub>i\<^sub>i by blast lemma C\<^sub>i\<^sub>i: "E y \<^bold>\ (ID(cod y) \<^bold>\ (cod y)\y \ y)" using C\<^sub>i\<^sub>i\<^sub>i by auto lemma D\<^sub>i\<^sub>i: "E x \<^bold>\ (ID(dom x) \<^bold>\ x\(dom x) \ x)" using D\<^sub>i\<^sub>i\<^sub>i by auto end subsubsection\AxiomsSet2 entails AxiomsSet3\ context AxiomsSet2 begin lemma S\<^sub>i\<^sub>i\<^sub>i: "(E(x\y) \<^bold>\ (E x \<^bold>\ E y)) \<^bold>\ (E(dom x) \<^bold>\ E x) \<^bold>\ (E(cod y) \<^bold>\ E y)" using S\<^sub>i\<^sub>i by blast lemma E\<^sub>i\<^sub>i\<^sub>i: "E(x\y) \<^bold>\ (dom x \ cod y \<^bold>\ E(cod y))" by (metis C\<^sub>i\<^sub>i D\<^sub>i\<^sub>i E\<^sub>i\<^sub>i S\<^sub>i\<^sub>i) lemma A\<^sub>i\<^sub>i\<^sub>i: "x\(y\z) \ (x\y)\z" using A\<^sub>i\<^sub>i by blast lemma C\<^sub>i\<^sub>i\<^sub>i: "E y \<^bold>\ (ID(cod y) \<^bold>\ (cod y)\y \ y)" using C\<^sub>i\<^sub>i by auto lemma D\<^sub>i\<^sub>i\<^sub>i: "E x \<^bold>\ (ID(dom x) \<^bold>\ x\(dom x) \ x)" using D\<^sub>i\<^sub>i by auto end subsection\The Axioms Set AxiomsSet4\ text\AxiomsSet4 simplifies the axioms $C_{iii}$ and $D_{iii}$. However, as it turned out, these simplifications also require the existence axiom $E_{iii}$ to be strengthened into an equivalence.\ locale AxiomsSet4 = assumes S\<^sub>i\<^sub>v: "(E(x\y) \<^bold>\ (E x \<^bold>\ E y)) \<^bold>\ (E(dom x) \<^bold>\ E x) \<^bold>\ (E(cod y) \<^bold>\ E y)" and E\<^sub>i\<^sub>v: "E(x\y) \<^bold>\ (dom x \ cod y \<^bold>\ E(cod y))" and A\<^sub>i\<^sub>v: "x\(y\z) \ (x\y)\z" and C\<^sub>i\<^sub>v: "(cod y)\y \ y" and D\<^sub>i\<^sub>v: "x\(dom x) \ x" begin lemma True nitpick [satisfy] oops \ \Consistency\ lemma assumes "\x. \<^bold>\(E x)" shows True nitpick [satisfy] oops \ \Consistency\ lemma assumes "(\x. \<^bold>\(E x)) \ (\x. (E x))" shows True nitpick [satisfy] oops \ \Consistency\ end subsubsection\AxiomsSet4 entails AxiomsSet3\ context AxiomsSet4 begin lemma S\<^sub>i\<^sub>i\<^sub>i: "(E(x\y) \<^bold>\ (E x \<^bold>\ E y)) \<^bold>\ (E(dom x) \<^bold>\ E x) \<^bold>\ (E(cod y) \<^bold>\ E y)" using S\<^sub>i\<^sub>v by blast lemma E\<^sub>i\<^sub>i\<^sub>i: "E(x\y) \<^bold>\ (dom x \ cod y \<^bold>\ (E(cod y)))" using E\<^sub>i\<^sub>v by blast lemma A\<^sub>i\<^sub>i\<^sub>i: "x\(y\z) \ (x\y)\z" using A\<^sub>i\<^sub>v by blast lemma C\<^sub>i\<^sub>i\<^sub>i: "E y \<^bold>\ (ID(cod y) \<^bold>\ (cod y)\y \ y)" by (metis C\<^sub>i\<^sub>v D\<^sub>i\<^sub>v E\<^sub>i\<^sub>v) lemma D\<^sub>i\<^sub>i\<^sub>i: "E x \<^bold>\ (ID(dom x) \<^bold>\ x\(dom x) \ x)" by (metis C\<^sub>i\<^sub>v D\<^sub>i\<^sub>v E\<^sub>i\<^sub>v) end subsubsection\AxiomsSet3 entails AxiomsSet4\ context AxiomsSet3 begin lemma S\<^sub>i\<^sub>v: "(E(x\y) \<^bold>\ (E x \<^bold>\ E y)) \<^bold>\ (E(dom x ) \<^bold>\ E x) \<^bold>\ (E(cod y) \<^bold>\ E y)" using S\<^sub>i\<^sub>i\<^sub>i by blast lemma E\<^sub>i\<^sub>v: "E(x\y) \<^bold>\ (dom x \ cod y \<^bold>\ E(cod y))" by (metis (full_types) A\<^sub>i\<^sub>i\<^sub>i C\<^sub>i\<^sub>i\<^sub>i D\<^sub>i\<^sub>i\<^sub>i E\<^sub>i\<^sub>i\<^sub>i S\<^sub>i\<^sub>i\<^sub>i) lemma A\<^sub>i\<^sub>v: "x\(y\z) \ (x\y)\z" using A\<^sub>i\<^sub>i\<^sub>i by blast lemma C\<^sub>i\<^sub>v: "(cod y)\y \ y" using C\<^sub>i\<^sub>i\<^sub>i S\<^sub>i\<^sub>i\<^sub>i by blast lemma D\<^sub>i\<^sub>v: "x\(dom x) \ x" using D\<^sub>i\<^sub>i\<^sub>i S\<^sub>i\<^sub>i\<^sub>i by blast end subsection\AxiomsSet5\ text\AxiomsSet5 has been proposed by Scott \cite{Scott79} in the 1970s. This set of axioms is equivalent to the axioms set presented by Freyd and Scedrov in their textbook ``Categories, Allegories'' \cite{FreydScedrov90} when encoded in free logic, corrected/adapted and further simplified, see Section 5.\ locale AxiomsSet5 = assumes S1: "E(dom x) \<^bold>\ E x" and S2: "E(cod y) \<^bold>\ E y" and S3: "E(x\y) \<^bold>\ dom x \ cod y" and S4: "x\(y\z) \ (x\y)\z" and S5: "(cod y)\y \ y" and S6: "x\(dom x) \ x" begin lemma True nitpick [satisfy] oops \ \Consistency\ lemma assumes "\x. \<^bold>\(E x)" shows True nitpick [satisfy] oops \ \Consistency\ lemma assumes "(\x. \<^bold>\(E x)) \ (\x. (E x))" shows True nitpick [satisfy] oops \ \Consistency\ end subsubsection\AxiomsSet5 entails AxiomsSet4\ context AxiomsSet5 begin lemma S\<^sub>i\<^sub>v: "(E(x\y) \<^bold>\ (E x \<^bold>\ E y)) \<^bold>\ (E(dom x ) \<^bold>\ E x) \<^bold>\ (E(cod y) \<^bold>\ E y)" using S1 S2 S3 by blast lemma E\<^sub>i\<^sub>v: "E(x\y) \<^bold>\ (dom x \ cod y \<^bold>\ E(cod y))" using S3 by metis lemma A\<^sub>i\<^sub>v: "x\(y\z) \ (x\y)\z" using S4 by blast lemma C\<^sub>i\<^sub>v: "(cod y)\y \ y" using S5 by blast lemma D\<^sub>i\<^sub>v: "x\(dom x) \ x" using S6 by blast end subsubsection\AxiomsSet4 entails AxiomsSet5\ context AxiomsSet4 begin lemma S1: "E(dom x) \<^bold>\ E x" using S\<^sub>i\<^sub>v by blast lemma S2: "E(cod y) \<^bold>\ E y" using S\<^sub>i\<^sub>v by blast lemma S3: "E(x\y) \<^bold>\ dom x \ cod y" using E\<^sub>i\<^sub>v by metis lemma S4: "x\(y\z) \ (x\y)\z" using A\<^sub>i\<^sub>v by blast lemma S5: "(cod y)\y \ y" using C\<^sub>i\<^sub>v by blast lemma S6: "x\(dom x) \ x" using D\<^sub>i\<^sub>v by blast end section\The Axioms Sets by Freyd and Scedrov \cite{FreydScedrov90}\ subsection\AxiomsSet6\ text\The axioms by Freyd and Scedrov \cite{FreydScedrov90} in our notation, when being corrected (cf. the modification in axiom A1). Freyd and Scedrov employ a different notation for $dom\ x$ and $cod\ x$. They denote these operations by $\Box x$ and $x\Box$. Moreover, they employ diagrammatic composition instead of the set-theoretic definition (functional composition from right to left) used so far. We leave it to the reader to verify that their axioms corresponds to the axioms presented here modulo an appropriate conversion of notation.\ locale AxiomsSet6 = assumes A1: "E(x\y) \<^bold>\ dom x \ cod y" and A2a: "cod(dom x) \ dom x" and A2b: "dom(cod y) \ cod y" and A3a: "x\(dom x) \ x" and A3b: "(cod y)\y \ y" and A4a: "dom(x\y) \ dom((dom x)\y)" and A4b: "cod(x\y) \ cod(x\(cod y))" and A5: "x\(y\z) \ (x\y)\z" begin lemma True nitpick [satisfy] oops \ \Consistency\ lemma assumes "\x. \<^bold>\(E x)" shows True nitpick [satisfy] oops \ \Consistency\ lemma assumes "(\x. \<^bold>\(E x)) \ (\x. (E x))" shows True nitpick [satisfy] oops \ \Consistency\ end subsubsection\AxiomsSet6 entails AxiomsSet5\ context AxiomsSet6 begin lemma S1: "E(dom x) \<^bold>\ E x" by (metis A1 A2a A3a) lemma S2: "E(cod y) \<^bold>\ E y" using A1 A2b A3b by metis lemma S3: "E(x\y) \<^bold>\ dom x \ cod y" by (metis A1) lemma S4: "x\(y\z) \ (x\y)\z" using A5 by blast lemma S5: "(cod y)\y \ y" using A3b by blast lemma S6: "x\(dom x) \ x" using A3a by blast lemma A4aRedundant: "dom(x\y) \ dom((dom x)\y)" using A1 A2a A3a A5 by metis lemma A4bRedundant: "cod(x\y) \ cod(x\(cod y))" using A1 A2b A3b A5 by (smt (verit)) - lemma A2aRedundant: "cod(dom x) \ dom x" using A1 A3a A3b A4a A4b by smt - lemma A2bRedundant: "dom(cod y) \ cod y" using A1 A3a A3b A4a A4b by smt + lemma A2aRedundant: "cod(dom x) \ dom x" using A1 A3a A3b A4a A4b by (smt (verit)) + lemma A2bRedundant: "dom(cod y) \ cod y" using A1 A3a A3b A4a A4b by (smt (verit)) end subsubsection\AxiomsSet5 entails AxiomsSet6\ context AxiomsSet5 begin lemma A1: "E(x\y) \<^bold>\ dom x \ cod y" using S3 by blast lemma A2: "cod(dom x) \ dom x" by (metis S1 S2 S3 S6) lemma A2b: "dom(cod y) \ cod y" using S1 S2 S3 S5 by metis lemma A3a: "x\(dom x) \ x" using S6 by auto lemma A3b: "(cod y)\y \ y" using S5 by blast lemma A4a: "dom(x\y) \ dom((dom x)\y)" by (metis S1 S3 S4 S5 S6) lemma A4b: "cod(x\y) \ cod(x\(cod y))" by (metis (full_types) S2 S3 S4 S5 S6) lemma A5: "x\(y\z) \ (x\y)\z" using S4 by blast end subsection\AxiomsSet7 (technically flawed)\ text\The axioms by Freyd and Scedrov in our notation, without the suggested correction of axiom A1. This axioms set is technically flawed when encoded in our given context. It leads to a constricted inconsistency.\ locale AxiomsSet7 = assumes A1: "E(x\y) \<^bold>\ dom x \ cod y" and A2a: "cod(dom x) \ dom x " and A2b: "dom(cod y) \ cod y" and A3a: "x\(dom x) \ x" and A3b: "(cod y)\y \ y" and A4a: "dom(x\y) \ dom((dom x)\y)" and A4b: "cod(x\y) \ cod(x\(cod y))" and A5: "x\(y\z) \ (x\y)\z" begin lemma True nitpick [satisfy] oops \ \Consistency\ (* lemma assumes "\x. \<^bold>\(E x)" shows True nitpick [satisfy] oops --{*No model found*} lemma assumes "(\x. \<^bold>\(E x)) \ (\x. (E x))" shows True nitpick [satisfy] oops --{*No model found*} *) lemma InconsistencyAutomatic: "(\x. \<^bold>\(E x)) \<^bold>\ False" by (metis A1 A2a A3a) \ \Inconsistency\ lemma "\x. E x" using InconsistencyAutomatic by auto lemma InconsistencyInteractive: assumes NEx: "\x. \<^bold>\(E x)" shows False proof - obtain a where 1: "\<^bold>\(E a)" using NEx by auto have 2: "a\(dom a) \ a" using A3a by blast have 3: "\<^bold>\(E(a\(dom a)))" using 1 2 by metis have 4: "E(a\(dom a)) \<^bold>\ dom a \ cod(dom a)" using A1 by blast have 5: "cod(dom a) \ dom a" using A2a by blast have 6: "E(a\(dom a)) \<^bold>\ dom a \ dom a" using 4 5 by auto have 7: "E(a\(dom a))" using 6 by blast then show ?thesis using 7 3 by blast qed end subsection\AxiomsSet7orig (technically flawed)\ text\The axioms by Freyd and Scedrov in their original notation, without the suggested correction of axiom A1. We present the constricted inconsistency argument from above once again, but this time in the original notation of Freyd and Scedrov.\ locale AxiomsSet7orig = fixes source:: "i\i" ("\_" [108] 109) and target:: "i\i" ("_\" [110] 111) and compositionF:: "i\i\i" (infix "\<^bold>\" 110) assumes A1: "E(x\<^bold>\y) \<^bold>\ (x\ \ \y)" and A2a: "((\x)\) \ \x" and A2b: "\(x\) \ \x" and A3a: "(\x)\<^bold>\x \ x" and A3b: "x\<^bold>\(x\) \ x" and A4a: "\(x\<^bold>\y) \ \(x\<^bold>\(\y))" and A4b: "(x\<^bold>\y)\ \ ((x\)\<^bold>\y)\" and A5: "x\<^bold>\(y\<^bold>\z) \ (x\<^bold>\y)\<^bold>\z" begin lemma True nitpick [satisfy] oops \ \Consistency\ (* lemma assumes "\x. \<^bold>\(E x)" shows True nitpick [satisfy] oops --{*No model found*} lemma assumes "(\x. \<^bold>\(E x)) \ (\x. (E x))" shows True nitpick [satisfy] oops --{*No model found*} *) lemma InconsistencyAutomatic: "(\x. \<^bold>\(E x)) \<^bold>\ False" by (metis A1 A2a A3a) \ \Inconsistency\ lemma "\x. E x" using InconsistencyAutomatic by auto lemma InconsistencyInteractive: assumes NEx: "\x. \<^bold>\(E x)" shows False proof - obtain a where 1: "\<^bold>\(E a)" using assms by auto have 2: "(\a)\<^bold>\a \ a" using A3a by blast have 3: "\<^bold>\(E((\a)\<^bold>\a))" using 1 2 by metis have 4: "E((\a)\<^bold>\a) \<^bold>\ (\a)\ \ \a" using A1 by blast have 5: "(\a)\ \ \a" using A2a by blast have 6: "E((\a)\<^bold>\a)" using 4 5 by blast then show ?thesis using 6 3 by blast qed end subsection\AxiomsSet8 (algebraic reading, still technically flawed)\ text\The axioms by Freyd and Scedrov in our notation again, but this time we adopt an algebraic reading of the free variables, meaning that they range over existing morphisms only.\ locale AxiomsSet8 = assumes B1: "\<^bold>\x.\<^bold>\y. E(x\y) \<^bold>\ dom x \ cod y" and B2a: "\<^bold>\x. cod(dom x) \ dom x " and B2b: "\<^bold>\y. dom(cod y) \ cod y" and B3a: "\<^bold>\x. x\(dom x) \ x" and B3b: "\<^bold>\y. (cod y)\y \ y" and B4a: "\<^bold>\x.\<^bold>\y. dom(x\y) \ dom((dom x)\y)" and B4b: "\<^bold>\x.\<^bold>\y. cod(x\y) \ cod(x\(cod y))" and B5: "\<^bold>\x.\<^bold>\y.\<^bold>\z. x\(y\z) \ (x\y)\z" begin lemma True nitpick [satisfy] oops \ \Consistency\ lemma assumes "\x. \<^bold>\(E x)" shows True nitpick [satisfy] oops \ \Consistency\ lemma assumes "(\x. \<^bold>\(E x)) \ (\x. (E x))" shows True nitpick [satisfy] oops \ \Consistency\ end text\None of the axioms in AxiomsSet5 are implied.\ context AxiomsSet8 begin lemma S1: "E(dom x) \<^bold>\ E x" nitpick oops \ \Nitpick finds a countermodel\ lemma S2: "E(cod y) \<^bold>\ E y" nitpick oops \ \Nitpick finds a countermodel\ lemma S3: "E(x\y) \<^bold>\ dom x \ cod y" nitpick oops \ \Nitpick finds a countermodel\ lemma S4: "x\(y\z) \ (x\y)\z" nitpick oops \ \Nitpick finds a countermodel\ lemma S5: "(cod y)\y \ y" nitpick oops \ \Nitpick finds a countermodel\ lemma S6: "x\(dom x) \ x" nitpick oops \ \Nitpick finds a countermodel\ end subsection\AxiomsSet8Strict (algebraic reading)\ text\The situation changes when strictness conditions are postulated. Note that in the algebraic framework of Freyd and Scedrov such conditions have to be assumed as given in the logic, while here we can explicitly encode them as axioms.\ locale AxiomsSet8Strict = AxiomsSet8 + assumes B0a: "E(x\y) \<^bold>\ (E x \<^bold>\ E y)" and B0b: "E(dom x) \<^bold>\ E x" and B0c: "E(cod x) \<^bold>\ E x" begin lemma True nitpick [satisfy] oops \ \Consistency\ lemma assumes "\x. \<^bold>\(E x)" shows True nitpick [satisfy] oops \ \Consistency\ lemma assumes "(\x. \<^bold>\(E x)) \ (\x. (E x))" shows True nitpick [satisfy] oops \ \Consistency\ end subsubsection\AxiomsSet8Strict entails AxiomsSet5\ context AxiomsSet8Strict begin lemma S1: "E(dom x) \<^bold>\ E x" using B0b by blast lemma S2: "E(cod y) \<^bold>\ E y" using B0c by blast lemma S3: "E(x\y) \<^bold>\ dom x \ cod y" by (metis B0a B0b B0c B1 B3a) lemma S4: "x\(y\z) \ (x\y)\z" by (meson B0a B5) lemma S5: "(cod y)\y \ y" using B0a B3b by blast lemma S6: "x\(dom x) \ x" using B0a B3a by blast end subsubsection\AxiomsSet5 entails AxiomsSet8Strict\ context AxiomsSet5 begin lemma B0a: "E(x\y) \<^bold>\ (E x \<^bold>\ E y)" using S1 S2 S3 by blast lemma B0b: "E(dom x) \<^bold>\ E x" using S1 by blast lemma B0c: "E(cod x) \<^bold>\ E x" using S2 by blast lemma B1: "\<^bold>\x.\<^bold>\y. E(x\y) \<^bold>\ dom x \ cod y" by (metis S3 S5) lemma B2a: "\<^bold>\x. cod(dom x) \ dom x" using A2 by blast lemma B2b: "\<^bold>\y. dom(cod y) \ cod y" using A2b by blast lemma B3a: "\<^bold>\x. x\(dom x) \ x" using S6 by blast lemma B3b: "\<^bold>\y. (cod y)\y \ y" using S5 by blast lemma B4a: "\<^bold>\x.\<^bold>\y. dom(x\y) \ dom((dom x)\y)" by (metis S1 S3 S4 S6) lemma B4b: "\<^bold>\x.\<^bold>\y. cod(x\y) \ cod(x\(cod y))" by (metis S1 S2 S3 S4 S5) lemma B5: "\<^bold>\x.\<^bold>\y.\<^bold>\z. x\(y\z) \ (x\y)\z" using S4 by blast end subsubsection\AxiomsSet8Strict is Redundant\ text\AxiomsSet8Strict is redundant: either the B2-axioms can be omitted or the B4-axioms.\ context AxiomsSet8Strict begin lemma B2aRedundant: "\<^bold>\x. cod(dom x) \ dom x " by (metis B0a B1 B3a) lemma B2bRedundant: "\<^bold>\y. dom(cod y) \ cod y" by (metis B0a B1 B3b) lemma B4aRedundant: "\<^bold>\x.\<^bold>\y. dom(x\y) \ dom((dom x)\y)" by (metis B0a B0b B1 B3a B5) lemma B4bRedundant: "\<^bold>\x.\<^bold>\y. cod(x\y) \ cod(x\(cod y))" by (metis B0a B0c B1 B3b B5) end section\The Axioms Sets of Mac Lane \cite{MacLane48}\ text\We analyse the axioms set suggested by Mac Lane~\cite{MacLane48} already in 1948. As for the theory by Freyd and Scedrov above, which was developed much later, we need to assume strictness of composition to show equivalence to our previous axiom sets. Note that his complicated conditions on existence of compositions proved to be unnecessary, as we show. It shows it is hard to think about partial operations.\ locale AxiomsSetMcL = assumes C\<^sub>0 : "E(x\y) \<^bold>\ (E x \<^bold>\ E y)" and C\<^sub>1 : "\<^bold>\\ \ \. (E(\\\) \<^bold>\ E((\\\)\\)) \<^bold>\ E(\\\)" and C\<^sub>1': "\<^bold>\\ \ \. (E(\\\) \<^bold>\ E(\\(\\\))) \<^bold>\ E(\\\)" and C\<^sub>2 : "\<^bold>\\ \ \. (E(\\\) \<^bold>\ E(\\\)) \<^bold>\ (E((\\\)\\) \<^bold>\ E(\\(\\\)) \<^bold>\ ((\\\)\\) = (\\(\\\)))" and C\<^sub>3 : "\<^bold>\\. \<^bold>\eD. IDMcL(eD) \<^bold>\ E(\\eD)" and C\<^sub>4 : "\<^bold>\\. \<^bold>\eR. IDMcL(eR) \<^bold>\ E(eR\\)" begin lemma True nitpick [satisfy] oops \ \Consistency\ lemma assumes "\x. \<^bold>\(E x)" shows True nitpick [satisfy] oops \ \Consistency\ lemma assumes "(\x. \<^bold>\(E x)) \ (\x. (E x))" shows True nitpick [satisfy] oops \ \Consistency\ end text\Remember that IDMcL was defined on p.~\pageref{IDMcL} and proved equivalent to ID.\ subsection\AxiomsSetMcL entails AxiomsSet1\ context AxiomsSetMcL begin lemma S\<^sub>i: "E(x\y) \<^bold>\ (E x \<^bold>\ E y)" using C\<^sub>0 by blast lemma E\<^sub>i: "E(x\y) \<^bold>\ (E x \<^bold>\ E y \<^bold>\ (\<^bold>\z. z\z \ z \<^bold>\ x\z \ x \<^bold>\ z\y \ y))" by (metis C\<^sub>2) lemma A\<^sub>i: "x\(y\z) \ (x\y)\z" by (metis C\<^sub>1 C\<^sub>1' C\<^sub>2 C\<^sub>0) lemma C\<^sub>i: "\<^bold>\y.\<^bold>\i. ID i \<^bold>\ i\y \ y" using C\<^sub>4 by fastforce lemma D\<^sub>i: "\<^bold>\x.\<^bold>\j. ID j \<^bold>\ x\j \ x" using C\<^sub>3 by fastforce end subsection\AxiomsSet1 entails AxiomsSetMcL\ context AxiomsSet1 begin lemma C\<^sub>0 : "E(x\y) \<^bold>\ (E x \<^bold>\ E y)" using S\<^sub>i by blast lemma C\<^sub>1 : "\<^bold>\\ \ \. (E(\\\) \<^bold>\ E((\\\)\\)) \<^bold>\ E(\\\)" by (metis A\<^sub>i S\<^sub>i) lemma C\<^sub>1': "\<^bold>\\ \ \. (E(\\\) \<^bold>\ E(\\(\\\))) \<^bold>\ E(\\\)" by (metis A\<^sub>i S\<^sub>i) - lemma C\<^sub>2 : "\<^bold>\\ \ \. (E(\\\) \<^bold>\ E(\\\)) \<^bold>\ (E((\\\)\\) \<^bold>\ E(\\(\\\)) \<^bold>\ ((\\\)\\) = (\\(\\\)))" by (smt A\<^sub>i C\<^sub>i E\<^sub>i S\<^sub>i) + lemma C\<^sub>2 : "\<^bold>\\ \ \. (E(\\\) \<^bold>\ E(\\\)) \<^bold>\ (E((\\\)\\) \<^bold>\ E(\\(\\\)) \<^bold>\ ((\\\)\\) = (\\(\\\)))" by (smt (verit) A\<^sub>i C\<^sub>i E\<^sub>i S\<^sub>i) lemma C\<^sub>3 : "\<^bold>\\. \<^bold>\eD. IDMcL(eD) \<^bold>\ E(\\eD)" using D\<^sub>i by force lemma C\<^sub>4 : "\<^bold>\\. \<^bold>\eR. IDMcL(eR) \<^bold>\ E(eR\\)" using C\<^sub>i by force end subsection\Skolemization of the Axioms of Mac Lane\ text\Mac Lane employs diagrammatic composition instead of the set-theoretic definition as used in our axiom sets. As we have seen above, this is not a problem as long as composition is the only primitive. But when adding the Skolem terms $dom$ and $cod$ care must be taken and we should actually transform all axioms into a common form. Below we address this (in a minimal way) by using $dom$ in axiom @{term "C\<^sub>3s"} and $cod$ in axiom @{term "C\<^sub>4s"}, which is opposite of what Mac Lane proposed. For this axioms set we then show equivalence to AxiomsSet1/2/5.\ locale SkolemizedAxiomsSetMcL = assumes C\<^sub>0s : "(E(x\y) \<^bold>\ (E x \<^bold>\ E y)) \ (E(dom x) \<^bold>\ E x) \ (E(cod y) \<^bold>\ E y)" and C\<^sub>1s : "\<^bold>\\ \ \. (E(\\\) \<^bold>\ E((\\\)\\)) \<^bold>\ E(\\\)" and C\<^sub>1's: "\<^bold>\\ \ \. (E(\\\) \<^bold>\ E(\\(\\\))) \<^bold>\ E(\\\)" and C\<^sub>2s : "\<^bold>\\ \ \. (E(\\\) \<^bold>\ E(\\\)) \<^bold>\ (E((\\\)\\) \<^bold>\ E(\\(\\\)) \<^bold>\ ((\\\)\\) = (\\(\\\)))" and C\<^sub>3s : "\<^bold>\\. IDMcL(dom \) \<^bold>\ E(\\(dom \))" and C\<^sub>4s : "\<^bold>\\. IDMcL(cod \) \<^bold>\ E((cod \)\\)" begin lemma True nitpick [satisfy] oops \ \Consistency\ lemma assumes "\x. \<^bold>\(E x)" shows True nitpick [satisfy] oops \ \Consistency\ lemma assumes "(\x. \<^bold>\(E x)) \ (\x. (E x))" shows True nitpick [satisfy] oops \ \Consistency\ end subsection\SkolemizedAxiomsSetMcL entails AxiomsSetMcL and AxiomsSet1-5\ context SkolemizedAxiomsSetMcL begin lemma C\<^sub>0 : "E(x\y) \<^bold>\ (E x \<^bold>\ E y)" using C\<^sub>0s by blast lemma C\<^sub>1 : "\<^bold>\\ \ \. (E(\\\) \<^bold>\ E((\\\)\\)) \<^bold>\ E(\\\)" using C\<^sub>1s by blast lemma C\<^sub>1': "\<^bold>\\ \ \. (E(\\\) \<^bold>\ E(\\(\\\))) \<^bold>\ E(\\\)" using C\<^sub>1's by blast lemma C\<^sub>2 : "\<^bold>\\ \ \. (E(\\\) \<^bold>\ E(\\\)) \<^bold>\ (E((\\\)\\) \<^bold>\ E(\\(\\\)) \<^bold>\ ((\\\)\\) = (\\(\\\)))" using C\<^sub>2s by blast lemma C\<^sub>3 : "\<^bold>\\. \<^bold>\eD. IDMcL(eD) \<^bold>\ E(\\eD)" by (metis C\<^sub>0s C\<^sub>3s) lemma C\<^sub>4 : "\<^bold>\\. \<^bold>\eR. IDMcL(eR) \<^bold>\ E(eR\\)" by (metis C\<^sub>0s C\<^sub>4s) lemma S\<^sub>i: "E(x\y) \<^bold>\ (E x \<^bold>\ E y)" using C\<^sub>0s by blast lemma E\<^sub>i: "E(x\y) \<^bold>\ (E x \<^bold>\ E y \<^bold>\ (\<^bold>\z. z\z \ z \<^bold>\ x\z \ x \<^bold>\ z\y \ y))" by (metis C\<^sub>2s) lemma A\<^sub>i: "x\(y\z) \ (x\y)\z" by (metis C\<^sub>1s C\<^sub>1's C\<^sub>2s C\<^sub>0s) lemma C\<^sub>i: "\<^bold>\y.\<^bold>\i. ID i \<^bold>\ i\y \ y" by (metis C\<^sub>0s C\<^sub>4s) lemma D\<^sub>i: "\<^bold>\x.\<^bold>\j. ID j \<^bold>\ x\j \ x" by (metis C\<^sub>0s C\<^sub>3s) lemma S\<^sub>i\<^sub>i: "(E(x\y) \<^bold>\ (E x \<^bold>\ E y)) \<^bold>\ (E(dom x ) \<^bold>\ E x) \<^bold>\ (E(cod y) \<^bold>\ E y)" using C\<^sub>0s by blast lemma E\<^sub>i\<^sub>i: "E(x\y) \<^bold>\ (E x \<^bold>\ E y \<^bold>\ (\<^bold>\z. z\z \ z \<^bold>\ x\z \ x \<^bold>\ z\y \ y))" by (metis C\<^sub>2s) lemma A\<^sub>i\<^sub>i: "x\(y\z) \ (x\y)\z" by (metis C\<^sub>1s C\<^sub>1's C\<^sub>2s C\<^sub>0s) lemma C\<^sub>i\<^sub>i: "E y \<^bold>\ (ID(cod y) \<^bold>\ (cod y)\y \ y)" using C\<^sub>4s by auto lemma D\<^sub>i\<^sub>i: "E x \<^bold>\ (ID(dom x) \<^bold>\ x\(dom x) \ x)" using C\<^sub>3s by auto \ \AxiomsSets3/4 are omitted here; we already know they are equivalent.\ lemma S1: "E(dom x) \<^bold>\ E x" using C\<^sub>0s by blast lemma S2: "E(cod y) \<^bold>\ E y" using C\<^sub>0s by blast lemma S3: "E(x\y) \<^bold>\ dom x \ cod y" by (metis (full_types) C\<^sub>0s C\<^sub>1s C\<^sub>1's C\<^sub>2s C\<^sub>3s C\<^sub>4s) lemma S4: "x\(y\z) \ (x\y)\z" by (metis C\<^sub>0s C\<^sub>1s C\<^sub>1's C\<^sub>2s) lemma S5: "(cod y)\y \ y" using C\<^sub>0s C\<^sub>4s by blast lemma S6: "x\(dom x) \ x" using C\<^sub>0s C\<^sub>3s by blast end (*<*) end (*>*) diff --git a/thys/Cubic_Quartic_Equations/Complex_Roots.thy b/thys/Cubic_Quartic_Equations/Complex_Roots.thy --- a/thys/Cubic_Quartic_Equations/Complex_Roots.thy +++ b/thys/Cubic_Quartic_Equations/Complex_Roots.thy @@ -1,516 +1,516 @@ section \$n$-th roots of complex numbers\ theory Complex_Roots imports Complex_Geometry.More_Complex Algebraic_Numbers.Complex_Algebraic_Numbers Factor_Algebraic_Polynomial.Roots_via_IA "HOL-Library.Product_Lexorder" begin subsection \An algorithm to compute all complex roots of (algebraic) complex numbers\ definition all_croots :: "nat \ complex \ complex list" where "all_croots n x = (if n = 0 then [] else if algebraic x then (let p = min_int_poly x; q = poly_nth_root n p; xs = complex_roots_of_int_poly q in filter (\ y. y^n = x) xs) else (SOME ys. set ys = {y. y^n = x}))" lemma all_croots: assumes n0: "n \ 0" shows "set (all_croots n x) = {y. y^n = x}" proof (cases "algebraic x") case True hence id: "(if n = 0 then y else if algebraic x then z else u) = z" for y z u :: "complex list" using n0 by auto define p where "p = poly_nth_root n (min_int_poly x)" show ?thesis unfolding Let_def p_def[symmetric] all_croots_def id proof (standard, force, standard, simp) fix y assume y: "y ^n = x" have "min_int_poly x represents x" using True by auto from represents_nth_root[OF n0 y this] have "p represents y" unfolding p_def by auto thus "y \ set (complex_roots_of_int_poly p)" by (subst complex_roots_of_int_poly, auto) qed next case False hence id: "(if n = 0 then y else if algebraic x then z else u) = u" for y z u :: "complex list" using n0 by auto show ?thesis unfolding Let_def all_croots_def id by (rule someI_ex, rule finite_list, insert n0, blast) qed text \TODO: One might change @{const complex_roots_of_int_poly} to @{const complex_roots_of_int_poly3} in order to avoid an unnecessary factorization of an integer polynomial. However, then this change already needs to be performed within the definition of @{const all_croots}.\ lift_definition all_croots_part1 :: "nat \ complex \ complex genuine_roots_aux" is "\ n x. if n = 0 \ x = 0 \ \ algebraic x then (1,[],0, filter_fun_complex 1) else let p = min_int_poly x; q = poly_nth_root n p; zeros = complex_roots_of_int_poly q; r = Polynomial.monom 1 n - [:x:] in (r,zeros, n, filter_fun_complex r)" subgoal for n x proof (cases "n = 0 \ x = 0 \ \ algebraic x") case True thus ?thesis by (simp add: filter_fun_complex) next case False hence *: "algebraic x" "n \ 0" "x \ 0" by auto { fix z assume zn: "z^n = x" from *(1) have repr: "min_int_poly x represents x" by auto from represents_nth_root[OF *(2) zn repr] have "poly_nth_root n (min_int_poly x) represents z" . } moreover have "card {z. z ^ n = x} = n" by (rule card_nth_roots) (use * in auto) ultimately show ?thesis using * by (auto simp: Let_def complex_roots_of_int_poly filter_fun_complex poly_monom) qed done lemma all_croots_code[code]: "all_croots n x = (if n = 0 then [] else if x = 0 then [0] else if algebraic x then genuine_roots_impl (all_croots_part1 n x) else Code.abort (STR ''all_croots invoked on non-algebraic number'') (\ _. all_croots n x))" proof (cases "n = 0") case True thus ?thesis unfolding all_croots_def by simp next case n: False show ?thesis proof (cases "x = 0") case x: False show ?thesis proof (cases "algebraic x") case False with n x show ?thesis by simp next case True define t where "t = ?thesis" have "t \ filter (\y. y ^ n = x) (complex_roots_of_int_poly (poly_nth_root n (min_int_poly x))) = genuine_roots_impl (all_croots_part1 n x)" unfolding t_def by (subst all_croots_def[of n x], unfold Let_def, insert n x True, auto) also have "\" using n x True unfolding genuine_roots_impl_def by (transfer, simp add: Let_def genuine_roots_def poly_monom) finally show ?thesis unfolding t_def by simp qed next case x: True have "set (all_croots n 0) = {0}" unfolding all_croots[OF n] using n by simp moreover have "distinct (all_croots n 0)" unfolding all_croots_def using n by (auto intro!: distinct_filter complex_roots_of_int_poly) ultimately have "all_croots n 0 = [0]" by (smt (verit, del_insts) distinct.simps(2) distinct_singleton insert_ident list.set_cases list.set_intros(1) list.simps(15) mem_Collect_eq set_empty singleton_conv) moreover have "?thesis \ all_croots n 0 = [0]" using n x by simp ultimately show ?thesis by auto qed qed subsection \A definition of \emph{the} complex root of a complex number\ text \While the definition of the complex root is quite natural and easy, the main task is a criterion to determine which of all possible roots of a complex number is the chosen one.\ definition croot :: "nat \ complex \ complex" where "croot n x = (rcis (root n (cmod x)) (Arg x / of_nat n))" lemma croot_0[simp]: "croot n 0 = 0" "croot 0 x = 0" unfolding croot_def by auto lemma croot_power: assumes n: "n \ 0" shows "(croot n x) ^ n = x" unfolding croot_def DeMoivre2 by (subst real_root_pow_pos2, insert n, auto simp: rcis_cmod_Arg) lemma Arg_of_real: "Arg (of_real x) = (if x < 0 then pi else 0)" proof (cases "x = 0") case False hence "x < 0 \ x > 0" by auto thus ?thesis by (intro cis_Arg_unique, auto simp: complex_sgn_def scaleR_complex.ctr complex_eq_iff) qed (auto simp: Arg_def) lemma Arg_rcis_cis[simp]: assumes "x > 0" shows "Arg (rcis x y) = Arg (cis y)" using assms unfolding rcis_def by simp lemma cis_Arg_1[simp]: "cis (Arg 1) = 1" using Arg_of_real[of 1] by simp lemma cis_Arg_power[simp]: assumes "x \ 0" shows "cis (Arg (x ^ n)) = cis (Arg x * real n)" proof (induct n) case (Suc n) show ?case unfolding power.simps proof (subst cis_arg_mult) show "cis (Arg x + Arg (x ^ n)) = cis (Arg x * real (Suc n))" unfolding mult.commute[of "Arg x"] DeMoivre[symmetric] unfolding power.simps using Suc by (metis DeMoivre cis_mult mult.commute) show "x * x ^ n \ 0" using assms by auto qed qed simp lemma Arg_croot[simp]: "Arg (croot n x) = Arg x / real n" proof (cases "n = 0 \ x = 0") case True thus ?thesis by (auto simp: Arg_def) next case False hence n: "n \ 0" and x: "x \ 0" by auto let ?root = "croot n x" from n have n1: "real n \ 1" "real n > 0" "real n \ 0" by auto have bounded: "- pi < Arg x / real n \ Arg x / real n \ pi" proof (cases "Arg x < 0") case True from Arg_bounded[of x] have "- pi < Arg x" by auto also have "\ \ Arg x / real n" using n1 True - by (smt (z3) div_by_1 divide_minus_left frac_le) + by (smt (verit) div_by_1 divide_minus_left frac_le) finally have one: "- pi < Arg x / real n" . have "Arg x / real n \ 0" using True n1 by (smt (verit) divide_less_0_iff) also have "\ \ pi" by simp finally show ?thesis using one by auto next case False hence ax: "Arg x \ 0" by auto have "Arg x / real n \ Arg x" using n1 ax by (smt (verit) div_by_1 frac_le) also have "\ \ pi" using Arg_bounded[of x] by simp finally have one: "Arg x / real n \ pi" . have "-pi < 0" by simp also have "\ \ Arg x / real n" using ax n1 by simp finally show ?thesis using one by auto qed have "Arg ?root = Arg (cis (Arg x / real n))" unfolding croot_def using x n by simp also have "\ = Arg x / real n" by (rule cis_Arg_unique, force, insert bounded, auto) finally show ?thesis . qed lemma cos_abs[simp]: "cos (abs x :: real) = cos x" proof (cases "x < 0") case True hence abs: "abs x = - x" by simp show ?thesis unfolding abs by simp qed simp lemma cos_mono_le: assumes "abs x \ pi" and "abs y \ pi" shows "cos x \ cos y \ abs y \ abs x" proof - have "cos x \ cos y \ cos (abs x) \ cos (abs y)" by simp also have "\ \ abs y \ abs x" by (subst cos_mono_le_eq, insert assms, auto) finally show ?thesis . qed lemma abs_add_2_mult_bound: fixes x :: "'a :: linordered_idom" assumes xy: "\x\ \ y" shows "\x\ \ \x + 2 * of_int i * y\" proof (cases "i = 0") case i: False let ?oi = "of_int :: int \ 'a" from xy have y: "y \ 0" by auto consider (pp) "x \ 0" "i \ 0" | (nn) "x \ 0" "i \ 0" | (pn) "x \ 0" "i \ 0" | (np) "x \ 0" "i \ 0" by linarith thus ?thesis proof cases case pp thus ?thesis using y by simp next case nn have "x \ x + 2 * ?oi i * y" using nn y by (simp add: mult_nonneg_nonpos2) with nn show ?thesis by linarith next case pn with i have "0 \ x" "i < 0" by auto define j where "j = nat (-i) - 1" define z where "z = x - 2 * y" define u where "u = 2 * ?oi (nat j) * y" have u: "u \ 0" unfolding u_def using y by auto have i: "i = - int (Suc j)" using \i < 0\ unfolding j_def by simp have id: "x + 2 * ?oi i * y = z - u" unfolding i z_def u_def by (simp add: field_simps) have z: "z \ 0" "abs z \ x" using xy y pn(1) unfolding z_def by auto show ?thesis unfolding id using pn(1) z u by simp next case np with i have "0 \ x" "i > 0" by auto define j where "j = nat i - 1" have i: "i = int (Suc j)" using \i > 0\ unfolding j_def by simp define u where "u = 2 * ?oi (nat j) * y" have u: "u \ 0" unfolding u_def using y by auto define z where "z = - x - 2 * y" have id: "x + 2 * ?oi i * y = - z + u" unfolding i z_def u_def by (simp add: field_simps) have z: "z \ 0" "abs z \ - x" using xy y np(1) unfolding z_def by auto show ?thesis unfolding id using np(1) z u by simp qed qed simp lemma abs_eq_add_2_mult: fixes y :: "'a :: linordered_idom" assumes abs_id: "\x\ = \x + 2 * of_int i * y\" and xy: "- y < x" "x \ y" and i: "i \ 0" shows "x = y \ i = -1" proof - let ?oi = "of_int :: int \ 'a" from xy have y: "y > 0" by auto consider (pp) "x \ 0" "i \ 0" | (nn) "x < 0" "i \ 0" | (pn) "x \ 0" "i \ 0" | (np) "x < 0" "i \ 0" by linarith hence "?thesis \ x = ?oi (- i) * y" proof cases case pp thus ?thesis using y abs_id xy i by simp next case nn hence "\x + 2 * ?oi i * y\ = - (x + 2 * ?oi i * y)" using y nn by (intro abs_of_nonpos add_nonpos_nonpos, force, simp, intro mult_nonneg_nonpos, auto) thus ?thesis using y abs_id xy i nn by auto next case pn with i have "0 \ x" "i < 0" by auto define j where "j = nat (-i) - 1" define z where "z = x - 2 * y" define u where "u = 2 * ?oi (nat j) * y" have u: "u \ 0" unfolding u_def using y by auto have i: "i = - int (Suc j)" using \i < 0\ unfolding j_def by simp have id: "x + 2 * ?oi i * y = z - u" unfolding i z_def u_def by (simp add: field_simps) have z: "z \ 0" "abs z \ x" using xy y pn(1) unfolding z_def by auto from abs_id[unfolded id] have "z - u = -x " using z u pn by auto from this[folded id] have "x = of_int (-i) * y" by auto thus ?thesis by auto next case np with i have "0 \ x" "i > 0" by auto define j where "j = nat i - 1" have i: "i = int (Suc j)" using \i > 0\ unfolding j_def by simp define u where "u = 2 * ?oi (nat j) * y" have u: "u \ 0" unfolding u_def using y by auto define z where "z = - x - 2 * y" have id: "x + 2 * ?oi i * y = - z + u" unfolding i z_def u_def by (simp add: field_simps) have z: "z \ 0" using xy y np(1) unfolding z_def by auto from abs_id[unfolded id] have "- z + u = - x" using u z np by auto from this[folded id] have "x = of_int (- i) * y" by auto thus ?thesis by auto qed thus ?thesis proof assume "x = ?oi (- i) * y" with xy i y show ?thesis by (smt (verit, ccfv_SIG) less_le minus_less_iff mult_le_cancel_right2 mult_minus1_right mult_minus_left mult_of_int_commute of_int_hom.hom_one of_int_le_1_iff of_int_minus) qed qed text \This is the core lemma. It tells us that @{const croot} will choose the principal root, i.e. the root with largest real part and if there are two roots with identical real part, then the largest imaginary part. This criterion will be crucial for implementing @{const croot}.\ lemma croot_principal: assumes n: "n \ 0" and y: "y ^ n = x" and neq: "y \ croot n x" shows "Re y < Re (croot n x) \ Re y = Re (croot n x) \ Im y < Im (croot n x)" proof (cases "x = 0") case True with neq y have False by auto thus ?thesis .. next case x: False let ?root = "croot n x" from n have n1: "real n \ 1" "real n > 0" "real n \ 0" by auto from x y n have y0: "y \ 0" by auto from croot_power[OF n, of x] y have id: "?root ^ n = y ^ n" by simp hence "cmod (?root ^ n) = cmod (y ^ n)" by simp hence norm_eq: "cmod ?root = cmod y" using n unfolding norm_power by (meson gr_zeroI norm_ge_zero power_eq_imp_eq_base) have "cis (Arg y * real n) = cis (Arg (y^n))" by (subst cis_Arg_power[OF y0], simp) also have "\ = cis (Arg x)" using y by simp finally have ciseq: "cis (Arg y * real n) = cis (Arg x)" by simp from cis_eq[OF ciseq] obtain i where "Arg y * real n - Arg x = 2 * real_of_int i * pi" by auto hence "Arg y * real n = Arg x + 2 * real_of_int i * pi" by auto from arg_cong[OF this, of "\ x. x / real n"] n1 have Argy: "Arg y = Arg ?root + 2 * real_of_int i * pi / real n" by (auto simp: field_simps) have i0: "i \ 0" proof assume "i = 0" hence "Arg y = Arg ?root" unfolding Argy by simp with norm_eq have "?root = y" by (metis rcis_cmod_Arg) with neq show False by simp qed from y0 have cy0: "cmod y > 0" by auto from Arg_bounded[of x] have abs_pi: "abs (Arg x) \ pi" by auto have "Re y \ Re ?root \ Re y / cmod y \ Re ?root / cmod y" using cy0 unfolding divide_le_cancel by simp also have cosy: "Re y / cmod y = cos (Arg y)" unfolding cos_arg[OF y0] .. also have cosrt: "Re ?root / cmod y = cos (Arg ?root)" unfolding norm_eq[symmetric] by (subst cos_arg, insert norm_eq cy0, auto) also have "cos (Arg y) \ cos (Arg ?root) \ abs (Arg ?root) \ abs (Arg y)" by (rule cos_mono_le, insert Arg_bounded[of y] Arg_bounded[of ?root], auto) also have "\ \ abs (Arg ?root) * real n \ abs (Arg y) * real n" unfolding mult_le_cancel_right using n1 by simp also have "\ \ abs (Arg x) \ \Arg x + 2 * real_of_int i * pi\" unfolding Argy using n1 by (simp add: field_simps) also have "\" using abs_pi by (rule abs_add_2_mult_bound) finally have le: "Re y \ Re (croot n x)" . show ?thesis proof (cases "Re y = Re (croot n x)") case False with le show ?thesis by auto next case True hence "Re y / cmod y = Re ?root / cmod y" by simp hence "cos (Arg y) = cos (Arg ?root)" unfolding cosy cosrt . hence "cos (abs (Arg y)) = cos (abs (Arg ?root))" unfolding cos_abs . from cos_inj_pi[OF _ _ _ _ this] have "abs (Arg y) = abs (Arg ?root)" using Arg_bounded[of y] Arg_bounded[of ?root] by auto hence "abs (Arg y) * real n = abs (Arg ?root) * real n" by simp hence "abs (Arg x) = \Arg x + 2 * real_of_int i * pi\" unfolding Argy using n1 by (simp add: field_simps) from abs_eq_add_2_mult[OF this _ _ \i \ 0\] Arg_bounded[of x] have Argx: "Arg x = pi" and i: "i = -1" by auto have Argy: "Arg y = -pi / real n" unfolding Argy Arg_croot i Argx by simp have "Im ?root > Im y \ Im ?root / cmod ?root > Im y / cmod y" unfolding norm_eq using cy0 by (meson divide_less_cancel divide_strict_right_mono) also have "\ \ sin (Arg ?root) > sin (Arg y)" by (subst (1 2) sin_arg, insert y0 norm_eq, auto) also have "\ \ sin (- pi / real n) < sin (pi / real n)" unfolding Argy Arg_croot Argx by simp also have \ proof - have "sin (- pi / real n) < 0" using n1 by (smt (verit) Arg_bounded Argy divide_neg_pos sin_gt_zero sin_minus) also have "\ < sin (pi / real n)" using n1 calculation by fastforce finally show ?thesis . qed finally show ?thesis using le by auto qed qed lemma croot_unique: assumes n: "n \ 0" and y: "y ^ n = x" and y_max_Re_Im: "\ z. z ^ n = x \ Re z < Re y \ Re z = Re y \ Im z \ Im y" shows "croot n x = y" proof (rule ccontr) assume "croot n x \ y" from croot_principal[OF n y this[symmetric]] have "Re y < Re (croot n x) \ Re y = Re (croot n x) \ Im y < Im (croot n x)" . with y_max_Re_Im[OF croot_power[OF n]] show False by auto qed lemma csqrt_is_croot_2: "csqrt = croot 2" proof fix x show "csqrt x = croot 2 x" proof (rule sym, rule croot_unique, force, force) let ?p = "[:-x,0,1:]" let ?cx = "csqrt x" have p: "?p = [:?cx,1:] * [:-?cx,1:]" by (simp add: power2_eq_square[symmetric]) fix y assume "y^2 = x" hence "True \ poly ?p y = 0" by (auto simp: power2_eq_square) also have "\ \ y = - ?cx \ y = ?cx" unfolding p poly_mult mult_eq_0_iff poly_root_factor by auto finally have "y = - ?cx \ y = ?cx" by simp thus "Re y < Re ?cx \ Re y = Re ?cx \ Im y \ Im ?cx" proof assume y: "y = - ?cx" show ?thesis proof (cases "Re ?cx = 0") case False with csqrt_principal[of x] have "Re ?cx > 0" by simp thus ?thesis unfolding y by simp next case True with csqrt_principal[of x] have "Im ?cx \ 0" by simp thus ?thesis unfolding y using True by auto qed qed auto qed qed lemma croot_via_root_selection: assumes roots: "set ys = { y. y^n = x}" and n: "n \ 0" shows "croot n x = arg_min_list (\ y. (- Re y, - Im y)) ys" (is "_ = arg_min_list ?f ys") proof (rule croot_unique[OF n]) let ?y = "arg_min_list ?f ys" have rt: "croot n x ^ n = x" using n by (rule croot_power) hence "croot n x \ set ys" unfolding roots by auto hence ys: "ys \ []" by auto from arg_min_list_in[OF this] have "?y \ set ys" by auto from this[unfolded roots] show "?y^n = x" by auto fix z assume "z^n = x" hence z: "z \ set ys" unfolding roots by auto from f_arg_min_list_f[OF ys, of ?f] z have "?f ?y \ ?f z" by simp thus "Re z < Re ?y \ Re z = Re ?y \ Im z \ Im ?y" by auto qed lemma croot_impl[code]: "croot n x = (if n = 0 then 0 else arg_min_list (\ y. (- Re y, - Im y)) (all_croots n x))" proof (cases "n = 0") case n0: False hence id: "(if n = 0 then y else z) = z" for y z u :: complex by auto show ?thesis unfolding id Let_def by (rule croot_via_root_selection[OF _ n0], rule all_croots[OF n0]) qed auto end \ No newline at end of file diff --git a/thys/Hahn_Jordan_Decomposition/Hahn_Jordan_Decomposition.thy b/thys/Hahn_Jordan_Decomposition/Hahn_Jordan_Decomposition.thy --- a/thys/Hahn_Jordan_Decomposition/Hahn_Jordan_Decomposition.thy +++ b/thys/Hahn_Jordan_Decomposition/Hahn_Jordan_Decomposition.thy @@ -1,2176 +1,2176 @@ section \Signed measures\ text \In this section we define signed measures. These are generalizations of measures that can also take negative values but cannot contain both $\infty$ and $-\infty$ in their range.\ subsection \Basic definitions\ theory Hahn_Jordan_Decomposition imports "HOL-Probability.Probability" Hahn_Jordan_Prelims begin definition signed_measure::"'a measure \ ('a set \ ereal) \ bool" where "signed_measure M \ \ \ {} = 0 \ (-\ \ range \ \ \ \ range \) \ (\A. range A \ sets M \ disjoint_family A \ \ (range A) \ sets M \ (\i. \ (A i)) sums \ (\ (range A))) \ (\A. range A \ sets M \ disjoint_family A \ \ (range A) \ sets M \ \\ (\ (range A))\ < \ \ summable (\i. real_of_ereal \\ (A i)\))" lemma signed_measure_empty: assumes "signed_measure M \" shows "\ {} = 0" using assms unfolding signed_measure_def by simp lemma signed_measure_sums: assumes "signed_measure M \" and "range A \ M" and "disjoint_family A" and "\ (range A) \ sets M" shows "(\i. \ (A i)) sums \ (\ (range A))" using assms unfolding signed_measure_def by simp lemma signed_measure_summable: assumes "signed_measure M \" and "range A \ M" and "disjoint_family A" and "\ (range A) \ sets M" and "\\ (\ (range A))\ < \" shows "summable (\i. real_of_ereal \\ (A i)\)" using assms unfolding signed_measure_def by simp lemma signed_measure_inf_sum: assumes "signed_measure M \" and "range A \ M" and "disjoint_family A" and "\ (range A) \ sets M" shows "(\i. \ (A i)) = \ (\ (range A))" using sums_unique assms signed_measure_sums by (metis) lemma signed_measure_abs_convergent: assumes "signed_measure M \" and "range A \ sets M" and "disjoint_family A" and "\ (range A) \ sets M" and "\\ (\ (range A))\ < \" shows "summable (\i. real_of_ereal \\ (A i)\)" using assms unfolding signed_measure_def by simp lemma signed_measure_additive: assumes "signed_measure M \" shows "additive M \" proof (auto simp add: additive_def) fix x y assume x: "x \ M" and y: "y \ M" and "x \ y = {}" hence "disjoint_family (binaryset x y)" by (auto simp add: disjoint_family_on_def binaryset_def) have "(\i. \ ((binaryset x y) i)) sums (\ x + \ y)" using binaryset_sums signed_measure_empty[of M \] assms by simp have "range (binaryset x y) = {x, y, {}}" using range_binaryset_eq by simp moreover have "{x, y, {}} \ M" using x y by auto moreover have "x\y \ sets M" using x y by simp moreover have "(\ (range (binaryset x y))) = x\ y" by (simp add: calculation(1)) ultimately have "(\i. \ ((binaryset x y) i)) sums \ (x \ y)" using assms x y signed_measure_empty[of M \] signed_measure_sums[of M \] \disjoint_family (binaryset x y)\ by (metis) then show "\ (x \ y) = \ x + \ y" using \(\i. \ ((binaryset x y) i)) sums (\ x + \ y)\ sums_unique2 by force qed lemma signed_measure_add: assumes "signed_measure M \" and "a\ sets M" and "b\ sets M" and "a\ b = {}" shows "\ (a\ b) = \ a + \ b" using additiveD[OF signed_measure_additive] assms by auto lemma signed_measure_disj_sum: shows "finite I \ signed_measure M \ \ disjoint_family_on A I \ (\i. i \ I \ A i \ sets M) \ \ (\ i\ I. A i) = (\ i\ I. \ (A i))" proof (induct rule:finite_induct) case empty then show ?case unfolding signed_measure_def by simp next case (insert x F) have "\ (\ (A ` insert x F)) = \ ((\ (A `F)) \ A x)" by (simp add: Un_commute) also have "... = \ (\ (A `F)) + \ (A x)" proof - have "(\ (A `F)) \ (A x) = {}" using insert by (metis disjoint_family_on_insert inf_commute) moreover have "\ (A `F) \ sets M" using insert by auto moreover have "A x \ sets M" using insert by simp ultimately show ?thesis by (meson insert.prems(1) signed_measure_add) qed also have "... = (\ i\ F. \ (A i)) + \ (A x)" using insert by (metis disjoint_family_on_insert insert_iff) also have "... = (\i\insert x F. \ (A i))" by (simp add: add.commute insert.hyps(1) insert.hyps(2)) finally show ?case . qed lemma pos_signed_measure_count_additive: assumes "signed_measure M \" and "\ E \ sets M. 0 \ \ E" shows "countably_additive (sets M) (\A. e2ennreal (\ A))" unfolding countably_additive_def proof (intro allI impI) fix A::"nat \ 'a set" assume "range A \ sets M" and "disjoint_family A" and "\ (range A) \ sets M" note Aprops = this have eq: "\i. \ (A i) = enn2ereal (e2ennreal (\ (A i)))" using assms enn2ereal_e2ennreal Aprops by simp have "(\n. \i\n. \ (A i)) \ \ (\ (range A))" using sums_def_le[of "\i. \ (A i)" "\ (\ (range A))"] assms signed_measure_sums[of M] Aprops by simp hence "((\n. e2ennreal (\i\n. \ (A i))) \ e2ennreal (\ (\ (range A)))) sequentially" using tendsto_e2ennrealI[of "(\n. \i\n. \ (A i))" "\ (\ (range A))"] by simp moreover have "\n. e2ennreal (\i\n. \ (A i)) = (\i\n. e2ennreal (\ (A i)))" using e2ennreal_finite_sum by (metis enn2ereal_nonneg eq finite_atMost) ultimately have "((\n. (\i\n. e2ennreal (\ (A i)))) \ e2ennreal (\ (\ (range A)))) sequentially" by simp hence "(\i. e2ennreal (\ (A i))) sums e2ennreal (\ (\ (range A)))" using sums_def_le[of "\i. e2ennreal (\ (A i))" "e2ennreal (\ (\ (range A)))"] by simp thus "(\i. e2ennreal (\ (A i))) = e2ennreal (\ (\ (range A)))" using sums_unique assms by (metis) qed lemma signed_measure_minus: assumes "signed_measure M \" shows "signed_measure M (\A. - \ A)" unfolding signed_measure_def proof (intro conjI) show "- \ {} = 0" using assms unfolding signed_measure_def by simp show "- \ \ range (\A. - \ A) \ \ \ range (\A. - \ A)" proof (cases "\ \ range \") case True hence "-\ \ range \" using assms unfolding signed_measure_def by simp hence "\ \ range (\A. - \ A)" using ereal_uminus_eq_reorder by blast thus "- \ \ range (\A. - \ A) \ \ \ range (\A. - \ A)" by simp next case False hence "-\ \ range (\A. - \ A)" using ereal_uminus_eq_reorder by (simp add: image_iff) thus "- \ \ range (\A. - \ A) \ \ \ range (\A. - \ A)" by simp qed show "\A. range A \ sets M \ disjoint_family A \ \ (range A) \ sets M \ \- \ (\ (range A))\ < \ \ summable (\i. real_of_ereal \- \ (A i)\)" proof (intro allI impI) fix A::"nat \ 'a set" assume "range A \ sets M" and "disjoint_family A" and "\ (range A) \ sets M" and "\- \ (\ (range A))\ < \" thus "summable (\i. real_of_ereal \- \ (A i)\)" using assms unfolding signed_measure_def by simp qed show "\A. range A \ sets M \ disjoint_family A \ \ (range A) \ sets M \ (\i. - \ (A i)) sums - \ (\ (range A))" proof - { fix A::"nat \ 'a set" assume "range A \ sets M" and "disjoint_family A" and "\ (range A) \ sets M" note Aprops = this have "- \ \ range (\i. \ (A i)) \ \ \ range (\i. \ (A i))" proof - have "range (\i. \ (A i)) \ range \" by auto thus ?thesis using assms unfolding signed_measure_def by auto qed moreover have "(\i. \ (A i)) sums \ (\ (range A))" using signed_measure_sums[of M] Aprops assms by simp ultimately have "(\i. - \ (A i)) sums - \ (\ (range A))" using sums_minus'[of "\i. \ (A i)"] by simp } thus ?thesis by auto qed qed locale near_finite_function = fixes \:: "'b set \ ereal" assumes inf_range: "- \ \ range \ \ \ \ range \" lemma (in near_finite_function) finite_subset: assumes "\\ E\ < \" and "A\ E" and "\ E = \ A + \ (E - A)" shows "\\ A\ < \" proof (cases "\ \ range \") case False show ?thesis proof (cases "0 < \ A") case True hence "\\ A\ = \ A" by simp also have "... < \" using False by (metis ereal_less_PInfty rangeI) finally show ?thesis . next case False hence "\\ A\ = -\ A" using not_less_iff_gr_or_eq by fastforce also have "... = \ (E - A) - \ E" proof - have "\ E = \ A + \ (E - A)" using assms by simp hence "\ E - \ A = \ (E - A)" by (metis abs_ereal_uminus assms(1) calculation ereal_diff_add_inverse ereal_infty_less(2) ereal_minus(5) ereal_minus_less_iff ereal_minus_less_minus ereal_uminus_uminus less_ereal.simps(2) minus_ereal_def plus_ereal.simps(3)) thus ?thesis using assms(1) ereal_add_uminus_conv_diff ereal_eq_minus by auto qed also have "... \ \ (E - A) + \\ E\" by (metis \- \ A = \ (E - A) - \ E\ abs_ereal_less0 abs_ereal_pos ereal_diff_le_self ereal_le_add_mono1 less_eq_ereal_def minus_ereal_def not_le_imp_less) also have "... < \" using assms \\ \ range \\ by (metis UNIV_I ereal_less_PInfty ereal_plus_eq_PInfty image_eqI) finally show ?thesis . qed next case True hence "-\ \ range \" using inf_range by simp hence "-\ < \ A" by (metis ereal_infty_less(2) rangeI) show ?thesis proof (cases "\ A < 0") case True hence "\\ A\ = -\ A" using not_less_iff_gr_or_eq by fastforce also have "... < \" using \-\ < \ A\ using ereal_uminus_less_reorder by blast finally show ?thesis . next case False hence "\\ A\ = \ A" by simp also have "... = \ E - \ (E - A)" proof - have "\ E = \ A + \ (E - A)" using assms by simp thus "\ A = \ E - \ (E - A)" by (metis add.right_neutral assms(1) add_diff_eq_ereal calculation ereal_diff_add_eq_diff_diff_swap ereal_diff_add_inverse ereal_infty_less(1) ereal_plus_eq_PInfty ereal_x_minus_x) qed also have "... \ \\ E\ - \ (E - A)" by (metis \\\ A\ = \ A\ \\ A = \ E - \ (E - A)\ abs_ereal_ge0 abs_ereal_pos abs_ereal_uminus antisym_conv ereal_0_le_uminus_iff ereal_abs_diff ereal_diff_le_mono_left ereal_diff_le_self le_cases less_eq_ereal_def minus_ereal_def) also have "... < \" proof - have "-\ < \ (E - A)" using \-\ \ range \\ by (metis ereal_infty_less(2) rangeI) hence "- \ (E - A) < \" using ereal_uminus_less_reorder by blast thus ?thesis using assms by (simp add: ereal_minus_eq_PInfty_iff ereal_uminus_eq_reorder) qed finally show ?thesis . qed qed locale signed_measure_space= fixes M::"'a measure" and \ assumes sgn_meas: "signed_measure M \" sublocale signed_measure_space \ near_finite_function proof (unfold_locales) show "- \ \ range \ \ \ \ range \" using sgn_meas unfolding signed_measure_def by simp qed context signed_measure_space begin lemma signed_measure_finite_subset: assumes "E \ sets M" and "\\ E\ < \" and "A\ sets M" and "A\ E" shows "\\ A\ < \" proof (rule finite_subset) show "\\ E\ < \" "A\ E" using assms by auto show "\ E = \ A + \ (E - A)" using assms sgn_meas signed_measure_add[of M \ A "E - A"] by (metis Diff_disjoint Diff_partition sets.Diff) qed lemma measure_space_e2ennreal : assumes "measure_space (space M) (sets M) m \ (\E \ sets M. m E < \) \ (\E \ sets M. m E \ 0)" shows "\E \ sets M. e2ennreal (m E) < \" proof fix E assume "E \ sets M" show "e2ennreal (m E) < \" proof - have "m E < \" using assms \E \ sets M\ by blast then have "e2ennreal (m E) < \" using e2ennreal_less_top using \m E < \\ by auto thus ?thesis by simp qed qed subsection \Positive and negative subsets\ text \The Hahn decomposition theorem is based on the notions of positive and negative measurable sets. A measurable set is positive (resp. negative) if all its measurable subsets have a positive (resp. negative) measure by $\mu$. The decomposition theorem states that any measure space for a signed measure can be decomposed into a positive and a negative measurable set.\ definition pos_meas_set where "pos_meas_set E \ E \ sets M \ (\A \ sets M. A \ E \ 0 \ \ A)" definition neg_meas_set where "neg_meas_set E \ E \ sets M \ (\A \ sets M. A \ E \ \ A \ 0)" lemma pos_meas_setI: assumes "E \ sets M" and "\A. A \ sets M \ A \ E \ 0 \ \ A" shows "pos_meas_set E" unfolding pos_meas_set_def using assms by simp lemma pos_meas_setD1 : assumes "pos_meas_set E" shows "E \ sets M" using assms unfolding pos_meas_set_def by simp lemma neg_meas_setD1 : assumes "neg_meas_set E" shows "E \ sets M" using assms unfolding neg_meas_set_def by simp lemma neg_meas_setI: assumes "E \ sets M" and "\A. A \ sets M \ A \ E \ \ A \ 0" shows "neg_meas_set E" unfolding neg_meas_set_def using assms by simp lemma pos_meas_self: assumes "pos_meas_set E" shows "0 \ \ E" using assms unfolding pos_meas_set_def by simp lemma empty_pos_meas_set: shows "pos_meas_set {}" by (metis bot.extremum_uniqueI eq_iff pos_meas_set_def sets.empty_sets sgn_meas signed_measure_empty) lemma empty_neg_meas_set: shows "neg_meas_set {}" by (metis neg_meas_set_def order_refl sets.empty_sets sgn_meas signed_measure_empty subset_empty) lemma pos_measure_meas: assumes "pos_meas_set E" and "A\ E" and "A\ sets M" shows "0 \ \ A" using assms unfolding pos_meas_set_def by simp lemma pos_meas_subset: assumes "pos_meas_set A" and "B\ A" and "B\ sets M" shows "pos_meas_set B" using assms pos_meas_set_def by auto lemma neg_meas_subset: assumes "neg_meas_set A" and "B\ A" and "B\ sets M" shows "neg_meas_set B" using assms neg_meas_set_def by auto lemma pos_meas_set_Union: assumes "\(i::nat). pos_meas_set (A i)" and "\i. A i \ sets M" and "\\ (\ i. A i)\ < \" shows "pos_meas_set (\ i. A i)" proof (rule pos_meas_setI) show "\ (range A) \ sets M" using sigma_algebra.countable_UN assms by simp obtain B where "disjoint_family B" and "(\(i::nat). B i) = (\(i::nat). A i)" and "\i. B i \ sets M" and "\i. B i \ A i" using disj_Union2 assms by auto fix C assume "C \ sets M" and "C\ (\ i. A i)" hence "C = C \ (\ i. A i)" by auto also have "... = C \ (\ i. B i)" using \(\i. B i) = (\i. A i)\ by simp also have "... = (\ i. C \ B i)" by auto finally have "C = (\ i. C \ B i)" . hence "\ C = \ (\ i. C \ B i)" by simp also have "... = (\i. \ (C \ (B i)))" proof (rule signed_measure_inf_sum[symmetric]) show "signed_measure M \" using sgn_meas by simp show "disjoint_family (\i. C \ B i)" using \disjoint_family B\ by (meson Int_iff disjoint_family_subset subset_iff) show "range (\i. C \ B i) \ sets M" using \C\ sets M\ \\i. B i \ sets M\ by auto show "(\i. C \ B i) \ sets M" using \C = (\ i. C \ B i)\ \C\ sets M\ by simp qed also have "... \ 0" proof (rule suminf_nonneg) show "\n. 0 \ \ (C \ B n)" proof - fix n have "C\ B n \ A n" using \\i. B i \ A i\ by auto moreover have "C \ B n \ sets M" using \C\ sets M\ \\i. B i \ sets M\ by simp ultimately show "0 \ \ (C \ B n)" using assms pos_measure_meas[of "A n"] by simp qed have "summable (\i. real_of_ereal (\ (C \ B i)))" proof (rule summable_norm_cancel) have "\n. norm (real_of_ereal (\ (C \ B n))) = real_of_ereal \\ (C \ B n)\" by simp moreover have "summable (\i. real_of_ereal \\ (C \ B i)\)" proof (rule signed_measure_abs_convergent) show "signed_measure M \" using sgn_meas by simp show "range (\i. C \ B i) \ sets M" using \C\ sets M\ \\i. B i \ sets M\ by auto show "disjoint_family (\i. C \ B i)" using \disjoint_family B\ by (meson Int_iff disjoint_family_subset subset_iff) show "(\i. C \ B i) \ sets M" using \C = (\ i. C \ B i)\ \C\ sets M\ by simp have "\\ C\ < \" proof (rule signed_measure_finite_subset) show "(\ i. A i) \ sets M" using assms by simp show "\\ (\ (range A))\ < \" using assms by simp show "C \ sets M" using \C \ sets M\ . show "C \ \ (range A)" using \C \ \ (range A) \ . qed thus "\\ (\i. C \ B i)\ < \" using \C = (\ i. C \ B i)\ by simp qed ultimately show "summable (\n. norm (real_of_ereal (\ (C \ B n))))" by auto qed thus "summable (\i. \ (C \ B i))" by (simp add: \\n. 0 \ \ (C \ B n)\ summable_ereal_pos) qed finally show "0 \ \ C" . qed lemma pos_meas_set_pos_lim: assumes "\(i::nat). pos_meas_set (A i)" and "\i. A i \ sets M" shows "0 \ \ (\ i. A i)" proof - obtain B where "disjoint_family B" and "(\(i::nat). B i) = (\(i::nat). A i)" and "\i. B i \ sets M" and "\i. B i \ A i" using disj_Union2 assms by auto note Bprops = this have sums: "(\n. \ (B n)) sums \ (\i. B i)" proof (rule signed_measure_sums) show "signed_measure M \" using sgn_meas . show "range B \ sets M" using Bprops by auto show "disjoint_family B" using Bprops by simp show "\ (range B) \ sets M" using Bprops by blast qed hence "summable (\n. \ (B n))" using sums_summable[of "\n. \ (B n)"] by simp hence "suminf (\n. \ (B n)) = \ (\i. B i)" using sums sums_iff by auto thus ?thesis using suminf_nonneg by (metis Bprops(2) Bprops(3) Bprops(4) \summable (\n. \ (B n))\ assms(1) pos_measure_meas) qed lemma pos_meas_disj_union: assumes "pos_meas_set A" and "pos_meas_set B" and "A\ B = {}" shows "pos_meas_set (A \ B)" unfolding pos_meas_set_def proof (intro conjI ballI impI) show "A\ B \ sets M" by (metis assms(1) assms(2) pos_meas_set_def sets.Un) next fix C assume "C\ sets M" and "C\ A\ B" define DA where "DA = C\ A" define DB where "DB = C\ B" have "DA\ sets M" using DA_def \C \ sets M\ assms(1) pos_meas_set_def by blast have "DB\ sets M" using DB_def \C \ sets M\ assms(2) pos_meas_set_def by blast have "DA \ DB = {}" unfolding DA_def DB_def using assms by auto have "C = DA \ DB" unfolding DA_def DB_def using \C\ A\ B\ by auto have "0 \ \ DB" using assms unfolding DB_def pos_meas_set_def by (metis DB_def Int_lower2\DB \ sets M\) also have "... \ \ DA + \ DB" using assms unfolding pos_meas_set_def by (metis DA_def Diff_Diff_Int Diff_subset Int_commute \DA \ sets M\ ereal_le_add_self2) also have "... = \ C" using signed_measure_add sgn_meas \DA \ sets M\ \DB \ sets M\ \DA \ DB = {}\ \C = DA \ DB\ by metis finally show "0 \ \ C" . qed lemma pos_meas_set_union: assumes "pos_meas_set A" and "pos_meas_set B" shows "pos_meas_set (A \ B)" proof - define C where "C = B - A" have "A\ C = A\ B" unfolding C_def by auto moreover have "pos_meas_set (A\ C)" proof (rule pos_meas_disj_union) show "pos_meas_set C" unfolding C_def by (meson Diff_subset assms(1) assms(2) sets.Diff signed_measure_space.pos_meas_set_def signed_measure_space.pos_meas_subset signed_measure_space_axioms) show "pos_meas_set A" using assms by simp show "A \ C = {}" unfolding C_def by auto qed ultimately show ?thesis by simp qed lemma neg_meas_disj_union: assumes "neg_meas_set A" and "neg_meas_set B" and "A\ B = {}" shows "neg_meas_set (A \ B)" unfolding neg_meas_set_def proof (intro conjI ballI impI) show "A\ B \ sets M" by (metis assms(1) assms(2) neg_meas_set_def sets.Un) next fix C assume "C\ sets M" and "C\ A\ B" define DA where "DA = C\ A" define DB where "DB = C\ B" have "DA\ sets M" using DA_def \C \ sets M\ assms(1) neg_meas_set_def by blast have "DB\ sets M" using DB_def \C \ sets M\ assms(2) neg_meas_set_def by blast have "DA \ DB = {}" unfolding DA_def DB_def using assms by auto have "C = DA \ DB" unfolding DA_def DB_def using \C\ A\ B\ by auto have "\ C = \ DA + \ DB" using signed_measure_add sgn_meas \DA \ sets M\ \DB \ sets M\ \DA \ DB = {}\ \C = DA \ DB\ by metis also have "... \ \ DB" using assms unfolding neg_meas_set_def by (metis DA_def Int_lower2 \DA \ sets M\ add_decreasing dual_order.refl) also have "... \ 0" using assms unfolding DB_def neg_meas_set_def by (metis DB_def Int_lower2\DB \ sets M\) finally show "\ C \ 0" . qed lemma neg_meas_set_union: assumes "neg_meas_set A" and "neg_meas_set B" shows "neg_meas_set (A \ B)" proof - define C where "C = B - A" have "A\ C = A\ B" unfolding C_def by auto moreover have "neg_meas_set (A\ C)" proof (rule neg_meas_disj_union) show "neg_meas_set C" unfolding C_def by (meson Diff_subset assms(1) assms(2) sets.Diff neg_meas_set_def neg_meas_subset signed_measure_space_axioms) show "neg_meas_set A" using assms by simp show "A \ C = {}" unfolding C_def by auto qed ultimately show ?thesis by simp qed lemma neg_meas_self : assumes "neg_meas_set E" shows "\ E \ 0" using assms unfolding neg_meas_set_def by simp lemma pos_meas_set_opp: assumes "signed_measure_space.pos_meas_set M (\ A. - \ A) A" shows "neg_meas_set A" proof - have m_meas_pos : "signed_measure M (\ A. - \ A)" using assms signed_measure_space_def by (simp add: sgn_meas signed_measure_minus) thus ?thesis by (metis assms ereal_0_le_uminus_iff neg_meas_setI signed_measure_space.intro signed_measure_space.pos_meas_set_def) qed lemma neg_meas_set_opp: assumes "signed_measure_space.neg_meas_set M (\ A. - \ A) A" shows "pos_meas_set A" proof - have m_meas_neg : "signed_measure M (\ A. - \ A)" using assms signed_measure_space_def by (simp add: sgn_meas signed_measure_minus) thus ?thesis by (metis assms ereal_uminus_le_0_iff m_meas_neg pos_meas_setI signed_measure_space.intro signed_measure_space.neg_meas_set_def) qed end lemma signed_measure_inter: assumes "signed_measure M \" and "A \ sets M" shows "signed_measure M (\E. \ (E \ A))" unfolding signed_measure_def proof (intro conjI) show "\ ({} \ A) = 0" using assms(1) signed_measure_empty by auto show "- \ \ range (\E. \ (E \ A)) \ \ \ range (\E. \ (E \ A))" proof (rule ccontr) assume "\ (- \ \ range (\E. \ (E \ A)) \ \ \ range (\E. \ (E \ A)))" hence "- \ \ range (\E. \ (E \ A)) \ \ \ range (\E. \ (E \ A))" by simp hence "- \ \ range \ \ \ \ range \" by auto thus False using assms unfolding signed_measure_def by simp qed show "\E. range E \ sets M \ disjoint_family E \ \ (range E) \ sets M \ (\i. \ (E i \ A)) sums \ (\ (range E) \ A)" proof (intro allI impI) fix E::"nat \ 'a set" assume "range E \ sets M" and "disjoint_family E" and "\ (range E) \ sets M" note Eprops = this define F where "F = (\i. E i \ A)" have "(\i. \ (F i)) sums \ (\ (range F))" proof (rule signed_measure_sums) show "signed_measure M \" using assms by simp show "range F \ sets M" using Eprops F_def assms by blast show "disjoint_family F" using Eprops F_def assms by (metis disjoint_family_subset inf.absorb_iff2 inf_commute inf_right_idem) show "\ (range F) \ sets M" using Eprops assms unfolding F_def by (simp add: Eprops assms countable_Un_Int(1) sets.Int) qed moreover have "\ (range F) = A \ \ (range E)" unfolding F_def by auto ultimately show "(\i. \ (E i \ A)) sums \ (\ (range E) \ A)" unfolding F_def by simp qed show "\E. range E \ sets M \ disjoint_family E \ \ (range E) \ sets M \ \\ (\ (range E) \ A)\ < \ \ summable (\i. real_of_ereal \\ (E i \ A)\)" proof (intro allI impI) fix E::"nat \ 'a set" assume "range E \ sets M" and "disjoint_family E" and "\ (range E) \ sets M" and "\\ (\ (range E) \ A)\ < \" note Eprops = this show "summable (\i. real_of_ereal \\ (E i \ A)\)" proof (rule signed_measure_summable) show "signed_measure M \" using assms by simp show "range (\i. E i \ A) \ sets M" using Eprops assms by blast show "disjoint_family (\i. E i \ A)" using Eprops assms disjoint_family_subset inf.absorb_iff2 inf_commute inf_right_idem by fastforce show "(\i. E i \ A) \ sets M" using Eprops assms by (simp add: Eprops assms countable_Un_Int(1) sets.Int) show "\\ (\i. E i \ A)\ < \" using Eprops by auto qed qed qed context signed_measure_space begin lemma pos_signed_to_meas_space : assumes "pos_meas_set M1" and "m1 = (\A. \ (A \ M1))" shows "measure_space (space M) (sets M) m1" unfolding measure_space_def proof (intro conjI) show "sigma_algebra (space M) (sets M)" by (simp add: sets.sigma_algebra_axioms) show "positive (sets M) m1" using assms unfolding pos_meas_set_def by (metis Sigma_Algebra.positive_def Un_Int_eq(4) e2ennreal_neg neg_meas_self sup_bot_right empty_neg_meas_set) show "countably_additive (sets M) m1" proof (rule pos_signed_measure_count_additive) show "\E\sets M. 0 \ m1 E" by (metis assms inf.cobounded2 pos_meas_set_def sets.Int) show "signed_measure M m1" using assms pos_meas_set_def signed_measure_inter[of M \ M1] sgn_meas by blast qed qed lemma neg_signed_to_meas_space : assumes "neg_meas_set M2" and "m2 = (\A. -\ (A \ M2))" shows "measure_space (space M) (sets M) m2" unfolding measure_space_def proof (intro conjI) show "sigma_algebra (space M) (sets M)" by (simp add: sets.sigma_algebra_axioms) show "positive (sets M) m2" using assms unfolding neg_meas_set_def by (metis Sigma_Algebra.positive_def e2ennreal_neg ereal_uminus_zero inf.absorb_iff2 inf.orderE inf_bot_right neg_meas_self pos_meas_self empty_neg_meas_set empty_pos_meas_set) show "countably_additive (sets M) m2" proof (rule pos_signed_measure_count_additive) show "\E\sets M. 0 \ m2 E" by (metis assms ereal_uminus_eq_reorder ereal_uminus_le_0_iff inf.cobounded2 neg_meas_set_def sets.Int) have "signed_measure M (\A. \ (A \ M2))" using assms neg_meas_set_def signed_measure_inter[of M \ M2] sgn_meas by blast thus "signed_measure M m2" using signed_measure_minus assms by simp qed qed lemma pos_part_meas_nul_neg_set : assumes "pos_meas_set M1" and "neg_meas_set M2" and "m1 = (\A. \ (A \ M1))" and "E \ sets M" and "E \ M2" shows "m1 E = 0" proof - have "m1 E \ 0" using assms unfolding pos_meas_set_def by (simp add: \E \ sets M\ sets.Int) have "\ E \ 0" using \E \ M2\ assms unfolding neg_meas_set_def using \E \ sets M\ by blast then have "m1 E \ 0" using \\ E \ 0\ assms by (metis Int_Un_eq(1) Un_subset_iff \E \ sets M\ \E \ M2\ pos_meas_setD1 sets.Int signed_measure_space.neg_meas_set_def signed_measure_space_axioms) thus "m1 E = 0" using \m1 E \ 0\ \m1 E \ 0\ by auto qed lemma neg_part_meas_nul_pos_set : assumes "pos_meas_set M1" and "neg_meas_set M2" and "m2 = (\A. -\ (A \ M2))" and "E \ sets M" and "E \ M1" shows "m2 E = 0" proof - have "m2 E \ 0" using assms unfolding neg_meas_set_def by (simp add: \E \ sets M\ sets.Int) have "\ E \ 0" using assms unfolding pos_meas_set_def by blast then have "m2 E \ 0" using \\ E \ 0\ assms by (metis \E \ sets M\ \E \ M1\ ereal_0_le_uminus_iff ereal_uminus_uminus inf_sup_ord(1) neg_meas_setD1 pos_meas_set_def pos_meas_subset sets.Int) thus "m2 E = 0" using \m2 E \ 0\ \m2 E \ 0\ by auto qed definition pos_sets where "pos_sets = {A. A \ sets M \ pos_meas_set A}" definition pos_img where "pos_img = {\ A|A. A\ pos_sets}" subsection \Essential uniqueness\ text \In this part, under the assumption that a measure space for a signed measure admits a decomposition into a positive and a negative set, we prove that this decomposition is essentially unique; in other words, that if two such decompositions $(P,N)$ and $(X,Y)$ exist, then any measurable subset of $(P\triangle X) \cup (N \triangle Y)$ has a null measure.\ definition hahn_space_decomp where "hahn_space_decomp M1 M2 \ (pos_meas_set M1) \ (neg_meas_set M2) \ (space M = M1 \ M2) \ (M1 \ M2 = {})" lemma pos_neg_null_set: assumes "pos_meas_set A" and "neg_meas_set A" shows "\ A = 0" using assms pos_meas_self[of A] neg_meas_self[of A] by simp lemma pos_diff_neg_meas_set: assumes "(pos_meas_set M1)" and "(neg_meas_set N2)" and "(space M = N1 \ N2)" and "N1 \ sets M" shows "neg_meas_set ((M1 - N1) \ space M)" using assms neg_meas_subset by (metis Diff_subset_conv Int_lower2 pos_meas_setD1 sets.Diff sets.Int_space_eq2) lemma neg_diff_pos_meas_set: assumes "(neg_meas_set M2)" and "(pos_meas_set N1)" and "(space M = N1 \ N2)" and "N2 \ sets M" shows "pos_meas_set ((M2 - N2) \ space M)" proof - have "(M2 - N2) \ space M \ N1" using assms by auto thus ?thesis using assms pos_meas_subset neg_meas_setD1 by blast qed lemma pos_sym_diff_neg_meas_set: assumes "hahn_space_decomp M1 M2" and "hahn_space_decomp N1 N2" shows "neg_meas_set ((sym_diff M1 N1) \ space M)" using assms unfolding hahn_space_decomp_def by (metis Int_Un_distrib2 neg_meas_set_union pos_meas_setD1 pos_diff_neg_meas_set) lemma neg_sym_diff_pos_meas_set: assumes "hahn_space_decomp M1 M2" and "hahn_space_decomp N1 N2" shows "pos_meas_set ((sym_diff M2 N2) \ space M)" using assms neg_diff_pos_meas_set unfolding hahn_space_decomp_def by (metis (no_types, lifting) Int_Un_distrib2 neg_meas_setD1 pos_meas_set_union) lemma pos_meas_set_diff: assumes "pos_meas_set A" and "B\ sets M" shows "pos_meas_set ((A - B) \ (space M))" using pos_meas_subset by (metis Diff_subset assms(1) assms(2) pos_meas_setD1 sets.Diff sets.Int_space_eq2) lemma pos_meas_set_sym_diff: assumes "pos_meas_set A" and "pos_meas_set B" shows "pos_meas_set ((sym_diff A B) \ space M)" using pos_meas_set_diff by (metis Int_Un_distrib2 assms(1) assms(2) pos_meas_setD1 pos_meas_set_union) lemma neg_meas_set_diff: assumes "neg_meas_set A" and "B\ sets M" shows "neg_meas_set ((A - B) \ (space M))" using neg_meas_subset by (metis Diff_subset assms(1) assms(2) neg_meas_setD1 sets.Diff sets.Int_space_eq2) lemma neg_meas_set_sym_diff: assumes "neg_meas_set A" and "neg_meas_set B" shows "neg_meas_set ((sym_diff A B) \ space M)" using neg_meas_set_diff by (metis Int_Un_distrib2 assms(1) assms(2) neg_meas_setD1 neg_meas_set_union) lemma hahn_decomp_space_diff: assumes "hahn_space_decomp M1 M2" and "hahn_space_decomp N1 N2" shows "pos_meas_set ((sym_diff M1 N1 \ sym_diff M2 N2) \ space M)" "neg_meas_set ((sym_diff M1 N1 \ sym_diff M2 N2) \ space M)" proof - show "pos_meas_set ((sym_diff M1 N1 \ sym_diff M2 N2) \ space M)" by (metis Int_Un_distrib2 assms(1) assms(2) hahn_space_decomp_def neg_sym_diff_pos_meas_set pos_meas_set_sym_diff pos_meas_set_union) show "neg_meas_set ((sym_diff M1 N1 \ sym_diff M2 N2) \ space M)" by (metis Int_Un_distrib2 assms(1) assms(2) hahn_space_decomp_def neg_meas_set_sym_diff neg_meas_set_union pos_sym_diff_neg_meas_set) qed lemma hahn_decomp_ess_unique: assumes "hahn_space_decomp M1 M2" and "hahn_space_decomp N1 N2" and "C \ sym_diff M1 N1 \ sym_diff M2 N2" and "C\ sets M" shows "\ C = 0" proof - have "C\ (sym_diff M1 N1 \ sym_diff M2 N2) \ space M" using assms by (simp add: sets.sets_into_space) thus ?thesis using assms hahn_decomp_space_diff pos_neg_null_set by (meson neg_meas_subset pos_meas_subset) qed section \Existence of a positive subset\ text \The goal of this part is to prove that any measurable set of finite and positive measure must contain a positive subset with a strictly positive measure.\ subsection \A sequence of negative subsets\ definition inf_neg where "inf_neg A = (if (A \ sets M \ pos_meas_set A) then (0::nat) else Inf {n|n. (1::nat) \ n \ (\B \ sets M. B \ A \ \ B < ereal(-1/n))})" lemma inf_neg_ne: assumes "A \ sets M" and "\ pos_meas_set A" shows "{n::nat|n. (1::nat) \ n \ (\B \ sets M. B \ A \ \ B < ereal (-1/n))} \ {}" proof - define N where "N = {n::nat|n. (1::nat) \ n \ (\B \ sets M. B \ A \ \ B < ereal (-1/n))}" have "\B \ sets M. B\ A \ \ B < 0" using assms unfolding pos_meas_set_def by auto from this obtain B where "B\ sets M" and "B\ A" and "\ B < 0" by auto hence "\n::nat. (1::nat) \ n \ \ B < ereal (-1/n)" proof (cases "\ B = -\") case True hence "\ B < -1/(2::nat)" by simp thus ?thesis using numeral_le_real_of_nat_iff one_le_numeral by blast next case False hence "real_of_ereal (\ B) < 0" using \\ B < 0\ by (metis Infty_neq_0(3) ereal_mult_eq_MInfty ereal_zero_mult less_eq_ereal_def less_eq_real_def less_ereal.simps(2) real_of_ereal_eq_0 real_of_ereal_le_0) hence "\n::nat. Suc 0 \ n \ real_of_ereal (\ B) < -1/n" proof - define nw where "nw = Suc (nat (floor (-1/ (real_of_ereal (\ B)))))" have "Suc 0 \ nw" unfolding nw_def by simp have "0 < -1/ (real_of_ereal (\ B))" using \real_of_ereal (\ B) < 0\ by simp have "-1/ (real_of_ereal (\ B)) < nw" unfolding nw_def by linarith hence "1/nw < 1/(-1/ (real_of_ereal (\ B)))" using \0 < -1/ (real_of_ereal (\ B))\ by (metis frac_less2 le_eq_less_or_eq of_nat_1 of_nat_le_iff zero_less_one) also have "... = - (real_of_ereal (\ B))" by simp finally have "1/nw < - (real_of_ereal (\ B))" . hence "real_of_ereal (\ B) < -1/nw" by simp thus ?thesis using \Suc 0 \ nw\ by auto qed from this obtain n1::nat where "Suc 0 \ n1" and "real_of_ereal (\ B) < -1/n1" by auto hence "ereal (real_of_ereal (\ B)) < -1/n1" using real_ereal_leq[of "\ B"] \\ B < 0\ by simp moreover have "\ B = real_of_ereal (\ B)" using \\ B < 0\ False by (metis less_ereal.simps(2) real_of_ereal.elims zero_ereal_def) ultimately show ?thesis using \Suc 0 \ n1\ by auto qed from this obtain n0::nat where "(1::nat) \ n0" and "\ B < -1/n0" by auto hence "n0 \ {n::nat|n. (1::nat) \ n \ (\B \ sets M. B \ A \ \ B < ereal(-1/n))}" using \B\ sets M\ \B\ A\ by auto thus ?thesis by auto qed lemma inf_neg_ge_1: assumes "A \ sets M" and "\ pos_meas_set A" shows "(1::nat) \ inf_neg A" proof - define N where "N = {n::nat|n. (1::nat) \ n \ (\B \ sets M. B \ A \ \ B < ereal (-1/n))}" have "N \ {}" unfolding N_def using assms inf_neg_ne by auto moreover have "\n. n\ N \ (1::nat) \ n" unfolding N_def by simp ultimately show "1 \ inf_neg A" unfolding inf_neg_def N_def using Inf_nat_def1 assms(1) assms(2) by presburger qed lemma inf_neg_pos: assumes "A \ sets M" and "\ pos_meas_set A" shows "\ B \ sets M. B\ A \ \ B < -1/(inf_neg A)" proof - define N where "N = {n::nat|n. (1::nat) \ n \ (\B \ sets M. B \ A \ \ B < ereal (-1/n))}" have "N \ {}" unfolding N_def using assms inf_neg_ne by auto hence "Inf N \ N" using Inf_nat_def1[of N] by simp hence "inf_neg A \ N" unfolding N_def inf_neg_def using assms by auto thus ?thesis unfolding N_def by auto qed definition rep_neg where "rep_neg A = (if (A \ sets M \ pos_meas_set A) then {} else SOME B. B \ sets M \ B \ A \ \ B \ ereal (-1 / (inf_neg A)))" lemma g_rep_neg: assumes "A\ sets M" and "\ pos_meas_set A" shows "rep_neg A \ sets M" "rep_neg A \ A" "\ (rep_neg A) \ ereal (-1 / (inf_neg A))" proof - have "\ B. B \ sets M \ B\ A \ \ B \ -1 / (inf_neg A)" using assms inf_neg_pos[of A] by auto from someI_ex[OF this] show "rep_neg A \ sets M" "rep_neg A \ A" "\ (rep_neg A) \ -1 / (inf_neg A)" unfolding rep_neg_def using assms by auto qed lemma rep_neg_sets: shows "rep_neg A \ sets M" proof (cases "A \ sets M \ pos_meas_set A") case True then show ?thesis unfolding rep_neg_def by simp next case False then show ?thesis using g_rep_neg(1) by blast qed lemma rep_neg_subset: shows "rep_neg A \ A" proof (cases "A \ sets M \ pos_meas_set A") case True then show ?thesis unfolding rep_neg_def by simp next case False then show ?thesis using g_rep_neg(2) by blast qed lemma rep_neg_less: assumes "A\ sets M" and "\ pos_meas_set A" shows "\ (rep_neg A) \ ereal (-1 / (inf_neg A))" using assms g_rep_neg(3) by simp lemma rep_neg_leq: shows "\ (rep_neg A) \ 0" proof (cases "A \ sets M \ pos_meas_set A") case True hence "rep_neg A = {}" unfolding rep_neg_def by simp then show ?thesis using sgn_meas signed_measure_empty by force next case False then show ?thesis using rep_neg_less by (metis le_ereal_le minus_divide_left neg_le_0_iff_le of_nat_0 of_nat_le_iff zero_ereal_def zero_le zero_le_divide_1_iff) qed subsection \Construction of the positive subset\ fun pos_wtn where pos_wtn_base: "pos_wtn E 0 = E"| pos_wtn_step: "pos_wtn E (Suc n) = pos_wtn E n - rep_neg (pos_wtn E n)" lemma pos_wtn_subset: shows "pos_wtn E n \ E" proof (induct n) case 0 then show ?case using pos_wtn_base by simp next case (Suc n) hence "rep_neg (pos_wtn E n) \ pos_wtn E n" using rep_neg_subset by simp then show ?case using Suc by auto qed lemma pos_wtn_sets: assumes "E\ sets M" shows "pos_wtn E n \ sets M" proof (induct n) case 0 then show ?case using assms by simp next case (Suc n) then show ?case using pos_wtn_step rep_neg_sets by auto qed definition neg_wtn where "neg_wtn E (n::nat) = rep_neg (pos_wtn E n)" lemma neg_wtn_neg_meas: shows "\ (neg_wtn E n) \ 0" unfolding neg_wtn_def using rep_neg_leq by simp lemma neg_wtn_sets: shows "neg_wtn E n \ sets M" unfolding neg_wtn_def using rep_neg_sets by simp lemma neg_wtn_subset: shows "neg_wtn E n \ E" unfolding neg_wtn_def using pos_wtn_subset[of E n] rep_neg_subset[of "pos_wtn E n"] by simp lemma neg_wtn_union_subset: shows "(\ i \ n. neg_wtn E i) \ E" using neg_wtn_subset by auto lemma pos_wtn_Suc: shows "pos_wtn E (Suc n) = E - (\ i \ n. neg_wtn E i)" unfolding neg_wtn_def proof (induct n) case 0 then show ?case using pos_wtn_base pos_wtn_step by simp next case (Suc n) have "pos_wtn E (Suc (Suc n)) = pos_wtn E (Suc n) - rep_neg (pos_wtn E (Suc n))" using pos_wtn_step by simp also have "... = (E - (\ i \ n. rep_neg (pos_wtn E i))) - rep_neg (pos_wtn E (Suc n))" using Suc by simp also have "... = E - (\ i \ (Suc n). rep_neg (pos_wtn E i))" using diff_union[of E "\i. rep_neg (pos_wtn E i)" n] by auto finally show "pos_wtn E (Suc (Suc n)) = E - (\ i \ (Suc n). rep_neg (pos_wtn E i))" . qed definition pos_sub where "pos_sub E = (\ n. pos_wtn E n)" lemma pos_sub_sets: assumes "E\ sets M" shows "pos_sub E \ sets M" unfolding pos_sub_def using pos_wtn_sets assms by auto lemma pos_sub_subset: shows "pos_sub E \ E" unfolding pos_sub_def using pos_wtn_subset by blast lemma pos_sub_infty: assumes "E \ sets M" and "\\ E\ < \" shows "\\ (pos_sub E)\ < \" using signed_measure_finite_subset assms pos_sub_sets pos_sub_subset by simp lemma neg_wtn_djn: shows "disjoint_family (\n. neg_wtn E n)" unfolding disjoint_family_on_def proof - { fix n fix m::nat assume "n < m" hence "\p. m = Suc p" using old.nat.exhaust by auto from this obtain p where "m = Suc p" by auto have "neg_wtn E m \ pos_wtn E m" unfolding neg_wtn_def by (simp add: rep_neg_subset) also have "... = E - (\ i \ p. neg_wtn E i)" using pos_wtn_Suc \m = Suc p\ by simp finally have "neg_wtn E m \ E - (\ i \ p. neg_wtn E i)" . moreover have "neg_wtn E n \ (\ i \ p. neg_wtn E i)" using \n < m\ \m = Suc p\ by (simp add: UN_upper) ultimately have "neg_wtn E n \ neg_wtn E m = {}" by auto } thus "\m\UNIV. \n\UNIV. m \ n \ neg_wtn E m \ neg_wtn E n = {}" by (metis inf_commute linorder_neqE_nat) qed end lemma disjoint_family_imp_on: assumes "disjoint_family A" shows "disjoint_family_on A S" using assms disjoint_family_on_mono subset_UNIV by blast context signed_measure_space begin lemma neg_wtn_union_neg_meas: shows "\ (\ i \ n. neg_wtn E i) \ 0" proof - have "\ (\ i \ n. neg_wtn E i) = (\i\{.. n}. \ (neg_wtn E i))" proof (rule signed_measure_disj_sum, simp+) show "signed_measure M \" using sgn_meas . show "disjoint_family_on (neg_wtn E) {..n}" using neg_wtn_djn disjoint_family_imp_on[of "neg_wtn E"] by simp show "\i. i \ {..n} \ neg_wtn E i \ sets M" using neg_wtn_sets by simp qed also have "... \ 0" using neg_wtn_neg_meas by (simp add: sum_nonpos) finally show ?thesis . qed lemma pos_wtn_meas_gt: assumes "0 < \ E" and "E\ sets M" shows "0 < \ (pos_wtn E n)" proof (cases "n = 0") case True then show ?thesis using assms by simp next case False hence "\m. n = Suc m" by (simp add: not0_implies_Suc) from this obtain m where "n = Suc m" by auto hence eq: "pos_wtn E n = E - (\ i \ m. neg_wtn E i)" using pos_wtn_Suc by simp hence "pos_wtn E n \ (\ i \ m. neg_wtn E i) = {}" by auto moreover have "E = pos_wtn E n \ (\ i \ m. neg_wtn E i)" using eq neg_wtn_union_subset[of E m] by auto ultimately have "\ E = \ (pos_wtn E n) + \ (\ i \ m. neg_wtn E i)" using signed_measure_add[of M \ "pos_wtn E n" "\ i \ m. neg_wtn E i"] pos_wtn_sets neg_wtn_sets assms sgn_meas by auto hence "0 < \ (pos_wtn E n) + \ (\ i \ m. neg_wtn E i)" using assms by simp thus ?thesis using neg_wtn_union_neg_meas by (metis add.right_neutral add_mono not_le) qed definition union_wit where "union_wit E = (\ n. neg_wtn E n)" lemma union_wit_sets: shows "union_wit E \ sets M" unfolding union_wit_def proof (intro sigma_algebra.countable_nat_UN) show "sigma_algebra (space M) (sets M)" by (simp add: sets.sigma_algebra_axioms) show "range (neg_wtn E) \ sets M" proof - { fix n have "neg_wtn E n \ sets M" unfolding neg_wtn_def by (simp add: rep_neg_sets) } thus ?thesis by auto qed qed lemma union_wit_subset: shows "union_wit E \ E" proof - { fix n have "neg_wtn E n \ E" unfolding neg_wtn_def using pos_wtn_subset rep_neg_subset[of "pos_wtn E n"] by auto } thus ?thesis unfolding union_wit_def by auto qed lemma pos_sub_diff: shows "pos_sub E = E - union_wit E" proof show "pos_sub E \ E - union_wit E" proof - have "pos_sub E \ E" using pos_sub_subset by simp moreover have "pos_sub E \ union_wit E = {}" proof (rule ccontr) assume "pos_sub E \ union_wit E \ {}" hence "\ a. a\ pos_sub E \ union_wit E" by auto from this obtain a where "a\ pos_sub E \ union_wit E" by auto hence "a\ union_wit E" by simp hence "\n. a \ rep_neg (pos_wtn E n)" unfolding union_wit_def neg_wtn_def by auto from this obtain n where "a \ rep_neg (pos_wtn E n)" by auto have "a \ pos_wtn E (Suc n)" using \a\ pos_sub E \ union_wit E\ unfolding pos_sub_def by blast hence "a\ rep_neg (pos_wtn E n)" using pos_wtn_step by simp thus False using \a \ rep_neg (pos_wtn E n)\ by simp qed ultimately show ?thesis by auto qed next show "E - union_wit E \ pos_sub E" proof fix a assume "a \ E - union_wit E" show "a \ pos_sub E" unfolding pos_sub_def proof fix n show "a \ pos_wtn E n" proof (cases "n = 0") case True thus ?thesis using pos_wtn_base \a\ E - union_wit E\ by simp next case False hence "\m. n = Suc m" by (simp add: not0_implies_Suc) from this obtain m where "n = Suc m" by auto have "(\ i \ m. rep_neg (pos_wtn E i)) \ (\ n. (rep_neg (pos_wtn E n)))" by auto hence "a \ E - (\ i \ m. rep_neg (pos_wtn E i))" using \a \ E - union_wit E\ unfolding union_wit_def neg_wtn_def by auto thus "a\ pos_wtn E n" using pos_wtn_Suc \n = Suc m\ unfolding neg_wtn_def by simp qed qed qed qed definition num_wtn where "num_wtn E n = inf_neg (pos_wtn E n)" lemma num_wtn_geq: shows "\ (neg_wtn E n) \ ereal (-1/(num_wtn E n))" proof (cases "(pos_wtn E n) \ sets M \ pos_meas_set (pos_wtn E n)") case True hence "neg_wtn E n = {}" unfolding neg_wtn_def rep_neg_def by simp moreover have "num_wtn E n = 0" using True unfolding num_wtn_def inf_neg_def by simp ultimately show ?thesis using sgn_meas signed_measure_empty by force next case False then show ?thesis using g_rep_neg(3)[of "pos_wtn E n"] unfolding neg_wtn_def num_wtn_def by simp qed lemma neg_wtn_infty: assumes "E \ sets M" and "\\ E\ < \" shows "\\ (neg_wtn E i)\ < \" proof (rule signed_measure_finite_subset) show "E \ sets M" "\\ E\ < \" using assms by auto show "neg_wtn E i \ sets M" proof (cases "pos_wtn E i \ sets M \ pos_meas_set (pos_wtn E i)") case True then show ?thesis unfolding neg_wtn_def rep_neg_def by simp next case False then show ?thesis unfolding neg_wtn_def using g_rep_neg(1)[of "pos_wtn E i"] by simp qed show "neg_wtn E i \ E" unfolding neg_wtn_def using pos_wtn_subset[of E] rep_neg_subset[of "pos_wtn E i"] by auto qed lemma union_wit_infty: assumes "E \ sets M" and "\\ E\ < \" shows "\\ (union_wit E)\ < \" using union_wit_subset union_wit_sets signed_measure_finite_subset assms unfolding union_wit_def by simp lemma neg_wtn_summable: assumes "E \ sets M" and "\\ E\ < \" shows "summable (\i. - real_of_ereal (\ (neg_wtn E i)))" proof - have "signed_measure M \" using sgn_meas . moreover have "range (neg_wtn E) \ sets M" unfolding neg_wtn_def using rep_neg_sets by auto moreover have "disjoint_family (neg_wtn E)" using neg_wtn_djn by simp moreover have "\ (range (neg_wtn E)) \ sets M" using union_wit_sets unfolding union_wit_def by simp moreover have "\\ (\ (range (neg_wtn E)))\ < \" using union_wit_subset signed_measure_finite_subset union_wit_sets assms unfolding union_wit_def by simp ultimately have "summable (\i. real_of_ereal \\ (neg_wtn E i)\)" using signed_measure_abs_convergent[of M ] by simp moreover have "\i. \\ (neg_wtn E i)\ = -(\ (neg_wtn E i))" proof - fix i have "\ (neg_wtn E i) \ 0" using rep_neg_leq[of "pos_wtn E i"] unfolding neg_wtn_def . thus "\\ (neg_wtn E i)\ = -\ (neg_wtn E i)" using less_eq_ereal_def by auto qed ultimately show ?thesis by simp qed lemma inv_num_wtn_summable: assumes "E \ sets M" and "\\ E\ < \" shows "summable (\n. 1/(num_wtn E n))" proof (rule summable_bounded) show "\i. 0 \ 1 / real (num_wtn E i)" by simp show "\i. 1 / real (num_wtn E i) \ (\n. -real_of_ereal (\ (neg_wtn E n))) i" proof - fix i have "\\ (neg_wtn E i)\ < \" using assms neg_wtn_infty by simp have "ereal (1/(num_wtn E i)) \ -\ (neg_wtn E i)" using num_wtn_geq[of E i] ereal_minus_le_minus by fastforce also have "... = ereal(- real_of_ereal (\ (neg_wtn E i)))" using \\\ (neg_wtn E i)\ < \\ ereal_real' by auto finally have "ereal (1/(num_wtn E i)) \ ereal(- real_of_ereal (\ (neg_wtn E i)))" . thus "1 / real (num_wtn E i) \ -real_of_ereal (\ (neg_wtn E i))" by simp qed show "summable (\i. - real_of_ereal (\ (neg_wtn E i)))" using assms neg_wtn_summable by simp qed lemma inv_num_wtn_shift_summable: assumes "E \ sets M" and "\\ E\ < \" shows "summable (\n. 1/(num_wtn E n - 1))" proof (rule sum_shift_denum) show "summable (\n. 1 / real (num_wtn E n))" using assms inv_num_wtn_summable by simp qed lemma neg_wtn_meas_sums: assumes "E \ sets M" and "\\ E\ < \" shows "(\i. - (\ (neg_wtn E i))) sums suminf (\i. - real_of_ereal (\ (neg_wtn E i)))" proof - have "(\i. ereal (- real_of_ereal (\ (neg_wtn E i)))) sums suminf (\i. - real_of_ereal (\ (neg_wtn E i)))" proof (rule sums_ereal[THEN iffD2]) have "summable (\i. - real_of_ereal (\ (neg_wtn E i)))" using neg_wtn_summable assms by simp thus "(\x. - real_of_ereal (\ (neg_wtn E x))) sums (\i. - real_of_ereal (\ (neg_wtn E i)))" by auto qed moreover have "\i. \ (neg_wtn E i) = ereal (real_of_ereal (\ (neg_wtn E i)))" proof - fix i show "\ (neg_wtn E i) = ereal (real_of_ereal (\ (neg_wtn E i)))" using assms(1) assms(2) ereal_real' neg_wtn_infty by auto qed ultimately show ?thesis by (metis (no_types, lifting) sums_cong uminus_ereal.simps(1)) qed lemma neg_wtn_meas_suminf_le: assumes "E \ sets M" and "\\ E\ < \" shows "suminf (\i. \ (neg_wtn E i)) \ - suminf (\n. 1/(num_wtn E n))" proof - have "suminf (\n. 1/(num_wtn E n)) \ suminf (\i. -real_of_ereal (\ (neg_wtn E i)))" proof (rule suminf_le) show "summable (\n. 1 / real (num_wtn E n))" using assms inv_num_wtn_summable[of E] summable_minus[of "\n. 1 / real (num_wtn E n)"] by simp show "summable (\i. -real_of_ereal (\ (neg_wtn E i)))" using neg_wtn_summable assms summable_minus[of "\i. real_of_ereal (\ (neg_wtn E i))"] by (simp add: summable_minus_iff) show "\n. 1 / real (num_wtn E n) \ -real_of_ereal (\ (neg_wtn E n))" proof - fix n have "\ (neg_wtn E n) \ ereal (- 1 / real (num_wtn E n))" using num_wtn_geq by simp hence "ereal (1/ real (num_wtn E n)) \ - \ (neg_wtn E n)" by (metis add.inverse_inverse eq_iff ereal_uminus_le_reorder linear minus_divide_left uminus_ereal.simps(1)) have "real_of_ereal (ereal (1 / real (num_wtn E n))) \ real_of_ereal (- \ (neg_wtn E n))" proof (rule real_of_ereal_positive_mono) show "0 \ ereal (1 / real (num_wtn E n))" by simp show "ereal (1 / real (num_wtn E n)) \ - \ (neg_wtn E n)" using \ereal (1 / real (num_wtn E n)) \ - \ (neg_wtn E n)\ . show "- \ (neg_wtn E n) \ \" using neg_wtn_infty[of E n] assms by auto qed thus "(1 / real (num_wtn E n)) \ -real_of_ereal ( \ (neg_wtn E n))" by simp qed qed also have "... = - suminf (\i. real_of_ereal (\ (neg_wtn E i)))" proof (rule suminf_minus) show "summable (\n. real_of_ereal (\ (neg_wtn E n)))" using neg_wtn_summable assms summable_minus[of "\i. real_of_ereal (\ (neg_wtn E i))"] by (simp add: summable_minus_iff) qed finally have "suminf (\n. 1/(num_wtn E n)) \ - suminf (\i. real_of_ereal (\ (neg_wtn E i)))" . hence a: "suminf (\i. real_of_ereal (\ (neg_wtn E i))) \ - suminf (\n. 1/(num_wtn E n))" by simp show "suminf (\i. (\ (neg_wtn E i))) \ ereal (-suminf (\n. 1/(num_wtn E n)))" proof - have sumeq: "suminf (\i. ereal (real_of_ereal (\ (neg_wtn E i)))) = suminf (\i. (real_of_ereal (\ (neg_wtn E i))))" proof (rule sums_suminf_ereal) have "summable (\i. -real_of_ereal (\ (neg_wtn E i)))" using neg_wtn_summable assms summable_minus[of "\i. real_of_ereal (\ (neg_wtn E i))"] by (simp add: summable_minus_iff) thus "(\i. real_of_ereal (\ (neg_wtn E i))) sums (\i. real_of_ereal (\ (neg_wtn E i)))" using neg_wtn_summable[of E] assms summable_minus_iff by blast qed hence "suminf (\i. \ (neg_wtn E i)) = suminf (\i. (real_of_ereal (\ (neg_wtn E i))))" proof - have "\i. ereal (real_of_ereal (\ (neg_wtn E i))) = \ (neg_wtn E i)" proof - fix i show "ereal (real_of_ereal (\ (neg_wtn E i))) = \ (neg_wtn E i)" using neg_wtn_infty[of E] assms by (simp add: ereal_real') qed thus ?thesis using sumeq by auto qed thus ?thesis using a by simp qed qed lemma union_wit_meas_le: assumes "E \ sets M" and "\\ E\ < \" shows "\ (union_wit E) \ - suminf (\n. 1 / real (num_wtn E n))" proof - have "\ (union_wit E) = \ (\ (range (neg_wtn E)))" unfolding union_wit_def by simp also have "... = (\i. \ (neg_wtn E i))" proof (rule signed_measure_inf_sum[symmetric]) show "signed_measure M \" using sgn_meas . show "range (neg_wtn E) \ sets M" by (simp add: image_subset_iff neg_wtn_def rep_neg_sets) show "disjoint_family (neg_wtn E)" using neg_wtn_djn by simp show "\ (range (neg_wtn E)) \ sets M" using union_wit_sets unfolding union_wit_def by simp qed also have "... \ - suminf (\n. 1 / real (num_wtn E n))" using assms neg_wtn_meas_suminf_le by simp finally show ?thesis . qed lemma pos_sub_pos_meas: assumes "E \ sets M" and "\\ E\ < \" and "0 < \ E" and "\ pos_meas_set E" shows "0 < \ (pos_sub E)" proof - have "0 < \ E" using assms by simp also have "... = \ (pos_sub E) + \ (union_wit E)" proof - have "E = pos_sub E \ (union_wit E)" using pos_sub_diff[of E] union_wit_subset by force moreover have "pos_sub E \ union_wit E = {}" using pos_sub_diff by auto ultimately show ?thesis using signed_measure_add[of M \ "pos_sub E" "union_wit E"] pos_sub_sets union_wit_sets assms sgn_meas by simp qed also have "... \ \ (pos_sub E) + (- suminf (\n. 1 / real (num_wtn E n)))" proof - have "\ (union_wit E) \ - suminf (\n. 1 / real (num_wtn E n))" using union_wit_meas_le[of E] assms by simp thus ?thesis using union_wit_infty assms using add_left_mono by blast qed also have "... = \ (pos_sub E) - suminf (\n. 1 / real (num_wtn E n))" by (simp add: minus_ereal_def) finally have "0 < \ (pos_sub E) - suminf (\n. 1 / real (num_wtn E n))" . moreover have "0 < suminf (\n. 1 / real (num_wtn E n))" proof (rule suminf_pos2) show "0 < 1 / real (num_wtn E 0)" using inf_neg_ge_1[of E] assms pos_wtn_base unfolding num_wtn_def by simp show "\n. 0 \ 1 / real (num_wtn E n)" by simp show "summable (\n. 1 / real (num_wtn E n))" using assms inv_num_wtn_summable by simp qed ultimately show ?thesis using pos_sub_infty assms by fastforce qed lemma num_wtn_conv: assumes "E \ sets M" and "\\ E\ < \" shows "(\n. 1/(num_wtn E n)) \ 0" proof (rule summable_LIMSEQ_zero) show "summable (\n. 1 / real (num_wtn E n))" using assms inv_num_wtn_summable by simp qed lemma num_wtn_shift_conv: assumes "E \ sets M" and "\\ E\ < \" shows "(\n. 1/(num_wtn E n - 1)) \ 0" proof (rule summable_LIMSEQ_zero) show "summable (\n. 1 / real (num_wtn E n - 1))" using assms inv_num_wtn_shift_summable by simp qed lemma inf_neg_E_set: assumes "0 < inf_neg E" shows "E \ sets M" using assms unfolding inf_neg_def by presburger lemma inf_neg_pos_meas: assumes "0 < inf_neg E" shows "\ pos_meas_set E" using assms unfolding inf_neg_def by presburger lemma inf_neg_mem: assumes "0 < inf_neg E" shows "inf_neg E \ {n::nat|n. (1::nat) \ n \ (\B \ sets M. B \ E \ \ B < ereal (-1/n))}" proof - have "E \ sets M" using assms unfolding inf_neg_def by presburger moreover have "\ pos_meas_set E" using assms unfolding inf_neg_def by presburger ultimately have "{n::nat|n. (1::nat) \ n \ (\B \ sets M. B \ E \ \ B < ereal (-1/n))} \ {}" using inf_neg_ne[of E] by simp thus ?thesis unfolding inf_neg_def by (meson Inf_nat_def1 \E \ sets M\ \\ pos_meas_set E\) qed lemma prec_inf_neg_pos: assumes "0 < inf_neg E - 1" and "B \ sets M" and "B\ E" shows "-1/(inf_neg E - 1) \ \ B" proof (rule ccontr) define S where "S = {p::nat|p. (1::nat) \ p \ (\B \ sets M. B \ E \ \ B < ereal (-1/p))}" assume "\ ereal (- 1 / real (inf_neg E - 1)) \ \ B" hence "\ B < -1/(inf_neg E - 1)" by auto hence "inf_neg E - 1\ S" unfolding S_def using assms by auto have "Suc 0 < inf_neg E" using assms by simp hence "inf_neg E \ S" unfolding S_def using inf_neg_mem[of E] by simp hence "S \ {}" by auto have "inf_neg E = Inf S" unfolding S_def inf_neg_def using assms inf_neg_E_set inf_neg_pos_meas by auto have "inf_neg E - 1 < inf_neg E" using assms by simp hence "inf_neg E -1 \ S" using cInf_less_iff[of S] \S \ {}\ \inf_neg E = Inf S\ by auto thus False using \inf_neg E - 1 \ S\ by simp qed lemma pos_wtn_meas_ge: assumes "E \ sets M" and "\\ E\ < \" and "C\ sets M" and "\n. C\ pos_wtn E n" and "\n. 0 < num_wtn E n" shows "\N. \n\ N. - 1/ (num_wtn E n - 1) \ \ C" proof - have "\N. \n\ N. 1/(num_wtn E n) < 1/2" using num_wtn_conv[of E] conv_0_half[of "\n. 1 / real (num_wtn E n)"] assms by simp from this obtain N where "\n\ N. 1/(num_wtn E n) < 1/2" by auto { fix n assume "N \ n" hence "1/(num_wtn E n) < 1/2" using \\n\ N. 1/(num_wtn E n) < 1/2\ by simp have "1/(1/2) < 1/(1/(num_wtn E n))" proof (rule frac_less2, auto) show "2 / real (num_wtn E n) < 1" using \1/(num_wtn E n) < 1/2\ by linarith show "0 < num_wtn E n" unfolding num_wtn_def using inf_neg_ge_1 assms by (simp add: num_wtn_def) qed hence "2 < (num_wtn E n)" by simp hence "Suc 0 < num_wtn E n - 1" unfolding num_wtn_def by simp hence "- 1/ (num_wtn E n - 1) \ \ C" using assms prec_inf_neg_pos unfolding num_wtn_def by simp } thus ?thesis by auto qed lemma pos_sub_pos_meas_subset: assumes "E \ sets M" and "\\ E\ < \" and "C\ sets M" and "C\ (pos_sub E)" and "\n. 0 < num_wtn E n" shows "0 \ \ C" proof - have "\n. C \ pos_wtn E n" using assms unfolding pos_sub_def by auto hence "\N. \n\ N. - 1/ (num_wtn E n - 1) \ \ C" using assms pos_wtn_meas_ge[of E C] by simp from this obtain N where Nprop: "\n\ N. - 1/ (num_wtn E n - 1) \ \ C" by auto show "0 \ \ C" proof (rule lim_mono) show "\n. N \ n \ - 1/ (num_wtn E n - 1) \ (\n. \ C) n" using Nprop by simp have "(\n. ( 1 / real (num_wtn E n - 1))) \ 0" using assms num_wtn_shift_conv[of E] by simp hence "(\n. (- 1 / real (num_wtn E n - 1))) \ 0" using tendsto_minus[of "\n. 1 / real (num_wtn E n - 1)" 0] by simp thus "(\n. ereal (- 1 / real (num_wtn E n - 1))) \ 0" by (simp add: zero_ereal_def) show "(\n. \ C) \ \ C" by simp qed qed lemma pos_sub_pos_meas': assumes "E \ sets M" and "\\ E\ < \" and "0 < \ E" and "\n. 0 < num_wtn E n" shows "0 < \ (pos_sub E)" proof - have "0 < \ E" using assms by simp also have "... = \ (pos_sub E) + \ (union_wit E)" proof - have "E = pos_sub E \ (union_wit E)" using pos_sub_diff[of E] union_wit_subset by force moreover have "pos_sub E \ union_wit E = {}" using pos_sub_diff by auto ultimately show ?thesis using signed_measure_add[of M \ "pos_sub E" "union_wit E"] pos_sub_sets union_wit_sets assms sgn_meas by simp qed also have "... \ \ (pos_sub E) + (- suminf (\n. 1 / real (num_wtn E n)))" proof - have "\ (union_wit E) \ - suminf (\n. 1 / real (num_wtn E n))" using union_wit_meas_le[of E] assms by simp thus ?thesis using union_wit_infty assms using add_left_mono by blast qed also have "... = \ (pos_sub E) - suminf (\n. 1 / real (num_wtn E n))" by (simp add: minus_ereal_def) finally have "0 < \ (pos_sub E) - suminf (\n. 1 / real (num_wtn E n))" . moreover have "0 < suminf (\n. 1 / real (num_wtn E n))" proof (rule suminf_pos2) show "0 < 1 / real (num_wtn E 0)" using assms by simp show "\n. 0 \ 1 / real (num_wtn E n)" by simp show "summable (\n. 1 / real (num_wtn E n))" using assms inv_num_wtn_summable by simp qed ultimately show ?thesis using pos_sub_infty assms by fastforce qed text \We obtain the main result of this part on the existence of a positive subset.\ lemma exists_pos_meas_subset: assumes "E \ sets M" and "\\ E\ < \" and "0 < \ E" shows "\A. A \ E \ pos_meas_set A \ 0 < \ A" proof (cases "\n. 0 < num_wtn E n") case True have "pos_meas_set (pos_sub E)" proof (rule pos_meas_setI) show "pos_sub E \ sets M" by (simp add: assms(1) pos_sub_sets) fix A assume "A \ sets M" and "A\ pos_sub E" thus "0 \ \ A" using assms True pos_sub_pos_meas_subset[of E] by simp qed moreover have "0 < \ (pos_sub E)" using pos_sub_pos_meas'[of E] True assms by simp ultimately show ?thesis using pos_meas_set_def by (metis pos_sub_subset) next case False hence "\n. num_wtn E n = 0" by simp from this obtain n where "num_wtn E n = 0" by auto hence "pos_wtn E n \ sets M \ pos_meas_set (pos_wtn E n)" using inf_neg_ge_1 unfolding num_wtn_def by fastforce hence "pos_meas_set (pos_wtn E n)" using assms by (simp add: \E \ sets M\ pos_wtn_sets) moreover have "0 < \ (pos_wtn E n)" using pos_wtn_meas_gt assms by simp ultimately show ?thesis using pos_meas_set_def by (meson pos_wtn_subset) qed section \The Hahn decomposition theorem\ definition seq_meas where "seq_meas = (SOME f. incseq f \ range f \ pos_img \ \ pos_img = \ range f)" lemma seq_meas_props: shows "incseq seq_meas \ range seq_meas \ pos_img \ \ pos_img = \ range seq_meas" proof - have ex: "\f. incseq f \ range f \ pos_img \ \ pos_img = \ range f" proof (rule Extended_Real.Sup_countable_SUP) show "pos_img \ {}" proof - have "{} \ pos_sets" using empty_pos_meas_set unfolding pos_sets_def by simp hence "\ {} \ pos_img" unfolding pos_img_def by auto thus ?thesis by auto qed qed let ?V = "SOME f. incseq f \ range f \ pos_img \ \ pos_img = \ range f" have vprop: "incseq ?V \ range ?V \ pos_img \ \ pos_img = \ range ?V" using someI_ex[of "\f. incseq f \ range f \ pos_img \ \ pos_img = \ range f"] ex by blast show ?thesis using seq_meas_def vprop by presburger qed definition seq_meas_rep where "seq_meas_rep n = (SOME A. A\ pos_sets \ seq_meas n = \ A)" lemma seq_meas_rep_ex: shows "seq_meas_rep n \ pos_sets \ \ (seq_meas_rep n) = seq_meas n" proof - have ex: "\A. A \ pos_sets \ seq_meas n = \ A" using seq_meas_props - by (smt (z3) UNIV_I image_subset_iff mem_Collect_eq pos_img_def) + by (smt (verit) UNIV_I image_subset_iff mem_Collect_eq pos_img_def) let ?V = "SOME A. A\ pos_sets \ seq_meas n = \ A" have vprop: "?V\ pos_sets \ seq_meas n = \ ?V" using someI_ex[of "\A. A\ pos_sets \ seq_meas n = \ A"] using ex by blast show ?thesis using seq_meas_rep_def vprop by fastforce qed lemma seq_meas_rep_pos: assumes "\E \ sets M. \ E < \" shows "pos_meas_set (\ i. seq_meas_rep i)" proof (rule pos_meas_set_Union) show " \i. pos_meas_set (seq_meas_rep i)" using seq_meas_rep_ex signed_measure_space.pos_sets_def signed_measure_space_axioms by auto then show "\i. seq_meas_rep i \ sets M" by (simp add: pos_meas_setD1) show "\\ (\ (range seq_meas_rep))\ < \" proof - have "(\ (range seq_meas_rep)) \ sets M" proof (rule sigma_algebra.countable_Union) show "sigma_algebra (space M) (sets M)" by (simp add: sets.sigma_algebra_axioms) show "countable (range seq_meas_rep)" by simp show "range seq_meas_rep \ sets M" by (simp add: \\i. seq_meas_rep i \ sets M\ image_subset_iff) qed hence "\ (\ (range seq_meas_rep)) \ 0 " using \\i. pos_meas_set (seq_meas_rep i)\ \\i. seq_meas_rep i \ sets M\ signed_measure_space.pos_meas_set_pos_lim signed_measure_space_axioms by blast thus ?thesis using assms \\ (range seq_meas_rep) \ sets M\ abs_ereal_ge0 by simp qed qed lemma sup_seq_meas_rep: assumes "\E \ sets M. \ E < \" and "S = (\ pos_img)" and "A = (\ i. seq_meas_rep i)" shows "\ A = S" proof - have pms: "pos_meas_set (\ i. seq_meas_rep i)" using assms seq_meas_rep_pos by simp hence "\ A \ S" by (metis (mono_tags, lifting) Sup_upper \S = \ pos_img\ mem_Collect_eq pos_img_def pos_meas_setD1 pos_sets_def assms(2) assms(3)) have "\n. (\ A = \ (A - seq_meas_rep n) + \ (seq_meas_rep n))" proof fix n have "A = (A - seq_meas_rep n) \ seq_meas_rep n " using \A = \ (range seq_meas_rep)\ by blast hence "\ A = \ ((A - seq_meas_rep n) \ seq_meas_rep n)" by simp also have "... = \ (A - seq_meas_rep n) + \ (seq_meas_rep n)" proof (rule signed_measure_add) show "signed_measure M \" using sgn_meas by simp show "seq_meas_rep n \ sets M" using pos_sets_def seq_meas_rep_ex by auto then show "A - seq_meas_rep n \ sets M" by (simp add: assms pms pos_meas_setD1 sets.Diff) show "(A - seq_meas_rep n) \ seq_meas_rep n = {}" by auto qed finally show "\ A = \ (A - seq_meas_rep n) + \ (seq_meas_rep n)". qed have "\n. \ A \ \ (seq_meas_rep n)" proof fix n have "\ A \ 0" using pms assms unfolding pos_meas_set_def by auto have "(A - seq_meas_rep n) \ A" by simp hence "pos_meas_set (A - seq_meas_rep n)" proof - have "(A - seq_meas_rep n) \ sets M" using pms assms pos_meas_setD1 pos_sets_def seq_meas_rep_ex by auto thus ?thesis using pms assms unfolding pos_meas_set_def by auto qed hence "\ (A - seq_meas_rep n) \ 0" unfolding pos_meas_set_def by auto thus "\ (seq_meas_rep n) \ \ A" using \\n. (\ A = \ (A - seq_meas_rep n) + \ (seq_meas_rep n))\ by (metis ereal_le_add_self2) qed hence "\ A \ (\ range seq_meas)" by (simp add: Sup_le_iff seq_meas_rep_ex) moreover have "S = (\ range seq_meas)" using seq_meas_props \S = (\ pos_img)\ by simp ultimately have "\ A \ S" by simp thus "\ A = S" using \\ A \ S\ by simp qed lemma seq_meas_rep_compl: assumes "\E \ sets M. \ E < \" and "A = (\ i. seq_meas_rep i)" shows "neg_meas_set ((space M) - A)" unfolding neg_meas_set_def proof (rule ccontr) assume asm: "\ (space M - A \ sets M \ (\Aa\sets M. Aa \ space M - A \ \ Aa \ 0))" define S where "S = (\ pos_img)" have "pos_meas_set A" using assms seq_meas_rep_pos by simp have "\ A = S" using sup_seq_meas_rep assms S_def by simp hence "S < \" using assms \pos_meas_set A\ pos_meas_setD1 by blast have "(space M - A \ sets M)" by (simp add: \pos_meas_set A\ pos_meas_setD1 sets.compl_sets) hence " \(\Aa\sets M. Aa \ space M - A \ \ Aa \ 0)" using asm by blast hence "\ E \ sets M. E \ ((space M) - A) \ \ E > 0" by (metis less_eq_ereal_def linear) from this obtain E where "E \ sets M" and "E \ ((space M) - A)" and "\ E > 0" by auto have "\ A0 \ E. pos_meas_set A0 \ \ A0 > 0" proof (rule exists_pos_meas_subset) show "E \ sets M" using \E \ sets M\ by simp show "0 < \ E" using \\ E > 0\ by simp show "\\ E\ < \" proof - have "\ E < \" using assms \E \ sets M\ by simp moreover have "- \ < \ E" using \0 < \ E\ by simp ultimately show ?thesis by (meson ereal_infty_less(1) not_inftyI) qed qed from this obtain A0 where "A0 \ E" and "pos_meas_set A0" and " \ A0 > 0" by auto have "pos_meas_set (A \ A0)" using pos_meas_set_union \pos_meas_set A0\ \pos_meas_set A\ by simp have "\ (A \ A0) = \ A + \ A0" proof (rule signed_measure_add) show "signed_measure M \" using sgn_meas by simp show "A \ sets M" using \pos_meas_set A\ unfolding pos_meas_set_def by simp show "A0 \ sets M" using \pos_meas_set A0\ unfolding pos_meas_set_def by simp show "(A \ A0) = {}" using \A0 \ E\ \E \ ((space M) - A)\ by auto qed then have "\ (A \ A0) > S" using \\ A = S\ \\ A0 > 0\ by (metis \S < \\ \pos_meas_set (A \ A0)\ abs_ereal_ge0 ereal_between(2) not_inftyI not_less_iff_gr_or_eq pos_meas_self) have "(A \ A0) \ pos_sets" proof - have " (A \ A0) \ sets M" using sigma_algebra.countable_Union by (simp add: \pos_meas_set (A \ A0)\ pos_meas_setD1) moreover have "pos_meas_set (A \ A0)" using \pos_meas_set (A \ A0)\ by simp ultimately show ?thesis unfolding pos_sets_def by simp qed then have "\ (A \ A0) \ pos_img" unfolding pos_img_def by auto show False using \\ (A \ A0) > S\ \\ (A \ A0) \ pos_img\ \S = (\ pos_img)\ by (metis Sup_upper sup.absorb_iff2 sup.strict_order_iff) qed lemma hahn_decomp_finite: assumes "\E \ sets M. \ E < \" shows "\ M1 M2. hahn_space_decomp M1 M2" unfolding hahn_space_decomp_def proof - define S where "S = (\ pos_img)" define A where "A = (\ i. seq_meas_rep i)" have "pos_meas_set A" unfolding A_def using assms seq_meas_rep_pos by simp have "neg_meas_set ((space M) - A)" using seq_meas_rep_compl assms unfolding A_def by simp show "\M1 M2. pos_meas_set M1 \ neg_meas_set M2 \ space M = M1 \ M2 \ M1 \ M2 = {}" proof (intro exI conjI) show "pos_meas_set A" using \pos_meas_set A\ . show "neg_meas_set (space M - A)" using \neg_meas_set (space M - A)\ . show "space M = A \ (space M - A)" by (metis Diff_partition \pos_meas_set A\ inf.absorb_iff2 pos_meas_setD1 sets.Int_space_eq1) show "A \ (space M - A) = {}" by auto qed qed theorem hahn_decomposition: shows "\ M1 M2. hahn_space_decomp M1 M2" proof (cases "\E \ sets M. \ E < \") case True thus ?thesis using hahn_decomp_finite by simp next case False define m where "m = (\A . - \ A)" have "\ M1 M2. signed_measure_space.hahn_space_decomp M m M1 M2" proof (rule signed_measure_space.hahn_decomp_finite) show "signed_measure_space M m" using signed_measure_minus sgn_meas \m = (\A . - \ A)\ by (unfold_locales, simp) show "\E\sets M. m E < \" proof fix E assume "E \ sets M" show "m E < \" proof show "m E \ \" proof (rule ccontr) assume "\ m E \ \" have "m E = \" using \\ m E \ \\ by auto have "signed_measure M m" using \signed_measure_space M m\ signed_measure_space_def by auto moreover have "m E = - \ E" using \m = (\A . - \ A)\ by auto then have "\ \ range m" using \signed_measure M m\ by (metis (no_types, lifting) False ereal_less_PInfty ereal_uminus_eq_reorder image_iff inf_range m_def rangeI) show False using \m E = \\ \\ \ range m\ by (metis rangeI) qed qed qed qed hence "\ M1 M2. (neg_meas_set M1) \ (pos_meas_set M2) \ (space M = M1 \ M2) \ (M1 \ M2 = {})" using pos_meas_set_opp neg_meas_set_opp unfolding m_def by (metis sgn_meas signed_measure_minus signed_measure_space_def signed_measure_space.hahn_space_decomp_def) thus ?thesis using hahn_space_decomp_def by (metis inf_commute sup_commute) qed section \The Jordan decomposition theorem\ definition jordan_decomp where "jordan_decomp m1 m2 \ ((measure_space (space M) (sets M) m1) \ (measure_space (space M) (sets M) m2) \ (\A\ sets M. 0 \ m1 A) \ (\ A\ sets M. 0 \ m2 A) \ (\A \ sets M. \ A = (m1 A) - (m2 A)) \ (\ P N A. hahn_space_decomp P N \ (A \ sets M \ A \ P \ (m2 A) = 0) \ (A \ sets M \ A \ N \ (m1 A) = 0)) \ ((\A \ sets M. m1 A < \) \ (\A \ sets M. m2 A < \)))" lemma jordan_decomp_pos_meas: assumes "jordan_decomp m1 m2" and "hahn_space_decomp P N" and "A \ sets M" shows "m1 A = \ (A \ P)" proof - have "A\P \ sets M" using assms unfolding hahn_space_decomp_def by (simp add: pos_meas_setD1 sets.Int) have "A\ N \ sets M" using assms unfolding hahn_space_decomp_def by (simp add: neg_meas_setD1 sets.Int) have "(A \ P) \ (A\ N) = {}" using assms unfolding hahn_space_decomp_def by auto have "A = (A \ P) \ (A\ N)" using assms unfolding hahn_space_decomp_def by (metis Int_Un_distrib sets.Int_space_eq2) hence "m1 A = m1 ((A \ P) \ (A\ N))" by simp also have "... = m1 (A \ P) + m1 (A \ N)" using assms pos_e2ennreal_additive[of M m1] \A\P \ sets M\ \A\N \ sets M\ \A \ P \ (A \ N) = {}\ unfolding jordan_decomp_def additive_def by simp also have "... = m1 (A \ P)" using assms unfolding jordan_decomp_def by (metis Int_lower2 \A \ N \ sets M\ add.right_neutral) also have "... = m1 (A \ P) - m2 (A \ P)" using assms unfolding jordan_decomp_def by (metis Int_subset_iff \A \ P \ sets M\ ereal_minus(7) local.pos_wtn_base pos_wtn_subset) also have "... = \ (A \ P)" using assms \A \ P \ sets M\ unfolding jordan_decomp_def by simp finally show ?thesis . qed lemma jordan_decomp_neg_meas: assumes "jordan_decomp m1 m2" and "hahn_space_decomp P N" and "A \ sets M" shows "m2 A = -\ (A \ N)" proof - have "A\P \ sets M" using assms unfolding hahn_space_decomp_def by (simp add: pos_meas_setD1 sets.Int) have "A\ N \ sets M" using assms unfolding hahn_space_decomp_def by (simp add: neg_meas_setD1 sets.Int) have "(A \ P) \ (A\ N) = {}" using assms unfolding hahn_space_decomp_def by auto have "A = (A \ P) \ (A\ N)" using assms unfolding hahn_space_decomp_def by (metis Int_Un_distrib sets.Int_space_eq2) hence "m2 A = m2 ((A \ P) \ (A\ N))" by simp also have "... = m2 (A \ P) + m2 (A \ N)" using pos_e2ennreal_additive[of M m2] assms \A\P \ sets M\ \A\N \ sets M\ \A \ P \ (A \ N) = {}\ unfolding jordan_decomp_def additive_def by simp also have "... = m2 (A \ N)" using assms unfolding jordan_decomp_def by (metis Int_lower2 \A \ P \ sets M\ add.commute add.right_neutral) also have "... = m2 (A \ N) - m1 (A \ N)" using assms unfolding jordan_decomp_def by (metis Int_lower2 \A \ N \ sets M\ ereal_minus(7)) also have "... = -\ (A \ N)" using assms \A \ P \ sets M\ unfolding jordan_decomp_def by (metis Diff_cancel Diff_eq_empty_iff Int_Un_eq(2) \A \ N \ sets M\ \m2 (A \ N) = m2 (A \ N) - m1 (A \ N)\ ereal_minus(8) ereal_uminus_eq_reorder sup.bounded_iff) finally show ?thesis . qed lemma pos_inter_neg_0: assumes "hahn_space_decomp M1 M2" and "hahn_space_decomp P N" and "A \ sets M" and "A \ N" shows "\ (A \ M1) = 0" proof - have "\ (A \ M1) = \ (A \ ((M1 \ P) \ (M1 \ (sym_diff M1 P))))" by (metis Diff_subset_conv Int_Un_distrib Un_upper1 inf.orderE) also have "... = \ ((A \ (M1 \ P)) \ (A \ (M1 \ (sym_diff M1 P))))" by (simp add: Int_Un_distrib) also have "... = \ (A \ (M1 \ P)) + \ (A \ (M1 \ (sym_diff M1 P)))" proof (rule signed_measure_add) show "signed_measure M \" using sgn_meas . show "A \ (M1 \ P) \ sets M" by (meson assms(1) assms(2) assms(3) hahn_space_decomp_def sets.Int signed_measure_space.pos_meas_setD1 signed_measure_space_axioms) show "A \ (M1 \ sym_diff M1 P) \ sets M" by (meson Diff_subset assms(1) assms(2) assms(3) hahn_space_decomp_def pos_meas_setD1 pos_meas_set_union pos_meas_subset sets.Diff sets.Int) show "A \ (M1 \ P) \ (A \ (M1 \ sym_diff M1 P)) = {}" by auto qed also have "... = \ (A \ (M1 \ (sym_diff M1 P)))" proof - have "A \ (M1 \ P) = {}" using assms hahn_space_decomp_def by auto thus ?thesis using signed_measure_empty[OF sgn_meas] by simp qed also have "... = 0" proof (rule hahn_decomp_ess_unique[OF assms(1) assms(2)]) show "A \ (M1 \ sym_diff M1 P) \ sym_diff M1 P \ sym_diff M2 N" by auto show "A \ (M1 \ sym_diff M1 P) \ sets M" proof - have "sym_diff M1 P \ sets M" using assms by (meson hahn_space_decomp_def sets.Diff sets.Un signed_measure_space.pos_meas_setD1 signed_measure_space_axioms) hence "M1 \ sym_diff M1 P \ sets M" by (meson assms(1) hahn_space_decomp_def pos_meas_setD1 sets.Int) thus ?thesis by (simp add: assms sets.Int) qed qed finally show ?thesis . qed lemma neg_inter_pos_0: assumes "hahn_space_decomp M1 M2" and "hahn_space_decomp P N" and "A \ sets M" and "A \ P" shows "\ (A \ M2) = 0" proof - have "\ (A \ M2) = \ (A \ ((M2 \ N) \ (M2 \ (sym_diff M2 N))))" by (metis Diff_subset_conv Int_Un_distrib Un_upper1 inf.orderE) also have "... = \ ((A \ (M2 \ N)) \ (A \ (M2 \ (sym_diff M2 N))))" by (simp add: Int_Un_distrib) also have "... = \ (A \ (M2 \ N)) + \ (A \ (M2 \ (sym_diff M2 N)))" proof (rule signed_measure_add) show "signed_measure M \" using sgn_meas . show "A \ (M2 \ N) \ sets M" by (meson assms(1) assms(2) assms(3) hahn_space_decomp_def sets.Int signed_measure_space.neg_meas_setD1 signed_measure_space_axioms) show "A \ (M2 \ sym_diff M2 N) \ sets M" by (meson Diff_subset assms(1) assms(2) assms(3) hahn_space_decomp_def neg_meas_setD1 neg_meas_set_union neg_meas_subset sets.Diff sets.Int) show "A \ (M2 \ N) \ (A \ (M2 \ sym_diff M2 N)) = {}" by auto qed also have "... = \ (A \ (M2 \ (sym_diff M2 N)))" proof - have "A \ (M2 \ N) = {}" using assms hahn_space_decomp_def by auto thus ?thesis using signed_measure_empty[OF sgn_meas] by simp qed also have "... = 0" proof (rule hahn_decomp_ess_unique[OF assms(1) assms(2)]) show "A \ (M2 \ sym_diff M2 N) \ sym_diff M1 P \ sym_diff M2 N" by auto show "A \ (M2 \ sym_diff M2 N) \ sets M" proof - have "sym_diff M2 N \ sets M" using assms by (meson hahn_space_decomp_def sets.Diff sets.Un signed_measure_space.neg_meas_setD1 signed_measure_space_axioms) hence "M2 \ sym_diff M2 N \ sets M" by (meson assms(1) hahn_space_decomp_def neg_meas_setD1 sets.Int) thus ?thesis by (simp add: assms sets.Int) qed qed finally show ?thesis . qed lemma jordan_decomposition : shows "\ m1 m2. jordan_decomp m1 m2" proof - have "\ M1 M2. hahn_space_decomp M1 M2" using hahn_decomposition unfolding hahn_space_decomp_def by simp from this obtain M1 M2 where "hahn_space_decomp M1 M2" by auto note Mprops = this define m1 where "m1 = (\A. \ (A \ M1))" define m2 where "m2 = (\A. -\ (A \ M2))" show ?thesis unfolding jordan_decomp_def proof (intro exI allI impI conjI ballI) show "measure_space (space M) (sets M) (\x. e2ennreal (m1 x))" using pos_signed_to_meas_space Mprops m1_def unfolding hahn_space_decomp_def by auto next show "measure_space (space M) (sets M) (\x. e2ennreal (m2 x))" using neg_signed_to_meas_space Mprops m2_def unfolding hahn_space_decomp_def by auto next fix A assume "A\ sets M" thus "0 \ m1 A" unfolding m1_def using Mprops unfolding hahn_space_decomp_def by (meson inf_sup_ord(2) pos_meas_setD1 sets.Int signed_measure_space.pos_measure_meas signed_measure_space_axioms) next fix A assume "A\ sets M" thus "0 \ m2 A" unfolding m2_def using Mprops unfolding hahn_space_decomp_def by (metis ereal_0_le_uminus_iff inf_sup_ord(2) neg_meas_self neg_meas_setD1 neg_meas_subset sets.Int) next fix A assume "A \ sets M" have "\ A = \ ((A \ M1) \ (A \ M2))" using Mprops unfolding hahn_space_decomp_def by (metis Int_Un_distrib \A \ sets M\ sets.Int_space_eq2) also have "... = \ (A \ M1) + \ (A \ M2)" proof (rule signed_measure_add) show "signed_measure M \" using sgn_meas . show "A \ M1 \ sets M" using Mprops \A \ sets M\ unfolding hahn_space_decomp_def by (simp add: pos_meas_setD1 sets.Int) show "A \ M2 \ sets M" using Mprops \A \ sets M\ unfolding hahn_space_decomp_def by (simp add: neg_meas_setD1 sets.Int) show "A \ M1 \ (A \ M2) = {}" using Mprops unfolding hahn_space_decomp_def by auto qed also have "... = m1 A - m2 A" using m1_def m2_def by simp finally show "\ A = m1 A - m2 A" . next fix P N A assume "hahn_space_decomp P N" and "A \ sets M" and "A \ N" note hn = this have "\ (A \ M1) = 0" proof (rule pos_inter_neg_0[OF _ hn]) show "hahn_space_decomp M1 M2" using Mprops unfolding hahn_space_decomp_def by simp qed thus "m1 A = 0" unfolding m1_def by simp next fix P N A assume "hahn_space_decomp P N" and "A \ sets M" and "A \ P" note hp = this have "\ (A \ M2) = 0" proof (rule neg_inter_pos_0[OF _ hp]) show "hahn_space_decomp M1 M2" using Mprops unfolding hahn_space_decomp_def by simp qed thus "m2 A = 0" unfolding m2_def by simp next show "(\E\sets M. m1 E < \) \ (\E\sets M. m2 E < \)" proof (cases "\ E \ sets M. m1 E < \") case True thus ?thesis by simp next case False have "\ E \ sets M. m2 E < \" proof fix E assume "E \ sets M" show "m2 E < \" proof - have "(m2 E) = -\ (E \ M2)" using m2_def by simp also have "... \ \" using False sgn_meas inf_range by (metis ereal_less_PInfty ereal_uminus_uminus m1_def rangeI) finally have "m2 E \ \" . thus ?thesis by (simp add: top.not_eq_extremum) qed qed thus ?thesis by simp qed qed qed lemma jordan_decomposition_unique : assumes "jordan_decomp m1 m2" and "jordan_decomp n1 n2" and "A \ sets M" shows "m1 A = n1 A" "m2 A = n2 A" proof - have "\ M1 M2. hahn_space_decomp M1 M2" using hahn_decomposition by simp from this obtain M1 M2 where "hahn_space_decomp M1 M2" by auto note mprop = this have "m1 A = \ (A \ M1)" using assms jordan_decomp_pos_meas mprop by simp also have "... = n1 A" using assms jordan_decomp_pos_meas[of n1] mprop by simp finally show "m1 A = n1 A" . have "m2 A = -\ (A \ M2)" using assms jordan_decomp_neg_meas mprop by simp also have "... = n2 A" using assms jordan_decomp_neg_meas[of n1] mprop by simp finally show "m2 A = n2 A" . qed end end diff --git a/thys/Lambda_Free_EPO/Chop.thy b/thys/Lambda_Free_EPO/Chop.thy --- a/thys/Lambda_Free_EPO/Chop.thy +++ b/thys/Lambda_Free_EPO/Chop.thy @@ -1,342 +1,343 @@ (* Title: The Chop Operation on Lambda-Free Higher-Order Terms Author: Alexander Bentkamp , 2018 Maintainer: Alexander Bentkamp *) section \The Chop Operation on Lambda-Free Higher-Order Terms\ theory Chop imports Embeddings begin definition chop :: "('s, 'v) tm \ ('s, 'v) tm" where "chop t = apps (hd (args t)) (tl (args t))" subsection \Basic properties\ lemma chop_App_Hd: "is_Hd s \ chop (App s t) = t" unfolding chop_def args.simps using args_Nil_iff_is_Hd by force lemma chop_apps: "is_App t \ chop (apps t ts) = apps (chop t) ts" unfolding chop_def by (simp add: args_Nil_iff_is_Hd) lemma vars_chop: "is_App t \ vars (chop t) \ vars_hd (head t) = vars t" by (induct rule:tm_induct_apps; metis (no_types, lifting) chop_def UN_insert Un_commute list.exhaust_sel list.simps(15) args_Nil_iff_is_Hd tm.simps(17) tm_exhaust_apps_sel vars_apps) lemma ground_chop: "is_App t \ ground t \ ground (chop t)" using vars_chop by auto lemma hsize_chop: "is_App t \ (Suc (hsize (chop t))) = hsize t" unfolding hsize_args[of t, symmetric] chop_def hsize_apps by (metis Nil_is_map_conv args_Nil_iff_is_Hd list.exhaust_sel list.map_sel(1) map_tl plus_1_eq_Suc sum_list.Cons) lemma hsize_chop_lt: "is_App t \ hsize (chop t) < hsize t" by (simp add: Suc_le_lessD less_or_eq_imp_le hsize_chop) lemma chop_fun: assumes "is_App t" "is_App (fun t)" shows "App (chop (fun t)) (arg t) = chop t" proof - have "args (fun t) \ []" using assms(2) args_Nil_iff_is_Hd by blast then show ?thesis unfolding chop_def using assms(1) by (metis (no_types) App_apps args.simps(2) hd_append2 tl_append2 tm.collapse(2)) qed subsection \Chop and the Embedding Relation\ lemma emb_step_chop: "is_App t \ t \\<^sub>e\<^sub>m\<^sub>b chop t" proof (induct "num_args t - 1" arbitrary:t) case 0 have nil: "num_args t = 0 \ t \\<^sub>e\<^sub>m\<^sub>b chop t" unfolding chop_def using 0 args_Nil_iff_is_Hd by force have single: "\a. args t = [a] \ t \\<^sub>e\<^sub>m\<^sub>b chop t" unfolding chop_def by (metis "0.prems" apps.simps(1) args.elims args_Nil_iff_is_Hd emb_step_arg last.simps last_snoc list.sel(1) list.sel(3) tm.sel(6)) then show ?case using nil single by (metis "0.hyps" length_0_conv length_tl list.exhaust_sel) next case (Suc x) have 1:"apps (Hd (head t)) (butlast (args t)) \\<^sub>e\<^sub>m\<^sub>b chop (apps (Hd (head t)) (butlast (args t)))" using Suc(1)[of "apps (Hd (head t)) (butlast (args t))"] by (metis Suc.hyps(2) Suc_eq_plus1 add_diff_cancel_right' args_Nil_iff_is_Hd length_butlast list.size(3) nat.distinct(1) tm_exhaust_apps_sel tm_inject_apps) have 2:"App (apps (Hd (head t)) (butlast (args t))) (last (args t)) = t" by (simp add: App_apps Suc.prems args_Nil_iff_is_Hd) have 3:"App (chop (apps (Hd (head t)) (butlast (args t)))) (last (args t)) = chop t" proof - have f1: "hd (args t) = hd (butlast (args t))" by (metis Suc.hyps(2) Suc.prems append_butlast_last_id args_Nil_iff_is_Hd hd_append2 length_0_conv length_butlast nat.simps(3)) have "tl (args t) = tl (butlast (args t)) @ [last (args t)]" by (metis (no_types) Suc.hyps(2) Suc.prems append_butlast_last_id args_Nil_iff_is_Hd length_0_conv length_butlast nat.simps(3) tl_append2) then show ?thesis using f1 chop_def by (metis App_apps append_Nil args.simps(1) args_apps) qed then show ?case using 1 2 3 by (metis context_left) qed lemma chop_emb_step_at: assumes "is_App t" shows "chop t = emb_step_at (replicate (num_args (fun t)) Left) Right t" using assms proof (induct "num_args (fun t)" arbitrary: t) case 0 then have rep_Nil:"replicate (num_args (fun t)) dir.Left = []" by simp then show ?case unfolding rep_Nil by (metis "0.hyps" "0.prems" emb_step_at_right append_Nil apps.simps(1) args.simps(2) chop_def length_0_conv list.sel(1) list.sel(3) tm.collapse(2)) next case (Suc n) then show ?case using Suc.hyps(1)[of "fun t"] using emb_step_at_left_context args.elims args_Nil_iff_is_Hd chop_fun butlast_snoc diff_Suc_1 length_0_conv length_butlast nat.distinct(1) replicate_Suc tm.collapse(2) tm.sel(4) by metis qed lemma emb_step_at_chop: assumes emb_step_at: "emb_step_at p Right t = s" and pos:"position_of t (p @ [Right])" and all_Left: "list_all (\x. x = Left) p" shows "chop t = s \ chop t \\<^sub>e\<^sub>m\<^sub>b s" proof - have "is_App t" by (metis emb_step_at_if_position emb_step_at_is_App emb_step_equiv pos) have p_replicate: "replicate (length p) Left = p" using replicate_length_same[of p Left] by (simp add: Ball_set all_Left) show ?thesis proof (cases "Suc (length p) = num_args t") case True then have "p = replicate (num_args (fun t)) Left" using p_replicate by (metis Suc_inject \is_App t\ args.elims args_Nil_iff_is_Hd length_append_singleton tm.sel(4)) then have "chop t = s" unfolding chop_emb_step_at[OF \is_App t\] using pos emb_step_at by blast then show ?thesis by blast next case False then have "Suc (length p) < num_args t" using pos emb_step_at \is_App t\ \list_all (\x. x = dir.Left) p\ proof (induct p arbitrary:t s) case Nil then show ?case by (metis Suc_lessI args_Nil_iff_is_Hd length_greater_0_conv list.size(3)) next case (Cons a p) have "a = Left" using Cons.prems(5) by auto have 1:"Suc (length p) \ num_args (fun t)" by (metis (no_types, lifting) Cons.prems(1) Cons.prems(4) args.elims args_Nil_iff_is_Hd length_Cons length_append_singleton tm.sel(4)) have 2:"position_of (fun t) (p @ [Right])" using \position_of t ((a # p) @ [Right])\ \is_App t\ by (metis (full_types) Cons.prems(5) position_of_left append_Cons list_all_simps(1) tm.collapse(2)) have 3: "emb_step_at p dir.Right (fun t) = emb_step_at p dir.Right (fun t)" using emb_step_at_left_context[of p Right "fun t" "arg t"] by blast have "Suc (length p) < num_args (fun t)" using Cons.hyps[OF 1 2 3] by (metis "2" Cons.prems(5) Nil_is_append_conv list_all_simps(1) not_Cons_self2 position_of.elims(2) tm.discI(2)) then show ?case by (metis Cons.prems(4) Suc_less_eq2 args.simps(2) length_Cons length_append_singleton tm.collapse(2)) qed define q where "q = replicate (num_args (fun t) - Suc (length p)) dir.Left" have "chop t = emb_step_at (p @ [Left] @ q) dir.Right t" proof - have "length p + (num_args (fun t) - length p) = num_args (fun t)" using \Suc (length p) < num_args t\ by (metis Suc_less_eq2 \is_App t\ args.simps(2) diff_Suc_1 leD length_butlast nat_le_linear ordered_cancel_comm_monoid_diff_class.add_diff_inverse snoc_eq_iff_butlast tm.collapse(2)) then have 1:"replicate (num_args (fun t)) dir.Left = p @ replicate (num_args (fun t) - length p) dir.Left" by (metis p_replicate replicate_add) have "0 < num_args (fun t) - length p" by (metis (no_types) False \is_App t\ \length p + (num_args (fun t) - length p) = num_args (fun t)\ args.simps(2) length_append_singleton less_Suc_eq less_add_Suc1 tm.collapse(2) zero_less_diff) then have "replicate (num_args (fun t) - length p) dir.Left = [Left] @ q" unfolding q_def by (metis (no_types) Cons_replicate_eq Nat.diff_cancel Suc_eq_plus1 \length p + (num_args (fun t) - length p) = num_args (fun t)\ append_Cons self_append_conv2) then show ?thesis using chop_emb_step_at using \is_App t\ 1 by (simp add: chop_emb_step_at) qed then have "chop t \\<^sub>e\<^sub>m\<^sub>b s" using pos merge_emb_step_at[of p Right q Right t] by (metis emb_step_at_if_position opp_simps(1) emb_step_at pos_emb_step_at_opp) then show ?thesis by blast qed qed lemma emb_step_at_remove_arg: assumes emb_step_at: "emb_step_at p Left t = s" and pos:"position_of t (p @ [Left])" and all_Left: "list_all (\x. x = Left) p" shows "let i = num_args t - Suc (length p) in head t = head s \ i < num_args t \ args s = take i (args t) @ drop (Suc i) (args t)" proof - have "is_App t" by (metis emb_step_at_if_position emb_step_at_is_App emb_step_equiv pos) have C1: "head t = head s" using all_Left emb_step_at pos proof (induct p arbitrary:s t) case Nil then have "s = emb_step_at [] dir.Left (App (fun t) (arg t))" by (metis position_of.elims(2) snoc_eq_iff_butlast tm.collapse(2) tm.discI(2)) then have "s = fun t" by simp then show ?case by simp next case (Cons a p) then have "a = Left" by simp then have "head (emb_step_at p Left (fun t)) = head t" by (metis Cons.hyps Cons.prems(1) head_fun list.pred_inject(2) position_if_emb_step_at) then show ?case using emb_step_at_left_context[of p a "fun t" "arg t"] by (metis Cons.prems(2) \a = Left\ emb_step_at_is_App head_App tm.collapse(2)) qed let ?i = "num_args t - Suc (length p)" have C2:"?i < num_args t" by (simp add: \is_App t\ args_Nil_iff_is_Hd) have C3:"args s = take ?i (args t) @ drop (Suc ?i) (args t)" using all_Left pos emb_step_at \is_App t\ proof (induct p arbitrary:s t) case Nil then show ?case using emb_step_at_left[of "fun t" "arg t"] by (simp, metis One_nat_def args.simps(2) butlast_conv_take butlast_snoc tm.collapse(2)) next case (Cons a p) have "position_of (fun t) (p @ [Left])" by (metis (full_types) Cons.prems(1) Cons.prems(2) Cons.prems(4) position_of_left append_Cons list.pred_inject(2) tm.collapse(2)) then have 0:"args (emb_step_at p Left (fun t)) = take (num_args (fun t) - Suc (length p)) (args (fun t)) @ drop (Suc (num_args (fun t) - Suc (length p))) (args (fun t))" using Cons.hyps[of "fun t"] by (metis Cons.prems(1) append_Nil args_Nil_iff_is_Hd drop_Nil emb_step_at_is_App list.size(3) list_all_simps(1) take_0 zero_diff) have 1:"s = App (emb_step_at p Left (fun t)) (arg t)" using emb_step_at_left_context[of p Left "fun t" "arg t"] using Cons.prems by auto define k where k_def:"k = (num_args (fun t) - Suc (length p))" have 2:"take k (args (fun t)) = take (num_args t - Suc (length (a # p))) (args t)" - by (smt k_def Cons.prems(4) args.elims args_Nil_iff_is_Hd butlast_snoc diff_Suc_eq_diff_pred - diff_Suc_less length_Cons length_butlast length_greater_0_conv take_butlast tm.sel(4)) + by (metis (no_types, lifting) Cons.prems(4) args.elims args_Nil_iff_is_Hd butlast_snoc + diff_Suc_eq_diff_pred diff_less k_def length_Cons length_butlast length_greater_0_conv + take_butlast tm.sel(4) zero_less_Suc) have k_def': "k = num_args t - Suc (Suc (length p))" using k_def by (metis args.simps(2) diff_Suc_Suc length_append_singleton local.Cons(5) tm.collapse(2)) have 3:"args (fun t) @ [arg t] = args t" by (metis Cons.prems(4) args.simps(2) tm.collapse(2)) have "num_args t > 1" using \position_of t ((a # p) @ [Left])\ by (metis "3" \position_of (fun t) (p @ [dir.Left])\ args_Nil_iff_is_Hd butlast_snoc emb_step.simps emb_step_at_if_position length_butlast length_greater_0_conv tm.discI(2) zero_less_diff) then have "Suc k1 < num_args t\ by linarith have "\k< num_args t. drop k (args (fun t)) @ [arg t] = drop k (args t)" by (metis (no_types, lifting) \args (fun t) @ [arg t] = args t\ drop_butlast drop_eq_Nil last_drop leD snoc_eq_iff_butlast) then show ?case using 0 1 2 3 k_def' using \Suc k < num_args t\ k_def by auto qed show ?thesis using C1 C2 C3 by simp qed lemma emb_step_cases [consumes 1, case_names chop extended_chop remove_arg under_arg]: assumes emb:"t \\<^sub>e\<^sub>m\<^sub>b s" and chop:"chop t = s \ P" and extended_chop:"chop t \\<^sub>e\<^sub>m\<^sub>b s \ P" and remove_arg:"\i. head t = head s \ i args s = take i (args t) @ drop (Suc i) (args t) \ P" and under_arg:"\i. head t = head s \ num_args t = num_args s \ args t ! i \\<^sub>e\<^sub>m\<^sub>b args s ! i \ (\j. j i \ j \ args t ! j = args s ! j) \ P" shows P proof - obtain p d where pd_def:"emb_step_at p d t = s" "position_of t (p @ [d])" using emb emb_step_equiv' position_if_emb_step_at by metis have "is_App t" by (metis emb emb_step_at_is_App emb_step_equiv) show ?thesis proof (cases "list_all (\x. x = Left) p") case True show ?thesis proof (cases d) case Left then show P using emb_step_at_remove_arg by (metis True pd_def(1) pd_def(2) remove_arg) next case Right then show P using True chop emb_step_at_chop extended_chop pd_def(1) pd_def(2) by blast qed next case False have 1:"num_args t = num_args s" using emb_step_under_args_num_args by (metis False pd_def(1)) have 2:"head t = head s" using emb_step_under_args_head by (metis False pd_def(1)) show ?thesis using 1 2 under_arg emb_step_under_args_emb_step by (metis False pd_def(1) pd_def(2)) qed qed lemma chop_position_of: assumes "is_App s" shows "position_of s (replicate (num_args (fun s)) dir.Left @ [Right])" by (metis Suc_n_not_le_n assms chop_emb_step_at lessI less_imp_le_nat position_if_emb_step_at hsize_chop) subsection \Chop and Substitutions\ (* TODO: move *) lemma Suc_num_args: "is_App t \ Suc (num_args (fun t)) = num_args t" by (metis args.simps(2) length_append_singleton tm.collapse(2)) (* TODO: move *) lemma fun_subst: "is_App s \ subst \ (fun s) = fun (subst \ s)" by (metis subst.simps(2) tm.collapse(2) tm.sel(4)) (* TODO: move *) lemma args_subst_Hd: assumes "is_Hd (subst \ (Hd (head s)))" shows "args (subst \ s) = map (subst \) (args s)" using assms by (metis append_Nil args_Nil_iff_is_Hd args_apps subst_apps tm_exhaust_apps_sel) lemma chop_subst_emb0: assumes "is_App s" assumes "chop (subst \ s) \ subst \ (chop s)" shows "emb_step_at (replicate (num_args (fun s)) Left) Right (chop (subst \ s)) = subst \ (chop s)" proof - have "is_App (subst \ s)" by (metis assms(1) subst.simps(2) tm.collapse(2) tm.disc(2)) have 1:"subst \ (chop s) = emb_step_at (replicate (num_args (fun s)) dir.Left) dir.Right (subst \ s)" using chop_emb_step_at[OF assms(1)] using emb_step_at_subst chop_position_of[OF \is_App s\] by (metis) have "num_args (fun s) \ num_args (fun (subst \ s))" using fun_subst[OF \is_App s\] by (metis args_subst leI length_append length_map not_add_less2) then have "num_args (fun s) < num_args (fun (subst \ s))" using assms(2) "1" \is_App (subst \ s)\ chop_emb_step_at le_imp_less_or_eq by fastforce then have "num_args s \ num_args (fun (subst \ s))" using Suc_num_args[OF \is_App s\] by linarith then have "replicate (num_args (fun s)) dir.Left @ [opp dir.Right] @ replicate (num_args (fun (subst \ s)) - num_args s) dir.Left = replicate (num_args (fun (subst \ s))) dir.Left" unfolding append.simps opp_simps replicate_Suc[symmetric] replicate_add[symmetric] using Suc_num_args[OF \is_App s\] by (metis add_Suc_shift ordered_cancel_comm_monoid_diff_class.add_diff_inverse) then show ?thesis unfolding 1 unfolding chop_emb_step_at[OF \is_App (subst \ s)\] by (metis merge_emb_step_at) qed lemma chop_subst_emb: assumes "is_App s" shows "chop (subst \ s) \\<^sub>e\<^sub>m\<^sub>b subst \ (chop s)" using chop_subst_emb0 by (metis assms emb.refl emb_step_equiv emb_step_is_emb) lemma chop_subst_Hd: assumes "is_App s" assumes "is_Hd (subst \ (Hd (head s)))" shows "chop (subst \ s) = subst \ (chop s)" proof - have "is_App (subst \ s)" by (metis assms(1) subst.simps(2) tm.collapse(2) tm.disc(2)) have "num_args (fun s) = num_args (fun (subst \ s))" unfolding fun_subst[OF \is_App s\,symmetric] using args_subst_Hd using assms(2) by auto then show ?thesis unfolding chop_emb_step_at[OF assms(1)] chop_emb_step_at[OF \is_App (subst \ s)\] using emb_step_at_subst[OF chop_position_of[OF \is_App s\]] by simp qed lemma chop_subst_Sym: assumes "is_App s" assumes "is_Sym (head s)" shows "chop (subst \ s) = subst \ (chop s)" by (metis assms(1) assms(2) chop_subst_Hd ground_imp_subst_iden hd.collapse(2) hd.simps(18) tm.disc(1) tm.simps(17)) end \ No newline at end of file diff --git a/thys/Lifting_the_Exponent/LTE.thy b/thys/Lifting_the_Exponent/LTE.thy --- a/thys/Lifting_the_Exponent/LTE.thy +++ b/thys/Lifting_the_Exponent/LTE.thy @@ -1,418 +1,418 @@ theory LTE imports "HOL-Number_Theory.Number_Theory" begin section "Library additions" lemma cong_sum_mono_neutral_right: assumes "finite T" assumes "S \ T" assumes zeros: "\i \ T - S. [g i = 0] (mod n)" shows "[sum g T = sum g S] (mod n)" proof - have "[sum g T = (\x\T. if x \ S then g x else 0)] (mod n)" using zeros by (auto intro: cong_sum) also have "(\x\T. if x \ S then g x else 0) = (\x\S. if x \ S then g x else 0)" by (intro sum.mono_neutral_right; fact?; auto) also have "... = sum g S" by (auto intro: sum.cong) finally show ?thesis. qed lemma power_odd_inj: fixes a b :: "'a::linordered_idom" assumes "odd k" and "a^k = b^k" shows "a = b" proof (cases "a \ 0") case True then have "b \ 0" using assms zero_le_odd_power by metis moreover from \odd k\ have "k > 0" by presburger show ?thesis by (rule power_eq_imp_eq_base; fact) next case False then have "b < 0" using assms power_less_zero_eq not_less by metis from \a^k = b^k\ have "(-a)^k = (-b)^k" using \odd k\ power_minus_odd by simp moreover have "-a \ 0" and "-b \ 0" using \\ a \ 0\ and \b < 0\ by auto moreover from \odd k\ have "k > 0" by presburger ultimately have "-a = -b" by (rule power_eq_imp_eq_base) then show ?thesis by simp qed lemma power_eq_abs: fixes a b :: "'a::linordered_idom" assumes "a^k = b^k" and "k > 0" shows "\a\ = \b\" proof - from \a^k = b^k\ have "\a\^k = \b\^k" using power_abs by metis show "\a\ = \b\" by (rule power_eq_imp_eq_base; fact?; auto) qed lemma cong_scale: "k \ 0 \ [a = b] (mod c) \ [k*a = k*b] (mod k*c)" unfolding cong_def by auto lemma odd_square_mod_4: fixes x :: int assumes "odd x" shows "[x^2 = 1] (mod 4)" proof - have "x^2 - 1 = (x - 1) * (x + 1)" by (simp add: ring_distribs power2_eq_square) moreover from \odd x\ have "2 dvd x - 1" and "2 dvd x + 1" by auto ultimately have "4 dvd x^2 - 1" by fastforce thus ?thesis by (simp add: cong_iff_dvd_diff) qed section \The \p > 2\ case\ context fixes x y :: int and p :: nat assumes "prime p" assumes "p dvd x - y" assumes "\p dvd x" "\p dvd y" begin lemma decompose_mod_p: "[(\ip dvd x - y\ have "[x = y] (mod p)" by (simp add: cong_iff_dvd_diff) hence "[y^(n - Suc i) * x^i = x^(n - Suc i) * x^i] (mod p)" by (intro cong_scalar_right cong_pow; rule cong_sym) also have "x^(n - Suc i) * x^i = x^(n - 1)" using \i < n\ by (simp flip: power_add) finally have "[y^(n - Suc i) * x^i = x^(n - 1)] (mod p)" by auto } hence "[(\iiiLemma 1:\ lemma multiplicity_diff_pow_coprime: assumes "coprime p n" shows "multiplicity p (x^n - y^n) = multiplicity p (x - y)" proof - have factor: "x^n - y^n = (\i p dvd (\iiprime p\ have "p dvd n \ p dvd x^(n-1)" by (simp add: prime_dvd_mult_eq_int) moreover from \coprime p n\ and \prime p\ have "\p dvd n" using coprime_absorb_right not_prime_unit by auto ultimately have "p dvd x^(n-1)" by simp hence "p dvd x" using \prime p\ prime_dvd_power_int prime_nat_int_transfer by blast with \\p dvd x\ show False by simp qed ultimately show "multiplicity p (x^n - y^n) = multiplicity p (x - y)" using \prime p\ by (auto intro: multiplicity_prime_elem_times_other) qed text \The inductive step:\ lemma multiplicity_diff_self_pow: assumes "p > 2" and "x \ y" shows "multiplicity p (x^p - y^p) = Suc (multiplicity p (x - y))" proof - have *: "multiplicity p (\itip dvd x - y\ obtain k::int where kp: "x = y + k * p" by (metis add.commute diff_add_cancel dvd_def mult.commute) have "[y^(p - Suc t) * x^t = y^(p-1) + t*k*p*y^(p-2)] (mod p^2)" if "t < p" for t proof (cases "t = 0") case False have "y^(p - Suc t) * x^t = y^(p - Suc t) * (y + k*p)^t" unfolding kp.. also have "... = y^(p - Suc t) * (\i\t. (t choose i) * (k*p)^i * y^(t-i))" by (simp flip: binomial_ring add: add.commute) also have "[... = y^(p - Suc t) * (\i\1. (t choose i) * (k*p)^i * y^(t-i))] (mod p^2)" \ \discard \i > 1\\ proof (intro cong_scalar_left cong_sum_mono_neutral_right; rule) fix i assume "i \ {..t} - {..1}" then have "i \ 2" by simp then obtain i' where "i = i' + 2" using add.commute le_Suc_ex by blast hence "(k*p)^i = (k*p)^i' * k^2 * p^2" by (simp add: ac_simps power2_eq_square) hence "[(k*p)^i = 0] (mod p^2)" by (simp add: cong_mult_self_right) thus "[(t choose i) * (k*p)^i * y^(t-i) = 0] (mod p^2)" by (simp add: cong_0_iff) qed (use \t \ 0\ in auto) also have "(\i\1. (t choose i) * (k*p)^i * y^(t-i)) = y^t + t*k*p*y^(t-1)" by simp also have "y^(p - Suc t) * ... = y^(p-1) + t*k*p*y^(p-2)" using \t < p\ \t \ 0\ by (auto simp add: algebra_simps numeral_eq_Suc simp flip: power_add) finally show ?thesis. qed simp hence "[(\ttttttp > 2\ and \prime p\ have "odd p" using prime_odd_nat by blast thus ?thesis by (metis (no_types, lifting) cong_0_iff div_mult_swap dvd_times_left_cancel_iff dvd_triv_left le_0_eq linorder_not_less mult.commute odd_pos odd_two_times_div_two_nat one_add_one power_add power_one_right) qed hence "[int ((p*(p - 1) div 2) * p)*k*y^(p-2) = 0] (mod p^2)" unfolding cong_0_iff using int_dvd_int_iff by fastforce thus ?thesis by (simp add: ac_simps) qed ultimately have "[(\t p^2 dvd p*y^(p-1)" using \p > 2\ \prime p\ \\ p dvd y\ by (simp add: power2_eq_square prime_dvd_power_int_iff) ultimately show "\ int p^(Suc 1) dvd (\tiprime p\ \x \ y\ multiplicity_zero * by auto ultimately show ?thesis by simp qed text \Theorem 1:\ theorem multiplicity_diff_pow: assumes "p > 2" and "x \ y" and "n > 0" shows "multiplicity p (x^n - y^n) = multiplicity p (x - y) + multiplicity p n" proof - obtain k where n: "n = p^multiplicity p n * k" and "\ p dvd k" using \n > 0\ \prime p\ by (metis neq0_conv not_prime_unit multiplicity_decompose') have "multiplicity p (x^(p^a * k) - y^(p^a * k)) = multiplicity p (x - y) + a" for a proof (induction a) case 0 from \\ p dvd k\ have "coprime p k" using \prime p\ by (intro prime_imp_coprime) thus ?case by (simp add: multiplicity_diff_pow_coprime) next case (Suc a) let ?x' = "x^(p^a*k)" and ?y' = "y^(p^a*k)" have "\ p dvd ?x'" and "\ p dvd ?y'" using \\ p dvd x\ \\ p dvd y\ and \prime p\ by (meson prime_dvd_power prime_nat_int_transfer)+ moreover have "p dvd ?x' - ?y'" using \p dvd x - y\ by (simp add: power_diff_sumr2) moreover have "?x' \ ?y'" proof assume "?x' = ?y'" moreover have "0 < p^a * k" using \prime p\ \n > 0\ n by (metis gr0I mult_is_0 power_not_zero prime_gt_0_nat) ultimately have "\x\ = \y\" by (intro power_eq_abs) with \x \ y\ have "x = -y" using abs_eq_iff by simp with \p dvd x - y\ have "p dvd 2*x" by simp with \prime p\ have "p dvd 2 \ p dvd x" by (metis int_dvd_int_iff of_nat_numeral prime_dvd_mult_iff prime_nat_int_transfer) with \p > 2\ have "p dvd x" by auto with \\ p dvd x\ show False.. qed moreover have "p^Suc a * k = p^a * k * p" by (simp add: ac_simps) ultimately show ?case using LTE.multiplicity_diff_self_pow[where x="?x'" and y="?y'", OF \prime p\] \p > 2\ and Suc.IH by (metis add_Suc_right power_mult) qed with n show ?thesis by metis qed end text \Theorem 2:\ corollary multiplicity_add_pow: fixes x y :: int and p n :: nat assumes "odd n" and "prime p" and "p > 2" and "p dvd x + y" and "\ p dvd x" "\ p dvd y" and "x \ -y" shows "multiplicity p (x^n + y^n) = multiplicity p (x + y) + multiplicity p n" proof - have [simp]: "(-y)^n = -(y^n)" using \odd n\ by (rule power_minus_odd) moreover have "n > 0" using \odd n\ by presburger with assms show ?thesis using multiplicity_diff_pow[where x=x and y="-y" and n=n] by simp qed section \The \p = 2\ case\ text \Theorem 3:\ theorem multiplicity_2_diff_pow_4div: fixes x y :: int assumes "odd x" "odd y" and "4 dvd x - y" and "n > 0" "x \ y" shows "multiplicity 2 (x^n - y^n) = multiplicity 2 (x - y) + multiplicity 2 n" proof - have "prime (2::nat)" by simp then obtain k where n: "n = 2^multiplicity 2 n * k" and "\ 2 dvd k" using \n > 0\ by (metis neq0_conv not_prime_unit multiplicity_decompose') have pow2: "multiplicity 2 (x^(2^k) - y^(2^k)) = multiplicity 2 (x - y) + k" for k proof (induction k) case (Suc k) have "x^(2^Suc k) - y^(2^Suc k) = (x^2^k)^2 - (y^2^k)^2" by (simp flip: power_mult algebra_simps) also have "... = (x^2^k - y^2^k)*(x^2^k + y^2^k)" by (simp add: power2_eq_square algebra_simps) finally have factor: "x^(2^Suc k) - y^(2^Suc k) = (x^2^k - y^2^k)*(x^2^k + y^2^k)". moreover have m_plus: "multiplicity 2 (x^2^k + y^2^k) = 1" proof (rule multiplicity_eqI) show "2^1 dvd x^2^k + y^2^k" using \odd x\ and \odd y\ by simp have "[x^2^k + y^2^k = 2] (mod 4)" proof (cases k) case 0 from \odd y\ have "[y = 1] (mod 2)" using cong_def by fastforce hence "[2*y = 2] (mod 4)" using cong_scale[where k=2 and b=1 and c=2, simplified] by force moreover from \4 dvd x - y\ have "[x - y = 0] (mod 4)" by (simp add: cong_0_iff) ultimately have "[x + y = 2] (mod 4)" - by (smt cong_add) + by (metis add.commute assms(3) cong_add_lcancel cong_iff_dvd_diff cong_trans mult_2) with \k = 0\ show ?thesis by simp next case (Suc k') then have "[x^2^k = 1] (mod 4)" and "[y^2^k = 1] (mod 4)" using \odd x\ \odd y\ by (auto simp add: power_mult power_Suc2 simp del: power_Suc intro: odd_square_mod_4) thus "[x^2^k + y^2^k = 2] (mod 4)" - by (smt cong_add) + using cong_add by fastforce qed thus "\ 2^Suc 1 dvd x^2^k + y^2^k" by (simp add: cong_dvd_iff) qed moreover have "x^2^k + y^2^k \ 0" using m_plus multiplicity_zero by auto moreover have "x^2^k - y^2^k \ 0" proof assume "x^2^k - y^2^k = 0" then have "\x\ = \y\" by (intro power_eq_abs, simp, simp) hence "x = y \ x = -y" using abs_eq_iff by auto with \x \ y\ have "x = -y" by simp with \4 dvd x - y\ have "4 dvd 2*x" by simp hence "2 dvd x" by auto with \odd x\ show False.. qed ultimately have "multiplicity 2 (x^2^Suc k - y^2^Suc k) = multiplicity 2 (x^2^k - y^2^k) + multiplicity 2 (x^2^k + y^2^k)" by (unfold factor; intro prime_elem_multiplicity_mult_distrib; auto) then show ?case using m_plus Suc.IH by simp qed simp moreover have even_diff: "int 2 dvd x^2^multiplicity 2 n - y^2^multiplicity 2 n" using \odd x\ and \odd y\ by simp moreover have odd_parts: "\ int 2 dvd x^2^multiplicity 2 n" "\ int 2 dvd y^2^multiplicity 2 n" using \odd x\ and \odd y\ by simp+ moreover have coprime: "coprime 2 k" using \\ 2 dvd k\ by simp show ?thesis apply (subst (1) n) apply (subst (2) n) apply (simp only: power_mult) apply (simp only: multiplicity_diff_pow_coprime[OF \prime 2\ even_diff odd_parts coprime, simplified]) by (rule pow2) qed text \Theorem 4:\ theorem multiplicity_2_diff_even_pow: fixes x y :: int assumes "odd x" "odd y" and "even n" and "n > 0" and "\x\ \ \y\" shows "multiplicity 2 (x^n - y^n) = multiplicity 2 (x - y) + multiplicity 2 (x + y) + multiplicity 2 n - 1" proof - obtain n' where "n = 2*n'" using \even n\ by auto with \n > 0\ have "n' > 0" by simp moreover have "4 dvd x^2 - y^2" proof - have "x^2 - y^2 = (x + y) * (x - y)" by (simp add: algebra_simps power2_eq_square) moreover have "2 dvd x + y" and "2 dvd x - y" using \odd x\ and \odd y\ by auto ultimately show "4 dvd x^2 - y^2" by fastforce qed moreover have "odd (x^2)" and "odd (y^2)" using \odd x\ \odd y\ by auto moreover from \\x\ \ \y\\ have "x^2 \ y^2" using diff_0 diff_0_right power2_eq_iff by fastforce ultimately have "multiplicity 2 ((x^2)^n' - (y^2)^n') = multiplicity 2 (x^2 - y^2) + multiplicity 2 n'" by (intro multiplicity_2_diff_pow_4div) also have "multiplicity 2 ((x^2)^n' - (y^2)^n') = multiplicity 2 (x^n - y^n)" unfolding \n = 2*n'\ by (simp add: power_mult) also have "multiplicity 2 (x^2 - y^2) = multiplicity 2 ((x - y) * (x + y))" by (simp add: algebra_simps power2_eq_square) also have "... = multiplicity 2 (x - y) + multiplicity 2 (x + y)" using \\x\ \ \y\\ by (auto intro: prime_elem_multiplicity_mult_distrib) also have "multiplicity 2 n = Suc (multiplicity 2 n')" unfolding \n = 2*n'\ using \n' > 0\ by (simp add: multiplicity_times_same) ultimately show ?thesis by simp qed end \ No newline at end of file diff --git a/thys/Stellar_Quorums/Stellar_Quorums.thy b/thys/Stellar_Quorums/Stellar_Quorums.thy --- a/thys/Stellar_Quorums/Stellar_Quorums.thy +++ b/thys/Stellar_Quorums/Stellar_Quorums.thy @@ -1,613 +1,612 @@ text \This theory formalizes some of the results appearing in the paper "Stellar Consensus By Reduction"\<^cite>\"disc_paper"\. We prove static properties of personal Byzantine quorum systems and Stellar quorum systems.\ theory Stellar_Quorums imports Main begin section "Personal Byzantine quorum systems" locale personal_quorums = fixes quorum_of :: "'node \ 'node set \ bool" assumes quorum_assm:"\ p p' . \quorum_of p Q; p' \ Q\ \ quorum_of p' Q" \ \In other words, a quorum (of some participant) is a quorum of all its members.\ begin definition blocks where \ \Set @{term R} blocks participant @{term p}.\ "blocks R p \ \ Q . quorum_of p Q \ Q \ R \ {}" abbreviation blocked_by where "blocked_by R \ {p . blocks R p}" lemma blocked_blocked_subset_blocked: "blocked_by (blocked_by R) \ blocked_by R" proof - have False if "p \ blocked_by (blocked_by R)" and "p \ blocked_by R" for p proof - have "Q \ blocked_by R \ {}" if "quorum_of p Q" for Q using \p \ blocked_by (blocked_by R)\ that unfolding blocks_def by auto have "Q \ R \ {}" if " quorum_of p Q" for Q proof - obtain p' where "p' \ blocked_by R" and "p' \ Q" by (meson Int_emptyI \\Q. quorum_of p Q \ Q \ blocked_by R \ {}\ \quorum_of p Q\) hence "quorum_of p' Q" using quorum_assm that by blast with \p' \ blocked_by R\ show "Q \ R \ {}" using blocks_def by auto qed hence "p \ blocked_by R" by (simp add: blocks_def) thus False using that(2) by auto qed thus "blocked_by (blocked_by R) \ blocked_by R" by blast qed end text \We now add the set of correct participants to the model.\ locale with_w = personal_quorums quorum_of for quorum_of :: "'node \ 'node set \ bool" + fixes W::"'node set" \ \@{term W} is the set of correct participants\ begin abbreviation B where "B \ -W" \ \@{term B} is the set of malicious participants.\ definition quorum_of_set where "quorum_of_set S Q \ \ p \ S . quorum_of p Q" subsection "The set of participants not blocked by malicious participants" definition L where "L \ W - (blocked_by B)" lemma l2: "p \ L \ \ Q \ W. quorum_of p Q" unfolding L_def blocks_def using DiffD2 by auto lemma l3: \ \If a participant is not blocked by the malicious participants, then it has a quorum consisting exclusively of correct participants which are not blocked by the malicious participants.\ assumes "p \ L" shows "\ Q \ L . quorum_of p Q" proof - have False if "\ Q . quorum_of p Q \ Q \ (-L) \ {}" proof - obtain Q where "quorum_of p Q" and "Q \ W" using l2 \p \ L\ by auto have "Q \ (-L) \ {}" using that \quorum_of p Q\ by simp obtain p' where "p' \ Q \ (-L)" and "quorum_of p' Q" using \Q \ - L \ {}\ \quorum_of p Q\ inf.left_idem quorum_assm by fastforce hence "Q \ B \ {}" unfolding L_def using CollectD Compl_Diff_eq Int_iff inf_le1 personal_quorums.blocks_def personal_quorums_axioms subset_empty by fastforce thus False using \Q \ W\ by auto qed thus ?thesis by (metis disjoint_eq_subset_Compl double_complement) qed subsection "Consensus clusters and intact sets" definition is_intertwined where \ \This definition is not used in this theory, but we include it to formalize the notion of intertwined set appearing in the DISC paper.\ "is_intertwined S \ S \ W \ (\ Q Q' . quorum_of_set S Q \ quorum_of_set S Q' \ W \ Q \ Q' \ {})" definition is_cons_cluster where \ \Consensus clusters\ "is_cons_cluster C \ C \ W \ (\ p \ C . \ Q \ C . quorum_of p Q) \ (\ Q Q' . quorum_of_set C Q \ quorum_of_set C Q' \ W \ Q \ Q' \ {})" definition strong_consensus_cluster where "strong_consensus_cluster I \ I \ W \ (\ p \ I . \ Q \ I . quorum_of p Q) \ (\ Q Q' . quorum_of_set I Q \ quorum_of_set I Q' \ I \ Q \ Q' \ {})" lemma strong_consensus_cluster_imp_cons_cluster: \ \Every intact set is a consensus cluster\ shows "strong_consensus_cluster I \ is_cons_cluster I" unfolding strong_consensus_cluster_def is_cons_cluster_def by blast lemma cons_cluster_neq_cons_cluster: \ \Some consensus clusters are not strong consensus clusters and have no superset that is a strong consensus cluster.\ shows "is_cons_cluster I \ (\ J . I \ J \ \strong_consensus_cluster J)" nitpick[falsify=false, card 'node=3, expect=genuine] oops text \Next we show that the union of two consensus clusters that intersect is a consensus cluster.\ theorem cluster_union: assumes "is_cons_cluster C\<^sub>1" and "is_cons_cluster C\<^sub>2" and "C\<^sub>1 \ C\<^sub>2 \ {}" shows "is_cons_cluster (C\<^sub>1\ C\<^sub>2)" proof - have "C\<^sub>1 \ C\<^sub>2 \ W" using assms(1) assms(2) is_cons_cluster_def by auto moreover have "\ p \ (C\<^sub>1\C\<^sub>2) . \ Q \ (C\<^sub>1\C\<^sub>2) . quorum_of p Q" using \is_cons_cluster C\<^sub>1\ \is_cons_cluster C\<^sub>2\ unfolding is_cons_cluster_def by (meson UnE le_supI1 le_supI2) moreover have "W \ Q\<^sub>1 \ Q\<^sub>2 \ {}" if "quorum_of_set (C\<^sub>1\C\<^sub>2) Q\<^sub>1" and "quorum_of_set (C\<^sub>1\C\<^sub>2) Q\<^sub>2" for Q\<^sub>1 Q\<^sub>2 proof - have "W \ Q\<^sub>1 \ Q\<^sub>2 \ {}" if "quorum_of_set C Q\<^sub>1" and "quorum_of_set C Q\<^sub>2" and "C = C\<^sub>1 \ C = C\<^sub>2" for C using \is_cons_cluster C\<^sub>1\ \is_cons_cluster C\<^sub>2\ \quorum_of_set (C\<^sub>1\C\<^sub>2) Q\<^sub>1\ \quorum_of_set (C\<^sub>1\C\<^sub>2) Q\<^sub>2\ that unfolding quorum_of_set_def is_cons_cluster_def by metis moreover have \W \ Q\<^sub>1 \ Q\<^sub>2 \ {}\ if "is_cons_cluster C\<^sub>1" and "is_cons_cluster C\<^sub>2" and "C\<^sub>1 \ C\<^sub>2 \ {}" and "quorum_of_set C\<^sub>1 Q\<^sub>1" and "quorum_of_set C\<^sub>2 Q\<^sub>2" for C\<^sub>1 C\<^sub>2 \ \We generalize to avoid repeating the argument twice\ proof - obtain p Q where "quorum_of p Q" and "p \ C\<^sub>1 \ C\<^sub>2" and "Q \ C\<^sub>2" using \C\<^sub>1 \ C\<^sub>2 \ {}\ \is_cons_cluster C\<^sub>2\ unfolding is_cons_cluster_def by blast have "Q \ Q\<^sub>1 \ {}" using \is_cons_cluster C\<^sub>1\ \quorum_of_set C\<^sub>1 Q\<^sub>1\ \quorum_of p Q\ \p \ C\<^sub>1 \ C\<^sub>2\ unfolding is_cons_cluster_def quorum_of_set_def by (metis Int_assoc Int_iff inf_bot_right) hence "quorum_of_set C\<^sub>2 Q\<^sub>1" using \Q \ C\<^sub>2\ \quorum_of_set C\<^sub>1 Q\<^sub>1\ quorum_assm unfolding quorum_of_set_def by blast thus "W \ Q\<^sub>1 \ Q\<^sub>2 \ {}" using \is_cons_cluster C\<^sub>2\ \quorum_of_set C\<^sub>2 Q\<^sub>2\ unfolding is_cons_cluster_def by blast qed ultimately show ?thesis using assms that unfolding quorum_of_set_def by auto qed ultimately show ?thesis using assms unfolding is_cons_cluster_def by simp qed text \Similarly, the union of two strong consensus clusters is a strong consensus cluster.\ lemma strong_cluster_union: assumes "strong_consensus_cluster C\<^sub>1" and "strong_consensus_cluster C\<^sub>2" and "C\<^sub>1 \ C\<^sub>2 \ {}" shows "strong_consensus_cluster (C\<^sub>1\ C\<^sub>2)" proof - have "C\<^sub>1 \ C\<^sub>2 \ W" using assms(1) assms(2) strong_consensus_cluster_def by auto moreover have "\ p \ (C\<^sub>1\C\<^sub>2) . \ Q \ (C\<^sub>1\C\<^sub>2) . quorum_of p Q" using \strong_consensus_cluster C\<^sub>1\ \strong_consensus_cluster C\<^sub>2\ unfolding strong_consensus_cluster_def by (meson UnE le_supI1 le_supI2) moreover have "(C\<^sub>1\C\<^sub>2) \ Q\<^sub>1 \ Q\<^sub>2 \ {}" if "quorum_of_set (C\<^sub>1\C\<^sub>2) Q\<^sub>1" and "quorum_of_set (C\<^sub>1\C\<^sub>2) Q\<^sub>2" for Q\<^sub>1 Q\<^sub>2 proof - have "C \ Q\<^sub>1 \ Q\<^sub>2 \ {}" if "quorum_of_set C Q\<^sub>1" and "quorum_of_set C Q\<^sub>2" and "C = C\<^sub>1 \ C = C\<^sub>2" for C using \strong_consensus_cluster C\<^sub>1\ \strong_consensus_cluster C\<^sub>2\ that unfolding quorum_of_set_def strong_consensus_cluster_def by metis hence "(C\<^sub>1\C\<^sub>2) \ Q\<^sub>1 \ Q\<^sub>2 \ {}" if "quorum_of_set C Q\<^sub>1" and "quorum_of_set C Q\<^sub>2" and "C = C\<^sub>1 \ C = C\<^sub>2" for C by (metis Int_Un_distrib2 disjoint_eq_subset_Compl sup.boundedE that) moreover have \(C\<^sub>1\C\<^sub>2) \ Q\<^sub>1 \ Q\<^sub>2 \ {}\ if "strong_consensus_cluster C\<^sub>1" and "strong_consensus_cluster C\<^sub>2" and "C\<^sub>1 \ C\<^sub>2 \ {}" and "quorum_of_set C\<^sub>1 Q\<^sub>1" and "quorum_of_set C\<^sub>2 Q\<^sub>2" for C\<^sub>1 C\<^sub>2 \ \We generalize to avoid repeating the argument twice\ proof - obtain p Q where "quorum_of p Q" and "p \ C\<^sub>1 \ C\<^sub>2" and "Q \ C\<^sub>2" using \C\<^sub>1 \ C\<^sub>2 \ {}\ \strong_consensus_cluster C\<^sub>2\ unfolding strong_consensus_cluster_def by blast have "Q \ Q\<^sub>1 \ {}" using \strong_consensus_cluster C\<^sub>1\ \quorum_of_set C\<^sub>1 Q\<^sub>1\ \quorum_of p Q\ \p \ C\<^sub>1 \ C\<^sub>2\ unfolding strong_consensus_cluster_def quorum_of_set_def by (metis Int_assoc Int_iff inf_bot_right) hence "quorum_of_set C\<^sub>2 Q\<^sub>1" using \Q \ C\<^sub>2\ \quorum_of_set C\<^sub>1 Q\<^sub>1\ quorum_assm unfolding quorum_of_set_def by blast thus "(C\<^sub>1\C\<^sub>2) \ Q\<^sub>1 \ Q\<^sub>2 \ {}" using \strong_consensus_cluster C\<^sub>2\ \quorum_of_set C\<^sub>2 Q\<^sub>2\ unfolding strong_consensus_cluster_def by blast qed ultimately show ?thesis using assms that unfolding quorum_of_set_def by auto qed ultimately show ?thesis using assms unfolding strong_consensus_cluster_def by simp qed end section "Stellar quorum systems" locale stellar = fixes slices :: "'node \ 'node set set" \ \the quorum slices\ and W :: "'node set" \ \the well-behaved nodes\ assumes slices_ne:"\p . p \ W \ slices p \ {}" begin definition quorum where "quorum Q \ \ p \ Q \ W . (\ Sl \ slices p . Sl \ Q)" definition quorum_of where "quorum_of p Q \ quorum Q \ (p \ W \ (\ Sl \ slices p . Sl \ Q))" \ \TODO: @{term "p\W"} needed?\ lemma quorum_union:"quorum Q \ quorum Q' \ quorum (Q \ Q')" unfolding quorum_def by (metis IntE Int_iff UnE inf_sup_aci(1) sup.coboundedI1 sup.coboundedI2) lemma l1: assumes "\ p . p \ S \ \ Q \ S . quorum_of p Q" and "p\ S" shows "quorum_of p S" using assms unfolding quorum_of_def quorum_def by (meson Int_iff subset_trans) lemma is_pbqs: assumes "quorum_of p Q" and "p' \ Q" shows "quorum_of p' Q" \ \This is the property required of a PBQS.\ using assms by (simp add: quorum_def quorum_of_def) interpretation with_w quorum_of \ \Stellar quorums form a personal quorum system.\ unfolding with_w_def personal_quorums_def quorum_def quorum_of_def by simp lemma quorum_is_quorum_of_some_slice: assumes "quorum_of p Q" and "p \ W" obtains S where "S \ slices p" and "S \ Q" and "\ p' . p' \ S \ W \ quorum_of p' Q" using assms unfolding quorum_def quorum_of_def by fastforce lemma "is_cons_cluster C \ quorum C" \ \Every consensus cluster is a quorum.\ unfolding is_cons_cluster_def by (metis inf.order_iff l1 quorum_of_def stellar.quorum_def stellar_axioms) subsection \Properties of blocking sets\ inductive blocking_min where \ \This is the set of correct participants that are eventually blocked by a set @{term R} when byzantine processors do not take steps.\ "\p \ W; \ Sl \ slices p . \ q \ Sl\W . q \ R \ blocking_min R q\ \ blocking_min R p" inductive_cases blocking_min_elim:"blocking_min R p" inductive blocking_max where \ \This is the set of participants that are eventually blocked by a set @{term R} when byzantine processors help epidemic propagation.\ "\p \ W; \ Sl \ slices p . \ q \ Sl . q \ R\B \ blocking_max R q\ \ blocking_max R p" inductive_cases "blocking_max R p" text \Next we show that if @{term \R\} blocks @{term \p\} and @{term p} belongs to a consensus cluster @{term S}, then @{term \R \ S \ {}\}.\ text \We first prove two auxiliary lemmas:\ lemma cons_cluster_wb:"p \ C \ is_cons_cluster C \ p\W" using is_cons_cluster_def by fastforce lemma cons_cluster_has_ne_slices: assumes "is_cons_cluster C" and "p\C" and "Sl \ slices p" shows "Sl \ {}" using assms unfolding is_cons_cluster_def quorum_of_set_def quorum_of_def quorum_def by (metis empty_iff inf_bot_left inf_bot_right subset_refl) lemma cons_cluster_has_cons_cluster_slice: assumes "is_cons_cluster C" and "p\C" obtains Sl where "Sl \ slices p" and "Sl \ C" using assms unfolding is_cons_cluster_def quorum_of_set_def quorum_of_def quorum_def by (metis Int_commute empty_iff inf.order_iff inf_bot_right le_infI1) theorem blocking_max_intersects_intact: \ \if @{term \R\} blocks @{term \p\} when malicious participants help epidemic propagation, and @{term p} belongs to a consensus cluster @{term C}, then @{term \R \ C \ {}\}\ assumes "blocking_max R p" and "is_cons_cluster C" and "p \ C" shows "R \ C \ {}" using assms proof (induct) case (1 p R) obtain Sl where "Sl \ slices p" and "Sl \ C" using cons_cluster_has_cons_cluster_slice using "1.prems" by blast moreover have "Sl \ W" using assms(2) calculation(2) is_cons_cluster_def by auto ultimately show ?case using "1.hyps" assms(2) by fastforce qed text \Now we show that if @{term \p \ C\}, @{term C} is a consensus cluster, and quorum @{term Q} is such that @{term \Q \ C \ {}\}, then @{term \Q \ W\} blocks @{term p}. We start by defining the set of participants reachable from a participant through correct participants. Their union trivially forms a quorum. Moreover, if @{term p} is not blocked by a set @{term R}, then we show that the set of participants reachable from @{term p} and not blocked by @{term R} forms a quorum disjoint from @{term R}. It follows that if @{term p } is a member of a consensus cluster @{term C} and @{term Q} is a quorum of a member of @{term C}, then @{term "Q\W"} must block @{term p}, as otherwise quorum intersection would be violated. \ inductive not_blocked for p R where "\Sl \ slices p; \ q \ Sl\W . q \ R \ \blocking_min R q; q \ Sl\ \ not_blocked p R q" | "\not_blocked p R p'; p' \ W; Sl \ slices p'; \ q \ Sl\W . q \ R \ \blocking_min R q; q \ Sl\ \ not_blocked p R q" inductive_cases not_blocked_cases:"not_blocked p R q" lemma l4: fixes Q p R defines "Q \ {q . not_blocked p R q}" shows "quorum Q" proof - have "\ S \ slices n . S \ Q" if "n\Q\W" for n proof- have "not_blocked p R n" using assms that by blast hence "n \ R" and "\blocking_min R n" by (metis Int_iff not_blocked.simps that)+ thus ?thesis using blocking_min.intros not_blocked.intros(2) that unfolding Q_def by (simp; metis mem_Collect_eq subsetI) qed thus ?thesis by (simp add: quorum_def) qed lemma l5: fixes Q p R defines "Q \ {q . not_blocked p R q}" assumes "\blocking_min R p" and \p\C\ and \is_cons_cluster C\ shows "quorum_of p Q" proof - have "p\W" using assms(3,4) cons_cluster_wb by blast obtain Sl where "Sl \ slices p" and "\ q \ Sl\W . q \ R \ \blocking_min R q" by (meson \p \ W\ assms(2) blocking_min.intros) hence "Sl \ Q" unfolding Q_def using not_blocked.intros(1) by blast with l4 \Sl \ slices p\ show "quorum_of p Q" using Q_def quorum_of_def by blast qed lemma cons_cluster_ne_slices: assumes "is_cons_cluster C" and "p\C" and "Sl \ slices p" shows "Sl\{}" using assms cons_cluster_has_ne_slices cons_cluster_wb stellar.quorum_of_def stellar_axioms by fastforce lemma l6: fixes Q p R defines "Q \ {q . not_blocked p R q}" shows "Q \ R \ W = {}" proof - have "q \ R" if "not_blocked p R q" and "q\ W" for q using that by (metis Int_iff not_blocked.simps) thus ?thesis unfolding Q_def by auto qed theorem quorum_blocks_cons_cluster: assumes "quorum_of_set C Q" and "p\C" and "is_cons_cluster C" shows "blocking_min (Q \ W) p" proof (rule ccontr) assume "\ blocking_min (Q \ W) p" have "p\W" using assms(2,3) is_cons_cluster_def by auto define Q' where "Q' \ {q . not_blocked p (Q\W) q}" have "quorum_of p Q'" using Q'_def \\ blocking_min (Q \ W) p\ assms(2) assms(3) l5(1) by blast moreover have "Q' \ Q \ W = {}" using Q'_def l6 by fastforce ultimately show False using assms unfolding is_cons_cluster_def by (metis Int_commute inf_sup_aci(2) quorum_of_set_def) qed subsection \Reachability through a set\ text \Here we define the part of a quorum @{term Q} of @{term p} that is reachable through correct participants from @{term p}. We show that if @{term p} and @{term p'} are members of the same consensus cluster and @{term Q} is a quorum of @{term p} and @{term Q'} is a quorum of @{term p'}, then the intersection @{term "Q\Q'\W"} is reachable from both @{term p} and @{term p'} through the consensus cluster.\ inductive reachable_through for p S where "reachable_through p S p" | "\reachable_through p S p'; p' \ W; Sl \ slices p'; Sl \ S; p'' \ Sl\ \ reachable_through p S p''" definition truncation where "truncation p S \ {p' . reachable_through p S p'}" lemma l13: assumes "quorum_of p Q" and "p \ W" and "reachable_through p Q p'" shows "quorum_of p' Q" using assms using quorum_assm reachable_through.cases by (metis is_pbqs subset_iff) lemma l14: assumes "quorum_of p Q" and "p \ W" shows "quorum (truncation p Q)" proof - have "\ S \ slices p' . \ q \ S . reachable_through p Q q" if "reachable_through p Q p'" and "p' \ W" for p' by (meson assms l13 quorum_is_quorum_of_some_slice stellar.reachable_through.intros(2) stellar_axioms that) thus ?thesis by (metis IntE mem_Collect_eq stellar.quorum_def stellar_axioms subsetI truncation_def) qed lemma l15: assumes "is_cons_cluster I" and "quorum_of p Q" and "quorum_of p' Q'" and "p \ I" and "p' \ I" and "Q \ Q' \ W \ {}" shows "W \ (truncation p Q) \ (truncation p' Q') \ {}" proof - have "quorum (truncation p Q)" and "quorum (truncation p' Q')" using l14 assms is_cons_cluster_def by auto moreover have "quorum_of_set I (truncation p Q)" and "quorum_of_set I (truncation p' Q')" by (metis IntI assms(4,5) calculation mem_Collect_eq quorum_def quorum_of_def quorum_of_set_def reachable_through.intros(1) truncation_def)+ moreover note \is_cons_cluster I\ ultimately show ?thesis unfolding is_cons_cluster_def by auto qed end subsection "Elementary quorums" text \In this section we define the notion of elementary quorum, which is a quorum that has no strict subset that is a quorum. It follows directly from the definition that every finite quorum contains an elementary quorum. Moreover, we show that if @{term Q} is an elementary quorum and @{term n\<^sub>1} and @{term n\<^sub>2} are members of @{term Q}, then @{term n\<^sub>2} is reachable from @{term n\<^sub>1} in the directed graph over participants defined as the set of edges @{term "(n,m)"} such that @{term m} is a member of a slice of @{term n}. This lemma is used in the companion paper to show that probabilistic leader-election is feasible.\ locale elementary = stellar begin definition elementary where "elementary s \ quorum s \ (\ s' . s' \ s \ \quorum s')" lemma finite_subset_wf: shows "wf {(X, Y). X \ Y \ finite Y}" by (metis finite_psubset_def wf_finite_psubset) lemma quorum_contains_elementary: assumes "finite s" and "\ elementary s" and "quorum s" shows "\ s' . s' \ s \ elementary s'" using assms proof (induct s rule:wf_induct[where ?r="{(X, Y). X \ Y \ finite Y}"]) case 1 then show ?case using finite_subset_wf by simp next case (2 x) then show ?case by (metis (full_types) elementary_def finite_psubset_def finite_subset in_finite_psubset less_le psubset_trans) qed inductive path where "path []" | "\ x . path [x]" | "\ l n . \path l; S \ Q (hd l); n \ S\ \ path (n#l)" theorem elementary_connected: assumes "elementary s" and "n\<^sub>1 \ s" and "n\<^sub>2 \ s" and "n\<^sub>1 \ W" and "n\<^sub>2 \ W" shows "\ l . hd (rev l) = n\<^sub>1 \ hd l = n\<^sub>2 \ path l" (is ?P) proof - { assume "\?P" define x where "x \ {n \ s . \ l . l \ [] \ hd (rev l) = n\<^sub>1 \ hd l = n \ path l}" have "n\<^sub>2 \ x" using \\?P\ x_def by auto have "n\<^sub>1 \ x" unfolding x_def using assms(2) path.intros(2) by force have "quorum x" proof - { fix n assume "n \ x" have "\ S . S \ slices n \ S \ x" proof - obtain S where "S \ slices n" and "S \ s" using \elementary s\ \n \ x\ unfolding x_def by (force simp add:elementary_def quorum_def) have "S \ x" proof - { assume "\ S \ x" obtain m where "m \ S" and "m \ x" using \\ S \ x\ by auto obtain l' where "hd (rev l') = n\<^sub>1" and "hd l' = n" and "path l'" and "l' \ []" using \n \ x\ x_def by blast have "path (m # l')" using \path l'\ \m\ S\ \S \ slices n\ \hd l' = n\ using path.intros(3) by fastforce moreover have "hd (rev (m # l')) = n\<^sub>1" using \hd (rev l') = n\<^sub>1\ \l' \ []\ by auto ultimately have "m \ x" using \m \ S\ \S \ s\ x_def by auto hence False using \m \ x\ by blast } thus ?thesis by blast qed thus ?thesis using \S \ slices n\ by blast qed } thus ?thesis by (meson Int_iff quorum_def) qed moreover have "x \ s" using \n\<^sub>2 \ x\ assms(3) x_def by blast ultimately have False using \elementary s\ using elementary_def by auto } thus ?P by blast qed end subsection \The intact sets of the Stellar Whitepaper\ definition project where "project slices S n \ {Sl \ S | Sl . Sl \ slices n}" \ \Projecting on @{term S} is the same as deleting the complement of @{term S}, where deleting is understood as in the Stellar Whitepaper.\ subsubsection \Intact and the Cascade Theorem\ locale intact = \ \Here we fix an intact set @{term I} and prove the cascade theorem.\ orig:stellar slices W + proj:stellar "project slices I" W \ \We consider the projection of the system on @{term I}.\ for slices W I + \ \An intact set is a set @{term I} satisfying the three assumptions below:\ assumes intact_wb:"I \ W" and q_avail:"orig.quorum I" \ \@{term I} is a quorum in the original system.\ and q_inter:"\ Q Q' . \proj.quorum Q; proj.quorum Q'; Q \ I \ {}; Q' \ I \ {}\ \ Q \ Q' \ I \ {}" \ \Any two sets that intersect @{term I} and that are quorums in the projected system intersect in @{term I}. Note that requiring that @{text \Q \ Q' \ {}\} instead of @{text \Q \ Q' \ I \ {}\} would be equivalent.\ begin theorem blocking_safe: \ \A set that blocks an intact node contains an intact node. If this were not the case, quorum availability would trivially be violated.\ fixes S n assumes "n\I" and "\ Sl\ slices n .Sl\S \ {}" shows "S \ I \ {}" using assms q_avail intact_wb unfolding orig.quorum_def by auto (metis inf.absorb_iff2 inf_assoc inf_bot_right inf_sup_aci(1)) theorem cascade: \ \If @{term U} is a quorum of an intact node and @{term S} is a super-set of @{term U}, then either @{term S} includes all intact nodes or there is an intact node outside of @{term S} which is blocked by the intact members of @{term S}. This shows that, in SCP, once the intact members of a quorum accept a statement, a cascading effect occurs and all intact nodes eventually accept it regardless of what befouled and faulty nodes do.\ fixes U S assumes "orig.quorum U" and "U \ I \ {}" and "U \ S" obtains "I \ S" | "\ n \ I - S . \ Sl \ slices n . Sl \ S \ I \ {}" proof - have False if 1:"\ n \ I - S . \ Sl \ slices n . Sl \ S \ I = {}" and 2:"\(I \ S)" proof - text \First we show that @{term \I-S\} is a quorum in the projected system. This is immediate from the definition of quorum and assumption 1.\ have "proj.quorum (I-S)" using 1 - unfolding proj.quorum_def project_def - by (auto; smt DiffI Diff_Compl Diff_Int_distrib Diff_eq Diff_eq_empty_iff Int_commute) + by (simp add: proj.quorum_def project_def) (metis DiffI IntE IntI empty_iff subsetI) text \Then we show that U is also a quorum in the projected system:\ moreover have "proj.quorum U" using \orig.quorum U\ unfolding proj.quorum_def orig.quorum_def project_def by (simp; meson Int_commute inf.coboundedI2) text \Since quorums of @{term I} must intersect, we get a contradiction:\ ultimately show False using \U \ S\ \U \ I \ {}\ \\(I\S)\ q_inter by auto qed thus ?thesis using that by blast qed end subsubsection "The Union Theorem" text \Here we prove that the union of two intact sets that intersect is intact. This implies that maximal intact sets are disjoint.\ locale intersecting_intact = i1:intact slices W I\<^sub>1 + i2:intact slices W I\<^sub>2 \ \We fix two intersecting intact sets @{term I\<^sub>1} and @{term I\<^sub>2}.\ + proj:stellar "project slices (I\<^sub>1\I\<^sub>2)" W \ \We consider the projection of the system on @{term \I\<^sub>1\I\<^sub>2\}.\ for slices W I\<^sub>1 I\<^sub>2 + assumes inter:"I\<^sub>1 \ I\<^sub>2 \ {}" begin theorem union_quorum: "i1.orig.quorum (I\<^sub>1\I\<^sub>2)" \ \@{term \I\<^sub>1\I\<^sub>2\} is a quorum in the original system.\ using i1.intact_axioms i2.intact_axioms unfolding intact_def stellar_def intact_axioms_def i1.orig.quorum_def by (metis Int_iff Un_iff le_supI1 le_supI2) theorem union_quorum_intersection: assumes "proj.quorum Q\<^sub>1" and "proj.quorum Q\<^sub>2" and "Q\<^sub>1 \ (I\<^sub>1\I\<^sub>2) \ {}" and "Q\<^sub>2 \ (I\<^sub>1\I\<^sub>2) \ {}" shows "Q\<^sub>1 \ Q\<^sub>2 \ (I\<^sub>1\I\<^sub>2) \ {}" \ \Any two sets that intersect @{term \I\<^sub>1\I\<^sub>2\} and that are quorums in the system projected on @{term \I\<^sub>1\I\<^sub>2\} intersect in @{term \I\<^sub>1\I\<^sub>2\}.\ proof - text \First we show that @{term Q\<^sub>1} and @{term Q\<^sub>2} are quorums in the projections on @{term I\<^sub>1} and @{term I\<^sub>2}.\ have "i1.proj.quorum Q\<^sub>1" using \proj.quorum Q\<^sub>1\ unfolding i1.proj.quorum_def proj.quorum_def project_def by auto (metis Int_Un_distrib Int_iff Un_subset_iff) moreover have "i2.proj.quorum Q\<^sub>2" using \proj.quorum Q\<^sub>2\ unfolding i2.proj.quorum_def proj.quorum_def project_def by auto (metis Int_Un_distrib Int_iff Un_subset_iff) moreover have "i2.proj.quorum Q\<^sub>1" using \proj.quorum Q\<^sub>1\ unfolding proj.quorum_def i2.proj.quorum_def project_def by auto (metis Int_Un_distrib Int_iff Un_subset_iff) moreover have "i1.proj.quorum Q\<^sub>2" using \proj.quorum Q\<^sub>2\ unfolding proj.quorum_def i1.proj.quorum_def project_def by auto (metis Int_Un_distrib Int_iff Un_subset_iff) text \Next we show that @{term Q\<^sub>1} and @{term Q\<^sub>2} intersect if they are quorums of, respectively, @{term I\<^sub>1} and @{term I\<^sub>2}. This is the only interesting part of the proof.\ moreover have "Q\<^sub>1 \ Q\<^sub>2 \ (I\<^sub>1\I\<^sub>2) \ {}" if "i1.proj.quorum Q\<^sub>1" and "i2.proj.quorum Q\<^sub>2" and "i2.proj.quorum Q\<^sub>1" and "Q\<^sub>1 \ I\<^sub>1 \ {}" and "Q\<^sub>2 \ I\<^sub>2 \ {}" for Q\<^sub>1 Q\<^sub>2 proof - have "i1.proj.quorum I\<^sub>2" proof - have "i1.orig.quorum I\<^sub>2" by (simp add: i2.q_avail) thus ?thesis unfolding i1.orig.quorum_def i1.proj.quorum_def project_def by auto (meson Int_commute Int_iff inf_le2 subset_trans) qed moreover note \i1.proj.quorum Q\<^sub>1\ ultimately have "Q\<^sub>1 \ I\<^sub>2 \ {}" using i1.q_inter inter \Q\<^sub>1 \ I\<^sub>1 \ {}\ by blast moreover note \i2.proj.quorum Q\<^sub>2\ moreover note \i2.proj.quorum Q\<^sub>1\ ultimately have "Q\<^sub>1 \ Q\<^sub>2 \ I\<^sub>2 \ {}" using i2.q_inter \Q\<^sub>2 \ I\<^sub>2 \ {}\ by blast thus ?thesis by (simp add: inf_sup_distrib1) qed text \Next we show that @{term Q\<^sub>1} and @{term Q\<^sub>2} intersect if they are quorums of the same intact set. This is obvious.\ moreover have "Q\<^sub>1 \ Q\<^sub>2 \ (I\<^sub>1\I\<^sub>2) \ {}" if "i1.proj.quorum Q\<^sub>1" and "i1.proj.quorum Q\<^sub>2" and "Q\<^sub>1 \ I\<^sub>1 \ {}" and "Q\<^sub>2 \ I\<^sub>1 \ {}" for Q\<^sub>1 Q\<^sub>2 by (simp add: Int_Un_distrib i1.q_inter that) moreover have "Q\<^sub>1 \ Q\<^sub>2 \ (I\<^sub>1\I\<^sub>2) \ {}" if "i2.proj.quorum Q\<^sub>1" and "i2.proj.quorum Q\<^sub>2" and "Q\<^sub>1 \ I\<^sub>2 \ {}" and "Q\<^sub>2 \ I\<^sub>2 \ {}" for Q\<^sub>1 Q\<^sub>2 by (simp add: Int_Un_distrib i2.q_inter that) text \Finally we have covered all the cases and get the final result:\ ultimately show ?thesis - by (smt Int_Un_distrib Int_commute assms(3,4) sup_bot.right_neutral) + by (smt (verit, best) Int_Un_distrib Int_commute assms(3) assms(4) sup_eq_bot_iff) qed end end diff --git a/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Substitutions.thy b/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Substitutions.thy --- a/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Substitutions.thy +++ b/thys/Sumcheck_Protocol/Generalized_Sumcheck_Protocol/Substitutions.thy @@ -1,104 +1,104 @@ (******************************************************************************* Project: Sumcheck Protocol Authors: Azucena Garvia Bosshard Christoph Sprenger, ETH Zurich Jonathan Bootle, IBM Research Europe *******************************************************************************) section \Substitutions\ theory Substitutions imports Main "HOL-Library.FuncSet" begin type_synonym ('v, 'a) subst = "'v \ 'a" definition substs :: "'v set \ 'a set \ ('v, 'a) subst set" where "substs V H = {\. dom \ = V \ ran \ \ H}" text \Small lemmas about the set of substitutions\ lemma substE [elim]: "\ \ \ substs V H; \ dom \ = V; ran \ \ H \ \ P \ \ P" by (simp add: substs_def) lemma substs_empty_dom [simp]: "substs {} H = {Map.empty}" by (auto simp add: substs_def) lemma substs_finite: "\ finite V; finite H \ \ finite (substs V H)" by (simp add: finite_set_of_finite_maps substs_def) lemma substs_nonempty: assumes "H \ {}" shows "substs V H \ {}" proof - obtain h where A1: "h \ H" using assms by(auto) obtain \ where A2: "\ = (\v. if v \ V then Some h else None)" by(simp) have "\ \ substs V H" using A1 A2 by(auto simp add: substs_def ran_def dom_def) then show ?thesis by(auto) qed lemma subst_dom: \\ \ \ substs V H; x \ V \ \ x \ dom \\ by(auto simp add: substs_def) lemma subst_add: assumes "x \ V" and "\ \ substs (V - {x}) H" and "a \ H" shows "\(x \ a) \ substs V H" using assms by(simp add: substs_def) (auto simp add: dom_def ran_def) lemma subst_im: assumes "x \ V" and "\ \ substs V H" shows "the (\ x) \ H" using assms by(auto simp add: substs_def dom_def ran_def) lemma subst_restr: assumes "x \ V" and "\ \ substs V H" shows "\ |` (dom \ - {x}) \ substs (V - {x}) H" using assms by(auto simp add: substs_def ran_def dom_def restrict_map_def) text \Bijection between sets of substitutions\ lemma restrict_map_dom: "\ |` dom \ = \" by (metis (no_types, lifting) domIff map_le_antisym map_le_def restrict_in restrict_out) lemma bij_betw_set_substs: assumes "x \ V" defines "f \ \(a, \::'v \ 'a). \(x \ a)" and "g \ \\::'v \ 'a. (the (\ x), \|`(dom \ - {x}))" shows "bij_betw f (H \ substs (V - {x}) H) (substs V H)" proof (intro bij_betwI) show "f \ H \ substs (V - {x}) H \ substs V H" using assms by(auto simp add: f_def subst_add) next show "g \ substs V H \ H \ substs (V - {x}) H" using assms by(auto simp add: g_def subst_im subst_restr) next fix xa assume "xa \ H \ substs (V - {x}) H" then show "g (f xa) = xa" using assms - by (smt (z3) Diff_empty Diff_insert0 Diff_insert_absorb SigmaE case_prod_conv - fun_upd_None_restrict fun_upd_same fun_upd_upd mk_disjoint_insert option.sel - restrict_map_dom subst_dom) + by (smt (verit, ccfv_threshold) Diff_insert_absorb SigmaE case_prod_conv domI + fun_upd_None_restrict fun_upd_same fun_upd_upd mk_disjoint_insert option.sel restrict_map_dom + subst_dom) next fix y assume "y \ substs V H" then show "f (g y) = y" using assms by(auto simp add: g_def f_def) (metis domIff fun_upd_restrict map_upd_triv option.exhaust_sel restrict_map_dom substE) qed end \ No newline at end of file