src/HOL/Codatatype/Basic_BNFs.thy
author blanchet
Tue Aug 28 17:16:00 2012 +0200 (2012-08-28)
changeset 48975 7f79f94a432c
child 48979 b62d14275b89
permissions -rw-r--r--
added new (co)datatype package + theories of ordinals and cardinals (with Dmitriy and Andrei)
blanchet@48975
     1
(*  Title:      HOL/Codatatype/Basic_BNFs.thy
blanchet@48975
     2
    Author:     Dmitriy Traytel, TU Muenchen
blanchet@48975
     3
    Author:     Andrei Popescu, TU Muenchen
blanchet@48975
     4
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@48975
     5
    Copyright   2012
blanchet@48975
     6
blanchet@48975
     7
Registration of various types as bounded natural functors.
blanchet@48975
     8
*)
blanchet@48975
     9
blanchet@48975
    10
header {* Registration of Various Types as Bounded Natural Functors *}
blanchet@48975
    11
blanchet@48975
    12
theory Basic_BNFs
blanchet@48975
    13
imports BNF_Def "~~/src/HOL/Quotient_Examples/FSet"
blanchet@48975
    14
        "~~/src/HOL/Library/Multiset" Countable_Set
blanchet@48975
    15
begin
blanchet@48975
    16
blanchet@48975
    17
lemmas natLeq_card_order = natLeq_Card_order[unfolded Field_natLeq]
blanchet@48975
    18
blanchet@48975
    19
lemma ctwo_card_order: "card_order ctwo"
blanchet@48975
    20
using Card_order_ctwo by (unfold ctwo_def Field_card_of)
blanchet@48975
    21
blanchet@48975
    22
lemma natLeq_cinfinite: "cinfinite natLeq"
blanchet@48975
    23
unfolding cinfinite_def Field_natLeq by (rule nat_infinite)
blanchet@48975
    24
blanchet@48975
    25
bnf_def ID = "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b" ["\<lambda>x. {x}"] "\<lambda>_:: 'a. natLeq" ["id :: 'a \<Rightarrow> 'a"]
blanchet@48975
    26
apply auto
blanchet@48975
    27
apply (rule natLeq_card_order)
blanchet@48975
    28
apply (rule natLeq_cinfinite)
blanchet@48975
    29
apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
blanchet@48975
    30
apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)
blanchet@48975
    31
apply (rule ordLeq_transitive)
blanchet@48975
    32
apply (rule ordLeq_cexp1[of natLeq])
blanchet@48975
    33
apply (rule Cinfinite_Cnotzero)
blanchet@48975
    34
apply (rule conjI)
blanchet@48975
    35
apply (rule natLeq_cinfinite)
blanchet@48975
    36
apply (rule natLeq_Card_order)
blanchet@48975
    37
apply (rule card_of_Card_order)
blanchet@48975
    38
apply (rule cexp_mono1)
blanchet@48975
    39
apply (rule ordLeq_csum1)
blanchet@48975
    40
apply (rule card_of_Card_order)
blanchet@48975
    41
apply (rule disjI2)
blanchet@48975
    42
apply (rule cone_ordLeq_cexp)
blanchet@48975
    43
apply (rule ordLeq_transitive)
blanchet@48975
    44
apply (rule cone_ordLeq_ctwo)
blanchet@48975
    45
apply (rule ordLeq_csum2)
blanchet@48975
    46
apply (rule Card_order_ctwo)
blanchet@48975
    47
apply (rule natLeq_Card_order)
blanchet@48975
    48
done
blanchet@48975
    49
blanchet@48975
    50
lemma ID_pred[simp]: "ID_pred \<phi> = \<phi>"
blanchet@48975
    51
unfolding ID_pred_def ID_rel_def Gr_def fun_eq_iff by auto
blanchet@48975
    52
blanchet@48975
    53
bnf_def DEADID = "id :: 'a \<Rightarrow> 'a" [] "\<lambda>_:: 'a. natLeq +c |UNIV :: 'a set|" ["SOME x :: 'a. True"]
blanchet@48975
    54
apply (auto simp add: wpull_id)
blanchet@48975
    55
apply (rule card_order_csum)
blanchet@48975
    56
apply (rule natLeq_card_order)
blanchet@48975
    57
apply (rule card_of_card_order_on)
blanchet@48975
    58
apply (rule cinfinite_csum)
blanchet@48975
    59
apply (rule disjI1)
blanchet@48975
    60
apply (rule natLeq_cinfinite)
blanchet@48975
    61
apply (rule ordLess_imp_ordLeq)
blanchet@48975
    62
apply (rule ordLess_ordLeq_trans)
blanchet@48975
    63
apply (rule ordLess_ctwo_cexp)
blanchet@48975
    64
apply (rule card_of_Card_order)
blanchet@48975
    65
apply (rule cexp_mono2'')
blanchet@48975
    66
apply (rule ordLeq_csum2)
blanchet@48975
    67
apply (rule card_of_Card_order)
blanchet@48975
    68
apply (rule ctwo_Cnotzero)
blanchet@48975
    69
by (rule card_of_Card_order)
blanchet@48975
    70
blanchet@48975
    71
lemma DEADID_pred[simp]: "DEADID_pred = (op =)"
blanchet@48975
    72
unfolding DEADID_pred_def DEADID.rel_Id by simp
blanchet@48975
    73
blanchet@48975
    74
ML {*
blanchet@48975
    75
blanchet@48975
    76
signature BASIC_BNFS =
blanchet@48975
    77
sig
blanchet@48975
    78
  val ID_bnf: BNF_Def.BNF
blanchet@48975
    79
  val ID_rel_def: thm
blanchet@48975
    80
  val ID_pred_def: thm
blanchet@48975
    81
blanchet@48975
    82
  val DEADID_bnf: BNF_Def.BNF
blanchet@48975
    83
end;
blanchet@48975
    84
blanchet@48975
    85
structure Basic_BNFs : BASIC_BNFS =
blanchet@48975
    86
struct
blanchet@48975
    87
blanchet@48975
    88
  val ID_bnf = the (BNF_Def.bnf_of @{context} "ID");
blanchet@48975
    89
  val DEADID_bnf = the (BNF_Def.bnf_of @{context} "DEADID");
blanchet@48975
    90
blanchet@48975
    91
  val rel_def = BNF_Def.rel_def_of_bnf ID_bnf;
blanchet@48975
    92
  val ID_rel_def = rel_def RS sym;
blanchet@48975
    93
  val ID_pred_def =
blanchet@48975
    94
    Local_Defs.unfold @{context} [rel_def] (BNF_Def.pred_def_of_bnf ID_bnf) RS sym;
blanchet@48975
    95
blanchet@48975
    96
end;
blanchet@48975
    97
*}
blanchet@48975
    98
blanchet@48975
    99
definition sum_setl :: "'a + 'b \<Rightarrow> 'a set" where
blanchet@48975
   100
"sum_setl x = (case x of Inl z => {z} | _ => {})"
blanchet@48975
   101
blanchet@48975
   102
definition sum_setr :: "'a + 'b \<Rightarrow> 'b set" where
blanchet@48975
   103
"sum_setr x = (case x of Inr z => {z} | _ => {})"
blanchet@48975
   104
blanchet@48975
   105
lemmas sum_set_defs = sum_setl_def[abs_def] sum_setr_def[abs_def]
blanchet@48975
   106
blanchet@48975
   107
bnf_def sum = sum_map [sum_setl, sum_setr] "\<lambda>_::'a + 'b. natLeq" [Inl, Inr]
blanchet@48975
   108
proof -
blanchet@48975
   109
  show "sum_map id id = id" by (rule sum_map.id)
blanchet@48975
   110
next
blanchet@48975
   111
  fix f1 f2 g1 g2
blanchet@48975
   112
  show "sum_map (g1 o f1) (g2 o f2) = sum_map g1 g2 o sum_map f1 f2"
blanchet@48975
   113
    by (rule sum_map.comp[symmetric])
blanchet@48975
   114
next
blanchet@48975
   115
  fix x f1 f2 g1 g2
blanchet@48975
   116
  assume a1: "\<And>z. z \<in> sum_setl x \<Longrightarrow> f1 z = g1 z" and
blanchet@48975
   117
         a2: "\<And>z. z \<in> sum_setr x \<Longrightarrow> f2 z = g2 z"
blanchet@48975
   118
  thus "sum_map f1 f2 x = sum_map g1 g2 x"
blanchet@48975
   119
  proof (cases x)
blanchet@48975
   120
    case Inl thus ?thesis using a1 by (clarsimp simp: sum_setl_def)
blanchet@48975
   121
  next
blanchet@48975
   122
    case Inr thus ?thesis using a2 by (clarsimp simp: sum_setr_def)
blanchet@48975
   123
  qed
blanchet@48975
   124
next
blanchet@48975
   125
  fix f1 f2
blanchet@48975
   126
  show "sum_setl o sum_map f1 f2 = image f1 o sum_setl"
blanchet@48975
   127
    by (rule ext, unfold o_apply) (simp add: sum_setl_def split: sum.split)
blanchet@48975
   128
next
blanchet@48975
   129
  fix f1 f2
blanchet@48975
   130
  show "sum_setr o sum_map f1 f2 = image f2 o sum_setr"
blanchet@48975
   131
    by (rule ext, unfold o_apply) (simp add: sum_setr_def split: sum.split)
blanchet@48975
   132
next
blanchet@48975
   133
  show "card_order natLeq" by (rule natLeq_card_order)
blanchet@48975
   134
next
blanchet@48975
   135
  show "cinfinite natLeq" by (rule natLeq_cinfinite)
blanchet@48975
   136
next
blanchet@48975
   137
  fix x
blanchet@48975
   138
  show "|sum_setl x| \<le>o natLeq"
blanchet@48975
   139
    apply (rule ordLess_imp_ordLeq)
blanchet@48975
   140
    apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
blanchet@48975
   141
    by (simp add: sum_setl_def split: sum.split)
blanchet@48975
   142
next
blanchet@48975
   143
  fix x
blanchet@48975
   144
  show "|sum_setr x| \<le>o natLeq"
blanchet@48975
   145
    apply (rule ordLess_imp_ordLeq)
blanchet@48975
   146
    apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
blanchet@48975
   147
    by (simp add: sum_setr_def split: sum.split)
blanchet@48975
   148
next
blanchet@48975
   149
  fix A1 :: "'a set" and A2 :: "'b set"
blanchet@48975
   150
  have in_alt: "{x. (case x of Inl z => {z} | _ => {}) \<subseteq> A1 \<and>
blanchet@48975
   151
    (case x of Inr z => {z} | _ => {}) \<subseteq> A2} = A1 <+> A2" (is "?L = ?R")
blanchet@48975
   152
  proof safe
blanchet@48975
   153
    fix x :: "'a + 'b"
blanchet@48975
   154
    assume "(case x of Inl z \<Rightarrow> {z} | _ \<Rightarrow> {}) \<subseteq> A1" "(case x of Inr z \<Rightarrow> {z} | _ \<Rightarrow> {}) \<subseteq> A2"
blanchet@48975
   155
    hence "x \<in> Inl ` A1 \<or> x \<in> Inr ` A2" by (cases x) simp+
blanchet@48975
   156
    thus "x \<in> A1 <+> A2" by blast
blanchet@48975
   157
  qed (auto split: sum.split)
blanchet@48975
   158
  show "|{x. sum_setl x \<subseteq> A1 \<and> sum_setr x \<subseteq> A2}| \<le>o
blanchet@48975
   159
    (( |A1| +c |A2| ) +c ctwo) ^c natLeq"
blanchet@48975
   160
    apply (rule ordIso_ordLeq_trans)
blanchet@48975
   161
    apply (rule card_of_ordIso_subst)
blanchet@48975
   162
    apply (unfold sum_set_defs)
blanchet@48975
   163
    apply (rule in_alt)
blanchet@48975
   164
    apply (rule ordIso_ordLeq_trans)
blanchet@48975
   165
    apply (rule Plus_csum)
blanchet@48975
   166
    apply (rule ordLeq_transitive)
blanchet@48975
   167
    apply (rule ordLeq_csum1)
blanchet@48975
   168
    apply (rule Card_order_csum)
blanchet@48975
   169
    apply (rule ordLeq_cexp1)
blanchet@48975
   170
    apply (rule conjI)
blanchet@48975
   171
    using Field_natLeq UNIV_not_empty czeroE apply fast
blanchet@48975
   172
    apply (rule natLeq_Card_order)
blanchet@48975
   173
    by (rule Card_order_csum)
blanchet@48975
   174
next
blanchet@48975
   175
  fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22
blanchet@48975
   176
  assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22"
blanchet@48975
   177
  hence
blanchet@48975
   178
    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"
blanchet@48975
   179
    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"
blanchet@48975
   180
    unfolding wpull_def by blast+
blanchet@48975
   181
  show "wpull {x. sum_setl x \<subseteq> A1 \<and> sum_setr x \<subseteq> A2}
blanchet@48975
   182
  {x. sum_setl x \<subseteq> B11 \<and> sum_setr x \<subseteq> B12} {x. sum_setl x \<subseteq> B21 \<and> sum_setr x \<subseteq> B22}
blanchet@48975
   183
  (sum_map f11 f12) (sum_map f21 f22) (sum_map p11 p12) (sum_map p21 p22)"
blanchet@48975
   184
    (is "wpull ?in ?in1 ?in2 ?mapf1 ?mapf2 ?mapp1 ?mapp2")
blanchet@48975
   185
  proof (unfold wpull_def)
blanchet@48975
   186
    { fix B1 B2
blanchet@48975
   187
      assume *: "B1 \<in> ?in1" "B2 \<in> ?in2" "?mapf1 B1 = ?mapf2 B2"
blanchet@48975
   188
      have "\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2"
blanchet@48975
   189
      proof (cases B1)
blanchet@48975
   190
        case (Inl b1)
blanchet@48975
   191
        { fix b2 assume "B2 = Inr b2"
blanchet@48975
   192
          with Inl *(3) have False by simp
blanchet@48975
   193
        } then obtain b2 where Inl': "B2 = Inl b2" by (cases B2) (simp, blast)
blanchet@48975
   194
        with Inl * have "b1 \<in> B11" "b2 \<in> B21" "f11 b1 = f21 b2"
blanchet@48975
   195
        by (simp add: sum_setl_def)+
blanchet@48975
   196
        with pull1 obtain a where "a \<in> A1" "p11 a = b1" "p21 a = b2" by blast+
blanchet@48975
   197
        with Inl Inl' have "Inl a \<in> ?in" "?mapp1 (Inl a) = B1 \<and> ?mapp2 (Inl a) = B2"
blanchet@48975
   198
        by (simp add: sum_set_defs)+
blanchet@48975
   199
        thus ?thesis by blast
blanchet@48975
   200
      next
blanchet@48975
   201
        case (Inr b1)
blanchet@48975
   202
        { fix b2 assume "B2 = Inl b2"
blanchet@48975
   203
          with Inr *(3) have False by simp
blanchet@48975
   204
        } then obtain b2 where Inr': "B2 = Inr b2" by (cases B2) (simp, blast)
blanchet@48975
   205
        with Inr * have "b1 \<in> B12" "b2 \<in> B22" "f12 b1 = f22 b2"
blanchet@48975
   206
        by (simp add: sum_set_defs)+
blanchet@48975
   207
        with pull2 obtain a where "a \<in> A2" "p12 a = b1" "p22 a = b2" by blast+
blanchet@48975
   208
        with Inr Inr' have "Inr a \<in> ?in" "?mapp1 (Inr a) = B1 \<and> ?mapp2 (Inr a) = B2"
blanchet@48975
   209
        by (simp add: sum_set_defs)+
blanchet@48975
   210
        thus ?thesis by blast
blanchet@48975
   211
      qed
blanchet@48975
   212
    }
blanchet@48975
   213
    thus "\<forall>B1 B2. B1 \<in> ?in1 \<and> B2 \<in> ?in2 \<and> ?mapf1 B1 = ?mapf2 B2 \<longrightarrow>
blanchet@48975
   214
      (\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2)" by fastforce
