--- a/src/HOL/Probability/Probability_Mass_Function.thy Fri Dec 12 14:31:57 2014 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy Fri Dec 12 14:42:37 2014 +0100
@@ -883,6 +883,52 @@
"measure_pmf M \<in> space (subprob_algebra (count_space UNIV))"
by (simp add: space_subprob_algebra) intro_locales
+lemma nn_integral_pair_pmf': "(\<integral>\<^sup>+x. f x \<partial>pair_pmf A B) = (\<integral>\<^sup>+a. \<integral>\<^sup>+b. f (a, b) \<partial>B \<partial>A)"
+proof -
+ have "(\<integral>\<^sup>+x. f x \<partial>pair_pmf A B) = (\<integral>\<^sup>+x. max 0 (f x) * indicator (A \<times> B) x \<partial>pair_pmf A B)"
+ by (subst nn_integral_max_0[symmetric])
+ (auto simp: AE_measure_pmf_iff set_pair_pmf intro!: nn_integral_cong_AE)
+ also have "\<dots> = (\<integral>\<^sup>+a. \<integral>\<^sup>+b. max 0 (f (a, b)) * indicator (A \<times> B) (a, b) \<partial>B \<partial>A)"
+ by (simp add: pair_pmf_def)
+ also have "\<dots> = (\<integral>\<^sup>+a. \<integral>\<^sup>+b. max 0 (f (a, b)) \<partial>B \<partial>A)"
+ by (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff)
+ finally show ?thesis
+ unfolding nn_integral_max_0 .
+qed
+
+lemma pair_map_pmf1: "pair_pmf (map_pmf f A) B = map_pmf (apfst f) (pair_pmf A B)"
+proof (safe intro!: pmf_eqI)
+ fix a :: "'a" and b :: "'b"
+ have [simp]: "\<And>c d. indicator (apfst f -` {(a, b)}) (c, d) = indicator (f -` {a}) c * (indicator {b} d::ereal)"
+ by (auto split: split_indicator)
+
+ have "ereal (pmf (pair_pmf (map_pmf f A) B) (a, b)) =
+ ereal (pmf (map_pmf (apfst f) (pair_pmf A B)) (a, b))"
+ unfolding pmf_pair ereal_pmf_map
+ by (simp add: nn_integral_pair_pmf' max_def emeasure_pmf_single nn_integral_multc pmf_nonneg
+ emeasure_map_pmf[symmetric] del: emeasure_map_pmf)
+ then show "pmf (pair_pmf (map_pmf f A) B) (a, b) = pmf (map_pmf (apfst f) (pair_pmf A B)) (a, b)"
+ by simp
+qed
+
+lemma pair_map_pmf2: "pair_pmf A (map_pmf f B) = map_pmf (apsnd f) (pair_pmf A B)"
+proof (safe intro!: pmf_eqI)
+ fix a :: "'a" and b :: "'b"
+ have [simp]: "\<And>c d. indicator (apsnd f -` {(a, b)}) (c, d) = indicator {a} c * (indicator (f -` {b}) d::ereal)"
+ by (auto split: split_indicator)
+
+ have "ereal (pmf (pair_pmf A (map_pmf f B)) (a, b)) =
+ ereal (pmf (map_pmf (apsnd f) (pair_pmf A B)) (a, b))"
+ unfolding pmf_pair ereal_pmf_map
+ by (simp add: nn_integral_pair_pmf' max_def emeasure_pmf_single nn_integral_cmult nn_integral_multc pmf_nonneg
+ emeasure_map_pmf[symmetric] del: emeasure_map_pmf)
+ then show "pmf (pair_pmf A (map_pmf f B)) (a, b) = pmf (map_pmf (apsnd f) (pair_pmf A B)) (a, b)"
+ by simp
+qed
+
+lemma map_pair: "map_pmf (\<lambda>(a, b). (f a, g b)) (pair_pmf A B) = pair_pmf (map_pmf f A) (map_pmf g B)"
+ by (simp add: pair_map_pmf2 pair_map_pmf1 map_pmf_comp split_beta')
+
lemma bind_pair_pmf:
assumes M[measurable]: "M \<in> measurable (count_space UNIV \<Otimes>\<^sub>M count_space UNIV) (subprob_algebra N)"
shows "measure_pmf (pair_pmf A B) \<guillemotright>= M = (measure_pmf A \<guillemotright>= (\<lambda>x. measure_pmf B \<guillemotright>= (\<lambda>y. M (x, y))))"
@@ -1384,5 +1430,82 @@
by(auto simp add: le_fun_def)
qed (fact natLeq_card_order natLeq_cinfinite)+
+lemma rel_pmf_return_pmf1: "rel_pmf R (return_pmf x) M \<longleftrightarrow> (\<forall>a\<in>M. R x a)"
+proof safe
+ fix a assume "a \<in> M" "rel_pmf R (return_pmf x) M"
+ then obtain pq where *: "\<And>a b. (a, b) \<in> set_pmf pq \<Longrightarrow> R a b"
+ and eq: "return_pmf x = map_pmf fst pq" "M = map_pmf snd pq"
+ by (force elim: rel_pmf.cases)
+ moreover have "set_pmf (return_pmf x) = {x}"
+ by (simp add: set_return_pmf)
+ with `a \<in> M` have "(x, a) \<in> pq"
+ by (force simp: eq set_map_pmf)
+ with * show "R x a"
+ by auto
+qed (auto intro!: rel_pmf.intros[where pq="pair_pmf (return_pmf x) M"]
+ simp: map_fst_pair_pmf map_snd_pair_pmf set_pair_pmf set_return_pmf)
+
+lemma rel_pmf_return_pmf2: "rel_pmf R M (return_pmf x) \<longleftrightarrow> (\<forall>a\<in>M. R a x)"
+ by (subst pmf.rel_flip[symmetric]) (simp add: rel_pmf_return_pmf1)
+
+lemma rel_pmf_rel_prod:
+ "rel_pmf (rel_prod R S) (pair_pmf A A') (pair_pmf B B') \<longleftrightarrow> rel_pmf R A B \<and> rel_pmf S A' B'"
+proof safe
+ assume "rel_pmf (rel_prod R S) (pair_pmf A A') (pair_pmf B B')"
+ then obtain pq where pq: "\<And>a b c d. ((a, c), (b, d)) \<in> set_pmf pq \<Longrightarrow> R a b \<and> S c d"
+ and eq: "map_pmf fst pq = pair_pmf A A'" "map_pmf snd pq = pair_pmf B B'"
+ by (force elim: rel_pmf.cases)
+ show "rel_pmf R A B"
+ proof (rule rel_pmf.intros)
+ let ?f = "\<lambda>(a, b). (fst a, fst b)"
+ have [simp]: "(\<lambda>x. fst (?f x)) = fst o fst" "(\<lambda>x. snd (?f x)) = fst o snd"
+ by auto
+
+ show "map_pmf fst (map_pmf ?f pq) = A"
+ by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_fst_pair_pmf)
+ show "map_pmf snd (map_pmf ?f pq) = B"
+ by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_fst_pair_pmf)
+
+ fix a b assume "(a, b) \<in> set_pmf (map_pmf ?f pq)"
+ then obtain c d where "((a, c), (b, d)) \<in> set_pmf pq"
+ by (auto simp: set_map_pmf)
+ from pq[OF this] show "R a b" ..
+ qed
+ show "rel_pmf S A' B'"
+ proof (rule rel_pmf.intros)
+ let ?f = "\<lambda>(a, b). (snd a, snd b)"
+ have [simp]: "(\<lambda>x. fst (?f x)) = snd o fst" "(\<lambda>x. snd (?f x)) = snd o snd"
+ by auto
+
+ show "map_pmf fst (map_pmf ?f pq) = A'"
+ by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_snd_pair_pmf)
+ show "map_pmf snd (map_pmf ?f pq) = B'"
+ by (simp add: map_pmf_comp pmf.map_comp[symmetric] eq map_snd_pair_pmf)
+
+ fix c d assume "(c, d) \<in> set_pmf (map_pmf ?f pq)"
+ then obtain a b where "((a, c), (b, d)) \<in> set_pmf pq"
+ by (auto simp: set_map_pmf)
+ from pq[OF this] show "S c d" ..
+ qed
+next
+ assume "rel_pmf R A B" "rel_pmf S A' B'"
+ then obtain Rpq Spq
+ where Rpq: "\<And>a b. (a, b) \<in> set_pmf Rpq \<Longrightarrow> R a b"
+ "map_pmf fst Rpq = A" "map_pmf snd Rpq = B"
+ and Spq: "\<And>a b. (a, b) \<in> set_pmf Spq \<Longrightarrow> S a b"
+ "map_pmf fst Spq = A'" "map_pmf snd Spq = B'"
+ by (force elim: rel_pmf.cases)
+
+ let ?f = "(\<lambda>((a, c), (b, d)). ((a, b), (c, d)))"
+ let ?pq = "map_pmf ?f (pair_pmf Rpq Spq)"
+ have [simp]: "(\<lambda>x. fst (?f x)) = (\<lambda>(a, b). (fst a, fst b))" "(\<lambda>x. snd (?f x)) = (\<lambda>(a, b). (snd a, snd b))"
+ by auto
+
+ show "rel_pmf (rel_prod R S) (pair_pmf A A') (pair_pmf B B')"
+ by (rule rel_pmf.intros[where pq="?pq"])
+ (auto simp: map_snd_pair_pmf map_fst_pair_pmf set_pair_pmf set_map_pmf map_pmf_comp Rpq Spq
+ map_pair)
+qed
+
end
--- a/src/HOL/Tools/BNF/bnf_comp.ML Fri Dec 12 14:31:57 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Fri Dec 12 14:42:37 2014 +0100
@@ -925,8 +925,10 @@
in qualify' o Binding.qualify true namei end;
val odead = dead_of_bnf bnf;
val olive = live_of_bnf bnf;
- val oDs_pos = find_indices op = [TFree ("dead", [])] (snd (Term.dest_Type
- (mk_T_of_bnf (replicate odead (TFree ("dead", []))) (replicate olive dummyT) bnf)));
+ val Ds = map (fn i => TFree (string_of_int i, [])) (1 upto odead);
+ val Us = snd (Term.dest_Type (mk_T_of_bnf Ds (replicate olive dummyT) bnf));
+ val oDs_pos = map (fn x => find_index (fn y => x = y) Us) Ds
+ |> filter (fn x => x >= 0);
val oDs = map (nth Ts) oDs_pos;
val Ts' = map (nth Ts) (subtract (op =) oDs_pos (0 upto length Ts - 1));
val ((inners, (Dss, Ass)), (accum', lthy')) =
--- a/src/HOL/Tools/BNF/bnf_def.ML Fri Dec 12 14:31:57 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Dec 12 14:42:37 2014 +0100
@@ -697,10 +697,8 @@
(collect_set_mapN, [Lazy.force (#collect_set_map facts)]),
(in_bdN, [Lazy.force (#in_bd facts)]),
(in_monoN, [Lazy.force (#in_mono facts)]),
- (in_relN, [Lazy.force (#in_rel facts)]),
(map_comp0N, [#map_comp0 axioms]),
(rel_mono_strong0N, [Lazy.force (#rel_mono_strong0 facts)]),
- (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
(set_map0N, #set_map0 axioms),
(set_bdN, #set_bd axioms)] @
(witNs ~~ wit_thmss_of_bnf bnf)
@@ -714,7 +712,8 @@
fun note_unless_dont_note (noted0, lthy0) =
let
val notes =
- [(inj_mapN, [Lazy.force (#inj_map facts)], []),
+ [(in_relN, [Lazy.force (#in_rel facts)], []),
+ (inj_mapN, [Lazy.force (#inj_map facts)], []),
(inj_map_strongN, [Lazy.force (#inj_map_strong facts)], []),
(map_compN, [Lazy.force (#map_comp facts)], []),
(map_cong0N, [#map_cong0 axioms], []),
@@ -732,6 +731,7 @@
(rel_GrpN, [Lazy.force (#rel_Grp facts)], []),
(rel_mapN, Lazy.force (#rel_map facts), []),
(rel_monoN, [Lazy.force (#rel_mono facts)], mono_attrs),
+ (rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)], []),
(rel_transferN, [Lazy.force (#rel_transfer facts)], []),
(set_mapN, map Lazy.force (#set_map facts), []),
(set_transferN, Lazy.force (#set_transfer facts), [])]
--- a/src/HOL/Tools/BNF/bnf_util.ML Fri Dec 12 14:31:57 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_util.ML Fri Dec 12 14:42:37 2014 +0100
@@ -147,7 +147,9 @@
val b' = fold_rev Binding.prefix_name (map (suffix "_" o fst) (#2 (Binding.dest b))) b;
val ((name, info), (lthy, lthy_old)) =
lthy
+ |> Local_Theory.conceal
|> Typedef.add_typedef true (b', Ts, mx) set opt_morphs tac
+ ||> Local_Theory.restore_naming lthy
||> `Local_Theory.restore;
val phi = Proof_Context.export_morphism lthy_old lthy;
in