# HG changeset patch # User traytel # Date 1375972708 -7200 # Node ID 2d2d9d1de1a9d791ca944eb20013165978318c55 # Parent bdd610910e2c421f5f991caed1181f43584d6f18 theorems relating {c,d}tor_(un)fold/(co)rec and {c,d}tor_map diff -r bdd610910e2c -r 2d2d9d1de1a9 src/HOL/BNF/BNF_FP_Basic.thy --- a/src/HOL/BNF/BNF_FP_Basic.thy Thu Aug 08 15:30:25 2013 +0200 +++ b/src/HOL/BNF/BNF_FP_Basic.thy Thu Aug 08 16:38:28 2013 +0200 @@ -113,6 +113,36 @@ lemma spec2: "\x y. P x y \ P x y" by blast +lemma rewriteR_comp_comp: "\g o h = r\ \ f o g o h = f o r" + unfolding o_def fun_eq_iff by auto + +lemma rewriteR_comp_comp2: "\g o h = r1 o r2; f o r1 = l\ \ f o g o h = l o r2" + unfolding o_def fun_eq_iff by auto + +lemma rewriteL_comp_comp: "\f o g = l\ \ f o (g o h) = l o h" + unfolding o_def fun_eq_iff by auto + +lemma rewriteL_comp_comp2: "\f o g = l1 o l2; l2 o h = r\ \ f o (g o h) = l1 o r" + unfolding o_def fun_eq_iff by auto + +lemma convol_o: " o h = " + unfolding convol_def by auto + +lemma map_pair_o_convol: "map_pair h1 h2 o =

