--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 04 16:17:22 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 04 16:27:27 2012 +0200
@@ -185,11 +185,13 @@
mk_inject_tac ctxt ctr_def fld_inject])
ms ctr_defs;
+ val half_distinct_tacss =
+ map (map (fn (def, def') => fn {context = ctxt, ...} =>
+ mk_half_distinct_tac ctxt fld_inject [def, def'])) (mk_half_pairss ctr_defs);
+
(*###*)
fun cheat_tac {context = ctxt, ...} = Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt);
- val half_distinct_tacss = map (map (K cheat_tac)) (mk_half_pairss ks);
-
val case_tacs = map (K cheat_tac) ks;
val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Tue Sep 04 16:17:22 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Tue Sep 04 16:27:27 2012 +0200
@@ -10,6 +10,7 @@
val mk_exhaust_tac: Proof.context -> int -> int list -> thm list -> thm -> thm -> tactic
val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
-> tactic
+ val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
val mk_inject_tac: Proof.context -> thm -> thm -> tactic
end;
@@ -34,6 +35,10 @@
SELECT_GOAL (Local_Defs.unfold_tac ctxt [th]) THEN'
atac) [rev cTs, cTs] [cunf, cfld] [unf_fld, fld_unf])) 1;
+fun mk_half_distinct_tac ctxt fld_inject ctr_defs =
+ Local_Defs.unfold_tac ctxt (fld_inject :: @{thms sum.inject} @ ctr_defs) THEN
+ rtac @{thm sum.distinct(1)} 1;
+
fun mk_inject_tac ctxt ctr_def fld_inject =
Local_Defs.unfold_tac ctxt [ctr_def] THEN
rtac (fld_inject RS ssubst) 1 THEN