--- 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
--- 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"
--- 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