Theory Sigma_Algebra

theory Sigma_Algebra
imports Main
(*  Title:      Sigma_Algebra.thy

    Author:     Stefan Richter, Markus Wenzel, TU Muenchen
    License:    LGPL

Changes for Accordance to Joe Hurd's conventions
and additions by Stefan Richter 2002
*)

subsection ‹Sigma algebras \label{sec:sigma}›

theory Sigma_Algebra imports Main begin

text ‹The $\isacommand {theory}$ command commences a formal document and enumerates the
  theories it depends on. With the ‹Main› theory, a standard
  selection of useful HOL theories excluding the real
  numbers is loaded. This theory includes and builds upon a tiny theory of the
  same name by Markus Wenzel. This theory as well as ‹Measure›
  in \ref{sec:measure-spaces} is heavily
  influenced by Joe Hurd's thesis \cite{hurd2002} and has been designed to keep the terminology as
  consistent as possible with that work.

  Sigma algebras are an elementary concept in measure
  theory. To measure --- that is to integrate --- functions, we first have
  to measure sets. Unfortunately, when dealing with a large universe,
  it is often not possible to consistently assign a measure to every
  subset. Therefore it is necessary to define the set of measurable
  subsets of the universe. A sigma algebra is such a set that has
  three very natural and desirable properties.›

definition
  sigma_algebra:: "'a set set ⇒ bool" where
  "sigma_algebra A ⟷
  {} ∈ A ∧ (∀a. a ∈ A ⟶ -a ∈ A) ∧
  (∀a. (∀ i::nat. a i ∈ A) ⟶ (⋃i. a i) ∈ A)"

text ‹
  The $\isacommand {definition}$ command defines new constants, which
  are just named functions in HOL. Mind that the third condition
  expresses the fact that the union of countably many sets in $A$ is
  again a set in $A$ without explicitly defining the notion of
  countability.

  Sigma algebras can naturally be created as the closure of any set of
  sets with regard to the properties just postulated. Markus Wenzel
  wrote the following
  inductive definition of the $\isa {sigma}$ operator.›


inductive_set
  sigma :: "'a set set ⇒ 'a set set"
  for A :: "'a set set"
  where
    basic: "a ∈ A ⟹ a ∈ sigma A"
  | empty: "{} ∈ sigma A"
  | complement: "a ∈ sigma A ⟹ -a ∈ sigma A"
  | Union: "(⋀i::nat. a i ∈ sigma A) ⟹ (⋃i. a i) ∈ sigma A"


text ‹He also proved the following basic facts. The easy proofs are omitted.
›

theorem sigma_UNIV: "UNIV ∈ sigma A"
(*<*)proof -
  have "{} ∈ sigma A" by (rule sigma.empty)
  hence "-{} ∈ sigma A" by (rule sigma.complement)
  also have "-{} = UNIV" by simp
  finally show ?thesis .
qed(*>*)


theorem sigma_Inter:
  "(⋀i::nat. a i ∈ sigma A) ⟹ (⋂i. a i) ∈ sigma A"
(*<*) proof -
  assume "⋀i::nat. a i ∈ sigma A"
  hence "⋀i::nat. -(a i) ∈ sigma A" by (rule sigma.complement)
  hence "(⋃i. -(a i)) ∈ sigma A" by (rule sigma.Union)
  hence "-(⋃i. -(a i)) ∈ sigma A" by (rule sigma.complement)
  also have "-(⋃i. -(a i)) = (⋂i. a i)" by simp
  finally show ?thesis .
qed(*>*)

text ‹It is trivial to show the connection between our first
  definitions. We use the opportunity to introduce the proof syntax.›


theorem assumes sa: "sigma_algebra A"
  ― ‹Named premises are introduced like this.›

  shows sigma_sigma_algebra: "sigma A = A"
proof

  txt ‹The $\isacommand {proof}$ command alone invokes a single standard rule to
    simplify the goal. Here the following two subgoals emerge.›

  show "A ⊆ sigma A"
    ― ‹The $\isacommand {show}$ command starts the proof of a subgoal.›

    by (auto simp add: sigma.basic)

  txt ‹This is easy enough to be solved by an automatic step,
    indicated by the keyword $\isacommand {by}$. The method $\isacommand {auto}$ is stated in parentheses, with attributes to it following.  In
    this case, the first introduction rule for the $\isacommand {sigma}$
    operator is given as an extra simplification rule.›

  show "sigma A ⊆ A"
  proof

    txt ‹Because this goal is not quite as trivial, another proof is
      invoked, delimiting a block as in a programming language.›

    fix x
    ― ‹A new named variable is introduced.›

    assume "x ∈ sigma A"

    txt ‹An assumption is made that must be justified by the current proof
      context. In this case the corresponding fact had been generated
      by a rule automatically invoked by the inner $\isacommand {proof}$
      command.›

    from this sa show "x ∈ A"

      txt ‹Named facts can explicitly be given to the proof methods using
        $\isacommand {from}$. A special name is ‹this›, which denotes
        current facts generated by the last command. Usually $\isacommand
        {from}$ ‹this sa› --- remember that ‹sa› is an assumption from above
        --- is abbreviated to $\isacommand {with}$ ‹sa›, but in this case the order of
        facts is relevant for the following method and $\isacommand
        {with}$
        would have put the current facts last.›

      by (induct rule: sigma.induct) (auto simp add: sigma_algebra_def)

    txt ‹Two methods may be carried out at $\isacommand {by}$. The first
      one applies induction here via the canonical rule generated by the
      inductive definition above, while the latter solves the
      resulting subgoals by an automatic step involving
      simplification.›

  qed
