author | paulson |

Tue Jan 19 12:56:27 1999 +0100 (1999-01-19) | |

changeset 6143 | 1eb364a68c54 |

parent 6142 | c0c93b9434ef |

child 6144 | 7d38744313c8 |

freeness reasoning: T.free_iffs

1.1 --- a/doc-src/ZF/ZF.tex Tue Jan 19 11:46:18 1999 +0100 1.2 +++ b/doc-src/ZF/ZF.tex Tue Jan 19 12:56:27 1999 +0100 1.3 @@ -1522,13 +1522,18 @@ 1.4 for example $\texttt{Nil}\not=\texttt{Cons}(a,l)$, and they are injective, for 1.5 example $\texttt{Cons}(a,l)=\texttt{Cons}(a',l') \bimp a=a' \conj l=l'$. 1.6 Because the number of freeness is quadratic in the number of constructors, the 1.7 -datatype package does not prove them, but instead provides several means of 1.8 -proving them dynamically. For the \texttt{list} datatype, freeness reasoning 1.9 -can be done in two ways: by simplifying with the theorems 1.10 -\texttt{list.free_iffs} or by invoking the classical reasoner with 1.11 -\texttt{list.free_SEs} as safe elimination rules. Occasionally this exposes 1.12 -the underlying representation of some constructor, which can be rectified 1.13 -using the command \hbox{\tt fold_tac list.con_defs}. 1.14 +datatype package does not prove them. Instead, it ensures that simplification 1.15 +will prove them dynamically: when the simplifier encounters a formula 1.16 +asserting the equality of two datatype constructors, it performs freeness 1.17 +reasoning. 1.18 + 1.19 +Freeness reasoning can also be done using the classical reasoner, but it is 1.20 +more complicated. You have to add some safe elimination rules rules to the 1.21 +claset. For the \texttt{list} datatype, they are called 1.22 +\texttt{list.free_SEs}. Occasionally this exposes the underlying 1.23 +representation of some constructor, which can be rectified using the command 1.24 +\hbox{\tt fold_tac list.con_defs}. 1.25 + 1.26 1.27 \subsubsection{Structural induction} 1.28 1.29 @@ -1631,8 +1636,7 @@ 1.30 1.31 Most of the theorems about datatypes become part of the default simpset. You 1.32 never need to see them again because the simplifier applies them 1.33 -automatically. Add freeness properties (\texttt{free_iffs}) to the simpset 1.34 -when you want them. Induction or exhaustion are usually invoked by hand, 1.35 +automatically. Induction or exhaustion are usually invoked by hand, 1.36 usually via these special-purpose tactics: 1.37 \begin{ttdescription} 1.38 \item[\ttindexbold{induct_tac} {\tt"}$x${\tt"} $i$] applies structural 1.39 @@ -1718,13 +1722,10 @@ 1.40 {\out ALL x r. Br(x, t2, r) ~= t2 |]} 1.41 {\out ==> ALL x r. Br(x, Br(a, t1, t2), r) ~= Br(a, t1, t2)} 1.42 \end{ttbox} 1.43 -Both subgoals are proved using the simplifier. Tactic 1.44 -\texttt{asm_full_simp_tac} is used, rewriting the assumptions. 1.45 -This is because simplification using the freeness properties can unfold the 1.46 -definition of constructor~\texttt{Br}, so we arrange that all occurrences are 1.47 -unfolded. 1.48 +Both subgoals are proved using \texttt{Auto_tac}, which performs the necessary 1.49 +freeness reasoning. 1.50 \begin{ttbox} 1.51 -by (ALLGOALS (asm_full_simp_tac (simpset() addsimps bt.free_iffs))); 1.52 +by Auto_tac; 1.53 {\out Level 2} 1.54 {\out l : bt(A) ==> ALL x r. Br(x, l, r) ~= l} 1.55 {\out No subgoals!} 1.56 @@ -1792,10 +1793,10 @@ 1.57 essentially binary notation, so freeness properties can be proved fast. 1.58 \begin{ttbox} 1.59 Goal "C00 ~= C01"; 1.60 -by (simp_tac (simpset() addsimps enum.free_iffs) 1); 1.61 +by (Simp_tac 1); 1.62 \end{ttbox} 1.63 You need not derive such inequalities explicitly. The simplifier will dispose 1.64 -of them automatically, given the theorem list \texttt{free_iffs}. 1.65 +of them automatically. 1.66 1.67 \index{*datatype|)} 1.68