Acciones

Diferencia entre revisiones de «Relación 4»

De Razonamiento automático (2017-18)

(Página creada con '<source lang="isar"> chapter {* R4: Cuantificadores sobre listas *} theory R4_Cuantificadores_sobre_listas imports Main begin text {* -------------------------------------...')
 
Línea 19: Línea 19:
 
*}
 
*}
  
 +
(*anddonram*)
 
fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
 
fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
−
   "todos p xs = undefined"
+
   "todos p [] = True"
 +
| "todos p (x#xs) = (p x ∧ todos p xs)"
  
 
text {*  
 
text {*  
Línea 35: Línea 37:
 
*}
 
*}
  
 +
(*anddonram*)
 
fun algunos  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
 
fun algunos  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
−
   "algunos p xs = undefined"
+
   "algunos p [] = False"
 +
|  "algunos p (x#xs) = (p x ∨ algunos p xs)"
  
 
text {*
 
text {*
Línea 44: Línea 48:
 
   ---------------------------------------------------------------------  
 
   ---------------------------------------------------------------------  
 
*}
 
*}
−
 
+
(*anddonram*)
 
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
 
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
−
oops
+
  by (induct xs) auto
 +
  
 
text {*
 
text {*
Línea 55: Línea 60:
 
*}
 
*}
  
 +
 +
(*anddonram[conmutatividad and porque no sé hacerlo de otra forma] *)
 +
lemma and_comm: "(a ∧ b) = (b ∧ a)"
 +
  by (cases a) auto
 +
 +
(*anddonram*)
 
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
 
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
−
oops
+
proof (induct xs)
 +
  show "todos (λx. P x ∧ Q x) [] = (todos P [] ∧ todos Q [])" by simp
 +
next
 +
  fix a xs
 +
  assume HI:"todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
 +
  have "todos (λx. P x ∧ Q x) (a # xs) = (P a ∧ Q a ∧ todos (λx. P x ∧ Q x) xs)" by simp
 +
  also have "... = (P a ∧ Q a ∧ todos P xs ∧ todos Q xs)" using HI by simp
 +
  also have "... = (P a ∧ Q a ∧ todos Q xs ∧ todos P xs)" by (simp add:and_comm)
 +
  also have "... = (P a ∧ todos Q (a # xs) ∧ todos P xs)" by simp
 +
  also have "... = (P a ∧ todos P xs ∧ Q a ∧ todos Q xs)" by (simp add:and_comm)
 +
  finally show "todos (λx. P x ∧ Q x) (a # xs) = (todos P (a # xs) ∧ todos Q (a # xs))"
 +
    by simp
 +
qed
  
 
text {*
 
text {*
Línea 65: Línea 88:
 
*}
 
*}
  
 +
(*anddonram*)
 
lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
 
lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
−
oops
+
  by (induct x) auto
 +
  
 
text {*
 
text {*

Revisión del 13:16 2 dic 2017

chapter {* R4: Cuantificadores sobre listas *}

theory R4_Cuantificadores_sobre_listas
imports Main 
begin

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 1. Definir la función 
     todos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
  tal que (todos p xs) se verifica si todos los elementos de la lista 
  xs cumplen la propiedad p. Por ejemplo, se verifica 
     todos (λx. 1<length x) [[2,1,4],[1,3]]
     ¬todos (λx. 1<length x) [[2,1,4],[3]]

  Nota: La función todos es equivalente a la predefinida list_all. 
  --------------------------------------------------------------------- 
*}

(*anddonram*)
fun todos :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "todos p [] = True"
| "todos p (x#xs) = (p x ∧ todos p xs)"

text {* 
  --------------------------------------------------------------------- 
  Ejercicio 2. Definir la función 
     algunos :: ('a ⇒ bool) ⇒ 'a list ⇒ bool
  tal que (algunos p xs) se verifica si algunos elementos de la lista 
  xs cumplen la propiedad p. Por ejemplo, se verifica 
     algunos (λx. 1<length x) [[2,1,4],[3]]
     ¬algunos (λx. 1<length x) [[],[3]]"

  Nota: La función algunos es equivalente a la predefinida list_ex. 
  --------------------------------------------------------------------- 
*}

(*anddonram*)
fun algunos  :: "('a ⇒ bool) ⇒ 'a list ⇒ bool" where
  "algunos p [] = False"
|  "algunos p (x#xs) = (p x ∨ algunos p xs)"

text {*
  --------------------------------------------------------------------- 
  Ejercicio 3.1. Demostrar o refutar automáticamente 
     todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
  --------------------------------------------------------------------- 
*}
 (*anddonram*)
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
  by (induct xs) auto
 

text {*
  --------------------------------------------------------------------- 
  Ejercicio 3.2. Demostrar o refutar detalladamente
     todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)
  --------------------------------------------------------------------- 
*}


(*anddonram[conmutatividad and porque no sé hacerlo de otra forma] *)
lemma and_comm: "(a ∧ b) = (b ∧ a)"
  by (cases a) auto

(*anddonram*)
lemma "todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
proof (induct xs)
  show "todos (λx. P x ∧ Q x) [] = (todos P [] ∧ todos Q [])" by simp
next 
  fix a xs
  assume HI:"todos (λx. P x ∧ Q x) xs = (todos P xs ∧ todos Q xs)"
  have "todos (λx. P x ∧ Q x) (a # xs) = (P a ∧ Q a ∧ todos (λx. P x ∧ Q x) xs)" by simp
  also have "... = (P a ∧ Q a ∧ todos P xs ∧ todos Q xs)" using HI by simp
  also have "... = (P a ∧ Q a ∧ todos Q xs ∧ todos P xs)" by (simp add:and_comm)
  also have "... = (P a ∧ todos Q (a # xs) ∧ todos P xs)" by simp
  also have "... = (P a ∧ todos P xs ∧ Q a ∧ todos Q xs)" by (simp add:and_comm)
  finally show "todos (λx. P x ∧ Q x) (a # xs) = (todos P (a # xs) ∧ todos Q (a # xs))"
    by simp
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 4.1. Demostrar o refutar automáticamente
     todos P (x @ y) = (todos P x ∧ todos P y)
  --------------------------------------------------------------------- 
*}

