# HG changeset patch
# User blanchet
# Date 1347377769 -7200
# Node ID 5f39b7940b4964159412108f1c0dc48c9fe882b1
# Parent  97809ae5f7bb1cc9eb239e063da453ba6b8a7275
spin off "bnf_def_tactics.ML"

diff -r 97809ae5f7bb -r 5f39b7940b49 src/HOL/Codatatype/BNF_Def.thy
--- a/src/HOL/Codatatype/BNF_Def.thy	Tue Sep 11 17:14:49 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Def.thy	Tue Sep 11 17:36:09 2012 +0200
@@ -14,6 +14,7 @@
 and
   "bnf_def" :: thy_goal
 uses
+  "Tools/bnf_def_tactics.ML"
   "Tools/bnf_def.ML"
 begin
 
diff -r 97809ae5f7bb -r 5f39b7940b49 src/HOL/Codatatype/Tools/bnf_comp_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Tue Sep 11 17:14:49 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML	Tue Sep 11 17:36:09 2012 +0200
@@ -33,6 +33,9 @@
 
   val mk_permute_in_alt_tac: ''a list -> ''a list -> tactic
   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_wit_tac: thm list -> tactic
 end;
 
 structure BNF_Comp_Tactics : BNF_COMP_TACTICS =
@@ -391,4 +394,11 @@
   TRY o rtac @{thm csum_Cnotzero2} THEN'
   rtac @{thm ctwo_Cnotzero}) 1;
 
+fun mk_map_wpull_tac comp_in_alt inner_map_wpulls outer_map_wpull =
+  (rtac (@{thm wpull_cong} OF (replicate 3 comp_in_alt)) THEN' rtac outer_map_wpull) 1 THEN
+  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_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));
+
 end;
diff -r 97809ae5f7bb -r 5f39b7940b49 src/HOL/Codatatype/Tools/bnf_def.ML
--- a/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 11 17:14:49 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML	Tue Sep 11 17:36:09 2012 +0200
@@ -98,7 +98,7 @@
 struct
 
 open BNF_Util
