--- a/doc-src/IsarOverview/Isar/document/Logic.tex Sun Nov 07 23:32:26 2010 +0100
+++ b/doc-src/IsarOverview/Isar/document/Logic.tex Mon Nov 08 00:00:47 2010 +0100
@@ -33,7 +33,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ {\isasymlongrightarrow}\ A{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -41,12 +41,12 @@
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
-\ {\isacharparenleft}rule\ impI{\isacharparenright}\isanewline
+\ {\isaliteral{28}{\isacharparenleft}}rule\ impI{\isaliteral{29}{\isacharparenright}}\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
-\ a{\isacharcolon}\ {\isachardoublequoteopen}A{\isachardoublequoteclose}\isanewline
+\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}A{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-{\isacharparenleft}rule\ a{\isacharparenright}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}rule\ a{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
@@ -59,9 +59,9 @@
\begin{isamarkuptext}%
\noindent
The operational reading: the \isakeyword{assume}-\isakeyword{show}
-block proves \isa{A\ {\isasymLongrightarrow}\ A} (\isa{a} is a degenerate rule (no
+block proves \isa{A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A} (\isa{a} is a degenerate rule (no
assumptions) that proves \isa{A} outright), which rule
-\isa{impI} (\isa{{\isacharparenleft}{\isacharquery}P\ {\isasymLongrightarrow}\ {\isacharquery}Q{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isasymlongrightarrow}\ {\isacharquery}Q}) turns into the desired \isa{A\ {\isasymlongrightarrow}\ A}. However, this text is much too detailed for comfort. Therefore
+\isa{impI} (\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q}) turns into the desired \isa{A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ A}. However, this text is much too detailed for comfort. Therefore
Isar implements the following principle: \begin{quote}\em Command
\isakeyword{proof} automatically tries to select an introduction rule
based on the goal and a predefined list of rules. \end{quote} Here
@@ -69,7 +69,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ {\isasymlongrightarrow}\ A{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -79,10 +79,10 @@
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
-\ a{\isacharcolon}\ A\isanewline
+\ a{\isaliteral{3A}{\isacharcolon}}\ A\isanewline
\ \ \isacommand{show}\isamarkupfalse%
\ A\ \isacommand{by}\isamarkupfalse%
-{\isacharparenleft}rule\ a{\isacharparenright}\isanewline
+{\isaliteral{28}{\isacharparenleft}}rule\ a{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
@@ -103,7 +103,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ {\isasymlongrightarrow}\ A{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -113,10 +113,10 @@
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
-\ a{\isacharcolon}\ {\isachardoublequoteopen}A{\isachardoublequoteclose}\isanewline
+\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ a\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}A{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
@@ -134,7 +134,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ {\isasymlongrightarrow}\ A\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -144,11 +144,11 @@
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
-\ a{\isacharcolon}\ {\isachardoublequoteopen}A{\isachardoublequoteclose}\isanewline
+\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ a\ \isakeyword{and}\ a\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ {\isasymand}\ A{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
-{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}rule\ conjI{\isaliteral{29}{\isacharparenright}}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
@@ -159,15 +159,15 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-\noindent Rule \isa{conjI} is of course \isa{{\isasymlbrakk}{\isacharquery}P{\isacharsemicolon}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isasymand}\ {\isacharquery}Q}.
+\noindent Rule \isa{conjI} is of course \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{3F}{\isacharquery}}P{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{3F}{\isacharquery}}Q{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}Q}.
-Proofs of the form \isakeyword{by}\isa{{\isacharparenleft}rule}~\emph{name}\isa{{\isacharparenright}}
+Proofs of the form \isakeyword{by}\isa{{\isaliteral{28}{\isacharparenleft}}rule}~\emph{name}\isa{{\isaliteral{29}{\isacharparenright}}}
can be abbreviated to ``..'' if \emph{name} refers to one of the
predefined introduction rules (or elimination rules, see below):%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ {\isasymlongrightarrow}\ A\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -177,10 +177,10 @@
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
-\ a{\isacharcolon}\ {\isachardoublequoteopen}A{\isachardoublequoteclose}\isanewline
+\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ a\ \isakeyword{and}\ a\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ {\isasymand}\ A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
@@ -205,14 +205,14 @@
\begin{isamarkuptext}%
A typical elimination rule is \isa{conjE}, $\land$-elimination:
\begin{isabelle}%
-\ \ \ \ \ {\isasymlbrakk}{\isacharquery}P\ {\isasymand}\ {\isacharquery}Q{\isacharsemicolon}\ {\isasymlbrakk}{\isacharquery}P{\isacharsemicolon}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R%
+\ \ \ \ \ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}Q{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{3F}{\isacharquery}}P{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{3F}{\isacharquery}}Q{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}R{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}R%
\end{isabelle} In the following proof it is applied
by hand, after its first (\emph{major}) premise has been eliminated via
-\isa{{\isacharbrackleft}OF\ ab{\isacharbrackright}}:%
+\isa{{\isaliteral{5B}{\isacharbrackleft}}OF\ ab{\isaliteral{5D}{\isacharbrackright}}}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -222,19 +222,19 @@
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
-\ ab{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\isanewline
+\ ab{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}B\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
-\ {\isacharparenleft}rule\ conjE{\isacharbrackleft}OF\ ab{\isacharbrackright}{\isacharparenright}\ \ %
-\isamarkupcmt{\isa{conjE{\isacharbrackleft}OF\ ab{\isacharbrackright}}: \isa{{\isacharparenleft}{\isasymlbrakk}A{\isacharsemicolon}\ B{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharquery}R}%
+\ {\isaliteral{28}{\isacharparenleft}}rule\ conjE{\isaliteral{5B}{\isacharbrackleft}}OF\ ab{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}\ \ %
+\isamarkupcmt{\isa{conjE{\isaliteral{5B}{\isacharbrackleft}}OF\ ab{\isaliteral{5D}{\isacharbrackright}}}: \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}A{\isaliteral{3B}{\isacharsemicolon}}\ B{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}R}%
}
\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
-\ a{\isacharcolon}\ {\isachardoublequoteopen}A{\isachardoublequoteclose}\ \isakeyword{and}\ b{\isacharcolon}\ {\isachardoublequoteopen}B{\isachardoublequoteclose}\isanewline
+\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ b{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{from}\isamarkupfalse%
\ b\ \isakeyword{and}\ a\ \isacommand{show}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
@@ -248,7 +248,7 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-\noindent Note that the term \isa{{\isacharquery}thesis} always stands for the
+\noindent Note that the term \isa{{\isaliteral{3F}{\isacharquery}}thesis} always stands for the
``current goal'', i.e.\ the enclosing \isakeyword{show} (or
\isakeyword{have}) statement.
@@ -270,7 +270,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -280,17 +280,17 @@
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
-\ ab{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\isanewline
+\ ab{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ ab\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}B\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
-\ a{\isacharcolon}\ {\isachardoublequoteopen}A{\isachardoublequoteclose}\ \isakeyword{and}\ b{\isacharcolon}\ {\isachardoublequoteopen}B{\isachardoublequoteclose}\isanewline
+\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ b{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{from}\isamarkupfalse%
\ b\ \isakeyword{and}\ a\ \isacommand{show}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
@@ -315,7 +315,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -325,17 +325,17 @@
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ this\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}B\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}B{\isachardoublequoteclose}\ {\isachardoublequoteopen}A{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{from}\isamarkupfalse%
\ this\ \isacommand{show}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
@@ -361,7 +361,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -371,18 +371,18 @@
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
-\ ab{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\isanewline
+\ ab{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ ab\ \isacommand{have}\isamarkupfalse%
-\ a{\isacharcolon}\ {\isachardoublequoteopen}A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ ab\ \isacommand{have}\isamarkupfalse%
-\ b{\isacharcolon}\ {\isachardoublequoteopen}B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ b{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ b\ a\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}B\ {\isasymand}\ A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
@@ -404,17 +404,17 @@
\begin{itemize}
\item
Method \isa{rule} can be given a list of rules, in which case
-\isa{{\isacharparenleft}rule}~\textit{rules}\isa{{\isacharparenright}} applies the first matching
+\isa{{\isaliteral{28}{\isacharparenleft}}rule}~\textit{rules}\isa{{\isaliteral{29}{\isacharparenright}}} applies the first matching
rule in the list \textit{rules}.
\item Command \isakeyword{from} can be
followed by any number of facts. Given \isakeyword{from}~\isa{f}$_1$~\dots~\isa{f}$_n$, the proof step
-\isa{{\isacharparenleft}rule}~\textit{rules}\isa{{\isacharparenright}} following a \isakeyword{have}
+\isa{{\isaliteral{28}{\isacharparenleft}}rule}~\textit{rules}\isa{{\isaliteral{29}{\isacharparenright}}} following a \isakeyword{have}
or \isakeyword{show} searches \textit{rules} for a rule whose first
$n$ premises can be proved by \isa{f}$_1$~\dots~\isa{f}$_n$ in the
given order.
\item ``..'' is short for
-\isa{by{\isacharparenleft}rule}~\textit{elim-rules intro-rules}\isa{{\isacharparenright}}\footnote{or
-merely \isa{{\isacharparenleft}rule}~\textit{intro-rules}\isa{{\isacharparenright}} if there are no facts
+\isa{by{\isaliteral{28}{\isacharparenleft}}rule}~\textit{elim-rules intro-rules}\isa{{\isaliteral{29}{\isacharparenright}}}\footnote{or
+merely \isa{{\isaliteral{28}{\isacharparenleft}}rule}~\textit{intro-rules}\isa{{\isaliteral{29}{\isacharparenright}}} if there are no facts
fed into the proof}, where \textit{elim-rules} and \textit{intro-rules}
are the predefined elimination and introduction rule. Thus
elimination rules are tried first (if there are incoming facts).
@@ -427,7 +427,7 @@
\isakeyword{from}~\isa{b\ a}.
A plain \isakeyword{proof} with no argument is short for
-\isakeyword{proof}~\isa{{\isacharparenleft}rule}~\textit{elim-rules intro-rules}\isa{{\isacharparenright}}\footnotemark[1].
+\isakeyword{proof}~\isa{{\isaliteral{28}{\isacharparenleft}}rule}~\textit{elim-rules intro-rules}\isa{{\isaliteral{29}{\isacharparenright}}}\footnotemark[1].
This means that the matching rule is selected by the incoming facts and the goal exactly as just explained.
Although we have only seen a few introduction and elimination rules so
@@ -437,7 +437,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ {\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -447,50 +447,50 @@
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
-\ n{\isacharcolon}\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ n{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
-\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline
+\ {\isaliteral{28}{\isacharparenleft}}rule\ ccontr{\isaliteral{29}{\isacharparenright}}\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
-\ nn{\isacharcolon}\ {\isachardoublequoteopen}{\isasymnot}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ nn{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymnot}\ A{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
-\ a{\isacharcolon}\ {\isachardoublequoteopen}A{\isachardoublequoteclose}\isanewline
+\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymnot}\ B{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
-\ b{\isacharcolon}\ {\isachardoublequoteopen}B{\isachardoublequoteclose}\isanewline
+\ b{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \ \ \ \ \isacommand{from}\isamarkupfalse%
\ a\ \isakeyword{and}\ b\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
\ n\ \isacommand{show}\isamarkupfalse%
-\ False\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ False\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
\ nn\ \isacommand{show}\isamarkupfalse%
-\ False\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ False\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{hence}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{with}\isamarkupfalse%
\ nn\ \isacommand{show}\isamarkupfalse%
-\ False\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ False\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
@@ -506,7 +506,7 @@
\begin{isamarkuptext}%
\noindent
Rule \isa{ccontr} (``classical contradiction'') is
-\isa{{\isacharparenleft}{\isasymnot}\ P\ {\isasymLongrightarrow}\ False{\isacharparenright}\ {\isasymLongrightarrow}\ P}.
+\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ False{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P}.
Apart from demonstrating the strangeness of classical
arguments by contradiction, this example also introduces two new
abbreviations:
@@ -526,11 +526,11 @@
%
\begin{isamarkuptext}%
So far our examples have been a bit unnatural: normally we want to
-prove rules expressed with \isa{{\isasymLongrightarrow}}, not \isa{{\isasymlongrightarrow}}. Here is an example:%
+prove rules expressed with \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}}, not \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}. Here is an example:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -540,14 +540,14 @@
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\ \isacommand{thus}\isamarkupfalse%
-\ {\isachardoublequoteopen}B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{thus}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\ \isacommand{thus}\isamarkupfalse%
-\ {\isachardoublequoteopen}A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{thus}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
@@ -560,12 +560,12 @@
%
\begin{isamarkuptext}%
\noindent The \isakeyword{proof} always works on the conclusion,
-\isa{B\ {\isasymand}\ A} in our case, thus selecting $\land$-introduction. Hence
+\isa{B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A} in our case, thus selecting $\land$-introduction. Hence
we must show \isa{B} and \isa{A}; both are proved by
$\land$-elimination and the proofs are separated by \isakeyword{next}:
\begin{description}
\item[\isakeyword{next}] deals with multiple subgoals. For example,
-when showing \isa{A\ {\isasymand}\ B} we need to show both \isa{A} and \isa{B}. Each subgoal is proved separately, in \emph{any} order. The
+when showing \isa{A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B} we need to show both \isa{A} and \isa{B}. Each subgoal is proved separately, in \emph{any} order. The
individual proofs are separated by \isakeyword{next}. \footnote{Each
\isakeyword{show} must prove one of the pending subgoals. If a
\isakeyword{show} matches multiple subgoals, e.g.\ if the subgoals
@@ -585,8 +585,8 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B\ {\isasymLongrightarrow}\ large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequoteclose}\isanewline
-\ \ \ \ \ \ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}AB\ {\isasymLongrightarrow}\ {\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}large{\isaliteral{5F}{\isacharunderscore}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ large{\isaliteral{5F}{\isacharunderscore}}B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ large{\isaliteral{5F}{\isacharunderscore}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ large{\isaliteral{5F}{\isacharunderscore}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{is}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}AB\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}A{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
%
\isadelimproof
%
@@ -596,14 +596,14 @@
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharquery}AB{\isachardoublequoteclose}\ \isacommand{thus}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharquery}B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}AB{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{thus}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharquery}AB{\isachardoublequoteclose}\ \isacommand{thus}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharquery}A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}AB{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{thus}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
@@ -616,8 +616,8 @@
%
\begin{isamarkuptext}%
\noindent Any formula may be followed by
-\isa{{\isacharparenleft}}\isakeyword{is}~\emph{pattern}\isa{{\isacharparenright}} which causes the pattern
-to be matched against the formula, instantiating the \isa{{\isacharquery}}-variables in
+\isa{{\isaliteral{28}{\isacharparenleft}}}\isakeyword{is}~\emph{pattern}\isa{{\isaliteral{29}{\isacharparenright}}} which causes the pattern
+to be matched against the formula, instantiating the \isa{{\isaliteral{3F}{\isacharquery}}}-variables in
the pattern. Subsequent uses of these variables in other terms causes
them to be replaced by the terms they stand for.
@@ -627,8 +627,8 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ \isakeyword{assumes}\ ab{\isacharcolon}\ {\isachardoublequoteopen}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{shows}\ {\isachardoublequoteopen}large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\ \isakeyword{assumes}\ ab{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}large{\isaliteral{5F}{\isacharunderscore}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ large{\isaliteral{5F}{\isacharunderscore}}B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}large{\isaliteral{5F}{\isacharunderscore}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ large{\isaliteral{5F}{\isacharunderscore}}A{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{is}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}A{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
%
\isadelimproof
%
@@ -639,13 +639,13 @@
\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ ab\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharquery}B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ ab\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharquery}A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
@@ -657,7 +657,7 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-\noindent Note the difference between \isa{{\isacharquery}AB}, a term, and
+\noindent Note the difference between \isa{{\isaliteral{3F}{\isacharquery}}AB}, a term, and
\isa{ab}, a fact.
Finally we want to start the proof with $\land$-elimination so we
@@ -666,8 +666,8 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ \isakeyword{assumes}\ ab{\isacharcolon}\ {\isachardoublequoteopen}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{shows}\ {\isachardoublequoteopen}large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequoteopen}{\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequoteclose}{\isacharparenright}\isanewline
+\ \isakeyword{assumes}\ ab{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}large{\isaliteral{5F}{\isacharunderscore}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ large{\isaliteral{5F}{\isacharunderscore}}B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}large{\isaliteral{5F}{\isacharunderscore}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ large{\isaliteral{5F}{\isacharunderscore}}A{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{is}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}A{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
%
\isadelimproof
%
@@ -679,8 +679,8 @@
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharquery}B{\isachardoublequoteclose}\ {\isachardoublequoteopen}{\isacharquery}A{\isachardoublequoteclose}\ \isacommand{thus}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}B{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{thus}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
@@ -704,14 +704,14 @@
\end{center}
Sometimes it is necessary to suppress the implicit application of rules in a
-\isakeyword{proof}. For example \isakeyword{show(s)}~\isa{{\isachardoublequote}P\ {\isasymor}\ Q{\isachardoublequote}}
+\isakeyword{proof}. For example \isakeyword{show(s)}~\isa{{\isaliteral{22}{\isachardoublequote}}P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequote}}}
would trigger $\lor$-introduction, requiring us to prove \isa{P}, which may
not be what we had in mind.
-A simple ``\isa{{\isacharminus}}'' prevents this \emph{faux pas}:%
+A simple ``\isa{{\isaliteral{2D}{\isacharminus}}}'' prevents this \emph{faux pas}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ \isakeyword{assumes}\ ab{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymor}\ B{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}B\ {\isasymor}\ A{\isachardoublequoteclose}\isanewline
+\ \isakeyword{assumes}\ ab{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C6F723E}{\isasymor}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -719,21 +719,21 @@
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
+\ {\isaliteral{2D}{\isacharminus}}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ ab\ \isacommand{show}\isamarkupfalse%
-\ {\isacharquery}thesis\isanewline
+\ {\isaliteral{3F}{\isacharquery}}thesis\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ A\ \isacommand{thus}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
\ B\ \isacommand{thus}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
@@ -747,12 +747,12 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-\noindent Alternatively one can feed \isa{A\ {\isasymor}\ B} directly
+\noindent Alternatively one can feed \isa{A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B} directly
into the proof, thus triggering the elimination rule:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ \isakeyword{assumes}\ ab{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymor}\ B{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}B\ {\isasymor}\ A{\isachardoublequoteclose}\isanewline
+\ \isakeyword{assumes}\ ab{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C6F723E}{\isasymor}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -765,13 +765,13 @@
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ A\ \isacommand{thus}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\isacommand{next}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
\ B\ \isacommand{thus}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
@@ -791,14 +791,14 @@
Too many names can easily clutter a proof. We already learned
about \isa{this} as a means of avoiding explicit names. Another
handy device is to refer to a fact not by name but by contents: for
-example, writing \isa{{\isacharbackquote}A\ {\isasymor}\ B{\isacharbackquote}} (enclosing the formula in back quotes)
-refers to the fact \isa{A\ {\isasymor}\ B}
+example, writing \isa{{\isaliteral{60}{\isacharbackquote}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{60}{\isacharbackquote}}} (enclosing the formula in back quotes)
+refers to the fact \isa{A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B}
without the need to name it. Here is a simple example, a revised version
of the previous proof%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasymor}\ B{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}B\ {\isasymor}\ A{\isachardoublequoteclose}\isanewline
+\ \isakeyword{assumes}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C6F723E}{\isasymor}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -806,7 +806,7 @@
%
\isatagproof
\isacommand{using}\isamarkupfalse%
-\ {\isacharbackquoteopen}A\ {\isasymor}\ B{\isacharbackquoteclose}%
+\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{60}{\isacharbackquoteclose}}%
\endisatagproof
{\isafoldproof}%
%
@@ -823,12 +823,12 @@
it in the preceding proof text.
The assumptions of a lemma can also be referred to via their
-predefined name \isa{assms}. Hence the \isa{{\isacharbackquote}A\ {\isasymor}\ B{\isacharbackquote}} in the
+predefined name \isa{assms}. Hence the \isa{{\isaliteral{60}{\isacharbackquote}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{60}{\isacharbackquote}}} in the
previous proof can also be replaced by \isa{assms}. Note that \isa{assms} refers to the list of \emph{all} assumptions. To pick out a
-specific one, say the second, write \isa{assms{\isacharparenleft}{\isadigit{2}}{\isacharparenright}}.
+specific one, say the second, write \isa{assms{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}.
This indexing notation $name(.)$ works for any $name$ that stands for
-a list of facts, for example $f$\isa{{\isachardot}simps}, the equations of the
+a list of facts, for example $f$\isa{{\isaliteral{2E}{\isachardot}}simps}, the equations of the
recursively defined function $f$. You may also select sublists by writing
$name(2-3)$.
@@ -840,7 +840,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}B\ {\isasymand}\ A{\isachardoublequoteclose}\isanewline
+\ \isakeyword{assumes}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -848,20 +848,20 @@
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
+\ {\isaliteral{2D}{\isacharminus}}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
-\ {\isacharbackquoteopen}A\ {\isasymand}\ B{\isacharbackquoteclose}\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
\ \ \isacommand{from}\isamarkupfalse%
-\ {\isacharbackquoteopen}A\ {\isasymand}\ B{\isacharbackquoteclose}\ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{60}{\isacharbackquoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{have}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}B\ {\isasymand}\ A{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
@@ -882,15 +882,15 @@
\subsection{Predicate calculus}
Command \isakeyword{fix} introduces new local variables into a
-proof. The pair \isakeyword{fix}-\isakeyword{show} corresponds to \isa{{\isasymAnd}}
+proof. The pair \isakeyword{fix}-\isakeyword{show} corresponds to \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}}
(the universal quantifier at the
meta-level) just like \isakeyword{assume}-\isakeyword{show} corresponds to
-\isa{{\isasymLongrightarrow}}. Here is a sample proof, annotated with the rules that are
+\isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}}. Here is a sample proof, annotated with the rules that are
applied implicitly:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ \isakeyword{assumes}\ P{\isacharcolon}\ {\isachardoublequoteopen}{\isasymforall}x{\isachardot}\ P\ x{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}x{\isachardot}\ P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ \isakeyword{assumes}\ P{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -899,16 +899,16 @@
\isatagproof
\isacommand{proof}\isamarkupfalse%
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ %
-\isamarkupcmt{\isa{allI}: \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymforall}x{\isachardot}\ {\isacharquery}P\ x}%
+\isamarkupcmt{\isa{allI}: \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x}%
}
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ a\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ P\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}P{\isacharparenleft}f\ a{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}P{\isaliteral{28}{\isacharparenleft}}f\ a{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\ \ %
-\isamarkupcmt{\isa{allE}: \isa{{\isasymlbrakk}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x{\isacharsemicolon}\ {\isacharquery}P\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isacharquery}R{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R}%
+\isamarkupcmt{\isa{allE}: \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}R{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}R}%
}
\isanewline
\isacommand{qed}\isamarkupfalse%
@@ -925,11 +925,11 @@
variable \isa{a} instead of \isa{x} merely to show that the choice of
local names is irrelevant.
-Next we look at \isa{{\isasymexists}} which is a bit more tricky.%
+Next we look at \isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}} which is a bit more tricky.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ \isakeyword{assumes}\ Pf{\isacharcolon}\ {\isachardoublequoteopen}{\isasymexists}x{\isachardot}\ P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequoteclose}\isanewline
+\ \isakeyword{assumes}\ Pf{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}y{\isaliteral{2E}{\isachardot}}\ P\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -937,23 +937,23 @@
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
+\ {\isaliteral{2D}{\isacharminus}}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ Pf\ \isacommand{show}\isamarkupfalse%
-\ {\isacharquery}thesis\isanewline
+\ {\isaliteral{3F}{\isacharquery}}thesis\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\ \ \ \ \ \ \ \ \ \ \ \ \ \ %
-\isamarkupcmt{\isa{exE}: \isa{{\isasymlbrakk}{\isasymexists}x{\isachardot}\ {\isacharquery}P\ x{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q}%
+\isamarkupcmt{\isa{exE}: \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}Q}%
}
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}P{\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{thus}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\ \ %
-\isamarkupcmt{\isa{exI}: \isa{{\isacharquery}P\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isasymexists}x{\isachardot}\ {\isacharquery}P\ x}%
+\isamarkupcmt{\isa{exI}: \isa{{\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}P\ x}%
}
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
@@ -975,7 +975,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ \isakeyword{assumes}\ Pf{\isacharcolon}\ {\isachardoublequoteopen}{\isasymexists}x{\isachardot}\ P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequoteclose}\isanewline
+\ \isakeyword{assumes}\ Pf{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}y{\isaliteral{2E}{\isachardot}}\ P\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -983,13 +983,13 @@
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
+\ {\isaliteral{2D}{\isacharminus}}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ Pf\ \isacommand{obtain}\isamarkupfalse%
-\ x\ \isakeyword{where}\ {\isachardoublequoteopen}P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ x\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}P{\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}y{\isaliteral{2E}{\isachardot}}\ P\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
@@ -1012,7 +1012,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ \isakeyword{assumes}\ ex{\isacharcolon}\ {\isachardoublequoteopen}{\isasymexists}x{\isachardot}\ {\isasymforall}y{\isachardot}\ P\ x\ y{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymforall}y{\isachardot}\ {\isasymexists}x{\isachardot}\ P\ x\ y{\isachardoublequoteclose}\isanewline
+\ \isakeyword{assumes}\ ex{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ P\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -1025,13 +1025,13 @@
\ y\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ ex\ \isacommand{obtain}\isamarkupfalse%
-\ x\ \isakeyword{where}\ {\isachardoublequoteopen}{\isasymforall}y{\isachardot}\ P\ x\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ x\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ P\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \isacommand{hence}\isamarkupfalse%
-\ {\isachardoublequoteopen}P\ x\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}P\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymexists}x{\isachardot}\ P\ x\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\isacommand{qed}\isamarkupfalse%
%
@@ -1054,7 +1054,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}S{\isaliteral{2E}{\isachardot}}\ S\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ range\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -1064,33 +1064,33 @@
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{let}\isamarkupfalse%
-\ {\isacharquery}S\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymnotin}\ f\ x{\isacharbraceright}{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ f\ x{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharquery}S\ {\isasymnotin}\ range\ f{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ range\ f{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharquery}S\ {\isasymin}\ range\ f{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ f{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
-\ y\ \isakeyword{where}\ {\isachardoublequoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ y\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{3D}{\isacharequal}}\ f\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ cases\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{3F}{\isacharquery}}S{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
-\ {\isacharbackquoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
+\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{3D}{\isacharequal}}\ f\ y{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
\ False\ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{3F}{\isacharquery}}S{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
-\ {\isacharbackquoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
+\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{3D}{\isacharequal}}\ f\ y{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
\ False\ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
@@ -1114,11 +1114,11 @@
the witness for the claim.
\item Proof by \isa{cases} starts a proof by cases. Note that it remains
implicit what the two cases are: it is merely expected that the two subproofs
-prove \isa{P\ {\isasymLongrightarrow}\ {\isacharquery}thesis} and \isa{{\isasymnot}P\ {\isasymLongrightarrow}\ {\isacharquery}thesis} (in that order)
+prove \isa{P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}thesis} and \isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}thesis} (in that order)
for some \isa{P}.
\end{itemize}
If you wonder how to \isakeyword{obtain} \isa{y}:
-via the predefined elimination rule \isa{{\isasymlbrakk}b\ {\isasymin}\ range\ f{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ b\ {\isacharequal}\ f\ x\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P}.
+via the predefined elimination rule \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}b\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ f{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ b\ {\isaliteral{3D}{\isacharequal}}\ f\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P}.
Method \isa{blast} is used because the contradiction does not follow easily
by just a single rule. If you find the proof too cryptic for human
@@ -1127,7 +1127,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}S{\isaliteral{2E}{\isachardot}}\ S\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ range\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -1137,45 +1137,45 @@
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{let}\isamarkupfalse%
-\ {\isacharquery}S\ {\isacharequal}\ {\isachardoublequoteopen}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymnotin}\ f\ x{\isacharbraceright}{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ f\ x{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharquery}S\ {\isasymnotin}\ range\ f{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ range\ f{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharquery}S\ {\isasymin}\ range\ f{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{5C3C696E3E}{\isasymin}}\ range\ f{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{then}\isamarkupfalse%
\ \isacommand{obtain}\isamarkupfalse%
-\ y\ \isakeyword{where}\ {\isachardoublequoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\ y\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{3D}{\isacharequal}}\ f\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
\ False\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\ cases\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{3F}{\isacharquery}}S{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
-\ {\isachardoublequoteopen}y\ {\isasymnotin}\ f\ y{\isachardoublequoteclose}\ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ f\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
-\ {\isachardoublequoteopen}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequoteclose}\ \ \ \ \isacommand{by}\isamarkupfalse%
-{\isacharparenleft}simp\ add{\isacharcolon}\ {\isacharbackquoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isacharbackquoteclose}{\isacharparenright}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{3F}{\isacharquery}}S{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ \isacommand{by}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{3D}{\isacharequal}}\ f\ y{\isaliteral{60}{\isacharbackquoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
-\ {\isacharbackquoteopen}y\ {\isasymin}\ {\isacharquery}S{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
+\ {\isaliteral{60}{\isacharbackquoteopen}}y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{3F}{\isacharquery}}S{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
\ False\ \isacommand{by}\isamarkupfalse%
\ contradiction\isanewline
\ \ \ \ \isacommand{next}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{3F}{\isacharquery}}S{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
-\ {\isachardoublequoteopen}y\ {\isasymin}\ f\ y{\isachardoublequoteclose}\ \ \ \isacommand{by}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ f\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \isacommand{by}\isamarkupfalse%
\ simp\isanewline
\ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
-\ {\isachardoublequoteopen}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequoteclose}\ \ \ \ \isacommand{by}\isamarkupfalse%
-{\isacharparenleft}simp\ add{\isacharcolon}\ {\isacharbackquoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isacharbackquoteclose}{\isacharparenright}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}y\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{3F}{\isacharquery}}S{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ \ \isacommand{by}\isamarkupfalse%
+{\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{3F}{\isacharquery}}S\ {\isaliteral{3D}{\isacharequal}}\ f\ y{\isaliteral{60}{\isacharbackquoteclose}}{\isaliteral{29}{\isacharparenright}}\isanewline
\ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
-\ {\isacharbackquoteopen}y\ {\isasymnotin}\ {\isacharquery}S{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
+\ {\isaliteral{60}{\isacharbackquoteopen}}y\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ {\isaliteral{3F}{\isacharquery}}S{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
\ False\ \isacommand{by}\isamarkupfalse%
\ contradiction\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
@@ -1201,7 +1201,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}S{\isaliteral{2E}{\isachardot}}\ S\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ range\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -1229,7 +1229,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x\ y{\isaliteral{2E}{\isachardot}}\ A\ x\ y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ x\ y\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ C\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -1240,18 +1240,18 @@
\isanewline
\ \ \isacommand{fix}\isamarkupfalse%
\ x\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymforall}y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}y{\isaliteral{2E}{\isachardot}}\ A\ x\ y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ x\ y\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ C\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ y\ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ x\ y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ x\ y\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ C\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ x\ y\ {\isasymand}\ B\ x\ y{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ x\ y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}C\ x\ y{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}C\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
\isanewline
\ \ \ \ \isacommand{qed}\isamarkupfalse%
\isanewline
@@ -1277,7 +1277,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x\ y{\isaliteral{2E}{\isachardot}}\ A\ x\ y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ x\ y\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ C\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -1285,21 +1285,21 @@
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
+\ {\isaliteral{2D}{\isacharminus}}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymAnd}x\ y{\isachardot}\ {\isasymlbrakk}\ A\ x\ y{\isacharsemicolon}\ B\ x\ y\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ A\ x\ y{\isaliteral{3B}{\isacharsemicolon}}\ B\ x\ y\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
+\ {\isaliteral{2D}{\isacharminus}}\isanewline
\ \ \ \ \isacommand{fix}\isamarkupfalse%
\ x\ y\ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ x\ y{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ x\ y{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}C\ x\ y{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}C\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
\isanewline
\ \ \isacommand{qed}\isamarkupfalse%
\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\isacommand{qed}\isamarkupfalse%
%
@@ -1317,7 +1317,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x\ y{\isaliteral{2E}{\isachardot}}\ A\ x\ y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ x\ y\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ C\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -1325,17 +1325,17 @@
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
-\ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
+\ {\isaliteral{2D}{\isacharminus}}\isanewline
+\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
\ \isacommand{fix}\isamarkupfalse%
\ x\ y\ \isacommand{assume}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ x\ y{\isachardoublequoteclose}\ {\isachardoublequoteopen}B\ x\ y{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}C\ x\ y{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse%
-\ \isacommand{{\isacharbraceright}}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}C\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
+\ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
\isanewline
\ \ \isacommand{thus}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\isacommand{qed}\isamarkupfalse%
%
@@ -1348,7 +1348,7 @@
%
\begin{isamarkuptext}%
\noindent The result of the raw proof block is the same theorem
-as above, namely \isa{{\isasymAnd}x\ y{\isachardot}\ {\isasymlbrakk}A\ x\ y{\isacharsemicolon}\ B\ x\ y{\isasymrbrakk}\ {\isasymLongrightarrow}\ C\ x\ y}. Raw
+as above, namely \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}A\ x\ y{\isaliteral{3B}{\isacharsemicolon}}\ B\ x\ y{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C\ x\ y}. Raw
proof blocks are like ordinary proofs except that they do not prove
some explicitly stated property but that the property emerges directly
out of the \isakeyword{fixe}s, \isakeyword{assume}s and
@@ -1386,60 +1386,60 @@
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
+\ {\isaliteral{2D}{\isacharminus}}\isanewline
\ \ \isacommand{have}\isamarkupfalse%
-\ {\isachardoublequoteopen}P\isactrlisub {\isadigit{1}}\ {\isasymor}\ P\isactrlisub {\isadigit{2}}\ {\isasymor}\ P\isactrlisub {\isadigit{3}}{\isachardoublequoteclose}\ \ %
+\ {\isaliteral{22}{\isachardoublequoteopen}}P\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ P\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ P\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}{\isaliteral{22}{\isachardoublequoteclose}}\ \ %
\isamarkupcmt{\dots%
}
\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
-\ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
+\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
\ \isacommand{assume}\isamarkupfalse%
-\ P\isactrlisub {\isadigit{1}}\isanewline
+\ P\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\isanewline
\ \ \ \ %
\isamarkupcmt{\dots%
}
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
-\ {\isacharquery}thesis\ \ %
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \ %
\isamarkupcmt{\dots%
}
-\ \isacommand{{\isacharbraceright}}\isamarkupfalse%
+\ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
-\ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
+\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
\ \isacommand{assume}\isamarkupfalse%
-\ P\isactrlisub {\isadigit{2}}\isanewline
+\ P\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\isanewline
\ \ \ \ %
\isamarkupcmt{\dots%
}
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
-\ {\isacharquery}thesis\ \ %
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \ %
\isamarkupcmt{\dots%
}
-\ \isacommand{{\isacharbraceright}}\isamarkupfalse%
+\ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
\isanewline
\ \ \isacommand{moreover}\isamarkupfalse%
\isanewline
-\ \ \isacommand{{\isacharbraceleft}}\isamarkupfalse%
+\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
\ \isacommand{assume}\isamarkupfalse%
-\ P\isactrlisub {\isadigit{3}}\isanewline
+\ P\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}\isanewline
\ \ \ \ %
\isamarkupcmt{\dots%
}
\isanewline
\ \ \ \ \isacommand{have}\isamarkupfalse%
-\ {\isacharquery}thesis\ \ %
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \ %
\isamarkupcmt{\dots%
}
-\ \isacommand{{\isacharbraceright}}\isamarkupfalse%
+\ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
\isanewline
\ \ \isacommand{ultimately}\isamarkupfalse%
\ \isacommand{show}\isamarkupfalse%
-\ {\isacharquery}thesis\ \isacommand{by}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{by}\isamarkupfalse%
\ blast\isanewline
\isacommand{qed}\isamarkupfalse%
%
@@ -1489,10 +1489,10 @@
If you want to remember intermediate fact(s) that cannot be
named directly, use \isakeyword{note}. For example the result of raw
proof block can be named by following it with
-\isakeyword{note}~\isa{some{\isacharunderscore}name\ {\isacharequal}\ this}. As a side effect,
+\isakeyword{note}~\isa{some{\isaliteral{5F}{\isacharunderscore}}name\ {\isaliteral{3D}{\isacharequal}}\ this}. As a side effect,
\isa{this} is set to the list of facts on the right-hand side. You
-can also say \isa{note\ some{\isacharunderscore}fact}, which simply sets \isa{this},
-i.e.\ recalls \isa{some{\isacharunderscore}fact}, e.g.\ in a \isakeyword{moreover} sequence.%
+can also say \isa{note\ some{\isaliteral{5F}{\isacharunderscore}}fact}, which simply sets \isa{this},
+i.e.\ recalls \isa{some{\isaliteral{5F}{\isacharunderscore}}fact}, e.g.\ in a \isakeyword{moreover} sequence.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1504,11 +1504,11 @@
Sometimes it is necessary to decorate a proposition with type
constraints, as in Cantor's theorem above. These type constraints tend
to make the theorem less readable. The situation can be improved a
-little by combining the type constraint with an outer \isa{{\isasymAnd}}:%
+little by combining the type constraint with an outer \isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymAnd}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isachardot}\ {\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ f{\isachardoublequoteclose}%
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}S{\isaliteral{2E}{\isachardot}}\ S\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ range\ f{\isaliteral{22}{\isachardoublequoteclose}}%
\isadelimproof
%
\endisadelimproof
@@ -1529,7 +1529,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\isamarkupfalse%
-\ \isakeyword{fixes}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ f{\isachardoublequoteclose}%
+\ \isakeyword{fixes}\ f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ set{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}S{\isaliteral{2E}{\isachardot}}\ S\ {\isaliteral{5C3C6E6F74696E3E}{\isasymnotin}}\ range\ f{\isaliteral{22}{\isachardoublequoteclose}}%
\isadelimproof
%
\endisadelimproof
@@ -1549,12 +1549,12 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ comm{\isacharunderscore}mono{\isacharcolon}\isanewline
-\ \ \isakeyword{fixes}\ r\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ {\isacharparenleft}\isakeyword{infix}\ {\isachardoublequoteopen}{\isachargreater}{\isachardoublequoteclose}\ {\isadigit{6}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{and}\isanewline
-\ \ \ \ \ \ \ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequoteclose}\ \ \ {\isacharparenleft}\isakeyword{infixl}\ {\isachardoublequoteopen}{\isacharplus}{\isacharplus}{\isachardoublequoteclose}\ {\isadigit{7}}{\isadigit{0}}{\isacharparenright}\isanewline
-\ \ \isakeyword{assumes}\ comm{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}x\ y{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isachardot}\ x\ {\isacharplus}{\isacharplus}\ y\ {\isacharequal}\ y\ {\isacharplus}{\isacharplus}\ x{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
-\ \ \ \ \ \ \ \ \ \ mono{\isacharcolon}\ {\isachardoublequoteopen}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isachardot}\ x\ {\isachargreater}\ y\ {\isasymLongrightarrow}\ x\ {\isacharplus}{\isacharplus}\ z\ {\isachargreater}\ y\ {\isacharplus}{\isacharplus}\ z{\isachardoublequoteclose}\isanewline
-\ \ \isakeyword{shows}\ {\isachardoublequoteopen}x\ {\isachargreater}\ y\ {\isasymLongrightarrow}\ z\ {\isacharplus}{\isacharplus}\ x\ {\isachargreater}\ z\ {\isacharplus}{\isacharplus}\ y{\isachardoublequoteclose}\isanewline
+\ comm{\isaliteral{5F}{\isacharunderscore}}mono{\isaliteral{3A}{\isacharcolon}}\isanewline
+\ \ \isakeyword{fixes}\ r\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infix}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3E}{\isachargreater}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{6}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ \isakeyword{and}\isanewline
+\ \ \ \ \ \ \ f\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}\ \ \ {\isaliteral{28}{\isacharparenleft}}\isakeyword{infixl}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isadigit{7}}{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \isakeyword{assumes}\ comm{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}\ y\ {\isaliteral{3D}{\isacharequal}}\ y\ {\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline
+\ \ \ \ \ \ \ \ \ \ mono{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y\ z{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{2E}{\isachardot}}\ x\ {\isaliteral{3E}{\isachargreater}}\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}\ z\ {\isaliteral{3E}{\isachargreater}}\ y\ {\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}\ z{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3E}{\isachargreater}}\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ z\ {\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}\ x\ {\isaliteral{3E}{\isachargreater}}\ z\ {\isaliteral{2B}{\isacharplus}}{\isaliteral{2B}{\isacharplus}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -1562,7 +1562,7 @@
%
\isatagproof
\isacommand{by}\isamarkupfalse%
-{\isacharparenleft}simp\ add{\isacharcolon}\ comm\ mono{\isacharparenright}%
+{\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ comm\ mono{\isaliteral{29}{\isacharparenright}}%
\endisatagproof
{\isafoldproof}%
%
@@ -1573,9 +1573,9 @@
\begin{isamarkuptext}%
\noindent The concrete syntax is dropped at the end of the proof and the
theorem becomes \begin{isabelle}%
-{\isasymlbrakk}{\isasymAnd}x\ y{\isachardot}\ {\isacharquery}f\ x\ y\ {\isacharequal}\ {\isacharquery}f\ y\ x{\isacharsemicolon}\isanewline
-\isaindent{\ }{\isasymAnd}x\ y\ z{\isachardot}\ {\isacharquery}r\ x\ y\ {\isasymLongrightarrow}\ {\isacharquery}r\ {\isacharparenleft}{\isacharquery}f\ x\ z{\isacharparenright}\ {\isacharparenleft}{\isacharquery}f\ y\ z{\isacharparenright}{\isacharsemicolon}\ {\isacharquery}r\ {\isacharquery}x\ {\isacharquery}y{\isasymrbrakk}\isanewline
-{\isasymLongrightarrow}\ {\isacharquery}r\ {\isacharparenleft}{\isacharquery}f\ {\isacharquery}z\ {\isacharquery}x{\isacharparenright}\ {\isacharparenleft}{\isacharquery}f\ {\isacharquery}z\ {\isacharquery}y{\isacharparenright}%
+{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}f\ x\ y\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{3F}{\isacharquery}}f\ y\ x{\isaliteral{3B}{\isacharsemicolon}}\isanewline
+\isaindent{\ }{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y\ z{\isaliteral{2E}{\isachardot}}\ {\isaliteral{3F}{\isacharquery}}r\ x\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}r\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}f\ x\ z{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}f\ y\ z{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{3F}{\isacharquery}}r\ {\isaliteral{3F}{\isacharquery}}x\ {\isaliteral{3F}{\isacharquery}}y{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\isanewline
+{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}r\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}z\ {\isaliteral{3F}{\isacharquery}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}z\ {\isaliteral{3F}{\isacharquery}}y{\isaliteral{29}{\isacharparenright}}%
\end{isabelle}
\tweakskip%
\end{isamarkuptext}%
@@ -1591,7 +1591,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequoteopen}{\isasymexists}x\ y{\isachardot}\ P\ x\ y\ {\isasymand}\ Q\ x\ y{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}R{\isachardoublequoteclose}\isanewline
+\ \isakeyword{assumes}\ A{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x\ y{\isaliteral{2E}{\isachardot}}\ P\ x\ y\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{shows}\ {\isaliteral{22}{\isachardoublequoteopen}}R{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -1599,10 +1599,10 @@
%
\isatagproof
\isacommand{proof}\isamarkupfalse%
-\ {\isacharminus}\isanewline
+\ {\isaliteral{2D}{\isacharminus}}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ A\ \isacommand{obtain}\isamarkupfalse%
-\ x\ y\ \isakeyword{where}\ P{\isacharcolon}\ {\isachardoublequoteopen}P\ x\ y{\isachardoublequoteclose}\ \isakeyword{and}\ Q{\isacharcolon}\ {\isachardoublequoteopen}Q\ x\ y{\isachardoublequoteclose}\ \ \isacommand{by}\isamarkupfalse%
+\ x\ y\ \isakeyword{where}\ P{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}P\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ Q{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}Q\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \ \isacommand{by}\isamarkupfalse%
\ blast%
\endisatagproof
{\isafoldproof}%
@@ -1613,7 +1613,7 @@
%
\begin{isamarkuptext}%
Remember also that one does not even need to start with a formula
-containing \isa{{\isasymexists}} as we saw in the proof of Cantor's theorem.%
+containing \isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}} as we saw in the proof of Cantor's theorem.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -1627,7 +1627,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
-\ {\isachardoublequoteopen}A\ {\isasymlongrightarrow}\ {\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ B{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
%
\isadelimproof
%
@@ -1637,15 +1637,15 @@
\isacommand{proof}\isamarkupfalse%
\isanewline
\ \ \isacommand{assume}\isamarkupfalse%
-\ a{\isacharcolon}\ {\isachardoublequoteopen}A{\isachardoublequoteclose}\isanewline
+\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \isacommand{show}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isacharparenleft}A\ {\isasymlongrightarrow}B{\isacharparenright}\ {\isasymlongrightarrow}\ B{\isachardoublequoteclose}\isanewline
+\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}rule\ impI{\isacharparenright}\isanewline
+{\isaliteral{28}{\isacharparenleft}}rule\ impI{\isaliteral{29}{\isacharparenright}}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline
+{\isaliteral{28}{\isacharparenleft}}erule\ impE{\isaliteral{29}{\isacharparenright}}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
-{\isacharparenleft}rule\ a{\isacharparenright}\isanewline
+{\isaliteral{28}{\isacharparenleft}}rule\ a{\isaliteral{29}{\isacharparenright}}\isanewline
\ \ \ \ \isacommand{apply}\isamarkupfalse%
\ assumption\isanewline
\ \ \ \ \isacommand{done}\isamarkupfalse%