avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)
authorhaftmann
Fri Aug 26 18:23:33 2011 +0200 (2011-08-26)
changeset 445534d39b032a021
parent 44552 4a36624c3db6
child 44554 a24b97aeec0c
avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)
src/HOL/Quotient.thy
     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