# HG changeset patch
# User blanchet
# Date 1409582080 -7200
# Node ID 43a1ba26a8cbdf197569a18d01515d29ceec1492
# Parent  b7cab82f488e9696e94bfb98cd50b9d9cdef49fa
renamed BNF theories

diff -r b7cab82f488e -r 43a1ba26a8cb src/HOL/BNF_Comp.thy
--- a/src/HOL/BNF_Comp.thy	Mon Sep 01 16:34:39 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,174 +0,0 @@
-(*  Title:      HOL/BNF_Comp.thy
-    Author:     Dmitriy Traytel, TU Muenchen
-    Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2012, 2013, 2014
-
-Composition of bounded natural functors.
-*)
-
-header {* Composition of Bounded Natural Functors *}
-
-theory BNF_Comp
-imports BNF_Def
-begin
-
-lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})"
-by (rule ext) simp
-
-lemma Union_natural: "Union o image (image f) = image f o Union"
-by (rule ext) (auto simp only: comp_apply)
-
-lemma in_Union_o_assoc: "x \<in> (Union o gset o gmap) A \<Longrightarrow> x \<in> (Union o (gset o gmap)) A"
-by (unfold comp_assoc)
-
-lemma comp_single_set_bd:
-  assumes fbd_Card_order: "Card_order fbd" and
-    fset_bd: "\<And>x. |fset x| \<le>o fbd" and
-    gset_bd: "\<And>x. |gset x| \<le>o gbd"
-  shows "|\<Union>(fset ` gset x)| \<le>o gbd *c fbd"
-apply simp
-apply (rule ordLeq_transitive)
-apply (rule card_of_UNION_Sigma)
-apply (subst SIGMA_CSUM)
-apply (rule ordLeq_transitive)
-apply (rule card_of_Csum_Times')
-apply (rule fbd_Card_order)
-apply (rule ballI)
-apply (rule fset_bd)
-apply (rule ordLeq_transitive)
-apply (rule cprod_mono1)
-apply (rule gset_bd)
-apply (rule ordIso_imp_ordLeq)
-apply (rule ordIso_refl)
-apply (rule Card_order_cprod)
-done
-
-lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
-apply (erule ordIso_transitive)
-apply (frule csum_absorb2')
-apply (erule ordLeq_refl)
-by simp
-
-lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r"
-apply (erule ordIso_transitive)
-apply (rule cprod_infinite)
-by simp
-
-lemma Union_image_insert: "\<Union>(f ` insert a B) = f a \<union> \<Union>(f ` B)"
-by simp
-
-lemma Union_image_empty: "A \<union> \<Union>(f ` {}) = A"
-by simp
-
-lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F"
-by (rule ext) (auto simp add: collect_def)
-
-lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})"
-by blast
-
-lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
-by blast
-
-lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
-by (unfold comp_apply collect_def) simp
-
-lemma wpull_cong:
-"\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2"
-by simp
-
-lemma Grp_fst_snd: "(Grp (Collect (split R)) fst)^--1 OO Grp (Collect (split R)) snd = R"
-unfolding Grp_def fun_eq_iff relcompp.simps by auto
-
-lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)^--1 OO Grp A g = (Grp B f)^--1 OO Grp B g"
-by (rule arg_cong)
-
-lemma vimage2p_relcompp_mono: "R OO S \<le> T \<Longrightarrow>
-  vimage2p f g R OO vimage2p g h S \<le> vimage2p f h T"
-  unfolding vimage2p_def by auto
-
-lemma type_copy_map_cong0: "M (g x) = N (h x) \<Longrightarrow> (f o M o g) x = (f o N o h) x"
-  by auto
-
-lemma type_copy_set_bd: "(\<And>y. |S y| \<le>o bd) \<Longrightarrow> |(S o Rep) x| \<le>o bd"
-  by auto
-
-lemma vimage2p_cong: "R = S \<Longrightarrow> vimage2p f g R = vimage2p f g S"
-  by simp
-
-context
-fixes Rep Abs
-assumes type_copy: "type_definition Rep Abs UNIV"
-begin
-
-lemma type_copy_map_id0: "M = id \<Longrightarrow> Abs o M o Rep = id"
-  using type_definition.Rep_inverse[OF type_copy] by auto
-
-lemma type_copy_map_comp0: "M = M1 o M2 \<Longrightarrow> f o M o g = (f o M1 o Rep) o (Abs o M2 o g)"
-  using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto
-
-lemma type_copy_set_map0: "S o M = image f o S' \<Longrightarrow> (S o Rep) o (Abs o M o g) = image f o (S' o g)"
-  using type_definition.Abs_inverse[OF type_copy UNIV_I] by (auto simp: o_def fun_eq_iff)
-
-lemma type_copy_wit: "x \<in> (S o Rep) (Abs y) \<Longrightarrow> x \<in> S y"
-  using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto
-
-lemma type_copy_vimage2p_Grp_Rep: "vimage2p f Rep (Grp (Collect P) h) =
-    Grp (Collect (\<lambda>x. P (f x))) (Abs o h o f)"
-  unfolding vimage2p_def Grp_def fun_eq_iff
-  by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
-   type_definition.Rep_inverse[OF type_copy] dest: sym)
-
-lemma type_copy_vimage2p_Grp_Abs:
-  "\<And>h. vimage2p g Abs (Grp (Collect P) h) = Grp (Collect (\<lambda>x. P (g x))) (Rep o h o g)"
-  unfolding vimage2p_def Grp_def fun_eq_iff
-  by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
-   type_definition.Rep_inverse[OF type_copy] dest: sym)
-
-lemma type_copy_ex_RepI: "(\<exists>b. F b) = (\<exists>b. F (Rep b))"
-proof safe
-  fix b assume "F b"
-  show "\<exists>b'. F (Rep b')"
-  proof (rule exI)
-    from `F b` show "F (Rep (Abs b))" using type_definition.Abs_inverse[OF type_copy] by auto
-  qed
-qed blast
-
-lemma vimage2p_relcompp_converse:
-  "vimage2p f g (R^--1 OO S) = (vimage2p Rep f R)^--1 OO vimage2p Rep g S"
-  unfolding vimage2p_def relcompp.simps conversep.simps fun_eq_iff image_def
-  by (auto simp: type_copy_ex_RepI)
-
-end
-
-bnf DEADID: 'a
-  map: "id :: 'a \<Rightarrow> 'a"
-  bd: natLeq
-  rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
-by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite)
-
-definition id_bnf_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp \<equiv> (\<lambda>x. x)"
-
-lemma id_bnf_comp_apply: "id_bnf_comp x = x"
-  unfolding id_bnf_comp_def by simp
-
-bnf ID: 'a
-  map: "id_bnf_comp :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
-  sets: "\<lambda>x. {x}"
-  bd: natLeq
-  rel: "id_bnf_comp :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
-unfolding id_bnf_comp_def
-apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
-apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
-apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
-done
-
-lemma type_definition_id_bnf_comp_UNIV: "type_definition id_bnf_comp id_bnf_comp UNIV"
-  unfolding id_bnf_comp_def by unfold_locales auto
-
-ML_file "Tools/BNF/bnf_comp_tactics.ML"
-ML_file "Tools/BNF/bnf_comp.ML"
-
-hide_const (open) id_bnf_comp
-hide_fact (open) id_bnf_comp_def type_definition_id_bnf_comp_UNIV
-
-end
diff -r b7cab82f488e -r 43a1ba26a8cb src/HOL/BNF_Composition.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF_Composition.thy	Mon Sep 01 16:34:40 2014 +0200
@@ -0,0 +1,174 @@
+(*  Title:      HOL/BNF_Composition.thy
+    Author:     Dmitriy Traytel, TU Muenchen
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2012, 2013, 2014
+
+Composition of bounded natural functors.
+*)
+
+header {* Composition of Bounded Natural Functors *}
+
+theory BNF_Composition
+imports BNF_Def
+begin
+
+lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})"
+  by (rule ext) simp
+
+lemma Union_natural: "Union o image (image f) = image f o Union"
+  by (rule ext) (auto simp only: comp_apply)
+
+lemma in_Union_o_assoc: "x \<in> (Union o gset o gmap) A \<Longrightarrow> x \<in> (Union o (gset o gmap)) A"
+  by (unfold comp_assoc)
+
+lemma comp_single_set_bd:
+  assumes fbd_Card_order: "Card_order fbd" and
+    fset_bd: "\<And>x. |fset x| \<le>o fbd" and
+    gset_bd: "\<And>x. |gset x| \<le>o gbd"
+  shows "|\<Union>(fset ` gset x)| \<le>o gbd *c fbd"
+  apply simp
+  apply (rule ordLeq_transitive)
+  apply (rule card_of_UNION_Sigma)
+  apply (subst SIGMA_CSUM)
+  apply (rule ordLeq_transitive)
+  apply (rule card_of_Csum_Times')
+  apply (rule fbd_Card_order)
+  apply (rule ballI)
+  apply (rule fset_bd)
+  apply (rule ordLeq_transitive)
+  apply (rule cprod_mono1)
+  apply (rule gset_bd)
+  apply (rule ordIso_imp_ordLeq)
+  apply (rule ordIso_refl)
+  apply (rule Card_order_cprod)
+  done
+
+lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
+  apply (erule ordIso_transitive)
+  apply (frule csum_absorb2')
+  apply (erule ordLeq_refl)
+  by simp
+
+lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r"
+  apply (erule ordIso_transitive)
+  apply (rule cprod_infinite)
+  by simp
+
+lemma Union_image_insert: "\<Union>(f ` insert a B) = f a \<union> \<Union>(f ` B)"
+  by simp
+
+lemma Union_image_empty: "A \<union> \<Union>(f ` {}) = A"
+  by simp
+
+lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F"
+  by (rule ext) (auto simp add: collect_def)
+
+lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})"
+  by blast
+
+lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
+  by blast
+
+lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>((\<lambda>f. f x) ` X)| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
+  by (unfold comp_apply collect_def) simp
+
+lemma wpull_cong:
+  "\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2"
+  by simp
+
+lemma Grp_fst_snd: "(Grp (Collect (split R)) fst)^--1 OO Grp (Collect (split R)) snd = R"
+  unfolding Grp_def fun_eq_iff relcompp.simps by auto
+
+lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)^--1 OO Grp A g = (Grp B f)^--1 OO Grp B g"
+  by (rule arg_cong)
+
+lemma vimage2p_relcompp_mono: "R OO S \<le> T \<Longrightarrow>
+  vimage2p f g R OO vimage2p g h S \<le> vimage2p f h T"
+  unfolding vimage2p_def by auto
+
+lemma type_copy_map_cong0: "M (g x) = N (h x) \<Longrightarrow> (f o M o g) x = (f o N o h) x"
+  by auto
+
+lemma type_copy_set_bd: "(\<And>y. |S y| \<le>o bd) \<Longrightarrow> |(S o Rep) x| \<le>o bd"
+  by auto
+
+lemma vimage2p_cong: "R = S \<Longrightarrow> vimage2p f g R = vimage2p f g S"
+  by simp
+
+context
+  fixes Rep Abs
+  assumes type_copy: "type_definition Rep Abs UNIV"
+begin
+
+lemma type_copy_map_id0: "M = id \<Longrightarrow> Abs o M o Rep = id"
+  using type_definition.Rep_inverse[OF type_copy] by auto
+
+lemma type_copy_map_comp0: "M = M1 o M2 \<Longrightarrow> f o M o g = (f o M1 o Rep) o (Abs o M2 o g)"
+  using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto
+
+lemma type_copy_set_map0: "S o M = image f o S' \<Longrightarrow> (S o Rep) o (Abs o M o g) = image f o (S' o g)"
+  using type_definition.Abs_inverse[OF type_copy UNIV_I] by (auto simp: o_def fun_eq_iff)
+
+lemma type_copy_wit: "x \<in> (S o Rep) (Abs y) \<Longrightarrow> x \<in> S y"
+  using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto
+
+lemma type_copy_vimage2p_Grp_Rep: "vimage2p f Rep (Grp (Collect P) h) =
+    Grp (Collect (\<lambda>x. P (f x))) (Abs o h o f)"
+  unfolding vimage2p_def Grp_def fun_eq_iff
+  by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
+   type_definition.Rep_inverse[OF type_copy] dest: sym)
+
+lemma type_copy_vimage2p_Grp_Abs:
+  "\<And>h. vimage2p g Abs (Grp (Collect P) h) = Grp (Collect (\<lambda>x. P (g x))) (Rep o h o g)"
+  unfolding vimage2p_def Grp_def fun_eq_iff
+  by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
+   type_definition.Rep_inverse[OF type_copy] dest: sym)
+
+lemma type_copy_ex_RepI: "(\<exists>b. F b) = (\<exists>b. F (Rep b))"
+proof safe
+  fix b assume "F b"
+  show "\<exists>b'. F (Rep b')"
+  proof (rule exI)
+    from `F b` show "F (Rep (Abs b))" using type_definition.Abs_inverse[OF type_copy] by auto
+  qed
+qed blast
+
+lemma vimage2p_relcompp_converse:
+  "vimage2p f g (R^--1 OO S) = (vimage2p Rep f R)^--1 OO vimage2p Rep g S"
+  unfolding vimage2p_def relcompp.simps conversep.simps fun_eq_iff image_def
+  by (auto simp: type_copy_ex_RepI)
+
+end
+
+bnf DEADID: 'a
+  map: "id :: 'a \<Rightarrow> 'a"
+  bd: natLeq
+  rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
+  by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite)
+
+definition id_bnf_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp \<equiv> (\<lambda>x. x)"
+
+lemma id_bnf_comp_apply: "id_bnf_comp x = x"
+  unfolding id_bnf_comp_def by simp
+
+bnf ID: 'a
+  map: "id_bnf_comp :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
+  sets: "\<lambda>x. {x}"
+  bd: natLeq
+  rel: "id_bnf_comp :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
+  unfolding id_bnf_comp_def
+  apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
+  apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
+  apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
+  done
+
+lemma type_definition_id_bnf_comp_UNIV: "type_definition id_bnf_comp id_bnf_comp UNIV"
+  unfolding id_bnf_comp_def by unfold_locales auto
+
+ML_file "Tools/BNF/bnf_comp_tactics.ML"
+ML_file "Tools/BNF/bnf_comp.ML"
+
+hide_const (open) id_bnf_comp
+hide_fact (open) id_bnf_comp_def type_definition_id_bnf_comp_UNIV
+
+end
diff -r b7cab82f488e -r 43a1ba26a8cb src/HOL/BNF_FP_Base.thy
--- a/src/HOL/BNF_FP_Base.thy	Mon Sep 01 16:34:39 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,232 +0,0 @@
-(*  Title:      HOL/BNF_FP_Base.thy
-    Author:     Lorenz Panny, TU Muenchen
-    Author:     Dmitriy Traytel, TU Muenchen
-    Author:     Jasmin Blanchette, TU Muenchen
-    Author:     Martin Desharnais, TU Muenchen
-    Copyright   2012, 2013, 2014
-
-Shared fixed point operations on bounded natural functors.
-*)
-
-header {* Shared Fixed Point Operations on Bounded Natural Functors *}
-
-theory BNF_FP_Base
-imports BNF_Comp Basic_BNFs
-begin
-
-lemma False_imp_eq_True: "(False \<Longrightarrow> Q) \<equiv> Trueprop True"
-  by default simp_all
-
-lemma conj_imp_eq_imp_imp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)"
-  by default simp_all
-
-lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
-by auto
-
-lemma predicate2D_conj: "P \<le> Q \<and> R \<Longrightarrow> P x y \<Longrightarrow> R \<and> Q x y"
-  by auto
-
-lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
-by blast
-
-lemma case_unit_Unity: "(case u of () \<Rightarrow> f) = f"
-by (cases u) (hypsubst, rule unit.case)
-
-lemma case_prod_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p"
-by simp
-
-lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
-by simp
-
-lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
-unfolding comp_def fun_eq_iff by simp
-
-lemma o_bij:
-  assumes gf: "g \<circ> f = id" and fg: "f \<circ> g = id"
-  shows "bij f"
-unfolding bij_def inj_on_def surj_def proof safe
-  fix a1 a2 assume "f a1 = f a2"
-  hence "g ( f a1) = g (f a2)" by simp
-  thus "a1 = a2" using gf unfolding fun_eq_iff by simp
-next
-  fix b
-  have "b = f (g b)"
-  using fg unfolding fun_eq_iff by simp
-  thus "EX a. b = f a" by blast
-qed
-
-lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp
-
-lemma case_sum_step:
-"case_sum (case_sum f' g') g (Inl p) = case_sum f' g' p"
-"case_sum f (case_sum f' g') (Inr p) = case_sum f' g' p"
-by auto
-
-lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
-by blast
-
-lemma type_copy_obj_one_point_absE:
-  assumes "type_definition Rep Abs UNIV" "\<forall>x. s = Abs x \<longrightarrow> P" shows P
-  using type_definition.Rep_inverse[OF assms(1)]
-  by (intro mp[OF spec[OF assms(2), of "Rep s"]]) simp
-
-lemma obj_sumE_f:
-  assumes "\<forall>x. s = f (Inl x) \<longrightarrow> P" "\<forall>x. s = f (Inr x) \<longrightarrow> P"
-  shows "\<forall>x. s = f x \<longrightarrow> P"
-proof
-  fix x from assms show "s = f x \<longrightarrow> P" by (cases x) auto
-qed
-
-lemma case_sum_if:
-"case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)"
-by simp
-
-lemma prod_set_simps:
-"fsts (x, y) = {x}"
-"snds (x, y) = {y}"
-unfolding fsts_def snds_def by simp+
-
-lemma sum_set_simps:
-"setl (Inl x) = {x}"
-"setl (Inr x) = {}"
-"setr (Inl x) = {}"
-"setr (Inr x) = {x}"
-unfolding sum_set_defs by simp+
-
-lemma Inl_Inr_False: "(Inl x = Inr y) = False"
-  by simp
-
-lemma Inr_Inl_False: "(Inr x = Inl y) = False"
-  by simp
-
-lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
-by blast
-
-lemma rewriteR_comp_comp: "\<lbrakk>g \<circ> h = r\<rbrakk> \<Longrightarrow> f \<circ> g \<circ> h = f \<circ> r"
-  unfolding comp_def fun_eq_iff by auto
-
-lemma rewriteR_comp_comp2: "\<lbrakk>g \<circ> h = r1 \<circ> r2; f \<circ> r1 = l\<rbrakk> \<Longrightarrow> f \<circ> g \<circ> h = l \<circ> r2"
-  unfolding comp_def fun_eq_iff by auto
-
-lemma rewriteL_comp_comp: "\<lbrakk>f \<circ> g = l\<rbrakk> \<Longrightarrow> f \<circ> (g \<circ> h) = l \<circ> h"
-  unfolding comp_def fun_eq_iff by auto
-
-lemma rewriteL_comp_comp2: "\<lbrakk>f \<circ> g = l1 \<circ> l2; l2 \<circ> h = r\<rbrakk> \<Longrightarrow> f \<circ> (g \<circ> h) = l1 \<circ> r"
-  unfolding comp_def fun_eq_iff by auto
-
-lemma convol_o: "\<langle>f, g\<rangle> \<circ> h = \<langle>f \<circ> h, g \<circ> h\<rangle>"
-  unfolding convol_def by auto
-
-lemma map_prod_o_convol: "map_prod h1 h2 \<circ> \<langle>f, g\<rangle> = \<langle>h1 \<circ> f, h2 \<circ> g\<rangle>"
-  unfolding convol_def by auto
-
-lemma map_prod_o_convol_id: "(map_prod f id \<circ> \<langle>id, g\<rangle>) x = \<langle>id \<circ> f, g\<rangle> x"
-  unfolding map_prod_o_convol id_comp comp_id ..
-
-lemma o_case_sum: "h \<circ> case_sum f g = case_sum (h \<circ> f) (h \<circ> g)"
-  unfolding comp_def by (auto split: sum.splits)
-
-lemma case_sum_o_map_sum: "case_sum f g \<circ> map_sum h1 h2 = case_sum (f \<circ> h1) (g \<circ> h2)"
-  unfolding comp_def by (auto split: sum.splits)
-
-lemma case_sum_o_map_sum_id: "(case_sum id g \<circ> map_sum f id) x = case_sum (f \<circ> id) g x"
-  unfolding case_sum_o_map_sum id_comp comp_id ..
-
-lemma rel_fun_def_butlast:
-  "rel_fun R (rel_fun S T) f g = (\<forall>x y. R x y \<longrightarrow> (rel_fun S T) (f x) (g y))"
-  unfolding rel_fun_def ..
-
-lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)"
-  by auto
-
-lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)"
-  by auto
-
-lemma eq_le_Grp_id_iff: "(op = \<le> Grp (Collect R) id) = (All R)"
-  unfolding Grp_def id_apply by blast
-
-lemma Grp_id_mono_subst: "(\<And>x y. Grp P id x y \<Longrightarrow> Grp Q id (f x) (f y)) \<equiv>
-   (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
-  unfolding Grp_def by rule auto
-
-lemma vimage2p_mono: "vimage2p f g R x y \<Longrightarrow> R \<le> S \<Longrightarrow> vimage2p f g S x y"
-  unfolding vimage2p_def by blast
-
-lemma vimage2p_refl: "(\<And>x. R x x) \<Longrightarrow> vimage2p f f R x x"
-  unfolding vimage2p_def by auto
-
-lemma
-  assumes "type_definition Rep Abs UNIV"
-  shows type_copy_Rep_o_Abs: "Rep \<circ> Abs = id" and type_copy_Abs_o_Rep: "Abs \<circ> Rep = id"
-  unfolding fun_eq_iff comp_apply id_apply
-    type_definition.Abs_inverse[OF assms UNIV_I] type_definition.Rep_inverse[OF assms] by simp_all
-
-lemma type_copy_map_comp0_undo:
-  assumes "type_definition Rep Abs UNIV"
-          "type_definition Rep' Abs' UNIV"
-          "type_definition Rep'' Abs'' UNIV"
-  shows "Abs' \<circ> M \<circ> Rep'' = (Abs' \<circ> M1 \<circ> Rep) \<circ> (Abs \<circ> M2 \<circ> Rep'') \<Longrightarrow> M1 \<circ> M2 = M"
-  by (rule sym) (auto simp: fun_eq_iff type_definition.Abs_inject[OF assms(2) UNIV_I UNIV_I]
-    type_definition.Abs_inverse[OF assms(1) UNIV_I]
-    type_definition.Abs_inverse[OF assms(3) UNIV_I] dest: spec[of _ "Abs'' x" for x])
-
-lemma vimage2p_id: "vimage2p id id R = R"
-  unfolding vimage2p_def by auto
-
-lemma vimage2p_comp: "vimage2p (f1 \<circ> f2) (g1 \<circ> g2) = vimage2p f2 g2 \<circ> vimage2p f1 g1"
-  unfolding fun_eq_iff vimage2p_def o_apply by simp
-
-lemma fun_cong_unused_0: "f = (\<lambda>x. g) \<Longrightarrow> f (\<lambda>x. 0) = g"
-  by (erule arg_cong)
-
-lemma inj_on_convol_ident: "inj_on (\<lambda>x. (x, f x)) X"
-  unfolding inj_on_def by simp
-
-lemma case_prod_app: "case_prod f x y = case_prod (\<lambda>l r. f l r y) x"
-  by (case_tac x) simp
-
-lemma case_sum_map_sum: "case_sum l r (map_sum f g x) = case_sum (l \<circ> f) (r \<circ> g) x"
-  by (case_tac x) simp+
-
-lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x"
-  by (case_tac x) simp+
-
-lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)"
-  by (simp add: inj_on_def)
-
-lemma eq_ifI: "(P \<longrightarrow> t = u1) \<Longrightarrow> (\<not> P \<longrightarrow> t = u2) \<Longrightarrow> t = (if P then u1 else u2)"
-  by simp
-
-ML_file "Tools/BNF/bnf_fp_util.ML"
-ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
-ML_file "Tools/BNF/bnf_lfp_size.ML"
-ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
-ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML"
-ML_file "Tools/BNF/bnf_fp_n2m.ML"
-ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML"
-
-ML_file "Tools/Function/old_size.ML"
-setup Old_Size.setup
-
-lemma size_bool[code]: "size (b\<Colon>bool) = 0"
-  by (cases b) auto
-
-lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"
-  by (induct n) simp_all
-
-declare prod.size[no_atp]
-
-lemma size_sum_o_map: "size_sum g1 g2 \<circ> map_sum f1 f2 = size_sum (g1 \<circ> f1) (g2 \<circ> f2)"
-  by (rule ext) (case_tac x, auto)
-
-lemma size_prod_o_map: "size_prod g1 g2 \<circ> map_prod f1 f2 = size_prod (g1 \<circ> f1) (g2 \<circ> f2)"
-  by (rule ext) auto
-
-setup {*
-BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size}
-  @{thms size_sum_o_map}
-#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size}
-  @{thms size_prod_o_map}
-*}
-
-end
diff -r b7cab82f488e -r 43a1ba26a8cb src/HOL/BNF_Fixpoint_Base.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF_Fixpoint_Base.thy	Mon Sep 01 16:34:40 2014 +0200
@@ -0,0 +1,232 @@
+(*  Title:      HOL/BNF_Fixpoint_Base.thy
+    Author:     Lorenz Panny, TU Muenchen
+    Author:     Dmitriy Traytel, TU Muenchen
+    Author:     Jasmin Blanchette, TU Muenchen
+    Author:     Martin Desharnais, TU Muenchen
+    Copyright   2012, 2013, 2014
+
+Shared fixed point operations on bounded natural functors.
+*)
+
+header {* Shared Fixed Point Operations on Bounded Natural Functors *}
+
+theory BNF_Fixpoint_Base
+imports BNF_Composition Basic_BNFs
+begin
+
+lemma False_imp_eq_True: "(False \<Longrightarrow> Q) \<equiv> Trueprop True"
+  by default simp_all
+
+lemma conj_imp_eq_imp_imp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)"
+  by default simp_all
+
+lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
+by auto
+
+lemma predicate2D_conj: "P \<le> Q \<and> R \<Longrightarrow> P x y \<Longrightarrow> R \<and> Q x y"
+  by auto
+
+lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
+by blast
+
+lemma case_unit_Unity: "(case u of () \<Rightarrow> f) = f"
+by (cases u) (hypsubst, rule unit.case)
+
+lemma case_prod_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p"
+by simp
+
+lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
+by simp
+
+lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
+unfolding comp_def fun_eq_iff by simp
+
+lemma o_bij:
+  assumes gf: "g \<circ> f = id" and fg: "f \<circ> g = id"
+  shows "bij f"
+unfolding bij_def inj_on_def surj_def proof safe
+  fix a1 a2 assume "f a1 = f a2"
+  hence "g ( f a1) = g (f a2)" by simp
+  thus "a1 = a2" using gf unfolding fun_eq_iff by simp
+next
+  fix b
+  have "b = f (g b)"
+  using fg unfolding fun_eq_iff by simp
+  thus "EX a. b = f a" by blast
+qed
+
+lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp
+
+lemma case_sum_step:
+"case_sum (case_sum f' g') g (Inl p) = case_sum f' g' p"
+"case_sum f (case_sum f' g') (Inr p) = case_sum f' g' p"
+by auto
+
+lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
+by blast
+
+lemma type_copy_obj_one_point_absE:
+  assumes "type_definition Rep Abs UNIV" "\<forall>x. s = Abs x \<longrightarrow> P" shows P
+  using type_definition.Rep_inverse[OF assms(1)]
+  by (intro mp[OF spec[OF assms(2), of "Rep s"]]) simp
+
+lemma obj_sumE_f:
+  assumes "\<forall>x. s = f (Inl x) \<longrightarrow> P" "\<forall>x. s = f (Inr x) \<longrightarrow> P"
+  shows "\<forall>x. s = f x \<longrightarrow> P"
+proof
+  fix x from assms show "s = f x \<longrightarrow> P" by (cases x) auto
+qed
+
+lemma case_sum_if:
+"case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)"
+by simp
+
+lemma prod_set_simps:
+"fsts (x, y) = {x}"
+"snds (x, y) = {y}"
+unfolding fsts_def snds_def by simp+
+
+lemma sum_set_simps:
+"setl (Inl x) = {x}"
+"setl (Inr x) = {}"
+"setr (Inl x) = {}"
+"setr (Inr x) = {x}"
+unfolding sum_set_defs by simp+
+
+lemma Inl_Inr_False: "(Inl x = Inr y) = False"
+  by simp
+
+lemma Inr_Inl_False: "(Inr x = Inl y) = False"
+  by simp
+
+lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
+by blast
+
+lemma rewriteR_comp_comp: "\<lbrakk>g \<circ> h = r\<rbrakk> \<Longrightarrow> f \<circ> g \<circ> h = f \<circ> r"
+  unfolding comp_def fun_eq_iff by auto
+
+lemma rewriteR_comp_comp2: "\<lbrakk>g \<circ> h = r1 \<circ> r2; f \<circ> r1 = l\<rbrakk> \<Longrightarrow> f \<circ> g \<circ> h = l \<circ> r2"
+  unfolding comp_def fun_eq_iff by auto
+
+lemma rewriteL_comp_comp: "\<lbrakk>f \<circ> g = l\<rbrakk> \<Longrightarrow> f \<circ> (g \<circ> h) = l \<circ> h"
+  unfolding comp_def fun_eq_iff by auto
+
+lemma rewriteL_comp_comp2: "\<lbrakk>f \<circ> g = l1 \<circ> l2; l2 \<circ> h = r\<rbrakk> \<Longrightarrow> f \<circ> (g \<circ> h) = l1 \<circ> r"
+  unfolding comp_def fun_eq_iff by auto
+
+lemma convol_o: "\<langle>f, g\<rangle> \<circ> h = \<langle>f \<circ> h, g \<circ> h\<rangle>"
+  unfolding convol_def by auto
+
+lemma map_prod_o_convol: "map_prod h1 h2 \<circ> \<langle>f, g\<rangle> = \<langle>h1 \<circ> f, h2 \<circ> g\<rangle>"
+  unfolding convol_def by auto
+
+lemma map_prod_o_convol_id: "(map_prod f id \<circ> \<langle>id, g\<rangle>) x = \<langle>id \<circ> f, g\<rangle> x"
+  unfolding map_prod_o_convol id_comp comp_id ..
+
+lemma o_case_sum: "h \<circ> case_sum f g = case_sum (h \<circ> f) (h \<circ> g)"
+  unfolding comp_def by (auto split: sum.splits)
+
+lemma case_sum_o_map_sum: "case_sum f g \<circ> map_sum h1 h2 = case_sum (f \<circ> h1) (g \<circ> h2)"
+  unfolding comp_def by (auto split: sum.splits)
+
+lemma case_sum_o_map_sum_id: "(case_sum id g \<circ> map_sum f id) x = case_sum (f \<circ> id) g x"
+  unfolding case_sum_o_map_sum id_comp comp_id ..
+
+lemma rel_fun_def_butlast:
+  "rel_fun R (rel_fun S T) f g = (\<forall>x y. R x y \<longrightarrow> (rel_fun S T) (f x) (g y))"
+  unfolding rel_fun_def ..
+
+lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)"
+  by auto
+
+lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)"
+  by auto
+
+lemma eq_le_Grp_id_iff: "(op = \<le> Grp (Collect R) id) = (All R)"
+  unfolding Grp_def id_apply by blast
+
+lemma Grp_id_mono_subst: "(\<And>x y. Grp P id x y \<Longrightarrow> Grp Q id (f x) (f y)) \<equiv>
+   (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
+  unfolding Grp_def by rule auto
+
+lemma vimage2p_mono: "vimage2p f g R x y \<Longrightarrow> R \<le> S \<Longrightarrow> vimage2p f g S x y"
+  unfolding vimage2p_def by blast
+
+lemma vimage2p_refl: "(\<And>x. R x x) \<Longrightarrow> vimage2p f f R x x"
+  unfolding vimage2p_def by auto
+
+lemma
+  assumes "type_definition Rep Abs UNIV"
+  shows type_copy_Rep_o_Abs: "Rep \<circ> Abs = id" and type_copy_Abs_o_Rep: "Abs \<circ> Rep = id"
+  unfolding fun_eq_iff comp_apply id_apply
+    type_definition.Abs_inverse[OF assms UNIV_I] type_definition.Rep_inverse[OF assms] by simp_all
+
+lemma type_copy_map_comp0_undo:
+  assumes "type_definition Rep Abs UNIV"
+          "type_definition Rep' Abs' UNIV"
+          "type_definition Rep'' Abs'' UNIV"
+  shows "Abs' \<circ> M \<circ> Rep'' = (Abs' \<circ> M1 \<circ> Rep) \<circ> (Abs \<circ> M2 \<circ> Rep'') \<Longrightarrow> M1 \<circ> M2 = M"
+  by (rule sym) (auto simp: fun_eq_iff type_definition.Abs_inject[OF assms(2) UNIV_I UNIV_I]
+    type_definition.Abs_inverse[OF assms(1) UNIV_I]
+    type_definition.Abs_inverse[OF assms(3) UNIV_I] dest: spec[of _ "Abs'' x" for x])
+
+lemma vimage2p_id: "vimage2p id id R = R"
+  unfolding vimage2p_def by auto
+
+lemma vimage2p_comp: "vimage2p (f1 \<circ> f2) (g1 \<circ> g2) = vimage2p f2 g2 \<circ> vimage2p f1 g1"
+  unfolding fun_eq_iff vimage2p_def o_apply by simp
+
+lemma fun_cong_unused_0: "f = (\<lambda>x. g) \<Longrightarrow> f (\<lambda>x. 0) = g"
+  by (erule arg_cong)
+
+lemma inj_on_convol_ident: "inj_on (\<lambda>x. (x, f x)) X"
+  unfolding inj_on_def by simp
+
+lemma case_prod_app: "case_prod f x y = case_prod (\<lambda>l r. f l r y) x"
+  by (case_tac x) simp
+
+lemma case_sum_map_sum: "case_sum l r (map_sum f g x) = case_sum (l \<circ> f) (r \<circ> g) x"
+  by (case_tac x) simp+
+
+lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x"
+  by (case_tac x) simp+
+
+lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)"
+  by (simp add: inj_on_def)
+
+lemma eq_ifI: "(P \<longrightarrow> t = u1) \<Longrightarrow> (\<not> P \<longrightarrow> t = u2) \<Longrightarrow> t = (if P then u1 else u2)"
+  by simp
+
+ML_file "Tools/BNF/bnf_fp_util.ML"
+ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
+ML_file "Tools/BNF/bnf_lfp_size.ML"
+ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
+ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML"
+ML_file "Tools/BNF/bnf_fp_n2m.ML"
+ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML"
+
+ML_file "Tools/Function/old_size.ML"
+setup Old_Size.setup
+
+lemma size_bool[code]: "size (b\<Colon>bool) = 0"
+  by (cases b) auto
+
+lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"
+  by (induct n) simp_all
+
+declare prod.size[no_atp]
+
+lemma size_sum_o_map: "size_sum g1 g2 \<circ> map_sum f1 f2 = size_sum (g1 \<circ> f1) (g2 \<circ> f2)"
+  by (rule ext) (case_tac x, auto)
+
+lemma size_prod_o_map: "size_prod g1 g2 \<circ> map_prod f1 f2 = size_prod (g1 \<circ> f1) (g2 \<circ> f2)"
+  by (rule ext) auto
+
+setup {*
+BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size}
+  @{thms size_sum_o_map}
+#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size}
+  @{thms size_prod_o_map}
+*}
+
+end
diff -r b7cab82f488e -r 43a1ba26a8cb src/HOL/BNF_GFP.thy
--- a/src/HOL/BNF_GFP.thy	Mon Sep 01 16:34:39 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,300 +0,0 @@
-(*  Title:      HOL/BNF_GFP.thy
-    Author:     Dmitriy Traytel, TU Muenchen
-    Author:     Lorenz Panny, TU Muenchen
-    Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2012, 2013, 2014
-
-Greatest fixed point operation on bounded natural functors.
-*)
-
-header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
-
-theory BNF_GFP
-imports BNF_FP_Base String
-keywords
-  "codatatype" :: thy_decl and
-  "primcorecursive" :: thy_goal and
-  "primcorec" :: thy_decl
-begin
-
-setup {*
-Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}
-*}
-
-lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-  by simp
-
-lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-  by (cases s) auto
-
-lemma not_TrueE: "\<not> True \<Longrightarrow> P"
-  by (erule notE, rule TrueI)
-
-lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
-  by fast
-
-lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
-  by (auto split: sum.splits)
-
-lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f"
-  apply rule
-   apply (rule ext, force split: sum.split)
-  by (rule ext, metis case_sum_o_inj(2))
-
-lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
-  by fast
-
-lemma equiv_proj:
-  assumes e: "equiv A R" and m: "z \<in> R"
-  shows "(proj R o fst) z = (proj R o snd) z"
-proof -
-  from m have z: "(fst z, snd z) \<in> R" by auto
-  with e have "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R"
-    unfolding equiv_def sym_def trans_def by blast+
-  then show ?thesis unfolding proj_def[abs_def] by auto
-qed
-
-(* Operators: *)
-definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
-
-lemma Id_on_Gr: "Id_on A = Gr A id"
-  unfolding Id_on_def Gr_def by auto
-
-lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
-  unfolding image2_def by auto
-
-lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
-  by auto
-
-lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
-  unfolding image2_def Gr_def by auto
-
-lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
-  unfolding Gr_def by simp
-
-lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
-  unfolding Gr_def by simp
-
-lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
-  unfolding Gr_def by auto
-
-lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
-  by blast
-
-lemma subset_CollectI: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> Q x \<Longrightarrow> P x) \<Longrightarrow> ({x \<in> B. Q x} \<subseteq> {x \<in> A. P x})"
-  by blast
-
-lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X"
-  unfolding fun_eq_iff by auto
-
-lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (split (in_rel Y))"
-  by auto
-
-lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
-  by force
-
-lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
-  unfolding fun_eq_iff by auto
-
-lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)"
-  unfolding fun_eq_iff by auto
-
-lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
-  unfolding Gr_def Grp_def fun_eq_iff by auto
-
-definition relImage where
-  "relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
-
-definition relInvImage where
-  "relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
-
-lemma relImage_Gr:
-  "\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
-  unfolding relImage_def Gr_def relcomp_def by auto
-
-lemma relInvImage_Gr: "\<lbrakk>R \<subseteq> B \<times> B\<rbrakk> \<Longrightarrow> relInvImage A R f = Gr A f O R O (Gr A f)^-1"
-  unfolding Gr_def relcomp_def image_def relInvImage_def by auto
-
-lemma relImage_mono:
-  "R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
-  unfolding relImage_def by auto
-
-lemma relInvImage_mono:
-  "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
-  unfolding relInvImage_def by auto
-
-lemma relInvImage_Id_on:
-  "(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id"
-  unfolding relInvImage_def Id_on_def by auto
-
-lemma relInvImage_UNIV_relImage:
-  "R \<subseteq> relInvImage UNIV (relImage R f) f"
-  unfolding relInvImage_def relImage_def by auto
-
-lemma relImage_proj:
-  assumes "equiv A R"
-  shows "relImage R (proj R) \<subseteq> Id_on (A//R)"
-  unfolding relImage_def Id_on_def
-  using proj_iff[OF assms] equiv_class_eq_iff[OF assms]
-  by (auto simp: proj_preserves)
-
-lemma relImage_relInvImage:
-  assumes "R \<subseteq> f ` A <*> f ` A"
-  shows "relImage (relInvImage A R f) f = R"
-  using assms unfolding relImage_def relInvImage_def by fast
-
-lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
-  by simp
-
-lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z" by simp
-lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z" by simp
-
-lemma fst_diag_fst: "fst o ((\<lambda>x. (x, x)) o fst) = fst" by auto
-lemma snd_diag_fst: "snd o ((\<lambda>x. (x, x)) o fst) = fst" by auto
-lemma fst_diag_snd: "fst o ((\<lambda>x. (x, x)) o snd) = snd" by auto
-lemma snd_diag_snd: "snd o ((\<lambda>x. (x, x)) o snd) = snd" by auto
-
-definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}"
-definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}"
-definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))"
-
-lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
-  unfolding Shift_def Succ_def by simp
-
-lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
-  unfolding Succ_def by simp
-
-lemmas SuccE = SuccD[elim_format]
-
-lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl"
-  unfolding Succ_def by simp
-
-lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl"
-  unfolding Shift_def by simp
-
-lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
-  unfolding Succ_def Shift_def by auto
-
-lemma length_Cons: "length (x # xs) = Suc (length xs)"
-  by simp
-
-lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)"
-  by simp
-
-(*injection into the field of a cardinal*)
-definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r"
-definition "toCard A r \<equiv> SOME f. toCard_pred A r f"
-
-lemma ex_toCard_pred:
-  "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
-  unfolding toCard_pred_def
-  using card_of_ordLeq[of A "Field r"]
-    ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
-  by blast
-
-lemma toCard_pred_toCard:
-  "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)"
-  unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
-
-lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> toCard A r x = toCard A r y \<longleftrightarrow> x = y"
-  using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
-
-definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k"
-
-lemma fromCard_toCard:
-  "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
-  unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
-
-lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
-  unfolding Field_card_of csum_def by auto
-
-lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
-  unfolding Field_card_of csum_def by auto
-
-lemma rec_nat_0_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
-  by auto
-
-lemma rec_nat_Suc_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
-  by auto
-
-lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
-  by auto
-
-lemma rec_list_Cons_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
-  by auto
-
-lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
-  by simp
-
-definition image2p where
-  "image2p f g R = (\<lambda>x y. \<exists>x' y'. R x' y' \<and> f x' = x \<and> g y' = y)"
-
-lemma image2pI: "R x y \<Longrightarrow> image2p f g R (f x) (g y)"
-  unfolding image2p_def by blast
-
-lemma image2pE: "\<lbrakk>image2p f g R fx gy; (\<And>x y. fx = f x \<Longrightarrow> gy = g y \<Longrightarrow> R x y \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"
-  unfolding image2p_def by blast
-
-lemma rel_fun_iff_geq_image2p: "rel_fun R S f g = (image2p f g R \<le> S)"
-  unfolding rel_fun_def image2p_def by auto
-
-lemma rel_fun_image2p: "rel_fun R (image2p f g R) f g"
-  unfolding rel_fun_def image2p_def by auto
-
-
-subsection {* Equivalence relations, quotients, and Hilbert's choice *}
-
-lemma equiv_Eps_in:
-"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (%x. x \<in> X) \<in> X"
-  apply (rule someI2_ex)
-  using in_quotient_imp_non_empty by blast
-
-lemma equiv_Eps_preserves:
-  assumes ECH: "equiv A r" and X: "X \<in> A//r"
-  shows "Eps (%x. x \<in> X) \<in> A"
-  apply (rule in_mono[rule_format])
-   using assms apply (rule in_quotient_imp_subset)
-  by (rule equiv_Eps_in) (rule assms)+
-
-lemma proj_Eps:
-  assumes "equiv A r" and "X \<in> A//r"
-  shows "proj r (Eps (%x. x \<in> X)) = X"
-unfolding proj_def
-proof auto
-  fix x assume x: "x \<in> X"
-  thus "(Eps (%x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
-next
-  fix x assume "(Eps (%x. x \<in> X),x) \<in> r"
-  thus "x \<in> X" using in_quotient_imp_closed[OF assms equiv_Eps_in[OF assms]] by fast
-qed
-
-definition univ where "univ f X == f (Eps (%x. x \<in> X))"
-
-lemma univ_commute:
-assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A"
-shows "(univ f) (proj r x) = f x"
-proof (unfold univ_def)
-  have prj: "proj r x \<in> A//r" using x proj_preserves by fast
-  hence "Eps (%y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
-  moreover have "proj r (Eps (%y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
-  ultimately have "(x, Eps (%y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast
-  thus "f (Eps (%y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce
-qed
-
-lemma univ_preserves:
-  assumes ECH: "equiv A r" and RES: "f respects r" and PRES: "\<forall>x \<in> A. f x \<in> B"
-  shows "\<forall>X \<in> A//r. univ f X \<in> B"
-proof
-  fix X assume "X \<in> A//r"
-  then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
-  hence "univ f X = f x" using ECH RES univ_commute by fastforce
-  thus "univ f X \<in> B" using x PRES by simp
-qed
-
-ML_file "Tools/BNF/bnf_gfp_util.ML"
-ML_file "Tools/BNF/bnf_gfp_tactics.ML"
-ML_file "Tools/BNF/bnf_gfp.ML"
-ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
-ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML"
-
-end
diff -r b7cab82f488e -r 43a1ba26a8cb src/HOL/BNF_Greatest_Fixpoint.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Mon Sep 01 16:34:40 2014 +0200
@@ -0,0 +1,300 @@
+(*  Title:      HOL/BNF_Greatest_Fixpoint.thy
+    Author:     Dmitriy Traytel, TU Muenchen
+    Author:     Lorenz Panny, TU Muenchen
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2012, 2013, 2014
+
+Greatest fixed point operation on bounded natural functors.
+*)
+
+header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
+
+theory BNF_Greatest_Fixpoint
+imports BNF_Fixpoint_Base String
+keywords
+  "codatatype" :: thy_decl and
+  "primcorecursive" :: thy_goal and
+  "primcorec" :: thy_decl
+begin
+
+setup {*
+Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}
+*}
+
+lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+  by simp
+
+lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+  by (cases s) auto
+
+lemma not_TrueE: "\<not> True \<Longrightarrow> P"
+  by (erule notE, rule TrueI)
+
+lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
+  by fast
+
+lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
+  by (auto split: sum.splits)
+
+lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f"
+  apply rule
+   apply (rule ext, force split: sum.split)
+  by (rule ext, metis case_sum_o_inj(2))
+
+lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
+  by fast
+
+lemma equiv_proj:
+  assumes e: "equiv A R" and m: "z \<in> R"
+  shows "(proj R o fst) z = (proj R o snd) z"
+proof -
+  from m have z: "(fst z, snd z) \<in> R" by auto
+  with e have "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R"
+    unfolding equiv_def sym_def trans_def by blast+
+  then show ?thesis unfolding proj_def[abs_def] by auto
+qed
+
+(* Operators: *)
+definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
+
+lemma Id_on_Gr: "Id_on A = Gr A id"
+  unfolding Id_on_def Gr_def by auto
+
+lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
+  unfolding image2_def by auto
+
+lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
+  by auto
+
+lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
+  unfolding image2_def Gr_def by auto
+
+lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
+  unfolding Gr_def by simp
+
+lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
+  unfolding Gr_def by simp
+
+lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
+  unfolding Gr_def by auto
+
+lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
+  by blast
+
+lemma subset_CollectI: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> Q x \<Longrightarrow> P x) \<Longrightarrow> ({x \<in> B. Q x} \<subseteq> {x \<in> A. P x})"
+  by blast
+
+lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X"
+  unfolding fun_eq_iff by auto
+
+lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (split (in_rel Y))"
+  by auto
+
+lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
+  by force
+
+lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
+  unfolding fun_eq_iff by auto
+
+lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)"
+  unfolding fun_eq_iff by auto
+
+lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
+  unfolding Gr_def Grp_def fun_eq_iff by auto
+
+definition relImage where
+  "relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
+
+definition relInvImage where
+  "relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
+
+lemma relImage_Gr:
+  "\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
+  unfolding relImage_def Gr_def relcomp_def by auto
+
+lemma relInvImage_Gr: "\<lbrakk>R \<subseteq> B \<times> B\<rbrakk> \<Longrightarrow> relInvImage A R f = Gr A f O R O (Gr A f)^-1"
+  unfolding Gr_def relcomp_def image_def relInvImage_def by auto
+
+lemma relImage_mono:
+  "R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
+  unfolding relImage_def by auto
+
+lemma relInvImage_mono:
+  "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
+  unfolding relInvImage_def by auto
+
+lemma relInvImage_Id_on:
+  "(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id"
+  unfolding relInvImage_def Id_on_def by auto
+
+lemma relInvImage_UNIV_relImage:
+  "R \<subseteq> relInvImage UNIV (relImage R f) f"
+  unfolding relInvImage_def relImage_def by auto
+
+lemma relImage_proj:
+  assumes "equiv A R"
+  shows "relImage R (proj R) \<subseteq> Id_on (A//R)"
+  unfolding relImage_def Id_on_def
+  using proj_iff[OF assms] equiv_class_eq_iff[OF assms]
+  by (auto simp: proj_preserves)
+
+lemma relImage_relInvImage:
+  assumes "R \<subseteq> f ` A <*> f ` A"
+  shows "relImage (relInvImage A R f) f = R"
+  using assms unfolding relImage_def relInvImage_def by fast
+
+lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
+  by simp
+
+lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z" by simp
+lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z" by simp
+
+lemma fst_diag_fst: "fst o ((\<lambda>x. (x, x)) o fst) = fst" by auto
+lemma snd_diag_fst: "snd o ((\<lambda>x. (x, x)) o fst) = fst" by auto
+lemma fst_diag_snd: "fst o ((\<lambda>x. (x, x)) o snd) = snd" by auto
+lemma snd_diag_snd: "snd o ((\<lambda>x. (x, x)) o snd) = snd" by auto
+
+definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}"
+definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}"
+definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))"
+
+lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
+  unfolding Shift_def Succ_def by simp
+
+lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
+  unfolding Succ_def by simp
+
+lemmas SuccE = SuccD[elim_format]
+
+lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl"
+  unfolding Succ_def by simp
+
+lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl"
+  unfolding Shift_def by simp
+
+lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
+  unfolding Succ_def Shift_def by auto
+
+lemma length_Cons: "length (x # xs) = Suc (length xs)"
+  by simp
+
+lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)"
+  by simp
+
+(*injection into the field of a cardinal*)
+definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r"
+definition "toCard A r \<equiv> SOME f. toCard_pred A r f"
+
+lemma ex_toCard_pred:
+  "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
+  unfolding toCard_pred_def
+  using card_of_ordLeq[of A "Field r"]
+    ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
+  by blast
+
+lemma toCard_pred_toCard:
+  "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)"
+  unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
+
+lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow> toCard A r x = toCard A r y \<longleftrightarrow> x = y"
+  using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
+
+definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k"
+
+lemma fromCard_toCard:
+  "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
+  unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
+
+lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
+  unfolding Field_card_of csum_def by auto
+
+lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
+  unfolding Field_card_of csum_def by auto
+
+lemma rec_nat_0_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
+  by auto
+
+lemma rec_nat_Suc_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
+  by auto
+
+lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
+  by auto
+
+lemma rec_list_Cons_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
+  by auto
+
+lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
+  by simp
+
+definition image2p where
+  "image2p f g R = (\<lambda>x y. \<exists>x' y'. R x' y' \<and> f x' = x \<and> g y' = y)"
+
+lemma image2pI: "R x y \<Longrightarrow> image2p f g R (f x) (g y)"
+  unfolding image2p_def by blast
+
+lemma image2pE: "\<lbrakk>image2p f g R fx gy; (\<And>x y. fx = f x \<Longrightarrow> gy = g y \<Longrightarrow> R x y \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"
+  unfolding image2p_def by blast
+
+lemma rel_fun_iff_geq_image2p: "rel_fun R S f g = (image2p f g R \<le> S)"
+  unfolding rel_fun_def image2p_def by auto
+
+lemma rel_fun_image2p: "rel_fun R (image2p f g R) f g"
+  unfolding rel_fun_def image2p_def by auto
+
+
+subsection {* Equivalence relations, quotients, and Hilbert's choice *}
+
+lemma equiv_Eps_in:
+"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (%x. x \<in> X) \<in> X"
+  apply (rule someI2_ex)
+  using in_quotient_imp_non_empty by blast
+
+lemma equiv_Eps_preserves:
+  assumes ECH: "equiv A r" and X: "X \<in> A//r"
+  shows "Eps (%x. x \<in> X) \<in> A"
+  apply (rule in_mono[rule_format])
+   using assms apply (rule in_quotient_imp_subset)
+  by (rule equiv_Eps_in) (rule assms)+
+
+lemma proj_Eps:
+  assumes "equiv A r" and "X \<in> A//r"
+  shows "proj r (Eps (%x. x \<in> X)) = X"
+unfolding proj_def
+proof auto
+  fix x assume x: "x \<in> X"
+  thus "(Eps (%x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
+next
+  fix x assume "(Eps (%x. x \<in> X),x) \<in> r"
+  thus "x \<in> X" using in_quotient_imp_closed[OF assms equiv_Eps_in[OF assms]] by fast
+qed
+
+definition univ where "univ f X == f (Eps (%x. x \<in> X))"
+
+lemma univ_commute:
+assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A"
+shows "(univ f) (proj r x) = f x"
+proof (unfold univ_def)
+  have prj: "proj r x \<in> A//r" using x proj_preserves by fast
+  hence "Eps (%y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
+  moreover have "proj r (Eps (%y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
+  ultimately have "(x, Eps (%y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast
+  thus "f (Eps (%y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce
+qed
+
+lemma univ_preserves:
+  assumes ECH: "equiv A r" and RES: "f respects r" and PRES: "\<forall>x \<in> A. f x \<in> B"
+  shows "\<forall>X \<in> A//r. univ f X \<in> B"
+proof
+  fix X assume "X \<in> A//r"
+  then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
+  hence "univ f X = f x" using ECH RES univ_commute by fastforce
+  thus "univ f X \<in> B" using x PRES by simp
+qed
+
+ML_file "Tools/BNF/bnf_gfp_util.ML"
+ML_file "Tools/BNF/bnf_gfp_tactics.ML"
+ML_file "Tools/BNF/bnf_gfp.ML"
+ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
+ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML"
+
+end
diff -r b7cab82f488e -r 43a1ba26a8cb src/HOL/BNF_LFP.thy
--- a/src/HOL/BNF_LFP.thy	Mon Sep 01 16:34:39 2014 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,198 +0,0 @@
-(*  Title:      HOL/BNF_LFP.thy
-    Author:     Dmitriy Traytel, TU Muenchen
-    Author:     Lorenz Panny, TU Muenchen
-    Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2012, 2013, 2014
-
-Least fixed point operation on bounded natural functors.
-*)
-
-header {* Least Fixed Point Operation on Bounded Natural Functors *}
-
-theory BNF_LFP
-imports BNF_FP_Base
-keywords
-  "datatype_new" :: thy_decl and
-  "datatype_compat" :: thy_decl
-begin
-
-lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
-  by blast
-
-lemma image_Collect_subsetI: "(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B"
-  by blast
-
-lemma Collect_restrict: "{x. x \<in> X \<and> P x} \<subseteq> X"
-  by auto
-
-lemma prop_restrict: "\<lbrakk>x \<in> Z; Z \<subseteq> {x. x \<in> X \<and> P x}\<rbrakk> \<Longrightarrow> P x"
-  by auto
-
-lemma underS_I: "\<lbrakk>i \<noteq> j; (i, j) \<in> R\<rbrakk> \<Longrightarrow> i \<in> underS R j"
-  unfolding underS_def by simp
-
-lemma underS_E: "i \<in> underS R j \<Longrightarrow> i \<noteq> j \<and> (i, j) \<in> R"
-  unfolding underS_def by simp
-
-lemma underS_Field: "i \<in> underS R j \<Longrightarrow> i \<in> Field R"
-  unfolding underS_def Field_def by auto
-
-lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
-  unfolding Field_def by auto
-
-lemma fst_convol': "fst (\<langle>f, g\<rangle> x) = f x"
-  using fst_convol unfolding convol_def by simp
-
-lemma snd_convol': "snd (\<langle>f, g\<rangle> x) = g x"
-  using snd_convol unfolding convol_def by simp
-
-lemma convol_expand_snd: "fst o f = g \<Longrightarrow> \<langle>g, snd o f\<rangle> = f"
-  unfolding convol_def by auto
-
-lemma convol_expand_snd':
-  assumes "(fst o f = g)"
-  shows "h = snd o f \<longleftrightarrow> \<langle>g, h\<rangle> = f"
-proof -
-  from assms have *: "\<langle>g, snd o f\<rangle> = f" by (rule convol_expand_snd)
-  then have "h = snd o f \<longleftrightarrow> h = snd o \<langle>g, snd o f\<rangle>" by simp
-  moreover have "\<dots> \<longleftrightarrow> h = snd o f" by (simp add: snd_convol)
-  moreover have "\<dots> \<longleftrightarrow> \<langle>g, h\<rangle> = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff)
-  ultimately show ?thesis by simp
-qed
-
-lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
-  unfolding bij_betw_def by auto
-
-lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B"
-  unfolding bij_betw_def by auto
-
-lemma f_the_inv_into_f_bij_betw: "bij_betw f A B \<Longrightarrow>
-  (bij_betw f A B \<Longrightarrow> x \<in> B) \<Longrightarrow> f (the_inv_into A f x) = x"
-  unfolding bij_betw_def by (blast intro: f_the_inv_into_f)
-
-lemma ex_bij_betw: "|A| \<le>o (r :: 'b rel) \<Longrightarrow> \<exists>f B :: 'b set. bij_betw f B A"
-  by (subst (asm) internalize_card_of_ordLeq)
-    (auto dest!: iffD2[OF card_of_ordIso ordIso_symmetric])
-
-lemma bij_betwI':
-  "\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y);
-    \<And>x. x \<in> X \<Longrightarrow> f x \<in> Y;
-    \<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> bij_betw f X Y"
-  unfolding bij_betw_def inj_on_def by blast
-
-lemma surj_fun_eq:
-  assumes surj_on: "f ` X = UNIV" and eq_on: "\<forall>x \<in> X. (g1 o f) x = (g2 o f) x"
-  shows "g1 = g2"
-proof (rule ext)
-  fix y
-  from surj_on obtain x where "x \<in> X" and "y = f x" by blast
-  thus "g1 y = g2 y" using eq_on by simp
-qed
-
-lemma Card_order_wo_rel: "Card_order r \<Longrightarrow> wo_rel r"
-unfolding wo_rel_def card_order_on_def by blast
-
-lemma Cinfinite_limit: "\<lbrakk>x \<in> Field r; Cinfinite r\<rbrakk> \<Longrightarrow>
-  \<exists>y \<in> Field r. x \<noteq> y \<and> (x, y) \<in> r"
-unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit)
-
-lemma Card_order_trans:
-  "\<lbrakk>Card_order r; x \<noteq> y; (x, y) \<in> r; y \<noteq> z; (y, z) \<in> r\<rbrakk> \<Longrightarrow> x \<noteq> z \<and> (x, z) \<in> r"
-unfolding card_order_on_def well_order_on_def linear_order_on_def
-  partial_order_on_def preorder_on_def trans_def antisym_def by blast
-
-lemma Cinfinite_limit2:
- assumes x1: "x1 \<in> Field r" and x2: "x2 \<in> Field r" and r: "Cinfinite r"
- shows "\<exists>y \<in> Field r. (x1 \<noteq> y \<and> (x1, y) \<in> r) \<and> (x2 \<noteq> y \<and> (x2, y) \<in> r)"
-proof -
-  from r have trans: "trans r" and total: "Total r" and antisym: "antisym r"
-    unfolding card_order_on_def well_order_on_def linear_order_on_def
-      partial_order_on_def preorder_on_def by auto
-  obtain y1 where y1: "y1 \<in> Field r" "x1 \<noteq> y1" "(x1, y1) \<in> r"
-    using Cinfinite_limit[OF x1 r] by blast
-  obtain y2 where y2: "y2 \<in> Field r" "x2 \<noteq> y2" "(x2, y2) \<in> r"
-    using Cinfinite_limit[OF x2 r] by blast
-  show ?thesis
-  proof (cases "y1 = y2")
-    case True with y1 y2 show ?thesis by blast
-  next
-    case False
-    with y1(1) y2(1) total have "(y1, y2) \<in> r \<or> (y2, y1) \<in> r"
-      unfolding total_on_def by auto
-    thus ?thesis
-    proof
-      assume *: "(y1, y2) \<in> r"
-      with trans y1(3) have "(x1, y2) \<in> r" unfolding trans_def by blast
-      with False y1 y2 * antisym show ?thesis by (cases "x1 = y2") (auto simp: antisym_def)
-    next
-      assume *: "(y2, y1) \<in> r"
-      with trans y2(3) have "(x2, y1) \<in> r" unfolding trans_def by blast
-      with False y1 y2 * antisym show ?thesis by (cases "x2 = y1") (auto simp: antisym_def)
-    qed
-  qed
-qed
-
-lemma Cinfinite_limit_finite: "\<lbrakk>finite X; X \<subseteq> Field r; Cinfinite r\<rbrakk>
- \<Longrightarrow> \<exists>y \<in> Field r. \<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)"
-proof (induct X rule: finite_induct)
-  case empty thus ?case unfolding cinfinite_def using ex_in_conv[of "Field r"] finite.emptyI by auto
-next
-  case (insert x X)
-  then obtain y where y: "y \<in> Field r" "\<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)" by blast
-  then obtain z where z: "z \<in> Field r" "x \<noteq> z \<and> (x, z) \<in> r" "y \<noteq> z \<and> (y, z) \<in> r"
-    using Cinfinite_limit2[OF _ y(1) insert(5), of x] insert(4) by blast
-  show ?case
-    apply (intro bexI ballI)
-    apply (erule insertE)
-    apply hypsubst
-    apply (rule z(2))
-    using Card_order_trans[OF insert(5)[THEN conjunct2]] y(2) z(3)
-    apply blast
-    apply (rule z(1))
-    done
-qed
-
-lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A"
-by auto
-
-(*helps resolution*)
-lemma well_order_induct_imp:
-  "wo_rel r \<Longrightarrow> (\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> y \<in> Field r \<longrightarrow> P y \<Longrightarrow> x \<in> Field r \<longrightarrow> P x) \<Longrightarrow>
-     x \<in> Field r \<longrightarrow> P x"
-by (erule wo_rel.well_order_induct)
-
-lemma meta_spec2:
-  assumes "(\<And>x y. PROP P x y)"
-  shows "PROP P x y"
-by (rule assms)
-
-lemma nchotomy_relcomppE:
-  assumes "\<And>y. \<exists>x. y = f x" "(r OO s) a c" "\<And>b. r a (f b) \<Longrightarrow> s (f b) c \<Longrightarrow> P"
-  shows P
-proof (rule relcompp.cases[OF assms(2)], hypsubst)
-  fix b assume "r a b" "s b c"
-  moreover from assms(1) obtain b' where "b = f b'" by blast
-  ultimately show P by (blast intro: assms(3))
-qed
-
-lemma vimage2p_rel_fun: "rel_fun (vimage2p f g R) R f g"
-  unfolding rel_fun_def vimage2p_def by auto
-
-lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
-  unfolding vimage2p_def by auto
-
-lemma id_transfer: "rel_fun A A id id"
-  unfolding rel_fun_def by simp
-
-lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
-  by (rule ssubst)
-
-ML_file "Tools/BNF/bnf_lfp_util.ML"
-ML_file "Tools/BNF/bnf_lfp_tactics.ML"
-ML_file "Tools/BNF/bnf_lfp.ML"
-ML_file "Tools/BNF/bnf_lfp_compat.ML"
-ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
-
-hide_fact (open) id_transfer
-
-end
diff -r b7cab82f488e -r 43a1ba26a8cb src/HOL/BNF_Least_Fixpoint.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF_Least_Fixpoint.thy	Mon Sep 01 16:34:40 2014 +0200
@@ -0,0 +1,198 @@
+(*  Title:      HOL/BNF_Least_Fixpoint.thy
+    Author:     Dmitriy Traytel, TU Muenchen
+    Author:     Lorenz Panny, TU Muenchen
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2012, 2013, 2014
+
+Least fixed point operation on bounded natural functors.
+*)
+
+header {* Least Fixed Point Operation on Bounded Natural Functors *}
+
+theory BNF_Least_Fixpoint
+imports BNF_Fixpoint_Base
+keywords
+  "datatype_new" :: thy_decl and
+  "datatype_compat" :: thy_decl
+begin
+
+lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
+  by blast
+
+lemma image_Collect_subsetI: "(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B"
+  by blast
+
+lemma Collect_restrict: "{x. x \<in> X \<and> P x} \<subseteq> X"
+  by auto
+
+lemma prop_restrict: "\<lbrakk>x \<in> Z; Z \<subseteq> {x. x \<in> X \<and> P x}\<rbrakk> \<Longrightarrow> P x"
+  by auto
+
+lemma underS_I: "\<lbrakk>i \<noteq> j; (i, j) \<in> R\<rbrakk> \<Longrightarrow> i \<in> underS R j"
+  unfolding underS_def by simp
+
+lemma underS_E: "i \<in> underS R j \<Longrightarrow> i \<noteq> j \<and> (i, j) \<in> R"
+  unfolding underS_def by simp
+
+lemma underS_Field: "i \<in> underS R j \<Longrightarrow> i \<in> Field R"
+  unfolding underS_def Field_def by auto
+
+lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
+  unfolding Field_def by auto
+
+lemma fst_convol': "fst (\<langle>f, g\<rangle> x) = f x"
+  using fst_convol unfolding convol_def by simp
+
+lemma snd_convol': "snd (\<langle>f, g\<rangle> x) = g x"
+  using snd_convol unfolding convol_def by simp
+
+lemma convol_expand_snd: "fst o f = g \<Longrightarrow> \<langle>g, snd o f\<rangle> = f"
+  unfolding convol_def by auto
+
+lemma convol_expand_snd':
+  assumes "(fst o f = g)"
+  shows "h = snd o f \<longleftrightarrow> \<langle>g, h\<rangle> = f"
+proof -
+  from assms have *: "\<langle>g, snd o f\<rangle> = f" by (rule convol_expand_snd)
+  then have "h = snd o f \<longleftrightarrow> h = snd o \<langle>g, snd o f\<rangle>" by simp
+  moreover have "\<dots> \<longleftrightarrow> h = snd o f" by (simp add: snd_convol)
+  moreover have "\<dots> \<longleftrightarrow> \<langle>g, h\<rangle> = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff)
+  ultimately show ?thesis by simp
+qed
+
+lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
+  unfolding bij_betw_def by auto
+
+lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B"
+  unfolding bij_betw_def by auto
+
+lemma f_the_inv_into_f_bij_betw: "bij_betw f A B \<Longrightarrow>
+  (bij_betw f A B \<Longrightarrow> x \<in> B) \<Longrightarrow> f (the_inv_into A f x) = x"
+  unfolding bij_betw_def by (blast intro: f_the_inv_into_f)
+
+lemma ex_bij_betw: "|A| \<le>o (r :: 'b rel) \<Longrightarrow> \<exists>f B :: 'b set. bij_betw f B A"
+  by (subst (asm) internalize_card_of_ordLeq)
+    (auto dest!: iffD2[OF card_of_ordIso ordIso_symmetric])
+
+lemma bij_betwI':
+  "\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y);
+    \<And>x. x \<in> X \<Longrightarrow> f x \<in> Y;
+    \<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> bij_betw f X Y"
+  unfolding bij_betw_def inj_on_def by blast
+
+lemma surj_fun_eq:
+  assumes surj_on: "f ` X = UNIV" and eq_on: "\<forall>x \<in> X. (g1 o f) x = (g2 o f) x"
+  shows "g1 = g2"
+proof (rule ext)
+  fix y
+  from surj_on obtain x where "x \<in> X" and "y = f x" by blast
+  thus "g1 y = g2 y" using eq_on by simp
+qed
+
+lemma Card_order_wo_rel: "Card_order r \<Longrightarrow> wo_rel r"
+unfolding wo_rel_def card_order_on_def by blast
+
+lemma Cinfinite_limit: "\<lbrakk>x \<in> Field r; Cinfinite r\<rbrakk> \<Longrightarrow>
+  \<exists>y \<in> Field r. x \<noteq> y \<and> (x, y) \<in> r"
+unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit)
+
+lemma Card_order_trans:
+  "\<lbrakk>Card_order r; x \<noteq> y; (x, y) \<in> r; y \<noteq> z; (y, z) \<in> r\<rbrakk> \<Longrightarrow> x \<noteq> z \<and> (x, z) \<in> r"
+unfolding card_order_on_def well_order_on_def linear_order_on_def
+  partial_order_on_def preorder_on_def trans_def antisym_def by blast
+
+lemma Cinfinite_limit2:
+ assumes x1: "x1 \<in> Field r" and x2: "x2 \<in> Field r" and r: "Cinfinite r"
+ shows "\<exists>y \<in> Field r. (x1 \<noteq> y \<and> (x1, y) \<in> r) \<and> (x2 \<noteq> y \<and> (x2, y) \<in> r)"
+proof -
+  from r have trans: "trans r" and total: "Total r" and antisym: "antisym r"
+    unfolding card_order_on_def well_order_on_def linear_order_on_def
+      partial_order_on_def preorder_on_def by auto
+  obtain y1 where y1: "y1 \<in> Field r" "x1 \<noteq> y1" "(x1, y1) \<in> r"
+    using Cinfinite_limit[OF x1 r] by blast
+  obtain y2 where y2: "y2 \<in> Field r" "x2 \<noteq> y2" "(x2, y2) \<in> r"
+    using Cinfinite_limit[OF x2 r] by blast
+  show ?thesis
+  proof (cases "y1 = y2")
+    case True with y1 y2 show ?thesis by blast
+  next
+    case False
+    with y1(1) y2(1) total have "(y1, y2) \<in> r \<or> (y2, y1) \<in> r"
+      unfolding total_on_def by auto
+    thus ?thesis
+    proof
+      assume *: "(y1, y2) \<in> r"
+      with trans y1(3) have "(x1, y2) \<in> r" unfolding trans_def by blast
+      with False y1 y2 * antisym show ?thesis by (cases "x1 = y2") (auto simp: antisym_def)
+    next
+      assume *: "(y2, y1) \<in> r"
+      with trans y2(3) have "(x2, y1) \<in> r" unfolding trans_def by blast
+      with False y1 y2 * antisym show ?thesis by (cases "x2 = y1") (auto simp: antisym_def)
+    qed
+  qed
+qed
+
+lemma Cinfinite_limit_finite: "\<lbrakk>finite X; X \<subseteq> Field r; Cinfinite r\<rbrakk>
+ \<Longrightarrow> \<exists>y \<in> Field r. \<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)"
+proof (induct X rule: finite_induct)
+  case empty thus ?case unfolding cinfinite_def using ex_in_conv[of "Field r"] finite.emptyI by auto
+next
+  case (insert x X)
+  then obtain y where y: "y \<in> Field r" "\<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)" by blast
+  then obtain z where z: "z \<in> Field r" "x \<noteq> z \<and> (x, z) \<in> r" "y \<noteq> z \<and> (y, z) \<in> r"
+    using Cinfinite_limit2[OF _ y(1) insert(5), of x] insert(4) by blast
+  show ?case
+    apply (intro bexI ballI)
+    apply (erule insertE)
+    apply hypsubst
+    apply (rule z(2))
+    using Card_order_trans[OF insert(5)[THEN conjunct2]] y(2) z(3)
+    apply blast
+    apply (rule z(1))
+    done
+qed
+
+lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A"
+by auto
+
+(*helps resolution*)
+lemma well_order_induct_imp:
+  "wo_rel r \<Longrightarrow> (\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> y \<in> Field r \<longrightarrow> P y \<Longrightarrow> x \<in> Field r \<longrightarrow> P x) \<Longrightarrow>
+     x \<in> Field r \<longrightarrow> P x"
+by (erule wo_rel.well_order_induct)
+
+lemma meta_spec2:
+  assumes "(\<And>x y. PROP P x y)"
+  shows "PROP P x y"
+by (rule assms)
+
+lemma nchotomy_relcomppE:
+  assumes "\<And>y. \<exists>x. y = f x" "(r OO s) a c" "\<And>b. r a (f b) \<Longrightarrow> s (f b) c \<Longrightarrow> P"
+  shows P
+proof (rule relcompp.cases[OF assms(2)], hypsubst)
+  fix b assume "r a b" "s b c"
+  moreover from assms(1) obtain b' where "b = f b'" by blast
+  ultimately show P by (blast intro: assms(3))
+qed
+
+lemma vimage2p_rel_fun: "rel_fun (vimage2p f g R) R f g"
+  unfolding rel_fun_def vimage2p_def by auto
+
+lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
+  unfolding vimage2p_def by auto
+
+lemma id_transfer: "rel_fun A A id id"
+  unfolding rel_fun_def by simp
+
+lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
+  by (rule ssubst)
+
+ML_file "Tools/BNF/bnf_lfp_util.ML"
+ML_file "Tools/BNF/bnf_lfp_tactics.ML"
+ML_file "Tools/BNF/bnf_lfp.ML"
+ML_file "Tools/BNF/bnf_lfp_compat.ML"
+ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
+
+hide_fact (open) id_transfer
+
+end
diff -r b7cab82f488e -r 43a1ba26a8cb src/HOL/Main.thy
--- a/src/HOL/Main.thy	Mon Sep 01 16:34:39 2014 +0200
+++ b/src/HOL/Main.thy	Mon Sep 01 16:34:40 2014 +0200
@@ -1,7 +1,8 @@
 header {* Main HOL *}
 
 theory Main
-imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick BNF_GFP
+imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick
+  BNF_Greatest_Fixpoint
 begin
 
 text {*
diff -r b7cab82f488e -r 43a1ba26a8cb src/HOL/Num.thy
--- a/src/HOL/Num.thy	Mon Sep 01 16:34:39 2014 +0200
+++ b/src/HOL/Num.thy	Mon Sep 01 16:34:40 2014 +0200
@@ -6,7 +6,7 @@
 header {* Binary Numerals *}
 
 theory Num
-imports Old_Datatype BNF_LFP
+imports BNF_Least_Fixpoint Old_Datatype
 begin
 
 subsection {* The @{text num} type *}
diff -r b7cab82f488e -r 43a1ba26a8cb src/HOL/Option.thy
--- a/src/HOL/Option.thy	Mon Sep 01 16:34:39 2014 +0200
+++ b/src/HOL/Option.thy	Mon Sep 01 16:34:40 2014 +0200
@@ -5,7 +5,7 @@
 header {* Datatype option *}
 
 theory Option
-imports BNF_LFP Old_Datatype Finite_Set
+imports BNF_Least_Fixpoint Old_Datatype Finite_Set
 begin
 
 datatype_new 'a option =
diff -r b7cab82f488e -r 43a1ba26a8cb src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Mon Sep 01 16:34:39 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Mon Sep 01 16:34:40 2014 +0200
@@ -54,8 +54,8 @@
 open BNF_Tactics
 open BNF_Comp_Tactics
 
-val ID_bnf = the (bnf_of @{context} "BNF_Comp.ID");
-val DEADID_bnf = the (bnf_of @{context} "BNF_Comp.DEADID");
+val ID_bnf = the (bnf_of @{context} "BNF_Composition.ID");
+val DEADID_bnf = the (bnf_of @{context} "BNF_Composition.DEADID");
 
 type comp_cache = (bnf * (typ list * typ list)) Typtab.table;
 
diff -r b7cab82f488e -r 43a1ba26a8cb src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Sep 01 16:34:39 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Sep 01 16:34:40 2014 +0200
@@ -289,9 +289,9 @@
           REPEAT_DETERM o etac conjE))) 1 THEN
       unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ sels @ simp_thms') THEN
       unfold_thms_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject ::
