doc-src/TutorialI/Types/document/Pairs.tex
author paulson
Fri, 21 Jan 2005 13:51:39 +0100
changeset 15446 b022b72ccc03
parent 14387 e96d5c42c4b0
child 15481 fc075ae929e4
permissions -rw-r--r--
auto update
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
     1
%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
     2
\begin{isabellebody}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
     3
\def\isabellecontext{Pairs}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
     4
\isamarkupfalse%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
     5
%
11428
332347b9b942 tidying the index
paulson
parents: 11277
diff changeset
     6
\isamarkupsection{Pairs and Tuples%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
     7
}
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
     8
\isamarkuptrue%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
     9
%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    10
\begin{isamarkuptext}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    11
\label{sec:products}
11428
332347b9b942 tidying the index
paulson
parents: 11277
diff changeset
    12
Ordered pairs were already introduced in \S\ref{sec:pairs}, but only with a minimal
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    13
repertoire of operations: pairing and the two projections \isa{fst} and
11149
e258b536a137 *** empty log message ***
nipkow
parents: 10950
diff changeset
    14
\isa{snd}. In any non-trivial application of pairs you will find that this
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    15
quickly leads to unreadable nests of projections. This
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    16
section introduces syntactic sugar to overcome this
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    17
problem: pattern matching with tuples.%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    18
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    19
\isamarkuptrue%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    20
%
10878
b254d5ad6dd4 auto update
paulson
parents: 10824
diff changeset
    21
\isamarkupsubsection{Pattern Matching with Tuples%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    22
}
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    23
\isamarkuptrue%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    24
%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    25
\begin{isamarkuptext}%
10878
b254d5ad6dd4 auto update
paulson
parents: 10824
diff changeset
    26
Tuples may be used as patterns in $\lambda$-abstractions,
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    27
for example \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharcomma}z{\isacharparenright}{\isachardot}x{\isacharplus}y{\isacharplus}z} and \isa{{\isasymlambda}{\isacharparenleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isacharcomma}z{\isacharparenright}{\isachardot}x{\isacharplus}y{\isacharplus}z}. In fact,
10878
b254d5ad6dd4 auto update
paulson
parents: 10824
diff changeset
    28
tuple patterns can be used in most variable binding constructs,
b254d5ad6dd4 auto update
paulson
parents: 10824
diff changeset
    29
and they can be nested. Here are
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    30
some typical examples:
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    31
\begin{quote}
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    32
\isa{let\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharequal}\ f\ z\ in\ {\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}}\\
12699
deae80045527 *** empty log message ***
nipkow
parents: 12627
diff changeset
    33
\isa{case\ xs\ of\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymRightarrow}\ {\isadigit{0}}\ {\isacharbar}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isacharhash}\ zs\ {\isasymRightarrow}\ x\ {\isacharplus}\ y}\\
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    34
\isa{{\isasymforall}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isasymin}A{\isachardot}\ x{\isacharequal}y}\\
10878
b254d5ad6dd4 auto update
paulson
parents: 10824
diff changeset
    35
\isa{{\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharcomma}z{\isacharparenright}{\isachardot}\ x{\isacharequal}z{\isacharbraceright}}\\
14387
e96d5c42c4b0 Polymorphic treatment of binary arithmetic using axclasses
paulson
parents: 13791
diff changeset
    36
\isa{{\isasymUnion}\isactrlbsub {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isasymin}A\isactrlesub \ {\isacharbraceleft}x\ {\isacharplus}\ y{\isacharbraceright}}
11149
e258b536a137 *** empty log message ***
nipkow
parents: 10950
diff changeset
    37
\end{quote}
10878
b254d5ad6dd4 auto update
paulson
parents: 10824
diff changeset
    38
The intuitive meanings of these expressions should be obvious.
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    39
Unfortunately, we need to know in more detail what the notation really stands
10878
b254d5ad6dd4 auto update
paulson
parents: 10824
diff changeset
    40
