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