Rel 12 (sol)

chapter ‹R12: Razonamiento sobre programas en Isabelle/HOL (III)›
 
theory R12_sol
imports Main 
begin

text ‹------------------------------------------------------------------ 
  En toda la relación de ejercicios las demostraciones han de realizarse
  de las formas siguientes:
  + en lenguaje natural
  + aplicativa o declarativa usando "simp"
  + aplicativa o declarativa usando "simp only: ..."  
  + automática

  Además, se recomienda el uso de lemas auxiliares (nuevos o de los 
  ejercicios anteriores) para que las demostraciones sean más cortas y 
  claras.
  ---------------------------------------------------------------------›
 
text ‹------------------------------------------------------------------ 
  Ejercicio 1. Definir la función
     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 []       = False"
| "estaEn x (a # xs) = (a = x ∨ estaEn x xs)"

text ‹------------------------------------------------------------------
  Ejercicio 2. Definir la función 
     sublista :: "'a list ⇒ 'a list ⇒ bool
  tal que (sublista xs ys) se verifica si todos los elementos de la
  lista xs están en la lista ys. Por ejemplo,
     sublista [(1::nat),2,3] [3,2,1,2] = True
     sublista [(1::nat),2,3] [2,1,2]   = False
 ----------------------------------------------------------------------›

fun sublista :: "'a list ⇒ 'a list ⇒ bool" where
  "sublista [] ys       = True"
| "sublista (x # xs) ys = (estaEn x ys ∧ sublista xs ys )"