blanchet@48975
   215
  qed
blanchet@48975
   216
qed (auto simp: sum_set_defs)
blanchet@48975
   217
blanchet@48975
   218
lemma sum_pred[simp]:
blanchet@48975
   219
  "sum_pred \<phi> \<psi> x y =
blanchet@48975
   220
    (case x of Inl a1 \<Rightarrow> (case y of Inl a2 \<Rightarrow> \<phi> a1 a2 | Inr _ \<Rightarrow> False)
blanchet@48975
   221
             | Inr b1 \<Rightarrow> (case y of Inl _ \<Rightarrow> False | Inr b2 \<Rightarrow> \<psi> b1 b2))"
blanchet@48975
   222
unfolding sum_setl_def sum_setr_def sum_pred_def sum_rel_def Gr_def relcomp_unfold converse_unfold
blanchet@48975
   223
by (fastforce split: sum.splits)+
blanchet@48975
   224
blanchet@48975
   225
lemma singleton_ordLeq_ctwo_natLeq: "|{x}| \<le>o ctwo *c natLeq"
blanchet@48975
   226
  apply (rule ordLeq_transitive)
blanchet@48975
   227
  apply (rule ordLeq_cprod2)
blanchet@48975
   228
  apply (rule ctwo_Cnotzero)
blanchet@48975
   229
  apply (auto simp: Field_card_of intro: card_of_card_order_on)
blanchet@48975
   230
  apply (rule cprod_mono2)
blanchet@48975
   231
  apply (rule ordLess_imp_ordLeq)
blanchet@48975
   232
  apply (unfold finite_iff_ordLess_natLeq[symmetric])
blanchet@48975
   233
  by simp
blanchet@48975
   234
blanchet@48975
   235
definition fsts :: "'a \<times> 'b \<Rightarrow> 'a set" where
blanchet@48975
   236
"fsts x = {fst x}"
blanchet@48975
   237
blanchet@48975
   238
definition snds :: "'a \<times> 'b \<Rightarrow> 'b set" where
blanchet@48975
   239
"snds x = {snd x}"
blanchet@48975
   240
blanchet@48975
   241
lemmas prod_set_defs = fsts_def[abs_def] snds_def[abs_def]
blanchet@48975
   242
blanchet@48975
   243
bnf_def prod = map_pair [fsts, snds] "\<lambda>_::'a \<times> 'b. ctwo *c natLeq" [Pair]
blanchet@48975
   244
proof (unfold prod_set_defs)
blanchet@48975
   245
  show "map_pair id id = id" by (rule map_pair.id)
blanchet@48975
   246
next
blanchet@48975
   247
  fix f1 f2 g1 g2
blanchet@48975
   248
  show "map_pair (g1 o f1) (g2 o f2) = map_pair g1 g2 o map_pair f1 f2"
blanchet@48975
   249
    by (rule map_pair.comp[symmetric])
blanchet@48975
   250
next
blanchet@48975
   251
  fix x f1 f2 g1 g2
blanchet@48975
   252
  assume "\<And>z. z \<in> {fst x} \<Longrightarrow> f1 z = g1 z" "\<And>z. z \<in> {snd x} \<Longrightarrow> f2 z = g2 z"
blanchet@48975
   253
  thus "map_pair f1 f2 x = map_pair g1 g2 x" by (cases x) simp
blanchet@48975
   254
next
blanchet@48975
   255
  fix f1 f2
blanchet@48975
   256
  show "(\<lambda>x. {fst x}) o map_pair f1 f2 = image f1 o (\<lambda>x. {fst x})"
blanchet@48975
   257
    by (rule ext, unfold o_apply) simp
blanchet@48975
   258
next
blanchet@48975
   259
  fix f1 f2
blanchet@48975
   260
  show "(\<lambda>x. {snd x}) o map_pair f1 f2 = image f2 o (\<lambda>x. {snd x})"
blanchet@48975
   261
    by (rule ext, unfold o_apply) simp
blanchet@48975
   262
next
blanchet@48975
   263
  show "card_order (ctwo *c natLeq)"
blanchet@48975
   264
    apply (rule card_order_cprod)
blanchet@48975
   265
    apply (rule ctwo_card_order)
blanchet@48975
   266
    by (rule natLeq_card_order)
blanchet@48975
   267
next
blanchet@48975
   268
  show "cinfinite (ctwo *c natLeq)"
blanchet@48975
   269
    apply (rule cinfinite_cprod2)
blanchet@48975
   270
    apply (rule ctwo_Cnotzero)
blanchet@48975
   271
    apply (rule conjI[OF _ natLeq_Card_order])
blanchet@48975
   272
    by (rule natLeq_cinfinite)
blanchet@48975
   273
next
blanchet@48975
   274
  fix x
blanchet@48975
   275
  show "|{fst x}| \<le>o ctwo *c natLeq"
blanchet@48975
   276
    by (rule singleton_ordLeq_ctwo_natLeq)
blanchet@48975
   277
next
blanchet@48975
   278
  fix x
blanchet@48975
   279
  show "|{snd x}| \<le>o ctwo *c natLeq"
blanchet@48975
   280
    by (rule singleton_ordLeq_ctwo_natLeq)
blanchet@48975
   281
next
blanchet@48975
   282
  fix A1 :: "'a set" and A2 :: "'b set"
blanchet@48975
   283
  have in_alt: "{x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2} = A1 \<times> A2" by auto
blanchet@48975
   284
  show "|{x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2}| \<le>o
blanchet@48975
   285
    ( ( |A1| +c |A2| ) +c ctwo) ^c (ctwo *c natLeq)"
blanchet@48975
   286
    apply (rule ordIso_ordLeq_trans)
blanchet@48975
   287
    apply (rule card_of_ordIso_subst)
blanchet@48975
   288
    apply (rule in_alt)
blanchet@48975
   289
    apply (rule ordIso_ordLeq_trans)
blanchet@48975
   290
    apply (rule Times_cprod)
blanchet@48975
   291
    apply (rule ordLeq_transitive)
blanchet@48975
   292
    apply (rule cprod_csum_cexp)
blanchet@48975
   293
    apply (rule cexp_mono)
blanchet@48975
   294
    apply (rule ordLeq_csum1)
blanchet@48975
   295
    apply (rule Card_order_csum)
blanchet@48975
   296
    apply (rule ordLeq_cprod1)
blanchet@48975
   297
    apply (rule Card_order_ctwo)
blanchet@48975
   298
    apply (rule Cinfinite_Cnotzero)
blanchet@48975
   299
    apply (rule conjI[OF _ natLeq_Card_order])
blanchet@48975
   300
    apply (rule natLeq_cinfinite)
blanchet@48975
   301
    apply (rule disjI2)
blanchet@48975
   302
    apply (rule cone_ordLeq_cexp)
blanchet@48975
   303
    apply (rule ordLeq_transitive)
blanchet@48975
   304
    apply (rule cone_ordLeq_ctwo)
blanchet@48975
   305
    apply (rule ordLeq_csum2)
blanchet@48975
   306
    apply (rule Card_order_ctwo)
blanchet@48975
   307
    apply (rule notE)
blanchet@48975
   308
    apply (rule ctwo_not_czero)
blanchet@48975
   309
    apply assumption
blanchet@48975
   310
    by (rule Card_order_ctwo)
blanchet@48975
   311
next
blanchet@48975
   312
  fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22
blanchet@48975
   313
  assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22"
blanchet@48975
   314
  thus "wpull {x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2}
blanchet@48975
   315
    {x. {fst x} \<subseteq> B11 \<and> {snd x} \<subseteq> B12} {x. {fst x} \<subseteq> B21 \<and> {snd x} \<subseteq> B22}
blanchet@48975
   316
   (map_pair f11 f12) (map_pair f21 f22) (map_pair p11 p12) (map_pair p21 p22)"
blanchet@48975
   317
    unfolding wpull_def by simp fast
blanchet@48975
   318
qed simp+
blanchet@48975
   319
blanchet@48975
   320
lemma prod_pred[simp]:
blanchet@48975
   321
"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))"
blanchet@48975
   322
unfolding prod_set_defs prod_pred_def prod_rel_def Gr_def relcomp_unfold converse_unfold by auto
blanchet@48975
   323
(* TODO: pred characterization for each basic BNF *)
blanchet@48975
   324
blanchet@48975
   325
(* Categorical version of pullback: *)
blanchet@48975
   326
lemma wpull_cat:
blanchet@48975
   327
assumes p: "wpull A B1 B2 f1 f2 p1 p2"
blanchet@48975
   328
and c: "f1 o q1 = f2 o q2"
blanchet@48975
   329
and r: "range q1 \<subseteq> B1" "range q2 \<subseteq> B2"
blanchet@48975
   330
obtains h where "range h \<subseteq> A \<and> q1 = p1 o h \<and> q2 = p2 o h"
blanchet@48975
   331
proof-
blanchet@48975
   332
  have *: "\<forall>d. \<exists>a \<in> A. p1 a = q1 d & p2 a = q2 d"
blanchet@48975
   333
  proof safe
blanchet@48975
   334
    fix d
blanchet@48975
   335
    have "f1 (q1 d) = f2 (q2 d)" using c unfolding comp_def[abs_def] by (rule fun_cong)
blanchet@48975
   336
    moreover
blanchet@48975
   337
    have "q1 d : B1" "q2 d : B2" using r unfolding image_def by auto
blanchet@48975
   338
    ultimately show "\<exists>a \<in> A. p1 a = q1 d \<and> p2 a = q2 d"
blanchet@48975
   339
      using p unfolding wpull_def by auto
blanchet@48975
   340
  qed
blanchet@48975
   341
  then obtain h where "!! d. h d \<in> A & p1 (h d) = q1 d & p2 (h d) = q2 d" by metis
blanchet@48975
   342
  thus ?thesis using that by fastforce
blanchet@48975
   343
qed
blanchet@48975
   344
blanchet@48975
   345
lemma card_of_bounded_range:
blanchet@48975
   346
  "|{f :: 'd \<Rightarrow> 'a. range f \<subseteq> B}| \<le>o |Func (UNIV :: 'd set) B|" (is "|?LHS| \<le>o |?RHS|")
blanchet@48975
   347
proof -
blanchet@48975
   348
  let ?f = "\<lambda>f. %x. if f x \<in> B then Some (f x) else None"
blanchet@48975
   349
  have "inj_on ?f ?LHS" unfolding inj_on_def
blanchet@48975
   350
  proof (unfold fun_eq_iff, safe)
blanchet@48975
   351
    fix g :: "'d \<Rightarrow> 'a" and f :: "'d \<Rightarrow> 'a" and x
blanchet@48975
   352
    assume "range f \<subseteq> B" "range g \<subseteq> B" and eq: "\<forall>x. ?f f x = ?f g x"
blanchet@48975
   353
    hence "f x \<in> B" "g x \<in> B" by auto
blanchet@48975
   354
    with eq have "Some (f x) = Some (g x)" by metis
blanchet@48975
   355
    thus "f x = g x" by simp
blanchet@48975
   356
  qed
blanchet@48975
   357
  moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Func_def by fastforce
blanchet@48975
   358
  ultimately show ?thesis using card_of_ordLeq by fast
blanchet@48975
   359
qed
blanchet@48975
   360
blanchet@48975
   361
bnf_def "fun" = "op \<circ>" [range] "\<lambda>_:: 'a \<Rightarrow> 'b. natLeq +c |UNIV :: 'a set|"
blanchet@48975
   362
  ["%c x::'b::type. c::'a::type"]
blanchet@48975
   363
proof
blanchet@48975
   364
  fix f show "id \<circ> f = id f" by simp
blanchet@48975
   365
next
blanchet@48975
   366
  fix f g show "op \<circ> (g \<circ> f) = op \<circ> g \<circ> op \<circ> f"
blanchet@48975
   367
  unfolding comp_def[abs_def] ..
blanchet@48975
   368
next
blanchet@48975
   369
  fix x f g
blanchet@48975
   370
  assume "\<And>z. z \<in> range x \<Longrightarrow> f z = g z"
blanchet@48975
   371
  thus "f \<circ> x = g \<circ> x" by auto
blanchet@48975
   372
next
blanchet@48975
   373
  fix f show "range \<circ> op \<circ> f = op ` f \<circ> range"
blanchet@48975
   374
  unfolding image_def comp_def[abs_def] by auto
blanchet@48975
   375
next
blanchet@48975
   376
  show "card_order (natLeq +c |UNIV| )" (is "_ (_ +c ?U)")
blanchet@48975
   377
  apply (rule card_order_csum)
blanchet@48975
   378
  apply (rule natLeq_card_order)
blanchet@48975
   379
  by (rule card_of_card_order_on)
blanchet@48975
   380
(*  *)
blanchet@48975
   381
  show "cinfinite (natLeq +c ?U)"
blanchet@48975
   382
    apply (rule cinfinite_csum)
blanchet@48975
   383
    apply (rule disjI1)
blanchet@48975
   384
    by (rule natLeq_cinfinite)
blanchet@48975
   385
next
blanchet@48975
   386
  fix f :: "'d => 'a"
blanchet@48975
   387
  have "|range f| \<le>o | (UNIV::'d set) |" (is "_ \<le>o ?U") by (rule card_of_image)
blanchet@48975
   388
  also have "?U \<le>o natLeq +c ?U"  by (rule ordLeq_csum2) (rule card_of_Card_order)
blanchet@48975
   389
  finally show "|range f| \<le>o natLeq +c ?U" .
blanchet@48975
   390
next
blanchet@48975
   391
  fix B :: "'a set"
blanchet@48975
   392
  have "|{f::'d => 'a. range f \<subseteq> B}| \<le>o |Func (UNIV :: 'd set) B|" by (rule card_of_bounded_range)
blanchet@48975
   393
  also have "|Func (UNIV :: 'd set) B| =o |B| ^c |UNIV :: 'd set|"
blanchet@48975
   394
    unfolding cexp_def Field_card_of by (rule card_of_refl)
blanchet@48975
   395
  also have "|B| ^c |UNIV :: 'd set| \<le>o