-open BNF_Tactics
+open BNF_Def_Tactics
 
 type axioms = {
   map_id: thm,
diff -r 97809ae5f7bb -r 5f39b7940b49 src/HOL/Codatatype/Tools/bnf_def_tactics.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codatatype/Tools/bnf_def_tactics.ML	Tue Sep 11 17:36:09 2012 +0200
@@ -0,0 +1,209 @@
+(*  Title:      HOL/Codatatype/Tools/bnf_def_tactics.ML
+    Author:     Dmitriy Traytel, TU Muenchen
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2012
+
+Tactics for definition of bounded natural functors.
+*)
+
+signature BNF_DEF_TACTICS =
+sig
+  val mk_collect_set_natural_tac: Proof.context -> thm list -> tactic
+  val mk_id': thm -> thm
+  val mk_comp': thm -> thm
+  val mk_in_mono_tac: int -> tactic
+  val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
+  val mk_set_natural': thm -> thm
+
+  val mk_rel_Gr_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
+    {prems: thm list, context: Proof.context} -> tactic
+  val mk_rel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
+  val mk_rel_O_tac: thm -> thm -> thm -> thm -> thm -> thm list ->
+    {prems: thm list, context: Proof.context} -> tactic
+  val mk_in_rel_tac: thm -> int -> {prems: 'b, context: Proof.context} -> tactic
+  val mk_rel_converse_tac: thm -> tactic
+  val mk_rel_converse_le_tac: thm -> thm -> thm -> thm -> thm list ->
+    {prems: thm list, context: Proof.context} -> tactic
+  val mk_rel_mono_tac: thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
+end;
+
+structure BNF_Def_Tactics : BNF_DEF_TACTICS =
+struct
+
+open BNF_Util
+open BNF_Tactics
+
+val set_mp = @{thm set_mp};
+
+fun mk_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply};
+fun mk_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
+fun mk_set_natural' set_natural = set_natural RS @{thm pointfreeE};
+fun mk_in_mono_tac n = if n = 0 then rtac @{thm subset_UNIV} 1
+  else (rtac subsetI THEN'
+  rtac CollectI) 1 THEN
+  REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN
+  REPEAT_DETERM_N (n - 1)
+    ((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN
+  (etac subset_trans THEN' atac) 1;
+
+fun mk_collect_set_natural_tac ctxt set_naturals =
+  substs_tac ctxt (@{thms collect_o image_insert image_empty} @ set_naturals) 1 THEN rtac refl 1;
+
+fun mk_map_wppull_tac map_id map_cong map_wpull map_comp set_naturals =
+  if null set_naturals then
+    EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1
+  else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull},
+    REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull,
+    REPEAT_DETERM o rtac @{thm wpull_thePull}, rtac ballI,
+    REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac CollectI,
+    CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
+      rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac])
+      set_naturals,
+    CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans),
+      rtac (map_comp RS trans RS sym), rtac map_cong,
+      REPEAT_DETERM_N (length set_naturals) o EVERY' [rtac (o_apply RS trans),
+        rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm,
+        rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1;
+
+fun mk_rel_Gr_tac rel_def map_id map_cong map_wpull in_cong map_id' map_comp set_naturals
+  {context = ctxt, prems = _} =
+  let
+    val n = length set_naturals;
+  in
+    if null set_naturals then
+      Local_Defs.unfold_tac ctxt [rel_def] THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
+    else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN
+      EVERY' [rtac equalityI, rtac subsetI,
+        REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
+        REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+        REPEAT_DETERM o etac conjE, hyp_subst_tac,
+        rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+        rtac sym, rtac trans, rtac map_comp, rtac map_cong,
+        REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac,
+          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
+          rtac (o_apply RS trans), rtac (@{thm fst_conv} RS arg_cong RS trans),
+          rtac (@{thm snd_conv} RS sym)],
+        rtac CollectI,
+        CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
+          rtac @{thm image_subsetI}, dtac @{thm set_rev_mp}, atac,
+          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
+          stac @{thm fst_conv}, atac]) set_naturals,
+        rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE],
+        REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+        REPEAT_DETERM o etac conjE, hyp_subst_tac,
+        rtac allE, rtac subst, rtac @{thm wpull_def}, rtac map_wpull,
+        REPEAT_DETERM_N n o rtac @{thm wpull_Gr}, etac allE, etac impE, rtac conjI, atac,
+        rtac conjI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
+        CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
+          rtac @{thm image_mono}, atac]) set_naturals,
+        rtac sym, rtac map_id', REPEAT_DETERM o eresolve_tac [bexE, conjE],
+        rtac @{thm relcompI}, rtac @{thm converseI},
+        REPEAT_DETERM_N 2 o EVERY' [rtac CollectI, rtac exI,
+          rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, etac sym,
+          etac @{thm set_rev_mp}, rtac equalityD1, rtac in_cong,
+          REPEAT_DETERM_N n o rtac @{thm Gr_def}]] 1
+  end;
+
+fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} =
+  Local_Defs.unfold_tac ctxt [rel_Gr, @{thm Id_alt}] THEN
+  subst_tac ctxt [map_id] 1 THEN
+    (if n = 0 then rtac refl 1
+    else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
+      rtac equalityI, rtac @{thm subset_UNIV}, rtac subsetI, rtac CollectI,
+      CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto n), rtac refl] 1);
+
+fun mk_rel_mono_tac rel_def in_mono {context = ctxt, prems = _} =
+  Local_Defs.unfold_tac ctxt [rel_def] THEN
+    EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]},
+      rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac,
+      rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1;
+
+fun mk_rel_converse_le_tac rel_def rel_Id map_cong map_comp set_naturals
+  {context = ctxt, prems = _} =
+  let
+    val n = length set_naturals;
+  in
+    if null set_naturals then
+      Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
+    else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN
+      EVERY' [rtac @{thm subrelI},
+        REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
+        REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+        REPEAT_DETERM o etac conjE, hyp_subst_tac, rtac @{thm converseI},
+        rtac @{thm relcompI}, rtac @{thm converseI},
+        EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
+          rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac trans,
+          rtac map_cong, REPEAT_DETERM_N n o rtac thm,
+          rtac (map_comp RS sym), rtac CollectI,
+          CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
+            etac @{thm flip_rel}]) set_naturals]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
+  end;
+
+fun mk_rel_converse_tac le_converse =
+  EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift},
+    rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1;
+
+fun mk_rel_O_tac rel_def rel_Id map_cong map_wppull map_comp set_naturals
+  {context = ctxt, prems = _} =
+  let
+    val n = length set_naturals;
+    fun in_tac nthO_in = rtac CollectI THEN'
+        CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
+          rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals;
+  in
+    if null set_naturals then Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
+    else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN
+      EVERY' [rtac equalityI, rtac @{thm subrelI},
+        REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
+        REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+        REPEAT_DETERM o etac conjE, hyp_subst_tac,
+        rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI},
+        rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+        rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
+        REPEAT_DETERM_N n o rtac @{thm fst_fstO},
+        in_tac @{thm fstO_in},
+        rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+        rtac sym, rtac trans, rtac map_comp, rtac map_cong,
+        REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, rtac ballE, rtac subst,
+          rtac @{thm csquare_def}, rtac @{thm csquare_fstO_sndO}, atac, etac notE,
+          etac set_mp, atac],
+        in_tac @{thm fstO_in},
+        rtac @{thm relcompI}, rtac @{thm converseI},
+        rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+        rtac sym, rtac trans, rtac map_comp, rtac map_cong,
+        REPEAT_DETERM_N n o rtac o_apply,
+        in_tac @{thm sndO_in},
+        rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+        rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
+        REPEAT_DETERM_N n o rtac @{thm snd_sndO},
+        in_tac @{thm sndO_in},
+        rtac @{thm subrelI},
+        REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
+        REPEAT_DETERM o eresolve_tac [exE, conjE],
+        REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+        REPEAT_DETERM o etac conjE, hyp_subst_tac,
+        rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull,
+        CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_naturals,
+        etac allE, etac impE, etac conjI, etac conjI, atac,
+        REPEAT_DETERM o eresolve_tac [bexE, conjE],
+        rtac @{thm relcompI}, rtac @{thm converseI},
+        EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
+          rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac sym, rtac trans,
+          rtac trans, rtac map_cong, REPEAT_DETERM_N n o rtac thm,
+          rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1
+  end;
+
+fun mk_in_rel_tac rel_def m {context = ctxt, prems = _} =
+  let
+    val ls' = replicate (Int.max (1, m)) ();
+  in
+    Local_Defs.unfold_tac ctxt (rel_def ::
+      @{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN
+    EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI,
+      rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl,
+      REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI,
+      REPEAT_DETERM_N 2 o EVERY' [rtac exI, rtac conjI, etac @{thm conjI[OF refl sym]},
+        CONJ_WRAP' (K atac) ls']] 1
+  end;
+
+end;
diff -r 97809ae5f7bb -r 5f39b7940b49 src/HOL/Codatatype/Tools/bnf_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_tactics.ML	Tue Sep 11 17:14:49 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML	Tue Sep 11 17:36:09 2012 +0200
@@ -23,30 +23,11 @@
   val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
   val mk_Abs_inj_thm: thm -> thm
 
