# HG changeset patch
# User blanchet
# Date 1403856704 -7200
# Node ID 882091eb1e9a8a39a3503fab5b3ee01832e3f1f8
# Parent  5004aca2082165b054c47902033ffa7dfdb73ba0
merged two small theory files

diff -r 5004aca20821 -r 882091eb1e9a src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Fri Jun 27 10:11:44 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Fri Jun 27 10:11:44 2014 +0200
@@ -2495,8 +2495,8 @@
     next
       fix R
       show "rel_fn R =
-            (BNF_Util.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn fst))\<inverse>\<inverse> OO
-             BNF_Util.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn snd)"
+            (BNF_Def.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn fst))\<inverse>\<inverse> OO
+             BNF_Def.Grp {x. set_fn x \<subseteq> Collect (split R)} (map_fn snd)"
         unfolding Grp_def fun_eq_iff relcompp.simps conversep.simps
         apply transfer
         unfolding rel_fun_def subset_iff image_iff
diff -r 5004aca20821 -r 882091eb1e9a src/HOL/BNF_Def.thy
--- a/src/HOL/BNF_Def.thy	Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/BNF_Def.thy	Fri Jun 27 10:11:44 2014 +0200
@@ -1,5 +1,6 @@
 (*  Title:      HOL/BNF_Def.thy
     Author:     Dmitriy Traytel, TU Muenchen
+    Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2012
 
 Definition of bounded natural functors.
@@ -8,12 +9,47 @@
 header {* Definition of Bounded Natural Functors *}
 
 theory BNF_Def
-imports BNF_Util Fun_Def_Base
+imports BNF_Cardinal_Arithmetic Fun_Def_Base
 keywords
   "print_bnfs" :: diag and
   "bnf" :: thy_goal
 begin
 
+definition
+  rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
+where
+  "rel_fun A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
+
+lemma rel_funI [intro]:
+  assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
+  shows "rel_fun A B f g"
+  using assms by (simp add: rel_fun_def)
+
+lemma rel_funD:
+  assumes "rel_fun A B f g" and "A x y"
+  shows "B (f x) (g y)"
+  using assms by (simp add: rel_fun_def)
+
+definition collect where
+"collect F x = (\<Union>f \<in> F. f x)"
+
+lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
+by simp
+
+lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
+by simp
+
+lemma bijI': "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
+unfolding bij_def inj_on_def by auto blast
+
+(* Operator: *)
+definition "Gr A f = {(a, f a) | a. a \<in> A}"
+
+definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)"
+
+definition vimage2p where
+  "vimage2p f g R = (\<lambda>x y. R (f x) (g y))"
+
 lemma collect_comp: "collect F \<circ> g = collect ((\<lambda>f. f \<circ> g) ` F)"
   by (rule ext) (auto simp only: comp_apply collect_def)
 
@@ -152,6 +188,8 @@
 lemma vimage2p_Grp: "vimage2p f g P = Grp UNIV f OO P OO (Grp UNIV g)\<inverse>\<inverse>"
   unfolding vimage2p_def Grp_def by auto
 
+ML_file "Tools/BNF/bnf_util.ML"
+ML_file "Tools/BNF/bnf_tactics.ML"
 ML_file "Tools/BNF/bnf_def_tactics.ML"
 ML_file "Tools/BNF/bnf_def.ML"
 
diff -r 5004aca20821 -r 882091eb1e9a src/HOL/BNF_Examples/Stream_Processor.thy
--- a/src/HOL/BNF_Examples/Stream_Processor.thy	Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/BNF_Examples/Stream_Processor.thy	Fri Jun 27 10:11:44 2014 +0200
@@ -126,7 +126,7 @@
 (*will be provided by the package*)
 lemma sp\<^sub>\<mu>_rel_map_map[unfolded vimage2p_def, simp]:
   "rel_sp\<^sub>\<mu> R1 R2 (map_sp\<^sub>\<mu> f1 f2 sp) (map_sp\<^sub>\<mu> g1 g2 sp') =
