Acciones

Diferencia entre revisiones de «R6»

De Razonamiento automático (2014-15)

(Página creada con '<source lang="isar"> header {* R6: Sustitución, inversión y eliminación *} theory R6_Sustitucion_inversion_y_eliminacion imports Main begin text {* Nota: En esta relaci...')
 
m (Texto reemplazado: «"isar"» por «"isabelle"»)
 
(No se muestran 2 ediciones intermedias de otro usuario)
Línea 1: Línea 1:
−
<source lang="isar">
+
<source lang="isabelle">
 
header {* R6: Sustitución, inversión y eliminación *}
 
header {* R6: Sustitución, inversión y eliminación *}
  
Línea 13: Línea 13:
 
   ---------------------------------------------------------------------  
 
   ---------------------------------------------------------------------  
 
   Ejercicio 1. Definir la función  
 
   Ejercicio 1. Definir la función  
−
     sust :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+
     sust :: "'a ⇒ 'a ⇒ 'a list ⇒ 'a list"
 
   tal que (sust x y zs) es la lista obtenida sustituyendo cada
 
   tal que (sust x y zs) es la lista obtenida sustituyendo cada
 
   occurrencia de x por y en la lista zs. Por ejemplo,
 
   occurrencia de x por y en la lista zs. Por ejemplo,
Línea 20: Línea 20:
 
*}
 
*}
  
−
fun sust :: "'a \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+
fun sust :: "'a ⇒ 'a ⇒ 'a list ⇒ 'a list" where
 
   "sust x y zs = undefined"
 
   "sust x y zs = undefined"
  
Línea 70: Línea 70:
 
   ---------------------------------------------------------------------  
 
   ---------------------------------------------------------------------  
 
   Ejercicio 6. Definir la función
 
   Ejercicio 6. Definir la función
−
     borra :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+
     borra :: "'a ⇒ 'a list ⇒ 'a list"
 
   tal que (borra x ys) es la lista obtenida borrando la primera
 
   tal que (borra x ys) es la lista obtenida borrando la primera
 
   ocurrencia del elemento x en la lista ys. Por ejemplo,
 
   ocurrencia del elemento x en la lista ys. Por ejemplo,
Línea 79: Línea 79:
 
*}
 
*}
  
−
fun borra :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+
fun borra :: "'a ⇒ 'a list ⇒ 'a list" where
 
   "borra x ys = undefined"
 
   "borra x ys = undefined"
  
Línea 87: Línea 87:
 
   ---------------------------------------------------------------------  
 
   ---------------------------------------------------------------------  
 
   Ejercicio 7. Definir la función
 
   Ejercicio 7. Definir la función
−
     borraTodas :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+
     borraTodas :: "'a ⇒ 'a list ⇒ 'a list"
 
   tal que (borraTodas x ys) es la lista obtenida borrando todas las
 
   tal que (borraTodas x ys) es la lista obtenida borrando todas las
 
   ocurrencias del elemento x en la lista ys. Por ejemplo,
 
   ocurrencias del elemento x en la lista ys. Por ejemplo,
Línea 94: Línea 94:
 
*}
 
*}
  
−
fun borraTodas :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
+
fun borraTodas :: "'a ⇒ 'a list ⇒ 'a list" where
 
   "borraTodas x ys = undefined"
 
   "borraTodas x ys = undefined"
  
Línea 221: Línea 221:
 
oops
 
oops
  
−
end  
+
end </source>
−
</source>
 

Revisión actual del 10:18 16 jul 2018

header {* R6: Sustitución, inversión y eliminación *}

theory R6_Sustitucion_inversion_y_eliminacion
imports Main 
begin

text {*
  Nota: En esta relación se pide hacer las demostraciones de forma 
  automática. *} 

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 1. Definir la función 
     sust :: "'a ⇒ 'a ⇒ 'a list ⇒ 'a list"
  tal que (sust x y zs) es la lista obtenida sustituyendo cada
  occurrencia de x por y en la lista zs. Por ejemplo,
     sust (1::int) 2 [1,2,3,4,1,2,3,4] = [2,2,3,4,2,2,3,4]
  --------------------------------------------------------------------- 
*}

fun sust :: "'a ⇒ 'a ⇒ 'a list ⇒ 'a list" where
  "sust x y zs = undefined"

value "sust (1::int) 2 [1,2,3,4,1,2,3,4]" -- "= [2,2,3,4,2,2,3,4]"

text {*
  --------------------------------------------------------------------- 
  Ejercicio 2. Demostrar o refutar 
     sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"
  ---------------------------------------------------------------------  
*}

