src/HOL/BNF/Tools/bnf_gfp_tactics.ML
changeset 51798 ad3a241def73
parent 51782 84e7225f5ab6
child 51850 106afdf5806c
     1.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sat Apr 27 11:37:50 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sat Apr 27 20:50:20 2013 +0200
     1.3 @@ -9,18 +9,21 @@
     1.4  
     1.5  signature BNF_GFP_TACTICS =
     1.6  sig
     1.7 -  val mk_Lev_sbd_tac: cterm option list -> thm list -> thm list -> thm list list -> tactic
     1.8 +  val mk_Lev_sbd_tac: Proof.context -> cterm option list -> thm list -> thm list ->
     1.9 +    thm list list -> tactic
    1.10    val mk_bd_card_order_tac: thm -> tactic
    1.11    val mk_bd_cinfinite_tac: thm -> tactic
    1.12    val mk_bis_Gr_tac: thm -> thm list -> thm list -> thm list -> thm list ->
    1.13      {prems: 'a, context: Proof.context} -> tactic
    1.14 -  val mk_bis_O_tac: int -> thm -> thm list -> thm list -> tactic
    1.15 +  val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic
    1.16    val mk_bis_Union_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
    1.17    val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic
    1.18 -  val mk_bis_srel_tac: int -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic
    1.19 +  val mk_bis_srel_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list ->
    1.20 +    thm list list -> tactic
    1.21    val mk_carT_set_tac: int -> int -> thm -> thm -> thm -> thm ->
    1.22      {prems: 'a, context: Proof.context} -> tactic
    1.23 -  val mk_card_of_carT_tac: int -> thm list -> thm -> thm -> thm -> thm -> thm -> thm list -> tactic
    1.24 +  val mk_card_of_carT_tac: Proof.context -> int -> thm list -> thm -> thm -> thm -> thm -> thm ->
    1.25 +    thm list -> tactic
    1.26    val mk_coalgT_tac: int -> thm list -> thm list -> thm list list ->
    1.27      {prems: 'a, context: Proof.context} -> tactic
    1.28    val mk_coalg_final_tac: int -> thm -> thm list -> thm list -> thm list list -> thm list list ->
    1.29 @@ -44,25 +47,25 @@
    1.30      thm -> thm -> tactic
    1.31    val mk_dtor_set_tac: int -> thm -> thm -> thm list -> tactic
    1.32    val mk_dtor_srel_coinduct_tac: 'a list -> thm -> thm -> tactic
    1.33 -  val mk_dtor_srel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm ->
    1.34 -    thm list -> thm list -> tactic
    1.35 -  val mk_dtor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
    1.36 -    thm list -> thm list -> thm list list -> tactic
    1.37 +  val mk_dtor_srel_strong_coinduct_tac: Proof.context -> int -> ctyp option list ->
    1.38 +    cterm option list -> thm -> thm list -> thm list -> tactic
    1.39 +  val mk_dtor_srel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
    1.40 +    thm -> thm -> thm list -> thm list -> thm list list -> tactic
    1.41    val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list ->
    1.42      {prems: 'a, context: Proof.context} -> tactic
    1.43    val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic
    1.44    val mk_hset_minimal_tac: int -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
    1.45    val mk_hset_rec_minimal_tac: int -> cterm option list -> thm list -> thm list ->
    1.46      {prems: 'a, context: Proof.context} -> tactic
    1.47 -  val mk_in_bd_tac: thm -> thm list -> thm -> thm -> thm -> thm -> thm list -> thm -> thm -> thm ->
    1.48 -    thm -> thm -> thm -> tactic
    1.49 +  val mk_in_bd_tac: Proof.context -> thm -> thm list -> thm -> thm -> thm -> thm -> thm list ->
    1.50 +    thm -> thm -> thm -> thm -> thm -> thm -> tactic
    1.51    val mk_incl_lsbis_tac: int -> int -> thm -> tactic
    1.52    val mk_isNode_hset_tac: int -> thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
    1.53    val mk_length_Lev'_tac: thm -> tactic
    1.54 -  val mk_length_Lev_tac: cterm option list -> thm list -> thm list -> tactic
    1.55 +  val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
    1.56    val mk_map_comp_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic
    1.57 -  val mk_mcong_tac: int -> (int -> tactic) -> thm list -> thm list -> thm list -> thm list list ->
    1.58 -    thm list list -> thm list list list -> tactic
    1.59 +  val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list ->
    1.60 +    thm list list -> thm list list -> thm list list list -> tactic
    1.61    val mk_map_id_tac: thm list -> thm -> thm -> tactic
    1.62    val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic
    1.63    val mk_dtor_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
    1.64 @@ -92,7 +95,7 @@
    1.65      {prems: 'a, context: Proof.context} -> tactic
    1.66    val mk_mor_unfold_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->
    1.67      thm list -> tactic
    1.68 -  val mk_prefCl_Lev_tac: cterm option list -> thm list -> thm list -> tactic
    1.69 +  val mk_prefCl_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
    1.70    val mk_pickWP_assms_tac: thm list -> thm list -> thm -> (int -> tactic)
    1.71    val mk_pick_col_tac: int -> int -> cterm option list -> thm list -> thm list -> thm list ->
    1.72      thm list list -> thm list -> (int -> tactic) list -> {prems: 'a, context: Proof.context} ->
    1.73 @@ -100,22 +103,22 @@
    1.74    val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
    1.75      thm list -> thm list -> thm -> thm list -> tactic
    1.76    val mk_rv_last_tac: ctyp option list -> cterm option list -> thm list -> thm list -> tactic
    1.77 -  val mk_sbis_lsbis_tac: thm list -> thm -> thm -> tactic
    1.78 -  val mk_set_Lev_tac: cterm option list -> thm list -> thm list -> thm list -> thm list ->
    1.79 -    thm list list -> tactic
    1.80 +  val mk_sbis_lsbis_tac: Proof.context -> thm list -> thm -> thm -> tactic
    1.81 +  val mk_set_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> thm list ->
    1.82 +    thm list -> thm list list -> tactic
    1.83    val mk_set_bd_tac: thm -> thm -> thm -> tactic
    1.84    val mk_set_hset_incl_hset_tac: int -> thm list -> thm -> int -> tactic
    1.85 -  val mk_set_image_Lev_tac: cterm option list -> thm list -> thm list -> thm list -> thm list ->
    1.86 -    thm list list -> thm list list -> tactic
    1.87 +  val mk_set_image_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list ->
    1.88 +    thm list -> thm list -> thm list list -> thm list list -> tactic
    1.89    val mk_set_incl_hin_tac: thm list -> tactic
    1.90    val mk_set_incl_hset_tac: thm -> thm -> tactic
    1.91    val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic
    1.92    val mk_set_map_tac: thm -> thm -> tactic
    1.93 -  val mk_set_rv_Lev_tac: int -> cterm option list -> thm list -> thm list -> thm list -> thm list ->
    1.94 -    thm list list -> thm list list -> tactic
    1.95 -  val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list ->
    1.96 -    cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list ->
    1.97 -    thm list list -> thm list list -> thm -> thm list list -> tactic
    1.98 +  val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
    1.99 +    thm list -> thm list -> thm list list -> thm list list -> tactic
   1.100 +  val mk_strT_hset_tac: Proof.context -> int -> int -> int -> ctyp option list ->
   1.101 +    ctyp option list -> cterm option list -> thm list -> thm list -> thm list -> thm list ->
   1.102 +    thm list list -> thm list list -> thm list list -> thm -> thm list list -> tactic
   1.103    val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
   1.104    val mk_unique_mor_tac: thm list -> thm -> tactic
   1.105    val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list ->
   1.106 @@ -256,7 +259,7 @@
   1.107    EVERY' [rtac (hset_def RS trans), rtac (refl RS @{thm UN_cong} RS trans), etac mor_hset_rec,
   1.108      atac, atac, rtac (hset_def RS sym)] 1
   1.109  
   1.110 -fun mk_bis_srel_tac m bis_def srel_O_Grs map_comps map_cong0s set_mapss =
   1.111 +fun mk_bis_srel_tac ctxt m bis_def srel_O_Grs map_comps map_cong0s set_mapss =
   1.112    let
   1.113      val n = length srel_O_Grs;
   1.114      val thms = ((1 upto n) ~~ map_comps ~~ map_cong0s ~~ set_mapss ~~ srel_O_Grs);
   1.115 @@ -288,7 +291,7 @@
   1.116          REPEAT_DETERM o eresolve_tac [@{thm GrE}, exE, conjE],
   1.117          REPEAT_DETERM o dtac Pair_eqD,
   1.118          REPEAT_DETERM o etac conjE,
   1.119 -        hyp_subst_tac,
   1.120 +        hyp_subst_tac ctxt,
   1.121          REPEAT_DETERM o eresolve_tac [CollectE, conjE],
   1.122          rtac bexI, rtac conjI, rtac trans, rtac map_comp, rtac trans, rtac map_cong0,
   1.123          REPEAT_DETERM_N m o rtac (@{thm id_o} RS fun_cong),
   1.124 @@ -327,7 +330,7 @@
   1.125          REPEAT_DETERM o etac allE,
   1.126          rtac @{thm converseI}, etac mp, etac @{thm converseD}]) (srel_congs ~~ srel_converses)] 1;
   1.127  
   1.128 -fun mk_bis_O_tac m bis_srel srel_congs srel_Os =
   1.129 +fun mk_bis_O_tac ctxt m bis_srel srel_congs srel_Os =
   1.130    EVERY' [stac bis_srel, REPEAT_DETERM o dtac (bis_srel RS iffD1),
   1.131      REPEAT_DETERM o etac conjE, rtac conjI,
   1.132      CONJ_WRAP' (K (EVERY' [etac @{thm relcomp_subset_Sigma}, atac])) srel_congs,
   1.133 @@ -339,7 +342,7 @@
   1.134          rtac srel_O,
   1.135          etac @{thm relcompE},
   1.136          REPEAT_DETERM o dtac Pair_eqD,
   1.137 -        etac conjE, hyp_subst_tac,
   1.138 +        etac conjE, hyp_subst_tac ctxt,
   1.139          REPEAT_DETERM o etac allE, rtac @{thm relcompI},
   1.140          etac mp, atac, etac mp, atac]) (srel_congs ~~ srel_Os)] 1;
   1.141  
   1.142 @@ -371,13 +374,13 @@
   1.143            atac]) (ks ~~ in_monos)] 1
   1.144    end;
   1.145  
   1.146 -fun mk_sbis_lsbis_tac lsbis_defs bis_Union bis_cong =
   1.147 +fun mk_sbis_lsbis_tac ctxt lsbis_defs bis_Union bis_cong =
   1.148    let
   1.149      val n = length lsbis_defs;
   1.150    in
   1.151      EVERY' [rtac (Thm.permute_prems 0 1 bis_cong), EVERY' (map rtac lsbis_defs),
   1.152        rtac bis_Union, rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE, exE],
   1.153 -      hyp_subst_tac, etac bis_cong, EVERY' (map (rtac o mk_nth_conv n) (1 upto n))] 1
   1.154 +      hyp_subst_tac ctxt, etac bis_cong, EVERY' (map (rtac o mk_nth_conv n) (1 upto n))] 1
   1.155    end;
   1.156  
   1.157  fun mk_incl_lsbis_tac n i lsbis_def =
   1.158 @@ -407,7 +410,7 @@
   1.159      val ks = 1 upto n;
   1.160      fun coalg_tac (i, ((passive_sets, active_sets), def)) =
   1.161        EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
   1.162 -        hyp_subst_tac, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
   1.163 +        hyp_subst_tac ctxt, rtac (def RS trans RS @{thm ssubst_mem}), etac (arg_cong RS trans),
   1.164          rtac (mk_sum_casesN n i), rtac CollectI,
   1.165          EVERY' (map (fn thm => EVERY' [rtac conjI, rtac (thm RS ord_eq_le_trans),
   1.166            etac ((trans OF [@{thm image_id} RS fun_cong, id_apply]) RS ord_eq_le_trans)])
   1.167 @@ -449,7 +452,7 @@
   1.168      CONJ_WRAP' coalg_tac (ks ~~ (map (chop m) set_mapss ~~ strT_defs)) 1
   1.169    end;
   1.170  
   1.171 -fun mk_card_of_carT_tac m isNode_defs sbd_sbd
   1.172 +fun mk_card_of_carT_tac ctxt m isNode_defs sbd_sbd
   1.173    sbd_card_order sbd_Card_order sbd_Cinfinite sbd_Cnotzero in_sbds =
   1.174    let
   1.175      val n = length isNode_defs;
   1.176 @@ -518,11 +521,11 @@
   1.177        if m = 0 then rtac @{thm Card_order_ctwo} else rtac @{thm Card_order_csum},
   1.178        rtac sbd_Cnotzero,
   1.179        rtac @{thm card_of_mono1}, rtac subsetI,
   1.180 -      REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm prod_caseE}], hyp_subst_tac,
   1.181 +      REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm prod_caseE}], hyp_subst_tac ctxt,
   1.182        rtac @{thm SigmaI}, rtac @{thm DiffI}, rtac set_mp, rtac equalityD2,
   1.183        rtac (@{thm cpow_def} RS arg_cong RS trans), rtac (@{thm Pow_def} RS arg_cong RS trans),
   1.184        rtac @{thm Field_card_of}, rtac CollectI, atac, rtac notI, etac @{thm singletonE},
   1.185 -      hyp_subst_tac, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp),
   1.186 +      hyp_subst_tac ctxt, etac @{thm emptyE}, rtac (@{thm Ffunc_def} RS equalityD2 RS set_mp),
   1.187        rtac CollectI, rtac conjI, rtac ballI, dtac bspec, etac thin_rl, atac, dtac conjunct1,
   1.188        CONJ_WRAP_GEN' (etac disjE) (fn (i, def) => EVERY'
   1.189          [rtac (mk_UnIN n i), dtac (def RS iffD1),
   1.190 @@ -538,7 +541,7 @@
   1.191    EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
   1.192      REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE],
   1.193      dtac Pair_eqD,
   1.194 -    etac conjE, hyp_subst_tac,
   1.195 +    etac conjE, hyp_subst_tac ctxt,
   1.196      dtac (isNode_def RS iffD1),
   1.197      REPEAT_DETERM o eresolve_tac [exE, conjE],
   1.198      rtac (equalityD2 RS set_mp),
   1.199 @@ -548,7 +551,7 @@
   1.200      rtac set_map, rtac imageI, etac (equalityD2 RS set_mp), rtac CollectI,
   1.201      etac @{thm prefCl_Succ}, atac] 1;
   1.202  
   1.203 -fun mk_strT_hset_tac n m j arg_cong_cTs cTs cts carT_defs strT_defs isNode_defs
   1.204 +fun mk_strT_hset_tac ctxt n m j arg_cong_cTs cTs cts carT_defs strT_defs isNode_defs
   1.205    set_incl_hsets set_hset_incl_hsetss coalg_setss carT_setss coalgT set_mapss =
   1.206    let
   1.207      val set_maps = map (fn xs => nth xs (j - 1)) set_mapss;
   1.208 @@ -564,7 +567,7 @@
   1.209          else EVERY' [dtac (carT_def RS equalityD1 RS set_mp),
   1.210            REPEAT_DETERM o eresolve_tac [CollectE, exE], etac conjE,
   1.211            dtac conjunct2, dtac Pair_eqD, etac conjE,
   1.212 -          hyp_subst_tac, dtac (isNode_def RS iffD1),
   1.213 +          hyp_subst_tac ctxt, dtac (isNode_def RS iffD1),
   1.214            REPEAT_DETERM o eresolve_tac [exE, conjE],
   1.215            rtac (mk_InN_not_InM i i' RS notE), etac (sym RS trans), atac]))
   1.216        (ks ~~ (carT_defs ~~ isNode_defs));
   1.217 @@ -601,7 +604,7 @@
   1.218          (strT_hsets @ (replicate n mp) ~~ (1 upto (m + n)))] 1)
   1.219    end;
   1.220  
   1.221 -fun mk_Lev_sbd_tac cts Lev_0s Lev_Sucs to_sbdss =
   1.222 +fun mk_Lev_sbd_tac ctxt cts Lev_0s Lev_Sucs to_sbdss =
   1.223    let
   1.224      val n = length Lev_0s;
   1.225      val ks = 1 upto n;
   1.226 @@ -615,7 +618,7 @@
   1.227          EVERY' [rtac ord_eq_le_trans, rtac Lev_Suc,
   1.228            CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least}))
   1.229              (fn (i, to_sbd) => EVERY' [rtac subsetI,
   1.230 -              REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
   1.231 +              REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
   1.232                rtac @{thm Cons_clists}, rtac (mk_InN_Field n i), etac to_sbd,
   1.233                etac set_rev_mp, REPEAT_DETERM o etac allE,
   1.234                etac (mk_conjunctN n i)])
   1.235 @@ -623,7 +626,7 @@
   1.236        (Lev_Sucs ~~ to_sbdss)] 1
   1.237    end;
   1.238  
   1.239 -fun mk_length_Lev_tac cts Lev_0s Lev_Sucs =
   1.240 +fun mk_length_Lev_tac ctxt cts Lev_0s Lev_Sucs =
   1.241    let
   1.242      val n = length Lev_0s;
   1.243      val ks = n downto 1;
   1.244 @@ -637,16 +640,17 @@
   1.245        CONJ_WRAP' (fn Lev_Suc =>
   1.246          EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
   1.247            CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
   1.248 -            (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
   1.249 -              rtac trans, rtac @{thm length_Cons}, rtac @{thm arg_cong[of _ _ Suc]},
   1.250 -              REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), etac mp, atac]) ks])
   1.251 +            (fn i =>
   1.252 +              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
   1.253 +                rtac trans, rtac @{thm length_Cons}, rtac @{thm arg_cong[of _ _ Suc]},
   1.254 +                REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i), etac mp, atac]) ks])
   1.255        Lev_Sucs] 1
   1.256    end;
   1.257  
   1.258  fun mk_length_Lev'_tac length_Lev =
   1.259    EVERY' [ftac length_Lev, etac ssubst, atac] 1;
   1.260  
   1.261 -fun mk_prefCl_Lev_tac cts Lev_0s Lev_Sucs =
   1.262 +fun mk_prefCl_Lev_tac ctxt cts Lev_0s Lev_Sucs =
   1.263    let
   1.264      val n = length Lev_0s;
   1.265      val ks = n downto 1;
   1.266 @@ -655,18 +659,21 @@
   1.267        REPEAT_DETERM o rtac allI,
   1.268        CONJ_WRAP' (fn Lev_0 =>
   1.269          EVERY' [rtac impI, etac conjE, dtac (Lev_0 RS equalityD1 RS set_mp),
   1.270 -          etac @{thm singletonE}, hyp_subst_tac, dtac @{thm prefixeq_Nil[THEN subst, of "%x. x"]},
   1.271 -          hyp_subst_tac, rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
   1.272 +          etac @{thm singletonE}, hyp_subst_tac ctxt,
   1.273 +          dtac @{thm prefixeq_Nil[THEN subst, of "%x. x"]},
   1.274 +          hyp_subst_tac ctxt,
   1.275 +          rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
   1.276            rtac Lev_0, rtac @{thm singletonI}]) Lev_0s,
   1.277        REPEAT_DETERM o rtac allI,
   1.278        CONJ_WRAP' (fn (Lev_0, Lev_Suc) =>
   1.279          EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
   1.280            CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
   1.281 -            (fn i => EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
   1.282 -              dtac @{thm prefixeq_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac,
   1.283 +            (fn i =>
   1.284 +              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
   1.285 +              dtac @{thm prefixeq_Cons[THEN subst, of "%x. x"]}, etac disjE, hyp_subst_tac ctxt,
   1.286                rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF list.size(3)]]]]},
   1.287                rtac Lev_0, rtac @{thm singletonI},
   1.288 -              REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac,
   1.289 +              REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt,
   1.290                rtac @{thm set_mp[OF equalityD2[OF trans[OF arg_cong[OF length_Cons]]]]},
   1.291                rtac Lev_Suc, rtac (mk_UnIN n i), rtac CollectI, REPEAT_DETERM o rtac exI, rtac conjI,
   1.292                rtac refl, etac conjI, REPEAT_DETERM o etac allE, dtac (mk_conjunctN n i),
   1.293 @@ -699,7 +706,7 @@
   1.294        ks)] 1
   1.295    end;
   1.296  
   1.297 -fun mk_set_rv_Lev_tac m cts Lev_0s Lev_Sucs rv_Nils rv_Conss coalg_setss from_to_sbdss =
   1.298 +fun mk_set_rv_Lev_tac ctxt m cts Lev_0s Lev_Sucs rv_Nils rv_Conss coalg_setss from_to_sbdss =
   1.299    let
   1.300      val n = length Lev_0s;
   1.301      val ks = 1 upto n;
   1.302 @@ -718,7 +725,7 @@
   1.303          EVERY' [rtac impI, etac conjE, dtac (Lev_Suc RS equalityD1 RS set_mp),
   1.304            CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
   1.305              (fn (i, (from_to_sbd, coalg_set)) =>
   1.306 -              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
   1.307 +              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
   1.308                rtac (rv_Cons RS arg_cong RS iffD2),
   1.309                rtac (mk_sum_casesN n i RS arg_cong RS trans RS iffD2),
   1.310                etac (from_to_sbd RS arg_cong), REPEAT_DETERM o etac allE,
   1.311 @@ -728,7 +735,7 @@
   1.312        ((Lev_Sucs ~~ rv_Conss) ~~ (from_to_sbdss ~~ coalg_setss))] 1
   1.313    end;
   1.314  
   1.315 -fun mk_set_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss =
   1.316 +fun mk_set_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss =
   1.317    let
   1.318      val n = length Lev_0s;
   1.319      val ks = 1 upto n;
   1.320 @@ -737,10 +744,10 @@
   1.321        REPEAT_DETERM o rtac allI,
   1.322        CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
   1.323          EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
   1.324 -          etac @{thm singletonE}, hyp_subst_tac,
   1.325 +          etac @{thm singletonE}, hyp_subst_tac ctxt,
   1.326            CONJ_WRAP' (fn i' => rtac impI THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'
   1.327              (if i = i'
   1.328 -            then EVERY' [dtac (mk_InN_inject n i), hyp_subst_tac,
   1.329 +            then EVERY' [dtac (mk_InN_inject n i), hyp_subst_tac ctxt,
   1.330                CONJ_WRAP' (fn (i'', Lev_0'') =>
   1.331                  EVERY' [rtac impI, rtac @{thm ssubst_mem[OF append_Nil]},
   1.332                    rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i''),
   1.333 @@ -756,7 +763,7 @@
   1.334          EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
   1.335            CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
   1.336              (fn (i, from_to_sbd) =>
   1.337 -              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
   1.338 +              EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
   1.339                  CONJ_WRAP' (fn i' => rtac impI THEN'
   1.340                    CONJ_WRAP' (fn i'' =>
   1.341                      EVERY' [rtac impI, rtac (Lev_Suc RS equalityD2 RS set_mp),
   1.342 @@ -774,7 +781,7 @@
   1.343        ((Lev_Sucs ~~ rv_Conss) ~~ from_to_sbdss)] 1
   1.344    end;
   1.345  
   1.346 -fun mk_set_image_Lev_tac cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss to_sbd_injss =
   1.347 +fun mk_set_image_Lev_tac ctxt cts Lev_0s Lev_Sucs rv_Nils rv_Conss from_to_sbdss to_sbd_injss =
   1.348    let
   1.349      val n = length Lev_0s;
   1.350      val ks = 1 upto n;
   1.351 @@ -783,18 +790,18 @@
   1.352        REPEAT_DETERM o rtac allI,
   1.353        CONJ_WRAP' (fn ((i, (Lev_0, Lev_Suc)), rv_Nil) =>
   1.354          EVERY' [rtac impI, dtac (Lev_0 RS equalityD1 RS set_mp),
   1.355 -          etac @{thm singletonE}, hyp_subst_tac,
   1.356 +          etac @{thm singletonE}, hyp_subst_tac ctxt,
   1.357            CONJ_WRAP' (fn i' => rtac impI THEN'
   1.358              CONJ_WRAP' (fn i'' => rtac impI  THEN' dtac (sym RS trans) THEN' rtac rv_Nil THEN'
   1.359                (if i = i''
   1.360                then EVERY' [dtac @{thm ssubst_mem[OF sym[OF append_Nil]]},
   1.361                  dtac (Lev_Suc RS equalityD1 RS set_mp), dtac (mk_InN_inject n i),
   1.362 -                hyp_subst_tac,
   1.363 +                hyp_subst_tac ctxt,
   1.364                  CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
   1.365                    (fn k => REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN'
   1.366                      dtac list_inject_iffD1 THEN' etac conjE THEN'
   1.367                      (if k = i'
   1.368 -                    then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac, etac imageI]
   1.369 +                    then EVERY' [dtac (mk_InN_inject n k), hyp_subst_tac ctxt, etac imageI]
   1.370                      else etac (mk_InN_not_InM i' k RS notE)))
   1.371                  (rev ks)]
   1.372                else etac (mk_InN_not_InM i'' i RS notE)))
   1.373 @@ -806,7 +813,7 @@
   1.374          EVERY' [rtac impI, dtac (Lev_Suc RS equalityD1 RS set_mp),
   1.375            CONJ_WRAP_GEN' (etac (Thm.permute_prems 1 1 UnE))
   1.376              (fn (i, (from_to_sbd, to_sbd_inj)) =>
   1.377 -              REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' hyp_subst_tac THEN'
   1.378 +              REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE] THEN' hyp_subst_tac ctxt THEN'
   1.379                CONJ_WRAP' (fn i' => rtac impI THEN'
   1.380                  dtac @{thm ssubst_mem[OF sym[OF append_Cons]]} THEN'
   1.381                  dtac (Lev_Suc RS equalityD1 RS set_mp) THEN'
   1.382 @@ -816,7 +823,7 @@
   1.383                    (if k = i
   1.384                    then EVERY' [dtac (mk_InN_inject n i),
   1.385                      dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
   1.386 -                    atac, atac, hyp_subst_tac] THEN'
   1.387 +                    atac, atac, hyp_subst_tac ctxt] THEN'
   1.388                      CONJ_WRAP' (fn i'' =>
   1.389                        EVERY' [rtac impI, dtac (sym RS trans),
   1.390                          rtac (rv_Cons RS trans), rtac (mk_sum_casesN n i RS arg_cong RS trans),
   1.391 @@ -875,7 +882,7 @@
   1.392                    rtac CollectI, rtac @{thm SuccI}, rtac @{thm UN_I}, rtac UNIV_I, etac set_Lev,
   1.393                    if n = 1 then rtac refl else atac, atac, rtac subsetI,
   1.394                    REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
   1.395 -                  rtac set_image_Lev, atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev',
   1.396 +                  rtac set_image_Lev, atac, dtac length_Lev, hyp_subst_tac ctxt, dtac length_Lev',
   1.397                    etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
   1.398                    if n = 1 then rtac refl else atac])
   1.399                (drop m set_maps ~~ (set_Levs ~~ set_image_Levs))])
   1.400 @@ -901,7 +908,7 @@
   1.401                    REPEAT_DETERM o eresolve_tac [CollectE, @{thm SuccE}, @{thm UN_E}],
   1.402                    REPEAT_DETERM_N 4 o etac thin_rl,
   1.403                    rtac set_image_Lev,
   1.404 -                  atac, dtac length_Lev, hyp_subst_tac, dtac length_Lev',
   1.405 +                  atac, dtac length_Lev, hyp_subst_tac ctxt, dtac length_Lev',
   1.406                    etac @{thm set_mp[OF equalityD1[OF arg_cong[OF length_append_singleton]]]},
   1.407                    if n = 1 then rtac refl else atac])
   1.408                (drop m set_maps ~~ (set_Levs ~~ set_image_Levs))])
   1.409 @@ -958,7 +965,7 @@
   1.410                  dtac list_inject_iffD1, etac conjE,
   1.411                  if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
   1.412                    dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
   1.413 -                  atac, atac, hyp_subst_tac, etac @{thm UN_I[OF UNIV_I]}]
   1.414 +                  atac, atac, hyp_subst_tac ctxt, etac @{thm UN_I[OF UNIV_I]}]
   1.415                  else etac (mk_InN_not_InM i' i'' RS notE)])
   1.416              (rev ks),
   1.417              rtac @{thm UN_least}, rtac subsetI, rtac CollectI, rtac @{thm UN_I[OF UNIV_I]},
   1.418 @@ -973,7 +980,7 @@
   1.419                  dtac list_inject_iffD1, etac conjE,
   1.420                  if i' = i'' then EVERY' [dtac (mk_InN_inject n i'),
   1.421                    dtac (Thm.permute_prems 0 2 (to_sbd_inj RS iffD1)),
   1.422 -                  atac, atac, hyp_subst_tac, atac]
   1.423 +                  atac, atac, hyp_subst_tac ctxt, atac]
   1.424                  else etac (mk_InN_not_InM i' i'' RS notE)])
   1.425              (rev ks),
   1.426              rtac (Lev_Suc RS equalityD2 RS set_mp), rtac (mk_UnIN n i'), rtac CollectI,
   1.427 @@ -1132,11 +1139,11 @@
   1.428      CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp,
   1.429        rtac CollectI, etac @{thm prod_caseI}])) ks] 1;
   1.430  
   1.431 -fun mk_dtor_srel_strong_coinduct_tac m cTs cts dtor_srel_coinduct srel_monos srel_Ids =
   1.432 +fun mk_dtor_srel_strong_coinduct_tac ctxt m cTs cts dtor_srel_coinduct srel_monos srel_Ids =
   1.433    EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_srel_coinduct),
   1.434      EVERY' (map2 (fn srel_mono => fn srel_Id =>
   1.435        EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], REPEAT_DETERM o etac allE,
   1.436 -        etac disjE, etac mp, atac, hyp_subst_tac, rtac (srel_mono RS set_mp),
   1.437 +        etac disjE, etac mp, atac, hyp_subst_tac ctxt, rtac (srel_mono RS set_mp),
   1.438          REPEAT_DETERM_N m o rtac @{thm subset_refl},
   1.439          REPEAT_DETERM_N (length srel_monos) o rtac @{thm Id_subset},
   1.440          rtac (srel_Id RS equalityD2 RS set_mp), rtac @{thm IdI}])
   1.441 @@ -1220,7 +1227,7 @@
   1.442          replicate n (@{thm o_id} RS fun_cong))))
   1.443      maps map_comps map_cong0s)] 1;
   1.444  
   1.445 -fun mk_mcong_tac m coinduct_tac map_comp's dtor_maps map_cong0s set_mapss set_hsetss
   1.446 +fun mk_mcong_tac ctxt m coinduct_tac map_comp's dtor_maps map_cong0s set_mapss set_hsetss
   1.447    set_hset_hsetsss =
   1.448    let
   1.449      val n = length map_comp's;
   1.450 @@ -1230,8 +1237,8 @@
   1.451        coinduct_tac] @
   1.452        maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong0), set_maps), set_hsets),
   1.453          set_hset_hsetss) =>
   1.454 -        [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, rtac conjI, rtac conjI,
   1.455 -         rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
   1.456 +        [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI, rtac conjI,
   1.457 +         rtac conjI, rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
   1.458           REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac id_apply),
   1.459           REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym,
   1.460           rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong0,
   1.461 @@ -1309,7 +1316,7 @@
   1.462      @{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite,
   1.463      ctrans, @{thm infinite_ordLeq_cexp}, sbd_Cinfinite, @{thm cexp_ordLeq_ccexp}]) 1;
   1.464  
   1.465 -fun mk_in_bd_tac isNode_hset isNode_hsets carT_def card_of_carT mor_image Rep_inverse mor_hsets
   1.466 +fun mk_in_bd_tac ctxt isNode_hset isNode_hsets carT_def card_of_carT mor_image Rep_inverse mor_hsets
   1.467    sbd_Cnotzero sbd_Card_order mor_Rep coalgT mor_T_final tcoalg =
   1.468    let
   1.469      val n = length isNode_hsets;
   1.470 @@ -1331,7 +1338,7 @@
   1.471        rtac set_rev_mp, rtac mor_image, rtac mor_Rep, rtac UNIV_I, rtac equalityD2,
   1.472        rtac @{thm proj_image},  rtac @{thm image_eqI}, atac,
   1.473        ftac (carT_def RS equalityD1 RS set_mp),
   1.474 -      REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
   1.475 +      REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
   1.476        rtac (carT_def RS equalityD2 RS set_mp), rtac CollectI, REPEAT_DETERM o rtac exI,
   1.477        rtac conjI, rtac refl, rtac conjI, etac conjI, etac conjI, etac conjI, rtac conjI,
   1.478        rtac ballI, dtac bspec, atac, REPEAT_DETERM o etac conjE, rtac conjI,
   1.479 @@ -1371,7 +1378,7 @@
   1.480    CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_maps)) =>
   1.481      EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
   1.482        REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
   1.483 -      hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
   1.484 +      hyp_subst_tac ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
   1.485        EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
   1.486        pickWP_assms_tac,
   1.487        SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}), rtac impI,
   1.488 @@ -1395,7 +1402,7 @@
   1.489        CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp)) =>
   1.490          EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
   1.491            REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
   1.492 -          hyp_subst_tac,
   1.493 +          hyp_subst_tac ctxt,
   1.494            SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}),
   1.495            rtac (map_comp RS trans),
   1.496            SELECT_GOAL (unfold_thms_tac ctxt (conv :: @{thms o_id id_o})),
   1.497 @@ -1412,7 +1419,7 @@
   1.498    CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) unfolds 1 THEN
   1.499    CONJ_WRAP' (fn (unfold, map_comp) =>
   1.500      EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
   1.501 -      hyp_subst_tac,
   1.502 +      hyp_subst_tac ctxt,
   1.503        SELECT_GOAL (unfold_thms_tac ctxt (unfold :: map_comp :: @{thms comp_def id_def})),
   1.504        rtac refl])
   1.505    (unfolds ~~ map_comps) 1;
   1.506 @@ -1431,7 +1438,7 @@
   1.507        CONJ_WRAP' (fn (rec_Suc, ((unfold, set_maps), (map_wpull, pickWP_assms_tac))) =>
   1.508          EVERY' [rtac impI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
   1.509            REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
   1.510 -          hyp_subst_tac, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
   1.511 +          hyp_subst_tac ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
   1.512            EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
   1.513            pickWP_assms_tac,
   1.514            rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
   1.515 @@ -1443,7 +1450,7 @@
   1.516            CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_map) =>
   1.517              EVERY' [rtac @{thm UN_least},
   1.518                SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_map, @{thm prod.cases}]),
   1.519 -              etac imageE, hyp_subst_tac, REPEAT_DETERM o etac allE,
   1.520 +              etac imageE, hyp_subst_tac ctxt, REPEAT_DETERM o etac allE,
   1.521                dtac (mk_conjunctN n i), etac mp, etac set_mp, atac])
   1.522            (ks ~~ rev (drop m set_maps))])
   1.523        (rec_Sucs ~~ ((unfolds ~~ set_mapss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
   1.524 @@ -1484,18 +1491,18 @@
   1.525          (eresolve_tac wit ORELSE'
   1.526          (dresolve_tac wit THEN'
   1.527            (etac FalseE ORELSE'
   1.528 -          EVERY' [hyp_subst_tac, dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
   1.529 +          EVERY' [hyp_subst_tac ctxt, dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
   1.530              K (unfold_thms_tac ctxt dtor_ctors), REPEAT_DETERM_N n o etac UnE]))))] 1);
   1.531  
   1.532  fun mk_coind_wit_tac induct unfolds set_nats wits {context = ctxt, prems = _} =
   1.533 -  rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac) THEN
   1.534 +  rtac induct 1 THEN ALLGOALS (TRY o rtac impI THEN' TRY o hyp_subst_tac ctxt) THEN
   1.535    unfold_thms_tac ctxt (unfolds @ set_nats @ @{thms image_id id_apply}) THEN
   1.536 -  ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac) THEN
   1.537 +  ALLGOALS (REPEAT_DETERM o etac imageE THEN' TRY o hyp_subst_tac ctxt) THEN
   1.538    ALLGOALS (TRY o
   1.539      FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
   1.540  
   1.541 -fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets dtor_inject dtor_ctor
   1.542 -  set_maps dtor_set_incls dtor_set_set_inclss =
   1.543 +fun mk_dtor_srel_tac ctxt in_Jsrels i in_srel map_comp map_cong0 dtor_map dtor_sets dtor_inject
   1.544 +    dtor_ctor set_maps dtor_set_incls dtor_set_set_inclss =
   1.545    let
   1.546      val m = length dtor_set_incls;
   1.547      val n = length dtor_set_set_inclss;
   1.548 @@ -1536,7 +1543,7 @@
   1.549                  dtac @{thm ssubst_mem[OF pair_collapse]}, dtac (in_Jsrel RS iffD1),
   1.550                  dtac @{thm someI_ex}, REPEAT_DETERM o etac conjE,
   1.551                  dtac (Thm.permute_prems 0 1 @{thm ssubst_mem}), atac,
   1.552 -                hyp_subst_tac, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
   1.553 +                hyp_subst_tac ctxt, REPEAT_DETERM o eresolve_tac [CollectE, conjE], atac])
   1.554              (rev (active_set_maps ~~ in_Jsrels))])
   1.555          (dtor_sets ~~ passive_set_maps),
   1.556          rtac conjI,