--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Fri Jan 10 14:39:37 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar.ML Fri Jan 10 14:39:37 2014 +0100
@@ -1237,7 +1237,7 @@
fun prove_disc_iff ({ctr_specs, ...} : corec_spec) exhaust_thms disc_thmss'
(({fun_args = exhaust_fun_args, ...} : coeqn_data_disc) :: _) disc_thms
({fun_name, fun_T, fun_args, ctr_no, prems, eqn_pos, ...} : coeqn_data_disc) =
- if null disc_thms orelse null exhaust_thms then
+ if null exhaust_thms then
[]
else
let
@@ -1247,17 +1247,14 @@
mk_conjs prems)
|> curry Logic.list_all (map dest_Free fun_args);
in
- if prems = [@{term False}] then
- []
- else
- mk_primcorec_disc_iff_tac lthy (map (fst o dest_Free) exhaust_fun_args)
- (the_single exhaust_thms) (the_single disc_thms) disc_thmss' (flat disc_excludess)
- |> K |> Goal.prove_sorry lthy [] [] goal
- |> Thm.close_derivation
- |> fold (fn rule => perhaps (try (fn thm => thm RS rule)))
- @{thms eqTrueE eq_False[THEN iffD1] notnotD}
- |> pair eqn_pos
- |> single
+ mk_primcorec_disc_iff_tac lthy (map (fst o dest_Free) exhaust_fun_args)
+ (the_single exhaust_thms) disc_thms disc_thmss' (flat disc_excludess)
+ |> K |> Goal.prove_sorry lthy [] [] goal
+ |> Thm.close_derivation
+ |> fold (fn rule => perhaps (try (fn thm => thm RS rule)))
+ @{thms eqTrueE eq_False[THEN iffD1] notnotD}
+ |> pair eqn_pos
+ |> single
end;
val disc_iff_thmss = map6 (flat ooo map2 oooo prove_disc_iff) corec_specs exhaust_thmss
--- a/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Fri Jan 10 14:39:37 2014 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_rec_sugar_tactics.ML Fri Jan 10 14:39:37 2014 +0100
@@ -12,7 +12,7 @@
val mk_primcorec_ctr_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 -> string list -> thm -> thm -> thm list list ->
+ val mk_primcorec_disc_iff_tac: Proof.context -> string list -> thm -> thm list -> thm list list ->
thm list -> tactic
val mk_primcorec_exhaust_tac: Proof.context -> string list -> int -> thm -> tactic
val mk_primcorec_nchotomy_tac: Proof.context -> thm list -> tactic
@@ -108,19 +108,20 @@
fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss =
prelude_tac ctxt defs disc_corec THEN cases_tac ctxt k m exclsss;
-fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_disc fun_discss disc_excludes =
+fun mk_primcorec_disc_iff_tac ctxt fun_exhaust_frees fun_exhaust fun_discs fun_discss
+ disc_excludes =
HEADGOAL (rtac iffI THEN'
rtac fun_exhaust THEN'
K (exhaust_inst_as_projs_tac ctxt fun_exhaust_frees) THEN'
EVERY' (map (fn [] => etac FalseE
- | [fun_disc'] =>
- if Thm.eq_thm (fun_disc', fun_disc) then
+ | fun_discs' as [fun_disc'] =>
+ if eq_list Thm.eq_thm (fun_discs', fun_discs) then
REPEAT_DETERM o etac conjI THEN' (atac ORELSE' rtac TrueI)
else
rtac FalseE THEN' rotate_tac 1 THEN' dtac fun_disc' THEN' REPEAT_DETERM o atac THEN'
dresolve_tac disc_excludes THEN' etac notE THEN' atac)
fun_discss) THEN'
- rtac (unfold_thms ctxt [atomize_conjL] fun_disc) THEN_MAYBE' atac);
+ resolve_tac (map (unfold_thms ctxt [atomize_conjL]) fun_discs) THEN_MAYBE' atac);
fun mk_primcorec_sel_tac ctxt defs distincts splits split_asms mapsx map_idents map_comps fun_sel k
m exclsss =