Acciones

Diferencia entre revisiones de «Relación 7»

De Razonamiento automático (2014-15)
Línea 260: Línea 260:
 
   ---------------------------------------------------------------------  
 
   ---------------------------------------------------------------------  
 
*}
 
*}
−
 
 
--"jeshorcob,davoremar"
 
--"jeshorcob,davoremar"
 
fun raiz :: "'a arbol ⇒ 'a" where
 
fun raiz :: "'a arbol ⇒ 'a" where
 
   "raiz (H x) = x"
 
   "raiz (H x) = x"
 
  |"raiz (N x _ _ ) = x"
 
  |"raiz (N x _ _ ) = x"
 +
 +
--"juacorvic"
 +
fun raiz :: "'a arbol ⇒ 'a" where
 +
  "raiz (H x) = x"
 +
|  "raiz (N x yy zz) = x"
 +
 +
(*juacorvic: A partir de aquí en mis definiciones cambio variables por _ .
 +
Pero, ¿Existe alguna diferencia si usamos variables en vez de _?, ¿Es
 +
solo por ahorrarnos escribir?
 +
*)
  
 
value "raiz (N e (N c (H a) (H d)) (N g (H f) (H h))) = e" -- "True"
 
value "raiz (N e (N c (H a) (H d)) (N g (H f) (H h))) = e" -- "True"
Línea 278: Línea 287:
 
*}
 
*}
  
−
--"jeshorcob,davoremar"
+
--"jeshorcob,davoremar,juacorvic"
 
fun extremo_izquierda :: "'a arbol ⇒ 'a" where
 
fun extremo_izquierda :: "'a arbol ⇒ 'a" where
 
   "extremo_izquierda (H x) = x"
 
   "extremo_izquierda (H x) = x"
Línea 295: Línea 304:
 
*}
 
*}
  
−
--"jeshorcob,davoremar"
+
--"jeshorcob,davoremar,juacorvic"
 
fun extremo_derecha :: "'a arbol ⇒ 'a" where
 
fun extremo_derecha :: "'a arbol ⇒ 'a" where
 
   "extremo_derecha (H x) = x"
 
   "extremo_derecha (H x) = x"
Línea 309: Línea 318:
 
*}
 
*}
  
−
--"jeshorcob,davoremar"
+
--"jeshorcob,davoremar,juacorvic"
 
