src/HOL/BNF/More_BNFs.thy
 changeset 54841 af71b753c459 parent 54539 bbab2ebda234 child 55066 4e5ddf3162ac
```     1.1 --- a/src/HOL/BNF/More_BNFs.thy	Fri Dec 20 21:09:01 2013 +0100
1.2 +++ b/src/HOL/BNF/More_BNFs.thy	Wed Dec 18 11:03:40 2013 +0100
1.3 @@ -50,18 +50,9 @@
1.4    show "|Option.set x| \<le>o natLeq"
1.5      by (cases x) (simp_all add: ordLess_imp_ordLeq finite_iff_ordLess_natLeq[symmetric])
1.6  next
1.7 -  fix A B1 B2 f1 f2 p1 p2
1.8 -  assume wpull: "wpull A B1 B2 f1 f2 p1 p2"
1.9 -  show "wpull {x. Option.set x \<subseteq> A} {x. Option.set x \<subseteq> B1} {x. Option.set x \<subseteq> B2}
1.10 -    (Option.map f1) (Option.map f2) (Option.map p1) (Option.map p2)"
1.11 -    (is "wpull ?A ?B1 ?B2 ?f1 ?f2 ?p1 ?p2")
1.12 -    unfolding wpull_def
1.13 -  proof (intro strip, elim conjE)
1.14 -    fix b1 b2
1.15 -    assume "b1 \<in> ?B1" "b2 \<in> ?B2" "?f1 b1 = ?f2 b2"
1.16 -    thus "\<exists>a \<in> ?A. ?p1 a = b1 \<and> ?p2 a = b2" using wpull
1.17 -      unfolding wpull_def by (cases b2) (auto 4 5)
1.18 -  qed
1.19 +  fix R S
1.20 +  show "option_rel R OO option_rel S \<le> option_rel (R OO S)"
1.21 +    by (auto simp: option_rel_def split: option.splits)
1.22  next
1.23    fix z
1.24    assume "z \<in> Option.set None"
1.25 @@ -76,28 +67,6 @@
1.26             split: option.splits)
1.27  qed
1.28
1.29 -lemma wpull_map:
1.30 -  assumes "wpull A B1 B2 f1 f2 p1 p2"
1.31 -  shows "wpull {x. set x \<subseteq> A} {x. set x \<subseteq> B1} {x. set x \<subseteq> B2} (map f1) (map f2) (map p1) (map p2)"
1.32 -    (is "wpull ?A ?B1 ?B2 _ _ _ _")
1.33 -proof (unfold wpull_def)
1.34 -  { fix as bs assume *: "as \<in> ?B1" "bs \<in> ?B2" "map f1 as = map f2 bs"
1.35 -    hence "length as = length bs" by (metis length_map)
1.36 -    hence "\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs" using *
1.37 -    proof (induct as bs rule: list_induct2)
1.38 -      case (Cons a as b bs)
1.39 -      hence "a \<in> B1" "b \<in> B2" "f1 a = f2 b" by auto
1.40 -      with assms obtain z where "z \<in> A" "p1 z = a" "p2 z = b" unfolding wpull_def by blast
1.41 -      moreover
1.42 -      from Cons obtain zs where "zs \<in> ?A" "map p1 zs = as" "map p2 zs = bs" by auto
1.43 -      ultimately have "z # zs \<in> ?A" "map p1 (z # zs) = a # as \<and> map p2 (z # zs) = b # bs" by auto
1.44 -      thus ?case by (rule_tac x = "z # zs" in bexI)
1.45 -    qed simp
1.46 -  }
1.47 -  thus "\<forall>as bs. as \<in> ?B1 \<and> bs \<in> ?B2 \<and> map f1 as = map f2 bs \<longrightarrow>
1.48 -    (\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs)" by blast
1.49 -qed
1.50 -
1.51  bnf "'a list"
1.52    map: map
1.53    sets: set
1.54 @@ -125,50 +94,21 @@
1.55    show "|set x| \<le>o natLeq"
1.56      by (metis List.finite_set finite_iff_ordLess_natLeq ordLess_imp_ordLeq)
1.57  next
1.58 +  fix R S
1.59 +  show "list_all2 R OO list_all2 S \<le> list_all2 (R OO S)"
1.60 +    by (metis list_all2_OO order_refl)
1.61 +next
1.62    fix R
1.63    show "list_all2 R =
1.64           (Grp {x. set x \<subseteq> {(x, y). R x y}} (map fst))\<inverse>\<inverse> OO
1.65           Grp {x. set x \<subseteq> {(x, y). R x y}} (map snd)"
1.66      unfolding list_all2_def[abs_def] Grp_def fun_eq_iff relcompp.simps conversep.simps
1.67      by (force simp: zip_map_fst_snd)
1.69 +qed simp_all
1.70
1.71
1.72  (* Finite sets *)
1.73
1.74 -lemma wpull_image:
1.75 -  assumes "wpull A B1 B2 f1 f2 p1 p2"
1.76 -  shows "wpull (Pow A) (Pow B1) (Pow B2) (image f1) (image f2) (image p1) (image p2)"
1.77 -unfolding wpull_def Pow_def Bex_def mem_Collect_eq proof clarify
1.78 -  fix Y1 Y2 assume Y1: "Y1 \<subseteq> B1" and Y2: "Y2 \<subseteq> B2" and EQ: "f1 ` Y1 = f2 ` Y2"
1.79 -  def X \<equiv> "{a \<in> A. p1 a \<in> Y1 \<and> p2 a \<in> Y2}"
1.80 -  show "\<exists>X\<subseteq>A. p1 ` X = Y1 \<and> p2 ` X = Y2"
1.81 -  proof (rule exI[of _ X], intro conjI)
1.82 -    show "p1 ` X = Y1"
1.83 -    proof
1.84 -      show "Y1 \<subseteq> p1 ` X"
1.85 -      proof safe
1.86 -        fix y1 assume y1: "y1 \<in> Y1"
1.87 -        then obtain y2 where y2: "y2 \<in> Y2" and eq: "f1 y1 = f2 y2" using EQ by auto
1.88 -        then obtain x where "x \<in> A" and "p1 x = y1" and "p2 x = y2"
1.89 -        using assms y1 Y1 Y2 unfolding wpull_def by blast
1.90 -        thus "y1 \<in> p1 ` X" unfolding X_def using y1 y2 by auto
1.91 -      qed
1.92 -    qed(unfold X_def, auto)
1.93 -    show "p2 ` X = Y2"
1.94 -    proof
1.95 -      show "Y2 \<subseteq> p2 ` X"
1.96 -      proof safe
1.97 -        fix y2 assume y2: "y2 \<in> Y2"
1.98 -        then obtain y1 where y1: "y1 \<in> Y1" and eq: "f1 y1 = f2 y2" using EQ by force
1.99 -        then obtain x where "x \<in> A" and "p1 x = y1" and "p2 x = y2"
1.100 -        using assms y2 Y1 Y2 unfolding wpull_def by blast
1.101 -        thus "y2 \<in> p2 ` X" unfolding X_def using y1 y2 by auto
1.102 -      qed
1.103 -    qed(unfold X_def, auto)
1.104 -  qed(unfold X_def, auto)
1.105 -qed
1.106 -
1.107  context
1.108  includes fset.lifting
1.109  begin
1.110 @@ -206,31 +146,6 @@
1.111    by (transfer, clarsimp, metis fst_conv)
1.112  qed
1.113
1.114 -lemma wpull_fimage:
1.115 -  assumes "wpull A B1 B2 f1 f2 p1 p2"
1.116 -  shows "wpull {x. fset x \<subseteq> A} {x. fset x \<subseteq> B1} {x. fset x \<subseteq> B2}
1.117 -              (fimage f1) (fimage f2) (fimage p1) (fimage p2)"
1.118 -unfolding wpull_def Pow_def Bex_def mem_Collect_eq proof clarify
1.119 -  fix y1 y2
1.120 -  assume Y1: "fset y1 \<subseteq> B1" and Y2: "fset y2 \<subseteq> B2"
1.121 -  assume "fimage f1 y1 = fimage f2 y2"
1.122 -  hence EQ: "f1 ` (fset y1) = f2 ` (fset y2)" by transfer simp
1.123 -  with Y1 Y2 obtain X where X: "X \<subseteq> A" and Y1: "p1 ` X = fset y1" and Y2: "p2 ` X = fset y2"
1.124 -    using wpull_image[OF assms] unfolding wpull_def Pow_def
1.125 -    by (auto elim!: allE[of _ "fset y1"] allE[of _ "fset y2"])
1.126 -  have "\<forall> y1' \<in> fset y1. \<exists> x. x \<in> X \<and> y1' = p1 x" using Y1 by auto
1.127 -  then obtain q1 where q1: "\<forall> y1' \<in> fset y1. q1 y1' \<in> X \<and> y1' = p1 (q1 y1')" by metis
1.128 -  have "\<forall> y2' \<in> fset y2. \<exists> x. x \<in> X \<and> y2' = p2 x" using Y2 by auto
1.129 -  then obtain q2 where q2: "\<forall> y2' \<in> fset y2. q2 y2' \<in> X \<and> y2' = p2 (q2 y2')" by metis
1.130 -  def X' \<equiv> "q1 ` (fset y1) \<union> q2 ` (fset y2)"
1.131 -  have X': "X' \<subseteq> A" and Y1: "p1 ` X' = fset y1" and Y2: "p2 ` X' = fset y2"
1.132 -  using X Y1 Y2 q1 q2 unfolding X'_def by auto
1.133 -  have fX': "finite X'" unfolding X'_def by transfer simp
1.134 -  then obtain x where X'eq: "X' = fset x" by transfer simp
1.135 -  show "\<exists>x. fset x \<subseteq> A \<and> fimage p1 x = y1 \<and> fimage p2 x = y2"
1.136 -     using X' Y1 Y2 by (auto simp: X'eq intro!: exI[of _ "x"]) (transfer, blast)+
1.137 -qed
1.138 -
1.139  bnf "'a fset"
1.140    map: fimage
1.141    sets: fset
1.142 @@ -245,7 +160,7 @@
1.143        apply (rule natLeq_card_order)
1.144       apply (rule natLeq_cinfinite)
1.145      apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq)
1.146 -  apply (erule wpull_fimage)
1.147 +   apply (fastforce simp: fset_rel_alt)
1.148   apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff fset_rel_alt fset_rel_aux)
1.149  apply transfer apply simp
1.150  done
1.151 @@ -550,6 +465,62 @@
1.152    show ?thesis unfolding A using finite_cartesian_product[OF assms] by auto
1.153  qed
1.154
1.155 +(* Weak pullbacks: *)
1.156 +definition wpull where
1.157 +"wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow>
1.158 + (\<forall> 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))"
1.159 +
1.160 +(* Weak pseudo-pullbacks *)
1.161 +definition wppull where
1.162 +"wppull A B1 B2 f1 f2 e1 e2 p1 p2 \<longleftrightarrow>
1.163 + (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow>
1.164 +           (\<exists> a \<in> A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2))"
1.165 +
1.166 +
1.167 +(* The pullback of sets *)
1.168 +definition thePull where
1.169 +"thePull B1 B2 f1 f2 = {(b1,b2). b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2}"
1.170 +
1.171 +lemma wpull_thePull:
1.172 +"wpull (thePull B1 B2 f1 f2) B1 B2 f1 f2 fst snd"
1.173 +unfolding wpull_def thePull_def by auto
1.174 +
1.175 +lemma wppull_thePull:
1.176 +assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
1.177 +shows
1.178 +"\<exists> j. \<forall> a' \<in> thePull B1 B2 f1 f2.
1.179 +   j a' \<in> A \<and>
1.180 +   e1 (p1 (j a')) = e1 (fst a') \<and> e2 (p2 (j a')) = e2 (snd a')"
1.181 +(is "\<exists> j. \<forall> a' \<in> ?A'. ?phi a' (j a')")
1.182 +proof(rule bchoice[of ?A' ?phi], default)
1.183 +  fix a' assume a': "a' \<in> ?A'"
1.184 +  hence "fst a' \<in> B1" unfolding thePull_def by auto
1.185 +  moreover
1.186 +  from a' have "snd a' \<in> B2" unfolding thePull_def by auto
1.187 +  moreover have "f1 (fst a') = f2 (snd a')"
1.188 +  using a' unfolding csquare_def thePull_def by auto
1.189 +  ultimately show "\<exists> ja'. ?phi a' ja'"
1.190 +  using assms unfolding wppull_def by blast
1.191 +qed
1.192 +
1.193 +lemma wpull_wppull:
1.194 +assumes wp: "wpull A' B1 B2 f1 f2 p1' p2'" and
1.195 +1: "\<forall> a' \<in> A'. j a' \<in> A \<and> e1 (p1 (j a')) = e1 (p1' a') \<and> e2 (p2 (j a')) = e2 (p2' a')"
1.196 +shows "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
1.197 +unfolding wppull_def proof safe
1.198 +  fix b1 b2
1.199 +  assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2" and f: "f1 b1 = f2 b2"
1.200 +  then obtain a' where a': "a' \<in> A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'"
1.201 +  using wp unfolding wpull_def by blast
1.202 +  show "\<exists>a\<in>A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2"
1.203 +  apply (rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto
1.204 +qed
1.205 +
1.206 +lemma wppull_fstOp_sndOp:
1.207 +shows "wppull (Collect (split (P OO Q))) (Collect (split P)) (Collect (split Q))
1.208 +  snd fst fst snd (fstOp P Q) (sndOp P Q)"
1.209 +using pick_middlep unfolding wppull_def fstOp_def sndOp_def relcompp.simps by auto
1.210 +
1.211  lemma wpull_mmap:
1.212  fixes A :: "'a set" and B1 :: "'b1 set" and B2 :: "'b2 set"
1.213  assumes wp: "wpull A B1 B2 f1 f2 p1 p2"
1.214 @@ -781,18 +752,33 @@
1.215    by transfer
1.216      (auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def)
1.217
1.218 +lemma wppull_mmap:
1.219 +  assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
1.220 +  shows "wppull {M. set_of M \<subseteq> A} {N1. set_of N1 \<subseteq> B1} {N2. set_of N2 \<subseteq> B2}
1.221 +    (mmap f1) (mmap f2) (mmap e1) (mmap e2) (mmap p1) (mmap p2)"
1.222 +proof -
1.223 +  from assms obtain j where j: "\<forall>a'\<in>thePull B1 B2 f1 f2.
1.224 +    j a' \<in> A \<and> e1 (p1 (j a')) = e1 (fst a') \<and> e2 (p2 (j a')) = e2 (snd a')"
1.225 +    by (blast dest: wppull_thePull)
1.226 +  then show ?thesis
1.227 +    by (intro wpull_wppull[OF wpull_mmap[OF wpull_thePull], of _ _ _ _ "mmap j"])
1.228 +      (auto simp: o_eq_dest_lhs[OF mmap_comp[symmetric]] o_eq_dest[OF set_of_mmap]
1.229 +        intro!: mmap_cong simp del: mem_set_of_iff simp: mem_set_of_iff[symmetric])
1.230 +qed
1.231 +
1.232  bnf "'a multiset"
1.233    map: mmap
1.234    sets: set_of
1.235    bd: natLeq
1.236    wits: "{#}"
1.237  by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd
1.238 -  intro: mmap_cong wpull_mmap)
1.239 +  Grp_def relcompp.simps intro: mmap_cong)
1.240 +  (metis wppull_mmap[OF wppull_fstOp_sndOp, unfolded wppull_def
1.241 +    o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def o_def, simplified])
1.242
1.243  inductive rel_multiset' where
1.244 -Zero: "rel_multiset' R {#} {#}"
1.245 -|
1.246 -Plus: "\<lbrakk>R a b; rel_multiset' R M N\<rbrakk> \<Longrightarrow> rel_multiset' R (M + {#a#}) (N + {#b#})"
1.247 +  Zero[intro]: "rel_multiset' R {#} {#}"
1.248 +| Plus[intro]: "\<lbrakk>R a b; rel_multiset' R M N\<rbrakk> \<Longrightarrow> rel_multiset' R (M + {#a#}) (N + {#b#})"
1.249
1.250  lemma map_multiset_Zero_iff[simp]: "mmap f M = {#} \<longleftrightarrow> M = {#}"
1.251  by (metis image_is_empty multiset.set_map set_of_eq_empty_iff)
1.252 @@ -998,8 +984,6 @@
1.253  (* Advanced relator customization *)
1.254
1.255  (* Set vs. sum relators: *)
1.256 -(* FIXME: All such facts should be declared as simps: *)
1.257 -declare sum_rel_simps[simp]
1.258
1.259  lemma set_rel_sum_rel[simp]:
1.260  "set_rel (sum_rel \<chi> \<phi>) A1 A2 \<longleftrightarrow>
```