--- a/src/HOL/BNF/BNF.thy Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/BNF.thy Wed Dec 18 11:03:40 2013 +0100
@@ -14,7 +14,7 @@
begin
hide_const (open) image2 image2p vimage2p Gr Grp collect fsts snds setl setr
- convol thePull pick_middlep fstOp sndOp csquare inver
- image2 relImage relInvImage prefCl PrefCl Succ Shift shift
+ convol pick_middlep fstOp sndOp csquare inver relImage relInvImage
+ prefCl PrefCl Succ Shift shift
end
--- a/src/HOL/BNF/BNF_Comp.thy Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/BNF_Comp.thy Wed Dec 18 11:03:40 2013 +0100
@@ -11,9 +11,6 @@
imports Basic_BNFs
begin
-lemma wpull_id: "wpull UNIV B1 B2 id id id id"
-unfolding wpull_def by simp
-
lemma empty_natural: "(\<lambda>_. {}) o f = image g o (\<lambda>_. {})"
by (rule ext) simp
--- a/src/HOL/BNF/BNF_Def.thy Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/BNF_Def.thy Wed Dec 18 11:03:40 2013 +0100
@@ -39,56 +39,13 @@
definition csquare where
"csquare A f1 f2 p1 p2 \<longleftrightarrow> (\<forall> a \<in> A. f1 (p1 a) = f2 (p2 a))"
-(* 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 blast
-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
-
lemma eq_alt: "op = = Grp UNIV id"
unfolding Grp_def by auto
lemma leq_conversepI: "R = op = \<Longrightarrow> R \<le> R^--1"
by auto
-lemma eq_OOI: "R = op = \<Longrightarrow> R = R OO R"
+lemma leq_OOI: "R = op = \<Longrightarrow> R \<le> R OO R"
by auto
lemma OO_Grp_alt: "(Grp A f)^--1 OO Grp A g = (\<lambda>x y. \<exists>z. z \<in> A \<and> f z = x \<and> g z = y)"
@@ -142,11 +99,6 @@
"csquare (Collect (split (P OO Q))) snd fst (fstOp P Q) (sndOp P Q)"
unfolding csquare_def fstOp_def sndOp_def using pick_middlep by simp
-lemma wppull_fstOp_sndOp:
-shows "wppull (Collect (split (P OO Q))) (Collect (split P)) (Collect (split Q))
- snd fst fst snd (fstOp P Q) (sndOp P Q)"
-using pick_middlep unfolding wppull_def fstOp_def sndOp_def relcompp.simps by auto
-
lemma snd_fst_flip: "snd xy = (fst o (%(x, y). (y, x))) xy"
by (simp split: prod.split)
--- a/src/HOL/BNF/BNF_GFP.thy Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/BNF_GFP.thy Wed Dec 18 11:03:40 2013 +0100
@@ -254,29 +254,6 @@
"\<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 where
-"pickWP A p1 p2 b1 b2 \<equiv> SOME a. a \<in> A \<and> p1 a = b1 \<and> p2 a = b2"
-
-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. a \<in> A \<and> p1 a = b1 \<and> p2 a = b2"
-using assms unfolding wpull_def by blast
-
-lemma pickWP_raw:
-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
- \<and> p1 (pickWP A p1 p2 b1 b2) = b1
- \<and> p2 (pickWP A p1 p2 b1 b2) = b2"
-unfolding pickWP_def using assms someI_ex[OF pickWP_pred] by fastforce
-
-lemmas pickWP =
- pickWP_raw[THEN conjunct1]
- pickWP_raw[THEN conjunct2, THEN conjunct1]
- pickWP_raw[THEN conjunct2, THEN conjunct2]
-
lemma Inl_Field_csum: "a \<in> Field r \<Longrightarrow> Inl a \<in> Field (r +c s)"
unfolding Field_card_of csum_def by auto
--- a/src/HOL/BNF/BNF_LFP.thy Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/BNF_LFP.thy Wed Dec 18 11:03:40 2013 +0100
@@ -224,6 +224,10 @@
shows "PROP P x y"
by (rule `(\<And>x y. PROP P x y)`)
+lemma nchotomy_relcomppE:
+ "\<lbrakk>\<And>y. \<exists>x. y = f x; (r OO s) a c; (\<And>b. r a (f b) \<Longrightarrow> s (f b) c \<Longrightarrow> P)\<rbrakk> \<Longrightarrow> P"
+ by (metis relcompp.cases)
+
lemma vimage2p_fun_rel: "(fun_rel (vimage2p f g R) R) f g"
unfolding fun_rel_def vimage2p_def by auto
--- a/src/HOL/BNF/BNF_Util.thy Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/BNF_Util.thy Wed Dec 18 11:03:40 2013 +0100
@@ -17,17 +17,6 @@
definition collect where
"collect F x = (\<Union>f \<in> F. f x)"
-(* Weak pullbacks: *)
-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))"
-
-(* 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))"
-
lemma fstI: "x = (y, z) \<Longrightarrow> fst x = y"
by simp
--- a/src/HOL/BNF/Basic_BNFs.thy Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/Basic_BNFs.thy Wed Dec 18 11:03:40 2013 +0100
@@ -17,9 +17,6 @@
Main
begin
-lemma wpull_Grp_def: "wpull A B1 B2 f1 f2 p1 p2 \<longleftrightarrow> Grp B1 f1 OO (Grp B2 f2)\<inverse>\<inverse> \<le> (Grp A p1)\<inverse>\<inverse> OO Grp A p2"
- unfolding wpull_def Grp_def by auto
-
bnf ID: 'a
map: "id :: ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
sets: "\<lambda>x. {x}"
@@ -34,7 +31,7 @@
map: "id :: 'a \<Rightarrow> 'a"
bd: "natLeq +c |UNIV :: 'a set|"
rel: "op = :: 'a \<Rightarrow> 'a \<Rightarrow> bool"
-by (auto simp add: wpull_Grp_def Grp_def
+by (auto simp add: Grp_def
card_order_csum natLeq_card_order card_of_card_order_on
cinfinite_csum natLeq_cinfinite)
@@ -93,47 +90,9 @@
apply (rule finite_iff_ordLess_natLeq[THEN iffD1])
by (simp add: setr_def split: sum.split)
next
- fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22
- assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22"
- hence
- pull1: "\<And>b1 b2. \<lbrakk>b1 \<in> B11; b2 \<in> B21; f11 b1 = f21 b2\<rbrakk> \<Longrightarrow> \<exists>a \<in> A1. p11 a = b1 \<and> p21 a = b2"
- and pull2: "\<And>b1 b2. \<lbrakk>b1 \<in> B12; b2 \<in> B22; f12 b1 = f22 b2\<rbrakk> \<Longrightarrow> \<exists>a \<in> A2. p12 a = b1 \<and> p22 a = b2"
- unfolding wpull_def by blast+
- show "wpull {x. setl x \<subseteq> A1 \<and> setr x \<subseteq> A2}
- {x. setl x \<subseteq> B11 \<and> setr x \<subseteq> B12} {x. setl x \<subseteq> B21 \<and> setr x \<subseteq> B22}
- (sum_map f11 f12) (sum_map f21 f22) (sum_map p11 p12) (sum_map p21 p22)"
- (is "wpull ?in ?in1 ?in2 ?mapf1 ?mapf2 ?mapp1 ?mapp2")
- proof (unfold wpull_def)
- { fix B1 B2
- assume *: "B1 \<in> ?in1" "B2 \<in> ?in2" "?mapf1 B1 = ?mapf2 B2"
- have "\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2"
- proof (cases B1)
- case (Inl b1)
- { fix b2 assume "B2 = Inr b2"
- with Inl *(3) have False by simp
- } then obtain b2 where Inl': "B2 = Inl b2" by (cases B2) (simp, blast)
- with Inl * have "b1 \<in> B11" "b2 \<in> B21" "f11 b1 = f21 b2"
- by (simp add: setl_def)+
- with pull1 obtain a where "a \<in> A1" "p11 a = b1" "p21 a = b2" by blast+
- with Inl Inl' have "Inl a \<in> ?in" "?mapp1 (Inl a) = B1 \<and> ?mapp2 (Inl a) = B2"
- by (simp add: sum_set_defs)+
- thus ?thesis by blast
- next
- case (Inr b1)
- { fix b2 assume "B2 = Inl b2"
- with Inr *(3) have False by simp
- } then obtain b2 where Inr': "B2 = Inr b2" by (cases B2) (simp, blast)
- with Inr * have "b1 \<in> B12" "b2 \<in> B22" "f12 b1 = f22 b2"
- by (simp add: sum_set_defs)+
- with pull2 obtain a where "a \<in> A2" "p12 a = b1" "p22 a = b2" by blast+
- with Inr Inr' have "Inr a \<in> ?in" "?mapp1 (Inr a) = B1 \<and> ?mapp2 (Inr a) = B2"
- by (simp add: sum_set_defs)+
- thus ?thesis by blast
- qed
- }
- thus "\<forall>B1 B2. B1 \<in> ?in1 \<and> B2 \<in> ?in2 \<and> ?mapf1 B1 = ?mapf2 B2 \<longrightarrow>
- (\<exists>A \<in> ?in. ?mapp1 A = B1 \<and> ?mapp2 A = B2)" by fastforce
- qed
+ fix R1 R2 S1 S2
+ show "sum_rel R1 R2 OO sum_rel S1 S2 \<le> sum_rel (R1 OO S1) (R2 OO S2)"
+ by (auto simp: sum_rel_def split: sum.splits)
next
fix R S
show "sum_rel R S =
@@ -187,12 +146,8 @@
show "|{snd x}| \<le>o natLeq"
by (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq finite.emptyI finite_insert)
next
- fix A1 A2 B11 B12 B21 B22 f11 f12 f21 f22 p11 p12 p21 p22
- assume "wpull A1 B11 B21 f11 f21 p11 p21" "wpull A2 B12 B22 f12 f22 p12 p22"
- thus "wpull {x. {fst x} \<subseteq> A1 \<and> {snd x} \<subseteq> A2}
- {x. {fst x} \<subseteq> B11 \<and> {snd x} \<subseteq> B12} {x. {fst x} \<subseteq> B21 \<and> {snd x} \<subseteq> B22}
- (map_pair f11 f12) (map_pair f21 f22) (map_pair p11 p12) (map_pair p21 p22)"
- unfolding wpull_def by simp fast
+ fix R1 R2 S1 S2
+ show "prod_rel R1 R2 OO prod_rel S1 S2 \<le> prod_rel (R1 OO S1) (R2 OO S2)" by auto
next
fix R S
show "prod_rel R S =
@@ -202,26 +157,6 @@
by auto
qed
-(* Categorical version of pullback: *)
-lemma wpull_cat:
-assumes p: "wpull A B1 B2 f1 f2 p1 p2"
-and c: "f1 o q1 = f2 o q2"
-and r: "range q1 \<subseteq> B1" "range q2 \<subseteq> B2"
-obtains h where "range h \<subseteq> A \<and> q1 = p1 o h \<and> q2 = p2 o h"
-proof-
- have *: "\<forall>d. \<exists>a \<in> A. p1 a = q1 d & p2 a = q2 d"
- proof safe
- fix d
- have "f1 (q1 d) = f2 (q2 d)" using c unfolding comp_def[abs_def] by (rule fun_cong)
- moreover
- have "q1 d : B1" "q2 d : B2" using r unfolding image_def by auto
- ultimately show "\<exists>a \<in> A. p1 a = q1 d \<and> p2 a = q2 d"
- using p unfolding wpull_def by auto
- qed
- then obtain h where "!! d. h d \<in> A & p1 (h d) = q1 d & p2 (h d) = q2 d" by metis
- thus ?thesis using that by fastforce
-qed
-
bnf "'a \<Rightarrow> 'b"
map: "op \<circ>"
sets: range
@@ -255,16 +190,8 @@
also have "?U \<le>o natLeq +c ?U" by (rule ordLeq_csum2) (rule card_of_Card_order)
finally show "|range f| \<le>o natLeq +c ?U" .
next
- fix A B1 B2 f1 f2 p1 p2 assume p: "wpull A B1 B2 f1 f2 p1 p2"
- show "wpull {h. range h \<subseteq> A} {g1. range g1 \<subseteq> B1} {g2. range g2 \<subseteq> B2}
- (op \<circ> f1) (op \<circ> f2) (op \<circ> p1) (op \<circ> p2)"
- unfolding wpull_def
- proof safe
- fix g1 g2 assume r: "range g1 \<subseteq> B1" "range g2 \<subseteq> B2"
- and c: "f1 \<circ> g1 = f2 \<circ> g2"
- show "\<exists>h \<in> {h. range h \<subseteq> A}. p1 \<circ> h = g1 \<and> p2 \<circ> h = g2"
- using wpull_cat[OF p c r] by simp metis
- qed
+ fix R S
+ show "fun_rel op = R OO fun_rel op = S \<le> fun_rel op = (R OO S)" by (auto simp: fun_rel_def)
next
fix R
show "fun_rel op = R =
--- a/src/HOL/BNF/Countable_Set_Type.thy Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/Countable_Set_Type.thy Wed Dec 18 11:03:40 2013 +0100
@@ -176,31 +176,9 @@
next
fix C show "|rcset C| \<le>o natLeq" by transfer (unfold countable_card_le_natLeq)
next
- fix A B1 B2 f1 f2 p1 p2
- assume wp: "wpull A B1 B2 f1 f2 p1 p2"
- show "wpull {x. rcset x \<subseteq> A} {x. rcset x \<subseteq> B1} {x. rcset x \<subseteq> B2}
- (cimage f1) (cimage f2) (cimage p1) (cimage p2)"
- unfolding wpull_def proof safe
- fix y1 y2
- assume Y1: "rcset y1 \<subseteq> B1" and Y2: "rcset y2 \<subseteq> B2"
- assume "cimage f1 y1 = cimage f2 y2"
- hence EQ: "f1 ` (rcset y1) = f2 ` (rcset y2)" by transfer
- with Y1 Y2 obtain X where X: "X \<subseteq> A"
- and Y1: "p1 ` X = rcset y1" and Y2: "p2 ` X = rcset y2"
- using wpull_image[OF wp] unfolding wpull_def Pow_def Bex_def mem_Collect_eq
- by (auto elim!: allE[of _ "rcset y1"] allE[of _ "rcset y2"])
- have "\<forall> y1' \<in> rcset y1. \<exists> x. x \<in> X \<and> y1' = p1 x" using Y1 by auto
- then obtain q1 where q1: "\<forall> y1' \<in> rcset y1. q1 y1' \<in> X \<and> y1' = p1 (q1 y1')" by metis
- have "\<forall> y2' \<in> rcset y2. \<exists> x. x \<in> X \<and> y2' = p2 x" using Y2 by auto
- then obtain q2 where q2: "\<forall> y2' \<in> rcset y2. q2 y2' \<in> X \<and> y2' = p2 (q2 y2')" by metis
- def X' \<equiv> "q1 ` (rcset y1) \<union> q2 ` (rcset y2)"
- have X': "X' \<subseteq> A" and Y1: "p1 ` X' = rcset y1" and Y2: "p2 ` X' = rcset y2"
- using X Y1 Y2 q1 q2 unfolding X'_def by fast+
- have fX': "countable X'" unfolding X'_def by simp
- then obtain x where X'eq: "X' = rcset x" by transfer blast
- show "\<exists>x\<in>{x. rcset x \<subseteq> A}. cimage p1 x = y1 \<and> cimage p2 x = y2"
- using X' Y1 Y2 unfolding X'eq by (intro bexI[of _ "x"]) (transfer, auto)
- qed
+ fix R S
+ show "cset_rel R OO cset_rel S \<le> cset_rel (R OO S)"
+ unfolding cset_rel_def[abs_def] by fast
next
fix R
show "cset_rel R =
--- a/src/HOL/BNF/More_BNFs.thy Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/More_BNFs.thy Wed Dec 18 11:03:40 2013 +0100
@@ -50,18 +50,9 @@
show "|Option.set x| \<le>o natLeq"
by (cases x) (simp_all add: ordLess_imp_ordLeq finite_iff_ordLess_natLeq[symmetric])
next
- fix A B1 B2 f1 f2 p1 p2
- assume wpull: "wpull A B1 B2 f1 f2 p1 p2"
- show "wpull {x. Option.set x \<subseteq> A} {x. Option.set x \<subseteq> B1} {x. Option.set x \<subseteq> B2}
- (Option.map f1) (Option.map f2) (Option.map p1) (Option.map p2)"
- (is "wpull ?A ?B1 ?B2 ?f1 ?f2 ?p1 ?p2")
- unfolding wpull_def
- proof (intro strip, elim conjE)
- fix b1 b2
- assume "b1 \<in> ?B1" "b2 \<in> ?B2" "?f1 b1 = ?f2 b2"
- thus "\<exists>a \<in> ?A. ?p1 a = b1 \<and> ?p2 a = b2" using wpull
- unfolding wpull_def by (cases b2) (auto 4 5)
- qed
+ fix R S
+ show "option_rel R OO option_rel S \<le> option_rel (R OO S)"
+ by (auto simp: option_rel_def split: option.splits)
next
fix z
assume "z \<in> Option.set None"
@@ -76,28 +67,6 @@
split: option.splits)
qed
-lemma wpull_map:
- assumes "wpull A B1 B2 f1 f2 p1 p2"
- shows "wpull {x. set x \<subseteq> A} {x. set x \<subseteq> B1} {x. set x \<subseteq> B2} (map f1) (map f2) (map p1) (map p2)"
- (is "wpull ?A ?B1 ?B2 _ _ _ _")
-proof (unfold wpull_def)
- { fix as bs assume *: "as \<in> ?B1" "bs \<in> ?B2" "map f1 as = map f2 bs"
- hence "length as = length bs" by (metis length_map)
- hence "\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs" using *
- proof (induct as bs rule: list_induct2)
- case (Cons a as b bs)
- hence "a \<in> B1" "b \<in> B2" "f1 a = f2 b" by auto
- with assms obtain z where "z \<in> A" "p1 z = a" "p2 z = b" unfolding wpull_def by blast
- moreover
- from Cons obtain zs where "zs \<in> ?A" "map p1 zs = as" "map p2 zs = bs" by auto
- ultimately have "z # zs \<in> ?A" "map p1 (z # zs) = a # as \<and> map p2 (z # zs) = b # bs" by auto
- thus ?case by (rule_tac x = "z # zs" in bexI)
- qed simp
- }
- thus "\<forall>as bs. as \<in> ?B1 \<and> bs \<in> ?B2 \<and> map f1 as = map f2 bs \<longrightarrow>
- (\<exists>zs \<in> ?A. map p1 zs = as \<and> map p2 zs = bs)" by blast
-qed
-
bnf "'a list"
map: map
sets: set
@@ -125,50 +94,21 @@
show "|set x| \<le>o natLeq"
by (metis List.finite_set finite_iff_ordLess_natLeq ordLess_imp_ordLeq)
next
+ fix R S
+ show "list_all2 R OO list_all2 S \<le> list_all2 (R OO S)"
+ by (metis list_all2_OO order_refl)
+next
fix R
show "list_all2 R =
(Grp {x. set x \<subseteq> {(x, y). R x y}} (map fst))\<inverse>\<inverse> OO
Grp {x. set x \<subseteq> {(x, y). R x y}} (map snd)"
unfolding list_all2_def[abs_def] Grp_def fun_eq_iff relcompp.simps conversep.simps
by (force simp: zip_map_fst_snd)
-qed (simp add: wpull_map)+
+qed simp_all
(* Finite sets *)
-lemma wpull_image:
- assumes "wpull A B1 B2 f1 f2 p1 p2"
- shows "wpull (Pow A) (Pow B1) (Pow B2) (image f1) (image f2) (image p1) (image p2)"
-unfolding wpull_def Pow_def Bex_def mem_Collect_eq proof clarify
- fix Y1 Y2 assume Y1: "Y1 \<subseteq> B1" and Y2: "Y2 \<subseteq> B2" and EQ: "f1 ` Y1 = f2 ` Y2"
- def X \<equiv> "{a \<in> A. p1 a \<in> Y1 \<and> p2 a \<in> Y2}"
- show "\<exists>X\<subseteq>A. p1 ` X = Y1 \<and> p2 ` X = Y2"
- proof (rule exI[of _ X], intro conjI)
- show "p1 ` X = Y1"
- proof
- show "Y1 \<subseteq> p1 ` X"
- proof safe
- fix y1 assume y1: "y1 \<in> Y1"
- then obtain y2 where y2: "y2 \<in> Y2" and eq: "f1 y1 = f2 y2" using EQ by auto
- then obtain x where "x \<in> A" and "p1 x = y1" and "p2 x = y2"
- using assms y1 Y1 Y2 unfolding wpull_def by blast
- thus "y1 \<in> p1 ` X" unfolding X_def using y1 y2 by auto
- qed
- qed(unfold X_def, auto)
- show "p2 ` X = Y2"
- proof
- show "Y2 \<subseteq> p2 ` X"
- proof safe
- fix y2 assume y2: "y2 \<in> Y2"
- then obtain y1 where y1: "y1 \<in> Y1" and eq: "f1 y1 = f2 y2" using EQ by force
- then obtain x where "x \<in> A" and "p1 x = y1" and "p2 x = y2"
- using assms y2 Y1 Y2 unfolding wpull_def by blast
- thus "y2 \<in> p2 ` X" unfolding X_def using y1 y2 by auto
- qed
- qed(unfold X_def, auto)
- qed(unfold X_def, auto)
-qed
-
context
includes fset.lifting
begin
@@ -206,31 +146,6 @@
by (transfer, clarsimp, metis fst_conv)
qed
-lemma wpull_fimage:
- assumes "wpull A B1 B2 f1 f2 p1 p2"
- shows "wpull {x. fset x \<subseteq> A} {x. fset x \<subseteq> B1} {x. fset x \<subseteq> B2}
- (fimage f1) (fimage f2) (fimage p1) (fimage p2)"
-unfolding wpull_def Pow_def Bex_def mem_Collect_eq proof clarify
- fix y1 y2
- assume Y1: "fset y1 \<subseteq> B1" and Y2: "fset y2 \<subseteq> B2"
- assume "fimage f1 y1 = fimage f2 y2"
- hence EQ: "f1 ` (fset y1) = f2 ` (fset y2)" by transfer simp
- with Y1 Y2 obtain X where X: "X \<subseteq> A" and Y1: "p1 ` X = fset y1" and Y2: "p2 ` X = fset y2"
- using wpull_image[OF assms] unfolding wpull_def Pow_def
- by (auto elim!: allE[of _ "fset y1"] allE[of _ "fset y2"])
- have "\<forall> y1' \<in> fset y1. \<exists> x. x \<in> X \<and> y1' = p1 x" using Y1 by auto
- then obtain q1 where q1: "\<forall> y1' \<in> fset y1. q1 y1' \<in> X \<and> y1' = p1 (q1 y1')" by metis
- have "\<forall> y2' \<in> fset y2. \<exists> x. x \<in> X \<and> y2' = p2 x" using Y2 by auto
- then obtain q2 where q2: "\<forall> y2' \<in> fset y2. q2 y2' \<in> X \<and> y2' = p2 (q2 y2')" by metis
- def X' \<equiv> "q1 ` (fset y1) \<union> q2 ` (fset y2)"
- have X': "X' \<subseteq> A" and Y1: "p1 ` X' = fset y1" and Y2: "p2 ` X' = fset y2"
- using X Y1 Y2 q1 q2 unfolding X'_def by auto
- have fX': "finite X'" unfolding X'_def by transfer simp
- then obtain x where X'eq: "X' = fset x" by transfer simp
- show "\<exists>x. fset x \<subseteq> A \<and> fimage p1 x = y1 \<and> fimage p2 x = y2"
- using X' Y1 Y2 by (auto simp: X'eq intro!: exI[of _ "x"]) (transfer, blast)+
-qed
-
bnf "'a fset"
map: fimage
sets: fset
@@ -245,7 +160,7 @@
apply (rule natLeq_card_order)
apply (rule natLeq_cinfinite)
apply transfer apply (metis ordLess_imp_ordLeq finite_iff_ordLess_natLeq)
- apply (erule wpull_fimage)
+ apply (fastforce simp: fset_rel_alt)
apply (simp add: Grp_def relcompp.simps conversep.simps fun_eq_iff fset_rel_alt fset_rel_aux)
apply transfer apply simp
done
@@ -550,6 +465,62 @@
show ?thesis unfolding A using finite_cartesian_product[OF assms] by auto
qed
+(* Weak pullbacks: *)
+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))"
+
+(* 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 blast
+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_fstOp_sndOp:
+shows "wppull (Collect (split (P OO Q))) (Collect (split P)) (Collect (split Q))
+ snd fst fst snd (fstOp P Q) (sndOp P Q)"
+using pick_middlep unfolding wppull_def fstOp_def sndOp_def relcompp.simps by auto
+
lemma wpull_mmap:
fixes A :: "'a set" and B1 :: "'b1 set" and B2 :: "'b2 set"
assumes wp: "wpull A B1 B2 f1 f2 p1 p2"
@@ -781,18 +752,33 @@
by transfer
(auto intro!: ordLess_imp_ordLeq simp: finite_iff_ordLess_natLeq[symmetric] multiset_def)
+lemma wppull_mmap:
+ assumes "wppull A B1 B2 f1 f2 e1 e2 p1 p2"
+ shows "wppull {M. set_of M \<subseteq> A} {N1. set_of N1 \<subseteq> B1} {N2. set_of N2 \<subseteq> B2}
+ (mmap f1) (mmap f2) (mmap e1) (mmap e2) (mmap p1) (mmap p2)"
+proof -
+ from assms obtain j where 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')"
+ by (blast dest: wppull_thePull)
+ then show ?thesis
+ by (intro wpull_wppull[OF wpull_mmap[OF wpull_thePull], of _ _ _ _ "mmap j"])
+ (auto simp: o_eq_dest_lhs[OF mmap_comp[symmetric]] o_eq_dest[OF set_of_mmap]
+ intro!: mmap_cong simp del: mem_set_of_iff simp: mem_set_of_iff[symmetric])
+qed
+
bnf "'a multiset"
map: mmap
sets: set_of
bd: natLeq
wits: "{#}"
by (auto simp add: mmap_id0 mmap_comp set_of_mmap natLeq_card_order natLeq_cinfinite set_of_bd
- intro: mmap_cong wpull_mmap)
+ Grp_def relcompp.simps intro: mmap_cong)
+ (metis wppull_mmap[OF wppull_fstOp_sndOp, unfolded wppull_def
+ o_eq_dest_lhs[OF mmap_comp[symmetric]] fstOp_def sndOp_def o_def, simplified])
inductive rel_multiset' where
-Zero: "rel_multiset' R {#} {#}"
-|
-Plus: "\<lbrakk>R a b; rel_multiset' R M N\<rbrakk> \<Longrightarrow> rel_multiset' R (M + {#a#}) (N + {#b#})"
+ Zero[intro]: "rel_multiset' R {#} {#}"
+| Plus[intro]: "\<lbrakk>R a b; rel_multiset' R M N\<rbrakk> \<Longrightarrow> rel_multiset' R (M + {#a#}) (N + {#b#})"
lemma map_multiset_Zero_iff[simp]: "mmap f M = {#} \<longleftrightarrow> M = {#}"
by (metis image_is_empty multiset.set_map set_of_eq_empty_iff)
@@ -998,8 +984,6 @@
(* Advanced relator customization *)
(* Set vs. sum relators: *)
-(* FIXME: All such facts should be declared as simps: *)
-declare sum_rel_simps[simp]
lemma set_rel_sum_rel[simp]:
"set_rel (sum_rel \<chi> \<phi>) A1 A2 \<longleftrightarrow>
--- a/src/HOL/BNF/Tools/bnf_comp.ML Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Wed Dec 18 11:03:40 2013 +0100
@@ -214,8 +214,8 @@
|> Thm.close_derivation
end;
- fun map_wpull_tac _ =
- mk_map_wpull_tac in_alt_thm (map map_wpull_of_bnf inners) (map_wpull_of_bnf outer);
+ fun le_rel_OO_tac _ = mk_le_rel_OO_tac (le_rel_OO_of_bnf outer) (rel_mono_of_bnf outer)
+ (map le_rel_OO_of_bnf inners);
fun rel_OO_Grp_tac _ =
let
@@ -234,7 +234,7 @@
end;
val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
+ bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac;
val outer_wits = mk_wits_of_bnf (replicate onwits oDs) (replicate onwits CAs) outer;
@@ -322,7 +322,9 @@
Goal.prove_sorry lthy [] [] goal (K kill_in_alt_tac) |> Thm.close_derivation
end;
- fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
+ fun le_rel_OO_tac {context = ctxt, prems = _} =
+ EVERY' [rtac @{thm ord_le_eq_trans}, rtac (le_rel_OO_of_bnf bnf)] 1 THEN
+ unfold_thms_tac ctxt @{thms eq_OO} THEN rtac refl 1;
fun rel_OO_Grp_tac _ =
let
@@ -340,7 +342,7 @@
end;
val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
+ bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac;
val bnf_wits = mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf;
@@ -420,12 +422,12 @@
Goal.prove_sorry lthy [] [] goal (K lift_in_alt_tac) |> Thm.close_derivation
end;
- fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
+ fun le_rel_OO_tac _ = rtac (le_rel_OO_of_bnf bnf) 1;
fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
+ bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -493,12 +495,12 @@
|> Thm.close_derivation
end;
- fun map_wpull_tac _ = mk_map_wpull_tac in_alt_thm [] (map_wpull_of_bnf bnf);
+ fun le_rel_OO_tac _ = rtac (le_rel_OO_of_bnf bnf) 1;
fun rel_OO_Grp_tac _ = mk_simple_rel_OO_Grp_tac (rel_OO_Grp_of_bnf bnf) in_alt_thm;
val tacs = zip_axioms map_id0_tac map_comp0_tac map_cong0_tac set_map0_tacs bd_card_order_tac
- bd_cinfinite_tac set_bd_tacs map_wpull_tac rel_OO_Grp_tac;
+ bd_cinfinite_tac set_bd_tacs le_rel_OO_tac rel_OO_Grp_tac;
val wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
@@ -633,7 +635,7 @@
val tacs = zip_axioms (mk_tac (map_id0_of_bnf bnf)) (mk_tac (map_comp0_of_bnf bnf))
(mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map0_of_bnf bnf))
(K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds)
- (mk_tac (map_wpull_of_bnf bnf))
+ (mk_tac (le_rel_OO_of_bnf bnf))
(mk_tac (rel_OO_Grp_of_bnf bnf));
val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);
--- a/src/HOL/BNF/Tools/bnf_comp_tactics.ML Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_comp_tactics.ML Wed Dec 18 11:03:40 2013 +0100
@@ -31,7 +31,7 @@
val mk_permute_in_alt_tac: ''a list -> ''a list -> tactic
- val mk_map_wpull_tac: thm -> thm list -> thm -> tactic
+ val mk_le_rel_OO_tac: thm -> thm -> thm list -> tactic
val mk_simple_rel_OO_Grp_tac: thm -> thm -> tactic
val mk_simple_wit_tac: thm list -> tactic
end;
@@ -241,10 +241,8 @@
mk_rotate_eq_tac (rtac refl) trans @{thm conj_assoc} @{thm conj_commute} @{thm conj_cong}
dest src) 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_le_rel_OO_tac outer_le_rel_OO outer_rel_mono inner_le_rel_OOs =
+ EVERY' (map rtac (@{thm order_trans} :: outer_le_rel_OO :: outer_rel_mono :: inner_le_rel_OOs)) 1;
fun mk_simple_rel_OO_Grp_tac rel_OO_Grp in_alt_thm =
rtac (trans OF [rel_OO_Grp, in_alt_thm RS @{thm OO_Grp_cong} RS sym]) 1;
--- a/src/HOL/BNF/Tools/bnf_def.ML Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_def.ML Wed Dec 18 11:03:40 2013 +0100
@@ -58,8 +58,7 @@
val map_id0_of_bnf: bnf -> thm
val map_id_of_bnf: bnf -> thm
val map_transfer_of_bnf: bnf -> thm
- val map_wppull_of_bnf: bnf -> thm
- val map_wpull_of_bnf: bnf -> thm
+ val le_rel_OO_of_bnf: bnf -> thm
val rel_def_of_bnf: bnf -> thm
val rel_Grp_of_bnf: bnf -> thm
val rel_OO_of_bnf: bnf -> thm
@@ -110,6 +109,18 @@
((thm list -> thm list list) -> thm list list -> Proof.context -> bnf * local_theory) *
local_theory * thm list
+ val define_bnf_consts: const_policy -> fact_policy -> typ list option ->
+ binding -> binding -> binding list ->
+ (((((binding * typ) * term) * term list) * term) * term list) * term option -> local_theory ->
+ ((typ list * typ list * typ list * typ) *
+ (term * term list * term * (int list * term) list * term) *
+ (thm * thm list * thm * thm list * thm) *
+ ((typ list -> typ list -> typ list -> term) *
+ (typ list -> typ list -> term -> term) *
+ (typ list -> typ list -> typ -> typ) *
+ (typ list -> typ list -> typ list -> term) *
+ (typ list -> typ list -> typ list -> term))) * local_theory
+
val bnf_def: const_policy -> (Proof.context -> fact_policy) -> (binding -> binding) ->
({prems: thm list, context: Proof.context} -> tactic) list ->
({prems: thm list, context: Proof.context} -> tactic) -> typ list option -> binding ->
@@ -135,13 +146,13 @@
bd_card_order: thm,
bd_cinfinite: thm,
set_bd: thm list,
- map_wpull: thm,
+ le_rel_OO: thm,
rel_OO_Grp: thm
};
-fun mk_axioms' ((((((((id, comp), cong), map), c_o), cinf), set_bd), wpull), rel) =
+fun mk_axioms' ((((((((id, comp), cong), map), c_o), cinf), set_bd), le_rel_OO), rel) =
{map_id0 = id, map_comp0 = comp, map_cong0 = cong, set_map0 = map, bd_card_order = c_o,
- bd_cinfinite = cinf, set_bd = set_bd, map_wpull = wpull, rel_OO_Grp = rel};
+ bd_cinfinite = cinf, set_bd = set_bd, le_rel_OO = le_rel_OO, rel_OO_Grp = rel};
fun dest_cons [] = raise List.Empty
| dest_cons (x :: xs) = (x, xs);
@@ -159,16 +170,16 @@
||> the_single
|> mk_axioms';
-fun zip_axioms mid mcomp mcong smap bdco bdinf sbd wpull rel =
- [mid, mcomp, mcong] @ smap @ [bdco, bdinf] @ sbd @ [wpull, rel];
+fun zip_axioms mid mcomp mcong smap bdco bdinf sbd le_rel_OO rel =
+ [mid, mcomp, mcong] @ smap @ [bdco, bdinf] @ sbd @ [le_rel_OO, rel];
fun dest_axioms {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd,
- map_wpull, rel_OO_Grp} =
- zip_axioms map_id0 map_comp0 map_cong0 set_map0 bd_card_order bd_cinfinite set_bd map_wpull
+ le_rel_OO, rel_OO_Grp} =
+ zip_axioms map_id0 map_comp0 map_cong0 set_map0 bd_card_order bd_cinfinite set_bd le_rel_OO
rel_OO_Grp;
fun map_axioms f {map_id0, map_comp0, map_cong0, set_map0, bd_card_order, bd_cinfinite, set_bd,
- map_wpull, rel_OO_Grp} =
+ le_rel_OO, rel_OO_Grp} =
{map_id0 = f map_id0,
map_comp0 = f map_comp0,
map_cong0 = f map_cong0,
@@ -176,7 +187,7 @@
bd_card_order = f bd_card_order,
bd_cinfinite = f bd_cinfinite,
set_bd = map f set_bd,
- map_wpull = f map_wpull,
+ le_rel_OO = f le_rel_OO,
rel_OO_Grp = f rel_OO_Grp};
val morph_axioms = map_axioms o Morphism.thm;
@@ -207,7 +218,6 @@
map_cong: thm lazy,
map_id: thm lazy,
map_transfer: thm lazy,
- map_wppull: thm lazy,
rel_eq: thm lazy,
rel_flip: thm lazy,
set_map: thm lazy list,
@@ -220,7 +230,7 @@
};
fun mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong in_mono in_rel
- map_comp map_cong map_id map_transfer map_wppull rel_eq rel_flip set_map rel_cong rel_mono
+ map_comp map_cong map_id map_transfer rel_eq rel_flip set_map rel_cong rel_mono
rel_mono_strong rel_Grp rel_conversep rel_OO = {
bd_Card_order = bd_Card_order,
bd_Cinfinite = bd_Cinfinite,
@@ -234,7 +244,6 @@
map_cong = map_cong,
map_id = map_id,
map_transfer = map_transfer,
- map_wppull = map_wppull,
rel_eq = rel_eq,
rel_flip = rel_flip,
set_map = set_map,
@@ -258,7 +267,6 @@
map_cong,
map_id,
map_transfer,
- map_wppull,
rel_eq,
rel_flip,
set_map,
@@ -280,7 +288,6 @@
map_cong = Lazy.map f map_cong,
map_id = Lazy.map f map_id,
map_transfer = Lazy.map f map_transfer,
- map_wppull = Lazy.map f map_wppull,
rel_eq = Lazy.map f rel_eq,
rel_flip = Lazy.map f rel_flip,
set_map = map (Lazy.map f) set_map,
@@ -402,8 +409,7 @@
val map_cong0_of_bnf = #map_cong0 o #axioms o rep_bnf;
val map_cong_of_bnf = Lazy.force o #map_cong o #facts o rep_bnf;
val map_transfer_of_bnf = Lazy.force o #map_transfer o #facts o rep_bnf;
-val map_wppull_of_bnf = Lazy.force o #map_wppull o #facts o rep_bnf;
-val map_wpull_of_bnf = #map_wpull o #axioms o rep_bnf;
+val le_rel_OO_of_bnf = #le_rel_OO o #axioms o rep_bnf;
val rel_def_of_bnf = #rel_def o #defs o rep_bnf;
val rel_eq_of_bnf = Lazy.force o #rel_eq o #facts o rep_bnf;
val rel_flip_of_bnf = Lazy.force o #rel_flip o #facts o rep_bnf;
@@ -569,7 +575,6 @@
val map_cong0N = "map_cong0";
val map_congN = "map_cong";
val map_transferN = "map_transfer";
-val map_wpullN = "map_wpull";
val rel_eqN = "rel_eq";
val rel_flipN = "rel_flip";
val set_map0N = "set_map0";
@@ -618,7 +623,6 @@
(map_comp0N, [#map_comp0 axioms]),
(map_id0N, [#map_id0 axioms]),
(map_transferN, [Lazy.force (#map_transfer facts)]),
- (map_wpullN, [#map_wpull axioms]),
(rel_mono_strongN, [Lazy.force (#rel_mono_strong facts)]),
(set_map0N, #set_map0 axioms),
(set_bdN, #set_bd axioms)] @
@@ -660,30 +664,10 @@
(* Define new BNFs *)
-fun prepare_def const_policy mk_fact_policy qualify prep_typ prep_term Ds_opt map_b rel_b set_bs
- ((((((raw_bnf_b, raw_bnf_T), raw_map), raw_sets), raw_bd), raw_wits), raw_rel_opt)
- no_defs_lthy =
+fun define_bnf_consts const_policy fact_policy Ds_opt map_b rel_b set_bs
+ ((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt) no_defs_lthy =
let
- val fact_policy = mk_fact_policy no_defs_lthy;
- val bnf_b = qualify raw_bnf_b;
- val live = length raw_sets;
-
- val T_rhs = prep_typ no_defs_lthy raw_bnf_T;
- val map_rhs = prep_term no_defs_lthy raw_map;
- val set_rhss = map (prep_term no_defs_lthy) raw_sets;
- val bd_rhs = prep_term no_defs_lthy raw_bd;
-
- fun err T =
- error ("Trying to register the type " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
- " as unnamed BNF");
-
- val (bnf_b, key) =
- if Binding.eq_name (bnf_b, Binding.empty) then
- (case T_rhs of
- Type (C, Ts) => if forall (can dest_TFree) Ts
- then (Binding.qualified_name C, C) else err T_rhs
- | T => err T)
- else (bnf_b, Local_Theory.full_name no_defs_lthy bnf_b);
+ val live = length set_rhss;
val def_qualify = Binding.conceal o Binding.qualify false (Binding.name_of bnf_b);
@@ -736,6 +720,7 @@
val phi = Proof_Context.export_morphism lthy_old lthy;
+
val bnf_map_def = Morphism.thm phi raw_map_def;
val bnf_set_defs = map (Morphism.thm phi) raw_set_defs;
val bnf_bd_def = Morphism.thm phi raw_bd_def;
@@ -744,57 +729,162 @@
(*TODO: handle errors*)
(*simple shape analysis of a map function*)
- val ((alphas, betas), (CA, _)) =
+ val ((alphas, betas), (Calpha, _)) =
fastype_of bnf_map
|> strip_typeN live
|>> map_split dest_funT
||> dest_funT
handle TYPE _ => error "Bad map function";
- val CA_params = map TVar (Term.add_tvarsT CA []);
+ val Calpha_params = map TVar (Term.add_tvarsT Calpha []);
val bnf_T = Morphism.typ phi T_rhs;
val bad_args = Term.add_tfreesT bnf_T [];
val _ = if null bad_args then () else error ("Locally fixed type arguments " ^
commas_quote (map (Syntax.string_of_typ no_defs_lthy o TFree) bad_args));
- val bnf_sets = map2 (normalize_set CA_params) alphas (map (Morphism.term phi) bnf_set_terms);
+ val bnf_sets =
+ map2 (normalize_set Calpha_params) alphas (map (Morphism.term phi) bnf_set_terms);
val bnf_bd =
- Term.subst_TVars (Term.add_tvar_namesT bnf_T [] ~~ CA_params) (Morphism.term phi bnf_bd_term);
+ Term.subst_TVars (Term.add_tvar_namesT bnf_T [] ~~ Calpha_params)
+ (Morphism.term phi bnf_bd_term);
(*TODO: assert Ds = (TVars of bnf_map) \ (alphas @ betas) as sets*)
val deads = (case Ds_opt of
NONE => subtract (op =) (alphas @ betas) (map TVar (Term.add_tvars bnf_map []))
| SOME Ds => map (Morphism.typ phi) Ds);
- val dead = length deads;
(*TODO: further checks of type of bnf_map*)
(*TODO: check types of bnf_sets*)
(*TODO: check type of bnf_bd*)
(*TODO: check type of bnf_rel*)
- val ((((((((((As', Bs'), Cs), Ds), B1Ts), B2Ts), domTs), ranTs), ranTs'), ranTs''),
- (Ts, T)) = lthy
+ fun mk_bnf_map Ds As' Bs' =
+ Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As') @ (betas ~~ Bs')) bnf_map;
+ fun mk_bnf_t Ds As' = Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As'));
+ fun mk_bnf_T Ds As' = Term.typ_subst_atomic ((deads ~~ Ds) @ (alphas ~~ As'));
+
+ val (((As, Bs), Ds), names_lthy) = lthy
+ |> mk_TFrees live
+ ||>> mk_TFrees live
+ ||>> mk_TFrees (length deads);
+ val RTs = map2 (curry HOLogic.mk_prodT) As Bs;
+ val pred2RTs = map2 mk_pred2T As Bs;
+ val (Rs, Rs') = names_lthy |> mk_Frees' "R" pred2RTs |> fst
+ val CA = mk_bnf_T Ds As Calpha;
+ val CR = mk_bnf_T Ds RTs Calpha;
+ val setRs =
+ map3 (fn R => fn T => fn U =>
+ HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split R) Rs As Bs;
+
+ (*Grp (in (Collect (split R1) .. Collect (split Rn))) (map fst .. fst)^--1 OO
+ Grp (in (Collect (split R1) .. Collect (split Rn))) (map snd .. snd)*)
+ val OO_Grp =
+ let
+ val map1 = Term.list_comb (mk_bnf_map Ds RTs As, map fst_const RTs);
+ val map2 = Term.list_comb (mk_bnf_map Ds RTs Bs, map snd_const RTs);
+ val bnf_in = mk_in setRs (map (mk_bnf_t Ds RTs) bnf_sets) CR;
+ in
+ mk_rel_compp (mk_conversep (mk_Grp bnf_in map1), mk_Grp bnf_in map2)
+ |> fold_rev Term.absfree Rs'
+ end;
+
+ val rel_rhs = the_default OO_Grp rel_rhs_opt;
+
+ val rel_bind_def =
+ (fn () => def_qualify (if Binding.is_empty rel_b then mk_prefix_binding relN else rel_b),
+ rel_rhs);
+
+ val wit_rhss =
+ if null wit_rhss then
+ [fold_rev Term.absdummy As (Term.list_comb (mk_bnf_map Ds As As,
+ map2 (fn T => fn i => Term.absdummy T (Bound i)) As (live downto 1)) $
+ Const (@{const_name undefined}, CA))]
+ else wit_rhss;
+ val nwits = length wit_rhss;
+ val wit_binds_defs =
+ let
+ val bs = if nwits = 1 then [fn () => def_qualify (mk_prefix_binding witN)]
+ else map (fn i => fn () => def_qualify (mk_prefix_binding (mk_witN i))) (1 upto nwits);
+ in bs ~~ wit_rhss end;
+
+ val (((bnf_rel_term, raw_rel_def), (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) =
+ lthy
+ |> maybe_define (is_some rel_rhs_opt) rel_bind_def
+ ||>> apfst split_list o fold_map (maybe_define (not (null wit_rhss))) wit_binds_defs
+ ||> `(maybe_restore lthy);
+
+ val phi = Proof_Context.export_morphism lthy_old lthy;
+ val bnf_rel_def = Morphism.thm phi raw_rel_def;
+ val bnf_rel = Morphism.term phi bnf_rel_term;
+ fun mk_bnf_rel Ds As' Bs' =
+ normalize_rel lthy (map2 mk_pred2T As' Bs') (mk_bnf_T Ds As' Calpha) (mk_bnf_T Ds Bs' Calpha)
+ bnf_rel;
+
+ val bnf_wit_defs = map (Morphism.thm phi) raw_wit_defs;
+ val bnf_wits =
+ map (normalize_wit Calpha_params Calpha alphas o Morphism.term phi) bnf_wit_terms;
+
+ fun mk_OO_Grp Ds' As' Bs' =
+ Term.subst_atomic_types ((Ds ~~ Ds') @ (As ~~ As') @ (Bs ~~ Bs')) OO_Grp;
+ in
+ (((alphas, betas, deads, Calpha),
+ (bnf_map, bnf_sets, bnf_bd, bnf_wits, bnf_rel),
+ (bnf_map_def, bnf_set_defs, bnf_bd_def, bnf_wit_defs, bnf_rel_def),
+ (mk_bnf_map, mk_bnf_t, mk_bnf_T, mk_bnf_rel, mk_OO_Grp)), lthy)
+ end;
+
+fun prepare_def const_policy mk_fact_policy qualify prep_typ prep_term Ds_opt map_b rel_b set_bs
+ ((((((raw_bnf_b, raw_bnf_T), raw_map), raw_sets), raw_bd), raw_wits), raw_rel_opt)
+ no_defs_lthy =
+ let
+ val fact_policy = mk_fact_policy no_defs_lthy;
+ val bnf_b = qualify raw_bnf_b;
+ val live = length raw_sets;
+
+ val T_rhs = prep_typ no_defs_lthy raw_bnf_T;
+ val map_rhs = prep_term no_defs_lthy raw_map;
+ val set_rhss = map (prep_term no_defs_lthy) raw_sets;
+ val bd_rhs = prep_term no_defs_lthy raw_bd;
+ val wit_rhss = map (prep_term no_defs_lthy) raw_wits;
+ val rel_rhs_opt = Option.map (prep_term no_defs_lthy) raw_rel_opt;
+
+ fun err T =
+ error ("Trying to register the type " ^ quote (Syntax.string_of_typ no_defs_lthy T) ^
+ " as unnamed BNF");
+
+ val (bnf_b, key) =
+ if Binding.eq_name (bnf_b, Binding.empty) then
+ (case T_rhs of
+ Type (C, Ts) => if forall (can dest_TFree) Ts
+ then (Binding.qualified_name C, C) else err T_rhs
+ | T => err T)
+ else (bnf_b, Local_Theory.full_name no_defs_lthy bnf_b);
+
+ val (((alphas, betas, deads, Calpha),
+ (bnf_map, bnf_sets, bnf_bd, bnf_wits, bnf_rel),
+ (bnf_map_def, bnf_set_defs, bnf_bd_def, bnf_wit_defs, bnf_rel_def),
+ (mk_bnf_map_Ds, mk_bnf_t_Ds, mk_bnf_T_Ds, _, mk_OO_Grp)), lthy) =
+ define_bnf_consts const_policy fact_policy Ds_opt map_b rel_b set_bs
+ ((((((bnf_b, T_rhs), map_rhs), set_rhss), bd_rhs), wit_rhss), rel_rhs_opt) no_defs_lthy;
+
+ val dead = length deads;
+
+ val ((((((As', Bs'), Cs), Ds), B1Ts), B2Ts), (Ts, T)) = lthy
|> mk_TFrees live
||>> mk_TFrees live
||>> mk_TFrees live
||>> mk_TFrees dead
||>> mk_TFrees live
||>> mk_TFrees live
- ||>> mk_TFrees live
- ||>> mk_TFrees live
- ||>> mk_TFrees live
- ||>> mk_TFrees live
||> fst o mk_TFrees 1
||> the_single
||> `(replicate live);
- fun mk_bnf_map As' Bs' =
- Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As') @ (betas ~~ Bs')) bnf_map;
- fun mk_bnf_t As' = Term.subst_atomic_types ((deads ~~ Ds) @ (alphas ~~ As'));
- fun mk_bnf_T As' = Term.typ_subst_atomic ((deads ~~ Ds) @ (alphas ~~ As'));
+ val mk_bnf_map = mk_bnf_map_Ds Ds;
+ val mk_bnf_t = mk_bnf_t_Ds Ds;
+ val mk_bnf_T = mk_bnf_T_Ds Ds;
- val RTs = map HOLogic.mk_prodT (As' ~~ Bs');
val pred2RTs = map2 mk_pred2T As' Bs';
val pred2RTsAsCs = map2 mk_pred2T As' Cs;
val pred2RTsBsCs = map2 mk_pred2T Bs' Cs;
@@ -803,12 +893,11 @@
val transfer_domRTs = map2 mk_pred2T As' B1Ts;
val transfer_ranRTs = map2 mk_pred2T Bs' B2Ts;
- val CA' = mk_bnf_T As' CA;
- val CB' = mk_bnf_T Bs' CA;
- val CC' = mk_bnf_T Cs CA;
- val CRs' = mk_bnf_T RTs CA;
- val CB1 = mk_bnf_T B1Ts CA;
- val CB2 = mk_bnf_T B2Ts CA;
+ val CA' = mk_bnf_T As' Calpha;
+ val CB' = mk_bnf_T Bs' Calpha;
+ val CC' = mk_bnf_T Cs Calpha;
+ val CB1 = mk_bnf_T B1Ts Calpha;
+ val CB2 = mk_bnf_T B2Ts Calpha;
val bnf_map_AsAs = mk_bnf_map As' As';
val bnf_map_AsBs = mk_bnf_map As' Bs';
@@ -817,10 +906,11 @@
val bnf_sets_As = map (mk_bnf_t As') bnf_sets;
val bnf_sets_Bs = map (mk_bnf_t Bs') bnf_sets;
val bnf_bd_As = mk_bnf_t As' bnf_bd;
+ fun mk_bnf_rel RTs CA CB = normalize_rel lthy RTs CA CB bnf_rel;
val pre_names_lthy = lthy;
- val ((((((((((((((((((((((((fs, gs), hs), x), y), zs), ys), As),
- As_copy), Xs), B1s), B2s), f1s), f2s), e1s), e2s), p1s), p2s), bs), (Rs, Rs')), Rs_copy), Ss),
+ val (((((((((((((((fs, gs), hs), x), y), zs), ys), As),
+ As_copy), bs), Rs), Rs_copy), Ss),
transfer_domRs), transfer_ranRs), names_lthy) = pre_names_lthy
|> mk_Frees "f" (map2 (curry op -->) As' Bs')
||>> mk_Frees "g" (map2 (curry op -->) Bs' Cs)
@@ -831,17 +921,8 @@
||>> mk_Frees "y" Bs'
||>> mk_Frees "A" (map HOLogic.mk_setT As')
||>> mk_Frees "A" (map HOLogic.mk_setT As')
- ||>> mk_Frees "A" (map HOLogic.mk_setT domTs)
- ||>> mk_Frees "B1" (map HOLogic.mk_setT B1Ts)
- ||>> mk_Frees "B2" (map HOLogic.mk_setT B2Ts)
- ||>> mk_Frees "f1" (map2 (curry op -->) B1Ts ranTs)
- ||>> mk_Frees "f2" (map2 (curry op -->) B2Ts ranTs)
- ||>> mk_Frees "e1" (map2 (curry op -->) B1Ts ranTs')
- ||>> mk_Frees "e2" (map2 (curry op -->) B2Ts ranTs'')
- ||>> mk_Frees "p1" (map2 (curry op -->) domTs B1Ts)
- ||>> mk_Frees "p2" (map2 (curry op -->) domTs B2Ts)
||>> mk_Frees "b" As'
- ||>> mk_Frees' "R" pred2RTs
+ ||>> mk_Frees "R" pred2RTs
||>> mk_Frees "R" pred2RTs
||>> mk_Frees "S" pred2RTsBsCs
||>> mk_Frees "R" transfer_domRTs
@@ -850,59 +931,8 @@
val fs_copy = map2 (retype_free o fastype_of) fs gs;
val x_copy = retype_free CA' y;
- val setRs =
- map3 (fn R => fn T => fn U =>
- HOLogic.Collect_const (HOLogic.mk_prodT (T, U)) $ HOLogic.mk_split R) Rs As' Bs';
-
- (*Grp (in (Collect (split R1) .. Collect (split Rn))) (map fst .. fst)^--1 OO
- Grp (in (Collect (split R1) .. Collect (split Rn))) (map snd .. snd)*)
- val OO_Grp =
- let
- val map1 = Term.list_comb (mk_bnf_map RTs As', map fst_const RTs);
- val map2 = Term.list_comb (mk_bnf_map RTs Bs', map snd_const RTs);
- val bnf_in = mk_in setRs (map (mk_bnf_t RTs) bnf_sets) CRs';
- in
- mk_rel_compp (mk_conversep (mk_Grp bnf_in map1), mk_Grp bnf_in map2)
- end;
-
- val rel_rhs = (case raw_rel_opt of
- NONE => fold_rev Term.absfree Rs' OO_Grp
- | SOME raw_rel => prep_term no_defs_lthy raw_rel);
-
- val rel_bind_def =
- (fn () => def_qualify (if Binding.is_empty rel_b then mk_prefix_binding relN else rel_b),
- rel_rhs);
-
- val wit_rhss =
- if null raw_wits then
- [fold_rev Term.absdummy As' (Term.list_comb (bnf_map_AsAs,
- map2 (fn T => fn i => Term.absdummy T (Bound i)) As' (live downto 1)) $
- Const (@{const_name undefined}, CA'))]
- else map (prep_term no_defs_lthy) raw_wits;
- val nwits = length wit_rhss;
- val wit_binds_defs =
- let
- val bs = if nwits = 1 then [fn () => def_qualify (mk_prefix_binding witN)]
- else map (fn i => fn () => def_qualify (mk_prefix_binding (mk_witN i))) (1 upto nwits);
- in bs ~~ wit_rhss end;
-
- val (((bnf_rel_term, raw_rel_def), (bnf_wit_terms, raw_wit_defs)), (lthy, lthy_old)) =
- lthy
- |> maybe_define (is_some raw_rel_opt) rel_bind_def
- ||>> apfst split_list o fold_map (maybe_define (not (null raw_wits))) wit_binds_defs
- ||> `(maybe_restore lthy);
-
- val phi = Proof_Context.export_morphism lthy_old lthy;
- val bnf_rel_def = Morphism.thm phi raw_rel_def;
- val bnf_rel = Morphism.term phi bnf_rel_term;
-
- fun mk_bnf_rel RTs CA' CB' = normalize_rel lthy RTs CA' CB' bnf_rel;
-
val rel = mk_bnf_rel pred2RTs CA' CB';
val relAsAs = mk_bnf_rel self_pred2RTs CA' CA';
-
- val bnf_wit_defs = map (Morphism.thm phi) raw_wit_defs;
- val bnf_wits = map (normalize_wit CA_params CA alphas o Morphism.term phi) bnf_wit_terms;
val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits;
val map_id0_goal =
@@ -959,31 +989,18 @@
map mk_goal bnf_sets_As
end;
- val map_wpull_goal =
- let
- val prems = map HOLogic.mk_Trueprop
- (map8 mk_wpull Xs B1s B2s f1s f2s (replicate live NONE) p1s p2s);
- val CX = mk_bnf_T domTs CA;
- val bnf_sets_CX = map2 (normalize_set (map (mk_bnf_T domTs) CA_params)) domTs bnf_sets;
- val bnf_sets_CB1 = map2 (normalize_set (map (mk_bnf_T B1Ts) CA_params)) B1Ts bnf_sets;
- val bnf_sets_CB2 = map2 (normalize_set (map (mk_bnf_T B2Ts) CA_params)) B2Ts bnf_sets;
- val bnf_map_app_f1 = Term.list_comb (mk_bnf_map B1Ts ranTs, f1s);
- val bnf_map_app_f2 = Term.list_comb (mk_bnf_map B2Ts ranTs, f2s);
- val bnf_map_app_p1 = Term.list_comb (mk_bnf_map domTs B1Ts, p1s);
- val bnf_map_app_p2 = Term.list_comb (mk_bnf_map domTs B2Ts, p2s);
+ val relAsCs = mk_bnf_rel pred2RTsAsCs CA' CC';
+ val relBsCs = mk_bnf_rel pred2RTsBsCs CB' CC';
+ val rel_OO_lhs = Term.list_comb (relAsCs, map2 (curry mk_rel_compp) Rs Ss);
+ val rel_OO_rhs = mk_rel_compp (Term.list_comb (rel, Rs), Term.list_comb (relBsCs, Ss));
+ val le_rel_OO_goal =
+ fold_rev Logic.all (Rs @ Ss) (HOLogic.mk_Trueprop (mk_leq rel_OO_rhs rel_OO_lhs));
- val map_wpull = mk_wpull (mk_in Xs bnf_sets_CX CX)
- (mk_in B1s bnf_sets_CB1 CB1) (mk_in B2s bnf_sets_CB2 CB2)
- bnf_map_app_f1 bnf_map_app_f2 NONE bnf_map_app_p1 bnf_map_app_p2;
- in
- fold_rev Logic.all (Xs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s)
- (Logic.list_implies (prems, HOLogic.mk_Trueprop map_wpull))
- end;
-
- val rel_OO_Grp_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs), OO_Grp));
+ val rel_OO_Grp_goal = fold_rev Logic.all Rs (mk_Trueprop_eq (Term.list_comb (rel, Rs),
+ Term.list_comb (mk_OO_Grp Ds As' Bs', Rs)));
val goals = zip_axioms map_id0_goal map_comp0_goal map_cong0_goal set_map0s_goal
- card_order_bd_goal cinfinite_bd_goal set_bds_goal map_wpull_goal rel_OO_Grp_goal;
+ card_order_bd_goal cinfinite_bd_goal set_bds_goal le_rel_OO_goal rel_OO_Grp_goal;
fun mk_wit_goals (I, wit) =
let
@@ -1018,7 +1035,7 @@
fun mk_collect_set_map () =
let
- val defT = mk_bnf_T Ts CA --> HOLogic.mk_setT T;
+ val defT = mk_bnf_T Ts Calpha --> HOLogic.mk_setT T;
val collect_map = HOLogic.mk_comp
(mk_collect (map (mk_bnf_t Ts) bnf_sets) defT,
Term.list_comb (mk_bnf_map As' Ts, hs));
@@ -1090,12 +1107,12 @@
let
val bdT = fst (dest_relT (fastype_of bnf_bd_As));
val bdTs = replicate live bdT;
- val bd_bnfT = mk_bnf_T bdTs CA;
+ val bd_bnfT = mk_bnf_T bdTs Calpha;
val surj_imp_ordLeq_inst = (if live = 0 then TrueI else
let
val ranTs = map (fn AT => mk_sumT (AT, HOLogic.unitT)) As';
val funTs = map (fn T => bdT --> T) ranTs;
- val ran_bnfT = mk_bnf_T ranTs CA;
+ val ran_bnfT = mk_bnf_T ranTs Calpha;
val (revTs, Ts) = `rev (bd_bnfT :: funTs);
val cTs = map (SOME o certifyT lthy) [ran_bnfT, Library.foldr1 HOLogic.mk_prodT Ts];
val tinst = fold (fn T => fn t => HOLogic.mk_split (Term.absdummy T t)) (tl revTs)
@@ -1123,42 +1140,6 @@
val in_bd = Lazy.lazy mk_in_bd;
- fun mk_map_wppull () =
- let
- val prems = if live = 0 then [] else
- [HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map8 mk_wpull Xs B1s B2s f1s f2s (map SOME (e1s ~~ e2s)) p1s p2s))];
- val CX = mk_bnf_T domTs CA;
- val bnf_sets_CX =
- map2 (normalize_set (map (mk_bnf_T domTs) CA_params)) domTs bnf_sets;
- val bnf_sets_CB1 =
- map2 (normalize_set (map (mk_bnf_T B1Ts) CA_params)) B1Ts bnf_sets;
- val bnf_sets_CB2 =
- map2 (normalize_set (map (mk_bnf_T B2Ts) CA_params)) B2Ts bnf_sets;
- val bnf_map_app_f1 = Term.list_comb (mk_bnf_map B1Ts ranTs, f1s);
- val bnf_map_app_f2 = Term.list_comb (mk_bnf_map B2Ts ranTs, f2s);
- val bnf_map_app_e1 = Term.list_comb (mk_bnf_map B1Ts ranTs', e1s);
- val bnf_map_app_e2 = Term.list_comb (mk_bnf_map B2Ts ranTs'', e2s);
- val bnf_map_app_p1 = Term.list_comb (mk_bnf_map domTs B1Ts, p1s);
- val bnf_map_app_p2 = Term.list_comb (mk_bnf_map domTs B2Ts, p2s);
-
- val concl = mk_wpull (mk_in Xs bnf_sets_CX CX)
- (mk_in B1s bnf_sets_CB1 CB1) (mk_in B2s bnf_sets_CB2 CB2)
- bnf_map_app_f1 bnf_map_app_f2 (SOME (bnf_map_app_e1, bnf_map_app_e2))
- bnf_map_app_p1 bnf_map_app_p2;
-
- val goal =
- fold_rev Logic.all (Xs @ B1s @ B2s @ f1s @ f2s @ e1s @ e2s @ p1s @ p2s)
- (Logic.list_implies (prems, HOLogic.mk_Trueprop concl))
- in
- Goal.prove_sorry lthy [] [] goal
- (fn _ => mk_map_wppull_tac (#map_id0 axioms) (#map_cong0 axioms)
- (#map_wpull axioms) (Lazy.force map_comp) (map Lazy.force set_map))
- |> Thm.close_derivation
- end;
-
- val map_wppull = Lazy.lazy mk_map_wppull;
-
val rel_OO_Grp = #rel_OO_Grp axioms;
val rel_OO_Grps = no_refl [rel_OO_Grp];
@@ -1234,18 +1215,12 @@
val rel_conversep = Lazy.lazy mk_rel_conversep;
fun mk_rel_OO () =
- let
- val relAsCs = mk_bnf_rel pred2RTsAsCs CA' CC';
- val relBsCs = mk_bnf_rel pred2RTsBsCs CB' CC';
- val lhs = Term.list_comb (relAsCs, map2 (curry mk_rel_compp) Rs Ss);
- val rhs = mk_rel_compp (Term.list_comb (rel, Rs), Term.list_comb (relBsCs, Ss));
- val goal = fold_rev Logic.all (Rs @ Ss) (mk_Trueprop_eq (lhs, rhs));
- in
- Goal.prove_sorry lthy [] [] goal
- (mk_rel_OO_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms)
- (Lazy.force map_wppull) (Lazy.force map_comp) (map Lazy.force set_map))
- |> Thm.close_derivation
- end;
+ Goal.prove_sorry lthy [] []
+ (fold_rev Logic.all (Rs @ Ss) (HOLogic.mk_Trueprop (mk_leq rel_OO_lhs rel_OO_rhs)))
+ (mk_rel_OO_le_tac rel_OO_Grps (Lazy.force rel_eq) (#map_cong0 axioms)
+ (Lazy.force map_comp) (map Lazy.force set_map))
+ |> Thm.close_derivation
+ |> (fn thm => @{thm antisym} OF [thm, #le_rel_OO axioms]);
val rel_OO = Lazy.lazy mk_rel_OO;
@@ -1305,7 +1280,7 @@
val defs = mk_defs bnf_map_def bnf_set_defs bnf_rel_def;
val facts = mk_facts bd_Card_order bd_Cinfinite bd_Cnotzero collect_set_map in_bd in_cong
- in_mono in_rel map_comp map_cong map_id map_transfer map_wppull rel_eq rel_flip set_map
+ in_mono in_rel map_comp map_cong map_id map_transfer rel_eq rel_flip set_map
rel_cong rel_mono rel_mono_strong rel_Grp rel_conversep rel_OO;
val wits = map2 mk_witness bnf_wits wit_thms;
@@ -1313,8 +1288,8 @@
val bnf_rel =
Term.subst_atomic_types ((Ds ~~ deads) @ (As' ~~ alphas) @ (Bs' ~~ betas)) rel;
- val bnf = mk_bnf bnf_b CA live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms defs
- facts wits bnf_rel;
+ val bnf = mk_bnf bnf_b Calpha live alphas betas dead deads bnf_map bnf_sets bnf_bd axioms
+ defs facts wits bnf_rel;
in
(bnf, lthy |> note_bnf_thms fact_policy qualify bnf_b bnf)
end;
@@ -1336,7 +1311,8 @@
K (TRYALL Goal.conjunction_tac) THEN'
(case triv_tac_opt of
SOME tac => tac set_maps
- | NONE => mk_unfold_thms_then_tac lthy one_step_defs wit_tac);
+ | NONE => fn {context = ctxt, prems} =>
+ unfold_thms_tac ctxt one_step_defs THEN wit_tac {context = ctxt, prems = prems});
val wit_goals = map Logic.mk_conjunction_balanced wit_goalss;
fun mk_wit_thms set_maps =
Goal.prove_sorry lthy [] [] (Logic.mk_conjunction_balanced wit_goals) (mk_wits_tac set_maps)
@@ -1345,7 +1321,8 @@
|> map (map (Thm.close_derivation o Thm.forall_elim_vars 0));
in
map2 (Thm.close_derivation oo Goal.prove_sorry lthy [] [])
- goals (map (mk_unfold_thms_then_tac lthy one_step_defs) tacs)
+ goals (map (fn tac => fn {context = ctxt, prems} =>
+ unfold_thms_tac ctxt one_step_defs THEN tac {context = ctxt, prems = prems}) tacs)
|> (fn thms => after_qed mk_wit_thms (map single thms) lthy)
end) oo prepare_def const_policy fact_policy qualify (K I) (K I) Ds map_b rel_b set_bs;
--- a/src/HOL/BNF/Tools/bnf_def_tactics.ML Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_def_tactics.ML Wed Dec 18 11:03:40 2013 +0100
@@ -13,13 +13,12 @@
val mk_map_comp: thm -> thm
val mk_map_cong_tac: Proof.context -> thm -> tactic
val mk_in_mono_tac: int -> tactic
- val mk_map_wppull_tac: thm -> thm -> thm -> thm -> thm list -> tactic
val mk_set_map: thm -> thm
val mk_rel_Grp_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
{prems: thm list, context: Proof.context} -> tactic
val mk_rel_eq_tac: int -> thm -> thm -> thm -> tactic
- val mk_rel_OO_tac: thm list -> thm -> thm -> thm -> thm -> thm list ->
+ val mk_rel_OO_le_tac: thm list -> thm -> thm -> thm -> thm list ->
{prems: thm list, context: Proof.context} -> tactic
val mk_rel_conversep_tac: thm -> thm -> tactic
val mk_rel_conversep_le_tac: thm list -> thm -> thm -> thm -> thm list ->
@@ -68,22 +67,6 @@
rtac set_map0) set_map0s) THEN'
rtac @{thm image_empty}) 1;
-fun mk_map_wppull_tac map_id0 map_cong0 map_wpull map_comp set_maps =
- if null set_maps then
- EVERY' [rtac @{thm wppull_id}, rtac map_wpull, rtac map_id0, rtac map_id0] 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 ord_eq_le_trans),
- rtac @{thm image_subsetI}, rtac conjunct1, etac bspec, etac set_mp, atac])
- set_maps,
- CONJ_WRAP' (fn thm => EVERY' [rtac (map_comp RS trans), rtac (map_comp RS trans),
- rtac (map_comp RS trans RS sym), rtac map_cong0,
- REPEAT_DETERM_N (length set_maps) 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_Grp_tac rel_OO_Grps map_id0 map_cong0 map_id map_comp set_maps
{context = ctxt, prems = _} =
let
@@ -163,7 +146,7 @@
rtac le_conversep, rtac @{thm iffD2[OF conversep_mono]}, rtac rel_mono,
REPEAT_DETERM o rtac @{thm eq_refl[OF sym[OF conversep_conversep]]}] 1;
-fun mk_rel_OO_tac rel_OO_Grps rel_eq map_cong0 map_wppull map_comp set_maps
+fun mk_rel_OO_le_tac rel_OO_Grps rel_eq map_cong0 map_comp set_maps
{context = ctxt, prems = _} =
let
val n = length set_maps;
@@ -171,13 +154,13 @@
CONJ_WRAP' (fn thm => EVERY' [rtac (thm RS ord_eq_le_trans),
rtac @{thm image_subsetI}, rtac nthO_in, etac set_mp, atac]) set_maps;
val rel_OO_Grps_tac = if null rel_OO_Grps then K all_tac
- else rtac (hd rel_OO_Grps RS trans) THEN'
+ else rtac (hd rel_OO_Grps RS ord_eq_le_trans) THEN'
rtac (@{thm arg_cong2[of _ _ _ _ "op OO"]} OF (replicate 2 (hd rel_OO_Grps RS sym)) RSN
- (2, trans));
+ (2, ord_le_eq_trans));
in
- if null set_maps then rtac (rel_eq RS @{thm eq_OOI}) 1
+ if null set_maps then rtac (rel_eq RS @{thm leq_OOI}) 1
else
- EVERY' [rel_OO_Grps_tac, rtac @{thm antisym}, rtac @{thm predicate2I},
+ EVERY' [rel_OO_Grps_tac, rtac @{thm predicate2I},
REPEAT_DETERM o
eresolve_tac [CollectE, exE, conjE, @{thm GrpE}, @{thm relcomppE}, @{thm conversepE}],
hyp_subst_tac ctxt,
@@ -197,18 +180,7 @@
in_tac @{thm sndOp_in},
rtac @{thm GrpI}, rtac trans, rtac map_comp, rtac sym, rtac map_cong0,
REPEAT_DETERM_N n o rtac @{thm snd_sndOp},
- in_tac @{thm sndOp_in},
- rtac @{thm predicate2I},
- REPEAT_DETERM o eresolve_tac [@{thm relcomppE}, @{thm conversepE}, @{thm GrpE}],
- hyp_subst_tac ctxt,
- rtac allE, rtac subst, rtac @{thm wppull_def}, rtac map_wppull,
- CONJ_WRAP' (K (rtac @{thm wppull_fstOp_sndOp})) set_maps,
- etac allE, etac impE, etac conjI, etac conjI, etac sym,
- REPEAT_DETERM o eresolve_tac [bexE, conjE],
- rtac @{thm relcomppI}, rtac @{thm conversepI},
- EVERY' (map (fn thm => EVERY' [rtac @{thm GrpI}, rtac trans,
- rtac trans, rtac map_cong0, REPEAT_DETERM_N n o rtac thm,
- rtac (map_comp RS sym), atac, atac]) [@{thm fst_fstOp}, @{thm snd_sndOp}])] 1
+ in_tac @{thm sndOp_in}] 1
end;
fun mk_rel_mono_strong_tac in_rel set_maps {context = ctxt, prems = _} =
--- a/src/HOL/BNF/Tools/bnf_gfp.ML Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Wed Dec 18 11:03:40 2013 +0100
@@ -85,16 +85,13 @@
val passives = map fst (subtract (op = o apsnd TFree) deads resBs);
(* tvars *)
- val ((((((((passiveAs, activeAs), passiveBs), activeBs), passiveCs), activeCs), passiveXs),
- passiveYs), idxT) = names_lthy
+ val ((((((passiveAs, activeAs), passiveBs), activeBs), passiveCs), activeCs), idxT) = names_lthy
|> variant_tfrees passives
||>> mk_TFrees n
||>> variant_tfrees passives
||>> mk_TFrees n
||>> mk_TFrees m
||>> mk_TFrees n
- ||>> mk_TFrees m
- ||>> mk_TFrees m
||> fst o mk_TFrees 1
||> the_single;
@@ -168,14 +165,15 @@
val hrecTs = map fastype_of Zeros;
val hsetTs = map (fn hrecT => Library.foldr (op -->) (sTs, HOLogic.natT --> hrecT)) hrecTs;
- val ((((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2),
- z's), As), Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy),
+ val (((((((((((((((((((((((((((((((((((zs, zs'), zs_copy), zs_copy2), z's), (ys, ys')),
+ As), Bs), Bs_copy), B's), B''s), ss), sum_ss), s's), s''s), fs), fs_copy),
self_fs), gs), all_gs), xFs), yFs), yFs_copy), RFs), (Rtuple, Rtuple')), (hrecs, hrecs')),
(nat, nat')), Rs), Rs_copy), R's), sRs), (idx, idx')), Idx), Ris), Kss), names_lthy) = lthy
|> mk_Frees' "b" activeAs
||>> mk_Frees "b" activeAs
||>> mk_Frees "b" activeAs
||>> mk_Frees "b" activeBs
+ ||>> mk_Frees' "y" passiveAs
||>> mk_Frees "A" ATs
||>> mk_Frees "B" BTs
||>> mk_Frees "B" BTs
@@ -230,7 +228,6 @@
val map_cong0s = map map_cong0_of_bnf bnfs;
val map_id0s = map map_id0_of_bnf bnfs;
val map_ids = map map_id_of_bnf bnfs;
- val map_wpulls = map map_wpull_of_bnf bnfs;
val set_bdss = map set_bd_of_bnf bnfs;
val set_mapss = map set_map_of_bnf bnfs;
val rel_congs = map rel_cong_of_bnf bnfs;
@@ -667,25 +664,6 @@
val set_hset_thmss' = transpose set_hset_thmss;
val set_hset_hset_thmsss' = transpose (map transpose set_hset_hset_thmsss);
- val set_incl_hin_thmss =
- let
- fun mk_set_incl_hin s x hsets1 set hsets2 T =
- fold_rev Logic.all (x :: ss @ As)
- (Logic.list_implies
- (map2 (fn hset => fn A => HOLogic.mk_Trueprop (mk_leq (hset $ x) A)) hsets1 As,
- HOLogic.mk_Trueprop (mk_leq (set $ (s $ x)) (mk_in As hsets2 T))));
-
- val set_incl_hin_goalss =
- map4 (fn s => fn x => fn sets => fn hsets =>
- map3 (mk_set_incl_hin s x hsets) (drop m sets) hsetssAs activeAs)
- ss zs setssAs hsetssAs;
- in
- map2 (map2 (fn goal => fn thms =>
- Goal.prove_sorry lthy [] [] goal (K (mk_set_incl_hin_tac thms))
- |> Thm.close_derivation))
- set_incl_hin_goalss set_hset_incl_hset_thmsss
- end;
-
val hset_minimal_thms =
let
fun mk_passive_prem set s x K =
@@ -1648,7 +1626,6 @@
val Ts = map (fn name => Type (name, params')) T_names;
fun mk_Ts passive = map (Term.typ_subst_atomic (passiveAs ~~ passive)) Ts;
val Ts' = mk_Ts passiveBs;
- val Ts'' = mk_Ts passiveCs;
val Rep_Ts = map2 (fn info => fn T => Const (#Rep_name info, T --> treeQT)) T_glob_infos Ts;
val Abs_Ts = map2 (fn info => fn T => Const (#Abs_name info, treeQT --> T)) T_glob_infos Ts;
@@ -1679,21 +1656,21 @@
val corec_Inls = map (Term.subst_atomic_types (activeBs ~~ Ts)) Inls;
val corec_UNIVs = map2 (HOLogic.mk_UNIV oo curry mk_sumT) Ts activeAs;
- val ((((((((((((((Jzs, Jzs'), (Jz's, Jz's')), Jzs_copy), Jz's_copy), Jzs1), Jzs2), Jpairs),
- FJzs), TRs), unfold_fs), unfold_fs_copy), corec_ss), phis), names_lthy) = names_lthy
+ val (((((((((((((Jzs, Jzs'), Jz's), Jzs_copy), Jz's_copy), Jzs1), Jzs2),
+ FJzs), TRs), unfold_fs), corec_ss), phis), dtor_set_induct_phiss),
+ names_lthy) = names_lthy
|> mk_Frees' "z" Ts
- ||>> mk_Frees' "y" Ts'
+ ||>> mk_Frees "y" Ts'
||>> mk_Frees "z'" Ts
||>> mk_Frees "y'" Ts'
||>> mk_Frees "z1" Ts
||>> mk_Frees "z2" Ts
- ||>> mk_Frees "j" (map2 (curry HOLogic.mk_prodT) Ts Ts')
||>> mk_Frees "x" prodFTs
||>> mk_Frees "r" (map (mk_relT o `I) Ts)
||>> mk_Frees "f" unfold_fTs
- ||>> mk_Frees "g" unfold_fTs
||>> mk_Frees "s" corec_sTs
- ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts);
+ ||>> mk_Frees "P" (map2 mk_pred2T Ts Ts)
+ ||>> mk_Freess "P" (map (fn A => map (mk_pred2T A) Ts) passiveAs);
fun dtor_bind i = nth external_bs (i - 1) |> Binding.prefix_name (dtorN ^ "_");
val dtor_name = Binding.name_of o dtor_bind;
@@ -1812,25 +1789,6 @@
|> Thm.close_derivation)
end;
- val unique_mor_thms =
- let
- val prems = [HOLogic.mk_Trueprop (mk_coalg passive_UNIVs Bs ss), HOLogic.mk_Trueprop
- (HOLogic.mk_conj (mk_mor Bs ss UNIVs dtors unfold_fs,
- mk_mor Bs ss UNIVs dtors unfold_fs_copy))];
- fun mk_fun_eq B f g z = HOLogic.mk_imp
- (HOLogic.mk_mem (z, B), HOLogic.mk_eq (f $ z, g $ z));
- val unique = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map4 mk_fun_eq Bs unfold_fs unfold_fs_copy zs));
-
- val unique_mor = Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (Bs @ ss @ unfold_fs @ unfold_fs_copy @ zs)
- (Logic.list_implies (prems, unique)))
- (K (mk_unique_mor_tac raw_coind_thms bis_image2_thm))
- |> Thm.close_derivation;
- in
- map (fn thm => conjI RSN (2, thm RS mp)) (split_conj_thm unique_mor)
- end;
-
val (unfold_unique_mor_thms, unfold_unique_mor_thm) =
let
val prem = HOLogic.mk_Trueprop (mk_mor active_UNIVs ss UNIVs dtors unfold_fs);
@@ -2086,6 +2044,59 @@
val timer = time (timer "coinduction");
+ val setss_by_bnf = map (fn i => map2 (mk_hset dtors i) ls passiveAs) ks;
+ val setss_by_range = transpose setss_by_bnf;
+
+ val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) =
+ let
+ fun tinst_of dtor =
+ map (SOME o certify lthy) (dtor :: remove (op =) dtor dtors);
+ fun tinst_of' dtor = case tinst_of dtor of t :: ts => t :: NONE :: ts;
+ val Tinst = map (pairself (certifyT lthy))
+ (map Logic.varifyT_global (deads @ allAs) ~~ (deads @ passiveAs @ Ts));
+ val set_incl_thmss =
+ map2 (fn dtor => map (singleton (Proof_Context.export names_lthy lthy) o
+ Drule.instantiate' [] (tinst_of' dtor) o
+ Thm.instantiate (Tinst, []) o Drule.zero_var_indexes))
+ dtors set_incl_hset_thmss;
+
+ val tinst = splice (map (SOME o certify lthy) dtors) (replicate n NONE)
+ val set_minimal_thms =
+ map (Drule.instantiate' [] tinst o Thm.instantiate (Tinst, []) o
+ Drule.zero_var_indexes)
+ hset_minimal_thms;
+
+ val set_set_incl_thmsss =
+ map2 (fn dtor => map (map (singleton (Proof_Context.export names_lthy lthy) o
+ Drule.instantiate' [] (NONE :: tinst_of' dtor) o
+ Thm.instantiate (Tinst, []) o Drule.zero_var_indexes)))
+ dtors set_hset_incl_hset_thmsss;
+
+ val set_set_incl_thmsss' = transpose (map transpose set_set_incl_thmsss);
+
+ val incls =
+ maps (map (fn thm => thm RS @{thm subset_Collect_iff})) set_incl_thmss @
+ @{thms subset_Collect_iff[OF subset_refl]};
+
+ fun mk_induct_tinst phis jsets y y' =
+ map4 (fn phi => fn jset => fn Jz => fn Jz' =>
+ SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y',
+ HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz))))))
+ phis jsets Jzs Jzs';
+ val dtor_set_induct_thms =
+ map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis =>
+ ((set_minimal
+ |> Drule.instantiate' [] (mk_induct_tinst phis jsets y y')
+ |> unfold_thms lthy incls) OF
+ (replicate n ballI @
+ maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss))
+ |> singleton (Proof_Context.export names_lthy lthy)
+ |> rule_by_tactic lthy (ALLGOALS (TRY o etac asm_rl)))
+ set_minimal_thms set_set_incl_thmsss' setss_by_range ys ys' dtor_set_induct_phiss
+ in
+ (set_incl_thmss, set_set_incl_thmsss, dtor_set_induct_thms)
+ end;
+
fun mk_dtor_map_DEADID_thm dtor_inject map_id0 =
trans OF [iffD2 OF [dtor_inject, id_apply], map_id0 RS sym];
@@ -2093,60 +2104,49 @@
trans OF [rel_eq_of_bnf bnf RS @{thm predicate2_eqD}, dtor_inject] RS sym;
val JphiTs = map2 mk_pred2T passiveAs passiveBs;
+ val Jpsi1Ts = map2 mk_pred2T passiveAs passiveCs;
+ val Jpsi2Ts = map2 mk_pred2T passiveCs passiveBs;
val prodTsTs' = map2 (curry HOLogic.mk_prodT) Ts Ts';
val fstsTsTs' = map fst_const prodTsTs';
val sndsTsTs' = map snd_const prodTsTs';
val activephiTs = map2 mk_pred2T activeAs activeBs;
val activeJphiTs = map2 mk_pred2T Ts Ts';
- val (((Jphis, activephis), activeJphis), names_lthy) = names_lthy
+ val (((((Jphis, Jpsi1s), Jpsi2s), activephis), activeJphis), names_lthy) = names_lthy
|> mk_Frees "R" JphiTs
+ ||>> mk_Frees "R" Jpsi1Ts
+ ||>> mk_Frees "Q" Jpsi2Ts
||>> mk_Frees "S" activephiTs
||>> mk_Frees "JR" activeJphiTs;
val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
val in_rels = map in_rel_of_bnf bnfs;
+ fun mk_Jrel_DEADID_coinduct_thm () =
+ mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis (map HOLogic.eq_const Ts) Jphis
+ Jzs Jz's dtors dtor's (fn {context = ctxt, prems} =>
+ (unfold_thms_tac ctxt @{thms le_fun_def le_bool_def all_simps(1,2)[symmetric]} THEN
+ REPEAT_DETERM (rtac allI 1) THEN rtac (dtor_coinduct_thm OF prems) 1)) lthy;
+
(*register new codatatypes as BNFs*)
- val (timer, Jbnfs, (folded_dtor_map_o_thms, folded_dtor_map_thms), folded_dtor_set_thmss',
- dtor_set_induct_thms, dtor_Jrel_thms, Jbnf_notes, lthy) =
+ val (timer, Jbnfs, (dtor_Jmap_o_thms, dtor_Jmap_thms), dtor_Jset_thmss',
+ dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_notes, lthy) =
if m = 0 then
(timer, replicate n DEADID_bnf,
map_split (`(mk_pointfree lthy)) (map2 mk_dtor_map_DEADID_thm dtor_inject_thms map_ids),
- replicate n [], [], map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs, [], lthy)
+ replicate n [], map2 mk_dtor_Jrel_DEADID_thm dtor_inject_thms bnfs,
+ mk_Jrel_DEADID_coinduct_thm (), [], lthy)
else let
val fTs = map2 (curry op -->) passiveAs passiveBs;
val gTs = map2 (curry op -->) passiveBs passiveCs;
- val f1Ts = map2 (curry op -->) passiveAs passiveYs;
- val f2Ts = map2 (curry op -->) passiveBs passiveYs;
- val p1Ts = map2 (curry op -->) passiveXs passiveAs;
- val p2Ts = map2 (curry op -->) passiveXs passiveBs;
- val pTs = map2 (curry op -->) passiveXs passiveCs;
val uTs = map2 (curry op -->) Ts Ts';
- val B1Ts = map HOLogic.mk_setT passiveAs;
- val B2Ts = map HOLogic.mk_setT passiveBs;
- val AXTs = map HOLogic.mk_setT passiveXs;
- val XTs = mk_Ts passiveXs;
- val YTs = mk_Ts passiveYs;
-
- val ((((((((((((((((((fs, fs'), fs_copy), gs), us),
- (Jys, Jys')), (Jys_copy, Jys'_copy)), dtor_set_induct_phiss),
- B1s), B2s), AXs), f1s), f2s), p1s), p2s), ps), (ys, ys')), (ys_copy, ys'_copy)),
- names_lthy) = names_lthy
+
+ val ((((((((fs, fs'), fs_copy), gs), us), (Jys, Jys')), (Jys_copy, Jys'_copy)),
+ (ys_copy, ys'_copy)), names_lthy) = names_lthy
|> mk_Frees' "f" fTs
||>> mk_Frees "f" fTs
||>> mk_Frees "g" gTs
||>> mk_Frees "u" uTs
||>> mk_Frees' "b" Ts'
||>> mk_Frees' "b" Ts'
- ||>> mk_Freess "P" (map (fn A => map (mk_pred2T A) Ts) passiveAs)
- ||>> mk_Frees "B1" B1Ts
- ||>> mk_Frees "B2" B2Ts
- ||>> mk_Frees "A" AXTs
- ||>> mk_Frees "f1" f1Ts
- ||>> mk_Frees "f2" f2Ts
- ||>> mk_Frees "p1" p1Ts
- ||>> mk_Frees "p2" p2Ts
- ||>> mk_Frees "p" pTs
- ||>> mk_Frees' "y" passiveAs
||>> mk_Frees' "y" passiveAs;
val map_FTFT's = map2 (fn Ds =>
@@ -2160,382 +2160,11 @@
HOLogic.mk_comp (mk_Fmap mk_const fs Ts Fmap, dtor)) dtors (mk_maps Ts mk_T));
val mk_map_id = mk_map HOLogic.id_const I;
val mk_mapsAB = mk_maps passiveAs passiveBs;
- val mk_mapsBC = mk_maps passiveBs passiveCs;
- val mk_mapsAC = mk_maps passiveAs passiveCs;
- val mk_mapsAY = mk_maps passiveAs passiveYs;
- val mk_mapsBY = mk_maps passiveBs passiveYs;
- val mk_mapsXA = mk_maps passiveXs passiveAs;
- val mk_mapsXB = mk_maps passiveXs passiveBs;
- val mk_mapsXC = mk_maps passiveXs passiveCs;
val fs_maps = map (mk_map_id Ts fs Ts' dtors mk_mapsAB) ks;
- val fs_copy_maps = map (mk_map_id Ts fs_copy Ts' dtors mk_mapsAB) ks;
- val gs_maps = map (mk_map_id Ts' gs Ts'' dtor's mk_mapsBC) ks;
- val fgs_maps =
- map (mk_map_id Ts (map2 (curry HOLogic.mk_comp) gs fs) Ts'' dtors mk_mapsAC) ks;
- val Xdtors = mk_dtors passiveXs;
- val UNIV's = map HOLogic.mk_UNIV Ts';
- val CUNIVs = map HOLogic.mk_UNIV passiveCs;
- val UNIV''s = map HOLogic.mk_UNIV Ts'';
- val dtor''s = mk_dtors passiveCs;
- val f1s_maps = map (mk_map_id Ts f1s YTs dtors mk_mapsAY) ks;
- val f2s_maps = map (mk_map_id Ts' f2s YTs dtor's mk_mapsBY) ks;
- val pid_maps = map (mk_map_id XTs ps Ts'' Xdtors mk_mapsXC) ks;
- val pfst_Fmaps =
- map (mk_Fmap fst_const p1s prodTsTs') (mk_mapsXA prodTsTs' (fst o HOLogic.dest_prodT));
- val psnd_Fmaps =
- map (mk_Fmap snd_const p2s prodTsTs') (mk_mapsXB prodTsTs' (snd o HOLogic.dest_prodT));
- val p1id_Fmaps = map (mk_Fmap HOLogic.id_const p1s prodTsTs') (mk_mapsXA prodTsTs' I);
- val p2id_Fmaps = map (mk_Fmap HOLogic.id_const p2s prodTsTs') (mk_mapsXB prodTsTs' I);
- val pid_Fmaps = map (mk_Fmap HOLogic.id_const ps prodTsTs') (mk_mapsXC prodTsTs' I);
-
- val (dtor_map_thms, map_thms) =
- let
- fun mk_goal fs_map map dtor dtor' = fold_rev Logic.all fs
- (mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_map),
- HOLogic.mk_comp (Term.list_comb (map, fs @ fs_maps), dtor)));
- val goals = map4 mk_goal fs_maps map_FTFT's dtors dtor's;
- val cTs = map (SOME o certifyT lthy) FTs';
- val maps =
- map5 (fn goal => fn cT => fn unfold => fn map_comp => fn map_cong0 =>
- Goal.prove_sorry lthy [] [] goal
- (K (mk_map_tac m n cT unfold map_comp map_cong0))
- |> Thm.close_derivation)
- goals cTs dtor_unfold_thms map_comps map_cong0s;
- in
- map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps
- end;
-
- val map_comp0_thms =
- let
- val goal = fold_rev Logic.all (fs @ gs)
- (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map3 (fn fmap => fn gmap => fn fgmap =>
- HOLogic.mk_eq (HOLogic.mk_comp (gmap, fmap), fgmap))
- fs_maps gs_maps fgs_maps)))
- in
- split_conj_thm (Goal.prove_sorry lthy [] [] goal
- (K (mk_map_comp0_tac m n map_thms map_comp0s map_cong0s dtor_unfold_unique_thm))
- |> Thm.close_derivation)
- end;
-
- val dtor_map_unique_thm =
- let
- fun mk_prem u map dtor dtor' =
- mk_Trueprop_eq (HOLogic.mk_comp (dtor', u),
- HOLogic.mk_comp (Term.list_comb (map, fs @ us), dtor));
- val prems = map4 mk_prem us map_FTFT's dtors dtor's;
- val goal =
- HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map2 (curry HOLogic.mk_eq) us fs_maps));
- in
- Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
- (mk_dtor_map_unique_tac dtor_unfold_unique_thm sym_map_comps)
- |> Thm.close_derivation
- end;
-
- val timer = time (timer "map functions for the new codatatypes");
-
- val setss_by_bnf = map (fn i => map2 (mk_hset dtors i) ls passiveAs) ks;
- val setss_by_bnf' = map (fn i => map2 (mk_hset dtor's i) ls passiveBs) ks;
- val setss_by_range = transpose setss_by_bnf;
-
- val dtor_set_thmss =
- let
- fun mk_simp_goal relate pas_set act_sets sets dtor z set =
- relate (set $ z, mk_union (pas_set $ (dtor $ z),
- Library.foldl1 mk_union
- (map2 (fn X => mk_UNION (X $ (dtor $ z))) act_sets sets)));
- fun mk_goals eq =
- map2 (fn i => fn sets =>
- map4 (fn Fsets =>
- mk_simp_goal eq (nth Fsets (i - 1)) (drop m Fsets) sets)
- FTs_setss dtors Jzs sets)
- ls setss_by_range;
-
- val le_goals = map
- (fold_rev Logic.all Jzs o HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj)
- (mk_goals (uncurry mk_leq));
- val set_le_thmss = map split_conj_thm
- (map4 (fn goal => fn hset_minimal => fn set_hsets => fn set_hset_hsetss =>
- Goal.prove_sorry lthy [] [] goal
- (K (mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss))
- |> Thm.close_derivation)
- le_goals hset_minimal_thms set_hset_thmss' set_hset_hset_thmsss');
-
- val simp_goalss = map (map2 (fn z => fn goal =>
- Logic.all z (HOLogic.mk_Trueprop goal)) Jzs)
- (mk_goals HOLogic.mk_eq);
- in
- map4 (map4 (fn goal => fn set_le => fn set_incl_hset => fn set_hset_incl_hsets =>
- Goal.prove_sorry lthy [] [] goal
- (K (mk_dtor_set_tac n set_le set_incl_hset set_hset_incl_hsets))
- |> Thm.close_derivation))
- simp_goalss set_le_thmss set_incl_hset_thmss' set_hset_incl_hset_thmsss'
- end;
-
- val timer = time (timer "set functions for the new codatatypes");
-
- val colss = map2 (fn j => fn T =>
- map (fn i => mk_hset_rec dtors nat i j T) ks) ls passiveAs;
- val colss' = map2 (fn j => fn T =>
- map (fn i => mk_hset_rec dtor's nat i j T) ks) ls passiveBs;
- val Xcolss = map2 (fn j => fn T =>
- map (fn i => mk_hset_rec Xdtors nat i j T) ks) ls passiveXs;
-
- val col_natural_thmss =
- let
- fun mk_col_natural f map z col col' =
- HOLogic.mk_eq (mk_image f $ (col $ z), col' $ (map $ z));
-
- fun mk_goal f cols cols' = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj
- (map4 (mk_col_natural f) fs_maps Jzs cols cols'));
-
- val goals = map3 mk_goal fs colss colss';
-
- val ctss =
- map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals;
-
- val thms =
- map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
- singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
- (mk_col_natural_tac cts rec_0s rec_Sucs dtor_map_thms set_mapss))
- |> Thm.close_derivation)
- goals ctss hset_rec_0ss' hset_rec_Sucss';
- in
- map (split_conj_thm o mk_specN n) thms
- end;
-
- val col_bd_thmss =
- let
- fun mk_col_bd z col = mk_ordLeq (mk_card_of (col $ z)) sbd;
-
- fun mk_goal cols = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj
- (map2 mk_col_bd Jzs cols));
-
- val goals = map mk_goal colss;
-
- val ctss =
- map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals;
-
- val thms =
- map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
- singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
- (K (mk_col_bd_tac m j cts rec_0s rec_Sucs
- sbd_Card_order sbd_Cinfinite set_sbdss)))
- |> Thm.close_derivation)
- ls goals ctss hset_rec_0ss' hset_rec_Sucss';
- in
- map (split_conj_thm o mk_specN n) thms
- end;
-
- val map_cong0_thms =
- let
- val cTs = map (SOME o certifyT lthy o
- Term.typ_subst_atomic (passiveAs ~~ passiveBs) o TFree) coinduct_params;
-
- fun mk_prem z set f g y y' =
- mk_Ball (set $ z) (Term.absfree y' (HOLogic.mk_eq (f $ y, g $ y)));
-
- fun mk_prems sets z =
- Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys')
-
- fun mk_map_cong0 sets z fmap gmap =
- HOLogic.mk_imp (mk_prems sets z, HOLogic.mk_eq (fmap $ z, gmap $ z));
-
- fun mk_coind_body sets (x, T) z fmap gmap y y_copy =
- HOLogic.mk_conj
- (HOLogic.mk_mem (z, HOLogic.mk_Collect (x, T, mk_prems sets z)),
- HOLogic.mk_conj (HOLogic.mk_eq (y, fmap $ z),
- HOLogic.mk_eq (y_copy, gmap $ z)))
-
- fun mk_cphi sets (z' as (x, T)) z fmap gmap y' y y'_copy y_copy =
- HOLogic.mk_exists (x, T, mk_coind_body sets z' z fmap gmap y y_copy)
- |> Term.absfree y'_copy
- |> Term.absfree y'
- |> certify lthy;
-
- val cphis =
- map9 mk_cphi setss_by_bnf Jzs' Jzs fs_maps fs_copy_maps Jys' Jys Jys'_copy Jys_copy;
-
- val coinduct = Drule.instantiate' cTs (map SOME cphis) dtor_map_coinduct_thm;
-
- val goal =
- HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map4 mk_map_cong0 setss_by_bnf Jzs fs_maps fs_copy_maps));
-
- val thm = singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] goal
- (K (mk_mcong_tac lthy m (rtac coinduct) map_comps dtor_map_thms map_cong0s set_mapss
- set_hset_thmss set_hset_hset_thmsss)))
- |> Thm.close_derivation
- in
- split_conj_thm thm
- end;
-
- val B1_ins = map2 (mk_in B1s) setss_by_bnf Ts;
- val B2_ins = map2 (mk_in B2s) setss_by_bnf' Ts';
- val thePulls = map4 mk_thePull B1_ins B2_ins f1s_maps f2s_maps;
- val thePullTs = passiveXs @ map2 (curry HOLogic.mk_prodT) Ts Ts';
- val thePull_ins = map2 (mk_in (AXs @ thePulls)) (mk_setss thePullTs) (mk_FTs thePullTs);
- val pickFs = map5 mk_pickWP thePull_ins pfst_Fmaps psnd_Fmaps
- (map2 (curry op $) dtors Jzs) (map2 (curry op $) dtor's Jz's);
- val pickF_ss = map3 (fn pickF => fn z => fn z' =>
- HOLogic.mk_split (Term.absfree z (Term.absfree z' pickF))) pickFs Jzs' Jz's';
- val picks = map (mk_unfold XTs pickF_ss) ks;
-
- val wpull_prem = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map8 mk_wpull AXs B1s B2s f1s f2s (replicate m NONE) p1s p2s));
-
- val map_eq_thms = map2 (fn simp => fn diff => box_equals OF [diff RS iffD2, simp, simp])
- dtor_map_thms dtor_inject_thms;
- val map_wpull_thms = map (fn thm => thm OF
- (replicate m asm_rl @ replicate n @{thm wpull_thePull})) map_wpulls;
- val pickWP_assms_tacs =
- map3 mk_pickWP_assms_tac set_incl_hset_thmss set_incl_hin_thmss map_eq_thms;
-
- val coalg_thePull_thm =
- let
- val coalg = HOLogic.mk_Trueprop
- (mk_coalg CUNIVs thePulls (map2 (curry HOLogic.mk_comp) pid_Fmaps pickF_ss));
- val goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s @ ps)
- (Logic.mk_implies (wpull_prem, coalg));
- in
- Goal.prove_sorry lthy [] [] goal (mk_coalg_thePull_tac m coalg_def map_wpull_thms
- set_mapss pickWP_assms_tacs)
- |> Thm.close_derivation
- end;
-
- val (mor_thePull_fst_thm, mor_thePull_snd_thm, mor_thePull_pick_thm) =
- let
- val mor_fst = HOLogic.mk_Trueprop
- (mk_mor thePulls (map2 (curry HOLogic.mk_comp) p1id_Fmaps pickF_ss)
- UNIVs dtors fstsTsTs');
- val mor_snd = HOLogic.mk_Trueprop
- (mk_mor thePulls (map2 (curry HOLogic.mk_comp) p2id_Fmaps pickF_ss)
- UNIV's dtor's sndsTsTs');
- val mor_pick = HOLogic.mk_Trueprop
- (mk_mor thePulls (map2 (curry HOLogic.mk_comp) pid_Fmaps pickF_ss)
- UNIV''s dtor''s (map2 (curry HOLogic.mk_comp) pid_maps picks));
-
- val fst_goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s)
- (Logic.mk_implies (wpull_prem, mor_fst));
- val snd_goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s)
- (Logic.mk_implies (wpull_prem, mor_snd));
- val pick_goal = fold_rev Logic.all (AXs @ B1s @ B2s @ f1s @ f2s @ p1s @ p2s @ ps)
- (Logic.mk_implies (wpull_prem, mor_pick));
- in
- (Goal.prove_sorry lthy [] [] fst_goal (mk_mor_thePull_fst_tac m mor_def map_wpull_thms
- map_comps pickWP_assms_tacs) |> Thm.close_derivation,
- Goal.prove_sorry lthy [] [] snd_goal (mk_mor_thePull_snd_tac m mor_def map_wpull_thms
- map_comps pickWP_assms_tacs) |> Thm.close_derivation,
- Goal.prove_sorry lthy [] [] pick_goal (mk_mor_thePull_pick_tac mor_def dtor_unfold_thms
- map_comps) |> Thm.close_derivation)
- end;
-
- val pick_col_thmss =
- let
- fun mk_conjunct AX Jpair pick thePull col =
- HOLogic.mk_imp (HOLogic.mk_mem (Jpair, thePull), mk_leq (col $ (pick $ Jpair)) AX);
-
- fun mk_concl AX cols =
- list_all_free Jpairs (Library.foldr1 HOLogic.mk_conj
- (map4 (mk_conjunct AX) Jpairs picks thePulls cols));
-
- val concls = map2 mk_concl AXs Xcolss;
-
- val ctss =
- map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) concls;
-
- val goals =
- map (fn concl => Logic.mk_implies (wpull_prem, HOLogic.mk_Trueprop concl)) concls;
-
- val thms =
- map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
- singleton (Proof_Context.export names_lthy lthy) (Goal.prove_sorry lthy [] [] goal
- (mk_pick_col_tac m j cts rec_0s rec_Sucs dtor_unfold_thms set_mapss
- map_wpull_thms pickWP_assms_tacs))
- |> Thm.close_derivation)
- ls goals ctss hset_rec_0ss' hset_rec_Sucss';
- in
- map (map (fn thm => thm RS mp) o split_conj_thm o mk_specN n) thms
- end;
-
- val timer = time (timer "helpers for BNF properties");
-
- val map_id0_tacs =
- map2 (K oo mk_map_id0_tac map_thms) dtor_unfold_unique_thms unfold_dtor_thms;
- val map_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) map_comp0_thms;
- val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
- val set_nat_tacss =
- map2 (map2 (K oo mk_set_map0_tac)) hset_defss (transpose col_natural_thmss);
-
- val bd_co_tacs = replicate n (K (rtac sbd_card_order 1));
- val bd_cinf_tacs = replicate n (K (rtac (sbd_Cinfinite RS conjunct1) 1));
-
- val set_bd_tacss =
- map2 (map2 (K oo mk_set_bd_tac sbd_Cinfinite)) hset_defss (transpose col_bd_thmss);
-
- val map_wpull_tacs =
- map3 (K ooo mk_wpull_tac m coalg_thePull_thm mor_thePull_fst_thm mor_thePull_snd_thm
- mor_thePull_pick_thm) unique_mor_thms (transpose pick_col_thmss) hset_defss;
-
- val rel_OO_Grp_tacs = replicate n (K (rtac refl 1));
-
- val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_nat_tacss
- bd_co_tacs bd_cinf_tacs set_bd_tacss map_wpull_tacs rel_OO_Grp_tacs;
-
- val (hset_dtor_incl_thmss, hset_hset_dtor_incl_thmsss, dtor_hset_induct_thms) =
- let
- fun tinst_of dtor =
- map (SOME o certify lthy) (dtor :: remove (op =) dtor dtors);
- fun tinst_of' dtor = case tinst_of dtor of t :: ts => t :: NONE :: ts;
- val Tinst = map (pairself (certifyT lthy))
- (map Logic.varifyT_global (deads @ allAs) ~~ (deads @ passiveAs @ Ts));
- val set_incl_thmss =
- map2 (fn dtor => map (singleton (Proof_Context.export names_lthy lthy) o
- Drule.instantiate' [] (tinst_of' dtor) o
- Thm.instantiate (Tinst, []) o Drule.zero_var_indexes))
- dtors set_incl_hset_thmss;
-
- val tinst = splice (map (SOME o certify lthy) dtors) (replicate n NONE)
- val set_minimal_thms =
- map (Drule.instantiate' [] tinst o Thm.instantiate (Tinst, []) o
- Drule.zero_var_indexes)
- hset_minimal_thms;
-
- val set_set_incl_thmsss =
- map2 (fn dtor => map (map (singleton (Proof_Context.export names_lthy lthy) o
- Drule.instantiate' [] (NONE :: tinst_of' dtor) o
- Thm.instantiate (Tinst, []) o Drule.zero_var_indexes)))
- dtors set_hset_incl_hset_thmsss;
-
- val set_set_incl_thmsss' = transpose (map transpose set_set_incl_thmsss);
-
- val incls =
- maps (map (fn thm => thm RS @{thm subset_Collect_iff})) set_incl_thmss @
- @{thms subset_Collect_iff[OF subset_refl]};
-
- fun mk_induct_tinst phis jsets y y' =
- map4 (fn phi => fn jset => fn Jz => fn Jz' =>
- SOME (certify lthy (Term.absfree Jz' (HOLogic.mk_Collect (fst y', snd y',
- HOLogic.mk_conj (HOLogic.mk_mem (y, jset $ Jz), phi $ y $ Jz))))))
- phis jsets Jzs Jzs';
- val dtor_set_induct_thms =
- map6 (fn set_minimal => fn set_set_inclss => fn jsets => fn y => fn y' => fn phis =>
- ((set_minimal
- |> Drule.instantiate' [] (mk_induct_tinst phis jsets y y')
- |> unfold_thms lthy incls) OF
- (replicate n ballI @
- maps (map (fn thm => thm RS @{thm subset_CollectI})) set_set_inclss))
- |> singleton (Proof_Context.export names_lthy lthy)
- |> rule_by_tactic lthy (ALLGOALS (TRY o etac asm_rl)))
- set_minimal_thms set_set_incl_thmsss' setss_by_range ys ys' dtor_set_induct_phiss
- in
- (set_incl_thmss, set_set_incl_thmsss, dtor_set_induct_thms)
- end;
+
+ val set_bss =
+ map (flat o map2 (fn B => fn b =>
+ if member (op =) resDs (TFree B) then [] else [b]) resBs) set_bss0;
fun close_wit I wit = (I, fold_rev Term.absfree (map (nth ys') I) wit);
@@ -2622,6 +2251,14 @@
val coind_witss =
maps (map (mk_coind_wits o prepare_args)) nonredundant_coind_wit_argsss;
+ val witss = map2 (fn Ds => fn bnf => mk_wits_of_bnf
+ (replicate (nwits_of_bnf bnf) Ds)
+ (replicate (nwits_of_bnf bnf) (passiveAs @ Ts)) bnf) Dss bnfs;
+
+ val ctor_witss =
+ map (map (uncurry close_wit o tree_to_ctor_wit ys ctors witss o snd o snd) o
+ filter_out (fst o snd)) wit_treess;
+
fun mk_coind_wit_thms ((I, dummys), (wits, wit_thms)) =
let
fun mk_goal sets y y_copy y'_copy j =
@@ -2653,57 +2290,253 @@
val coind_wit_thms = maps mk_coind_wit_thms coind_witss;
- val witss = map2 (fn Ds => fn bnf => mk_wits_of_bnf
- (replicate (nwits_of_bnf bnf) Ds)
- (replicate (nwits_of_bnf bnf) (passiveAs @ Ts)) bnf) Dss bnfs;
-
- val ctor_witss =
- map (map (uncurry close_wit o tree_to_ctor_wit ys ctors witss o snd o snd) o
- filter_out (fst o snd)) wit_treess;
-
- val all_witss =
+ val (wit_thmss, all_witss) =
fold (fn ((i, wit), thms) => fn witss =>
nth_map i (fn (thms', wits) => (thms @ thms', wit :: wits)) witss)
coind_wit_thms (map (pair []) ctor_witss)
- |> map (apsnd (map snd o minimize_wits));
-
- val wit_tac = mk_wit_tac n dtor_ctor_thms (flat dtor_set_thmss) (maps wit_thms_of_bnf bnfs);
-
- val set_bss =
- map (flat o map2 (fn B => fn b =>
- if member (op =) resDs (TFree B) then [] else [b]) resBs) set_bss0;
-
- val (Jbnfs, lthy) =
- fold_map9 (fn tacs => fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets =>
- fn T => fn (thms, wits) => fn lthy =>
- bnf_def Dont_Inline (user_policy Note_Some) I tacs (wit_tac thms) (SOME deads) map_b
- rel_b set_bs
- ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy
- |> register_bnf (Local_Theory.full_name lthy b))
- tacss bs map_bs rel_bs set_bss fs_maps setss_by_bnf Ts all_witss lthy;
-
- val fold_maps = fold_thms lthy (map (fn bnf =>
- mk_unabs_def m (map_def_of_bnf bnf RS meta_eq_to_obj_eq)) Jbnfs);
-
- val fold_sets = fold_thms lthy (maps (fn bnf =>
- map (fn thm => thm RS meta_eq_to_obj_eq) (set_defs_of_bnf bnf)) Jbnfs);
-
- val timer = time (timer "registered new codatatypes as BNFs");
-
- val dtor_set_incl_thmss = map (map fold_sets) hset_dtor_incl_thmss;
- val dtor_set_set_incl_thmsss = map (map (map fold_sets)) hset_hset_dtor_incl_thmsss;
- val dtor_set_induct_thms = map fold_sets dtor_hset_induct_thms;
-
- val Jrels = map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs;
-
- val Jrelphis = map (fn Jrel => Term.list_comb (Jrel, Jphis)) Jrels;
+ |> map (apsnd (map snd o minimize_wits))
+ |> split_list;
+
+ val (Jbnf_consts, lthy) =
+ fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits =>
+ fn T => fn lthy =>
+ define_bnf_consts Dont_Inline (user_policy Note_Some lthy) (SOME deads)
+ map_b rel_b set_bs
+ ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sbd), wits), NONE) lthy)
+ bs map_bs rel_bs set_bss fs_maps setss_by_bnf all_witss Ts lthy;
+
+ val (_, Jconsts, Jconst_defs, mk_Jconsts) = split_list4 Jbnf_consts;
+ val (_, Jsetss, Jbds_Ds, Jwitss_Ds, _) = split_list5 Jconsts;
+ val (Jmap_defs, Jset_defss, Jbd_defs, Jwit_defss, Jrel_defs) = split_list5 Jconst_defs;
+ val (mk_Jmaps_Ds, mk_Jt_Ds, _, mk_Jrels_Ds, _) = split_list5 mk_Jconsts;
+
+ val Jrel_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Jrel_defs;
+ val Jset_defs = flat Jset_defss;
+ val Jset_unabs_defs = map (fn def => def RS meta_eq_to_obj_eq RS fun_cong) Jset_defs;
+
+ fun mk_Jmaps As Bs = map (fn mk => mk deads As Bs) mk_Jmaps_Ds;
+ fun mk_Jsetss As = map2 (fn mk => fn Jsets => map (mk deads As) Jsets) mk_Jt_Ds Jsetss;
+ val Jbds = map2 (fn mk => mk deads passiveAs) mk_Jt_Ds Jbds_Ds;
+ val Jwitss =
+ map2 (fn mk => fn Jwits => map (mk deads passiveAs o snd) Jwits) mk_Jt_Ds Jwitss_Ds;
+ fun mk_Jrels As Bs = map (fn mk => mk deads As Bs) mk_Jrels_Ds;
+
+ val Jmaps = mk_Jmaps passiveAs passiveBs;
+ val fs_Jmaps = map (fn m => Term.list_comb (m, fs)) Jmaps;
+ val fs_copy_Jmaps = map (fn m => Term.list_comb (m, fs_copy)) Jmaps;
+ val gs_Jmaps = map (fn m => Term.list_comb (m, gs)) (mk_Jmaps passiveBs passiveCs);
+ val fgs_Jmaps = map (fn m => Term.list_comb (m, map2 (curry HOLogic.mk_comp) gs fs))
+ (mk_Jmaps passiveAs passiveCs);
+ val (Jsetss_by_range, Jsetss_by_bnf) = `transpose (mk_Jsetss passiveAs);
+
+ val timer = time (timer "bnf constants for the new datatypes");
+
+ val (dtor_Jmap_thms, Jmap_thms) =
+ let
+ fun mk_goal fs_Jmap map dtor dtor' = fold_rev Logic.all fs
+ (mk_Trueprop_eq (HOLogic.mk_comp (dtor', fs_Jmap),
+ HOLogic.mk_comp (Term.list_comb (map, fs @ fs_Jmaps), dtor)));
+ val goals = map4 mk_goal fs_Jmaps map_FTFT's dtors dtor's;
+ val cTs = map (SOME o certifyT lthy) FTs';
+ val maps =
+ map5 (fn goal => fn cT => fn unfold => fn map_comp => fn map_cong0 =>
+ Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
+ mk_map_tac m n cT unfold map_comp map_cong0)
+ |> Thm.close_derivation)
+ goals cTs dtor_unfold_thms map_comps map_cong0s;
+ in
+ map_split (fn thm => (thm RS @{thm comp_eq_dest}, thm)) maps
+ end;
+
+ val dtor_Jmap_unique_thm =
+ let
+ fun mk_prem u map dtor dtor' =
+ mk_Trueprop_eq (HOLogic.mk_comp (dtor', u),
+ HOLogic.mk_comp (Term.list_comb (map, fs @ us), dtor));
+ val prems = map4 mk_prem us map_FTFT's dtors dtor's;
+ val goal =
+ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
+ (map2 (curry HOLogic.mk_eq) us fs_Jmaps));
+ in
+ Goal.prove_sorry lthy [] []
+ (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
+ (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jmap_defs THEN
+ mk_dtor_map_unique_tac dtor_unfold_unique_thm sym_map_comps ctxt)
+ |> Thm.close_derivation
+ end;
+
+ val Jmap_comp0_thms =
+ let
+ val goal = fold_rev Logic.all (fs @ gs)
+ (HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
+ (map3 (fn fmap => fn gmap => fn fgmap =>
+ HOLogic.mk_eq (HOLogic.mk_comp (gmap, fmap), fgmap))
+ fs_Jmaps gs_Jmaps fgs_Jmaps)))
+ in
+ split_conj_thm (Goal.prove_sorry lthy [] [] goal
+ (K (mk_map_comp0_tac Jmap_thms map_comp0s dtor_Jmap_unique_thm))
+ |> Thm.close_derivation)
+ end;
+
+ val timer = time (timer "map functions for the new codatatypes");
+
+ val (dtor_Jset_thmss', dtor_Jset_thmss) =
+ let
+ fun mk_simp_goal relate pas_set act_sets sets dtor z set =
+ relate (set $ z, mk_union (pas_set $ (dtor $ z),
+ Library.foldl1 mk_union
+ (map2 (fn X => mk_UNION (X $ (dtor $ z))) act_sets sets)));
+ fun mk_goals eq =
+ map2 (fn i => fn sets =>
+ map4 (fn Fsets =>
+ mk_simp_goal eq (nth Fsets (i - 1)) (drop m Fsets) sets)
+ FTs_setss dtors Jzs sets)
+ ls Jsetss_by_range;
+
+ val le_goals = map
+ (fold_rev Logic.all Jzs o HOLogic.mk_Trueprop o Library.foldr1 HOLogic.mk_conj)
+ (mk_goals (uncurry mk_leq));
+ val set_le_thmss = map split_conj_thm
+ (map4 (fn goal => fn hset_minimal => fn set_hsets => fn set_hset_hsetss =>
+ Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
+ mk_set_le_tac n hset_minimal set_hsets set_hset_hsetss)
+ |> Thm.close_derivation)
+ le_goals hset_minimal_thms set_hset_thmss' set_hset_hset_thmsss');
+
+ val ge_goalss = map (map2 (fn z => fn goal =>
+ Logic.all z (HOLogic.mk_Trueprop goal)) Jzs)
+ (mk_goals (uncurry mk_leq o swap));
+ val set_ge_thmss =
+ map3 (map3 (fn goal => fn set_incl_hset => fn set_hset_incl_hsets =>
+ Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
+ mk_set_ge_tac n set_incl_hset set_hset_incl_hsets)
+ |> Thm.close_derivation))
+ ge_goalss set_incl_hset_thmss' set_hset_incl_hset_thmsss'
+ in
+ map2 (map2 (fn le => fn ge => equalityI OF [le, ge])) set_le_thmss set_ge_thmss
+ |> `transpose
+ end;
+
+ val timer = time (timer "set functions for the new codatatypes");
+
+ val colss = map2 (fn j => fn T =>
+ map (fn i => mk_hset_rec dtors nat i j T) ks) ls passiveAs;
+ val colss' = map2 (fn j => fn T =>
+ map (fn i => mk_hset_rec dtor's nat i j T) ks) ls passiveBs;
+
+ val col_natural_thmss =
+ let
+ fun mk_col_natural f map z col col' =
+ HOLogic.mk_eq (mk_image f $ (col $ z), col' $ (map $ z));
+
+ fun mk_goal f cols cols' = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj
+ (map4 (mk_col_natural f) fs_Jmaps Jzs cols cols'));
+
+ val goals = map3 mk_goal fs colss colss';
+
+ val ctss =
+ map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat]) goals;
+
+ val thms =
+ map4 (fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
+ singleton (Proof_Context.export names_lthy lthy)
+ (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
+ (mk_col_natural_tac cts rec_0s rec_Sucs dtor_Jmap_thms set_mapss))
+ |> Thm.close_derivation)
+ goals ctss hset_rec_0ss' hset_rec_Sucss';
+ in
+ map (split_conj_thm o mk_specN n) thms
+ end;
+
+ val col_bd_thmss =
+ let
+ fun mk_col_bd z col bd = mk_ordLeq (mk_card_of (col $ z)) bd;
+
+ fun mk_goal bds cols = list_all_free Jzs (Library.foldr1 HOLogic.mk_conj
+ (map3 mk_col_bd Jzs cols bds));
+
+ val goals = map (mk_goal Jbds) colss;
+
+ val ctss = map (fn phi => map (SOME o certify lthy) [Term.absfree nat' phi, nat])
+ (map (mk_goal (replicate n sbd)) colss);
+
+ val thms =
+ map5 (fn j => fn goal => fn cts => fn rec_0s => fn rec_Sucs =>
+ singleton (Proof_Context.export names_lthy lthy)
+ (Goal.prove_sorry lthy [] [] (HOLogic.mk_Trueprop goal)
+ (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jbd_defs THEN
+ mk_col_bd_tac m j cts rec_0s rec_Sucs sbd_Card_order sbd_Cinfinite set_sbdss))
+ |> Thm.close_derivation)
+ ls goals ctss hset_rec_0ss' hset_rec_Sucss';
+ in
+ map (split_conj_thm o mk_specN n) thms
+ end;
+
+ val map_cong0_thms =
+ let
+ val cTs = map (SOME o certifyT lthy o
+ Term.typ_subst_atomic (passiveAs ~~ passiveBs) o TFree) coinduct_params;
+
+ fun mk_prem z set f g y y' =
+ mk_Ball (set $ z) (Term.absfree y' (HOLogic.mk_eq (f $ y, g $ y)));
+
+ fun mk_prems sets z =
+ Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys')
+
+ fun mk_map_cong0 sets z fmap gmap =
+ HOLogic.mk_imp (mk_prems sets z, HOLogic.mk_eq (fmap $ z, gmap $ z));
+
+ fun mk_coind_body sets (x, T) z fmap gmap y y_copy =
+ HOLogic.mk_conj
+ (HOLogic.mk_mem (z, HOLogic.mk_Collect (x, T, mk_prems sets z)),
+ HOLogic.mk_conj (HOLogic.mk_eq (y, fmap $ z),
+ HOLogic.mk_eq (y_copy, gmap $ z)))
+
+ fun mk_cphi sets (z' as (x, T)) z fmap gmap y' y y'_copy y_copy =
+ HOLogic.mk_exists (x, T, mk_coind_body sets z' z fmap gmap y y_copy)
+ |> Term.absfree y'_copy
+ |> Term.absfree y'
+ |> certify lthy;
+
+ val cphis = map9 mk_cphi
+ Jsetss_by_bnf Jzs' Jzs fs_Jmaps fs_copy_Jmaps Jys' Jys Jys'_copy Jys_copy;
+
+ val coinduct = unfold_thms lthy Jset_defs
+ (Drule.instantiate' cTs (map SOME cphis) dtor_map_coinduct_thm);
+
+ val goal =
+ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
+ (map4 mk_map_cong0 Jsetss_by_bnf Jzs fs_Jmaps fs_copy_Jmaps));
+
+ val thm = singleton (Proof_Context.export names_lthy lthy)
+ (Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Jset_defs THEN
+ mk_mcong_tac lthy m (rtac coinduct) map_comps dtor_Jmap_thms map_cong0s
+ set_mapss set_hset_thmss set_hset_hset_thmsss))
+ |> Thm.close_derivation
+ in
+ split_conj_thm thm
+ end;
+
+ val in_Jrels = map (fn def => trans OF [def, @{thm OO_Grp_alt}] RS @{thm predicate2_eqD})
+ Jrel_unabs_defs;
+
+ val fold_Jsets = fold_thms lthy Jset_unabs_defs;
+ val dtor_Jset_incl_thmss = map (map fold_Jsets) hset_dtor_incl_thmss;
+ val dtor_set_Jset_incl_thmsss = map (map (map fold_Jsets)) hset_hset_dtor_incl_thmsss;
+ val dtor_Jset_induct_thms = map fold_Jsets dtor_hset_induct_thms;
+ val Jwit_thmss = map (map fold_Jsets) wit_thmss;
+
+ val Jrels = mk_Jrels passiveAs passiveBs;
+ val Jrelphis = map (fn rel => Term.list_comb (rel, Jphis)) Jrels;
val relphis = map (fn rel => Term.list_comb (rel, Jphis @ Jrelphis)) rels;
- val in_Jrels = map in_rel_of_bnf Jbnfs;
-
- val folded_dtor_map_thms = map fold_maps dtor_map_thms;
- val folded_dtor_map_o_thms = map fold_maps map_thms;
- val folded_dtor_set_thmss = map (map fold_sets) dtor_set_thmss;
- val folded_dtor_set_thmss' = transpose folded_dtor_set_thmss;
+ val Jrelpsi1s = map (fn rel => Term.list_comb (rel, Jpsi1s)) (mk_Jrels passiveAs passiveCs);
+ val Jrelpsi2s = map (fn rel => Term.list_comb (rel, Jpsi2s)) (mk_Jrels passiveCs passiveBs);
+ val Jrelpsi12s = map (fn rel =>
+ Term.list_comb (rel, map2 (curry mk_rel_compp) Jpsi1s Jpsi2s)) Jrels;
val dtor_Jrel_thms =
let
@@ -2718,43 +2551,11 @@
(K (mk_dtor_rel_tac lthy in_Jrels i in_rel map_comp0 map_cong0 dtor_map dtor_sets
dtor_inject dtor_ctor set_map0s dtor_set_incls dtor_set_set_inclss))
|> Thm.close_derivation)
- ks goals in_rels map_comps map_cong0s folded_dtor_map_thms folded_dtor_set_thmss'
- dtor_inject_thms dtor_ctor_thms set_mapss dtor_set_incl_thmss
- dtor_set_set_incl_thmsss
+ ks goals in_rels map_comps map_cong0s dtor_Jmap_thms dtor_Jset_thmss'
+ dtor_inject_thms dtor_ctor_thms set_mapss dtor_Jset_incl_thmss
+ dtor_set_Jset_incl_thmsss
end;
- val timer = time (timer "additional properties");
-
- val ls' = if m = 1 then [0] else ls;
-
- val Jbnf_common_notes =
- [(dtor_map_uniqueN, [fold_maps dtor_map_unique_thm])] @
- map2 (fn i => fn thm => (mk_dtor_set_inductN i, [thm])) ls' dtor_set_induct_thms
- |> map (fn (thmN, thms) =>
- ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
-
- val Jbnf_notes =
- [(dtor_mapN, map single folded_dtor_map_thms),
- (dtor_relN, map single dtor_Jrel_thms),
- (dtor_set_inclN, dtor_set_incl_thmss),
- (dtor_set_set_inclN, map flat dtor_set_set_incl_thmsss)] @
- map2 (fn i => fn thms => (mk_dtor_setN i, map single thms)) ls' folded_dtor_set_thmss
- |> maps (fn (thmN, thmss) =>
- map2 (fn b => fn thms =>
- ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
- bs thmss)
- in
- (timer, Jbnfs, (folded_dtor_map_o_thms, folded_dtor_map_thms), folded_dtor_set_thmss',
- dtor_set_induct_thms, dtor_Jrel_thms, Jbnf_common_notes @ Jbnf_notes, lthy)
- end;
-
- val dtor_unfold_o_map_thms = mk_xtor_un_fold_o_map_thms Greatest_FP false m
- dtor_unfold_unique_thm folded_dtor_map_o_thms (map (mk_pointfree lthy) dtor_unfold_thms)
- sym_map_comps map_cong0s;
- val dtor_corec_o_map_thms = mk_xtor_un_fold_o_map_thms Greatest_FP true m
- dtor_corec_unique_thm folded_dtor_map_o_thms (map (mk_pointfree lthy) dtor_corec_thms)
- sym_map_comps map_cong0s;
-
val passiveABs = map2 (curry HOLogic.mk_prodT) passiveAs passiveBs;
val zip_ranTs = passiveABs @ prodTsTs';
val allJphis = Jphis @ activeJphis;
@@ -2773,19 +2574,17 @@
val all_fsts = fstABs @ fstsTsTs';
val map_all_fsts = map2 (fn Ds => fn bnf =>
Term.list_comb (mk_map_of_bnf Ds zip_ranTs (passiveAs @ Ts) bnf, all_fsts)) Dss bnfs;
- val Jmap_fsts = map2 (fn bnf => fn T => if m = 0 then HOLogic.id_const T
- else Term.list_comb (mk_map_of_bnf deads passiveABs passiveAs bnf, fstABs)) Jbnfs Ts;
+ val Jmap_fsts = map2 (fn map => fn T => if m = 0 then HOLogic.id_const T
+ else Term.list_comb (map, fstABs)) (mk_Jmaps passiveABs passiveAs) Ts;
val sndABs = map snd_const passiveABs;
val all_snds = sndABs @ sndsTsTs';
val map_all_snds = map2 (fn Ds => fn bnf =>
Term.list_comb (mk_map_of_bnf Ds zip_ranTs (passiveBs @ Ts') bnf, all_snds)) Dss bnfs;
- val Jmap_snds = map2 (fn bnf => fn T => if m = 0 then HOLogic.id_const T
- else Term.list_comb (mk_map_of_bnf deads passiveABs passiveBs bnf, sndABs)) Jbnfs Ts;
+ val Jmap_snds = map2 (fn map => fn T => if m = 0 then HOLogic.id_const T
+ else Term.list_comb (map, sndABs)) (mk_Jmaps passiveABs passiveBs) Ts;
val zip_unfolds = map (mk_unfold zip_zTs (map HOLogic.mk_split zips)) ks;
- val zip_setss = map (mk_sets_of_bnf (replicate m deads) (replicate m passiveABs)) Jbnfs
- |> transpose;
- val in_Jrels = map in_rel_of_bnf Jbnfs;
+ val zip_setss = mk_Jsetss passiveABs |> transpose;
val Jrel_coinduct_tac =
let
@@ -2813,7 +2612,7 @@
(map6 (mk_helper_coind_concl false)
activeJphis Jzs Jz's_copy Jz's Jmap_snds zip_unfolds));
val helper_coind_tac = mk_rel_coinduct_coind_tac m dtor_map_coinduct_thm ks map_comps
- map_cong0s map_arg_cong_thms set_mapss dtor_unfold_thms folded_dtor_map_thms;
+ map_cong0s map_arg_cong_thms set_mapss dtor_unfold_thms dtor_Jmap_thms;
fun mk_helper_coind_thms vars concl =
Goal.prove_sorry lthy [] []
(fold_rev Logic.all (Jphis @ activeJphis @ vars @ zips)
@@ -2845,22 +2644,111 @@
(mk_rel_coinduct_ind_tac m ks dtor_unfold_thms set_mapss j set_induct)
|> Thm.close_derivation
|> split_conj_thm)
- mk_helper_ind_concls ls dtor_set_induct_thms
+ mk_helper_ind_concls ls dtor_Jset_induct_thms
|> transpose;
in
mk_rel_coinduct_tac in_rels in_Jrels
helper_ind_thmss helper_coind1_thms helper_coind2_thms
end;
-
- val Jrels = if m = 0 then map HOLogic.eq_const Ts
- else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs;
+
val Jrel_coinduct_thm =
mk_rel_xtor_co_induct_thm Greatest_FP rels activeJphis Jrels Jphis Jzs Jz's dtors dtor's
Jrel_coinduct_tac lthy;
+ val le_Jrel_OO_thm =
+ let
+ fun mk_le_Jrel_OO Jrelpsi1 Jrelpsi2 Jrelpsi12 =
+ mk_leq (mk_rel_compp (Jrelpsi1, Jrelpsi2)) Jrelpsi12;
+ val goals = map3 mk_le_Jrel_OO Jrelpsi1s Jrelpsi2s Jrelpsi12s;
+
+ val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals);
+ in
+ singleton (Proof_Context.export names_lthy lthy)
+ (Goal.prove_sorry lthy [] [] goal
+ (K (mk_le_rel_OO_tac Jrel_coinduct_thm dtor_Jrel_thms rel_OOs)))
+ |> Thm.close_derivation
+ end;
+
+ val timer = time (timer "helpers for BNF properties");
+
+ val map_id0_tacs =
+ map2 (K oo mk_map_id0_tac Jmap_thms) dtor_unfold_unique_thms unfold_dtor_thms;
+ val map_comp0_tacs = map (fn thm => K (rtac (thm RS sym) 1)) Jmap_comp0_thms;
+ val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
+ val set_nat_tacss =
+ map2 (map2 (fn def => fn col => fn {context = ctxt, prems = _} =>
+ unfold_thms_tac ctxt Jset_defs THEN mk_set_map0_tac def col))
+ hset_defss (transpose col_natural_thmss);
+
+ val Jbd_card_orders = map (fn def => fold_thms lthy [def] sbd_card_order) Jbd_defs;
+ val Jbd_Cinfinites = map (fn def => fold_thms lthy [def] sbd_Cinfinite) Jbd_defs;
+
+ val bd_co_tacs = map (fn thm => K (rtac thm 1)) Jbd_card_orders;
+ val bd_cinf_tacs = map (fn thm => K (rtac (thm RS conjunct1) 1)) Jbd_Cinfinites;
+
+ val set_bd_tacss =
+ map3 (fn Cinf => map2 (fn def => fn col => fn {context = ctxt, prems = _} =>
+ unfold_thms_tac ctxt Jset_defs THEN mk_set_bd_tac Cinf def col))
+ Jbd_Cinfinites hset_defss (transpose col_bd_thmss);
+
+ val le_rel_OO_tacs = map (fn i => K (rtac (le_Jrel_OO_thm RS mk_conjunctN n i) 1)) ks;
+
+ val rel_OO_Grp_tacs = map (fn def => K (rtac def 1)) Jrel_unabs_defs;
+
+ val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_nat_tacss
+ bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs;
+
+ fun wit_tac thms {context = ctxt, prems = _} = unfold_thms_tac ctxt (flat Jwit_defss) THEN
+ mk_wit_tac n dtor_ctor_thms (flat dtor_Jset_thmss) (maps wit_thms_of_bnf bnfs) thms ctxt;
+
+ val (Jbnfs, lthy) =
+ fold_map6 (fn tacs => fn map_b => fn rel_b => fn set_bs => fn Jwit_thms => fn consts =>
+ fn lthy =>
+ bnf_def Do_Inline (user_policy Note_Some) I tacs (wit_tac Jwit_thms) (SOME deads)
+ map_b rel_b set_bs consts lthy
+ |> register_bnf (Local_Theory.full_name lthy b))
+ tacss map_bs rel_bs set_bss Jwit_thmss
+ ((((((bs ~~ Ts) ~~ Jmaps) ~~ Jsetss_by_bnf) ~~ Jbds) ~~ Jwitss) ~~ map SOME Jrels)
+ lthy;
+
+ val timer = time (timer "registered new codatatypes as BNFs");
+
+ val ls' = if m = 1 then [0] else ls;
+
+ val Jbnf_common_notes =
+ [(dtor_map_uniqueN, [dtor_Jmap_unique_thm])] @
+ map2 (fn i => fn thm => (mk_dtor_set_inductN i, [thm])) ls' dtor_Jset_induct_thms
+ |> map (fn (thmN, thms) =>
+ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
+
+ val Jbnf_notes =
+ [(dtor_mapN, map single dtor_Jmap_thms),
+ (dtor_relN, map single dtor_Jrel_thms),
+ (dtor_set_inclN, dtor_Jset_incl_thmss),
+ (dtor_set_set_inclN, map flat dtor_set_Jset_incl_thmsss)] @
+ map2 (fn i => fn thms => (mk_dtor_setN i, map single thms)) ls' dtor_Jset_thmss
+ |> maps (fn (thmN, thmss) =>
+ map2 (fn b => fn thms =>
+ ((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
+ bs thmss)
+ in
+ (timer, Jbnfs, (Jmap_thms, dtor_Jmap_thms), dtor_Jset_thmss',
+ dtor_Jrel_thms, Jrel_coinduct_thm, Jbnf_common_notes @ Jbnf_notes, lthy)
+ end;
+
+ val dtor_unfold_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP false m
+ dtor_unfold_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_unfold_thms)
+ sym_map_comps map_cong0s;
+ val dtor_corec_o_Jmap_thms = mk_xtor_un_fold_o_map_thms Greatest_FP true m
+ dtor_corec_unique_thm dtor_Jmap_o_thms (map (mk_pointfree lthy) dtor_corec_thms)
+ sym_map_comps map_cong0s;
+
val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
+
val dtor_unfold_transfer_thms =
- mk_un_fold_transfer_thms Greatest_FP rels activephis Jrels Jphis
+ mk_un_fold_transfer_thms Greatest_FP rels activephis
+ (if m = 0 then map HOLogic.eq_const Ts
+ else map (mk_rel_of_bnf deads passiveAs passiveBs) Jbnfs) Jphis
(mk_unfolds passiveAs activeAs) (mk_unfolds passiveBs activeBs)
(mk_unfold_transfer_tac m Jrel_coinduct_thm (map map_transfer_of_bnf bnfs)
dtor_unfold_thms)
@@ -2887,8 +2775,8 @@
(dtor_unfoldN, dtor_unfold_thms),
(dtor_unfold_uniqueN, dtor_unfold_unique_thms),
(dtor_corec_uniqueN, dtor_corec_unique_thms),
- (dtor_unfold_o_mapN, dtor_unfold_o_map_thms),
- (dtor_corec_o_mapN, dtor_corec_o_map_thms)]
+ (dtor_unfold_o_mapN, dtor_unfold_o_Jmap_thms),
+ (dtor_corec_o_mapN, dtor_corec_o_Jmap_thms)]
|> map (apsnd (map single))
|> maps (fn (thmN, thmss) =>
map2 (fn b => fn thms =>
@@ -2905,10 +2793,10 @@
xtor_co_induct = dtor_coinduct_thm, dtor_ctors = dtor_ctor_thms,
ctor_dtors = ctor_dtor_thms,
ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
- xtor_map_thms = folded_dtor_map_thms, xtor_set_thmss = folded_dtor_set_thmss',
+ xtor_map_thms = dtor_Jmap_thms, xtor_set_thmss = dtor_Jset_thmss',
xtor_rel_thms = dtor_Jrel_thms,
xtor_co_iter_thmss = transpose [dtor_unfold_thms, dtor_corec_thms],
- xtor_co_iter_o_map_thmss = transpose [dtor_unfold_o_map_thms, dtor_corec_o_map_thms],
+ xtor_co_iter_o_map_thmss = transpose [dtor_unfold_o_Jmap_thms, dtor_corec_o_Jmap_thms],
rel_xtor_co_induct_thm = Jrel_coinduct_thm},
lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Jbnf_notes)) |> snd)
end;
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Wed Dec 18 11:03:40 2013 +0100
@@ -23,8 +23,6 @@
val mk_coalg_final_tac: int -> thm -> thm list -> thm list -> thm list list -> thm list list ->
tactic
val mk_coalg_set_tac: thm -> tactic
- val mk_coalg_thePull_tac: int -> thm -> thm list -> thm list list -> (int -> tactic) list ->
- {prems: 'a, context: Proof.context} -> tactic
val mk_coind_wit_tac: thm -> thm list -> thm list -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
val mk_col_bd_tac: int -> int -> cterm option list -> thm list -> thm list -> thm -> thm ->
@@ -37,7 +35,6 @@
val mk_corec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
tactic
val mk_dtor_map_coinduct_tac: int -> int list -> thm -> thm -> tactic
- val mk_dtor_set_tac: int -> thm -> thm -> thm list -> tactic
val mk_dtor_coinduct_tac: int -> thm -> thm -> thm list -> tactic
val mk_dtor_rel_tac: Proof.context -> thm list -> int -> thm -> thm -> thm -> thm -> thm list ->
thm -> thm -> thm list -> thm list -> thm list list -> tactic
@@ -50,12 +47,12 @@
val mk_incl_lsbis_tac: int -> int -> thm -> tactic
val mk_length_Lev'_tac: thm -> tactic
val mk_length_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
- val mk_map_comp0_tac: int -> int -> thm list -> thm list -> thm list -> thm -> tactic
+ val mk_map_comp0_tac: thm list -> thm list -> thm -> tactic
val mk_mcong_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list -> thm list ->
thm list list -> thm list list -> thm list list list -> tactic
val mk_map_id0_tac: thm list -> thm -> thm -> tactic
val mk_map_tac: int -> int -> ctyp option -> thm -> thm -> thm -> tactic
- val mk_dtor_map_unique_tac: thm -> thm list -> {prems: 'a, context: Proof.context} -> tactic
+ val mk_dtor_map_unique_tac: thm -> thm list -> Proof.context -> tactic
val mk_mor_Abs_tac: thm list -> thm list -> {prems: 'a, context: Proof.context} -> tactic
val mk_mor_Rep_tac: int -> thm list -> thm list -> thm list -> thm list list -> thm list ->
thm list -> {prems: 'a, context: Proof.context} -> tactic
@@ -73,19 +70,9 @@
val mk_mor_incl_tac: thm -> thm list -> tactic
val mk_mor_str_tac: 'a list -> thm -> tactic
val mk_mor_sum_case_tac: 'a list -> thm -> tactic
- val mk_mor_thePull_fst_tac: int -> thm -> thm list -> thm list -> (int -> tactic) list ->
- {prems: thm list, context: Proof.context} -> tactic
- val mk_mor_thePull_snd_tac: int -> thm -> thm list -> thm list -> (int -> tactic) list ->
- {prems: thm list, context: Proof.context} -> tactic
- val mk_mor_thePull_pick_tac: thm -> thm list -> thm list ->
- {prems: 'a, context: Proof.context} -> tactic
val mk_mor_unfold_tac: int -> thm -> thm list -> thm list -> thm list -> thm list -> thm list ->
thm list -> tactic
val mk_prefCl_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list -> tactic
- val mk_pickWP_assms_tac: thm list -> thm list -> thm -> (int -> tactic)
- val mk_pick_col_tac: int -> int -> cterm option list -> thm list -> thm list -> thm list ->
- thm list list -> thm list -> (int -> tactic) list -> {prems: 'a, context: Proof.context} ->
- tactic
val mk_raw_coind_tac: thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm -> thm list ->
thm list -> thm list -> thm -> thm list -> tactic
val mk_rel_coinduct_tac: thm list -> thm list -> thm list list -> thm list -> thm list ->
@@ -102,8 +89,8 @@
val mk_set_hset_incl_hset_tac: int -> thm list -> thm -> int -> tactic
val mk_set_image_Lev_tac: Proof.context -> cterm option list -> thm list -> thm list ->
thm list -> thm list -> thm list list -> thm list list -> tactic
- val mk_set_incl_hin_tac: thm list -> tactic
val mk_set_incl_hset_tac: thm -> thm -> tactic
+ val mk_set_ge_tac: int -> thm -> thm list -> tactic
val mk_set_le_tac: int -> thm -> thm list -> thm list list -> tactic
val mk_set_map0_tac: thm -> thm -> tactic
val mk_set_rv_Lev_tac: Proof.context -> int -> cterm option list -> thm list -> thm list ->
@@ -111,10 +98,8 @@
val mk_unfold_unique_mor_tac: thm list -> thm -> thm -> thm list -> tactic
val mk_unfold_transfer_tac: int -> thm -> thm list -> thm list ->
{prems: thm list, context: Proof.context} -> tactic
- val mk_unique_mor_tac: thm list -> thm -> tactic
- val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list ->
- {prems: 'a, context: Proof.context} -> tactic
- val mk_wpull_tac: int -> thm -> thm -> thm -> thm -> thm -> thm list -> thm list -> tactic
+ val mk_wit_tac: int -> thm list -> thm list -> thm list -> thm list -> Proof.context -> tactic
+ val mk_le_rel_OO_tac: thm -> thm list -> thm list -> tactic
end;
structure BNF_GFP_Tactics : BNF_GFP_TACTICS =
@@ -206,11 +191,6 @@
mk_UnIN n i] @
[etac @{thm UN_I}, atac]) 1;
-fun mk_set_incl_hin_tac incls =
- if null incls then rtac subset_UNIV 1
- else EVERY' [rtac subsetI, rtac CollectI,
- CONJ_WRAP' (fn incl => EVERY' [rtac subset_trans, etac incl, atac]) incls] 1;
-
fun mk_hset_rec_minimal_tac m cts rec_0s rec_Sucs {context = ctxt, prems = _} =
EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
REPEAT_DETERM o rtac allI,
@@ -940,12 +920,6 @@
(Rep_injects ~~ (equiv_LSBISs ~~ (incl_lsbiss ~~ lsbis_incls)))] 1
end;
-fun mk_unique_mor_tac raw_coinds bis =
- CONJ_WRAP' (fn raw_coind =>
- EVERY' [rtac impI, rtac (bis RS raw_coind RS set_mp RS @{thm IdD}), atac,
- etac conjunct1, atac, etac conjunct2, rtac @{thm image2_eqI}, rtac refl, rtac refl, atac])
- raw_coinds 1;
-
fun mk_unfold_unique_mor_tac raw_coinds bis mor unfold_defs =
CONJ_WRAP' (fn (raw_coind, unfold_def) =>
EVERY' [rtac ext, etac (bis RS raw_coind RS set_mp RS @{thm IdD}), rtac mor,
@@ -1023,8 +997,8 @@
EVERY' (map (fn thm => EVERY' [etac @{thm UN_E}, etac thm, atac]) set_hset_hsets)])
(1 upto n) set_hsets set_hset_hsetss)] 1;
-fun mk_dtor_set_tac n set_le set_incl_hset set_hset_incl_hsets =
- EVERY' [rtac equalityI, rtac set_le, rtac @{thm Un_least}, rtac set_incl_hset,
+fun mk_set_ge_tac n set_incl_hset set_hset_incl_hsets =
+ EVERY' [rtac @{thm Un_least}, rtac set_incl_hset,
REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least},
EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1;
@@ -1032,20 +1006,15 @@
EVERY' [rtac (unfold_unique RS trans), EVERY' (map (rtac o mk_sym) maps),
rtac unfold_dtor] 1;
-fun mk_map_comp0_tac m n maps map_comp0s map_cong0s unfold_unique =
- EVERY' [rtac unfold_unique,
- EVERY' (map3 (fn map_thm => fn map_comp0 => fn map_cong0 =>
+fun mk_map_comp0_tac maps map_comp0s map_unique =
+ EVERY' [rtac map_unique,
+ EVERY' (map2 (fn map_thm => fn map_comp0 =>
EVERY' (map rtac
- ([@{thm o_assoc} RS trans,
- @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl] RS trans,
- @{thm o_assoc} RS trans RS sym,
+ [@{thm o_assoc} RS trans,
@{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_thm, refl] RS trans,
@{thm o_assoc} RS sym RS trans, map_thm RS arg_cong RS trans, @{thm o_assoc} RS trans,
- @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl] RS trans,
- ext, o_apply RS trans, o_apply RS trans RS sym, map_cong0] @
- replicate m (@{thm id_o} RS fun_cong) @
- replicate n (@{thm o_id} RS fun_cong))))
- maps map_comp0s map_cong0s)] 1;
+ @{thm arg_cong2[of _ _ _ _ "op o"]} OF [map_comp0 RS sym, refl]]))
+ maps map_comp0s)] 1;
fun mk_mcong_tac ctxt m coinduct_tac map_comps dtor_maps map_cong0s set_map0ss set_hsetss
set_hset_hsetsss =
@@ -1082,7 +1051,7 @@
rtac conjI, rtac refl, rtac refl]) ks]) 1
end
-fun mk_dtor_map_unique_tac unfold_unique sym_map_comps {context = ctxt, prems = _} =
+fun mk_dtor_map_unique_tac unfold_unique sym_map_comps ctxt =
rtac unfold_unique 1 THEN
unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc id_o o_id}) THEN
ALLGOALS (etac sym);
@@ -1135,128 +1104,16 @@
@{thm UNION_Cinfinite_bound}, ordIso_ordLeq_trans, @{thm card_of_nat},
@{thm natLeq_ordLeq_cinfinite}, sbd_Cinfinite, ballI, col_bd, sbd_Cinfinite]) 1;
-fun mk_pickWP_assms_tac set_incl_hsets set_incl_hins map_eq =
- let
- val m = length set_incl_hsets;
- in
- EVERY' [REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
- EVERY' (map (fn thm => rtac conjI THEN' etac (thm RS @{thm subset_trans})) set_incl_hsets),
- CONJ_WRAP' (fn thm => rtac thm THEN' REPEAT_DETERM_N m o atac) set_incl_hins,
- REPEAT_DETERM o eresolve_tac [CollectE, conjE], rtac CollectI,
- EVERY' (map (fn thm => rtac conjI THEN' etac (thm RS @{thm subset_trans})) set_incl_hsets),
- CONJ_WRAP' (fn thm => rtac thm THEN' REPEAT_DETERM_N m o atac) set_incl_hins,
- REPEAT_DETERM o eresolve_tac [CollectE, conjE], etac map_eq]
- end;
-
-fun mk_coalg_thePull_tac m coalg_def map_wpulls set_map0ss pickWP_assms_tacs
- {context = ctxt, prems = _} =
- unfold_thms_tac ctxt [coalg_def] THEN
- CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, set_map0s)) =>
- EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
- REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
- hyp_subst_tac ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
- EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
- pickWP_assms_tac,
- SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}), rtac impI,
- REPEAT_DETERM o eresolve_tac [CollectE, conjE],
- rtac CollectI,
- REPEAT_DETERM_N m o (rtac conjI THEN' rtac subset_UNIV),
- CONJ_WRAP' (fn set_map0 =>
- EVERY' [rtac ord_eq_le_trans, rtac trans, rtac set_map0,
- rtac trans_fun_cong_image_id_id_apply, atac])
- (drop m set_map0s)])
- (map_wpulls ~~ (pickWP_assms_tacs ~~ set_map0ss)) 1;
-
-fun mk_mor_thePull_nth_tac conv pick m mor_def map_wpulls map_comp0s pickWP_assms_tacs
- {context = ctxt, prems = _: thm list} =
- let
- val n = length map_comp0s;
- in
- unfold_thms_tac ctxt [mor_def] THEN
- EVERY' [rtac conjI,
- CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) (1 upto n),
- CONJ_WRAP' (fn (map_wpull, (pickWP_assms_tac, map_comp0)) =>
- EVERY' [rtac ballI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
- REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
- hyp_subst_tac ctxt,
- SELECT_GOAL (unfold_thms_tac ctxt @{thms o_apply prod.cases}),
- rtac (map_comp0 RS trans),
- SELECT_GOAL (unfold_thms_tac ctxt (conv :: @{thms o_id id_o})),
- rtac (map_wpull RS pick), REPEAT_DETERM_N m o atac,
- pickWP_assms_tac])
- (map_wpulls ~~ (pickWP_assms_tacs ~~ map_comp0s))] 1
- end;
-
-val mk_mor_thePull_fst_tac = mk_mor_thePull_nth_tac @{thm fst_conv} @{thm pickWP(2)};
-val mk_mor_thePull_snd_tac = mk_mor_thePull_nth_tac @{thm snd_conv} @{thm pickWP(3)};
+fun mk_le_rel_OO_tac coinduct rel_Jrels rel_OOs =
+ EVERY' (rtac coinduct :: map2 (fn rel_Jrel => fn rel_OO =>
+ let val Jrel_imp_rel = rel_Jrel RS iffD1;
+ in
+ EVERY' [rtac (rel_OO RS sym RS @{thm eq_refl} RS @{thm predicate2D}), etac @{thm relcomppE},
+ rtac @{thm relcomppI}, etac Jrel_imp_rel, etac Jrel_imp_rel]
+ end)
+ rel_Jrels rel_OOs) 1;
-fun mk_mor_thePull_pick_tac mor_def unfolds map_comp0s {context = ctxt, prems = _} =
- unfold_thms_tac ctxt [mor_def, @{thm thePull_def}] THEN rtac conjI 1 THEN
- CONJ_WRAP' (K (rtac ballI THEN' rtac UNIV_I)) unfolds 1 THEN
- CONJ_WRAP' (fn (unfold, map_comp0) =>
- EVERY' [rtac ballI, REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}, conjE],
- hyp_subst_tac ctxt,
- SELECT_GOAL (unfold_thms_tac ctxt (unfold :: map_comp0 :: @{thms comp_def id_def})),
- rtac refl])
- (unfolds ~~ map_comp0s) 1;
-
-fun mk_pick_col_tac m j cts rec_0s rec_Sucs unfolds set_map0ss map_wpulls pickWP_assms_tacs
- {context = ctxt, prems = _} =
- let
- val n = length rec_0s;
- val ks = n downto 1;
- in
- EVERY' [rtac (Drule.instantiate' [] cts nat_induct),
- REPEAT_DETERM o rtac allI,
- CONJ_WRAP' (fn thm => EVERY'
- [rtac impI, rtac ord_eq_le_trans, rtac thm, rtac @{thm empty_subsetI}]) rec_0s,
- REPEAT_DETERM o rtac allI,
- CONJ_WRAP' (fn (rec_Suc, ((unfold, set_map0s), (map_wpull, pickWP_assms_tac))) =>
- EVERY' [rtac impI, dtac @{thm set_mp[OF equalityD1[OF thePull_def]]},
- REPEAT_DETERM o eresolve_tac [CollectE, @{thm prod_caseE}],
- hyp_subst_tac ctxt, rtac rev_mp, rtac (map_wpull RS @{thm pickWP(1)}),
- EVERY' (map (etac o mk_conjunctN m) (1 upto m)),
- pickWP_assms_tac,
- rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
- rtac ord_eq_le_trans, rtac rec_Suc,
- rtac @{thm Un_least},
- SELECT_GOAL (unfold_thms_tac ctxt [unfold, nth set_map0s (j - 1),
- @{thm prod.cases}]),
- etac ord_eq_le_trans_trans_fun_cong_image_id_id_apply,
- CONJ_WRAP_GEN' (rtac (Thm.permute_prems 0 1 @{thm Un_least})) (fn (i, set_map0) =>
- EVERY' [rtac @{thm UN_least},
- SELECT_GOAL (unfold_thms_tac ctxt [unfold, set_map0, @{thm prod.cases}]),
- etac imageE, hyp_subst_tac ctxt, REPEAT_DETERM o etac allE,
- dtac (mk_conjunctN n i), etac mp, etac set_mp, atac])
- (ks ~~ rev (drop m set_map0s))])
- (rec_Sucs ~~ ((unfolds ~~ set_map0ss) ~~ (map_wpulls ~~ pickWP_assms_tacs)))] 1
- end;
-
-fun mk_wpull_tac m coalg_thePull mor_thePull_fst mor_thePull_snd mor_thePull_pick
- mor_unique pick_cols hset_defs =
- EVERY' [rtac (@{thm wpull_def} RS iffD2), REPEAT_DETERM o rtac allI, rtac impI,
- REPEAT_DETERM o etac conjE, rtac bexI, rtac conjI,
- rtac box_equals, rtac mor_unique,
- rtac coalg_thePull, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
- rtac mor_thePull_pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
- rtac mor_thePull_fst, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
- rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI,
- rtac @{thm prod_caseI}, etac conjI, etac conjI, atac, rtac o_apply, rtac @{thm fst_conv},
- rtac box_equals, rtac mor_unique,
- rtac coalg_thePull, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
- rtac mor_thePull_pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
- rtac mor_thePull_snd, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
- rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI,
- rtac @{thm prod_caseI}, etac conjI, etac conjI, atac, rtac o_apply, rtac @{thm snd_conv},
- rtac CollectI,
- CONJ_WRAP' (fn (pick, def) =>
- EVERY' [rtac (def RS ord_eq_le_trans), rtac @{thm UN_least},
- rtac pick, REPEAT_DETERM_N (m - 1) o etac conjI, atac,
- rtac @{thm set_mp[OF equalityD2[OF thePull_def]]}, rtac CollectI,
- rtac @{thm prod_caseI}, etac conjI, etac conjI, atac])
- (pick_cols ~~ hset_defs)] 1;
-
-fun mk_wit_tac n dtor_ctors dtor_set wit coind_wits {context = ctxt, prems = _} =
+fun mk_wit_tac n dtor_ctors dtor_set wit coind_wits ctxt =
ALLGOALS (TRY o (eresolve_tac coind_wits THEN' rtac refl)) THEN
REPEAT_DETERM (atac 1 ORELSE
EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac dtor_set,
--- a/src/HOL/BNF/Tools/bnf_gfp_util.ML Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_gfp_util.ML Wed Dec 18 11:03:40 2013 +0100
@@ -24,14 +24,12 @@
val mk_fromCard: term -> term -> term
val mk_list_rec: term -> term -> term
val mk_nat_rec: term -> term -> term
- val mk_pickWP: term -> term -> term -> term -> term -> term
val mk_prefCl: term -> term
val mk_prefixeq: term -> term -> term
val mk_proj: term -> term
val mk_quotient: term -> term -> term
val mk_shift: term -> term -> term
val mk_size: term -> term
- val mk_thePull: term -> term -> term -> term -> term
val mk_toCard: term -> term -> term
val mk_undefined: typ -> term
val mk_univ: term -> term
@@ -160,29 +158,6 @@
Const (@{const_name list_rec}, T --> consT --> HOLogic.listT U --> T) $ Nil $ Cons
end;
-fun mk_thePull B1 B2 f1 f2 =
- let
- val fT1 = fastype_of f1;
- val fT2 = fastype_of f2;
- val BT1 = domain_type fT1;
- val BT2 = domain_type fT2;
- in
- Const (@{const_name thePull}, HOLogic.mk_setT BT1 --> HOLogic.mk_setT BT2 --> fT1 --> fT2 -->
- mk_relT (BT1, BT2)) $ B1 $ B2 $ f1 $ f2
- end;
-
-fun mk_pickWP A f1 f2 b1 b2 =
- let
- val fT1 = fastype_of f1;
- val fT2 = fastype_of f2;
- val AT = domain_type fT1;
- val BT1 = range_type fT1;
- val BT2 = range_type fT2;
- in
- Const (@{const_name pickWP}, HOLogic.mk_setT AT --> fT1 --> fT2 --> BT1 --> BT2 --> AT) $
- A $ f1 $ f2 $ b1 $ b2
- end;
-
fun mk_InN_not_InM 1 _ = @{thm Inl_not_Inr}
| mk_InN_not_InM n m =
if n > m then mk_InN_not_InM m n RS @{thm not_sym}
--- a/src/HOL/BNF/Tools/bnf_lfp.ML Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML Wed Dec 18 11:03:40 2013 +0100
@@ -55,15 +55,15 @@
val passives = map fst (subtract (op = o apsnd TFree) deads resBs);
(* tvars *)
- val ((((((passiveAs, activeAs), passiveBs), activeBs), activeCs), passiveXs), passiveYs) =
+ val (((((passiveAs, activeAs), passiveBs), activeBs), passiveCs), activeCs) =
names_lthy
|> variant_tfrees passives
||>> mk_TFrees n
||>> variant_tfrees passives
||>> mk_TFrees n
+ ||>> variant_tfrees passives
||>> mk_TFrees n
- ||>> mk_TFrees m
- ||> fst o mk_TFrees m;
+ |> fst;
val allAs = passiveAs @ activeAs;
val allBs' = passiveBs @ activeBs;
@@ -174,8 +174,9 @@
val map_cong0s = map map_cong0_of_bnf bnfs;
val map_id0s = map map_id0_of_bnf bnfs;
val map_ids = map map_id_of_bnf bnfs;
- val map_wpulls = map map_wpull_of_bnf bnfs;
val set_mapss = map set_map_of_bnf bnfs;
+ val rel_mono_strongs = map rel_mono_strong_of_bnf bnfs;
+ val rel_OOs = map rel_OO_of_bnf bnfs;
val timer = time (timer "Extracted terms & thms");
@@ -1402,16 +1403,20 @@
trans OF [ctor_inject, rel_eq_of_bnf bnf RS @{thm predicate2_eqD} RS sym];
val IphiTs = map2 mk_pred2T passiveAs passiveBs;
+ val Ipsi1Ts = map2 mk_pred2T passiveAs passiveCs;
+ val Ipsi2Ts = map2 mk_pred2T passiveCs passiveBs;
val activephiTs = map2 mk_pred2T activeAs activeBs;
val activeIphiTs = map2 mk_pred2T Ts Ts';
- val (((Iphis, activephis), activeIphis), names_lthy) = names_lthy
+ val (((((Iphis, Ipsi1s), Ipsi2s), activephis), activeIphis), names_lthy) = names_lthy
|> mk_Frees "R" IphiTs
+ ||>> mk_Frees "R" Ipsi1Ts
+ ||>> mk_Frees "Q" Ipsi2Ts
||>> mk_Frees "S" activephiTs
||>> mk_Frees "IR" activeIphiTs;
val rels = map2 (fn Ds => mk_rel_of_bnf Ds (passiveAs @ Ts) (passiveBs @ Ts')) Dss bnfs;
(*register new datatypes as BNFs*)
- val (timer, Ibnfs, (folded_ctor_map_o_thms, folded_ctor_map_thms), folded_ctor_set_thmss',
+ val (timer, Ibnfs, (ctor_Imap_o_thms, ctor_Imap_thms), ctor_Iset_thmss',
ctor_Irel_thms, Ibnf_notes, lthy) =
if m = 0 then
(timer, replicate n DEADID_bnf,
@@ -1419,31 +1424,13 @@
replicate n [], map2 mk_ctor_Irel_DEADID_thm ctor_inject_thms bnfs, [], lthy)
else let
val fTs = map2 (curry op -->) passiveAs passiveBs;
- val f1Ts = map2 (curry op -->) passiveAs passiveYs;
- val f2Ts = map2 (curry op -->) passiveBs passiveYs;
- val p1Ts = map2 (curry op -->) passiveXs passiveAs;
- val p2Ts = map2 (curry op -->) passiveXs passiveBs;
val uTs = map2 (curry op -->) Ts Ts';
- val B1Ts = map HOLogic.mk_setT passiveAs;
- val B2Ts = map HOLogic.mk_setT passiveBs;
- val AXTs = map HOLogic.mk_setT passiveXs;
- val XTs = mk_Ts passiveXs;
- val YTs = mk_Ts passiveYs;
- val (((((((((((((fs, fs'), fs_copy), us),
- B1s), B2s), AXs), (xs, xs')), f1s), f2s), p1s), p2s), (ys, ys')),
+ val (((((fs, fs'), fs_copy), us), (ys, ys')),
names_lthy) = names_lthy
|> mk_Frees' "f" fTs
||>> mk_Frees "f" fTs
||>> mk_Frees "u" uTs
- ||>> mk_Frees "B1" B1Ts
- ||>> mk_Frees "B2" B2Ts
- ||>> mk_Frees "A" AXTs
- ||>> mk_Frees' "x" XTs
- ||>> mk_Frees "f1" f1Ts
- ||>> mk_Frees "f2" f2Ts
- ||>> mk_Frees "p1" p1Ts
- ||>> mk_Frees "p2" p2Ts
||>> mk_Frees' "y" passiveAs;
val map_FTFT's = map2 (fn Ds =>
@@ -1456,51 +1443,9 @@
mk_fold Ts (map2 (mk_map_fold_arg fs Ts') ctors (mk_maps Ts'));
val pmapsABT' = mk_passive_maps passiveAs passiveBs;
val fs_maps = map (mk_map Ts fs Ts' ctor's pmapsABT') ks;
- val fs_copy_maps = map (mk_map Ts fs_copy Ts' ctor's pmapsABT') ks;
- val Yctors = mk_ctors passiveYs;
- val f1s_maps = map (mk_map Ts f1s YTs Yctors (mk_passive_maps passiveAs passiveYs)) ks;
- val f2s_maps = map (mk_map Ts' f2s YTs Yctors (mk_passive_maps passiveBs passiveYs)) ks;
- val p1s_maps = map (mk_map XTs p1s Ts ctors (mk_passive_maps passiveXs passiveAs)) ks;
- val p2s_maps = map (mk_map XTs p2s Ts' ctor's (mk_passive_maps passiveXs passiveBs)) ks;
-
- val (ctor_map_thms, ctor_map_o_thms) =
- let
- fun mk_goal fs_map map ctor ctor' = fold_rev Logic.all fs
- (mk_Trueprop_eq (HOLogic.mk_comp (fs_map, ctor),
- HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_maps))));
- val goals = map4 mk_goal fs_maps map_FTFT's ctors ctor's;
- val maps =
- map4 (fn goal => fn foldx => fn map_comp_id => fn map_cong0 =>
- Goal.prove_sorry lthy [] [] goal (K (mk_map_tac m n foldx map_comp_id map_cong0))
- |> Thm.close_derivation)
- goals ctor_fold_thms map_comp_id_thms map_cong0s;
- in
- `(map (fn thm => thm RS @{thm comp_eq_dest})) maps
- end;
-
- val (ctor_map_unique_thms, ctor_map_unique_thm) =
- let
- fun mk_prem u map ctor ctor' =
- mk_Trueprop_eq (HOLogic.mk_comp (u, ctor),
- HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ us)));
- val prems = map4 mk_prem us map_FTFT's ctors ctor's;
- val goal =
- HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map2 (curry HOLogic.mk_eq) us fs_maps));
- val unique = Goal.prove_sorry lthy [] []
- (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
- (mk_ctor_map_unique_tac ctor_fold_unique_thm sym_map_comps)
- |> Thm.close_derivation;
- in
- `split_conj_thm unique
- end;
-
- val timer = time (timer "map functions for the new datatypes");
val ls = 1 upto m;
val setsss = map (mk_setss o mk_set_Ts) passiveAs;
- val map_setss = map (fn T => map2 (fn Ds =>
- mk_map_of_bnf Ds (passiveAs @ Ts) (mk_set_Ts T)) Dss bnfs) passiveAs;
fun mk_col l T z z' sets =
let
@@ -1515,198 +1460,9 @@
val setss_by_range = map (fn cols => map (mk_fold Ts cols) ks) colss;
val setss_by_bnf = transpose setss_by_range;
- val ctor_set_thmss =
- let
- fun mk_goal sets ctor set col map =
- mk_Trueprop_eq (HOLogic.mk_comp (set, ctor),
- HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets)));
- val goalss =
- map3 (fn sets => map4 (mk_goal sets) ctors sets) setss_by_range colss map_setss;
- val setss = map (map2 (fn foldx => fn goal =>
- Goal.prove_sorry lthy [] [] goal (K (mk_set_tac foldx)) |> Thm.close_derivation)
- ctor_fold_thms) goalss;
-
- fun mk_simp_goal pas_set act_sets sets ctor z set =
- Logic.all z (mk_Trueprop_eq (set $ (ctor $ z),
- mk_union (pas_set $ z,
- Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets))));
- val simp_goalss =
- map2 (fn i => fn sets =>
- map4 (fn Fsets => mk_simp_goal (nth Fsets (i - 1)) (drop m Fsets) sets)
- FTs_setss ctors xFs sets)
- ls setss_by_range;
-
- val ctor_setss = map3 (fn i => map3 (fn set_nats => fn goal => fn set =>
- Goal.prove_sorry lthy [] [] goal
- (K (mk_ctor_set_tac set (nth set_nats (i - 1)) (drop m set_nats)))
- |> Thm.close_derivation)
- set_mapss) ls simp_goalss setss;
- in
- ctor_setss
- end;
-
- fun mk_set_thms ctor_set = (@{thm xt1(3)} OF [ctor_set, @{thm Un_upper1}]) ::
- map (fn i => (@{thm xt1(3)} OF [ctor_set, @{thm Un_upper2}]) RS
- (mk_Un_upper n i RS subset_trans) RSN
- (2, @{thm UN_upper} RS subset_trans))
- (1 upto n);
- val Fset_set_thmsss = transpose (map (map mk_set_thms) ctor_set_thmss);
-
- val timer = time (timer "set functions for the new datatypes");
-
- val cxs = map (SOME o certify lthy) Izs;
- val setss_by_bnf' =
- map (map (Term.subst_atomic_types (passiveAs ~~ passiveBs))) setss_by_bnf;
- val setss_by_range' = transpose setss_by_bnf';
-
- val set_map0_thmss =
- let
- fun mk_set_map0 f map z set set' =
- HOLogic.mk_eq (mk_image f $ (set $ z), set' $ (map $ z));
-
- fun mk_cphi f map z set set' = certify lthy
- (Term.absfree (dest_Free z) (mk_set_map0 f map z set set'));
-
- val csetss = map (map (certify lthy)) setss_by_range';
-
- val cphiss = map3 (fn f => fn sets => fn sets' =>
- (map4 (mk_cphi f) fs_maps Izs sets sets')) fs setss_by_range setss_by_range';
-
- val inducts = map (fn cphis =>
- Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss;
-
- val goals =
- map3 (fn f => fn sets => fn sets' =>
- HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map4 (mk_set_map0 f) fs_maps Izs sets sets')))
- fs setss_by_range setss_by_range';
-
- fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_mapss ctor_map_thms;
- val thms =
- map5 (fn goal => fn csets => fn ctor_sets => fn induct => fn i =>
- singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] goal (mk_tac induct csets ctor_sets i))
- |> Thm.close_derivation)
- goals csetss ctor_set_thmss inducts ls;
- in
- map split_conj_thm thms
- end;
-
- val set_bd_thmss =
- let
- fun mk_set_bd z set = mk_ordLeq (mk_card_of (set $ z)) sum_bd;
-
- fun mk_cphi z set = certify lthy (Term.absfree (dest_Free z) (mk_set_bd z set));
-
- val cphiss = map (map2 mk_cphi Izs) setss_by_range;
-
- val inducts = map (fn cphis =>
- Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss;
-
- val goals =
- map (fn sets =>
- HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map2 mk_set_bd Izs sets))) setss_by_range;
-
- fun mk_tac induct = mk_set_bd_tac m (rtac induct) sum_Cinfinite set_bd_sumss;
- val thms =
- map4 (fn goal => fn ctor_sets => fn induct => fn i =>
- singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] goal (mk_tac induct ctor_sets i))
- |> Thm.close_derivation)
- goals ctor_set_thmss inducts ls;
- in
- map split_conj_thm thms
- end;
-
- val map_cong0_thms =
- let
- fun mk_prem z set f g y y' =
- mk_Ball (set $ z) (Term.absfree y' (HOLogic.mk_eq (f $ y, g $ y)));
-
- fun mk_map_cong0 sets z fmap gmap =
- HOLogic.mk_imp
- (Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys'),
- HOLogic.mk_eq (fmap $ z, gmap $ z));
-
- fun mk_cphi sets z fmap gmap =
- certify lthy (Term.absfree (dest_Free z) (mk_map_cong0 sets z fmap gmap));
-
- val cphis = map4 mk_cphi setss_by_bnf Izs fs_maps fs_copy_maps;
-
- val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm;
-
- val goal =
- HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
- (map4 mk_map_cong0 setss_by_bnf Izs fs_maps fs_copy_maps));
-
- val thm = singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] goal
- (mk_mcong_tac (rtac induct) Fset_set_thmsss map_cong0s ctor_map_thms))
- |> Thm.close_derivation;
- in
- split_conj_thm thm
- end;
-
- val Xsetss = map (map (Term.subst_atomic_types (passiveAs ~~ passiveXs))) setss_by_bnf;
-
- val map_wpull_thms =
- let
- val cTs = map (SOME o certifyT lthy o TFree) induct2_params;
- val cxs = map (SOME o certify lthy) (splice Izs1 Izs2);
-
- fun mk_prem z1 z2 sets1 sets2 map1 map2 =
- HOLogic.mk_conj
- (HOLogic.mk_mem (z1, mk_in B1s sets1 (fastype_of z1)),
- HOLogic.mk_conj
- (HOLogic.mk_mem (z2, mk_in B2s sets2 (fastype_of z2)),
- HOLogic.mk_eq (map1 $ z1, map2 $ z2)));
-
- val prems = map6 mk_prem Izs1 Izs2 setss_by_bnf setss_by_bnf' f1s_maps f2s_maps;
-
- fun mk_concl z1 z2 sets map1 map2 T x x' =
- mk_Bex (mk_in AXs sets T) (Term.absfree x'
- (HOLogic.mk_conj (HOLogic.mk_eq (map1 $ x, z1), HOLogic.mk_eq (map2 $ x, z2))));
-
- val concls = map8 mk_concl Izs1 Izs2 Xsetss p1s_maps p2s_maps XTs xs xs';
-
- val goals = map2 (curry HOLogic.mk_imp) prems concls;
-
- fun mk_cphi z1 z2 goal = certify lthy (Term.absfree z1 (Term.absfree z2 goal));
-
- val cphis = map3 mk_cphi Izs1' Izs2' goals;
-
- val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct2_thm;
-
- val goal = Logic.list_implies (map HOLogic.mk_Trueprop
- (map8 mk_wpull AXs B1s B2s f1s f2s (replicate m NONE) p1s p2s),
- HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals));
-
- val thm = singleton (Proof_Context.export names_lthy lthy)
- (Goal.prove_sorry lthy [] [] goal
- (K (mk_lfp_map_wpull_tac lthy m (rtac induct) map_wpulls ctor_map_thms
- (transpose ctor_set_thmss) Fset_set_thmsss ctor_inject_thms)))
- |> Thm.close_derivation;
- in
- split_conj_thm thm
- end;
-
- val timer = time (timer "helpers for BNF properties");
-
- val map_id0_tacs = map (K o mk_map_id0_tac map_id0s) ctor_map_unique_thms;
- val map_comp0_tacs =
- map2 (K oo mk_map_comp0_tac map_comps ctor_map_thms) ctor_map_unique_thms ks;
- val map_cong0_tacs = map (mk_map_cong0_tac m) map_cong0_thms;
- val set_nat_tacss = map (map (K o mk_set_map0_tac)) (transpose set_map0_thmss);
- val bd_co_tacs = replicate n (K (mk_bd_card_order_tac bd_card_orders));
- val bd_cinf_tacs = replicate n (K (rtac (sum_Cinfinite RS conjunct1) 1));
- val set_bd_tacss = map (map (fn thm => K (rtac thm 1))) (transpose set_bd_thmss);
- val map_wpull_tacs = map (K o mk_wpull_tac) map_wpull_thms;
-
- val rel_OO_Grp_tacs = replicate n (K (rtac refl 1));
-
- val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_nat_tacss
- bd_co_tacs bd_cinf_tacs set_bd_tacss map_wpull_tacs rel_OO_Grp_tacs;
+ val set_bss =
+ map (flat o map2 (fn B => fn b =>
+ if member (op =) resDs (TFree B) then [] else [b]) resBs) set_bss0;
val ctor_witss =
let
@@ -1733,45 +1489,227 @@
ctors (0 upto n - 1) witss
end;
- fun wit_tac {context = ctxt, prems = _} =
- mk_wit_tac ctxt n (flat ctor_set_thmss) (maps wit_thms_of_bnf bnfs);
-
- val set_bss =
- map (flat o map2 (fn B => fn b =>
- if member (op =) resDs (TFree B) then [] else [b]) resBs) set_bss0;
-
- val (Ibnfs, lthy) =
- fold_map9 (fn tacs => fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets =>
- fn T => fn wits => fn lthy =>
- bnf_def Dont_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads)
+ val (Ibnf_consts, lthy) =
+ fold_map8 (fn b => fn map_b => fn rel_b => fn set_bs => fn mapx => fn sets => fn wits =>
+ fn T => fn lthy =>
+ define_bnf_consts Dont_Inline (user_policy Note_Some lthy) (SOME deads)
map_b rel_b set_bs
- ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sum_bd), wits), NONE)
- lthy
- |> register_bnf (Local_Theory.full_name lthy b))
- tacss bs map_bs rel_bs set_bss fs_maps setss_by_bnf Ts ctor_witss lthy;
+ ((((((b, T), fold_rev Term.absfree fs' mapx), sets), sum_bd), wits), NONE) lthy)
+ bs map_bs rel_bs set_bss fs_maps setss_by_bnf ctor_witss Ts lthy;
+
+ val (_, Iconsts, Iconst_defs, mk_Iconsts) = split_list4 Ibnf_consts;
+ val (_, Isetss, Ibds_Ds, Iwitss_Ds, _) = split_list5 Iconsts;
+ val (Imap_defs, Iset_defss, Ibd_defs, Iwit_defss, Irel_defs) = split_list5 Iconst_defs;
+ val (mk_Imaps_Ds, mk_It_Ds, _, mk_Irels_Ds, _) = split_list5 mk_Iconsts;
+
+ val Irel_unabs_defs = map (fn def => mk_unabs_def m (def RS meta_eq_to_obj_eq)) Irel_defs;
+ val Iset_defs = flat Iset_defss;
+
+ fun mk_Imaps As Bs = map (fn mk => mk deads As Bs) mk_Imaps_Ds;
+ fun mk_Isetss As = map2 (fn mk => fn Isets => map (mk deads As) Isets) mk_It_Ds Isetss;
+ val Ibds = map2 (fn mk => mk deads passiveAs) mk_It_Ds Ibds_Ds;
+ val Iwitss =
+ map2 (fn mk => fn Iwits => map (mk deads passiveAs o snd) Iwits) mk_It_Ds Iwitss_Ds;
+ fun mk_Irels As Bs = map (fn mk => mk deads As Bs) mk_Irels_Ds;
+
+ val Imaps = mk_Imaps passiveAs passiveBs;
+ val fs_Imaps = map (fn m => Term.list_comb (m, fs)) Imaps;
+ val fs_copy_Imaps = map (fn m => Term.list_comb (m, fs_copy)) Imaps;
+ val (Isetss_by_range, Isetss_by_bnf) = `transpose (mk_Isetss passiveAs);
+
+ val map_setss = map (fn T => map2 (fn Ds =>
+ mk_map_of_bnf Ds (passiveAs @ Ts) (mk_set_Ts T)) Dss bnfs) passiveAs;
+
+ val timer = time (timer "bnf constants for the new datatypes");
+
+ val (ctor_Imap_thms, ctor_Imap_o_thms) =
+ let
+ fun mk_goal fs_map map ctor ctor' = fold_rev Logic.all fs
+ (mk_Trueprop_eq (HOLogic.mk_comp (fs_map, ctor),
+ HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ fs_Imaps))));
+ val goals = map4 mk_goal fs_Imaps map_FTFT's ctors ctor's;
+ val maps =
+ map4 (fn goal => fn foldx => fn map_comp_id => fn map_cong0 =>
+ Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN
+ mk_map_tac m n foldx map_comp_id map_cong0)
+ |> Thm.close_derivation)
+ goals ctor_fold_thms map_comp_id_thms map_cong0s;
+ in
+ `(map (fn thm => thm RS @{thm comp_eq_dest})) maps
+ end;
- val fold_maps = fold_thms lthy (map (fn bnf =>
- mk_unabs_def m (map_def_of_bnf bnf RS meta_eq_to_obj_eq)) Ibnfs);
+ val (ctor_Imap_unique_thms, ctor_Imap_unique_thm) =
+ let
+ fun mk_prem u map ctor ctor' =
+ mk_Trueprop_eq (HOLogic.mk_comp (u, ctor),
+ HOLogic.mk_comp (ctor', Term.list_comb (map, fs @ us)));
+ val prems = map4 mk_prem us map_FTFT's ctors ctor's;
+ val goal =
+ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
+ (map2 (curry HOLogic.mk_eq) us fs_Imaps));
+ val unique = Goal.prove_sorry lthy [] []
+ (fold_rev Logic.all (us @ fs) (Logic.list_implies (prems, goal)))
+ (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Imap_defs THEN
+ mk_ctor_map_unique_tac ctor_fold_unique_thm sym_map_comps ctxt)
+ |> Thm.close_derivation;
+ in
+ `split_conj_thm unique
+ end;
+
+ val timer = time (timer "map functions for the new datatypes");
+
+ val ctor_Iset_thmss =
+ let
+ fun mk_goal sets ctor set col map =
+ mk_Trueprop_eq (HOLogic.mk_comp (set, ctor),
+ HOLogic.mk_comp (col, Term.list_comb (map, passive_ids @ sets)));
+ val goalss =
+ map3 (fn sets => map4 (mk_goal sets) ctors sets) Isetss_by_range colss map_setss;
+ val setss = map (map2 (fn foldx => fn goal =>
+ Goal.prove_sorry lthy [] [] goal (fn {context = ctxt, prems = _} =>
+ unfold_thms_tac ctxt Iset_defs THEN mk_set_tac foldx)
+ |> Thm.close_derivation)
+ ctor_fold_thms) goalss;
+
+ fun mk_simp_goal pas_set act_sets sets ctor z set =
+ Logic.all z (mk_Trueprop_eq (set $ (ctor $ z),
+ mk_union (pas_set $ z,
+ Library.foldl1 mk_union (map2 (fn X => mk_UNION (X $ z)) act_sets sets))));
+ val simp_goalss =
+ map2 (fn i => fn sets =>
+ map4 (fn Fsets => mk_simp_goal (nth Fsets (i - 1)) (drop m Fsets) sets)
+ FTs_setss ctors xFs sets)
+ ls Isetss_by_range;
+
+ val ctor_setss = map3 (fn i => map3 (fn set_nats => fn goal => fn set =>
+ Goal.prove_sorry lthy [] [] goal
+ (K (mk_ctor_set_tac set (nth set_nats (i - 1)) (drop m set_nats)))
+ |> Thm.close_derivation)
+ set_mapss) ls simp_goalss setss;
+ in
+ ctor_setss
+ end;
- val fold_sets = fold_thms lthy (maps (fn bnf =>
- map (fn thm => thm RS meta_eq_to_obj_eq) (set_defs_of_bnf bnf)) Ibnfs);
+ fun mk_set_thms ctor_set = (@{thm xt1(3)} OF [ctor_set, @{thm Un_upper1}]) ::
+ map (fn i => (@{thm xt1(3)} OF [ctor_set, @{thm Un_upper2}]) RS
+ (mk_Un_upper n i RS subset_trans) RSN
+ (2, @{thm UN_upper} RS subset_trans))
+ (1 upto n);
+ val set_Iset_thmsss = transpose (map (map mk_set_thms) ctor_Iset_thmss);
+
+ val timer = time (timer "set functions for the new datatypes");
+
+ val cxs = map (SOME o certify lthy) Izs;
+ val Isetss_by_range' =
+ map (map (Term.subst_atomic_types (passiveAs ~~ passiveBs))) Isetss_by_range;
+
+ val Iset_Imap0_thmss =
+ let
+ fun mk_set_map0 f map z set set' =
+ HOLogic.mk_eq (mk_image f $ (set $ z), set' $ (map $ z));
+
+ fun mk_cphi f map z set set' = certify lthy
+ (Term.absfree (dest_Free z) (mk_set_map0 f map z set set'));
+
+ val csetss = map (map (certify lthy)) Isetss_by_range';
+
+ val cphiss = map3 (fn f => fn sets => fn sets' =>
+ (map4 (mk_cphi f) fs_Imaps Izs sets sets')) fs Isetss_by_range Isetss_by_range';
- val timer = time (timer "registered new datatypes as BNFs");
+ val inducts = map (fn cphis =>
+ Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss;
+
+ val goals =
+ map3 (fn f => fn sets => fn sets' =>
+ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
+ (map4 (mk_set_map0 f) fs_Imaps Izs sets sets')))
+ fs Isetss_by_range Isetss_by_range';
+
+ fun mk_tac induct = mk_set_nat_tac m (rtac induct) set_mapss ctor_Imap_thms;
+ val thms =
+ map5 (fn goal => fn csets => fn ctor_sets => fn induct => fn i =>
+ singleton (Proof_Context.export names_lthy lthy)
+ (Goal.prove_sorry lthy [] [] goal (mk_tac induct csets ctor_sets i))
+ |> Thm.close_derivation)
+ goals csetss ctor_Iset_thmss inducts ls;
+ in
+ map split_conj_thm thms
+ end;
+
+ val Iset_bd_thmss =
+ let
+ fun mk_set_bd z bd set = mk_ordLeq (mk_card_of (set $ z)) bd;
+
+ fun mk_cphi z set = certify lthy (Term.absfree (dest_Free z) (mk_set_bd z sum_bd set));
- val Irels = map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
+ val cphiss = map (map2 mk_cphi Izs) Isetss_by_range;
+
+ val inducts = map (fn cphis =>
+ Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm) cphiss;
+
+ val goals =
+ map (fn sets =>
+ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
+ (map3 mk_set_bd Izs Ibds sets))) Isetss_by_range;
+
+ fun mk_tac induct = mk_set_bd_tac m (rtac induct) sum_Cinfinite set_bd_sumss;
+ val thms =
+ map4 (fn goal => fn ctor_sets => fn induct => fn i =>
+ singleton (Proof_Context.export names_lthy lthy)
+ (Goal.prove_sorry lthy [] [] goal
+ (fn {context = ctxt, prems = _} => unfold_thms_tac ctxt Ibd_defs THEN
+ mk_tac induct ctor_sets i ctxt))
+ |> Thm.close_derivation)
+ goals ctor_Iset_thmss inducts ls;
+ in
+ map split_conj_thm thms
+ end;
- val Irelphis = map (fn Irel => Term.list_comb (Irel, Iphis)) Irels;
- val relphis = map (fn rel => Term.list_comb (rel, Iphis @ Irelphis)) rels;
+ val Imap_cong0_thms =
+ let
+ fun mk_prem z set f g y y' =
+ mk_Ball (set $ z) (Term.absfree y' (HOLogic.mk_eq (f $ y, g $ y)));
+
+ fun mk_map_cong0 sets z fmap gmap =
+ HOLogic.mk_imp
+ (Library.foldr1 HOLogic.mk_conj (map5 (mk_prem z) sets fs fs_copy ys ys'),
+ HOLogic.mk_eq (fmap $ z, gmap $ z));
+
+ fun mk_cphi sets z fmap gmap =
+ certify lthy (Term.absfree (dest_Free z) (mk_map_cong0 sets z fmap gmap));
+
+ val cphis = map4 mk_cphi Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps;
+
+ val induct = Drule.instantiate' cTs (map SOME cphis @ cxs) ctor_induct_thm;
+
+ val goal =
+ HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj
+ (map4 mk_map_cong0 Isetss_by_bnf Izs fs_Imaps fs_copy_Imaps));
+
+ val thm = singleton (Proof_Context.export names_lthy lthy)
+ (Goal.prove_sorry lthy [] [] goal
+ (mk_mcong_tac (rtac induct) set_Iset_thmsss map_cong0s ctor_Imap_thms))
+ |> Thm.close_derivation;
+ in
+ split_conj_thm thm
+ end;
val in_rels = map in_rel_of_bnf bnfs;
- val in_Irels = map in_rel_of_bnf Ibnfs;
+ val in_Irels = map (fn def => trans OF [def, @{thm OO_Grp_alt}] RS @{thm predicate2_eqD})
+ Irel_unabs_defs;
+
+ val ctor_Iset_incl_thmss = map (map hd) set_Iset_thmsss;
+ val ctor_set_Iset_incl_thmsss = map (transpose o map tl) set_Iset_thmsss;
+ val ctor_Iset_thmss' = transpose ctor_Iset_thmss;
- val ctor_set_incl_thmss = map (map (fold_sets o hd)) Fset_set_thmsss;
- val ctor_set_set_incl_thmsss = map (transpose o map (map fold_sets o tl)) Fset_set_thmsss;
- val folded_ctor_map_thms = map fold_maps ctor_map_thms;
- val folded_ctor_map_o_thms = map fold_maps ctor_map_o_thms;
- val folded_ctor_set_thmss = map (map fold_sets) ctor_set_thmss;
- val folded_ctor_set_thmss' = transpose folded_ctor_set_thmss;
+ val Irels = mk_Irels passiveAs passiveBs;
+ val Irelphis = map (fn rel => Term.list_comb (rel, Iphis)) Irels;
+ val relphis = map (fn rel => Term.list_comb (rel, Iphis @ Irelphis)) rels;
+ val Irelpsi1s = map (fn rel => Term.list_comb (rel, Ipsi1s)) (mk_Irels passiveAs passiveCs);
+ val Irelpsi2s = map (fn rel => Term.list_comb (rel, Ipsi2s)) (mk_Irels passiveCs passiveBs);
+ val Irelpsi12s = map (fn rel =>
+ Term.list_comb (rel, map2 (curry mk_rel_compp) Ipsi1s Ipsi2s)) Irels;
val ctor_Irel_thms =
let
@@ -1786,46 +1724,99 @@
(K (mk_ctor_rel_tac lthy in_Irels i in_rel map_comp0 map_cong0 ctor_map ctor_sets
ctor_inject ctor_dtor set_map0s ctor_set_incls ctor_set_set_inclss))
|> Thm.close_derivation)
- ks goals in_rels map_comps map_cong0s folded_ctor_map_thms folded_ctor_set_thmss'
- ctor_inject_thms ctor_dtor_thms set_mapss ctor_set_incl_thmss
- ctor_set_set_incl_thmsss
+ ks goals in_rels map_comps map_cong0s ctor_Imap_thms ctor_Iset_thmss'
+ ctor_inject_thms ctor_dtor_thms set_mapss ctor_Iset_incl_thmss
+ ctor_set_Iset_incl_thmsss
+ end;
+
+ val le_Irel_OO_thm =
+ let
+ fun mk_le_Irel_OO Irelpsi1 Irelpsi2 Irelpsi12 Iz1 Iz2 =
+ HOLogic.mk_imp (mk_rel_compp (Irelpsi1, Irelpsi2) $ Iz1 $ Iz2,
+ Irelpsi12 $ Iz1 $ Iz2);
+ val goals = map5 mk_le_Irel_OO Irelpsi1s Irelpsi2s Irelpsi12s Izs1 Izs2;
+
+ val cTs = map (SOME o certifyT lthy o TFree) induct2_params;
+ val cxs = map (SOME o certify lthy) (splice Izs1 Izs2);
+ fun mk_cphi z1 z2 goal = SOME (certify lthy (Term.absfree z1 (Term.absfree z2 goal)));
+ val cphis = map3 mk_cphi Izs1' Izs2' goals;
+ val induct = Drule.instantiate' cTs (cphis @ cxs) ctor_induct2_thm;
+
+ val goal = HOLogic.mk_Trueprop (Library.foldr1 HOLogic.mk_conj goals);
+ in
+ singleton (Proof_Context.export names_lthy lthy)
+ (Goal.prove_sorry lthy [] [] goal
+ (mk_le_rel_OO_tac m induct ctor_nchotomy_thms ctor_Irel_thms rel_mono_strongs
+ rel_OOs))
+ |> Thm.close_derivation
end;
- val timer = time (timer "additional properties");
+ val timer = time (timer "helpers for BNF properties");
+
+ val map_id0_tacs = map (K o mk_map_id0_tac map_id0s) ctor_Imap_unique_thms;
+ val map_comp0_tacs =
+ map2 (K oo mk_map_comp0_tac map_comps ctor_Imap_thms) ctor_Imap_unique_thms ks;
+ val map_cong0_tacs = map (mk_map_cong0_tac m) Imap_cong0_thms;
+ val set_map0_tacss = map (map (K o mk_set_map0_tac)) (transpose Iset_Imap0_thmss);
+ val bd_co_tacs = replicate n (fn {context = ctxt, prems = _} =>
+ unfold_thms_tac ctxt Ibd_defs THEN mk_bd_card_order_tac bd_card_orders);
+ val bd_cinf_tacs = replicate n (fn {context = ctxt, prems = _} =>
+ unfold_thms_tac ctxt Ibd_defs THEN rtac (sum_Cinfinite RS conjunct1) 1);
+ val set_bd_tacss = map (map (fn thm => K (rtac thm 1))) (transpose Iset_bd_thmss);
+ val le_rel_OO_tacs = map (fn i =>
+ K ((rtac @{thm predicate2I} THEN' etac (le_Irel_OO_thm RS mk_conjunctN n i RS mp)) 1)) ks;
+
+ val rel_OO_Grp_tacs = map (fn def => K (rtac def 1)) Irel_unabs_defs;
+
+ val tacss = map9 zip_axioms map_id0_tacs map_comp0_tacs map_cong0_tacs set_map0_tacss
+ bd_co_tacs bd_cinf_tacs set_bd_tacss le_rel_OO_tacs rel_OO_Grp_tacs;
+
+ fun wit_tac {context = ctxt, prems = _} = unfold_thms_tac ctxt (flat Iwit_defss) THEN
+ mk_wit_tac ctxt n (flat ctor_Iset_thmss) (maps wit_thms_of_bnf bnfs);
+
+ val (Ibnfs, lthy) =
+ fold_map5 (fn tacs => fn map_b => fn rel_b => fn set_bs => fn consts => fn lthy =>
+ bnf_def Do_Inline (user_policy Note_Some) I tacs wit_tac (SOME deads)
+ map_b rel_b set_bs consts lthy
+ |> register_bnf (Local_Theory.full_name lthy b))
+ tacss map_bs rel_bs set_bss
+ ((((((bs ~~ Ts) ~~ Imaps) ~~ Isetss_by_bnf) ~~ Ibds) ~~ Iwitss) ~~ map SOME Irels)
+ lthy;
+
+ val timer = time (timer "registered new datatypes as BNFs");
val ls' = if m = 1 then [0] else ls
val Ibnf_common_notes =
- [(ctor_map_uniqueN, [fold_maps ctor_map_unique_thm])]
+ [(ctor_map_uniqueN, [ctor_Imap_unique_thm])]
|> map (fn (thmN, thms) =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]));
val Ibnf_notes =
- [(ctor_mapN, map single folded_ctor_map_thms),
+ [(ctor_mapN, map single ctor_Imap_thms),
(ctor_relN, map single ctor_Irel_thms),
- (ctor_set_inclN, ctor_set_incl_thmss),
- (ctor_set_set_inclN, map flat ctor_set_set_incl_thmsss)] @
- map2 (fn i => fn thms => (mk_ctor_setN i, map single thms)) ls' folded_ctor_set_thmss
+ (ctor_set_inclN, ctor_Iset_incl_thmss),
+ (ctor_set_set_inclN, map flat ctor_set_Iset_incl_thmsss)] @
+ map2 (fn i => fn thms => (mk_ctor_setN i, map single thms)) ls' ctor_Iset_thmss
|> maps (fn (thmN, thmss) =>
map2 (fn b => fn thms =>
((Binding.qualify true (Binding.name_of b) (Binding.name thmN), []), [(thms, [])]))
bs thmss)
in
- (timer, Ibnfs, (folded_ctor_map_o_thms, folded_ctor_map_thms), folded_ctor_set_thmss',
+ (timer, Ibnfs, (ctor_Imap_o_thms, ctor_Imap_thms), ctor_Iset_thmss',
ctor_Irel_thms, Ibnf_common_notes @ Ibnf_notes, lthy)
end;
- val ctor_fold_o_map_thms = mk_xtor_un_fold_o_map_thms Least_FP false m ctor_fold_unique_thm
- folded_ctor_map_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s;
- val ctor_rec_o_map_thms = mk_xtor_un_fold_o_map_thms Least_FP true m ctor_rec_unique_thm
- folded_ctor_map_o_thms (map (mk_pointfree lthy) ctor_rec_thms) sym_map_comps map_cong0s;
+ val ctor_fold_o_Imap_thms = mk_xtor_un_fold_o_map_thms Least_FP false m ctor_fold_unique_thm
+ ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_fold_thms) sym_map_comps map_cong0s;
+ val ctor_rec_o_Imap_thms = mk_xtor_un_fold_o_map_thms Least_FP true m ctor_rec_unique_thm
+ ctor_Imap_o_thms (map (mk_pointfree lthy) ctor_rec_thms) sym_map_comps map_cong0s;
val Irels = if m = 0 then map HOLogic.eq_const Ts
else map (mk_rel_of_bnf deads passiveAs passiveBs) Ibnfs;
val Irel_induct_thm =
mk_rel_xtor_co_induct_thm Least_FP rels activeIphis Irels Iphis xFs yFs ctors ctor's
- (mk_rel_induct_tac m ctor_induct2_thm ks ctor_Irel_thms (map rel_mono_strong_of_bnf bnfs))
- lthy;
+ (mk_rel_induct_tac m ctor_induct2_thm ks ctor_Irel_thms rel_mono_strongs) lthy;
val rels = map2 (fn Ds => mk_rel_of_bnf Ds allAs allBs') Dss bnfs;
val ctor_fold_transfer_thms =
@@ -1850,8 +1841,8 @@
(ctor_foldN, ctor_fold_thms),
(ctor_fold_uniqueN, ctor_fold_unique_thms),
(ctor_rec_uniqueN, ctor_rec_unique_thms),
- (ctor_fold_o_mapN, ctor_fold_o_map_thms),
- (ctor_rec_o_mapN, ctor_rec_o_map_thms),
+ (ctor_fold_o_mapN, ctor_fold_o_Imap_thms),
+ (ctor_rec_o_mapN, ctor_rec_o_Imap_thms),
(ctor_injectN, ctor_inject_thms),
(ctor_recN, ctor_rec_thms),
(dtor_ctorN, dtor_ctor_thms),
@@ -1871,10 +1862,10 @@
({Ts = Ts, bnfs = Ibnfs, ctors = ctors, dtors = dtors, xtor_co_iterss = transpose [folds, recs],
xtor_co_induct = ctor_induct_thm, dtor_ctors = dtor_ctor_thms, ctor_dtors = ctor_dtor_thms,
ctor_injects = ctor_inject_thms, dtor_injects = dtor_inject_thms,
- xtor_map_thms = folded_ctor_map_thms, xtor_set_thmss = folded_ctor_set_thmss',
+ xtor_map_thms = ctor_Imap_thms, xtor_set_thmss = ctor_Iset_thmss',
xtor_rel_thms = ctor_Irel_thms,
xtor_co_iter_thmss = transpose [ctor_fold_thms, ctor_rec_thms],
- xtor_co_iter_o_map_thmss = transpose [ctor_fold_o_map_thms, ctor_rec_o_map_thms],
+ xtor_co_iter_o_map_thmss = transpose [ctor_fold_o_Imap_thms, ctor_rec_o_Imap_thms],
rel_xtor_co_induct_thm = Irel_induct_thm},
lthy |> Local_Theory.notes (maybe_conceal_notes (common_notes @ notes @ Ibnf_notes)) |> snd)
end;
--- a/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_lfp_tactics.ML Wed Dec 18 11:03:40 2013 +0100
@@ -37,12 +37,12 @@
val mk_fold_transfer_tac: int -> thm -> thm list -> thm list ->
{prems: thm list, context: Proof.context} -> tactic
val mk_least_min_alg_tac: thm -> thm -> tactic
- val mk_lfp_map_wpull_tac: Proof.context -> int -> (int -> tactic) -> thm list -> thm list ->
- thm list list -> thm list list list -> thm list -> tactic
+ val mk_le_rel_OO_tac: int -> thm -> thm list -> thm list -> thm list -> thm list ->
+ {prems: 'a, context: Proof.context} -> tactic
val mk_map_comp0_tac: thm list -> thm list -> thm -> int -> tactic
val mk_map_id0_tac: thm list -> thm -> tactic
val mk_map_tac: int -> int -> thm -> thm -> thm -> tactic
- val mk_ctor_map_unique_tac: thm -> thm list -> {prems: thm list, context: Proof.context} -> tactic
+ val mk_ctor_map_unique_tac: thm -> thm list -> Proof.context -> tactic
val mk_mcong_tac: (int -> tactic) -> thm list list list -> thm list -> thm list ->
{prems: 'a, context: Proof.context} -> tactic
val mk_min_algs_card_of_tac: ctyp -> cterm -> int -> thm -> thm list -> thm list -> thm -> thm ->
@@ -69,13 +69,12 @@
val mk_rec_unique_mor_tac: thm list -> thm list -> thm -> {prems: 'a, context: Proof.context} ->
tactic
val mk_set_bd_tac: int -> (int -> tactic) -> thm -> thm list list -> thm list -> int ->
- {prems: 'a, context: Proof.context} -> tactic
+ Proof.context -> tactic
val mk_set_nat_tac: int -> (int -> tactic) -> thm list list -> thm list -> cterm list ->
thm list -> int -> {prems: 'a, context: Proof.context} -> tactic
val mk_set_map0_tac: thm -> tactic
val mk_set_tac: thm -> tactic
val mk_wit_tac: Proof.context -> int -> thm list -> thm list -> tactic
- val mk_wpull_tac: thm -> tactic
end;
structure BNF_LFP_Tactics : BNF_LFP_TACTICS =
@@ -584,7 +583,7 @@
REPEAT_DETERM_N n o (EVERY' (map rtac [trans, o_apply, id_apply])),
rtac sym, rtac o_apply] 1;
-fun mk_ctor_map_unique_tac fold_unique sym_map_comps {context = ctxt, prems = _} =
+fun mk_ctor_map_unique_tac fold_unique sym_map_comps ctxt =
rtac fold_unique 1 THEN
unfold_thms_tac ctxt (sym_map_comps @ @{thms o_assoc[symmetric] id_o o_id}) THEN
ALLGOALS atac;
@@ -624,7 +623,7 @@
(induct_tac THEN' EVERY' (map4 mk_set_nat csets ctor_maps ctor_sets set_mapss)) 1
end;
-fun mk_set_bd_tac m induct_tac bd_Cinfinite set_bdss ctor_sets i {context = ctxt, prems = _} =
+fun mk_set_bd_tac m induct_tac bd_Cinfinite set_bdss ctor_sets i ctxt =
let
val n = length ctor_sets;
@@ -658,49 +657,18 @@
(induct_tac THEN' EVERY' (map3 mk_map_cong0 ctor_maps map_cong0s set_setsss)) 1
end;
-fun mk_lfp_map_wpull_tac ctxt m induct_tac wpulls ctor_maps ctor_setss set_setsss ctor_injects =
- let
- val n = length wpulls;
- val ks = 1 upto n;
- val ls = 1 upto m;
-
- fun use_pass_asm thm = rtac conjI THEN' etac (thm RS subset_trans);
- fun use_act_asm thm = etac (thm RS subset_trans) THEN' atac;
-
- fun useIH set_sets i = EVERY' [rtac ssubst, rtac @{thm wpull_def},
- REPEAT_DETERM_N m o etac thin_rl, select_prem_tac n (dtac asm_rl) i,
- rtac allI, rtac allI, rtac impI, REPEAT_DETERM o etac conjE,
- REPEAT_DETERM o dtac @{thm meta_spec},
- dtac meta_mp, atac,
- dtac meta_mp, atac, etac mp,
- rtac conjI, rtac CollectI, CONJ_WRAP' use_act_asm set_sets,
- rtac conjI, rtac CollectI, CONJ_WRAP' use_act_asm set_sets,
- atac];
-
- fun mk_subset thm = EVERY' [rtac ord_eq_le_trans, rtac thm, rtac @{thm Un_least}, atac,
- REPEAT_DETERM_N (n - 1) o rtac @{thm Un_least},
- REPEAT_DETERM_N n o
- EVERY' [rtac @{thm UN_least}, rtac CollectE, etac set_rev_mp, atac,
- REPEAT_DETERM o etac conjE, atac]];
-
- fun mk_wpull wpull ctor_map ctor_sets set_setss ctor_inject =
- EVERY' [rtac impI, REPEAT_DETERM o eresolve_tac [CollectE, conjE],
- rtac rev_mp, rtac wpull,
- EVERY' (map (fn i => REPEAT_DETERM_N (i - 1) o etac thin_rl THEN' atac) ls),
- EVERY' (map2 useIH (transpose (map tl set_setss)) ks),
- rtac impI, REPEAT_DETERM_N (m + n) o etac thin_rl,
- dtac @{thm subst[OF wpull_def, of "%x. x"]}, etac allE, etac allE, etac impE,
- rtac conjI, rtac CollectI, EVERY' (map (use_pass_asm o hd) set_setss),
- CONJ_WRAP' (K (rtac subset_refl)) ks,
- rtac conjI, rtac CollectI, EVERY' (map (use_pass_asm o hd) set_setss),
- CONJ_WRAP' (K (rtac subset_refl)) ks,
- rtac subst, rtac ctor_inject, rtac trans, rtac sym, rtac ctor_map,
- rtac trans, atac, rtac ctor_map, REPEAT_DETERM o eresolve_tac [CollectE, conjE, bexE],
- hyp_subst_tac ctxt, rtac bexI, rtac conjI, rtac ctor_map, rtac ctor_map, rtac CollectI,
- CONJ_WRAP' mk_subset ctor_sets];
- in
- (induct_tac THEN' EVERY' (map5 mk_wpull wpulls ctor_maps ctor_setss set_setsss ctor_injects)) 1
- end;
+fun mk_le_rel_OO_tac m induct ctor_nchotomys ctor_Irels rel_mono_strongs rel_OOs
+ {context = ctxt, prems = _} =
+ EVERY' (rtac induct ::
+ map4 (fn nchotomy => fn Irel => fn rel_mono => fn rel_OO =>
+ EVERY' [rtac impI, etac (nchotomy RS @{thm nchotomy_relcomppE}),
+ REPEAT_DETERM_N 2 o dtac (Irel RS iffD1), rtac (Irel RS iffD2),
+ rtac rel_mono, rtac (rel_OO RS @{thm predicate2_eqD} RS iffD2),
+ rtac @{thm relcomppI}, atac, atac,
+ REPEAT_DETERM_N m o EVERY' [rtac ballI, rtac ballI, rtac impI, atac],
+ REPEAT_DETERM_N (length rel_OOs) o
+ EVERY' [rtac ballI, rtac ballI, Goal.assume_rule_tac ctxt]])
+ ctor_nchotomys ctor_Irels rel_mono_strongs rel_OOs) 1;
(* BNF tactics *)
@@ -730,10 +698,6 @@
fun mk_bd_card_order_tac bd_card_orders =
CONJ_WRAP_GEN' (rtac @{thm card_order_csum}) rtac bd_card_orders 1;
-fun mk_wpull_tac wpull =
- EVERY' [rtac ssubst, rtac @{thm wpull_def}, rtac allI, rtac allI,
- rtac wpull, REPEAT_DETERM o atac] 1;
-
fun mk_wit_tac ctxt n ctor_set wit =
REPEAT_DETERM (atac 1 ORELSE
EVERY' [dtac set_rev_mp, rtac equalityD1, resolve_tac ctor_set,
--- a/src/HOL/BNF/Tools/bnf_tactics.ML Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_tactics.ML Wed Dec 18 11:03:40 2013 +0100
@@ -11,7 +11,6 @@
include CTR_SUGAR_GENERAL_TACTICS
val fo_rtac: thm -> Proof.context -> int -> tactic
- val mk_unfold_thms_then_tac: Proof.context -> thm list -> ('a -> tactic) -> 'a -> tactic
val mk_flatten_assoc_tac: (int -> tactic) -> thm -> thm -> thm -> tactic
val mk_rotate_eq_tac: (int -> tactic) -> thm -> thm -> thm -> thm -> ''a list -> ''a list ->
@@ -45,8 +44,6 @@
rtac (Drule.instantiate_normalize insts thm) 1
end);
-fun mk_unfold_thms_then_tac ctxt defs tac x = unfold_thms_tac ctxt defs THEN tac x;
-
(*transforms f (g x) = h (k x) into f o g = h o k using first order matches for f, g, h, and k*)
fun mk_pointfree ctxt thm = thm
|> Thm.prop_of |> HOLogic.dest_Trueprop |> HOLogic.dest_eq
--- a/src/HOL/BNF/Tools/bnf_util.ML Fri Dec 20 21:09:01 2013 +0100
+++ b/src/HOL/BNF/Tools/bnf_util.ML Wed Dec 18 11:03:40 2013 +0100
@@ -45,6 +45,7 @@
'a list -> 'b list -> 'c list -> 'd list -> 'e list -> 'f list -> 'g list -> 'h list ->
'i list -> 'j -> 'k list * 'j
val split_list4: ('a * 'b * 'c * 'd) list -> 'a list * 'b list * 'c list * 'd list
+ val split_list5: ('a * 'b * 'c * 'd * 'e) list -> 'a list * 'b list * 'c list * 'd list * 'e list
val find_indices: ('b * 'a -> bool) -> 'a list -> 'b list -> int list
val mk_TFreess: int list -> Proof.context -> typ list list * Proof.context
@@ -98,7 +99,6 @@
val mk_ordLeq: term -> term -> term
val mk_rel_comp: term * term -> term
val mk_rel_compp: term * term -> term
- val mk_wpull: term -> term -> term -> term -> term -> (term * term) option -> term -> term -> term
(*parameterized terms*)
val mk_nthN: int -> term -> int -> term
@@ -252,6 +252,11 @@
let val (xs1, xs2, xs3, xs4) = split_list4 xs;
in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4) end;
+fun split_list5 [] = ([], [], [], [], [])
+ | split_list5 ((x1, x2, x3, x4, x5) :: xs) =
+ let val (xs1, xs2, xs3, xs4, xs5) = split_list5 xs;
+ in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4, x5 :: xs5) end;
+
val parse_binding_colon = parse_binding --| @{keyword ":"};
val parse_opt_binding_colon = Scan.optional parse_binding_colon Binding.empty;
@@ -460,39 +465,6 @@
else HOLogic.mk_UNIV T
end;
-fun mk_wpull A B1 B2 f1 f2 pseudo p1 p2 =
- let
- val AT = fastype_of A;
- val BT1 = fastype_of B1;
- val BT2 = fastype_of B2;
- val FT1 = fastype_of f1;
- val FT2 = fastype_of f2;
- val PT1 = fastype_of p1;
- val PT2 = fastype_of p2;
- val T1 = HOLogic.dest_setT BT1;
- val T2 = HOLogic.dest_setT BT2;
- val domP = domain_type PT1;
- val ranF = range_type FT1;
- val _ = if is_some pseudo orelse
- (HOLogic.dest_setT AT = domP andalso
- domain_type FT1 = T1 andalso
- domain_type FT2 = T2 andalso
- domain_type PT2 = domP andalso
- range_type PT1 = T1 andalso
- range_type PT2 = T2 andalso
- range_type FT2 = ranF)
- then () else raise TYPE ("mk_wpull", [BT1, BT2, FT1, FT2, PT1, PT2], []);
- in
- (case pseudo of
- NONE => Const (@{const_name wpull},
- AT --> BT1 --> BT2 --> FT1 --> FT2 --> PT1 --> PT2 --> HOLogic.boolT) $
- A $ B1 $ B2 $ f1 $ f2 $ p1 $ p2
- | SOME (e1, e2) => Const (@{const_name wppull},
- AT --> BT1 --> BT2 --> FT1 --> FT2 --> fastype_of e1 --> fastype_of e2 -->
- PT1 --> PT2 --> HOLogic.boolT) $
- A $ B1 $ B2 $ f1 $ f2 $ e1 $ e2 $ p1 $ p2)
- end;
-
fun mk_leq t1 t2 =
Const (@{const_name less_eq}, (fastype_of t1) --> (fastype_of t2) --> HOLogic.boolT) $ t1 $ t2;