0.6.  НАТУРАЛЬНЫЕ, ЦЕЛЫЕ И ВЕЩЕСТВЕННЫЕ

     Введем типы натуральных (UInt), целых (Int) и  вещественных
(Real) чисел и наметим доказательство того, что  в  определенном
выше смысле тип  целых  не  является  подтипом  вещественных  и,
поэтому,  класс  целых  не  может  быть  наследован  из   класса
вещественных.
     
     0.6.1.  Тип натуральных чисел

     В этой версии будем  строить  множество  натуральных  чисел
начиная с 0.

     Спецификация множество натуральных чисел с системой  аксиом
Пеано.
scheme PEANO =
    class
        type                        -- обозначили  тип натуральных N
            N
        value
                                7
                                 

            zero : N,               -- завели величину zero
            succ: N -> N            -- величина - функция из N в N
        axiom
          [first_is_zero]
            all n : N :-            -- для каждого натурального n
                ~(succ(n) is zero)  -- применение succ(n) не есть zero

         ,[linear_order]
            all  n1, n2 : N :-
                (succ(n1) is succ(n2)) => (n1 is n2)
         , [induction]
            all p : N -> Bool :-    -- для любого предиката
                    (p(zero) / (all n : N :- p(n) => p(succ(n)))) =>
                             (all n : N :- p(n))
    end

--
-- ~     отрицание
-- :-    выполняется
-- =>    влечет
-- /    логическое и
--
-- exist квантор существования
--
--
Множеством  натуральных  чисел  N  по   построению   будут   все
последовательные применения функции succ
  zero,
  succ(zero),
  succ(succ(zero)),
  succ(succ(succ(zero))),
  ...

     К аксиомам Пеано добавим операцию сложения.
PEANO                           --  подключение схемы PEANO

scheme NAT =
    extend PEANO with
    class
        value
          plus : N >< N -> N    -- вводим функции (операции)  сложить
          ,
          mult : N >< N -> N    -- и умножить
        axiom
          [plus_zero]
            all n : N :-
            plus(n, zero) is n
            ,
          [plus_succ]
            all n1, n2 : N :-
            plus(n1, succ(n2)) is succ(plus(n1, n2))
            ,
          [mult_zero]
            all n : N :-
            mult(n, zero) is zero
            ,
          [mult_succ]
            all n1, n2 : N :-
            mult(n1, succ(n2)) is plus(mult(n1, n2), n1)

    end

     через 1 обозначим символ succ(zero) и  покажем,  что  любое
                                8
                                 

число из N может быть представлено в виде
   plus(1,plus(1,...,plus(1,1)...))

     Рассмотрим succ(1). По аксиоме plus\_zero
 succ(1)  = succ(plus(1,zero)
По аксиоме plus\_succ
 succ(plus(1,zero) = plus(1, succ(zero)) = plus( 1, 1)
то есть,
  [2]
  succ(1) = plus(1,1)
Следующее число succ(succ(1)). По доказанному равенству 2
  succ(succ(1)) = succ(plus(1,1))
Далее по plus\_succ и по 2 получаем
  [2_1]
  succ(plus(1,1)) = plus (1, succ(1)) = plus(1, plus(1,1))
В сухом остатке равенство
 [3]
 succ(succ(1)) =  plus(1, plus(1,1))
Последний раз для числа succ(succ(succ(1)))
 succ(succ(succ(1))) = succ( plus(1, plus(1,1)))
и с учетом 2\_1
  succ( plus(1, plus(1,1))) = plus (1, succ(plus(1,1))) =
             = plus(1, plus(1, plus(1,1)))

     По видимому, не  затруднит  применить  принцип  матиндукции
(аксиома induction) и доказать требуемое свойство.
 

[first_is_zero]
         ,[linear_order]
         , [induction]

....
     В этой версии будем  строить  множество  натуральных  чисел
начиная с 0.
...

scheme NAT =
    extend PEANO with
    class
        value
          plus : N >< N -> N    -- вводим функции (операции)  сложить
          ,
          mult : N >< N -> N    -- и умножить
        axiom
          [plus_zero]
            all n : N :-
            plus(n, zero) is n
            ,
          [plus_succ]
            all n1, n2 : N :-
            plus(n1, succ(n2)) is succ(plus(n1, n2))
            ,
          [mult_zero]
            all n : N :-
            mult(n, zero) is zero
            ,
          [mult_succ]
            all n1, n2 : N :-
            mult(n1, succ(n2)) is plus(mult(n1, n2), n1)

    end

NAT
scheme Z =
    extend NAT with
    class
        value
          minus : N  -> N    -- вводим обратный элемент
        axiom
          [minus_zero]
            minus( zero) is zero      -- -0 = 0
         ,[plus_minus2]
            all n1, n2 : N :-         -- (-n1)+(-n2) = -(n1+n2)
            plus(minus(n1), minus(n2)) is minus(plus(n1, n2))
         ,[plus_minus1]                -- n + (-n) = 0
            all n : N :-   plus(n, minus(n)) is zero
         ,[minus_minus]                --  -(-n) = n
            all n : N :-    minus(minus(n)) is n
    end

UInt a =  1 ;
Int b = a;
b-= 2 ;   // хрясь,  и нога пополам.  1 - 2  взято из ребенка UInt и не определено