-  rel_sp\<^sub>\<mu> (BNF_Util.vimage2p f1 g1 R1) (BNF_Util.vimage2p f2 g2 R2) sp sp'"
+  rel_sp\<^sub>\<mu> (BNF_Def.vimage2p f1 g1 R1) (BNF_Def.vimage2p f2 g2 R2) sp sp'"
 by (tactic {*
   let val ks = 1 upto 2;
   in
diff -r 5004aca20821 -r 882091eb1e9a src/HOL/BNF_Util.thy
--- a/src/HOL/BNF_Util.thy	Fri Jun 27 10:11:44 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,53 +0,0 @@
-(*  Title:      HOL/BNF_Util.thy
-    Author:     Dmitriy Traytel, TU Muenchen
-    Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2012
-
-Library for bounded natural functors.
-*)
-
-header {* Library for Bounded Natural Functors *}
-
-theory BNF_Util
-imports BNF_Cardinal_Arithmetic
-begin
-
-definition
-  rel_fun :: "('a \<Rightarrow> 'c \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'd \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('c \<Rightarrow> 'd) \<Rightarrow> bool"
-where
-  "rel_fun A B = (\<lambda>f g. \<forall>x y. A x y \<longrightarrow> B (f x) (g y))"
-
-lemma rel_funI [intro]:
-  assumes "\<And>x y. A x y \<Longrightarrow> B (f x) (g y)"
-  shows "rel_fun A B f g"
-  using assms by (simp add: rel_fun_def)
-
-lemma rel_funD:
-  assumes "rel_fun A B f g" and "A x y"
-  shows "B (f x) (g y)"
-  using assms by (simp add: rel_fun_def)
-
-definition collect where
-"collect F x = (\<Union>f \<in> F. f x)"
-
-lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
-by simp
-
-lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
-by simp
-
-lemma bijI': "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
-unfolding bij_def inj_on_def by auto blast
-
-(* Operator: *)
-definition "Gr A f = {(a, f a) | a. a \<in> A}"
-
-definition "Grp A f = (\<lambda>a b. b = f a \<and> a \<in> A)"
-
-definition vimage2p where
-  "vimage2p f g R = (\<lambda>x y. R (f x) (g y))"
-
-ML_file "Tools/BNF/bnf_util.ML"
-ML_file "Tools/BNF/bnf_tactics.ML"
-
-end
diff -r 5004aca20821 -r 882091eb1e9a src/HOL/Library/Countable_Set_Type.thy
--- a/src/HOL/Library/Countable_Set_Type.thy	Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Library/Countable_Set_Type.thy	Fri Jun 27 10:11:44 2014 +0200
@@ -11,7 +11,7 @@
 imports Countable_Set Cardinal_Notations
 begin
 
-abbreviation "Grp \<equiv> BNF_Util.Grp"
+abbreviation "Grp \<equiv> BNF_Def.Grp"
 
 
 subsection{* Cardinal stuff *}
diff -r 5004aca20821 -r 882091eb1e9a src/HOL/Library/FSet.thy
--- a/src/HOL/Library/FSet.thy	Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Library/FSet.thy	Fri Jun 27 10:11:44 2014 +0200
@@ -931,8 +931,8 @@
 
 lemma rel_fset_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>
- ((BNF_Util.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage fst))\<inverse>\<inverse> OO
-  BNF_Util.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage snd)) a b" (is "?L = ?R")
+ ((BNF_Def.Grp {a. fset a \<subseteq> {(a, b). R a b}} (fimage fst))\<inverse>\<inverse> OO
+  BNF_Def.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'")
diff -r 5004aca20821 -r 882091eb1e9a src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Lifting.thy	Fri Jun 27 10:11:44 2014 +0200
@@ -163,7 +163,7 @@
 
 lemma Quotient_alt_def5:
   "Quotient R Abs Rep T \<longleftrightarrow>
-    T \<le> BNF_Util.Grp UNIV Abs \<and> BNF_Util.Grp UNIV Rep \<le> T\<inverse>\<inverse> \<and> R = T OO T\<inverse>\<inverse>"
+    T \<le> BNF_Def.Grp UNIV Abs \<and> BNF_Def.Grp UNIV Rep \<le> T\<inverse>\<inverse> \<and> R = T OO T\<inverse>\<inverse>"
   unfolding Quotient_alt_def4 Grp_def by blast
 
 lemma fun_quotient:
diff -r 5004aca20821 -r 882091eb1e9a src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Fri Jun 27 10:11:44 2014 +0200
+++ b/src/HOL/Transfer.thy	Fri Jun 27 10:11:44 2014 +0200
@@ -230,7 +230,7 @@
 definition eq_onp :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool" 
   where "eq_onp R = (\<lambda>x y. R x \<and> x = y)"
 
-lemma eq_onp_Grp: "eq_onp P = BNF_Util.Grp (Collect P) id" 
+lemma eq_onp_Grp: "eq_onp P = BNF_Def.Grp (Collect P) id" 
 unfolding eq_onp_def Grp_def by auto 
 
 lemma eq_onp_to_eq: