src/HOL/BNF/Tools/bnf_def_tactics.ML
author blanchet
Mon May 06 21:20:54 2013 +0200 (2013-05-06)
changeset 51884 2928fda12661
parent 51798 ad3a241def73
child 51893 596baae88a88
permissions -rw-r--r--
factor out construction of iterator
blanchet@49509
     1
(*  Title:      HOL/BNF/Tools/bnf_def_tactics.ML
blanchet@49284
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@49284
     3
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@49284
     4
    Copyright   2012
blanchet@49284
     5
blanchet@49284
     6
Tactics for definition of bounded natural functors.
blanchet@49284
     7
*)
blanchet@49284
     8
blanchet@49284
     9
signature BNF_DEF_TACTICS =
blanchet@49284
    10
sig
blanchet@51766
    11
  val mk_collect_set_map_tac: thm list -> tactic
blanchet@51762
    12
  val mk_map_id': thm -> thm
blanchet@51762
    13
  val mk_map_comp': thm -> thm
wenzelm@51798
    14
  val mk_map_cong_tac: Proof.context -> thm -> tactic
blanchet@49284
    15
  val mk_in_mono_tac: int -> tactic
blanchet@49284
    16
  val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
blanchet@51766
    17
  val mk_set_map': thm -> thm
blanchet@49284
    18
blanchet@49506
    19
  val mk_srel_Gr_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
blanchet@49284
    20
    {prems: thm list, context: Proof.context} -> tactic
blanchet@49506
    21
  val mk_srel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
blanchet@49506
    22
  val mk_srel_O_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
blanchet@49284
    23
    {prems: thm list, context: Proof.context} -> tactic
blanchet@49506
    24
  val mk_in_srel_tac: thm list -> int -> {prems: 'b, context: Proof.context} -> tactic
blanchet@49506
    25
  val mk_srel_converse_tac: thm -> tactic
blanchet@49506
    26
  val mk_srel_converse_le_tac: thm list -> thm -> thm -> thm -> thm list ->
blanchet@49284
    27
    {prems: thm list, context: Proof.context} -> tactic
blanchet@49506
    28
  val mk_srel_mono_tac: thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
blanchet@49284
    29
end;
blanchet@49284
    30
blanchet@49284
    31
structure BNF_Def_Tactics : BNF_DEF_TACTICS =
blanchet@49284
    32
struct
blanchet@49284
    33
blanchet@49284
    34
open BNF_Util
blanchet@49284
    35
open BNF_Tactics
blanchet@49284
    36
blanchet@51762
    37
fun mk_map_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply};
blanchet@51762
    38
fun mk_map_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
wenzelm@51798
    39
fun mk_map_cong_tac ctxt cong0 =
wenzelm@51798
    40
  (hyp_subst_tac ctxt THEN' rtac cong0 THEN'
blanchet@51762
    41
   REPEAT_DETERM o (dtac meta_spec THEN' etac meta_mp THEN' atac)) 1;
blanchet@51766
    42
fun mk_set_map' set_map = set_map RS @{thm pointfreeE};
traytel@49490
    43
fun mk_in_mono_tac n = if n = 0 then rtac subset_UNIV 1
blanchet@49284
    44
  else (rtac subsetI THEN'
blanchet@49284
    45
  rtac CollectI) 1 THEN
blanchet@49284
    46
  REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN
blanchet@49284
    47
  REPEAT_DETERM_N (n - 1)
blanchet@49284
    48
    ((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN
blanchet@49284
    49
  (etac subset_trans THEN' atac) 1;
blanchet@49284
    50
blanchet@51766
    51
fun mk_collect_set_map_tac set_maps =
traytel@49623
    52
  (rtac (@{thm collect_o} RS trans) THEN' rtac @{thm arg_cong[of _ _ collect]} THEN'
blanchet@51766
    53
  EVERY' (map (fn set_map =>
traytel@49623
    54
    rtac (mk_trans @{thm image_insert} @{thm arg_cong2[of _ _ _ _ insert]}) THEN'
blanchet@51766
    55
    rtac set_map) set_maps) THEN'
traytel@49623
    56
  rtac @{thm image_empty}) 1;
blanchet@49284
    57
blanchet@51766
    58
fun mk_map_wppull_tac map_id map_cong0 map_wpull map_comp set_maps =
blanchet@51766
    59
  if null set_maps then
blanchet@49284
    60
    EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1
blanchet@49284
    61
  else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull},
blanchet@49284
    62
    REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull,
blanchet@49284
    63
    REPEAT_DETERM o rtac @{thm wpull_thePull}, rtac ballI,
blanchet@49284
    64
    REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac CollectI,
blanchet@49284
    65
    CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
blanchet@49284
    66
      rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac])
blanchet@51766
    67
      set_maps,
blanchet@49284
    68
    CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans),
blanchet@51761
    69
      rtac (map_comp RS trans RS sym), rtac map_cong0,
blanchet@51766
    70
      REPEAT_DETERM_N (length set_maps) o EVERY' [rtac (o_apply RS trans),
