src/HOL/Tools/BNF/Tools/bnf_comp_tactics.ML
author blanchet
Mon Jan 20 18:24:56 2014 +0100 (2014-01-20)
changeset 55058 4e700eb471d4
parent 54841 src/HOL/BNF/Tools/bnf_comp_tactics.ML@af71b753c459
permissions -rw-r--r--
moved BNF files to 'HOL'
     1 (*  Title:      HOL/BNF/Tools/bnf_comp_tactics.ML
     2     Author:     Dmitriy Traytel, TU Muenchen
     3     Author:     Jasmin Blanchette, TU Muenchen
     4     Copyright   2012
     5 
     6 Tactics for composition of bounded natural functors.
     7 *)
     8 
     9 signature BNF_COMP_TACTICS =
    10 sig
    11   val mk_comp_bd_card_order_tac: thm list -> thm -> tactic
    12   val mk_comp_bd_cinfinite_tac: thm -> thm -> tactic
    13   val mk_comp_in_alt_tac: Proof.context -> thm list -> tactic
    14   val mk_comp_map_comp0_tac: thm -> thm -> thm list -> tactic
    15   val mk_comp_map_cong0_tac: thm list -> thm -> thm list -> tactic
    16   val mk_comp_map_id0_tac: thm -> thm -> thm list -> tactic
    17   val mk_comp_set_alt_tac: Proof.context -> thm -> tactic
    18   val mk_comp_set_bd_tac: Proof.context -> thm -> thm list -> tactic
    19   val mk_comp_set_map0_tac: thm -> thm -> thm -> thm list -> tactic
    20   val mk_comp_wit_tac: Proof.context -> thm list -> thm -> thm list -> tactic
    21 
    22   val mk_kill_bd_card_order_tac: int -> thm -> tactic
    23   val mk_kill_bd_cinfinite_tac: thm -> tactic
    24   val kill_in_alt_tac: tactic
    25   val mk_kill_map_cong0_tac: Proof.context -> int -> int -> thm -> tactic
    26   val mk_kill_set_bd_tac: thm -> thm -> tactic
    27 
    28   val empty_natural_tac: tactic
    29   val lift_in_alt_tac: tactic
    30   val mk_lift_set_bd_tac: thm -> tactic
    31 
    32   val mk_permute_in_alt_tac: ''a list -> ''a list -> tactic
    33 
    34   val mk_le_rel_OO_tac: thm -> thm -> thm list -> tactic
    35   val mk_simple_rel_OO_Grp_tac: thm -> thm -> tactic
    36   val mk_simple_wit_tac: thm list -> tactic
    37 end;
    38 
    39 structure BNF_Comp_Tactics : BNF_COMP_TACTICS =
    40 struct
    41 
    42 open BNF_Util
    43 open BNF_Tactics
    44 
    45 val Cnotzero_UNIV = @{thm Cnotzero_UNIV};
    46 val arg_cong_Union = @{thm arg_cong[of _ _ Union]};
    47 val csum_Cnotzero1 = @{thm csum_Cnotzero1};
    48 val o_eq_dest_lhs = @{thm o_eq_dest_lhs};
    49 val trans_image_cong_o_apply = @{thm trans[OF image_cong[OF o_apply refl]]};
    50 val trans_o_apply = @{thm trans[OF o_apply]};
    51 
    52 
    53 
    54 (* Composition *)
    55 
    56 fun mk_comp_set_alt_tac ctxt collect_set_map =
    57   unfold_thms_tac ctxt @{thms sym[OF o_assoc]} THEN
    58   unfold_thms_tac ctxt [collect_set_map RS sym] THEN
    59   rtac refl 1;
    60 
    61 fun mk_comp_map_id0_tac Gmap_id0 Gmap_cong0 map_id0s =
    62   EVERY' ([rtac ext, rtac (Gmap_cong0 RS trans)] @
    63     map (fn thm => rtac (thm RS fun_cong)) map_id0s @ [rtac (Gmap_id0 RS fun_cong)]) 1;
    64 
    65 fun mk_comp_map_comp0_tac Gmap_comp0 Gmap_cong0 map_comp0s =
    66   EVERY' ([rtac ext, rtac sym, rtac trans_o_apply,
    67     rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans), rtac Gmap_cong0] @
    68     map (fn thm => rtac (thm RS sym RS fun_cong)) map_comp0s) 1;
    69 
    70 fun mk_comp_set_map0_tac Gmap_comp0 Gmap_cong0 Gset_map0 set_map0s =
    71   EVERY' ([rtac ext] @
    72     replicate 3 (rtac trans_o_apply) @
    73     [rtac (arg_cong_Union RS trans),
    74      rtac (@{thm arg_cong2[of _ _ _ _ collect, OF refl]} RS trans),
    75      rtac (Gmap_comp0 RS sym RS o_eq_dest_lhs RS trans),
    76      rtac Gmap_cong0] @
    77      map (fn thm => rtac (thm RS fun_cong)) set_map0s @
    78      [rtac (Gset_map0 RS o_eq_dest_lhs), rtac sym, rtac trans_o_apply,
    79      rtac trans_image_cong_o_apply, rtac trans_image_cong_o_apply,
    80      rtac (@{thm image_cong} OF [Gset_map0 RS o_eq_dest_lhs RS arg_cong_Union, refl] RS trans),
    81      rtac @{thm trans[OF comp_eq_dest[OF Union_natural[symmetric]]]}, rtac arg_cong_Union,
    82      rtac @{thm trans[OF o_eq_dest_lhs[OF image_o_collect[symmetric]]]},
    83      rtac @{thm fun_cong[OF arg_cong[of _ _ collect]]}] @
    84      [REPEAT_DETERM_N (length set_map0s) o EVERY' [rtac @{thm trans[OF image_insert]},
    85         rtac @{thm arg_cong2[of _ _ _ _ insert]}, rtac ext, rtac trans_o_apply,
    86         rtac trans_image_cong_o_apply, rtac @{thm trans[OF image_image]},
    87         rtac @{thm sym[OF trans[OF o_apply]]}, rtac @{thm image_cong[OF refl o_apply]}],
    88      rtac @{thm image_empty}]) 1;
    89 
    90 fun mk_comp_map_cong0_tac comp_set_alts map_cong0 map_cong0s =
    91   let
    92      val n = length comp_set_alts;
    93   in
    94     (if n = 0 then rtac refl 1
    95     else rtac map_cong0 1 THEN
    96       EVERY' (map_index (fn (i, map_cong0) =>
    97         rtac map_cong0 THEN' EVERY' (map_index (fn (k, set_alt) =>
    98           EVERY' [select_prem_tac n (dtac @{thm meta_spec}) (k + 1), etac meta_mp,
    99             rtac (equalityD2 RS set_mp), rtac (set_alt RS fun_cong RS trans),
   100             rtac trans_o_apply, rtac (@{thm collect_def} RS arg_cong_Union),
   101             rtac @{thm UnionI}, rtac @{thm UN_I}, REPEAT_DETERM_N i o rtac @{thm insertI2},
   102             rtac @{thm insertI1}, rtac (o_apply RS equalityD2 RS set_mp),
   103             etac @{thm imageI}, atac])
   104           comp_set_alts))
   105       map_cong0s) 1)
   106   end;
   107 
   108 fun mk_comp_bd_card_order_tac Fbd_card_orders Gbd_card_order =
   109   let
   110     val (card_orders, last_card_order) = split_last Fbd_card_orders;
   111     fun gen_before thm = rtac @{thm card_order_csum} THEN' rtac thm;
   112   in
   113     (rtac @{thm card_order_cprod} THEN'
   114     WRAP' gen_before (K (K all_tac)) card_orders (rtac last_card_order) THEN'
   115     rtac Gbd_card_order) 1
   116   end;
   117 
   118 fun mk_comp_bd_cinfinite_tac Fbd_cinfinite Gbd_cinfinite =
   119   (rtac @{thm cinfinite_cprod} THEN'
   120    ((K (TRY ((rtac @{thm cinfinite_csum} THEN' rtac disjI1) 1)) THEN'
   121      ((rtac @{thm cinfinite_csum} THEN' rtac disjI1 THEN' rtac Fbd_cinfinite) ORELSE'
   122       rtac Fbd_cinfinite)) ORELSE'
   123     rtac Fbd_cinfinite) THEN'
   124    rtac Gbd_cinfinite) 1;
   125 
   126 fun mk_comp_set_bd_tac ctxt comp_set_alt Gset_Fset_bds =
   127   let
   128     val (bds, last_bd) = split_last Gset_Fset_bds;
   129     fun gen_before bd =
   130       rtac ctrans THEN' rtac @{thm Un_csum} THEN'
   131       rtac ctrans THEN' rtac @{thm csum_mono} THEN'
   132       rtac bd;
   133     fun gen_after _ = rtac @{thm ordIso_imp_ordLeq} THEN' rtac @{thm cprod_csum_distrib1};
   134   in
   135     unfold_thms_tac ctxt [comp_set_alt] THEN
   136     rtac @{thm comp_set_bd_Union_o_collect} 1 THEN
   137     unfold_thms_tac ctxt @{thms Union_image_insert Union_image_empty Union_Un_distrib o_apply} THEN
   138     (rtac ctrans THEN'
   139      WRAP' gen_before gen_after bds (rtac last_bd) THEN'
   140      rtac @{thm ordIso_imp_ordLeq} THEN'
   141      rtac @{thm cprod_com}) 1
   142   end;
   143 
   144 val comp_in_alt_thms = @{thms o_apply collect_def SUP_def image_insert image_empty Union_insert
   145   Union_empty Un_empty_right Union_Un_distrib Un_subset_iff conj_subset_def UN_image_subset
   146   conj_assoc};
   147 
   148 fun mk_comp_in_alt_tac ctxt comp_set_alts =
   149   unfold_thms_tac ctxt (comp_set_alts @ comp_in_alt_thms) THEN
   150   unfold_thms_tac ctxt @{thms set_eq_subset} THEN
   151   rtac conjI 1 THEN
   152   REPEAT_DETERM (
   153     rtac @{thm subsetI} 1 THEN
   154     unfold_thms_tac ctxt @{thms mem_Collect_eq Ball_def} THEN
   155     (REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
   156      REPEAT_DETERM (CHANGED ((
   157        (rtac conjI THEN' (atac ORELSE' rtac subset_UNIV)) ORELSE'
   158        atac ORELSE'
   159        (rtac subset_UNIV)) 1)) ORELSE rtac subset_UNIV 1));
   160 
   161 val comp_wit_thms = @{thms Union_empty_conv o_apply collect_def SUP_def
   162   Union_image_insert Union_image_empty};
   163 
   164 fun mk_comp_wit_tac ctxt Gwit_thms collect_set_map Fwit_thms =
   165   ALLGOALS (dtac @{thm in_Union_o_assoc}) THEN
   166   unfold_thms_tac ctxt (collect_set_map :: comp_wit_thms) THEN
   167   REPEAT_DETERM ((atac ORELSE'
   168     REPEAT_DETERM o eresolve_tac @{thms UnionE UnE} THEN'
   169     etac imageE THEN' TRY o dresolve_tac Gwit_thms THEN'
   170     (etac FalseE ORELSE'
   171     hyp_subst_tac ctxt THEN'
   172     dresolve_tac Fwit_thms THEN'
   173     (etac FalseE ORELSE' atac))) 1);
   174 
   175 
   176 
   177 (* Kill operation *)
   178 
   179 fun mk_kill_map_cong0_tac ctxt n m map_cong0 =
   180   (rtac map_cong0 THEN' EVERY' (replicate n (rtac refl)) THEN'
   181     EVERY' (replicate m (Goal.assume_rule_tac ctxt))) 1;
   182 
   183 fun mk_kill_bd_card_order_tac n bd_card_order =
   184   (rtac @{thm card_order_cprod} THEN'
   185   K (REPEAT_DETERM_N (n - 1)
   186     ((rtac @{thm card_order_csum} THEN'
   187     rtac @{thm card_of_card_order_on}) 1)) THEN'
   188   rtac @{thm card_of_card_order_on} THEN'
   189   rtac bd_card_order) 1;
   190 
   191 fun mk_kill_bd_cinfinite_tac bd_Cinfinite =
   192   (rtac @{thm cinfinite_cprod2} THEN'
   193   TRY o rtac csum_Cnotzero1 THEN'
   194   rtac Cnotzero_UNIV THEN'
   195   rtac bd_Cinfinite) 1;
   196 
   197 fun mk_kill_set_bd_tac bd_Card_order set_bd =
   198   (rtac ctrans THEN'
   199   rtac set_bd THEN'
   200   rtac @{thm ordLeq_cprod2} THEN'
   201   TRY o rtac csum_Cnotzero1 THEN'
   202   rtac Cnotzero_UNIV THEN'
   203   rtac bd_Card_order) 1
   204 
   205 val kill_in_alt_tac =
   206   ((rtac @{thm Collect_cong} THEN' rtac iffI) 1 THEN
   207   REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
   208   REPEAT_DETERM (CHANGED ((etac conjI ORELSE'
   209     rtac conjI THEN' rtac subset_UNIV) 1)) THEN
   210   (rtac subset_UNIV ORELSE' atac) 1 THEN
   211   REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
   212   REPEAT_DETERM (CHANGED ((etac conjI ORELSE' atac) 1))) ORELSE
   213   ((rtac @{thm UNIV_eq_I} THEN' rtac CollectI) 1 THEN
   214     REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac subset_UNIV 1));
   215 
   216 
   217 
   218 (* Lift operation *)
   219 
   220 val empty_natural_tac = rtac @{thm empty_natural} 1;
   221 
   222 fun mk_lift_set_bd_tac bd_Card_order = (rtac @{thm Card_order_empty} THEN' rtac bd_Card_order) 1;
   223 
   224 val lift_in_alt_tac =
   225   ((rtac @{thm Collect_cong} THEN' rtac iffI) 1 THEN
   226   REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
   227   REPEAT_DETERM (CHANGED ((etac conjI ORELSE' atac) 1)) THEN
   228   REPEAT_DETERM (CHANGED (etac conjE 1)) THEN
   229   REPEAT_DETERM (CHANGED ((etac conjI ORELSE'
   230     rtac conjI THEN' rtac @{thm empty_subsetI}) 1)) THEN
   231   (rtac @{thm empty_subsetI} ORELSE' atac) 1) ORELSE
   232   ((rtac sym THEN' rtac @{thm UNIV_eq_I} THEN' rtac CollectI) 1 THEN
   233     REPEAT_DETERM (TRY (rtac conjI 1) THEN rtac @{thm empty_subsetI} 1));
   234 
   235 
   236 
   237 (* Permute operation *)
   238 
   239 fun mk_permute_in_alt_tac src dest =
   240   (rtac @{thm Collect_cong} THEN'
   241   mk_rotate_eq_tac (rtac refl) trans @{thm conj_assoc} @{thm conj_commute} @{thm conj_cong}
   242     dest src) 1;
   243 
   244 fun mk_le_rel_OO_tac outer_le_rel_OO outer_rel_mono inner_le_rel_OOs =
   245   EVERY' (map rtac (@{thm order_trans} :: outer_le_rel_OO :: outer_rel_mono :: inner_le_rel_OOs)) 1;
   246 
   247 fun mk_simple_rel_OO_Grp_tac rel_OO_Grp in_alt_thm =
   248   rtac (trans OF [rel_OO_Grp, in_alt_thm RS @{thm OO_Grp_cong} RS sym]) 1;
   249 
   250 fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));
   251 
   252 end;