src/HOL/Tools/BNF/bnf_fp_util.ML
changeset 57983 6edc3529bb4e
parent 57700 a2c4adb839a9
child 58115 bfde04fc5190
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -71,7 +71,10 @@
     1.4    val caseN: string
     1.5    val coN: string
     1.6    val coinductN: string
     1.7 +  val coinduct_strongN: string
     1.8    val corecN: string
     1.9 +  val corec_discN: string
    1.10 +  val corec_disc_iffN: string
    1.11    val ctorN: string
    1.12    val ctor_dtorN: string
    1.13    val ctor_exhaustN: string
    1.14 @@ -91,8 +94,6 @@
    1.15    val ctor_rel_inductN: string
    1.16    val ctor_set_inclN: string
    1.17    val ctor_set_set_inclN: string
    1.18 -  val disc_corecN: string
    1.19 -  val disc_corec_iffN: string
    1.20    val dtorN: string
    1.21    val dtor_coinductN: string
    1.22    val dtor_corecN: string
    1.23 @@ -103,13 +104,13 @@
    1.24    val dtor_injectN: string
    1.25    val dtor_mapN: string
    1.26    val dtor_map_coinductN: string
    1.27 -  val dtor_map_strong_coinductN: string
    1.28 +  val dtor_map_coinduct_strongN: string
    1.29    val dtor_map_uniqueN: string
    1.30    val dtor_relN: string
    1.31    val dtor_rel_coinductN: string
    1.32    val dtor_set_inclN: string
    1.33    val dtor_set_set_inclN: string
    1.34 -  val dtor_strong_coinductN: string
    1.35 +  val dtor_coinduct_strongN: string
    1.36    val dtor_unfoldN: string
    1.37    val dtor_unfold_o_mapN: string
    1.38    val dtor_unfold_transferN: string
    1.39 @@ -134,14 +135,13 @@
    1.40    val rel_distinctN: string
    1.41    val rel_selN: string
    1.42    val rvN: string
    1.43 -  val sel_corecN: string
    1.44 +  val corec_selN: string
    1.45    val set_inclN: string
    1.46    val set_set_inclN: string
    1.47    val setN: string
    1.48    val simpsN: string
    1.49    val strTN: string
    1.50    val str_initN: string
    1.51 -  val strong_coinductN: string
    1.52    val sum_bdN: string
    1.53    val sum_bdTN: string
    1.54    val uniqueN: string
    1.55 @@ -206,7 +206,7 @@
    1.56    val mk_xtor_un_fold_o_map_thms: BNF_Util.fp_kind -> bool -> int -> thm -> thm list -> thm list ->
    1.57      thm list -> thm list -> thm list
    1.58  
    1.59 -  val mk_strong_coinduct_thm: thm -> thm list -> thm list -> (thm -> thm) -> Proof.context -> thm
    1.60 +  val mk_coinduct_strong_thm: thm -> thm list -> thm list -> (thm -> thm) -> Proof.context -> thm
    1.61  
    1.62    val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list ->
    1.63        BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory -> 'a) ->
    1.64 @@ -393,9 +393,9 @@
    1.65  val ctor_induct2N = ctor_inductN ^ "2"
    1.66  val dtor_map_coinductN = dtor_mapN ^ "_" ^ coinductN
    1.67  val dtor_coinductN = dtorN ^ "_" ^ coinductN
    1.68 -val strong_coinductN = "strong_" ^ coinductN
    1.69 -val dtor_map_strong_coinductN = dtor_mapN ^ "_" ^ strong_coinductN
    1.70 -val dtor_strong_coinductN = dtorN ^ "_" ^ strong_coinductN
    1.71 +val coinduct_strongN = coinductN ^ "_strong"
    1.72 +val dtor_map_coinduct_strongN = dtor_mapN ^ "_" ^ coinduct_strongN
    1.73 +val dtor_coinduct_strongN = dtorN ^ "_" ^ coinduct_strongN
    1.74  val colN = "col"
    1.75  val set_inclN = "set_incl"
    1.76  val ctor_set_inclN = ctorN ^ "_" ^ set_inclN
    1.77 @@ -406,9 +406,9 @@
    1.78  
    1.79  val caseN = "case"
    1.80  val discN = "disc"
    1.81 -val disc_corecN = discN ^ "_" ^ corecN
    1.82 +val corec_discN = corecN ^ "_" ^ discN
    1.83  val iffN = "_iff"
    1.84 -val disc_corec_iffN = discN ^ "_" ^ corecN ^ iffN
    1.85 +val corec_disc_iffN = corec_discN ^ iffN
    1.86  val distinctN = "distinct"
    1.87  val rel_distinctN = relN ^ "_" ^ distinctN
    1.88  val injectN = "inject"
    1.89 @@ -421,7 +421,7 @@
    1.90  val rel_inductN = relN ^ "_" ^ inductN
    1.91  val ctor_rel_inductN = ctorN ^ "_" ^ rel_inductN
    1.92  val selN = "sel"
    1.93 -val sel_corecN = selN ^ "_" ^ corecN
    1.94 +val corec_selN = corecN ^ "_" ^ selN
    1.95  
    1.96  fun co_prefix fp = case_fp fp "" "co";
    1.97  
    1.98 @@ -634,7 +634,7 @@
    1.99      split_conj_thm (un_fold_unique OF map (case_fp fp I mk_sym) unique_prems)
   1.100    end;
   1.101  
   1.102 -fun mk_strong_coinduct_thm coind rel_eqs rel_monos mk_vimage2p ctxt =
   1.103 +fun mk_coinduct_strong_thm coind rel_eqs rel_monos mk_vimage2p ctxt =
   1.104    let
   1.105      val n = Thm.nprems_of coind;
   1.106      val m = Thm.nprems_of (hd rel_monos) - n;