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]
  --------------------------------------------------------------------- 
*}

(* pabflomar: Hola, son las 03:37 y por fin funciona el wiki. No he podido copiar ni una sola solución. :@ *)

-- "maresccas4 domlloriv diecabmen1 irealetei juaruipav pabflomar marescpla julrobrel jaisalmen zoiruicha"

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)"

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

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

-- "maresccas4 domlloriv diecabmen1 irealetei juaruipav pabflomar marescpla jaisalmen zoiruicha"

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

-- "julrobrel: usando apply, por probar"
lemma 
  "sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"
  apply (induct_tac xs)
  apply (auto)
done

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

-- "maresccas4 juaruipav domlloriv marescpla"

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

-- "diecabmen1 misma solución solamente quito el último also have para evitar redundar con finally"
-- "jaisalmen zoiruicha"
lemma sust_append2: 
  "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 xs
  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
    finally show"?P x y (a#xs) ys" using C1 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
    finally show"?P x y (a#xs) ys" using C2 by simp
  qed
qed

(*pabflomar: 100% de acuerdo con Irene. *)
-- "irealetei me gusta más sin abreviar "
-- "pabflomar"
lemma sust_append3: 
  "sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"
proof (induction xs)
  show "sust x y ([] @ ys) = sust x y [] @ sust x y ys" by simp
next
fix xs a
assume HI:"sust x y (xs @ ys) = sust x y xs @ sust x y ys"
show "sust x y ((a # xs) @ ys) = sust x y (a # xs) @ sust x y ys"
proof (cases)
assume A: "x=a"
 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 A by simp
 finally show "sust x y ((a # xs) @ ys) = sust x y (a # xs) @ sust x y ys" by simp
next
assume A: "x≠a"
 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 A by simp
 finally show "sust x y ((a # xs) @ ys) = sust x y (a#xs) @ sust x y ys" by simp
qed
qed

(* Juaruipav: Yo no llamaría a las dos hipótesis iguales, aunque no haya conflictos*)


