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