equal
deleted
inserted
replaced
117 \ {\isadigit{1}}{\isachardot}\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}\ j{\isacharparenright}{\isachardot}\ j\ {\isacharless}\ i\ {\isasymand}\ i\ {\isasymle}\ N{\isacharbraceright}\ {\isasymsubseteq}\ measure\ {\isacharparenleft}op\ {\isacharminus}\ N{\isacharparenright}% |
117 \ {\isadigit{1}}{\isachardot}\ {\isacharbraceleft}{\isacharparenleft}i{\isacharcomma}\ j{\isacharparenright}{\isachardot}\ j\ {\isacharless}\ i\ {\isasymand}\ i\ {\isasymle}\ N{\isacharbraceright}\ {\isasymsubseteq}\ measure\ {\isacharparenleft}op\ {\isacharminus}\ N{\isacharparenright}% |
118 \end{isabelle} |
118 \end{isabelle} |
119 |
119 |
120 \noindent |
120 \noindent |
121 The inclusion remains to be proved. After unfolding some definitions, |
121 The inclusion remains to be proved. After unfolding some definitions, |
122 we are left with simple arithmetic:% |
122 we are left with simple arithmetic that is dispatched automatically.% |
123 \end{isamarkuptxt}% |
|
124 \isamarkuptrue% |
|
125 \isacommand{apply}\isamarkupfalse% |
|
126 \ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}% |
|
127 \begin{isamarkuptxt}% |
|
128 \begin{isabelle}% |
|
129 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}a\ b{\isachardot}\ {\isasymlbrakk}b\ {\isacharless}\ a{\isacharsemicolon}\ a\ {\isasymle}\ N{\isasymrbrakk}\ {\isasymLongrightarrow}\ N\ {\isacharminus}\ a\ {\isacharless}\ N\ {\isacharminus}\ b% |
|
130 \end{isabelle} |
|
131 |
|
132 \noindent |
|
133 And that is dispatched automatically:% |
|
134 \end{isamarkuptxt}% |
123 \end{isamarkuptxt}% |
135 \isamarkuptrue% |
124 \isamarkuptrue% |
136 \isacommand{by}\isamarkupfalse% |
125 \isacommand{by}\isamarkupfalse% |
137 \ arith% |
126 \ {\isacharparenleft}clarify{\isacharcomma}\ simp\ add{\isacharcolon}\ measure{\isacharunderscore}def\ inv{\isacharunderscore}image{\isacharunderscore}def{\isacharparenright}% |
138 \endisatagproof |
127 \endisatagproof |
139 {\isafoldproof}% |
128 {\isafoldproof}% |
140 % |
129 % |
141 \isadelimproof |
130 \isadelimproof |
142 % |
131 % |