# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1264438388 -3600
# Node ID c46b6abad24b33b59326520b1cb875404d2506a0
# Parent  7be9b054f6721ad1013d7b6141ef5e0eb8f159c2
cleaned some theorems

diff -r 7be9b054f672 -r c46b6abad24b FIXME-TODO
--- a/FIXME-TODO	Sun Jan 24 23:41:27 2010 +0100
+++ b/FIXME-TODO	Mon Jan 25 17:53:08 2010 +0100
@@ -1,19 +1,9 @@
 Highest Priority
 ================
 
-- better lookup mechanism for quotient definition
-  (see fixme in quotient_term.ML)
-
 Higher Priority
 ===============
 
-- If the user defines twice the same quotient constant,
-  for example funion, then the line 
-
-    val Free (lhs_str, lhs_ty) = lhs
-
-  in quotient_def raises a bind exception.
-
 - If the constant definition gives the wrong definition
   term, one gets a cryptic message about absrep_fun
 
diff -r 7be9b054f672 -r c46b6abad24b Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Sun Jan 24 23:41:27 2010 +0100
+++ b/Quot/QuotMain.thy	Mon Jan 25 17:53:08 2010 +0100
@@ -1,4 +1,4 @@
-(*  Title:      ??/QuotMain.thy
+(*  Title:      QuotMain.thy
     Author:     Cezary Kaliszyk and Christian Urban
 *)
 
@@ -32,6 +32,11 @@
 where
   "rep a = Eps (Rep a)"
 
+text {*
+  The naming of the lemmas follows the quotient paper
+  by Peter Homeier.
+*}
+
 lemma lem9:
   shows "R (Eps (R x)) = R x"
 proof -
@@ -62,12 +67,12 @@
 by (simp add: equivp[simplified equivp_def])
 
 lemma lem7:
-  shows "(R x = R y) = (Abs (R x) = Abs (R y))"
-apply(rule iffI)
-apply(simp)
-apply(drule rep_inject[THEN iffD2])
-apply(simp add: abs_inverse)
-done
+  shows "(R x = R y) = (Abs (R x) = Abs (R y))" (is "?LHS = ?RHS")
+proof -
+  have "?RHS = (Rep (Abs (R x)) = Rep (Abs (R y)))" by (simp add: rep_inject)
+  also have "\<dots> = ?LHS" by (simp add: abs_inverse)
+  finally show "?LHS = ?RHS" by simp
+qed
 
 theorem thm11:
   shows "R r r' = (abs r = abs r')"
@@ -81,7 +86,7 @@
 
 lemma Quotient:
   shows "Quotient R abs rep"
-apply(unfold Quotient_def)
+unfolding Quotient_def
 apply(simp add: thm10)
 apply(simp add: rep_refl)
 apply(subst thm11[symmetric])
@@ -90,11 +95,9 @@
 
 end
 
-term Quot_Type.abs
-
 section {* ML setup *}
 
-(* Auxiliary data for the quotient package *)
+text {* Auxiliary data for the quotient package *}
 
 use "quotient_info.ML"
 
@@ -104,34 +107,32 @@
 lemmas [quot_respect] = quot_rel_rsp
 lemmas [quot_equiv] = identity_equivp
 
-(* Lemmas about simplifying id's. *)
+
+text {* Lemmas about simplifying id's. *}
 lemmas [id_simps] =
+  id_def[symmetric, THEN eq_reflection]
   fun_map_id[THEN eq_reflection]
   id_apply[THEN eq_reflection]
   id_o[THEN eq_reflection]
-  id_def[symmetric, THEN eq_reflection]
   o_id[THEN eq_reflection]
   eq_comp_r
 
-(* The translation functions for the lifting process. *)
+text {* Translation functions for the lifting process. *}
 use "quotient_term.ML" 
 
 
-(* Definition of the quotient types *)
+text {* Definitions of the quotient types. *}
 use "quotient_typ.ML"
 
 
-(* Definitions for quotient constants *)
+text {* Definitions for quotient constants. *}
 use "quotient_def.ML"
 
-(* Tactics for proving the lifted theorems *)
 
-lemma eq_imp_rel:  
-  "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" 
-by (simp add: equivp_reflp)
-
-(* An auxiliar constant for recording some information *) 
-(* about the lifted theorem in a tactic.               *)
+text {* 
+  An auxiliar constant for recording some information  
+  about the lifted theorem in a tactic.       
+*}
 definition
   "Quot_True x \<equiv> True"
 
@@ -146,6 +147,7 @@
 lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
 by (simp add: Quot_True_def)
 
+text {* Tactics for proving the lifted theorems *}
 use "quotient_tacs.ML"
 
 
diff -r 7be9b054f672 -r c46b6abad24b Quot/QuotScript.thy
--- a/Quot/QuotScript.thy	Sun Jan 24 23:41:27 2010 +0100
+++ b/Quot/QuotScript.thy	Mon Jan 25 17:53:08 2010 +0100
@@ -36,6 +36,10 @@
   shows "equivp R"
   using assms by (simp add: equivp_reflp_symp_transp)
 
+lemma eq_imp_rel:  
+  shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" 
+by (simp add: equivp_reflp)
+
 definition
   "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
 
@@ -380,10 +384,10 @@
 apply rule+
 apply (erule_tac x="xb" in ballE)
 prefer 2
-apply (metis in_respects)
+apply (metis)
 apply (erule_tac x="ya" in ballE)
 prefer 2
-apply (metis in_respects)
+apply (metis)
 apply (metis in_respects)
 apply (erule conjE)+
 apply (erule bexE)
@@ -394,10 +398,10 @@
 apply rule+
 apply (erule_tac x="xb" in ballE)
 prefer 2
-apply (metis in_respects)
+apply (metis)
 apply (erule_tac x="ya" in ballE)
 prefer 2
-apply (metis in_respects)
+apply (metis)
 apply (metis in_respects)
 done