# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264677889 -3600
# Node ID 9d35c6145dd208f9123609209a477b6762fabaec
# Parent  a88e16b69d0f891143f32579e7b0581aa30f45c2
Renamed Bexeq to Bex1_rel

diff -r a88e16b69d0f -r 9d35c6145dd2 Attic/Unused.thy
--- a/Attic/Unused.thy	Thu Jan 28 10:52:10 2010 +0100
+++ b/Attic/Unused.thy	Thu Jan 28 12:24:49 2010 +0100
@@ -6,9 +6,9 @@
   by(auto simp add: QUOT_TRUE_def)
 
 syntax
-  "Bexeq" :: "id \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("(3\<exists>!!_\<in>_./ _)" [0, 0, 10] 10)
+  "Bex1_rel" :: "id \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" ("(3\<exists>!!_\<in>_./ _)" [0, 0, 10] 10)
 translations
-  "\<exists>!!x\<in>A. P"  == "Bexeq A (%x. P)"
+  "\<exists>!!x\<in>A. P"  == "Bex1_rel A (%x. P)"
 
 
 (* Atomize infrastructure *)
diff -r a88e16b69d0f -r 9d35c6145dd2 Quot/Examples/SigmaEx.thy
--- a/Quot/Examples/SigmaEx.thy	Thu Jan 28 10:52:10 2010 +0100
+++ b/Quot/Examples/SigmaEx.thy	Thu Jan 28 12:24:49 2010 +0100
@@ -128,8 +128,8 @@
 sorry
 
   
-lemma bex1_bex1reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bexeq R (\<lambda>x. P x))"
-apply (simp add: Bex1_def Ex1_def Bexeq_def in_respects)
+lemma bex1_bex1reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
+apply (simp add: Bex1_def Ex1_def Bex1_rel_def in_respects)
 apply clarify
 apply auto
 apply (rule bexI)
@@ -207,10 +207,10 @@
  \<forall> fpar\<in>Respects (op = ===> op = ===> alpha_method ===> op =).
  \<forall> fsgm\<in>Respects (op = ===> (op = ===> alpha_obj) ===> op =).
 
- Bexeq (alpha_obj ===> op =) (\<lambda>hom_o\<Colon>robj \<Rightarrow> 'a .
- Bexeq (list_rel (prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b.
- Bexeq ((prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c.
- Bexeq (alpha_method ===> op =) (\<lambda>hom_m\<Colon>rmethod \<Rightarrow> 'd.
+ Bex1_rel (alpha_obj ===> op =) (\<lambda>hom_o\<Colon>robj \<Rightarrow> 'a .
+ Bex1_rel (list_rel (prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_d\<Colon>(char list \<times> rmethod) list \<Rightarrow> 'b.
+ Bex1_rel ((prod_rel (op =) alpha_method) ===> op =) (\<lambda>hom_e\<Colon>char list \<times> rmethod \<Rightarrow> 'c.
+ Bex1_rel (alpha_method ===> op =) (\<lambda>hom_m\<Colon>rmethod \<Rightarrow> 'd.
 (
  (\<forall>x. hom_o (rVar x) = fvar x) \<and>
  (\<forall>d. hom_o (rObj d) = fobj (hom_d d) d) \<and>
diff -r a88e16b69d0f -r 9d35c6145dd2 Quot/QuotBase.thy
--- a/Quot/QuotBase.thy	Thu Jan 28 10:52:10 2010 +0100
+++ b/Quot/QuotBase.thy	Thu Jan 28 12:24:49 2010 +0100
@@ -451,19 +451,19 @@
   using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply
   by metis
 
-section {* Bexeq quantifier *}
+section {* Bex1_rel quantifier *}
 
 definition
-  Bexeq :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
+  Bex1_rel :: "('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)))"
+  "Bex1_rel 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)"
+  shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
 apply simp
-unfolding Bexeq_def
+unfolding Bex1_rel_def
 apply rule
 apply rule
 apply rule
@@ -500,9 +500,9 @@
 
 lemma ex1_prs:
   assumes a: "Quotient R absf repf"
-  shows "((absf ---> id) ---> id) (Bexeq R) f = Ex1 f"
+  shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f"
 apply simp
-apply (subst Bexeq_def)
+apply (subst Bex1_rel_def)
 apply (subst Bex_def)
 apply (subst Ex1_def)
 apply simp
@@ -535,8 +535,8 @@
 apply metis
 done
 
-lemma bex1_bexeq_reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bexeq R (\<lambda>x. P x))"
-  apply (simp add: Bex1_def Ex1_def Bexeq_def in_respects)
+lemma bex1_bexeq_reg: "(\<exists>!x\<in>Respects R. P x) \<longrightarrow> (Bex1_rel R (\<lambda>x. P x))"
+  apply (simp add: Bex1_def Ex1_def Bex1_rel_def in_respects)
   apply clarify
   apply auto
   apply (rule bexI)
diff -r a88e16b69d0f -r 9d35c6145dd2 Quot/quotient_tacs.ML
--- a/Quot/quotient_tacs.ML	Thu Jan 28 10:52:10 2010 +0100
+++ b/Quot/quotient_tacs.ML	Thu Jan 28 12:24:49 2010 +0100
@@ -366,7 +366,7 @@
       => rtac @{thm fun_rel_id} THEN' quot_true_tac ctxt unlam
 
 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
-    (Const(@{const_name Bexeq},_) $ _) $ (Const(@{const_name Bexeq},_) $ _)
+    (Const(@{const_name Bex1_rel},_) $ _) $ (Const(@{const_name Bex1_rel},_) $ _)
       => rtac @{thm bexeq_rsp} THEN' quotient_tac ctxt
 
 | (_ $