renamed 'rel_mono_strong' to 'rel_mono_strong0'
authordesharna
Mon Aug 18 13:46:22 2014 +0200 (2014-08-18)
changeset 57967e6d2e998c30f
parent 57966 6fab7e95587d
child 57968 00e9c6d367e7
renamed 'rel_mono_strong' to 'rel_mono_strong0'
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_def_tactics.ML
src/HOL/Tools/BNF/bnf_lfp.ML
src/HOL/Tools/BNF/bnf_lfp_tactics.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Sun Aug 17 22:27:58 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Mon Aug 18 13:46:22 2014 +0200
     1.3 @@ -73,7 +73,7 @@
     1.4    val rel_cong_of_bnf: bnf -> thm
     1.5    val rel_conversep_of_bnf: bnf -> thm
     1.6    val rel_mono_of_bnf: bnf -> thm
     1.7 -  val rel_mono_strong_of_bnf: bnf -> thm
     1.8 +  val rel_mono_strong0_of_bnf: bnf -> thm
     1.9    val rel_eq_of_bnf: bnf -> thm
    1.10    val rel_flip_of_bnf: bnf -> thm
    1.11    val set_bd_of_bnf: bnf -> thm list
    1.12 @@ -234,7 +234,7 @@
    1.13    rel_cong: thm lazy,
    1.14    rel_map: thm list lazy,
    1.15    rel_mono: thm lazy,
    1.16 -  rel_mono_strong: thm lazy,
    1.17 +  rel_mono_strong0: thm lazy,
    1.18    rel_Grp: thm lazy,
    1.19    rel_conversep: thm lazy,
    1.20    rel_OO: thm lazy
    1.21 @@ -242,7 +242,7 @@
    1.22  
    1.23  fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
    1.24      inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq rel_flip set_map
    1.25 -    rel_cong rel_map rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO = {
    1.26 +    rel_cong rel_map rel_mono rel_mono_strong0 rel_Grp rel_conversep rel_OO = {
    1.27    bd_Card_order = bd_Card_order,
    1.28    bd_Cinfinite = bd_Cinfinite,
    1.29    bd_Cnotzero = bd_Cnotzero,
    1.30 @@ -264,7 +264,7 @@
    1.31    rel_cong = rel_cong,
    1.32    rel_map = rel_map,
    1.33    rel_mono = rel_mono,
    1.34 -  rel_mono_strong = rel_mono_strong,
    1.35 +  rel_mono_strong0 = rel_mono_strong0,
    1.36    rel_Grp = rel_Grp,
    1.37    rel_conversep = rel_conversep,
    1.38    rel_OO = rel_OO};
    1.39 @@ -291,7 +291,7 @@
    1.40    rel_cong,
    1.41    rel_map,
    1.42    rel_mono,
    1.43 -  rel_mono_strong,
    1.44 +  rel_mono_strong0,
    1.45    rel_Grp,
    1.46    rel_conversep,
    1.47    rel_OO} =
    1.48 @@ -316,7 +316,7 @@
    1.49      rel_cong = Lazy.map f rel_cong,
    1.50      rel_map = Lazy.map (map f) rel_map,
    1.51      rel_mono = Lazy.map f rel_mono,
    1.52 -    rel_mono_strong = Lazy.map f rel_mono_strong,
    1.53 +    rel_mono_strong0 = Lazy.map f rel_mono_strong0,
    1.54      rel_Grp = Lazy.map f rel_Grp,
    1.55      rel_conversep = Lazy.map f rel_conversep,
    1.56      rel_OO = Lazy.map f rel_OO};
    1.57 @@ -445,7 +445,7 @@
    1.58  val set_map_of_bnf = map Lazy.force o #set_map o #facts o rep_bnf;
    1.59  val rel_cong_of_bnf = Lazy.force o #rel_cong o #facts o rep_bnf;
    1.60  val rel_mono_of_bnf = Lazy.force o #rel_mono o #facts o rep_bnf;
    1.61 -val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf;
    1.62 +val rel_mono_strong0_of_bnf = Lazy.force o #rel_mono_strong0 o #facts o rep_bnf;
    1.63  val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
    1.64  val rel_conversep_of_bnf = Lazy.force o #rel_conversep o #facts o rep_bnf;
    1.65  val rel_OO_of_bnf = Lazy.force o #rel_OO o #facts o rep_bnf;
    1.66 @@ -615,7 +615,7 @@
    1.67  val rel_conversepN = "rel_conversep";
    1.68  val rel_mapN = "rel_map"
    1.69  val rel_monoN = "rel_mono"
    1.70 -val rel_mono_strongN = "rel_mono_strong"
    1.71 +val rel_mono_strong0N = "rel_mono_strong0"
    1.72  val rel_comppN = "rel_compp";
    1.73  val rel_compp_GrpN = "rel_compp_Grp";
    1.74  
    1.75 @@ -655,7 +655,7 @@
    1.76             (inj_mapN, [Lazy.force (#inj_map facts)]),
    1.77             (map_comp0N, [#map_comp0 axioms]),
    1.78             (map_transferN, [Lazy.force (#map_transfer facts)]),
    1.79 -           (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
    1.80 +           (rel_mono_strong0N, [Lazy.force (#rel_mono_strong0 facts)]),
    1.81             (set_map0N, #set_map0 axioms),
    1.82             (set_bdN, #set_bd axioms)] @
    1.83            (witNs ~~ wit_thmss_of_bnf bnf)
    1.84 @@ -1299,7 +1299,7 @@
    1.85  
    1.86          val rel_flip = Lazy.lazy mk_rel_flip;
    1.87  
    1.88 -        fun mk_rel_mono_strong () =
    1.89 +        fun mk_rel_mono_strong0 () =
    1.90            let
    1.91              fun mk_prem setA setB R S a b =
    1.92                HOLogic.mk_Trueprop
    1.93 @@ -1312,12 +1312,12 @@
    1.94            in
    1.95              Goal.prove_sorry lthy [] []
    1.96                (fold_rev Logic.all (x :: y :: Rs @ Rs_copy) (Logic.list_implies (prems, concl)))
    1.97 -              (fn {context = ctxt, prems = _} => mk_rel_mono_strong_tac ctxt (Lazy.force in_rel)
    1.98 +              (fn {context = ctxt, prems = _} => mk_rel_mono_strong0_tac ctxt (Lazy.force in_rel)
    1.99                  (map Lazy.force set_map))
   1.100              |> Thm.close_derivation
   1.101            end;
   1.102  
   1.103 -        val rel_mono_strong = Lazy.lazy mk_rel_mono_strong;
   1.104 +        val rel_mono_strong0 = Lazy.lazy mk_rel_mono_strong0;
   1.105  
   1.106          fun mk_rel_map () =
   1.107            let
   1.108 @@ -1368,7 +1368,7 @@
   1.109  
   1.110          val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
   1.111            in_mono in_rel inj_map map_comp map_cong map_id map_ident0 map_ident map_transfer rel_eq
   1.112 -          rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
   1.113 +          rel_flip set_map rel_cong rel_map rel_mono rel_mono_strong0 rel_Grp rel_conversep rel_OO;
   1.114  
   1.115          val wits = map2 mk_witness bnf_wits wit_thms;
   1.116  
     2.1 --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Sun Aug 17 22:27:58 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Mon Aug 18 13:46:22 2014 +0200
     2.3 @@ -25,7 +25,7 @@
     2.4    val mk_rel_conversep_le_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm list -> tactic
     2.5    val mk_rel_map0_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> tactic
     2.6    val mk_rel_mono_tac: thm list -> thm -> tactic
     2.7 -  val mk_rel_mono_strong_tac: Proof.context -> thm -> thm list -> tactic
     2.8 +  val mk_rel_mono_strong0_tac: Proof.context -> thm -> thm list -> tactic
     2.9  
    2.10    val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic
    2.11  
    2.12 @@ -211,7 +211,7 @@
    2.13          in_tac @{thm sndOp_in}] 1
    2.14    end;
    2.15  
    2.16 -fun mk_rel_mono_strong_tac ctxt in_rel set_maps =
    2.17 +fun mk_rel_mono_strong0_tac ctxt in_rel set_maps =
    2.18    if null set_maps then atac 1
    2.19    else
    2.20      unfold_tac ctxt [in_rel] THEN
     3.1 --- a/src/HOL/Tools/BNF/bnf_lfp.ML	Sun Aug 17 22:27:58 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML	Mon Aug 18 13:46:22 2014 +0200
     3.3 @@ -167,7 +167,7 @@
     3.4      val map_id0s = map map_id0_of_bnf bnfs;
     3.5      val map_ids = map map_id_of_bnf bnfs;
     3.6      val set_mapss = map set_map_of_bnf bnfs;
     3.7 -    val rel_mono_strongs = map rel_mono_strong_of_bnf bnfs;
     3.8 +    val rel_mono_strong0s = map rel_mono_strong0_of_bnf bnfs;
     3.9      val le_rel_OOs = map le_rel_OO_of_bnf bnfs;
    3.10  
    3.11      val timer = time (timer "Extracted terms & thms");
    3.12 @@ -1691,7 +1691,7 @@
    3.13            in
    3.14              Goal.prove_sorry lthy [] [] goal
    3.15                (fn {context = ctxt, prems = _} => mk_le_rel_OO_tac ctxt m induct ctor_nchotomy_thms
    3.16 -                ctor_Irel_thms rel_mono_strongs le_rel_OOs)
    3.17 +                ctor_Irel_thms rel_mono_strong0s le_rel_OOs)
    3.18              |> Thm.close_derivation
    3.19              |> singleton (Proof_Context.export names_lthy lthy)
    3.20            end;
    3.21 @@ -1762,7 +1762,7 @@
    3.22      val Irel_induct_thm =
    3.23        mk_rel_xtor_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's
    3.24          (fn {context = ctxt, prems = IHs} => mk_rel_induct_tac ctxt IHs m ctor_induct2_thm ks
    3.25 -           ctor_Irel_thms rel_mono_strongs) lthy;
    3.26 +           ctor_Irel_thms rel_mono_strong0s) lthy;
    3.27  
    3.28      val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
    3.29      val ctor_fold_transfer_thms =
     4.1 --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Sun Aug 17 22:27:58 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML	Mon Aug 18 13:46:22 2014 +0200
     4.3 @@ -582,7 +582,7 @@
     4.4      (induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1
     4.5    end;
     4.6  
     4.7 -fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strongs le_rel_OOs =
     4.8 +fun mk_le_rel_OO_tac ctxt m induct ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs =
     4.9    EVERY' (rtac induct ::
    4.10    map4 (fn nchotomy => fn Irel => fn rel_mono => fn le_rel_OO =>
    4.11      EVERY' [rtac impI, etac (nchotomy RS @{thm nchotomy_relcomppE}),
    4.12 @@ -592,7 +592,7 @@
    4.13        REPEAT_DETERM_N m o EVERY' [rtac ballI, rtac ballI, rtac impI, atac],
    4.14        REPEAT_DETERM_N (length le_rel_OOs) o
    4.15          EVERY' [rtac ballI, rtac ballI, Goal.assume_rule_tac ctxt]])
    4.16 -  ctor_nchotomys ctor_Irels rel_mono_strongs le_rel_OOs) 1;
    4.17 +  ctor_nchotomys ctor_Irels rel_mono_strong0s le_rel_OOs) 1;
    4.18  
    4.19  (* BNF tactics *)
    4.20  
    4.21 @@ -701,19 +701,19 @@
    4.22      EVERY' [rtac iffI, if_tac, only_if_tac] 1
    4.23    end;
    4.24  
    4.25 -fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strongs =
    4.26 +fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strong0s =
    4.27    let val n = length ks;
    4.28    in
    4.29      unfold_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
    4.30      EVERY' [REPEAT_DETERM o rtac allI, rtac ctor_induct2,
    4.31 -      EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong =>
    4.32 +      EVERY' (map3 (fn IH => fn ctor_rel => fn rel_mono_strong0 =>
    4.33          EVERY' [rtac impI, dtac (ctor_rel RS iffD1), rtac (IH RS @{thm spec2} RS mp),
    4.34 -          etac rel_mono_strong,
    4.35 +          etac rel_mono_strong0,
    4.36            REPEAT_DETERM_N m o rtac @{thm ballI[OF ballI[OF imp_refl]]},
    4.37            EVERY' (map (fn j =>
    4.38              EVERY' [select_prem_tac n (dtac asm_rl) j, rtac @{thm ballI[OF ballI]},
    4.39                Goal.assume_rule_tac ctxt]) ks)])
    4.40 -      IHs ctor_rels rel_mono_strongs)] 1
    4.41 +      IHs ctor_rels rel_mono_strong0s)] 1
    4.42    end;
    4.43  
    4.44  fun mk_fold_transfer_tac ctxt m ctor_rel_induct map_transfers folds =