author wenzelm Tue, 06 Jun 2006 16:07:10 +0200 changeset 19792 e8e3da6d3ff7 parent 19791 ab326de16ad5 child 19793 14fdd2a3d117
quoted "if";
 doc-src/TutorialI/Advanced/simp.thy file | annotate | diff | comparison | revisions doc-src/TutorialI/Misc/simp.thy file | annotate | diff | comparison | revisions doc-src/TutorialI/Recdef/simplification.thy file | annotate | diff | comparison | revisions doc-src/ZF/If.thy file | annotate | diff | comparison | revisions
--- a/doc-src/TutorialI/Advanced/simp.thy	Tue Jun 06 15:02:55 2006 +0200
+++ b/doc-src/TutorialI/Advanced/simp.thy	Tue Jun 06 16:07:10 2006 +0200
@@ -42,7 +42,7 @@
Only the first argument is simplified; the others remain unchanged.
This makes simplification much faster and is faithful to the evaluation
strategy in programming languages, which is why this is the default
-congruence rule for @{text if}. Analogous rules control the evaluation of
+congruence rule for @{text "if"}. Analogous rules control the evaluation of
@{text case} expressions.

You can declare your own congruence rules with the attribute \attrdx{cong},
@@ -170,7 +170,7 @@
P \land Q &\mapsto& P,\ Q \nonumber\\
\forall x.~P~x &\mapsto& P~\Var{x}\nonumber\\
\forall x \in A.\ P~x &\mapsto& \Var{x} \in A \Longrightarrow P~\Var{x} \nonumber\\
-@{text if}\ P\ @{text then}\ Q\ @{text else}\ R &\mapsto&
+@{text "if"}\ P\ @{text then}\ Q\ @{text else}\ R &\mapsto&
P \Longrightarrow Q,\ \neg P \Longrightarrow R \nonumber
\end{eqnarray}
Once this conversion process is finished, all remaining non-equations
--- a/doc-src/TutorialI/Misc/simp.thy	Tue Jun 06 15:02:55 2006 +0200
+++ b/doc-src/TutorialI/Misc/simp.thy	Tue Jun 06 16:07:10 2006 +0200
@@ -330,7 +330,7 @@
text{*
Polished proofs typically perform splitting within @{text simp} rather than
invoking the @{text split} method.  However, if a goal contains
-several @{text if} and @{text case} expressions,
+several @{text "if"} and @{text case} expressions,
the @{text split} method can be
helpful in selectively exploring the effects of splitting.

--- a/doc-src/TutorialI/Recdef/simplification.thy	Tue Jun 06 15:02:55 2006 +0200
+++ b/doc-src/TutorialI/Recdef/simplification.thy	Tue Jun 06 16:07:10 2006 +0200
@@ -7,7 +7,7 @@
recursion equations become simplification rules, just as with
\isacommand{primrec}. In most cases this works fine, but there is a subtle
problem that must be mentioned: simplification may not
-terminate because of automatic splitting of @{text if}.
+terminate because of automatic splitting of @{text "if"}.
\index{*if expressions!splitting of}
Let us look at an example:
*}
@@ -26,7 +26,7 @@
the recursive call inside the @{text else} branch, which is why programming
languages and our simplifier don't do that. Unfortunately the simplifier does
something else that leads to the same problem: it splits
-each @{text if}-expression unless its
+each @{text "if"}-expression unless its
condition simplifies to @{term True} or @{term False}.  For
example, simplification reduces
@{term[display]"gcd(m,n) = k"}
@@ -35,7 +35,7 @@
where the condition cannot be reduced further, and splitting leads to
@{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
-an @{text if}, it is unfolded again, which leads to an infinite chain of
+an @{text "if"}, it is unfolded again, which leads to an infinite chain of
simplification steps. Fortunately, this problem can be avoided in many
different ways.

@@ -43,10 +43,10 @@
@{thm[source]split_if},
as shown in \S\ref{sec:AutoCaseSplits}.  However, we do not recommend this
approach: you will often have to invoke the rule explicitly when
-@{text if} is involved.
+@{text "if"} is involved.

If possible, the definition should be given by pattern matching on the left
-rather than @{text if} on the right. In the case of @{term gcd} the
+rather than @{text "if"} on the right. In the case of @{term gcd} the
following alternative definition suggests itself:
*}

@@ -61,7 +61,7 @@
@{prop"n ~= (0::nat)"}.  Unfortunately, in general the case distinction
may not be expressible by pattern matching.

-A simple alternative is to replace @{text if} by @{text case},
+A simple alternative is to replace @{text "if"} by @{text case},
which is also available for @{typ bool} and is not split automatically:
*}

@@ -88,7 +88,7 @@

text{*\noindent
Simplification terminates for these proofs because the condition of the @{text
-if} simplifies to @{term True} or @{term False}.
+"if"} simplifies to @{term True} or @{term False}.
Now we can disable the original simplification rule:
*}

--- a/doc-src/ZF/If.thy	Tue Jun 06 15:02:55 2006 +0200
+++ b/doc-src/ZF/If.thy	Tue Jun 06 16:07:10 2006 +0200
@@ -9,8 +9,8 @@
theory If imports FOL begin

constdefs
-  if :: "[o,o,o]=>o"
-   "if(P,Q,R) == P&Q | ~P&R"
+  "if" :: "[o,o,o]=>o"
+  "if(P,Q,R) == P&Q | ~P&R"

lemma ifI:
"[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)"