# HG changeset patch
# User blanchet
# Date 1347131066 -7200
# Node ID 975ccb0130cbb781fe7b920dd448bdb3e6567fc1
# Parent  ca59649170b0738e7cd65c0dced3f8a28398a9c0
some work on coiter tactic

diff -r ca59649170b0 -r 975ccb0130cb src/HOL/Codatatype/Tools/bnf_fp_sugar.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
@@ -21,8 +21,8 @@
 open BNF_FP_Sugar_Tactics
 
 val caseN = "case";
-val coitersN = "iters";
-val corecsN = "recs";
+val coitersN = "coiters";
+val corecsN = "corecs";
 val itersN = "iters";
 val recsN = "recs";
 
@@ -480,9 +480,14 @@
               map7 (map3 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss cgsss;
             val goal_corecss =
               map7 (map3 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss chsss;
+
+            val coiter_tacss =
+              map3 (map oo mk_coiter_like_tac coiter_defs) fp_iter_thms pre_map_defs ctr_defss;
           in
-            (map (map (Skip_Proof.make_thm (Proof_Context.theory_of lthy))) goal_coiterss,
-             map (map (Skip_Proof.make_thm (Proof_Context.theory_of lthy))) goal_coiterss (*### goal_corecss*))
+            (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
+               goal_coiterss coiter_tacss,
+             map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
+               goal_coiterss coiter_tacss (* TODO: should be corecs *))
           end;
 
         val notes =
diff -r ca59649170b0 -r 975ccb0130cb src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
@@ -8,6 +8,7 @@
 signature BNF_FP_SUGAR_TACTICS =
 sig
   val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
+  val mk_coiter_like_tac: thm list -> thm -> thm -> thm -> Proof.context -> 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
@@ -56,4 +57,14 @@
   Local_Defs.unfold_tac ctxt (ctr_def :: pre_map_def :: iter_like_defs @ fld_iter_likes) THEN
   Local_Defs.unfold_tac ctxt iter_like_thms THEN rtac refl 1;
 
+val coiter_like_ss = ss_only @{thms if_True if_False};
+val coiter_like_thms = @{thms sum_map.simps map_pair_def id_def prod.cases};
+
+fun mk_coiter_like_tac coiter_like_defs fld_unf_coiter_like pre_map_def ctr_def ctxt =
+  Local_Defs.unfold_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
+  Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms) THEN
+  rtac refl 1;
+
 end;
diff -r ca59649170b0 -r 975ccb0130cb src/HOL/Codatatype/Tools/bnf_gfp.ML
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sat Sep 08 21:04:26 2012 +0200
@@ -2126,7 +2126,7 @@
     val fld_exhaust_thms = map (fn thm => thm RS exE) fld_nchotomy_thms;
 
     val fld_coiter_thms = map3 (fn unf_inject => fn coiter => fn unf_fld =>
-      iffD1 OF [unf_inject, trans  OF [coiter, unf_fld RS sym]])
+      iffD1 OF [unf_inject, trans OF [coiter, unf_fld RS sym]])
       unf_inject_thms coiter_thms unf_fld_thms;
 
     val timer = time (timer "fld definitions & thms");
@@ -3000,8 +3000,8 @@
             ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
           bs thmss)
   in
-    ((unfs, flds, coiters, corecs, unf_fld_thms, fld_unf_thms, fld_inject_thms, coiter_thms,
-      corec_thms),
+    ((unfs, flds, coiters, corecs, unf_fld_thms, fld_unf_thms, fld_inject_thms, fld_coiter_thms,
+      corec_thms (* FIXME: should be "fld_corec_thms" *)),
      lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
   end;
 
diff -r ca59649170b0 -r 975ccb0130cb src/HOL/Codatatype/Tools/bnf_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
@@ -8,6 +8,8 @@
 
 signature BNF_TACTICS =
 sig
+  val ss_only: thm list -> simpset
+
   val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
   val fo_rtac: thm -> Proof.context -> int -> tactic
   val subst_asm_tac: Proof.context -> thm list -> int -> tactic
@@ -56,6 +58,8 @@
 
 open BNF_Util
 
+fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms;
+
 val set_mp = @{thm set_mp};
 
 fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl,
diff -r ca59649170b0 -r 975ccb0130cb src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
@@ -29,8 +29,6 @@
 
 fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P});
 
-fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms
-
 fun mk_nchotomy_tac n exhaust =
   (rtac allI THEN' rtac exhaust THEN'
    EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1;