blanchet@48975
   396
             ( |B| +c ctwo) ^c (natLeq +c |UNIV :: 'd set| )"
blanchet@48975
   397
    apply (rule cexp_mono)
blanchet@48975
   398
     apply (rule ordLeq_csum1) apply (rule card_of_Card_order)
blanchet@48975
   399
     apply (rule ordLeq_csum2) apply (rule card_of_Card_order)
blanchet@48975
   400
     apply (rule disjI2) apply (rule cone_ordLeq_cexp)
blanchet@48975
   401
      apply (rule ordLeq_transitive) apply (rule cone_ordLeq_ctwo) apply (rule ordLeq_csum2)
blanchet@48975
   402
      apply (rule Card_order_ctwo)
blanchet@48975
   403
     apply (rule notE) apply (rule conjunct1) apply (rule Cnotzero_UNIV) apply blast
blanchet@48975
   404
     apply (rule card_of_Card_order)
blanchet@48975
   405
  done
blanchet@48975
   406
  finally
blanchet@48975
   407
  show "|{f::'d => 'a. range f \<subseteq> B}| \<le>o
blanchet@48975
   408
        ( |B| +c ctwo) ^c (natLeq +c |UNIV :: 'd set| )" .
blanchet@48975
   409
next
blanchet@48975
   410
  fix A B1 B2 f1 f2 p1 p2 assume p: "wpull A B1 B2 f1 f2 p1 p2"
blanchet@48975
   411
  show "wpull {h. range h \<subseteq> A} {g1. range g1 \<subseteq> B1} {g2. range g2 \<subseteq> B2}
blanchet@48975
   412
    (op \<circ> f1) (op \<circ> f2) (op \<circ> p1) (op \<circ> p2)"
blanchet@48975
   413
  unfolding wpull_def
blanchet@48975
   414
  proof safe
blanchet@48975
   415
    fix g1 g2 assume r: "range g1 \<subseteq> B1" "range g2 \<subseteq> B2"
blanchet@48975
   416
    and c: "f1 \<circ> g1 = f2 \<circ> g2"
blanchet@48975
   417
    show "\<exists>h \<in> {h. range h \<subseteq> A}. p1 \<circ> h = g1 \<and> p2 \<circ> h = g2"
blanchet@48975
   418
    using wpull_cat[OF p c r] by simp metis
blanchet@48975
   419
  qed
blanchet@48975
   420
qed auto
blanchet@48975
   421
blanchet@48975
   422
lemma fun_pred[simp]: "fun_pred \<phi> f g = (\<forall>x. \<phi> (f x) (g x))"
blanchet@48975
   423
unfolding fun_rel_def fun_pred_def Gr_def relcomp_unfold converse_unfold
blanchet@48975
   424
by (auto intro!: exI dest!: in_mono)
blanchet@48975
   425
blanchet@48975
   426
lemma card_of_list_in:
blanchet@48975
   427
  "|{xs. set xs \<subseteq> A}| \<le>o |Pfunc (UNIV :: nat set) A|" (is "|?LHS| \<le>o |?RHS|")
blanchet@48975
   428
proof -
blanchet@48975
   429
  let ?f = "%xs. %i. if i < length xs \<and> set xs \<subseteq> A then Some (nth xs i) else None"
blanchet@48975
   430
  have "inj_on ?f ?LHS" unfolding inj_on_def fun_eq_iff
blanchet@48975
   431
  proof safe
blanchet@48975
   432
    fix xs :: "'a list" and ys :: "'a list"
blanchet@48975
   433
    assume su: "set xs \<subseteq> A" "set ys \<subseteq> A" and eq: "\<forall>i. ?f xs i = ?f ys i"
blanchet@48975
   434
    hence *: "length xs = length ys"
blanchet@48975
   435
    by (metis linorder_cases option.simps(2) order_less_irrefl)
blanchet@48975
   436
    thus "xs = ys" by (rule nth_equalityI) (metis * eq su option.inject)
blanchet@48975
   437
  qed
blanchet@48975
   438
  moreover have "?f ` ?LHS \<subseteq> ?RHS" unfolding Pfunc_def by fastforce
blanchet@48975
   439
  ultimately show ?thesis using card_of_ordLeq by blast
blanchet@48975
   440
qed
blanchet@48975
   441
blanchet@48975
   442
lemma list_in_empty: "A = {} \<Longrightarrow> {x. set x \<subseteq> A} = {[]}"
blanchet@48975
   443
by simp
blanchet@48975
   444
blanchet@48975
   445
lemma card_of_Func: "|Func A B| =o |B| ^c |A|"
blanchet@48975
   446
unfolding cexp_def Field_card_of by (rule card_of_refl)
blanchet@48975
   447
blanchet@48975
   448
lemma not_emp_czero_notIn_ordIso_Card_order:
blanchet@48975
   449
"A \<noteq> {} \<Longrightarrow> ( |A|, czero) \<notin> ordIso \<and> Card_order |A|"
blanchet@48975
   450
  apply (rule conjI)
blanchet@48975
   451
  apply (metis Field_card_of czeroE)
blanchet@48975
   452
  by (rule card_of_Card_order)
blanchet@48975
   453
blanchet@48975
   454
lemma list_in_bd: "|{x. set x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq"
blanchet@48975
   455
proof -
blanchet@48975
   456
  fix A :: "'a set"
blanchet@48975
   457
  show "|{x. set x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq"
blanchet@48975
   458
  proof (cases "A = {}")
blanchet@48975
   459
    case False thus ?thesis
blanchet@48975
   460
      apply -
blanchet@48975
   461
      apply (rule ordLeq_transitive)
blanchet@48975
   462
      apply (rule card_of_list_in)
blanchet@48975
   463
      apply (rule ordLeq_transitive)
blanchet@48975
   464
      apply (erule card_of_Pfunc_Pow_Func)
blanchet@48975
   465
      apply (rule ordIso_ordLeq_trans)
blanchet@48975
   466
      apply (rule Times_cprod)
blanchet@48975
   467
      apply (rule cprod_cinfinite_bound)
blanchet@48975
   468
      apply (rule ordIso_ordLeq_trans)
blanchet@48975
   469
      apply (rule Pow_cexp_ctwo)
blanchet@48975
   470
      apply (rule ordIso_ordLeq_trans)
blanchet@48975
   471
      apply (rule cexp_cong2)
blanchet@48975
   472
      apply (rule card_of_nat)
blanchet@48975
   473
      apply (rule Card_order_ctwo)
blanchet@48975
   474
      apply (rule card_of_Card_order)
blanchet@48975
   475
      apply (rule natLeq_Card_order)
blanchet@48975
   476
      apply (rule disjI1)
blanchet@48975
   477
      apply (rule ctwo_Cnotzero)
blanchet@48975
   478
      apply (rule cexp_mono1)
blanchet@48975
   479
      apply (rule ordLeq_csum2)
blanchet@48975
   480
      apply (rule Card_order_ctwo)
blanchet@48975
   481
      apply (rule disjI1)
blanchet@48975
   482
      apply (rule ctwo_Cnotzero)
blanchet@48975
   483
      apply (rule natLeq_Card_order)
blanchet@48975
   484
      apply (rule ordIso_ordLeq_trans)
blanchet@48975
   485
      apply (rule card_of_Func)
blanchet@48975
   486
      apply (rule ordIso_ordLeq_trans)
blanchet@48975
   487
      apply (rule cexp_cong2)
blanchet@48975
   488
      apply (rule card_of_nat)
blanchet@48975
   489
      apply (rule card_of_Card_order)
blanchet@48975
   490
      apply (rule card_of_Card_order)
blanchet@48975
   491
      apply (rule natLeq_Card_order)
blanchet@48975
   492
      apply (rule disjI1)
blanchet@48975
   493
      apply (erule not_emp_czero_notIn_ordIso_Card_order)
blanchet@48975
   494
      apply (rule cexp_mono1)
blanchet@48975
   495
      apply (rule ordLeq_csum1)
blanchet@48975
   496
      apply (rule card_of_Card_order)
blanchet@48975
   497
      apply (rule disjI1)
blanchet@48975
   498
      apply (erule not_emp_czero_notIn_ordIso_Card_order)
blanchet@48975
   499
      apply (rule natLeq_Card_order)
blanchet@48975
   500
      apply (rule card_of_Card_order)
blanchet@48975
   501
      apply (rule card_of_Card_order)
blanchet@48975
   502
      apply (rule Cinfinite_cexp)
blanchet@48975
   503
      apply (rule ordLeq_csum2)
blanchet@48975
   504
      apply (rule Card_order_ctwo)
blanchet@48975
   505
      apply (rule conjI)
blanchet@48975
   506
      apply (rule natLeq_cinfinite)
blanchet@48975
   507
      by (rule natLeq_Card_order)
blanchet@48975
   508
  next
blanchet@48975
   509
    case True thus ?thesis
blanchet@48975
   510
      apply -
blanchet@48975
   511
      apply (rule ordIso_ordLeq_trans)
blanchet@48975
   512
      apply (rule card_of_ordIso_subst)
blanchet@48975
   513
      apply (erule list_in_empty)
blanchet@48975
   514
      apply (rule ordIso_ordLeq_trans)
blanchet@48975
   515
      apply (rule single_cone)
blanchet@48975
   516
      apply (rule cone_ordLeq_cexp)
blanchet@48975
   517
      apply (rule ordLeq_transitive)
blanchet@48975
   518
      apply (rule cone_ordLeq_ctwo)
blanchet@48975
   519
      apply (rule ordLeq_csum2)
blanchet@48975
   520
      by (rule Card_order_ctwo)
blanchet@48975
   521
  qed
blanchet@48975
   522
qed
blanchet@48975
   523
blanchet@48975
   524
bnf_def list = map [set] "\<lambda>_::'a list. natLeq" ["[]"]
blanchet@48975
   525
proof -
blanchet@48975
   526
  show "map id = id" by (rule List.map.id)
blanchet@48975
   527
next
blanchet@48975
   528
  fix f g
blanchet@48975
   529
  show "map (g o f) = map g o map f" by (rule List.map.comp[symmetric])
blanchet@48975
   530
next
blanchet@48975
   531
  fix x f g
blanchet@48975
   532
  assume "\<And>z. z \<in> set x \<Longrightarrow> f z = g z"
blanchet@48975
   533
  thus "map f x = map g x" by simp
blanchet@48975
   534
next
blanchet@48975
   535
  fix f
blanchet@48975
   536
  show "set o map f = image f o set" by (rule ext, unfold o_apply, rule set_map)
blanchet@48975
   537
next
blanchet@48975
   538
  show "card_order natLeq" by (rule natLeq_card_order)
blanchet@48975
   539
next
blanchet@48975
   540
  show "cinfinite natLeq" by (rule natLeq_cinfinite)
blanchet@48975
   541
next
blanchet@48975
   542
  fix x
blanchet@48975
   543
  show "|set x| \<le>o natLeq"
blanchet@48975
   544
    apply (rule ordLess_imp_ordLeq)
blanchet@48975
   545
    apply (rule finite_ordLess_infinite[OF _ natLeq_Well_order])
blanchet@48975
   546
    unfolding Field_natLeq Field_card_of by (auto simp: card_of_well_order_on)
blanchet@48975
   547
next
blanchet@48975
   548
  fix A :: "'a set"
blanchet@48975
   549
  show "|{x. set x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" by (rule list_in_bd)
blanchet@48975
   550
next
blanchet@48975
   551
  fix A B1 B2 f1 f2 p1 p2
blanchet@48975
   552
  assume "wpull A B1 B2 f1 f2 p1 p2"
blanchet@48975
   553
  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"
blanchet@48975
   554
    unfolding wpull_def by auto
blanchet@48975
   555
  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)"
blanchet@48975
   556
    (is "wpull ?A ?B1 ?B2 _ _ _ _")
blanchet@48975
   557
  proof (unfold wpull_def)
blanchet@48975
   558
    { fix as bs assume *: "as \<in> ?B1" "bs \<in> ?B2" "map f1 as = map f2 bs"
blanchet@48975
   559
      hence "length as = length bs" by (metis length_map)
blanchet@48975
   560
      hence "\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs" using *
blanchet@48975
   561
      proof (induct as bs rule: list_induct2)
blanchet@48975
   562
        case (Cons a as b bs)
blanchet@48975
   563
        hence "a \<in> B1" "b \<in> B2" "f1 a = f2 b" by auto
blanchet@48975
   564
        with pull obtain z where "z \<in> A" "p1 z = a" "p2 z = b" by blast
blanchet@48975
   565
        moreover
blanchet@48975
   566
        from Cons obtain zs where "zs \<in> ?A" "map p1 zs = as" "map p2 zs = bs" by auto
blanchet@48975
   567
        ultimately have "z # zs \<in> ?A" "map p1 (z # zs) = a # as \<and> map p2 (z # zs) = b # bs" by auto
blanchet@48975
   568
        thus ?case by (rule_tac x = "z # zs" in bexI)
blanchet@48975
   569
      qed simp
blanchet@48975
   570
    }
blanchet@48975
   571
    thus "\<forall>as bs. as \<in> ?B1 \<and> bs \<in> ?B2 \<and> map f1 as = map f2 bs \<longrightarrow>
blanchet@48975
   572
      (\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs)" by blast
blanchet@48975
   573
  qed
blanchet@48975
   574
qed auto
blanchet@48975
   575
blanchet@48975
   576
bnf_def deadlist = "map id" [] "\<lambda>_::'a list. |lists (UNIV :: 'a set)|" ["[]"]
blanchet@48975
   577
by (auto simp add: cinfinite_def wpull_def infinite_UNIV_listI map.id
blanchet@48975
   578
  ordLeq_transitive ctwo_def card_of_card_order_on Field_card_of card_of_mono1 ordLeq_cexp2)
blanchet@48975
   579
blanchet@48975
   580
(* Finite sets *)
blanchet@48975
   581
abbreviation afset where "afset \<equiv> abs_fset"
blanchet@48975
   582
abbreviation rfset where "rfset \<equiv> rep_fset"
blanchet@48975
   583
blanchet@48975
   584
lemma fset_fset_member:
blanchet@48975
   585
"fset A = {a. a |\<in>| A}"
blanchet@48975
   586
unfolding fset_def fset_member_def by auto
blanchet@48975
   587
blanchet@48975
   588
lemma afset_rfset:
blanchet@48975
   589
"afset (rfset x) = x"
blanchet@48975
   590
by (rule Quotient_fset[unfolded Quotient_def, THEN conjunct1, rule_format])
blanchet@48975
   591
blanchet@48975
   592
lemma afset_rfset_id:
blanchet@48975
   593
"afset o rfset = id"
blanchet@48975
   594
unfolding comp_def afset_rfset id_def ..
blanchet@48975
   595
blanchet@48975
   596
lemma rfset:
blanchet@48975
   597
"rfset A = rfset B \<longleftrightarrow> A = B"
blanchet@48975
   598
by (metis afset_rfset)
blanchet@48975
   599
blanchet@48975
   600
lemma afset_set:
blanchet@48975
   601
"afset as = afset bs \<longleftrightarrow> set as = set bs"
blanchet@48975
   602
using Quotient_fset unfolding Quotient_def list_eq_def by auto
blanchet@48975
   603
blanchet@48975
   604
lemma surj_afset:
blanchet@48975
   605
"\<exists> as. A = afset as"
blanchet@48975
   606
by (metis afset_rfset)
blanchet@48975
   607
blanchet@48975
   608
lemma fset_def2:
blanchet@48975
   609
"fset = set o rfset"
blanchet@48975
   610
unfolding fset_def map_fun_def[abs_def] by simp
blanchet@48975
   611
blanchet@48975
   612
lemma fset_def2_raw:
blanchet@48975
   613
"fset A = set (rfset A)"
blanchet@48975
   614
unfolding fset_def2 by simp
blanchet@48975
   615
blanchet@48975
   616
lemma fset_comp_afset:
blanchet@48975
   617
"fset o afset = set"
blanchet@48975
   618
unfolding fset_def2 comp_def apply(rule ext)
blanchet@48975
   619
unfolding afset_set[symmetric] afset_rfset ..
blanchet@48975
   620
blanchet@48975
   621
lemma fset_afset:
blanchet@48975
   622
"fset (afset as) = set as"
blanchet@48975
   623
unfolding fset_comp_afset[symmetric] by simp
blanchet@48975
   624
blanchet@48975
   625
lemma set_rfset_afset:
blanchet@48975
   626
"set (rfset (afset as)) = set as"
blanchet@48975
   627
unfolding afset_set[symmetric] afset_rfset ..
blanchet@48975
   628
blanchet@48975
   629
lemma map_fset_comp_afset:
blanchet@48975
   630
"(map_fset f) o afset = afset o (map f)"
blanchet@48975
   631
unfolding map_fset_def map_fun_def[abs_def] comp_def apply(rule ext)
blanchet@48975
   632
unfolding afset_set set_map set_rfset_afset id_apply ..
blanchet@48975
   633
blanchet@48975
   634
lemma map_fset_afset:
blanchet@48975
   635
"(map_fset f) (afset as) = afset (map f as)"
blanchet@48975
   636
using map_fset_comp_afset unfolding comp_def fun_eq_iff by auto
blanchet@48975
   637
blanchet@48975
   638
lemma fset_map_fset:
blanchet@48975
   639
"fset (map_fset f A) = (image f) (fset A)"
blanchet@48975
   640
apply(subst afset_rfset[symmetric, of A])
blanchet@48975
   641
unfolding map_fset_afset fset_afset set_map
blanchet@48975
   642
unfolding fset_def2_raw ..
blanchet@48975
   643
blanchet@48975
   644
lemma map_fset_def2:
blanchet@48975
   645
"map_fset f = afset o (map f) o rfset"
blanchet@48975
   646
unfolding map_fset_def map_fun_def[abs_def] by simp
blanchet@48975
   647
blanchet@48975
   648
lemma map_fset_def2_raw:
blanchet@48975
   649
"map_fset f A = afset (map f (rfset A))"
blanchet@48975
   650
unfolding map_fset_def2 by simp
blanchet@48975
   651
blanchet@48975
   652
lemma finite_ex_fset:
blanchet@48975
   653
assumes "finite A"
blanchet@48975
   654
shows "\<exists> B. fset B = A"
blanchet@48975
   655
by (metis assms finite_list fset_afset)
blanchet@48975
   656
blanchet@48975
   657
lemma wpull_image:
blanchet@48975
   658
assumes "wpull A B1 B2 f1 f2 p1 p2"
blanchet@48975
   659
shows "wpull (Pow A) (Pow B1) (Pow B2) (image f1) (image f2) (image p1) (image p2)"
blanchet@48975
   660
unfolding wpull_def Pow_def Bex_def mem_Collect_eq proof clarify
blanchet@48975
   661
  fix Y1 Y2 assume Y1: "Y1 \<subseteq> B1" and Y2: "Y2 \<subseteq> B2" and EQ: "f1 ` Y1 = f2 ` Y2"
blanchet@48975
   662
  def X \<equiv> "{a \<in> A. p1 a \<in> Y1 \<and> p2 a \<in> Y2}"
blanchet@48975
   663
  show "\<exists>X\<subseteq>A. p1 ` X = Y1 \<and> p2 ` X = Y2"
blanchet@48975
   664
  proof (rule exI[of _ X], intro conjI)
blanchet@48975
   665
    show "p1 ` X = Y1"
blanchet@48975
   666
    proof
blanchet@48975
   667
      show "Y1 \<subseteq> p1 ` X"
blanchet@48975
   668
      proof safe
blanchet@48975
   669
        fix y1 assume y1: "y1 \<in> Y1"
blanchet@48975
   670
        then obtain y2 where y2: "y2 \<in> Y2" and eq: "f1 y1 = f2 y2" using EQ by auto
blanchet@48975
   671
        then obtain x where "x \<in> A" and "p1 x = y1" and "p2 x = y2"
blanchet@48975
   672
        using assms y1 Y1 Y2 unfolding wpull_def by blast
blanchet@48975
   673
        thus "y1 \<in> p1 ` X" unfolding X_def using y1 y2 by auto
blanchet@48975
   674
      qed
blanchet@48975
   675
    qed(unfold X_def, auto)
blanchet@48975
   676
    show "p2 ` X = Y2"
blanchet@48975
   677
    proof
blanchet@48975
   678
      show "Y2 \<subseteq> p2 ` X"
blanchet@48975
   679
      proof safe
blanchet@48975
   680
        fix y2 assume y2: "y2 \<in> Y2"
blanchet@48975
   681
        then obtain y1 where y1: "y1 \<in> Y1" and eq: "f1 y1 = f2 y2" using EQ by force
blanchet@48975
   682
        then obtain x where "x \<in> A" and "p1 x = y1" and "p2 x = y2"
blanchet@48975
   683
        using assms y2 Y1 Y2 unfolding wpull_def by blast
blanchet@48975
   684
        thus "y2 \<in> p2 ` X" unfolding X_def using y1 y2 by auto
blanchet@48975
   685
      qed
blanchet@48975
   686
    qed(unfold X_def, auto)
blanchet@48975
   687
  qed(unfold X_def, auto)
blanchet@48975
   688
qed
blanchet@48975
   689
blanchet@48975
   690
lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
blanchet@48975
   691
by (rule f_the_inv_into_f) (auto simp: inj_on_def fset_cong dest!: finite_ex_fset)
blanchet@48975
   692
blanchet@48975
   693
bnf_def fset = map_fset [fset] "\<lambda>_::'a fset. natLeq" ["{||}"]
blanchet@48975
   694
proof -
blanchet@48975
   695
  show "map_fset id = id"
blanchet@48975
   696
  unfolding map_fset_def2 map_id o_id afset_rfset_id ..
blanchet@48975
   697
next
blanchet@48975
   698
  fix f g
blanchet@48975
   699
  show "map_fset (g o f) = map_fset g o map_fset f"
blanchet@48975
   700
  unfolding map_fset_def2 map.comp[symmetric] comp_def apply(rule ext)
blanchet@48975
   701
  unfolding afset_set set_map fset_def2_raw[symmetric] image_image[symmetric]
blanchet@48975
   702
  unfolding map_fset_afset[symmetric] map_fset_image afset_rfset
blanchet@48975
   703
  by (rule refl)
blanchet@48975
   704
next
blanchet@48975
   705
  fix x f g
blanchet@48975
   706
  assume "\<And>z. z \<in> fset x \<Longrightarrow> f z = g z"
blanchet@48975
   707
  hence "map f (rfset x) = map g (rfset x)"
blanchet@48975
   708
  apply(intro map_cong) unfolding fset_def2_raw by auto
blanchet@48975
   709
  thus "map_fset f x = map_fset g x" unfolding map_fset_def2_raw
blanchet@48975
   710
  by (rule arg_cong)
blanchet@48975
   711
next
blanchet@48975
   712
  fix f
blanchet@48975
   713
  show "fset o map_fset f = image f o fset"
blanchet@48975
   714
  unfolding comp_def fset_map_fset ..
blanchet@48975
   715
next
blanchet@48975
   716
  show "card_order natLeq" by (rule natLeq_card_order)
blanchet@48975
   717
next
blanchet@48975
   718
  show "cinfinite natLeq" by (rule natLeq_cinfinite)
blanchet@48975
   719
next
blanchet@48975
   720
  fix x
blanchet@48975
   721
  show "|fset x| \<le>o natLeq"
blanchet@48975
   722
  unfolding fset_def2_raw
blanchet@48975
   723
  apply (rule ordLess_imp_ordLeq)
blanchet@48975
   724
  apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
blanchet@48975
   725
  by (rule finite_set)
blanchet@48975
   726
next
blanchet@48975
   727
  fix A :: "'a set"
blanchet@48975
   728
  have "|{x. fset x \<subseteq> A}| \<le>o |afset ` {as. set as \<subseteq> A}|"
blanchet@48975
   729
  apply(rule card_of_mono1) unfolding fset_def2_raw apply auto
blanchet@48975
   730
  apply (rule image_eqI)
blanchet@48975
   731
  by (auto simp: afset_rfset)
blanchet@48975
   732
  also have "|afset ` {as. set as \<subseteq> A}| \<le>o |{as. set as \<subseteq> A}|" using card_of_image .
blanchet@48975
   733
  also have "|{as. set as \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" by (rule list_in_bd)
blanchet@48975
   734
  finally show "|{x. fset x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" .
blanchet@48975
   735
next
blanchet@48975
   736
  fix A B1 B2 f1 f2 p1 p2
blanchet@48975
   737
  assume wp: "wpull A B1 B2 f1 f2 p1 p2"
blanchet@48975
   738
  hence "wpull (Pow A) (Pow B1) (Pow B2) (image f1) (image f2) (image p1) (image p2)"
blanchet@48975
   739
  by(rule wpull_image)
blanchet@48975
   740
  show "wpull {x. fset x \<subseteq> A} {x. fset x \<subseteq> B1} {x. fset x \<subseteq> B2}
blanchet@48975
   741
              (map_fset f1) (map_fset f2) (map_fset p1) (map_fset p2)"
blanchet@48975
   742
  unfolding wpull_def Pow_def Bex_def mem_Collect_eq proof clarify
blanchet@48975
   743
    fix y1 y2
blanchet@48975
   744
    assume Y1: "fset y1 \<subseteq> B1" and Y2: "fset y2 \<subseteq> B2"
blanchet@48975
   745
    assume "map_fset f1 y1 = map_fset f2 y2"
blanchet@48975
   746
    hence EQ: "f1 ` (fset y1) = f2 ` (fset y2)" unfolding map_fset_def2_raw
blanchet@48975
   747
    unfolding afset_set set_map fset_def2_raw .
blanchet@48975
   748
    with Y1 Y2 obtain X where X: "X \<subseteq> A"
blanchet@48975
   749
    and Y1: "p1 ` X = fset y1" and Y2: "p2 ` X = fset y2"
blanchet@48975
   750
    using wpull_image[OF wp] unfolding wpull_def Pow_def
blanchet@48975
   751
    unfolding Bex_def mem_Collect_eq apply -
blanchet@48975
   752
    apply(erule allE[of _ "fset y1"], erule allE[of _ "fset y2"]) by auto
blanchet@48975
   753
    have "\<forall> y1' \<in> fset y1. \<exists> x. x \<in> X \<and> y1' = p1 x" using Y1 by auto
blanchet@48975
   754
    then obtain q1 where q1: "\<forall> y1' \<in> fset y1. q1 y1' \<in> X \<and> y1' = p1 (q1 y1')" by metis
blanchet@48975
   755
    have "\<forall> y2' \<in> fset y2. \<exists> x. x \<in> X \<and> y2' = p2 x" using Y2 by auto
blanchet@48975
   756
    then obtain q2 where q2: "\<forall> y2' \<in> fset y2. q2 y2' \<in> X \<and> y2' = p2 (q2 y2')" by metis
blanchet@48975
   757
    def X' \<equiv> "q1 ` (fset y1) \<union> q2 ` (fset y2)"
blanchet@48975
   758
    have X': "X' \<subseteq> A" and Y1: "p1 ` X' = fset y1" and Y2: "p2 ` X' = fset y2"
blanchet@48975
   759
    using X Y1 Y2 q1 q2 unfolding X'_def by auto
blanchet@48975
   760
    have fX': "finite X'" unfolding X'_def by simp
blanchet@48975
   761
    then obtain x where X'eq: "X' = fset x" by (auto dest: finite_ex_fset)
blanchet@48975
   762
    show "\<exists>x. fset x \<subseteq> A \<and> map_fset p1 x = y1 \<and> map_fset p2 x = y2"
blanchet@48975
   763
    apply(intro exI[of _ "x"]) using X' Y1 Y2
blanchet@48975
   764
    unfolding X'eq map_fset_def2_raw fset_def2_raw set_map[symmetric]
blanchet@48975
   765
    afset_set[symmetric] afset_rfset by simp
blanchet@48975
   766
  qed
blanchet@48975
   767
qed auto
blanchet@48975
   768
blanchet@48975
   769
lemma fset_pred[simp]: "fset_pred R a b \<longleftrightarrow>
blanchet@48975
   770
  ((\<forall>t \<in> fset a. (\<exists>u \<in> fset b. R t u)) \<and>
blanchet@48975
   771
   (\<forall>t \<in> fset b. (\<exists>u \<in> fset a. R u t)))" (is "?L = ?R")
blanchet@48975
   772
proof
blanchet@48975
   773
  assume ?L thus ?R unfolding fset_rel_def fset_pred_def
blanchet@48975
   774
    Gr_def relcomp_unfold converse_unfold
blanchet@48975
   775
  apply (simp add: subset_eq Ball_def)
blanchet@48975
   776
  apply (rule conjI)
blanchet@48975
   777
  apply (clarsimp, metis snd_conv)
blanchet@48975
   778
  by (clarsimp, metis fst_conv)
blanchet@48975
   779
next
blanchet@48975
   780
  assume ?R
blanchet@48975
   781
  def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?R'")
blanchet@48975
   782
  have "finite ?R'" by (intro finite_Int[OF disjI2] finite_cartesian_product) auto
blanchet@48975
   783
  hence *: "fset R' = ?R'" unfolding R'_def by (intro fset_to_fset)
blanchet@48975
   784
  show ?L unfolding fset_rel_def fset_pred_def Gr_def relcomp_unfold converse_unfold
blanchet@48975
   785
  proof (intro CollectI prod_caseI exI conjI)
blanchet@48975
   786
    from * show "(R', a) = (R', map_fset fst R')" using conjunct1[OF `?R`]
blanchet@48975
   787
      by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits)
