src/HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML
author blanchet
Tue Oct 01 14:05:25 2013 +0200 (2013-10-01)
changeset 54006 9fe1bd54d437
parent 53920 c6de7f20c845
permissions -rw-r--r--
renamed theory file
     1 (*  Title:      HOL/BNF/Tools/bnf_ctr_sugar_tactics.ML
     2     Author:     Jasmin Blanchette, TU Muenchen
     3     Copyright   2012
     4 
     5 Tactics for wrapping existing freely generated type's constructors.
     6 *)
     7 
     8 signature CTR_SUGAR_TACTICS =
     9 sig
    10   val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
    11   val mk_case_tac: Proof.context -> int -> int -> thm -> thm list -> thm list list -> tactic
    12   val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic
    13   val mk_case_conv_if_tac: Proof.context -> int -> thm -> thm list -> thm list list ->
    14     thm list list -> tactic
    15   val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
    16   val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
    17   val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list ->
    18     thm list list list -> thm list list list -> tactic
    19   val mk_half_disc_exclude_tac: Proof.context -> int -> thm -> thm -> tactic
    20   val mk_nchotomy_tac: int -> thm -> tactic
    21   val mk_other_half_disc_exclude_tac: thm -> tactic
    22   val mk_sel_exhaust_tac: int -> thm -> thm list -> tactic
    23   val mk_split_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> thm list
    24     list list -> tactic
    25   val mk_split_asm_tac: Proof.context -> thm -> tactic
    26   val mk_unique_disc_def_tac: int -> thm -> tactic
    27 end;
    28 
    29 structure Ctr_Sugar_Tactics : CTR_SUGAR_TACTICS =
    30 struct
    31 
    32 open BNF_Util
    33 open BNF_Tactics
    34 
    35 val meta_mp = @{thm meta_mp};
    36 
    37 fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P});
    38 
    39 fun mk_nchotomy_tac n exhaust =
    40   HEADGOAL (rtac allI THEN' rtac exhaust THEN'
    41    EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n)));
    42 
    43 fun mk_unique_disc_def_tac m uexhaust =
    44   HEADGOAL (EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl]);
    45 
    46 fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust =
    47   HEADGOAL (EVERY' ([rtac (other_disc_def RS @{thm arg_cong[of _ _ Not]} RS trans),
    48     rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
    49     hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
    50     rtac distinct, rtac uexhaust] @
    51     (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
    52      |> k = 1 ? swap |> op @)));
    53 
    54 fun mk_half_disc_exclude_tac ctxt m discD disc' =
    55   HEADGOAL (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
    56     rtac disc');
    57 
    58 fun mk_other_half_disc_exclude_tac half = HEADGOAL (etac @{thm contrapos_pn} THEN' etac half);
    59 
    60 fun mk_disc_or_sel_exhaust_tac n exhaust destIs =
    61   HEADGOAL (rtac exhaust THEN'
    62     EVERY' (map2 (fn k => fn destI => dtac destI THEN'
    63       select_prem_tac n (etac meta_mp) k THEN' atac) (1 upto n) destIs));
    64 
    65 val mk_disc_exhaust_tac = mk_disc_or_sel_exhaust_tac;
    66 
    67 fun mk_sel_exhaust_tac n disc_exhaust collapses =
    68   mk_disc_or_sel_exhaust_tac n disc_exhaust collapses ORELSE
    69   HEADGOAL (etac meta_mp THEN' resolve_tac collapses);
    70 
    71 fun mk_collapse_tac ctxt m discD sels =
    72   HEADGOAL (dtac discD THEN'
    73     (if m = 0 then
    74        atac
    75      else
    76        REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
    77        SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl));
    78 
    79 fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss
    80     disc_excludesss' =
    81   if ms = [0] then
    82     HEADGOAL (rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses))) THEN'
    83       TRY o EVERY' [rtac udisc_exhaust, atac, rtac vdisc_exhaust, atac])
    84   else
    85     let val ks = 1 upto n in
    86       HEADGOAL (rtac udisc_exhaust THEN'
    87         EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' =>
    88             fn uuncollapse =>
    89           EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac,
    90             rtac sym, rtac vdisc_exhaust,
    91             EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse =>
    92               EVERY'
    93                 (if k' = k then
    94                    [rtac (vuncollapse RS trans), TRY o atac] @
    95                    (if m = 0 then
    96                       [rtac refl]
    97                     else
    98                       [if n = 1 then K all_tac else EVERY' [dtac meta_mp, atac, dtac meta_mp, atac],
    99                        REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE,
   100                        asm_simp_tac (ss_only [] ctxt)])
   101                  else
   102                    [dtac (the_single (if k = n then disc_excludes else disc_excludes')),
   103                     etac (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}),
   104                     atac, atac]))
   105               ks disc_excludess disc_excludess' uncollapses)])
   106           ks ms disc_excludesss disc_excludesss' uncollapses))
   107     end;
   108 
   109 fun mk_case_same_ctr_tac ctxt injects =
   110   REPEAT_DETERM o etac exE THEN' etac conjE THEN'
   111     (case injects of
   112       [] => atac
   113     | [inject] => dtac (inject RS iffD1) THEN' REPEAT_DETERM o etac conjE THEN'
   114         hyp_subst_tac ctxt THEN' rtac refl);
   115 
   116 fun mk_case_distinct_ctrs_tac ctxt distincts =
   117   REPEAT_DETERM o etac exE THEN' etac conjE THEN' full_simp_tac (ss_only distincts ctxt);
   118 
   119 fun mk_case_tac ctxt n k case_def injects distinctss =
   120   let
   121     val case_def' = mk_unabs_def (n + 1) (case_def RS meta_eq_to_obj_eq);
   122     val ks = 1 upto n;
   123   in
   124     HEADGOAL (rtac (case_def' RS trans) THEN' rtac @{thm the_equality} THEN'
   125       rtac (mk_disjIN n k) THEN' REPEAT_DETERM o rtac exI THEN' rtac conjI THEN' rtac refl THEN'
   126       rtac refl THEN'
   127       EVERY' (map2 (fn k' => fn distincts =>
   128         (if k' < n then etac disjE else K all_tac) THEN'
   129         (if k' = k then mk_case_same_ctr_tac ctxt injects
   130          else mk_case_distinct_ctrs_tac ctxt distincts)) ks distinctss))
   131   end;
   132 
   133 fun mk_case_conv_if_tac ctxt n uexhaust cases discss' selss =
   134   HEADGOAL (rtac uexhaust THEN'
   135     EVERY' (map3 (fn casex => fn if_discs => fn sels =>
   136         EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)),
   137           rtac casex])
   138       cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss));
   139 
   140 fun mk_case_cong_tac ctxt uexhaust cases =
   141   HEADGOAL (rtac uexhaust THEN'
   142     EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases));
   143 
   144 fun mk_split_tac ctxt uexhaust cases selss injectss distinctsss =
   145   HEADGOAL (rtac uexhaust) THEN
   146   ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
   147      simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @
   148        flat (nth distinctsss (k - 1))) ctxt)) k) THEN
   149   ALLGOALS (blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt));
   150 
   151 val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
   152 
   153 fun mk_split_asm_tac ctxt split =
   154   HEADGOAL (rtac (split RS trans)) THEN unfold_thms_tac ctxt split_asm_thms THEN
   155   HEADGOAL (rtac refl);
   156 
   157 end;