text ‹------------------------------------------------------------------
  Ejercicio 3. Demostrar la siguiente propiedad: si xs es sublista de 
  ys, entonces xs también es sublista de la lista (y # ys). Es decir,
     sublista xs ys ⟹ sublista xs (y # ys)
 ----------------------------------------------------------------------›

― ‹Demostración en lenguaje natural:
Por inducción en xs.

+ Caso base: Sea xs = []. 
  Supongamos que "sublista [] ys", entonces se tiene 
  "sublista [] (y # ys)" por la definición de sublista.

+ Paso inductivo: Sea x un elemento y xs una lista de elementos que
  verifica la hipótesis de inducción (HI): 
     sublista xs ys ⟶ sublista xs (y # ys)
  Hay que probar que 
     sublista (x # xs) ys ⟶ sublista (x # xs) (y # ys)
  Para ello, se supone que
     1. sublista (x # xs) ys 
  y basta probar que 
     sublista (x # xs) (y # ys).
  La demostración es
     2. estaEn x ys /\ sublista xs ys             (de 1, por def. sublista)
     3. sublista xs ys                            (de 2, por conjunct2)
     4. sublista xs (y # ys)                      (de 4 e HI, por mp)
     5. estaEn x ys                               (de 2, por conjunct1)
     6. estaEn x (y # ys)                         (de 5, por def. estaEn)
     7. estaEn x (y # ys) /\ sublista xs (y # ys) (de 6 y 4, por conjI)
     8. sublista (x # xs) (y # ys)                (de 7, por def. sublista)
›

― ‹Demostración declarativa con simp:›
lemma  
  "sublista xs ys ⟶ sublista xs (y # ys)"
proof (induct xs)
  show "sublista [] ys ⟶ sublista [] (y # ys)" by simp
next
  fix a xs
  assume HI: "sublista xs ys ⟶ sublista xs (y # ys)" 
  show "sublista (a # xs) ys ⟶ sublista (a # xs) (y # ys)" 
    by (simp add: HI)
qed

― ‹Demostración declarativa detallada:›
lemma sublistaMono_d: 
  "sublista xs ys ⟶ sublista xs (y # ys)"
proof (induct xs)
  show "sublista [] ys ⟶ sublista [] (y # ys)" 
  proof (rule impI)
    assume "sublista [] ys" 
    show "sublista [] (y # ys)" 
      by (simp only: sublista.simps(1))
  qed
next
  fix a xs
  assume HI: "sublista xs ys ⟶ sublista xs (y # ys)" 
  show "sublista (a # xs) ys ⟶ sublista (a # xs) (y # ys)" 
  proof (rule impI)
    assume "sublista (a # xs) ys"
    then have 1: "(estaEn a ys ∧ sublista xs ys )" 
      by (simp only: sublista.simps(2))
    then have "estaEn a ys" 
      by (rule conjunct1)
    then have "y = a ∨ estaEn a ys" 
      by (rule disjI2)
    then have "estaEn a (y # ys)" 
      by (simp only: estaEn.simps(2))
    have "sublista xs ys" 
      using 1 by (rule conjunct2)
    with HI have "sublista xs (y # ys)" 
      by (rule mp)
    with ‹estaEn a (y # ys)› 
    have "estaEn a (y # ys) ∧ sublista xs (y # ys)" 
      by (rule conjI)
    then show "sublista (a # xs) (y # ys)" 
      by (simp only: sublista.simps(2))
  qed
qed

lemma sublistaMono_de: 
  assumes "sublista xs ys"
  shows "sublista xs (y#ys)"
proof -
  have  "sublista xs ys ⟶ sublista xs (y#ys)" 
    by (rule sublistaMono_d)
  then show  "sublista xs (y#ys)" 
    using assms by (rule mp)
qed

― ‹Demostración aplicativa detallada:›
lemma sublistaMono: "sublista xs ys ⟹ sublista xs (y # ys)"
  apply (induct xs)
   apply (simp only: sublista.simps(1))
  apply (simp only: sublista.simps(2))
  apply (rule conjI)
   apply (erule conjE)
   apply (simp only: estaEn.simps(2))
   apply (rule disjI2)
   apply (simp only: implies_True_equals)+
  done

text ‹------------------------------------------------------------------
  Ejercicio 4. Demostrar que la relación sublista es reflexiva. Es 
  decir,
     sublista xs xs
  ---------------------------------------------------------------------›

― ‹Demostración en lenguaje natural:
Por inducción en xs.

+ Caso base: xs = []
   Se verifica "sublista [] []"     (por def. de sublista)

+ Paso inductivo: Sean x un elemento y xs una lista de elementos que
  verifican la hipótesis de inducción (HI):
     sublista xs xs
  Hay que probarque 
     sublista (x # xs) (x # xs)

  En efecto:
     1. sublista xs xs                           (por HI)
     2. sublista xs (x # xs)                     (por 1 y sublistaMono)
     3. estaEn x (x # xs)                        (por lema auxiliar)
     4. estaEn x (x # xs) ∧ sublista xs (x # xs) (de 3 y 2, por conjI)
     5. sublista (x # xs) (x # xs)               (de 4 por def. sublista)
›

― ‹Demostración declarativa:›
lemma sublistaReflexiva_d: "sublista xs xs"
proof (induct xs)
  show "sublista [] []" 
    by (simp only: sublista.simps(1))
next
  fix x :: "'a" and xs :: "'a list"
  assume "sublista xs xs"
  then show "sublista (x # xs) (x # xs)"
    by (simp add: sublistaMono) 
qed

(* Lema auxiliar *)
lemma estaEn1: "estaEn x (x # xs)"
  apply (simp only: estaEn.simps(2))
  apply (rule disjI1)
  apply (rule refl)
  done

― ‹Demostración declarativa detallada›
lemma  "sublista xs xs"
proof (induct xs)
  show "sublista [] []" 
    by (simp only: sublista.simps(1))
next
  fix x :: "'a" and xs :: "'a list"
  assume "sublista xs xs"
  then have "sublista xs (x # xs)" 
    by (rule sublistaMono)
  then have "estaEn x (x # xs) ∧ sublista xs (x # xs)" 
    by (simp only: estaEn1)
  then show "sublista (x # xs) (x # xs)" 
    by (simp only: sublista.simps(2))
qed

― ‹Demostración aplicativa detallada›
lemma sublistaReflexiva: "sublista xs xs"
  apply (induct xs)
   apply (simp only: sublista.simps(1))
  apply (simp only: sublista.simps(2))
  apply (rule conjI)
   apply (rule estaEn1)
  apply (rule sublistaMono, assumption)
  done

text ‹------------------------------------------------------------------
  Ejercicio 5. Probar, como corolario, que 
     sublista xs (x # xs)
  ---------------------------------------------------------------------›

― ‹Demostración en lenguaje natural:
 Se verifica "sublista xs xs" por el lema sublistaReflexiva. Por tanto, 
 aplicando el lema sublistaMono, se tiene "sublista xs (x # xs)".›

― ‹Demostración declarativa detallada›
corollary sublistaInc_d: "sublista xs (x # xs)"
proof-
  have "sublista xs xs" 
    by (rule sublistaReflexiva)
  then show  "sublista xs (x # xs)" 
    by (rule sublistaMono)
qed

― ‹Demostración aplicativa detallada›
corollary sublistaInc: "sublista xs (x # xs)"
  apply (rule sublistaMono)
  apply (rule sublistaReflexiva)
  done

text ‹------------------------------------------------------------------
  Ejercicio 6. Probar que la relación sublista es transitiva. Es decir,
     sublista xs ys ∧ sublista ys zs ⟶ sublista xs zs
  ---------------------------------------------------------------------›

― ‹Demostración en lenguaje natural:
Por inducción en xs.

+ Caso base: Supongamos que xs = [].
  Hay que probar que
     "sublista [] ys ∧ sublista ys zs ⟶ sublista [] zs"
  Para ello, supongamos que 
     "sublista [] ys ∧ sublista ys zs"
  Entonces "sublista [] zs" se tiene por la definición de sublista.

+ Paso inductivo: Sean a un elemento y xs una lista de elementos para
 los que se cumple la hipótesis de inducción (HI):
     "sublista xs ys ∧ sublista ys zs ⟶ sublista xs zs"
  Hay que probar que
     "sublista (a # xs) ys ∧ sublista ys zs ⟶ sublista (a # xs) zs" 
  Para ello, supongamos que 
    1. "sublista (a # xs) ys ∧ sublista ys zs" 
  y hay que probar que 
    "sublista (a # xs) zs".
  Su prueba es
    2. (estaEn a ys ∧ sublista xs ys) ∧ sublista ys zs 
          (de 1, por def. sublista)
    3. sublista xs ys ∧ sublista ys zs                 
          (de 2, por la asociativa de la conjunción y la eliminación de 
          la conjunción)
    4. sublista xs zs                                   
          (de 3, por HI)
    5. estaEn a ys                                     
          (de 2, por eliminación de la conjunción)
    6. sublista ys zs                                   
          (de 3)
    7. estaEn a zs                                      
          (de 5 y 6 por lema auxiliar)
    8. sublista (a # xs) zs                                 
          (de 7 y 4, por def. sublista)
›

(* Auxiliar *)
lemma sublistaEstaEn: 
  "estaEn x xs ∧ sublista xs ys ⟶ estaEn x ys"
  apply (induct xs)
   apply (rule impI)
   apply (simp only: estaEn.simps(1))
   apply (drule conjunct1)
   apply (simp only: False_implies_equals)
  apply (rule impI)
  apply (simp only: estaEn.simps(2))
  apply (erule conjE)
  apply (erule disjE)
   apply (simp only: sublista.simps(2))
  apply (simp only: sublista.simps(2))
  done

― ‹Demostración declarativa:›

lemma sublistaTransitiva_e: 
  "sublista xs ys ∧ sublista ys zs ⟶ sublista xs zs"
proof (induct xs)
  show "sublista [] ys ∧ sublista ys zs ⟶ sublista [] zs"
    by simp
next
  fix a xs
  assume HI:"sublista xs ys ∧ sublista ys zs ⟶ sublista xs zs"
  show " sublista (a # xs) ys ∧ sublista ys zs ⟶ sublista (a # xs) zs" 
  proof (rule impI)
    assume "sublista (a # xs) ys ∧ sublista ys zs"
    then have 1: "(estaEn a ys ∧ sublista xs ys) ∧ sublista ys zs" by simp
    then have "estaEn a ys" by simp
    have "sublista ys zs" using 1 by simp
   then have "estaEn a zs" using ‹estaEn a ys› 
     by (simp add: sublistaEstaEn)
   have "sublista xs ys ∧ sublista ys zs" using 1 by simp
   then have "sublista xs zs" using HI by simp
   then show "sublista (a # xs) zs" using ‹estaEn a zs› by simp
 qed
qed

― ‹Demostración declarativa detallada›
lemma sublistaTransitiva_d: 
  "sublista xs ys ∧ sublista ys zs ⟶ sublista xs zs"
proof (induct xs)
  show "sublista [] ys ∧ sublista ys zs ⟶ sublista [] zs"
  proof (rule impI)
    assume "sublista [] ys ∧ sublista ys zs"
    show "sublista [] zs" 
      by (simp only: sublista.simps(1))
  qed
next
  fix a xs
  assume HI: "sublista xs ys ∧ sublista ys zs ⟶ sublista xs zs"
  show " sublista (a # xs) ys ∧ sublista ys zs ⟶ sublista (a # xs) zs" 
  proof (rule impI)
    assume "sublista (a # xs) ys ∧ sublista ys zs"
    then have "(estaEn a ys ∧ sublista xs ys) ∧ sublista ys zs" 
      by (simp only: sublista.simps(2))
    then have 1: "estaEn a ys ∧ (sublista xs ys ∧ sublista ys zs)" 
      by (simp only: conj_assoc)
    then have "sublista xs ys ∧ sublista ys zs" 
      by (rule conjunct2)
    with HI have "sublista xs zs" 
      by (rule mp)
    have "estaEn a ys" 
      using 1 by (rule conjunct1)
    have "sublista ys zs" 
      using ‹sublista xs ys ∧ sublista ys zs› by (rule conjunct2)
    with ‹estaEn a ys› have "estaEn a zs" 
      by (simp only: sublistaEstaEn)
    then show "sublista (a # xs) zs" 
      using ‹sublista xs zs› by (simp only: sublista.simps(2))
  qed
qed

― ‹Demostración aplicativa detallada›
lemma sublistaTransitiva: 
  "sublista xs ys ∧ sublista ys zs ⟶ sublista xs zs"
  apply (induct xs) 
   apply (rule impI)
   apply (simp only: sublista.simps(1))
  apply (simp only: sublista.simps(2))
  apply (rule impI)
  apply (rule conjI)
   apply (simp only: conj_comms)
   apply (frule conjunct1)
   apply (drule conjunct2)+
   apply (simp only: sublistaEstaEn)
  apply (erule mp)
  apply (rule conjI)
   apply (drule conjunct1)
   apply (drule conjunct2, assumption)+
  done
 
text ‹------------------------------------------------------------------
  Ejercicio 7. Definir la función
     coge :: nat ⇒ 'a list ⇒ 'a list
  tal que (coge n xs) es la lista de los n primeros elementos de xs. Por 
  ejemplo, 
     coge 2 [a,c,d,b,e] = [a,c]
  ------------------------------------------------------------------ ›

fun coge :: "nat ⇒ 'a list ⇒ 'a list" where
  "coge n []           = []"
| "coge 0 xs           = []"
| "coge (Suc n) (x # xs) = x # (coge n xs)"

text ‹------------------------------------------------------------------
  Ejercicio 8. Probar que 
     coge 0 xs = []
  ---------------------------------------------------------------------›

― ‹Demostración en lenguaje natural:
Por casos sobre los posibles valores de xs.

+ Caso 1: Supongamos que xs = []. En este caso, "coge 0 [] = []" por la 
  primera ecuación de la definición de coge.

+ Caso 2: Supongamos quexs es de la forma y#ys. En este caso, 
  "coge 0 (y#ys) = []" por la segunda ecuación de la definición de coge.
›

― ‹Demostración declarativa detallada›
lemma coge0_d: "coge 0 xs = []"
proof (cases xs)
  case Nil
  then show ?thesis by (simp only: coge.simps(1))
next
  case Cons
  then show ?thesis by (simp only: coge.simps(2))
qed

― ‹Demostración aplicativa detallada›
lemma coge0: "coge 0 xs = []"
  apply (case_tac xs) 
   apply (simp only: coge.simps(1))
  apply (simp only: coge.simps(2))
  done

text ‹------------------------------------------------------------------
  Ejercicio 9. Probar que 
     length xs ≤ n ⟹ coge n xs = xs
  ---------------------------------------------------------------------›

― ‹Demostración en lenguaje natural:
Por inducción según el esquema coge.induct. Se generan los tres casos 
siguientes:

+ Caso 1: "⋀n. length [] ≤ n ⟶ coge n [] = []"
   Sea n cualquiera. Por la regla impI, hay que suponer "length [] ≤ n"
   y probar "coge n [] = []", lo que es cierto por la definición de coge.

+ Caso 2: "⋀x xs. length (x # xs) ≤ 0 ⟶ coge 0 (x # xs) = x # xs"
  Sean x un elemento y xs una lista. 
     2.1. length (x # xs) ≤ 0         (por supuesto)
     2.2. False                       (de 2.1 por def. de length)
     2.3. coge 0 (x # xs) = x # xs    (de 2.2 por eliminación de False)
    
+ Caso 3. "⋀n x xs. 
           length xs ≤ n ⟶ coge n xs = xs ⟹ 
           length (x # xs) ≤ Suc n ⟶ coge (Suc n) (x # xs) = x # xs"
  
   Sean n un número natural, x un elememto y xs una lista.
   HI: "length xs ≤ n ⟶ coge n xs = xs"
   Hay que probar: 
      length (x # xs) ≤ Suc n ⟶ coge (Suc n) (x # xs) = x # xs"
   Aplicando la regla impI, suponemos 3.1.
      3.1. length (x # xs) ≤ Suc n  
      3.2.  1 + length xs ≤ Suc n               (de 3.1 por def. de length)
      3.3. length xs ≤ n                        (de 3.2 por monotonía)
      3.4. coge n xs = xs                        (de 3.4 por HI)
      3.5. coge (Suc n) (x # xs) = x # coge n xs (por def. de coge) 
      3.6. coge (Suc n) (x # xs) = x # xs        (de 3.5 y 3.4)
›

― ‹Demostración declarativa›
lemma  
  "length xs ≤ n ⟶ coge n xs = xs"
proof (induct rule: coge.induct)
  fix n
  show "length [] ≤ n ⟶ coge n [] = []" by simp
next
  fix x :: "'a" and xs :: "'a list"
  show "length (x # xs) ≤ 0 ⟶ coge 0 (x # xs) = x # xs" by simp
next
  fix n
  fix x :: "'a" and xs :: "'a list"
  assume HI: "length xs ≤ n ⟶ coge n xs = xs"
  show "length (x # xs) ≤ Suc n ⟶ coge (Suc n) (x # xs) = x # xs" 
    by (simp add: HI)
qed

― ‹Demostración declarativa detallada ›
lemma cogeTodos_d: 
  "length xs ≤ n ⟶ coge n xs = xs"
proof (induct rule: coge.induct)
  fix n
  show "length [] ≤ n ⟶ coge n [] = []" 
  proof (rule impI)
    assume "length [] ≤ n"
    show "coge n [] = []" 
      by (simp only:coge.simps(1))
  qed
next
  fix x :: "'a" and xs :: "'a list"
  show "length (x # xs) ≤ 0 ⟶ coge 0 (x # xs) = x # xs" 
  proof (rule impI)
    assume "length (x # xs) ≤ 0"
    then have False 
      by (simp only: list.size)
    then show "coge 0 (x # xs) = x # xs" 
      by (rule FalseE)
  qed
next
  fix n and x :: "'a" and xs :: "'a list"
  assume HI: "length xs ≤ n ⟶ coge n xs = xs"
  show "length (x # xs) ≤ Suc n ⟶ coge (Suc n) (x # xs) = x # xs" 
  proof (rule impI)
    assume "length (x # xs) ≤ Suc n"
    then have "1 + length xs ≤ Suc n" 
      by (simp only: list.size(4))
    then have "length xs ≤ n" 
      by (simp only: Suc_le_mono)
    with HI have "coge n xs = xs" 
      by (rule mp)
    have "coge (Suc n) (x # xs) = x # coge n xs" 
      by (simp only: coge.simps(3))
    also have "… = x#xs" 
      using ‹coge n xs = xs› by (rule arg_cong)
    finally show "coge (Suc n) (x # xs) = x # xs" 
      by this
  qed
qed

lemma cogeTodos_de: 
  assumes "length xs ≤ n"
  shows "coge n xs = xs"
proof-
  have "length xs ≤ n ⟶ coge n xs = xs" 
    by (rule cogeTodos_d)
  then show  "coge n xs = xs" 
    using assms by (rule mp)
qed

― ‹Demostración aplicativa detallada:›
lemma cogeTodos: "length xs ≤ n ⟹ coge n xs = xs"
  apply (induct rule: coge.induct)
    apply (simp only: coge.simps(1))
   apply (simp only: list.size)
  apply (simp only: coge.simps(3))
  apply (simp only: list.size)
  done

text ‹------------------------------------------------------------------
  Ejercicio 10. Probar que 
     length (coge n xs) ≤ n
  ---------------------------------------------------------------------›

― ‹Demostración en lenguaje natural:
Por inducción en n con xs arbitrario.

+ Caso base: Supongamos que n = 0.
    Hay que probar: ∀xs. length (coge 0 xs) ≤ 0
    En efecto, sea xs una lista cualquiera. 
         length (coge 0 xs)   
         = length []          (def. de coge)
         = 0                  (def. de length)   
         ≤ 0

+ Paso inductivo: 
    HI:  ∀xs. length (coge n xs) ≤ n
    Hay que probar:  ∀xs. length (coge (n+1) xs) ≤ n+1
    Sea xs una lista cualquiera. Consideramos dos casos para xs:
      + Caso 1: xs = []
        length (coge (n+1) [])   
        = length []              (def. de coge)
        = 0                      (def. de lenght)
        ≤ n+1                    (aritmética)

     + Caso 2: xs = y#ys
       length (coge (n+1) (y#ys)) 
       = length (y#(coge n ys))      (def. de coge) 
       = 1 + length (coge n ys)      (def. de length)
       ≤ 1 + n                      (HI aplicada a ys) 
       = n + 1
›

― ‹Demostración declarativa›
lemma  "length (coge n xs) ≤ n"
proof (induct n arbitrary: xs)
  fix xs :: "'a list"
  show "length (coge 0 xs) ≤ 0" 
    by (simp add: coge0)
next
  fix n and xs :: "'a list"
  assume HI: "(⋀xs :: 'a list. length (coge n xs) ≤ n)"
  show "length (coge (Suc n) xs) ≤ Suc n" 
  proof (cases xs)
    assume "xs = []" 
    then show "length (coge (Suc n) xs) ≤ Suc n" 
      by simp 
  next
    fix y ys 
    assume 1: "xs = y # ys"
    show "length (coge (Suc n) xs) ≤ Suc n" 
    proof -
      have 2: "length (coge n ys) ≤ n" 
        using HI by simp 
      have "length (coge (Suc n) xs) = 
            length (coge (Suc n) (y#ys))" 
        using 1 by (rule arg_cong)
      also have "… = length (y#(coge n ys))" 
        by (simp only: coge.simps(3))
      also have "… = 1 + length (coge n ys)" 
        by (simp only: list.size(4))
      also have "… ≤ 1 + n" using 2 
        by (rule add_left_mono)
      also have "… = Suc n"
        by (simp only: Suc_eq_plus1_left)
      finally show ?thesis 
        by this
    qed
  qed
qed

― ‹Demostración declarativa detallada›
lemma  "length (coge n xs) ≤ n"
proof (induct n arbitrary: xs)
  fix xs :: "'a list"
  show "length (coge 0 xs) ≤ 0" 
  proof- 
    have "coge 0 xs = []" 
      by (rule coge0)
    then have "length (coge 0 xs) = 0" 
      by (simp only: list.size(3))
    then show "length (coge 0 xs) ≤ 0" 
      by (simp only: order_refl)
  qed
next
  fix n and xs :: "'a list"
  assume HI: "(⋀xs :: 'a list. length (coge n xs) ≤ n)"
  show "length (coge (Suc n) xs) ≤ Suc n" 
  proof (cases xs)
    assume "xs = []" 
    then have "coge (Suc n) xs = coge (Suc n) []" 
      by (rule arg_cong)
    also have "… = []" 
      by (simp only:coge.simps(1))
    finally have "coge (Suc n) xs = []" 
      by this
    then have "length (coge (Suc n) xs) = 0" 
      by (simp only: list.size)      
    then show "length (coge (Suc n) xs) ≤ Suc n" 
      by (simp only: zero_le)
  next
    fix y ys 
    assume 1: "xs = y # ys"
    show "length (coge (Suc n) xs) ≤ Suc n" 
    proof -
      have 2: "length (coge n ys) ≤ n" 
        using HI by this
      have "length (coge (Suc n) xs) = 
            length (coge (Suc n) (y#ys))" 
        using 1 by (rule arg_cong)
      also have "… = length (y#(coge n ys))" 
        by (simp only: coge.simps(3))
      also have "… = 1 + length (coge n ys)" 
        by (simp only: list.size(4))
      also have "… ≤ 1 + n" using 2 
        by (rule add_left_mono)
      also have "… = Suc n"
        by (simp only: Suc_eq_plus1_left)
      finally show ?thesis 
        by this
    qed
  qed
qed

― ‹Demostración aplicativa detallada:›
lemma cogeLongN: "length (coge n xs) ≤ n"
  apply(induct n arbitrary:xs)
   apply (simp only: coge0)
   apply (simp only: list.size)
  apply (case_tac xs)
   apply (simp only: coge.simps(1))
   apply (simp only: list.size)
  apply (simp only: coge.simps(3))
  apply (simp only: list.size)
  apply (simp only: add_Suc_right)
  apply (simp only: Suc_le_mono)
  apply (simp only: add.right_neutral)
  done

text ‹------------------------------------------------------------------
  Ejercicio 11. Probar que 
      length (coge n xs) ≤ length xs
  ---------------------------------------------------------------------›

 ― ‹Demostración en lenguaje natural:
Por inducción en n con xs arbitrario. Hay que probar los siguientes casos:

+ Caso base: ⋀xs. length (coge 0 xs) ≤ length xs
  En efecto, sea xs una lista cualquiera,  
      length (coge 0 xs)
   =  0                    (por coge0 y prop. de length)
   ≤  0

+ Paso inductivo: sea n un número natural y xs una lista.
  Por  HI se tiene ⋀xs. length (coge n xs) ≤ length xs 
  Y hay que probar: length (coge (Suc n) xs) ≤ length xs
  La demostración se realiza por casos, según los posibles 
  casos de xs.

  + Caso 1: xs = []
    En este caso,
       1. coge (Suc n) [] = []                  (por def. de coge)
       2. length (coge (Suc n) xs) = 0          (de 1, por def. de length) 
       3. length (coge (Suc n) xs) ≤ length xs  (de 2, por def. de length)
   
  + Caso 2: xs = y # ys
    En este caso se tiene  
       1. length (coge n ys) ≤ length ys  (por HI)
       Luego:
       length (coge (Suc n) xs) 
     = length (coge (Suc n) (y#ys))      (por xs = y # ys)
     = length (y#(coge n ys))            (por def. de coge)
     = 1 + length (coge n ys)            (por def. de length)
     ≤ 1 + length ys"                    (por 1 y monotonía)
     = length (y#ys)                     (por def. de length)
     = length xs
›

― ‹Demostración declarativa detallada:›

lemma cogeLongL_d: "length (coge n xs) ≤ length xs"
proof (induct n arbitrary: xs) 
  fix xs :: "'a list"
  show "length (coge 0 xs) ≤ length xs" 
    by (simp only: coge0 list.size(3))
next
  fix n and xs :: "'a list"
  assume HI: "⋀xs:: 'a list. length (coge n xs) ≤ length xs"
  show "length (coge (Suc n) xs) ≤ length xs"
  proof (cases xs)
    assume "xs = []" 
    then have "coge (Suc n) xs = coge (Suc n) []" 
      by (rule arg_cong)
    also have "… = []" 
      by (simp only: coge.simps(1))
    finally have "coge (Suc n) xs = []" 
      by this
    then have "length (coge (Suc n) xs) = 0" 
      by (simp only: list.size) 
    then show "length (coge (Suc n) xs) ≤ length xs" 
      by (simp only: list.size(3))
  next
    fix y ys
    assume 1:"xs = y # ys"
    have 2: "length (coge n ys) ≤ length ys" 
      using HI by this
    have "length (coge (Suc n) xs) = length (coge (Suc n) (y#ys))" 
      using 1 by (rule arg_cong)
    also have "… = length (y#(coge n ys))" 
      by (simp only: coge.simps(3))
    also have "… = 1 + length (coge n ys)" 
      by (simp only: list.size(4))
    also have "… ≤ 1 + length ys" 
      using 2 by (simp only: Suc_le_mono)
    also have "… = length (y#ys)" 
      by (simp only: list.size(4))
    also have "… = length xs" 
      using 1 by (simp only:list.size(4))
    finally show "length (coge (Suc n) xs) ≤ length xs" 
      by this
  qed
qed

― ‹Demostración aplicativa detallada:›
lemma cogeLongL: "length (coge n xs) ≤ length xs"
  apply (induct n arbitrary: xs) 
   apply (simp only: coge0 list.size(3))
  apply (case_tac xs)
   apply (simp only: coge.simps(1))
  apply (simp only: coge.simps(3))
  apply (simp only: list.size(4))
  apply (simp only: add_Suc_right)
  apply (simp only: add.right_neutral)
  apply (simp only: Suc_le_mono)
  done

text ‹------------------------------------------------------------------
  Ejercicio 12. Probar que 
     length (coge n xs) = min n (length xs)
  ---------------------------------------------------------------------›

 ― ‹Demostración en lenguaje natural:
Se pueden realizar distintas demostraciones.

(A) Primera demostración:
  Por inducción en xs con n arbitrario, se generan los dos
    casos siguientes:
  + Caso base: ⋀n. length (coge n []) = min n (length [])
    En este caso, sea n un número natural,
       length (coge n [])       
    =  length []              (por def. de coge)
    =  0                      (por def. de length)
    = min n 0                 (por prop. de min)
    = min n (length [])
  
  + Paso inductivo:  ⋀x xs n.
       (⋀n. length (coge n xs) = min n (length xs)) ==>
            length (coge n (x # xs)) = min n (length (x # xs))
    Sean x un elemento, xs una lista y n un natural, se tiene
    HI: length (coge n xs) = min n (length xs)), y
    hay que probar: length (coge n (x # xs)) = min n (length (x # xs))
    Para ello, consideramos dos casos según n:
    
    + Caso 1: n = 0
      En este caso,
        length (coge 0 (x # xs))
      = length []                        (por coge0)
      = 0                                (por def. de length)
      = min 0 (length (x # xs))          (por prop. de min y length)

    + Caso 2: n = m + 1
      En este caso,
        length (coge (m+1) (x # xs))
      = length (x # (coge m xs))         (por def. de coge)
      = 1 + length m xs                  (por def. de coge)
      = 1 + min m (length xs)            (por HI)
      = min (1 + m) (1 + length xs)      (por prop. de min)
      = min n (length (x # xs))          (por def. de length)
  
(B) Segunda demostración:
  Por inducción en n con xs arbitrario, hay que demostrar los siguintes
  casos:
+ Caso base: ⋀xs. length (coge 0 xs) = min 0 (length xs)
  En efecto, sea xs una lista cualquiera.
    length (coge 0 xs)
  = length []                     (por def. de coge)
  = 0                             (por def. de length)
  = min 0 (length xs)             (por prop. de length)

+ Paso inductivo:
          ⋀n xs. (⋀xs. length (coge n xs) = min n (length xs)) ⟹ 
          length (coge (Suc n) xs) = min (Suc n) (length xs)
  Sea n un número natural y xs una lista cualquiera.
  Por HI: (⋀xs. length (coge n xs) = min n (length xs))
  Hay que probar: length (coge (Suc n) xs) = min (Suc n) (length xs)
  Para ello, distinguimos dos casos, según los valores que puede tomar
  xs.
  + Caso 1: xs = []
    En este caso, 
      length (coge (Suc n) []) 
    = length []                     (por def. de coge)
    = 0                             (por def. de length)
    = min (Suc n) 0                 (por prop. de min)
    = min (Suc n) (length [])       (por def. de length)

  + Caso 2: xs = y # ys
    En este caso,
       length (coge (Suc n) (y # ys)) 
     = length (y # (coge n ys))          (por def. de coge)
     = 1 + length (coge n ys)            (por def. de length)
     = 1 + min n (length ys)             (por HI aplicada a ys)
     = min (1 + n) (1 + length ys)       (por prop. de min)
     = min (Suc n) (length (y # ys))     (por def. de length)
     = min (Suc n) (length xs)
  
(C) Tercera demostración:
  Por doble desigualdad, probando como lemas auxiliares:
  C1: "length (coge n xs) ≤ min n (length xs)"
  C2: "min n (length xs) ≤ length (coge n xs)"

›

― ‹Demostración declarativa detallada de la primera demostración›

lemma lengthCogeMin_d:"length (coge n xs) = min n (length xs)"
proof (induct xs arbitrary:n)
  fix n::"nat"
  have "length (coge n []) = 0"
    by (simp only:coge.simps(1) list.size)
  then show "length (coge n []) = min n (length [])"
    by (simp only:list.size min_0R)
next
  fix x::"'a" and xs::"'a list" and n::"nat" 
  assume HI:"⋀n. length (coge n xs) = min n (length xs)"
  show "length (coge n (x#xs)) = min n (length (x#xs))"
  proof (cases n)
    assume "n = 0"
    then have "0 = n" by (rule sym)
    have "length (coge 0 (x#xs)) = 0" by (simp only:coge0 list.size)
    then have "length (coge 0 (x#xs)) = min 0 (length (x#xs))"
      by (simp only:min_0L)
    with`0=n` show "length (coge n (x#xs))  = min n (length (x#xs))"
      by (rule subst)
  next
    fix m::"nat"
    assume 1:"n = Suc(m)"
    then have 2:"Suc(m) = n" by (rule sym)
    have "length (coge n (x#xs)) = length (x # coge m xs)"
      using 1 by (simp only:coge.simps(3))
    then have "length (coge n (x#xs)) = 1 + length (coge m xs)"
      by (simp only:list.size)
    then have "length (coge n (x#xs)) = 1 + min m (length xs)"
      using HI by simp
    then have "length (coge n (x#xs)) = min (Suc m) (1+length xs)"
      by simp
    then show "length (coge n (x # xs)) = min n (length (x#xs))"
      using 2 by (simp only:list.size)
  qed
qed

― ‹Demostración aplicativa detallada de la segunda demostración:›
lemma lengthCogeMin: "length (coge n xs) = min n (length xs)"
  apply (induct n arbitrary: xs)
   apply (simp only: coge0)
   apply (simp only: list.size(3))
  apply (case_tac xs)
   apply (simp only: coge.simps(1))
   apply (simp only: list.size(3))
  apply (simp only: coge.simps(3))
  apply (simp only: list.size(4))
  done


― ‹Demostración declarativa detallada de la tercera demostración:›

lemma lengthCogeMenorMin: 
  "length (coge n xs) ≤ min n (length xs)"
proof -
  have 1: "length (coge n xs) ≤ n" 
    by (rule cogeLongN)
  have 2:  "length (coge n xs) ≤ length xs" 
    by (rule cogeLongL)
  show "length (coge n xs) ≤ min n (length xs)" 
    using 1 2 by (rule min.boundedI)
qed

lemma lengthCogeMayorMin:
  "min n (length xs) ≤ length (coge n xs)"
proof (induct n arbitrary: xs)
  fix xs:: "'a list"
  show "min 0 (length xs) ≤ length (coge 0 xs)" 
    by simp
next
  fix n and xs:: "'a list"
  assume HI: "⋀xs::'a list. min n (length xs) ≤ length (coge n xs)"
  show "min (Suc n) (length xs) ≤ length (coge (Suc n) xs)"
  proof (cases xs)
    assume "xs = []" 
    then show  "min (Suc n) (length xs) ≤ length (coge (Suc n) xs)" 
      by simp
  next
    fix y :: "'a" and ys :: "'a list"
    assume 1: "xs = y # ys"
    have 2: "min n (length ys) ≤ length (coge n ys)" 
      using HI by this
    show "min (Suc n) (length xs) ≤ length (coge (Suc n) xs)"
    proof -
      have "min (Suc n) (length xs) = min (Suc n) (length (y # ys))" 
        using 1 by (rule arg_cong)
      also have "… = min (Suc n) (1 + length ys)" 
        by (simp only: list.size(4))
      also have "… = 1 + min n (length ys)"  
        by (simp only: min_add_distrib_right)
      also have "… ≤ 1 + length (coge n ys)" 
        using HI by simp
      also have "… = length (y # coge n ys)" 
        by (simp only: list.size(4))
      also have "… = length (coge (Suc n) (y # ys))"  
        by (simp only: coge.simps(3))
      also have "… = length (coge (Suc n) xs)" 
        using 1 by (simp only: list.size(4))
      finally show ?thesis 
        by this
    qed
  qed
qed

lemma lengthCogeMin_d2: 
  "length (coge n xs) = min n (length xs)"
proof -
  have 1: "length (coge n xs) ≤ min n (length xs)" 
    by (rule lengthCogeMenorMin)
  have "min n (length xs) ≤ length (coge n xs)" 
    by (rule lengthCogeMayorMin)
  with 1 show ?thesis by (rule le_antisym)
qed


text ‹------------------------------------------------------------------
  Ejercicio 13. Probar que
     estaEn x (coge n xs) ⟹ estaEn x xs
  ---------------------------------------------------------------------›

― ‹Demostración en lenguaje natural:
Por inducción según el esquema coge.induct, se generan los tres
casos siguientes:

  + Caso base 1. ⋀n. estaEn x (coge n []) ⟶ estaEn x []
    Sea n un número natural. Hay que probar,
    estaEn x (coge n []) ⟶ estaEn x []. Para ello, se supone
    1.1. estaEn x (coge n [])
    y hay que probar estaEn x []
    En efecto,
        1.2. coge n [] = []        (por def. de coge)
    ==> 1.3 estaEn x []            (de 1.1 y 1.2)
    ==> 1.4. False                 (por def. de estaEn)
    ==> 1.5 estaEn x []            (de 1.4 y eliminación de False)

  + Caso base 2. ⋀y ys. estaEn x (coge 0 (y # ys)) ⟶ estaEn x (y # ys)
    Sean y un elemento e ys una lista. Hay que probar
    estaEn x (coge 0 (y # ys)) ⟶ estaEn x (y # ys). Para ello, se supone
    2.1. estaEn x (coge 0 (y # ys)) y basta probar estaEn x (y # ys)
    En efecto,
        2.2. coge 0 (y # ys) = []      (por el lema coge0)
    ==> 2.3. estaEn x []               (de 2.1 y 2.3)
    ==> 2.4. False                     (por def. de estaEn)
    ==> 2.5 estaEn x (y # ys)          (de 2.4. y eliminación de False) 

  + Paso inductivo: ⋀n y ys. estaEn x (coge n ys) ⟶ estaEn x ys 
               ⟹ estaEn x (coge (Suc n) (y # ys)) ⟶ estaEn x (y # ys)
   Sean n un número natural, y un elemento e ys una lista. Se tiene por
   HI: estaEn x (coge n ys) ⟶ estaEn x ys 
   Hay que probar: estaEn x (coge (Suc n) (y # ys)) ⟶ estaEn x (y # ys)
   Para ello, se supone
      3.1 estaEn x (coge (Suc n) (y # ys)) 
      y basta probar "estaEn x (y # ys)"
   En efecto,
      3.2 estaEn x (y # coge n ys)         (de 3.1, por def. de coge)
      3.3. y = x ∨ estaEn x (coge n ys)    (de 3.2, por def de estaEn)
      De 3.3, la prueba se sivide en dos casos
      + Caso 1: y = x
        En este caso, se verifica "estaEn y (y # ys)", por def. de estaEn

      + Caso 2: estaEn x (coge n ys)
        En este caso, por HI se tiene "estaEn x ys". Y, por def. de estaEn
        se verifica "estaEn x (y # ys)".
›

― ‹Demostración declarativa›
lemma 
  "estaEn x (coge n xs) ⟶ estaEn x xs"
proof (induct rule: coge.induct)
  fix n
  show "estaEn x (coge n []) ⟶ estaEn x []" 
    by simp
next 
  fix y ys
  show "estaEn x (coge 0 (y # ys)) ⟶ estaEn x (y # ys)"
  proof (rule impI)
    assume "estaEn x (coge 0 (y # ys))"
    then have "estaEn x []" 
      by simp
    then show "estaEn x (y # ys)" 
      by simp
  qed
next
  fix n and y :: "'a" and ys :: "'a list"
  assume HI: "estaEn x (coge n ys) ⟶ estaEn x ys" 
  show "estaEn x (coge (Suc n) (y # ys)) ⟶ estaEn x (y # ys)"
  proof (rule impI)
    assume "estaEn x (coge (Suc n) (y # ys))"
    then have "estaEn x (y# coge n ys)" 
      by simp
    then have "((y = x) ∨ (estaEn x (coge n ys)))" 
      by (simp only: estaEn.simps(2))
    then show "estaEn x (y # ys)"
    proof (rule disjE)
      assume "y = x"
      then have "((y = x) ∨ (estaEn x ys))" 
        by (rule disjI1)
      then show "estaEn x (y # ys)" 
        by (simp only:estaEn.simps(2))
    next  
      assume "estaEn x (coge n ys)"
      with HI have "estaEn x ys" 
        by (rule mp)
      then have "((y = x) ∨ (estaEn x ys))" 
        by (rule disjI2)
      then show "estaEn x (y # ys)" 
        by (simp only: estaEn.simps(2))
    qed
  qed
qed

― ‹Demostración declarativa detallada:›
lemma estaEnCoge_d: 
  "estaEn x (coge n xs) ⟶ estaEn x xs"
proof (induct rule: coge.induct)
  fix n
  show "estaEn x (coge n []) ⟶ estaEn x []" 
  proof (rule impI)
    assume "estaEn x (coge n [])"
    then have "estaEn x []" 
      by (simp only: coge.simps(1))
    then have False 
      by (simp only: estaEn.simps(1))
    then show "estaEn x []" 
      by (rule FalseE)
  qed
next 
  fix y ys
  show "estaEn x (coge 0 (y # ys)) ⟶ estaEn x (y # ys)"
  proof (rule impI)
    assume "estaEn x (coge 0 (y # ys))"
    then have "estaEn x []" 
      by (simp only: coge.simps(2))
    then have False 
      by (simp only: estaEn.simps(1))
    then show "estaEn x (y # ys)" 
      by (rule FalseE)
  qed
next
  fix n and y :: "'a" and ys :: "'a list"
  assume HI: "estaEn x (coge n ys) ⟶ estaEn x ys" 
  show "estaEn x (coge (Suc n) (y # ys)) ⟶ estaEn x (y # ys)"
  proof (rule impI)
    assume "estaEn x (coge (Suc n) (y # ys))"
    then have "estaEn x (y # coge n ys)" 
      by (simp only: coge.simps(3))
    then have "y = x ∨ estaEn x (coge n ys)" 
      by (simp only: estaEn.simps(2))
    then show "estaEn x (y # ys)"
    proof (rule disjE)
      assume "y = x"
      then have "y = x ∨ estaEn x ys" 
        by (rule disjI1)
      then show "estaEn x (y # ys)" 
        by (simp only: estaEn.simps(2))
    next  
      assume "estaEn x (coge n ys)"
      with HI have "estaEn x ys" 
        by (rule mp)
      then have "y = x ∨ estaEn x ys" 
        by (rule disjI2)
      then show "estaEn x (y # ys)" 
        by (simp only: estaEn.simps(2))
    qed
  qed
qed

lemma estaEnCoge_de: 
  assumes "estaEn x (coge n xs)" 
  shows "estaEn x xs"
proof-
  have "estaEn x (coge n xs) ⟶ estaEn x xs" 
    by (rule estaEnCoge_d)
  then show "estaEn x xs" using assms by (rule mp)
 qed

― ‹Demostración aplicativa detallada›
lemma estaEnCoge: 
  "estaEn x (coge n xs) ⟹ estaEn x xs"
  apply (induct rule: coge.induct)
    apply (simp only: coge.simps(1))
   apply (simp only: coge.simps(2) estaEn.simps(1))
  apply (simp only: coge.simps(3))
  apply (simp only: estaEn.simps(2))
  apply (erule disjE)
   apply (rule disjI1, assumption)
  apply (rule disjI2, assumption)
  done

text ‹------------------------------------------------------------------
  Ejercicio 14. Probar que 
     sublista (coge n xs) xs
  ---------------------------------------------------------------------›

 ― ‹Demostración en lenguaje natural:
Por inducción según el esquema coge.induct, se generan los tres casos
siguientes:

+ Caso base 1. ⋀n. sublista (coge n []) []
  Sea n un número natural.
     1.1. coge n [] = []            (por def. de coge)
     1.2. sublista [] []            (por def. de sublista)
     1.3. sublista (coge n []) []   (de 1.1 y 1.2)

+ Caso base 2. ⋀x xs. sublista (coge 0 (x # xs)) (x # xs)
  Sean x un elemento y xs una lista cualquiera
     2.1. coge 0 (x # xs) = []                 
          (por coge0)
     2.2. sublista (coge 0 (x # xs)) (x # xs)  
          (de 2.1,por def. de sublista)

+ Paso inductivo. ⋀n x xs. sublista (coge n xs) xs 
              ⟹ sublista (coge (Suc n) (x # xs)) (x # xs)
  Sean n un número natural, x un elemento y xs una lista. Se verifica por 
  HI: sublista (coge n xs) xs. 
  Y hay que probar: sublista (coge (Suc n) (x # xs)) (x # xs)
  En efecto,
      3.1. coge (Suc n) (x # xs) = x # coge n xs     
            (por def. de coge)
      3.2. estaEn x (x # xs)                         
            (por estaEn1)
      3.3. sublista (coge n xs) (x # xs)             
            (por HI y el lema sublistaMono)
      3.4. sublista (x # coge n xs) (x # xs)         
            (de 3.2, 3.3, por def. sublista)
      3.5. sublista (coge (Suc n) (x # xs)) (x # xs) 
            (de 3.1 y 3.4)
›

― ‹Demostración declarativa›
lemma  "sublista (coge n xs) xs"
proof (induct rule: coge.induct)
  fix n
  show "sublista (coge n []) []" 
    by (simp only: coge.simps(1) sublista.simps(1))
next
  fix y :: "'a" and ys :: "'a list"
  show "sublista (coge 0 (y # ys)) (y # ys)" 
    by simp
next
  fix n and x::"'a" and xs::"'a list"
  assume HI: "sublista (coge n xs) xs" 
  then have "sublista (x # coge n xs) (x # xs)" 
    by (simp add: sublistaMono)
  then show "sublista (coge (Suc n) (x # xs)) (x # xs)" 
    by simp
qed

― ‹Demostración declarativa detallada:›
lemma sublistaCoge_d: "sublista (coge n xs) xs"
proof (induct rule: coge.induct)
  fix n
  show "sublista (coge n []) []" 
    by (simp only: coge.simps(1) sublista.simps(1))
next
  fix y :: "'a" and ys :: "'a list"
  have "coge 0 (y#ys) = []" 
    by (rule coge0)
  then show "sublista (coge 0 (y # ys)) (y # ys)" 
    by (simp only: sublista.simps(1))
next
  fix n and x :: "'a" and xs :: "'a list"
  assume HI: "sublista (coge n xs) xs" 
  then have "sublista (coge n xs) (x # xs)"  
    by (simp only: sublistaMono)
  then have "(estaEn x (x # xs) ∧ sublista (coge n xs) (x # xs))" 
    by (simp only: estaEn1)
  then have "sublista (x # coge n xs) (x # xs)" 
    by (simp only: sublista.simps(2))
  then show "sublista (coge (Suc n) (x # xs)) (x # xs)" 
    by (simp only: coge.simps(3))
qed

― ‹Demostración aplicativa detallada›
lemma sublistaCoge: "sublista (coge n xs) xs"
  apply (induct rule: coge.induct)
    apply (simp only: coge.simps(1) sublista.simps(1))
   apply (simp only: coge.simps(2) sublista.simps(1))
  apply (simp only: coge.simps(3))
  apply (simp only: sublista.simps(2))
  apply (rule conjI)
   apply (rule estaEn1)
  apply (simp only: sublistaMono)
  done

end