# HG changeset patch # User desharna # Date 1413904991 -7200 # Node ID 854eed6e5aed503f88d7c8804ec15d7c4e2bedfa # Parent 43a3ef574065f5d7dccb9d76bc335dde46a4fa21 move theorem 'rec_o_map' * * * move documentation of 'rec_o_map' diff -r 43a3ef574065 -r 854eed6e5aed src/HOL/BNF_Fixpoint_Base.thy --- a/src/HOL/BNF_Fixpoint_Base.thy Tue Oct 21 17:23:10 2014 +0200 +++ b/src/HOL/BNF_Fixpoint_Base.thy Tue Oct 21 17:23:11 2014 +0200 @@ -199,6 +199,9 @@ lemma case_prod_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 case_prod_o_map_prod: "case_prod f \ map_prod g1 g2 = case_prod (\l r. f (g1 l) (g2 r))" + unfolding comp_def by auto + lemma case_prod_transfer: "(rel_fun (rel_fun A (rel_fun B C)) (rel_fun (rel_prod A B) C)) case_prod case_prod" unfolding rel_fun_def rel_prod_def by simp diff -r 43a3ef574065 -r 854eed6e5aed src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Oct 21 17:23:10 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Oct 21 17:23:11 2014 +0200 @@ -42,6 +42,7 @@ co_rec_selss: thm list list, co_rec_codes: thm list, co_rec_transfers: thm list, + rec_o_maps: thm list, common_rel_co_inducts: thm list, rel_co_inducts: thm list, common_set_inducts: thm list, @@ -176,6 +177,7 @@ val corec_transferN = "corec_transfer"; val map_disc_iffN = "map_disc_iff"; val map_selN = "map_sel"; +val rec_o_mapN = "rec_o_map"; val rec_transferN = "rec_transfer"; val set_casesN = "set_cases"; val set_introsN = "set_intros"; @@ -216,6 +218,7 @@ co_rec_selss: thm list list, co_rec_codes: thm list, co_rec_transfers: thm list, + rec_o_maps: thm list, common_rel_co_inducts: thm list, rel_co_inducts: thm list, common_set_inducts: thm list, @@ -254,7 +257,7 @@ set_cases = map (Morphism.thm phi) set_cases}; fun morph_fp_co_induct_sugar phi ({co_rec, common_co_inducts, co_inducts, co_rec_def, co_rec_thms, - co_rec_discs, co_rec_disc_iffs, co_rec_selss, co_rec_codes, co_rec_transfers, + co_rec_discs, co_rec_disc_iffs, co_rec_selss, co_rec_codes, co_rec_transfers, rec_o_maps, common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts} : fp_co_induct_sugar) = {co_rec = Morphism.term phi co_rec, common_co_inducts = map (Morphism.thm phi) common_co_inducts, @@ -266,6 +269,7 @@ co_rec_selss = map (map (Morphism.thm phi)) co_rec_selss, co_rec_codes = map (Morphism.thm phi) co_rec_codes, co_rec_transfers = map (Morphism.thm phi) co_rec_transfers, + rec_o_maps = map (Morphism.thm phi) rec_o_maps, common_rel_co_inducts = map (Morphism.thm phi) common_rel_co_inducts, rel_co_inducts = map (Morphism.thm phi) rel_co_inducts, common_set_inducts = map (Morphism.thm phi) common_set_inducts, @@ -348,7 +352,7 @@ rel_distinctss map_disc_iffss map_selsss rel_selss rel_intross rel_casess set_thmss set_selsssss set_introsssss set_casess ctr_transferss case_transferss disc_transferss co_rec_disc_iffss co_rec_codess co_rec_transferss common_rel_co_inducts rel_co_inductss common_set_inducts - set_inductss sel_transferss noted = + set_inductss sel_transferss rec_o_mapss noted = let val fp_sugars = map_index (fn (kk, T) => @@ -388,6 +392,7 @@ co_rec_selss = nth co_rec_selsss kk, co_rec_codes = nth co_rec_codess kk, co_rec_transfers = nth co_rec_transferss kk, + rec_o_maps = nth rec_o_mapss kk, common_rel_co_inducts = common_rel_co_inducts, rel_co_inducts = nth rel_co_inductss kk, common_set_inducts = common_set_inducts, @@ -1999,7 +2004,7 @@ dtors = dtors0, xtor_co_recs = xtor_co_recs0, xtor_co_induct, dtor_ctors, ctor_dtors, ctor_injects, dtor_injects, xtor_maps, xtor_setss, xtor_rels, xtor_co_rec_thms, xtor_rel_co_induct, dtor_set_inducts, - xtor_co_rec_transfers, ...}, + xtor_co_rec_transfers, xtor_co_rec_o_maps, ...}, lthy)) = fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) (map dest_TFree killed_As) fp_eqs no_defs_lthy @@ -2048,6 +2053,7 @@ val pre_rel_defs = map rel_def_of_bnf pre_bnfs; val fp_nesting_set_maps = maps set_map_of_bnf fp_nesting_bnfs; val live_nesting_map_id0s = map map_id0_of_bnf live_nesting_bnfs; + val live_nesting_map_ident0s = map map_ident0_of_bnf live_nesting_bnfs; val live_nesting_set_maps = maps set_map_of_bnf live_nesting_bnfs; val live_nesting_rel_eqs = map rel_eq_of_bnf live_nesting_bnfs; @@ -2064,6 +2070,7 @@ (liveness_of_fp_bnf num_As any_fp_bnf) As Bs0; val B_ify_T = Term.typ_subst_atomic (As ~~ Bs); + val live_AsBs = filter (op <>) (As ~~ Bs); val ctors = map (mk_ctor As) ctors0; val dtors = map (mk_dtor As) dtors0; @@ -2208,11 +2215,10 @@ fun mk_co_rec_transfer_goals lthy co_recs = let - val liveAsBs = filter (op <>) (As ~~ Bs); - val B_ify = Term.subst_atomic_types (liveAsBs @ (Cs ~~ Es)); + val B_ify = Term.subst_atomic_types (live_AsBs @ (Cs ~~ Es)); val ((Rs, Ss), names_lthy) = lthy - |> mk_Frees "R" (map (uncurry mk_pred2T) liveAsBs) + |> mk_Frees "R" (map (uncurry mk_pred2T) live_AsBs) ||>> mk_Frees "S" (map2 mk_pred2T Cs Es); val co_recBs = map B_ify co_recs; @@ -2231,6 +2237,73 @@ |> map Thm.close_derivation end; + fun derive_rec_o_map_thmss lthy recs rec_defs = + if live = 0 then replicate nn [] + else + let + fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy); + + val maps0 = map map_of_bnf fp_bnfs; + val ABs = As ~~ Bs + val liveness = map (op <>) ABs; + val f_names = variant_names num_As "f"; + val fs = map2 (curry Free) f_names (map (op -->) ABs); + val live_gs = AList.find (op =) (fs ~~ liveness) true; + + val gmaps = map (fn map0 => Term.list_comb (mk_map live As Bs map0, live_gs)) maps0; + + val rec_Ts as rec_T1 :: _ = map fastype_of recs; + val rec_arg_Ts = binder_fun_types rec_T1; + + val B_ify_T = Term.typ_subst_atomic (As ~~ Bs); + + val num_rec_args = length rec_arg_Ts; + val g_Ts = map B_ify_T rec_arg_Ts; + val g_names = variant_names num_rec_args "g"; + val gs = map2 (curry Free) g_names g_Ts; + val grecs = map (fn recx => Term.list_comb (Term.map_types B_ify_T recx, gs)) recs; + + val rec_o_map_lhss = map2 (curry HOLogic.mk_comp) grecs gmaps; + + val ABfs = ABs ~~ fs; + + fun mk_rec_arg_arg (x as Free (_, T)) = + let val U = B_ify_T T in + if T = U then x else build_map lthy [] (the o AList.lookup (op =) ABfs) (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 gs 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) [fs, gs] o HOLogic.mk_Trueprop oo + curry HOLogic.mk_eq) rec_o_map_lhss rec_o_map_rhss; + val rec_o_map_thms = + @{map 3} (fn goal => fn rec_def => fn ctor_rec_o_map => + Goal.prove_sorry lthy [] [] 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 xtor_co_rec_o_maps; + in + map single rec_o_map_thms + end; + fun derive_note_induct_recs_thms_for_types ((((map_thmss, map_disc_iffss, map_selsss, rel_injectss, rel_distinctss, rel_selss, rel_intross, rel_casess, set_thmss, set_selsssss, set_introsssss, @@ -2265,6 +2338,8 @@ (rel_induct_attrs, rel_induct_attrs)) end; + val rec_o_map_thmss = derive_rec_o_map_thmss lthy recs rec_defs; + val simp_thmss = @{map 6} mk_simp_thms ctr_sugars rec_thmss map_thmss rel_injectss rel_distinctss set_thmss; @@ -2279,6 +2354,7 @@ val notes = [(inductN, map single induct_thms, fn T_name => induct_attrs @ [induct_type_attr T_name]), (recN, rec_thmss, K rec_attrs), + (rec_o_mapN, rec_o_map_thmss, K []), (rec_transferN, rec_transfer_thmss, K []), (rel_inductN, rel_induct_thmss, K (rel_induct_attrs @ [induct_pred_attr ""])), (simpsN, simp_thmss, K [])] @@ -2297,6 +2373,7 @@ rel_intross rel_casess set_thmss set_selsssss set_introsssss set_casess ctr_transferss case_transferss disc_transferss (replicate nn []) (replicate nn []) rec_transfer_thmss common_rel_induct_thms rel_induct_thmss [] (replicate nn []) sel_transferss + rec_o_map_thmss end; fun derive_corec_transfer_thms lthy corecs corec_defs = @@ -2416,7 +2493,7 @@ rel_intross rel_casess set_thmss set_selsssss set_introsssss set_casess ctr_transferss case_transferss disc_transferss corec_disc_iff_thmss (map single corec_code_thms) corec_transfer_thmss common_rel_coinduct_thms rel_coinduct_thmss set_induct_thms - (replicate nn (if nn = 1 then set_induct_thms else [])) sel_transferss + (replicate nn (if nn = 1 then set_induct_thms else [])) sel_transferss (replicate nn []) end; val lthy'' = lthy' diff -r 43a3ef574065 -r 854eed6e5aed src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Oct 21 17:23:10 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Oct 21 17:23:11 2014 +0200 @@ -34,6 +34,8 @@ val mk_map_disc_iff_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> tactic val mk_map_sel_tac: Proof.context -> cterm -> thm -> thm list -> thm list -> thm list -> thm list -> tactic + val mk_rec_o_map_tac: Proof.context -> thm -> thm list -> thm list -> thm list -> thm -> thm -> + thm Seq.seq val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list -> @@ -161,6 +163,18 @@ @{thms comp_def convol_def fst_conv id_def case_prod_Pair_iden snd_conv split_conv case_unit_Unity} @ sumprod_thms_map; +fun mk_rec_o_map_tac ctxt rec_def pre_map_defs map_ident0s abs_inverses ctor_rec_o_map = + let + 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}; + in + HEADGOAL (subst_tac @{context} (SOME [1, 2]) [rec_def] THEN' + rtac (ctor_rec_o_map RS trans) THEN' + CONVERSION Thm.eta_long_conversion THEN' + asm_simp_tac (ss_only (pre_map_defs @ distinct Thm.eq_thm_prop (map_ident0s @ abs_inverses) @ + rec_o_map_simps) ctxt)) + end; + fun mk_rec_tac pre_map_defs map_ident0s rec_defs ctor_rec fp_abs_inverse abs_inverse ctr_def ctxt = HEADGOAL ((if is_def_looping ctr_def then subst_tac ctxt NONE else SELECT_GOAL o unfold_thms_tac ctxt) [ctr_def]) THEN diff -r 43a3ef574065 -r 854eed6e5aed src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Oct 21 17:23:10 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Oct 21 17:23:11 2014 +0200 @@ -297,7 +297,8 @@ fp_bnf_sugar = {map_disc_iffs, map_selss, rel_injects, rel_distincts, rel_sels, rel_intros, rel_cases, set_thms, set_selssss, set_introssss, set_cases, ...}, fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers, - common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts, ...}, + rec_o_maps, common_rel_co_inducts, rel_co_inducts, common_set_inducts, + set_inducts, ...}, ...} : fp_sugar) = {T = T, BT = T (*wrong but harmless*), X = X, fp = fp, fp_res = fp_res, fp_res_index = kk, pre_bnf = pre_bnf, fp_bnf = nth (#bnfs fp_res) kk, absT_info = absT_info, @@ -334,6 +335,7 @@ co_rec_selss = co_rec_sel_thmss, co_rec_codes = co_rec_codes, co_rec_transfers = co_rec_transfers, + rec_o_maps = rec_o_maps, common_rel_co_inducts = common_rel_co_inducts, rel_co_inducts = rel_co_inducts, common_set_inducts = common_set_inducts, diff -r 43a3ef574065 -r 854eed6e5aed src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Oct 21 17:23:10 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Oct 21 17:23:11 2014 +0200 @@ -109,6 +109,7 @@ co_rec_selss = [], co_rec_codes = [], co_rec_transfers = [], + rec_o_maps = @{thms case_sum_o_map_sum}, common_rel_co_inducts = [], rel_co_inducts = [], common_set_inducts = [], @@ -174,6 +175,7 @@ co_rec_selss = [], co_rec_codes = [], co_rec_transfers = [], + rec_o_maps = @{thms case_prod_o_map_prod}, common_rel_co_inducts = [], rel_co_inducts = [], common_set_inducts = [], diff -r 43a3ef574065 -r 854eed6e5aed src/HOL/Tools/BNF/bnf_lfp_size.ML --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Oct 21 17:23:10 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Tue Oct 21 17:23:11 2014 +0200 @@ -22,8 +22,6 @@ open BNF_FP_Def_Sugar val size_N = "size_"; - -val rec_o_mapN = "rec_o_map"; val sizeN = "size"; val size_o_mapN = "size_o_map"; @@ -62,14 +60,6 @@ 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}; -fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses - ctor_rec_o_map = - HEADGOAL (subst_tac @{context} (SOME [1, 2]) [rec_def] THEN' rtac (ctor_rec_o_map RS trans) THEN' - CONVERSION Thm.eta_long_conversion THEN' - asm_simp_tac (ss_only (pre_map_defs @ - distinct Thm.eq_thm_prop (live_nesting_map_ident0s @ abs_inverses) @ rec_o_map_simps) - ctxt)); - val size_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 = @@ -271,63 +261,12 @@ val maps0 = map map_of_bnf fp_bnfs; - val (rec_o_map_thmss, size_o_map_thmss) = - if live = 0 then - `I (replicate nn []) + val size_o_map_thmss = + if live = 0 then 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 o #fp_co_induct_sugar) 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_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 = - @{map 3} (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 @@ -346,6 +285,8 @@ 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 rec_o_maps = fold_rev (curry (op @) o (#rec_o_maps o #fp_co_induct_sugar)) fp_sugars []; + val size_o_map_thmss = if nested_size_o_maps_complete then @{map 3} (fn goal => fn size_def => fn rec_o_map => @@ -353,11 +294,11 @@ mk_size_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_map_thms + size_o_map_goals size_defs rec_o_maps else replicate nn []; in - (map single rec_o_map_thms, size_o_map_thmss) + size_o_map_thmss end; (* Ideally, the "[code]" attribute would be generated only if the "code" plugin is enabled. *) @@ -372,8 +313,7 @@ #> filter_out (null o fst o hd o snd); val notes = - [(rec_o_mapN, rec_o_map_thmss, []), - (sizeN, size_thmss, code_attrs :: nitpicksimp_attrs @ simp_attrs), + [(sizeN, size_thmss, code_attrs :: nitpicksimp_attrs @ simp_attrs), (size_o_mapN, size_o_map_thmss, [])] |> massage_multi_notes;