src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
author wenzelm
Fri Mar 06 15:58:56 2015 +0100 (2015-03-06)
changeset 59621 291934bac95e
parent 59611 63f8527db07f
child 60251 98754695b421
permissions -rw-r--r--
Thm.cterm_of and Thm.ctyp_of operate on local context;
blanchet@55061
     1
(*  Title:      HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
blanchet@53303
     2
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@53303
     3
    Copyright   2013
blanchet@53303
     4
blanchet@54246
     5
Tactics for corecursor sugar.
blanchet@53303
     6
*)
blanchet@53303
     7
blanchet@54246
     8
signature BNF_GFP_REC_SUGAR_TACTICS =
blanchet@53303
     9
sig
blanchet@54044
    10
  val mk_primcorec_assumption_tac: Proof.context -> thm list -> int -> tactic
blanchet@54978
    11
  val mk_primcorec_code_tac: Proof.context -> thm list -> thm list -> thm -> tactic
blanchet@54954
    12
  val mk_primcorec_ctr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
blanchet@53693
    13
  val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
blanchet@53693
    14
    tactic
blanchet@54969
    15
  val mk_primcorec_disc_iff_tac: Proof.context -> string list -> thm -> thm list -> thm list list ->
blanchet@54923
    16
    thm list -> tactic
blanchet@54923
    17
  val mk_primcorec_exhaust_tac: Proof.context -> string list -> int -> thm -> tactic
blanchet@54924
    18
  val mk_primcorec_nchotomy_tac: Proof.context -> thm list -> tactic
blanchet@54978
    19
  val mk_primcorec_raw_code_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
blanchet@54978
    20
    int list -> thm list -> thm option -> tactic
blanchet@53910
    21
  val mk_primcorec_sel_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
blanchet@54955
    22
    thm list -> thm list -> thm list -> thm -> int -> int -> thm list list list -> tactic
blanchet@53303
    23
end;
blanchet@53303
    24
blanchet@54246
    25
structure BNF_GFP_Rec_Sugar_Tactics : BNF_GFP_REC_SUGAR_TACTICS =
blanchet@53303
    26
struct
blanchet@53303
    27
blanchet@53303
    28
open BNF_Util
blanchet@53303
    29
open BNF_Tactics
blanchet@54923
    30
open BNF_FP_Util
blanchet@53303
    31
blanchet@54899
    32
val atomize_conjL = @{thm atomize_conjL};
blanchet@53905
    33
val falseEs = @{thms not_TrueE FalseE};
blanchet@53910
    34
val neq_eq_eq_contradict = @{thm neq_eq_eq_contradict};
blanchet@53902
    35
val split_if = @{thm split_if};
blanchet@53902
    36
val split_if_asm = @{thm split_if_asm};
blanchet@53902
    37
val split_connectI = @{thms allI impI conjI};
blanchet@54953
    38
val unfold_lets = @{thms Let_def[abs_def] split_beta}
blanchet@53902
    39
blanchet@54923
    40
fun exhaust_inst_as_projs ctxt frees thm =
blanchet@54923
    41
  let
blanchet@54923
    42
    val num_frees = length frees;
wenzelm@59582
    43
    val fs = Term.add_vars (Thm.prop_of thm) [] |> filter (can dest_funT o snd);
blanchet@54923
    44
    fun find s = find_index (curry (op =) s) frees;
blanchet@54923
    45
    fun mk_cfp (f as ((s, _), T)) =
wenzelm@59621
    46
      (Thm.cterm_of ctxt (Var f), Thm.cterm_of ctxt (mk_proj T num_frees (find s)));
blanchet@54923
    47
    val cfps = map mk_cfp fs;
blanchet@54923
    48
  in
blanchet@54923
    49
    Drule.cterm_instantiate cfps thm
blanchet@54923
    50
  end;
blanchet@54923
    51
blanchet@54923
    52
val exhaust_inst_as_projs_tac = PRIMITIVE oo exhaust_inst_as_projs;
blanchet@54923
    53
blanchet@54923
    54
fun distinct_in_prems_tac distincts =
wenzelm@59498
    55
  eresolve0_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac;
