1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Thu Dec 05 17:52:12 2013 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,116 +0,0 @@
1.4 -(* Title: HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML
1.5 - Author: Jasmin Blanchette, TU Muenchen
1.6 - Copyright 2013
1.7 -
1.8 -Tactics for recursor and corecursor sugar.
1.9 -*)
1.10 -
1.11 -signature BNF_FP_REC_SUGAR_TACTICS =
1.12 -sig
1.13 - val mk_primcorec_assumption_tac: Proof.context -> thm list -> int -> tactic
1.14 - val mk_primcorec_code_of_raw_code_tac: thm list -> thm -> tactic
1.15 - val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic
1.16 - val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list ->
1.17 - tactic
1.18 - val mk_primcorec_raw_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list ->
1.19 - thm list -> int list -> thm list -> tactic
1.20 - val mk_primcorec_sel_tac: Proof.context -> thm list -> thm list -> thm list -> thm list ->
1.21 - thm list -> thm list -> thm list -> thm -> int -> int -> thm list list list -> tactic
1.22 - val mk_primrec_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> tactic
1.23 -end;
1.24 -
1.25 -structure BNF_FP_Rec_Sugar_Tactics : BNF_FP_REC_SUGAR_TACTICS =
1.26 -struct
1.27 -
1.28 -open BNF_Util
1.29 -open BNF_Tactics
1.30 -
1.31 -val falseEs = @{thms not_TrueE FalseE};
1.32 -val neq_eq_eq_contradict = @{thm neq_eq_eq_contradict};
1.33 -val split_if = @{thm split_if};
1.34 -val split_if_asm = @{thm split_if_asm};
1.35 -val split_connectI = @{thms allI impI conjI};
1.36 -
1.37 -fun mk_primrec_tac ctxt num_extra_args map_idents map_comps fun_defs recx =
1.38 - unfold_thms_tac ctxt fun_defs THEN
1.39 - HEADGOAL (rtac (funpow num_extra_args (fn thm => thm RS fun_cong) recx RS trans)) THEN
1.40 - unfold_thms_tac ctxt (@{thms id_def split o_def fst_conv snd_conv} @ map_comps @ map_idents) THEN
1.41 - HEADGOAL (rtac refl);
1.42 -
1.43 -fun mk_primcorec_assumption_tac ctxt discIs =
1.44 - SELECT_GOAL (unfold_thms_tac ctxt
1.45 - @{thms not_not not_False_eq_True de_Morgan_conj de_Morgan_disj} THEN
1.46 - SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE'
1.47 - resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE'
1.48 - dresolve_tac discIs THEN' atac ORELSE'
1.49 - etac notE THEN' atac ORELSE'
1.50 - etac disjE))));
1.51 -
1.52 -fun mk_primcorec_same_case_tac m =
1.53 - HEADGOAL (if m = 0 then rtac TrueI
1.54 - else REPEAT_DETERM_N (m - 1) o (rtac conjI THEN' atac) THEN' atac);
1.55 -
1.56 -fun mk_primcorec_different_case_tac ctxt excl =
1.57 - unfold_thms_tac ctxt @{thms not_not not_False_eq_True not_True_eq_False} THEN
1.58 - HEADGOAL (rtac excl THEN_ALL_NEW mk_primcorec_assumption_tac ctxt []);
1.59 -
1.60 -fun mk_primcorec_cases_tac ctxt k m exclsss =
1.61 - let val n = length exclsss in
1.62 - EVERY (map (fn [] => if k = n then all_tac else mk_primcorec_same_case_tac m
1.63 - | [excl] => mk_primcorec_different_case_tac ctxt excl)
1.64 - (take k (nth exclsss (k - 1))))
1.65 - end;
1.66 -
1.67 -fun mk_primcorec_prelude ctxt defs thm =
1.68 - unfold_thms_tac ctxt defs THEN HEADGOAL (rtac thm) THEN
1.69 - unfold_thms_tac ctxt @{thms Let_def split};
1.70 -
1.71 -fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss =
1.72 - mk_primcorec_prelude ctxt defs disc_corec THEN mk_primcorec_cases_tac ctxt k m exclsss;
1.73 -
1.74 -fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms maps map_idents map_comps f_sel k m
1.75 - exclsss =
1.76 - mk_primcorec_prelude ctxt defs (f_sel RS trans) THEN
1.77 - mk_primcorec_cases_tac ctxt k m exclsss THEN
1.78 - HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' rtac ext ORELSE'
1.79 - eresolve_tac falseEs ORELSE'
1.80 - resolve_tac split_connectI ORELSE'
1.81 - Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
1.82 - Splitter.split_tac (split_if :: splits) ORELSE'
1.83 - eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
1.84 - etac notE THEN' atac ORELSE'
1.85 - (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt
1.86 - (@{thms id_apply o_def split_def sum.cases} @ maps @ map_comps @ map_idents)))));
1.87 -
1.88 -fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs =
1.89 - HEADGOAL (rtac ((if null sel_fs then collapse else collapse RS sym) RS trans) THEN'
1.90 - (the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN
1.91 - unfold_thms_tac ctxt sel_fs THEN HEADGOAL (rtac refl);
1.92 -
1.93 -(* TODO: reduce code duplication with selector tactic above *)
1.94 -fun mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m f_ctr =
1.95 - HEADGOAL (REPEAT o (resolve_tac split_connectI ORELSE' split_tac (split_if :: splits))) THEN
1.96 - mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN
1.97 - HEADGOAL ((REPEAT_DETERM_N m o mk_primcorec_assumption_tac ctxt discIs) THEN'
1.98 - SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
1.99 - (rtac refl ORELSE' atac ORELSE'
1.100 - resolve_tac split_connectI ORELSE'
1.101 - Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
1.102 - Splitter.split_tac (split_if :: splits) ORELSE'
1.103 - mk_primcorec_assumption_tac ctxt discIs ORELSE'
1.104 - eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
1.105 - (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))));
1.106 -
1.107 -fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms ctr_thms =
1.108 - EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms)
1.109 - ms ctr_thms);
1.110 -
1.111 -fun mk_primcorec_code_of_raw_code_tac splits raw =
1.112 - HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN' REPEAT_DETERM o
1.113 - (rtac refl ORELSE'
1.114 - (TRY o rtac sym) THEN' atac ORELSE'
1.115 - resolve_tac split_connectI ORELSE'
1.116 - Splitter.split_tac (split_if :: splits) ORELSE'
1.117 - etac notE THEN' atac));
1.118 -
1.119 -end;