# HG changeset patch # User traytel # Date 1374763613 -7200 # Node ID dacd47a0633f116eafa6351125b7f64e94e8c39f # Parent 6bf02eb4ddf7dac47d20c8633198dcf7ffa44a33 transfer rule for {c,d}tor_{,un}fold diff -r 6bf02eb4ddf7 -r dacd47a0633f src/HOL/BNF/BNF.thy --- a/src/HOL/BNF/BNF.thy Thu Jul 25 12:25:07 2013 +0200 +++ b/src/HOL/BNF/BNF.thy Thu Jul 25 16:46:53 2013 +0200 @@ -13,7 +13,7 @@ imports More_BNFs begin -hide_const (open) vimagep Gr Grp collect fsts snds setl setr +hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr convol thePull pick_middlep fstOp sndOp csquare inver image2 relImage relInvImage prefCl PrefCl Succ Shift shift diff -r 6bf02eb4ddf7 -r dacd47a0633f src/HOL/BNF/BNF_Def.thy --- a/src/HOL/BNF/BNF_Def.thy Thu Jul 25 12:25:07 2013 +0200 +++ b/src/HOL/BNF/BNF_Def.thy Thu Jul 25 16:46:53 2013 +0200 @@ -193,20 +193,20 @@ ((\i. if i \ g ` C then the_inv_into C g i else x) o g) i = id i" unfolding Func_def by (auto elim: the_inv_into_f_f) -definition vimagep where - "vimagep f g R = (\x y. R (f x) (g y))" +definition vimage2p where + "vimage2p f g R = (\x y. R (f x) (g y))" -lemma vimagepI: "R (f x) (g y) \ vimagep f g R x y" - unfolding vimagep_def by - +lemma vimage2pI: "R (f x) (g y) \ vimage2p f g R x y" + unfolding vimage2p_def by - -lemma vimagepD: "vimagep f g R x y \ R (f x) (g y)" - unfolding vimagep_def by - +lemma vimage2pD: "vimage2p f g R x y \ R (f x) (g y)" + unfolding vimage2p_def by - -lemma fun_rel_iff_leq_vimagep: "(fun_rel R S) f g = (R \ vimagep f g S)" - unfolding fun_rel_def vimagep_def by auto +lemma fun_rel_iff_leq_vimage2p: "(fun_rel R S) f g = (R \ vimage2p f g S)" + unfolding fun_rel_def vimage2p_def by auto -lemma convol_image_vimagep: " ` Collect (split (vimagep f g R)) \ Collect (split R)" - unfolding vimagep_def convol_def by auto +lemma convol_image_vimage2p: " ` Collect (split (vimage2p f g R)) \ Collect (split R)" + unfolding vimage2p_def convol_def by auto ML_file "Tools/bnf_def_tactics.ML" ML_file "Tools/bnf_def.ML" diff -r 6bf02eb4ddf7 -r dacd47a0633f src/HOL/BNF/BNF_FP_Basic.thy --- a/src/HOL/BNF/BNF_FP_Basic.thy Thu Jul 25 12:25:07 2013 +0200 +++ b/src/HOL/BNF/BNF_FP_Basic.thy Thu Jul 25 16:46:53 2013 +0200 @@ -113,6 +113,10 @@ lemma spec2: "\x y. P x y \ P x y" by blast +lemma fun_rel_def_butlast: + "(fun_rel R (fun_rel S T)) f g = (\x y. R x y \ (fun_rel S T) (f x) (g y))" + unfolding fun_rel_def .. + ML_file "Tools/bnf_fp_util.ML" ML_file "Tools/bnf_fp_def_sugar_tactics.ML" ML_file "Tools/bnf_fp_def_sugar.ML" diff -r 6bf02eb4ddf7 -r dacd47a0633f src/HOL/BNF/BNF_GFP.thy --- a/src/HOL/BNF/BNF_GFP.thy Thu Jul 25 12:25:07 2013 +0200 +++ b/src/HOL/BNF/BNF_GFP.thy Thu Jul 25 16:46:53 2013 +0200 @@ -307,6 +307,27 @@ lemma Collect_splitD: "x \ Collect (split A) \ A (fst x) (snd x)" by auto +definition image2p where + "image2p f g R = (\x y. \x' y'. R x' y' \ f x' = x \ g y' = y)" + +lemma image2pI: "R x y \ (image2p f g R) (f x) (g y)" + unfolding image2p_def by blast + +lemma image2p_eqI: "\fx = f x; gy = g y; R x y\ \ (image2p f g R) fx gy" + unfolding image2p_def by blast + +lemma image2pE: "\(image2p f g R) fx gy; (\x y. fx = f x \ gy = g y \ R x y \ P)\ \ P" + unfolding image2p_def by blast + +lemma fun_rel_iff_geq_image2p: "(fun_rel R S) f g = (image2p f g R \ S)" + unfolding fun_rel_def image2p_def by auto + +lemma convol_image_image2p: " ` Collect (split R) \ Collect (split (image2p f g R))" + unfolding convol_def image2p_def by fastforce + +lemma fun_rel_image2p: "(fun_rel R (image2p f g R)) f g" + unfolding fun_rel_def image2p_def by auto + ML_file "Tools/bnf_gfp_util.ML" ML_file "Tools/bnf_gfp_tactics.ML" ML_file "Tools/bnf_gfp.ML" diff -r 6bf02eb4ddf7 -r dacd47a0633f src/HOL/BNF/BNF_LFP.thy --- a/src/HOL/BNF/BNF_LFP.thy Thu Jul 25 12:25:07 2013 +0200 +++ b/src/HOL/BNF/BNF_LFP.thy Thu Jul 25 16:46:53 2013 +0200 @@ -226,6 +226,12 @@ shows "PROP P x y" by (rule `(\x y. PROP P x y)`) +lemma vimage2p_fun_rel: "(fun_rel (vimage2p f g R) R) f g" + unfolding fun_rel_def vimage2p_def by auto + +lemma predicate2D_vimage2p: "\R \ vimage2p f g S; R x y\ \ S (f x) (g y)" + unfolding vimage2p_def by auto + ML_file "Tools/bnf_lfp_util.ML" ML_file "Tools/bnf_lfp_tactics.ML" ML_file "Tools/bnf_lfp.ML" diff -r 6bf02eb4ddf7 -r dacd47a0633f src/HOL/BNF/Tools/bnf_def.ML --- a/src/HOL/BNF/Tools/bnf_def.ML Thu Jul 25 12:25:07 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def.ML Thu Jul 25 16:46:53 2013 +0200 @@ -374,7 +374,7 @@ val map_comp'_of_bnf = Lazy.force o #map_comp' o #facts o rep_bnf; val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf; val map_cong_of_bnf = Lazy.force o #map_cong o #facts o rep_bnf; -val map_transfer_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf; +val map_transfer_of_bnf = Lazy.force o #map_transfer o #facts o rep_bnf; val map_wppull_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf; val map_wpull_of_bnf = #map_wpull o #axioms o rep_bnf; val rel_def_of_bnf = #rel_def o #defs o rep_bnf; diff -r 6bf02eb4ddf7 -r dacd47a0633f src/HOL/BNF/Tools/bnf_def_tactics.ML --- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Jul 25 12:25:07 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Thu Jul 25 16:46:53 2013 +0200 @@ -217,13 +217,13 @@ val n = length set_map's; in REPEAT_DETERM_N n (HEADGOAL (rtac @{thm fun_relI})) THEN - unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimagep} THEN + unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimage2p} THEN HEADGOAL (EVERY' [rtac @{thm order_trans}, rtac rel_mono, REPEAT_DETERM_N n o atac, rtac @{thm predicate2I}, dtac (in_rel RS iffD1), REPEAT_DETERM o eresolve_tac [exE, CollectE, conjE], hyp_subst_tac ctxt, - rtac @{thm vimagepI}, rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI, + rtac @{thm vimage2pI}, rtac (in_rel RS iffD2), rtac exI, rtac conjI, rtac CollectI, CONJ_WRAP' (fn thm => - etac (thm RS @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimagep]]})) + etac (thm RS @{thm ord_eq_le_trans[OF _ subset_trans[OF image_mono convol_image_vimage2p]]})) set_map's, rtac conjI, EVERY' (map (fn convol => diff -r 6bf02eb4ddf7 -r dacd47a0633f src/HOL/BNF/Tools/bnf_fp_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Jul 25 12:25:07 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Jul 25 16:46:53 2013 +0200 @@ -54,6 +54,7 @@ val ctor_injectN: string val ctor_foldN: string val ctor_fold_uniqueN: string + val ctor_fold_transferN: string val ctor_mapN: string val ctor_map_uniqueN: string val ctor_recN: string @@ -82,6 +83,7 @@ val dtor_strong_coinductN: string val dtor_unfoldN: string val dtor_unfold_uniqueN: string + val dtor_unfold_transferN: string val exhaustN: string val foldN: string val hsetN: string @@ -169,6 +171,9 @@ val mk_rel_co_induct_thm: fp_kind -> term list -> term list -> term list -> term list -> term list -> term list -> term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) -> Proof.context -> thm + val mk_un_fold_transfer_thms: fp_kind -> term list -> term list -> term list -> term list -> + term list -> term list -> ({prems: thm list, context: Proof.context} -> tactic) -> + Proof.context -> thm list val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory -> 'a) -> @@ -240,6 +245,7 @@ val foldN = "fold" val unfoldN = unN ^ foldN val uniqueN = "_unique" +val transferN = "_transfer" val simpsN = "simps" val ctorN = "ctor" val dtorN = "dtor" @@ -247,6 +253,8 @@ val dtor_unfoldN = dtorN ^ "_" ^ unfoldN val ctor_fold_uniqueN = ctor_foldN ^ uniqueN val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN +val ctor_fold_transferN = ctor_foldN ^ transferN +val dtor_unfold_transferN = dtor_unfoldN ^ transferN val ctor_dtor_unfoldN = ctorN ^ "_" ^ dtor_unfoldN val ctor_mapN = ctorN ^ "_" ^ mapN val dtor_mapN = dtorN ^ "_" ^ mapN @@ -485,6 +493,25 @@ |> (fn thm => thm OF (replicate (length pre_rels) @{thm allI[OF allI[OF impI]]})) end; +fun mk_un_fold_transfer_thms fp pre_rels pre_phis rels phis un_folds un_folds' tac lthy = + let + val pre_relphis = map (fn rel => Term.list_comb (rel, phis @ pre_phis)) pre_rels; + val relphis = map (fn rel => Term.list_comb (rel, phis)) rels; + fun flip f x y = if fp = Greatest_FP then f y x else f x y; + + val arg_rels = map2 (flip mk_fun_rel) pre_relphis pre_phis; + fun mk_transfer relphi pre_phi un_fold un_fold' = + fold_rev mk_fun_rel arg_rels (flip mk_fun_rel relphi pre_phi) $ un_fold $ un_fold'; + val transfers = map4 mk_transfer relphis pre_phis un_folds un_folds'; + + val goal = fold_rev Logic.all (phis @ pre_phis) + (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj transfers)); + in + Goal.prove_sorry lthy [] [] goal tac + |> Thm.close_derivation + |> split_conj_thm + end; + fun fp_bnf construct_fp bs resBs eqs lthy = let val timer = time (Timer.startRealTimer ()); diff -r 6bf02eb4ddf7 -r dacd47a0633f src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Jul 25 12:25:07 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Jul 25 16:46:53 2013 +0200 @@ -72,12 +72,12 @@ val names_lthy = fold Variable.declare_typ deads lthy; (* tvars *) - val ((((((((passiveAs, activeAs), allAs)), (passiveBs, activeBs)), + val ((((((((passiveAs, activeAs), allAs)), ((passiveBs, activeBs), allBs')), (passiveCs, activeCs)), passiveXs), passiveYs), idxT) = names_lthy |> mk_TFrees live |> apfst (`(chop m)) ||> mk_TFrees live - ||>> apfst (chop m) + ||>> apfst (`(chop m)) ||> mk_TFrees live ||>> apfst (chop m) ||>> mk_TFrees m @@ -1762,6 +1762,11 @@ val phi = Proof_Context.export_morphism lthy_old lthy; val unfolds = map (Morphism.term phi) unfold_frees; val unfold_names = map (fst o dest_Const) unfolds; + fun mk_unfolds passives actives = + map3 (fn name => fn T => fn active => + Const (name, Library.foldr (op -->) + (map2 (curry (op -->)) actives (mk_FTs (passives @ actives)), active --> T))) + unfold_names (mk_Ts passives) actives; fun mk_unfold Ts ss i = Term.list_comb (Const (nth unfold_names (i - 1), Library.foldr (op -->) (map fastype_of ss, domain_type (fastype_of (nth ss (i - 1))) --> nth Ts (i - 1))), ss); val unfold_defs = map ((fn thm => thm RS fun_cong) o Morphism.thm phi) unfold_def_frees; @@ -2116,9 +2121,11 @@ val prodTsTs' = map2 (curry HOLogic.mk_prodT) Ts Ts'; val fstsTsTs' = map fst_const prodTsTs'; val sndsTsTs' = map snd_const prodTsTs'; + val activephiTs = map2 mk_pred2T activeAs activeBs; val activeJphiTs = map2 mk_pred2T Ts Ts'; - val ((Jphis, activeJphis), names_lthy) = names_lthy + val (((Jphis, activephis), activeJphis), names_lthy) = names_lthy |> mk_Frees "R" JphiTs + ||>> 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; @@ -2867,6 +2874,14 @@ mk_rel_co_induct_thm Greatest_FP rels activeJphis Jrels Jphis Jzs Jz's dtors dtor's Jrel_coinduct_tac lthy; + val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs; + val dtor_unfold_transfer_thms = + mk_un_fold_transfer_thms Greatest_FP rels activephis Jrels Jphis + (mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs) + (mk_unfold_transfer_tac m Jrel_coinduct_thm (map map_transfer_of_bnf bnfs) + dtor_unfold_thms) + lthy; + val timer = time (timer "relator coinduction"); val common_notes = @@ -2874,7 +2889,8 @@ (dtor_map_coinductN, [dtor_map_coinduct_thm]), (dtor_map_strong_coinductN, [dtor_map_strong_coinduct_thm]), (dtor_strong_coinductN, [dtor_strong_coinduct_thm]), - (rel_coinductN, [Jrel_coinduct_thm])] + (rel_coinductN, [Jrel_coinduct_thm]), + (dtor_unfold_transferN, dtor_unfold_transfer_thms)] |> map (fn (thmN, thms) => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); diff -r 6bf02eb4ddf7 -r dacd47a0633f src/HOL/BNF/Tools/bnf_gfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Jul 25 12:25:07 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Jul 25 16:46:53 2013 +0200 @@ -115,6 +115,8 @@ val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list -> thm list -> thm list -> thm list list -> thm list list -> tactic val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic + val mk_unfold_transfer_tac: int -> thm -> thm list -> thm list -> + {prems: thm list, context: Proof.context} -> tactic val mk_unique_mor_tac: thm list -> thm -> tactic val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic @@ -1458,4 +1460,23 @@ (in_Jrels ~~ (helper_indss ~~ (helper_coind1s ~~ helper_coind2s))) 1 end; +fun mk_unfold_transfer_tac m rel_coinduct map_transfers unfolds {context = ctxt, prems = _} = + let + val n = length map_transfers; + in + unfold_thms_tac ctxt + @{thms fun_rel_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN + unfold_thms_tac ctxt @{thms fun_rel_iff_geq_image2p} THEN + HEADGOAL (EVERY' + [REPEAT_DETERM o resolve_tac [allI, impI], rtac rel_coinduct, + EVERY' (map (fn map_transfer => EVERY' + [REPEAT_DETERM o resolve_tac [allI, impI], etac @{thm image2pE}, hyp_subst_tac ctxt, + SELECT_GOAL (unfold_thms_tac ctxt unfolds), + rtac (funpow (m + n + 1) (fn thm => thm RS @{thm fun_relD}) map_transfer), + REPEAT_DETERM_N m o rtac @{thm id_transfer}, + REPEAT_DETERM_N n o rtac @{thm fun_rel_image2p}, + etac @{thm predicate2D}, etac @{thm image2pI}]) + map_transfers)]) + end; + end; diff -r 6bf02eb4ddf7 -r dacd47a0633f src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Jul 25 12:25:07 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Jul 25 16:46:53 2013 +0200 @@ -42,12 +42,12 @@ val names_lthy = fold Variable.declare_typ deads lthy; (* tvars *) - val (((((((passiveAs, activeAs), allAs)), (passiveBs, activeBs)), + val (((((((passiveAs, activeAs), allAs)), ((passiveBs, activeBs), allBs')), activeCs), passiveXs), passiveYs) = names_lthy |> mk_TFrees live |> apfst (`(chop m)) ||> mk_TFrees live - ||>> apfst (chop m) + ||>> apfst (`(chop m)) ||>> mk_TFrees n ||>> mk_TFrees m ||> fst o mk_TFrees m; @@ -1091,6 +1091,11 @@ val phi = Proof_Context.export_morphism lthy_old lthy; val folds = map (Morphism.term phi) fold_frees; val fold_names = map (fst o dest_Const) folds; + fun mk_folds passives actives = + map3 (fn name => fn T => fn active => + Const (name, Library.foldr (op -->) + (map2 (curry (op -->)) (mk_FTs (passives @ actives)) actives, T --> active))) + fold_names (mk_Ts passives) actives; fun mk_fold Ts ss i = Term.list_comb (Const (nth fold_names (i - 1), Library.foldr (op -->) (map fastype_of ss, nth Ts (i - 1) --> range_type (fastype_of (nth ss (i - 1))))), ss); val fold_defs = map (Morphism.thm phi) fold_def_frees; @@ -1382,9 +1387,11 @@ trans OF [ctor_inject, rel_eq_of_bnf bnf RS @{thm predicate2_eqD} RS sym]; val IphiTs = map2 mk_pred2T passiveAs passiveBs; + val activephiTs = map2 mk_pred2T activeAs activeBs; val activeIphiTs = map2 mk_pred2T Ts Ts'; - val ((Iphis, activeIphis), names_lthy) = names_lthy + val (((Iphis, activephis), activeIphis), names_lthy) = names_lthy |> mk_Frees "R" IphiTs + ||>> mk_Frees "S" activephiTs ||>> mk_Frees "IR" activeIphiTs; val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; @@ -1801,12 +1808,20 @@ (mk_rel_induct_tac m ctor_induct2_thm ks ctor_Irel_thms (map rel_mono_strong_of_bnf bnfs)) lthy; + val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs; + val ctor_fold_transfer_thms = + mk_un_fold_transfer_thms Least_FP rels activephis Irels Iphis + (mk_folds passiveAs activeAs) (mk_folds passiveBs activeBs) + (mk_fold_transfer_tac m Irel_induct_thm (map map_transfer_of_bnf bnfs) ctor_fold_thms) + lthy; + val timer = time (timer "relator induction"); val common_notes = [(ctor_inductN, [ctor_induct_thm]), (ctor_induct2N, [ctor_induct2_thm]), - (rel_inductN, [Irel_induct_thm])] + (rel_inductN, [Irel_induct_thm]), + (ctor_fold_transferN, ctor_fold_transfer_thms)] |> map (fn (thmN, thms) => ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])); diff -r 6bf02eb4ddf7 -r dacd47a0633f src/HOL/BNF/Tools/bnf_lfp_tactics.ML --- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Jul 25 12:25:07 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Jul 25 16:46:53 2013 +0200 @@ -34,6 +34,8 @@ thm list -> tactic val mk_iso_alt_tac: thm list -> thm -> tactic val mk_fold_unique_mor_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> tactic + val mk_fold_transfer_tac: int -> thm -> thm list -> thm list -> + {prems: thm list, context: Proof.context} -> tactic val mk_least_min_alg_tac: thm -> thm -> tactic val mk_lfp_map_wpull_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list list -> thm list list list -> thm list -> tactic @@ -838,4 +840,24 @@ IHs ctor_rels rel_mono_strongs)] 1 end; +fun mk_fold_transfer_tac m rel_induct map_transfers folds {context = ctxt, prems = _} = + let + val n = length map_transfers; + in + unfold_thms_tac ctxt + @{thms fun_rel_def_butlast all_conj_distrib[symmetric] imp_conjR[symmetric]} THEN + unfold_thms_tac ctxt @{thms fun_rel_iff_leq_vimage2p} THEN + HEADGOAL (EVERY' + [REPEAT_DETERM o resolve_tac [allI, impI], rtac rel_induct, + EVERY' (map (fn map_transfer => EVERY' + [REPEAT_DETERM o resolve_tac [allI, impI, @{thm vimage2pI}], + SELECT_GOAL (unfold_thms_tac ctxt folds), + etac @{thm predicate2D_vimage2p}, + rtac (funpow (m + n + 1) (fn thm => thm RS @{thm fun_relD}) map_transfer), + REPEAT_DETERM_N m o rtac @{thm id_transfer}, + REPEAT_DETERM_N n o rtac @{thm vimage2p_fun_rel}, + atac]) + map_transfers)]) + end; + end;