# HG changeset patch
# User blanchet
# Date 1377859419 -7200
# Node ID 802ae7dae691bdca2c3944d1681d13f71c39bf11
# Parent  8af01463b2d3adf47801387fe49e8d8e2a2cc6e8
tuned theory name

diff -r 8af01463b2d3 -r 802ae7dae691 src/HOL/BNF/BNF_FP_Base.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/BNF/BNF_FP_Base.thy	Fri Aug 30 12:43:39 2013 +0200
@@ -0,0 +1,184 @@
+(*  Title:      HOL/BNF/BNF_FP_Base.thy
+    Author:     Lorenz Panny, TU Muenchen
+    Author:     Dmitriy Traytel, TU Muenchen
+    Author:     Jasmin Blanchette, TU Muenchen
+    Copyright   2012, 2013
+
+Shared fixed point operations on bounded natural functors, including
+*)
+
+header {* Shared Fixed Point Operations on Bounded Natural Functors *}
+
+theory BNF_FP_Base
+imports BNF_Comp BNF_Ctr_Sugar
+keywords
+  "defaults"
+begin
+
+lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
+by auto
+
+lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
+by blast
+
+lemma unit_case_Unity: "(case u of () => f) = f"
+by (cases u) (hypsubst, rule unit.cases)
+
+lemma prod_case_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 prod_all_impI: "(\<And>x y. P (x, y) \<Longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
+by clarify
+
+lemma prod_all_impI_step: "(\<And>x. \<forall>y. P (x, y) \<longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
+by auto
+
+lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
+unfolding o_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 sum_case_step:
+"sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p"
+"sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p"
+by auto
+
+lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+by simp
+
+lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
+by blast
+
+lemma obj_sumE_f:
+"\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f x \<longrightarrow> P"
+by (rule allI) (metis sumE)
+
+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 sum_case_if:
+"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
+by simp
+
+lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
+by blast
+
+lemma UN_compreh_eq_eq:
+"\<Union>{y. \<exists>x\<in>A. y = {}} = {}"
+"\<Union>{y. \<exists>x\<in>A. y = {x}} = A"
+by blast+
+
+lemma Inl_Inr_False: "(Inl x = Inr y) = False"
+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 prod_rel_simp:
+"prod_rel P Q (x, y) (x', y') \<longleftrightarrow> P x x' \<and> Q y y'"
+unfolding prod_rel_def by simp
+
+lemma sum_rel_simps:
+"sum_rel P Q (Inl x) (Inl x') \<longleftrightarrow> P x x'"
+"sum_rel P Q (Inr y) (Inr y') \<longleftrightarrow> Q y y'"
+"sum_rel P Q (Inl x) (Inr y') \<longleftrightarrow> False"
+"sum_rel P Q (Inr y) (Inl x') \<longleftrightarrow> False"
+unfolding sum_rel_def by simp+
+
+lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
+by blast
+
+lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r"
+  unfolding o_def fun_eq_iff by auto
+
+lemma rewriteR_comp_comp2: "\<lbrakk>g o h = r1 o r2; f o r1 = l\<rbrakk> \<Longrightarrow> f o g o h = l o r2"
+  unfolding o_def fun_eq_iff by auto
+
+lemma rewriteL_comp_comp: "\<lbrakk>f o g = l\<rbrakk> \<Longrightarrow> f o (g o h) = l o h"
+  unfolding o_def fun_eq_iff by auto
+
+lemma rewriteL_comp_comp2: "\<lbrakk>f o g = l1 o l2; l2 o h = r\<rbrakk> \<Longrightarrow> f o (g o h) = l1 o r"
+  unfolding o_def fun_eq_iff by auto
+
+lemma convol_o: "<f, g> o h = <f o h, g o h>"
+  unfolding convol_def by auto
+
+lemma map_pair_o_convol: "map_pair h1 h2 o <f, g> = <h1 o f, h2 o g>"
+  unfolding convol_def by auto
+
+lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x"
+  unfolding map_pair_o_convol id_o o_id ..
+
+lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)"
+  unfolding o_def by (auto split: sum.splits)
+
+lemma sum_case_o_sum_map: "sum_case f g o sum_map h1 h2 = sum_case (f o h1) (g o h2)"
+  unfolding o_def by (auto split: sum.splits)
+
+lemma sum_case_o_sum_map_id: "(sum_case id g o sum_map f id) x = sum_case (f o id) g x"
+  unfolding sum_case_o_sum_map id_o o_id ..
+
+lemma fun_rel_def_butlast:
+  "(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
+  unfolding fun_rel_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 if_if_True:
+  "(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) =
+   (if b then x else if b' then x' else f y')"
+  by simp
+
+lemma if_if_False:
+  "(if (if b then False else b') then (if b then x else x') else f (if b then y else y')) =
+   (if b then f y else if b' then x' else f y')"
+  by simp
+
+ML_file "Tools/bnf_fp_util.ML"
+ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
+ML_file "Tools/bnf_fp_def_sugar.ML"
+ML_file "Tools/bnf_fp_n2m_tactics.ML"
+ML_file "Tools/bnf_fp_n2m.ML"
+ML_file "Tools/bnf_fp_n2m_sugar.ML"
+ML_file "Tools/bnf_fp_rec_sugar_util.ML"
+ML_file "Tools/bnf_fp_rec_sugar_tactics.ML"
+ML_file "Tools/bnf_fp_rec_sugar.ML"
+
+end
diff -r 8af01463b2d3 -r 802ae7dae691 src/HOL/BNF/BNF_FP_Basic.thy
--- a/src/HOL/BNF/BNF_FP_Basic.thy	Fri Aug 30 12:37:03 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,183 +0,0 @@
-(*  Title:      HOL/BNF/BNF_FP_Basic.thy
-    Author:     Dmitriy Traytel, TU Muenchen
-    Author:     Jasmin Blanchette, TU Muenchen
-    Copyright   2012
-
-Basic fixed point operations on bounded natural functors.
-*)
-
-header {* Basic Fixed Point Operations on Bounded Natural Functors *}
-
-theory BNF_FP_Basic
-imports BNF_Comp BNF_Ctr_Sugar
-keywords
-  "defaults"
-begin
-
-lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
-by auto
-
-lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
-by blast
-
-lemma unit_case_Unity: "(case u of () => f) = f"
-by (cases u) (hypsubst, rule unit.cases)
-
-lemma prod_case_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 prod_all_impI: "(\<And>x y. P (x, y) \<Longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
-by clarify
-
-lemma prod_all_impI_step: "(\<And>x. \<forall>y. P (x, y) \<longrightarrow> Q (x, y)) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
-by auto
-
-lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
-unfolding o_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 sum_case_step:
-"sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p"
-"sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p"
-by auto
-
-lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-by simp
-
-lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
-by blast
-
-lemma obj_sumE_f:
-"\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f x \<longrightarrow> P"
-by (rule allI) (metis sumE)
-
-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 sum_case_if:
-"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
-by simp
-
-lemma mem_UN_compreh_eq: "(z : \<Union>{y. \<exists>x\<in>A. y = F x}) = (\<exists>x\<in>A. z : F x)"
-by blast
-
-lemma UN_compreh_eq_eq:
-"\<Union>{y. \<exists>x\<in>A. y = {}} = {}"
-"\<Union>{y. \<exists>x\<in>A. y = {x}} = A"
-by blast+
-
-lemma Inl_Inr_False: "(Inl x = Inr y) = False"
-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 prod_rel_simp:
-"prod_rel P Q (x, y) (x', y') \<longleftrightarrow> P x x' \<and> Q y y'"
-unfolding prod_rel_def by simp
-
-lemma sum_rel_simps:
-"sum_rel P Q (Inl x) (Inl x') \<longleftrightarrow> P x x'"
-"sum_rel P Q (Inr y) (Inr y') \<longleftrightarrow> Q y y'"
-"sum_rel P Q (Inl x) (Inr y') \<longleftrightarrow> False"
-"sum_rel P Q (Inr y) (Inl x') \<longleftrightarrow> False"
-unfolding sum_rel_def by simp+
-
-lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
-by blast
-
-lemma rewriteR_comp_comp: "\<lbrakk>g o h = r\<rbrakk> \<Longrightarrow> f o g o h = f o r"
-  unfolding o_def fun_eq_iff by auto
-
-lemma rewriteR_comp_comp2: "\<lbrakk>g o h = r1 o r2; f o r1 = l\<rbrakk> \<Longrightarrow> f o g o h = l o r2"
-  unfolding o_def fun_eq_iff by auto
-
-lemma rewriteL_comp_comp: "\<lbrakk>f o g = l\<rbrakk> \<Longrightarrow> f o (g o h) = l o h"
-  unfolding o_def fun_eq_iff by auto
-
-lemma rewriteL_comp_comp2: "\<lbrakk>f o g = l1 o l2; l2 o h = r\<rbrakk> \<Longrightarrow> f o (g o h) = l1 o r"
-  unfolding o_def fun_eq_iff by auto
-
-lemma convol_o: "<f, g> o h = <f o h, g o h>"
-  unfolding convol_def by auto
-
-lemma map_pair_o_convol: "map_pair h1 h2 o <f, g> = <h1 o f, h2 o g>"
-  unfolding convol_def by auto
-
-lemma map_pair_o_convol_id: "(map_pair f id \<circ> <id , g>) x = <id \<circ> f , g> x"
-  unfolding map_pair_o_convol id_o o_id ..
-
-lemma o_sum_case: "h o sum_case f g = sum_case (h o f) (h o g)"
-  unfolding o_def by (auto split: sum.splits)
-
-lemma sum_case_o_sum_map: "sum_case f g o sum_map h1 h2 = sum_case (f o h1) (g o h2)"
-  unfolding o_def by (auto split: sum.splits)
-
-lemma sum_case_o_sum_map_id: "(sum_case id g o sum_map f id) x = sum_case (f o id) g x"
-  unfolding sum_case_o_sum_map id_o o_id ..
-
-lemma fun_rel_def_butlast:
-  "(fun_rel R (fun_rel S T)) f g = (\<forall>x y. R x y \<longrightarrow> (fun_rel S T) (f x) (g y))"
-  unfolding fun_rel_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 if_if_True:
-  "(if (if b then True else b') then (if b then x else x') else f (if b then y else y')) =
-   (if b then x else if b' then x' else f y')"
-  by simp
-
-lemma if_if_False:
-  "(if (if b then False else b') then (if b then x else x') else f (if b then y else y')) =
-   (if b then f y else if b' then x' else f y')"
-  by simp
-
-ML_file "Tools/bnf_fp_util.ML"
-ML_file "Tools/bnf_fp_def_sugar_tactics.ML"
-ML_file "Tools/bnf_fp_def_sugar.ML"
-ML_file "Tools/bnf_fp_n2m_tactics.ML"
-ML_file "Tools/bnf_fp_n2m.ML"
-ML_file "Tools/bnf_fp_n2m_sugar.ML"
-ML_file "Tools/bnf_fp_rec_sugar_util.ML"
-ML_file "Tools/bnf_fp_rec_sugar_tactics.ML"
-ML_file "Tools/bnf_fp_rec_sugar.ML"
-
-end
diff -r 8af01463b2d3 -r 802ae7dae691 src/HOL/BNF/BNF_GFP.thy
--- a/src/HOL/BNF/BNF_GFP.thy	Fri Aug 30 12:37:03 2013 +0200
+++ b/src/HOL/BNF/BNF_GFP.thy	Fri Aug 30 12:43:39 2013 +0200
@@ -8,7 +8,7 @@
 header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
 
 theory BNF_GFP
-imports BNF_FP_Basic Equiv_Relations_More "~~/src/HOL/Library/Sublist"
+imports BNF_FP_Base Equiv_Relations_More "~~/src/HOL/Library/Sublist"
 keywords
   "codatatype" :: thy_decl and
   "primcorec" :: thy_goal and
diff -r 8af01463b2d3 -r 802ae7dae691 src/HOL/BNF/BNF_LFP.thy
--- a/src/HOL/BNF/BNF_LFP.thy	Fri Aug 30 12:37:03 2013 +0200
+++ b/src/HOL/BNF/BNF_LFP.thy	Fri Aug 30 12:43:39 2013 +0200
@@ -10,7 +10,7 @@
 header {* Least Fixed Point Operation on Bounded Natural Functors *}
 
 theory BNF_LFP
-imports BNF_FP_Basic
+imports BNF_FP_Base
 keywords
   "datatype_new" :: thy_decl and
   "datatype_new_compat" :: thy_decl and