# HG changeset patch
# User blanchet
# Date 1348154707 -7200
# Node ID e6d6869eed08e1d003fc464fa1404d3c66f085a4
# Parent  504f0a38f608c4ec9c0dcf4743379e482474a9e8
generate coiter_iff and corec_iff theorems

diff -r 504f0a38f608 -r e6d6869eed08 src/HOL/Codatatype/Tools/bnf_fp.ML
--- 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
diff -r 504f0a38f608 -r e6d6869eed08 src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- 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) =>
diff -r 504f0a38f608 -r e6d6869eed08 src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- 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'