# HG changeset patch # User wenzelm # Date 1119026185 -7200 # Node ID 7efee005e568fd02c9569141afe9d3b89ac8f725 # Parent 4c6fd0c01d28f20a47ee7ea267a282015b36e0cb updated; diff -r 4c6fd0c01d28 -r 7efee005e568 doc-src/IsarOverview/Isar/document/Induction.tex --- a/doc-src/IsarOverview/Isar/document/Induction.tex Fri Jun 17 18:35:27 2005 +0200 +++ b/doc-src/IsarOverview/Isar/document/Induction.tex Fri Jun 17 18:36:25 2005 +0200 @@ -26,15 +26,19 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ A{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\ cases\isanewline +\ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse% +\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{next}\isanewline +\ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}\ \isamarkupfalse% +\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent The two cases must come in this order because \isa{cases} merely abbreviates \isa{{\isacharparenleft}rule\ case{\isacharunderscore}split{\isacharunderscore}thm{\isacharparenright}} where @@ -51,15 +55,19 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ A{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\ {\isacharparenleft}cases\ {\isachardoublequote}A{\isachardoublequote}{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{case}\ True\ \isamarkupfalse% +\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{next}\isanewline +\ \ \isamarkupfalse% +\isacommand{case}\ False\ \isamarkupfalse% +\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent which is like the previous proof but instantiates @@ -76,15 +84,19 @@ \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}length{\isacharparenleft}tl\ xs{\isacharparenright}\ {\isacharequal}\ length\ xs\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\ {\isacharparenleft}cases\ xs{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{case}\ Nil\ \isamarkupfalse% +\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse% +\isacommand{by}\ simp\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{next}\isanewline +\ \ \isamarkupfalse% +\isacommand{case}\ Cons\ \isamarkupfalse% +\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse% +\isacommand{by}\ simp\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent Here `\isakeyword{case}~\isa{Nil}' abbreviates @@ -117,7 +129,7 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{by}\ {\isacharparenleft}induct\ n{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isamarkupfalse% % \begin{isamarkuptext}% \noindent The constraint \isa{{\isacharcolon}{\isacharcolon}nat} is needed because all of @@ -130,15 +142,20 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}{\isacharquery}P\ {\isadigit{0}}{\isachardoublequote}\ \isamarkupfalse% +\isacommand{by}\ simp\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{next}\isanewline +\ \ \isamarkupfalse% +\isacommand{fix}\ n\ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{thus}\ {\isachardoublequote}{\isacharquery}P{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse% +\isacommand{by}\ simp\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent We could refine this further to show more of the equational @@ -148,15 +165,19 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{case}\ {\isadigit{0}}\ \isamarkupfalse% +\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse% +\isacommand{by}\ simp\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{next}\isanewline +\ \ \isamarkupfalse% +\isacommand{case}\ Suc\ \isamarkupfalse% +\isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse% +\isacommand{by}\ simp\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent The implicitly defined \isa{{\isacharquery}case} refers to the @@ -171,15 +192,19 @@ \isamarkuptrue% \isacommand{lemma}\ \isakeyword{fixes}\ n{\isacharcolon}{\isacharcolon}nat\ \isakeyword{shows}\ {\isachardoublequote}n\ {\isacharless}\ n{\isacharasterisk}n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{case}\ {\isadigit{0}}\ \isamarkupfalse% +\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse% +\isacommand{by}\ simp\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{next}\isanewline +\ \ \isamarkupfalse% +\isacommand{case}\ {\isacharparenleft}Suc\ i{\isacharparenright}\ \isamarkupfalse% +\isacommand{thus}\ {\isachardoublequote}Suc\ i\ {\isacharless}\ Suc\ i\ {\isacharasterisk}\ Suc\ i\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequote}\ \isamarkupfalse% +\isacommand{by}\ simp\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent Of course we could again have written @@ -211,33 +236,56 @@ \isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isacharparenleft}{\isasymAnd}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ m{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}{\isachardoublequote}\isanewline \ \ \isakeyword{shows}\ {\isachardoublequote}P{\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\ {\isacharparenleft}rule\ A{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}{\isasymAnd}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ m{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{case}\ {\isadigit{0}}\ \isamarkupfalse% +\isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse% +\isacommand{by}\ simp\isanewline +\ \ \isamarkupfalse% +\isacommand{next}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{case}\ {\isacharparenleft}Suc\ n{\isacharparenright}\ \ \ % +\isamarkupcmt{\isakeyword{fix} \isa{m} \isakeyword{assume} \isa{Suc}: \isa{{\isachardoublequote}{\isacharquery}m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ {\isacharquery}m{\isachardoublequote}} \isa{{\isachardoublequote}m\ {\isacharless}\ Suc\ n{\isachardoublequote}}% +} +\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{show}\ {\isacharquery}case\ \ \ \ % +\isamarkupcmt{\isa{P\ m}% +} +\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{proof}\ cases\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{assume}\ eq{\isacharcolon}\ {\isachardoublequote}m\ {\isacharequal}\ n{\isachardoublequote}\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{from}\ Suc\ \isakeyword{and}\ A\ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}P\ n{\isachardoublequote}\ \isamarkupfalse% +\isacommand{by}\ blast\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{with}\ eq\ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}P\ m{\isachardoublequote}\ \isamarkupfalse% +\isacommand{by}\ simp\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{next}\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}m\ {\isasymnoteq}\ n{\isachardoublequote}\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{with}\ Suc\ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}m\ {\isacharless}\ n{\isachardoublequote}\ \isamarkupfalse% +\isacommand{by}\ arith\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{thus}\ {\isachardoublequote}P\ m{\isachardoublequote}\ \isamarkupfalse% +\isacommand{by}{\isacharparenleft}rule\ Suc{\isacharparenright}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{qed}\isanewline +\ \ \isamarkupfalse% +\isacommand{qed}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent Given the explanations above and the comments in the @@ -284,16 +332,21 @@ \isamarkuptrue% \isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{using}\ A\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\ induct\isanewline +\ \ \isamarkupfalse% +\isacommand{case}\ refl\ \isamarkupfalse% +\isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse% +\isacommand{{\isachardot}}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{next}\isanewline +\ \ \isamarkupfalse% +\isacommand{case}\ step\ \isamarkupfalse% +\isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse% +\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isachardot}step{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent Rule induction is triggered by a fact $(x_1,\dots,x_n) @@ -308,22 +361,37 @@ \isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isakeyword{and}\ B{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline \ \ \isakeyword{shows}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\ {\isacharminus}\isanewline +\ \ \isamarkupfalse% +\isacommand{from}\ A\ B\ \isamarkupfalse% +\isacommand{show}\ {\isacharquery}thesis\isanewline +\ \ \isamarkupfalse% +\isacommand{proof}\ induct\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{fix}\ x\ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \ % +\isamarkupcmt{\isa{B}[\isa{y} := \isa{x}]% +} +\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{thus}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}}\isanewline +\ \ \isamarkupfalse% +\isacommand{next}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{fix}\ x{\isacharprime}\ x\ y\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{assume}\ {\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharprime}{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isachardoublequote}\ \isakeyword{and}\isanewline +\ \ \ \ \ \ \ \ \ \ \ IH{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isakeyword{and}\isanewline +\ \ \ \ \ \ \ \ \ \ \ B{\isacharcolon}\ \ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{from}\ {\isadigit{1}}\ IH{\isacharbrackleft}OF\ B{\isacharbrackright}\ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x{\isacharprime}{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isamarkupfalse% +\isacommand{by}{\isacharparenleft}rule\ rtc{\isachardot}step{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{qed}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent We start the proof with \isakeyword{from}~\isa{A\ B}. Only \isa{A} is ``consumed'' by the induction step. @@ -381,28 +449,38 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ rot\ xs\ {\isacharequal}\ tl\ xs\ {\isacharat}\ {\isacharbrackleft}hd\ xs{\isacharbrackright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\ {\isacharparenleft}induct\ xs\ rule{\isacharcolon}\ rot{\isachardot}induct{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{case}\ {\isadigit{1}}\ \isamarkupfalse% +\isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse% +\isacommand{by}\ simp\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{next}\isanewline +\ \ \isamarkupfalse% +\isacommand{case}\ {\isadigit{2}}\ \isamarkupfalse% +\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse% +\isacommand{by}\ simp\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{next}\isanewline +\ \ \isamarkupfalse% +\isacommand{case}\ {\isacharparenleft}{\isadigit{3}}\ a\ b\ cs{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}rot\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ cs{\isacharparenright}\ {\isacharequal}\ b\ {\isacharhash}\ rot{\isacharparenleft}a\ {\isacharhash}\ cs{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse% +\isacommand{by}\ simp\isanewline +\ \ \isamarkupfalse% +\isacommand{also}\ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ b\ {\isacharhash}\ tl{\isacharparenleft}a\ {\isacharhash}\ cs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}hd{\isacharparenleft}a\ {\isacharhash}\ cs{\isacharparenright}{\isacharbrackright}{\isachardoublequote}\ \isamarkupfalse% +\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}{\isadigit{3}}{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{also}\ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ tl\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ cs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}hd\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ cs{\isacharparenright}{\isacharbrackright}{\isachardoublequote}\ \isamarkupfalse% +\isacommand{by}\ simp\isanewline +\ \ \isamarkupfalse% +\isacommand{finally}\ \isamarkupfalse% +\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse% +\isacommand{{\isachardot}}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -420,7 +498,7 @@ \end{isamarkuptext}% \isamarkuptrue% \isamarkupfalse% -\isanewline +\isacommand{by}\ {\isacharparenleft}induct\ xs\ rule{\isacharcolon}\ rot{\isachardot}induct{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline \isamarkupfalse% \isamarkupfalse% \end{isabellebody}% diff -r 4c6fd0c01d28 -r 7efee005e568 doc-src/IsarOverview/Isar/document/Logic.tex --- a/doc-src/IsarOverview/Isar/document/Logic.tex Fri Jun 17 18:35:27 2005 +0200 +++ b/doc-src/IsarOverview/Isar/document/Logic.tex Fri Jun 17 18:36:25 2005 +0200 @@ -22,11 +22,14 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\ {\isacharparenleft}rule\ impI{\isacharparenright}\isanewline +\ \ \isamarkupfalse% +\isacommand{assume}\ a{\isacharcolon}\ {\isachardoublequote}A{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse% +\isacommand{by}{\isacharparenleft}rule\ a{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -42,11 +45,14 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \isamarkupfalse% +\isacommand{assume}\ a{\isacharcolon}\ A\isanewline +\ \ \isamarkupfalse% +\isacommand{show}\ A\ \isamarkupfalse% +\isacommand{by}{\isacharparenleft}rule\ a{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent Single-identifier formulae such as \isa{A} need not @@ -60,11 +66,14 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% To hide proofs by assumption further, \isakeyword{by}\isa{{\isacharparenleft}method{\isacharparenright}} @@ -74,11 +83,14 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A\ {\isasymand}\ A{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}A\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse% +\isacommand{by}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent Rule \isa{conjI} is of course \isa{{\isasymlbrakk}{\isacharquery}P{\isacharsemicolon}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isasymand}\ {\isacharquery}Q}. @@ -92,11 +104,14 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A\ {\isasymand}\ A{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}A\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -121,15 +136,25 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \isamarkupfalse% +\isacommand{assume}\ AB{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{proof}\ {\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}% +} +\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ {\isachardoublequote}B{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline +\ \ \isamarkupfalse% +\isacommand{qed}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent Note that the term \isa{{\isacharquery}thesis} always stands for the @@ -155,16 +180,23 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \isamarkupfalse% +\isacommand{assume}\ AB{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{from}\ AB\ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ {\isachardoublequote}B{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline +\ \ \isamarkupfalse% +\isacommand{qed}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% Now we come to a second important principle: @@ -178,16 +210,23 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{from}\ this\ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ {\isachardoublequote}B{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline +\ \ \isamarkupfalse% +\isacommand{qed}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent Because of the frequency of \isakeyword{from}~\isa{this}, Isar provides two abbreviations: @@ -203,18 +242,23 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \isamarkupfalse% +\isacommand{assume}\ ab{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{from}\ ab\ \isamarkupfalse% +\isacommand{have}\ a{\isacharcolon}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline +\ \ \isamarkupfalse% +\isacommand{from}\ ab\ \isamarkupfalse% +\isacommand{have}\ b{\isacharcolon}\ {\isachardoublequote}B{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline +\ \ \isamarkupfalse% +\isacommand{from}\ b\ a\ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent It is worth examining this text in detail because it @@ -265,19 +309,25 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \isamarkupfalse% +\isacommand{assume}\ ab{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{from}\ ab\ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}B{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline +\ \ \isamarkupfalse% +\isacommand{moreover}\isanewline +\ \ \isamarkupfalse% +\isacommand{from}\ ab\ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline +\ \ \isamarkupfalse% +\isacommand{ultimately}\ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent You can combine any number of facts \isa{A{\isadigit{1}}} \dots\ \isa{An} into a sequence by separating their proofs with @@ -296,36 +346,56 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ {\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \isamarkupfalse% +\isacommand{assume}\ n{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{proof}\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{assume}\ nn{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isacharparenright}{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}{\isasymnot}\ B{\isachardoublequote}\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \ \ \ \ \ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}B{\isachardoublequote}\isanewline +\ \ \ \ \ \ \ \ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline +\ \ \ \ \ \ \ \ \isamarkupfalse% +\isacommand{with}\ n\ \isamarkupfalse% +\isacommand{show}\ False\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{qed}\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{hence}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{with}\ nn\ \isamarkupfalse% +\isacommand{show}\ False\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{qed}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{hence}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{with}\ nn\ \isamarkupfalse% +\isacommand{show}\ False\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline +\ \ \isamarkupfalse% +\isacommand{qed}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -355,15 +425,19 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\ \isamarkupfalse% +\isacommand{thus}\ {\isachardoublequote}B{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{next}\isanewline +\ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\ \isamarkupfalse% +\isacommand{thus}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent The \isakeyword{proof} always works on the conclusion, @@ -394,15 +468,19 @@ \isacommand{lemma}\ {\isachardoublequote}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B\ {\isasymLongrightarrow}\ large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequote}\isanewline \ \ \ \ \ \ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}AB\ {\isasymLongrightarrow}\ {\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequote}{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}{\isacharquery}AB{\isachardoublequote}\ \isamarkupfalse% +\isacommand{thus}\ {\isachardoublequote}{\isacharquery}B{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{next}\isanewline +\ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}{\isacharquery}AB{\isachardoublequote}\ \isamarkupfalse% +\isacommand{thus}\ {\isachardoublequote}{\isacharquery}A{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent Any formula may be followed by @@ -419,15 +497,19 @@ \isacommand{lemma}\ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequote}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B{\isachardoublequote}\isanewline \ \ \isakeyword{shows}\ {\isachardoublequote}large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequote}{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \isamarkupfalse% +\isacommand{from}\ AB\ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}{\isacharquery}B{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{next}\isanewline +\ \ \isamarkupfalse% +\isacommand{from}\ AB\ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}{\isacharquery}A{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent Note the difference between \isa{{\isacharquery}AB}, a term, and @@ -441,12 +523,15 @@ \isacommand{lemma}\ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequote}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B{\isachardoublequote}\isanewline \ \ \isakeyword{shows}\ {\isachardoublequote}large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequote}{\isacharparenright}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{using}\ AB\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}{\isacharquery}A{\isachardoublequote}\ {\isachardoublequote}{\isacharquery}B{\isachardoublequote}\ \isamarkupfalse% +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent Command \isakeyword{using} can appear before a proof @@ -468,19 +553,26 @@ \isamarkuptrue% \isacommand{lemma}\ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequote}A\ {\isasymor}\ B{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}B\ {\isasymor}\ A{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\ {\isacharminus}\isanewline +\ \ \isamarkupfalse% +\isacommand{from}\ AB\ \isamarkupfalse% +\isacommand{show}\ {\isacharquery}thesis\isanewline +\ \ \isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{assume}\ A\ \isamarkupfalse% +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline +\ \ \isamarkupfalse% +\isacommand{next}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{assume}\ B\ \isamarkupfalse% +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline +\ \ \isamarkupfalse% +\isacommand{qed}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \isamarkupsubsection{Predicate calculus% } @@ -497,12 +589,21 @@ \isamarkuptrue% \isacommand{lemma}\ \isakeyword{assumes}\ P{\isacharcolon}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ P\ x{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ % +\isamarkupcmt{\isa{allI}: \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymforall}x{\isachardot}\ {\isacharquery}P\ x}% +} +\isanewline +\ \ \isamarkupfalse% +\isacommand{fix}\ a\isanewline +\ \ \isamarkupfalse% +\isacommand{from}\ P\ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}P{\isacharparenleft}f\ a{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\ \ % +\isamarkupcmt{\isa{allE}: \isa{{\isasymlbrakk}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x{\isacharsemicolon}\ {\isacharquery}P\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isacharquery}R{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R}% +} +\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent Note that in the proof we have chosen to call the bound @@ -514,16 +615,29 @@ \isamarkuptrue% \isacommand{lemma}\ \isakeyword{assumes}\ Pf{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\ {\isacharminus}\isanewline +\ \ \isamarkupfalse% +\isacommand{from}\ Pf\ \isamarkupfalse% +\isacommand{show}\ {\isacharquery}thesis\isanewline +\ \ \isamarkupfalse% +\isacommand{proof}\ \ \ \ \ \ \ \ \ \ \ \ \ \ % +\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}% +} +\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{fix}\ x\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\ \ % +\isamarkupcmt{\isa{exI}: \isa{{\isacharquery}P\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isasymexists}x{\isachardot}\ {\isacharquery}P\ x}% +} +\isanewline +\ \ \isamarkupfalse% +\isacommand{qed}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent Explicit $\exists$-elimination as seen above can become @@ -534,13 +648,16 @@ \isamarkuptrue% \isacommand{lemma}\ \isakeyword{assumes}\ Pf{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\ {\isacharminus}\isanewline +\ \ \isamarkupfalse% +\isacommand{from}\ Pf\ \isamarkupfalse% +\isacommand{obtain}\ x\ \isakeyword{where}\ {\isachardoublequote}P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline +\ \ \isamarkupfalse% +\isacommand{thus}\ {\isachardoublequote}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent Note how the proof text follows the usual mathematical style @@ -555,16 +672,21 @@ \isamarkuptrue% \isacommand{lemma}\ \isakeyword{assumes}\ ex{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ {\isasymforall}y{\isachardot}\ P\ x\ y{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ {\isasymexists}x{\isachardot}\ P\ x\ y{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \isamarkupfalse% +\isacommand{fix}\ y\isanewline +\ \ \isamarkupfalse% +\isacommand{from}\ ex\ \isamarkupfalse% +\isacommand{obtain}\ x\ \isakeyword{where}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ P\ x\ y{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline +\ \ \isamarkupfalse% +\isacommand{hence}\ {\isachardoublequote}P\ x\ y{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline +\ \ \isamarkupfalse% +\isacommand{thus}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P\ x\ y{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \isamarkupsubsection{Making bigger steps% } @@ -579,28 +701,43 @@ \isamarkuptrue% \isacommand{theorem}\ {\isachardoublequote}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \isamarkupfalse% +\isacommand{let}\ {\isacharquery}S\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymnotin}\ f\ x{\isacharbraceright}{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}{\isacharquery}S\ {\isasymnotin}\ range\ f{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}{\isacharquery}S\ {\isasymin}\ range\ f{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{then}\ \isamarkupfalse% +\isacommand{obtain}\ y\ \isakeyword{where}\ fy{\isacharcolon}\ {\isachardoublequote}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{show}\ False\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{proof}\ cases\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequote}\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{with}\ fy\ \isamarkupfalse% +\isacommand{show}\ False\ \isamarkupfalse% +\isacommand{by}\ blast\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{next}\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequote}\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{with}\ fy\ \isamarkupfalse% +\isacommand{show}\ False\ \isamarkupfalse% +\isacommand{by}\ blast\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{qed}\isanewline +\ \ \isamarkupfalse% +\isacommand{qed}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -624,34 +761,53 @@ \isamarkuptrue% \isacommand{theorem}\ {\isachardoublequote}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \isamarkupfalse% +\isacommand{let}\ {\isacharquery}S\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymnotin}\ f\ x{\isacharbraceright}{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}{\isacharquery}S\ {\isasymnotin}\ range\ f{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}{\isacharquery}S\ {\isasymin}\ range\ f{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{then}\ \isamarkupfalse% +\isacommand{obtain}\ y\ \isakeyword{where}\ fy{\isacharcolon}\ {\isachardoublequote}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequote}\ \isamarkupfalse% +\isacommand{{\isachardot}{\isachardot}}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{show}\ False\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{proof}\ cases\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequote}\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{hence}\ {\isachardoublequote}y\ {\isasymnotin}\ f\ y{\isachardoublequote}\ \ \ \isamarkupfalse% +\isacommand{by}\ simp\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{hence}\ {\isachardoublequote}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequote}\ \ \ \ \isamarkupfalse% +\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}fy{\isacharparenright}\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{thus}\ False\ \ \ \ \ \ \ \ \ \isamarkupfalse% +\isacommand{by}\ contradiction\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{next}\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequote}\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{hence}\ {\isachardoublequote}y\ {\isasymin}\ f\ y{\isachardoublequote}\ \ \ \isamarkupfalse% +\isacommand{by}\ simp\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{hence}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequote}\ \ \ \ \isamarkupfalse% +\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}fy{\isacharparenright}\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{thus}\ False\ \ \ \ \ \ \ \ \ \isamarkupfalse% +\isacommand{by}\ contradiction\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{qed}\isanewline +\ \ \isamarkupfalse% +\isacommand{qed}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent Method \isa{contradiction} succeeds if both $P$ and @@ -664,7 +820,7 @@ \isamarkuptrue% \isacommand{theorem}\ {\isachardoublequote}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{by}\ best\isamarkupfalse% % \isamarkupsubsection{Raw proof blocks% } @@ -680,19 +836,28 @@ \isamarkupfalse% \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \isamarkupfalse% +\isacommand{fix}\ x\ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{fix}\ y\ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}A\ x\ y\ {\isasymand}\ B\ x\ y{\isachardoublequote}\isanewline +\ \ \ \ \ \ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}C\ x\ y{\isachardoublequote}\ \isamarkupfalse% +\isacommand{sorry}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{qed}\isanewline +\ \ \isamarkupfalse% +\isacommand{qed}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent Since we are only interested in the decomposition and not the @@ -706,17 +871,24 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\ {\isacharminus}\isanewline +\ \ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}{\isasymAnd}x\ y{\isachardot}\ {\isasymlbrakk}\ A\ x\ y{\isacharsemicolon}\ B\ x\ y\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{proof}\ {\isacharminus}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{fix}\ x\ y\ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}A\ x\ y{\isachardoublequote}\ {\isachardoublequote}B\ x\ y{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}C\ x\ y{\isachardoublequote}\ \isamarkupfalse% +\isacommand{sorry}\isanewline +\ \ \isamarkupfalse% +\isacommand{qed}\isanewline +\ \ \isamarkupfalse% +\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse% +\isacommand{by}\ blast\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent @@ -726,16 +898,20 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\ {\isacharminus}\isanewline +\ \ \isamarkupfalse% +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse% +\isacommand{fix}\ x\ y\ \isamarkupfalse% +\isacommand{assume}\ {\isachardoublequote}A\ x\ y{\isachardoublequote}\ {\isachardoublequote}B\ x\ y{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}C\ x\ y{\isachardoublequote}\ \isamarkupfalse% +\isacommand{sorry}\ \isamarkupfalse% +\isacommand{{\isacharbraceright}}\isanewline +\ \ \isamarkupfalse% +\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse% +\isacommand{by}\ blast\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent The result of the raw proof block is the same theorem @@ -771,31 +947,67 @@ % \renewcommand{\isamarkupcmt}[1]{#1} \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\ {\isacharminus}\isanewline +\ \ \isamarkupfalse% +\isacommand{have}\ {\isachardoublequote}P\isactrlisub {\isadigit{1}}\ {\isasymor}\ P\isactrlisub {\isadigit{2}}\ {\isasymor}\ P\isactrlisub {\isadigit{3}}{\isachardoublequote}\ \isamarkupfalse% +\ % +\isamarkupcmt{\dots% +} +\isanewline +\ \ \isamarkupfalse% +\isacommand{moreover}\isanewline +\ \ \isamarkupfalse% +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse% +\isacommand{assume}\ P\isactrlisub {\isadigit{1}}\isanewline +\ \ \ \ % +\isamarkupcmt{\dots% +} +\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{have}\ {\isacharquery}thesis\ \isamarkupfalse% +\ % +\isamarkupcmt{\dots% +} +\ \isamarkupfalse% +\isacommand{{\isacharbraceright}}\isanewline +\ \ \isamarkupfalse% +\isacommand{moreover}\isanewline +\ \ \isamarkupfalse% +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse% +\isacommand{assume}\ P\isactrlisub {\isadigit{2}}\isanewline +\ \ \ \ % +\isamarkupcmt{\dots% +} +\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{have}\ {\isacharquery}thesis\ \isamarkupfalse% +\ % +\isamarkupcmt{\dots% +} +\ \isamarkupfalse% +\isacommand{{\isacharbraceright}}\isanewline +\ \ \isamarkupfalse% +\isacommand{moreover}\isanewline +\ \ \isamarkupfalse% +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse% +\isacommand{assume}\ P\isactrlisub {\isadigit{3}}\isanewline +\ \ \ \ % +\isamarkupcmt{\dots% +} +\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{have}\ {\isacharquery}thesis\ \isamarkupfalse% +\ % +\isamarkupcmt{\dots% +} +\ \isamarkupfalse% +\isacommand{{\isacharbraceright}}\isanewline +\ \ \isamarkupfalse% +\isacommand{ultimately}\ \isamarkupfalse% +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse% +\isacommand{by}\ blast\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \renewcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}} % @@ -878,7 +1090,7 @@ \ \ \ \ \ \ \ \ \ \ mono{\isacharcolon}\ {\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isachardot}\ x\ {\isachargreater}\ y\ {\isasymLongrightarrow}\ x\ {\isacharplus}{\isacharplus}\ z\ {\isachargreater}\ y\ {\isacharplus}{\isacharplus}\ z{\isachardoublequote}\isanewline \ \ \isakeyword{shows}\ {\isachardoublequote}x\ {\isachargreater}\ y\ {\isasymLongrightarrow}\ z\ {\isacharplus}{\isacharplus}\ x\ {\isachargreater}\ z\ {\isacharplus}{\isacharplus}\ y{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% +\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ comm\ mono{\isacharparenright}\isamarkupfalse% % \begin{isamarkuptext}% \noindent The concrete syntax is dropped at the end of the proof and the @@ -902,10 +1114,11 @@ \isamarkuptrue% \isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x\ y{\isachardot}\ P\ x\ y\ {\isasymand}\ Q\ x\ y{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}R{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\ {\isacharminus}\isanewline +\ \ \isamarkupfalse% +\isacommand{from}\ A\ \isamarkupfalse% +\isacommand{obtain}\ x\ y\ \isakeyword{where}\ P{\isacharcolon}\ {\isachardoublequote}P\ x\ y{\isachardoublequote}\ \isakeyword{and}\ Q{\isacharcolon}\ {\isachardoublequote}Q\ x\ y{\isachardoublequote}\ \ \isamarkupfalse% +\isacommand{by}\ blast\isamarkupfalse% \isamarkupfalse% % \begin{isamarkuptext}% @@ -926,15 +1139,23 @@ \isamarkuptrue% \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ {\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ B{\isachardoublequote}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{proof}\isanewline +\ \ \isamarkupfalse% +\isacommand{assume}\ a{\isacharcolon}\ {\isachardoublequote}A{\isachardoublequote}\isanewline +\ \ \isamarkupfalse% +\isacommand{show}\ {\isachardoublequote}{\isacharparenleft}A\ {\isasymlongrightarrow}B{\isacharparenright}\ {\isasymlongrightarrow}\ B{\isachardoublequote}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}rule\ impI{\isacharparenright}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{apply}{\isacharparenleft}rule\ a{\isacharparenright}\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{apply}\ assumption\isanewline +\ \ \ \ \isamarkupfalse% +\isacommand{done}\isanewline \isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% -\isamarkupfalse% +\isacommand{qed}\isamarkupfalse% % \begin{isamarkuptext}% \noindent You may need to resort to this technique if an