Demostración automática de teoremas (2014-15) Demostración automática de teoremas (2014-15)

header {* R7: Definiciones inductivas: clausuras *}

theory R7
imports Main
begin

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 1. Considerar la siguiente definición de la clausura tran-
 sitiva de una relación r, y probar que es la menor relación reflexiva y
 transitiva que contiene a r.

 Nota: Establecer los lemas necesarios.
  --------------------------------------------------------------------- 
*}

inductive star' :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool" for r where
refl': "star' r x x" |
step': "star' r x y ⟹ r y z ⟹ star' r x z"


text {*  
  --------------------------------------------------------------------- 
  Ejercicio 2. 
  Considerar la siguiente definición inductiva. Probar que 
  "star' r x y sysss (∃ n. iter r n x y)"
  --------------------------------------------------------------------- 
*}
inductive iter :: "('a ⇒ 'a ⇒ bool) ⇒ nat ⇒ 'a ⇒ 'a ⇒ bool" 
for r where
  iterRefl: "iter r 0 x x"
| iterStep: "iter r n x y ⟹ r y z ⟹ iter r (n+1) x z"


text {*  
  --------------------------------------------------------------------- 
  Ejercicio 3. 
  Dar una definición inductiva de la clausura reflexiva, simétrica y 
  transitiva de una relación binaria r.
  --------------------------------------------------------------------- 
*}

text {*
inductive rst1 :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ 'a ⇒ bool"  for r where
 ...
*}

text {*  
  --------------------------------------------------------------------- 
  Ejercicio 4. Probar que, en efecto, es la menor relación reflexiva, 
  simétrica y transitiva que contiene a r.

  Nota: Establecer los lemas auxiliares necesarios.
   --------------------------------------------------------------------- 
*}

end