# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260231943 -3600
# Node ID 51a4208162ed0b26d2b3cfc40353777b00183645
# Parent 018aabbffd0839d9e1b9cba62f3b2024fa726a7d
added a thm list for ids
diff -r 018aabbffd08 -r 51a4208162ed Quot/QuotMain.thy
--- a/Quot/QuotMain.thy Tue Dec 08 01:00:21 2009 +0100
+++ b/Quot/QuotMain.thy Tue Dec 08 01:25:43 2009 +0100
@@ -147,8 +147,6 @@
(* Throws now an exception: *)
(* declare [[map "option" = (bla, blu)]] *)
-
-(* identity quotient is not here as it has to be applied first *)
lemmas [quotient_thm] =
fun_quotient prod_quotient
@@ -160,19 +158,17 @@
lemmas [quotient_equiv] =
identity_equivp prod_equivp
-
(* definition of the quotient types *)
(* FIXME: should be called quotient_typ.ML *)
use "quotient.ML"
-
(* lifting of constants *)
use "quotient_def.ML"
section {* Simset setup *}
-(* since HOL_basic_ss is too "big", we need to set up *)
-(* our own minimal simpset *)
+(* Since HOL_basic_ss is too "big" for us, *)
+(* we set up our own minimal simpset. *)
ML {*
fun mk_minimal_ss ctxt =
Simplifier.context ctxt empty_ss
@@ -181,13 +177,10 @@
*}
ML {*
-(* TODO/FIXME not needed anymore? *)
-fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
-
fun OF1 thm1 thm2 = thm2 RS thm1
*}
-section {* atomize *}
+section {* Atomize Infrastructure *}
lemma atomize_eqv[atomize]:
shows "(Trueprop A \<equiv> Trueprop B) \<equiv> (A \<equiv> B)"
@@ -219,24 +212,20 @@
end
*}
-section {* infrastructure about id *}
+section {* Infrastructure about id *}
+
+print_attributes
(* TODO: think where should this be *)
lemma prod_fun_id: "prod_fun id id \<equiv> id"
by (rule eq_reflection) (simp add: prod_fun_def)
-(* FIXME: make it a list and add map_id to it *)
-lemmas id_simps =
+lemmas [id_simps] =
fun_map_id[THEN eq_reflection]
id_apply[THEN eq_reflection]
id_def[THEN eq_reflection,symmetric]
prod_fun_id
-ML {*
-fun simp_ids thm =
- MetaSimplifier.rewrite_rule @{thms id_simps} thm
-*}
-
section {* Debugging infrastructure for testing tactics *}
ML {*
@@ -1008,7 +997,7 @@
val _ = tracing ("te rule:\n" ^ (Syntax.string_of_term ctxt (prop_of te)));
val ti =
(let
- val ts = MetaSimplifier.rewrite_rule @{thms id_simps} te
+ val ts = MetaSimplifier.rewrite_rule (id_simps_get ctxt) te
val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
in
Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
@@ -1017,7 +1006,7 @@
val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm)
val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te
in
- MetaSimplifier.rewrite_rule @{thms id_simps} td
+ MetaSimplifier.rewrite_rule (id_simps_get ctxt) td
end);
val _ = if not (Term.is_Const a2 andalso fst (dest_Const a2) = @{const_name "id"}) then
(tracing "lambda_prs";
@@ -1045,8 +1034,8 @@
(* 2. folding of definitions: (rep ---> abs) oldConst == newconst *)
(* and simplification with *)
thm all_prs ex_prs
-(* 3. simplification with *)
-thm fun_map.simps id_simps Quotient_abs_rep Quotient_rel_rep
+(* 3. simplification with id_simps and *)
+thm fun_map.simps Quotient_abs_rep Quotient_rel_rep
(* 4. Test for refl *)
ML {*
@@ -1056,8 +1045,8 @@
val defs = map (Thm.varifyT o symmetric o #def) (qconsts_dest thy)
(* FIXME: shouldn't the definitions already be varified? *)
val thms1 = @{thms all_prs ex_prs} @ defs
- val thms2 = @{thms eq_reflection[OF fun_map.simps]}
- @ @{thms id_simps Quotient_abs_rep Quotient_rel_rep}
+ val thms2 = @{thms eq_reflection[OF fun_map.simps]} @ (id_simps_get lthy)
+ @ @{thms Quotient_abs_rep Quotient_rel_rep}
fun simps thms = (mk_minimal_ss lthy) addsimps thms addSolver quotient_solver
in
EVERY' [lambda_prs_tac lthy,
diff -r 018aabbffd08 -r 51a4208162ed Quot/quotient_info.ML
--- a/Quot/quotient_info.ML Tue Dec 08 01:00:21 2009 +0100
+++ b/Quot/quotient_info.ML Tue Dec 08 01:25:43 2009 +0100
@@ -26,6 +26,7 @@
val equiv_rules_get: Proof.context -> thm list
val equiv_rules_add: attribute
val rsp_rules_get: Proof.context -> thm list
+ val id_simps_get: Proof.context -> thm list
val quotient_rules_get: Proof.context -> thm list
val quotient_rules_add: attribute
end;
@@ -174,6 +175,9 @@
OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants"
OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
+(* FIXME/TODO: check the various lemmas conform *)
+(* with the required shape *)
+
(* equivalence relation theorems *)
structure EquivRules = Named_Thms
(val name = "quotient_equiv"
@@ -189,6 +193,13 @@
val rsp_rules_get = RspRules.get
+(* respectfulness theorems *)
+structure IdSimps = Named_Thms
+ (val name = "id_simps"
+ val description = "Identity simp rules for maps.")
+
+val id_simps_get = IdSimps.get
+
(* quotient theorems *)
structure QuotientRules = Named_Thms
(val name = "quotient_thm"
@@ -201,6 +212,7 @@
val _ = Context.>> (Context.map_theory
(EquivRules.setup #>
RspRules.setup #>
+ IdSimps.setup #>
QuotientRules.setup))
end; (* structure *)