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

comparison src/zorn.agda @ 870:f9fc8da87b5a

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 Thu, 15 Sep 2022 03:32:06 +0900
parents 1ca338c3f09c
children 2eaa61279c36
comparison
equal deleted inserted replaced
869:1ca338c3f09c 870:f9fc8da87b5a
445 sup : {x : Ordinal } → x o≤ z → SUP A (UnionCF A f mf ay supf x) 445 sup : {x : Ordinal } → x o≤ z → SUP A (UnionCF A f mf ay supf x)
446 sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z 446 sup=u : {b : Ordinal} → (ab : odef A b) → b o≤ z
447 → IsSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → supf b ≡ b 447 → IsSup A (UnionCF A f mf ay supf b) ab ∧ (¬ HasPrev A (UnionCF A f mf ay supf b) b f) → supf b ≡ b
448 supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) ) 448 supf-is-sup : {x : Ordinal } → (x≤z : x o≤ z) → supf x ≡ & (SUP.sup (sup x≤z) )
449 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y 449 supf-mono : {x y : Ordinal } → x o≤ y → supf x o≤ supf y
450 csupf : {b : Ordinal } → supf b o< z → odef (UnionCF A f mf ay supf z) (supf b) 450 csupf : {b : Ordinal } → supf b o≤ z → odef (UnionCF A f mf ay supf z) (supf b)
451 451
452 452
453 chain∋init : odef chain y 453 chain∋init : odef chain y
454 chain∋init = ⟪ ay , ch-init (init ay refl) ⟫ 454 chain∋init = ⟪ ay , ch-init (init ay refl) ⟫
455 f-next : {a : Ordinal} → odef chain a → odef chain (f a) 455 f-next : {a : Ordinal} → odef chain a → odef chain (f a)
488 488
489 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) 489 record ZChain1 ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)
490 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where 490 {y : Ordinal} (ay : odef A y) (zc : ZChain A f mf ay (& A)) ( z : Ordinal ) : Set (Level.suc n) where
491 supf = ZChain.supf zc 491 supf = ZChain.supf zc
492 field 492 field
493 order : {b s z1 : Ordinal} → b o< z → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
494 is-max : {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → b o< z → (ab : odef A b) 493 is-max : {a b : Ordinal } → (ca : odef (UnionCF A f mf ay supf z) a ) → b o< z → (ab : odef A b)
495 → HasPrev A (UnionCF A f mf ay supf z) b f ∨ IsSup A (UnionCF A f mf ay supf z) ab 494 → HasPrev A (UnionCF A f mf ay supf z) b f ∨ IsSup A (UnionCF A f mf ay supf z) ab
496 → * a < * b → odef ((UnionCF A f mf ay supf z)) b 495 → * a < * b → odef ((UnionCF A f mf ay supf z)) b
497 496
498 initial-segment : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f) 497 initial-segment : ( A : HOD ) ( f : Ordinal → Ordinal ) (mf : ≤-monotonic-f A f)
631 csupf-fc {b} {s} {z1} b≤z ss<sb (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05 where 630 csupf-fc {b} {s} {z1} b≤z ss<sb (init x refl ) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc05 where
632 s<b : s o< b 631 s<b : s o< b
633 s<b = ZChain.supf-inject zc ss<sb 632 s<b = ZChain.supf-inject zc ss<sb
634 s≤<z : s o≤ & A 633 s≤<z : s o≤ & A
635 s≤<z = ordtrans s<b b≤z 634 s≤<z = ordtrans s<b b≤z
636 zc04 : odef (UnionCF A f mf ay supf (supf s)) (supf s) 635 zc04 : odef (UnionCF A f mf ay supf (& A)) (supf s)
637 zc04 = ? ZChain.csupf zc ? 636 zc04 = ZChain.csupf zc (o<→≤ (z09 (ZChain.asupf zc)))
638 zc03 : odef (UnionCF A f mf ay supf (& A)) (supf s)
639 zc03 = ZChain.csupf zc ?
640 zc05 : odef (UnionCF A f mf ay supf b) (supf s) 637 zc05 : odef (UnionCF A f mf ay supf b) (supf s)
641 zc05 with zc04 638 zc05 with zc04
642 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫ 639 ... | ⟪ as , ch-init fc ⟫ = ⟪ as , ch-init fc ⟫
643 ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u (zc09 u<x ) is-sup fc ⟫ where 640 ... | ⟪ as , ch-is-sup u u<x is-sup fc ⟫ = ⟪ as , ch-is-sup u ? is-sup fc ⟫ where
641 zc07 : FClosure A f (supf u) (supf s) -- supf u ≤ supf s → supf u o≤ supf s
642 zc07 = fc
644 zc06 : supf u ≡ u 643 zc06 : supf u ≡ u
645 zc06 = ChainP.supu=u is-sup 644 zc06 = ChainP.supu=u is-sup
646 zc09 : u o< supf s → u o< b 645 zc09 : u o≤ supf s → u o< b
647 zc09 u<s = ordtrans (ZChain.supf-inject zc (subst (λ k → k o< supf s) (sym zc06) u<s)) s<b 646 zc09 u≤s with osuc-≡< u≤s
647 ... | case1 u=ss = ZChain.supf-inject zc (subst (λ k → k o< supf b) (sym (trans zc06 u=ss)) ss<sb )
648 ... | case2 u<ss = ordtrans (ZChain.supf-inject zc (subst (λ k → k o< supf s) (sym zc06) u<ss)) s<b
648 csupf-fc {b} {s} {z1} b<z ss≤sb (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04 where 649 csupf-fc {b} {s} {z1} b<z ss≤sb (fsuc x fc) = subst (λ k → odef (UnionCF A f mf ay supf b) k ) (sym &iso) zc04 where
649 zc04 : odef (UnionCF A f mf ay supf b) (f x) 650 zc04 : odef (UnionCF A f mf ay supf b) (f x)
650 zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss≤sb fc ) 651 zc04 with subst (λ k → odef (UnionCF A f mf ay supf b) k ) &iso (csupf-fc b<z ss≤sb fc )
651 ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫ 652 ... | ⟪ as , ch-init fc ⟫ = ⟪ proj2 (mf _ as) , ch-init (fsuc _ fc) ⟫
652 ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫ 653 ... | ⟪ as , ch-is-sup u u≤x is-sup fc ⟫ = ⟪ proj2 (mf _ as) , ch-is-sup u u≤x is-sup (fsuc _ fc) ⟫
653 order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b) 654 order : {b s z1 : Ordinal} → b o< & A → supf s o< supf b → FClosure A f (supf s) z1 → (z1 ≡ supf b) ∨ (z1 << supf b)
654 order {b} {s} {z1} b<z ss<sb fc = zc04 where 655 order {b} {s} {z1} b<z ss<sb fc = zc04 where
655 zc00 : ( * z1 ≡ SUP.sup (ZChain.sup zc (o<→≤ b<z) )) ∨ ( * z1 < SUP.sup ( ZChain.sup zc (o<→≤ b<z) ) ) 656 zc00 : ( * z1 ≡ SUP.sup (ZChain.sup zc (o<→≤ b<z) )) ∨ ( * z1 < SUP.sup ( ZChain.sup zc (o<→≤ b<z) ) )
656 zc00 = SUP.x<sup (ZChain.sup zc (o<→≤ b<z) ) (csupf-fc (o<→≤ b<z) ss<sb fc ) 657 zc00 = SUP.x<sup (ZChain.sup zc (o<→≤ b<z) ) (csupf-fc (o<→≤ b<z) ss<sb fc )
658 -- supf (supf b) ≡ supf b
657 zc04 : (z1 ≡ supf b) ∨ (z1 << supf b) 659 zc04 : (z1 ≡ supf b) ∨ (z1 << supf b)
658 zc04 with zc00 660 zc04 with zc00
659 ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (ZChain.supf-is-sup zc (o<→≤ b<z)) ) (cong (&) eq) ) 661 ... | case1 eq = case1 (subst₂ (λ j k → j ≡ k ) &iso (sym (ZChain.supf-is-sup zc (o<→≤ b<z)) ) (cong (&) eq) )
660 ... | case2 lt = case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (ZChain.supf-is-sup zc (o<→≤ b<z) ) ))) lt ) 662 ... | case2 lt = case2 (subst₂ (λ j k → j < k ) refl (subst₂ (λ j k → j ≡ k ) *iso refl (cong (*) (sym (ZChain.supf-is-sup zc (o<→≤ b<z) ) ))) lt )
661 663
856 -- supf0 px ≡ px 858 -- supf0 px ≡ px
857 -- supf0 px ≡ supf0 x 859 -- supf0 px ≡ supf0 x
858 860
859 no-extension : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A pchain x f) → ZChain A f mf ay x 861 no-extension : ( (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ HasPrev A pchain x f) → ZChain A f mf ay x
860 no-extension P = record { supf = supf0 ; asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono 862 no-extension P = record { supf = supf0 ; asupf = ZChain.asupf zc ; sup = λ lt → STMP.tsup (sup lt ) ; supf-mono = supf-mono
861 ; order = ? ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) } where 863 ; sup=u = sup=u ; supf-is-sup = λ lt → STMP.tsup=sup (sup lt) } where
862 zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z 864 zc10 : {z : Ordinal} → OD.def (od pchain) z → OD.def (od pchain1) z
863 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫ 865 zc10 {z} ⟪ az , ch-init fc ⟫ = ⟪ az , ch-init fc ⟫
864 zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) u1-is-sup fc ⟫ 866 zc10 {z} ⟪ az , ch-is-sup u1 u1<x u1-is-sup fc ⟫ = ⟪ az , ch-is-sup u1 (ordtrans u1<x (pxo<x op)) u1-is-sup fc ⟫
865 zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ (HasPrev A pchain x f ) 867 zc11 : (¬ xSUP (UnionCF A f mf ay supf0 px) x ) ∨ (HasPrev A pchain x f )
866 → {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z ∨ ( (supf0 px ≡ px) ∧ FClosure A f px z ) 868 → {z : Ordinal} → OD.def (od pchain1) z → OD.def (od pchain) z ∨ ( (supf0 px ≡ px) ∧ FClosure A f px z )
1083 1085
1084 zc70 : HasPrev A pchain x f → ¬ xSUP pchain x 1086 zc70 : HasPrev A pchain x f → ¬ xSUP pchain x
1085 zc70 pr xsup = ? 1087 zc70 pr xsup = ?
1086 1088
1087 no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) x ) → ZChain A f mf ay x 1089 no-extension : ¬ ( xSUP (UnionCF A f mf ay supf0 x) x ) → ZChain A f mf ay x
1088 no-extension ¬sp=x = record { supf = supf1 ; sup=u = sup=u ; order = ? 1090 no-extension ¬sp=x = record { supf = supf1 ; sup=u = sup=u
1089 ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!} ; asupf = ? } where 1091 ; sup = sup ; supf-is-sup = sis ; supf-mono = {!!} ; asupf = ? } where
1090 supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal 1092 supfu : {u : Ordinal } → ( a : u o< x ) → (z : Ordinal) → Ordinal
1091 supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z 1093 supfu {u} a z = ZChain.supf (pzc (osuc u) (ob<x lim a)) z
1092 pchain0=1 : pchain ≡ pchain1 1094 pchain0=1 : pchain ≡ pchain1
1093 pchain0=1 = ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where 1095 pchain0=1 = ==→o≡ record { eq→ = zc10 ; eq← = zc11 } where