renamed BNF theories
authorblanchet
Mon Sep 01 16:34:40 2014 +0200 (2014-09-01)
changeset 5812843a1ba26a8cb
parent 58127 b7cab82f488e
child 58129 3ec65a7f2b50
renamed BNF theories
src/HOL/BNF_Comp.thy
src/HOL/BNF_Composition.thy
src/HOL/BNF_FP_Base.thy
src/HOL/BNF_Fixpoint_Base.thy
src/HOL/BNF_GFP.thy
src/HOL/BNF_Greatest_Fixpoint.thy
src/HOL/BNF_LFP.thy
src/HOL/BNF_Least_Fixpoint.thy
src/HOL/Main.thy
src/HOL/Num.thy
src/HOL/Option.thy
src/HOL/Tools/BNF/bnf_comp.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
src/HOL/Tools/BNF/bnf_lfp_size.ML
src/HOL/Transfer.thy
     1.1 --- a/src/HOL/BNF_Comp.thy	Mon Sep 01 16:34:39 2014 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,174 +0,0 @@
     1.4 -(*  Title:      HOL/BNF_Comp.thy
     1.5 -    Author:     Dmitriy Traytel, TU Muenchen
     1.6 -    Author:     Jasmin Blanchette, TU Muenchen
     1.7 -    Copyright   2012, 2013, 2014
     1.8 -
     1.9 -Composition of bounded natural functors.
    1.10 -*)
    1.11 -
    1.12 -header {* Composition of Bounded Natural Functors *}
    1.13 -
    1.14 -theory BNF_Comp
    1.15 -imports BNF_Def
    1.16 -begin
    1.17 -
    1.18 -lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})"
    1.19 -by (rule ext) simp
    1.20 -
    1.21 -lemma Union_natural: "Union o image (image f) = image f o Union"
    1.22 -by (rule ext) (auto simp only: comp_apply)
    1.23 -
    1.24 -lemma in_Union_o_assoc: "x \<in> (Union o gset o gmap) A \<Longrightarrow> x \<in> (Union o (gset o gmap)) A"
    1.25 -by (unfold comp_assoc)
    1.26 -
    1.27 -lemma comp_single_set_bd:
    1.28 -  assumes fbd_Card_order: "Card_order fbd" and
    1.29 -    fset_bd: "\<And>x. |fset x| \<le>o fbd" and
    1.30 -    gset_bd: "\<And>x. |gset x| \<le>o gbd"
    1.31 -  shows "|\<Union>(fset ` gset x)| \<le>o gbd *c fbd"
    1.32 -apply simp
    1.33 -apply (rule ordLeq_transitive)
    1.34 -apply (rule card_of_UNION_Sigma)
    1.35 -apply (subst SIGMA_CSUM)
    1.36 -apply (rule ordLeq_transitive)
    1.37 -apply (rule card_of_Csum_Times')
    1.38 -apply (rule fbd_Card_order)
    1.39 -apply (rule ballI)
    1.40 -apply (rule fset_bd)
    1.41 -apply (rule ordLeq_transitive)
    1.42 -apply (rule cprod_mono1)
    1.43 -apply (rule gset_bd)
    1.44 -apply (rule ordIso_imp_ordLeq)
    1.45 -apply (rule ordIso_refl)
    1.46 -apply (rule Card_order_cprod)
    1.47 -done
    1.48 -
    1.49 -lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
    1.50 -apply (erule ordIso_transitive)
    1.51 -apply (frule csum_absorb2')
    1.52 -apply (erule ordLeq_refl)
    1.53 -by simp
    1.54 -
    1.55 -lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r"
    1.56 -apply (erule ordIso_transitive)
    1.57 -apply (rule cprod_infinite)
    1.58 -by simp
    1.59 -
    1.60 -lemma Union_image_insert: "\<Union>(f ` insert a B) = f a \<union> \<Union>(f ` B)"
    1.61 -by simp
    1.62 -
    1.63 -lemma Union_image_empty: "A \<union> \<Union>(f ` {}) = A"
    1.64 -by simp
    1.65 -
    1.66 -lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F"
    1.67 -by (rule ext) (auto simp add: collect_def)
    1.68 -
    1.69 -lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})"
    1.70 -by blast
    1.71 -
    1.72 -lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
    1.73 -by blast
    1.74 -
    1.75 -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"
    1.76 -by (unfold comp_apply collect_def) simp
    1.77 -
    1.78 -lemma wpull_cong:
    1.79 -"\<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"
    1.80 -by simp
    1.81 -
    1.82 -lemma Grp_fst_snd: "(Grp (Collect (split R)) fst)^--1 OO Grp (Collect (split R)) snd = R"
    1.83 -unfolding Grp_def fun_eq_iff relcompp.simps by auto
    1.84 -
    1.85 -lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)^--1 OO Grp A g = (Grp B f)^--1 OO Grp B g"
    1.86 -by (rule arg_cong)
    1.87 -
    1.88 -lemma vimage2p_relcompp_mono: "R OO S \<le> T \<Longrightarrow>
    1.89 -  vimage2p f g R OO vimage2p g h S \<le> vimage2p f h T"
    1.90 -  unfolding vimage2p_def by auto
    1.91 -
    1.92 -lemma type_copy_map_cong0: "M (g x) = N (h x) \<Longrightarrow> (f o M o g) x = (f o N o h) x"
    1.93 -  by auto
    1.94 -
    1.95 -lemma type_copy_set_bd: "(\<And>y. |S y| \<le>o bd) \<Longrightarrow> |(S o Rep) x| \<le>o bd"
    1.96 -  by auto
    1.97 -
    1.98 -lemma vimage2p_cong: "R = S \<Longrightarrow> vimage2p f g R = vimage2p f g S"
    1.99 -  by simp
   1.100 -
   1.101 -context
   1.102 -fixes Rep Abs
   1.103 -assumes type_copy: "type_definition Rep Abs UNIV"
   1.104 -begin
   1.105 -
   1.106 -lemma type_copy_map_id0: "M = id \<Longrightarrow> Abs o M o Rep = id"
   1.107 -  using type_definition.Rep_inverse[OF type_copy] by auto
   1.108 -
   1.109 -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)"
   1.110 -  using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto
   1.111 -
   1.112 -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)"
   1.113 -  using type_definition.Abs_inverse[OF type_copy UNIV_I] by (auto simp: o_def fun_eq_iff)
   1.114 -
   1.115 -lemma type_copy_wit: "x \<in> (S o Rep) (Abs y) \<Longrightarrow> x \<in> S y"
   1.116 -  using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto
   1.117 -
   1.118 -lemma type_copy_vimage2p_Grp_Rep: "vimage2p f Rep (Grp (Collect P) h) =
   1.119 -    Grp (Collect (\<lambda>x. P (f x))) (Abs o h o f)"
   1.120 -  unfolding vimage2p_def Grp_def fun_eq_iff
   1.121 -  by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
   1.122 -   type_definition.Rep_inverse[OF type_copy] dest: sym)
   1.123 -
   1.124 -lemma type_copy_vimage2p_Grp_Abs:
   1.125 -  "\<And>h. vimage2p g Abs (Grp (Collect P) h) = Grp (Collect (\<lambda>x. P (g x))) (Rep o h o g)"
   1.126 -  unfolding vimage2p_def Grp_def fun_eq_iff
   1.127 -  by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
   1.128 -   type_definition.Rep_inverse[OF type_copy] dest: sym)
   1.129 -
   1.130 -lemma type_copy_ex_RepI: "(\<exists>b. F b) = (\<exists>b. F (Rep b))"
   1.131 -proof safe
   1.132 -  fix b assume "F b"
   1.133 -  show "\<exists>b'. F (Rep b')"
   1.134 -  proof (rule exI)
   1.135 -    from `F b` show "F (Rep (Abs b))" using type_definition.Abs_inverse[OF type_copy] by auto
   1.136 -  qed
   1.137 -qed blast
   1.138 -
   1.139 -lemma vimage2p_relcompp_converse:
   1.140 -  "vimage2p f g (R^--1 OO S) = (vimage2p Rep f R)^--1 OO vimage2p Rep g S"
   1.141 -  unfolding vimage2p_def relcompp.simps conversep.simps fun_eq_iff image_def
   1.142 -  by (auto simp: type_copy_ex_RepI)
   1.143 -
   1.144 -end
   1.145 -
   1.146 -bnf DEADID: 'a
   1.147 -  map: "id :: 'a \<Rightarrow> 'a"
   1.148 -  bd: natLeq
   1.149 -  rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
   1.150 -by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite)
   1.151 -
   1.152 -definition id_bnf_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp \<equiv> (\<lambda>x. x)"
   1.153 -
   1.154 -lemma id_bnf_comp_apply: "id_bnf_comp x = x"
   1.155 -  unfolding id_bnf_comp_def by simp
   1.156 -
   1.157 -bnf ID: 'a
   1.158 -  map: "id_bnf_comp :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
   1.159 -  sets: "\<lambda>x. {x}"
   1.160 -  bd: natLeq
   1.161 -  rel: "id_bnf_comp :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
   1.162 -unfolding id_bnf_comp_def
   1.163 -apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
   1.164 -apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
   1.165 -apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
   1.166 -done
   1.167 -
   1.168 -lemma type_definition_id_bnf_comp_UNIV: "type_definition id_bnf_comp id_bnf_comp UNIV"
   1.169 -  unfolding id_bnf_comp_def by unfold_locales auto
   1.170 -
   1.171 -ML_file "Tools/BNF/bnf_comp_tactics.ML"
   1.172 -ML_file "Tools/BNF/bnf_comp.ML"
   1.173 -
   1.174 -hide_const (open) id_bnf_comp
   1.175 -hide_fact (open) id_bnf_comp_def type_definition_id_bnf_comp_UNIV
   1.176 -
   1.177 -end
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/BNF_Composition.thy	Mon Sep 01 16:34:40 2014 +0200
     2.3 @@ -0,0 +1,174 @@
     2.4 +(*  Title:      HOL/BNF_Composition.thy
     2.5 +    Author:     Dmitriy Traytel, TU Muenchen
     2.6 +    Author:     Jasmin Blanchette, TU Muenchen
     2.7 +    Copyright   2012, 2013, 2014
     2.8 +
     2.9 +Composition of bounded natural functors.
    2.10 +*)
    2.11 +
    2.12 +header {* Composition of Bounded Natural Functors *}
    2.13 +
    2.14 +theory BNF_Composition
    2.15 +imports BNF_Def
    2.16 +begin
    2.17 +
    2.18 +lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})"
    2.19 +  by (rule ext) simp
    2.20 +
    2.21 +lemma Union_natural: "Union o image (image f) = image f o Union"
    2.22 +  by (rule ext) (auto simp only: comp_apply)
    2.23 +
    2.24 +lemma in_Union_o_assoc: "x \<in> (Union o gset o gmap) A \<Longrightarrow> x \<in> (Union o (gset o gmap)) A"
    2.25 +  by (unfold comp_assoc)
    2.26 +
    2.27 +lemma comp_single_set_bd:
    2.28 +  assumes fbd_Card_order: "Card_order fbd" and
    2.29 +    fset_bd: "\<And>x. |fset x| \<le>o fbd" and
    2.30 +    gset_bd: "\<And>x. |gset x| \<le>o gbd"
    2.31 +  shows "|\<Union>(fset ` gset x)| \<le>o gbd *c fbd"
    2.32 +  apply simp
    2.33 +  apply (rule ordLeq_transitive)
    2.34 +  apply (rule card_of_UNION_Sigma)
    2.35 +  apply (subst SIGMA_CSUM)
    2.36 +  apply (rule ordLeq_transitive)
    2.37 +  apply (rule card_of_Csum_Times')
    2.38 +  apply (rule fbd_Card_order)
    2.39 +  apply (rule ballI)
    2.40 +  apply (rule fset_bd)
    2.41 +  apply (rule ordLeq_transitive)
    2.42 +  apply (rule cprod_mono1)
    2.43 +  apply (rule gset_bd)
    2.44 +  apply (rule ordIso_imp_ordLeq)
    2.45 +  apply (rule ordIso_refl)
    2.46 +  apply (rule Card_order_cprod)
    2.47 +  done
    2.48 +
    2.49 +lemma csum_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p +c p' =o r +c r \<Longrightarrow> p +c p' =o r"
    2.50 +  apply (erule ordIso_transitive)
    2.51 +  apply (frule csum_absorb2')
    2.52 +  apply (erule ordLeq_refl)
    2.53 +  by simp
    2.54 +
    2.55 +lemma cprod_dup: "cinfinite r \<Longrightarrow> Card_order r \<Longrightarrow> p *c p' =o r *c r \<Longrightarrow> p *c p' =o r"
    2.56 +  apply (erule ordIso_transitive)
    2.57 +  apply (rule cprod_infinite)
    2.58 +  by simp
    2.59 +
    2.60 +lemma Union_image_insert: "\<Union>(f ` insert a B) = f a \<union> \<Union>(f ` B)"
    2.61 +  by simp
    2.62 +
    2.63 +lemma Union_image_empty: "A \<union> \<Union>(f ` {}) = A"
    2.64 +  by simp
    2.65 +
    2.66 +lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F"
    2.67 +  by (rule ext) (auto simp add: collect_def)
    2.68 +
    2.69 +lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})"
    2.70 +  by blast
    2.71 +
    2.72 +lemma UN_image_subset: "\<Union>(f ` g x) \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
    2.73 +  by blast
    2.74 +
    2.75 +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"
    2.76 +  by (unfold comp_apply collect_def) simp
    2.77 +
    2.78 +lemma wpull_cong:
    2.79 +  "\<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"
    2.80 +  by simp
    2.81 +
    2.82 +lemma Grp_fst_snd: "(Grp (Collect (split R)) fst)^--1 OO Grp (Collect (split R)) snd = R"
    2.83 +  unfolding Grp_def fun_eq_iff relcompp.simps by auto
    2.84 +
    2.85 +lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)^--1 OO Grp A g = (Grp B f)^--1 OO Grp B g"
    2.86 +  by (rule arg_cong)
    2.87 +
    2.88 +lemma vimage2p_relcompp_mono: "R OO S \<le> T \<Longrightarrow>
    2.89 +  vimage2p f g R OO vimage2p g h S \<le> vimage2p f h T"
    2.90 +  unfolding vimage2p_def by auto
    2.91 +
    2.92 +lemma type_copy_map_cong0: "M (g x) = N (h x) \<Longrightarrow> (f o M o g) x = (f o N o h) x"
    2.93 +  by auto
    2.94 +
    2.95 +lemma type_copy_set_bd: "(\<And>y. |S y| \<le>o bd) \<Longrightarrow> |(S o Rep) x| \<le>o bd"
    2.96 +  by auto
    2.97 +
    2.98 +lemma vimage2p_cong: "R = S \<Longrightarrow> vimage2p f g R = vimage2p f g S"
    2.99 +  by simp
   2.100 +
   2.101 +context
   2.102 +  fixes Rep Abs
   2.103 +  assumes type_copy: "type_definition Rep Abs UNIV"
   2.104 +begin
   2.105 +
   2.106 +lemma type_copy_map_id0: "M = id \<Longrightarrow> Abs o M o Rep = id"
   2.107 +  using type_definition.Rep_inverse[OF type_copy] by auto
   2.108 +
   2.109 +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)"
   2.110 +  using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto
   2.111 +
   2.112 +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)"
   2.113 +  using type_definition.Abs_inverse[OF type_copy UNIV_I] by (auto simp: o_def fun_eq_iff)
   2.114 +
   2.115 +lemma type_copy_wit: "x \<in> (S o Rep) (Abs y) \<Longrightarrow> x \<in> S y"
   2.116 +  using type_definition.Abs_inverse[OF type_copy UNIV_I] by auto
   2.117 +
   2.118 +lemma type_copy_vimage2p_Grp_Rep: "vimage2p f Rep (Grp (Collect P) h) =
   2.119 +    Grp (Collect (\<lambda>x. P (f x))) (Abs o h o f)"
   2.120 +  unfolding vimage2p_def Grp_def fun_eq_iff
   2.121 +  by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
   2.122 +   type_definition.Rep_inverse[OF type_copy] dest: sym)
   2.123 +
   2.124 +lemma type_copy_vimage2p_Grp_Abs:
   2.125 +  "\<And>h. vimage2p g Abs (Grp (Collect P) h) = Grp (Collect (\<lambda>x. P (g x))) (Rep o h o g)"
   2.126 +  unfolding vimage2p_def Grp_def fun_eq_iff
   2.127 +  by (auto simp: type_definition.Abs_inverse[OF type_copy UNIV_I]
   2.128 +   type_definition.Rep_inverse[OF type_copy] dest: sym)
   2.129 +
   2.130 +lemma type_copy_ex_RepI: "(\<exists>b. F b) = (\<exists>b. F (Rep b))"
   2.131 +proof safe
   2.132 +  fix b assume "F b"
   2.133 +  show "\<exists>b'. F (Rep b')"
   2.134 +  proof (rule exI)
   2.135 +    from `F b` show "F (Rep (Abs b))" using type_definition.Abs_inverse[OF type_copy] by auto
   2.136 +  qed
   2.137 +qed blast
   2.138 +
   2.139 +lemma vimage2p_relcompp_converse:
   2.140 +  "vimage2p f g (R^--1 OO S) = (vimage2p Rep f R)^--1 OO vimage2p Rep g S"
   2.141 +  unfolding vimage2p_def relcompp.simps conversep.simps fun_eq_iff image_def
   2.142 +  by (auto simp: type_copy_ex_RepI)
   2.143 +
   2.144 +end
   2.145 +
   2.146 +bnf DEADID: 'a
   2.147 +  map: "id :: 'a \<Rightarrow> 'a"
   2.148 +  bd: natLeq
   2.149 +  rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
   2.150 +  by (auto simp add: Grp_def natLeq_card_order natLeq_cinfinite)
   2.151 +
   2.152 +definition id_bnf_comp :: "'a \<Rightarrow> 'a" where "id_bnf_comp \<equiv> (\<lambda>x. x)"
   2.153 +
   2.154 +lemma id_bnf_comp_apply: "id_bnf_comp x = x"
   2.155 +  unfolding id_bnf_comp_def by simp
   2.156 +
   2.157 +bnf ID: 'a
   2.158 +  map: "id_bnf_comp :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
   2.159 +  sets: "\<lambda>x. {x}"
   2.160 +  bd: natLeq
   2.161 +  rel: "id_bnf_comp :: ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> bool"
   2.162 +  unfolding id_bnf_comp_def
   2.163 +  apply (auto simp: Grp_def fun_eq_iff relcompp.simps natLeq_card_order natLeq_cinfinite)
   2.164 +  apply (rule ordLess_imp_ordLeq[OF finite_ordLess_infinite[OF _ natLeq_Well_order]])
   2.165 +  apply (auto simp add: Field_card_of Field_natLeq card_of_well_order_on)[3]
   2.166 +  done
   2.167 +
   2.168 +lemma type_definition_id_bnf_comp_UNIV: "type_definition id_bnf_comp id_bnf_comp UNIV"
   2.169 +  unfolding id_bnf_comp_def by unfold_locales auto
   2.170 +
   2.171 +ML_file "Tools/BNF/bnf_comp_tactics.ML"
   2.172 +ML_file "Tools/BNF/bnf_comp.ML"
   2.173 +
   2.174 +hide_const (open) id_bnf_comp
   2.175 +hide_fact (open) id_bnf_comp_def type_definition_id_bnf_comp_UNIV
   2.176 +
   2.177 +end
     3.1 --- a/src/HOL/BNF_FP_Base.thy	Mon Sep 01 16:34:39 2014 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,232 +0,0 @@
     3.4 -(*  Title:      HOL/BNF_FP_Base.thy
     3.5 -    Author:     Lorenz Panny, TU Muenchen
     3.6 -    Author:     Dmitriy Traytel, TU Muenchen
     3.7 -    Author:     Jasmin Blanchette, TU Muenchen
     3.8 -    Author:     Martin Desharnais, TU Muenchen
     3.9 -    Copyright   2012, 2013, 2014
    3.10 -
    3.11 -Shared fixed point operations on bounded natural functors.
    3.12 -*)
    3.13 -
    3.14 -header {* Shared Fixed Point Operations on Bounded Natural Functors *}
    3.15 -
    3.16 -theory BNF_FP_Base
    3.17 -imports BNF_Comp Basic_BNFs
    3.18 -begin
    3.19 -
    3.20 -lemma False_imp_eq_True: "(False \<Longrightarrow> Q) \<equiv> Trueprop True"
    3.21 -  by default simp_all
    3.22 -
    3.23 -lemma conj_imp_eq_imp_imp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)"
    3.24 -  by default simp_all
    3.25 -
    3.26 -lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
    3.27 -by auto
    3.28 -
    3.29 -lemma predicate2D_conj: "P \<le> Q \<and> R \<Longrightarrow> P x y \<Longrightarrow> R \<and> Q x y"
    3.30 -  by auto
    3.31 -
    3.32 -lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
    3.33 -by blast
    3.34 -
    3.35 -lemma case_unit_Unity: "(case u of () \<Rightarrow> f) = f"
    3.36 -by (cases u) (hypsubst, rule unit.case)
    3.37 -
    3.38 -lemma case_prod_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p"
    3.39 -by simp
    3.40 -
    3.41 -lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
    3.42 -by simp
    3.43 -
    3.44 -lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
    3.45 -unfolding comp_def fun_eq_iff by simp
    3.46 -
    3.47 -lemma o_bij:
    3.48 -  assumes gf: "g \<circ> f = id" and fg: "f \<circ> g = id"
    3.49 -  shows "bij f"
    3.50 -unfolding bij_def inj_on_def surj_def proof safe
    3.51 -  fix a1 a2 assume "f a1 = f a2"
    3.52 -  hence "g ( f a1) = g (f a2)" by simp
    3.53 -  thus "a1 = a2" using gf unfolding fun_eq_iff by simp
    3.54 -next
    3.55 -  fix b
    3.56 -  have "b = f (g b)"
    3.57 -  using fg unfolding fun_eq_iff by simp
    3.58 -  thus "EX a. b = f a" by blast
    3.59 -qed
    3.60 -
    3.61 -lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp
    3.62 -
    3.63 -lemma case_sum_step:
    3.64 -"case_sum (case_sum f' g') g (Inl p) = case_sum f' g' p"
    3.65 -"case_sum f (case_sum f' g') (Inr p) = case_sum f' g' p"
    3.66 -by auto
    3.67 -
    3.68 -lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
    3.69 -by blast
    3.70 -
    3.71 -lemma type_copy_obj_one_point_absE:
    3.72 -  assumes "type_definition Rep Abs UNIV" "\<forall>x. s = Abs x \<longrightarrow> P" shows P
    3.73 -  using type_definition.Rep_inverse[OF assms(1)]
    3.74 -  by (intro mp[OF spec[OF assms(2), of "Rep s"]]) simp
    3.75 -
    3.76 -lemma obj_sumE_f:
    3.77 -  assumes "\<forall>x. s = f (Inl x) \<longrightarrow> P" "\<forall>x. s = f (Inr x) \<longrightarrow> P"
    3.78 -  shows "\<forall>x. s = f x \<longrightarrow> P"
    3.79 -proof
    3.80 -  fix x from assms show "s = f x \<longrightarrow> P" by (cases x) auto
    3.81 -qed
    3.82 -
    3.83 -lemma case_sum_if:
    3.84 -"case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)"
    3.85 -by simp
    3.86 -
    3.87 -lemma prod_set_simps:
    3.88 -"fsts (x, y) = {x}"
    3.89 -"snds (x, y) = {y}"
    3.90 -unfolding fsts_def snds_def by simp+
    3.91 -
    3.92 -lemma sum_set_simps:
    3.93 -"setl (Inl x) = {x}"
    3.94 -"setl (Inr x) = {}"
    3.95 -"setr (Inl x) = {}"
    3.96 -"setr (Inr x) = {x}"
    3.97 -unfolding sum_set_defs by simp+
    3.98 -
    3.99 -lemma Inl_Inr_False: "(Inl x = Inr y) = False"
   3.100 -  by simp
   3.101 -
   3.102 -lemma Inr_Inl_False: "(Inr x = Inl y) = False"
   3.103 -  by simp
   3.104 -
   3.105 -lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
   3.106 -by blast
   3.107 -
   3.108 -lemma rewriteR_comp_comp: "\<lbrakk>g \<circ> h = r\<rbrakk> \<Longrightarrow> f \<circ> g \<circ> h = f \<circ> r"
   3.109 -  unfolding comp_def fun_eq_iff by auto
   3.110 -
   3.111 -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"
   3.112 -  unfolding comp_def fun_eq_iff by auto
   3.113 -
   3.114 -lemma rewriteL_comp_comp: "\<lbrakk>f \<circ> g = l\<rbrakk> \<Longrightarrow> f \<circ> (g \<circ> h) = l \<circ> h"
   3.115 -  unfolding comp_def fun_eq_iff by auto
   3.116 -
   3.117 -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"
   3.118 -  unfolding comp_def fun_eq_iff by auto
   3.119 -
   3.120 -lemma convol_o: "\<langle>f, g\<rangle> \<circ> h = \<langle>f \<circ> h, g \<circ> h\<rangle>"
   3.121 -  unfolding convol_def by auto
   3.122 -
   3.123 -lemma map_prod_o_convol: "map_prod h1 h2 \<circ> \<langle>f, g\<rangle> = \<langle>h1 \<circ> f, h2 \<circ> g\<rangle>"
   3.124 -  unfolding convol_def by auto
   3.125 -
   3.126 -lemma map_prod_o_convol_id: "(map_prod f id \<circ> \<langle>id, g\<rangle>) x = \<langle>id \<circ> f, g\<rangle> x"
   3.127 -  unfolding map_prod_o_convol id_comp comp_id ..
   3.128 -
   3.129 -lemma o_case_sum: "h \<circ> case_sum f g = case_sum (h \<circ> f) (h \<circ> g)"
   3.130 -  unfolding comp_def by (auto split: sum.splits)
   3.131 -
   3.132 -lemma case_sum_o_map_sum: "case_sum f g \<circ> map_sum h1 h2 = case_sum (f \<circ> h1) (g \<circ> h2)"
   3.133 -  unfolding comp_def by (auto split: sum.splits)
   3.134 -
   3.135 -lemma case_sum_o_map_sum_id: "(case_sum id g \<circ> map_sum f id) x = case_sum (f \<circ> id) g x"
   3.136 -  unfolding case_sum_o_map_sum id_comp comp_id ..
   3.137 -
   3.138 -lemma rel_fun_def_butlast:
   3.139 -  "rel_fun R (rel_fun S T) f g = (\<forall>x y. R x y \<longrightarrow> (rel_fun S T) (f x) (g y))"
   3.140 -  unfolding rel_fun_def ..
   3.141 -
   3.142 -lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)"
   3.143 -  by auto
   3.144 -
   3.145 -lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)"
   3.146 -  by auto
   3.147 -
   3.148 -lemma eq_le_Grp_id_iff: "(op = \<le> Grp (Collect R) id) = (All R)"
   3.149 -  unfolding Grp_def id_apply by blast
   3.150 -
   3.151 -lemma Grp_id_mono_subst: "(\<And>x y. Grp P id x y \<Longrightarrow> Grp Q id (f x) (f y)) \<equiv>
   3.152 -   (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
   3.153 -  unfolding Grp_def by rule auto
   3.154 -
   3.155 -lemma vimage2p_mono: "vimage2p f g R x y \<Longrightarrow> R \<le> S \<Longrightarrow> vimage2p f g S x y"
   3.156 -  unfolding vimage2p_def by blast
   3.157 -
   3.158 -lemma vimage2p_refl: "(\<And>x. R x x) \<Longrightarrow> vimage2p f f R x x"
   3.159 -  unfolding vimage2p_def by auto
   3.160 -
   3.161 -lemma
   3.162 -  assumes "type_definition Rep Abs UNIV"
   3.163 -  shows type_copy_Rep_o_Abs: "Rep \<circ> Abs = id" and type_copy_Abs_o_Rep: "Abs \<circ> Rep = id"
   3.164 -  unfolding fun_eq_iff comp_apply id_apply
   3.165 -    type_definition.Abs_inverse[OF assms UNIV_I] type_definition.Rep_inverse[OF assms] by simp_all
   3.166 -
   3.167 -lemma type_copy_map_comp0_undo:
   3.168 -  assumes "type_definition Rep Abs UNIV"
   3.169 -          "type_definition Rep' Abs' UNIV"
   3.170 -          "type_definition Rep'' Abs'' UNIV"
   3.171 -  shows "Abs' \<circ> M \<circ> Rep'' = (Abs' \<circ> M1 \<circ> Rep) \<circ> (Abs \<circ> M2 \<circ> Rep'') \<Longrightarrow> M1 \<circ> M2 = M"
   3.172 -  by (rule sym) (auto simp: fun_eq_iff type_definition.Abs_inject[OF assms(2) UNIV_I UNIV_I]
   3.173 -    type_definition.Abs_inverse[OF assms(1) UNIV_I]
   3.174 -    type_definition.Abs_inverse[OF assms(3) UNIV_I] dest: spec[of _ "Abs'' x" for x])
   3.175 -
   3.176 -lemma vimage2p_id: "vimage2p id id R = R"
   3.177 -  unfolding vimage2p_def by auto
   3.178 -
   3.179 -lemma vimage2p_comp: "vimage2p (f1 \<circ> f2) (g1 \<circ> g2) = vimage2p f2 g2 \<circ> vimage2p f1 g1"
   3.180 -  unfolding fun_eq_iff vimage2p_def o_apply by simp
   3.181 -
   3.182 -lemma fun_cong_unused_0: "f = (\<lambda>x. g) \<Longrightarrow> f (\<lambda>x. 0) = g"
   3.183 -  by (erule arg_cong)
   3.184 -
   3.185 -lemma inj_on_convol_ident: "inj_on (\<lambda>x. (x, f x)) X"
   3.186 -  unfolding inj_on_def by simp
   3.187 -
   3.188 -lemma case_prod_app: "case_prod f x y = case_prod (\<lambda>l r. f l r y) x"
   3.189 -  by (case_tac x) simp
   3.190 -
   3.191 -lemma case_sum_map_sum: "case_sum l r (map_sum f g x) = case_sum (l \<circ> f) (r \<circ> g) x"
   3.192 -  by (case_tac x) simp+
   3.193 -
   3.194 -lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x"
   3.195 -  by (case_tac x) simp+
   3.196 -
   3.197 -lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)"
   3.198 -  by (simp add: inj_on_def)
   3.199 -
   3.200 -lemma eq_ifI: "(P \<longrightarrow> t = u1) \<Longrightarrow> (\<not> P \<longrightarrow> t = u2) \<Longrightarrow> t = (if P then u1 else u2)"
   3.201 -  by simp
   3.202 -
   3.203 -ML_file "Tools/BNF/bnf_fp_util.ML"
   3.204 -ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
   3.205 -ML_file "Tools/BNF/bnf_lfp_size.ML"
   3.206 -ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
   3.207 -ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML"
   3.208 -ML_file "Tools/BNF/bnf_fp_n2m.ML"
   3.209 -ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML"
   3.210 -
   3.211 -ML_file "Tools/Function/old_size.ML"
   3.212 -setup Old_Size.setup
   3.213 -
   3.214 -lemma size_bool[code]: "size (b\<Colon>bool) = 0"
   3.215 -  by (cases b) auto
   3.216 -
   3.217 -lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"
   3.218 -  by (induct n) simp_all
   3.219 -
   3.220 -declare prod.size[no_atp]
   3.221 -
   3.222 -lemma size_sum_o_map: "size_sum g1 g2 \<circ> map_sum f1 f2 = size_sum (g1 \<circ> f1) (g2 \<circ> f2)"
   3.223 -  by (rule ext) (case_tac x, auto)
   3.224 -
   3.225 -lemma size_prod_o_map: "size_prod g1 g2 \<circ> map_prod f1 f2 = size_prod (g1 \<circ> f1) (g2 \<circ> f2)"
   3.226 -  by (rule ext) auto
   3.227 -
   3.228 -setup {*
   3.229 -BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size}
   3.230 -  @{thms size_sum_o_map}
   3.231 -#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size}
   3.232 -  @{thms size_prod_o_map}
   3.233 -*}
   3.234 -
   3.235 -end
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/BNF_Fixpoint_Base.thy	Mon Sep 01 16:34:40 2014 +0200
     4.3 @@ -0,0 +1,232 @@
     4.4 +(*  Title:      HOL/BNF_Fixpoint_Base.thy
     4.5 +    Author:     Lorenz Panny, TU Muenchen
     4.6 +    Author:     Dmitriy Traytel, TU Muenchen
     4.7 +    Author:     Jasmin Blanchette, TU Muenchen
     4.8 +    Author:     Martin Desharnais, TU Muenchen
     4.9 +    Copyright   2012, 2013, 2014
    4.10 +
    4.11 +Shared fixed point operations on bounded natural functors.
    4.12 +*)
    4.13 +
    4.14 +header {* Shared Fixed Point Operations on Bounded Natural Functors *}
    4.15 +
    4.16 +theory BNF_Fixpoint_Base
    4.17 +imports BNF_Composition Basic_BNFs
    4.18 +begin
    4.19 +
    4.20 +lemma False_imp_eq_True: "(False \<Longrightarrow> Q) \<equiv> Trueprop True"
    4.21 +  by default simp_all
    4.22 +
    4.23 +lemma conj_imp_eq_imp_imp: "(P \<and> Q \<Longrightarrow> PROP R) \<equiv> (P \<Longrightarrow> Q \<Longrightarrow> PROP R)"
    4.24 +  by default simp_all
    4.25 +
    4.26 +lemma mp_conj: "(P \<longrightarrow> Q) \<and> R \<Longrightarrow> P \<Longrightarrow> R \<and> Q"
    4.27 +by auto
    4.28 +
    4.29 +lemma predicate2D_conj: "P \<le> Q \<and> R \<Longrightarrow> P x y \<Longrightarrow> R \<and> Q x y"
    4.30 +  by auto
    4.31 +
    4.32 +lemma eq_sym_Unity_conv: "(x = (() = ())) = x"
    4.33 +by blast
    4.34 +
    4.35 +lemma case_unit_Unity: "(case u of () \<Rightarrow> f) = f"
    4.36 +by (cases u) (hypsubst, rule unit.case)
    4.37 +
    4.38 +lemma case_prod_Pair_iden: "(case p of (x, y) \<Rightarrow> (x, y)) = p"
    4.39 +by simp
    4.40 +
    4.41 +lemma unit_all_impI: "(P () \<Longrightarrow> Q ()) \<Longrightarrow> \<forall>x. P x \<longrightarrow> Q x"
    4.42 +by simp
    4.43 +
    4.44 +lemma pointfree_idE: "f \<circ> g = id \<Longrightarrow> f (g x) = x"
    4.45 +unfolding comp_def fun_eq_iff by simp
    4.46 +
    4.47 +lemma o_bij:
    4.48 +  assumes gf: "g \<circ> f = id" and fg: "f \<circ> g = id"
    4.49 +  shows "bij f"
    4.50 +unfolding bij_def inj_on_def surj_def proof safe
    4.51 +  fix a1 a2 assume "f a1 = f a2"
    4.52 +  hence "g ( f a1) = g (f a2)" by simp
    4.53 +  thus "a1 = a2" using gf unfolding fun_eq_iff by simp
    4.54 +next
    4.55 +  fix b
    4.56 +  have "b = f (g b)"
    4.57 +  using fg unfolding fun_eq_iff by simp
    4.58 +  thus "EX a. b = f a" by blast
    4.59 +qed
    4.60 +
    4.61 +lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp
    4.62 +
    4.63 +lemma case_sum_step:
    4.64 +"case_sum (case_sum f' g') g (Inl p) = case_sum f' g' p"
    4.65 +"case_sum f (case_sum f' g') (Inr p) = case_sum f' g' p"
    4.66 +by auto
    4.67 +
    4.68 +lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
    4.69 +by blast
    4.70 +
    4.71 +lemma type_copy_obj_one_point_absE:
    4.72 +  assumes "type_definition Rep Abs UNIV" "\<forall>x. s = Abs x \<longrightarrow> P" shows P
    4.73 +  using type_definition.Rep_inverse[OF assms(1)]
    4.74 +  by (intro mp[OF spec[OF assms(2), of "Rep s"]]) simp
    4.75 +
    4.76 +lemma obj_sumE_f:
    4.77 +  assumes "\<forall>x. s = f (Inl x) \<longrightarrow> P" "\<forall>x. s = f (Inr x) \<longrightarrow> P"
    4.78 +  shows "\<forall>x. s = f x \<longrightarrow> P"
    4.79 +proof
    4.80 +  fix x from assms show "s = f x \<longrightarrow> P" by (cases x) auto
    4.81 +qed
    4.82 +
    4.83 +lemma case_sum_if:
    4.84 +"case_sum f g (if p then Inl x else Inr y) = (if p then f x else g y)"
    4.85 +by simp
    4.86 +
    4.87 +lemma prod_set_simps:
    4.88 +"fsts (x, y) = {x}"
    4.89 +"snds (x, y) = {y}"
    4.90 +unfolding fsts_def snds_def by simp+
    4.91 +
    4.92 +lemma sum_set_simps:
    4.93 +"setl (Inl x) = {x}"
    4.94 +"setl (Inr x) = {}"
    4.95 +"setr (Inl x) = {}"
    4.96 +"setr (Inr x) = {x}"
    4.97 +unfolding sum_set_defs by simp+
    4.98 +
    4.99 +lemma Inl_Inr_False: "(Inl x = Inr y) = False"
   4.100 +  by simp
   4.101 +
   4.102 +lemma Inr_Inl_False: "(Inr x = Inl y) = False"
   4.103 +  by simp
   4.104 +
   4.105 +lemma spec2: "\<forall>x y. P x y \<Longrightarrow> P x y"
   4.106 +by blast
   4.107 +
   4.108 +lemma rewriteR_comp_comp: "\<lbrakk>g \<circ> h = r\<rbrakk> \<Longrightarrow> f \<circ> g \<circ> h = f \<circ> r"
   4.109 +  unfolding comp_def fun_eq_iff by auto
   4.110 +
   4.111 +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"
   4.112 +  unfolding comp_def fun_eq_iff by auto
   4.113 +
   4.114 +lemma rewriteL_comp_comp: "\<lbrakk>f \<circ> g = l\<rbrakk> \<Longrightarrow> f \<circ> (g \<circ> h) = l \<circ> h"
   4.115 +  unfolding comp_def fun_eq_iff by auto
   4.116 +
   4.117 +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"
   4.118 +  unfolding comp_def fun_eq_iff by auto
   4.119 +
   4.120 +lemma convol_o: "\<langle>f, g\<rangle> \<circ> h = \<langle>f \<circ> h, g \<circ> h\<rangle>"
   4.121 +  unfolding convol_def by auto
   4.122 +
   4.123 +lemma map_prod_o_convol: "map_prod h1 h2 \<circ> \<langle>f, g\<rangle> = \<langle>h1 \<circ> f, h2 \<circ> g\<rangle>"
   4.124 +  unfolding convol_def by auto
   4.125 +
   4.126 +lemma map_prod_o_convol_id: "(map_prod f id \<circ> \<langle>id, g\<rangle>) x = \<langle>id \<circ> f, g\<rangle> x"
   4.127 +  unfolding map_prod_o_convol id_comp comp_id ..
   4.128 +
   4.129 +lemma o_case_sum: "h \<circ> case_sum f g = case_sum (h \<circ> f) (h \<circ> g)"
   4.130 +  unfolding comp_def by (auto split: sum.splits)
   4.131 +
   4.132 +lemma case_sum_o_map_sum: "case_sum f g \<circ> map_sum h1 h2 = case_sum (f \<circ> h1) (g \<circ> h2)"
   4.133 +  unfolding comp_def by (auto split: sum.splits)
   4.134 +
   4.135 +lemma case_sum_o_map_sum_id: "(case_sum id g \<circ> map_sum f id) x = case_sum (f \<circ> id) g x"
   4.136 +  unfolding case_sum_o_map_sum id_comp comp_id ..
   4.137 +
   4.138 +lemma rel_fun_def_butlast:
   4.139 +  "rel_fun R (rel_fun S T) f g = (\<forall>x y. R x y \<longrightarrow> (rel_fun S T) (f x) (g y))"
   4.140 +  unfolding rel_fun_def ..
   4.141 +
   4.142 +lemma subst_eq_imp: "(\<forall>a b. a = b \<longrightarrow> P a b) \<equiv> (\<forall>a. P a a)"
   4.143 +  by auto
   4.144 +
   4.145 +lemma eq_subset: "op = \<le> (\<lambda>a b. P a b \<or> a = b)"
   4.146 +  by auto
   4.147 +
   4.148 +lemma eq_le_Grp_id_iff: "(op = \<le> Grp (Collect R) id) = (All R)"
   4.149 +  unfolding Grp_def id_apply by blast
   4.150 +
   4.151 +lemma Grp_id_mono_subst: "(\<And>x y. Grp P id x y \<Longrightarrow> Grp Q id (f x) (f y)) \<equiv>
   4.152 +   (\<And>x. x \<in> P \<Longrightarrow> f x \<in> Q)"
   4.153 +  unfolding Grp_def by rule auto
   4.154 +
   4.155 +lemma vimage2p_mono: "vimage2p f g R x y \<Longrightarrow> R \<le> S \<Longrightarrow> vimage2p f g S x y"
   4.156 +  unfolding vimage2p_def by blast
   4.157 +
   4.158 +lemma vimage2p_refl: "(\<And>x. R x x) \<Longrightarrow> vimage2p f f R x x"
   4.159 +  unfolding vimage2p_def by auto
   4.160 +
   4.161 +lemma
   4.162 +  assumes "type_definition Rep Abs UNIV"
   4.163 +  shows type_copy_Rep_o_Abs: "Rep \<circ> Abs = id" and type_copy_Abs_o_Rep: "Abs \<circ> Rep = id"
   4.164 +  unfolding fun_eq_iff comp_apply id_apply
   4.165 +    type_definition.Abs_inverse[OF assms UNIV_I] type_definition.Rep_inverse[OF assms] by simp_all
   4.166 +
   4.167 +lemma type_copy_map_comp0_undo:
   4.168 +  assumes "type_definition Rep Abs UNIV"
   4.169 +          "type_definition Rep' Abs' UNIV"
   4.170 +          "type_definition Rep'' Abs'' UNIV"
   4.171 +  shows "Abs' \<circ> M \<circ> Rep'' = (Abs' \<circ> M1 \<circ> Rep) \<circ> (Abs \<circ> M2 \<circ> Rep'') \<Longrightarrow> M1 \<circ> M2 = M"
   4.172 +  by (rule sym) (auto simp: fun_eq_iff type_definition.Abs_inject[OF assms(2) UNIV_I UNIV_I]
   4.173 +    type_definition.Abs_inverse[OF assms(1) UNIV_I]
   4.174 +    type_definition.Abs_inverse[OF assms(3) UNIV_I] dest: spec[of _ "Abs'' x" for x])
   4.175 +
   4.176 +lemma vimage2p_id: "vimage2p id id R = R"
   4.177 +  unfolding vimage2p_def by auto
   4.178 +
   4.179 +lemma vimage2p_comp: "vimage2p (f1 \<circ> f2) (g1 \<circ> g2) = vimage2p f2 g2 \<circ> vimage2p f1 g1"
   4.180 +  unfolding fun_eq_iff vimage2p_def o_apply by simp
   4.181 +
   4.182 +lemma fun_cong_unused_0: "f = (\<lambda>x. g) \<Longrightarrow> f (\<lambda>x. 0) = g"
   4.183 +  by (erule arg_cong)
   4.184 +
   4.185 +lemma inj_on_convol_ident: "inj_on (\<lambda>x. (x, f x)) X"
   4.186 +  unfolding inj_on_def by simp
   4.187 +
   4.188 +lemma case_prod_app: "case_prod f x y = case_prod (\<lambda>l r. f l r y) x"
   4.189 +  by (case_tac x) simp
   4.190 +
   4.191 +lemma case_sum_map_sum: "case_sum l r (map_sum f g x) = case_sum (l \<circ> f) (r \<circ> g) x"
   4.192 +  by (case_tac x) simp+
   4.193 +
   4.194 +lemma case_prod_map_prod: "case_prod h (map_prod f g x) = case_prod (\<lambda>l r. h (f l) (g r)) x"
   4.195 +  by (case_tac x) simp+
   4.196 +
   4.197 +lemma prod_inj_map: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (map_prod f g)"
   4.198 +  by (simp add: inj_on_def)
   4.199 +
   4.200 +lemma eq_ifI: "(P \<longrightarrow> t = u1) \<Longrightarrow> (\<not> P \<longrightarrow> t = u2) \<Longrightarrow> t = (if P then u1 else u2)"
   4.201 +  by simp
   4.202 +
   4.203 +ML_file "Tools/BNF/bnf_fp_util.ML"
   4.204 +ML_file "Tools/BNF/bnf_fp_def_sugar_tactics.ML"
   4.205 +ML_file "Tools/BNF/bnf_lfp_size.ML"
   4.206 +ML_file "Tools/BNF/bnf_fp_def_sugar.ML"
   4.207 +ML_file "Tools/BNF/bnf_fp_n2m_tactics.ML"
   4.208 +ML_file "Tools/BNF/bnf_fp_n2m.ML"
   4.209 +ML_file "Tools/BNF/bnf_fp_n2m_sugar.ML"
   4.210 +
   4.211 +ML_file "Tools/Function/old_size.ML"
   4.212 +setup Old_Size.setup
   4.213 +
   4.214 +lemma size_bool[code]: "size (b\<Colon>bool) = 0"
   4.215 +  by (cases b) auto
   4.216 +
   4.217 +lemma size_nat[simp, code]: "size (n\<Colon>nat) = n"
   4.218 +  by (induct n) simp_all
   4.219 +
   4.220 +declare prod.size[no_atp]
   4.221 +
   4.222 +lemma size_sum_o_map: "size_sum g1 g2 \<circ> map_sum f1 f2 = size_sum (g1 \<circ> f1) (g2 \<circ> f2)"
   4.223 +  by (rule ext) (case_tac x, auto)
   4.224 +
   4.225 +lemma size_prod_o_map: "size_prod g1 g2 \<circ> map_prod f1 f2 = size_prod (g1 \<circ> f1) (g2 \<circ> f2)"
   4.226 +  by (rule ext) auto
   4.227 +
   4.228 +setup {*
   4.229 +BNF_LFP_Size.register_size_global @{type_name sum} @{const_name size_sum} @{thms sum.size}
   4.230 +  @{thms size_sum_o_map}
   4.231 +#> BNF_LFP_Size.register_size_global @{type_name prod} @{const_name size_prod} @{thms prod.size}
   4.232 +  @{thms size_prod_o_map}
   4.233 +*}
   4.234 +
   4.235 +end
     5.1 --- a/src/HOL/BNF_GFP.thy	Mon Sep 01 16:34:39 2014 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,300 +0,0 @@
     5.4 -(*  Title:      HOL/BNF_GFP.thy
     5.5 -    Author:     Dmitriy Traytel, TU Muenchen
     5.6 -    Author:     Lorenz Panny, TU Muenchen
     5.7 -    Author:     Jasmin Blanchette, TU Muenchen
     5.8 -    Copyright   2012, 2013, 2014
     5.9 -
    5.10 -Greatest fixed point operation on bounded natural functors.
    5.11 -*)
    5.12 -
    5.13 -header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
    5.14 -
    5.15 -theory BNF_GFP
    5.16 -imports BNF_FP_Base String
    5.17 -keywords
    5.18 -  "codatatype" :: thy_decl and
    5.19 -  "primcorecursive" :: thy_goal and
    5.20 -  "primcorec" :: thy_decl
    5.21 -begin
    5.22 -
    5.23 -setup {*
    5.24 -Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}
    5.25 -*}
    5.26 -
    5.27 -lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    5.28 -  by simp
    5.29 -
    5.30 -lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    5.31 -  by (cases s) auto
    5.32 -
    5.33 -lemma not_TrueE: "\<not> True \<Longrightarrow> P"
    5.34 -  by (erule notE, rule TrueI)
    5.35 -
    5.36 -lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
    5.37 -  by fast
    5.38 -
    5.39 -lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
    5.40 -  by (auto split: sum.splits)
    5.41 -
    5.42 -lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f"
    5.43 -  apply rule
    5.44 -   apply (rule ext, force split: sum.split)
    5.45 -  by (rule ext, metis case_sum_o_inj(2))
    5.46 -
    5.47 -lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
    5.48 -  by fast
    5.49 -
    5.50 -lemma equiv_proj:
    5.51 -  assumes e: "equiv A R" and m: "z \<in> R"
    5.52 -  shows "(proj R o fst) z = (proj R o snd) z"
    5.53 -proof -
    5.54 -  from m have z: "(fst z, snd z) \<in> R" by auto
    5.55 -  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"
    5.56 -    unfolding equiv_def sym_def trans_def by blast+
    5.57 -  then show ?thesis unfolding proj_def[abs_def] by auto
    5.58 -qed
    5.59 -
    5.60 -(* Operators: *)
    5.61 -definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
    5.62 -
    5.63 -lemma Id_on_Gr: "Id_on A = Gr A id"
    5.64 -  unfolding Id_on_def Gr_def by auto
    5.65 -
    5.66 -lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
    5.67 -  unfolding image2_def by auto
    5.68 -
    5.69 -lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
    5.70 -  by auto
    5.71 -
    5.72 -lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
    5.73 -  unfolding image2_def Gr_def by auto
    5.74 -
    5.75 -lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
    5.76 -  unfolding Gr_def by simp
    5.77 -
    5.78 -lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
    5.79 -  unfolding Gr_def by simp
    5.80 -
    5.81 -lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
    5.82 -  unfolding Gr_def by auto
    5.83 -
    5.84 -lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
    5.85 -  by blast
    5.86 -
    5.87 -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})"
    5.88 -  by blast
    5.89 -
    5.90 -lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X"
    5.91 -  unfolding fun_eq_iff by auto
    5.92 -
    5.93 -lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (split (in_rel Y))"
    5.94 -  by auto
    5.95 -
    5.96 -lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
    5.97 -  by force
    5.98 -
    5.99 -lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
   5.100 -  unfolding fun_eq_iff by auto
   5.101 -
   5.102 -lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)"
   5.103 -  unfolding fun_eq_iff by auto
   5.104 -
   5.105 -lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
   5.106 -  unfolding Gr_def Grp_def fun_eq_iff by auto
   5.107 -
   5.108 -definition relImage where
   5.109 -  "relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
   5.110 -
   5.111 -definition relInvImage where
   5.112 -  "relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
   5.113 -
   5.114 -lemma relImage_Gr:
   5.115 -  "\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
   5.116 -  unfolding relImage_def Gr_def relcomp_def by auto
   5.117 -
   5.118 -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"
   5.119 -  unfolding Gr_def relcomp_def image_def relInvImage_def by auto
   5.120 -
   5.121 -lemma relImage_mono:
   5.122 -  "R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
   5.123 -  unfolding relImage_def by auto
   5.124 -
   5.125 -lemma relInvImage_mono:
   5.126 -  "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
   5.127 -  unfolding relInvImage_def by auto
   5.128 -
   5.129 -lemma relInvImage_Id_on:
   5.130 -  "(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id"
   5.131 -  unfolding relInvImage_def Id_on_def by auto
   5.132 -
   5.133 -lemma relInvImage_UNIV_relImage:
   5.134 -  "R \<subseteq> relInvImage UNIV (relImage R f) f"
   5.135 -  unfolding relInvImage_def relImage_def by auto
   5.136 -
   5.137 -lemma relImage_proj:
   5.138 -  assumes "equiv A R"
   5.139 -  shows "relImage R (proj R) \<subseteq> Id_on (A//R)"
   5.140 -  unfolding relImage_def Id_on_def
   5.141 -  using proj_iff[OF assms] equiv_class_eq_iff[OF assms]
   5.142 -  by (auto simp: proj_preserves)
   5.143 -
   5.144 -lemma relImage_relInvImage:
   5.145 -  assumes "R \<subseteq> f ` A <*> f ` A"
   5.146 -  shows "relImage (relInvImage A R f) f = R"
   5.147 -  using assms unfolding relImage_def relInvImage_def by fast
   5.148 -
   5.149 -lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
   5.150 -  by simp
   5.151 -
   5.152 -lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z" by simp
   5.153 -lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z" by simp
   5.154 -
   5.155 -lemma fst_diag_fst: "fst o ((\<lambda>x. (x, x)) o fst) = fst" by auto
   5.156 -lemma snd_diag_fst: "snd o ((\<lambda>x. (x, x)) o fst) = fst" by auto
   5.157 -lemma fst_diag_snd: "fst o ((\<lambda>x. (x, x)) o snd) = snd" by auto
   5.158 -lemma snd_diag_snd: "snd o ((\<lambda>x. (x, x)) o snd) = snd" by auto
   5.159 -
   5.160 -definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}"
   5.161 -definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}"
   5.162 -definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))"
   5.163 -
   5.164 -lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
   5.165 -  unfolding Shift_def Succ_def by simp
   5.166 -
   5.167 -lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
   5.168 -  unfolding Succ_def by simp
   5.169 -
   5.170 -lemmas SuccE = SuccD[elim_format]
   5.171 -
   5.172 -lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl"
   5.173 -  unfolding Succ_def by simp
   5.174 -
   5.175 -lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl"
   5.176 -  unfolding Shift_def by simp
   5.177 -
   5.178 -lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
   5.179 -  unfolding Succ_def Shift_def by auto
   5.180 -
   5.181 -lemma length_Cons: "length (x # xs) = Suc (length xs)"
   5.182 -  by simp
   5.183 -
   5.184 -lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)"
   5.185 -  by simp
   5.186 -
   5.187 -(*injection into the field of a cardinal*)
   5.188 -definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r"
   5.189 -definition "toCard A r \<equiv> SOME f. toCard_pred A r f"
   5.190 -
   5.191 -lemma ex_toCard_pred:
   5.192 -  "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
   5.193 -  unfolding toCard_pred_def
   5.194 -  using card_of_ordLeq[of A "Field r"]
   5.195 -    ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
   5.196 -  by blast
   5.197 -
   5.198 -lemma toCard_pred_toCard:
   5.199 -  "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)"
   5.200 -  unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
   5.201 -
   5.202 -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"
   5.203 -  using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
   5.204 -
   5.205 -definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k"
   5.206 -
   5.207 -lemma fromCard_toCard:
   5.208 -  "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
   5.209 -  unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
   5.210 -
   5.211 -lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
   5.212 -  unfolding Field_card_of csum_def by auto
   5.213 -
   5.214 -lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
   5.215 -  unfolding Field_card_of csum_def by auto
   5.216 -
   5.217 -lemma rec_nat_0_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
   5.218 -  by auto
   5.219 -
   5.220 -lemma rec_nat_Suc_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
   5.221 -  by auto
   5.222 -
   5.223 -lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
   5.224 -  by auto
   5.225 -
   5.226 -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)"
   5.227 -  by auto
   5.228 -
   5.229 -lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
   5.230 -  by simp
   5.231 -
   5.232 -definition image2p where
   5.233 -  "image2p f g R = (\<lambda>x y. \<exists>x' y'. R x' y' \<and> f x' = x \<and> g y' = y)"
   5.234 -
   5.235 -lemma image2pI: "R x y \<Longrightarrow> image2p f g R (f x) (g y)"
   5.236 -  unfolding image2p_def by blast
   5.237 -
   5.238 -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"
   5.239 -  unfolding image2p_def by blast
   5.240 -
   5.241 -lemma rel_fun_iff_geq_image2p: "rel_fun R S f g = (image2p f g R \<le> S)"
   5.242 -  unfolding rel_fun_def image2p_def by auto
   5.243 -
   5.244 -lemma rel_fun_image2p: "rel_fun R (image2p f g R) f g"
   5.245 -  unfolding rel_fun_def image2p_def by auto
   5.246 -
   5.247 -
   5.248 -subsection {* Equivalence relations, quotients, and Hilbert's choice *}
   5.249 -
   5.250 -lemma equiv_Eps_in:
   5.251 -"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (%x. x \<in> X) \<in> X"
   5.252 -  apply (rule someI2_ex)
   5.253 -  using in_quotient_imp_non_empty by blast
   5.254 -
   5.255 -lemma equiv_Eps_preserves:
   5.256 -  assumes ECH: "equiv A r" and X: "X \<in> A//r"
   5.257 -  shows "Eps (%x. x \<in> X) \<in> A"
   5.258 -  apply (rule in_mono[rule_format])
   5.259 -   using assms apply (rule in_quotient_imp_subset)
   5.260 -  by (rule equiv_Eps_in) (rule assms)+
   5.261 -
   5.262 -lemma proj_Eps:
   5.263 -  assumes "equiv A r" and "X \<in> A//r"
   5.264 -  shows "proj r (Eps (%x. x \<in> X)) = X"
   5.265 -unfolding proj_def
   5.266 -proof auto
   5.267 -  fix x assume x: "x \<in> X"
   5.268 -  thus "(Eps (%x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
   5.269 -next
   5.270 -  fix x assume "(Eps (%x. x \<in> X),x) \<in> r"
   5.271 -  thus "x \<in> X" using in_quotient_imp_closed[OF assms equiv_Eps_in[OF assms]] by fast
   5.272 -qed
   5.273 -
   5.274 -definition univ where "univ f X == f (Eps (%x. x \<in> X))"
   5.275 -
   5.276 -lemma univ_commute:
   5.277 -assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A"
   5.278 -shows "(univ f) (proj r x) = f x"
   5.279 -proof (unfold univ_def)
   5.280 -  have prj: "proj r x \<in> A//r" using x proj_preserves by fast
   5.281 -  hence "Eps (%y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
   5.282 -  moreover have "proj r (Eps (%y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
   5.283 -  ultimately have "(x, Eps (%y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast
   5.284 -  thus "f (Eps (%y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce
   5.285 -qed
   5.286 -
   5.287 -lemma univ_preserves:
   5.288 -  assumes ECH: "equiv A r" and RES: "f respects r" and PRES: "\<forall>x \<in> A. f x \<in> B"
   5.289 -  shows "\<forall>X \<in> A//r. univ f X \<in> B"
   5.290 -proof
   5.291 -  fix X assume "X \<in> A//r"
   5.292 -  then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
   5.293 -  hence "univ f X = f x" using ECH RES univ_commute by fastforce
   5.294 -  thus "univ f X \<in> B" using x PRES by simp
   5.295 -qed
   5.296 -
   5.297 -ML_file "Tools/BNF/bnf_gfp_util.ML"
   5.298 -ML_file "Tools/BNF/bnf_gfp_tactics.ML"
   5.299 -ML_file "Tools/BNF/bnf_gfp.ML"
   5.300 -ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
   5.301 -ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML"
   5.302 -
   5.303 -end
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/BNF_Greatest_Fixpoint.thy	Mon Sep 01 16:34:40 2014 +0200
     6.3 @@ -0,0 +1,300 @@
     6.4 +(*  Title:      HOL/BNF_Greatest_Fixpoint.thy
     6.5 +    Author:     Dmitriy Traytel, TU Muenchen
     6.6 +    Author:     Lorenz Panny, TU Muenchen
     6.7 +    Author:     Jasmin Blanchette, TU Muenchen
     6.8 +    Copyright   2012, 2013, 2014
     6.9 +
    6.10 +Greatest fixed point operation on bounded natural functors.
    6.11 +*)
    6.12 +
    6.13 +header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
    6.14 +
    6.15 +theory BNF_Greatest_Fixpoint
    6.16 +imports BNF_Fixpoint_Base String
    6.17 +keywords
    6.18 +  "codatatype" :: thy_decl and
    6.19 +  "primcorecursive" :: thy_goal and
    6.20 +  "primcorec" :: thy_decl
    6.21 +begin
    6.22 +
    6.23 +setup {*
    6.24 +Sign.const_alias @{binding proj} @{const_name Equiv_Relations.proj}
    6.25 +*}
    6.26 +
    6.27 +lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    6.28 +  by simp
    6.29 +
    6.30 +lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
    6.31 +  by (cases s) auto
    6.32 +
    6.33 +lemma not_TrueE: "\<not> True \<Longrightarrow> P"
    6.34 +  by (erule notE, rule TrueI)
    6.35 +
    6.36 +lemma neq_eq_eq_contradict: "\<lbrakk>t \<noteq> u; s = t; s = u\<rbrakk> \<Longrightarrow> P"
    6.37 +  by fast
    6.38 +
    6.39 +lemma case_sum_expand_Inr: "f o Inl = g \<Longrightarrow> f x = case_sum g (f o Inr) x"
    6.40 +  by (auto split: sum.splits)
    6.41 +
    6.42 +lemma case_sum_expand_Inr': "f o Inl = g \<Longrightarrow> h = f o Inr \<longleftrightarrow> case_sum g h = f"
    6.43 +  apply rule
    6.44 +   apply (rule ext, force split: sum.split)
    6.45 +  by (rule ext, metis case_sum_o_inj(2))
    6.46 +
    6.47 +lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
    6.48 +  by fast
    6.49 +
    6.50 +lemma equiv_proj:
    6.51 +  assumes e: "equiv A R" and m: "z \<in> R"
    6.52 +  shows "(proj R o fst) z = (proj R o snd) z"
    6.53 +proof -
    6.54 +  from m have z: "(fst z, snd z) \<in> R" by auto
    6.55 +  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"
    6.56 +    unfolding equiv_def sym_def trans_def by blast+
    6.57 +  then show ?thesis unfolding proj_def[abs_def] by auto
    6.58 +qed
    6.59 +
    6.60 +(* Operators: *)
    6.61 +definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
    6.62 +
    6.63 +lemma Id_on_Gr: "Id_on A = Gr A id"
    6.64 +  unfolding Id_on_def Gr_def by auto
    6.65 +
    6.66 +lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
    6.67 +  unfolding image2_def by auto
    6.68 +
    6.69 +lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
    6.70 +  by auto
    6.71 +
    6.72 +lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
    6.73 +  unfolding image2_def Gr_def by auto
    6.74 +
    6.75 +lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
    6.76 +  unfolding Gr_def by simp
    6.77 +
    6.78 +lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
    6.79 +  unfolding Gr_def by simp
    6.80 +
    6.81 +lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
    6.82 +  unfolding Gr_def by auto
    6.83 +
    6.84 +lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
    6.85 +  by blast
    6.86 +
    6.87 +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})"
    6.88 +  by blast
    6.89 +
    6.90 +lemma in_rel_Collect_split_eq: "in_rel (Collect (split X)) = X"
    6.91 +  unfolding fun_eq_iff by auto
    6.92 +
    6.93 +lemma Collect_split_in_rel_leI: "X \<subseteq> Y \<Longrightarrow> X \<subseteq> Collect (split (in_rel Y))"
    6.94 +  by auto
    6.95 +
    6.96 +lemma Collect_split_in_rel_leE: "X \<subseteq> Collect (split (in_rel Y)) \<Longrightarrow> (X \<subseteq> Y \<Longrightarrow> R) \<Longrightarrow> R"
    6.97 +  by force
    6.98 +
    6.99 +lemma conversep_in_rel: "(in_rel R)\<inverse>\<inverse> = in_rel (R\<inverse>)"
   6.100 +  unfolding fun_eq_iff by auto
   6.101 +
   6.102 +lemma relcompp_in_rel: "in_rel R OO in_rel S = in_rel (R O S)"
   6.103 +  unfolding fun_eq_iff by auto
   6.104 +
   6.105 +lemma in_rel_Gr: "in_rel (Gr A f) = Grp A f"
   6.106 +  unfolding Gr_def Grp_def fun_eq_iff by auto
   6.107 +
   6.108 +definition relImage where
   6.109 +  "relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
   6.110 +
   6.111 +definition relInvImage where
   6.112 +  "relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
   6.113 +
   6.114 +lemma relImage_Gr:
   6.115 +  "\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
   6.116 +  unfolding relImage_def Gr_def relcomp_def by auto
   6.117 +
   6.118 +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"
   6.119 +  unfolding Gr_def relcomp_def image_def relInvImage_def by auto
   6.120 +
   6.121 +lemma relImage_mono:
   6.122 +  "R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
   6.123 +  unfolding relImage_def by auto
   6.124 +
   6.125 +lemma relInvImage_mono:
   6.126 +  "R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
   6.127 +  unfolding relInvImage_def by auto
   6.128 +
   6.129 +lemma relInvImage_Id_on:
   6.130 +  "(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (Id_on B) f \<subseteq> Id"
   6.131 +  unfolding relInvImage_def Id_on_def by auto
   6.132 +
   6.133 +lemma relInvImage_UNIV_relImage:
   6.134 +  "R \<subseteq> relInvImage UNIV (relImage R f) f"
   6.135 +  unfolding relInvImage_def relImage_def by auto
   6.136 +
   6.137 +lemma relImage_proj:
   6.138 +  assumes "equiv A R"
   6.139 +  shows "relImage R (proj R) \<subseteq> Id_on (A//R)"
   6.140 +  unfolding relImage_def Id_on_def
   6.141 +  using proj_iff[OF assms] equiv_class_eq_iff[OF assms]
   6.142 +  by (auto simp: proj_preserves)
   6.143 +
   6.144 +lemma relImage_relInvImage:
   6.145 +  assumes "R \<subseteq> f ` A <*> f ` A"
   6.146 +  shows "relImage (relInvImage A R f) f = R"
   6.147 +  using assms unfolding relImage_def relInvImage_def by fast
   6.148 +
   6.149 +lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
   6.150 +  by simp
   6.151 +
   6.152 +lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z" by simp
   6.153 +lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z" by simp
   6.154 +
   6.155 +lemma fst_diag_fst: "fst o ((\<lambda>x. (x, x)) o fst) = fst" by auto
   6.156 +lemma snd_diag_fst: "snd o ((\<lambda>x. (x, x)) o fst) = fst" by auto
   6.157 +lemma fst_diag_snd: "fst o ((\<lambda>x. (x, x)) o snd) = snd" by auto
   6.158 +lemma snd_diag_snd: "snd o ((\<lambda>x. (x, x)) o snd) = snd" by auto
   6.159 +
   6.160 +definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}"
   6.161 +definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}"
   6.162 +definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))"
   6.163 +
   6.164 +lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
   6.165 +  unfolding Shift_def Succ_def by simp
   6.166 +
   6.167 +lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
   6.168 +  unfolding Succ_def by simp
   6.169 +
   6.170 +lemmas SuccE = SuccD[elim_format]
   6.171 +
   6.172 +lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl"
   6.173 +  unfolding Succ_def by simp
   6.174 +
   6.175 +lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl"
   6.176 +  unfolding Shift_def by simp
   6.177 +
   6.178 +lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
   6.179 +  unfolding Succ_def Shift_def by auto
   6.180 +
   6.181 +lemma length_Cons: "length (x # xs) = Suc (length xs)"
   6.182 +  by simp
   6.183 +
   6.184 +lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)"
   6.185 +  by simp
   6.186 +
   6.187 +(*injection into the field of a cardinal*)
   6.188 +definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r"
   6.189 +definition "toCard A r \<equiv> SOME f. toCard_pred A r f"
   6.190 +
   6.191 +lemma ex_toCard_pred:
   6.192 +  "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
   6.193 +  unfolding toCard_pred_def
   6.194 +  using card_of_ordLeq[of A "Field r"]
   6.195 +    ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
   6.196 +  by blast
   6.197 +
   6.198 +lemma toCard_pred_toCard:
   6.199 +  "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)"
   6.200 +  unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
   6.201 +
   6.202 +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"
   6.203 +  using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
   6.204 +
   6.205 +definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k"
   6.206 +
   6.207 +lemma fromCard_toCard:
   6.208 +  "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
   6.209 +  unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
   6.210 +
   6.211 +lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
   6.212 +  unfolding Field_card_of csum_def by auto
   6.213 +
   6.214 +lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
   6.215 +  unfolding Field_card_of csum_def by auto
   6.216 +
   6.217 +lemma rec_nat_0_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
   6.218 +  by auto
   6.219 +
   6.220 +lemma rec_nat_Suc_imp: "f = rec_nat f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
   6.221 +  by auto
   6.222 +
   6.223 +lemma rec_list_Nil_imp: "f = rec_list f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
   6.224 +  by auto
   6.225 +
   6.226 +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)"
   6.227 +  by auto
   6.228 +
   6.229 +lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
   6.230 +  by simp
   6.231 +
   6.232 +definition image2p where
   6.233 +  "image2p f g R = (\<lambda>x y. \<exists>x' y'. R x' y' \<and> f x' = x \<and> g y' = y)"
   6.234 +
   6.235 +lemma image2pI: "R x y \<Longrightarrow> image2p f g R (f x) (g y)"
   6.236 +  unfolding image2p_def by blast
   6.237 +
   6.238 +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"
   6.239 +  unfolding image2p_def by blast
   6.240 +
   6.241 +lemma rel_fun_iff_geq_image2p: "rel_fun R S f g = (image2p f g R \<le> S)"
   6.242 +  unfolding rel_fun_def image2p_def by auto
   6.243 +
   6.244 +lemma rel_fun_image2p: "rel_fun R (image2p f g R) f g"
   6.245 +  unfolding rel_fun_def image2p_def by auto
   6.246 +
   6.247 +
   6.248 +subsection {* Equivalence relations, quotients, and Hilbert's choice *}
   6.249 +
   6.250 +lemma equiv_Eps_in:
   6.251 +"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (%x. x \<in> X) \<in> X"
   6.252 +  apply (rule someI2_ex)
   6.253 +  using in_quotient_imp_non_empty by blast
   6.254 +
   6.255 +lemma equiv_Eps_preserves:
   6.256 +  assumes ECH: "equiv A r" and X: "X \<in> A//r"
   6.257 +  shows "Eps (%x. x \<in> X) \<in> A"
   6.258 +  apply (rule in_mono[rule_format])
   6.259 +   using assms apply (rule in_quotient_imp_subset)
   6.260 +  by (rule equiv_Eps_in) (rule assms)+
   6.261 +
   6.262 +lemma proj_Eps:
   6.263 +  assumes "equiv A r" and "X \<in> A//r"
   6.264 +  shows "proj r (Eps (%x. x \<in> X)) = X"
   6.265 +unfolding proj_def
   6.266 +proof auto
   6.267 +  fix x assume x: "x \<in> X"
   6.268 +  thus "(Eps (%x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
   6.269 +next
   6.270 +  fix x assume "(Eps (%x. x \<in> X),x) \<in> r"
   6.271 +  thus "x \<in> X" using in_quotient_imp_closed[OF assms equiv_Eps_in[OF assms]] by fast
   6.272 +qed
   6.273 +
   6.274 +definition univ where "univ f X == f (Eps (%x. x \<in> X))"
   6.275 +
   6.276 +lemma univ_commute:
   6.277 +assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A"
   6.278 +shows "(univ f) (proj r x) = f x"
   6.279 +proof (unfold univ_def)
   6.280 +  have prj: "proj r x \<in> A//r" using x proj_preserves by fast
   6.281 +  hence "Eps (%y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
   6.282 +  moreover have "proj r (Eps (%y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
   6.283 +  ultimately have "(x, Eps (%y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast
   6.284 +  thus "f (Eps (%y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce
   6.285 +qed
   6.286 +
   6.287 +lemma univ_preserves:
   6.288 +  assumes ECH: "equiv A r" and RES: "f respects r" and PRES: "\<forall>x \<in> A. f x \<in> B"
   6.289 +  shows "\<forall>X \<in> A//r. univ f X \<in> B"
   6.290 +proof
   6.291 +  fix X assume "X \<in> A//r"
   6.292 +  then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
   6.293 +  hence "univ f X = f x" using ECH RES univ_commute by fastforce
   6.294 +  thus "univ f X \<in> B" using x PRES by simp
   6.295 +qed
   6.296 +
   6.297 +ML_file "Tools/BNF/bnf_gfp_util.ML"
   6.298 +ML_file "Tools/BNF/bnf_gfp_tactics.ML"
   6.299 +ML_file "Tools/BNF/bnf_gfp.ML"
   6.300 +ML_file "Tools/BNF/bnf_gfp_rec_sugar_tactics.ML"
   6.301 +ML_file "Tools/BNF/bnf_gfp_rec_sugar.ML"
   6.302 +
   6.303 +end
     7.1 --- a/src/HOL/BNF_LFP.thy	Mon Sep 01 16:34:39 2014 +0200
     7.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.3 @@ -1,198 +0,0 @@
     7.4 -(*  Title:      HOL/BNF_LFP.thy
     7.5 -    Author:     Dmitriy Traytel, TU Muenchen
     7.6 -    Author:     Lorenz Panny, TU Muenchen
     7.7 -    Author:     Jasmin Blanchette, TU Muenchen
     7.8 -    Copyright   2012, 2013, 2014
     7.9 -
    7.10 -Least fixed point operation on bounded natural functors.
    7.11 -*)
    7.12 -
    7.13 -header {* Least Fixed Point Operation on Bounded Natural Functors *}
    7.14 -
    7.15 -theory BNF_LFP
    7.16 -imports BNF_FP_Base
    7.17 -keywords
    7.18 -  "datatype_new" :: thy_decl and
    7.19 -  "datatype_compat" :: thy_decl
    7.20 -begin
    7.21 -
    7.22 -lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
    7.23 -  by blast
    7.24 -
    7.25 -lemma image_Collect_subsetI: "(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B"
    7.26 -  by blast
    7.27 -
    7.28 -lemma Collect_restrict: "{x. x \<in> X \<and> P x} \<subseteq> X"
    7.29 -  by auto
    7.30 -
    7.31 -lemma prop_restrict: "\<lbrakk>x \<in> Z; Z \<subseteq> {x. x \<in> X \<and> P x}\<rbrakk> \<Longrightarrow> P x"
    7.32 -  by auto
    7.33 -
    7.34 -lemma underS_I: "\<lbrakk>i \<noteq> j; (i, j) \<in> R\<rbrakk> \<Longrightarrow> i \<in> underS R j"
    7.35 -  unfolding underS_def by simp
    7.36 -
    7.37 -lemma underS_E: "i \<in> underS R j \<Longrightarrow> i \<noteq> j \<and> (i, j) \<in> R"
    7.38 -  unfolding underS_def by simp
    7.39 -
    7.40 -lemma underS_Field: "i \<in> underS R j \<Longrightarrow> i \<in> Field R"
    7.41 -  unfolding underS_def Field_def by auto
    7.42 -
    7.43 -lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
    7.44 -  unfolding Field_def by auto
    7.45 -
    7.46 -lemma fst_convol': "fst (\<langle>f, g\<rangle> x) = f x"
    7.47 -  using fst_convol unfolding convol_def by simp
    7.48 -
    7.49 -lemma snd_convol': "snd (\<langle>f, g\<rangle> x) = g x"
    7.50 -  using snd_convol unfolding convol_def by simp
    7.51 -
    7.52 -lemma convol_expand_snd: "fst o f = g \<Longrightarrow> \<langle>g, snd o f\<rangle> = f"
    7.53 -  unfolding convol_def by auto
    7.54 -
    7.55 -lemma convol_expand_snd':
    7.56 -  assumes "(fst o f = g)"
    7.57 -  shows "h = snd o f \<longleftrightarrow> \<langle>g, h\<rangle> = f"
    7.58 -proof -
    7.59 -  from assms have *: "\<langle>g, snd o f\<rangle> = f" by (rule convol_expand_snd)
    7.60 -  then have "h = snd o f \<longleftrightarrow> h = snd o \<langle>g, snd o f\<rangle>" by simp
    7.61 -  moreover have "\<dots> \<longleftrightarrow> h = snd o f" by (simp add: snd_convol)
    7.62 -  moreover have "\<dots> \<longleftrightarrow> \<langle>g, h\<rangle> = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff)
    7.63 -  ultimately show ?thesis by simp
    7.64 -qed
    7.65 -
    7.66 -lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
    7.67 -  unfolding bij_betw_def by auto
    7.68 -
    7.69 -lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B"
    7.70 -  unfolding bij_betw_def by auto
    7.71 -
    7.72 -lemma f_the_inv_into_f_bij_betw: "bij_betw f A B \<Longrightarrow>
    7.73 -  (bij_betw f A B \<Longrightarrow> x \<in> B) \<Longrightarrow> f (the_inv_into A f x) = x"
    7.74 -  unfolding bij_betw_def by (blast intro: f_the_inv_into_f)
    7.75 -
    7.76 -lemma ex_bij_betw: "|A| \<le>o (r :: 'b rel) \<Longrightarrow> \<exists>f B :: 'b set. bij_betw f B A"
    7.77 -  by (subst (asm) internalize_card_of_ordLeq)
    7.78 -    (auto dest!: iffD2[OF card_of_ordIso ordIso_symmetric])
    7.79 -
    7.80 -lemma bij_betwI':
    7.81 -  "\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y);
    7.82 -    \<And>x. x \<in> X \<Longrightarrow> f x \<in> Y;
    7.83 -    \<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> bij_betw f X Y"
    7.84 -  unfolding bij_betw_def inj_on_def by blast
    7.85 -
    7.86 -lemma surj_fun_eq:
    7.87 -  assumes surj_on: "f ` X = UNIV" and eq_on: "\<forall>x \<in> X. (g1 o f) x = (g2 o f) x"
    7.88 -  shows "g1 = g2"
    7.89 -proof (rule ext)
    7.90 -  fix y
    7.91 -  from surj_on obtain x where "x \<in> X" and "y = f x" by blast
    7.92 -  thus "g1 y = g2 y" using eq_on by simp
    7.93 -qed
    7.94 -
    7.95 -lemma Card_order_wo_rel: "Card_order r \<Longrightarrow> wo_rel r"
    7.96 -unfolding wo_rel_def card_order_on_def by blast
    7.97 -
    7.98 -lemma Cinfinite_limit: "\<lbrakk>x \<in> Field r; Cinfinite r\<rbrakk> \<Longrightarrow>
    7.99 -  \<exists>y \<in> Field r. x \<noteq> y \<and> (x, y) \<in> r"
   7.100 -unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit)
   7.101 -
   7.102 -lemma Card_order_trans:
   7.103 -  "\<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"
   7.104 -unfolding card_order_on_def well_order_on_def linear_order_on_def
   7.105 -  partial_order_on_def preorder_on_def trans_def antisym_def by blast
   7.106 -
   7.107 -lemma Cinfinite_limit2:
   7.108 - assumes x1: "x1 \<in> Field r" and x2: "x2 \<in> Field r" and r: "Cinfinite r"
   7.109 - shows "\<exists>y \<in> Field r. (x1 \<noteq> y \<and> (x1, y) \<in> r) \<and> (x2 \<noteq> y \<and> (x2, y) \<in> r)"
   7.110 -proof -
   7.111 -  from r have trans: "trans r" and total: "Total r" and antisym: "antisym r"
   7.112 -    unfolding card_order_on_def well_order_on_def linear_order_on_def
   7.113 -      partial_order_on_def preorder_on_def by auto
   7.114 -  obtain y1 where y1: "y1 \<in> Field r" "x1 \<noteq> y1" "(x1, y1) \<in> r"
   7.115 -    using Cinfinite_limit[OF x1 r] by blast
   7.116 -  obtain y2 where y2: "y2 \<in> Field r" "x2 \<noteq> y2" "(x2, y2) \<in> r"
   7.117 -    using Cinfinite_limit[OF x2 r] by blast
   7.118 -  show ?thesis
   7.119 -  proof (cases "y1 = y2")
   7.120 -    case True with y1 y2 show ?thesis by blast
   7.121 -  next
   7.122 -    case False
   7.123 -    with y1(1) y2(1) total have "(y1, y2) \<in> r \<or> (y2, y1) \<in> r"
   7.124 -      unfolding total_on_def by auto
   7.125 -    thus ?thesis
   7.126 -    proof
   7.127 -      assume *: "(y1, y2) \<in> r"
   7.128 -      with trans y1(3) have "(x1, y2) \<in> r" unfolding trans_def by blast
   7.129 -      with False y1 y2 * antisym show ?thesis by (cases "x1 = y2") (auto simp: antisym_def)
   7.130 -    next
   7.131 -      assume *: "(y2, y1) \<in> r"
   7.132 -      with trans y2(3) have "(x2, y1) \<in> r" unfolding trans_def by blast
   7.133 -      with False y1 y2 * antisym show ?thesis by (cases "x2 = y1") (auto simp: antisym_def)
   7.134 -    qed
   7.135 -  qed
   7.136 -qed
   7.137 -
   7.138 -lemma Cinfinite_limit_finite: "\<lbrakk>finite X; X \<subseteq> Field r; Cinfinite r\<rbrakk>
   7.139 - \<Longrightarrow> \<exists>y \<in> Field r. \<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)"
   7.140 -proof (induct X rule: finite_induct)
   7.141 -  case empty thus ?case unfolding cinfinite_def using ex_in_conv[of "Field r"] finite.emptyI by auto
   7.142 -next
   7.143 -  case (insert x X)
   7.144 -  then obtain y where y: "y \<in> Field r" "\<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)" by blast
   7.145 -  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"
   7.146 -    using Cinfinite_limit2[OF _ y(1) insert(5), of x] insert(4) by blast
   7.147 -  show ?case
   7.148 -    apply (intro bexI ballI)
   7.149 -    apply (erule insertE)
   7.150 -    apply hypsubst
   7.151 -    apply (rule z(2))
   7.152 -    using Card_order_trans[OF insert(5)[THEN conjunct2]] y(2) z(3)
   7.153 -    apply blast
   7.154 -    apply (rule z(1))
   7.155 -    done
   7.156 -qed
   7.157 -
   7.158 -lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A"
   7.159 -by auto
   7.160 -
   7.161 -(*helps resolution*)
   7.162 -lemma well_order_induct_imp:
   7.163 -  "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>
   7.164 -     x \<in> Field r \<longrightarrow> P x"
   7.165 -by (erule wo_rel.well_order_induct)
   7.166 -
   7.167 -lemma meta_spec2:
   7.168 -  assumes "(\<And>x y. PROP P x y)"
   7.169 -  shows "PROP P x y"
   7.170 -by (rule assms)
   7.171 -
   7.172 -lemma nchotomy_relcomppE:
   7.173 -  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"
   7.174 -  shows P
   7.175 -proof (rule relcompp.cases[OF assms(2)], hypsubst)
   7.176 -  fix b assume "r a b" "s b c"
   7.177 -  moreover from assms(1) obtain b' where "b = f b'" by blast
   7.178 -  ultimately show P by (blast intro: assms(3))
   7.179 -qed
   7.180 -
   7.181 -lemma vimage2p_rel_fun: "rel_fun (vimage2p f g R) R f g"
   7.182 -  unfolding rel_fun_def vimage2p_def by auto
   7.183 -
   7.184 -lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
   7.185 -  unfolding vimage2p_def by auto
   7.186 -
   7.187 -lemma id_transfer: "rel_fun A A id id"
   7.188 -  unfolding rel_fun_def by simp
   7.189 -
   7.190 -lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
   7.191 -  by (rule ssubst)
   7.192 -
   7.193 -ML_file "Tools/BNF/bnf_lfp_util.ML"
   7.194 -ML_file "Tools/BNF/bnf_lfp_tactics.ML"
   7.195 -ML_file "Tools/BNF/bnf_lfp.ML"
   7.196 -ML_file "Tools/BNF/bnf_lfp_compat.ML"
   7.197 -ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
   7.198 -
   7.199 -hide_fact (open) id_transfer
   7.200 -
   7.201 -end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/BNF_Least_Fixpoint.thy	Mon Sep 01 16:34:40 2014 +0200
     8.3 @@ -0,0 +1,198 @@
     8.4 +(*  Title:      HOL/BNF_Least_Fixpoint.thy
     8.5 +    Author:     Dmitriy Traytel, TU Muenchen
     8.6 +    Author:     Lorenz Panny, TU Muenchen
     8.7 +    Author:     Jasmin Blanchette, TU Muenchen
     8.8 +    Copyright   2012, 2013, 2014
     8.9 +
    8.10 +Least fixed point operation on bounded natural functors.
    8.11 +*)
    8.12 +
    8.13 +header {* Least Fixed Point Operation on Bounded Natural Functors *}
    8.14 +
    8.15 +theory BNF_Least_Fixpoint
    8.16 +imports BNF_Fixpoint_Base
    8.17 +keywords
    8.18 +  "datatype_new" :: thy_decl and
    8.19 +  "datatype_compat" :: thy_decl
    8.20 +begin
    8.21 +
    8.22 +lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
    8.23 +  by blast
    8.24 +
    8.25 +lemma image_Collect_subsetI: "(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B"
    8.26 +  by blast
    8.27 +
    8.28 +lemma Collect_restrict: "{x. x \<in> X \<and> P x} \<subseteq> X"
    8.29 +  by auto
    8.30 +
    8.31 +lemma prop_restrict: "\<lbrakk>x \<in> Z; Z \<subseteq> {x. x \<in> X \<and> P x}\<rbrakk> \<Longrightarrow> P x"
    8.32 +  by auto
    8.33 +
    8.34 +lemma underS_I: "\<lbrakk>i \<noteq> j; (i, j) \<in> R\<rbrakk> \<Longrightarrow> i \<in> underS R j"
    8.35 +  unfolding underS_def by simp
    8.36 +
    8.37 +lemma underS_E: "i \<in> underS R j \<Longrightarrow> i \<noteq> j \<and> (i, j) \<in> R"
    8.38 +  unfolding underS_def by simp
    8.39 +
    8.40 +lemma underS_Field: "i \<in> underS R j \<Longrightarrow> i \<in> Field R"
    8.41 +  unfolding underS_def Field_def by auto
    8.42 +
    8.43 +lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
    8.44 +  unfolding Field_def by auto
    8.45 +
    8.46 +lemma fst_convol': "fst (\<langle>f, g\<rangle> x) = f x"
    8.47 +  using fst_convol unfolding convol_def by simp
    8.48 +
    8.49 +lemma snd_convol': "snd (\<langle>f, g\<rangle> x) = g x"
    8.50 +  using snd_convol unfolding convol_def by simp
    8.51 +
    8.52 +lemma convol_expand_snd: "fst o f = g \<Longrightarrow> \<langle>g, snd o f\<rangle> = f"
    8.53 +  unfolding convol_def by auto
    8.54 +
    8.55 +lemma convol_expand_snd':
    8.56 +  assumes "(fst o f = g)"
    8.57 +  shows "h = snd o f \<longleftrightarrow> \<langle>g, h\<rangle> = f"
    8.58 +proof -
    8.59 +  from assms have *: "\<langle>g, snd o f\<rangle> = f" by (rule convol_expand_snd)
    8.60 +  then have "h = snd o f \<longleftrightarrow> h = snd o \<langle>g, snd o f\<rangle>" by simp
    8.61 +  moreover have "\<dots> \<longleftrightarrow> h = snd o f" by (simp add: snd_convol)
    8.62 +  moreover have "\<dots> \<longleftrightarrow> \<langle>g, h\<rangle> = f" by (subst (2) *[symmetric]) (auto simp: convol_def fun_eq_iff)
    8.63 +  ultimately show ?thesis by simp
    8.64 +qed
    8.65 +
    8.66 +lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
    8.67 +  unfolding bij_betw_def by auto
    8.68 +
    8.69 +lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B"
    8.70 +  unfolding bij_betw_def by auto
    8.71 +
    8.72 +lemma f_the_inv_into_f_bij_betw: "bij_betw f A B \<Longrightarrow>
    8.73 +  (bij_betw f A B \<Longrightarrow> x \<in> B) \<Longrightarrow> f (the_inv_into A f x) = x"
    8.74 +  unfolding bij_betw_def by (blast intro: f_the_inv_into_f)
    8.75 +
    8.76 +lemma ex_bij_betw: "|A| \<le>o (r :: 'b rel) \<Longrightarrow> \<exists>f B :: 'b set. bij_betw f B A"
    8.77 +  by (subst (asm) internalize_card_of_ordLeq)
    8.78 +    (auto dest!: iffD2[OF card_of_ordIso ordIso_symmetric])
    8.79 +
    8.80 +lemma bij_betwI':
    8.81 +  "\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y);
    8.82 +    \<And>x. x \<in> X \<Longrightarrow> f x \<in> Y;
    8.83 +    \<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> bij_betw f X Y"
    8.84 +  unfolding bij_betw_def inj_on_def by blast
    8.85 +
    8.86 +lemma surj_fun_eq:
    8.87 +  assumes surj_on: "f ` X = UNIV" and eq_on: "\<forall>x \<in> X. (g1 o f) x = (g2 o f) x"
    8.88 +  shows "g1 = g2"
    8.89 +proof (rule ext)
    8.90 +  fix y
    8.91 +  from surj_on obtain x where "x \<in> X" and "y = f x" by blast
    8.92 +  thus "g1 y = g2 y" using eq_on by simp
    8.93 +qed
    8.94 +
    8.95 +lemma Card_order_wo_rel: "Card_order r \<Longrightarrow> wo_rel r"
    8.96 +unfolding wo_rel_def card_order_on_def by blast
    8.97 +
    8.98 +lemma Cinfinite_limit: "\<lbrakk>x \<in> Field r; Cinfinite r\<rbrakk> \<Longrightarrow>
    8.99 +  \<exists>y \<in> Field r. x \<noteq> y \<and> (x, y) \<in> r"
   8.100 +unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit)
   8.101 +
   8.102 +lemma Card_order_trans:
   8.103 +  "\<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"
   8.104 +unfolding card_order_on_def well_order_on_def linear_order_on_def
   8.105 +  partial_order_on_def preorder_on_def trans_def antisym_def by blast
   8.106 +
   8.107 +lemma Cinfinite_limit2:
   8.108 + assumes x1: "x1 \<in> Field r" and x2: "x2 \<in> Field r" and r: "Cinfinite r"
   8.109 + shows "\<exists>y \<in> Field r. (x1 \<noteq> y \<and> (x1, y) \<in> r) \<and> (x2 \<noteq> y \<and> (x2, y) \<in> r)"
   8.110 +proof -
   8.111 +  from r have trans: "trans r" and total: "Total r" and antisym: "antisym r"
   8.112 +    unfolding card_order_on_def well_order_on_def linear_order_on_def
   8.113 +      partial_order_on_def preorder_on_def by auto
   8.114 +  obtain y1 where y1: "y1 \<in> Field r" "x1 \<noteq> y1" "(x1, y1) \<in> r"
   8.115 +    using Cinfinite_limit[OF x1 r] by blast
   8.116 +  obtain y2 where y2: "y2 \<in> Field r" "x2 \<noteq> y2" "(x2, y2) \<in> r"
   8.117 +    using Cinfinite_limit[OF x2 r] by blast
   8.118 +  show ?thesis
   8.119 +  proof (cases "y1 = y2")
   8.120 +    case True with y1 y2 show ?thesis by blast
   8.121 +  next
   8.122 +    case False
   8.123 +    with y1(1) y2(1) total have "(y1, y2) \<in> r \<or> (y2, y1) \<in> r"
   8.124 +      unfolding total_on_def by auto
   8.125 +    thus ?thesis
   8.126 +    proof
   8.127 +      assume *: "(y1, y2) \<in> r"
   8.128 +      with trans y1(3) have "(x1, y2) \<in> r" unfolding trans_def by blast
   8.129 +      with False y1 y2 * antisym show ?thesis by (cases "x1 = y2") (auto simp: antisym_def)
   8.130 +    next
   8.131 +      assume *: "(y2, y1) \<in> r"
   8.132 +      with trans y2(3) have "(x2, y1) \<in> r" unfolding trans_def by blast
   8.133 +      with False y1 y2 * antisym show ?thesis by (cases "x2 = y1") (auto simp: antisym_def)
   8.134 +    qed
   8.135 +  qed
   8.136 +qed
   8.137 +
   8.138 +lemma Cinfinite_limit_finite: "\<lbrakk>finite X; X \<subseteq> Field r; Cinfinite r\<rbrakk>
   8.139 + \<Longrightarrow> \<exists>y \<in> Field r. \<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)"
   8.140 +proof (induct X rule: finite_induct)
   8.141 +  case empty thus ?case unfolding cinfinite_def using ex_in_conv[of "Field r"] finite.emptyI by auto
   8.142 +next
   8.143 +  case (insert x X)
   8.144 +  then obtain y where y: "y \<in> Field r" "\<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)" by blast
   8.145 +  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"
   8.146 +    using Cinfinite_limit2[OF _ y(1) insert(5), of x] insert(4) by blast
   8.147 +  show ?case
   8.148 +    apply (intro bexI ballI)
   8.149 +    apply (erule insertE)
   8.150 +    apply hypsubst
   8.151 +    apply (rule z(2))
   8.152 +    using Card_order_trans[OF insert(5)[THEN conjunct2]] y(2) z(3)
   8.153 +    apply blast
   8.154 +    apply (rule z(1))
   8.155 +    done
   8.156 +qed
   8.157 +
   8.158 +lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A"
   8.159 +by auto
   8.160 +
   8.161 +(*helps resolution*)
   8.162 +lemma well_order_induct_imp:
   8.163 +  "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>
   8.164 +     x \<in> Field r \<longrightarrow> P x"
   8.165 +by (erule wo_rel.well_order_induct)
   8.166 +
   8.167 +lemma meta_spec2:
   8.168 +  assumes "(\<And>x y. PROP P x y)"
   8.169 +  shows "PROP P x y"
   8.170 +by (rule assms)
   8.171 +
   8.172 +lemma nchotomy_relcomppE:
   8.173 +  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"
   8.174 +  shows P
   8.175 +proof (rule relcompp.cases[OF assms(2)], hypsubst)
   8.176 +  fix b assume "r a b" "s b c"
   8.177 +  moreover from assms(1) obtain b' where "b = f b'" by blast
   8.178 +  ultimately show P by (blast intro: assms(3))
   8.179 +qed
   8.180 +
   8.181 +lemma vimage2p_rel_fun: "rel_fun (vimage2p f g R) R f g"
   8.182 +  unfolding rel_fun_def vimage2p_def by auto
   8.183 +
   8.184 +lemma predicate2D_vimage2p: "\<lbrakk>R \<le> vimage2p f g S; R x y\<rbrakk> \<Longrightarrow> S (f x) (g y)"
   8.185 +  unfolding vimage2p_def by auto
   8.186 +
   8.187 +lemma id_transfer: "rel_fun A A id id"
   8.188 +  unfolding rel_fun_def by simp
   8.189 +
   8.190 +lemma ssubst_Pair_rhs: "\<lbrakk>(r, s) \<in> R; s' = s\<rbrakk> \<Longrightarrow> (r, s') \<in> R"
   8.191 +  by (rule ssubst)
   8.192 +
   8.193 +ML_file "Tools/BNF/bnf_lfp_util.ML"
   8.194 +ML_file "Tools/BNF/bnf_lfp_tactics.ML"
   8.195 +ML_file "Tools/BNF/bnf_lfp.ML"
   8.196 +ML_file "Tools/BNF/bnf_lfp_compat.ML"
   8.197 +ML_file "Tools/BNF/bnf_lfp_rec_sugar_more.ML"
   8.198 +
   8.199 +hide_fact (open) id_transfer
   8.200 +
   8.201 +end
     9.1 --- a/src/HOL/Main.thy	Mon Sep 01 16:34:39 2014 +0200
     9.2 +++ b/src/HOL/Main.thy	Mon Sep 01 16:34:40 2014 +0200
     9.3 @@ -1,7 +1,8 @@
     9.4  header {* Main HOL *}
     9.5  
     9.6  theory Main
     9.7 -imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick BNF_GFP
     9.8 +imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick
     9.9 +  BNF_Greatest_Fixpoint
    9.10  begin
    9.11  
    9.12  text {*
    10.1 --- a/src/HOL/Num.thy	Mon Sep 01 16:34:39 2014 +0200
    10.2 +++ b/src/HOL/Num.thy	Mon Sep 01 16:34:40 2014 +0200
    10.3 @@ -6,7 +6,7 @@
    10.4  header {* Binary Numerals *}
    10.5  
    10.6  theory Num
    10.7 -imports Old_Datatype BNF_LFP
    10.8 +imports BNF_Least_Fixpoint Old_Datatype
    10.9  begin
   10.10  
   10.11  subsection {* The @{text num} type *}
    11.1 --- a/src/HOL/Option.thy	Mon Sep 01 16:34:39 2014 +0200
    11.2 +++ b/src/HOL/Option.thy	Mon Sep 01 16:34:40 2014 +0200
    11.3 @@ -5,7 +5,7 @@
    11.4  header {* Datatype option *}
    11.5  
    11.6  theory Option
    11.7 -imports BNF_LFP Old_Datatype Finite_Set
    11.8 +imports BNF_Least_Fixpoint Old_Datatype Finite_Set
    11.9  begin
   11.10  
   11.11  datatype_new 'a option =
    12.1 --- a/src/HOL/Tools/BNF/bnf_comp.ML	Mon Sep 01 16:34:39 2014 +0200
    12.2 +++ b/src/HOL/Tools/BNF/bnf_comp.ML	Mon Sep 01 16:34:40 2014 +0200
    12.3 @@ -54,8 +54,8 @@
    12.4  open BNF_Tactics
    12.5  open BNF_Comp_Tactics
    12.6  
    12.7 -val ID_bnf = the (bnf_of @{context} "BNF_Comp.ID");
    12.8 -val DEADID_bnf = the (bnf_of @{context} "BNF_Comp.DEADID");
    12.9 +val ID_bnf = the (bnf_of @{context} "BNF_Composition.ID");
   12.10 +val DEADID_bnf = the (bnf_of @{context} "BNF_Composition.DEADID");
   12.11  
   12.12  type comp_cache = (bnf * (typ list * typ list)) Typtab.table;
   12.13  
    13.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Sep 01 16:34:39 2014 +0200
    13.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Sep 01 16:34:40 2014 +0200
    13.3 @@ -289,9 +289,9 @@
    13.4            REPEAT_DETERM o etac conjE))) 1 THEN
    13.5        unfold_thms_tac ctxt ((discs RL [eqTrueI, eqFalseI]) @ sels @ simp_thms') THEN
    13.6        unfold_thms_tac ctxt (dtor_ctor :: rel_pre_def :: abs_inverse :: ctor_inject ::
    13.7 -        abs_inject :: ctor_defs @ nesting_rel_eqs @ simp_thms' @ @{thms BNF_Comp.id_bnf_comp_def
    13.8 -        rel_sum_simps rel_prod_apply vimage2p_def Inl_Inr_False iffD2[OF eq_False Inr_not_Inl]
    13.9 -        sum.inject prod.inject}) THEN
   13.10 +        abs_inject :: ctor_defs @ nesting_rel_eqs @ simp_thms' @
   13.11 +        @{thms BNF_Composition.id_bnf_comp_def rel_sum_simps rel_prod_apply vimage2p_def
   13.12 +        Inl_Inr_False iffD2[OF eq_False Inr_not_Inl] sum.inject prod.inject}) THEN
   13.13        REPEAT_DETERM (HEADGOAL ((REPEAT_DETERM o etac conjE) THEN' (REPEAT_DETERM o rtac conjI) THEN'
   13.14          (rtac refl ORELSE' atac))))
   13.15      cts assms exhausts discss selss ctor_defss dtor_ctors ctor_injects abs_injects rel_pre_defs
   13.16 @@ -305,7 +305,7 @@
   13.17            (rtac (cterm_instantiate_pos (replicate 4 NONE @ [SOME cterm]) @{thm arg_cong2} RS iffD2)
   13.18              THEN' atac THEN' atac THEN' TRY o resolve_tac assms))) THEN
   13.19          unfold_thms_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
   13.20 -          @{thms BNF_Comp.id_bnf_comp_def vimage2p_def}) THEN
   13.21 +          @{thms BNF_Composition.id_bnf_comp_def vimage2p_def}) THEN
   13.22          TRYALL (hyp_subst_tac ctxt) THEN
   13.23          unfold_thms_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
   13.24            Inr_Inl_False  sum.inject prod.inject}) THEN
   13.25 @@ -354,7 +354,7 @@
   13.26      Abs_pre_inverses =
   13.27    let
   13.28      val assms_ctor_defs =
   13.29 -      map (unfold_thms ctxt (@{thm BNF_Comp.id_bnf_comp_def} :: ctor_defs)) assms;
   13.30 +      map (unfold_thms ctxt (@{thm BNF_Composition.id_bnf_comp_def} :: ctor_defs)) assms;
   13.31      val exhausts' = map (fn thm => thm RS @{thm asm_rl[of "P x y" for P x y]}) exhausts
   13.32        |> map2 (fn ct => cterm_instantiate_pos [NONE, SOME ct]) cts;
   13.33    in
   13.34 @@ -364,7 +364,7 @@
   13.35           cterm_instantiate_pos (replicate 4 NONE @ [SOME ct]) @{thm arg_cong2} RS iffD2) cts)
   13.36          THEN' atac THEN' hyp_subst_tac ctxt)) THEN
   13.37      unfold_thms_tac ctxt (Abs_pre_inverses @ dtor_ctors @ set_pre_defs @ ctor_defs @
   13.38 -      @{thms BNF_Comp.id_bnf_comp_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert
   13.39 +      @{thms BNF_Composition.id_bnf_comp_def o_apply sum_set_simps prod_set_simps UN_empty UN_insert
   13.40          Un_empty_left Un_empty_right empty_iff singleton_iff}) THEN
   13.41      REPEAT_DETERM (HEADGOAL
   13.42        (TRY o etac UnE THEN' TRY o etac @{thm singletonE} THEN' TRY o hyp_subst_tac ctxt THEN'
    14.1 --- a/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Sep 01 16:34:39 2014 +0200
    14.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML	Mon Sep 01 16:34:40 2014 +0200
    14.3 @@ -65,7 +65,7 @@
    14.4  
    14.5  val rec_o_map_simp_thms =
    14.6    @{thms o_def[abs_def] id_def case_prod_app case_sum_map_sum case_prod_map_prod
    14.7 -      BNF_Comp.id_bnf_comp_def};
    14.8 +      BNF_Composition.id_bnf_comp_def};
    14.9  
   14.10  fun mk_rec_o_map_tac ctxt rec_def pre_map_defs live_nesting_map_ident0s abs_inverses
   14.11      ctor_rec_o_map =
    15.1 --- a/src/HOL/Transfer.thy	Mon Sep 01 16:34:39 2014 +0200
    15.2 +++ b/src/HOL/Transfer.thy	Mon Sep 01 16:34:40 2014 +0200
    15.3 @@ -6,7 +6,7 @@
    15.4  header {* Generic theorem transfer using relations *}
    15.5  
    15.6  theory Transfer
    15.7 -imports Hilbert_Choice BNF_FP_Base Metis Option
    15.8 +imports Hilbert_Choice Metis Option
    15.9  begin
   15.10  
   15.11  (* We include Option here although it's not needed here.