--- a/FIXME-TODO	Mon Jan 25 18:13:44 2010 +0100
+++ b/FIXME-TODO	Mon Jan 25 18:52:22 2010 +0100
@@ -4,6 +4,12 @@
 Higher Priority
 ===============
 
+- Ask Markus how the files Quot* should be named.
+  (There is a HOL/Library/Quotient.thy --- seems to be an example. *)
+
+- Is Bexeq the right name?
+
+
 - If the constant definition gives the wrong definition
   term, one gets a cryptic message about absrep_fun
 

--- a/Quot/QuotBase.thy	Mon Jan 25 18:13:44 2010 +0100
+++ b/Quot/QuotBase.thy	Mon Jan 25 18:52:22 2010 +0100
@@ -49,11 +49,17 @@
   shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" 
 by (simp add: equivp_reflp)
 
+lemma identity_equivp:
+  shows "equivp (op =)"
+  unfolding equivp_def
+  by auto
+
+
 text {* Partial equivalences: not yet used anywhere *}
 definition
   "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
 
-lemma equivp_IMP_part_equivp:
+lemma equivp_implies_part_equivp:
   assumes a: "equivp E"
   shows "part_equivp E"
   using a 
@@ -66,6 +72,56 @@
 where
   "r1 OOO r2 \<equiv> r1 OO r2 OO r1"
 
+lemma eq_comp_r: "op = OO R OO op = \<equiv> R"
+  apply (rule eq_reflection)
+  apply (rule ext)+
+  apply auto
+  done
+
+section {* Respects predicate *}
+
+definition
+  Respects
+where
+  "Respects R x \<equiv> (R x x)"
+
+lemma in_respects:
+  shows "(x \<in> Respects R) = R x x"
+  unfolding mem_def Respects_def 
+  by simp
+
+section {* Function map and function relation *}
+
+definition
+  fun_map (infixr "--->" 55)
+where
+[simp]: "fun_map f g h x = g (h (f x))"
+
+definition
+  fun_rel (infixr "===>" 55)
+where
+[simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
+
+
+lemma fun_map_id:
+  shows "(id ---> id) = id"
+  by (simp add: expand_fun_eq id_def)
+
+lemma fun_rel_eq:
+  shows "(op =) ===> (op =) \<equiv> (op =)"
+  by (rule eq_reflection) (simp add: expand_fun_eq)
+
+lemma fun_rel_id:
+  assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
+  shows "(R1 ===> R2) f g"
+  using a by simp
+
+lemma fun_rel_id_asm:
+  assumes a: "\<And>x y. R1 x y \<Longrightarrow> (A \<longrightarrow> R2 (f x) (g y))"
+  shows "A \<longrightarrow> (R1 ===> R2) f g"
+  using a by auto
+
+
 section {* Quotient Predicate *}
 
 definition
@@ -125,39 +181,11 @@
   using a unfolding Quotient_def transp_def
   by metis
 
-section {* Lemmas about (op =) *}
-
-lemma identity_equivp:
-  shows "equivp (op =)"
-  unfolding equivp_def
-  by auto
-
 lemma identity_quotient:
   shows "Quotient (op =) id id"
   unfolding Quotient_def id_def
   by blast
 
-section {* Function map and function relation *}
-
-definition
-  fun_map (infixr "--->" 55)
-where
-[simp]: "fun_map f g h x = g (h (f x))"
-
-definition
-  fun_rel (infixr "===>" 55)
-where
-[simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
-
-
-lemma fun_map_id:
-  shows "(id ---> id) = id"
-  by (simp add: expand_fun_eq id_def)
-
-lemma fun_rel_eq:
-  shows "(op =) ===> (op =) \<equiv> (op =)"
-  by (rule eq_reflection) (simp add: expand_fun_eq)
-
 lemma fun_quotient:
   assumes q1: "Quotient R1 abs1 rep1"
   and     q2: "Quotient R2 abs2 rep2"
@@ -192,16 +220,12 @@
     unfolding Quotient_def by blast
 qed
 
-section {* Respects predicate *}
-
-definition
-  Respects
-where
-  "Respects R x \<equiv> (R x x)"
-
-lemma in_respects:
-  shows "(x \<in> Respects R) = R x x"
-  unfolding mem_def Respects_def by simp
+lemma abs_o_rep:
+  assumes a: "Quotient R Abs Rep"
+  shows "Abs o Rep = id"
+  apply(rule ext)
+  apply(simp add: Quotient_abs_rep[OF a])
+  done
 
 lemma equals_rsp:
   assumes q: "Quotient R Abs Rep"
@@ -230,13 +254,15 @@
   assumes q: "Quotient R Abs Rep"
   and     a: "R x1 x2"
   shows "R x1 (Rep (Abs x2))"
-  using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])
+using a 
+by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])
 
 lemma rep_abs_rsp_left:
   assumes q: "Quotient R Abs Rep"
   and     a: "R x1 x2"
   shows "R (Rep (Abs x1)) x2"
