respect order of/additional type variables supplied by the user in fixed point constructions;
(* Title: HOL/Codatatype/Basic_BNFs.thy
Author: Dmitriy Traytel, TU Muenchen
Author: Andrei Popescu, TU Muenchen
Author: Jasmin Blanchette, TU Muenchen
Copyright 2012
Registration of various types as bounded natural functors.
*)
header {* Registration of Various Types as Bounded Natural Functors *}
theory Basic_BNFs
imports BNF_Def "~~/src/HOL/Quotient_Examples/FSet" "~~/src/HOL/Library/Multiset" Countable_Set
begin
lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]
lemma ctwo_card_order: "card_order ctwo"
using Card_order_ctwo by (unfold ctwo_def Field_card_of)
lemma natLeq_cinfinite: "cinfinite natLeq"
unfolding cinfinite_def Field_natLeq by (rule nat_infinite)
bnf_def ID = "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
apply auto
apply (rule natLeq_card_order)
apply (rule natLeq_cinfinite)
apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)
apply (rule ordLeq_transitive)
apply (rule ordLeq_cexp1[of natLeq])
apply (rule Cinfinite_Cnotzero)
apply (rule conjI)
apply (rule natLeq_cinfinite)
apply (rule natLeq_Card_order)
apply (rule card_of_Card_order)
apply (rule cexp_mono1)
apply (rule ordLeq_csum1)
apply (rule card_of_Card_order)
apply (rule disjI2)
apply (rule cone_ordLeq_cexp)
apply (rule ordLeq_transitive)
apply (rule cone_ordLeq_ctwo)
apply (rule ordLeq_csum2)
apply (rule Card_order_ctwo)
apply (rule natLeq_Card_order)
done
lemma ID_pred[simp]: "ID_pred \<phi> = \<phi>"
unfolding ID_pred_def ID_rel_def Gr_def fun_eq_iff by auto
bnf_def DEADID = "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"]
apply (auto simp add: wpull_id)
apply (rule card_order_csum)
apply (rule natLeq_card_order)
apply (rule card_of_card_order_on)
apply (rule cinfinite_csum)
apply (rule disjI1)
apply (rule natLeq_cinfinite)
apply (rule ordLess_imp_ordLeq)
apply (rule ordLess_ordLeq_trans)
apply (rule ordLess_ctwo_cexp)
apply (rule card_of_Card_order)
apply (rule cexp_mono2'')
apply (rule ordLeq_csum2)
apply (rule card_of_Card_order)
apply (rule ctwo_Cnotzero)
by (rule card_of_Card_order)
lemma DEADID_pred[simp]: "DEADID_pred = (op =)"
unfolding DEADID_pred_def DEADID.rel_Id by simp
ML {*
signature BASIC_BNFS =
sig
val ID_bnf: BNF_Def.BNF
val ID_rel_def: thm
val ID_pred_def: thm
val DEADID_bnf: BNF_Def.BNF
end;
structure Basic_BNFs : BASIC_BNFS =
struct
val ID_bnf = the (BNF_Def.bnf_of @{context} "ID");
val DEADID_bnf = the (BNF_Def.bnf_of @{context} "DEADID");
val rel_def = BNF_Def.rel_def_of_bnf ID_bnf;
val ID_rel_def = rel_def RS sym;
val ID_pred_def =
Local_Defs.unfold @{context} [rel_def] (BNF_Def.pred_def_of_bnf ID_bnf) RS sym;
end;
*}
definition sum_setl :: "'a + 'b \<Rightarrow> 'a set" where
"sum_setl x = (case x of Inl z => {z} | _ => {})"
definition sum_setr :: "'a + 'b \<Rightarrow> 'b set" where
"sum_setr x = (case x of Inr z => {z} | _ => {})"
lemmas sum_set_defs = sum_setl_def[abs_def] sum_setr_def[abs_def]
bnf_def sum = sum_map [sum_setl, sum_setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr]
proof -
show "sum_map id id = id" by (rule sum_map.id)
next
fix f1 f2 g1 g2
show "sum_map (g1 o f1) (g2 o f2) = sum_map g1 g2 o sum_map f1 f2"
by (rule sum_map.comp[symmetric])
next
fix x f1 f2 g1 g2
assume a1: "\<And>z. z \<in> sum_setl x \<Longrightarrow> f1 z = g1 z" and
a2: "\<And>z. z \<in> sum_setr x \<Longrightarrow> f2 z = g2 z"
thus "sum_map f1 f2 x = sum_map g1 g2 x"
proof (cases x)
case Inl thus ?thesis using a1 by (clarsimp simp: sum_setl_def)
next
case Inr thus ?thesis using a2 by (clarsimp simp: sum_setr_def)
qed
next
fix f1 f2
show "sum_setl o sum_map f1 f2 = image f1 o sum_setl"
by (rule ext, unfold o_apply) (simp add: sum_setl_def split: sum.split)
next
fix f1 f2
show "sum_setr o sum_map f1 f2 = image f2 o sum_setr"
by (rule ext, unfold o_apply) (simp add: sum_setr_def split: sum.split)
next
show "card_order natLeq" by (rule natLeq_card_order)
next
show "cinfinite natLeq" by (rule natLeq_cinfinite)
next
fix x
show "|sum_setl x| \<le>o natLeq"
apply (rule ordLess_imp_ordLeq)
apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
by (simp add: sum_setl_def split: sum.split)
next
fix x
show "|sum_setr x| \<le>o natLeq"
apply (rule ordLess_imp_ordLeq)
apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
by (simp add: sum_setr_def split: sum.split)
next
fix A1 :: "'a set" and A2 :: "'b set"
have in_alt: "{x. (case x of Inl z => {z} | _ => {}) \<subseteq> A1 \<and>
(case x of Inr z => {z} | _ => {}) \<subseteq> A2} = A1 <+> A2" (is "?L = ?R")
proof safe
fix x :: "'a + 'b"
assume "(case x of Inl z \<Rightarrow> {z} | _ \<Rightarrow> {}) \<subseteq> A1" "(case x of Inr z \<Rightarrow> {z} | _ \<Rightarrow> {}) \<subseteq> A2"
hence "x \<in> Inl ` A1 \<or> x \<in> Inr ` A2" by (cases x) simp+
thus "x \<in> A1 <+> A2" by blast
qed (auto split: sum.split)
show "|{x. sum_setl x \<subseteq> A1 \<and> sum_setr x \<subseteq> A2}| \<le>o
(( |A1| +c |A2| ) +c ctwo) ^c natLeq"
apply (rule ordIso_ordLeq_trans)
apply (rule card_of_ordIso_subst)
apply (unfold sum_set_defs)
apply (rule in_alt)
apply (rule ordIso_ordLeq_trans)
apply (rule Plus_csum)
apply (rule ordLeq_transitive)
apply (rule ordLeq_csum1)
apply (rule Card_order_csum)
apply (rule ordLeq_cexp1)
apply (rule conjI)
using Field_natLeq UNIV_not_empty czeroE apply fast
apply (rule natLeq_Card_order)
by (rule Card_order_csum)
next
fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22
assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22"
hence
pull1: "\<And>b1 b2. \<lbrakk>b1 \<in> B11; b2 \<in> B21; f11 b1 = f21 b2\<rbrakk> \<Longrightarrow> \<exists>a \<in> A1. p11 a = b1 \<and> p21 a = b2"
and pull2: "\<And>b1 b2. \<lbrakk>b1 \<in> B12; b2 \<in> B22; f12 b1 = f22 b2\<rbrakk> \<Longrightarrow> \<exists>a \<in> A2. p12 a = b1 \<and> p22 a = b2"
unfolding wpull_def by blast+
show "wpull {x. sum_setl x \<subseteq> A1 \<and> sum_setr x \<subseteq> A2}
{x. sum_setl x \<subseteq> B11 \<and> sum_setr x \<subseteq> B12} {x. sum_setl x \<subseteq> B21 \<and> sum_setr x \<subseteq> B22}
(sum_map f11 f12) (sum_map f21 f22) (sum_map p11 p12) (sum_map p21 p22)"
(is "wpull ?in ?in1 ?in2 ?mapf1 ?mapf2 ?mapp1 ?mapp2")
proof (unfold wpull_def)
{ fix B1 B2
assume *: "B1 \<in> ?in1" "B2 \<in> ?in2" "?mapf1 B1 = ?mapf2 B2"
have "\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2"
proof (cases B1)
case (Inl b1)
{ fix b2 assume "B2 = Inr b2"
with Inl *(3) have False by simp
} then obtain b2 where Inl': "B2 = Inl b2" by (cases B2) (simp, blast)
with Inl * have "b1 \<in> B11" "b2 \<in> B21" "f11 b1 = f21 b2"
by (simp add: sum_setl_def)+
with pull1 obtain a where "a \<in> A1" "p11 a = b1" "p21 a = b2" by blast+
with Inl Inl' have "Inl a \<in> ?in" "?mapp1 (Inl a) = B1 \<and> ?mapp2 (Inl a) = B2"
by (simp add: sum_set_defs)+
thus ?thesis by blast
next
case (Inr b1)
{ fix b2 assume "B2 = Inl b2"
with Inr *(3) have False by simp
} then obtain b2 where Inr': "B2 = Inr b2" by (cases B2) (simp, blast)
with Inr * have "b1 \<in> B12" "b2 \<in> B22" "f12 b1 = f22 b2"
by (simp add: sum_set_defs)+
with pull2 obtain a where "a \<in> A2" "p12 a = b1" "p22 a = b2" by blast+
with Inr Inr' have "Inr a \<in> ?in" "?mapp1 (Inr a) = B1 \<and> ?mapp2 (Inr a) = B2"
by (simp add: sum_set_defs)+
thus ?thesis by blast
qed
}
thus "\<forall>B1 B2. B1 \<in> ?in1 \<and> B2 \<in> ?in2 \<and> ?mapf1 B1 = ?mapf2 B2 \<longrightarrow>
(\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2)" by fastforce
qed
qed (auto simp: sum_set_defs)
lemma sum_pred[simp]:
"sum_pred \<phi> \<psi> x y =
(case x of Inl a1 \<Rightarrow> (case y of Inl a2 \<Rightarrow> \<phi> a1 a2 | Inr _ \<Rightarrow> False)
| Inr b1 \<Rightarrow> (case y of Inl _ \<Rightarrow> False | Inr b2 \<Rightarrow> \<psi> b1 b2))"
unfolding sum_setl_def sum_setr_def sum_pred_def sum_rel_def Gr_def relcomp_unfold converse_unfold
by (fastforce split: sum.splits)+
lemma singleton_ordLeq_ctwo_natLeq: "|{x}| \<le>o ctwo *c natLeq"
apply (rule ordLeq_transitive)
apply (rule ordLeq_cprod2)
apply (rule ctwo_Cnotzero)
apply (auto simp: Field_card_of intro: card_of_card_order_on)
apply (rule cprod_mono2)
apply (rule ordLess_imp_ordLeq)
apply (unfold finite_iff_ordLess_natLeq[symmetric])
by simp
definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where
"fsts x = {fst x}"
definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where
"snds x = {snd x}"
lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
bnf_def prod = map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair]
proof (unfold prod_set_defs)
show "map_pair id id = id" by (rule map_pair.id)
next
fix f1 f2 g1 g2
show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2"
by (rule map_pair.comp[symmetric])
next
fix x f1 f2 g1 g2
assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z"
thus "map_pair f1 f2 x = map_pair g1 g2 x" by (cases x) simp
next
fix f1 f2
show "(\<lambda>x. {fst x}) o map_pair f1 f2 = image f1 o (\<lambda>x. {fst x})"
by (rule ext, unfold o_apply) simp
next
fix f1 f2
show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})"
by (rule ext, unfold o_apply) simp
next
show "card_order (ctwo *c natLeq)"
apply (rule card_order_cprod)
apply (rule ctwo_card_order)
by (rule natLeq_card_order)
next
show "cinfinite (ctwo *c natLeq)"
apply (rule cinfinite_cprod2)
apply (rule ctwo_Cnotzero)
apply (rule conjI[OF _ natLeq_Card_order])
by (rule natLeq_cinfinite)
next
fix x
show "|{fst x}| \<le>o ctwo *c natLeq"
by (rule singleton_ordLeq_ctwo_natLeq)
next
fix x
show "|{snd x}| \<le>o ctwo *c natLeq"
by (rule singleton_ordLeq_ctwo_natLeq)
next
fix A1 :: "'a set" and A2 :: "'b set"
have in_alt: "{x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2} = A1 \<times> A2" by auto
show "|{x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2}| \<le>o
( ( |A1| +c |A2| ) +c ctwo) ^c (ctwo *c natLeq)"
apply (rule ordIso_ordLeq_trans)
apply (rule card_of_ordIso_subst)
apply (rule in_alt)
apply (rule ordIso_ordLeq_trans)
apply (rule Times_cprod)
apply (rule ordLeq_transitive)
apply (rule cprod_csum_cexp)
apply (rule cexp_mono)
apply (rule ordLeq_csum1)
apply (rule Card_order_csum)
apply (rule ordLeq_cprod1)
apply (rule Card_order_ctwo)
apply (rule Cinfinite_Cnotzero)
apply (rule conjI[OF _ natLeq_Card_order])
apply (rule natLeq_cinfinite)
apply (rule disjI2)
apply (rule cone_ordLeq_cexp)
apply (rule ordLeq_transitive)
apply (rule cone_ordLeq_ctwo)
apply (rule ordLeq_csum2)
apply (rule Card_order_ctwo)
apply (rule notE)
apply (rule ctwo_not_czero)
apply assumption
by (rule Card_order_ctwo)
next
fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22
assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22"
thus "wpull {x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2}
{x. {fst x} \<subseteq> B11 \<and> {snd x} \<subseteq> B12} {x. {fst x} \<subseteq> B21 \<and> {snd x} \<subseteq> B22}
(map_pair f11 f12) (map_pair f21 f22) (map_pair p11 p12) (map_pair p21 p22)"
unfolding wpull_def by simp fast
qed simp+
lemma prod_pred[simp]:
"prod_pred \<phi> \<psi> p1 p2 = (case p1 of (a1, b1) \<Rightarrow> case p2 of (a2, b2) \<Rightarrow> (\<phi> a1 a2 \<and> \<psi> b1 b2))"
unfolding prod_set_defs prod_pred_def prod_rel_def Gr_def relcomp_unfold converse_unfold by auto
(* TODO: pred characterization for each basic BNF *)
(* Categorical version of pullback: *)
lemma wpull_cat:
assumes p: "wpull A B1 B2 f1 f2 p1 p2"
and c: "f1 o q1 = f2 o q2"
and r: "range q1 \<subseteq> B1" "range q2 \<subseteq> B2"
obtains h where "range h \<subseteq> A \<and> q1 = p1 o h \<and> q2 = p2 o h"
proof-
have *: "\<forall>d. \<exists>a \<in> A. p1 a = q1 d & p2 a = q2 d"
proof safe
fix d
have "f1 (q1 d) = f2 (q2 d)" using c unfolding comp_def[abs_def] by (rule fun_cong)
moreover
have "q1 d : B1" "q2 d : B2" using r unfolding image_def by auto
ultimately show "\<exists>a \<in> A. p1 a = q1 d \<and> p2 a = q2 d"
using p unfolding wpull_def by auto
qed
then obtain h where "!! d. h d \<in> A & p1 (h d) = q1 d & p2 (h d) = q2 d" by metis
thus ?thesis using that by fastforce
qed
lemma card_of_bounded_range:
"|{f :: 'd \<Rightarrow> 'a. range f \<subseteq> B}| \<le>o |Func (UNIV :: 'd set) B|" (is "|?LHS| \<le>o |?RHS|")
proof -
let ?f = "\<lambda>f. %x. if f x \<in> B then Some (f x) else None"
have "inj_on ?f ?LHS" unfolding inj_on_def
proof (unfold fun_eq_iff, safe)
fix g :: "'d \<Rightarrow> 'a" and f :: "'d \<Rightarrow> 'a" and x
assume "range f \<subseteq> B" "range g \<subseteq> B" and eq: "\<forall>x. ?f f x = ?f g x"
hence "f x \<in> B" "g x \<in> B" by auto
with eq have "Some (f x) = Some (g x)" by metis
thus "f x = g x" by simp
qed
moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Func_def by fastforce
ultimately show ?thesis using card_of_ordLeq by fast
qed
bnf_def "fun" = "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|"
["%c x::'b::type. c::'a::type"]
proof
fix f show "id \<circ> f = id f" by simp
next
fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f"
unfolding comp_def[abs_def] ..
next
fix x f g
assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z"
thus "f \<circ> x = g \<circ> x" by auto
next
fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
unfolding image_def comp_def[abs_def] by auto
next
show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
apply (rule card_order_csum)
apply (rule natLeq_card_order)
by (rule card_of_card_order_on)
(* *)
show "cinfinite (natLeq +c ?U)"
apply (rule cinfinite_csum)
apply (rule disjI1)
by (rule natLeq_cinfinite)
next
fix f :: "'d => 'a"
have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image)
also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order)
finally show "|range f| \<le>o natLeq +c ?U" .
next
fix B :: "'a set"
have "|{f::'d => 'a. range f \<subseteq> B}| \<le>o |Func (UNIV :: 'd set) B|" by (rule card_of_bounded_range)
also have "|Func (UNIV :: 'd set) B| =o |B| ^c |UNIV :: 'd set|"
unfolding cexp_def Field_card_of by (rule card_of_refl)
also have "|B| ^c |UNIV :: 'd set| \<le>o
( |B| +c ctwo) ^c (natLeq +c |UNIV :: 'd set| )"
apply (rule cexp_mono)
apply (rule ordLeq_csum1) apply (rule card_of_Card_order)
apply (rule ordLeq_csum2) apply (rule card_of_Card_order)
apply (rule disjI2) apply (rule cone_ordLeq_cexp)
apply (rule ordLeq_transitive) apply (rule cone_ordLeq_ctwo) apply (rule ordLeq_csum2)
apply (rule Card_order_ctwo)
apply (rule notE) apply (rule conjunct1) apply (rule Cnotzero_UNIV) apply blast
apply (rule card_of_Card_order)
done
finally
show "|{f::'d => 'a. range f \<subseteq> B}| \<le>o
( |B| +c ctwo) ^c (natLeq +c |UNIV :: 'd set| )" .
next
fix A B1 B2 f1 f2 p1 p2 assume p: "wpull A B1 B2 f1 f2 p1 p2"
show "wpull {h. range h \<subseteq> A} {g1. range g1 \<subseteq> B1} {g2. range g2 \<subseteq> B2}
(op \<circ> f1) (op \<circ> f2) (op \<circ> p1) (op \<circ> p2)"
unfolding wpull_def
proof safe
fix g1 g2 assume r: "range g1 \<subseteq> B1" "range g2 \<subseteq> B2"
and c: "f1 \<circ> g1 = f2 \<circ> g2"
show "\<exists>h \<in> {h. range h \<subseteq> A}. p1 \<circ> h = g1 \<and> p2 \<circ> h = g2"
using wpull_cat[OF p c r] by simp metis
qed
qed auto
lemma fun_pred[simp]: "fun_pred \<phi> f g = (\<forall>x. \<phi> (f x) (g x))"
unfolding fun_rel_def fun_pred_def Gr_def relcomp_unfold converse_unfold
by (auto intro!: exI dest!: in_mono)
lemma card_of_list_in:
"|{xs. set xs \<subseteq> A}| \<le>o |Pfunc (UNIV :: nat set) A|" (is "|?LHS| \<le>o |?RHS|")
proof -
let ?f = "%xs. %i. if i < length xs \<and> set xs \<subseteq> A then Some (nth xs i) else None"
have "inj_on ?f ?LHS" unfolding inj_on_def fun_eq_iff
proof safe
fix xs :: "'a list" and ys :: "'a list"
assume su: "set xs \<subseteq> A" "set ys \<subseteq> A" and eq: "\<forall>i. ?f xs i = ?f ys i"
hence *: "length xs = length ys"
by (metis linorder_cases option.simps(2) order_less_irrefl)
thus "xs = ys" by (rule nth_equalityI) (metis * eq su option.inject)
qed
moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Pfunc_def by fastforce
ultimately show ?thesis using card_of_ordLeq by blast
qed
lemma list_in_empty: "A = {} \<Longrightarrow> {x. set x \<subseteq> A} = {[]}"
by simp
lemma card_of_Func: "|Func A B| =o |B| ^c |A|"
unfolding cexp_def Field_card_of by (rule card_of_refl)
lemma not_emp_czero_notIn_ordIso_Card_order:
"A \<noteq> {} \<Longrightarrow> ( |A|, czero) \<notin> ordIso \<and> Card_order |A|"
apply (rule conjI)
apply (metis Field_card_of czeroE)
by (rule card_of_Card_order)
lemma list_in_bd: "|{x. set x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq"
proof -
fix A :: "'a set"
show "|{x. set x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq"
proof (cases "A = {}")
case False thus ?thesis
apply -
apply (rule ordLeq_transitive)
apply (rule card_of_list_in)
apply (rule ordLeq_transitive)
apply (erule card_of_Pfunc_Pow_Func)
apply (rule ordIso_ordLeq_trans)
apply (rule Times_cprod)
apply (rule cprod_cinfinite_bound)
apply (rule ordIso_ordLeq_trans)
apply (rule Pow_cexp_ctwo)
apply (rule ordIso_ordLeq_trans)
apply (rule cexp_cong2)
apply (rule card_of_nat)
apply (rule Card_order_ctwo)
apply (rule card_of_Card_order)
apply (rule natLeq_Card_order)
apply (rule disjI1)
apply (rule ctwo_Cnotzero)
apply (rule cexp_mono1)
apply (rule ordLeq_csum2)
apply (rule Card_order_ctwo)
apply (rule disjI1)
apply (rule ctwo_Cnotzero)
apply (rule natLeq_Card_order)
apply (rule ordIso_ordLeq_trans)
apply (rule card_of_Func)
apply (rule ordIso_ordLeq_trans)
apply (rule cexp_cong2)
apply (rule card_of_nat)
apply (rule card_of_Card_order)
apply (rule card_of_Card_order)
apply (rule natLeq_Card_order)
apply (rule disjI1)
apply (erule not_emp_czero_notIn_ordIso_Card_order)
apply (rule cexp_mono1)
apply (rule ordLeq_csum1)
apply (rule card_of_Card_order)
apply (rule disjI1)
apply (erule not_emp_czero_notIn_ordIso_Card_order)
apply (rule natLeq_Card_order)
apply (rule card_of_Card_order)
apply (rule card_of_Card_order)
apply (rule Cinfinite_cexp)
apply (rule ordLeq_csum2)
apply (rule Card_order_ctwo)
apply (rule conjI)
apply (rule natLeq_cinfinite)
by (rule natLeq_Card_order)
next
case True thus ?thesis
apply -
apply (rule ordIso_ordLeq_trans)
apply (rule card_of_ordIso_subst)
apply (erule list_in_empty)
apply (rule ordIso_ordLeq_trans)
apply (rule single_cone)
apply (rule cone_ordLeq_cexp)
apply (rule ordLeq_transitive)
apply (rule cone_ordLeq_ctwo)
apply (rule ordLeq_csum2)
by (rule Card_order_ctwo)
qed
qed
bnf_def list = map [set] "\<lambda>_::'a list. natLeq" ["[]"]
proof -
show "map id = id" by (rule List.map.id)
next
fix f g
show "map (g o f) = map g o map f" by (rule List.map.comp[symmetric])
next
fix x f g
assume "\<And>z. z \<in> set x \<Longrightarrow> f z = g z"
thus "map f x = map g x" by simp
next
fix f
show "set o map f = image f o set" by (rule ext, unfold o_apply, rule set_map)
next
show "card_order natLeq" by (rule natLeq_card_order)
next
show "cinfinite natLeq" by (rule natLeq_cinfinite)
next
fix x
show "|set x| \<le>o natLeq"
apply (rule ordLess_imp_ordLeq)
apply (rule finite_ordLess_infinite[OF _ natLeq_Well_order])
unfolding Field_natLeq Field_card_of by (auto simp: card_of_well_order_on)
next
fix A :: "'a set"
show "|{x. set x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" by (rule list_in_bd)
next
fix A B1 B2 f1 f2 p1 p2
assume "wpull A B1 B2 f1 f2 p1 p2"
hence pull: "\<And>b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<Longrightarrow> \<exists>a \<in> A. p1 a = b1 \<and> p2 a = b2"
unfolding wpull_def by auto
show "wpull {x. set x \<subseteq> A} {x. set x \<subseteq> B1} {x. set x \<subseteq> B2} (map f1) (map f2) (map p1) (map p2)"
(is "wpull ?A ?B1 ?B2 _ _ _ _")
proof (unfold wpull_def)
{ fix as bs assume *: "as \<in> ?B1" "bs \<in> ?B2" "map f1 as = map f2 bs"
hence "length as = length bs" by (metis length_map)
hence "\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs" using *
proof (induct as bs rule: list_induct2)
case (Cons a as b bs)
hence "a \<in> B1" "b \<in> B2" "f1 a = f2 b" by auto
with pull obtain z where "z \<in> A" "p1 z = a" "p2 z = b" by blast
moreover
from Cons obtain zs where "zs \<in> ?A" "map p1 zs = as" "map p2 zs = bs" by auto
ultimately have "z # zs \<in> ?A" "map p1 (z # zs) = a # as \<and> map p2 (z # zs) = b # bs" by auto
thus ?case by (rule_tac x = "z # zs" in bexI)
qed simp
}
thus "\<forall>as bs. as \<in> ?B1 \<and> bs \<in> ?B2 \<and> map f1 as = map f2 bs \<longrightarrow>
(\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs)" by blast
qed
qed auto
bnf_def deadlist = "map id" [] "\<lambda>_::'a list. |lists (UNIV :: 'a set)|" ["[]"]
by (auto simp add: cinfinite_def wpull_def infinite_UNIV_listI map.id
ordLeq_transitive ctwo_def card_of_card_order_on Field_card_of card_of_mono1 ordLeq_cexp2)
(* Finite sets *)
abbreviation afset where "afset \<equiv> abs_fset"
abbreviation rfset where "rfset \<equiv> rep_fset"
lemma fset_fset_member:
"fset A = {a. a |\<in>| A}"
unfolding fset_def fset_member_def by auto
lemma afset_rfset:
"afset (rfset x) = x"
by (rule Quotient_fset[unfolded Quotient_def, THEN conjunct1, rule_format])
lemma afset_rfset_id:
"afset o rfset = id"
unfolding comp_def afset_rfset id_def ..
lemma rfset:
"rfset A = rfset B \<longleftrightarrow> A = B"
by (metis afset_rfset)
lemma afset_set:
"afset as = afset bs \<longleftrightarrow> set as = set bs"
using Quotient_fset unfolding Quotient_def list_eq_def by auto
lemma surj_afset:
"\<exists> as. A = afset as"
by (metis afset_rfset)
lemma fset_def2:
"fset = set o rfset"
unfolding fset_def map_fun_def[abs_def] by simp
lemma fset_def2_raw:
"fset A = set (rfset A)"
unfolding fset_def2 by simp
lemma fset_comp_afset:
"fset o afset = set"
unfolding fset_def2 comp_def apply(rule ext)
unfolding afset_set[symmetric] afset_rfset ..
lemma fset_afset:
"fset (afset as) = set as"
unfolding fset_comp_afset[symmetric] by simp
lemma set_rfset_afset:
"set (rfset (afset as)) = set as"
unfolding afset_set[symmetric] afset_rfset ..
lemma map_fset_comp_afset:
"(map_fset f) o afset = afset o (map f)"
unfolding map_fset_def map_fun_def[abs_def] comp_def apply(rule ext)
unfolding afset_set set_map set_rfset_afset id_apply ..
lemma map_fset_afset:
"(map_fset f) (afset as) = afset (map f as)"
using map_fset_comp_afset unfolding comp_def fun_eq_iff by auto
lemma fset_map_fset:
"fset (map_fset f A) = (image f) (fset A)"
apply(subst afset_rfset[symmetric, of A])
unfolding map_fset_afset fset_afset set_map
unfolding fset_def2_raw ..
lemma map_fset_def2:
"map_fset f = afset o (map f) o rfset"
unfolding map_fset_def map_fun_def[abs_def] by simp
lemma map_fset_def2_raw:
"map_fset f A = afset (map f (rfset A))"
unfolding map_fset_def2 by simp
lemma finite_ex_fset:
assumes "finite A"
shows "\<exists> B. fset B = A"
by (metis assms finite_list fset_afset)
lemma wpull_image:
assumes "wpull A B1 B2 f1 f2 p1 p2"
shows "wpull (Pow A) (Pow B1) (Pow B2) (image f1) (image f2) (image p1) (image p2)"
unfolding wpull_def Pow_def Bex_def mem_Collect_eq proof clarify
fix Y1 Y2 assume Y1: "Y1 \<subseteq> B1" and Y2: "Y2 \<subseteq> B2" and EQ: "f1 ` Y1 = f2 ` Y2"
def X \<equiv> "{a \<in> A. p1 a \<in> Y1 \<and> p2 a \<in> Y2}"
show "\<exists>X\<subseteq>A. p1 ` X = Y1 \<and> p2 ` X = Y2"
proof (rule exI[of _ X], intro conjI)
show "p1 ` X = Y1"
proof
show "Y1 \<subseteq> p1 ` X"
proof safe
fix y1 assume y1: "y1 \<in> Y1"
then obtain y2 where y2: "y2 \<in> Y2" and eq: "f1 y1 = f2 y2" using EQ by auto
then obtain x where "x \<in> A" and "p1 x = y1" and "p2 x = y2"
using assms y1 Y1 Y2 unfolding wpull_def by blast
thus "y1 \<in> p1 ` X" unfolding X_def using y1 y2 by auto
qed
qed(unfold X_def, auto)
show "p2 ` X = Y2"
proof
show "Y2 \<subseteq> p2 ` X"
proof safe
fix y2 assume y2: "y2 \<in> Y2"
then obtain y1 where y1: "y1 \<in> Y1" and eq: "f1 y1 = f2 y2" using EQ by force
then obtain x where "x \<in> A" and "p1 x = y1" and "p2 x = y2"
using assms y2 Y1 Y2 unfolding wpull_def by blast
thus "y2 \<in> p2 ` X" unfolding X_def using y1 y2 by auto
qed
qed(unfold X_def, auto)
qed(unfold X_def, auto)
qed
lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
by (rule f_the_inv_into_f) (auto simp: inj_on_def fset_cong dest!: finite_ex_fset)
bnf_def fset = map_fset [fset] "\<lambda>_::'a fset. natLeq" ["{||}"]
proof -
show "map_fset id = id"
unfolding map_fset_def2 map_id o_id afset_rfset_id ..
next
fix f g
show "map_fset (g o f) = map_fset g o map_fset f"
unfolding map_fset_def2 map.comp[symmetric] comp_def apply(rule ext)
unfolding afset_set set_map fset_def2_raw[symmetric] image_image[symmetric]
unfolding map_fset_afset[symmetric] map_fset_image afset_rfset
by (rule refl)
next
fix x f g
assume "\<And>z. z \<in> fset x \<Longrightarrow> f z = g z"
hence "map f (rfset x) = map g (rfset x)"
apply(intro map_cong) unfolding fset_def2_raw by auto
thus "map_fset f x = map_fset g x" unfolding map_fset_def2_raw
by (rule arg_cong)
next
fix f
show "fset o map_fset f = image f o fset"
unfolding comp_def fset_map_fset ..
next
show "card_order natLeq" by (rule natLeq_card_order)
next
show "cinfinite natLeq" by (rule natLeq_cinfinite)
next
fix x
show "|fset x| \<le>o natLeq"
unfolding fset_def2_raw
apply (rule ordLess_imp_ordLeq)
apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
by (rule finite_set)
next
fix A :: "'a set"
have "|{x. fset x \<subseteq> A}| \<le>o |afset ` {as. set as \<subseteq> A}|"
apply(rule card_of_mono1) unfolding fset_def2_raw apply auto
apply (rule image_eqI)
by (auto simp: afset_rfset)
also have "|afset ` {as. set as \<subseteq> A}| \<le>o |{as. set as \<subseteq> A}|" using card_of_image .
also have "|{as. set as \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" by (rule list_in_bd)
finally show "|{x. fset x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" .
next
fix A B1 B2 f1 f2 p1 p2
assume wp: "wpull A B1 B2 f1 f2 p1 p2"
hence "wpull (Pow A) (Pow B1) (Pow B2) (image f1) (image f2) (image p1) (image p2)"
by(rule wpull_image)
show "wpull {x. fset x \<subseteq> A} {x. fset x \<subseteq> B1} {x. fset x \<subseteq> B2}
(map_fset f1) (map_fset f2) (map_fset p1) (map_fset p2)"
unfolding wpull_def Pow_def Bex_def mem_Collect_eq proof clarify
fix y1 y2
assume Y1: "fset y1 \<subseteq> B1" and Y2: "fset y2 \<subseteq> B2"
assume "map_fset f1 y1 = map_fset f2 y2"
hence EQ: "f1 ` (fset y1) = f2 ` (fset y2)" unfolding map_fset_def2_raw
unfolding afset_set set_map fset_def2_raw .
with Y1 Y2 obtain X where X: "X \<subseteq> A"
and Y1: "p1 ` X = fset y1" and Y2: "p2 ` X = fset y2"
using wpull_image[OF wp] unfolding wpull_def Pow_def
unfolding Bex_def mem_Collect_eq apply -
apply(erule allE[of _ "fset y1"], erule allE[of _ "fset y2"]) by auto
have "\<forall> y1' \<in> fset y1. \<exists> x. x \<in> X \<and> y1' = p1 x" using Y1 by auto
then obtain q1 where q1: "\<forall> y1' \<in> fset y1. q1 y1' \<in> X \<and> y1' = p1 (q1 y1')" by metis
have "\<forall> y2' \<in> fset y2. \<exists> x. x \<in> X \<and> y2' = p2 x" using Y2 by auto
then obtain q2 where q2: "\<forall> y2' \<in> fset y2. q2 y2' \<in> X \<and> y2' = p2 (q2 y2')" by metis
def X' \<equiv> "q1 ` (fset y1) \<union> q2 ` (fset y2)"
have X': "X' \<subseteq> A" and Y1: "p1 ` X' = fset y1" and Y2: "p2 ` X' = fset y2"
using X Y1 Y2 q1 q2 unfolding X'_def by auto
have fX': "finite X'" unfolding X'_def by simp
then obtain x where X'eq: "X' = fset x" by (auto dest: finite_ex_fset)
show "\<exists>x. fset x \<subseteq> A \<and> map_fset p1 x = y1 \<and> map_fset p2 x = y2"
apply(intro exI[of _ "x"]) using X' Y1 Y2
unfolding X'eq map_fset_def2_raw fset_def2_raw set_map[symmetric]
afset_set[symmetric] afset_rfset by simp
qed
qed auto
lemma fset_pred[simp]: "fset_pred R a b \<longleftrightarrow>
((\<forall>t \<in> fset a. (\<exists>u \<in> fset b. R t u)) \<and>
(\<forall>t \<in> fset b. (\<exists>u \<in> fset a. R u t)))" (is "?L = ?R")
proof
assume ?L thus ?R unfolding fset_rel_def fset_pred_def
Gr_def relcomp_unfold converse_unfold
apply (simp add: subset_eq Ball_def)
apply (rule conjI)
apply (clarsimp, metis snd_conv)
by (clarsimp, metis fst_conv)
next
assume ?R
def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?R'")
have "finite ?R'" by (intro finite_Int[OF disjI2] finite_cartesian_product) auto
hence *: "fset R' = ?R'" unfolding R'_def by (intro fset_to_fset)
show ?L unfolding fset_rel_def fset_pred_def Gr_def relcomp_unfold converse_unfold
proof (intro CollectI prod_caseI exI conjI)
from * show "(R', a) = (R', map_fset fst R')" using conjunct1[OF `?R`]
by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits)
from * show "(R', b) = (R', map_fset snd R')" using conjunct2[OF `?R`]
by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits)
qed (auto simp add: *)
qed
(* Countable sets *)
lemma card_of_countable_sets_range:
fixes A :: "'a set"
shows "|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |{f::nat \<Rightarrow> 'a. range f \<subseteq> A}|"
apply(rule card_of_ordLeqI[of fromNat]) using inj_on_fromNat
unfolding inj_on_def by auto
lemma card_of_countable_sets_Func:
"|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |A| ^c natLeq"
using card_of_countable_sets_range card_of_Func_UNIV[THEN ordIso_symmetric]
unfolding cexp_def Field_natLeq Field_card_of
by(rule ordLeq_ordIso_trans)
lemma ordLeq_countable_subsets:
"|A| \<le>o |{X. X \<subseteq> A \<and> countable X}|"
apply(rule card_of_ordLeqI[of "\<lambda> a. {a}"]) unfolding inj_on_def by auto
lemma finite_countable_subset:
"finite {X. X \<subseteq> A \<and> countable X} \<longleftrightarrow> finite A"
apply default
apply (erule contrapos_pp)
apply (rule card_of_ordLeq_infinite)
apply (rule ordLeq_countable_subsets)
apply assumption
apply (rule finite_Collect_conjI)
apply (rule disjI1)
by (erule finite_Collect_subsets)
lemma card_of_countable_sets:
"|{X. X \<subseteq> A \<and> countable X}| \<le>o ( |A| +c ctwo) ^c natLeq"
(is "|?L| \<le>o _")
proof(cases "finite A")
let ?R = "Func (UNIV::nat set) (A <+> (UNIV::bool set))"
case True hence "finite ?L" by simp
moreover have "infinite ?R"
apply(rule infinite_Func[of _ "Inr True" "Inr False"]) by auto
ultimately show ?thesis unfolding cexp_def csum_def ctwo_def Field_natLeq Field_card_of
apply(intro ordLess_imp_ordLeq) by (rule finite_ordLess_infinite2)
next
case False
hence "|{X. X \<subseteq> A \<and> countable X}| =o |{X. X \<subseteq> A \<and> countable X} - {{}}|"
by (intro card_of_infinite_diff_finitte finite.emptyI finite.insertI ordIso_symmetric)
(unfold finite_countable_subset)
also have "|{X. X \<subseteq> A \<and> countable X} - {{}}| \<le>o |A| ^c natLeq"
using card_of_countable_sets_Func[of A] unfolding set_diff_eq by auto
also have "|A| ^c natLeq \<le>o ( |A| +c ctwo) ^c natLeq"
apply(rule cexp_mono1_cone_ordLeq)
apply(rule ordLeq_csum1, rule card_of_Card_order)
apply (rule cone_ordLeq_cexp)
apply (rule cone_ordLeq_Cnotzero)
using csum_Cnotzero2 ctwo_Cnotzero apply blast
by (rule natLeq_Card_order)
finally show ?thesis .
qed
bnf_def cset = cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"]
proof -
show "cIm id = id" unfolding cIm_def[abs_def] id_def by auto
next
fix f g show "cIm (g \<circ> f) = cIm g \<circ> cIm f"
unfolding cIm_def[abs_def] apply(rule ext) unfolding comp_def by auto
next
fix C f g assume eq: "\<And>a. a \<in> rcset C \<Longrightarrow> f a = g a"
thus "cIm f C = cIm g C"
unfolding cIm_def[abs_def] unfolding image_def by auto
next
fix f show "rcset \<circ> cIm f = op ` f \<circ> rcset" unfolding cIm_def[abs_def] by auto
next
show "card_order natLeq" by (rule natLeq_card_order)
next
show "cinfinite natLeq" by (rule natLeq_cinfinite)
next
fix C show "|rcset C| \<le>o natLeq" using rcset unfolding countable_def .
next
fix A :: "'a set"
have "|{Z. rcset Z \<subseteq> A}| \<le>o |acset ` {X. X \<subseteq> A \<and> countable X}|"
apply(rule card_of_mono1) unfolding Pow_def image_def
proof (rule Collect_mono, clarsimp)
fix x
assume "rcset x \<subseteq> A"
hence "rcset x \<subseteq> A \<and> countable (rcset x) \<and> x = acset (rcset x)"
using acset_rcset[of x] rcset[of x] by force
thus "\<exists>y \<subseteq> A. countable y \<and> x = acset y" by blast
qed
also have "|acset ` {X. X \<subseteq> A \<and> countable X}| \<le>o |{X. X \<subseteq> A \<and> countable X}|"
using card_of_image .
also have "|{X. X \<subseteq> A \<and> countable X}| \<le>o ( |A| +c ctwo) ^c natLeq"
using card_of_countable_sets .
finally show "|{Z. rcset Z \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" .
next
fix A B1 B2 f1 f2 p1 p2
assume wp: "wpull A B1 B2 f1 f2 p1 p2"
show "wpull {x. rcset x \<subseteq> A} {x. rcset x \<subseteq> B1} {x. rcset x \<subseteq> B2}
(cIm f1) (cIm f2) (cIm p1) (cIm p2)"
unfolding wpull_def proof safe
fix y1 y2
assume Y1: "rcset y1 \<subseteq> B1" and Y2: "rcset y2 \<subseteq> B2"
assume "cIm f1 y1 = cIm f2 y2"
hence EQ: "f1 ` (rcset y1) = f2 ` (rcset y2)"
unfolding cIm_def by auto
with Y1 Y2 obtain X where X: "X \<subseteq> A"
and Y1: "p1 ` X = rcset y1" and Y2: "p2 ` X = rcset y2"
using wpull_image[OF wp] unfolding wpull_def Pow_def
unfolding Bex_def mem_Collect_eq apply -
apply(erule allE[of _ "rcset y1"], erule allE[of _ "rcset y2"]) by auto
have "\<forall> y1' \<in> rcset y1. \<exists> x. x \<in> X \<and> y1' = p1 x" using Y1 by auto
then obtain q1 where q1: "\<forall> y1' \<in> rcset y1. q1 y1' \<in> X \<and> y1' = p1 (q1 y1')" by metis
have "\<forall> y2' \<in> rcset y2. \<exists> x. x \<in> X \<and> y2' = p2 x" using Y2 by auto
then obtain q2 where q2: "\<forall> y2' \<in> rcset y2. q2 y2' \<in> X \<and> y2' = p2 (q2 y2')" by metis
def X' \<equiv> "q1 ` (rcset y1) \<union> q2 ` (rcset y2)"
have X': "X' \<subseteq> A" and Y1: "p1 ` X' = rcset y1" and Y2: "p2 ` X' = rcset y2"
using X Y1 Y2 q1 q2 unfolding X'_def by fast+
have fX': "countable X'" unfolding X'_def by simp
then obtain x where X'eq: "X' = rcset x" by (metis rcset_acset)
show "\<exists>x\<in>{x. rcset x \<subseteq> A}. cIm p1 x = y1 \<and> cIm p2 x = y2"
apply(intro bexI[of _ "x"]) using X' Y1 Y2 unfolding X'eq cIm_def by auto
qed
qed (unfold cEmp_def, auto)
(* Multisets *)
lemma setsum_gt_0_iff:
fixes f :: "'a \<Rightarrow> nat" assumes "finite A"
shows "setsum f A > 0 \<longleftrightarrow> (\<exists> a \<in> A. f a > 0)"
(is "?L \<longleftrightarrow> ?R")
proof-
have "?L \<longleftrightarrow> \<not> setsum f A = 0" by fast
also have "... \<longleftrightarrow> (\<exists> a \<in> A. f a \<noteq> 0)" using assms by simp
also have "... \<longleftrightarrow> ?R" by simp
finally show ?thesis .
qed
(* *)
definition mmap :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> 'b \<Rightarrow> nat" where
"mmap h f b = setsum f {a. h a = b \<and> f a > 0}"
lemma mmap_id: "mmap id = id"
proof (rule ext)+
fix f a show "mmap id f a = id f a"
proof(cases "f a = 0")
case False
hence 1: "{aa. aa = a \<and> 0 < f aa} = {a}" by auto
show ?thesis by (simp add: mmap_def id_apply 1)
qed(unfold mmap_def, auto)
qed
lemma inj_on_setsum_inv:
assumes f: "f \<in> multiset"
and 1: "(0::nat) < setsum f {a. h a = b' \<and> 0 < f a}" (is "0 < setsum f ?A'")
and 2: "{a. h a = b \<and> 0 < f a} = {a. h a = b' \<and> 0 < f a}" (is "?A = ?A'")
shows "b = b'"
proof-
have "finite ?A'" using f unfolding multiset_def by auto
hence "?A' \<noteq> {}" using 1 setsum_gt_0_iff by auto
thus ?thesis using 2 by auto
qed
lemma mmap_comp:
fixes h1 :: "'a \<Rightarrow> 'b" and h2 :: "'b \<Rightarrow> 'c"
assumes f: "f \<in> multiset"
shows "mmap (h2 o h1) f = (mmap h2 o mmap h1) f"
unfolding mmap_def[abs_def] comp_def proof(rule ext)+
fix c :: 'c
let ?A = "{a. h2 (h1 a) = c \<and> 0 < f a}"
let ?As = "\<lambda> b. {a. h1 a = b \<and> 0 < f a}"
let ?B = "{b. h2 b = c \<and> 0 < setsum f (?As b)}"
have 0: "{?As b | b. b \<in> ?B} = ?As ` ?B" by auto
have "\<And> b. finite (?As b)" using f unfolding multiset_def by simp
hence "?B = {b. h2 b = c \<and> ?As b \<noteq> {}}" using setsum_gt_0_iff by auto
hence A: "?A = \<Union> {?As b | b. b \<in> ?B}" by auto
have "setsum f ?A = setsum (setsum f) {?As b | b. b \<in> ?B}"
unfolding A apply(rule setsum_Union_disjoint)
using f unfolding multiset_def by auto
also have "... = setsum (setsum f) (?As ` ?B)" unfolding 0 ..
also have "... = setsum (setsum f o ?As) ?B" apply(rule setsum_reindex)
unfolding inj_on_def apply auto using inj_on_setsum_inv[OF f, of h1] by blast
also have "... = setsum (\<lambda> b. setsum f (?As b)) ?B" unfolding comp_def ..
finally show "setsum f ?A = setsum (\<lambda> b. setsum f (?As b)) ?B" .
qed
lemma mmap_comp1:
fixes h1 :: "'a \<Rightarrow> 'b" and h2 :: "'b \<Rightarrow> 'c"
assumes "f \<in> multiset"
shows "mmap (\<lambda> a. h2 (h1 a)) f = mmap h2 (mmap h1 f)"
using mmap_comp[OF assms] unfolding comp_def by auto
lemma mmap:
assumes "f \<in> multiset"
shows "mmap h f \<in> multiset"
using assms unfolding mmap_def[abs_def] multiset_def proof safe
assume fin: "finite {a. 0 < f a}" (is "finite ?A")
show "finite {b. 0 < setsum f {a. h a = b \<and> 0 < f a}}"
(is "finite {b. 0 < setsum f (?As b)}")
proof- let ?B = "{b. 0 < setsum f (?As b)}"
have "\<And> b. finite (?As b)" using assms unfolding multiset_def by simp
hence B: "?B = {b. ?As b \<noteq> {}}" using setsum_gt_0_iff by auto
hence "?B \<subseteq> h ` ?A" by auto
thus ?thesis using finite_surj[OF fin] by auto
qed
qed
lemma mmap_cong:
assumes "\<And>a. a \<in># M \<Longrightarrow> f a = g a"
shows "mmap f (count M) = mmap g (count M)"
using assms unfolding mmap_def[abs_def] by (intro ext, intro setsum_cong) auto
abbreviation supp where "supp f \<equiv> {a. f a > 0}"
lemma mmap_image_comp:
assumes f: "f \<in> multiset"
shows "(supp o mmap h) f = (image h o supp) f"
unfolding mmap_def[abs_def] comp_def proof-
have "\<And> b. finite {a. h a = b \<and> 0 < f a}" (is "\<And> b. finite (?As b)")
using f unfolding multiset_def by auto
thus "{b. 0 < setsum f (?As b)} = h ` {a. 0 < f a}"
using setsum_gt_0_iff by auto
qed
lemma mmap_image:
assumes f: "f \<in> multiset"
shows "supp (mmap h f) = h ` (supp f)"
using mmap_image_comp[OF assms] unfolding comp_def .
lemma set_of_Abs_multiset:
assumes f: "f \<in> multiset"
shows "set_of (Abs_multiset f) = supp f"
using assms unfolding set_of_def by (auto simp: Abs_multiset_inverse)
lemma supp_count:
"supp (count M) = set_of M"
using assms unfolding set_of_def by auto
lemma multiset_of_surj:
"multiset_of ` {as. set as \<subseteq> A} = {M. set_of M \<subseteq> A}"
proof safe
fix M assume M: "set_of M \<subseteq> A"
obtain as where eq: "M = multiset_of as" using surj_multiset_of unfolding surj_def by auto
hence "set as \<subseteq> A" using M by auto
thus "M \<in> multiset_of ` {as. set as \<subseteq> A}" using eq by auto
next
show "\<And>x xa xb. \<lbrakk>set xa \<subseteq> A; xb \<in> set_of (multiset_of xa)\<rbrakk> \<Longrightarrow> xb \<in> A"
by (erule set_mp) (unfold set_of_multiset_of)
qed
lemma card_of_set_of:
"|{M. set_of M \<subseteq> A}| \<le>o |{as. set as \<subseteq> A}|"
apply(rule card_of_ordLeqI2[of _ multiset_of]) using multiset_of_surj by auto
lemma nat_sum_induct:
assumes "\<And>n1 n2. (\<And> m1 m2. m1 + m2 < n1 + n2 \<Longrightarrow> phi m1 m2) \<Longrightarrow> phi n1 n2"
shows "phi (n1::nat) (n2::nat)"
proof-
let ?chi = "\<lambda> n1n2 :: nat * nat. phi (fst n1n2) (snd n1n2)"
have "?chi (n1,n2)"
apply(induct rule: measure_induct[of "\<lambda> n1n2. fst n1n2 + snd n1n2" ?chi])
using assms by (metis fstI sndI)
thus ?thesis by simp
qed
lemma matrix_count:
fixes ct1 ct2 :: "nat \<Rightarrow> nat"
assumes "setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2}"
shows
"\<exists> ct. (\<forall> i1 \<le> n1. setsum (\<lambda> i2. ct i1 i2) {..<Suc n2} = ct1 i1) \<and>
(\<forall> i2 \<le> n2. setsum (\<lambda> i1. ct i1 i2) {..<Suc n1} = ct2 i2)"
(is "?phi ct1 ct2 n1 n2")
proof-
have "\<forall> ct1 ct2 :: nat \<Rightarrow> nat.
setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2} \<longrightarrow> ?phi ct1 ct2 n1 n2"
proof(induct rule: nat_sum_induct[of
"\<lambda> n1 n2. \<forall> ct1 ct2 :: nat \<Rightarrow> nat.
setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2} \<longrightarrow> ?phi ct1 ct2 n1 n2"],
clarify)
fix n1 n2 :: nat and ct1 ct2 :: "nat \<Rightarrow> nat"
assume IH: "\<And> m1 m2. m1 + m2 < n1 + n2 \<Longrightarrow>
\<forall> dt1 dt2 :: nat \<Rightarrow> nat.
setsum dt1 {..<Suc m1} = setsum dt2 {..<Suc m2} \<longrightarrow> ?phi dt1 dt2 m1 m2"
and ss: "setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2}"
show "?phi ct1 ct2 n1 n2"
proof(cases n1)
case 0 note n1 = 0
show ?thesis
proof(cases n2)
case 0 note n2 = 0
let ?ct = "\<lambda> i1 i2. ct2 0"
show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by simp
next
case (Suc m2) note n2 = Suc
let ?ct = "\<lambda> i1 i2. ct2 i2"
show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by auto
qed
next
case (Suc m1) note n1 = Suc
show ?thesis
proof(cases n2)
case 0 note n2 = 0
let ?ct = "\<lambda> i1 i2. ct1 i1"
show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by auto
next
case (Suc m2) note n2 = Suc
show ?thesis
proof(cases "ct1 n1 \<le> ct2 n2")
case True
def dt2 \<equiv> "\<lambda> i2. if i2 = n2 then ct2 i2 - ct1 n1 else ct2 i2"
have "setsum ct1 {..<Suc m1} = setsum dt2 {..<Suc n2}"
unfolding dt2_def using ss n1 True by auto
hence "?phi ct1 dt2 m1 n2" using IH[of m1 n2] n1 by simp
then obtain dt where
1: "\<And> i1. i1 \<le> m1 \<Longrightarrow> setsum (\<lambda> i2. dt i1 i2) {..<Suc n2} = ct1 i1" and
2: "\<And> i2. i2 \<le> n2 \<Longrightarrow> setsum (\<lambda> i1. dt i1 i2) {..<Suc m1} = dt2 i2" by auto
let ?ct = "\<lambda> i1 i2. if i1 = n1 then (if i2 = n2 then ct1 n1 else 0)
else dt i1 i2"
show ?thesis apply(rule exI[of _ ?ct])
using n1 n2 1 2 True unfolding dt2_def by simp
next
case False
hence False: "ct2 n2 < ct1 n1" by simp
def dt1 \<equiv> "\<lambda> i1. if i1 = n1 then ct1 i1 - ct2 n2 else ct1 i1"
have "setsum dt1 {..<Suc n1} = setsum ct2 {..<Suc m2}"
unfolding dt1_def using ss n2 False by auto
hence "?phi dt1 ct2 n1 m2" using IH[of n1 m2] n2 by simp
then obtain dt where
1: "\<And> i1. i1 \<le> n1 \<Longrightarrow> setsum (\<lambda> i2. dt i1 i2) {..<Suc m2} = dt1 i1" and
2: "\<And> i2. i2 \<le> m2 \<Longrightarrow> setsum (\<lambda> i1. dt i1 i2) {..<Suc n1} = ct2 i2" by force
let ?ct = "\<lambda> i1 i2. if i2 = n2 then (if i1 = n1 then ct2 n2 else 0)
else dt i1 i2"
show ?thesis apply(rule exI[of _ ?ct])
using n1 n2 1 2 False unfolding dt1_def by simp
qed
qed
qed
qed
thus ?thesis using assms by auto
qed
definition
"inj2 u B1 B2 \<equiv>
\<forall> b1 b1' b2 b2'. {b1,b1'} \<subseteq> B1 \<and> {b2,b2'} \<subseteq> B2 \<and> u b1 b2 = u b1' b2'
\<longrightarrow> b1 = b1' \<and> b2 = b2'"
lemma matrix_count_finite:
assumes B1: "B1 \<noteq> {}" "finite B1" and B2: "B2 \<noteq> {}" "finite B2" and u: "inj2 u B1 B2"
and ss: "setsum N1 B1 = setsum N2 B2"
shows "\<exists> M :: 'a \<Rightarrow> nat.
(\<forall> b1 \<in> B1. setsum (\<lambda> b2. M (u b1 b2)) B2 = N1 b1) \<and>
(\<forall> b2 \<in> B2. setsum (\<lambda> b1. M (u b1 b2)) B1 = N2 b2)"
proof-
obtain n1 where "card B1 = Suc n1" using B1 by (metis card_insert finite.simps)
then obtain e1 where e1: "bij_betw e1 {..<Suc n1} B1"
using ex_bij_betw_finite_nat[OF B1(2)] by (metis atLeast0LessThan bij_betw_the_inv_into)
hence e1_inj: "inj_on e1 {..<Suc n1}" and e1_surj: "e1 ` {..<Suc n1} = B1"
unfolding bij_betw_def by auto
def f1 \<equiv> "inv_into {..<Suc n1} e1"
have f1: "bij_betw f1 B1 {..<Suc n1}"
and f1e1[simp]: "\<And> i1. i1 < Suc n1 \<Longrightarrow> f1 (e1 i1) = i1"
and e1f1[simp]: "\<And> b1. b1 \<in> B1 \<Longrightarrow> e1 (f1 b1) = b1" unfolding f1_def
apply (metis bij_betw_inv_into e1, metis bij_betw_inv_into_left e1 lessThan_iff)
by (metis e1_surj f_inv_into_f)
(* *)
obtain n2 where "card B2 = Suc n2" using B2 by (metis card_insert finite.simps)
then obtain e2 where e2: "bij_betw e2 {..<Suc n2} B2"
using ex_bij_betw_finite_nat[OF B2(2)] by (metis atLeast0LessThan bij_betw_the_inv_into)
hence e2_inj: "inj_on e2 {..<Suc n2}" and e2_surj: "e2 ` {..<Suc n2} = B2"
unfolding bij_betw_def by auto
def f2 \<equiv> "inv_into {..<Suc n2} e2"
have f2: "bij_betw f2 B2 {..<Suc n2}"
and f2e2[simp]: "\<And> i2. i2 < Suc n2 \<Longrightarrow> f2 (e2 i2) = i2"
and e2f2[simp]: "\<And> b2. b2 \<in> B2 \<Longrightarrow> e2 (f2 b2) = b2" unfolding f2_def
apply (metis bij_betw_inv_into e2, metis bij_betw_inv_into_left e2 lessThan_iff)
by (metis e2_surj f_inv_into_f)
(* *)
let ?ct1 = "N1 o e1" let ?ct2 = "N2 o e2"
have ss: "setsum ?ct1 {..<Suc n1} = setsum ?ct2 {..<Suc n2}"
unfolding setsum_reindex[OF e1_inj, symmetric] setsum_reindex[OF e2_inj, symmetric]
e1_surj e2_surj using ss .
obtain ct where
ct1: "\<And> i1. i1 \<le> n1 \<Longrightarrow> setsum (\<lambda> i2. ct i1 i2) {..<Suc n2} = ?ct1 i1" and
ct2: "\<And> i2. i2 \<le> n2 \<Longrightarrow> setsum (\<lambda> i1. ct i1 i2) {..<Suc n1} = ?ct2 i2"
using matrix_count[OF ss] by blast
(* *)
def A \<equiv> "{u b1 b2 | b1 b2. b1 \<in> B1 \<and> b2 \<in> B2}"
have "\<forall> a \<in> A. \<exists> b1b2 \<in> B1 <*> B2. u (fst b1b2) (snd b1b2) = a"
unfolding A_def Ball_def mem_Collect_eq by auto
then obtain h1h2 where h12:
"\<And>a. a \<in> A \<Longrightarrow> u (fst (h1h2 a)) (snd (h1h2 a)) = a \<and> h1h2 a \<in> B1 <*> B2" by metis
def h1 \<equiv> "fst o h1h2" def h2 \<equiv> "snd o h1h2"
have h12[simp]: "\<And>a. a \<in> A \<Longrightarrow> u (h1 a) (h2 a) = a"
"\<And> a. a \<in> A \<Longrightarrow> h1 a \<in> B1" "\<And> a. a \<in> A \<Longrightarrow> h2 a \<in> B2"
using h12 unfolding h1_def h2_def by force+
{fix b1 b2 assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2"
hence inA: "u b1 b2 \<in> A" unfolding A_def by auto
hence "u b1 b2 = u (h1 (u b1 b2)) (h2 (u b1 b2))" by auto
moreover have "h1 (u b1 b2) \<in> B1" "h2 (u b1 b2) \<in> B2" using inA by auto
ultimately have "h1 (u b1 b2) = b1 \<and> h2 (u b1 b2) = b2"
using u b1 b2 unfolding inj2_def by fastforce
}
hence h1[simp]: "\<And> b1 b2. \<lbrakk>b1 \<in> B1; b2 \<in> B2\<rbrakk> \<Longrightarrow> h1 (u b1 b2) = b1" and
h2[simp]: "\<And> b1 b2. \<lbrakk>b1 \<in> B1; b2 \<in> B2\<rbrakk> \<Longrightarrow> h2 (u b1 b2) = b2" by auto
def M \<equiv> "\<lambda> a. ct (f1 (h1 a)) (f2 (h2 a))"
show ?thesis
apply(rule exI[of _ M]) proof safe
fix b1 assume b1: "b1 \<in> B1"
hence f1b1: "f1 b1 \<le> n1" using f1 unfolding bij_betw_def
by (metis bij_betwE f1 lessThan_iff less_Suc_eq_le)
have "(\<Sum>b2\<in>B2. M (u b1 b2)) = (\<Sum>i2<Suc n2. ct (f1 b1) (f2 (e2 i2)))"
unfolding e2_surj[symmetric] setsum_reindex[OF e2_inj]
unfolding M_def comp_def apply(intro setsum_cong) apply force
by (metis e2_surj b1 h1 h2 imageI)
also have "... = N1 b1" using b1 ct1[OF f1b1] by simp
finally show "(\<Sum>b2\<in>B2. M (u b1 b2)) = N1 b1" .
next
fix b2 assume b2: "b2 \<in> B2"
hence f2b2: "f2 b2 \<le> n2" using f2 unfolding bij_betw_def
by (metis bij_betwE f2 lessThan_iff less_Suc_eq_le)
have "(\<Sum>b1\<in>B1. M (u b1 b2)) = (\<Sum>i1<Suc n1. ct (f1 (e1 i1)) (f2 b2))"
unfolding e1_surj[symmetric] setsum_reindex[OF e1_inj]
unfolding M_def comp_def apply(intro setsum_cong) apply force
by (metis e1_surj b2 h1 h2 imageI)
also have "... = N2 b2" using b2 ct2[OF f2b2] by simp
finally show "(\<Sum>b1\<in>B1. M (u b1 b2)) = N2 b2" .
qed
qed
lemma supp_vimage_mmap:
assumes "M \<in> multiset"
shows "supp M \<subseteq> f -` (supp (mmap f M))"
using assms by (auto simp: mmap_image)
lemma mmap_ge_0:
assumes "M \<in> multiset"
shows "0 < mmap f M b \<longleftrightarrow> (\<exists>a. 0 < M a \<and> f a = b)"
proof-
have f: "finite {a. f a = b \<and> 0 < M a}" using assms unfolding multiset_def by auto
show ?thesis unfolding mmap_def setsum_gt_0_iff[OF f] by auto
qed
lemma finite_twosets:
assumes "finite B1" and "finite B2"
shows "finite {u b1 b2 |b1 b2. b1 \<in> B1 \<and> b2 \<in> B2}" (is "finite ?A")
proof-
have A: "?A = (\<lambda> b1b2. u (fst b1b2) (snd b1b2)) ` (B1 <*> B2)" by force
show ?thesis unfolding A using finite_cartesian_product[OF assms] by auto
qed
lemma wp_mmap:
fixes A :: "'a set" and B1 :: "'b1 set" and B2 :: "'b2 set"
assumes wp: "wpull A B1 B2 f1 f2 p1 p2"
shows
"wpull {M. M \<in> multiset \<and> supp M \<subseteq> A}
{N1. N1 \<in> multiset \<and> supp N1 \<subseteq> B1} {N2. N2 \<in> multiset \<and> supp N2 \<subseteq> B2}
(mmap f1) (mmap f2) (mmap p1) (mmap p2)"
unfolding wpull_def proof (safe, unfold Bex_def mem_Collect_eq)
fix N1 :: "'b1 \<Rightarrow> nat" and N2 :: "'b2 \<Rightarrow> nat"
assume mmap': "mmap f1 N1 = mmap f2 N2"
and N1[simp]: "N1 \<in> multiset" "supp N1 \<subseteq> B1"
and N2[simp]: "N2 \<in> multiset" "supp N2 \<subseteq> B2"
have mN1[simp]: "mmap f1 N1 \<in> multiset" using N1 by (auto simp: mmap)
have mN2[simp]: "mmap f2 N2 \<in> multiset" using N2 by (auto simp: mmap)
def P \<equiv> "mmap f1 N1"
have P1: "P = mmap f1 N1" and P2: "P = mmap f2 N2" unfolding P_def using mmap' by auto
note P = P1 P2
have P_mult[simp]: "P \<in> multiset" unfolding P_def using N1 by auto
have fin_N1[simp]: "finite (supp N1)" using N1(1) unfolding multiset_def by auto
have fin_N2[simp]: "finite (supp N2)" using N2(1) unfolding multiset_def by auto
have fin_P[simp]: "finite (supp P)" using P_mult unfolding multiset_def by auto
(* *)
def set1 \<equiv> "\<lambda> c. {b1 \<in> supp N1. f1 b1 = c}"
have set1[simp]: "\<And> c b1. b1 \<in> set1 c \<Longrightarrow> f1 b1 = c" unfolding set1_def by auto
have fin_set1: "\<And> c. c \<in> supp P \<Longrightarrow> finite (set1 c)"
using N1(1) unfolding set1_def multiset_def by auto
have set1_NE: "\<And> c. c \<in> supp P \<Longrightarrow> set1 c \<noteq> {}"
unfolding set1_def P1 mmap_ge_0[OF N1(1)] by auto
have supp_N1_set1: "supp N1 = (\<Union> c \<in> supp P. set1 c)"
using supp_vimage_mmap[OF N1(1), of f1] unfolding set1_def P1 by auto
hence set1_inclN1: "\<And>c. c \<in> supp P \<Longrightarrow> set1 c \<subseteq> supp N1" by auto
hence set1_incl: "\<And> c. c \<in> supp P \<Longrightarrow> set1 c \<subseteq> B1" using N1(2) by blast
have set1_disj: "\<And> c c'. c \<noteq> c' \<Longrightarrow> set1 c \<inter> set1 c' = {}"
unfolding set1_def by auto
have setsum_set1: "\<And> c. setsum N1 (set1 c) = P c"
unfolding P1 set1_def mmap_def apply(rule setsum_cong) by auto
(* *)
def set2 \<equiv> "\<lambda> c. {b2 \<in> supp N2. f2 b2 = c}"
have set2[simp]: "\<And> c b2. b2 \<in> set2 c \<Longrightarrow> f2 b2 = c" unfolding set2_def by auto
have fin_set2: "\<And> c. c \<in> supp P \<Longrightarrow> finite (set2 c)"
using N2(1) unfolding set2_def multiset_def by auto
have set2_NE: "\<And> c. c \<in> supp P \<Longrightarrow> set2 c \<noteq> {}"
unfolding set2_def P2 mmap_ge_0[OF N2(1)] by auto
have supp_N2_set2: "supp N2 = (\<Union> c \<in> supp P. set2 c)"
using supp_vimage_mmap[OF N2(1), of f2] unfolding set2_def P2 by auto
hence set2_inclN2: "\<And>c. c \<in> supp P \<Longrightarrow> set2 c \<subseteq> supp N2" by auto
hence set2_incl: "\<And> c. c \<in> supp P \<Longrightarrow> set2 c \<subseteq> B2" using N2(2) by blast
have set2_disj: "\<And> c c'. c \<noteq> c' \<Longrightarrow> set2 c \<inter> set2 c' = {}"
unfolding set2_def by auto
have setsum_set2: "\<And> c. setsum N2 (set2 c) = P c"
unfolding P2 set2_def mmap_def apply(rule setsum_cong) by auto
(* *)
have ss: "\<And> c. c \<in> supp P \<Longrightarrow> setsum N1 (set1 c) = setsum N2 (set2 c)"
unfolding setsum_set1 setsum_set2 ..
have "\<forall> c \<in> supp P. \<forall> b1b2 \<in> (set1 c) \<times> (set2 c).
\<exists> a \<in> A. p1 a = fst b1b2 \<and> p2 a = snd b1b2"
using wp set1_incl set2_incl unfolding wpull_def Ball_def mem_Collect_eq
by simp (metis set1 set2 set_rev_mp)
then obtain uu where uu:
"\<forall> c \<in> supp P. \<forall> b1b2 \<in> (set1 c) \<times> (set2 c).
uu c b1b2 \<in> A \<and> p1 (uu c b1b2) = fst b1b2 \<and> p2 (uu c b1b2) = snd b1b2" by metis
def u \<equiv> "\<lambda> c b1 b2. uu c (b1,b2)"
have u[simp]:
"\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> u c b1 b2 \<in> A"
"\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> p1 (u c b1 b2) = b1"
"\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> p2 (u c b1 b2) = b2"
using uu unfolding u_def by auto
{fix c assume c: "c \<in> supp P"
have "inj2 (u c) (set1 c) (set2 c)" unfolding inj2_def proof clarify
fix b1 b1' b2 b2'
assume "{b1, b1'} \<subseteq> set1 c" "{b2, b2'} \<subseteq> set2 c" and 0: "u c b1 b2 = u c b1' b2'"
hence "p1 (u c b1 b2) = b1 \<and> p2 (u c b1 b2) = b2 \<and>
p1 (u c b1' b2') = b1' \<and> p2 (u c b1' b2') = b2'"
using u(2)[OF c] u(3)[OF c] by simp metis
thus "b1 = b1' \<and> b2 = b2'" using 0 by auto
qed
} note inj = this
def sset \<equiv> "\<lambda> c. {u c b1 b2 | b1 b2. b1 \<in> set1 c \<and> b2 \<in> set2 c}"
have fin_sset[simp]: "\<And> c. c \<in> supp P \<Longrightarrow> finite (sset c)" unfolding sset_def
using fin_set1 fin_set2 finite_twosets by blast
have sset_A: "\<And> c. c \<in> supp P \<Longrightarrow> sset c \<subseteq> A" unfolding sset_def by auto
{fix c a assume c: "c \<in> supp P" and ac: "a \<in> sset c"
then obtain b1 b2 where b1: "b1 \<in> set1 c" and b2: "b2 \<in> set2 c"
and a: "a = u c b1 b2" unfolding sset_def by auto
have "p1 a \<in> set1 c" and p2a: "p2 a \<in> set2 c"
using ac a b1 b2 c u(2) u(3) by simp+
hence "u c (p1 a) (p2 a) = a" unfolding a using b1 b2 inj[OF c]
unfolding inj2_def by (metis c u(2) u(3))
} note u_p12[simp] = this
{fix c a assume c: "c \<in> supp P" and ac: "a \<in> sset c"
hence "p1 a \<in> set1 c" unfolding sset_def by auto
}note p1[simp] = this
{fix c a assume c: "c \<in> supp P" and ac: "a \<in> sset c"
hence "p2 a \<in> set2 c" unfolding sset_def by auto
}note p2[simp] = this
(* *)
{fix c assume c: "c \<in> supp P"
hence "\<exists> M. (\<forall> b1 \<in> set1 c. setsum (\<lambda> b2. M (u c b1 b2)) (set2 c) = N1 b1) \<and>
(\<forall> b2 \<in> set2 c. setsum (\<lambda> b1. M (u c b1 b2)) (set1 c) = N2 b2)"
unfolding sset_def
using matrix_count_finite[OF set1_NE[OF c] fin_set1[OF c]
set2_NE[OF c] fin_set2[OF c] inj[OF c] ss[OF c]] by auto
}
then obtain Ms where
ss1: "\<And> c b1. \<lbrakk>c \<in> supp P; b1 \<in> set1 c\<rbrakk> \<Longrightarrow>
setsum (\<lambda> b2. Ms c (u c b1 b2)) (set2 c) = N1 b1" and
ss2: "\<And> c b2. \<lbrakk>c \<in> supp P; b2 \<in> set2 c\<rbrakk> \<Longrightarrow>
setsum (\<lambda> b1. Ms c (u c b1 b2)) (set1 c) = N2 b2"
by metis
def SET \<equiv> "\<Union> c \<in> supp P. sset c"
have fin_SET[simp]: "finite SET" unfolding SET_def apply(rule finite_UN_I) by auto
have SET_A: "SET \<subseteq> A" unfolding SET_def using sset_A by auto
have u_SET[simp]: "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk> \<Longrightarrow> u c b1 b2 \<in> SET"
unfolding SET_def sset_def by blast
{fix c a assume c: "c \<in> supp P" and a: "a \<in> SET" and p1a: "p1 a \<in> set1 c"
then obtain c' where c': "c' \<in> supp P" and ac': "a \<in> sset c'"
unfolding SET_def by auto
hence "p1 a \<in> set1 c'" unfolding sset_def by auto
hence eq: "c = c'" using p1a c c' set1_disj by auto
hence "a \<in> sset c" using ac' by simp
} note p1_rev = this
{fix c a assume c: "c \<in> supp P" and a: "a \<in> SET" and p2a: "p2 a \<in> set2 c"
then obtain c' where c': "c' \<in> supp P" and ac': "a \<in> sset c'"
unfolding SET_def by auto
hence "p2 a \<in> set2 c'" unfolding sset_def by auto
hence eq: "c = c'" using p2a c c' set2_disj by auto
hence "a \<in> sset c" using ac' by simp
} note p2_rev = this
(* *)
have "\<forall> a \<in> SET. \<exists> c \<in> supp P. a \<in> sset c" unfolding SET_def by auto
then obtain h where h: "\<forall> a \<in> SET. h a \<in> supp P \<and> a \<in> sset (h a)" by metis
have h_u[simp]: "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
\<Longrightarrow> h (u c b1 b2) = c"
by (metis h p2 set2 u(3) u_SET)
have h_u1: "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
\<Longrightarrow> h (u c b1 b2) = f1 b1"
using h unfolding sset_def by auto
have h_u2: "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
\<Longrightarrow> h (u c b1 b2) = f2 b2"
using h unfolding sset_def by auto
def M \<equiv> "\<lambda> a. if a \<in> SET \<and> p1 a \<in> supp N1 \<and> p2 a \<in> supp N2 then Ms (h a) a else 0"
have sM: "supp M \<subseteq> SET" "supp M \<subseteq> p1 -` (supp N1)" "supp M \<subseteq> p2 -` (supp N2)"
unfolding M_def by auto
show "\<exists>M. (M \<in> multiset \<and> supp M \<subseteq> A) \<and> mmap p1 M = N1 \<and> mmap p2 M = N2"
proof(rule exI[of _ M], safe)
show "M \<in> multiset"
unfolding multiset_def using finite_subset[OF sM(1) fin_SET] by simp
next
fix a assume "0 < M a"
thus "a \<in> A" unfolding M_def using SET_A by (cases "a \<in> SET") auto
next
show "mmap p1 M = N1"
unfolding mmap_def[abs_def] proof(rule ext)
fix b1
let ?K = "{a. p1 a = b1 \<and> 0 < M a}"
show "setsum M ?K = N1 b1"
proof(cases "b1 \<in> supp N1")
case False
hence "?K = {}" using sM(2) by auto
thus ?thesis using False by auto
next
case True
def c \<equiv> "f1 b1"
have c: "c \<in> supp P" and b1: "b1 \<in> set1 c"
unfolding set1_def c_def P1 using True by (auto simp: mmap_image)
have "setsum M ?K = setsum M {a. p1 a = b1 \<and> a \<in> SET}"
apply(rule setsum_mono_zero_cong_left) unfolding M_def by auto
also have "... = setsum M ((\<lambda> b2. u c b1 b2) ` (set2 c))"
apply(rule setsum_cong) using c b1 proof safe
fix a assume p1a: "p1 a \<in> set1 c" and "0 < P c" and "a \<in> SET"
hence ac: "a \<in> sset c" using p1_rev by auto
hence "a = u c (p1 a) (p2 a)" using c by auto
moreover have "p2 a \<in> set2 c" using ac c by auto
ultimately show "a \<in> u c (p1 a) ` set2 c" by auto
next
fix b2 assume b1: "b1 \<in> set1 c" and b2: "b2 \<in> set2 c"
hence "u c b1 b2 \<in> SET" using c by auto
qed auto
also have "... = setsum (\<lambda> b2. M (u c b1 b2)) (set2 c)"
unfolding comp_def[symmetric] apply(rule setsum_reindex)
using inj unfolding inj_on_def inj2_def using b1 c u(3) by blast
also have "... = N1 b1" unfolding ss1[OF c b1, symmetric]
apply(rule setsum_cong[OF refl]) unfolding M_def
using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1] by fastforce
finally show ?thesis .
qed
qed
next
show "mmap p2 M = N2"
unfolding mmap_def[abs_def] proof(rule ext)
fix b2
let ?K = "{a. p2 a = b2 \<and> 0 < M a}"
show "setsum M ?K = N2 b2"
proof(cases "b2 \<in> supp N2")
case False
hence "?K = {}" using sM(3) by auto
thus ?thesis using False by auto
next
case True
def c \<equiv> "f2 b2"
have c: "c \<in> supp P" and b2: "b2 \<in> set2 c"
unfolding set2_def c_def P2 using True by (auto simp: mmap_image)
have "setsum M ?K = setsum M {a. p2 a = b2 \<and> a \<in> SET}"
apply(rule setsum_mono_zero_cong_left) unfolding M_def by auto
also have "... = setsum M ((\<lambda> b1. u c b1 b2) ` (set1 c))"
apply(rule setsum_cong) using c b2 proof safe
fix a assume p2a: "p2 a \<in> set2 c" and "0 < P c" and "a \<in> SET"
hence ac: "a \<in> sset c" using p2_rev by auto
hence "a = u c (p1 a) (p2 a)" using c by auto
moreover have "p1 a \<in> set1 c" using ac c by auto
ultimately show "a \<in> (\<lambda>b1. u c b1 (p2 a)) ` set1 c" by auto
next
fix b2 assume b1: "b1 \<in> set1 c" and b2: "b2 \<in> set2 c"
hence "u c b1 b2 \<in> SET" using c by auto
qed auto
also have "... = setsum (M o (\<lambda> b1. u c b1 b2)) (set1 c)"
apply(rule setsum_reindex)
using inj unfolding inj_on_def inj2_def using b2 c u(2) by blast
also have "... = setsum (\<lambda> b1. M (u c b1 b2)) (set1 c)"
unfolding comp_def[symmetric] by simp
also have "... = N2 b2" unfolding ss2[OF c b2, symmetric]
apply(rule setsum_cong[OF refl]) unfolding M_def set2_def
using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2]
unfolding set1_def by fastforce
finally show ?thesis .
qed
qed
qed
qed
definition mset_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
"mset_map h = Abs_multiset \<circ> mmap h \<circ> count"
bnf_def mset = mset_map [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"]
unfolding mset_map_def
proof -
show "Abs_multiset \<circ> mmap id \<circ> count = id" unfolding mmap_id by (auto simp: count_inverse)
next
fix f g
show "Abs_multiset \<circ> mmap (g \<circ> f) \<circ> count =
Abs_multiset \<circ> mmap g \<circ> count \<circ> (Abs_multiset \<circ> mmap f \<circ> count)"
unfolding comp_def apply(rule ext)
by (auto simp: Abs_multiset_inverse count mmap_comp1 mmap)
next
fix M f g assume eq: "\<And>a. a \<in> set_of M \<Longrightarrow> f a = g a"
thus "(Abs_multiset \<circ> mmap f \<circ> count) M = (Abs_multiset \<circ> mmap g \<circ> count) M" apply auto
unfolding cIm_def[abs_def] image_def
by (auto intro!: mmap_cong simp: Abs_multiset_inject count mmap)
next
fix f show "set_of \<circ> (Abs_multiset \<circ> mmap f \<circ> count) = op ` f \<circ> set_of"
by (auto simp: count mmap mmap_image set_of_Abs_multiset supp_count)
next
show "card_order natLeq" by (rule natLeq_card_order)
next
show "cinfinite natLeq" by (rule natLeq_cinfinite)
next
fix M show "|set_of M| \<le>o natLeq"
apply(rule ordLess_imp_ordLeq)
unfolding finite_iff_ordLess_natLeq[symmetric] using finite_set_of .
next
fix A :: "'a set"
have "|{M. set_of M \<subseteq> A}| \<le>o |{as. set as \<subseteq> A}|" using card_of_set_of .
also have "|{as. set as \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq"
by (rule list_in_bd)
finally show "|{M. set_of M \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" .
next
fix A B1 B2 f1 f2 p1 p2
let ?map = "\<lambda> f. Abs_multiset \<circ> mmap f \<circ> count"
assume wp: "wpull A B1 B2 f1 f2 p1 p2"
show "wpull {x. set_of x \<subseteq> A} {x. set_of x \<subseteq> B1} {x. set_of x \<subseteq> B2}
(?map f1) (?map f2) (?map p1) (?map p2)"
unfolding wpull_def proof safe
fix y1 y2
assume y1: "set_of y1 \<subseteq> B1" and y2: "set_of y2 \<subseteq> B2"
and m: "?map f1 y1 = ?map f2 y2"
def N1 \<equiv> "count y1" def N2 \<equiv> "count y2"
have "N1 \<in> multiset \<and> supp N1 \<subseteq> B1" and "N2 \<in> multiset \<and> supp N2 \<subseteq> B2"
and "mmap f1 N1 = mmap f2 N2"
using y1 y2 m unfolding N1_def N2_def
by (auto simp: Abs_multiset_inject count mmap)
then obtain M where M: "M \<in> multiset \<and> supp M \<subseteq> A"
and N1: "mmap p1 M = N1" and N2: "mmap p2 M = N2"
using wp_mmap[OF wp] unfolding wpull_def by auto
def x \<equiv> "Abs_multiset M"
show "\<exists>x\<in>{x. set_of x \<subseteq> A}. ?map p1 x = y1 \<and> ?map p2 x = y2"
apply(intro bexI[of _ x]) using M N1 N2 unfolding N1_def N2_def x_def
by (auto simp: count_inverse Abs_multiset_inverse)
qed
qed (unfold set_of_empty, auto)
end