# HG changeset patch # User desharna # Date 1413904994 -7200 # Node ID 2af42aecc12096708eccae80b2848ca12593a5a3 # Parent b45405874f8fa3b49e423e7087ecca368032a431 rename 'size_o_map' to 'size_gen_o_map' diff -r b45405874f8f -r 2af42aecc120 src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Oct 21 17:23:14 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Oct 21 17:23:14 2014 +0200 @@ -24,7 +24,7 @@ val size_N = "size_"; val sizeN = "size"; val size_genN = "size_gen"; -val size_o_mapN = "size_o_map"; +val size_gen_o_mapN = "size_gen_o_map"; val nitpicksimp_attrs = @{attributes [nitpick_simp]}; val simp_attrs = @{attributes [simp]}; @@ -37,11 +37,11 @@ fun merge data = Symtab.merge (K true) data; ); -fun register_size 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))))); +fun register_size T_name size_name size_simps size_gen_o_maps = + Context.proof_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_gen_o_maps))))); -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))))); +fun register_size_global T_name size_name size_simps size_gen_o_maps = + Context.theory_map (Data.map (Symtab.update (T_name, (size_name, (size_simps, size_gen_o_maps))))); val size_of = Symtab.lookup o Data.get o Context.Proof; val size_of_global = Symtab.lookup o Data.get o Context.Theory; @@ -61,12 +61,12 @@ val rec_o_map_simps = @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum case_prod_map_prod id_bnf_def}; -val size_o_map_simps = @{thms prod_inj_map inj_on_id snd_comp_apfst[unfolded apfst_def]}; +val size_gen_o_map_simps = @{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 = +fun mk_size_gen_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_simps) ctxt)) THEN + asm_simp_tac (ss_only (inj_maps @ size_maps @ size_gen_o_map_simps) ctxt)) THEN IF_UNSOLVED (unfold_thms_tac ctxt @{thms o_def} THEN HEADGOAL (rtac refl)); fun generate_datatype_size (fp_sugars as ({T = Type (_, As), BT = Type (_, Bs), fp = Least_FP, @@ -116,12 +116,12 @@ 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)) => + SOME (size_name, (_, size_gen_o_maps)) => let - val (args, size_o_mapss') = fold_map mk_size_of_typ Ts []; + val (args, size_gen_o_mapss') = fold_map mk_size_of_typ Ts []; val size_const = Const (size_name, map fastype_of args ---> mk_to_natT T); in - append (size_o_maps :: size_o_mapss') + append (size_gen_o_maps :: size_gen_o_mapss') #> pair (Term.list_comb (size_const, args)) end | _ => pair (mk_abs_zero_nat T)) @@ -155,14 +155,14 @@ 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_mapss) = + val (summands, size_gen_o_mapss) = fold_map mk_size_of_arg xs [] |>> remove (op =) HOLogic.zero; val sum = if null summands then base_case else foldl1 mk_plus_nat (summands @ [HOLogic.Suc_zero]); in - append size_o_mapss + append size_gen_o_mapss #> pair (fold_rev Term.lambda (map substCnatT xs) sum) end; @@ -173,11 +173,11 @@ val maybe_conceal_def_binding = Thm.def_binding #> not (Config.get lthy0 bnf_note_all) ? Binding.conceal; - val (size_rhss, nested_size_o_mapss) = fold_map mk_size_rhs recs []; + val (size_rhss, nested_size_gen_o_mapss) = fold_map mk_size_rhs recs []; val size_Ts = map fastype_of size_rhss; - val nested_size_o_maps_complete = forall (not o null) nested_size_o_mapss; - val nested_size_o_maps = fold (union Thm.eq_thm_prop) nested_size_o_mapss []; + val nested_size_gen_o_maps_complete = forall (not o null) nested_size_gen_o_mapss; + val nested_size_gen_o_maps = fold (union Thm.eq_thm_prop) nested_size_gen_o_mapss []; val ((raw_size_consts, raw_size_defs), (lthy1', lthy1)) = lthy0 |> apfst split_list o @{fold_map 2} (fn b => fn rhs => @@ -231,7 +231,7 @@ (Spec_Rules.retrieve lthy0 @{const size ('a)} |> map_filter (try (fn (Spec_Rules.Equational, (_, [thm])) => thm))); - val nested_size_maps = map (mk_pointfull lthy2) nested_size_o_maps @ nested_size_o_maps; + val nested_size_maps = map (mk_pointfull lthy2) nested_size_gen_o_maps @ nested_size_gen_o_maps; val all_inj_maps = map inj_map_of_bnf (fp_bnfs @ fp_nesting_bnfs @ live_nesting_bnfs) |> distinct Thm.eq_thm_prop; @@ -263,45 +263,45 @@ val maps0 = map map_of_bnf fp_bnfs; - val size_o_map_thmss = + val size_gen_o_map_thmss = if live = 0 then replicate nn [] else let val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0; - val size_o_map_conds = - if exists (can Logic.dest_implies o Thm.prop_of) nested_size_o_maps then + val size_gen_o_map_conds = + if exists (can Logic.dest_implies o Thm.prop_of) nested_size_gen_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 size_gen_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_gen_o_map_rhss = map (fn c => Term.list_comb (c, fgs)) size_consts; - val size_o_map_goals = + val size_gen_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; + curry Logic.list_implies size_gen_o_map_conds o HOLogic.mk_Trueprop oo + curry HOLogic.mk_eq) size_gen_o_map_lhss size_gen_o_map_rhss; val rec_o_maps = fold_rev (curry (op @) o (#co_rec_o_maps o #fp_co_induct_sugar)) fp_sugars []; - val size_o_map_thmss = - if nested_size_o_maps_complete then + val size_gen_o_map_thmss = + if nested_size_gen_o_maps_complete then @{map 3} (fn goal => fn size_def => fn rec_o_map => Goal.prove_sorry lthy2 [] [] goal (fn {context = ctxt, ...} => - mk_size_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps) + mk_size_gen_o_map_tac ctxt size_def rec_o_map all_inj_maps nested_size_maps) |> Thm.close_derivation |> single) - size_o_map_goals size_defs rec_o_maps + size_gen_o_map_goals size_defs rec_o_maps else replicate nn []; in - size_o_map_thmss + size_gen_o_map_thmss end; (* Ideally, the "[code]" attribute would be generated only if the "code" plugin is enabled. *) @@ -318,7 +318,7 @@ val notes = [(sizeN, size_thmss, code_attrs :: nitpicksimp_attrs @ simp_attrs), (size_genN, size_gen_thmss, []), - (size_o_mapN, size_o_map_thmss, [])] + (size_gen_o_mapN, size_gen_o_map_thmss, [])] |> massage_multi_notes; val (noted, lthy3) = @@ -332,7 +332,7 @@ |> 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)))) + pairself (map (Morphism.thm (phi0 $> phi))) (size_simps, flat size_gen_o_map_thmss)))) T_names size_consts)) end | generate_datatype_size _ lthy = lthy;