--- a/src/HOL/BNF_FP_Base.thy Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/BNF_FP_Base.thy Wed Apr 23 10:23:26 2014 +0200
@@ -89,34 +89,34 @@
lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
by blast
-lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r"
+lemma rewriteR_comp_comp: "\<lbrakk>g \<circ> h = r\<rbrakk> \<Longrightarrow> f \<circ> g \<circ> h = f \<circ> r"
unfolding comp_def fun_eq_iff by auto
-lemma rewriteR_comp_comp2: "\<lbrakk>g o h = r1 o r2; f o r1 = l\<rbrakk> \<Longrightarrow> f o g o h = l o r2"
+lemma rewriteR_comp_comp2: "\<lbrakk>g \<circ> h = r1 \<circ> r2; f \<circ> r1 = l\<rbrakk> \<Longrightarrow> f \<circ> g \<circ> h = l \<circ> r2"
unfolding comp_def fun_eq_iff by auto
-lemma rewriteL_comp_comp: "\<lbrakk>f o g = l\<rbrakk> \<Longrightarrow> f o (g o h) = l o h"
+lemma rewriteL_comp_comp: "\<lbrakk>f \<circ> g = l\<rbrakk> \<Longrightarrow> f \<circ> (g \<circ> h) = l \<circ> h"
unfolding comp_def fun_eq_iff by auto
-lemma rewriteL_comp_comp2: "\<lbrakk>f o g = l1 o l2; l2 o h = r\<rbrakk> \<Longrightarrow> f o (g o h) = l1 o r"
+lemma rewriteL_comp_comp2: "\<lbrakk>f \<circ> g = l1 \<circ> l2; l2 \<circ> h = r\<rbrakk> \<Longrightarrow> f \<circ> (g \<circ> h) = l1 \<circ> r"
unfolding comp_def fun_eq_iff by auto
-lemma convol_o: "<f, g> o h = <f o h, g o h>"
+lemma convol_o: "<f, g> \<circ> h = <f \<circ> h, g \<circ> h>"
unfolding convol_def by auto
-lemma map_prod_o_convol: "map_prod h1 h2 o <f, g> = <h1 o f, h2 o g>"
+lemma map_prod_o_convol: "map_prod h1 h2 \<circ> <f, g> = <h1 \<circ> f, h2 \<circ> g>"
unfolding convol_def by auto
lemma map_prod_o_convol_id: "(map_prod f id \<circ> <id , g>) x = <id \<circ> f , g> x"
unfolding map_prod_o_convol id_comp comp_id ..
-lemma o_case_sum: "h o case_sum f g = case_sum (h o f) (h o g)"
+lemma o_case_sum: "h \<circ> case_sum f g = case_sum (h \<circ> f) (h \<circ> g)"
unfolding comp_def by (auto split: sum.splits)
-lemma case_sum_o_map_sum: "case_sum f g o map_sum h1 h2 = case_sum (f o h1) (g o h2)"
+lemma case_sum_o_map_sum: "case_sum f g \<circ> map_sum h1 h2 = case_sum (f \<circ> h1) (g \<circ> h2)"
unfolding comp_def by (auto split: sum.splits)
-lemma case_sum_o_map_sum_id: "(case_sum id g o map_sum f id) x = case_sum (f o id) g x"
+lemma case_sum_o_map_sum_id: "(case_sum id g \<circ> map_sum f id) x = case_sum (f \<circ> id) g x"
unfolding case_sum_o_map_sum id_comp comp_id ..
lemma rel_fun_def_butlast:
@@ -144,7 +144,7 @@
lemma
assumes "type_definition Rep Abs UNIV"
- shows type_copy_Rep_o_Abs: "Rep \<circ> Abs = id" and type_copy_Abs_o_Rep: "Abs o Rep = id"
+ shows type_copy_Rep_o_Abs: "Rep \<circ> Abs = id" and type_copy_Abs_o_Rep: "Abs \<circ> Rep = id"
unfolding fun_eq_iff comp_apply id_apply
type_definition.Abs_inverse[OF assms UNIV_I] type_definition.Rep_inverse[OF assms] by simp_all
@@ -152,7 +152,7 @@
assumes "type_definition Rep Abs UNIV"
"type_definition Rep' Abs' UNIV"
"type_definition Rep'' Abs'' UNIV"
- shows "Abs' o M o Rep'' = (Abs' o M1 o Rep) o (Abs o M2 o Rep'') \<Longrightarrow> M1 o M2 = M"
+ shows "Abs' \<circ> M \<circ> Rep'' = (Abs' \<circ> M1 \<circ> Rep) \<circ> (Abs \<circ> M2 \<circ> Rep'') \<Longrightarrow> M1 \<circ> M2 = M"
by (rule sym) (auto simp: fun_eq_iff type_definition.Abs_inject[OF assms(2) UNIV_I UNIV_I]
type_definition.Abs_inverse[OF assms(1) UNIV_I]
type_definition.Abs_inverse[OF assms(3) UNIV_I] dest: spec[of _ "Abs'' x" for x])
@@ -160,7 +160,7 @@
lemma vimage2p_id: "vimage2p id id R = R"
unfolding vimage2p_def by auto
-lemma vimage2p_comp: "vimage2p (f1 o f2) (g1 o g2) = vimage2p f2 g2 o vimage2p f1 g1"
+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
ML_file "Tools/BNF/bnf_fp_util.ML"
--- a/src/HOL/BNF_LFP.thy Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/BNF_LFP.thy Wed Apr 23 10:23:26 2014 +0200
@@ -186,12 +186,29 @@
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)
+
+declare [[ML_print_depth = 10000]] (*###*)
+
ML_file "Tools/BNF/bnf_lfp_util.ML"
ML_file "Tools/BNF/bnf_lfp_tactics.ML"
ML_file "Tools/BNF/bnf_lfp.ML"
@@ -201,4 +218,58 @@
hide_fact (open) id_transfer
+datatype_new ('a, 'b) j = J0 | J 'a "('a, 'b) j"
+thm j.size j.rec_o_map j.size_o_map
+
+datatype_new 'a l = N nat nat | C 'a "'a l"
+thm l.size l.rec_o_map l.size_o_map
+
+datatype_new ('a, 'b) x = XN 'b | XC 'a "('a, 'b) x"
+thm x.size x.rec_o_map x.size_o_map
+
+datatype_new
+ 'a tl = TN | TC "'a mt" "'a tl" and
+ 'a mt = MT 'a "'a tl"
+thm tl.size tl.rec_o_map tl.size_o_map
+thm mt.size mt.rec_o_map mt.size_o_map
+
+datatype_new 'a t = T nat 'a "'a t l"
+thm t.size t.rec_o_map t.size_o_map
+
+datatype_new 'a fset = FSet0 | FSet 'a "'a fset"
+thm fset.size fset.rec_o_map fset.size_o_map
+
+datatype_new 'a u = U 'a "'a u fset"
+thm u.size u.rec_o_map u.size_o_map
+
+datatype_new
+ ('a, 'b) v = V "nat l" | V' 'a "('a, 'b) w" and
+ ('a, 'b) w = W 'b "('a, 'b) v fset l"
+thm v.size v.rec_o_map v.size_o_map
+thm w.size w.rec_o_map w.size_o_map
+
+(*TODO:
+* deal with *unused* dead variables and other odd cases (e.g. recursion through fun)
+* what happens if recursion through arbitrary bnf, like 'fsize'?
+ * by default
+ * offer possibility to register size function and theorems
+* non-recursive types use 'case' instead of 'rec', causes trouble (revert?)
+* compat with old size?
+ * recursion of old through new (e.g. through list)?
+ * recursion of new through old?
+ * should they share theory data?
+* code generator setup?
+*)
+
+
end
+datatype_new 'a x = X0 | X 'a (*###*)
+thm x.size
+thm x.size_o_map
+datatype_new 'a x = X0 | X 'a "'a x" (*###*)
+thm x.size
+thm x.size_o_map
+datatype_new 'a l = N | C 'a "'a l"
+datatype_new ('a, 'b) tl = TN 'b | TC 'a "'a l"
+
+end
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Apr 23 10:23:26 2014 +0200
@@ -22,6 +22,7 @@
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,
@@ -137,6 +138,7 @@
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,
@@ -161,6 +163,7 @@
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,
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Wed Apr 23 10:23:26 2014 +0200
@@ -239,7 +239,7 @@
val co_recs = of_fp_res #xtor_co_recs;
val ns = map (length o #Ts o #fp_res) fp_sugars;
- fun substT rho (Type (@{type_name "fun"}, [T, U])) = substT rho T --> substT rho U
+ fun substT rho (Type (@{type_name fun}, [T, U])) = substT rho T --> substT rho U
| substT rho (Type (s, Ts)) = Type (s, map (typ_subst_nonatomic rho) Ts)
| substT _ T = T;
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Wed Apr 23 10:23:26 2014 +0200
@@ -9,13 +9,15 @@
struct
open BNF_Util
+open BNF_Tactics
open BNF_Def
open BNF_FP_Def_Sugar
val size_N = "size_"
+val rec_o_mapN = "rec_o_map"
val sizeN = "size"
-val size_mapN = "size_map"
+val size_o_mapN = "size_o_map"
structure Data = Theory_Data
(
@@ -34,209 +36,287 @@
fun mk_abs_zero_nat T = Term.absdummy T zero_nat;
-fun generate_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs),
- fp_res = {bnfs = fp_bnfs, ...}, common_co_inducts = common_inducts, ...} : fp_sugar) :: _) thy =
- let
- val data = Data.get thy;
+fun pointfill ctxt th = unfold_thms ctxt [o_apply] (th RS fun_cong);
+
+fun mk_unabs_def_unused_0 n =
+ 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};
- val Ts = map #T fp_sugars
- val T_names = map (fst o dest_Type) Ts;
- val nn = length Ts;
+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
+ HEADGOAL (rtac (ctor_rec_o_map RS trans) THEN'
+ K (PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion)) THEN' asm_simp_tac
+ (ss_only (pre_map_defs @ distinct Thm.eq_thm_prop abs_inverses @ rec_o_map_simp_thms) ctxt));
- val B_ify = Term.typ_subst_atomic (As ~~ Bs);
+val size_o_map_simp_thms =
+ @{thms o_apply prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]};
+
+fun mk_size_o_map_tac ctxt size_def rec_o_map inj_maps size_maps =
+ unfold_thms_tac ctxt [size_def] THEN
+ HEADGOAL (rtac (rec_o_map RS trans) THEN'
+ asm_simp_tac (ss_only (inj_maps @ size_maps @ size_o_map_simp_thms) ctxt));
- val recs = map #co_rec fp_sugars;
- val rec_thmss = map #co_rec_thms fp_sugars;
- val rec_Ts = map fastype_of recs;
- val Cs = map body_type rec_Ts;
- val Cs_rho = map (rpair HOLogic.natT) Cs;
- val substCT = Term.subst_atomic_types Cs_rho;
+fun generate_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, ...}
+ : fp_sugar) :: _) thy =
+ let
+ val data = Data.get thy;
+
+ val Ts = map #T fp_sugars
+ val T_names = map (fst o dest_Type) Ts;
+ val nn = length Ts;
+
+ val B_ify = Term.typ_subst_atomic (As ~~ Bs);
- val f_Ts = map mk_to_natT As;
- val f_TsB = map mk_to_natT Bs;
- val num_As = length As;
+ val recs = map #co_rec fp_sugars;
+ val rec_thmss = map #co_rec_thms fp_sugars;
+ val rec_Ts as rec_T1 :: _ = map fastype_of recs;
+ val rec_arg_Ts = binder_fun_types rec_T1;
+ val Cs = map body_type rec_Ts;
+ val Cs_rho = map (rpair HOLogic.natT) Cs;
+ val substCnatT = Term.subst_atomic_types Cs_rho;
- val f_names = map (prefix "f" o string_of_int) (1 upto num_As);
- val fs = map2 (curry Free) f_names f_Ts;
- val fsB = map2 (curry Free) f_names f_TsB;
- val As_fs = As ~~ fs;
+ val f_Ts = map mk_to_natT As;
+ val f_TsB = map mk_to_natT Bs;
+ val num_As = length As;
- val gen_size_names = map (Long_Name.map_base_name (prefix size_N)) T_names;
+ val f_names = map (prefix "f" o string_of_int) (1 upto num_As);
+ val fs = map2 (curry Free) f_names f_Ts;
+ val fsB = map2 (curry Free) f_names f_TsB;
+ val As_fs = As ~~ fs;
- fun is_pair_C @{type_name prod} [_, T'] = member (op =) Cs T'
- | is_pair_C _ _ = false;
+ val size_names = map (Long_Name.map_base_name (prefix size_N)) T_names;
+
+ fun is_pair_C @{type_name prod} [_, T'] = member (op =) Cs T'
+ | is_pair_C _ _ = false;
- fun mk_size_of_typ (T as TFree _) =
- pair (case AList.lookup (op =) As_fs T of
- SOME f => f
- | NONE => if member (op =) Cs T then Term.absdummy T (Bound 0) else mk_abs_zero_nat T)
- | mk_size_of_typ (T as Type (s, Ts)) =
- if is_pair_C s Ts then
- pair (snd_const T)
- else if exists (exists_subtype_in As) Ts then
- (case Symtab.lookup data s of
- SOME (gen_size_name, (_, gen_size_maps)) =>
- let
- val (args, gen_size_mapss') = split_list (map (fn T => mk_size_of_typ T []) Ts);
- val gen_size_const = Const (gen_size_name, map fastype_of args ---> mk_to_natT T);
- in
- fold (union Thm.eq_thm) (gen_size_maps :: gen_size_mapss')
- #> pair (Term.list_comb (gen_size_const, args))
- end
- | NONE => pair (mk_abs_zero_nat T))
- else
- pair (mk_abs_zero_nat T);
+ fun mk_size_of_typ (T as TFree _) =
+ pair (case AList.lookup (op =) As_fs T of
+ SOME f => f
+ | NONE => if member (op =) Cs T then Term.absdummy T (Bound 0) else mk_abs_zero_nat T)
+ | mk_size_of_typ (T as Type (s, Ts)) =
+ if is_pair_C s Ts then
+ pair (snd_const T)
+ else if exists (exists_subtype_in As) Ts then
+ (case Symtab.lookup data s of
+ SOME (size_name, (_, size_o_maps)) =>
+ let
+ val (args, size_o_mapss') = split_list (map (fn T => mk_size_of_typ T []) Ts);
+ val size_const = Const (size_name, map fastype_of args ---> mk_to_natT T);
+ in
+ fold (union Thm.eq_thm) (size_o_maps :: size_o_mapss')
+ #> pair (Term.list_comb (size_const, args))
+ end
+ | NONE => pair (mk_abs_zero_nat T))
+ else
+ pair (mk_abs_zero_nat T);
- fun mk_size_of_arg t =
- mk_size_of_typ (fastype_of t) #>> (fn s => substCT (betapply (s, t)));
+ fun mk_size_of_arg t =
+ mk_size_of_typ (fastype_of t) #>> (fn s => substCnatT (betapply (s, t)));
- fun mk_gen_size_arg arg_T gen_size_maps =
- let
- val x_Ts = binder_types arg_T;
- val m = length x_Ts;
- val x_names = map (prefix "x" o string_of_int) (1 upto m);
- val xs = map2 (curry Free) x_names x_Ts;
- val (summands, gen_size_maps') =
- fold_map mk_size_of_arg xs gen_size_maps
- |>> remove (op =) zero_nat;
- val sum =
- if null summands then HOLogic.zero
- else foldl1 mk_plus_nat (summands @ [HOLogic.Suc_zero]);
- in
- (fold_rev Term.lambda (map substCT xs) sum, gen_size_maps')
- end;
+ fun mk_size_arg rec_arg_T size_o_maps =
+ let
+ val x_Ts = binder_types rec_arg_T;
+ val m = length x_Ts;
+ val x_names = map (prefix "x" o string_of_int) (1 upto m);
+ val xs = map2 (curry Free) x_names x_Ts;
+ val (summands, size_o_maps') =
+ fold_map mk_size_of_arg xs size_o_maps
+ |>> remove (op =) zero_nat;
+ val sum =
+ if null summands then HOLogic.zero
+ else foldl1 mk_plus_nat (summands @ [HOLogic.Suc_zero]);
+ in
+ (fold_rev Term.lambda (map substCnatT xs) sum, size_o_maps')
+ end;
+
+ fun mk_size_rhs recx size_o_maps =
+ let val (args, size_o_maps') = fold_map mk_size_arg rec_arg_Ts size_o_maps in
+ (fold_rev Term.lambda fs (Term.list_comb (substCnatT recx, args)), size_o_maps')
+ end;
+
+ fun mk_def_binding f =
+ Binding.conceal o Binding.name o Thm.def_name o f o Long_Name.base_name;
- fun mk_gen_size_rhs rec_T recx gen_size_maps =
- let
- val arg_Ts = binder_fun_types rec_T;
- val (args, gen_size_maps') = fold_map mk_gen_size_arg arg_Ts gen_size_maps;
- in
- (fold_rev Term.lambda fs (Term.list_comb (substCT recx, args)), gen_size_maps')
- end;
+ val (size_rhss, nested_size_o_maps) = fold_map mk_size_rhs recs [];
+ val size_Ts = map fastype_of size_rhss;
+ val size_consts = map2 (curry Const) size_names size_Ts;
+ val size_constsB = map (Term.map_types B_ify) size_consts;
+ val size_def_bs = map (mk_def_binding I) size_names;
- fun mk_def_binding f = Binding.conceal o Binding.name o Thm.def_name o f o Long_Name.base_name;
+ val (size_defs, thy2) =
+ thy
+ |> Sign.add_consts (map (fn (s, T) => (Binding.name (Long_Name.base_name s), T, NoSyn))
+ (size_names ~~ size_Ts))
+ |> Global_Theory.add_defs false (map Thm.no_attributes (size_def_bs ~~
+ map Logic.mk_equals (size_consts ~~ size_rhss)));
+
+ val zeros = map mk_abs_zero_nat As;
- val (gen_size_rhss, nested_gen_size_maps) = fold_map2 mk_gen_size_rhs rec_Ts recs [];
- val gen_size_Ts = map fastype_of gen_size_rhss;
- val gen_size_consts = map2 (curry Const) gen_size_names gen_size_Ts;
- val gen_size_constsB = map (Term.map_types B_ify) gen_size_consts;
- val gen_size_def_bs = map (mk_def_binding I) gen_size_names;
+ val overloaded_size_rhss = map (fn c => Term.list_comb (c, zeros)) size_consts;
+ val overloaded_size_Ts = map fastype_of overloaded_size_rhss;
+ val overloaded_size_consts = map (curry Const @{const_name size}) overloaded_size_Ts;
+ val overloaded_size_def_bs = map (mk_def_binding (suffix "_overloaded")) size_names;
- val (gen_size_defs, thy2) =
- thy
- |> Sign.add_consts (map (fn (s, T) => (Binding.name (Long_Name.base_name s), T, NoSyn))
- (gen_size_names ~~ gen_size_Ts))
- |> Global_Theory.add_defs false (map Thm.no_attributes (gen_size_def_bs ~~
- map Logic.mk_equals (gen_size_consts ~~ gen_size_rhss)));
-
- val zeros = map mk_abs_zero_nat As;
-
- val spec_size_rhss = map (fn c => Term.list_comb (c, zeros)) gen_size_consts;
- val spec_size_Ts = map fastype_of spec_size_rhss;
- val spec_size_consts = map (curry Const @{const_name size}) spec_size_Ts;
- val spec_size_def_bs = map (mk_def_binding (suffix "_overloaded")) gen_size_names;
+ fun define_overloaded_size def_b lhs0 rhs lthy =
+ let
+ val Free (c, _) = Syntax.check_term lthy lhs0;
+ val (thm, lthy') = lthy
+ |> Local_Theory.define ((Binding.name c, NoSyn), ((def_b, []), rhs))
+ |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
+ val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
+ val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
+ in (thm', lthy') end;
- fun define_spec_size def_b lhs0 rhs lthy =
- let
- val Free (c, _) = Syntax.check_term lthy lhs0;
- val (thm, lthy') = lthy
- |> Local_Theory.define ((Binding.name c, NoSyn), ((def_b, []), rhs))
- |-> (fn (t, (_, thm)) => Spec_Rules.add Spec_Rules.Equational ([t], [thm]) #> pair thm);
- val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
- val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm;
- in (thm', lthy') end;
+ val (overloaded_size_defs, thy3) = thy2
+ |> Class.instantiation (T_names, map dest_TFree As, [HOLogic.class_size])
+ |> fold_map3 define_overloaded_size overloaded_size_def_bs overloaded_size_consts
+ overloaded_size_rhss
+ ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
+ ||> Local_Theory.exit_global;
+
+ val thy3_ctxt = Proof_Context.init_global thy3;
+
+ val size_defs' =
+ map (mk_unabs_def (num_As + 1) o (fn thm => thm RS meta_eq_to_obj_eq)) size_defs;
+ val size_defs_unused_0 =
+ map (mk_unabs_def_unused_0 (num_As + 1) o (fn thm => thm RS meta_eq_to_obj_eq)) size_defs;
+ val overloaded_size_defs' =
+ map (mk_unabs_def 1 o (fn thm => thm RS meta_eq_to_obj_eq)) overloaded_size_defs;
- val (spec_size_defs, thy3) = thy2
- |> Class.instantiation (T_names, map dest_TFree As, [HOLogic.class_size])
- |> fold_map3 define_spec_size spec_size_def_bs spec_size_consts spec_size_rhss
- ||> Class.prove_instantiation_instance (K (Class.intro_classes_tac []))
- ||> Local_Theory.exit_global;
+ val nested_size_maps = map (pointfill thy3_ctxt) nested_size_o_maps @ nested_size_o_maps;
+ val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ nested_bnfs);
- val thy3_ctxt = Proof_Context.init_global thy3;
+ fun derive_size_simp size_def' simp0 =
+ (trans OF [size_def', simp0])
+ |> Simplifier.asm_full_simplify (ss_only (@{thms inj_on_convol_id snd_o_convol} @
+ all_inj_maps @ nested_size_maps) thy3_ctxt)
+ |> fold_thms thy3_ctxt size_defs_unused_0;
+ fun derive_overloaded_size_simp size_def' simp0 =
+ (trans OF [size_def', simp0])
+ |> unfold_thms thy3_ctxt @{thms add_0_left add_0_right}
+ |> fold_thms thy3_ctxt overloaded_size_defs';
- val gen_size_defs' =
- map (mk_unabs_def (num_As + 1) o (fn thm => thm RS meta_eq_to_obj_eq)) gen_size_defs;
- val spec_size_defs' =
- map (mk_unabs_def 1 o (fn thm => thm RS meta_eq_to_obj_eq)) spec_size_defs;
+ val size_simpss = map2 (map o derive_size_simp) size_defs' rec_thmss;
+ val size_simps = flat size_simpss;
+ val overloaded_size_simpss =
+ map2 (map o derive_overloaded_size_simp) overloaded_size_defs' size_simpss;
- fun derive_size_simp unfolds folds size_def' simp0 =
- fold_thms thy3_ctxt folds (unfold_thms thy3_ctxt unfolds (trans OF [size_def', simp0]));
- val derive_gen_size_simp =
- derive_size_simp (@{thm snd_o_convol} :: nested_gen_size_maps) gen_size_defs';
- val derive_spec_size_simp = derive_size_simp @{thms add_0_left add_0_right} spec_size_defs';
+ val ABs = As ~~ Bs;
+ val g_names = map (prefix "g" o string_of_int) (1 upto num_As);
+ val gs = map2 (curry Free) g_names (map (op -->) ABs);
- val gen_size_simpss = map2 (map o derive_gen_size_simp) gen_size_defs' rec_thmss;
- val gen_size_simps = flat gen_size_simpss;
- val spec_size_simpss = map2 (map o derive_spec_size_simp) spec_size_defs' gen_size_simpss;
+ val liveness = map (op <>) ABs;
+ val live_gs = AList.find (op =) (gs ~~ liveness) true;
+ val live = length live_gs;
- val ABs = As ~~ Bs;
- val g_names = map (prefix "g" o string_of_int) (1 upto num_As);
- val gs = map2 (curry Free) g_names (map (op -->) ABs);
+ val maps0 = map map_of_bnf fp_bnfs;
- val liveness = map (op <>) ABs;
- val live_gs = AList.find (op =) (gs ~~ liveness) true;
- val live = length live_gs;
+ val (rec_o_map_thmss, size_o_map_thmss) =
+ if live = 0 then
+ `I (replicate nn [])
+ else
+ let
+ val pre_bnfs = map #pre_bnf fp_sugars;
+ val pre_map_defs = map map_def_of_bnf pre_bnfs;
+ val abs_inverses = map (#abs_inverse o #absT_info) fp_sugars;
+ val rec_defs = map #co_rec_def fp_sugars;
- val u_names = map (prefix "u" o string_of_int) (1 upto nn);
- val us = map2 (curry Free) u_names Ts;
+ val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0;
- val maps0 = map map_of_bnf fp_bnfs;
- val map_thms = maps #maps fp_sugars;
+ val num_rec_args = length rec_arg_Ts;
+ val h_Ts = map B_ify rec_arg_Ts;
+ val h_names = map (prefix "h" o string_of_int) (1 upto num_rec_args);
+ val hs = map2 (curry Free) h_names h_Ts;
+ val hrecs = map (fn recx => Term.list_comb (Term.map_types B_ify recx, hs)) recs;
- fun mk_gen_size_map_tac ctxt =
- HEADGOAL (rtac (co_induct_of common_inducts)) THEN
- ALLGOALS (asm_simp_tac (ss_only (o_apply :: map_thms @ gen_size_simps) ctxt));
+ val rec_o_map_lhss = map2 (curry HOLogic.mk_comp) hrecs gmaps;
+
+ val ABgs = ABs ~~ gs;
+
+ fun mk_rec_arg_arg (x as Free (_, T)) =
+ let val U = B_ify T in
+ if T = U then x else build_map thy3_ctxt (the o AList.lookup (op =) ABgs) (T, U) $ x
+ end;
- val gen_size_map_thmss =
- if live = 0 then
- replicate nn []
- else if null nested_gen_size_maps then
- let
- val xgmaps =
- map2 (fn map0 => fn u => Term.list_comb (mk_map live As Bs map0, live_gs) $ u) maps0 us;
- val fsizes =
- map (fn gen_size_constB => Term.list_comb (gen_size_constB, fsB)) gen_size_constsB;
- val lhss = map2 (curry (op $)) fsizes xgmaps;
+ fun mk_rec_o_map_arg rec_arg_T h =
+ let
+ val x_Ts = binder_types rec_arg_T;
+ val m = length x_Ts;
+ val x_names = map (prefix "x" o string_of_int) (1 upto m);
+ val xs = map2 (curry Free) x_names x_Ts;
+ val xs' = map mk_rec_arg_arg xs;
+ in
+ fold_rev Term.lambda xs (Term.list_comb (h, xs'))
+ end;
+
+ fun mk_rec_o_map_rhs recx =
+ let val args = map2 mk_rec_o_map_arg rec_arg_Ts hs in
+ Term.list_comb (recx, args)
+ end;
+
+ val rec_o_map_rhss = map mk_rec_o_map_rhs recs;
- val fgs = map2 (fn fB => fn g as Free (_, Type (_, [A, B])) =>
- if A = B then fB else HOLogic.mk_comp (fB, g)) fsB gs;
- val rhss = map2 (fn gen_size_const => fn u => Term.list_comb (gen_size_const, fgs) $ u)
- gen_size_consts us;
+ val rec_o_map_goals =
+ map2 (HOLogic.mk_Trueprop oo curry HOLogic.mk_eq) rec_o_map_lhss rec_o_map_rhss;
+ val rec_o_map_thms =
+ map3 (fn goal => fn rec_def => fn ctor_rec_o_map =>
+ Goal.prove_global thy3 [] [] goal (fn {context = ctxt, ...} =>
+ mk_rec_o_map_tac ctxt rec_def pre_map_defs abs_inverses ctor_rec_o_map)
+ |> Thm.close_derivation)
+ rec_o_map_goals rec_defs ctor_rec_o_maps;
+
+ val size_o_map_conds =
+ if exists (can Logic.dest_implies o Thm.prop_of) nested_size_o_maps then
+ map (HOLogic.mk_Trueprop o mk_inj) live_gs
+ else
+ [];
+
+ val fsizes = map (fn size_constB => Term.list_comb (size_constB, fsB)) size_constsB;
+ val size_o_map_lhss = map2 (curry HOLogic.mk_comp) fsizes gmaps;
- val goal = Library.foldr1 HOLogic.mk_conj (map2 (curry HOLogic.mk_eq) lhss rhss)
- |> HOLogic.mk_Trueprop;
- in
- Goal.prove_global thy3 [] [] goal (mk_gen_size_map_tac o #context)
- |> Thm.close_derivation
- |> conj_dests nn
- |> map single
- end
- else
- (* TODO: implement general case, with nesting of datatypes that themselves nest other
- types *)
- replicate nn [];
+ val fgs = map2 (fn fB => fn g as Free (_, Type (_, [A, B])) =>
+ if A = B then fB else HOLogic.mk_comp (fB, g)) fsB gs;
+ val size_o_map_rhss = map (fn c => Term.list_comb (c, fgs)) size_consts;
+
+ val size_o_map_goals =
+ map2 (curry Logic.list_implies size_o_map_conds o HOLogic.mk_Trueprop oo
+ curry HOLogic.mk_eq) size_o_map_lhss size_o_map_rhss;
+ val size_o_map_thms =
+ map3 (fn goal => fn size_def => fn rec_o_map =>
+ Goal.prove_global thy3 [] [] goal (fn {context = ctxt, ...} =>
+ mk_size_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps)
+ |> Thm.close_derivation)
+ size_o_map_goals size_defs rec_o_map_thms;
+ in
+ pairself (map single) (rec_o_map_thms, size_o_map_thms)
+ end;
- val (_, thy4) = thy3
- |> fold_map3 (fn T_name => fn size_simps => fn gen_size_map_thms =>
- let val qualify = Binding.qualify true (Long_Name.base_name T_name) in
- Global_Theory.note_thmss ""
- ([((qualify (Binding.name sizeN),
- [Simplifier.simp_add, Nitpick_Simps.add, Thm.declaration_attribute
- (fn thm => Context.mapping (Code.add_default_eqn thm) I)]),
- [(size_simps, [])]),
- ((qualify (Binding.name size_mapN), []), [(gen_size_map_thms, [])])]
- |> filter_out (forall (null o fst) o snd))
- end)
- T_names (map2 append gen_size_simpss spec_size_simpss) gen_size_map_thmss
- ||> Spec_Rules.add_global Spec_Rules.Equational (gen_size_consts, gen_size_simps);
- in
- thy4
- |> Data.map (fold2 (fn T_name => fn gen_size_name =>
- Symtab.update_new (T_name, (gen_size_name, (gen_size_simps, flat gen_size_map_thmss))))
- T_names gen_size_names)
- end;
+ val (_, thy4) = thy3
+ |> fold_map4 (fn T_name => fn size_simps => fn rec_o_map_thms => fn size_o_map_thms =>
+ let val qualify = Binding.qualify true (Long_Name.base_name T_name) in
+ Global_Theory.note_thmss ""
+ ([((qualify (Binding.name rec_o_mapN), []), [(rec_o_map_thms, [])]),
+ ((qualify (Binding.name sizeN),
+ [Simplifier.simp_add, Nitpick_Simps.add, Thm.declaration_attribute
+ (fn thm => Context.mapping (Code.add_default_eqn thm) I)]),
+ [(size_simps, [])]),
+ ((qualify (Binding.name size_o_mapN), []), [(size_o_map_thms, [])])]
+ |> filter_out (forall (null o fst) o snd))
+ end)
+ T_names (map2 append size_simpss overloaded_size_simpss) rec_o_map_thmss size_o_map_thmss
+ ||> Spec_Rules.add_global Spec_Rules.Equational (size_consts, size_simps);
+ in
+ thy4
+ |> Data.map (fold2 (fn T_name => fn size_name =>
+ Symtab.update_new (T_name, (size_name, (size_simps, flat size_o_map_thmss))))
+ T_names size_names)
+ end
+ | generate_size _ thy = thy;
-(* FIXME: get rid of "perhaps o try" once the code is stable *)
-val _ = Theory.setup (fp_sugar_interpretation (perhaps o try o generate_size));
+val _ = Theory.setup (fp_sugar_interpretation generate_size);
end;
--- a/src/HOL/Tools/BNF/bnf_util.ML Wed Apr 23 10:23:26 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML Wed Apr 23 10:23:26 2014 +0200
@@ -215,7 +215,6 @@
map15 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s x14s x15s
| map15 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths;
-
fun fold_map4 _ [] [] [] [] acc = ([], acc)
| fold_map4 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) acc =
let