Mercurial > hg > Members > kono > Proof > ZF-in-agda

annotate filter.agda @ 265:9bf100ae50ac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
filter
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 30 Sep 2019 16:34:15 +0900
parents 650bdad56729
children 0d7d6e4da36f
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 open import Level
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
2 open import Ordinals
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
3 module filter {n : Level } (O : Ordinals {n}) where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
4
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import zf
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
6 open import logic
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
7 import OD
193
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 191
diff changeset
8
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import Relation.Nullary
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Relation.Binary
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Data.Empty
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open import Relation.Binary
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 open import Relation.Binary.Core
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 open import Relation.Binary.PropositionalEquality
191
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
15 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
16
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
17 open inOrdinal O
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
18 open OD O
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
19 open OD.OD
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20
236
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
21 open _∧_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
22 open _∨_
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
23 open Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 193
diff changeset
24
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
25 record Filter ( L : OD ) : Set (suc n) where
191
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
26 field
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
27 F1 : { p q : OD } → L ∋ p → od→ord p o< od→ord q → L ∋ q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
28 F2 : { p q : OD } → L ∋ p → L ∋ q → def L (minα (od→ord p ) (od→ord q ))
191
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
29
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
30 open Filter
191
9eb6a8691f02 choice function cannot jump between ordinal level
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 190
diff changeset
31
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
32 proper-filter : {L : OD} → Filter L → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
33 proper-filter {L} P = ¬ ( L ∋ od∅ )
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
35 prime-filter : {L : OD} → Filter L → {p q : OD } → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
36 prime-filter {L} P {p} {q} = def L ( maxα ( od→ord p ) (od→ord q )) → ( L ∋ p ) ∨ ( L ∋ q )
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
38 ultra-filter : {L : OD} → Filter L → {p : OD } → Set n
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
39 ultra-filter {L} P {p} = ( L ∋ p ) ∨ ( ¬ ( L ∋ p ))
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
41 -- H(ω,2) = Lower ( Lower ω ) = Def ( Def ω))
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42
265
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
43 postulate
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
44 dist-ord : {p q r : Ordinal } → minα p ( maxα q r ) ≡ maxα ( minα p q ) ( minα p r )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
45
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
46 filter-lemma1 : {L : OD} → (P : Filter L) → {p q : OD } → ( (p : OD) → ultra-filter {L} P {p} ) → prime-filter {L} P {p} {q}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 236
diff changeset
47 filter-lemma1 {L} P {p} {q} u lt = {!!}