-using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])
+using a 
+by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q])
 
 (* In the following theorem R1 can be instantiated with anything,
    but we know some of the types of the Rep and Abs functions;
@@ -255,7 +281,7 @@
   shows "R2 (f x) (g y)"
   using a by simp
 
-(* Set of lemmas for regularisation of ball and bex *)
+section {* lemmas for regularisation of ball and bex *}
 
 lemma ball_reg_eqv:
   fixes P :: "'a \<Rightarrow> bool"
@@ -349,74 +375,13 @@
   "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))"
   by auto
 
-(* Bounded abstraction *)
+section {* Bounded abstraction *}
+
 definition
   Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 where
   "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
 
-definition
-  Bexeq :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
-where
-  "Bexeq R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))"
-
-(* 3 lemmas needed for proving repabs_inj *)
-lemma ball_rsp:
-  assumes a: "(R ===> (op =)) f g"
-  shows "Ball (Respects R) f = Ball (Respects R) g"
-  using a by (simp add: Ball_def in_respects)
-
-lemma bex_rsp:
-  assumes a: "(R ===> (op =)) f g"
-  shows "(Bex (Respects R) f = Bex (Respects R) g)"
-  using a by (simp add: Bex_def in_respects)
-
-lemma bex1_rsp:
-  assumes a: "(R ===> (op =)) f g"
-  shows "(Bex1 (Respects R) f = Bex1 (Respects R) g)"
-  using a 
-by (simp add: Ex1_def Bex1_def in_respects) auto
-
-(* TODO/FIXME: simplify the repetitions in this proof *)
-lemma bexeq_rsp:
-assumes a: "Quotient R absf repf"
-shows "((R ===> op =) ===> op =) (Bexeq R) (Bexeq R)"
-apply simp
-unfolding Bexeq_def
-apply rule
-apply rule
-apply rule
-apply rule
-apply (erule conjE)+
-apply (erule bexE)
-apply rule
-apply (rule_tac x="xa" in bexI)
-apply metis
-apply metis
-apply rule+
-apply (erule_tac x="xb" in ballE)
-prefer 2
-apply (metis)
-apply (erule_tac x="ya" in ballE)
-prefer 2
-apply (metis)
-apply (metis in_respects)
-apply (erule conjE)+
-apply (erule bexE)
-apply rule
-apply (rule_tac x="xa" in bexI)
-apply metis
-apply metis
-apply rule+
-apply (erule_tac x="xb" in ballE)
-prefer 2
-apply (metis)
-apply (erule_tac x="ya" in ballE)
-prefer 2
-apply (metis)
-apply (metis in_respects)
-done
-
 lemma babs_rsp:
   assumes q: "Quotient R1 Abs1 Rep1"
   and     a: "(R1 ===> R2) f g"
@@ -458,6 +423,24 @@
   shows "equivp R \<Longrightarrow> Babs (Respects R) P = P"
   by (simp add: expand_fun_eq Babs_def in_respects equivp_reflp)
 
+
+(* 3 lemmas needed for proving repabs_inj *)
+lemma ball_rsp:
+  assumes a: "(R ===> (op =)) f g"
+  shows "Ball (Respects R) f = Ball (Respects R) g"
+  using a by (simp add: Ball_def in_respects)
+
+lemma bex_rsp:
+  assumes a: "(R ===> (op =)) f g"
+  shows "(Bex (Respects R) f = Bex (Respects R) g)"
+  using a by (simp add: Bex_def in_respects)
+
+lemma bex1_rsp:
+  assumes a: "(R ===> (op =)) f g"
+  shows "(Bex1 (Respects R) f = Bex1 (Respects R) g)"
+  using a 
+by (simp add: Ex1_def Bex1_def in_respects) auto
+
 (* 3 lemmas needed for cleaning of quantifiers *)
 lemma all_prs:
   assumes a: "Quotient R absf repf"
@@ -471,6 +454,53 @@
   using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply
   by metis
 
+section {* Bexeq quantifier *}
+
+definition
+  Bexeq :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+where
+  "Bexeq R P \<equiv> (\<exists>x \<in> Respects R. P x) \<and> (\<forall>x \<in> Respects R. \<forall>y \<in> Respects R. ((P x \<and> P y) \<longrightarrow> (R x y)))"
+
+(* TODO/FIXME: simplify the repetitions in this proof *)
+lemma bexeq_rsp:
+  assumes a: "Quotient R absf repf"
+  shows "((R ===> op =) ===> op =) (Bexeq R) (Bexeq R)"
+apply simp
+unfolding Bexeq_def
+apply rule
+apply rule
+apply rule
+apply rule
+apply (erule conjE)+
+apply (erule bexE)
+apply rule
+apply (rule_tac x="xa" in bexI)
+apply metis
+apply metis
+apply rule+
+apply (erule_tac x="xb" in ballE)
+prefer 2
+apply (metis)
+apply (erule_tac x="ya" in ballE)
+prefer 2
+apply (metis)
+apply (metis in_respects)
+apply (erule conjE)+
+apply (erule bexE)
+apply rule
+apply (rule_tac x="xa" in bexI)
+apply metis
+apply metis
+apply rule+
+apply (erule_tac x="xb" in ballE)
+prefer 2
+apply (metis)
+apply (erule_tac x="ya" in ballE)
+prefer 2
+apply (metis)
+apply (metis in_respects)
+done
+
 lemma ex1_prs:
   assumes a: "Quotient R absf repf"
   shows "((absf ---> id) ---> id) (Bexeq R) f = Ex1 f"
@@ -508,15 +538,7 @@
 apply metis
 done
 
-lemma fun_rel_id:
-  assumes a: "\<And>x y. R1 x y \<Longrightarrow> R2 (f x) (g y)"
-  shows "(R1 ===> R2) f g"
-  using a by simp
-
-lemma fun_rel_id_asm:
-  assumes a: "\<And>x y. R1 x y \<Longrightarrow> (A \<longrightarrow> R2 (f x) (g y))"
-  shows "A \<longrightarrow> (R1 ===> R2) f g"
-  using a by auto
+section {* Various respects and preserve lemmas *}
 
 lemma quot_rel_rsp:
   assumes a: "Quotient R Abs Rep"
@@ -575,16 +597,15 @@
   using apply_rsp[OF q1 a1] a2 by auto
 
 
-
-
 (******************************************)
 (* REST OF THE FILE IS UNUSED (until now) *)
 (******************************************)
 
+text {*
 lemma in_fun:
   shows "x \<in> ((f ---> g) s) = g (f x \<in> s)"
   by (simp add: mem_def)
-
+ 
 lemma respects_thm:
   shows "Respects (R1 ===> R2) f = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (f y))"
   unfolding Respects_def
@@ -612,19 +633,6 @@
   using a b unfolding Respects_def
   by simp
 
-lemma abs_o_rep:
-  assumes a: "Quotient r absf repf"
-  shows "absf o repf = id"
-  apply(rule ext)
-  apply(simp add: Quotient_abs_rep[OF a])
-  done
-
-lemma eq_comp_r: "op = OO R OO op = \<equiv> R"
-  apply (rule eq_reflection)
-  apply (rule ext)+
-  apply auto
-  done
-
 lemma fun_rel_eq_rel:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
@@ -690,5 +698,7 @@
   shows "R (id e1) (id e2)"
   using a by auto
 
+*}
+
 end