src/HOL/BNF/Tools/bnf_gfp_tactics.ML
changeset 51766 f19a4d0ab1bf
parent 51761 4c9f08836d87
child 51782 84e7225f5ab6
     1.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Wed Apr 24 17:03:43 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Wed Apr 24 17:47:22 2013 +0200
     1.3 @@ -110,7 +110,7 @@
     1.4    val mk_set_incl_hin_tac: thm list -> tactic
     1.5    val mk_set_incl_hset_tac: thm -> thm -> tactic
     1.6    val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic
     1.7 -  val mk_set_natural_tac: thm -> thm -> tactic
     1.8 +  val mk_set_map_tac: thm -> thm -> tactic
     1.9    val mk_set_rv_Lev_tac: int -> cterm option list -> thm list -> thm list -> thm list -> thm list ->
    1.10      thm list list -> thm list list -> tactic
    1.11    val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list ->
    1.12 @@ -230,38 +230,38 @@
    1.13      EVERY' (replicate ((n + 1) * n) (Goal.assume_rule_tac ctxt)), rtac impI,
    1.14      REPEAT_DETERM o eresolve_tac [allE, conjE], atac])) hset_defs) 1
    1.15  
    1.16 -fun mk_mor_hset_rec_tac m n cts j rec_0s rec_Sucs morEs set_naturalss coalg_setss =
    1.17 +fun mk_mor_hset_rec_tac m n cts j rec_0s rec_Sucs morEs set_mapss coalg_setss =
    1.18    EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
    1.19      REPEAT_DETERM o rtac allI,
    1.20      CONJ_WRAP' (fn thm => EVERY' (map rtac [impI, thm RS trans, thm RS sym])) rec_0s,
    1.21      REPEAT_DETERM o rtac allI,
    1.22      CONJ_WRAP'
    1.23 -      (fn (rec_Suc, (morE, ((passive_set_naturals, active_set_naturals), coalg_sets))) =>
    1.24 +      (fn (rec_Suc, (morE, ((passive_set_maps, active_set_maps), coalg_sets))) =>
    1.25          EVERY' [rtac impI, rtac (rec_Suc RS trans), rtac (rec_Suc RS trans RS sym),
    1.26            if m = 0 then K all_tac
    1.27            else EVERY' [rtac @{thm Un_cong}, rtac box_equals,
    1.28 -            rtac (nth passive_set_naturals (j - 1) RS sym),
    1.29 +            rtac (nth passive_set_maps (j - 1) RS sym),
    1.30              rtac trans_fun_cong_image_id_id_apply, etac (morE RS arg_cong), atac],
    1.31            CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
    1.32 -            (fn (i, (set_natural, coalg_set)) =>
    1.33 +            (fn (i, (set_map, coalg_set)) =>
    1.34                EVERY' [rtac sym, rtac trans, rtac (refl RSN (2, @{thm UN_cong})),
    1.35 -                etac (morE RS sym RS arg_cong RS trans), atac, rtac set_natural,
    1.36 +                etac (morE RS sym RS arg_cong RS trans), atac, rtac set_map,
    1.37                  rtac (@{thm UN_simps(10)} RS trans), rtac (refl RS @{thm UN_cong}),
    1.38                  ftac coalg_set, atac, dtac set_mp, atac, rtac mp, rtac (mk_conjunctN n i),
    1.39                  REPEAT_DETERM o etac allE, atac, atac])
    1.40 -            (rev ((1 upto n) ~~ (active_set_naturals ~~ coalg_sets)))])
    1.41 -      (rec_Sucs ~~ (morEs ~~ (map (chop m) set_naturalss ~~ map (drop m) coalg_setss)))] 1;
    1.42 +            (rev ((1 upto n) ~~ (active_set_maps ~~ coalg_sets)))])
    1.43 +      (rec_Sucs ~~ (morEs ~~ (map (chop m) set_mapss ~~ map (drop m) coalg_setss)))] 1;
    1.44  
    1.45  fun mk_mor_hset_tac hset_def mor_hset_rec =
    1.46    EVERY' [rtac (hset_def RS trans), rtac (refl RS @{thm UN_cong} RS trans), etac mor_hset_rec,
    1.47      atac, atac, rtac (hset_def RS sym)] 1
    1.48  
    1.49 -fun mk_bis_srel_tac m bis_def srel_O_Grs map_comps map_cong0s set_naturalss =
    1.50 +fun mk_bis_srel_tac m bis_def srel_O_Grs map_comps map_cong0s set_mapss =
    1.51    let
    1.52      val n = length srel_O_Grs;
    1.53 -    val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_naturalss ~~ srel_O_Grs);
    1.54 +    val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_mapss ~~ srel_O_Grs);
    1.55  
    1.56 -    fun mk_if_tac ((((i, map_comp), map_cong0), set_naturals), srel_O_Gr) =
    1.57 +    fun mk_if_tac ((((i, map_comp), map_cong0), set_maps), srel_O_Gr) =
    1.58        EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i),
    1.59          etac allE, etac allE, etac impE, atac, etac bexE, etac conjE,
    1.60          rtac (srel_O_Gr RS equalityD2 RS set_mp),
    1.61 @@ -275,12 +275,12 @@
    1.62                  etac @{thm image_mono}, rtac @{thm image_subsetI}, etac @{thm Id_onI}]
    1.63                else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
    1.64                  rtac trans_fun_cong_image_id_id_apply, atac])
    1.65 -            (1 upto (m + n) ~~ set_naturals),
    1.66 +            (1 upto (m + n) ~~ set_maps),
    1.67              rtac trans, rtac trans, rtac map_comp, rtac map_cong0, REPEAT_DETERM_N m o rtac thm,
    1.68              REPEAT_DETERM_N n o rtac (@{thm o_id} RS fun_cong), atac])
    1.69            @{thms fst_diag_id snd_diag_id})];
    1.70  
    1.71 -    fun mk_only_if_tac ((((i, map_comp), map_cong0), set_naturals), srel_O_Gr) =
    1.72 +    fun mk_only_if_tac ((((i, map_comp), map_cong0), set_maps), srel_O_Gr) =
    1.73        EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI,
    1.74          etac allE, etac allE, etac impE, atac,
    1.75          dtac (srel_O_Gr RS equalityD1 RS set_mp),
    1.76 @@ -306,7 +306,7 @@
    1.77              rtac @{thm Id_on_fst}, etac set_mp, atac]
    1.78            else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm,
    1.79              rtac trans_fun_cong_image_id_id_apply, atac])
    1.80 -        (1 upto (m + n) ~~ set_naturals)];
    1.81 +        (1 upto (m + n) ~~ set_maps)];
    1.82    in
    1.83      EVERY' [rtac (bis_def RS trans),
    1.84        rtac iffI, etac conjE, etac conjI, CONJ_WRAP' mk_if_tac thms,
    1.85 @@ -401,7 +401,7 @@
    1.86      rtac incl_lsbis, rtac bis_O, rtac sbis_lsbis, rtac sbis_lsbis,
    1.87      etac @{thm relcompI}, atac] 1;
    1.88  
    1.89 -fun mk_coalgT_tac m defs strT_defs set_naturalss {context = ctxt, prems = _} =
    1.90 +fun mk_coalgT_tac m defs strT_defs set_mapss {context = ctxt, prems = _} =
    1.91    let
    1.92      val n = length strT_defs;
    1.93      val ks = 1 upto n;
    1.94 @@ -446,7 +446,7 @@
    1.95              rtac (@{thm append_Nil} RS sym RS arg_cong)])) ks]) (ks ~~ active_sets)];
    1.96    in
    1.97      unfold_thms_tac ctxt defs THEN
    1.98 -    CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_naturalss ~~ strT_defs)) 1
    1.99 +    CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_mapss ~~ strT_defs)) 1
   1.100    end;
   1.101  
   1.102  fun mk_card_of_carT_tac m isNode_defs sbd_sbd
   1.103 @@ -539,7 +539,7 @@
   1.104        atac] 1
   1.105    end;
   1.106  
   1.107 -fun mk_carT_set_tac n i carT_def strT_def isNode_def set_natural {context = ctxt, prems = _}=
   1.108 +fun mk_carT_set_tac n i carT_def strT_def isNode_def set_map {context = ctxt, prems = _}=
   1.109    EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
   1.110      REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
   1.111      dtac Pair_eqD,
   1.112 @@ -550,20 +550,20 @@
   1.113      rtac (strT_def RS arg_cong RS trans),
   1.114      etac (arg_cong RS trans),
   1.115      fo_rtac (mk_sum_casesN n i RS arg_cong RS trans) ctxt,
   1.116 -    rtac set_natural, rtac imageI, etac (equalityD2 RS set_mp), rtac CollectI,
   1.117 +    rtac set_map, rtac imageI, etac (equalityD2 RS set_mp), rtac CollectI,
   1.118      etac @{thm prefCl_Succ}, atac] 1;
   1.119  
   1.120  fun mk_strT_hset_tac n m j arg_cong_cTs cTs cts carT_defs strT_defs isNode_defs
   1.121 -  set_incl_hsets set_hset_incl_hsetss coalg_setss carT_setss coalgT set_naturalss =
   1.122 +  set_incl_hsets set_hset_incl_hsetss coalg_setss carT_setss coalgT set_mapss =
   1.123    let
   1.124 -    val set_naturals = map (fn xs => nth xs (j - 1)) set_naturalss;
   1.125 +    val set_maps = map (fn xs => nth xs (j - 1)) set_mapss;
   1.126      val ks = 1 upto n;
   1.127 -    fun base_tac (i, (cT, (strT_def, (set_incl_hset, set_natural)))) =
   1.128 +    fun base_tac (i, (cT, (strT_def, (set_incl_hset, set_map)))) =
   1.129        CONJ_WRAP' (fn (i', (carT_def, isNode_def)) => rtac impI THEN' etac conjE THEN'
   1.130          (if i = i'
   1.131          then EVERY' [rtac @{thm xt1(4)}, rtac set_incl_hset,
   1.132            rtac (strT_def RS arg_cong RS trans), etac (arg_cong RS trans),
   1.133 -          rtac (Thm.permute_prems 0 1 (set_natural RS box_equals)),
   1.134 +          rtac (Thm.permute_prems 0 1 (set_map RS box_equals)),
   1.135            rtac (trans OF [@{thm image_id} RS fun_cong, id_apply]),
   1.136            rtac (mk_sum_casesN n i RS (Drule.instantiate' [cT] [] arg_cong) RS sym)]
   1.137          else EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
   1.138 @@ -585,7 +585,7 @@
   1.139      EVERY' [rtac (Drule.instantiate' cTs cts @{thm list.induct}),
   1.140        REPEAT_DETERM o rtac allI, rtac impI,
   1.141        CONJ_WRAP' base_tac
   1.142 -        (ks ~~ (arg_cong_cTs ~~ (strT_defs ~~ (set_incl_hsets ~~ set_naturals)))),
   1.143 +        (ks ~~ (arg_cong_cTs ~~ (strT_defs ~~ (set_incl_hsets ~~ set_maps)))),
   1.144        REPEAT_DETERM o rtac allI, rtac impI,
   1.145        REPEAT_DETERM o eresolve_tac [allE, impE], etac @{thm ShiftI},
   1.146        CONJ_WRAP' (fn i => dtac (mk_conjunctN n i) THEN' rtac (mk_sumEN n) THEN'
   1.147 @@ -840,14 +840,14 @@
   1.148  
   1.149  fun mk_mor_beh_tac m mor_def mor_cong beh_defs carT_defs strT_defs isNode_defs
   1.150    to_sbd_injss from_to_sbdss Lev_0s Lev_Sucs rv_Nils rv_Conss Lev_sbds length_Levs length_Lev's
   1.151 -  prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_naturalss coalg_setss
   1.152 +  prefCl_Levs rv_lastss set_rv_Levsss set_Levsss set_image_Levsss set_mapss coalg_setss
   1.153    map_comp_ids map_cong0s map_arg_congs {context = ctxt, prems = _} =
   1.154    let
   1.155      val n = length beh_defs;
   1.156      val ks = 1 upto n;
   1.157  
   1.158      fun fbetw_tac (i, (carT_def, (isNode_def, (Lev_0, (rv_Nil, (Lev_sbd,
   1.159 -      ((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_naturals,
   1.160 +      ((length_Lev, length_Lev'), (prefCl_Lev, (rv_lasts, (set_maps,
   1.161          (coalg_sets, (set_rv_Levss, (set_Levss, set_image_Levss))))))))))))) =
   1.162        EVERY' [rtac ballI, rtac (carT_def RS equalityD2 RS set_mp),
   1.163          rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI, rtac refl, rtac conjI,
   1.164 @@ -863,29 +863,29 @@
   1.165          rtac conjI,
   1.166            rtac ballI, etac @{thm UN_E}, rtac conjI,
   1.167            if n = 1 then K all_tac else rtac (mk_sumEN n),
   1.168 -          EVERY' (map6 (fn i => fn isNode_def => fn set_naturals =>
   1.169 +          EVERY' (map6 (fn i => fn isNode_def => fn set_maps =>
   1.170              fn set_rv_Levs => fn set_Levs => fn set_image_Levs =>
   1.171              EVERY' [rtac (mk_disjIN n i), rtac (isNode_def RS ssubst),
   1.172                rtac exI, rtac conjI,
   1.173                (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
   1.174                else rtac (@{thm if_P} RS arg_cong RS trans) THEN' etac length_Lev' THEN'
   1.175                  etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
   1.176 -              EVERY' (map2 (fn set_natural => fn set_rv_Lev =>
   1.177 -                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans),
   1.178 +              EVERY' (map2 (fn set_map => fn set_rv_Lev =>
   1.179 +                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map RS trans),
   1.180                    rtac trans_fun_cong_image_id_id_apply,
   1.181                    etac set_rv_Lev, TRY o atac, etac conjI, atac])
   1.182 -              (take m set_naturals) set_rv_Levs),
   1.183 -              CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) =>
   1.184 -                EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI},
   1.185 +              (take m set_maps) set_rv_Levs),
   1.186 +              CONJ_WRAP' (fn (set_map, (set_Lev, set_image_Lev)) =>
   1.187 +                EVERY' [rtac (set_map RS trans), rtac equalityI, rtac @{thm image_subsetI},
   1.188                    rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
   1.189                    if n = 1 then rtac refl else atac, atac, rtac subsetI,
   1.190                    REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
   1.191                    rtac set_image_Lev, atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev',
   1.192                    etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
   1.193                    if n = 1 then rtac refl else atac])
   1.194 -              (drop m set_naturals ~~ (set_Levs ~~ set_image_Levs))])
   1.195 -          ks isNode_defs set_naturalss set_rv_Levss set_Levss set_image_Levss),
   1.196 -          CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_naturals,
   1.197 +              (drop m set_maps ~~ (set_Levs ~~ set_image_Levs))])
   1.198 +          ks isNode_defs set_mapss set_rv_Levss set_Levss set_image_Levss),
   1.199 +          CONJ_WRAP' (fn (i, (rv_last, (isNode_def, (set_maps,
   1.200              (set_rv_Levs, (set_Levs, set_image_Levs)))))) =>
   1.201              EVERY' [rtac ballI,
   1.202                REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
   1.203 @@ -894,13 +894,13 @@
   1.204                (if n = 1 then rtac @{thm if_P} THEN' etac length_Lev'
   1.205                else rtac (@{thm if_P} RS trans) THEN' etac length_Lev' THEN'
   1.206                  etac (sum_case_weak_cong RS trans) THEN' rtac (mk_sum_casesN n i)),
   1.207 -              EVERY' (map2 (fn set_natural => fn set_rv_Lev =>
   1.208 -                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans),
   1.209 +              EVERY' (map2 (fn set_map => fn set_rv_Lev =>
   1.210 +                EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map RS trans),
   1.211                    rtac trans_fun_cong_image_id_id_apply,
   1.212                    etac set_rv_Lev, TRY o atac, etac conjI, atac])
   1.213 -              (take m set_naturals) set_rv_Levs),
   1.214 -              CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) =>
   1.215 -                EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI},
   1.216 +              (take m set_maps) set_rv_Levs),
   1.217 +              CONJ_WRAP' (fn (set_map, (set_Lev, set_image_Lev)) =>
   1.218 +                EVERY' [rtac (set_map RS trans), rtac equalityI, rtac @{thm image_subsetI},
   1.219                    rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
   1.220                    if n = 1 then rtac refl else atac, atac, rtac subsetI,
   1.221                    REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
   1.222 @@ -909,8 +909,8 @@
   1.223                    atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev',
   1.224                    etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
   1.225                    if n = 1 then rtac refl else atac])
   1.226 -              (drop m set_naturals ~~ (set_Levs ~~ set_image_Levs))])
   1.227 -          (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_naturalss ~~
   1.228 +              (drop m set_maps ~~ (set_Levs ~~ set_image_Levs))])
   1.229 +          (ks ~~ (rv_lasts ~~ (isNode_defs ~~ (set_mapss ~~
   1.230              (set_rv_Levss ~~ (set_Levss ~~ set_image_Levss)))))),
   1.231          (**)
   1.232            rtac allI, rtac impI, rtac @{thm if_not_P}, rtac notI,
   1.233 @@ -921,12 +921,12 @@
   1.234            CONVERSION (Conv.top_conv
   1.235              (K (Conv.try_conv (Conv.rewr_conv (rv_Nil RS eq_reflection)))) ctxt),
   1.236            if n = 1 then rtac refl else rtac (mk_sum_casesN n i),
   1.237 -          EVERY' (map2 (fn set_natural => fn coalg_set =>
   1.238 -            EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_natural RS trans),
   1.239 +          EVERY' (map2 (fn set_map => fn coalg_set =>
   1.240 +            EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac (set_map RS trans),
   1.241                rtac trans_fun_cong_image_id_id_apply, etac coalg_set, atac])
   1.242 -            (take m set_naturals) (take m coalg_sets)),
   1.243 -          CONJ_WRAP' (fn (set_natural, (set_Lev, set_image_Lev)) =>
   1.244 -            EVERY' [rtac (set_natural RS trans), rtac equalityI, rtac @{thm image_subsetI},
   1.245 +            (take m set_maps) (take m coalg_sets)),
   1.246 +          CONJ_WRAP' (fn (set_map, (set_Lev, set_image_Lev)) =>
   1.247 +            EVERY' [rtac (set_map RS trans), rtac equalityI, rtac @{thm image_subsetI},
   1.248                rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, rtac set_Lev,
   1.249                rtac (Lev_0 RS equalityD2 RS set_mp), rtac @{thm singletonI}, rtac rv_Nil,
   1.250                atac, rtac subsetI,
   1.251 @@ -936,7 +936,7 @@
   1.252                etac @{thm set_mp[OF equalityD1[OF arg_cong[OF
   1.253                  trans[OF length_append_singleton arg_cong[of _ _ Suc, OF list.size(3)]]]]]},
   1.254                rtac rv_Nil])
   1.255 -          (drop m set_naturals ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))];
   1.256 +          (drop m set_maps ~~ (nth set_Levss (i - 1) ~~ nth set_image_Levss (i - 1)))];
   1.257  
   1.258      fun mor_tac (i, (strT_def, (((Lev_0, Lev_Suc), (rv_Nil, rv_Cons)),
   1.259        ((map_comp_id, (map_cong0, map_arg_cong)), (length_Lev', (from_to_sbds, to_sbd_injs)))))) =
   1.260 @@ -997,7 +997,7 @@
   1.261      CONJ_WRAP' fbetw_tac
   1.262        (ks ~~ (carT_defs ~~ (isNode_defs ~~ (Lev_0s ~~ (rv_Nils ~~ (Lev_sbds ~~
   1.263          ((length_Levs ~~ length_Lev's) ~~ (prefCl_Levs ~~ (rv_lastss ~~
   1.264 -          (set_naturalss ~~ (coalg_setss ~~
   1.265 +          (set_mapss ~~ (coalg_setss ~~
   1.266              (set_rv_Levsss ~~ (set_Levsss ~~ set_image_Levsss))))))))))))) THEN'
   1.267      CONJ_WRAP' mor_tac
   1.268        (ks ~~ (strT_defs ~~ (((Lev_0s ~~ Lev_Sucs) ~~ (rv_Nils ~~ rv_Conss)) ~~
   1.269 @@ -1015,22 +1015,22 @@
   1.270      equiv_LSBISs), rtac sym, rtac (o_apply RS trans),
   1.271      etac (sym RS arg_cong RS trans), rtac map_comp_id] 1;
   1.272  
   1.273 -fun mk_coalg_final_tac m coalg_def congruent_str_finals equiv_LSBISs set_naturalss coalgT_setss =
   1.274 +fun mk_coalg_final_tac m coalg_def congruent_str_finals equiv_LSBISs set_mapss coalgT_setss =
   1.275    EVERY' [stac coalg_def,
   1.276 -    CONJ_WRAP' (fn ((set_naturals, coalgT_sets), (equiv_LSBIS, congruent_str_final)) =>
   1.277 +    CONJ_WRAP' (fn ((set_maps, coalgT_sets), (equiv_LSBIS, congruent_str_final)) =>
   1.278        EVERY' [rtac @{thm univ_preserves}, rtac equiv_LSBIS, rtac congruent_str_final,
   1.279          rtac ballI, rtac @{thm ssubst_mem}, rtac o_apply, rtac CollectI,
   1.280 -        EVERY' (map2 (fn set_natural => fn coalgT_set =>
   1.281 -          EVERY' [rtac conjI, rtac (set_natural RS ord_eq_le_trans),
   1.282 +        EVERY' (map2 (fn set_map => fn coalgT_set =>
   1.283 +          EVERY' [rtac conjI, rtac (set_map RS ord_eq_le_trans),
   1.284              rtac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
   1.285              etac coalgT_set])
   1.286 -        (take m set_naturals) (take m coalgT_sets)),
   1.287 -        CONJ_WRAP' (fn (equiv_LSBIS, (set_natural, coalgT_set)) =>
   1.288 -          EVERY' [rtac (set_natural RS ord_eq_le_trans),
   1.289 +        (take m set_maps) (take m coalgT_sets)),
   1.290 +        CONJ_WRAP' (fn (equiv_LSBIS, (set_map, coalgT_set)) =>
   1.291 +          EVERY' [rtac (set_map RS ord_eq_le_trans),
   1.292              rtac @{thm image_subsetI}, rtac ssubst, rtac @{thm proj_in_iff},
   1.293              rtac equiv_LSBIS, etac set_rev_mp, etac coalgT_set])
   1.294 -        (equiv_LSBISs ~~ drop m (set_naturals ~~ coalgT_sets))])
   1.295 -    ((set_naturalss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1;
   1.296 +        (equiv_LSBISs ~~ drop m (set_maps ~~ coalgT_sets))])
   1.297 +    ((set_mapss ~~ coalgT_setss) ~~ (equiv_LSBISs ~~ congruent_str_finals))] 1;
   1.298  
   1.299  fun mk_mor_T_final_tac mor_def congruent_str_finals equiv_LSBISs =
   1.300    EVERY' [stac mor_def, rtac conjI,
   1.301 @@ -1225,7 +1225,7 @@
   1.302          replicate n (@{thm o_id} RS fun_cong))))
   1.303      maps map_comps map_cong0s)] 1;
   1.304  
   1.305 -fun mk_mcong_tac m coinduct_tac map_comp's dtor_maps map_cong0s set_naturalss set_hsetss
   1.306 +fun mk_mcong_tac m coinduct_tac map_comp's dtor_maps map_cong0s set_mapss set_hsetss
   1.307    set_hset_hsetsss =
   1.308    let
   1.309      val n = length map_comp's;
   1.310 @@ -1233,7 +1233,7 @@
   1.311    in
   1.312      EVERY' ([rtac rev_mp,
   1.313        coinduct_tac] @
   1.314 -      maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong0), set_naturals), set_hsets),
   1.315 +      maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong0), set_maps), set_hsets),
   1.316          set_hset_hsetss) =>
   1.317          [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, rtac conjI, rtac conjI,
   1.318           rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
   1.319 @@ -1244,16 +1244,16 @@
   1.320             [rtac o_apply_trans_sym, rtac (id_apply RS trans), etac CollectE,
   1.321             REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets),
   1.322           REPEAT_DETERM_N n o rtac snd_convol_fun_cong_sym,
   1.323 -         CONJ_WRAP' (fn (set_natural, set_hset_hsets) =>
   1.324 +         CONJ_WRAP' (fn (set_map, set_hset_hsets) =>
   1.325             EVERY' [REPEAT_DETERM o rtac allI, rtac impI, rtac @{thm image_convolD},
   1.326 -             etac set_rev_mp, rtac ord_eq_le_trans, rtac set_natural,
   1.327 +             etac set_rev_mp, rtac ord_eq_le_trans, rtac set_map,
   1.328               rtac @{thm image_mono}, rtac subsetI, rtac CollectI, etac CollectE,
   1.329               REPEAT_DETERM o etac conjE,
   1.330               CONJ_WRAP' (fn set_hset_hset =>
   1.331                 EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets])
   1.332 -           (drop m set_naturals ~~ set_hset_hsetss)])
   1.333 +           (drop m set_maps ~~ set_hset_hsetss)])
   1.334          (map (fn th => th RS trans) map_comp's ~~ map (fn th => th RS trans) dtor_maps ~~
   1.335 -          map_cong0s ~~ set_naturalss ~~ set_hsetss ~~ set_hset_hsetsss) @
   1.336 +          map_cong0s ~~ set_mapss ~~ set_hsetss ~~ set_hset_hsetsss) @
   1.337        [rtac impI,
   1.338         CONJ_WRAP' (fn k =>
   1.339           EVERY' [rtac impI, dtac (mk_conjunctN n k), etac mp, rtac exI, rtac conjI, etac CollectI,
   1.340 @@ -1265,7 +1265,7 @@
   1.341    unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
   1.342    ALLGOALS (etac sym);
   1.343  
   1.344 -fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_naturalss
   1.345 +fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_mapss
   1.346    {context = ctxt, prems = _} =
   1.347    let
   1.348      val n = length dtor_maps;
   1.349 @@ -1281,10 +1281,10 @@
   1.350          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
   1.351            (fn i => EVERY' [rtac @{thm UN_cong[OF refl]},
   1.352              REPEAT_DETERM o etac allE, etac (mk_conjunctN n i)]) (n downto 1)])
   1.353 -      (rec_Sucs ~~ (dtor_maps ~~ set_naturalss))] 1
   1.354 +      (rec_Sucs ~~ (dtor_maps ~~ set_mapss))] 1
   1.355    end;
   1.356  
   1.357 -fun mk_set_natural_tac hset_def col_natural =
   1.358 +fun mk_set_map_tac hset_def col_natural =
   1.359    EVERY' (map rtac [ext, (o_apply RS trans), (hset_def RS trans), sym,
   1.360      (o_apply RS trans), (@{thm image_cong} OF [hset_def, refl] RS trans),
   1.361      (@{thm image_UN} RS trans), (refl RS @{thm UN_cong}), col_natural]) 1;
   1.362 @@ -1370,10 +1370,10 @@
   1.363        REPEAT_DETERM o eresolve_tac [CollectE, conjE], etac map_eq]
   1.364    end;
   1.365  
   1.366 -fun mk_coalg_thePull_tac m coalg_def map_wpulls set_naturalss pickWP_assms_tacs
   1.367 +fun mk_coalg_thePull_tac m coalg_def map_wpulls set_mapss pickWP_assms_tacs
   1.368    {context = ctxt, prems = _} =
   1.369    unfold_thms_tac ctxt [coalg_def] THEN
   1.370 -  CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_naturals)) =>
   1.371 +  CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_maps)) =>
   1.372      EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
   1.373        REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
   1.374        hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
   1.375 @@ -1383,11 +1383,11 @@
   1.376        REPEAT_DETERM o eresolve_tac [CollectE, conjE],
   1.377        rtac CollectI,
   1.378        REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV),
   1.379 -      CONJ_WRAP' (fn set_natural =>
   1.380 -        EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_natural,
   1.381 +      CONJ_WRAP' (fn set_map =>
   1.382 +        EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_map,
   1.383            rtac trans_fun_cong_image_id_id_apply, atac])
   1.384 -      (drop m set_naturals)])
   1.385 -  (map_wpulls ~~ (pickWP_assms_tacs ~~ set_naturalss)) 1;
   1.386 +      (drop m set_maps)])
   1.387 +  (map_wpulls ~~ (pickWP_assms_tacs ~~ set_mapss)) 1;
   1.388  
   1.389  fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comps pickWP_assms_tacs
   1.390    {context = ctxt, prems = _: thm list} =
   1.391 @@ -1422,7 +1422,7 @@
   1.392        rtac refl])
   1.393    (unfolds ~~ map_comps) 1;
   1.394  
   1.395 -fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_naturalss map_wpulls pickWP_assms_tacs
   1.396 +fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_mapss map_wpulls pickWP_assms_tacs
   1.397    {context = ctxt, prems = _} =
   1.398    let
   1.399      val n = length rec_0s;
   1.400 @@ -1433,7 +1433,7 @@
   1.401        CONJ_WRAP' (fn thm => EVERY'
   1.402          [rtac impI, rtac ord_eq_le_trans, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,
   1.403        REPEAT_DETERM o rtac allI,
   1.404 -      CONJ_WRAP' (fn (rec_Suc, ((unfold, set_naturals), (map_wpull, pickWP_assms_tac))) =>
   1.405 +      CONJ_WRAP' (fn (rec_Suc, ((unfold, set_maps), (map_wpull, pickWP_assms_tac))) =>
   1.406          EVERY' [rtac impI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
   1.407            REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
   1.408            hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
   1.409 @@ -1442,16 +1442,16 @@
   1.410            rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
   1.411            rtac ord_eq_le_trans, rtac rec_Suc,
   1.412            rtac @{thm Un_least},
   1.413 -          SELECT_GOAL (unfold_thms_tac ctxt [unfold, nth set_naturals (j - 1),
   1.414 +          SELECT_GOAL (unfold_thms_tac ctxt [unfold, nth set_maps (j - 1),
   1.415              @{thm prod.cases}]),
   1.416            etac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
   1.417 -          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_natural) =>
   1.418 +          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_map) =>
   1.419              EVERY' [rtac @{thm UN_least},
   1.420 -              SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_natural, @{thm prod.cases}]),
   1.421 +              SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_map, @{thm prod.cases}]),
   1.422                etac imageE, hyp_subst_tac, REPEAT_DETERM o etac allE,
   1.423                dtac (mk_conjunctN n i), etac mp, etac set_mp, atac])
   1.424 -          (ks ~~ rev (drop m set_naturals))])
   1.425 -      (rec_Sucs ~~ ((unfolds ~~ set_naturalss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
   1.426 +          (ks ~~ rev (drop m set_maps))])
   1.427 +      (rec_Sucs ~~ ((unfolds ~~ set_mapss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
   1.428    end;
   1.429  
   1.430  fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick
   1.431 @@ -1500,26 +1500,26 @@
   1.432      FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
   1.433  
   1.434  fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets dtor_inject dtor_ctor
   1.435 -  set_naturals dtor_set_incls dtor_set_set_inclss =
   1.436 +  set_maps dtor_set_incls dtor_set_set_inclss =
   1.437    let
   1.438      val m = length dtor_set_incls;
   1.439      val n = length dtor_set_set_inclss;
   1.440 -    val (passive_set_naturals, active_set_naturals) = chop m set_naturals;
   1.441 +    val (passive_set_maps, active_set_maps) = chop m set_maps;
   1.442      val in_Jsrel = nth in_Jsrels (i - 1);
   1.443      val if_tac =
   1.444        EVERY' [dtac (in_Jsrel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
   1.445          rtac (in_srel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
   1.446 -        EVERY' (map2 (fn set_natural => fn set_incl =>
   1.447 -          EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_natural,
   1.448 +        EVERY' (map2 (fn set_map => fn set_incl =>
   1.449 +          EVERY' [rtac conjI, rtac ord_eq_le_trans, rtac set_map,
   1.450              rtac ord_eq_le_trans, rtac trans_fun_cong_image_id_id_apply,
   1.451              etac (set_incl RS @{thm subset_trans})])
   1.452 -        passive_set_naturals dtor_set_incls),
   1.453 -        CONJ_WRAP' (fn (in_Jsrel, (set_natural, dtor_set_set_incls)) =>
   1.454 -          EVERY' [rtac ord_eq_le_trans, rtac set_natural, rtac @{thm image_subsetI},
   1.455 +        passive_set_maps dtor_set_incls),
   1.456 +        CONJ_WRAP' (fn (in_Jsrel, (set_map, dtor_set_set_incls)) =>
   1.457 +          EVERY' [rtac ord_eq_le_trans, rtac set_map, rtac @{thm image_subsetI},
   1.458              rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
   1.459              CONJ_WRAP' (fn thm => etac (thm RS @{thm subset_trans}) THEN' atac) dtor_set_set_incls,
   1.460              rtac conjI, rtac refl, rtac refl])
   1.461 -        (in_Jsrels ~~ (active_set_naturals ~~ dtor_set_set_inclss)),
   1.462 +        (in_Jsrels ~~ (active_set_maps ~~ dtor_set_set_inclss)),
   1.463          CONJ_WRAP' (fn conv =>
   1.464            EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
   1.465            REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
   1.466 @@ -1529,21 +1529,21 @@
   1.467      val only_if_tac =
   1.468        EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
   1.469          rtac (in_Jsrel RS iffD2), rtac exI, rtac conjI, rtac CollectI,
   1.470 -        CONJ_WRAP' (fn (dtor_set, passive_set_natural) =>
   1.471 +        CONJ_WRAP' (fn (dtor_set, passive_set_map) =>
   1.472            EVERY' [rtac ord_eq_le_trans, rtac dtor_set, rtac @{thm Un_least},
   1.473 -            rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_natural,
   1.474 +            rtac ord_eq_le_trans, rtac box_equals, rtac passive_set_map,
   1.475              rtac (dtor_ctor RS sym RS arg_cong), rtac trans_fun_cong_image_id_id_apply, atac,
   1.476              CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
   1.477 -              (fn (active_set_natural, in_Jsrel) => EVERY' [rtac ord_eq_le_trans,
   1.478 +              (fn (active_set_map, in_Jsrel) => EVERY' [rtac ord_eq_le_trans,
   1.479                  rtac @{thm UN_cong[OF _ refl]}, rtac @{thm box_equals[OF _ _ refl]},
   1.480 -                rtac active_set_natural, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least},
   1.481 +                rtac active_set_map, rtac (dtor_ctor RS sym RS arg_cong), rtac @{thm UN_least},
   1.482                  dtac set_rev_mp, etac @{thm image_mono}, etac imageE,
   1.483                  dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jsrel RS iffD1),
   1.484                  dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
   1.485                  dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
   1.486                  hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
   1.487 -            (rev (active_set_naturals ~~ in_Jsrels))])
   1.488 -        (dtor_sets ~~ passive_set_naturals),
   1.489 +            (rev (active_set_maps ~~ in_Jsrels))])
   1.490 +        (dtor_sets ~~ passive_set_maps),
   1.491          rtac conjI,
   1.492          REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map,
   1.493            rtac box_equals, rtac map_comp, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,