blanchet@48975
   788
    from * show "(R', b) = (R', map_fset snd R')" using conjunct2[OF `?R`]
blanchet@48975
   789
      by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits)
blanchet@48975
   790
  qed (auto simp add: *)
blanchet@48975
   791
qed
blanchet@48975
   792
blanchet@48975
   793
(* Countable sets *)
blanchet@48975
   794
blanchet@48975
   795
lemma card_of_countable_sets_range:
blanchet@48975
   796
fixes A :: "'a set"
blanchet@48975
   797
shows "|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |{f::nat \<Rightarrow> 'a. range f \<subseteq> A}|"
blanchet@48975
   798
apply(rule card_of_ordLeqI[of fromNat]) using inj_on_fromNat
blanchet@48975
   799
unfolding inj_on_def by auto
blanchet@48975
   800
blanchet@48975
   801
lemma card_of_countable_sets_Func:
blanchet@48975
   802
"|{X. X \<subseteq> A \<and> countable X \<and> X \<noteq> {}}| \<le>o |A| ^c natLeq"
blanchet@48975
   803
using card_of_countable_sets_range card_of_Func_UNIV[THEN ordIso_symmetric]
blanchet@48975
   804
unfolding cexp_def Field_natLeq Field_card_of
blanchet@48975
   805
by(rule ordLeq_ordIso_trans)
blanchet@48975
   806
blanchet@48975
   807
lemma ordLeq_countable_subsets:
blanchet@48975
   808
"|A| \<le>o |{X. X \<subseteq> A \<and> countable X}|"
blanchet@48975
   809
apply(rule card_of_ordLeqI[of "\<lambda> a. {a}"]) unfolding inj_on_def by auto
blanchet@48975
   810
blanchet@48975
   811
lemma finite_countable_subset:
blanchet@48975
   812
"finite {X. X \<subseteq> A \<and> countable X} \<longleftrightarrow> finite A"
blanchet@48975
   813
apply default
blanchet@48975
   814
 apply (erule contrapos_pp)
blanchet@48975
   815
 apply (rule card_of_ordLeq_infinite)
blanchet@48975
   816
 apply (rule ordLeq_countable_subsets)
blanchet@48975
   817
 apply assumption
blanchet@48975
   818
apply (rule finite_Collect_conjI)
blanchet@48975
   819
apply (rule disjI1)
blanchet@48975
   820
by (erule finite_Collect_subsets)
blanchet@48975
   821
blanchet@48975
   822
lemma card_of_countable_sets:
blanchet@48975
   823
"|{X. X \<subseteq> A \<and> countable X}| \<le>o ( |A| +c ctwo) ^c natLeq"
blanchet@48975
   824
(is "|?L| \<le>o _")
blanchet@48975
   825
proof(cases "finite A")
blanchet@48975
   826
  let ?R = "Func (UNIV::nat set) (A <+> (UNIV::bool set))"
blanchet@48975
   827
  case True hence "finite ?L" by simp
blanchet@48975
   828
  moreover have "infinite ?R"
blanchet@48975
   829
  apply(rule infinite_Func[of _ "Inr True" "Inr False"]) by auto
blanchet@48975
   830
  ultimately show ?thesis unfolding cexp_def csum_def ctwo_def Field_natLeq Field_card_of
blanchet@48975
   831
  apply(intro ordLess_imp_ordLeq) by (rule finite_ordLess_infinite2)
blanchet@48975
   832
next
blanchet@48975
   833
  case False
blanchet@48975
   834
  hence "|{X. X \<subseteq> A \<and> countable X}| =o |{X. X \<subseteq> A \<and> countable X} - {{}}|"
blanchet@48975
   835
  by (intro card_of_infinite_diff_finitte finite.emptyI finite.insertI ordIso_symmetric)
blanchet@48975
   836
     (unfold finite_countable_subset)
blanchet@48975
   837
  also have "|{X. X \<subseteq> A \<and> countable X} - {{}}| \<le>o |A| ^c natLeq"
blanchet@48975
   838
  using card_of_countable_sets_Func[of A] unfolding set_diff_eq by auto
blanchet@48975
   839
  also have "|A| ^c natLeq \<le>o ( |A| +c ctwo) ^c natLeq"
blanchet@48975
   840
  apply(rule cexp_mono1_cone_ordLeq)
blanchet@48975
   841
    apply(rule ordLeq_csum1, rule card_of_Card_order)
blanchet@48975
   842
    apply (rule cone_ordLeq_cexp)
blanchet@48975
   843
    apply (rule cone_ordLeq_Cnotzero)
blanchet@48975
   844
    using csum_Cnotzero2 ctwo_Cnotzero apply blast
