module AnInfiniteOmniscientSet where

-- By Martin Escardo, 2 September 2011.
--
-- This is a formal constructive proof in the sense of ML type theory,
-- written in Agda notation.
--
-- It is based on the author's paper 
--
---------------------------------------------------------------
--      Infinite sets that satisfy the principle of omniscience 
--      in all varieties of constructive mathematics
---------------------------------------------------------------
--
--      http://www.cs.bham.ac.uk/~mhe/papers/omniscient.pdf
--
--
-- to be presented at the Types'2011 meeting in Bergen, Norway,
-- September 8-11,
--
-- Theorem-3·6 of that paper is proved in the module
-- DrinkerParadox. This module derives the main corollary, the fact
-- that the infinite set ℕ∞, defined in the module
-- GenericConvergentSequence, satisfies the principle of omniscience.
--
----------------------------------------------------------------------
-- You can click at any word or symbol to navigate to the module that
-- defines it in the html rendering of this set of agda modules.
----------------------------------------------------------------------
--
-- The agda files are collected together at
--
--      http://www.cs.bham.ac.uk/~mhe/papers/omniscient.zip



open import Logic
open import Equality
open import Naturals
open import Two 
open import Cantor
open import GenericConvergentSequence
open import DrinkerParadox


Theorem[ℕ∞-is-omniscient] :
------------------------------------
  ∀(p : ₂ℕ  )  extensional p  
   ( \(x : ₂ℕ)  x  ℕ∞  p x  )
  (∀  (x : ₂ℕ)  x  ℕ∞  p x  )
------------------------------------
Theorem[ℕ∞-is-omniscient] p extensionality-of-p = 
 two-equality-cases case₀ case₁
 where e :  \(x : ₂ℕ)  x  ℕ∞  
              (p x    ∀(y : ₂ℕ)  y  ℕ∞  p y  )
       e = Theorem-3·6 p extensionality-of-p

       x : ₂ℕ
       x = ∃-witness e

       m : x  ℕ∞
       m = ∧-elim₀(∃-elim e)

       case₀ : p x    ( \(x : ₂ℕ)  x  ℕ∞  p x  )
                        (∀  (x : ₂ℕ)  x  ℕ∞  p x  )
       case₀ r = ∨-intro₀(∃-intro x (∧-intro m r))

       case₁ : p x    ( \(x : ₂ℕ)  x  ℕ∞  p x  )
                        (∀  (x : ₂ℕ)  x  ℕ∞  p x  )
       case₁ r = ∨-intro₁(∧-elim₁(∃-elim e) r)