for once we have to reason about it.  Abstraction
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    41
over pairs and tuples is merely a convenient shorthand for a more complex
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    42
internal representation.  Thus the internal and external form of a term may
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    43
differ, which can affect proofs. If you want to avoid this complication,
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    44
stick to \isa{fst} and \isa{snd} and write \isa{{\isasymlambda}p{\isachardot}\ fst\ p\ {\isacharplus}\ snd\ p}
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    45
instead of \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharplus}y}.  These terms are distinct even though they
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    46
denote the same function.
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    47
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    48
Internally, \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ t} becomes \isa{split\ {\isacharparenleft}{\isasymlambda}x\ y{\isachardot}\ t{\isacharparenright}}, where
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    49
\cdx{split} is the uncurrying function of type \isa{{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}c} defined as
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    50
\begin{center}
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    51
\isa{split\ {\isasymequiv}\ {\isasymlambda}c\ p{\isachardot}\ c\ {\isacharparenleft}fst\ p{\isacharparenright}\ {\isacharparenleft}snd\ p{\isacharparenright}}
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    52
\hfill(\isa{split{\isacharunderscore}def})
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    53
\end{center}
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    54
Pattern matching in
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    55
other variable binding constructs is translated similarly. Thus we need to
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    56
understand how to reason about such constructs.%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    57
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    58
\isamarkuptrue%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    59
%
10878
b254d5ad6dd4 auto update
paulson
parents: 10824
diff changeset
    60
\isamarkupsubsection{Theorem Proving%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    61
}
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    62
\isamarkuptrue%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    63
%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    64
\begin{isamarkuptext}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    65
The most obvious approach is the brute force expansion of \isa{split}:%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    66
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    67
\isamarkuptrue%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    68
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}x{\isacharparenright}\ p\ {\isacharequal}\ fst\ p{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    69
\isamarkupfalse%
12815
wenzelm
parents: 12699
diff changeset
    70
\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    71
%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    72
\begin{isamarkuptext}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    73
This works well if rewriting with \isa{split{\isacharunderscore}def} finishes the
11149
e258b536a137 *** empty log message ***
nipkow
parents: 10950
diff changeset
    74
proof, as it does above.  But if it does not, you end up with exactly what
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    75
we are trying to avoid: nests of \isa{fst} and \isa{snd}. Thus this
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    76
approach is neither elegant nor very practical in large examples, although it
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    77
can be effective in small ones.
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    78
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    79
If we consider why this lemma presents a problem, 
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    80
we quickly realize that we need to replace the variable~\isa{p} by some pair \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}}.  Then both sides of the
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    81
equation would simplify to \isa{a} by the simplification rules
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    82
\isa{split\ c\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ c\ a\ b} and \isa{fst\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ a}.  
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    83
To reason about tuple patterns requires some way of
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    84
converting a variable of product type into a pair.
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    85
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    86
In case of a subterm of the form \isa{split\ f\ p} this is easy: the split
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    87
rule \isa{split{\isacharunderscore}split} replaces \isa{p} by a pair:%
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
    88
\index{*split (method)}%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    89
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    90
\isamarkuptrue%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    91
\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}y{\isacharparenright}\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    92
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    93
\isacommand{apply}{\isacharparenleft}split\ split{\isacharunderscore}split{\isacharparenright}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
    94
%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    95
\begin{isamarkuptxt}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    96
\begin{isabelle}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    97
\ {\isadigit{1}}{\isachardot}\ {\isasymforall}x\ y{\isachardot}\ p\ {\isacharequal}\ {\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}\ {\isasymlongrightarrow}\ y\ {\isacharequal}\ snd\ p%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
    98
\end{isabelle}
10824
4a212e635318 *** empty log message ***
nipkow
parents: 10654
diff changeset
    99
This subgoal is easily proved by simplification. Thus we could have combined
4a212e635318 *** empty log message ***
nipkow
parents: 10654
diff changeset
   100
simplification and splitting in one command that proves the goal outright:%
4a212e635318 *** empty log message ***
nipkow
parents: 10654
diff changeset
   101
\end{isamarkuptxt}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   102
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   103
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   104
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   105
\isacommand{by}{\isacharparenleft}simp\ split{\isacharcolon}\ split{\isacharunderscore}split{\isacharparenright}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   106
%
10824
4a212e635318 *** empty log message ***
nipkow
parents: 10654
diff changeset
   107