blanchet@48975
   845
    by (rule natLeq_Card_order)
blanchet@48975
   846
  finally show ?thesis .
blanchet@48975
   847
qed
blanchet@48975
   848
blanchet@48975
   849
bnf_def cset = cIm [rcset] "\<lambda>_::'a cset. natLeq" ["cEmp"]
blanchet@48975
   850
proof -
blanchet@48975
   851
  show "cIm id = id" unfolding cIm_def[abs_def] id_def by auto
blanchet@48975
   852
next
blanchet@48975
   853
  fix f g show "cIm (g \<circ> f) = cIm g \<circ> cIm f"
blanchet@48975
   854
  unfolding cIm_def[abs_def] apply(rule ext) unfolding comp_def by auto
blanchet@48975
   855
next
blanchet@48975
   856
  fix C f g assume eq: "\<And>a. a \<in> rcset C \<Longrightarrow> f a = g a"
blanchet@48975
   857
  thus "cIm f C = cIm g C"
blanchet@48975
   858
  unfolding cIm_def[abs_def] unfolding image_def by auto
blanchet@48975
   859
next
blanchet@48975
   860
  fix f show "rcset \<circ> cIm f = op ` f \<circ> rcset" unfolding cIm_def[abs_def] by auto
blanchet@48975
   861
next
blanchet@48975
   862
  show "card_order natLeq" by (rule natLeq_card_order)
blanchet@48975
   863
next
blanchet@48975
   864
  show "cinfinite natLeq" by (rule natLeq_cinfinite)
blanchet@48975
   865
next
blanchet@48975
   866
  fix C show "|rcset C| \<le>o natLeq" using rcset unfolding countable_def .
blanchet@48975
   867
next
blanchet@48975
   868
  fix A :: "'a set"
blanchet@48975
   869
  have "|{Z. rcset Z \<subseteq> A}| \<le>o |acset ` {X. X \<subseteq> A \<and> countable X}|"
blanchet@48975
   870
  apply(rule card_of_mono1) unfolding Pow_def image_def
blanchet@48975
   871
  proof (rule Collect_mono, clarsimp)
blanchet@48975
   872
    fix x
blanchet@48975
   873
    assume "rcset x \<subseteq> A"
blanchet@48975
   874
    hence "rcset x \<subseteq> A \<and> countable (rcset x) \<and> x = acset (rcset x)"
blanchet@48975
   875
    using acset_rcset[of x] rcset[of x] by force
blanchet@48975
   876
    thus "\<exists>y \<subseteq> A. countable y \<and> x = acset y" by blast
blanchet@48975
   877
  qed
blanchet@48975
   878
  also have "|acset ` {X. X \<subseteq> A \<and> countable X}| \<le>o |{X. X \<subseteq> A \<and> countable X}|"
blanchet@48975
   879
  using card_of_image .
blanchet@48975
   880
  also have "|{X. X \<subseteq> A \<and> countable X}| \<le>o ( |A| +c ctwo) ^c natLeq"
blanchet@48975
   881
  using card_of_countable_sets .
blanchet@48975
   882
  finally show "|{Z. rcset Z \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" .
blanchet@48975
   883
next
blanchet@48975
   884
  fix A B1 B2 f1 f2 p1 p2
blanchet@48975
   885
  assume wp: "wpull A B1 B2 f1 f2 p1 p2"
blanchet@48975
   886
  show "wpull {x. rcset x \<subseteq> A} {x. rcset x \<subseteq> B1} {x. rcset x \<subseteq> B2}
blanchet@48975
   887
              (cIm f1) (cIm f2) (cIm p1) (cIm p2)"
blanchet@48975
   888
  unfolding wpull_def proof safe
blanchet@48975
   889
    fix y1 y2
blanchet@48975
   890
    assume Y1: "rcset y1 \<subseteq> B1" and Y2: "rcset y2 \<subseteq> B2"
blanchet@48975
   891
    assume "cIm f1 y1 = cIm f2 y2"
blanchet@48975
   892
    hence EQ: "f1 ` (rcset y1) = f2 ` (rcset y2)"
blanchet@48975
   893
    unfolding cIm_def by auto
blanchet@48975
   894
    with Y1 Y2 obtain X where X: "X \<subseteq> A"
blanchet@48975
   895
    and Y1: "p1 ` X = rcset y1" and Y2: "p2 ` X = rcset y2"
blanchet@48975
   896
    using wpull_image[OF wp] unfolding wpull_def Pow_def
blanchet@48975
   897
    unfolding Bex_def mem_Collect_eq apply -
blanchet@48975
   898
    apply(erule allE[of _ "rcset y1"], erule allE[of _ "rcset y2"]) by auto
blanchet@48975
   899
    have "\<forall> y1' \<in> rcset y1. \<exists> x. x \<in> X \<and> y1' = p1 x" using Y1 by auto
blanchet@48975
   900
    then obtain q1 where q1: "\<forall> y1' \<in> rcset y1. q1 y1' \<in> X \<and> y1' = p1 (q1 y1')" by metis
blanchet@48975
   901
    have "\<forall> y2' \<in> rcset y2. \<exists> x. x \<in> X \<and> y2' = p2 x" using Y2 by auto
blanchet@48975
   902
    then obtain q2 where q2: "\<forall> y2' \<in> rcset y2. q2 y2' \<in> X \<and> y2' = p2 (q2 y2')" by metis
blanchet@48975
   903
    def X' \<equiv> "q1 ` (rcset y1) \<union> q2 ` (rcset y2)"
blanchet@48975
   904
    have X': "X' \<subseteq> A" and Y1: "p1 ` X' = rcset y1" and Y2: "p2 ` X' = rcset y2"
blanchet@48975
   905
    using X Y1 Y2 q1 q2 unfolding X'_def by fast+
blanchet@48975
   906
    have fX': "countable X'" unfolding X'_def by simp
blanchet@48975
   907
    then obtain x where X'eq: "X' = rcset x" by (metis rcset_acset)
blanchet@48975
   908
    show "\<exists>x\<in>{x. rcset x \<subseteq> A}. cIm p1 x = y1 \<and> cIm p2 x = y2"
blanchet@48975
   909
    apply(intro bexI[of _ "x"]) using X' Y1 Y2 unfolding X'eq cIm_def by auto
blanchet@48975
   910
  qed
blanchet@48975
   911
qed (unfold cEmp_def, auto)
blanchet@48975
   912
blanchet@48975
   913
blanchet@48975
   914
(* Multisets *)
blanchet@48975
   915
blanchet@48975
   916
lemma setsum_gt_0_iff:
blanchet@48975
   917
fixes f :: "'a \<Rightarrow> nat" assumes "finite A"
blanchet@48975
   918
shows "setsum f A > 0 \<longleftrightarrow> (\<exists> a \<in> A. f a > 0)"
blanchet@48975
   919
(is "?L \<longleftrightarrow> ?R")
blanchet@48975
   920
proof-
blanchet@48975
   921
  have "?L \<longleftrightarrow> \<not> setsum f A = 0" by fast
blanchet@48975
   922
  also have "... \<longleftrightarrow> (\<exists> a \<in> A. f a \<noteq> 0)" using assms by simp
blanchet@48975
   923
  also have "... \<longleftrightarrow> ?R" by simp
blanchet@48975
   924
  finally show ?thesis .
blanchet@48975
   925
qed
blanchet@48975
   926
blanchet@48975
   927
(*   *)
blanchet@48975
   928
definition mmap :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> nat) \<Rightarrow> 'b \<Rightarrow> nat" where
blanchet@48975
   929
"mmap h f b = setsum f {a. h a = b \<and> f a > 0}"
blanchet@48975
   930
blanchet@48975
   931
lemma mmap_id: "mmap id = id"
blanchet@48975
   932
proof (rule ext)+
blanchet@48975
   933
  fix f a show "mmap id f a = id f a"
blanchet@48975
   934
  proof(cases "f a = 0")
blanchet@48975
   935
    case False
blanchet@48975
   936
    hence 1: "{aa. aa = a \<and> 0 < f aa} = {a}" by auto
blanchet@48975
   937
    show ?thesis by (simp add: mmap_def id_apply 1)
blanchet@48975
   938
  qed(unfold mmap_def, auto)
blanchet@48975
   939
qed
blanchet@48975
   940
blanchet@48975
   941
lemma inj_on_setsum_inv:
blanchet@48975
   942
assumes f: "f \<in> multiset"
blanchet@48975
   943
and 1: "(0::nat) < setsum f {a. h a = b' \<and> 0 < f a}" (is "0 < setsum f ?A'")
blanchet@48975
   944
and 2: "{a. h a = b \<and> 0 < f a} = {a. h a = b' \<and> 0 < f a}" (is "?A = ?A'")
blanchet@48975
   945
shows "b = b'"
blanchet@48975
   946
proof-
blanchet@48975
   947
  have "finite ?A'" using f unfolding multiset_def by auto
blanchet@48975
   948
  hence "?A' \<noteq> {}" using 1 setsum_gt_0_iff by auto
blanchet@48975
   949
  thus ?thesis using 2 by auto
blanchet@48975
   950
qed
blanchet@48975
   951
blanchet@48975
   952
lemma mmap_comp:
blanchet@48975
   953
fixes h1 :: "'a \<Rightarrow> 'b" and h2 :: "'b \<Rightarrow> 'c"
blanchet@48975
   954
assumes f: "f \<in> multiset"
blanchet@48975
   955
shows "mmap (h2 o h1) f = (mmap h2 o mmap h1) f"
blanchet@48975
   956
unfolding mmap_def[abs_def] comp_def proof(rule ext)+
blanchet@48975
   957
  fix c :: 'c
blanchet@48975
   958
  let ?A = "{a. h2 (h1 a) = c \<and> 0 < f a}"
blanchet@48975
   959
  let ?As = "\<lambda> b. {a. h1 a = b \<and> 0 < f a}"
blanchet@48975
   960
  let ?B = "{b. h2 b = c \<and> 0 < setsum f (?As b)}"
blanchet@48975
   961
  have 0: "{?As b | b.  b \<in> ?B} = ?As ` ?B" by auto
blanchet@48975
   962
  have "\<And> b. finite (?As b)" using f unfolding multiset_def by simp
blanchet@48975
   963
  hence "?B = {b. h2 b = c \<and> ?As b \<noteq> {}}" using setsum_gt_0_iff by auto
blanchet@48975
   964
  hence A: "?A = \<Union> {?As b | b.  b \<in> ?B}" by auto
blanchet@48975
   965
  have "setsum f ?A = setsum (setsum f) {?As b | b.  b \<in> ?B}"
blanchet@48975
   966
  unfolding A apply(rule setsum_Union_disjoint)
blanchet@48975
   967
  using f unfolding multiset_def by auto
blanchet@48975
   968
  also have "... = setsum (setsum f) (?As ` ?B)" unfolding 0 ..
blanchet@48975
   969
  also have "... = setsum (setsum f o ?As) ?B" apply(rule setsum_reindex)
blanchet@48975
   970
  unfolding inj_on_def apply auto using inj_on_setsum_inv[OF f, of h1] by blast
blanchet@48975
   971
  also have "... = setsum (\<lambda> b. setsum f (?As b)) ?B" unfolding comp_def ..
blanchet@48975
   972
  finally show "setsum f ?A = setsum (\<lambda> b. setsum f (?As b)) ?B" .
blanchet@48975
   973
qed
blanchet@48975
   974
blanchet@48975
   975
lemma mmap_comp1:
blanchet@48975
   976
fixes h1 :: "'a \<Rightarrow> 'b" and h2 :: "'b \<Rightarrow> 'c"
blanchet@48975
   977
assumes "f \<in> multiset"
blanchet@48975
   978
shows "mmap (\<lambda> a. h2 (h1 a)) f = mmap h2 (mmap h1 f)"
blanchet@48975
   979
using mmap_comp[OF assms] unfolding comp_def by auto
blanchet@48975
   980
blanchet@48975
   981
lemma mmap:
blanchet@48975
   982
assumes "f \<in> multiset"
blanchet@48975
   983
shows "mmap h f \<in> multiset"
blanchet@48975
   984
using assms unfolding mmap_def[abs_def] multiset_def proof safe
blanchet@48975
   985
  assume fin: "finite {a. 0 < f a}"  (is "finite ?A")
blanchet@48975
   986
  show "finite {b. 0 < setsum f {a. h a = b \<and> 0 < f a}}"
blanchet@48975
   987
  (is "finite {b. 0 < setsum f (?As b)}")
blanchet@48975
   988
  proof- let ?B = "{b. 0 < setsum f (?As b)}"
blanchet@48975
   989
    have "\<And> b. finite (?As b)" using assms unfolding multiset_def by simp
blanchet@48975
   990
    hence B: "?B = {b. ?As b \<noteq> {}}" using setsum_gt_0_iff by auto
blanchet@48975
   991
    hence "?B \<subseteq> h ` ?A" by auto
blanchet@48975
   992
    thus ?thesis using finite_surj[OF fin] by auto
blanchet@48975
   993
  qed
blanchet@48975
   994
qed
blanchet@48975
   995
blanchet@48975
   996
lemma mmap_cong:
blanchet@48975
   997
assumes "\<And>a. a \<in># M \<Longrightarrow> f a = g a"
blanchet@48975
   998
shows "mmap f (count M) = mmap g (count M)"
blanchet@48975
   999
using assms unfolding mmap_def[abs_def] by (intro ext, intro setsum_cong) auto
blanchet@48975
  1000
blanchet@48975
  1001
abbreviation supp where "supp f \<equiv> {a. f a > 0}"
blanchet@48975
  1002
blanchet@48975
  1003
lemma mmap_image_comp:
blanchet@48975
  1004
assumes f: "f \<in> multiset"
blanchet@48975
  1005
shows "(supp o mmap h) f = (image h o supp) f"
blanchet@48975
  1006
unfolding mmap_def[abs_def] comp_def proof-
blanchet@48975
  1007
  have "\<And> b. finite {a. h a = b \<and> 0 < f a}" (is "\<And> b. finite (?As b)")
blanchet@48975
  1008
  using f unfolding multiset_def by auto
blanchet@48975
  1009
  thus "{b. 0 < setsum f (?As b)} = h ` {a. 0 < f a}"
blanchet@48975
  1010
  using setsum_gt_0_iff by auto
blanchet@48975
  1011
qed
blanchet@48975
  1012
blanchet@48975
  1013
lemma mmap_image:
blanchet@48975
  1014
assumes f: "f \<in> multiset"
blanchet@48975
  1015
shows "supp (mmap h f) = h ` (supp f)"
blanchet@48975
  1016
using mmap_image_comp[OF assms] unfolding comp_def .
blanchet@48975
  1017
blanchet@48975
  1018
lemma set_of_Abs_multiset:
blanchet@48975
  1019
assumes f: "f \<in> multiset"
blanchet@48975
  1020
shows "set_of (Abs_multiset f) = supp f"
blanchet@48975
  1021
using assms unfolding set_of_def by (auto simp: Abs_multiset_inverse)
blanchet@48975
  1022
blanchet@48975
  1023
lemma supp_count:
blanchet@48975
  1024
"supp (count M) = set_of M"
blanchet@48975
  1025
using assms unfolding set_of_def by auto
blanchet@48975
  1026
blanchet@48975
  1027
lemma multiset_of_surj:
blanchet@48975
  1028
"multiset_of ` {as. set as \<subseteq> A} = {M. set_of M \<subseteq> A}"
blanchet@48975
  1029
proof safe
blanchet@48975
  1030
  fix M assume M: "set_of M \<subseteq> A"
blanchet@48975
  1031
  obtain as where eq: "M = multiset_of as" using surj_multiset_of unfolding surj_def by auto
blanchet@48975
  1032
  hence "set as \<subseteq> A" using M by auto
blanchet@48975
  1033
  thus "M \<in> multiset_of ` {as. set as \<subseteq> A}" using eq by auto
blanchet@48975
  1034
next
blanchet@48975
  1035
  show "\<And>x xa xb. \<lbrakk>set xa \<subseteq> A; xb \<in> set_of (multiset_of xa)\<rbrakk> \<Longrightarrow> xb \<in> A"