(*anddonram*)
lemma "todos P (x @ y) = (todos P x ∧ todos P y)"
  by (induct x) auto
 

text {*
  --------------------------------------------------------------------- 
  Ejercicio 4.2. Demostrar o refutar detalladamente
     todos P (x @ y) = (todos P x ∧ todos P y)
  --------------------------------------------------------------------- 
*}

lemma todos_append:
  "todos P (x @ y) = (todos P x ∧ todos P y)"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 5.1. Demostrar o refutar automáticamente 
     todos P (rev xs) = todos P xs
  --------------------------------------------------------------------- 
*}

lemma "todos P (rev xs) = todos P xs"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 5.2. Demostrar o refutar detalladamente
     todos P (rev xs) = todos P xs
  --------------------------------------------------------------------- 
*}

lemma "todos P (rev xs) = todos P xs"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 6. Demostrar o refutar:
    algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)
  --------------------------------------------------------------------- 
*}

lemma "algunos (λx. P x ∧ Q x) xs = (algunos P xs ∧ algunos Q xs)"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 7.1. Demostrar o refutar automáticamente 
     algunos P (map f xs) = algunos (P ∘ f) xs
  --------------------------------------------------------------------- 
*}

lemma "algunos P (map f xs) = algunos (P o f) xs"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 7.2. Demostrar o refutar datalladamente
     algunos P (map f xs) = algunos (P ∘ f) xs
  --------------------------------------------------------------------- 
*}

lemma "algunos P (map f xs) = algunos (P o f) xs"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 8.1. Demostrar o refutar automáticamente 
     algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
  --------------------------------------------------------------------- 
*}

lemma "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 8.2. Demostrar o refutar detalladamente
     algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)
  --------------------------------------------------------------------- 
*}

lemma algunos_append:
  "algunos P (xs @ ys) = (algunos P xs ∨ algunos P ys)"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 9.1. Demostrar o refutar automáticamente
     algunos P (rev xs) = algunos P xs
  --------------------------------------------------------------------- 
*}

lemma "algunos P (rev xs) = algunos P xs"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 9.2. Demostrar o refutar detalladamente
     algunos P (rev xs) = algunos P xs
  --------------------------------------------------------------------- 
*}

lemma "algunos P (rev xs) = algunos P xs"
oops

text {*
  --------------------------------------------------------------------- 
  Ejercicio 10. Encontrar un término no trivial Z tal que sea cierta la 
  siguiente ecuación:
     algunos (λx. P x ∨ Q x) xs = Z
  y demostrar la equivalencia de forma automática y detallada.
  --------------------------------------------------------------------- 
*}

text {*
  --------------------------------------------------------------------- 
  Ejercicio 11.1. Demostrar o refutar automáticamente
     algunos P xs = (¬ todos (λx. (¬ P x)) xs)
  --------------------------------------------------------------------- 
*}

lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
oops
     
text {*
  --------------------------------------------------------------------- 
  Ejercicio 11.2. Demostrar o refutar datalladamente
     algunos P xs = (¬ todos (λx. (¬ P x)) xs)
  --------------------------------------------------------------------- 
*}

lemma "algunos P xs = (¬ todos (λx. (¬ P x)) xs)"
oops
     
text {*
  --------------------------------------------------------------------- 
  Ejercicio 12. Definir la funcion primitiva recursiva 
     estaEn :: 'a ⇒ 'a list ⇒ bool
  tal que (estaEn x xs) se verifica si el elemento x está en la lista
  xs. Por ejemplo, 
     estaEn (2::nat) [3,2,4] = True
     estaEn (1::nat) [3,2,4] = False
  --------------------------------------------------------------------- 
*}

fun estaEn :: "'a ⇒ 'a list ⇒ bool" where
  "estaEn x xs = undefined"

text {*
  --------------------------------------------------------------------- 
  Ejercicio 13. Expresar la relación existente entre estaEn y algunos. 
  Demostrar dicha relación de forma automática y detallada.
  --------------------------------------------------------------------- 
*}

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