\begin{isamarkuptext}%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   108
Let us look at a second example:%
10824
4a212e635318 *** empty log message ***
nipkow
parents: 10654
diff changeset
   109
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   110
\isamarkuptrue%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   111
\isacommand{lemma}\ {\isachardoublequote}let\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ p\ in\ fst\ p\ {\isacharequal}\ x{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   112
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   113
\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ Let{\isacharunderscore}def{\isacharparenright}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   114
%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   115
\begin{isamarkuptxt}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   116
\begin{isabelle}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   117
\ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ fst\ p\ {\isacharequal}\ x{\isacharparenright}\ p%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   118
\end{isabelle}
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   119
A paired \isa{let} reduces to a paired $\lambda$-abstraction, which
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   120
can be split as above. The same is true for paired set comprehension:%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   121
\end{isamarkuptxt}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   122
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   123
\isamarkupfalse%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   124
\isacommand{lemma}\ {\isachardoublequote}p\ {\isasymin}\ {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y{\isacharbraceright}\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   125
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   126
\isacommand{apply}\ simp\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   127
%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   128
\begin{isamarkuptxt}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   129
\begin{isabelle}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   130
\ {\isadigit{1}}{\isachardot}\ split\ op\ {\isacharequal}\ p\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   131
\end{isabelle}
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   132
Again, simplification produces a term suitable for \isa{split{\isacharunderscore}split}
11277
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11161
diff changeset
   133
as above. If you are worried about the strange form of the premise:
15446
b022b72ccc03 auto update
paulson
parents: 14387
diff changeset
   134
\isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isachardot}\ x\ {\isacharequal}\ y} is short for \isa{{\isasymlambda}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y}.
11277
a2bff98d6e5d *** empty log message ***
nipkow
parents: 11161
diff changeset
   135
