# HG changeset patch # User blanchet # Date 1398241406 -7200 # Node ID 0a35354137a5e7abf48d2b111ecd6ae81a511110 # Parent c9d6b581bd3be343d95249e218eaee9137d7ab96 generate 'rec_o_map' and 'size_o_map' in size extension diff -r c9d6b581bd3b -r 0a35354137a5 src/HOL/BNF_FP_Base.thy --- 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: "\x y. P x y \ P x y" by blast -lemma rewriteR_comp_comp: "\g o h = r\ \ f o g o h = f o r" +lemma rewriteR_comp_comp: "\g \ h = r\ \ f \ g \ h = f \ r" unfolding comp_def fun_eq_iff by auto -lemma rewriteR_comp_comp2: "\g o h = r1 o r2; f o r1 = l\ \ f o g o h = l o r2" +lemma rewriteR_comp_comp2: "\g \ h = r1 \ r2; f \ r1 = l\ \ f \ g \ h = l \ r2" unfolding comp_def fun_eq_iff by auto -lemma rewriteL_comp_comp: "\f o g = l\ \ f o (g o h) = l o h" +lemma rewriteL_comp_comp: "\f \ g = l\ \ f \ (g \ h) = l \ h" unfolding comp_def fun_eq_iff by auto -lemma rewriteL_comp_comp2: "\f o g = l1 o l2; l2 o h = r\ \ f o (g o h) = l1 o r" +lemma rewriteL_comp_comp2: "\f \ g = l1 \ l2; l2 \ h = r\ \ f \ (g \ h) = l1 \ r" unfolding comp_def fun_eq_iff by auto -lemma convol_o: " o h = " +lemma convol_o: " \ h = h, g \ h>" unfolding convol_def by auto -lemma map_prod_o_convol: "map_prod h1 h2 o =

" +lemma map_prod_o_convol: "map_prod h1 h2 \ =

f, h2 \ g>" unfolding convol_def by auto lemma map_prod_o_convol_id: "(map_prod f id \ ) x = 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 \ case_sum f g = case_sum (h \ f) (h \ 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 \ map_sum h1 h2 = case_sum (f \ h1) (g \ 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 \ map_sum f id) x = case_sum (f \ 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 \ Abs = id" and type_copy_Abs_o_Rep: "Abs o Rep = id" + shows type_copy_Rep_o_Abs: "Rep \ Abs = id" and type_copy_Abs_o_Rep: "Abs \ 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'') \ M1 o M2 = M" + shows "Abs' \ M \ Rep'' = (Abs' \ M1 \ Rep) \ (Abs \ M2 \ Rep'') \ M1 \ 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 \ f2) (g1 \ g2) = vimage2p f2 g2 \ vimage2p f1 g1" unfolding fun_eq_iff vimage2p_def o_apply by simp ML_file "Tools/BNF/bnf_fp_util.ML" diff -r c9d6b581bd3b -r 0a35354137a5 src/HOL/BNF_LFP.thy --- 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: "\(r, s) \ R; s' = s\ \ (r, s') \ R" by (rule ssubst) +lemma fun_cong_unused_0: "f = (\x. g) \ f (\x. 0) = g" + by (erule arg_cong) + lemma snd_o_convol: "(snd \ (\x. (f x, g x))) = g" by (rule ext) simp lemma inj_on_convol_id: "inj_on (\x. (x, f x)) X" unfolding inj_on_def by simp +lemma case_prod_app: "case_prod f x y = case_prod (\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 \ f) (r \ g) x" + by (case_tac x) simp+ + +lemma case_prod_o_map_prod: "case_prod h (map_prod f g x) = case_prod (\l r. h (f l) (g r)) x" + by (case_tac x) simp+ + +lemma prod_inj_map: "inj f \ inj g \ 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 diff -r c9d6b581bd3b -r 0a35354137a5 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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, diff -r c9d6b581bd3b -r 0a35354137a5 src/HOL/Tools/BNF/bnf_fp_n2m.ML --- 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; diff -r c9d6b581bd3b -r 0a35354137a5 src/HOL/Tools/BNF/bnf_lfp_size.ML --- 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; diff -r c9d6b581bd3b -r 0a35354137a5 src/HOL/Tools/BNF/bnf_util.ML --- 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