Razonamiento automático (2013-14) Razonamiento automático (2013-14)

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

theory R6
imports Main 
begin

section {* Sustitución, inversión y eliminación *}

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::nat) 2 [1,2,3,4,1,2,3,4] = [2,2,3,4,2,2,3,4]
  --------------------------------------------------------------------- 
*}

-- "maresccas4"

fun sust :: "'a ⇒ 'a ⇒ 'a list ⇒ 'a list" where
  "sust x y [] = []"
| "sust x y (z#zs) = (if z=x then y#sust x y zs else z#sust x y zs)"

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

-- "maresccas4"

lemma 
  "sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"
  by (induct xs) auto

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

-- "maresccas4"

lemma sust_append: 
  "sust x y (xs@ys) = (sust x y xs)@(sust x y ys)" (is "?P x y xs ys")
proof (induct xs)
 show "?P x y [] ys" by simp
next 
 fix a :: "'a"
 fix xs :: "'a list"
 assume HI: "?P x y xs ys "
 show "?P x y (a#xs) ys"
 proof cases
  assume C1: "a=x"
  then have "sust x y ((a#xs)@ys) = y # sust x y (xs@ys)" by simp
  also have "... = (y # sust x y xs) @ sust x y ys" using HI by simp
  also have "... = sust x y (a#xs) @ sust x y ys" using C1 by simp
  finally show "?P x y (a#xs) ys" by simp
 next
  assume C2: "a≠x"
  then have "sust x y ((a#xs)@ys) = a # sust x y (xs@ys)" by simp
  also have "... = (a # sust x y xs) @ sust x y ys" using HI by simp
  also have "... = sust x y (a#xs) @ sust x y ys" using C2 by simp
  finally show "?P x y (a#xs) ys" by simp
 qed
qed

text {*
  --------------------------------------------------------------------- 
  Ejercicio 3.1. Demostrar o refutar automáticamente
     rev (sust x y zs) = sust x y (rev zs)
  --------------------------------------------------------------------- 
*}

-- "maresccas4"

lemma 
  "rev(sust x y zs) = sust x y (rev zs)" (is "?P x y zs")
by (induct zs) (auto simp add:sust_append)

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

-- "maresccas4"

lemma rev_sust: 
  "rev(sust x y zs) = sust x y (rev zs)" (is "?P x y zs")
proof (induct zs)
 show "?P x y []" by simp
next
 fix z :: "'a"
 fix zs :: "'a list"
 assume HI: "?P x y zs"
 show "?P x y (z#zs)"
 proof cases
  assume C1: "z=x"
  then have "rev(sust x y (z#zs)) = rev(y # (sust x y zs))" by simp
  also have "... = rev (sust x y zs) @ [y]" by (simp only: rev.simps(2))
  also have "... = sust x y (rev zs) @ [y]" using HI by simp
  also have "... = sust x y (rev (z#zs))" using C1 by (simp add:sust_append)
  finally show "?P x y (z#zs)" by simp
 next
  assume C2: "z≠x"
  then have "rev(sust x y (z#zs)) = rev(z # (sust x y zs))" by simp
  also have "... = rev (sust x y zs) @ [z]" by (simp only: rev.simps(2))
  also have "... = sust x y (rev zs) @ [z]" using HI by simp
  also have "... = sust x y (rev (z#zs))" using C2 by (simp add:sust_append)
  finally show "?P x y (z#zs)" by simp
 qed
qed

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

-- "maresccas4"

lemma 
  "sust x y (sust u v zs) = sust u v (sust x y zs)"
quickcheck
oops
(* Contraejemplo:
  x = a⇣1
  y = a⇣2
  u = a⇣2
  v = a⇣1
  zs = [a⇣1]
*)

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

-- "maresccas4"

lemma 
  "sust y z (sust x y zs) = sust x z zs"
  quickcheck
oops
(* Contraejemplo
  y = a⇣1
  z = a⇣2
  x = a⇣2
  zs = [a⇣1]
*)

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::nat) [1,2,3,2] = [1,3,2]

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

-- "maresccas4"

fun borra :: "'a ⇒ 'a list ⇒ 'a list" where
  "borra x [] = []"
| "borra x (y#ys) = (if x=y then ys else y # borra x ys)"

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::nat) [1,2,3,2] = [1,3]
  --------------------------------------------------------------------- 
*}

-- "maresccas4"

