Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Height.thy Sprache: Isabelle

Original von: Isabelle^©

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

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.