# HG changeset patch # User wenzelm # Date 1408212885 -7200 # Node ID ee1ba48488960bd7ee046df5effc6fa38000cc18 # Parent 1bfed12a7646854a79237d6c11c78580876c7a98 updated to named_theorems; modernized setup; diff -r 1bfed12a7646 -r ee1ba4848896 src/HOL/Quotient.thy --- 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)]] diff -r 1bfed12a7646 -r ee1ba4848896 src/HOL/Tools/Quotient/quotient_def.ML --- 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 diff -r 1bfed12a7646 -r ee1ba4848896 src/HOL/Tools/Quotient/quotient_info.ML --- 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 *) diff -r 1bfed12a7646 -r ee1ba4848896 src/HOL/Tools/Quotient/quotient_tacs.ML --- 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 diff -r 1bfed12a7646 -r ee1ba4848896 src/HOL/Tools/Quotient/quotient_type.ML --- 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