--- 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
--- /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
--- 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
--- /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
--- 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
--- /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
--- 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
--- /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
--- 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 {*
--- 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 *}
--- 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 =
--- 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;
--- 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'
--- 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 =
--- 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.