Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: setoid_test.v   Sprache: Coq

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.1 Sekunden  (vorverarbeitet)  ¤





Download des
Quellennavigators
Download des
sprechenden Kalenders

Eigene Datei ansehen




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.


Bot Zugriff



                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik