SSL Height.thy Interaktion und
PortierbarkeitIsabelle

theory Height
  imports "HOL-Nominal.Nominal"
begin

text \<open>
  A small problem suggested by D. Wang. It shows how
  the height of a lambda-terms behaves under substitution.
\<close>

atom_decl name

nominal_datatype lam =
    Var "name"
  | App "lam" "lam"
  | Lam "\name\lam" (\Lam [_]._\ [100,100] 100)

text \<open>Definition of the height-function on lambda-terms.\<close>

nominal_primrec
  height :: "lam \ int"
where
  "height (Var x) = 1"
| "height (App t1 t2) = (max (height t1) (height t2)) + 1"
| "height (Lam [a].t) = (height t) + 1"
  apply(finite_guess add: perm_int_def)+
  apply(rule TrueI)+
  apply(simp add: fresh_int)
  apply(fresh_guess add: perm_int_def)+
  done

text \<open>Definition of capture-avoiding substitution.\<close>

nominal_primrec
  subst :: "lam \ name \ lam \ lam" (\_[_::=_]\ [100,100,100] 100)
where
  "(Var x)[y::=t'] = (if x=y then t' else (Var x))"
| "(App t1 t2)[y::=t'] = App (t1[y::=t']) (t2[y::=t'])"
| "\x\y; x\t'\ \ (Lam [x].t)[y::=t'] = Lam [x].(t[y::=t'])"
apply(finite_guess)+
apply(rule TrueI)+
apply(simp add: abs_fresh)
apply(fresh_guess)+
done

text\<open>The next lemma is needed in the Var-case of the theorem below.\<close>

lemma height_ge_one:
  shows "1 \ (height e)"
by (nominal_induct e rule: lam.strong_induct) (simp_all)

text \<open>
  Unlike the proplem suggested by Wang, however, the
  theorem is here formulated entirely by using functions.
\<close>

theorem height_subst:
  shows "height (e[x::=e']) \ ((height e) - 1) + (height e')"
proof (nominal_induct e avoiding: x e' rule: lam.strong_induct)
  case (Var y)
  have "1 \ height e'" by (rule height_ge_one)
  then show "height (Var y[x::=e']) \ height (Var y) - 1 + height e'" by simp
next
  case (Lam y e1)
  hence ih: "height (e1[x::=e']) \ ((height e1) - 1) + (height e')" by simp
  moreover
  have vc: "y\x" "y\e'" by fact+ (* usual variable convention *)
  ultimately show "height ((Lam [y].e1)[x::=e']) \ height (Lam [y].e1) - 1 + height e'" by simp
next
  case (App e1 e2)
  hence ih1: "height (e1[x::=e']) \ ((height e1) - 1) + (height e')"
    and ih2: "height (e2[x::=e']) \ ((height e2) - 1) + (height e')" by simp_all
  then show "height ((App e1 e2)[x::=e']) \ height (App e1 e2) - 1 + height e'" by simp
qed

end

quality100%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.1Bemerkung: Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.

SSL Height.thy Interaktion und PortierbarkeitIsabelle

Haftungshinweis

Bemerkung:

SSL Height.thy Interaktion und
PortierbarkeitIsabelle