-- "julrobrel"
lemma sust_append_jrr: 
  "sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"
  proof (induct xs)
     show "sust x y ([] @ ys) = sust x y [] @ sust x y ys" by simp
  next
     fix a xs
     assume HI:"sust x y (xs@ys) = (sust x y xs)@(sust x y ys)"
     show "sust x y ((a # xs) @ ys) = sust x y (a # xs) @ sust x y ys"
     proof (cases)
      assume C1: "x=a"
      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 (x#xs))@(sust x y ys)" by simp
      also have "...=(sust x y (a#xs))@(sust x y ys)" using C1 by simp
      finally show "sust x y ((a # xs) @ ys) = sust x y (a # xs) @ sust x y ys" by simp
     next
      assume C2: "¬(x=a)"
      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 "sust x y ((a # xs) @ ys) = sust x y (a # xs) @ sust x y 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 diecabmen1 irealetei juaruipav domlloriv pabflomar marescpla jaisalmen zoiruicha"
(*domllriv -> Me apunto a este pero a mi no me funciona. Fall add:sust_append*)

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


--"julrobrel: por probar otra vez"
lemma 
  "rev(sust x y zs) = sust x y (rev zs)"
  apply (induct_tac zs)
  apply (simp_all add: sust_append)
done

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

-- "maresccas4"
-- "jaisalmen zoiruicha"
(* jaisalmen: la inducción es sobre los elementos de zs*)

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

-- "diecabmen1"
lemma rev_sust2: 
  "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 a zs
  assume HI: "?P x y zs"
  show "?P x y (a#zs)"
  proof cases
    assume C1:"x=a"
    then have "rev(sust x y (a#zs)) = rev(y # sust x y zs)" by simp
    also have "… = rev(sust x y zs) @ [y]" by simp
    also have "… = sust x y (rev zs) @ [y]" using HI by simp
    finally show "?P x y (a#zs)" using C1 by (simp add:sust_append2)
  next
    assume C2: "x≠a"
    then have "rev(sust x y (a#zs)) = rev(a # sust x y zs)" by simp
    also have "… = rev(sust x y zs) @ [a]" by simp
    also have "… = sust x y (rev zs) @ [a]" using HI by simp
    finally show "?P x y (a#zs)" using C2 by (simp add:sust_append2)
  qed
qed

-- "irealetei pabflomar"
lemma rev_sust3: 
  "rev(sust x y zs) = sust x y (rev zs)"
proof (induct zs)
  show "rev (sust x y []) = sust x y (rev [])" by simp
next
  fix a zs
  assume HI:" rev (sust x y zs) = sust x y (rev zs)"
  show "rev (sust x y (a # zs)) = sust x y (rev (a # zs))"
  proof (cases)
   assume A1:"x=a"
   then have "rev (sust x y (a # zs))= rev(y#sust x y zs)" by simp
   also have "... = (rev(sust x y zs)@[y])" by simp
   also have "...=sust x y (rev zs)@[y]" using HI by simp
   also have "...=sust x y (rev(a # zs))" using A1 by (simp add:sust_append)
   finally show "rev (sust x y (a # zs))=sust x y (rev(a # zs))" by simp
  next
   assume A2:"x≠a"
   then have "rev (sust x y (a # zs))= rev(a#sust x y zs)" by simp
   also have "... = (rev(sust x y zs)@[a])" by simp
   also have "...=sust x y (rev zs)@[a]" using HI by simp
   also have "...=sust x y (rev(a # zs))" using A2 by (simp add:sust_append)
   finally show "rev (sust x y (a # zs))=sust x y (rev(a # zs))" by simp
  qed
qed

--"juaruipav domlloriv marescpla"
lemma rev_sust: 
  "rev(sust x y zs) = sust x y (rev zs)"
  proof (induct zs)
    show "rev (sust x y []) = sust x y (rev [])" by simp
   next
   fix a zs
   assume HI:" rev (sust x y zs) = sust x y (rev zs)"
   show " rev (sust x y (a # zs)) = sust x y (rev (a # zs))"
   proof(cases)
   assume C1: "a=x"
  then have "rev( sust x y (a #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 zs)) @ (sust x y [a])" using C1 by (simp add:sust_append)
  also have "... = sust x y (rev zs@[a])" by (simp add:sust_append)
  also have "...=sust x y (rev (a#zs))" by (simp only: rev.simps(2))
  finally show ?thesis by simp
next
   assume C2: "a≠x"
   then have "rev( sust x y (a #zs))= rev( x# sust x y zs)" by simp
   also have "...= rev(sust x y zs) @ [x]"  by (simp only: rev.simps(2))
   also have "...= sust x y (rev zs)@ [x]" using HI by simp
   also have "...= (sust x y (rev zs)) @ (sust x y [a])" using C2 by (simp add:sust_append)
   also have "... = sust x y (rev zs@[a])" by (simp add:sust_append)
   also have "...=sust x y (rev (a#zs))" by (simp only: rev.simps(2))
  finally show ?thesis by simp
qed
qed

oops --"julrobrel: lo he puesto para comprobar mi edicion"

--"julrobrel"
lemma rev_sust_jrr: 
  "rev(sust x y zs) = sust x y (rev zs)"
  proof (induct zs)
    show "rev (sust x y []) = sust x y (rev [])" by simp
  next
    fix a zs
    assume HI:"rev(sust x y zs) = sust x y (rev zs)"
    show "rev (sust x y (a # zs)) = sust x y (rev (a # zs))"
    proof (cases)
      assume C1: "x=a"
      then have "rev (sust x y (a # zs)) = rev (y # sust x y zs)" by simp
      also have "...=rev (sust x y zs) @ [y]" by simp
      also have "...=sust x y (rev zs) @ [y]" using HI by simp
      also have "...=sust x y (rev zs) @ sust x y [x]" by simp
      also have "...=sust x y ((rev zs)@[x])" by (simp add:sust_append_jrr)
      also have "...=sust x y (rev (x#zs))" by simp
      also have "...=sust x y (rev (a#zs))" using C1 by simp
      finally show "rev (sust x y (a # zs)) = sust x y (rev (a # zs))" .
    next
      assume C2: "¬(x=a)"
      then have "rev (sust x y (a # zs)) = rev (a # sust x y zs)" by simp
      also have "...= rev(sust x y zs)@[a]" by simp
      also have "...= sust x y (rev zs)@[a]" using HI by simp
      also have "...= sust x y (rev (a#zs))" using C2 by (simp add:sust_append_jrr)
      finally show "rev (sust x y (a # zs)) = sust x y (rev (a # zs))" .
    qed
qed

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

-- "maresccas4 domlloriv diecabmen1 irealetei juaruipav pabflomar marescpla julrobrel jaisalmen zoiruicha"

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 domlloriv diecabmen1 irealetei juaruipav pabflomar marescpla julrobrel jaisalmen zoiruicha"

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 domlloriv diecabmen1 irealetei juaruipav pabflomar marescpla julrobrel jaisalmen zoiruicha"

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

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

-- "maresccas4 domlloriv irealetei diecabmen1 juaruipav pabflomar marescpla julrobrel jaisalmen zoiruicha"

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)"

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

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

-- "maresccas4 domlloriv irealetei diecabmen1 juaruipav pabflomar marescpla julrobrel jaisalmen zoiruicha"

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 diecabmen1 domlloriv agrego nombre a lemma para ejercicio 12.1  marescpla"

lemma borra_borraTodas:
  "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

-- "irealetei pabflomar"
lemma borrax_BorraTodasx_xs:
  "borra x (borraTodas x xs) = borraTodas x xs"
proof (induct xs)
  show "borra x (borraTodas x []) = borraTodas x []" by simp
next
  fix a xs
  assume HI:"borra x (borraTodas x xs) = borraTodas x xs"
  show "borra x (borraTodas x (a # xs)) = borraTodas x (a # xs)"
  proof (cases)
    assume A1:"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
    finally show "borra x (borraTodas x (a # xs)) = borraTodas x (a#xs)" using A1 by simp
  next
    assume A2:"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 A2  by simp  
    also have "...=a # borraTodas x xs" using HI by simp
    finally show "borra x (borraTodas x (a # xs)) = borraTodas x (a#xs)" using A2 by simp
   qed
  qed


--" juaruipav"

lemma borradora:
  "borra x (borraTodas x xs) = borraTodas x xs"
proof (induct xs)
  show " borra x (borraTodas x []) = borraTodas x []" by simp
