--- a/doc-src/IsarRef/Thy/Synopsis.thy Thu Jun 02 13:59:23 2011 +0200
+++ b/doc-src/IsarRef/Thy/Synopsis.thy Thu Jun 02 14:08:46 2011 +0200
@@ -104,7 +104,7 @@
assume "x \<noteq> y"
note this [symmetric]
- txt {* Adhoc-simplication (take care!): *}
+ txt {* Adhoc-simplification (take care!): *}
assume "P ([] @ xs)"
note this [simplified]
end
@@ -954,4 +954,155 @@
then obtain a where "a \<in> A" and "x \<in> a" ..
end
+
+section {* Generalized elimination and cases *}
+
+subsection {* General elimination rules *}
+
+text {*
+ The general format of elimination rules is illustrated by the
+ following typical representatives:
+*}
+
+thm exE -- {* local parameter *}
+thm conjE -- {* local premises *}
+thm disjE -- {* split into cases *}
+
+text {*
+ Combining these characteristics leads to the following general scheme
+ for elimination rules with cases:
+
+ \begin{itemize}
+
+ \item prefix of assumptions (or ``major premises'')
+
+ \item one or more cases that enable to establish the main conclusion
+ in an augmented context
+
+ \end{itemize}
+*}
+
+notepad
+begin
+ assume r:
+ "A1 \<Longrightarrow> A2 \<Longrightarrow> (* assumptions *)
+ (\<And>x y. B1 x y \<Longrightarrow> C1 x y \<Longrightarrow> R) \<Longrightarrow> (* case 1 *)
+ (\<And>x y. B2 x y \<Longrightarrow> C2 x y \<Longrightarrow> R) \<Longrightarrow> (* case 2 *)
+ R (* main conclusion *)"
+
+ have A1 and A2 sorry
+ then have R
+ proof (rule r)
+ fix x y
+ assume "B1 x y" and "C1 x y"
+ show ?thesis sorry
+ next
+ fix x y
+ assume "B2 x y" and "C2 x y"
+ show ?thesis sorry
+ qed
+end
+
+text {* Here @{text "?thesis"} is used to refer to the unchanged goal
+ statement. *}
+
+
+subsection {* Rules with cases *}
+
+text {*
+ Applying an elimination rule to some goal, leaves that unchanged
+ but allows to augment the context in the sub-proof of each case.
+
+ Isar provides some infrastructure to support this:
+
+ \begin{itemize}
+
+ \item native language elements to state eliminations
+
+ \item symbolic case names
+
+ \item method @{method cases} to recover this structure in a
+ sub-proof
+
+ \end{itemize}
+*}
+
+print_statement exE
+print_statement conjE
+print_statement disjE
+
+lemma
+ assumes A1 and A2 -- {* assumptions *}
+ obtains
+ (case1) x y where "B1 x y" and "C1 x y"
+ | (case2) x y where "B2 x y" and "C2 x y"
+ sorry
+
+
+subsubsection {* Example *}
+
+lemma tertium_non_datur:
+ obtains
+ (T) A
+ | (F) "\<not> A"
+ by blast
+
+notepad
+begin
+ fix x y :: 'a
+ have C
+ proof (cases "x = y" rule: tertium_non_datur)
+ case T
+ from `x = y` show ?thesis sorry
+ next
+ case F
+ from `x \<noteq> y` show ?thesis sorry
+ qed
+end
+
+
+subsubsection {* Example *}
+
+text {*
+ Isabelle/HOL specification mechanisms (datatype, inductive, etc.)
+ provide suitable derived cases rules.
+*}
+
+datatype foo = Foo | Bar foo
+
+notepad
+begin
+ fix x :: foo
+ have C
+ proof (cases x)
+ case Foo
+ from `x = Foo` show ?thesis sorry
+ next
+ case (Bar a)
+ from `x = Bar a` show ?thesis sorry
+ qed
+end
+
+
+subsection {* Obtaining local contexts *}
+
+text {* A single ``case'' branch may be inlined into Isar proof text
+ via @{command obtain}. This proves @{prop "(\<And>x. B x \<Longrightarrow> thesis) \<Longrightarrow>
+ thesis"} on the spot, and augments the context afterwards. *}
+
+notepad
+begin
+ fix B :: "'a \<Rightarrow> bool"
+
+ obtain x where "B x" sorry
+ note `B x`
+
+ txt {* Conclusions from this context may not mention @{term x} again! *}
+ {
+ obtain x where "B x" sorry
+ from `B x` have C sorry
+ }
+ note `C`
+end
+
end
\ No newline at end of file
--- a/doc-src/IsarRef/Thy/document/Synopsis.tex Thu Jun 02 13:59:23 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Synopsis.tex Thu Jun 02 14:08:46 2011 +0200
@@ -260,7 +260,7 @@
\ \ \isacommand{note}\isamarkupfalse%
\ this\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}%
\begin{isamarkuptxt}%
-Adhoc-simplication (take care!):%
+Adhoc-simplification (take care!):%
\end{isamarkuptxt}%
\isamarkuptrue%
\ \ \isacommand{assume}\isamarkupfalse%
@@ -2374,6 +2374,326 @@
%
\endisadelimproof
\isacommand{end}\isamarkupfalse%
+%
+\isamarkupsection{Generalized elimination and cases%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{General elimination rules%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The general format of elimination rules is illustrated by the
+ following typical representatives:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{thm}\isamarkupfalse%
+\ exE\ \ \ \ \ %
+\isamarkupcmt{local parameter%
+}
+\isanewline
+\isacommand{thm}\isamarkupfalse%
+\ conjE\ \ \ %
+\isamarkupcmt{local premises%
+}
+\isanewline
+\isacommand{thm}\isamarkupfalse%
+\ disjE\ \ \ %
+\isamarkupcmt{split into cases%
+}
+%
+\begin{isamarkuptext}%
+Combining these characteristics leads to the following general scheme
+ for elimination rules with cases:
+
+ \begin{itemize}
+
+ \item prefix of assumptions (or ``major premises'')
+
+ \item one or more cases that enable to establish the main conclusion
+ in an augmented context
+
+ \end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{notepad}\isamarkupfalse%
+\isanewline
+\isakeyword{begin}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{assume}\isamarkupfalse%
+\ r{\isaliteral{3A}{\isacharcolon}}\isanewline
+\ \ \ \ {\isaliteral{22}{\isachardoublequoteopen}}A{\isadigit{1}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A{\isadigit{2}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ assumptions\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y{\isaliteral{2E}{\isachardot}}\ B{\isadigit{1}}\ x\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isadigit{1}}\ x\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ case\ {\isadigit{1}}\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x\ y{\isaliteral{2E}{\isachardot}}\ B{\isadigit{2}}\ x\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isadigit{2}}\ x\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ case\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ R\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}\ main\ conclusion\ {\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ A{\isadigit{1}}\ \isakeyword{and}\ A{\isadigit{2}}\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ R\isanewline
+\ \ \isacommand{proof}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ x\ y\isanewline
+\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{1}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}C{\isadigit{1}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \ \ \isacommand{show}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ x\ y\isanewline
+\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{2}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}C{\isadigit{2}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ \ \ \isacommand{show}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isacommand{end}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Here \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}thesis{\isaliteral{22}{\isachardoublequote}}} is used to refer to the unchanged goal
+ statement.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Rules with cases%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Applying an elimination rule to some goal, leaves that unchanged
+ but allows to augment the context in the sub-proof of each case.
+
+ Isar provides some infrastructure to support this:
+
+ \begin{itemize}
+
+ \item native language elements to state eliminations
+
+ \item symbolic case names
+
+ \item method \hyperlink{method.cases}{\mbox{\isa{cases}}} to recover this structure in a
+ sub-proof
+
+ \end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
+\ exE\isanewline
+\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
+\ conjE\isanewline
+\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse%
+\ disjE\isanewline
+\isanewline
+\isacommand{lemma}\isamarkupfalse%
+\isanewline
+\ \ \isakeyword{assumes}\ A{\isadigit{1}}\ \isakeyword{and}\ A{\isadigit{2}}\ \ %
+\isamarkupcmt{assumptions%
+}
+\isanewline
+\ \ \isakeyword{obtains}\isanewline
+\ \ \ \ {\isaliteral{28}{\isacharparenleft}}case{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ \ x\ y\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{1}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}C{\isadigit{1}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{28}{\isacharparenleft}}case{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ \ x\ y\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{2}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}C{\isadigit{2}}\ x\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{sorry}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isamarkupsubsubsection{Example%
+}
+\isamarkuptrue%
+\isacommand{lemma}\isamarkupfalse%
+\ tertium{\isaliteral{5F}{\isacharunderscore}}non{\isaliteral{5F}{\isacharunderscore}}datur{\isaliteral{3A}{\isacharcolon}}\isanewline
+\ \ \isakeyword{obtains}\isanewline
+\ \ \ \ {\isaliteral{28}{\isacharparenleft}}T{\isaliteral{29}{\isacharparenright}}\ \ A\isanewline
+\ \ {\isaliteral{7C}{\isacharbar}}\ {\isaliteral{28}{\isacharparenleft}}F{\isaliteral{29}{\isacharparenright}}\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{by}\isamarkupfalse%
+\ blast%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isanewline
+\isacommand{notepad}\isamarkupfalse%
+\isanewline
+\isakeyword{begin}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{fix}\isamarkupfalse%
+\ x\ y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ C\isanewline
+\ \ \isacommand{proof}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}cases\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\ rule{\isaliteral{3A}{\isacharcolon}}\ tertium{\isaliteral{5F}{\isacharunderscore}}non{\isaliteral{5F}{\isacharunderscore}}datur{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \isacommand{case}\isamarkupfalse%
+\ T\isanewline
+\ \ \ \ \isacommand{from}\isamarkupfalse%
+\ {\isaliteral{60}{\isacharbackquoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{case}\isamarkupfalse%
+\ F\isanewline
+\ \ \ \ \isacommand{from}\isamarkupfalse%
+\ {\isaliteral{60}{\isacharbackquoteopen}}x\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ y{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isacommand{end}\isamarkupfalse%
+%
+\isamarkupsubsubsection{Example%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isabelle/HOL specification mechanisms (datatype, inductive, etc.)
+ provide suitable derived cases rules.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\isamarkupfalse%
+\ foo\ {\isaliteral{3D}{\isacharequal}}\ Foo\ {\isaliteral{7C}{\isacharbar}}\ Bar\ foo\isanewline
+\isanewline
+\isacommand{notepad}\isamarkupfalse%
+\isanewline
+\isakeyword{begin}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{fix}\isamarkupfalse%
+\ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ foo\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ C\isanewline
+\ \ \isacommand{proof}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}cases\ x{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \isacommand{case}\isamarkupfalse%
+\ Foo\isanewline
+\ \ \ \ \isacommand{from}\isamarkupfalse%
+\ {\isaliteral{60}{\isacharbackquoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ Foo{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{case}\isamarkupfalse%
+\ {\isaliteral{28}{\isacharparenleft}}Bar\ a{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \isacommand{from}\isamarkupfalse%
+\ {\isaliteral{60}{\isacharbackquoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ Bar\ a{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{show}\isamarkupfalse%
+\ {\isaliteral{3F}{\isacharquery}}thesis\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isacommand{end}\isamarkupfalse%
+%
+\isamarkupsubsection{Obtaining local contexts%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+A single ``case'' branch may be inlined into Isar proof text
+ via \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}. This proves \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ thesis{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ thesis{\isaliteral{22}{\isachardoublequote}}} on the spot, and augments the context afterwards.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{notepad}\isamarkupfalse%
+\isanewline
+\isakeyword{begin}\isanewline
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{fix}\isamarkupfalse%
+\ B\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
+\isanewline
+\ \ \isacommand{obtain}\isamarkupfalse%
+\ x\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ {\isaliteral{60}{\isacharbackquoteopen}}B\ x{\isaliteral{60}{\isacharbackquoteclose}}%
+\begin{isamarkuptxt}%
+Conclusions from this context may not mention \isa{x} again!%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{obtain}\isamarkupfalse%
+\ x\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{from}\isamarkupfalse%
+\ {\isaliteral{60}{\isacharbackquoteopen}}B\ x{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{have}\isamarkupfalse%
+\ C\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
+\isanewline
+\ \ \isacommand{note}\isamarkupfalse%
+\ {\isaliteral{60}{\isacharbackquoteopen}}C{\isaliteral{60}{\isacharbackquoteclose}}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+\isanewline
+%
+\endisadelimproof
+\isacommand{end}\isamarkupfalse%
\isanewline
%
\isadelimtheory