--- a/src/HOL/BNF_FP_Base.thy Wed Apr 23 10:23:27 2014 +0200
+++ b/src/HOL/BNF_FP_Base.thy Wed Apr 23 10:23:27 2014 +0200
@@ -163,11 +163,58 @@
lemma vimage2p_comp: "vimage2p (f1 \<circ> f2) (g1 \<circ> g2) = vimage2p f2 g2 \<circ> vimage2p f1 g1"
unfolding fun_eq_iff vimage2p_def o_apply by simp
+lemma fun_cong_unused_0: "f = (\<lambda>x. g) \<Longrightarrow> f (\<lambda>x. 0) = g"
+ by (erule arg_cong)
+
+lemma snd_o_convol: "(snd \<circ> (\<lambda>x. (f x, g x))) = g"
+ by (rule ext) simp
+
+lemma inj_on_convol_id: "inj_on (\<lambda>x. (x, f x)) X"
+ unfolding inj_on_def by simp
+
+lemma case_prod_app: "case_prod f x y = case_prod (\<lambda>l r. f l r y) x"
+ by (case_tac x) simp
+
+lemma case_sum_map_sum: "case_sum l r (map_sum f g x) = case_sum (l \<circ> f) (r \<circ> g) x"
+ by (case_tac x) simp+
+
+lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x"
+ by (case_tac x) simp+
+
+lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)"
+ by (simp add: inj_on_def)
+
+
ML_file "Tools/BNF/bnf_fp_util.ML"
ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
+ML_file "Tools/BNF/bnf_lfp_size.ML"
ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML"
ML_file "Tools/BNF/bnf_fp_n2m.ML"
ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML"
+ML_file "Tools/Function/size.ML"
+setup Size.setup
+
+lemma size_bool[code]: "size (b\<Colon>bool) = 0"
+ by (cases b) auto
+
+lemma nat_size[simp, code]: "size (n\<Colon>nat) = n"
+ by (induct n) simp_all
+
+declare prod.size[no_atp]
+
+lemma sum_size_o_map: "sum_size g1 g2 \<circ> map_sum f1 f2 = sum_size (g1 \<circ> f1) (g2 \<circ> f2)"
+ by (rule ext) (case_tac x, auto)
+
+lemma prod_size_o_map: "prod_size g1 g2 \<circ> map_prod f1 f2 = prod_size (g1 \<circ> f1) (g2 \<circ> f2)"
+ by (rule ext) auto
+
+setup {*
+BNF_LFP_Size.register_size @{type_name sum} @{const_name sum_size} @{thms sum.size}
+ @{thms sum_size_o_map}
+#> BNF_LFP_Size.register_size @{type_name prod} @{const_name prod_size} @{thms prod.size}
+ @{thms prod_size_o_map}
+*}
+
end
--- a/src/HOL/BNF_LFP.thy Wed Apr 23 10:23:27 2014 +0200
+++ b/src/HOL/BNF_LFP.thy Wed Apr 23 10:23:27 2014 +0200
@@ -186,61 +186,14 @@
lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
by (rule ssubst)
-lemma fun_cong_unused_0: "f = (\<lambda>x. g) \<Longrightarrow> f (\<lambda>x. 0) = g"
- by (erule arg_cong)
-
-lemma snd_o_convol: "(snd \<circ> (\<lambda>x. (f x, g x))) = g"
- by (rule ext) simp
-
-lemma inj_on_convol_id: "inj_on (\<lambda>x. (x, f x)) X"
- unfolding inj_on_def by simp
-
-lemma case_prod_app: "case_prod f x y = case_prod (\<lambda>l r. f l r y) x"
- by (case_tac x) simp
-
-lemma case_sum_o_map_sum: "case_sum l r (map_sum f g x) = case_sum (l \<circ> f) (r \<circ> g) x"
- by (case_tac x) simp+
-
-lemma case_prod_o_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x"
- by (case_tac x) simp+
-
-lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)"
- by (simp add: inj_on_def)
-
ML_file "Tools/BNF/bnf_lfp_util.ML"
ML_file "Tools/BNF/bnf_lfp_tactics.ML"
ML_file "Tools/BNF/bnf_lfp.ML"
ML_file "Tools/BNF/bnf_lfp_compat.ML"
ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
-
-subsection {* Size of a datatype value *}
-
-ML_file "Tools/BNF/bnf_lfp_size.ML"
-ML_file "Tools/Function/size.ML"
-setup Size.setup
-
-lemma size_bool[code]: "size (b\<Colon>bool) = 0"
- by (cases b) auto
-
-lemma nat_size[simp, code]: "size (n\<Colon>nat) = n"
- by (induct n) simp_all
-
-declare prod.size[no_atp]
-
-lemma sum_size_o_map: "sum_size g1 g2 \<circ> map_sum f1 f2 = sum_size (g1 \<circ> f1) (g2 \<circ> f2)"
- by (rule ext) (case_tac x, auto)
-
-lemma prod_size_o_map: "prod_size g1 g2 \<circ> map_prod f1 f2 = prod_size (g1 \<circ> f1) (g2 \<circ> f2)"
- by (rule ext) auto
-
-setup {*
-BNF_LFP_Size.register_size @{type_name sum} @{const_name sum_size} @{thms sum.size}
- @{thms sum_size_o_map}
-#> BNF_LFP_Size.register_size @{type_name prod} @{const_name prod_size} @{thms prod.size}
- @{thms prod_size_o_map}
-*}
-
hide_fact (open) id_transfer
+datatype_new 'a x = X 'a
+
end
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Apr 23 10:23:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Apr 23 10:23:27 2014 +0200
@@ -7,37 +7,10 @@
signature BNF_FP_DEF_SUGAR =
sig
- type fp_sugar =
- {T: typ,
- BT: typ,
- X: typ,
- fp: BNF_Util.fp_kind,
- fp_res_index: int,
- fp_res: BNF_FP_Util.fp_result,
- pre_bnf: BNF_Def.bnf,
- absT_info: BNF_Comp.absT_info,
- nested_bnfs: BNF_Def.bnf list,
- nesting_bnfs: BNF_Def.bnf list,
- ctrXs_Tss: typ list list,
- ctr_defs: thm list,
- ctr_sugar: Ctr_Sugar.ctr_sugar,
- co_rec: term,
- co_rec_def: thm,
- maps: thm list,
- common_co_inducts: thm list,
- co_inducts: thm list,
- co_rec_thms: thm list,
- disc_co_recs: thm list,
- sel_co_recss: thm list list,
- rel_injects: thm list,
- rel_distincts: thm list};
-
- val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
- val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar
- val fp_sugar_of: Proof.context -> string -> fp_sugar option
- val fp_sugars_of: Proof.context -> fp_sugar list
- val fp_sugar_interpretation: (fp_sugar list -> theory -> theory) -> theory -> theory
- val register_fp_sugars: fp_sugar list -> local_theory -> local_theory
+ val fp_sugar_of: Proof.context -> string -> BNF_FP_Util.fp_sugar option
+ val fp_sugars_of: Proof.context -> BNF_FP_Util.fp_sugar list
+ val fp_sugar_interpretation: (BNF_FP_Util.fp_sugar list -> theory -> theory) -> theory -> theory
+ val register_fp_sugars: BNF_FP_Util.fp_sugar list -> local_theory -> local_theory
val co_induct_of: 'a list -> 'a
val strong_co_induct_of: 'a list -> 'a
@@ -121,63 +94,10 @@
open BNF_Def
open BNF_FP_Util
open BNF_FP_Def_Sugar_Tactics
+open BNF_LFP_Size
val EqN = "Eq_";
-type fp_sugar =
- {T: typ,
- BT: typ,
- X: typ,
- fp: fp_kind,
- fp_res_index: int,
- fp_res: fp_result,
- pre_bnf: bnf,
- absT_info: absT_info,
- nested_bnfs: bnf list,
- nesting_bnfs: bnf list,
- ctrXs_Tss: typ list list,
- ctr_defs: thm list,
- ctr_sugar: Ctr_Sugar.ctr_sugar,
- co_rec: term,
- co_rec_def: thm,
- maps: thm list,
- common_co_inducts: thm list,
- co_inducts: thm list,
- co_rec_thms: thm list,
- disc_co_recs: thm list,
- sel_co_recss: thm list list,
- rel_injects: thm list,
- rel_distincts: thm list};
-
-fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, nested_bnfs,
- nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts,
- co_inducts, co_rec_thms, disc_co_recs, sel_co_recss, rel_injects, rel_distincts} : fp_sugar) =
- {T = Morphism.typ phi T,
- BT = Morphism.typ phi BT,
- X = Morphism.typ phi X,
- fp = fp,
- fp_res = morph_fp_result phi fp_res,
- fp_res_index = fp_res_index,
- pre_bnf = morph_bnf phi pre_bnf,
- absT_info = morph_absT_info phi absT_info,
- nested_bnfs = map (morph_bnf phi) nested_bnfs,
- nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
- ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
- ctr_defs = map (Morphism.thm phi) ctr_defs,
- ctr_sugar = morph_ctr_sugar phi ctr_sugar,
- co_rec = Morphism.term phi co_rec,
- co_rec_def = Morphism.thm phi co_rec_def,
- maps = map (Morphism.thm phi) maps,
- common_co_inducts = map (Morphism.thm phi) common_co_inducts,
- co_inducts = map (Morphism.thm phi) co_inducts,
- co_rec_thms = map (Morphism.thm phi) co_rec_thms,
- disc_co_recs = map (Morphism.thm phi) disc_co_recs,
- sel_co_recss = map (map (Morphism.thm phi)) sel_co_recss,
- rel_injects = map (Morphism.thm phi) rel_injects,
- rel_distincts = map (Morphism.thm phi) rel_distincts};
-
-val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
-
structure Data = Generic_Data
(
type T = fp_sugar Symtab.table;
@@ -211,11 +131,12 @@
val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_repaired_path;
-fun register_fp_sugars fp_sugars =
+fun register_fp_sugars (fp_sugars as {fp, ...} :: _) =
fold (fn fp_sugar as {T = Type (s, _), ...} =>
Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Data.map (Symtab.update (s, morph_fp_sugar phi fp_sugar))))
fp_sugars
+ #> Local_Theory.background_theory (generate_lfp_size fp_sugars)
#> Local_Theory.background_theory (FP_Sugar_Interpretation.data fp_sugars);
fun register_as_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos nested_bnfs nesting_bnfs fp_res
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Apr 23 10:23:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Apr 23 10:23:27 2014 +0200
@@ -8,7 +8,7 @@
signature BNF_FP_N2M =
sig
val construct_mutualized_fp: BNF_Util.fp_kind -> int list -> typ list ->
- BNF_FP_Def_Sugar.fp_sugar list -> binding list -> (string * sort) list ->
+ BNF_FP_Util.fp_sugar list -> binding list -> (string * sort) list ->
typ list * typ list list -> BNF_Def.bnf list -> BNF_Comp.absT_info list -> local_theory ->
BNF_FP_Util.fp_result * local_theory
end;
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Apr 23 10:23:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Apr 23 10:23:27 2014 +0200
@@ -11,13 +11,13 @@
val dest_map: Proof.context -> string -> term -> term * term list
val mutualize_fp_sugars: BNF_Util.fp_kind -> int list -> binding list -> typ list -> term list ->
- term list list list list -> BNF_FP_Def_Sugar.fp_sugar list -> local_theory ->
- (BNF_FP_Def_Sugar.fp_sugar list
+ term list list list list -> BNF_FP_Util.fp_sugar list -> local_theory ->
+ (BNF_FP_Util.fp_sugar list
* (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
* local_theory
val nested_to_mutual_fps: BNF_Util.fp_kind -> binding list -> typ list -> term list ->
(term * term list list) list list -> local_theory ->
- (typ list * int list * BNF_FP_Def_Sugar.fp_sugar list
+ (typ list * int list * BNF_FP_Util.fp_sugar list
* (BNF_FP_Def_Sugar.lfp_sugar_thms option * BNF_FP_Def_Sugar.gfp_sugar_thms option))
* local_theory
end;
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Apr 23 10:23:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Apr 23 10:23:27 2014 +0200
@@ -28,6 +28,34 @@
val morph_fp_result: morphism -> fp_result -> fp_result
+ type fp_sugar =
+ {T: typ,
+ BT: typ,
+ X: typ,
+ fp: BNF_Util.fp_kind,
+ fp_res_index: int,
+ fp_res: fp_result,
+ pre_bnf: BNF_Def.bnf,
+ absT_info: BNF_Comp.absT_info,
+ nested_bnfs: BNF_Def.bnf list,
+ nesting_bnfs: BNF_Def.bnf list,
+ ctrXs_Tss: typ list list,
+ ctr_defs: thm list,
+ ctr_sugar: Ctr_Sugar.ctr_sugar,
+ co_rec: term,
+ co_rec_def: thm,
+ maps: thm list,
+ common_co_inducts: thm list,
+ co_inducts: thm list,
+ co_rec_thms: thm list,
+ disc_co_recs: thm list,
+ sel_co_recss: thm list list,
+ rel_injects: thm list,
+ rel_distincts: thm list};
+
+ val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
+ val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar
+
val time: Proof.context -> Timer.real_timer -> string -> Timer.real_timer
val fixpoint: ('a * 'a -> bool) -> ('a list -> 'a list) -> 'a list -> 'a list
@@ -184,6 +212,7 @@
structure BNF_FP_Util : BNF_FP_UTIL =
struct
+open Ctr_Sugar
open BNF_Comp
open BNF_Def
open BNF_Util
@@ -226,6 +255,60 @@
xtor_co_rec_o_map_thms = map (Morphism.thm phi) xtor_co_rec_o_map_thms,
rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm};
+type fp_sugar =
+ {T: typ,
+ BT: typ,
+ X: typ,
+ fp: fp_kind,
+ fp_res_index: int,
+ fp_res: fp_result,
+ pre_bnf: bnf,
+ absT_info: absT_info,
+ nested_bnfs: bnf list,
+ nesting_bnfs: bnf list,
+ ctrXs_Tss: typ list list,
+ ctr_defs: thm list,
+ ctr_sugar: Ctr_Sugar.ctr_sugar,
+ co_rec: term,
+ co_rec_def: thm,
+ maps: thm list,
+ common_co_inducts: thm list,
+ co_inducts: thm list,
+ co_rec_thms: thm list,
+ disc_co_recs: thm list,
+ sel_co_recss: thm list list,
+ rel_injects: thm list,
+ rel_distincts: thm list};
+
+fun morph_fp_sugar phi ({T, BT, X, fp, fp_res, fp_res_index, pre_bnf, absT_info, nested_bnfs,
+ nesting_bnfs, ctrXs_Tss, ctr_defs, ctr_sugar, co_rec, co_rec_def, maps, common_co_inducts,
+ co_inducts, co_rec_thms, disc_co_recs, sel_co_recss, rel_injects, rel_distincts} : fp_sugar) =
+ {T = Morphism.typ phi T,
+ BT = Morphism.typ phi BT,
+ X = Morphism.typ phi X,
+ fp = fp,
+ fp_res = morph_fp_result phi fp_res,
+ fp_res_index = fp_res_index,
+ pre_bnf = morph_bnf phi pre_bnf,
+ absT_info = morph_absT_info phi absT_info,
+ nested_bnfs = map (morph_bnf phi) nested_bnfs,
+ nesting_bnfs = map (morph_bnf phi) nesting_bnfs,
+ ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss,
+ ctr_defs = map (Morphism.thm phi) ctr_defs,
+ ctr_sugar = morph_ctr_sugar phi ctr_sugar,
+ co_rec = Morphism.term phi co_rec,
+ co_rec_def = Morphism.thm phi co_rec_def,
+ maps = map (Morphism.thm phi) maps,
+ common_co_inducts = map (Morphism.thm phi) common_co_inducts,
+ co_inducts = map (Morphism.thm phi) co_inducts,
+ co_rec_thms = map (Morphism.thm phi) co_rec_thms,
+ disc_co_recs = map (Morphism.thm phi) disc_co_recs,
+ sel_co_recss = map (map (Morphism.thm phi)) sel_co_recss,
+ rel_injects = map (Morphism.thm phi) rel_injects,
+ rel_distincts = map (Morphism.thm phi) rel_distincts};
+
+val transfer_fp_sugar = morph_fp_sugar o Morphism.transfer_morphism o Proof_Context.theory_of;
+
fun time ctxt timer msg = (if Config.get ctxt bnf_timing
then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
"ms")
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Wed Apr 23 10:23:27 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Wed Apr 23 10:23:27 2014 +0200
@@ -9,6 +9,7 @@
sig
val register_size: string -> string -> thm list -> thm list -> theory -> theory
val lookup_size: theory -> string -> (string * (thm list * thm list)) option
+ val generate_lfp_size: BNF_FP_Util.fp_sugar list -> theory -> theory
end;
structure BNF_LFP_Size : BNF_LFP_SIZE =
@@ -17,7 +18,7 @@
open BNF_Util
open BNF_Tactics
open BNF_Def
-open BNF_FP_Def_Sugar
+open BNF_FP_Util
val size_N = "size_"
@@ -53,8 +54,7 @@
funpow n (fn thm => thm RS @{thm fun_cong_unused_0} handle THM _ => thm RS fun_cong);
val rec_o_map_simp_thms =
- @{thms o_def id_apply case_prod_app case_sum_o_map_sum case_prod_o_map_prod
- BNF_Comp.id_bnf_comp_def};
+ @{thms o_def id_apply case_prod_app case_sum_map_sum case_prod_map_prod BNF_Comp.id_bnf_comp_def};
fun mk_rec_o_map_tac ctxt rec_def pre_map_defs abs_inverses ctor_rec_o_map =
unfold_thms_tac ctxt [rec_def] THEN
@@ -71,7 +71,7 @@
asm_simp_tac (ss_only (inj_maps @ size_maps @ size_o_map_simp_thms) ctxt)) THEN
IF_UNSOLVED (unfold_thms_tac ctxt @{thms o_def} THEN HEADGOAL (rtac refl));
-fun generate_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP,
+fun generate_lfp_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP,
fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_map_thms = ctor_rec_o_maps, ...}, nested_bnfs,
nesting_bnfs, ...} : fp_sugar) :: _) thy =
let
@@ -335,8 +335,6 @@
Symtab.update_new (T_name, (size_name, (size_simps, flat size_o_map_thmss))))
T_names size_names)
end
- | generate_size _ thy = thy;
-
-val _ = Theory.setup (fp_sugar_interpretation generate_size);
+ | generate_lfp_size _ thy = thy;
end;