lowercase type constructor, for consistency (cf. fp_result not FP_result nor FP_Result)
--- a/src/HOL/BNF/Tools/bnf_comp.ML Tue Apr 30 13:34:31 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Tue Apr 30 13:38:41 2013 +0200
@@ -8,21 +8,21 @@
signature BNF_COMP =
sig
- val ID_bnf: BNF_Def.BNF
- val DEADID_bnf: BNF_Def.BNF
+ val ID_bnf: BNF_Def.bnf
+ val DEADID_bnf: BNF_Def.bnf
type unfold_set
val empty_unfolds: unfold_set
val bnf_of_typ: BNF_Def.const_policy -> (binding -> binding) ->
((string * sort) list list -> (string * sort) list) -> typ -> unfold_set * Proof.context ->
- (BNF_Def.BNF * (typ list * typ list)) * (unfold_set * Proof.context)
+ (BNF_Def.bnf * (typ list * typ list)) * (unfold_set * Proof.context)
val default_comp_sort: (string * sort) list list -> (string * sort) list
val normalize_bnfs: (int -> binding -> binding) -> ''a list list -> ''a list ->
- (''a list list -> ''a list) -> BNF_Def.BNF list -> unfold_set -> Proof.context ->
- (int list list * ''a list) * (BNF_Def.BNF list * (unfold_set * Proof.context))
- val seal_bnf: unfold_set -> binding -> typ list -> BNF_Def.BNF -> Proof.context ->
- (BNF_Def.BNF * typ list) * local_theory
+ (''a list list -> ''a list) -> BNF_Def.bnf list -> unfold_set -> Proof.context ->
+ (int list list * ''a list) * (BNF_Def.bnf list * (unfold_set * Proof.context))
+ val seal_bnf: unfold_set -> binding -> typ list -> BNF_Def.bnf -> Proof.context ->
+ (BNF_Def.bnf * typ list) * local_theory
end;
structure BNF_Comp : BNF_COMP =
--- a/src/HOL/BNF/Tools/bnf_def.ML Tue Apr 30 13:34:31 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML Tue Apr 30 13:38:41 2013 +0200
@@ -8,21 +8,21 @@
signature BNF_DEF =
sig
- type BNF
+ type bnf
type nonemptiness_witness = {I: int list, wit: term, prop: thm list}
- val morph_bnf: morphism -> BNF -> BNF
- val eq_bnf: BNF * BNF -> bool
- val bnf_of: Proof.context -> string -> BNF option
- val register_bnf: string -> (BNF * local_theory) -> (BNF * local_theory)
+ val morph_bnf: morphism -> bnf -> bnf
+ val eq_bnf: bnf * bnf -> bool
+ val bnf_of: Proof.context -> string -> bnf option
+ val register_bnf: string -> (bnf * local_theory) -> (bnf * local_theory)
- val name_of_bnf: BNF -> binding
- val T_of_bnf: BNF -> typ
- val live_of_bnf: BNF -> int
- val lives_of_bnf: BNF -> typ list
- val dead_of_bnf: BNF -> int
- val deads_of_bnf: BNF -> typ list
- val nwits_of_bnf: BNF -> int
+ val name_of_bnf: bnf -> binding
+ val T_of_bnf: bnf -> typ
+ val live_of_bnf: bnf -> int
+ val lives_of_bnf: bnf -> typ list
+ val dead_of_bnf: bnf -> int
+ val deads_of_bnf: bnf -> typ list
+ val nwits_of_bnf: bnf -> int
val mapN: string
val relN: string
@@ -30,59 +30,59 @@
val mk_setN: int -> string
val srelN: string
- val map_of_bnf: BNF -> term
- val sets_of_bnf: BNF -> term list
- val rel_of_bnf: BNF -> term
+ val map_of_bnf: bnf -> term
+ val sets_of_bnf: bnf -> term list
+ val rel_of_bnf: bnf -> term
- val mk_T_of_bnf: typ list -> typ list -> BNF -> typ
- val mk_bd_of_bnf: typ list -> typ list -> BNF -> term
- val mk_map_of_bnf: typ list -> typ list -> typ list -> BNF -> term
- val mk_rel_of_bnf: typ list -> typ list -> typ list -> BNF -> term
- val mk_sets_of_bnf: typ list list -> typ list list -> BNF -> term list
- val mk_srel_of_bnf: typ list -> typ list -> typ list -> BNF -> term
- val mk_wits_of_bnf: typ list list -> typ list list -> BNF -> (int list * term) list
+ val mk_T_of_bnf: typ list -> typ list -> bnf -> typ
+ val mk_bd_of_bnf: typ list -> typ list -> bnf -> term
+ val mk_map_of_bnf: typ list -> typ list -> typ list -> bnf -> term
+ val mk_rel_of_bnf: typ list -> typ list -> typ list -> bnf -> term
+ val mk_sets_of_bnf: typ list list -> typ list list -> bnf -> term list
+ val mk_srel_of_bnf: typ list -> typ list -> typ list -> bnf -> term
+ val mk_wits_of_bnf: typ list list -> typ list list -> bnf -> (int list * term) list
- val bd_Card_order_of_bnf: BNF -> thm
- val bd_Cinfinite_of_bnf: BNF -> thm
- val bd_Cnotzero_of_bnf: BNF -> thm
- val bd_card_order_of_bnf: BNF -> thm
- val bd_cinfinite_of_bnf: BNF -> thm
- val collect_set_map_of_bnf: BNF -> thm
- val in_bd_of_bnf: BNF -> thm
- val in_cong_of_bnf: BNF -> thm
- val in_mono_of_bnf: BNF -> thm
- val in_srel_of_bnf: BNF -> thm
- val map_comp'_of_bnf: BNF -> thm
- val map_comp_of_bnf: BNF -> thm
- val map_cong0_of_bnf: BNF -> thm
- val map_cong_of_bnf: BNF -> thm
- val map_def_of_bnf: BNF -> thm
- val map_id'_of_bnf: BNF -> thm
- val map_id_of_bnf: BNF -> thm
- val map_wppull_of_bnf: BNF -> thm
- val map_wpull_of_bnf: BNF -> thm
- val rel_def_of_bnf: BNF -> thm
- val rel_eq_of_bnf: BNF -> thm
- val rel_flip_of_bnf: BNF -> thm
- val rel_srel_of_bnf: BNF -> thm
- val set_bd_of_bnf: BNF -> thm list
- val set_defs_of_bnf: BNF -> thm list
- val set_map'_of_bnf: BNF -> thm list
- val set_map_of_bnf: BNF -> thm list
- val srel_def_of_bnf: BNF -> thm
- val srel_Gr_of_bnf: BNF -> thm
- val srel_Id_of_bnf: BNF -> thm
- val srel_O_of_bnf: BNF -> thm
- val srel_O_Gr_of_bnf: BNF -> thm
- val srel_cong_of_bnf: BNF -> thm
- val srel_converse_of_bnf: BNF -> thm
- val srel_mono_of_bnf: BNF -> thm
- val wit_thms_of_bnf: BNF -> thm list
- val wit_thmss_of_bnf: BNF -> thm list list
+ val bd_Card_order_of_bnf: bnf -> thm
+ val bd_Cinfinite_of_bnf: bnf -> thm
+ val bd_Cnotzero_of_bnf: bnf -> thm
+ val bd_card_order_of_bnf: bnf -> thm
+ val bd_cinfinite_of_bnf: bnf -> thm
+ val collect_set_map_of_bnf: bnf -> thm
+ val in_bd_of_bnf: bnf -> thm
+ val in_cong_of_bnf: bnf -> thm
+ val in_mono_of_bnf: bnf -> thm
+ val in_srel_of_bnf: bnf -> thm
+ val map_comp'_of_bnf: bnf -> thm
+ val map_comp_of_bnf: bnf -> thm
+ val map_cong0_of_bnf: bnf -> thm
+ val map_cong_of_bnf: bnf -> thm
+ val map_def_of_bnf: bnf -> thm
+ val map_id'_of_bnf: bnf -> thm
+ val map_id_of_bnf: bnf -> thm
+ val map_wppull_of_bnf: bnf -> thm
+ val map_wpull_of_bnf: bnf -> thm
+ val rel_def_of_bnf: bnf -> thm
+ val rel_eq_of_bnf: bnf -> thm
+ val rel_flip_of_bnf: bnf -> thm
+ val rel_srel_of_bnf: bnf -> thm
+ val set_bd_of_bnf: bnf -> thm list
+ val set_defs_of_bnf: bnf -> thm list
+ val set_map'_of_bnf: bnf -> thm list
+ val set_map_of_bnf: bnf -> thm list
+ val srel_def_of_bnf: bnf -> thm
+ val srel_Gr_of_bnf: bnf -> thm
+ val srel_Id_of_bnf: bnf -> thm
+ val srel_O_of_bnf: bnf -> thm
+ val srel_O_Gr_of_bnf: bnf -> thm
+ val srel_cong_of_bnf: bnf -> thm
+ val srel_converse_of_bnf: bnf -> thm
+ val srel_mono_of_bnf: bnf -> thm
+ val wit_thms_of_bnf: bnf -> thm list
+ val wit_thmss_of_bnf: bnf -> thm list list
val mk_witness: int list * term -> thm list -> nonemptiness_witness
val minimize_wits: (''a list * 'b) list -> (''a list * 'b) list
- val wits_of_bnf: BNF -> nonemptiness_witness list
+ val wits_of_bnf: bnf -> nonemptiness_witness list
val zip_axioms: 'a -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a list -> 'a -> 'a -> 'a -> 'a list
@@ -98,7 +98,7 @@
({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding ->
binding -> binding list ->
((((binding * term) * term list) * term) * term list) * term option ->
- local_theory -> BNF * local_theory
+ local_theory -> bnf * local_theory
end;
structure BNF_Def : BNF_DEF =
@@ -286,7 +286,7 @@
fun map_witness f g {I, wit, prop} = {I = I, wit = f wit, prop = map g prop};
fun morph_witness phi = map_witness (Morphism.term phi) (Morphism.thm phi);
-datatype BNF = BNF of {
+datatype bnf = BNF of {
name: binding,
T: typ,
live: int,
@@ -434,7 +434,7 @@
structure Data = Generic_Data
(
- type T = BNF Symtab.table;
+ type T = bnf Symtab.table;
val empty = Symtab.empty;
val extend = I;
val merge = Symtab.merge eq_bnf;
--- a/src/HOL/BNF/Tools/bnf_fp.ML Tue Apr 30 13:34:31 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp.ML Tue Apr 30 13:38:41 2013 +0200
@@ -9,7 +9,7 @@
signature BNF_FP =
sig
type fp_result =
- {bnfs: BNF_Def.BNF list,
+ {bnfs: BNF_Def.bnf list,
dtors: term list,
ctors: term list,
folds: term list,
@@ -158,10 +158,10 @@
val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
val fp_bnf: (mixfix list -> (string * sort) list option -> binding list -> binding list ->
- binding list -> binding list list -> typ list * typ list list -> BNF_Def.BNF list ->
+ binding list -> binding list list -> typ list * typ list list -> BNF_Def.bnf list ->
local_theory -> 'a) ->
binding list -> mixfix list -> binding list -> binding list -> binding list list ->
- (string * sort) list -> ((string * sort) * typ) list -> local_theory -> BNF_Def.BNF list * 'a
+ (string * sort) list -> ((string * sort) * typ) list -> local_theory -> BNF_Def.bnf list * 'a
end;
structure BNF_FP : BNF_FP =
@@ -172,7 +172,7 @@
open BNF_Util
type fp_result =
- {bnfs: BNF_Def.BNF list,
+ {bnfs: BNF_Def.bnf list,
dtors: term list,
ctors: term list,
folds: term list,
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue Apr 30 13:34:31 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Tue Apr 30 13:38:41 2013 +0200
@@ -15,14 +15,14 @@
val fp_of: Proof.context -> string -> fp option
- val derive_induct_fold_rec_thms_for_types: BNF_Def.BNF list -> term list -> term list -> thm ->
- thm list -> thm list -> BNF_Def.BNF list -> BNF_Def.BNF list -> typ list -> typ list ->
+ val derive_induct_fold_rec_thms_for_types: BNF_Def.bnf list -> term list -> term list -> thm ->
+ thm list -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list -> typ list -> typ list ->
typ list -> term list list -> thm list list -> term list -> term list -> thm list -> thm list ->
Proof.context ->
(thm * thm list * Args.src list) * (thm list list * Args.src list)
* (thm list list * Args.src list)
- val derive_coinduct_unfold_corec_thms_for_types: BNF_Def.BNF list -> term list -> term list ->
- thm -> thm -> thm list -> thm list -> thm list -> BNF_Def.BNF list -> BNF_Def.BNF list ->
+ val derive_coinduct_unfold_corec_thms_for_types: BNF_Def.bnf list -> term list -> term list ->
+ thm -> thm -> thm list -> thm list -> thm list -> BNF_Def.bnf list -> BNF_Def.bnf list ->
typ list -> typ list -> typ list -> int list list -> int list list -> int list ->
term list list -> thm list list -> BNF_Ctr_Sugar.ctr_wrap_result list -> term list ->
term list -> thm list -> thm list -> Proof.context ->
@@ -33,7 +33,7 @@
val datatypes: bool ->
(mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
- binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
+ binding list list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory ->
BNF_FP.fp_result * local_theory) ->
(bool * bool) * (((((binding * (typ * sort)) list * binding) * (binding * binding)) * mixfix) *
((((binding * binding) * (binding * typ) list) * (binding * term) list) *
@@ -41,7 +41,7 @@
local_theory -> local_theory
val parse_datatype_cmd: bool ->
(mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
- binding list list -> typ list * typ list list -> BNF_Def.BNF list -> local_theory ->
+ binding list list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory ->
BNF_FP.fp_result * local_theory) ->
(local_theory -> local_theory) parser
end;
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Tue Apr 30 13:34:31 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Tue Apr 30 13:38:41 2013 +0200
@@ -10,7 +10,7 @@
signature BNF_GFP =
sig
val construct_gfp: mixfix list -> (string * sort) list option -> binding list -> binding list ->
- binding list -> binding list list -> typ list * typ list list -> BNF_Def.BNF list ->
+ binding list -> binding list list -> typ list * typ list list -> BNF_Def.bnf list ->
local_theory -> BNF_FP.fp_result * local_theory
end;
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Tue Apr 30 13:34:31 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Tue Apr 30 13:38:41 2013 +0200
@@ -9,7 +9,7 @@
signature BNF_LFP =
sig
val construct_lfp: mixfix list -> (string * sort) list option -> binding list -> binding list ->
- binding list -> binding list list -> typ list * typ list list -> BNF_Def.BNF list ->
+ binding list -> binding list list -> typ list * typ list list -> BNF_Def.bnf list ->
local_theory -> BNF_FP.fp_result * local_theory
end;