--- a/src/HOL/BNF/BNF_FP_Basic.thy Thu Aug 08 16:10:05 2013 +0200
+++ b/src/HOL/BNF/BNF_FP_Basic.thy Thu Aug 08 16:38:50 2013 +0200
@@ -113,6 +113,36 @@
lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
by blast
+lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r"
+ unfolding o_def fun_eq_iff by auto
+
+lemma rewriteR_comp_comp2: "\<lbrakk>g o h = r1 o r2; f o r1 = l\<rbrakk> \<Longrightarrow> f o g o h = l o r2"
+ unfolding o_def fun_eq_iff by auto
+
+lemma rewriteL_comp_comp: "\<lbrakk>f o g = l\<rbrakk> \<Longrightarrow> f o (g o h) = l o h"
+ unfolding o_def fun_eq_iff by auto
+
+lemma rewriteL_comp_comp2: "\<lbrakk>f o g = l1 o l2; l2 o h = r\<rbrakk> \<Longrightarrow> f o (g o h) = l1 o r"
+ unfolding o_def fun_eq_iff by auto
+
+lemma convol_o: "<f, g> o h = <f o h, g o h>"
+ unfolding convol_def by auto
+
+lemma map_pair_o_convol: "map_pair h1 h2 o <f, g> = <h1 o f, h2 o g>"
+ unfolding convol_def by auto
+
+lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> 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 = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
unfolding fun_rel_def ..
--- a/src/HOL/BNF/BNF_GFP.thy Thu Aug 08 16:10:05 2013 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy Thu Aug 08 16:38:50 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 \<Longrightarrow> f x = sum_case g (f o Inr) x"
by (auto split: sum.splits)
--- a/src/HOL/BNF/BNF_LFP.thy Thu Aug 08 16:10:05 2013 +0200
+++ b/src/HOL/BNF/BNF_LFP.thy Thu Aug 08 16:38:50 2013 +0200
@@ -44,9 +44,6 @@
lemma snd_convol': "snd (<f, g> x) = g x"
using snd_convol unfolding convol_def by simp
-lemma convol_o: "<f, g> o h = <f o h, g o h>"
- unfolding convol_def by auto
-
lemma convol_expand_snd: "fst o f = g \<Longrightarrow> <g, snd o f> = f"
unfolding convol_def by auto
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Aug 08 16:10:05 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Thu Aug 08 16:38:50 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 ());
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 08 16:10:05 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 08 16:38:50 2013 +0200
@@ -210,7 +210,7 @@
val bd_Cinfinite = hd bd_Cinfinites;
val in_monos = map in_mono_of_bnf bnfs;
val map_comps = map map_comp_of_bnf bnfs;
- val sym_map_comps = map (fn thm => thm RS sym) map_comps;
+ val sym_map_comps = map mk_sym map_comps;
val map_comp's = map map_comp'_of_bnf bnfs;
val map_cong0s = map map_cong0_of_bnf bnfs;
val map_ids = map map_id_of_bnf bnfs;
@@ -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;
@@ -2254,7 +2255,7 @@
in
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
- (mk_dtor_map_unique_tac dtor_unfold_unique_thm map_comps)
+ (mk_dtor_map_unique_tac dtor_unfold_unique_thm sym_map_comps)
|> Thm.close_derivation
end;
@@ -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 =>
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 08 16:10:05 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 08 16:38:50 2013 +0200
@@ -1061,7 +1061,7 @@
EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1;
fun mk_map_id_tac maps unfold_unique unfold_dtor =
- EVERY' [rtac (unfold_unique RS trans), EVERY' (map (fn thm => rtac (thm RS sym)) maps),
+ EVERY' [rtac (unfold_unique RS trans), EVERY' (map (rtac o mk_sym) maps),
rtac unfold_dtor] 1;
fun mk_map_comp_tac m n maps map_comps map_cong0s unfold_unique =
@@ -1114,9 +1114,9 @@
rtac conjI, rtac refl, rtac refl]) ks]) 1
end
-fun mk_dtor_map_unique_tac unfold_unique map_comps {context = ctxt, prems = _} =
+fun mk_dtor_map_unique_tac unfold_unique sym_map_comps {context = ctxt, prems = _} =
rtac unfold_unique 1 THEN
- unfold_thms_tac ctxt (map (fn thm => thm RS sym) map_comps @ @{thms o_assoc id_o o_id}) THEN
+ unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc id_o o_id}) THEN
ALLGOALS (etac sym);
fun mk_col_natural_tac cts rec_0s rec_Sucs dtor_maps set_mapss
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 08 16:10:05 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Thu Aug 08 16:38:50 2013 +0200
@@ -1133,8 +1133,8 @@
`split_conj_thm unique_mor
end;
- val ctor_fold_unique_thms =
- split_conj_thm (mk_conjIN n RS
+ val (ctor_fold_unique_thms, ctor_fold_unique_thm) =
+ `split_conj_thm (mk_conjIN n RS
(mor_UNIV_thm RS iffD2 RS fold_unique_mor_thm))
val fold_ctor_thms =
@@ -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) =
@@ -1472,7 +1474,7 @@
(map2 (curry HOLogic.mk_eq) us fs_maps));
val unique = Goal.prove_sorry lthy [] []
(fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
- (K (mk_ctor_map_unique_tac m mor_def fold_unique_mor_thm map_comp_id_thms map_cong0s))
+ (mk_ctor_map_unique_tac ctor_fold_unique_thm sym_map_comps)
|> Thm.close_derivation;
in
`split_conj_thm unique
@@ -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),
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 08 16:10:05 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Thu Aug 08 16:38:50 2013 +0200
@@ -42,7 +42,7 @@
val mk_map_comp_tac: thm list -> thm list -> thm -> int -> tactic
val mk_map_id_tac: thm list -> thm -> tactic
val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic
- val mk_ctor_map_unique_tac: int -> thm -> thm -> thm list -> thm list -> tactic
+ val mk_ctor_map_unique_tac: thm -> thm list -> {prems: thm list, context: Proof.context} -> tactic
val mk_mcong_tac: (int -> tactic) -> thm list list list -> thm list -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
val mk_min_algs_card_of_tac: ctyp -> cterm -> int -> thm -> thm list -> thm list -> thm -> thm ->
@@ -584,19 +584,10 @@
REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])),
rtac sym, rtac o_apply] 1;
-fun mk_ctor_map_unique_tac m mor_def fold_unique_mor map_comp_ids map_cong0s =
- let
- val n = length map_cong0s;
- fun mk_mor (comp_id, cong) = EVERY' [rtac ballI, rtac trans, etac @{thm comp_eq_dest},
- rtac sym, rtac trans, rtac o_apply, rtac trans, rtac (comp_id RS arg_cong),
- rtac (cong RS arg_cong),
- REPEAT_DETERM_N m o rtac refl,
- REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply]))];
- in
- EVERY' [rtac fold_unique_mor, rtac ssubst, rtac mor_def, rtac conjI,
- CONJ_WRAP' (K (EVERY' [rtac ballI, rtac UNIV_I])) map_cong0s,
- CONJ_WRAP' mk_mor (map_comp_ids ~~ map_cong0s)] 1
- end;
+fun mk_ctor_map_unique_tac fold_unique sym_map_comps {context = ctxt, prems = _} =
+ rtac fold_unique 1 THEN
+ unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc[symmetric] id_o o_id}) THEN
+ ALLGOALS atac;
fun mk_set_tac foldx = EVERY' [rtac ext, rtac trans, rtac o_apply,
rtac trans, rtac foldx, rtac sym, rtac o_apply] 1;
--- a/src/HOL/BNF/Tools/bnf_tactics.ML Thu Aug 08 16:10:05 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML Thu Aug 08 16:38:50 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 *)
--- a/src/HOL/BNF/Tools/bnf_util.ML Thu Aug 08 16:10:05 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_util.ML Thu Aug 08 16:38:50 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]};