312 reasoning about a well-formedness predicate. |
312 reasoning about a well-formedness predicate. |
313 |
313 |
314 The problem with introducing a new type in Isabelle/HOL is that in order to |
314 The problem with introducing a new type in Isabelle/HOL is that in order to |
315 be useful, a reasoning infrastructure needs to be ``lifted'' from the |
315 be useful, a reasoning infrastructure needs to be ``lifted'' from the |
316 underlying subset to the new type. This is usually a tricky and arduous |
316 underlying subset to the new type. This is usually a tricky and arduous |
317 task. To ease it, we re-implemented in Isabelle/HOL \cite{KaliszykUrban11} the quotient package |
317 task. To ease it, we re-implemented in Isabelle/HOL \cite{KaliszykUrban11} |
318 described by Homeier \cite{Homeier05} for the HOL4 system. This package |
318 the quotient package described by Homeier \cite{Homeier05} for the HOL4 |
319 allows us to lift definitions and theorems involving raw terms to |
319 system. This package allows us to lift definitions and theorems involving |
320 definitions and theorems involving alpha-equated terms. For example if we |
320 raw terms to definitions and theorems involving alpha-equated terms. For |
321 define the free-variable function over raw lambda-terms |
321 example if we define the free-variable function over raw lambda-terms |
322 |
322 |
323 \begin{center} |
323 \[ |
324 @{text "fv(x) \<equiv> {x}"}\\ |
324 \mbox{\begin{tabular}{l@ {\hspace{1mm}}r@ {\hspace{1mm}}l} |
325 @{text "fv(t\<^isub>1 t\<^isub>2) \<equiv> fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\hspace{8mm} |
325 @{text "fv(x)"} & @{text "\<equiv>"} & @{text "{x}"}\\ |
326 @{text "fv(\<lambda>x.t) \<equiv> fv(t) - {x}"} |
326 @{text "fv(t\<^isub>1 t\<^isub>2)"} & @{text "\<equiv>"} & @{text "fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\\ |
327 \end{center} |
327 @{text "fv(\<lambda>x.t)"} & @{text "\<equiv>"} & @{text "fv(t) - {x}"} |
|
328 \end{tabular}} |
|
329 \]\smallskip |
328 |
330 |
329 \noindent |
331 \noindent |
330 then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\<alpha>"} |
332 then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\<alpha>"} |
331 operating on quotients, or alpha-equivalence classes of lambda-terms. This |
333 operating on quotients, or alpha-equivalence classes of lambda-terms. This |
332 lifted function is characterised by the equations |
334 lifted function is characterised by the equations |
333 |
335 |
334 \begin{center} |
336 \[ |
335 @{text "fv\<^sup>\<alpha>(x) = {x}"}\hspace{8mm} |
337 \mbox{\begin{tabular}{l@ {\hspace{1mm}}r@ {\hspace{1mm}}l} |
336 @{text "fv\<^sup>\<alpha>(t\<^isub>1 t\<^isub>2) = fv\<^sup>\<alpha>(t\<^isub>1) \<union> fv\<^sup>\<alpha>(t\<^isub>2)"}\hspace{8mm} |
338 @{text "fv\<^sup>\<alpha>(x)"} & @{text "="} & @{text "{x}"}\\ |
337 @{text "fv\<^sup>\<alpha>(\<lambda>x.t) = fv\<^sup>\<alpha>(t) - {x}"} |
339 @{text "fv\<^sup>\<alpha>(t\<^isub>1 t\<^isub>2)"} & @{text "="} & @{text "fv\<^sup>\<alpha>(t\<^isub>1) \<union> fv\<^sup>\<alpha>(t\<^isub>2)"}\\ |
338 \end{center} |
340 @{text "fv\<^sup>\<alpha>(\<lambda>x.t)"} & @{text "="} & @{text "fv\<^sup>\<alpha>(t) - {x}"} |
|
341 \end{tabular}} |
|
342 \]\smallskip |
339 |
343 |
340 \noindent |
344 \noindent |
341 (Note that this means also the term-constructors for variables, applications |
345 (Note that this means also the term-constructors for variables, applications |
342 and lambda are lifted to the quotient level.) This construction, of course, |
346 and lambda are lifted to the quotient level.) This construction, of course, |
343 only works if alpha-equivalence is indeed an equivalence relation, and the |
347 only works if alpha-equivalence is indeed an equivalence relation, and the |