305 \end{isamarkuptext}% |
305 \end{isamarkuptext}% |
306 \isamarkuptrue% |
306 \isamarkuptrue% |
307 \isacommand{interpretation}\isamarkupfalse% |
307 \isacommand{interpretation}\isamarkupfalse% |
308 \ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline |
308 \ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline |
309 \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline |
309 \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline |
310 \ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline |
310 \ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}meet{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline |
311 \ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ dvd\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline |
311 \ \ \ \ \isakeyword{and}\ nat{\isacharunderscore}dvd{\isacharunderscore}join{\isacharunderscore}eq{\isacharcolon}\ {\isachardoublequoteopen}lattice{\isachardot}join\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline |
312 % |
312 % |
313 \isadelimproof |
313 \isadelimproof |
314 % |
314 % |
315 \endisadelimproof |
315 \endisadelimproof |
316 % |
316 % |
328 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
328 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
329 \ auto\ {\isacharbrackleft}{\isadigit{1}}{\isacharbrackright}\isanewline |
329 \ auto\ {\isacharbrackleft}{\isadigit{1}}{\isacharbrackright}\isanewline |
330 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
330 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
331 \ {\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequoteopen}lcm\ x\ y{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline |
331 \ {\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isachardoublequoteopen}lcm\ x\ y{\isachardoublequoteclose}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline |
332 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
332 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
333 \ {\isacharparenleft}auto\ intro{\isacharcolon}\ lcm{\isacharunderscore}dvd{\isadigit{1}}\ lcm{\isacharunderscore}dvd{\isadigit{2}}\ lcm{\isacharunderscore}least{\isacharparenright}\isanewline |
333 \ {\isacharparenleft}auto\ intro{\isacharcolon}\ nat{\isacharunderscore}lcm{\isacharunderscore}least{\isacharparenright}\isanewline |
334 \ \ \ \ \isacommand{done}\isamarkupfalse% |
334 \ \ \ \ \isacommand{done}\isamarkupfalse% |
335 \isanewline |
335 \isanewline |
336 \ \ \isacommand{then}\isamarkupfalse% |
336 \ \ \isacommand{then}\isamarkupfalse% |
337 \ \isacommand{interpret}\isamarkupfalse% |
337 \ \isacommand{interpret}\isamarkupfalse% |
338 \ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% |
338 \ nat{\isacharunderscore}dvd{\isacharcolon}\ lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\ \isacommand{{\isachardot}}\isamarkupfalse% |
340 \ \ \isacommand{show}\isamarkupfalse% |
340 \ \ \isacommand{show}\isamarkupfalse% |
341 \ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline |
341 \ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline |
342 \ \ \ \ \isacommand{by}\isamarkupfalse% |
342 \ \ \ \ \isacommand{by}\isamarkupfalse% |
343 \ {\isacharparenleft}rule\ nat{\isacharunderscore}dvd{\isacharunderscore}less{\isacharunderscore}eq{\isacharparenright}\isanewline |
343 \ {\isacharparenleft}rule\ nat{\isacharunderscore}dvd{\isacharunderscore}less{\isacharunderscore}eq{\isacharparenright}\isanewline |
344 \ \ \isacommand{show}\isamarkupfalse% |
344 \ \ \isacommand{show}\isamarkupfalse% |
345 \ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline |
345 \ {\isachardoublequoteopen}lattice{\isachardot}meet\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline |
346 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
346 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
347 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq{\isacharparenright}\isanewline |
347 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq{\isacharparenright}\isanewline |
348 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
348 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
349 \ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}meet{\isacharunderscore}def{\isacharparenright}\isanewline |
349 \ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}meet{\isacharunderscore}def{\isacharparenright}\isanewline |
350 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
350 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
352 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
352 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
353 \ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}is{\isacharunderscore}inf{\isacharunderscore}def{\isacharparenright}\isanewline |
353 \ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}is{\isacharunderscore}inf{\isacharunderscore}def{\isacharparenright}\isanewline |
354 \ \ \ \ \isacommand{by}\isamarkupfalse% |
354 \ \ \ \ \isacommand{by}\isamarkupfalse% |
355 \ auto\isanewline |
355 \ auto\isanewline |
356 \ \ \isacommand{show}\isamarkupfalse% |
356 \ \ \isacommand{show}\isamarkupfalse% |
357 \ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ dvd\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline |
357 \ {\isachardoublequoteopen}lattice{\isachardot}join\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline |
358 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
358 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
359 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq{\isacharparenright}\isanewline |
359 \ {\isacharparenleft}auto\ simp\ add{\isacharcolon}\ expand{\isacharunderscore}fun{\isacharunderscore}eq{\isacharparenright}\isanewline |
360 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
360 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
361 \ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}join{\isacharunderscore}def{\isacharparenright}\isanewline |
361 \ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}join{\isacharunderscore}def{\isacharparenright}\isanewline |
362 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
362 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
363 \ {\isacharparenleft}rule\ the{\isacharunderscore}equality{\isacharparenright}\isanewline |
363 \ {\isacharparenleft}rule\ the{\isacharunderscore}equality{\isacharparenright}\isanewline |
364 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
364 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
365 \ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}\isanewline |
365 \ {\isacharparenleft}unfold\ nat{\isacharunderscore}dvd{\isachardot}is{\isacharunderscore}sup{\isacharunderscore}def{\isacharparenright}\isanewline |
366 \ \ \ \ \isacommand{by}\isamarkupfalse% |
366 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
367 \ {\isacharparenleft}auto\ intro{\isacharcolon}\ lcm{\isacharunderscore}dvd{\isadigit{1}}\ lcm{\isacharunderscore}dvd{\isadigit{2}}\ lcm{\isacharunderscore}least{\isacharparenright}\isanewline |
367 \ {\isacharparenleft}auto\ intro{\isacharcolon}\ nat{\isacharunderscore}lcm{\isacharunderscore}least\ iff{\isacharcolon}\ nat{\isacharunderscore}lcm{\isacharunderscore}unique{\isacharparenright}\isanewline |
|
368 \ \ \ \ \isacommand{done}\isamarkupfalse% |
|
369 \isanewline |
368 \isacommand{qed}\isamarkupfalse% |
370 \isacommand{qed}\isamarkupfalse% |
369 % |
371 % |
370 \endisatagproof |
372 \endisatagproof |
371 {\isafoldproof}% |
373 {\isafoldproof}% |
372 % |
374 % |
405 \isatagvisible |
407 \isatagvisible |
406 \isacommand{interpretation}\isamarkupfalse% |
408 \isacommand{interpretation}\isamarkupfalse% |
407 \ nat{\isacharunderscore}dvd{\isacharcolon}\isanewline |
409 \ nat{\isacharunderscore}dvd{\isacharcolon}\isanewline |
408 \ \ distrib{\isacharunderscore}lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline |
410 \ \ distrib{\isacharunderscore}lattice\ {\isachardoublequoteopen}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline |
409 \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline |
411 \ \ \isakeyword{where}\ {\isachardoublequoteopen}partial{\isacharunderscore}order{\isachardot}less\ op\ dvd\ {\isacharparenleft}x{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ y\ {\isacharequal}\ {\isacharparenleft}x\ dvd\ y\ {\isasymand}\ x\ {\isasymnoteq}\ y{\isacharparenright}{\isachardoublequoteclose}\isanewline |
410 \ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ op\ dvd\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline |
412 \ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}meet\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ gcd{\isachardoublequoteclose}\isanewline |
411 \ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ op\ dvd\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline |
413 \ \ \ \ \isakeyword{and}\ {\isachardoublequoteopen}lattice{\isachardot}join\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isacharequal}\ lcm{\isachardoublequoteclose}\isanewline |
412 \isacommand{proof}\isamarkupfalse% |
414 \isacommand{proof}\isamarkupfalse% |
413 \ {\isacharminus}\isanewline |
415 \ {\isacharminus}\isanewline |
414 \ \ \isacommand{show}\isamarkupfalse% |
416 \ \ \isacommand{show}\isamarkupfalse% |
415 \ {\isachardoublequoteopen}distrib{\isacharunderscore}lattice\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline |
417 \ {\isachardoublequoteopen}distrib{\isacharunderscore}lattice\ {\isacharparenleft}op\ dvd\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ bool{\isacharparenright}{\isachardoublequoteclose}\isanewline |
416 \ \ \ \ \isacommand{apply}\isamarkupfalse% |
418 \ \ \ \ \isacommand{apply}\isamarkupfalse% |