--- a/src/HOL/Quotient.thy Sat Aug 16 19:20:11 2014 +0200
+++ b/src/HOL/Quotient.thy Sat Aug 16 20:14:45 2014 +0200
@@ -748,8 +748,12 @@
text {* Auxiliary data for the quotient package *}
+named_theorems quot_equiv "equivalence relation theorems"
+named_theorems quot_respect "respectfulness theorems"
+named_theorems quot_preserve "preservation theorems"
+named_theorems id_simps "identity simp rules for maps"
+named_theorems quot_thm "quotient theorems"
ML_file "Tools/Quotient/quotient_info.ML"
-setup Quotient_Info.setup
declare [[mapQ3 "fun" = (rel_fun, fun_quotient3)]]
--- a/src/HOL/Tools/Quotient/quotient_def.ML Sat Aug 16 19:20:11 2014 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Sat Aug 16 20:14:45 2014 +0200
@@ -84,8 +84,7 @@
Quotient_Info.update_quotconsts c qcinfo
| _ => I))
|> (snd oo Local_Theory.note)
- ((rsp_thm_name, [Attrib.internal (K Quotient_Info.rsp_rules_add)]),
- [rsp_thm])
+ ((rsp_thm_name, @{attributes [quot_respect]}), [rsp_thm])
in
(qconst_data, lthy'')
end
--- a/src/HOL/Tools/Quotient/quotient_info.ML Sat Aug 16 19:20:11 2014 +0200
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Sat Aug 16 20:14:45 2014 +0200
@@ -33,17 +33,6 @@
val dest_quotconsts_global: theory -> quotconsts list
val dest_quotconsts: Proof.context -> quotconsts list
val print_quotconsts: Proof.context -> unit
-
- val equiv_rules: Proof.context -> thm list
- val equiv_rules_add: attribute
- val rsp_rules: Proof.context -> thm list
- val rsp_rules_add: attribute
- val prs_rules: Proof.context -> thm list
- val prs_rules_add: attribute
- val id_simps: Proof.context -> thm list
- val quotient_rules: Proof.context -> thm list
- val quotient_rules_add: attribute
- val setup: theory -> theory
end;
structure Quotient_Info: QUOTIENT_INFO =
@@ -69,16 +58,17 @@
(* FIXME export proper internal update operation!? *)
-val quotmaps_attribute_setup =
- Attrib.setup @{binding mapQ3}
- ((Args.type_name {proper = true, strict = true} --| Scan.lift @{keyword "="}) --
- (Scan.lift @{keyword "("} |--
- Args.const {proper = true, strict = true} --| Scan.lift @{keyword ","} --
- Attrib.thm --| Scan.lift @{keyword ")"}) >>
- (fn (tyname, (relname, qthm)) =>
- let val minfo = {relmap = relname, quot_thm = qthm}
- in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))
- "declaration of map information"
+val _ =
+ Theory.setup
+ (Attrib.setup @{binding mapQ3}
+ ((Args.type_name {proper = true, strict = true} --| Scan.lift @{keyword "="}) --
+ (Scan.lift @{keyword "("} |--
+ Args.const {proper = true, strict = true} --| Scan.lift @{keyword ","} --
+ Attrib.thm --| Scan.lift @{keyword ")"}) >>
+ (fn (tyname, (relname, qthm)) =>
+ let val minfo = {relmap = relname, quot_thm = qthm}
+ in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))
+ "declaration of map information")
fun print_quotmaps ctxt =
let
@@ -235,66 +225,6 @@
|> Pretty.writeln
end
-(* equivalence relation theorems *)
-structure Equiv_Rules = Named_Thms
-(
- val name = @{binding quot_equiv}
- val description = "equivalence relation theorems"
-)
-
-val equiv_rules = Equiv_Rules.get
-val equiv_rules_add = Equiv_Rules.add
-
-(* respectfulness theorems *)
-structure Rsp_Rules = Named_Thms
-(
- val name = @{binding quot_respect}
- val description = "respectfulness theorems"
-)
-
-val rsp_rules = Rsp_Rules.get
-val rsp_rules_add = Rsp_Rules.add
-
-(* preservation theorems *)
-structure Prs_Rules = Named_Thms
-(
- val name = @{binding quot_preserve}
- val description = "preservation theorems"
-)
-
-val prs_rules = Prs_Rules.get
-val prs_rules_add = Prs_Rules.add
-
-(* id simplification theorems *)
-structure Id_Simps = Named_Thms
-(
- val name = @{binding id_simps}
- val description = "identity simp rules for maps"
-)
-
-val id_simps = Id_Simps.get
-
-(* quotient theorems *)
-structure Quotient_Rules = Named_Thms
-(
- val name = @{binding quot_thm}
- val description = "quotient theorems"
-)
-
-val quotient_rules = Quotient_Rules.get
-val quotient_rules_add = Quotient_Rules.add
-
-
-(* theory setup *)
-
-val setup =
- quotmaps_attribute_setup #>
- Equiv_Rules.setup #>
- Rsp_Rules.setup #>
- Prs_Rules.setup #>
- Id_Simps.setup #>
- Quotient_Rules.setup
-
(* outer syntax commands *)
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Sat Aug 16 19:20:11 2014 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sat Aug 16 20:14:45 2014 +0200
@@ -55,14 +55,14 @@
(** solvers for equivp and quotient assumptions **)
fun equiv_tac ctxt =
- REPEAT_ALL_NEW (resolve_tac (Quotient_Info.equiv_rules ctxt))
+ REPEAT_ALL_NEW (resolve_tac (rev (Named_Theorems.get ctxt @{named_theorems quot_equiv})))
val equiv_solver = mk_solver "Equivalence goal solver" equiv_tac
fun quotient_tac ctxt =
(REPEAT_ALL_NEW (FIRST'
[rtac @{thm identity_quotient3},
- resolve_tac (Quotient_Info.quotient_rules ctxt)]))
+ resolve_tac (rev (Named_Theorems.get ctxt @{named_theorems quot_thm}))]))
val quotient_solver = mk_solver "Quotient goal solver" quotient_tac
@@ -144,11 +144,12 @@
fun reflp_get ctxt =
map_filter (fn th => if prems_of th = [] then SOME (OF1 @{thm equivp_reflp} th) else NONE
- handle THM _ => NONE) (Quotient_Info.equiv_rules ctxt)
+ handle THM _ => NONE) (rev (Named_Theorems.get ctxt @{named_theorems quot_equiv}))
val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)}
-fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (Quotient_Info.equiv_rules ctxt)
+fun eq_imp_rel_get ctxt =
+ map (OF1 eq_imp_rel) (rev (Named_Theorems.get ctxt @{named_theorems quot_equiv}))
fun regularize_tac ctxt =
let
@@ -370,7 +371,8 @@
(* respectfulness of constants; in particular of a simple relation *)
| _ $ (Const _) $ (Const _) (* rel_fun, list_rel, etc but not equality *)
- => resolve_tac (Quotient_Info.rsp_rules ctxt) THEN_ALL_NEW quotient_tac ctxt
+ => resolve_tac (rev (Named_Theorems.get ctxt @{named_theorems quot_respect}))
+ THEN_ALL_NEW quotient_tac ctxt
(* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
(* observe map_fun *)
@@ -516,20 +518,20 @@
4. test for refl
*)
-fun clean_tac lthy =
+fun clean_tac ctxt =
let
- val thy = Proof_Context.theory_of lthy
+ val thy = Proof_Context.theory_of ctxt
val defs = map (Thm.symmetric o #def) (Quotient_Info.dest_quotconsts_global thy)
- val prs = Quotient_Info.prs_rules lthy
- val ids = Quotient_Info.id_simps lthy
+ val prs = rev (Named_Theorems.get ctxt @{named_theorems quot_preserve})
+ val ids = rev (Named_Theorems.get ctxt @{named_theorems id_simps})
val thms =
@{thms Quotient3_abs_rep Quotient3_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
- val simpset = (mk_minimal_simpset lthy) addsimps thms addSolver quotient_solver
+ val simpset = (mk_minimal_simpset ctxt) addsimps thms addSolver quotient_solver
in
EVERY' [
- map_fun_tac lthy,
- lambda_prs_tac lthy,
+ map_fun_tac ctxt,
+ lambda_prs_tac ctxt,
simp_tac simpset,
TRY o rtac refl]
end
--- a/src/HOL/Tools/Quotient/quotient_type.ML Sat Aug 16 19:20:11 2014 +0200
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Sat Aug 16 20:14:45 2014 +0200
@@ -206,11 +206,10 @@
|> init_quotient_infr gen_code quotient_thm equiv_thm opt_par_thm
|> (snd oo Local_Theory.note)
((equiv_thm_name,
- if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]),
+ if partial then [] else @{attributes [quot_equiv]}),
[equiv_thm])
|> (snd oo Local_Theory.note)
- ((quotient_thm_name, [Attrib.internal (K Quotient_Info.quotient_rules_add)]),
- [quotient_thm])
+ ((quotient_thm_name, @{attributes [quot_thm]}), [quotient_thm])
in
(quotients, lthy4)
end