" + unfolding convol_def by auto + +lemma map_pair_o_convol_id: "(map_pair f id \ ) x = f , g> x" + unfolding map_pair_o_convol id_o o_id .. + +lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)" + unfolding o_def by (auto split: sum.splits) + +lemma sum_case_o_sum_map: "sum_case f g o sum_map h1 h2 = sum_case (f o h1) (g o h2)" + unfolding o_def by (auto split: sum.splits) + +lemma sum_case_o_sum_map_id: "(sum_case id g o sum_map f id) x = sum_case (f o id) g x" + unfolding sum_case_o_sum_map id_o o_id .. + 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 .. diff -r bdd610910e2c -r 2d2d9d1de1a9 src/HOL/BNF/BNF_GFP.thy --- a/src/HOL/BNF/BNF_GFP.thy Thu Aug 08 15:30:25 2013 +0200 +++ b/src/HOL/BNF/BNF_GFP.thy Thu Aug 08 16:38:28 2013 +0200 @@ -13,9 +13,6 @@ "codatatype" :: thy_decl begin -lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)" -unfolding o_def by (auto split: sum.splits) - lemma sum_case_expand_Inr: "f o Inl = g \ f x = sum_case g (f o Inr) x" by (auto split: sum.splits) diff -r bdd610910e2c -r 2d2d9d1de1a9 src/HOL/BNF/BNF_LFP.thy --- a/src/HOL/BNF/BNF_LFP.thy Thu Aug 08 15:30:25 2013 +0200 +++ b/src/HOL/BNF/BNF_LFP.thy Thu Aug 08 16:38:28 2013 +0200 @@ -44,9 +44,6 @@ lemma snd_convol': "snd ( x) = g x" using snd_convol unfolding convol_def by simp -lemma convol_o: " o h = " - unfolding convol_def by auto - lemma convol_expand_snd: "fst o f = g \ = f" unfolding convol_def by auto diff -r bdd610910e2c -r 2d2d9d1de1a9 src/HOL/BNF/Tools/bnf_fp_util.ML --- a/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Aug 08 15:30:25 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Aug 08 16:38:28 2013 +0200 @@ -9,6 +9,7 @@ signature BNF_FP_UTIL = sig datatype fp_kind = Least_FP | Greatest_FP + val fp_case: fp_kind -> 'a -> 'a -> 'a type fp_result = {Ts: typ list, @@ -54,11 +55,13 @@ val ctor_inductN: string val ctor_injectN: string val ctor_foldN: string + val ctor_fold_o_mapN: string + val ctor_fold_transferN: string val ctor_fold_uniqueN: string - val ctor_fold_transferN: string val ctor_mapN: string val ctor_map_uniqueN: string val ctor_recN: string + val ctor_rec_o_mapN: string val ctor_rec_uniqueN: string val ctor_relN: string val ctor_set_inclN: string @@ -70,6 +73,7 @@ val dtorN: string val dtor_coinductN: string val dtor_corecN: string + val dtor_corec_o_mapN: string val dtor_corec_uniqueN: string val dtor_ctorN: string val dtor_exhaustN: string @@ -83,8 +87,9 @@ val dtor_set_set_inclN: string val dtor_strong_coinductN: string val dtor_unfoldN: string + val dtor_unfold_o_mapN: string + val dtor_unfold_transferN: string val dtor_unfold_uniqueN: string - val dtor_unfold_transferN: string val exhaustN: string val foldN: string val hsetN: string @@ -175,6 +180,8 @@ 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 mk_xtor_un_fold_o_map_thms: fp_kind -> bool -> int -> thm -> thm list -> thm list -> + thm list -> thm list -> thm list val fp_bnf: (binding list -> (string * sort) list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory -> 'a) -> @@ -190,6 +197,8 @@ open BNF_Util datatype fp_kind = Least_FP | Greatest_FP; +fun fp_case Least_FP f1 _ = f1 + | fp_case Greatest_FP _ f2 = f2; type fp_result = {Ts: typ list, @@ -256,7 +265,9 @@ val ctor_foldN = ctorN ^ "_" ^ foldN val dtor_unfoldN = dtorN ^ "_" ^ unfoldN val ctor_fold_uniqueN = ctor_foldN ^ uniqueN +val ctor_fold_o_mapN = ctor_foldN ^ "_o_" ^ mapN val dtor_unfold_uniqueN = dtor_unfoldN ^ uniqueN +val dtor_unfold_o_mapN = dtor_unfoldN ^ "_o_" ^ mapN val ctor_fold_transferN = ctor_foldN ^ transferN val dtor_unfold_transferN = dtor_unfoldN ^ transferN val ctor_dtor_unfoldN = ctorN ^ "_" ^ dtor_unfoldN @@ -287,8 +298,10 @@ val recN = "rec" val corecN = coN ^ recN val ctor_recN = ctorN ^ "_" ^ recN +val ctor_rec_o_mapN = ctor_recN ^ "_o_" ^ mapN val ctor_rec_uniqueN = ctor_recN ^ uniqueN val dtor_corecN = dtorN ^ "_" ^ corecN +val dtor_corec_o_mapN = dtor_corecN ^ "_o_" ^ mapN val dtor_corec_uniqueN = dtor_corecN ^ uniqueN val ctor_dtor_corecN = ctorN ^ "_" ^ dtor_corecN @@ -516,6 +529,37 @@ |> split_conj_thm end; +fun mk_xtor_un_fold_o_map_thms fp is_rec m un_fold_unique xtor_maps xtor_un_folds sym_map_comps + map_cong0s = + let + val n = length sym_map_comps; + val rewrite_comp_comp2 = fp_case fp @{thm rewriteR_comp_comp2} @{thm rewriteL_comp_comp2}; + val rewrite_comp_comp = fp_case fp @{thm rewriteR_comp_comp} @{thm rewriteL_comp_comp}; + val map_cong_passive_args1 = replicate m (fp_case fp @{thm id_o} @{thm o_id} RS fun_cong); + val map_cong_active_args1 = replicate n (if is_rec + then fp_case fp @{thm convol_o} @{thm o_sum_case} RS fun_cong + else refl); + val map_cong_passive_args2 = replicate m (fp_case fp @{thm o_id} @{thm id_o} RS fun_cong); + val map_cong_active_args2 = replicate n (if is_rec + then fp_case fp @{thm map_pair_o_convol_id} @{thm sum_case_o_sum_map_id} + else fp_case fp @{thm id_o} @{thm o_id} RS fun_cong); + fun mk_map_congs passive active = map (fn thm => thm OF (passive @ active) RS ext) map_cong0s; + val map_cong1s = mk_map_congs map_cong_passive_args1 map_cong_active_args1; + val map_cong2s = mk_map_congs map_cong_passive_args2 map_cong_active_args2; + + fun mk_rewrites map_congs = map2 (fn sym_map_comp => fn map_cong => + mk_trans sym_map_comp map_cong RS rewrite_comp_comp) sym_map_comps map_congs; + val rewrite1s = mk_rewrites map_cong1s; + val rewrite2s = mk_rewrites map_cong2s; + val unique_prems = + map4 (fn xtor_map => fn un_fold => fn rewrite1 => fn rewrite2 => + mk_trans (rewrite_comp_comp2 OF [xtor_map, un_fold]) + (mk_trans rewrite1 (mk_sym rewrite2))) + xtor_maps xtor_un_folds rewrite1s rewrite2s; + in + split_conj_thm (un_fold_unique OF map (fp_case fp I mk_sym) unique_prems) + end; + fun fp_bnf construct_fp bs resBs eqs lthy = let val timer = time (Timer.startRealTimer ()); diff -r bdd610910e2c -r 2d2d9d1de1a9 src/HOL/BNF/Tools/bnf_gfp.ML --- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 08 15:30:25 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 08 16:38:28 2013 +0200 @@ -2003,8 +2003,8 @@ |> Thm.close_derivation end; - val dtor_corec_unique_thms = - split_conj_thm (split_conj_prems n + val (dtor_corec_unique_thms, dtor_corec_unique_thm) = + `split_conj_thm (split_conj_prems n (mor_UNIV_thm RS iffD2 RS corec_unique_mor_thm) |> Local_Defs.unfold lthy (@{thms o_sum_case o_id id_o o_assoc sum_case_o_inj(1)} @ map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ sum_case, OF refl]}); @@ -2131,10 +2131,11 @@ val in_rels = map in_rel_of_bnf bnfs; (*register new codatatypes as BNFs*) - val (timer, Jbnfs, folded_dtor_map_thms, folded_dtor_set_thmss', dtor_set_induct_thms, - dtor_Jrel_thms, lthy) = + val (timer, Jbnfs, (folded_dtor_map_o_thms, folded_dtor_map_thms), folded_dtor_set_thmss', + dtor_set_induct_thms, dtor_Jrel_thms, lthy) = if m = 0 then - (timer, replicate n DEADID_bnf, map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_id's, + (timer, replicate n DEADID_bnf, + map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_id's), replicate n [], [], map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs, lthy) else let val fTs = map2 (curry op -->) passiveAs passiveBs; @@ -2725,6 +2726,7 @@ val in_Jrels = map in_rel_of_bnf Jbnfs; val folded_dtor_map_thms = map fold_maps dtor_map_thms; + val folded_dtor_map_o_thms = map fold_maps map_thms; val folded_dtor_set_thmss = map (map fold_sets) dtor_set_thmss; val folded_dtor_set_thmss' = transpose folded_dtor_set_thmss; @@ -2767,10 +2769,18 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss) in - (timer, Jbnfs, folded_dtor_map_thms, folded_dtor_set_thmss', dtor_set_induct_thms, - dtor_Jrel_thms, lthy |> Local_Theory.notes (Jbnf_common_notes @ Jbnf_notes) |> snd) + (timer, Jbnfs, (folded_dtor_map_o_thms, folded_dtor_map_thms), folded_dtor_set_thmss', + dtor_set_induct_thms, dtor_Jrel_thms, + lthy |> Local_Theory.notes (Jbnf_common_notes @ Jbnf_notes) |> snd) end; + val dtor_unfold_o_map_thms = mk_xtor_un_fold_o_map_thms Greatest_FP false m + dtor_unfold_unique_thm folded_dtor_map_o_thms (map (mk_pointfree lthy) dtor_unfold_thms) + sym_map_comps map_cong0s; + val dtor_corec_o_map_thms = mk_xtor_un_fold_o_map_thms Greatest_FP true m + dtor_corec_unique_thm folded_dtor_map_o_thms (map (mk_pointfree lthy) dtor_corec_thms) + sym_map_comps map_cong0s; + val passiveABs = map2 (curry HOLogic.mk_prodT) passiveAs passiveBs; val zip_ranTs = passiveABs @ prodTsTs'; val allJphis = Jphis @ activeJphis; @@ -2906,7 +2916,9 @@ (dtor_injectN, dtor_inject_thms), (dtor_unfoldN, dtor_unfold_thms), (dtor_unfold_uniqueN, dtor_unfold_unique_thms), - (dtor_corec_uniqueN, dtor_corec_unique_thms)] + (dtor_corec_uniqueN, dtor_corec_unique_thms), + (dtor_unfold_o_mapN, dtor_unfold_o_map_thms), + (dtor_corec_o_mapN, dtor_corec_o_map_thms)] |> map (apsnd (map single)) |> maps (fn (thmN, thmss) => map2 (fn b => fn thms => diff -r bdd610910e2c -r 2d2d9d1de1a9 src/HOL/BNF/Tools/bnf_lfp.ML --- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 08 15:30:25 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 08 16:38:28 2013 +0200 @@ -1294,8 +1294,8 @@ |> Thm.close_derivation end; - val ctor_rec_unique_thms = - split_conj_thm (split_conj_prems n + val (ctor_rec_unique_thms, ctor_rec_unique_thm) = + `split_conj_thm (split_conj_prems n (mor_UNIV_thm RS iffD2 RS rec_unique_mor_thm) |> Local_Defs.unfold lthy (@{thms convol_o o_id id_o o_assoc[symmetric] fst_convol} @ map_ids @ sym_map_comps) OF replicate n @{thm arg_cong2[of _ _ _ _ convol, OF refl]}); @@ -1396,9 +1396,11 @@ val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs; (*register new datatypes as BNFs*) - val (timer, Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms, lthy) = + val (timer, Ibnfs, (folded_ctor_map_o_thms, folded_ctor_map_thms), folded_ctor_set_thmss', + ctor_Irel_thms, lthy) = if m = 0 then - (timer, replicate n DEADID_bnf, map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_id's, + (timer, replicate n DEADID_bnf, + map_split (`(mk_pointfree lthy)) (map2 mk_ctor_map_DEADID_thm ctor_inject_thms map_id's), replicate n [], map2 mk_ctor_Irel_DEADID_thm ctor_inject_thms bnfs, lthy) else let val fTs = map2 (curry op -->) passiveAs passiveBs; @@ -1446,7 +1448,7 @@ val p1s_maps = map (mk_map XTs p1s Ts ctors (mk_passive_maps passiveXs passiveAs)) ks; val p2s_maps = map (mk_map XTs p2s Ts' ctor's (mk_passive_maps passiveXs passiveBs)) ks; - val ctor_map_thms = + val (ctor_map_thms, ctor_map_o_thms) = let fun mk_goal fs_map map ctor ctor' = fold_rev Logic.all fs (mk_Trueprop_eq (HOLogic.mk_comp (fs_map, ctor), @@ -1458,7 +1460,7 @@ |> Thm.close_derivation) goals ctor_fold_thms map_comp_id_thms map_cong0s; in - map (fn thm => thm RS @{thm comp_eq_dest}) maps + `(map (fn thm => thm RS @{thm comp_eq_dest})) maps end; val (ctor_map_unique_thms, ctor_map_unique_thm) = @@ -1756,6 +1758,7 @@ val ctor_set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss; val ctor_set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss; val folded_ctor_map_thms = map fold_maps ctor_map_thms; + val folded_ctor_map_o_thms = map fold_maps ctor_map_o_thms; val folded_ctor_set_thmss = map (map fold_sets) ctor_set_thmss; val folded_ctor_set_thmss' = transpose folded_ctor_set_thmss; @@ -1797,10 +1800,15 @@ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])])) bs thmss) in - (timer, Ibnfs, folded_ctor_map_thms, folded_ctor_set_thmss', ctor_Irel_thms, - lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd) + (timer, Ibnfs, (folded_ctor_map_o_thms, folded_ctor_map_thms), folded_ctor_set_thmss', + ctor_Irel_thms, lthy |> Local_Theory.notes (Ibnf_common_notes @ Ibnf_notes) |> snd) end; + val ctor_fold_o_map_thms = mk_xtor_un_fold_o_map_thms Least_FP false m ctor_fold_unique_thm + folded_ctor_map_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s; + val ctor_rec_o_map_thms = mk_xtor_un_fold_o_map_thms Least_FP true m ctor_rec_unique_thm + folded_ctor_map_o_thms (map (mk_pointfree lthy) ctor_rec_thms) sym_map_comps map_cong0s; + val Irels = if m = 0 then map HOLogic.eq_const Ts else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs; val Irel_induct_thm = @@ -1831,6 +1839,8 @@ (ctor_foldN, ctor_fold_thms), (ctor_fold_uniqueN, ctor_fold_unique_thms), (ctor_rec_uniqueN, ctor_rec_unique_thms), + (ctor_fold_o_mapN, ctor_fold_o_map_thms), + (ctor_rec_o_mapN, ctor_rec_o_map_thms), (ctor_injectN, ctor_inject_thms), (ctor_recN, ctor_rec_thms), (dtor_ctorN, dtor_ctor_thms), diff -r bdd610910e2c -r 2d2d9d1de1a9 src/HOL/BNF/Tools/bnf_tactics.ML --- a/src/HOL/BNF/Tools/bnf_tactics.ML Thu Aug 08 15:30:25 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_tactics.ML Thu Aug 08 16:38:28 2013 +0200 @@ -19,6 +19,8 @@ val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list -> int -> tactic + val mk_pointfree: Proof.context -> thm -> thm + val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm val mk_Abs_inj_thm: thm -> thm @@ -53,6 +55,16 @@ fun mk_unfold_thms_then_tac lthy defs tac x = unfold_thms_tac lthy defs THEN tac x; +(*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*) +fun mk_pointfree ctxt thm = thm + |> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq + |> pairself (dest_comb #> apsnd (dest_comb #> fst) #> HOLogic.mk_comp) + |> mk_Trueprop_eq + |> (fn goal => Goal.prove_sorry ctxt [] [] goal + (fn {context=ctxt, prems = _} => + unfold_thms_tac ctxt [@{thm o_def}, mk_sym thm] THEN rtac refl 1)) + |> Thm.close_derivation; + (* Theorems for open typedefs with UNIV as representing set *) diff -r bdd610910e2c -r 2d2d9d1de1a9 src/HOL/BNF/Tools/bnf_util.ML --- a/src/HOL/BNF/Tools/bnf_util.ML Thu Aug 08 15:30:25 2013 +0200 +++ b/src/HOL/BNF/Tools/bnf_util.ML Thu Aug 08 16:38:28 2013 +0200 @@ -604,7 +604,7 @@ (map_index (fn (i, y) => if member (op =) xs y then SOME i else NONE) ys); fun mk_trans thm1 thm2 = trans OF [thm1, thm2]; -fun mk_sym thm = sym OF [thm]; +fun mk_sym thm = thm RS sym; (*TODO: antiquote heavily used theorems once*) val Pair_eqD = @{thm iffD1[OF Pair_eq]};