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