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