(*jeshorcob: al intentar hacer la prueba automática, el sistema se  
 
(*jeshorcob: al intentar hacer la prueba automática, el sistema se  
 
pregunta por el caso en el que la lista sea vacía. Debemos indicar que
 
pregunta por el caso en el que la lista sea vacía. Debemos indicar que
Línea 316: Línea 325:
 
by (induct a, simp_all)
 
by (induct a, simp_all)
  
−
--"jeshorcob,davoremar"
+
--"jeshorcob,davoremar,juacorvic"
 
theorem "last (inOrden a) = extremo_derecha a"
 
theorem "last (inOrden a) = extremo_derecha a"
 
by (induct a, simp_all add: a1)
 
by (induct a, simp_all add: a1)
  
−
--"jeshorcob,davoremar"
+
--"jeshorcob,davoremar,juacorvic"
 
lemma  "inOrden a ≠ []"
 
lemma  "inOrden a ≠ []"
 
proof (induct a)
 
proof (induct a)
Línea 343: Línea 352:
 
   finally show "?P (N x y z)" by simp
 
   finally show "?P (N x y z)" by simp
 
qed
 
qed
 +
 +
--"juacorvic:(En mi demostración no uso patrones y no consigo demostrar)"
 +
theorem "last (inOrden a) = extremo_derecha a"
 +
proof (induct a)
 +
  fix a::"'a"
 +
  show "last (inOrden (H a)) = extremo_derecha (H a)" by simp
 +
next
 +
  fix a1::"'a"
 +
  fix a2 a3::"'a arbol"
 +
  assume  h1: "last (inOrden a2) = extremo_derecha a2"
 +
  assume  h2: "last (inOrden a3) = extremo_derecha a3"
 +
  have "last (inOrden (N a1 a2 a3)) = last(inOrden a2 @[a1]@ inOrden a3)"
 +
        by simp
 +
  then have "... = last (inOrden a3)" by (simp add: a1)
 +
  then have "... = extremo_derecha a3" using h2 by simp
 +
  thus "last (inOrden(N a1 a2 a3))=extremo_derecha(N a1 a2 a3)" by simp
 +
qde
 +
oops
  
 
--"Pedrosrei"
 
--"Pedrosrei"

Revisión del 10:22 3 dic 2014

header {* R7: Recorridos de árboles *}

theory R7
imports Main 
begin 

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 1. Definir el tipo de datos arbol para representar los
  árboles binarios que tiene información en los nodos y en las hojas. 
  Por ejemplo, el árbol
          e
         / \
        /   \
       c     g
      / \   / \
     a   d f   h 
  se representa por "N e (N c (H a) (H d)) (N g (H f) (H h))".
  --------------------------------------------------------------------- 
*}

datatype 'a arbol = H "'a" | N "'a" "'a arbol" "'a arbol"

value "N e (N c (H a) (H d)) (N g (H f) (H h))" 

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 2. Definir la función 
     preOrden :: "'a arbol ⇒ 'a list"
  tal que (preOrden a) es el recorrido pre orden del árbol a. Por
  ejemplo, 
     preOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
     = [e,c,a,d,g,f,h] 
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic"
fun preOrden :: "'a arbol ⇒ 'a list" where
  "preOrden (H x) = [x]"
 |"preOrden (N x yy zz) = x#(preOrden yy @ preOrden zz)"

value "preOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
 = [e,c,a,d,g,f,h]" -- "True"

value "preOrden (N e (N c (N a1 (H a2) (H a3)) (H d)) (N g (H f) (H h))) 
 = [e, c, a1, a2, a3, d, g, f, h]" -- "True"

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 3. Definir la función 
     postOrden :: "'a arbol ⇒ 'a list"
  tal que (postOrden a) es el recorrido post orden del árbol a. Por
  ejemplo, 
     postOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
     = [a,d,c,f,h,g,e]
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic"
fun postOrden :: "'a arbol ⇒ 'a list" where
  "postOrden (H x) = [x]"
 |"postOrden (N x yy zz)= postOrden yy @ postOrden zz @ [x]"

value "postOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
 = [a,d,c,f,h,g,e]" -- "True"

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 4. Definir la función 
     inOrden :: "'a arbol ⇒ 'a list"
  tal que (inOrden a) es el recorrido in orden del árbol a. Por
  ejemplo, 
     inOrden (N e (N c (H a) (H d)) (N g (H f) (H h)))
     = [a,c,d,e,f,g,h]
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic"
fun inOrden :: "'a arbol ⇒ 'a list" where
  "inOrden (H x) = [x]"
 |"inOrden (N x yy zz) = inOrden yy @ [x] @ inOrden zz"

value "inOrden (N e (N c (H a) (H d)) (N g (H f) (H h))) 
 = [a,c,d,e,f,g,h]" -- "True"

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 5. Definir la función 
     espejo :: "'a arbol ⇒ 'a arbol"
  tal que (espejo a) es la imagen especular del árbol a. Por ejemplo, 
     espejo (N e (N c (H a) (H d)) (N g (H f) (H h)))
     = N e (N g (H h) (H f)) (N c (H d) (H a))
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic"
fun espejo :: "'a arbol ⇒ 'a arbol" where
  "espejo (H x) = (H x)"
 |"espejo (N x yy zz) = (N x (espejo zz) (espejo yy))"

value "espejo (N e (N c (H a) (H d)) (N g (H f) (H h)))
 = N e (N g (H h) (H f)) (N c (H d) (H a))" -- "True"

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 6. Demostrar que
     preOrden (espejo a) = rev (postOrden a)
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic"
lemma  "preOrden (espejo a) = rev (postOrden a)"
by (induct a, simp_all)

--"jeshorcob,davoremar"
lemma  "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
  fix x show "?P (H x)" by simp
next
  fix x yy zz
  assume h1: "?P yy"
  assume h2: "?P zz"
  have "preOrden (espejo (N x yy zz))
    = preOrden (N x (espejo zz) (espejo yy))" by simp
  also have "... = x#(preOrden(espejo zz)@preOrden(espejo yy))" by simp
  also have "... = x#rev(postOrden zz)@rev(postOrden yy)" 
    using h1 h2 by simp
  also have "... = rev((postOrden yy)@(postOrden zz)@[x])" by simp
  finally show "?P (N x yy zz)" by simp
qed

-- "juacorvic (Igual pero un paso más. Se usan variables sugeridas)" 
lemma  "preOrden (espejo a) = rev (postOrden a)" (is "?P a")
proof (induct a)
  fix a
  show "?P (H a)" by simp
next
  fix a1 a2 a3
  assume h1: "?P a2"
  assume h2: "?P a3"
  have "preOrden (espejo (N a1 a2 a3)) = preOrden (N a1 (espejo a3) 
     (espejo a2))" by simp
  also have "... = a1#(preOrden (espejo a3) @ preOrden (espejo a2))"
      by simp 
  also have "... = a1#(rev (postOrden a3) @ rev(postOrden a2))" 
      using h1 h2 by simp
  also have "... = rev( (postOrden a2) @ (postOrden a3) @[a1] )" 
       by simp 
  also have "... = rev (postOrden (N a1 a2 a3))" by simp
  finally show "?P (N a1 a2 a3)" by simp
