# HG changeset patch # User blanchet # Date 1455539404 -3600 # Node ID 1abe8175861946520f5e8c7629a960de39126b80 # Parent dc837462033236b58cebc6e5dd5cb04e5c1c9623 keep 'ctor_iff_dtor' theorem around in BNF FP database diff -r dc8374620332 -r 1abe81758619 src/HOL/Basic_BNF_LFPs.thy --- a/src/HOL/Basic_BNF_LFPs.thy Mon Feb 15 12:48:10 2016 +0100 +++ b/src/HOL/Basic_BNF_LFPs.thy Mon Feb 15 13:30:04 2016 +0100 @@ -32,6 +32,9 @@ lemma xtor_rel_induct: "(\x y. vimage2p id_bnf id_bnf R x y \ IR (xtor x) (xtor y)) \ R \ IR" unfolding xtor_def vimage2p_def id_bnf_def .. +lemma xtor_iff_xtor: "u = xtor w \ xtor u = w" + unfolding xtor_def .. + lemma Inl_def_alt: "Inl \ (\a. xtor (id_bnf (Inl a)))" unfolding xtor_def id_bnf_def by (rule reflexive) diff -r dc8374620332 -r 1abe81758619 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Feb 15 12:48:10 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Mon Feb 15 13:30:04 2016 +0100 @@ -10,6 +10,7 @@ sig type fp_ctr_sugar = {ctrXs_Tss: typ list list, + ctor_iff_dtor: thm, ctr_defs: thm list, ctr_sugar: Ctr_Sugar.ctr_sugar, ctr_transfers: thm list, @@ -181,9 +182,10 @@ open BNF_FP_Util open BNF_FP_Def_Sugar_Tactics -val EqN = "Eq_"; +val Eq_prefix = "Eq_"; val case_transferN = "case_transfer"; +val ctor_iff_dtorN = "ctor_iff_dtor"; val ctr_transferN = "ctr_transfer"; val disc_transferN = "disc_transfer"; val sel_transferN = "sel_transfer"; @@ -201,6 +203,7 @@ type fp_ctr_sugar = {ctrXs_Tss: typ list list, + ctor_iff_dtor: thm, ctr_defs: thm list, ctr_sugar: Ctr_Sugar.ctr_sugar, ctr_transfers: thm list, @@ -295,9 +298,10 @@ common_set_inducts = map (Morphism.thm phi) common_set_inducts, set_inducts = map (Morphism.thm phi) set_inducts}; -fun morph_fp_ctr_sugar phi ({ctrXs_Tss, ctr_defs, ctr_sugar, ctr_transfers, case_transfers, - disc_transfers, sel_transfers} : fp_ctr_sugar) = +fun morph_fp_ctr_sugar phi ({ctrXs_Tss, ctor_iff_dtor, ctr_defs, ctr_sugar, ctr_transfers, + case_transfers, disc_transfers, sel_transfers} : fp_ctr_sugar) = {ctrXs_Tss = map (map (Morphism.typ phi)) ctrXs_Tss, + ctor_iff_dtor = Morphism.thm phi ctor_iff_dtor, ctr_defs = map (Morphism.thm phi) ctr_defs, ctr_sugar = morph_ctr_sugar phi ctr_sugar, ctr_transfers = map (Morphism.thm phi) ctr_transfers, @@ -364,8 +368,8 @@ register_fp_sugars_raw fp_sugars #> interpret_fp_sugars plugins fp_sugars; 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 + live_nesting_bnfs fp_res ctrXs_Tsss ctor_iff_dtors 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_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 @@ -379,6 +383,7 @@ fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs, fp_ctr_sugar = {ctrXs_Tss = nth ctrXs_Tsss kk, + ctor_iff_dtor = nth ctor_iff_dtors kk, ctr_defs = nth ctr_defss kk, ctr_sugar = nth ctr_sugars kk, ctr_transfers = nth ctr_transferss kk, @@ -1542,7 +1547,7 @@ flat (map2 append disc_concls ctr_concls) end; - val coinduct_cases = quasi_unambiguous_case_names (map (prefix EqN) fp_b_names); + val coinduct_cases = quasi_unambiguous_case_names (map (prefix Eq_prefix) fp_b_names); val coinduct_conclss = @{map 3} (quasi_unambiguous_case_names ooo mk_coinduct_concls) mss discss ctrss; @@ -2190,6 +2195,19 @@ val u = Free (u', fpT); + val ctor_iff_dtor_thm = + let + val goal = + fold_rev Logic.all [w, u] + (mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w))); + val vars = Variable.add_free_names lthy goal []; + in + Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} => + mk_ctor_iff_dtor_tac ctxt (map (SOME o Thm.ctyp_of lthy) [ctr_absT, fpT]) + (Thm.cterm_of lthy ctor) (Thm.cterm_of lthy dtor) ctor_dtor dtor_ctor) + |> Thm.close_derivation + end; + val ctr_rhss = map2 (fn k => fn xs => fold_rev Term.lambda xs (ctor $ mk_absumprod ctr_absT abs n k xs)) ks xss; @@ -2213,26 +2231,11 @@ fun wrap_ctrs lthy = let + val sumEN_thm' = + unfold_thms lthy @{thms unit_all_eq1} (mk_absumprodE type_definition ms); + fun exhaust_tac {context = ctxt, prems = _} = - let - val ctor_iff_dtor_thm = - let - val goal = - fold_rev Logic.all [w, u] - (mk_Trueprop_eq (HOLogic.mk_eq (u, ctor $ w), HOLogic.mk_eq (dtor $ u, w))); - val vars = Variable.add_free_names lthy goal []; - in - Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, ...} => - mk_ctor_iff_dtor_tac ctxt (map (SOME o Thm.ctyp_of lthy) [ctr_absT, fpT]) - (Thm.cterm_of lthy ctor) (Thm.cterm_of lthy dtor) ctor_dtor dtor_ctor) - |> Thm.close_derivation - end; - - val sumEN_thm' = - unfold_thms lthy @{thms unit_all_eq1} (mk_absumprodE type_definition ms); - in - mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor_thm sumEN_thm' - end; + mk_exhaust_tac ctxt n ctr_defs ctor_iff_dtor_thm sumEN_thm'; val inject_tacss = map2 (fn ctr_def => fn 0 => [] | _ => [fn {context = ctxt, ...} => @@ -2264,14 +2267,22 @@ val anonymous_notes = [([case_cong], fundefcong_attrs)] |> map (fn (thms, attrs) => ((Binding.empty, attrs), [(thms, [])])); + + val notes = + if Config.get lthy' bnf_internals then + [(ctor_iff_dtorN, [ctor_iff_dtor_thm], K [])] + |> massage_simple_notes fp_b_name + else + []; in - (ctr_sugar, lthy' |> Local_Theory.notes anonymous_notes |> snd) + (ctr_sugar, lthy' |> Local_Theory.notes (anonymous_notes @ notes) |> snd) end; fun mk_binding pre = Binding.qualify false fp_b_name (Binding.prefix_name (pre ^ "_") fp_b); fun massage_res (((ctr_sugar, maps_sets_rels), co_rec_res), lthy) = - (((maps_sets_rels, (ctrs, xss, ctr_defs, ctr_sugar)), co_rec_res), lthy); + (((maps_sets_rels, (ctrs, xss, ctor_iff_dtor_thm, ctr_defs, ctr_sugar)), co_rec_res), + lthy); in (wrap_ctrs #> (fn (ctr_sugar, lthy) => @@ -2288,7 +2299,7 @@ fun wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types (wrap_one_etc, lthy) = fold_map I wrap_one_etc lthy - |>> apsnd split_list o apfst (apsnd @{split_list 4} o apfst @{split_list 16} o split_list) + |>> apsnd split_list o apfst (apsnd @{split_list 5} o apfst @{split_list 16} o split_list) o split_list; fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects @@ -2394,7 +2405,7 @@ ((((map_thmss, map_disc_iffss, map_selsss, rel_injectss, rel_distinctss, rel_selss, rel_intross, rel_casess, set_thmss, set_selsssss, set_introsssss, set_casess, ctr_transferss, case_transferss, disc_transferss, sel_transferss), - (ctrss, _, ctr_defss, ctr_sugars)), + (ctrss, _, ctor_iff_dtors, ctr_defss, ctr_sugars)), (recs, rec_defs)), lthy) = let val ((induct_thms, induct_thm, induct_attrs), (rec_thmss, rec_attrs)) = @@ -2453,8 +2464,8 @@ |>> name_noted_thms (fst (dest_Type (hd fpTs)) ^ implode (map (prefix "_") (tl fp_b_names))) inductN |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Least_FP pre_bnfs absT_infos - 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 []) + fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctor_iff_dtors 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_selsss rel_selss 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 @@ -2541,7 +2552,7 @@ ((((map_thmss, map_disc_iffss, map_selsss, rel_injectss, rel_distinctss, rel_selss, rel_intross, rel_casess, set_thmss, set_selsssss, set_introsssss, set_casess, ctr_transferss, case_transferss, disc_transferss, sel_transferss), - (_, _, ctr_defss, ctr_sugars)), + (_, _, ctor_iff_dtors, ctr_defss, ctr_sugars)), (corecs, corec_defs)), lthy) = let val (([(coinduct_thms, coinduct_thm), (coinduct_strong_thms, coinduct_strong_thm)], @@ -2631,8 +2642,8 @@ [flat corec_sel_thmss, flat corec_thmss] |> Local_Theory.notes (common_notes @ notes) |-> interpret_bnfs_register_fp_sugars plugins fpTs fpBTs Xs Greatest_FP pre_bnfs absT_infos - fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars corecs corec_defs - map_thmss [coinduct_thm, coinduct_strong_thm] + fp_nesting_bnfs live_nesting_bnfs fp_res ctrXs_Tsss ctor_iff_dtors ctr_defss ctr_sugars + corecs corec_defs 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_selsss rel_selss rel_intross rel_casess set_thmss set_selsssss set_introsssss set_casess ctr_transferss diff -r dc8374620332 -r 1abe81758619 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Feb 15 12:48:10 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Mon Feb 15 13:30:04 2016 +0100 @@ -144,6 +144,7 @@ morph_ctr_sugar phi ctr_sugar end; + val ctor_iff_dtors = map (#ctor_iff_dtor o #fp_ctr_sugar) fp_sugars0; val ctr_defss = map (#ctr_defs o #fp_ctr_sugar) fp_sugars0; val mapss = map (#map_thms o #fp_bnf_sugar) fp_sugars0; val ctr_sugars = map2 target_ctr_sugar_of_fp_sugar fpTs fp_sugars0; @@ -291,8 +292,8 @@ val names_lthy = lthy |> fold Variable.declare_typ (As @ Cs @ Xs); val phi = Proof_Context.export_morphism names_lthy lthy; - fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctr_defs ctr_sugar co_rec - co_rec_def map_thms co_inducts co_rec_thms co_rec_disc_thms co_rec_sel_thmss + fun mk_target_fp_sugar T X kk pre_bnf absT_info ctrXs_Tss ctor_iff_dtor ctr_defs ctr_sugar + co_rec 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, sel_transfers, ...}, 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, ...}, @@ -305,6 +306,7 @@ fp_nesting_bnfs = fp_nesting_bnfs, live_nesting_bnfs = live_nesting_bnfs, fp_ctr_sugar = {ctrXs_Tss = ctrXs_Tss, + ctor_iff_dtor = ctor_iff_dtor, ctr_defs = ctr_defs, ctr_sugar = ctr_sugar, ctr_transfers = ctr_transfers, @@ -343,8 +345,8 @@ |> morph_fp_sugar phi; val target_fp_sugars = - @{map 16} mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctr_defss - ctr_sugars co_recs co_rec_defs mapss (transpose co_inductss') co_rec_thmss + @{map 17} mk_target_fp_sugar fpTs Xs kks pre_bnfs absT_infos ctrXs_Tsss ctor_iff_dtors + ctr_defss ctr_sugars co_recs co_rec_defs mapss (transpose co_inductss') co_rec_thmss co_rec_disc_thmss co_rec_sel_thmsss fp_sugars0; val n2m_sugar = (target_fp_sugars, fp_sugar_thms); diff -r dc8374620332 -r 1abe81758619 src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Feb 15 12:48:10 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Mon Feb 15 13:30:04 2016 +0100 @@ -74,6 +74,7 @@ live_nesting_bnfs = [], fp_ctr_sugar = {ctrXs_Tss = ctr_Tss, + ctor_iff_dtor = @{thm xtor_iff_xtor}, ctr_defs = @{thms Inl_def_alt Inr_def_alt}, ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name, ctr_transfers = @{thms Inl_transfer Inr_transfer}, @@ -142,6 +143,7 @@ live_nesting_bnfs = [], fp_ctr_sugar = {ctrXs_Tss = [ctr_Ts], + ctor_iff_dtor = @{thm xtor_iff_xtor}, ctr_defs = @{thms Pair_def_alt}, ctr_sugar = the_frozen_ctr_sugar_of ctxt fpT_name, ctr_transfers = @{thms Pair_transfer},