fun borraTodas :: "'a ⇒ 'a list ⇒ 'a list" where
  "borraTodas x [] = []"
| "borraTodas x (y#ys) = (if x=y then borraTodas x ys else y # borraTodas x ys)"

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

-- "maresccas4"

lemma 
  "borra x (borraTodas x xs) = borraTodas x xs"
by (induct xs) auto

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

-- "maresccas4"

lemma 
  "borra x (borraTodas x xs) = borraTodas x xs" (is "?P x xs")
proof (induct xs)
 show "?P x []" by simp
next
 fix a :: "'a"
 fix xs :: "'a list"
 assume HI: "?P x xs"
 show "?P x (a#xs)"
 proof cases
  assume C1: "x=a"
  then have "borra x (borraTodas x (a#xs)) = borra x (borraTodas x xs)" by simp
  also have "... = borraTodas x xs" using HI by simp
  also have "... = borraTodas x (a#xs)" using C1 by simp
  finally show "?P x (a#xs)" by simp
 next
  assume C2: "x≠a"
  then have "borra x (borraTodas x (a#xs)) = borra x (a # borraTodas x xs)" by simp
  also have "... = a # borra x (borraTodas x xs)" using C2 by simp
  also have "... = a # borraTodas x xs" using HI by simp
  also have "... = borraTodas x (a#xs)" using C2 by simp
  finally show "?P x (a#xs)" by simp
 qed
qed

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

-- "maresccas4"

lemma 
  "borraTodas x (borraTodas x xs) = borraTodas x xs"
by (induct xs) auto

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

-- "maresccas4"

lemma 
  "borraTodas x (borraTodas x xs) = borraTodas x xs" (is "?P x xs")
proof (induct xs)
 show "?P x []" by simp
next
 fix a :: "'a"
 fix xs :: "'a list"
 assume HI: "?P x xs"
 show "?P x (a#xs)"
 proof cases
  assume C1: "x=a"
  then have "borraTodas x (borraTodas x (a#xs)) = borraTodas x (borraTodas x xs)" by simp
  also have "... = borraTodas x xs" using HI by simp
  also have "... = borraTodas x (a#xs)" using C1 by simp
  finally show "?P x (a#xs)" by simp
 next
  assume C2: "x≠a"
  then have "borraTodas x (borraTodas x (a#xs)) = a # borraTodas x (borraTodas x xs)" by simp
  also have "... = a # borraTodas x xs" using HI by simp
  also have "... = borraTodas x (a#xs)" using C2 by simp
  finally show "?P x (a#xs)" by simp
 qed
qed

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

-- "maresccas4"

lemma 
  "borraTodas x (borra x xs) = borraTodas x xs"
by (induct xs) auto
    
text {*
  --------------------------------------------------------------------- 
  Ejercicio 10.2. Demostrar o refutar detalladamente
     borraTodas x (borra x xs) = borraTodas x xs
  --------------------------------------------------------------------- 
*}

-- "maresccas4"

lemma 
  "borraTodas x (borra x xs) = borraTodas x xs" (is "?P x xs")
proof (induct xs)
 show "?P x []" by simp
next
 fix a :: "'a"
 fix xs :: "'a list"
 assume HI: "?P x xs"
 show "?P x (a#xs)"
 proof cases
  assume C1: "x=a"
  then have "borraTodas x (borra x (a#xs)) = borraTodas x xs" by simp
  also have "... = borraTodas x (a#xs)" using C1 by simp
  finally show "?P x (a#xs)" by simp
 next
  assume C2: "x≠a"
  then have "borraTodas x (borra x (a#xs)) = a # borraTodas x (borra x xs)" by simp
  also have "... = a # borraTodas x xs" using HI by simp
  also have "... = borraTodas x (a#xs)" using C2 by simp
  finally show "?P x (a#xs)" by simp
 qed
qed
    
text {*
  --------------------------------------------------------------------- 
  Ejercicio 11.1. Demostrar o automáticamente
     borra x (borra y xs) = borra y (borra x xs)
  --------------------------------------------------------------------- 
*}

-- "maresccas4"

lemma 
  "borra x (borra y xs) = borra y (borra x xs)"
by (induct xs) auto

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

-- "maresccas4"

lemma 
  "borra x (borra y xs) = borra y (borra x xs)" (is "?P x y xs")
proof (induct xs)
 show "?P x y []" by simp
