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.68 -qed (simp add: wpull_map)+
    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>