summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Tue, 06 Jun 2006 16:07:10 +0200 | |

changeset 19792 | e8e3da6d3ff7 |

parent 19791 | ab326de16ad5 |

child 19793 | 14fdd2a3d117 |

quoted "if";

--- 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)"