equal
deleted
inserted
replaced
115 |
115 |
116 \item We allow lifting only some occurrences of quotiented |
116 \item We allow lifting only some occurrences of quotiented |
117 types. Rsp/Prs extended. (used in nominal) |
117 types. Rsp/Prs extended. (used in nominal) |
118 |
118 |
119 \item The quotient package is very modular. Definitions can be added |
119 \item The quotient package is very modular. Definitions can be added |
120 separately, rsp and prs can be proved separately and theorems can |
120 separately, rsp and prs can be proved separately, Quotients and maps |
121 be lifted on a need basis. (useful with type-classes). |
121 can be defined separately and theorems can |
|
122 be lifted on a need basis. (useful with type-classes). |
122 |
123 |
123 \item Can be used both manually (attribute, separate tactics, |
124 \item Can be used both manually (attribute, separate tactics, |
124 rsp/prs databases) and programatically (automated definition of |
125 rsp/prs databases) and programatically (automated definition of |
125 lifted constants, the rsp proof obligations and theorem statement |
126 lifted constants, the rsp proof obligations and theorem statement |
126 translation according to given quotients). |
127 translation according to given quotients). |
429 @{thm (rhs) ball_reg_eqv_range[no_vars]} & = & @{thm (lhs) ball_reg_eqv_range[no_vars]}\\ |
430 @{thm (rhs) ball_reg_eqv_range[no_vars]} & = & @{thm (lhs) ball_reg_eqv_range[no_vars]}\\ |
430 @{thm (rhs) bex_reg_eqv_range[no_vars]} & = & @{thm (lhs) bex_reg_eqv_range[no_vars]} |
431 @{thm (rhs) bex_reg_eqv_range[no_vars]} & = & @{thm (lhs) bex_reg_eqv_range[no_vars]} |
431 \end{eqnarray} |
432 \end{eqnarray} |
432 \end{lemma} |
433 \end{lemma} |
433 |
434 |
|
435 Monos. |
|
436 |
434 Other lemmas used in regularization: |
437 Other lemmas used in regularization: |
435 @{thm [display] ball_reg_eqv[no_vars]} |
438 @{thm [display] ball_reg_eqv[no_vars]} |
436 @{thm [display] bex_reg_eqv[no_vars]} |
|
437 @{thm [display] babs_reg_eqv[no_vars]} |
439 @{thm [display] babs_reg_eqv[no_vars]} |
438 @{thm [display] babs_simp[no_vars]} |
440 @{thm [display] babs_simp[no_vars]} |
439 |
441 |
440 @{thm [display] ball_reg_right[no_vars]} |
442 @{thm [display] ball_reg_right[no_vars]} |
|
443 |
|
444 *} |
|
445 |
|
446 (* |
441 @{thm [display] bex_reg_left[no_vars]} |
447 @{thm [display] bex_reg_left[no_vars]} |
442 @{thm [display] bex1_bexeq_reg[no_vars]} |
448 @{thm [display] bex1_bexeq_reg[no_vars]} |
443 |
449 @{thm [display] bex_reg_eqv[no_vars]} |
444 *} |
450 *) |
445 |
451 |
446 subsection {* Injection *} |
452 subsection {* Injection *} |
447 |
453 |
448 text {* |
454 text {* |
449 |
455 |
463 |
469 |
464 text {* Preservation of quantifiers, abstractions, relations, quotient-constants |
470 text {* Preservation of quantifiers, abstractions, relations, quotient-constants |
465 (definitions) and user given constant preservation lemmas *} |
471 (definitions) and user given constant preservation lemmas *} |
466 |
472 |
467 section {* Examples *} |
473 section {* Examples *} |
|
474 |
|
475 |
468 |
476 |
469 section {* Related Work *} |
477 section {* Related Work *} |
470 |
478 |
471 text {* |
479 text {* |
472 \begin{itemize} |
480 \begin{itemize} |