src/HOL/BNF/Tools/bnf_gfp_tactics.ML
changeset 49541 32fb6e4c7f4b
parent 49516 d4859efc1096
child 49542 b39354db8629
     1.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
     1.3 @@ -1220,7 +1220,7 @@
     1.4          replicate n (@{thm o_id} RS fun_cong))))
     1.5      maps map_comps map_congs)] 1;
     1.6  
     1.7 -fun mk_mcong_tac m coinduct_tac map_comp's map_simps map_congs set_naturalss set_hsetss
     1.8 +fun mk_mcong_tac m coinduct_tac map_comp's dtor_maps map_congs set_naturalss set_hsetss
     1.9    set_hset_hsetsss =
    1.10    let
    1.11      val n = length map_comp's;
    1.12 @@ -1228,13 +1228,13 @@
    1.13    in
    1.14      EVERY' ([rtac rev_mp,
    1.15        coinduct_tac] @
    1.16 -      maps (fn (((((map_comp'_trans, map_simps_trans), map_cong), set_naturals), set_hsets),
    1.17 +      maps (fn (((((map_comp'_trans, dtor_maps_trans), map_cong), set_naturals), set_hsets),
    1.18          set_hset_hsetss) =>
    1.19          [REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI, rtac conjI, rtac conjI,
    1.20 -         rtac map_comp'_trans, rtac sym, rtac map_simps_trans, rtac map_cong,
    1.21 +         rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong,
    1.22           REPEAT_DETERM_N m o (rtac o_apply_trans_sym THEN' rtac @{thm id_apply}),
    1.23           REPEAT_DETERM_N n o rtac fst_convol_fun_cong_sym,
    1.24 -         rtac map_comp'_trans, rtac sym, rtac map_simps_trans, rtac map_cong,
    1.25 +         rtac map_comp'_trans, rtac sym, rtac dtor_maps_trans, rtac map_cong,
    1.26           EVERY' (maps (fn set_hset =>
    1.27             [rtac o_apply_trans_sym, rtac (@{thm id_apply} RS trans), etac CollectE,
    1.28             REPEAT_DETERM o etac conjE, etac bspec, etac set_hset]) set_hsets),
    1.29 @@ -1247,7 +1247,7 @@
    1.30               CONJ_WRAP' (fn set_hset_hset =>
    1.31                 EVERY' [rtac ballI, etac bspec, etac set_hset_hset, atac]) set_hset_hsets])
    1.32             (drop m set_naturals ~~ set_hset_hsetss)])
    1.33 -        (map (fn th => th RS trans) map_comp's ~~ map (fn th => th RS trans) map_simps ~~
    1.34 +        (map (fn th => th RS trans) map_comp's ~~ map (fn th => th RS trans) dtor_maps ~~
    1.35            map_congs ~~ set_naturalss ~~ set_hsetss ~~ set_hset_hsetsss) @
    1.36        [rtac impI,
    1.37         CONJ_WRAP' (fn k =>
    1.38 @@ -1260,23 +1260,23 @@
    1.39    unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
    1.40    ALLGOALS (etac sym);
    1.41  
    1.42 -fun mk_col_natural_tac cts rec_0s rec_Sucs map_simps set_naturalss
    1.43 +fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_naturalss
    1.44    {context = ctxt, prems = _} =
    1.45    let
    1.46 -    val n = length map_simps;
    1.47 +    val n = length dtor_maps;
    1.48    in
    1.49      EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
    1.50        REPEAT_DETERM o rtac allI, SELECT_GOAL (unfold_thms_tac ctxt rec_0s),
    1.51        CONJ_WRAP' (K (rtac @{thm image_empty})) rec_0s,
    1.52        REPEAT_DETERM o rtac allI,
    1.53 -      CONJ_WRAP' (fn (rec_Suc, (map_simp, set_nats)) => EVERY'
    1.54 +      CONJ_WRAP' (fn (rec_Suc, (dtor_map, set_nats)) => EVERY'
    1.55          [SELECT_GOAL (unfold_thms_tac ctxt
    1.56 -          (rec_Suc :: map_simp :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
    1.57 +          (rec_Suc :: dtor_map :: set_nats @ @{thms image_Un image_UN UN_simps(10)})),
    1.58          rtac @{thm Un_cong}, rtac refl,
    1.59          CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_cong}))
    1.60            (fn i => EVERY' [rtac @{thm UN_cong[OF refl]},
    1.61              REPEAT_DETERM o etac allE, etac (mk_conjunctN n i)]) (n downto 1)])
    1.62 -      (rec_Sucs ~~ (map_simps ~~ set_naturalss))] 1
    1.63 +      (rec_Sucs ~~ (dtor_maps ~~ set_naturalss))] 1
    1.64    end;
    1.65  
    1.66  fun mk_set_natural_tac hset_def col_natural =
    1.67 @@ -1494,7 +1494,7 @@
    1.68    ALLGOALS (TRY o
    1.69      FIRST' [rtac TrueI, rtac refl, etac (refl RSN (2, mp)), dresolve_tac wits THEN' etac FalseE])
    1.70  
    1.71 -fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong map_simp set_simps dtor_inject dtor_ctor
    1.72 +fun mk_dtor_srel_tac in_Jsrels i in_srel map_comp map_cong dtor_map set_simps dtor_inject dtor_ctor
    1.73    set_naturals set_incls set_set_inclss =
    1.74    let
    1.75      val m = length set_incls;
    1.76 @@ -1519,7 +1519,7 @@
    1.77            EVERY' [rtac trans, rtac map_comp, rtac trans, rtac map_cong,
    1.78            REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
    1.79            REPEAT_DETERM_N n o EVERY' (map rtac [trans, o_apply, conv]),
    1.80 -          rtac trans, rtac sym, rtac map_simp, rtac (dtor_inject RS iffD2), atac])
    1.81 +          rtac trans, rtac sym, rtac dtor_map, rtac (dtor_inject RS iffD2), atac])
    1.82          @{thms fst_conv snd_conv}];
    1.83      val only_if_tac =
    1.84        EVERY' [dtac (in_srel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, conjE, CollectE],
    1.85 @@ -1540,7 +1540,7 @@
    1.86              (rev (active_set_naturals ~~ in_Jsrels))])
    1.87          (set_simps ~~ passive_set_naturals),
    1.88          rtac conjI,
    1.89 -        REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac map_simp,
    1.90 +        REPEAT_DETERM_N 2 o EVERY'[rtac (dtor_inject RS iffD1), rtac trans, rtac dtor_map,
    1.91            rtac box_equals, rtac map_comp, rtac (dtor_ctor RS sym RS arg_cong), rtac trans,
    1.92            rtac map_cong, REPEAT_DETERM_N m o rtac @{thm fun_cong[OF o_id]},
    1.93            EVERY' (map (fn in_Jsrel => EVERY' [rtac trans, rtac o_apply, dtac set_rev_mp, atac,