239 (*

   240 

   241 Regularizing a theorem means:

   242  - Quantifiers over a type that needs lifting are replaced by

   243    bounded quantifiers, for example:

   244       \<forall>x. P     \<Longrightarrow>     \<forall>x\<in>(Respects R). P

   245  - Abstractions over a type that needs lifting are replaced

   246    by bounded abstactions:

   247       \<lambda>x. P     \<Longrightarrow>     Ball (Respects R) (\<lambda>x. P)

   248 

   249  - Equalities over the type being lifted are replaced by

   250    appropriate relations:

   251       A = B     \<Longrightarrow>     A \<approx> B

   252    Example with more complicated types of A, B:

   253       A = B     \<Longrightarrow>     (op = \<Longrightarrow> op \<approx>) A B

   254 

   255 Regularizing is done in 3 phases:

   256  - First a regularized term is created

   257  - Next we prove that the original theorem implies the new one

   258  - Finally using MP we get the new theorem.

   259 

   260 To prove that the old theorem implies the new one, we first

   261 atomize it and then try:

   262  - Reflexivity of the relation

   263  - Assumption

   264  - Elimnating quantifiers on both sides of toplevel implication

   265  - Simplifying implications on both sides of toplevel implication

   266  - Ball (Respects ?E) ?P = All ?P

   267  - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q

   268 

   269 *)