blanchet@48975
  1036
  by (erule set_mp) (unfold set_of_multiset_of)
blanchet@48975
  1037
qed
blanchet@48975
  1038
blanchet@48975
  1039
lemma card_of_set_of:
blanchet@48975
  1040
"|{M. set_of M \<subseteq> A}| \<le>o |{as. set as \<subseteq> A}|"
blanchet@48975
  1041
apply(rule card_of_ordLeqI2[of _ multiset_of]) using multiset_of_surj by auto
blanchet@48975
  1042
blanchet@48975
  1043
lemma nat_sum_induct:
blanchet@48975
  1044
assumes "\<And>n1 n2. (\<And> m1 m2. m1 + m2 < n1 + n2 \<Longrightarrow> phi m1 m2) \<Longrightarrow> phi n1 n2"
blanchet@48975
  1045
shows "phi (n1::nat) (n2::nat)"
blanchet@48975
  1046
proof-
blanchet@48975
  1047
  let ?chi = "\<lambda> n1n2 :: nat * nat. phi (fst n1n2) (snd n1n2)"
blanchet@48975
  1048
  have "?chi (n1,n2)"
blanchet@48975
  1049
  apply(induct rule: measure_induct[of "\<lambda> n1n2. fst n1n2 + snd n1n2" ?chi])
blanchet@48975
  1050
  using assms by (metis fstI sndI)
blanchet@48975
  1051
  thus ?thesis by simp
blanchet@48975
  1052
qed
blanchet@48975
  1053
blanchet@48975
  1054
lemma matrix_count:
blanchet@48975
  1055
fixes ct1 ct2 :: "nat \<Rightarrow> nat"
blanchet@48975
  1056
assumes "setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2}"
blanchet@48975
  1057
shows
blanchet@48975
  1058
"\<exists> ct. (\<forall> i1 \<le> n1. setsum (\<lambda> i2. ct i1 i2) {..<Suc n2} = ct1 i1) \<and>
blanchet@48975
  1059
       (\<forall> i2 \<le> n2. setsum (\<lambda> i1. ct i1 i2) {..<Suc n1} = ct2 i2)"
blanchet@48975
  1060
(is "?phi ct1 ct2 n1 n2")
blanchet@48975
  1061
proof-
blanchet@48975
  1062
  have "\<forall> ct1 ct2 :: nat \<Rightarrow> nat.
blanchet@48975
  1063
        setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2} \<longrightarrow> ?phi ct1 ct2 n1 n2"
blanchet@48975
  1064
  proof(induct rule: nat_sum_induct[of
blanchet@48975
  1065
"\<lambda> n1 n2. \<forall> ct1 ct2 :: nat \<Rightarrow> nat.
blanchet@48975
  1066
     setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2} \<longrightarrow> ?phi ct1 ct2 n1 n2"],
blanchet@48975
  1067
      clarify)
blanchet@48975
  1068
  fix n1 n2 :: nat and ct1 ct2 :: "nat \<Rightarrow> nat"
blanchet@48975
  1069
  assume IH: "\<And> m1 m2. m1 + m2 < n1 + n2 \<Longrightarrow>
blanchet@48975
  1070
                \<forall> dt1 dt2 :: nat \<Rightarrow> nat.
blanchet@48975
  1071
                setsum dt1 {..<Suc m1} = setsum dt2 {..<Suc m2} \<longrightarrow> ?phi dt1 dt2 m1 m2"
blanchet@48975
  1072
  and ss: "setsum ct1 {..<Suc n1} = setsum ct2 {..<Suc n2}"
blanchet@48975
  1073
  show "?phi ct1 ct2 n1 n2"
blanchet@48975
  1074
  proof(cases n1)
blanchet@48975
  1075
    case 0 note n1 = 0
blanchet@48975
  1076
    show ?thesis
blanchet@48975
  1077
    proof(cases n2)
blanchet@48975
  1078
      case 0 note n2 = 0
blanchet@48975
  1079
      let ?ct = "\<lambda> i1 i2. ct2 0"
blanchet@48975
  1080
      show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by simp
blanchet@48975
  1081
    next
blanchet@48975
  1082
      case (Suc m2) note n2 = Suc
blanchet@48975
  1083
      let ?ct = "\<lambda> i1 i2. ct2 i2"
blanchet@48975
  1084
      show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by auto
blanchet@48975
  1085
    qed
blanchet@48975
  1086
  next
blanchet@48975
  1087
    case (Suc m1) note n1 = Suc
blanchet@48975
  1088
    show ?thesis
blanchet@48975
  1089
    proof(cases n2)
blanchet@48975
  1090
      case 0 note n2 = 0
blanchet@48975
  1091
      let ?ct = "\<lambda> i1 i2. ct1 i1"
blanchet@48975
  1092
      show ?thesis apply(rule exI[of _ ?ct]) using n1 n2 ss by auto
blanchet@48975
  1093
    next
blanchet@48975
  1094
      case (Suc m2) note n2 = Suc
blanchet@48975
  1095
      show ?thesis
blanchet@48975
  1096
      proof(cases "ct1 n1 \<le> ct2 n2")
blanchet@48975
  1097
        case True
blanchet@48975
  1098
        def dt2 \<equiv> "\<lambda> i2. if i2 = n2 then ct2 i2 - ct1 n1 else ct2 i2"
blanchet@48975
  1099
        have "setsum ct1 {..<Suc m1} = setsum dt2 {..<Suc n2}"
blanchet@48975
  1100
        unfolding dt2_def using ss n1 True by auto
blanchet@48975
  1101
        hence "?phi ct1 dt2 m1 n2" using IH[of m1 n2] n1 by simp
blanchet@48975
  1102
        then obtain dt where
blanchet@48975
  1103
        1: "\<And> i1. i1 \<le> m1 \<Longrightarrow> setsum (\<lambda> i2. dt i1 i2) {..<Suc n2} = ct1 i1" and
blanchet@48975
  1104
        2: "\<And> i2. i2 \<le> n2 \<Longrightarrow> setsum (\<lambda> i1. dt i1 i2) {..<Suc m1} = dt2 i2" by auto
blanchet@48975
  1105
        let ?ct = "\<lambda> i1 i2. if i1 = n1 then (if i2 = n2 then ct1 n1 else 0)
blanchet@48975
  1106
                                       else dt i1 i2"
blanchet@48975
  1107
        show ?thesis apply(rule exI[of _ ?ct])
blanchet@48975
  1108
        using n1 n2 1 2 True unfolding dt2_def by simp
blanchet@48975
  1109
      next
blanchet@48975
  1110
        case False
blanchet@48975
  1111
        hence False: "ct2 n2 < ct1 n1" by simp
blanchet@48975
  1112
        def dt1 \<equiv> "\<lambda> i1. if i1 = n1 then ct1 i1 - ct2 n2 else ct1 i1"
blanchet@48975
  1113
        have "setsum dt1 {..<Suc n1} = setsum ct2 {..<Suc m2}"
blanchet@48975
  1114
        unfolding dt1_def using ss n2 False by auto
blanchet@48975
  1115
        hence "?phi dt1 ct2 n1 m2" using IH[of n1 m2] n2 by simp
blanchet@48975
  1116
        then obtain dt where
blanchet@48975
  1117
        1: "\<And> i1. i1 \<le> n1 \<Longrightarrow> setsum (\<lambda> i2. dt i1 i2) {..<Suc m2} = dt1 i1" and
blanchet@48975
  1118
        2: "\<And> i2. i2 \<le> m2 \<Longrightarrow> setsum (\<lambda> i1. dt i1 i2) {..<Suc n1} = ct2 i2" by force
blanchet@48975
  1119
        let ?ct = "\<lambda> i1 i2. if i2 = n2 then (if i1 = n1 then ct2 n2 else 0)
blanchet@48975
  1120
                                       else dt i1 i2"
blanchet@48975
  1121
        show ?thesis apply(rule exI[of _ ?ct])
blanchet@48975
  1122
        using n1 n2 1 2 False unfolding dt1_def by simp
blanchet@48975
  1123
      qed
blanchet@48975
  1124
    qed
blanchet@48975
  1125
  qed
blanchet@48975
  1126
  qed
blanchet@48975
  1127
  thus ?thesis using assms by auto
blanchet@48975
  1128
qed
blanchet@48975
  1129
blanchet@48975
  1130
definition
blanchet@48975
  1131
"inj2 u B1 B2 \<equiv>
blanchet@48975
  1132
 \<forall> b1 b1' b2 b2'. {b1,b1'} \<subseteq> B1 \<and> {b2,b2'} \<subseteq> B2 \<and> u b1 b2 = u b1' b2'
blanchet@48975
  1133
                  \<longrightarrow> b1 = b1' \<and> b2 = b2'"
blanchet@48975
  1134
blanchet@48975
  1135
lemma matrix_count_finite:
blanchet@48975
  1136
assumes B1: "B1 \<noteq> {}" "finite B1" and B2: "B2 \<noteq> {}" "finite B2" and u: "inj2 u B1 B2"
blanchet@48975
  1137
and ss: "setsum N1 B1 = setsum N2 B2"
blanchet@48975
  1138
shows "\<exists> M :: 'a \<Rightarrow> nat.
blanchet@48975
  1139
            (\<forall> b1 \<in> B1. setsum (\<lambda> b2. M (u b1 b2)) B2 = N1 b1) \<and>
blanchet@48975
  1140
            (\<forall> b2 \<in> B2. setsum (\<lambda> b1. M (u b1 b2)) B1 = N2 b2)"
blanchet@48975
  1141
proof-
blanchet@48975
  1142
  obtain n1 where "card B1 = Suc n1" using B1 by (metis card_insert finite.simps)
blanchet@48975
  1143
  then obtain e1 where e1: "bij_betw e1 {..<Suc n1} B1"
blanchet@48975
  1144
  using ex_bij_betw_finite_nat[OF B1(2)] by (metis atLeast0LessThan bij_betw_the_inv_into)
blanchet@48975
  1145
  hence e1_inj: "inj_on e1 {..<Suc n1}" and e1_surj: "e1 ` {..<Suc n1} = B1"
blanchet@48975
  1146
  unfolding bij_betw_def by auto
blanchet@48975
  1147
  def f1 \<equiv> "inv_into {..<Suc n1} e1"
blanchet@48975
  1148
  have f1: "bij_betw f1 B1 {..<Suc n1}"
blanchet@48975
  1149
  and f1e1[simp]: "\<And> i1. i1 < Suc n1 \<Longrightarrow> f1 (e1 i1) = i1"
blanchet@48975
  1150
  and e1f1[simp]: "\<And> b1. b1 \<in> B1 \<Longrightarrow> e1 (f1 b1) = b1" unfolding f1_def
blanchet@48975
  1151
  apply (metis bij_betw_inv_into e1, metis bij_betw_inv_into_left e1 lessThan_iff)
blanchet@48975
  1152
  by (metis e1_surj f_inv_into_f)
blanchet@48975
  1153
  (*  *)
blanchet@48975
  1154
  obtain n2 where "card B2 = Suc n2" using B2 by (metis card_insert finite.simps)
blanchet@48975
  1155
  then obtain e2 where e2: "bij_betw e2 {..<Suc n2} B2"
blanchet@48975
  1156
  using ex_bij_betw_finite_nat[OF B2(2)] by (metis atLeast0LessThan bij_betw_the_inv_into)
blanchet@48975
  1157
  hence e2_inj: "inj_on e2 {..<Suc n2}" and e2_surj: "e2 ` {..<Suc n2} = B2"
blanchet@48975
  1158
  unfolding bij_betw_def by auto
blanchet@48975
  1159
  def f2 \<equiv> "inv_into {..<Suc n2} e2"
blanchet@48975
  1160
  have f2: "bij_betw f2 B2 {..<Suc n2}"
blanchet@48975
  1161
  and f2e2[simp]: "\<And> i2. i2 < Suc n2 \<Longrightarrow> f2 (e2 i2) = i2"
blanchet@48975
  1162
  and e2f2[simp]: "\<And> b2. b2 \<in> B2 \<Longrightarrow> e2 (f2 b2) = b2" unfolding f2_def
blanchet@48975
  1163
  apply (metis bij_betw_inv_into e2, metis bij_betw_inv_into_left e2 lessThan_iff)
blanchet@48975
  1164
  by (metis e2_surj f_inv_into_f)
blanchet@48975
  1165
  (*  *)
blanchet@48975
  1166
  let ?ct1 = "N1 o e1"  let ?ct2 = "N2 o e2"
blanchet@48975
  1167
  have ss: "setsum ?ct1 {..<Suc n1} = setsum ?ct2 {..<Suc n2}"
blanchet@48975
  1168
  unfolding setsum_reindex[OF e1_inj, symmetric] setsum_reindex[OF e2_inj, symmetric]
blanchet@48975
  1169
  e1_surj e2_surj using ss .
blanchet@48975
  1170
  obtain ct where
blanchet@48975
  1171
  ct1: "\<And> i1. i1 \<le> n1 \<Longrightarrow> setsum (\<lambda> i2. ct i1 i2) {..<Suc n2} = ?ct1 i1" and
blanchet@48975
  1172
  ct2: "\<And> i2. i2 \<le> n2 \<Longrightarrow> setsum (\<lambda> i1. ct i1 i2) {..<Suc n1} = ?ct2 i2"
blanchet@48975
  1173
  using matrix_count[OF ss] by blast
blanchet@48975
  1174
  (*  *)
blanchet@48975
  1175
  def A \<equiv> "{u b1 b2 | b1 b2. b1 \<in> B1 \<and> b2 \<in> B2}"
blanchet@48975
  1176
  have "\<forall> a \<in> A. \<exists> b1b2 \<in> B1 <*> B2. u (fst b1b2) (snd b1b2) = a"
blanchet@48975
  1177
  unfolding A_def Ball_def mem_Collect_eq by auto
blanchet@48975
  1178
  then obtain h1h2 where h12:
blanchet@48975
  1179
  "\<And>a. a \<in> A \<Longrightarrow> u (fst (h1h2 a)) (snd (h1h2 a)) = a \<and> h1h2 a \<in> B1 <*> B2" by metis
blanchet@48975
  1180
  def h1 \<equiv> "fst o h1h2"  def h2 \<equiv> "snd o h1h2"
blanchet@48975
  1181
  have h12[simp]: "\<And>a. a \<in> A \<Longrightarrow> u (h1 a) (h2 a) = a"
blanchet@48975
  1182
                  "\<And> a. a \<in> A \<Longrightarrow> h1 a \<in> B1"  "\<And> a. a \<in> A \<Longrightarrow> h2 a \<in> B2"
blanchet@48975
  1183
  using h12 unfolding h1_def h2_def by force+
blanchet@48975
  1184
  {fix b1 b2 assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2"
blanchet@48975
  1185
   hence inA: "u b1 b2 \<in> A" unfolding A_def by auto
blanchet@48975
  1186
   hence "u b1 b2 = u (h1 (u b1 b2)) (h2 (u b1 b2))" by auto
blanchet@48975
  1187
   moreover have "h1 (u b1 b2) \<in> B1" "h2 (u b1 b2) \<in> B2" using inA by auto
blanchet@48975
  1188
   ultimately have "h1 (u b1 b2) = b1 \<and> h2 (u b1 b2) = b2"
blanchet@48975
  1189
   using u b1 b2 unfolding inj2_def by fastforce
blanchet@48975
  1190
  }
blanchet@48975
  1191
  hence h1[simp]: "\<And> b1 b2. \<lbrakk>b1 \<in> B1; b2 \<in> B2\<rbrakk> \<Longrightarrow> h1 (u b1 b2) = b1" and
blanchet@48975
  1192
        h2[simp]: "\<And> b1 b2. \<lbrakk>b1 \<in> B1; b2 \<in> B2\<rbrakk> \<Longrightarrow> h2 (u b1 b2) = b2" by auto
blanchet@48975
  1193
  def M \<equiv> "\<lambda> a. ct (f1 (h1 a)) (f2 (h2 a))"
blanchet@48975
  1194
  show ?thesis
blanchet@48975
  1195
  apply(rule exI[of _ M]) proof safe