qed



text {*  
  --------------------------------------------------------------------- 
  Ejercicio 7. Demostrar que
     postOrden (espejo a) = rev (preOrden a)
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic"
lemma "postOrden (espejo a) = rev (preOrden a)"
by (induct a, simp_all)

--"jeshorcob,davoremar"
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof (induct a)
  fix x show "?P (H x)" by simp
next
  fix x y z
  assume h1: "?P y"
  assume h2: "?P z"
  have "postOrden (espejo (N x y z)) = 
    postOrden (N x (espejo z) (espejo y))" by simp
  also have "... = postOrden(espejo z)@postOrden(espejo y)@[x]" by simp
  also have "... = rev(preOrden z)@rev(preOrden y)@[x]" 
    using h1 h2 by simp
  also have "... = rev(x#(preOrden y)@(preOrden z))" by simp
  finally show "?P (N x y z)" by simp
qed

-- "juacorvic (Igual pero un paso más. Se usan variables sugeridas)" 
lemma "postOrden (espejo a) = rev (preOrden a)" (is "?P a")
proof  (induct a)
  fix a
  show "?P (H a)" by simp
next
  fix a1 a2 a3
  assume h1: "?P a2"
  assume h2: "?P a3"
  have "postOrden (espejo (N a1 a2 a3)) = postOrden (N a1 (espejo a3) 
      (espejo a2))" by simp
  also have "... = postOrden (espejo a3) @  postOrden (espejo a2) @ [a1]" 
       by simp
  also have "... = rev (preOrden a3) @ rev (preOrden a2) @ [a1]" 
       using h1 h2 by simp
  also have "... = rev(a1#(preOrden a2)@(preOrden a3))" by simp
  also have "... = rev(preOrden (N a1 a2 a3))" by simp  
  finally show "?P (N a1 a2 a3)" by simp
qed


text {*  
  --------------------------------------------------------------------- 
  Ejercicio 8. Demostrar que
     inOrden (espejo a) = rev (inOrden a)
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic"
theorem "inOrden (espejo a) = rev (inOrden a)"
by (induct a, simp_all)

--"jeshorcob,davoremar"
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
  fix x show "?P (H x)" by simp
next
  fix x y z
  assume h1: "?P y"
  assume h2: "?P z"
  have "inOrden(espejo (N x y z)) = 
    inOrden(N x (espejo z) (espejo y))" by simp
  also have "... = inOrden(espejo z)@[x]@inOrden(espejo y)" by simp
  also have "... = rev(inOrden z)@[x]@rev(inOrden y)" using h1 h2 by simp
  also have "... = rev(inOrden y @ [x] @ inOrden z)" by simp
  finally show "?P (N x y z)" by simp
qed

-- "juacorvic (Igual pero un paso más. Se usan variables sugeridas)" 
theorem "inOrden (espejo a) = rev (inOrden a)" (is "?P a")
proof (induct a)
  fix a
  show "?P (H a)" by simp
next
  fix a1 a2 a3
  assume h1: "?P a2"
  assume h2: "?P a3"
  have "inOrden (espejo (N a1 a2 a3)) = inOrden (N a1 (espejo a3) 
     (espejo a2))" by simp
  also have "... = inOrden (espejo a3) @ [a1] @ inOrden (espejo a2)"
      by simp
  also have "... = rev (inOrden a3) @ [a1] @ rev (inOrden a2)" 
      using h1 h2 by simp
  also have "... = rev (inOrden a2 @ [a1] @ inOrden a3)" by simp
  also have "... = rev (inOrden (N a1 a2 a3))" by simp
  finally show "?P (N a1 a2 a3)" by simp
