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

header {* T15 (b) Interpretaciones de teorías: sustitución
                  de definiciones *}

theory T15b
imports T14
begin

text {* En la interpretación siguiente, se añade la sustitución
de la relación less definida en el contexto local de ódenes 
parciales, por la relación  <  en los enteros.
Se generan dos objetivos
  1. partial_order op ≤ 
  2. partial_order.less op ≤ x y = (x < y)

El primero de ellos se prueba de forma automática, expandiendo las 
definiciones del contexto local.
Para probar el segundo objetivo es necesario expandir la definición
de la relación less para el caso particular de la relación  ≤. 
Observar que hay que hacerlo de forma explícita, pues aún no estamos
en el contexto local interpretado.
*}

interpretation int: partial_order "op ≤ :: [int, int] ⇒ bool"
    where "int.less x y = (x < y)"
  proof -
    show "partial_order (op ≤ :: int ⇒ int ⇒ bool)"
      by unfold_locales auto
    show "partial_order.less op ≤ x y = (x < y)"
      unfolding partial_order.less_def [OF `partial_order op ≤`]
      by auto
  qed

end