src/HOL/Codatatype/Tools/bnf_def_tactics.ML
author blanchet
Tue Sep 11 18:39:47 2012 +0200 (2012-09-11)
changeset 49286 dde4967c9233
parent 49284 5f39b7940b49
child 49452 e053519494d6
permissions -rw-r--r--
added "defaults" option
     1 (*  Title:      HOL/Codatatype/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_natural_tac: Proof.context -> thm list -> tactic
    12   val mk_id': thm -> thm
    13   val mk_comp': thm -> thm
    14   val mk_in_mono_tac: int -> tactic
    15   val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
    16   val mk_set_natural': thm -> thm
    17 
    18   val mk_rel_Gr_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
    19     {prems: thm list, context: Proof.context} -> tactic
    20   val mk_rel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
    21   val mk_rel_O_tac: thm -> thm -> thm -> thm -> thm -> thm list ->
    22     {prems: thm list, context: Proof.context} -> tactic
    23   val mk_in_rel_tac: thm -> int -> {prems: 'b, context: Proof.context} -> tactic
    24   val mk_rel_converse_tac: thm -> tactic
    25   val mk_rel_converse_le_tac: thm -> thm -> thm -> thm -> thm list ->
    26     {prems: thm list, context: Proof.context} -> tactic
    27   val mk_rel_mono_tac: thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
    28 end;
    29 
    30 structure BNF_Def_Tactics : BNF_DEF_TACTICS =
    31 struct
    32 
    33 open BNF_Util
    34 open BNF_Tactics
    35 
    36 val set_mp = @{thm set_mp};
    37 
    38 fun mk_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply};
    39 fun mk_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
    40 fun mk_set_natural' set_natural = set_natural RS @{thm pointfreeE};
    41 fun mk_in_mono_tac n = if n = 0 then rtac @{thm subset_UNIV} 1
    42   else (rtac subsetI THEN'
    43   rtac CollectI) 1 THEN
    44   REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN
    45   REPEAT_DETERM_N (n - 1)
    46     ((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN
    47   (etac subset_trans THEN' atac) 1;
    48 
    49 fun mk_collect_set_natural_tac ctxt set_naturals =
    50   substs_tac ctxt (@{thms collect_o image_insert image_empty} @ set_naturals) 1 THEN rtac refl 1;
    51 
    52 fun mk_map_wppull_tac map_id map_cong map_wpull map_comp set_naturals =
    53   if null set_naturals then
    54     EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1
    55   else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull},
    56     REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull,
    57     REPEAT_DETERM o rtac @{thm wpull_thePull}, rtac ballI,
    58     REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac CollectI,
    59     CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
    60       rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac])
    61       set_naturals,
    62     CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans),
    63       rtac (map_comp RS trans RS sym), rtac map_cong,
    64       REPEAT_DETERM_N (length set_naturals) o EVERY' [rtac (o_apply RS trans),
    65         rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm,
    66         rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1;
    67 
    68 fun mk_rel_Gr_tac rel_def map_id map_cong map_wpull in_cong map_id' map_comp set_naturals
    69   {context = ctxt, prems = _} =
    70   let
    71     val n = length set_naturals;
    72   in
    73     if null set_naturals then
    74       Local_Defs.unfold_tac ctxt [rel_def] THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
    75     else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN
    76       EVERY' [rtac equalityI, rtac subsetI,
    77         REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
    78         REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
    79         REPEAT_DETERM o etac conjE, hyp_subst_tac,
    80         rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
    81         rtac sym, rtac trans, rtac map_comp, rtac map_cong,
    82         REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac,
    83           REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
    84           rtac (o_apply RS trans), rtac (@{thm fst_conv} RS arg_cong RS trans),
    85           rtac (@{thm snd_conv} RS sym)],
    86         rtac CollectI,
    87         CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
    88           rtac @{thm image_subsetI}, dtac @{thm set_rev_mp}, atac,
    89           REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
    90           stac @{thm fst_conv}, atac]) set_naturals,
    91         rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE],
    92         REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
    93         REPEAT_DETERM o etac conjE, hyp_subst_tac,
    94         rtac allE, rtac subst, rtac @{thm wpull_def}, rtac map_wpull,
    95         REPEAT_DETERM_N n o rtac @{thm wpull_Gr}, etac allE, etac impE, rtac conjI, atac,
    96         rtac conjI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
    97         CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
    98           rtac @{thm image_mono}, atac]) set_naturals,
    99         rtac sym, rtac map_id', REPEAT_DETERM o eresolve_tac [bexE, conjE],
   100         rtac @{thm relcompI}, rtac @{thm converseI},
   101         REPEAT_DETERM_N 2 o EVERY' [rtac CollectI, rtac exI,
   102           rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, etac sym,
   103           etac @{thm set_rev_mp}, rtac equalityD1, rtac in_cong,
   104           REPEAT_DETERM_N n o rtac @{thm Gr_def}]] 1
   105   end;
   106 
   107 fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} =
   108   Local_Defs.unfold_tac ctxt [rel_Gr, @{thm Id_alt}] THEN
   109   subst_tac ctxt [map_id] 1 THEN
   110     (if n = 0 then rtac refl 1
   111     else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
   112       rtac equalityI, rtac @{thm subset_UNIV}, rtac subsetI, rtac CollectI,
   113       CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto n), rtac refl] 1);
   114 
   115 fun mk_rel_mono_tac rel_def in_mono {context = ctxt, prems = _} =
   116   Local_Defs.unfold_tac ctxt [rel_def] THEN
   117     EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]},
   118       rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac,
   119       rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1;
   120 
   121 fun mk_rel_converse_le_tac rel_def rel_Id map_cong map_comp set_naturals
   122   {context = ctxt, prems = _} =
   123   let
   124     val n = length set_naturals;
   125   in
   126     if null set_naturals then
   127       Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
   128     else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN
   129       EVERY' [rtac @{thm subrelI},
   130         REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
   131         REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
   132         REPEAT_DETERM o etac conjE, hyp_subst_tac, rtac @{thm converseI},
   133         rtac @{thm relcompI}, rtac @{thm converseI},
   134         EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
   135           rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac trans,
   136           rtac map_cong, REPEAT_DETERM_N n o rtac thm,
   137           rtac (map_comp RS sym), rtac CollectI,
   138           CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
   139             etac @{thm flip_rel}]) set_naturals]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
   140   end;
   141 
   142 fun mk_rel_converse_tac le_converse =
   143   EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift},
   144     rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1;
   145 
   146 fun mk_rel_O_tac rel_def rel_Id map_cong map_wppull map_comp set_naturals
   147   {context = ctxt, prems = _} =
   148   let
   149     val n = length set_naturals;
   150     fun in_tac nthO_in = rtac CollectI THEN'
   151         CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
   152           rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals;
   153   in
   154     if null set_naturals then Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
   155     else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN
   156       EVERY' [rtac equalityI, rtac @{thm subrelI},
   157         REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
   158         REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
   159         REPEAT_DETERM o etac conjE, hyp_subst_tac,
   160         rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI},
   161         rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
   162         rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
   163         REPEAT_DETERM_N n o rtac @{thm fst_fstO},
   164         in_tac @{thm fstO_in},
   165         rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
   166         rtac sym, rtac trans, rtac map_comp, rtac map_cong,
   167         REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, rtac ballE, rtac subst,
   168           rtac @{thm csquare_def}, rtac @{thm csquare_fstO_sndO}, atac, etac notE,
   169           etac set_mp, atac],
   170         in_tac @{thm fstO_in},
   171         rtac @{thm relcompI}, rtac @{thm converseI},
   172         rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
   173         rtac sym, rtac trans, rtac map_comp, rtac map_cong,
   174         REPEAT_DETERM_N n o rtac o_apply,
   175         in_tac @{thm sndO_in},
   176         rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
   177         rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
   178         REPEAT_DETERM_N n o rtac @{thm snd_sndO},
   179         in_tac @{thm sndO_in},
   180         rtac @{thm subrelI},
   181         REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
   182         REPEAT_DETERM o eresolve_tac [exE, conjE],
   183         REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
   184         REPEAT_DETERM o etac conjE, hyp_subst_tac,
   185         rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull,
   186         CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_naturals,
   187         etac allE, etac impE, etac conjI, etac conjI, atac,
   188         REPEAT_DETERM o eresolve_tac [bexE, conjE],
   189         rtac @{thm relcompI}, rtac @{thm converseI},
   190         EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
   191           rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac sym, rtac trans,
   192           rtac trans, rtac map_cong, REPEAT_DETERM_N n o rtac thm,
   193           rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1
   194   end;
   195 
   196 fun mk_in_rel_tac rel_def m {context = ctxt, prems = _} =
   197   let
   198     val ls' = replicate (Int.max (1, m)) ();
   199   in
   200     Local_Defs.unfold_tac ctxt (rel_def ::
   201       @{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN
   202     EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI,
   203       rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl,
   204       REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI,
   205       REPEAT_DETERM_N 2 o EVERY' [rtac exI, rtac conjI, etac @{thm conjI[OF refl sym]},
   206         CONJ_WRAP' (K atac) ls']] 1
   207   end;
   208 
   209 end;