--- a/src/Doc/Datatypes/Datatypes.thy Tue Oct 01 17:04:27 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Tue Oct 01 17:06:35 2013 +0200
@@ -1776,7 +1776,7 @@
text {* \blankline *}
primcorec iterate\<^sub>i\<^sub>s :: "('a \<Rightarrow> 'a fset) \<Rightarrow> 'a \<Rightarrow> 'a tree\<^sub>i\<^sub>s" where
- "iterate\<^sub>i\<^sub>s f x = Node\<^sub>i\<^sub>s x (fmap (iterate\<^sub>i\<^sub>s f) (f x))"
+ "iterate\<^sub>i\<^sub>s f x = Node\<^sub>i\<^sub>s x (fimage (iterate\<^sub>i\<^sub>s f) (f x))"
text {*
\noindent
--- a/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy Tue Oct 01 17:04:27 2013 +0200
+++ b/src/HOL/BNF/Examples/Derivation_Trees/DTree.thy Tue Oct 01 17:06:35 2013 +0200
@@ -26,14 +26,14 @@
definition "corec rt ct \<equiv> dtree_corec rt (the_inv fset o ct)"
lemma finite_cont[simp]: "finite (cont tr)"
- unfolding cont_def o_apply by (cases tr, clarsimp) (transfer, simp)
+ unfolding cont_def o_apply by (cases tr, clarsimp)
lemma Node_root_cont[simp]:
"Node (root tr) (cont tr) = tr"
unfolding Node_def cont_def o_apply
apply (rule trans[OF _ dtree.collapse])
apply (rule arg_cong2[OF refl the_inv_into_f_f[unfolded inj_on_def]])
- apply transfer apply simp_all
+ apply (simp_all add: fset_inject)
done
lemma dtree_simps[simp]:
--- a/src/HOL/BNF/Examples/Lambda_Term.thy Tue Oct 01 17:04:27 2013 +0200
+++ b/src/HOL/BNF/Examples/Lambda_Term.thy Tue Oct 01 17:06:35 2013 +0200
@@ -28,20 +28,20 @@
"varsOf (Var a) = {a}"
| "varsOf (App f x) = varsOf f \<union> varsOf x"
| "varsOf (Lam x b) = {x} \<union> varsOf b"
-| "varsOf (Lt F t) = varsOf t \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| fmap (map_pair id varsOf) F})"
+| "varsOf (Lt F t) = varsOf t \<union> (\<Union> { {x} \<union> X | x X. (x,X) |\<in>| fimage (map_pair id varsOf) F})"
primrec_new fvarsOf :: "'a trm \<Rightarrow> 'a set" where
"fvarsOf (Var x) = {x}"
| "fvarsOf (App t1 t2) = fvarsOf t1 \<union> fvarsOf t2"
| "fvarsOf (Lam x t) = fvarsOf t - {x}"
-| "fvarsOf (Lt xts t) = fvarsOf t - {x | x X. (x,X) |\<in>| fmap (map_pair id varsOf) xts} \<union>
- (\<Union> {X | x X. (x,X) |\<in>| fmap (map_pair id varsOf) xts})"
+| "fvarsOf (Lt xts t) = fvarsOf t - {x | x X. (x,X) |\<in>| fimage (map_pair id varsOf) xts} \<union>
+ (\<Union> {X | x X. (x,X) |\<in>| fimage (map_pair id varsOf) xts})"
lemma diff_Un_incl_triv: "\<lbrakk>A \<subseteq> D; C \<subseteq> E\<rbrakk> \<Longrightarrow> A - B \<union> C \<subseteq> D \<union> E" by blast
lemma in_fmap_map_pair_fset_iff[simp]:
- "(x, y) |\<in>| fmap (map_pair f g) xts \<longleftrightarrow> (\<exists> t1 t2. (t1, t2) |\<in>| xts \<and> x = f t1 \<and> y = g t2)"
- by transfer auto
+ "(x, y) |\<in>| fimage (map_pair f g) xts \<longleftrightarrow> (\<exists> t1 t2. (t1, t2) |\<in>| xts \<and> x = f t1 \<and> y = g t2)"
+ by force
lemma fvarsOf_varsOf: "fvarsOf t \<subseteq> varsOf t"
proof induct
--- a/src/HOL/BNF/Examples/TreeFsetI.thy Tue Oct 01 17:04:27 2013 +0200
+++ b/src/HOL/BNF/Examples/TreeFsetI.thy Tue Oct 01 17:06:35 2013 +0200
@@ -25,13 +25,13 @@
lemma tmap_simps[simp]:
"lab (tmap f t) = f (lab t)"
-"sub (tmap f t) = fmap (tmap f) (sub t)"
+"sub (tmap f t) = fimage (tmap f) (sub t)"
unfolding tmap_def treeFsetI.sel_unfold by simp+
lemma "tmap (f o g) x = tmap f (tmap g x)"
apply (rule treeFsetI.coinduct[of "%x1 x2. \<exists>x. x1 = tmap (f o g) x \<and> x2 = tmap f (tmap g x)"])
apply auto
-apply (unfold fset_rel_def)
+apply (unfold fset_rel_alt)
by auto
end
--- a/src/HOL/BNF/More_BNFs.thy Tue Oct 01 17:04:27 2013 +0200
+++ b/src/HOL/BNF/More_BNFs.thy Tue Oct 01 17:06:35 2013 +0200
@@ -13,7 +13,7 @@
theory More_BNFs
imports
Basic_BNFs
- "~~/src/HOL/Quotient_Examples/Lift_FSet"
+ "~~/src/HOL/Library/FSet"
"~~/src/HOL/Library/Multiset"
Countable_Type
begin
@@ -119,42 +119,6 @@
(* Finite sets *)
-definition fset_rel :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a fset \<Rightarrow> 'b fset \<Rightarrow> bool" where
-"fset_rel R a b \<longleftrightarrow>
- (\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and>
- (\<forall>t \<in> fset b. \<exists>u \<in> fset a. R u t)"
-
-
-lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
- by (rule f_the_inv_into_f[unfolded inj_on_def])
- (transfer, simp,
- transfer, metis Collect_finite_eq_lists lists_UNIV mem_Collect_eq)
-
-
-lemma fset_rel_aux:
-"(\<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>
- ((Grp {a. fset a \<subseteq> {(a, b). R a b}} (fmap fst))\<inverse>\<inverse> OO
- Grp {a. fset a \<subseteq> {(a, b). R a b}} (fmap snd)) a b" (is "?L = ?R")
-proof
- assume ?L
- def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?L'")
- have "finite ?L'" by (intro finite_Int[OF disjI2] finite_cartesian_product) (transfer, simp)+
- hence *: "fset R' = ?L'" unfolding R'_def by (intro fset_to_fset)
- show ?R unfolding Grp_def relcompp.simps conversep.simps
- proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
- from * show "a = fmap fst R'" using conjunct1[OF `?L`]
- by (transfer, auto simp add: image_def Int_def split: prod.splits)
- from * show "b = fmap snd R'" using conjunct2[OF `?L`]
- by (transfer, auto simp add: image_def Int_def split: prod.splits)
- qed (auto simp add: *)
-next
- assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
- apply (simp add: subset_eq Ball_def)
- apply (rule conjI)
- apply (transfer, clarsimp, metis snd_conv)
- by (transfer, clarsimp, metis fst_conv)
-qed
-
lemma wpull_image:
assumes "wpull A B1 B2 f1 f2 p1 p2"
shows "wpull (Pow A) (Pow B1) (Pow B2) (image f1) (image f2) (image p1) (image p2)"
@@ -188,14 +152,51 @@
qed(unfold X_def, auto)
qed
+context
+includes fset.lifting
+begin
+
+lemma fset_rel_alt: "fset_rel R a b \<longleftrightarrow> (\<forall>t \<in> fset a. \<exists>u \<in> fset b. R t u) \<and>
+ (\<forall>t \<in> fset b. \<exists>u \<in> fset a. R u t)"
+ by transfer (simp add: set_rel_def)
+
+lemma fset_to_fset: "finite A \<Longrightarrow> fset (the_inv fset A) = A"
+ apply (rule f_the_inv_into_f[unfolded inj_on_def])
+ apply (simp add: fset_inject) apply (rule range_eqI Abs_fset_inverse[symmetric] CollectI)+
+ .
+
+lemma fset_rel_aux:
+"(\<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>
+ ((Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage fst))\<inverse>\<inverse> OO
+ Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage snd)) a b" (is "?L = ?R")
+proof
+ assume ?L
+ def R' \<equiv> "the_inv fset (Collect (split R) \<inter> (fset a \<times> fset b))" (is "the_inv fset ?L'")
+ have "finite ?L'" by (intro finite_Int[OF disjI2] finite_cartesian_product) (transfer, simp)+
+ hence *: "fset R' = ?L'" unfolding R'_def by (intro fset_to_fset)
+ show ?R unfolding Grp_def relcompp.simps conversep.simps
+ proof (intro CollectI prod_caseI exI[of _ a] exI[of _ b] exI[of _ R'] conjI refl)
+ from * show "a = fimage fst R'" using conjunct1[OF `?L`]
+ by (transfer, auto simp add: image_def Int_def split: prod.splits)
+ from * show "b = fimage snd R'" using conjunct2[OF `?L`]
+ by (transfer, auto simp add: image_def Int_def split: prod.splits)
+ qed (auto simp add: *)
+next
+ assume ?R thus ?L unfolding Grp_def relcompp.simps conversep.simps
+ apply (simp add: subset_eq Ball_def)
+ apply (rule conjI)
+ apply (transfer, clarsimp, metis snd_conv)
+ by (transfer, clarsimp, metis fst_conv)
+qed
+
lemma wpull_fmap:
assumes "wpull A B1 B2 f1 f2 p1 p2"
shows "wpull {x. fset x \<subseteq> A} {x. fset x \<subseteq> B1} {x. fset x \<subseteq> B2}
- (fmap f1) (fmap f2) (fmap p1) (fmap p2)"
+ (fimage f1) (fimage f2) (fimage p1) (fimage p2)"
unfolding wpull_def Pow_def Bex_def mem_Collect_eq proof clarify
fix y1 y2
assume Y1: "fset y1 \<subseteq> B1" and Y2: "fset y2 \<subseteq> B2"
- assume "fmap f1 y1 = fmap f2 y2"
+ assume "fimage f1 y1 = fimage f2 y2"
hence EQ: "f1 ` (fset y1) = f2 ` (fset y2)" by transfer simp
with Y1 Y2 obtain X where X: "X \<subseteq> A" and Y1: "p1 ` X = fset y1" and Y2: "p2 ` X = fset y2"
using wpull_image[OF assms] unfolding wpull_def Pow_def
@@ -208,29 +209,31 @@
have X': "X' \<subseteq> A" and Y1: "p1 ` X' = fset y1" and Y2: "p2 ` X' = fset y2"
using X Y1 Y2 q1 q2 unfolding X'_def by auto
have fX': "finite X'" unfolding X'_def by transfer simp
- then obtain x where X'eq: "X' = fset x" by transfer (metis finite_list)
- show "\<exists>x. fset x \<subseteq> A \<and> fmap p1 x = y1 \<and> fmap p2 x = y2"
- using X' Y1 Y2 by (auto simp: X'eq intro!: exI[of _ "x"]) (transfer, simp)+
+ then obtain x where X'eq: "X' = fset x" by transfer simp
+ show "\<exists>x. fset x \<subseteq> A \<and> fimage p1 x = y1 \<and> fimage p2 x = y2"
+ using X' Y1 Y2 by (auto simp: X'eq intro!: exI[of _ "x"]) (transfer, blast)+
qed
-bnf fmap [fset] "\<lambda>_::'a fset. natLeq" ["{||}"] fset_rel
+bnf fimage [fset] "\<lambda>_::'a fset. natLeq" ["{||}"] fset_rel
apply -
apply transfer' apply simp
- apply transfer' apply simp
+ apply transfer' apply force
apply transfer apply force
- apply transfer apply force
+ apply transfer' apply force
apply (rule natLeq_card_order)
apply (rule natLeq_cinfinite)
- apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite_set)
+ apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq)
apply (erule wpull_fmap)
- apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff fset_rel_def fset_rel_aux)
+ apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff fset_rel_alt fset_rel_aux)
apply transfer apply simp
done
-lemmas [simp] = fset.map_comp fset.map_id fset.set_map
+lemma fset_rel_fset: "set_rel \<chi> (fset A1) (fset A2) = fset_rel \<chi> A1 A2"
+ by transfer (rule refl)
-lemma fset_rel_fset: "set_rel \<chi> (fset A1) (fset A2) = fset_rel \<chi> A1 A2"
- unfolding fset_rel_def set_rel_def by auto
+end
+
+lemmas [simp] = fset.map_comp fset.map_id fset.set_map
(* Countable sets *)
--- a/src/HOL/Library/FSet.thy Tue Oct 01 17:04:27 2013 +0200
+++ b/src/HOL/Library/FSet.thy Tue Oct 01 17:06:35 2013 +0200
@@ -63,6 +63,12 @@
abbreviation finter :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|\<inter>|" 65) where "xs |\<inter>| ys \<equiv> inf xs ys"
abbreviation fminus :: "'a fset \<Rightarrow> 'a fset \<Rightarrow> 'a fset" (infixl "|-|" 65) where "xs |-| ys \<equiv> minus xs ys"
+instantiation fset :: (equal) equal
+begin
+definition "HOL.equal A B \<longleftrightarrow> A |\<subseteq>| B \<and> B |\<subseteq>| A"
+instance by intro_classes (auto simp add: equal_fset_def)
+end
+
instantiation fset :: (type) conditionally_complete_lattice
begin