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

comparison ordinal-definable.agda @ 36:4d64509067d0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
transitive
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 23 May 2019 02:32:02 +0900
parents c9ad0d97ce41
children f10ceee99d00
comparison
equal deleted inserted replaced
35:88b77cecaeba 36:4d64509067d0
24 open OD 24 open OD
25 open import Data.Unit 25 open import Data.Unit
26 26
27 postulate 27 postulate
28 od→ord : {n : Level} → OD {n} → Ordinal {n} 28 od→ord : {n : Level} → OD {n} → Ordinal {n}
29 29 ord→od : {n : Level} → Ordinal {n} → OD {n}
30 ord→od : {n : Level} → Ordinal {n} → OD {n}
31 ord→od x = record { def = λ y → x ≡ y }
32 30
33 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n 31 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n
34 _∋_ {n} a x = def a ( od→ord x ) 32 _∋_ {n} a x = def a ( od→ord x )
35 33
36 _c<_ : { n : Level } → ( a x : OD {n} ) → Set n 34 _c<_ : { n : Level } → ( a x : OD {n} ) → Set n
38 36
39 _c≤_ : {n : Level} → OD {n} → OD {n} → Set (suc n) 37 _c≤_ : {n : Level} → OD {n} → OD {n} → Set (suc n)
40 a c≤ b = (a ≡ b) ∨ ( b ∋ a ) 38 a c≤ b = (a ≡ b) ∨ ( b ∋ a )
41 39
42 postulate 40 postulate
43 c<→o< : {n : Level} {x y : OD {n} } → x c< y → od→ord x o< od→ord x 41 c<→o< : {n : Level} {x y : OD {n} } → x c< y → od→ord x o< od→ord y
44 o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → ord→od x c< ord→od x 42 o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → ord→od x c< ord→od y
45 oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x 43 oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x
46 diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x 44 diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
47 sup-od : {n : Level } → ( OD {n} → OD {n}) → OD {n} 45 sup-od : {n : Level } → ( OD {n} → OD {n}) → OD {n}
48 sup-c< : {n : Level } → ( ψ : OD {n} → OD {n}) → ∀ {x : OD {n}} → ψ x c< sup-od ψ 46 sup-c< : {n : Level } → ( ψ : OD {n} → OD {n}) → ∀ {x : OD {n}} → ψ x c< sup-od ψ
49 47
77 c3 lx (OSuc .lx x₁) d not | t | () 75 c3 lx (OSuc .lx x₁) d not | t | ()
78 c3 (Suc lx) (ℵ lx) d not with not ( record { lv = Suc lx ; ord = OSuc (Suc lx) (Φ (Suc lx)) } ) 76 c3 (Suc lx) (ℵ lx) d not with not ( record { lv = Suc lx ; ord = OSuc (Suc lx) (Φ (Suc lx)) } )
79 ... | t with t (case2 (s< (ℵΦ< {_} {_} {Φ (Suc lx)}))) 77 ... | t with t (case2 (s< (ℵΦ< {_} {_} {Φ (Suc lx)})))
80 c3 .(Suc lx) (ℵ lx) d not | t | () 78 c3 .(Suc lx) (ℵ lx) d not | t | ()
81 79
82 ∅2 : {n : Level} → od→ord ( od∅ {n} ) ≡ o∅ {n} 80 def-subst : {n : Level } {Z : OD {n}} {X : Ordinal {n} }{z : OD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z → X ≡ x → def z x
83 ∅2 {n} = {!!} 81 def-subst df refl refl = df
82
83 transitive : {n : Level } { x y z : OD {n} } → y ∋ x → z ∋ y → z ∋ x
84 transitive {n} {x} {y} {z} x∋y z∋y with ordtrans ( c<→o< {n} {x} {y} x∋y ) ( c<→o< {n} {y} {z} z∋y )
85 ... | t = lemma0 (lemma t) where
86 lemma : ( od→ord x ) o< ( od→ord z ) → def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x )))
87 lemma xo<z = o<→c< xo<z
88 lemma0 : def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x ))) → def z (od→ord x)
89 lemma0 dz = def-subst {n} { ord→od ( od→ord z )} { od→ord ( ord→od ( od→ord x))} dz (oiso) (diso)
90
91 open Ordinal
84 92
85 HOD→ZF : {n : Level} → ZF {suc n} {suc n} 93 HOD→ZF : {n : Level} → ZF {suc n} {suc n}
86 HOD→ZF {n} = record { 94 HOD→ZF {n} = record {
87 ZFSet = OD {n} 95 ZFSet = OD {n}
88 ; _∋_ = λ a x → Lift (suc n) ( a ∋ x ) 96 ; _∋_ = λ a x → Lift (suc n) ( a ∋ x )
143 proj1 (pair A B ) = lift ( case1 refl ) 151 proj1 (pair A B ) = lift ( case1 refl )
144 proj2 (pair A B ) = lift ( case2 refl ) 152 proj2 (pair A B ) = lift ( case2 refl )
145 empty : (x : OD {n} ) → ¬ Lift (suc n) (od∅ ∋ x) 153 empty : (x : OD {n} ) → ¬ Lift (suc n) (od∅ ∋ x)
146 empty x (lift (lift ())) 154 empty x (lift (lift ()))
147 union→ : (X x y : OD {n} ) → Lift (suc n) (X ∋ x) → Lift (suc n) (x ∋ y) → Lift (suc n) (Union X ∋ y) 155 union→ : (X x y : OD {n} ) → Lift (suc n) (X ∋ x) → Lift (suc n) (x ∋ y) → Lift (suc n) (Union X ∋ y)
148 union→ X x y (lift X∋x) (lift x∋y) = lift lemma where 156 union→ X x y (lift X∋x) (lift x∋y) = lift {!!} where
149 lemma : {z : Ordinal {n} } → def X z → z ≡ od→ord y 157 lemma : {z : Ordinal {n} } → def X z → z ≡ od→ord y
150 lemma {z} X∋z = {!!} 158 lemma {z} X∋z = {!!}
151 -- _∋_ {n} a x = def a ( od→ord x )
152 ¬∅ : (x : OD {n} ) → ¬ x ≡ od∅ → Ordinal {n}
153 ¬∅ = {!!}
154 ¬∅∈ : (x : OD {n} ) → (not : ¬ x ≡ od∅ ) → x ∋ (ord→od (¬∅ x not))
155 ¬∅∈ = {!!}
156 minimul : OD {n} → ( OD {n} ∧ OD {n} ) 159 minimul : OD {n} → ( OD {n} ∧ OD {n} )
157 minimul x = {!!} 160 minimul x = record { proj1 = record { def = {!!} } ; proj2 = record { def = {!!} } }
158 regularity : (x : OD) → ¬ x ≡ od∅ → 161 regularity : (x : OD) → ¬ x ≡ od∅ →
159 Lift (suc n) (x ∋ proj1 (minimul x)) ∧ 162 Lift (suc n) (x ∋ proj1 (minimul x)) ∧
160 (Select (proj1 (minimul x ) , x) (λ x₁ → Lift (suc n) (proj1 ( minimul x ) ∋ x₁) ∧ Lift (suc n) (x ∋ x₁)) ≡ od∅) 163 (Select (proj1 (minimul x ) , x) (λ x₁ → Lift (suc n) (proj1 ( minimul x ) ∋ x₁) ∧ Lift (suc n) (x ∋ x₁)) ≡ od∅)
161 proj1 ( regularity x non ) = lift lemma where 164 proj1 ( regularity x non ) = lift lemma where
162 lemma : def x (od→ord (proj1 (minimul x))) 165 lemma : def x (od→ord (proj1 (minimul x)))