The same proof procedure works for%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   136
\end{isamarkuptxt}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   137
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   138
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   139
\isacommand{lemma}\ {\isachardoublequote}p\ {\isasymin}\ {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y{\isacharbraceright}\ {\isasymLongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   140
%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   141
\begin{isamarkuptxt}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   142
\noindent
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   143
except that we now have to use \isa{split{\isacharunderscore}split{\isacharunderscore}asm}, because
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   144
\isa{split} occurs in the assumptions.
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   145
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   146
However, splitting \isa{split} is not always a solution, as no \isa{split}
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   147
may be present in the goal. Consider the following function:%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   148
\end{isamarkuptxt}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   149
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   150
\isamarkupfalse%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   151
\isacommand{consts}\ swap\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymtimes}\ {\isacharprime}a{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   152
\isamarkupfalse%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   153
\isacommand{primrec}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   154
\ \ {\isachardoublequote}swap\ {\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}y{\isacharcomma}x{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   155
%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   156
\begin{isamarkuptext}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   157
\noindent
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   158
Note that the above \isacommand{primrec} definition is admissible
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   159
because \isa{{\isasymtimes}} is a datatype. When we now try to prove%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   160
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   161
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   162
\isacommand{lemma}\ {\isachardoublequote}swap{\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ p{\isachardoublequote}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   163
%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   164
\begin{isamarkuptxt}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   165
\noindent
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   166
simplification will do nothing, because the defining equation for \isa{swap}
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   167
expects a pair. Again, we need to turn \isa{p} into a pair first, but this
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   168
time there is no \isa{split} in sight. In this case the only thing we can do
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   169
is to split the term by hand:%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   170
\end{isamarkuptxt}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   171
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   172
\isacommand{apply}{\isacharparenleft}case{\isacharunderscore}tac\ p{\isacharparenright}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   173
%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   174
\begin{isamarkuptxt}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   175
\noindent
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   176
\begin{isabelle}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   177
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ p\ {\isacharequal}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isasymLongrightarrow}\ swap\ {\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ p%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   178
\end{isabelle}
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   179
Again, \methdx{case_tac} is applicable because \isa{{\isasymtimes}} is a datatype.
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   180
The subgoal is easily proved by \isa{simp}.
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   181
10824
4a212e635318 *** empty log message ***
nipkow
parents: 10654
diff changeset
   182
Splitting by \isa{case{\isacharunderscore}tac} also solves the previous examples and may thus
4a212e635318 *** empty log message ***
nipkow
parents: 10654
diff changeset
   183
appear preferable to the more arcane methods introduced first. However, see
4a212e635318 *** empty log message ***
nipkow
parents: 10654
diff changeset
   184
the warning about \isa{case{\isacharunderscore}tac} in \S\ref{sec:struct-ind-case}.
4a212e635318 *** empty log message ***
nipkow
parents: 10654
diff changeset
   185
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   186
In case the term to be split is a quantified variable, there are more options.
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   187
You can split \emph{all} \isa{{\isasymAnd}}-quantified variables in a goal
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   188
with the rewrite rule \isa{split{\isacharunderscore}paired{\isacharunderscore}all}:%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   189
\end{isamarkuptxt}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   190
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   191
\isamarkupfalse%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   192
\isacommand{lemma}\ {\isachardoublequote}{\isasymAnd}p\ q{\isachardot}\ swap{\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ q\ {\isasymlongrightarrow}\ p\ {\isacharequal}\ q{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   193
\isamarkupfalse%
12627
08eee994bf99 updated;
wenzelm
parents: 11866
diff changeset
   194
\isacommand{apply}{\isacharparenleft}simp\ only{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   195
%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   196
\begin{isamarkuptxt}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   197
\noindent
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   198
\begin{isabelle}%
10577
b9c290f0343d auto update
paulson
parents: 10560
diff changeset
   199
\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b\ aa\ ba{\isachardot}\isanewline
10950
aa788fcb75a5 updated;
wenzelm
parents: 10878
diff changeset
   200
\isaindent{\ {\isadigit{1}}{\isachardot}\ \ \ \ }swap\ {\isacharparenleft}swap\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}\ {\isasymlongrightarrow}\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}aa{\isacharcomma}\ ba{\isacharparenright}%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   201
\end{isabelle}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   202
\end{isamarkuptxt}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   203
\isamarkuptrue%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   204
\isacommand{apply}\ simp\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   205
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   206
\isacommand{done}\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   207
%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   208
\begin{isamarkuptext}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   209
\noindent
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   210
Note that we have intentionally included only \isa{split{\isacharunderscore}paired{\isacharunderscore}all}
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   211
in the first simplification step, and then we simplify again. 
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   212
This time the reason was not merely
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   213
pedagogical:
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   214
\isa{split{\isacharunderscore}paired{\isacharunderscore}all} may interfere with other functions
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   215
of the simplifier.
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   216
The following command could fail (here it does not)
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   217
where two separate \isa{simp} applications succeed.%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   218
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   219
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   220
\isamarkupfalse%
13791
3b6ff7ceaf27 *** empty log message ***
nipkow
parents: 13778
diff changeset
   221
\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   222
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   223
%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   224
\begin{isamarkuptext}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   225
\noindent
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   226
Finally, the simplifier automatically splits all \isa{{\isasymforall}} and
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   227
\isa{{\isasymexists}}-quantified variables:%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   228
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   229
\isamarkuptrue%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   230
\isacommand{lemma}\ {\isachardoublequote}{\isasymforall}p{\isachardot}\ {\isasymexists}q{\isachardot}\ swap\ p\ {\isacharequal}\ swap\ q{\isachardoublequote}\isanewline
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   231
\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   232
\isacommand{by}\ simp\isamarkupfalse%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   233
%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   234
\begin{isamarkuptext}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   235
\noindent
11494
23a118849801 revisions and indexing
paulson
parents: 11428
diff changeset
   236
To turn off this automatic splitting, just disable the
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   237
responsible simplification rules:
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   238
\begin{center}
10654
458068404143 *** empty log message ***
nipkow
parents: 10608
diff changeset
   239
\isa{{\isacharparenleft}{\isasymforall}x{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymforall}a\ b{\isachardot}\ P\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}}
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   240
\hfill
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   241
(\isa{split{\isacharunderscore}paired{\isacharunderscore}All})\\
10654
458068404143 *** empty log message ***
nipkow
parents: 10608
diff changeset
   242
\isa{{\isacharparenleft}{\isasymexists}x{\isachardot}\ P\ x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymexists}a\ b{\isachardot}\ P\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}{\isacharparenright}}
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   243
\hfill
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   244
(\isa{split{\isacharunderscore}paired{\isacharunderscore}Ex})
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   245
\end{center}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   246
\end{isamarkuptext}%
11866
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   247
\isamarkuptrue%
fbd097aec213 updated;
wenzelm
parents: 11708
diff changeset
   248
\isamarkupfalse%
10560
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   249
\end{isabellebody}%
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   250
%%% Local Variables:
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   251
%%% mode: latex
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   252
%%% TeX-master: "root"
f4da791d4850 *** empty log message ***
nipkow
parents:
diff changeset
   253
%%% End: