1.1 --- a/src/HOL/Quotient.thy	Tue Nov 09 14:02:13 2010 +0100
     1.2 +++ b/src/HOL/Quotient.thy	Tue Nov 09 14:02:13 2010 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4  header {* Definition of Quotient Types *}
     1.5  
     1.6  theory Quotient
     1.7 -imports Plain Hilbert_Choice
     1.8 +imports Plain Hilbert_Choice Equiv_Relations
     1.9  uses
    1.10    ("Tools/Quotient/quotient_info.ML")
    1.11    ("Tools/Quotient/quotient_typ.ML")
    1.12 @@ -21,33 +21,49 @@
    1.13  *}
    1.14  
    1.15  definition
    1.16 -  "equivp E \<equiv> \<forall>x y. E x y = (E x = E y)"
    1.17 +  "reflp E \<longleftrightarrow> (\<forall>x. E x x)"
    1.18 +
    1.19 +lemma refl_reflp:
    1.20 +  "refl A \<longleftrightarrow> reflp (\<lambda>x y. (x, y) \<in> A)"
    1.21 +  by (simp add: refl_on_def reflp_def)
    1.22  
    1.23  definition
    1.24 -  "reflp E \<equiv> \<forall>x. E x x"
    1.25 +  "symp E \<longleftrightarrow> (\<forall>x y. E x y \<longrightarrow> E y x)"
    1.26 +
    1.27 +lemma sym_symp:
    1.28 +  "sym A \<longleftrightarrow> symp (\<lambda>x y. (x, y) \<in> A)"
    1.29 +  by (simp add: sym_def symp_def)
    1.30  
    1.31  definition
    1.32 -  "symp E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
    1.33 +  "transp E \<longleftrightarrow> (\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)"
    1.34 +
    1.35 +lemma trans_transp:
    1.36 +  "trans A \<longleftrightarrow> transp (\<lambda>x y. (x, y) \<in> A)"
    1.37 +  by (auto simp add: trans_def transp_def)
    1.38  
    1.39  definition
    1.40 -  "transp E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
    1.41 +  "equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))"
    1.42  
    1.43  lemma equivp_reflp_symp_transp:
    1.44    shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
    1.45    unfolding equivp_def reflp_def symp_def transp_def fun_eq_iff
    1.46    by blast
    1.47  
    1.48 +lemma equiv_equivp:
    1.49 +  "equiv UNIV A \<longleftrightarrow> equivp (\<lambda>x y. (x, y) \<in> A)"
    1.50 +  by (simp add: equiv_def equivp_reflp_symp_transp refl_reflp sym_symp trans_transp)
    1.51 +
    1.52  lemma equivp_reflp:
    1.53    shows "equivp E \<Longrightarrow> E x x"
    1.54    by (simp only: equivp_reflp_symp_transp reflp_def)
    1.55  
    1.56  lemma equivp_symp:
    1.57    shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y x"
    1.58 -  by (metis equivp_reflp_symp_transp symp_def)
    1.59 +  by (simp add: equivp_def)
    1.60  
    1.61  lemma equivp_transp:
    1.62    shows "equivp E \<Longrightarrow> E x y \<Longrightarrow> E y z \<Longrightarrow> E x z"
    1.63 -  by (metis equivp_reflp_symp_transp transp_def)
    1.64 +  by (simp add: equivp_def)
    1.65  
    1.66  lemma equivpI:
    1.67    assumes "reflp R" "symp R" "transp R"
    1.68 @@ -62,7 +78,7 @@
    1.69  text {* Partial equivalences *}
    1.70  
    1.71  definition
    1.72 -  "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)))"
    1.73 +  "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)))"
    1.74  
    1.75  lemma equivp_implies_part_equivp:
    1.76    assumes a: "equivp E"
    1.77 @@ -114,6 +130,11 @@
    1.78    then show "part_equivp E" unfolding part_equivp_def using a by metis
    1.79  qed
    1.80  
    1.81 +lemma part_equivpI:
    1.82 +  assumes "\<exists>x. R x x" "symp R" "transp R"
    1.83 +  shows "part_equivp R"
    1.84 +  using assms by (simp add: part_equivp_refl_symp_transp)
    1.85 +
    1.86  text {* Composition of Relations *}
    1.87  
    1.88  abbreviation
    1.89 @@ -128,45 +149,54 @@
    1.90  subsection {* Respects predicate *}
    1.91  
    1.92  definition
    1.93 -  Respects
    1.94 +  Respects :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set"
    1.95  where
    1.96 -  "Respects R x \<equiv> R x x"
    1.97 +  "Respects R x = R x x"
    1.98  
    1.99  lemma in_respects:
   1.100 -  shows "(x \<in> Respects R) = R x x"
   1.101 +  shows "x \<in> Respects R \<longleftrightarrow> R x x"
   1.102    unfolding mem_def Respects_def
   1.103    by simp
   1.104  
   1.105  subsection {* Function map and function relation *}
   1.106  
   1.107  definition
   1.108 -  fun_map (infixr "--->" 55)
   1.109 +  fun_map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow> 'd" (infixr "--->" 55)
   1.110  where
   1.111 -[simp]: "fun_map f g h x = g (h (f x))"
   1.112 +  "fun_map f g = (\<lambda>h. g \<circ> h \<circ> f)"
   1.113 +
   1.114 +lemma fun_map_apply [simp]:
   1.115 +  "(f ---> g) h x = g (h (f x))"
   1.116 +  by (simp add: fun_map_def)
   1.117 +
   1.118 +lemma fun_map_id:
   1.119 +  "(id ---> id) = id"
   1.120 +  by (simp add: fun_eq_iff id_def)
   1.121  
   1.122  definition
   1.123 -  fun_rel (infixr "===>" 55)
   1.124 +  fun_rel :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> ('b \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> bool" (infixr "===>" 55)
   1.125  where
   1.126 -[simp]: "fun_rel E1 E2 f g = (\<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
   1.127 +  "fun_rel E1 E2 = (\<lambda>f g. \<forall>x y. E1 x y \<longrightarrow> E2 (f x) (g y))"
   1.128  
   1.129  lemma fun_relI [intro]:
   1.130 -  assumes "\<And>a b. P a b \<Longrightarrow> Q (x a) (y b)"
   1.131 -  shows "(P ===> Q) x y"
   1.132 +  assumes "\<And>x y. E1 x y \<Longrightarrow> E2 (f x) (g y)"
   1.133 +  shows "(E1 ===> E2) f g"
   1.134    using assms by (simp add: fun_rel_def)
   1.135  
   1.136 -lemma fun_map_id:
   1.137 -  shows "(id ---> id) = id"
   1.138 -  by (simp add: fun_eq_iff id_def)
   1.139 +lemma fun_relE:
   1.140 +  assumes "(E1 ===> E2) f g" and "E1 x y"
   1.141 +  obtains "E2 (f x) (g y)"
   1.142 +  using assms by (simp add: fun_rel_def)
   1.143  
   1.144  lemma fun_rel_eq:
   1.145    shows "((op =) ===> (op =)) = (op =)"
   1.146 -  by (simp add: fun_eq_iff)
   1.147 +  by (auto simp add: fun_eq_iff elim: fun_relE)
   1.148  
   1.149  
   1.150  subsection {* Quotient Predicate *}
   1.151  
   1.152  definition
   1.153 -  "Quotient E Abs Rep \<equiv>
   1.154 +  "Quotient E Abs Rep \<longleftrightarrow>
   1.155       (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and>
   1.156       (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
   1.157  
   1.158 @@ -232,21 +262,17 @@
   1.159    and     q2: "Quotient R2 abs2 rep2"
   1.160    shows "Quotient (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)"
   1.161  proof -
   1.162 -  have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
   1.163 -    using q1 q2
   1.164 -    unfolding Quotient_def
   1.165 -    unfolding fun_eq_iff
   1.166 -    by simp
   1.167 +  have "\<And>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a"
   1.168 +    using q1 q2 by (simp add: Quotient_def fun_eq_iff)
   1.169    moreover
   1.170 -  have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
   1.171 -    using q1 q2
   1.172 -    unfolding Quotient_def
   1.173 -    by (simp (no_asm)) (metis)
   1.174 +  have "\<And>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)"
   1.175 +    by (rule fun_relI)
   1.176 +      (insert q1 q2 Quotient_rel_abs [of R1 abs1 rep1] Quotient_rel_rep [of R2 abs2 rep2],
   1.177 +        simp (no_asm) add: Quotient_def, simp)
   1.178    moreover
   1.179 -  have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
   1.180 +  have "\<And>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and>
   1.181          (rep1 ---> abs2) r  = (rep1 ---> abs2) s)"
   1.182 -    unfolding fun_eq_iff
   1.183 -    apply(auto)
   1.184 +    apply(auto simp add: fun_rel_def fun_eq_iff)
   1.185      using q1 q2 unfolding Quotient_def
   1.186      apply(metis)
   1.187      using q1 q2 unfolding Quotient_def
   1.188 @@ -281,7 +307,7 @@
   1.189    shows "(Rep1 ---> Abs2) (\<lambda>x. Rep2 (f (Abs1 x))) = (\<lambda>x. f x)"
   1.190    unfolding fun_eq_iff
   1.191    using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
   1.192 -  by simp
   1.193 +  by (simp add:)
   1.194  
   1.195  lemma lambda_prs1:
   1.196    assumes q1: "Quotient R1 Abs1 Rep1"
   1.197 @@ -289,7 +315,7 @@
   1.198    shows "(Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x) = (\<lambda>x. f x)"
   1.199    unfolding fun_eq_iff
   1.200    using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2]
   1.201 -  by simp
   1.202 +  by (simp add:)
   1.203  
   1.204  lemma rep_abs_rsp:
   1.205    assumes q: "Quotient R Abs Rep"
   1.206 @@ -317,12 +343,12 @@
   1.207    assumes q: "Quotient R1 Abs1 Rep1"
   1.208    and     a: "(R1 ===> R2) f g" "R1 x y"
   1.209    shows "R2 (f x) (g y)"
   1.210 -  using a by simp
   1.211 +  using a by (auto elim: fun_relE)
   1.212  
   1.213  lemma apply_rsp':
   1.214    assumes a: "(R1 ===> R2) f g" "R1 x y"
   1.215    shows "R2 (f x) (g y)"
   1.216 -  using a by simp
   1.217 +  using a by (auto elim: fun_relE)
   1.218  
   1.219  subsection {* lemmas for regularisation of ball and bex *}
   1.220  
   1.221 @@ -370,7 +396,7 @@
   1.222    apply(rule iffI)
   1.223    apply(rule allI)
   1.224    apply(drule_tac x="\<lambda>y. f x" in bspec)
   1.225 -  apply(simp add: in_respects)
   1.226 +  apply(simp add: in_respects fun_rel_def)
   1.227    apply(rule impI)
   1.228    using a equivp_reflp_symp_transp[of "R2"]
   1.229    apply(simp add: reflp_def)
   1.230 @@ -384,7 +410,7 @@
   1.231    apply(auto)
   1.232    apply(rule_tac x="\<lambda>y. f x" in bexI)
   1.233    apply(simp)
   1.234 -  apply(simp add: Respects_def in_respects)
   1.235 +  apply(simp add: Respects_def in_respects fun_rel_def)
   1.236    apply(rule impI)
   1.237    using a equivp_reflp_symp_transp[of "R2"]
   1.238    apply(simp add: reflp_def)
   1.239 @@ -429,7 +455,7 @@
   1.240  subsection {* Bounded abstraction *}
   1.241  
   1.242  definition
   1.243 -  Babs :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
   1.244 +  Babs :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b"
   1.245  where
   1.246    "x \<in> p \<Longrightarrow> Babs p m x = m x"
   1.247  
   1.248 @@ -437,10 +463,10 @@
   1.249    assumes q: "Quotient R1 Abs1 Rep1"
   1.250    and     a: "(R1 ===> R2) f g"
   1.251    shows      "(R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)"
   1.252 -  apply (auto simp add: Babs_def in_respects)
   1.253 +  apply (auto simp add: Babs_def in_respects fun_rel_def)
   1.254    apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
   1.255 -  using a apply (simp add: Babs_def)
   1.256 -  apply (simp add: in_respects)
   1.257 +  using a apply (simp add: Babs_def fun_rel_def)
   1.258 +  apply (simp add: in_respects fun_rel_def)
   1.259    using Quotient_rel[OF q]
   1.260    by metis
   1.261  
   1.262 @@ -449,7 +475,7 @@
   1.263    and     q2: "Quotient R2 Abs2 Rep2"
   1.264    shows "((Rep1 ---> Abs2) (Babs (Respects R1) ((Abs1 ---> Rep2) f))) = f"
   1.265    apply (rule ext)
   1.266 -  apply (simp)
   1.267 +  apply (simp add:)
   1.268    apply (subgoal_tac "Rep1 x \<in> Respects R1")
   1.269    apply (simp add: Babs_def Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2])
   1.270    apply (simp add: in_respects Quotient_rel_rep[OF q1])
   1.271 @@ -460,7 +486,7 @@
   1.272    shows "((R1 ===> R2) (Babs (Respects R1) f) (Babs (Respects R1) g)) = ((R1 ===> R2) f g)"
   1.273    apply(rule iffI)
   1.274    apply(simp_all only: babs_rsp[OF q])
   1.275 -  apply(auto simp add: Babs_def)
   1.276 +  apply(auto simp add: Babs_def fun_rel_def)
   1.277    apply (subgoal_tac "x \<in> Respects R1 \<and> y \<in> Respects R1")
   1.278    apply(metis Babs_def)
   1.279    apply (simp add: in_respects)
   1.280 @@ -478,30 +504,29 @@
   1.281  lemma ball_rsp:
   1.282    assumes a: "(R ===> (op =)) f g"
   1.283    shows "Ball (Respects R) f = Ball (Respects R) g"
   1.284 -  using a by (simp add: Ball_def in_respects)
   1.285 +  using a by (auto simp add: Ball_def in_respects elim: fun_relE)
   1.286  
   1.287  lemma bex_rsp:
   1.288    assumes a: "(R ===> (op =)) f g"
   1.289    shows "(Bex (Respects R) f = Bex (Respects R) g)"
   1.290 -  using a by (simp add: Bex_def in_respects)
   1.291 +  using a by (auto simp add: Bex_def in_respects elim: fun_relE)
   1.292  
   1.293  lemma bex1_rsp:
   1.294    assumes a: "(R ===> (op =)) f g"
   1.295    shows "Ex1 (\<lambda>x. x \<in> Respects R \<and> f x) = Ex1 (\<lambda>x. x \<in> Respects R \<and> g x)"
   1.296 -  using a
   1.297 -  by (simp add: Ex1_def in_respects) auto
   1.298 +  using a by (auto elim: fun_relE simp add: Ex1_def in_respects) 
   1.299  
   1.300  (* 2 lemmas needed for cleaning of quantifiers *)
   1.301  lemma all_prs:
   1.302    assumes a: "Quotient R absf repf"
   1.303    shows "Ball (Respects R) ((absf ---> id) f) = All f"
   1.304 -  using a unfolding Quotient_def Ball_def in_respects fun_map_def id_apply
   1.305 +  using a unfolding Quotient_def Ball_def in_respects id_apply comp_def fun_map_def
   1.306    by metis
   1.307  
   1.308  lemma ex_prs:
   1.309    assumes a: "Quotient R absf repf"
   1.310    shows "Bex (Respects R) ((absf ---> id) f) = Ex f"
   1.311 -  using a unfolding Quotient_def Bex_def in_respects fun_map_def id_apply
   1.312 +  using a unfolding Quotient_def Bex_def in_respects id_apply comp_def fun_map_def
   1.313    by metis
   1.314  
   1.315  subsection {* @{text Bex1_rel} quantifier *}
   1.316 @@ -552,7 +577,7 @@
   1.317  lemma bex1_rel_rsp:
   1.318    assumes a: "Quotient R absf repf"
   1.319    shows "((R ===> op =) ===> op =) (Bex1_rel R) (Bex1_rel R)"
   1.320 -  apply simp
   1.321 +  apply (simp add: fun_rel_def)
   1.322    apply clarify
   1.323    apply rule
   1.324    apply (simp_all add: bex1_rel_aux bex1_rel_aux2)
   1.325 @@ -564,7 +589,7 @@
   1.326  lemma ex1_prs:
   1.327    assumes a: "Quotient R absf repf"
   1.328    shows "((absf ---> id) ---> id) (Bex1_rel R) f = Ex1 f"
   1.329 -apply simp
   1.330 +apply (simp add:)
   1.331  apply (subst Bex1_rel_def)
   1.332  apply (subst Bex_def)
   1.333  apply (subst Ex1_def)
   1.334 @@ -643,12 +668,12 @@
   1.335    shows "((Abs2 ---> Rep3) ---> (Abs1 ---> Rep2) ---> (Rep1 ---> Abs3)) op \<circ> = op \<circ>"
   1.336    and   "(id ---> (Abs1 ---> id) ---> Rep1 ---> id) op \<circ> = op \<circ>"
   1.337    using Quotient_abs_rep[OF q1] Quotient_abs_rep[OF q2] Quotient_abs_rep[OF q3]
   1.338 -  unfolding o_def fun_eq_iff by simp_all
   1.339 +  by (simp_all add: fun_eq_iff)
   1.340  
   1.341  lemma o_rsp:
   1.342    "((R2 ===> R3) ===> (R1 ===> R2) ===> (R1 ===> R3)) op \<circ> op \<circ>"
   1.343    "(op = ===> (R1 ===> op =) ===> R1 ===> op =) op \<circ> op \<circ>"
   1.344 -  unfolding fun_rel_def o_def fun_eq_iff by auto
   1.345 +  by (auto intro!: fun_relI elim: fun_relE)
   1.346  
   1.347  lemma cond_prs:
   1.348    assumes a: "Quotient R absf repf"
   1.349 @@ -664,7 +689,7 @@
   1.350  lemma if_rsp:
   1.351    assumes q: "Quotient R Abs Rep"
   1.352    shows "(op = ===> R ===> R ===> R) If If"
   1.353 -  by auto
   1.354 +  by (auto intro!: fun_relI)
   1.355  
   1.356  lemma let_prs:
   1.357    assumes q1: "Quotient R1 Abs1 Rep1"
   1.358 @@ -675,11 +700,11 @@
   1.359  
   1.360  lemma let_rsp:
   1.361    shows "(R1 ===> (R1 ===> R2) ===> R2) Let Let"
   1.362 -  by auto
   1.363 +  by (auto intro!: fun_relI elim: fun_relE)
   1.364  
   1.365  lemma mem_rsp:
   1.366    shows "(R1 ===> (R1 ===> R2) ===> R2) op \<in> op \<in>"
   1.367 -  by (simp add: mem_def)
   1.368 +  by (auto intro!: fun_relI elim: fun_relE simp add: mem_def)
   1.369  
   1.370  lemma mem_prs:
   1.371    assumes a1: "Quotient R1 Abs1 Rep1"
   1.372 @@ -689,13 +714,12 @@
   1.373  
   1.374  lemma id_rsp:
   1.375    shows "(R ===> R) id id"
   1.376 -  by simp
   1.377 +  by (auto intro: fun_relI)
   1.378  
   1.379  lemma id_prs:
   1.380    assumes a: "Quotient R Abs Rep"
   1.381    shows "(Rep ---> Abs) id = id"
   1.382 -  unfolding fun_eq_iff
   1.383 -  by (simp add: Quotient_abs_rep[OF a])
   1.384 +  by (simp add: fun_eq_iff Quotient_abs_rep [OF a])
   1.385  
   1.386  
   1.387  locale quot_type =
   1.388 @@ -710,12 +734,12 @@
   1.389  begin
   1.390  
   1.391  definition
   1.392 -  abs::"'a \<Rightarrow> 'b"
   1.393 +  abs :: "'a \<Rightarrow> 'b"
   1.394  where
   1.395 -  "abs x \<equiv> Abs (R x)"
   1.396 +  "abs x = Abs (R x)"
   1.397  
   1.398  definition
   1.399 -  rep::"'b \<Rightarrow> 'a"
   1.400 +  rep :: "'b \<Rightarrow> 'a"
   1.401  where
   1.402    "rep a = Eps (Rep a)"
   1.403  
   1.404 @@ -799,7 +823,9 @@
   1.405    about the lifted theorem in a tactic.
   1.406  *}
   1.407  definition
   1.408 -  "Quot_True (x :: 'a) \<equiv> True"
   1.409 +  Quot_True :: "'a \<Rightarrow> bool"
   1.410 +where
   1.411 +  "Quot_True x \<longleftrightarrow> True"
   1.412  
   1.413  lemma
   1.414    shows QT_all: "Quot_True (All P) \<Longrightarrow> Quot_True P"
   1.415 @@ -858,4 +884,3 @@
   1.416    fun_rel (infixr "===>" 55)
   1.417  
   1.418  end
   1.419 -