qed

text "These two steps finish their respective proofs, checking
  that all subgoals have been proven."

text ‹To end this theory we prove a special case of the ‹sigma_Inter› theorem above. It seems trivial that
  the fact holds for two sets as well as for countably many.
  We get a first taste of the cost of formal reasoning here, however. The
  idea must be made precise by exhibiting a concrete sequence of
  sets.›

primrec trivial_series:: "'a set ⇒ 'a set ⇒ (nat ⇒ 'a set)"
where
  "trivial_series a b 0 = a"
| "trivial_series a b (Suc n) = b"

text ‹Using $\isacommand {primrec}$, primitive recursive functions over
  inductively defined data types --- the natural numbers in this case ---
  may be constructed.›


theorem assumes s: "sigma_algebra A" and a: "a ∈ A" and b: "b ∈ A"
  shows sigma_algebra_inter: "a ∩ b ∈ A"
proof -
    ― ‹This form of $\isacommand {proof}$ foregoes the application of a rule.›

  have "a ∩ b = (⋂i::nat. trivial_series a b i)"

    txt ‹Intermediate facts that do not solve any subgoals yet are established this way.›

  proof (rule set_eqI)

    txt ‹The  $\isacommand {proof}$ command may also take one explicit method
      as an argument like the single rule application in this instance.›

    fix x

    {
      fix i
      assume "x ∈ a ∩ b"
      hence "x ∈ trivial_series a b i" by (cases i) auto
        ― ‹This is just an abbreviation for $\isacommand {"from this have"}$.›
    }

    txt ‹Curly braces can be used to explicitly delimit
      blocks. In conjunction with $\isacommand {fix}$, universal
      quantification over the fixed variable $i$ is achieved
      for the last statement in the block, which is exported to the
      enclosing block.›

    hence "x ∈ a ∩ b ⟹ ∀i. x ∈ trivial_series a b i"
      by fast
    also

    txt ‹The statement $\isacommand {also}$ introduces calculational
      reasoning. This basically amounts to collecting facts. With
      $\isacommand {also}$, the current fact is added to a special list of
      theorems called the calculation and
      an automatically selected transitivity rule
      is additionally applied from the second collected fact on.›

    { assume "⋀i. x ∈ trivial_series a b i"
      hence "x ∈ trivial_series a b 0" and "x ∈ trivial_series a b 1"
        by this+
      hence "x ∈ a ∩ b"
        by simp
    }
    hence "∀i. x ∈ trivial_series a b i ⟹ x ∈ a ∩ b"
      by blast

    ultimately have "x ∈ a ∩ b = (∀i::nat. x ∈ trivial_series a b i)" ..

    txt ‹The accumulated calculational facts including the current one
      are exposed to the next statement by  $\isacommand {ultimately}$ and
      the calculation list is then erased. The two dots after the
      statement here indicate proof by a single automatically
      selected rule.›

    also have "… =  (x ∈ (⋂i::nat. trivial_series a b i))"
      by simp
    finally show "x ∈ a ∩ b = (x ∈ (⋂i::nat. trivial_series a b i))" .

    txt ‹The $\isacommand {finally}$ directive behaves like $\isacommand {ultimately}$
      with the addition of a further transitivity rule application. A
      single dot stands for proof by assumption.›

  qed

  moreover have "(⋂i::nat. trivial_series a b i) ∈ A"
  proof -
    { fix i
      from a b have "trivial_series a b i ∈ A"
        by (cases i) auto
    }
    hence "⋀i. trivial_series a b i ∈ sigma A"
      by (simp only: sigma.basic)
    hence "(⋂i::nat. trivial_series a b i) ∈ sigma A"
      by (simp only: sigma_Inter)
    with s show ?thesis
      by (simp only: sigma_sigma_algebra)
  qed

  ultimately show ?thesis by simp
qed

text ‹Of course, a like theorem holds for union instead of
  intersection.  But as we will not need it in what follows, the
  theory is finished with the following easy properties instead.
  Note that the former is a kind of generalization of the last result and
  could be used to  shorten its proof. Unfortunately, this one was needed ---
  and therefore found --- only late in the development.
›

theorem sigma_INTER:
  assumes a:"(⋀i::nat. i ∈ S ⟹ a i ∈ sigma A)"
  shows "(⋂i∈S. a i) ∈ sigma A"(*<*)
proof -
  from a have "⋀i. (if i∈S then {} else UNIV) ∪ a i ∈ sigma A"
    by (simp add: sigma.intros sigma_UNIV)
  hence "(⋂i. (if i∈S then {} else UNIV) ∪ a i) ∈ sigma A"
    by (rule sigma_Inter)
  also have "(⋂i. (if i∈S then {} else UNIV) ∪ a i) = (⋂i∈S. a i)"
    by force
  finally show ?thesis .
qed(*>*)


lemma assumes s: "sigma_algebra a" shows sigma_algebra_UNIV: "UNIV ∈ a"(*<*)
proof -
  from s have "{}∈a" by (unfold sigma_algebra_def) blast
  with s show ?thesis by (unfold sigma_algebra_def) auto
qed(*>*)


end