--- a/Quot/QuotMain.thy Tue Dec 22 07:42:16 2009 +0100
+++ b/Quot/QuotMain.thy Tue Dec 22 20:51:37 2009 +0100
@@ -74,14 +74,13 @@
unfolding abs_def
by (simp only: equivp[simplified equivp_def] lem7)
-
lemma rep_abs_rsp:
shows "R f (rep (abs g)) = R f g"
and "R (rep (abs g)) f = R g f"
by (simp_all add: thm10 thm11)
lemma Quotient:
- "Quotient R abs rep"
+ shows "Quotient R abs rep"
apply(unfold Quotient_def)
apply(simp add: thm10)
apply(simp add: rep_refl)
@@ -91,56 +90,65 @@
end
-section {* type definition for the quotient type *}
-(* auxiliary data for the quotient package *)
+section {* ML setup *}
+
+(* Auxiliary data for the quotient package *)
use "quotient_info.ML"
declare [[map "fun" = (fun_map, fun_rel)]]
lemmas [quot_thm] = fun_quotient
lemmas [quot_respect] = quot_rel_rsp
-
-(* fun_map is not here since equivp is not true *)
lemmas [quot_equiv] = identity_equivp
-(* definition of the quotient types *)
+(* Lemmas about simplifying id's. *)
+lemmas [id_simps] =
+ fun_map_id[THEN eq_reflection]
+ id_apply[THEN eq_reflection]
+ id_def[THEN eq_reflection, symmetric]
+ id_o[THEN eq_reflection]
+ o_id[THEN eq_reflection]
+
+(* Definition of the quotient types *)
use "quotient_typ.ML"
-(* lifting of constants *)
+
+(* Definitions for quotient constants *)
use "quotient_def.ML"
-(* the translation functions for the lifting process *)
+
+(* The translation functions for the lifting process. *)
use "quotient_term.ML"
-(* tactics for proving the theorems *)
+
+(* Tactics for proving the lifted theorems *)
lemma eq_imp_rel:
- "equivp R ==> a = b \<longrightarrow> R a b"
+ "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
by (simp add: equivp_reflp)
-(* an auxiliar constant that records some information *)
-(* about the lifted theorem *)
+(* An auxiliar constant for recording some information *)
+(* about the lifted theorem in a tactic. *)
definition
- "QUOT_TRUE x \<equiv> True"
+ "Quot_True x \<equiv> True"
-lemma quot_true_dests:
- shows QT_all: "QUOT_TRUE (All P) \<Longrightarrow> QUOT_TRUE P"
- and QT_ex: "QUOT_TRUE (Ex P) \<Longrightarrow> QUOT_TRUE P"
- and QT_lam: "QUOT_TRUE (\<lambda>x. P x) \<Longrightarrow> (\<And>x. QUOT_TRUE (P x))"
- and QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)"
-by (simp_all add: QUOT_TRUE_def ext)
+lemma
+ shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
+ and QT_ex: "Quot_True (Ex P) \<Longrightarrow> Quot_True P"
+ and QT_lam: "Quot_True (\<lambda>x. P x) \<Longrightarrow> (\<And>x. Quot_True (P x))"
+ and QT_ext: "(\<And>x. Quot_True (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (Quot_True a \<Longrightarrow> f = g)"
+by (simp_all add: Quot_True_def ext)
-lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
-by (simp add: QUOT_TRUE_def)
-
-lemma regularize_to_injection:
- shows "(QUOT_TRUE l \<Longrightarrow> y) \<Longrightarrow> (l = r) \<longrightarrow> y"
-by(auto simp add: QUOT_TRUE_def)
+lemma QT_imp: "Quot_True a \<equiv> Quot_True b"
+by (simp add: Quot_True_def)
use "quotient_tacs.ML"
-(* atomize infrastructure *)
+
+(* Atomize infrastructure *)
+(* FIXME/TODO: is this really needed? *)
+(*
lemma atomize_eqv[atomize]:
shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
proof
@@ -160,15 +168,7 @@
qed
then show "A \<equiv> B" by (rule eq_reflection)
qed
-
-(* lemmas about simplifying id *)
-lemmas [id_simps] =
- fun_map_id[THEN eq_reflection]
- id_apply[THEN eq_reflection]
- id_def[THEN eq_reflection, symmetric]
- id_o[THEN eq_reflection]
- o_id[THEN eq_reflection]
-
+*)
section {* Methods / Interface *}
@@ -193,7 +193,7 @@
{* Proves automatically the regularization goals from the lifting procedure. *}
method_setup injection =
- {* Scan.succeed (mk_method2 Quotient_Tacs.all_inj_repabs_tac) *}
+ {* Scan.succeed (mk_method2 Quotient_Tacs.all_injection_tac) *}
{* Proves automatically the rep/abs injection goals from the lifting procedure. *}
method_setup cleaning =