# HG changeset patch
# User desharna
# Date 1408362382 -7200
# Node ID e6d2e998c30fbefb8e0ed2b476742f8c29fcefa1
# Parent  6fab7e95587d0911ae07ae542f71d6af6a399f7f
renamed 'rel_mono_strong' to 'rel_mono_strong0'

diff -r 6fab7e95587d -r e6d2e998c30f src/HOL/Tools/BNF/bnf_def.ML
--- a/src/HOL/Tools/BNF/bnf_def.ML	Sun Aug 17 22:27:58 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Aug 18 13:46:22 2014 +0200
@@ -73,7 +73,7 @@
   val rel_cong_of_bnf: bnf -> thm
   val rel_conversep_of_bnf: bnf -> thm
   val rel_mono_of_bnf: bnf -> thm
-  val rel_mono_strong_of_bnf: bnf -> thm
+  val rel_mono_strong0_of_bnf: bnf -> thm
   val rel_eq_of_bnf: bnf -> thm
   val rel_flip_of_bnf: bnf -> thm
   val set_bd_of_bnf: bnf -> thm list
@@ -234,7 +234,7 @@
   rel_cong: thm lazy,
   rel_map: thm list lazy,
   rel_mono: thm lazy,
-  rel_mono_strong: thm lazy,
+  rel_mono_strong0: thm lazy,
   rel_Grp: thm lazy,
   rel_conversep: thm lazy,
   rel_OO: thm lazy
@@ -242,7 +242,7 @@
 
 fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
     inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq rel_flip set_map
-    rel_cong rel_map rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO = {
+    rel_cong rel_map rel_mono rel_mono_strong0 rel_Grp rel_conversep rel_OO = {
   bd_Card_order = bd_Card_order,
   bd_Cinfinite = bd_Cinfinite,
   bd_Cnotzero = bd_Cnotzero,
@@ -264,7 +264,7 @@
   rel_cong = rel_cong,
   rel_map = rel_map,
   rel_mono = rel_mono,
-  rel_mono_strong = rel_mono_strong,
+  rel_mono_strong0 = rel_mono_strong0,
   rel_Grp = rel_Grp,
   rel_conversep = rel_conversep,
   rel_OO = rel_OO};
@@ -291,7 +291,7 @@
   rel_cong,
   rel_map,
   rel_mono,
-  rel_mono_strong,
+  rel_mono_strong0,
   rel_Grp,
   rel_conversep,
   rel_OO} =
@@ -316,7 +316,7 @@
     rel_cong = Lazy.map f rel_cong,
     rel_map = Lazy.map (map f) rel_map,
     rel_mono = Lazy.map f rel_mono,
-    rel_mono_strong = Lazy.map f rel_mono_strong,
+    rel_mono_strong0 = Lazy.map f rel_mono_strong0,
     rel_Grp = Lazy.map f rel_Grp,
     rel_conversep = Lazy.map f rel_conversep,
     rel_OO = Lazy.map f rel_OO};
@@ -445,7 +445,7 @@
 val set_map_of_bnf = map Lazy.force o #set_map o #facts o rep_bnf;
 val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf;
 val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf;
-val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf;
+val rel_mono_strong0_of_bnf = Lazy.force o #rel_mono_strong0 o #facts o rep_bnf;
 val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
 val rel_conversep_of_bnf = Lazy.force o #rel_conversep o #facts o rep_bnf;
 val rel_OO_of_bnf = Lazy.force o #rel_OO o #facts o rep_bnf;
@@ -615,7 +615,7 @@
 val rel_conversepN = "rel_conversep";
 val rel_mapN = "rel_map"
 val rel_monoN = "rel_mono"
-val rel_mono_strongN = "rel_mono_strong"
+val rel_mono_strong0N = "rel_mono_strong0"
 val rel_comppN = "rel_compp";
 val rel_compp_GrpN = "rel_compp_Grp";
 
