# HG changeset patch # User traytel # Date 1392892803 -3600 # Node ID 257bd115fcca950c7220e50126cf6e6d48a8293f # Parent b7f4da504b7538367479a8ab03ada36d40554d76 made tactics more robust diff -r b7f4da504b75 -r 257bd115fcca src/HOL/Tools/BNF/bnf_gfp.ML --- a/src/HOL/Tools/BNF/bnf_gfp.ML Wed Feb 19 22:08:47 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp.ML Thu Feb 20 11:40:03 2014 +0100 @@ -1500,7 +1500,6 @@ val UNIVs = map HOLogic.mk_UNIV Ts; val FTs = mk_FTs (passiveAs @ Ts); - val FTs' = mk_FTs (passiveBs @ Ts); val prodTs = map (HOLogic.mk_prodT o `I) Ts; val prodFTs = mk_FTs (passiveAs @ prodTs); val FTs_setss = mk_setss (passiveAs @ Ts); @@ -2172,14 +2171,13 @@ (mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_Jmap), HOLogic.mk_comp (Term.list_comb (map, fs @ fs_Jmaps), dtor))); val goals = map4 mk_goal fs_Jmaps map_FTFT's dtors dtor's; - val cTs = map (SOME o certifyT lthy) FTs'; val maps = - map5 (fn goal => fn cT => fn unfold => fn map_comp => fn map_cong0 => + map5 (fn goal => fn unfold => fn map_comp => fn map_cong0 => fn map_arg_cong => Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN - mk_map_tac m n cT unfold map_comp map_cong0) + mk_map_tac m n map_arg_cong unfold map_comp map_cong0) |> Thm.close_derivation) - goals cTs dtor_unfold_thms map_comps map_cong0s; + goals dtor_unfold_thms map_comps map_cong0s map_arg_cong_thms; in map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps end; @@ -2398,10 +2396,10 @@ val zipFTs = mk_FTs zip_ranTs; val zipTs = map3 (fn T => fn T' => fn FT => T --> T' --> FT) Ts Ts' zipFTs; val zip_zTs = mk_Ts passiveABs; - val (((zips, (abs, abs')), zip_zs), names_lthy) = names_lthy + val (((zips, (abs, abs')), (zip_zs, zip_zs')), names_lthy) = names_lthy |> mk_Frees "zip" zipTs ||>> mk_Frees' "ab" passiveABs - ||>> mk_Frees "z" zip_zTs; + ||>> mk_Frees' "z" zip_zTs; val Iphi_sets = map2 (fn phi => fn T => HOLogic.Collect_const T $ HOLogic.mk_split phi) allJphis zip_ranTs; @@ -2424,6 +2422,7 @@ fun Jrel_coinduct_tac {context = ctxt, prems = CIHs} = let +val lthy = Config.put quick_and_dirty false lthy (*XXX*) fun mk_helper_prem phi in_phi zip x y map map' dtor dtor' = let val zipxy = zip $ x $ y; @@ -2435,53 +2434,76 @@ end; val helper_prems = map9 mk_helper_prem activeJphis in_phis zips Jzs Jz's map_all_fsts map_all_snds dtors dtor's; - fun mk_helper_coind_concl fst phi x alt y map zip_unfold = - HOLogic.mk_imp (list_exists_free [if fst then y else x] (HOLogic.mk_conj (phi $ x $ y, - HOLogic.mk_eq (alt, map $ (zip_unfold $ HOLogic.mk_prod (x, y))))), - HOLogic.mk_eq (alt, if fst then x else y)); + fun mk_helper_coind_phi fst phi x alt y map zip_unfold = + list_exists_free [if fst then y else x] (HOLogic.mk_conj (phi $ x $ y, + HOLogic.mk_eq (alt, map $ (zip_unfold $ HOLogic.mk_prod (x, y))))) + val coind1_phis = map6 (mk_helper_coind_phi true) + activeJphis Jzs Jzs_copy Jz's Jmap_fsts zip_unfolds; + val coind2_phis = map6 (mk_helper_coind_phi false) + activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds; + fun mk_cts zs z's phis = + map3 (fn z => fn z' => fn phi => + SOME (certify lthy (fold_rev (Term.absfree o Term.dest_Free) [z', z] phi))) + zs z's phis @ + map (SOME o certify lthy) (splice z's zs); + val cts1 = mk_cts Jzs Jzs_copy coind1_phis; + val cts2 = mk_cts Jz's Jz's_copy coind2_phis; + + fun mk_helper_coind_concl z alt coind_phi = + HOLogic.mk_imp (coind_phi, HOLogic.mk_eq (alt, z)); val helper_coind1_concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map6 (mk_helper_coind_concl true) - activeJphis Jzs Jzs_copy Jz's Jmap_fsts zip_unfolds)); + (map3 mk_helper_coind_concl Jzs Jzs_copy coind1_phis)); val helper_coind2_concl = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj - (map6 (mk_helper_coind_concl false) - activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds)); - fun mk_helper_coind_thms vars concl = - Goal.prove_sorry lthy [] [] - (fold_rev Logic.all (Jphis @ activeJphis @ vars @ zips) - (Logic.list_implies (helper_prems, concl))) + (map3 mk_helper_coind_concl Jz's Jz's_copy coind2_phis)); + + fun mk_helper_coind_thms concl cts = + Goal.prove_sorry lthy [] [] (Logic.list_implies (helper_prems, concl)) (fn {context = ctxt, prems = _} => mk_rel_coinduct_coind_tac ctxt m - dtor_map_coinduct_thm ks map_comps map_cong0s map_arg_cong_thms set_mapss - dtor_unfold_thms dtor_Jmap_thms) + (cterm_instantiate_pos cts dtor_map_coinduct_thm) ks map_comps map_cong0s + map_arg_cong_thms set_mapss dtor_unfold_thms dtor_Jmap_thms) |> Thm.close_derivation - |> split_conj_thm; - val helper_coind1_thms = mk_helper_coind_thms (Jzs @ Jzs_copy) helper_coind1_concl; - val helper_coind2_thms = mk_helper_coind_thms (Jz's @ Jz's_copy) helper_coind2_concl; - - fun mk_helper_ind_concl phi ab' ab fst snd z active_phi x y zip_unfold set = - mk_Ball (set $ z) (Term.absfree ab' (list_all_free [x, y] (HOLogic.mk_imp + |> split_conj_thm + |> Proof_Context.export names_lthy lthy; + + val helper_coind1_thms = mk_helper_coind_thms helper_coind1_concl cts1; + val helper_coind2_thms = mk_helper_coind_thms helper_coind2_concl cts2; + + fun mk_helper_ind_phi phi ab fst snd z active_phi x y zip_unfold = + list_all_free [x, y] (HOLogic.mk_imp (HOLogic.mk_conj (active_phi $ x $ y, HOLogic.mk_eq (z, zip_unfold $ HOLogic.mk_prod (x, y))), - phi $ (fst $ ab) $ (snd $ ab))))); + phi $ (fst $ ab) $ (snd $ ab))); + val helper_ind_phiss = + map4 (fn Jphi => fn ab => fn fst => fn snd => + map5 (mk_helper_ind_phi Jphi ab fst snd) + zip_zs activeJphis Jzs Jz's zip_unfolds) + Jphis abs fstABs sndABs; + val ctss = map2 (fn ab' => fn phis => + map2 (fn z' => fn phi => + SOME (certify lthy (Term.absfree ab' (Term.absfree z' phi)))) + zip_zs' phis @ + map (SOME o certify lthy) zip_zs) + abs' helper_ind_phiss; + fun mk_helper_ind_concl ab' z ind_phi set = + mk_Ball (set $ z) (Term.absfree ab' ind_phi); val mk_helper_ind_concls = - map6 (fn Jphi => fn ab' => fn ab => fn fst => fn snd => fn zip_sets => - map6 (mk_helper_ind_concl Jphi ab' ab fst snd) - zip_zs activeJphis Jzs Jz's zip_unfolds zip_sets) - Jphis abs' abs fstABs sndABs zip_setss + map3 (fn ab' => fn ind_phis => fn zip_sets => + map3 (mk_helper_ind_concl ab') zip_zs ind_phis zip_sets) + abs' helper_ind_phiss zip_setss |> map (HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj); - + val helper_ind_thmss = if m = 0 then replicate n [] else - map3 (fn concl => fn j => fn set_induct => - Goal.prove_sorry lthy [] [] - (fold_rev Logic.all (Jphis @ activeJphis @ zip_zs @ zips) - (Logic.list_implies (helper_prems, concl))) + map4 (fn concl => fn j => fn set_induct => fn cts => + Goal.prove_sorry lthy [] [] (Logic.list_implies (helper_prems, concl)) (fn {context = ctxt, prems = _} => mk_rel_coinduct_ind_tac ctxt m ks - dtor_unfold_thms set_mapss j set_induct) + dtor_unfold_thms set_mapss j (cterm_instantiate_pos cts set_induct)) |> Thm.close_derivation - |> split_conj_thm) - mk_helper_ind_concls ls dtor_Jset_induct_thms + |> split_conj_thm + |> Proof_Context.export names_lthy lthy) + mk_helper_ind_concls ls dtor_Jset_induct_thms ctss |> transpose; in mk_rel_coinduct_tac ctxt CIHs in_rels in_Jrels diff -r b7f4da504b75 -r 257bd115fcca src/HOL/Tools/BNF/bnf_gfp_tactics.ML --- a/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Wed Feb 19 22:08:47 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_gfp_tactics.ML Thu Feb 20 11:40:03 2014 +0100 @@ -43,7 +43,7 @@ val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list -> thm list list -> thm list list -> thm list list list -> tactic val mk_map_id0_tac: thm list -> thm -> thm -> tactic - val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic + val mk_map_tac: int -> int -> thm -> thm -> thm -> thm -> tactic val mk_dtor_map_unique_tac: Proof.context -> thm -> thm list -> tactic val mk_mor_Abs_tac: Proof.context -> thm list -> thm list -> tactic val mk_mor_Rep_tac: Proof.context -> thm list -> thm list -> thm list -> thm list list -> @@ -795,12 +795,12 @@ rtac CollectI, etac (refl RSN (2, @{thm subst_Pair}))]) ks] 1 end; -fun mk_map_tac m n cT unfold map_comp map_cong0 = +fun mk_map_tac m n map_arg_cong unfold map_comp map_cong0 = EVERY' [rtac ext, rtac (o_apply RS trans RS sym), rtac (o_apply RS trans RS sym), rtac (unfold RS trans), rtac (Thm.permute_prems 0 1 (map_comp RS box_equals)), 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), - rtac (o_apply RS (Drule.instantiate' [cT] [] arg_cong) RS sym)] 1; + rtac map_arg_cong, rtac (o_apply RS sym)] 1; fun mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss = EVERY' [rtac hset_minimal, @@ -1018,7 +1018,7 @@ dtor_unfolds dtor_maps = let val n = length ks; in - EVERY' [DETERM o rtac coinduct, + EVERY' [rtac coinduct, EVERY' (map7 (fn i => fn map_comp0 => fn map_cong => fn map_arg_cong => fn set_map0s => fn dtor_unfold => fn dtor_map => EVERY' [REPEAT_DETERM o eresolve_tac [exE, conjE],