src/HOL/BNF/Tools/bnf_gfp_tactics.ML
changeset 49581 4e5bd3883429
parent 49545 8bb6e2d7346b
child 49585 5c4a12550491
     1.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Wed Sep 26 10:00:59 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Wed Sep 26 10:00:59 2012 +0200
     1.3 @@ -37,14 +37,14 @@
     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_dtor_coinduct_tac: int -> int list -> thm -> thm -> tactic
     1.8 +  val mk_dtor_map_coinduct_tac: int -> int list -> thm -> thm -> tactic
     1.9 +  val mk_dtor_map_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm ->
    1.10 +    thm -> thm -> tactic
    1.11    val mk_dtor_srel_coinduct_tac: 'a list -> thm -> thm -> tactic
    1.12    val mk_dtor_srel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm ->
    1.13      thm list -> thm list -> tactic
    1.14    val mk_dtor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
    1.15      thm list -> thm list -> thm list list -> tactic
    1.16 -  val mk_dtor_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm ->
    1.17 -    thm -> thm -> tactic
    1.18    val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list ->
    1.19      {prems: 'a, context: Proof.context} -> tactic
    1.20    val mk_equiv_lsbis_tac: thm -> thm -> thm -> thm -> thm -> thm -> tactic
    1.21 @@ -1144,7 +1144,7 @@
    1.22      rtac impI, REPEAT_DETERM o etac conjE,
    1.23      CONJ_WRAP' (K (rtac impI THEN' etac mp THEN' etac disjI1)) srel_Ids] 1;
    1.24  
    1.25 -fun mk_dtor_coinduct_tac m ks raw_coind bis_def =
    1.26 +fun mk_dtor_map_coinduct_tac m ks raw_coind bis_def =
    1.27    let
    1.28      val n = length ks;
    1.29    in
    1.30 @@ -1165,8 +1165,8 @@
    1.31          rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1
    1.32    end;
    1.33  
    1.34 -fun mk_dtor_strong_coinduct_tac ks cTs cts dtor_coinduct bis_def bis_diag =
    1.35 -  EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_coinduct),
    1.36 +fun mk_dtor_map_strong_coinduct_tac ks cTs cts dtor_map_coinduct bis_def bis_diag =
    1.37 +  EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_map_coinduct),
    1.38      EVERY' (map (fn i =>
    1.39        EVERY' [etac disjE, REPEAT_DETERM o dtac @{thm meta_spec}, etac @{thm meta_mp},
    1.40          atac, rtac rev_mp, rtac subst, rtac bis_def, rtac bis_diag,