@@ -655,7 +655,7 @@
            (inj_mapN, [Lazy.force (#inj_map facts)]),
            (map_comp0N, [#map_comp0 axioms]),
            (map_transferN, [Lazy.force (#map_transfer facts)]),
-           (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
+           (rel_mono_strong0N, [Lazy.force (#rel_mono_strong0 facts)]),
            (set_map0N, #set_map0 axioms),
            (set_bdN, #set_bd axioms)] @
           (witNs ~~ wit_thmss_of_bnf bnf)
@@ -1299,7 +1299,7 @@
 
         val rel_flip = Lazy.lazy mk_rel_flip;
 
-        fun mk_rel_mono_strong () =
+        fun mk_rel_mono_strong0 () =
           let
             fun mk_prem setA setB R S a b =
               HOLogic.mk_Trueprop
@@ -1312,12 +1312,12 @@
           in
             Goal.prove_sorry lthy [] []
               (fold_rev Logic.all (x :: y :: Rs @ Rs_copy) (Logic.list_implies (prems, concl)))
-              (fn {context = ctxt, prems = _} => mk_rel_mono_strong_tac ctxt (Lazy.force in_rel)
+              (fn {context = ctxt, prems = _} => mk_rel_mono_strong0_tac ctxt (Lazy.force in_rel)
                 (map Lazy.force set_map))
             |> Thm.close_derivation
           end;
 
-        val rel_mono_strong = Lazy.lazy mk_rel_mono_strong;
+        val rel_mono_strong0 = Lazy.lazy mk_rel_mono_strong0;
 
         fun mk_rel_map () =
           let
@@ -1368,7 +1368,7 @@
 
         val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
           in_mono in_rel inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq
-          rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
+          rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_Grp rel_conversep rel_OO;
 
         val wits = map2 mk_witness bnf_wits wit_thms;
 
diff -r 6fab7e95587d -r e6d2e998c30f src/HOL/Tools/BNF/bnf_def_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Sun Aug 17 22:27:58 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Mon Aug 18 13:46:22 2014 +0200
@@ -25,7 +25,7 @@
   val mk_rel_conversep_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
   val mk_rel_map0_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic
   val mk_rel_mono_tac: thm list -> thm -> tactic
-  val mk_rel_mono_strong_tac: Proof.context -> thm -> thm list -> tactic
+  val mk_rel_mono_strong0_tac: Proof.context -> thm -> thm list -> tactic
 
   val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic
 
@@ -211,7 +211,7 @@
         in_tac @{thm sndOp_in}] 1
   end;
 
-fun mk_rel_mono_strong_tac ctxt in_rel set_maps =
+fun mk_rel_mono_strong0_tac ctxt in_rel set_maps =
   if null set_maps then atac 1
   else
     unfold_tac ctxt [in_rel] THEN
diff -r 6fab7e95587d -r e6d2e998c30f src/HOL/Tools/BNF/bnf_lfp.ML
--- a/src/HOL/Tools/BNF/bnf_lfp.ML	Sun Aug 17 22:27:58 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Aug 18 13:46:22 2014 +0200
@@ -167,7 +167,7 @@
     val map_id0s = map map_id0_of_bnf bnfs;
     val map_ids = map map_id_of_bnf bnfs;
     val set_mapss = map set_map_of_bnf bnfs;
-    val rel_mono_strongs = map rel_mono_strong_of_bnf bnfs;
+    val rel_mono_strong0s = map rel_mono_strong0_of_bnf bnfs;
     val le_rel_OOs = map le_rel_OO_of_bnf bnfs;
 
     val timer = time (timer "Extracted terms & thms");
@@ -1691,7 +1691,7 @@
           in
             Goal.prove_sorry lthy [] [] goal
               (fn {context = ctxt, prems = _} => mk_le_rel_OO_tac ctxt m induct ctor_nchotomy_thms
-                ctor_Irel_thms rel_mono_strongs le_rel_OOs)
+                ctor_Irel_thms rel_mono_strong0s le_rel_OOs)
             |> Thm.close_derivation
             |> singleton (Proof_Context.export names_lthy lthy)
           end;
@@ -1762,7 +1762,7 @@
     val Irel_induct_thm =
       mk_rel_xtor_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's
         (fn {context = ctxt, prems = IHs} => mk_rel_induct_tac ctxt IHs m ctor_induct2_thm ks
-           ctor_Irel_thms rel_mono_strongs) lthy;
+           ctor_Irel_thms rel_mono_strong0s) lthy;
 
     val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
     val ctor_fold_transfer_thms =
diff -r 6fab7e95587d -r e6d2e998c30f src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Sun Aug 17 22:27:58 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Mon Aug 18 13:46:22 2014 +0200
@@ -582,7 +582,7 @@
     (induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1
   end;
 
-fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strongs le_rel_OOs =
+fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs =
   EVERY' (rtac induct ::
   map4 (fn nchotomy => fn Irel => fn rel_mono => fn le_rel_OO =>
     EVERY' [rtac impI, etac (nchotomy RS @{thm nchotomy_relcomppE}),
@@ -592,7 +592,7 @@
       REPEAT_DETERM_N m o EVERY' [rtac ballI, rtac ballI, rtac impI, atac],
       REPEAT_DETERM_N (length le_rel_OOs) o
         EVERY' [rtac ballI, rtac ballI, Goal.assume_rule_tac ctxt]])
-  ctor_nchotomys ctor_Irels rel_mono_strongs le_rel_OOs) 1;
+  ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs) 1;
 
 (* BNF tactics *)
 
@@ -701,19 +701,19 @@
     EVERY' [rtac iffI, if_tac, only_if_tac] 1
   end;
 
-fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strongs =
+fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strong0s =
   let val n = length ks;
   in
     unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
     EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2,
-      EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong =>
+      EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong0 =>
         EVERY' [rtac impI, dtac (ctor_rel RS iffD1), rtac (IH RS @{thm spec2} RS mp),
-          etac rel_mono_strong,
+          etac rel_mono_strong0,
           REPEAT_DETERM_N m o rtac @{thm ballI[OF ballI[OF imp_refl]]},
           EVERY' (map (fn j =>
             EVERY' [select_prem_tac n (dtac asm_rl) j, rtac @{thm ballI[OF ballI]},
               Goal.assume_rule_tac ctxt]) ks)])
-      IHs ctor_rels rel_mono_strongs)] 1
+      IHs ctor_rels rel_mono_strong0s)] 1
   end;
 
 fun mk_fold_transfer_tac ctxt m ctor_rel_induct map_transfers folds =