src/HOL/BNF/BNF_Def.thy

--- 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)