374 it replaces quantifiers and abstractions involving raw types |
374 it replaces quantifiers and abstractions involving raw types |
375 by bounded ones, and equalities involving raw types are replaced |
375 by bounded ones, and equalities involving raw types are replaced |
376 by appropriate aggregate relations. It is defined as follows: |
376 by appropriate aggregate relations. It is defined as follows: |
377 |
377 |
378 \begin{itemize} |
378 \begin{itemize} |
379 \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>y : \<sigma>. s) = \<lambda>x : \<sigma>. REG (t, s)"} |
379 \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<sigma>. s) = \<lambda>x : \<sigma>. REG (t, s)"} |
380 \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>y : \<tau>. s) = \<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"} |
380 \item @{text "REG (\<lambda>x : \<sigma>. t, \<lambda>x : \<tau>. s) = \<lambda>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"} |
381 \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>y : \<sigma>. s) = \<forall>x : \<sigma>. REG (t, s)"} |
381 \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<sigma>. s) = \<forall>x : \<sigma>. REG (t, s)"} |
382 \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>y : \<tau>. s) = \<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"} |
382 \item @{text "REG (\<forall>x : \<sigma>. t, \<forall>x : \<tau>. s) = \<forall>x : \<sigma> \<in> Res (REL (\<sigma>, \<tau>)). REG (t, s)"} |
383 \item @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>) = (op =) : \<sigma>"} |
383 \item @{text "REG ((op =) : \<sigma>, (op =) : \<sigma>) = (op =) : \<sigma>"} |
384 \item @{text "REG ((op =) : \<sigma>, (op =) : \<tau>) = REL (\<sigma>, \<tau>) : \<sigma>"} |
384 \item @{text "REG ((op =) : \<sigma>, (op =) : \<tau>) = REL (\<sigma>, \<tau>) : \<sigma>"} |
385 \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)"} |
385 \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)"} |
386 \item @{text "REG (_, v) = v"} |
386 \item @{text "REG (v\<^isub>1, v\<^isub>2) = v\<^isub>1"} |
387 \item @{text "REG (_, c) = c"} |
387 \item @{text "REG (c\<^isub>1, c\<^isub>2) = c\<^isub>1"} |
388 \end{itemize} |
388 \end{itemize} |
389 |
389 |
390 Existential quantifiers and unique existential quantifiers are defined |
390 Existential quantifiers and unique existential quantifiers are defined |
391 similarily to the universal one. |
391 similarily to the universal one. |
|
392 |
|
393 The function that gives the statment of the injected theorem |
|
394 takes the statement of the regularized theorems and the statement |
|
395 of the lifted theorem both as terms. |
|
396 |
|
397 \begin{itemize} |
|
398 \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<sigma>) = \<lambda>x. (INJ (t, s)"} |
|
399 \item @{text "INJ ((\<lambda>x. t) : \<sigma>, (\<lambda>x. s) : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (\<lambda>x. (INJ (t, s))))"} |
|
400 \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))))"} |
|
401 \item @{text "INJ (\<forall> t, \<forall> s) = \<forall> (INJ (t, s)"} |
|
402 \item @{text "INJ (\<forall> t \<in> R, \<forall> s) = \<forall> (INJ (t, s) \<in> R"} |
|
403 \item @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) = INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"} |
|
404 \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<sigma>) = v\<^isub>1"} |
|
405 \item @{text "INJ (v\<^isub>1 : \<sigma>, v\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (v\<^isub>1))"} |
|
406 \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<sigma>) = c\<^isub>1"} |
|
407 \item @{text "INJ (c\<^isub>1 : \<sigma>, c\<^isub>2 : \<tau>) = REP(\<sigma>,\<tau>) (ABS (\<sigma>,\<tau>) (c\<^isub>1))"} |
|
408 \end{itemize} |
|
409 |
|
410 For existential quantifiers and unique existential quantifiers it is |
|
411 defined similarily to the universal one. |
392 |
412 |
393 *} |
413 *} |
394 |
414 |
395 subsection {* Proof of Regularization *} |
415 subsection {* Proof of Regularization *} |
396 |
416 |