next
 fix a :: "'a"
 fix xs :: "'a list"
 assume HI: "?P x y xs"
 show "?P x y (a#xs)"
 proof cases
  assume C1: "x=a ∧ y=a"
  then have "borra x (borra y (a#xs)) = borra x xs" by simp
  also have "... = borra y xs" using C1 by simp
  also have "... = borra y (borra x (a#xs))" using C1 by simp
  finally show "?P x y (a#xs)" by simp
 next
  assume C2: "¬(x=a ∧ y=a)"
   show "?P x y (a#xs)"
  proof cases
   assume C3: "x=a"
   then have "borra x (borra y (a#xs)) = borra x (a # borra y xs)" by simp
   also have "... = borra y xs" using C3 by simp
   also have "... = borra y (borra x (a#xs))" using C3 by simp
   finally show "?P x y (a#xs)" by simp
  next
   assume C4: "x≠a"
   show "?P x y (a#xs)"
   proof cases
    assume C5: "y=a"
    then have "borra x (borra y (a#xs)) = borra x xs" by simp
    also have "... = borra y (a # borra x xs)" using C5 by simp
    also have "... = borra y (borra x (a#xs))" using C5 by simp
    finally show "?P x y (a#xs)" by simp
   next
    assume C6: "y≠a"
    then have "borra x (borra y (a#xs)) = a # borra x (borra y xs)" using C4  by simp
    also have "... = a # borra y (borra x xs)" using HI by simp
    also have "... = borra y (a # borra x xs)" using C6 by simp
    also have "... = borra y (borra x (a#xs))" using C4 by simp
    finally show "?P x y (a#xs)" by simp
   qed
  qed
 qed
qed

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

-- "maresccas4"

lemma 
  "borraTodas x (borra y xs) = borra y (borraTodas x xs)"
by (induct xs)(auto simp add:borra_borraTodas)

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

-- "maresccas4"

lemma 
  "borraTodas x (borra y xs) = borra y (borraTodas x xs)" (is "?P x y xs")
proof (induct xs)
 show "?P x y []" by simp
next
 fix a :: "'a"
 fix xs :: "'a list"
 assume HI: "?P x y xs"
 show "?P x y (a#xs)"
 proof cases
  assume C1: "x=a ∧ y=a"
  then have "borraTodas x (borra y (a#xs)) = borraTodas x xs" by simp
  also have "... = borra y (borraTodas x (a#xs))" using C1 by (simp add:borra_borraTodas)
  finally show "?P x y (a#xs)" by simp
 next
  assume C2: "¬(x=a ∧ y=a)"
  show "?P x y (a#xs)"
  proof cases
   assume C3: "x=a"
   then have "borraTodas x (borra y (a#xs)) = borraTodas x (a # borra y xs)" using C2  by simp
   also have "... = borraTodas x (borra y xs)" using C3 by simp
   also have "... = borra y (borraTodas x xs)" using HI by simp
   also have "... = borra y (borraTodas x (a#xs))" using C3 by simp
   finally show "?P x y (a#xs)" by simp
  next
   assume C4: "x≠a"
   show "?P x y (a#xs)"
   proof cases
    assume C5: "y=a"
    then have "borraTodas x (borra y (a#xs)) = borraTodas x xs" by simp
    also have "... = borra y (a # borraTodas x xs)" using C5 by simp
    also have "... = borra y (borraTodas x (a#xs))" using C4 by simp
    finally show "?P x y (a#xs)" by simp
   next
    assume C6: "y≠a"
    then have "borraTodas x (borra y (a#xs)) = borraTodas x (a # borra y xs)" by simp
    also have "... = a # borraTodas x (borra y xs)" using C4 by simp
    also have "... = a # borra y (borraTodas x xs)" using HI by simp
    finally show "?P x y (a#xs)" using C6 C4 by simp
   qed
  qed
 qed
qed     

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

-- "maresccas4"

lemma 
  "borra y (sust x y xs) = borra x xs"
quickcheck
oops
(* Contraejemplo
  y = a⇣1
  x = a⇣2
  xs = [a⇣1]
*)

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

-- "maresccas4"

lemma 
  "borraTodas y (sust x y xs) = borraTodas x xs"
quickcheck
oops
(* Contraejemplo
 y = a⇣1
 x = a⇣2
 xs = [a⇣1]
*)