blanchet@48975
  1196
    fix b1 assume b1: "b1 \<in> B1"
blanchet@48975
  1197
    hence f1b1: "f1 b1 \<le> n1" using f1 unfolding bij_betw_def
blanchet@48975
  1198
    by (metis bij_betwE f1 lessThan_iff less_Suc_eq_le)
blanchet@48975
  1199
    have "(\<Sum>b2\<in>B2. M (u b1 b2)) = (\<Sum>i2<Suc n2. ct (f1 b1) (f2 (e2 i2)))"
blanchet@48975
  1200
    unfolding e2_surj[symmetric] setsum_reindex[OF e2_inj]
blanchet@48975
  1201
    unfolding M_def comp_def apply(intro setsum_cong) apply force
blanchet@48975
  1202
    by (metis e2_surj b1 h1 h2 imageI)
blanchet@48975
  1203
    also have "... = N1 b1" using b1 ct1[OF f1b1] by simp
blanchet@48975
  1204
    finally show "(\<Sum>b2\<in>B2. M (u b1 b2)) = N1 b1" .
blanchet@48975
  1205
  next
blanchet@48975
  1206
    fix b2 assume b2: "b2 \<in> B2"
blanchet@48975
  1207
    hence f2b2: "f2 b2 \<le> n2" using f2 unfolding bij_betw_def
blanchet@48975
  1208
    by (metis bij_betwE f2 lessThan_iff less_Suc_eq_le)
blanchet@48975
  1209
    have "(\<Sum>b1\<in>B1. M (u b1 b2)) = (\<Sum>i1<Suc n1. ct (f1 (e1 i1)) (f2 b2))"
blanchet@48975
  1210
    unfolding e1_surj[symmetric] setsum_reindex[OF e1_inj]
blanchet@48975
  1211
    unfolding M_def comp_def apply(intro setsum_cong) apply force
blanchet@48975
  1212
    by (metis e1_surj b2 h1 h2 imageI)
blanchet@48975
  1213
    also have "... = N2 b2" using b2 ct2[OF f2b2] by simp
blanchet@48975
  1214
    finally show "(\<Sum>b1\<in>B1. M (u b1 b2)) = N2 b2" .
blanchet@48975
  1215
  qed
blanchet@48975
  1216
qed
blanchet@48975
  1217
blanchet@48975
  1218
lemma supp_vimage_mmap:
blanchet@48975
  1219
assumes "M \<in> multiset"
blanchet@48975
  1220
shows "supp M \<subseteq> f -` (supp (mmap f M))"
blanchet@48975
  1221
using assms by (auto simp: mmap_image)
blanchet@48975
  1222
blanchet@48975
  1223
lemma mmap_ge_0:
blanchet@48975
  1224
assumes "M \<in> multiset"
blanchet@48975
  1225
shows "0 < mmap f M b \<longleftrightarrow> (\<exists>a. 0 < M a \<and> f a = b)"
blanchet@48975
  1226
proof-
blanchet@48975
  1227
  have f: "finite {a. f a = b \<and> 0 < M a}" using assms unfolding multiset_def by auto
blanchet@48975
  1228
  show ?thesis unfolding mmap_def setsum_gt_0_iff[OF f] by auto
blanchet@48975
  1229
qed
blanchet@48975
  1230
blanchet@48975
  1231
lemma finite_twosets:
blanchet@48975
  1232
assumes "finite B1" and "finite B2"
blanchet@48975
  1233
shows "finite {u b1 b2 |b1 b2. b1 \<in> B1 \<and> b2 \<in> B2}"  (is "finite ?A")
blanchet@48975
  1234
proof-
blanchet@48975
  1235
  have A: "?A = (\<lambda> b1b2. u (fst b1b2) (snd b1b2)) ` (B1 <*> B2)" by force
blanchet@48975
  1236
  show ?thesis unfolding A using finite_cartesian_product[OF assms] by auto
blanchet@48975
  1237
qed
blanchet@48975
  1238
blanchet@48975
  1239
lemma wp_mmap:
blanchet@48975
  1240
fixes A :: "'a set" and B1 :: "'b1 set" and B2 :: "'b2 set"
blanchet@48975
  1241
assumes wp: "wpull A B1 B2 f1 f2 p1 p2"
blanchet@48975
  1242
shows
blanchet@48975
  1243
"wpull {M. M \<in> multiset \<and> supp M \<subseteq> A}
blanchet@48975
  1244
       {N1. N1 \<in> multiset \<and> supp N1 \<subseteq> B1} {N2. N2 \<in> multiset \<and> supp N2 \<subseteq> B2}
blanchet@48975
  1245
       (mmap f1) (mmap f2) (mmap p1) (mmap p2)"
blanchet@48975
  1246
unfolding wpull_def proof (safe, unfold Bex_def mem_Collect_eq)
blanchet@48975
  1247
  fix N1 :: "'b1 \<Rightarrow> nat" and N2 :: "'b2 \<Rightarrow> nat"
blanchet@48975
  1248
  assume mmap': "mmap f1 N1 = mmap f2 N2"
blanchet@48975
  1249
  and N1[simp]: "N1 \<in> multiset" "supp N1 \<subseteq> B1"
blanchet@48975
  1250
  and N2[simp]: "N2 \<in> multiset" "supp N2 \<subseteq> B2"
blanchet@48975
  1251
  have mN1[simp]: "mmap f1 N1 \<in> multiset" using N1 by (auto simp: mmap)
blanchet@48975
  1252
  have mN2[simp]: "mmap f2 N2 \<in> multiset" using N2 by (auto simp: mmap)
blanchet@48975
  1253
  def P \<equiv> "mmap f1 N1"
blanchet@48975
  1254
  have P1: "P = mmap f1 N1" and P2: "P = mmap f2 N2" unfolding P_def using mmap' by auto
blanchet@48975
  1255
  note P = P1 P2
blanchet@48975
  1256
  have P_mult[simp]: "P \<in> multiset" unfolding P_def using N1 by auto
blanchet@48975
  1257
  have fin_N1[simp]: "finite (supp N1)" using N1(1) unfolding multiset_def by auto
blanchet@48975
  1258
  have fin_N2[simp]: "finite (supp N2)" using N2(1) unfolding multiset_def by auto
blanchet@48975
  1259
  have fin_P[simp]: "finite (supp P)" using P_mult unfolding multiset_def by auto
blanchet@48975
  1260
  (*  *)
blanchet@48975
  1261
  def set1 \<equiv> "\<lambda> c. {b1 \<in> supp N1. f1 b1 = c}"
blanchet@48975
  1262
  have set1[simp]: "\<And> c b1. b1 \<in> set1 c \<Longrightarrow> f1 b1 = c" unfolding set1_def by auto
blanchet@48975
  1263
  have fin_set1: "\<And> c. c \<in> supp P \<Longrightarrow> finite (set1 c)"
blanchet@48975
  1264
  using N1(1) unfolding set1_def multiset_def by auto
blanchet@48975
  1265
  have set1_NE: "\<And> c. c \<in> supp P \<Longrightarrow> set1 c \<noteq> {}"
blanchet@48975
  1266
  unfolding set1_def P1 mmap_ge_0[OF N1(1)] by auto
blanchet@48975
  1267
  have supp_N1_set1: "supp N1 = (\<Union> c \<in> supp P. set1 c)"
blanchet@48975
  1268
  using supp_vimage_mmap[OF N1(1), of f1] unfolding set1_def P1 by auto
blanchet@48975
  1269
  hence set1_inclN1: "\<And>c. c \<in> supp P \<Longrightarrow> set1 c \<subseteq> supp N1" by auto
blanchet@48975
  1270
  hence set1_incl: "\<And> c. c \<in> supp P \<Longrightarrow> set1 c \<subseteq> B1" using N1(2) by blast
blanchet@48975
  1271
  have set1_disj: "\<And> c c'. c \<noteq> c' \<Longrightarrow> set1 c \<inter> set1 c' = {}"
blanchet@48975
  1272
  unfolding set1_def by auto
blanchet@48975
  1273
  have setsum_set1: "\<And> c. setsum N1 (set1 c) = P c"
blanchet@48975
  1274
  unfolding P1 set1_def mmap_def apply(rule setsum_cong) by auto
blanchet@48975
  1275
  (*  *)
blanchet@48975
  1276
  def set2 \<equiv> "\<lambda> c. {b2 \<in> supp N2. f2 b2 = c}"
blanchet@48975
  1277
  have set2[simp]: "\<And> c b2. b2 \<in> set2 c \<Longrightarrow> f2 b2 = c" unfolding set2_def by auto
blanchet@48975
  1278
  have fin_set2: "\<And> c. c \<in> supp P \<Longrightarrow> finite (set2 c)"
blanchet@48975
  1279
  using N2(1) unfolding set2_def multiset_def by auto
blanchet@48975
  1280
  have set2_NE: "\<And> c. c \<in> supp P \<Longrightarrow> set2 c \<noteq> {}"
blanchet@48975
  1281
  unfolding set2_def P2 mmap_ge_0[OF N2(1)] by auto
blanchet@48975
  1282
  have supp_N2_set2: "supp N2 = (\<Union> c \<in> supp P. set2 c)"
blanchet@48975
  1283
  using supp_vimage_mmap[OF N2(1), of f2] unfolding set2_def P2 by auto
blanchet@48975
  1284
  hence set2_inclN2: "\<And>c. c \<in> supp P \<Longrightarrow> set2 c \<subseteq> supp N2" by auto
blanchet@48975
  1285
  hence set2_incl: "\<And> c. c \<in> supp P \<Longrightarrow> set2 c \<subseteq> B2" using N2(2) by blast
blanchet@48975
  1286
  have set2_disj: "\<And> c c'. c \<noteq> c' \<Longrightarrow> set2 c \<inter> set2 c' = {}"
blanchet@48975
  1287
  unfolding set2_def by auto
blanchet@48975
  1288
  have setsum_set2: "\<And> c. setsum N2 (set2 c) = P c"
blanchet@48975
  1289
  unfolding P2 set2_def mmap_def apply(rule setsum_cong) by auto
blanchet@48975
  1290
  (*  *)
blanchet@48975
  1291
  have ss: "\<And> c. c \<in> supp P \<Longrightarrow> setsum N1 (set1 c) = setsum N2 (set2 c)"
blanchet@48975
  1292
  unfolding setsum_set1 setsum_set2 ..
blanchet@48975
  1293
  have "\<forall> c \<in> supp P. \<forall> b1b2 \<in> (set1 c) \<times> (set2 c).
blanchet@48975
  1294
          \<exists> a \<in> A. p1 a = fst b1b2 \<and> p2 a = snd b1b2"
blanchet@48975
  1295
  using wp set1_incl set2_incl unfolding wpull_def Ball_def mem_Collect_eq
blanchet@48975
  1296
  by simp (metis set1 set2 set_rev_mp)
blanchet@48975
  1297
  then obtain uu where uu:
blanchet@48975
  1298
  "\<forall> c \<in> supp P. \<forall> b1b2 \<in> (set1 c) \<times> (set2 c).
blanchet@48975
  1299
     uu c b1b2 \<in> A \<and> p1 (uu c b1b2) = fst b1b2 \<and> p2 (uu c b1b2) = snd b1b2" by metis
blanchet@48975
  1300
  def u \<equiv> "\<lambda> c b1 b2. uu c (b1,b2)"
blanchet@48975
  1301
  have u[simp]:
blanchet@48975
  1302
  "\<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"
blanchet@48975
  1303
  "\<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"
blanchet@48975
  1304
  "\<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"
blanchet@48975
  1305
  using uu unfolding u_def by auto
blanchet@48975
  1306
  {fix c assume c: "c \<in> supp P"
blanchet@48975
  1307
   have "inj2 (u c) (set1 c) (set2 c)" unfolding inj2_def proof clarify
blanchet@48975
  1308
     fix b1 b1' b2 b2'
blanchet@48975
  1309
     assume "{b1, b1'} \<subseteq> set1 c" "{b2, b2'} \<subseteq> set2 c" and 0: "u c b1 b2 = u c b1' b2'"
blanchet@48975
  1310
     hence "p1 (u c b1 b2) = b1 \<and> p2 (u c b1 b2) = b2 \<and>
blanchet@48975
  1311
            p1 (u c b1' b2') = b1' \<and> p2 (u c b1' b2') = b2'"
blanchet@48975
  1312
     using u(2)[OF c] u(3)[OF c] by simp metis
blanchet@48975
  1313
     thus "b1 = b1' \<and> b2 = b2'" using 0 by auto
blanchet@48975
  1314
   qed
blanchet@48975
  1315
  } note inj = this
blanchet@48975
  1316
  def sset \<equiv> "\<lambda> c. {u c b1 b2 | b1 b2. b1 \<in> set1 c \<and> b2 \<in> set2 c}"
blanchet@48975
  1317
  have fin_sset[simp]: "\<And> c. c \<in> supp P \<Longrightarrow> finite (sset c)" unfolding sset_def
blanchet@48975
  1318
  using fin_set1 fin_set2 finite_twosets by blast
blanchet@48975
  1319
  have sset_A: "\<And> c. c \<in> supp P \<Longrightarrow> sset c \<subseteq> A" unfolding sset_def by auto
blanchet@48975
  1320
  {fix c a assume c: "c \<in> supp P" and ac: "a \<in> sset c"
blanchet@48975
  1321
   then obtain b1 b2 where b1: "b1 \<in> set1 c" and b2: "b2 \<in> set2 c"
blanchet@48975
  1322
   and a: "a = u c b1 b2" unfolding sset_def by auto
blanchet@48975
  1323
   have "p1 a \<in> set1 c" and p2a: "p2 a \<in> set2 c"
blanchet@48975
  1324
   using ac a b1 b2 c u(2) u(3) by simp+
blanchet@48975
  1325
   hence "u c (p1 a) (p2 a) = a" unfolding a using b1 b2 inj[OF c]
blanchet@48975
  1326
   unfolding inj2_def by (metis c u(2) u(3))
blanchet@48975
  1327
  } note u_p12[simp] = this
blanchet@48975
  1328
  {fix c a assume c: "c \<in> supp P" and ac: "a \<in> sset c"
blanchet@48975
  1329
   hence "p1 a \<in> set1 c" unfolding sset_def by auto
blanchet@48975
  1330
  }note p1[simp] = this
blanchet@48975
  1331
  {fix c a assume c: "c \<in> supp P" and ac: "a \<in> sset c"
blanchet@48975
  1332
   hence "p2 a \<in> set2 c" unfolding sset_def by auto
blanchet@48975
  1333
  }note p2[simp] = this
blanchet@48975
  1334
  (*  *)
blanchet@48975
  1335
  {fix c assume c: "c \<in> supp P"
blanchet@48975
  1336
   hence "\<exists> M. (\<forall> b1 \<in> set1 c. setsum (\<lambda> b2. M (u c b1 b2)) (set2 c) = N1 b1) \<and>
blanchet@48975
  1337
               (\<forall> b2 \<in> set2 c. setsum (\<lambda> b1. M (u c b1 b2)) (set1 c) = N2 b2)"
blanchet@48975
  1338
   unfolding sset_def
blanchet@48975
  1339
   using matrix_count_finite[OF set1_NE[OF c] fin_set1[OF c]
blanchet@48975
  1340
                                set2_NE[OF c] fin_set2[OF c] inj[OF c] ss[OF c]] by auto
blanchet@48975
  1341
  }
blanchet@48975
  1342
  then obtain Ms where
blanchet@48975
  1343
  ss1: "\<And> c b1. \<lbrakk>c \<in> supp P; b1 \<in> set1 c\<rbrakk> \<Longrightarrow>
blanchet@48975
  1344
                   setsum (\<lambda> b2. Ms c (u c b1 b2)) (set2 c) = N1 b1" and
blanchet@48975
  1345
  ss2: "\<And> c b2. \<lbrakk>c \<in> supp P; b2 \<in> set2 c\<rbrakk> \<Longrightarrow>
blanchet@48975
  1346
                   setsum (\<lambda> b1. Ms c (u c b1 b2)) (set1 c) = N2 b2"
blanchet@48975
  1347
  by metis
