diff -r 42671298f037 -r 313a24b66a8d doc-src/IsarOverview/Isar/document/Logic.tex --- 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%