equal
deleted
inserted
replaced
496 (* test *) |
496 (* test *) |
497 partial_function (tailrec) |
497 partial_function (tailrec) |
498 solve |
498 solve |
499 where |
499 where |
500 "solve X ES = (if (card ES = 1) then ES else solve X (Iter X ES))" |
500 "solve X ES = (if (card ES = 1) then ES else solve X (Iter X ES))" |
|
501 |
|
502 thm solve.simps |
501 |
503 |
502 |
504 |
503 text {* |
505 text {* |
504 Since the @{text "while"} combinator from HOL library is used to implement @{text "Solve X ES"}, |
506 Since the @{text "while"} combinator from HOL library is used to implement @{text "Solve X ES"}, |
505 the induction principle @{thm [source] while_rule} is used to proved the desired properties |
507 the induction principle @{thm [source] while_rule} is used to proved the desired properties |