equal
deleted
inserted
replaced
480 The following term @{text "Reduce X ES"} repeatedly removes characteriztion equations |
480 The following term @{text "Reduce X ES"} repeatedly removes characteriztion equations |
481 for unknowns other than @{text "X"} until one is left. |
481 for unknowns other than @{text "X"} until one is left. |
482 *} |
482 *} |
483 |
483 |
484 abbreviation |
484 abbreviation |
485 "Test ES \<equiv> card ES \<noteq> 1" |
485 "Cond ES \<equiv> card ES \<noteq> 1" |
486 |
486 |
487 definition |
487 definition |
488 "Solve X ES \<equiv> while Test (Iter X) ES" |
488 "Solve X ES \<equiv> while Cond (Iter X) ES" |
489 |
489 |
490 text {* |
490 text {* |
491 Since the @{text "while"} combinator from HOL library is used to implement @{text "Solve X ES"}, |
491 Since the @{text "while"} combinator from HOL library is used to implement @{text "Solve X ES"}, |
492 the induction principle @{thm [source] while_rule} is used to proved the desired properties |
492 the induction principle @{thm [source] while_rule} is used to proved the desired properties |
493 of @{text "Solve X ES"}. For this purpose, an invariant predicate @{text "invariant"} is defined |
493 of @{text "Solve X ES"}. For this purpose, an invariant predicate @{text "invariant"} is defined |