# HG changeset patch # User blanchet # Date 1409814163 -7200 # Node ID 2de7b0313de33f40f64db906d42ac5ee081d3a4d # Parent 695ba3101b37acf33f39b2c3b8fe30383d63cf43 tuned size function generation diff -r 695ba3101b37 -r 2de7b0313de3 src/HOL/BNF_Fixpoint_Base.thy --- a/src/HOL/BNF_Fixpoint_Base.thy Thu Sep 04 09:02:36 2014 +0200 +++ b/src/HOL/BNF_Fixpoint_Base.thy Thu Sep 04 09:02:43 2014 +0200 @@ -200,34 +200,9 @@ 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/old_size.ML" -setup Old_Size.setup - -lemma size_bool[code]: "size (b\bool) = 0" - by (cases b) auto - -lemma size_nat[simp, code]: "size (n\nat) = n" - by (induct n) simp_all - -declare prod.size[no_atp] - -lemma size_sum_o_map: "size_sum g1 g2 \ map_sum f1 f2 = size_sum (g1 \ f1) (g2 \ f2)" - by (rule ext) (case_tac x, auto) - -lemma size_prod_o_map: "size_prod g1 g2 \ map_prod f1 f2 = size_prod (g1 \ f1) (g2 \ f2)" - by (rule ext) auto - -setup {* -BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size} - @{thms size_sum_o_map} -#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size} - @{thms size_prod_o_map} -*} - end diff -r 695ba3101b37 -r 2de7b0313de3 src/HOL/BNF_Least_Fixpoint.thy --- a/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 04 09:02:36 2014 +0200 +++ b/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 04 09:02:43 2014 +0200 @@ -186,6 +186,29 @@ 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" +ML_file "Tools/BNF/bnf_lfp_size.ML" +ML_file "Tools/Function/old_size.ML" + +lemma size_bool[code]: "size (b\bool) = 0" + by (cases b) auto + +lemma size_nat[simp, code]: "size (n\nat) = n" + by (induct n) simp_all + +declare prod.size[no_atp] + +lemma size_sum_o_map: "size_sum g1 g2 \ map_sum f1 f2 = size_sum (g1 \ f1) (g2 \ f2)" + by (rule ext) (case_tac x, auto) + +lemma size_prod_o_map: "size_prod g1 g2 \ map_prod f1 f2 = size_prod (g1 \ f1) (g2 \ f2)" + by (rule ext) auto + +setup {* +BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size} + @{thms size_sum_o_map} +#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size} + @{thms size_prod_o_map} +*} hide_fact (open) id_transfer diff -r 695ba3101b37 -r 2de7b0313de3 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 04 09:02:36 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Thu Sep 04 09:02:43 2014 +0200 @@ -97,7 +97,6 @@ open BNF_Def open BNF_FP_Util open BNF_FP_Def_Sugar_Tactics -open BNF_LFP_Size val EqN = "Eq_"; @@ -174,12 +173,11 @@ val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_repaired_path; -fun register_fp_sugars (fp_sugars as {fp, ...} :: _) = +fun register_fp_sugars fp_sugars = 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 - #> fp = Least_FP ? generate_lfp_size fp_sugars #> FP_Sugar_Interpretation.data fp_sugars; fun interpret_bnfs_register_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs @@ -1726,9 +1724,8 @@ if null goals then [] else Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) - (fn {context = ctxt, prems = _} => - mk_disc_transfer_tac ctxt (the_single rel_sel_thms) - (the_single exhaust_discs) (flat (flat distinct_discsss))) + (K (mk_disc_transfer_tac (the_single rel_sel_thms) + (the_single exhaust_discs) (flat (flat distinct_discsss)))) |> Conjunction.elim_balanced (length goals) |> Proof_Context.export names_lthy lthy |> map Thm.close_derivation @@ -2110,6 +2107,6 @@ fun parse_co_datatype_cmd fp construct_fp = parse_co_datatype >> co_datatype_cmd fp construct_fp; -val _ = Context.>> (Context.map_theory FP_Sugar_Interpretation.init); +val _ = Theory.setup FP_Sugar_Interpretation.init; end; diff -r 695ba3101b37 -r 2de7b0313de3 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Sep 04 09:02:36 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Sep 04 09:02:43 2014 +0200 @@ -22,7 +22,7 @@ val mk_ctor_iff_dtor_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm -> tactic val mk_ctr_transfer_tac: thm list -> tactic - val mk_disc_transfer_tac: Proof.context -> thm -> thm -> thm list -> tactic + val mk_disc_transfer_tac: thm -> thm -> thm list -> tactic val mk_exhaust_tac: Proof.context -> int -> thm list -> thm -> thm -> tactic val mk_half_distinct_tac: Proof.context -> thm -> thm -> thm list -> tactic val mk_induct_tac: Proof.context -> int -> int list -> int list list -> int list list list -> @@ -103,7 +103,7 @@ ALLGOALS (REPEAT o (resolve_tac (@{thm rel_funI} :: rel_intros) THEN' REPEAT_DETERM o atac)); -fun mk_disc_transfer_tac ctxt rel_sel exhaust_disc distinct_disc= +fun mk_disc_transfer_tac rel_sel exhaust_disc distinct_disc= let fun last_disc_tac iffD = HEADGOAL (rtac (rotate_prems ~1 exhaust_disc) THEN' atac THEN' diff -r 695ba3101b37 -r 2de7b0313de3 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Sep 04 09:02:36 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Sep 04 09:02:43 2014 +0200 @@ -113,8 +113,7 @@ |> map_filter I; (* TODO: test with sort constraints on As *) -fun mutualize_fp_sugars fp cliques bs fpTs callers callssss (fp_sugars0 as fp_sugars01 :: _) - no_defs_lthy0 = +fun mutualize_fp_sugars fp cliques bs fpTs callers callssss fp_sugars0 no_defs_lthy0 = let val thy = Proof_Context.theory_of no_defs_lthy0; diff -r 695ba3101b37 -r 2de7b0313de3 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Thu Sep 04 09:02:36 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Sep 04 09:02:43 2014 +0200 @@ -2432,11 +2432,11 @@ mk_wit_tac ctxt n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms; val (Jbnfs, lthy) = - fold_map7 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn wit_thms => + fold_map6 (fn tacs => fn map_b => fn rel_b => fn set_bs => fn wit_thms => fn consts => bnf_def Hardly_Inline (user_policy Note_Some) false I tacs (wit_tac wit_thms) (SOME deads) map_b rel_b set_bs consts) - bs tacss map_bs rel_bs set_bss wit_thmss + tacss map_bs rel_bs set_bss wit_thmss ((((((replicate n Binding.empty ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ all_witss) ~~ map SOME Jrels) lthy; diff -r 695ba3101b37 -r 2de7b0313de3 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Sep 04 09:02:36 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Sep 04 09:02:43 2014 +0200 @@ -1720,10 +1720,10 @@ mk_wit_tac ctxt n (flat ctor_Iset_thmss) (maps wit_thms_of_bnf bnfs); val (Ibnfs, lthy) = - fold_map6 (fn b => fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts => + fold_map5 (fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts => bnf_def Do_Inline (user_policy Note_Some) false I tacs wit_tac (SOME deads) map_b rel_b set_bs consts) - bs tacss map_bs rel_bs set_bss + tacss map_bs rel_bs set_bss ((((((replicate n Binding.empty ~~ Ts) ~~ Imaps) ~~ Isetss_by_bnf) ~~ Ibds) ~~ Iwitss) ~~ map SOME Irels) lthy; diff -r 695ba3101b37 -r 2de7b0313de3 src/HOL/Tools/BNF/bnf_lfp_compat.ML --- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Sep 04 09:02:36 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Sep 04 09:02:43 2014 +0200 @@ -331,10 +331,7 @@ |> snd end; -fun datatype_compat_global fpT_names = - Named_Target.theory_init - #> datatype_compat fpT_names - #> Named_Target.exit; +val datatype_compat_global = map_local_theory o datatype_compat; fun datatype_compat_cmd raw_fpT_names lthy = let @@ -360,9 +357,7 @@ in (fpT_names, thy - |> Named_Target.theory_init - |> co_datatypes Least_FP construct_lfp ((false, false), new_specs) - |> Named_Target.exit + |> map_local_theory (co_datatypes Least_FP construct_lfp ((false, false), new_specs)) |> nesting_pref = Unfold_Nesting ? perhaps (try (datatype_compat_global fpT_names))) end; diff -r 695ba3101b37 -r 2de7b0313de3 src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Sep 04 09:02:36 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Sep 04 09:02:43 2014 +0200 @@ -9,9 +9,8 @@ sig val register_size: string -> string -> thm list -> thm list -> local_theory -> local_theory val register_size_global: string -> string -> thm list -> thm list -> theory -> theory - val lookup_size: Proof.context -> string -> (string * (thm list * thm list)) option - val lookup_size_global: theory -> string -> (string * (thm list * thm list)) option - val generate_lfp_size: BNF_FP_Util.fp_sugar list -> local_theory -> local_theory + val size_of: Proof.context -> string -> (string * (thm list * thm list)) option + val size_of_global: theory -> string -> (string * (thm list * thm list)) option end; structure BNF_LFP_Size : BNF_LFP_SIZE = @@ -21,6 +20,7 @@ open BNF_Tactics open BNF_Def open BNF_FP_Util +open BNF_FP_Def_Sugar val size_N = "size_" @@ -46,8 +46,8 @@ fun register_size_global T_name size_name size_simps size_o_maps = Context.theory_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_o_maps))))); -val lookup_size = Symtab.lookup o Data.get o Context.Proof; -val lookup_size_global = Symtab.lookup o Data.get o Context.Theory; +val size_of = Symtab.lookup o Data.get o Context.Proof; +val size_of_global = Symtab.lookup o Data.get o Context.Theory; val zero_nat = @{const zero_class.zero (nat)}; @@ -84,292 +84,297 @@ 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_lfp_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), - fp_res = {bnfs = fp_bnfs, xtor_co_rec_o_map_thms = ctor_rec_o_maps, ...}, fp_nesting_bnfs, - live_nesting_bnfs, ...} : fp_sugar) :: _) lthy0 = - let - val data = Data.get (Context.Proof lthy0); - - 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 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_Ts = map mk_to_natT As; - val f_TsB = map mk_to_natT Bs; - val num_As = length As; - - fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy0); - - val f_names = variant_names num_As "f"; - val fs = map2 (curry Free) f_names f_Ts; - val fsB = map2 (curry Free) f_names f_TsB; - val As_fs = As ~~ fs; +fun generate_datatype_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, ...}, fp_nesting_bnfs, + live_nesting_bnfs, ...} : fp_sugar) :: _) lthy0 = + let + val data = Data.get (Context.Proof lthy0); - val size_bs = - map ((fn base => Binding.qualify false base (Binding.name (prefix size_N base))) o - Long_Name.base_name) T_names; - - fun is_pair_C @{type_name prod} [_, T'] = member (op =) Cs T' - | is_pair_C _ _ = false; + val Ts = map #T fp_sugars + val T_names = map (fst o dest_Type) Ts; + val nn = length Ts; - 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 @ Cs)) 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_prop) (size_o_maps :: size_o_mapss') - #> pair (Term.list_comb (size_const, args)) - end - | _ => 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 => substCnatT (betapply (s, t))); + val B_ify = Term.typ_subst_atomic (As ~~ Bs); - 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 = variant_names m "x"; - 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; + 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; - fun mk_size_rhs recx size_o_maps = - fold_map mk_size_arg rec_arg_Ts size_o_maps - |>> (fn args => fold_rev Term.lambda fs (Term.list_comb (substCnatT recx, args))); - - val maybe_conceal_def_binding = Thm.def_binding - #> Config.get lthy0 bnf_note_all = false ? Binding.conceal; - - val (size_rhss, nested_size_o_maps) = fold_map mk_size_rhs recs []; - val size_Ts = map fastype_of size_rhss; - - val ((raw_size_consts, raw_size_defs), (lthy1', lthy1)) = lthy0 - |> apfst split_list o fold_map2 (fn b => fn rhs => - Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs)) #>> apsnd snd) - size_bs size_rhss - ||> `Local_Theory.restore; + val f_Ts = map mk_to_natT As; + val f_TsB = map mk_to_natT Bs; + val num_As = length As; - val phi = Proof_Context.export_morphism lthy1 lthy1'; - - val size_defs = map (Morphism.thm phi) raw_size_defs; - - val size_consts0 = map (Morphism.term phi) raw_size_consts; - val size_consts = map2 retype_const_or_free size_Ts size_consts0; - val size_constsB = map (Term.map_types B_ify) size_consts; + fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy0); - val zeros = map mk_abs_zero_nat As; - - 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 (maybe_conceal_def_binding o Binding.suffix_name "_overloaded") size_bs; + val f_names = variant_names num_As "f"; + val fs = map2 (curry Free) f_names f_Ts; + val fsB = map2 (curry Free) f_names f_TsB; + val As_fs = As ~~ fs; - 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; + val size_bs = + map ((fn base => Binding.qualify false base (Binding.name (prefix size_N base))) o + Long_Name.base_name) T_names; - val (overloaded_size_defs, lthy2) = lthy1 - |> Local_Theory.background_theory_result - (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); + fun is_pair_C @{type_name prod} [_, T'] = member (op =) Cs T' + | is_pair_C _ _ = false; - 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 all_overloaded_size_defs = overloaded_size_defs @ - (Spec_Rules.retrieve lthy0 @{const size ('a)} - |> map_filter (try (fn (Spec_Rules.Equational, (_, [thm])) => thm))); - - val nested_size_maps = map (pointfill lthy2) nested_size_o_maps @ nested_size_o_maps; - val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ fp_nesting_bnfs @ live_nesting_bnfs) - |> distinct Thm.eq_thm_prop; - - fun derive_size_simp size_def' simp0 = - (trans OF [size_def', simp0]) - |> Simplifier.asm_full_simplify (ss_only (@{thms inj_on_convol_ident id_def o_def snd_conv} @ - all_inj_maps @ nested_size_maps) lthy2) - |> fold_thms lthy2 size_defs_unused_0; - - fun derive_overloaded_size_simp overloaded_size_def' simp0 = - (trans OF [overloaded_size_def', simp0]) - |> unfold_thms lthy2 @{thms add_0_left add_0_right} - |> fold_thms lthy2 all_overloaded_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; - val size_thmss = map2 append size_simpss overloaded_size_simpss; - - val ABs = As ~~ Bs; - val g_names = variant_names num_As "g"; - val gs = map2 (curry Free) g_names (map (op -->) ABs); - - val liveness = map (op <>) ABs; - val live_gs = AList.find (op =) (gs ~~ liveness) true; - val live = length live_gs; - - val maps0 = map map_of_bnf fp_bnfs; - - 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 live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs; - val abs_inverses = map (#abs_inverse o #absT_info) fp_sugars; - val rec_defs = map #co_rec_def fp_sugars; - - val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0; - - val num_rec_args = length rec_arg_Ts; - val h_Ts = map B_ify rec_arg_Ts; - val h_names = variant_names num_rec_args "h"; - 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; - - val rec_o_map_lhss = map2 (curry HOLogic.mk_comp) hrecs gmaps; - - val ABgs = ABs ~~ gs; + 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 @ Cs)) 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_prop) (size_o_maps :: size_o_mapss') + #> pair (Term.list_comb (size_const, args)) + end + | _ => pair (mk_abs_zero_nat T)) + else + pair (mk_abs_zero_nat T); - fun mk_rec_arg_arg (x as Free (_, T)) = - let val U = B_ify T in - if T = U then x else build_map lthy2 [] (the o AList.lookup (op =) ABgs) (T, U) $ x - end; - - 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 = variant_names m "x"; - 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; + fun mk_size_of_arg t = + mk_size_of_typ (fastype_of t) #>> (fn s => substCnatT (betapply (s, t))); - val rec_o_map_goals = - map2 (fold_rev (fold_rev Logic.all) [gs, hs] o 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_sorry lthy2 [] [] goal (fn {context = ctxt, ...} => - mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s 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 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 (fold_rev (fold_rev Logic.all) [fsB, gs] o - 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; - - (* The "size o map" theorem generation will fail if 'nested_size_maps' is incomplete, - which occurs when there is recursion through non-datatypes. In this case, we simply - avoid generating the theorem. The resulting characteristic lemmas are then expressed - in terms of "map", which is not the end of the world. *) - val size_o_map_thmss = - map3 (fn goal => fn size_def => the_list o try (fn rec_o_map => - Goal.prove (*no sorry*) lthy2 [] [] 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 + 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 = variant_names m "x"; + 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 - (map single rec_o_map_thms, size_o_map_thmss) + (fold_rev Term.lambda (map substCnatT xs) sum, size_o_maps') end; - val massage_multi_notes = - maps (fn (thmN, thmss, attrs) => - map2 (fn T_name => fn thms => - ((Binding.qualify true (Long_Name.base_name T_name) (Binding.name thmN), attrs), - [(thms, [])])) - T_names thmss) - #> filter_out (null o fst o hd o snd); + fun mk_size_rhs recx size_o_maps = + fold_map mk_size_arg rec_arg_Ts size_o_maps + |>> (fn args => fold_rev Term.lambda fs (Term.list_comb (substCnatT recx, args))); + + val maybe_conceal_def_binding = Thm.def_binding + #> Config.get lthy0 bnf_note_all = false ? Binding.conceal; + + val (size_rhss, nested_size_o_maps) = fold_map mk_size_rhs recs []; + val size_Ts = map fastype_of size_rhss; + + val ((raw_size_consts, raw_size_defs), (lthy1', lthy1)) = lthy0 + |> apfst split_list o fold_map2 (fn b => fn rhs => + Local_Theory.define ((b, NoSyn), ((maybe_conceal_def_binding b, []), rhs)) + #>> apsnd snd) + size_bs size_rhss + ||> `Local_Theory.restore; + + val phi = Proof_Context.export_morphism lthy1 lthy1'; + + val size_defs = map (Morphism.thm phi) raw_size_defs; + + val size_consts0 = map (Morphism.term phi) raw_size_consts; + val size_consts = map2 retype_const_or_free size_Ts size_consts0; + val size_constsB = map (Term.map_types B_ify) size_consts; + + val zeros = map mk_abs_zero_nat As; + + 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 (maybe_conceal_def_binding o Binding.suffix_name "_overloaded") size_bs; + + 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; + + val (overloaded_size_defs, lthy2) = lthy1 + |> Local_Theory.background_theory_result + (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 notes = - [(rec_o_mapN, rec_o_map_thmss, []), - (sizeN, size_thmss, code_nitpicksimp_simp_attrs), - (size_o_mapN, size_o_map_thmss, [])] - |> massage_multi_notes; + 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 all_overloaded_size_defs = overloaded_size_defs @ + (Spec_Rules.retrieve lthy0 @{const size ('a)} + |> map_filter (try (fn (Spec_Rules.Equational, (_, [thm])) => thm))); + + val nested_size_maps = map (pointfill lthy2) nested_size_o_maps @ nested_size_o_maps; + val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ fp_nesting_bnfs @ live_nesting_bnfs) + |> distinct Thm.eq_thm_prop; + + fun derive_size_simp size_def' simp0 = + (trans OF [size_def', simp0]) + |> Simplifier.asm_full_simplify (ss_only (@{thms inj_on_convol_ident id_def o_def + snd_conv} @ all_inj_maps @ nested_size_maps) lthy2) + |> fold_thms lthy2 size_defs_unused_0; + + fun derive_overloaded_size_simp overloaded_size_def' simp0 = + (trans OF [overloaded_size_def', simp0]) + |> unfold_thms lthy2 @{thms add_0_left add_0_right} + |> fold_thms lthy2 all_overloaded_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; + val size_thmss = map2 append size_simpss overloaded_size_simpss; + + val ABs = As ~~ Bs; + val g_names = variant_names num_As "g"; + val gs = map2 (curry Free) g_names (map (op -->) ABs); + + val liveness = map (op <>) ABs; + val live_gs = AList.find (op =) (gs ~~ liveness) true; + val live = length live_gs; + + val maps0 = map map_of_bnf fp_bnfs; + + 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 live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs; + val abs_inverses = map (#abs_inverse o #absT_info) fp_sugars; + val rec_defs = map #co_rec_def fp_sugars; + + val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0; - val (noted, lthy3) = - lthy2 - |> Spec_Rules.add Spec_Rules.Equational (size_consts, size_simps) - |> Local_Theory.notes notes; + val num_rec_args = length rec_arg_Ts; + val h_Ts = map B_ify rec_arg_Ts; + val h_names = variant_names num_rec_args "h"; + 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; + + 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 lthy2 [] (the o AList.lookup (op =) ABgs) (T, U) $ x + end; + + 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 = variant_names m "x"; + 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 rec_o_map_goals = + map2 (fold_rev (fold_rev Logic.all) [gs, hs] o 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_sorry lthy2 [] [] goal (fn {context = ctxt, ...} => + mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s 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 phi0 = substitute_noted_thm noted; - in - lthy3 - |> Local_Theory.declaration {syntax = false, pervasive = true} - (fn phi => Data.map (fold2 (fn T_name => fn Const (size_name, _) => - Symtab.update (T_name, (size_name, - pairself (map (Morphism.thm (phi0 $> phi))) (size_simps, flat size_o_map_thmss)))) - T_names size_consts)) - end; + 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 (fold_rev (fold_rev Logic.all) [fsB, gs] o + 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; + + (* The "size o map" theorem generation will fail if "nested_size_maps" is incomplete, + which occurs when there is recursion through non-datatypes. In this case, we simply + avoid generating the theorem. The resulting characteristic lemmas are then expressed + in terms of "map", which is not the end of the world. *) + val size_o_map_thmss = + map3 (fn goal => fn size_def => the_list o try (fn rec_o_map => + Goal.prove (*no sorry*) lthy2 [] [] 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 + (map single rec_o_map_thms, size_o_map_thmss) + end; + + val massage_multi_notes = + maps (fn (thmN, thmss, attrs) => + map2 (fn T_name => fn thms => + ((Binding.qualify true (Long_Name.base_name T_name) (Binding.name thmN), attrs), + [(thms, [])])) + T_names thmss) + #> filter_out (null o fst o hd o snd); + + val notes = + [(rec_o_mapN, rec_o_map_thmss, []), + (sizeN, size_thmss, code_nitpicksimp_simp_attrs), + (size_o_mapN, size_o_map_thmss, [])] + |> massage_multi_notes; + + val (noted, lthy3) = + lthy2 + |> Spec_Rules.add Spec_Rules.Equational (size_consts, size_simps) + |> Local_Theory.notes notes; + + val phi0 = substitute_noted_thm noted; + in + lthy3 + |> Local_Theory.declaration {syntax = false, pervasive = true} + (fn phi => Data.map (fold2 (fn T_name => fn Const (size_name, _) => + Symtab.update (T_name, (size_name, + pairself (map (Morphism.thm (phi0 $> phi))) (size_simps, flat size_o_map_thmss)))) + T_names size_consts)) + end + | generate_datatype_size _ lthy = lthy; + +val _ = Theory.setup (fp_sugar_interpretation (map_local_theory o generate_datatype_size) + generate_datatype_size); end; diff -r 695ba3101b37 -r 2de7b0313de3 src/HOL/Tools/BNF/bnf_util.ML --- a/src/HOL/Tools/BNF/bnf_util.ML Thu Sep 04 09:02:36 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_util.ML Thu Sep 04 09:02:43 2014 +0200 @@ -149,6 +149,7 @@ val parse_type_args_named_constrained: (binding option * (string * string option)) list parser val parse_map_rel_bindings: (binding * binding) parser + val map_local_theory: (local_theory -> local_theory) -> theory -> theory val typedef: binding * (string * sort) list * mixfix -> term -> (binding * binding) option -> tactic -> local_theory -> (string * Typedef.info) * local_theory end; @@ -314,6 +315,7 @@ >> (fn ps => fold extract_map_rel ps no_map_rel) || Scan.succeed no_map_rel; +fun map_local_theory f = Named_Target.theory_init #> f #> Local_Theory.exit_global; (*TODO: is this really different from Typedef.add_typedef_global?*) fun typedef (b, Ts, mx) set opt_morphs tac lthy = diff -r 695ba3101b37 -r 2de7b0313de3 src/HOL/Tools/Function/old_size.ML --- a/src/HOL/Tools/Function/old_size.ML Thu Sep 04 09:02:36 2014 +0200 +++ b/src/HOL/Tools/Function/old_size.ML Thu Sep 04 09:02:43 2014 +0200 @@ -4,12 +4,7 @@ Size functions for old-style datatypes. *) -signature OLD_SIZE = -sig - val setup: theory -> theory -end; - -structure Old_Size: OLD_SIZE = +structure Old_Size: sig end = struct fun plus (t1, t2) = Const (@{const_name Groups.plus}, @@ -30,7 +25,7 @@ | SOME t => t); fun is_poly thy (Old_Datatype_Aux.DtType (name, dts)) = - is_some (BNF_LFP_Size.lookup_size_global thy name) andalso exists (is_poly thy) dts + is_some (BNF_LFP_Size.size_of_global thy name) andalso exists (is_poly thy) dts | is_poly _ _ = true; fun constrs_of thy name = @@ -68,8 +63,8 @@ val param_size = AList.lookup op = param_size_fs; val extra_rewrites = descr |> map (#1 o snd) |> distinct op = |> - map_filter (Option.map (fst o snd) o BNF_LFP_Size.lookup_size_global thy) |> flat; - val extra_size = Option.map fst o BNF_LFP_Size.lookup_size_global thy; + map_filter (Option.map (fst o snd) o BNF_LFP_Size.size_of_global thy) |> flat; + val extra_size = Option.map fst o BNF_LFP_Size.size_of_global thy; val (((size_names, size_fns), def_names), def_names') = recTs1 |> map (fn T as Type (s, _) => @@ -228,6 +223,6 @@ |> Sign.restore_naming thy end; -val setup = Old_Datatype_Data.interpretation add_size_thms; +val _ = Context.>> (Context.map_theory (Old_Datatype_Data.interpretation add_size_thms)); end; diff -r 695ba3101b37 -r 2de7b0313de3 src/HOL/Tools/Lifting/lifting_bnf.ML --- a/src/HOL/Tools/Lifting/lifting_bnf.ML Thu Sep 04 09:02:36 2014 +0200 +++ b/src/HOL/Tools/Lifting/lifting_bnf.ML Thu Sep 04 09:02:43 2014 +0200 @@ -115,8 +115,8 @@ snd (Local_Theory.notes notes lthy) end -val _ = Context.>> (Context.map_theory (bnf_interpretation +val _ = Theory.setup (bnf_interpretation (bnf_only_type_ctr (map_local_theory o lifting_bnf_interpretation)) - (bnf_only_type_ctr lifting_bnf_interpretation))) + (bnf_only_type_ctr lifting_bnf_interpretation)) end diff -r 695ba3101b37 -r 2de7b0313de3 src/HOL/Tools/Transfer/transfer_bnf.ML --- a/src/HOL/Tools/Transfer/transfer_bnf.ML Thu Sep 04 09:02:36 2014 +0200 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Thu Sep 04 09:02:43 2014 +0200 @@ -290,9 +290,9 @@ snd (Local_Theory.notes (constr_notes @ relator_eq_notes @ pred_notes) lthy) end -val _ = Context.>> (Context.map_theory (bnf_interpretation +val _ = Theory.setup (bnf_interpretation (bnf_only_type_ctr (map_local_theory o transfer_bnf_interpretation)) - (bnf_only_type_ctr (transfer_bnf_interpretation)))) + (bnf_only_type_ctr (transfer_bnf_interpretation))) (* simplification rules for the predicator *) @@ -361,8 +361,8 @@ snd (Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) lthy) end -val _ = Context.>> (Context.map_theory (fp_sugar_interpretation +val _ = Theory.setup (fp_sugar_interpretation (fp_sugar_only_type_ctr (map_local_theory o fold transfer_fp_sugar_interpretation)) - (fp_sugar_only_type_ctr (fold transfer_fp_sugar_interpretation)))) + (fp_sugar_only_type_ctr (fold transfer_fp_sugar_interpretation))) end