# HG changeset patch # User blanchet # Date 1398241407 -7200 # Node ID fc105315822af0fca3290a53401c981792d6774b # Parent 1f9ab71d43a5b467ff6b1e4b0249cbf646e9e597 localize new size function generation code diff -r 1f9ab71d43a5 -r fc105315822a src/HOL/BNF_FP_Base.thy --- 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 @@ -184,7 +184,6 @@ lemma prod_inj_map: "inj f \ inj g \ 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" @@ -211,9 +210,9 @@ by (rule ext) auto setup {* -BNF_LFP_Size.register_size @{type_name sum} @{const_name sum_size} @{thms sum.size} +BNF_LFP_Size.register_size_global @{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} +#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name prod_size} @{thms prod.size} @{thms prod_size_o_map} *} diff -r 1f9ab71d43a5 -r fc105315822a src/HOL/BNF_LFP.thy --- 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 @@ -194,6 +194,4 @@ hide_fact (open) id_transfer -datatype_new 'a x = X 'a - end diff -r 1f9ab71d43a5 -r fc105315822a src/HOL/Library/FSet.thy --- a/src/HOL/Library/FSet.thy Wed Apr 23 10:23:27 2014 +0200 +++ b/src/HOL/Library/FSet.thy Wed Apr 23 10:23:27 2014 +0200 @@ -1005,7 +1005,7 @@ by (auto simp: Abs_fset_inverse setsum_reindex_cong[OF subset_inj_on[OF _ top_greatest]]) setup {* -BNF_LFP_Size.register_size @{type_name fset} @{const_name size_fset} +BNF_LFP_Size.register_size_global @{type_name fset} @{const_name size_fset} @{thms size_fset_simps size_fset_overloaded_simps} @{thms fset_size_o_map} *} diff -r 1f9ab71d43a5 -r fc105315822a src/HOL/Tools/BNF/bnf_def.ML --- a/src/HOL/Tools/BNF/bnf_def.ML Wed Apr 23 10:23:27 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_def.ML Wed Apr 23 10:23:27 2014 +0200 @@ -941,8 +941,8 @@ ||>> mk_Frees "R" transfer_domRTs ||>> mk_Frees "S" transfer_ranRTs; - val fs_copy = map2 (retype_free o fastype_of) fs gs; - val x_copy = retype_free CA' y; + val fs_copy = map2 (retype_const_or_free o fastype_of) fs gs; + val x_copy = retype_const_or_free CA' y; val rel = mk_bnf_rel pred2RTs CA' CB'; val relAsAs = mk_bnf_rel self_pred2RTs CA' CA'; diff -r 1f9ab71d43a5 -r fc105315822a src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- 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 @@ -122,12 +122,13 @@ val eq: T * T -> bool = op = o pairself (map #T); ); +(* FIXME naming *) fun with_repaired_path f (fp_sugars as ({T = Type (s, _), ...} : fp_sugar) :: _) thy = thy - |> Sign.root_path (* FIXME *) - |> Sign.add_path (Long_Name.qualifier s) + (*|> Sign.root_path*) + (*|> Sign.add_path (Long_Name.qualifier s)*) |> f fp_sugars - |> Sign.restore_naming thy; + (*|> Sign.restore_naming thy*); val fp_sugar_interpretation = FP_Sugar_Interpretation.interpretation o with_repaired_path; @@ -136,7 +137,7 @@ 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) + #> fp = Least_FP ? 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 diff -r 1f9ab71d43a5 -r fc105315822a src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Wed Apr 23 10:23:27 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML Wed Apr 23 10:23:27 2014 +0200 @@ -29,7 +29,7 @@ val exists_strict_subtype_in: typ list -> typ -> bool val tvar_subst: theory -> typ list -> typ list -> ((string * int) * typ) list - val retype_free: typ -> term -> term + val retype_const_or_free: typ -> term -> term val drop_all: term -> term val permute_args: int -> term -> term @@ -82,8 +82,9 @@ fun tvar_subst thy Ts Us = Vartab.fold (cons o apsnd snd) (fold (Sign.typ_match thy) (Ts ~~ Us) Vartab.empty) []; -fun retype_free T (Free (s, _)) = Free (s, T) - | retype_free _ t = raise TERM ("retype_free", [t]); +fun retype_const_or_free T (Const (s, _)) = Const (s, T) + | retype_const_or_free T (Free (s, _)) = Free (s, T) + | retype_const_or_free _ t = raise TERM ("retype_const_or_free", [t]); fun drop_all t = subst_bounds (strip_qnt_vars @{const_name Pure.all} t |> map Free |> rev, diff -r 1f9ab71d43a5 -r fc105315822a src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Wed Apr 23 10:23:27 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Wed Apr 23 10:23:27 2014 +0200 @@ -906,9 +906,9 @@ ||>> mk_Frees "f" fTs ||>> mk_Frees "s" rec_sTs; - val Izs = map2 retype_free Ts zs; - val phis = map2 retype_free (map mk_pred1T Ts) init_phis; - val phi2s = map2 retype_free (map2 mk_pred2T Ts Ts') init_phis; + val Izs = map2 retype_const_or_free Ts zs; + val phis = map2 retype_const_or_free (map mk_pred1T Ts) init_phis; + val phi2s = map2 retype_const_or_free (map2 mk_pred2T Ts Ts') init_phis; fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_"); val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind; diff -r 1f9ab71d43a5 -r fc105315822a src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Wed Apr 23 10:23:27 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Wed Apr 23 10:23:27 2014 +0200 @@ -333,10 +333,11 @@ nth_map arg_idx (K (nth ctr_args ctr_arg_idx))) no_calls' |> fold (fn (ctr_arg_idx, (arg_idx, T)) => fn xs => - nth_map arg_idx (K (ensure_unique xs (retype_free T (nth ctr_args ctr_arg_idx)))) xs) + nth_map arg_idx (K (ensure_unique xs + (retype_const_or_free T (nth ctr_args ctr_arg_idx)))) xs) mutual_calls' |> fold (fn (ctr_arg_idx, (arg_idx, T)) => - nth_map arg_idx (K (retype_free T (nth ctr_args ctr_arg_idx)))) + nth_map arg_idx (K (retype_const_or_free T (nth ctr_args ctr_arg_idx)))) nested_calls'; val fun_name_ctr_pos_list = diff -r 1f9ab71d43a5 -r fc105315822a src/HOL/Tools/BNF/bnf_lfp_size.ML --- 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 @@ -7,9 +7,11 @@ signature BNF_LFP_SIZE = 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 + 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 end; structure BNF_LFP_Size : BNF_LFP_SIZE = @@ -26,7 +28,11 @@ val sizeN = "size" val size_o_mapN = "size_o_map" -structure Data = Theory_Data +val nitpicksimp_attrs = @{attributes [nitpick_simp]}; +val simp_attrs = @{attributes [simp]}; +val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: nitpicksimp_attrs @ simp_attrs; + +structure Data = Generic_Data ( type T = (string * (thm list * thm list)) Symtab.table; val empty = Symtab.empty; @@ -35,9 +41,13 @@ ); fun register_size T_name size_name size_simps size_o_maps = - Data.map (Symtab.update (T_name, (size_name, (size_simps, size_o_maps)))); + Context.proof_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_o_maps))))); -val lookup_size = Symtab.lookup o Data.get; +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 zero_nat = @{const zero_class.zero (nat)}; @@ -54,16 +64,16 @@ 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_map_sum case_prod_map_prod BNF_Comp.id_bnf_comp_def}; + @{thms o_def id_def 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 - 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)); + HEADGOAL (rtac (ctor_rec_o_map RS trans)) THEN + PRIMITIVE (Conv.fconv_rule Thm.eta_long_conversion) THEN + HEADGOAL (asm_simp_tac (ss_only (pre_map_defs @ distinct Thm.eq_thm_prop abs_inverses @ + rec_o_map_simp_thms) ctxt)); -val size_o_map_simp_thms = - @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]}; +val size_o_map_simp_thms = @{thms 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 @@ -71,270 +81,273 @@ 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 = 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 - val data = Data.get thy; +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, ...}, nested_bnfs, + 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 Ts = map #T fp_sugars - val T_names = map (fst o dest_Type) Ts; - val nn = length Ts; + 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; + + val size_bs = map (Binding.name o prefix size_N o Long_Name.base_name) T_names; + + fun is_pair_C @{type_name prod} [_, T'] = member (op =) Cs T' + | is_pair_C _ _ = false; - val B_ify = Term.typ_subst_atomic (As ~~ Bs); + 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 as _ :: _)) => + 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 + | _ => pair (mk_abs_zero_nat T)) + else + pair (mk_abs_zero_nat T); - 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_of_arg t = + mk_size_of_typ (fastype_of t) #>> (fn s => substCnatT (betapply (s, t))); + + 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; + + 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; + + 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 f_Ts = map mk_to_natT As; - val f_TsB = map mk_to_natT Bs; - val num_As = length As; + 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 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 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 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 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 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 as _ :: _)) => - 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 - | _ => pair (mk_abs_zero_nat T)) - else - pair (mk_abs_zero_nat T); + 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 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 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 @ nested_bnfs @ nesting_bnfs); + + 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) lthy2) + |> fold_thms lthy2 size_defs_unused_0; + fun derive_overloaded_size_simp size_def' simp0 = + (trans OF [size_def', simp0]) + |> unfold_thms lthy2 @{thms add_0_left add_0_right} + |> fold_thms lthy2 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 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; - fun mk_size_of_arg t = - mk_size_of_typ (fastype_of t) #>> (fn s => substCnatT (betapply (s, t))); + 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; - 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]); + 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 lthy2 [] [] 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 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; + val size_o_map_thms = + map3 (fn goal => fn size_def => fn rec_o_map => + Goal.prove 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 - (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') + pairself (map single) (rec_o_map_thms, size_o_map_thms) end; - fun mk_def_binding f = - Binding.conceal o Binding.name o Thm.def_name o f o Long_Name.base_name; - - 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; - - 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 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; - - 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, 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 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 @ nesting_bnfs); - - 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 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 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 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; - - (* This disables much of the functionality of the size extension within a locale. It is not - clear how to make the code below work with locales, given that interpretations are based on - theories. *) - val has_hyps = not (null (Thm.hyps_of (hd (hd rec_thmss)))); - - val (rec_o_map_thmss, size_o_map_thmss) = - if has_hyps orelse 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 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 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 = 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; - - 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; - - 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 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 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_map4 (fn T_name => fn size_simps => fn rec_o_map_thms => fn size_o_map_thms => - if has_hyps then - pair [] - else - 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_lfp_size _ thy = thy; + 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; + in + lthy2 + |> Local_Theory.notes notes |> snd + |> Spec_Rules.add Spec_Rules.Equational (size_consts, size_simps) + |> 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 phi)) (size_simps, flat size_o_map_thmss)))) + T_names size_consts)) + end; end; diff -r 1f9ab71d43a5 -r fc105315822a src/HOL/Tools/Function/size.ML --- a/src/HOL/Tools/Function/size.ML Wed Apr 23 10:23:27 2014 +0200 +++ b/src/HOL/Tools/Function/size.ML Wed Apr 23 10:23:27 2014 +0200 @@ -30,7 +30,7 @@ | SOME t => t); fun is_poly thy (Datatype_Aux.DtType (name, dts)) = - is_some (BNF_LFP_Size.lookup_size thy name) andalso exists (is_poly thy) dts + is_some (BNF_LFP_Size.lookup_size_global thy name) andalso exists (is_poly thy) dts | is_poly _ _ = true; fun constrs_of thy name = @@ -68,8 +68,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 thy) |> flat; - val extra_size = Option.map fst o BNF_LFP_Size.lookup_size thy; + 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; val (((size_names, size_fns), def_names), def_names') = recTs1 |> map (fn T as Type (s, _) => @@ -207,7 +207,7 @@ in fold2 (fn new_type_name => fn size_name => - BNF_LFP_Size.register_size new_type_name size_name size_thms []) + BNF_LFP_Size.register_size_global new_type_name size_name size_thms []) new_type_names size_names thy'' end end; diff -r 1f9ab71d43a5 -r fc105315822a src/HOL/Tools/Transfer/transfer_bnf.ML --- a/src/HOL/Tools/Transfer/transfer_bnf.ML Wed Apr 23 10:23:27 2014 +0200 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Wed Apr 23 10:23:27 2014 +0200 @@ -18,6 +18,7 @@ open BNF_Util open BNF_Def +open BNF_FP_Util open BNF_FP_Def_Sugar (* util functions *)