blanchet@49284
    71
        rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm,
blanchet@49284
    72
        rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1;
blanchet@49284
    73
blanchet@51766
    74
fun mk_srel_Gr_tac srel_O_Grs map_id map_cong0 map_id' map_comp set_maps
blanchet@49284
    75
  {context = ctxt, prems = _} =
blanchet@49284
    76
  let
blanchet@51766
    77
    val n = length set_maps;
blanchet@49284
    78
  in
blanchet@51766
    79
    if null set_maps then
blanchet@49506
    80
      unfold_thms_tac ctxt srel_O_Grs THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
blanchet@49506
    81
    else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN
blanchet@49284
    82
      EVERY' [rtac equalityI, rtac subsetI,
blanchet@49284
    83
        REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
traytel@49488
    84
        REPEAT_DETERM o dtac Pair_eqD,
wenzelm@51798
    85
        REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
traytel@49488
    86
        rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
blanchet@51761
    87
        rtac sym, rtac trans, rtac map_comp, rtac map_cong0,
blanchet@49284
    88
        REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac,
wenzelm@51798
    89
          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
blanchet@49284
    90
          rtac (o_apply RS trans), rtac (@{thm fst_conv} RS arg_cong RS trans),
blanchet@49284
    91
          rtac (@{thm snd_conv} RS sym)],
blanchet@49284
    92
        rtac CollectI,
blanchet@49284
    93
        CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
blanchet@49284
    94
          rtac @{thm image_subsetI}, dtac @{thm set_rev_mp}, atac,
wenzelm@51798
    95
          REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac ctxt,
blanchet@51766
    96
          stac @{thm fst_conv}, atac]) set_maps,
blanchet@49284
    97
        rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE],
traytel@49488
    98
        REPEAT_DETERM o dtac Pair_eqD,
wenzelm@51798
    99
        REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
blanchet@49284
   100
        rtac @{thm relcompI}, rtac @{thm converseI},
traytel@49495
   101
        EVERY' (map2 (fn convol => fn map_id =>
traytel@49495
   102
          EVERY' [rtac CollectI, rtac exI, rtac conjI,
traytel@49495
   103
            rtac Pair_eqI, rtac conjI, rtac refl, rtac sym,
blanchet@51761
   104
            rtac (box_equals OF [map_cong0, map_comp RS sym, map_id]),
traytel@49495
   105
            REPEAT_DETERM_N n o rtac (convol RS fun_cong),
traytel@49495
   106
            REPEAT_DETERM o eresolve_tac [CollectE, conjE],
traytel@49495
   107
            rtac CollectI,
traytel@49495
   108
            CONJ_WRAP' (fn thm =>
traytel@49495
   109
              EVERY' [rtac @{thm ord_eq_le_trans}, rtac thm, rtac @{thm image_subsetI},
traytel@49495
   110
                rtac @{thm convol_memI[of id _ "%x. x", OF id_apply refl]}, etac set_mp, atac])
blanchet@51766
   111
            set_maps])
traytel@49495
   112
          @{thms fst_convol snd_convol} [map_id', refl])] 1
blanchet@49284
   113
  end;
blanchet@49284
   114
blanchet@49506
   115
fun mk_srel_Id_tac n srel_Gr map_id {context = ctxt, prems = _} =
blanchet@49506
   116
  unfold_thms_tac ctxt [srel_Gr, @{thm Id_alt}] THEN
traytel@49621
   117
  (if n = 0 then rtac refl 1
traytel@49621
   118
  else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
traytel@49621
   119
    rtac equalityI, rtac subset_UNIV, rtac subsetI, rtac CollectI,
traytel@49621
   120
    CONJ_WRAP' (K (rtac subset_UNIV)) (1 upto n), rtac map_id] 1);
blanchet@49284
   121
blanchet@49506
   122
fun mk_srel_mono_tac srel_O_Grs in_mono {context = ctxt, prems = _} =
blanchet@49506
   123
  unfold_thms_tac ctxt srel_O_Grs THEN
blanchet@49284
   124
    EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]},
blanchet@49284
   125
      rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac,
blanchet@49284
   126
      rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1;
blanchet@49284
   127
blanchet@51766
   128
fun mk_srel_converse_le_tac srel_O_Grs srel_Id map_cong0 map_comp set_maps
blanchet@49284
   129
  {context = ctxt, prems = _} =
blanchet@49284
   130
  let
blanchet@51766
   131
    val n = length set_maps;
blanchet@49284
   132
  in
blanchet@51766
   133
    if null set_maps then
blanchet@49506
   134
      unfold_thms_tac ctxt [srel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
blanchet@49506
   135
    else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN
blanchet@49284
   136
      EVERY' [rtac @{thm subrelI},
blanchet@49284
   137
        REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
traytel@49488
   138
        REPEAT_DETERM o dtac Pair_eqD,
wenzelm@51798
   139
        REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt, rtac @{thm converseI},
blanchet@49284
   140
        rtac @{thm relcompI}, rtac @{thm converseI},
blanchet@49284
   141
        EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
traytel@49488
   142
          rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac trans,
blanchet@51761
   143
          rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
blanchet@49284
   144
          rtac (map_comp RS sym), rtac CollectI,
blanchet@49284
   145
          CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
blanchet@51766
   146
            etac @{thm flip_rel}]) set_maps]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
