updated to named_theorems;
authorwenzelm
Sat Aug 16 20:14:45 2014 +0200 (2014-08-16)
changeset 57960ee1ba4848896
parent 57959 1bfed12a7646
child 57961 10b2f60b70f0
updated to named_theorems;
modernized setup;
src/HOL/Quotient.thy
src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_info.ML
src/HOL/Tools/Quotient/quotient_tacs.ML
src/HOL/Tools/Quotient/quotient_type.ML
     1.1 --- a/src/HOL/Quotient.thy	Sat Aug 16 19:20:11 2014 +0200
     1.2 +++ b/src/HOL/Quotient.thy	Sat Aug 16 20:14:45 2014 +0200
     1.3 @@ -748,8 +748,12 @@
     1.4  
     1.5  text {* Auxiliary data for the quotient package *}
     1.6  
     1.7 +named_theorems quot_equiv "equivalence relation theorems"
     1.8 +named_theorems quot_respect "respectfulness theorems"
     1.9 +named_theorems quot_preserve "preservation theorems"
    1.10 +named_theorems id_simps "identity simp rules for maps"
    1.11 +named_theorems quot_thm "quotient theorems"
    1.12  ML_file "Tools/Quotient/quotient_info.ML"
    1.13 -setup Quotient_Info.setup
    1.14  
    1.15  declare [[mapQ3 "fun" = (rel_fun, fun_quotient3)]]
    1.16  
     2.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Sat Aug 16 19:20:11 2014 +0200
     2.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Sat Aug 16 20:14:45 2014 +0200
     2.3 @@ -84,8 +84,7 @@
     2.4                Quotient_Info.update_quotconsts c qcinfo
     2.5            | _ => I))
     2.6        |> (snd oo Local_Theory.note) 
     2.7 -        ((rsp_thm_name, [Attrib.internal (K Quotient_Info.rsp_rules_add)]),
     2.8 -        [rsp_thm])
     2.9 +        ((rsp_thm_name, @{attributes [quot_respect]}), [rsp_thm])
    2.10    in
    2.11      (qconst_data, lthy'')
    2.12    end
     3.1 --- a/src/HOL/Tools/Quotient/quotient_info.ML	Sat Aug 16 19:20:11 2014 +0200
     3.2 +++ b/src/HOL/Tools/Quotient/quotient_info.ML	Sat Aug 16 20:14:45 2014 +0200
     3.3 @@ -33,17 +33,6 @@
     3.4    val dest_quotconsts_global: theory -> quotconsts list
     3.5    val dest_quotconsts: Proof.context -> quotconsts list
     3.6    val print_quotconsts: Proof.context -> unit
     3.7 -
     3.8 -  val equiv_rules: Proof.context -> thm list
     3.9 -  val equiv_rules_add: attribute
    3.10 -  val rsp_rules: Proof.context -> thm list
    3.11 -  val rsp_rules_add: attribute
    3.12 -  val prs_rules: Proof.context -> thm list
    3.13 -  val prs_rules_add: attribute
    3.14 -  val id_simps: Proof.context -> thm list
    3.15 -  val quotient_rules: Proof.context -> thm list
    3.16 -  val quotient_rules_add: attribute
    3.17 -  val setup: theory -> theory
    3.18  end;
    3.19  
    3.20  structure Quotient_Info: QUOTIENT_INFO =
    3.21 @@ -69,16 +58,17 @@
    3.22  
    3.23  (* FIXME export proper internal update operation!? *)
    3.24  
    3.25 -val quotmaps_attribute_setup =
    3.26 -  Attrib.setup @{binding mapQ3}
    3.27 -    ((Args.type_name {proper = true, strict = true} --| Scan.lift @{keyword "="}) --
    3.28 -      (Scan.lift @{keyword "("} |--
    3.29 -        Args.const {proper = true, strict = true} --| Scan.lift @{keyword ","} --
    3.30 -        Attrib.thm --| Scan.lift @{keyword ")"}) >>
    3.31 -      (fn (tyname, (relname, qthm)) =>
    3.32 -        let val minfo = {relmap = relname, quot_thm = qthm}
    3.33 -        in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))
    3.34 -    "declaration of map information"
    3.35 +val _ =
    3.36 +  Theory.setup
    3.37 +   (Attrib.setup @{binding mapQ3}
    3.38 +      ((Args.type_name {proper = true, strict = true} --| Scan.lift @{keyword "="}) --
    3.39 +        (Scan.lift @{keyword "("} |--
    3.40 +          Args.const {proper = true, strict = true} --| Scan.lift @{keyword ","} --
    3.41 +          Attrib.thm --| Scan.lift @{keyword ")"}) >>
    3.42 +        (fn (tyname, (relname, qthm)) =>
    3.43 +          let val minfo = {relmap = relname, quot_thm = qthm}
    3.44 +          in Thm.declaration_attribute (fn _ => Quotmaps.map (Symtab.update (tyname, minfo))) end))
    3.45 +      "declaration of map information")
    3.46  
    3.47  fun print_quotmaps ctxt =
    3.48    let
    3.49 @@ -235,66 +225,6 @@
    3.50      |> Pretty.writeln
    3.51    end
    3.52  
    3.53 -(* equivalence relation theorems *)
    3.54 -structure Equiv_Rules = Named_Thms
    3.55 -(
    3.56 -  val name = @{binding quot_equiv}
    3.57 -  val description = "equivalence relation theorems"
    3.58 -)
    3.59 -
    3.60 -val equiv_rules = Equiv_Rules.get
    3.61 -val equiv_rules_add = Equiv_Rules.add
    3.62 -
    3.63 -(* respectfulness theorems *)
    3.64 -structure Rsp_Rules = Named_Thms
    3.65 -(
    3.66 -  val name = @{binding quot_respect}
    3.67 -  val description = "respectfulness theorems"
    3.68 -)
    3.69 -
    3.70 -val rsp_rules = Rsp_Rules.get
    3.71 -val rsp_rules_add = Rsp_Rules.add
    3.72 -
    3.73 -(* preservation theorems *)
    3.74 -structure Prs_Rules = Named_Thms
    3.75 -(
    3.76 -  val name = @{binding quot_preserve}
    3.77 -  val description = "preservation theorems"
    3.78 -)
    3.79 -
    3.80 -val prs_rules = Prs_Rules.get
    3.81 -val prs_rules_add = Prs_Rules.add
    3.82 -
    3.83 -(* id simplification theorems *)
    3.84 -structure Id_Simps = Named_Thms
    3.85 -(
    3.86 -  val name = @{binding id_simps}
    3.87 -  val description = "identity simp rules for maps"
    3.88 -)
    3.89 -
    3.90 -val id_simps = Id_Simps.get
    3.91 -
    3.92 -(* quotient theorems *)
    3.93 -structure Quotient_Rules = Named_Thms
    3.94 -(
    3.95 -  val name = @{binding quot_thm}
    3.96 -  val description = "quotient theorems"
    3.97 -)
    3.98 -
    3.99 -val quotient_rules = Quotient_Rules.get
   3.100 -val quotient_rules_add = Quotient_Rules.add
   3.101 -
   3.102 -
   3.103 -(* theory setup *)
   3.104 -
   3.105 -val setup =
   3.106 -  quotmaps_attribute_setup #>
   3.107 -  Equiv_Rules.setup #>
   3.108 -  Rsp_Rules.setup #>
   3.109 -  Prs_Rules.setup #>
   3.110 -  Id_Simps.setup #>
   3.111 -  Quotient_Rules.setup
   3.112 -
   3.113  
   3.114  (* outer syntax commands *)
   3.115  
     4.1 --- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Aug 16 19:20:11 2014 +0200
     4.2 +++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Sat Aug 16 20:14:45 2014 +0200
     4.3 @@ -55,14 +55,14 @@
     4.4  (** solvers for equivp and quotient assumptions **)
     4.5  
     4.6  fun equiv_tac ctxt =
     4.7 -  REPEAT_ALL_NEW (resolve_tac (Quotient_Info.equiv_rules ctxt))
     4.8 +  REPEAT_ALL_NEW (resolve_tac (rev (Named_Theorems.get ctxt @{named_theorems quot_equiv})))
     4.9  
    4.10  val equiv_solver = mk_solver "Equivalence goal solver" equiv_tac
    4.11  
    4.12  fun quotient_tac ctxt =
    4.13    (REPEAT_ALL_NEW (FIRST'
    4.14      [rtac @{thm identity_quotient3},
    4.15 -     resolve_tac (Quotient_Info.quotient_rules ctxt)]))
    4.16 +     resolve_tac (rev (Named_Theorems.get ctxt @{named_theorems quot_thm}))]))
    4.17  
    4.18  val quotient_solver = mk_solver "Quotient goal solver" quotient_tac
    4.19  
    4.20 @@ -144,11 +144,12 @@
    4.21  
    4.22  fun reflp_get ctxt =
    4.23    map_filter (fn th => if prems_of th = [] then SOME (OF1 @{thm equivp_reflp} th) else NONE
    4.24 -    handle THM _ => NONE) (Quotient_Info.equiv_rules ctxt)
    4.25 +    handle THM _ => NONE) (rev (Named_Theorems.get ctxt @{named_theorems quot_equiv}))
    4.26  
    4.27  val eq_imp_rel = @{lemma "equivp R ==> a = b --> R a b" by (simp add: equivp_reflp)}
    4.28  
    4.29 -fun eq_imp_rel_get ctxt = map (OF1 eq_imp_rel) (Quotient_Info.equiv_rules ctxt)
    4.30 +fun eq_imp_rel_get ctxt =
    4.31 +  map (OF1 eq_imp_rel) (rev (Named_Theorems.get ctxt @{named_theorems quot_equiv}))
    4.32  
    4.33  fun regularize_tac ctxt =
    4.34    let
    4.35 @@ -370,7 +371,8 @@
    4.36  
    4.37       (* respectfulness of constants; in particular of a simple relation *)
    4.38    | _ $ (Const _) $ (Const _)  (* rel_fun, list_rel, etc but not equality *)
    4.39 -      => resolve_tac (Quotient_Info.rsp_rules ctxt) THEN_ALL_NEW quotient_tac ctxt
    4.40 +      => resolve_tac (rev (Named_Theorems.get ctxt @{named_theorems quot_respect}))
    4.41 +          THEN_ALL_NEW quotient_tac ctxt
    4.42  
    4.43        (* R (...) (Rep (Abs ...)) ----> R (...) (...) *)
    4.44        (* observe map_fun *)
    4.45 @@ -516,20 +518,20 @@
    4.46  
    4.47    4. test for refl
    4.48  *)
    4.49 -fun clean_tac lthy =
    4.50 +fun clean_tac ctxt =
    4.51    let
    4.52 -    val thy =  Proof_Context.theory_of lthy
    4.53 +    val thy =  Proof_Context.theory_of ctxt
    4.54      val defs = map (Thm.symmetric o #def) (Quotient_Info.dest_quotconsts_global thy)
    4.55 -    val prs = Quotient_Info.prs_rules lthy
    4.56 -    val ids = Quotient_Info.id_simps lthy
    4.57 +    val prs = rev (Named_Theorems.get ctxt @{named_theorems quot_preserve})
    4.58 +    val ids = rev (Named_Theorems.get ctxt @{named_theorems id_simps})
    4.59      val thms =
    4.60        @{thms Quotient3_abs_rep Quotient3_rel_rep babs_prs all_prs ex_prs ex1_prs} @ ids @ prs @ defs
    4.61  
    4.62 -    val simpset = (mk_minimal_simpset lthy) addsimps thms addSolver quotient_solver
    4.63 +    val simpset = (mk_minimal_simpset ctxt) addsimps thms addSolver quotient_solver
    4.64    in
    4.65      EVERY' [
    4.66 -      map_fun_tac lthy,
    4.67 -      lambda_prs_tac lthy,
    4.68 +      map_fun_tac ctxt,
    4.69 +      lambda_prs_tac ctxt,
    4.70        simp_tac simpset,
    4.71        TRY o rtac refl]
    4.72    end
     5.1 --- a/src/HOL/Tools/Quotient/quotient_type.ML	Sat Aug 16 19:20:11 2014 +0200
     5.2 +++ b/src/HOL/Tools/Quotient/quotient_type.ML	Sat Aug 16 20:14:45 2014 +0200
     5.3 @@ -206,11 +206,10 @@
     5.4        |> init_quotient_infr gen_code quotient_thm equiv_thm opt_par_thm
     5.5        |> (snd oo Local_Theory.note)
     5.6          ((equiv_thm_name,
     5.7 -          if partial then [] else [Attrib.internal (K Quotient_Info.equiv_rules_add)]),
     5.8 +          if partial then [] else @{attributes [quot_equiv]}),
     5.9            [equiv_thm])
    5.10        |> (snd oo Local_Theory.note)
    5.11 -        ((quotient_thm_name, [Attrib.internal (K Quotient_Info.quotient_rules_add)]),
    5.12 -          [quotient_thm])
    5.13 +        ((quotient_thm_name, @{attributes [quot_thm]}), [quotient_thm])
    5.14    in
    5.15      (quotients, lthy4)
    5.16    end