# HG changeset patch # User Christian Urban # Date 1313567017 -7200 # Node ID 5d145fe77ec1c38ee2740bf5ac81a9cc5564ce3f # Parent 5df574281b69d1cc1ae2cd3dd1858e80358b7ce1 a little tuning on the paper diff -r 5df574281b69 -r 5d145fe77ec1 LMCS-Paper/Paper.thy --- a/LMCS-Paper/Paper.thy Tue Aug 16 17:48:09 2011 +0200 +++ b/LMCS-Paper/Paper.thy Wed Aug 17 09:43:37 2011 +0200 @@ -314,28 +314,32 @@ The problem with introducing a new type in Isabelle/HOL is that in order to be useful, a reasoning infrastructure needs to be ``lifted'' from the underlying subset to the new type. This is usually a tricky and arduous - task. To ease it, we re-implemented in Isabelle/HOL \cite{KaliszykUrban11} the quotient package - described by Homeier \cite{Homeier05} for the HOL4 system. This package - allows us to lift definitions and theorems involving raw terms to - definitions and theorems involving alpha-equated terms. For example if we - define the free-variable function over raw lambda-terms + task. To ease it, we re-implemented in Isabelle/HOL \cite{KaliszykUrban11} + the quotient package described by Homeier \cite{Homeier05} for the HOL4 + system. This package allows us to lift definitions and theorems involving + raw terms to definitions and theorems involving alpha-equated terms. For + example if we define the free-variable function over raw lambda-terms - \begin{center} - @{text "fv(x) \ {x}"}\\ - @{text "fv(t\<^isub>1 t\<^isub>2) \ fv(t\<^isub>1) \ fv(t\<^isub>2)"}\hspace{8mm} - @{text "fv(\x.t) \ fv(t) - {x}"} - \end{center} + \[ + \mbox{\begin{tabular}{l@ {\hspace{1mm}}r@ {\hspace{1mm}}l} + @{text "fv(x)"} & @{text "\"} & @{text "{x}"}\\ + @{text "fv(t\<^isub>1 t\<^isub>2)"} & @{text "\"} & @{text "fv(t\<^isub>1) \ fv(t\<^isub>2)"}\\ + @{text "fv(\x.t)"} & @{text "\"} & @{text "fv(t) - {x}"} + \end{tabular}} + \]\smallskip \noindent then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\"} operating on quotients, or alpha-equivalence classes of lambda-terms. This lifted function is characterised by the equations - \begin{center} - @{text "fv\<^sup>\(x) = {x}"}\hspace{8mm} - @{text "fv\<^sup>\(t\<^isub>1 t\<^isub>2) = fv\<^sup>\(t\<^isub>1) \ fv\<^sup>\(t\<^isub>2)"}\hspace{8mm} - @{text "fv\<^sup>\(\x.t) = fv\<^sup>\(t) - {x}"} - \end{center} + \[ + \mbox{\begin{tabular}{l@ {\hspace{1mm}}r@ {\hspace{1mm}}l} + @{text "fv\<^sup>\(x)"} & @{text "="} & @{text "{x}"}\\ + @{text "fv\<^sup>\(t\<^isub>1 t\<^isub>2)"} & @{text "="} & @{text "fv\<^sup>\(t\<^isub>1) \ fv\<^sup>\(t\<^isub>2)"}\\ + @{text "fv\<^sup>\(\x.t)"} & @{text "="} & @{text "fv\<^sup>\(t) - {x}"} + \end{tabular}} + \]\smallskip \noindent (Note that this means also the term-constructors for variables, applications