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

comparison src/zorn.agda @ 532:90f61d55cc54

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 22 Apr 2022 13:56:31 +0900
parents 5ca59261a4aa
children 7325484fc491
comparison
equal deleted inserted replaced
531:5ca59261a4aa 532:90f61d55cc54
467 sa = subst (λ k → odef A (& k) ) (sym *iso) ( ODC.x∋minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) ) 467 sa = subst (λ k → odef A (& k) ) (sym *iso) ( ODC.x∋minimal O A (λ eq → ¬x<0 ( subst (λ k → o∅ o< k ) (=od∅→≡o∅ eq) 0<A )) )
468 HasMaximal : HOD 468 HasMaximal : HOD
469 HasMaximal = record { od = record { def = λ x → odef A x ∧ ( (m : Ordinal) → odef A m → ¬ (* x < * m)) } ; odmax = & A ; <odmax = z07 } where 469 HasMaximal = record { od = record { def = λ x → odef A x ∧ ( (m : Ordinal) → odef A m → ¬ (* x < * m)) } ; odmax = & A ; <odmax = z07 } where
470 z07 : {y : Ordinal} → odef A y ∧ ((m : Ordinal) → odef A m → ¬ (* y < * m)) → y o< & A 470 z07 : {y : Ordinal} → odef A y ∧ ((m : Ordinal) → odef A m → ¬ (* y < * m)) → y o< & A
471 z07 {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p ))) 471 z07 {y} p = subst (λ k → k o< & A) &iso ( c<→o< (subst (λ k → odef A k ) (sym &iso ) (proj1 p )))
472 no-maximum : HasMaximal =h= od∅ → (x : Ordinal) → ((m : Ordinal) → odef A m → odef A x ∧ (¬ (* x < * m) )) → ⊥
473 no-maximum nomx x P = ¬x<0 (eq→ nomx {x} ? )
474 Gtx : { x : HOD} → A ∋ x → HOD
475 Gtx {x} ax = record { od = record { def = λ y → odef A y ∧ (x < (* y)) } ; odmax = & A ; <odmax = {!!} }
472 cf : ¬ Maximal A → Ordinal → Ordinal 476 cf : ¬ Maximal A → Ordinal → Ordinal
473 cf = {!!} 477 cf nmx x with ODC.∋-p O A (* x)
478 ... | no _ = o∅
479 ... | yes ax with is-o∅ (& ( Gtx ax ))
480 ... | yes nogt = ⊥-elim (no-maximum ? x x-is-maximal ) where -- no larger element, so it is maximal
481 x-is-maximal : (m : Ordinal) → odef A m → odef A x ∧ (¬ (* x < * m))
482 x-is-maximal m am = ⟪ subst (λ k → odef A k) &iso ax , ¬x<m ⟫ where
483 ¬x<m : ¬ (* x < * m)
484 ¬x<m x<m = ∅< {Gtx ax} {* m} ⟪ subst (λ k → odef A k) (sym &iso) am , subst (λ k → * x < k ) (cong (*) (sym &iso)) x<m ⟫ (≡o∅→=od∅ nogt)
485 ... | no not = & (ODC.minimal O (Gtx ax) (λ eq → not (=od∅→≡o∅ eq)))
474 cf-is-<-monotonic : (nmx : ¬ Maximal A ) → (x : Ordinal) → odef A x → ( * x < * (cf nmx x) ) ∧ odef A (cf nmx x ) 486 cf-is-<-monotonic : (nmx : ¬ Maximal A ) → (x : Ordinal) → odef A x → ( * x < * (cf nmx x) ) ∧ odef A (cf nmx x )
475 cf-is-<-monotonic = {!!} 487 cf-is-<-monotonic nmx x ax = ⟪ {!!} , {!!} ⟫
476 cf-is-≤-monotonic : (nmx : ¬ Maximal A ) → ≤-monotonic-f A ( cf nmx ) 488 cf-is-≤-monotonic : (nmx : ¬ Maximal A ) → ≤-monotonic-f A ( cf nmx )
477 cf-is-≤-monotonic = {!!} 489 cf-is-≤-monotonic nmx x ax = ⟪ case2 (proj1 ( cf-is-<-monotonic nmx x ax )) , proj2 ( cf-is-<-monotonic nmx x ax ) ⟫
478 zsup : ZChain A sa (& A) → ( f : Ordinal → Ordinal ) → ≤-monotonic-f A f → Ordinal 490 zsup : (zc : ZChain A sa (& A)) → ( f : Ordinal → Ordinal ) → ≤-monotonic-f A f → SUP A (ZChain.chain zc)
479 zsup zc f mf = & ( SUP.sup (supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc f mf ) ) ) 491 zsup zc f mf = supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc f mf )
480 A∋zsup : (zc : ZChain A sa (& A)) → (nmx : ¬ Maximal A ) → A ∋ * (zsup zc (cf nmx) (cf-is-≤-monotonic nmx)) 492 -- zsup zc f mf = & ( SUP.sup (supP (ZChain.chain zc) (ZChain.chain⊆A zc) ( ZChain.f-total zc f mf ) ) )
481 A∋zsup zc nmx = {!!} 493 A∋zsup : (zc : ZChain A sa (& A)) → (nmx : ¬ Maximal A ) → A ∋ * ( & ( SUP.sup (zsup zc (cf nmx) (cf-is-≤-monotonic nmx)) ))
482 z03 : (zc : ZChain A sa (& A)) → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → f (zsup zc f mf ) ≡ zsup zc f mf 494 A∋zsup zc nmx = subst (λ k → odef A (& k )) (sym *iso) ( SUP.A∋maximal (zsup zc (cf nmx) (cf-is-≤-monotonic nmx)) )
495 z03 : (zc : ZChain A sa (& A)) → ( f : Ordinal → Ordinal ) → (mf : ≤-monotonic-f A f ) → f (& ( SUP.sup (zsup zc f mf ))) ≡ & (SUP.sup (zsup zc f mf ))
483 z03 = {!!} 496 z03 = {!!}
484 z04 : (zc : ZChain A sa (& A)) → ¬ Maximal A → ⊥ 497 z04 : (zc : ZChain A sa (& A)) → ¬ Maximal A → ⊥
485 z04 zc nmx = z01 {* (cf nmx c)} {* c} sa (A∋zsup zc nmx ) (case1 ( cong (*)( z03 zc (cf nmx) (cf-is-≤-monotonic nmx )))) 498 z04 zc nmx = z01 {* (cf nmx c)} {* c} {!!} (A∋zsup zc nmx ) (case1 ( cong (*)( z03 zc (cf nmx) (cf-is-≤-monotonic nmx ))))
486 (proj1 (cf-is-<-monotonic nmx c ((subst λ k → odef A k ) &iso (A∋zsup zc nmx )))) where 499 (proj1 (cf-is-<-monotonic nmx c ((subst λ k → odef A k ) &iso (A∋zsup zc nmx )))) where
487 c = zsup zc (cf nmx) (cf-is-≤-monotonic nmx) 500 c = & (SUP.sup (zsup zc (cf nmx) (cf-is-≤-monotonic nmx)))
488 -- ZChain is not compatible with the SUP condition 501 -- ZChain is not compatible with the SUP condition
489 ind : (x : Ordinal) → ((y : Ordinal) → y o< x → ZChain A sa y ∨ Maximal A ) 502 ind : (x : Ordinal) → ((y : Ordinal) → y o< x → ZChain A sa y ∨ Maximal A )
490 → ZChain A sa x ∨ Maximal A 503 → ZChain A sa x ∨ Maximal A
491 ind x prev with Oprev-p x 504 ind x prev with Oprev-p x
492 ... | yes op with ODC.∋-p O A (* x) 505 ... | yes op with ODC.∋-p O A (* x)