-  val mk_Card_order_tac: thm -> tactic
-  val mk_collect_set_natural_tac: Proof.context -> thm list -> tactic
-  val mk_id': thm -> thm
-  val mk_comp': thm -> thm
-  val mk_in_mono_tac: int -> tactic
+  val mk_pred_unfold_tac: thm -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
+
   val mk_map_comp_id_tac: thm -> tactic
   val mk_map_cong_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic
   val mk_map_congL_tac: int -> thm -> thm -> tactic
-  val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
-  val mk_map_wpull_tac: thm -> thm list -> thm -> tactic
-  val mk_set_natural': thm -> thm
-  val mk_simple_wit_tac: thm list -> tactic
-
-  val mk_pred_unfold_tac: thm -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
-  val mk_rel_Gr_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
-    {prems: thm list, context: Proof.context} -> tactic
-  val mk_rel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
-  val mk_rel_O_tac: thm -> thm -> thm -> thm -> thm -> thm list ->
-    {prems: thm list, context: Proof.context} -> tactic
-  val mk_in_rel_tac: thm -> int -> {prems: 'b, context: Proof.context} -> tactic
-  val mk_rel_converse_tac: thm -> tactic
-  val mk_rel_converse_le_tac: thm -> thm -> thm -> thm -> thm list ->
-    {prems: thm list, context: Proof.context} -> tactic
-  val mk_rel_mono_tac: thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
 end;
 
 structure BNF_Tactics : BNF_TACTICS =
@@ -56,8 +37,6 @@
 
 fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms;
 
-val set_mp = @{thm set_mp};
-
 fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl,
   tac, REPEAT_DETERM_N (n - k) o etac thin_rl]);
 
@@ -108,206 +87,22 @@
     gen_tac
   end;
 