blanchet@48975
  1348
  def SET \<equiv> "\<Union> c \<in> supp P. sset c"
blanchet@48975
  1349
  have fin_SET[simp]: "finite SET" unfolding SET_def apply(rule finite_UN_I) by auto
blanchet@48975
  1350
  have SET_A: "SET \<subseteq> A" unfolding SET_def using sset_A by auto
blanchet@48975
  1351
  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"
blanchet@48975
  1352
  unfolding SET_def sset_def by blast
blanchet@48975
  1353
  {fix c a assume c: "c \<in> supp P" and a: "a \<in> SET" and p1a: "p1 a \<in> set1 c"
blanchet@48975
  1354
   then obtain c' where c': "c' \<in> supp P" and ac': "a \<in> sset c'"
blanchet@48975
  1355
   unfolding SET_def by auto
blanchet@48975
  1356
   hence "p1 a \<in> set1 c'" unfolding sset_def by auto
blanchet@48975
  1357
   hence eq: "c = c'" using p1a c c' set1_disj by auto
blanchet@48975
  1358
   hence "a \<in> sset c" using ac' by simp
blanchet@48975
  1359
  } note p1_rev = this
blanchet@48975
  1360
  {fix c a assume c: "c \<in> supp P" and a: "a \<in> SET" and p2a: "p2 a \<in> set2 c"
blanchet@48975
  1361
   then obtain c' where c': "c' \<in> supp P" and ac': "a \<in> sset c'"
blanchet@48975
  1362
   unfolding SET_def by auto
blanchet@48975
  1363
   hence "p2 a \<in> set2 c'" unfolding sset_def by auto
blanchet@48975
  1364
   hence eq: "c = c'" using p2a c c' set2_disj by auto
blanchet@48975
  1365
   hence "a \<in> sset c" using ac' by simp
blanchet@48975
  1366
  } note p2_rev = this
blanchet@48975
  1367
  (*  *)
blanchet@48975
  1368
  have "\<forall> a \<in> SET. \<exists> c \<in> supp P. a \<in> sset c" unfolding SET_def by auto
blanchet@48975
  1369
  then obtain h where h: "\<forall> a \<in> SET. h a \<in> supp P \<and> a \<in> sset (h a)" by metis
blanchet@48975
  1370
  have h_u[simp]: "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
blanchet@48975
  1371
                      \<Longrightarrow> h (u c b1 b2) = c"
blanchet@48975
  1372
  by (metis h p2 set2 u(3) u_SET)
blanchet@48975
  1373
  have h_u1: "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
blanchet@48975
  1374
                      \<Longrightarrow> h (u c b1 b2) = f1 b1"
blanchet@48975
  1375
  using h unfolding sset_def by auto
blanchet@48975
  1376
  have h_u2: "\<And> c b1 b2. \<lbrakk>c \<in> supp P; b1 \<in> set1 c; b2 \<in> set2 c\<rbrakk>
blanchet@48975
  1377
                      \<Longrightarrow> h (u c b1 b2) = f2 b2"
blanchet@48975
  1378
  using h unfolding sset_def by auto
blanchet@48975
  1379
  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"
blanchet@48975
  1380
  have sM: "supp M \<subseteq> SET" "supp M \<subseteq> p1 -` (supp N1)" "supp M \<subseteq> p2 -` (supp N2)"
blanchet@48975
  1381
  unfolding M_def by auto
blanchet@48975
  1382
  show "\<exists>M. (M \<in> multiset \<and> supp M \<subseteq> A) \<and> mmap p1 M = N1 \<and> mmap p2 M = N2"
blanchet@48975
  1383
  proof(rule exI[of _ M], safe)
blanchet@48975
  1384
    show "M \<in> multiset"
blanchet@48975
  1385
    unfolding multiset_def using finite_subset[OF sM(1) fin_SET] by simp
blanchet@48975
  1386
  next
blanchet@48975
  1387
    fix a assume "0 < M a"
blanchet@48975
  1388
    thus "a \<in> A" unfolding M_def using SET_A by (cases "a \<in> SET") auto
blanchet@48975
  1389
  next
blanchet@48975
  1390
    show "mmap p1 M = N1"
blanchet@48975
  1391
    unfolding mmap_def[abs_def] proof(rule ext)
blanchet@48975
  1392
      fix b1
blanchet@48975
  1393
      let ?K = "{a. p1 a = b1 \<and> 0 < M a}"
blanchet@48975
  1394
      show "setsum M ?K = N1 b1"
blanchet@48975
  1395
      proof(cases "b1 \<in> supp N1")
blanchet@48975
  1396
        case False
blanchet@48975
  1397
        hence "?K = {}" using sM(2) by auto
blanchet@48975
  1398
        thus ?thesis using False by auto
blanchet@48975
  1399
      next
blanchet@48975
  1400
        case True
blanchet@48975
  1401
        def c \<equiv> "f1 b1"
blanchet@48975
  1402
        have c: "c \<in> supp P" and b1: "b1 \<in> set1 c"
blanchet@48975
  1403
        unfolding set1_def c_def P1 using True by (auto simp: mmap_image)
blanchet@48975
  1404
        have "setsum M ?K = setsum M {a. p1 a = b1 \<and> a \<in> SET}"
blanchet@48975
  1405
        apply(rule setsum_mono_zero_cong_left) unfolding M_def by auto
blanchet@48975
  1406
        also have "... = setsum M ((\<lambda> b2. u c b1 b2) ` (set2 c))"
blanchet@48975
  1407
        apply(rule setsum_cong) using c b1 proof safe
blanchet@48975
  1408
          fix a assume p1a: "p1 a \<in> set1 c" and "0 < P c" and "a \<in> SET"
blanchet@48975
  1409
          hence ac: "a \<in> sset c" using p1_rev by auto
blanchet@48975
  1410
          hence "a = u c (p1 a) (p2 a)" using c by auto
blanchet@48975
  1411
          moreover have "p2 a \<in> set2 c" using ac c by auto
blanchet@48975
  1412
          ultimately show "a \<in> u c (p1 a) ` set2 c" by auto
blanchet@48975
  1413
        next
blanchet@48975
  1414
          fix b2 assume b1: "b1 \<in> set1 c" and b2: "b2 \<in> set2 c"
blanchet@48975
  1415
          hence "u c b1 b2 \<in> SET" using c by auto
blanchet@48975
  1416
        qed auto
blanchet@48975
  1417
        also have "... = setsum (\<lambda> b2. M (u c b1 b2)) (set2 c)"
blanchet@48975
  1418
        unfolding comp_def[symmetric] apply(rule setsum_reindex)
blanchet@48975
  1419
        using inj unfolding inj_on_def inj2_def using b1 c u(3) by blast
blanchet@48975
  1420
        also have "... = N1 b1" unfolding ss1[OF c b1, symmetric]
blanchet@48975
  1421
          apply(rule setsum_cong[OF refl]) unfolding M_def
blanchet@48975
  1422
          using True h_u[OF c b1] set2_def u(2,3)[OF c b1] u_SET[OF c b1] by fastforce
blanchet@48975
  1423
        finally show ?thesis .
blanchet@48975
  1424
      qed
blanchet@48975
  1425
    qed
blanchet@48975
  1426
  next
blanchet@48975
  1427
    show "mmap p2 M = N2"
blanchet@48975
  1428
    unfolding mmap_def[abs_def] proof(rule ext)
blanchet@48975
  1429
      fix b2
blanchet@48975
  1430
      let ?K = "{a. p2 a = b2 \<and> 0 < M a}"
blanchet@48975
  1431
      show "setsum M ?K = N2 b2"
blanchet@48975
  1432
      proof(cases "b2 \<in> supp N2")
blanchet@48975
  1433
        case False
blanchet@48975
  1434
        hence "?K = {}" using sM(3) by auto
blanchet@48975
  1435
        thus ?thesis using False by auto
blanchet@48975
  1436
      next
blanchet@48975
  1437
        case True
blanchet@48975
  1438
        def c \<equiv> "f2 b2"
blanchet@48975
  1439
        have c: "c \<in> supp P" and b2: "b2 \<in> set2 c"
blanchet@48975
  1440
        unfolding set2_def c_def P2 using True by (auto simp: mmap_image)
blanchet@48975
  1441
        have "setsum M ?K = setsum M {a. p2 a = b2 \<and> a \<in> SET}"
blanchet@48975
  1442
        apply(rule setsum_mono_zero_cong_left) unfolding M_def by auto
blanchet@48975
  1443
        also have "... = setsum M ((\<lambda> b1. u c b1 b2) ` (set1 c))"
blanchet@48975
  1444
        apply(rule setsum_cong) using c b2 proof safe
blanchet@48975
  1445
          fix a assume p2a: "p2 a \<in> set2 c" and "0 < P c" and "a \<in> SET"
blanchet@48975
  1446
          hence ac: "a \<in> sset c" using p2_rev by auto
blanchet@48975
  1447
          hence "a = u c (p1 a) (p2 a)" using c by auto
blanchet@48975
  1448
          moreover have "p1 a \<in> set1 c" using ac c by auto
blanchet@48975
  1449
          ultimately show "a \<in> (\<lambda>b1. u c b1 (p2 a)) ` set1 c" by auto
blanchet@48975
  1450
        next
blanchet@48975
  1451
          fix b2 assume b1: "b1 \<in> set1 c" and b2: "b2 \<in> set2 c"
blanchet@48975
  1452
          hence "u c b1 b2 \<in> SET" using c by auto
blanchet@48975
  1453
        qed auto
blanchet@48975
  1454
        also have "... = setsum (M o (\<lambda> b1. u c b1 b2)) (set1 c)"
blanchet@48975
  1455
        apply(rule setsum_reindex)
blanchet@48975
  1456
        using inj unfolding inj_on_def inj2_def using b2 c u(2) by blast
blanchet@48975
  1457
        also have "... = setsum (\<lambda> b1. M (u c b1 b2)) (set1 c)"
blanchet@48975
  1458
        unfolding comp_def[symmetric] by simp
blanchet@48975
  1459
        also have "... = N2 b2" unfolding ss2[OF c b2, symmetric]
blanchet@48975
  1460
          apply(rule setsum_cong[OF refl]) unfolding M_def set2_def
blanchet@48975
  1461
          using True h_u1[OF c _ b2] u(2,3)[OF c _ b2] u_SET[OF c _ b2]
blanchet@48975
  1462
          unfolding set1_def by fastforce
blanchet@48975
  1463
        finally show ?thesis .
blanchet@48975
  1464
      qed
blanchet@48975
  1465
    qed
blanchet@48975
  1466
  qed
blanchet@48975
  1467
qed
blanchet@48975
  1468
blanchet@48975
  1469
definition mset_map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a multiset \<Rightarrow> 'b multiset" where
blanchet@48975
  1470
"mset_map h = Abs_multiset \<circ> mmap h \<circ> count"
blanchet@48975
  1471
blanchet@48975
  1472
bnf_def mset = mset_map [set_of] "\<lambda>_::'a multiset. natLeq" ["{#}"]
blanchet@48975
  1473
unfolding mset_map_def
blanchet@48975
  1474
proof -
blanchet@48975
  1475
  show "Abs_multiset \<circ> mmap id \<circ> count = id" unfolding mmap_id by (auto simp: count_inverse)
blanchet@48975
  1476
next
blanchet@48975
  1477
  fix f g
blanchet@48975
  1478
  show "Abs_multiset \<circ> mmap (g \<circ> f) \<circ> count =
blanchet@48975
  1479
        Abs_multiset \<circ> mmap g \<circ> count \<circ> (Abs_multiset \<circ> mmap f \<circ> count)"
blanchet@48975
  1480
  unfolding comp_def apply(rule ext)
blanchet@48975
  1481
  by (auto simp: Abs_multiset_inverse count mmap_comp1 mmap)
blanchet@48975
  1482
next
blanchet@48975
  1483
  fix M f g assume eq: "\<And>a. a \<in> set_of M \<Longrightarrow> f a = g a"
blanchet@48975
  1484
  thus "(Abs_multiset \<circ> mmap f \<circ> count) M = (Abs_multiset \<circ> mmap g \<circ> count) M" apply auto
blanchet@48975
  1485
  unfolding cIm_def[abs_def] image_def
blanchet@48975
  1486
  by (auto intro!: mmap_cong simp: Abs_multiset_inject count mmap)
blanchet@48975
  1487
next
blanchet@48975
  1488
  fix f show "set_of \<circ> (Abs_multiset \<circ> mmap f \<circ> count) = op ` f \<circ> set_of"
blanchet@48975
  1489
  by (auto simp: count mmap mmap_image set_of_Abs_multiset supp_count)
blanchet@48975
  1490
next
blanchet@48975
  1491
  show "card_order natLeq" by (rule natLeq_card_order)
blanchet@48975
  1492
next
blanchet@48975
  1493
  show "cinfinite natLeq" by (rule natLeq_cinfinite)
blanchet@48975
  1494
next
blanchet@48975
  1495
  fix M show "|set_of M| \<le>o natLeq"
blanchet@48975
  1496
  apply(rule ordLess_imp_ordLeq)
blanchet@48975
  1497
  unfolding finite_iff_ordLess_natLeq[symmetric] using finite_set_of .
blanchet@48975
  1498
next
blanchet@48975
  1499
  fix A :: "'a set"
blanchet@48975
  1500
  have "|{M. set_of M \<subseteq> A}| \<le>o |{as. set as \<subseteq> A}|" using card_of_set_of .
blanchet@48975
  1501
  also have "|{as. set as \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq"
blanchet@48975
  1502
  by (rule list_in_bd)
blanchet@48975
  1503
  finally show "|{M. set_of M \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" .
blanchet@48975
  1504
next
blanchet@48975
  1505
  fix A B1 B2 f1 f2 p1 p2
blanchet@48975
  1506
  let ?map = "\<lambda> f. Abs_multiset \<circ> mmap f \<circ> count"
blanchet@48975
  1507
  assume wp: "wpull A B1 B2 f1 f2 p1 p2"
blanchet@48975
  1508
  show "wpull {x. set_of x \<subseteq> A} {x. set_of x \<subseteq> B1} {x. set_of x \<subseteq> B2}
blanchet@48975
  1509
              (?map f1) (?map f2) (?map p1) (?map p2)"
blanchet@48975
  1510
  unfolding wpull_def proof safe
blanchet@48975
  1511
    fix y1 y2
blanchet@48975
  1512
    assume y1: "set_of y1 \<subseteq> B1" and y2: "set_of y2 \<subseteq> B2"
blanchet@48975
  1513
    and m: "?map f1 y1 = ?map f2 y2"
blanchet@48975
  1514
    def N1 \<equiv> "count y1"  def N2 \<equiv> "count y2"
blanchet@48975
  1515
    have "N1 \<in> multiset \<and> supp N1 \<subseteq> B1" and "N2 \<in> multiset \<and> supp N2 \<subseteq> B2"
blanchet@48975
  1516
    and "mmap f1 N1 = mmap f2 N2"
blanchet@48975
  1517
    using y1 y2 m unfolding N1_def N2_def
blanchet@48975
  1518
    by (auto simp: Abs_multiset_inject count mmap)
blanchet@48975
  1519
    then obtain M where M: "M \<in> multiset \<and> supp M \<subseteq> A"
blanchet@48975
  1520
    and N1: "mmap p1 M = N1" and N2: "mmap p2 M = N2"
blanchet@48975
  1521
    using wp_mmap[OF wp] unfolding wpull_def by auto
blanchet@48975
  1522
    def x \<equiv> "Abs_multiset M"
blanchet@48975
  1523
    show "\<exists>x\<in>{x. set_of x \<subseteq> A}. ?map p1 x = y1 \<and> ?map p2 x = y2"
blanchet@48975
  1524
    apply(intro bexI[of _ x]) using M N1 N2 unfolding N1_def N2_def x_def
blanchet@48975
  1525
    by (auto simp: count_inverse Abs_multiset_inverse)
blanchet@48975
  1526
  qed
blanchet@48975
  1527
qed (unfold set_of_empty, auto)
blanchet@48975
  1528
blanchet@48975
  1529
end