1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{simp{\isadigit{2}}}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \isamarkupsection{Simplification% |
|
19 } |
|
20 \isamarkuptrue% |
|
21 % |
|
22 \begin{isamarkuptext}% |
|
23 \label{sec:simplification-II}\index{simplification|(} |
|
24 This section describes features not covered until now. It also |
|
25 outlines the simplification process itself, which can be helpful |
|
26 when the simplifier does not do what you expect of it.% |
|
27 \end{isamarkuptext}% |
|
28 \isamarkuptrue% |
|
29 % |
|
30 \isamarkupsubsection{Advanced Features% |
|
31 } |
|
32 \isamarkuptrue% |
|
33 % |
|
34 \isamarkupsubsubsection{Congruence Rules% |
|
35 } |
|
36 \isamarkuptrue% |
|
37 % |
|
38 \begin{isamarkuptext}% |
|
39 \label{sec:simp-cong} |
|
40 While simplifying the conclusion $Q$ |
|
41 of $P \Imp Q$, it is legal to use the assumption $P$. |
|
42 For $\Imp$ this policy is hardwired, but |
|
43 contextual information can also be made available for other |
|
44 operators. For example, \isa{xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ xs\ {\isaliteral{40}{\isacharat}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs} simplifies to \isa{True} because we may use \isa{xs\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} when simplifying \isa{xs\ {\isaliteral{40}{\isacharat}}\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs}. The generation of contextual information during simplification is |
|
45 controlled by so-called \bfindex{congruence rules}. This is the one for |
|
46 \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}: |
|
47 \begin{isabelle}% |
|
48 \ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}P\ {\isaliteral{3D}{\isacharequal}}\ P{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ {\isaliteral{3D}{\isacharequal}}\ Q{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}% |
|
49 \end{isabelle} |
|
50 It should be read as follows: |
|
51 In order to simplify \isa{P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q} to \isa{P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ Q{\isaliteral{27}{\isacharprime}}}, |
|
52 simplify \isa{P} to \isa{P{\isaliteral{27}{\isacharprime}}} |
|
53 and assume \isa{P{\isaliteral{27}{\isacharprime}}} when simplifying \isa{Q} to \isa{Q{\isaliteral{27}{\isacharprime}}}. |
|
54 |
|
55 Here are some more examples. The congruence rules for bounded |
|
56 quantifiers supply contextual information about the bound variable: |
|
57 \begin{isabelle}% |
|
58 \ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}A\ {\isaliteral{3D}{\isacharequal}}\ B{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x\ {\isaliteral{3D}{\isacharequal}}\ Q\ x{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
59 \isaindent{\ \ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{5C3C696E3E}{\isasymin}}A{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{5C3C696E3E}{\isasymin}}B{\isaliteral{2E}{\isachardot}}\ Q\ x{\isaliteral{29}{\isacharparenright}}% |
|
60 \end{isabelle} |
|
61 One congruence rule for conditional expressions supplies contextual |
|
62 information for simplifying the \isa{then} and \isa{else} cases: |
|
63 \begin{isabelle}% |
|
64 \ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}b\ {\isaliteral{3D}{\isacharequal}}\ c{\isaliteral{3B}{\isacharsemicolon}}\ c\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{3D}{\isacharequal}}\ u{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ c\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ y\ {\isaliteral{3D}{\isacharequal}}\ v{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline |
|
65 \isaindent{\ \ \ \ \ }{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}if\ b\ then\ x\ else\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ c\ then\ u\ else\ v{\isaliteral{29}{\isacharparenright}}% |
|
66 \end{isabelle} |
|
67 An alternative congruence rule for conditional expressions |
|
68 actually \emph{prevents} simplification of some arguments: |
|
69 \begin{isabelle}% |
|
70 \ \ \ \ \ b\ {\isaliteral{3D}{\isacharequal}}\ c\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}if\ b\ then\ x\ else\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ c\ then\ x\ else\ y{\isaliteral{29}{\isacharparenright}}% |
|
71 \end{isabelle} |
|
72 Only the first argument is simplified; the others remain unchanged. |
|
73 This makes simplification much faster and is faithful to the evaluation |
|
74 strategy in programming languages, which is why this is the default |
|
75 congruence rule for \isa{if}. Analogous rules control the evaluation of |
|
76 \isa{case} expressions. |
|
77 |
|
78 You can declare your own congruence rules with the attribute \attrdx{cong}, |
|
79 either globally, in the usual manner, |
|
80 \begin{quote} |
|
81 \isacommand{declare} \textit{theorem-name} \isa{{\isaliteral{5B}{\isacharbrackleft}}cong{\isaliteral{5D}{\isacharbrackright}}} |
|
82 \end{quote} |
|
83 or locally in a \isa{simp} call by adding the modifier |
|
84 \begin{quote} |
|
85 \isa{cong{\isaliteral{3A}{\isacharcolon}}} \textit{list of theorem names} |
|
86 \end{quote} |
|
87 The effect is reversed by \isa{cong\ del} instead of \isa{cong}. |
|
88 |
|
89 \begin{warn} |
|
90 The congruence rule \isa{conj{\isaliteral{5F}{\isacharunderscore}}cong} |
|
91 \begin{isabelle}% |
|
92 \ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}P\ {\isaliteral{3D}{\isacharequal}}\ P{\isaliteral{27}{\isacharprime}}{\isaliteral{3B}{\isacharsemicolon}}\ P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ {\isaliteral{3D}{\isacharequal}}\ Q{\isaliteral{27}{\isacharprime}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}P{\isaliteral{27}{\isacharprime}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q{\isaliteral{27}{\isacharprime}}{\isaliteral{29}{\isacharparenright}}% |
|
93 \end{isabelle} |
|
94 \par\noindent |
|
95 is occasionally useful but is not a default rule; you have to declare it explicitly. |
|
96 \end{warn}% |
|
97 \end{isamarkuptext}% |
|
98 \isamarkuptrue% |
|
99 % |
|
100 \isamarkupsubsubsection{Permutative Rewrite Rules% |
|
101 } |
|
102 \isamarkuptrue% |
|
103 % |
|
104 \begin{isamarkuptext}% |
|
105 \index{rewrite rules!permutative|bold}% |
|
106 An equation is a \textbf{permutative rewrite rule} if the left-hand |
|
107 side and right-hand side are the same up to renaming of variables. The most |
|
108 common permutative rule is commutativity: \isa{x\ {\isaliteral{2B}{\isacharplus}}\ y\ {\isaliteral{3D}{\isacharequal}}\ y\ {\isaliteral{2B}{\isacharplus}}\ x}. Other examples |
|
109 include \isa{x\ {\isaliteral{2D}{\isacharminus}}\ y\ {\isaliteral{2D}{\isacharminus}}\ z\ {\isaliteral{3D}{\isacharequal}}\ x\ {\isaliteral{2D}{\isacharminus}}\ z\ {\isaliteral{2D}{\isacharminus}}\ y} in arithmetic and \isa{insert\ x\ {\isaliteral{28}{\isacharparenleft}}insert\ y\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ insert\ y\ {\isaliteral{28}{\isacharparenleft}}insert\ x\ A{\isaliteral{29}{\isacharparenright}}} for sets. Such rules are problematic because |
|
110 once they apply, they can be used forever. The simplifier is aware of this |
|
111 danger and treats permutative rules by means of a special strategy, called |
|
112 \bfindex{ordered rewriting}: a permutative rewrite |
|
113 rule is only applied if the term becomes smaller with respect to a fixed |
|
114 lexicographic ordering on terms. For example, commutativity rewrites |
|
115 \isa{b\ {\isaliteral{2B}{\isacharplus}}\ a} to \isa{a\ {\isaliteral{2B}{\isacharplus}}\ b}, but then stops because \isa{a\ {\isaliteral{2B}{\isacharplus}}\ b} is strictly |
|
116 smaller than \isa{b\ {\isaliteral{2B}{\isacharplus}}\ a}. Permutative rewrite rules can be turned into |
|
117 simplification rules in the usual manner via the \isa{simp} attribute; the |
|
118 simplifier recognizes their special status automatically. |
|
119 |
|
120 Permutative rewrite rules are most effective in the case of |
|
121 associative-commutative functions. (Associativity by itself is not |
|
122 permutative.) When dealing with an AC-function~$f$, keep the |
|
123 following points in mind: |
|
124 \begin{itemize}\index{associative-commutative function} |
|
125 |
|
126 \item The associative law must always be oriented from left to right, |
|
127 namely $f(f(x,y),z) = f(x,f(y,z))$. The opposite orientation, if |
|
128 used with commutativity, can lead to nontermination. |
|
129 |
|
130 \item To complete your set of rewrite rules, you must add not just |
|
131 associativity~(A) and commutativity~(C) but also a derived rule, {\bf |
|
132 left-com\-mut\-ativ\-ity} (LC): $f(x,f(y,z)) = f(y,f(x,z))$. |
|
133 \end{itemize} |
|
134 Ordered rewriting with the combination of A, C, and LC sorts a term |
|
135 lexicographically: |
|
136 \[\def\maps#1{~\stackrel{#1}{\leadsto}~} |
|
137 f(f(b,c),a) \maps{A} f(b,f(c,a)) \maps{C} f(b,f(a,c)) \maps{LC} f(a,f(b,c)) \] |
|
138 |
|
139 Note that ordered rewriting for \isa{{\isaliteral{2B}{\isacharplus}}} and \isa{{\isaliteral{2A}{\isacharasterisk}}} on numbers is rarely |
|
140 necessary because the built-in arithmetic prover often succeeds without |
|
141 such tricks.% |
|
142 \end{isamarkuptext}% |
|
143 \isamarkuptrue% |
|
144 % |
|
145 \isamarkupsubsection{How the Simplifier Works% |
|
146 } |
|
147 \isamarkuptrue% |
|
148 % |
|
149 \begin{isamarkuptext}% |
|
150 \label{sec:SimpHow} |
|
151 Roughly speaking, the simplifier proceeds bottom-up: subterms are simplified |
|
152 first. A conditional equation is only applied if its condition can be |
|
153 proved, again by simplification. Below we explain some special features of |
|
154 the rewriting process.% |
|
155 \end{isamarkuptext}% |
|
156 \isamarkuptrue% |
|
157 % |
|
158 \isamarkupsubsubsection{Higher-Order Patterns% |
|
159 } |
|
160 \isamarkuptrue% |
|
161 % |
|
162 \begin{isamarkuptext}% |
|
163 \index{simplification rule|(} |
|
164 So far we have pretended the simplifier can deal with arbitrary |
|
165 rewrite rules. This is not quite true. For reasons of feasibility, |
|
166 the simplifier expects the |
|
167 left-hand side of each rule to be a so-called \emph{higher-order |
|
168 pattern}~\cite{nipkow-patterns}\indexbold{patterns!higher-order}. |
|
169 This restricts where |
|
170 unknowns may occur. Higher-order patterns are terms in $\beta$-normal |
|
171 form. (This means there are no subterms of the form $(\lambda x. M)(N)$.) |
|
172 Each occurrence of an unknown is of the form |
|
173 $\Var{f}~x@1~\dots~x@n$, where the $x@i$ are distinct bound |
|
174 variables. Thus all ordinary rewrite rules, where all unknowns are |
|
175 of base type, for example \isa{{\isaliteral{3F}{\isacharquery}}a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}b\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}c\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}b\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{3F}{\isacharquery}}c{\isaliteral{29}{\isacharparenright}}}, are acceptable: if an unknown is |
|
176 of base type, it cannot have any arguments. Additionally, the rule |
|
177 \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}Q\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}Q\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}} is also acceptable, in |
|
178 both directions: all arguments of the unknowns \isa{{\isaliteral{3F}{\isacharquery}}P} and |
|
179 \isa{{\isaliteral{3F}{\isacharquery}}Q} are distinct bound variables. |
|
180 |
|
181 If the left-hand side is not a higher-order pattern, all is not lost. |
|
182 The simplifier will still try to apply the rule provided it |
|
183 matches directly: without much $\lambda$-calculus hocus |
|
184 pocus. For example, \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ {\isaliteral{3F}{\isacharquery}}f{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ True} rewrites |
|
185 \isa{g\ a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ g} to \isa{True}, but will fail to match |
|
186 \isa{g{\isaliteral{28}{\isacharparenleft}}h\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ g{\isaliteral{28}{\isacharparenleft}}h\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}. However, you can |
|
187 eliminate the offending subterms --- those that are not patterns --- |
|
188 by adding new variables and conditions. |
|
189 In our example, we eliminate \isa{{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}x} and obtain |
|
190 \isa{{\isaliteral{3F}{\isacharquery}}y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ {\isaliteral{3F}{\isacharquery}}f{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ True}, which is fine |
|
191 as a conditional rewrite rule since conditions can be arbitrary |
|
192 terms. However, this trick is not a panacea because the newly |
|
193 introduced conditions may be hard to solve. |
|
194 |
|
195 There is no restriction on the form of the right-hand |
|
196 sides. They may not contain extraneous term or type variables, though.% |
|
197 \end{isamarkuptext}% |
|
198 \isamarkuptrue% |
|
199 % |
|
200 \isamarkupsubsubsection{The Preprocessor% |
|
201 } |
|
202 \isamarkuptrue% |
|
203 % |
|
204 \begin{isamarkuptext}% |
|
205 \label{sec:simp-preprocessor} |
|
206 When a theorem is declared a simplification rule, it need not be a |
|
207 conditional equation already. The simplifier will turn it into a set of |
|
208 conditional equations automatically. For example, \isa{f\ x\ {\isaliteral{3D}{\isacharequal}}\ g\ x\ {\isaliteral{5C3C616E643E}{\isasymand}}\ h\ x\ {\isaliteral{3D}{\isacharequal}}\ k\ x} becomes the two separate |
|
209 simplification rules \isa{f\ x\ {\isaliteral{3D}{\isacharequal}}\ g\ x} and \isa{h\ x\ {\isaliteral{3D}{\isacharequal}}\ k\ x}. In |
|
210 general, the input theorem is converted as follows: |
|
211 \begin{eqnarray} |
|
212 \neg P &\mapsto& P = \hbox{\isa{False}} \nonumber\\ |
|
213 P \longrightarrow Q &\mapsto& P \Longrightarrow Q \nonumber\\ |
|
214 P \land Q &\mapsto& P,\ Q \nonumber\\ |
|
215 \forall x.~P~x &\mapsto& P~\Var{x}\nonumber\\ |
|
216 \forall x \in A.\ P~x &\mapsto& \Var{x} \in A \Longrightarrow P~\Var{x} \nonumber\\ |
|
217 \isa{if}\ P\ \isa{then}\ Q\ \isa{else}\ R &\mapsto& |
|
218 P \Longrightarrow Q,\ \neg P \Longrightarrow R \nonumber |
|
219 \end{eqnarray} |
|
220 Once this conversion process is finished, all remaining non-equations |
|
221 $P$ are turned into trivial equations $P =\isa{True}$. |
|
222 For example, the formula |
|
223 \begin{center}\isa{{\isaliteral{28}{\isacharparenleft}}p\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ t\ {\isaliteral{3D}{\isacharequal}}\ u\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ r{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ s}\end{center} |
|
224 is converted into the three rules |
|
225 \begin{center} |
|
226 \isa{p\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ t\ {\isaliteral{3D}{\isacharequal}}\ u},\quad \isa{p\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ r\ {\isaliteral{3D}{\isacharequal}}\ False},\quad \isa{s\ {\isaliteral{3D}{\isacharequal}}\ True}. |
|
227 \end{center} |
|
228 \index{simplification rule|)} |
|
229 \index{simplification|)}% |
|
230 \end{isamarkuptext}% |
|
231 \isamarkuptrue% |
|
232 % |
|
233 \isadelimtheory |
|
234 % |
|
235 \endisadelimtheory |
|
236 % |
|
237 \isatagtheory |
|
238 % |
|
239 \endisatagtheory |
|
240 {\isafoldtheory}% |
|
241 % |
|
242 \isadelimtheory |
|
243 % |
|
244 \endisadelimtheory |
|
245 \end{isabellebody}% |
|
246 %%% Local Variables: |
|
247 %%% mode: latex |
|
248 %%% TeX-master: "root" |
|
249 %%% End: |
|