equal
deleted
inserted
replaced
795 |
795 |
796 text {* |
796 text {* |
797 |
797 |
798 Isabelle provides a set of \emph{mono} rules, that are used to split implications |
798 Isabelle provides a set of \emph{mono} rules, that are used to split implications |
799 of similar statements into simpler implication subgoals. These are enhanced |
799 of similar statements into simpler implication subgoals. These are enhanced |
800 with special quotient theorem in the regularization goal. Below we only show |
800 with special quotient theorem in the regularization proof. Below we only show |
801 the versions for the universal quantifier. For the existential quantifier |
801 the versions for the universal quantifier. For the existential quantifier |
802 and abstraction they are analogous. |
802 and abstraction they are analogous. |
803 |
803 |
804 First, bounded universal quantifiers can be removed on the right: |
804 First, bounded universal quantifiers can be removed on the right: |
805 |
805 |
806 @{thm [display, indent=10] ball_reg_right[no_vars]} |
806 @{thm [display, indent=10] ball_reg_right_unfolded[no_vars]} |
807 |
807 |
808 They can be removed anywhere if the relation is an equivalence relation: |
808 They can be removed anywhere if the relation is an equivalence relation: |
809 |
809 |
810 @{thm [display, indent=10] ball_reg_eqv[no_vars]} |
810 @{thm [display, indent=10] ball_reg_eqv[no_vars]} |
811 |
811 |