lemma sust_append: 
  "sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 3. Demostrar o refutar 
     rev (sust x y zs) = sust x y (rev zs)
  --------------------------------------------------------------------- 
*}

lemma rev_sust: 
  "rev(sust x y zs) = sust x y (rev zs)"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 4. Demostrar o refutar:
     sust x y (sust u v zs) = sust u v (sust x y zs)
  --------------------------------------------------------------------- 
*}

lemma "sust x y (sust u v zs) = sust u v (sust x y zs)"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 5. Demostrar o refutar:
     sust y z (sust x y zs) = sust x z zs
  --------------------------------------------------------------------- 
*}

lemma "sust y z (sust x y zs) = sust x z zs"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 6. Definir la función
     borra :: "'a ⇒ 'a list ⇒ 'a list"
  tal que (borra x ys) es la lista obtenida borrando la primera
  ocurrencia del elemento x en la lista ys. Por ejemplo,
     borra (2::int) [1,2,3,2] = [1,3,2]

  Nota: La función borra es equivalente a la predefinida remove1. 
  --------------------------------------------------------------------- 
*}

fun borra :: "'a ⇒ 'a list ⇒ 'a list" where
  "borra x ys = undefined"

value "borra (2::int) [1,2,3,2]" -- "= [1,3,2]"

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 7. Definir la función
     borraTodas :: "'a ⇒ 'a list ⇒ 'a list"
  tal que (borraTodas x ys) es la lista obtenida borrando todas las
  ocurrencias del elemento x en la lista ys. Por ejemplo,
     borraTodas (2::int) [1,2,3,2] = [1,3]
  --------------------------------------------------------------------- 
*}

fun borraTodas :: "'a ⇒ 'a list ⇒ 'a list" where
  "borraTodas x ys = undefined"

value "borraTodas (2::int) [1,2,3,2]" -- "= [1,3]"

text {*
  --------------------------------------------------------------------- 
  Ejercicio 8. Demostrar o refutar 
     borra x (borraTodas x xs) = borraTodas x xs
  --------------------------------------------------------------------- 
*}

lemma "borra x (borraTodas x xs) = borraTodas x xs"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 9. Demostrar o refutar 
     borraTodas x (borraTodas x xs) = borraTodas x xs
  --------------------------------------------------------------------- 
*}

lemma "borraTodas x (borraTodas x xs) = borraTodas x xs"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 10. Demostrar o refutar automáticamente
     borraTodas x (borra x xs) = borraTodas x xs
  --------------------------------------------------------------------- 
*}

lemma borraTodas_borra: 
  "borraTodas x (borra x xs) = borraTodas x xs"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 11. Demostrar o refutar 
     borra x (borra y xs) = borra y (borra x xs)
  --------------------------------------------------------------------- 
*}

lemma "borra x (borra y xs) = borra y (borra x xs)"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 12. Demostrar o refutar automáticamente
     borraTodas x (borra y xs) = borra y (borraTodas x xs)
  --------------------------------------------------------------------- 
*}

lemma "borraTodas x (borra y xs) = borra y (borraTodas x xs)"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 13. Demostrar o refutar:
     borra y (sust x y xs) = borra x xs
  --------------------------------------------------------------------- 
*}

lemma "borra y (sust x y xs) = borra x xs"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 14. Demostrar o refutar:
     borraTodas y (sust x y xs) = borraTodas x xs"
  --------------------------------------------------------------------- 
*}

lemma "borraTodas y (sust x y xs) = borraTodas x xs"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 15. Demostrar o refutar 
     sust x y (borraTodas x zs) = borraTodas x zs
  --------------------------------------------------------------------- 
*}

lemma "sust x y (borraTodas x zs) = borraTodas x zs"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 16. Demostrar o refutar
     sust x y (borraTodas z zs) = borraTodas z (sust x y zs)
  --------------------------------------------------------------------- 
*}

lemma "sust x y (borraTodas z zs) = borraTodas z (sust x y zs)"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 17. Demostrar o refutar:
     rev (borra x xs) = borra x (rev xs)
  --------------------------------------------------------------------- 
*}

lemma "rev (borra x xs) = borra x (rev xs)"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 18. Demostrar o refutar 
     borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)
  --------------------------------------------------------------------- 
*}

lemma borraTodas_append:
  "borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 19. Demostrar o refutar 
     rev (borraTodas x xs) = borraTodas x (rev xs)
  --------------------------------------------------------------------- 
*}

lemma "rev (borraTodas x xs) = borraTodas x (rev xs)"
oops

end
Obtenido de «https://www.glc.us.es/~jalonso/RA2014/index.php?title=R6&oldid=304»