350 \end{tabular} |
350 \end{tabular} |
351 \end{center} |
351 \end{center} |
352 |
352 |
353 Apart from the last 2 points the definition is same as the one implemented in |
353 Apart from the last 2 points the definition is same as the one implemented in |
354 in Homeier's HOL package. Adding composition in last two cases is necessary |
354 in Homeier's HOL package. Adding composition in last two cases is necessary |
355 for compositional quotients. We ilustrate the different behaviour of the |
355 for compositional quotients. We illustrate the different behaviour of the |
356 definition by showing the derived definition of @{term fconcat}: |
356 definition by showing the derived definition of @{term fconcat}: |
357 |
357 |
358 @{thm fconcat_def[no_vars]} |
358 @{thm fconcat_def[no_vars]} |
359 |
359 |
360 The aggregate @{term Abs} function takes a finite set of finite sets |
360 The aggregate @{term Abs} function takes a finite set of finite sets |
542 \item @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"} |
542 \item @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"} |
543 \item @{text "REG (v\<^isub>1, v\<^isub>2) = v\<^isub>1"} |
543 \item @{text "REG (v\<^isub>1, v\<^isub>2) = v\<^isub>1"} |
544 \item @{text "REG (c\<^isub>1, c\<^isub>2) = c\<^isub>1"} |
544 \item @{text "REG (c\<^isub>1, c\<^isub>2) = c\<^isub>1"} |
545 \end{itemize} |
545 \end{itemize} |
546 |
546 |
547 In the above definition we ommited the cases for existential quantifiers |
547 In the above definition we omitted the cases for existential quantifiers |
548 and unique existential quantifiers, as they are very similar to the cases |
548 and unique existential quantifiers, as they are very similar to the cases |
549 for the universal quantifier. |
549 for the universal quantifier. |
550 |
550 |
551 Next we define the function @{text INJ} which takes the statement of |
551 Next we define the function @{text INJ} which takes the statement of |
552 the regularized theorems and the statement of the lifted theorem both as |
552 the regularized theorems and the statement of the lifted theorem both as |
553 terms and returns the statment of the injected theorem: |
553 terms and returns the statement of the injected theorem: |
554 |
554 |
555 \begin{itemize} |
555 \begin{itemize} |
556 \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) = \<lambda>x. (INJ (t, s)"} |
556 \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) = \<lambda>x. (INJ (t, s)"} |
557 \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"} |
557 \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"} |
558 \item @{text "INJ ((\<lambda>x \<in> R. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x \<in> R. (INJ (t, s))))"} |
558 \item @{text "INJ ((\<lambda>x \<in> R. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x \<in> R. (INJ (t, s))))"} |
564 \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) = c\<^isub>1"} |
564 \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) = c\<^isub>1"} |
565 \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"} |
565 \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"} |
566 \end{itemize} |
566 \end{itemize} |
567 |
567 |
568 For existential quantifiers and unique existential quantifiers it is |
568 For existential quantifiers and unique existential quantifiers it is |
569 defined similarily to the universal one. |
569 defined similarly to the universal one. |
570 |
570 |
571 *} |
571 *} |
572 |
572 |
573 subsection {* Proof procedure *} |
573 subsection {* Proof procedure *} |
574 |
574 |
608 subsection {* Proving Regularization *} |
608 subsection {* Proving Regularization *} |
609 |
609 |
610 text {* |
610 text {* |
611 |
611 |
612 Isabelle provides a set of \emph{mono} rules, that are used to split implications |
612 Isabelle provides a set of \emph{mono} rules, that are used to split implications |
613 of similar statements into simpler implication subgoals. These are enchanced |
613 of similar statements into simpler implication subgoals. These are enhanced |
614 with special quotient theorem in the regularization goal. Below we only show |
614 with special quotient theorem in the regularization goal. Below we only show |
615 the versions for the universal quantifier. For the existential quantifier |
615 the versions for the universal quantifier. For the existential quantifier |
616 and abstraction they are analoguous with some symmetry. |
616 and abstraction they are analogous with some symmetry. |
617 |
617 |
618 First, bounded universal quantifiers can be removed on the right: |
618 First, bounded universal quantifiers can be removed on the right: |
619 |
619 |
620 @{thm [display] ball_reg_right[no_vars]} |
620 @{thm [display] ball_reg_right[no_vars]} |
621 |
621 |
725 @{text "lemma (op \<approx> \<Longrightarrow> op \<approx> \<Longrightarrow> op \<approx>) plus_raw plus_raw"} |
725 @{text "lemma (op \<approx> \<Longrightarrow> op \<approx> \<Longrightarrow> op \<approx>) plus_raw plus_raw"} |
726 |
726 |
727 Can be proved automatically by the system just by unfolding the definition |
727 Can be proved automatically by the system just by unfolding the definition |
728 of @{term "op \<Longrightarrow>"}. |
728 of @{term "op \<Longrightarrow>"}. |
729 |
729 |
730 Now the user can either prove a lifted lemma explicitely: |
730 Now the user can either prove a lifted lemma explicitly: |
731 |
731 |
732 @{text "lemma 0 + i = i by lifting plus_zero_raw"} |
732 @{text "lemma 0 + i = i by lifting plus_zero_raw"} |
733 |
733 |
734 Or in this simple case use the automated translation mechanism: |
734 Or in this simple case use the automated translation mechanism: |
735 |
735 |