prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
authorwenzelm
Sat Aug 16 11:35:33 2014 +0200 (2014-08-16)
changeset 57945cacb00a569e0
parent 57944 fff8d328da56
child 57946 6a26aa5fa65e
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
src/CCL/Wfd.thy
src/Cube/Cube.thy
src/HOL/HOLCF/Cfun.thy
src/HOL/HOLCF/Cont.thy
src/HOL/HOLCF/Domain.thy
src/HOL/HOLCF/Domain_Aux.thy
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
src/HOL/HOLCF/Tools/fixrec.ML
src/ZF/UNITY/Constrains.thy
src/ZF/UNITY/SubstAx.thy
     1.1 --- a/src/CCL/Wfd.thy	Fri Aug 15 18:02:34 2014 +0200
     1.2 +++ b/src/CCL/Wfd.thy	Sat Aug 16 11:35:33 2014 +0200
     1.3 @@ -483,15 +483,14 @@
     1.4  
     1.5  subsection {* Evaluation *}
     1.6  
     1.7 +named_theorems eval "evaluation rules"
     1.8 +
     1.9  ML {*
    1.10 -structure Eval_Rules =
    1.11 -  Named_Thms(val name = @{binding eval} val description = "evaluation rules");
    1.12 -
    1.13  fun eval_tac ths =
    1.14 -  Subgoal.FOCUS_PREMS (fn {context, prems, ...} =>
    1.15 -    DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ Eval_Rules.get context) 1));
    1.16 +  Subgoal.FOCUS_PREMS (fn {context = ctxt, prems, ...} =>
    1.17 +    let val eval_rules = Named_Theorems.get ctxt @{named_theorems eval}
    1.18 +    in DEPTH_SOLVE_1 (resolve_tac (ths @ prems @ rev eval_rules) 1) end)
    1.19  *}
    1.20 -setup Eval_Rules.setup
    1.21  
    1.22  method_setup eval = {*
    1.23    Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (CHANGED o eval_tac ths ctxt))
     2.1 --- a/src/Cube/Cube.thy	Fri Aug 15 18:02:34 2014 +0200
     2.2 +++ b/src/Cube/Cube.thy	Sat Aug 16 11:35:33 2014 +0200
     2.3 @@ -10,14 +10,7 @@
     2.4  
     2.5  setup Pure_Thy.old_appl_syntax_setup
     2.6  
     2.7 -ML {*
     2.8 -  structure Rules = Named_Thms
     2.9 -  (
    2.10 -    val name = @{binding rules}
    2.11 -    val description = "Cube inference rules"
    2.12 -  )
    2.13 -*}
    2.14 -setup Rules.setup
    2.15 +named_theorems rules "Cube inference rules"
    2.16  
    2.17  typedecl "term"
    2.18  typedecl "context"
     3.1 --- a/src/HOL/HOLCF/Cfun.thy	Fri Aug 15 18:02:34 2014 +0200
     3.2 +++ b/src/HOL/HOLCF/Cfun.thy	Sat Aug 16 11:35:33 2014 +0200
     3.3 @@ -147,7 +147,7 @@
     3.4        val [T, U] = Thm.dest_ctyp (ctyp_of_term f);
     3.5        val tr = instantiate' [SOME T, SOME U] [SOME f]
     3.6            (mk_meta_eq @{thm Abs_cfun_inverse2});
     3.7 -      val rules = Cont2ContData.get ctxt;
     3.8 +      val rules = Named_Theorems.get ctxt @{named_theorems cont2cont};
     3.9        val tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules));
    3.10      in SOME (perhaps (SINGLE (tac 1)) tr) end
    3.11  *}
     4.1 --- a/src/HOL/HOLCF/Cont.thy	Fri Aug 15 18:02:34 2014 +0200
     4.2 +++ b/src/HOL/HOLCF/Cont.thy	Sat Aug 16 11:35:33 2014 +0200
     4.3 @@ -120,15 +120,8 @@
     4.4  
     4.5  subsection {* Collection of continuity rules *}
     4.6  
     4.7 -ML {*
     4.8 -structure Cont2ContData = Named_Thms
     4.9 -(
    4.10 -  val name = @{binding cont2cont}
    4.11 -  val description = "continuity intro rule"
    4.12 -)
    4.13 -*}
    4.14 +named_theorems cont2cont "continuity intro rule"
    4.15  
    4.16 -setup Cont2ContData.setup
    4.17  
    4.18  subsection {* Continuity of basic functions *}
    4.19  
     5.1 --- a/src/HOL/HOLCF/Domain.thy	Fri Aug 15 18:02:34 2014 +0200
     5.2 +++ b/src/HOL/HOLCF/Domain.thy	Sat Aug 16 11:35:33 2014 +0200
     5.3 @@ -316,12 +316,13 @@
     5.4  
     5.5  subsection {* Setting up the domain package *}
     5.6  
     5.7 +named_theorems domain_defl_simps "theorems like DEFL('a t) = t_defl$DEFL('a)"
     5.8 +named_theorems domain_isodefl "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
     5.9 +
    5.10  ML_file "Tools/Domain/domain_isomorphism.ML"
    5.11  ML_file "Tools/Domain/domain_axioms.ML"
    5.12  ML_file "Tools/Domain/domain.ML"
    5.13  
    5.14 -setup Domain_Isomorphism.setup
    5.15 -
    5.16  lemmas [domain_defl_simps] =
    5.17    DEFL_cfun DEFL_sfun DEFL_ssum DEFL_sprod DEFL_prod DEFL_u
    5.18    liftdefl_eq LIFTDEFL_prod u_liftdefl_liftdefl_of
     6.1 --- a/src/HOL/HOLCF/Domain_Aux.thy	Fri Aug 15 18:02:34 2014 +0200
     6.2 +++ b/src/HOL/HOLCF/Domain_Aux.thy	Sat Aug 16 11:35:33 2014 +0200
     6.3 @@ -344,6 +344,9 @@
     6.4  
     6.5  subsection {* ML setup *}
     6.6  
     6.7 +named_theorems domain_deflation "theorems like deflation a ==> deflation (foo_map$a)"
     6.8 +named_theorems domain_map_ID "theorems like foo_map$ID = ID"
     6.9 +
    6.10  ML_file "Tools/Domain/domain_take_proofs.ML"
    6.11  ML_file "Tools/cont_consts.ML"
    6.12  ML_file "Tools/cont_proc.ML"
     7.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Fri Aug 15 18:02:34 2014 +0200
     7.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Aug 16 11:35:33 2014 +0200
     7.3 @@ -28,8 +28,6 @@
     7.4    val domain_isomorphism_cmd :
     7.5      (string list * binding * mixfix * string * (binding * binding) option) list
     7.6        -> theory -> theory
     7.7 -
     7.8 -  val setup : theory -> theory
     7.9  end
    7.10  
    7.11  structure Domain_Isomorphism : DOMAIN_ISOMORPHISM =
    7.12 @@ -41,24 +39,6 @@
    7.13  
    7.14  fun is_cpo thy T = Sign.of_sort thy (T, @{sort cpo})
    7.15  
    7.16 -(******************************************************************************)
    7.17 -(******************************** theory data *********************************)
    7.18 -(******************************************************************************)
    7.19 -
    7.20 -structure RepData = Named_Thms
    7.21 -(
    7.22 -  val name = @{binding domain_defl_simps}
    7.23 -  val description = "theorems like DEFL('a t) = t_defl$DEFL('a)"
    7.24 -)
    7.25 -
    7.26 -structure IsodeflData = Named_Thms
    7.27 -(
    7.28 -  val name = @{binding domain_isodefl}
    7.29 -  val description = "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
    7.30 -)
    7.31 -
    7.32 -val setup = RepData.setup #> IsodeflData.setup
    7.33 -
    7.34  
    7.35  (******************************************************************************)
    7.36  (************************** building types and terms **************************)
    7.37 @@ -170,7 +150,7 @@
    7.38      val cont_thm =
    7.39        let
    7.40          val prop = mk_trp (mk_cont functional)
    7.41 -        val rules = Cont2ContData.get (Proof_Context.init_global thy)
    7.42 +        val rules = Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems cont2cont}
    7.43          val tac = REPEAT_ALL_NEW (match_tac rules) 1
    7.44        in
    7.45          Goal.prove_global thy [] [] prop (K tac)
    7.46 @@ -207,7 +187,8 @@
    7.47      (tab2 : (typ * term) list)
    7.48      (T : typ) : term =
    7.49    let
    7.50 -    val defl_simps = RepData.get (Proof_Context.init_global thy)
    7.51 +    val defl_simps =
    7.52 +      Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_defl_simps}
    7.53      val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) defl_simps
    7.54      val rules' = map (apfst mk_DEFL) tab1 @ map (apfst mk_LIFTDEFL) tab2
    7.55      fun proc1 t =
    7.56 @@ -522,7 +503,8 @@
    7.57          val ((_, _, _, {DEFL, ...}), thy) =
    7.58            Domaindef.add_domaindef spec defl NONE thy
    7.59          (* declare domain_defl_simps rules *)
    7.60 -        val thy = Context.theory_map (RepData.add_thm DEFL) thy
    7.61 +        val thy =
    7.62 +          Context.theory_map (Named_Theorems.add_thm @{named_theorems domain_defl_simps} DEFL) thy
    7.63        in
    7.64          (DEFL, thy)
    7.65        end
    7.66 @@ -532,7 +514,8 @@
    7.67      fun mk_DEFL_eq_thm (lhsT, rhsT) =
    7.68        let
    7.69          val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT)
    7.70 -        val DEFL_simps = RepData.get (Proof_Context.init_global thy)
    7.71 +        val DEFL_simps =
    7.72 +          Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_defl_simps}
    7.73          fun tac ctxt =
    7.74            rewrite_goals_tac ctxt (map mk_meta_eq DEFL_simps)
    7.75            THEN TRY (resolve_tac defl_unfold_thms 1)
    7.76 @@ -637,7 +620,7 @@
    7.77          val isodefl_rules =
    7.78            @{thms conjI isodefl_ID_DEFL isodefl_LIFTDEFL}
    7.79            @ isodefl_abs_rep_thms
    7.80 -          @ IsodeflData.get (Proof_Context.init_global thy)
    7.81 +          @ Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_isodefl}
    7.82        in
    7.83          Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>
    7.84           EVERY
    7.85 @@ -661,7 +644,9 @@
    7.86      val (isodefl_thms, thy) = thy |>
    7.87        (Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
    7.88          (conjuncts isodefl_binds isodefl_thm)
    7.89 -    val thy = fold (Context.theory_map o IsodeflData.add_thm) isodefl_thms thy
    7.90 +    val thy =
    7.91 +      fold (Context.theory_map o Named_Theorems.add_thm @{named_theorems domain_isodefl})
    7.92 +        isodefl_thms thy
    7.93  
    7.94      (* prove map_ID theorems *)
    7.95      fun prove_map_ID_thm
     8.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Fri Aug 15 18:02:34 2014 +0200
     8.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sat Aug 16 11:35:33 2014 +0200
     8.3 @@ -123,31 +123,20 @@
     8.4    fun merge data = Symtab.merge (K true) data
     8.5  )
     8.6  
     8.7 -structure DeflMapData = Named_Thms
     8.8 -(
     8.9 -  val name = @{binding domain_deflation}
    8.10 -  val description = "theorems like deflation a ==> deflation (foo_map$a)"
    8.11 -)
    8.12 -
    8.13 -structure Map_Id_Data = Named_Thms
    8.14 -(
    8.15 -  val name = @{binding domain_map_ID}
    8.16 -  val description = "theorems like foo_map$ID = ID"
    8.17 -)
    8.18 -
    8.19  fun add_rec_type (tname, bs) =
    8.20      Rec_Data.map (Symtab.insert (K true) (tname, bs))
    8.21  
    8.22  fun add_deflation_thm thm =
    8.23 -    Context.theory_map (DeflMapData.add_thm thm)
    8.24 +    Context.theory_map (Named_Theorems.add_thm @{named_theorems domain_deflation} thm)
    8.25  
    8.26  val get_rec_tab = Rec_Data.get
    8.27 -fun get_deflation_thms thy = DeflMapData.get (Proof_Context.init_global thy)
    8.28 +fun get_deflation_thms thy =
    8.29 +  Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_deflation}
    8.30  
    8.31 -val map_ID_add = Map_Id_Data.add
    8.32 -val get_map_ID_thms = Map_Id_Data.get o Proof_Context.init_global
    8.33 +val map_ID_add = Named_Theorems.add @{named_theorems domain_map_ID}
    8.34 +fun get_map_ID_thms thy =
    8.35 +  Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_map_ID}
    8.36  
    8.37 -val _ = Theory.setup (DeflMapData.setup #> Map_Id_Data.setup)
    8.38  
    8.39  (******************************************************************************)
    8.40  (************************** building types and terms **************************)
     9.1 --- a/src/HOL/HOLCF/Tools/fixrec.ML	Fri Aug 15 18:02:34 2014 +0200
     9.2 +++ b/src/HOL/HOLCF/Tools/fixrec.ML	Sat Aug 16 11:35:33 2014 +0200
     9.3 @@ -130,7 +130,7 @@
     9.4            "or simp rules are configured for all non-HOLCF constants.\n" ^
     9.5            "The error occurred for the goal statement:\n" ^
     9.6            Syntax.string_of_term lthy prop)
     9.7 -        val rules = Cont2ContData.get lthy
     9.8 +        val rules = Named_Theorems.get lthy @{named_theorems cont2cont}
     9.9          val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules))
    9.10          val slow_tac = SOLVED' (simp_tac lthy)
    9.11          val tac = fast_tac 1 ORELSE slow_tac 1 ORELSE err
    10.1 --- a/src/ZF/UNITY/Constrains.thy	Fri Aug 15 18:02:34 2014 +0200
    10.2 +++ b/src/ZF/UNITY/Constrains.thy	Sat Aug 16 11:35:33 2014 +0200
    10.3 @@ -453,6 +453,9 @@
    10.4    used by Always_Int_I) *)
    10.5  lemmas Always_thin = thin_rl [of "F \<in> Always(A)"]
    10.6  
    10.7 +(*To allow expansion of the program's definition when appropriate*)
    10.8 +named_theorems program "program definitions"
    10.9 +
   10.10  ML
   10.11  {*
   10.12  (*Combines two invariance ASSUMPTIONS into one.  USEFUL??*)
   10.13 @@ -461,13 +464,6 @@
   10.14  (*Combines a list of invariance THEOREMS into one.*)
   10.15  val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I});
   10.16  
   10.17 -(*To allow expansion of the program's definition when appropriate*)
   10.18 -structure Program_Defs = Named_Thms
   10.19 -(
   10.20 -  val name = @{binding program}
   10.21 -  val description = "program definitions"
   10.22 -);
   10.23 -
   10.24  (*proves "co" properties when the program is specified*)
   10.25  
   10.26  fun constrains_tac ctxt =
   10.27 @@ -481,7 +477,7 @@
   10.28                (* Three subgoals *)
   10.29                rewrite_goal_tac ctxt [@{thm st_set_def}] 3,
   10.30                REPEAT (force_tac ctxt 2),
   10.31 -              full_simp_tac (ctxt addsimps (Program_Defs.get ctxt)) 1,
   10.32 +              full_simp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems program})) 1,
   10.33                ALLGOALS (clarify_tac ctxt),
   10.34                REPEAT (FIRSTGOAL (etac @{thm disjE})),
   10.35                ALLGOALS (clarify_tac ctxt),
   10.36 @@ -495,8 +491,6 @@
   10.37      rtac @{thm AlwaysI} i THEN force_tac ctxt i THEN constrains_tac ctxt i;
   10.38  *}
   10.39  
   10.40 -setup Program_Defs.setup
   10.41 -
   10.42  method_setup safety = {*
   10.43    Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
   10.44    "for proving safety properties"
    11.1 --- a/src/ZF/UNITY/SubstAx.thy	Fri Aug 15 18:02:34 2014 +0200
    11.2 +++ b/src/ZF/UNITY/SubstAx.thy	Sat Aug 16 11:35:33 2014 +0200
    11.3 @@ -358,7 +358,7 @@
    11.4                  REPEAT (ares_tac [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis},
    11.5                                    @{thm EnsuresI}, @{thm ensuresI}] 1),
    11.6              (*now there are two subgoals: co & transient*)
    11.7 -            simp_tac (ctxt addsimps (Program_Defs.get ctxt)) 2,
    11.8 +            simp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems program})) 2,
    11.9              res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2,
   11.10                 (*simplify the command's domain*)
   11.11              simp_tac (ctxt addsimps [@{thm domain_def}]) 3,