1.1 --- a/src/HOL/BNF/Tools/ctr_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,172 +0,0 @@
1.4 -(* Title: HOL/BNF/Tools/ctr_sugar_tactics.ML
1.5 - Author: Jasmin Blanchette, TU Muenchen
1.6 - Copyright 2012
1.7 -
1.8 -Tactics for wrapping existing freely generated type's constructors.
1.9 -*)
1.10 -
1.11 -signature CTR_SUGAR_GENERAL_TACTICS =
1.12 -sig
1.13 - val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
1.14 - val unfold_thms_tac: Proof.context -> thm list -> tactic
1.15 -end;
1.16 -
1.17 -signature CTR_SUGAR_TACTICS =
1.18 -sig
1.19 - include CTR_SUGAR_GENERAL_TACTICS
1.20 -
1.21 - val mk_alternate_disc_def_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
1.22 - val mk_case_tac: Proof.context -> int -> int -> thm -> thm list -> thm list list -> tactic
1.23 - val mk_case_cong_tac: Proof.context -> thm -> thm list -> tactic
1.24 - val mk_case_conv_if_tac: Proof.context -> int -> thm -> thm list -> thm list list ->
1.25 - thm list list -> tactic
1.26 - val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
1.27 - val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
1.28 - val mk_expand_tac: Proof.context -> int -> int list -> thm -> thm -> thm list ->
1.29 - thm list list list -> thm list list list -> tactic
1.30 - val mk_half_disc_exclude_tac: Proof.context -> int -> thm -> thm -> tactic
1.31 - val mk_nchotomy_tac: int -> thm -> tactic
1.32 - val mk_other_half_disc_exclude_tac: thm -> tactic
1.33 - val mk_sel_exhaust_tac: int -> thm -> thm list -> tactic
1.34 - val mk_split_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> thm list
1.35 - list list -> tactic
1.36 - val mk_split_asm_tac: Proof.context -> thm -> tactic
1.37 - val mk_unique_disc_def_tac: int -> thm -> tactic
1.38 -end;
1.39 -
1.40 -structure Ctr_Sugar_Tactics : CTR_SUGAR_TACTICS =
1.41 -struct
1.42 -
1.43 -open Ctr_Sugar_Util
1.44 -
1.45 -val meta_mp = @{thm meta_mp};
1.46 -
1.47 -fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl,
1.48 - tac, REPEAT_DETERM_N (n - k) o etac thin_rl]);
1.49 -
1.50 -fun unfold_thms_tac _ [] = all_tac
1.51 - | unfold_thms_tac ctxt thms = Local_Defs.unfold_tac ctxt (distinct Thm.eq_thm_prop thms);
1.52 -
1.53 -fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P});
1.54 -
1.55 -fun mk_nchotomy_tac n exhaust =
1.56 - HEADGOAL (rtac allI THEN' rtac exhaust THEN'
1.57 - EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n)));
1.58 -
1.59 -fun mk_unique_disc_def_tac m uexhaust =
1.60 - HEADGOAL (EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl]);
1.61 -
1.62 -fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct uexhaust =
1.63 - HEADGOAL (EVERY' ([rtac (other_disc_def RS @{thm arg_cong[of _ _ Not]} RS trans),
1.64 - rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
1.65 - hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
1.66 - rtac distinct, rtac uexhaust] @
1.67 - (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
1.68 - |> k = 1 ? swap |> op @)));
1.69 -
1.70 -fun mk_half_disc_exclude_tac ctxt m discD disc' =
1.71 - HEADGOAL (dtac discD THEN' REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
1.72 - rtac disc');
1.73 -
1.74 -fun mk_other_half_disc_exclude_tac half = HEADGOAL (etac @{thm contrapos_pn} THEN' etac half);
1.75 -
1.76 -fun mk_disc_or_sel_exhaust_tac n exhaust destIs =
1.77 - HEADGOAL (rtac exhaust THEN'
1.78 - EVERY' (map2 (fn k => fn destI => dtac destI THEN'
1.79 - select_prem_tac n (etac meta_mp) k THEN' atac) (1 upto n) destIs));
1.80 -
1.81 -val mk_disc_exhaust_tac = mk_disc_or_sel_exhaust_tac;
1.82 -
1.83 -fun mk_sel_exhaust_tac n disc_exhaust collapses =
1.84 - mk_disc_or_sel_exhaust_tac n disc_exhaust collapses ORELSE
1.85 - HEADGOAL (etac meta_mp THEN' resolve_tac collapses);
1.86 -
1.87 -fun mk_collapse_tac ctxt m discD sels =
1.88 - HEADGOAL (dtac discD THEN'
1.89 - (if m = 0 then
1.90 - atac
1.91 - else
1.92 - REPEAT_DETERM_N m o etac exE THEN' hyp_subst_tac ctxt THEN'
1.93 - SELECT_GOAL (unfold_thms_tac ctxt sels) THEN' rtac refl));
1.94 -
1.95 -fun mk_expand_tac ctxt n ms udisc_exhaust vdisc_exhaust uncollapses disc_excludesss
1.96 - disc_excludesss' =
1.97 - if ms = [0] then
1.98 - HEADGOAL (rtac (@{thm trans_sym} OF (replicate 2 (the_single uncollapses))) THEN'
1.99 - TRY o EVERY' [rtac udisc_exhaust, atac, rtac vdisc_exhaust, atac])
1.100 - else
1.101 - let val ks = 1 upto n in
1.102 - HEADGOAL (rtac udisc_exhaust THEN'
1.103 - EVERY' (map5 (fn k => fn m => fn disc_excludess => fn disc_excludess' =>
1.104 - fn uuncollapse =>
1.105 - EVERY' [rtac (uuncollapse RS trans) THEN' TRY o atac,
1.106 - rtac sym, rtac vdisc_exhaust,
1.107 - EVERY' (map4 (fn k' => fn disc_excludes => fn disc_excludes' => fn vuncollapse =>
1.108 - EVERY'
1.109 - (if k' = k then
1.110 - [rtac (vuncollapse RS trans), TRY o atac] @
1.111 - (if m = 0 then
1.112 - [rtac refl]
1.113 - else
1.114 - [if n = 1 then K all_tac else EVERY' [dtac meta_mp, atac, dtac meta_mp, atac],
1.115 - REPEAT_DETERM_N (Int.max (0, m - 1)) o etac conjE,
1.116 - asm_simp_tac (ss_only [] ctxt)])
1.117 - else
1.118 - [dtac (the_single (if k = n then disc_excludes else disc_excludes')),
1.119 - etac (if k = n then @{thm iff_contradict(1)} else @{thm iff_contradict(2)}),
1.120 - atac, atac]))
1.121 - ks disc_excludess disc_excludess' uncollapses)])
1.122 - ks ms disc_excludesss disc_excludesss' uncollapses))
1.123 - end;
1.124 -
1.125 -fun mk_case_same_ctr_tac ctxt injects =
1.126 - REPEAT_DETERM o etac exE THEN' etac conjE THEN'
1.127 - (case injects of
1.128 - [] => atac
1.129 - | [inject] => dtac (inject RS iffD1) THEN' REPEAT_DETERM o etac conjE THEN'
1.130 - hyp_subst_tac ctxt THEN' rtac refl);
1.131 -
1.132 -fun mk_case_distinct_ctrs_tac ctxt distincts =
1.133 - REPEAT_DETERM o etac exE THEN' etac conjE THEN' full_simp_tac (ss_only distincts ctxt);
1.134 -
1.135 -fun mk_case_tac ctxt n k case_def injects distinctss =
1.136 - let
1.137 - val case_def' = mk_unabs_def (n + 1) (case_def RS meta_eq_to_obj_eq);
1.138 - val ks = 1 upto n;
1.139 - in
1.140 - HEADGOAL (rtac (case_def' RS trans) THEN' rtac @{thm the_equality} THEN'
1.141 - rtac (mk_disjIN n k) THEN' REPEAT_DETERM o rtac exI THEN' rtac conjI THEN' rtac refl THEN'
1.142 - rtac refl THEN'
1.143 - EVERY' (map2 (fn k' => fn distincts =>
1.144 - (if k' < n then etac disjE else K all_tac) THEN'
1.145 - (if k' = k then mk_case_same_ctr_tac ctxt injects
1.146 - else mk_case_distinct_ctrs_tac ctxt distincts)) ks distinctss))
1.147 - end;
1.148 -
1.149 -fun mk_case_conv_if_tac ctxt n uexhaust cases discss' selss =
1.150 - HEADGOAL (rtac uexhaust THEN'
1.151 - EVERY' (map3 (fn casex => fn if_discs => fn sels =>
1.152 - EVERY' [hyp_subst_tac ctxt, SELECT_GOAL (unfold_thms_tac ctxt (if_discs @ sels)),
1.153 - rtac casex])
1.154 - cases (map2 (seq_conds if_P_or_not_P_OF n) (1 upto n) discss') selss));
1.155 -
1.156 -fun mk_case_cong_tac ctxt uexhaust cases =
1.157 - HEADGOAL (rtac uexhaust THEN'
1.158 - EVERY' (maps (fn casex => [dtac sym, asm_simp_tac (ss_only [casex] ctxt)]) cases));
1.159 -
1.160 -fun mk_split_tac ctxt uexhaust cases selss injectss distinctsss =
1.161 - HEADGOAL (rtac uexhaust) THEN
1.162 - ALLGOALS (fn k => (hyp_subst_tac ctxt THEN'
1.163 - simp_tac (ss_only (@{thms simp_thms} @ cases @ nth selss (k - 1) @ nth injectss (k - 1) @
1.164 - flat (nth distinctsss (k - 1))) ctxt)) k) THEN
1.165 - ALLGOALS (blast_tac (put_claset (claset_of @{theory_context HOL}) ctxt));
1.166 -
1.167 -val split_asm_thms = @{thms imp_conv_disj de_Morgan_conj de_Morgan_disj not_not not_ex};
1.168 -
1.169 -fun mk_split_asm_tac ctxt split =
1.170 - HEADGOAL (rtac (split RS trans)) THEN unfold_thms_tac ctxt split_asm_thms THEN
1.171 - HEADGOAL (rtac refl);
1.172 -
1.173 -end;
1.174 -
1.175 -structure Ctr_Sugar_General_Tactics: CTR_SUGAR_GENERAL_TACTICS = Ctr_Sugar_Tactics;