# HG changeset patch # User desharna # Date 1413292295 -7200 # Node ID 4cc24f1e52d5cdbe5805b459905bb91d22c9f880 # Parent 97c6818f46969fbe4f015f96c91ddf7af96ccdf8 preserve the structure of 'set_sel' theorem in ML diff -r 97c6818f4696 -r 4cc24f1e52d5 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Oct 14 13:51:38 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Oct 14 15:11:35 2014 +0200 @@ -26,7 +26,7 @@ rel_intros: thm list, rel_cases: thm list, set_thms: thm list, - set_sels: thm list, + set_selssss: thm list list list list, set_intros: thm list, set_cases: thm list} @@ -197,7 +197,7 @@ rel_intros: thm list, rel_cases: thm list, set_thms: thm list, - set_sels: thm list, + set_selssss: thm list list list list, set_intros: thm list, set_cases: thm list}; @@ -233,7 +233,7 @@ fp_co_induct_sugar: fp_co_induct_sugar}; fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, map_sels, rel_injects, rel_distincts, - rel_sels, rel_intros, rel_cases, set_thms, set_sels, set_intros, set_cases} : fp_bnf_sugar) = + rel_sels, rel_intros, rel_cases, set_thms, set_selssss, set_intros, set_cases} : fp_bnf_sugar) = {map_thms = map (Morphism.thm phi) map_thms, map_disc_iffs = map (Morphism.thm phi) map_disc_iffs, map_sels = map (Morphism.thm phi) map_sels, @@ -243,7 +243,7 @@ rel_intros = map (Morphism.thm phi) rel_intros, rel_cases = map (Morphism.thm phi) rel_cases, set_thms = map (Morphism.thm phi) set_thms, - set_sels = map (Morphism.thm phi) set_sels, + set_selssss = map (map (map (map (Morphism.thm phi)))) set_selssss, set_intros = map (Morphism.thm phi) set_intros, set_cases = map (Morphism.thm phi) set_cases}; @@ -337,7 +337,7 @@ fun interpret_bnfs_register_fp_sugars plugins Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs map_thmss common_co_inducts co_inductss co_rec_thmss co_rec_discss co_rec_selsss rel_injectss - rel_distinctss map_disc_iffss map_selss rel_selss rel_intross rel_casess set_thmss set_selss + rel_distinctss map_disc_iffss map_selss rel_selss rel_intross rel_casess set_thmss set_selsssss set_intross 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 noted = @@ -364,7 +364,7 @@ rel_intros = nth rel_intross kk, rel_cases = nth rel_casess kk, set_thms = nth set_thmss kk, - set_sels = nth set_selss kk, + set_selssss = nth set_selsssss kk, set_intros = nth set_intross kk, set_cases = nth set_casess kk}, fp_co_induct_sugar = @@ -408,6 +408,11 @@ | zed xs (y :: ys) = f (xs, y, ys) :: zed (xs @ [y]) ys in zed [] end; +val unfla = fold_map (fn _ => fn y :: ys => (y, ys)) +val unflat = fold_map unfla +val unflatt = fold_map unflat +val unflattt = fold_map unflatt + fun uncurry_thm 0 thm = thm | uncurry_thm 1 thm = thm | uncurry_thm n thm = rotate_prems ~1 (uncurry_thm (n - 1) (rotate_prems 1 (conjI RS thm))); @@ -922,9 +927,9 @@ |> map Thm.close_derivation end; - val set_sel_thms = + val (set_sel_thmssss, set_sel_thms) = let - fun mk_goal discA selA setA ctxt = + fun mk_goal setA discA selA ctxt = let val prem = Term.betapply (discA, ta); val sel_rangeT = range_type (fastype_of selA); @@ -963,21 +968,22 @@ else ([], ctxt) end; - val (goals, names_lthy) = apfst (flat o flat o flat) - (@{fold_map 2} (fn disc => - fold_map (fn sel => fold_map (mk_goal disc sel) setAs)) - discAs selAss names_lthy); + + val (goalssss, names_lthy) = + fold_map (fn set => @{fold_map 2} (fold_map o mk_goal set) discAs selAss) + setAs names_lthy; + val goals = flat (flat (flat goalssss)); in - if null goals then - [] - else - Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) - (fn {context = ctxt, prems = _} => - mk_set_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss) (flat sel_thmss) - set0_thms) - |> Conjunction.elim_balanced (length goals) - |> Proof_Context.export names_lthy lthy - |> map Thm.close_derivation + `(fst o unflattt goalssss) + (if null goals then [] + else + Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) + (fn {context = ctxt, prems = _} => + mk_set_sel_tac ctxt (certify ctxt ta) exhaust (flat disc_thmss) + (flat sel_thmss) set0_thms) + |> Conjunction.elim_balanced (length goals) + |> Proof_Context.export names_lthy lthy + |> map Thm.close_derivation) end; val code_attrs = if plugins @{plugin code} then [Code.add_default_eqn_attrib] else []; @@ -1023,7 +1029,7 @@ map subst rel_intro_thms, [subst rel_cases_thm], map subst set_thms, - map subst set_sel_thms, + map (map (map (map subst))) set_sel_thmssss, map subst set_intros_thms, map subst set_cases_thms, map subst ctr_transfer_thms, @@ -2169,7 +2175,7 @@ fun derive_note_induct_recs_thms_for_types ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss, - rel_intross, rel_casess, set_thmss, set_selss, set_intross, set_casess, ctr_transferss, + rel_intross, rel_casess, set_thmss, set_selsssss, set_intross, set_casess, ctr_transferss, case_transferss, disc_transferss), (ctrss, _, ctr_defss, ctr_sugars)), (recs, rec_defs)), lthy) = @@ -2230,7 +2236,7 @@ fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars recs rec_defs map_thmss [induct_thm] (map single induct_thms) rec_thmss (replicate nn []) (replicate nn []) rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss - rel_intross rel_casess set_thmss set_selss set_intross set_casess ctr_transferss + rel_intross rel_casess set_thmss set_selsssss set_intross set_casess ctr_transferss case_transferss disc_transferss (replicate nn []) (replicate nn []) rec_transfer_thmss common_rel_induct_thms rel_induct_thmss [] (replicate nn []) end; @@ -2252,7 +2258,7 @@ fun derive_note_coinduct_corecs_thms_for_types ((((map_thmss, map_disc_iffss, map_selss, rel_injectss, rel_distinctss, rel_selss, - rel_intross, rel_casess, set_thmss, set_selss, set_intross, set_casess, ctr_transferss, + rel_intross, rel_casess, set_thmss, set_selsssss, set_intross, set_casess, ctr_transferss, case_transferss, disc_transferss), (_, _, ctr_defss, ctr_sugars)), (corecs, corec_defs)), lthy) = @@ -2349,7 +2355,7 @@ map_thmss [coinduct_thm, coinduct_strong_thm] (transpose [coinduct_thms, coinduct_strong_thms]) corec_thmss corec_disc_thmss corec_sel_thmsss rel_injectss rel_distinctss map_disc_iffss map_selss rel_selss - rel_intross rel_casess set_thmss set_selss set_intross set_casess ctr_transferss + rel_intross rel_casess set_thmss set_selsssss set_intross 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 [])) diff -r 97c6818f4696 -r 4cc24f1e52d5 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Oct 14 13:51:38 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Tue Oct 14 15:11:35 2014 +0200 @@ -295,7 +295,7 @@ co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss ({fp_ctr_sugar = {ctr_transfers, case_transfers, disc_transfers, ...}, fp_bnf_sugar = {map_disc_iffs, map_sels, rel_injects, rel_distincts, rel_sels, - rel_intros, rel_cases, set_thms, set_sels, set_intros, set_cases, ...}, + rel_intros, rel_cases, set_thms, set_selssss, set_intros, 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, ...}, ...} : fp_sugar) = @@ -319,7 +319,7 @@ rel_intros = rel_intros, rel_cases = rel_cases, set_thms = set_thms, - set_sels = set_sels, + set_selssss = set_selssss, set_intros = set_intros, set_cases = set_cases}, fp_co_induct_sugar = diff -r 97c6818f4696 -r 4cc24f1e52d5 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Oct 14 13:51:38 2014 +0200 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Tue Oct 14 15:11:35 2014 +0200 @@ -93,7 +93,7 @@ rel_intros = [], rel_cases = [], set_thms = [], - set_sels = [], + set_selssss = [], set_intros = [], set_cases = []}, fp_co_induct_sugar = @@ -156,7 +156,7 @@ rel_intros = [], rel_cases = [], set_thms = [], - set_sels = [], + set_selssss = [], set_intros = [], set_cases = []}, fp_co_induct_sugar =