diff -r 8d3f92694e85 -r d1eaed018e5d Quot/QuotBase.thy
--- a/Quot/QuotBase.thy	Wed Feb 10 12:30:26 2010 +0100
+++ b/Quot/QuotBase.thy	Wed Feb 10 17:02:29 2010 +0100
@@ -3,7 +3,7 @@
 *)
 
 theory QuotBase
-imports Plain ATP_Linkup Predicate
+imports Plain ATP_Linkup
 begin
 
 text {*
@@ -11,17 +11,18 @@
   that are represented by predicates.
 *}
 
+(* TODO check where definitions can be changed to \<longleftrightarrow> *)
 definition
-  "equivp E \<equiv> \<forall>x y. E x y = (E x = E y)"
+  "equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))"
 
 definition
-  "reflp E \<equiv> \<forall>x. E x x"
+  "reflp E \<longleftrightarrow> (\<forall>x. E x x)"
 
 definition
-  "symp E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
+  "symp E \<longleftrightarrow> (\<forall>x y. E x y \<longrightarrow> E y x)"
 
 definition
-  "transp E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
+  "transp E \<longleftrightarrow> (\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)"
 
 lemma equivp_reflp_symp_transp:
   shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
@@ -29,15 +30,15 @@
   by blast
 
 lemma equivp_reflp:
-  shows "equivp E \<Longrightarrow> (\<And>x. E x x)"
+  shows "equivp E \<Longrightarrow> E x x"
   by (simp only: equivp_reflp_symp_transp reflp_def)
 
 lemma equivp_symp:
-  shows "equivp E \<Longrightarrow> (\<And>x y. E x y \<Longrightarrow> E y x)"
+  shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x"
   by (metis equivp_reflp_symp_transp symp_def)
 
 lemma equivp_transp:
-  shows "equivp E \<Longrightarrow> (\<And>x y z. E x y \<Longrightarrow> E y z \<Longrightarrow> E x z)"
+  shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z"
   by (metis equivp_reflp_symp_transp transp_def)
 
 lemma equivpI:
@@ -57,7 +58,7 @@
 
 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)))"
+  "part_equivp E \<longleftrightarrow> ((\<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_implies_part_equivp:
   assumes a: "equivp E"
@@ -81,7 +82,7 @@
 definition
   Respects
 where
-  "Respects R x \<equiv> (R x x)"
+  "Respects R x \<longleftrightarrow> (R x x)"
 
 lemma in_respects:
   shows "(x \<in> Respects R) = R x x"
@@ -123,7 +124,7 @@
 section {* Quotient Predicate *}
 
 definition
-  "Quotient E Abs Rep \<equiv> 
+  "Quotient E Abs Rep \<longleftrightarrow>
      (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and>
      (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
 
@@ -378,7 +379,7 @@
 definition
   Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
 where
-  "(x \<in> p) \<Longrightarrow> (Babs p m x = m x)"
+  "x \<in> p \<Longrightarrow> Babs p m x = m x"
 
 lemma babs_rsp:
   assumes q: "Quotient R1 Abs1 Rep1"
@@ -456,7 +457,7 @@
 definition
   Bex1_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"
 where
-  "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)))"
+  "Bex1_rel R P \<longleftrightarrow> (\<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)))"
 
 lemma bex1_rel_aux:
   "\<lbrakk>\<forall>xa ya. R xa ya \<longrightarrow> x xa = y ya; Bex1_rel R x\<rbrakk> \<Longrightarrow> Bex1_rel R y"
@@ -613,102 +614,5 @@
   shows "R2 ((Let x f)::'c) ((Let y g)::'c)"
   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
-  by (simp add: expand_fun_eq)
-
-lemma respects_rep_abs:
-  assumes a: "Quotient R1 Abs1 Rep1"
-  and     b: "Respects (R1 ===> R2) f"
-  and     c: "R1 x x"
-  shows "R2 (f (Rep1 (Abs1 x))) (f x)"
-  using a b[simplified respects_thm] c unfolding Quotient_def
-  by blast
-
-lemma respects_mp:
-  assumes a: "Respects (R1 ===> R2) f"
-  and     b: "R1 x y"
-  shows "R2 (f x) (f y)"
-  using a b unfolding Respects_def
-  by simp
-
-lemma respects_o:
-  assumes a: "Respects (R2 ===> R3) f"
-  and     b: "Respects (R1 ===> R2) g"
-  shows "Respects (R1 ===> R3) (f o g)"
-  using a b unfolding Respects_def
-  by simp
-
-lemma fun_rel_eq_rel:
-  assumes q1: "Quotient R1 Abs1 Rep1"
-  and     q2: "Quotient R2 Abs2 Rep2"
-  shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g)
-                             \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))"
-  using fun_quotient[OF q1 q2] unfolding Respects_def Quotient_def expand_fun_eq
-  by blast
-
-lemma let_babs:
-  "v \<in> r \<Longrightarrow> Let v (Babs r lam) = Let v lam"
-  by (simp add: Babs_def)
-
-lemma fun_rel_equals:
-  assumes q1: "Quotient R1 Abs1 Rep1"
-  and     q2: "Quotient R2 Abs2 Rep2"
-  and     r1: "Respects (R1 ===> R2) f"
-  and     r2: "Respects (R1 ===> R2) g"
-  shows "((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g) = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))"
-  apply(rule_tac iffI)
-  apply(rule)+
-  apply (rule apply_rsp'[of "R1" "R2"])
-  apply(subst Quotient_rel[OF fun_quotient[OF q1 q2]])
-  apply auto
-  using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def
-  apply (metis let_rsp q1)
-  apply (metis fun_rel_eq_rel let_rsp q1 q2 r2)
-  using r1 unfolding Respects_def expand_fun_eq
-  apply(simp (no_asm_use))
-  apply(metis Quotient_rel[OF q2] Quotient_rel_rep[OF q1])
-  done
-
-(* ask Peter: fun_rel_IMP used twice *) 
-lemma fun_rel_IMP2:
-  assumes q1: "Quotient R1 Abs1 Rep1"
-  and     q2: "Quotient R2 Abs2 Rep2"
-  and     r1: "Respects (R1 ===> R2) f"
-  and     r2: "Respects (R1 ===> R2) g" 
-  and     a:  "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g"
-  shows "R1 x y \<Longrightarrow> R2 (f x) (g y)"
-  using q1 q2 r1 r2 a
-  by (simp add: fun_rel_equals)
-
-lemma lambda_rep_abs_rsp:
-  assumes r1: "\<And>r r'. R1 r r' \<Longrightarrow>R1 r (Rep1 (Abs1 r'))"
-  and     r2: "\<And>r r'. R2 r r' \<Longrightarrow>R2 r (Rep2 (Abs2 r'))"
-  shows "(R1 ===> R2) f1 f2 \<Longrightarrow> (R1 ===> R2) f1 ((Abs1 ---> Rep2) ((Rep1 ---> Abs2) f2))"
-  using r1 r2 by auto
-
-(* We use id_simps which includes id_apply; so these 2 theorems can be removed *)
-lemma id_prs:
-  assumes q: "Quotient R Abs Rep"
-  shows "Abs (id (Rep e)) = id e"
-  using Quotient_abs_rep[OF q] by auto
-
-lemma id_rsp:
-  assumes q: "Quotient R Abs Rep"
-  and     a: "R e1 e2"
-  shows "R (id e1) (id e2)"
-  using a by auto
-
-*}
-
 end