# HG changeset patch # User blanchet # Date 1388692269 -3600 # Node ID a426e38a8a7eb86be0364ff6f1126e49816d6623 # Parent aa891e065af128c239de6e192768ff0758bc8e39 made tactic handle corner cases, where some of the 'disc' properties are missing, correctly diff -r aa891e065af1 -r a426e38a8a7e src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 02 20:25:40 2014 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Thu Jan 02 20:51:09 2014 +0100 @@ -1208,7 +1208,7 @@ [] else mk_primcorec_disc_iff_tac lthy (the_single exhaust_thms) (the_single disc_thms) - (flat disc_thmss) (flat disc_excludess) + disc_thmss (flat disc_excludess) |> K |> Goal.prove lthy [] [] goal |> Thm.close_derivation |> single diff -r aa891e065af1 -r a426e38a8a7e src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Thu Jan 02 20:25:40 2014 +0100 +++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Thu Jan 02 20:51:09 2014 +0100 @@ -12,7 +12,7 @@ val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm option -> thm list -> tactic val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list -> tactic - val mk_primcorec_disc_iff_tac: Proof.context -> thm -> thm -> thm list -> thm list -> tactic + val mk_primcorec_disc_iff_tac: Proof.context -> thm -> thm -> thm list list -> thm list -> tactic val mk_primcorec_exhaust_tac: int -> thm -> tactic val mk_primcorec_raw_code_of_ctr_tac: Proof.context -> thm list -> thm list -> thm list -> thm list -> int list -> thm list -> thm option -> tactic @@ -77,16 +77,17 @@ fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss = mk_primcorec_prelude ctxt defs disc_corec THEN mk_primcorec_cases_tac ctxt k m exclsss; -fun mk_primcorec_disc_iff_tac ctxt fun_exhaust fun_disc fun_discs disc_excludes = +fun mk_primcorec_disc_iff_tac ctxt fun_exhaust fun_disc fun_discss disc_excludes = HEADGOAL (rtac iffI THEN' rtac fun_exhaust THEN' - EVERY' (map (fn fun_disc' => - if Thm.eq_thm (fun_disc', fun_disc) then - REPEAT_DETERM o etac conjI THEN' (atac ORELSE' rtac TrueI) - else - dtac fun_disc' THEN' (REPEAT_DETERM o atac) THEN' - DETERM o (dresolve_tac disc_excludes THEN' etac notE THEN' atac)) - fun_discs) THEN' + EVERY' (map (fn [] => etac FalseE + | [fun_disc'] => + if Thm.eq_thm (fun_disc', fun_disc) then + REPEAT_DETERM o etac conjI THEN' (atac ORELSE' rtac TrueI) + else + rtac FalseE THEN' dtac fun_disc' THEN' REPEAT_DETERM o atac THEN' + DETERM o (dresolve_tac disc_excludes THEN' etac notE THEN' atac)) + fun_discss) THEN' rtac (unfold_thms ctxt [atomize_conjL] fun_disc) THEN_MAYBE' atac); fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms map_idents map_comps fun_sel k m