src/HOL/Tools/BNF/bnf_def_tactics.ML
changeset 57970 eaa986cd285a
parent 57967 e6d2e998c30f
child 58104 c5316f843f72
     1.1 --- a/src/HOL/Tools/BNF/bnf_def_tactics.ML	Mon Aug 18 13:49:47 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML	Mon Aug 18 14:09:09 2014 +0200
     1.3 @@ -11,6 +11,7 @@
     1.4  sig
     1.5    val mk_collect_set_map_tac: thm list -> tactic
     1.6    val mk_in_mono_tac: int -> tactic
     1.7 +  val mk_inj_map_strong_tac: Proof.context -> thm -> thm list -> thm -> tactic
     1.8    val mk_inj_map_tac: int -> thm -> thm -> thm -> thm -> tactic
     1.9    val mk_map_id: thm -> thm
    1.10    val mk_map_ident: Proof.context -> thm -> thm
    1.11 @@ -70,6 +71,17 @@
    1.12          REPEAT_DETERM_N n o atac))
    1.13    end;
    1.14  
    1.15 +fun mk_inj_map_strong_tac ctxt rel_eq rel_maps rel_mono_strong =
    1.16 +  let
    1.17 +    val rel_eq' = rel_eq RS @{thm predicate2_eqD};
    1.18 +    val rel_maps' = map (fn thm => thm RS iffD1) rel_maps;
    1.19 +  in
    1.20 +    HEADGOAL (dtac (rel_eq' RS iffD2) THEN' rtac (rel_eq' RS iffD1)) THEN
    1.21 +    EVERY (map (HEADGOAL o dtac) rel_maps') THEN
    1.22 +    HEADGOAL (etac rel_mono_strong) THEN
    1.23 +    TRYALL (Goal.assume_rule_tac ctxt)
    1.24 +  end;
    1.25 +
    1.26  fun mk_collect_set_map_tac set_map0s =
    1.27    (rtac (@{thm collect_comp} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN'
    1.28    EVERY' (map (fn set_map0 =>
    1.29 @@ -197,7 +209,7 @@
    1.30          REPEAT_DETERM_N n o rtac @{thm fst_fstOp},
    1.31          in_tac @{thm fstOp_in},
    1.32          rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac map_cong0,
    1.33 -        REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, 
    1.34 +        REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply,
    1.35            rtac ballE, rtac subst,
    1.36            rtac @{thm csquare_def}, rtac @{thm csquare_fstOp_sndOp}, atac, etac notE,
    1.37            etac set_mp, atac],
    1.38 @@ -252,10 +264,10 @@
    1.39      let
    1.40        val bd'_Cinfinite = bd_Cinfinite RS @{thm Cinfinite_csum1};
    1.41        val inserts =
    1.42 -        map (fn set_bd => 
    1.43 +        map (fn set_bd =>
    1.44            iffD2 OF [@{thm card_of_ordLeq}, @{thm ordLeq_ordIso_trans} OF
    1.45              [set_bd, bd_Card_order RS @{thm card_of_Field_ordIso} RS @{thm ordIso_symmetric}]])
    1.46 -        set_bds;        
    1.47 +        set_bds;
    1.48      in
    1.49        EVERY' [rtac (Drule.rotate_prems 1 ctrans), rtac @{thm cprod_cinfinite_bound},
    1.50          rtac (ctrans OF @{thms ordLeq_csum2 ordLeq_cexp2}), rtac @{thm card_of_Card_order},