# HG changeset patch
# User traytel
# Date 1380639995 -7200
# Node ID 21dac9a60f0ccdc2ecda62368b765dcf64a7d805
# Parent  38c0bbb8348b018ed4f7787ab09e4fe885061186
base the fset bnf on the new FSet theory

diff -r 38c0bbb8348b -r 21dac9a60f0c src/Doc/Datatypes/Datatypes.thy
--- 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
diff -r 38c0bbb8348b -r 21dac9a60f0c src/HOL/BNF/Examples/Derivation_Trees/DTree.thy
--- 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]:
diff -r 38c0bbb8348b -r 21dac9a60f0c src/HOL/BNF/Examples/Lambda_Term.thy
--- 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
diff -r 38c0bbb8348b -r 21dac9a60f0c src/HOL/BNF/Examples/TreeFsetI.thy
--- 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
diff -r 38c0bbb8348b -r 21dac9a60f0c src/HOL/BNF/More_BNFs.thy
--- 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 *)
 
diff -r 38c0bbb8348b -r 21dac9a60f0c src/HOL/Library/FSet.thy
--- 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