src/HOL/BNF/Tools/bnf_gfp_tactics.ML
changeset 51739 3514b90d0a8b
parent 51447 a19e973fa2cf
child 51761 4c9f08836d87
     1.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Tue Apr 23 11:14:51 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Tue Apr 23 11:43:09 2013 +0200
     1.3 @@ -37,6 +37,8 @@
     1.4    val mk_congruent_str_final_tac: int -> thm -> thm -> thm -> thm list -> tactic
     1.5    val mk_corec_tac: int -> thm list -> thm -> thm -> thm list ->
     1.6      {prems: 'a, context: Proof.context} -> tactic
     1.7 +  val mk_corec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
     1.8 +    tactic
     1.9    val mk_dtor_map_coinduct_tac: int -> int list -> thm -> thm -> tactic
    1.10    val mk_dtor_map_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm ->
    1.11      thm -> thm -> tactic
    1.12 @@ -1121,6 +1123,11 @@
    1.13      REPEAT_DETERM_N m o rtac refl,
    1.14      EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
    1.15  
    1.16 +fun mk_corec_unique_mor_tac corec_defs corec_Inls unfold_unique_mor {context = ctxt, prems = _} =
    1.17 +  unfold_thms_tac ctxt
    1.18 +    (corec_defs @ map (fn thm => thm RS @{thm sum_case_expand_Inr'}) corec_Inls) THEN
    1.19 +  etac unfold_unique_mor 1;
    1.20 +
    1.21  fun mk_dtor_srel_coinduct_tac ks raw_coind bis_srel =
    1.22    EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_srel, rtac conjI,
    1.23      CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) ks,