# HG changeset patch # User wenzelm # Date 1306926405 -7200 # Node ID 8c0a49d7285739a9931e08286b0fa80f73f83a7a # Parent 6e83c2f732403903e1480de4b42662f21b7d7e11 some material on "Structured Natural Deduction"; tuned; diff -r 6e83c2f73240 -r 8c0a49d72857 doc-src/IsarRef/Thy/Synopsis.thy --- a/doc-src/IsarRef/Thy/Synopsis.thy Wed Jun 01 12:39:04 2011 +0200 +++ b/doc-src/IsarRef/Thy/Synopsis.thy Wed Jun 01 13:06:45 2011 +0200 @@ -332,7 +332,7 @@ notepad begin - txt {* A vacous proof: *} + txt {* A vacuous proof: *} have A sorry moreover have B sorry @@ -350,7 +350,7 @@ ultimately have "A \ B \ C" by blast next - txt {* More ambitous bigstep reasoning involving structured results: *} + txt {* More ambitious bigstep reasoning involving structured results: *} have "A \ B \ C" sorry moreover { assume A have R sorry } @@ -362,4 +362,398 @@ have R by blast -- {* ``big-bang integration'' of proof blocks (occasionally fragile) *} end + +section {* Structured Natural Deduction *} + +subsection {* Rule statements *} + +text {* + Isabelle/Pure ``theorems'' are always natural deduction rules, + which sometimes happen to consist of a conclusion only. + + The framework connectives @{text "\"} and @{text "\"} indicate the + rule structure declaratively. For example: *} + +thm conjI +thm impI +thm nat.induct + +text {* + The object-logic is embedded into the Pure framework via an implicit + derivability judgment @{term "Trueprop :: bool \ prop"}. + + Thus any HOL formulae appears atomic to the Pure framework, while + the rule structure outlines the corresponding proof pattern. + + This can be made explicit as follows: +*} + +notepad +begin + write Trueprop ("Tr") + + thm conjI + thm impI + thm nat.induct +end + +text {* + Isar provides first-class notation for rule statements as follows. +*} + +print_statement conjI +print_statement impI +print_statement nat.induct + + +subsubsection {* Examples *} + +text {* + Introductions and eliminations of some standard connectives of + the object-logic can be written as rule statements as follows. (The + proof ``@{command "by"}~@{method blast}'' serves as sanity check.) +*} + +lemma "(P \ False) \ \ P" by blast +lemma "\ P \ P \ Q" by blast + +lemma "P \ Q \ P \ Q" by blast +lemma "P \ Q \ (P \ Q \ R) \ R" by blast + +lemma "P \ P \ Q" by blast +lemma "Q \ P \ Q" by blast +lemma "P \ Q \ (P \ R) \ (Q \ R) \ R" by blast + +lemma "(\x. P x) \ (\x. P x)" by blast +lemma "(\x. P x) \ P x" by blast + +lemma "P x \ (\x. P x)" by blast +lemma "(\x. P x) \ (\x. P x \ R) \ R" by blast + +lemma "x \ A \ x \ B \ x \ A \ B" by blast +lemma "x \ A \ B \ (x \ A \ x \ B \ R) \ R" by blast + +lemma "x \ A \ x \ A \ B" by blast +lemma "x \ B \ x \ A \ B" by blast +lemma "x \ A \ B \ (x \ A \ R) \ (x \ B \ R) \ R" by blast + + +subsection {* Isar context elements *} + +text {* We derive some results out of the blue, using Isar context + elements and some explicit blocks. This illustrates their meaning + wrt.\ Pure connectives, without goal states getting in the way. *} + +notepad +begin + { + fix x + have "B x" sorry + } + have "\x. B x" by fact + +next + + { + assume A + have B sorry + } + have "A \ B" by fact + +next + + { + def x \ t + have "B x" sorry + } + have "B t" by fact + +next + + { + obtain x :: 'a where "B x" sorry + have C sorry + } + have C by fact + +end + + +subsection {* Pure rule composition *} + +text {* + The Pure framework provides means for: + + \begin{itemize} + + \item backward-chaining of rules by @{inference resolution} + + \item closing of branches by @{inference assumption} + + \end{itemize} + + Both principles involve higher-order unification of @{text \}-terms + modulo @{text "\\\"}-equivalence (cf.\ Huet and Miller). *} + +notepad +begin + assume a: A and b: B + thm conjI + thm conjI [of A B] -- "instantiation" + thm conjI [of A B, OF a b] -- "instantiation and composition" + thm conjI [OF a b] -- "composition via unification (trivial)" + thm conjI [OF `A` `B`] + + thm conjI [OF disjI1] +end + +text {* Note: Low-level rule composition is tedious and leads to + unreadable~/ unmaintainable expressions in the text. *} + + +subsection {* Structured backward reasoning *} + +text {* Idea: Canonical proof decomposition via @{command fix}~/ + @{command assume}~/ @{command show}, where the body produces a + natural deduction rule to refine some goal. *} + +notepad +begin + fix A B :: "'a \ bool" + + have "\x. A x \ B x" + proof - + fix x + assume "A x" + show "B x" sorry + qed + + have "\x. A x \ B x" + proof - + { + fix x + assume "A x" + show "B x" sorry + } -- "implicit block structure made explicit" + note `\x. A x \ B x` + -- "side exit for the resulting rule" + qed +end + + +subsection {* Structured rule application *} + +text {* + Idea: Previous facts and new claims are composed with a rule from + the context (or background library). +*} + +notepad +begin + assume r1: "A \ B \ C" -- {* simple rule (Horn clause) *} + + have A sorry -- "prefix of facts via outer sub-proof" + then have C + proof (rule r1) + show B sorry -- "remaining rule premises via inner sub-proof" + qed + + have C + proof (rule r1) + show A sorry + show B sorry + qed + + have A and B sorry + then have C + proof (rule r1) + qed + + have A and B sorry + then have C by (rule r1) + +next + + assume r2: "A \ (\x. B1 x \ B2 x) \ C" -- {* nested rule *} + + have A sorry + then have C + proof (rule r2) + fix x + assume "B1 x" + show "B2 x" sorry + qed + + txt {* The compound rule premise @{prop "\x. B1 x \ B2 x"} is better + addressed via @{command fix}~/ @{command assume}~/ @{command show} + in the nested proof body. *} +end + + +subsection {* Example: predicate logic *} + +text {* + Using the above principles, standard introduction and elimination proofs + of predicate logic connectives of HOL work as follows. +*} + +notepad +begin + have "A \ B" and A sorry + then have B .. + + have A sorry + then have "A \ B" .. + + have B sorry + then have "A \ B" .. + + have "A \ B" sorry + then have C + proof + assume A + then show C sorry + next + assume B + then show C sorry + qed + + have A and B sorry + then have "A \ B" .. + + have "A \ B" sorry + then have A .. + + have "A \ B" sorry + then have B .. + + have False sorry + then have A .. + + have True .. + + have "\ A" + proof + assume A + then show False sorry + qed + + have "\ A" and A sorry + then have B .. + + have "\x. P x" + proof + fix x + show "P x" sorry + qed + + have "\x. P x" sorry + then have "P a" .. + + have "\x. P x" + proof + show "P a" sorry + qed + + have "\x. P x" sorry + then have C + proof + fix a + assume "P a" + show C sorry + qed + + txt {* Less awkward version using @{command obtain}: *} + have "\x. P x" sorry + then obtain a where "P a" .. +end + +text {* Further variations to illustrate Isar sub-proofs involving + @{command show}: *} + +notepad +begin + have "A \ B" + proof -- {* two strictly isolated subproofs *} + show A sorry + next + show B sorry + qed + + have "A \ B" + proof -- {* one simultaneous sub-proof *} + show A and B sorry + qed + + have "A \ B" + proof -- {* two subproofs in the same context *} + show A sorry + show B sorry + qed + + have "A \ B" + proof -- {* swapped order *} + show B sorry + show A sorry + qed + + have "A \ B" + proof -- {* sequential subproofs *} + show A sorry + show B using `A` sorry + qed +end + + +subsubsection {* Example: set-theoretic operators *} + +text {* There is nothing special about logical connectives (@{text + "\"}, @{text "\"}, @{text "\"}, @{text "\"} etc.). Operators from + set-theory or lattice-theory for analogously. It is only a matter + of rule declarations in the library; rules can be also specified + explicitly. +*} + +notepad +begin + have "x \ A" and "x \ B" sorry + then have "x \ A \ B" .. + + have "x \ A" sorry + then have "x \ A \ B" .. + + have "x \ B" sorry + then have "x \ A \ B" .. + + have "x \ A \ B" sorry + then have C + proof + assume "x \ A" + then show C sorry + next + assume "x \ B" + then show C sorry + qed + +next + have "x \ \A" + proof + fix a + assume "a \ A" + show "x \ a" sorry + qed + + have "x \ \A" sorry + then have "x \ a" + proof + show "a \ A" sorry + qed + + have "a \ A" and "x \ a" sorry + then have "x \ \A" .. + + have "x \ \A" sorry + then obtain a where "a \ A" and "x \ a" .. +end + end \ No newline at end of file diff -r 6e83c2f73240 -r 8c0a49d72857 doc-src/IsarRef/Thy/document/Synopsis.tex --- a/doc-src/IsarRef/Thy/document/Synopsis.tex Wed Jun 01 12:39:04 2011 +0200 +++ b/doc-src/IsarRef/Thy/document/Synopsis.tex Wed Jun 01 13:06:45 2011 +0200 @@ -748,7 +748,7 @@ \isatagproof % \begin{isamarkuptxt}% -A vacous proof:% +A vacuous proof:% \end{isamarkuptxt}% \isamarkuptrue% \ \ \isacommand{have}\isamarkupfalse% @@ -796,7 +796,7 @@ \isacommand{next}\isamarkupfalse% % \begin{isamarkuptxt}% -More ambitous bigstep reasoning involving structured results:% +More ambitious bigstep reasoning involving structured results:% \end{isamarkuptxt}% \isamarkuptrue% \ \ \isacommand{have}\isamarkupfalse% @@ -842,6 +842,1108 @@ \endisadelimproof \isanewline \isacommand{end}\isamarkupfalse% +% +\isamarkupsection{Structured Natural Deduction% +} +\isamarkuptrue% +% +\isamarkupsubsection{Rule statements% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Isabelle/Pure ``theorems'' are always natural deduction rules, + which sometimes happen to consist of a conclusion only. + + The framework connectives \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}{\isaliteral{22}{\isachardoublequote}}} and \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}{\isaliteral{22}{\isachardoublequote}}} indicate the + rule structure declaratively. For example:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{thm}\isamarkupfalse% +\ conjI\isanewline +\isacommand{thm}\isamarkupfalse% +\ impI\isanewline +\isacommand{thm}\isamarkupfalse% +\ nat{\isaliteral{2E}{\isachardot}}induct% +\begin{isamarkuptext}% +The object-logic is embedded into the Pure framework via an implicit + derivability judgment \isa{{\isaliteral{22}{\isachardoublequote}}Trueprop\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ bool\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ prop{\isaliteral{22}{\isachardoublequote}}}. + + Thus any HOL formulae appears atomic to the Pure framework, while + the rule structure outlines the corresponding proof pattern. + + This can be made explicit as follows:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{notepad}\isamarkupfalse% +\isanewline +\isakeyword{begin}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{write}\isamarkupfalse% +\ Trueprop\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}Tr{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +\isanewline +% +\endisadelimproof +\isanewline +\ \ \isacommand{thm}\isamarkupfalse% +\ conjI\isanewline +\ \ \isacommand{thm}\isamarkupfalse% +\ impI\isanewline +\ \ \isacommand{thm}\isamarkupfalse% +\ nat{\isaliteral{2E}{\isachardot}}induct\isanewline +\isacommand{end}\isamarkupfalse% +% +\begin{isamarkuptext}% +Isar provides first-class notation for rule statements as follows.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse% +\ conjI\isanewline +\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse% +\ impI\isanewline +\isacommand{print{\isaliteral{5F}{\isacharunderscore}}statement}\isamarkupfalse% +\ nat{\isaliteral{2E}{\isachardot}}induct% +\isamarkupsubsubsection{Examples% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Introductions and eliminations of some standard connectives of + the object-logic can be written as rule statements as follows. (The + proof ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\hyperlink{method.blast}{\mbox{\isa{blast}}}'' serves as sanity check.)% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ False{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P{\isaliteral{22}{\isachardoublequoteclose}}% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ blast% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ blast% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ blast% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequoteclose}}% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ blast% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ blast% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q{\isaliteral{22}{\isachardoublequoteclose}}% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ blast% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}P\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}Q\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequoteclose}}% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ blast% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ blast% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ blast% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ blast% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ P\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequoteclose}}% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ blast% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ B{\isaliteral{22}{\isachardoublequoteclose}}% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ blast% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequoteclose}}% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ blast% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ blast% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ blast% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isanewline +\isacommand{lemma}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ R{\isaliteral{22}{\isachardoublequoteclose}}% +\isadelimproof +\ % +\endisadelimproof +% +\isatagproof +\isacommand{by}\isamarkupfalse% +\ blast% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +% +\isamarkupsubsection{Isar context elements% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +We derive some results out of the blue, using Isar context + elements and some explicit blocks. This illustrates their meaning + wrt.\ Pure connectives, without goal states getting in the way.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{notepad}\isamarkupfalse% +\isanewline +\isakeyword{begin}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{fix}\isamarkupfalse% +\ x\isanewline +\ \ \ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse% +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% +\ fact\isanewline +\isanewline +\isacommand{next}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{assume}\isamarkupfalse% +\ A\isanewline +\ \ \ \ \isacommand{have}\isamarkupfalse% +\ B\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse% +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% +\ fact\isanewline +\isanewline +\isacommand{next}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{def}\isamarkupfalse% +\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t\isanewline +\ \ \ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse% +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}B\ t{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{by}\isamarkupfalse% +\ fact\isanewline +\isanewline +\isacommand{next}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{obtain}\isamarkupfalse% +\ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{have}\isamarkupfalse% +\ C\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse% +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ C\ \isacommand{by}\isamarkupfalse% +\ fact% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +\isanewline +% +\endisadelimproof +\isanewline +\isacommand{end}\isamarkupfalse% +% +\isamarkupsubsection{Pure rule composition% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +The Pure framework provides means for: + + \begin{itemize} + + \item backward-chaining of rules by \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} + + \item closing of branches by \hyperlink{inference.assumption}{\mbox{\isa{assumption}}} + + \end{itemize} + + Both principles involve higher-order unification of \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-terms + modulo \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{5C3C626574613E}{\isasymbeta}}{\isaliteral{5C3C6574613E}{\isasymeta}}{\isaliteral{22}{\isachardoublequote}}}-equivalence (cf.\ Huet and Miller).% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{notepad}\isamarkupfalse% +\isanewline +\isakeyword{begin}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{assume}\isamarkupfalse% +\ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isakeyword{and}\ b{\isaliteral{3A}{\isacharcolon}}\ B% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +\isanewline +% +\endisadelimproof +\ \ \isacommand{thm}\isamarkupfalse% +\ conjI\isanewline +\ \ \isacommand{thm}\isamarkupfalse% +\ conjI\ {\isaliteral{5B}{\isacharbrackleft}}of\ A\ B{\isaliteral{5D}{\isacharbrackright}}\ \ % +\isamarkupcmt{instantiation% +} +\isanewline +\ \ \isacommand{thm}\isamarkupfalse% +\ conjI\ {\isaliteral{5B}{\isacharbrackleft}}of\ A\ B{\isaliteral{2C}{\isacharcomma}}\ OF\ a\ b{\isaliteral{5D}{\isacharbrackright}}\ \ % +\isamarkupcmt{instantiation and composition% +} +\isanewline +\ \ \isacommand{thm}\isamarkupfalse% +\ conjI\ {\isaliteral{5B}{\isacharbrackleft}}OF\ a\ b{\isaliteral{5D}{\isacharbrackright}}\ \ % +\isamarkupcmt{composition via unification (trivial)% +} +\isanewline +\ \ \isacommand{thm}\isamarkupfalse% +\ conjI\ {\isaliteral{5B}{\isacharbrackleft}}OF\ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\ {\isaliteral{60}{\isacharbackquoteopen}}B{\isaliteral{60}{\isacharbackquoteclose}}{\isaliteral{5D}{\isacharbrackright}}\isanewline +\isanewline +\ \ \isacommand{thm}\isamarkupfalse% +\ conjI\ {\isaliteral{5B}{\isacharbrackleft}}OF\ disjI{\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\isanewline +\isacommand{end}\isamarkupfalse% +% +\begin{isamarkuptext}% +Note: Low-level rule composition is tedious and leads to + unreadable~/ unmaintainable expressions in the text.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Structured backward reasoning% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Idea: Canonical proof decomposition via \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~/ + \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~/ \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}, where the body produces a + natural deduction rule to refine some goal.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{notepad}\isamarkupfalse% +\isanewline +\isakeyword{begin}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{fix}\isamarkupfalse% +\ A\ B\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\ {\isaliteral{2D}{\isacharminus}}\isanewline +\ \ \ \ \isacommand{fix}\isamarkupfalse% +\ x\isanewline +\ \ \ \ \isacommand{assume}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}A\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\ {\isaliteral{2D}{\isacharminus}}\isanewline +\ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse% +\isanewline +\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse% +\ x\isanewline +\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}A\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \ \ \ \ \isacommand{show}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}B\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse% +\ % +\isamarkupcmt{implicit block structure made explicit% +} +\isanewline +\ \ \ \ \isacommand{note}\isamarkupfalse% +\ {\isaliteral{60}{\isacharbackquoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ A\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ x{\isaliteral{60}{\isacharbackquoteclose}}\isanewline +\ \ \ \ \ \ % +\isamarkupcmt{side exit for the resulting rule% +} +\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +\isanewline +% +\endisadelimproof +\isacommand{end}\isamarkupfalse% +% +\isamarkupsubsection{Structured rule application% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Idea: Previous facts and new claims are composed with a rule from + the context (or background library).% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{notepad}\isamarkupfalse% +\isanewline +\isakeyword{begin}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{assume}\isamarkupfalse% +\ r{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \ % +\isamarkupcmt{simple rule (Horn clause)% +} +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ A\ \isacommand{sorry}\isamarkupfalse% +\ \ % +\isamarkupcmt{prefix of facts via outer sub-proof% +} +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{have}\isamarkupfalse% +\ C\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ B\ \isacommand{sorry}\isamarkupfalse% +\ \ % +\isamarkupcmt{remaining rule premises via inner sub-proof% +} +\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ C\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ A\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ B\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{have}\isamarkupfalse% +\ C\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{have}\isamarkupfalse% +\ C\ \isacommand{by}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline +\isanewline +\isacommand{next}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{assume}\isamarkupfalse% +\ r{\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B{\isadigit{1}}\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isadigit{2}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\ \ % +\isamarkupcmt{nested rule% +} +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ A\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{have}\isamarkupfalse% +\ C\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\ {\isaliteral{28}{\isacharparenleft}}rule\ r{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\isanewline +\ \ \ \ \isacommand{fix}\isamarkupfalse% +\ x\isanewline +\ \ \ \ \isacommand{assume}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{1}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}B{\isadigit{2}}\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +% +\begin{isamarkuptxt}% +The compound rule premise \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B{\isadigit{1}}\ x\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isadigit{2}}\ x{\isaliteral{22}{\isachardoublequote}}} is better + addressed via \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}~/ \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}~/ \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} + in the nested proof body.% +\end{isamarkuptxt}% +\isamarkuptrue% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +% +\endisadelimproof +\isacommand{end}\isamarkupfalse% +% +\isamarkupsubsection{Example: predicate logic% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Using the above principles, standard introduction and elimination proofs + of predicate logic connectives of HOL work as follows.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{notepad}\isamarkupfalse% +\isanewline +\isakeyword{begin}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ A\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{have}\isamarkupfalse% +\ B\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ A\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ B\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C6F723E}{\isasymor}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{have}\isamarkupfalse% +\ C\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{assume}\isamarkupfalse% +\ A\isanewline +\ \ \ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{show}\isamarkupfalse% +\ C\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{next}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{assume}\isamarkupfalse% +\ B\isanewline +\ \ \ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{show}\isamarkupfalse% +\ C\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{have}\isamarkupfalse% +\ A\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{have}\isamarkupfalse% +\ B\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ False\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{have}\isamarkupfalse% +\ A\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ True\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{assume}\isamarkupfalse% +\ A\isanewline +\ \ \ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{show}\isamarkupfalse% +\ False\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ A\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{have}\isamarkupfalse% +\ B\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{fix}\isamarkupfalse% +\ x\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{have}\isamarkupfalse% +\ C\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{fix}\isamarkupfalse% +\ a\isanewline +\ \ \ \ \isacommand{assume}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ C\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +% +\begin{isamarkuptxt}% +Less awkward version using \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}:% +\end{isamarkuptxt}% +\isamarkuptrue% +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{obtain}\isamarkupfalse% +\ a\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}P\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +\isanewline +% +\endisadelimproof +\isacommand{end}\isamarkupfalse% +% +\begin{isamarkuptext}% +Further variations to illustrate Isar sub-proofs involving + \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}}:% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{notepad}\isamarkupfalse% +\isanewline +\isakeyword{begin}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\ \ % +\isamarkupcmt{two strictly isolated subproofs% +} +\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ A\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{next}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ B\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\ \ % +\isamarkupcmt{one simultaneous sub-proof% +} +\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ A\ \isakeyword{and}\ B\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\ \ % +\isamarkupcmt{two subproofs in the same context% +} +\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ A\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ B\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\ \ % +\isamarkupcmt{swapped order% +} +\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ B\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ A\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\ \ % +\isamarkupcmt{sequential subproofs% +} +\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ A\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ B\ \isacommand{using}\isamarkupfalse% +\ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +\isanewline +% +\endisadelimproof +\isacommand{end}\isamarkupfalse% +% +\isamarkupsubsubsection{Example: set-theoretic operators% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +There is nothing special about logical connectives (\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C616E643E}{\isasymand}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6F723E}{\isasymor}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}{\isaliteral{22}{\isachardoublequote}}} etc.). Operators from + set-theory or lattice-theory for analogously. It is only a matter + of rule declarations in the library; rules can be also specified + explicitly.% +\end{isamarkuptext}% +\isamarkuptrue% +\isacommand{notepad}\isamarkupfalse% +\isanewline +\isakeyword{begin}\isanewline +% +\isadelimproof +\ \ % +\endisadelimproof +% +\isatagproof +\isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C696E7465723E}{\isasyminter}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{have}\isamarkupfalse% +\ C\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{assume}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{show}\isamarkupfalse% +\ C\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{next}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{assume}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ B{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{show}\isamarkupfalse% +\ C\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +\isanewline +\isanewline +\isacommand{next}\isamarkupfalse% +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C496E7465723E}{\isasymInter}}A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{fix}\isamarkupfalse% +\ a\isanewline +\ \ \ \ \isacommand{assume}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C496E7465723E}{\isasymInter}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\isanewline +\ \ \isacommand{proof}\isamarkupfalse% +\isanewline +\ \ \ \ \isacommand{show}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{qed}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% +\isanewline +\isanewline +\ \ \isacommand{have}\isamarkupfalse% +\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ {\isaliteral{5C3C556E696F6E3E}{\isasymUnion}}A{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{sorry}\isamarkupfalse% +\isanewline +\ \ \isacommand{then}\isamarkupfalse% +\ \isacommand{obtain}\isamarkupfalse% +\ a\ \isakeyword{where}\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ a{\isaliteral{22}{\isachardoublequoteclose}}\ \isacommand{{\isaliteral{2E}{\isachardot}}{\isaliteral{2E}{\isachardot}}}\isamarkupfalse% +% +\endisatagproof +{\isafoldproof}% +% +\isadelimproof +\isanewline +% +\endisadelimproof +\isacommand{end}\isamarkupfalse% \isanewline % \isadelimtheory