1.1 --- a/src/HOL/BNF_FP_Base.thy Sat Jul 05 20:51:24 2014 +0200
1.2 +++ b/src/HOL/BNF_FP_Base.thy Mon Jul 07 16:06:46 2014 +0200
1.3 @@ -13,6 +13,12 @@
1.4 imports BNF_Comp Basic_BNFs
1.5 begin
1.6
1.7 +lemma False_imp_eq_True: "(False \<Longrightarrow> Q) \<equiv> Trueprop True"
1.8 + by default simp_all
1.9 +
1.10 +lemma conj_imp_eq_imp_imp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)"
1.11 + by default simp_all
1.12 +
1.13 lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
1.14 by auto
1.15
2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sat Jul 05 20:51:24 2014 +0200
2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Jul 07 16:06:46 2014 +0200
2.3 @@ -111,6 +111,9 @@
2.4 fun merge data : T = Symtab.merge (K true) data;
2.5 );
2.6
2.7 +fun choose_relator Rs AB = find_first
2.8 + (fastype_of #> binder_types #> (fn [T1, T2] => AB = (T1, T2))) Rs;
2.9 +
2.10 fun fp_sugar_of ctxt =
2.11 Symtab.lookup (Data.get (Context.Proof ctxt))
2.12 #> Option.map (transfer_fp_sugar ctxt);
2.13 @@ -472,12 +475,9 @@
2.14 ||>> mk_Freesss "a" ctrAs_Tsss
2.15 ||>> mk_Freesss "b" ctrBs_Tsss;
2.16
2.17 - fun choose_relator AB = the (find_first
2.18 - (fastype_of #> binder_types #> (fn [T1, T2] => AB = (T1, T2))) (Rs @ IRs));
2.19 -
2.20 val premises =
2.21 let
2.22 - fun build_the_rel A B = build_rel lthy fpA_Ts choose_relator (A, B);
2.23 + fun build_the_rel A B = build_rel lthy fpA_Ts (the o choose_relator (Rs @ IRs)) (A, B);
2.24 fun build_rel_app a b = build_the_rel (fastype_of a) (fastype_of b) $ a $ b;
2.25
2.26 fun mk_prem ctrA ctrB argAs argBs =
2.27 @@ -489,8 +489,8 @@
2.28 flat (map4 (map4 mk_prem) ctrAss ctrBss ctrAsss ctrBsss)
2.29 end;
2.30
2.31 - val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
2.32 - (map2 mk_leq (map (build_rel lthy [] choose_relator) (fpA_Ts ~~ fpB_Ts)) IRs));
2.33 + val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq
2.34 + (map (build_rel lthy [] (the o choose_relator (Rs @ IRs))) (fpA_Ts ~~ fpB_Ts)) IRs));
2.35
2.36 val rel_induct0_thm = Goal.prove_sorry lthy [] premises goal
2.37 (fn {context = ctxt, prems = prems} =>
2.38 @@ -725,12 +725,9 @@
2.39 (mk_discss fpBs Bs, mk_selsss fpBs Bs))
2.40 end;
2.41
2.42 - fun choose_relator AB = the (find_first
2.43 - (fastype_of #> binder_types #> (fn [T1, T2] => AB = (T1, T2))) (Rs @ IRs));
2.44 -
2.45 val premises =
2.46 let
2.47 - fun build_the_rel A B = build_rel lthy fpA_Ts choose_relator (A, B);
2.48 + fun build_the_rel A B = build_rel lthy fpA_Ts (the o choose_relator (Rs @ IRs)) (A, B);
2.49
2.50 fun build_rel_app selA_t selB_t =
2.51 (build_the_rel (fastype_of selA_t) (fastype_of selB_t )) $ selA_t $ selB_t
2.52 @@ -755,8 +752,8 @@
2.53 map8 mk_prem IRs fpAs fpBs ns discA_tss selA_tsss discB_tss selB_tsss
2.54 end;
2.55
2.56 - val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
2.57 - (map2 mk_leq IRs (map (build_rel lthy [] choose_relator) (fpA_Ts ~~ fpB_Ts))));
2.58 + val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj (map2 mk_leq
2.59 + IRs (map (build_rel lthy [] (the o choose_relator (Rs @ IRs))) (fpA_Ts ~~ fpB_Ts))));
2.60
2.61 val rel_coinduct0_thm = Goal.prove_sorry lthy [] premises goal
2.62 (fn {context = ctxt, prems = prems} =>
2.63 @@ -1259,7 +1256,7 @@
2.64 end;
2.65
2.66 fun derive_maps_sets_rels (ctr_sugar as {case_cong, discs, selss, ctrs, exhaust, disc_thmss,
2.67 - sel_thmss, ...} : ctr_sugar, lthy) =
2.68 + sel_thmss, injects, distincts, ...} : ctr_sugar, lthy) =
2.69 if live = 0 then
2.70 ((([], [], [], []), ctr_sugar), lthy)
2.71 else
2.72 @@ -1314,14 +1311,93 @@
2.73
2.74 val sets = map (mk_set (snd (Term.dest_Type fpT))) (sets_of_bnf fp_bnf);
2.75
2.76 - val (disc_map_iff_thms, sel_map_thms, sel_set_thms) =
2.77 + val set_empty_thms =
2.78 + let
2.79 + val ctr_argT_namess = map ((fn Ts => fold Term.add_tfree_namesT Ts []) o
2.80 + binder_types o fastype_of) ctrs;
2.81 + val setTs = map (HOLogic.dest_setT o range_type o fastype_of) sets;
2.82 + val setT_names = map (fn T => the_single (Term.add_tfree_namesT T [])) setTs;
2.83 +
2.84 + fun mk_set_empty_goal disc set T =
2.85 + Logic.mk_implies (HOLogic.mk_Trueprop (disc $ u),
2.86 + mk_Trueprop_eq (set $ u, HOLogic.mk_set T []));
2.87 +
2.88 + val goals =
2.89 + if null discs then
2.90 + []
2.91 + else
2.92 + map_filter I (flat
2.93 + (map2 (fn names => fn disc =>
2.94 + map3 (fn name => fn setT => fn set =>
2.95 + if member (op =) names name then NONE
2.96 + else SOME (mk_set_empty_goal disc set setT))
2.97 + setT_names setTs sets)
2.98 + ctr_argT_namess discs));
2.99 + in
2.100 + if null goals then
2.101 + []
2.102 + else
2.103 + Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
2.104 + (fn {context = ctxt, prems = _} =>
2.105 + mk_set_empty_tac ctxt (certify ctxt u) exhaust set_thms (flat disc_thmss))
2.106 + |> Conjunction.elim_balanced (length goals)
2.107 + |> Proof_Context.export names_lthy lthy
2.108 + end;
2.109 +
2.110 + val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns);
2.111 +
2.112 + fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
2.113 + fold_thms lthy ctr_defs'
2.114 + (unfold_thms lthy (pre_rel_def :: abs_inverse ::
2.115 + (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @
2.116 + @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]})
2.117 + (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
2.118 + |> postproc
2.119 + |> singleton (Proof_Context.export names_lthy no_defs_lthy);
2.120 +
2.121 + fun mk_rel_inject_thm ((ctr_def', cxIn), (_, cyIn)) =
2.122 + mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] cxIn cyIn;
2.123 +
2.124 + fun mk_rel_intro_thm thm =
2.125 + let
2.126 + fun impl thm = rotate_prems (~1) (impl (rotate_prems 1 (conjI RS thm)))
2.127 + handle THM _ => thm
2.128 + in
2.129 + impl (thm RS iffD2)
2.130 + handle THM _ => thm
2.131 + end;
2.132 +
2.133 + fun mk_half_rel_distinct_thm ((xctr_def', cxIn), (yctr_def', cyIn)) =
2.134 + mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def']
2.135 + cxIn cyIn;
2.136 +
2.137 + fun mk_other_half_rel_distinct_thm thm =
2.138 + flip_rels lthy live thm
2.139 + RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2);
2.140 +
2.141 + val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos);
2.142 + val rel_intro_thms = map mk_rel_intro_thm rel_inject_thms;
2.143 +
2.144 + val half_rel_distinct_thmss =
2.145 + map (map mk_half_rel_distinct_thm) (mk_half_pairss rel_infos);
2.146 + val other_half_rel_distinct_thmss =
2.147 + map (map mk_other_half_rel_distinct_thm) half_rel_distinct_thmss;
2.148 + val (rel_distinct_thms, _) =
2.149 + join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss;
2.150 +
2.151 + val rel_eq_thms =
2.152 + map (fn th => th RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms @
2.153 + map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th)
2.154 + rel_inject_thms ms;
2.155 +
2.156 + val (disc_map_iff_thms, sel_map_thms, sel_set_thms, (rel_cases_thm, rel_cases_attrs)) =
2.157 let
2.158 val (((Ds, As), Bs), names_lthy) = lthy
2.159 |> mk_TFrees (dead_of_bnf fp_bnf)
2.160 ||>> mk_TFrees (live_of_bnf fp_bnf)
2.161 ||>> mk_TFrees (live_of_bnf fp_bnf);
2.162 val TA as Type (_, ADs) = mk_T_of_bnf Ds As fp_bnf;
2.163 - val Type (_, BDs) = mk_T_of_bnf Ds Bs fp_bnf;
2.164 + val TB as Type (_, BDs) = mk_T_of_bnf Ds Bs fp_bnf;
2.165 val fTs = map2 (curry op -->) As Bs;
2.166 val ((fs, ta), names_lthy) = names_lthy
2.167 |> mk_Frees "f" fTs
2.168 @@ -1331,6 +1407,60 @@
2.169 val selssA = map (map (mk_disc_or_sel ADs)) selss;
2.170 val disc_sel_pairs = flat (map2 (map o pair) discsA selssA);
2.171
2.172 + val (rel_cases_thm, rel_cases_attrs) =
2.173 + let
2.174 + val rel = mk_rel_of_bnf Ds As Bs fp_bnf;
2.175 + val (((thesis, Rs), tb), names_lthy) = names_lthy
2.176 + |> yield_singleton (mk_Frees "thesis") HOLogic.boolT
2.177 + |>> HOLogic.mk_Trueprop
2.178 + ||>> mk_Frees "R" (map2 mk_pred2T As Bs)
2.179 + ||>> yield_singleton (mk_Frees "b") TB;
2.180 +
2.181 + val _ = apfst HOLogic.mk_Trueprop;
2.182 + val rel_Rs_a_b = list_comb (rel, Rs) $ ta $ tb;
2.183 + val ctrAs = map (mk_ctr ADs) ctrs;
2.184 + val ctrBs = map (mk_ctr BDs) ctrs;
2.185 +
2.186 + fun mk_assms ctrA ctrB ctxt =
2.187 + let
2.188 + val argA_Ts = binder_types (fastype_of ctrA);
2.189 + val argB_Ts = binder_types (fastype_of ctrB);
2.190 + val ((argAs, argBs), names_ctxt) = ctxt
2.191 + |> mk_Frees "x" argA_Ts
2.192 + ||>> mk_Frees "y" argB_Ts;
2.193 + val ctrA_args = list_comb (ctrA, argAs);
2.194 + val ctrB_args = list_comb (ctrB, argBs);
2.195 + fun build_the_rel A B =
2.196 + build_rel lthy [] (the o choose_relator Rs) (A, B);
2.197 + fun build_rel_app a b =
2.198 + build_the_rel (fastype_of a) (fastype_of b) $ a $ b;
2.199 + in
2.200 + (fold_rev Logic.all (argAs @ argBs) (Logic.list_implies
2.201 + (mk_Trueprop_eq (ta, ctrA_args) ::
2.202 + mk_Trueprop_eq (tb, ctrB_args) ::
2.203 + map2 (HOLogic.mk_Trueprop oo build_rel_app) argAs argBs,
2.204 + thesis)),
2.205 + names_ctxt)
2.206 + end;
2.207 +
2.208 + val (assms, names_lthy) = fold_map2 mk_assms ctrAs ctrBs names_lthy;
2.209 + val goal = Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms,
2.210 + thesis);
2.211 + val thm = Goal.prove_sorry lthy [] [] goal
2.212 + (fn {context = ctxt, prems = _} =>
2.213 + mk_rel_cases_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
2.214 + injects rel_inject_thms distincts rel_distinct_thms)
2.215 + |> singleton (Proof_Context.export names_lthy lthy)
2.216 + |> Thm.close_derivation;
2.217 +
2.218 + val ctr_names = quasi_unambiguous_case_names ((map name_of_ctr) ctrAs);
2.219 + val case_names_attr = Attrib.internal (K (Rule_Cases.case_names ctr_names));
2.220 + val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1));
2.221 + val cases_pred_attr = Attrib.internal o K o Induct.cases_pred;
2.222 + in
2.223 + (thm, [consumes_attr, case_names_attr, cases_pred_attr ""])
2.224 + end;
2.225 +
2.226 val disc_map_iff_thms =
2.227 let
2.228 val discsB = map (mk_disc_or_sel BDs) discs;
2.229 @@ -1453,88 +1583,9 @@
2.230 |> Proof_Context.export names_lthy lthy
2.231 end;
2.232 in
2.233 - (disc_map_iff_thms, sel_map_thms, sel_set_thms)
2.234 + (disc_map_iff_thms, sel_map_thms, sel_set_thms, (rel_cases_thm, rel_cases_attrs))
2.235 end;
2.236
2.237 - val set_empty_thms =
2.238 - let
2.239 - val ctr_argT_namess = map ((fn Ts => fold Term.add_tfree_namesT Ts []) o
2.240 - binder_types o fastype_of) ctrs;
2.241 - val setTs = map (HOLogic.dest_setT o range_type o fastype_of) sets;
2.242 - val setT_names = map (fn T => the_single (Term.add_tfree_namesT T [])) setTs;
2.243 -
2.244 - fun mk_set_empty_goal disc set T =
2.245 - Logic.mk_implies (HOLogic.mk_Trueprop (disc $ u),
2.246 - mk_Trueprop_eq (set $ u, HOLogic.mk_set T []));
2.247 -
2.248 - val goals =
2.249 - if null discs then
2.250 - []
2.251 - else
2.252 - map_filter I (flat
2.253 - (map2 (fn names => fn disc =>
2.254 - map3 (fn name => fn setT => fn set =>
2.255 - if member (op =) names name then NONE
2.256 - else SOME (mk_set_empty_goal disc set setT))
2.257 - setT_names setTs sets)
2.258 - ctr_argT_namess discs));
2.259 - in
2.260 - if null goals then
2.261 - []
2.262 - else
2.263 - Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals)
2.264 - (fn {context = ctxt, prems = _} =>
2.265 - mk_set_empty_tac ctxt (certify ctxt u) exhaust set_thms (flat disc_thmss))
2.266 - |> Conjunction.elim_balanced (length goals)
2.267 - |> Proof_Context.export names_lthy lthy
2.268 - end;
2.269 -
2.270 - val rel_infos = (ctr_defs' ~~ cxIns, ctr_defs' ~~ cyIns);
2.271 -
2.272 - fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
2.273 - fold_thms lthy ctr_defs'
2.274 - (unfold_thms lthy (pre_rel_def :: abs_inverse ::
2.275 - (if fp = Least_FP then [] else [dtor_ctor]) @ sumprod_thms_rel @
2.276 - @{thms vimage2p_def sum.inject sum.distinct(1)[THEN eq_False[THEN iffD2]]})
2.277 - (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
2.278 - |> postproc
2.279 - |> singleton (Proof_Context.export names_lthy no_defs_lthy);
2.280 -
2.281 - fun mk_rel_inject_thm ((ctr_def', cxIn), (_, cyIn)) =
2.282 - mk_rel_thm (unfold_thms lthy @{thms eq_sym_Unity_conv}) [ctr_def'] cxIn cyIn;
2.283 -
2.284 - fun mk_rel_intro_thm thm =
2.285 - let
2.286 - fun impl thm = rotate_prems (~1) (impl (rotate_prems 1 (conjI RS thm)))
2.287 - handle THM _ => thm
2.288 - in
2.289 - impl (thm RS iffD2)
2.290 - handle THM _ => thm
2.291 - end;
2.292 -
2.293 - fun mk_half_rel_distinct_thm ((xctr_def', cxIn), (yctr_def', cyIn)) =
2.294 - mk_rel_thm (fn thm => thm RS @{thm eq_False[THEN iffD1]}) [xctr_def', yctr_def']
2.295 - cxIn cyIn;
2.296 -
2.297 - fun mk_other_half_rel_distinct_thm thm =
2.298 - flip_rels lthy live thm
2.299 - RS (rel_flip RS sym RS @{thm arg_cong[of _ _ Not]} RS iffD2);
2.300 -
2.301 - val rel_inject_thms = map mk_rel_inject_thm (op ~~ rel_infos);
2.302 - val rel_intro_thms = map mk_rel_intro_thm rel_inject_thms;
2.303 -
2.304 - val half_rel_distinct_thmss =
2.305 - map (map mk_half_rel_distinct_thm) (mk_half_pairss rel_infos);
2.306 - val other_half_rel_distinct_thmss =
2.307 - map (map mk_other_half_rel_distinct_thm) half_rel_distinct_thmss;
2.308 - val (rel_distinct_thms, _) =
2.309 - join_halves n half_rel_distinct_thmss other_half_rel_distinct_thmss;
2.310 -
2.311 - val rel_eq_thms =
2.312 - map (fn th => th RS @{thm eq_False[THEN iffD2]}) rel_distinct_thms @
2.313 - map2 (fn th => fn 0 => th RS @{thm eq_True[THEN iffD2]} | _ => th)
2.314 - rel_inject_thms ms;
2.315 -
2.316 val anonymous_notes =
2.317 [([case_cong], fundefcong_attrs),
2.318 (rel_eq_thms, code_nitpicksimp_attrs)]
2.319 @@ -1543,6 +1594,7 @@
2.320 val notes =
2.321 [(disc_map_iffN, disc_map_iff_thms, simp_attrs),
2.322 (mapN, map_thms, code_nitpicksimp_attrs @ simp_attrs),
2.323 + (rel_casesN, [rel_cases_thm], rel_cases_attrs),
2.324 (rel_distinctN, rel_distinct_thms, simp_attrs),
2.325 (rel_injectN, rel_inject_thms, simp_attrs),
2.326 (rel_introsN, rel_intro_thms, []),
3.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Sat Jul 05 20:51:24 2014 +0200
3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Mon Jul 07 16:06:46 2014 +0200
3.3 @@ -26,6 +26,8 @@
3.4 val mk_inject_tac: Proof.context -> thm -> thm -> thm -> tactic
3.5 val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
3.6 tactic
3.7 + val mk_rel_cases_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list ->
3.8 + thm list -> thm list -> tactic
3.9 val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list ->
3.10 thm list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
3.11 thm list -> thm list -> thm list -> tactic
3.12 @@ -211,6 +213,17 @@
3.13 (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
3.14 selsss));
3.15
3.16 +fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts =
3.17 + HEADGOAL (rtac (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW
3.18 + rtac (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW
3.19 + hyp_subst_tac ctxt) THEN
3.20 + Local_Defs.unfold_tac ctxt (injects @ rel_injects @ @{thms conj_imp_eq_imp_imp simp_thms(6)
3.21 + True_implies_equals conj_imp_eq_imp_imp} @
3.22 + map (fn thm => iffD2 OF [@{thm eq_False}, thm]) (distincts @ rel_distincts) @
3.23 + map (fn thm => thm RS @{thm eqTrueI}) rel_injects) THEN
3.24 + TRYALL (atac ORELSE' etac FalseE ORELSE' (REPEAT_DETERM o dtac @{thm meta_spec} THEN'
3.25 + REPEAT_DETERM o (dtac @{thm meta_mp} THEN' rtac refl) THEN' Goal.assume_rule_tac ctxt));
3.26 +
3.27 fun mk_rel_coinduct0_tac ctxt dtor_rel_coinduct cts assms exhausts discss selss ctor_defss
3.28 dtor_ctors ctor_injects abs_injects rel_pre_defs abs_inverses nesting_rel_eqs =
3.29 rtac dtor_rel_coinduct 1 THEN
4.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Sat Jul 05 20:51:24 2014 +0200
4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Jul 07 16:06:46 2014 +0200
4.3 @@ -124,6 +124,7 @@
4.4 val morN: string
4.5 val nchotomyN: string
4.6 val recN: string
4.7 + val rel_casesN: string
4.8 val rel_coinductN: string
4.9 val rel_inductN: string
4.10 val rel_injectN: string
4.11 @@ -406,6 +407,7 @@
4.12 val distinctN = "distinct"
4.13 val rel_distinctN = relN ^ "_" ^ distinctN
4.14 val injectN = "inject"
4.15 +val rel_casesN = relN ^ "_cases"
4.16 val rel_injectN = relN ^ "_" ^ injectN
4.17 val rel_introsN = relN ^ "_intros"
4.18 val rel_coinductN = relN ^ "_" ^ coinductN
5.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Sat Jul 05 20:51:24 2014 +0200
5.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_tactics.ML Mon Jul 07 16:06:46 2014 +0200
5.3 @@ -54,7 +54,7 @@
5.4
5.5 fun mk_nchotomy_tac n exhaust =
5.6 HEADGOAL (rtac allI THEN' rtac exhaust THEN'
5.7 - EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n)));
5.8 + EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n)));
5.9
5.10 fun mk_unique_disc_def_tac m uexhaust =
5.11 HEADGOAL (EVERY' [rtac iffI, rtac uexhaust, REPEAT_DETERM_N m o rtac exI, atac, rtac refl]);