qed



text {*  
  --------------------------------------------------------------------- 
  Ejercicio 9. Definir la función 
     raiz :: "'a arbol ⇒ 'a"
  tal que (raiz a) es la raiz del árbol a. Por ejemplo, 
     raiz (N e (N c (H a) (H d)) (N g (H f) (H h))) = e
  --------------------------------------------------------------------- 
*}
--"jeshorcob,davoremar"
fun raiz :: "'a arbol ⇒ 'a" where
  "raiz (H x) = x"
 |"raiz (N x _ _ ) = x"

--"juacorvic"
fun raiz :: "'a arbol ⇒ 'a" where
   "raiz (H x) = x"
|  "raiz (N x yy zz) = x"

(*juacorvic: A partir de aquí en mis definiciones cambio variables por _ .
Pero, ¿Existe alguna diferencia si usamos variables en vez de _?, ¿Es 
solo por ahorrarnos escribir?
*)

value "raiz (N e (N c (H a) (H d)) (N g (H f) (H h))) = e" -- "True"

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 10. Definir la función 
     extremo_izquierda :: "'a arbol ⇒ 'a"
  tal que (extremo_izquierda a) es el nodo más a la izquierda del árbol
  a. Por ejemplo,  
     extremo_izquierda (N e (N c (H a) (H d)) (N g (H f) (H h))) = a
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic"
fun extremo_izquierda :: "'a arbol ⇒ 'a" where
  "extremo_izquierda (H x) = x"
 |"extremo_izquierda (N _ yy _) = extremo_izquierda yy"

value "extremo_izquierda (N e (N c (H a) (H d)) (N g (H f) (H h)))" -- "= a"

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 11. Definir la función 
     extremo_derecha :: "'a arbol ⇒ 'a"
  tal que (extremo_derecha a) es el nodo más a la derecha del árbol
  a. Por ejemplo,  
     extremo_derecha (N e (N c (H a) (H d)) (N g (H f) (H h))) = h
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic"
fun extremo_derecha :: "'a arbol ⇒ 'a" where
  "extremo_derecha (H x) = x"
 |"extremo_derecha (N _ _ zz) = extremo_derecha zz"

value "extremo_derecha (N e (N c (H a) (H d)) (N g (H f) (H h)))" -- "= h"

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 12. Demostrar o refutar
     last (inOrden a) = extremo_derecha a
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar,juacorvic"
(*jeshorcob: al intentar hacer la prueba automática, el sistema se 
pregunta por el caso en el que la lista sea vacía. Debemos indicar que
esto no puede ocurrir y para ello añadimos un lema auxiliar.*)
lemma a1: "inOrden a ≠ []"
by (induct a, simp_all)

--"jeshorcob,davoremar,juacorvic"
theorem "last (inOrden a) = extremo_derecha a"
by (induct a, simp_all add: a1)

--"jeshorcob,davoremar,juacorvic"
lemma  "inOrden a ≠ []"
proof (induct a)
  fix x::"'a" show "inOrden (H x) ≠ []" by simp
next
  fix x::"'a" and y z::"'a arbol"
  assume h1: "inOrden y ≠ []"
  assume h2: "inOrden z ≠ []"
  show "inOrden (N x y z) ≠ []" using h1 h2 by simp  
qed

--"jeshorcob,davoremar"
theorem "last (inOrden a) = extremo_derecha a" (is "?P a")
proof (induct a)
  fix x show "?P (H x)" by simp
next
  fix x y z
  assume h2: "?P z"
  have "last(inOrden(N x y z))=last(inOrden y @[x]@ inOrden z)" by simp
  also have "... = last(inOrden z)" by (simp add: a1)
  also have "... = extremo_derecha z" using h2 by simp
  finally show "?P (N x y z)" by simp
qed

--"juacorvic:(En mi demostración no uso patrones y no consigo demostrar)" 
theorem "last (inOrden a) = extremo_derecha a"
proof (induct a)
  fix a::"'a"
  show "last (inOrden (H a)) = extremo_derecha (H a)" by simp
