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

annotate ODC.agda @ 276:6f10c47e4e7a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
separate choice fix sup-o
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 09 May 2020 09:02:52 +0900
parents OD.agda@29a85a427ed2
children d9d3654baee1
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
16
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 15
diff changeset
1 open import Level
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
2 open import Ordinals
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
3 module ODC {n : Level } (O : Ordinals {n} ) where
3
e7990ff544bf reocrd ZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
14
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
5 open import zf
23
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 22
diff changeset
6 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
14
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
7 open import Relation.Binary.PropositionalEquality
e11e95d5ddee separete constructible set
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 11
diff changeset
8 open import Data.Nat.Properties
6
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
9 open import Data.Empty
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
10 open import Relation.Nullary
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
11 open import Relation.Binary
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
12 open import Relation.Binary.Core
d9b704508281 isEquiv and isZF
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 4
diff changeset
13
213
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 210
diff changeset
14 open import logic
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 210
diff changeset
15 open import nat
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
16 import OD
213
22d435172d1a separate logic and nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 210
diff changeset
17
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
18 open inOrdinal O
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
19 open OD O
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
20 open OD.OD
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
21 open OD._==_
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
22
29
fce60b99dc55 posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
23 postulate
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
24 -- mimimul and x∋minimal is an Axiom of choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
25 minimal : (x : OD ) → ¬ (x == od∅ )→ OD
117
a4c97390d312 minimum assuption
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 116
diff changeset
26 -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x )
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
27 x∋minimal : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimal x ne ) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
28 -- minimality (may proved by ε-induction )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
29 minimal-1 : (x : OD ) → ( ne : ¬ (x == od∅ ) ) → (y : OD ) → ¬ ( def (minimal x ne) (od→ord y)) ∧ (def x (od→ord y) )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
30
188
1f2c8b094908 axiom of choice → p ∨ ¬ p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
31
189
540b845ea2de Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
32 --
540b845ea2de Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
33 -- Axiom of choice in intutionistic logic implies the exclude middle
540b845ea2de Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
34 -- https://plato.stanford.edu/entries/axiom-choice/#AxiChoLog
540b845ea2de Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
35 --
257
53b7acd63481 move product to OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
36
53b7acd63481 move product to OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
37 ppp : { p : Set n } { a : OD } → record { def = λ x → p } ∋ a → p
53b7acd63481 move product to OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
38 ppp {p} {a} d = d
53b7acd63481 move product to OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 254
diff changeset
39
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
40 p∨¬p : ( p : Set n ) → p ∨ ( ¬ p ) -- assuming axiom of choice
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
41 p∨¬p p with is-o∅ ( od→ord ( record { def = λ x → p } ))
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
42 p∨¬p p | yes eq = case2 (¬p eq) where
189
540b845ea2de Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
43 ps = record { def = λ x → p }
540b845ea2de Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
44 lemma : ps == od∅ → p → ⊥
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
45 lemma eq p0 = ¬x<0 {od→ord ps} (eq→ eq p0 )
189
540b845ea2de Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
46 ¬p : (od→ord ps ≡ o∅) → p → ⊥
540b845ea2de Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
47 ¬p eq = lemma ( subst₂ (λ j k → j == k ) oiso o∅≡od∅ ( o≡→== eq ))
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
48 p∨¬p p | no ¬p = case1 (ppp {p} {minimal ps (λ eq → ¬p (eqo∅ eq))} lemma) where
189
540b845ea2de Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
49 ps = record { def = λ x → p }
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
50 eqo∅ : ps == od∅ → od→ord ps ≡ o∅
188
1f2c8b094908 axiom of choice → p ∨ ¬ p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
51 eqo∅ eq = subst (λ k → od→ord ps ≡ k) ord-od∅ ( cong (λ k → od→ord k ) (==→o≡ eq))
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
52 lemma : ps ∋ minimal ps (λ eq → ¬p (eqo∅ eq))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
53 lemma = x∋minimal ps (λ eq → ¬p (eqo∅ eq))
188
1f2c8b094908 axiom of choice → p ∨ ¬ p
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 187
diff changeset
54
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
55 decp : ( p : Set n ) → Dec p -- assuming axiom of choice
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
56 decp p with p∨¬p p
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
57 decp p | case1 x = yes x
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
58 decp p | case2 x = no x
189
540b845ea2de Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
59
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
60 double-neg-eilm : {A : Set n} → ¬ ¬ A → A -- we don't have this in intutionistic logic
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
61 double-neg-eilm {A} notnot with decp A -- assuming axiom of choice
189
540b845ea2de Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
62 ... | yes p = p
540b845ea2de Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
63 ... | no ¬p = ⊥-elim ( notnot ¬p )
540b845ea2de Axiom of choies implies p ∨ ( ¬ p )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 188
diff changeset
64
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
65 OrdP : ( x : Ordinal ) ( y : OD ) → Dec ( Ord x ∋ y )
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
66 OrdP x y with trio< x (od→ord y)
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
67 OrdP x y | tri< a ¬b ¬c = no ¬c
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
68 OrdP x y | tri≈ ¬a refl ¬c = no ( o<¬≡ refl )
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
69 OrdP x y | tri> ¬a ¬b c = yes c
119
6e264c78e420 infinite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 118
diff changeset
70
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
71 open import zfc
190
6e778b0a7202 add filter
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 189
diff changeset
72
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
73 OD→ZFC : ZFC
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
74 OD→ZFC = record {
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
75 ZFSet = OD
43
0d9b9db14361 equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
76 ; _∋_ = _∋_
0d9b9db14361 equalitu and internal parametorisity
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 42
diff changeset
77 ; _≈_ = _==_
29
fce60b99dc55 posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
78 ; ∅ = od∅
28
f36e40d5d2c3 OD continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
79 ; Select = Select
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
80 ; isZFC = isZFC
28
f36e40d5d2c3 OD continue
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 27
diff changeset
81 } where
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
82 -- infixr 200 _∈_
96
f239ffc27fd0 Power Set and L
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 95
diff changeset
83 -- infixr 230 _∩_ _∪_
276
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
84 isZFC : IsZFC (OD ) _∋_ _==_ od∅ Select
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
85 isZFC = record {
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
86 choice-func = choice-func ;
6f10c47e4e7a separate choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
87 choice = choice
29
fce60b99dc55 posturate OD is isomorphic to Ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 28
diff changeset
88 } where
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
89 -- Axiom of choice ( is equivalent to the existence of minimal in our case )
162
b06f5d2f34b1 Axiom of choice
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 161
diff changeset
90 -- ∀ X [ ∅ ∉ X → (∃ f : X → ⋃ X ) → ∀ A ∈ X ( f ( A ) ∈ A ) ]
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
91 choice-func : (X : OD ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
92 choice-func X {x} not X∋x = minimal x not
223
2e1f19c949dc sepration of ordinal from OD
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 219
diff changeset
93 choice : (X : OD ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A
258
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 257
diff changeset
94 choice X {A} X∋A not = x∋minimal A not
78
9a7a64b2388c infinite and replacement begin
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 77
diff changeset
95
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
96 --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
97 ---
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
98 record choiced ( X : OD) : Set (suc n) where
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
99 field
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
100 a-choice : OD
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
101 is-in : X ∋ a-choice
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
102
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
103 choice-func' : (X : OD ) → (p∨¬p : ( p : Set (suc n)) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
104 choice-func' X p∨¬p not = have_to_find where
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
105 ψ : ( ox : Ordinal ) → Set (suc n)
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
106 ψ ox = (( x : Ordinal ) → x o< ox → ( ¬ def X x )) ∨ choiced X
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
107 lemma-ord : ( ox : Ordinal ) → ψ ox
235
846e0926bb89 fix cardinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 234
diff changeset
108 lemma-ord ox = TransFinite {ψ} induction ox where
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
109 ∋-p : (A x : OD ) → Dec ( A ∋ x )
271
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 262
diff changeset
110 ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x )) -- LEM
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
111 ∋-p A x | case1 (lift t) = yes t
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
112 ∋-p A x | case2 t = no (λ x → t (lift x ))
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
113 ∀-imply-or : {A : Ordinal → Set n } {B : Set (suc n) }
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
114 → ((x : Ordinal ) → A x ∨ B) → ((x : Ordinal ) → A x) ∨ B
271
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 262
diff changeset
115 ∀-imply-or {A} {B} ∀AB with p∨¬p (Lift ( suc n ) ((x : Ordinal ) → A x)) -- LEM
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
116 ∀-imply-or {A} {B} ∀AB | case1 (lift t) = case1 t
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
117 ∀-imply-or {A} {B} ∀AB | case2 x = case2 (lemma (λ not → x (lift not ))) where
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
118 lemma : ¬ ((x : Ordinal ) → A x) → B
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
119 lemma not with p∨¬p B
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
120 lemma not | case1 b = b
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
121 lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b ))
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
122 induction : (x : Ordinal) → ((y : Ordinal) → y o< x → ψ y) → ψ x
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
123 induction x prev with ∋-p X ( ord→od x)
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
124 ... | yes p = case2 ( record { a-choice = ord→od x ; is-in = p } )
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
125 ... | no ¬p = lemma where
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
126 lemma1 : (y : Ordinal) → (y o< x → def X y → ⊥) ∨ choiced X
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
127 lemma1 y with ∋-p X (ord→od y)
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
128 lemma1 y | yes y<X = case2 ( record { a-choice = ord→od y ; is-in = y<X } )
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
129 lemma1 y | no ¬y<X = case1 ( λ lt y<X → ¬y<X (subst (λ k → def X k ) (sym diso) y<X ) )
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
130 lemma : ((y : Ordinals.ord O) → (O Ordinals.o< y) x → def X y → ⊥) ∨ choiced X
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
131 lemma = ∀-imply-or lemma1
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
132 have_to_find : choiced X
271
2169d948159b fix incl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 262
diff changeset
133 have_to_find = dont-or (lemma-ord (od→ord X )) ¬¬X∋x where
234
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
134 ¬¬X∋x : ¬ ((x : Ordinal) → x o< (od→ord X) → def X x → ⊥)
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
135 ¬¬X∋x nn = not record {
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
136 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt)
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
137 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
138 }
e06b76e5b682 ac from LEM in abstract ordinal
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 228
diff changeset
139