-fun mk_Card_order_tac card_order =
-  (rtac conjE THEN'
-  rtac @{thm card_order_on_Card_order} THEN'
-  rtac card_order THEN'
-  atac) 1;
-
-fun mk_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply};
-fun mk_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
-fun mk_set_natural' set_natural = set_natural RS @{thm pointfreeE};
-fun mk_in_mono_tac n = if n = 0 then rtac @{thm subset_UNIV} 1
-  else (rtac subsetI THEN'
-  rtac CollectI) 1 THEN
-  REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN
-  REPEAT_DETERM_N (n - 1)
-    ((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN
-  (etac subset_trans THEN' atac) 1;
-
-fun mk_map_wpull_tac comp_in_alt inner_map_wpulls outer_map_wpull =
-  (rtac (@{thm wpull_cong} OF (replicate 3 comp_in_alt)) THEN' rtac outer_map_wpull) 1 THEN
-  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_collect_set_natural_tac ctxt set_naturals =
-  substs_tac ctxt (@{thms collect_o image_insert image_empty} @ set_naturals) 1 THEN rtac refl 1;
-
-fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));
+fun mk_pred_unfold_tac pred_def pred_defs rel_unfold {context = ctxt, prems = _} =
+  Local_Defs.unfold_tac ctxt (@{thm mem_Collect_eq_split} :: pred_def :: pred_defs) THEN
+  rtac rel_unfold 1;
 
 fun mk_map_comp_id_tac map_comp =
   (rtac trans THEN' rtac map_comp) 1 THEN
   REPEAT_DETERM (stac @{thm o_id} 1) THEN
   rtac refl 1;
 
+fun mk_map_cong_tac m map_cong {context = ctxt, prems = _} =
+  EVERY' [rtac mp, rtac map_cong,
+    CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1;
+
 fun mk_map_congL_tac passive map_cong map_id' =
   (rtac trans THEN' rtac map_cong THEN' EVERY' (replicate passive (rtac refl))) 1 THEN
   REPEAT_DETERM (EVERY' [rtac trans, etac bspec, atac, rtac sym, rtac @{thm id_apply}] 1) THEN
   rtac map_id' 1;
 
-fun mk_map_wppull_tac map_id map_cong map_wpull map_comp set_naturals =
-  if null set_naturals then
-    EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1
-  else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull},
-    REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull,
-    REPEAT_DETERM o rtac @{thm wpull_thePull}, rtac ballI,
-    REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac CollectI,
-    CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
-      rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac])
-      set_naturals,
-    CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans),
-      rtac (map_comp RS trans RS sym), rtac map_cong,
-      REPEAT_DETERM_N (length set_naturals) o EVERY' [rtac (o_apply RS trans),
-        rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm,
-        rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1;
-
-fun mk_rel_Gr_tac rel_def map_id map_cong map_wpull in_cong map_id' map_comp set_naturals
-  {context = ctxt, prems = _} =
-  let
-    val n = length set_naturals;
-  in
-    if null set_naturals then
-      Local_Defs.unfold_tac ctxt [rel_def] THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
-    else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN
-      EVERY' [rtac equalityI, rtac subsetI,
-        REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
-        REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
-        REPEAT_DETERM o etac conjE, hyp_subst_tac,
-        rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
-        rtac sym, rtac trans, rtac map_comp, rtac map_cong,
-        REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac,
-          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
-          rtac (o_apply RS trans), rtac (@{thm fst_conv} RS arg_cong RS trans),
-          rtac (@{thm snd_conv} RS sym)],
-        rtac CollectI,
-        CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
-          rtac @{thm image_subsetI}, dtac @{thm set_rev_mp}, atac,
-          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
-          stac @{thm fst_conv}, atac]) set_naturals,
-        rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE],
-        REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
-        REPEAT_DETERM o etac conjE, hyp_subst_tac,
-        rtac allE, rtac subst, rtac @{thm wpull_def}, rtac map_wpull,
-        REPEAT_DETERM_N n o rtac @{thm wpull_Gr}, etac allE, etac impE, rtac conjI, atac,
-        rtac conjI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
-        CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
-          rtac @{thm image_mono}, atac]) set_naturals,
-        rtac sym, rtac map_id', REPEAT_DETERM o eresolve_tac [bexE, conjE],
-        rtac @{thm relcompI}, rtac @{thm converseI},
-        REPEAT_DETERM_N 2 o EVERY' [rtac CollectI, rtac exI,
-          rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, etac sym,
-          etac @{thm set_rev_mp}, rtac equalityD1, rtac in_cong,
-          REPEAT_DETERM_N n o rtac @{thm Gr_def}]] 1
-  end;
-
-fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} =
-  Local_Defs.unfold_tac ctxt [rel_Gr, @{thm Id_alt}] THEN
-  subst_tac ctxt [map_id] 1 THEN
-    (if n = 0 then rtac refl 1
-    else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
-      rtac equalityI, rtac @{thm subset_UNIV}, rtac subsetI, rtac CollectI,
-      CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto n), rtac refl] 1);
-
-fun mk_rel_mono_tac rel_def in_mono {context = ctxt, prems = _} =
-  Local_Defs.unfold_tac ctxt [rel_def] THEN
-    EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]},
-      rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac,
-      rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1;
-
-fun mk_map_cong_tac m map_cong {context = ctxt, prems = _} =
-  EVERY' [rtac mp, rtac map_cong,
-    CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1;
-
-fun mk_rel_converse_le_tac rel_def rel_Id map_cong map_comp set_naturals
-  {context = ctxt, prems = _} =
-  let
-    val n = length set_naturals;
-  in
-    if null set_naturals then
-      Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
-    else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN
-      EVERY' [rtac @{thm subrelI},
-        REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
-        REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
-        REPEAT_DETERM o etac conjE, hyp_subst_tac, rtac @{thm converseI},
-        rtac @{thm relcompI}, rtac @{thm converseI},
-        EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
-          rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac trans,
-          rtac map_cong, REPEAT_DETERM_N n o rtac thm,
-          rtac (map_comp RS sym), rtac CollectI,
-          CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
-            etac @{thm flip_rel}]) set_naturals]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
-  end;
-
-fun mk_rel_converse_tac le_converse =
-  EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift},
-    rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1;
-
-fun mk_rel_O_tac rel_def rel_Id map_cong map_wppull map_comp set_naturals
-  {context = ctxt, prems = _} =
-  let
-    val n = length set_naturals;
-    fun in_tac nthO_in = rtac CollectI THEN'
-        CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
-          rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals;
-  in
-    if null set_naturals then Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
-    else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN
-      EVERY' [rtac equalityI, rtac @{thm subrelI},
-        REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
-        REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
-        REPEAT_DETERM o etac conjE, hyp_subst_tac,
-        rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI},
-        rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
-        rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
-        REPEAT_DETERM_N n o rtac @{thm fst_fstO},
-        in_tac @{thm fstO_in},
-        rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
-        rtac sym, rtac trans, rtac map_comp, rtac map_cong,
-        REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, rtac ballE, rtac subst,
-          rtac @{thm csquare_def}, rtac @{thm csquare_fstO_sndO}, atac, etac notE,
-          etac set_mp, atac],
-        in_tac @{thm fstO_in},
-        rtac @{thm relcompI}, rtac @{thm converseI},
-        rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
-        rtac sym, rtac trans, rtac map_comp, rtac map_cong,
-        REPEAT_DETERM_N n o rtac o_apply,
-        in_tac @{thm sndO_in},
-        rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
-        rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
-        REPEAT_DETERM_N n o rtac @{thm snd_sndO},
-        in_tac @{thm sndO_in},
-        rtac @{thm subrelI},
-        REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
-        REPEAT_DETERM o eresolve_tac [exE, conjE],
-        REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
-        REPEAT_DETERM o etac conjE, hyp_subst_tac,
-        rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull,
-        CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_naturals,
-        etac allE, etac impE, etac conjI, etac conjI, atac,
-        REPEAT_DETERM o eresolve_tac [bexE, conjE],
-        rtac @{thm relcompI}, rtac @{thm converseI},
-        EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
-          rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac sym, rtac trans,
-          rtac trans, rtac map_cong, REPEAT_DETERM_N n o rtac thm,
-          rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1
-  end;
-
-fun mk_in_rel_tac rel_def m {context = ctxt, prems = _} =
-  let
-    val ls' = replicate (Int.max (1, m)) ();
-  in
-    Local_Defs.unfold_tac ctxt (rel_def ::
-      @{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN
-    EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI,
-      rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl,
-      REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI,
-      REPEAT_DETERM_N 2 o EVERY' [rtac exI, rtac conjI, etac @{thm conjI[OF refl sym]},
-        CONJ_WRAP' (K atac) ls']] 1
-  end;
-
-fun mk_pred_unfold_tac pred_def pred_defs rel_unfold {context = ctxt, prems = _} =
-  Local_Defs.unfold_tac ctxt (@{thm mem_Collect_eq_split} :: pred_def :: pred_defs) THEN
-  rtac rel_unfold 1;
-
 end;