# HG changeset patch # User desharna # Date 1415697968 -3600 # Node ID 0297e1277ed2ab87375a638835c4829948b257be # Parent a62cdcc5344b02a7e6acc0096b5ed98874d19348 make 'rec_transfer' tactic more robust diff -r a62cdcc5344b -r 0297e1277ed2 src/HOL/Datatype_Examples/Misc_Datatype.thy --- a/src/HOL/Datatype_Examples/Misc_Datatype.thy Tue Nov 11 08:57:46 2014 +0100 +++ b/src/HOL/Datatype_Examples/Misc_Datatype.thy Tue Nov 11 10:26:08 2014 +0100 @@ -34,6 +34,8 @@ datatype (discs_sels) 'a multi_live_direct8 = MultiLiveDirect8 'a 'a 'a 'a 'a 'a 'a 'a datatype (discs_sels) 'a multi_live_direct9 = MultiLiveDirect9 'a 'a 'a 'a 'a 'a 'a 'a 'a +datatype ('a, 'b) ite = ITE "'a \ bool" "'a \ 'b" "'a \ 'b" + datatype 'a live_and_fun = LiveAndFun nat "nat \ 'a" datatype (discs_sels) hfset = HFset "hfset fset" diff -r a62cdcc5344b -r 0297e1277ed2 src/HOL/Tools/BNF/bnf_fp_def_sugar.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Nov 11 08:57:46 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Tue Nov 11 10:26:08 2014 +0100 @@ -2227,12 +2227,12 @@ (Rs, Ss, map2 (mk_parametricity_goal lthy (Rs @ Ss)) co_recs co_recBs, names_lthy) end; - fun derive_rec_transfer_thms lthy recs rec_defs = + fun derive_rec_transfer_thms lthy recs rec_defs (SOME (_, _, _, xsssss)) = let val (Rs, Ss, goals, names_lthy) = mk_co_rec_transfer_goals lthy recs in Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced goals) (fn {context = ctxt, prems = _} => - mk_rec_transfer_tac ctxt nn ns (map (certify ctxt) Ss) (map (certify ctxt) Rs) rec_defs - xtor_co_rec_transfers pre_rel_defs live_nesting_rel_eqs) + mk_rec_transfer_tac ctxt nn ns (map (certify ctxt) Ss) (map (certify ctxt) Rs) xsssss + rec_defs xtor_co_rec_transfers pre_rel_defs live_nesting_rel_eqs) |> Conjunction.elim_balanced nn |> Proof_Context.export names_lthy lthy |> map Thm.close_derivation @@ -2319,7 +2319,7 @@ val rec_transfer_thmss = if live = 0 then replicate nn [] - else map single (derive_rec_transfer_thms lthy recs rec_defs); + else map single (derive_rec_transfer_thms lthy recs rec_defs recs_args_types); val induct_type_attr = Attrib.internal o K o Induct.induct_type; val induct_pred_attr = Attrib.internal o K o Induct.induct_pred; diff -r a62cdcc5344b -r 0297e1277ed2 src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Nov 11 08:57:46 2014 +0100 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Tue Nov 11 10:26:08 2014 +0100 @@ -39,7 +39,7 @@ val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context -> tactic val mk_rec_transfer_tac: Proof.context -> int -> int list -> cterm list -> cterm list -> - thm list -> thm list -> thm list -> thm list -> tactic + 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_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list -> @@ -182,12 +182,19 @@ unfold_thms_tac ctxt (ctor_rec :: fp_abs_inverse :: abs_inverse :: rec_defs @ pre_map_defs @ map_ident0s @ rec_unfold_thms) THEN HEADGOAL (rtac refl); -fun mk_rec_transfer_tac ctxt nn ns actives passives rec_defs ctor_rec_transfers rel_pre_T_defs +fun mk_rec_transfer_tac ctxt nn ns actives passives xssss rec_defs ctor_rec_transfers rel_pre_T_defs rel_eqs = let val ctor_rec_transfers' = map (cterm_instantiate_pos (map SOME (passives @ actives))) ctor_rec_transfers; val total_n = Integer.sum ns; + val True = @{term True}; + fun magic eq xs xs' = Subgoal.FOCUS (fn {prems, ...} => + let + val thm = prems + |> Ctr_Sugar_Util.permute_like eq xs xs' + |> Library.foldl1 (fn (acc, elem) => elem RS (acc RS @{thm rel_funD})) + in HEADGOAL (rtac thm) end) in HEADGOAL Goal.conjunction_tac THEN EVERY (map (fn ctor_rec_transfer => @@ -195,23 +202,27 @@ unfold_thms_tac ctxt rec_defs THEN HEADGOAL (etac (mk_rel_funDN_rotated (nn + 1) ctor_rec_transfer)) THEN unfold_thms_tac ctxt rel_pre_T_defs THEN - EVERY (fst (fold_map (fn k => fn acc => rpair (k + acc) + EVERY (fst (@{fold_map 2} (fn k => fn xsss => fn acc => + rpair (k + acc) (HEADGOAL (rtac (mk_rel_funDN_rotated 2 @{thm comp_transfer})) THEN HEADGOAL (rtac @{thm vimage2p_rel_fun}) THEN unfold_thms_tac ctxt rel_eqs THEN - EVERY (map (fn n => - REPEAT_DETERM (HEADGOAL - (rtac (mk_rel_funDN 2 case_sum_transfer_eq) ORELSE' - rtac (mk_rel_funDN 2 case_sum_transfer))) THEN + EVERY (@{map 2} (fn n => fn xss => + REPEAT_DETERM (HEADGOAL (resolve_tac + [mk_rel_funDN 2 case_sum_transfer_eq, mk_rel_funDN 2 case_sum_transfer])) THEN HEADGOAL (select_prem_tac total_n (dtac asm_rl) (acc + n)) THEN HEADGOAL (SELECT_GOAL (HEADGOAL - ((REPEAT_DETERM o (atac ORELSE' - rtac (mk_rel_funDN 1 case_prod_transfer_eq) ORELSE' - rtac (mk_rel_funDN 1 case_prod_transfer) ORELSE' - rtac rel_funI)) THEN_ALL_NEW - (REPEAT_ALL_NEW (dtac rel_funD) THEN_ALL_NEW atac))))) - (1 upto k)))) - ns 0))) + (REPEAT_DETERM o (atac ORELSE' resolve_tac + [mk_rel_funDN 1 case_prod_transfer_eq, + mk_rel_funDN 1 case_prod_transfer, + rel_funI]) THEN_ALL_NEW + (Subgoal.FOCUS (fn {prems, ...} => + let val thm = prems + |> permute_like (op =) (True :: flat xss) (True :: flat_rec_arg_args xss) + |> Library.foldl1 (fn (acc, elem) => elem RS (acc RS rel_funD)) + in HEADGOAL (rtac thm) end) ctxt))))) + (1 upto k) xsss))) + ns xssss 0))) ctor_rec_transfers') end;