--- a/src/HOL/Codatatype/BNF_Def.thy Tue Sep 11 19:43:06 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Def.thy Tue Sep 11 19:45:12 2012 +0200
@@ -8,14 +8,12 @@
header {* Definition of Bounded Natural Functors *}
theory BNF_Def
-imports BNF_Library
+imports BNF_Util
keywords
- "print_bnfs" :: diag
-and
+ "print_bnfs" :: diag and
"bnf_def" :: thy_goal
uses
- "Tools/bnf_util.ML"
- "Tools/bnf_tactics.ML"
+ "Tools/bnf_def_tactics.ML"
"Tools/bnf_def.ML"
begin
--- a/src/HOL/Codatatype/BNF_Library.thy Tue Sep 11 19:43:06 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,849 +0,0 @@
-(* Title: HOL/Codatatype/BNF_Library.thy
- Author: Dmitriy Traytel, TU Muenchen
- Copyright 2012
-
-Library for bounded natural functors.
-*)
-
-header {* Library for Bounded Natural Functors *}
-
-theory BNF_Library
-imports
- "../Ordinals_and_Cardinals/Cardinal_Arithmetic"
- "~~/src/HOL/Library/Prefix_Order"
- Equiv_Relations_More
-begin
-
-lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
-by (erule iffI) (erule contrapos_pn)
-
-lemma all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()" by simp
-
-lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))" by clarsimp
-
-lemma False_imp_eq: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
-by presburger
-
-lemma case_unit: "(case u of () => f) = f"
-by (cases u) (hypsubst, rule unit.cases)
-
-lemma All_point_1: "(\<And>z. z = b \<Longrightarrow> phi z) \<equiv> Trueprop (phi b)"
-by presburger
-
-lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
-by blast
-
-lemma subset_CollectI: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> Q x \<Longrightarrow> P x) \<Longrightarrow> ({x \<in> B. Q x} \<subseteq> {x \<in> A. P x})"
-by blast
-
-lemma mem_Collect_eq_split: "{(x, y). (x, y) \<in> X} = X"
-by simp
-
-lemma image_comp: "image (f o g) = image f o image g"
-by (rule ext) (auto simp only: o_apply image_def)
-
-lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})"
-by (rule ext) simp
-
-lemma Union_natural: "Union o image (image f) = image f o Union"
-by (rule ext) (auto simp only: o_apply)
-
-lemma in_Union_o_assoc: "x \<in> (Union o gset o gmap) A \<Longrightarrow> x \<in> (Union o (gset o gmap)) A"
-by (unfold o_assoc)
-
-lemma comp_single_set_bd:
- assumes fbd_Card_order: "Card_order fbd" and
- fset_bd: "\<And>x. |fset x| \<le>o fbd" and
- gset_bd: "\<And>x. |gset x| \<le>o gbd"
- shows "|\<Union>fset ` gset x| \<le>o gbd *c fbd"
-apply (subst sym[OF SUP_def])
-apply (rule ordLeq_transitive)
-apply (rule card_of_UNION_Sigma)
-apply (subst SIGMA_CSUM)
-apply (rule ordLeq_transitive)
-apply (rule card_of_Csum_Times')
-apply (rule fbd_Card_order)
-apply (rule ballI)
-apply (rule fset_bd)
-apply (rule ordLeq_transitive)
-apply (rule cprod_mono1)
-apply (rule gset_bd)
-apply (rule ordIso_imp_ordLeq)
-apply (rule ordIso_refl)
-apply (rule Card_order_cprod)
-done
-
-lemma Union_image_insert: "\<Union>f ` insert a B = f a \<union> \<Union>f ` B"
-by simp
-
-lemma Union_image_empty: "A \<union> \<Union>f ` {} = A"
-by simp
-
-definition collect where
- "collect F x = (\<Union>f \<in> F. f x)"
-
-lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
-by (rule ext) (auto simp only: o_apply collect_def)
-
-lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F"
-by (rule ext) (auto simp add: collect_def)
-
-lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})"
-by blast
-
-lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
-by blast
-
-lemma rev_bspec: "a \<in> A \<Longrightarrow> \<forall>z \<in> A. P z \<Longrightarrow> P a"
-by simp
-
-lemma Un_cong: "\<lbrakk>A = B; C = D\<rbrakk> \<Longrightarrow> A \<union> C = B \<union> D"
-by simp
-
-lemma UN_image_subset: "\<Union>f ` g x \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
-by blast
-
-lemma image_Collect_subsetI:
- "(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B"
-by blast
-
-lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>(\<lambda>f. f x) ` X| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
-by (unfold o_apply collect_def SUP_def)
-
-lemma sum_case_comp_Inl:
-"sum_case f g \<circ> Inl = f"
-unfolding comp_def by simp
-
-lemma sum_case_expand_Inr: "f o Inl = g \<Longrightarrow> f x = sum_case g (f o Inr) x"
-by (auto split: sum.splits)
-
-lemma converse_mono:
-"R1 ^-1 \<subseteq> R2 ^-1 \<longleftrightarrow> R1 \<subseteq> R2"
-unfolding converse_def by auto
-
-lemma converse_shift:
-"R1 \<subseteq> R2 ^-1 \<Longrightarrow> R1 ^-1 \<subseteq> R2"
-unfolding converse_def by auto
-
-lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
-by auto
-
-lemma equiv_triv1:
-assumes "equiv A R" and "(a, b) \<in> R" and "(a, c) \<in> R"
-shows "(b, c) \<in> R"
-using assms unfolding equiv_def sym_def trans_def by blast
-
-lemma equiv_triv2:
-assumes "equiv A R" and "(a, b) \<in> R" and "(b, c) \<in> R"
-shows "(a, c) \<in> R"
-using assms unfolding equiv_def trans_def by blast
-
-lemma equiv_proj:
- assumes e: "equiv A R" and "z \<in> R"
- shows "(proj R o fst) z = (proj R o snd) z"
-proof -
- from assms(2) have z: "(fst z, snd z) \<in> R" by auto
- have P: "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" by (erule equiv_triv1[OF e z])
- have "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R" by (erule equiv_triv2[OF e z])
- with P show ?thesis unfolding proj_def[abs_def] by auto
-qed
-
-
-section{* Weak pullbacks: *}
-
-definition csquare where
-"csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))"
-
-definition wpull where
-"wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow>
- (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow> (\<exists> a \<in> A. p1 a = b1 \<and> p2 a = b2))"
-
-lemma wpull_cong:
-"\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2"
-by simp
-
-lemma wpull_id: "wpull UNIV B1 B2 id id id id"
-unfolding wpull_def by simp
-
-
-(* Weak pseudo-pullbacks *)
-
-definition wppull where
-"wppull A B1 B2 f1 f2 e1 e2 p1 p2 \<longleftrightarrow>
- (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow>
- (\<exists> a \<in> A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2))"
-
-
-(* The pullback of sets *)
-definition thePull where
-"thePull B1 B2 f1 f2 = {(b1,b2). b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2}"
-
-lemma wpull_thePull:
-"wpull (thePull B1 B2 f1 f2) B1 B2 f1 f2 fst snd"
-unfolding wpull_def thePull_def by auto
-
-lemma wppull_thePull:
-assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
-shows
-"\<exists> j. \<forall> a' \<in> thePull B1 B2 f1 f2.
- j a' \<in> A \<and>
- e1 (p1 (j a')) = e1 (fst a') \<and> e2 (p2 (j a')) = e2 (snd a')"
-(is "\<exists> j. \<forall> a' \<in> ?A'. ?phi a' (j a')")
-proof(rule bchoice[of ?A' ?phi], default)
- fix a' assume a': "a' \<in> ?A'"
- hence "fst a' \<in> B1" unfolding thePull_def by auto
- moreover
- from a' have "snd a' \<in> B2" unfolding thePull_def by auto
- moreover have "f1 (fst a') = f2 (snd a')"
- using a' unfolding csquare_def thePull_def by auto
- ultimately show "\<exists> ja'. ?phi a' ja'"
- using assms unfolding wppull_def by auto
-qed
-
-lemma wpull_wppull:
-assumes wp: "wpull A' B1 B2 f1 f2 p1' p2'" and
-1: "\<forall> a' \<in> A'. j a' \<in> A \<and> e1 (p1 (j a')) = e1 (p1' a') \<and> e2 (p2 (j a')) = e2 (p2' a')"
-shows "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
-unfolding wppull_def proof safe
- fix b1 b2
- assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2" and f: "f1 b1 = f2 b2"
- then obtain a' where a': "a' \<in> A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'"
- using wp unfolding wpull_def by blast
- show "\<exists>a\<in>A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2"
- apply(rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto
-qed
-
-lemma wppull_id: "\<lbrakk>wpull UNIV UNIV UNIV f1 f2 p1 p2; e1 = id; e2 = id\<rbrakk> \<Longrightarrow>
- wppull UNIV UNIV UNIV f1 f2 e1 e2 p1 p2"
-by (erule wpull_wppull) auto
-
-
-(* Operators: *)
-definition diag where "diag A \<equiv> {(a,a) | a. a \<in> A}"
-definition "Gr A f = {(a,f a) | a. a \<in> A}"
-definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
-
-lemma diagI: "x \<in> A \<Longrightarrow> (x, x) \<in> diag A"
-unfolding diag_def by simp
-
-lemma diagE: "(a, b) \<in> diag A \<Longrightarrow> a = b"
-unfolding diag_def by simp
-
-lemma diagE': "x \<in> diag A \<Longrightarrow> fst x = snd x"
-unfolding diag_def by auto
-
-lemma diag_fst: "x \<in> diag A \<Longrightarrow> fst x \<in> A"
-unfolding diag_def by auto
-
-lemma diag_UNIV: "diag UNIV = Id"
-unfolding diag_def by auto
-
-lemma diag_converse: "diag A = (diag A) ^-1"
-unfolding diag_def by auto
-
-lemma diag_Comp: "diag A = diag A O diag A"
-unfolding diag_def by auto
-
-lemma diag_Gr: "diag A = Gr A id"
-unfolding diag_def Gr_def by simp
-
-lemma diag_UNIV_I: "x = y \<Longrightarrow> (x, y) \<in> diag UNIV"
-unfolding diag_def by auto
-
-lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
-unfolding image2_def by auto
-
-lemma Id_def': "Id = {(a,b). a = b}"
-by auto
-
-lemma Id_alt: "Id = Gr UNIV id"
-unfolding Gr_def by auto
-
-lemma Id_subset: "Id \<subseteq> {(a, b). P a b \<or> a = b}"
-by auto
-
-lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
-by auto
-
-lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
-unfolding image2_def Gr_def by auto
-
-lemma GrI: "\<lbrakk>x \<in> A; f x = fx\<rbrakk> \<Longrightarrow> (x, fx) \<in> Gr A f"
-unfolding Gr_def by simp
-
-lemma GrE: "(x, fx) \<in> Gr A f \<Longrightarrow> (x \<in> A \<Longrightarrow> f x = fx \<Longrightarrow> P) \<Longrightarrow> P"
-unfolding Gr_def by simp
-
-lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
-unfolding Gr_def by simp
-
-lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
-unfolding Gr_def by simp
-
-lemma Gr_UNIV_id: "f = id \<Longrightarrow> (Gr UNIV f)^-1 O Gr UNIV f = Gr UNIV f"
-unfolding Gr_def by auto
-
-lemma Gr_fst_snd: "(Gr R fst)^-1 O Gr R snd = R"
-unfolding Gr_def by auto
-
-lemma Gr_mono: "A \<subseteq> B \<Longrightarrow> Gr A f \<subseteq> Gr B f"
-unfolding Gr_def by auto
-
-lemma subst_rel_def: "A = B \<Longrightarrow> (Gr A f)^-1 O Gr A g = (Gr B f)^-1 O Gr B g"
-by simp
-
-lemma abs_pred_def: "\<lbrakk>\<And>x y. (x, y) \<in> rel = pred x y\<rbrakk> \<Longrightarrow> rel = Collect (split pred)"
-by auto
-
-lemma Collect_split_cong: "Collect (split pred) = Collect (split pred') \<Longrightarrow> pred = pred'"
-by blast
-
-lemma pred_def_abs: "rel = Collect (split pred) \<Longrightarrow> pred = (\<lambda>x y. (x, y) \<in> rel)"
-by auto
-
-lemma wpull_Gr:
-"wpull (Gr A f) A (f ` A) f id fst snd"
-unfolding wpull_def Gr_def by auto
-
-lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
-unfolding Gr_def by auto
-
-lemma equiv_Image: "equiv A R \<Longrightarrow> (\<And>a b. (a, b) \<in> R \<Longrightarrow> a \<in> A \<and> b \<in> A \<and> R `` {a} = R `` {b})"
-unfolding equiv_def refl_on_def Image_def by (auto intro: transD symD)
-
-definition relImage where
-"relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
-
-definition relInvImage where
-"relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
-
-lemma relImage_Gr:
-"\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
-unfolding relImage_def Gr_def relcomp_def by auto
-
-lemma relInvImage_Gr: "\<lbrakk>R \<subseteq> B \<times> B\<rbrakk> \<Longrightarrow> relInvImage A R f = Gr A f O R O (Gr A f)^-1"
-unfolding Gr_def relcomp_def image_def relInvImage_def by auto
-
-lemma relImage_mono:
-"R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
-unfolding relImage_def by auto
-
-lemma relInvImage_mono:
-"R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
-unfolding relInvImage_def by auto
-
-lemma relInvImage_diag:
-"(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (diag B) f \<subseteq> Id"
-unfolding relInvImage_def diag_def by auto
-
-lemma relInvImage_UNIV_relImage:
-"R \<subseteq> relInvImage UNIV (relImage R f) f"
-unfolding relInvImage_def relImage_def by auto
-
-lemma relImage_proj:
-assumes "equiv A R"
-shows "relImage R (proj R) \<subseteq> diag (A//R)"
-unfolding relImage_def diag_def apply safe
-using proj_iff[OF assms]
-by (metis assms equiv_Image proj_def proj_preserves)
-
-lemma relImage_relInvImage:
-assumes "R \<subseteq> f ` A <*> f ` A"
-shows "relImage (relInvImage A R f) f = R"
-using assms unfolding relImage_def relInvImage_def by fastforce
-
-
-(* Relation composition as a weak pseudo-pullback *)
-
-(* pick middle *)
-definition "pickM P Q a c = (SOME b. (a,b) \<in> P \<and> (b,c) \<in> Q)"
-
-lemma pickM:
-assumes "(a,c) \<in> P O Q"
-shows "(a, pickM P Q a c) \<in> P \<and> (pickM P Q a c, c) \<in> Q"
-unfolding pickM_def apply(rule someI_ex)
-using assms unfolding relcomp_def by auto
-
-definition fstO where "fstO P Q ac = (fst ac, pickM P Q (fst ac) (snd ac))"
-definition sndO where "sndO P Q ac = (pickM P Q (fst ac) (snd ac), snd ac)"
-
-lemma fstO_in: "ac \<in> P O Q \<Longrightarrow> fstO P Q ac \<in> P"
-by (metis assms fstO_def pickM surjective_pairing)
-
-lemma fst_fstO: "fst bc = (fst \<circ> fstO P Q) bc"
-unfolding comp_def fstO_def by simp
-
-lemma snd_sndO: "snd bc = (snd \<circ> sndO P Q) bc"
-unfolding comp_def sndO_def by simp
-
-lemma sndO_in: "ac \<in> P O Q \<Longrightarrow> sndO P Q ac \<in> Q"
-by (metis assms sndO_def pickM surjective_pairing)
-
-lemma csquare_fstO_sndO:
-"csquare (P O Q) snd fst (fstO P Q) (sndO P Q)"
-unfolding csquare_def fstO_def sndO_def using pickM by auto
-
-lemma wppull_fstO_sndO:
-shows "wppull (P O Q) P Q snd fst fst snd (fstO P Q) (sndO P Q)"
-using pickM unfolding wppull_def fstO_def sndO_def relcomp_def by auto
-
-lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
-by simp
-
-lemma snd_fst_flip: "snd xy = (fst o (%(x, y). (y, x))) xy"
-by (simp split: prod.split)
-
-lemma fst_snd_flip: "fst xy = (snd o (%(x, y). (y, x))) xy"
-by (simp split: prod.split)
-
-lemma flip_rel: "A \<subseteq> (R ^-1) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> R"
-by auto
-
-lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z"
-by simp
-
-lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z"
-by simp
-
-lemma fst_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> fst (snd x) = y"
-by simp
-
-lemma snd_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> snd (snd x) = z"
-by simp
-
-lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
-by simp
-
-lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
-by simp
-
-lemma Collect_restrict: "{x. x \<in> X \<and> P x} \<subseteq> X"
-by auto
-
-lemma Collect_restrict': "{(x, y) | x y. phi x y \<and> P x y} \<subseteq> {(x, y) | x y. phi x y}"
-by auto
-
-lemma prop_restrict: "\<lbrakk>x \<in> Z; Z \<subseteq> {x. x \<in> X \<and> P x}\<rbrakk> \<Longrightarrow> P x"
-by auto
-
-lemma underS_I: "\<lbrakk>i \<noteq> j; (i, j) \<in> R\<rbrakk> \<Longrightarrow> i \<in> rel.underS R j"
-unfolding rel.underS_def by simp
-
-lemma underS_E: "i \<in> rel.underS R j \<Longrightarrow> i \<noteq> j \<and> (i, j) \<in> R"
-unfolding rel.underS_def by simp
-
-lemma underS_Field: "i \<in> rel.underS R j \<Longrightarrow> i \<in> Field R"
-unfolding rel.underS_def Field_def by auto
-
-lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
-unfolding Field_def by auto
-
-
-subsection {* Convolution product *}
-
-definition convol ("<_ , _>") where
-"<f , g> \<equiv> %a. (f a, g a)"
-
-lemma fst_convol:
-"fst o <f , g> = f"
-apply(rule ext)
-unfolding convol_def by simp
-
-lemma snd_convol:
-"snd o <f , g> = g"
-apply(rule ext)
-unfolding convol_def by simp
-
-lemma fst_convol': "fst (<f, g> x) = f x"
-using fst_convol unfolding convol_def by simp
-
-lemma snd_convol': "snd (<f, g> x) = g x"
-using snd_convol unfolding convol_def by simp
-
-lemma image_convolD: "\<lbrakk>(a, b) \<in> <f, g> ` X\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> X \<and> a = f x \<and> b = g x"
-unfolding convol_def by auto
-
-lemma convol_expand_snd: "fst o f = g \<Longrightarrow> <g, snd o f> = f"
-unfolding convol_def by auto
-
-subsection{* Facts about functions *}
-
-lemma pointfreeE: "f o g = f' o g' \<Longrightarrow> f (g x) = f' (g' x)"
-unfolding o_def fun_eq_iff by simp
-
-lemma pointfree_idE: "f o g = id \<Longrightarrow> f (g x) = x"
-unfolding o_def fun_eq_iff by simp
-
-definition inver where
- "inver g f A = (ALL a : A. g (f a) = a)"
-
-lemma bij_betw_iff_ex:
- "bij_betw f A B = (EX g. g ` B = A \<and> inver g f A \<and> inver f g B)" (is "?L = ?R")
-proof (rule iffI)
- assume ?L
- hence f: "f ` A = B" and inj_f: "inj_on f A" unfolding bij_betw_def by auto
- let ?phi = "% b a. a : A \<and> f a = b"
- have "ALL b : B. EX a. ?phi b a" using f by blast
- then obtain g where g: "ALL b : B. g b : A \<and> f (g b) = b"
- using bchoice[of B ?phi] by blast
- hence gg: "ALL b : f ` A. g b : A \<and> f (g b) = b" using f by blast
- have gf: "inver g f A" unfolding inver_def by (metis gg imageI inj_f the_inv_into_f_f)
- moreover have "g ` B \<le> A \<and> inver f g B" using g unfolding inver_def by blast
- moreover have "A \<le> g ` B"
- proof safe
- fix a assume a: "a : A"
- hence "f a : B" using f by auto
- moreover have "a = g (f a)" using a gf unfolding inver_def by auto
- ultimately show "a : g ` B" by blast
- qed
- ultimately show ?R by blast
-next
- assume ?R
- then obtain g where g: "g ` B = A \<and> inver g f A \<and> inver f g B" by blast
- show ?L unfolding bij_betw_def
- proof safe
- show "inj_on f A" unfolding inj_on_def
- proof safe
- fix a1 a2 assume a: "a1 : A" "a2 : A" and "f a1 = f a2"
- hence "g (f a1) = g (f a2)" by simp
- thus "a1 = a2" using a g unfolding inver_def by simp
- qed
- next
- fix a assume "a : A"
- then obtain b where b: "b : B" and a: "a = g b" using g by blast
- hence "b = f (g b)" using g unfolding inver_def by auto
- thus "f a : B" unfolding a using b by simp
- next
- fix b assume "b : B"
- hence "g b : A \<and> b = f (g b)" using g unfolding inver_def by auto
- thus "b : f ` A" by auto
- qed
-qed
-
-lemma bijI: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
-unfolding bij_def inj_on_def by auto blast
-
-lemma bij_betw_ex_weakE:
- "\<lbrakk>bij_betw f A B\<rbrakk> \<Longrightarrow> \<exists>g. g ` B \<subseteq> A \<and> inver g f A \<and> inver f g B"
-by (auto simp only: bij_betw_iff_ex)
-
-lemma inver_surj: "\<lbrakk>g ` B \<subseteq> A; f ` A \<subseteq> B; inver g f A\<rbrakk> \<Longrightarrow> g ` B = A"
-unfolding inver_def by auto (rule rev_image_eqI, auto)
-
-lemma inver_mono: "\<lbrakk>A \<subseteq> B; inver f g B\<rbrakk> \<Longrightarrow> inver f g A"
-unfolding inver_def by auto
-
-lemma inver_pointfree: "inver f g A = (\<forall>a \<in> A. (f o g) a = a)"
-unfolding inver_def by simp
-
-lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
-unfolding bij_betw_def by auto
-
-lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B"
-unfolding bij_betw_def by auto
-
-lemma inverE: "\<lbrakk>inver f f' A; x \<in> A\<rbrakk> \<Longrightarrow> f (f' x) = x"
-unfolding inver_def by auto
-
-lemma bij_betw_inver1: "bij_betw f A B \<Longrightarrow> inver (inv_into A f) f A"
-unfolding bij_betw_def inver_def by auto
-
-lemma bij_betw_inver2: "bij_betw f A B \<Longrightarrow> inver f (inv_into A f) B"
-unfolding bij_betw_def inver_def by auto
-
-lemma bij_betwI: "\<lbrakk>bij_betw g B A; inver g f A; inver f g B\<rbrakk> \<Longrightarrow> bij_betw f A B"
-by (metis bij_betw_iff_ex bij_betw_imageE)
-
-lemma bij_betwI':
- "\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y);
- \<And>x. x \<in> X \<Longrightarrow> f x \<in> Y;
- \<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> bij_betw f X Y"
-unfolding bij_betw_def inj_on_def by auto (metis rev_image_eqI)
-
-lemma o_bij:
- assumes gf: "g o f = id" and fg: "f o g = id"
- shows "bij f"
-unfolding bij_def inj_on_def surj_def proof safe
- fix a1 a2 assume "f a1 = f a2"
- hence "g ( f a1) = g (f a2)" by simp
- thus "a1 = a2" using gf unfolding fun_eq_iff by simp
-next
- fix b
- have "b = f (g b)"
- using fg unfolding fun_eq_iff by simp
- thus "EX a. b = f a" by blast
-qed
-
-lemma surj_fun_eq:
- assumes surj_on: "f ` X = UNIV" and eq_on: "\<forall>x \<in> X. (g1 o f) x = (g2 o f) x"
- shows "g1 = g2"
-proof (rule ext)
- fix y
- from surj_on obtain x where "x \<in> X" and "y = f x" by blast
- thus "g1 y = g2 y" using eq_on by simp
-qed
-
-lemma Card_order_wo_rel: "Card_order r \<Longrightarrow> wo_rel r"
-unfolding wo_rel_def card_order_on_def by blast
-
-lemma Cinfinite_limit: "\<lbrakk>x \<in> Field r; Cinfinite r\<rbrakk> \<Longrightarrow>
- \<exists>y \<in> Field r. x \<noteq> y \<and> (x, y) \<in> r"
-unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit)
-
-lemma Card_order_trans:
- "\<lbrakk>Card_order r; x \<noteq> y; (x, y) \<in> r; y \<noteq> z; (y, z) \<in> r\<rbrakk> \<Longrightarrow> x \<noteq> z \<and> (x, z) \<in> r"
-unfolding card_order_on_def well_order_on_def linear_order_on_def
- partial_order_on_def preorder_on_def trans_def antisym_def by blast
-
-lemma Cinfinite_limit2:
- assumes x1: "x1 \<in> Field r" and x2: "x2 \<in> Field r" and r: "Cinfinite r"
- shows "\<exists>y \<in> Field r. (x1 \<noteq> y \<and> (x1, y) \<in> r) \<and> (x2 \<noteq> y \<and> (x2, y) \<in> r)"
-proof -
- from r have trans: "trans r" and total: "Total r" and antisym: "antisym r"
- unfolding card_order_on_def well_order_on_def linear_order_on_def
- partial_order_on_def preorder_on_def by auto
- obtain y1 where y1: "y1 \<in> Field r" "x1 \<noteq> y1" "(x1, y1) \<in> r"
- using Cinfinite_limit[OF x1 r] by blast
- obtain y2 where y2: "y2 \<in> Field r" "x2 \<noteq> y2" "(x2, y2) \<in> r"
- using Cinfinite_limit[OF x2 r] by blast
- show ?thesis
- proof (cases "y1 = y2")
- case True with y1 y2 show ?thesis by blast
- next
- case False
- with y1(1) y2(1) total have "(y1, y2) \<in> r \<or> (y2, y1) \<in> r"
- unfolding total_on_def by auto
- thus ?thesis
- proof
- assume *: "(y1, y2) \<in> r"
- with trans y1(3) have "(x1, y2) \<in> r" unfolding trans_def by blast
- with False y1 y2 * antisym show ?thesis by (cases "x1 = y2") (auto simp: antisym_def)
- next
- assume *: "(y2, y1) \<in> r"
- with trans y2(3) have "(x2, y1) \<in> r" unfolding trans_def by blast
- with False y1 y2 * antisym show ?thesis by (cases "x2 = y1") (auto simp: antisym_def)
- qed
- qed
-qed
-
-lemma Cinfinite_limit_finite: "\<lbrakk>finite X; X \<subseteq> Field r; Cinfinite r\<rbrakk>
- \<Longrightarrow> \<exists>y \<in> Field r. \<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)"
-proof (induct X rule: finite_induct)
- case empty thus ?case unfolding cinfinite_def using ex_in_conv[of "Field r"] finite.emptyI by auto
-next
- case (insert x X)
- then obtain y where y: "y \<in> Field r" "\<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)" by blast
- then obtain z where z: "z \<in> Field r" "x \<noteq> z \<and> (x, z) \<in> r" "y \<noteq> z \<and> (y, z) \<in> r"
- using Cinfinite_limit2[OF _ y(1) insert(5), of x] insert(4) by blast
- show ?case by (metis Card_order_trans insert(5) insertE y(2) z)
-qed
-
-lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A"
-by auto
-
-(*helps resolution*)
-lemma well_order_induct_imp:
- "wo_rel r \<Longrightarrow> (\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> y \<in> Field r \<longrightarrow> P y \<Longrightarrow> x \<in> Field r \<longrightarrow> P x) \<Longrightarrow>
- x \<in> Field r \<longrightarrow> P x"
-by (erule wo_rel.well_order_induct)
-
-lemma meta_spec2:
- assumes "(\<And>x y. PROP P x y)"
- shows "PROP P x y"
-by (rule `(\<And>x y. PROP P x y)`)
-
-(*Extended Sublist*)
-
-definition prefCl where
- "prefCl Kl = (\<forall> kl1 kl2. kl1 \<le> kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl)"
-definition PrefCl where
- "PrefCl A n = (\<forall>kl kl'. kl \<in> A n \<and> kl' \<le> kl \<longrightarrow> (\<exists>m\<le>n. kl' \<in> A m))"
-
-lemma prefCl_UN:
- "\<lbrakk>\<And>n. PrefCl A n\<rbrakk> \<Longrightarrow> prefCl (\<Union>n. A n)"
-unfolding prefCl_def PrefCl_def by fastforce
-
-definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}"
-definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}"
-definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))"
-
-lemmas sh_def = Shift_def shift_def
-
-lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
-unfolding Shift_def Succ_def by simp
-
-lemma Shift_clists: "Kl \<subseteq> Field (clists r) \<Longrightarrow> Shift Kl k \<subseteq> Field (clists r)"
-unfolding Shift_def clists_def Field_card_of by auto
-
-lemma Shift_prefCl: "prefCl Kl \<Longrightarrow> prefCl (Shift Kl k)"
-unfolding prefCl_def Shift_def
-proof safe
- fix kl1 kl2
- assume "\<forall>kl1 kl2. kl1 \<le> kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl"
- "kl1 \<le> kl2" "k # kl2 \<in> Kl"
- thus "k # kl1 \<in> Kl" using Cons_prefix_Cons[of k kl1 k kl2] by blast
-qed
-
-lemma not_in_Shift: "kl \<notin> Shift Kl x \<Longrightarrow> x # kl \<notin> Kl"
-unfolding Shift_def by simp
-
-lemma prefCl_Succ: "\<lbrakk>prefCl Kl; k # kl \<in> Kl\<rbrakk> \<Longrightarrow> k \<in> Succ Kl []"
-unfolding Succ_def proof
- assume "prefCl Kl" "k # kl \<in> Kl"
- moreover have "k # [] \<le> k # kl" by auto
- ultimately have "k # [] \<in> Kl" unfolding prefCl_def by blast
- thus "[] @ [k] \<in> Kl" by simp
-qed
-
-lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
-unfolding Succ_def by simp
-
-lemmas SuccE = SuccD[elim_format]
-
-lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl"
-unfolding Succ_def by simp
-
-lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl"
-unfolding Shift_def by simp
-
-lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
-unfolding Succ_def Shift_def by auto
-
-lemma ShiftI: "k # kl \<in> Kl \<Longrightarrow> kl \<in> Shift Kl k"
-unfolding Shift_def by simp
-
-lemma Func_cexp: "|Func A B| =o |B| ^c |A|"
-unfolding cexp_def Field_card_of by (simp only: card_of_refl)
-
-lemma clists_bound: "A \<in> Field (cpow (clists r)) - {{}} \<Longrightarrow> |A| \<le>o clists r"
-unfolding cpow_def clists_def Field_card_of by (auto simp: card_of_mono1)
-
-lemma cpow_clists_czero: "\<lbrakk>A \<in> Field (cpow (clists r)) - {{}}; |A| =o czero\<rbrakk> \<Longrightarrow> False"
-unfolding cpow_def clists_def
-by (auto simp add: card_of_ordIso_czero_iff_empty[symmetric])
- (erule notE, erule ordIso_transitive, rule czero_ordIso)
-
-lemma incl_UNION_I:
-assumes "i \<in> I" and "A \<subseteq> F i"
-shows "A \<subseteq> UNION I F"
-using assms by auto
-
-lemma Nil_clists: "{[]} \<subseteq> Field (clists r)"
-unfolding clists_def Field_card_of by auto
-
-lemma Cons_clists:
- "\<lbrakk>x \<in> Field r; xs \<in> Field (clists r)\<rbrakk> \<Longrightarrow> x # xs \<in> Field (clists r)"
-unfolding clists_def Field_card_of by auto
-
-lemma length_Cons: "length (x#xs) = Suc (length xs)"
-by simp
-
-lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)"
-by simp
-
-(*injection into the field of a cardinal*)
-definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r"
-definition "toCard A r \<equiv> SOME f. toCard_pred A r f"
-
-lemma ex_toCard_pred:
-"\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
-unfolding toCard_pred_def
-using card_of_ordLeq[of A "Field r"]
- ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
-by blast
-
-lemma toCard_pred_toCard:
- "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)"
-unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
-
-lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow>
- toCard A r x = toCard A r y \<longleftrightarrow> x = y"
-using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
-
-lemma toCard: "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> toCard A r b \<in> Field r"
-using toCard_pred_toCard unfolding toCard_pred_def by blast
-
-definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k"
-
-lemma fromCard_toCard:
-"\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
-unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
-
-(* pick according to the weak pullback *)
-definition pickWP_pred where
-"pickWP_pred A p1 p2 b1 b2 a \<equiv>
- a \<in> A \<and> p1 a = b1 \<and> p2 a = b2"
-
-definition pickWP where
-"pickWP A p1 p2 b1 b2 \<equiv>
- SOME a. pickWP_pred A p1 p2 b1 b2 a"
-
-lemma pickWP_pred:
-assumes "wpull A B1 B2 f1 f2 p1 p2" and
-"b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2"
-shows "\<exists> a. pickWP_pred A p1 p2 b1 b2 a"
-using assms unfolding wpull_def pickWP_pred_def by blast
-
-lemma pickWP_pred_pickWP:
-assumes "wpull A B1 B2 f1 f2 p1 p2" and
-"b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2"
-shows "pickWP_pred A p1 p2 b1 b2 (pickWP A p1 p2 b1 b2)"
-unfolding pickWP_def using assms by(rule someI_ex[OF pickWP_pred])
-
-lemma pickWP:
-assumes "wpull A B1 B2 f1 f2 p1 p2" and
-"b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2"
-shows "pickWP A p1 p2 b1 b2 \<in> A"
- "p1 (pickWP A p1 p2 b1 b2) = b1"
- "p2 (pickWP A p1 p2 b1 b2) = b2"
-using assms pickWP_pred_pickWP unfolding pickWP_pred_def by fastforce+
-
-lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp
-
-lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
-unfolding Field_card_of csum_def by auto
-
-lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
-unfolding Field_card_of csum_def by auto
-
-lemma nat_rec_0: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
-by auto
-
-lemma nat_rec_Suc: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
-by auto
-
-lemma list_rec_Nil: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
-by auto
-
-lemma list_rec_Cons: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
-by auto
-
-lemma sum_case_cong: "p = q \<Longrightarrow> sum_case f g p = sum_case f g q"
-by simp
-
-lemma sum_case_step:
- "sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p"
- "sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p"
-by auto
-
-lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-by simp
-
-lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
-by blast
-
-lemma obj_sumE_f:
-"\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f x \<longrightarrow> P"
-by (metis sum.exhaust)
-
-lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
-by (cases s) auto
-
-lemma obj_sum_step:
- "\<lbrakk>\<forall>x. s = f (Inr (Inl x)) \<longrightarrow> P; \<forall>x. s = f (Inr (Inr x)) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f (Inr x) \<longrightarrow> P"
-by (metis obj_sumE)
-
-lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
-by simp
-
-end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codatatype/BNF_Util.thy Tue Sep 11 19:45:12 2012 +0200
@@ -0,0 +1,859 @@
+(* Title: HOL/Codatatype/BNF_Util.thy
+ Author: Dmitriy Traytel, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2012
+
+Library for bounded natural functors.
+*)
+
+header {* Library for Bounded Natural Functors *}
+
+theory BNF_Util
+imports
+ "../Ordinals_and_Cardinals/Cardinal_Arithmetic"
+ "~~/src/HOL/Library/Prefix_Order"
+ Equiv_Relations_More
+uses
+ ("Tools/bnf_util.ML")
+begin
+
+lemma iffI_np: "\<lbrakk>x \<Longrightarrow> \<not> y; \<not> x \<Longrightarrow> y\<rbrakk> \<Longrightarrow> \<not> x \<longleftrightarrow> y"
+by (erule iffI) (erule contrapos_pn)
+
+lemma all_unit_eq: "(\<And>x. PROP P x) \<equiv> PROP P ()" by simp
+
+lemma all_prod_eq: "(\<And>x. PROP P x) \<equiv> (\<And>a b. PROP P (a, b))" by clarsimp
+
+lemma False_imp_eq: "(False \<Longrightarrow> P) \<equiv> Trueprop True"
+by presburger
+
+lemma case_unit: "(case u of () => f) = f"
+by (cases u) (hypsubst, rule unit.cases)
+
+lemma All_point_1: "(\<And>z. z = b \<Longrightarrow> phi z) \<equiv> Trueprop (phi b)"
+by presburger
+
+lemma subset_Collect_iff: "B \<subseteq> A \<Longrightarrow> (B \<subseteq> {x \<in> A. P x}) = (\<forall>x \<in> B. P x)"
+by blast
+
+lemma subset_CollectI: "B \<subseteq> A \<Longrightarrow> (\<And>x. x \<in> B \<Longrightarrow> Q x \<Longrightarrow> P x) \<Longrightarrow> ({x \<in> B. Q x} \<subseteq> {x \<in> A. P x})"
+by blast
+
+lemma mem_Collect_eq_split: "{(x, y). (x, y) \<in> X} = X"
+by simp
+
+lemma image_comp: "image (f o g) = image f o image g"
+by (rule ext) (auto simp only: o_apply image_def)
+
+lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})"
+by (rule ext) simp
+
+lemma Union_natural: "Union o image (image f) = image f o Union"
+by (rule ext) (auto simp only: o_apply)
+
+lemma in_Union_o_assoc: "x \<in> (Union o gset o gmap) A \<Longrightarrow> x \<in> (Union o (gset o gmap)) A"
+by (unfold o_assoc)
+
+lemma comp_single_set_bd:
+ assumes fbd_Card_order: "Card_order fbd" and
+ fset_bd: "\<And>x. |fset x| \<le>o fbd" and
+ gset_bd: "\<And>x. |gset x| \<le>o gbd"
+ shows "|\<Union>fset ` gset x| \<le>o gbd *c fbd"
+apply (subst sym[OF SUP_def])
+apply (rule ordLeq_transitive)
+apply (rule card_of_UNION_Sigma)
+apply (subst SIGMA_CSUM)
+apply (rule ordLeq_transitive)
+apply (rule card_of_Csum_Times')
+apply (rule fbd_Card_order)
+apply (rule ballI)
+apply (rule fset_bd)
+apply (rule ordLeq_transitive)
+apply (rule cprod_mono1)
+apply (rule gset_bd)
+apply (rule ordIso_imp_ordLeq)
+apply (rule ordIso_refl)
+apply (rule Card_order_cprod)
+done
+
+lemma Union_image_insert: "\<Union>f ` insert a B = f a \<union> \<Union>f ` B"
+by simp
+
+lemma Union_image_empty: "A \<union> \<Union>f ` {} = A"
+by simp
+
+definition collect where
+ "collect F x = (\<Union>f \<in> F. f x)"
+
+lemma collect_o: "collect F o g = collect ((\<lambda>f. f o g) ` F)"
+by (rule ext) (auto simp only: o_apply collect_def)
+
+lemma image_o_collect: "collect ((\<lambda>f. image g o f) ` F) = image g o collect F"
+by (rule ext) (auto simp add: collect_def)
+
+lemma conj_subset_def: "A \<subseteq> {x. P x \<and> Q x} = (A \<subseteq> {x. P x} \<and> A \<subseteq> {x. Q x})"
+by blast
+
+lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
+by blast
+
+lemma rev_bspec: "a \<in> A \<Longrightarrow> \<forall>z \<in> A. P z \<Longrightarrow> P a"
+by simp
+
+lemma Un_cong: "\<lbrakk>A = B; C = D\<rbrakk> \<Longrightarrow> A \<union> C = B \<union> D"
+by simp
+
+lemma UN_image_subset: "\<Union>f ` g x \<subseteq> X = (g x \<subseteq> {x. f x \<subseteq> X})"
+by blast
+
+lemma image_Collect_subsetI:
+ "(\<And>x. P x \<Longrightarrow> f x \<in> B) \<Longrightarrow> f ` {x. P x} \<subseteq> B"
+by blast
+
+lemma comp_set_bd_Union_o_collect: "|\<Union>\<Union>(\<lambda>f. f x) ` X| \<le>o hbd \<Longrightarrow> |(Union \<circ> collect X) x| \<le>o hbd"
+by (unfold o_apply collect_def SUP_def)
+
+lemma sum_case_comp_Inl:
+"sum_case f g \<circ> Inl = f"
+unfolding comp_def by simp
+
+lemma sum_case_expand_Inr: "f o Inl = g \<Longrightarrow> f x = sum_case g (f o Inr) x"
+by (auto split: sum.splits)
+
+lemma converse_mono:
+"R1 ^-1 \<subseteq> R2 ^-1 \<longleftrightarrow> R1 \<subseteq> R2"
+unfolding converse_def by auto
+
+lemma converse_shift:
+"R1 \<subseteq> R2 ^-1 \<Longrightarrow> R1 ^-1 \<subseteq> R2"
+unfolding converse_def by auto
+
+lemma converse_Times: "(A \<times> B) ^-1 = B \<times> A"
+by auto
+
+lemma equiv_triv1:
+assumes "equiv A R" and "(a, b) \<in> R" and "(a, c) \<in> R"
+shows "(b, c) \<in> R"
+using assms unfolding equiv_def sym_def trans_def by blast
+
+lemma equiv_triv2:
+assumes "equiv A R" and "(a, b) \<in> R" and "(b, c) \<in> R"
+shows "(a, c) \<in> R"
+using assms unfolding equiv_def trans_def by blast
+
+lemma equiv_proj:
+ assumes e: "equiv A R" and "z \<in> R"
+ shows "(proj R o fst) z = (proj R o snd) z"
+proof -
+ from assms(2) have z: "(fst z, snd z) \<in> R" by auto
+ have P: "\<And>x. (fst z, x) \<in> R \<Longrightarrow> (snd z, x) \<in> R" by (erule equiv_triv1[OF e z])
+ have "\<And>x. (snd z, x) \<in> R \<Longrightarrow> (fst z, x) \<in> R" by (erule equiv_triv2[OF e z])
+ with P show ?thesis unfolding proj_def[abs_def] by auto
+qed
+
+
+section{* Weak pullbacks: *}
+
+definition csquare where
+"csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))"
+
+definition wpull where
+"wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow>
+ (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow> (\<exists> a \<in> A. p1 a = b1 \<and> p2 a = b2))"
+
+lemma wpull_cong:
+"\<lbrakk>A' = A; B1' = B1; B2' = B2; wpull A B1 B2 f1 f2 p1 p2\<rbrakk> \<Longrightarrow> wpull A' B1' B2' f1 f2 p1 p2"
+by simp
+
+lemma wpull_id: "wpull UNIV B1 B2 id id id id"
+unfolding wpull_def by simp
+
+
+(* Weak pseudo-pullbacks *)
+
+definition wppull where
+"wppull A B1 B2 f1 f2 e1 e2 p1 p2 \<longleftrightarrow>
+ (\<forall> b1 b2. b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2 \<longrightarrow>
+ (\<exists> a \<in> A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2))"
+
+
+(* The pullback of sets *)
+definition thePull where
+"thePull B1 B2 f1 f2 = {(b1,b2). b1 \<in> B1 \<and> b2 \<in> B2 \<and> f1 b1 = f2 b2}"
+
+lemma wpull_thePull:
+"wpull (thePull B1 B2 f1 f2) B1 B2 f1 f2 fst snd"
+unfolding wpull_def thePull_def by auto
+
+lemma wppull_thePull:
+assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
+shows
+"\<exists> j. \<forall> a' \<in> thePull B1 B2 f1 f2.
+ j a' \<in> A \<and>
+ e1 (p1 (j a')) = e1 (fst a') \<and> e2 (p2 (j a')) = e2 (snd a')"
+(is "\<exists> j. \<forall> a' \<in> ?A'. ?phi a' (j a')")
+proof(rule bchoice[of ?A' ?phi], default)
+ fix a' assume a': "a' \<in> ?A'"
+ hence "fst a' \<in> B1" unfolding thePull_def by auto
+ moreover
+ from a' have "snd a' \<in> B2" unfolding thePull_def by auto
+ moreover have "f1 (fst a') = f2 (snd a')"
+ using a' unfolding csquare_def thePull_def by auto
+ ultimately show "\<exists> ja'. ?phi a' ja'"
+ using assms unfolding wppull_def by auto
+qed
+
+lemma wpull_wppull:
+assumes wp: "wpull A' B1 B2 f1 f2 p1' p2'" and
+1: "\<forall> a' \<in> A'. j a' \<in> A \<and> e1 (p1 (j a')) = e1 (p1' a') \<and> e2 (p2 (j a')) = e2 (p2' a')"
+shows "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
+unfolding wppull_def proof safe
+ fix b1 b2
+ assume b1: "b1 \<in> B1" and b2: "b2 \<in> B2" and f: "f1 b1 = f2 b2"
+ then obtain a' where a': "a' \<in> A'" and b1: "b1 = p1' a'" and b2: "b2 = p2' a'"
+ using wp unfolding wpull_def by blast
+ show "\<exists>a\<in>A. e1 (p1 a) = e1 b1 \<and> e2 (p2 a) = e2 b2"
+ apply(rule bexI[of _ "j a'"]) unfolding b1 b2 using a' 1 by auto
+qed
+
+lemma wppull_id: "\<lbrakk>wpull UNIV UNIV UNIV f1 f2 p1 p2; e1 = id; e2 = id\<rbrakk> \<Longrightarrow>
+ wppull UNIV UNIV UNIV f1 f2 e1 e2 p1 p2"
+by (erule wpull_wppull) auto
+
+
+(* Operators: *)
+definition diag where "diag A \<equiv> {(a,a) | a. a \<in> A}"
+definition "Gr A f = {(a,f a) | a. a \<in> A}"
+definition image2 where "image2 A f g = {(f a, g a) | a. a \<in> A}"
+
+lemma diagI: "x \<in> A \<Longrightarrow> (x, x) \<in> diag A"
+unfolding diag_def by simp
+
+lemma diagE: "(a, b) \<in> diag A \<Longrightarrow> a = b"
+unfolding diag_def by simp
+
+lemma diagE': "x \<in> diag A \<Longrightarrow> fst x = snd x"
+unfolding diag_def by auto
+
+lemma diag_fst: "x \<in> diag A \<Longrightarrow> fst x \<in> A"
+unfolding diag_def by auto
+
+lemma diag_UNIV: "diag UNIV = Id"
+unfolding diag_def by auto
+
+lemma diag_converse: "diag A = (diag A) ^-1"
+unfolding diag_def by auto
+
+lemma diag_Comp: "diag A = diag A O diag A"
+unfolding diag_def by auto
+
+lemma diag_Gr: "diag A = Gr A id"
+unfolding diag_def Gr_def by simp
+
+lemma diag_UNIV_I: "x = y \<Longrightarrow> (x, y) \<in> diag UNIV"
+unfolding diag_def by auto
+
+lemma image2_eqI: "\<lbrakk>b = f x; c = g x; x \<in> A\<rbrakk> \<Longrightarrow> (b, c) \<in> image2 A f g"
+unfolding image2_def by auto
+
+lemma Id_def': "Id = {(a,b). a = b}"
+by auto
+
+lemma Id_alt: "Id = Gr UNIV id"
+unfolding Gr_def by auto
+
+lemma Id_subset: "Id \<subseteq> {(a, b). P a b \<or> a = b}"
+by auto
+
+lemma IdD: "(a, b) \<in> Id \<Longrightarrow> a = b"
+by auto
+
+lemma image2_Gr: "image2 A f g = (Gr A f)^-1 O (Gr A g)"
+unfolding image2_def Gr_def by auto
+
+lemma GrI: "\<lbrakk>x \<in> A; f x = fx\<rbrakk> \<Longrightarrow> (x, fx) \<in> Gr A f"
+unfolding Gr_def by simp
+
+lemma GrE: "(x, fx) \<in> Gr A f \<Longrightarrow> (x \<in> A \<Longrightarrow> f x = fx \<Longrightarrow> P) \<Longrightarrow> P"
+unfolding Gr_def by simp
+
+lemma GrD1: "(x, fx) \<in> Gr A f \<Longrightarrow> x \<in> A"
+unfolding Gr_def by simp
+
+lemma GrD2: "(x, fx) \<in> Gr A f \<Longrightarrow> f x = fx"
+unfolding Gr_def by simp
+
+lemma Gr_UNIV_id: "f = id \<Longrightarrow> (Gr UNIV f)^-1 O Gr UNIV f = Gr UNIV f"
+unfolding Gr_def by auto
+
+lemma Gr_fst_snd: "(Gr R fst)^-1 O Gr R snd = R"
+unfolding Gr_def by auto
+
+lemma Gr_mono: "A \<subseteq> B \<Longrightarrow> Gr A f \<subseteq> Gr B f"
+unfolding Gr_def by auto
+
+lemma subst_rel_def: "A = B \<Longrightarrow> (Gr A f)^-1 O Gr A g = (Gr B f)^-1 O Gr B g"
+by simp
+
+lemma abs_pred_def: "\<lbrakk>\<And>x y. (x, y) \<in> rel = pred x y\<rbrakk> \<Longrightarrow> rel = Collect (split pred)"
+by auto
+
+lemma Collect_split_cong: "Collect (split pred) = Collect (split pred') \<Longrightarrow> pred = pred'"
+by blast
+
+lemma pred_def_abs: "rel = Collect (split pred) \<Longrightarrow> pred = (\<lambda>x y. (x, y) \<in> rel)"
+by auto
+
+lemma wpull_Gr:
+"wpull (Gr A f) A (f ` A) f id fst snd"
+unfolding wpull_def Gr_def by auto
+
+lemma Gr_incl: "Gr A f \<subseteq> A <*> B \<longleftrightarrow> f ` A \<subseteq> B"
+unfolding Gr_def by auto
+
+lemma equiv_Image: "equiv A R \<Longrightarrow> (\<And>a b. (a, b) \<in> R \<Longrightarrow> a \<in> A \<and> b \<in> A \<and> R `` {a} = R `` {b})"
+unfolding equiv_def refl_on_def Image_def by (auto intro: transD symD)
+
+definition relImage where
+"relImage R f \<equiv> {(f a1, f a2) | a1 a2. (a1,a2) \<in> R}"
+
+definition relInvImage where
+"relInvImage A R f \<equiv> {(a1, a2) | a1 a2. a1 \<in> A \<and> a2 \<in> A \<and> (f a1, f a2) \<in> R}"
+
+lemma relImage_Gr:
+"\<lbrakk>R \<subseteq> A \<times> A\<rbrakk> \<Longrightarrow> relImage R f = (Gr A f)^-1 O R O Gr A f"
+unfolding relImage_def Gr_def relcomp_def by auto
+
+lemma relInvImage_Gr: "\<lbrakk>R \<subseteq> B \<times> B\<rbrakk> \<Longrightarrow> relInvImage A R f = Gr A f O R O (Gr A f)^-1"
+unfolding Gr_def relcomp_def image_def relInvImage_def by auto
+
+lemma relImage_mono:
+"R1 \<subseteq> R2 \<Longrightarrow> relImage R1 f \<subseteq> relImage R2 f"
+unfolding relImage_def by auto
+
+lemma relInvImage_mono:
+"R1 \<subseteq> R2 \<Longrightarrow> relInvImage A R1 f \<subseteq> relInvImage A R2 f"
+unfolding relInvImage_def by auto
+
+lemma relInvImage_diag:
+"(\<And>a1 a2. f a1 = f a2 \<longleftrightarrow> a1 = a2) \<Longrightarrow> relInvImage A (diag B) f \<subseteq> Id"
+unfolding relInvImage_def diag_def by auto
+
+lemma relInvImage_UNIV_relImage:
+"R \<subseteq> relInvImage UNIV (relImage R f) f"
+unfolding relInvImage_def relImage_def by auto
+
+lemma relImage_proj:
+assumes "equiv A R"
+shows "relImage R (proj R) \<subseteq> diag (A//R)"
+unfolding relImage_def diag_def apply safe
+using proj_iff[OF assms]
+by (metis assms equiv_Image proj_def proj_preserves)
+
+lemma relImage_relInvImage:
+assumes "R \<subseteq> f ` A <*> f ` A"
+shows "relImage (relInvImage A R f) f = R"
+using assms unfolding relImage_def relInvImage_def by fastforce
+
+
+(* Relation composition as a weak pseudo-pullback *)
+
+(* pick middle *)
+definition "pickM P Q a c = (SOME b. (a,b) \<in> P \<and> (b,c) \<in> Q)"
+
+lemma pickM:
+assumes "(a,c) \<in> P O Q"
+shows "(a, pickM P Q a c) \<in> P \<and> (pickM P Q a c, c) \<in> Q"
+unfolding pickM_def apply(rule someI_ex)
+using assms unfolding relcomp_def by auto
+
+definition fstO where "fstO P Q ac = (fst ac, pickM P Q (fst ac) (snd ac))"
+definition sndO where "sndO P Q ac = (pickM P Q (fst ac) (snd ac), snd ac)"
+
+lemma fstO_in: "ac \<in> P O Q \<Longrightarrow> fstO P Q ac \<in> P"
+by (metis assms fstO_def pickM surjective_pairing)
+
+lemma fst_fstO: "fst bc = (fst \<circ> fstO P Q) bc"
+unfolding comp_def fstO_def by simp
+
+lemma snd_sndO: "snd bc = (snd \<circ> sndO P Q) bc"
+unfolding comp_def sndO_def by simp
+
+lemma sndO_in: "ac \<in> P O Q \<Longrightarrow> sndO P Q ac \<in> Q"
+by (metis assms sndO_def pickM surjective_pairing)
+
+lemma csquare_fstO_sndO:
+"csquare (P O Q) snd fst (fstO P Q) (sndO P Q)"
+unfolding csquare_def fstO_def sndO_def using pickM by auto
+
+lemma wppull_fstO_sndO:
+shows "wppull (P O Q) P Q snd fst fst snd (fstO P Q) (sndO P Q)"
+using pickM unfolding wppull_def fstO_def sndO_def relcomp_def by auto
+
+lemma subst_Pair: "P x y \<Longrightarrow> a = (x, y) \<Longrightarrow> P (fst a) (snd a)"
+by simp
+
+lemma snd_fst_flip: "snd xy = (fst o (%(x, y). (y, x))) xy"
+by (simp split: prod.split)
+
+lemma fst_snd_flip: "fst xy = (snd o (%(x, y). (y, x))) xy"
+by (simp split: prod.split)
+
+lemma flip_rel: "A \<subseteq> (R ^-1) \<Longrightarrow> (%(x, y). (y, x)) ` A \<subseteq> R"
+by auto
+
+lemma fst_diag_id: "(fst \<circ> (%x. (x, x))) z = id z"
+by simp
+
+lemma snd_diag_id: "(snd \<circ> (%x. (x, x))) z = id z"
+by simp
+
+lemma fst_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> fst (snd x) = y"
+by simp
+
+lemma snd_snd: "\<lbrakk>snd x = (y, z)\<rbrakk> \<Longrightarrow> snd (snd x) = z"
+by simp
+
+lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
+by simp
+
+lemma sndI: "x = (y, z) \<Longrightarrow> snd x = z"
+by simp
+
+lemma Collect_restrict: "{x. x \<in> X \<and> P x} \<subseteq> X"
+by auto
+
+lemma Collect_restrict': "{(x, y) | x y. phi x y \<and> P x y} \<subseteq> {(x, y) | x y. phi x y}"
+by auto
+
+lemma prop_restrict: "\<lbrakk>x \<in> Z; Z \<subseteq> {x. x \<in> X \<and> P x}\<rbrakk> \<Longrightarrow> P x"
+by auto
+
+lemma underS_I: "\<lbrakk>i \<noteq> j; (i, j) \<in> R\<rbrakk> \<Longrightarrow> i \<in> rel.underS R j"
+unfolding rel.underS_def by simp
+
+lemma underS_E: "i \<in> rel.underS R j \<Longrightarrow> i \<noteq> j \<and> (i, j) \<in> R"
+unfolding rel.underS_def by simp
+
+lemma underS_Field: "i \<in> rel.underS R j \<Longrightarrow> i \<in> Field R"
+unfolding rel.underS_def Field_def by auto
+
+lemma FieldI2: "(i, j) \<in> R \<Longrightarrow> j \<in> Field R"
+unfolding Field_def by auto
+
+
+subsection {* Convolution product *}
+
+definition convol ("<_ , _>") where
+"<f , g> \<equiv> %a. (f a, g a)"
+
+lemma fst_convol:
+"fst o <f , g> = f"
+apply(rule ext)
+unfolding convol_def by simp
+
+lemma snd_convol:
+"snd o <f , g> = g"
+apply(rule ext)
+unfolding convol_def by simp
+
+lemma fst_convol': "fst (<f, g> x) = f x"
+using fst_convol unfolding convol_def by simp
+
+lemma snd_convol': "snd (<f, g> x) = g x"
+using snd_convol unfolding convol_def by simp
+
+lemma image_convolD: "\<lbrakk>(a, b) \<in> <f, g> ` X\<rbrakk> \<Longrightarrow> \<exists>x. x \<in> X \<and> a = f x \<and> b = g x"
+unfolding convol_def by auto
+
+lemma convol_expand_snd: "fst o f = g \<Longrightarrow> <g, snd o f> = f"
+unfolding convol_def by auto
+
+subsection{* Facts about functions *}
+
+lemma pointfreeE: "f o g = f' o g' \<Longrightarrow> f (g x) = f' (g' x)"
+unfolding o_def fun_eq_iff by simp
+
+lemma pointfree_idE: "f o g = id \<Longrightarrow> f (g x) = x"
+unfolding o_def fun_eq_iff by simp
+
+definition inver where
+ "inver g f A = (ALL a : A. g (f a) = a)"
+
+lemma bij_betw_iff_ex:
+ "bij_betw f A B = (EX g. g ` B = A \<and> inver g f A \<and> inver f g B)" (is "?L = ?R")
+proof (rule iffI)
+ assume ?L
+ hence f: "f ` A = B" and inj_f: "inj_on f A" unfolding bij_betw_def by auto
+ let ?phi = "% b a. a : A \<and> f a = b"
+ have "ALL b : B. EX a. ?phi b a" using f by blast
+ then obtain g where g: "ALL b : B. g b : A \<and> f (g b) = b"
+ using bchoice[of B ?phi] by blast
+ hence gg: "ALL b : f ` A. g b : A \<and> f (g b) = b" using f by blast
+ have gf: "inver g f A" unfolding inver_def by (metis gg imageI inj_f the_inv_into_f_f)
+ moreover have "g ` B \<le> A \<and> inver f g B" using g unfolding inver_def by blast
+ moreover have "A \<le> g ` B"
+ proof safe
+ fix a assume a: "a : A"
+ hence "f a : B" using f by auto
+ moreover have "a = g (f a)" using a gf unfolding inver_def by auto
+ ultimately show "a : g ` B" by blast
+ qed
+ ultimately show ?R by blast
+next
+ assume ?R
+ then obtain g where g: "g ` B = A \<and> inver g f A \<and> inver f g B" by blast
+ show ?L unfolding bij_betw_def
+ proof safe
+ show "inj_on f A" unfolding inj_on_def
+ proof safe
+ fix a1 a2 assume a: "a1 : A" "a2 : A" and "f a1 = f a2"
+ hence "g (f a1) = g (f a2)" by simp
+ thus "a1 = a2" using a g unfolding inver_def by simp
+ qed
+ next
+ fix a assume "a : A"
+ then obtain b where b: "b : B" and a: "a = g b" using g by blast
+ hence "b = f (g b)" using g unfolding inver_def by auto
+ thus "f a : B" unfolding a using b by simp
+ next
+ fix b assume "b : B"
+ hence "g b : A \<and> b = f (g b)" using g unfolding inver_def by auto
+ thus "b : f ` A" by auto
+ qed
+qed
+
+lemma bijI: "\<lbrakk>\<And>x y. (f x = f y) = (x = y); \<And>y. \<exists>x. y = f x\<rbrakk> \<Longrightarrow> bij f"
+unfolding bij_def inj_on_def by auto blast
+
+lemma bij_betw_ex_weakE:
+ "\<lbrakk>bij_betw f A B\<rbrakk> \<Longrightarrow> \<exists>g. g ` B \<subseteq> A \<and> inver g f A \<and> inver f g B"
+by (auto simp only: bij_betw_iff_ex)
+
+lemma inver_surj: "\<lbrakk>g ` B \<subseteq> A; f ` A \<subseteq> B; inver g f A\<rbrakk> \<Longrightarrow> g ` B = A"
+unfolding inver_def by auto (rule rev_image_eqI, auto)
+
+lemma inver_mono: "\<lbrakk>A \<subseteq> B; inver f g B\<rbrakk> \<Longrightarrow> inver f g A"
+unfolding inver_def by auto
+
+lemma inver_pointfree: "inver f g A = (\<forall>a \<in> A. (f o g) a = a)"
+unfolding inver_def by simp
+
+lemma bij_betwE: "bij_betw f A B \<Longrightarrow> \<forall>a\<in>A. f a \<in> B"
+unfolding bij_betw_def by auto
+
+lemma bij_betw_imageE: "bij_betw f A B \<Longrightarrow> f ` A = B"
+unfolding bij_betw_def by auto
+
+lemma inverE: "\<lbrakk>inver f f' A; x \<in> A\<rbrakk> \<Longrightarrow> f (f' x) = x"
+unfolding inver_def by auto
+
+lemma bij_betw_inver1: "bij_betw f A B \<Longrightarrow> inver (inv_into A f) f A"
+unfolding bij_betw_def inver_def by auto
+
+lemma bij_betw_inver2: "bij_betw f A B \<Longrightarrow> inver f (inv_into A f) B"
+unfolding bij_betw_def inver_def by auto
+
+lemma bij_betwI: "\<lbrakk>bij_betw g B A; inver g f A; inver f g B\<rbrakk> \<Longrightarrow> bij_betw f A B"
+by (metis bij_betw_iff_ex bij_betw_imageE)
+
+lemma bij_betwI':
+ "\<lbrakk>\<And>x y. \<lbrakk>x \<in> X; y \<in> X\<rbrakk> \<Longrightarrow> (f x = f y) = (x = y);
+ \<And>x. x \<in> X \<Longrightarrow> f x \<in> Y;
+ \<And>y. y \<in> Y \<Longrightarrow> \<exists>x \<in> X. y = f x\<rbrakk> \<Longrightarrow> bij_betw f X Y"
+unfolding bij_betw_def inj_on_def by auto (metis rev_image_eqI)
+
+lemma o_bij:
+ assumes gf: "g o f = id" and fg: "f o g = id"
+ shows "bij f"
+unfolding bij_def inj_on_def surj_def proof safe
+ fix a1 a2 assume "f a1 = f a2"
+ hence "g ( f a1) = g (f a2)" by simp
+ thus "a1 = a2" using gf unfolding fun_eq_iff by simp
+next
+ fix b
+ have "b = f (g b)"
+ using fg unfolding fun_eq_iff by simp
+ thus "EX a. b = f a" by blast
+qed
+
+lemma surj_fun_eq:
+ assumes surj_on: "f ` X = UNIV" and eq_on: "\<forall>x \<in> X. (g1 o f) x = (g2 o f) x"
+ shows "g1 = g2"
+proof (rule ext)
+ fix y
+ from surj_on obtain x where "x \<in> X" and "y = f x" by blast
+ thus "g1 y = g2 y" using eq_on by simp
+qed
+
+lemma Card_order_wo_rel: "Card_order r \<Longrightarrow> wo_rel r"
+unfolding wo_rel_def card_order_on_def by blast
+
+lemma Cinfinite_limit: "\<lbrakk>x \<in> Field r; Cinfinite r\<rbrakk> \<Longrightarrow>
+ \<exists>y \<in> Field r. x \<noteq> y \<and> (x, y) \<in> r"
+unfolding cinfinite_def by (auto simp add: infinite_Card_order_limit)
+
+lemma Card_order_trans:
+ "\<lbrakk>Card_order r; x \<noteq> y; (x, y) \<in> r; y \<noteq> z; (y, z) \<in> r\<rbrakk> \<Longrightarrow> x \<noteq> z \<and> (x, z) \<in> r"
+unfolding card_order_on_def well_order_on_def linear_order_on_def
+ partial_order_on_def preorder_on_def trans_def antisym_def by blast
+
+lemma Cinfinite_limit2:
+ assumes x1: "x1 \<in> Field r" and x2: "x2 \<in> Field r" and r: "Cinfinite r"
+ shows "\<exists>y \<in> Field r. (x1 \<noteq> y \<and> (x1, y) \<in> r) \<and> (x2 \<noteq> y \<and> (x2, y) \<in> r)"
+proof -
+ from r have trans: "trans r" and total: "Total r" and antisym: "antisym r"
+ unfolding card_order_on_def well_order_on_def linear_order_on_def
+ partial_order_on_def preorder_on_def by auto
+ obtain y1 where y1: "y1 \<in> Field r" "x1 \<noteq> y1" "(x1, y1) \<in> r"
+ using Cinfinite_limit[OF x1 r] by blast
+ obtain y2 where y2: "y2 \<in> Field r" "x2 \<noteq> y2" "(x2, y2) \<in> r"
+ using Cinfinite_limit[OF x2 r] by blast
+ show ?thesis
+ proof (cases "y1 = y2")
+ case True with y1 y2 show ?thesis by blast
+ next
+ case False
+ with y1(1) y2(1) total have "(y1, y2) \<in> r \<or> (y2, y1) \<in> r"
+ unfolding total_on_def by auto
+ thus ?thesis
+ proof
+ assume *: "(y1, y2) \<in> r"
+ with trans y1(3) have "(x1, y2) \<in> r" unfolding trans_def by blast
+ with False y1 y2 * antisym show ?thesis by (cases "x1 = y2") (auto simp: antisym_def)
+ next
+ assume *: "(y2, y1) \<in> r"
+ with trans y2(3) have "(x2, y1) \<in> r" unfolding trans_def by blast
+ with False y1 y2 * antisym show ?thesis by (cases "x2 = y1") (auto simp: antisym_def)
+ qed
+ qed
+qed
+
+lemma Cinfinite_limit_finite: "\<lbrakk>finite X; X \<subseteq> Field r; Cinfinite r\<rbrakk>
+ \<Longrightarrow> \<exists>y \<in> Field r. \<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)"
+proof (induct X rule: finite_induct)
+ case empty thus ?case unfolding cinfinite_def using ex_in_conv[of "Field r"] finite.emptyI by auto
+next
+ case (insert x X)
+ then obtain y where y: "y \<in> Field r" "\<forall>x \<in> X. (x \<noteq> y \<and> (x, y) \<in> r)" by blast
+ then obtain z where z: "z \<in> Field r" "x \<noteq> z \<and> (x, z) \<in> r" "y \<noteq> z \<and> (y, z) \<in> r"
+ using Cinfinite_limit2[OF _ y(1) insert(5), of x] insert(4) by blast
+ show ?case by (metis Card_order_trans insert(5) insertE y(2) z)
+qed
+
+lemma insert_subsetI: "\<lbrakk>x \<in> A; X \<subseteq> A\<rbrakk> \<Longrightarrow> insert x X \<subseteq> A"
+by auto
+
+(*helps resolution*)
+lemma well_order_induct_imp:
+ "wo_rel r \<Longrightarrow> (\<And>x. \<forall>y. y \<noteq> x \<and> (y, x) \<in> r \<longrightarrow> y \<in> Field r \<longrightarrow> P y \<Longrightarrow> x \<in> Field r \<longrightarrow> P x) \<Longrightarrow>
+ x \<in> Field r \<longrightarrow> P x"
+by (erule wo_rel.well_order_induct)
+
+lemma meta_spec2:
+ assumes "(\<And>x y. PROP P x y)"
+ shows "PROP P x y"
+by (rule `(\<And>x y. PROP P x y)`)
+
+(*Extended Sublist*)
+
+definition prefCl where
+ "prefCl Kl = (\<forall> kl1 kl2. kl1 \<le> kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl)"
+definition PrefCl where
+ "PrefCl A n = (\<forall>kl kl'. kl \<in> A n \<and> kl' \<le> kl \<longrightarrow> (\<exists>m\<le>n. kl' \<in> A m))"
+
+lemma prefCl_UN:
+ "\<lbrakk>\<And>n. PrefCl A n\<rbrakk> \<Longrightarrow> prefCl (\<Union>n. A n)"
+unfolding prefCl_def PrefCl_def by fastforce
+
+definition Succ where "Succ Kl kl = {k . kl @ [k] \<in> Kl}"
+definition Shift where "Shift Kl k = {kl. k # kl \<in> Kl}"
+definition shift where "shift lab k = (\<lambda>kl. lab (k # kl))"
+
+lemmas sh_def = Shift_def shift_def
+
+lemma empty_Shift: "\<lbrakk>[] \<in> Kl; k \<in> Succ Kl []\<rbrakk> \<Longrightarrow> [] \<in> Shift Kl k"
+unfolding Shift_def Succ_def by simp
+
+lemma Shift_clists: "Kl \<subseteq> Field (clists r) \<Longrightarrow> Shift Kl k \<subseteq> Field (clists r)"
+unfolding Shift_def clists_def Field_card_of by auto
+
+lemma Shift_prefCl: "prefCl Kl \<Longrightarrow> prefCl (Shift Kl k)"
+unfolding prefCl_def Shift_def
+proof safe
+ fix kl1 kl2
+ assume "\<forall>kl1 kl2. kl1 \<le> kl2 \<and> kl2 \<in> Kl \<longrightarrow> kl1 \<in> Kl"
+ "kl1 \<le> kl2" "k # kl2 \<in> Kl"
+ thus "k # kl1 \<in> Kl" using Cons_prefix_Cons[of k kl1 k kl2] by blast
+qed
+
+lemma not_in_Shift: "kl \<notin> Shift Kl x \<Longrightarrow> x # kl \<notin> Kl"
+unfolding Shift_def by simp
+
+lemma prefCl_Succ: "\<lbrakk>prefCl Kl; k # kl \<in> Kl\<rbrakk> \<Longrightarrow> k \<in> Succ Kl []"
+unfolding Succ_def proof
+ assume "prefCl Kl" "k # kl \<in> Kl"
+ moreover have "k # [] \<le> k # kl" by auto
+ ultimately have "k # [] \<in> Kl" unfolding prefCl_def by blast
+ thus "[] @ [k] \<in> Kl" by simp
+qed
+
+lemma SuccD: "k \<in> Succ Kl kl \<Longrightarrow> kl @ [k] \<in> Kl"
+unfolding Succ_def by simp
+
+lemmas SuccE = SuccD[elim_format]
+
+lemma SuccI: "kl @ [k] \<in> Kl \<Longrightarrow> k \<in> Succ Kl kl"
+unfolding Succ_def by simp
+
+lemma ShiftD: "kl \<in> Shift Kl k \<Longrightarrow> k # kl \<in> Kl"
+unfolding Shift_def by simp
+
+lemma Succ_Shift: "Succ (Shift Kl k) kl = Succ Kl (k # kl)"
+unfolding Succ_def Shift_def by auto
+
+lemma ShiftI: "k # kl \<in> Kl \<Longrightarrow> kl \<in> Shift Kl k"
+unfolding Shift_def by simp
+
+lemma Func_cexp: "|Func A B| =o |B| ^c |A|"
+unfolding cexp_def Field_card_of by (simp only: card_of_refl)
+
+lemma clists_bound: "A \<in> Field (cpow (clists r)) - {{}} \<Longrightarrow> |A| \<le>o clists r"
+unfolding cpow_def clists_def Field_card_of by (auto simp: card_of_mono1)
+
+lemma cpow_clists_czero: "\<lbrakk>A \<in> Field (cpow (clists r)) - {{}}; |A| =o czero\<rbrakk> \<Longrightarrow> False"
+unfolding cpow_def clists_def
+by (auto simp add: card_of_ordIso_czero_iff_empty[symmetric])
+ (erule notE, erule ordIso_transitive, rule czero_ordIso)
+
+lemma incl_UNION_I:
+assumes "i \<in> I" and "A \<subseteq> F i"
+shows "A \<subseteq> UNION I F"
+using assms by auto
+
+lemma Nil_clists: "{[]} \<subseteq> Field (clists r)"
+unfolding clists_def Field_card_of by auto
+
+lemma Cons_clists:
+ "\<lbrakk>x \<in> Field r; xs \<in> Field (clists r)\<rbrakk> \<Longrightarrow> x # xs \<in> Field (clists r)"
+unfolding clists_def Field_card_of by auto
+
+lemma length_Cons: "length (x#xs) = Suc (length xs)"
+by simp
+
+lemma length_append_singleton: "length (xs @ [x]) = Suc (length xs)"
+by simp
+
+(*injection into the field of a cardinal*)
+definition "toCard_pred A r f \<equiv> inj_on f A \<and> f ` A \<subseteq> Field r \<and> Card_order r"
+definition "toCard A r \<equiv> SOME f. toCard_pred A r f"
+
+lemma ex_toCard_pred:
+"\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> \<exists> f. toCard_pred A r f"
+unfolding toCard_pred_def
+using card_of_ordLeq[of A "Field r"]
+ ordLeq_ordIso_trans[OF _ card_of_unique[of "Field r" r], of "|A|"]
+by blast
+
+lemma toCard_pred_toCard:
+ "\<lbrakk>|A| \<le>o r; Card_order r\<rbrakk> \<Longrightarrow> toCard_pred A r (toCard A r)"
+unfolding toCard_def using someI_ex[OF ex_toCard_pred] .
+
+lemma toCard_inj: "\<lbrakk>|A| \<le>o r; Card_order r; x \<in> A; y \<in> A\<rbrakk> \<Longrightarrow>
+ toCard A r x = toCard A r y \<longleftrightarrow> x = y"
+using toCard_pred_toCard unfolding inj_on_def toCard_pred_def by blast
+
+lemma toCard: "\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> toCard A r b \<in> Field r"
+using toCard_pred_toCard unfolding toCard_pred_def by blast
+
+definition "fromCard A r k \<equiv> SOME b. b \<in> A \<and> toCard A r b = k"
+
+lemma fromCard_toCard:
+"\<lbrakk>|A| \<le>o r; Card_order r; b \<in> A\<rbrakk> \<Longrightarrow> fromCard A r (toCard A r b) = b"
+unfolding fromCard_def by (rule some_equality) (auto simp add: toCard_inj)
+
+(* pick according to the weak pullback *)
+definition pickWP_pred where
+"pickWP_pred A p1 p2 b1 b2 a \<equiv>
+ a \<in> A \<and> p1 a = b1 \<and> p2 a = b2"
+
+definition pickWP where
+"pickWP A p1 p2 b1 b2 \<equiv>
+ SOME a. pickWP_pred A p1 p2 b1 b2 a"
+
+lemma pickWP_pred:
+assumes "wpull A B1 B2 f1 f2 p1 p2" and
+"b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2"
+shows "\<exists> a. pickWP_pred A p1 p2 b1 b2 a"
+using assms unfolding wpull_def pickWP_pred_def by blast
+
+lemma pickWP_pred_pickWP:
+assumes "wpull A B1 B2 f1 f2 p1 p2" and
+"b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2"
+shows "pickWP_pred A p1 p2 b1 b2 (pickWP A p1 p2 b1 b2)"
+unfolding pickWP_def using assms by(rule someI_ex[OF pickWP_pred])
+
+lemma pickWP:
+assumes "wpull A B1 B2 f1 f2 p1 p2" and
+"b1 \<in> B1" and "b2 \<in> B2" and "f1 b1 = f2 b2"
+shows "pickWP A p1 p2 b1 b2 \<in> A"
+ "p1 (pickWP A p1 p2 b1 b2) = b1"
+ "p2 (pickWP A p1 p2 b1 b2) = b2"
+using assms pickWP_pred_pickWP unfolding pickWP_pred_def by fastforce+
+
+lemma ssubst_mem: "\<lbrakk>t = s; s \<in> X\<rbrakk> \<Longrightarrow> t \<in> X" by simp
+
+lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
+unfolding Field_card_of csum_def by auto
+
+lemma Inr_Field_csum: "a \<in> Field s \<Longrightarrow> Inr a \<in> Field (r +c s)"
+unfolding Field_card_of csum_def by auto
+
+lemma nat_rec_0: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f 0 = f1"
+by auto
+
+lemma nat_rec_Suc: "f = nat_rec f1 (%n rec. f2 n rec) \<Longrightarrow> f (Suc n) = f2 n (f n)"
+by auto
+
+lemma list_rec_Nil: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f [] = f1"
+by auto
+
+lemma list_rec_Cons: "f = list_rec f1 (%x xs rec. f2 x xs rec) \<Longrightarrow> f (x # xs) = f2 x xs (f xs)"
+by auto
+
+lemma sum_case_cong: "p = q \<Longrightarrow> sum_case f g p = sum_case f g q"
+by simp
+
+lemma sum_case_step:
+ "sum_case (sum_case f' g') g (Inl p) = sum_case f' g' p"
+ "sum_case f (sum_case f' g') (Inr p) = sum_case f' g' p"
+by auto
+
+lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+by simp
+
+lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
+by blast
+
+lemma obj_sumE_f:
+"\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f x \<longrightarrow> P"
+by (metis sum.exhaust)
+
+lemma obj_sumE: "\<lbrakk>\<forall>x. s = Inl x \<longrightarrow> P; \<forall>x. s = Inr x \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
+by (cases s) auto
+
+lemma obj_sum_step:
+ "\<lbrakk>\<forall>x. s = f (Inr (Inl x)) \<longrightarrow> P; \<forall>x. s = f (Inr (Inr x)) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f (Inr x) \<longrightarrow> P"
+by (metis obj_sumE)
+
+lemma sum_case_if:
+"sum_case f g (if p then Inl x else Inr y) = (if p then f x else g y)"
+by simp
+
+lemma not_arg_cong_Inr: "x \<noteq> y \<Longrightarrow> Inr x \<noteq> Inr y"
+by simp
+
+ML_file "Tools/bnf_util.ML"
+ML_file "Tools/bnf_tactics.ML"
+
+end
--- a/src/HOL/Codatatype/BNF_Wrap.thy Tue Sep 11 19:43:06 2012 +0200
+++ b/src/HOL/Codatatype/BNF_Wrap.thy Tue Sep 11 19:45:12 2012 +0200
@@ -8,9 +8,10 @@
header {* Wrapping Datatypes *}
theory BNF_Wrap
-imports BNF_Def
+imports BNF_Util
keywords
- "wrap_data" :: thy_goal
+ "wrap_data" :: thy_goal and
+ "no_dests"
uses
"Tools/bnf_wrap_tactics.ML"
"Tools/bnf_wrap.ML"
--- a/src/HOL/Codatatype/Codatatype.thy Tue Sep 11 19:43:06 2012 +0200
+++ b/src/HOL/Codatatype/Codatatype.thy Tue Sep 11 19:45:12 2012 +0200
@@ -10,11 +10,11 @@
header {* The (Co)datatype Package *}
theory Codatatype
-imports BNF_Wrap BNF_LFP BNF_GFP
+imports BNF_LFP BNF_GFP BNF_Wrap
keywords
- "data" :: thy_decl
-and
- "codata" :: thy_decl
+ "data" :: thy_decl and
+ "codata" :: thy_decl and
+ "defaults"
uses
"Tools/bnf_fp_sugar_tactics.ML"
"Tools/bnf_fp_sugar.ML"
--- a/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML Tue Sep 11 19:43:06 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_comp_tactics.ML Tue Sep 11 19:45:12 2012 +0200
@@ -33,6 +33,9 @@
val mk_permute_in_alt_tac: ''a list -> ''a list -> tactic
val mk_permute_in_bd_tac: ''a list -> ''a list -> thm -> thm -> thm -> tactic
+
+ val mk_map_wpull_tac: thm -> thm list -> thm -> tactic
+ val mk_simple_wit_tac: thm list -> tactic
end;
structure BNF_Comp_Tactics : BNF_COMP_TACTICS =
@@ -391,4 +394,11 @@
TRY o rtac @{thm csum_Cnotzero2} THEN'
rtac @{thm ctwo_Cnotzero}) 1;
+fun mk_map_wpull_tac comp_in_alt inner_map_wpulls outer_map_wpull =
+ (rtac (@{thm wpull_cong} OF (replicate 3 comp_in_alt)) THEN' rtac outer_map_wpull) 1 THEN
+ WRAP (fn thm => rtac thm 1 THEN REPEAT_DETERM (atac 1)) (K all_tac) inner_map_wpulls all_tac THEN
+ TRY (REPEAT_DETERM (atac 1 ORELSE rtac @{thm wpull_id} 1));
+
+fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));
+
end;
--- a/src/HOL/Codatatype/Tools/bnf_def.ML Tue Sep 11 19:43:06 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_def.ML Tue Sep 11 19:45:12 2012 +0200
@@ -98,7 +98,7 @@
struct
open BNF_Util
-open BNF_Tactics
+open BNF_Def_Tactics
type axioms = {
map_id: thm,
@@ -1182,8 +1182,7 @@
map2 (Thm.close_derivation oo Skip_Proof.prove lthy [] [])
goals (map (unfold_defs_tac lthy defs) tacs)
|> (fn thms => after_qed (map single thms @ wit_thms) lthy)
- end) oo prepare_def const_policy fact_policy qualify
- (singleton o Type_Infer_Context.infer_types) Ds;
+ end) oo prepare_def const_policy fact_policy qualify (K I) Ds;
val bnf_def_cmd = (fn (goals, wit_goals, after_qed, lthy, defs) =>
Proof.unfolding ([[(defs, [])]])
@@ -1222,8 +1221,8 @@
val _ =
Outer_Syntax.local_theory_to_proof @{command_spec "bnf_def"} "define a BNF for an existing type"
- (((Parse.binding --| Parse.$$$ "=") -- Parse.term --
- (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- Parse.term --
- (Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]")) >> bnf_def_cmd);
+ (((Parse.binding --| @{keyword "="}) -- Parse.term --
+ (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) -- Parse.term --
+ (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"})) >> bnf_def_cmd);
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Codatatype/Tools/bnf_def_tactics.ML Tue Sep 11 19:45:12 2012 +0200
@@ -0,0 +1,209 @@
+(* Title: HOL/Codatatype/Tools/bnf_def_tactics.ML
+ Author: Dmitriy Traytel, TU Muenchen
+ Author: Jasmin Blanchette, TU Muenchen
+ Copyright 2012
+
+Tactics for definition of bounded natural functors.
+*)
+
+signature BNF_DEF_TACTICS =
+sig
+ val mk_collect_set_natural_tac: Proof.context -> thm list -> tactic
+ val mk_id': thm -> thm
+ val mk_comp': thm -> thm
+ val mk_in_mono_tac: int -> tactic
+ val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
+ val mk_set_natural': thm -> thm
+
+ val mk_rel_Gr_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
+ {prems: thm list, context: Proof.context} -> tactic
+ val mk_rel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
+ val mk_rel_O_tac: thm -> thm -> thm -> thm -> thm -> thm list ->
+ {prems: thm list, context: Proof.context} -> tactic
+ val mk_in_rel_tac: thm -> int -> {prems: 'b, context: Proof.context} -> tactic
+ val mk_rel_converse_tac: thm -> tactic
+ val mk_rel_converse_le_tac: thm -> thm -> thm -> thm -> thm list ->
+ {prems: thm list, context: Proof.context} -> tactic
+ val mk_rel_mono_tac: thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
+end;
+
+structure BNF_Def_Tactics : BNF_DEF_TACTICS =
+struct
+
+open BNF_Util
+open BNF_Tactics
+
+val set_mp = @{thm set_mp};
+
+fun mk_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply};
+fun mk_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
+fun mk_set_natural' set_natural = set_natural RS @{thm pointfreeE};
+fun mk_in_mono_tac n = if n = 0 then rtac @{thm subset_UNIV} 1
+ else (rtac subsetI THEN'
+ rtac CollectI) 1 THEN
+ REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN
+ REPEAT_DETERM_N (n - 1)
+ ((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN
+ (etac subset_trans THEN' atac) 1;
+
+fun mk_collect_set_natural_tac ctxt set_naturals =
+ substs_tac ctxt (@{thms collect_o image_insert image_empty} @ set_naturals) 1 THEN rtac refl 1;
+
+fun mk_map_wppull_tac map_id map_cong map_wpull map_comp set_naturals =
+ if null set_naturals then
+ EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1
+ else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull},
+ REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull,
+ REPEAT_DETERM o rtac @{thm wpull_thePull}, rtac ballI,
+ REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac CollectI,
+ CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
+ rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac])
+ set_naturals,
+ CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans),
+ rtac (map_comp RS trans RS sym), rtac map_cong,
+ REPEAT_DETERM_N (length set_naturals) o EVERY' [rtac (o_apply RS trans),
+ rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm,
+ rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1;
+
+fun mk_rel_Gr_tac rel_def map_id map_cong map_wpull in_cong map_id' map_comp set_naturals
+ {context = ctxt, prems = _} =
+ let
+ val n = length set_naturals;
+ in
+ if null set_naturals then
+ Local_Defs.unfold_tac ctxt [rel_def] THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
+ else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN
+ EVERY' [rtac equalityI, rtac subsetI,
+ REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
+ REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+ REPEAT_DETERM o etac conjE, hyp_subst_tac,
+ rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+ rtac sym, rtac trans, rtac map_comp, rtac map_cong,
+ REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac,
+ REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
+ rtac (o_apply RS trans), rtac (@{thm fst_conv} RS arg_cong RS trans),
+ rtac (@{thm snd_conv} RS sym)],
+ rtac CollectI,
+ CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
+ rtac @{thm image_subsetI}, dtac @{thm set_rev_mp}, atac,
+ REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
+ stac @{thm fst_conv}, atac]) set_naturals,
+ rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE],
+ REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+ REPEAT_DETERM o etac conjE, hyp_subst_tac,
+ rtac allE, rtac subst, rtac @{thm wpull_def}, rtac map_wpull,
+ REPEAT_DETERM_N n o rtac @{thm wpull_Gr}, etac allE, etac impE, rtac conjI, atac,
+ rtac conjI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
+ CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
+ rtac @{thm image_mono}, atac]) set_naturals,
+ rtac sym, rtac map_id', REPEAT_DETERM o eresolve_tac [bexE, conjE],
+ rtac @{thm relcompI}, rtac @{thm converseI},
+ REPEAT_DETERM_N 2 o EVERY' [rtac CollectI, rtac exI,
+ rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, etac sym,
+ etac @{thm set_rev_mp}, rtac equalityD1, rtac in_cong,
+ REPEAT_DETERM_N n o rtac @{thm Gr_def}]] 1
+ end;
+
+fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} =
+ Local_Defs.unfold_tac ctxt [rel_Gr, @{thm Id_alt}] THEN
+ subst_tac ctxt [map_id] 1 THEN
+ (if n = 0 then rtac refl 1
+ else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
+ rtac equalityI, rtac @{thm subset_UNIV}, rtac subsetI, rtac CollectI,
+ CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto n), rtac refl] 1);
+
+fun mk_rel_mono_tac rel_def in_mono {context = ctxt, prems = _} =
+ Local_Defs.unfold_tac ctxt [rel_def] THEN
+ EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]},
+ rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac,
+ rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1;
+
+fun mk_rel_converse_le_tac rel_def rel_Id map_cong map_comp set_naturals
+ {context = ctxt, prems = _} =
+ let
+ val n = length set_naturals;
+ in
+ if null set_naturals then
+ Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
+ else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN
+ EVERY' [rtac @{thm subrelI},
+ REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
+ REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+ REPEAT_DETERM o etac conjE, hyp_subst_tac, rtac @{thm converseI},
+ rtac @{thm relcompI}, rtac @{thm converseI},
+ EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
+ rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac trans,
+ rtac map_cong, REPEAT_DETERM_N n o rtac thm,
+ rtac (map_comp RS sym), rtac CollectI,
+ CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
+ etac @{thm flip_rel}]) set_naturals]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
+ end;
+
+fun mk_rel_converse_tac le_converse =
+ EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift},
+ rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1;
+
+fun mk_rel_O_tac rel_def rel_Id map_cong map_wppull map_comp set_naturals
+ {context = ctxt, prems = _} =
+ let
+ val n = length set_naturals;
+ fun in_tac nthO_in = rtac CollectI THEN'
+ CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
+ rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals;
+ in
+ if null set_naturals then Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
+ else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN
+ EVERY' [rtac equalityI, rtac @{thm subrelI},
+ REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
+ REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+ REPEAT_DETERM o etac conjE, hyp_subst_tac,
+ rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI},
+ rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+ rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
+ REPEAT_DETERM_N n o rtac @{thm fst_fstO},
+ in_tac @{thm fstO_in},
+ rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+ rtac sym, rtac trans, rtac map_comp, rtac map_cong,
+ REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, rtac ballE, rtac subst,
+ rtac @{thm csquare_def}, rtac @{thm csquare_fstO_sndO}, atac, etac notE,
+ etac set_mp, atac],
+ in_tac @{thm fstO_in},
+ rtac @{thm relcompI}, rtac @{thm converseI},
+ rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+ rtac sym, rtac trans, rtac map_comp, rtac map_cong,
+ REPEAT_DETERM_N n o rtac o_apply,
+ in_tac @{thm sndO_in},
+ rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
+ rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
+ REPEAT_DETERM_N n o rtac @{thm snd_sndO},
+ in_tac @{thm sndO_in},
+ rtac @{thm subrelI},
+ REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
+ REPEAT_DETERM o eresolve_tac [exE, conjE],
+ REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
+ REPEAT_DETERM o etac conjE, hyp_subst_tac,
+ rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull,
+ CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_naturals,
+ etac allE, etac impE, etac conjI, etac conjI, atac,
+ REPEAT_DETERM o eresolve_tac [bexE, conjE],
+ rtac @{thm relcompI}, rtac @{thm converseI},
+ EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
+ rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac sym, rtac trans,
+ rtac trans, rtac map_cong, REPEAT_DETERM_N n o rtac thm,
+ rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1
+ end;
+
+fun mk_in_rel_tac rel_def m {context = ctxt, prems = _} =
+ let
+ val ls' = replicate (Int.max (1, m)) ();
+ in
+ Local_Defs.unfold_tac ctxt (rel_def ::
+ @{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN
+ EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI,
+ rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl,
+ REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI,
+ REPEAT_DETERM_N 2 o EVERY' [rtac exI, rtac conjI, etac @{thm conjI[OF refl sym]},
+ CONJ_WRAP' (K atac) ls']] 1
+ end;
+
+end;
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 11 19:43:06 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML Tue Sep 11 19:45:12 2012 +0200
@@ -48,6 +48,8 @@
val lists_bmoc = fold (fn xs => fn t => Term.list_comb (t, xs))
+fun mk_predT T = T --> HOLogic.boolT;
+
fun mk_id T = Const (@{const_name id}, T --> T);
fun mk_tupled_fun x f xs = HOLogic.tupled_lambda x (Term.list_comb (f, xs));
@@ -58,10 +60,9 @@
fun tick v f = Term.lambda v (HOLogic.mk_prod (v, f $ v));
fun tack z_name (c, v) f =
- let
- val T = fastype_of v;
- val z = Free (z_name, mk_sumT (T, fastype_of c))
- in Term.lambda z (mk_sum_case (mk_id T, Term.lambda c (f $ c)) $ z) end;
+ let val z = Free (z_name, mk_sumT (fastype_of v, fastype_of c)) in
+ Term.lambda z (mk_sum_case (Term.lambda v v, Term.lambda c (f $ c)) $ z)
+ end;
fun cannot_merge_types () = error "Mutually recursive types must have the same type parameters";
@@ -89,13 +90,17 @@
fun mixfix_of ((_, mx), _) = mx;
fun ctr_specs_of (_, ctr_specs) = ctr_specs;
-fun disc_of (((disc, _), _), _) = disc;
-fun ctr_of (((_, ctr), _), _) = ctr;
-fun args_of ((_, args), _) = args;
+fun disc_of ((((disc, _), _), _), _) = disc;
+fun ctr_of ((((_, ctr), _), _), _) = ctr;
+fun args_of (((_, args), _), _) = args;
+fun defaults_of ((_, ds), _) = ds;
fun ctr_mixfix_of (_, mx) = mx;
-fun prepare_datatype prepare_typ lfp specs fake_lthy no_defs_lthy =
+fun prepare_datatype prepare_typ prepare_term lfp (no_dests, specs) fake_lthy no_defs_lthy =
let
+ val _ = if not lfp andalso no_dests then error "Cannot define destructor-less codatatypes"
+ else ();
+
val constrained_As =
map (map (apfst (prepare_typ fake_lthy)) o type_args_constrained_of) specs
|> Library.foldr1 (merge_type_args_constrained no_defs_lthy);
@@ -132,6 +137,8 @@
val sel_bindersss = map (map (map fst)) ctr_argsss;
val fake_ctr_Tsss = map (map (map (prepare_typ fake_lthy o snd))) ctr_argsss;
+ val raw_sel_defaultsss = map (map defaults_of) ctr_specss;
+
val rhs_As' = fold (fold (fold Term.add_tfreesT)) fake_ctr_Tsss [];
val _ = (case subtract (op =) As' rhs_As' of
[] => ()
@@ -211,12 +218,8 @@
val fp_iter_fun_Ts = fst (split_last (binder_types (fastype_of fp_iter1)));
val fp_rec_fun_Ts = fst (split_last (binder_types (fastype_of fp_rec1)));
- fun dest_rec_pair (T as Type (@{type_name prod}, Us as [_, U])) =
- if member (op =) Cs U then Us else [T]
- | dest_rec_pair T = [T];
-
val ((iter_only as (gss, _, _), rec_only as (hss, _, _)),
- (zs, cs, cpss, coiter_only as ((pgss, cgsss), _), corec_only as ((phss, chsss), _))) =
+ (zs, cs, cpss, coiter_only as ((pgss, crgsss), _), corec_only as ((phss, cshsss), _))) =
if lfp then
let
val y_Tsss =
@@ -228,18 +231,25 @@
lthy
|> mk_Freess "f" g_Tss
||>> mk_Freesss "x" y_Tsss;
+ val yssss = map (map (map single)) ysss;
+
+ fun dest_rec_prodT (T as Type (@{type_name prod}, Us as [_, U])) =
+ if member (op =) Cs U then Us else [T]
+ | dest_rec_prodT T = [T];
val z_Tssss =
- map3 (fn n => fn ms => map2 (map dest_rec_pair oo dest_tupleT) ms o
+ map3 (fn n => fn ms => map2 (map dest_rec_prodT oo dest_tupleT) ms o
dest_sumTN_balanced n o domain_type) ns mss fp_rec_fun_Ts;
val h_Tss = map2 (map2 (fold_rev (curry (op --->)))) z_Tssss Css;
val hss = map2 (map2 retype_free) gss h_Tss;
- val (zssss, _) =
+ val zssss_hd = map2 (map2 (map2 (fn y => fn T :: _ => retype_free y T))) ysss z_Tssss;
+ val (zssss_tl, _) =
lthy
- |> mk_Freessss "x" z_Tssss;
+ |> mk_Freessss "y" (map (map (map tl)) z_Tssss);
+ val zssss = map2 (map2 (map2 cons)) zssss_hd zssss_tl;
in
- (((gss, g_Tss, map (map (map single)) ysss), (hss, h_Tss, zssss)),
+ (((gss, g_Tss, yssss), (hss, h_Tss, zssss)),
([], [], [], (([], []), ([], [])), (([], []), ([], []))))
end
else
@@ -247,49 +257,71 @@
(*avoid "'a itself" arguments in coiterators and corecursors*)
val mss' = map (fn [0] => [1] | ms => ms) mss;
- val p_Tss =
- map2 (fn C => fn n => replicate (Int.max (0, n - 1)) (C --> HOLogic.boolT)) Cs ns;
+ val p_Tss = map2 (fn n => replicate (Int.max (0, n - 1)) o mk_predT) ns Cs;
+
+ fun zip_predss_getterss qss fss = maps (op @) (qss ~~ fss);
- fun zip_preds_getters [] [fs] = fs
- | zip_preds_getters (p :: ps) (fs :: fss) = p :: fs @ zip_preds_getters ps fss;
+ fun zip_preds_predsss_gettersss [] [qss] [fss] = zip_predss_getterss qss fss
+ | zip_preds_predsss_gettersss (p :: ps) (qss :: qsss) (fss :: fsss) =
+ p :: zip_predss_getterss qss fss @ zip_preds_predsss_gettersss ps qsss fsss;
- fun mk_types fun_Ts =
+ fun mk_types maybe_dest_sumT fun_Ts =
let
val f_sum_prod_Ts = map range_type fun_Ts;
val f_prod_Tss = map2 dest_sumTN_balanced ns f_sum_prod_Ts;
- val f_Tsss =
- map3 (fn C => map2 (map (curry (op -->) C) oo dest_tupleT)) Cs mss' f_prod_Tss;
- val pf_Tss = map2 zip_preds_getters p_Tss f_Tsss
- in (f_sum_prod_Ts, f_Tsss, pf_Tss) end;
+ val f_Tssss =
+ map3 (fn C => map2 (map (map (curry (op -->) C) o maybe_dest_sumT) oo dest_tupleT))
+ Cs mss' f_prod_Tss;
+ val q_Tssss =
+ map (map (map (fn [_] => [] | [_, C] => [mk_predT (domain_type C)]))) f_Tssss;
+ val pf_Tss = map3 zip_preds_predsss_gettersss p_Tss q_Tssss f_Tssss;
+ in (q_Tssss, f_sum_prod_Ts, f_Tssss, pf_Tss) end;
- val (g_sum_prod_Ts, g_Tsss, pg_Tss) = mk_types fp_iter_fun_Ts;
- val (h_sum_prod_Ts, h_Tsss, ph_Tss) = mk_types fp_rec_fun_Ts;
+ val (r_Tssss, g_sum_prod_Ts, g_Tssss, pg_Tss) = mk_types single fp_iter_fun_Ts;
- val ((((Free (z, _), cs), pss), gsss), _) =
+ val ((((Free (z, _), cs), pss), gssss), _) =
lthy
|> yield_singleton (mk_Frees "z") dummyT
||>> mk_Frees "a" Cs
||>> mk_Freess "p" p_Tss
- ||>> mk_Freesss "g" g_Tsss;
+ ||>> mk_Freessss "g" g_Tssss;
+ val rssss = map (map (map (fn [] => []))) r_Tssss;
+
+ fun dest_corec_sumT (T as Type (@{type_name sum}, Us as [_, U])) =
+ if member (op =) Cs U then Us else [T]
+ | dest_corec_sumT T = [T];
- val hsss = map2 (map2 (map2 retype_free)) gsss h_Tsss;
+ val (s_Tssss, h_sum_prod_Ts, h_Tssss, ph_Tss) = mk_types dest_corec_sumT fp_rec_fun_Ts;
+
+ val hssss_hd = map2 (map2 (map2 (fn [g] => fn T :: _ => retype_free g T))) gssss h_Tssss;
+ val ((sssss, hssss_tl), _) =
+ lthy
+ |> mk_Freessss "q" s_Tssss
+ ||>> mk_Freessss "h" (map (map (map tl)) h_Tssss);
+ val hssss = map2 (map2 (map2 cons)) hssss_hd hssss_tl;
val cpss = map2 (fn c => map (fn p => p $ c)) cs pss;
- fun mk_terms fsss =
+ fun mk_preds_getters_join [] [cf] = cf
+ | mk_preds_getters_join [cq] [cf, cf'] =
+ mk_If cq (mk_Inl (fastype_of cf') cf) (mk_Inr (fastype_of cf) cf');
+
+ fun mk_terms qssss fssss =
let
- val pfss = map2 zip_preds_getters pss fsss;
- val cfsss = map2 (fn c => map (map (fn f => f $ c))) cs fsss
- in (pfss, cfsss) end;
+ val pfss = map3 zip_preds_predsss_gettersss pss qssss fssss;
+ val cqssss = map2 (fn c => map (map (map (fn f => f $ c)))) cs qssss;
+ val cfssss = map2 (fn c => map (map (map (fn f => f $ c)))) cs fssss;
+ val cqfsss = map2 (map2 (map2 mk_preds_getters_join)) cqssss cfssss;
+ in (pfss, cqfsss) end;
in
((([], [], []), ([], [], [])),
- ([z], cs, cpss, (mk_terms gsss, (g_sum_prod_Ts, pg_Tss)),
- (mk_terms hsss, (h_sum_prod_Ts, ph_Tss))))
+ ([z], cs, cpss, (mk_terms rssss gssss, (g_sum_prod_Ts, pg_Tss)),
+ (mk_terms sssss hssss, (h_sum_prod_Ts, ph_Tss))))
end;
- fun pour_some_sugar_on_type (((((((((((((((((b, fpT), C), fld), unf), fp_iter), fp_rec),
+ fun define_ctrs_case_for_type ((((((((((((((((((b, fpT), C), fld), unf), fp_iter), fp_rec),
fld_unf), unf_fld), fld_inject), n), ks), ms), ctr_binders), ctr_mixfixes), ctr_Tss),
- disc_binders), sel_binderss) no_defs_lthy =
+ disc_binders), sel_binderss), raw_sel_defaultss) no_defs_lthy =
let
val unfT = domain_type (fastype_of fld);
val ctr_prod_Ts = map HOLogic.mk_tupleT ctr_Tss;
@@ -368,7 +400,7 @@
val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss @ [case_tacs];
- fun some_lfp_sugar ((selss0, discIs, sel_thmss), no_defs_lthy) =
+ fun define_iter_rec ((selss0, discIs, sel_thmss), no_defs_lthy) =
let
val fpT_to_C = fpT --> C;
@@ -384,11 +416,11 @@
map2 (mk_sum_caseN_balanced oo map2 mk_uncurried2_fun) fss xssss));
in (binder, spec) end;
- val iter_likes =
+ val iter_like_bundles =
[(iterN, fp_iter, iter_only),
(recN, fp_rec, rec_only)];
- val (binders, specs) = map generate_iter_like iter_likes |> split_list;
+ val (binders, specs) = map generate_iter_like iter_like_bundles |> split_list;
val ((csts, defs), (lthy', lthy)) = no_defs_lthy
|> apfst split_list o fold_map2 (fn b => fn spec =>
@@ -407,31 +439,32 @@
lthy)
end;
- fun some_gfp_sugar ((selss0, discIs, sel_thmss), no_defs_lthy) =
+ fun define_coiter_corec ((selss0, discIs, sel_thmss), no_defs_lthy) =
let
val B_to_fpT = C --> fpT;
- fun generate_coiter_like (suf, fp_iter_like, ((pfss, cfsss), (f_sum_prod_Ts, pf_Tss))) =
+ fun mk_preds_getterss_join c n cps sum_prod_T cqfss =
+ Term.lambda c (mk_IfN sum_prod_T cps
+ (map2 (mk_InN_balanced sum_prod_T n) (map HOLogic.mk_tuple cqfss) (1 upto n)));
+
+ fun generate_coiter_like (suf, fp_iter_like, ((pfss, cqfsss), (f_sum_prod_Ts,
+ pf_Tss))) =
let
val res_T = fold_rev (curry (op --->)) pf_Tss B_to_fpT;
val binder = Binding.suffix_name ("_" ^ suf) b;
- fun mk_preds_getters_join c n cps sum_prod_T cfss =
- Term.lambda c (mk_IfN sum_prod_T cps
- (map2 (mk_InN_balanced sum_prod_T n) (map HOLogic.mk_tuple cfss) (1 upto n)));
-
val spec =
mk_Trueprop_eq (lists_bmoc pfss (Free (Binding.name_of binder, res_T)),
Term.list_comb (fp_iter_like,
- map5 mk_preds_getters_join cs ns cpss f_sum_prod_Ts cfsss));
+ map5 mk_preds_getterss_join cs ns cpss f_sum_prod_Ts cqfsss));
in (binder, spec) end;
- val coiter_likes =
+ val coiter_like_bundles =
[(coiterN, fp_iter, coiter_only),
(corecN, fp_rec, corec_only)];
- val (binders, specs) = map generate_coiter_like coiter_likes |> split_list;
+ val (binders, specs) = map generate_coiter_like coiter_like_bundles |> split_list;
val ((csts, defs), (lthy', lthy)) = no_defs_lthy
|> apfst split_list o fold_map2 (fn b => fn spec =>
@@ -449,9 +482,16 @@
((ctrs, selss0, coiter, corec, v, xss, ctr_defs, discIs, sel_thmss, coiter_def,
corec_def), lthy)
end;
+
+ fun wrap lthy =
+ let val sel_defaultss = map (map (apsnd (prepare_term lthy))) raw_sel_defaultss in
+ wrap_datatype tacss (((no_dests, ctrs0), casex0), (disc_binders, (sel_binderss,
+ sel_defaultss))) lthy
+ end;
+
+ val define_iter_likes = if lfp then define_iter_rec else define_coiter_corec;
in
- wrap_datatype tacss ((ctrs0, casex0), (disc_binders, sel_binderss)) lthy'
- |> (if lfp then some_lfp_sugar else some_gfp_sugar)
+ ((wrap, define_iter_likes), lthy')
end;
val pre_map_defs = map map_def_of_bnf pre_bnfs;
@@ -470,7 +510,7 @@
val args = map build_arg TUs;
in Term.list_comb (mapx, args) end;
- fun pour_more_sugar_on_lfps ((ctrss, _, iters, recs, vs, xsss, ctr_defss, _, _, iter_defs,
+ fun derive_iter_rec_thms_for_types ((ctrss, _, iters, recs, vs, xsss, ctr_defss, _, _, iter_defs,
rec_defs), lthy) =
let
val xctrss = map2 (map2 (curry Term.list_comb)) ctrss xsss;
@@ -491,14 +531,14 @@
~1 => build_map (build_call fiter_likes maybe_tick) T U
| j => maybe_tick (nth vs j) (nth fiter_likes j));
- fun mk_U maybe_prodT =
- typ_subst (map2 (fn fpT => fn C => (fpT, maybe_prodT fpT C)) fpTs Cs);
+ fun mk_U maybe_mk_prodT =
+ typ_subst (map2 (fn fpT => fn C => (fpT, maybe_mk_prodT fpT C)) fpTs Cs);
- fun repair_calls fiter_likes maybe_cons maybe_tick maybe_prodT (x as Free (_, T)) =
+ fun repair_calls fiter_likes maybe_cons maybe_tick maybe_mk_prodT (x as Free (_, T)) =
if member (op =) fpTs T then
maybe_cons x [build_call fiter_likes (K I) (T, mk_U (K I) T) $ x]
else if exists_subtype (member (op =) fpTs) T then
- [build_call fiter_likes maybe_tick (T, mk_U maybe_prodT T) $ x]
+ [build_call fiter_likes maybe_tick (T, mk_U maybe_mk_prodT T) $ x]
else
[x];
@@ -514,11 +554,9 @@
val rec_tacss =
map2 (map o mk_iter_like_tac pre_map_defs map_ids rec_defs) fp_rec_thms ctr_defss;
in
- (map2 (map2 (fn goal => fn tac =>
- Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation))
+ (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
goal_iterss iter_tacss,
- map2 (map2 (fn goal => fn tac =>
- Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation))
+ map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
goal_recss rec_tacss)
end;
@@ -533,8 +571,8 @@
lthy |> Local_Theory.notes notes |> snd
end;
- fun pour_more_sugar_on_gfps ((ctrss, selsss, coiters, corecs, vs, _, ctr_defss, discIss,
- sel_thmsss, coiter_defs, corec_defs), lthy) =
+ fun derive_coiter_corec_thms_for_types ((ctrss, selsss, coiters, corecs, vs, _, ctr_defss,
+ discIss, sel_thmsss, coiter_defs, corec_defs), lthy) =
let
val z = the_single zs;
@@ -558,23 +596,24 @@
~1 => build_map (build_call fiter_likes maybe_tack) T U
| j => maybe_tack (nth cs j, nth vs j) (nth fiter_likes j));
- fun mk_U maybe_sumT =
- typ_subst (map2 (fn C => fn fpT => (maybe_sumT fpT C, fpT)) Cs fpTs);
+ fun mk_U maybe_mk_sumT =
+ typ_subst (map2 (fn C => fn fpT => (maybe_mk_sumT fpT C, fpT)) Cs fpTs);
- fun repair_calls fiter_likes maybe_sumT maybe_tack
- (cf as Free (_, Type (_, [_, T])) $ _) =
- if exists_subtype (member (op =) Cs) T then
- build_call fiter_likes maybe_tack (T, mk_U maybe_sumT T) $ cf
- else
- cf;
+ fun repair_calls fiter_likes maybe_mk_sumT maybe_tack cqf =
+ let val T = fastype_of cqf in
+ if exists_subtype (member (op =) Cs) T then
+ build_call fiter_likes maybe_tack (T, mk_U maybe_mk_sumT T) $ cqf
+ else
+ cqf
+ end;
- val cgsss' = map (map (map (repair_calls gcoiters (K I) (K I)))) cgsss;
- val chsss' = map (map (map (repair_calls hcorecs (curry mk_sumT) (tack z)))) chsss;
+ val crgsss' = map (map (map (repair_calls gcoiters (K I) (K I)))) crgsss;
+ val cshsss' = map (map (map (repair_calls hcorecs (curry mk_sumT) (tack z)))) cshsss;
val goal_coiterss =
- map8 (map4 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss mss cgsss';
+ map8 (map4 oooo mk_goal_coiter_like pgss) cs cpss gcoiters ns kss ctrss mss crgsss';
val goal_corecss =
- map8 (map4 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss mss chsss';
+ map8 (map4 oooo mk_goal_coiter_like phss) cs cpss hcorecs ns kss ctrss mss cshsss';
val coiter_tacss =
map3 (map oo mk_coiter_like_tac coiter_defs map_ids) fp_iter_thms pre_map_defs
@@ -583,9 +622,12 @@
map3 (map oo mk_coiter_like_tac corec_defs map_ids) fp_rec_thms pre_map_defs
ctr_defss;
in
- (map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
+ (map2 (map2 (fn goal => fn tac =>
+ Skip_Proof.prove lthy [] [] goal (tac o #context) |> Thm.close_derivation))
goal_coiterss coiter_tacss,
- map2 (map2 (fn goal => fn tac => Skip_Proof.prove lthy [] [] goal (tac o #context)))
+ map2 (map2 (fn goal => fn tac =>
+ Skip_Proof.prove lthy [] [] goal (tac o #context)
+ |> Local_Defs.unfold lthy @{thms sum_case_if} |> Thm.close_derivation))
goal_corecss corec_tacss)
end;
@@ -627,12 +669,15 @@
lthy |> Local_Theory.notes notes |> snd
end;
+ fun wrap_types_and_define_iter_likes ((wraps, define_iter_likess), lthy) =
+ fold_map2 (curry (op o)) define_iter_likess wraps lthy |>> split_list11
+
val lthy' = lthy
- |> fold_map pour_some_sugar_on_type (bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~
+ |> fold_map define_ctrs_case_for_type (bs ~~ fpTs ~~ Cs ~~ flds ~~ unfs ~~ fp_iters ~~
fp_recs ~~ fld_unfs ~~ unf_flds ~~ fld_injects ~~ ns ~~ kss ~~ mss ~~ ctr_binderss ~~
- ctr_mixfixess ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss)
- |>> split_list11
- |> (if lfp then pour_more_sugar_on_lfps else pour_more_sugar_on_gfps);
+ ctr_mixfixess ~~ ctr_Tsss ~~ disc_binderss ~~ sel_bindersss ~~ raw_sel_defaultsss)
+ |>> split_list |> wrap_types_and_define_iter_likes
+ |> (if lfp then derive_iter_rec_thms_for_types else derive_coiter_corec_thms_for_types);
val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
(if lfp then "" else "co") ^ "datatype"));
@@ -640,7 +685,7 @@
(timer; lthy')
end;
-fun datatype_cmd info specs lthy =
+fun datatype_cmd lfp (bundle as (_, specs)) lthy =
let
(* TODO: cleaner handling of fake contexts, without "background_theory" *)
(*the "perhaps o try" below helps gracefully handles the case where the new type is defined in a
@@ -650,26 +695,31 @@
(type_binder_of spec, length (type_args_constrained_of spec), mixfix_of spec)))) specs;
val fake_lthy = Proof_Context.background_theory fake_thy lthy;
in
- prepare_datatype Syntax.read_typ info specs fake_lthy lthy
+ prepare_datatype Syntax.read_typ Syntax.read_term lfp bundle fake_lthy lthy
end;
-val parse_opt_binding_colon = Scan.optional (Parse.binding --| Parse.$$$ ":") no_binder
+val parse_opt_binding_colon = Scan.optional (Parse.binding --| @{keyword ":"}) no_binder
val parse_ctr_arg =
- Parse.$$$ "(" |-- parse_opt_binding_colon -- Parse.typ --| Parse.$$$ ")" ||
+ @{keyword "("} |-- parse_opt_binding_colon -- Parse.typ --| @{keyword ")"} ||
(Parse.typ >> pair no_binder);
+val parse_defaults =
+ @{keyword "("} |-- @{keyword "defaults"} |-- Scan.repeat parse_bound_term --| @{keyword ")"};
+
val parse_single_spec =
Parse.type_args_constrained -- Parse.binding -- Parse.opt_mixfix --
(@{keyword "="} |-- Parse.enum1 "|" (parse_opt_binding_colon -- Parse.binding --
- Scan.repeat parse_ctr_arg -- Parse.opt_mixfix));
+ Scan.repeat parse_ctr_arg -- Scan.optional parse_defaults [] -- Parse.opt_mixfix));
+
+val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_single_spec;
val _ =
Outer_Syntax.local_theory @{command_spec "data"} "define BNF-based inductive datatypes"
- (Parse.and_list1 parse_single_spec >> datatype_cmd true);
+ (parse_datatype >> datatype_cmd true);
val _ =
Outer_Syntax.local_theory @{command_spec "codata"} "define BNF-based coinductive datatypes"
- (Parse.and_list1 parse_single_spec >> datatype_cmd false);
+ (parse_datatype >> datatype_cmd false);
end;
--- a/src/HOL/Codatatype/Tools/bnf_fp_util.ML Tue Sep 11 19:43:06 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_util.ML Tue Sep 11 19:45:12 2012 +0200
@@ -101,6 +101,7 @@
val dest_tupleT: int -> typ -> typ list
val mk_Field: term -> term
+ val mk_If: term -> term -> term -> term
val mk_union: term * term -> term
val mk_sumEN: int -> thm
@@ -258,6 +259,10 @@
val mk_sum_caseN = Library.foldr1 mk_sum_case;
val mk_sum_caseN_balanced = Balanced_Tree.make mk_sum_case;
+fun mk_If p t f =
+ let val T = fastype_of t;
+ in Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ p $ t $ f end;
+
fun mk_Field r =
let val T = fst (dest_relT (fastype_of r));
in Const (@{const_name Field}, mk_relT (T, T) --> HOLogic.mk_setT T) $ r end;
--- a/src/HOL/Codatatype/Tools/bnf_gfp.ML Tue Sep 11 19:43:06 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp.ML Tue Sep 11 19:45:12 2012 +0200
@@ -3006,9 +3006,9 @@
end;
val _ =
- Outer_Syntax.local_theory @{command_spec "codata_raw"} "greatest fixed points for BNF equations"
+ Outer_Syntax.local_theory @{command_spec "codata_raw"} "greatest fixed points of BNF equations"
(Parse.and_list1
- ((Parse.binding --| Parse.$$$ ":") -- (Parse.typ --| Parse.$$$ "=" -- Parse.typ)) >>
+ ((Parse.binding --| @{keyword ":"}) -- (Parse.typ --| @{keyword "="} -- Parse.typ)) >>
(snd oo fp_bnf_cmd bnf_gfp o apsnd split_list o split_list));
end;
--- a/src/HOL/Codatatype/Tools/bnf_gfp_util.ML Tue Sep 11 19:43:06 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_gfp_util.ML Tue Sep 11 19:45:12 2012 +0200
@@ -12,7 +12,6 @@
val dest_listT: typ -> typ
val mk_Cons: term -> term -> term
- val mk_If: term -> term -> term -> term
val mk_Shift: term -> term -> term
val mk_Succ: term -> term -> term
val mk_Times: term * term -> term
@@ -122,10 +121,6 @@
fun mk_size t = HOLogic.size_const (fastype_of t) $ t;
-fun mk_If p t f =
- let val T = fastype_of t;
- in Const (@{const_name If}, HOLogic.boolT --> T --> T --> T) $ p $ t $ f end;
-
fun mk_quotient A R =
let val T = fastype_of A;
in Const (@{const_name quotient}, T --> fastype_of R --> HOLogic.mk_setT T) $ A $ R end;
--- a/src/HOL/Codatatype/Tools/bnf_lfp.ML Tue Sep 11 19:43:06 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_lfp.ML Tue Sep 11 19:45:12 2012 +0200
@@ -1821,9 +1821,9 @@
end;
val _ =
- Outer_Syntax.local_theory @{command_spec "data_raw"} "least fixed points for BNF equations"
+ Outer_Syntax.local_theory @{command_spec "data_raw"} "least fixed points of BNF equations"
(Parse.and_list1
- ((Parse.binding --| Parse.$$$ ":") -- (Parse.typ --| Parse.$$$ "=" -- Parse.typ)) >>
+ ((Parse.binding --| @{keyword ":"}) -- (Parse.typ --| @{keyword "="} -- Parse.typ)) >>
(snd oo fp_bnf_cmd bnf_lfp o apsnd split_list o split_list));
end;
--- a/src/HOL/Codatatype/Tools/bnf_tactics.ML Tue Sep 11 19:43:06 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_tactics.ML Tue Sep 11 19:45:12 2012 +0200
@@ -23,30 +23,11 @@
val mk_Abs_bij_thm: Proof.context -> thm -> thm -> thm
val mk_Abs_inj_thm: thm -> thm
- val mk_Card_order_tac: thm -> tactic
- val mk_collect_set_natural_tac: Proof.context -> thm list -> tactic
- val mk_id': thm -> thm
- val mk_comp': thm -> thm
- val mk_in_mono_tac: int -> tactic
+ val mk_pred_unfold_tac: thm -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
+
val mk_map_comp_id_tac: thm -> tactic
val mk_map_cong_tac: int -> thm -> {prems: 'a, context: Proof.context} -> tactic
val mk_map_congL_tac: int -> thm -> thm -> tactic
- val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
- val mk_map_wpull_tac: thm -> thm list -> thm -> tactic
- val mk_set_natural': thm -> thm
- val mk_simple_wit_tac: thm list -> tactic
-
- val mk_pred_unfold_tac: thm -> thm list -> thm -> {prems: 'a, context: Proof.context} -> tactic
- val mk_rel_Gr_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
- {prems: thm list, context: Proof.context} -> tactic
- val mk_rel_Id_tac: int -> thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
- val mk_rel_O_tac: thm -> thm -> thm -> thm -> thm -> thm list ->
- {prems: thm list, context: Proof.context} -> tactic
- val mk_in_rel_tac: thm -> int -> {prems: 'b, context: Proof.context} -> tactic
- val mk_rel_converse_tac: thm -> tactic
- val mk_rel_converse_le_tac: thm -> thm -> thm -> thm -> thm list ->
- {prems: thm list, context: Proof.context} -> tactic
- val mk_rel_mono_tac: thm -> thm -> {prems: 'a, context: Proof.context} -> tactic
end;
structure BNF_Tactics : BNF_TACTICS =
@@ -56,8 +37,6 @@
fun ss_only thms = Simplifier.clear_ss HOL_basic_ss addsimps thms;
-val set_mp = @{thm set_mp};
-
fun select_prem_tac n tac k = DETERM o (EVERY' [REPEAT_DETERM_N (k - 1) o etac thin_rl,
tac, REPEAT_DETERM_N (n - k) o etac thin_rl]);
@@ -108,206 +87,22 @@
gen_tac
end;
-fun mk_Card_order_tac card_order =
- (rtac conjE THEN'
- rtac @{thm card_order_on_Card_order} THEN'
- rtac card_order THEN'
- atac) 1;
-
-fun mk_id' id = mk_trans (fun_cong OF [id]) @{thm id_apply};
-fun mk_comp' comp = @{thm o_eq_dest_lhs} OF [mk_sym comp];
-fun mk_set_natural' set_natural = set_natural RS @{thm pointfreeE};
-fun mk_in_mono_tac n = if n = 0 then rtac @{thm subset_UNIV} 1
- else (rtac subsetI THEN'
- rtac CollectI) 1 THEN
- REPEAT_DETERM (eresolve_tac [CollectE, conjE] 1) THEN
- REPEAT_DETERM_N (n - 1)
- ((rtac conjI THEN' etac subset_trans THEN' atac) 1) THEN
- (etac subset_trans THEN' atac) 1;
-
-fun mk_map_wpull_tac comp_in_alt inner_map_wpulls outer_map_wpull =
- (rtac (@{thm wpull_cong} OF (replicate 3 comp_in_alt)) THEN' rtac outer_map_wpull) 1 THEN
- WRAP (fn thm => rtac thm 1 THEN REPEAT_DETERM (atac 1)) (K all_tac) inner_map_wpulls all_tac THEN
- TRY (REPEAT_DETERM (atac 1 ORELSE rtac @{thm wpull_id} 1));
-
-fun mk_collect_set_natural_tac ctxt set_naturals =
- substs_tac ctxt (@{thms collect_o image_insert image_empty} @ set_naturals) 1 THEN rtac refl 1;
-
-fun mk_simple_wit_tac wit_thms = ALLGOALS (atac ORELSE' eresolve_tac (@{thm emptyE} :: wit_thms));
+fun mk_pred_unfold_tac pred_def pred_defs rel_unfold {context = ctxt, prems = _} =
+ Local_Defs.unfold_tac ctxt (@{thm mem_Collect_eq_split} :: pred_def :: pred_defs) THEN
+ rtac rel_unfold 1;
fun mk_map_comp_id_tac map_comp =
(rtac trans THEN' rtac map_comp) 1 THEN
REPEAT_DETERM (stac @{thm o_id} 1) THEN
rtac refl 1;
+fun mk_map_cong_tac m map_cong {context = ctxt, prems = _} =
+ EVERY' [rtac mp, rtac map_cong,
+ CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1;
+
fun mk_map_congL_tac passive map_cong map_id' =
(rtac trans THEN' rtac map_cong THEN' EVERY' (replicate passive (rtac refl))) 1 THEN
REPEAT_DETERM (EVERY' [rtac trans, etac bspec, atac, rtac sym, rtac @{thm id_apply}] 1) THEN
rtac map_id' 1;
-fun mk_map_wppull_tac map_id map_cong map_wpull map_comp set_naturals =
- if null set_naturals then
- EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id, rtac map_id] 1
- else EVERY' [REPEAT_DETERM o etac conjE, REPEAT_DETERM o dtac @{thm wppull_thePull},
- REPEAT_DETERM o etac exE, rtac @{thm wpull_wppull}, rtac map_wpull,
- REPEAT_DETERM o rtac @{thm wpull_thePull}, rtac ballI,
- REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac conjI, rtac CollectI,
- CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
- rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac])
- set_naturals,
- CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans),
- rtac (map_comp RS trans RS sym), rtac map_cong,
- REPEAT_DETERM_N (length set_naturals) o EVERY' [rtac (o_apply RS trans),
- rtac (o_apply RS trans RS sym), rtac (o_apply RS trans), rtac thm,
- rtac conjunct2, etac bspec, etac set_mp, atac]]) [conjunct1, conjunct2]] 1;
-
-fun mk_rel_Gr_tac rel_def map_id map_cong map_wpull in_cong map_id' map_comp set_naturals
- {context = ctxt, prems = _} =
- let
- val n = length set_naturals;
- in
- if null set_naturals then
- Local_Defs.unfold_tac ctxt [rel_def] THEN EVERY' [rtac @{thm Gr_UNIV_id}, rtac map_id] 1
- else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN
- EVERY' [rtac equalityI, rtac subsetI,
- REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
- REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
- REPEAT_DETERM o etac conjE, hyp_subst_tac,
- rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
- rtac sym, rtac trans, rtac map_comp, rtac map_cong,
- REPEAT_DETERM_N n o EVERY' [dtac @{thm set_rev_mp}, atac,
- REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
- rtac (o_apply RS trans), rtac (@{thm fst_conv} RS arg_cong RS trans),
- rtac (@{thm snd_conv} RS sym)],
- rtac CollectI,
- CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
- rtac @{thm image_subsetI}, dtac @{thm set_rev_mp}, atac,
- REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE], hyp_subst_tac,
- stac @{thm fst_conv}, atac]) set_naturals,
- rtac @{thm subrelI}, etac CollectE, REPEAT_DETERM o eresolve_tac [exE, conjE],
- REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
- REPEAT_DETERM o etac conjE, hyp_subst_tac,
- rtac allE, rtac subst, rtac @{thm wpull_def}, rtac map_wpull,
- REPEAT_DETERM_N n o rtac @{thm wpull_Gr}, etac allE, etac impE, rtac conjI, atac,
- rtac conjI, REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
- CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
- rtac @{thm image_mono}, atac]) set_naturals,
- rtac sym, rtac map_id', REPEAT_DETERM o eresolve_tac [bexE, conjE],
- rtac @{thm relcompI}, rtac @{thm converseI},
- REPEAT_DETERM_N 2 o EVERY' [rtac CollectI, rtac exI,
- rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, etac sym,
- etac @{thm set_rev_mp}, rtac equalityD1, rtac in_cong,
- REPEAT_DETERM_N n o rtac @{thm Gr_def}]] 1
- end;
-
-fun mk_rel_Id_tac n rel_Gr map_id {context = ctxt, prems = _} =
- Local_Defs.unfold_tac ctxt [rel_Gr, @{thm Id_alt}] THEN
- subst_tac ctxt [map_id] 1 THEN
- (if n = 0 then rtac refl 1
- else EVERY' [rtac @{thm arg_cong2[of _ _ _ _ Gr]},
- rtac equalityI, rtac @{thm subset_UNIV}, rtac subsetI, rtac CollectI,
- CONJ_WRAP' (K (rtac @{thm subset_UNIV})) (1 upto n), rtac refl] 1);
-
-fun mk_rel_mono_tac rel_def in_mono {context = ctxt, prems = _} =
- Local_Defs.unfold_tac ctxt [rel_def] THEN
- EVERY' [rtac @{thm relcomp_mono}, rtac @{thm iffD2[OF converse_mono]},
- rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac,
- rtac @{thm Gr_mono}, rtac in_mono, REPEAT_DETERM o atac] 1;
-
-fun mk_map_cong_tac m map_cong {context = ctxt, prems = _} =
- EVERY' [rtac mp, rtac map_cong,
- CONJ_WRAP' (K (rtac ballI THEN' Goal.assume_rule_tac ctxt)) (1 upto m)] 1;
-
-fun mk_rel_converse_le_tac rel_def rel_Id map_cong map_comp set_naturals
- {context = ctxt, prems = _} =
- let
- val n = length set_naturals;
- in
- if null set_naturals then
- Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac equalityD2 1 THEN rtac @{thm converse_Id} 1
- else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN
- EVERY' [rtac @{thm subrelI},
- REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
- REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
- REPEAT_DETERM o etac conjE, hyp_subst_tac, rtac @{thm converseI},
- rtac @{thm relcompI}, rtac @{thm converseI},
- EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
- rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac trans,
- rtac map_cong, REPEAT_DETERM_N n o rtac thm,
- rtac (map_comp RS sym), rtac CollectI,
- CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
- etac @{thm flip_rel}]) set_naturals]) [@{thm snd_fst_flip}, @{thm fst_snd_flip}])] 1
- end;
-
-fun mk_rel_converse_tac le_converse =
- EVERY' [rtac equalityI, rtac le_converse, rtac @{thm xt1(6)}, rtac @{thm converse_shift},
- rtac le_converse, REPEAT_DETERM o stac @{thm converse_converse}, rtac subset_refl] 1;
-
-fun mk_rel_O_tac rel_def rel_Id map_cong map_wppull map_comp set_naturals
- {context = ctxt, prems = _} =
- let
- val n = length set_naturals;
- fun in_tac nthO_in = rtac CollectI THEN'
- CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS @{thm ord_eq_le_trans}),
- rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_naturals;
- in
- if null set_naturals then Local_Defs.unfold_tac ctxt [rel_Id] THEN rtac (@{thm Id_O_R} RS sym) 1
- else Local_Defs.unfold_tac ctxt [rel_def, @{thm Gr_def}] THEN
- EVERY' [rtac equalityI, rtac @{thm subrelI},
- REPEAT_DETERM o eresolve_tac [CollectE, exE, conjE, @{thm relcompE}, @{thm converseE}],
- REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
- REPEAT_DETERM o etac conjE, hyp_subst_tac,
- rtac @{thm relcompI}, rtac @{thm relcompI}, rtac @{thm converseI},
- rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
- rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
- REPEAT_DETERM_N n o rtac @{thm fst_fstO},
- in_tac @{thm fstO_in},
- rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
- rtac sym, rtac trans, rtac map_comp, rtac map_cong,
- REPEAT_DETERM_N n o EVERY' [rtac trans, rtac o_apply, rtac ballE, rtac subst,
- rtac @{thm csquare_def}, rtac @{thm csquare_fstO_sndO}, atac, etac notE,
- etac set_mp, atac],
- in_tac @{thm fstO_in},
- rtac @{thm relcompI}, rtac @{thm converseI},
- rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
- rtac sym, rtac trans, rtac map_comp, rtac map_cong,
- REPEAT_DETERM_N n o rtac o_apply,
- in_tac @{thm sndO_in},
- rtac CollectI, rtac exI, rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl,
- rtac sym, rtac trans, rtac map_comp, rtac sym, rtac map_cong,
- REPEAT_DETERM_N n o rtac @{thm snd_sndO},
- in_tac @{thm sndO_in},
- rtac @{thm subrelI},
- REPEAT_DETERM o eresolve_tac [CollectE, @{thm relcompE}, @{thm converseE}],
- REPEAT_DETERM o eresolve_tac [exE, conjE],
- REPEAT_DETERM o dtac @{thm Pair_eq[THEN subst, of "%x. x"]},
- REPEAT_DETERM o etac conjE, hyp_subst_tac,
- rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull,
- CONJ_WRAP' (K (rtac @{thm wppull_fstO_sndO})) set_naturals,
- etac allE, etac impE, etac conjI, etac conjI, atac,
- REPEAT_DETERM o eresolve_tac [bexE, conjE],
- rtac @{thm relcompI}, rtac @{thm converseI},
- EVERY' (map (fn thm => EVERY' [rtac CollectI, rtac exI,
- rtac conjI, stac @{thm Pair_eq}, rtac conjI, rtac refl, rtac sym, rtac trans,
- rtac trans, rtac map_cong, REPEAT_DETERM_N n o rtac thm,
- rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstO}, @{thm snd_sndO}])] 1
- end;
-
-fun mk_in_rel_tac rel_def m {context = ctxt, prems = _} =
- let
- val ls' = replicate (Int.max (1, m)) ();
- in
- Local_Defs.unfold_tac ctxt (rel_def ::
- @{thms Gr_def converse_unfold relcomp_unfold mem_Collect_eq prod.cases Pair_eq}) THEN
- EVERY' [rtac iffI, REPEAT_DETERM o eresolve_tac [exE, conjE], hyp_subst_tac, rtac exI,
- rtac conjI, CONJ_WRAP' (K atac) ls', rtac conjI, rtac refl, rtac refl,
- REPEAT_DETERM o eresolve_tac [exE, conjE], rtac exI, rtac conjI,
- REPEAT_DETERM_N 2 o EVERY' [rtac exI, rtac conjI, etac @{thm conjI[OF refl sym]},
- CONJ_WRAP' (K atac) ls']] 1
- end;
-
-fun mk_pred_unfold_tac pred_def pred_defs rel_unfold {context = ctxt, prems = _} =
- Local_Defs.unfold_tac ctxt (@{thm mem_Collect_eq_split} :: pred_def :: pred_defs) THEN
- rtac rel_unfold 1;
-
end;
--- a/src/HOL/Codatatype/Tools/bnf_util.ML Tue Sep 11 19:43:06 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_util.ML Tue Sep 11 19:45:12 2012 +0200
@@ -2,7 +2,7 @@
Author: Dmitriy Traytel, TU Muenchen
Copyright 2012
-General library functions.
+Library for bounded natural functors.
*)
signature BNF_UTIL =
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 11 19:43:06 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Tue Sep 11 19:45:12 2012 +0200
@@ -11,8 +11,11 @@
val mk_half_pairss: 'a list -> ('a * 'a) list list
val mk_ctr: typ list -> term -> term
val wrap_datatype: ({prems: thm list, context: Proof.context} -> tactic) list list ->
- (term list * term) * (binding list * binding list list) -> local_theory ->
+ ((bool * term list) * term) *
+ (binding list * (binding list list * (binding * term) list list)) -> local_theory ->
(term list list * thm list * thm list list) * local_theory
+ val parse_wrap_options: bool parser
+ val parse_bound_term: (binding * string) parser
end;
structure BNF_Wrap : BNF_WRAP =
@@ -55,8 +58,7 @@
fun mk_half_pairss ys = mk_half_pairss' [[]] ys;
-(* TODO: provide a way to have a different default value, e.g. "tl Nil = Nil" *)
-fun mk_undef T Ts = Const (@{const_name undefined}, Ts ---> T);
+fun mk_undefined T = Const (@{const_name undefined}, T);
fun mk_ctr Ts ctr =
let val Type (_, Ts0) = body_type (fastype_of ctr) in
@@ -66,27 +68,29 @@
fun eta_expand_case_arg xs f_xs = fold_rev Term.lambda xs f_xs;
fun name_of_ctr c =
- case head_of c of
+ (case head_of c of
Const (s, _) => s
| Free (s, _) => s
- | _ => error "Cannot extract name of constructor";
+ | _ => error "Cannot extract name of constructor");
-fun prepare_wrap_datatype prep_term ((raw_ctrs, raw_case), (raw_disc_binders, raw_sel_binderss))
- no_defs_lthy =
+fun prepare_wrap_datatype prep_term (((no_dests, raw_ctrs), raw_case),
+ (raw_disc_binders, (raw_sel_binderss, raw_sel_defaultss))) no_defs_lthy =
let
(* TODO: sanity checks on arguments *)
(* TODO: attributes (simp, case_names, etc.) *)
(* TODO: case syntax *)
(* TODO: integration with function package ("size") *)
- val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs;
- val case0 = prep_term no_defs_lthy raw_case;
-
- val n = length ctrs0;
+ val n = length raw_ctrs;
val ks = 1 upto n;
val _ = if n > 0 then () else error "No constructors specified";
+ val ctrs0 = map (prep_term no_defs_lthy) raw_ctrs;
+ val case0 = prep_term no_defs_lthy raw_case;
+ val sel_defaultss =
+ pad_list [] n (map (map (apsnd (prep_term no_defs_lthy))) raw_sel_defaultss);
+
val Type (fpT_name, As0) = body_type (fastype_of (hd ctrs0));
val b = Binding.qualified_name fpT_name;
@@ -173,81 +177,107 @@
val exist_xs_v_eq_ctrs =
map2 (fn xctr => fn xs => list_exists_free xs (HOLogic.mk_eq (v, xctr))) xctrs xss;
- fun disc_free b = Free (Binding.name_of b, fpT --> HOLogic.boolT);
+ val unique_disc_no_def = TrueI; (*arbitrary marker*)
+ val alternate_disc_no_def = FalseE; (*arbitrary marker*)
- fun disc_spec b exist_xs_v_eq_ctr = mk_Trueprop_eq (disc_free b $ v, exist_xs_v_eq_ctr);
-
- fun alternate_disc_lhs k =
+ fun alternate_disc_lhs get_disc k =
HOLogic.mk_not
(case nth disc_binders (k - 1) of
NONE => nth exist_xs_v_eq_ctrs (k - 1)
- | SOME b => disc_free b $ v);
-
- fun alternate_disc k =
- if n = 2 then Term.lambda v (alternate_disc_lhs (3 - k)) else error "Cannot use \"*\" here"
+ | SOME b => get_disc b (k - 1) $ v);
- fun mk_sel_case_args proto_sels T =
- map2 (fn Ts => fn i =>
- case AList.lookup (op =) proto_sels i of
- NONE => mk_undef T Ts
- | SOME (xs, x) => fold_rev Term.lambda xs x) ctr_Tss ks;
+ val (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy') =
+ if no_dests then
+ (true, [], [], [], [], [], no_defs_lthy)
+ else
+ let
+ fun disc_free b = Free (Binding.name_of b, fpT --> HOLogic.boolT);
+
+ fun disc_spec b exist_xs_v_eq_ctr = mk_Trueprop_eq (disc_free b $ v, exist_xs_v_eq_ctr);
+
+ fun alternate_disc k = Term.lambda v (alternate_disc_lhs (K o disc_free) (3 - k));
- fun sel_spec b proto_sels =
- let
- val _ =
- (case duplicates (op =) (map fst proto_sels) of
- k :: _ => error ("Duplicate selector name " ^ quote (Binding.name_of b) ^
- " for constructor " ^ quote (Syntax.string_of_term no_defs_lthy (nth ctrs (k - 1))))
- | [] => ())
- val T =
- (case distinct (op =) (map (fastype_of o snd o snd) proto_sels) of
- [T] => T
- | T :: T' :: _ => error ("Inconsistent range type for selector " ^
- quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
- " vs. " ^ quote (Syntax.string_of_typ no_defs_lthy T')));
- in
- mk_Trueprop_eq (Free (Binding.name_of b, fpT --> T) $ v,
- Term.list_comb (mk_case As T, mk_sel_case_args proto_sels T) $ v)
- end;
+ fun mk_sel_case_args b proto_sels T =
+ map2 (fn Ts => fn k =>
+ (case AList.lookup (op =) proto_sels k of
+ NONE =>
+ let val def_T = Ts ---> T in
+ (case AList.lookup Binding.eq_name (rev (nth sel_defaultss (k - 1))) b of
+ NONE => mk_undefined def_T
+ | SOME t => fold_rev (fn T => Term.lambda (Free (Name.uu, T))) Ts
+ (Term.subst_atomic_types [(fastype_of t, T)] t))
+ end
+ | SOME (xs, x) => fold_rev Term.lambda xs x)) ctr_Tss ks;
- val missing_unique_disc_def = TrueI; (*arbitrary marker*)
- val missing_alternate_disc_def = FalseE; (*arbitrary marker*)
+ fun sel_spec b proto_sels =
+ let
+ val _ =
+ (case duplicates (op =) (map fst proto_sels) of
+ k :: _ => error ("Duplicate selector name " ^ quote (Binding.name_of b) ^
+ " for constructor " ^
+ quote (Syntax.string_of_term no_defs_lthy (nth ctrs (k - 1))))
+ | [] => ())
+ val T =
+ (case distinct (op =) (map (fastype_of o snd o snd) proto_sels) of
+ [T] => T
+ | T :: T' :: _ => error ("Inconsistent range type for selector " ^
+ quote (Binding.name_of b) ^ ": " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
+ " vs. " ^ quote (Syntax.string_of_typ no_defs_lthy T')));
+ in
+ mk_Trueprop_eq (Free (Binding.name_of b, fpT --> T) $ v,
+ Term.list_comb (mk_case As T, mk_sel_case_args b proto_sels T) $ v)
+ end;
- val proto_selss = map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss;
- val sel_bundles = AList.group Binding.eq_name (flat sel_binderss ~~ flat proto_selss);
- val sel_binders = map fst sel_bundles;
+ val sel_binders = flat sel_binderss;
+ val uniq_sel_binders = distinct Binding.eq_name sel_binders;
+ val all_sels_distinct = (length uniq_sel_binders = length sel_binders);
+
+ val sel_binder_index =
+ if all_sels_distinct then 1 upto length sel_binders
+ else map (fn b => find_index (curry Binding.eq_name b) uniq_sel_binders) sel_binders;
- fun unflat_selss xs = unflat_lookup Binding.eq_name sel_binders xs sel_binderss;
+ val proto_sels = flat (map3 (fn k => fn xs => map (fn x => (k, (xs, x)))) ks xss xss);
+ val sel_bundles =
+ AList.group (op =) (sel_binder_index ~~ proto_sels)
+ |> sort (int_ord o pairself fst)
+ |> map snd |> curry (op ~~) uniq_sel_binders;
+ val sel_binders = map fst sel_bundles;
+
+ fun unflat_selss xs = unflat_lookup Binding.eq_name sel_binders xs sel_binderss;
- val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
- no_defs_lthy
- |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_v_eq_ctr =>
- fn NONE =>
- if n = 1 then pair (Term.lambda v (mk_v_eq_v ()), missing_unique_disc_def)
- else if m = 0 then pair (Term.lambda v exist_xs_v_eq_ctr, refl)
- else pair (alternate_disc k, missing_alternate_disc_def)
- | SOME b => Specification.definition (SOME (b, NONE, NoSyn),
- ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr)) #>> apsnd snd)
- ks ms exist_xs_v_eq_ctrs disc_binders
- ||>> apfst split_list o fold_map (fn (b, proto_sels) =>
- Specification.definition (SOME (b, NONE, NoSyn),
- ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_bundles
- ||> `Local_Theory.restore;
+ val (((raw_discs, raw_disc_defs), (raw_sels, raw_sel_defs)), (lthy', lthy)) =
+ no_defs_lthy
+ |> apfst split_list o fold_map4 (fn k => fn m => fn exist_xs_v_eq_ctr =>
+ fn NONE =>
+ if n = 1 then pair (Term.lambda v (mk_v_eq_v ()), unique_disc_no_def)
+ else if m = 0 then pair (Term.lambda v exist_xs_v_eq_ctr, refl)
+ else pair (alternate_disc k, alternate_disc_no_def)
+ | SOME b => Specification.definition (SOME (b, NONE, NoSyn),
+ ((Thm.def_binding b, []), disc_spec b exist_xs_v_eq_ctr)) #>> apsnd snd)
+ ks ms exist_xs_v_eq_ctrs disc_binders
+ ||>> apfst split_list o fold_map (fn (b, proto_sels) =>
+ Specification.definition (SOME (b, NONE, NoSyn),
+ ((Thm.def_binding b, []), sel_spec b proto_sels)) #>> apsnd snd) sel_bundles
+ ||> `Local_Theory.restore;
- (*transforms defined frees into consts (and more)*)
- val phi = Proof_Context.export_morphism lthy lthy';
+ (*transforms defined frees into consts (and more)*)
+ val phi = Proof_Context.export_morphism lthy lthy';
- val disc_defs = map (Morphism.thm phi) raw_disc_defs;
- val sel_defss = unflat_selss (map (Morphism.thm phi) raw_sel_defs);
+ val disc_defs = map (Morphism.thm phi) raw_disc_defs;
+ val sel_defs = map (Morphism.thm phi) raw_sel_defs;
+ val sel_defss = unflat_selss sel_defs;
- val discs0 = map (Morphism.term phi) raw_discs;
- val selss0 = unflat_selss (map (Morphism.term phi) raw_sels);
+ val discs0 = map (Morphism.term phi) raw_discs;
+ val selss0 = unflat_selss (map (Morphism.term phi) raw_sels);
+
+ fun mk_disc_or_sel Ts c =
+ Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of c))) ~~ Ts) c;
- fun mk_disc_or_sel Ts c =
- Term.subst_atomic_types (snd (Term.dest_Type (domain_type (fastype_of c))) ~~ Ts) c;
-
- val discs = map (mk_disc_or_sel As) discs0;
- val selss = map (map (mk_disc_or_sel As)) selss0;
+ val discs = map (mk_disc_or_sel As) discs0;
+ val selss = map (map (mk_disc_or_sel As)) selss0;
+ in
+ (all_sels_distinct, discs, selss, disc_defs, sel_defs, sel_defss, lthy')
+ end;
fun mk_imp_p Qs = Logic.list_implies (Qs, HOLogic.mk_Trueprop p);
@@ -309,133 +339,163 @@
Skip_Proof.prove lthy [] [] goal (fn _ => mk_nchotomy_tac n exhaust_thm)
end;
- val sel_thmss =
- map2 (fn case_thm => map (fn sel_def => case_thm RS (sel_def RS trans))) case_thms
- sel_defss;
-
- fun mk_unique_disc_def () =
- let
- val m = the_single ms;
- val goal = mk_Trueprop_eq (mk_v_eq_v (), the_single exist_xs_v_eq_ctrs);
- in
- Skip_Proof.prove lthy [] [] goal (fn _ => mk_unique_disc_def_tac m exhaust_thm')
- |> singleton (Proof_Context.export names_lthy lthy)
- |> Thm.close_derivation
- end;
-
- fun mk_alternate_disc_def k =
- let
- val goal =
- mk_Trueprop_eq (Morphism.term phi (alternate_disc_lhs (3 - k)),
- nth exist_xs_v_eq_ctrs (k - 1));
- in
- Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k)) (nth distinct_thms (2 - k))
- exhaust_thm')
- |> singleton (Proof_Context.export names_lthy lthy)
- |> Thm.close_derivation
- end;
-
- val has_alternate_disc_def =
- exists (fn def => Thm.eq_thm_prop (def, missing_alternate_disc_def)) disc_defs;
-
- val disc_defs' =
- map2 (fn k => fn def =>
- if Thm.eq_thm_prop (def, missing_unique_disc_def) then mk_unique_disc_def ()
- else if Thm.eq_thm_prop (def, missing_alternate_disc_def) then mk_alternate_disc_def k
- else def)
- ks disc_defs;
-
- val discD_thms = map (fn def => def RS iffD1) disc_defs';
- val discI_thms =
- map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms disc_defs';
- val not_discI_thms =
- map2 (fn m => fn def => funpow m (fn thm => allI RS thm)
- (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]})))
- ms disc_defs';
-
- val (disc_thmss', disc_thmss) =
- let
- fun mk_thm discI _ [] = refl RS discI
- | mk_thm _ not_discI [distinct] = distinct RS not_discI;
- fun mk_thms discI not_discI distinctss = map (mk_thm discI not_discI) distinctss;
- in
- map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose
- end;
-
- val disc_thms = flat (map2 (fn true => K [] | false => I) no_discs disc_thmss);
-
- val disc_exclude_thms =
- if has_alternate_disc_def then
- []
+ val (all_sel_thms, sel_thmss, disc_thms, discI_thms, disc_exclude_thms, disc_exhaust_thms,
+ collapse_thms, case_eq_thms) =
+ if no_dests then
+ ([], [], [], [], [], [], [], [])
else
let
- fun mk_goal [] = []
- | mk_goal [((_, true), (_, true))] = []
- | mk_goal [(((_, disc), _), ((_, disc'), _))] =
- [Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (betapply (disc, v)),
- HOLogic.mk_Trueprop (HOLogic.mk_not (betapply (disc', v)))))];
- fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac);
+ fun make_sel_thm case_thm sel_def = case_thm RS (sel_def RS trans);
+
+ fun has_undefined_rhs thm =
+ (case snd (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of thm))) of
+ Const (@{const_name undefined}, _) => true
+ | _ => false);
+
+ val sel_thmss = map2 (map o make_sel_thm) case_thms sel_defss;
+
+ val all_sel_thms =
+ (if all_sels_distinct andalso forall null sel_defaultss then
+ flat sel_thmss
+ else
+ map_product (fn s => fn c => make_sel_thm c s) sel_defs case_thms)
+ |> filter_out has_undefined_rhs;
+
+ fun mk_unique_disc_def () =
+ let
+ val m = the_single ms;
+ val goal = mk_Trueprop_eq (mk_v_eq_v (), the_single exist_xs_v_eq_ctrs);
+ in
+ Skip_Proof.prove lthy [] [] goal (fn _ => mk_unique_disc_def_tac m exhaust_thm')
+ |> singleton (Proof_Context.export names_lthy lthy)
+ |> Thm.close_derivation
+ end;
- val bundles = ms ~~ discD_thms ~~ discs ~~ no_discs;
- val half_pairss = mk_half_pairss bundles;
+ fun mk_alternate_disc_def k =
+ let
+ val goal =
+ mk_Trueprop_eq (alternate_disc_lhs (K (nth discs)) (3 - k),
+ nth exist_xs_v_eq_ctrs (k - 1));
+ in
+ Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+ mk_alternate_disc_def_tac ctxt k (nth disc_defs (2 - k))
+ (nth distinct_thms (2 - k)) exhaust_thm')
+ |> singleton (Proof_Context.export names_lthy lthy)
+ |> Thm.close_derivation
+ end;
+
+ val has_alternate_disc_def =
+ exists (fn def => Thm.eq_thm_prop (def, alternate_disc_no_def)) disc_defs;
+
+ val disc_defs' =
+ map2 (fn k => fn def =>
+ if Thm.eq_thm_prop (def, unique_disc_no_def) then mk_unique_disc_def ()
+ else if Thm.eq_thm_prop (def, alternate_disc_no_def) then mk_alternate_disc_def k
+ else def) ks disc_defs;
+
+ val discD_thms = map (fn def => def RS iffD1) disc_defs';
+ val discI_thms =
+ map2 (fn m => fn def => funpow m (fn thm => exI RS thm) (def RS iffD2)) ms
+ disc_defs';
+ val not_discI_thms =
+ map2 (fn m => fn def => funpow m (fn thm => allI RS thm)
+ (Local_Defs.unfold lthy @{thms not_ex} (def RS @{thm ssubst[of _ _ Not]})))
+ ms disc_defs';
+
+ val (disc_thmss', disc_thmss) =
+ let
+ fun mk_thm discI _ [] = refl RS discI
+ | mk_thm _ not_discI [distinct] = distinct RS not_discI;
+ fun mk_thms discI not_discI distinctss = map (mk_thm discI not_discI) distinctss;
+ in
+ map3 mk_thms discI_thms not_discI_thms distinct_thmsss' |> `transpose
+ end;
+
+ val disc_thms = flat (map2 (fn true => K [] | false => I) no_discs disc_thmss);
- val goal_halvess = map mk_goal half_pairss;
- val half_thmss =
- map3 (fn [] => K (K []) | [goal] => fn [((((m, discD), _), _), _)] => fn disc_thm =>
- [prove (mk_half_disc_exclude_tac m discD disc_thm) goal])
- goal_halvess half_pairss (flat disc_thmss');
+ val disc_exclude_thms =
+ if has_alternate_disc_def then
+ []
+ else
+ let
+ fun mk_goal [] = []
+ | mk_goal [((_, true), (_, true))] = []
+ | mk_goal [(((_, disc), _), ((_, disc'), _))] =
+ [Logic.all v (Logic.mk_implies (HOLogic.mk_Trueprop (betapply (disc, v)),
+ HOLogic.mk_Trueprop (HOLogic.mk_not (betapply (disc', v)))))];
+ fun prove tac goal = Skip_Proof.prove lthy [] [] goal (K tac);
+
+ val bundles = ms ~~ discD_thms ~~ discs ~~ no_discs;
+ val half_pairss = mk_half_pairss bundles;
+
+ val goal_halvess = map mk_goal half_pairss;
+ val half_thmss =
+ map3 (fn [] => K (K []) | [goal] => fn [((((m, discD), _), _), _)] =>
+ fn disc_thm => [prove (mk_half_disc_exclude_tac m discD disc_thm) goal])
+ goal_halvess half_pairss (flat disc_thmss');
+
+ val goal_other_halvess = map (mk_goal o map swap) half_pairss;
+ val other_half_thmss =
+ map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss
+ goal_other_halvess;
+ in
+ interleave (flat half_thmss) (flat other_half_thmss)
+ end;
- val goal_other_halvess = map (mk_goal o map swap) half_pairss;
- val other_half_thmss =
- map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss goal_other_halvess;
- in
- interleave (flat half_thmss) (flat other_half_thmss)
- end;
+ val disc_exhaust_thms =
+ if has_alternate_disc_def orelse no_discs_at_all then
+ []
+ else
+ let
+ fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (betapply (disc, v))];
+ val goal = fold_rev Logic.all [p, v] (mk_imp_p (map mk_prem discs));
+ in
+ [Skip_Proof.prove lthy [] [] goal (fn _ =>
+ mk_disc_exhaust_tac n exhaust_thm discI_thms)]
+ end;
- val disc_exhaust_thms =
- if has_alternate_disc_def orelse no_discs_at_all then
- []
- else
- let
- fun mk_prem disc = mk_imp_p [HOLogic.mk_Trueprop (betapply (disc, v))];
- val goal = fold_rev Logic.all [p, v] (mk_imp_p (map mk_prem discs));
+ val collapse_thms =
+ if no_dests then
+ []
+ else
+ let
+ fun mk_goal ctr disc sels =
+ let
+ val prem = HOLogic.mk_Trueprop (betapply (disc, v));
+ val concl =
+ mk_Trueprop_eq ((null sels ? swap)
+ (Term.list_comb (ctr, map ap_v sels), v));
+ in
+ if prem aconv concl then NONE
+ else SOME (Logic.all v (Logic.mk_implies (prem, concl)))
+ end;
+ val goals = map3 mk_goal ctrs discs selss;
+ in
+ map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal =>
+ Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+ mk_collapse_tac ctxt m discD sel_thms)
+ |> perhaps (try (fn thm => refl RS thm)))) ms discD_thms sel_thmss goals
+ |> map_filter I
+ end;
+
+ val case_eq_thms =
+ if no_dests then
+ []
+ else
+ let
+ fun mk_body f sels = Term.list_comb (f, map ap_v sels);
+ val goal =
+ mk_Trueprop_eq (fcase $ v, mk_IfN B (map ap_v discs) (map2 mk_body fs selss));
+ in
+ [Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
+ mk_case_eq_tac ctxt n exhaust_thm' case_thms disc_thmss' sel_thmss)]
+ |> Proof_Context.export names_lthy lthy
+ end;
in
- [Skip_Proof.prove lthy [] [] goal (fn _ =>
- mk_disc_exhaust_tac n exhaust_thm discI_thms)]
+ (all_sel_thms, sel_thmss, disc_thms, discI_thms, disc_exclude_thms, disc_exhaust_thms,
+ collapse_thms, case_eq_thms)
end;
- val collapse_thms =
- let
- fun mk_goal ctr disc sels =
- let
- val prem = HOLogic.mk_Trueprop (betapply (disc, v));
- val concl =
- mk_Trueprop_eq ((null sels ? swap) (Term.list_comb (ctr, map ap_v sels), v));
- in
- if prem aconv concl then NONE
- else SOME (Logic.all v (Logic.mk_implies (prem, concl)))
- end;
- val goals = map3 mk_goal ctrs discs selss;
- in
- map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal =>
- Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_collapse_tac ctxt m discD sel_thms)
- |> perhaps (try (fn thm => refl RS thm)))) ms discD_thms sel_thmss goals
- |> map_filter I
- end;
-
- val case_eq_thm =
- let
- fun mk_body f sels = Term.list_comb (f, map ap_v sels);
- val goal =
- mk_Trueprop_eq (fcase $ v, mk_IfN B (map ap_v discs) (map2 mk_body fs selss));
- in
- Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
- mk_case_eq_tac ctxt n exhaust_thm' case_thms disc_thmss' sel_thmss)
- |> singleton (Proof_Context.export names_lthy lthy)
- end;
-
val (case_cong_thm, weak_case_cong_thm) =
let
fun mk_prem xctr xs f g =
@@ -484,7 +544,7 @@
val notes =
[(case_congN, [case_cong_thm]),
- (case_eqN, [case_eq_thm]),
+ (case_eqN, case_eq_thms),
(casesN, case_thms),
(collapseN, collapse_thms),
(discsN, disc_thms),
@@ -494,7 +554,7 @@
(exhaustN, [exhaust_thm]),
(injectN, flat inject_thmss),
(nchotomyN, [nchotomy_thm]),
- (selsN, flat sel_thmss),
+ (selsN, all_sel_thms),
(splitN, [split_thm]),
(split_asmN, [split_asm_thm]),
(weak_case_cong_thmsN, [weak_case_cong_thm])]
@@ -510,20 +570,29 @@
fun wrap_datatype tacss = (fn (goalss, after_qed, lthy) =>
map2 (map2 (Skip_Proof.prove lthy [] [])) goalss tacss
- |> (fn thms => after_qed thms lthy)) oo
- prepare_wrap_datatype (K I) (* FIXME? (singleton o Type_Infer_Context.infer_types) *)
+ |> (fn thms => after_qed thms lthy)) oo prepare_wrap_datatype (K I);
+
+fun parse_bracket_list parser = @{keyword "["} |-- Parse.list parser --| @{keyword "]"};
-val parse_bindings = Parse.$$$ "[" |-- Parse.list Parse.binding --| Parse.$$$ "]";
-val parse_bindingss = Parse.$$$ "[" |-- Parse.list parse_bindings --| Parse.$$$ "]";
+val parse_bindings = parse_bracket_list Parse.binding;
+val parse_bindingss = parse_bracket_list parse_bindings;
+
+val parse_bound_term = (Parse.binding --| @{keyword ":"}) -- Parse.term;
+val parse_bound_terms = parse_bracket_list parse_bound_term;
+val parse_bound_termss = parse_bracket_list parse_bound_terms;
val wrap_datatype_cmd = (fn (goalss, after_qed, lthy) =>
Proof.theorem NONE (snd oo after_qed) (map (map (rpair [])) goalss) lthy) oo
prepare_wrap_datatype Syntax.read_term;
+val parse_wrap_options =
+ Scan.optional (@{keyword "("} |-- (@{keyword "no_dests"} >> K true) --| @{keyword ")"}) false;
+
val _ =
Outer_Syntax.local_theory_to_proof @{command_spec "wrap_data"} "wraps an existing datatype"
- (((Parse.$$$ "[" |-- Parse.list Parse.term --| Parse.$$$ "]") -- Parse.term --
- Scan.optional (parse_bindings -- Scan.optional parse_bindingss []) ([], []))
+ ((parse_wrap_options -- (@{keyword "["} |-- Parse.list Parse.term --| @{keyword "]"}) --
+ Parse.term -- Scan.optional (parse_bindings -- Scan.optional (parse_bindingss --
+ Scan.optional parse_bound_termss []) ([], [])) ([], ([], [])))
>> wrap_datatype_cmd);
end;