blanchet@54923
    56
blanchet@57983
    57
fun mk_primcorec_nchotomy_tac ctxt exhaust_discs =
blanchet@57983
    58
  HEADGOAL (Method.insert_tac exhaust_discs THEN' clean_blast_tac ctxt);
blanchet@54924
    59
blanchet@54923
    60
fun mk_primcorec_exhaust_tac ctxt frees n nchotomy =
blanchet@54844
    61
  let val ks = 1 upto n in
blanchet@54905
    62
    HEADGOAL (atac ORELSE'
blanchet@54905
    63
      cut_tac nchotomy THEN'
blanchet@54923
    64
      K (exhaust_inst_as_projs_tac ctxt frees) THEN'
blanchet@54905
    65
      EVERY' (map (fn k =>
blanchet@54905
    66
          (if k < n then etac disjE else K all_tac) THEN'
blanchet@54920
    67
          REPEAT o (dtac meta_mp THEN' atac ORELSE'
blanchet@54920
    68
            etac conjE THEN' dtac meta_mp THEN' atac ORELSE'
blanchet@54920
    69
            atac))
blanchet@54905
    70
        ks))
blanchet@54844
    71
  end;
blanchet@54844
    72
blanchet@53903
    73
fun mk_primcorec_assumption_tac ctxt discIs =
blanchet@54954
    74
  SELECT_GOAL (unfold_thms_tac ctxt @{thms fst_conv snd_conv not_not not_False_eq_True
blanchet@54954
    75
      not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN
blanchet@53926
    76
    SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE'
wenzelm@59498
    77
    eresolve_tac ctxt falseEs ORELSE'
wenzelm@59498
    78
    resolve_tac ctxt @{thms TrueI conjI disjI1 disjI2} ORELSE'
wenzelm@59498
    79
    dresolve_tac ctxt discIs THEN' atac ORELSE'
blanchet@53929
    80
    etac notE THEN' atac ORELSE'
blanchet@54044
    81
    etac disjE))));
blanchet@53303
    82
desharna@59274
    83
fun ss_fst_snd_conv ctxt = simpset_of (ss_only @{thms fst_conv snd_conv} ctxt);
blanchet@54954
    84
desharna@59274
    85
fun case_atac ctxt = simp_tac (put_simpset (ss_fst_snd_conv ctxt) ctxt);
blanchet@54954
    86
blanchet@54954
    87
fun same_case_tac ctxt m =
blanchet@53303
    88
  HEADGOAL (if m = 0 then rtac TrueI
blanchet@54954
    89
    else REPEAT_DETERM_N (m - 1) o (rtac conjI THEN' case_atac ctxt) THEN' case_atac ctxt);
blanchet@53303
    90
blanchet@54971
    91
fun different_case_tac ctxt m exclude =
blanchet@54954
    92
  HEADGOAL (if m = 0 then
blanchet@54954
    93
      mk_primcorec_assumption_tac ctxt []
blanchet@54954
    94
    else
blanchet@54971
    95
      dtac exclude THEN' (REPEAT_DETERM_N (m - 1) o case_atac ctxt) THEN'
blanchet@54954
    96
      mk_primcorec_assumption_tac ctxt []);
blanchet@53303
    97
blanchet@54971
    98
fun cases_tac ctxt k m excludesss =
blanchet@54971
    99
  let val n = length excludesss in
blanchet@54954
   100
    EVERY (map (fn [] => if k = n then all_tac else same_case_tac ctxt m
blanchet@54971
   101
        | [exclude] => different_case_tac ctxt m exclude)
blanchet@54971
   102
      (take k (nth excludesss (k - 1))))
blanchet@53303
   103
  end;
blanchet@53303
   104
blanchet@54954
   105
fun prelude_tac ctxt defs thm =
blanchet@54954
   106
  unfold_thms_tac ctxt defs THEN HEADGOAL (rtac thm) THEN unfold_thms_tac ctxt unfold_lets;
blanchet@53303
   107
blanchet@57983
   108
fun mk_primcorec_disc_tac ctxt defs corec_disc k m excludesss =
blanchet@57983
   109
  prelude_tac ctxt defs corec_disc THEN cases_tac ctxt k m excludesss;
blanchet@53303
   110
blanchet@54969
   111
fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_discs fun_discss
blanchet@57983
   112
    distinct_discs =
blanchet@54910
   113
  HEADGOAL (rtac iffI THEN'
blanchet@54910
   114
    rtac fun_exhaust THEN'
blanchet@54959
   115
    K (exhaust_inst_as_projs_tac ctxt fun_exhaust_frees) THEN'
blanchet@54917
   116
    EVERY' (map (fn [] => etac FalseE
blanchet@54969
   117
        | fun_discs' as [fun_disc'] =>
blanchet@54969
   118
          if eq_list Thm.eq_thm (fun_discs', fun_discs) then
blanchet@54917
   119
            REPEAT_DETERM o etac conjI THEN' (atac ORELSE' rtac TrueI)
blanchet@54917
   120
          else
blanchet@54977
   121
            rtac FalseE THEN'
blanchet@59611
   122
            (rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT o atac ORELSE'
blanchet@54977
   123
             cut_tac fun_disc') THEN'
wenzelm@59498
   124
            dresolve_tac ctxt distinct_discs THEN' etac notE THEN' atac)
blanchet@54917
   125
      fun_discss) THEN'
