# HG changeset patch # User wenzelm # Date 1379530486 -7200 # Node ID edbd6bc472b4cc7a24bfda98a9868cd30fd9fec4 # Parent 2a9a5dcf764f8420218776c1bdc678923926d7fd# Parent 9e28c41e3595af7e1fe9f11c95eff439bf57986d merged; diff -r 2a9a5dcf764f -r edbd6bc472b4 src/HOL/BNF/Tools/bnf_ctr_sugar.ML --- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Wed Sep 18 20:33:36 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML Wed Sep 18 20:54:46 2013 +0200 @@ -518,23 +518,23 @@ ks goals inject_thmss distinct_thmsss end; - val (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms, - disc_exhaust_thms, collapse_thms, expand_thms, case_conv_thms) = + val (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, nontriv_discI_thms, + disc_exclude_thms, disc_exhaust_thms, collapse_thms, expand_thms, case_conv_thms) = if no_discs_sels then - ([], [], [], [], [], [], [], [], [], []) + ([], [], [], [], [], [], [], [], [], [], []) else let fun make_sel_thm xs' case_thm sel_def = zero_var_indexes (Drule.gen_all (Drule.rename_bvars' (map (SOME o fst) xs') (Drule.forall_intr_vars (case_thm RS (sel_def RS trans))))); + val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss; + fun has_undefined_rhs thm = (case snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) of Const (@{const_name undefined}, _) => true | _ => false); - val sel_thmss = map3 (map oo make_sel_thm) xss' case_thms sel_defss; - val all_sel_thms = (if all_sels_distinct andalso forall null sel_defaultss then flat sel_thmss @@ -593,8 +593,16 @@ map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose end; - val disc_thms = flat (map2 (fn b => if is_disc_binding_valid b then I else K []) - disc_bindings disc_thmss); + val nontriv_disc_thms = + flat (map2 (fn b => if is_disc_binding_valid b then I else K []) + disc_bindings disc_thmss); + + fun is_discI_boring b = + (n = 1 andalso Binding.is_empty b) orelse Binding.eq_name (b, equal_binding); + + val nontriv_discI_thms = + flat (map2 (fn b => if is_discI_boring b then K [] else single) disc_bindings + discI_thms); val (disc_exclude_thms, (disc_exclude_thmsss', disc_exclude_thmsss)) = let @@ -693,12 +701,11 @@ |> Proof_Context.export names_lthy lthy end; in - (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms, - [disc_exhaust_thm], collapse_thms, expand_thms, case_conv_thms) + (all_sel_thms, sel_thmss, disc_thmss, nontriv_disc_thms, discI_thms, + nontriv_discI_thms, disc_exclude_thms, [disc_exhaust_thm], collapse_thms, + expand_thms, case_conv_thms) end; - val nontriv_discI_thms = if n = 1 then [] else discI_thms; - val (case_cong_thm, weak_case_cong_thm) = let fun mk_prem xctr xs xf xg = @@ -753,7 +760,7 @@ (case_congN, [case_cong_thm], []), (case_convN, case_conv_thms, []), (collapseN, collapse_thms, simp_attrs), - (discN, disc_thms, simp_attrs), + (discN, nontriv_disc_thms, simp_attrs), (discIN, nontriv_discI_thms, []), (disc_excludeN, disc_exclude_thms, []), (disc_exhaustN, disc_exhaust_thms, [exhaust_case_names_attr]), diff -r 2a9a5dcf764f -r edbd6bc472b4 src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Wed Sep 18 20:33:36 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_tactics.ML Wed Sep 18 20:54:46 2013 +0200 @@ -13,8 +13,10 @@ val mk_primcorec_ctr_of_dtr_tac: Proof.context -> int -> thm -> thm -> thm list -> tactic val mk_primcorec_ctr_or_sel_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list -> thm list -> thm list -> thm list -> tactic + val mk_primcorec_disc_of_ctr_tac: thm -> thm -> tactic; val mk_primcorec_disc_tac: Proof.context -> thm list -> thm -> int -> int -> thm list list list -> tactic + val mk_primcorec_sel_of_ctr_tac: thm -> thm -> tactic; val mk_primrec_tac: Proof.context -> int -> thm list -> thm list -> thm list -> thm -> tactic end; @@ -51,23 +53,29 @@ fun mk_primcorec_prelude ctxt defs thm = unfold_thms_tac ctxt defs THEN HEADGOAL (rtac thm) THEN unfold_thms_tac ctxt @{thms split}; -fun mk_primcorec_disc_tac ctxt defs disc k m exclsss = - mk_primcorec_prelude ctxt defs disc THEN mk_primcorec_cases_tac ctxt k m exclsss; +fun mk_primcorec_disc_tac ctxt defs disc_corec k m exclsss = + mk_primcorec_prelude ctxt defs disc_corec THEN mk_primcorec_cases_tac ctxt k m exclsss; -fun mk_primcorec_ctr_or_sel_tac ctxt defs eq_thm k m exclsss maps map_idents map_comps = - mk_primcorec_prelude ctxt defs (eq_thm RS trans) THEN +fun mk_primcorec_ctr_or_sel_tac ctxt defs f_eq k m exclsss maps map_idents map_comps = + mk_primcorec_prelude ctxt defs (f_eq RS trans) THEN mk_primcorec_cases_tac ctxt k m exclsss THEN unfold_thms_tac ctxt (@{thms if_if_True if_if_False if_True if_False if_cancel[of _ True] if_cancel[of _ False] o_def split_def sum.cases} @ maps @ map_comps @ map_idents) THEN HEADGOAL (rtac refl); -fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse disc sels = - HEADGOAL (rtac (collapse RS sym RS trans) THEN' rtac disc THEN' REPEAT_DETERM_N m o atac) THEN - unfold_thms_tac ctxt sels THEN HEADGOAL (rtac refl); +fun mk_primcorec_ctr_of_dtr_tac ctxt m collapse disc_f sel_fs = + HEADGOAL (rtac (collapse RS sym RS trans) THEN' rtac disc_f THEN' REPEAT_DETERM_N m o atac) THEN + unfold_thms_tac ctxt sel_fs THEN HEADGOAL (rtac refl); + +fun mk_primcorec_disc_of_ctr_tac discI f_ctr = + HEADGOAL (rtac discI THEN' rtac f_ctr) THEN ALLGOALS atac; -fun mk_primcorec_code_of_ctr_case_tac ctxt m ctr_thm = +fun mk_primcorec_sel_of_ctr_tac sel f_ctr = + HEADGOAL (etac (f_ctr RS arg_cong RS trans) THEN' rtac sel); + +fun mk_primcorec_code_of_ctr_case_tac ctxt m f_ctr = HEADGOAL (REPEAT o rtac @{thm eq_ifI}) THEN - mk_primcorec_prelude ctxt [] (ctr_thm RS trans) THEN + mk_primcorec_prelude ctxt [] (f_ctr RS trans) THEN REPEAT_DETERM_N m (mk_primcorec_assumption_tac ctxt) THEN HEADGOAL (asm_simp_tac (ss_only @{thms if_True if_False not_False_eq_True} ctxt)); diff -r 2a9a5dcf764f -r edbd6bc472b4 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 18 20:33:36 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML Wed Sep 18 20:54:46 2013 +0200 @@ -31,6 +31,8 @@ sels: term list, pred: int option, calls: corec_call list, + discI: thm, + sel_thms: thm list, collapse: thm, corec_thm: thm, disc_corec: thm, @@ -96,6 +98,8 @@ sels: term list, pred: int option, calls: corec_call list, + discI: thm, + sel_thms: thm list, collapse: thm, corec_thm: thm, disc_corec: thm, @@ -431,11 +435,13 @@ else No_Corec) g_i | call_of _ [q_i] [g_i, g_i'] _ = Direct_Corec (q_i, g_i, g_i'); - fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss collapse corec_thm disc_corec sel_corecs = + fun mk_ctr_spec ctr disc sels p_ho q_iss f_iss f_Tss discI sel_thms collapse corec_thm + disc_corec sel_corecs = let val nullary = not (can dest_funT (fastype_of ctr)) in {ctr = substA ctr, disc = substA disc, sels = map substA sels, pred = p_ho, - calls = map3 (call_of nullary) q_iss f_iss f_Tss, collapse = collapse, - corec_thm = corec_thm, disc_corec = disc_corec, sel_corecs = sel_corecs} + calls = map3 (call_of nullary) q_iss f_iss f_Tss, discI = discI, sel_thms = sel_thms, + collapse = collapse, corec_thm = corec_thm, disc_corec = disc_corec, + sel_corecs = sel_corecs} end; fun mk_ctr_specs index ctr_sugars p_is q_isss f_isss f_Tsss coiter_thmsss disc_coitersss @@ -445,14 +451,16 @@ val discs = #discs (nth ctr_sugars index); val selss = #selss (nth ctr_sugars index); val p_ios = map SOME p_is @ [NONE]; + val discIs = #discIs (nth ctr_sugars index); + val sel_thmss = #sel_thmss (nth ctr_sugars index); val collapses = #collapses (nth ctr_sugars index); val corec_thms = co_rec_of (nth coiter_thmsss index); val disc_corecs = (case co_rec_of (nth disc_coitersss index) of [] => [TrueI] | thms => thms); val sel_corecss = co_rec_of (nth sel_coiterssss index); in - map11 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss collapses corec_thms - disc_corecs sel_corecss + map13 mk_ctr_spec ctrs discs selss p_ios q_isss f_isss f_Tsss discIs sel_thmss collapses + corec_thms disc_corecs sel_corecss end; fun mk_spec {T, index, ctr_sugars, co_iterss = coiterss, co_iter_thmsss = coiter_thmsss, diff -r 2a9a5dcf764f -r edbd6bc472b4 src/HOL/BNF/Tools/bnf_util.ML --- a/src/HOL/BNF/Tools/bnf_util.ML Wed Sep 18 20:33:36 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_util.ML Wed Sep 18 20:54:46 2013 +0200 @@ -29,6 +29,9 @@ val map12: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm) -> 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> 'i list -> 'j list -> 'k list -> 'l list -> 'm list + val map13: ('a -> 'b -> 'c -> 'd -> 'e -> 'f -> 'g -> 'h -> 'i -> 'j -> 'k -> 'l -> 'm -> 'n) -> + 'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list -> + 'i list -> 'j list -> 'k list -> 'l list -> 'm list -> 'n list val fold_map2: ('a -> 'b -> 'c -> 'd * 'c) -> 'a list -> 'b list -> 'c -> 'd list * 'c val fold_map3: ('a -> 'b -> 'c -> 'd -> 'e * 'd) -> 'a list -> 'b list -> 'c list -> 'd -> 'e list * 'd @@ -248,6 +251,13 @@ map12 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s | map12 _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; +fun map13 _ [] [] [] [] [] [] [] [] [] [] [] [] [] = [] + | map13 f (x1::x1s) (x2::x2s) (x3::x3s) (x4::x4s) (x5::x5s) + (x6::x6s) (x7::x7s) (x8::x8s) (x9::x9s) (x10::x10s) (x11::x11s) (x12::x12s) (x13::x13s) = + f x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 :: + map13 f x1s x2s x3s x4s x5s x6s x7s x8s x9s x10s x11s x12s x13s + | map13 _ _ _ _ _ _ _ _ _ _ _ _ _ _ = raise ListPair.UnequalLengths; + fun fold_map2 _ [] [] acc = ([], acc) | fold_map2 f (x1::x1s) (x2::x2s) acc = let