next
  fix a1::"'a"
  fix a2 a3::"'a arbol" 
  assume  h1: "last (inOrden a2) = extremo_derecha a2"
  assume  h2: "last (inOrden a3) = extremo_derecha a3"
  have "last (inOrden (N a1 a2 a3)) = last(inOrden a2 @[a1]@ inOrden a3)" 
        by simp
  then have "... = last (inOrden a3)" by (simp add: a1)
  then have "... = extremo_derecha a3" using h2 by simp
  thus "last (inOrden(N a1 a2 a3))=extremo_derecha(N a1 a2 a3)" by simp
qde
oops

--"Pedrosrei"
theorem "last (inOrden a) = extremo_derecha a"
apply (induct a, simp_all) apply (metis append_is_Nil_conv arbol.exhaust
  inOrden.simps(1) inOrden.simps(2) list.distinct(1)) done

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 13. Demostrar o refutar
     hd (inOrden a) = extremo_izquierda a
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar"
(*jeshorcob: aquí necesitamos el mismo lema por un motivo similar*)
theorem "hd (inOrden a) = extremo_izquierda a"
by (induct a, simp_all add: a1)

--"jeshorcob,davoremar"
theorem "hd (inOrden a) = extremo_izquierda a" (is "?P a")
proof (induct a)
  fix x show "?P (H x)" by simp
next
  fix x y z
  assume h1: "?P y"
  have "hd(inOrden(N x y z))=hd(inOrden y @[x]@ inOrden z)" by simp
  also have "... = hd(inOrden y)" by (simp add: a1)
  also have "... = extremo_izquierda y" using h1 by simp
  finally show "?P (N x y z)" by simp
qed

--"Pedrosrei"
theorem "hd (inOrden a) = extremo_izquierda a"
apply (induct a, simp_all) apply (metis Nil_is_append_conv
  extremo_izquierda.cases hd_append inOrden.simps(1) inOrden.simps(2)
  list.distinct(1)) done

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 14. Demostrar o refutar
     hd (preOrden a) = last (postOrden a)
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar"
theorem "hd (preOrden a) = last (postOrden a)"
by (induct a, simp_all)

--"jeshorcob,davoremar"
theorem "hd (preOrden a) = last (postOrden a)" (is "?P a")
proof (induct a)
  fix x show "?P (H x)" by simp
next
  fix x::"'a" and y z
  have "hd(preOrden(N x y z)) = hd(x#(preOrden y @ preOrden z))" by simp
  also have "... = x" by simp
  also have "... = last(postOrden y @ postOrden z @[x])" by simp
  finally show "?P (N x y z)" by simp
qed

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 15. Demostrar o refutar
     hd (preOrden a) = raiz a
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar"
theorem "hd (preOrden a) = raiz a"
by (induct a, simp_all)

--"jeshorcob,davoremar"
theorem "hd (preOrden a) = raiz a" (is "?P a")
proof (induct a)
  fix x show "?P (H x)" by simp
next
  fix x::"'a" and y z
  have "hd(preOrden(N x y z)) = hd(x#(preOrden y @ preOrden z))" by simp
  also have "... = x" by simp
  finally show "?P (N x y z)" by simp
qed

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 16. Demostrar o refutar
     hd (inOrden a) = raiz a
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar"
theorem "hd (inOrden a) = raiz a"
quickcheck
oops
(*Encuentra el contrajemplo:
a = N a⇩1 (H a⇩2) (H a⇩1)

ya que evaluando se ve que son distindos:
hd (inOrden a) = a⇩2
raiz a = a⇩1
*)

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 17. Demostrar o refutar
     last (postOrden a) = raiz a
  --------------------------------------------------------------------- 
*}

--"jeshorcob,davoremar"
theorem "last (postOrden a) = raiz a"
by (induct a, simp_all)

--"jeshorcob,davoremar"
theorem "last (postOrden a) = raiz a" (is "?P a")
proof (induct a)
  fix x show "?P (H x)" by simp
next
  fix x::"'a" and y z
  have "last(postOrden(N x y z)) = 
    last(postOrden y @ postOrden z @ [x])" by simp
  also have "... = x" by simp
  finally show "?P (N x y z)" by simp
qed

end
Obtenido de «https://www.glc.us.es/~jalonso/RA2014/index.php?title=Relación_7&oldid=191»