445 a\ +\ b\ =\ b\ +\ a% |
445 a\ +\ b\ =\ b\ +\ a% |
446 \rulenamedx{add.commute}\isanewline |
446 \rulenamedx{add.commute}\isanewline |
447 a\ +\ (b\ +\ c)\ =\ b\ +\ (a\ +\ c) |
447 a\ +\ (b\ +\ c)\ =\ b\ +\ (a\ +\ c) |
448 \rulename{add.left_commute} |
448 \rulename{add.left_commute} |
449 \end{isabelle} |
449 \end{isabelle} |
450 The name \isa{add_ac}\index{*add_ac (theorems)} |
450 The name \isa{ac_simps}\index{*ac_simps (theorems)} |
451 refers to the list of all three theorems; similarly |
451 refers to the list of all three theorems; similarly |
452 there is \isa{mult_ac}.\index{*mult_ac (theorems)} |
452 there is \isa{ac_simps}.\index{*ac_simps (theorems)} |
453 They are all proved for semirings and therefore hold for all numeric types. |
453 They are all proved for semirings and therefore hold for all numeric types. |
454 |
454 |
455 Here is an example of the sorting effect. Start |
455 Here is an example of the sorting effect. Start |
456 with this goal, which involves type \isa{nat}. |
456 with this goal, which involves type \isa{nat}. |
457 \begin{isabelle} |
457 \begin{isabelle} |
458 \ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\ |
458 \ 1.\ Suc\ (i\ +\ j\ *\ l\ *\ k\ +\ m\ *\ n)\ =\ |
459 f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l) |
459 f\ (n\ *\ m\ +\ i\ +\ k\ *\ j\ *\ l) |
460 \end{isabelle} |
460 \end{isabelle} |
461 % |
461 % |
462 Simplify using \isa{add_ac} and \isa{mult_ac}. |
462 Simplify using \isa{ac_simps} and \isa{ac_simps}. |
463 \begin{isabelle} |
463 \begin{isabelle} |
464 \isacommand{apply}\ (simp\ add:\ add_ac\ mult_ac) |
464 \isacommand{apply}\ (simp\ add:\ ac_simps\ ac_simps) |
465 \end{isabelle} |
465 \end{isabelle} |
466 % |
466 % |
467 Here is the resulting subgoal. |
467 Here is the resulting subgoal. |
468 \begin{isabelle} |
468 \begin{isabelle} |
469 \ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\ |
469 \ 1.\ Suc\ (i\ +\ (m\ *\ n\ +\ j\ *\ (k\ *\ l)))\ |