1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Mon Nov 04 16:53:43 2013 +0100
1.3 @@ -0,0 +1,135 @@
1.4 +(* Title: HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML
1.5 + Author: Jasmin Blanchette, TU Muenchen
1.6 + Copyright 2013
1.7 +
1.8 +Tactics for corecursor sugar.
1.9 +*)
1.10 +
1.11 +signature BNF_GFP_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: Proof.context -> thm list -> 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 +end;
1.23 +
1.24 +structure BNF_GFP_Rec_Sugar_Tactics : BNF_GFP_REC_SUGAR_TACTICS =
1.25 +struct
1.26 +
1.27 +open BNF_Util
1.28 +open BNF_Tactics
1.29 +
1.30 +val falseEs = @{thms not_TrueE FalseE};
1.31 +val Let_def = @{thm Let_def};
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_primcorec_assumption_tac ctxt discIs =
1.38 + SELECT_GOAL (unfold_thms_tac ctxt
1.39 + @{thms not_not not_False_eq_True not_True_eq_False de_Morgan_conj de_Morgan_disj} THEN
1.40 + SOLVE (HEADGOAL (REPEAT o (rtac refl ORELSE' atac ORELSE' etac conjE ORELSE'
1.41 + eresolve_tac falseEs ORELSE'
1.42 + resolve_tac @{thms TrueI conjI disjI1 disjI2} ORELSE'
1.43 + dresolve_tac discIs THEN' atac ORELSE'
1.44 + etac notE THEN' atac ORELSE'
1.45 + etac disjE))));
1.46 +
1.47 +fun mk_primcorec_same_case_tac m =
1.48 + HEADGOAL (if m = 0 then rtac TrueI
1.49 + else REPEAT_DETERM_N (m - 1) o (rtac conjI THEN' atac) THEN' atac);
1.50 +
1.51 +fun mk_primcorec_different_case_tac ctxt m excl =
1.52 + HEADGOAL (if m = 0 then mk_primcorec_assumption_tac ctxt []
1.53 + else dtac excl THEN' (REPEAT_DETERM_N (m - 1) o atac) THEN' mk_primcorec_assumption_tac ctxt []);
1.54 +
1.55 +fun mk_primcorec_cases_tac ctxt k m exclsss =
1.56 + let val n = length exclsss in
1.57 + EVERY (map (fn [] => if k = n then all_tac else mk_primcorec_same_case_tac m
1.58 + | [excl] => mk_primcorec_different_case_tac ctxt m excl)
1.59 + (take k (nth exclsss (k - 1))))
1.60 + end;
1.61 +
1.62 +fun mk_primcorec_prelude ctxt defs thm =
1.63 + unfold_thms_tac ctxt defs THEN HEADGOAL (rtac thm) THEN
1.64 + unfold_thms_tac ctxt @{thms Let_def split};
1.65 +
1.66 +fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss =
1.67 + mk_primcorec_prelude ctxt defs disc_corec THEN mk_primcorec_cases_tac ctxt k m exclsss;
1.68 +
1.69 +fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms maps map_idents map_comps f_sel k m
1.70 + exclsss =
1.71 + mk_primcorec_prelude ctxt defs (f_sel RS trans) THEN
1.72 + mk_primcorec_cases_tac ctxt k m exclsss THEN
1.73 + HEADGOAL (REPEAT_DETERM o (rtac refl ORELSE' rtac ext ORELSE'
1.74 + eresolve_tac falseEs ORELSE'
1.75 + resolve_tac split_connectI ORELSE'
1.76 + Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
1.77 + Splitter.split_tac (split_if :: splits) ORELSE'
1.78 + eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac ORELSE'
1.79 + etac notE THEN' atac ORELSE'
1.80 + (CHANGED o SELECT_GOAL (unfold_thms_tac ctxt
1.81 + (@{thms id_def o_def split_def sum.cases} @ maps @ map_comps @ map_idents)))));
1.82 +
1.83 +fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse maybe_disc_f sel_fs =
1.84 + HEADGOAL (rtac ((if null sel_fs then collapse else collapse RS sym) RS trans) THEN'
1.85 + (the_default (K all_tac) (Option.map rtac maybe_disc_f)) THEN' REPEAT_DETERM_N m o atac) THEN
1.86 + unfold_thms_tac ctxt (Let_def :: sel_fs) THEN HEADGOAL (rtac refl);
1.87 +
1.88 +fun inst_split_eq ctxt split =
1.89 + (case prop_of split of
1.90 + @{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ (Var (_, Type (_, [T, _])) $ _) $ _) =>
1.91 + let
1.92 + val s = Name.uu;
1.93 + val eq = Abs (Name.uu, T, HOLogic.mk_eq (Free (s, T), Bound 0));
1.94 + val split' = Drule.instantiate' [] [SOME (certify ctxt eq)] split;
1.95 + in
1.96 + Thm.generalize ([], [s]) (Thm.maxidx_of split' + 1) split'
1.97 + end
1.98 + | _ => split);
1.99 +
1.100 +fun distinct_in_prems_tac distincts =
1.101 + eresolve_tac (map (fn thm => thm RS neq_eq_eq_contradict) distincts) THEN' atac;
1.102 +
1.103 +(* TODO: reduce code duplication with selector tactic above *)
1.104 +fun mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms m f_ctr =
1.105 + let
1.106 + val splits' =
1.107 + map (fn th => th RS iffD2) (@{thm split_if_eq2} :: map (inst_split_eq ctxt) splits)
1.108 + in
1.109 + HEADGOAL (REPEAT o (resolve_tac (splits' @ split_connectI))) THEN
1.110 + mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN
1.111 + HEADGOAL ((REPEAT_DETERM_N m o mk_primcorec_assumption_tac ctxt discIs) THEN'
1.112 + SELECT_GOAL (SOLVE (HEADGOAL (REPEAT_DETERM o
1.113 + (rtac refl ORELSE' atac ORELSE'
1.114 + resolve_tac (@{thm Code.abort_def} :: split_connectI) ORELSE'
1.115 + Splitter.split_tac (split_if :: splits) ORELSE'
1.116 + Splitter.split_asm_tac (split_if_asm :: split_asms) ORELSE'
1.117 + mk_primcorec_assumption_tac ctxt discIs ORELSE'
1.118 + distinct_in_prems_tac distincts ORELSE'
1.119 + (TRY o dresolve_tac discIs) THEN' etac notE THEN' atac)))))
1.120 + end;
1.121 +
1.122 +fun mk_primcorec_raw_code_of_ctr_tac ctxt distincts discIs splits split_asms ms f_ctrs =
1.123 + EVERY (map2 (mk_primcorec_raw_code_of_ctr_single_tac ctxt distincts discIs splits split_asms) ms
1.124 + f_ctrs) THEN
1.125 + IF_UNSOLVED (unfold_thms_tac ctxt @{thms Code.abort_def} THEN
1.126 + HEADGOAL (REPEAT_DETERM o resolve_tac (refl :: split_connectI)));
1.127 +
1.128 +fun mk_primcorec_code_of_raw_code_tac ctxt distincts splits raw =
1.129 + HEADGOAL (rtac raw ORELSE' rtac (raw RS trans) THEN'
1.130 + SELECT_GOAL (unfold_thms_tac ctxt [Let_def]) THEN' REPEAT_DETERM o
1.131 + (rtac refl ORELSE' atac ORELSE'
1.132 + resolve_tac split_connectI ORELSE'
1.133 + Splitter.split_tac (split_if :: splits) ORELSE'
1.134 + distinct_in_prems_tac distincts ORELSE'
1.135 + rtac sym THEN' atac ORELSE'
1.136 + etac notE THEN' atac));
1.137 +
1.138 +end;