--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Aug 15 18:02:34 2014 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sat Aug 16 11:35:33 2014 +0200
@@ -28,8 +28,6 @@
val domain_isomorphism_cmd :
(string list * binding * mixfix * string * (binding * binding) option) list
-> theory -> theory
-
- val setup : theory -> theory
end
structure Domain_Isomorphism : DOMAIN_ISOMORPHISM =
@@ -41,24 +39,6 @@
fun is_cpo thy T = Sign.of_sort thy (T, @{sort cpo})
-(******************************************************************************)
-(******************************** theory data *********************************)
-(******************************************************************************)
-
-structure RepData = Named_Thms
-(
- val name = @{binding domain_defl_simps}
- val description = "theorems like DEFL('a t) = t_defl$DEFL('a)"
-)
-
-structure IsodeflData = Named_Thms
-(
- val name = @{binding domain_isodefl}
- val description = "theorems like isodefl d t ==> isodefl (foo_map$d) (foo_defl$t)"
-)
-
-val setup = RepData.setup #> IsodeflData.setup
-
(******************************************************************************)
(************************** building types and terms **************************)
@@ -170,7 +150,7 @@
val cont_thm =
let
val prop = mk_trp (mk_cont functional)
- val rules = Cont2ContData.get (Proof_Context.init_global thy)
+ val rules = Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems cont2cont}
val tac = REPEAT_ALL_NEW (match_tac rules) 1
in
Goal.prove_global thy [] [] prop (K tac)
@@ -207,7 +187,8 @@
(tab2 : (typ * term) list)
(T : typ) : term =
let
- val defl_simps = RepData.get (Proof_Context.init_global thy)
+ val defl_simps =
+ Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_defl_simps}
val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) defl_simps
val rules' = map (apfst mk_DEFL) tab1 @ map (apfst mk_LIFTDEFL) tab2
fun proc1 t =
@@ -522,7 +503,8 @@
val ((_, _, _, {DEFL, ...}), thy) =
Domaindef.add_domaindef spec defl NONE thy
(* declare domain_defl_simps rules *)
- val thy = Context.theory_map (RepData.add_thm DEFL) thy
+ val thy =
+ Context.theory_map (Named_Theorems.add_thm @{named_theorems domain_defl_simps} DEFL) thy
in
(DEFL, thy)
end
@@ -532,7 +514,8 @@
fun mk_DEFL_eq_thm (lhsT, rhsT) =
let
val goal = mk_eqs (mk_DEFL lhsT, mk_DEFL rhsT)
- val DEFL_simps = RepData.get (Proof_Context.init_global thy)
+ val DEFL_simps =
+ Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_defl_simps}
fun tac ctxt =
rewrite_goals_tac ctxt (map mk_meta_eq DEFL_simps)
THEN TRY (resolve_tac defl_unfold_thms 1)
@@ -637,7 +620,7 @@
val isodefl_rules =
@{thms conjI isodefl_ID_DEFL isodefl_LIFTDEFL}
@ isodefl_abs_rep_thms
- @ IsodeflData.get (Proof_Context.init_global thy)
+ @ Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_isodefl}
in
Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>
EVERY
@@ -661,7 +644,9 @@
val (isodefl_thms, thy) = thy |>
(Global_Theory.add_thms o map (Thm.no_attributes o apsnd Drule.zero_var_indexes))
(conjuncts isodefl_binds isodefl_thm)
- val thy = fold (Context.theory_map o IsodeflData.add_thm) isodefl_thms thy
+ val thy =
+ fold (Context.theory_map o Named_Theorems.add_thm @{named_theorems domain_isodefl})
+ isodefl_thms thy
(* prove map_ID theorems *)
fun prove_map_ID_thm