Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison ODC.agda @ 279:197e0b3d39dc
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 09 May 2020 16:41:40 +0900 |
parents | d9d3654baee1 |
children | 5544f4921a44 |
comparison
equal
deleted
inserted
replaced
278:bfb5e807718b | 279:197e0b3d39dc |
---|---|
92 choice-func : (X : OD ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD | 92 choice-func : (X : OD ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD |
93 choice-func X {x} not X∋x = minimal x not | 93 choice-func X {x} not X∋x = minimal x not |
94 choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A | 94 choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A |
95 choice X {A} X∋A not = x∋minimal A not | 95 choice X {A} X∋A not = x∋minimal A not |
96 | 96 |
97 --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice | |
98 --- | |
99 record choiced ( X : OD) : Set (suc n) where | |
100 field | |
101 a-choice : OD | |
102 is-in : X ∋ a-choice | |
103 | |
104 choice-func' : (X : OD ) → (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X | |
105 choice-func' X p∨¬p not = have_to_find where | |
106 ψ : ( ox : Ordinal ) → Set (suc n) | |
107 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X | |
108 lemma-ord : ( ox : Ordinal ) → ψ ox | |
109 lemma-ord ox = TransFinite {ψ} induction ox where | |
110 ∋-p : (A x : OD ) → Dec ( A ∋ x ) | |
111 ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM | |
112 ∋-p A x | case1 (lift t) = yes t | |
113 ∋-p A x | case2 t = no (λ x → t (lift x )) | |
114 ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) } | |
115 → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B | |
116 ∀-imply-or {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) -- LEM | |
117 ∀-imply-or {A} {B} ∀AB | case1 (lift t) = case1 t | |
118 ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x (lift not ))) where | |
119 lemma : ¬ ((x : Ordinal ) → A x) → B | |
120 lemma not with p∨¬p B | |
121 lemma not | case1 b = b | |
122 lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b )) | |
123 induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x | |
124 induction x prev with ∋-p X ( ord→od x) | |
125 ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } ) | |
126 ... | no ¬p = lemma where | |
127 lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X | |
128 lemma1 y with ∋-p X (ord→od y) | |
129 lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } ) | |
130 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) ) | |
131 lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X | |
132 lemma = ∀-imply-or lemma1 | |
133 have_to_find : choiced X | |
134 have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where | |
135 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥) | |
136 ¬¬X∋x nn = not record { | |
137 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt) | |
138 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt ) | |
139 } | |
140 |