40 \mbox{\isa{\isacommand{have}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} & prove local result \\ |
40 \mbox{\isa{\isacommand{have}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} & prove local result \\ |
41 \mbox{\isa{\isacommand{show}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} & prove local result, refining some goal \\ |
41 \mbox{\isa{\isacommand{show}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} & prove local result, refining some goal \\ |
42 \mbox{\isa{\isacommand{using}}}~\isa{a} & indicate use of additional facts \\ |
42 \mbox{\isa{\isacommand{using}}}~\isa{a} & indicate use of additional facts \\ |
43 \mbox{\isa{\isacommand{unfolding}}}~\isa{a} & unfold definitional equations \\ |
43 \mbox{\isa{\isacommand{unfolding}}}~\isa{a} & unfold definitional equations \\ |
44 \mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}~\dots~\mbox{\isa{\isacommand{qed}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} & indicate proof structure and refinements \\ |
44 \mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}~\dots~\mbox{\isa{\isacommand{qed}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} & indicate proof structure and refinements \\ |
45 \mbox{\isa{\isacommand{{\isacharbraceleft}}}}~\dots~\mbox{\isa{\isacommand{{\isacharbraceright}}}} & indicate explicit blocks \\ |
45 \mbox{\isa{\isacommand{{\isacharbraceleft}}}}~\isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\mbox{\isa{\isacommand{{\isacharbraceright}}}} & indicate explicit blocks \\ |
46 \mbox{\isa{\isacommand{next}}} & switch blocks \\ |
46 \mbox{\isa{\isacommand{next}}} & switch blocks \\ |
47 \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b{\isachardoublequote}} & reconsider facts \\ |
47 \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}a\ {\isacharequal}\ b{\isachardoublequote}} & reconsider facts \\ |
48 \mbox{\isa{\isacommand{let}}}~\isa{{\isachardoublequote}p\ {\isacharequal}\ t{\isachardoublequote}} & abbreviate terms by higher-order matching \\ |
48 \mbox{\isa{\isacommand{let}}}~\isa{{\isachardoublequote}p\ {\isacharequal}\ t{\isachardoublequote}} & abbreviate terms by higher-order matching \\ |
49 \end{tabular} |
49 \end{tabular} |
50 |
50 |
51 \begin{matharray}{rcl} |
51 \medskip |
52 \isa{{\isachardoublequote}theory{\isasymdash}stmt{\isachardoublequote}} & = & \mbox{\isa{\isacommand{theorem}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props\ proof{\isachardoublequote}} \Or \mbox{\isa{\isacommand{definition}}}~\dots \Or \dots \\[1ex] |
52 |
|
53 \begin{tabular}{rcl} |
|
54 \isa{{\isachardoublequote}theory{\isasymdash}stmt{\isachardoublequote}} & = & \mbox{\isa{\isacommand{theorem}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props\ proof\ \ {\isacharbar}{\isachardoublequote}}~~\mbox{\isa{\isacommand{definition}}}~\isa{{\isachardoublequote}{\isasymdots}\ \ {\isacharbar}\ \ {\isasymdots}{\isachardoublequote}} \\[1ex] |
53 \isa{{\isachardoublequote}proof{\isachardoublequote}} & = & \isa{{\isachardoublequote}prfx\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}method\ stmt\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\mbox{\isa{\isacommand{qed}}}~\isa{method} \\ |
55 \isa{{\isachardoublequote}proof{\isachardoublequote}} & = & \isa{{\isachardoublequote}prfx\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}method\ stmt\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\mbox{\isa{\isacommand{qed}}}~\isa{method} \\ |
54 & \Or & \isa{{\isachardoublequote}prfx\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\mbox{\isa{\isacommand{done}}} \\[1ex] |
56 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \isa{{\isachardoublequote}prfx\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\mbox{\isa{\isacommand{done}}} \\[1ex] |
55 \isa{prfx} & = & \mbox{\isa{\isacommand{apply}}}~\isa{method} \\ |
57 \isa{prfx} & = & \mbox{\isa{\isacommand{apply}}}~\isa{method} \\ |
56 & \Or & \mbox{\isa{\isacommand{using}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} \\ |
58 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{using}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} \\ |
57 & \Or & \mbox{\isa{\isacommand{unfolding}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} \\ |
59 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{unfolding}}}~\isa{{\isachardoublequote}facts{\isachardoublequote}} \\ |
58 \isa{stmt} & = & \mbox{\isa{\isacommand{{\isacharbraceleft}}}}~\isa{{\isachardoublequote}stmt\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\mbox{\isa{\isacommand{{\isacharbraceright}}}} \\ |
60 \isa{stmt} & = & \mbox{\isa{\isacommand{{\isacharbraceleft}}}}~\isa{{\isachardoublequote}stmt\isactrlsup {\isacharasterisk}{\isachardoublequote}}~\mbox{\isa{\isacommand{{\isacharbraceright}}}} \\ |
59 & \Or & \mbox{\isa{\isacommand{next}}} \\ |
61 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{next}}} \\ |
60 & \Or & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ facts{\isachardoublequote}} \\ |
62 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}name\ {\isacharequal}\ facts{\isachardoublequote}} \\ |
61 & \Or & \mbox{\isa{\isacommand{let}}}~\isa{{\isachardoublequote}term\ {\isacharequal}\ term{\isachardoublequote}} \\ |
63 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{let}}}~\isa{{\isachardoublequote}term\ {\isacharequal}\ term{\isachardoublequote}} \\ |
62 & \Or & \mbox{\isa{\isacommand{fix}}}~\isa{{\isachardoublequote}var\isactrlsup {\isacharplus}{\isachardoublequote}} \\ |
64 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{fix}}}~\isa{{\isachardoublequote}var\isactrlsup {\isacharplus}{\isachardoublequote}} \\ |
63 & \Or & \mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props{\isachardoublequote}} \\ |
65 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props{\isachardoublequote}} \\ |
64 & \Or & \mbox{\isa{\isacommand{then}}}\isa{{\isachardoublequote}\isactrlsup {\isacharquery}{\isachardoublequote}}~\isa{goal} \\ |
66 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{then}}}\isa{{\isachardoublequote}\isactrlsup {\isacharquery}{\isachardoublequote}}~\isa{goal} \\ |
65 \isa{goal} & = & \mbox{\isa{\isacommand{have}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props\ proof{\isachardoublequote}} \\ |
67 \isa{goal} & = & \mbox{\isa{\isacommand{have}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props\ proof{\isachardoublequote}} \\ |
66 & \Or & \mbox{\isa{\isacommand{show}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props\ proof{\isachardoublequote}} \\ |
68 & \isa{{\isachardoublequote}{\isacharbar}{\isachardoublequote}} & \mbox{\isa{\isacommand{show}}}~\isa{{\isachardoublequote}name{\isacharcolon}\ props\ proof{\isachardoublequote}} \\ |
67 \end{matharray}% |
69 \end{tabular}% |
68 \end{isamarkuptext}% |
70 \end{isamarkuptext}% |
69 \isamarkuptrue% |
71 \isamarkuptrue% |
70 % |
72 % |
71 \isamarkupsubsection{Abbreviations and synonyms% |
73 \isamarkupsubsection{Abbreviations and synonyms% |
72 } |
74 } |
73 \isamarkuptrue% |
75 \isamarkuptrue% |
74 % |
76 % |
75 \begin{isamarkuptext}% |
77 \begin{isamarkuptext}% |
76 \begin{matharray}{rcl} |
78 \begin{tabular}{rcl} |
77 \mbox{\isa{\isacommand{by}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}{\isachardoublequote}} & \equiv & \mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}~\mbox{\isa{\isacommand{qed}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} \\ |
79 \mbox{\isa{\isacommand{by}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}\ m\isactrlsub {\isadigit{2}}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & |
78 \mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}} & \equiv & \mbox{\isa{\isacommand{by}}}~\isa{rule} \\ |
80 \mbox{\isa{\isacommand{proof}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{1}}{\isachardoublequote}}~\mbox{\isa{\isacommand{qed}}}~\isa{{\isachardoublequote}m\isactrlsub {\isadigit{2}}{\isachardoublequote}} \\ |
79 \mbox{\isa{\isacommand{{\isachardot}}}} & \equiv & \mbox{\isa{\isacommand{by}}}~\isa{this} \\ |
81 \mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{by}}}~\isa{rule} \\ |
80 \mbox{\isa{\isacommand{hence}}} & \equiv & \mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{have}}} \\ |
82 \mbox{\isa{\isacommand{{\isachardot}}}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{by}}}~\isa{this} \\ |
81 \mbox{\isa{\isacommand{thus}}} & \equiv & \mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{show}}} \\ |
83 \mbox{\isa{\isacommand{hence}}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{have}}} \\ |
82 \mbox{\isa{\isacommand{from}}}~\isa{a} & \equiv & \mbox{\isa{\isacommand{note}}}~\isa{a}~\mbox{\isa{\isacommand{then}}} \\ |
84 \mbox{\isa{\isacommand{thus}}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{then}}}~\mbox{\isa{\isacommand{show}}} \\ |
83 \mbox{\isa{\isacommand{with}}}~\isa{a} & \equiv & \mbox{\isa{\isacommand{from}}}~\isa{{\isachardoublequote}a\ {\isasymAND}\ this{\isachardoublequote}} \\[1ex] |
85 \mbox{\isa{\isacommand{from}}}~\isa{a} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{note}}}~\isa{a}~\mbox{\isa{\isacommand{then}}} \\ |
84 \mbox{\isa{\isacommand{from}}}~\isa{this} & \equiv & \mbox{\isa{\isacommand{then}}} \\ |
86 \mbox{\isa{\isacommand{with}}}~\isa{a} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{from}}}~\isa{{\isachardoublequote}a\ {\isasymAND}\ this{\isachardoublequote}} \\[1ex] |
85 \mbox{\isa{\isacommand{from}}}~\isa{this}~\mbox{\isa{\isacommand{have}}} & \equiv & \mbox{\isa{\isacommand{hence}}} \\ |
87 \mbox{\isa{\isacommand{from}}}~\isa{this} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{then}}} \\ |
86 \mbox{\isa{\isacommand{from}}}~\isa{this}~\mbox{\isa{\isacommand{show}}} & \equiv & \mbox{\isa{\isacommand{thus}}} \\ |
88 \mbox{\isa{\isacommand{from}}}~\isa{this}~\mbox{\isa{\isacommand{have}}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{hence}}} \\ |
87 \end{matharray}% |
89 \mbox{\isa{\isacommand{from}}}~\isa{this}~\mbox{\isa{\isacommand{show}}} & \isa{{\isachardoublequote}{\isasymequiv}{\isachardoublequote}} & \mbox{\isa{\isacommand{thus}}} \\ |
|
90 \end{tabular}% |
88 \end{isamarkuptext}% |
91 \end{isamarkuptext}% |
89 \isamarkuptrue% |
92 \isamarkuptrue% |
90 % |
93 % |
91 \isamarkupsubsection{Derived elements% |
94 \isamarkupsubsection{Derived elements% |
92 } |
95 } |
93 \isamarkuptrue% |
96 \isamarkuptrue% |
94 % |
97 % |
95 \begin{isamarkuptext}% |
98 \begin{isamarkuptext}% |
96 \begin{matharray}{rcl} |
99 \begin{tabular}{rcl} |
97 \mbox{\isa{\isacommand{also}}}\isa{{\isachardoublequote}\isactrlsub {\isadigit{0}}{\isachardoublequote}} & \approx & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ this{\isachardoublequote}} \\ |
100 \mbox{\isa{\isacommand{also}}}\isa{{\isachardoublequote}\isactrlsub {\isadigit{0}}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} & |
98 \mbox{\isa{\isacommand{also}}}\isa{{\isachardoublequote}\isactrlsub n\isactrlsub {\isacharplus}\isactrlsub {\isadigit{1}}{\isachardoublequote}} & \approx & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ trans\ {\isacharbrackleft}OF\ calculation\ this{\isacharbrackright}{\isachardoublequote}} \\ |
101 \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ this{\isachardoublequote}} \\ |
99 \mbox{\isa{\isacommand{finally}}} & \approx & \mbox{\isa{\isacommand{also}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\[0.5ex] |
102 \mbox{\isa{\isacommand{also}}}\isa{{\isachardoublequote}\isactrlsub n\isactrlsub {\isacharplus}\isactrlsub {\isadigit{1}}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} & |
100 \mbox{\isa{\isacommand{moreover}}} & \approx & \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ calculation\ this{\isachardoublequote}} \\ |
103 \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ trans\ {\isacharbrackleft}OF\ calculation\ this{\isacharbrackright}{\isachardoublequote}} \\ |
101 \mbox{\isa{\isacommand{ultimately}}} & \approx & \mbox{\isa{\isacommand{moreover}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\[0.5ex] |
104 \mbox{\isa{\isacommand{finally}}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} & |
102 \mbox{\isa{\isacommand{presume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} & \approx & \mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} \\ |
105 \mbox{\isa{\isacommand{also}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\[0.5ex] |
103 \mbox{\isa{\isacommand{def}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}} & \approx & \mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}} \\ |
106 \mbox{\isa{\isacommand{moreover}}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} & |
104 \mbox{\isa{\isacommand{obtain}}}~\isa{{\isachardoublequote}x\ {\isasymWHERE}\ a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} & \approx & \dots~\mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} \\ |
107 \mbox{\isa{\isacommand{note}}}~\isa{{\isachardoublequote}calculation\ {\isacharequal}\ calculation\ this{\isachardoublequote}} \\ |
105 \mbox{\isa{\isacommand{case}}}~\isa{c} & \approx & \mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} \\ |
108 \mbox{\isa{\isacommand{ultimately}}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} & |
106 \mbox{\isa{\isacommand{sorry}}} & \approx & \mbox{\isa{\isacommand{by}}}~\isa{cheating} \\ |
109 \mbox{\isa{\isacommand{moreover}}}~\mbox{\isa{\isacommand{from}}}~\isa{calculation} \\[0.5ex] |
107 \end{matharray}% |
110 \mbox{\isa{\isacommand{presume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} & |
|
111 \mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} \\ |
|
112 \mbox{\isa{\isacommand{def}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} & |
|
113 \mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ x\ {\isasymequiv}\ t{\isachardoublequote}} \\ |
|
114 \mbox{\isa{\isacommand{obtain}}}~\isa{{\isachardoublequote}x\ {\isasymWHERE}\ a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} & |
|
115 \isa{{\isachardoublequote}{\isasymdots}{\isachardoublequote}}~\mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}a{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} \\ |
|
116 \mbox{\isa{\isacommand{case}}}~\isa{c} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} & |
|
117 \mbox{\isa{\isacommand{fix}}}~\isa{x}~\mbox{\isa{\isacommand{assume}}}~\isa{{\isachardoublequote}c{\isacharcolon}\ {\isasymphi}{\isachardoublequote}} \\ |
|
118 \mbox{\isa{\isacommand{sorry}}} & \isa{{\isachardoublequote}{\isasymapprox}{\isachardoublequote}} & |
|
119 \mbox{\isa{\isacommand{by}}}~\isa{cheating} \\ |
|
120 \end{tabular}% |
108 \end{isamarkuptext}% |
121 \end{isamarkuptext}% |
109 \isamarkuptrue% |
122 \isamarkuptrue% |
110 % |
123 % |
111 \isamarkupsubsection{Diagnostic commands% |
124 \isamarkupsubsection{Diagnostic commands% |
112 } |
125 } |