24 % |
24 % |
25 \endisadelimML |
25 \endisadelimML |
26 % |
26 % |
27 \isatagML |
27 \isatagML |
28 \isacommand{ML}\isamarkupfalse% |
28 \isacommand{ML}\isamarkupfalse% |
29 \ {\isachardoublequoteopen}Pretty{\isachardot}margin{\isacharunderscore}default\ {\isacharcolon}{\isacharequal}\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}% |
29 \ {\isaliteral{22}{\isachardoublequoteopen}}Pretty{\isaliteral{2E}{\isachardot}}margin{\isaliteral{5F}{\isacharunderscore}}default\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{6}}{\isadigit{4}}{\isaliteral{22}{\isachardoublequoteclose}}% |
30 \endisatagML |
30 \endisatagML |
31 {\isafoldML}% |
31 {\isafoldML}% |
32 % |
32 % |
33 \isadelimML |
33 \isadelimML |
34 \isanewline |
34 \isanewline |
35 % |
35 % |
36 \endisadelimML |
36 \endisadelimML |
37 \isacommand{declare}\isamarkupfalse% |
37 \isacommand{declare}\isamarkupfalse% |
38 \ {\isacharbrackleft}{\isacharbrackleft}thy{\isacharunderscore}output{\isacharunderscore}indent\ {\isacharequal}\ {\isadigit{0}}{\isacharbrackright}{\isacharbrackright}% |
38 \ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}thy{\isaliteral{5F}{\isacharunderscore}}output{\isaliteral{5F}{\isacharunderscore}}indent\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}% |
39 \begin{isamarkuptext}% |
39 \begin{isamarkuptext}% |
40 numeric literals; default simprules; can re-orient% |
40 numeric literals; default simprules; can re-orient% |
41 \end{isamarkuptext}% |
41 \end{isamarkuptext}% |
42 \isamarkuptrue% |
42 \isamarkuptrue% |
43 \isacommand{lemma}\isamarkupfalse% |
43 \isacommand{lemma}\isamarkupfalse% |
44 \ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m{\isachardoublequoteclose}% |
44 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ m\ {\isaliteral{3D}{\isacharequal}}\ m\ {\isaliteral{2B}{\isacharplus}}\ m{\isaliteral{22}{\isachardoublequoteclose}}% |
45 \isadelimproof |
45 \isadelimproof |
46 % |
46 % |
47 \endisadelimproof |
47 \endisadelimproof |
48 % |
48 % |
49 \isatagproof |
49 \isatagproof |
50 % |
50 % |
51 \begin{isamarkuptxt}% |
51 \begin{isamarkuptxt}% |
52 \begin{isabelle}% |
52 \begin{isabelle}% |
53 \ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m% |
53 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ m\ {\isaliteral{3D}{\isacharequal}}\ m\ {\isaliteral{2B}{\isacharplus}}\ m% |
54 \end{isabelle}% |
54 \end{isabelle}% |
55 \end{isamarkuptxt}% |
55 \end{isamarkuptxt}% |
56 \isamarkuptrue% |
56 \isamarkuptrue% |
57 \isacommand{oops}\isamarkupfalse% |
57 \isacommand{oops}\isamarkupfalse% |
58 % |
58 % |
63 % |
63 % |
64 \endisadelimproof |
64 \endisadelimproof |
65 \isanewline |
65 \isanewline |
66 \isanewline |
66 \isanewline |
67 \isacommand{consts}\isamarkupfalse% |
67 \isacommand{consts}\isamarkupfalse% |
68 \ h\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline |
68 \ h\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
69 \isacommand{recdef}\isamarkupfalse% |
69 \isacommand{recdef}\isamarkupfalse% |
70 \ h\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline |
70 \ h\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
71 {\isachardoublequoteopen}h\ i\ {\isacharequal}\ {\isacharparenleft}if\ i\ {\isacharequal}\ {\isadigit{3}}\ then\ {\isadigit{2}}\ else\ i{\isacharparenright}{\isachardoublequoteclose}% |
71 {\isaliteral{22}{\isachardoublequoteopen}}h\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ then\ {\isadigit{2}}\ else\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
72 \begin{isamarkuptext}% |
72 \begin{isamarkuptext}% |
73 \isa{h\ {\isadigit{3}}\ {\isacharequal}\ {\isadigit{2}}} |
73 \isa{h\ {\isadigit{3}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}} |
74 \isa{h\ i\ {\isacharequal}\ i}% |
74 \isa{h\ i\ {\isaliteral{3D}{\isacharequal}}\ i}% |
75 \end{isamarkuptext}% |
75 \end{isamarkuptext}% |
76 \isamarkuptrue% |
76 \isamarkuptrue% |
77 % |
77 % |
78 \begin{isamarkuptext}% |
78 \begin{isamarkuptext}% |
79 \begin{isabelle}% |
79 \begin{isabelle}% |
80 Numeral{\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}% |
80 Numeral{\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}% |
81 \end{isabelle} |
81 \end{isabelle} |
82 \rulename{numeral_0_eq_0} |
82 \rulename{numeral_0_eq_0} |
83 |
83 |
84 \begin{isabelle}% |
84 \begin{isabelle}% |
85 Numeral{\isadigit{1}}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharparenright}% |
85 Numeral{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}% |
86 \end{isabelle} |
86 \end{isabelle} |
87 \rulename{numeral_1_eq_1} |
87 \rulename{numeral_1_eq_1} |
88 |
88 |
89 \begin{isabelle}% |
89 \begin{isabelle}% |
90 {\isadigit{2}}\ {\isacharplus}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}% |
90 {\isadigit{2}}\ {\isaliteral{2B}{\isacharplus}}\ n\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}% |
91 \end{isabelle} |
91 \end{isabelle} |
92 \rulename{add_2_eq_Suc} |
92 \rulename{add_2_eq_Suc} |
93 |
93 |
94 \begin{isabelle}% |
94 \begin{isabelle}% |
95 n\ {\isacharplus}\ {\isadigit{2}}\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}% |
95 n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}% |
96 \end{isabelle} |
96 \end{isabelle} |
97 \rulename{add_2_eq_Suc'} |
97 \rulename{add_2_eq_Suc'} |
98 |
98 |
99 \begin{isabelle}% |
99 \begin{isabelle}% |
100 a\ {\isacharplus}\ b\ {\isacharplus}\ c\ {\isacharequal}\ a\ {\isacharplus}\ {\isacharparenleft}b\ {\isacharplus}\ c{\isacharparenright}% |
100 a\ {\isaliteral{2B}{\isacharplus}}\ b\ {\isaliteral{2B}{\isacharplus}}\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2B}{\isacharplus}}\ c{\isaliteral{29}{\isacharparenright}}% |
101 \end{isabelle} |
101 \end{isabelle} |
102 \rulename{add_assoc} |
102 \rulename{add_assoc} |
103 |
103 |
104 \begin{isabelle}% |
104 \begin{isabelle}% |
105 a\ {\isacharplus}\ b\ {\isacharequal}\ b\ {\isacharplus}\ a% |
105 a\ {\isaliteral{2B}{\isacharplus}}\ b\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2B}{\isacharplus}}\ a% |
106 \end{isabelle} |
106 \end{isabelle} |
107 \rulename{add_commute} |
107 \rulename{add_commute} |
108 |
108 |
109 \begin{isabelle}% |
109 \begin{isabelle}% |
110 b\ {\isacharplus}\ {\isacharparenleft}a\ {\isacharplus}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharplus}\ {\isacharparenleft}b\ {\isacharplus}\ c{\isacharparenright}% |
110 b\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2B}{\isacharplus}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2B}{\isacharplus}}\ c{\isaliteral{29}{\isacharparenright}}% |
111 \end{isabelle} |
111 \end{isabelle} |
112 \rulename{add_left_commute} |
112 \rulename{add_left_commute} |
113 |
113 |
114 these form add_ac; similarly there is mult_ac% |
114 these form add_ac; similarly there is mult_ac% |
115 \end{isamarkuptext}% |
115 \end{isamarkuptext}% |
116 \isamarkuptrue% |
116 \isamarkuptrue% |
117 \isacommand{lemma}\isamarkupfalse% |
117 \isacommand{lemma}\isamarkupfalse% |
118 \ {\isachardoublequoteopen}Suc{\isacharparenleft}i\ {\isacharplus}\ j{\isacharasterisk}l{\isacharasterisk}k\ {\isacharplus}\ m{\isacharasterisk}n{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}n{\isacharasterisk}m\ {\isacharplus}\ i\ {\isacharplus}\ k{\isacharasterisk}j{\isacharasterisk}l{\isacharparenright}{\isachardoublequoteclose}% |
118 \ {\isaliteral{22}{\isachardoublequoteopen}}Suc{\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ j{\isaliteral{2A}{\isacharasterisk}}l{\isaliteral{2A}{\isacharasterisk}}k\ {\isaliteral{2B}{\isacharplus}}\ m{\isaliteral{2A}{\isacharasterisk}}n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2A}{\isacharasterisk}}m\ {\isaliteral{2B}{\isacharplus}}\ i\ {\isaliteral{2B}{\isacharplus}}\ k{\isaliteral{2A}{\isacharasterisk}}j{\isaliteral{2A}{\isacharasterisk}}l{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
119 \isadelimproof |
119 \isadelimproof |
120 % |
120 % |
121 \endisadelimproof |
121 \endisadelimproof |
122 % |
122 % |
123 \isatagproof |
123 \isatagproof |
124 % |
124 % |
125 \begin{isamarkuptxt}% |
125 \begin{isamarkuptxt}% |
126 \begin{isabelle}% |
126 \begin{isabelle}% |
127 \ {\isadigit{1}}{\isachardot}\ Suc\ {\isacharparenleft}i\ {\isacharplus}\ j\ {\isacharasterisk}\ l\ {\isacharasterisk}\ k\ {\isacharplus}\ m\ {\isacharasterisk}\ n{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}n\ {\isacharasterisk}\ m\ {\isacharplus}\ i\ {\isacharplus}\ k\ {\isacharasterisk}\ j\ {\isacharasterisk}\ l{\isacharparenright}% |
127 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ j\ {\isaliteral{2A}{\isacharasterisk}}\ l\ {\isaliteral{2A}{\isacharasterisk}}\ k\ {\isaliteral{2B}{\isacharplus}}\ m\ {\isaliteral{2A}{\isacharasterisk}}\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2A}{\isacharasterisk}}\ m\ {\isaliteral{2B}{\isacharplus}}\ i\ {\isaliteral{2B}{\isacharplus}}\ k\ {\isaliteral{2A}{\isacharasterisk}}\ j\ {\isaliteral{2A}{\isacharasterisk}}\ l{\isaliteral{29}{\isacharparenright}}% |
128 \end{isabelle}% |
128 \end{isabelle}% |
129 \end{isamarkuptxt}% |
129 \end{isamarkuptxt}% |
130 \isamarkuptrue% |
130 \isamarkuptrue% |
131 \isacommand{apply}\isamarkupfalse% |
131 \isacommand{apply}\isamarkupfalse% |
132 \ {\isacharparenleft}simp\ add{\isacharcolon}\ add{\isacharunderscore}ac\ mult{\isacharunderscore}ac{\isacharparenright}% |
132 \ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ add{\isaliteral{5F}{\isacharunderscore}}ac\ mult{\isaliteral{5F}{\isacharunderscore}}ac{\isaliteral{29}{\isacharparenright}}% |
133 \begin{isamarkuptxt}% |
133 \begin{isamarkuptxt}% |
134 \begin{isabelle}% |
134 \begin{isabelle}% |
135 \ {\isadigit{1}}{\isachardot}\ Suc\ {\isacharparenleft}i\ {\isacharplus}\ {\isacharparenleft}m\ {\isacharasterisk}\ n\ {\isacharplus}\ j\ {\isacharasterisk}\ {\isacharparenleft}k\ {\isacharasterisk}\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline |
135 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{2A}{\isacharasterisk}}\ n\ {\isaliteral{2B}{\isacharplus}}\ j\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{2A}{\isacharasterisk}}\ l{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
136 \isaindent{\ {\isadigit{1}}{\isachardot}\ }f\ {\isacharparenleft}i\ {\isacharplus}\ {\isacharparenleft}m\ {\isacharasterisk}\ n\ {\isacharplus}\ j\ {\isacharasterisk}\ {\isacharparenleft}k\ {\isacharasterisk}\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}% |
136 \isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ }f\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{2A}{\isacharasterisk}}\ n\ {\isaliteral{2B}{\isacharplus}}\ j\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{2A}{\isacharasterisk}}\ l{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}% |
137 \end{isabelle}% |
137 \end{isabelle}% |
138 \end{isamarkuptxt}% |
138 \end{isamarkuptxt}% |
139 \isamarkuptrue% |
139 \isamarkuptrue% |
140 \isacommand{oops}\isamarkupfalse% |
140 \isacommand{oops}\isamarkupfalse% |
141 % |
141 % |
146 % |
146 % |
147 \endisadelimproof |
147 \endisadelimproof |
148 % |
148 % |
149 \begin{isamarkuptext}% |
149 \begin{isamarkuptext}% |
150 \begin{isabelle}% |
150 \begin{isabelle}% |
151 m\ {\isasymle}\ n\ {\isasymLongrightarrow}\ m\ div\ k\ {\isasymle}\ n\ div\ k% |
151 m\ {\isaliteral{5C3C6C653E}{\isasymle}}\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ m\ div\ k\ {\isaliteral{5C3C6C653E}{\isasymle}}\ n\ div\ k% |
152 \end{isabelle} |
152 \end{isabelle} |
153 \rulename{div_le_mono} |
153 \rulename{div_le_mono} |
154 |
154 |
155 \begin{isabelle}% |
155 \begin{isabelle}% |
156 {\isacharparenleft}m\ {\isacharminus}\ n{\isacharparenright}\ {\isacharasterisk}\ k\ {\isacharequal}\ m\ {\isacharasterisk}\ k\ {\isacharminus}\ n\ {\isacharasterisk}\ k% |
156 {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{2D}{\isacharminus}}\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ k\ {\isaliteral{3D}{\isacharequal}}\ m\ {\isaliteral{2A}{\isacharasterisk}}\ k\ {\isaliteral{2D}{\isacharminus}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ k% |
157 \end{isabelle} |
157 \end{isabelle} |
158 \rulename{diff_mult_distrib} |
158 \rulename{diff_mult_distrib} |
159 |
159 |
160 \begin{isabelle}% |
160 \begin{isabelle}% |
161 m\ mod\ n\ {\isacharasterisk}\ k\ {\isacharequal}\ m\ {\isacharasterisk}\ k\ mod\ {\isacharparenleft}n\ {\isacharasterisk}\ k{\isacharparenright}% |
161 m\ mod\ n\ {\isaliteral{2A}{\isacharasterisk}}\ k\ {\isaliteral{3D}{\isacharequal}}\ m\ {\isaliteral{2A}{\isacharasterisk}}\ k\ mod\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2A}{\isacharasterisk}}\ k{\isaliteral{29}{\isacharparenright}}% |
162 \end{isabelle} |
162 \end{isabelle} |
163 \rulename{mod_mult_distrib} |
163 \rulename{mod_mult_distrib} |
164 |
164 |
165 \begin{isabelle}% |
165 \begin{isabelle}% |
166 P\ {\isacharparenleft}a\ {\isacharminus}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenleft}a\ {\isacharless}\ b\ {\isasymlongrightarrow}\ P\ {\isadigit{0}}{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}d{\isachardot}\ a\ {\isacharequal}\ b\ {\isacharplus}\ d\ {\isasymlongrightarrow}\ P\ d{\isacharparenright}{\isacharparenright}% |
166 P\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2D}{\isacharminus}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{3C}{\isacharless}}\ b\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}d{\isaliteral{2E}{\isachardot}}\ a\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2B}{\isacharplus}}\ d\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P\ d{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}% |
167 \end{isabelle} |
167 \end{isabelle} |
168 \rulename{nat_diff_split}% |
168 \rulename{nat_diff_split}% |
169 \end{isamarkuptext}% |
169 \end{isamarkuptext}% |
170 \isamarkuptrue% |
170 \isamarkuptrue% |
171 \isacommand{lemma}\isamarkupfalse% |
171 \isacommand{lemma}\isamarkupfalse% |
172 \ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ n\ {\isacharminus}\ {\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline |
172 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ n\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
173 % |
173 % |
174 \isadelimproof |
174 \isadelimproof |
175 % |
175 % |
176 \endisadelimproof |
176 \endisadelimproof |
177 % |
177 % |
178 \isatagproof |
178 \isatagproof |
179 \isacommand{apply}\isamarkupfalse% |
179 \isacommand{apply}\isamarkupfalse% |
180 \ {\isacharparenleft}clarsimp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split\ iff\ del{\isacharcolon}\ less{\isacharunderscore}Suc{\isadigit{0}}{\isacharparenright}\isanewline |
180 \ {\isaliteral{28}{\isacharparenleft}}clarsimp\ split{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{5F}{\isacharunderscore}}diff{\isaliteral{5F}{\isacharunderscore}}split\ iff\ del{\isaliteral{3A}{\isacharcolon}}\ less{\isaliteral{5F}{\isacharunderscore}}Suc{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline |
181 \ % |
181 \ % |
182 \isamarkupcmt{\begin{isabelle}% |
182 \isamarkupcmt{\begin{isabelle}% |
183 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}d{\isachardot}\ {\isasymlbrakk}n\ {\isacharless}\ Suc\ {\isadigit{0}}{\isacharsemicolon}\ n\ {\isacharasterisk}\ n\ {\isacharequal}\ Suc\ d{\isasymrbrakk}\ {\isasymLongrightarrow}\ d\ {\isacharequal}\ {\isadigit{0}}% |
183 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}d{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}n\ {\isaliteral{3C}{\isacharless}}\ Suc\ {\isadigit{0}}{\isaliteral{3B}{\isacharsemicolon}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ n\ {\isaliteral{3D}{\isacharequal}}\ Suc\ d{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ d\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}% |
184 \end{isabelle}% |
184 \end{isabelle}% |
185 } |
185 } |
186 \isanewline |
186 \isanewline |
187 \isacommand{apply}\isamarkupfalse% |
187 \isacommand{apply}\isamarkupfalse% |
188 \ {\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequoteopen}n{\isacharequal}{\isadigit{0}}{\isachardoublequoteclose}{\isacharcomma}\ force{\isacharcomma}\ arith{\isacharparenright}\isanewline |
188 \ {\isaliteral{28}{\isacharparenleft}}subgoal{\isaliteral{5F}{\isacharunderscore}}tac\ {\isaliteral{22}{\isachardoublequoteopen}}n{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{2C}{\isacharcomma}}\ force{\isaliteral{2C}{\isacharcomma}}\ arith{\isaliteral{29}{\isacharparenright}}\isanewline |
189 \isacommand{done}\isamarkupfalse% |
189 \isacommand{done}\isamarkupfalse% |
190 % |
190 % |
191 \endisatagproof |
191 \endisatagproof |
192 {\isafoldproof}% |
192 {\isafoldproof}% |
193 % |
193 % |
196 % |
196 % |
197 \endisadelimproof |
197 \endisadelimproof |
198 \isanewline |
198 \isanewline |
199 \isanewline |
199 \isanewline |
200 \isacommand{lemma}\isamarkupfalse% |
200 \isacommand{lemma}\isamarkupfalse% |
201 \ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharminus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ n\ {\isacharminus}\ {\isacharparenleft}{\isadigit{4}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline |
201 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ n\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{4}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
202 % |
202 % |
203 \isadelimproof |
203 \isadelimproof |
204 % |
204 % |
205 \endisadelimproof |
205 \endisadelimproof |
206 % |
206 % |
207 \isatagproof |
207 \isatagproof |
208 \isacommand{apply}\isamarkupfalse% |
208 \isacommand{apply}\isamarkupfalse% |
209 \ {\isacharparenleft}simp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharcomma}\ clarify{\isacharparenright}\isanewline |
209 \ {\isaliteral{28}{\isacharparenleft}}simp\ split{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{5F}{\isacharunderscore}}diff{\isaliteral{5F}{\isacharunderscore}}split{\isaliteral{2C}{\isacharcomma}}\ clarify{\isaliteral{29}{\isacharparenright}}\isanewline |
210 \ % |
210 \ % |
211 \isamarkupcmt{\begin{isabelle}% |
211 \isamarkupcmt{\begin{isabelle}% |
212 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}d{\isachardot}\ {\isasymlbrakk}n\ {\isacharless}\ {\isadigit{2}}{\isacharsemicolon}\ n\ {\isacharasterisk}\ n\ {\isacharequal}\ {\isadigit{4}}\ {\isacharplus}\ d{\isasymrbrakk}\ {\isasymLongrightarrow}\ d\ {\isacharequal}\ {\isadigit{0}}% |
212 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}d{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}n\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ d{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ d\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}% |
213 \end{isabelle}% |
213 \end{isabelle}% |
214 } |
214 } |
215 \isanewline |
215 \isanewline |
216 \isacommand{apply}\isamarkupfalse% |
216 \isacommand{apply}\isamarkupfalse% |
217 \ {\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequoteopen}n{\isacharequal}{\isadigit{0}}\ {\isacharbar}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequoteclose}{\isacharcomma}\ force{\isacharcomma}\ arith{\isacharparenright}\isanewline |
217 \ {\isaliteral{28}{\isacharparenleft}}subgoal{\isaliteral{5F}{\isacharunderscore}}tac\ {\isaliteral{22}{\isachardoublequoteopen}}n{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}\ {\isaliteral{7C}{\isacharbar}}\ n{\isaliteral{3D}{\isacharequal}}{\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{2C}{\isacharcomma}}\ force{\isaliteral{2C}{\isacharcomma}}\ arith{\isaliteral{29}{\isacharparenright}}\isanewline |
218 \isacommand{done}\isamarkupfalse% |
218 \isacommand{done}\isamarkupfalse% |
219 % |
219 % |
220 \endisatagproof |
220 \endisatagproof |
221 {\isafoldproof}% |
221 {\isafoldproof}% |
222 % |
222 % |
224 % |
224 % |
225 \endisadelimproof |
225 \endisadelimproof |
226 % |
226 % |
227 \begin{isamarkuptext}% |
227 \begin{isamarkuptext}% |
228 \begin{isabelle}% |
228 \begin{isabelle}% |
229 m\ mod\ n\ {\isacharequal}\ {\isacharparenleft}if\ m\ {\isacharless}\ n\ then\ m\ else\ {\isacharparenleft}m\ {\isacharminus}\ n{\isacharparenright}\ mod\ n{\isacharparenright}% |
229 m\ mod\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ m\ {\isaliteral{3C}{\isacharless}}\ n\ then\ m\ else\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{2D}{\isacharminus}}\ n{\isaliteral{29}{\isacharparenright}}\ mod\ n{\isaliteral{29}{\isacharparenright}}% |
230 \end{isabelle} |
230 \end{isabelle} |
231 \rulename{mod_if} |
231 \rulename{mod_if} |
232 |
232 |
233 \begin{isabelle}% |
233 \begin{isabelle}% |
234 a\ div\ b\ {\isacharasterisk}\ b\ {\isacharplus}\ a\ mod\ b\ {\isacharequal}\ a% |
234 a\ div\ b\ {\isaliteral{2A}{\isacharasterisk}}\ b\ {\isaliteral{2B}{\isacharplus}}\ a\ mod\ b\ {\isaliteral{3D}{\isacharequal}}\ a% |
235 \end{isabelle} |
235 \end{isabelle} |
236 \rulename{mod_div_equality} |
236 \rulename{mod_div_equality} |
237 |
237 |
238 |
238 |
239 \begin{isabelle}% |
239 \begin{isabelle}% |
240 a\ {\isacharasterisk}\ b\ div\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ div\ c{\isacharparenright}\ {\isacharplus}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ div\ c% |
240 a\ {\isaliteral{2A}{\isacharasterisk}}\ b\ div\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ div\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ div\ c% |
241 \end{isabelle} |
241 \end{isabelle} |
242 \rulename{div_mult1_eq} |
242 \rulename{div_mult1_eq} |
243 |
243 |
244 \begin{isabelle}% |
244 \begin{isabelle}% |
245 a\ {\isacharasterisk}\ b\ mod\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ mod\ c% |
245 a\ {\isaliteral{2A}{\isacharasterisk}}\ b\ mod\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ mod\ c% |
246 \end{isabelle} |
246 \end{isabelle} |
247 \rulename{mod_mult_right_eq} |
247 \rulename{mod_mult_right_eq} |
248 |
248 |
249 \begin{isabelle}% |
249 \begin{isabelle}% |
250 a\ div\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ a\ div\ b\ div\ c% |
250 a\ div\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ div\ b\ div\ c% |
251 \end{isabelle} |
251 \end{isabelle} |
252 \rulename{div_mult2_eq} |
252 \rulename{div_mult2_eq} |
253 |
253 |
254 \begin{isabelle}% |
254 \begin{isabelle}% |
255 a\ mod\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ b\ {\isacharasterisk}\ {\isacharparenleft}a\ div\ b\ mod\ c{\isacharparenright}\ {\isacharplus}\ a\ mod\ b% |
255 a\ mod\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}a\ div\ b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ a\ mod\ b% |
256 \end{isabelle} |
256 \end{isabelle} |
257 \rulename{mod_mult2_eq} |
257 \rulename{mod_mult2_eq} |
258 |
258 |
259 \begin{isabelle}% |
259 \begin{isabelle}% |
260 c\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymLongrightarrow}\ c\ {\isacharasterisk}\ a\ div\ {\isacharparenleft}c\ {\isacharasterisk}\ b{\isacharparenright}\ {\isacharequal}\ a\ div\ b% |
260 c\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ c\ {\isaliteral{2A}{\isacharasterisk}}\ a\ div\ {\isaliteral{28}{\isacharparenleft}}c\ {\isaliteral{2A}{\isacharasterisk}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ div\ b% |
261 \end{isabelle} |
261 \end{isabelle} |
262 \rulename{div_mult_mult1} |
262 \rulename{div_mult_mult1} |
263 |
263 |
264 \begin{isabelle}% |
264 \begin{isabelle}% |
265 a\ div\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}% |
265 a\ div\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}% |
266 \end{isabelle} |
266 \end{isabelle} |
267 \rulename{div_by_0} |
267 \rulename{div_by_0} |
268 |
268 |
269 \begin{isabelle}% |
269 \begin{isabelle}% |
270 a\ mod\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharequal}\ a% |
270 a\ mod\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a% |
271 \end{isabelle} |
271 \end{isabelle} |
272 \rulename{mod_by_0} |
272 \rulename{mod_by_0} |
273 |
273 |
274 \begin{isabelle}% |
274 \begin{isabelle}% |
275 {\isasymlbrakk}m\ dvd\ n{\isacharsemicolon}\ n\ dvd\ m{\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n% |
275 {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}m\ dvd\ n{\isaliteral{3B}{\isacharsemicolon}}\ n\ dvd\ m{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ m\ {\isaliteral{3D}{\isacharequal}}\ n% |
276 \end{isabelle} |
276 \end{isabelle} |
277 \rulename{dvd_antisym} |
277 \rulename{dvd_antisym} |
278 |
278 |
279 \begin{isabelle}% |
279 \begin{isabelle}% |
280 {\isasymlbrakk}a\ dvd\ b{\isacharsemicolon}\ a\ dvd\ c{\isasymrbrakk}\ {\isasymLongrightarrow}\ a\ dvd\ b\ {\isacharplus}\ c% |
280 {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}a\ dvd\ b{\isaliteral{3B}{\isacharsemicolon}}\ a\ dvd\ c{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ dvd\ b\ {\isaliteral{2B}{\isacharplus}}\ c% |
281 \end{isabelle} |
281 \end{isabelle} |
282 \rulename{dvd_add} |
282 \rulename{dvd_add} |
283 |
283 |
284 For the integers, I'd list a few theorems that somehow involve negative |
284 For the integers, I'd list a few theorems that somehow involve negative |
285 numbers.% |
285 numbers.% |
289 \begin{isamarkuptext}% |
289 \begin{isamarkuptext}% |
290 Division, remainder of negatives |
290 Division, remainder of negatives |
291 |
291 |
292 |
292 |
293 \begin{isabelle}% |
293 \begin{isabelle}% |
294 {\isadigit{0}}\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isasymle}\ a\ mod\ b% |
294 {\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ b\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isadigit{0}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ a\ mod\ b% |
295 \end{isabelle} |
295 \end{isabelle} |
296 \rulename{pos_mod_sign} |
296 \rulename{pos_mod_sign} |
297 |
297 |
298 \begin{isabelle}% |
298 \begin{isabelle}% |
299 {\isadigit{0}}\ {\isacharless}\ b\ {\isasymLongrightarrow}\ a\ mod\ b\ {\isacharless}\ b% |
299 {\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ b\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ mod\ b\ {\isaliteral{3C}{\isacharless}}\ b% |
300 \end{isabelle} |
300 \end{isabelle} |
301 \rulename{pos_mod_bound} |
301 \rulename{pos_mod_bound} |
302 |
302 |
303 \begin{isabelle}% |
303 \begin{isabelle}% |
304 b\ {\isacharless}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ a\ mod\ b\ {\isasymle}\ {\isadigit{0}}% |
304 b\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{0}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ mod\ b\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isadigit{0}}% |
305 \end{isabelle} |
305 \end{isabelle} |
306 \rulename{neg_mod_sign} |
306 \rulename{neg_mod_sign} |
307 |
307 |
308 \begin{isabelle}% |
308 \begin{isabelle}% |
309 b\ {\isacharless}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ b\ {\isacharless}\ a\ mod\ b% |
309 b\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{0}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ b\ {\isaliteral{3C}{\isacharless}}\ a\ mod\ b% |
310 \end{isabelle} |
310 \end{isabelle} |
311 \rulename{neg_mod_bound} |
311 \rulename{neg_mod_bound} |
312 |
312 |
313 \begin{isabelle}% |
313 \begin{isabelle}% |
314 {\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ div\ c\ {\isacharequal}\ a\ div\ c\ {\isacharplus}\ b\ div\ c\ {\isacharplus}\ {\isacharparenleft}a\ mod\ c\ {\isacharplus}\ b\ mod\ c{\isacharparenright}\ div\ c% |
314 {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2B}{\isacharplus}}\ b{\isaliteral{29}{\isacharparenright}}\ div\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ div\ c\ {\isaliteral{2B}{\isacharplus}}\ b\ div\ c\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}a\ mod\ c\ {\isaliteral{2B}{\isacharplus}}\ b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ div\ c% |
315 \end{isabelle} |
315 \end{isabelle} |
316 \rulename{zdiv_zadd1_eq} |
316 \rulename{zdiv_zadd1_eq} |
317 |
317 |
318 \begin{isabelle}% |
318 \begin{isabelle}% |
319 {\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ mod\ c\ {\isacharequal}\ {\isacharparenleft}a\ mod\ c\ {\isacharplus}\ b\ mod\ c{\isacharparenright}\ mod\ c% |
319 {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2B}{\isacharplus}}\ b{\isaliteral{29}{\isacharparenright}}\ mod\ c\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a\ mod\ c\ {\isaliteral{2B}{\isacharplus}}\ b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ mod\ c% |
320 \end{isabelle} |
320 \end{isabelle} |
321 \rulename{mod_add_eq} |
321 \rulename{mod_add_eq} |
322 |
322 |
323 \begin{isabelle}% |
323 \begin{isabelle}% |
324 a\ {\isacharasterisk}\ b\ div\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ div\ c{\isacharparenright}\ {\isacharplus}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ div\ c% |
324 a\ {\isaliteral{2A}{\isacharasterisk}}\ b\ div\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ div\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ div\ c% |
325 \end{isabelle} |
325 \end{isabelle} |
326 \rulename{zdiv_zmult1_eq} |
326 \rulename{zdiv_zmult1_eq} |
327 |
327 |
328 \begin{isabelle}% |
328 \begin{isabelle}% |
329 a\ {\isacharasterisk}\ b\ mod\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ mod\ c% |
329 a\ {\isaliteral{2A}{\isacharasterisk}}\ b\ mod\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ mod\ c% |
330 \end{isabelle} |
330 \end{isabelle} |
331 \rulename{zmod_zmult1_eq} |
331 \rulename{zmod_zmult1_eq} |
332 |
332 |
333 \begin{isabelle}% |
333 \begin{isabelle}% |
334 {\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ a\ div\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ a\ div\ b\ div\ c% |
334 {\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ c\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ div\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ div\ b\ div\ c% |
335 \end{isabelle} |
335 \end{isabelle} |
336 \rulename{zdiv_zmult2_eq} |
336 \rulename{zdiv_zmult2_eq} |
337 |
337 |
338 \begin{isabelle}% |
338 \begin{isabelle}% |
339 {\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ a\ mod\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ b\ {\isacharasterisk}\ {\isacharparenleft}a\ div\ b\ mod\ c{\isacharparenright}\ {\isacharplus}\ a\ mod\ b% |
339 {\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ c\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ mod\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}a\ div\ b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ a\ mod\ b% |
340 \end{isabelle} |
340 \end{isabelle} |
341 \rulename{zmod_zmult2_eq}% |
341 \rulename{zmod_zmult2_eq}% |
342 \end{isamarkuptext}% |
342 \end{isamarkuptext}% |
343 \isamarkuptrue% |
343 \isamarkuptrue% |
344 \isacommand{lemma}\isamarkupfalse% |
344 \isacommand{lemma}\isamarkupfalse% |
345 \ {\isachardoublequoteopen}abs\ {\isacharparenleft}x{\isacharplus}y{\isacharparenright}\ {\isasymle}\ abs\ x\ {\isacharplus}\ abs\ {\isacharparenleft}y\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequoteclose}\isanewline |
345 \ {\isaliteral{22}{\isachardoublequoteopen}}abs\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2B}{\isacharplus}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ abs\ x\ {\isaliteral{2B}{\isacharplus}}\ abs\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
346 % |
346 % |
347 \isadelimproof |
347 \isadelimproof |
348 % |
348 % |
349 \endisadelimproof |
349 \endisadelimproof |
350 % |
350 % |
378 % |
378 % |
379 \begin{isamarkuptext}% |
379 \begin{isamarkuptext}% |
380 Induction rules for the Integers |
380 Induction rules for the Integers |
381 |
381 |
382 \begin{isabelle}% |
382 \begin{isabelle}% |
383 {\isasymlbrakk}k\ {\isasymle}\ i{\isacharsemicolon}\ P\ k{\isacharsemicolon}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}k\ {\isasymle}\ i{\isacharsemicolon}\ P\ i{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ i% |
383 {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}k\ {\isaliteral{5C3C6C653E}{\isasymle}}\ i{\isaliteral{3B}{\isacharsemicolon}}\ P\ k{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}i{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}k\ {\isaliteral{5C3C6C653E}{\isasymle}}\ i{\isaliteral{3B}{\isacharsemicolon}}\ P\ i{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ i% |
384 \end{isabelle} |
384 \end{isabelle} |
385 \rulename{int_ge_induct} |
385 \rulename{int_ge_induct} |
386 |
386 |
387 \begin{isabelle}% |
387 \begin{isabelle}% |
388 {\isasymlbrakk}k\ {\isacharless}\ i{\isacharsemicolon}\ P\ {\isacharparenleft}k\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isacharsemicolon}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}k\ {\isacharless}\ i{\isacharsemicolon}\ P\ i{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ i% |
388 {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}k\ {\isaliteral{3C}{\isacharless}}\ i{\isaliteral{3B}{\isacharsemicolon}}\ P\ {\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}i{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}k\ {\isaliteral{3C}{\isacharless}}\ i{\isaliteral{3B}{\isacharsemicolon}}\ P\ i{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ i% |
389 \end{isabelle} |
389 \end{isabelle} |
390 \rulename{int_gr_induct} |
390 \rulename{int_gr_induct} |
391 |
391 |
392 \begin{isabelle}% |
392 \begin{isabelle}% |
393 {\isasymlbrakk}i\ {\isasymle}\ k{\isacharsemicolon}\ P\ k{\isacharsemicolon}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}i\ {\isasymle}\ k{\isacharsemicolon}\ P\ i{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}i\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ i% |
393 {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ k{\isaliteral{3B}{\isacharsemicolon}}\ P\ k{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}i{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ k{\isaliteral{3B}{\isacharsemicolon}}\ P\ i{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ i% |
394 \end{isabelle} |
394 \end{isabelle} |
395 \rulename{int_le_induct} |
395 \rulename{int_le_induct} |
396 |
396 |
397 \begin{isabelle}% |
397 \begin{isabelle}% |
398 {\isasymlbrakk}i\ {\isacharless}\ k{\isacharsemicolon}\ P\ {\isacharparenleft}k\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}{\isacharsemicolon}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}i\ {\isacharless}\ k{\isacharsemicolon}\ P\ i{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}i\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ i% |
398 {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}i\ {\isaliteral{3C}{\isacharless}}\ k{\isaliteral{3B}{\isacharsemicolon}}\ P\ {\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}i{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}i\ {\isaliteral{3C}{\isacharless}}\ k{\isaliteral{3B}{\isacharsemicolon}}\ P\ i{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ i% |
399 \end{isabelle} |
399 \end{isabelle} |
400 \rulename{int_less_induct}% |
400 \rulename{int_less_induct}% |
401 \end{isamarkuptext}% |
401 \end{isamarkuptext}% |
402 \isamarkuptrue% |
402 \isamarkuptrue% |
403 % |
403 % |
404 \begin{isamarkuptext}% |
404 \begin{isamarkuptext}% |
405 FIELDS |
405 FIELDS |
406 |
406 |
407 \begin{isabelle}% |
407 \begin{isabelle}% |
408 x\ {\isacharless}\ y\ {\isasymLongrightarrow}\ {\isasymexists}z{\isachargreater}x{\isachardot}\ z\ {\isacharless}\ y% |
408 x\ {\isaliteral{3C}{\isacharless}}\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}z{\isaliteral{3E}{\isachargreater}}x{\isaliteral{2E}{\isachardot}}\ z\ {\isaliteral{3C}{\isacharless}}\ y% |
409 \end{isabelle} |
409 \end{isabelle} |
410 \rulename{dense} |
410 \rulename{dense} |
411 |
411 |
412 \begin{isabelle}% |
412 \begin{isabelle}% |
413 a\ {\isacharasterisk}\ {\isacharparenleft}b\ {\isacharslash}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharasterisk}\ b\ {\isacharslash}\ c% |
413 a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2F}{\isacharslash}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ b\ {\isaliteral{2F}{\isacharslash}}\ c% |
414 \end{isabelle} |
414 \end{isabelle} |
415 \rulename{times_divide_eq_right} |
415 \rulename{times_divide_eq_right} |
416 |
416 |
417 \begin{isabelle}% |
417 \begin{isabelle}% |
418 b\ {\isacharslash}\ c\ {\isacharasterisk}\ a\ {\isacharequal}\ b\ {\isacharasterisk}\ a\ {\isacharslash}\ c% |
418 b\ {\isaliteral{2F}{\isacharslash}}\ c\ {\isaliteral{2A}{\isacharasterisk}}\ a\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2A}{\isacharasterisk}}\ a\ {\isaliteral{2F}{\isacharslash}}\ c% |
419 \end{isabelle} |
419 \end{isabelle} |
420 \rulename{times_divide_eq_left} |
420 \rulename{times_divide_eq_left} |
421 |
421 |
422 \begin{isabelle}% |
422 \begin{isabelle}% |
423 a\ {\isacharslash}\ {\isacharparenleft}b\ {\isacharslash}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharasterisk}\ c\ {\isacharslash}\ b% |
423 a\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2F}{\isacharslash}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ c\ {\isaliteral{2F}{\isacharslash}}\ b% |
424 \end{isabelle} |
424 \end{isabelle} |
425 \rulename{divide_divide_eq_right} |
425 \rulename{divide_divide_eq_right} |
426 |
426 |
427 \begin{isabelle}% |
427 \begin{isabelle}% |
428 a\ {\isacharslash}\ b\ {\isacharslash}\ c\ {\isacharequal}\ a\ {\isacharslash}\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}% |
428 a\ {\isaliteral{2F}{\isacharslash}}\ b\ {\isaliteral{2F}{\isacharslash}}\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}% |
429 \end{isabelle} |
429 \end{isabelle} |
430 \rulename{divide_divide_eq_left} |
430 \rulename{divide_divide_eq_left} |
431 |
431 |
432 \begin{isabelle}% |
432 \begin{isabelle}% |
433 {\isacharminus}\ {\isacharparenleft}a\ {\isacharslash}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharminus}\ a\ {\isacharslash}\ b% |
433 {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2F}{\isacharslash}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}\ a\ {\isaliteral{2F}{\isacharslash}}\ b% |
434 \end{isabelle} |
434 \end{isabelle} |
435 \rulename{minus_divide_left} |
435 \rulename{minus_divide_left} |
436 |
436 |
437 \begin{isabelle}% |
437 \begin{isabelle}% |
438 {\isacharminus}\ {\isacharparenleft}a\ {\isacharslash}\ b{\isacharparenright}\ {\isacharequal}\ a\ {\isacharslash}\ {\isacharminus}\ b% |
438 {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2F}{\isacharslash}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{2D}{\isacharminus}}\ b% |
439 \end{isabelle} |
439 \end{isabelle} |
440 \rulename{minus_divide_right} |
440 \rulename{minus_divide_right} |
441 |
441 |
442 This last NOT a simprule |
442 This last NOT a simprule |
443 |
443 |
444 \begin{isabelle}% |
444 \begin{isabelle}% |
445 {\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharslash}\ c\ {\isacharequal}\ a\ {\isacharslash}\ c\ {\isacharplus}\ b\ {\isacharslash}\ c% |
445 {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2B}{\isacharplus}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2F}{\isacharslash}}\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2F}{\isacharslash}}\ c\ {\isaliteral{2B}{\isacharplus}}\ b\ {\isaliteral{2F}{\isacharslash}}\ c% |
446 \end{isabelle} |
446 \end{isabelle} |
447 \rulename{add_divide_distrib}% |
447 \rulename{add_divide_distrib}% |
448 \end{isamarkuptext}% |
448 \end{isamarkuptext}% |
449 \isamarkuptrue% |
449 \isamarkuptrue% |
450 \isacommand{lemma}\isamarkupfalse% |
450 \isacommand{lemma}\isamarkupfalse% |
451 \ {\isachardoublequoteopen}{\isadigit{3}}{\isacharslash}{\isadigit{4}}\ {\isacharless}\ {\isacharparenleft}{\isadigit{7}}{\isacharslash}{\isadigit{8}}\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequoteclose}\isanewline |
451 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{3}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{7}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ real{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
452 % |
452 % |
453 \isadelimproof |
453 \isadelimproof |
454 % |
454 % |
455 \endisadelimproof |
455 \endisadelimproof |
456 % |
456 % |
464 \ \isanewline |
464 \ \isanewline |
465 % |
465 % |
466 \endisadelimproof |
466 \endisadelimproof |
467 \isanewline |
467 \isanewline |
468 \isacommand{lemma}\isamarkupfalse% |
468 \isacommand{lemma}\isamarkupfalse% |
469 \ {\isachardoublequoteopen}P\ {\isacharparenleft}{\isacharparenleft}{\isadigit{3}}{\isacharslash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}{\isacharslash}{\isadigit{1}}{\isadigit{5}}\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}% |
469 \ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{8}}{\isaliteral{2F}{\isacharslash}}{\isadigit{1}}{\isadigit{5}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
470 \isadelimproof |
470 \isadelimproof |
471 % |
471 % |
472 \endisadelimproof |
472 \endisadelimproof |
473 % |
473 % |
474 \isatagproof |
474 \isatagproof |
475 % |
475 % |
476 \begin{isamarkuptxt}% |
476 \begin{isamarkuptxt}% |
477 \begin{isabelle}% |
477 \begin{isabelle}% |
478 \ {\isadigit{1}}{\isachardot}\ P\ {\isacharparenleft}{\isadigit{3}}\ {\isacharslash}\ {\isadigit{4}}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}\ {\isacharslash}\ {\isadigit{1}}{\isadigit{5}}{\isacharparenright}{\isacharparenright}% |
478 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ P\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{8}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{1}}{\isadigit{5}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}% |
479 \end{isabelle}% |
479 \end{isabelle}% |
480 \end{isamarkuptxt}% |
480 \end{isamarkuptxt}% |
481 \isamarkuptrue% |
481 \isamarkuptrue% |
482 \isacommand{apply}\isamarkupfalse% |
482 \isacommand{apply}\isamarkupfalse% |
483 \ simp% |
483 \ simp% |
484 \begin{isamarkuptxt}% |
484 \begin{isamarkuptxt}% |
485 \begin{isabelle}% |
485 \begin{isabelle}% |
486 \ {\isadigit{1}}{\isachardot}\ P\ {\isacharparenleft}{\isadigit{2}}\ {\isacharslash}\ {\isadigit{5}}{\isacharparenright}% |
486 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ P\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{5}}{\isaliteral{29}{\isacharparenright}}% |
487 \end{isabelle}% |
487 \end{isabelle}% |
488 \end{isamarkuptxt}% |
488 \end{isamarkuptxt}% |
489 \isamarkuptrue% |
489 \isamarkuptrue% |
490 \isacommand{oops}\isamarkupfalse% |
490 \isacommand{oops}\isamarkupfalse% |
491 % |
491 % |
496 % |
496 % |
497 \endisadelimproof |
497 \endisadelimproof |
498 \isanewline |
498 \isanewline |
499 \isanewline |
499 \isanewline |
500 \isacommand{lemma}\isamarkupfalse% |
500 \isacommand{lemma}\isamarkupfalse% |
501 \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{3}}{\isacharslash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}{\isacharslash}{\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequoteclose}% |
501 \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{8}}{\isaliteral{2F}{\isacharslash}}{\isadigit{1}}{\isadigit{5}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ real{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
502 \isadelimproof |
502 \isadelimproof |
503 % |
503 % |
504 \endisadelimproof |
504 \endisadelimproof |
505 % |
505 % |
506 \isatagproof |
506 \isatagproof |
507 % |
507 % |
508 \begin{isamarkuptxt}% |
508 \begin{isamarkuptxt}% |
509 \begin{isabelle}% |
509 \begin{isabelle}% |
510 \ {\isadigit{1}}{\isachardot}\ {\isadigit{3}}\ {\isacharslash}\ {\isadigit{4}}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}\ {\isacharslash}\ {\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ x% |
510 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{8}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{1}}{\isadigit{5}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}\ x% |
511 \end{isabelle}% |
511 \end{isabelle}% |
512 \end{isamarkuptxt}% |
512 \end{isamarkuptxt}% |
513 \isamarkuptrue% |
513 \isamarkuptrue% |
514 \isacommand{apply}\isamarkupfalse% |
514 \isacommand{apply}\isamarkupfalse% |
515 \ simp% |
515 \ simp% |
516 \begin{isamarkuptxt}% |
516 \begin{isamarkuptxt}% |
517 \begin{isabelle}% |
517 \begin{isabelle}% |
518 \ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ {\isacharless}\ x\ {\isacharasterisk}\ {\isadigit{5}}% |
518 \ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isadigit{2}}\ {\isaliteral{3C}{\isacharless}}\ x\ {\isaliteral{2A}{\isacharasterisk}}\ {\isadigit{5}}% |
519 \end{isabelle}% |
519 \end{isabelle}% |
520 \end{isamarkuptxt}% |
520 \end{isamarkuptxt}% |
521 \isamarkuptrue% |
521 \isamarkuptrue% |
522 \isacommand{oops}\isamarkupfalse% |
522 \isacommand{oops}\isamarkupfalse% |
523 % |
523 % |
532 Ring and Field |
532 Ring and Field |
533 |
533 |
534 Requires a field, or else an ordered ring |
534 Requires a field, or else an ordered ring |
535 |
535 |
536 \begin{isabelle}% |
536 \begin{isabelle}% |
537 {\isacharparenleft}a\ {\isacharasterisk}\ b\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ b\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}{\isacharparenright}% |
537 {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2A}{\isacharasterisk}}\ b\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ b\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}% |
538 \end{isabelle} |
538 \end{isabelle} |
539 \rulename{mult_eq_0_iff} |
539 \rulename{mult_eq_0_iff} |
540 |
540 |
541 \begin{isabelle}% |
541 \begin{isabelle}% |
542 {\isacharparenleft}a\ {\isacharasterisk}\ c\ {\isacharequal}\ b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}% |
542 {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2A}{\isacharasterisk}}\ c\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}c\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{29}{\isacharparenright}}% |
543 \end{isabelle} |
543 \end{isabelle} |
544 \rulename{mult_cancel_right} |
544 \rulename{mult_cancel_right} |
545 |
545 |
546 \begin{isabelle}% |
546 \begin{isabelle}% |
547 {\isacharparenleft}c\ {\isacharasterisk}\ a\ {\isacharequal}\ c\ {\isacharasterisk}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}% |
547 {\isaliteral{28}{\isacharparenleft}}c\ {\isaliteral{2A}{\isacharasterisk}}\ a\ {\isaliteral{3D}{\isacharequal}}\ c\ {\isaliteral{2A}{\isacharasterisk}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}c\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{29}{\isacharparenright}}% |
548 \end{isabelle} |
548 \end{isabelle} |
549 \rulename{mult_cancel_left}% |
549 \rulename{mult_cancel_left}% |
550 \end{isamarkuptext}% |
550 \end{isamarkuptext}% |
551 \isamarkuptrue% |
551 \isamarkuptrue% |
552 % |
552 % |
553 \begin{isamarkuptext}% |
553 \begin{isamarkuptext}% |
554 effect of show sorts on the above |
554 effect of show sorts on the above |
555 |
555 |
556 \begin{isabelle}% |
556 \begin{isabelle}% |
557 {\isacharparenleft}{\isacharparenleft}c{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isacharequal}\isanewline |
557 {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}ring{\isaliteral{5F}{\isacharunderscore}}no{\isaliteral{5F}{\isacharunderscore}}zero{\isaliteral{5F}{\isacharunderscore}}divisors{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}ring{\isaliteral{5F}{\isacharunderscore}}no{\isaliteral{5F}{\isacharunderscore}}zero{\isaliteral{5F}{\isacharunderscore}}divisors{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
558 \isaindent{{\isacharparenleft}}c\ {\isacharasterisk}\ {\isacharparenleft}b{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline |
558 \isaindent{{\isaliteral{28}{\isacharparenleft}}}c\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}ring{\isaliteral{5F}{\isacharunderscore}}no{\isaliteral{5F}{\isacharunderscore}}zero{\isaliteral{5F}{\isacharunderscore}}divisors{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
559 {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}% |
559 {\isaliteral{28}{\isacharparenleft}}c\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}ring{\isaliteral{5F}{\isacharunderscore}}no{\isaliteral{5F}{\isacharunderscore}}zero{\isaliteral{5F}{\isacharunderscore}}divisors{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{29}{\isacharparenright}}% |
560 \end{isabelle} |
560 \end{isabelle} |
561 \rulename{mult_cancel_left}% |
561 \rulename{mult_cancel_left}% |
562 \end{isamarkuptext}% |
562 \end{isamarkuptext}% |
563 \isamarkuptrue% |
563 \isamarkuptrue% |
564 % |
564 % |
565 \begin{isamarkuptext}% |
565 \begin{isamarkuptext}% |
566 absolute value |
566 absolute value |
567 |
567 |
568 \begin{isabelle}% |
568 \begin{isabelle}% |
569 {\isasymbar}a\ {\isacharasterisk}\ b{\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\ {\isacharasterisk}\ {\isasymbar}b{\isasymbar}% |
569 {\isaliteral{5C3C6261723E}{\isasymbar}}a\ {\isaliteral{2A}{\isacharasterisk}}\ b{\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6261723E}{\isasymbar}}a{\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C6261723E}{\isasymbar}}b{\isaliteral{5C3C6261723E}{\isasymbar}}% |
570 \end{isabelle} |
570 \end{isabelle} |
571 \rulename{abs_mult} |
571 \rulename{abs_mult} |
572 |
572 |
573 \begin{isabelle}% |
573 \begin{isabelle}% |
574 {\isacharparenleft}{\isasymbar}a{\isasymbar}\ {\isasymle}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a\ {\isasymle}\ b\ {\isasymand}\ {\isacharminus}\ a\ {\isasymle}\ b{\isacharparenright}% |
574 {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6261723E}{\isasymbar}}a{\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{5C3C6C653E}{\isasymle}}\ b\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{2D}{\isacharminus}}\ a\ {\isaliteral{5C3C6C653E}{\isasymle}}\ b{\isaliteral{29}{\isacharparenright}}% |
575 \end{isabelle} |
575 \end{isabelle} |
576 \rulename{abs_le_iff} |
576 \rulename{abs_le_iff} |
577 |
577 |
578 \begin{isabelle}% |
578 \begin{isabelle}% |
579 {\isasymbar}a\ {\isacharplus}\ b{\isasymbar}\ {\isasymle}\ {\isasymbar}a{\isasymbar}\ {\isacharplus}\ {\isasymbar}b{\isasymbar}% |
579 {\isaliteral{5C3C6261723E}{\isasymbar}}a\ {\isaliteral{2B}{\isacharplus}}\ b{\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{5C3C6261723E}{\isasymbar}}a{\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5C3C6261723E}{\isasymbar}}b{\isaliteral{5C3C6261723E}{\isasymbar}}% |
580 \end{isabelle} |
580 \end{isabelle} |
581 \rulename{abs_triangle_ineq} |
581 \rulename{abs_triangle_ineq} |
582 |
582 |
583 \begin{isabelle}% |
583 \begin{isabelle}% |
584 a\isactrlbsup m\ {\isacharplus}\ n\isactrlesup \ {\isacharequal}\ a\isactrlbsup m\isactrlesup \ {\isacharasterisk}\ a\isactrlbsup n\isactrlesup % |
584 a\isaliteral{5C3C5E627375703E}{}\isactrlbsup m\ {\isaliteral{2B}{\isacharplus}}\ n\isaliteral{5C3C5E657375703E}{}\isactrlesup \ {\isaliteral{3D}{\isacharequal}}\ a\isaliteral{5C3C5E627375703E}{}\isactrlbsup m\isaliteral{5C3C5E657375703E}{}\isactrlesup \ {\isaliteral{2A}{\isacharasterisk}}\ a\isaliteral{5C3C5E627375703E}{}\isactrlbsup n\isaliteral{5C3C5E657375703E}{}\isactrlesup % |
585 \end{isabelle} |
585 \end{isabelle} |
586 \rulename{power_add} |
586 \rulename{power_add} |
587 |
587 |
588 \begin{isabelle}% |
588 \begin{isabelle}% |
589 a\isactrlbsup m\ {\isacharasterisk}\ n\isactrlesup \ {\isacharequal}\ a\isactrlbsup m\isactrlesup \isactrlbsup n\isactrlesup % |
589 a\isaliteral{5C3C5E627375703E}{}\isactrlbsup m\ {\isaliteral{2A}{\isacharasterisk}}\ n\isaliteral{5C3C5E657375703E}{}\isactrlesup \ {\isaliteral{3D}{\isacharequal}}\ a\isaliteral{5C3C5E627375703E}{}\isactrlbsup m\isaliteral{5C3C5E657375703E}{}\isactrlesup \isaliteral{5C3C5E627375703E}{}\isactrlbsup n\isaliteral{5C3C5E657375703E}{}\isactrlesup % |
590 \end{isabelle} |
590 \end{isabelle} |
591 \rulename{power_mult} |
591 \rulename{power_mult} |
592 |
592 |
593 \begin{isabelle}% |
593 \begin{isabelle}% |
594 {\isasymbar}a\isactrlbsup n\isactrlesup {\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\isactrlbsup n\isactrlesup % |
594 {\isaliteral{5C3C6261723E}{\isasymbar}}a\isaliteral{5C3C5E627375703E}{}\isactrlbsup n\isaliteral{5C3C5E657375703E}{}\isactrlesup {\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6261723E}{\isasymbar}}a{\isaliteral{5C3C6261723E}{\isasymbar}}\isaliteral{5C3C5E627375703E}{}\isactrlbsup n\isaliteral{5C3C5E657375703E}{}\isactrlesup % |
595 \end{isabelle} |
595 \end{isabelle} |
596 \rulename{power_abs}% |
596 \rulename{power_abs}% |
597 \end{isamarkuptext}% |
597 \end{isamarkuptext}% |
598 \isamarkuptrue% |
598 \isamarkuptrue% |
599 % |
599 % |