blanchet@54977
   126
    (etac FalseE ORELSE'
wenzelm@59498
   127
     resolve_tac ctxt (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' atac));
blanchet@54899
   128
blanchet@57399
   129
fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_ident0s map_comps fun_sel k
blanchet@54971
   130
    m excludesss =
blanchet@54954
   131
  prelude_tac ctxt defs (fun_sel RS trans) THEN
blanchet@54971
   132
  cases_tac ctxt k m excludesss THEN
blanchet@55341
   133
  HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE'
wenzelm@59498
   134
    eresolve_tac ctxt falseEs ORELSE'
wenzelm@59498
   135
    resolve_tac ctxt split_connectI ORELSE'
wenzelm@58956
   136
    Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE'
wenzelm@58956
   137
    Splitter.split_tac ctxt (split_if :: splits) ORELSE'
wenzelm@59498
   138
    eresolve_tac ctxt (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
blanchet@54044
   139
    etac notE THEN' atac ORELSE'
blanchet@55067
   140
    (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt (@{thms fst_conv snd_conv id_def comp_def split_def
blanchet@57279
   141
         sum.case sum.sel sum.distinct[THEN eq_False[THEN iffD2]]} @
blanchet@57399
   142
       mapsx @ map_ident0s @ map_comps))) ORELSE'
blanchet@55341
   143
    fo_rtac @{thm cong} ctxt ORELSE'
blanchet@59610
   144
    rtac @{thm ext} ORELSE'
blanchet@59610
   145
    mk_primcorec_assumption_tac ctxt []));
blanchet@53303
   146
blanchet@54954
   147
fun mk_primcorec_ctr_tac ctxt m collapse disc_fun_opt sel_funs =
blanchet@54900
   148
  HEADGOAL (rtac ((if null sel_funs then collapse else collapse RS sym) RS trans) THEN'
blanchet@54926
   149
    (the_default (K all_tac) (Option.map rtac disc_fun_opt)) THEN' REPEAT_DETERM_N m o atac) THEN
blanchet@55004
   150
  unfold_thms_tac ctxt (@{thm split_def} :: unfold_lets @ sel_funs) THEN HEADGOAL (rtac refl);
blanchet@53706
   151
blanchet@54138
   152
fun inst_split_eq ctxt split =
wenzelm@59582
   153
  (case Thm.prop_of split of
blanchet@54138
   154
    @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ (Var (_, Type (_, [T, _])) $ _) $ _) =>
blanchet@54138
   155
    let
blanchet@54138
   156
      val s = Name.uu;
blanchet@54138
   157
      val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
wenzelm@59621
   158
      val split' = Drule.instantiate' [] [SOME (Thm.cterm_of ctxt eq)] split;
blanchet@54138
   159
    in
blanchet@54138
   160
      Thm.generalize ([], [s]) (Thm.maxidx_of split' + 1) split'
blanchet@54138
   161
    end
blanchet@54138
   162
  | _ => split);
blanchet@54138
   163
blanchet@54978
   164
fun raw_code_single_tac ctxt distincts discIs splits split_asms m fun_ctr =
blanchet@54138
   165
  let
blanchet@54138
   166
    val splits' =
blanchet@55342
   167
      map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits);