next
  fix a xs
  assume HI: " borra x (borraTodas x xs) = borraTodas x xs"
  show " borra x (borraTodas x (a # xs)) = borraTodas x (a # xs)"
  proof(cases)
  assume C1: "x=a"
    show " borra x (borraTodas x (a # xs)) = borraTodas x (a#xs)" using HI using C1 by simp 
  next
  assume C2: "x≠a"
   show " borra x (borraTodas x (a # xs)) = borraTodas x (a#xs)" using HI using C2 by simp 
  qed
qed

--"julrobrel"
lemma
  "borra x (borraTodas x xs) = borraTodas x xs"
  proof (induct xs)
    show  "borra x (borraTodas x []) = borraTodas x []" by simp
  next
   fix a xs
   assume HI: "borra x (borraTodas x xs) = borraTodas x xs"
   show "borra x (borraTodas x (a#xs)) = borraTodas 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
     finally show "borra x (borraTodas x (a#xs)) = borraTodas x (a#xs)" using C1 by simp
   next
     assume C2:"¬(x=a)"
     then have "borra x (borraTodas x (a#xs)) = a#(borra x (borraTodas x xs))" using C2 by simp
     also have "...=a#borraTodas x xs" using HI by simp
     finally show "borra x (borraTodas x (a#xs)) = borraTodas x (a#xs)" using C2 by simp
  qed
qed

-- "jaisalmen zoiruicha -- no hace falta fijar a y xs en dos líneas"
lemma borra_borraTodas:
  "borra x (borraTodas x xs) = borraTodas x xs" (is "?P x xs")
proof (induct xs)
  show "?P x []" by simp
next
  fix a xs
  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 domlloriv irealetei diecabmen1 juaruipav pabflomar marescpla julrobrel jaisalmen zoiruicha"

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

-- "irealetei pabflomar"
lemma 
  "borraTodas x (borraTodas x xs) = borraTodas x xs"
proof (induct xs)
  show "borraTodas x (borraTodas x []) = borraTodas x []" by simp
next
  fix a xs
  assume HI:"borraTodas x (borraTodas x xs) = borraTodas x xs"
  show "borraTodas x (borraTodas x (a # xs)) = borraTodas x (a # xs)"
  proof (cases)
    assume A1:"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
    finally show "borraTodas x (borraTodas x (a # xs)) = borraTodas x (a#xs)" using A1 by simp
  next
    assume A2:"x≠a"
    then have "borraTodas x (borraTodas x (a # xs)) = borraTodas x (a#(borraTodas x xs))" by simp
    also have "...=a # borraTodas x (borraTodas x xs)" using A2  by simp  
    also have "...=a # borraTodas x xs" using HI by simp
    finally show "borraTodas x (borraTodas x (a # xs)) = borraTodas x (a#xs)" using A2 by simp
   qed
  qed

--"diecabmen1 domlloriv marescpla"
lemma 
  "borraTodas x (borraTodas x xs) = borraTodas x xs" (is "?P x xs")
proof (induct xs)
  show "?P x []" by simp
next
  fix a xs
  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
    finally show "?P x (a # xs)" using C1 by simp
  next
    assume C2: "x≠a"
    then have "borraTodas x (borraTodas x (a # xs)) = borraTodas x (a # borraTodas x xs)" by simp
    also have "… = a # borraTodas x (borraTodas x xs)" using C2 by simp
    also have "… = a # borraTodas x xs" using HI by simp
    finally show "?P x (a # xs)" using C2 by simp
  qed
qed

--"juaruipav"

lemma 
  "borraTodas x (borraTodas x xs) = borraTodas x xs"
proof(induct xs)
show " borraTodas x (borraTodas x []) = borraTodas x []" by simp
next
  fix a xs
  assume HI:"borraTodas x (borraTodas x xs) = borraTodas x xs"
    show "borraTodas x (borraTodas x (a # xs)) = borraTodas x (a # xs)"
    proof(cases)
    assume C1: "x=a"
       show "borraTodas x (borraTodas x (a # xs)) = borraTodas x (a # xs)" using HI using C1 by simp
       next
    assume C2: "x≠a"
       show "borraTodas x (borraTodas x (a # xs)) = borraTodas x (a # xs)" using HI using C2 by simp
qed
qed

--"julrobrel"
lemma 
  "borraTodas x (borraTodas x xs) = borraTodas x xs"
proof (induct xs)  
  show "borraTodas x (borraTodas x []) = borraTodas x []" by simp
