src/HOL/BNF/Tools/bnf_gfp_tactics.ML
changeset 49545 8bb6e2d7346b
parent 49544 24094fa47e0d
child 49581 4e5bd3883429
     1.1 --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML	Sun Sep 23 14:52:53 2012 +0200
     1.3 @@ -38,6 +38,9 @@
     1.4    val mk_corec_tac: int -> thm list -> thm -> thm -> thm list ->
     1.5      {prems: 'a, context: Proof.context} -> tactic
     1.6    val mk_dtor_coinduct_tac: int -> int list -> thm -> thm -> tactic
     1.7 +  val mk_dtor_srel_coinduct_tac: 'a list -> thm -> thm -> tactic
     1.8 +  val mk_dtor_srel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm ->
     1.9 +    thm list -> thm list -> tactic
    1.10    val mk_dtor_srel_tac: thm list -> int -> thm -> thm -> thm -> thm -> thm list -> thm -> thm ->
    1.11      thm list -> thm list -> thm list list -> tactic
    1.12    val mk_dtor_strong_coinduct_tac: int list -> ctyp option list -> cterm option list -> thm ->
    1.13 @@ -108,9 +111,6 @@
    1.14    val mk_set_rv_Lev_tac: int -> cterm option list -> thm list -> thm list -> thm list -> thm list ->
    1.15      thm list list -> thm list list -> tactic
    1.16    val mk_set_simp_tac: int -> thm -> thm -> thm list -> tactic
    1.17 -  val mk_srel_coinduct_tac: 'a list -> thm -> thm -> tactic
    1.18 -  val mk_srel_strong_coinduct_tac: int -> ctyp option list -> cterm option list -> thm ->
    1.19 -    thm list -> thm list -> tactic
    1.20    val mk_strT_hset_tac: int -> int -> int -> ctyp option list -> ctyp option list ->
    1.21      cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list ->
    1.22      thm list list -> thm list list -> thm -> thm list list -> tactic
    1.23 @@ -1123,7 +1123,7 @@
    1.24      REPEAT_DETERM_N m o rtac refl,
    1.25      EVERY' (map (fn thm => rtac @{thm sum_case_expand_Inr} THEN' rtac thm) corec_Inls)] 1;
    1.26  
    1.27 -fun mk_srel_coinduct_tac ks raw_coind bis_srel =
    1.28 +fun mk_dtor_srel_coinduct_tac ks raw_coind bis_srel =
    1.29    EVERY' [rtac rev_mp, rtac raw_coind, rtac ssubst, rtac bis_srel, rtac conjI,
    1.30      CONJ_WRAP' (K (rtac @{thm ord_le_eq_trans[OF subset_UNIV UNIV_Times_UNIV[THEN sym]]})) ks,
    1.31      CONJ_WRAP' (K (EVERY' [rtac allI, rtac allI, rtac impI,
    1.32 @@ -1132,8 +1132,8 @@
    1.33      CONJ_WRAP' (K (EVERY' [rtac impI, rtac @{thm IdD}, etac set_mp,
    1.34        rtac CollectI, etac @{thm prod_caseI}])) ks] 1;
    1.35  
    1.36 -fun mk_srel_strong_coinduct_tac m cTs cts srel_coinduct srel_monos srel_Ids =
    1.37 -  EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts srel_coinduct),
    1.38 +fun mk_dtor_srel_strong_coinduct_tac m cTs cts dtor_srel_coinduct srel_monos srel_Ids =
    1.39 +  EVERY' [rtac rev_mp, rtac (Drule.instantiate' cTs cts dtor_srel_coinduct),
    1.40      EVERY' (map2 (fn srel_mono => fn srel_Id =>
    1.41        EVERY' [REPEAT_DETERM o resolve_tac [allI, impI], REPEAT_DETERM o etac allE,
    1.42          etac disjE, etac mp, atac, hyp_subst_tac, rtac (srel_mono RS set_mp),