1667 val recursor_eqns : thm list \textrm{equations for the recursor} |
1667 val recursor_eqns : thm list \textrm{equations for the recursor} |
1668 val con_defs : thm list \textrm{definitions of the case operator and constructors} |
1668 val con_defs : thm list \textrm{definitions of the case operator and constructors} |
1669 val free_iffs : thm list \textrm{logical equivalences for proving freeness} |
1669 val free_iffs : thm list \textrm{logical equivalences for proving freeness} |
1670 val free_SEs : thm list \textrm{elimination rules for proving freeness} |
1670 val free_SEs : thm list \textrm{elimination rules for proving freeness} |
1671 val mk_free : string -> thm \textrm{A function for proving freeness theorems} |
1671 val mk_free : string -> thm \textrm{A function for proving freeness theorems} |
1672 val mk_cases : thm list -> string -> thm \textrm{case analysis, see below} |
1672 val mk_cases : string -> thm \textrm{case analysis, see below} |
1673 val defs : thm list \textrm{definitions of operators} |
1673 val defs : thm list \textrm{definitions of operators} |
1674 val bnd_mono : thm list \textrm{monotonicity property} |
1674 val bnd_mono : thm list \textrm{monotonicity property} |
1675 val dom_subset : thm list \textrm{inclusion in `bounding set'} |
1675 val dom_subset : thm list \textrm{inclusion in `bounding set'} |
1676 \end{ttbox} |
1676 \end{ttbox} |
1677 Furthermore there is the theorem $C$\texttt{_I} for every constructor~$C$; for |
1677 Furthermore there is the theorem $C$\texttt{_I} for every constructor~$C$; for |
1744 {\out val Br_iff =} |
1744 {\out val Br_iff =} |
1745 {\out "Br(?a, ?l, ?r) = Br(?a', ?l', ?r') <->} |
1745 {\out "Br(?a, ?l, ?r) = Br(?a', ?l', ?r') <->} |
1746 {\out ?a = ?a' & ?l = ?l' & ?r = ?r'" : thm} |
1746 {\out ?a = ?a' & ?l = ?l' & ?r = ?r'" : thm} |
1747 \end{ttbox} |
1747 \end{ttbox} |
1748 |
1748 |
1749 The purpose of \ttindex{mk_cases} is to generate simplified instances of the |
1749 The purpose of \ttindex{mk_cases} is to generate instances of the elimination |
1750 elimination (case analysis) rule. Its theorem list argument is a list of |
1750 (case analysis) rule that have been simplified using freeness reasoning. For |
1751 constructor definitions, which it uses for freeness reasoning. For example, |
1751 example, this instance of the elimination rule propagates type-checking |
1752 this instance of the elimination rule propagates type-checking information |
1752 information from the premise $\texttt{Br}(a,l,r)\in\texttt{bt}(A)$: |
1753 from the premise $\texttt{Br}(a,l,r)\in\texttt{bt}(A)$: |
1753 \begin{ttbox} |
1754 \begin{ttbox} |
1754 val BrE = bt.mk_cases "Br(a,l,r) : bt(A)"; |
1755 val BrE = bt.mk_cases bt.con_defs "Br(a,l,r) : bt(A)"; |
|
1756 {\out val BrE =} |
1755 {\out val BrE =} |
1757 {\out "[| Br(?a, ?l, ?r) : bt(?A);} |
1756 {\out "[| Br(?a, ?l, ?r) : bt(?A);} |
1758 {\out [| ?a : ?A; ?l : bt(?A); ?r : bt(?A) |] ==> ?Q |] ==> ?Q" : thm} |
1757 {\out [| ?a : ?A; ?l : bt(?A); ?r : bt(?A) |] ==> ?Q |] ==> ?Q" : thm} |
1759 \end{ttbox} |
1758 \end{ttbox} |
1760 |
1759 |
2128 having the same name. The the substructure contains the following elements: |
2127 having the same name. The the substructure contains the following elements: |
2129 |
2128 |
2130 \begin{ttbox} |
2129 \begin{ttbox} |
2131 val intrs : thm list \textrm{the introduction rules} |
2130 val intrs : thm list \textrm{the introduction rules} |
2132 val elim : thm \textrm{the elimination (case analysis) rule} |
2131 val elim : thm \textrm{the elimination (case analysis) rule} |
2133 val mk_cases : thm list -> string -> thm \textrm{case analysis, see below} |
2132 val mk_cases : string -> thm \textrm{case analysis, see below} |
2134 val induct : thm \textrm{the standard induction rule} |
2133 val induct : thm \textrm{the standard induction rule} |
2135 val mutual_induct : thm \textrm{the mutual induction rule, or \texttt{True}} |
2134 val mutual_induct : thm \textrm{the mutual induction rule, or \texttt{True}} |
2136 val defs : thm list \textrm{definitions of operators} |
2135 val defs : thm list \textrm{definitions of operators} |
2137 val bnd_mono : thm list \textrm{monotonicity property} |
2136 val bnd_mono : thm list \textrm{monotonicity property} |
2138 val dom_subset : thm list \textrm{inclusion in `bounding set'} |
2137 val dom_subset : thm list \textrm{inclusion in `bounding set'} |
2158 \end{ttbox} |
2157 \end{ttbox} |
2159 The theory goes on to define contraction and parallel contraction |
2158 The theory goes on to define contraction and parallel contraction |
2160 inductively. Then the file \texttt{ex/Comb.ML} defines special cases of |
2159 inductively. Then the file \texttt{ex/Comb.ML} defines special cases of |
2161 contraction using \texttt{mk_cases}: |
2160 contraction using \texttt{mk_cases}: |
2162 \begin{ttbox} |
2161 \begin{ttbox} |
2163 val K_contractE = contract.mk_cases comb.con_defs "K -1-> r"; |
2162 val K_contractE = contract.mk_cases "K -1-> r"; |
2164 {\out val K_contractE = "K -1-> ?r ==> ?Q" : thm} |
2163 {\out val K_contractE = "K -1-> ?r ==> ?Q" : thm} |
2165 \end{ttbox} |
2164 \end{ttbox} |
2166 We can read this as saying that the combinator \texttt{K} cannot reduce to |
2165 We can read this as saying that the combinator \texttt{K} cannot reduce to |
2167 anything. Similar elimination rules for \texttt{S} and application are also |
2166 anything. Similar elimination rules for \texttt{S} and application are also |
2168 generated and are supplied to the classical reasoner. Note that |
2167 generated and are supplied to the classical reasoner. Note that |