--- a/src/HOL/Codatatype/Tools/bnf_fp.ML Thu Sep 20 13:32:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp.ML Thu Sep 20 17:25:07 2012 +0200
@@ -20,8 +20,10 @@
val coinductN: string
val coiterN: string
val coitersN: string
+ val coiter_iffN: string
val corecN: string
val corecsN: string
+ val corec_iffN: string
val disc_coitersN: string
val disc_corecsN: string
val exhaustN: string
@@ -237,6 +239,9 @@
val discN = "disc"
val disc_coitersN = discN ^ "_" ^ coitersN
val disc_corecsN = discN ^ "_" ^ corecsN
+val iffN = "_iff"
+val coiter_iffN = coiterN ^ iffN
+val corec_iffN = corecN ^ iffN
val selN = "sel"
val sel_coitersN = selN ^ "_" ^ coitersN
val sel_corecsN = selN ^ "_" ^ corecsN
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Thu Sep 20 13:32:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Thu Sep 20 17:25:07 2012 +0200
@@ -777,6 +777,16 @@
(coiter_thmss, corec_thmss, safe_coiter_thmss, safe_corec_thmss)
end;
+ val (coiter_iff_thmss, corec_iff_thmss) =
+ let
+ (* TODO: smoothly handle the n = 1 case *)
+
+ val coiter_iff_thmss = [];
+ val corec_iff_thmss = [];
+ in
+ (coiter_iff_thmss, corec_iff_thmss)
+ end;
+
fun mk_disc_coiter_like_thms coiter_likes discIs =
map (op RS) (filter_out (is_triv_implies o snd) (coiter_likes ~~ discIs));
@@ -821,10 +831,12 @@
val notes =
[(coinductN, map single coinduct_thms, []), (* FIXME: attribs *)
(coitersN, coiter_thmss, []),
+ (coiter_iffN, coiter_iff_thmss, simp_attrs),
+ (corecsN, corec_thmss, []),
+ (corec_iffN, corec_iff_thmss, simp_attrs),
(disc_coitersN, disc_coiter_thmss, simp_attrs),
+ (disc_corecsN, disc_corec_thmss, simp_attrs),
(sel_coitersN, sel_coiter_thmss, simp_attrs),
- (corecsN, corec_thmss, []),
- (disc_corecsN, disc_corec_thmss, simp_attrs),
(sel_corecsN, sel_corec_thmss, simp_attrs),
(simpsN, simp_thmss, [])]
|> maps (fn (thmN, thmss, attrs) =>
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Thu Sep 20 13:32:48 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML Thu Sep 20 17:25:07 2012 +0200
@@ -9,6 +9,8 @@
sig
val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
val mk_coiter_like_tac: thm list -> thm list -> thm -> thm -> thm -> Proof.context -> tactic
+ val mk_coiter_like_iff_tac: Proof.context -> int -> int -> thm list -> thm list ->
+ thm list list -> tactic
val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm ->
tactic
@@ -78,15 +80,23 @@
iter_like_thms) THEN unfold_defs_tac ctxt @{thms id_def} THEN rtac refl 1;
val coiter_like_ss = ss_only @{thms if_True if_False};
-val coiter_like_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases};
+val coiter_like_unfold_thms = @{thms id_apply map_pair_def sum_map.simps prod.cases};
fun mk_coiter_like_tac coiter_like_defs map_ids fld_unf_coiter_like pre_map_def ctr_def ctxt =
unfold_defs_tac ctxt (ctr_def :: coiter_like_defs) THEN
subst_tac ctxt [fld_unf_coiter_like] 1 THEN asm_simp_tac coiter_like_ss 1 THEN
- unfold_defs_tac ctxt (pre_map_def :: coiter_like_thms @ map_ids) THEN
+ unfold_defs_tac ctxt (pre_map_def :: coiter_like_unfold_thms @ map_ids) THEN
unfold_defs_tac ctxt @{thms id_def} THEN
TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
+fun mk_coiter_like_iff_tac ctxt n k case_splits' coiter_like_thms distinctss =
+ EVERY (map4 (fn k' => fn case_split_tac => fn coiter_like_thm => fn distincts =>
+ case_split_tac 1 THEN
+ unfold_defs_tac ctxt [coiter_like_thm] THEN
+ asm_simp_tac (ss_only @{thms simp_thms(7,8,12,14,22,24)}) 1 THEN
+ (if k' = k then all_tac else rtac (the_single distincts) 1))
+ (1 upto n) (map rtac case_splits' @ [K all_tac]) coiter_like_thms distinctss);
+
val solve_prem_prem_tac =
REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
hyp_subst_tac ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'