# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1257339826 -3600
# Node ID e9212a4a44be0f4e2808667df05769cc8e14a7b8
# Parent  46e6d06efe3fd2d3369893c2f27399339a97fb85
Description of regularize

diff -r 46e6d06efe3f -r e9212a4a44be QuotMain.thy
--- a/QuotMain.thy	Wed Nov 04 13:33:13 2009 +0100
+++ b/QuotMain.thy	Wed Nov 04 14:03:46 2009 +0100
@@ -236,6 +236,37 @@
 ML {* atomize_thm @{thm list.induct} *}
 
 section {* REGULARIZE *}
+(*
+
+Regularizing a theorem means:
+ - Quantifiers over a type that needs lifting are replaced by
+   bounded quantifiers, for example:
+      \<forall>x. P     \<Longrightarrow>     \<forall>x\<in>(Respects R). P
+ - Abstractions over a type that needs lifting are replaced
+   by bounded abstactions:
+      \<lambda>x. P     \<Longrightarrow>     Ball (Respects R) (\<lambda>x. P)
+
+ - Equalities over the type being lifted are replaced by
+   appropriate relations:
+      A = B     \<Longrightarrow>     A \<approx> B
+   Example with more complicated types of A, B:
+      A = B     \<Longrightarrow>     (op = \<Longrightarrow> op \<approx>) A B
+
+Regularizing is done in 3 phases:
+ - First a regularized term is created
+ - Next we prove that the original theorem implies the new one
+ - Finally using MP we get the new theorem.
+
+To prove that the old theorem implies the new one, we first
+atomize it and then try:
+ - Reflexivity of the relation
+ - Assumption
+ - Elimnating quantifiers on both sides of toplevel implication
+ - Simplifying implications on both sides of toplevel implication
+ - Ball (Respects ?E) ?P = All ?P
+ - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q
+
+*)
 
 text {* tyRel takes a type and builds a relation that a quantifier over this
   type needs to respect. *}