next
  fix a xs
  assume HI: "borraTodas x (borraTodas x xs) = borraTodas x xs"
  show "borraTodas x (borraTodas x (a#xs)) = borraTodas 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 "borraTodas x (borraTodas x (a#xs)) = borraTodas x (a#xs)" .
  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 "borraTodas x (borraTodas x (a#xs)) = borraTodas x (a#xs)" .
  qed
qed

-- "jaisalmen zoiruicha -- no hace falta indicar a y xs por separado"

lemma 
  "borraTodas x (borraTodas x xs) = borraTodas x xs" (is "?P x xs")
proof (induct xs)
 show "?P x []" by simp
next
 fix a xs
 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 domlloriv irealetei diecabmen1 juaruipav pabflomar marescpla jaisalmen zoiruicha"

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

--"julrobrel"
lemma borraTodas_jrr:
  "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 diecabmen1 no va un finally sin un also have antes"

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

-- "irealetei pabflomar marescpla"
lemma 
  "borraTodas x (borra x xs) = borraTodas x xs"
proof (induct xs)
  show "borraTodas x (borra x []) = borraTodas x []" by simp
next
  fix a xs
  assume HI:"borraTodas x (borra x xs) = borraTodas x xs"
  show "borraTodas x (borra x (a # xs)) = borraTodas x (a # xs)"
  proof (cases)
    assume A1:"x=a"
    then have "borraTodas x (borra x (a # xs)) = borraTodas x xs" by simp
    also have "...=borraTodas x (a # xs)" using A1 by simp
    finally show "borraTodas x (borra x (a # xs)) = borraTodas x (a#xs)" by simp
  next
    assume A2:"x≠a"
    then have "borraTodas x (borra x (a # xs)) = borraTodas x (a#(borra x xs))" by simp
    also have "...=a # borraTodas x (borra x xs)" using A2  by simp  
    also have "...=a # borraTodas x xs" using HI by simp
    finally show "borraTodas x (borra x (a # xs)) = borraTodas x (a#xs)" using A2 by simp
   qed
  qed

--" juaruipav domlloriv"
(*Domlloriv -> Este no me ha salido pero me apunto a la solucion de Juan que es mas simple*)
lemma borraTodas_conmut:
  "borraTodas x (borra x xs) = borraTodas x xs"
proof (induct xs)
    show " borraTodas x (borra x []) = borraTodas x []" by simp
 next
 fix a xs
 assume HI: " borraTodas x (borra x xs) = borraTodas x xs"
 show "borraTodas x (borra x (a # xs)) = borraTodas x (a # xs)"
 proof(cases)
  assume C1: "x=a"
    show "borraTodas x (borra x (a#xs))=borraTodas x (a #xs)" using HI using C1 by simp
  next
  assume C2: "x≠a"
     show "borraTodas x (borra x (a#xs))=borraTodas x (a #xs)" using HI using C2 by simp
  qed
qed

--"julrobrel"
lemma 
  "borraTodas x (borraTodas x xs) = borraTodas x xs"
proof (induct xs)  
  show "borraTodas x (borraTodas x []) = borraTodas x []" by simp
next
  fix a xs
  assume HI: "borraTodas x (borraTodas x xs) = borraTodas x xs"
  show "borraTodas x (borraTodas x (a#xs)) = borraTodas 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 "borraTodas x (borraTodas x (a#xs)) = borraTodas x (a#xs)" .
  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 "borraTodas x (borraTodas x (a#xs)) = borraTodas x (a#xs)" .
  qed
qed

-- "jaisalmen zoiruicha -- similar a los anteriores con a y xs"
lemma 
  "borraTodas x (borra x xs) = borraTodas x xs" (is "?P x xs")
proof (induct xs)
 show "?P x []" by simp
next
  fix a xs 
  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 domlloriv irealetei diecabmen1 juaruipav pabflomar marescpla julrobrel jaisalmen zoiruicha"

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


-- "irealetei diecabmen1 domlloriv pabflomar"
lemma 
  "borra x (borra y xs) = borra y (borra x xs)"
proof (induct xs)
 show  "borra x (borra y []) = borra y (borra x [])" by simp
next
  fix a xs
  assume HI: "borra x (borra y xs) = borra y (borra x xs)"
  show  "borra x (borra y (a # xs)) = borra y (borra x (a # xs))"
  proof (cases)
    assume A1:"x=a"
    then have "borra x (borra y (a # xs)) = borra x (a#borra y xs)" by simp
    also have "... = borra y xs" using A1 by simp
    also have "...=borra y ( borra x (a # xs))" using A1 by simp
    finally show "borra x (borra y (a # xs)) = borra y ( borra x (a # xs))" by simp
  next
    assume A2:"x≠a"
    show "borra x (borra y (a # xs)) = borra y (borra x (a # xs))"
      proof (cases)
        assume A3:"y=a"
        then have "borra x (borra y (a # xs)) = borra x xs"  by simp
        also have "...=borra y (a # borra x xs)" using A3  by simp  
        finally show "borra x (borra y (a # xs)) = borra y (borra x (a # xs))" using A2 by simp
      next
        assume A4:"y≠a"
        then have "borra x (borra y (a # xs)) =borra x (a#borra y xs)"  by simp
        also have "...=(a#(borra x (borra y xs)))" using A2  by simp  
        also have "...=(a#(borra y (borra x xs)))" using HI by simp
        also have "...= borra y (a # borra x xs)" using A4 by simp
        finally show "borra x (borra y (a # xs)) = borra y (borra x (a # xs))" using A2 by simp
   qed
  qed
qed

--"juaruipav"
lemma 
  "borra x (borra y xs) = borra y (borra x xs)"
proof (induct xs)
  show " borra x (borra y []) = borra y (borra x [])" by simp
next
  fix a xs
  assume HI:" borra x (borra y xs) = borra y (borra x xs)"
  show " borra x (borra y (a # xs)) = borra y (borra x (a # xs))"
  proof (cases)
  assume C1: "x=a"
    show " borra x (borra y (a # xs)) = borra y (borra x (a # xs))" using HI using C1 by simp
next
   assume C2: "x≠a"
   show " borra x (borra y (a # xs)) = borra y (borra x (a # xs))" using HI using C2 by simp
qed
qed


--"marescpla: Bueno, ya he visto que no es el más corto, pero es como lo hice"

lemma 
  "borra x (borra y xs) = borra y (borra x xs)" (is "?P xs")
proof (induct xs)
show "?P []" by simp
next
fix a xs
assume HI: "?P xs"
show "?P (a#xs)"
proof (cases)
assume I: "x=a"
  show "?P (a#xs)"
  proof (cases)
    assume II: "y=a"
    then have "borra x (borra y (a#xs))= borra x xs" by simp
    also have "...=borra y xs" using I II by simp
    finally show "?P (a#xs)" using I by simp
  next
    assume III: "y≠a"
    then have "borra x (borra y (a#xs))= borra x (a# borra y xs)" by simp
    also have "...=borra y xs" using I by simp
    finally show "?P (a#xs)"using I by simp
  qed
  next
  assume III: "x≠a"
  show "?P (a#xs)"
    proof (cases)
    assume IV: "y=a"
    then have "borra x (borra y (a#xs))=borra x xs" by simp
    also have "...=borra y (a#borra x xs)" using IV by simp
    finally show "?P (a#xs)" using III by simp
  next
    assume V: "y≠a"
    then have "borra x (borra y (a#xs))= borra x (a# borra y xs)" by simp
    also have "...=a#borra x (borra y xs)"using III by simp
    also have "...=a#borra y (borra x xs)"using HI by simp
    finally show "?P (a#xs)"using V III by simp
  next
  qed
qed
qed

--"julrobrel"
lemma 
  "borra x (borra y xs) = borra y (borra x xs)"
  proof (cases)
    assume C1: "x=y"
    show "borra x (borra y xs) = borra y (borra x xs)" using C1 by simp
  next
    assume C2: "¬(x=y)"
    show "borra x (borra y xs) = borra y (borra x xs)"
    proof (induct xs) 
      show "borra x (borra y []) = borra y (borra x [])" by simp
    next
      fix a xs
      show "borra x (borra y xs) = borra y (borra x xs) ⟹ borra x (borra y (a # xs)) = borra y (borra x (a # xs))" using C2 by simp
    qed
qed

-- "jaisalmen zoiruicha"
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 xs
  assume HI:"?P x y xs"
    show "?P x y (a#xs)"
  proof (cases)
    assume C1: "x=a"
    show " borra x (borra y (a # xs)) = borra y (borra x (a # xs))" using HI using C1 by simp
  next
    assume C2: "x≠a"
    show " borra x (borra y (a # xs)) = borra y (borra x (a # xs))" using HI using C2 by simp
qed
qed


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

-- "maresccas4 diecabmen1 domlloriv marescpla jaisalmen zoiruicha"

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

-- "irealetei pabflomar"
lemma 
  "borraTodas x (borra y xs) = borra y (borraTodas x xs)"
by (induct xs) (auto simp add:borrax_BorraTodasx_xs)

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

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

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     


-- "irealetei"
lemma 
  "borraTodas x (borra y xs) = borra y (borraTodas x xs)"
proof (induct xs)
  show " borraTodas x (borra y []) = borra y (borraTodas x [])" by simp
next
  fix a xs
  assume HI:"borraTodas x (borra y xs) = borra y (borraTodas x xs)"
  show "borraTodas x (borra y (a # xs)) = borra y (borraTodas x (a # xs))"
  proof (cases)
    assume A1:"y=a"
     show "borraTodas x (borra y (a # xs)) = borra y (borraTodas x (a # xs))"
     proof (cases)
        assume A3:"x=a"
        then have "borraTodas x (borra y (a # xs))=borraTodas x xs" using A1 by simp
        also have "...=borra y (a#borraTodas x xs)" using A1 by simp
        also have "...=borra y (borraTodas x (a # xs))" using A3 using A1 by (simp add:borrax_BorraTodasx_xs)
        finally show "borraTodas x (borra y (a # xs)) = borra y (borraTodas x (a # xs))" by simp
      next
        assume A2:"x≠a"
        then have "borraTodas x (borra y (a # xs))=borraTodas x xs" using A1 by simp
        also have "...=borra y (a#borraTodas x xs)" using A1 by simp
        finally show "borraTodas x (borra y (a # xs))=borra y (borraTodas x (a#xs))" using A2 by simp
      qed
      next
        assume A4:"y≠a"
        show "borraTodas x (borra y (a # xs)) = borra y (borraTodas x (a # xs))"
        proof (cases)
           assume A5:"x=a"
           then have "borraTodas x (borra y (a # xs))=borraTodas x (a#borra y xs)"using A4 by simp
           also have "...=borraTodas x (borra y xs)" using A5 by simp
           also have "...=borra y (borraTodas x xs)" using HI by simp
           also have "...=borra y (borraTodas x (a#xs))" using A5 by simp
           finally show "borraTodas x (borra y (a # xs)) = borra y (borraTodas x (a # xs))" by simp
        next
          assume A5:"x≠a"
           then have "borraTodas x (borra y (a # xs))=borraTodas x (a#borra y xs)"using A4 by simp
           also have "...=a#borraTodas x (borra y xs)" using A5 by simp
           also have "...=a#borra y (borraTodas x xs)" using HI by simp
           also have "...=borra y (a#borraTodas x (xs))" using A4 by simp
           finally show "borraTodas x (borra y (a # xs)) = borra y (borraTodas x (a # xs))" using A5 by simp
      qed
    qed
qed

--"juaruipav"
lemma 
  "borraTodas x (borra y xs) = borra y (borraTodas x xs)"
proof (induct xs)
 show " borraTodas x (borra y []) = borra y (borraTodas x [])" by simp
next
  fix a xs
  assume HI: " borraTodas x (borra y xs) = borra y (borraTodas x xs)"
  show "  borraTodas x (borra y (a # xs)) = borra y (borraTodas x (a # xs))"
  proof (cases)
  assume C1: "x=a"
    show "borraTodas x (borra y (a # xs)) = borra y (borraTodas x (a # xs))" using HI using C1 by( simp add:borradora)
  next
   assume C2: "x≠a"
     show "borraTodas x (borra y (a # xs)) = borra y (borraTodas x (a # xs))" using HI using C2 by( simp add:borradora)
qed
qed

--"diecabmen1"
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 xs
  assume HI: "?P x y xs"
  show "?P x y (a # xs)"
  proof cases
    assume C1: "y = a"
    show "?P x y (a # xs)"
    proof cases
      assume C2: "x = a"
      then have "borraTodas x (borra y (a # xs)) = borra y (a # borraTodas x xs)" using C1 by simp
      also have "… = borra y (a # borraTodas x (a # xs))" using C2 by simp
      also have "… = borra y (a # borra y (borraTodas x (a # xs)))"using C2 using C1 by (simp add: borra_borraTodas)
      finally show "?P x y (a # xs)" using C1 by simp    
    next
      assume C3: "x ≠ a"
      then have "borraTodas x (borra y (a # xs)) = borraTodas x xs" using C1 by simp
      also have "… = borra y (a # borraTodas x xs)" using C1 by simp
      finally show "?P x y (a # xs)" using C3 by simp
   qed
  next
    assume C4: "y ≠ a"
    show "?P x y (a # xs)"
    proof cases
      assume C5: "x = a"
      then have "borraTodas x (borra y (a # xs)) = borraTodas x (a # borra y xs)" using C4 by simp
      also have "… = borraTodas x (borra y xs)" using C5 by simp
      also have "… = borra y (borraTodas x xs)" using HI by simp
      finally show "?P x y (a # xs)" using C5 by simp
    next
      assume C6: "x ≠ a"
      then have "borraTodas x (borra y (a # xs)) = borraTodas x (a # borra y xs)" using C4 by simp
      also have "… = a # borraTodas x (borra y xs)" using C6 by simp
      also have "… = a # borra y (borraTodas x xs)" using HI by simp
      also have "… = borra y (a # borraTodas x xs)" using C4 by simp
      finally show "?P x y (a # xs)" using C6 by simp
    qed
  qed
qed


--"julrobrel"
lemma 
  "borraTodas x (borra y xs) = borra y (borraTodas x xs)"
proof (induct xs)
  show "borraTodas x (borra y []) = borra y (borraTodas x [])" by simp
next
  fix a xs
  assume HI: "borraTodas x (borra y xs) = borra y (borraTodas x xs)"
  show "borraTodas x (borra y (a#xs)) = borra y (borraTodas x (a#xs))"
  proof (cases)
    assume C1: "x=a"
    then have "borraTodas x (borra y (a#xs)) = borraTodas x (borra y xs)" using C1 by (simp add:borraTodas_jrr)
    also have "...=borra y (borraTodas x xs)" using HI by simp
    finally show  "borraTodas x (borra y (a#xs)) = borra y (borraTodas x (a#xs))" using C1 by simp
  next
    assume C2: "¬(x=a)"
    show "borraTodas x (borra y (a#xs)) = borra y (borraTodas x (a#xs))"
    proof (cases)
      assume C3: "y=a"
      then have "borraTodas x (borra y (a#xs)) = borraTodas x xs" using C3 by simp
      also have "...=borra y (a#borraTodas x xs)" using C3 by simp
      also have "...=borra y (borraTodas x (a#xs))" using C2 by simp
      finally show "borraTodas x (borra y (a#xs)) = borra y (borraTodas x (a#xs))" by simp
    next
      assume C4: "¬(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 C2 by simp
      also have "...=a#(borra y (borraTodas x xs))" using HI by simp
      also have "...=borra y (a#borraTodas x xs)" using C4 by simp
      also have "...=borra y (borraTodas x (a#xs))" using C2 by simp
      finally show "borraTodas x (borra y (a#xs)) = borra y (borraTodas x (a#xs))" .
    qed
  qed
qed

-- "jaisalmen zoiruicha"
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 xs
  assume HI: "?P x y xs"
  show "?P x y (a#xs)"
  proof (cases)
  assume C1: "x=a"
    show "borraTodas x (borra y (a # xs)) = borra y (borraTodas x (a # xs))" using HI using C1 by( simp add:borra_borraTodas)
  next
   assume C2: "x≠a"
     show "borraTodas x (borra y (a # xs)) = borra y (borraTodas x (a # xs))" using HI using C2 by( simp add:borra_borraTodas)
qed
qed


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

-- "maresccas4 irealetei juaruipav domlloriv diecabmen1 marescpla julrobrel zoiruicha jaisalmen" 

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 irealetei juaruipav domlloriv diecabmen1 marescpla julrobrel"

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 irealetei domlloriv diecabmen1 marescpla julrobrel"
(*Domlloriv - A mi el quickcheck no me ha encontrado ningún contra ejemplo*)

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

-- "juaruipav"
lemma 
  "sust x y (borraTodas x zs) = borraTodas x zs"
quickcheck
oops
(*Quickcheck found a counterexample:

x = a⇩2
y = a⇩1
zs = [a⇩1]

Evaluated terms:
sust x y (borraTodas x zs) = [a⇩2]
borraTodas x zs = [a⇩1]*)


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

-- "maresccas4 diecabmen1 domlloriv marescpla"

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

--"irealetei"
lemma 
  "sust x y (borraTodas x zs) = borraTodas x zs"
proof (induct zs)
  show "sust x y (borraTodas x []) = borraTodas x []" by simp
next
  fix a zs
  assume HI:"sust x y (borraTodas x zs) = borraTodas x zs"
  show "sust x y (borraTodas x (a # zs)) = borraTodas x (a # zs)"
  proof (cases)
    assume A:"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 "sust x y (borraTodas x (a # zs))= borraTodas x (a # zs)" using A by simp
  next
     assume A:"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 A by simp
    also have "...=a#(borraTodas x zs)" using HI by simp
    finally show "sust x y (borraTodas x (a # zs))= borraTodas x (a # zs)" using A by simp
   qed
qed

--"juaruipav"
lemma 
  "sust x y (borraTodas x zs) = borraTodas x zs"
proof (induct zs)
  show " sust x y (borraTodas x []) = borraTodas x []" by simp
next
fix a zs
 assume HI: "sust x y (borraTodas x zs) = borraTodas x zs"
 show " sust x y (borraTodas x (a # zs)) = borraTodas x (a # zs)"
 proof(cases)
 assume C1: "x=a"
 show " sust x y (borraTodas x (a # zs)) = borraTodas x (a # zs)" using HI using C1 by simp
 next
 assume C2: "x≠a"
  show " sust x y (borraTodas x (a # zs)) = borraTodas x (a # zs)" using HI using C2 by simp
qed
qed
(* Juaruipav: Falla con el siguiente mensaje:  1. sust x y (borraTodas x zs) = borraTodas x zs ⟹ x ≠ a ⟹ False
Relacionado con la salida del quickcheck*)

--"julrobrel"
lemma
  "sust x y (borraTodas x zs) = borraTodas x zs"
proof (induct zs)
  show "sust x y (borraTodas x []) = borraTodas x []" by simp
next
  fix a zs
  assume HI:"sust x y (borraTodas x zs) = borraTodas x zs"
  show "sust x y (borraTodas x (a#zs)) = borraTodas x (a#zs)"
  proof (cases)
    assume C1: "x=a"
    then have "sust x y (borraTodas x (a#zs)) = sust x y (borraTodas x zs)" using C1 by simp
    also have "...=borraTodas x zs" using HI by simp
    also have "...=borraTodas x (a#zs)" using C1 by simp
    finally show "sust x y (borraTodas x (a#zs)) = borraTodas x (a#zs)" .
  next
   assume C2: "¬(x=a)"
   then have "sust x y (borraTodas x (a#zs)) = sust x y (a#borraTodas x zs)" using C2 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
   also have "...=borraTodas x (a#zs)" using C2 by simp
   finally show "sust x y (borraTodas x (a#zs)) = borraTodas x (a#zs)" .
  qed
qed




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

-- "maresccas4 irealetei juaruipav domlloriv diecabmen1 marescpla julrobrel"

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 irealetei juaruipav domlloriv diecabmen1 marescpla julrobrel"

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 irealetei domlloriv diecabmen1 marescpla"

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

--"julrobrel"
lemma borraTodas_cat_jrr:
  "borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)"
by (induct xs) auto

-- "juaripav"
lemma borraTodas_conj:
  "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 diecabmen1"

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

--"irealetei"
lemma "borraTodas_concatenacion":
  "borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)"
proof (induct xs)
  show "borraTodas x ([] @ ys) = borraTodas x [] @ borraTodas x ys" by simp
next
  fix a xs
  assume HI:"borraTodas x (xs @ ys) = borraTodas x xs @ borraTodas x ys"
  show " borraTodas x ((a # xs) @ ys) = borraTodas x (a # xs) @ borraTodas x ys"
  proof (cases)
    assume A:"(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 " borraTodas x ((a # xs) @ ys) = borraTodas x (a # xs) @ borraTodas x ys" using A by simp
  next
    assume A:"(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 " borraTodas x ((a # xs) @ ys) = borraTodas x (a # xs) @ borraTodas x ys" using A by simp
  qed
qed

-- "juaruipav"
lemma 
  "borraTodas x (xs@ys) = (borraTodas x xs)@(borraTodas x ys)"
proof (induct xs)
  show " borraTodas x ([] @ ys) = borraTodas x [] @ borraTodas x ys" by simp
next
fix a xs
assume HI: " borraTodas x (xs @ ys) = borraTodas x xs @ borraTodas x ys "
show "borraTodas x ((a # xs) @ ys) = borraTodas x (a # xs) @ borraTodas x ys"
proof(cases)
 assume C1: "x=a"
  show "borraTodas x ((a # xs) @ ys) = borraTodas x (a # xs) @ borraTodas x ys" using HI using C1 by simp
 next
 assume C2: "x≠a"
  show "borraTodas x ((a # xs) @ ys) = borraTodas x (a # xs) @ borraTodas x ys" using HI using C2 by simp
qed
qed

(* Es curioso como Isabelle me avisa como poder resolverlo con un lema anterior:

Auto solve_direct: The current goal can be solved directly with
  R6.borraTodas_conj:
    borraTodas ?x (?xs @ ?ys) =
    borraTodas ?x ?xs @ borraTodas ?x ?ys *)



--"julrobrel"
lemma 
  "sust x y (borraTodas x zs) = borraTodas x zs"
proof (induct zs)
  show "sust x y (borraTodas x []) = borraTodas x []" by simp
next
  fix a zs
  assume HI:"sust x y (borraTodas x zs) = borraTodas x zs"
  show "sust x y (borraTodas x (a#zs)) = borraTodas x (a#zs)"
  proof (cases)
    assume C1: "x=a"
    then have "sust x y (borraTodas x (a#zs)) = sust x y (borraTodas x zs)" using C1 by simp
    also have "...=borraTodas x zs" using HI by simp
    also have "...=borraTodas x (a#zs)" using C1 by simp
    finally show "sust x y (borraTodas x (a#zs)) = borraTodas x (a#zs)" .
  next
   assume C2: "¬(x=a)"
   then have "sust x y (borraTodas x (a#zs)) = sust x y (a#borraTodas x zs)" using C2 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
   also have "...=borraTodas x (a#zs)" using C2 by simp
   finally show "sust x y (borraTodas x (a#zs)) = borraTodas x (a#zs)" .
  qed
qed


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

-- "maresccas4 diecabmen1 marescpla"

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

-- "irealetei"

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

-- "juaruipav domlloriv"

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


-- "julrobrel"
lemma 
  "rev (borraTodas x xs) = borraTodas x (rev xs)"
by (induct xs) (auto simp add:borraTodas_cat_jrr)

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

--"irealetei domlloriv"
lemma 
  "rev (borraTodas x xs) = borraTodas x (rev xs)"
proof (induct xs)
  show "rev (borraTodas x []) = borraTodas x (rev [])" by simp
next
  fix a xs
  assume HI:" rev (borraTodas x xs) = borraTodas x (rev xs)"
  show "rev (borraTodas x (a # xs)) = borraTodas x (rev (a # xs))"
  proof (cases)
    assume A:"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 (a#(rev xs))" using A by simp
    finally show "rev (borraTodas x (a # xs)) = borraTodas x (rev (a # xs))"using A by (simp add:borraTodas_concatenacion)
  next
    assume A:"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))@[a])" using HI by simp
    finally show "rev (borraTodas x (a # xs)) = borraTodas x (rev (a # xs))"using A by (simp add:borraTodas_concatenacion)
  qed
 qed

--"juaruipav"
lemma 
  "rev (borraTodas x xs) = borraTodas x (rev xs)"
proof(induct xs)
  show "rev (borraTodas x []) = borraTodas x (rev [])" by simp
next
fix a xs
assume HI:"rev (borraTodas x xs) = borraTodas x (rev xs)"
show "rev (borraTodas x (a # xs)) = borraTodas x (rev (a # xs))"
proof(cases)
   assume C1: "x=a"
   show "rev (borraTodas x (a # xs)) = borraTodas x (rev (a # xs))" using HI using C1 by (simp add:borraTodas_conj)
   next
   assume C2: "x≠a"
   show "rev (borraTodas x (a # xs)) = borraTodas x (rev (a # xs))" using HI using C2 by (simp add:borraTodas_conj)
qed
qed

--"julrobrel"
lemma 
  "rev (borraTodas x xs) = borraTodas x (rev xs)"
proof (induct xs)
  show "rev (borraTodas x []) = borraTodas x (rev [])" by simp
next
  fix a xs
  assume HI: "rev (borraTodas x xs) = borraTodas x (rev xs)"
    then have "rev (borraTodas x (a#xs)) = rev (borraTodas x ([a]@xs))" by simp
    also have "...=rev((borraTodas x [a]) @ (borraTodas x xs))" by (simp add:borraTodas_cat_jrr)
    also have "...=rev(borraTodas x xs) @ rev(borraTodas x [a])" by simp
    also have "...=borraTodas x (rev xs) @ borraTodas x (rev [a])" using HI by simp
    also have "...=borraTodas x ((rev xs)@rev [a])" by (simp add:borraTodas_cat_jrr)
    also have "...=borraTodas x ((rev xs)@[a])" by simp
    also have "...=borraTodas x (rev (a#xs))" by simp
    finally show "rev (borraTodas x (a#xs)) = borraTodas x (rev (a#xs))" .
qed

end