blanchet@49284
   147
  end;
blanchet@49284
   148
blanchet@49506
   149
fun mk_srel_converse_tac le_converse =
blanchet@49284
   150
  EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift},
blanchet@49284
   151
    rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1;
blanchet@49284
   152
blanchet@51766
   153
fun mk_srel_O_tac srel_O_Grs srel_Id map_cong0 map_wppull map_comp set_maps
blanchet@49284
   154
  {context = ctxt, prems = _} =
blanchet@49284
   155
  let
blanchet@51766
   156
    val n = length set_maps;
blanchet@49284
   157
    fun in_tac nthO_in = rtac CollectI THEN'
blanchet@49284
   158
        CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
blanchet@51766
   159
          rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_maps;
blanchet@49284
   160
  in
blanchet@51766
   161
    if null set_maps then unfold_thms_tac ctxt [srel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
blanchet@49506
   162
    else unfold_thms_tac ctxt (@{thm Gr_def} :: srel_O_Grs) THEN
blanchet@49284
   163
      EVERY' [rtac equalityI, rtac @{thm subrelI},
blanchet@49284
   164
        REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
traytel@49488
   165
        REPEAT_DETERM o dtac Pair_eqD,
wenzelm@51798
   166
        REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
blanchet@49284
   167
        rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI},
traytel@49488
   168
        rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
blanchet@51761
   169
        rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
blanchet@49284
   170
        REPEAT_DETERM_N n o rtac @{thm fst_fstO},
blanchet@49284
   171
        in_tac @{thm fstO_in},
traytel@49488
   172
        rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
blanchet@51761
   173
        rtac sym, rtac trans, rtac map_comp, rtac map_cong0,
blanchet@49284
   174
        REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, rtac ballE, rtac subst,
blanchet@49284
   175
          rtac @{thm csquare_def}, rtac @{thm csquare_fstO_sndO}, atac, etac notE,
blanchet@49284
   176
          etac set_mp, atac],
blanchet@49284
   177
        in_tac @{thm fstO_in},
blanchet@49284
   178
        rtac @{thm relcompI}, rtac @{thm converseI},
traytel@49488
   179
        rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
blanchet@51761
   180
        rtac sym, rtac trans, rtac map_comp, rtac map_cong0,
blanchet@49284
   181
        REPEAT_DETERM_N n o rtac o_apply,
blanchet@49284
   182
        in_tac @{thm sndO_in},
traytel@49488
   183
        rtac CollectI, rtac exI, rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl,
blanchet@51761
   184
        rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
blanchet@49284
   185
        REPEAT_DETERM_N n o rtac @{thm snd_sndO},
blanchet@49284
   186
        in_tac @{thm sndO_in},
blanchet@49284
   187
        rtac @{thm subrelI},
blanchet@49284
   188
        REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
blanchet@49284
   189
        REPEAT_DETERM o eresolve_tac [exE, conjE],
traytel@49488
   190
        REPEAT_DETERM o dtac Pair_eqD,
wenzelm@51798
   191
        REPEAT_DETERM o etac conjE, hyp_subst_tac ctxt,
blanchet@49284
   192
        rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull,
blanchet@51766
   193
        CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_maps,
blanchet@49284
   194
        etac allE, etac impE, etac conjI, etac conjI, atac,
blanchet@49284
   195
        REPEAT_DETERM o eresolve_tac [bexE, conjE],
blanchet@49284
   196
        rtac @{thm relcompI}, rtac @{thm converseI},
blanchet@49284
   197
        EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
traytel@49488
   198
          rtac conjI, rtac Pair_eqI, rtac conjI, rtac refl, rtac sym, rtac trans,
blanchet@51761
   199
          rtac trans, rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
blanchet@49284
   200
          rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1
blanchet@49284
   201
  end;
blanchet@49284
   202
blanchet@49506
   203
fun mk_in_srel_tac srel_O_Grs m {context = ctxt, prems = _} =
blanchet@49284
   204
  let
blanchet@49284
   205
    val ls' = replicate (Int.max (1, m)) ();
blanchet@49284
   206
  in
blanchet@49506
   207
    unfold_thms_tac ctxt (srel_O_Grs @
blanchet@49284
   208
      @{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN
wenzelm@51798
   209
    EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac ctxt, rtac exI,
blanchet@49284
   210
      rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl,
blanchet@49284
   211
      REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI,
blanchet@49284
   212
      REPEAT_DETERM_N 2 o EVERY' [rtac exI, rtac conjI, etac @{thm conjI[OF refl sym]},
blanchet@49284
   213
        CONJ_WRAP' (K atac) ls']] 1
blanchet@49284
   214
  end;
blanchet@49284
   215
blanchet@49284
   216
end;