1.1 --- a/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy Wed Mar 13 10:47:00 2013 +0100
1.2 +++ b/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy Wed Mar 13 13:23:16 2013 +0100
1.3 @@ -26,12 +26,15 @@
1.4 definition "corec rt qt ct dt \<equiv> dtree_corec rt qt (the_inv fset o ct) (the_inv fset o dt)"
1.5
1.6 lemma finite_cont[simp]: "finite (cont tr)"
1.7 -unfolding cont_def by auto
1.8 + unfolding cont_def o_apply by (cases tr, clarsimp) (transfer, simp)
1.9
1.10 lemma Node_root_cont[simp]:
1.11 -"Node (root tr) (cont tr) = tr"
1.12 -using dtree.collapse unfolding Node_def cont_def
1.13 -by (metis cont_def finite_cont fset_cong fset_to_fset o_def)
1.14 + "Node (root tr) (cont tr) = tr"
1.15 + unfolding Node_def cont_def o_apply
1.16 + apply (rule trans[OF _ dtree.collapse])
1.17 + apply (rule arg_cong2[OF refl the_inv_into_f_f[unfolded inj_on_def]])
1.18 + apply transfer apply simp_all
1.19 + done
1.20
1.21 lemma dtree_simps[simp]:
1.22 assumes "finite as" and "finite as'"
1.23 @@ -77,7 +80,7 @@
1.24 using dtree.sel_unfold[of rt "the_inv fset \<circ> ct" b] unfolding unfold_def
1.25 apply - apply metis
1.26 unfolding cont_def comp_def
1.27 -by (metis (no_types) fset_to_fset map_fset_image)
1.28 +by simp
1.29
1.30 lemma corec:
1.31 "root (corec rt qt ct dt b) = rt b"
1.32 @@ -89,6 +92,6 @@
1.33 apply -
1.34 apply simp
1.35 unfolding cont_def comp_def id_def
1.36 -by (metis (no_types) fset_to_fset map_fset_image)
1.37 +by simp
1.38
1.39 end
2.1 --- a/src/HOL/BNF/Examples/Lambda_Term.thy Wed Mar 13 10:47:00 2013 +0100
2.2 +++ b/src/HOL/BNF/Examples/Lambda_Term.thy Wed Mar 13 13:23:16 2013 +0100
2.3 @@ -34,17 +34,9 @@
2.4 apply (rule Var)
2.5 apply (erule App, assumption)
2.6 apply (erule Lam)
2.7 -using Lt unfolding fset_fset_member mem_Collect_eq
2.8 -apply (rule meta_mp)
2.9 -defer
2.10 -apply assumption
2.11 -apply (erule thin_rl)
2.12 -apply assumption
2.13 -apply (drule meta_spec)
2.14 -apply (drule meta_spec)
2.15 -apply (drule meta_mp)
2.16 -apply assumption
2.17 -apply (auto simp: snds_def)
2.18 +apply (rule Lt)
2.19 +apply transfer
2.20 +apply (auto simp: snds_def)+
2.21 done
2.22
2.23
2.24 @@ -62,7 +54,7 @@
2.25 "varsOf (App t1 t2) = varsOf t1 \<union> varsOf t2"
2.26 "varsOf (Lam x t) = varsOf t \<union> {x}"
2.27 "varsOf (Lt xts t) =
2.28 - varsOf t \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| map_fset (\<lambda> (x,t1). (x,varsOf t1)) xts})"
2.29 + varsOf t \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| fmap (\<lambda> (x,t1). (x,varsOf t1)) xts})"
2.30 unfolding varsOf_def by (simp add: map_pair_def)+
2.31
2.32 definition "fvarsOf = trm_fold
2.33 @@ -77,16 +69,15 @@
2.34 "fvarsOf (Lam x t) = fvarsOf t - {x}"
2.35 "fvarsOf (Lt xts t) =
2.36 fvarsOf t
2.37 - - {x | x X. (x,X) |\<in>| map_fset (\<lambda> (x,t1). (x,fvarsOf t1)) xts}
2.38 - \<union> (\<Union> {X | x X. (x,X) |\<in>| map_fset (\<lambda> (x,t1). (x,fvarsOf t1)) xts})"
2.39 + - {x | x X. (x,X) |\<in>| fmap (\<lambda> (x,t1). (x,fvarsOf t1)) xts}
2.40 + \<union> (\<Union> {X | x X. (x,X) |\<in>| fmap (\<lambda> (x,t1). (x,fvarsOf t1)) xts})"
2.41 unfolding fvarsOf_def by (simp add: map_pair_def)+
2.42
2.43 lemma diff_Un_incl_triv: "\<lbrakk>A \<subseteq> D; C \<subseteq> E\<rbrakk> \<Longrightarrow> A - B \<union> C \<subseteq> D \<union> E" by blast
2.44
2.45 lemma in_map_fset_iff:
2.46 -"(x, X) |\<in>| map_fset (\<lambda>(x, t1). (x, f t1)) xts \<longleftrightarrow>
2.47 - (\<exists> t1. (x,t1) |\<in>| xts \<and> X = f t1)"
2.48 -unfolding map_fset_def2_raw in_fset fset_afset unfolding fset_def2_raw by auto
2.49 + "(x, X) |\<in>| fmap (\<lambda>(x, t1). (x, f t1)) xts \<longleftrightarrow> (\<exists> t1. (x,t1) |\<in>| xts \<and> X = f t1)"
2.50 + by transfer auto
2.51
2.52 lemma fvarsOf_varsOf: "fvarsOf t \<subseteq> varsOf t"
2.53 proof induct
2.54 @@ -94,16 +85,16 @@
2.55 thus ?case unfolding fvarsOf_simps varsOf_simps
2.56 proof (elim diff_Un_incl_triv)
2.57 show
2.58 - "\<Union>{X | x X. (x, X) |\<in>| map_fset (\<lambda>(x, t1). (x, fvarsOf t1)) xts}
2.59 - \<subseteq> \<Union>{{x} \<union> X |x X. (x, X) |\<in>| map_fset (\<lambda>(x, t1). (x, varsOf t1)) xts}"
2.60 + "\<Union>{X | x X. (x, X) |\<in>| fmap (\<lambda>(x, t1). (x, fvarsOf t1)) xts}
2.61 + \<subseteq> \<Union>{{x} \<union> X |x X. (x, X) |\<in>| fmap (\<lambda>(x, t1). (x, varsOf t1)) xts}"
2.62 (is "_ \<subseteq> \<Union> ?L")
2.63 proof(rule Sup_mono, safe)
2.64 fix a x X
2.65 - assume "(x, X) |\<in>| map_fset (\<lambda>(x, t1). (x, fvarsOf t1)) xts"
2.66 + assume "(x, X) |\<in>| fmap (\<lambda>(x, t1). (x, fvarsOf t1)) xts"
2.67 then obtain t1 where x_t1: "(x,t1) |\<in>| xts" and X: "X = fvarsOf t1"
2.68 unfolding in_map_fset_iff by auto
2.69 let ?Y = "varsOf t1"
2.70 - have x_Y: "(x,?Y) |\<in>| map_fset (\<lambda>(x, t1). (x, varsOf t1)) xts"
2.71 + have x_Y: "(x,?Y) |\<in>| fmap (\<lambda>(x, t1). (x, varsOf t1)) xts"
2.72 using x_t1 unfolding in_map_fset_iff by auto
2.73 show "\<exists> Y \<in> ?L. X \<subseteq> Y" unfolding X using Lt(1) x_Y x_t1 by auto
2.74 qed
3.1 --- a/src/HOL/BNF/Examples/TreeFsetI.thy Wed Mar 13 10:47:00 2013 +0100
3.2 +++ b/src/HOL/BNF/Examples/TreeFsetI.thy Wed Mar 13 13:23:16 2013 +0100
3.3 @@ -25,7 +25,7 @@
3.4
3.5 lemma tmap_simps[simp]:
3.6 "lab (tmap f t) = f (lab t)"
3.7 -"sub (tmap f t) = map_fset (tmap f) (sub t)"
3.8 +"sub (tmap f t) = fmap (tmap f) (sub t)"
3.9 unfolding tmap_def treeFsetI.sel_unfold by simp+
3.10
3.11 lemma "tmap (f o g) x = tmap f (tmap g x)"
4.1 --- a/src/HOL/BNF/More_BNFs.thy Wed Mar 13 10:47:00 2013 +0100
4.2 +++ b/src/HOL/BNF/More_BNFs.thy Wed Mar 13 13:23:16 2013 +0100
4.3 @@ -14,7 +14,7 @@
4.4 imports
4.5 BNF_LFP
4.6 BNF_GFP
4.7 - "~~/src/HOL/Quotient_Examples/FSet"
4.8 + "~~/src/HOL/Quotient_Examples/Lift_FSet"
4.9 "~~/src/HOL/Library/Multiset"
4.10 Countable_Type
4.11 begin
4.12 @@ -195,6 +195,28 @@
4.13 qed
4.14 qed
4.15
4.16 +lemma wpull_map:
4.17 + assumes "wpull A B1 B2 f1 f2 p1 p2"
4.18 + 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)"
4.19 + (is "wpull ?A ?B1 ?B2 _ _ _ _")
4.20 +proof (unfold wpull_def)
4.21 + { fix as bs assume *: "as \<in> ?B1" "bs \<in> ?B2" "map f1 as = map f2 bs"
4.22 + hence "length as = length bs" by (metis length_map)
4.23 + hence "\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs" using *
4.24 + proof (induct as bs rule: list_induct2)
4.25 + case (Cons a as b bs)
4.26 + hence "a \<in> B1" "b \<in> B2" "f1 a = f2 b" by auto
4.27 + with assms obtain z where "z \<in> A" "p1 z = a" "p2 z = b" unfolding wpull_def by blast
4.28 + moreover
4.29 + from Cons obtain zs where "zs \<in> ?A" "map p1 zs = as" "map p2 zs = bs" by auto
4.30 + ultimately have "z # zs \<in> ?A" "map p1 (z # zs) = a # as \<and> map p2 (z # zs) = b # bs" by auto
4.31 + thus ?case by (rule_tac x = "z # zs" in bexI)
4.32 + qed simp
4.33 + }
4.34 + thus "\<forall>as bs. as \<in> ?B1 \<and> bs \<in> ?B2 \<and> map f1 as = map f2 bs \<longrightarrow>
4.35 + (\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs)" by blast
4.36 +qed
4.37 +
4.38 bnf_def map [set] "\<lambda>_::'a list. natLeq" ["[]"]
4.39 proof -
4.40 show "map id = id" by (rule List.map.id)
4.41 @@ -221,112 +243,55 @@
4.42 next
4.43 fix A :: "'a set"
4.44 show "|{x. set x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" by (rule list_in_bd)
4.45 -next
4.46 - fix A B1 B2 f1 f2 p1 p2
4.47 - assume "wpull A B1 B2 f1 f2 p1 p2"
4.48 - 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"
4.49 - unfolding wpull_def by auto
4.50 - 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)"
4.51 - (is "wpull ?A ?B1 ?B2 _ _ _ _")
4.52 - proof (unfold wpull_def)
4.53 - { fix as bs assume *: "as \<in> ?B1" "bs \<in> ?B2" "map f1 as = map f2 bs"
4.54 - hence "length as = length bs" by (metis length_map)
4.55 - hence "\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs" using *
4.56 - proof (induct as bs rule: list_induct2)
4.57 - case (Cons a as b bs)
4.58 - hence "a \<in> B1" "b \<in> B2" "f1 a = f2 b" by auto
4.59 - with pull obtain z where "z \<in> A" "p1 z = a" "p2 z = b" by blast
4.60 - moreover
4.61 - from Cons obtain zs where "zs \<in> ?A" "map p1 zs = as" "map p2 zs = bs" by auto
4.62 - ultimately have "z # zs \<in> ?A" "map p1 (z # zs) = a # as \<and> map p2 (z # zs) = b # bs" by auto
4.63 - thus ?case by (rule_tac x = "z # zs" in bexI)
4.64 - qed simp
4.65 - }
4.66 - thus "\<forall>as bs. as \<in> ?B1 \<and> bs \<in> ?B2 \<and> map f1 as = map f2 bs \<longrightarrow>
4.67 - (\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs)" by blast
4.68 - qed
4.69 -qed simp+
4.70 +qed (simp add: wpull_map)+
4.71
4.72 (* Finite sets *)
4.73 -abbreviation afset where "afset \<equiv> abs_fset"
4.74 -abbreviation rfset where "rfset \<equiv> rep_fset"
4.75
4.76 -lemma fset_fset_member:
4.77 -"fset A = {a. a |\<in>| A}"
4.78 -unfolding fset_def fset_member_def by auto
4.79 +definition fset_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" where
4.80 +"fset_rel R a b \<longleftrightarrow>
4.81 + (\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and>
4.82 + (\<forall>t \<in> fset b. \<exists>u \<in> fset a. R u t)"
4.83
4.84 -lemma afset_rfset:
4.85 -"afset (rfset x) = x"
4.86 -by (rule Quotient_fset[unfolded Quotient_def, THEN conjunct1, rule_format])
4.87
4.88 -lemma afset_rfset_id:
4.89 -"afset o rfset = id"
4.90 -unfolding comp_def afset_rfset id_def ..
4.91 +lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
4.92 + by (rule f_the_inv_into_f[unfolded inj_on_def])
4.93 + (transfer, simp,
4.94 + transfer, metis Collect_finite_eq_lists lists_UNIV mem_Collect_eq)
4.95
4.96 -lemma rfset:
4.97 -"rfset A = rfset B \<longleftrightarrow> A = B"
4.98 -by (metis afset_rfset)
4.99
4.100 -lemma afset_set:
4.101 -"afset as = afset bs \<longleftrightarrow> set as = set bs"
4.102 -using Quotient_fset unfolding Quotient_def list_eq_def by auto
4.103 +lemma fset_rel_aux:
4.104 +"(\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>u \<in> fset b. \<exists>t \<in> fset a. R t u) \<longleftrightarrow>
4.105 + (a, b) \<in> (Gr {a. fset a \<subseteq> {(a, b). R a b}} (fmap fst))\<inverse> O
4.106 + Gr {a. fset a \<subseteq> {(a, b). R a b}} (fmap snd)" (is "?L = ?R")
4.107 +proof
4.108 + assume ?L
4.109 + def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?L'")
4.110 + have "finite ?L'" by (intro finite_Int[OF disjI2] finite_cartesian_product) (transfer, simp)+
4.111 + hence *: "fset R' = ?L'" unfolding R'_def by (intro fset_to_fset)
4.112 + show ?R unfolding Gr_def relcomp_unfold converse_unfold
4.113 + proof (intro CollectI prod_caseI exI conjI)
4.114 + from * show "(R', a) = (R', fmap fst R')" using conjunct1[OF `?L`]
4.115 + by (clarify, transfer, auto simp add: image_def Int_def split: prod.splits)
4.116 + from * show "(R', b) = (R', fmap snd R')" using conjunct2[OF `?L`]
4.117 + by (clarify, transfer, auto simp add: image_def Int_def split: prod.splits)
4.118 + qed (auto simp add: *)
4.119 +next
4.120 + assume ?R thus ?L unfolding Gr_def relcomp_unfold converse_unfold
4.121 + apply (simp add: subset_eq Ball_def)
4.122 + apply (rule conjI)
4.123 + apply (transfer, clarsimp, metis snd_conv)
4.124 + by (transfer, clarsimp, metis fst_conv)
4.125 +qed
4.126
4.127 -lemma surj_afset:
4.128 -"\<exists> as. A = afset as"
4.129 -by (metis afset_rfset)
4.130 +lemma abs_fset_rep_fset[simp]: "abs_fset (rep_fset x) = x"
4.131 + by (rule Quotient_fset[unfolded Quotient_def, THEN conjunct1, rule_format])
4.132
4.133 -lemma fset_def2:
4.134 -"fset = set o rfset"
4.135 -unfolding fset_def map_fun_def[abs_def] by simp
4.136 -
4.137 -lemma fset_def2_raw:
4.138 -"fset A = set (rfset A)"
4.139 -unfolding fset_def2 by simp
4.140 -
4.141 -lemma fset_comp_afset:
4.142 -"fset o afset = set"
4.143 -unfolding fset_def2 comp_def apply(rule ext)
4.144 -unfolding afset_set[symmetric] afset_rfset ..
4.145 -
4.146 -lemma fset_afset:
4.147 -"fset (afset as) = set as"
4.148 -unfolding fset_comp_afset[symmetric] by simp
4.149 -
4.150 -lemma set_rfset_afset:
4.151 -"set (rfset (afset as)) = set as"
4.152 -unfolding afset_set[symmetric] afset_rfset ..
4.153 -
4.154 -lemma map_fset_comp_afset:
4.155 -"(map_fset f) o afset = afset o (map f)"
4.156 -unfolding map_fset_def map_fun_def[abs_def] comp_def apply(rule ext)
4.157 -unfolding afset_set set_map set_rfset_afset id_apply ..
4.158 -
4.159 -lemma map_fset_afset:
4.160 -"(map_fset f) (afset as) = afset (map f as)"
4.161 -using map_fset_comp_afset unfolding comp_def fun_eq_iff by auto
4.162 -
4.163 -lemma fset_map_fset:
4.164 -"fset (map_fset f A) = (image f) (fset A)"
4.165 -apply(subst afset_rfset[symmetric, of A])
4.166 -unfolding map_fset_afset fset_afset set_map
4.167 -unfolding fset_def2_raw ..
4.168 -
4.169 -lemma map_fset_def2:
4.170 -"map_fset f = afset o (map f) o rfset"
4.171 -unfolding map_fset_def map_fun_def[abs_def] by simp
4.172 -
4.173 -lemma map_fset_def2_raw:
4.174 -"map_fset f A = afset (map f (rfset A))"
4.175 -unfolding map_fset_def2 by simp
4.176 -
4.177 -lemma finite_ex_fset:
4.178 -assumes "finite A"
4.179 -shows "\<exists> B. fset B = A"
4.180 -by (metis assms finite_list fset_afset)
4.181 +lemma wpull_Gr_def: "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> Gr B1 f1 O (Gr B2 f2)\<inverse> \<subseteq> (Gr A p1)\<inverse> O Gr A p2"
4.182 + unfolding wpull_def Gr_def relcomp_unfold converse_unfold by auto
4.183
4.184 lemma wpull_image:
4.185 -assumes "wpull A B1 B2 f1 f2 p1 p2"
4.186 -shows "wpull (Pow A) (Pow B1) (Pow B2) (image f1) (image f2) (image p1) (image p2)"
4.187 + assumes "wpull A B1 B2 f1 f2 p1 p2"
4.188 + shows "wpull (Pow A) (Pow B1) (Pow B2) (image f1) (image f2) (image p1) (image p2)"
4.189 unfolding wpull_def Pow_def Bex_def mem_Collect_eq proof clarify
4.190 fix Y1 Y2 assume Y1: "Y1 \<subseteq> B1" and Y2: "Y2 \<subseteq> B2" and EQ: "f1 ` Y1 = f2 ` Y2"
4.191 def X \<equiv> "{a \<in> A. p1 a \<in> Y1 \<and> p2 a \<in> Y2}"
4.192 @@ -357,123 +322,51 @@
4.193 qed(unfold X_def, auto)
4.194 qed
4.195
4.196 -lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
4.197 -by (rule f_the_inv_into_f) (auto simp: inj_on_def fset_cong dest!: finite_ex_fset)
4.198 -
4.199 -definition fset_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" where
4.200 -"fset_rel R a b \<longleftrightarrow>
4.201 - (\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and>
4.202 - (\<forall>t \<in> fset b. \<exists>u \<in> fset a. R u t)"
4.203 -
4.204 -lemma fset_rel_aux:
4.205 -"(\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and> (\<forall>u \<in> fset b. \<exists>t \<in> fset a. R t u) \<longleftrightarrow>
4.206 - (a, b) \<in> (Gr {a. fset a \<subseteq> {(a, b). R a b}} (map_fset fst))\<inverse> O
4.207 - Gr {a. fset a \<subseteq> {(a, b). R a b}} (map_fset snd)" (is "?L = ?R")
4.208 -proof
4.209 - assume ?L
4.210 - def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?L'")
4.211 - have "finite ?L'" by (intro finite_Int[OF disjI2] finite_cartesian_product) auto
4.212 - hence *: "fset R' = ?L'" unfolding R'_def by (intro fset_to_fset)
4.213 - show ?R unfolding Gr_def relcomp_unfold converse_unfold
4.214 - proof (intro CollectI prod_caseI exI conjI)
4.215 - from * show "(R', a) = (R', map_fset fst R')" using conjunct1[OF `?L`]
4.216 - by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits)
4.217 - from * show "(R', b) = (R', map_fset snd R')" using conjunct2[OF `?L`]
4.218 - by (auto simp add: fset_cong[symmetric] image_def Int_def split: prod.splits)
4.219 - qed (auto simp add: *)
4.220 -next
4.221 - assume ?R thus ?L unfolding Gr_def relcomp_unfold converse_unfold
4.222 - apply (simp add: subset_eq Ball_def)
4.223 - apply (rule conjI)
4.224 - apply (clarsimp, metis snd_conv)
4.225 - by (clarsimp, metis fst_conv)
4.226 +lemma wpull_fmap:
4.227 + assumes "wpull A B1 B2 f1 f2 p1 p2"
4.228 + shows "wpull {x. fset x \<subseteq> A} {x. fset x \<subseteq> B1} {x. fset x \<subseteq> B2}
4.229 + (fmap f1) (fmap f2) (fmap p1) (fmap p2)"
4.230 +unfolding wpull_def Pow_def Bex_def mem_Collect_eq proof clarify
4.231 + fix y1 y2
4.232 + assume Y1: "fset y1 \<subseteq> B1" and Y2: "fset y2 \<subseteq> B2"
4.233 + assume "fmap f1 y1 = fmap f2 y2"
4.234 + hence EQ: "f1 ` (fset y1) = f2 ` (fset y2)" by transfer simp
4.235 + with Y1 Y2 obtain X where X: "X \<subseteq> A" and Y1: "p1 ` X = fset y1" and Y2: "p2 ` X = fset y2"
4.236 + using wpull_image[OF assms] unfolding wpull_def Pow_def
4.237 + by (auto elim!: allE[of _ "fset y1"] allE[of _ "fset y2"])
4.238 + have "\<forall> y1' \<in> fset y1. \<exists> x. x \<in> X \<and> y1' = p1 x" using Y1 by auto
4.239 + then obtain q1 where q1: "\<forall> y1' \<in> fset y1. q1 y1' \<in> X \<and> y1' = p1 (q1 y1')" by metis
4.240 + have "\<forall> y2' \<in> fset y2. \<exists> x. x \<in> X \<and> y2' = p2 x" using Y2 by auto
4.241 + then obtain q2 where q2: "\<forall> y2' \<in> fset y2. q2 y2' \<in> X \<and> y2' = p2 (q2 y2')" by metis
4.242 + def X' \<equiv> "q1 ` (fset y1) \<union> q2 ` (fset y2)"
4.243 + have X': "X' \<subseteq> A" and Y1: "p1 ` X' = fset y1" and Y2: "p2 ` X' = fset y2"
4.244 + using X Y1 Y2 q1 q2 unfolding X'_def by auto
4.245 + have fX': "finite X'" unfolding X'_def by transfer simp
4.246 + then obtain x where X'eq: "X' = fset x" by transfer (metis finite_list)
4.247 + show "\<exists>x. fset x \<subseteq> A \<and> fmap p1 x = y1 \<and> fmap p2 x = y2"
4.248 + using X' Y1 Y2 by (auto simp: X'eq intro!: exI[of _ "x"]) (transfer, simp)+
4.249 qed
4.250
4.251 -bnf_def map_fset [fset] "\<lambda>_::'a fset. natLeq" ["{||}"] fset_rel
4.252 -proof -
4.253 - show "map_fset id = id"
4.254 - unfolding map_fset_def2 map_id o_id afset_rfset_id ..
4.255 -next
4.256 - fix f g
4.257 - show "map_fset (g o f) = map_fset g o map_fset f"
4.258 - unfolding map_fset_def2 map.comp[symmetric] comp_def apply(rule ext)
4.259 - unfolding afset_set set_map fset_def2_raw[symmetric] image_image[symmetric]
4.260 - unfolding map_fset_afset[symmetric] map_fset_image afset_rfset
4.261 - by (rule refl)
4.262 -next
4.263 - fix x f g
4.264 - assume "\<And>z. z \<in> fset x \<Longrightarrow> f z = g z"
4.265 - hence "map f (rfset x) = map g (rfset x)"
4.266 - apply(intro map_cong) unfolding fset_def2_raw by auto
4.267 - thus "map_fset f x = map_fset g x" unfolding map_fset_def2_raw
4.268 - by (rule arg_cong)
4.269 -next
4.270 - fix f
4.271 - show "fset o map_fset f = image f o fset"
4.272 - unfolding comp_def fset_map_fset ..
4.273 -next
4.274 - show "card_order natLeq" by (rule natLeq_card_order)
4.275 -next
4.276 - show "cinfinite natLeq" by (rule natLeq_cinfinite)
4.277 -next
4.278 - fix x
4.279 - show "|fset x| \<le>o natLeq"
4.280 - unfolding fset_def2_raw
4.281 - apply (rule ordLess_imp_ordLeq)
4.282 - apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
4.283 - by (rule finite_set)
4.284 -next
4.285 - fix A :: "'a set"
4.286 - have "|{x. fset x \<subseteq> A}| \<le>o |afset ` {as. set as \<subseteq> A}|"
4.287 - apply(rule card_of_mono1) unfolding fset_def2_raw apply auto
4.288 - apply (rule image_eqI)
4.289 - by (auto simp: afset_rfset)
4.290 - also have "|afset ` {as. set as \<subseteq> A}| \<le>o |{as. set as \<subseteq> A}|" using card_of_image .
4.291 - also have "|{as. set as \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" by (rule list_in_bd)
4.292 - finally show "|{x. fset x \<subseteq> A}| \<le>o ( |A| +c ctwo) ^c natLeq" .
4.293 -next
4.294 - fix A B1 B2 f1 f2 p1 p2
4.295 - assume wp: "wpull A B1 B2 f1 f2 p1 p2"
4.296 - hence "wpull (Pow A) (Pow B1) (Pow B2) (image f1) (image f2) (image p1) (image p2)"
4.297 - by (rule wpull_image)
4.298 - show "wpull {x. fset x \<subseteq> A} {x. fset x \<subseteq> B1} {x. fset x \<subseteq> B2}
4.299 - (map_fset f1) (map_fset f2) (map_fset p1) (map_fset p2)"
4.300 - unfolding wpull_def Pow_def Bex_def mem_Collect_eq proof clarify
4.301 - fix y1 y2
4.302 - assume Y1: "fset y1 \<subseteq> B1" and Y2: "fset y2 \<subseteq> B2"
4.303 - assume "map_fset f1 y1 = map_fset f2 y2"
4.304 - hence EQ: "f1 ` (fset y1) = f2 ` (fset y2)" unfolding map_fset_def2_raw
4.305 - unfolding afset_set set_map fset_def2_raw .
4.306 - with Y1 Y2 obtain X where X: "X \<subseteq> A"
4.307 - and Y1: "p1 ` X = fset y1" and Y2: "p2 ` X = fset y2"
4.308 - using wpull_image[OF wp] unfolding wpull_def Pow_def
4.309 - unfolding Bex_def mem_Collect_eq apply -
4.310 - apply(erule allE[of _ "fset y1"], erule allE[of _ "fset y2"]) by auto
4.311 - have "\<forall> y1' \<in> fset y1. \<exists> x. x \<in> X \<and> y1' = p1 x" using Y1 by auto
4.312 - then obtain q1 where q1: "\<forall> y1' \<in> fset y1. q1 y1' \<in> X \<and> y1' = p1 (q1 y1')" by metis
4.313 - have "\<forall> y2' \<in> fset y2. \<exists> x. x \<in> X \<and> y2' = p2 x" using Y2 by auto
4.314 - then obtain q2 where q2: "\<forall> y2' \<in> fset y2. q2 y2' \<in> X \<and> y2' = p2 (q2 y2')" by metis
4.315 - def X' \<equiv> "q1 ` (fset y1) \<union> q2 ` (fset y2)"
4.316 - have X': "X' \<subseteq> A" and Y1: "p1 ` X' = fset y1" and Y2: "p2 ` X' = fset y2"
4.317 - using X Y1 Y2 q1 q2 unfolding X'_def by auto
4.318 - have fX': "finite X'" unfolding X'_def by simp
4.319 - then obtain x where X'eq: "X' = fset x" by (auto dest: finite_ex_fset)
4.320 - show "\<exists>x. fset x \<subseteq> A \<and> map_fset p1 x = y1 \<and> map_fset p2 x = y2"
4.321 - apply(intro exI[of _ "x"]) using X' Y1 Y2
4.322 - unfolding X'eq map_fset_def2_raw fset_def2_raw set_map[symmetric]
4.323 - afset_set[symmetric] afset_rfset by simp
4.324 - qed
4.325 -next
4.326 - fix R
4.327 - show "{p. fset_rel (\<lambda>x y. (x, y) \<in> R) (fst p) (snd p)} =
4.328 - (Gr {x. fset x \<subseteq> R} (map_fset fst))\<inverse> O Gr {x. fset x \<subseteq> R} (map_fset snd)"
4.329 - unfolding fset_rel_def fset_rel_aux by simp
4.330 -qed auto
4.331 +bnf_def fmap [fset] "\<lambda>_::'a fset. natLeq" ["{||}"] fset_rel
4.332 +apply -
4.333 + apply transfer' apply simp
4.334 + apply transfer' apply simp
4.335 + apply transfer apply force
4.336 + apply transfer apply force
4.337 + apply (rule natLeq_card_order)
4.338 + apply (rule natLeq_cinfinite)
4.339 + apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite_set)
4.340 + apply (rule ordLeq_transitive[OF surj_imp_ordLeq[of _ abs_fset] list_in_bd])
4.341 + apply (auto simp: fset_def intro!: image_eqI[of _ abs_fset]) []
4.342 + apply (erule wpull_fmap)
4.343 + apply (simp add: Gr_def relcomp_unfold converse_unfold fset_rel_def fset_rel_aux)
4.344 +apply transfer apply simp
4.345 +done
4.346
4.347 lemmas [simp] = fset.map_comp' fset.map_id' fset.set_natural'
4.348
4.349 lemma fset_rel_fset: "set_rel \<chi> (fset A1) (fset A2) = fset_rel \<chi> A1 A2"
4.350 -unfolding fset_rel_def set_rel_def by auto
4.351 + unfolding fset_rel_def set_rel_def by auto
4.352
4.353 (* Countable sets *)
4.354
5.1 --- a/src/HOL/Quotient_Examples/Lift_FSet.thy Wed Mar 13 10:47:00 2013 +0100
5.2 +++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Wed Mar 13 13:23:16 2013 +0100
5.3 @@ -35,7 +35,7 @@
5.4
5.5 subsection {* Lifted constant definitions *}
5.6
5.7 -lift_definition fnil :: "'a fset" is "[]" parametric Nil_transfer
5.8 +lift_definition fnil :: "'a fset" ("{||}") is "[]" parametric Nil_transfer
5.9 by simp
5.10
5.11 lift_definition fcons :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Cons parametric Cons_transfer
5.12 @@ -86,6 +86,22 @@
5.13 done
5.14 qed
5.15
5.16 +syntax
5.17 + "_insert_fset" :: "args => 'a fset" ("{|(_)|}")
5.18 +
5.19 +translations
5.20 + "{|x, xs|}" == "CONST fcons x {|xs|}"
5.21 + "{|x|}" == "CONST fcons x {||}"
5.22 +
5.23 +lift_definition fset_member :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<in>|" 50) is "\<lambda>x xs. x \<in> set xs"
5.24 + by simp
5.25 +
5.26 +abbreviation notin_fset :: "'a \<Rightarrow> 'a fset \<Rightarrow> bool" (infix "|\<notin>|" 50) where
5.27 + "x |\<notin>| S \<equiv> \<not> (x |\<in>| S)"
5.28 +
5.29 +lemma fset_member_fmap[simp]: "a |\<in>| fmap f X = (\<exists>b. b |\<in>| X \<and> a = f b)"
5.30 + by transfer auto
5.31 +
5.32 text {* We can export code: *}
5.33
5.34 export_code fnil fcons fappend fmap ffilter fset in SML