# HG changeset patch # User traytel # Date 1393405838 -3600 # Node ID 565a20b22f098e3f3ef6a10574e5fde6a3acc96d # Parent e5128a9c431133e56f6e6f18724d7006d21d4fde made tactics more robust diff -r e5128a9c4311 -r 565a20b22f09 src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Tue Feb 25 23:14:51 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Wed Feb 26 10:10:38 2014 +0100 @@ -248,7 +248,7 @@ in Goal.prove_sorry lthy [] [] (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs))) - (K (mk_map_comp_id_tac map_comp0)) + (fn {context = ctxt, prems = _} => mk_map_comp_id_tac ctxt map_comp0) |> Thm.close_derivation end; diff -r e5128a9c4311 -r 565a20b22f09 src/HOL/Tools/BNF/bnf_lfp.ML --- a/src/HOL/Tools/BNF/bnf_lfp.ML Tue Feb 25 23:14:51 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp.ML Wed Feb 26 10:10:38 2014 +0100 @@ -119,8 +119,8 @@ bd0s Dss bnfs; val witss = map wits_of_bnf bnfs; - val ((((((((((((((((((zs, zs'), Bs), Bs_copy), B's), B''s), ss), prod_ss), s's), s''s), - fs), fs_copy), inv_fs), self_fs), gs), all_gs), (xFs, xFs')), (yFs, yFs')), + val (((((((((((((((((zs, zs'), Bs), Bs_copy), B's), B''s), ss), prod_ss), s's), s''s), + fs), fs_copy), inv_fs), self_fs), gs), all_gs), (xFs, xFs')), names_lthy) = lthy |> mk_Frees' "z" activeAs ||>> mk_Frees "B" BTs @@ -137,8 +137,7 @@ ||>> mk_Frees "f" self_fTs ||>> mk_Frees "g" gTs ||>> mk_Frees "g" all_gTs - ||>> mk_Frees' "x" FTsAs - ||>> mk_Frees' "y" FTsBs; + ||>> mk_Frees' "x" FTsAs; val passive_UNIVs = map HOLogic.mk_UNIV passiveAs; val active_UNIVs = map HOLogic.mk_UNIV activeAs; @@ -211,7 +210,7 @@ in Goal.prove_sorry lthy [] [] (fold_rev Logic.all (x :: fs @ all_gs) (mk_Trueprop_eq (lhs, rhs))) - (K (mk_map_comp_id_tac map_comp0)) + (fn {context = ctxt, prems = _} => mk_map_comp_id_tac ctxt map_comp0) |> Thm.close_derivation end; @@ -515,11 +514,11 @@ val inver_prems = map HOLogic.mk_Trueprop (map3 mk_inver inv_fs fs Bs @ map3 mk_inver fs inv_fs B's); val all_prems = prems @ inver_prems; - fun mk_s f s mapT y y' = Term.absfree y' (f $ (s $ - (Term.list_comb (mapT, passive_ids @ inv_fs) $ y))); + fun mk_s f s mapT = Library.foldl1 HOLogic.mk_comp [f, s, + Term.list_comb (mapT, passive_ids @ inv_fs)]; val alg = HOLogic.mk_Trueprop - (mk_alg B's (map5 mk_s fs ss mapsBsAs yFs yFs')); + (mk_alg B's (map3 mk_s fs ss mapsBsAs)); val copy_str_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs) (Logic.list_implies (all_prems, alg))) @@ -527,11 +526,12 @@ |> Thm.close_derivation; val iso = HOLogic.mk_Trueprop - (mk_iso B's (map5 mk_s fs ss mapsBsAs yFs yFs') Bs ss inv_fs fs_copy); + (mk_iso B's (map3 mk_s fs ss mapsBsAs) Bs ss inv_fs fs_copy); val copy_alg_thm = Goal.prove_sorry lthy [] [] (fold_rev Logic.all (Bs @ ss @ B's @ inv_fs @ fs) (Logic.list_implies (all_prems, iso))) - (K (mk_copy_alg_tac set_mapss alg_set_thms mor_def iso_alt_thm copy_str_thm)) + (fn {context = ctxt, prems = _} => + mk_copy_alg_tac ctxt set_mapss alg_set_thms mor_def iso_alt_thm copy_str_thm) |> Thm.close_derivation; val ex = HOLogic.mk_Trueprop @@ -983,11 +983,11 @@ val rec_fsts = map (Term.subst_atomic_types (activeBs ~~ Ts)) fsts; val rec_UNIVs = map2 (HOLogic.mk_UNIV oo curry HOLogic.mk_prodT) Ts activeAs; - val (((((((((Izs1, Izs1'), (Izs2, Izs2')), (xFs, xFs')), yFs), (AFss, AFss')), + val (((((((((Izs1, Izs1'), (Izs2, Izs2')), xFs), yFs), (AFss, AFss')), (fold_f, fold_f')), fs), rec_ss), names_lthy) = names_lthy |> mk_Frees' "z1" Ts ||>> mk_Frees' "z2" Ts' - ||>> mk_Frees' "x" FTs + ||>> mk_Frees "x" FTs ||>> mk_Frees "y" FTs' ||>> mk_Freess' "z" setFTss ||>> yield_singleton (apfst (op ~~) oo mk_Frees' "f") foldT @@ -1001,16 +1001,16 @@ fun ctor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (ctorN ^ "_"); val ctor_def_bind = rpair [] o Binding.conceal o Thm.def_binding o ctor_bind; - fun ctor_spec abs str map_FT_init x x' = - Term.absfree x' (abs $ (str $ - (Term.list_comb (map_FT_init, map HOLogic.id_const passiveAs @ Rep_Ts) $ x))); + fun ctor_spec abs str map_FT_init = + Library.foldl1 HOLogic.mk_comp [abs, str, + Term.list_comb (map_FT_init, map HOLogic.id_const passiveAs @ Rep_Ts)]; val ((ctor_frees, (_, ctor_def_frees)), (lthy, lthy_old)) = lthy - |> fold_map6 (fn i => fn abs => fn str => fn mapx => fn x => fn x' => + |> fold_map4 (fn i => fn abs => fn str => fn mapx => Local_Theory.define - ((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec abs str mapx x x'))) - ks Abs_Ts str_inits map_FT_inits xFs xFs' + ((ctor_bind i, NoSyn), (ctor_def_bind i, ctor_spec abs str mapx))) + ks Abs_Ts str_inits map_FT_inits |>> apsnd split_list o split_list ||> `Local_Theory.restore; diff -r e5128a9c4311 -r 565a20b22f09 src/HOL/Tools/BNF/bnf_lfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Tue Feb 25 23:14:51 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Wed Feb 26 10:10:38 2014 +0100 @@ -16,7 +16,7 @@ val mk_bd_card_order_tac: thm list -> tactic val mk_bd_limit_tac: int -> thm -> tactic val mk_card_of_min_alg_tac: thm -> thm -> thm -> thm -> thm -> tactic - val mk_copy_alg_tac: thm list list -> thm list -> thm -> thm -> thm -> tactic + val mk_copy_alg_tac: Proof.context -> thm list list -> thm list -> thm -> thm -> thm -> tactic val mk_copy_str_tac: thm list list -> thm -> thm list -> tactic val mk_ctor_induct_tac: Proof.context -> int -> thm list list -> thm -> thm list -> thm -> thm list -> thm list -> thm list -> tactic @@ -216,7 +216,8 @@ val copy_str_tac = CONJ_WRAP' (fn (thms, thm) => EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac set_mp, - rtac equalityD1, etac @{thm bij_betw_imageE}, rtac imageI, etac thm, + rtac equalityD1, etac @{thm bij_betw_imageE}, + REPEAT_DETERM_N 2 o rtac @{thm ssubst_mem[OF o_apply]}, rtac imageI, etac thm, REPEAT_DETERM_N n o set_tac thms]) (set_maps ~~ alg_sets); in @@ -224,7 +225,7 @@ stac alg_def THEN' copy_str_tac) 1 end; -fun mk_copy_alg_tac set_maps alg_sets mor_def iso_alt copy_str = +fun mk_copy_alg_tac ctxt set_maps alg_sets mor_def iso_alt copy_str = let val n = length alg_sets; val fbetw_tac = CONJ_WRAP' (K (etac @{thm bij_betwE})) alg_sets; @@ -234,12 +235,11 @@ rtac equalityD1, etac @{thm bij_betw_imageE}]; val mor_tac = CONJ_WRAP' (fn (thms, thm) => - EVERY' [rtac ballI, etac CollectE, etac @{thm inverE}, etac thm, - REPEAT_DETERM_N n o set_tac thms]) + EVERY' [rtac ballI, etac CollectE, SELECT_GOAL (unfold_thms_tac ctxt [o_apply]), + etac @{thm inverE}, etac thm, REPEAT_DETERM_N n o set_tac thms]) (set_maps ~~ alg_sets); in - (rtac (iso_alt RS iffD2) THEN' - etac copy_str THEN' REPEAT_DETERM o atac THEN' + (rtac (iso_alt RS iffD2) THEN' etac copy_str THEN' REPEAT_DETERM o atac THEN' rtac conjI THEN' stac mor_def THEN' rtac conjI THEN' fbetw_tac THEN' mor_tac THEN' CONJ_WRAP' (K atac) alg_sets) 1 end; diff -r e5128a9c4311 -r 565a20b22f09 src/HOL/Tools/BNF/bnf_tactics.ML --- a/src/HOL/Tools/BNF/bnf_tactics.ML Tue Feb 25 23:14:51 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_tactics.ML Wed Feb 26 10:10:38 2014 +0100 @@ -20,7 +20,7 @@ val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm val mk_Abs_inj_thm: thm -> thm - val mk_map_comp_id_tac: thm -> tactic + val mk_map_comp_id_tac: Proof.context -> thm -> tactic val mk_map_cong0_tac: Proof.context -> int -> thm -> tactic val mk_map_cong0L_tac: int -> thm -> thm -> tactic end; @@ -82,8 +82,8 @@ gen_tac end; -fun mk_map_comp_id_tac map_comp0 = - (rtac trans THEN' rtac map_comp0 THEN' REPEAT_DETERM o stac @{thm comp_id} THEN' rtac refl) 1; +fun mk_map_comp_id_tac ctxt map_comp0 = + (rtac trans THEN' rtac map_comp0 THEN' K (unfold_thms_tac ctxt @{thms comp_id}) THEN' rtac refl) 1; fun mk_map_cong0_tac ctxt m map_cong0 = EVERY' [rtac mp, rtac map_cong0,