560 |
560 |
561 \begin{property}\label{supppermeq} |
561 \begin{property}\label{supppermeq} |
562 @{thm[mode=IfThen] supp_perm_eq[no_vars]} |
562 @{thm[mode=IfThen] supp_perm_eq[no_vars]} |
563 \end{property} |
563 \end{property} |
564 |
564 |
565 \begin{property} |
565 \begin{property}\label{avoiding} |
566 For a finite set @{text as} and a finitely supported @{text x} with |
566 For a finite set @{text as} and a finitely supported @{text x} with |
567 @{term "as \<sharp>* x"} and also a finitely supported @{text c}, there |
567 @{term "as \<sharp>* x"} and also a finitely supported @{text c}, there |
568 exists a permutation @{text p} such that @{term "(p \<bullet> as) \<sharp>* c"} and |
568 exists a permutation @{text p} such that @{term "(p \<bullet> as) \<sharp>* c"} and |
569 @{term "supp x \<sharp>* p"}. |
569 @{term "supp x \<sharp>* p"}. |
570 \end{property} |
570 \end{property} |
1628 and obtain @{text "\<bullet>bn\<^isup>\<alpha>"}. A property that shows that this definition is correct is: |
1628 and obtain @{text "\<bullet>bn\<^isup>\<alpha>"}. A property that shows that this definition is correct is: |
1629 |
1629 |
1630 %% We could get this from ExLet/perm_bn lemma. |
1630 %% We could get this from ExLet/perm_bn lemma. |
1631 \begin{lemma} For every bn function @{text "bn\<^isup>\<alpha>\<^isub>i"}, |
1631 \begin{lemma} For every bn function @{text "bn\<^isup>\<alpha>\<^isub>i"}, |
1632 \begin{eqnarray} |
1632 \begin{eqnarray} |
1633 @{term "\<pi> \<bullet> bn\<^isup>\<alpha>\<^isub>i x"} & = & @{term "bn\<^isup>\<alpha>\<^isub>i(p \<bullet>bn\<^isup>\<alpha>\<^isub>i x)"}\\ |
1633 @{text "\<pi> \<bullet> bn\<^isup>\<alpha>\<^isub>i x"} & = & @{text "bn\<^isup>\<alpha>\<^isub>i(p \<bullet>bn\<^isup>\<alpha>\<^isub>i x)"}\\ |
1634 @{term "fv_bn\<^isup>\<alpha>\<^isub>i x"} & = & @{term "fv_bn\<^isup>\<alpha>\<^isub>i(p \<bullet>bn\<^isup>\<alpha>\<^isub>i x)"} |
1634 @{text "fv_bn\<^isup>\<alpha>\<^isub>i x"} & = & @{text "fv_bn\<^isup>\<alpha>\<^isub>i(p \<bullet>bn\<^isup>\<alpha>\<^isub>i x)"} |
1635 \end{eqnarray} |
1635 \end{eqnarray} |
1636 \end{lemma} |
1636 \end{lemma} |
1637 \begin{proof} By induction on the lifted type it follows from the definitions of |
1637 \begin{proof} By induction on the lifted type it follows from the definitions of |
1638 permutations on the lifted type and the lifted defining equations of @{text "\<bullet>bn"} |
1638 permutations on the lifted type and the lifted defining equations of @{text "\<bullet>bn"} |
1639 and @{text "fv_bn"}. |
1639 and @{text "fv_bn"}. |
1640 \end{proof} |
1640 \end{proof} |
|
1641 |
|
1642 *} |
|
1643 |
|
1644 section {* Strong Induction Principles *} |
|
1645 |
|
1646 text {* |
|
1647 With the help of @{text "\<bullet>bn"} functions defined in the previous section |
|
1648 we can show that binders can be substituted in term constructors. We show |
|
1649 this only for the specification from Figure~\ref{nominalcorehas}. The only |
|
1650 constructor with a complicated binding structure is @{text "ACons"}. For this |
|
1651 constructor we prove: |
|
1652 \begin{eqnarray} |
|
1653 \lefteqn{@{text "supp (Abs_lst (bv pat) trm) \<sharp>* \<pi> \<Longrightarrow>"}} \nonumber \\ |
|
1654 & & @{text "ACons pat trm al = ACons (\<pi> \<bullet>bv pat) (\<pi> \<bullet> trm) al"} \nonumber |
|
1655 \end{eqnarray} |
|
1656 |
|
1657 With the Property~\ref{avoiding} we can prove a strong induction principle |
|
1658 which we show again only for the Core Haskell example: |
|
1659 |
|
1660 |
1641 |
1661 |
1642 *} |
1662 *} |
1643 |
1663 |
1644 text {* |
1664 text {* |
1645 |
1665 |
1713 one obtains automatically a reasoning infrastructure for Core-Haskell. |
1733 one obtains automatically a reasoning infrastructure for Core-Haskell. |
1714 \label{nominalcorehas}} |
1734 \label{nominalcorehas}} |
1715 \end{figure} |
1735 \end{figure} |
1716 *} |
1736 *} |
1717 |
1737 |
1718 |
|
1719 (* @{thm "ACons_subst[no_vars]"}*) |
|
1720 |
|
1721 section {* Strong Induction Principles *} |
|
1722 |
|
1723 section {* Related Work *} |
1738 section {* Related Work *} |
1724 |
1739 |
1725 text {* |
1740 text {* |
1726 To our knowledge the earliest usage of general binders in a theorem prover |
1741 To our knowledge the earliest usage of general binders in a theorem prover |
1727 setting is in \cite{NaraschewskiNipkow99}, which describes a formalisation |
1742 setting is in \cite{NaraschewskiNipkow99}, which describes a formalisation |