1574 Corecursive functions over codatatypes can be specified using @{command |
1559 Corecursive functions over codatatypes can be specified using @{command |
1575 primcorec}, which supports primitive corecursion, or using the more general |
1560 primcorec}, which supports primitive corecursion, or using the more general |
1576 \keyw{partial\_function} command. Here, the focus is on @{command primcorec}. |
1561 \keyw{partial\_function} command. Here, the focus is on @{command primcorec}. |
1577 More examples can be found in the directory \verb|~~/src/HOL/BNF/Examples|. |
1562 More examples can be found in the directory \verb|~~/src/HOL/BNF/Examples|. |
1578 |
1563 |
1579 \begin{framed} |
|
1580 \noindent |
|
1581 \textbf{Warning:}\enskip The @{command primcorec} command is under heavy |
|
1582 development. Much of the functionality described here is vaporware. Until the |
|
1583 command is fully in place, it is recommended to define corecursive functions |
|
1584 directly using the generated @{text t_unfold} or @{text t_corec} combinators. |
|
1585 \end{framed} |
|
1586 |
|
1587 %%% TODO: partial_function? E.g. for defining tail recursive function on lazy |
|
1588 %%% lists (cf. terminal0 in TLList.thy) |
|
1589 *} |
|
1590 |
|
1591 |
|
1592 subsection {* Introductory Examples |
|
1593 \label{ssec:primcorec-introductory-examples} *} |
|
1594 |
|
1595 text {* |
|
1596 Primitive corecursion is illustrated through concrete examples based on the |
|
1597 codatatypes defined in Section~\ref{ssec:codatatype-introductory-examples}. More |
|
1598 examples can be found in the directory \verb|~~/src/HOL/BNF/Examples|. |
|
1599 *} |
|
1600 |
|
1601 |
|
1602 subsubsection {* Simple Corecursion |
|
1603 \label{sssec:primcorec-simple-corecursion} *} |
|
1604 |
|
1605 text {* |
|
1606 Whereas recursive functions consume datatypes one constructor at a time, |
1564 Whereas recursive functions consume datatypes one constructor at a time, |
1607 corecursive functions construct codatatypes one constructor at a time. |
1565 corecursive functions construct codatatypes one constructor at a time. |
1608 Reflecting a lack of agreement among proponents of coalgebraic methods, Isabelle |
1566 Reflecting a lack of agreement among proponents of coalgebraic methods, Isabelle |
1609 supports two competing syntaxes for specifying a function $f$: |
1567 supports two competing syntaxes for specifying a function $f$: |
1610 |
1568 |
1611 \begin{itemize} |
1569 \begin{itemize} |
|
1570 \setlength{\itemsep}{0pt} |
|
1571 |
1612 \abovedisplayskip=.5\abovedisplayskip |
1572 \abovedisplayskip=.5\abovedisplayskip |
1613 \belowdisplayskip=.5\belowdisplayskip |
1573 \belowdisplayskip=.5\belowdisplayskip |
1614 |
|
1615 \item The \emph{constructor view} specifies $f$ by equations of the form |
|
1616 \[@{text "f x\<^sub>1 \<dots> x\<^sub>n = \<dots>"}\] |
|
1617 Lazy functional programming languages such as Haskell support this style. |
|
1618 |
1574 |
1619 \item The \emph{destructor view} specifies $f$ by implications of the form |
1575 \item The \emph{destructor view} specifies $f$ by implications of the form |
1620 \[@{text "\<dots> \<Longrightarrow> is_C\<^sub>j (f x\<^sub>1 \<dots> x\<^sub>n)"}\] and |
1576 \[@{text "\<dots> \<Longrightarrow> is_C\<^sub>j (f x\<^sub>1 \<dots> x\<^sub>n)"}\] and |
1621 equations of the form |
1577 equations of the form |
1622 \[@{text "un_C\<^sub>ji (f x\<^sub>1 \<dots> x\<^sub>n) = \<dots>"}\] |
1578 \[@{text "un_C\<^sub>ji (f x\<^sub>1 \<dots> x\<^sub>n) = \<dots>"}\] |
1623 This style is popular in the coalgebraic literature. |
1579 This style is popular in the coalgebraic literature. |
|
1580 |
|
1581 \item The \emph{constructor view} specifies $f$ by equations of the form |
|
1582 \[@{text "\<dots> \<Longrightarrow> f x\<^sub>1 \<dots> x\<^sub>n = C \<dots>"}\] |
|
1583 |
|
1584 \item The \emph{code view} specifies $f$ by a single equation of the form |
|
1585 \[@{text "f x\<^sub>1 \<dots> x\<^sub>n = \<dots>"}\] |
|
1586 with restrictions on the format of the right-hand side. Lazy functional |
|
1587 programming languages such as Haskell support a generalized version of this |
|
1588 style. |
1624 \end{itemize} |
1589 \end{itemize} |
1625 |
1590 |
1626 \noindent |
1591 \noindent |
1627 Both styles are available as input syntax to @{command primcorec}. Whichever |
1592 The constructor and code views coincide for functions that construct values |
1628 syntax is chosen, characteristic theorems following both styles are generated. |
1593 using repeated applications of a single constructor. |
1629 |
1594 |
1630 In the constructor view, corecursive calls are allowed on the right-hand side |
1595 \noindent |
1631 as long as they occur under a constructor. The constructor itself normally |
1596 All three styles are available as input syntax to @{command primcorec}. |
1632 appears directly to the right of the equal sign: |
1597 Whichever syntax is chosen, characteristic theorems for all three styles are |
|
1598 generated. |
|
1599 |
|
1600 \begin{framed} |
|
1601 \noindent |
|
1602 \textbf{Warning:}\enskip The @{command primcorec} command is under heavy |
|
1603 development. Some of the functionality described here is vaporware. An |
|
1604 alternative is to define corecursive functions directly using the generated |
|
1605 @{text t_unfold} or @{text t_corec} combinators. |
|
1606 \end{framed} |
|
1607 |
|
1608 %%% TODO: partial_function? E.g. for defining tail recursive function on lazy |
|
1609 %%% lists (cf. terminal0 in TLList.thy) |
|
1610 *} |
|
1611 |
|
1612 |
|
1613 subsection {* Introductory Examples |
|
1614 \label{ssec:primcorec-introductory-examples} *} |
|
1615 |
|
1616 text {* |
|
1617 Primitive corecursion is illustrated through concrete examples based on the |
|
1618 codatatypes defined in Section~\ref{ssec:codatatype-introductory-examples}. More |
|
1619 examples can be found in the directory \verb|~~/src/HOL/BNF/Examples|. The code |
|
1620 view is favored in the examples below. Sections |
|
1621 \ref{ssec:primrec-constructor-view} and \ref{ssec:primrec-destructor-view} |
|
1622 present the same examples expressed using the constructor and destructor views. |
|
1623 *} |
|
1624 |
|
1625 (*<*) |
|
1626 locale code_view |
|
1627 begin |
|
1628 (*>*) |
|
1629 |
|
1630 subsubsection {* Simple Corecursion |
|
1631 \label{sssec:primcorec-simple-corecursion} *} |
|
1632 |
|
1633 text {* |
|
1634 In the code view, corecursive calls are allowed on the right-hand side as long |
|
1635 as they occur under a constructor, which itself appears either directly to the |
|
1636 right of the equal sign or in a conditional expression: |
1633 *} |
1637 *} |
1634 |
1638 |
1635 primcorec literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where |
1639 primcorec literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where |
1636 "literate f x = LCons x (literate f (f x))" |
1640 "literate f x = LCons x (literate f (f x))" |
1637 . |
1641 . |
1643 . |
1647 . |
1644 |
1648 |
1645 text {* |
1649 text {* |
1646 \noindent |
1650 \noindent |
1647 The constructor ensures that progress is made---i.e., the function is |
1651 The constructor ensures that progress is made---i.e., the function is |
1648 \emph{productive}. The above function computes the infinite lazy list or stream |
1652 \emph{productive}. The above functions compute the infinite lazy list or stream |
1649 @{text "[x, f x, f (f x), \<dots>]"}. Productivity guarantees that prefixes |
1653 @{text "[x, f x, f (f x), \<dots>]"}. Productivity guarantees that prefixes |
1650 @{text "[x, f x, f (f x), \<dots>, (f ^^ k) x]"} of arbitrary finite length |
1654 @{text "[x, f x, f (f x), \<dots>, (f ^^ k) x]"} of arbitrary finite length |
1651 @{text k} can be computed by unfolding the equation a finite number of times. |
1655 @{text k} can be computed by unfolding the code equation a finite number of |
1652 The period (\keyw{.}) at the end of the commands discharge the zero proof |
1656 times. The period (\keyw{.}) at the end of the commands discharge the zero proof |
1653 obligations. |
1657 obligations. |
1654 |
|
1655 These two functions can be specified as follows in the destructor view: |
|
1656 *} |
|
1657 |
|
1658 (*<*) |
|
1659 locale dummy_dest_view |
|
1660 begin |
|
1661 (*>*) |
|
1662 primcorec literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where |
|
1663 "\<not> lnull (literate _ x)" | |
|
1664 "lhd (literate _ x) = x" | |
|
1665 "ltl (literate f x) = literate f (f x)" |
|
1666 . |
|
1667 |
|
1668 text {* \blankline *} |
|
1669 |
|
1670 primcorec siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where |
|
1671 "shd (siterate _ x) = x" | |
|
1672 "stl (siterate f x) = siterate f (f x)" |
|
1673 . |
|
1674 (*<*) |
|
1675 end |
|
1676 (*>*) |
|
1677 |
|
1678 text {* |
|
1679 \noindent |
|
1680 The first formula in the @{const literate} specification indicates which |
|
1681 constructor to choose. For @{const siterate}, no such formula is necessary, |
|
1682 since the type has only one constructor. The last two formulas are equations |
|
1683 specifying the value of the result for the relevant selectors. Corecursive calls |
|
1684 are allowed to appear directly to the right of the equal sign. Their arguments |
|
1685 are unrestricted. |
|
1686 |
1658 |
1687 Corecursive functions necessarily construct codatatype values. Nothing prevents |
1659 Corecursive functions necessarily construct codatatype values. Nothing prevents |
1688 them from also consuming such values. The following function drops ever second |
1660 them from also consuming such values. The following function drops ever second |
1689 element in a stream: |
1661 element in a stream: |
1690 *} |
1662 *} |
1784 Choice (random_process (every_snd s) (f \<circ> f) (f n)) |
1703 Choice (random_process (every_snd s) (f \<circ> f) (f n)) |
1785 (random_process (every_snd (stl s)) (f \<circ> f) (f (f n))))" |
1704 (random_process (every_snd (stl s)) (f \<circ> f) (f (f n))))" |
1786 |
1705 |
1787 text {* |
1706 text {* |
1788 \noindent |
1707 \noindent |
1789 The main disadvantage of the constructor view in this case is that the |
1708 The main disadvantage of the code view is that the conditions are tested |
1790 conditions are tested sequentially. This is visible in the generated theorems. |
1709 sequentially. This is visible in the generated theorems. The constructor and |
1791 In this respect, the destructor view is more elegant: |
1710 destructor views offer non-sequential alternatives. |
1792 *} |
1711 *} |
|
1712 |
|
1713 |
|
1714 subsubsection {* Mutual Corecursion |
|
1715 \label{sssec:primcorec-mutual-corecursion} *} |
|
1716 |
|
1717 text {* |
|
1718 The syntax for mutually corecursive functions over mutually corecursive |
|
1719 datatypes is unsurprising: |
|
1720 *} |
|
1721 |
|
1722 primcorec |
|
1723 even_infty :: even_enat and |
|
1724 odd_infty :: odd_enat |
|
1725 where |
|
1726 "even_infty = Even_ESuc odd_infty" | |
|
1727 "odd_infty = Odd_ESuc even_infty" |
|
1728 . |
|
1729 |
|
1730 |
|
1731 subsubsection {* Nested Corecursion |
|
1732 \label{sssec:primcorec-nested-corecursion} *} |
|
1733 |
|
1734 text {* |
|
1735 The next pair of examples generalize the @{const literate} and @{const siterate} |
|
1736 functions (Section~\ref{sssec:primcorec-nested-corecursion}) to possibly |
|
1737 infinite trees in which subnodes are organized either as a lazy list (@{text |
|
1738 tree\<^sub>i\<^sub>i}) or as a finite set (@{text tree\<^sub>i\<^sub>s}): |
|
1739 *} |
|
1740 |
|
1741 primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where |
|
1742 "iterate\<^sub>i\<^sub>i f x = Node\<^sub>i\<^sub>i x (lmap (iterate\<^sub>i\<^sub>i f) (f x))" |
|
1743 . |
|
1744 |
|
1745 text {* \blankline *} |
|
1746 |
|
1747 primcorec iterate\<^sub>i\<^sub>s :: "('a \<Rightarrow> 'a fset) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>s" where |
|
1748 "iterate\<^sub>i\<^sub>s f x = Node\<^sub>i\<^sub>s x (fmap (iterate\<^sub>i\<^sub>s f) (f x))" |
|
1749 . |
|
1750 |
|
1751 text {* |
|
1752 Deterministic finite automata (DFAs) are usually defined as 5-tuples |
|
1753 @{text "(Q, \<Sigma>, \<delta>, q\<^sub>0, F)"}, where @{text Q} is a finite set of states, |
|
1754 @{text \<Sigma>} is a finite alphabet, @{text \<delta>} is a transition function, @{text q\<^sub>0} |
|
1755 is an initial state, and @{text F} is a set of final states. The following |
|
1756 function translates a DFA into a @{type state_machine}: |
|
1757 *} |
|
1758 |
|
1759 primcorec of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a state_machine" where |
|
1760 "of_dfa \<delta> F q = State_Machine (q \<in> F) (of_dfa \<delta> F o \<delta> q)" |
|
1761 . |
|
1762 |
|
1763 |
|
1764 subsubsection {* Nested-as-Mutual Corecursion |
|
1765 \label{sssec:primcorec-nested-as-mutual-corecursion} *} |
|
1766 |
|
1767 text {* |
|
1768 Just as it is possible to recurse over nested recursive datatypes as if they |
|
1769 were mutually recursive |
|
1770 (Section~\ref{sssec:primrec-nested-as-mutual-recursion}), it is possible to |
|
1771 corecurse over nested codatatypes as if they were mutually corecursive. For |
|
1772 example: |
|
1773 *} |
|
1774 |
|
1775 primcorec_notyet |
|
1776 iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" and |
|
1777 iterates\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a llist \<Rightarrow> 'a tree\<^sub>i\<^sub>i llist" |
|
1778 where |
|
1779 "iterate\<^sub>i\<^sub>i f x = Node\<^sub>i\<^sub>i x (iterates\<^sub>i\<^sub>i f (f x))" | |
|
1780 "iterates\<^sub>i\<^sub>i f xs = |
|
1781 (case xs of |
|
1782 LNil \<Rightarrow> LNil |
|
1783 | LCons x xs' \<Rightarrow> LCons (iterate\<^sub>i\<^sub>i f x) (iterates\<^sub>i\<^sub>i f xs'))" |
1793 |
1784 |
1794 (*<*) |
1785 (*<*) |
1795 context dummy_dest_view |
1786 end |
|
1787 (*>*) |
|
1788 |
|
1789 |
|
1790 subsubsection {* Constructor View |
|
1791 \label{ssec:primrec-constructor-view} *} |
|
1792 |
|
1793 (*<*) |
|
1794 locale ctr_view = code_view |
1796 begin |
1795 begin |
1797 (*>*) |
1796 (*>*) |
|
1797 |
|
1798 text {* |
|
1799 For the next example, the constructor view is slighlty more involved than the |
|
1800 code equation: |
|
1801 *} |
|
1802 |
|
1803 primcorec lappend :: "'a llist \<Rightarrow> 'a llist \<Rightarrow> 'a llist" where |
|
1804 "lnull xs \<Longrightarrow> lnull ys \<Longrightarrow> lappend xs ys = LNil" | |
|
1805 "_ \<Longrightarrow> lappend xs ys = LCons (lhd (if lnull xs then ys else xs)) |
|
1806 (if xs = LNil then ltl ys else lappend (ltl xs) ys)" |
|
1807 . |
|
1808 |
|
1809 text {* |
|
1810 \noindent |
|
1811 Recall the code view version presented in |
|
1812 Section~\ref{sssec:primcorec-simple-corecursion}. |
|
1813 % TODO: \[{thm code_view.lappend.code}\] |
|
1814 The constructor view requires us to analyze the second argument (@{term ys}). |
|
1815 The code equation generated for the constructor view also suffers from this |
|
1816 complication. |
|
1817 % TODO: \[{thm lappend.code}\] |
|
1818 *} |
|
1819 |
|
1820 primcorec_notyet random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process" where |
|
1821 "n mod 4 = 0 \<Longrightarrow> random_process s f n = Fail" | |
|
1822 "n mod 4 = 1 \<Longrightarrow> random_process s f n = Skip (random_process s f (f n))" | |
|
1823 "n mod 4 = 2 \<Longrightarrow> random_process s f n = |
|
1824 Action (shd s) (random_process (stl s) f (f n))" | |
|
1825 "n mod 4 = 3 \<Longrightarrow> random_process s f n = |
|
1826 Choice (random_process (every_snd s) f (f n)) |
|
1827 (random_process (every_snd (stl s)) f (f n))" |
|
1828 (* FIXME: by auto *) |
|
1829 |
|
1830 (*<*) |
|
1831 end |
|
1832 (*>*) |
|
1833 |
|
1834 |
|
1835 subsubsection {* Destructor View |
|
1836 \label{ssec:primrec-constructor-view} *} |
|
1837 |
|
1838 text {* |
|
1839 The destructor view is in many respects dual to the constructor view. Conditions |
|
1840 determine which constructor to choose, and these conditions are interpreted |
|
1841 sequentially or not depending on the @{text "sequential"} option. |
|
1842 |
|
1843 Consider the following examples: |
|
1844 *} |
|
1845 |
|
1846 (*<*) |
|
1847 locale dest_view |
|
1848 begin |
|
1849 (*>*) |
|
1850 |
|
1851 primcorec literate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a llist" where |
|
1852 "\<not> lnull (literate _ x)" | |
|
1853 "lhd (literate _ x) = x" | |
|
1854 "ltl (literate f x) = literate f (f x)" |
|
1855 . |
|
1856 |
|
1857 primcorec siterate :: "('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a stream" where |
|
1858 "shd (siterate _ x) = x" | |
|
1859 "stl (siterate f x) = siterate f (f x)" |
|
1860 . |
|
1861 |
|
1862 primcorec every_snd :: "'a stream \<Rightarrow> 'a stream" where |
|
1863 "shd (every_snd s) = shd s" | |
|
1864 "stl (every_snd s) = stl (stl s)" |
|
1865 . |
|
1866 |
|
1867 text {* |
|
1868 \noindent |
|
1869 The first formula in the @{const literate} specification indicates which |
|
1870 constructor to choose. For @{const siterate} and @{const every_snd}, no such |
|
1871 formula is necessary, since the type has only one constructor. The last two |
|
1872 formulas are equations specifying the value of the result for the relevant |
|
1873 selectors. Corecursive calls appear directly to the right of the equal sign. |
|
1874 Their arguments are unrestricted. |
|
1875 *} |
|
1876 |
1798 primcorec_notyet random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process" where |
1877 primcorec_notyet random_process :: "'a stream \<Rightarrow> (int \<Rightarrow> int) \<Rightarrow> int \<Rightarrow> 'a process" where |
1799 "n mod 4 = 0 \<Longrightarrow> is_Fail (random_process s f n)" | |
1878 "n mod 4 = 0 \<Longrightarrow> is_Fail (random_process s f n)" | |
1800 "n mod 4 = 1 \<Longrightarrow> is_Skip (random_process s f n)" | |
1879 "n mod 4 = 1 \<Longrightarrow> is_Skip (random_process s f n)" | |
1801 "n mod 4 = 2 \<Longrightarrow> is_Action (random_process s f n)" | |
1880 "n mod 4 = 2 \<Longrightarrow> is_Action (random_process s f n)" | |
1802 "n mod 4 = 3 \<Longrightarrow> is_Choice (random_process s f n)" | |
1881 "n mod 4 = 3 \<Longrightarrow> is_Choice (random_process s f n)" | |
1803 "cont (random_process s f n) = random_process s f (f n)" (* of Skip FIXME *) | |
1882 "cont (random_process s f n) = random_process s f (f n)" (* of Skip FIXME *) | |
1804 "prefix (random_process s f n) = shd s" | |
1883 "prefix (random_process s f n) = shd s" | |
1805 "cont (random_process s f n) = random_process (stl s) f (f n)" (* of Action FIXME *) | |
1884 "cont (random_process s f n) = random_process (stl s) f (f n)" (* of Action FIXME *) | |
1806 "left (random_process s f n) = random_process (every_snd s) f (f n)" | |
1885 "left (random_process s f n) = random_process (every_snd s) f (f n)" | |
1807 "right (random_process s f n) = random_process (every_snd (stl s)) f (f n)" |
1886 "right (random_process s f n) = random_process (every_snd (stl s)) f (f n)" |
1808 (* by auto FIXME *) |
1887 (* FIXME: by auto *) |
1809 (*<*) |
1888 |
1810 end |
1889 text {* |
1811 (*>*) |
1890 |
1812 |
1891 *} |
1813 text {* |
1892 |
1814 \noindent |
|
1815 The price to pay for this elegance is that we must discharge exclusivity proof |
|
1816 obligations, one for each pair of conditions |
|
1817 @{term "(n mod 4 = i, n mod 4 = j)"}. If we prefer not to discharge any |
|
1818 obligations, we can specify the option @{text "(sequential)"} after the |
|
1819 @{command primcorec} keyword. This pushes the problem to the users of the |
|
1820 generated properties, as with the constructor view. |
|
1821 *} |
|
1822 |
|
1823 |
|
1824 subsubsection {* Mutual Corecursion |
|
1825 \label{sssec:primcorec-mutual-corecursion} *} |
|
1826 |
|
1827 text {* |
|
1828 The syntax for mutually corecursive functions over mutually corecursive |
|
1829 datatypes is anything but surprising. Following the constructor view: |
|
1830 *} |
|
1831 |
|
1832 primcorec |
|
1833 even_infty :: even_enat and |
|
1834 odd_infty :: odd_enat |
|
1835 where |
|
1836 "even_infty = Even_ESuc odd_infty" | |
|
1837 "odd_infty = Odd_ESuc even_infty" |
|
1838 . |
|
1839 |
|
1840 text {* |
|
1841 And following the destructor view: |
|
1842 *} |
|
1843 |
|
1844 (*<*) |
|
1845 context dummy_dest_view |
|
1846 begin |
|
1847 (*>*) |
|
1848 primcorec |
1893 primcorec |
1849 even_infty :: even_enat and |
1894 even_infty :: even_enat and |
1850 odd_infty :: odd_enat |
1895 odd_infty :: odd_enat |
1851 where |
1896 where |
1852 "\<not> is_Even_EZero even_infty" | |
1897 "\<not> is_Even_EZero even_infty" | |
1853 "un_Even_ESuc even_infty = odd_infty" | |
1898 "un_Even_ESuc even_infty = odd_infty" | |
1854 "un_Odd_ESuc odd_infty = even_infty" |
1899 "un_Odd_ESuc odd_infty = even_infty" |
1855 . |
1900 . |
1856 (*<*) |
1901 |
1857 end |
|
1858 (*>*) |
|
1859 |
|
1860 |
|
1861 subsubsection {* Nested Corecursion |
|
1862 \label{sssec:primcorec-nested-corecursion} *} |
|
1863 |
|
1864 text {* |
|
1865 The next pair of examples generalize the @{const literate} and @{const siterate} |
|
1866 functions (Section~\ref{sssec:primcorec-nested-corecursion}) to possibly |
|
1867 infinite trees in which subnodes are organized either as a lazy list (@{text |
|
1868 tree\<^sub>i\<^sub>i}) or as a finite set (@{text tree\<^sub>i\<^sub>s}): |
|
1869 *} |
|
1870 |
|
1871 primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where |
|
1872 "iterate\<^sub>i\<^sub>i f x = Node\<^sub>i\<^sub>i x (lmap (iterate\<^sub>i\<^sub>i f) (f x))" |
|
1873 . |
|
1874 |
|
1875 text {* \blankline *} |
|
1876 |
|
1877 primcorec iterate\<^sub>i\<^sub>s :: "('a \<Rightarrow> 'a fset) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>s" where |
|
1878 "iterate\<^sub>i\<^sub>s f x = Node\<^sub>i\<^sub>s x (fmap (iterate\<^sub>i\<^sub>s f) (f x))" |
|
1879 . |
|
1880 |
|
1881 text {* |
|
1882 Again, let us not forget our destructor-oriented passengers. Here is the first |
|
1883 example in the destructor view: |
|
1884 *} |
|
1885 |
|
1886 (*<*) |
|
1887 context dummy_dest_view |
|
1888 begin |
|
1889 (*>*) |
|
1890 primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where |
1902 primcorec iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" where |
1891 "lbl\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i f x) = x" | |
1903 "lbl\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i f x) = x" | |
1892 "sub\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i f x) = lmap (iterate\<^sub>i\<^sub>i f) (f x)" |
1904 "sub\<^sub>i\<^sub>i (iterate\<^sub>i\<^sub>i f x) = lmap (iterate\<^sub>i\<^sub>i f) (f x)" |
1893 . |
1905 . |
|
1906 |
1894 (*<*) |
1907 (*<*) |
1895 end |
1908 end |
1896 (*>*) |
1909 (*>*) |
1897 |
1910 |
1898 text {* |
|
1899 Deterministic finite automata (DFAs) are usually defined as 5-tuples |
|
1900 @{text "(Q, \<Sigma>, \<delta>, q\<^sub>0, F)"}, where @{text Q} is a finite set of states, |
|
1901 @{text \<Sigma>} is a finite alphabet, @{text \<delta>} is a transition function, @{text q\<^sub>0} |
|
1902 is an initial state, and @{text F} is a set of final states. The following |
|
1903 function translates a DFA into a @{type state_machine}: |
|
1904 *} |
|
1905 |
|
1906 primcorec of_dfa :: "('q \<Rightarrow> 'a \<Rightarrow> 'q) \<Rightarrow> 'q set \<Rightarrow> 'q \<Rightarrow> 'a state_machine" where |
|
1907 "of_dfa \<delta> F q = State_Machine (q \<in> F) (of_dfa \<delta> F o \<delta> q)" |
|
1908 . |
|
1909 |
|
1910 |
|
1911 subsubsection {* Nested-as-Mutual Corecursion |
|
1912 \label{sssec:primcorec-nested-as-mutual-corecursion} *} |
|
1913 |
|
1914 text {* |
|
1915 Just as it is possible to recurse over nested recursive datatypes as if they |
|
1916 were mutually recursive |
|
1917 (Section~\ref{sssec:primrec-nested-as-mutual-recursion}), it is possible to |
|
1918 corecurse over nested codatatypes as if they were mutually corecursive. For |
|
1919 example: |
|
1920 *} |
|
1921 |
|
1922 (*<*) |
|
1923 locale dummy_iterate |
|
1924 begin |
|
1925 (*>*) |
|
1926 primcorec_notyet |
|
1927 iterate\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>i" and |
|
1928 iterates\<^sub>i\<^sub>i :: "('a \<Rightarrow> 'a llist) \<Rightarrow> 'a llist \<Rightarrow> 'a tree\<^sub>i\<^sub>i llist" |
|
1929 where |
|
1930 "iterate\<^sub>i\<^sub>i f x = Node\<^sub>i\<^sub>i x (iterates\<^sub>i\<^sub>i f (f x))" | |
|
1931 "iterates\<^sub>i\<^sub>i f xs = |
|
1932 (case xs of |
|
1933 LNil \<Rightarrow> LNil |
|
1934 | LCons x xs' \<Rightarrow> LCons (iterate\<^sub>i\<^sub>i f x) (iterates\<^sub>i\<^sub>i f xs'))" |
|
1935 (*<*) |
|
1936 end |
|
1937 (*>*) |
|
1938 |
|
1939 |
|
1940 subsection {* Command Syntax |
1911 subsection {* Command Syntax |
1941 \label{ssec:primcorec-command-syntax} *} |
1912 \label{ssec:primcorec-command-syntax} *} |
1942 |
1913 |
1943 |
1914 |
1944 subsubsection {* \keyw{primcorec} |
1915 subsubsection {* \keyw{primcorec} |