462 *} |
462 *} |
463 |
463 |
464 subsection {* Proving Regularization *} |
464 subsection {* Proving Regularization *} |
465 |
465 |
466 text {* |
466 text {* |
467 Isabelle provides |
467 |
468 |
468 Isabelle provides a set of \emph{mono} rules, that are used to split implications |
469 |
469 of similar statements into simpler implication subgoals. These are enchanced |
470 |
470 with special quotient theorem in the regularization goal. Below we only show |
471 Separtion of regularization from injection thanks to the following 2 lemmas: |
471 the versions for the universal quantifier. For the existential quantifier |
472 \begin{lemma} |
472 and abstraction they are analoguous with some symmetry. |
473 If @{term R2} is an equivalence relation, then: |
473 |
474 \begin{eqnarray} |
474 First, bounded universal quantifiers can be removed on the right: |
475 @{thm (rhs) ball_reg_eqv_range[no_vars]} & = & @{thm (lhs) ball_reg_eqv_range[no_vars]}\\ |
475 |
476 @{thm (rhs) bex_reg_eqv_range[no_vars]} & = & @{thm (lhs) bex_reg_eqv_range[no_vars]} |
476 @{thm [display] ball_reg_right[no_vars]} |
477 \end{eqnarray} |
477 |
478 \end{lemma} |
478 They can be removed anywhere if the relation is an equivalence relation: |
479 |
479 |
480 Monos. |
|
481 |
|
482 Other lemmas used in regularization: |
|
483 @{thm [display] ball_reg_eqv[no_vars]} |
480 @{thm [display] ball_reg_eqv[no_vars]} |
484 @{thm [display] babs_reg_eqv[no_vars]} |
481 |
485 @{thm [display] babs_simp[no_vars]} |
482 And finally it can be removed anywhere if @{term R2} is an equivalence relation, then: |
486 |
483 \[ |
487 @{thm [display] ball_reg_right[no_vars]} |
484 @{thm (rhs) ball_reg_eqv_range[no_vars]} = @{thm (lhs) ball_reg_eqv_range[no_vars]} |
|
485 \] |
|
486 |
|
487 The last theorem is new in comparison with Homeier's package; it allows separating |
|
488 regularization from injection. |
488 |
489 |
489 *} |
490 *} |
490 |
491 |
491 (* |
492 (* |
|
493 @{thm (rhs) bex_reg_eqv_range[no_vars]} = @{thm (lhs) bex_reg_eqv_range[no_vars]} |
492 @{thm [display] bex_reg_left[no_vars]} |
494 @{thm [display] bex_reg_left[no_vars]} |
493 @{thm [display] bex1_bexeq_reg[no_vars]} |
495 @{thm [display] bex1_bexeq_reg[no_vars]} |
494 @{thm [display] bex_reg_eqv[no_vars]} |
496 @{thm [display] bex_reg_eqv[no_vars]} |
|
497 @{thm [display] babs_reg_eqv[no_vars]} |
|
498 @{thm [display] babs_simp[no_vars]} |
495 *) |
499 *) |
496 |
500 |
497 subsection {* Injection *} |
501 subsection {* Injection *} |
498 |
502 |
499 text {* |
503 text {* |