# HG changeset patch # User traytel # Date 1394459182 -3600 # Node ID 8d3df792d47e450e932461942d022f5146ba1632 # Parent 8875cdcfc85b3423607d9cfa0887d955fc8d23a8 tuned tactic diff -r 8875cdcfc85b -r 8d3df792d47e src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 10 13:23:16 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Mon Mar 10 14:46:22 2014 +0100 @@ -231,7 +231,7 @@ val rel_converseps = map rel_conversep_of_bnf bnfs; val rel_Grps = map rel_Grp_of_bnf bnfs; val rel_OOs = map rel_OO_of_bnf bnfs; - val rel_OO_Grps = map rel_OO_Grp_of_bnf bnfs; + val in_rels = map in_rel_of_bnf bnfs; val timer = time (timer "Extracted terms & thms"); @@ -757,7 +757,7 @@ Goal.prove_sorry lthy [] [] (fold_rev Logic.all (Bs @ ss @ B's @ s's @ Rs @ Rs_copy) (Logic.list_implies (prems, concl))) - (K ((hyp_subst_tac lthy THEN' atac) 1)) + (fn {context = ctxt, prems = _} => (hyp_subst_tac ctxt THEN' atac) 1) |> Thm.close_derivation end; @@ -775,7 +775,7 @@ Goal.prove_sorry lthy [] [] (fold_rev Logic.all (Bs @ ss @ B's @ s's @ Rs) (mk_Trueprop_eq (mk_bis Bs ss B's s's Rs, rhs))) - (K (mk_bis_rel_tac lthy m bis_def rel_OO_Grps map_comps map_cong0s set_mapss)) + (K (mk_bis_rel_tac m bis_def in_rels map_comps map_cong0s set_mapss)) |> Thm.close_derivation end; @@ -1905,7 +1905,6 @@ ||>> mk_Frees "S" activephiTs ||>> mk_Frees "JR" activeJphiTs; val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; - val in_rels = map in_rel_of_bnf bnfs; fun mk_Jrel_DEADID_coinduct_thm () = mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis (map HOLogic.eq_const Ts) Jphis diff -r 8875cdcfc85b -r 8d3df792d47e src/HOL/Tools/BNF/bnf_gfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Mon Mar 10 13:23:16 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Mon Mar 10 14:46:22 2014 +0100 @@ -13,7 +13,7 @@ val mk_bis_O_tac: Proof.context -> int -> thm -> thm list -> thm list -> tactic val mk_bis_Union_tac: Proof.context -> thm -> thm list -> tactic val mk_bis_converse_tac: int -> thm -> thm list -> thm list -> tactic - val mk_bis_rel_tac: Proof.context -> int -> thm -> thm list -> thm list -> thm list -> + val mk_bis_rel_tac: int -> thm -> thm list -> thm list -> thm list -> thm list list -> tactic val mk_coalgT_tac: Proof.context -> int -> thm list -> thm list -> thm list list -> tactic val mk_coalg_final_tac: int -> thm -> thm list -> thm list -> thm list list -> thm list list -> @@ -214,38 +214,36 @@ (rev ((1 upto n) ~~ (active_set_map0s ~~ coalg_sets)))]) (rec_Sucs ~~ (morEs ~~ (map (chop m) set_map0ss ~~ map (drop m) coalg_setss)))] 1; -fun mk_bis_rel_tac ctxt m bis_def rel_OO_Grps map_comp0s map_cong0s set_map0ss = +fun mk_bis_rel_tac m bis_def in_rels map_comp0s map_cong0s set_map0ss = let - val n = length rel_OO_Grps; - val thms = ((1 upto n) ~~ map_comp0s ~~ map_cong0s ~~ set_map0ss ~~ rel_OO_Grps); + val n = length in_rels; + val thms = ((1 upto n) ~~ map_comp0s ~~ map_cong0s ~~ set_map0ss ~~ in_rels); - fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), rel_OO_Grp) = + fun mk_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) = EVERY' [rtac allI, rtac allI, rtac impI, dtac (mk_conjunctN n i), - etac allE, etac allE, etac impE, atac, etac bexE, etac conjE, - rtac (rel_OO_Grp RS sym RS @{thm eq_refl} RS @{thm predicate2D}), - rtac @{thm relcomppI}, rtac @{thm conversepI}, - EVERY' (map (fn thm => - EVERY' [rtac @{thm GrpI}, - rtac trans, rtac trans, rtac map_comp0, rtac map_cong0, REPEAT_DETERM_N m o rtac thm, - REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong), atac, - REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI, - CONJ_WRAP' (fn (i, thm) => - if i <= m - then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans, - etac @{thm image_mono}, rtac @{thm image_subsetI}, rtac CollectI, - rtac @{thm case_prodI}, rtac refl] - else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm, - rtac trans_fun_cong_image_id_id_apply, etac @{thm Collect_split_in_rel_leI}]) - (1 upto (m + n) ~~ set_map0s)]) - @{thms fst_diag_id snd_diag_id})]; + etac allE, etac allE, etac impE, atac, etac bexE, + REPEAT_DETERM o eresolve_tac [CollectE, conjE], + rtac (in_rel RS iffD2), rtac exI, rtac (Drule.rotate_prems 1 conjI), + CONJ_WRAP' (fn thm => EVERY' [rtac trans, rtac trans, rtac map_comp0, rtac map_cong0, + REPEAT_DETERM_N m o rtac thm, REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong), + atac]) + @{thms fst_diag_id snd_diag_id}, + rtac CollectI, + CONJ_WRAP' (fn (i, thm) => + if i <= m + then EVERY' [rtac ord_eq_le_trans, rtac thm, rtac subset_trans, + etac @{thm image_mono}, rtac @{thm image_subsetI}, rtac CollectI, + rtac @{thm case_prodI}, rtac refl] + else EVERY' [rtac ord_eq_le_trans, rtac trans, rtac thm, + rtac trans_fun_cong_image_id_id_apply, etac @{thm Collect_split_in_rel_leI}]) + (1 upto (m + n) ~~ set_map0s)]; - fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_map0s), rel_OO_Grp) = + fun mk_only_if_tac ((((i, map_comp0), map_cong0), set_map0s), in_rel) = EVERY' [dtac (mk_conjunctN n i), rtac allI, rtac allI, rtac impI, etac allE, etac allE, etac impE, atac, - dtac (rel_OO_Grp RS @{thm eq_refl} RS @{thm predicate2D}), + dtac (in_rel RS @{thm iffD1}), REPEAT_DETERM o eresolve_tac ([CollectE, conjE, exE] @ - @{thms GrpE relcomppE conversepE CollectE Collect_split_in_rel_leE}), - hyp_subst_tac ctxt, + @{thms CollectE Collect_split_in_rel_leE}), rtac bexI, rtac conjI, rtac trans, rtac map_comp0, rtac trans, rtac map_cong0, REPEAT_DETERM_N m o rtac (@{thm id_comp} RS fun_cong), REPEAT_DETERM_N n o rtac (@{thm comp_id} RS fun_cong),