1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Sat Sep 08 21:04:26 2012 +0200
     1.3 @@ -21,8 +21,8 @@
     1.4  open BNF_FP_Sugar_Tactics
     1.5  
     1.6  val caseN = "case";
     1.7 -val coitersN = "iters";
     1.8 -val corecsN = "recs";
     1.9 +val coitersN = "coiters";
    1.10 +val corecsN = "corecs";
    1.11  val itersN = "iters";
    1.12  val recsN = "recs";
    1.13  
    1.14 @@ -480,9 +480,14 @@
    1.15                map7 (map3 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss cgsss;
    1.16              val goal_corecss =
    1.17                map7 (map3 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss chsss;
    1.18 +
    1.19 +            val coiter_tacss =
    1.20 +              map3 (map oo mk_coiter_like_tac coiter_defs) fp_iter_thms pre_map_defs ctr_defss;
    1.21            in
    1.22 -            (map (map (Skip_Proof.make_thm (Proof_Context.theory_of lthy))) goal_coiterss,
    1.23 -             map (map (Skip_Proof.make_thm (Proof_Context.theory_of lthy))) goal_coiterss (*### goal_corecss*))
    1.24 +            (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
    1.25 +               goal_coiterss coiter_tacss,
    1.26 +             map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
    1.27 +               goal_coiterss coiter_tacss (* TODO: should be corecs *))
    1.28            end;
    1.29  
    1.30          val notes =

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
     2.3 @@ -8,6 +8,7 @@
     2.4  signature BNF_FP_SUGAR_TACTICS =
     2.5  sig
     2.6    val mk_case_tac: Proof.context -> int -> int -> int -> thm -> thm -> thm -> tactic
     2.7 +  val mk_coiter_like_tac: thm list -> thm -> thm -> thm -> Proof.context -> tactic
     2.8    val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic
     2.9    val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
    2.10      -> tactic
    2.11 @@ -56,4 +57,14 @@
    2.12    Local_Defs.unfold_tac ctxt (ctr_def :: pre_map_def :: iter_like_defs @ fld_iter_likes) THEN
    2.13    Local_Defs.unfold_tac ctxt iter_like_thms THEN rtac refl 1;
    2.14  
    2.15 +val coiter_like_ss = ss_only @{thms if_True if_False};
    2.16 +val coiter_like_thms = @{thms sum_map.simps map_pair_def id_def prod.cases};
    2.17 +
    2.18 +fun mk_coiter_like_tac coiter_like_defs fld_unf_coiter_like pre_map_def ctr_def ctxt =
    2.19 +  Local_Defs.unfold_tac ctxt (ctr_def :: coiter_like_defs) THEN
    2.20 +  subst_tac ctxt [fld_unf_coiter_like] 1 THEN
    2.21 +  asm_simp_tac coiter_like_ss 1 THEN
    2.22 +  Local_Defs.unfold_tac ctxt (pre_map_def :: coiter_like_thms) THEN
    2.23 +  rtac refl 1;
    2.24 +
    2.25  end;

     3.1 --- a/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sat Sep 08 21:04:26 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML	Sat Sep 08 21:04:26 2012 +0200
     3.3 @@ -2126,7 +2126,7 @@
     3.4      val fld_exhaust_thms = map (fn thm => thm RS exE) fld_nchotomy_thms;
     3.5  
     3.6      val fld_coiter_thms = map3 (fn unf_inject => fn coiter => fn unf_fld =>
     3.7 -      iffD1 OF [unf_inject, trans  OF [coiter, unf_fld RS sym]])
     3.8 +      iffD1 OF [unf_inject, trans OF [coiter, unf_fld RS sym]])
     3.9        unf_inject_thms coiter_thms unf_fld_thms;
    3.10  
    3.11      val timer = time (timer "fld definitions & thms");
    3.12 @@ -3000,8 +3000,8 @@
    3.13              ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
    3.14            bs thmss)
    3.15    in
    3.16 -    ((unfs, flds, coiters, corecs, unf_fld_thms, fld_unf_thms, fld_inject_thms, coiter_thms,
    3.17 -      corec_thms),
    3.18 +    ((unfs, flds, coiters, corecs, unf_fld_thms, fld_unf_thms, fld_inject_thms, fld_coiter_thms,
    3.19 +      corec_thms (* FIXME: should be "fld_corec_thms" *)),
    3.20       lthy |> Local_Theory.notes (common_notes @ notes) |> snd)
    3.21    end;
    3.22  

     4.1 --- a/src/HOL/Codatatype/Tools/bnf_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
     4.2 +++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
     4.3 @@ -8,6 +8,8 @@
     4.4  
     4.5  signature BNF_TACTICS =
     4.6  sig
     4.7 +  val ss_only: thm list -> simpset
     4.8 +
     4.9    val select_prem_tac: int -> (int -> tactic) -> int -> int -> tactic
    4.10    val fo_rtac: thm -> Proof.context -> int -> tactic
    4.11    val subst_asm_tac: Proof.context -> thm list -> int -> tactic
    4.12 @@ -56,6 +58,8 @@
    4.13  
    4.14  open BNF_Util
    4.15  
    4.16 +fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms;
    4.17 +
    4.18  val set_mp = @{thm set_mp};
    4.19  
    4.20  fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl,

     5.1 --- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
     5.2 +++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Sat Sep 08 21:04:26 2012 +0200
     5.3 @@ -29,8 +29,6 @@
     5.4  
     5.5  fun if_P_or_not_P_OF pos thm = thm RS (if pos then @{thm if_P} else @{thm if_not_P});
     5.6  
     5.7 -fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms
     5.8 -
     5.9  fun mk_nchotomy_tac n exhaust =
    5.10    (rtac allI THEN' rtac exhaust THEN'
    5.11     EVERY' (maps (fn k => [rtac (mk_disjIN n k), REPEAT_DETERM o rtac exI, atac]) (1 upto n))) 1;