src/HOL/Codatatype/Tools/bnf_comp_tactics.ML

--- a/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Thu Sep 20 02:42:49 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Thu Sep 20 02:42:49 2012 +0200
@@ -35,6 +35,7 @@
   val mk_permute_in_bd_tac: ''a list -> ''a list -> thm -> thm -> thm -> tactic
 
   val mk_map_wpull_tac: thm -> thm list -> thm -> tactic
+  val mk_simple_rel_O_Gr_tac: Proof.context -> thm -> thm -> thm -> tactic
   val mk_simple_wit_tac: thm list -> tactic
 end;
 
@@ -65,8 +66,8 @@
 (* Composition *)
 
 fun mk_comp_set_alt_tac ctxt collect_set_natural =
-  Local_Defs.unfold_tac ctxt @{thms sym[OF o_assoc]} THEN
-  Local_Defs.unfold_tac ctxt [collect_set_natural RS sym] THEN
+  unfold_defs_tac ctxt @{thms sym[OF o_assoc]} THEN
+  unfold_defs_tac ctxt [collect_set_natural RS sym] THEN
   rtac refl 1;
 
 fun mk_comp_map_comp_tac Gmap_comp Gmap_cong map_comps =
@@ -139,10 +140,9 @@
       rtac bd;
     fun gen_after _ = rtac @{thm ordIso_imp_ordLeq} THEN' rtac @{thm cprod_csum_distrib1};
   in
-    Local_Defs.unfold_tac ctxt [comp_set_alt] THEN
+    unfold_defs_tac ctxt [comp_set_alt] THEN
     rtac @{thm comp_set_bd_Union_o_collect} 1 THEN
-    Local_Defs.unfold_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib
-      o_apply} THEN
+    unfold_defs_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN
     (rtac ctrans THEN'
      WRAP' gen_before gen_after bds (rtac last_bd) THEN'
      rtac @{thm ordIso_imp_ordLeq} THEN'
@@ -154,12 +154,12 @@
   conj_assoc};
 
 fun mk_comp_in_alt_tac ctxt comp_set_alts =
-  Local_Defs.unfold_tac ctxt (comp_set_alts @ comp_in_alt_thms) THEN
-  Local_Defs.unfold_tac ctxt @{thms set_eq_subset} THEN
+  unfold_defs_tac ctxt (comp_set_alts @ comp_in_alt_thms) THEN
+  unfold_defs_tac ctxt @{thms set_eq_subset} THEN
   rtac conjI 1 THEN
   REPEAT_DETERM (
     rtac @{thm subsetI} 1 THEN
-    Local_Defs.unfold_tac ctxt @{thms mem_Collect_eq Ball_def} THEN
+    unfold_defs_tac ctxt @{thms mem_Collect_eq Ball_def} THEN
     (REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
      REPEAT_DETERM (CHANGED ((
        (rtac conjI THEN' (atac ORELSE' rtac subset_UNIV)) ORELSE'
@@ -216,7 +216,7 @@
 
 fun mk_comp_wit_tac ctxt Gwit_thms collect_set_natural Fwit_thms =
   ALLGOALS (dtac @{thm in_Union_o_assoc}) THEN
-  Local_Defs.unfold_tac ctxt (collect_set_natural :: comp_wit_thms) THEN
+  unfold_defs_tac ctxt (collect_set_natural :: comp_wit_thms) THEN
   REPEAT_DETERM (
     atac 1 ORELSE
     REPEAT_DETERM (eresolve_tac @{thms UnionE UnE imageE} 1) THEN
@@ -409,6 +409,10 @@
   WRAP (fn thm => rtac thm 1 THEN REPEAT_DETERM (atac 1)) (K all_tac) inner_map_wpulls all_tac THEN
   TRY (REPEAT_DETERM (atac 1 ORELSE rtac @{thm wpull_id} 1));
 
+fun mk_simple_rel_O_Gr_tac ctxt rel_def rel_O_Gr in_alt_thm =
+  rtac (unfold_defs ctxt [rel_def] (trans OF [rel_O_Gr, in_alt_thm RS @{thm subst_rel_def} RS sym]))
+    1;
+
 fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));
 
 end;