src/HOL/Quotient.thy
 changeset 44553 4d39b032a021 parent 44413 80d460bc6fa8 child 44921 58eef4843641
```     1.1 --- a/src/HOL/Quotient.thy	Thu Aug 25 23:32:12 2011 +0200
1.2 +++ b/src/HOL/Quotient.thy	Fri Aug 26 18:23:33 2011 +0200
1.3 @@ -35,12 +35,11 @@
1.4  definition
1.5    Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set"
1.6  where
1.7 -  "Respects R x = R x x"
1.8 +  "Respects R = {x. R x x}"
1.9
1.10  lemma in_respects:
1.11    shows "x \<in> Respects R \<longleftrightarrow> R x x"
1.12 -  unfolding mem_def Respects_def
1.13 -  by simp
1.14 +  unfolding Respects_def by simp
1.15
1.16  subsection {* Function map and function relation *}
1.17
1.18 @@ -268,14 +267,14 @@
1.19    by (auto simp add: in_respects)
1.20
1.21  lemma ball_reg_right:
1.22 -  assumes a: "\<And>x. R x \<Longrightarrow> P x \<longrightarrow> Q x"
1.23 +  assumes a: "\<And>x. x \<in> R \<Longrightarrow> P x \<longrightarrow> Q x"
1.24    shows "All P \<longrightarrow> Ball R Q"
1.25 -  using a by (metis Collect_def Collect_mem_eq)
1.26 +  using a by (metis Collect_mem_eq)
1.27
1.28  lemma bex_reg_left:
1.29 -  assumes a: "\<And>x. R x \<Longrightarrow> Q x \<longrightarrow> P x"
1.30 +  assumes a: "\<And>x. x \<in> R \<Longrightarrow> Q x \<longrightarrow> P x"
1.31    shows "Bex R Q \<longrightarrow> Ex P"
1.32 -  using a by (metis Collect_def Collect_mem_eq)
1.33 +  using a by (metis Collect_mem_eq)
1.34
1.35  lemma ball_reg_left:
1.36    assumes a: "equivp R"
1.37 @@ -327,16 +326,16 @@
1.38    using a b by metis
1.39
1.40  lemma ball_reg:
1.41 -  assumes a: "!x :: 'a. (R x --> P x --> Q x)"
1.42 +  assumes a: "!x :: 'a. (x \<in> R --> P x --> Q x)"
1.43    and     b: "Ball R P"
1.44    shows "Ball R Q"
1.45 -  using a b by (metis Collect_def Collect_mem_eq)
1.46 +  using a b by (metis Collect_mem_eq)
1.47
1.48  lemma bex_reg:
1.49 -  assumes a: "!x :: 'a. (R x --> P x --> Q x)"
1.50 +  assumes a: "!x :: 'a. (x \<in> R --> P x --> Q x)"
1.51    and     b: "Bex R P"
1.52    shows "Bex R Q"
1.53 -  using a b by (metis Collect_def Collect_mem_eq)
1.54 +  using a b by (metis Collect_mem_eq)
1.55
1.56
1.57  lemma ball_all_comm:
1.58 @@ -599,16 +598,6 @@
1.59    shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
1.60    by (auto intro!: fun_relI elim: fun_relE)
1.61
1.62 -lemma mem_rsp:
1.63 -  shows "(R1 ===> (R1 ===> R2) ===> R2) op \<in> op \<in>"
1.64 -  by (auto intro!: fun_relI elim: fun_relE simp add: mem_def)
1.65 -
1.66 -lemma mem_prs:
1.67 -  assumes a1: "Quotient R1 Abs1 Rep1"
1.68 -  and     a2: "Quotient R2 Abs2 Rep2"
1.69 -  shows "(Rep1 ---> (Abs1 ---> Rep2) ---> Abs2) op \<in> = op \<in>"
1.70 -  by (simp add: fun_eq_iff mem_def Quotient_abs_rep[OF a1] Quotient_abs_rep[OF a2])
1.71 -
1.72  lemma id_rsp:
1.73    shows "(R ===> R) id id"
1.74    by (auto intro: fun_relI)
1.75 @@ -686,8 +675,8 @@
1.76  declare [[map set = (vimage, set_rel)]]
1.77
1.78  lemmas [quot_thm] = fun_quotient
1.79 -lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp mem_rsp id_rsp
1.80 -lemmas [quot_preserve] = if_prs o_prs let_prs mem_prs id_prs
1.81 +lemmas [quot_respect] = quot_rel_rsp if_rsp o_rsp let_rsp id_rsp
1.82 +lemmas [quot_preserve] = if_prs o_prs let_prs id_prs
1.83  lemmas [quot_equiv] = identity_equivp
1.84
1.85
```