# HG changeset patch # User blanchet # Date 1455725316 -3600 # Node ID e85c42f4f30af2b4ccda496e0d8f148e7b3c99fc # Parent 15176172701e3e2020a2c1cede8210163cda99e8 making 'pred_inject' a first-class BNF citizen diff -r 15176172701e -r e85c42f4f30a NEWS --- a/NEWS Wed Feb 17 17:08:03 2016 +0100 +++ b/NEWS Wed Feb 17 17:08:36 2016 +0100 @@ -27,6 +27,10 @@ "bnf" outputs a new proof obligation expressing pred in terms of set (not giving a specification for pred makes this one reflexive) INCOMPATIBILITY: manual "bnf" declarations may need adjustment + - Renamed lemmas: + rel_prod_apply ~> rel_prod_inject + pred_prod_apply ~> pred_prod_inject + INCOMPATIBILITY. New in Isabelle2016 (February 2016) diff -r 15176172701e -r e85c42f4f30a src/HOL/BNF_Fixpoint_Base.thy --- a/src/HOL/BNF_Fixpoint_Base.thy Wed Feb 17 17:08:03 2016 +0100 +++ b/src/HOL/BNF_Fixpoint_Base.thy Wed Feb 17 17:08:36 2016 +0100 @@ -236,6 +236,12 @@ lemma Pair_transfer: "rel_fun A (rel_fun B (rel_prod A B)) Pair Pair" unfolding rel_fun_def by simp +lemma eq_onp_live_step: "x = y \ eq_onp P a a \ x \ P a \ y" + by (simp only: eq_onp_same_args) + +lemma top_conj: "top x \ P \ P" "P \ top x \ P" + by blast+ + ML_file "Tools/BNF/bnf_fp_util.ML" ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML" ML_file "Tools/BNF/bnf_fp_def_sugar.ML" diff -r 15176172701e -r e85c42f4f30a src/HOL/Basic_BNF_LFPs.thy --- a/src/HOL/Basic_BNF_LFPs.thy Wed Feb 17 17:08:03 2016 +0100 +++ b/src/HOL/Basic_BNF_LFPs.thy Wed Feb 17 17:08:36 2016 +0100 @@ -97,7 +97,7 @@ ML_file "~~/src/HOL/Tools/Old_Datatype/old_size.ML" -lemma size_bool[code]: "size (b::bool) = 0" +lemma size_bool[code]: "size (b :: bool) = 0" by (cases b) auto declare prod.size[no_atp] diff -r 15176172701e -r e85c42f4f30a src/HOL/Basic_BNFs.thy --- a/src/HOL/Basic_BNFs.thy Wed Feb 17 17:08:03 2016 +0100 +++ b/src/HOL/Basic_BNFs.thy Wed Feb 17 17:08:36 2016 +0100 @@ -36,6 +36,11 @@ "P1 a \ pred_sum P1 P2 (Inl a)" | "P2 b \ pred_sum P1 P2 (Inr b)" +lemma pred_sum_inject[code, simp]: + "pred_sum P1 P2 (Inl a) \ P1 a" + "pred_sum P1 P2 (Inr b) \ P2 b" + by (simp add: pred_sum.simps)+ + bnf "'a + 'b" map: map_sum sets: setl setr @@ -114,11 +119,11 @@ where "\P1 a; P2 b\ \ pred_prod P1 P2 (a, b)" -lemma rel_prod_apply [code, simp]: +lemma rel_prod_inject [code, simp]: "rel_prod R1 R2 (a, b) (c, d) \ R1 a c \ R2 b d" by (auto intro: rel_prod.intros elim: rel_prod.cases) -lemma pred_prod_apply [code, simp]: +lemma pred_prod_inject [code, simp]: "pred_prod P1 P2 (a, b) \ P1 a \ P2 b" by (auto intro: pred_prod.intros elim: pred_prod.cases) @@ -178,7 +183,7 @@ show "rel_prod R S = (\x y. \z. ({fst z} \ {(x, y). R x y} \ {snd z} \ {(x, y). S x y}) \ map_prod fst fst z = x \ map_prod snd snd z = y)" - unfolding prod_set_defs rel_prod_apply relcompp.simps conversep.simps fun_eq_iff + unfolding prod_set_defs rel_prod_inject relcompp.simps conversep.simps fun_eq_iff by auto qed auto diff -r 15176172701e -r e85c42f4f30a src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Feb 17 17:08:03 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Wed Feb 17 17:08:36 2016 +0100 @@ -27,6 +27,7 @@ rel_sels: thm list, rel_intros: thm list, rel_cases: thm list, + pred_injects: thm list, set_thms: thm list, set_selssss: thm list list list list, set_introssss: thm list list list list, @@ -195,6 +196,7 @@ val map_disc_iffN = "map_disc_iff"; val map_o_corecN = "map_o_corec"; val map_selN = "map_sel"; +val pred_injectN = "pred_inject"; val rec_o_mapN = "rec_o_map"; val rec_transferN = "rec_transfer"; val set_casesN = "set_cases"; @@ -221,6 +223,7 @@ rel_sels: thm list, rel_intros: thm list, rel_cases: thm list, + pred_injects: thm list, set_thms: thm list, set_selssss: thm list list list list, set_introssss: thm list list list list, @@ -265,7 +268,7 @@ fun strong_co_induct_of [_, s] = s; fun morph_fp_bnf_sugar phi ({map_thms, map_disc_iffs, map_selss, rel_injects, rel_distincts, - rel_sels, rel_intros, rel_cases, set_thms, set_selssss, set_introssss, + rel_sels, rel_intros, rel_cases, pred_injects, set_thms, set_selssss, set_introssss, set_cases} : fp_bnf_sugar) = {map_thms = map (Morphism.thm phi) map_thms, map_disc_iffs = map (Morphism.thm phi) map_disc_iffs, @@ -275,6 +278,7 @@ rel_sels = map (Morphism.thm phi) rel_sels, rel_intros = map (Morphism.thm phi) rel_intros, rel_cases = map (Morphism.thm phi) rel_cases, + pred_injects = map (Morphism.thm phi) pred_injects, set_thms = map (Morphism.thm phi) set_thms, set_selssss = map (map (map (map (Morphism.thm phi)))) set_selssss, set_introssss = map (map (map (map (Morphism.thm phi)))) set_introssss, @@ -369,10 +373,10 @@ 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 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 - set_inductss sel_transferss co_rec_o_mapss noted = + rel_distinctss map_disc_iffss map_selsss rel_selss rel_intross rel_casess pred_injectss + 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 co_rec_o_mapss noted = let val fp_sugars = map_index (fn (kk, T) => @@ -398,6 +402,7 @@ rel_sels = nth rel_selss kk, rel_intros = nth rel_intross kk, rel_cases = nth rel_casess kk, + pred_injects = nth pred_injectss kk, set_thms = nth set_thmss kk, set_selssss = nth set_selsssss kk, set_introssss = nth set_introsssss kk, @@ -566,10 +571,10 @@ b_names Ts thmss) #> filter_out (null o fst o hd o snd); -fun derive_map_set_rel_thms plugins fp live As Bs C E abs_inverses ctr_defs' fp_nesting_set_maps - live_nesting_map_id0s live_nesting_set_maps live_nesting_rel_eqs fp_b_name fp_bnf fpT ctor - ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm - ctr_Tss abs +fun derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs' + fp_nesting_set_maps fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps + live_nesting_rel_eqs live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor ctor_dtor + dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs ({casex, case_thms, discs, selss, sel_defs, ctrs, exhaust, exhaust_discs, disc_thmss, sel_thmss, injects, distincts, distinct_discsss, ...} : ctr_sugar) lthy = @@ -582,13 +587,15 @@ val fpBT = B_ify_T fpT; val live_AsBs = filter (op <>) (As ~~ Bs); + val live_As = map fst live_AsBs; val fTs = map (op -->) live_AsBs; - val (((((((xss, yss), fs), Rs), ta), tb), thesis), names_lthy) = lthy + val ((((((((xss, yss), fs), Ps), Rs), ta), tb), thesis), names_lthy) = lthy |> fold (fold Variable.declare_typ) [As, Bs] |> mk_Freess "x" ctr_Tss ||>> mk_Freess "y" (map (map B_ify_T) ctr_Tss) ||>> mk_Frees "f" fTs + ||>> mk_Frees "P" (map mk_pred1T live_As) ||>> mk_Frees "R" (map (uncurry mk_pred2T) live_AsBs) ||>> yield_singleton (mk_Frees "a") fpT ||>> yield_singleton (mk_Frees "b") fpBT @@ -597,7 +604,7 @@ val ctrAs = map (mk_ctr As) ctrs; val ctrBs = map (mk_ctr Bs) ctrs; - fun derive_rel_cases relAsBs rel_inject_thms rel_distinct_thms = + fun derive_rel_case relAsBs rel_inject_thms rel_distinct_thms = let val rel_Rs_a_b = list_comb (relAsBs, Rs) $ ta $ tb; @@ -622,13 +629,13 @@ val goal = Logic.list_implies (HOLogic.mk_Trueprop rel_Rs_a_b :: assms, thesis); in Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => - mk_rel_cases_tac ctxt (Thm.cterm_of ctxt ta) (Thm.cterm_of ctxt tb) exhaust injects + mk_rel_case_tac ctxt (Thm.cterm_of ctxt ta) (Thm.cterm_of ctxt tb) exhaust injects rel_inject_thms distincts rel_distinct_thms live_nesting_rel_eqs) |> singleton (Proof_Context.export names_lthy lthy) |> Thm.close_derivation end; - fun derive_case_transfer rel_cases_thm = + fun derive_case_transfer rel_case_thm = let val (S, names_lthy) = yield_singleton (mk_Frees "S") (mk_pred2T C E) names_lthy; val caseA = mk_case As C casex; @@ -636,7 +643,7 @@ val goal = mk_parametricity_goal names_lthy (S :: Rs) caseA caseB; in Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => - mk_case_transfer_tac ctxt rel_cases_thm case_thms) + mk_case_transfer_tac ctxt rel_case_thm case_thms) |> singleton (Proof_Context.export names_lthy lthy) |> Thm.close_derivation end; @@ -645,9 +652,9 @@ if plugins transfer_plugin then let val relAsBs = HOLogic.eq_const fpT; - val rel_cases_thm = derive_rel_cases relAsBs [] []; - - val case_transfer_thm = derive_case_transfer rel_cases_thm; + val rel_case_thm = derive_rel_case relAsBs [] []; + + val case_transfer_thm = derive_case_transfer rel_case_thm; val notes = [(case_transferN, [case_transfer_thm], K [])] @@ -658,11 +665,11 @@ val subst = Morphism.thm (substitute_noted_thm noted); in - (([], [], [], [], [], [], [], [], [], [], [], [], [], [subst case_transfer_thm], [], []), - lthy') + (([], [], [], [], [], [], [], [], [], [], [], [], [], [], [subst case_transfer_thm], [], + []), lthy') end else - (([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], []), lthy) + (([], [], [], [], [], [], [], [], [], [], [], [], [], [], [], [], []), lthy) else let val mapx = mk_map live As Bs (map_of_bnf fp_bnf); @@ -891,7 +898,8 @@ (map (rapp ta) selAs) (map (rapp tb) selBs)))]); val goals = - if n = 0 then [] + if n = 0 then + [] else [mk_Trueprop_eq (build_rel_app names_lthy Rs [] ta tb, (case flat (@{map 5} (mk_conjunct n) (1 upto n) discAs selAss discBs selBss) of @@ -909,9 +917,9 @@ map prove goals end; - val (rel_cases_thm, rel_cases_attrs) = + val (rel_case_thm, rel_case_attrs) = let - val thm = derive_rel_cases relAsBs rel_inject_thms rel_distinct_thms; + val thm = derive_rel_case relAsBs rel_inject_thms rel_distinct_thms; val ctr_names = quasi_unambiguous_case_names (map name_of_ctr ctrAs); val case_names_attr = Attrib.internal (K (Rule_Cases.case_names ctr_names)); val consumes_attr = Attrib.internal (K (Rule_Cases.consumes 1)); @@ -920,16 +928,18 @@ (thm, [consumes_attr, case_names_attr, cases_pred_attr ""]) end; - val case_transfer_thm = derive_case_transfer rel_cases_thm; + val case_transfer_thm = derive_case_transfer rel_case_thm; val sel_transfer_thms = - if null selAss then [] + if null selAss then + [] else let val shared_sels = foldl1 (uncurry (inter (op =))) (map (op ~~) (selAss ~~ selBss)); val goals = map (uncurry (mk_parametricity_goal names_lthy Rs)) shared_sels; in - if null goals then [] + if null goals then + [] else let val goal = Logic.mk_conjunction_balanced goals; @@ -1092,6 +1102,51 @@ end) end; + val pred_injects = + let + fun top_sweep_rewr_conv rewrs = + Conv.top_sweep_conv (K (Conv.rewrs_conv rewrs)) @{context}; + + val rel_eq_onp_with_tops_of = Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv + (top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}))); + + val eq_onps = map (rel_eq_onp_with_tops_of) + (map rel_eq_onp_of_bnf fp_bnfs @ fp_nesting_rel_eq_onps @ live_nesting_rel_eq_onps); + val cTs = map (SOME o Thm.ctyp_of lthy) (maps (replicate 2) live_As); + val cts = map (SOME o Thm.cterm_of lthy) (map mk_eq_onp Ps); + + val get_rhs = Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq #> snd; + + val pred_eq_onp_conj = + List.foldr (fn (_, thm) => thm RS @{thm eq_onp_live_step}) @{thm refl[of True]}; + + fun predify_rel_inject rel_inject = + let + val conjuncts = try (get_rhs #> HOLogic.dest_conj) rel_inject |> the_default []; + + fun postproc thm = + if conjuncts <> [] then + @{thm box_equals} OF [thm, @{thm eq_onp_same_args}, + pred_eq_onp_conj conjuncts |> unfold_thms lthy @{thms simp_thms(21)}] + else + thm RS (@{thm eq_onp_same_args} RS iffD1); + in + rel_inject + |> Thm.instantiate' cTs cts + |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv + (Raw_Simplifier.rewrite lthy false + @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}))) + |> unfold_thms lthy eq_onps + |> postproc + |> unfold_thms lthy @{thms top_conj} + end; + in + rel_inject_thms + |> map (unfold_thms lthy [@{thm conj_assoc}]) + |> map predify_rel_inject + |> Proof_Context.export names_lthy lthy + end; + val code_attrs = if plugins code_plugin then [Code.add_default_eqn_attrib] else []; val anonymous_notes = @@ -1106,7 +1161,8 @@ (mapN, map_thms, K (code_attrs @ nitpicksimp_attrs @ simp_attrs)), (map_disc_iffN, map_disc_iff_thms, K simp_attrs), (map_selN, map_sel_thms, K []), - (rel_casesN, [rel_cases_thm], K rel_cases_attrs), + (pred_injectN, pred_injects, K simp_attrs), + (rel_casesN, [rel_case_thm], K rel_case_attrs), (rel_distinctN, rel_distinct_thms, K simp_attrs), (rel_injectN, rel_inject_thms, K simp_attrs), (rel_introsN, rel_intro_thms, K []), @@ -1133,7 +1189,8 @@ map subst rel_distinct_thms, map subst rel_sel_thms, map subst rel_intro_thms, - [subst rel_cases_thm], + [subst rel_case_thm], + map subst pred_injects, map subst set_thms, map (map (map (map subst))) set_sel_thmssss, map (map (map (map subst))) set_intros_thmssss, @@ -2143,10 +2200,12 @@ val pre_set_defss = map set_defs_of_bnf pre_bnfs; 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 fp_nesting_rel_eq_onps = map rel_eq_onp_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; + val live_nesting_rel_eq_onps = map rel_eq_onp_of_bnf live_nesting_bnfs; val live = live_of_bnf any_fp_bnf; val _ = @@ -2287,10 +2346,11 @@ in (wrap_ctrs #> (fn (ctr_sugar, lthy) => - derive_map_set_rel_thms plugins fp live As Bs C E abs_inverses ctr_defs' - fp_nesting_set_maps live_nesting_map_id0s live_nesting_set_maps live_nesting_rel_eqs - fp_b_name fp_bnf fpT ctor ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def - fp_map_thm fp_set_thms fp_rel_thm ctr_Tss abs ctr_sugar lthy + derive_map_set_rel_pred_thms plugins fp live As Bs C E abs_inverses ctr_defs' + fp_nesting_set_maps fp_nesting_rel_eq_onps live_nesting_map_id0s live_nesting_set_maps + live_nesting_rel_eqs live_nesting_rel_eq_onps fp_b_name fp_bnf fp_bnfs fpT ctor + ctor_dtor dtor_ctor pre_map_def pre_set_defs pre_rel_def fp_map_thm fp_set_thms + fp_rel_thm ctr_Tss abs ctr_sugar lthy |>> pair ctr_sugar) ##>> (if fp = Least_FP then define_rec (the recs_args_types) mk_binding fpTs Cs reps @@ -2298,9 +2358,9 @@ #> massage_res, lthy') end; - fun wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types (wrap_one_etc, lthy) = + fun wrap_ctrs_derive_map_set_rel_pred_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 5} o apfst @{split_list 16} o split_list) + |>> apsnd split_list o apfst (apsnd @{split_list 5} o apfst @{split_list 17} o split_list) o split_list; fun mk_simp_thms ({injects, distincts, case_thms, ...} : ctr_sugar) co_recs map_thms rel_injects @@ -2337,7 +2397,8 @@ end; fun derive_rec_o_map_thmss lthy recs rec_defs = - if live = 0 then replicate nn [] + if live = 0 then + replicate nn [] else let fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy); @@ -2404,7 +2465,7 @@ 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, + rel_intross, rel_casess, pred_injectss, set_thmss, set_selsssss, set_introsssss, set_casess, ctr_transferss, case_transferss, disc_transferss, sel_transferss), (ctrss, _, ctor_iff_dtors, ctr_defss, ctr_sugars)), (recs, rec_defs)), lthy) = @@ -2468,10 +2529,10 @@ 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 - common_rel_induct_thms rel_induct_thmss [] (replicate nn []) sel_transferss - rec_o_map_thmss + rel_intross rel_casess pred_injectss 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 = @@ -2491,7 +2552,8 @@ end; fun derive_map_o_corec_thmss lthy0 lthy2 corecs corec_defs = - if live = 0 then replicate nn [] + if live = 0 then + replicate nn [] else let fun variant_names n pre = fst (Variable.variant_fixes (replicate n pre) lthy0); @@ -2551,8 +2613,8 @@ fun derive_note_coinduct_corecs_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, set_casess, - ctr_transferss, case_transferss, disc_transferss, sel_transferss), + rel_intross, rel_casess, pred_injectss, set_thmss, set_selsssss, set_introsssss, + set_casess, ctr_transferss, case_transferss, disc_transferss, sel_transferss), (_, _, ctor_iff_dtors, ctr_defss, ctr_sugars)), (corecs, corec_defs)), lthy) = let @@ -2647,10 +2709,11 @@ 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 - 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 map_o_corec_thmss + rel_intross rel_casess pred_injectss 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 map_o_corec_thmss end; val lthy'' = lthy' @@ -2659,7 +2722,7 @@ xtor_co_recs ctor_dtors dtor_ctors ctor_injects pre_map_defs pre_set_defss pre_rel_defs xtor_maps xtor_setss xtor_rels ns kss mss abss abs_injects type_definitions ctr_bindingss ctr_mixfixess ctr_Tsss disc_bindingss sel_bindingsss raw_sel_default_eqss - |> wrap_ctrs_derive_map_set_rel_thms_define_co_rec_for_types + |> wrap_ctrs_derive_map_set_rel_pred_thms_define_co_rec_for_types |> case_fp fp derive_note_induct_recs_thms_for_types derive_note_coinduct_corecs_thms_for_types; diff -r 15176172701e -r e85c42f4f30a src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Feb 17 17:08:03 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Wed Feb 17 17:08:36 2016 +0100 @@ -40,8 +40,8 @@ tactic val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list -> term list list list list -> thm list -> thm list -> thm list -> thm list -> tactic - val mk_rel_cases_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> - thm list -> thm list -> thm list -> tactic + val mk_rel_case_tac: Proof.context -> cterm -> cterm -> thm -> thm list -> thm list -> thm list -> + thm list -> thm list -> tactic val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list -> thm list list -> thm list list -> thm list list -> thm list -> thm list -> thm list -> thm list -> thm list -> thm list -> tactic @@ -79,7 +79,7 @@ @{thms UN_empty UN_insert UN_iff Un_empty_left Un_empty_right Un_iff Union_Un_distrib o_apply map_prod_simp mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps}; val sumprod_thms_set = @{thms UN_simps(10) image_iff} @ basic_sumprod_thms_set; -val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_apply prod.inject id_apply conj_assoc}; +val sumprod_thms_rel = @{thms rel_sum_simps rel_prod_inject prod.inject id_apply conj_assoc}; fun is_def_looping def = (case Thm.prop_of def of @@ -103,10 +103,10 @@ val co_induct_inst_as_projs_tac = PRIMITIVE oo co_induct_inst_as_projs; -fun mk_case_transfer_tac ctxt rel_cases cases = - let val n = length (tl (Thm.prems_of rel_cases)) in +fun mk_case_transfer_tac ctxt rel_case cases = + let val n = length (tl (Thm.prems_of rel_case)) in REPEAT_DETERM (HEADGOAL (rtac ctxt rel_funI)) THEN - HEADGOAL (etac ctxt rel_cases) THEN + HEADGOAL (etac ctxt rel_case) THEN ALLGOALS (hyp_subst_tac ctxt) THEN unfold_thms_tac ctxt cases THEN ALLGOALS (fn k => (select_prem_tac ctxt n (dtac ctxt asm_rl) k) k) THEN @@ -408,7 +408,7 @@ unfold_thms_tac ctxt (@{thm id_apply} :: maps @ sels @ map_id0s) THEN ALLGOALS (rtac ctxt refl); -fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs = +fun mk_rel_case_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs = HEADGOAL (rtac ctxt (infer_instantiate' ctxt [SOME ct1] exhaust) THEN_ALL_NEW rtac ctxt (infer_instantiate' ctxt [SOME ct2] exhaust) THEN_ALL_NEW hyp_subst_tac ctxt) THEN @@ -436,7 +436,7 @@ unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ sels @ simp_thms') THEN unfold_thms_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject :: abs_inject :: ctor_defs @ nesting_rel_eqs @ simp_thms' @ - @{thms id_bnf_def rel_sum_simps rel_prod_apply vimage2p_def Inl_Inr_False + @{thms id_bnf_def rel_sum_simps rel_prod_inject vimage2p_def Inl_Inr_False iffD2[OF eq_False Inr_not_Inl] sum.inject prod.inject}) THEN REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac ctxt conjE) THEN' (REPEAT_DETERM o rtac ctxt conjI) THEN' (rtac ctxt refl ORELSE' assume_tac ctxt)))) @@ -454,7 +454,7 @@ unfold_thms_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @ @{thms id_bnf_def vimage2p_def}) THEN TRYALL (hyp_subst_tac ctxt) THEN - unfold_thms_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False + unfold_thms_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_inject Inl_Inr_False Inr_Inl_False sum.inject prod.inject}) THEN TRYALL (rtac ctxt refl ORELSE' etac ctxt FalseE ORELSE' (REPEAT_DETERM o etac ctxt conjE) THEN' assume_tac ctxt)) diff -r 15176172701e -r e85c42f4f30a src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Feb 17 17:08:03 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Wed Feb 17 17:08:36 2016 +0100 @@ -299,7 +299,8 @@ 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, ...}, + rel_intros, rel_cases, pred_injects, set_thms, set_selssss, set_introssss, + set_cases, ...}, fp_co_induct_sugar = {co_rec_disc_iffs, co_rec_codes, co_rec_transfers, co_rec_o_maps, common_rel_co_inducts, rel_co_inducts, common_set_inducts, set_inducts, ...}, @@ -325,6 +326,7 @@ rel_sels = rel_sels, rel_intros = rel_intros, rel_cases = rel_cases, + pred_injects = pred_injects, set_thms = set_thms, set_selssss = set_selssss, set_introssss = set_introssss, diff -r 15176172701e -r e85c42f4f30a src/HOL/Tools/BNF/bnf_fp_util.ML --- a/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Feb 17 17:08:03 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Wed Feb 17 17:08:36 2016 +0100 @@ -661,7 +661,7 @@ val timer = time (timer "FP construction in total"); in - timer; ((pre_bnfs, absT_infos), res) + ((pre_bnfs, absT_infos), res) end; fun fp_antiquote_setup binding = diff -r 15176172701e -r e85c42f4f30a src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML --- a/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Wed Feb 17 17:08:03 2016 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_basic_sugar.ML Wed Feb 17 17:08:36 2016 +0100 @@ -90,6 +90,7 @@ rel_sels = @{thms rel_sum_sel}, rel_intros = @{thms rel_sum.intros}, rel_cases = @{thms rel_sum.cases}, + pred_injects = @{thms pred_sum_inject}, set_thms = @{thms sum_set_simps}, set_selssss = [[[@{thms set_sum_sel(1)}], [[]]], [[[]], [@{thms set_sum_sel(2)}]]], set_introssss = [[[@{thms setl.intros[OF refl]}], [[]]], @@ -154,11 +155,12 @@ {map_thms = @{thms map_prod_simp}, map_disc_iffs = [], map_selss = [@{thms fst_map_prod snd_map_prod}], - rel_injects = @{thms rel_prod_apply}, + rel_injects = @{thms rel_prod_inject}, rel_distincts = [], rel_sels = @{thms rel_prod_sel}, rel_intros = @{thms rel_prod.intros}, rel_cases = @{thms rel_prod.cases}, + pred_injects = @{thms pred_prod_inject}, set_thms = @{thms prod_set_simps}, set_selssss = [[[@{thms fsts.intros}, []]], [[[], @{thms snds.intros}]]], set_introssss = [[[@{thms fsts.intros[of "(a, b)" for a b, unfolded fst_conv]}, []]], diff -r 15176172701e -r e85c42f4f30a src/HOL/Tools/Transfer/transfer_bnf.ML --- a/src/HOL/Tools/Transfer/transfer_bnf.ML Wed Feb 17 17:08:03 2016 +0100 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Wed Feb 17 17:08:36 2016 +0100 @@ -36,14 +36,6 @@ Const (@{const_name Domainp}, PT --> argT --> HOLogic.boolT) $ P end -fun mk_eq_onp arg = - let - val argT = domain_type (fastype_of arg) - in - Const (@{const_name eq_onp}, (argT --> HOLogic.boolT) --> argT --> argT --> HOLogic.boolT) - $ arg - end - fun type_name_of_bnf bnf = T_of_bnf bnf |> dest_Type |> fst fun is_Type (Type _) = true @@ -252,57 +244,6 @@ SOME data => data | NONE => raise NO_PRED_DATA () -val rel_eq_onp_with_tops_of = Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg1_conv - (Transfer.top_sweep_rewr_conv @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}))); - -fun prove_pred_inject lthy ({T = fpT, fp_nesting_bnfs, live_nesting_bnfs, - fp_res = {bnfs = fp_bnfs, ...}, fp_bnf_sugar = {rel_injects, ...}, ...} : fp_sugar) = - let - val As = snd (dest_Type fpT) - val liveness = liveness_of_fp_bnf (length As) (hd fp_bnfs) - val lives = map_filter (uncurry (fn true => SOME | false => K NONE)) (liveness ~~ As) - - val involved_bnfs = distinct (op = o @{apply 2} BNF_Def.T_of_bnf) - (fp_nesting_bnfs @ live_nesting_bnfs @ fp_bnfs) - val eq_onps = map (rel_eq_onp_with_tops_of o rel_eq_onp_of_bnf) involved_bnfs - val old_lthy = lthy - val (As, lthy) = mk_TFrees' (map Type.sort_of_atyp lives) lthy - val predTs = map mk_pred1T As - val (preds, lthy) = mk_Frees "P" predTs lthy - val args = map mk_eq_onp preds - val cTs = map (SOME o Thm.ctyp_of lthy) (maps (replicate 2) As) - val cts = map (SOME o Thm.cterm_of lthy) args - fun get_rhs thm = thm |> Thm.concl_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq |> snd - fun is_eqn thm = can get_rhs thm - fun rel2pred_massage thm = - let - val live_step = @{lemma "x = y \ (eq_onp P a a \ x) = (P a \ y)" by (simp only: eq_onp_same_args)} - val kill_top1 = @{lemma "(top x \ P) = P" by blast} - val kill_top2 = @{lemma "(P \ top x) = P" by blast} - fun pred_eq_onp_conj conjs = List.foldr (fn (_, thm) => thm RS live_step) - @{thm refl[of True]} conjs - val conjuncts = if is_eqn thm then thm |> get_rhs |> HOLogic.dest_conj else [] - val kill_top = Local_Defs.unfold lthy [kill_top2] #> Local_Defs.unfold lthy [kill_top1] - val kill_True = Local_Defs.unfold lthy [@{thm HOL.simp_thms(21)}] - in - thm - |> Thm.instantiate' cTs cts - |> Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.arg_conv - (Raw_Simplifier.rewrite lthy false @{thms eq_onp_top_eq_eq[symmetric, THEN eq_reflection]}))) - |> Local_Defs.unfold lthy eq_onps - |> (fn thm => if conjuncts <> [] then @{thm box_equals} - OF [thm, @{thm eq_onp_same_args}, pred_eq_onp_conj conjuncts |> kill_True] - else thm RS (@{thm eq_onp_same_args} RS iffD1)) - |> kill_top - end - in - rel_injects - |> map (Local_Defs.unfold lthy [@{thm conj_assoc}]) - |> map rel2pred_massage - |> Variable.export lthy old_lthy - |> map Drule.zero_var_indexes - end - (* fp_sugar interpretation *) @@ -317,28 +258,22 @@ map (fn thm => ((Binding.empty, []), [([thm], transfer_attr)])) transfer_rules end -fun pred_injects fp_sugar lthy = +fun register_pred_injects fp_sugar lthy = let - val pred_injects = prove_pred_inject lthy fp_sugar - fun qualify defname suffix = Binding.qualified true suffix defname - val pred_inject_thm_name = qualify (base_name_of_bnf (bnf_of_fp_sugar fp_sugar)) "pred_inject" - val simp_attrs = @{attributes [simp]} + val pred_injects = #pred_injects (#fp_bnf_sugar fp_sugar) val type_name = type_name_of_bnf (#fp_bnf fp_sugar) val pred_data = lookup_defined_pred_data lthy type_name |> Transfer.update_pred_simps pred_injects in lthy - |> Local_Theory.note ((pred_inject_thm_name, simp_attrs), pred_injects) - |> snd |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => Transfer.update_pred_data type_name (Transfer.morph_pred_data phi pred_data)) |> Local_Theory.restore end - fun transfer_fp_sugars_interpretation fp_sugar lthy = let - val lthy = pred_injects fp_sugar lthy + val lthy = register_pred_injects fp_sugar lthy val transfer_rules_notes = fp_sugar_transfer_rules fp_sugar in lthy