-        abs_inject :: ctor_defs @ nesting_rel_eqs @ simp_thms' @ @{thms BNF_Comp.id_bnf_comp_def
-        rel_sum_simps rel_prod_apply vimage2p_def Inl_Inr_False iffD2[OF eq_False Inr_not_Inl]
-        sum.inject prod.inject}) THEN
+        abs_inject :: ctor_defs @ nesting_rel_eqs @ simp_thms' @
+        @{thms BNF_Composition.id_bnf_comp_def rel_sum_simps rel_prod_apply vimage2p_def
+        Inl_Inr_False iffD2[OF eq_False Inr_not_Inl] sum.inject prod.inject}) THEN
       REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac conjE) THEN' (REPEAT_DETERM o rtac conjI) THEN'
         (rtac refl ORELSE' atac))))
     cts assms exhausts discss selss ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs
@@ -305,7 +305,7 @@
           (rtac (cterm_instantiate_pos (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2)
             THEN' atac THEN' atac THEN' TRY o resolve_tac assms))) THEN
         unfold_thms_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
-          @{thms BNF_Comp.id_bnf_comp_def vimage2p_def}) THEN
+          @{thms BNF_Composition.id_bnf_comp_def vimage2p_def}) THEN
         TRYALL (hyp_subst_tac ctxt) THEN
         unfold_thms_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
           Inr_Inl_False  sum.inject prod.inject}) THEN