blanchet@54138
   168
  in
wenzelm@59498
   169
    HEADGOAL (REPEAT o (resolve_tac ctxt (splits' @ split_connectI))) THEN
blanchet@54954
   170
    prelude_tac ctxt [] (fun_ctr RS trans) THEN
blanchet@54138
   171
    HEADGOAL ((REPEAT_DETERM_N m o mk_primcorec_assumption_tac ctxt discIs) THEN'
blanchet@54138
   172
      SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
blanchet@54138
   173
      (rtac refl ORELSE' atac ORELSE'
wenzelm@59498
   174
       resolve_tac ctxt (@{thm Code.abort_def} :: split_connectI) ORELSE'
wenzelm@58956
   175
       Splitter.split_tac ctxt (split_if :: splits) ORELSE'
wenzelm@58956
   176
       Splitter.split_asm_tac ctxt (split_if_asm :: split_asms) ORELSE'
blanchet@54138
   177
       mk_primcorec_assumption_tac ctxt discIs ORELSE'
blanchet@54174
   178
       distinct_in_prems_tac distincts ORELSE'
wenzelm@59498
   179
       (TRY o dresolve_tac ctxt discIs) THEN' etac notE THEN' atac)))))
blanchet@54138
   180
  end;
blanchet@53903
   181
blanchet@54842
   182
fun rulify_nchotomy n = funpow (n - 1) (fn thm => thm RS @{thm Meson.make_pos_rule'});
blanchet@54832
   183
blanchet@54978
   184
fun mk_primcorec_raw_code_tac ctxt distincts discIs splits split_asms ms fun_ctrs nchotomy_opt =
blanchet@54832
   185
  let
blanchet@54832
   186
    val n = length ms;
blanchet@54900
   187
    val (ms', fun_ctrs') =
blanchet@54926
   188
      (case nchotomy_opt of
blanchet@54900
   189
        NONE => (ms, fun_ctrs)
blanchet@54842
   190
      | SOME nchotomy =>
blanchet@54832
   191
        (ms |> split_last ||> K [n - 1] |> op @,
blanchet@54900
   192
         fun_ctrs
blanchet@54843
   193
         |> split_last
blanchet@54899
   194
         ||> unfold_thms ctxt [atomize_conjL]
blanchet@54908
   195
         ||> (fn thm => [rulify_nchotomy n nchotomy RS thm] handle THM _ => [thm])
blanchet@54843
   196
         |> op @));
blanchet@54832
   197
  in
blanchet@54978
   198
    EVERY (map2 (raw_code_single_tac ctxt distincts discIs splits split_asms) ms' fun_ctrs') THEN
blanchet@54832
   199
    IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN
wenzelm@59498
   200
      HEADGOAL (REPEAT_DETERM o resolve_tac ctxt (refl :: split_connectI)))
blanchet@54832
   201
  end;
blanchet@53693
   202
blanchet@54978
   203
fun mk_primcorec_code_tac ctxt distincts splits raw =
blanchet@54101
   204
  HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN'
blanchet@54954
   205
    SELECT_GOAL (unfold_thms_tac ctxt unfold_lets) THEN' REPEAT_DETERM o
blanchet@54174
   206
    (rtac refl ORELSE' atac ORELSE'
wenzelm@59498
   207
     resolve_tac ctxt split_connectI ORELSE'
wenzelm@58956
   208
     Splitter.split_tac ctxt (split_if :: splits) ORELSE'
blanchet@54174
   209
     distinct_in_prems_tac distincts ORELSE'
blanchet@54174
   210
     rtac sym THEN' atac ORELSE'
blanchet@54042
   211
     etac notE THEN' atac));
blanchet@53921
   212
blanchet@53303
   213
end;