--- a/src/HOL/BNF_Def.thy Wed Feb 17 11:39:26 2016 +0100
+++ b/src/HOL/BNF_Def.thy Wed Feb 17 15:18:06 2016 +0100
@@ -265,6 +265,10 @@
lemma Ball_image_comp: "Ball (f ` A) g = Ball A (g o f)"
by auto
+lemma rel_fun_Collect_case_prodD:
+ "rel_fun A B f g \<Longrightarrow> X \<subseteq> Collect (case_prod A) \<Longrightarrow> x \<in> X \<Longrightarrow> B ((f o fst) x) ((g o snd) x)"
+ unfolding rel_fun_def by auto
+
ML_file "Tools/BNF/bnf_util.ML"
ML_file "Tools/BNF/bnf_tactics.ML"
ML_file "Tools/BNF/bnf_def_tactics.ML"
--- a/src/HOL/Tools/BNF/bnf_def.ML Wed Feb 17 11:39:26 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML Wed Feb 17 15:18:06 2016 +0100
@@ -85,6 +85,8 @@
val pred_mono_strong_of_bnf: bnf -> thm
val pred_set_of_bnf: bnf -> thm
val pred_rel_of_bnf: bnf -> thm
+ val pred_transfer_of_bnf: bnf -> thm
+ val pred_True_of_bnf: bnf -> thm
val rel_Grp_of_bnf: bnf -> thm
val rel_OO_Grp_of_bnf: bnf -> thm
val rel_OO_of_bnf: bnf -> thm
@@ -290,6 +292,7 @@
rel_transp: thm lazy,
rel_transfer: thm lazy,
rel_eq_onp: thm lazy,
+ pred_transfer: thm lazy,
pred_True: thm lazy,
pred_map: thm lazy,
pred_rel: thm lazy,
@@ -304,8 +307,8 @@
inj_map inj_map_strong map_comp map_cong map_cong_simp map_cong_pred map_id map_ident0 map_ident
map_transfer rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp rel_map rel_mono
rel_mono_strong0 rel_mono_strong set_transfer rel_Grp rel_conversep rel_OO rel_refl
- rel_refl_strong rel_reflp rel_symp rel_transp rel_transfer rel_eq_onp pred_True pred_map pred_rel
- pred_mono_strong0 pred_mono_strong pred_cong0 pred_cong pred_cong_simp = {
+ rel_refl_strong rel_reflp rel_symp rel_transp rel_transfer rel_eq_onp pred_transfer pred_True
+ pred_map pred_rel pred_mono_strong0 pred_mono_strong pred_cong0 pred_cong pred_cong_simp = {
bd_Card_order = bd_Card_order,
bd_Cinfinite = bd_Cinfinite,
bd_Cnotzero = bd_Cnotzero,
@@ -345,6 +348,7 @@
rel_transp = rel_transp,
set_transfer = set_transfer,
rel_eq_onp = rel_eq_onp,
+ pred_transfer = pred_transfer,
pred_True = pred_True,
pred_map = pred_map,
pred_rel = pred_rel,
@@ -394,6 +398,7 @@
rel_transp,
set_transfer,
rel_eq_onp,
+ pred_transfer,
pred_True,
pred_map,
pred_rel,
@@ -441,6 +446,7 @@
rel_transp = Lazy.map f rel_transp,
set_transfer = Lazy.map (map f) set_transfer,
rel_eq_onp = Lazy.map f rel_eq_onp,
+ pred_transfer = Lazy.map f pred_transfer,
pred_True = Lazy.map f pred_True,
pred_map = Lazy.map f pred_map,
pred_rel = Lazy.map f pred_rel,
@@ -577,15 +583,17 @@
val map_ident_of_bnf = Lazy.force o #map_ident o #facts o rep_bnf;
val map_transfer_of_bnf = Lazy.force o #map_transfer o #facts o rep_bnf;
val rel_eq_onp_of_bnf = Lazy.force o #rel_eq_onp o #facts o rep_bnf;
-val pred_rel_of_bnf = Lazy.force o #pred_rel o #facts o rep_bnf;
+val pred_def_of_bnf = #pred_def o #defs o rep_bnf;
val pred_map_of_bnf = Lazy.force o #pred_map o #facts o rep_bnf;
val pred_mono_strong0_of_bnf = Lazy.force o #pred_mono_strong0 o #facts o rep_bnf;
val pred_mono_strong_of_bnf = Lazy.force o #pred_mono_strong o #facts o rep_bnf;
val pred_cong0_of_bnf = Lazy.force o #pred_cong0 o #facts o rep_bnf;
val pred_cong_of_bnf = Lazy.force o #pred_cong o #facts o rep_bnf;
val pred_cong_simp_of_bnf = Lazy.force o #pred_cong_simp o #facts o rep_bnf;
-val pred_def_of_bnf = #pred_def o #defs o rep_bnf;
+val pred_rel_of_bnf = Lazy.force o #pred_rel o #facts o rep_bnf;
val pred_set_of_bnf = #pred_set o #axioms o rep_bnf;
+val pred_transfer_of_bnf = Lazy.force o #pred_transfer o #facts o rep_bnf;
+val pred_True_of_bnf = Lazy.force o #pred_True o #facts o rep_bnf;
val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
val rel_OO_Grp_of_bnf = #rel_OO_Grp o #axioms o rep_bnf;
val rel_OO_of_bnf = Lazy.force o #rel_OO o #facts o rep_bnf;
@@ -794,6 +802,7 @@
val map_transferN = "map_transfer";
val pred_mono_strong0N = "pred_mono_strong0";
val pred_mono_strongN = "pred_mono_strong";
+val pred_transferN = "pred_transfer";
val pred_TrueN = "pred_True";
val pred_mapN = "pred_map";
val pred_relN = "pred_rel";
@@ -889,6 +898,7 @@
(pred_cong_simpN, [Lazy.force (#pred_cong_simp facts)], []),
(pred_mapN, [Lazy.force (#pred_map facts)], []),
(pred_relN, [Lazy.force (#pred_rel facts)], []),
+ (pred_transferN, [Lazy.force (#pred_transfer facts)], []),
(pred_TrueN, [Lazy.force (#pred_True facts)], []),
(pred_setN, [#pred_set axioms], []),
(rel_comppN, [Lazy.force (#rel_OO facts)], []),
@@ -1837,6 +1847,23 @@
val map_transfer = Lazy.lazy mk_map_transfer;
+ fun mk_pred_transfer () =
+ let
+ val iff = HOLogic.eq_const HOLogic.boolT;
+ val prem_rels = map (fn T => mk_rel_fun T iff) Rs;
+ val prem_elems = mk_rel_fun (Term.list_comb (rel, Rs)) iff;
+ val goal = HOLogic.mk_Trueprop
+ (fold_rev mk_rel_fun prem_rels prem_elems $ pred $ pred');
+ val vars = Variable.add_free_names lthy goal [];
+ in
+ Goal.prove_sorry lthy vars [] goal (fn {context = ctxt, prems = _} =>
+ mk_pred_transfer_tac ctxt live (Lazy.force in_rel) (Lazy.force pred_map)
+ (Lazy.force pred_cong))
+ |> Thm.close_derivation
+ end;
+
+ val pred_transfer = Lazy.lazy mk_pred_transfer;
+
fun mk_rel_transfer () =
let
val iff = HOLogic.eq_const HOLogic.boolT;
@@ -1912,8 +1939,8 @@
map_ident0 map_ident map_transfer rel_eq rel_flip set_map rel_cong0 rel_cong rel_cong_simp
rel_map rel_mono rel_mono_strong0 rel_mono_strong set_transfer rel_Grp rel_conversep
rel_OO rel_refl rel_refl_strong rel_reflp rel_symp rel_transp rel_transfer rel_eq_onp
- pred_True pred_map pred_rel pred_mono_strong0 pred_mono_strong pred_cong0 pred_cong
- pred_cong_simp;
+ pred_transfer pred_True pred_map pred_rel pred_mono_strong0 pred_mono_strong pred_cong0
+ pred_cong pred_cong_simp;
val wits = map2 mk_witness bnf_wits wit_thms;
--- a/src/HOL/Tools/BNF/bnf_def_tactics.ML Wed Feb 17 11:39:26 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_def_tactics.ML Wed Feb 17 15:18:06 2016 +0100
@@ -19,7 +19,6 @@
val mk_map_comp: thm -> thm
val mk_map_cong_tac: Proof.context -> thm -> tactic
val mk_set_map: thm -> thm
- val mk_set_transfer_tac: Proof.context -> thm -> thm list -> tactic
val mk_rel_Grp_tac: Proof.context -> thm list -> thm -> thm -> thm -> thm -> thm list -> tactic
val mk_rel_eq_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
@@ -30,11 +29,13 @@
val mk_rel_mono_tac: Proof.context -> thm list -> thm -> tactic
val mk_rel_mono_strong0_tac: Proof.context -> thm -> thm list -> tactic
val mk_rel_cong_tac: Proof.context -> thm list * thm list -> thm -> tactic
- val mk_rel_transfer_tac: Proof.context -> thm -> thm list -> thm -> tactic
val mk_rel_eq_onp_tac: Proof.context -> thm -> thm -> thm -> tactic
val mk_pred_mono_strong0_tac: Proof.context -> thm -> thm -> tactic
val mk_map_transfer_tac: Proof.context -> thm -> thm -> thm list -> thm -> thm -> tactic
+ val mk_pred_transfer_tac: Proof.context -> int -> thm -> thm -> thm -> tactic
+ val mk_rel_transfer_tac: Proof.context -> thm -> thm list -> thm -> tactic
+ val mk_set_transfer_tac: Proof.context -> thm -> thm list -> tactic
val mk_in_bd_tac: Proof.context -> int -> thm -> thm -> thm -> thm -> thm list -> thm list ->
thm -> thm -> thm -> thm -> tactic
@@ -388,4 +389,11 @@
unfold_thms_tac ctxt [pred_rel] THEN
HEADGOAL (etac ctxt rel_mono_strong0 THEN_ALL_NEW etac ctxt @{thm eq_onp_mono0});
+fun mk_pred_transfer_tac ctxt n in_rel pred_map pred_cong =
+ HEADGOAL (EVERY' [REPEAT_DETERM_N (n + 1) o rtac ctxt rel_funI, dtac ctxt (in_rel RS iffD1),
+ REPEAT_DETERM o eresolve_tac ctxt [exE, conjE, CollectE], hyp_subst_tac ctxt,
+ rtac ctxt (box_equals OF [@{thm _}, pred_map RS sym, pred_map RS sym]),
+ rtac ctxt (refl RS pred_cong), REPEAT_DETERM_N n o
+ (etac ctxt @{thm rel_fun_Collect_case_prodD[where B="op ="]} THEN_ALL_NEW assume_tac ctxt)]);
+
end;
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Wed Feb 17 11:39:26 2016 +0100
+++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Wed Feb 17 15:18:06 2016 +0100
@@ -149,8 +149,8 @@
fun bnf_transfer_rules bnf =
let
- val transfer_rules = map_transfer_of_bnf bnf :: rel_transfer_of_bnf bnf
- :: set_transfer_of_bnf bnf
+ val transfer_rules = map_transfer_of_bnf bnf :: pred_transfer_of_bnf bnf
+ :: rel_transfer_of_bnf bnf :: set_transfer_of_bnf bnf
val transfer_attr = @{attributes [transfer_rule]}
in
map (fn thm => ((Binding.empty,[]),[([thm],transfer_attr)])) transfer_rules