text {*
  --------------------------------------------------------------------- 
  Ejercicio 15.1. Demostrar o refutar automáticamente
     sust x y (borraTodas x zs) = borraTodas x zs
  --------------------------------------------------------------------- 
*}

-- "maresccas4"

lemma 
  "sust x y (borraTodas x zs) = borraTodas x zs"
by (induct zs) auto

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

-- "maresccas4"

lemma sust_borraTodas:
  "sust x y (borraTodas x zs) = borraTodas x zs" (is "?P x y zs")
proof (induct zs)
 show "?P x y []" by simp
next
 fix a :: "'a"
 fix zs :: "'a list"
 assume HI: "?P x y zs"
 show "?P x y (a#zs)"
 proof cases
  assume C1: "x=a"
  then have "sust x y (borraTodas x (a#zs)) = sust x y (borraTodas x zs)" by simp
  also have "... = borraTodas x zs" using HI by simp
  finally show "?P x y (a#zs)" using C1 by simp
 next
  assume C2: "x≠a"
  then have "sust x y (borraTodas x (a#zs)) = sust x y (a # borraTodas x zs)" by simp
  also have "... = a # sust x y (borraTodas x zs)" using C2 by simp
  also have "... = a # borraTodas x zs" using HI by simp
  finally show "?P x y (a#zs)" using C2 by simp
 qed
qed

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

-- "maresccas4"

lemma 
  "sust x y (borraTodas z zs) = borraTodas z (sust x y zs)"
quickcheck
oops
(* Contraejemplo
 x = a⇣1
 y = a⇣2
 z = a⇣1
 zs = [a⇣1]
*)

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

-- "maresccas4"

lemma 
  "rev (borra x xs) = borra x (rev xs)"
quickcheck
oops
(* Contraejemplo
 x = a⇣1
 xs = [a⇣1, a⇣2, a⇣1]
*)

text {*
  --------------------------------------------------------------------- 
  Ejercicio 18.1. Demostrar o refutar automáticamente
     borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)
  --------------------------------------------------------------------- 
*}

-- "maresccas4"

lemma 
  "borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)"
by (induct xs) auto

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

-- "maresccas4"

lemma borraTodas_concat:
  "borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)" (is "?P x xs ys")
proof (induct xs)
 show "?P x [] ys" by simp
next
 fix a :: "'a"
 fix xs :: "'a list"
 assume HI: "?P x xs ys"
 show "?P x (a#xs) ys"
 proof cases
  assume C1: "x=a"
  then have "borraTodas x ((a#xs)@ys) = borraTodas x (xs@ys)" by simp
  also have "... = (borraTodas x xs)@(borraTodas x ys)" using HI by simp
  finally show "?P x (a#xs) ys" using C1 by simp
 next
  assume C2: "x≠a"
  then have "borraTodas x ((a#xs)@ys) = a # borraTodas x (xs@ys)" by simp
  also have "... = a # (borraTodas x xs)@(borraTodas x ys)" using HI by simp
  finally show "?P x (a#xs) ys" using C2 by simp
 qed
qed

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

-- "maresccas4"

lemma 
  "rev (borraTodas x xs) = borraTodas x (rev xs)"
by (induct xs) (auto simp add: borraTodas_concat)

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

-- "maresccas4"

lemma 
  "rev (borraTodas x xs) = borraTodas x (rev xs)" (is "?P x xs")
proof (induct xs)
 show "?P x []" by simp
next
 fix a :: "'a"
 fix xs :: "'a list"
 assume HI: "?P x xs"
 show "?P x (a#xs)"
 proof cases
  assume C1: "x=a"
  then have "rev (borraTodas x (a#xs)) = rev (borraTodas x xs)" by simp
  also have "... = borraTodas x (rev xs)" using HI by simp
  also have "... = borraTodas x (rev xs) @ borraTodas x (rev [a])" using C1 by simp
  also have "... = borraTodas x (rev (a#xs))" by (simp add: borraTodas_concat)
  finally show "?P x (a#xs)" by simp
 next
  assume C2: "x≠a"
  then have "rev (borraTodas x (a#xs)) = rev (a # borraTodas x xs)" by simp
  also have "... = rev (borraTodas x xs) @ [a]" by simp
  also have "... = borraTodas x (rev xs) @ borraTodas x [a]" using HI C2 by simp
  also have "... = borraTodas x (rev xs @ [a])" by (simp add: borraTodas_concat)
  finally show "?P x (a#xs)" by simp
 qed
qed

end