nat_lat.miz



    begin

    reserve n,m for Nat;

    definition

      :: NAT_LAT:def1

      func hcflat -> BinOp of NAT means

      : Def1: (it . (m,n)) = (m gcd n);

      existence

      proof

        deffunc O( Nat, Nat) = ($1 gcd $2);

        consider o be BinOp of NAT such that

         A1: for a,b be Element of NAT holds (o . (a,b)) = O(a,b) from BINOP_1:sch 4;

        take o;

        let m, n;

        m in NAT & n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let f1,f2 be BinOp of NAT such that

         A2: (f1 . (m,n)) = (m gcd n) and

         A3: (f2 . (m,n)) = (m gcd n);

        now

          let m,n be Element of NAT ;

          

          thus (f1 . (m,n)) = (m gcd n) by A2

          .= (f2 . (m,n)) by A3;

        end;

        hence thesis;

      end;

      :: NAT_LAT:def2

      func lcmlat -> BinOp of NAT means

      : Def2: (it . (m,n)) = (m lcm n);

      existence

      proof

        deffunc O( Nat, Nat) = ($1 lcm $2);

        consider o be BinOp of NAT such that

         A4: for a,b be Element of NAT holds (o . (a,b)) = O(a,b) from BINOP_1:sch 4;

        take o;

        let m, n;

        m in NAT & n in NAT by ORDINAL1:def 12;

        hence thesis by A4;

      end;

      uniqueness

      proof

        let f1,f2 be BinOp of NAT such that

         A5: (f1 . (m,n)) = (m lcm n) and

         A6: (f2 . (m,n)) = (m lcm n);

        now

          let m,n be Element of NAT ;

          

          thus (f1 . (m,n)) = (m lcm n) by A5

          .= (f2 . (m,n)) by A6;

        end;

        hence thesis;

      end;

    end

    definition

      :: NAT_LAT:def3

      func Nat_Lattice -> strict non empty LattStr equals LattStr (# NAT , lcmlat , hcflat #);

      coherence ;

    end

    registration

      cluster the carrier of Nat_Lattice -> natural-membered;

      coherence ;

    end

    reserve p,q,r for Element of Nat_Lattice ;

    registration

      let p, q;

      identify p lcm q with p "\/" q;

      compatibility by Def2;

      identify p gcd q with p "/\" q;

      compatibility by Def1;

    end

    theorem :: NAT_LAT:1

    (p "\/" q) = (p lcm q);

    theorem :: NAT_LAT:2

    (p "/\" q) = (p gcd q);

    theorem :: NAT_LAT:3

    for a,b be Element of Nat_Lattice st a [= b holds a divides b by NEWTON: 44;

    definition

      :: NAT_LAT:def4

      func 0_NN -> Element of Nat_Lattice equals 1;

      coherence ;

      :: NAT_LAT:def5

      func 1_NN -> Element of Nat_Lattice equals 0 ;

      coherence ;

    end

    theorem :: NAT_LAT:4

     0_NN = 1;

    

     Lm1: for a be Element of Nat_Lattice holds ( 0_NN "/\" a) = 0_NN & (a "/\" 0_NN ) = 0_NN by NEWTON: 51;

    registration

      cluster Nat_Lattice -> Lattice-like;

      coherence

      proof

        thus (for p, q holds (p "\/" q) = (q "\/" p)) & (for p, q, r holds (p "\/" (q "\/" r)) = ((p "\/" q) "\/" r)) & (for p, q holds ((p "/\" q) "\/" q) = q) & (for p, q holds (p "/\" q) = (q "/\" p)) & (for p, q, r holds (p "/\" (q "/\" r)) = ((p "/\" q) "/\" r)) & for p, q holds (p "/\" (p "\/" q)) = p by NEWTON: 43, NEWTON: 48, NEWTON: 53, NEWTON: 54;

      end;

    end

    registration

      cluster Nat_Lattice -> strict;

      coherence ;

    end

    reserve p,q,r for Element of Nat_Lattice ;

    registration

      cluster Nat_Lattice -> lower-bounded;

      coherence by Lm1;

    end

    theorem :: NAT_LAT:5

    

     Th5: ( lcmlat . (p,q)) = ( lcmlat . (q,p))

    proof

      

      thus ( lcmlat . (p,q)) = (q "\/" p) by LATTICES:def 1

      .= ( lcmlat . (q,p));

    end;

    theorem :: NAT_LAT:6

    

     Th6: ( hcflat . (q,p)) = ( hcflat . (p,q))

    proof

      

      thus ( hcflat . (q,p)) = (p "/\" q) by LATTICES:def 2

      .= ( hcflat . (p,q));

    end;

    theorem :: NAT_LAT:7

    

     Th7: ( lcmlat . (p,( lcmlat . (q,r)))) = ( lcmlat . (( lcmlat . (p,q)),r))

    proof

      set s = (q "\/" r);

      

      thus ( lcmlat . (p,( lcmlat . (q,r)))) = (p "\/" s)

      .= ((p "\/" q) "\/" r) by NEWTON: 43

      .= ( lcmlat . (( lcmlat . (p,q)),r));

    end;

    theorem :: NAT_LAT:8

    ( lcmlat . (p,( lcmlat . (q,r)))) = ( lcmlat . (( lcmlat . (q,p)),r)) & ( lcmlat . (p,( lcmlat . (q,r)))) = ( lcmlat . (( lcmlat . (p,r)),q)) & ( lcmlat . (p,( lcmlat . (q,r)))) = ( lcmlat . (( lcmlat . (r,q)),p)) & ( lcmlat . (p,( lcmlat . (q,r)))) = ( lcmlat . (( lcmlat . (r,p)),q))

    proof

      set s = (r "\/" q);

      

      thus ( lcmlat . (p,( lcmlat . (q,r)))) = ( lcmlat . (( lcmlat . (p,q)),r)) by Th7

      .= ( lcmlat . (( lcmlat . (q,p)),r)) by Th5;

      

      thus

       A1: ( lcmlat . (p,( lcmlat . (q,r)))) = ( lcmlat . (p,( lcmlat . (r,q)))) by Th5

      .= ( lcmlat . (( lcmlat . (p,r)),q)) by Th7;

      

      thus ( lcmlat . (p,( lcmlat . (q,r)))) = ( lcmlat . (p,s)) by LATTICES:def 1

      .= ( lcmlat . (( lcmlat . (r,q)),p)) by Th5;

      thus thesis by A1, Th5;

    end;

    theorem :: NAT_LAT:9

    

     Th9: ( hcflat . (p,( hcflat . (q,r)))) = ( hcflat . (( hcflat . (p,q)),r))

    proof

      set s = (q "/\" r);

      

      thus ( hcflat . (p,( hcflat . (q,r)))) = (p "/\" s)

      .= ((p "/\" q) "/\" r) by NEWTON: 48

      .= ( hcflat . (( hcflat . (p,q)),r));

    end;

    theorem :: NAT_LAT:10

    ( hcflat . (p,( hcflat . (q,r)))) = ( hcflat . (( hcflat . (q,p)),r)) & ( hcflat . (p,( hcflat . (q,r)))) = ( hcflat . (( hcflat . (p,r)),q)) & ( hcflat . (p,( hcflat . (q,r)))) = ( hcflat . (( hcflat . (r,q)),p)) & ( hcflat . (p,( hcflat . (q,r)))) = ( hcflat . (( hcflat . (r,p)),q))

    proof

      set s = (r "/\" q);

      

      thus ( hcflat . (p,( hcflat . (q,r)))) = ( hcflat . (( hcflat . (p,q)),r)) by Th9

      .= ( hcflat . (( hcflat . (q,p)),r)) by Th6;

      

      thus

       A1: ( hcflat . (p,( hcflat . (q,r)))) = ( hcflat . (p,( hcflat . (r,q)))) by Th6

      .= ( hcflat . (( hcflat . (p,r)),q)) by Th9;

      

      thus ( hcflat . (p,( hcflat . (q,r)))) = ( hcflat . (p,s)) by LATTICES:def 2

      .= ( hcflat . (( hcflat . (r,q)),p)) by Th6;

      thus thesis by A1, Th6;

    end;

    theorem :: NAT_LAT:11

    ( hcflat . (q,( lcmlat . (q,p)))) = q & ( hcflat . (( lcmlat . (p,q)),q)) = q & ( hcflat . (q,( lcmlat . (p,q)))) = q & ( hcflat . (( lcmlat . (q,p)),q)) = q

    proof

      set s = (q "\/" p);

      

      thus

       A1: ( hcflat . (q,( lcmlat . (q,p)))) = (q "/\" s)

      .= q by NEWTON: 54;

      

      thus

       A2: ( hcflat . (( lcmlat . (p,q)),q)) = ( hcflat . ((p "\/" q),q))

      .= (q "/\" (q "\/" p)) by LATTICES:def 2

      .= q by NEWTON: 54;

      thus ( hcflat . (q,( lcmlat . (p,q)))) = q by A1, Th5;

      thus thesis by A2, Th5;

    end;

    theorem :: NAT_LAT:12

    ( lcmlat . (q,( hcflat . (q,p)))) = q & ( lcmlat . (( hcflat . (p,q)),q)) = q & ( lcmlat . (q,( hcflat . (p,q)))) = q & ( lcmlat . (( hcflat . (q,p)),q)) = q

    proof

      set r = (p "/\" q);

      

      thus

       A1: ( lcmlat . (q,( hcflat . (q,p)))) = ( lcmlat . (q,(q "/\" p)))

      .= ((p "/\" q) "\/" q) by LATTICES:def 1

      .= q by NEWTON: 53;

      

      thus

       A2: ( lcmlat . (( hcflat . (p,q)),q)) = (r "\/" q)

      .= q by NEWTON: 53;

      thus ( lcmlat . (q,( hcflat . (p,q)))) = q by A1, Th6;

      thus thesis by A2, Th6;

    end;

    definition

      :: NAT_LAT:def6

      func NATPLUS -> Subset of NAT means

      : Def6: for n be Nat holds n in it iff 0 < n;

      existence

      proof

        defpred P[ Nat] means 0 < $1;

        consider X be Subset of NAT such that

         A1: for n be Element of NAT holds n in X iff P[n] from SUBSET_1:sch 3;

        take X;

        let n be Nat;

        thus n in X implies 0 < n by A1;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let X,Y be Subset of NAT such that

         A2: for n be Nat holds n in X iff 0 < n and

         A3: for n be Nat holds n in Y iff 0 < n;

        thus X c= Y by A2, A3;

        let x be object;

        assume

         A4: x in Y;

        then

        reconsider x as Nat;

         0 < x by A3, A4;

        hence thesis by A2;

      end;

    end

    registration

      cluster NATPLUS -> non empty;

      coherence

      proof

         0 < 1;

        hence thesis by Def6;

      end;

    end

    definition

      let D be non empty set, S be non empty Subset of D, N be non empty Subset of S;

      :: original: Element

      redefine

      mode Element of N -> Element of S ;

      coherence

      proof

        let x be Element of N;

        thus thesis;

      end;

    end

    registration

      let D be Subset of REAL ;

      cluster -> real for Element of D;

      coherence ;

    end

    registration

      let D be Subset of NAT ;

      cluster -> real for Element of D;

      coherence ;

    end

    definition

      mode NatPlus is Element of NATPLUS ;

    end

    definition

      let k be Nat;

      :: NAT_LAT:def7

      func @ k -> NatPlus equals

      : Def7: k;

      coherence by A1, Def6;

    end

    registration

      cluster -> natural non zero for NatPlus;

      coherence by Def6;

    end

    reserve m,n for NatPlus;

    definition

      :: NAT_LAT:def8

      func hcflatplus -> BinOp of NATPLUS means

      : Def8: (it . (m,n)) = (m gcd n);

      existence

      proof

        deffunc O( NatPlus, NatPlus) = ( @ ($1 gcd $2));

        consider f be BinOp of NATPLUS such that

         A1: for m,n be NatPlus holds (f . (m,n)) = O(m,n) from BINOP_1:sch 4;

        take f;

        let m,n be NatPlus;

        

         A2: (f . (m,n)) = ( @ (m gcd n)) by A1;

        n > 0 by Def6;

        hence thesis by A2, Def7, NEWTON: 58;

      end;

      uniqueness

      proof

        deffunc O( NatPlus, NatPlus) = ($1 gcd $2);

        thus for o1,o2 be BinOp of NATPLUS st (for a,b be NatPlus holds (o1 . (a,b)) = O(a,b)) & (for a,b be NatPlus holds (o2 . (a,b)) = O(a,b)) holds o1 = o2 from BINOP_2:sch 2;

      end;

      :: NAT_LAT:def9

      func lcmlatplus -> BinOp of NATPLUS means

      : Def9: (it . (m,n)) = (m lcm n);

      existence

      proof

        deffunc O( NatPlus, NatPlus) = ( @ ($1 lcm $2));

        consider f be BinOp of NATPLUS such that

         A3: for m,n be NatPlus holds (f . (m,n)) = O(m,n) from BINOP_1:sch 4;

        take f;

        let m,n be NatPlus;

        

         A4: m > 0 & n > 0 by Def6;

        

        thus (f . (m,n)) = O(m,n) by A3

        .= (m lcm n) by A4, Def7, NEWTON: 59;

      end;

      uniqueness

      proof

        deffunc O( NatPlus, NatPlus) = ($1 lcm $2);

        thus for o1,o2 be BinOp of NATPLUS st (for a,b be NatPlus holds (o1 . (a,b)) = O(a,b)) & (for a,b be NatPlus holds (o2 . (a,b)) = O(a,b)) holds o1 = o2 from BINOP_2:sch 2;

      end;

    end

    definition

      :: NAT_LAT:def10

      func NatPlus_Lattice -> strict LattStr equals LattStr (# NATPLUS , lcmlatplus , hcflatplus #);

      coherence ;

    end

    registration

      cluster NatPlus_Lattice -> non empty;

      coherence ;

    end

    definition

      let m be Element of NatPlus_Lattice ;

      :: NAT_LAT:def11

      func @ m -> NatPlus equals m;

      coherence ;

    end

    registration

      cluster -> natural non zero for Element of NatPlus_Lattice ;

      coherence ;

    end

    reserve p,q for Element of NatPlus_Lattice ;

    registration

      let p,q be Element of NatPlus_Lattice ;

      identify p lcm q with p "\/" q;

      compatibility by Def9;

      identify p gcd q with p "/\" q;

      compatibility by Def8;

    end

    theorem :: NAT_LAT:13

    (p "\/" q) = (( @ p) lcm ( @ q));

    theorem :: NAT_LAT:14

    (p "/\" q) = (( @ p) gcd ( @ q));

    

     Lm2: (for a,b be Element of NatPlus_Lattice holds (a "\/" b) = (b "\/" a)) & for a,b,c be Element of NatPlus_Lattice holds (a "\/" (b "\/" c)) = ((a "\/" b) "\/" c) by NEWTON: 43;

    

     Lm3: (for a,b be Element of NatPlus_Lattice holds ((a "/\" b) "\/" b) = b) & for a,b be Element of NatPlus_Lattice holds (a "/\" b) = (b "/\" a) by NEWTON: 53;

    

     Lm4: (for a,b,c be Element of NatPlus_Lattice holds (a "/\" (b "/\" c)) = ((a "/\" b) "/\" c)) & for a,b be Element of NatPlus_Lattice holds (a "/\" (a "\/" b)) = a by NEWTON: 48, NEWTON: 54;

    registration

      cluster NatPlus_Lattice -> join-commutative join-associative meet-commutative meet-associative join-absorbing meet-absorbing;

      coherence by Lm2, Lm3, Lm4;

    end

     Lm5:

    now

      let L be Lattice;

       [:the carrier of L, the carrier of L:] = ( dom the L_join of L) by FUNCT_2:def 1;

      hence the L_join of L = (the L_join of L || the carrier of L) by RELAT_1: 68;

       [:the carrier of L, the carrier of L:] = ( dom the L_meet of L) by FUNCT_2:def 1;

      hence the L_meet of L = (the L_meet of L || the carrier of L) by RELAT_1: 68;

    end;

    definition

      let L be Lattice;

      :: NAT_LAT:def12

      mode SubLattice of L -> Lattice means

      : Def12: the carrier of it c= the carrier of L & the L_join of it = (the L_join of L || the carrier of it ) & the L_meet of it = (the L_meet of L || the carrier of it );

      existence

      proof

        take L;

        thus thesis by Lm5;

      end;

    end

    registration

      let L be Lattice;

      cluster strict for SubLattice of L;

      existence

      proof

        set S = LattStr (# the carrier of L, the L_join of L, the L_meet of L #);

         A1:

        now

          let a,b,c be Element of S;

          reconsider a9 = a, b9 = b, c9 = c as Element of L;

          

          thus (a "\/" (b "\/" c)) = (a9 "\/" (b9 "\/" c9))

          .= ((a9 "\/" b9) "\/" c9) by LATTICES:def 5

          .= ((a "\/" b) "\/" c);

        end;

         A2:

        now

          let a,b be Element of S;

          reconsider a9 = a, b9 = b as Element of L;

          

          thus ((a "/\" b) "\/" b) = ((a9 "/\" b9) "\/" b9)

          .= b by LATTICES:def 8;

        end;

         A3:

        now

          let a,b be Element of S;

          reconsider a9 = a, b9 = b as Element of L;

          

          thus (a "/\" (a "\/" b)) = (a9 "/\" (a9 "\/" b9))

          .= a by LATTICES:def 9;

        end;

         A4:

        now

          let a,b,c be Element of S;

          reconsider a9 = a, b9 = b, c9 = c as Element of L;

          

          thus (a "/\" (b "/\" c)) = (a9 "/\" (b9 "/\" c9))

          .= ((a9 "/\" b9) "/\" c9) by LATTICES:def 7

          .= ((a "/\" b) "/\" c);

        end;

        

         A5: for a,b be Element of S, a9,b9 be Element of L st a = a9 & b = b9 holds (a "\/" b) = (a9 "\/" b9) & (a "/\" b) = (a9 "/\" b9);

         A6:

        now

          let a,b be Element of S;

          reconsider a9 = a, b9 = b as Element of L;

          

          thus (a "/\" b) = (b9 "/\" a9) by A5

          .= (b "/\" a);

        end;

        now

          let a,b be Element of S;

          reconsider a9 = a, b9 = b as Element of L;

          

          thus (a "\/" b) = (b9 "\/" a9) by A5

          .= (b "\/" a);

        end;

        then S is join-commutative join-associative meet-absorbing meet-commutative meet-associative join-absorbing by A1, A2, A6, A4, A3;

        then

        reconsider S as Lattice;

        the L_join of S = (the L_join of L || the carrier of S) & the L_meet of S = (the L_meet of L || the carrier of S) by RELSET_1: 19;

        then S is SubLattice of L by Def12;

        hence thesis;

      end;

    end

    theorem :: NAT_LAT:15

    for L be Lattice holds L is SubLattice of L

    proof

      let L be Lattice;

      thus the carrier of L c= the carrier of L;

      thus thesis by Lm5;

    end;

    theorem :: NAT_LAT:16

     NatPlus_Lattice is SubLattice of Nat_Lattice

    proof

      

       A1: for x be object st x in ( dom hcflatplus ) holds ( hcflatplus . x) = ( hcflat . x)

      proof

        let x be object;

        assume

         A2: x in ( dom hcflatplus );

        then

         A3: x in [: NATPLUS , NATPLUS :] by FUNCT_2:def 1;

        consider y1,y2 be object such that

         A4: [y1, y2] = x by A2, RELAT_1:def 1;

        y1 in NATPLUS & y2 in NATPLUS by A3, A4, ZFMISC_1: 87;

        then

        reconsider n = y1, k = y2 as Nat;

        

         A5: ( hcflat . (n,k)) = (n gcd k) by Def1;

        reconsider n = y1, k = y2 as NatPlus by A3, A4, ZFMISC_1: 87;

        ( hcflatplus . (n,k)) = ( hcflat . (n,k)) by A5, Def8;

        hence thesis by A4;

      end;

      ( dom hcflatplus ) = [: NATPLUS , NATPLUS :] & ( dom hcflat ) = [: NAT , NAT :] by FUNCT_2:def 1;

      then ( dom hcflatplus ) = (( dom hcflat ) /\ [: NATPLUS , NATPLUS :]) by XBOOLE_1: 28, ZFMISC_1: 96;

      then

       A6: hcflatplus = ( hcflat || NATPLUS ) by A1, FUNCT_1: 46;

      

       A7: for x be object st x in ( dom lcmlatplus ) holds ( lcmlatplus . x) = ( lcmlat . x)

      proof

        let x be object;

        assume

         A8: x in ( dom lcmlatplus );

        then

         A9: x in [: NATPLUS , NATPLUS :] by FUNCT_2:def 1;

        consider y1,y2 be object such that

         A10: [y1, y2] = x by A8, RELAT_1:def 1;

        y1 in NATPLUS & y2 in NATPLUS by A9, A10, ZFMISC_1: 87;

        then

        reconsider n = y1, k = y2 as Nat;

        

         A11: ( lcmlat . (n,k)) = (n lcm k) by Def2;

        reconsider n = y1, k = y2 as NatPlus by A9, A10, ZFMISC_1: 87;

        ( lcmlatplus . (n,k)) = ( lcmlat . (n,k)) by A11, Def9;

        hence thesis by A10;

      end;

      ( dom lcmlatplus ) = [: NATPLUS , NATPLUS :] & ( dom lcmlat ) = [: NAT , NAT :] by FUNCT_2:def 1;

      then ( dom lcmlatplus ) = (( dom lcmlat ) /\ [: NATPLUS , NATPLUS :]) by XBOOLE_1: 28, ZFMISC_1: 96;

      then lcmlatplus = ( lcmlat || NATPLUS ) by A7, FUNCT_1: 46;

      hence thesis by A6, Def12;

    end;