# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1275741425 -7200
# Node ID 9d0673c319d1866d2ea9998aeeeae270fb35d0d4
# Parent  6aaec9dd0c6230aa7e9337e7e004c72cd686324a
qpaper / injection proof.

diff -r 6aaec9dd0c62 -r 9d0673c319d1 Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Sat Jun 05 10:03:42 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Sat Jun 05 14:37:05 2010 +0200
@@ -501,19 +501,30 @@
 subsection {* Injection *}
 
 text {*
+  The injection proof starts with an equality between the regularized theorem
+  and the injected version. The proof again follows by the structure of the
+  two term, and is defined for a goal being a relation between the two terms.
 
-  The 2 key lemmas are:
+  \begin{itemize}
+  \item For two constants, an appropriate constant respectfullness assumption is used.
+  \item For two variables, the regularization assumptions state that they are related.
+  \item For two abstractions, they are eta-expanded and beta-reduced.
+  \end{itemize}
 
-  @{thm [display] apply_rsp[no_vars]}
+  Otherwise the two terms are applications. There are two cases: If there is a REP/ABS
+  in the injected theorem we can use the theorem:
+
   @{thm [display] rep_abs_rsp[no_vars]}
 
+  and continue the proof.
 
+  Otherwise we introduce an appropriate relation between the subterms and continue with
+  two subgoals using the lemma:
+
+  @{thm [display] apply_rsp[no_vars]}
 
 *}
 
-
-
-
 subsection {* Cleaning *}
 
 text {* Preservation of quantifiers, abstractions, relations, quotient-constants