--- a/src/HOL/BNF_Least_Fixpoint.thy Mon Sep 01 14:14:47 2014 +0200
+++ b/src/HOL/BNF_Least_Fixpoint.thy Thu Sep 25 16:35:50 2014 +0200
@@ -178,6 +178,29 @@
lemma id_transfer: "rel_fun A A id id"
unfolding rel_fun_def by simp
+lemma fst_transfer: "rel_fun (rel_prod A B) A fst fst"
+ unfolding rel_fun_def rel_prod_def by simp
+
+lemma snd_transfer: "rel_fun (rel_prod A B) B snd snd"
+ unfolding rel_fun_def rel_prod_def by simp
+
+lemma case_sum_transfer:
+ "rel_fun (rel_fun R T) (rel_fun (rel_fun S T) (rel_fun (rel_sum R S) T)) case_sum case_sum"
+ unfolding rel_fun_def rel_sum_def by (auto split: sum.splits)
+
+lemma map_sum_transfer:
+ "rel_fun (rel_fun R T) (rel_fun (rel_fun S U) (rel_fun (rel_sum R S) (rel_sum T U))) map_sum map_sum"
+ unfolding rel_fun_def rel_sum_def by (auto split: sum.splits)
+
+lemma convol_transfer:
+ "rel_fun (rel_fun R S) (rel_fun (rel_fun R T) (rel_fun R (rel_prod S T))) BNF_Def.convol BNF_Def.convol"
+ unfolding rel_prod_def rel_fun_def convol_def by auto
+
+lemma comp_transfer:
+ "rel_fun (rel_fun B C) (rel_fun (rel_fun A B) (rel_fun A C)) (op \<circ>) (op \<circ>)"
+ unfolding rel_fun_def by simp
+
+
lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
by (rule ssubst)
--- a/src/HOL/Lifting_Product.thy Mon Sep 01 14:14:47 2014 +0200
+++ b/src/HOL/Lifting_Product.thy Thu Sep 25 16:35:50 2014 +0200
@@ -22,11 +22,8 @@
lemma Pair_transfer [transfer_rule]: "(A ===> B ===> rel_prod A B) Pair Pair"
unfolding rel_fun_def rel_prod_def by simp
-lemma fst_transfer [transfer_rule]: "(rel_prod A B ===> A) fst fst"
- unfolding rel_fun_def rel_prod_def by simp
-
-lemma snd_transfer [transfer_rule]: "(rel_prod A B ===> B) snd snd"
- unfolding rel_fun_def rel_prod_def by simp
+declare fst_transfer [transfer_rule]
+declare snd_transfer [transfer_rule]
lemma case_prod_transfer [transfer_rule]:
"((A ===> B ===> C) ===> rel_prod A B ===> C) case_prod case_prod"
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Mon Sep 01 14:14:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Thu Sep 25 16:35:50 2014 +0200
@@ -62,6 +62,7 @@
val ctor_map_uniqueN: string
val ctor_recN: string
val ctor_rec_o_mapN: string
+ val ctor_rec_transferN: string
val ctor_rec_uniqueN: string
val ctor_relN: string
val ctor_rel_inductN: string
@@ -294,6 +295,7 @@
val corecN = coN ^ recN
val ctor_recN = ctorN ^ "_" ^ recN
val ctor_rec_o_mapN = ctor_recN ^ "_o_" ^ mapN
+val ctor_rec_transferN = ctor_recN ^ transferN
val ctor_rec_uniqueN = ctor_recN ^ uniqueN
val dtor_corecN = dtorN ^ "_" ^ corecN
val dtor_corec_o_mapN = dtor_corecN ^ "_o_" ^ mapN
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Mon Sep 01 14:14:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Sep 25 16:35:50 2014 +0200
@@ -1786,7 +1786,8 @@
val ctor_rec_transfer_thms =
mk_co_iter_transfer_thms Least_FP rec_rels rec_activephis activephis Irels Iphis
(mk_recs Ts passiveAs activeAs) (mk_recs Ts' passiveBs activeBs)
- (fn {context = ctxt, prems = _} => print_tac ctxt "xxx" THEN Skip_Proof.cheat_tac 1)
+ (fn {context = ctxt, prems = _} => mk_ctor_rec_transfer_tac ctxt n m rec_defs
+ ctor_fold_transfer_thms (map map_transfer_of_bnf bnfs) ctor_Irel_thms)
lthy;
val timer = time (timer "relator induction");
@@ -1795,6 +1796,7 @@
[(ctor_inductN, [ctor_induct_thm]),
(ctor_induct2N, [ctor_induct2_thm]),
(ctor_fold_transferN, ctor_fold_transfer_thms),
+ (ctor_rec_transferN, ctor_rec_transfer_thms),
(ctor_rel_inductN, [Irel_induct_thm])]
|> map (fn (thmN, thms) =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Mon Sep 01 14:14:47 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Thu Sep 25 16:35:50 2014 +0200
@@ -22,6 +22,8 @@
val mk_ctor_induct2_tac: Proof.context -> ctyp option list -> cterm option list -> thm ->
thm list -> tactic
val mk_ctor_set_tac: thm -> thm -> thm list -> tactic
+ val mk_ctor_rec_transfer_tac: Proof.context -> int -> int -> thm list -> thm list -> thm list ->
+ thm list -> tactic
val mk_ctor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
thm -> thm -> thm list -> thm list -> thm list list -> tactic
val mk_dtor_o_ctor_tac: thm -> thm -> thm -> thm -> thm list -> tactic
@@ -701,6 +703,29 @@
EVERY' [rtac iffI, if_tac, only_if_tac] 1
end;
+fun mk_ctor_rec_transfer_tac ctxt n m ctor_rec_defs ctor_fold_transfers pre_T_map_transfers
+ ctor_rels =
+ let
+ val rel_funD = @{thm rel_funD};
+ fun rel_funD_n n = funpow n (fn thm => thm RS rel_funD);
+ val rel_funD_n_rotated = rotate_prems ~1 oo rel_funD_n;
+ in
+ CONJ_WRAP (fn (ctor_rec_def, ctor_fold_transfer) =>
+ REPEAT_DETERM (HEADGOAL (rtac @{thm rel_funI})) THEN
+ unfold_thms_tac ctxt [ctor_rec_def, o_apply] THEN
+ HEADGOAL (rtac @{thm rel_funD[OF snd_transfer]} THEN'
+ etac (rel_funD_n_rotated (n + 1) ctor_fold_transfer) THEN'
+ EVERY' (map2 (fn pre_T_map_transfer => fn ctor_rel =>
+ etac (rel_funD_n_rotated 2 @{thm convol_transfer}) THEN'
+ rtac (rel_funD_n_rotated 2 @{thm comp_transfer}) THEN'
+ rtac (rel_funD_n (m + n) pre_T_map_transfer) THEN'
+ REPEAT_DETERM_N m o rtac @{thm id_transfer} THEN'
+ REPEAT_DETERM o rtac @{thm fst_transfer} THEN'
+ rtac @{thm rel_funI} THEN'
+ etac (ctor_rel RS iffD2)) pre_T_map_transfers ctor_rels)))
+ (ctor_rec_defs ~~ ctor_fold_transfers)
+ end;
+
fun mk_rel_induct_tac ctxt IHs m ctor_induct2 ks ctor_rels rel_mono_strong0s =
let val n = length ks;
in
--- a/src/HOL/Transfer.thy Mon Sep 01 14:14:47 2014 +0200
+++ b/src/HOL/Transfer.thy Thu Sep 25 16:35:50 2014 +0200
@@ -458,9 +458,7 @@
lemma id_transfer [transfer_rule]: "(A ===> A) id id"
unfolding rel_fun_def by simp
-lemma comp_transfer [transfer_rule]:
- "((B ===> C) ===> (A ===> B) ===> (A ===> C)) (op \<circ>) (op \<circ>)"
- unfolding rel_fun_def by simp
+declare comp_transfer [transfer_rule]
lemma fun_upd_transfer [transfer_rule]:
assumes [transfer_rule]: "bi_unique A"