Tema 15(a): sustitución de parámetros.

header {* T15a Interpretaciones de teorías: sustitución de parámetros *}

theory T15a
imports T14
begin

text {* Los entornos locales se pueden interpretar en teorías y pruebas,
  para lo que se usa el comando interpretation.

  Ejemplo: La relación ≤ en los enteros es un orden parcial.

  Los argumentos del comando interpretation son un contexto 
  local, precedido de un identificador (int:) y los términos que 
  sustituyen a los parámetros del contexto local (en este caso, sólo
  hay un parámetro, ⊑.

  Se genera el objetivo
     partial_order op ≤
  que se prueba de forma automática. *}
 
interpretation int: partial_order 
  "op ≤ :: int ⇒ int ⇒ bool"  
by unfold_locales auto

text {* El efecto de la interpretación es que las instancias de
  todas las conclusiones del contexto local son válidas en la teoría
  actual, con los nombres incluyendo la etiqueta como prefijo. *}

thm int.trans

text {* El prefijo int también se le aplica a las definiciones y 
  teoremas. Por ejemplo, *}

thm int.less_def
thm int.less_le_trans

end

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