lowercase type constructor, for consistency (cf. fp_result not FP_result nor FP_Result)
authorblanchet
Tue Apr 30 13:38:41 2013 +0200 (2013-04-30)
changeset 51837087498724486
parent 51836 4d6dcd51dd52
child 51838 1999b2e0b157
lowercase type constructor, for consistency (cf. fp_result not FP_result nor FP_Result)
src/HOL/BNF/Tools/bnf_comp.ML
src/HOL/BNF/Tools/bnf_def.ML
src/HOL/BNF/Tools/bnf_fp.ML
src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
src/HOL/BNF/Tools/bnf_gfp.ML
src/HOL/BNF/Tools/bnf_lfp.ML
     1.1 --- a/src/HOL/BNF/Tools/bnf_comp.ML	Tue Apr 30 13:34:31 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_comp.ML	Tue Apr 30 13:38:41 2013 +0200
     1.3 @@ -8,21 +8,21 @@
     1.4  
     1.5  signature BNF_COMP =
     1.6  sig
     1.7 -  val ID_bnf: BNF_Def.BNF
     1.8 -  val DEADID_bnf: BNF_Def.BNF
     1.9 +  val ID_bnf: BNF_Def.bnf
    1.10 +  val DEADID_bnf: BNF_Def.bnf
    1.11  
    1.12    type unfold_set
    1.13    val empty_unfolds: unfold_set
    1.14  
    1.15    val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
    1.16      ((string * sort) list list -> (string * sort) list) -> typ -> unfold_set * Proof.context ->
    1.17 -    (BNF_Def.BNF * (typ list * typ list)) * (unfold_set * Proof.context)
    1.18 +    (BNF_Def.bnf * (typ list * typ list)) * (unfold_set * Proof.context)
    1.19    val default_comp_sort: (string * sort) list list -> (string * sort) list
    1.20    val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list ->
    1.21 -    (''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_set -> Proof.context ->
    1.22 -    (int list list * ''a list) * (BNF_Def.BNF list * (unfold_set * Proof.context))
    1.23 -  val seal_bnf: unfold_set -> binding -> typ list -> BNF_Def.BNF -> Proof.context ->
    1.24 -    (BNF_Def.BNF * typ list) * local_theory
    1.25 +    (''a list list -> ''a list) -> BNF_Def.bnf list -> unfold_set -> Proof.context ->
    1.26 +    (int list list * ''a list) * (BNF_Def.bnf list * (unfold_set * Proof.context))
    1.27 +  val seal_bnf: unfold_set -> binding -> typ list -> BNF_Def.bnf -> Proof.context ->
    1.28 +    (BNF_Def.bnf * typ list) * local_theory
    1.29  end;
    1.30  
    1.31  structure BNF_Comp : BNF_COMP =
     2.1 --- a/src/HOL/BNF/Tools/bnf_def.ML	Tue Apr 30 13:34:31 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_def.ML	Tue Apr 30 13:38:41 2013 +0200
     2.3 @@ -8,21 +8,21 @@
     2.4  
     2.5  signature BNF_DEF =
     2.6  sig
     2.7 -  type BNF
     2.8 +  type bnf
     2.9    type nonemptiness_witness = {I: int list, wit: term, prop: thm list}
    2.10  
    2.11 -  val morph_bnf: morphism -> BNF -> BNF
    2.12 -  val eq_bnf: BNF * BNF -> bool
    2.13 -  val bnf_of: Proof.context -> string -> BNF option
    2.14 -  val register_bnf: string -> (BNF * local_theory) -> (BNF * local_theory)
    2.15 +  val morph_bnf: morphism -> bnf -> bnf
    2.16 +  val eq_bnf: bnf * bnf -> bool
    2.17 +  val bnf_of: Proof.context -> string -> bnf option
    2.18 +  val register_bnf: string -> (bnf * local_theory) -> (bnf * local_theory)
    2.19  
    2.20 -  val name_of_bnf: BNF -> binding
    2.21 -  val T_of_bnf: BNF -> typ
    2.22 -  val live_of_bnf: BNF -> int
    2.23 -  val lives_of_bnf: BNF -> typ list
    2.24 -  val dead_of_bnf: BNF -> int
    2.25 -  val deads_of_bnf: BNF -> typ list
    2.26 -  val nwits_of_bnf: BNF -> int
    2.27 +  val name_of_bnf: bnf -> binding
    2.28 +  val T_of_bnf: bnf -> typ
    2.29 +  val live_of_bnf: bnf -> int
    2.30 +  val lives_of_bnf: bnf -> typ list
    2.31 +  val dead_of_bnf: bnf -> int
    2.32 +  val deads_of_bnf: bnf -> typ list
    2.33 +  val nwits_of_bnf: bnf -> int
    2.34  
    2.35    val mapN: string
    2.36    val relN: string
    2.37 @@ -30,59 +30,59 @@
    2.38    val mk_setN: int -> string
    2.39    val srelN: string
    2.40  
    2.41 -  val map_of_bnf: BNF -> term
    2.42 -  val sets_of_bnf: BNF -> term list
    2.43 -  val rel_of_bnf: BNF -> term
    2.44 +  val map_of_bnf: bnf -> term
    2.45 +  val sets_of_bnf: bnf -> term list
    2.46 +  val rel_of_bnf: bnf -> term
    2.47  
    2.48 -  val mk_T_of_bnf: typ list -> typ list -> BNF -> typ
    2.49 -  val mk_bd_of_bnf: typ list -> typ list -> BNF -> term
    2.50 -  val mk_map_of_bnf: typ list -> typ list -> typ list -> BNF -> term
    2.51 -  val mk_rel_of_bnf: typ list -> typ list -> typ list -> BNF -> term
    2.52 -  val mk_sets_of_bnf: typ list list -> typ list list -> BNF -> term list
    2.53 -  val mk_srel_of_bnf: typ list -> typ list -> typ list -> BNF -> term
    2.54 -  val mk_wits_of_bnf: typ list list -> typ list list -> BNF -> (int list * term) list
    2.55 +  val mk_T_of_bnf: typ list -> typ list -> bnf -> typ
    2.56 +  val mk_bd_of_bnf: typ list -> typ list -> bnf -> term
    2.57 +  val mk_map_of_bnf: typ list -> typ list -> typ list -> bnf -> term
    2.58 +  val mk_rel_of_bnf: typ list -> typ list -> typ list -> bnf -> term
    2.59 +  val mk_sets_of_bnf: typ list list -> typ list list -> bnf -> term list
    2.60 +  val mk_srel_of_bnf: typ list -> typ list -> typ list -> bnf -> term
    2.61 +  val mk_wits_of_bnf: typ list list -> typ list list -> bnf -> (int list * term) list
    2.62  
    2.63 -  val bd_Card_order_of_bnf: BNF -> thm
    2.64 -  val bd_Cinfinite_of_bnf: BNF -> thm
    2.65 -  val bd_Cnotzero_of_bnf: BNF -> thm
    2.66 -  val bd_card_order_of_bnf: BNF -> thm
    2.67 -  val bd_cinfinite_of_bnf: BNF -> thm
    2.68 -  val collect_set_map_of_bnf: BNF -> thm
    2.69 -  val in_bd_of_bnf: BNF -> thm
    2.70 -  val in_cong_of_bnf: BNF -> thm
    2.71 -  val in_mono_of_bnf: BNF -> thm
    2.72 -  val in_srel_of_bnf: BNF -> thm
    2.73 -  val map_comp'_of_bnf: BNF -> thm
    2.74 -  val map_comp_of_bnf: BNF -> thm
    2.75 -  val map_cong0_of_bnf: BNF -> thm
    2.76 -  val map_cong_of_bnf: BNF -> thm
    2.77 -  val map_def_of_bnf: BNF -> thm
    2.78 -  val map_id'_of_bnf: BNF -> thm
    2.79 -  val map_id_of_bnf: BNF -> thm
    2.80 -  val map_wppull_of_bnf: BNF -> thm
    2.81 -  val map_wpull_of_bnf: BNF -> thm
    2.82 -  val rel_def_of_bnf: BNF -> thm
    2.83 -  val rel_eq_of_bnf: BNF -> thm
    2.84 -  val rel_flip_of_bnf: BNF -> thm
    2.85 -  val rel_srel_of_bnf: BNF -> thm
    2.86 -  val set_bd_of_bnf: BNF -> thm list
    2.87 -  val set_defs_of_bnf: BNF -> thm list
    2.88 -  val set_map'_of_bnf: BNF -> thm list
    2.89 -  val set_map_of_bnf: BNF -> thm list
    2.90 -  val srel_def_of_bnf: BNF -> thm
    2.91 -  val srel_Gr_of_bnf: BNF -> thm
    2.92 -  val srel_Id_of_bnf: BNF -> thm
    2.93 -  val srel_O_of_bnf: BNF -> thm
    2.94 -  val srel_O_Gr_of_bnf: BNF -> thm
    2.95 -  val srel_cong_of_bnf: BNF -> thm
    2.96 -  val srel_converse_of_bnf: BNF -> thm
    2.97 -  val srel_mono_of_bnf: BNF -> thm
    2.98 -  val wit_thms_of_bnf: BNF -> thm list
    2.99 -  val wit_thmss_of_bnf: BNF -> thm list list
   2.100 +  val bd_Card_order_of_bnf: bnf -> thm
   2.101 +  val bd_Cinfinite_of_bnf: bnf -> thm
   2.102 +  val bd_Cnotzero_of_bnf: bnf -> thm
   2.103 +  val bd_card_order_of_bnf: bnf -> thm
   2.104 +  val bd_cinfinite_of_bnf: bnf -> thm
   2.105 +  val collect_set_map_of_bnf: bnf -> thm
   2.106 +  val in_bd_of_bnf: bnf -> thm
   2.107 +  val in_cong_of_bnf: bnf -> thm
   2.108 +  val in_mono_of_bnf: bnf -> thm
   2.109 +  val in_srel_of_bnf: bnf -> thm
   2.110 +  val map_comp'_of_bnf: bnf -> thm
   2.111 +  val map_comp_of_bnf: bnf -> thm
   2.112 +  val map_cong0_of_bnf: bnf -> thm
   2.113 +  val map_cong_of_bnf: bnf -> thm
   2.114 +  val map_def_of_bnf: bnf -> thm
   2.115 +  val map_id'_of_bnf: bnf -> thm
   2.116 +  val map_id_of_bnf: bnf -> thm
   2.117 +  val map_wppull_of_bnf: bnf -> thm
   2.118 +  val map_wpull_of_bnf: bnf -> thm
   2.119 +  val rel_def_of_bnf: bnf -> thm
   2.120 +  val rel_eq_of_bnf: bnf -> thm
   2.121 +  val rel_flip_of_bnf: bnf -> thm
   2.122 +  val rel_srel_of_bnf: bnf -> thm
   2.123 +  val set_bd_of_bnf: bnf -> thm list
   2.124 +  val set_defs_of_bnf: bnf -> thm list
   2.125 +  val set_map'_of_bnf: bnf -> thm list
   2.126 +  val set_map_of_bnf: bnf -> thm list
   2.127 +  val srel_def_of_bnf: bnf -> thm
   2.128 +  val srel_Gr_of_bnf: bnf -> thm
   2.129 +  val srel_Id_of_bnf: bnf -> thm
   2.130 +  val srel_O_of_bnf: bnf -> thm
   2.131 +  val srel_O_Gr_of_bnf: bnf -> thm
   2.132 +  val srel_cong_of_bnf: bnf -> thm
   2.133 +  val srel_converse_of_bnf: bnf -> thm
   2.134 +  val srel_mono_of_bnf: bnf -> thm
   2.135 +  val wit_thms_of_bnf: bnf -> thm list
   2.136 +  val wit_thmss_of_bnf: bnf -> thm list list
   2.137  
   2.138    val mk_witness: int list * term -> thm list -> nonemptiness_witness
   2.139    val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list
   2.140 -  val wits_of_bnf: BNF -> nonemptiness_witness list
   2.141 +  val wits_of_bnf: bnf -> nonemptiness_witness list
   2.142  
   2.143    val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a -> 'a list
   2.144  
   2.145 @@ -98,7 +98,7 @@
   2.146      ({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding ->
   2.147      binding -> binding list ->
   2.148      ((((binding * term) * term list) * term) * term list) * term option ->
   2.149 -    local_theory -> BNF * local_theory
   2.150 +    local_theory -> bnf * local_theory
   2.151  end;
   2.152  
   2.153  structure BNF_Def : BNF_DEF =
   2.154 @@ -286,7 +286,7 @@
   2.155  fun map_witness f g {I, wit, prop} = {I = I, wit = f wit, prop = map g prop};
   2.156  fun morph_witness phi = map_witness (Morphism.term phi) (Morphism.thm phi);
   2.157  
   2.158 -datatype BNF = BNF of {
   2.159 +datatype bnf = BNF of {
   2.160    name: binding,
   2.161    T: typ,
   2.162    live: int,
   2.163 @@ -434,7 +434,7 @@
   2.164  
   2.165  structure Data = Generic_Data
   2.166  (
   2.167 -  type T = BNF Symtab.table;
   2.168 +  type T = bnf Symtab.table;
   2.169    val empty = Symtab.empty;
   2.170    val extend = I;
   2.171    val merge = Symtab.merge eq_bnf;
     3.1 --- a/src/HOL/BNF/Tools/bnf_fp.ML	Tue Apr 30 13:34:31 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_fp.ML	Tue Apr 30 13:38:41 2013 +0200
     3.3 @@ -9,7 +9,7 @@
     3.4  signature BNF_FP =
     3.5  sig
     3.6    type fp_result =
     3.7 -    {bnfs: BNF_Def.BNF list,
     3.8 +    {bnfs: BNF_Def.bnf list,
     3.9       dtors: term list,
    3.10       ctors: term list,
    3.11       folds: term list,
    3.12 @@ -158,10 +158,10 @@
    3.13    val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
    3.14  
    3.15    val fp_bnf: (mixfix list -> (string * sort) list option -> binding list -> binding list ->
    3.16 -      binding list -> binding list list -> typ list * typ list list -> BNF_Def.BNF list ->
    3.17 +      binding list -> binding list list -> typ list * typ list list -> BNF_Def.bnf list ->
    3.18        local_theory -> 'a) ->
    3.19      binding list -> mixfix list -> binding list -> binding list -> binding list list ->
    3.20 -    (string * sort) list -> ((string * sort) * typ) list -> local_theory -> BNF_Def.BNF list * 'a
    3.21 +    (string * sort) list -> ((string * sort) * typ) list -> local_theory -> BNF_Def.bnf list * 'a
    3.22  end;
    3.23  
    3.24  structure BNF_FP : BNF_FP =
    3.25 @@ -172,7 +172,7 @@
    3.26  open BNF_Util
    3.27  
    3.28  type fp_result =
    3.29 -  {bnfs: BNF_Def.BNF list,
    3.30 +  {bnfs: BNF_Def.bnf list,
    3.31     dtors: term list,
    3.32     ctors: term list,
    3.33     folds: term list,
     4.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 30 13:34:31 2013 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 30 13:38:41 2013 +0200
     4.3 @@ -15,14 +15,14 @@
     4.4  
     4.5    val fp_of: Proof.context -> string -> fp option
     4.6  
     4.7 -  val derive_induct_fold_rec_thms_for_types: BNF_Def.BNF list -> term list -> term list -> thm ->
     4.8 -    thm list -> thm list -> BNF_Def.BNF list -> BNF_Def.BNF list -> typ list -> typ list ->
     4.9 +  val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list -> term list -> thm ->
    4.10 +    thm list -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list ->
    4.11      typ list -> term list list -> thm list list -> term list -> term list -> thm list -> thm list ->
    4.12      Proof.context ->
    4.13      (thm * thm list * Args.src list) * (thm list list * Args.src list)
    4.14      * (thm list list * Args.src list)
    4.15 -  val derive_coinduct_unfold_corec_thms_for_types: BNF_Def.BNF list -> term list -> term list ->
    4.16 -    thm -> thm -> thm list -> thm list -> thm list -> BNF_Def.BNF list -> BNF_Def.BNF list ->
    4.17 +  val derive_coinduct_unfold_corec_thms_for_types: BNF_Def.bnf list -> term list -> term list ->
    4.18 +    thm -> thm -> thm list -> thm list -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list ->
    4.19      typ list -> typ list -> typ list -> int list list -> int list list -> int list ->
    4.20      term list list -> thm list list -> BNF_Ctr_Sugar.ctr_wrap_result list -> term list ->
    4.21      term list -> thm list -> thm list -> Proof.context ->
    4.22 @@ -33,7 +33,7 @@
    4.23  
    4.24    val datatypes: bool ->
    4.25      (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
    4.26 -      binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    4.27 +      binding list list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory ->
    4.28        BNF_FP.fp_result * local_theory) ->
    4.29      (bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) *
    4.30        ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
    4.31 @@ -41,7 +41,7 @@
    4.32      local_theory -> local_theory
    4.33    val parse_datatype_cmd: bool ->
    4.34      (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
    4.35 -      binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
    4.36 +      binding list list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory ->
    4.37        BNF_FP.fp_result * local_theory) ->
    4.38      (local_theory -> local_theory) parser
    4.39  end;
     5.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Tue Apr 30 13:34:31 2013 +0200
     5.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Tue Apr 30 13:38:41 2013 +0200
     5.3 @@ -10,7 +10,7 @@
     5.4  signature BNF_GFP =
     5.5  sig
     5.6    val construct_gfp: mixfix list -> (string * sort) list option -> binding list -> binding list ->
     5.7 -    binding list -> binding list list -> typ list * typ list list -> BNF_Def.BNF list ->
     5.8 +    binding list -> binding list list -> typ list * typ list list -> BNF_Def.bnf list ->
     5.9      local_theory -> BNF_FP.fp_result * local_theory
    5.10  end;
    5.11  
     6.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Tue Apr 30 13:34:31 2013 +0200
     6.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Tue Apr 30 13:38:41 2013 +0200
     6.3 @@ -9,7 +9,7 @@
     6.4  signature BNF_LFP =
     6.5  sig
     6.6    val construct_lfp: mixfix list -> (string * sort) list option -> binding list -> binding list ->
     6.7 -    binding list -> binding list list -> typ list * typ list list -> BNF_Def.BNF list ->
     6.8 +    binding list -> binding list list -> typ list * typ list list -> BNF_Def.bnf list ->
     6.9      local_theory -> BNF_FP.fp_result * local_theory
    6.10  end;
    6.11