@@ -354,7 +354,7 @@
     Abs_pre_inverses =
   let
     val assms_ctor_defs =
-      map (unfold_thms ctxt (@{thm BNF_Comp.id_bnf_comp_def} :: ctor_defs)) assms;
+      map (unfold_thms ctxt (@{thm BNF_Composition.id_bnf_comp_def} :: ctor_defs)) assms;
     val exhausts' = map (fn thm => thm RS @{thm asm_rl[of "P x y" for P x y]}) exhausts
       |> map2 (fn ct => cterm_instantiate_pos [NONE, SOME ct]) cts;
   in
@@ -364,7 +364,7 @@
          cterm_instantiate_pos (replicate 4 NONE @ [SOME ct]) @{thm arg_cong2} RS iffD2) cts)
         THEN' atac THEN' hyp_subst_tac ctxt)) THEN
     unfold_thms_tac ctxt (Abs_pre_inverses @ dtor_ctors @ set_pre_defs @ ctor_defs @
-      @{thms BNF_Comp.id_bnf_comp_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert
+      @{thms BNF_Composition.id_bnf_comp_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert
         Un_empty_left Un_empty_right empty_iff singleton_iff}) THEN
     REPEAT_DETERM (HEADGOAL
       (TRY o etac UnE THEN' TRY o etac @{thm singletonE} THEN' TRY o hyp_subst_tac ctxt THEN'
diff -r b7cab82f488e -r 43a1ba26a8cb src/HOL/Tools/BNF/bnf_lfp_size.ML
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Sep 01 16:34:39 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Sep 01 16:34:40 2014 +0200
@@ -65,7 +65,7 @@
 
 val rec_o_map_simp_thms =
   @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum case_prod_map_prod
-      BNF_Comp.id_bnf_comp_def};
+      BNF_Composition.id_bnf_comp_def};
 
 fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
     ctor_rec_o_map =
diff -r b7cab82f488e -r 43a1ba26a8cb src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Mon Sep 01 16:34:39 2014 +0200
+++ b/src/HOL/Transfer.thy	Mon Sep 01 16:34:40 2014 +0200
@@ -6,7 +6,7 @@
 header {* Generic theorem transfer using relations *}
 
 theory Transfer
-imports Hilbert_Choice BNF_FP_Base Metis Option
+imports Hilbert_Choice Metis Option
 begin
 
 (* We include Option here although it's not needed here.