17 |
17 |
18 \section{Simplification for dummies} |
18 \section{Simplification for dummies} |
19 \label{sec:simp-for-dummies} |
19 \label{sec:simp-for-dummies} |
20 |
20 |
21 Basic use of the simplifier is particularly easy because each theory |
21 Basic use of the simplifier is particularly easy because each theory |
22 is equipped with an implicit {\em current |
22 is equipped with sensible default information controlling the rewrite |
23 simpset}\index{simpset!current}. This provides sensible default |
23 process --- namely the implicit {\em current |
24 information in many cases. A suite of commands refer to the implicit |
24 simpset}\index{simpset!current}. A suite of simple commands is |
25 simpset of the current theory context. |
25 provided that refer to the implicit simpset of the current theory |
|
26 context. |
26 |
27 |
27 \begin{warn} |
28 \begin{warn} |
28 Make sure that you are working within the correct theory context. |
29 Make sure that you are working within the correct theory context. |
29 Executing proofs interactively, or loading them from ML files |
30 Executing proofs interactively, or loading them from ML files |
30 without associated theories may require setting the current theory |
31 without associated theories may require setting the current theory |
52 \item[\ttindexbold{Full_simp_tac}] is like \verb$Simp_tac$, but also |
53 \item[\ttindexbold{Full_simp_tac}] is like \verb$Simp_tac$, but also |
53 simplifies the assumptions (without using the assumptions to |
54 simplifies the assumptions (without using the assumptions to |
54 simplify each other or the actual goal). |
55 simplify each other or the actual goal). |
55 |
56 |
56 \item[\ttindexbold{Asm_full_simp_tac}] is like \verb$Asm_simp_tac$, |
57 \item[\ttindexbold{Asm_full_simp_tac}] is like \verb$Asm_simp_tac$, |
57 but also simplifies the assumptions one by one. Working from |
58 but also simplifies the assumptions one by one. Strictly working |
58 \emph{left to right}, it uses each assumption in the simplification |
59 from \emph{left to right}, it uses each assumption in the |
59 of those following. |
60 simplification of those following. |
60 |
61 |
61 \item[set \ttindexbold{trace_simp};] makes the simplifier output |
62 \item[set \ttindexbold{trace_simp};] makes the simplifier output |
62 internal operations. This includes rewrite steps, but also |
63 internal operations. This includes rewrite steps, but also |
63 bookkeeping like modifications of the simpset. |
64 bookkeeping like modifications of the simpset. |
64 \end{ttdescription} |
65 \end{ttdescription} |
235 called \ttindexbold{HOL_basic_ss}. |
236 called \ttindexbold{HOL_basic_ss}. |
236 |
237 |
237 \item[\ttindexbold{merge_ss} ($ss@1$, $ss@2$)] merges simpsets $ss@1$ |
238 \item[\ttindexbold{merge_ss} ($ss@1$, $ss@2$)] merges simpsets $ss@1$ |
238 and $ss@2$ by building the union of their respective rewrite rules, |
239 and $ss@2$ by building the union of their respective rewrite rules, |
239 simplification procedures and congruences. The other components |
240 simplification procedures and congruences. The other components |
240 (tactics etc.) cannot be merged, though; they are simply inherited |
241 (tactics etc.) cannot be merged, though; they are taken from either |
241 from either simpset. |
242 simpset\footnote{Actually from $ss@1$, but it would unwise to count |
|
243 on that.}. |
242 |
244 |
243 \end{ttdescription} |
245 \end{ttdescription} |
244 |
246 |
245 |
247 |
246 \subsection{Accessing the current simpset} |
248 \subsection{Accessing the current simpset} |
349 \begin{ttbox} |
351 \begin{ttbox} |
350 addsimprocs : simpset * simproc list -> simpset |
352 addsimprocs : simpset * simproc list -> simpset |
351 delsimprocs : simpset * simproc list -> simpset |
353 delsimprocs : simpset * simproc list -> simpset |
352 \end{ttbox} |
354 \end{ttbox} |
353 |
355 |
354 Simplification procedures are {\ML} functions that may produce |
356 Simplification procedures are {\ML} objects of abstract type |
|
357 \texttt{simproc}. Basically they are just functions that may produce |
355 \emph{proven} rewrite rules on demand. They are associated with |
358 \emph{proven} rewrite rules on demand. They are associated with |
356 certain patterns that conceptually represent left-hand sides of |
359 certain patterns that conceptually represent left-hand sides of |
357 equations; these are shown by \texttt{print_ss}. During its |
360 equations; these are shown by \texttt{print_ss}. During its |
358 operation, the simplifier may offer a simplification procedure the |
361 operation, the simplifier may offer a simplification procedure the |
359 current redex and ask for a suitable rewrite rule. Thus rules may be |
362 current redex and ask for a suitable rewrite rule. Thus rules may be |
368 |
371 |
369 \item[$ss$ \ttindexbold{delsimprocs} $procs$] deletes simplification |
372 \item[$ss$ \ttindexbold{delsimprocs} $procs$] deletes simplification |
370 procedures $procs$ from the current simpset. |
373 procedures $procs$ from the current simpset. |
371 |
374 |
372 \end{ttdescription} |
375 \end{ttdescription} |
|
376 |
|
377 For example, simplification procedures \ttindexbold{nat_cancel} of |
|
378 \texttt{HOL/Arith} cancel common summands and constant factors out of |
|
379 several relations of sums over natural numbers. |
|
380 |
|
381 Consider the following goal, which after cancelling $a$ on both sides |
|
382 contains a factor of $2$. Simplifying with the simpset of |
|
383 \texttt{Arith.thy} will do the cancellation automatically: |
|
384 \begin{ttbox} |
|
385 {\out 1. x + a + x < y + y + 2 + a + a + a + a + a} |
|
386 by (Simp_tac 1); |
|
387 {\out 1. x < Suc (a + (a + y))} |
|
388 \end{ttbox} |
373 |
389 |
374 |
390 |
375 \subsection{*Congruence rules}\index{congruence rules}\label{sec:simp-congs} |
391 \subsection{*Congruence rules}\index{congruence rules}\label{sec:simp-congs} |
376 \begin{ttbox} |
392 \begin{ttbox} |
377 addcongs : simpset * thm list -> simpset \hfill{\bf infix 4} |
393 addcongs : simpset * thm list -> simpset \hfill{\bf infix 4} |
681 asm_simplify : simpset -> thm -> thm |
697 asm_simplify : simpset -> thm -> thm |
682 full_simplify : simpset -> thm -> thm |
698 full_simplify : simpset -> thm -> thm |
683 asm_full_simplify : simpset -> thm -> thm |
699 asm_full_simplify : simpset -> thm -> thm |
684 \end{ttbox} |
700 \end{ttbox} |
685 |
701 |
686 These are forward rules, simplifying theorems in a similar way as the |
702 These functions provide \emph{forward} rules for simplification. |
687 corresponding simplification tactics do. The forward rules affect the whole |
703 Their effect is analogous to the corresponding tactics described in |
688 |
704 \S\ref{simp-tactics}, but affect the whole theorem instead of just a |
689 subgoals of a proof state. The |
705 certain subgoal. Also note that the looper~/ solver process as |
690 looper~/ solver process as described in \S\ref{sec:simp-looper} and |
706 described in \S\ref{sec:simp-looper} and \S\ref{sec:simp-solver} is |
691 \S\ref{sec:simp-solver} does not apply here, though. |
707 omitted in forward simplification. |
692 |
708 |
693 \begin{warn} |
709 \begin{warn} |
694 Forward simplification should be used rarely in ordinary proof |
710 Forward simplification should be used rarely in ordinary proof |
695 scripts. It as mainly intended to provide an internal interface to |
711 scripts. It as mainly intended to provide an internal interface to |
696 the simplifier for ML coded special utilities. |
712 the simplifier for special utilities. |
697 \end{warn} |
713 \end{warn} |
698 |
714 |
699 |
715 |
700 \section{Examples of using the simplifier} |
716 \section{Examples of using the simplifier} |
701 \index{examples!of simplification} Assume we are working within {\tt |
717 \index{examples!of simplification} Assume we are working within {\tt |
710 \item[induct] |
726 \item[induct] |
711 is the induction rule $\List{\Var{P}(0);\; \Forall x. \Var{P}(x)\Imp |
727 is the induction rule $\List{\Var{P}(0);\; \Forall x. \Var{P}(x)\Imp |
712 \Var{P}(Suc(x))} \Imp \Var{P}(\Var{n})$. |
728 \Var{P}(Suc(x))} \Imp \Var{P}(\Var{n})$. |
713 \end{ttdescription} |
729 \end{ttdescription} |
714 We augment the implicit simpset inherited from \texttt{Nat} with the |
730 We augment the implicit simpset inherited from \texttt{Nat} with the |
715 basic rewrite rules for natural numbers: |
731 basic rewrite rules for addition of natural numbers: |
716 \begin{ttbox} |
732 \begin{ttbox} |
717 Addsimps [add_0, add_Suc]; |
733 Addsimps [add_0, add_Suc]; |
718 \end{ttbox} |
734 \end{ttbox} |
719 |
735 |
720 \subsection{A trivial example} |
736 \subsection{A trivial example} |
751 {\out No subgoals!} |
767 {\out No subgoals!} |
752 \end{ttbox} |
768 \end{ttbox} |
753 |
769 |
754 \subsection{An example of tracing} |
770 \subsection{An example of tracing} |
755 \index{tracing!of simplification|(}\index{*trace_simp} |
771 \index{tracing!of simplification|(}\index{*trace_simp} |
756 Let us prove a similar result involving more complex terms. The two |
772 |
757 equations together can be used to prove that addition is commutative. |
773 Let us prove a similar result involving more complex terms. We prove |
|
774 that addition is commutative. |
758 \begin{ttbox} |
775 \begin{ttbox} |
759 goal Nat.thy "m+Suc(n) = Suc(m+n)"; |
776 goal Nat.thy "m+Suc(n) = Suc(m+n)"; |
760 {\out Level 0} |
777 {\out Level 0} |
761 {\out m + Suc(n) = Suc(m + n)} |
778 {\out m + Suc(n) = Suc(m + n)} |
762 {\out 1. m + Suc(n) = Suc(m + n)} |
779 {\out 1. m + Suc(n) = Suc(m + n)} |
763 \end{ttbox} |
780 \end{ttbox} |
764 We again perform induction on~$m$ and get two subgoals: |
781 Performing induction on~$m$ yields two subgoals: |
765 \begin{ttbox} |
782 \begin{ttbox} |
766 by (res_inst_tac [("n","m")] induct 1); |
783 by (res_inst_tac [("n","m")] induct 1); |
767 {\out Level 1} |
784 {\out Level 1} |
768 {\out m + Suc(n) = Suc(m + n)} |
785 {\out m + Suc(n) = Suc(m + n)} |
769 {\out 1. 0 + Suc(n) = Suc(0 + n)} |
786 {\out 1. 0 + Suc(n) = Suc(0 + n)} |
812 {\out m + Suc(n) = Suc(m + n)} |
829 {\out m + Suc(n) = Suc(m + n)} |
813 {\out No subgoals!} |
830 {\out No subgoals!} |
814 \end{ttbox} |
831 \end{ttbox} |
815 \index{tracing!of simplification|)} |
832 \index{tracing!of simplification|)} |
816 |
833 |
|
834 |
817 \subsection{Free variables and simplification} |
835 \subsection{Free variables and simplification} |
818 Here is a conjecture to be proved for an arbitrary function~$f$ satisfying |
836 |
819 the law $f(Suc(\Var{n})) = Suc(f(\Var{n}))$: |
837 Here is a conjecture to be proved for an arbitrary function~$f$ |
|
838 satisfying the law $f(Suc(\Var{n})) = Suc(f(\Var{n}))$: |
820 \begin{ttbox} |
839 \begin{ttbox} |
821 val [prem] = goal Nat.thy |
840 val [prem] = goal Nat.thy |
822 "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)"; |
841 "(!!n. f(Suc(n)) = Suc(f(n))) ==> f(i+j) = i+f(j)"; |
823 {\out Level 0} |
842 {\out Level 0} |
824 {\out f(i + j) = i + f(j)} |
843 {\out f(i + j) = i + f(j)} |
969 "sum f 0 = 0" |
988 "sum f 0 = 0" |
970 "sum f (Suc n) = f(n) + sum f n" |
989 "sum f (Suc n) = f(n) + sum f n" |
971 end |
990 end |
972 \end{ttbox} |
991 \end{ttbox} |
973 The \texttt{primrec} declaration automatically adds rewrite rules for |
992 The \texttt{primrec} declaration automatically adds rewrite rules for |
974 \texttt{sum} to the default simpset. We now insert the AC-rules for~$+$: |
993 \texttt{sum} to the default simpset. We now remove the |
975 \begin{ttbox} |
994 \texttt{nat_cancel} simplification procedures (in order not to spoil |
|
995 the example) and insert the AC-rules for~$+$: |
|
996 \begin{ttbox} |
|
997 Delsimprocs nat_cancel; |
976 Addsimps add_ac; |
998 Addsimps add_ac; |
977 \end{ttbox} |
999 \end{ttbox} |
978 Our desired theorem now reads ${\tt sum} \, (\lambda i.i) \, (n+1) = |
1000 Our desired theorem now reads ${\tt sum} \, (\lambda i.i) \, (n+1) = |
979 n\times(n+1)/2$. The Isabelle goal has both sides multiplied by~$2$: |
1001 n\times(n+1)/2$. The Isabelle goal has both sides multiplied by~$2$: |
980 \begin{ttbox} |
1002 \begin{ttbox} |
1026 Ordered rewriting is equally successful in proving |
1048 Ordered rewriting is equally successful in proving |
1027 $\sum@{i=1}^n i^3 = n^2\times(n+1)^2/4$. |
1049 $\sum@{i=1}^n i^3 = n^2\times(n+1)^2/4$. |
1028 |
1050 |
1029 |
1051 |
1030 \subsection{Re-orienting equalities} |
1052 \subsection{Re-orienting equalities} |
1031 Ordered rewriting with the derived rule {\tt symmetry} can reverse equality |
1053 Ordered rewriting with the derived rule {\tt symmetry} can reverse |
1032 signs: |
1054 equations: |
1033 \begin{ttbox} |
1055 \begin{ttbox} |
1034 val symmetry = prove_goal HOL.thy "(x=y) = (y=x)" |
1056 val symmetry = prove_goal HOL.thy "(x=y) = (y=x)" |
1035 (fn _ => [Blast_tac 1]); |
1057 (fn _ => [Blast_tac 1]); |
1036 \end{ttbox} |
1058 \end{ttbox} |
1037 This is frequently useful. Assumptions of the form $s=t$, where $t$ occurs |
1059 This is frequently useful. Assumptions of the form $s=t$, where $t$ occurs |
1102 making it rewrite only actual abstractions. The simplification |
1124 making it rewrite only actual abstractions. The simplification |
1103 procedure \texttt{pair_eta_expand_proc} is defined as follows: |
1125 procedure \texttt{pair_eta_expand_proc} is defined as follows: |
1104 \begin{ttbox} |
1126 \begin{ttbox} |
1105 local |
1127 local |
1106 val lhss = |
1128 val lhss = |
1107 [read_cterm (sign_of Prod.thy) ("f::'a*'b=>'c", TVar (("'a", 0), []))]; |
1129 [read_cterm (sign_of Prod.thy) ("f::'a*'b=>'c", TVar (("'z", 0), []))]; |
1108 val rew = mk_meta_eq pair_eta_expand; \medskip |
1130 val rew = mk_meta_eq pair_eta_expand; \medskip |
1109 fun proc _ _ (Abs _) = Some rew |
1131 fun proc _ _ (Abs _) = Some rew |
1110 | proc _ _ _ = None; |
1132 | proc _ _ _ = None; |
1111 in |
1133 in |
1112 val pair_eta_expand_proc = Simplifier.mk_simproc "pair_eta_expand" lhss proc; |
1134 val pair_eta_expand_proc = |
|
1135 Simplifier.mk_simproc "pair_eta_expand" lhss proc; |
1113 end; |
1136 end; |
1114 \end{ttbox} |
1137 \end{ttbox} |
1115 This is an example of using \texttt{pair_eta_expand_proc}: |
1138 This is an example of using \texttt{pair_eta_expand_proc}: |
1116 \begin{ttbox} |
1139 \begin{ttbox} |
1117 {\out 1. P (\%p::'a * 'a. fst p + snd p + z)} |
1140 {\out 1. P (\%p::'a * 'a. fst p + snd p + z)} |
1124 In the above example the simplification procedure just did fine |
1147 In the above example the simplification procedure just did fine |
1125 grained control over rule application, beyond higher-order pattern |
1148 grained control over rule application, beyond higher-order pattern |
1126 matching. Usually, procedures would do some more work, in particular |
1149 matching. Usually, procedures would do some more work, in particular |
1127 prove particular theorems depending on the current redex. |
1150 prove particular theorems depending on the current redex. |
1128 |
1151 |
1129 For example, simplification procedures \ttindexbold{nat_cancel} of |
|
1130 \texttt{HOL/Arith} cancel common summands and constant factors out of |
|
1131 several relations of sums over natural numbers. |
|
1132 |
|
1133 Consider the following goal, which after cancelling $a$ on both sides |
|
1134 contains a factor of $2$. Simplifying with the simpset of |
|
1135 \texttt{Arith.thy} will do the cancellation automatically: |
|
1136 \begin{ttbox} |
|
1137 {\out 1. x + a + x < y + y + 2 + a + a + a + a + a} |
|
1138 by (Simp_tac 1); |
|
1139 {\out 1. x < Suc (a + (a + y))} |
|
1140 \end{ttbox} |
|
1141 |
|
1142 \medskip |
|
1143 |
|
1144 The {\ML} sources for these simplification procedures consist of a |
|
1145 generic part (files \texttt{cancel_sums.ML} and |
|
1146 \texttt{cancel_factor.ML} in \texttt{Provers/Arith}), and a |
|
1147 \texttt{HOL} specific part in \texttt{HOL/arith_data.ML}. |
|
1148 |
|
1149 |
1152 |
1150 \section{*Setting up the simplifier}\label{sec:setting-up-simp} |
1153 \section{*Setting up the simplifier}\label{sec:setting-up-simp} |
1151 \index{simplification!setting up} |
1154 \index{simplification!setting up} |
1152 |
1155 |
1153 Setting up the simplifier for new logics is complicated. This section |
1156 Setting up the simplifier for new logics is complicated. This section |
1161 \begin{ttbox} |
1164 \begin{ttbox} |
1162 use "$ISABELLE_HOME/src/Provers/simplifier.ML"; |
1165 use "$ISABELLE_HOME/src/Provers/simplifier.ML"; |
1163 use "$ISABELLE_HOME/src/Provers/splitter.ML"; |
1166 use "$ISABELLE_HOME/src/Provers/splitter.ML"; |
1164 \end{ttbox} |
1167 \end{ttbox} |
1165 |
1168 |
1166 Simplification works by reducing various object-equalities to |
1169 Simplification requires reflecting various object-equalities to |
1167 meta-equality. It requires rules stating that equal terms and equivalent |
1170 meta-level rewrite rules. This demands rules stating that equal terms |
1168 formulae are also equal at the meta-level. The rule declaration part of |
1171 and equivalent formulae are also equal at the meta-level. The rule |
1169 the file {\tt FOL/IFOL.thy} contains the two lines |
1172 declaration part of the file {\tt FOL/IFOL.thy} contains the two lines |
1170 \begin{ttbox}\index{*eq_reflection theorem}\index{*iff_reflection theorem} |
1173 \begin{ttbox}\index{*eq_reflection theorem}\index{*iff_reflection theorem} |
1171 eq_reflection "(x=y) ==> (x==y)" |
1174 eq_reflection "(x=y) ==> (x==y)" |
1172 iff_reflection "(P<->Q) ==> (P==Q)" |
1175 iff_reflection "(P<->Q) ==> (P==Q)" |
1173 \end{ttbox} |
1176 \end{ttbox} |
1174 Of course, you should only assert such rules if they are true for your |
1177 Of course, you should only assert such rules if they are true for your |
1181 work for later variants of Constructive Type Theory that use |
1184 work for later variants of Constructive Type Theory that use |
1182 intensional equality~\cite{nordstrom90}. |
1185 intensional equality~\cite{nordstrom90}. |
1183 |
1186 |
1184 |
1187 |
1185 \subsection{A collection of standard rewrite rules} |
1188 \subsection{A collection of standard rewrite rules} |
1186 The file begins by proving lots of standard rewrite rules about the logical |
1189 |
1187 connectives. These include cancellation and associative laws. To prove |
1190 We first prove lots of standard rewrite rules about the logical |
1188 them easily, it defines a function that echoes the desired law and then |
1191 connectives. These include cancellation and associative laws. We |
1189 supplies it the theorem prover for intuitionistic \FOL: |
1192 define a function that echoes the desired law and then supplies it the |
|
1193 prover for intuitionistic \FOL: |
1190 \begin{ttbox} |
1194 \begin{ttbox} |
1191 fun int_prove_fun s = |
1195 fun int_prove_fun s = |
1192 (writeln s; |
1196 (writeln s; |
1193 prove_goal IFOL.thy s |
1197 prove_goal IFOL.thy s |
1194 (fn prems => [ (cut_facts_tac prems 1), |
1198 (fn prems => [ (cut_facts_tac prems 1), |
1368 By adding the congruence rule {\tt conj_cong}, we could obtain a similar |
1372 By adding the congruence rule {\tt conj_cong}, we could obtain a similar |
1369 effect for conjunctions. |
1373 effect for conjunctions. |
1370 |
1374 |
1371 |
1375 |
1372 \subsection{Case splitting} |
1376 \subsection{Case splitting} |
1373 To set up case splitting, we must prove the theorem below and pass it to |
1377 |
1374 \ttindexbold{mk_case_split_tac}. The tactic \ttindexbold{split_tac} uses |
1378 To set up case splitting, we must prove the theorem \texttt{meta_iffD} |
1375 {\tt mk_meta_eq}, defined above, to convert the splitting rules to |
1379 below and pass it to \ttindexbold{mk_case_split_tac}. The tactic |
1376 meta-equalities. |
1380 \ttindexbold{split_tac} uses {\tt mk_meta_eq}, defined above, to |
|
1381 convert the splitting rules to meta-equalities. |
1377 \begin{ttbox} |
1382 \begin{ttbox} |
1378 val meta_iffD = |
1383 val meta_iffD = |
1379 prove_goal FOL.thy "[| P==Q; Q |] ==> P" |
1384 prove_goal FOL.thy "[| P==Q; Q |] ==> P" |
1380 (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]) |
1385 (fn [prem1,prem2] => [rewtac prem1, rtac prem2 1]) |
1381 \ttbreak |
1386 \ttbreak |