{-- QUESTÃO 1
Complete a defição do ADT abaixo que deve representar uma árvore binária 
de busca de inteiros onde a função \code{emptyTree} inicializa uma árvore 
vazia (1.0). Defina as funções \code{addElement} (1.0) que insere um 
elemento na árvore, e \code{isInTree} (1.0) que verifica se um elemento 
está na árvore. Defina ainda funções para somar, \code{sumTree} (1.0), e 
dobrar, \code{doubleTree} (1.0) os elementos da árvore.
 --}
module Tree (Tree, emptyTree, addElement, isInTree, sumTree, doubleTree)
  where
  data Tree = Bin Int (Tree) (Tree) | NULL deriving Show
  
  emptyTree :: Tree
  emptyTree = NULL
  
  addElement :: Int -> Tree -> Tree
  addElement v NULL = Bin v NULL NULL
  addElement v (Bin i left right) 
    | v > i     = Bin i left (addElement v right)
    | otherwise = Bin i (addElement v left) right
    
    
  isInTree :: Int -> Tree -> Bool
  isInTree _ NULL = False
  isInTree v (Bin i left right)
    | v == i    = True
    | v > i     = isInTree v right
    | otherwise = isInTree v left

  sumTree :: Tree -> Int
  sumTree NULL = 0
  sumTree (Bin v left right) = v + (sumTree left) + (sumTree right)
  
  doubleTree :: Tree -> Tree
  doubleTree NULL = NULL
  doubleTree (Bin v left right) = Bin (2*v) (doubleTree left) (doubleTree right)

{-- QUESTÃO 2 
Considerando o ADT definido na questão anterior escreva a 
expressão que cria a seguinte árvore:
                4
              /   \
             2     6
            / \   / \
           1   3 5   7
                      \
                       8
                       
--}

addElement 8 (addElement 7 (addElement 5 (addElement 6 (addElement 3 (addElement 1 (addElement 2 (addElement 4 emptyTree))))))) 
  
{--Questão 3
Considerando o ADT definido na questão 1 e suas funções prove que 
sumTree (doubleTree x) = 2 * (sumTree x) para todas as árvores x finitas.

Caso base x = NULL

Passo da indução x = Bin y left right
assumindo que é válido para left e right ou seja
    sumTree (doubleTree left) = 2 * (sumTree left)
    e
    sumTree (doubleTree right) = 2 * (sumTree right)

Caso base 
sumTree (doubleTree NULL) = 2* sumTree NULL

sumTree (doubleTree NULL) 
  = sumTree NULL                (pela definição de doubleTree)
  = 0                           (pela definição de sumTree)
  
2 * sumTree NULL
  = 2 * 0                       (pela definição de sumTree)
  = 0                           (pela aritmética)

Passo indutivo 
sumTree (doubleTree (Bin y left right)) = 2 * sumTree (Bin y left right)


sumTree (doubleTree (Bin y left right)) 
  = sumTree (Bin (2*y) (doubleTree left) (doubleTree right))        (pela definição de doubleTree)
  = 2*y + sumTree (doubleTree left) + sumTree (doubleTree right)    (pela definição de sumTree)
  = 2*y + 2 * sumTree left + 2 * sumTree right                      (pela hipótese da indução)
  = 2 * (y + sumTree left + sumTree right)                          (pela aritmética)
  = 2 * sumTree (Bin y left right)                                  (pela definição de sumTree)

PROVADO
--}

{--QUESTÃO 4

O que devemos acrescentar na prova acima para provar que a 
propriedade é válida para todas as árvores incluindo as 
infinitas? Por que? Complete então a prova para todas as 
árvores incluindo as infinitas.

Devemos acrescentar undef ao caso base, de modo a mostrar
que a prova é válida para todas as aproximações de árvores infinitas,
como undef, Bin 4 (undef) (undef), Bin 4 (undef) (Bin 5 undef undef),
Bin 4 (Bin 3 undef undef) (Bin 5 undef undef), etc.

Caso base x = undef

sumTree (doubleTree undef) = 2* sumTree undef

sumTree (doubleTree undef) 
  = sumTree undef               (por undef)
  = undef                       (por undef)
   
2 * sumTree undef
  = 2 * undef                   (por undef)
  = undef                       (por undef)

--}